Loop guards and container access

A list_get in Prismio is not one machine instruction. It is a representation test, a bounds test, and two loads from the list header, and a loop pays all of them on every iteration. Loop guards move that work out of the loop: one predicate in the preheader proves what every access in the body needs, LLVM versions the loop on it, and the fast version accesses memory directly.

This page describes the mechanism, the analysis that decides which loops qualify, the soundness argument for each thing it removes, and the measurements. It is an implementation deep dive for compiler and runtime contributors; nothing here is observable from the source language except speed.

What application developers need to know

• Container access has the same meaning whether or not a loop is guarded. list_get past the end still returns the element type's zero, and list_set past the end is still a no-op.
• You do not opt in. A while loop over a Vec<Int> is guarded when the compiler can prove it, and takes the ordinary path when it cannot.
• Two source patterns decide whether the loop can also vectorize: write the update as an unconditional store, and prefer std.math's max/min over a hand-written branch. A conditional store cannot be widened by any compiler.
• A call inside a hot loop is no longer automatically a performance cliff, but a call that can grow a list still is. See What may appear in a guarded loop.

The cost being removed

RtList is a 40-byte header holding, among other fields, a data pointer, a length, and an elem_size stamp that records whether elements are stored inline or as pointers. A scalar read compiles to list_get_inline_scalar, whose body is:

unsigned long long list_get_inline_scalar(void* lp, int index, int elem_size) {
    RtList* l = (RtList*)lp;
    if ((unsigned)index >= (unsigned)l->len) return 0;   // bounds
    if (l->elem_size != elem_size) {                     // representation
        return (unsigned long long)(uintptr_t)l->data[index];
    }
    ...
}

Both tests are load-bearing. The representation test exists because list_get_inline returns two different kinds of thing — a slot's address for an inline list, a slot's contents for a boxed one — and only a scalar element can tell those apart. The bounds test exists because an index out of range stops the program (list_index_fail), and the inline paths emit that test themselves (list_bounds_or_fail): a cold call that never returns, so the in-range path is a guard with no join. Until 2026-10-16 list_get was total, answering zero, and the inline paths implemented that a second time.

Inlined into a DP loop, one iteration of a 1-D knapsack emitted three representation tests, two bounds tests, and six or seven reloads of the header. The equivalent C++ inner loop is two loads, a compare, a csel, and a store.

The bounds check is why the header reloads

This is the non-obvious part, and it is what makes the guard worth building rather than hand-optimising the runtime.

l->data is loaded only on the in-range path. A conditional load is one LICM will not hoist, because it cannot prove the address dereferenceable on the path that skips it. So the bounds check is not a cost sitting beside the header reload — it is the cause of it. Remove the condition and LLVM hoists the pointer into a register by itself.

Measured on a model of the same loop over the real RtList layout:

The third row is the one worth pausing on. Hoisting the base pointer yourself — the obvious fix, and the one an earlier design note recommended — is worth nothing. Removing the check gets the hoist for free, and adding the hoist on top of that changes nothing again.

The guard

One i1 per loop, computed in the preheader, is the conjunction of everything the body needs. It carries two kinds of fact.

Representation

For every guarded access, elem_size == stride, where stride is the static inline width of the element type. One conjunction rather than one test per site: LLVM will not clone a loop for 2^n independent invariant conditions, and a fused loop over five lists measured worse with per-site tests than with none.

Range

For every guarded access, 0 <= lowest index and highest index < len, evaluated in i64 so the arithmetic cannot wrap a 32-bit Int.

The range is recovered from the loop itself. For a while (V op B) loop whose body updates V exactly once, as its last statement, and every one of whose guarded accesses indexes V, V + E or V - E for a loop-invariant E, the values V takes in the body are exactly [B, V_init] going down or [V_init, B] going up — and V_init needs no symbolic reasoning, because the preheader still holds it.

