M5: analyses, promotion, copy elimination and local storage

The plan is in PLAN.md. This file records the middle-end passes, their analyses and translation validation, and the measurements that guide their implementation.

cd nanofil/src
../bin/nanofil -O cc prog.i > prog.s         # with the middle end
../bin/nanofil -O cc-ir prog.i               # the promoted IR
../bin/nanofil -O difftest FILE.ir OUTDIR   # validate run by run
NANOFIL_OPT=-O ../tests/difftest.sh FILE...     # every suite takes this
NANOFIL_OPT=-O ../tests/progtest.sh

Without -O nothing changes: the IR goes to the backend as loaded. That path is the reference every optimization is checked against.

Source context survives the middle end

Lowered C carries an optional context(Function, Records) beside each function. It records resolved bindings, shallow typed-expression origins, temporary hints, live instruction/phi/jump sites, and eliminated aliases. The grammar is in provenance.pl. Executable temporary names, labels, classes and instruction lists retain their old meaning.

Each pass transports sites while it emits or deletes instructions. Promotion names scalar phis from their original storage binding and marks their origins as generated merges; copy elimination records substitutions without renaming the survivor; local storage retains access origins; pizlonation gives a check and its access the same source origin. Neither source context nor C types are safety evidence. Interpreter/layout and assembly boundaries discard context; checked-IR validation does not erase intervening instructions to make an invalid proof/use pair acceptable.

The playground and workbench consume these compiler products. Subscripted names are presentation only: highlighting uses raw temporary identities. Origin locations still have the parser's enclosing-statement precision, not token spans. Generated merges can have several contributing lines. Historical value records keep displayed numbering stable across passes. Reused executable spellings retire the old definition into history/5; incoming aliases cite historical(Id) rather than accidentally naming the new proof. Promotion shares one conservative store-origin summary per slot: its contributors are not a claim about which stores reach a phi. Metadata-free hand-written IR remains supported, as do legacy loc/2 markers, converted to context at unchecked transformation boundaries.

Modules

 IR module ──▶ opt.pl: optimize(o0 | o1)
                 │ o1
                 ▼
              promote.pl ──uses──▶ escape.pl   which allocs can go
                 │         ──uses──▶ cfg.pl     CFG, dominators, frontiers,
                 ▼                              liveness (pure, assocs)
               copy.pl   ──uses──▶ strict SSA and dominators
                 │
                 ▼
          local_storage.pl ─uses─▶ escape.pl, exact bounds
                 │
                 ▼
              IR module, fewer heap allocs, copies and phis

• src/cfg.pl: pure functions from a function's blocks to assocs keyed by label. Reverse postorder, successors and predecessors; immediate dominators (Cooper, Harvey and Kennedy); dominator-tree children and pre/post intervals for constant-time dominates; dominance frontiers; and a generic backward liveness over any names (gen/kill per block plus uses on edges, which is how phi arguments count). Temp liveness is that instance; promote uses it again for memory slots. natural_loops/3 groups reachable backedges by their dominating header and reports each loop's latches and body.
• src/alias.pl: same-class address expressions with allocation, parameter, symbol or opaque-value bases and modular offsets. These are not disjointness or bounds proofs; see below.
• src/escape.pl: after QBE's ALoc/AEsc. An alloc is local(Size, Accesses) when every use of its address, directly or through add/sub of constants and copy, is the address operand of a load or store; Accesses is the set of acc(Offset, Width). Anything else is escapes(Why): stored as a value, passed to a call, returned, compared, converted with ptoi, offset by a variable, merged in a phi, or a derived temp that is defined more than once. Unknown means escaping; the analysis never guesses.
• src/promote.pl: mem2reg. See below.
• src/copy.pl: same-class SSA copy elimination, after promotion. No load/store elimination or check removal.
• src/opt.pl: optimize/3 for the driver and refines/2, the comparison translation validation uses.
• src/cfg_tabled.pl: the same analyses as tabled relations over asserted facts, versioned and incremental (not alias or natural-loop analysis). They exist for the measurement below and as a cross-check; no pass uses them.

