Axiom 0.7.0

0.7.0 — 2026-09-03

A segfault the gate battery was structurally unable to see, the Rust
FFI's first lint gate of any kind, and a front page that stopped being a
reference manual. Four of this release's findings were stale artifacts
sitting behind a CI failure that stopped the run at gate 20 of 70 — each
found by fixing the gate in front of it.

A lambda's parameters were typed by the function around it, and an Int was retained as a pointer

(:: g (-> String Int Int))
(fn (g s k) (let ((f (lambda (a b) (+ a b)))) (+ k (f 999999999 2))))

exited 139. Change g's signature to (-> Int Int Int) and the same
lambda prints 1000000002. Codegen keeps the parameter NAMES it is
emitting in word 17 and the declaration whose signature TYPES them in
word 36; emitLamDef set the first to the lambda's parameters and left
the second on the enclosing declaration, so curParamRefClass typed the
lambda's a as g's String, set the closure record's map bit for it,
and emitted axiom_retain on the integer. The parser curries
(lambda (a b) ..), so every multi-parameter lambda took the path,
and the classification was wrong whenever the enclosing arrow disagreed
at that index. Below 4096 the runtime's immediate guard swallows it.

Fixed with pairSlot 7, set while a lifted lambda's body is emitted and
read by the two classifiers that lacked the identity check their three
siblings (paramFlowBit, paramIsString, paramClassOf) already made.
A flag rather than their name comparison, because a lambda shadowing the
function's parameters with the same arity and spelling passes that test
and is still a different binding — term 5 of the fixture.

The compiler's own source never took the path, and that is measured:
compiling the identical self_host/main.ax with the pre-fix and post-fix
compilers gives byte-identical IR, 8,729,830 bytes. So no gate, no
self-host fixpoint and no bootstrap could have gone red on it. It is the
zero-population region the 2026-08-10 corpus survey named FIRST
("multi-parameter lambda, 0 of 97 lambdas"), producing its second bug
after the first was fixed. Gate: tests/stdlib/472-lambda-param-class.ax,
five terms, exit 139 on the pre-fix compiler having printed nothing.

A Map you cannot enumerate is not a Map, and an Option nothing reads is not a type

mapKeyAt, mapValAt and mapStateAt were all private, so the public
surface offered mapLen and mapCap — a loop bound with nothing to read
inside it — and no caller outside stdlib/Map.ax could name a table's
contents. The evidence it was felt is in the module: mapSumKeys and
mapSumVals exist, and their comment says the two sums "pin down a small
map's contents well enough to test with".

Added: mapLiveFrom (a cursor answering (Option Int)), mapKeys and
mapValues (sharing one traversal and one slot order, so they zip), with
mapKeyAt/mapValAt made pub. mapStateAt stays private — tombstones
are an artifact of how delete keeps linear probing terminating.

Separately, fourteen public functions across Str, Vec, Intern,
Utf8 and Path answer an (Option a) and the standard library shipped
zero ways to read one. isSome, isNone, optUnwrapOr, optMap,
optAndThen and optOr join Err.ax beside okOr and toOption.

check-agent-policy.sh then contradicted a sentence in the new module
comment claiming the cursor is allocation-free: mapLiveFrom is charged
Alloc because Some is a heap block — call i64 @axiom_alloc(i64 16)
per live slot, read out of the emitted IR. The comment now says so. The
gate was right.

Gates: 107 stdlib tests; check-stdlib-api.sh with both floors
re-derived — the name sweep 400 → 700 against a measured 749 (three
hundred and forty-nine names could have been deleted with it green), and
the documentation ratchet 290 → 560.

The Rust workspace had no lint gate at all, and the freestanding runtime read a failed syscall as a short write

CI ran cargo test and nothing else over ~9,500 lines of hand-written
Rust, most of it unsafe. Moving to edition 2024 (for
unsafe_op_in_unsafe_fn, a hard error there — 116 unmarked operations)
with a declared MSRV of 1.85 and a [workspace.lints] policy then
found, and this release fixes: 33 unsafe blocks with no // SAFETY:
line, 36 undocumented public items, 7 missing_safety_doc, and six libc
shims declaring *mut u8 where the ABI is *mut c_void.

Every boundary handle was Send + Sync — AxStr, AxVec,
AxFn1/2/3 and the owning AxString — while axiom_retain is a plain
load-add-store. A NotThreadSafe marker fixes it at zero representation
cost; four compile_fail doctests hold it, and weakening the marker
makes all four report "compiled successfully, but it's marked
compile_fail".