Why the restriction is not cosmetic: the update must be the body's last statement, and an earlier version of this analysis shows why the restriction is not cosmetic. Widening the range by one step to allow the update anywhere makes the lower bound of at - weight equal weight - 1 - weight, which is -1, so the conjunct >= 0 is false at run time always. The guard never fired, the loop still paid to be versioned, and the result was 1.29x slower — with correct output, correct-looking IR, and a passing test suite. Only the benchmark distinguished a guard that fires from one that cannot.

Loop versioning, and why totality survives

The guard is a loop-invariant i1, so LLVM versions the loop on it: two copies, one entered when it holds and one when it does not.

The false version is byte-for-byte what the compiler emitted before guards existed. That is the whole soundness story for the language's semantics. Nothing in this mechanism can make an out-of-range access do something new; it can only decide which of two loops runs, and a loop whose indices are not provably in range runs the one that checks them.

This is HotSpot's loop predication with a better failure mode. HotSpot must deoptimise when a hoisted check fails; Prismio keeps both loops and picks one.

What may appear in a guarded loop

A call in the body can invalidate the guard, so the compiler needs an answer for each one. The question is narrower than "does this touch a list", and the difference is most of the language.

The guard proves the element representation and the index range. A read cannot change either. Nor can a write — list_set and its inline siblings store into a slot that already exists. Only moving the element block can: growth reallocates it, and release frees it. The element width itself cannot change at all — a list receives it in its constructor and keeps it for life.

So the compiler classifies every function in the module by whether it can reach one of those primitives:

irPrimitiveMovesBlock   list_push and family, list_inline_grow,
                        list_release,
                        rc_release, cyc_release
irPrimitiveIsSettled    list_get, list_set, list_len, rc_retain, ...

A module pass then runs a greatest fixed point over the call graph. Every function with a body starts assumed settled; each sweep takes that away from any function reaching a block-moving primitive, an unknown extern fn, a spawn or join, or a trait-object call (DYN_CALL), which runs whichever impl the vtable holds. The loop analyses refuse those three node kinds directly too (irIsUnjudgedCall): until they did, a dyn method that pushed to the list a loop was reading left the guarded copy reading a freed element block. Sweeps repeat until nothing changes, which terminates because a verdict only ever moves one way and the module is finite.

Starting optimistic is what admits recursion: a function that calls only itself moves no block, and a pessimistic start would wait on itself forever.

Each function is judged under its own symbol, and a call reads the verdict of the function sema resolved it to (CALL_EXPR.s2, the name codegen calls). The table also keeps a verdict per source name, safe only when every function carrying the name is, and a call falls back to it when it has no resolved symbol. Keying by name alone made one unsafe overload poison every call spelled the same way: Buffer.eq calls an extern, so in any program importing std.mem every Map probe -- whose eq is an Int comparison -- lost its guard, and one closure that pushes took the guard from every closure call.

Only functions the program can reach are judged at all: the standard-library functions it cannot call are dropped after type checking (src/driver/prune.psm), so a dead overload can no longer decide how a live call compiles.

Why not inlining

The obvious explanation for a call being expensive is that it was not inlined, and it is wrong here. A two-line maxInt(a, b) helper called from a DP loop measured 1.79x slower than the branch it replaced — and the disassembly contains no call to it. LLVM inlined it.

It was slower because the guard analysis runs in Prismio's codegen, before LLVM sees the module at all. The loop lost its guards at that point, and inlining afterwards could not give them back. Inlining was never the missing piece; looking through the call was.

Emission

Inside the true version, an access skips what the guard already proved:

The read is ir_list_flat_scalar_elem with check_bounds cleared; the write is ir_list_flat_scalar_set. Both branch on the guard and fall back to the ordinary runtime entry point on the false arm.