Address expressions and natural loops

alias_facts/2 maps an l or p temp to addr(Class, Base, Offset). Same-class copies and constant additions/subtractions preserve the base. Offsets are signed representatives modulo 2^64, not unbounded byte distances: adding 2^64-1 to p+4 gives p+3. For class p, the capability is preserved too. Parameters, allocations and symbol getters start bases param(T), alloc(T) and symbol(S). Other definitions, including loads, calls, pointer/integer casts, variable arithmetic and phis, start an opaque value(T) base. In particular, a cast round-trip does not acquire the allocation's capability. Word temporaries are not address aliases. Non-strict-SSA functions return no facts; a missing fact is unknown, never proof of safety.

Different bases may alias. A parameter may point into a known alloc or global, and two pointer loads may produce the same pointer. An alloc base names that definition's current execution, not a common object for all iterations of a loop. The facts must not be used on their own to remove checks, infer disjoint objects or move memory operations across control flow. Keeping phis opaque also avoids confusing an earlier iteration's pointer with a newly allocated object.

natural_loops(Cfg, Idom, Loops) maps each header to loop(Latches, Body), both sorted label sets. A backedge's header must dominate its latch. Walking backwards from all those latches, stopping at the header, gives the combined loop body; unreachable predecessors are excluded. Nested loops retain separate entries, multiple latches share one entry, and a self-loop contains only its header. Irreducible cycles without a dominating header are not natural loops. An empty result does not prove acyclicity or permit pollcheck removal.

These APIs are available to later M5/M6/M7 work. Neither is wired into code generation or check removal yet; escape classification and promotion keep their existing, stricter policy.

Validation on both SWI and Trealla compared 500 seeded random CFGs against an independent path-based reference (dominance by deleting a node, loop membership by reachability). On 100 generated functions with shuffled block layout and mixed pointer/integer operations, every alias fact was checked against the interpreter's actual addresses and complete capabilities. The unit cases cover nested loops, shared latches, unreachable predecessors, irreducible cycles, wraps, casts, loads, symbols and non-SSA input. Planted errors in subtraction's sign and the loop-header stopping rule fail their respective unit tests.

tests/bench-cfg.pl now measures both APIs in the Nix check. On swa with SWI 9.2.9, bigfn.py 1 300 (298 blocks) takes 0.002 CPU seconds for loops and 0.013 for aliases; bigfn.py 1 3000 (2572 blocks) takes 0.022 and 0.126 seconds. The latter has 349 natural loops and 363 address facts. Alias timing includes the strict-SSA check; loop timing reuses dominators. Synthetic 1000/4000/16000-link address chains take 0.008/0.033/0.140 seconds on SWI and 0.045/0.212/0.943 on Trealla. Single-ring CFGs of those sizes take 0.011/0.043/0.201 seconds for loop analysis on SWI and 0.077/0.347/1.590 on Trealla, excluding CFG/dominator construction.

promote

An alloc is promoted, all its slots at once, when:

• escape.pl calls it local;
• it is in the entry block, so it runs once per call and its fresh contents are the only initial state (the validator forbids jumps to the entry block);
• its size is a constant and every slot lies inside it, so no access could trap or be undefined;
• its slots do not overlap and each offset has one width, so every load reads exactly the bytes one store wrote;
• in Fil-C mode, p slots are 8-aligned, so no load(p) or store(p, ...) could trap as misaligned;
• the function is in strict SSA form (one definition per temp, dominating its uses). The C frontend's output always is; a function that is not is left alone.

Each slot becomes an SSA variable. Phis go on the iterated dominance frontier of the blocks that store to it, pruned to blocks where the slot is live (Cytron et al.). A walk of the dominator tree replaces loads with the slot's current value and deletes the stores, the alloc and its derived addresses. A narrow load re-extends the stored value (loadsb → extsb, loadsw at l → extsw, at w → copy), which is what the bytes would give. Before any store a slot is 0: Fil-C allocations are zeroed (so a p slot is a pointer without a capability, which traps when used, as before), and in plain mode the bytes are unknown, so 0 is one value they could have had.

