LLVM contract attributes: adopting the rest of the vocabulary
Plan note (2026-10-26, user question: what else like musttail should
we adopt from LLVM). The pattern: Cinch’s type/effect/ownership
analyses already prove most of what LLVM’s attribute vocabulary
asserts, so adoption is translation, not new analysis. No em dashes.
Translate from existing analyses (implementation in the P20/P18 era)
- Effect-derived function attributes: an empty effect row with no
foreign calls becomes
memory(none) speculatable;Io-headed or mutating definitions becomememory(read)/memory(readwrite); P20#[no-alloc]addsnofree;willreturnonly where the totality/boundedmachinery proves return (never guessed). - Usage-derived parameter attributes: P5 non-escape becomes
captures(none); P11 non-null default becomesnonnull; scalars getnoundef;repr/layout facts givealign(and!alignon loads through borrows). !rangemetadata from primitive widths,Fin n,Bool, and literal range checking, on returns and typed loads.llvm.assumewith operand bundles (align,nonnull,dereferenceable,range) from P20’s verified assertions andreprfacts. A satisfied safety assertion becomes an optimizer input; the IR carries a second machine-readable statement of the contract.noreturnon fault functions +unreachableafter fault calls (audit pass: every fault path should mark its successor dead).byval/sretas the native spelling of D66’s const-pointer-in/results-out aggregate ABI at FFI boundaries.
Adopt with discipline
freezeat untrusted boundaries: values read fromRawPtr, foreign buffers, andBytesdata freeze before branching or comparison. Poison/undef cannot leak from foreign input into otherwise-safe code; this is a safety property.!llvm.loop:mustprogresswhere progress is proven (#[recursion "bounded"]or totality); unroll and vectorize hints only under P10 rewrite contracts (wrapping reassociates freely, checked does not, FP needs its own contract).immargforprimdeclaration parameters that must be immediates (shift amounts, SIMD lane indices);llvm.sideeffectonasmfragments so DCE cannot drop them (P18).
Not adopting
- Fast-math flags as defaults (IEEE default-rounding contract); only under an explicit rewrite-level relaxation.
returns_twice/setjmp-family anything (JPL rule 1; no such control flow exists).- Coroutine intrinsics (thunks and the cooperative task backend are our own state machines).
convergentunless the SIMD barrier story demands it.- CFI/sanitizer metadata (later; orthogonal to the language contract).
Where it lands
The translations attach to the P20 implementation (assertions to
llvm.assume) and the P18 prim work (immarg, sideeffect); the
freeze/noreturn/!range/ABI-attribute pass is its own hardening
slice (tracked as the LLVM contract surface phase). Evidence style:
IR-observation tests (the attribute appears on the emitted unit where
the analysis proves the fact; its absence where it does not), never
wiring tests.
