M7: reusing access-check evidence

This is M7's first deliverable (PLAN.md): one narrowly specified alternative to repeated runtime checking. A heap access check's proof may cover later scalar accesses through the same pointer, in the same block (round 1) or along CFG edges (round 2), as long as nothing on any path in between can change what the check established. Everything else keeps its adjacent check. The pass is off by default (--checks=reference); --checks=reuse or NANOFIL_CHECKS=reuse selects it, and the reference path stays the differential reference.

The obligation

A raw scalar access raw_load(T, Off) or raw_store(W, Off, V, A) at a proof A requires, at the moment it executes:

Before M7 one proof discharged one access: check(Lo, Hi, Rights, Align) on P, immediately followed by the raw access that reads its result. The reference path still produces exactly that.

Evidence

A proof tmp(Q) defined by let(tmp(Q), a, check(Lo, Hi, R, Al), [P]) in block B establishes those facts for P's value (address and capability) and the object's state when the check ran, for every access the check covers (ir:covered_access/6). The facts stay true until one of these happens:

The instructions that preserve evidence are a closed list (ir:evidence_preserving/1): pure lets (integer and float arithmetic, comparisons, extensions, conversions, ptoi, non-symbol copy), flight, loc, heap checks, check_local with its access, scalar raw_load and raw_store, and raw pointer loads with one of the closed heap or local load effect lists. None calls a helper or reaches a safepoint. A scalar store cannot change any object's bounds, rights or lifetime: upper and flags sit in the header below the lower, outside every capability's range. A pointer load reads aux and box words only (pointer_load_effect//4). Atomics, fences and volatile accesses, if they are ever added, must stay off the list.

Merge: see Across edges (in round 1 the facts at block entry were none). Transfer: a heap check adds its proof once its first access has run; a preserving instruction keeps every fact except those naming the temporary it defines; anything else empties the set. No fact exists without a check that ran at the original access's place.

Checked IR contract

No new term. ir:checked_insts/5's acceptance rule changed:

1. Every check is still immediately followed by a first use it covers. Checks are never moved or widened beyond their first access, which is what keeps trap timing.
2. A heap check's proof may also be read by later scalar raw accesses that it covers, where the validator's own dataflow (below) shows the evidence live: on every path from the check, only preserving instructions and plain edges, and neither Q nor P redefined.
3. Proofs still never reach phis, parameters, call arguments, results or memory. Local and function proofs keep immediate single use; a pointer access never reads a reused proof.

Interpreter contract

Unchanged. A raw access evaluates its proof's captured value and checks the access against the capability's current region state; a violation is unchecked(Why), not a trap. Stale evidence after a modeled free and too narrow or read-only evidence therefore show up as unchecked, which refines nothing. Evidence about the wrong object is safe, so it shows up only as a changed outcome. Effects the interpreter abstracts (polls, allocation exits, ensure-aux, concurrent free) are covered by the validator's invalidator list and by native GC tests.

Emitter contract

fused_blocks/5 keeps fused(Check, Access) for each check and its first use. A later scalar raw access at proof Q becomes reused(Access), Access at the check's operand P: emission loads P's address from its rooted slot and performs the access without a check. Its liveness view reads P, so P stays live, and its slot unshared, until its last reused access. The emitter forgets a proof once Q or P is redefined, including by a fused access or call, because it reloads P where the interpreter reads Q's captured value. Since round 3 a reused access at a nonzero offset reloads P and adds the offset; beyond 32 bits it throws. It does not repeat the validator's invalidator analysis.

The pass

check_reuse:reuse_checks/2 runs after pizlonation. It walks each block forward (entry facts per Across edges) with the facts avail(P, Q, Lo, Hi, Rights, Align) and deletes a heap check whose first use is a scalar raw access when an available proof of the same operand P subsumes the deleted check itself (range, rights, alignment), not just its access, and when the deleted proof has one definition and one reader in the function (round 2; round 1 asked only that nothing later in the block read it); the access then reads that proof. It never widens a check or adds one. Its transfer function (transparent/1) is stated separately from the validator's evidence_preserving/1. Context sites follow the instructions, and alias(Q, tmp(Q1), none, Os) records which proof replaced a deleted one.

check_reuse:reuse_refines/2 is the independent identity check the driver applies after the pass: the output is the input less deleted heap checks, each of whose single access now reads either an earlier proof in its block or a function-wide singly defined proof, of the same operand, whose check subsumes the deleted one; and the deleted proof had one definition and one reader. valid_module/1 then checks the safety rule. A rewiring to another object's proof is safe, so only this check rejects it.

Observation contract

The same outcomes as the reference checked module on every interpreted run, traps and their reasons included, and the same block count. A deleted check would have succeeded: its proof's check succeeded on the same capability and address with at least its range and rights, and nothing between could change the object's bounds, rights or lifetime. Deterministic executions are unchanged. A free by another thread, racing without synchronization with the later access, may lose its trap; Fil-C already tolerates that race between any check and its access (pizlonation.md), the memory cannot be reclaimed while P is rooted, and no trap is added or moved earlier.

Evidence

The reference path's 1032 snapshot outputs are byte-identical to the preceding compiler's. With reuse, the Nix check runs difftest (unchecked vs reused interpretation, and native) on the Fil-C fixtures, tests/c and big1.c with and without -O; the native ABI, GC, setjmp, pointer-effect and exception fixtures and the programs under FUGC_SCRIBBLE=1 FUGC_VERIFY=1; the corpus; and the GC fixtures with --registers=local (since October 2026 --registers=temps, local having been retired). Hello, zlib, bzip2, lz4 and Lua are built with --checks=reuse with and without -O, and SQLite with -O --checks=reuse, and must match filcc.

tests/filc/reuse.ir has one function per mistake: a call (free) between two reads, a 4-byte proof before an 8-byte read, a read proof before a readonly store, two objects, and evidence across a dominating edge. tests/filc/reuse-gc.ir reuses p after a collection-forcing call and after many new temporaries, while a new pointer o would take p's slot if the reused read did not keep p live. Unit tests (reuse_validation, reuse_semantics, reuse_pass, reuse_emission) reject each invalidator, too little range, read-for-write, pointer reuse and (round 1 only) cross-block evidence, and show stale evidence as unchecked(out_of_bounds) and a wrong-object rewiring as 11 instead of 12.

Planted mistakes, each run against the unit tests, difftest reuse.ir and run-c reuse-gc under GC stress with reuse on:

Static yield over the c-testsuite, tests/c and tests/c/prog (252 files): 4451 to 3780 heap checks emitted without -O (15.1% fewer), 1214 to 1152 with -O (5.1%). Promotion leaves fewer repeated accesses through one temporary, and a read proof never covers a later write, so p->x++ keeps both checks. These are counts of emitted checks, not measured speed.

Review

Oracle reviewed the design before implementation and found it safe. It required three changes, all made: subsumption against the deleted check rather than its access (a hand-written wider or write check would otherwise lose its trap), forgetting a fact whose proof name is redefined, and the emitter's own redefinition guard. It recommended keeping reuse_refines/2 as the wrong-object check, which interpreter tests alone rarely discriminate.

Oracle then reviewed the implementation and found no blockers. It found two gaps, both fixed with tests: reuse_refines/2 accepted a rewiring when the deleted proof's name was read again later (reachable only from hand-written checked IR, since pizlonation names proofs freshly), and the emitter's guard ignored definitions made by a fused first access. On its advice the pointer-load entry is tied to the closed load effect lists.

For round 2, Oracle reviewed the design (four spec findings, folded into the section below) and then the result. The result review found no unsound case and two gaps, both fixed: the emitter's proof index counted definitions once per check, quadratic on the default path too (a 3000-statement function spent 54 s in it; it now sorts the names once), and no test exercised the emitter's guard that Q has one definition (now in reuse_edges, and it fails with the guard removed).

Across edges (round 2)

Round 2 lets evidence flow forward along CFG edges. The facts, the intra-block transfer and the invalidators are unchanged. Only how a block's entry facts are formed changes. Oracle reviewed this design before implementation and found it sound; its four spec findings are folded in below (marked review).

Facts and lattice

The facts are the same as within a block: live(Q, P, Lo, Hi, Rights, Align) (validator) and avail(P, Q, Lo, Hi, Rights, Align) (pass). A fact is a ground term, and two facts are equal only when they are identical. The set of facts is ordered by inclusion; smaller sets are more conservative.

Edges

A poll may run deferred signal handlers, which may call free, and it is a collector handshake. Spatial facts could in principle survive a poll with a renewed temporal check, as FilPizlonator does, but nanofil's facts are not split into spatial and temporal parts. So a poll kills every fact. Pizlonation polls every edge to a block at or before its source, so every back edge carries nothing and no fact is ever carried around a loop.

Merge and order

Blocks are processed once, in the order of the function's block list. A block's entry facts are the intersection over every incoming edge, from every predecessor including unreachable ones, of the facts that edge carries. Edges are not deduplicated per predecessor: branch(V, poll(L), L) contributes a polled and a plain edge, and the polled one empties the intersection (review). A block with no incoming edge starts with none; the intersection of no sets is empty, not everything (review). The phis' destinations then kill the facts that name them, matching P through its tmp/1 wrapper (review). No iteration is needed: an edge from a block not yet processed carries nothing, which can only lose facts. By induction on the order, every computed fact holds on every path. In pizlonated IR every not-yet-processed predecessor reaches the block through a polled edge, so this single pass loses nothing.

Acceptance

The validator (ir:stage_func/4, checked_block/5) computes its own entry sets this way from its own evidence_preserving/1, independently of the pass. A scalar raw access in any block may read a live proof that covers it. Its facts need no uniqueness: redefinitions are killed on each path.

The pass computes avail with its own transparent/1 and its own edge rule. Facts cross an edge only when Q has exactly one definition and P at most one, counting parameters, phis and every instruction form (ir:temp_defs/3), the same condition the emitter needs (review). It deletes a check only when its proof has one definition and one reader in the whole function; this replaces round 1's block-local rule.

reuse_refines/2 becomes function-wide: a rewired access must read a uniquely defined heap check of the same operand that subsumes the deleted check, and the deleted proof must have had no other reader. Its availability on every path remains the validator's question.

Emission

A reused access in another block reloads P. To be correct it needs P to hold the value that was checked, so the emitter accepts a cross-block reuse only when Q and P each have at most one definition in the function (a parameter counts as one). With strict SSA, a reachable use of Q is dominated by Q's check, and P's single definition dominates that check, so the reload yields the checked value. Liveness reads P at the reused access, so P stays live, rooted and unshared across the edges.

The emitter's own guard (single_proofs/3) counts definitions the same way; a cross-block reuse that fails it falls through to the unchecked-access error, never to a reload of a different value.

Tests

reuse_edges (unit) accepts reuse across a plain edge and through a diamond, and rejects, in the validator:

• Branch-only evidence: q proves 8 bytes on one arm and 4 on the other (hand-written, so q dominates the join); the 8-byte read after the join is rejected. A check only on one arm does not even dominate.
• Free on one path, with the freeing block before and after the join in block order.
• Loop-carried staleness: a preheader check, a back edge after a free.
• A forward poll edge, branch(V, poll(L), L), and a phi redefining P.

The pass keeps the join's check after a free on one path and in a loop, deletes it in a diamond, and all three modules (unchecked, checked, reused) give the same outcomes; it carries nothing over a poll edge and rewires nothing across an edge when P has two definitions. The emitter refuses that case; refines rejects a deleted proof read in another block. tests/filc/reuse.ir adds diamond and loop_free (difftest, native); reuse-gc.ir's survive2 reuses p two blocks after its check while a new pointer would take p's slot, under forced GC.

Planted cross-edge mistakes (unit, difftest reuse.ir and run-c reuse-gc with reuse on):

A pass whose phis keep facts is not separately observable: a phi that redefines P gives P a second definition, so the single-definition filter already drops the fact. The phi kill stays as the stated rule.

Static yield, the same 256 files (c-testsuite, tests/c, tests/c/prog), emitted heap checks:

These are counts, not timings. Round 1's earlier figures (15.1%, 5.1%) were on 252 files before the corpus grew.

Runtime effect (October 2026)

Measured at bf0e86d on swa (Ryzen 9 7950X3D, not a VM). Each program was built by nanofil in four modes through nanofil-cc, as the Nix checks build them, plus a filcc -O2 reference. Every nanofil binary's output was first checked byte for byte against the reference on 4 MB of text and of random data, including bzip2 and lz4 with reuse, which their Nix checks did not then build. Then 7 trials after one warm-up, modes shuffled within each trial, pinned to one core, perf stat user instructions and task-clock; medians.

With -O, reuse changes executed instructions by at most 0.2%, yet times still move by up to 3.9% with separated trial ranges (zlib -d): that is code layout, and it sets the noise floor. Only the three bold rows, each with a 7–10% instruction drop, are clearly above it. So reuse helps unoptimized code by up to about 6% and does nothing measurable after -O, where nearly every access has its own flight pointer and no earlier proof of the same SSA pointer.

For scale, filcc's -O2 was 5–28× faster than nanofil without -O, and 2–7× faster than nanofil -O (e.g. bzip2 -9: 0.29 s, 3.01 s, 1.08 s). The gap is general code quality, not checks.

Related pointers (round 3)

Implemented (perf.md item 6c-1) from the reviewed contract below; Implementation records what differs. With -O each field access has its own flight from the struct pointer, so the same-SSA-pointer rule finds almost nothing (the runtime-effect table above: 0.0% of instructions). Round 3 relates a check's pointer to an earlier proof's pointer when both are constant offsets from one root, and changes nothing else: the evidence facts, invalidators, edges, merge and the validator's acceptance rule stay as in rounds 1 and 2.

Relation

base(X) = R + K when tmp(X) has exactly one definition in the function and it is flight(tmp(X), add, [address(B), const(K0)], lower(B)), sub with -K0, or copy with [address(B)] and K0 = 0, with the same B as address and lower donor, and B a temporary with one definition; then base(X) = base(B) + K0. Any other pointer P has base(P) = P + 0. P and P1 are related with distance D when base(P) = R + K, base(P1) = R + K1, R is the same singly defined temporary (or P == P1, D = 0), and D = K − K1. Then P and P1 have R's capability (exactly, by lower(B) at every step), and P's address is P1's plus D in unsigned 64-bit arithmetic, which is how flight computes addresses. The walk from P to R carries a visited set and stops at a cycle (review: an unreachable block may hold a self-referential flight, which the validator accepts and on which the prototype did not terminate).

Why it holds at the deleted check S (review; a single static definition can run many times, so "single definition" alone is not the argument): the input is validated before the pass, so every reachable use is dominated by its single definition. If R's definition ran again after P's chain was last computed and before S, some path from entry to S would avoid P's definition, contradicting its dominance of S; the same holds for each intermediate flight. On P1's side, Q1's fact reaches S only along plain forward edges, and a rerun of R between Q1's check and S would sit in a block whose entry evidence contains Q1, which by the validator's round-2 induction is impossible since R's block dominates Q1's. So at S both carry R's current capability and their addresses differ by D, at reachable points only.

The pass

A heap check check(Lo, Hi, Rights, Align) of P whose first use is a scalar access at offset Off may be deleted when an available fact avail(P1, Q1, Lo1, Hi1, Rights1, Align1) has P1 related to P with distance D and subsumes check(Lo + D, Hi + D, Rights, Align), and the deleted proof has one definition and one reader (round 2). The access is rewritten to read Q1 at offset Off + D. Subsumption is against the deleted check shifted by D, not against its access, as before.

Acceptance

Unchanged. The rewritten access reads Q1 at Off + D, which the validator accepts only if Q1's live check covers [Off + D, Off + D + Size) with its rights and alignment (covered_access/6). So the validator alone establishes that the access stays inside Q1's checked range, whatever the pass did. reuse_refines/2 gains the relation: the rewired access must read a proof whose pointer is related to the deleted check's pointer with exactly the distance by which the offset changed, and that proof's check must subsume the shifted deleted check. That is the identity side (same object, same address), which the validator does not see; the shifted subsumption is also what keeps the trap of a hand-written check wider than its access. The relation code is shared by the pass and reuse_refines/2 (review), so a bug in it defeats both; unit tests therefore hand reuse_refines/2 modules rewired by a wrong distance and a wrong root, and the planted relation bugs must be caught by difftest values. The provenance record alias(Q, tmp(Q1), none, Os) must not claim Q's address equals Q1's when the distance is not 0.

Interpreter

Unchanged. A raw access at Q1 + (Off + D) evaluates Q1's captured pointer plus the offset against the capability's current state, so a wrong distance shows up as a changed value or unchecked, and stale evidence as unchecked.

Emission

fused_insts/5 stops throwing on a reused access at a nonzero offset when the offset fits a signed 32-bit immediate (else it still throws). reused(Access) loads P1's address from its rooted slot, adds the offset (add $Off, %rax), then emits the access at offset 0. The liveness view reads P1, so P1 stays live and rooted until the last access that reuses it; the emitter's redefinition guard and single-definition rule for P1 (round 2) apply unchanged. P itself may then be dead, which is fine: nothing reads it.

Observation contract

Unchanged from rounds 1 and 2. A deleted check would have succeeded: an earlier check of the same capability already succeeded on a range containing the shifted one, with at least its rights and alignment, and nothing in between could free the object, change its bounds or rights, or reach a safepoint. No check moves, widens or is added, so every trap happens at the same access with the same text. Racing free is the same tolerated race as before.

Tests and plants

• Unit: a field read after another field's check is rewired at the right offset; rejected when the two flights have different lower donors, different roots, a root or flight with two definitions, a distance that takes the access outside the proof's range (validator), a read proof for a store, and across a call or poll.
• tests/filc/reuse.ir: fields at offsets 0, 4 and 8 of one object, holding distinct values (so a dropped add or an ignored K changes the output), a free between, and an out-of-bounds field after an in-bounds one, which must still trap at the second access. A later field's check first keeps the earlier field's check: pizlonated checks have Lo = 0, so a negative distance never deletes in emitted code (review); a hand-written unit case with Lo1 < 0 exercises a real negative-distance reuse in the interpreter.
• Termination: unreachable self-referential and two-cycle flights.
• Shapes: chained flights ((R+4)+4 against R+8), sub and copy flights, a parameter root, a loop-header phi root with fields read on both sides of the back edge, a wrapping constant (2^64−8 against −8, which must only fail to match), and a related field read across a plain edge (rounds 2 and 3 together), natively.
• reuse-gc.ir: a reused related access is the only reader keeping P1 live while a new pointer would take its slot, under forced GC.
• Plants: relation ignores the lower donor; relation ignores K (distance 0 always); pass compares the unshifted check; refines accepts any distance; emitter drops the add. Each must be caught by unit, difftest reuse.ir or run-c reuse-gc.
• Gate: the bench in O-reuse, and the ten Nix checks, which build every program with --checks=reuse too.

Review

Oracle reviewed this contract and the prototype (/tmp, not committed) and found no case in reachable, validated IR where an access runs unchecked, a trap moves or changes text, the wrong address is accessed or rooting breaks. It confirmed the emission (add $Off, %rax after reloading P1, flags dead, no safepoint before the access, liveness reading P1, the checkers knowing add with an immediate). Its findings are folded in above, marked review: the soundness argument, cycle termination, the shared relation code, provenance, negative distance and the extra tests.

Implementation (round 3)

check_reuse.pl: names_info/3 records each single-definition flight from a singly defined base with the same address and lower donor; base_of/4 walks them with a visited set; related/4 gives the distance, used by the pass and by insts_refine/3. The alias record is written only for distance 0: a distance cannot be stated in provenance's alias/4 without changing its grammar, so a nonzero rewiring leaves Q as an eliminated value with no replacement. filc_amd64.pl: a reused access at an offset within 32 bits reloads P1 and adds it. The root definition count in the contract's relation is implied by the flight table, so related/4 does not repeat it.

Pizlonated checks are check(0, Size, …), so in pizlonated IR a rewiring always has distance 0: what round 3 finds there is the same field reached by two flights (a reload of p->c). Nonzero offsets come only from hand-written checked IR, which tests/filc/reuse-offset.ir runs natively.

Tests: unit reuse_related (rewiring and its value, emission with one check, wrong-distance and wrong-root rewirings that only refines rejects, kept checks for another lower donor, another root, a shifted range outside the proof, a read proof before a store and a free, the validator rejecting a rewired access outside the proof, a negative distance, and self-referential and two-cycle flights); tests/filc/reuse.ir fields and fields_free (distinct field values, free, a field past the end, a reload across a plain edge); reuse-gc.ir survive3; reuse-offset.ir. reuse_related fails on the preceding compiler.

Measured yield (prototype)

0–3.4% of instructions under -O --checks=reuse (perf.md item 6c), and static heap checks over c-testsuite, tests/c and tests/c/prog with -O go from 711 (round 2) to 643, against 770 with no reuse. It changes nothing by default unless --checks=reuse becomes the -O default, which is a separate decision.

Spatial evidence and renewal (round 4)

Rounds 1–3 treat a check's evidence as one fact that every safepoint kills, so nothing survives a call, and nothing survives a loop's back edge, which always polls. Checks are 18–39% of -O's instructions (perf.md, "Where we are now"), and bzip2 -9 runs 539M of them against filcc's 230M. This round splits the fact in two. The spatial part (bounds and alignment) lasts as long as the object does. The temporal part (not freed, and for a store not read-only) is renewed at the access by a flag test. That test stands exactly where the full check stood, so no check moves.

Measured first

Method (scratch, not kept): the gate's workloads built with -O (at 2f960d1 plus the emission fix 6bbc117), a symbol at every block label, callgrind's entry count per block, joined to a per-block analysis of the same IR after pizlonation and --checks=reuse. For every check that reuse leaves, it asks which rule would cover it:

• d (this contract): a heap check of the same root (round 3's relation: single-definition, constant-offset flights with the same lower donor), whose bounds and alignment subsume this check's, either earlier in the block or in a block that dominates it. Rights are ignored, since the renewal tests them. Functions with setjmp are excluded.
• p: a loop's steady state with rounds 1–3's kills, but the back edge's poll carrying facts. This needs a peeled first iteration, or a loop copy entered when the poll's slow path runs.
• q: as p, but with spatial facts that only a redefinition kills. This also needs peeling.
• index: what d leaves inside loops when the root is a flight with a variable offset (block[i]).

Executed checks, millions:

bzip2 -9's reference count, 539M, matches perf.md's independent count of the gate binary.

So d covers more than peeling, and without duplicating any code. Variable-index accesses are the largest class that no rule here reaches. They need induction-range reasoning and a non-trapping guard that versions the loop. That is a separate, larger contract, because the guard must not trap earlier than the reference does. A path-intersection rule for spatial facts, round 2's merge with the universe as top, covers less than d. Unreachable predecessors, which the frontend leaves behind (read_buf's L22 in zlib), join with no facts. The same effect costs round 2 some reuse today.

The facts

Lifetime lemma (runtime, at the pin): an object's lower, upper and read-only flag are written only when it is created (filc_runtime.c 2760, 2846, 2895, 8597) and by free_impl (3172–3194), which sets upper = lower and the FREE flag. Nothing else writes upper or read-only. mprotect changes no flags (10156). munmap of a whole mapping frees the object (9955). Whole or partial, it remaps the range anonymous read-write (filc_unmap, 9930–9953), so it faults nothing, in the reference or here. The other flag writes are FREE and WEAK_KEY (3640, filc_runtime_inlines.h 742). A GC cycle never frees a rooted object, and P1 stays rooted in its frame slot. So a span stays true for the same object until it is freed. The FREE flag is set exactly when it is freed, whether by this thread at a call, by a handler at a poll, or by another thread.

The term

One new op, approved separately as a grammar change:

Like a check, it is followed immediately by its first access, which reads the renew's own result tmp(Q) at offset 0, as a pizlonated check's does. This slice allows distance 0 only: the deleted check's pointer P and Q1's pointer P1 have the same address and lower donor (round 3's relation with K = 0), so %rax:%rcx loaded from P1 is exactly P (review: with a nonzero distance the fail call would report P1, not P, and the term has no place for the distance).

Acceptance (validator, independent of the pass)

let(tmp(Q), a, renew(Lo, Hi, Rights, Align), [tmp(Q1)]) is accepted iff all of these hold:

1. Q1 has exactly one definition, a heap check(Lo1, Hi1, _, Al1) of P1. Rights do not matter.
2. P1 has at most one definition, counting parameters, phis and every instruction form (temp_defs/3).
3. The function has no setjmp.
4. Lo1 ≤ Lo < Hi ≤ Hi1, Al1 mod Align = 0 and (Lo − Lo1) mod Align = 0. Size Hi − Lo is positive, as the emitter requires (review).
5. The next instruction is an access it covers (covered_access/6), heap storage effects, as for check.

Strict SSA's existing check (definitions_dominate) already requires Q1's single definition to dominate the renew; within a block, at an earlier index. That is the whole availability rule: no dataflow and no kill list.

renew is on evidence_preserving/1 (a flag load and a branch to a non-returning fail block). After its access it adds live(Q, tmp(P1), Lo, Hi, Rights, Align), so later scalar accesses may reuse Q under rounds 1–3 (review).

Why dominance suffices. Let C be Q1's check and Y the renew, with C dominating Y. Suppose some path from the last execution of C to Y redefined P1. P1's single definition D dominates C, so a path from entry to the first D avoids C. Join it to the segment from that later D to Y, which also avoids C. The result is a path from entry to Y that avoids C, which contradicts dominance. So at Y, P1 and Q1 hold the values that C checked. Loops change nothing: each iteration's re-execution of D is followed by C again before Y. cfg_idoms is an iterative fixpoint, so irreducible CFGs are covered. setjmp's second return adds edges the CFG does not show, so functions with setjmp are left out; inlining refuses setjmp in callee and caller, and an unwind leaves the frame.

Interpreter

renew runs the same access_res/7 as check on Q1's captured value ptr(A, Cap) with its own range, rights and alignment (review):

• a freed region traps out_of_bounds, the reference check's reason, since free empties the bounds;
• a write to ro(_) traps readonly;
• any other failure is unchecked(span): the span the validator relied on was false, a validator or pass mistake, never a program trap;
• otherwise it yields ptr(A, Cap).

So every lost span, bounds or alignment, shows as unchecked where the reference traps or succeeds, and difftest catches it.

Emission

fused(renew(Lo, Hi, Rights, Align), Access):

flight load of P1           ; address into %rax, lower into %rcx, from rooted slots
test $Mask, -2(%rcx)        ; Mask = 4 (FREE), or 6 (FREE|READONLY) for a write
jnz  <the fail label of k(Hi−Lo, Write, Align)>
<Access, as after a check>

-2(%rcx) is the low flags byte of aux, the byte write_check//2 already tests. This is FilPizlonator's own NotFree/CanWrite renewal (FilPizlonator.cpp 4048–4086). The renewal needs no null test, because the capability is non-null and unchanged, and no bounds or alignment test, because those are invariant. On failure it calls filc_optimized_access_check_fail with %rax:%rcx = P and the deleted check's origin. That function derives its message from the object's state: null, then FREE, then bounds, then read-only (4431–4467), so a freed object prints "free object" and a live read-only one "read-only", as the full check would.

Bookkeeping (review): single_proofs/3 maps a renew's Q to P1 as it maps a check's, so a later reuse of Q reloads P1; the emitter refuses a renew whose Q1 or P1 has two definitions; inst_check_kind/2 gets a fused(renew(...), _) clause so its fail label is emitted; live_inst reads P1 at the renew, so P1 stays live and rooted across the calls in between. --registers=temps homes only w and l scalars, so P1's address and lower are in rooted frame slots there.

Pointer consumers may follow a renew: it leaves %rax:%rcx as a check does, and a pointer store is then check-equivalent, ensure-aux, store, as in the reference.

The pass

For each heap check that rounds 1–3 keep, the pass (check_reuse.pl) replaces it with renew when an earlier heap check of a pointer related at distance 0, in the same block or in a dominating block, subsumes its bounds and alignment, Q1 and P1 have a single definition, and the function has no setjmp. Its avail fact after the access is keyed by P1. renew_refines/2 accepts exactly that rewrite: the same position, the same range and rights, and Q1 a single-definition heap check of a pointer related at distance 0. The pass is opt-in, as --checks=renew (NANOFIL_CHECKS=renew), which runs rounds 1–3 first.

Observation contract, and the back-edge poll

Every remaining full check stays where it was, and each renew stands at the index of the check it replaces, with the same origin and pointer. In every object state, the renew traps exactly when that check would, and for the same reason. A free, by a call, by a signal handler run at a poll, or by another thread before the access in happens-before order, makes both trap, with "free object". A read-only object makes both trap on a write. Otherwise both succeed, because the bounds and alignment have not changed. Block counts are unchanged. A free by another thread that races with the renew may lose its trap, as with every check and its access today; free_impl writes upper before it sets FREE, so in that unsynchronized window a renew can pass where a full check would fail (review). That is the same tolerated race.

A back-edge poll kills temporal facts and no spatial ones. The handler it may run can free the object, which the next iteration's renew observes. It cannot move the bounds. So in a loop over a loop-invariant pointer whose check runs before the loop, each iteration's first access of an object is a renew, and later accesses in that iteration reuse its proof under rounds 1–3. Spatial facts first established inside the loop do not reach the header, because the preheader edge does not carry them. Reaching them needs p or q's peeling, which is not part of this slice.

Tests and plants (planned; as built, see Implementation)

• Validator rejects: a renew whose Q1 is defined twice, or whose P1 is defined twice (also through a phi); a renew in a setjmp function; a renew covering more than Q1's range or at a weaker alignment; Size 0; Q1 later in the same block; a renew of a local or function proof; a renew not followed by its access.
• Interpreter: a free between the check and the renew (on another path, after a call, and in a loop) traps out_of_bounds like the reference. A write renew of a read-only object traps readonly. A renew forged without a span, and one at a stricter alignment than Q1's, show unchecked(span).
• Native: reuse.ir cases for free-then-renew in a loop, a read-then-write p->x++ (rights upgrade), Q1 in an irreducible loop, and a renew fused with a pointer store across ensure-aux. reuse-gc keeps P1 live across a forced collection and a call, under FUGC_SCRIBBLE/FUGC_VERIFY. The message text and origin must match the reference on the free and read-only traps, compared as bytes.
• Plants: ignore Q1's definition count; ignore P1's phi definitions; allow setjmp; test FREE only on a write; allow a nonzero distance; liveness does not read P1; accept a range wider than Q1's; renew missing from inst_check_kind; the renew loads the address only; renew not evidence-preserving. Each must be caught by unit, difftest, run-c or the trap-text comparison.
• Gate: snapshot identical with reuse off, the ten Nix checks, and the bench in O-reuse.

Review

Oracle reviewed this contract before implementation. It confirmed the lifetime lemma at the pin (upper, lower and read-only change only at creation and free; frames are marked plainly, FUGC is non-moving and redirects only heap and box slots), trap equivalence, the dominance argument and the setjmp exclusion. Its findings are folded in above (review): distance 0 only, the fact a renew leaves and the emitter's bookkeeping, a full span check in the interpreter, the flight load and Size > 0, the munmap wording and the upper-before-FREE race. Not verified: vfork (no runtime wrapper found), and dlclose or thread-exit paths touching live objects' headers. The measured d column counts nonzero distances too, so the slice's yield is at most d.

Implementation (round 4)

--checks=renew (NANOFIL_CHECKS=renew) runs rounds 1–3, then renew_checks/2, then renew_refines/2 against round 3's output, then valid_module/1. It was opt-in when it landed (the snapshot gate reported every output identical to 7ebcae8) and is now the -O default (below).

• ir.pl: the renew row, kind_arity, its class [a], and evidence_preserving. renew_sources/3 keeps, per function, the heap checks whose proof and pointer have one definition each, and none when the function has a setjmp. The checked-stage clause requires coverage, Size > 0 and the next instruction's covered access, then adds live(Q, P1, …).
• interp.pl: renew runs access_res/7 on Q1's value; a failure is out_of_bounds for a freed object, readonly for a write to ro(_), and unchecked(span) otherwise.
• filc_amd64.pl: single_proofs/3 maps a renew's Q to P1 (only when Q1's check is itself single), renewed_inst/8 refuses anything else, a cas or an offset, and inst(fused(renew(…), _)) emits the flight load of P1, testb $4 or $6, -2(%rcx) and jnz to the check's fail label, then the access. inst_check_kind/2 knows the renew.
• check_reuse.pl: for each remaining heap check followed by a scalar or ordinary pointer access, the pass takes the shallowest dominating source of the same root at distance 0 that covers it. Subsumption and dominance are transitive, so that source is never itself renewed.

The validator and pass previously rescanned every fact at every definition, which was quadratic. Evidence is now indexed by the names it mentions (ir.pl ev/3, check_reuse.pl st/3), and a definition kills only the facts indexed under its name. Reuse-mode output on 560 corpus files, with and without -O, is byte-identical to 7ebcae8's.

Tests: unit renew_validation (accepted after a call, across a poll edge and a polled back edge; rejected when Q1 does not dominate, is later in the block or is defined twice, when P1 is also a phi, in a setjmp function, for a wider range, a range starting below Q1's, an offset Q1's alignment does not reach, a stricter alignment, an empty range, an access not next, and a renew of a renew; the emitter refuses the two-definition cases on its own), renew_semantics (a free before the renew traps out_of_bounds, a read-only write traps readonly, a wider or stricter span is unchecked(span)), and renew_pass (a loop's read and write after a call are renewed, the interpreter agrees; wrong-object and wrong-distance rewirings pass the validator but not renew_refines; the pass's facts end at a redefinition of the pointer). Natively: tests/renew-trap.sh builds tests/c/prog/renew-free.c (the object is freed by a call inside the loop) and renew-readonly.c (a write after a read to a read-only object) with -O under both reference and renew. It requires fewer full checks in the renew build and the same stdout, exit status and whole stderr, with addresses and the pid masked: the message ("cannot read pointer to free object.", "cannot write to read-only object."), the pointer's state, the expected bytes and the origins, after the same output. tests/c/prog/const-read-renew.c renews reads of a read-only object, which must not trap. The Nix check runs difftest, run-c under FUGC_SCRIBBLE/FUGC_VERIFY (including reuse-gc, whose reads after c_gc are renewed without -O), progtest and --registers=temps under renew. The hello, zlib, Lua, bzip2, lz4 and SQLite checks also build a renew variant that must match filcc.

Measured (round 4)

User instructions (callgrind, millions; Lua seeds its string hash from addresses and time, so its rows move by up to 3% between identical runs). Each workload's output is byte-identical across the three builds.

Compile time (one process at a time on this orb; seconds of wall time):

The 3000-statement function took 148 s (reference) and 212 s (reuse) without -O before this round. The pass took 84 s and each validation 41 s; they now take 0.55 s and 1.0 s. The rest is emission, which reuse and renew shorten by removing checks. On sqlite3.c without -O, the phases are: validation 13–15 s each, reuse 8.0 s, its refinement check 2.1 s, renewal 4.7 s and its refinement check 3.5 s. Renew mode validates once after both passes, since a renew keeps its check's proof and index.

Renewal as the -O default

After the cheap middle end became the -O default (c30eed9, --simplify=full), the gate was measured again. User instructions, callgrind, millions, -O against -O --checks=renew on the same tree, with outputs byte-identical:

Simplification removes none of the same work; the share renewal removes grows. sqlite3.c compiles in 280 s with reference checks and 293 s with renewal (+4.8%, serially on this orb). So -O now selects --checks=renew; without -O, and with --checks=reference or --checks=reuse, nothing changes. The snapshot pins --checks=reference, and check.nix keeps -O --checks=reference suites, as do the hello, zlib, bzip2, lz4, Lua and SQLite checks (O-refchecks, refchecks-optimized, refchecks).

Natively, too: tests/c/prog/renew-irreducible.c renews a check made inside an irreducible loop (entered at two blocks) and traps after a free exactly as the reference does, and pointer-store-renew.c renews a pointer store (flag test, ensure-aux, barrier, store) after a malloc and a forced collection each iteration, under FUGC_SCRIBBLE/FUGC_VERIFY in progtest. A unit case accepts a renew in a block of an irreducible loop that only the checking block enters, and rejects one in the loop's other entry.

Reverted on time. Defaults are judged on time, not instructions. On a quiet swa (Zen 4), the gate's geomean was 2.00 with renewal against 1.98 with reference checks, and bzip2 -d ran 24% slower (2.83 against 2.29) despite 10% fewer instructions. In BZ2_decompress pipeline resyncs went from 0.03M to 7.1M. These are memory-dependence mispredictions in the frame-to-frame phi copy blocks, and they vanish with speculative store bypass disabled. Renewal keeps P1 live, which grew the frame from 1296 to 1712 bytes and changed those copies; the flag test itself accounts for about a third of the cost (perf.md). So -O selects --checks=reference again, and --checks=renew stays selectable. Renewal can come back once no gate workload is slower with it.

Default again (on the pointers base). With renew reading the replaced check's own pointer (49cd76d) and -O defaulting to --registers=pointers (fae7737), the quiet swa gate (7 trials, load 0.8) has a geomean of -O 1.85, renew 1.81 and guard 1.82, and renewal is nowhere slower than -O beyond noise: bzip2 -9 1.71 to 1.61, bzip2 -d 2.33 to 2.25, lz4 -9 2.08 to 1.93, SQLite 1.84 to 1.78. bzip2 -d's resyncs stay at baseline (41–43k). Guard loses 5% on lz4 -d, so it stays opt-in. -O selects --checks=renew again, with a4351bc's configurations: check.nix runs renew without -O and keeps -O --checks=reference suites, the program checks build O-refchecks (refchecks-optimized, refchecks), and the snapshot pins --checks=reference.

To find the sites that cause the resyncs, NANOFIL_RENEW_SITES=Fn:From-To keeps only function Fn's renewals numbered From to To − 1, in the pass's block order, and leaves every other check in place (Fn alone keeps all of Fn's). Any subset of renewals is valid checked IR, so the selector needs no rule of its own; it is for bisecting, not a mode.

Review (result)

Oracle reviewed the implementation and found no blockers: no validated input in which a reachable renew runs on a false span or a different P1. It confirmed that the index rewrite kills exactly what the old scans did, and that the passes leave no choicepoints. Its should-fix items were five planted mistakes that every gate missed. Each now has a test and a row above: a read renew testing READONLY, the validator's lower bound and offset alignment, a wrong-distance rewiring, and the pass's pointer index. It also asked for the trap comparison to cover the whole stderr. A renew's in-block proof now maps through Q1, so a twice-defined renew result is no longer refused. Not covered then, both since covered (next section): Q1 in an irreducible loop, and a renew fused with a pointer store under GC stress.

Addendum: renew reads its own pointer

Why. On Zen 4, bzip2 -d runs slower with renewal than without (perf.md): memory-dependence resyncs in BZ2_decompress go from 0.14M to 7.2M, and the perf thread found they follow the frame renewal produces, not particular sites. That frame is 1712 bytes against 1296, and all 416 extra bytes are pointer-pool slots: the function zeroes 47 lowers at entry instead of 21, so 26 more pointer slots of 16 bytes. They come from P1's live range. The emitter loads the flags byte through P1's lower, so live_inst reads P1 at every renew, and single_proofs maps the renew's proof to P1, so a later reused access reloads P1 too. P1 is otherwise dead after its check's access; the interval allocator then keeps it from first touch to its last renew, across most of the function, and its slot is shared with nothing in between. The deleted check's own pointer P is live at the renew anyway, because it was that check's operand, and carries the same address and capability.

The term. renew(Lo, Hi, Rights, Align) reads [a Q1, p P], where P is the pointer of the check it replaces. The grammar change is the second operand only.

Acceptance. Rules 1–5 above, and in addition:

6. same_pointer(Once, P, tmp(P1)): P and P1 reach one single-definition base B through guard_chain/3 (round 5's walk over single-definition add, sub and copy flights whose lower donor is their address operand) at point offsets K and K1 with K ≡ K1 (mod 2⁶⁴). P == P1 is the case B = P1, K = K1 = 0.

The fact the renew adds after its access is live(Q, P, …), keyed by P, not P1. That is the fact the replaced check added. Rounds 1–3 run before renewal, so every later access that reads Q was validated against live(Q, P, …), and its kills, P's redefinition or store, stay as they were.

Why it holds. Let Y be the renew. Every definition on either chain dominates Y: P's chain because P is Y's operand, P1's because P1's definition dominates Q1's check, which dominates Y (rule 1 and strict SSA). B's definition dominates each of them. Lemma: if B's definition dominates D and D dominates Y, then on every path from entry to Y, D runs after B's last run before Y. Otherwise join a path from entry to B's first run, which contains no D because every D is preceded by B, to the suffix from B's last run to Y, which contains none by assumption. The result is a path from entry to Y that avoids D, a contradiction. Applied link by link, every flight on both chains last ran on B's current value, and a flight's address and lower are functions of its base's (a constant offset, the base's lower). So at Y, P and P1 have B's capability and addresses B + K and B + K1, equal modulo 2⁶⁴, as flight computes them. Irreducible loops change nothing, since the argument uses only dominance. Rule 1's argument that P1 still holds the value Q1's check saw stands, so P names the object whose span and alignment Q1 proved.

Interpreter. renew with operands [ptr(A, Cap), V] runs the access test on ptr(A, Cap) as before when V is ptr(A, Cap) (the same address term and capability), and yields it. Otherwise the result is unchecked(alias): rule 6 was wrong. So a validator mistake shows in difftest as a changed outcome.

Emission. The flight load is P's, from P's slots. live_inst reads P at the renew, and single_proofs and the in-block proofs map the renew's Q to P, when P has one definition, as for a check. P1 is no longer read. The fail call gets %rax:%rcx = P, exactly the deleted check's pointer, so the report is the check's own (before, it was P1, which was equal).

What does not change. Rules 1–5, the interpreter's outcomes for a valid renew, and the masks and fail labels. renew_refines/2 still requires distance 0 through round 3's relation. The pass writes P as the second operand and renews only where same_pointer/3 holds, so it makes nothing the validator rejects. The validator now also rejects the wrong-distance and wrong-object rewirings that only renew_refines/2 caught before.

Review. Oracle found the argument sound: phis and parameters as the base, irreducible loops, unreachable cycles (a renew there never runs), point offsets exact modulo 2⁶⁴, and keying the fact by P, whose readers the renew dominates. P's slot is live and unshared from its definition to the renew, and pointers are never register-homed under --registers=temps. The one blocker: the pass related P and P1 by round 3's unbounded walk, and guard_chain/3 stops at 64 links, so a 70-step p++ chain made the validator reject the pass's renew, a compile error. The pass now calls same_pointer/3 itself (the 70-link C file compiles and runs as filcc's; renew_pass checks 10 and 65 links). Planted mistakes:

Measured. Frames under -O, in bytes, with the pointer slots zeroed at entry in brackets (16 bytes each):

All 416 bytes renew added to BZ2_decompress were pointer slots of P1s kept live; 400 are gone, and the remaining 16 bytes are one pointer slot, not cut by any site range (NANOFIL_RENEW_SITES ranges of 100 all give 1312, and so does --checks=reuse, which renews nothing). Guard's larger Lua and SQLite frames are span-test results G, scalar slots live through their loops. Instructions (callgrind, millions, main thread for SQLite) barely move: zlib -6 6794 against 6874 before, bzip2 -d 3731 against 3741, SQLite 19606 against 19713; guard zlib -6 6554, bzip2 -d 3680.

The resyncs went with the frame. bzip2 -d on swa at 49cd76d (perf thread, counts only; swa was loaded, so no cycles yet):

Before the addendum, renew and guard had 8.46M and 8.72M resyncs. Renew now matches the NANOFIL_RENEW_SITES=BZ2_decompress:0-690 build: baseline resyncs with all of renewal's instruction savings.

Quiet swa (perf thread, 49cd76d, load about 1). bzip2 -d, minimum of 5 runs, twice: reference 1.060G cycles, renew 1.016G, guard 1.026G. Gate time against filcc -O2 (7 trials, instructions in brackets):

Renewal now wins in time (2% overall, 4% on bzip2 -d). Guards run fewer instructions than renewal but are slightly slower.

Range guards (round 5): contract, reviewed

Round 4 renews a check only when an earlier full check of the same pointer dominates it. Inside a loop, the check of a[i], or of a field of a state pointer that nothing checked before the loop, still runs in full on every iteration. This round tests, once and without trapping, whether the object covers every byte the loop's accesses through one pointer can reach. Each access then runs as a renewal when that test passed, and as its unchanged full check when it did not. No check moves, and nothing traps earlier.

Measured first

Method (scratch, not kept): the gate's programs built with the -O default at a4351bc (renewal on), a symbol at every block label, callgrind's per-block counts, joined to a classification of every full check left after renewal. Every class below needs a loop-invariant root pointer, meaning a single definition outside the check's innermost natural loop.

• inv: constant offset from the root, with no dominating check before the loop (such as s->lookahead in deflate_slow).
• narrow: the offset is a zero- or sign-extended byte or short, scaled and shifted by constants (ftab[c]).
• mask c, mask v: the offset is bounded by and or urem with a constant (c) or with an invariant name (v, such as zlib's & wmask).
• iv: the offset is affine in a basic induction variable, with a dominating exit test against an invariant (ptr[i] in mainQSort3).

Executed full checks, millions, after renewal:

What is not guardable:

• Offsets loaded in the loop (block[ptr[i]]).
• Roots loaded in the loop (s->window reloaded after a store), which a middle-end load hoist would make invariant.
• Pointer phis (p++, Lua's pc).
• Induction variables without a bound test (while (a[i])).
• Checks outside any loop.

Bounded induction (the block[i] case) is 33M of bzip2 -9's 286M and nothing in zlib. So the guard is the mechanism, in two slices:

1. Slice A, constant spans: inv, narrow and constant masks. The guard's span is constants relative to the root, and no names or induction rule are needed. It covers about 150M of the 220M guardable.
2. Slice B, symbolic spans: linear forms over invariant names, for iv and for symbolic masks (ext(uw)(and(x, m)) lies in [0, V] when V is ext(uw)(m), a guard argument). Contracted below and implemented after slice A is measured.

Expected cost:

• A full read check is 8 instructions after its flight load (null, lower and upper tests), and a write check adds the flag test.
• The guarded renewal's fast path is 4: a test of G, a branch to an out-of-line full check, the flag test and its branch.
• So a passing guard saves about 4 instructions per read and 6 per write. For slice A that is roughly 3% of zlib -6, 2.5% of bzip2 -9, 2% of bzip2 -d and 2% of lz4 -9, if every guard passes.
• Versioning the loop (a copy whose accesses are plain renews) would save about twice that. It can be accepted just as locally (see Review), and is left for later.

The fact

span(G, P0, Lo, Hi): if G = 1, then when G's span test ran, P0's capability was non-null and its object's bounds contained every address in [addr(P0) + Lo, addr(P0) + Hi), computed modulo 2⁶⁴. By round 4's lifetime lemma, an object's bounds change only when it is freed, which empties them and sets FREE. So the fact holds for the same object until it is freed, and every access that uses it still tests FREE and READONLY itself.

The terms

Two new ops, a grammar change that needs separate approval:

Like check, renew_if is followed immediately by its first access, which reads its result at offset 0. Both ops are on evidence_preserving/1. After its access, renew_if adds live(Q, P, Lo, Hi, Rights, Align), so rounds 1–3 can reuse Q. The emitter's single_proofs and fused_insts map Q to P, as they do for a check. Without this, a guard at the end of idom(H) would end the round-2 facts that enter H over the plain preheader edge.

Acceptance (validator, independent of the pass)

let(tmp(Q), a, renew_if(Lo, Hi, Rights, Align), [P, tmp(G)]) is accepted iff all of these hold:

1. G has one definition, a span_test(GLo, GHi) of [P0 | Vs], and strict SSA makes it dominate the access.
2. Every name the derivation passes through has exactly one definition by temp_defs/3: P0, each V, the flights from P0 to P, every offset temp, and in slice B the induction variable, its increments and the exit test's condition. definitions_dominate alone accepts a name defined twice when one definition dominates the use. Reading "the" definition of such a name would be unsound.
3. The function has no setjmp.
4. P is P0 plus an offset, through flights add and sub whose lower donors chain to P0 (round 3's relation, with non-constant offsets). A sub flight negates its term's interval. The offset's interval is [OLo, OHi], by the rules below. Each end is compared separately: GLo ≤ OLo + Lo and OHi + Hi ≤ GHi. In slice B the coefficient vectors must be equal and the constants are then compared.
5. The next instruction is an access it covers, with heap effects, as for check.

Interval rules. An interval bounds the signed value of a temp in its own width. A constant is first reduced to signed in that width (the IR stores w values unsigned). A rule rejects when its conditions fail.

• const(c): [c, c], c taken signed in its width.
• ext(ub), ext(uh) of anything, and raw_load(ub/uh): [0, 255] and [0, 65535]. For sb and sh: [−128, 127] and [−32768, 32767].
• and with const(m), 0 ≤ m < 2^(width−1): [0, m]. urem by const(m), 0 < m ≤ 2^(width−1): [0, m−1].
• ext(sw) of a w interval: the same interval. ext(uw) only of an interval within [0, 2³¹).
• shl by const(k), 0 ≤ k < width, and mul by const(c): scale both ends, swapping them for c < 0. add of two intervals, and sub of a constant, add the ends.
• In class w, every end of a result must lie in [−2³¹, 2³¹) for every value its names can take: a guard V that is ext(sw) of a w name ranges over [−2³¹, 2³¹), any other over the full 64-bit range. This rules out a[i + k] with a w add that wraps. In class l no fit condition is needed. The program's value is congruent modulo 2⁶⁴ to the exact form, and the guard bounds the exact form with overflow detection (Emission).
• Slice B, names: a guard V, or a w name x such that some V is ext(sw) of x: [V, V].
• Slice B, basic induction variable i. i is a phi in block H. Each of its operands from a reachable predecessor is either Init, the same name everywhere (a V, x as above, or a constant), or a single- definition add(i, const(1)) of i's class, whose definition is dominated by T. Some block E ends in branch(tmp(c), T, F), read from the jump term, with edge_label(F) ≠ T. Here c has one definition, cmp(slt, K) of [i, N] with K i's class and N of the same forms as Init. T's only reachable predecessor is E, and T dominates the access. Then i is in [Init, N − 1] at the access.
  • Why: H dominates the cmp, because the cmp uses i. The cmp's block dominates E, and T dominates both the access and every increment. So every increment of i followed a passing test i < N ≤ max, and cannot wrap. And the latest test before the access saw the current i.
  • This needs only dominance and single definitions, so irreducible loops, multiple latches and multiple exits change nothing. When Init ≥ N, the access never runs.

At the access, G, P0 and every name above hold the values the guard used, by round 4's dominance argument. Any path from the guard to a redefinition and on to the access would yield a path from entry to the access that avoids the guard.

Interpreter

span_test is 0 for a none, fn(_) or ext(_) capability, and otherwise compares the object's current bounds with the span computed over unbounded integers, modulo 2⁶⁴ as native code computes addresses. renew_if with G = 0 is check. With G = 1 it runs the full access_res/7:

• a freed object traps out_of_bounds;
• a write to ro(_) traps readonly;
• a misaligned address traps misaligned, as the check would, because the fast path tests alignment itself;
• any other failure is unchecked(span), meaning the guard or the interval rules were wrong.

Emission

span_test:

• P0's flight load into %rax:%rcx; G = 0 if %rcx is null.
• GLo and GHi as signed 64-bit values, with imul and add overflow (jo) sending G to 0. In slice A they are immediates.
• L = %rax + GLo and H = %rax + GHi, modulo 2⁶⁴.
• G = 1 iff lower ≤ L < H ≤ upper (-16(%rcx)), compared unsigned.

This reads only what a full check reads. Special objects and the free singleton have upper = lower, so their guard fails.

renew_if:

flight load of P                       ; once, for both paths
cmpl $0, G ; je .Lfull_<blk>_<i>
testb $Mask, -2(%rcx) ; jnz <fail k(Size, Write, Align)>
[alignment test as in access_check//2, when Align > 1]
.Laccess_<blk>_<i>: <Access>
…
.Lfull_<blk>_<i>:                      ; out of line
<access_check//2 of P, to the same fail label> ; jmp .Laccess_<blk>_<i>

Both paths fail to the same label, with %rax:%rcx = P and the same origin, so the report is the check's. Labels are per block and index (local_label/5), and inst_check_kind knows the op. Liveness reads P and G, and G is a w temporary, homed across calls.

The pass

For each natural loop with header H (natural_loops skips irreducible cycles), in a function without setjmp, the pass takes each full check left after rounds 1–4 that is followed by a scalar or ordinary pointer access, and whose root P0 and every derivation name meet the rules above and are defined outside the loop:

• It groups these checks by root, and in slice B by coefficient vector.
• For each group it emits one span_test at the end of idom(H), over the group's least Lo and greatest Hi. Every name used in the loop and defined outside it dominates H, and so the end of idom(H). A branch ending idom(H) reads its condition after the guard, and the guard writes only G.
• Each check in the group becomes a renew_if on that guard.

guard_refines/2 accepts exactly this rewrite: new span_test lets at block ends, and checks replaced in place by renew_if with the same range, rights and alignment. It is selectable as --checks=guard (rounds 1–4, then guards), off by default until measured.

Observation contract

• The guard never traps, reaches no safepoint, and writes nothing but G. A failing or unused guard changes cost, not outcome.
• Every renew_if stands at its check's index with the same origin, range, rights and alignment. With G = 0 it is that check. With G = 1 the bounds part is proven, and the fast path tests everything else the check tests: FREE, READONLY for a write, and alignment. So it traps exactly when the check would, with the same reason.
• Calls and back-edge polls may free the object. FREE is then set, and the next access traps "free object" as the reference does.
• A free racing another thread between guard and access may pass unnoticed, the same tolerated race as round 4. free_impl writes upper before it sets FREE. FUGC never writes upper, and P0 keeps the object mapped while the guard reads it.

Tests and plants (planned)

• Validator rejects:
  • a span missing either end by one byte;
  • another root, or another lower donor;
  • a guard that does not dominate the access;
  • a twice-defined offset name, V, P0, i, i+1 or c;
  • a latch increment not dominated by T (it skips the test);
  • branch(c, T, T), and an exit taken on the true edge;
  • ult, step 2, and Init not among the guard's forms;
  • a w add that can wrap (a[i + k]);
  • and with 0x80000000 in w, urem by 3·10⁹ in w, and shl by the width or more;
  • a symbolic mask in slice A;
  • setjmp.
• Interpreter:
  • a forged guard gives unchecked(span);
  • G = 0 behaves exactly as the check;
  • G = 1 traps out_of_bounds after a free, misaligned on a misaligned address, and readonly on a write to ro(_).
• Native (trap text compared as bytes):
  • guards that pass and fail (one element short);
  • with G = 1: a free inside the loop, a misaligned int *, a write to a const table;
  • guards on malloc(0), a freed object and a special object;
  • zero-trip loops, and Init > N;
  • byte-indexed tables of 256 and 255 entries;
  • an idom(H) ending in a branch, and an H with two entries;
  • G kept across calls under --registers=temps;
  • two renew_ifs in one block, and reuse of a renew_if's Q;
  • GC stress with renewed pointer stores.
• Plants:
  • the guard drops jo, or compares upper signed, or H < upper;
  • the slow path skips the flight load or the alignment test;
  • the fast path skips FREE;
  • liveness drops G;
  • span_test is missing from evidence_preserving;
  • a sub flight is not negated;
  • the narrow rule treats sb as unsigned;
  • the IV rule ignores where the increment is dominated, or takes predecessors from the CFG's ordsets;
  • the interpreter maps misaligned to unchecked;
  • guard_refines accepts a moved check.
• Gate: snapshot identical; the Nix checks with a guard variant; instructions before and after on bench/run.py; compile time on sqlite3.c.

Review

Oracle reviewed this contract before any implementation. It found three blockers in the first draft, all now fixed in the text above:

• the IV rule let a latch increment that never passed the exit test wrap i (now: every increment is dominated by T);
• it read definitions of names that may have several, and took the exit edge from the CFG's ordsets, where branch(c, T, T) looks like a single edge (now: single definitions throughout, and the edge is read from the jump term);
• it stated its fit conditions for 64 bits while w adds wrap at 32 and w constants are stored unsigned (now: signed intervals per width, and an exact, overflow-checked guard, which makes l-class arithmetic need no fit condition).

Its should-fix items are folded in: misalignment keeps its trap under G = 1, odd capabilities give 0, both ops preserve evidence, the flight load is shared with an out-of-line slow path, and the arithmetic is stated exactly. It also proposed the cheaper slice A.

It confirmed that the guard's reads are safe against free, special objects and FUGC. It confirmed the dominance argument and the guard's placement at the end of idom(H), including several entries and a branch there.

For later: versioning can be accepted just as locally. In the copy, an access may be a plain renew when it is dominated by a block T whose only predecessor E ends in branch(G, T, F) with F ≠ T. guard_refines would then also check that the copy is a label-renamed duplicate.

Not verified: vfork, dlclose and thread-exit header paths (as in round 4), and how often guards pass at run time.

Survey: guards, hoisting, versioning, peeling, cheap wins

Before choosing new ops, every full check that the -O default (renewal on) leaves was counted once on the gate. The method is the one described under "Measured first". The extra rules are these:

• Hoist: the root is a pointer loaded in the loop, from an address whose root is invariant. The loop has no call and no pointer store, and the load executes on every iteration before any exit (or after a side-effect-free header test, with loop rotation). Otherwise the hoisted load's check would move.
• Peel: a constant-offset check of an invariant root whose block dominates every latch. Peeling one iteration lets the loop's copy renew it with today's ops. Counted net of loop entries.
• Distance > 0: a dominating check of the same root at another constant offset whose span covers this one.
• Fields: a dominating check of the same root that does not cover this one.

Executed full checks removable (millions), and the instructions saved as a share of the run. A guarded access saves 4 (read) or 6 (write) instructions. A versioned or peeled access, which becomes a plain renew, saves 6 or 8.

* Only with type-based aliasing (scalar stores in the loop) and loop rotation.

• Hoisting removes almost nothing under the trap rule. The large "root loaded in the loop" sites either sit in loops with calls or pointer stores (bzip2's copy_input_until_stop, handle_compress), or their load is conditional inside the loop (zlib's deflate_slow L342, the hash insert behind if). Hoisting such a load would run its check on paths that never ran it.
• Distance > 0 renewal finds nothing. Pizlonated checks start at offset 0, so a dominating check of another field never covers this one.
• Write evidence covering a later read is already used, and what remains of distance-0 coverage is 0.2–2.3M.
• Fields of an already-checked struct are mostly in the guard classes. Covering them is span_test's job, not a cheaper rule.
• Peeling uses today's ops and validator only (a middle-end loop copy), and reaches 1.1–1.4% on bzip2 and nothing elsewhere.

Instruction counts are only a proxy here. On swa, renewal is 10% fewer instructions but 24% slower on bzip2 -d (perf.md, BZ2_decompress's layout), while on this orb it is 4% faster than reference checks on the same workload.

Slice A: implementation

--checks=guard runs reuse, then renewal, then guards (check_reuse.pl's guard_checks/2), and validates the result once. It is opt-in. The reference and renew paths are unchanged: the snapshot is identical, and --checks=renew output is byte-identical to before on the gate.

• IR (ir.pl). span_test(Lo, Hi) (w, [p]) and renew_if(Lo, Hi, Rights, Align) (a, [p, w]), both checked-stage and evidence-preserving. stage_sources/3 builds once per function the map of single definitions that renew and renew_if read (empty with a setjmp). guard_chain/3 walks P's single-definition add, sub and copy flights to each base, adding offset intervals (offset_interval/6: constants signed in their width, narrow extensions and loads, and with a non-negative constant, urem, shl, mul by constants, add, sub of a constant, ext(sw), ext(uw) of a non-negative interval, w results within [−2³¹, 2³¹)). guard_covers/5 accepts when G's single definition is a span test of a single-definition base on that chain whose span holds both ends. A renew may also read a renew_if's proof, which proves the same bounds as the check it replaced.
• Interpreter. span_test compares the object's current bounds, modulo 2⁶⁴, and is 0 for anything but an object's capability. renew_if with G = 1 runs the whole access test: a freed object traps out_of_bounds, a read-only write readonly, a misaligned address misaligned, anything else is unchecked(span).
• Emission. The span test is the flight load, a null test, two leas and three unsigned compares, then 0 or 1 into G's slot. renew_if loads P's flight once, then cmpl $0, G; je .Lfull, the flags test of round 4 and the alignment test, and its access after a local label. Each .Lfull path is emitted after the function's failure blocks: the full access_check//2 to the same fail label, then a jump back. G is read by cmpl from its slot, so it never takes a register home, and the liveness view of a guarded access is uses(Access, [G]) (cfg.pl, filc_abi.pl), which keeps G's slot live through the loop.
• Pass. A check followed by a renewable access is a candidate when its pointer's chain reaches a base defined outside a loop around it whose definition dominates that loop's idom(H); the outermost such loop is taken. The idom(H)s of one base and kind that lie in the same loop (or in none) share one guard, at the end of their nearest common dominator, or of the base's definition block (the entry, for a parameter) when that is deeper; a place inside another loop falls back to each idom(H). So one guard serves every loop reading the base and runs only where every path to those loops runs. A guard placed per loop, as first built, made bzip2 -d slower: BZ2_decompress has dozens of bit-reading loops that run once or twice, each paying a span test for two accesses. Spans of one base, place and kind are clustered: constant offsets where they overlap or lie within 64 bytes, and each distinct ranged span alone, since a span test fails as a whole. A ranged span wider than 256 KiB is skipped, and so is any span whose ends leave the signed 64-bit range, which no span_test can state. The first is a type's bound times a stride (bzip2's s->len[t][v] for a byte t spans 1 MB of a 55 KB state), so its guard would always fail and add the test of G to each full check. guard_refines/2 accepts only fresh span tests at block ends and checks replaced in place by renew_if of the same operands. None of this placement is trusted: the validator checks each renew_if against its guard's single, dominating definition.
• NANOFIL_RENEW_SITES (round 4's bisect selector) applies to renew mode only.

The emitter's fused_insts no longer scans the block's proofs at each instruction: they are an assoc from proof to pointer and an index from pointer name to proofs, so a block with tens of thousands of checks (a large struct copy) is not quadratic. A 16 KB struct copy compiles in 16.5 s instead of 22.1 s under -O, with the same output.

Tests:

• Unit: guard_validation (one byte short at either end, byte tables of 256 and 255, a signed byte, a sub flight, masks and scales, w arithmetic that may wrap, and with 2³¹, urem by 3·10⁹, shl by 32 and by 64, ext(uw) of a signed byte, mul by −1, a w constant 0xFFFFFFFF, urem one element short, another root, another lower donor, a non-span guard, an offset name or base defined twice, setjmp, no access after it, a guard that does not dominate), guard_semantics (the span test's ends, a freed object, G = 0 as the check, G = 1 after a free, misaligned and read-only, a forged guard) and guard_pass.
• Native, whole stderr against reference checks (renew-trap.sh): guard-free (G = 1, freed in the loop), guard-short (G = 0, one table entry short of the span), guard-below (the span's low end below lower), guard-readonly (G = 1, a write to read-only data), guard-misaligned and guard-misaligned-slow (G = 1 and G = 0), guard-pressure (G's slot under frame-slot sharing).
• Native against filcc (progtest, under FUGC_SCRIBBLE/FUGC_VERIFY): guards.c, with passing and failing guards, a centred signed index, zero-trip loops, nested loops, two loop entries, facts crossing the guard into an else arm, guards on empty, freed and function objects, and guarded pointer stores across forced collections.
• check.nix runs difftest, run-c and progtest under guard with and without -O, and the corpus under -O.

Plants, each run against unit, renew-trap.sh, difftest and progtest (with and without -O):

Oracle's review of the result found one blocker, now fixed: a span end outside a signed 32-bit displacement was built as movabsq $Hi, %rax; addq %rax, %rax, which doubles the address instead of adding to it. Validated IR (span_test(2³² − 8, 2³²) of a global) returned 0 natively and 1 in the interpreter, and before guard_worth bounded ranged spans a C loop read 8 bytes past its object under setarch -R. The immediate now goes through %rsi (movabsq $U, %rsi; leaq (%rax,%rsi), Reg), and tests/filc/guard-span.ir (each end past 32 bits, an inverted span, one byte more than the object) is in the difftest lists. The review's other findings, also fixed: the pass could make a span_test past 2⁶³, which the validator rejects (a compile error, now span_fits/2); offset_interval walked shared subterms once per path, exponential on x = x + x repeated (now memoised per name and class); the pass's loop list per block was blocks × loops (now one walk over the loop bodies); and a fresh guard name could equal a parameter's. Five interval rules had no test that failed when they were broken; each now has a unit reject (the table above).

Measured (slice A)

User instructions, callgrind, millions, all three builds of the same tree (a12cc89 plus slice A), with outputs identical. Lua and SQLite run collector threads whose counts vary by up to 25% between runs (Lua str totals 4.2–5.5G under renew alone), so their rows count the main thread only; lz4 compresses on worker threads, so its rows count all threads. An earlier table, from all-thread totals, credited guards with −3.8% on Lua str: that was collector noise.

Slice A yields less than the survey's estimate (2–3%) on bzip2. bzip2 -9's largest slice-A sites in sendMTFValues index s->len[t][v] and similar tables with a byte t, so their spans exceed the 55 KB state, and the guard is skipped. On copy_input_until_stop it saves 6%.

Compile time on sqlite3.c with -O, the three modes compiled at once on this orb: reference 302.7 s, renew 314.5 s, guard 321.6 s (+2.3% over renew). A loop around a 1500-case switch compiles in 17.0 s with renew and 18.7 s with guard; Oracle measured 11.1 s in the pass alone before the loop lists were built once per function.

BZ2_decompress's frame is 1728 bytes under guard, against 1712 under renew and 1296 under reference checks, with 98 guarded accesses. The perf thread found renew's bzip2 -d time regression on Zen 4 to follow the frame renewal produces (memory-dependence resyncs), so guard, which builds on renewal, likely inherits it; its resync count needs swa.

Time on swa is not measured here, since this orb cannot reach it. A default depends on that measurement. It also depends on renewal's own bzip2 -d regression in time, which the perf thread is bisecting with NANOFIL_RENEW_SITES, because guards build on renewal.

Limits

• No motion. Rounds 1–3 carry no evidence around a loop, because every back edge polls and a poll kills every fact. Round 4 keeps only bounds and alignment across polls and calls, and still tests the flags at every access that a full check guarded; spatial facts first established inside a loop do not reach its header.
• Across an edge, only proofs and pointers with a single definition.
• Rounds 1–3 reuse for scalar consumers only; pointer accesses keep their check, or (round 4) its renewal.
• Same SSA pointer, or (round 3) a constant-offset flight from the same root with the same lower donor: a variable index (a[i], a[i+1]) or a pointer reloaded from memory is not related.
• Read evidence never covers a write under rounds 1–3; a round-4 renew of a write tests the read-only flag itself.
• Local (check_local) and function proofs are not reused.
• Polls, alloc and helper exits are trusted to the invalidator list and native tests; the interpreter models only explicit free.
• Renewal needs distance 0, single-definition Q1 and P1, and no setjmp in the function; a variable index (block[i]) in a loop is not covered (the "index" column above), which is the next contract.