And a real bug in nostd_runtime.rs, behind a feature no member
enables and which therefore did not compile under edition 2024 at all:
both Darwin call3 implementations were missing the b.cc/jnc
branch-and-negate that targetSyscallAsm emits. A BSD kernel signals
failure through the carry flag with a POSITIVE errno, so a write
failing with EBADF came back as 9 and write_stderr's if n <= 0
read it as nine bytes written. Verified by reading the emitted assembly
for both targets (b.lo/jae are the assembler's spellings).

self_host/rustbind.ax emits unsafe extern "C" now, because edition
2024 refuses the bare form and a generator writes into somebody else's
crate. Gate: check-ffi.sh runs clippy -D warnings and cargo fmt --check over three surfaces — the workspace, --features host, and
--features nostd-runtime — because the workspace sweep reaches neither
feature, and each hid a finding.

The front door was a reference manual: README 75,806 bytes to 7,587

Two thirds of it was ## Implementation Status, whose rows average 1,195
characters. That, the type table, the CLI list and the diagnostics
showcase moved verbatim to docs/status.md; ### Targets stayed,
being the one copy of the supported-target list and of the sentence that
defines supported. Five gate readers were repointed in the same commit,
and two of them caught the move doing damage: check-release-targets
refused the condensed Targets section for dropping the darwin-x86_64
exception, and check-version refused a README with no version banner.

check-doc-drift.sh gained a claim — the compiler's own line count, now
recomputed in every prose document that states it — and lost a blind
spot: claim() strips a thousands separator before comparing, so
97,017 and 97017 are the same claim where the readable spelling used
to be invisible.

Three goldens had decayed while the gate ahead of them was red

26df546's CI died at gate 20 of 70, so gates 21-70 never ran on it.
Behind the failure sat three stale artifacts, each found by fixing the
one in front: tests/fmt/corpus-fmt.golden at 64 unpinned files against
a ceiling of 60; the three symbols-zoo goldens 62 rows short because
Platform.darwin.ax gained an (import Err) and symbols lists a
transitive closure; and tests/agent/stdlib-effects.allow recording
which HOST blessed it — both linux legs failed on a two-line diff that
was only a file name, Platform.darwin.ax against
Platform.linux-aarch64.ax, with the effect identical. The derived set
now collapses Platform.<host>.ax to Platform.ax.

Also check-net.sh moved to the serial set: it serves 20,400 real HTTP
requests and asserts every byte returns, which under six-way parallelism
reported "echoed 5983 of 10000" and passed alone immediately after. The
header's own rule — the tell is the RATIO, not the clock.

ERR-ADOPT-1: the failure column reaches zero, and the question it waited on is answered

compat/SENTINELS reads 3 absence + 0 failure (from 7 + 9). The
nine failure rows waited on one question — may println's effect row
widen? — and it is answered with a measurement rather than a
workaround. With sysWriteFd ported alone, the row widens from IO to
Alloc,IO on 11 functions in the compiler's whole closure, six of
them public (sysWriteFd, sysWriteAllFd, writeStr, printLit,
printlnLit, rpcPut), and zero restrict(no-alloc) claims are
refused: nothing in the tree claims to print without allocating. What
widens the row is the failure path — a failed write builds an
Error through sysResult — and the success path builds nothing,
because sysWriteAllFd matches the call directly and reads two
registers. That is what the 2026-08-30 attempt could not say, when an
(Ok n) block per write turned ten gates red. So println's row
may widen, because println can allocate, and only when a write
fails.

Ported to (Result Int Error): sysWriteFd, sysReadFd, netAccept,
netAcceptFrom, netPollWait, sysNowMicros, sysNowMonotonic, and
the seam under the first two, platformWriteFd and platformReadFd
in all five Sys/Platform.*.ax (the four ENOSYS stubs lose their
pure tag, because an Err is built; Windows answers Ok 0 at end
of file as before). sysWriteAllFd and writeStr keep their Int
channel — println's value is that Int in 804 expansions — and
sysWriteAllFd holds its match in a let so the partial-write
recursion keeps its loop. The compiler's own stderr writes, Tui's
flush and the echo server's reply go through sysWriteAllFd now,
which retries a short write where they used to drop it. Every reader
matches the call directly (keyInFill, Http, Rpc, the REPL), so
no bytes-arrived path builds a block. The alternative measured and not
taken — a private raw twin under sysWriteAllFd to keep println at
IO exactly — was defeated by the seam: platformWriteFd builds the
same Error on its own failure path, so the row widens through it
either way. Every widened public row is declared in compat/BREAKING
under 0.6.4; docs/error-model.md §10.1 carries the decision and the
alternative.

ERR-ADOPT-1: the absence rows no-alloc held back are Option, claims intact

strHexVal, utf8DecodeAt and utf8CharAt answer (Option Int) and
KEEP restrict(no-io,no-alloc,no-foreign): each is the pair shape, so
its body builds no block on any path and the claim is checked against
the emitted IR (scripts/check-unboxed-sums.sh section 6 holds the
self-compile's rows to their definitions). utf8CharAt forwards
utf8DecodeAt's two registers as they arrive. netPollSignalAt answers
(Option Int) too, and its row stays IO alone. Every caller matches
the call directly; the three that needed all of several digits before
answering (Json's \uXXXX, Http's and the LSP's percent-decoding)
got a private helper that nests the matches. compat/SENTINELS:
Utf8.ax 2 → 0, Str.ax 2 → 1, Sys.ax absence 1 → 0. What stays,
and why: strFindByte tail-calls itself, the one shape the pair
does not take yet, so a port would keep the boxed body and refuse its
own claim; keyStrEnd and keyInFill answer three outcomes each and
want a data of their own, which the pair refuses by name. The floor
is 3.

The seed learns the mirror

A reseed, because the ports above use restrict(no-alloc) on a
constructor-answering function and the committed seed's checker
refused exactly that — the seed-skew rule is land, reseed, then use.
bootstrap/CHAIN gains its row; the generator was the committed seed,
as scripts/reseed.sh requires.

The box is the caller's, and restrict(no-alloc) holds for an Option lookup

A function whose every tail is None or (Some e) no longer
allocates on any path, and the checker knows it. Until now the
register-pair specialisation of 0.6.3 emitted @F$pair BESIDE the
boxed @F, so the function genuinely could allocate — whichever
caller it got decided — and restrict(no-alloc) on strHexVal,
utf8DecodeAt, utf8CharAt, keyStrEnd and strFindByte was the
reason five absence sentinels could not become Option
(docs/unboxed-sums-design.md "not lifted", docs/error-model.md
§10). Three changes close it:

• The emitter writes the body once, as the pair. @F is a
  wrapper that calls it and boxes, kept only for a reference taken as
  a value. Every direct call calls the pair: a match reads the
  registers, a tail leaf of another pair function forwards them
  (utf8CharAt → utf8DecodeAt), and any other site boxes the pair
  in the caller's own definition — the same shape word, tag, count
  and field store a constructor writes. With nothing written twice,
  the "would be lifted twice" refusal is gone and the pair set on the
  compiler's own source grows from 8 functions to 24; a tail match the
  tail emitter could only lower boxed goes to the ordinary emitter
  instead, so every pairMatchOK match reads registers.
• The checker mirrors the eligibility test (tcPairFnOK and its
  neighbours in self_host/typecheck.ax) and charges Alloc where
  the block is built: not at a pair function's constructor leaves, at
  every call of a pair function that is not a matched direct call or a
  forwarding leaf, and at a pair function named as a value. Measured
  on the self-compile, internFind, pathLastSlash and
  scopeFindIdx lose Alloc from their rows; nothing gains an
  effect it did not already carry, so every compat movement is
  NARROWED.
• The two are held to one answer. scripts/check-unboxed-sums.sh
  gains section 5 — check accepts no-alloc on the lookup and on a
  caller that matches it, refuses it (AX3049) on a caller that
  let-binds the answer, and symbols and the IR say the same — and
  section 6, scripts/lib/alloc-rows.py over the whole self-compile:
  every function whose row lacks Alloc has a definition with no
  axiom_alloc (3,482 rows held, 0 disagreements). The mirror may
  over-charge and never under-charge; section 6 is what would notice
  the other direction.

tests/diagnostics/384-restrict-no-alloc-ctor.ax's some arm is
silent, and a new held arm — the same value stored past its match —
is the refusal that keeps the silence honest. What is not here: a
self-tail-recursive function still keeps the boxed shape, a match in
tail position of a pair function is still not a pair tail, and a
third sum type is still refused by name — each a refusal with the
boxed path and Alloc charged as the fallback, never a wrong answer.
The ports the lift permits are the next commit's, after a reseed: the
committed seed's checker refuses the claims this one accepts, and the
seed-skew rule is land, reseed, then use.

Region-annotated signatures and the escape rule — stage S3 of the regions note

A signature may name the region a reference lives in, (:: intern (-> (String @s) (Table @r) (Sym @r))), and MM-RGN-3 of
memory-model-v2-design.md §2.3 is
checked over every body: a value may be stored into, returned into or
captured by a place only if its region outlives the place's. Four
errors — AX3060 a store, AX3061 a return, AX3062 a closure
(named against the capture), AX3063 arguments that disagree on a
region the callee names, or a result-only region — one fixture per
shape in tests/diagnostics/645–649, and restrict(no-escape) on
the restriction rail (refuted through the callee by name, unverifiable
over an unresolved call, AX3057 under strict).

An un-annotated callee is READ, not assumed. The checker computes
per function, as a fixpoint over the call graph like the effect row,
which parameters the body stores a fresh value into and which
parameters flow into which — vecPush stores its second into its
first and allocates into its first when it grows — so (vecPush v x)
is refused across regions and accepted within one with nothing written
on vecPush, and (strLen s) on a string from any region is legal.
§2.4's "region-monomorphic in the caller's current region", stated as
invariance, would have refused the second.

A program that never writes @ is untouched, measured two ways.
The pass is absent - not silent - when no signature names a region
(rgnCheckAll's first line), and the annotation lives in a spare word
of the type node that no reader of a type consults, so an annotated
program and its stripped twin emit byte-identical IR (1,652 lines,
tests/stdlib/468-region-signatures.ax). The type checker's own
functions that moved for the annotation: zero.

scripts/check-region-escape.sh holds all of it from the outside:
the byte-identity, the five refusals by code and name, an ABLATED
compiler (rgnCheckAll answering 0) that accepts 640–643 and then
runs tests/region/escape-store.ax — the program the rule exists to
refuse, which stores a string from a region into a cell that outlives
it, resets the arena, reuses the bytes and reads the cell back, and
must not print hello at exit 0 — and §5's two-region sweep as a
program (scripts/lib/region-sweep.py: 241 of 6,206 functions relate
two regions, 3.88%, inside the 3.5–5.2% the hand audit gave). fifty-six
gates call gate_build_axc now.

What S3 is not, stated in the note beside the staging table:
nothing allocates INTO a named region yet, so a value the body makes
cannot be stored into a @r place or answered as (T @r) — growing a
@r vector included — until S4 hands a callee a region; the witness
of §2.5 is deferred to S4 with its first reader, because a hidden
trailing word would change the IR of exactly the programs this stage
proves inert; and (region r ...), S2's form, is walked against its
contract but is another track's to parse and lower. The seed's parser
cannot read @r, so nothing in self_host/ or stdlib/ carries an
annotation: land, reseed, then use.

Also: @r in the formatter (fpType prints it, fpExpr refuses it)
and in the tree-sitter grammar (region_annotation, region_type; the
@ in OPERATOR_CHAR stays, because region_annotation is the longer
match wherever it is valid); AX3052's closed list gains no-escape,
which re-blessed tests/diagnostics/376.

A mutual tail call runs in constant stack at --opt 0, and a let body always was a tail position

(fn (ev i acc) (if (>= i n) acc (od (+ i 1) (+ acc 1)))) — ten
million alternating calls, --opt 0, a 512 KiB stack — answers.
Before, it died by SIGSEGV at --opt 0 and ran only because LLVM's
sibling-call pass happens to rescue it at --opt 1, which is what
docs/memory-model.md MM-EXEC-6c said and what a program MUST NOT
rely on. emitPlainCall now marks the call musttail, LLVM's
guaranteed tail call — llc lowers it to a jump at every level or
refuses the module — when every one of LLVM's conditions and this
compiler's holds (mustTailOK in self_host/codegen.ax is the list:
tail position with no leaf retain owed, a defined callee applied to
exactly its arity, a plain fn caller that is not a self-tail loop, no
let temporary pending, identical prototypes — the same i64 count,
evidence word included — and no owned temporary the caller releases
after the call). tests/stdlib/467-mutual-tail.ax pins six terms;
scripts/check-tail-calls.sh builds it at --opt 0, runs it under
512 KiB, and then deletes the marker from the same IR and requires
the program to die by signal, because the marker is the whole
mechanism and a fixture that survived without it would be measuring
the stack rather than the guarantee. On the compiler's own IR: 386
of the 1,059 calls sitting immediately before a ret are marked
(the gate holds a floor of 300).

What is NOT guaranteed, stated rather than implied. A callee of a
DIFFERENT arity stays a plain call — 603 of the compiler's own tail
calls — because LLVM requires identical prototypes for musttail
under the C convention. The tailcc convention lifts that, and it was
measured rather than assumed: llc -O0 accepts musttail between
tailcc functions of two and three parameters and emits a jump on all
seven triples, and the darwin binary runs ten million such calls under
512 KiB. It is not adopted here, because every function in the module
would change convention and the runtime's callback trampoline and
every extern boundary with it; MM-EXEC-6c records it as the measured
next step. A call handing over an OWNED TEMPORARY —
(od (+ i 1) (strConcat s "x")) — also stays plain, and must: the
caller releases the temporary after the callee returns, and releasing
it before the call would free a block the callee is about to read.
The gate holds both refusals, the second with its axiom_release
still following the call.

And a correction the measurement forced. docs/reference.md's
Optimisation section and scripts/check-stack-depth.sh's header both
said a tail call in a let body was not a tail position and needed
--opt 1. It has been one since 2026-08-22 (the comment under
tailCallsSelf); measured 2026-09-03, a self call through a let
body, a cond arm, a match arm and a { } tail each ran ten million
iterations at --opt 0. Both documents now say so, MM-EXEC-6b lists
every tail position and the three that are not, and the stack-depth
gate's header keeps its history in the past tense.

LTO was measured and deliberately not flagged. A program is one
LLVM module already, and the emitter prunes unreachable definitions
before opt sees it, so -Wl,-dead_strip recovers 10 runtime symbols
and 752 bytes on a hello world and 32 bytes on the compiler — not a
byte-layout change worth making on every target. Cross-language LTO
over extern is reachable and stays a documented next step: a crate's
--emit=llvm-bc links into the module with llvm-link and one
opt -O2 inlines the Rust function into the Axiom loop, once the
"target-cpu" attribute rustc stamps on it is stripped; a
-C linker-plugin-lto staticlib carries no bitcode member (0 of 393)
and cannot feed it. docs/reference.md's Optimisation section holds
the measurements; the C ABI (check-c-abi, check-ffi) is untouched.

The stack-depth gate reports 600 KiB with and without this change.
Its header and ci.yml quoted ~224 and ~216 KiB from August; the
number moved with the tree, not with musttail, and the gate's
ceiling of 1024 KiB still holds.

Automatic vectorisation: what opt already does to an Axiom loop, and the trap that sat inside it

Read-only loops vectorize today, at --opt 2. Measured 2026-09-03
with opt --pass-remarks-output on four fixtures (scripts/check-simd.sh
carries them): a for over a (Vec Int) that sums is vectorized at
width 2, interleave 4, and runs 3.1x faster than at --opt 1; a
byte scan over a String at width 16, 1.9x (best of five,
interleaved arms, load average 9). The driver's default --opt 1 runs
no vectorizer at all — LLVM enables the loop and SLP vectorizers at
speedup level 2 — and the default is unchanged, because on the
compiler's own IR opt -O2 costs 4.2 s against 2.9 s at -O1
(202,424 lines, three interleaved runs each, load average 7), which is
not nil. docs/reference.md's Optimisation section now says which
loop shapes vectorize and why the others do not, with the command that
shows it.

What does not vectorize, and why, in LLVM's own words. A map
through vecSet is refused four ways at once: the length, data
pointer and ownership flag are re-read every iteration because a
__store64 through an integer address may alias any of them; the
range check's trap was an EXIT inside the loop ("early exit loop with
writes"); the ownership branch keeps an axiom_release call in the
body ("call instruction cannot be vectorized"); and even with every
access tagged by hand so the header words hoist and the trap folds,
vecSet's silent out-of-range skip is a predicated store, which
baseline NEON and SSE2 have no masked-store instruction for, so the
cost model declines ("not beneficial"). An i64 multiply is not
native on either baseline either: the same map with * 3 is refused
on cost where + 1 is accepted. The Collatz while is refused
correctly — its trip count is data-dependent. LoopVersioningLICM
answers IllegalLoopStruct for the loop as emitted. None of this is
asserted; each row is a remark in the gate's YAML.

The emitter change: the six traps are noreturn cold.
__axiom_index_out_of_range and its five siblings end in an exit
syscall — or a recovery point's longjmp — and then unreachable, so
noreturn states a fact. Before the attribute, Vec$vecGet and every
accessor like it was inlined everywhere and carried the trap's body —
two syscalls and a @__axiom_backtrace call — with it: 1,518
inlined copies in the compiler's own IR at --opt 2, 1,685 at
--opt 1, one inside every hot function that indexes a vector. With
the callee cold the inliner leaves it a call, and with it noreturn the
block after the call is unreachable rather than an edge back into
the loop. 2 copies now at either level, the compiler binary
6.9% smaller (2,153,352 → 2,004,600 bytes; __TEXT 1,687,552 →
1,540,096, 8.7%), and three more of its loops vectorize (98 →
101: lsp$lspChSites, lsp$lspSignatureHelp, lsp$lspViewHintsCall).
nounwind was measured beside it and moved nothing, so it is not
there. Every fixture in tests/stdlib/ answers the same bytes; the
self-hosting fixpoint holds.

The gate. scripts/check-simd.sh holds behaviour across --opt 0,
1 and 2 first, then that the reduction and the byte scan are reported
Vectorized and carry <N x i64> and <N x i8> operations (the
width is the target's baseline, not pinned), that the Collatz loop is
not (the reader must be able to answer zero), that the trap is defined
noreturn cold and the in-place map's body holds no copy of it while
the module still calls it — with an ablation that blanks trapFnAttrs
in a copy of the tree, rebuilds, and requires the copies back — and a
census over self_host/main.ax with a ceiling of 2 copies and a
floor of 50 vectorized loops. the count of gates that do is stated once in this section, in the parallel entry below.
now, up from the previous count by this one.

What is NOT done, stated so nobody infers it. No aliasing fact is
asserted to LLVM: the header/element distinction that would let the
length hoist is true (docs/memory-model.md: a data block never
overlaps a header block) and was prototyped as scalar TBAA on the IR
by hand, and it is not enough on its own — the data pointer read sits
inside the range check's branch and LICM will not speculate a load
through an integer address, the ownership branch's release call
clobbers everything on its path, and the predicated store remains.
Making write loops vectorize needs three things together: the
attribute on the release runtime that says which words it touches,
the accessors reading the header before the check, and a vecSet
whose out-of-range answer is a fold rather than a skip; that is a
design note's worth of memory-model argument, not a flag.
inbounds/nsw were not added: no refusal named wrap.

parallel, and the thread lowering behind it

One construct, two lowerings. (parallel p ((a e1) (b e2)) body)
runs every binding's expression beside the caller and binds the
answers in the order written, whichever finished first —
MM-PAR-5's rule for the process pool, now a language form
(docs/memory-model-v2-design.md MM-RGN-7, S6 of its staging table).
The parser desugars it into lets over two primitives, __par_spawn
and __par_join, so no AST tag was added and no consumer of one moved
(self_host/parser.ax, parseParallelExpr); p is bound to the arena
mark of the region the form runs in, the witness §2.5 of the design
says a region carries.

Processes by default, threads on request. __par_spawn lowers to a
fork, one MAP_SHARED page per binding and a wait4 — the isolation
MM-PAR-3 makes true by construction, importing nothing — and, under
axiom build --threads, to the platform's pthread_create
(emitPrimPar and emitParRuntime in self_host/codegen.ax). That
is S5: cgThreads is a scan now rather than a constant false —
it answers 1 when the module names __thread_spawn, or names
__par_spawn under --threads, and the eight mutable globals of the
emitted runtime take thread_local(localexec) exactly then, so each
thread starts from the zeroed image and allocates in an arena of its
own (MM-PAR-6). Two more pairs name their lowering outright:
__thread_spawn/__thread_join and __proc_spawn/__proc_join. All
six carry IO, asserted primitive by primitive in
scripts/check-agent-policy.sh.

Measured, not argued:

• scripts/check-parallel.sh, new, builds tests/stdlib/470-parallel.ax
  (seven terms, twelve bindings at most) and 471-parallel-trap.ax
  under both lowerings and requires the same stdout and the same exit
  status — the trap fixture exits 77 out of both, because under
  processes the join reads the child's wait status and re-raises it
  and under threads the trap is already exit_group. The process
  lowering adds no import over a program that spawns nothing; the
  thread lowering adds exactly pthread_create, pthread_join and, on
  Darwin, __tlv_bootstrap. A program with no parallel built under
  --threads is byte-identical to the same program without it.
• scripts/check-thread-local.sh reaches the ON path through a
  program that really spawns a thread, where before it could only
  ablate cgThreads's body; the eight-globals-and-nothing-else
  assertion, the OFF path's zero TLS imports and the local-exec
  assertions are unchanged.
• The targets that cannot: --threads on freebsd-* or windows-x86_64,
  and __thread_spawn there, are refused at build time as AX4006
  (self_host/main.ax, before any IR is written; freebsd links no
  libthr here and is unmeasured, windows has no fork either). On
  windows-x86_64 both primitives compile to a trap that says
  axiom: parallel is not available on this target and exits 79,
  so every cross-target sweep still emits and assembles the fixture;
  a spawn the kernel refuses is 78 everywhere. Both join the
  status table in docs/memory-model.md.
• tests/diagnostics/640-parallel-shape (mut on a binding is
  AX2001) and 641-parallel-word (a String binding is AX3004 at
  the expression). tests/fmt/parity/200-parallel-layout and
  201-parallel-arg-position pin the formatter's layout and the rule
  that parallel off the head is an identifier; the tree-sitter grammar
  has parallel_expression and parallel_binding, and its corpus a
  case for both.

What crosses a join is a word, and that is the stated limit. The
thunk is (-> Int Int): under processes the answer crosses an address
space through one page, and under threads it would have to be promoted
out of the child's arena, which is the typed promotion S3/S4 own. The
thread lowering does not yet check what a binding captures — a heap
value shared with the parent is touched from two threads with no
fence; the static rule that refuses it is MM-RGN-3 over sibling
regions (§3.2 of the design), and until it lands processes are the
default for exactly this reason. Nothing in self_host/ or stdlib/
uses parallel yet: the committed seed cannot parse it, and the rule
is land, reseed, then use. sixty gates call gate_build_axc now.

region returns as a checked scope — S2 of the memory-model v2 design

(region r body) is a keyword again. It reads the allocator's
waterline when body starts and rolls it back when body ends —
MM-RGN-1 over the runtime MM-ALLOC-15/16 already specify — and
answers body's value. docs/memory-model-v2-design.md §4's S2 row
asked for exactly this: mark/reset, names scope-checked, and AX2004's
false advice deleted. region had been refused on the strength of an
inference that was withdrawn the same month (§1.4), and the advice —
"lifetimes are inferred" — outlived the model it described in the
parser, in explain AX2004, in README and in reference.md. All four
say the true thing now, and a region at the top level reports
AX3027 like any other expression head; the fixture that pinned the
refusal, tests/diagnostics/940-removed-region, is deleted with it. Measured before the change:
(region r 0) in expression position drew AX3001 undefined variable region, because the AX2004 arm only ever fired at the top level.

The mark cell is a stack slot, not the heap cell a hand-written mark
allocates. __axiom_arena_mark takes its 24 bytes from axiom_alloc
below the waterline it then records, so it is never reclaimed, and a
mark per loop iteration leaks a cell per iteration into the arena it
means to keep flat. emitRegion loads the three words the mark
function reads into one hoisted alloca per region form and hands that
to the unchanged @__axiom_arena_reset_fn, so MM-ALLOC-16a's
status-75 walk and 16b's status-76 evidence check run as they run
for a hand-written mark. 2,000 regions of 64 KiB each leave the
waterline where it was (tests/stdlib/168-region.ax, terms 2 and 3),
and a region inside a live handle's extent still dispatches after
its reset (term 8).

Checked, with no types yet — and the two refusals say exactly what a
scope check can see. AX3059 region-escape: the region's own value
must be a scalar (Int, Bool, Char, Float, Unit), because it
is handed past the reset by value and a String is a descriptor over
a second block; and a set inside the region on a binding bound
outside it must store a scalar, (set x.f v) included
(tests/diagnostics/631-region-escape.ax: three rows, and three silent
shapes beside them written with the same strConcat). AX3058 region-name-shadowed: a nested region may not reuse an open name,
because MM-RGN-2 orders regions by nesting and a name meaning two
extents cannot be ordered (630; siblings may share one). The node is
real — TAG_E_REGION, the name's span in its third word — rather than
a for-style desugaring, because S3's escape rule has to FIND region
extents; the checker keeps the stack of open regions S3's @r will
resolve against, and a macro template's own region name is gensymed
like a let binder's.

What it does not see is written down, not implied. A call that
stores a region-allocated reference for you and a raw Int that is an
address are MM-ALLOC-16's program obligation, as for a hand-written
mark; S3 is what closes them. A region contributes Alloc — the
primitives' row — so a restrict(no-alloc) body cannot hold one.

Byte-identical for everyone else. A program that writes no
region reaches none of this: the compiler built from the commit
before and the compiler built from this one emit the same 202,021
lines for self_host/main.ax, byte for byte, and the same IR for
tests/stdlib/165-arena-keep.ax. That is MM-RGN-4's
one-region-instance claim, measured.

scripts/check-region-scope.sh holds four things: a no-region
program emits no region cell and a two-region program emits exactly
two; 4,000 iterations of a region allocating and filling 64 KiB,
against the same body with the word deleted, is 185x on
peak RSS; 631 and 630 draw exactly their rows; and the ABLATION — a
compiler rebuilt with rgTyScalar answering 1 for every type accepts
the refused store, and hello world written into an outer binding
from inside a region reads back as XXXXXXXXXXX, the string built after
it, because the waterline was rolled back to exactly where the region
began and the next descriptor landed on the old one. It calls
gate_build_axc, and the count of gates that do is stated once in
this section, in the parallel entry above.

Around the keyword: axiom fmt prints it as while is printed and
refuses a second body (tests/fmt/parity/210, 211; the bank is 50
cases, 25 rewrites and 25 refusals); the tree-sitter grammar has a
region_expression and region left removed_keyword
(tree-sitter-axiom/test/corpus/expressions.txt, removed.txt); the
LSP offers the keyword and treats its name as a binder in a fix;
explain AX3058 and AX3059 answer. region is an ordinary
identifier off the head of a form (168, term 10).

Seed skew, and what therefore does not use it yet. The committed
seed cannot parse region, so nothing in self_host/ or stdlib/
writes one — land, reseed, then use. The compiler's own per-line
checkModule reset and the pre-forked server's per-request mark are
the first two candidates once a reseed lands.

for is a keyword, and it has two shapes

(for i lo hi body) counts [lo, hi); (for x xs body) binds x
to each element of a (Vec a). One keyword, told apart by ARITY —
three operands after the binder is the range, two is the container —
because a parser knows no types and arity is the only discriminator it
has. That forces exactly ONE body expression: a variadic body would
make (for x xs a b) ambiguous with the range, so { ... } sequences
several, and a fifth element is AX2001 naming both shapes
(tests/diagnostics/625-for-shape). Both shapes answer 0, as while
does. tests/stdlib/466-for-loop.ax pins twelve terms and its header
says what each establishes; docs/reference.md documents both shapes
in a section of their own under Let Bindings.

A keyword and not a macro, and stdlib/Pre.ax's range header
recorded why before this existed. An expression macro has exactly one
shape (MAC-LANG-14 — the rule form's templates are declarations), and
for needs two. Measured then, they could not even coexist as two
macros: Html.ax exported its own (for x xs body), and a program
importing it beside a range for resolved to Html's and answered
AX3001: undefined variable i in the body rather than an ambiguity at
the import. The container half additionally needed an ELEMENT type,
which is docs/generics-design.md §5 item 6 waiting on item 5 — and
item 5 landed in the entry below this one.

Desugared in the parser into nodes that already exist —
parseForExpr in self_host/parser.ax emits let/while/set —
so no AST tag was added and expand.ax, typecheck.ax, codegen.ax
and lsp.ax did not move. The IR a for emits is by construction the
hand-written loop's: measured on a range over println against the
let/while/set it stands for, byte-identical at 1,196 lines.
Both ends are bound BEFORE the loop — the range's lo and hi, the
container and its length — so a body that pushes onto the very vector
the bound came from still runs its entry count (466 terms 4 and 5; the
while shape this replaces re-reads (vecLen xs) every iteration and
runs until memory is gone).

Hygiene without a renamer. The desugaring binds for$lo, for$n,
for$i and for$v, and $ is AX1001 unexpected character inside an
identifier, so a user cannot write or capture them — 466 term 6 binds a
caller's own i, n and v around both shapes and prints them after.
The element read is the MANGLED Vec$vecGet/Vec$vecLen, the spelling
mangledFromChain gives Vec::vecGet, for the reason MAC-CAP-10.5
records: a bare vecLen in a generated body IS captured by an entry
file's own function of that name. Term 12 and
tests/diagnostics/626-for-not-a-container both declare a vecLen
answering 99, and the loop runs twice. A tree with no path to Vec at
all gets AX3001 undefined variable Vec::vecLen at the for, which is
a diagnostic rather than a silence.

A non-container is refused at the USER's expression. (for x n body) over an Int underlines n, not the word for: AX3004 expected Vec _a, found Int, two rows per site because the desugaring
reads the container twice and the checker does not poison a binding
after one bad use. The second row deliberately carries the keyword's
span — measured, two rows with the same message at the same span read
as a compiler bug rather than as two uses (626, four rows).

stdlib/Html.ax's for and forInt macros, and the three helpers
hVecLen, hVecStr and hVecWord that existed only to SPELL their
element reads, are deleted, and not one call site moved: a keyword
head wins over a macro of the same name with no diagnostic at all
(measured — (macro (for a b c d) 42) then (for k 0 2 0) answers
0), and the rendered bytes of tests/stdlib/420-html-render.ax are
unchanged, forInt over Ints now reading for over Ints with the
same <ol>. examples/web/server.ax's (for it items ...) is
untouched. compat/BREAKING declares five removals under 0.6.4: the
three hVec* rows now say REMOVED rather than retyped, and the two
macros have rows of their own — AXSYM emits a macro as kind M, 114
of them in the 0.5.0 baseline, so a deleted macro is a break the gate
sees rather than one it has to be told about.

showResolve read a placeholder instead of resolving it, and the
container loop is what exposed it. An un-annotated let over a
container binds its element to a fresh var that pinning later BINDS
(scripts/check-type-pinning.sh); the show lowering read the
placeholder itself, saw TAG_T_VAR, and answered AX3025 its type is a type variable about a type that was not a variable any more —
measured, (strLen y) type-checked and (println y) on the SAME
binding one line above was refused. It resolves first now
(tyResolve, which walks BOUND placeholders only, so an unbound var
still reaches every refusal in tests/diagnostics/620-show-refusals).
Inert on the tree: axiom emit-llvm self_host/main.ax byte-identical at
202,021 lines, zero diagnostic movement over 256 corpus files. 466
term 7 is the fixture — (println s) directly on a (Vec String)'s
element.

The formatter is a separate grammar and had to learn the head.
Before fpFor, a four-operand unknown head with a { } body printed
as the APPLICATION layout — idempotent, re-checkable, and wrong for
every for in the tree. It prints like while now, the head line
carrying everything the loop is controlled by and the one body indented
under it (tests/fmt/parity/198-for-head-layout.axp), and for in
parameter, binder, pattern and argument position prints as the
identifier it is (199-for-arg-position.axp). The parity bank is 50
cases, 26 rewrites and 24 refusals, up from 48; regenerating it moved
no other case's bytes. tests/fmt/syntax-zoo.ax carries both shapes.

Tree-sitter gains for_expression — binder, two operands and an
optional third, which is how one rule covers both shapes — and a
@keyword.repeat group holding while and for, while having been
missing from highlights.scm until the group existed. The corpus pins
a range nested over a container. check-tree-sitter parses every .ax
in the tree with it.

What is NOT done, stated rather than implied. self_host/ and
stdlib/ do not USE for. The compiler's own sources are built by the
committed seed, which does not know the keyword, and scripts/reseed.sh
states the order: land the construct, reseed, THEN use it. So range
stays in the prelude — its template is what the keyword's range shape
mirrors, binding for binding — and self_host/symbols.ax still spells
its one loop with it. The reseed and the migration of the hand-written
while loops (about a hundred, per range's header) are the next
commits, not this one.

Vec carries its element type, and the port is landed

stdlib/Vec.ax handed out a bare Int handle. It hands out a
parameterised (Vec a) now, and the 4,432 errors that produced
across the tree are at zero: stdlib/, every REPL module and the
whole closure of self_host/main.ax typecheck clean, and
check-stdlib-selfhost runs the tests/stdlib/ corpus against its
goldens. The self-hosting fixpoint holds — stage2 and stage3 are
byte-identical at 201,920 lines of emitted IR, which is the
acceptance test that mattered.

How it closed is the part worth recording. The mechanical driver
reached 181 errors over 130 declarations and stopped, and not for
want of a rule: docs/generics-design.md §4c measures four experiments
and a whole-chain inferencer against that wall, and the inferencer's
own verdict is that the source has erased the distinction at those
positions — it decides 417 of them and then merges 8,866 into one
class, because vecAppendFrom : (-> (Vec a) ...) is a declaration
every vector in the program passes through. Three readers then decided
the 130 element types from the code and three fixers applied them.
Automation was worth 4,432 → 181; people were worth 181 → 0.

New typed accessors, because some of this compiler's vectors are
heterogeneous by construction — pruneMark's ctx holds an interner
in slot 0 and vectors in 1..3, so no element type describes it and the
ACCESS is what needs a type. Reading: vecGetVec, and memGetWordVec
/ nodeAVec / nodeBVec / nodeCVec for a raw word read back as a
container. Writing: vecPushStr and vecPushVec. (vecGetStr already
existed; it was retyped, not added.)

vecPushStr takes its share EXPLICITLY, and that is a memory-model
requirement rather than a style choice. The obvious alternative is a
cast at the call site — and it type-checks and is a use-after-free:

(vecPush v (cast Int s))     type-checks, LEAKS THE RETAIN

vecPush's element parameter is a type VARIABLE, and
docs/memory-model.md MM-VAL-22 measures that a cast at an argument
root in a type-variable position classifies that value's evidence 0 —
so memSetWord's __retainref emits nothing and the String's share
is never taken. The accessor pairs the cast with the retain, so the
count matches a (Vec String) push. The widest shape this covered was
44 vecPush sites whose element is a String.

vecPop refuses an empty vector (status 77, through
__indexTrap), where it used to answer 0. (-> (Vec a) a) forces
it: an a cannot be fabricated, and for a reference element the old
0 was a null the caller dereferenced. vecLast inherits the trap by
delegating to vecGet. This is the port's one BEHAVIOUR break as
opposed to a retype.

The IR is NOT byte-identical to the pre-port tree, and that is the
ARC system working rather than a regression. 200,155 lines before,
201,920 after, with __evw on 157 define lines, up from 36.
Typing these containers is what created genuinely polymorphic
parameters, and a genuinely polymorphic parameter carries an evidence
word so ARC can decide at run time whether it holds a reference.
docs/generics-design.md §3 proposed byte-identical IR as the
acceptance test on the reasoning that (Vec a) and Int share a
representation; the representation claim holds and the conclusion did
not, and §3 is corrected rather than met.

Breaks declared: compat/BREAKING, 0.6.4 — 39 the census sees
(35 functions and 4 structs whose fields held vectors), plus eleven
Tui names it cannot, because Tui/Edit and Tui/Term postdate the
compat/0.5.0.axsym baseline and so read as ADDED, while a consumer
making the only available hop, v0.6.3 → 0.6.4, breaks on them.
check-compat.sh reports every breaking difference declared.

The Vec port's measure was wrong, and the searches were reading it now

With pinning in the tree and the full rule set, the port goes 4,432
errors to 210, and stops. Four more rules and three accessors took it
from 370 to 210, and each is design rather than heuristic:

• vecGetVec (-> (Vec a) Int (Vec b)), cast at the return. Some
  of this compiler's vectors are HETEROGENEOUS by construction —
  pruneMark's ctx holds an interner in slot 0 and vectors in 1..3 —
  so no element type describes them and the READ is what needs a type.
• vecPushStr / vecPushVec, and MM-VAL-22 is why they exist
  rather than a call-site cast. (vecPush r (cast Int s)) type-checks
  and is a use-after-free: the element parameter is a type variable, a
  cast at an argument root classifies the evidence 0, and
  memSetWord's __retainref emits nothing. The accessor takes the
  share EXPLICITLY and pairs it with the cast — one retain, exactly the
  one the cast suppressed.
• the let-init typed view, fixing at the binding rather than at
  each use (1,531 → 1,068 alone).
• discarding a container result: vecPush answers the handle, so
  (if c 0 (vecPush ...)) has two types where it had one.

The wall has a name, and part of it was the measure. The port
needs a declaration and its callers to change together, so a correct
coupled change RAISES the error count — typing
parseNamedFieldTypes's names as (Vec String) is right and reddens
every call site. Every search above accepted a move only when errors
dropped, so every one of them rejected the correct move.

The monotone measure is how many DECLARATIONS the errors touch:
fixing one removes it and adds only the callers that were always going
to need fixing. Switching the objective, and fanning the trials across
eight workers, moved a search stuck at 210 for hours to
149 declarations / 202 errors → 130 / 181.

A second bug was hiding inside the first: a trial's rollback restored
the FILE it edited and not the tree, while the convergence pass it ran
had rewritten dozens of others — so a round that kept two moves came
out 37 declarations WORSE and read as evidence against the method. It
was evidence about the harness.

The plateau is still real at 130 declarations. The search now takes
one move a round, which closes the port in about a hundred rounds and
is not a plan. The limit is the candidates: they come from positions an
error already names, and a coupled fix needs the positions that have no
error yet. That is the whole-chain inference this keeps arriving at —
which now has a measure to optimise that will not reject its answers. docs/generics-design.md §4c records the rules and
the plateau; the highest-value one was the let-init typed view
((let ((v (nodeB t))) ... (vecLen v)) fixes at the BINDING, not at
every use), worth 1,531 → 1,068 on its own.

Four experiments say the plateau is structural rather than a missing
rule. A clean restart with every rule available lands at 370, the
incremental run at 354. Applying every candidate at once goes to
5,611. Applying only the positions every error AGREES about — 183 of
them — goes to 5,462. One at a time with a convergence lookahead,
serial or across eight workers, buys about two errors a round.

The residue is 181 errors over 130 declarations, each a decision
about what a particular vector holds, and the decisions are COUPLED:
typing parseNamedFieldTypes's names as (Vec String) raises the
count until every caller moves with it, so one-at-a-time verification
rejects it and bulk application — which moves the wrong ones too — is
worse still.

A cast is not the way out, and the memory model says why: the
widest shape is 44 vecPush sites whose element is a String in a
vector the port typed (Vec Int), and vecPush's element parameter
is a type VARIABLE, so MM-VAL-22 applies — a cast at an argument root
there classifies the evidence 0 and suppresses the retain. The
String's share would never be taken. The element type is the fix.

What would finish it is element-type inference over declaration
positions: a union-find whose nodes are parameters, results and
fields, seeded by the certain sites and propagated through calls —
the same shape as pinning, one level up. That inferencer was built,
and the entry above records what it was worth: 417 positions from the
source alone, then one class of 8,866. The port is landed; the last
130 declarations were decided by people.

A bound type placeholder now stays bound

tyCompat COMPARED types and recorded nothing. A minted placeholder
matched anything and went on matching anything, which is a sound
under-approximation for a value read once and unsound for one that is
BOUND and then used twice — which is exactly what a container is:

(let ((v vecNew))
  { (vecPush v 42) (needVec (vecGet v 0)) })

Each vecPush matched its OWN fresh placeholder, the let's was never
pinned, and check answered OK for a program that exits 139 — an Int
read back as a block header with no cast written anywhere. That is
AX3040's own failure reached without AX3040's coercion.

A placeholder from INSTANTIATION now binds. Word 2 of a
TAG_T_VAR node is 0 until something pins it; parser.ax documents
that tag as a=name and every consumer dispatches on the tag and reads
only the name, so the slot aliases nothing. tyCompat resolves both
sides before dispatching and tyVarCompat pins instead of matching.

FOUR OBLIGATIONS, each a rule in the code rather than a hope:

1. Only an instantiation placeholder binds. freshTVar mints for
   two jobs. Instantiating a declared signature mints "the type the
   caller chose for a here", and two uses of one binding must agree.
   Every other use — a cond with no arms yet, a pattern binder, a
   missing parameter type — mints "not known", and pinning THAT reports
   an error where the checker has no information. Separated by name:
   _iN binds, _tN does not, and mkSilentWild never does.
2. Nothing binds to poison, or one error would cascade instead of
   stopping.
3. The occurs check is not optional — a cycle would be followed
   forever by tyResolve and by the reference-map walk.
4. There is no backtracking, so binding is monotone only because
   no caller speculates. All 53 tyCompat call sites were read.

Nearly inert on the tree as it stands, which is what made it safe
to land ahead of the port: 47 of 4,434 signatures mention a source type
variable at all, so almost nothing is instantiated. Byte-identical
fixpoint from the seed; check-self-host 179/179, check-diagnostics
194/194, check-stdlib-selfhost — no gate moved.

Diagnostics now render what a placeholder was pinned TO. The first
build reported expected _a, found String; tyRenderIn and
tyVarsInto resolve first, so it reads expected Int, found String.

scripts/check-type-pinning.sh, 5 checks, in two halves — a checker
that refused everything would pass the first. The unsound shapes are
refused (both were ACCEPTED before, measured), and the correct ones are
still accepted, including two containers pinned to DIFFERENT element
types in one scope, which is what separates this from a global
substitution. Not asserted, deliberately: that an UNDECLARED function
may be used at two types. It may not, and it could not before pinning
either — that is a pre-existing rule about inference without
generalisation, and recording it here would be a false attribution.

The Vec migration's premise only half holds, and it blocks the port

(Vec a) exists to stop a caller putting an Int in and taking a
String out. Measured against a migrated Vec.ax, it does that
exactly where a declaration names the element type, and nowhere
else — and the second half is the shape AX3040 was promoted to an
error for.

the program	check	runs
push a String into a declared (Vec Int) parameter	refused	—
pass a (Vec Int) where (Vec String) is declared	refused	—
read an element through a declared return type at the wrong type	refused	—
(let ((v vecNew)) { (vecPush v 42) (needVec (vecGet v 0)) })	OK	exit 139

The last row contains no cast at all: an Int goes in, a
(Vec Int) comes out, and vecLen dereferences 42 as a block header.

The cause is that the checker does not unify. tyCompat is a
COMPATIBILITY PREDICATE — it answers 1 or 0 and records nothing — and a
minted placeholder "still matches anything". With no binding written
down, (Vec _a) is compatible with (Vec Int) and then just as
happily with (Vec String), because each vecPush matches its own
fresh placeholder rather than the one in the let. It is not a general
unifier defect, which narrows the fix: (Box a) and (-> a a) both
behave, because a constructor hands over a concrete type and nothing
has to be remembered. The hole needs a placeholder that OUTLIVES the
expression that could have pinned it — which is what a let-bound
mutable container is, and why Vec is where it bites.

So the migration is BLOCKED rather than merely expensive, and
docs/generics-design.md §5 now puts pinning ahead of it. Landing the
port first would trade a visible unsafety for a silent one: today
reading an element back at a reference type is spelled vecGetStr or
an explicit cast, and #raw/AXSYM can enumerate the unsafe layer,
whereas afterwards (vecGet v 0) would quietly become whatever the
context asked for. §2's narrowing of AX3040 stays right and its
argument is completed in place: "an empty container holds no value of
type a" is true at construction and stops being the whole story one
line later, when the caller mutates at the type it chose.

No code changed. §4d records the four probes; nothing is in the tree.

A Vec field silently unmapped the record that held it

fldClass had no arm for Vec, so a record holding one leaked its
OTHER fields. The classifier answers 0 (machine scalar), 2
(reference) or 1 (UNCLASSIFIABLE), and 1 does not mean "skip this
field" — it forces the whole block to the LEAF shape. Vec reached
that arm the day it became a writable type: not a scalar name, not one
of the String/Option/Handle trio, and, being seeded by the
checker rather than declared, not in the module's data list either.

Measured on one record, one field type apart:

the record	shape word	the String field
(data Rec (MkRec Int String))	262152	walked
(data Rec (MkRec (Vec Int) String))	8	never walked

262152 is 0x40008 — bit 18 names block word 2, the String. At
8 the map is empty and the sibling's share is never handed back. No
diagnostic, every gate green, reachable from ordinary source.

Vec is class 0, and that is an ownership decision.
stdlib/Vec.ax says "a vector is born owned ... and vecFree is the
only thing that ends one", so a record that merely HOLDS a vector must
not release it — and class 0 is exactly what such a field got while it
was spelled Int, which is what keeps typing the handle free of
reclamation consequences. Class 2 is the other defensible answer and is
a SEPARATE decision: an automatic release beside an explicit vecFree
is a double free, so it would have to audit every call first. The name
is spelled in the two lists the tree requires to agree — scalarTyName
in codegen and evScalarName in typecheck — so evidence reaches the
same answer the reference map does.

Inert for everything that exists: stage-matched emission of
self_host/main.ax before and after is 199,765 lines of IR, byte for
byte identical. Only a Vec-typed field can move, and nothing in the
tree has one yet.

scripts/check-vec-field-shape.sh, 5 checks. Its table has four rows
rather than one because a single equality passes just as well from an
extractor that answers one constant: two rows must read a DIFFERENT
number, and the (Vec Int)/String row read 8 before this. Ablated
by deleting the classification and rebuilding — the gate exits 1 and
names the leaf shape.

The Vec migration is not mechanical, measured

docs/generics-design.md §3 said the port "is mechanical and the type
checker drives it". The second half is withdrawn, in place, and §4c
records what driving it actually measured.

Flipping Vec.ax's thirty container positions typechecks Vec.ax
itself with zero errors and leaves 4,406 in the tree, every one
AX3004. A checker-driven rewriter reduced that to 1,916 over four
rules, each verified by recompiling and rolled back when it made things
worse. Three converge — the typed view (memGetWordVec, nodeBVec),
widening a parameter USED as a Vec, and the (== v 0) handle
comparison. The fourth, widening a parameter that RECEIVES a Vec,
diverges: 1,916 → 5,990 → 10,102 → 14,392, and never comes back.
The compiler uses Int as a universal word type on purpose, so many
functions are genuinely polymorphic by punning and separating Vec out
is a decision per function rather than a rule.

vecPop is a second vecGet and §4 did not name it — its 0 on
an empty vector fabricates an a under (-> (Vec a) a), and takes the
same __indexTrap answer. vecLast inherits the trap by delegating.

What remains is 1,916 errors over 648 declarations, headed by the
compiler's context constructors (newCG, tcNew, smNew), which
build records of many Vec fields through raw words — and which the
classification above had to be right about first.

vecGet refuses an out-of-range index

The decision in docs/generics-design.md §4, built. vecGet
answered 0 past the end; it raises (__indexTrap) now — status
77, recoverable. vecTry is unchanged and is the reader for an index
nobody has checked.

The seed had to move first, and that is the whole reason this is a
separate commit from the primitive. build-shared-axc.sh compiles
stdlib/ with the installed compiler, so a library using a primitive
the seed does not know cannot build. reseed.sh's own header states
the rule — "land the construct the compiler must learn, reseed, THEN
use it" — and this is the third step of it.

Two fixtures pinned the old behaviour on purpose, and both went
red. tests/stdlib/313-vec-try.ax asserted that vecGet answers the
same for a stored zero and a missing element, with a comment saying it
was "asserted here, not assumed, because if vecGet ever started
distinguishing them this file should say so rather than quietly keep
passing." It started; the file says so. Its header now records the
premise it was built on and what answered it, instead of being rewritten
as though the argument never happened. 070-vec read out of range in
five places and moved them to vecTry.

A trap cannot be tested beside passing assertions — it ends the
program — so the refusal itself is pinned by
tests/stdlib/464-index-trap.ax and its .exit, and 313 keeps only
the half that can still be asserted inline: Some 0 for the stored
zero, None for the element past the end.

Recorded in compat/BREAKING even though nothing can compute it.
The signature is (-> Int Int Int) before and after and #effects=
does not move — a trap is not an effect — so verify-compat.py sees
nothing. It is a behaviour a caller could depend on, which is what that
file is for.

The compiler itself never read out of range: check-self-host
179/179 and check-diagnostics 194/194 passed on the first build with
the trap live, which is a stronger statement about the compiler's own
indexing than anything that was previously asserted about it.

__indexTrap: a call that never returns, and status 77

A trap stdlib/ can reach. Traps in Axiom are internal LLVM
functions the runtime block emits, so nothing in the library could
raise one. (__indexTrap) is a nullary primitive that lowers to
@__axiom_index_out_of_range — message, __axiom_recover_abort first,
backtrace, exit 77.

Typed (mkTVar "a") — a bare variable, freshly instantiated at each
use — so it inhabits every result type. One call stands in an Int
result and a String result in the same program, which a
concrete-typed trap could not. That is AX3040's own stated way out:
"make it DIVERGE, so every path ends in a call that never returns,
which is what makes for all a honest".

The divergence fixpoint never entered it, and I expected it to. I
recorded last commit that admitting a builtin to the greatest fixpoint
over Axiom-level tails would be a type-system change. It is not: that
fixpoint decides whether a declaration with a result-only variable is
honest, and a builtin registered in fns has no declaration to ask
about. The teeth were in the wrong place.

vecGet does NOT use it yet, and the reason is the bootstrap.
build-shared-axc.sh compiles stdlib/ with the installed
compiler, so a library using a primitive the seed does not know cannot
build — error[AX3001]: undefined variable __indexTrap at
stdlib/Vec.ax:225. A primitive lands in the compiler first and the
library uses it once the seed advances. Ordinary for a bootstrapped
language, and it is why this stops one step short of the change it
exists for.

tests/stdlib/464-index-trap.ax pins all of it: the two result types,
the value arms still answering, and the trap's own stderr and exit
status beside it.

The formatter table was re-pinned, not re-blessed.
check-fmt-selfhost refuses a table that leaves more than sixty
source files unpinned, and today's editing retired sixty-five — an edited file retires its own entry
by design, which is what keeps the table from churning. Entries were
appended for exactly those 65 (0 refused); no surviving pin was
touched. The golden's header warns that "a re-bless is how a broken
formatter becomes the reference", and the gate's preservation and
rebuild halves do not read this file, so a formatter that had gone
wrong still fails there.

Vec is a type, and AX3040 was refusing every empty container

Two pieces toward parameterised containers, both landed, both inert
until the decision in docs/generics-design.md §4 is made.

Vec is seeded beside Option — a DataEnt with no
constructors: abstract and parameterised. A Vec is made by vecNew
and read by vecGet, never matched, so there is nothing for a pattern
to name. (Vec a) is a writable type; before this it was AX3002 undefined type. The runtime shape does not move — a Vec is the
handle it always was, one word — which is what lets the type land
before the migration that uses it.

AX3040 narrowed to a BARE result variable, because it was wrong as
written. (pub :: vecNew (Vec a)) drew "the caller chooses the type
and a cast fabricates the value". It does not: (-> Int (Vec a))
returns a Vec, and an empty container holds no value of type a
for anything to have fabricated. The rule's own sentence says "returns
type variable a", and that is now what it checks. None : (Option a)
has had this exact shape since Option was seeded — it escaped only
because a builtin constructor never passes through the check. Before
this, every polymorphic empty constructor was refused, so no generic
container could declare the one function it cannot do without.
tests/diagnostics/347-result-only-tyvar.ax carries both arms.

What the migration costs, measured: flipping four signatures in
Vec.ax produces 3,934 errors. That is mechanical and the checker
drives it — and because (Vec a) and Int share a runtime
representation, a correct type-level migration must emit
byte-identical IR, which is the acceptance test.

What stops it is not types. Flipping all thirty container positions
leaves 42 errors inside Vec.ax, and vecGet is the reason: its body
answers 0 out of range, and under (-> (Vec a) Int a) that is
fabricating an a — a null for a reference element. You cannot make
up an a. So generics forces a decision about vecGet's sentinel:
answer (Option a), trap, or go ;@axiom:raw with vecTry as the
checked surface. §4 lays out the three; the first matches
compat/SENTINELS's direction rule and costs hundreds of call sites.

A route tried and rejected, recorded in §6 so it is not
re-proposed: a transparent-newtype representation ((data Vec (a) (MkVec Int)) represented AS its field). It works and is free, and it
is wrong twice over — fldClass answers from the type NAME, so a
newtype over Int would be released as a pointer; and Handle carries
a close/inert protocol the FFI keys on identity, which collapsing the
wrapper breaks (demo/060-opaque-handle, exit 73). None of it is in
the tree.

range, the counted loop — and for reserved for a keyword

(range i 0 n body) in the prelude: body once per i in
[lo, hi), with both ends read once. The shape it replaces is
written by hand about a hundred times in this repository —

(let ((mut i 0)) (while (< i (vecLen xs)) { BODY (set i (+ i 1)) }))

— and it re-reads (vecLen xs) every iteration. That is a correctness
difference, not only an ergonomic one: a bound that reads a structure
the body mutates is a loop whose length moves under it.
tests/stdlib/463-range-loop.ax pins six terms, including that one
(the body pushes onto the very Vec the bound came from and the loop
must still run twice) and hygiene (a, b, cur are the template's
names; a caller holding its own must still read its own).

for IS RESERVED, NOT TAKEN. It is to be a language keyword
covering both a range and a container, and a macro cannot be that: an
expression macro has ONE shape (MAC-LANG-14 — the rule form's
templates are declarations), so (for i 0 n …) and (for x xs …)
cannot share a name. Measured, they cannot even coexist: Html.ax
exports its own (for x xs body), and a program importing both
resolved for to Html's and answered AX3001: undefined variable i
in the body rather than an ambiguity at the import.

And a container for needs something this language does not have
yet. Vec is untyped, so an element is read through vecGetStr or
vecGetWord — which is exactly why Html.ax carries two loop
macros for one idea. Parameterised containers come first; for is the
keyword that follows them. Html.ax is untouched here.

Dogfooded at one site (self_host/symbols.ax), which is also the
proof that the seed expands it.

unproven joins the restriction manifest, and the tail match specialises

tests/agent/restrictions.allow read ok for a declaration the
compiler REFUSES. AX3057 was not in derive_manifest's verdict
map, so the three strict fixtures fell through to the default. A
derived file reporting less than the compiler knows is the defect this
gate exists to catch in others; unproven is a verdict now, and the
manifest shows the restriction system's whole vocabulary in one place —
ok, violated, unverifiable, unknown, unproven.

Three more of the compiler's absence sentinels answer Option Int:
scopeFindIdx (typecheck), graphStackIndex (typecheck) and
externLibBadAt (parser). All three had a wild read one comparison
away — (vecGet stack on), (strSlice lib bad 1), an index into the
scope vector. Six of the seven ported so far specialise to a register
pair; the compiler's IR carries 7 pair variants over 16 call sites.

emitMatchTail is hooked, so a match that IS a function's tail
specialises too. It was a second emitter and the first version hooked
only one — invisible in the gate, whose fixture's match sits inside an
argument. Armed only where scrutineeReleasable answers 0: an arm
in tail position may emit its own ret, and a release written after
the arms would sit past it, unreachable — a leak rather than a
diagnostic. That costs nothing today: scripts/check-unboxed-sums.sh
section 3b exercises the tail path directly, and every Option Int
lookup this tree has ported is in the releaseless case.

check-unboxed-sums grows to 15 checks with the tail-position
section, so the second emitter is not unexercised machinery.

Measured: only 3 of 37 -1 sentinels in self_host/ carry
restrict(no-alloc), so the blocker that stops four of the nine stdlib
rows is not systemic in the compiler — the adoption can proceed here.

restrict(..., strict) — when unproven has to mean refused

AX3057, an error: a strict restriction the effect walk cannot
prove. restrict(no-io) is a claim the compiler checks; where it
cannot settle the claim it says AX3051, a warning, and the
program compiles. Measured: (fn (runIt f n) { (f "x") n }) under
restrict(no-io) warns, checks OK, and prints to stdout at run time.
That is not a guarantee, and a restriction on a sensitive operation
is asked for as one.

The default is unchanged, deliberately. severity.policy records
why AX3051 is a warning: a body dispatching through a stored
function is a correct program the walk cannot follow, and refusing it
would make that shape unwriteable under any restriction rather than
merely unverified. That decision stands. strict is the author's side
of the same argument, per declaration: prove it or refuse the
program. A reader who sees restrict(no-io) and assumes it was checked
is worse off than one who sees nothing, which is the whole reason an
unproven guarantee can be worth less than no claim at all.

strict is a MODIFIER, not a restriction. It names nothing a body
must not do — it says what happens when the walk cannot settle what the
body does. So it is neither dispatched as a restriction nor reported by
AX3052: restrict(strict) alone restricts nothing and is silent,
where any other unknown word in that list is an error.

The seven arms, all in tests/diagnostics/393-restrict-strict.ax:

declaration	claim	answer
hardIo, hardAlloc, hardRec	X, strict over a called parameter	AX3057
softIo	no-io alone, same body	AX3051, warning — default untouched
provable	no-io, strict, settled and kept	silent — what strict asks for
refuted	no-io, strict, body performs IO	AX3049 — refuted beats unproven
strictOnly	strict alone	silent, and specifically not AX3052
lexStrict	no-cast, strict	silent — lexical, nothing to escalate

no-recursion was already complete for the graph it can see: mutual
recursion is caught with the cycle path (pingR -> pongR -> pingR).
What strict closes is the cycle whose middle edge is a parameter
the graph has no edge for — the case 391 records as silent before
AX3051 existed.

Zero AX3051 in the tree today, so nothing was reclassified.

GATES: check-diagnostics 194/194 (up from 193), check-render-selfhost
190/190, check-restrictions (393 added to the fixture table),
check-doc-drift, check-fmt, check-compat, check-agent-policy,
check-unboxed-sums, run-stdlib-tests 95/95, check-self-host
179/179, byte-identical fixpoint (199,145 lines, twice).

The compiler's own absence sentinels, slice 1

namedFieldIndex and findExternUnit answer Option Int. The
first two of self_host/'s absence column, and both specialise to a
register pair, so the type costs nothing: 5 pair variants and 14 call
sites in the compiler's own IR, up from 3 and 11.

namedFieldIndex is why the absence column is worth closing rather
than documenting. Its only caller used the answer as
(vecGet pats j) — a miss that reached the index is a wild read,
not a wrong answer, and the only thing standing between them was a
(< j 0) the caller had to remember to write. The type is what stops
it now.

findExternUnit had the sentinel one comparison from a real
answer: 0 is the entry file's own unit, and -1 was the miss.

Both keep the raw -1 in a private recursion — Path.ax's
pathLastSlashFrom pattern — because a walk that has not finished is
not a boundary.

expRepIndex is EXCLUDED, deliberately, and the reason is not
cost. Its five sites are in the macro expander, and
expShadowingRule uses two of its answers (ke, kl) as numbers and
as presence flags inside one nested condition. Porting it there is a
readability regression in the code that decides which macro rule
shadows which — the place where a subtle wrong answer is most
expensive and least visible. It wants its own slice with its own
fixture, not a mechanical rewrite at the end of another one.

restrict(no-alloc) does NOT unblock, and this corrects a claim made today

docs/unboxed-sums-design.md §5 argued that if (Some v) stops
allocating, the four restrict(no-alloc) absence sentinels —
strHexVal, utf8DecodeAt, utf8CharAt, keyStrEnd — are unblocked.
Measured false. A restrict(no-alloc) function answering
(Option Int) in the specialised shape still draws AX3049.

The reason is not an oversight in the checker: the boxed @F is
still emitted for callers that do not immediately match, so the
function genuinely can allocate — it depends on the caller. no-alloc
is a property of the function, and after the specialisation it is a
property of the function and its call sites, which is a
whole-program question the effect walk does not ask. Corrected in the
design note and in compat/SENTINELS; those four stay blocked, and
lifting them is a decision about what the claim means.

GATES: byte-identical fixpoint (199,022 lines, twice),
run-stdlib-tests 95/95, check-self-host 179/179,
check-diagnostics 193/193, check-fmt, check-restrictions,
check-doc-drift, check-unboxed-sums (13).

Result and reference payloads join the register pair

The two shapes the first slice refused are admitted.
(Result T E) — both arms fieldful — and any Option/Result whose
payload is a reference now specialise. pairRetOK accepts Option
with one type argument and Result with two, of any class the
reference maps can name; pairEntryOfArity accepts rep 0 (all-boxed,
which is what Result is) beside rep 2.

The ownership rule, which is the whole of the work.

• Construction retains only what does not already own a share. A
  reference payload is moved when valueOwnedRef says the value
  arrived owned, and retained when it is borrowed.
  emitFieldStores reaches the same place by a longer road — retain,
  store, then release the temporary again — which is a move written as
  +1 −1. Here it is written as nothing at all.
• The release belongs to the ARM, not to the match. A block was
  released once because one release reached every field through the
  shape word. A pair has no shape word, and (Result Int Error) has a
  machine word in Ok and a share in Err, so releasing
  unconditionally would hand axiom_release an Int above 4096 and it
  would read it as a block header. Each arm releases its own payload,
  or does not.
• scrutineeReleasable is reused unchanged, so an arm whose binder
  escapes still turns the release off for the whole match — the same
  guard the boxed path uses.

THE FIRST VERSION OF THE RETAIN RULE LEAKED, and the gate now catches
it. Retaining unconditionally meant (Err (mkError ...)) — which
answers an owned Error — took a second share, and the consumer's
single release left one behind: 13.5 MB against 1.28 MB boxed over
100,000 iterations. Fixed, and re-measured at 1.30 MB.

The gate grew the assertion that found it: 10 checks to 13. It now
compiles a fixture over both new shapes and reads the arena mark
(tests/stdlib/370-error-propagation.ax uses the same cell — word 0
the bump, word 2 the chunk) before and after 40,000 iterations. The
bump moves 208 bytes; a leaked payload is 32 bytes and up per
iteration, so a real leak is megabytes. It also asserts the Result
consumer emits exactly one release — releasing both arms is the
wild read above.

Coverage, stated plainly. On the compiler's own source this changes
nothing — still 3 variants and 11 call sites, because self_host/ does
not use Result or a reference Option in the direct-call-immediately-
matched shape. tests/stdlib/371-err-module.ax gets 1 variant and 2
sites, so it does fire on real Result code. What the slice buys is
that the shapes are no longer refused, which is what the rest of
ERR-ADOPT-1 is written in.

VALIDATED: byte-identical fixpoint (198,937 lines, twice),
run-stdlib-tests 95/95, check-self-host 179/179, check-fmt,
check-compat (32), check-restrictions (20), check-agent-policy,
check-unboxed-sums (13).

Option Int is free: the register pair, built

(Some v) no longer allocates where it is immediately matched.
docs/unboxed-sums-design.md's specialisation, implemented:
self_host/codegen.ax emits @F$pair returning { i64, i64 } beside
an unchanged @F, and rewrites a match on a DIRECT call to F to
call it and read the tag and payload from registers.

What the compiler now emits for the canonical absence shape:

define { i64, i64 } @optFind$pair(i64 %n) #0 {
.L3:
  ret { i64, i64 } { i64 1, i64 0 }          ; None
.L4:
  %.t6 = mul i64 %n, 2
  %.t7 = insertvalue { i64, i64 } undef, i64 0, 0
  %.t8 = insertvalue { i64, i64 } %.t7, i64 %.t6, 1
  ret { i64, i64 } %.t8                      ; Some, no block
}

and at the site, call { i64, i64 } plus two extractvalues and an
icmp — no axiom_alloc, no shape word, no refcount, no
axiom_release. check-unboxed-sums.sh moves from 1 block and 1
release to 0 and 0, which is the gated claim.

On the compiler's own source it fires 3 times and rewrites 11 call
sites — internFind, pathLastSlash, pathExtIndex: the absence-
column family exactly.

BENCHMARKED, with the control run. Two stage-matched compilers —
same source, same input, differing only in whether the code generator
has the specialisation — on the interner benchmark, best of seven:

variant	per lookup	wrapper
no Option at all	49.54 ns	—
boxed	56.70 ns	7.15 ns
register pair	49.59 ns	0.04 ns

99.4% of the boxing cost recovered, 12.5% off the workload, landing
0.08% above having no Option in the language at all — better than the
hand-written prototype's 96.9%, because the compiler also removes the
match-on-a-block the prototype kept.

On the compiler's own self-compile it is a wash: −0.14% and +0.93%
across two stage-matched pairs, bracketing zero. Seven of nine
internFind sites specialise, pruneMark among them; the two that do
not have a let-bound scrutinee rather than a direct call, which is
the restriction working. internFind is not hot enough in a
self-compile for that to move a 1.13s number.

The 38% was entirely a stage artifact, and the control proves it:
axcB and axc3 are both stage-2 and differ by under 1%. The 38% was
two BUILDERS, not two code generators.

This corrects an earlier number. compat/SENTINELS records the
internFind port as costing "about +4% on code generation", from pairs
reading +3.5% and +4.6%. Removing that cost now yields nothing
measurable. Those runs read 1.75s in-process against 1.13s today — the
machine was ~55% slower, i.e. loaded — so compiler-level differences
of a few percent are not resolvable here, and +4% is an upper bound,
not a measurement. The block count is not subject to that: it is exact,
and it is what the gate holds.

What refuses, and why each refusal is a hazard declined rather than
handled: main; no signature; a function taking an evidence word; a
return type that is not (Option T) with T a machine word; a tail
that is not None or (Some e); a body holding anything that would be
lifted twice; and a self tail call, because TCO rewrites that into a
jump to a loop header the variant does not have. Anything unrecognised
keeps the boxed path, so the failure mode is "no speedup", never
"wrong answer".

A reference payload is refused on purpose. The block owns a share
of a reference field and axiom_release hands it back; a pair has no
refcount to give that share back with, so a variant there would be a
use-after-free rather than a speedup. (Option String) still boxes,
and the gate asserts it — which is also what proves the counter reads
the IR at all.

The shape word bit back, from the other side. The state needed four
words and CG had no room: a block's reference map covers 47 words and
CG was at 47, so a 50-field record is AX3040-adjacent AX3029,
"too wide for one reference map". It is packed into one field holding a
four-slot Vec. That limit is docs/memory-model.md MM-LIFE-2d, and it
is the same shape word this optimisation exists to stop writing.

The token cannot be stolen by a nested call. emitPlainCall
captures the arm and disarms it before emitting arguments, restoring
its own copy for its own call line — so a call inside an argument
cannot consume the token the match site armed for the outermost call.
releaseOwnedArgs still runs on both paths, which is why the pair form
is a branch at the existing call seam rather than a second call
emitter.

VALIDATED: byte-identical self-hosting fixpoint (198,598 lines, twice),
run-stdlib-tests 95/95, check-self-host 179/179, check-fmt,
check-compat (32, census unchanged at 10 + 9), check-restrictions
(20), check-agent-policy, check-doc-drift, check-unboxed-sums
(10, up from 7 — the gate now proves the specialisation HAPPENED before
reading its zeroes, because a zero block count is satisfied just as
well by a function that was never emitted).

The gate that will prove the Option win, before the win exists

scripts/check-unboxed-sums.sh — the gate
docs/unboxed-sums-design.md §4 asks for, written first and on
purpose. It counts the heap blocks an Option construction costs in
the emitted IR, for a fixture whose matched lookups are a known
number. The count stood at fifty-four then, up from fifty-two — this one
and check-vec-field-shape.sh; the section's own count is stated above.

Why a count and not a timing: bench-compile.sh is explicit that a
wall-clock bound on a shared runner is a flaky test, and the ratio
gates here measure scaling rather than constants. Blocks-per-
construction is neither — it is a property of the module, it is exact,
and it is what the optimisation is about. A timing gate goes red on a
noisy runner and stays green on a representation regression; this does
the reverse.

Seven checks:

• the fixture answers 249500 at --opt 0, 1 and 2, because a faster
  wrong answer is not the goal and behaviour is asserted before cost;
• optFind builds 1 block and its matching consumer performs 1
  release — the numbers are in the gate, and when the register-pair
  specialisation lands both become 0, which is the proof. The win
  gets asserted by a number in the emitted module rather than by a
  stopwatch;
• a second construction must raise the count — without it, an awk
  range that matched nothing would read 0 and look exactly like a
  landed optimisation, which is this repository's most common defect;
• the count is anchored on one definition — moving the
  construction into a different function must leave optFind at 0.
  The third check proves the counter can rise; the fourth proves it is
  not just counting every axiom_alloc in the program.

The fixture lives in the gate as a heredoc rather than under tests/:
every .ax added to tests/selfhost/ is swept by gates carrying
population counts, and a fixture whose only reader is this gate should
not move numbers in gates that have nothing to say about it.

Option and Result can be free: 11.86 ns of box, measured away

docs/unboxed-sums-design.md — designed, prototyped, not built.
(Some v), (Ok v) and (Err e) are each a 16-byte heap block with a
refcount, a shape word, a tag and the field. Measured over 20,000,000
interner lookups at --opt 2, best of five:

variant	per lookup	wrapper
raw -1, no Option at all	80.30 ns	—
(Option Int), boxed — today	92.16 ns	11.86 ns
(Option Int), two registers — prototype	80.67 ns	0.36 ns

96.9% of the box recovered, and 0.45% above having no Option in the
language at all. The prototype is hand-written LLVM derived from the
compiler's own output, run through the same opt -O2 / llc -O2 / cc
pipeline bench-compile.sh uses, printing the same checksum — so it is
a measurement of the REPRESENTATION, not of an implementation. No
compiler code changed.

The representation: a sum whose constructors carry at most one word
becomes {tag, payload} in two registers. That is not an arbitrary
cutoff — 16 bytes is what x0/x1 and rax/rdx return before both
ABIs spill to memory. Option T qualifies for every T; Result T E
qualifies for the shape stdlib/Err.ax uses throughout.

A one-word niche cannot do it. Representing (Some x) as x works
where every T is a heap value, and fails on exactly the case that
matters: an Int is a raw i64, so (Some 5) would be 5, which is
indistinguishable from an immediate tag under the icmp slt %v, 4096
that opens every match.

Why this is not only a speed change. Four of the nine absence
sentinels in compat/SENTINELS — strHexVal, utf8DecodeAt,
utf8CharAt, keyStrEnd — cannot become Option today without
withdrawing a restrict(no-alloc) claim. If (Some v) does not
allocate, that blocker is gone. Every WIDENED row in ERR-ADOPT-1 is
widened because building a Result allocates; an unboxed Ok widens
nothing. So this comes before the rest of the migration, or those
functions are ported twice.

The cheap alternative was measured and rejected. At -O2 LLVM
inlines neither axiom_alloc nor axiom_release — two real calls per
wrapper — so emitting the allocator's fast path inline is the obvious
smaller fix. Marking both alwaysinline recovers 14.3% of the box
against the register pair's 99.2%. The call overhead is a seventh
of the cost; the rest is the free-list pop, the shape word, the tag,
the refcount, the field store, the caller's two loads and the release's
decrement and push. Inlining moves none of that. There is no cheaper
fix, and §3a of the note exists so it is not re-proposed.

The implementation plan changed as a result of writing it down. The
first draft proposed a general type-directed representation — unboxed
in flight, boxed in storage — whose two hardest pieces were the storage
boundary and ownership with no shape word. Both are avoidable.
Emitting a second definition (@F unchanged, plus @F$pair
returning {i64,i64}) and rewriting only call sites that immediately
match the result means a pair never reaches a let that outlives the
match, a Vec, a struct field or another function's argument — so
there is nothing to coerce and no ownership to transfer. It needs one
fact codegen can already look up (the callee's declared return type,
via findFSigCg) rather than the per-node types it does not have, and
an unrecognised tail shape falls back to the boxed path, so the failure
mode is "no speedup" rather than "wrong answer". Restricting the
payload to a non-reference at first covers every row this unblocks —
they are all Option Int.

Not built, and deliberately not bolted onto the port that measured
it. This is the code generator of a self-hosted compiler that must
reach a byte-identical fixpoint, and a half-right return convention
fails as a silent miscompile rather than a red gate. It wants its own
change and its own gate — counting axiom_alloc calls in the emitted
IR for a fixture with a known number of matched lookups, with an
ablation that forces the boxed path and must move the count.

The interner's miss is None, and the effect row said who would pay

internFind answers (Option Int) instead of an Int that is a
dense id when non-negative and -1 when the string was never interned.
compat/SENTINELS: stdlib/Intern.ax 1 → 0 absence, and the
library is 10 failure + 9 absence over 6 modules, gated by
check-compat.sh.

This was the one row of the ten that the entry below left to a
measurement rather than to a claim. Two compilers, built by the same
compiler from sources differing only in this port, both compiling the
same 197,338-line input, best of five runs each:

stage	-1	(Option Int)
check (lex, parse, expand, typecheck)	0.4484s	0.4469s	flat
serialise and write the IR	1.2980s	1.3440s	+3.5%
in the axiom process	1.7464s	1.7909s	+2.5%
axiom build, end to end			+0.4%

Quoted as a range, because two pairs were taken and they do not
agree to the tenth. An earlier pair, built and measured the same way,
read +4.6% and +3.4% for the same two rows. So the honest statement is
about +4% on code generation and +2.5–3.4% in the process; a single
pair reported to two decimals would be false precision at this
separation, which is the same reason bench-compile.sh takes best-of-5
rather than a mean.

End to end is +0.4% because 84% of a build is opt and llc. The
number that matters is the code-generation row, and it is DECLARED,
not gated: bench-compile.sh is explicit that a wall-clock
bound on a shared runner is a flaky test, and the ratio gates that
exist here measure scaling rather than constants. The before-and-after
is above and the port is one commit to revert.

#effects= PARTITIONED THE CALLERS BEFORE A LINE WAS EDITED, and the
measurement matched it. Nine external callers, every one of them
(< id 0). The two in self_host/namespace.ax already read
Alloc,Mut and run during resolve — the check stage did not move. The
five in self_host/codegen.ax had an empty row, and the whole
+4.6% is in the stage those five run in.

The interner's own hot path pays nothing. internFindFrom keeps
the -1 and stays private; internIntern calls it directly rather
than through the public wrapper, the same exception Path.ax's
pathExtIndex takes. The concern that had kept this row unmeasured —
one library caller, running once per interned string — costs one line,
because a public boundary and a recursion are not the same place.

Intern.ax carries no restrict claim, which is why this one was
a measurement where the four below are refusals. Check #restrict= as
well as #effects=; axiom symbols prints both.

A BARE None ARM HEAD IS A VARIABLE PATTERN, NOT A CONSTRUCTOR
TEST — found while porting, and every arm here is parenthesised because
of it. docs/reference.md writes nullary patterns as ((Nothing) d)
and ((Nil) 0); the unparenthesised (None x) that reads exactly like
a None arm is a binder named None that matches ANYTHING. It lowers
to an unconditional default with no tag test at all:

;; (None 99)            ;; ((None) 99)
.L2:                    .L2:
  store i64 99, ...       %.t26 = icmp eq i64 %o, 1
                          br i1 %.t26, label %.L27, label %.L25

For a two-constructor Option both behave identically, which is why
nothing catches it — but the bare form skips the tag test and satisfies
exhaustiveness trivially, so a wider data would fall into it in
silence. All eight arms this change adds use ((None) …).

The formatter is the thing that noticed, and it was right to.
axiom fmt REFUSES (None <compound>) while accepting
(None <atom>) — the ambiguity is real and its grammar declines to
guess. That refusal is what sent this to the emitted IR; see
check-fmt.sh, which formats a copy and so tests whether formatting
changes MEANING.

scripts/check-name-scale.sh needed re-anchoring and said so. Its
red half ablates mangleIdxHas by matching that function's whole body
as a literal; the port rewrote the body, so the gate failed with "its
shape has moved" rather than passing on an ablation that no longer
applied. Re-anchored, and the ablated compiler still fails the doubling
arm.

GATES: check-compat (32 checks, census 10 + 9), check-stdlib-api
(regenerated — internFind now reads (-> Int String (Option Int))
with Alloc), check-name-scale (both arms, ablation load-bearing),
tests/stdlib/090-intern (every pre-existing golden line
byte-identical, two appended that assert which constructor came back).
One WIDENED row in compat/BREAKING for 0.6.4.

Option allocates, and four of the absence sentinels claim no-alloc

(Some v) is a constructor application, so restrict(no-alloc)
refuses it (AX3049). Measured 2026-09-01. That settles the plan for
the other half of ERR-ADOPT-1: strHexVal, utf8DecodeAt,
utf8CharAt and keyStrEnd all read
#restrict=no-io,no-alloc,no-foreign in axiom symbols, so they
cannot become Option without WITHDRAWING a checked claim — a
different decision from porting one.

docs/error-model.md §10 reasoned the other way while refuting P6: the
modules dense with restrict carry absence sentinels, "which become
Option, which has no Error, no computed message and none of the
traffic the blocker is about". The first half is right; the conclusion
does not follow. Option carries no Error and builds no message, and
it still allocates.

It was invisible until 0.6.1. Before that, restrict(no-alloc)
could not fail — a constructor contributed nothing to the effect walk —
so a lookup answering (Some v) under the claim would have checked
clean. Closing that hole is what made this measurable.

Gated rather than asserted:
tests/diagnostics/384-restrict-no-alloc-ctor.ax gains a some arm
(AX3049) beside a none arm (silent). The pair is the measurement —
None is an immediate tag with no block behind it, so what is refused
is carrying a VALUE out of a lookup, and a partial migration answering
only None would never have found it.

compat/SENTINELS now names all ten absence rows with the reason each
is not moving. Nine are blocked or excluded on a measurement; the tenth,
internFind, is the only one where a measurement would decide it, and
it sits on the interner's own hot path.

ERR-ADOPT-1 slice 4: the working directory, and the first port that costs a caller nothing

sysGetCwd and IO.cwd answer (Result String Error). The census
falls 11 → 10 failure, stdlib/Sys.ax 8 → 7.

This slice was found by disbelieving an exclusion. Everything left
in Sys.ax is set aside on a measurement — sysWriteFd, sysReadFd,
netAccept, netAcceptFrom and netPollWait are #effects=IO alone,
and porting them widens the row under writeStr, under println, at
804 macro expansions. sysGetCwd was set aside for a different kind of
reason: that it "answers a String and its failure is "" rather than
an errno, so it is a different port". That is a remark about shape, not
a measurement, and the shape was the only thing in the way.

Measured before and after, #effects= is Alloc,IO,Mut both times
— the function already memAllocs a 4097-byte buffer and strDups its
answer, so the Ok/Err constructor disappears into a row that was
already there. These are the first ERR-ADOPT-1 rows in
compat/BREAKING that are CHANGED rather than WIDENED; every
earlier one gained Alloc.

What the sentinel cost: ERANGE (a path longer than the buffer), ENOENT
(a working directory unlinked out from under the process) and EACCES (a
. that cannot be opened) all arrived as the same "", with the errno
in hand at all three failure points and discarded. All five call sites
read it as a presence test. self_host/lsp.ax's two now say
(unwrapOr sysGetCwd "") — the same behaviour, with the decision
written down rather than inherited.

A comment in stdlib/Sys.ax said the migration was unblocked, and it was wrong

sysResult's comment read "Ok, Err and mkError are effect-free"
and "a Result-returning function whose message is a literal has NO
effect row at all", concluding that the effect row no longer blocked
the migration. Measured 2026-09-01, sysResult is #effects=Alloc and
its body is nothing but the constructor — so the constructor is the
allocation. A literal message removes Mut, not the row.

It sat a hundred lines above sysWriteAllFd's comment, which states
the opposite correctly, and it would have told the next reader that
sysWriteFd and sysReadFd were portable. They are not.
docs/error-model.md §10 had the same measurement right the whole time
(openish Alloc,Mut against openLit Alloc, neither of them
empty).

Also corrected in docs/error-model.md §10.1: the absence column read
nine against a gated ten — netPollSignalAt's declared move
from failure to absence was recorded in compat/SENTINELS and never
carried into the document. Nothing holds §10.1's numbers to that file,
which is why it drifted.

web/package.json and its lock are version sites

axiom-site@0.6.1 sat in a tree whose VERSION read 0.6.3. Nothing
held it there: version-sites.sh listed web/src/data/site.ts and
web/src/data/bench.ts and stopped, so the manifest sitting beside them
drifted two releases without a gate noticing. It is invisible — the
package is never published — but a number nothing checks is the defect
this file is about.

Both the manifest and web/package-lock.json are listed now: 35 sites
over 22 files, up from 32 over 20, with 22 extractor/site pairs
observed red rather than 20.

The lock needed a reader of its own. json_version matches every
"version": "x.y.z" in a file, which in a lock file is three hundred
npm packages rather than one site, so npmlock_version anchors on the
site's own name and takes only the version that FOLLOWS it — exactly
what lock_version does for the two Cargo locks, for exactly the same
reason. And the lock is listed for the reason those were: a site's
OUTPUT is still a site. npm install writes it from the manifest, both
Cargo locks shipped a release still stating the version before it
because nothing read them, and leaving this one to npm to keep in step
would have been the same bet.