What it removes, alloc count before → after:

Plain-mode fixtures are also compiled by real qbe before and after promote. That found a qbe miscompile: qbe's own promote turns loadsw and loaduw of a w slot read at class l into the same copy, so their difference is 0. The repro is tests/backend/load-ext-l.ir, with the other qbe bugs M1 found.

Bearing on safety. In Fil-C mode a promoted local is no longer a heap object, so its loads and stores lose their access checks. That is a removal of checks, and it is sound only because every condition above is established, never assumed: escape classification treats any use it does not understand as an escape, and promote refuses unless every access is inside the allocation, aligned and non-overlapping, so none of the removed checks could have failed. A p value that was in a slot is now a p temp, which the backend roots in its own frame slot, so rooting is unchanged; the GC stress tests pass with -O, also under FUGC_SCRIBBLE=1 FUGC_VERIFY=1. Keeping non-escaping arrays on the stack (the oobp gap in m4.md) is not done yet: arrays indexed by a variable still escape here and stay on the heap.

Copy elimination

copy_module/2 removes same-class temporary copies and w/l constant copies, normalizing constants to their defining width. It rewrites uses in instructions, stores, direct/indirect calls, branches, returns, tuples and phi edges. An l-to-w narrowing copy stays, as do extensions, casts, effects, and symbol/pointer-literal materializations. Symbol copies may call getters; they are not interchangeable with ordinary operands.

The pass reuses promotion's strict-SSA check. A non-SSA function is left entirely alone. Only reachable definitions become aliases; dead uses of those aliases are rewritten too, so removing a live definition never leaves a dangling reference in a dead block. Dead definitions and their possible cycles are not chased. Indexed chains are resolved to terminal values with memoized paths, not repeated whole-function scans. On reversed cross-block chains of 1000/4000/16000 copies, copy-pass CPU time was 0.035/0.149/0.651 s on SWI and 0.239/1.060/4.767 s on Trealla.

Safety review: Oracle approved these rules before adoption. A removed p copy aliases the same address and capability, and the terminal definition still has its own frame root. This preserves still-live capabilities, not accidental retention of dead objects: a loop may overwrite a terminal's slot after its last use. The pass does not promise identical GC/finalizer timing. Keeping pointer materialization also keeps the copy pass from changing module mode.

Trivial-phi elimination

After resolving copies, copy_module/2 also removes a reachable phi when all its non-self inputs name one value. All operands must be same-class temps or w/l integer constants normalized to the phi's width. It keeps all-self phis, differing inputs, narrowing phis and pointer/symbol literals. Dead incoming edges count too; dead definitions stay, and dead uses of removed definitions are rewritten.

A dependency worklist redirects each removed phi's users to its source, then revisits only those users. Dependencies follow the source if it is another candidate phi; terminal values need no user maintenance. Final aliases are flattened with fresh memoization before rewriting the IR. Reverse chains of 1000/4000/16000 invariant phis take 0.019/0.078/0.343 CPU seconds on SWI 9.2.9. An earlier version also merged users into terminal values and took 10.5 seconds at 16000: maintaining those unused sets was quadratic.

Safety review: Oracle approved the singleton-non-self rule before implementation. Strict SSA guarantees that the surviving definition dominates the removed phi: on any first path into its block, the phi cannot yet select itself. A removed p phi aliases both address and capability. Its representative keeps a scanned root. If that representative is an outer loop phi overwritten on the same edge, the remaining phi shadows capture the old pointer before simultaneous updates and the pollcheck. No CFG, memory check, allocation or pollcheck is removed.

The fixtures exercise copy-to-phi chains in shuffled block order, normalized constants, narrowing, self edges, swaps and dead predecessors. Unit tests require removal and retention of the intended phis, recheck strict SSA on the transformed functions, compare exact pointer results, and extend the bounded symbolic return queries. The GC fixture adds three removable inner-loop pointer phis: a fresh anchor and aliases of both outer-loop swap pointers. The anchor is not retained by the list or the C caller. The full Nix check passes on both hosts, including forced GC with scribble/verify.