Implementation note: Every access this backend emits carries a TBAA leaf, and the store above was briefly written without one. An untagged store may alias anything — including the data pointer loaded from the header two instructions earlier — so LICM could not hoist that load, the base was re-read every iteration, and cross-iteration dependence analysis was impossible. The loop stayed scalar with nothing in the assembly to say why. One tag_scalar call fixed it, and it is what lets a guarded loop vectorize at all.

Vectorization, and the one thing source code controls

With the guard in place the inner loop is straight-line memory access, which is the precondition for LLVM to widen it. Whether it actually does is decided by one property of the source: is the store unconditional?

// Conditional store. Correct, and cannot be vectorized — by any compiler.
if (candidate > list_get(best, at)) { list_set(best, at, candidate) }

// Unconditional store of a select. Widens to four elements per iteration.
list_set(best, at, max(list_get(best, at), candidate))

This is not a Prismio limitation. Modelled on a raw C array, the same loop is 220,000ns with if and 188,000ns with max, 7 NEON operations against 22. LLVM declines to speculate a store it cannot prove safe to execute unconditionally, and so does every other production compiler.

std.math's max, min and abs exist for this reason. They lower to llvm.smax.i32, llvm.smin.i32 and llvm.abs.i32, which LLVM lists as trivially vectorizable — a branch written by hand is not. std.math's Float functions are marked guard-safe the same way: every __builtin_f64_* name is in the table before the sweep, so a loop calling x.sqrt() or a.max(b) keeps its guard.

Index arithmetic in 64 bits, where it is proved

Int is 32 bits and wraps, and an index is sign-extended to 64 bits before it becomes an address. A plain sub i32 there hides the index's shape from LLVM. In knapsack's best[at] = max(best[at], best[at - weight] + value) the vectoriser cannot express the distance between best[at] and best[at - weight], so it guards its vector loop with a run-time test that the two ranges do not overlap. They always do, so the vector loop never runs. C++ has the same problem with an int index, and the same loop with an int64_t index is 4.8x faster.

The proved copy already knows more than LLVM does: the range guard holds 0 <= at - weight < len. So rangeMarkIndex (src/ir/ranges.psm) marks the index's + and - with the loop's proof, and the proved copy emits them nsw. With that, LLVM computes the index in 64 bits, sees a distance of weight, and drops both the wrap check and the overlap check.

nsw is a promise, and a broken one is poison, so the rule is strict:

• An op is marked only when its result and both operands are inside Int. The guard's i64 interval is the loop's value only modulo 2^32, and (i + k) - k is in range while i + k wraps. A value inside Int does equal its interval's value, though. So operands inside Int are what the loop computed, and their exact sum is the result.
• What is known inside Int comes from facts the guard already holds: the index itself, which is in [0, len), and the operand of / or %, which the guard keeps inside Int. A literal offset carries the bound down: c - 1 in [0, len) puts c in [1, len], which is why every op of edit_distance's current + c - 1 is marked. c - 2 is not, because c could then be INT_MAX + 1.
• No fact is ever added to earn a mark. A fact that failed at run time would send the loop to its checked copy, so a mark could cost more than it saves.
• Multiplies are never marked, and neither is anything outside a proved index, so trip counts keep their wrapping arithmetic. §9 of the Int width decision (see Performance decisions and rejected experiments) measured what marking a trip-count multiply costs: dead_code_elimination lost a closed-form fold.

The difference-bound tier already did this for the indices it proves: each term it interprets folds its own no-wrap facts and is marked by relCommit.

Loops over sized arrays

A fixed Array<T, N> index is checked against N (generateArrayIndexCheck in src/ir/expr.psm, lowered by ir_array_index_check to a compare and a branch to the cold, noreturn array_index_fail; a constant index out of range is refused in sema). An access the proved copy covers skips the check. Its loops are versioned when the guard holds something LLVM cannot work out for itself. A loop with no list guard runs the same analysis over its sized-array accesses (arrays in src/ir/ranges.psm), with the type's N as the length. The guard then holds the facts that keep every access in [0, N) over the counters' whole range, and the proved copy marks the arithmetic those facts make safe.

