STATUS.md

Component: ir

Status: tested Last updated: 2026-07-29 · S41 — the geometry queries gained a consumer-coverage gate. tests/consumer_coverage.rs is ADR-0033's hand-run grep, executed on every build: for each backend crate, tile_plan and elem_plan must be consumed, or the backend must be Exempt with a written reason and an end condition (cuda: predates tile_plan — landed S25, last CUDA session S23 — exemption ends when the NVPTX leg lands; verilog: not-started stub). Three properties make it a gate rather than a report: a backend directory missing from the table fails (no exemption by omission), a stale exemption fails (a backend that starts consuming loses its exemption, so the gate cannot go quiet), and a self-check ensures a path typo cannot make every check pass vacuously. Scope is geometry only — path_plan/guard_plan/emission_plan/last_use_plan/bounds_proof are per-backend capability decisions, not genericity obligations. This is the durable answer to the nine-session drift ADR-0033 was written about, and it is independent of how backends are packaged (Sapir, S41: "the tests should guard it by checking all consumers all the time"). No mapal-ir source changed. Previous: S40 — the arm owns the loop; gating is stable across LiftLoops (plan-s40-the-arm-owns-the-loop, SHIPPED — S39's §4a P0 CLOSED). The v1 refusal keyed a site's semantics on graph shape (SCC presence), and LiftLoops changes shape while preserving meaning — the same site was strict raw and gated rewritten, breaking eval ∘ rewrite = eval (three pinned seeds). The replacement: loops join an arm as UNITS — a unit is the whole region the flat walk hands the driver (SCC-incident + machinery + loop_plan cones), machinery is never per-morphism ownable (per-morphism closure provably cannot complete a cycle, so the only machinery it reaches alone is the exit boundary, and gating that fragment starves the driver — the S39 route object built before read failure, now explained), a canonical unit joins iff every external consumer of every member's target is owned, and it is represented in own by its LoopEnter handle alone (internals stay out, so subtraction/re-close/skip-sets never see them; the handle carries the unit's transitive can_trap, and a loop is heavy by definition). A non-canonical unit (no loop_plan) never joins — and cannot lift either, since LiftLoops consumes loop_plan facts: no stability hole. Found by test on first run: a site inside a loop vacuously "owns" its enclosing unit (every external consumer satisfied from inside), so a site whose boundary edge is a unit member never joins that unit. Two topologies, one mechanism: loop-inside-arm gates through the handle; arm-inside-loop-body gates through ordinary closure once machinery is barred (the LLVM loop emitter's cones gained the gated-skip interp already had — an asymmetry invisible while such sites could not exist). Consumers: interp and LLVM fire the driver from the Phi (run_loop/emit_loop on the handle) and skip a gated LoopEnter in every walk; path_plan folds a gated loop into its Phi's scalar Seq component instead of minting a launch-dispatched loop task; ConstFold refuses to fold a Phi whose arm owns a LoopEnter, transitively through nested sites (dropping a whole unit is replay surgery; the fixpoint driver refolds after LiftLoops). CUDA skipped (Sapir): "cuda can be skipped it will be translated to nvptx later anyways" — the host emitter keeps strict semantics for loop-touching sites via a ctx-build filter; goldens unmoved, and the shapes are unreachable from surface (L1406). Gate: three seeds pass, PROPTEST_CASES=1024 green, LLVM differential 37/37 in 419.6 s (1,280 runs), CUDA suite 163 green, workspace 1006 passed / 0 failed (post-review-round), fmt clean; A/B emission vs 8b40442: 103 identical, 1 differs (examples/calc.mapal raw — S39's own change, pinned by its goldens), 0 new emit failures — S40 moved zero surface emissions. Tests: +3 algos.rs (unit join, shared-loop refusal, in-body arm), +3 interp guards.rs (untaken loop does not run, taken loop still traps, in-body untaken arm), unit-atomicity invariants in guard_ownership.rs, +6 review regressions in mapal-rewrite/tests/guard_loops.rs. Coverage gap recorded: testgen builds only loop-inside-arm (topology a); arm-inside-loop-body (topology b) rests on the two hand-built tests. The 17-agent adversarial review confirmed seven defects in the first build — all fixed same-session (plan-s40 §6b): in this crate, the re-close could not unwind a joined unit (the handle is now re-tested with the join predicate — its merge-only test was vacuous, every consumer a member), sink unit members joined vacuously (a loop writing Return gated; observable sinks now refuse), and an in-body guard's loop-invariant work was double-owned (the subtraction now sees nested Phis through owned handles). The remaining four were rewrite-crate (DCE pin on gated(), ConstFold alias-mirrored drop + loop-armed fold refusal, and DCE's verdict-cone dead-sink pin closing the [5] class for DCE — see rewrite STATUS). Post-close (Sapir's catch): guard_plan gained a Phi-free early return — it built units, bounds_proof and the trap fixpoint even for Phi-free functions, per pass per fixpoint round, which was most of a +16.4% compile-time regression on the emission sweep; with the early exits (this + DCE's) the sweep is +1.7% vs 8b40442 and results are exactly unchanged (performance/s40-compile-time.md). Previous: S39 — guards gate the flow; an arm that is not taken does not run (plan-s39-guards-are-conditional, SHIPPED). guard_plan joins the deduced queries: per Phi-position guard, the condition object and each arm's exclusive work. (1 > 0) -> { -true-> 42; -false-> 7 / 0; } printed nothing and exited 101; it now prints 42. The root error was a realization promoted to the semantics — category-ir §4.4 justified computing both arms by "both datapaths exist" in hardware and the "branchless-by-default bias for GPU codegen", which are statements about how to emit a guard on one machine, written down as what a guard means (FRAMEWORK §4.2: a TrnLoc promoted to a Trn). Two distinctions the strict reading collapsed: pure is not total (the arm restrictions buy purity, but Div/Mod/Index/Update are pure partial morphisms, so evaluating both arms implements the copair only where BOTH are defined — the wrong morphism, not a different schedule of the right one), and compiled is not computed (both arms stay in the binary; only running is conditional). Mapal already gated one placement and not the other: I4's loop fork hangs LoopBack/LoopExit off one shared Bool that fire mutually exclusively, validate()-enforced — so -true-> { … -> loop; } gated while -true-> 42 did not. Same syntax, same Bool, two semantics; this removes the exception rather than adding a feature. Five defects the plan did not predict, each found by running rather than reading. (1) Ownership is consumer closure, not liveness: the plan proposed "what DCE would delete if the arm edge were removed", and the 1,280-run differential refuted it (testgen case #94, read before write) — nothing deletes dead code before execution, so a Proj feeding both an arm and a dead Neg looked exclusive, got gated, and the dead Neg read an object the unchosen arm never wrote. A morphism is arm-owned iff EVERY consumer of its target is arm-owned. (2) Subtraction of a nested site's work can orphan a morphism whose consumers left with it — re-closed to a fixpoint. (3) can_trap/heavy must be transitive through nested sites, in guard_plan and in ConstFold's losing-arm drop: calc's right-folded 5-arm match hides Div/Mod in the innermost site, so without transitivity the outer arms went ungated and calc(0, 20, 0) still trapped — and the ConstFold half made the rewritten build trap while the oracle returned 20, an R1 divergence caught only by running both. The cost cut is measured, not assumed: an arm's own-list is never empty (it always ends with its boundary Pair edge), so the first implementation branched even for -true-> x, and in sepia that branch landed inside a per-element map body where it would cost the loop its vectorization. GuardSite::gated() is legality-then-cost — an arm that can trap must be gated (no cost argument buys it), a heavy arm (bulk op or call) is worth gating, two arms of scalar arithmetic are left alone. Emission is unchanged almost everywhere, structurally: 103 of 104 A/B emissions byte-identical against 8b40442 (= 24f52c9 + a rename-only commit) (every bench shape, every matmul, abs, sepia, all three faces), the one change being examples/calc.mapal; linked binaries byte-identical; zero new emit failures. The class had zero differential coverage — a census found 0 trapping arms in 82 guard sites over 320 testgen programs, which is why the bug reached production; Step::PhiTrapArm now generates them (139 sites, 60 trapping). OPEN P0: gating is not stable across LiftLoops — guard_arm's refusal (skip the site when arm work touches a loop SCC) makes the semantics depend on whether a pass ran; the raw graph runs strict and traps, the rewritten one gates. The gated side is correct; the refusal cannot just be deleted (loops break: route object built before read), so arm-owned work must fire through the loop driver. IR-only — L1406 keeps -> loop out of a Phi arm, so no surface program is affected; the 1,280-run differential passes. Gate 992/2, three seeds pinned. Owed: the CUDA device (kernel) form is still strict — only the host form is gated — and no CUDA change has hardware verification. Previous: S38 — trap order is source order; the S37 P0 is CLOSED (plan-s38-trap-order-is-source-order, SHIPPED). topo_order's ready worklist is now a min-heap on (loc.start, loc.end, insertion index) instead of a FIFO, because insertion order is a property of the compiler and trap order is observable, so it must be a property of the program: the graph does not order two independent trapping ops at all, rewriting creates and destroys objects, and Inline could therefore turn Trapped(IndexOob) into Trapped(DivZero) — breaking eval ∘ rewrite = eval. This is S29's clock-read fence generalised (same sentence: "the graph orders pure work against a clock read not at all"), and it makes SourceLoc a semantic attribute rather than debug metadata — every rewrite now owes it a discipline exactly as it owes value-preservation (ADR candidate, plan §6.2, OPEN). Companion: testgen's const L = SourceLoc{0,0} at 122 sites became a per-build monotonic counter, without which the new key degenerates straight back to insertion order and the corpus tests nothing. The plan's cheaper variant A′ was priced and REFUTED — 62.2% of raw lowered objects (484 of 778 over 14 examples) change position, only 9 of 36 functions are already in source order and all nine are 3–9 objects; the deviation is systematic (an object's loc is the operator token, not the sub-expression extent, so (x > 0) puts > at 483 and its operand 0 at 485 with the constant created first), so "make lowering create objects in source order" would churn every golden in the tree rather than A's 38. The bug is wider than the plan stated, and the wider form is the better demonstration: the same root cause let a trap swallow output written before it, because mapal_par_run_pinned runs its body synchronously on the host thread — same program, both exit 101, PRE prints nothing and POST prints 111\n222\n. Invisible to the 1,280-run sweep by construction (expect_native maps Trapped to (None, 101) and the stdout assert is if let Some(want)), now pinned by differential_trap_preserves_preceding_output as a verified negative control. Gate 981 passed / 0 failed, differential 37/37 in 403.93 s, fmt clean. 38 goldens moved, all adjudicated (60+ subagent verifier/refuter pairs over three rounds): 37 ordering-only, one intended behaviour change (example_calc) signed off by Sapir; the observable-effect axis closed by proof — 34 unchanged sequences, and the 3 where a PRINT crosses a mapal_par_check are safe because those modules hold zero mapal_par_trap sites and the only production writer of run.trap is mapal_par_trap, so check_trap's if trap != 0 can never fire. Perf on the i9 (3 passes × 101 alternating, both faces, values byte-identical): the "nothing moves" pre-registration is refuted — saxpy 1t +5.3% ×3, conv2d 1t −3…−8% but par +3…+7%, mm1024 +2.6% conformance yet flat on the FMA face; mechanism deliberately not isolated (Sapir), and vector-instruction counts are byte-identical pre/post so it is scheduling, not codegen. Previous: S37 — elem_plan: what out[i] IS, as a deduced graph fact (plan-s37-stage-structure). ElemSrc = Index | Broadcast | Load (the cut) | Pair | Apply, with ElemPlan/CategoryIr::elem_plan(f) joining the six existing per-fn queries in algo.rs. The law is the unique homomorphism from the producer DAG into the term algebra — Iota ↦ Index, Fill ↦ Broadcast, Zip ↦ Pair(·,·), Enumerate ↦ Pair(Index, ·), everything else ↦ the cut — so stage composition is nothing but the recursion continuing past a cut. Enumerate needs no constructor of its own, which is the proof this is one notion rather than five: ADR-0018 already calls Zip the canonical iso Aⁿ × Bⁿ ≅ (A×B)ⁿ, and enumerate a ≅ zip(iota n, a). Three guards, each preventing a distinct wrong answer: single in-edge (a multi-producer object has no unique law), outside every loop SCC (a loop-carried array differs per iteration), depth cap 16 (the tile_iota_size/element_range precedent; cutting early is always sound because Load is the status quo). Producers are an exact op-tag set, not a "carries no body" shape test — trap-freedom is a documented guarantee of those four tags specifically. Map joins only as ElemSrc::Apply, behind body_is_classifiable (trap-free via tile_trap_free + loop-free + an explicit Print/TimeMs check, because tile_trap_free's catch-all arm would admit them); Apply carries the producer's materialised array so a backend that DECLINES to recompute degrades to a load instead of poisoning the law containing it. No cost model here (ADR-0032, Sapir): the query says what the element is, never what it costs; store-vs-recompute is the backend's, and gets a different answer per target. Same change migrates tile_iota_size off literal op-tag matching — it asked op == Operation::Iota, what the node is tagged, where it means to ask what the element is; behaviour identical today, and the check now follows the fact. Pinned first by backends/llvm/tests/tile_sites_pin.rs (15 sources) because tile_site calls it twice per site and a lost site falls silently to the scalar emitter — a 4.0× cliff. 7 unit tests incl. the trapping-body gate with its positive control; 78 ✅. Open (P0): topo_order breaks ties on object insertion order, which rewriting reshuffles — Inline can change which of two independent traps fires. Fix ratified and deferred: plans/plan-s38-trap-order-is-source-order.md. Previous: S36c — the fold's sequentiality is now a named, planned gap. Operation::Fold becomes TaskKind::Seq { morphisms: vec![m] } (algo.rs:1221) while Map in the arm directly above becomes TaskKind::Split — so a reduce runs on one lane and pays full pool cost. Measured consequence: on the pinned i9 the reduce cell reads 1.98 ms par against 0.367 1t, but the honest reading is "the same left fold, one lane" — at one thread, where Mapal, C++ and Rust all compute the same function, Mapal is the fastest of the three (0.3668 / 0.3821 / 0.3821); the baselines' parallel legs reassociate and compute a different function. Splitting it is not a wider Split: Split is sound because slices write disjoint elements and path_plan asserts one producer per object (algo.rs:1347), while every slice of a split fold writes the same scalar — it needs a third task shape with per-lane partials, a pinned merge, and a runtime completion hook. Designed in plans/plan-s37-scan-recurrence.md, which consolidates Map/Fold/window/scan into one Scan object carrying window/jump/carry plus a partial combine?/unit? pair that is defined exactly when the recurrence is splittable. Integers deduce structurally (ADR-0028's exact-op set, accepted 2026, never implemented); floats need ADR-0032 D1's precision lattice, which Ty does not carry. Previous — S36 — a clock read is a DAG node (plan-s33b §3, SHIPPED here rather than in the runtime). path_plan stops leaving TimeMs on the host spine as a bare checkpoint: it becomes its own single-morphism Seq task with pinned = true, carrying edges both ways off Morphism.loc.start — tasks with task_max_loc < start are its deps (S29's fence, restated as dependencies), tasks with task_min_loc > start depend on it (the half that was missing). Without the second half the bracketed work was dispatched the moment its inputs were ready, while the host was still walking toward the read, so t1 - t0 measured an interval the work had already left: 6/100 threaded fir 65 536 runs read under 0.01 ms for a ~0.07 ms kernel; after, 0/100, values byte-identical and total wall time unchanged. The two edge sets are disjoint (max < start vs min > start) and a read is in neither of its own, so no clock edge can close a cycle; a read left on the spine inside an effectful loop region keeps its Checkpoint, which is the only fence it has. Evidence: the new path_time_ms_holds_back_the_work_written_after_it plus the two S29 clock tests restated against deps (the fence moved location, not meaning); 972 workspace tests green, crates/mapal-rt/ untouched. Previous — S29 time builtin + the two path_plan clock rules (plan-time-builtin, the mapal-ir half): Operation::TimeMs : IoToken → (IoToken × f64) — Core's second effect and its first clock read (34th variant): bare-token source (no internal pair — unlike print there is no value operand), target the (rebound token, monotonic ms) pair the caller projs apart; builder FnBuilder::time_ms, edge_type_ok twin + 5 §5.1 golden rows (1 legal, 4 rejected), mermaid label "TimeMs". I4/I4b/I5 gained no clause — a token-bearing target rides ty_contains_token unchanged, so a clock read threads exactly as a print does. The substance is in path_plan, where two bugs were found and fixed, both mutation-verified: (1) the fence — a TimeMs checkpoint now waits for the COMPLETION (threshold: None) of every task all of whose morphisms start before the read in the SOURCE (task_max_loc vs morph.loc.start). Source order, because the dataflow graph orders pure work against a clock read not at all — topo order legally (and actually) ran the bracketed work after the closing read; source position is what makes t1 - t0 the work written between the two reads, and what lets a bracket opened after data generation exclude it (the S28 conv2d gen/kernel finding). (2) the host cone — TimeMs is the first host-spine op producing a VALUE and not just a token; tasks are dispatched before the host writes it, so a task consuming a clock read raced the write and reported a NEGATIVE elapsed (FRAMEWORK §4.5 Law 1 — a transformation reading data not present at its location, a data teleport). The whole consumer cone of a clock read now stays on the spine (host_value/host_cone folded into is_host); the cone is scalar arithmetic in practice, a bulk op fed by a clock read is pinned sequential — correct before fast. Evidence: path_time_ms_fences_only_the_tasks_entirely_before_the_read (t0 fences the generation above it but not the kernel it opens; t1 fences both; neither fences the post-bracket readout) + path_time_ms_consumer_cone_stays_on_the_host_spine, over a shared time_bracket_fixture with ascending per-line spans, with path_plan_is_deterministic extended to it; time_ms_builds_and_validates/time_ms_rejects_non_token_source; +4 tests → 184 ir-suite (of which 64 in tests/algos.rs). DESIGN §5/§5.1/§8/§10 carry the op, §13 + the deduced-morphism table carry path_plan and its two rules (its IMPLEMENTATION row, missing since S24, is now written). Previous — S28 conv2d k-split recording (plan-s28-shapes-ladder work item A1, the mapal-ir half): TileRead gains the partial morphism ksplit? : TileRead → TileKSplit ({div, cq, cr} — the k = kq·div + kr decomposition of the fold's counted axis; read address base + ci·i + clane·lane + ck·k + cq·(k÷div) + cr·(k%div)), the fold-body analog of the map body's (t÷C, t%C) split one level down: tile_fold_shape binds a Div/Mod pair on the fold element (slot fold_captures + 1, one shared literal divisor, depth % div == 0 else the pair stays unbound and the site refuses) as kq/kr identity leaves in tile_affine; rule 1 ksplit.is_some() ⇒ ck == 0 (mixed raw/derived k refuses); pair bound but unused ⇒ ksplit: None, so matmul/fir records stay bit-identical, and conv2d_16 (benches/shapes/) now records its site (was refused on the raw sdiv/srem). Evidence: tile_conv2d_site_recognized (full-site assert — rows=16, c=16, k=9, a=w{ck:1, clane:0, ksplit:None}, b=img{ci:18, ck:0, clane:1, ksplit:Some{div:3, cq:18, cr:1}}) + refusal pins tile_refuses_conv2d_non_rectangular_window/tile_refuses_conv2d_divisor_mismatch/tile_refuses_conv2d_mixed_raw_and_derived_k; +4 tests → 180 ir-suite. Remaining ceilings live in backend-llvm (conv emission TI, im2col, emission branch selection); the ir-side ceiling — general ksplit with ck ≠ 0, needs a wider coefficient space, no measured demand — is suggestions #2. Previous — S25 tile emission WP-T1/T1b: tile_plan deduced query (plan-tile-emission — recognizes map{fold} sites whose cell chains may be interleaved bit-exactly: affine-triple reads TileRead{slot,base,ci,ck,clane} via a checked recursive walker, 2-D div/mod + 1-D lane modes, legality = one lane-invariant + one lane-stride-1 read, bounds_proof-proven indices, trap-free bodies with Call/nested-site refusal — the orchestrator-review R1 fix, DeadCall pin; suggestion #9 verified shipped-at-S20c and pinned bounds_matmul_fold_body_proven_through_captures; +11 tests → 176 ir-suite). Previous — S24 parallel orchestrator: path_plan deduced query (loop_plan's sibling — the execution graph's task DAG, backend-independent per the ratified plan-parallel-orchestrator: Task{Split|Seq, deps, rank, trap_min, pinned} + threshold Checkpoints/WaitEntry; token chain and effectful-loop regions stay host; transitive fn_trap_capabilities fixpoint attributes body/callee traps at the referencing site's topo; critical-path ranks; +12 tests → 165 ir-suite). Previous — S22 minimal-emission WP-A: emission_plan deduced query (EmissionClass::{Dissolved,Inline,Named} — the plan-minimal-emission §1 classification; dissolution Pair-built-only after the orchestrator review caught the Proj-produced-tuple silent count drop, an R-NODUP break; +9 tests → 153). S21 ADR-0029 stage 2/amendment: Operation::Widen (33rd Core variant — explicit numeric widening, lattice i32→i64 · i32→f32 · i32→f64 · f32→f64 validate-enforced, InvalidWiden builder/validate twins; builder widen(src, target, dest, loc) rides the family Dest contract) + fill_from(pair, dest, loc) (the replay entry — emits Fill from an EXISTING internal tuple, minting nothing; the S21 rewrite-fixpoint fix's ir half; same static-n rule, slot-1 feeder scanned via in_edges). S20: last_use_plan + bounds_proof deduced queries; Iota/Fill (stage 1) Spec references: category-ir.md §3 (IR data structures) + §5 (Graph representation) + CHANGES.md §1 (structural fixes: single-source/single-target morphisms, first-class Phi, loops as trace + LoopMerge, back-edges as real adjacency edges) + ADR-0013 / ERRATA LC-4 (dataflow-is-edges realization). Supporting: architecture.md §3. Authoritative design: DESIGN.md (this folder) — 3-way adversarially reviewed, then implementation 2-way reviewed + soundness-attacked + fix round, Session 04. plans/plan-last-use.md (query shipped). Depends on: (none — defines its own SourceLoc, D8) Depended on by: lower, check, interp, rewrite, backend-llvm, backend-cuda, backend-verilog, cli

What works

• Full Core graph IR per DESIGN §2–§15: slotmap arena (objects/morphisms/functions), SecondaryMap adjacency + owner maps, zero HashMap anywhere (I12 determinism).
• 34-variant Core Operation set (ADR-0013 + ADR-0018 + ADR-0021 + ADR-0029 incl. the S21 Widen amendment: scalar explicit widening, total/pure/trap-free, the four-edge lattice — i64→f64 deliberately excluded as not value-exact): per-slot Pair{slot,arity} product formation, Proj, arith/cmp/logic + Neg, Phi, Call, Map/Fold (bodies as non-first-class FuncDefs), Index, Update (array element write (Array,I,T)→Array, OOB traps like Index; ADR-0021), Zip/Enumerate (collection primitives, ADR-0018), Iota/Fill (array-construction primitives, ADR-0029 — iota(n) = [i32; n] of 0..n-1, count as a Constant source; fill(x, n) = [T; n], count as the internal 2-tuple's slot-1 Constant; both trap-free; static-n owned by the builder (NonStaticCount) and re-derived by validate (IotaCountMismatch twin)), Print, TimeMs (S29, plan-time-builtin — IoToken → (IoToken, f64), the monotonic-ms clock read; effectful, so the token thread already forbids reordering/const-folding/CSE/DCE), LoopEnter/LoopBack/LoopExit, Output.
• Builder with per-call typing (DESIGN §5.1 table), composite atomic primitives, typestate LoopHandle, Dest-mediated ret writes; seal() is the only producer of CategoryIr and re-checks everything global (I4/I4b tokens, I5 per-edge loop placement incl. carried-state-in-SCC, I6 acyclicity + StructNameConflict, I-RET, Str placement).
• validate(): independent re-derivation of every graph-shape clause (separate module, own helpers); module docs list the provenance clauses it cannot certify.
• Iterative Tarjan sccs(f), Kahn topo_order(f) (LoopBack emitted-not-gating, header-first; S12: LoopEnter deferred until no other morphism is ready — every multi-hop loop-invariant precedes its loop header, a theorem the interp driver and straight-line backends rely on; regression topo_orders_multi_hop_invariants_before_loop_enter), loop_structure(f) — the backend-verilog capability predicate (single-loop accept vs multi-merge reject shapes tested). S13: loop_plan(f, merge) -> Option<LoopPlan> — the per-merge canonical loop CFG (init/carried/decide/advance feeders + SCC-membership exit attribution), the one source of truth (BL7) that interp's run_loop, rewrite's is_canonical/replay, and backend-llvm all delegate to; None = non-canonical.
• S20: last_use_plan(f) -> LastUsePlan (plan-last-use §2, the deduced last_use query — BL7 pattern): per-object death positions (greatest topo position of any use, counting Pair/Phi retention pins — a packed handle lives as long as the product holding it), the conservative escape classification (rule 2: Parameters + reachability into Output/Return; the loop's own carried state — merge, Proj views, back-route state cone — is exempt through its own LoopExit, the per-iteration release valve), carried_by (rule 3: value crosses LoopBack into a merge), and dead_after(o, idx) (rule 4's in-place-Update predicate). Rule 1's ranking re-orders each canonical loop's morphisms to the quartet order decide < LoopExit < advance < LoopBack within their topo slots. Total and deterministic on any sealed fn; non-canonical loops degrade to the conservative fallback (rule 6). Consumers: backend-cuda in-place Update + back-edge freeing, backend-llvm Update elision, arena v1.1 coloring.
• S20: bounds_proof(f) -> BoundsProof (the deduced provably-in-bounds query — same BL7 pattern, one topo_order interval pass): unsigned interval ranges from Constants, Iota elements ([0, n)), enumerate indices (.0 of (i32, X) over n), literal-ramp arrays ([min, max]), and Map/Fold body quantification (a body's element param rides the site source's element range — iota / enumerate / literal-ramp). An Index is proven iff its index's range lies inside the array's static size; anything unknown, wrapping, negative-going, or loop-carried is NOT proven (consumers keep today's guards there — zero behavior change). The matmul-cell affine shape (i = t/4, j = t%4, a[i*4+j]) proves at size ≥ 64 and correctly refuses at 32. Consumers (W6): llvm guard elision (the vectorization unlock — the 36–115× znver2 gap), cuda guard + trap-param elimination on now-trap-free kernels.
• S38: topo_order ties break on source position — (loc.start, loc.end, insertion index), popped from a BinaryHeap<Reverse<…>> rather than a FIFO cursor. Trap order (and, since emission derives from the same walk, effect order) is therefore a function of the program rather than of arena insertion. Exact loc ties — a Parameter and Return sharing the function span, loop objects sharing the loop span — fall back to insertion order; none of those objects trap on their own, so the ordering they receive is unobservable. Consumers inherit it for free: the oracle walks topo_order (interp/src/eval.rs:101), sequential LLVM emits in that order, and the parallel runtime CAS-mins on the same topo index — which is why approach A was taken over changing the interpreter's selection key alone (that would need "oracle key == backend key" maintained across llvm/cuda/verilog forever).
• Deterministic Mermaid dump (§14 format: f{i}o{j} ids, quoted labels, single --> style, "LoopBack ↩" + ⟲ merge prefix) + lint_mermaid (label-stripping arrow scan).
• path_plan(f) -> PathPlan (S24 plan-parallel-orchestrator, backend-independent): the execution graph's task DAG — Task{Split{site,n}|Seq{morphisms}, deps, rank, trap_min, pinned} in first-topo-occurrence order + host-spine Checkpoints carrying WaitEntry{task, threshold} (Some(w) = watermark, None = completion) at every token op and at exit; token-bearing morphisms and effectful-loop regions stay host; fn_trap_capabilities is a transitive fixpoint attributed at each reference site's topo. Clock rules (S29, amended S36): a TimeMs is its own pinned task whose deps fence every task written entirely above it in the SOURCE (loc.start, not topo — the graph gives no order between pure work and a clock read) and whose dependents are every task written entirely below it, so the bracketed work cannot be dispatched before the read happens; a clock read's whole consumer cone stays on the spine (it is the first spine op producing a value, and pooled tasks are dispatched before the host writes it — FRAMEWORK §4.5 Law 1).
• IO-as-linear-token: Print/TimeMs chains, loop-carried tokens with the structural loop-fork I4 exception (forward-cone classification), token-sink I4b.

What does not / known issues

• Cross-builder id mixing is UB with no defense (DESIGN §10; pinned by cross_builder_funcid_mixing_is_unsupported_ub). The earlier "versioned-key defense" claim was disproven by review SND-2 — escalate to an ADR (builder nonce in id types) if a second constructing client ever appears. Flagged for Sapir.
• Well-formedness ≠ unique meaning: multiple unconditional full-value Return writers seal clean; exclusivity is mapal-check/interp's obligation (DESIGN §17).
• Deliberately out (P4/later): JSON serialization (§5.3), mutation/removal API (CSE/DCE need it; additive rewrites fit v1), bifunctor-image tagging (§9.5 — recomputable from adjacency).
• ValueTyMismatch is declared but unreachable via the public API (constant() derives ty from value) — kept as defense for future direct-value APIs, documented by test.
• Session 05 fix (lower design-review finding TY-1): zero-field Struct tys sealed clean but failed validate() with BadInEdges (a 0-component pack_struct minted an in-edge-less Temporary), breaching the headline "seal Ok ⇒ validate empty" property. Fixed two-layer: I9 intake now rejects zero-field Struct (NonCoreType, mirroring Tuple ≥2 / Array ≥1) and pack_struct(&[]) is EmptyProduct; +4 regression tests.

Invariants enforced (and where in code)

DESIGN §9 ledger I1–I12 + I-RET + I4b + I9s. Mapping: I1/I11 type-level (Morphism fields); I2 builder.rs per-call dispatch + validate.rs::edge_type_ok; I3/I-RET builder atomic primitives + check_i_ret + validate; I4/I4b builder.rs::check_token_linearity (seal) + validate (shared predicate ty::ty_contains_token, loop-fork via forward-cone BFS); I5 builder.rs::check_loops + validate.rs::check_loops (both test the carried state's SCC membership — route-object membership was proven insufficient, review F2/SND-1); I6 seal acyclicity (iterative DFS) + owner checks; I7 constant() sole setter; I8 ret-write API + validate graph-shape form; I9/I9s intake on declared and synthesized tys + seal check_str; I10 iterative depth-guarded Ty walks (MAX_TY_DEPTH=64); I12 storage discipline + tested determinism. S29's TimeMs adds no clause anywhere in this ledger: the token rules are keyed on ty::ty_contains_token and a (IoToken, f64) target is token-bearing like any other product, so linearity/sink/loop-escape all apply unchanged.

Test coverage (golden / property / differential / skipped+why)

184 tests green (cargo test -p mapal-ir --release, S29 — per-suite counts re-run this session: 78 unit · 64 algos · 24 builder_rejections · 14 golden Mermaid · 4 proptests; the per-suite content notes below predate S24/S25/S28/S29, so read the Last-updated line for what the newest rows cover; +4 S29 time — time_ms_builds_and_validates / time_ms_rejects_non_token_source (unit) and path_time_ms_fences_only_the_tasks_entirely_before_the_read / path_time_ms_consumer_cone_stays_on_the_host_spine (algos, both mutation-verified — reverting either path_plan fix fails its test), plus 5 TimeMs rows inside the §5.1 golden oracle and path_plan_is_deterministic extended over the bench-bracket fixture; +9 S22 emission_plan — 6 directed + the 128-case law proptest (codex WP-A) + 2 orchestrator R-NODUP regressions emission_nested_product_dissolution_is_pair_built_only / emission_proj_produced_tuple_fanout_is_named_not_dropped; +9 S20 last_use_plan, +7 ADR-0029, +7 bounds_proof; +2 S21 Widen — builder_rejections::invalid_widen_rejects, validate::widen_twin::invalid_widen_edge_flagged, plus the §5.1 typing-table golden gains the 4-legal/3-rejected Widen rows): 78 unit (rejection matrix — every reachable IrError variant driven + ty predicates; the §5.1 typing-table golden oracle typing_table_golden::edge_type_ok_matches_design_5_1, pinning validate's per-op typing judgment against the DESIGN §5.1 rows op-by-op — incl. Zip/Enumerate and the ADR-0021 Update rows; the ADR-0018 zip/enumerate happy-path + rejection tests; S13 update_builds_and_validates/update_non_array_rejects/update_index_not_int_rejects/update_value_elem_mismatch_rejects; the enumerate-bound twin enumerate_bound_twin::oversize_enumerate_edge_flagged; the ADR-0029 static-count twins iota_count_twin::{drifted_iota_count_flagged,drifted_fill_count_flagged}) · 24 builder_rejections integration (reviewer-named holes: Eq-on-Bool vs Lt-on-Bool, Str-in-product, SingletonTuple, RetNotProduct, LoopBackOutsideScc-with-real-guard, TokenInPhi nested, TokenNotEscaping, TokenDropped, StructNameConflict, oversize-array slots, cross-builder UB pin; + ADR-0029 static-count rejections iota_non_constant_count_rejects/iota_zero_count_rejects/iota_oversize_count_rejects/fill_of_str_rejects/fill_zero_count_rejects) · 14 golden Mermaid (the §16 graphs (a)–(i) incl. §4.5 two-route loop B=U and B≠U, fanout no-join vs join, print-inside-loop token-U, 3-way value-guard Phi chain; every snapshot hand-verified + linted; 2 lint-regression goldens) · 4 proptests (headline interleaved valid+invalid seal⇒validate-empty @256 — generator now also emits array-build/Zip/Enumerate steps so the new ops are covered by the headline property, positive generator @128, Str-bearing-ty property, determinism byte-identical dumps + identical topo/sccs) · 64 algos (SCC contents, cycle-breakers, topo ordering incl. body<LoopExit<consumers, nested multi-merge, 100k-chain no stack overflow — J1 — plus the S20 last-use rows: chain/diamond death positions incl. the use-less-object case, carried-pair matmul4-class (update result carried, merge source dead_after the update, cond never carried, decide<LoopExit<advance<LoopBack ranking), escape-via-pair-field, borrowed-init (Parameter feeding LoopEnter never dead — the consumer's borrowed veto), two-sequential-loops per-loop carried attribution (the S12 trap), determinism run-twice, non-canonical fused-loops graceful degradation + 100k-chain linear sweep totality; the mapal-rewrite testgen generator is NOT reachable from mapal-ir's tests — it imports mapal_interp, downstream of mapal-ir — so the plan §6.1 brute-force agreement row rides the consumers' differentials). Differential: n/a until interp (P3). Nothing skipped.

Performance notes (numbers + bench name + date; regressions flagged)

ir_scale (criterion, 2026-06-12): build+seal / to_mermaid / sccs — chain 1k: 0.60ms / 0.63ms / 0.070ms · chain 10k: 5.9ms / 6.5ms / 0.70ms · chain 100k: 65ms / 69ms / 7.9ms · grid 100k: 31ms / 29ms / 5.0ms. Near-linear O(V+E); to_mermaid was O(n²) in draft and fixed to O(V+E) during implementation.

Open questions (→ ADR candidates)

• Cross-builder id nonce (above) — ADR candidate if ever needed.
• Bifunctor-image tagging: revisit in rewrite's design (DESIGN §17).
• E3 frontier vs fanout-join boundary: if mapal-check needs the block boundary as data, escalate (DESIGN §17).
• Trap semantics (div/mod-zero, OOB) revert to Kleisli(Result) typing with Core+1 coproducts (ADR-0013).