Negative controls were confined to scratch copies: disabling phi removal fails the structural tests; truncating l phi constants to 32 bits gives $phi_constants(0): ret 2 before, ret 18446744069414584322 after and fails translation validation. Hiding just the anchor's root during c_gc, then restoring its capability from the unscanned address slot, changes the native list checksum from 199990000 to -4702111234274994122 with exit 0. Thus checking the checksum, not just successful exit, catches the lost root.

Compared with 01abcc0, the five existing tests/c/*.c inputs have no trivial phis left after promotion/copy elimination, so their output is unchanged. Generated bigfn.py 1 300 drops from 397 to 395 phis and 37012 to 36904 bytes of object text; bigfn.py 1 3000 drops from 3726 to 3685 phis and 363844 to 361624 bytes. These are modest code-size improvements, not a claimed runtime or compile-time speedup.

Generated-code measurements

Against 73b480c, on swa with SWI 9.2.9, compile tests/bigfn.py SEED STATEMENTS with -O, assemble and link with the same filcc-built harness. These are generated structured C functions, not representative whole applications:

Execution is the median of three alternating before/after runs, summing big(i & 255, 2) over 2000000 calls for the 300-statement functions and 300000 calls for the 3000-statement function. Checksums match. The large function's stack frame shrinks from 166688 to 108256 bytes (35%). This is less stack traffic without introducing register allocation. Compilation remained around 1.9 s for the large input; no compile-time speedup is claimed from this pass. Representative basic.c and hello.c output also shrinks, but much less than these copy-heavy functions.

Validation beyond concrete return values

The two copy.ir fixtures cover narrowing, constant widths, redefinitions, dead cycles, phi swaps, effects, pointer capabilities, globals, indirect calls, tuples, and unchanged null/OOB/readonly/non-function traps. Unit tests compare complete pointer results before/after the copy pass: unlike promotion, it moves no allocations, so pointers into different objects must not compare equal merely because their offsets match.

symbolic_optimized_returns shares CLP(Z) inputs between the original and optimized interpreters and searches for unequal returns, including across branches, loops and initialized concrete-address memory. Labeling closes the finite domains: diamond uses 0..15 × 0..3, the loops 0..6 or 0..7, and narrowing includes both sides of the 32-bit sign edge. Unexpected traps or fuel exhaustion fail the query rather than counting as proof. This is bounded translation validation, not proof for all integers or symbolic addresses. A deliberately wrong truncation finds a counterexample at 4294967296.

The GC fixture now includes 18 removable pointer copies across allocation, forced collections and backedges, including simultaneous pointer-phi swaps. Unit tests require their removal. The unchanged C harness still checks list = 199990000, with scribble/verify enabled in the Nix check. Planted bugs were caught and restored: wrong constant width, bypassed SSA guards, lost pointer identity, and (in scratch assembly) zero scanned roots, which corrupted the GC result despite exiting normally.

Translation validation

main.pl -O difftest runs every # run: line on both the unoptimized and the optimized module in the interpreter, in the same findall step, and fails unless the optimized outcome refines the original:

• undefined behaviour in the original allows anything;
• an unknown result (uninitialized bytes in plain mode) allows any value its constraints allow;
• otherwise the outcomes are equal. A returned pointer into an alloc compares by its offset in the object, since removing allocs moves the others.

Promote keeps every block and branch, so a correct result needs exactly the fuel the original needs. Both run with the same fuel, growing from 1,000 blocks until the original finishes, so a broken pass that loops ends as out_of_fuel cheaply. (The interpreter's memory grows fast with blocks run: a loop of 10,000 blocks took 10 GB and 3 minutes, so a run to the full 1,000,000 would exhaust memory before reporting.)

The optimized IR is also checked with valid_module/1 there and in the unit tests, not on every cc -O, because the validator is quadratic in the number of blocks (11.7 s for a 1557-block function in the corpus). That function, c-testsuite/00200, takes 21 s to compile without -O, over the corpus check's 20 s limit, so the check now allows 60 s. Computing each block's predecessors once in valid_block (ir.pl) would bring cc-ir on it from 12.5 s to 5.3 s; ir.pl is shared, so that is left to its owner.

The Nix check runs every existing suite again with NANOFIL_OPT=-O: fixtures, qbe-bugs, the 200-function gen.py corpus, tests/filc, tests/c, a 300-statement bigfn.py function, interop, GC stress, and progtest including its scribble/verify run. Each difftest also validates in the interpreter as above. The M4f corpus (tests/corpus.py) was run with -O by hand and gives the recorded outcomes for all 416 sources. It is not in the check twice because of its run time.

A broken promote that leaves every alloc in place would pass all of that. promote_removes_allocs in tests/unit.pl pins which allocs must go and which must stay, worked out by hand.

Planted bugs, each caught and then restored:

Tabled, versioned or functional analyses

PLAN asked whether analyses should be tabled relations keyed on versioned IR facts or incrementally tabled facts, at realistic sizes. tests/bench-cfg.pl runs all three on the largest function of each file and throws if they disagree; tests/bigfn.py generates structured C (nested if/for, early returns, a dozen locals), so the functions have hundreds of blocks and small live sets. CPU seconds, native Trealla 12f4cbd:

The answer:

• Liveness: a wash. The three-rule tabled liveness is never more than 1.5× faster than an assoc worklist, and asserting the facts costs about what the tabled version saves. The first functional version (round-robin until nothing changed) was 2.4× slower at 298 blocks; a postorder worklist closed the gap.
• Dominators: functional, by far. Dominance has no short monotone Datalog form. The tabled one needs a reachability-avoiding-D table per block, so it grows with the cube of the size: 60× slower at 119 blocks, 190× at 298, minutes at 887.
• Incremental tabling buys little. It wins after promote (fewer facts change than a version holds), but after a one-instruction edit it re-derives about as much as recomputing, because each of incremental_live_in(_, _) and incremental_live_out(_, _) is one table that any changed fact invalidates whole.

So passes use cfg.pl: pure, no asserted state, and no driver-level version bookkeeping. The "versioned facts at pass boundaries" exception in PLAN's rules is not needed by M5. cfg_tabled.pl stays as the declarative specification the functional code is checked against in the Nix check.

A Trealla tabling bug. In 12f4cbd, a \+ or if-then-else written inline after a tabled call, in a tabled clause, gives wrong answers. It reported temps live into the block that defines them. The same negation moved into a helper predicate is right:

:- table li/2, lo/2.
li(B,T) :- g(B,T).
li(B,T) :- lo(B,T), \+ k(B,T).     % [b2-x,b1-x,b0-x]: b1 kills x, wrong
lo(B,T) :- li(S,T), p(S,B).
g(b2,x). k(b1,x). p(b2,b1). p(b1,b0).

With li(B,T) :- lo(B,T), notk(B,T). and notk(B,T) :- \+ k(B,T). the answer is [b2-x]. cfg_tabled.pl uses the helper form. This matters to anyone who writes tabled analyses with negation, as the handoff proposed.

Host: SWI-Prolog

The measurements above are on Trealla. After M5 the default host became SWI-Prolog 9.2.9 (PLAN decision 3), with src/swi/ adapting it to the Trealla dialect and bin/nanofil choosing the host. Output is identical on both hosts: the gen1 assembly, the IR of every tests/c file, and the corpus outcomes. Wall-clock times, Trealla against SWI:

Most of the interpreter's time went to CLP(Z) propagation on values that were already integers. The interpreter now computes known values with is/2 and branches on them with if-then-else, keeping constraints for unknown values, and module_prepared/2 indexes functions and blocks once per module. Results are identical; difftest got 2 to 4 times faster on SWI (gen1 with -O: 3.2 s to 0.8 s, about 0.3 s of it startup) and 13 times on Trealla (memory.ssa: 15.7 s to 1.2 s). NANOFIL_PROFILE=N runs any nanofil command under SWI's profiler and prints the top N predicates.

Compiler profiling after the interpreter fast path

The next pass targets compiler work, without changing the IR or emitted code. On swa with SWI 9.2.9, medians of five separate invocations against the preceding revision (e669408ad01c):

Each pair produced byte-identical output. Input generation and Prolog profiling are outside these wall-clock measurements; startup, target profile discovery and printing are included. Peak RSS did not increase: for example, hello.c fell from 163 to 146 MiB. These are local machine measurements, not directly comparable to the earlier orb timings.

The changes follow the profiles:

• Startup: compile-only commands were loading the interpreter and CLP(Z), although neither runs. SWI now autoloads the interpreter on first use; Trealla still loads it normally. The IR module's unused CLP(Z) import is gone. Symbolic runs still use the same solver.
• Preprocessing: located_splice/4 was a leading cost on hello.c. It now shares one File:Line term per physical line instead of constructing one per character; splices and token locations are unchanged. No header or target-profile cache was added.
• Backend: nth0 scans for pollchecks took 26% of profiled compilation of 00200.c. The Fil-C backend indexes block positions and phis once, then looks up both ends of each edge. It still tests layout order, including self-edges, not lexical label order, and emits the same checks and phi copies.
• Promotion: on bigfn.py 1 3000, collecting each slot's store blocks took 51% of the profiled pass and escape-event classification another 15%. Both now group their input once by slot/allocation; assembly uses the existing phi assoc rather than searching its original list. Stable event order preserves the first escape reason. No promotion eligibility, liveness or dominance rule changed. Profiling just promote_module/2 fell from 1.58 to 0.55 CPU seconds; assoc lookups fell from 2.31 million to 0.30 million.

The full Nix check, forced to build locally on swa both times, passed in 31 seconds versus 38 before, including the unchanged Trealla checks. Separate validation compared 92 complete assembly/IR outputs against the old compiler: the existing C and IR fixtures, three extra 1000-statement seeds (2, 3, 17), and a case with a self-edge, non-lexical block order, an unreachable phi predecessor and an unused allocation, all with and without -O. All were byte-identical. Full preprocessing token terms also matched for LF/CRLF splices and multiline comments, including their locations. No permanent tests were added for these representation-only changes; the existing semantic and GC-stress suites still apply.

To repeat the compile profiles, generate the inputs with tests/bigfn.py or tests/gen.pl, then run, for example:

NANOFIL_PROFILE=25 bin/nanofil -O cc big.c >/dev/null
# Measure separately without the profiler:
/usr/bin/time -f '%e s, %M KiB peak RSS' bin/nanofil -O cc big.c >/dev/null

Removing the address-chain scaling cliff

The staging Fil-C compiler already contains the frame-coloring fix: at -O0, always-live allocas made a dense interference graph, and trying colors by repeatedly scanning neighbors made coloring cubic. That fix represents the dense relation implicitly. Nanofil does not have frame coloring yet, but the lesson applies to its existing analyses too.

escape:address_temps/2 used to rescan every constant-offset definition until a fixed point. A chain of N pointer additions resolved one more temporary per round: N whole-function scans even if the definitions were already in dependency order. At 500/1000/2000/4000 links, it used 1.80/7.09/28.18/112.36 million Prolog inferences. That is quadratic work, not just a large constant.

It now indexes outgoing dependencies by source temp and processes only the newly resolved sources. Every edge is visited once, with logarithmic assoc operations. Breadth-first layers preserve the old result when definitions compete: earliest resolved layer wins, then original instruction order. Already-resolved temps never change, and unrooted cycles stay unresolved. This changes neither the escape policy nor promotion eligibility; it makes this part of M5 scale before adding more alias and copy analysis.

Complete -O compile wall time on SWI 9.2.9, swa, medians of three runs against 248807c:

The 4000-link address analysis alone went from 5.14 s to 0.028 s; 16000 links now take 0.118 s. Assembly is byte-identical at each measured compile size. Peak process memory at 4000 links is still about 39 MiB.

Validation compared the complete address maps and escape classifications on 2086 functions: existing IR fixtures, 2000 seeded generated graphs, 20 shuffled 100-link chains and a directed conflict/cycle case. All matched the old analysis exactly. A deliberately broken copy that omitted the instruction-order tie-break differed on the first case, so the comparison detects that mistake. Trealla also produces the same assembly for the 1000-link compile. The full Nix check retains the semantic and GC-stress coverage.

Reproduce the compiler scaling input without a separate generator:

python3 - 4000 > chain.ir <<'PY'
import sys
n = int(sys.argv[1])
ins = [f'let(tmp(t0), p, alloc(8), [const({n + 1})])']
ins += [f'let(tmp(t{i}), p, add, [tmp(t{i - 1}), const(1)])' for i in range(1, n + 1)]
ins += [f'store(b, const(42), tmp(t{n}))', f'let(tmp(result), w, load(ub), [tmp(t{n})])']
print('func(chain, export, w, [], [block(start, [], [')
print(',\n'.join(ins))
print('], ret(tmp(result)))]).')
PY
/usr/bin/time -f '%e s, %M KiB' bin/nanofil -O compile chain.ir > chain.s

Nonescaping local storage

After promotion and copy elimination, local_storage.pl selects constant entry allocations whose address chains have only fixed-offset memory uses. Unlike promotion, overlapping accesses and mixed pointer/scalar contents are allowed. Selection requires strict SSA and every access inside the original requested size. It excludes returns-twice functions, dynamic or nonentry allocations, unknown uses, float loads not described by escape's slot vocabulary, and objects beyond a conservative 4096-byte per-function payload/aux budget (including header/root/alignment costs). All unsupported objects keep their heap representation.

The grammar makes object provenance explicit without exposing a native stack address as a pointer:

local_alloc(Name, Size)
local_load(tmp(D), K, Type, Name, Offset)
local_store(Width, Value, Name, Offset)
let(tmp(Q), a, check_local(Name, Offset, Bytes, Rights, Align), [])

The last form is the checked-stage proof, immediately consumed by an existing raw access at offset zero. Pointer loads execute [aux_read, address_read]; pointer stores execute [lower_write, address_write]. The validator requires the local protocol only behind a local proof: heap barriers, ensure-aux, and box resolution do not apply to explicit local memory. Scalar stores leave aux unchanged. All bounds/alignment checks remain emitted, including constant checks.

The backend uses the pinned LocalExplicit protocol. Each object has a zeroed 16-aligned payload and separate zeroed aux, both physically rounded to 16 bytes; an aux count header precedes its lower words. Logical bounds remain exactly Size, including the empty interval for a zero-sized object. frame(Plain, Roots, Aliases) carries local(Name,Size) and a distinct stack_aux(Name) root. Origins count these roots in the special suffix before setjmp slots. The native stack address is never an ordinary heap lower. A root starts null and is published only after the object's payload, aux and header are initialized. Storage is not reused and lives until the invocation leaves its Fil-C frame.

The interpreter allocates each local's identity at its declaration, with exact bounds but the replaced heap allocation's rounded reservation stride. Fresh invocation metadata, separate from temporaries, holds those identities. Exiting an invocation invalidates only its bound stack regions in the latest memory state; recursive caller locals and callee heap allocations/frees survive. Oracle reviewed the grammar, rooting protocol and this lazy per-invocation identity model before adoption.

tests/local_storage.pl checks selection, refinement, invalid proofs, recursion, repeated prepared executions and symbolic backtracking. tests/filc/local.ir runs 15 native/interpreter cases covering exact and zero bounds, negative/huge offsets, alignment, zeroing, capability forgery, recursive frames and heap effects across local cleanup. The optimized gc.ir case roots two pointees solely through local aux across forced collections and poll edges. A scratch mutant that nulls that root returns 6438275382588823896 instead of 46 under GC scribbling; the restored binary returns 46. This checks reachability, not just assembly shape.

Not done

• General symbolic memory validation. The bounded integer-return queries above still require concrete memory addresses.
• General C local OOB precision (the oobp gap in m4.md). Existing alloc means rounded heap bounds. Selecting an access into that padding would change its IR contract, so it is deliberately not selected; interpreter refinement has not been weakened. Dynamic offsets, local address values, lifetime markers and storage reuse remain outside this conservative subset.