The freestanding knapsack is the case it exists for:

let mut c = 1500
while (c >= w) {
    best[c] = max(best[c], best[c - w] + v)
    c = c - 1
}

c runs over [w, 1500], so best[c - w] in [0, 1501) puts w >= 0 in the guard. From that one fact LLVM proves the loop cannot wrap and adds the nsw itself. It also sees that every read trails the store, and interleaves four iterations at a time: with NEON off, as the suite builds, that is ldp/stp pairs rather than a vector loop. Instructions executed, aarch64 freestanding:

C's undefined overflow never supplied this fact: C reaches 3.14M only when the fact is written into its source, with or without -fwrapv. The guard the obvious argument suggests is w != Int.MIN, which only keeps c - 1 from wrapping. It measured 6,259,472, worse than no guard: c widened to 64 bits, with c - w still computed in 32, costs a truncation and an extension per access.

Two rules keep the duplicated code small:

• Innermost loops only. Versioning an outer loop copies every loop inside it, for facts about the outer loop's own accesses. Knapsack's item loop got a second copy of the capacity loop and nothing for it.
• Only when the proof marks arithmetic. for i in 0..<n { a[i] } would gain a second copy for the fact n <= N alone, and LLVM already makes that one fact out of the check: one compare of n against N before the loop, which still vectorises (measured 2026-10-16).

A [T] parameter has no length the preheader can read, so it is left to the facts below.

Facts an unchecked access implies

An element of a [T] view is addressed without a check, and the language requires every index to be in range (Bounds and storage in the specification's undefined behaviour page); an element of a fixed array is checked, which stops the program on any other index. Either way an access that ran says its index was in [0, len). Every length fits Int, so the index was at most Int.MAX - 1. The fact holds until the name is assigned or bound again: a scalar cannot be passed inout and closures capture by value, so only an assignment in the same function changes a local Int.

The subscripts that give a fact are a name, name + k and name - k, for a literal k. A name + k that wrapped is negative, so an access that ran rules the wrap out. A name - k that wrapped is in [Int.MAX - k + 1, Int.MAX], so its fact is taken only when the last index plus k stays at or below Int.MAX. That holds for any fixed array of a practical length. A view's indices reach Int.MAX - 1, so a view's a[i - 2] could have run with i at Int.MIN + 1, and it gives no fact on i. viewBelow in test_270_array_nowrap.psm checks that.

src/ir/nowrap.psm walks each function that has a loop or subscripts a fixed array, before its body is generated. It marks two kinds of +/- nsw, in every copy of every loop, and proves indices in range (below):

• Bounded. The facts bound every operand, and the exact result is inside Int. Nothing is assumed. Quicksort's scan while (a[i] < p) { i = i + 1 } adds 1 to an i the access left at most Int.MAX - 1. That scan has no bound a guard could use, because it stops on the data.
• A subscript with a non-negative left operand. In best[c - w] after best[c], c - w with c >= 0 can only wrap upwards, to a negative value. A wrapped result is therefore out of range, and the access that is its only use is undefined anyway. Only the subscript is marked this way, never its operands.

Facts flow forward in evaluation order:

• Code that may not run keeps its facts. Facts from the right side of and, or and ?? stay inside it.
• Comparisons narrow. a < b (and <=, >, >=, ==) narrows the locals it names on the taken branch, a below b's largest value and b above a's smallest, and its negation narrows them on the else branch and after a loop that has no break. != trims an interval whose edge it names. An operand with no fact is anything its type holds.
• Branches meet. An if joins the facts of its two branches.
• Loop heads keep what is inductive. A loop head keeps the facts on names the loop never assigns, and on names it does assign when one is an invariant (below).
• A Vec gives no facts yet. Its out-of-range read now stops the program, so a read that returned implies its index was in range, as a Slice access does; using that is not done.

An update is marked only when its loop's subscripts are. The same widening that made w != Int.MIN a loss applies here. nsw on c = c - 1 with c - w unmarked measured 6.26M, against 5.69M with neither. So the pass walks twice. The first walk records every counter that some subscript in a loop combines without a mark. The second walk marks, and leaves those counters' updates in those loops plain.

Counted loops

A while whose condition bounds a counter, and whose body ends by stepping it, bounds the counter in the body too. That takes three things:

• A bound. One and conjunct of the condition is i < e, i <= e, i > e or i >= e, where e is a literal or a name the loop does not assign.
• A step. The body's last statement is i = i + c or i = i - c for a literal c, towards the bound.
• Nothing else. No other statement in the loop assigns or binds i.

Every check of the condition that gets past the bounding conjunct has i on the bound's side, and nothing moves i before the last statement. So the step cannot wrap, as long as the bound plus c fits Int, and i stays between where it entered and the bound. The fact holds from the bounding conjunct on. A conjunct ahead of it also runs on the last check, when i is already past the bound:

fn note(inout v: [Int], x: Int) -> Bool {
    v[0] = x
    return true
}

fn last(start: Int) -> Int {
    let mut seen: Array<Int, 1>
    let limit = 999999999 + 999999999 + 147483649
    let mut i = start
    while (note(seen, 1 + i) and i < limit) {
        i = i + 1
    }
    return seen[0]
}

fn main() -> Int {
    if (last(2147483645) == 0 - 2147483647 - 1) { return 0 }
    return 1
}

i is in [start, Int.MAX - 1] in the body, but 1 + i in the first conjunct runs once more with i at Int.MAX, and wraps; it is not marked.

The walk also counts the loop. With a fact on i where the loop starts, it runs at most (bound - start) / c + 1 times, unless the body holds a continue, which skips the step. The count is what bounds the contents of an array, below.

Loop invariants

Binary search keeps lo and hi in [0, 4096], but only as a pair: hi = mid and lo = mid + 1 stay inside it because lo < hi held where mid was computed. No single assignment shows it, so a loop head that forgot every name the loop assigns lost both, and table[mid] kept its check. nowrapInvariants finds such facts by trying them:

• Candidates. Each local of a fact type the loop assigns that had a fact where the loop started.
• A probe. One walk of the condition and body from the head's facts with the guesses added, in a mode that marks nothing and records nothing (NOWRAP_PROBE). Its marks go to a pass of their own, and the walk's loop and block counters are put back afterwards.
• Widening with thresholds (Blanchet et al., PLDI 2003). A guess grows to the hull of itself and what the probe leaves at the end of the body. From the third round a bound that still moves jumps to the next of the name's thresholds, a literal the loop compares it with, one either side of that, or its entry bound, else to its type's edge. From the sixth a guess that still moves is dropped, so it does not hold the others up. When a probe moves nothing, the guesses are inductive.
• Exits. A continue anywhere in the body (a labelled one in a nested loop included) is a way back the walk does not follow, so the loop gets no invariants. A break leaves from inside the body, so the invariants hold in the body but are not the facts after the loop.

A function spends at most 400 probes (NOWRAP_PROBE_BUDGET); past that a loop keeps what it kept before. Compiling the compiler took the same time within noise.

Narrow integers and proved indices

The facts are I64 intervals over every integer type of at most 32 bits: Int, U32, U16, U8, I16, I8. Each operation is checked against its own type's range and succeeds only if its exact result fits, so a fact is never a wrapped value: +, -, *, >> and & by a literal, an unsigned % by a literal or by a divisor bounded above zero, and as between integers when the value fits the target (truncation, extension and reinterpretation agree there). for i in a..<b bounds i between its ends in either direction. Only a signed Int +/- is marked nsw.

An access to a fixed array whose subscript's interval lies inside [0, N) is marked on the INDEX_EXPR (nowrapMarkInRange), and generateArrayIndexCheck emits no check for it (nowrapIndexInRange). That is what keeps binary_search, pointer_chase and bytecode_interpreter free of checks in their hot loops:

test_311_proved_indices.psm holds the proved shapes and twelve that look provable and are not (an off-by-one <=, a U32 below zero, an exit the end of the body does not see, a large U32 cast, a mask one too wide, a store nothing bounds, a let bound twice), each of which must still stop at its index; proved_indices in test_runner.py reads the IR for which keep a check.

What a local array holds

Edit distance keeps two rows of costs, and each new cost is one more than a neighbour or equal to one:

cur[j] = __builtin_min(__builtin_min(prev[j] + 1, cur[j - 1] + 1), prev[j - 1] + cost)

C's compiler turns min(a + 1, b + 1) into min(a, b) + 1, one add fewer per cell, because C's overflow is undefined. For Prismio it may only if neither add can wrap, which depends on what the rows hold, not on any index. src/ir/contents.psm keeps a bound on the elements of a local array of any fact type:

• Which arrays. Nothing but a subscript names the array, in its function and outside any closure, and its name is bound once there. A view, an inout argument, a copy or a for x in could write it where the walk does not look.
• One lifetime. The bound holds from the declaration, which zero-fills or initialises the array each time it runs, to the end of its block. Arrays declared in one block are a family and share the bound, because a store into one reads the others.
• A form per store. A stored value is a concrete interval from literals and facts, or relative to the family's bound [L, M] through the elements it reads: prev[j] + 1 is at most M + 1. Sums, min and max combine forms; a program's own min or max counts when its body is one comparison of its two parameters and a return of each (nowrapSelection), since a freestanding program cannot import std.math. A value read through an immutable let bound once in the function (let t = order[i]; ... order[j] = t) is a read of that array. Anything else, or a sum of two elements, leaves the family without a bound.
• Types. The bound must lie inside each member's element type. A member too narrow for it, a U8 row beside an Int one, fails alone, and the rest settle again without it.
• Growth. L holds if no store can go below it. M grows by at most the relative part of each store, so over one lifetime it stays at or below the largest initial or concrete value, plus that part times the store's executions. The counted loops between the declaration and the store bound the executions.

The benchmark's rows start at zero and receive 600 x 600 stores of at most M + 1 per lifetime, so the elements stay in [0, 360600] and all three adds are marked. An array that fails, because a store's value has no form, takes with it only the arrays whose stores read it.

Wrapping integers and tight loops has the investigation: the shapes behind the gap, every alternative measured and the prior art.

Remainders by a literal

A checksum loop ends every iteration with a remainder that depends on the last one:

for i in 0..<n {
    let value = i % 997
    checksum = (checksum + value) % 1000000007
}

LLVM emits each % as a multiply by a magic constant — smull; asr; add; msub, about eleven cycles — and the chain through checksum serialises them. It cannot do better, because it does not track the range of a value carried around a loop. The access-facts walk can, and src/ir/residues.psm adds what it needs:

• A remainder's range. x % m for a literal m >= 1 lies in [-(m - 1), m - 1] with the dividend's sign, whatever x was, and no wider than a bounded dividend allows.
• What a loop keeps. A name every assignment in a loop sets to a remainder by a literal, which entered the loop inside that range, is inside it at every head: no assignment can leave it, so no induction over the body is needed. Other names assigned in the loop are still forgotten.
• One step. On a dividend in (-2m, 2m) the signed remainder is x - m from m up, x + m from -m down, and x in between. The walk records which of four forms the dividend's interval allows — the dividend itself in (-m, m), the subtract in (-m, 2m), the add in (-2m, m), both in (-2m, 2m) — and generateBinary emits compares and selects instead of srem. Neither the add nor the subtract is nsw; the arm a select discards may wrap.

A range runs either way at run time (0..<n counts down when n is negative), so value above is only known to lie in (-997, 997), and checksum + value needs both steps. That is still the loop in 4.06 ms rather than 9.67 (vector_growth, 4M iterations); a dividend known non-negative takes one step, 3.04 ms in the C model of the same loop. A divisor up to Int.MAX is read, but a dividend whose range does not fit Int keeps its remainder, so % 2147483647 on a sum stays srem.

PRISMIO_NOWRAP=0 turns the forms off with the nsw marks: they come from the same facts.

Square bounds and stride tiling

A sieve's outer loop is bounded by a square, while (p * p <= n). The range guard folds the facts that keep the square exact, so the conjunct bounds p: that proves prime[p] and makes p = p + 1 nsw, which is what lets LLVM count and interleave the inner loop. A nest that stores one value at a stride is also run one cache-sized window at a time, as a hand-written segmented sieve is. Both, with why reordering the stores is legal and what was measured, are on Stride tiling and square bounds.

Measurements

knapsack, a 1-D DP over Vec<Int> with 576,000 inner iterations, against C++ -O3 and Rust opt-level=3 on the same machine, 31 alternating samples, checksums equal:

The last row is the vector loop running at all, not Prismio outpacing clang's code: the C++ arm indexes with int and never enters its vector loop, and the same C++ with an int64_t index gets the same factor.

Rust is scalar on this workload and pays bounds checks Prismio no longer does, which is why Prismio is roughly three times faster there while still level with C++.

The mechanism is not specific to one benchmark. Across the 34-program suite it changed 13 of 53 functions, and tokenization — a string workload with no DP loop at all — is 0.56x of C++.

Measurement warning: This suite is layout-sensitive well past its recorded noise floor. gcd_lcm read 0.868x reproducibly across 31 alternating samples on byte-identical code; the symbol had merely moved 132 bytes, changing its 64-byte alignment. Before believing any number here, diff the per-symbol mnemonic sequences of the two binaries and measure only the functions that actually changed.

What is declined

The analysis is deliberately narrow, and each of these is a separate widening with its own soundness argument:

• loop forms. while and range for loops carry the guard.
• An induction variable updated anywhere but the body's last statement, more than once, or by a non-literal step.
• An index that is not V, V + E or V - E for a loop-invariant E.
• A receiver reached through a field (w.items). A stale length is an out-of-bounds store, and an assignment through a field is not what the module pass inspects.
• Any loop calling a function that can reach a block-moving primitive, an unknown extern fn, or a spawn.
• Struct elements in the write path, whose setter can run a user releaser.
• A sized array in a loop that also has a list guard. The guard serves the lists, and a fact about an array that failed at run time would cost the lists their unchecked copy.
• Access facts from a Vec and from a Slice, whose checks both trap and so would supply them. Neither is done yet.
• Heapsort's while (root * 2 + 1 <= end). root = pick is no counter, and proving the multiply needs root >= 0 carried through the loop plus a guard on start and end. An emulation measured 3.2% on a row already inside the parity band; see docs/KNOWN_ISSUES.md.
• Counted for and loop forms, and a counter stepped anywhere but the body's last statement.
• Array contents through a sum of two elements (t[i] + t[i] doubles, and no form describes it), a cast, a call other than __builtin_min and __builtin_max, or a store that can lower the bound.

Implementation map

Debugging a guard change

Ask whether the guard fired before asking whether it helped. A guard that is emitted and always false looks identical in the test suite to one that works. Count cmp against the stride in the disassembly: once, in the preheader, means it fired; once per access means it did not.

Then check the fast version, not the first loop you find. A versioned loop has two bodies, and the checked one is often the one your eye lands on first.

Write the adversarial test before the optimistic one. A helper that pushes to the list under test must decline the guard; so must one that reaches a pusher through another call. Those two cases are the entire soundness claim of the effect analysis, and they fail loudly — a stale length past a list_push is an out-of-bounds access, not a wrong answer.