verified-codegen-roadmap.yaml

# Verified Codegen Roadmap (ASPICE SWE.1 / SWE.2 — forward-looking program)
#
# System: Synth -- WebAssembly-to-ARM/RISC-V AOT compiler
#
# WHY THIS EXISTS
# The oracle-gated cleanup audit keeps reaching the same conclusion: the
# recurring greedy-fixes (reciprocal-mult cost-gates, the i64/temp
# register-exhaustion HARD-FAIL, and the "selector missed an op" bug class
# #223/#226/#232) are SYMPTOMS of two single-pass, hand-written components —
# the instruction selector and the register allocator. Each fix is locally
# correct and oracle-gated, but they accrete because the substrate forces them.
# A compiler-landscape research pass (Cranelift ISLE/Crocus, regalloc2/aegraph,
# CompCert/CakeML, Sail, WasmCert-Coq, equality saturation) identified the
# best-in-class structural cure. This file PLANS that cure as typed, phased,
# parallelizable requirements so the infrastructure can be built incrementally
# alongside the per-issue gale cadence WITHOUT a big-bang rewrite.
#
# All items are `proposed` — this is the backlog, not shipped work. Each carries
# a falsifiable kill-criterion (PulseEngine methodology). Behavior is frozen:
# every phase must keep the differential fixtures (control_step 0x00210A55,
# flat+inlined flight_algo 0x07FDF307, divseam 338/338) bit-identical and is
# gated by the existing oracle before merge.
#
# Format: rivet generic-yaml

artifacts:

  # ---------------------------------------------------------------------------
  # Program north-star
  # ---------------------------------------------------------------------------

  - id: VCR-001
    type: system-req
    title: Foundationally-verified, allocator-robust codegen core
    description: >
      Synth's code generator shall evolve from a hand-written single-pass
      selector + single-pass allocator into principled, foundationally-verified
      infrastructure, so correctness comes from construction rather than from an
      accreting set of locally-correct patches. The end state: (a) instruction
      selection is expressed as verified rewrite rules discharged against
      synth's Rocq integer/control-flow core, not open-coded match arms;
      (b) register allocation spills under pressure instead of hard-failing,
      eliminating the exhaustion that forces cost-gated fallbacks; (c) the
      target and source semantics the proofs rest on are the authoritative ISA
      (Sail) and Wasm (WasmCert) models; (d) the differential oracle is
      coverage-complete and theorem-linked. Migration is incremental and
      oracle-gated: every step keeps the frozen fixtures bit-identical.
    status: proposed
    tags: [codegen, verification, roadmap, north-star, real-compiler]
    links:
      - type: derives-from
        target: BR-001
      - type: derives-from
        target: BR-002
    fields:
      req-type: non-functional
      priority: should
      verification-criteria: >
        Over the program's lifetime: zero NEW cost-gate/fallback shortcuts
        added to the selector; the register-exhaustion hard-fail path is
        removed; the "selector missed an op" gale bug rate trends to zero; all
        frozen fixtures stay bit-identical at every step.
      rationale: >
        Antidote to the patch-accretion the cleanup audit repeatedly surfaces.
        Sources: Cranelift ISLE + Crocus (ASPLOS'24 SMT rule verification),
        regalloc2/aegraph, CompCert/CakeML (foundational lowering), Sail RISC-V
        (official Rocq export), WasmCert-Coq (FM'21).

  # ---------------------------------------------------------------------------
  # Track A — codegen core (sequential within: allocator first, then selector)
  # ---------------------------------------------------------------------------

  # PROGRESS (substrate, side-by-side / unwired):
  #  - reg_effect + per-segment dead-store/redundant-const analysis
  #    (synth-synthesis/src/liveness.rs)
  #  - CFG-aware liveness: cfg_liveness() builds the label-form basic-block CFG
  #    and solves per-block live-in/live-out via the backward dataflow fixpoint
  #    (the interference-graph substrate). Pure analysis, zero codegen callers,
  #    so every frozen fixture stays bit-identical by construction. Leaf-only,
  #    label-form scope; declines (None) on calls/offset/computed branches.
  #  - Interference graph: interference_graph() derives per-instruction liveness
  #    from cfg_liveness (backward from each block's live_out) and builds the
  #    undirected "cannot share a physical register" graph — defs interfere with
  #    everything live-after + with co-defs (Umull rdlo/rdhi). This is the
  #    colouring input. Still unwired. Exposes interferes/neighbors/degree.
  #  - Graph colouring: color_graph(graph, k) -> Colored(map) | Spilled(set) via
  #    Chaitin/Briggs simplify (push degree<k) + optimistic spill + select (lowest
  #    free colour; no colour => actual spill). THE allocation decision the
  #    single-pass allocator can't make (it hard-fails instead). Verified on real
  #    selector output: colourable within the R0-R8 pool (k=9). Still unwired.
  #  - Precolouring: color_graph_precolored(graph, k, pins) pins nodes to fixed
  #    colours (never simplified/spilled, only constrain neighbours) — the
  #    mechanism for synth's reserved regs (R9/R10/R11/R12) + ABI arg pins.
  #    color_graph() now delegates with empty pins. Still unwired.
  #  - Allocation verifier (wiring plan step 1): verify_allocation(graph, assign)
  #    -> Ok | Err(SameColor|Unassigned). The self-check the wired allocator runs
  #    on its own output before emitting (independent of color_graph => real
  #    cross-check / defense-in-depth). Verified to accept color_graph's own
  #    output on real codegen. Still unwired. Wiring plan:
  #    docs/design/vcr-ra-allocator-wiring.md.
  #  - Spill-cost ranking (wiring step 2): color_graph_precolored_costed picks
  #    the optimistic spill candidate by Chaitin's cost/degree (cost = def+use
  #    occurrence count via use_def_counts) instead of degree-only; the uncosted
  #    API delegates with all-costs-equal, reproducing the historic choice
  #    exactly. allocate_function now ranks by real counts. Pure, unwired,
  #    fixtures bit-identical (verified by cmp + full differential).
  #  - Range interference + colouring (step 3a, part 1): range_interference
  #    builds the adjacency over VALUE RANGES (vreg ids; dies-at-birth boundary
  #    deliberately non-interfering, co-defs always interfere) and color_ranges
  #    k-colours it via the chaitin_core now generic over node id (Reg for the
  #    physical graph, usize for vregs — type-parameter refactor, identical
  #    algorithm/tie-breaks). The spurious-physical-spill elimination is now
  #    unit-proven in miniature (r0 reused for 3 values -> 3 independent ranges
  #    -> colours at true pressure 4). Pure, unwired, fixtures bit-identical.
  #  - Spill-on-exhaustion retry (step 3b-lite, LANDED): the i32 register-
  #    exhaustion hard-fail ("all allocatable registers are live on the stack",
  #    alloc_temp_safe) is now recoverable — the backend retries the failed
  #    function once with spill_on_exhaustion, which always reserves the i64
  #    spill area and makes alloc_temp_or_spill spill the deepest stack value
  #    (reusing the #171 StackVal::Spilled reload-on-pop machinery) instead of
  #    failing. Bit-identity is STRUCTURAL: only functions whose first
  #    (unmodified) pass already failed ever reach the retry. Honest bound:
  #    the hard-fail shrinks, doesn't vanish — I64_SPILL_SLOTS=8 pool
  #    exhaustion, the i64 consecutive-pair site, and the call-result
  #    callee-saved site keep their Err. Oracle: high_pressure_i32.wat
  #    (fails on pre-3b main, compiles + unicorn-vs-wasmtime PASS now) +
  #    3 frozen fixtures sha256-identical.
  #    Remaining for VCR-RA-001 (CONSEQUENTIAL, changes emitted bytes, full
  #    differential gate): rename_def + apply_range_coloring (3a part 2) ->
  #    flag-gated re-allocation pass + measured flip -> full 3b virtual temps ->
  #    spill-code insertion -> wire-in + per-function flip where the
  #    differential proves no-regression -> delete a hard-fail site.
  - id: VCR-RA-001
    type: sw-req
    title: SSA-based register allocator with spilling (remove the hard-fail)
    description: >
      Replace the single-pass allocator (fixed R0-R8 pool, hard-fail on
      exhaustion at instruction_selector.rs:330/356/577/4667) with an
      SSA/liveness-based allocator that spills under pressure (regalloc2-class:
      live ranges, spill/reload, coalescing). This is the FIRST track item
      because the exhaustion hard-fail is what forces the reciprocal-mult
      cost-gate (v0.11.20) and the 2-temp UMULL path; removing it lets those
      shortcuts be reverted toward the clean form. Must keep the reserved-reg
      architecture (R9 globals / R11 mem-base / R12 IP-scratch) and the
      bounds-mode R10 invariant.

      LOCAL-PROMOTION SCOPING SPIKE (2026-06-24, #390, scripts/repro/
      local_promotion_headroom.py): the structural gap to native parity is that the
      SELECTOR lowers every wasm local to a frame slot (`compute_local_layout` →
      LocalGet/Set/Tee emit `ldr/str [sp,#off]`), so locals never reach this
      allocator. Measured cost+pressure on the frozen fixtures: flight_algo 22% of
      instructions are local sp-traffic (25/109) from just 4 DISTINCT slots;
      control_step 2 slots, filter_step 3, controller_step 1. Distinct slots (1–4)
      are far below the allocatable pool (R0–R8 minus result/scratch ≈ 6–7), so on
      these fixtures EVERY local fits in a register with NO SPILLING — the spill
      path (the historically bug-prone part, #193→#226) is never exercised; the
      built `color_graph`/`color_ranges` colour a ≤4-node graph trivially. CONCLUSION:
      selector-side local promotion is HIGH headroom (≈22% removable on the hot fn)
      + LOW risk (no-spill at this pressure), and is the right next parity lever —
      more tractable than a general allocator rewrite. The spike script asserts the
      no-spill scope and fails loudly if a fixture ever exceeds the pool (then the
      spill path + its risk return).

      LOCAL-PROMOTION v1 (2026-06-24, #390, PR #458): the spike's lever, LANDED.
      Keep eligible non-param i32 locals in callee-saved registers (r4..r8) instead
      of frame slots. Behind SYNTH_LOCAL_PROMOTE (default off ⇒ frame path
      bit-identical, frozen gates green). Reuses the #193 param-reservation
      machinery (seed local_to_reg before the param_regs snapshot) rather than a
      new allocator. Scope v1: i32 only, write-before-read only (read-before-write
      = #457), dominance via control-flow depth-0, cost-gated, budget r4..r8 with
      frame overflow, and LEAF-ONLY (declines functions with calls — the
      post-selection range-reallocator can remap a callee-saved home to a
      caller-saved reg that a bl would clobber; lift once VCR-RA-003 is shown to
      reject that remap). Validated: flag-on local_promote_i32 fixture (7 live
      locals → 2 overflow, dirty r4..r8/frame sentinels) clean==dirty==wasmtime;
      control_step 0x00210A55 + flight_seam 0x07FDF307 preserved; flight_seam
      sp-traffic 39→5, .text 902→798 B. ARM-only (RV32 untouched). The default-on
      flip is a separate gated step (re-freeze + G474RE silicon), like cmp→select.

      LEAF-ONLY LIFT — REALLOCATOR-SAFETY PROBE (2026-06-24, #390, fast-follow #1):
      the empirical question the leaf-only gate was set on — can the post-selection
      range-reallocator move a promoted local's callee-saved home to a CALLER-saved
      register that an intervening `bl` would clobber? RESOLVED: NO, by construction.
      reallocate_function FLUSHES its segment at every non-straight-line op
      (liveness.rs:2341), and `Bl` has reg_effect→None, so a call SPLITS segments;
      the pre-call segment's live-out (the cross-call value) is its last-opened
      range per register ⇒ PINNED to its original register (liveness.rs:2371). The
      reallocator never renames across a call. Pinned by the unit test
      `reallocate_function_preserves_callee_saved_value_across_call` (constructs the
      exact promotion+call shape under interior pressure; r5 stays r5, not remapped
      to a caller-saved reg). This is the specific mechanism the v1 advisor flagged;
      it is safe. HONEST REMAINING GAP before lifting the gate: this validates the
      reallocator pass in isolation; the LIFT still needs an end-to-end WITH-CALL
      differential (flag-on execution oracle over the full selector-seed +
      preserve_caller_saved + realloc pipeline, like local_promote_i32) before the
      gate comes off — flag-off stays bit-identical, but flag-on for call-containing
      functions is new codegen wiring = a SEPARATE gated step, not an idle-tick
      change. This pass landed only the frozen-safe probe + finding.

      LEAF-ONLY LIFT — END-TO-END GAP CLOSED EMPIRICALLY (2026-06-24, #390,
      fast-follow #1 cont.): the with-call fixture scripts/repro/
      local_promote_cross_call.wat (exported `cross_call` holds an i32 local `acc`
      live across a `bl` to `$helper`; acc satisfies every v1 promotion predicate
      except leaf-only). With leaf-only ON it compiles byte-IDENTICAL flag-on vs
      flag-off (promotion declines — the gate holds end-to-end, frozen-safe). Under
      a THROWAWAY leaf-only lift (experiment reverted, NOT committed), promotion
      runs on the call fn and objdump confirms the FULL pipeline is correct: acc is
      promoted to r4 (`mov r4,r3`), survives the `bl func_0` by AAPCS, and is read
      back from r4 AFTER the call (`adds r6,r4,r0`) — NOT remapped to a caller-saved
      reg, exactly as the #459 reallocator-isolation proof predicted. So the
      end-to-end with-call promotion is correctness-ready. REMAINING to lift the
      gate (the byte-changing gated step, NOT this tick): make the committed lift PR
      (a) remove the leaf-only early-return, (b) add a with-call EXECUTION
      differential (resolve the internal BL, run flag-on vs wasmtime) as the gate,
      (c) re-freeze + G474RE silicon. This pass landed the frozen-safe fixture +
      finding; flag-off bit-identical, no codegen change.

      STACK-FWD + FRAME-SLOT-DCE FLIP TO DEFAULT-ON (#242 feature loop): the two
      paired lowering passes — `forward_stack_reloads` (a `local.set; local.get`
      reload `ldr rY,[sp,#N]` whose value still lives in `rX` becomes `mov rY,rX`)
      and `eliminate_dead_frame_stores` (the now-dead `str rX,[sp,#N]` whose slot is
      overwritten-before-read is removed) — shipped flag-off in PR #514/#515 and are
      now DEFAULT-ON. Escape hatch `SYNTH_NO_STACK_FWD=1` restores the frame-resident
      bytes. Gated exactly like the cmp→select (v0.13.0) and local-promotion
      (v0.14.0) flips: RESULTS re-verified bit-identical on every frozen anchor
      (control_step 0x00210A55 13/13; flat AND inlined flight_algo 0x07FDF307 —
      flight_seam_differential.py MATCH both) while .text shrank on the SHIPPED
      --relocatable path (flight_seam 774→738, flight_seam_flat 910→878; control_step
      unchanged — no spurious slot reuse; signed_div_const + all RV32 unchanged,
      ARM-only). Frozen goldens re-frozen + an escape-hatch gate asserts the opt-out
      restores the pre-flip bytes. SOUNDNESS: overwrite-only DCE (dead only when a
      later store to the same immediate slot overwrites it with no intervening read;
      reaching the function end does NOT count), sub-word sp accesses (ldrb/ldrh/…)
      as blockers (advisor-caught #483-class hole, test verified failing pre-fix); 8
      unit tests pin the boundaries. Instruction/memory proxy: flight_algo sp-traffic
      20→7, 139→135 insns — the measured CYCLE number is gale's G474RE (post-ship
      confirmation, the cmp→select silicon-gate-waiver precedent). Broad oracle:
      `cargo test --workspace` green under the new default (wast/spec suite is
      compile-only, so gale silicon is the broad-execution check). NOT flipped:
      const-CSE (SYNTH_CONST_CSE) stays flag-off — its alias-eviction prerequisite is
      open and it is inert on flat_flight. NO-REGRESSION FIX (#242, 2026-06-26): gale's
      v0.17.0 burndown found const-CSE GREW a `--relocatable` `gust_mix` 90→92 B (the
      post-hoc `apply_const_cse` retargeted a use, kept a constant resident longer, and
      defeated a downstream immediate-fold). Fixed by running `apply_const_cse` LAST in
      the pass pipeline (after every immediate-fold, so foldable consts are already
      gone) plus a per-segment SIZE GUARD (commit a segment's removals/retargets only
      when they do not grow its estimated bytes — e.g. a retarget flipping a 16-bit
      `ldr` to 32-bit is declined). Guard decline path proven non-vacuously by two
      contrasting liveness unit tests; per-function no-regression gate added to
      `const_cse_differential.py`; flag-off byte-identical (frozen gate green). The
      pressure/size prerequisite for the eventual default-on flip is now CLOSED;
      alias-eviction remains the sole open prerequisite. (Not empirically reproduced on
      gale's exact `gust_mix` — fixture requested to pin the trigger.)
    status: verified
    release: v0.24.0
    tags: [codegen, register-allocation, ssa, regalloc2, track-a, release-v0.11.40]
    links:
      - type: derives-from
        target: VCR-001
      # Bootstrap-verification wiring: the SSA allocator is the structural
      # satisfaction of the two STPA code-generation constraints that the
      # single-pass allocator violates by construction (H-CODE-1).
      - type: constraint-satisfies
        target: SC-CODE-1
      - type: constraint-satisfies
        target: SC-CODE-2
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        control_step + flight_algo + a high-pressure i64 module compile with no
        hard-fail; all frozen fixtures bit-identical; cycles equal-or-better;
        the reciprocal-mult cost-gate becomes revert-able with no regression.

  - id: VCR-SEL-001
    type: sw-req
    title: Rocq-discharged verified instruction-selection DSL
    description: >
      Express lowering as a rule DSL (`lower(op) = [target seq]`) whose
      well-formed rules emit Rocq proof obligations auto-closed by the existing
      synth_binop_proof / synth_comparison_proof / synth_unop_proof tactic
      family — "ISLE with a proof-assistant backend": foundational discharge,
      not Crocus-style per-rule SMT, and unlike CompCert it is a reusable rule
      DSL rather than monolithic hand-proofs. Replaces the open-coded selector
      match arms incrementally (one op-class at a time, behind the oracle). This
      structurally kills the "selector missed an op" bug class (#223/#226/#232):
      a missing rule is a coverage gap the DSL can enumerate, not a silent
      miscompile. Depends on VCR-RA-001 landing first (a verified rule that
      can't be allocated is not yet correct end-to-end).

      FIRST MEASUREMENT (2026-06-20, coq/Synth/Synth/VcrSelPilot.v, built green
      via //coq:vcr_sel_pilot, 7 Qed / 0 Admitted): the go/abandon question is
      whether the existing synth_binop_proof tactic family still auto-discharges
      once a rule is lifted from fixed R0/R1 to universally-quantified registers.
      Two-tier result. (A) NO-SCRATCH single-instruction i32 binops
      (Add/Sub/Mul/And/Or/Xor): 6/6 auto-discharge UNCHANGED — synth_binop_proof_poly
      is verbatim synth_binop_proof modulo the lowering-unfold target; one Qed per
      op covers every aliasing (universal over rd/rn/rm). (B) SCRATCH-USING
      multi-instruction op (Rotl = RSB scratch + ROR): generalizes too but NOT for
      free — needs an explicit rs<>rn scratch-non-aliasing side condition (the
      fixed-register proof's `discriminate` on R0<>R2 becomes a real hypothesis
      the DSL must carry and feed the allocator) plus a per-shape proof. CONCLUSION:
      DSL viable; auto-discharge "for free" is ~100% only for the no-scratch class,
      and the DSL must model scratch non-aliasing — exactly why SEL depends on
      RA-001. NOT YET MET: the >=70%-per-attempted-rule over the FULL integer
      pilot (div/rem trap-control-flow tail unmeasured), and the bit-for-bit
      selector match (this is a discharge measurement, not a wired DSL — generates
      no Rust, replaces no selector arms). Also: the lemmas carry but do not USE
      the wasm hypotheses (pre-existing T1 property — they prove "ARM computes the
      named result", not "ARM refines the WASM op").

      CONTROL-FLOW OP CLASS GATED ON VCR-ISA-001: the measurement is complete for
      the straight-line classes (no-scratch binops generalize free; scratch ops
      need the rs<>rn non-aliasing constraint). The TRAP-GUARDED ops (i32 div/rem)
      are NOT a register-generalization question at all — their fixed-register
      proofs are already Admitted (coq/STATUS.md), blocked upstream by the flat
      exec_program's no-op BCondOffset (see VCR-ISA-001). So div/rem SEL coverage
      depends on VCR-ISA-001's real-control-flow executor, not on this track.

      MOTIVATION-1 RE-SCOPED — "selector missed an op" silent-drop is already
      structurally closed (measured 2026-06-20). The original framing ("a missing
      rule is a silent miscompile the DSL enumerates away") is now only partly a
      DSL job, because the existing selectors no longer silent-drop:
        - ARM select_default (instruction_selector.rs:1799→4189) is an EXHAUSTIVE
          match over WasmOp with NO `_ =>` wildcard (the SIMD and
          MemoryCopy|MemoryFill arms `return Err`). A newly-added WasmOp variant is
          a COMPILE error, not a silent NOP — exhaustiveness checking IS coverage
          enumeration for ARM. select_with_stack's `_ =>` (10057) delegates to
          select_default, so every op is Ok-or-typed-Err: no drop path.
        - RISC-V selector.rs:911 `other => Err(SelectorError::Unsupported(op))` is a
          RUNTIME typed loud-skip — kills silent WRONG-CODE but, unlike ARM, is not
          compile-checked, so a new op silently DIVERGES (loud-skipped on RV32,
          lowered on ARM) rather than failing the build.
        - Clean split of the cited #223/#226/#232 class: the REGALLOC subset (#226
          alloc_temp live-value clobber) is owned by VCR-RA-001 and already landed;
          the OP-GAP subset (#223/#232 "RV32 rejected ops ARM handles") is NOT a
          silent drop — it is a CROSS-BACKEND PARITY gap (ARM lowers X; RV32
          loud-declines X) that no oracle covers today and gale, not a gate, caught.
      So VCR-SEL-001's remaining value is NOT silent-drop prevention (the compiler
      + typed-Err terminals own that). It is: (i) correctness-by-construction of the
      lowering rules; (ii) collapsing the two/three-selector accretion
      (select_default / select_with_stack / optimizer_bridge) into one verified
      source; and (iii) cross-backend op-parity — the concrete near-term increment,
      tracked as VCR-SEL-005 below.

      FIRST INCREMENT SCOPE (2026-07-03, docs/design/vcr-sel-001-first-increment.md):
      (1) OP FAMILIES: exactly the pilot's tier-A no-scratch single-instruction
      i32 ALU class — Add/Sub/Mul/And/Or/Xor, the measured 6/6 auto-discharge
      set — plus, as the increment's stretch (proves the DSL can carry side
      conditions), ONE scratch-using shape (i32.rotl: RSB scratch + ROR) with
      the explicit rs<>rn non-aliasing hypothesis. Excluded from increment 1:
      trap-guarded div/rem (Admitted upstream, gated on VCR-ISA-001's real
      control-flow executor), i64 pairs, memory, control flow, and everything
      the optimized path (select_with_stack/optimizer_bridge) does — the DSL
      targets select_default's arms only.
      (2) COEXISTENCE: the DSL is a checked-in rule table
      (declarative op -> parameterized ARM sequence) + a generator emitting
      plain Rust lowering fns committed to the tree (reviewable, no build-time
      magic); select_default KEEPS dispatch ownership — a migrated op's match
      arm delegates to the generated rule behind SYNTH_SEL_DSL (default off),
      unmigrated arms untouched. OFF ≡ baseline byte-identical by construction.
      (3) ROCQ OBLIGATION PER RULE: one universally-quantified T1 theorem per
      rule in the VcrSelPilot.v form — forall rd rn rm (+ scratch hypotheses
      where the shape needs them), exec of the rule's emitted sequence yields
      the op's I32 semantics in rd — auto-discharged by synth_binop_proof_poly;
      rule<->theorem naming is 1:1 and a coverage check fails the //coq build
      if a rule lacks its Qed (a rule without a theorem cannot merge).
      (4) FROZEN-ANCHOR GATE for the flip: per-op mirror-pinning first (the
      #511/#513 pattern — a test lowers the probe set through BOTH the
      hand-written arm and the generated rule and asserts byte-equality, so the
      two must-agree implementations are pinned before any flip); then
      SYNTH_SEL_DSL=1 must keep control_step 0x00210A55, flat+inlined
      flight_algo 0x07FDF307, and divseam bit-identical (the generated rules
      reproduce the current lowering EXACTLY — increment 1 migrates structure,
      never bytes); only then may the flag default flip, one op-class per
      release, full differential green. Success criterion for increment 1: the
      six ALU arms + rotl are served from the DSL with their seven Qed theorems,
      fixtures bit-identical, and deleting a hand-written arm body becomes a
      no-op — the first structural (not additive) step of the migration.

      INCREMENT 1 LANDED (2026-07-07, flag-off): the checked-in rule table
      (crates/synth-synthesis/src/sel_dsl/mod.rs RULES, 7 rules: tier-A six +
      rotl with SideCondition::NotAlias(Rs, Rn)) + generator emitting committed
      plain-Rust lowerings (sel_dsl/generated.rs, pinned rustfmt-stable by
      generated_lowering_is_up_to_date); select_default's seven arms delegate
      behind SYNTH_SEL_DSL (default OFF ⇒ original hand-written body,
      byte-identical by construction). Rocq: coq/Synth/Synth/VcrSelRules.v —
      7 Qed / 0 Admitted, 1:1 rule<->theorem naming, tier-A discharged by
      synth_binop_proof_poly verbatim, rotl by the pilot's stepped proof with
      the rs<>rn hypothesis. Coverage gate wired: //coq:verify_proofs is now a
      test_suite = rocq_proofs + vcr_sel_rules_coverage (manifest
      coq/vcr_sel_rules.manifest pinned to RULES by a cargo test; missing
      theorem or non-Qed proof fails the //coq gate CI runs). Gate 1 evidence:
      per-op mirror-pin
      (sel_dsl_mirror_pin_generated_rules_match_handwritten_arms_242) asserts
      hand-written ≡ generated ArmOp sequences for all 7 rules; frozen
      byte-gate green with the flag OFF (by construction) AND with
      SYNTH_SEL_DSL=1.

      INCREMENT 2 LANDED (2026-07-08, flag-off,
      docs/design/vcr-sel-001-increment-2.md): +14 rules = 21 total, each with
      its 1:1 Qed (21/21, 0 Admitted, 0 holdout theorems). (a) i32 register
      shifts shl/shr_s/shr_u + rotr — measured TIER-A (single instruction, NO
      scratch; the inc-1 side-condition machinery turned out unneeded for
      shifts, remains exercised by rotl alone), discharged by the same
      synth_binop_proof_poly; delegated in BOTH selectors (Delegation::Both),
      byte-identical. (b) The ten i32 comparisons — the CMP+SetCond shape,
      modeled per the Compilation.v convention as CMP; MOV rd #0; MOVcc rd #1;
      NO aliasing side conditions (CMP latches NZCV before rd is written, so
      the universal quantifier admits every aliasing); 7/10 discharged by
      synth_cmp_binop_proof_poly (synth_cmp_binop_proof generalized to
      universally-quantified registers) + the same three manual scripts
      (ne/lt_s/lt_u) as their CorrectnessI32.v ancestors, register-generalized
      verbatim. DELEGATION HONESTY: comparisons delegate in
      select_with_stack's reg-reg arm (the load-bearing CMP+SetCond emission,
      byte-identical by construction; the #258 imm-fold peephole stays
      hand-written on both flag settings, pinned) because select_default's
      comparison arms are a blind bare-Cmp lowering that never materializes
      the 0/1 result — production-unreachable AND unprovable as T1
      result-correspondence, so they stay hand-written (the increment's
      documented holdout; this choice also keeps the flip strictly
      byte-invisible). Mirror-pins:
      sel_dsl_mirror_pin_generated_rules_match_handwritten_arms_242 (the 11
      select_default-delegated rules) +
      sel_dsl_mirror_pin_select_with_stack_rules_byte_identical_242 (the 14
      select_with_stack-delegated rules, with a non-vacuity window check that
      the delegation actually fired) +
      sel_dsl_cmp_imm_fold_path_stays_handwritten_and_byte_identical_242.
      INCREMENT 3 LANDED (2026-07-08, flag-off,
      docs/design/vcr-sel-001-increment-3.md): +6 rules = 27 total, each with
      its 1:1 Qed (27/27, 0 Admitted, 0 holdouts among attempted rules). The
      i64 register-pair family — add/sub/and/or/xor (two-instruction pair
      shapes ADDS+ADC / SUBS+SBC / ANDx2 / ORRx2 / EORx2 over SIX register
      variables rd_lo..rm_hi) + eqz (single I64SetCondZ). Chosen deliberately:
      the #615/#632/#633/#643/#599 miscompile cluster is all hand-written i64
      paths, zero bugs in DSL-covered ops. MODEL FINDING: the Rocq flat model
      needed ZERO extension for pairs — ADDS/ADC carry coupling +
      combine_i32/lo_of_i64/hi_of_i64 have carried the pair convention since
      v0.8.0; the increment is the pilot's fixed-to-universal register lift
      applied to CorrectnessI64.v's ancestors. SIDE-CONDITION DESIGN (the
      #632 lesson made structural): each pair rule carries THREE explicit
      aliasing hypotheses (rd_hi<>rd_lo, rd_lo<>rn_hi, rd_lo<>rm_hi — the
      low-half write must not clobber the high-half operands still to be
      read, and the high write must not destroy the low result), runtime
      Ok-or-Err in the generated Rust; in-place rd=rn reuse (select_default's
      fixed R0:R1 op= R2:R3) is deliberately admitted, so one Qed covers both
      selectors. Theorems are pair-result T1: BOTH words proven
      (rd_lo=lo_of_i64, rd_hi=hi_of_i64 post-conditions), discharged by
      synth_i64_carry_pair_proof_poly (via the existing i64_add_via_adds_adc
      / i64_sub_via_subs_sbc, no new axiom) and
      synth_i64_bitwise_pair_proof_poly (combine lemmas imported from
      CorrectnessI64, not duplicated); eqz via i64_setcondz_bits_spec.
      Delegation::Both — select_default fixed-register arms + the
      select_with_stack allocated-pair arms (alloc_consecutive_pair's
      extra_avoid satisfies the side conditions by construction). Mirror-pins:
      the select_default loop now covers 17 rules; the dedicated
      sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242 probes i64-typed
      stacks with the RMW-vacuity window check;
      i64_pair_side_conditions_are_enforced pins all three Errs per rule.
      FLIP LANDED (default-on): with all 40 rules mirror-pinned
      byte-identical, the SYNTH_SEL_DSL default-on flip shipped — the DSL is
      now the SHIPPED lowering path for its 40 covered ops (opt-out
      SYNTH_NO_SEL_DSL=1, CI-gated to the hand-written path). The flip was
      byte-invisible by construction: the frozen 10/10 anchors did not move
      (frozen_codegen_bytes), the mirror-pins stayed green, and the broad
      default-vs-opt-out differential was bit-identical across all 88
      compilable scripts/repro fixtures — on the default (optimized), the
      --relocatable (select_with_stack, the path the DSL rules ship on) AND
      the --no-optimize paths — including flight_seam(_flat), controller_step,
      filter_axis and signed_div_const; the 2 flag-gated fixtures
      (gust_mix_686, spill_on_exhaust_242) fail identically on both paths.
      Status stays `implemented` (NOT `verified`): the flip
      clears exactly the default-flip item; still NOT done (hence not
      verified) — i64 mul/div/shifts/rotates/comparisons (I64SetCond) +
      optimizer_bridge + the remaining select_with_stack families; div/rem
      (VCR-ISA-001-gated).
    status: implemented
    tags: [codegen, selector, isle, verified-dsl, rocq, track-a, novel, release-v0.12.1]
    links:
      - type: derives-from
        target: VCR-001
      - type: constrained-by
        target: VCR-RA-001
      - type: constrained-by
        target: VCR-ISA-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        A pilot op-class (e.g. i32 arithmetic) is fully expressed as DSL rules
        with >=70% auto-discharged by existing tactics (kill-criterion: below
        70% it collapses into "CompCert with extra syntax" — abandon); the
        generated lowering matches the current selector bit-for-bit on all
        fixtures. CALIBRATION (Crocus, ASPLOS'24 deep-research 2026-06-10):
        the SMT state of the art hit ~88% per-attempted-rule on the Wasm 1.0
        integer subset but needed 136-182 manual annotations (~1000 LOC),
        custom VCs for 6 rules, timeouts on wide mul/div/rem/popcnt, and its
        verified rules covered only 19.8% of dynamically-invoked rules — so
        measure the criterion PER-ATTEMPTED-RULE on the integer pilot, budget
        for annotations, and do NOT promise full-selector coverage. A rule DSL
        is an enabler, not a prerequisite: CompCert verifies selection
        functions directly, and synth's existing T1 tactic suite
        (synth_binop_proof family vs exec_indexed) IS that direct path — the
        DSL pays off only when rule count amortizes its cost.

  - id: VCR-SEL-005
    type: sw-req
    title: Cross-backend op-parity oracle (ARM / RISC-V / AArch64)
    description: >
      A test-time gate (crates/synth-backend-riscv/tests/cross_backend_op_parity.rs)
      that lowers self-contained, minimally-valid WasmOp sequences on ALL THREE
      shipping selectors — ARM (Thumb-2), RISC-V (RV32IMAC) and AArch64 (A64) —
      and asserts integer-core PARITY against ARM as the reference: an op the ARM
      selector lowers must be lowered-or-explicitly-ledgered by the RV32 selector
      (`cross_backend_integer_op_parity_242`) and by the aarch64 selector
      (`aarch64_integer_op_parity_851`). NOTE the backend count: this description
      said "BOTH the ARM and RISC-V selectors" until v0.55 (#893) — it has spanned
      three backends since v0.53 (#883). This is the concrete near-term increment
      of VCR-SEL-001: the
      VCR-SEL-001 pilot measurement (2026-06-20) established that "selector missed
      an op" is no longer a silent miscompile (ARM select_default is an exhaustive
      WasmOp match; RV32 ends dispatch with a typed Unsupported Err), so the
      residual #223/#232 risk is purely cross-backend DIVERGENCE — ARM lowers op
      X, RV32 loud-declines it, and the function silently compiles on one target
      and is skipped on the other. Historically that gap was found only by gale on
      qemu; this oracle surfaces it as a gate.

      The ledger (KNOWN_DIVERGENCES) is bidirectional: a NEW divergence not in the
      ledger fails the build (a fresh op-gap, owned here not on silicon), and a
      ledgered divergence that has CLOSED also fails (a stale entry the fix must
      delete) — so a parity claim cannot outlive the gap it documents, and a
      landed RV32 lowering is forced to retire its ledger line.

      FIRST MEASUREMENT (2026-06-20, first run): the oracle found FIVE
      ARM-lowers / RV32-declines integer op-gaps, all the Zbb bit-manipulation
      class — i32.rotl, i32.rotr, i32.clz, i32.ctz, i32.popcnt. RV32IMAC and
      rv32imc (incl. ESP32-C3) do not include Zbb, so there is no single native
      instruction; ARM lowers them via sequences (ROR/CLZ/RBIT, and a software
      sequence for popcount which ARMv7-M also lacks natively), proving they are
      sequence-lowerable on RV32 too (as Select already is). Recorded as tracked
      deferrals under this requirement. NOTE the i64 bit-manip analogues
      (i64.clz/i64.popcnt) came back at PARITY — not flagged. SCOPE: integer core
      only; float (VFP) and SIMD (Helium) parity is a separate, large, known gap
      and is intentionally NOT asserted by this oracle.

      FOLLOW-UP (the work this oracle drives): implement the five RV32 sequence
      lowerings, each differential-validated against wasmtime per the established
      bug-loop discipline; landing each one retires its ledger entry via the
      stale-entry check.

      COVERAGE WIDENING (2026-06-24, frozen-safe test-only increment): the curated
      set grew from ~50 to 76 probes — now NEAR-EXHAUSTIVE over the integer core:
      the i32 compare set completed (gt_u/le_s/le_u/ge_s), the FULL i64 compare set
      added (ne + signed+unsigned lt/gt/le/ge), i64 shr_s/rotl/rotr/ctz, all four
      i64 div/rem, the sub-word i64.extend{8,16,32}_s, and i64.load/i64.store. ALL
      26 new probes came back at PARITY (verified both-Ok, not vacuous both-Err) —
      ZERO new divergences; the ledger stays exactly the five i32 Zbb deferrals.
      Floor raised 30→65. This widens the net for the #223-class cross-backend gap
      (gale would otherwise hit it on qemu) over div/rem, the full compare lattice,
      and i64 memory — none of which were previously probed. ASYMMETRY FOUND:
      i64.rotl/i64.rotr LOWER on RV32 (sequence-composed in the i64 path) while
      i32.rotl/i32.rotr are ledgered RV32-declines — evidence the i32 Zbb rotate
      deferral is closable by routing i32 rotate through the same shift+or sequence
      the i64 path already uses (sharpens the FOLLOW-UP's first target; byte-changing
      codegen, gated — NOT in this test-only increment).

      UNIVERSE-COMPLETENESS UPGRADE (2026-07-17, #49, frozen-safe test-only): the
      oracle was hardened from a CURATED integer probe list (whose vacuity trap is
      that a new WasmOp variant is silently never probed) to a COMPILER-ENFORCED
      universe-complete gate. Every WasmOp variant is now assigned a ParityClass by
      a NO-WILDCARD match (classify()); a new op fails to COMPILE until classified
      (the #615 no-wildcard tripwire). Integer-core ops carry a probe and are
      asserted; float/f64/SIMD are StructurallyExcluded with a written reason —
      their ARM lowering is TARGET-PARAMETERIZED (measured: f32.add DECLINES with
      fpu=None, LOWERS with FPUPrecision::Single/Double; f64.add needs Double), so
      asserting "ARM lowers float" at a fixed no-FPU probe would be FALSE; float/SIMD
      parity stays a separately-tracked gap. Enumerating the FULL universe surfaced
      SIXTEEN previously-unprobed ARM-lowers / RV32-loud-declines one-sided gaps
      (each confirmed END-TO-END via `synth compile -b riscv`, "unsupported wasm op
      for RV32 skeleton: …"): global.get, global.set, memory.size, memory.grow,
      memory.copy, memory.fill, br_table, and the nine sub-word i64 loads/stores
      (i64.load8_s/u, i64.load16_s/u, i64.load32_s/u, i64.store8/16/32 — the
      full-word i64.load/i64.store DO lower on both; only the sub-word extend/
      truncate variants are the gap). All sixteen are now ledgered VCR-SEL-005
      RV32-selector DEFERRALS (a gated, owned fact instead of a silicon surprise) —
      the KNOWN_DIVERGENCES ledger is now 5 Zbb + 16 new = 21 entries. RED-FIRST
      non-vacuity is now a first-class companion test
      (red_first_unledgered_one_sided_gap_is_caught): it drops the real i32.rotl
      ledger entry and asserts the gate reports it as an unexpected divergence on
      the REAL backends (no synthetic op, no shipping-code change). A
      ledger-liveness test guards drift. The gate is now WIRED as a named CI job
      (vcr-sel-005-cross-backend-op-parity-gate) so a regression is visible on its
      own failing check.

      FOLLOW-UP EXPANDED: the RV32 sequence-lowering backlog this oracle drives now
      also covers globals, the memory intrinsics (size/grow/copy/fill), br_table,
      and the sub-word i64 memory variants — each landing retires its ledger line
      via the stale-entry check.

      THIRD BACKEND (v0.53, #883/#851): aarch64 joined the same no-wildcard
      enumeration. Before that its only breadth check was 25 hand-written probes,
      so "what does aarch64 not lower?" had no mechanical answer and gap-picking
      was guesswork. The aarch64 leg (`aarch64_integer_op_parity_851`, ledger
      `aarch64_known_divergences`) enumerated TWENTY ARM-lowers/aarch64-declines
      integer-core gaps on first run; each decline names the missing selector arm
      AND the A64 instruction that would implement it, so the ledger reads as a
      work plan rather than an absence. Thirteen closed in the same release
      (`select` via CSEL/FCSEL, `drop`/`nop`, `i32.wrap_i64`,
      `i64.extend_i32_{s,u}`, the five `extend8/16/32_s` forms, fixed-memory
      `memory.size`/`memory.grow` — selector 148 -> 161 ops, gale's matrix 35 ->
      45); v0.54 closed `global.get`/`global.set`. aarch64 also gets what ARM and
      RV32 structurally cannot have: a probed FLOAT/SIMD surface
      (`a64_extended_surface`, floor `probed >= 100`). Float is
      `StructurallyExcluded` from the ARM/RV32 leg because ARM float lowering is
      TARGET-parameterized (f32.add DECLINES at fpu=None, LOWERS at
      Single/Double) and RV32 has no FPU — but the aarch64 backend has ONE fixed
      host profile, so both directions are assertable there, and a stale "gap"
      claim is caught the same way a stale divergence is.

      LEDGER STATE (2026-08, keep in step with the arrays — a drifting count is
      the #893 class this oracle exists to prevent): ARM<->RV32 18 entries
      (5 Zbb + 16 universe-completeness − `memory.size`/`memory.grow` closed
      v0.50 − `br_table` closed v0.53 #882); ARM<->aarch64 5 entries — br_table,
      `local.set`+get on a PARAM local, `local.tee` on a PARAM local (two
      separate entries, both the leaf-function param-homing prerequisite),
      memory.copy, memory.fill — after v0.54 closed `global.get`/`global.set`.
      Non-vacuity floors: `at_parity >= 65` (RV32),
      `at_parity >= 60` (aarch64), `probed >= 100` (aarch64 extended surface).
      Both legs carry their own red-first companion
      (`red_first_unledgered_one_sided_gap_is_caught` drops the real i32.rotl
      entry; `red_first_unledgered_aarch64_gap_is_caught` does the same on the
      aarch64 leg) and their own ledger-liveness test.
    status: implemented
    tags: [codegen, selector, riscv, aarch64, parity, oracle, track-a, release-v0.11.51, release-v0.53, synth-883, synth-893]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-SEL-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        All EIGHT tests in cross_backend_op_parity.rs are green: every WasmOp
        variant is classified by a no-wildcard match (universe-complete by
        construction — a new variant fails to COMPILE until classified, the #615
        tripwire), and every integer-core probe is at parity with ARM on BOTH the
        RV32 and the aarch64 leg OR carries a reasoned ledger entry. The
        at-parity floors (>=65 RV32, >=60 aarch64 common-core ops; >=100 probed
        on the aarch64 extended float/SIMD surface) guard against a construction
        regression that would let "everything errors" masquerade as parity. Each
        leg carries its own red-first companion proving non-vacuity on the REAL
        backends — red_first_unledgered_one_sided_gap_is_caught surfaces the real
        i32.rotl gap once its ledger entry is removed, and
        red_first_unledgered_aarch64_gap_is_caught does the same for aarch64 — and
        a ledger-liveness test per leg guards drift. Stale entries fail too, in
        both directions: a divergence that has CLOSED reddens the gate until its
        line is deleted, so a parity claim cannot outlive the gap it documents.
        CI-wired as vcr-sel-005-cross-backend-op-parity-gate.

  - id: VCR-A64-CF-001
    type: sw-req
    title: AArch64 multi-way dispatch (br_table) + value-carrying structured control flow
    description: >
      The VCR-SEL-005 third-backend enumeration (#851) is a MECHANICALLY DERIVED
      complement: whatever the aarch64 selector does not lower is named, by op,
      in `aarch64_known_divergences()` and in the `a64_extended_surface` gap
      column. After v0.53/v0.54 closed the integer core, the floats, globals and
      `call_indirect`, the TWO LARGEST remaining entries in that complement were
      structural, not arithmetic:

        (a) `br_table` — the multi-way branch. Declined outright ("aarch64
            selector has no BrTable arm"), so any wasm switch/jump-table shape
            skipped the whole function on `-b aarch64`.
        (b) VALUE-CARRYING `block`/`loop`/`if` — a typed (`(result T)`) frame.
            Declined because the straight-line value-stack model had no
            RESULT-REGISTER RECONCILIATION: two paths reaching one `end` leave
            the result in path-dependent temps. This is the #509 block-arity
            class, and it is what makes `(block (result i32) … br_if …)` — the
            shape every non-trivial optimizing producer emits — uncompilable.

      THIS REQUIREMENT closes both, with the residual named rather than widened:

      br_table lowers as a COMPARE-AND-BRANCH CHAIN, deliberately the same
      construction #882 chose for RV32 so the two backends stay reviewable
      against each other: `cbz w_idx, L0` for entry 0, then `cmp w_idx, #i` +
      `b.eq L_i` per further entry, then an unconditional `b L_default`. The
      index is compared in the W view, so the i32 UNSIGNED semantics hold
      exactly: only 0..len-1 match, and every other index — including the
      "negative" i32s that are huge unsigned values — falls to the default
      label, per WASM core semantics. Targets may mix FORWARD (block/if end,
      patched at `End`) and BACKWARD (loop header, resolved eagerly to a
      negative offset) destinations in one table, since the chain dispatches on
      the TARGET FRAME's kind exactly like `br`/`br_if` already do.

      Value-carrying frames get a RESERVED RECONCILIATION REGISTER PAIR (one GP,
      one FP — the file is not known from the arity side-table, which carries
      counts only) allocated at frame entry and withheld from the temp
      allocator for the frame's whole extent. Every path that reaches the
      frame's label MOVES its result into that register before transferring:
      `br` and `br_if` at the branch, the then-arm at `else`, the fall-through
      at `end`. At `end` the frame pushes the reserved register as the frame's
      value, so the result is in ONE register on every path by construction —
      the reconciliation the old decline said was missing.

      SOUNDNESS-CRITICAL DISTINCTION (named because getting it wrong is a silent
      miscompile, not a decline): a `br` to a `loop` targets the loop HEADER and
      carries the loop's PARAMETER count, NOT its result count. So a
      `loop (result i32)` — arity (0,1) — must NOT reconcile on its back-edge;
      its reserved register is written only by the fall-through `end`. The frame
      therefore carries `label_arity` (= params for Loop, results for Block/If)
      SEPARATELY from `result_arity`, and branch reconciliation is driven off
      `label_arity`. Reconciling the back-edge would deposit a garbage value
      into the result register on every iteration.

      HONEST RESIDUALS (loud declines with machine reasons, each pinned by name
      in `br_table_subshape_asymmetry_882` so the gap claim cannot outlive the
      gap, and each MOVED not deleted):
        * `br_table` past BR_TABLE_MAX_TARGETS (16) — the chain is O(n); a real
          jump table (PC-relative dispatch + bounds check) is the follow-up.
          Same threshold and same decline as RV32 #882.
        * `br_table` with VALUE-CARRYING targets — a per-path result move would
          have to sit on the taken edge of each compare, which the flat chain
          has no room for. Conservatively refused when any targeted frame
          (default included) has non-zero label arity or was entered at a
          different height than the post-pop height.
        * block/loop/if with PARAMETERS, or with MORE THAN ONE result
          (multi-value) — the reserved pair is a single slot.
      Frozen-safe by construction: a VOID frame reserves nothing and emits no
      reconciliation move, so all pre-existing aarch64 control-flow output is
      byte-identical.
    status: implemented
    tags: [codegen, selector, aarch64, control-flow, parity, track-a, issue-851]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-SEL-005
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        (1) The aarch64 leg of the op-parity gate no longer ledgers `br_table`
        as an ARM-lowers/aarch64-declines divergence, and the stale-entry check
        proves it (the gate reddens if the line survives the lowering).
        (2) `br_table_subshape_asymmetry_882` asserts the THREE aarch64
        residuals by name in both directions: a 17-target table declines, a
        value-carrying table declines, and the probed in-scope shape LOWERS.
        (3) Execution-differential vs wasmtime under unicorn (and natively on an
        arm64 host): br_table default arm, index at the table bound, index over
        the bound, index 0xFFFFFFFF, a table mixing loop and block targets, and
        a value-carrying loop's back-edge — plus a trap case, so the gate cannot
        collapse to "everything returns a value".
        (4) The pre-existing void control-flow differentials stay green with
        UNCHANGED output (no spurious reconciliation move on a void frame).

  # ---------------------------------------------------------------------------
  # Track B — authoritative semantics (independent; parallel with Track A)
  # ---------------------------------------------------------------------------

  - id: VCR-ISA-001
    type: sw-req
    title: Re-base ARM/RISC-V semantics on Sail-generated Rocq
    description: >
      Replace the hand-written ARM (ArmSemantics.v) and RISC-V execution models
      with definitions imported from the official Sail ISA models (the RISC-V
      Sail model exports to Rocq today; ARM-ARM is machine-readable ASL),
      restricted to the RV32IMAC / Thumb-2 slice synth targets, and re-prove the
      integer core against them. Collapses a major TCB component: "verified
      against the authoritative spec" becomes a defensible claim. Independent of
      Track A — can proceed in parallel.

      GATES THE TRAP-GUARD ADMITS (found via the VCR-SEL-001 pilot, 2026-06-20):
      the current hand-written ArmSemantics.v exec_program is a FLAT sequential
      executor with no program counter — BCondOffset is a literal no-op
      (ArmSemantics.v ~715, "No-op in sequential model"). So every trap-guarded
      lowering (CMP; BCondOffset; UDF; <op> — i32 div/rem, the 4 i32_div*/rem*
      admits + their i64 analogues, the bulk of coq/STATUS.md's 9 admits) CANNOT
      be discharged: the model can't express "skip the UDF when the divisor is
      non-zero". A real-control-flow executor (PC-indexed, which a Sail-derived
      model supplies natively) is the precondition. This also gates VCR-SEL-001
      coverage of the control-flow op class (div/rem) — straight-line and
      scratch-using ops generalize without it, control-flow ops do not.

      FEASIBILITY SPIKE DONE (2026-07-08, docs/design/vcr-isa-001-spike.md):
      the 2026-06-10 gate is answered. Tool: VERIFIED alive (Sail 0.20 via
      nixpkgs ships --coq, bbv|stdpp styles; coq-sail maintained). Generated
      ARM model IMPORT: REFUTED as a build path — sail-arm arm-v9.4-a covers
      all of T32/A32 (instrs32.sail) but its Coq snapshot is a single 42 MB
      armv9.v pinned to stdpp-unstable + git-pinned coq-sail-stdpp (the 2019
      v8.5 snapshot needed ~40 GB RAM on Coq 8.9.1) — incompatible with the
      hermetic Rocq 9 Bazel toolchain and CI. WORKING ALTERNATIVE LANDED:
      per-instruction transcribe-and-bridge — coq/Synth/ARM/SailArmBridge.v
      (in //coq:verify_proofs, 23 Qed / 0 Admitted) hand-transcribes
      AddWithCarry + the AArch32 ADD/CMP register-form execute clauses from
      sail-arm @ 1bf2e5574ba9 with file:line provenance, and proves
      ArmSemantics.v's ADD/ADDS/CMP ≡ the transcription on registers AND all
      four NZCV flags (the six hand-written compute_*_flag definitions equal
      ASL's AddWithCarry outputs — the foundation under every CMP-based
      comparison lowering). Abstraction gaps documented in-file: shift_n=0,
      d<>15 (no PC — the executor gap above is NOT closed by the bridge and
      stays this item's core prerequisite), no IT blocks, bits(32) as Z mod
      2^32. Measured cost: flag machinery proven once (~230 lines incl.
      reusable mod-case/testbit/NOT helpers + blast tactics); remaining
      AddWithCarry family (SUB/SUBS/CMN/RSB) near-free, ~0.5-1 day per
      remaining straight-line op class; memory ops widest gap (byte-addressed
      Sail memory vs Z->I32 model). RISC-V half unmeasured — sail-riscv's
      maintained Coq export may admit the import path there; re-evaluate
      separately.

      ROUND 2 LANDED (2026-07-08, same day): the spike's priority items (1)
      and (2) + the moves stretch — SailArmBridge.v now 81 Qed / 0 Admitted /
      0 new axioms covering the FULL AddWithCarry family (ADD/ADDS/CMP +
      SUB/SUBS/CMN/RSB + ADC/SBC with live-C carry_in — the i64 pair-codegen
      primitives), flag-free ALU (AND/ORR/EOR/MVN), all four shifts in
      immediate (1..31) and register (0 < amt < 32; amt = 0 on the unsigned
      view) forms via a faithful Shift_C transcription incl. shifter
      carry-out, and MOV/MOVW/MOVT. Measured cost ~0.5 day for six-plus
      classes (well under the spike's per-class estimate; the flag-machinery
      amortization held). BONUS FINDING: the bridge surfaced two latent
      hand-model divergences from the ASL (LSR/ASR #32 and register shift
      amounts >= 32 — unreachable from Compilation.v since WASM masks to
      0..31), documented in-file as gaps 6-7 — the exact bug class this item
      exists to surface. Still open (why not implemented): PC-indexed
      executor (the trap-guard admits, this item's core motivation),
      MUL/UMULL/CLZ/RBIT/memory/branches, and the whole RISC-V half.
    status: approved
    tags: [semantics, sail, isa, trust, rocq, track-b, unblocks-admits]
    links:
      - type: derives-from
        target: VCR-001
    fields:
      req-type: non-functional
      priority: could
      verification-criteria: >
        The i32 Tier-1 theorems re-discharge against the Sail-generated Rocq
        target model for the supported instruction subset; if the Sail state
        monad makes the proofs intractable to port, fall back to using Sail
        emulators as a differential oracle (kill-criterion / partial credit).
        GATE ADDED (deep-research 2026-06-10): substrate freshness is
        UNVERIFIED — no claim about 2025-26 Sail-Rocq export maturity for the
        Thumb-2/RV32IMAC integer slice survived adversarial verification. A
        bounded feasibility SPIKE (can the Sail RV32 Rocq export build + one
        instruction's semantics be related to ArmSemantics/RiscvSemantics?)
        must precede any release commitment.
        GATE ANSWERED for the ARM half (spike 2026-07-08, evidence
        docs/design/vcr-isa-001-spike.md + coq/Synth/ARM/SailArmBridge.v):
        one instruction family bridged end-to-end with Qed proofs; criterion
        for the item REVISED accordingly — re-discharge is per-instruction
        transcribe-and-bridge against provenance-pinned Sail source, not
        against an imported generated model. RV32 export build remains
        unmeasured (the spike's ARM no-go on import does not transfer).
        STATUS proposed -> approved (2026-07-08): two landed increments
        (23 then 81 Qed, //coq:verify_proofs green) validate the revised
        criterion's method on the i32 straight-line integer core; approved
        means the approach is committed, NOT that the item is implemented —
        the PC-executor refactor, memory ops, and the RISC-V half remain.

  - id: VCR-WASM-001
    type: sw-req
    title: Anchor source semantics on WasmCert-Coq
    description: >
      Map synth's hand-written WasmSemantics.v stack machine onto WasmCert-Coq
      (the mechanized Wasm spec, FM'21) as the authoritative source semantics,
      and prove the frontend decode/validate refines it — giving the
      verified-source -> verified-lowering -> verified-target triangle (with
      Sail at the bottom via VCR-ISA-001). The Component Model layer stays an
      open problem (no mechanized semantics yet) and is explicitly out of scope
      for this item. Independent of Track A.
    status: implemented
    tags: [semantics, wasmcert, source, rocq, track-b]
    links:
      - type: derives-from
        target: VCR-001
    fields:
      req-type: non-functional
      priority: could
      verification-criteria: >
        synth's core-Wasm reduction relates to WasmCert-Coq's for the
        integer/control-flow fragment; kill-criterion: if the semantic gap is
        too large to relate without a major proof, scope to that fragment only.
        GATE ADDED (deep-research 2026-06-10): WasmCert-Coq maintenance state
        is UNVERIFIED (no surviving claim) — same bounded feasibility spike
        required before release commitment.

        BOUNDED FIRST INCREMENT LANDED (v0.45, VCR-WASM-001). The WASM-side
        analogue of SailArmBridge.v (VCR-ISA-001): coq/Synth/WASM/
        WasmCertReference.v transcribes WasmCert-Coq's i32.add operational rule
        (= CompCert Int.add, repr(unsigned x + unsigned y)) into synth's I32
        primitives with line-level provenance; WasmCertBridge.v proves (2 Qed,
        real — not reflexivity) that synth's exec_wasm_instr I32Add refines
        that INDEPENDENT reference. Non-vacuous: the reference is phrased only
        in repr/unsigned/Z, never I32.add/exec_wasm_instr, so a wrong add
        semantics fails the proof; the raw-vs-normalized (Zplus_mod) gap is
        genuinely discharged. SCOPE: 1 op, establishing the pattern.
        FOLLOW-UP (status stays implemented, not verified, until then): a real
        external WasmCert-Coq/CompCert coq dependency into the hermetic
        bazel/nix toolchain (the transcription is the bounded scaffold), plus
        the full integer/control-flow fragment.

        PHASE 2 (v0.47): real-dependency FEASIBILITY SPIKE result — nix-level
        FEASIBLE, bazel-level DEFERRED on three named blockers. Evidence:
        coqPackages.wasmcert (coq9.0-wasm-2.2.0) EXISTS in the exact nixpkgs
        commit the rules_rocq_rust toolchain pins (88d3861a) and nix-builds
        GREEN against the same Rocq 9.0.1 (verified 2026-07-17), propagating
        coq-ext-lib 0.13.0, mathcomp-boot 2.5.0, parseque 0.3.0, flocq 4.2.1,
        compcert 3.16 — the phase-1 "drags mathcomp+CompCert, no-go" wording
        is obsolete. Blockers for wiring it into bazel: (1) rules_rocq_rust
        has NO generic extra-coq-package hook — coqutil/hammer/smpl are
        hard-coded attrs across extensions.bzl + toolchain.bzl + rocq.bzl, so
        a fork change (or a large MODULE.bazel patch) is required; (2)
        LICENSE: nixpkgs wasmcert 2.2.0 depends on CompCert 3.16, license
        inria-compcert (meta.license.free = false) — an unfree dep in the
        default CI proof toolchain needs an explicit allowUnfree opt-in and a
        project policy decision; (3) upstream WasmCert-Coq 2.2.1 (master,
        coq >= 9.0 & < 9.2) DROPS the coq-compcert dependency entirely, so
        waiting for the next nixpkgs wasmcert bump removes blocker (2) for
        free. Verdict: land the ruleset extra-package hook + take the dep when
        wasmcert >= 2.2.1 reaches nixpkgs. Meanwhile phase 2 batch-extends the
        transcription bridge: the full i32 arithmetic/bitwise/shift + eqz +
        compare family (19 ops), each transcribed from the PINNED
        coq9.0-wasm-2.2.0 sources (numerics.v / operations.v line-level
        provenance, CompCert 3.16 lib/Integers.v for the underlying ops) with
        a real-Qed refinement lemma per op in WasmCertBridge.v.

        PHASE 3 (v0.48, #242): the extra-coq-package HOOK is LANDED — blocker
        (1) is CLOSED; the dep stays PENDING on blockers (2)+(3). Delivered as
        patches/rules_rocq_rust_extra_coq_pkg.patch (applied via the existing
        MODULE.bazel git_override patch list): a new
        `rocq.extra_coq_package(name=, attribute_path=)` bzlmod tag that emits
        one nixpkgs_package per declaration (exposing `:vo` compiled artifacts +
        `:sources`), letting a module pull an arbitrary coqPackages.<attr> from
        the pinned nixpkgs into the hermetic Rocq toolchain WITHOUT forking the
        ruleset — the generic mechanism the coqutil/hammer/smpl hard-coded attrs
        lacked. The hook is INERT as shipped: NO extra_coq_package tag is
        declared, zero repos are emitted, //coq:verify_proofs stays GREEN and
        the 536 Qed are untouched. The REAL WasmCert-Coq dep is NOT wired,
        because it is refused by CI's no-unfree-dependency policy: re-verified
        2026-07-17 by nix eval against pin 88d3861a — coqPackages.wasmcert is
        version 2.2.0 (meta.license MIT, free) but PROPAGATES coqPackages.
        compcert 3.16 (meta.license inria-compcert, meta.license.free = false,
        meta.unfree = true), and wasmcert 2.2.0's Int32 IS CompCert's
        Integers.Make, so compcert cannot be dropped from the 2.2.0 build graph.
        wasmcert >= 2.2.1 (which removes the CompCert dep) is NOT yet in the
        pin. REMAINING WORK to retire the transcription (all mechanical once a
        pin ships wasmcert >= 2.2.1): (a) bump the nixpkgs pin in
        rules_rocq_rust to a rev carrying wasmcert >= 2.2.1 — removes blockers
        (2)+(3); (b) uncomment the `rocq.extra_coq_package(name="rocq_wasmcert",
        attribute_path="coqPackages.wasmcert")` tag + `use_repo` in MODULE.bazel;
        (c) swap WasmCertBridge.v's `Require Import Synth.WASM.WasmCertReference`
        for a `Require` of the real WasmCert numerics/operations modules and
        delete WasmCertReference.v. Until (a) lands upstream, the transcription
        stays — the "trusted transcription" caveat is NOT yet retired.

        PHASE 3 TRANSCRIPTION BATCH (#242): while the real dep stays blocked, the
        hand transcription is EXTENDED to the i64 integer family (22 ops:
        add/sub/mul/and/or/xor/shl/shr_u/shr_s/rotl/rotr/eqz/eq/ne/lt_u/lt_s/
        gt_u/gt_s/le_u/le_s/ge_u/ge_s), from the SAME pinned coq9.0-wasm-2.2.0
        sources — arithmetic/bitwise/shift/compare cite the same generic Make
        functor lines as i32 (read at wordsize 64, Int64 at numerics.v:1038-1039);
        the two rotates newly cite CompCert 3.16 Integers.v:217-222 (rol/ror).
        Each op has a real-Qed op-level refinement lemma; the 16 ops WIRED in
        exec_wasm_instr (shifts + rotates + 11 comparisons (incl. eqz)) also get an
        executor-level Qed. NAMED RESIDUAL (not forced): i64 add/sub/mul/and/or/xor
        have op-level refinement ONLY — exec_wasm_instr returns None for those
        constructors (unwired in the model), so no executor-level lemma is
        claimed; wiring them is a semantics-model change, out of scope for a
        transcription batch. Rocq Qed total 536 -> 585 (WasmCertBridge.v 49 -> 98);
        the rotate proofs discharge a genuine n=0 boundary gap (synth re-normalizes
        the [64-n] sub-shift count while the reference's is raw, reconciled via
        lor-idempotence at the boundary). Still a hand transcription — the caveat
        stands.

  # ---------------------------------------------------------------------------
  # Track C — validation methodology (can start now; feeds Tracks A and B)
  # ---------------------------------------------------------------------------

  - id: VCR-ORACLE-001
    type: sw-req
    title: Coverage-guided, theorem-linked differential oracle
    description: >
      Evolve the frozen-fixture differential into a coverage-complete,
      proof-aware suite: (1) coverage-guided fixture generation over wasm inputs
      (libFuzzer/AFL-style) instead of hand-picked vectors; (2) MC/DC-style
      coverage on the selector/lowering rules; (3) prioritize fixtures on ops
      NOT covered by a Tier-1 theorem, and re-frame the suite as the empirical
      witness that the hand-written ARM/RISC-V model matches silicon (validating
      the proof's assumptions). Can start immediately and feeds every other
      track.
      FIRST SLICE LANDED (2026-06-23): the frozen-fixture BYTE gate
      (`crates/synth-cli/tests/frozen_codegen_bytes.rs`) — compiles each frozen
      fixture flag-off and asserts a locked SHA-256 of its `.text`, on BOTH
      backends: ARM (control_step / flight_seam / flight_seam_flat /
      signed_div_const) and RV32 (control_step / signed_div_const — the rv32imac
      skeleton's import-call gap excludes flight_seam; scoped to fixtures with a
      `_riscv_differential.py`). The RISC-V backend is an INDEPENDENT codegen path
      with its own miscompile history (#220/#223/#226), so the ARM gate gave it
      zero protection. Promotes the
      previously OUT-OF-CI "stay bit-identical" invariant (asserted only by the
      `scripts/repro/*_differential.py` unicorn scripts, never run by cargo CI nor
      the Renode bazel suite) into a cargo-CI gate. It is the LOCALLY-VERIFIABLE
      complement to the python differentials (derivable + checkable with `cargo
      test`, no emulator) — guards against ACCIDENTAL drift (e.g. the open
      dependabot wasmparser 0.248->0.252 / wat bumps shifting decode). SCOPE BOUND:
      this proves byte-IDENTITY, NOT result-identity — it is NOT the execution
      differential the VCR-SEL-004 default-on flip owes (that flip deliberately
      changes these bytes and must prove the RESULT survives; this gate will
      correctly FAIL it and demand a deliberate re-freeze).
      EXECUTION SLICE LANDED (2026-06-23, #452): the first RESULT-identity
      execution differential now runs in cargo CI — `scripts/repro/
      cmp_select_two_move_differential.py` executes the two-move select fixture
      under unicorn (ARM Thumb, faithful IT-block predication) flag-off vs flag-on
      vs wasmtime, 11/11 result-identical, gated as an ISOLATED `cmp-select-oracle`
      job. This CORRECTS an assumption above: the execution harness does NOT need
      "a qemu-system binary CI lacks" — unicorn is a CPU emulator pip-installable
      in an isolated job (unicorn/wasmtime there only, so `cargo test --workspace`
      is untaxed by the C-lib build graph); synth-qemu's full-system shell-out is
      NOT the path. CI GOTCHA worth carrying: `synth disasm`'s symbol-table text
      output formats differently ubuntu-vs-macOS, so symbol-parse-based fixture
      lookup is fragile — read the function entry from the ELF directly (`.text`
      offset 0 for single-function fixtures, or pyelftools `.symtab` for
      multi-function) instead. STILL PROPOSED (the bulk): coverage-guided fixture
      generation, MC/DC rule coverage, the theorem-LINKED result-identity
      differential (the #452 slice is result-identity but not yet theorem-linked),
      and generalizing the execution harness beyond the single cmp-select fixture
      (the existing `*_differential.py` already validate control_step 0x00210A55 /
      flight_seam etc. locally but are not yet CI-wired — though for FROZEN fixtures
      that is redundant with the byte gate, so the value is in NON-frozen / flag-on
      paths the byte gate cannot cover).
      RV32 LEVER-BASELINE SLICE LANDED (2026-06-25, #472/#484/#485): the RISC-V
      lever port (porting the ARM perf levers to `synth-backend-riscv`) is the next
      perf track, scoped frozen-safe in `scripts/repro/riscv_lever_parity_472.md`
      (#484) and given its oracle in `crates/synth-backend-riscv/src/selector.rs`
      (#485). The RV32 path has NO cargo byte-gate beyond the frozen-fixture SHA
      (control_step / signed_div_const only) and no local RISC-V disassembler, so
      three `*_baseline_472` selector tests PIN the current pre-lever RV32 codegen
      at the RiscVOp-stream level: const-address store NOT folded (`add _,s11,addr;
      sw v,0(t)`), constant shift uses register `sll` not `slli #shamt`, non-param
      i32 local frame-spilled not register-homed. Each is green today (frozen-safe,
      asserts what the selector emits now) and FLIPS when its lever lands default-on,
      so a codegen change on the un-byte-gated RV32 path surfaces as a deliberate,
      reviewed assertion update rather than silent drift. Scoping finding that
      reshaped the port: cmp->select is N/A for RV32IMAC (no conditional-move / no
      IT-predication; `lower_select` is already the minimal branchy form), so the
      port is local-promotion + immediate-shift-fold + a RISC-V-specific
      const-address-fold (the base is already pinned in s11 — #468's base-hoist half
      does not exist on RV32), NOT a 1:1 port of the three ARM levers. The
      byte-changing lever implementations remain SEPARATE gated steps (each flag-off
      -> RV32 execution differential -> qemu_riscv32/ESP32-C3 cycle gate -> flip).
      DRIVER-CLASS FRONTIER — NON-LEAF THIN-FORWARDER PROLOGUE (2026-06-25, #428):
      a measurement pass on thin-seam driver primitives (a leaf that forwards
      through a single imported call) surfaced a gap the arithmetic levers do not
      reach: such a forwarder still emits the full `push {r4-r8,lr}` + frame even
      though it touches no callee-saved register. ROOT CAUSE (verified in source):
      the prologue-shrink levers `shrink_callee_saved_saves` (default-on) and
      `elide_dead_frame` (VCR-RA-002 dead-frame, flag-off) both DECLINE on any
      function containing a call — `reg_effect` returns None on `Bl`, and the pass
      bails rather than reason past the clobber boundary, so they are effectively
      leaf-only. A distinct lever — non-leaf thin-forwarder prologue minimization
      (a function that calls but writes no callee-saved register and reserves no
      live frame collapses its save-set/frame to `{lr}`, or tail-calls) — is the
      piece that reaches I/O-bound driver code; it does not exist yet. The two
      companion driver-class residuals are already tracked: redundant adjacent
      `str [sp,#N]; ldr [sp,#N]` is `forward_stack_reloads` (#455, built, flag-off
      behind `SYNTH_STACK_FWD`, awaiting the on-silicon flip), and the
      materialized-boolean-then-branch (`setcc; cmp #0; bCC`) is the already-deferred
      `br_if`->predicated-branch half of the cmp->select item (split candidate).
      All three are SEPARATE gated steps (flag-off -> differential -> silicon),
      never an idle-tick increment.
      LEVER IMPLEMENTED, BLOCKED ON A BASE-SELECTOR CLOBBER (2026-06-25, #490): the
      non-leaf prologue lever was implemented flag-off (relax `elide_dead_frame` +
      `shrink_callee_saved_saves` across DIRECT calls; 9 unit tests:
      even-count/8-byte-aligned push, keeps callee-saved held across a call,
      declines on indirect/non-8/live-frame). Its execution differential then
      proved the shrink's soundness is NON-LOCAL — pruning a forwarder's save-set
      is only correct if every callee preserves r4-r8, which the OPTIMIZED PATH
      does not: `alloc_i32_scratch` hands out the callee-saved [R4..R8] pool to
      every function with a scratch temp and the path emits NO callee-saved push,
      so even the silicon-validated `control_step` clobbers r4/r6/r8 (masked only
      because it is top-level / its callers fall back to the pushing direct
      selector). This is a SYSTEMIC base-selector ABI bug (#490), not a small-leaf
      special case — the scratch pool is shared, so fixing it (push-what-you-use in
      the optimized path) re-freezes control_step/filter_step and needs gale
      re-validation. NOT a live miscompile in shipped firmware (gale ships
      `--relocatable`, which uses the direct selector that preserves r4-r8
      correctly); it is a latent optimized-path violation that BLOCKS this lever's
      flip. The lever stays unmerged (branch wip/nonleaf-prologue-blocked-on-leaf-clobber,
      the differential = repro) until #490 lands. This is a "correctness from
      construction" item (the north star itself) and gates the perf lever
      downstream of it.
      RESOLVED + BROADER OPTIMIZER-BRIDGE CONTROL-FLOW FRONTIER (2026-06-26,
      #490/#483/#500): #490 LANDED (PR #495) — the optimized path now wraps any
      body that genuinely touches r4-r8 in `push {r4-r8,lr}` / `pop {r4-r8,pc}`,
      decided on the POST-realloc body (only genuinely-clobbered regs saved, so a
      cs-free leaf never gets a spurious permanent push; >4-param functions
      decline to the direct selector, so the inserted push cannot perturb
      incoming stack-arg offsets — verified byte-identical to `--no-optimize`),
      gated by `scripts/repro/callee_saved_490_differential.py` (r4-r8 sentinels +
      result vs wasmtime, covering the 16-bit push and the 32-bit PUSH.W
      high-register form). The non-leaf thin-forwarder prologue lever this blocked
      is now unblocked for a deliberate flip. A companion optimized-path
      control-flow miscompile LANDED the same arc (#483, PR #497): a forward
      `block`+`br_if` branch landed mid-instruction — two causes, the closing
      `End` labelled with its OWN id instead of the id of the block it closes (so
      the `br_if` resolved against an id no label held, left as the unpatched
      offset-0 placeholder), plus a `byte_offsets` size estimate that sized
      `Strh`/`Strb`/`Ldrh`/`Ldrsh`/`Ldrb`/`Ldrsb` as 2 when the high-base
      optimized path emits the 4-byte `.w` form — gated by
      `scripts/repro/block_brif_483_differential.py` (linear-memory diff vs
      wasmtime, both branch directions, forward + nested blocks). A multi-modal
      control-flow SWEEP then established these are ONE CLUSTER of optimizer_bridge
      (optimized-path) control-flow / ABI defects — the concrete measured evidence
      for VCR-SEL-001's "(ii) collapse the two/three-selector accretion
      (select_default / select_with_stack / optimizer_bridge) into one verified
      source" motivation — and the next gated frontier, none of it in shipped
      firmware (gale ships `--relocatable` / direct): #500 — `br_if` STILL
      unresolved for if/else (nested block+br_if+`br`) and SEQUENTIAL-block shapes
      (`seqblocks`, two non-nested blocks, is the minimal repro; the #483
      End-label fix is necessary-not-sufficient; the Pattern-3 select matcher was
      ruled OUT); #499 — a spill frame (`sub sp,#N`) not deallocated under control
      flow (missing `add sp`), a latent SP leak that #490's `pop {..,pc}` epilogue
      turned FATAL (#215-class "epilogue change exposes a latent frame bug"); #498
      — the `byte_offsets` estimator still lacks `Cmp`/`Cmn`/`Adds`/`Subs`/`Popcnt`
      (structural: synth-synthesis cannot depend on synth-backend, so the size
      table is a hand-maintained mirror of the encoder that drifts); #496 —
      register-exhausting i32 folds silently miscompiled (no spill, no decline).
      All four are SEPARATE gated steps (flag-off / differential / silicon as
      applicable), never idle-tick increments.
      FRONTIER ADVANCED + A LOAD-BEARING NEGATIVE RESULT (2026-06-26, second arc,
      #496/#503/#507/#509): three of the cluster LANDED, each with a new CI
      execution oracle, and a fourth mapped the hard boundary of the
      decline-to-direct pattern. #496 RESOLVED (PR #502, `988ea3b`): the optimized
      path's `alloc_i32_scratch` borrowed R12/IP (the encoder's indexed-load base
      scratch, #212) on R4-R8 exhaustion → collision miscompile (control_step
      execution-faulted `add ip,ip,ip`=2×base; flight_seam_flat wrong values); fix
      flags exhaustion via a Cell and DECLINES the whole function to the direct
      selector (which spills), gated by `r12_spill_496_differential.py` (both
      silicon fixtures, default path, execute == wasmtime). #503 RESOLVED + SHIPPED
      v0.16.0 (PR #504, `8e917a2`) — but only its >8-SCALAR sub-case; #503 the ISSUE
      STAYS OPEN for the 64-bit-stack-param sub-case. The SHIPPED `--relocatable`
      direct selector SKIPPED functions needing the AAPCS stack-arg path beyond a
      conservative cap (>8 scalar params, or a call passing >8 args) — the
      incoming/outgoing stack-arg machinery was already generic, so the fix lifts
      the `>8` caps and leans on the existing 12-bit `[sp,#imm]` guards. Gated by
      `stack_args_503_differential.py` (sum10/sum25-reading-param-24/outgoing/
      combined, all == wasmtime) — the standalone >8-i32 capability is confirmed.
      FALCON RESULT CORRECTED (gale-verified v0.16.0 @ `4a6b1ef`, 2026-06-26):
      this unblocked **0 of the 3** named falcon helpers, NOT the "2 of 3" an
      earlier optimistic note here claimed — all three carry i64, so lifting the
      >8-scalar cap only EXPOSED their true blocker (the earlier "10 params / 25
      params" labels were the scalar check tripping FIRST and masking the i64
      signature). `func_57` `(…i64 i64 i64)` + `func_163` `(i32 i64 i64 i64 i64)`
      hit the 64-bit-stack-param case #503 stays open for; `func_58` hits a
      DISTINCT wall — i64-register-pair allocation (no high register free for the
      R8 pair), #242/regalloc territory, NOT the stack-arg path. falcon skip count
      29/145 unchanged from 0.15.1 until the 64-bit-stack-param piece + the i64-pair
      allocation both land. jess v0.6.0 correctly lists #503 as a still-open v0.7.0
      supplier pole. This is the first SHIPPED-path member of the cluster, hence the
      v0.16.0 minor (the optimized-path-only #490/#483/#496/#507 ride along, no
      individual tags). #507 RESOLVED (PR #508, `ed3e48c`): the
      optimized path DROPPED `br_table` during wasm→IR (no `cmp`, selector never
      loaded → all arms fell through); since the drop precedes `ir_to_arm`, the fix
      detects `br_table` on the RAW wasm op stream in `arm_backend` and forces the
      direct selector (#496-pattern), gated by `br_table_507_differential.py`
      (void seq/shared shapes × every selector). #509 — NEGATIVE RESULT, the
      load-bearing one: the DIRECT selector (so the SHIPPED `--relocatable` path)
      ALSO drops the carried value of a value-returning branch — `br`/`br_if`/
      `br_table`-direct to a result-typed block returns 0 for the dispatched arm
      (`pick(0)=0` vs wasmtime 10). The #507 decline-to-direct shortcut DOES NOT
      WORK here and must not be re-attempted: the IR carries no block-result arity
      (`WasmOp::Block` is a UNIT variant; the decoder tracks none), so a
      "non-empty vstack at the branch ⇒ decline" heuristic cannot distinguish a
      CARRIED result from an UNWOUND void-target value (`i32.const 1; br 2` to a
      VOID block is legal WASM that compiles correctly today), and the decline
      over-refuses valid code (broke 4 selector tests, 3 plain-`Br`). Trading a
      latent miscompile for a latent regression is not progress, and no shipped
      artifact hits it today (gust's `br_table` is void-dispatch) — so #509 is
      BACKGROUND priority and requires the REAL fix: thread block-result arity
      (decoder → `WasmOp::Block`/`Loop`/`If` → selector) + a result-register
      convention generalizing the #313 if/else reconciliation to labeled-block
      branches. That is precisely VCR-SEL-001's "(ii) collapse the selector
      accretion into one verified source" — the value-carry boundary is the
      sharpest evidence yet that the hand-written selectors lack the structured
      block-arity model a verified DSL would carry by construction. Cross-cutting,
      byte-changing, silicon-gated — never an idle-tick increment.
      #509 ORACLE-FIRST (2026-06-27, frozen-safe, NOT yet fixed): the
      characterization oracle now exists in-tree —
      `scripts/repro/br_table_value_509_differential.py` +
      `br_value_509.wat` (value-returning `br_table` `pick`, value-returning
      `br_if` `pick_brif`, and a branchless value-returning `ctrl` control). Measured
      vs wasmtime under unicorn on BOTH paths: the SHIPPED direct path drops the
      carried value on every dispatched/taken arm (`pick(1)`→2 vs 12, `pick_brif(1)`
      →0 vs 10) while the branchless `ctrl` stays correct — isolating the defect to
      the branch value-carry, not result-typed blocks in general. A richer fact than
      the issue stated: the DEFAULT (optimized) path handles `br_if` value-carry but
      still drops `br_table` value-carry, so the bug is not uniform across paths. The
      script is a stable characterization (exit 0 = bug-as-documented); the gated
      block-arity fix flips `EXPECT_MISCOMPILE`→False and it becomes the correctness
      gate. Also corrected a STALE over-claim: `br_table_507_differential.py`'s
      header advertised a "value-returning" shape its `FIXTURES` never contained
      (only the two void-dispatch shapes) — now points at the #509 oracle for the
      carried-value case. Still byte-changing / background — its own gated step.
      #518 ORACLE-FIRST (2026-06-27, third arc member, NOT yet fixed): an i64
      binop reading an i64 PARAM silently miscompiles on BOTH selectors — the same
      `func_58`-class i64-pair-register wall the #503 falcon correction named, now
      isolated to a minimal fixture and quantified ahead of the gated fix. The
      defect is ONE omission with two surface forms: an i64 PARAM is never
      classified as i64. (a) DIRECT/`--relocatable` (`select_with_stack`):
      `infer_i64_locals` learns width only from `LocalSet`/`LocalTee` of an i64
      producer, so a param that is only READ keeps `is_i64=false` → `local.get`
      pushes `StackVal::Reg{is_i64:false}` → its implicit hi (`i64_pair_hi(R0)=R1`)
      is unreserved on the vstack → the following `i64.const` allocates INTO R1 →
      `i64.add` reads the clobbered `a_hi`. Low half correct, high half returns the
      const's low word (`t_add(7)` → `0x5_0000_000C`). (b) OPTIMIZED (`ir_to_arm`):
      the `I64Load` param-home guard (`num_params >= 2`/`>= 4`) confuses a REGISTER
      count with a PARAM count — `(param i64)` has num_params==1, falls through to a
      fresh callee-saved pair (R4:R5) never homed from R0:R1, dropping the param
      (`t_add(7)` → 5, the bare const). Characterization oracle landed THIS tick
      (frozen-safe, no codegen touched): `scripts/repro/i64_param_518.wat` +
      `i64_param_518_differential.py` — AAPCS-correct arg placement (even-aligned
      i64 pairs: `(i32,i64)` → R0,R2:R3), i64-aware result readback (R0|R1<<32),
      runs BOTH paths vs wasmtime. Measured: 10/10 i64-param functions diverge on
      each path; the i32 control (`t_i32`) stays correct on both. The fixture
      covers the FULL AAPCS i64-param register-assignment matrix the fix's mapping
      logic must get right — not just the single leading `(i64)` (R0:R1) case but
      the multi-param shapes the sequential `index_to_reg(i)` mapping botches:
      `(i64,i64)` (p1 = even-aligned R2:R3, mis-mapped to R1 → computes p0.lo+p0.hi
      instead of p0+p1), `(i64,i32)` (p1=R2 ignored), and reading ONLY the second
      i64 param (sequential reads R1, and the const clobbers the real p1.lo=R2). The script is a
      stable characterization (exit 0 = "bug reproduces as the root cause
      documents"); the gated fix flips its `EXPECT_MISCOMPILE→False` and it becomes
      the correctness gate. BOUNDED FIX SPEC for the gated step (NOT this tick):
      direct path — seed `i64_locals` from `self.params_i64` and replace the
      sequential `index_to_reg(i)` param mapping with AAPCS-correct even-aligned
      pair assignment; optimized path — DECLINE i64-param functions to the direct
      selector (the #359/#188/#507 honest-degradation pattern, since `ir_to_arm`
      lacks the param TYPES needed to compute AAPCS pairing). DECLINE LOUDLY at the
      #503-i64 boundary (an i64 param past R3 → stack-passed → still open). Functions
      with no i64 param are byte-identical by construction (the frozen anchors carry
      no i64 params), so the fix is frozen-safe on flip. Byte-changing, silicon-
      gated — its own gated session, never an idle tick.
      CROSS-BACKEND CONTRAST (2026-06-27, measured): the SAME root cause is SILENT
      on ARM but LOUD-SKIPPED on RISC-V. The RV32 selector validates the operand-
      stack TYPE before lowering an i64 op, so an i64 param reaching `I64Add` as an
      i32 operand trips `stack type mismatch ... expected i64, found i32` → typed
      `Err` → `warning: skipping function …` + absent symbol (the #378/#180/#185
      never-guess Ok-or-Err contract as the honest-fail backstop ARM's
      `select_with_stack` LACKS for i64 params). So on this class RV32 is INCOMPLETE
      (cannot yet compile i64-param functions) but SOUND (no silent wrong-code),
      while ARM is COMPLETE-but-UNSOUND until the gated fix — the precise
      VCR-SEL-005 parity shape (ARM lowers X; RV32 loud-declines X). Pinned by
      `scripts/repro/i64_param_518_riscv_loudskip.py` (all 7 i64-param fns
      loud-skipped, i32 control emitted): a regression removing the RV32 stack-type
      guard would flip a loud-skip into a silent miscompile, which the oracle
      catches.
    status: approved
    tags: [oracle, differential, coverage, mcdc, validation, track-c, riscv]
    links:
      - type: derives-from
        target: VCR-001
    fields:
      req-type: non-functional
      priority: should
      verification-criteria: >
        Rule-coverage is measured and reported; unproven-op fixtures are
        prioritized; the suite flags any op exercised on silicon but absent from
        the model; frozen fixtures remain a subset and stay bit-identical.
        GLUE COVERAGE (deep-research 2026-06-10, CVE-2022-31146 lesson): bugs
        escape through the UNCHECKED boundary around a checked core — the
        oracle must exercise prologue/epilogue, branch resolution, relocation,
        and encoder glue explicitly, not just the allocator/selector cores.

  # ---------------------------------------------------------------------------
  # Program-level verification gate
  # ---------------------------------------------------------------------------

  - id: VCR-VER-001
    type: sys-verification
    title: "Program gate: patch-accretion reverses, fixtures frozen"
    description: >
      The standing oracle-gated cleanup audit is the program's progress meter.
      As Track A lands, previously load-bearing greedy-fixes (the reciprocal-mult
      cost-gate, the 2-temp UMULL path) shall become revert-able toward the clean
      form with the full differential staying bit-identical and cycles
      equal-or-better — the exact condition the audit checks each cycle. Success
      is measured by those reversions becoming possible, not by new patches.

      GATE DEMONSTRATED (2026-07-08, evidence: scripts/repro/vcr_ver_001_gate.md).
      TWO reversals, one complete and one revertable-behind-flag:
      (1) the v0.11.20 reciprocal-mult COST-GATE — load-bearing when added
      (v0.11.19 hard-failed control_step's 4x const div_u) — was DELETED
      outright in PR #322 once the #320 spill retry covered its case: full
      differential bit-identical (+-0 B, the fallback was dead on the whole
      frozen suite), cycles trivially equal, no new cost-gate since — the
      pass-criteria met literally.
      (2) the #496 exhaustion hard-DECLINE is revertable behind
      SYNTH_SPILL_ON_EXHAUST (#580, default off = fix stays): flag-on the
      original red case stays green (r12_spill_496 differential PASS incl.
      0x00210A55/0x07FDF307; all five pressure differentials PASS on the
      reversal bytes), frozen pinned goldens 10/10 in BOTH flag states, the
      three result anchors' default-path bytes byte-identical flag-on (locked
      by vcr_ver_001_gate_242.rs), declines 14->8 across the corpus. HONEST
      HOLD: the weighted cycle proxy REGRESSES on i32 shapes (+30.4%
      spill_on_exhaust_242, +32.4% spill_rung_581, +8.0% high_pressure_i32,
      +120% signed_div_const whose 34-B direct lowering becomes a 76-B
      optimized-path compile; i64 shapes improve -5.5%/-1.4%) — the decline
      remains load-bearing FOR CYCLES, not correctness. Missing capability
      (VCR-RA follow-on): post-exhaustion code quality on the optimized path
      (allocation-time spill placement/coalescing; frame-slot-DCE/stack-fwd
      do not reach allocation-time slots). The default-on flip stays a
      separate later PR gated on closing that gap + gale G474RE cycles (#580).
    status: implemented
    tags: [verification, audit, regression, frozen-fixtures]
    links:
      - type: verifies
        target: VCR-001
    fields:
      method: analysis
      preconditions:
        - "Track A (VCR-RA-001) landed"
        - "Frozen-fixture differentials green at baseline"
      steps:
        - "Re-run the cleanup audit: is the reciprocal-mult cost-gate now revert-able?"
        - "Revert toward the clean form; confirm all fixtures bit-identical"
        - "Measure cycles equal-or-better; measure no new exhaustion hard-fail"
      pass-criteria: >
        At least one previously load-bearing greedy-fix is removed with the full
        differential bit-identical and cycles equal-or-better; no new cost-gate
        introduced.

  - id: VCR-VER-002
    type: sys-verification
    title: "Trap-preservation VC catches dropped WASM traps (i32+i64 div/rem, memory OOB, call_indirect, unreachable, float→int trunc); live-validator wiring in progress"
    description: >
      Make trap-preservation a checkable, oracle-gated proof obligation so a
      lowering that DROPS a WASM trap (div-by-zero / overflow guard, OOB
      bounds check, call_indirect bounds/null/type, unreachable, float→int
      truncation NaN/∞/out-of-range) can no longer
      pass value-only equivalence — the systematic end of the per-op
      soundness whack-a-mole (#633/#666/#665/#642/#709).

      Foundation: consume ordeal 0.9.0's new `ordeal::trap` module (co-designed
      in ordeal#59 / TR-019) — QF_BV trap-condition builders over operand/
      pointer bits plus trap-preservation VCs (`prove_trap_equivalence`,
      `prove_trap_condition_equivalence`). Boundary held: ordeal classifies
      bits, never models op values (consumer-supplied) or floating point;
      soundness is that of the certificate-checked pipeline (Unsat carries an
      LRAT proof, re-checked before acceptance).

      STATUS in-progress (v0.40.x). LANDED:
      (1) synth-verify bumped ordeal 0.4 -> 0.9.
      (2) `synth_verify::trap` wrapper maps synth WASM ops to trap conditions
      over synth's own BV/Bool and exposes the gate as a `TrapVerdict`
      {Preserved | Dropped(model) | Unknown}.
      (3) RED-FIRST non-vacuity gate (tests/trap_preservation.rs, 6 tests, 5
      op classes): for each class a trap-DROPPING lowering is CAUGHT
      (Dropped/Sat) and a trap-PRESERVING lowering accepted (Preserved/Unsat)
      — including both call_indirect TypeTrap modes (Runtime and
      StaticallyDischarged). Proves the gate rejects the exact bug shapes.
      (4) a DEDICATED always-checks div/rem trap-preservation method,
      TranslationValidator::verify_div_rem_trap_preservation (full VC, ARM trap
      condition derived structurally from the Udf guard), exercised by unit
      tests: an unguarded i32 div/rem is rejected with a divisor==0
      counterexample, a guarded one accepted.
      (5) Phase B (ordeal 0.9.1, ordeal#59/TR-020): the float->int TRUNC trap
      class (#709). ordeal's `trap_trunc` classifies the trap predicate
      (NaN / +-inf / out-of-range) purely over the float operand's BIT PATTERN
      - exponent-field patterns plus sign-split monotonic magnitude threshold
      compares; floats enter as BV32/BV64, no FP theory. synth_verify::trap
      maps all six WasmOp trunc variants (i32/i64.trunc_f32/f64_s/u as decoded;
      i64.trunc_f32_* are not WasmOp variants) via trunc_op + trap_trunc,
      trap-clause-only VC (synth models no float->int value). Red-first gate
      extended (11 tests total): for all six variants a guard-dropping lowering
      is CAUGHT (Dropped/Sat) with a counterexample validated as genuinely
      trapping against the real-float reference, an identical-guard lowering
      accepted (Preserved/Unsat, LRAT re-checked); a signedness-confused guard
      (unsigned range check on trunc_f32_s - the VCVT-saturate partial-drop
      shape) is caught; and the classifier ENCODING itself is eval-tested
      against the synth #709 boundary table (the reference-oracle check
      ordeal#59 called for: 2^31/0x4F000000 traps signed, -2^31/0xCF000000
      in range, -1.0 traps unsigned, 2^32 traps, NaN/+-inf trap, 3e9/-3e9
      trap, 2.5/0.5/-0.0 in range, plus f64 and i64-target anchors) - both
      directly via ordeal::eval and at ground inputs through the
      certificate-checked pipeline, with a wrong-expectation non-vacuity
      control.

      LIVE-VALIDATOR WIRING (v0.43+, the may_trap flag now threaded through the
      ArmState exec model via encode_sequence_br — is_trap_gated_op MANDATORILY
      routes these to verify_trap_preservation, so a value-only proof can no
      longer accept a dropped trap on the live path). Classes with a DERIVED
      ARM trap term:
      - i32 div/rem (full VC: trap + guarded value), unreachable, i32
        load/store (all widths), i32.trunc_f32_s/u, call_indirect (v0.43).
      - i64 div/rem (#756): field-derived trap-condition VC. ARM32 has no
        64-bit divide, so the shipped I64Div/I64Rem pseudo-op carries its
        guards as elide_zero_guard/elide_overflow_guard FIELDS and leaves the
        quotient symbolic; the ARM trap term is CONSTRUCTED from those fields
        (a set elide_* deletes the clause), so a guard elided without a
        discharged fact is rejected. Certifies the selector's elision decision
        (like call_indirect); byte-expansion is execution-gated.
      - i32.trunc_f64_s/u (#756): D-register domain guard, condition-only VC.
        The ordered VCMP.F64 compares (F64Lt/F64Gt/F64Ge) get real f64
        bit-pattern semantics in the executor (f64_is_nan / f64_ordered_lt),
        the 64-bit twin of the f32 trunc wiring.

      DOCUMENTED GAP (why in-progress, not implemented):
      - i64.trunc_f64_s/u is NOT live: the selector loud-declines it (i64
        register pairs are unsupported on 32-bit ARM), so there is no shipped
        lowering to derive an ARM trap term from. Its trap classifier
        (trap_trunc(F64,I64,...), incl. the 2^63/-2^63/2^64 boundaries) stays
        unit-gated in tests/trap_preservation.rs.
      - The value-only div-rule fixtures (comprehensive_verification.rs) that
        exercise verify_equivalence directly are unaffected; the i64 quotient
        remains unmodeled (no bvsdiv term at 64-bit), so i64 div/rem carries a
        trap-condition VC rather than the i32 full-value VC.
    status: proposed
    tags: [verification, trap-preservation, soundness, ordeal]
    links:
      - type: verifies
        target: VCR-001
      - type: refines
        target: VCR-VER-001
    fields:
      method: formal-verification
      preconditions:
        - "ordeal 0.9.0 `ordeal::trap` module available (ordeal#59)"
        - "ordeal 0.9.1 `trap_trunc` float→int classifier available (ordeal#59/TR-020)"
      steps:
        - "Bump synth-verify to ordeal 0.9; build + tests green"
        - "Wrap ordeal::trap over synth BV/Bool (synth_verify::trap)"
        - "Red-first gate: Sat-on-drop / Unsat-on-preserve for every op class"
        - "Wire div/rem trap-preservation into the translation validator"
        - "Phase B: map the six WasmOp trunc variants to ordeal 0.9.1 trap_trunc; eval-gate the classifier against the #709 boundary table"
      pass-criteria: >
        A trap-dropping lowering is rejected (Sat/Dropped) and a
        trap-preserving lowering accepted (Unsat/Preserved) for every partial-op
        class in the unit gate; div/rem trap-preservation is a mandatory
        validator obligation. Full auto-derivation for all classes is the
        documented exec-model follow-on.

  - id: VCR-VER-003
    type: sys-verification
    title: "Static-data addressing VC catches the overlapping-segment wrong-segment miscompile (#757) at compile time on every module"
    description: >
      Make static-data-relocation resolution a checkable, per-compilation proof
      obligation so the #757 silent miscompile — an overlapping active data
      segment binding a static reloc to the WRONG (earlier) segment — can no
      longer ship. #757 survived four releases (0.43.0/0.43.1/0.44.0/0.45.0)
      because value-differential oracles are COVERAGE-limited: 7 synthetic
      reconstructions were all green, and only gale's real fused gust:os node
      (three active segments all at linmem 0x100000, string in the LAST) hit it.

      Invariant (per compiled relocatable object, N data segments): for EVERY
      emitted static-data relocation (symbol __synth_wasm_seg_K, addend A), the
      byte the packed .data serves (seg[K].bytes[A]) EQUALS the byte the RUNTIME
      linear-memory image holds at the original access address (seg[K].off + A),
      where the runtime image applies every active segment in WASM declaration
      order, later-wins. This lifts the post-hoc #757 differential
      (scripts/repro/mem757_gale_differential.py) into a per-compilation
      validator: a wrong-segment resolution FAILS at compile time on ANY module.

      Concrete byte-equality, NOT fabricated SMT: there are no symbolic operands
      (unlike VCR-VER-002's trap VCs), so the honest form is a direct comparison
      against an independently reconstructed truth image. The runtime image is
      derived ONLY from the segment list — never from the chosen K — so the
      validator cannot be satisfied by mirroring the code under test
      (mirror-pinning vacuity is structurally excluded).

      STATUS implemented (v0.46). LANDED:
      (1) synth_core::static_data_addr — validate_reloc_resolutions() over
      DataSegment + the EMITTED RelocResolution (seg_index, addend), returning
      Verdict {Consistent | Mismatch(Vec<AddrMismatch>)}. Lives in synth-core so
      it runs UNCONDITIONALLY: the shipping build is `--features riscv`, NOT
      `verify`, so a verify-gated check would stay dormant in exactly the build
      that shipped #757. synth-verify::addr re-exports it (VCR-VER-002 structure
      parity), single source, no mirror drift.
      (2) Wired into the mixed-split reloc retargeting path (synth-cli main.rs):
      the loop records the EMITTED (k, new_addend) per static-data reloc — never
      recomputed — and hard-errors the compile (anyhow::bail!) on any Mismatch,
      naming the symbol/addend/served/runtime bytes.
      (3) RED-FIRST non-vacuity gate. Permanent discrimination unit test
      (synth_core::static_data_addr, red_on_first_match_green_on_last_match): the
      SAME validator, on a synthetic 3-overlap module with DISTINCT bytes, goes
      Mismatch on the .position() (first-match, the #757 bug) resolution and
      Consistent on the .rposition() (last-match, correct) resolution — the
      tie-break is an ARGUMENT (resolve_owner last_wins), so no source revert.
      Plus partial-overlap-tail-wins, non-overlapping-both-consistent,
      out-of-range-mismatch.
      (4) DURABLE end-to-end gate (synth-cli tests/vcr_ver_003_addr_777.rs):
      compiles gale's REAL loom.wasm and asserts exit 0. Because the validator is
      wired unconditionally, this GREEN goes RED the instant main.rs reverts
      .rposition() -> .position(). That revert was demonstrated by hand for the
      PR: compile FAILS with `func 9 reloc @ 0x250: __synth_wasm_seg_0+0x8 ->
      linmem 0x100008 serves 0x02 but the runtime image owns 0x67` — exactly
      gale's historical got=[2,0,0,0,..] = __synth_wasm_seg_0+8.

      TRIGGER SCOPE: the validator runs on the native-pointer relocatable
      mixed-split path (`--native-pointer-abi --relocatable` + the
      mixed_separable geometry — the only path that emits per-segment
      __synth_wasm_seg_K retargets). The #757 wrong-segment class exists ONLY on
      that path, so "catches #757 on every module" holds: no module can exhibit
      the wrong-segment miscompile uncaught. It is not a check that runs on every
      compile in general.

      PHASE 2 (v0.47, #777 follow-ups) — the phase-1 BOUNDED items, landed:
      (5) MULTI-BYTE SPANS (validate_reloc_resolutions_spanned): beyond the
      addend byte, every runtime-covered byte a conservatively-widened access
      (MAX_ACCESS_BYTES = 8; CodeRelocation records no width — the Abs32
      literal is a pointer) could read must equal what the SHIPPED packed init
      blob serves at that position (the emission extends the validated blob,
      so the served side is the real artifact). Catches the staggered-overlap
      straddle (addend byte correct, tail bytes runtime-owned by a LATER
      segment — demonstrated live: the v0.46 binary compiled the synthetic
      straddle fixture clean with packed seg_0 serving a4a5 where the runtime
      image owns b0b1; phase 2 hard-fails it with `span byte +2`), the
      4-align-padding-shifted crossing, and the init-region escape. DOCUMENTED
      RESIDUE: a span byte NO segment covers at runtime (implicit-zero linmem)
      is skipped — flagging it would hard-error the ubiquitous "pointer near a
      sparse segment's end, narrow access" shape; exact checking needs a
      recorded access width (named follow-up).
      (6) SELF-CONTAINED --cortex-m (#758 ROM-copy): the dense flash image is
      packed by the shared declaration-order packer (pack_rom_image) and
      validated unconditionally against the reconstructed runtime image
      (validate_served_image — every blob byte equals the later-wins byte,
      zero in gaps; garbage-in-gap and first-wins packs are RED in the
      permanent unit gate, the overwrite policy is an argument). The dense
      layout (index = linmem offset) preserves spans/overlaps structurally, so
      the straddle fixture that the mixed split refuses compiles CORRECTLY
      here (e2e green gate).
      (7) RV32 single-base scheme (s11 = __linear_memory_base, zeroed RAM):
      the object used to ship NO static-data initializer image at all —
      probing found active nonzero data segments were silently DROPPED (loads
      read 0x00); v0.47 held a loud warning. SHIPPED in v0.48 (#798, the RV32
      analogue of #758): active segments pack into sparse per-segment records
      ([u32 off][u32 len][bytes][pad4], declaration order — synth_core::
      static_data_addr::pack_segment_records) emitted as a `.wasm_data`
      PROGBITS section; the generated linker.ld places it in flash
      (__wasm_data_records_start/end, before _data_load) and the generated
      startup.c byte-copies each record to `__linear_memory_base + off` at
      reset (record order ⇒ later-wins). The VCR-VER-003 arm READS BACK the
      emitted blob (served_image_from_records — never a recompute) and
      hard-errors the compile on any served/runtime disagreement; a segment
      past the declared memory is refused (instantiation would trap, #758
      parity). Gated red-first: the control_step RV32 differential was
      DE-VACUATED (linmem init now comes from the shipped records, not
      wasmtime's memory image — pre-fix object FAILS loud, 0x00000000 vs
      0x00210a55) and a full-boot oracle
      (rv32_data_798_boot_differential.py: clang riscv32 + ld.lld + unicorn
      from _reset) proves the REAL startup copy loop serves the later-wins
      image for overlapping segments. Data-free modules ship no section and
      stay byte-identical (frozen fixtures' .text unchanged — no re-pin
      needed; a reversed-order pack is RED in the permanent unit gate).
      (8) AArch64: N/A, verified — the -b aarch64 integer subset has no
      linear-memory loads/stores (every memory op loud-declines at selection:
      "unsupported wasm op for aarch64 subset"), so compiled code cannot
      observe static data; there is nothing to validate.

      BOUNDED (named follow-ups after phase 2): recorded per-reloc access
      widths (removes the uncovered-span-byte tolerance and the conservative
      8-byte widening); all-addressing coverage (dynamic base+index accesses
      that cross packed-segment boundaries at runtime are out of static reach
      on the mixed split). RV32 initializer shipping landed v0.48 (#798,
      item 7 above).
    status: implemented
    tags: [verification, addressing, relocation, soundness, mem757]
    links:
      - type: verifies
        target: VCR-001
      - type: refines
        target: VCR-VER-002
    fields:
      method: translation-validation
      preconditions:
        - "#354 mixed-split per-segment reloc retargeting (__synth_wasm_seg_K)"
        - "#757 fix: overlapping addresses resolve to the last-declared owner (.rposition())"
      steps:
        - "synth_core::static_data_addr: runtime-image reconstruction + per-reloc byte-equality validator"
        - "Wire the EMITTED (k, addend) into the mixed-split retarget loop; hard-error on Mismatch"
        - "Red-first unit gate: Mismatch on .position(), Consistent on .rposition() (same validator, argument toggle)"
        - "Durable e2e gate: real gale loom.wasm compiles exit-0; regresses to RED on the .position() revert"
        - "Phase 2: spanned reloc check against the SHIPPED init blob (straddle refused e2e, owner access green)"
        - "Phase 2: #758 dense ROM image packed via pack_rom_image + validate_served_image (first-wins pack RED in the unit gate)"
        - "Phase 2: RV32 zero-served-image check — nonzero dropped initializers WARN loudly; zero-overwritten silent"
        - "#798 (v0.48): RV32 ships .wasm_data records (linker placement + startup copy); read-back validate_served_image hard-errors; de-vacuated control_step differential + full-boot unicorn oracle"
      pass-criteria: >
        On any compiled relocatable object every static-data reloc resolves to
        the runtime-correct byte (segments later-wins), else the compile fails.
        The validator is Mismatch on the #757 wrong-segment (.position())
        resolution and Consistent on the correct (.rposition()) one for an
        overlapping-segment module; the real gale module compiles clean and
        regresses to a hard error under the .position() revert. Phase 2: the
        staggered-overlap straddle fixture is REFUSED on the mixed split with
        a span diagnostic (and compiles CORRECTLY self-contained); the #758
        ROM image validates on every self-contained build (first-wins pack is
        Mismatch in the unit gate); RV32 SHIPS its active segments as
        .wasm_data records whose read-back served image must equal the
        runtime image (hard error on mismatch; reversed-order pack is
        Mismatch in the unit gate; de-vacuated control_step differential +
        full-boot oracle green); AArch64 is documented N/A (no linear-memory
        ops in the subset).

  - id: VCR-VER-004
    type: sys-verification
    title: "ABI observable-contract validator: a per-compilation check that fails DIFFERENTLY from the two dataflow validators that shared a blind spot (#242)"
    description: >
      SHIPPED v0.54. Filed into this roadmap in v0.55 (#893) — it was absent
      entirely, which README calls out as a real gap because this file is
      "the single source of truth for roadmap status" and VCR-VER-004 is a
      shipped North-Star component.

      THE MEASUREMENT THAT MOTIVATES IT (v0.53). Emptying `cfg_exit_observable`
      — the exit contract the join-aware graph allocator and its OWN CFG
      validator SHARE — makes the compiler emit code that leaves the return
      value in the WRONG REGISTER, and BOTH per-compilation validators accept
      it: `validate_cfg_rewrite` returns `Ok` and VCR-RA-003's
      `validate_final_allocation` returns `Consistent`. Only EXECUTION caught
      it. Two independent-LOOKING instruments, one shared blind spot — #872's
      lesson one level up, and a direct counterexample to the claim that
      per-compilation validation is an independent check on the code generator.

      THE RESPONSE IS NOT A THIRD FILE ON THE SAME AXIS. Independence is not
      obtained by writing a second checker, only by checking a different WAY.
      `synth_synthesis::abi_contract::validate_abi_contract` differs on four
      axes that matter:
        (1) ITS OBLIGATION CANNOT BE EMPTIED. The exit obligation is
            `RETURN_CONTRACT_REGS = [R0, R1]`, a constant of the AAPCS hard-named
            in the module's own source. Deleting `cfg_exit_observable` outright
            would not change one line of it.
        (2) IT IS FORWARD, and a forward value analysis is structurally
            incapable of the fail-open mode that bit v0.53.
            `validate_cfg_rewrite` is a BACKWARD MUST-analysis whose obligation
            set is a VARIABLE — and the empty set is a fixpoint, so an empty
            seed means zero obligations means vacuous green. A forward
            evaluation always produces EXACTLY ONE value for `R0` at each
            return. There is no seed to shrink.
        (3) ITS EVIDENCE IS A VALUE, NOT A NAME-PAIR. Per side independently it
            builds a value graph (`Init(r)` / `Def(i,k)` / `Phi(b,n)`) and
            compares by GREATEST-FIXPOINT BISIMULATION; on a deterministic term
            graph that is equality of the infinite unfoldings, so loops and back
            edges are handled coinductively rather than by unrolling. `Init(r)`
            is one node SHARED by both sides — the AAPCS PARAMETER half of the
            anchor — so reading an argument out of the wrong register is a value
            change too.
        (4) IT TAKES NOTHING FROM THE PASS. The signature is
            `(orig, rewritten)`; the CFG is re-derived from both streams'
            label-form branch structure and the two must agree. The v0.50 join
            attempt failed precisely by letting the pass hand the checker its own
            seed.

      CALLS ARE MODELLED, NOT EXEMPTED. Each clobbered register
      `{R0-R3, R12, LR}` is rebound to a FRESH node whose operands are the
      PRE-CALL argument values, while `R4-R11`/`SP` flow through — so a call
      result is an opaque value equal across the sides exactly when the same
      callee got the same arguments. The AAPCS call effect reuses
      `liveness::call_effect`, the ONE definition the pass and
      `validate_cfg_rewrite` already share, because two divergent call models
      would be a fresh instance of the very blind-spot class this module
      attacks.

      HONEST LIMITS — three, stated because the point of this artifact is that a
      validator which quietly shares its pass's blind spot is worse than no
      validator:
        (a) IT IS A GATE ONLY ON THE FLAG-OFF graph-colouring allocator. On the
            DEFAULT path it is a report-only audit held to a CI floor. Making it
            gate the default path means hard-erroring a user's compile on a
            checker whose false-positive rate is MEASURED, not proven; that flip
            is deliberately not taken.
        (b) MEMORY IS NOT IN ITS OBLIGATION. A mis-renamed store address that a
            later load reads back is a false negative for this instrument (it is
            covered by `validate_cfg_rewrite`'s use-equations when that seed is
            intact — the two are COMPLEMENTARY, which is what independence looks
            like, not redundancy).
        (c) THE OP MODEL IS STILL SHARED. Def/use extraction runs through
            `liveness::reg_effect`, so a MISMODELED OP remains a blind spot
            common to ALL THREE instruments. VCR-VER-004 closes the shared-
            CONTRACT hole, not the shared-OP-MODEL hole. `synth-verify`'s
            `ArmSemantics::encode_op` is a genuinely second model of the same
            operations; PINNING THE TWO AGAINST EACH OTHER IS THE NEXT RUNG (the
            VCR-ISA-001 Sail-derived semantics are the eventual anchor), and
            until it is done "three independent validators" WOULD BE AN
            OVERCLAIM. This is the named follow-up.
    status: implemented
    tags: [validation, abi, aapcs, translation-validation, independence, register-allocation, track-c, epic-242, release-v0.54, synth-893]
    links:
      # Same shape as its two siblings VCR-VER-003 / VCR-VER-761: a
      # sys-verification measure must `verifies` a system requirement.
      - type: verifies
        target: VCR-001
      - type: traces-to
        target: VCR-RA-003
      - type: traces-to
        target: VCR-DEC-001
      # The shared-op-model residual (c) below names VCR-ISA-001's Sail-derived
      # semantics as the eventual anchor for pinning `liveness::reg_effect`
      # against a genuinely second model.
      - type: traces-to
        target: VCR-ISA-001
    fields:
      method: translation-validation
      preconditions:
        - "v0.53 #872: the shared-blind-spot class demonstrated by mutation on validate_segment_rewrite"
        - "VCR-DEC-001 increment 3 (#896): the graph-colouring allocator colours across calls, so the gate must model the AAPCS call effect rather than decline it"
      steps:
        - "synth_synthesis::abi_contract: forward value-graph construction + greatest-fixpoint bisimulation over RETURN_CONTRACT_REGS"
        - "graph_alloc::abi_gate wires it as the accept/reject gate on the flag-off colouring allocator (NotAttempted is a DECLINE, not an accept)"
        - "Re-run v0.53's EXACT mutation from the committed patch (scripts/repro/mutations/v053_shared_exit_contract.patch), not a reconstruction"
        - "Report-only audit of the SHIPPING allocator over the repro corpus, held to a CI floor"
        - "CI: instrument-independence-oracle asserts the BASELINE direction first, then the mutation, then that the tree was restored"
      pass-criteria: >
        On the mutated compiler and ONE compilation: `validate_cfg_rewrite`
        returns Ok and VCR-RA-003 returns Consistent (both still green — the
        shared blind spot is real and unpatched by this change) while
        `validate_abi_contract` REJECTS with a concrete violation naming the ABI
        result register — `Violated { sink: 81, reg: R0 }` on
        `brif_outer_740::poll`, the function that returned 0x1111 instead of its
        parameter — and the miscompile is NOT emitted. Proven RED-FIRST: make
        `abi_gate` treat `Violated` as an accept and the mutated compiler goes
        back to emitting the miscompile. COSTS NOTHING on the gated path —
        composed with VCR-DEC-001 increment 3 over the ARM repro corpus, 617
        functions, 307 applied, 40822 -> 40722 bytes (−100 B relocatable,
        −120 B self-contained): increment 3's result TO THE BYTE, with the check
        conservative enough to demand both R0 and R1 for every function and to
        decline whenever it cannot analyze. On the DEFAULT (shipping) path the
        audit measured `Holds 431 / NotAttempted 202 / Violated 0` over 633
        corpus functions — ~68 % of the shipping path proven, `bl`/`blx` calls
        included — with the corpus GROWING as lanes add fixtures, so the pinned
        invariant is `Violated 0`, not the absolute counts. Both CI steps assert
        machine-readable counts (`ASSERTIONS=4/4`, five `OK` lines,
        `VIOLATED=0`) rather than trusting exit 0, and the job fails if the
        mutation was left in the tree.

  - id: VCR-VER-761
    type: sys-verification
    title: "Self-contained --cortex-m linmem<->globals disjointness geometry gate catches the R9-overlap alias (#761)"
    description: >
      Extend the VCR-VER-003 static-data addressing validator with a
      per-compilation GEOMETRY invariant that closes the #761 latent-soundness
      hazard: on the self-contained --cortex-m image the full-page linear-memory
      view can OVERLAP the R9 globals table at the top of SRAM, so a store to the
      top of the first page silently ALIASES a global slot (or vice versa) — a
      wrong-value miscompile, the worst class for a safety backend.

      ROOT CAUSE (a single off-by-0x100 in the layout, not a fundamental
      infeasibility): the compiled functions address linear memory at
      optimized_linmem_base (= the startup R11 base + 0x100, the #687 gap), but
      the startup materialized the R9 globals table at `R11_base + memory_size`,
      forgetting that 0x100 shift. For a `(memory 1)` module the table landed at
      0x2001_0000 while a function's store to wasm offset 0xFF00 lands at
      0x2000_0100 + 0xFF00 = 0x2001_0000 — exactly global slot 0. The top 0x100
      of the page aliased the table, in BOTH stack layouts (--stack-layout=low
      shifts both bases equally, so the gap persists — the issue's guess that
      low sidesteps it is FALSE, disproven by the boot oracle).

      REPRODUCED end-to-end (not a synthetic reconstruction, the #757 lesson):
      scripts/repro/mem761_linmem_r9_overlap.wat stores 0xDEADBEEF to mem[0xFF00]
      then returns global 0 (init 0xABCD); the boot oracle
      (mem761_linmem_r9_overlap_differential.py) boots the REAL self-contained
      image through its reset path (materializing R9) under unicorn and calls the
      export. PRE-FIX: 0xDEADBEEF (the store landed on the global) vs wasmtime
      0xABCD — a live alias, in high AND low layouts. A disjoint witness (store
      at offset 0) is unaffected either way.

      FIX (separate the bases, not a decline — `(memory 1)` + a global is the
      most common self-contained shape): base R9 at
      `func_visible_linmem_base + memory_size` (= the page ceiling the functions
      can reach), so the table sits AT/above the ceiling and the regions are
      disjoint. One change fixes both stack layouts (func_visible base already
      carries the low-layout stack reserve). RAM sizing raised by the same 0x100
      gap so the auto-scaled RAM/SP stays above the table. POST-FIX: R9 =
      0x2001_0100 (high) / 0x2001_1100 (low); the oracle returns 0xABCD in both.

      LANDED:
      (1) synth_core::static_data_addr::validate_linmem_globals_disjoint —
      a pure geometry check returning LayoutVerdict {Disjoint | Overlap{..}}:
      the globals table base must be >= func_visible_linmem_base + linmem_bytes
      (half-open page; no-globals modules trivially disjoint). Lives in
      synth-core so it runs UNCONDITIONALLY (shipping build is --features riscv,
      not verify). Concrete geometry, no bytes — complements the byte-equality
      served-image gate; catches the placement bug, not a packing bug.
      (2) Wired into build_multi_func_cortex_m_elf (synth-cli): hard-errors the
      compile (anyhow::bail!) on any Overlap, naming the table base, the page
      window and the overlap byte count. Runs on every self-contained image.
      (3) RED-FIRST non-vacuity unit gate (5 tests): the EXACT pre-fix
      R11-based geometry is caught as a 0x100 Overlap; the fixed
      func-visible-based geometry is Disjoint; the ceiling boundary is exclusive
      (exact-ceiling = Disjoint, one below = 1-byte Overlap); no-globals is
      trivially Disjoint; the --stack-layout=low shape is Disjoint when fixed and
      still a 0x100 Overlap under the pre-fix placement.
      (4) DURABLE end-to-end boot oracle
      (scripts/repro/mem761_linmem_r9_overlap_differential.py): the real
      self-contained image, booted from reset under unicorn, RED pre-fix
      (0xDEADBEEF vs 0xABCD) and GREEN post-fix in both stack layouts; wired as a
      CI oracle step. Frozen fixtures' .text is byte-identical (the R9 base lives
      in the self-contained startup blob, not the --relocatable .text the frozen
      hashes cover; the #649 boot oracle stays green with the shifted R9), so no
      re-pin was needed.
    status: implemented
    tags: [verification, addressing, soundness, layout, mem761, cortex-m]
    links:
      - type: verifies
        target: VCR-001
      - type: refines
        target: VCR-VER-003
    fields:
      method: static-analysis
      preconditions:
        - "#687 optimized_linmem_base = R11 base + 0x100 (the function-visible linmem gap)"
        - "#649 R9 globals-table materialization in the self-contained startup"
      steps:
        - "synth_core::static_data_addr::validate_linmem_globals_disjoint: globals_base >= func_visible_linmem_base + linmem_bytes"
        - "Fix: base R9 at func_visible_linmem_base + memory_size (both stack layouts); raise RAM sizing by the 0x100 gap"
        - "Wire the geometry gate into build_multi_func_cortex_m_elf; hard-error on Overlap"
        - "Red-first unit gate: pre-fix R11-based geometry = 0x100 Overlap, fixed = Disjoint (high + low)"
        - "Durable e2e boot oracle: real image from reset under unicorn, RED pre-fix (0xDEADBEEF vs 0xABCD), GREEN post-fix"
      pass-criteria: >
        On every self-contained --cortex-m image the R9 globals table sits at or
        above the function-visible linear-memory page ceiling, else the compile
        hard-errors. The validator is Overlap on the pre-fix R11-based placement
        and Disjoint on the fixed func-visible-based placement, in both stack
        layouts; the boot oracle returns the correct global value (0xABCD) after
        the aliasing store in high and low layouts (RED pre-fix). Frozen
        fixtures' .text stays byte-identical (no re-pin).

  # ---------------------------------------------------------------------------
  # Parallel ROI tracks (measured 2026-06-06): the allocator (VCR-RA-001) is the
  # north-star but the const-remat is partly FORCED by the 9-register pool, so
  # its measured win is modest. gale's #209 decomposition put the BIGGEST single
  # chunk in clamp lowering (18 IT-blocks vs native 6), and a +1-register pool
  # (free R10 when bounds-off) is a cheap pressure multiplier. B + C run in
  # PARALLEL with A — disjoint code, gated by RESULT-identity (flight_seam
  # 0x07FDF307) + measured delta, not byte-identity, so no fixture-freeze
  # conflict.
  # ---------------------------------------------------------------------------

  - id: VCR-SEL-002
    type: sw-req
    title: Tighter int8-saturation (clamp) lowering — biggest measured lever (track B)
    description: >
      The int8 control saturations `if(x>127)x=127; if(x<-127)x=-127` (clamp to
      [-127,127]) lower to 18 IT-blocks on flat_flight vs native gcc's 6 — gale's
      #209 decomposition's single biggest chunk (~the middle of the 255->103
      gap). ARM SSAT does NOT apply ([-127,127] != SSAT's [-128,127]); the lever
      is a tighter Select/conditional-move lowering of the saturation idiom
      (fewer moves per clamp, reuse a resident bound) emitted by the selector.
      Independent of the allocator (different code region); composes with it.
    status: proposed
    tags: [codegen, selector, instruction-selection, clamp, track-b, perf, release-v0.11.35]
    links:
      - type: derives-from
        target: VCR-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        flat_flight IT-block count strictly decreases; all three differential
        fixtures RESULT-identical (control_step 0x00210A55 / flight_seam
        0x07FDF307 / div_const 338/338); gale confirms on-target cycles
        equal-or-better on the five frozen benches; flag-gated until confirmed.

  - id: VCR-SEL-003
    type: sw-req
    title: Multi-value-return ABI — multi-result call feeding select (selector op-gap, gale #329)
    description: >
      `synth compile --cortex-m --all-exports` silently skips a function when a
      multi-value `call` result feeds a `select` (falcon-flight func_39; func_30
      LocalSet one consumer over) — on a module `wasm-tools validate` accepts.
      Root cause is two-sided and confirmed from source @ v0.11.40: (1) caller —
      the `Call` arm (instruction_selector.rs ~7252) pushes exactly ONE operand
      per call regardless of result count (no `func_ret_count` metadata is
      threaded; only `func_ret_i64` exists), so `select` (pops 3) underflows in
      `pop_operand`; (2) callee — multi-value return is unimplemented: `$two`
      emits `movs r4,#10; movs r5,#20; bx lr`, leaving results in r4/r5, not the
      AAPCS return registers r0/r1. The two sides MUST land together: a
      caller-only push would compile-but-MISCOMPILE (read r0/r1, callee wrote
      r4/r5), converting today's safe skip into silent wrong-code. This is the
      "selector missed an op" class (VCR-SEL-001), not a one-line patch — it
      needs result-count metadata threaded through both codegen paths, an N-result
      push at call sites, and multi-result placement in r0..r(N-1) in both the
      explicit `Return` and the implicit fall-through epilogue. Non-blocking: no
      shipped wasm-cross-LTO module hits this shape (gale concurs). Regression
      lock landed in tests/fixtures/multivalue_call_select (PR #330).
    status: proposed
    tags: [codegen, selector, instruction-selection, multi-value, abi, op-gap, gale-329, track-a]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-SEL-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        repro_call_select.wat compiles AND `f` evaluates to the wasmtime golden
        (f(1)=10, f(0)=20) on a differential RUN — not merely "it compiles"; the
        three control fixtures stay compiling; >register-capacity result counts
        (>4 int results / memory-return-area) stay a clean skip, never a
        miscompile; the three frozen differentials (control_step 0x00210A55 /
        flight_seam 0x07FDF307 / div_const 338/338) remain RESULT-identical.

  - id: VCR-SEL-004
    type: sw-req
    title: Compare→select/br_if fusion — drop the bool-materialize+re-test flag round-trip (gale #209)
    description: >
      synth lowers each wasm op independently, so an `i32` comparison whose result
      feeds a `select`/`br_if` is materialized into a GPR bool (ITE + two movCC)
      and then RE-TESTED (`cmp #0`) to recover a condition the original comparison
      already set — `cmp <real>; ite; movCC #1/#0; cmp #0; it; movCC` = 7
      instructions where 3 suffice (`cmp <real>; it CC; movCC` / a predicated
      branch). gale #209 measured this on `control_step_decide`: 6 re-test sites,
      ~4 removable insns each ≈ 24 cyc ≈ 29% of the 84-cyc gap to native, and it
      recurs in every dissolved body with a comparison feeding a select
      (controller_step/filter_axis clamps, k_sem_give). Fix: a LATE peephole —
      when an i32 comparison's result is sole-consumed by a select/br_if in the
      same block with no intervening flag clobber, keep the condition in NZCV and
      emit the consumer as a single predicated movCC / conditional branch.
      Detection is local (def = comparison, single use = select/br_if), so it
      fits the existing SelectMove + reg_effect flag modeling (#279) without a
      flag-liveness rework. Byte-changing → deliberate fixture re-freeze. The
      companion finding (21% [sp] spill density on the sem path) is the VCR-RA
      allocator track, not this item.
      RE-CONFIRMED on v0.12.0 (gale #428, 2026-06-23): with loom v1.1.16's
      inline+DCE merging the gust_mix export wrapper (loom#228), gale isolated the
      gap to synth — gust_mix 2.81× → 2.63× LLVM (fn-only 1.125 → 1.05 ticks/call),
      frame 24 B → 8 B; "synth is now the SOLE remaining factor." The merged
      gust_mix lowered by synth 0.12.0 still shows the materialized-bool clamps
      (`cmp r4,r5; ite lt; movlt #1; movge #0; cmp #0; it ne; movne` ×2). gale
      re-ranks THIS (#4 cmp→select → IT-block predication) as the HIGHEST single
      win (~7 insns → 2-3, ×2 here), ahead of (3) immediate folding (`lsl #8` /
      `uxth` for the `movw r5,#8; lsl` and `movw r3,#0xffff; and` it also flagged)
      and (1) wiring the now-CI-gated allocator (#441) to drop the 6-reg leaf
      prologue. v0.12.0 shipped the DWARF (#440) + spill-pressure CI-gate (#441,
      regalloc GROUNDWORK/measurement — NOT a lowering fix) but not this. This is
      the NEXT DEDICATED GATED RELEASE (not an idle-tick increment): implement the
      late peephole, re-freeze the three frozen differentials (0x00210A55 /
      0x07FDF307 / divseam) result-identical, differential oracle, then gale's
      `benches/gust/src/bin/gust_codegen_bench.rs` (≤1.3× fn-only) is the agreed
      on-silicon kill-criterion.
      IMPLEMENTATION LANDED — SELECT HALF ONLY (2026-06-23, flag-off /
      frozen-safe). SCOPE: this PR lands the `select`→`movCC` half of the
      title's "select/br_if" fusion. The `br_if`→predicated-BRANCH half (a
      comparison sole-consumed by a conditional branch → keep NZCV, emit a single
      `bCC`) is NOT done — `fuse_cmp_select` matches only `SelectMove` consumers;
      branch consumers are unmodeled by `reg_effect` and never match. That half
      is a deferred follow-up (split candidate). The late peephole is
      `synth_synthesis::liveness::fuse_cmp_select` — deletes the
      `SetCond D,c` + select's `cmp D,#0` and retargets the predicated moves to
      `c` / `invert(c)` (the textbook predicated clamp). Wired into arm_backend.rs
      AFTER range-realloc, BEHIND `SYNTH_CMP_SELECT_FUSE=1` (default-off => a literal
      no-op => the three frozen differentials stay bit-identical, un-rerun). Proven
      sound by construction: flags reused only when nothing clobbers them in the
      `SetCond`->`cmp` window (`clobbers_flags` allowlist), and the bool deleted
      only when provably dead (`reg_dead_by_redef`, R0-live-out safe). Validation
      this step: 8 liveness unit tests (positive incl. the gust_mix x2 in-place
      clamp, 5 negative guards), 3 encoder byte-tests (all 10 IT conditions),
      rewrite-count>0 on real fixtures (control_step 3, flight_algo/controller 5-6),
      and an arm-none-eabi-objdump diff confirming `cmp r0,#19; movcc r5,r6` is
      emitted in place of the 5-insn materialize+re-test, with the unsafe sites
      (bool reused) correctly DECLINED. STILL OWED by the default-on flip step
      (NOT done here, deliberately deferred): execution-level differential under the
      flag (VCR-ORACLE-001 Rust unicorn harness) + gale's `gust_codegen_bench` on
      G474RE; only then does the flag flip default-on and the tag cut. EMPIRICAL
      GAP the flip differential MUST close: every fused site on the real fixtures
      was the IN-PLACE single-move form (`movCC`), so the two-move
      `moveq→mov{invert(c)}` path — the only place `invert()` matters at RUNTIME —
      has executed in unit/encoder tests but NEVER selector→fusion→encoder→exec on
      a real function. The flip's differential must include a fixture that forces a
      fusable NON-in-place select (e.g. `val2` a live param), or the `mov{!c}` path
      reaches silicon never having run (the #204/#206 IR-right/composition-wrong
      lesson). The `br_if`→predicated-branch half is separate deferred work.
      GALE BENCH + INVESTIGATION (#428, 2026-06-23): gale ran gust_codegen_bench
      (qemu -icount, M3 proxy): flag-off vs SYNTH_CMP_SELECT_FUSE=1 is CORRECTNESS-
      IDENTICAL over [0,2047], fn-only 1.05→0.95 ticks, 2.63×→2.375× LLVM, .text
      132→124 B — a monotonic correctness-preserving win. Two findings: (a) ≤1.3×
      is the COMBINED program target (VCR-VER-001), NOT this lever's gate — #1's
      gate is correct+not-slower+smaller, met on qemu; (b) gale's gust_mix clamp #2
      DECLINED while clamp #1 fused. ROOT CAUSE (verified via objdump of the
      synthetic two-move fixture scripts/repro/cmp_select_two_move.wat — NOT gale's
      "narrow dst-match" guess): `reg_dead_by_redef` requires an explicit downstream
      REDEFINITION of the boolean; the real selector ABANDONS the boolean temp after
      the select (used once, not live-out, never rewritten), so the guard
      conservatively declines. This is ONE mechanism unifying BOTH the clamp-#2
      decline AND the two-move-arm-never-fires gap: the two-move arm is effectively
      UNREACHABLE through the real selector today. Characterization test
      (cmp_select_two_move_coverage.rs) locks it (two-move fixture fuses 0,
      in-place control_step fuses >0). FOLLOW-ON (byte-changing, separate gated
      step): teach reg_dead_by_redef that "abandoned + not-live-out" is dead — this
      both closes gale's clamp-#2 coverage AND makes the two-move arm reachable, so
      the flip's owed two-move differential can finally run end-to-end. FLIP
      PRECONDITIONS (both, per gale exchange): (1) the two-move arm exercised
      end-to-end [blocked on this deadness follow-on], (2) gale's G474RE DWT-cycle
      run shows no M4-specific regression vs the qemu proxy (gale wiring it).
      DEADNESS FOLLOW-ON LANDED (#7, 2026-06-23, flag-off / frozen-safe):
      reg_dead_by_redef now recognizes the function RETURN terminator (`bx lr` /
      `pop {…,pc}`) — where live-out ⊆ ABI result regs {R0,R1} — so an ABANDONED
      boolean in R2..R8 (the shape the real selector emits) is proven dead and the
      two-move arm fuses end-to-end. Verified: the synthetic fixture now lowers to
      `cmp r0,r1; movlt r4,r0; movge r4,r2` — the `mov{invert(c)}` (movge) arm
      firing for the FIRST time, semantically identical to the select. Soundness
      locked by IR unit tests: positive (abandoned boolean + return ⇒ fuse) and the
      load-bearing negatives that keep it sound — result-reg boolean (d∈{R0,R1}),
      branch-in-tail, and bx-to-non-LR all still DECLINE (the scan bails on every
      Label/branch via reg_effect→None, never walking past a join point). Frozen
      byte gates #445/#446 stay GREEN flag-off (default path byte-identical).
      CENSUS LANDED (#450, 2026-06-23, flag-off / frozen-safe): a CI-gated fusion
      census (cmp_select_fusion_census.rs, via additive fuse_cmp_select_with_stats
      + SYNTH_FUSE_STATS in-place/two-move split) measured the blast radius across
      the frozen fixtures — 27 fused sites (control_step 3, flight_seam 12,
      flight_seam_flat 12, signed_div_const 0), ALL in-place. FINDING: the two-move
      count is ZERO on EVERY real frozen fixture — #7's `mov{invert(c)}` arm fires
      on no shipped fixture; its only exercisers are gale's gust_mix bench and the
      synthetic cmp_select_two_move.wat. CONSEQUENCE for the flip criteria: precond
      (1) "two-move arm exercised end-to-end" can ONLY ever be satisfied by gale's
      bench — there is no frozen-fixture path to regression-cover this arm, so
      gale's gust_codegen_bench is the SOLE runtime exerciser (load-bearing, not
      redundant), and the flip will ship without frozen-differential coverage of its
      novel path by construction. The census baseline asserts two_move==0 and fires
      loudly if a future selector change ever gives a real fixture coverage (a
      deliberate-bump + notify-gale event). STILL OWED / NOT claimed: (a) the
      two-move arm is reachable + objdump- and IR-correct but NOT execution-validated
      anywhere except via gale's bench (see census consequence) — watch correctness
      there. (b) "closes clamp #2" is by the same mechanism but UNVERIFIED locally
      (no gust_mix.wasm) — gale's bench confirms which clamps now fuse. The flip
      still gates on both preconditions above (now (1) is unblocked pending that
      gale bench, which the census confirms is the only possible exerciser).
      GALE CORRECTION + EXECUTION ORACLE (#428, 2026-06-23): gale ran flag-on
      gust_mix on gust_codegen_bench and the census CONSEQUENCE above was WRONG on
      one point — gust_mix does NOT exercise the two-move arm either. Both its
      clamps (incl the now-fusing clamp #2) lower to the IN-PLACE single-move form
      (`it; movlt`, dst preloaded with the false-case value); there is no
      `mov{invert(c)}` anywhere in flag-on gust_mix. So the two-move arm is exercised
      by NOTHING real — gale's bench included — and the SOLE exerciser is the
      synthetic cmp_select_two_move.wat. (#449 win still confirmed: 2.375x -> 2.125x
      LLVM, correctness-identical [0,2047], .text 132 -> 116 B.) RESOLUTION of precond
      (1): rather than the empirically-unsatisfiable "a real fixture exercises it",
      the synthetic is now EXECUTED, not just disassembled — scripts/repro/
      cmp_select_two_move_differential.py runs two_move_sel under unicorn (faithful
      Thumb-2 IT predication) flag-off vs flag-on vs wasmtime across a sweep that
      straddles the compare (both movlt and the movge=mov{invert(c)} arm fire; 7/11
      vectors hit movge incl signed-compare + i32-wrap edges). Result: 11/11
      off==on==wasmtime, the mov{invert(c)} arm runtime-validated for the FIRST time.
      CI-gated as an isolated job (cmp-select-oracle, unicorn pip-installed there
      only so cargo test --workspace is untaxed) = VCR-ORACLE-001 first deliverable.
      Non-vacuity guards: aborts unless flag-on has >=1 two-move fusion AND the sweep
      hits both arms. GALE EXHAUSTIVE SWEEP (#428, 2026-06-23, gale PR #102
      gale_decider_diff): independently covers precond (1) from the OTHER angle —
      behavioral equivalence on the WHOLE real primitive set. All 8 verified gale
      deciders (sem give/take, msgq put/get, mutex lock/unlock, event post/wait)
      dissolved loom->synth, every decision over each decider's full input domain
      folded into one FNV-1a checksum, 10,596 cases three-way: native-gale-wasm-ref
      == dissolved-0.12.0-flag-off == dissolved-flag-ON = 0x88e73178d232bcf5 (ALL
      identical). Proves (a) native==dissolved (no 0.12.0/loom-1.1.16 codegen
      regression) and (b) flag-off==flag-on changes ZERO decisions across the real
      primitive set (not just gust_mix); fusion fired widely (dissolved .text
      2574->2502 B). These deciders, like gust_mix, mostly lower single-move in-place
      — so the sweep is broad BEHAVIORAL coverage but does NOT exercise the two-move
      opcode; that unique runtime coverage stays the synthetic oracle above. TOGETHER
      they cover precond (1) both ways: exhaustive real-workload equivalence (gale)
      + the two-move opcode executed (synthetic). gale's harness is a reusable gate,
      re-run on each synth bump. Precond (1) now MET (synthetic execution + gale
      exhaustive sweep); precond (2) (G474RE silicon no-regression) still OWED —
      gale's bench is thumbv7m/qemu today — flip stays held on it (user call
      2026-06-23: keep the silicon gate; close the exec gap first).
      FLIP SHIPPED v0.13.0 (2026-06-24, #428): default-on landed. User authorized
      shipping on the qemu+sweep+oracle evidence and WAIVING precond (2) for the
      release (gale takes the on-silicon G474RE DWT no-regression as a tracked
      post-ship follow-up). Re-froze the fused .text on the same commit the
      named-anchor differentials were re-run on (control_step preserved 0x00210A55,
      flat+inlined flight_algo preserved 0x07FDF307; .text −262 B across the frozen
      fixtures). Escape hatch SYNTH_NO_CMP_SELECT_FUSE=1 reverts the lowering.
      SCOPE: the select half shipped; the br_if→predicated-branch half remains a
      separate follow-up (branch consumers unmodeled by reg_effect).
    status: implemented
    tags: [codegen, selector, peephole, compare-select, flag-fusion, gale-209, perf, track-b, vcr-oracle-001]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-SEL-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        A re-decode of control_step_decide shows NO `cmp <real>; ite; movCC #1/#0;
        cmp #0; it; movCC` round-trip for a comparison feeding a select (gale's
        kill-criterion); the three frozen differentials stay RESULT-identical
        (bytes re-froze, results preserved); gale confirms on-silicon
        control_step drops toward ~127 cyc (151 − ~24) and k_sem_give materially
        below 860 on the G474RE; flag-gated until that silicon confirmation.

  - id: VCR-RA-002
    type: sw-req
    title: Conditional register pool — free R10 when bounds-checking is off (track C)
    description: >
      R10 is reserved unconditionally ("memory size for bounds checks") but used
      ONLY in BoundsCheckConfig::{Software,Mpu,Masking} (verified:
      instruction_selector.rs ~3952). In BoundsCheckConfig::None it is a wasted
      reserve — a cheap +1 allocatable register (pool 9 -> 10) that directly
      relieves the const-remat/spill pressure the 9-register limit forces (the
      9-vs-12 gap to native). Make R10 allocatable iff bounds-checking is off.
      Composes with the allocator (which reads the pool size from config).
    status: proposed
    tags: [codegen, register-allocation, pool, reserved-registers, track-c, perf, release-v0.11.41]
    links:
      - type: derives-from
        target: VCR-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        With bounds-checking off, R10 is allocatable and flat_flight spill count
        decreases; all three differentials RESULT-identical; with bounds-checking
        ON, R10 stays reserved and bounds-mode codegen is byte-identical; gale
        confirms on-target equal-or-better. Deliberate fixture re-freeze (bytes
        change, result preserved) is part of landing it, not a violation.

  # ---------------------------------------------------------------------------
  # Research-driven additions (deep-research run wf_2310ef0b-097, 2026-06-10:
  # Crocus/regalloc2/CompCert-validation literature, 103 agents, 25 claims
  # adversarially verified). The headline: per-run translation VALIDATION with
  # a small mechanically-verified validator is the literature-consensus sweet
  # spot (Rideau/Leroy CC'10: equal soundness, ~10x less proof, invented for
  # register-poor targets) — so the validator, not the allocator, is the thing
  # to verify.
  # ---------------------------------------------------------------------------

  - id: VCR-RA-003
    type: sw-req
    title: Backward-dataflow allocation validator (Rideau/Leroy-style), then mechanize it
    description: >
      Evolve verify_allocation + the per-segment edge-recheck into a single
      backward-dataflow translation validator over (original, rewritten)
      segment pairs — the Rideau/Leroy CC'10 architecture (350-line validator,
      900-line Coq soundness proof in CompCert): refine liveness backward,
      checking that every use in the rewritten code reads a location provably
      holding the right value, covering renaming, coalescing, live-range
      splitting, spill/reload, and architectural register constraints in one
      pass. v1 = Rust, unverified but independent and complete for synth's
      transformation class, wired as the re-allocation pass's acceptance
      check and mutation-tested. v2 = Rocq-mechanized soundness (the
      tool-qualification pillar-1 artifact for the allocator, cheaper and
      stronger than proving the Chaitin/Briggs pass itself). Adaptations from
      the paper: synth validates phys-to-phys rewrites (treat input physical
      registers as variables); constant rematerialization is out of the
      validated class initially (decline, don't guess).
    status: implemented
    tags: [codegen, register-allocation, translation-validation, rocq, track-a, release-v0.11.39]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-RA-001
      - type: constraint-satisfies
        target: SC-CODE-1
    fields:
      req-type: safety
      priority: must
      verification-criteria: >
        v1 accepts every rewrite the current pass produces on the fixtures AND
        rejects mutation-injected wrong rewrites (>=95% mutant kill on a
        seeded corpus of bad renames/clobbers); wired as the gate the pass
        cannot bypass. v2: soundness theorem (validator-accepts implies
        behavior preserved) Qed against exec_indexed for the straight-line
        fragment. Kill-criterion: if the validator's decline rate on real
        selector output exceeds ~5% of segments, its completeness is too weak
        and the approach is re-evaluated (CompCert tested relative
        completeness empirically; so will synth).
        PROGRESS (criteria 1 + 3): the empirical real-codegen completeness gate
        (realloc_on_repro_fixture_streams_has_zero_validator_rejects) now spans
        the FULL ARM frozen suite — 32 functions / 57 segments across 10
        fixtures (was 3) — with 0 validator-attributable declines (0% << the 5%
        kill-criterion, which is now asserted explicitly, not just the stronger
        0 pin). v2 (Rocq-mechanized soundness) remains the open step.
        V-NEXT (from gale #331): extend the validator to the SPILL-SLOT /
        frame-allocation layer — it currently validates register rewrites in
        straight-line segments only, NOT frame-slot non-aliasing. #331 was a
        param-home vs spill-pool slot collision (`i64_spill_base` aliases the
        #204 `param_slots` when `has_i64 == false`); a "validate slot
        non-aliasing" invariant would have caught it mechanically. Fixed for now
        by an `area_reserved` guard on the call-result park (ladder-recoverable
        Err → retry reserves the area), but the validator does not yet cover this
        class.
        IMPLEMENTED (v0.48, epic #242): the V-NEXT spill-slot layer + the #490
        callee-saved class now ship as an UNCONDITIONAL single-stream final
        validator - `synth_synthesis::liveness::validate_final_allocation`
        (RaFinalVerdict / RaFinalViolation) - wired in `arm_backend.rs`
        immediately after `validate_instructions`, on EVERY ARM compile in the
        default `--features riscv` build (NOT verify-gated; the #757 dormant-in-
        shipping lesson). It hard-errors the compile on (1) callee-saved
        preservation #490 (a body def of R4-R8 not saved by a prologue
        `push {..,lr}` / not restored by a return `pop {..,pc}`) and (2)
        spill-slot non-aliasing — the class #331 EXEMPLIFIES (two
        simultaneously-live values sharing a frame slot: a reload after an
        unreloaded overwrite, per straight-line segment via the holder model).
        NOTE the scope honestly: the red test proves the aliasing CLASS is
        caught, NOT a reproduction of the historical #331 (whose param-home vs
        i64-spill collision may present as a caller/prologue-written home or span
        a segment boundary, outside this in-segment str/str/ldr shape). BOUNDED
        first increment = straight-line + spill/reload discipline only;
        branches / CF joins and unmodeled ops (calls / i64-pair / FP) are the
        NAMED PHASE-2 boundary (the spill check segments at them, never claiming
        cross-join coherence - a loud honest scope, never a false pass).
        The callee-saved check is FAIL-SAFE on unmodeled ops (calls / i64-pair /
        FP / BrTable): an op `reg_effect` cannot model MIGHT write R4-R8, so a
        no-prologue body containing one is flagged — the checker-correct
        (false-negative-avoiding) direction, mirroring the pass it validates
        (`body_uses_callee_saved`, which forces a push on None); verified to not
        false-positive (frozen + full workspace green). RED-FIRST non-vacuity
        proven (10 unit tests, `ra003_*` in liveness.rs): 4 RED synthetically
        revert a known-fixed clobber and assert the validator CATCHES it (revert
        #490 prologue -> CalleeSavedNotSaved; drop the epilogue restore ->
        CalleeSavedNotRestored; alias two live values on one slot ->
        SpillSlotAliased; an unmodeled op with no prologue -> fail-safe
        CalleeSavedNotSaved) + 6 GREEN assert it is SILENT on correct code (the
        real `ensure_callee_saved_prologue` output; balanced push/pop; a
        pure-scratch leaf; sequential single-slot reuse; an unmodeled op WITH a
        prologue; a call as a spill-segment barrier).
        Frozen-safe (emits nothing; `.text` byte-identical, control_step
        0x00210A55 / flight_algo 0x07FDF307) - the frozen suite compiling the
        whole ARM fixture set THROUGH the unconditional gate (10/10 green) is the
        silent-on-every-real-function proof. CI-gated:
        `vcr-ra-003-alloc-validator-gate` in ci.yml (red-first unit tests +
        frozen suite). Distinct from the PAIRWISE `validate_segment_rewrite`
        (which needs a pre-alloc reference and runs INSIDE the re-alloc pass):
        the final validator inspects the SINGLE emitted stream with no reference,
        so it checks only invariants whose reference lives in the stream. Placed
        in synth-synthesis (not synth-core) because ArmOp/Reg live there and the
        register-assigned stream is consumed in arm_backend before main.rs.
        ARM-scoped this increment; RV32 / AArch64 get their own arms later
        (per-backend, like VCR-VER-003).
        PHASE 2 (v0.49, #49) — WHOLE-FUNCTION across CALLS and JOINS: the named
        phase-2 boundary is now extended past straight-line with two more
        invariants, each anchored on a reference OUTSIDE inferred value-identity
        (the v0.48 vacuity lesson: generic GP-liveness on one stream cannot tell
        a clobber from a redefinition). (3) CALLER-SAVED PRESERVATION ACROSS A
        CALL: a value in R2/R3/R12 defined before a bl/blx/call and read after it
        with no intervening redef crossed a boundary the AAPCS is contractually
        allowed to clobber -> `CallerSavedLiveAcrossCall`; the reference is the
        ABI contract at the call, not an inferred value. R0/R1 are EXCLUDED (a
        call DEFINES them: the return value) - a documented false-NEGATIVE
        boundary (FN < FP). Reasoned locally at the call site; does NOT modify the
        shared `reg_effect` (whose None-on-call meaning the phase-1 callee-saved
        fail-safe and `eliminate_unread_frame_stores` both depend on). (4) VALUE
        AVAILABILITY ACROSS A JOIN: a register live-in to a CF join (>=2 preds)
        must be AVAILABLE - must-defined on EVERY incoming path, or an entry
        live-in -> else `JoinValueNotAvailable`. Solved by a forward MUST
        (intersection) availability fixpoint (UNIVERSE-init, not empty - it is a
        must-analysis) over a DEDICATED join CFG (`build_join_cfg`) that admits
        `bx lr` returns (sinks) and calls (fall-through with a caller-saved
        def-set), so branchy functions with calls/returns remain analyzable
        instead of wholesale-declining. Entry seed = params R0-R3, SP, LR, AND the
        RESERVED registers R9/R10/R11/R12 (`contracts::regalloc::RESERVED_REGS` -
        R11 = linmem base etc., never allocated, resident by construction);
        seeding them is REQUIRED to avoid a false positive on every
        memory-touching branchy function (the block_brif_483 `nested` case: a
        `str [r11,#off]` at a join, R11 defined nowhere in the stream - this lane
        FOUND + FIXED that regression). RaFinalVerdict gains `NotAttempted {
        reason }` - a LOUD honest decline when the join CFG cannot be built
        (numeric branch, BrTable, computed Bx, duplicate label); NON-FATAL at the
        arm_backend call site (only Violation hard-errors), so a construct the
        checker cannot model never blocks a correct compile but is also never
        silently passed. RED-FIRST non-vacuity extended (17 `ra003_*` tests): +2
        RED assert the SPECIFIC violation (a caller-saved value live across a bl
        -> CallerSavedLiveAcrossCall; a value in R4 on one join path but not the
        other -> JoinValueNotAvailable), +4 GREEN (return-value-after-call,
        callee-saved-across-call, both-paths-define, dominator-defined at a join),
        +1 NotAttempted (BrTable -> loud decline). Vacuity-in-practice VERIFIED:
        invariant 4 FIRES on real branchy codegen (if_else_result_343 /
        cf_shapes_500 / block_brif_483 joins all Consistent, incl. a real R11
        availability check) - not unit-tested-but-dead-in-shipping.
        HONEST PATH SCOPE: invariant 4 FIRES (analyzable label-form CFG) on the
        RELOCATABLE / direct-selector path; on the DEFAULT optimized path branches
        are already resolved to NUMERIC offsets (BOffset/BCondOffset) before the
        validator runs, so the join CFG cannot be built and invariant 4 declines
        to NotAttempted THERE (invariants 1-3 still run on both paths - a
        false-positive Violation on either would hard-error the compile). Verified
        BOTH paths: control_step on the DEFAULT path (the control_step
        differential's own input) + 7 branchy fixtures × {relocatable, default} =
        16 pairs, 0 false positives; the full 130-fixture default-path sweep is
        also 0 violations. The NotAttempted decline is COMMON on the default path
        (~41/130 fixtures), so its diagnostic eprintln is gated behind
        `SYNTH_RA003_VERBOSE` (a production compile stays quiet; the verdict is
        observable on demand). Extending invariant 4 to the numeric-branch
        optimized path (a resolved-offset CFG builder, the #606 geometry) is a
        NAMED follow-up. CI-gated: the third `vcr-ra-003-alloc-validator-gate`
        step runs `scripts/repro/vcr_ra_003_phase2_join_call.py` over
        branchy/mem/call fixtures on BOTH paths (silent-on-real-branchy-codegen).
        Frozen-safe (emits nothing; control_step 0x00210A55 / flight_algo
        0x07FDF307 byte-identical, 10/10). v2 (Rocq-mechanized soundness of the
        straight-line fragment) remains the open step.
        RV32 ARM LANDED (v0.50, #815) — the per-backend RV32 analogue promised at
        "RV32 / AArch64 get their own arms later" now ships: a PARALLEL
        re-implementation `synth_backend_riscv::alloc_validator::
        validate_final_allocation_rv32` (RaFinalVerdict / RaFinalViolation in that
        crate), keyed on the RV32 calling convention — NOT a reuse of the
        ARM-coupled `validate_final_allocation` (different instruction enum
        RiscVOp, different callee-saved set, different `addi sp,-N` + `sw s_k`
        prologue shape). Wired UNCONDITIONALLY in `backend.rs`
        (`compile_function_with_opts`, on `selection.ops` immediately after the
        selector) on EVERY RV32 compile in the default `--features riscv` build
        (both `compile_module` — the ELF path — and `compile_function` reach it),
        hard-erroring on a Violation. Two STRAIGHT-LINE invariants (the two #815
        names): (1) CALLEE-SAVED PRESERVATION — a body write (op_dest) of an
        s-register the pass saves (s1, s2..s10 = `is_callee_saved_temp`, mirroring
        `preserve_callee_saved` EXACTLY; the reserved s0/fp + s11/linmem-base are
        excluded so the checker never false-positives on the pass's own output)
        must be saved by a prologue `sw s_k, off(sp)` and restored by every
        epilogue `lw s_k, off(sp)` before a `ret` (jalr x0,0(ra)) ->
        CalleeSavedNotSaved / CalleeSavedNotRestored; (2) SPILL-SLOT NON-ALIASING
        — the same holder model as the ARM validator, per straight-line segment,
        an `addi sp` frame adjust resetting the slot map (the RV analogue of ARM's
        `ldr sp,[sp,#N]` clear) -> SpillSlotAliased. A `Call` is the ARM
        phase-2 across-call/across-join frontier (no RV `cfg_liveness` yet) ->
        NON-FATAL NotAttempted { reason: "rv32-call-boundary" } (decline > guess;
        the two straight-line invariants still ran). DELIBERATELY NO
        "unmodeled-op → force-prologue" fail-safe (unlike ARM): on RV every
        op_dest==None op is CF/system/label/call and writes no s-register, so the
        fail-safe would be vacuous AND disagree with the pass -> a false-positive;
        omitting it keeps validator↔pass agreement. RED-FIRST non-vacuity (8
        `ra003rv_*` unit tests in alloc_validator.rs): 3 RED synthetically revert a
        known-fixed clobber and assert the CATCH (drop the prologue save of a used
        s2 -> CalleeSavedNotSaved; drop the epilogue restore -> CalleeSavedNotRestored;
        alias two live values on one slot -> SpillSlotAliased) + 4 GREEN assert
        SILENT (the balanced save/use/restore leaf; a pure-scratch t0/a0 leaf;
        sequential single-slot reuse; a Call -> NotAttempted) + 1 asserting a
        straight-line Violation BEFORE a Call still fires (the Call does not mask
        it). SILENT-ON-REAL-CODEGEN: the frozen RV32 oracle
        (`frozen_fixtures_rv32_text_is_bit_identical_oracle_001`, control_step
        0x00210A55) compiles through the unconditional validator — 0 false
        positives, byte-identical — PLUS a dedicated repro
        (`scripts/repro/vcr_ra_003_rv32_alloc_validator.py`) sweeps 9 RV32 fixtures
        × {relocatable, default} = 18 pairs (callee-saved-heavy control_step /
        controller_step, spill-heavy gust_kernel, branchy flight_seam, call-bearing
        reachable_helper) with 0 validator false-positives. CI-gated:
        `vcr-ra-003-rv32-alloc-validator-gate` in ci.yml (red-first unit tests +
        frozen RV32 oracle + the silent-on-real repro). AArch64 arm still open (the
        integer subset has minimal spill traffic; a NAMED follow-up).

  - id: VCR-RA-004
    type: sw-req
    title: Cycle-safe parallel-move resolver for spill/reload insertion
    description: >
      Step-4 spill insertion adds moves that form arbitrary permutations
      (including cycles) at split points. The literature names this the
      correctness-critical sub-piece (CompCert proves its parallel-move
      algorithm separately, Rideau/Serpette/Leroy; regalloc2 needs a scratch
      register, a stackslot-as-scratch fallback, and a last-ditch emergency
      spill). Build the resolver as its own pure, testable component:
      sequentialize a parallel move set with cycle detection, scratch
      selection from dead registers, and a guaranteed-progress fallback;
      property-tested against a reference permutation semantics. The second
      named pitfall — split points landing inside hot loops — is bounded at
      this stage by synth's straight-line segment scope (no interior loops),
      and re-checked when segments widen.

      DELIVERED v0.11.38 — `synth_synthesis::parallel_move` (`sequentialize`),
      a pure module with no compiler state: destinations must be pairwise
      distinct (anything else is a caller bug and is REJECTED, not guessed at);
      self-moves are dropped; phase 1 emits chain moves leaf-first from a
      worklist until what remains is exactly a set of disjoint cycles; phase 2
      breaks each cycle through a scratch register filtered against the move set,
      or — when no scratch survives the filter — through ONE self-bracketing
      stack-scratch pair (`MoveStep::SpillScratch` / `ReloadScratch`, lowered by
      the consumer to `str`/`ldr [sp, #resolver_slot]`). That stack fallback is
      the "guaranteed-progress" clause: there is no fixpoint-and-hope loop —
      phase 1 removes exactly one pending move per pop, the phase-2 walk removes
      one per step against the disjoint-cycle invariant, the outer loop ASSERTS
      the pending set strictly shrank, and the emitted sequence is asserted
      bounded by `moves.len() + 2 * cycle_count` before returning.

      CONSUMED, twice, and each time it removed a real defect rather than only
      adding a component:
        * v0.11.39 (#327, gale #326): `emit_arg_moves` call-marshalling. The old
          cycle-breaker DEMANDED a callee-saved register, so the dissolved
          k_mutex_unlock hard-failed under saturation; it also MISCOMPILED
          genuine 2-swaps (duplicated a value). Phase 1 emits the
          lowest-destination ready move first — exactly the order the legacy
          `emit_parallel_move` produced for ascending-destination arg lists — so
          wiring the resolver in was byte-invisible for everything that already
          compiled.
        * v0.53 (#881, GI-FPU-002): VFP register-file spilling. `VCR-RA-001`
          gave the INTEGER file Belady spilling in v0.24 but the VFP file never
          got it, so five falcon v1.128 entry points died on `S0..S15 all live`
          / `caller-saved VFP D-register file exhausted`. Both files now spill
          and reload, and the swap/cycle cases go through THIS resolver. This is
          the delivery the v0.53 notes tagged `VCR-RA-004`; the status field is
          what had not been flipped (#893).

      STATUS IS `implemented`, NOT `verified`, deliberately. All three
      verification-criteria clauses have evidence (below), but no `sw-verification`
      artifact linked `verifies` to this requirement until v0.55 (#893), and the
      second named pitfall — split points landing inside hot loops — is still
      bounded by assumption (synth's straight-line segment scope, no interior
      loops) rather than by a check that fails when segments widen. That
      re-check remains open and is stated here rather than implied away.
    status: implemented
    tags: [codegen, register-allocation, parallel-move, spilling, track-a, release-v0.11.38, release-v0.53, synth-327, synth-881, synth-893]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-RA-001
    fields:
      req-type: functional
      priority: must
      verification-criteria: >
        Property test: for random permutations (incl. cycles, swaps,
        self-moves) over 1..9 registers with 0..2 free scratch regs, the
        sequentialized moves produce the permutation's final state; spill
        insertion on a synthetic over-pressure module compiles and runs
        result-identical to wasmtime; no resolver path can emit an
        unbounded-progress sequence.

        MET, clause by clause — the linked verification artifact carries the run
        recipe and the honest bound:
        (1) `property_random_move_sets_match_parallel_semantics`
        (crates/synth-synthesis/src/parallel_move.rs) runs 2000 deterministic
        iterations over R0..R8 — alternating a FULL random permutation
        (guaranteeing cycles and self-moves) with a partial move set (chains,
        fan-out, self-moves, cycles) — and re-runs each against scratch sets of
        size 0, 1 and 2, i.e. 6000 sequentializations, each checked against a
        reference parallel semantics and against the size bound. Twelve directed
        cases cover the named shapes explicitly (two_swap, three_cycle,
        two_disjoint_cycles, chain_into_cycle, the scratch-collision filter, and
        the no-scratch stack pair).
        (2) `scripts/repro/high_pressure_i32.wat` + its unicorn-vs-wasmtime
        differential: hard `Err` on v0.11.37, 6/6 on v0.11.38. v0.53 (#881) adds
        the spilled-VFP differential — 7 shapes on `-t cortex-m7dp
        --relocatable`, 109 rows bit-identical to wasmtime, NaN-aware per WASM
        §4.3.3, with the internal `bl` resolved by a REAL link so an unresolved
        relocation cannot be silently skipped.
        (3) Unbounded progress is excluded structurally, not empirically: the
        `moves.len() + 2 * cycle_count` bound and the strictly-shrinking pending
        set are `assert!`s in the resolver itself, so a violating path aborts
        rather than emitting.
        OPEN: the "split points inside hot loops" pitfall is still bounded by
        synth's straight-line segment scope, and the re-check owed when segments
        widen does not exist yet.

  - id: VCR-DEC-001
    type: sw-req
    title: "Decision: Chaitin/Briggs colouring over backtracking-bundle allocation — rationale + revisit trigger"
    description: >
      The production fast-compile Wasm allocators are NOT graph colouring:
      regalloc2 (IonMonkey lineage) is a backtracking allocator over precise
      live ranges (bundles, priority-queue assignment, eviction, on-demand
      splitting), LLVM-greedy is the same family, and regalloc3
      (github.com/Amanieu/regalloc3, active 2026) continues that line as
      regalloc2's designed successor. synth deliberately stays on
      Chaitin/Briggs + value-range splitting because (a) an AOT embedded
      compiler's compile-time budget tolerates colouring, (b) the colouring
      decision layer is simpler to translation-validate (VCR-RA-003) and its
      interference convention matches the proof substrate, and (c) the
      regalloc2 transition data shows the win comes from live-range
      SPLITTING + sophistication, which synth gets via value ranges, not from
      the backtracking search per se. REVISIT TRIGGER: if, after VCR-RA-001
      acceptance, gale's on-target benches still show >=10% cycle gap
      attributable to allocation (spill placement / split quality), evaluate
      adopting or porting regalloc3's bundle model behind the same validator
      — the validator (not the allocator) carries the assurance, so the
      algorithm can be swapped without re-doing proofs (the exact decoupling
      Rideau/Leroy name as validation's advantage).
    status: approved
    tags: [codegen, register-allocation, decision, regalloc3, track-a]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-RA-001
    fields:
      req-type: constraint
      priority: must
      verification-criteria: >
        The revisit trigger is checked at VCR-RA-001 acceptance (v0.11.40
        gate): an explicit measured statement "allocation-attributable gap
        <10% or regalloc3 evaluation filed" appears in the release notes.

  - id: VCR-REACH-001
    type: sw-req
    title: "VCR-DEC-001 increment 4: REACH — widen the shared op model to the i64 register-pair pseudo-ops (`pair_effect`)"
    description: >
      Increments 2 (joins, v0.53) and 3 (calls, v0.54) both returned the same
      verdict — DO NOT FLIP — and for the same reason: the limiting factor is
      REACH, not soundness. Every function the colourer emits is VCR-RA-003-
      clean, `validate_cfg_rewrite`-clean and (since v0.54) clean under the ABI
      observable contract;
      it simply DECLINES too often to dominate the greedy allocator. The v0.54
      decline histogram over the 633-function ARM repro corpus (relocatable
      path) is `unmodeled-op` 175, `single-block` 73, `identity-colouring` 31,
      `call-indirect-pseudo` 17, `unreachable-block` 11, `numeric-branch` 10 —
      so `unmodeled-op` is 47 % of all declines and the single biggest bucket.
      A per-function census of WHICH ops force that decline (the complete set,
      not just the first blocker) attributes 167 of the 175 to ONE coherent
      family: the i64 register-pair pseudo-ops (`I64Const` 96 functions,
      `I32WrapI64` 61, `I64Shl` 51, `I64Ldr` 36, `I64ShrU` 28, `I64Str` 28,
      `I64SetCond` 22, then a long tail); the residual 8 are `MemorySize` /
      `MemoryGrow`. This increment models that family.

      METHOD — a NEW shared definition, never a widened `reg_effect`.
      `liveness::reg_effect` returns `None` for these ops DELIBERATELY, and the
      SHIPPING pipeline depends on that `None`: `local_dead_defs`,
      `reallocate_function` (`SYNTH_SPILL_REALLOC`, default-on since v0.24.0),
      the range-realloc pass and `fuse_cmp_select`'s dead-by-redef check all
      bail on it. Turning it into `Some` would silently hand the greedy/segment
      allocator streams it has always refused and break the frozen anchors. So
      increment 4 follows increment 3's `call_effect` pattern exactly: ONE new
      definition, `liveness::pair_effect`, consumed by BOTH the pass
      (`graph_alloc::joins` liveness / interference / pins) AND its oracles
      (`validate_cfg_rewrite`'s backward transfer, VCR-RA-003's independently
      written CFG builder). `reg_effect` is untouched, so flag-off output is
      byte-identical BY CONSTRUCTION.

      METHOD — the model is verified against the ENCODER, not the IR
      declaration. These are pseudo-ops EXPANDED downstream, the exact class
      increment 3 declined `Call`/`CallIndirect` for ("the register footprint
      this pass would colour is not the one that ships"). A naive
      `defs = {rd_lo, rd_hi}` model is WRONG for several of them and would be a
      blind spot COMMON TO ALL THREE INSTRUMENTS — #872's standing lesson. Each
      admitted op must therefore pass three checks against the real expansions
      in `arm_encoder.rs` (BOTH the Thumb-2 and the A32 path):
        1. FOOTPRINT — does the expansion write a register outside the naive
           def set? (`I64Shl`/`I64ShrU`/`I64ShrS` overwrite `rm_lo` via
           `AND rm_lo,rm_lo,#63` and use `rm_hi` as a pure temporary clobber.)
        2. IMPLICIT DISTINCTNESS — a `defs`/`uses` `RegEffect` structurally
           cannot express "these two operands must differ", so it is checked
           separately and discharged with PRE-COLOURED INTERFERENCE EDGES, not
           with a wider effect set. (`I64Ldr` emits
           `LDR rdlo,[base,#off]; LDR rdhi,[base,#off+4]`, so coalescing `rdlo`
           onto `base` — which a plain interference graph will do whenever
           `base` is dead after — makes the SECOND load read a clobbered base.
           `I64Const` needs `rdlo != rdhi`.)
        3. RENAME-INVARIANCE — the expansions are hand-emitted raw halfwords
           with FIXED internal branch offsets, so any 16-bit register form
           inside makes a rename unsafe (the #180 / #311 / H-CODE-9 class). An
           op carrying one is DECLINED by name, not guessed at.
      An op that fails a check keeps its decline and the decline is RENAMED so
      the residual stays actionable — the decline MOVES, it is never deleted.
    status: proposed
    tags: [codegen, register-allocation, graph-colouring, reach, i64, track-a]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-DEC-001
      - type: refines
        target: VCR-RA-001
      - type: traces-to
        target: VCR-RA-003
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        (1) `SYNTH_GRAPH_ALLOC` stays OFF by default and flag-off output is
        byte-identical — the frozen anchors stay 10/10 and the corpus byte
        totals with the flag off are unchanged from v0.54.
        (2) EVERY function the pass emits is clean under all three instruments
        — `validate_cfg_rewrite`, VCR-RA-003 `validate_final_allocation`, and
        the v0.54 ABI observable contract `abi_contract::validate_abi_contract` (`NotAttempted` counts as a
        DECLINE, never as a pass).
        (3) Necessary but NOT sufficient: increments 2 and 3 EACH found a real
        miscompile that both liveness-equation validators accepted and only
        EXECUTION caught. The new i64-pair shapes are therefore also executed
        against wasmtime by
        `scripts/repro/vcr_dec_001_join_alloc_execution_differential.py`, and
        the new coverage is proven NON-VACUOUS BY MUTATION: removing the
        `rm_lo`/`rm_hi` clobbers from a shift op's `pair_effect`, or dropping
        the `rdlo`—`base` interference edge, must turn the differential RED.
        A mutation that stays green means the fixture does not keep the
        clobbered value live across the op and the coverage is vacuous.
        (4) The DELIVERABLE is the measurement: applied-function count, the
        updated decline histogram WITH the corpus size (the corpus grows as
        lanes add fixtures — 617 at v0.53, 633 at v0.54), and the byte delta
        (ELF symtab) plus cycle delta (`--emit-wcet` sound bounds) against BOTH
        the greedy allocator and increment 3. That measurement is the v0.56
        flip-criterion input. Reach converts to BYTES only through
        `shrink_callee_saved_saves`, which is LEAF-ONLY, so a modest byte delta
        with a large reach delta is the EXPECTED result, not a failure.

  - id: VCR-DEC-002
    type: sw-req
    title: "Decision: spill-reduction leapfrogs greedy heuristics — optimal-because-tiny + SSA-chordal + proof-carrying facts (gale #209)"
    description: >
      gale's #209 strategic framing (2026-06-14, on G474RE composed-bench data:
      t_lock +82%, handoff +21%, dominated by 21-34% `[sp]` spill density):
      the spill-reduction increment must NOT re-implement LLVM/GCC greedy
      heuristics — those are heuristic ONLY because they must scale to
      million-instruction TUs. synth's hot kernels are tiny (sem 83, mutex 167,
      control_step 113 insns), so the scaling constraint does not apply, which
      unlocks three shortcuts a mature backend cannot retrofit:
      (1) OPTIMAL allocation — PBQP (Scholz-Eckstein) or a small ILP is
      tractable in ms at <200 insns -> provably minimal spills, not greedy
      leftovers; directly attacks the measured `[sp]` density and beats
      LLVM-by-construction on exactly the functions that matter.
      (2) SSA-CHORDAL coloring (Hack 2006) — on SSA the interference graph is
      chordal -> optimal coloring in P-time; LLVM/GCC destruct SSA before
      regalloc so they cannot use this. Aligns with VCR-RA-001's SSA substrate.
      (3) PROOF-CARRYING optimization facts — pipe Verus's value-range /
      no-overflow / alias facts (we own Verus -> wasm -> loom -> synth) into
      synth as optimization inputs (narrower types, elided bounds/overflow
      guards). The lever that makes verified code FASTER than defensive C.
      TENSION with VCR-DEC-001: that decision chose Chaitin/Briggs (heuristic)
      for translation-validation simplicity; #209 argues optimal is tractable
      AND the validator (VCR-RA-003), not the allocator, carries assurance, so
      an optimal core can sit behind the same validator. Resolve at the
      spill-reduction increment: evaluate PBQP/ILP + SSA-chordal against the
      Chaitin/Briggs baseline under VCR-RA-003, pick by measured spill count +
      validation cost. Target: below LLVM-LTO on the tiny hot kernels, not
      merely parity. Pairs with loom#219 (dissolve the seam first, then
      allocate the smaller result optimally).
    status: proposed
    tags: [codegen, register-allocation, decision, optimal, pbqp, ssa-chordal, proof-carrying, gale-209, track-a]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-RA-001
      - type: refines
        target: VCR-DEC-001
      - type: traces-to
        target: gale:209
    fields:
      req-type: constraint
      priority: should
      verification-criteria: >
        At the spill-reduction increment, the release notes report: the chosen
        allocation core (optimal PBQP/ILP vs Chaitin/Briggs), the measured spill
        count before/after on the hot kernels (sem/mutex/control_step), and
        gale's G474RE composed-bench delta against the 860/472 baselines (kill-
        criterion: t_lock << 887, handoff < 1661). All frozen fixtures stay
        bit-identical at every step.

  - id: VCR-DEC-003
    type: sw-req
    title: "Decision: emit `synth-provenance-v1` branch-transformation map for witness MC/DC source-to-object reconciliation (#396, witness#130)"
    description: >
      witness (#396, PR witness#130 — reconciler + `witness object-disposition`
      CLI landed AHEAD of synth) defines the contract synth must emit so MC/DC
      coverage measured on the WASM can be reconciled against the object code
      synth's branch folding/splitting actually produces. Schema
      `synth-provenance-v1`: a list of entries
      `{ func_index, instruction_offset, kind, count?, scry_evidence? }` where
      `kind ∈ preserved | folded-predication | eliminated-constant |
      split-into-object-branches`. witness's reconciler maps each to an
      object-verdict: preserved/folded-predication → obligation-stands (WASM MC/DC
      authoritative); eliminated-constant → justified-infeasible (carries optional
      scry#51 evidence); split-into-object-branches → needs-object-coverage (N new
      object obligations); an object branch witness never instrumented →
      only-in-synth divergence (surfaced, not hidden). Output extends the
      rivet-evidence schema as `witness-object-disposition-v1`.

      FEASIBILITY — the join key ALREADY EXISTS in synth. witness keys by the WASM
      `(func_index, byte_offset)` (from walrus `InstrLocId`); synth's decoder
      records exactly this as the `op_offsets` side-table (VCR-DBG-001 step 1,
      SWVER-016 — per-op WASM byte offset, parallel to ops, per function). No
      decoder/manifest change is needed on either side; an if/else's two arms share
      one WASM op offset (one `if` instruction), matching witness's intentionally
      many-to-one join (emit one entry per WASM instruction, not per witness
      branch-arm).

      TAXONOMY maps cleanly onto synth's real transformations: folded-predication =
      the cmp→select→IT fuse (VCR-SEL-004, SYNTH_CMP_SELECT_FUSE, default-on);
      eliminated-constant = constant-condition guard elision (Opt-1a) carrying
      scry#51 reachability evidence; split-into-object-branches = `br_table`
      lowering (#508) and the i64 ops that expand one WASM branch into a multi-cmp/
      branch object sequence (I64SetCond / I64Shl / I64DivU / …); preserved =
      every 1:1 `br_if`.

      OFFSET-NORMALIZATION DOMAIN — RESOLVED on synth's side (#396, 2026-06-27):
      synth's `op_offsets` are ABSOLUTE byte offsets into the original `.wasm`
      binary, verified from code — `wasm_decoder.rs` feeds the whole module to
      wasmparser (`Parser::new(0).parse_all(wasm_bytes)`, base 0) and reads per-op
      offsets via `into_iter_with_offsets()` (whole-buffer positions, NOT
      function-body-relative). walrus `InstrLocId` is the same origin (offset in
      the original Wasm buffer), so the join is DIRECT — no per-function header
      subtraction, no normalization. Pending only witness's confirmation of the
      walrus side. The replacement invariant to carry in the contract: both tools
      must key off the SAME input `.wasm` bytes (witness measures the module before
      synth lowers it; if witness re-serializes via walrus, the `InstrLocId`s must
      refer to the bytes synth then compiles).

      EMITTER MILESTONE — LANDED (v0.45.0, PR feat/45-396-mcdc-provenance). The
      `synth-provenance-v1` map is emitted behind `--emit-provenance` as a JSON
      sidecar (`<output>.provenance.json`), frozen-safe (ELF byte-identical with
      and without the flag, verified on control_step.wasm). The emitter derives
      provenance POST-HOC at the CLI from the compiled op stream + `op_offsets` +
      the ARM `line_map` and a new object-branch side-table `BranchMap`
      (`crate::backend::BranchClass`, captured at the ARM encode loop parallel to
      `line_map` — the one datum post-hoc CLI derivation could not recover: which
      emitted instruction IS a conditional branch vs a predicated move).
      GATE-EXERCISED kinds (BOUNDED v1): `preserved` (br_if/br),
      `folded-predication` (select → IT-block predicated move, no branch),
      `split-into-object-branches` (br_table, `count` = object branches) — all
      three asserted on the reconciliation fixture. `eliminated-constant`
      (fact-spec-dropped source branch, derived from the `kept` set) is WIRED in
      the schema + emitter with the correct byte-offset join key, but not yet
      gate-exercised (fact-spec deletions today are pure condition slices +
      proven-dead `if` regions; a fixture that drops a covered branch op is a v1
      follow-up). Every entry carries its object realization (`object_pcs`), and a
      per-function `object_cond_branches` list reconciles every REAL object
      conditional branch back to its source condition — an object branch no
      covered source op explains is surfaced with `resolved: false` + a note
      (i64-expansion / trap-guard), NOT hidden. The reconciliation gate
      (`provenance_reconciliation_396`, CI job `provenance-gate`) is non-vacuous:
      it asserts clauses (a) every object cond branch resolves and (b) the folded
      select is recorded folded with its predicated object PC — verified RED under
      an adversarial mislabel of SelectMove. FOLLOW-UP (uncovered in v1, named):
      the optimized `ir_to_arm` path may drop `source_line` on some op shapes
      (verified: this fixture keeps it on both the direct AND optimized paths) —
      a function whose `line_map` came back all-None is LOUD-DECLINED from the
      sidecar (warn + skip) rather than mislabeled; i64-expansion/trap-guard
      object branches are surfaced-unresolved rather than reconciled; RISC-V/
      AArch64 carry no `branch_map`; the eliminated-constant fixture; witness#130
      `object-disposition` end-to-end compose.
    status: implemented
    tags: [witness, mcdc, traceability, provenance, vcr-dbg, decision, integration, synth-396]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-DBG-001
      # synth#396 (the MC/DC source-to-object obligation this decision settles the
      # contract for) is tracked in rivet as VCR-COV-001 — the issue body says so
      # verbatim ("Tracked in rivet as VCR-COV-001, sibling to VCR-DBG-001") and
      # VCR-COV-001's title carries "(synth #396)". A GitHub ISSUE NUMBER is not an
      # artifact id; the link belongs on the artifact, and the issue number stays in
      # the title/tags where it is a reference rather than a resolvable target.
      - type: traces-to
        target: VCR-COV-001
      - type: traces-to
        target: witness:130
    fields:
      req-type: constraint
      priority: should
      verification-criteria: >
        Contract-settling step (this artifact): the `synth-provenance-v1` schema +
        kind-taxonomy + join-key (op_offsets) are agreed with witness on #396, and
        the offset-normalization domain is resolved. Implementation milestone
        (separate): `witness object-disposition --manifest m.witness.json
        --provenance synth-map.json` composes end-to-end on a shared fixture, with
        each kind producing its specified object-verdict; the emitter is frozen-safe
        (no frozen `.text` byte changes — control_step 0x00210A55, flight_algo
        0x07FDF307).

  - id: VCR-PERF-001
    type: sw-req
    title: "Silicon-quantified gust hot-path size gap: 3.9× vs LLVM, per-pass attribution (gale #390)"
    description: >
      gale #390 (2026-06-20, synth v0.11.50 / loom v1.1.14, gust mini-RTOS
      dissolve, thumbv7m disassembly): synth's wasm→ARM lowering emits 3.9× the
      code size of native rustc/LLVM on the gust scheduler hot path — gust_poll
      816 B (240 insns) vs 208 B (104), gust_mix 44 B vs 12 B. The input wasm
      from loom is already compact; the gap is almost entirely synth-side
      lowering. This SUPERSEDES gale #209's qualitative "regalloc is the
      universal lever" with hard per-category byte attribution, and is the
      measurement / kill-criterion the VCR-RA program (epic #242) was waiting
      for. Attribution of the 608 B gap (per gale's disassembly):
        - Pass 1 — NO register allocation: every wasm local/operand spilled to a
          stack slot, the `sched` pointer reloaded from [sp,#0x3c] 10×. ~288 B
          (47%). OWNER: VCR-RA-001 + the allocator-wiring substrate (built:
          interference graph, Chaitin/Briggs color_graph, spill-cost ranking,
          allocation verifier — all side-by-side, UNWIRED). #390 is the payoff
          number that justifies wiring. THE HEADLINE.
        - Pass 2 — const linmem offset not folded into the addressing mode;
          scaled-index `ldr.w rD,[rN,rM,lsl#k]` unused; address materialized in
          r12 before every access. ~128 B. OWNER: addressing-mode folding,
          EXTENDS #382 fold_mem_offset (which folded the const-BASE path; the
          reg-base fold + scaled-index is new).
        - Pass 3 — `__stack_pointer` shadow-stack prologue/epilogue emitted even
          when the function touches no linmem below the frame (gust_poll is
          by-pointer, needs no shadow stack). ~64 B. OWNER: VCR-MEM-001 (#383) +
          scry. CONVERGENCE: this is the SAME analysis as #383 at a third
          granularity — scry's analyze().stack_usage.max_stack_bytes proves the
          worst-case depth; Bytes(0) ⇒ the whole prologue/epilogue is provably
          dead and ELIDED (not just the .bss shrunk). Unblocked by the scry
          integration (scry#51, VCR-MEM-001 layer-2).
        - Pass 4 — comparison feeding only a br_if materialized as bool+cmp#0
          instead of branching off flags. ~46 B. OWNER: VCR-SEL-004 (already
          filed, gale #209).
        - Pass 5 — no copy coalescing (identity mov survive); `and #0xffff` not
          peepholed to `uxth`. ~6 B. OWNER: regalloc coalescing + peephole.
        - Pass 6 — unconditional callee-save of r4–r8 in leaf-ish wrappers.
          ~4 B/fn. OWNER: prologue minimization (save only clobbered).
      Passes 1+3 dominate. Estimated 1–3 alone bring gust_poll from 816 B toward
      ~300–350 B (≈1.5–1.7× vs LLVM), within the project's 10–20%-overhead thesis.

      IN-TREE Pass-1 BASELINE (2026-06-21, frozen-safe, `scripts/repro/spill_baseline_measure.sh`):
      gale measured Pass-1 on gust silicon; this reproduces the SAME mechanism on
      synth's own frozen fixtures so the spill waste is regression-tracked in-tree
      (zero codegen change — compiles the fixtures, reads emitted ARM via thumb
      objdump + the existing SYNTH_SHADOW_ALLOC instrumentation). Per fixture:
      `[sp,#]` spill loads/stores vs peak *value*-pressure (the allocator's
      distinct-simultaneously-live-values count):
        - flight_seam_flat: 56 spill ops / 356 insns, peak value-pressure 7 (≤9)
        - flight_seam:      39 spill ops / 300 insns, peak value-pressure 7–8
        - control_step:      6 spill ops / 113 insns, peak value-pressure 8
      FINDING: the spills are SPURIOUS. synth keeps WASM locals frame-resident BY
      MODEL (local.get→ldr [sp]; local.set→str [sp]), NOT from register pressure —
      every live value fits the R0–R8 pool (peak ≤9). The value-based SSA allocator
      (VCR-RA-001, today shadow-only behind SYNTH_SHADOW_ALLOC) promotes them into
      registers and eliminates the traffic. PRECISION on "the substrate is built
      side-by-side, UNWIRED": accurate for the spill-ELIMINATING value allocator
      (`allocate_function` — shadow-logged only). The default-on range-realloc
      (`reallocate_function`, v0.11.36) is a RENAMER — it never adds/removes
      instructions, so it provably cannot capture Pass-1; and `apply_const_cse` is
      flag-gated (SYNTH_CONST_CSE=1, off by default). So Pass-1 is genuinely
      unrealized in default codegen — #390's headline holds.
      FORK RESOLUTION (the const-CSE-vs-spill question): const/remat opportunities
      are 0–2 on these kernels (synth already lowers consts as immediates), while
      spill-elimination is 56/39/6 — the spill axis is where the bytes are, and it
      is INDEPENDENT of the const-remat axis. Confirms the spill-elimination wiring
      (not const-CSE) as the #390 headline lever. DE-RISK NOTE for the wiring step:
      the frozen fixtures DO exhibit Pass-1 (56 ops on flight_seam_flat), so they
      are a valid in-tree target — the byte-changing wiring still gates on a
      deliberate re-freeze + differential + gale on-silicon (never an idle tick).
      CI-GATED ORACLE (2026-06-23, frozen-safe, #242 idle-tick increment):
      promoted the load-bearing claim from the shell script into a CI test
      (`crates/synth-cli/tests/spill_baseline_pressure_390.rs`,
      `pass1_spills_are_spurious_pressure_fits_r0_r8_390`) so the baseline can no
      longer silently drift. It drives the real `synth` binary with
      SYNTH_SHADOW_ALLOC=1 (zero-byte instrumentation — no selector-config
      divergence, no external disassembler) and locks: every measured function on
      the 3 frozen kernels has peak value-pressure ≤ 9 (the R0–R8 pool ⇒ the
      `[sp,#]` spills are spurious), with loud-failure guards (non-empty output +
      exact per-fixture line/peak counts so a log-format change fails rather than
      passes vacuously) and an aggregate ≥1 spurious-spill demonstration (6
      functions / 2 spurious measured). NOT change-detection (the frozen hashes
      already do that) — it locks the INTERPRETATION + is the before-baseline the
      value-based allocator (VCR-RA-001) wiring must beat. Sibling of
      `scry_const_remat_signal.rs` (the const-remat axis); together they CI-gate
      both #390 levers.
      GAP RE-MEASURED on v0.12.0 (gale #428, 2026-06-23): loom v1.1.16 inline+DCE
      (loom#228) merged the gust_mix wrapper → gap 2.81× → 2.63× LLVM, "synth is
      the SOLE remaining factor." gale re-ranks the levers (cmp→select predication
      #1, then immediate folding, then allocator wiring) — detail + the
      `gust_codegen_bench` kill-criterion recorded under VCR-SEL-004. The
      byte-changing wiring of these levers stays the next DEDICATED gated release,
      not an idle tick.
    status: proposed
    tags: [codegen, perf, regalloc, addressing-mode, size, gale-390, measurement, track-a, silicon]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-RA-001
      - type: traces-to
        target: VCR-MEM-001
      - type: traces-to
        target: VCR-SEL-004
    fields:
      req-type: non-functional
      priority: should
      verification-criteria: >
        Each pass lands behind the frozen-fixture re-freeze (control_step
        0x00210A55, flat+inlined flight_algo 0x07FDF307, divseam) + the
        differential oracle + gale's on-silicon size confirmation — byte-changing
        optimizations on the flight path, never rushed (the #193/#212/#215
        latent-regalloc lesson). Headline kill-criterion: wiring the built
        allocator substrate (pass 1) drops gust_poll spill count to near-zero and
        the size toward LLVM parity, measured on gale's compare-codegen.sh
        before/after; no frozen fixture changes a byte except via a deliberate,
        gale-confirmed re-freeze.

  - id: VCR-PERF-002
    type: sw-req
    title: "Proof-carrying specialization: consume loom wsc.facts premises to elide proven-dead guards (beat-LLVM, #494)"
    description: >
      DESIGN (2026-07-03, docs/design/proof-carrying-specialization.md; GitHub
      #494 part (a), loom#240/loom#231 fact-passing contract, epic #242).
      The below-native lever: gale measured the floor on gust_floor_bench
      (gale PR pulseengine/gale#121, qemu -icount, re-run-identical) — eliding
      gust_mix's dead clamp under a proven ch∈[524,1524] takes it from 0.825 to
      0.225 ticks/call = 0.45x of native LLVM, past the 0.70x target, a lowering
      LLVM structurally cannot reach because it never had the bound. The span to
      capture is 0.825 -> 0.225 (3.7x) on that one function; the enabling
      information exists only in the verified pipeline (closed fused module +
      machine-checked invariants).

      WHAT LOOM FORWARDS (the loom#231 contract; loom is the PROVER): a custom
      section `wsc.facts` (sibling of wsc.transformation.attestation) carrying
      invariants loom's validator already discharges, keyed by (function index,
      value identification): value-range (v ∈ [lo,hi]), shift-bound (<32/<64),
      divisor-nonzero, in-bounds access, memory disjointness, select-totality.
      Fail-safe skew rule (loom#231 Q4): synth IGNORES unknown fact kinds and a
      missing/unparseable section entirely — facts are optional accelerators,
      and the facts-absent compile is byte-identical to today's baseline BY
      CONSTRUCTION.

      HOW SYNTH CONSUMES THEM (synth is a CONDITIONAL optimizer, not a
      re-prover): each fact becomes a premise available at selection time; a
      specialization (dead clamp-branch elision first; later bounds-check /
      trap-guard / mask-materialization elision) fires only with a PER-ELISION
      PROOF OBLIGATION discharged before emission by the ordeal-backed
      translation validator (#553/#595: certificate-checked QF_BV behind the
      BvSolver trait, no C++ toolchain): assert the premise P as a hypothesis
      and check general_lowering ≢ specialized_lowering under P is UNSAT —
      certificate-checked, so the elision carries evidence, not trust in a
      heuristic. Unknown/Sat/conflict-budget-exceeded => DECLINE loudly and emit
      the general lowering (conservative; never a silent wrong-code path).
      Trust split (loom#231 Q3): synth does NOT re-derive loom's fact — it
      proves the conditional correctness of its OWN transformation given the
      fact; fact validity stays loom's obligation (Z3 translation validation
      upstream), attested via the existing wsc attestation channel.

      ORACLE STRATEGY (every elision gated twice): (1) certificate — the
      per-elision ordeal obligation above, logged per function; (2) differential
      — the specialized build must be result-identical to BOTH wasmtime and the
      unspecialized synth build over the proven bound (and ONLY over the bound —
      that side-condition IS the contract, exit-coded exactly like gale's
      gust_floor_bench soundness gate mix_proven ≡ mix_native ≡ gust_mix on
      [524,1524]). Frozen fixtures carry no wsc.facts section, so every frozen
      anchor is bit-identical trivially; the lever is additionally flag-gated
      (SYNTH_FACT_SPEC, default off) until gale confirms on silicon.

      PHASING (each phase its own oracle-gated PR):
      Phase 1 — fact ingestion: parse wsc.facts, thread premises to
      CompileConfig/selector, ZERO codegen change (byte-identical, frozen-safe);
      schema versioned, unknown-kind-tolerant. IMPLEMENTED (2026-07-07): binary
      encoding schema v1 specified in docs/design/wsc-facts-encoding.md
      (resolves loom#231 open questions 1/2: keyed by (function index, value
      id = producing-operator index), kind bytes 1-6 value-range-first,
      length-prefixed records); total fail-safe parser
      crates/synth-core/src/wsc_facts.rs wired into decode_wasm_module and
      threaded to CompileConfig::wsc_facts / current_func_facts (the
      volatile_segments/#543-Phase-1 inert-plumbing pattern) with NO consumer;
      phase-1 verification-criteria locked by
      crates/synth-cli/tests/wsc_facts_ingestion_494.rs (facts-present .text
      byte-identical to facts-stripped; malformed/wrong-version sections
      ignored end-to-end; non-vacuity decode guard) + parser unit tests (all
      six kinds, unknown-kind skip, truncation/version/overrun => ignored).
      Phase 2 — single-elision prototype: value-range => dead conditional-branch
      elision (the gust_mix clamp shape), flag-gated, per-elision validator
      obligation + in-bounds differential red/green oracle. IMPLEMENTED
      (2026-07-08): crates/synth-verify/src/fact_spec.rs — backend-agnostic
      WasmOp-stream rewrite; at every no-else `if` the pass discharges
      UNSAT(P ∧ cond ≠ 0) through the ordeal-backed BvSolver BEFORE emission
      (this implies the general/specialized equivalence obligation for a
      no-else if, whose not-taken path is the identity by wasm blocktype
      validation); Unsat => admit + per-function certificate log line; Sat
      (with model counterexample) / Unknown / untracked shape / impure
      condition slice => DECLINE LOUDLY, general lowering emitted. Driver gate
      maybe_fact_spec in synth-cli (both compile paths; SYNTH_FACT_SPEC
      default OFF; requires the `verify` feature — absent it the flag declines
      loudly). div/rem deliberately untracked (a deleted condition slice must
      be effect-free under ALL inputs, not just P-admissible ones — trap-guard
      elision is the separate divisor-nonzero fact, out of phase-2 scope).
      Oracles: synth-verify fact_spec unit gates (admit/decline matrix,
      declined-region havoc soundness, tee-impurity non-erasability,
      block-arity ordinal repair, out-of-range value_id vacuity); synth-cli
      tests/fact_spec_clamp_494.rs (flag/fact byte-identity matrix,
      certificate evidence trail, wrong-bound Sat loud-decline); in-bounds
      execution differential scripts/repro/fact_spec_clamp_494_differential.py
      (specialized ≡ wasmtime ≡ unspecialized over the proven bound
      [524,1524] ONLY; non-vacuity: exactly 2 ADMITs + .text shrink required)
      — all CI-gated by the fact-spec-oracle job. The gust_mix clamp fixture
      collapses 20 -> 6 ops (both clamp comparisons + branches + bodies gone);
      measured cortex-m4 codegen 84 B/23 insns -> 14 B/6 insns (vs the 6 B
      add+bx measured floor: residual const-materialization + reg-shuffle +
      callee-saved frame — allocator/peephole residue, a Phase-3 datum).
      Phase 2b — divisor-nonzero trap-guard elision (fact kind 3).
      IMPLEMENTED (2026-07-08): the fact_spec walk now TRACKS i32/i64 div/rem
      (upgrading the phase-2 hard stop) — never deleting them (they can trap;
      result carries no erasable slice) but discharging up to TWO INDEPENDENT
      per-site guard obligations: divide-by-zero = UNSAT(P AND divisor == 0)
      (div_u/div_s/rem_u/rem_s, both widths) and INT_MIN/-1 overflow =
      UNSAT(P AND dividend == INT_MIN AND divisor == -1) (div_s ONLY). THE
      TWO-GUARD DISTINCTION (#633/#634 synergy): a divisor-nonzero fact
      discharges the first but NOT the second — divisor != 0 does not exclude
      -1, so the overflow guard is RETAINED (loud decline) unless the premises
      independently prove it (a value-range divisor in [1,N] proves both;
      either fact kind works). Discharged obligations become per-site elision
      marks (FactSpecResult::elide_div_zero/elide_div_ovf, remapped through
      any clamp-elision rewrite) threaded via
      CompileConfig::fact_div_zero_elide/fact_div_ovf_elide to the DIRECT
      selector only — the optimized path's IR passes renumber instructions,
      so marked functions route to select_with_stack (the #507/#509
      honest-degradation pattern; never fires without flag+facts+obligation).
      i32 guards are selector-emitted and simply skipped; i64 guards live
      inside the ArmOp::I64Div*/I64Rem* encoder expansions, which gained
      per-guard elision flags (Thumb-2 + A32), with estimator sizes tracking
      the flags (estimator<->encoder agreement oracle extended with the 5
      elided variants — zero guard 8 B Thumb / 12 B A32, div_s overflow 22 B
      / 24 B). Oracles: fact_spec unit gates (two-guard matrix, i64 width
      discipline via current_func_params_i64, mark remapping); encoder splice
      pins (elision removes EXACTLY the guard bytes, overflow retained under
      zero-only); synth-cli tests/fact_spec_div_494.rs (byte evidence on the
      qu/qs/ru/qs64 fixture: guard UDFs present without facts, absent with
      facts+flag, qs64's INT64_MIN/-1 guard retained under kind 3 = 1 UDF
      left; Sat-decline byte-identity; the debug-only
      SYNTH_FACT_SPEC_FORCE_ADMIT red lever screams);
      scripts/repro/fact_spec_div_494_differential.py (1584-case in-bounds
      sweep specialized ≡ wasmtime ≡ unspecialized over the proven divisor
      bound, retained-guard trap qs64(INT64_MIN,-1) fires in BOTH wasmtime
      and the specialized build, --expect-decline byte-identity leg,
      --force-admit RED leg demonstrating the wasmtime-traps/unsound-build-
      returns-0 divergence) — all CI-gated by the fact-spec-oracle job.
      Phase 3 NOT started — the requirement's kill-criterion is gale-measured;
      status stays at implemented (not verified) until Phase 3 reports.
      Phase 3 — measurement vs the 0.45x floor: gale re-measures gust_mix on
      gust_floor_bench (qemu -icount) and STM32F100 silicon (DWT CYCCNT);
      kill-criterion unchanged from #494: shipped dissolved lane <1.0x then
      <=0.70x vs native LLVM, bit-identical under the proven bound. The measured
      floor (0.45x) gives the target 0.25x of headroom — if the productized
      elision cannot land inside it, the premise-to-selector plumbing (not the
      idea) is at fault and the phase re-plans.
    # implemented (not verified): Phases 1+2+2b of 3 landed with their oracles —
    # the elision exists, certificate-gated and differential-tested. The
    # requirement's kill-criterion (Phase 3, gale-measured 0.70x vs native)
    # has NO evidence yet — never strengthen a traceability claim beyond it.
    status: implemented
    tags: [codegen, perf, proof-carrying, specialization, wsc-facts, loom-integration, ordeal, beat-llvm, synth-494, gale-121]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-PERF-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        Phase 1: a module with a wsc.facts section compiles byte-identical to
        the same module with the section stripped (ingestion is codegen-neutral);
        malformed/unknown-kind sections are ignored with a diagnostic, never an
        error. Phase 2: each fired elision has (a) an ordeal certificate for
        "general ≡ specialized under premise" logged per function and (b) a
        differential PASS (wasmtime + unspecialized-build agreement) over the
        proven bound; Unknown/Sat declines to the general lowering; all frozen
        fixtures bit-identical (no facts => lever cannot fire); SYNTH_FACT_SPEC=0
        is byte-identical to baseline. Phase 3 (kill-criterion, gale-measured):
        gust_mix on gust_floor_bench + STM32F100 DWT reaches <1.0x then <=0.70x
        vs native LLVM with the soundness gate green; below-target after the
        single-elision prototype => re-plan before widening fact kinds.

  # ---------------------------------------------------------------------------
  # gale-proposed (issue #290, 2026-06-10): scry consumption at two trust levels
  # ---------------------------------------------------------------------------

  - id: VCR-RA-010
    type: sw-req
    title: "scry → synth: sound AI annotations as untrusted regalloc oracle + soundness-bearing narrowing pass"
    description: >
      synth consumes scry's sound over-approximation (range / known-bits /
      reachability lattices over fused Core-Model modules emitted by meld) at
      two distinct trust levels, kept architecturally separate so scry's
      soundness is load-bearing in exactly one of them.
      (A) UNTRUSTED ORACLE — regalloc quality: annotations feed
      rematerialization candidate selection, spill-cost pricing (MOV /
      MOVW+MOVT / literal-pool costs from the known constant), coalescing,
      split placement, and liveness pruning via constant-condition dead-edge
      elimination. HINTS only: VCR-RA-003 re-derives liveness/interference
      and validates the assignment, so nothing scry asserts enters the TCB —
      a wrong annotation degrades quality, never correctness.
      (B) SOUNDNESS-BEARING — narrowing rewrite BEFORE regalloc: where scry
      proves an i64's observable range fits 32 bits, synth carries it in one
      GP register and synthesizes the high half on demand, halving pressure
      for that value on 32-bit Cortex. Each narrowing carries its own
      discharged refinement obligation in the Rocq substrate; no narrowing
      fires without it — the assurance surface is one localized refinement
      check, not the interpreter-in-TCB (Verasco-style).
      Relationship to VCR-DEC-001: path (A) is a candidate to close part of
      the VCR-RA-001 revisit-trigger cycle gap WITHOUT porting regalloc3's
      bundle model (the regalloc2 win came from split/remat sophistication,
      which scry sharpens directly). Depends on a scry-side annotation schema
      + soundness statement (SCRY-001, being filed in the scry repo per scry#51,
      2026-06-20; linked here as text until it has an ID). UPDATE (scry#51): scry
      is at v1.11, NOT the stale v0.2 framing — the sound call graph incl.
      call_indirect target sets (FEAT-006), recursion/SCC flag (FEAT-007), and
      the longest-weighted-path stack bound (FEAT-021) ALL shipped, consumable as
      the crates.io crate `scry-sai-core` (`use scry_analyze_core::analyze`).
      First synth consumer is VCR-MEM-001 (gale #383), spike-confirmed on a real
      module (max_stack_bytes = Bytes(32)).

      API-FITNESS CHECK (2026-06-20, spike on real kernels, the v1.12
      `AnalysisResult.invariants` InvariantBundle): the existing API IS
      sufficient for both paths — NO scry change needed for the interval uses.
      `InvariantBundle.points[].locals[]` gives per-`(func, pc, local_index)`
      `AbstractValue::{I32Interval,I64Interval}(Interval{lo,hi})`: a SINGLETON
      interval = known constant (path-A remat candidate); an `I64Interval` that
      fits 32 bits = path-B narrowing candidate. Per-LOCAL granularity is the
      RIGHT granularity — locals are the long-lived pressure (the #390 "sched
      reloaded 10×" is a local). MEASURED known-constant locals: flight_seam_flat
      44/70, control_step 6/24, controller_step 6/20 — exactly the
      const-materialization waste gale measured (#390 pass-5 / #209). Path-B
      (i64-narrowing) found 0 candidates on these i32-dominated kernels (real in
      principle, not exercised here). TWO honest caveats: (1) precision is
      OPPORTUNISTIC — msgq/filter_axis came back all-`top` (values flow from
      memory/params with no constraining context), so scry-remat is a win on
      constant-heavy kernels and SILENT elsewhere — fine for an untrusted oracle
      (no signal ⇒ no hint ⇒ fall back to synth's own analysis, never wrong).
      (2) The real integration cost is SYNTH-side, not a scry gap: scry keys by
      WASM `(func,pc,local)`, synth's regalloc runs on post-selection ARM vregs;
      consuming the signal needs a `(pc,local) → ARM-vreg` mapping
      (`ArmInstruction.source_line` gives the thread — validate with a spike
      before wiring, like the shadow-stack one). Forward-looking observations
      that don't block synth filed to scry as a help-them-improve issue
      (operand-stack abstract values not surfaced; interprocedural range
      propagation via the call graph to sharpen param/memory-derived locals;
      an eventual known-bits domain for alignment/strength-reduction). NOTE the
      CORE regalloc (#390 pass-1 liveness/interference/colouring/spill) does NOT
      need scry — synth's substrate computes it; scry is an opportunistic quality
      oracle on top, never in the TCB.
    status: proposed
    tags: [codegen, register-allocation, scry, abstract-interpretation, do-333, track-a]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-RA-001
      # scry SCRY-001 soundness contract (scry REQ-011, tagged scry-001): the
      # over-approximation facts (resolved-targets, recursive) this consumes are
      # HINTS — VCR-RA-003 re-validates — but the narrowing path (B) rests on it.
      - type: traces-to
        target: scry:REQ-011
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        (A) Annotation-fuzzing: under arbitrary/corrupted scry annotations,
        VCR-RA-003 still accepts and observable behaviour is identical to the
        no-annotation build — only cycle counts move (evidence path A is
        outside the TCB). (B) CI fails on any narrowing rewrite without a
        discharged refinement obligation. (C) At VCR-RA-001 acceptance
        (v0.11.40 gate) the release notes report the measured cycle-gap delta
        attributable to scry-driven remat + narrowing, feeding VCR-DEC-001's
        revisit decision.

  - id: VCR-MEM-001
    type: sw-req
    title: "Bounded + provable native-pointer linear-memory footprint (shadow-stack budget → scry stack-depth AI) — gale #383"
    description: >
      gale #383: under --native-pointer-abi, build_relocatable_elf
      (synth-cli/src/main.rs:2475) sizes the wasm linmem region to
      used_extent = max(data_end, sp_top, global_top, static_top,
      static_top_abs32).min(linear_memory_bytes). The sp_top term is sp_init —
      the shadow-stack top, which wasm-ld sets to the DECLARED page top (65536
      for `(memory 1)`). So the region spans [0, 65536) even when actual data +
      live stack is a few KB, and an 8 KiB-RAM target (STM32F100) cannot place
      it. MEASURED 2026-06-20 (synthetic repro, no gale binary needed —
      reproduced like #354/#382): a `(memory 1)` module with sp_init=65536
      emits a 64 KiB NOBITS .bss (all-zero linmem) or a 64 KiB PROGBITS .data
      (with an init segment below the static region). Root cause is purely
      structural — sp_top dominates used_extent.

      DO NOT fix as a bare CLI cap (integrator declares a number, synth shrinks
      the reservation blindly): shrinking below the live shadow-stack depth
      silently overflows the stack into static data. The integrator declaring a
      RAM budget is the INPUT; the obligation is to keep the footprint claim
      HONEST about what is proven vs asserted. CRITICAL DISCOVERY (2026-06-20):
      synth has ZERO shadow-stack tracking today — the comment at main.rs:2522
      ("the shadow stack is reached only via the SP register value, dynamic,
      never a static reloc") confirms it treats [0, sp_init) as opaque. So the
      shadow stack is a wasm-level construct (the __stack_pointer global's
      decrement idiom), NOT the ARM machine-stack frame_size. Computing its
      depth is a NEW abstract interpretation — which is scry's mandate. Layered
      by risk (advisor-reviewed) so the unblock does NOT depend on the new AI:

        (1) LOAD-BEARING — layout re-base + integrator budget + consistency
            check + honest refuse (THIS issue's fix). New
            `--shadow-stack-size <bytes>` on `compile`: re-base sp_init to a
            budget B instead of the declared page top. Output is "asserted
            (B), not proven"; DEFAULT unset = full-page = byte-identical
            (frozen-safe). SCOPE CORRECTION (2026-06-20, measured on the REAL
            gust-family module msgq_put_359.wasm, not just a synthetic repro):
            sp_init doubles as the selector's classification boundary
            (set_native_pointer_stack → wasm_data_base, instruction_selector.rs:1623;
            classify at 6735/6846: addr >= boundary ⇒ static `__synth_wasm_data + C`
            reloc, < ⇒ SP-relative frame). The selector ALREADY RAN with
            boundary=65536, so a pure post-selection re-base is sound ONLY when
            nothing was classified against it (no static reloc). BUT the real
            msgq module carries 10 `__synth_wasm_data` relocs (zero-init
            k_spinlock-class statics ABOVE the shadow stack: .bss=0x10018=65560 =
            stack [0,65536) + zero statics [65536,65560)). So pure-only REFUSES
            on the real module — it would ship green and NOT unblock gale. The
            actual layer-1 is the #354 per-region retarget extended to the
            NOBITS region: shift the high `__synth_wasm_data + C` (C >= boundary)
            relocs DOWN by (sp_init - B) and size the .bss to B + zero-static
            extent, so the stack reservation shrinks while the zero statics
            stay covered. Re-bases the SP global slot init to B. Sound (stack
            grows down from B; statics at [B, B+ext) above it never overlap).
            HONEST REFUSE for unhandled geometries (static C below the stack /
            B > sp_init / non-Abs32 static relocs). This is link-fragile
            native-pointer surgery (the #354 step-2 work it explicitly
            deferred) on the path gale FLIES ⇒ silicon-gated (held for gale
            confirmation, the #368→#359 lesson — do not rush-ship). The one
            open disambiguation posted to gale: does the gust target use the
            --stack-first layout (statics above the stack, as msgq shows) so
            the down-shift is a uniform addend rewrite.
        (2) OPT-IN, NOT LOAD-BEARING — auto-PROOF of the budget. UPDATE
            (2026-06-20, scry#51): synth does NOT hand-roll the shadow-frame
            idiom extraction — scry ALREADY SHIPPED it. scry v1.11.0 (crates.io
            `scry-sai-core`, `use scry_analyze_core::analyze`) returns, on a
            single pre-meld Core module, `AnalysisResult.stack_usage.max_stack_bytes`
            = longest-weighted-path shadow-stack bound (FEAT-021),
            `call_graph: Vec<CallEdge>` with sound `resolved_targets` for
            call_indirect (FEAT-006) + `soundness` tag, and
            `function_summaries[].recursive` (FEAT-007, Tarjan SCC) — the exact
            honest-fail gate. GROUNDED SPIKE on the real msgq_put_359.wasm:
            stack_usage.max_stack_bytes = Bytes(32), 0 recursive, 0 indirect,
            Sound — i.e. scry PROVES the true shadow-stack worst case is 32 bytes
            where synth reserves 65536 (a 2048x over-reservation). So layer-2 is
            "consume scry as a crate dep, use max_stack_bytes (cross-checked
            against synth's own re-derived longest-path per the VCR-RA-010 trust
            model) as the PROVEN budget; Unbounded/Unknown ⇒ fall back to (1)'s
            integrator-asserted budget or honest-refuse". This SUBSUMES the old
            hand-rolled idiom-extraction plan AND the call_indirect-refuse
            limitation — scry's resolved_targets handle the indirect tail that
            (the old) (2) had to refuse (#383 ↔ #275). Synth-side cost: a
            MODULE.bazel crate pin alongside the Cargo dep (synth builds under
            cargo + Bazel).
        (3) was "scry tail" — now FOLDED INTO (2): the indirect/recursive cases
            are not a separate synth track, they are fields on the same
            scry AnalysisResult. SCRY-001 (scry filing it via PR #53) is the
            soundness statement of resolved_targets (⊇ concrete) + recursive
            (⇒ reachable cycle); synth VCR-MEM-001 / VCR-RA-010 `verifies`-link
            it once it has an ID.
      WIRING HOLDS FOR scry v1.12.0 (scry PR #53, MERGEABLE 2026-06-20): it
      finalizes the API synth consumes — adds `AnalysisResult.reachable_from_exports`
      as a DEDICATED call (instead of synth hand-deriving reachability from
      call_graph, the v1.11 interim shape), confirms the integration is the
      crates.io LIBRARY `scry-sai-core` (not the wasm component), and files
      SCRY-001 with a Rocq `reach_superset` proof. So bind layer-2 against v1.12
      in ONE shot (max_stack_bytes + reachable_from_exports + recursive + the
      SCRY-001 verifies-link) rather than wiring the soon-superseded v1.11 shape
      now — the spike already PROVED the capability (Bytes(32) on real msgq), so
      nothing is lost by holding the binding for the final API.
      Build order: (1) the ELF retarget — silicon-gated on gale's --stack-first
      answer; (2) the scry-proven budget — capability confirmed (spike), BINDING
      held for scry v1.12.0 (PR #53) to finalize the API. The two are independent:
      (1) is the mechanics
      (shrink the .bss), (2) is the proof (how big is safe). Stays opt-in until
      silicon-validated (the #345/#354/#359 lesson — gale/jess confirms the image).

      LAYER-1 INPUTS NOW IN HAND (2026-06-21, gale #383): the two preconditions
      that gated the byte-changing ELF retarget are RESOLVED + verified against
      the artifact (scripts/repro/gust_kernel.wasm, from gale #91, in-tree):
        - LAYOUT = stack-first (the direct down-shift case, NOT the refuse
          geometry). Verified: memory[0] = 17 pages declared; __stack_pointer
          init sp_init = 1048576; the lone .rodata segment (143 B) sits AT 1048576
          (__data_end 1048719 / __heap_base 1048720) — statics at/above sp_init,
          NONE below. So every static addend >= sp_init shifts down by a uniform
          (sp_init - B); no static-below-stack refuse case to handle for gust.
        - FIXTURE: synth@main (no flag) reproduces gale's number exactly —
          text 1370 / data 156 / bss 1048720 (~1 MiB over-reservation, all of it
          the [0, sp_init) stack page); --shadow-stack-size errors honestly
          (PR #388 scaffold). B = 4096 -> reserve B + 144 = ~4.2 KB, inside the
          8 KiB STM32F100 part.
        - SCRY-PROVEN DEPTH (measured 2026-06-22, dev-dep): scry proves
          gust_kernel's worst-case shadow-stack depth is Bytes(16) (sp_global=0,
          no recursion, 6 reachable) — so jess's flashed asserted B=4096 clears
          the proven depth with a 256x margin (16 <= 4096): the live silicon-rung
          budget is SOUND, not an under-reservation. layer-2 would auto-derive
          16 B (ProvenStackDepth) — 256x tighter than the asserted 4096 and
          65536x under the 1 MiB declared-page default. Locked by the dev-dep
          test `layer2_gust_kernel_proven_depth_clears_flashed_budget_383`, so a
          future scry bump raising the proven depth above the flashed budget
          reddens CI before silicon, not after.
      So layer-1 is unblocked and its geometry is the clean uniform-down-shift.
      Remaining = the byte-changing retarget itself (re-base sp_init -> B; shift
      every __synth_wasm_data static addend >= sp_init down by (sp_init - B),
      across both MovwAbs pairs and Abs32 literal-pool words; resize the region
      to B + static-extent; keep the refuse-on-collision guard) + the post-link
      oracle (stack/static no-overlap; every relocated access in-reservation, the
      #359 check), behind the opt-in flag so frozen fixtures stay bit-identical.
      gale offered on-silicon reflash on this exact gust_kernel.wasm as the final
      gate. A FOCUSED gated step, not an idle-tick increment.

      LAYER-2 DOWN-SHIFT LANDED (2026-07-10, gale #678). The SHIPPED layer-1
      (#383) was narrower than the layer-1 the roadmap sketched above: it
      re-based the SP slot + resized the .bss but REFUSED any residual
      `__synth_wasm_data + C` reloc with C != 0 still pointing into the
      reservation ("down-shifting inline statics is the deferred general case").
      That refusal gated EVERY buffer-carrying dissolved node (wit-bindgen
      `list<u8>` — gale's gust:os `log`/`channel`/`io` capabilities) AND every
      plain `static mut` array (a `spawn` task table), because the wit-bindgen
      canonical ABI / any stateful CM node puts data + zero-init scratch in the
      static tail `[sp_init, used_extent)`. So only pure-stateless-scalar nodes
      (gale's drivers, the gust:os `time` interface) fit an MCU today; the whole
      gust:os OS milestone beyond `time` was blocked. #678 completes the
      down-shift the shipped layer-1 deferred: each residual tail static rebases
      in place `C -> C - (sp_init - budget)` (Abs32 REL literal word patched like
      the #354 retarget), landing in the down-shifted `.bss` tail — which is a
      ZERO byte, exactly wasm's zero-init semantics, because a residual reloc is
      NEVER inside a `(data)` segment (the split path either has no segments —
      `split_linmem_bss` — or retargets ALL of them into `.data`). The addend-0
      region-base pointer (`global.get $sp` base) is stable and left as-is; the
      SP VALUE rides the re-based `__synth_globals` slot. Sound-decline sub-cases
      kept LOUD + precise: a load window straddling a `(data)` segment boundary
      (part in `.data`, part in `.bss` tail), an addend below sp_init (would
      collide with the live stack), and the one-PROGBITS fallback geometry.
      Opt-in (only fires with `--shadow-stack-size`) ⇒ frozen fixtures
      bit-identical (10/10). Evidence: `static_downshift_678.rs` (4 tests:
      bss-static + buffer+bss down-shift, straddle decline, no-flag frozen) +
      the execution differential `native_pointer_static_downshift_678.py`
      (a shadow-stack roundtrip + a `.data` buffer + a down-shifted BSS static,
      all agreeing with wasmtime `run(p) == 43 + 2p` incl. negative p). NOT to
      be confused with the roadmap's numbered layer-2 (scry-PROVEN auto-budget,
      `--shadow-stack-size auto`) below, which is orthogonal (this fixes the ELF
      mechanics of the down-shift; that computes how big B may safely be).

      MULTI-SP CO-REBASE LANDED (2026-07-11, gale #707). After #701 (#678 tail
      down-shift) cleared the buffer-carrying blocker, a multi-provider
      meld-fused gust:os node (`app-tl` = app + time-provider + log-provider)
      compiled all functions but `--shadow-stack-size` then REFUSED: the fused
      shared-memory module carries N mutable `__stack_pointer` globals (one per
      fused component), ALL with `init == sp_init`, and the re-base picked the
      UNIQUE such global — bailing on ambiguity ("could not uniquely identify the
      shadow-stack global ... N globals have init == sp_init"). #707 re-bases the
      whole `init == sp_init` equivalence class: in a `meld fuse --memory shared`
      module the per-component SP globals all point into the ONE shared
      reservation, so sliding all of them to the shrunk budget is correct (they
      alias the same stack). A single-SP module has exactly one match ⇒
      byte-identical (the #383 tests still pin that path); only the len==0 case
      remains an honest refuse. Evidence: `multi_sp_rebase_707.rs` (compile
      red→green + all-slots-rebased + no-flag frozen) + the execution differential
      `multi_sp_707_differential.py` (each of 3 exports roundtrips through its own
      co-rebased SP global and restores its own slot to B; faithful — fails when
      the expected init is wrong). This unblocks the gust:os v0.4.0 buffer-interface
      OS node (log carries `list<u8>`), the last synth gate before that cut.

      LAYER-2 DECISION LOGIC LANDED (2026-06-22, frozen-safe, no dep change):
      `synth-cli/src/shadow_budget.rs` — a pure `budget_from_bound(bound,
      sp_init, fallback) -> BudgetDecision` over a synth-OWNED `StackDepthBound`
      enum (Bytes(u64)|Unbounded|Unknown), so the decision compiles and unit-
      tests (9 cases) WITHOUT scry in the build graph. Primary-source-confirmed
      scope (scry-sai-core-1.12 lib.rs:276-281: max_stack_bytes is "the deepest
      weighted path … each function weighted by the frame its prologue subtracts
      from the __stack_pointer global … guest shadow-stack only") ⇒ Bytes(n)
      yields source=ProvenStackDepth labelled "proven stack DEPTH, asserted
      no-heap" (NOT a bare "proven footprint" — the #383 overclaim shape is
      explicitly guarded against). Refuses when proven depth > sp_init (names it
      as the ORIGINAL image under-provisioning its stack, a latent source bug
      surfaced for free). Unbounded/Unknown ⇒ AssertedFallback or honest-refuse;
      Unknown NEVER yields ProvenStackDepth even with a fallback (unit-tested).
      B is rounded up to 16-byte AAPCS/LLVM stack alignment (rounding up keeps
      B >= proven depth ⇒ soundness preserved). `#[allow(dead_code)]` until the
      gated call site lands.

      TWO GATED STEPS REMAIN, the first a USER DECISION:
        (2a) DEP ARCHITECTURE — promoting scry-sai-core from dev-dep to a
             PRODUCTION dep of synth-cli pulls its full transitive closure into
             the Bazel `rust_binary` compile (synth-cli IS in the Bazel graph:
             crates/BUILD.bazel:230). MODULE.bazel uses `crate.from_specs()`
             (21 manual `crate.spec`s, NOT `from_cargo`) — likely because z3
             needs `features=["static-link-z3"]`. So the cascade is real and the
             fix is one of {from_cargo migration, feature-gate the scry call out
             of the Bazel build, ~28 manual specs}. NOT an idle-tick or a unilateral
             call — taken to the user.
        (2b) ADAPTER + WIRING — `scry_analyze_core::StackBound -> StackDepthBound`
             adapter at a gated call site that runs `analyze()` on the pre-link
             Core module, feeds `budget_from_bound`, and routes the result into
             the layer-1 shrink. Opt-in (e.g. `--shadow-stack-size auto`); default
             unchanged ⇒ frozen fixtures bit-identical. verifies-link scry SCRY-001.
    status: proposed
    tags: [codegen, native-pointer-abi, memory-layout, abstract-interpretation, scry, stack-depth, gale-383, track-a]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-RA-010
      # scry SCRY-001 soundness contract (filed 2026-06-20 as scry REQ-011,
      # tagged scry-001): resolved-targets ⊇ concrete + recursive ⇒ reachable
      # cycle; reach_superset mechanized. The footprint proof rests on it.
      - type: traces-to
        target: scry:REQ-011
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        LAYER (1), this release: with `--shadow-stack-size B`, a `(memory 1)`
        native-pointer module (sp_init=65536, small static-data extent) reserves
        static_data_high_water + B and re-bases sp_init to that top — a region
        of a few KB instead of 64 KiB, placeable in an 8 KiB-RAM linker script.
        Synth REFUSES honestly (typed Err, never silent shrink) when the
        static-data high-water would collide with the re-based stack top. The
        emitted footprint is labelled "asserted (B), not proven". WITHOUT the
        flag the reservation and every byte are UNCHANGED ⇒ all frozen fixtures
        (control_step 0x00210A55, flat+inlined flight_algo 0x07FDF307, divseam)
        byte-identical. A post-link oracle asserts (a) stack region and data
        region do not overlap AND (b) the reservation still covers every
        relocated __synth_wasm_data access (the #359 msgq regression check).
        LAYER (2), next: acyclic + direct-only + canonical-frame modules derive
        B automatically (output "proven"); call_indirect / recursion / non-canonical
        frame ⇒ refuse → fall back to (1). LAYER (3): scry#51 proves the tail.
        LAYER (2) DECISION-LOGIC criterion (LANDED 2026-06-22, frozen-safe):
        `budget_from_bound` unit suite (synth-cli src/shadow_budget.rs) asserts —
        Bytes(n) ⇒ source=ProvenStackDepth with B=align16(n); Bytes(n>sp_init) ⇒
        Refuse naming the original-image under-provision; Unbounded/Unknown+fallback
        ⇒ source=AssertedFallback (NEVER ProvenStackDepth, even for Unknown);
        Unbounded/Unknown+no-fallback ⇒ honest Refuse with the cause. Compiles +
        passes with scry ABSENT from the build graph (dep-free synth-owned bound
        enum). The scry production-dep wiring (2a/2b above) is the separate gated
        step; default-off ⇒ frozen fixtures unaffected.
        LAYER (2) END-TO-END criterion (LANDED 2026-06-22, frozen-safe): the
        join the #392 spike (scry raw output only) and the decision-logic suite
        (synthetic bounds only) each cover half of — `layer2_budget_pipeline_msgq
        _end_to_end_383` (synth-cli main.rs cfg(test)) runs scry's `analyze()` on
        the REAL msgq_put_359.wasm gust fixture, maps StackBound→StackDepthBound
        (the 1:1 adapter that becomes `impl From` in 2b), feeds budget_from_bound,
        and asserts the 2048x over-reservation (65536) collapses to a PROVEN 32 B
        budget (source=ProvenStackDepth, preferred over the asserted 4096
        fallback). scry stays a DEV-dep exercised only under cfg(test) ⇒ the
        production binary pulls no scry and emits identical bytes. This test is
        the oracle the gated 2b wiring must match.
        LAYER (2) PROVEN-DEPTH + HONEST-FAIL coverage (LANDED 2026-06-22,
        frozen-safe): the proven path is now anchored on BOTH real shadow-stack
        fixtures — msgq (Bytes(32)) and gust_kernel (Bytes(16), the fixture jess
        flashes; proven ≤ flashed 4096, silicon budget sound, #424). The
        soundness-critical REFUSAL path is anchored against real scry output via
        `recursive_shadow_stack.wat` (recurses through the SP global ⇒ scry
        returns recursive=true + Unbounded): `layer2_unbounded_recursion_refuses
        _proven_budget_242` asserts an unbounded depth NEVER yields a
        ProvenStackDepth — only the asserted fallback (if given) or an honest
        refuse. This guards the upstream assumption the entire honest-fail gate
        rests on (scry flags recursion-through-the-shadow-stack as non-finite), so
        a scry regression that returned a finite bound for an unbounded stack —
        the one failure that would silently under-reserve on silicon — reddens CI.

  - id: VCR-MEM-002
    type: sw-req
    title: "Multi-memory structural isolation: lower N wasm memories to N distinct native bases (synth #406, meld #300, gale #86/#404)"
    description: >
      Cross-repo decision (meld #300, 2026-06-21): the committed dissolved-
      library-OS inter-component isolation model is STRUCTURAL — meld preserves
      each component's memory as a distinct region (`MemoryStrategy::MultiMemory`,
      tested in meld-core/tests/multi_memory.rs: separate-memories, preserves-
      isolation, cross-memory copy) so the MPU/PMP region boundary IS the
      semantic boundary: a component cannot even FORM a pointer into a neighbour
      (distinct native base), vs single-shared + embedder MPU-carve (model 1,
      retained SECONDARY) where a miscomputed address lands in a neighbour's
      sub-range and only the MPU catches it. meld emits the multi-memory
      structure + cross-memory ops today ⇒ SYNTH IS THE REMAINING GATE.
      SHIPPED UPSTREAM (meld v0.34.0, 2026-06-23): the #300 decision is now
      formalized as meld ADR-4 (safety/adr/ADR-4-inter-component-isolation-model)
      and released — model 2 is the committed structural-isolation path, meld
      guarantees `MultiMemory` output STABLE as synth's lowering target (adjusts
      only if synth hits an unconsumable shape), and ADR-4 names this synth-side
      lowering (synth#404/#369) as the committed remaining work, anchored on
      meld's gating tests (`test_multi_memory_result_copy_adapter`, SR-21/SR-23).
      No synth build impact (no cargo dep on meld); the synth obligation is the
      staged byte-changing track below, unchanged in scope.

      Today synth is single-memory: the memory index is DROPPED at the IR level
      (the load/store `WasmOp` variants carry no `memory_index` — wasm_op.rs),
      cross-memory `memory.copy`/`memory.fill` (non-zero dst_mem/src_mem) are
      loud-skipped in wasm_decoder.rs, and the linmem base is one hardcoded
      register (R11 = 0x20000000 / 0x20000100). MPU is config-only
      (mpu_allocator computes region base/size/perms + init code, nothing wired
      to codegen — see VCR-MEM-001 / #377). Latent infra: `synth_memory::
      MemoryTable` (MAX_MEMORIES=8), unwired.

      WORK (staged, gated — byte-changing on the load/store path):
        (1) Carry `memidx` through the IR — add `memory_index` to the
            load/store/memory.* WasmOp variants; stop dropping it in the decoder.
        (2) Per-memory native bases — place memory[k] at a distinct base; the
            common case pins the function's home-memory base in R11 (≈ today's
            cost), cross-memory access resolves via the per-memory base/size
            table (synth_memory::MemoryTable). Steady-state cost ≈ 0; only
            cross-memory access pays.
        (3) Cross-memory ops — emit memory.copy/fill with distinct dst/src mem
            explicitly instead of loud-skipping (#369-adjacent).
        (4) Expose per-memory base/size so an embedder programs one MPU/PMP
            region per memory (wire mpu_allocator from the per-memory layout —
            ties to #377 MPU runtime wiring).
      MPU/PMP region cap (~8 ARMv7-M, PMP similar) bounds practical N — fine for
      a handful of mutually-distrusting components, NOT arbitrary scale; applies
      to model 1 equally (not a differentiator). meld keeps MultiMemory output
      stable as the lowering target; file against meld on an unconsumable shape.
    status: proposed
    tags: [codegen, memory, isolation, mpu, multi-memory, meld-coordination, byte-changing, track-c, synth-406]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-MEM-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        Each of the 4 steps lands gated: WITHOUT multi-memory input every byte
        is UNCHANGED ⇒ all frozen fixtures (control_step 0x00210A55, flat+inlined
        flight_algo 0x07FDF307, divseam) byte-identical (single-memory modules
        take the same path as today). A multi-memory module lowers to N regions
        with per-memory bases; a differential oracle confirms cross-memory
        copy/load/store are result-correct vs wasmtime, and a post-link check
        asserts the N regions are disjoint and each carries the base/size an
        embedder maps to one MPU/PMP region. Byte-changing steps gate on the
        frozen-fixture re-freeze + differential + gale on-silicon (the
        #193/#212/#215 latent-regalloc lesson) — never an idle-tick increment.

  - id: VCR-MEM-003
    type: sw-req
    title: "Stack-guard ladder for self-contained images: low stack layout → MPU guard → v8-M PSPLIM (synth #687)"
    description: >
      Today's self-contained Cortex-M image puts the initial SP at the TOP of
      SRAM growing DOWN toward the R9 globals table and linear memory — a
      stack overflow silently corrupts them (measured under unicorn: deep
      recursion sweeps the linmem canaries and only faults once SP exits SRAM
      entirely). Graded fix ladder (maintainer design 2026-07-10, #687):

        (1) IMPLEMENTED — `--stack-layout=low` (+ `--stack-size`, default
            4096): SP init = SRAM start + stack_size; linear memory, the R9
            globals table AND the optimized path's absolute linmem base
            (CompileConfig::linmem_base, default 0x2000_0100) shift UP by
            stack_size — the entire RAM-anchored layout moves as one. An
            overflow descends past 0x2000_0000 into reserved/flash-alias
            space and BusFaults on the FIRST errant push — every Cortex-M,
            no MPU. Applies ONLY to self-contained images; --relocatable /
            imported-function ET_REL / non-Cortex-M backends REFUSE the flag
            loudly (the linker script owns their layout). Default
            --stack-layout=high is byte-identical by construction (reserve=0
            degenerates every formula; the startup's MOVW/MOVT R11 encodes
            the historical fixed bytes; whole-ELF cmp vs main on three
            fixtures + frozen gate 10/10). Layout contract documented on
            build_multi_func_cortex_m_elf, cross-referenced from the
            #650/#669 R11 table contract (CallIndirectGuards).
        (2) OPEN — MPU guard region below a stack-HIGH stack (reuse the
            --safety-bounds mpu machinery, #404/#406 region model); costs one
            v7-M region, catches overflow without moving the layout.
        (3) OPEN — PSPLIM/MSPLIM hardware stack limit on ARMv8-M targets
            (M33/M55); wire when a v8-M target matters.

      Status "implemented" covers rung (1) ONLY — rungs (2)/(3) are future
      issues on this artifact.
    status: implemented
    tags: [codegen, memory, stack, layout, busfault, self-contained, track-c, synth-687]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-MEM-001
      - type: traces-to
        target: VCR-MEM-002
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        scripts/repro/stack_layout_687_differential.py (unicorn + wasmtime,
        artifact-derived: the image's OWN vector-table SP + reset path): RED —
        stack-HIGH deep recursion silently corrupts linmem canary words
        (4/8 clobbered) BEFORE any fault (fault only at the SRAM floor,
        SP 0x1FFFFFF0); GREEN — stack-LOW faults UC_ERR_WRITE_UNMAPPED at the
        SRAM start (SP 0x20000010) with ALL 8 canaries intact — the BusFault
        precedes any linmem damage. TRANSPARENT — in-budget calls match
        wasmtime under BOTH layouts, and the existing #649 i64-global-init
        differential passes unchanged under EXTRA_SYNTH_FLAGS="--stack-layout
        low" (R9 shifts 0x20010000→0x20011000). SHIFT PIN — low-layout canary
        addresses sit exactly stack_size above their high-layout twins.
        Flag-off: frozen byte gate 10/10 + whole-ELF cmp vs main byte-identical
        on stack_canary_687 / i64_global_init_649 / control_step self-contained
        images.

  - id: VCR-MEM-004
    type: sw-req
    title: "ProvenSafeBoundsChecker: fail-closed elision of software bounds guards from scry's proven-safe verdicts (synth #901, scry #114)"
    description: >
      WasmBounds (Sudo & Winstein, Stanford CS191 Spring 2026) shows the payoff
      end to end: abstract interpretation identifies provably in-bounds wasm
      memory accesses, their bounds checks are elided, and they measure 1.21x.
      Their motivation IS synth's target — hardware guard pages need virtual
      memory, so on no-MMU embedded (and under Memory64 / Custom Page Sizes)
      every access falls back to a SOFTWARE bounds check. synth's own
      `synth_memory::SoftwareBoundsChecker` documents that cost as
      "~25-40% overhead", and `--safety-bounds software` emits the #752
      wraparound-safe SUB/CMP/BHS/UDF/CMP/BLS/UDF guard (16 B) at every i32
      access site.

      Difference from WasmBounds: we own BOTH halves. scry proves the access
      in-bounds (sound AI, admit-free Rocq) and synth proves the codegen
      correct (Rocq), so the elision is PROOF-CARRYING and ATTESTED rather than
      a trusted optimizer flag. This artifact is the CONSUMER side; the producer
      is scry #114 (`safe-accesses.json`, schema `scry/safe-accesses/v1`,
      FEAT-046 OOB verdicts). Relation to VCR-PERF-002 (#494): #494 already
      strips this exact guard, but its authority is a PER-SITE ordeal obligation
      discharged inside synth from loom's `wsc.facts` premises. VCR-MEM-004
      reuses the SAME per-site strip mechanism
      (`InstructionSelector::apply_mem_bounds_elision`) under a DIFFERENT
      authority: a whole-module external abstract interpretation, hash-bound to
      one exact module. The two are independent evidence channels for one
      mechanism, and the sidecar records WHICH one authorized each site.

      SAFETY PROPERTIES — these are the deliverable, not the speedup:
        (1) FAIL CLOSED on `module_sha256` mismatch. The hash is verified
            against the EXACT bytes handed to the decoder (post-WAT-parse,
            post-loom, post-#418 arena-bind), so any pre-compile module rewrite
            that shifts function/op indices ALSO breaks the hash and refuses —
            index skew and byte skew collapse into one gate. Eliding on a stale
            analysis is a memory-safety hole, not a stale optimization.
        (2) ABSENCE MEANS "NOT PROVEN", NEVER "UNSAFE". A site not listed in
            `proven_safe` delegates to `SoftwareBoundsChecker` unchanged. The
            verdict list is non-exhaustive by contract (WasmBounds' own output
            contract), so a partial list must yield a partially-guarded binary.
        (3) FAIL CLOSED on `memory_min_bytes` disagreement. Verdicts are proven
            against scry's declared floor; if it differs from synth's declared
            minimum for this module, every verdict is unsound HERE — refuse and
            name both values. (A matching hash implies they agree, so a
            mismatch means the producer is broken, and trusting a broken prover
            is the hole this artifact closes.)
        (4) SELF-CHECKING KEY. `(func, pc)` is the wasmparser operator index
            space — `pc` is the 0-based op index within the function body (the
            space scry's own guard refinement walks as `ops[pc..pc+4]`, and the
            space synth's `op_offsets` side-table and #494's elision marks are
            indexed by). Ingestion VALIDATES each entry against the decoded
            stream: `func` must exist, `pc` must be in range, and the op at
            `pc` must be a memory access whose access width matches the
            declared `width`. A mismatch DROPS that entry with a counted
            diagnostic — so if the producer ever emits byte offsets instead of
            op indices, essentially every entry fails validation and the build
            elides NOTHING loudly, instead of stripping the guard off the wrong
            access silently.
        (5) MALFORMED / MISSING / UNPARSEABLE ⇒ no elisions WITH a diagnostic,
            never an error and never partial trust — the `wsc.facts` fail-safe
            skew rule (`synth_core::wsc_facts`, loom#231 Q4) applied to a JSON
            carrier.
        (6) FACT-SPEC COMBINATION REFUSED. `SYNTH_FACT_SPEC` may REWRITE the op
            stream before selection (`SpecializedFn::kept`), which renumbers the
            index space `pc` is stated in. When a function was specialized, its
            scry marks are DROPPED with a loud per-function diagnostic rather
            than remapped — a remap is a future increment that must be gated on
            its own differential, not assumed.
        (7) ZERO-ELISION IS LOUD. `--proven-safe` accepted but nothing stripped
            is the failure mode that looks like success. Every reason is named:
            file refused, no site validated, `--safety-bounds` not `software`,
            or the function took the optimized path (`optimizer_bridge`'s
            `push_software_bounds_guard` sites are NOT mark-driven — the same
            boundary #494 has).

      ATTESTATION (loop step 6, sigil): every `--proven-safe` compile writes
      `<out>.proven-safe-elisions.json` (schema
      `synth-proven-safe-elisions-v1`) carrying the accepted/refused verdict
      and its reason, `scry_version`, `module_sha256`, `memory_min_bytes`, the
      `--safety-bounds` mode, and the per-site elision set (func, pc, op,
      width) — emitted ON REFUSAL TOO, so sigil can distinguish "nothing to
      elide" from "file rejected" instead of reading a brag sheet.

      CRATE GRAPH (the `shadow_budget.rs` shape, deliberately): ingestion, hash
      verification and attestation live in `synth-core` (which already carries
      `sha2`/`serde_json`); the named `ProvenSafeBoundsChecker` lives in
      `synth-memory/src/bounds.rs` beside the `BoundsChecker` trait and is
      DEP-FREE (its whole dep list is `bitflags` and it supports no_std). synth-
      memory is `publish = false` and nothing depends on it, so a CLI path dep
      is impossible without changing the published surface; the two halves are
      joined by this documented contract, not a compile-time link. Named
      residual, not hidden.
    status: implemented
    tags: [codegen, memory, bounds-elision, scry, proof-carrying, attestation, sigil, track-c, synth-901, scry-114]
    links:
      - type: derives-from
        target: VCR-001
      - type: traces-to
        target: VCR-MEM-001
      - type: traces-to
        target: VCR-PERF-002
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        RED-FIRST, one per safety property, all three failing before the change
        (crates/synth-cli/tests/proven_safe_bounds_901.rs, plus dep-free trait
        unit tests in synth-memory): (1) a `safe-accesses.json` whose
        `module_sha256` is one nibble off elides NOTHING and warns — and the
        MUTATION that inverts the hash comparison turns the differential's
        out-of-bounds leg RED (a silent OOB access), which is the evidence the
        gate is load-bearing rather than decorative; (2) a list covering 5 of
        the fixture's 8 access sites leaves EXACTLY 3 guards standing (byte
        delta = 5 x 16 B) and an unlisted site still TRAPS under execution;
        (3) a full list strips all 8 and the compile stays result-identical to
        wasmtime across an in-bounds sweep. Malformed/missing/wrong-schema/
        wrong-`memory_min_bytes` files each elide nothing with a NAMED
        diagnostic and exit 0. Execution differential
        (scripts/repro/proven_safe_bounds_901_differential.py, unicorn +
        wasmtime, CI-wired in the same commit): elided ≡ checked ≡ wasmtime on
        every in-bounds case (return value AND full final memory image), and
        the not-proven OOB case still traps. Flag-off is byte-identical by
        construction (the mark vector defaults empty) and locked by the frozen
        anchors 10/10.

  # ---------------------------------------------------------------------------
  # Toolchain completeness — debuggability (not a VCR correctness item, but
  # Tier-2 depends on the VCR-RA value→location mapping)
  # ---------------------------------------------------------------------------

  - id: VCR-DBG-001
    type: sw-req
    title: "Emit DWARF in the ARM/RISC-V ELF — synth drops debug info (synth #394)"
    description: >
      synth #394: synth lowers WASM → bare-metal ELF but emits ZERO DWARF
      (confirmed: no `.debug_*` in any output), so a synth-compiled image is not
      source-debuggable (no source line at a PC, no variable locations, no named
      backtraces). The input carries it and the upstream preserves it: real
      Rust/clang→wasm modules ship DWARF in custom sections (e.g.
      msgq_put_359.wasm: `.debug_*` across 8 custom sections), and MELD already
      REMAPS that wasm DWARF through fusion (meld-core/src/dwarf.rs +
      dwarf_remap_witness/dwarf_passthrough tests). synth is the ONLY stage that
      drops it — like meld adjusts wasm-DWARF through its transform, synth must
      EMIT ARM/RISC-V-ELF DWARF through its WASM→machine lowering.
      TRACTABLE — synth already has the spine: every ArmInstruction carries
      `source_line` (the wasm op index, ~220 threading sites) = the
      (machine-addr → wasm-offset) half; compose with the wasm DWARF
      (wasm-offset → source) for (machine-addr → source).
      TWO TIERS:
        - Tier 1 `.debug_line` (near-term, raw material ready): machine-addr →
          source line ⇒ breakpoints/single-step land on source, file:line
          backtraces. Independent of regalloc.
        - Tier 2 `.debug_info` variable locations (DWARF location lists):
          source var → ARM reg/stack-slot range. Needs the value→physical-location
          mapping the register allocator produces — the SAME (pc, local) →
          ARM-vreg mapping surfaced in VCR-RA-010 — so it is GATED on the VCR-RA
          allocator wiring.
      DWARF is additive non-loadable sections ⇒ `.text` and the frozen fixtures
      stay bit-identical. Coordinate the line/var encodings with meld so
      source → meld → synth → on-target debugger composes end-to-end.

      FEATURE-LOOP PLAN — Tier 1, release v0.12.0 (the FIRST North-Star FEATURE
      release; user-selected 2026-06-20). Chosen first because additive
      non-loadable sections ⇒ ZERO flight-path risk (no re-freeze, no silicon
      gate) while delivering real integrator value + exercising the
      source-to-object provenance spine. DE-RISKED (spike 2026-06-20): the core
      crux is that synth's `source_line` is the wasm OP INDEX
      (instruction_selector.rs:5428 `wasm_ops.iter().enumerate()`), NOT the wasm
      code BYTE-OFFSET that DWARF .debug_line keys on; and the decoder
      (wasm_decoder.rs decode_function_body:445) DISCARDS the byte offsets
      wasmparser exposes. So the bridge is wasm-op-index → wasm-byte-offset.
      Steps, each oracle-gated:
        (1) DECODER byte-offset side-table: capture per-op wasm code byte offset
            in decode_function_body (wasmparser OperatorsReaderWithOffsets) →
            additive `op_offsets: Vec<u32>` on FunctionOps. Codegen IGNORES it ⇒
            .text byte-identical ⇒ frozen fixtures bit-identical (the first,
            safe, enabling step).
        (2) READ the input wasm DWARF: extract `.debug_*` custom sections
            (wasmparser, already a dep) + parse `.debug_line` (gimli, NEW
            production dep ⇒ deliberate MODULE.bazel pin + repin — in-scope for a
            feature loop) → (wasm-byte-offset → file:line) rows.
        (3) COMPOSE: ARM-text-offset → wasm-op-index (source_line) → wasm-byte-offset
            (step 1) → file:line (step 2). Build the address→line table.
        (4) EMIT the ARM/RV32 `.debug_line` (+ minimal `.debug_info`/`.debug_abbrev`/
            `.debug_str`) as non-ALLOC ELF sections; ensure they survive the
            relocatable host-link path.
        (5) ORACLE: parse the output ELF's `.debug_line`, assert a known
            ARM address resolves to the correct source line; AND assert `.text`
            byte-identical to the no-DWARF build (the load-bearing safety
            property). Then cut v0.12.0.
      PROGRESS:
        - step (1) MERGED #399 (decoder `op_offsets` byte-offset side-table).
        - step (2) READ side proven in-tree 2026-06-21 (frozen-safe spike,
          crates/synth-core/tests/dwarf_line_read_spike.rs): gimli DEV-dep
          extracts the `.debug_*` custom sections (wasmparser) and parses
          `.debug_line` into (wasm-byte-offset → file:line) rows on the
          DWARF-carrying fixture k_mutex_unlock.dissolved.wasm — e.g.
          wasm+0x0094 → panicking.rs:80. DEV-dep ⇒ no production gimli dep, no
          MODULE.bazel pin (Bazel globs src/ only), zero codegen change, frozen
          fixtures bit-identical. The PRODUCTION gimli dep + MODULE.bazel pin
          land with the EMITTER (step 4), as a feature-loop release step — not
          an idle-tick increment.
        - step (3) compose — DE-RISK FINDING 2026-06-21 (offset-space probe,
          since removed): the two address spaces DO NOT trivially align, and
          step 3 must reconcile them BEFORE any join is correct (a guessed join
          yields silently-wrong source lines — worse than none for a debugger).
          Measured on k_mutex_unlock.dissolved.wasm: synth's `op_offsets` are
          MODULE-relative (fn0 0x137..0x13a, fn1 0x140..0x1bd, fn2 0x1c0..0x1c5,
          fn3 0x1cb..0x288; code section at module 0x86), but the `.debug_line`
          row addresses are 0x03 / 0x94 / 0x98 — far below ANY op_offset and not
          reconcilable by the constant code-section base. Two compounding causes:
          (a) DWARF-for-wasm addresses use a CODE-section-relative convention,
          not module-relative — op_offsets need normalizing into it (subtract the
          code-section content base, per-function body-offset aware); and
          (b) this FIXTURE is meld-DISSOLVED and its `.debug_*` describe Rust
          std/core glue (panicking.rs/int_macros.rs/macros.rs/traits.rs) against
          what looks like the PRE-fusion layout — i.e. incoherent with the bytes
          synth compiles. CONCLUSION: step 3 needs (i) the exact DWARF-for-wasm
          address convention pinned + an op_offsets→DWARF-address normalizer, and
          (ii) a COHERENCE-CHECKED fixture — ideally a direct rustc→wasm
          (non-dissolved) module whose `.debug_line` describes its own code — or
          a meld-remapped dissolved module verified coherent. Until then the join
          is unbounded for an idle tick. Acquire/build a coherent-DWARF fixture
          as the first sub-step of the dedicated step-3 work.
        - step (3) FIXTURE-ACQUISITION FINDING 2026-06-22: the obvious paths to a
          small committable coherent-DWARF fixture are BOTH dead ends with the
          local toolchains. (a) `rustc --target wasm32-unknown-unknown -C
          debuginfo={1,2}` on a 2-function no_std cdylib produces COHERENT DWARF
          (.debug_str carries axpy/clampi + the source path — the line table
          describes its OWN code, unlike the dissolved fixtures), and synth
          decodes it cleanly (6 funcs, op_offsets present, NO loud-skip — so the
          synth-DECODE side of step 3 is validated on coherent input). BUT it is
          ~550 KB: rustc emits line tables + .debug_str/.debug_info for the WHOLE
          cdylib's std/core machinery (.debug_line alone 129 KB), not just the 2
          functions — uncommittable next to the repo's <6 KB fixtures, and
          stripping non-line sections doesn't shrink the 129 KB line table.
          (b) Apple `/usr/bin/clang` has NO wasm32 target ("No available targets
          compatible with triple wasm32"). CONCLUSION: a clean step-3 fixture
          needs one of — a wasi-sdk clang+wasm-ld (not installed), a hand-crafted
          minimal `.debug_line` over a tiny hand-written wasm, or a wasm-tools
          pass that extracts just the 2 functions' line-program subset. The
          address-normalizer can be validated against the big /tmp rustc fixture
          in a scratch test before committing anything. Fixture acquisition (not
          the compose logic) is the gating sub-step.
        - step (3) FIXTURE ACQUIRED 2026-06-22 (RESOLVED the blocker): the
          shrink IS achievable — `-C panic=abort -C overflow-checks=off
          -C opt-level=1` with wrapping ops drops the panic/overflow/std-fmt
          machinery that bloated the linked DWARF, yielding a 1.4 KB module with
          a 249-byte `.debug_line` describing only axpy/clampi.
          scripts/repro/dwarf_coherent.{wasm,rs,README} committed + locked by
          crates/synth-core/tests/dwarf_coherent_fixture.rs, which asserts: synth
          decodes it with parallel op_offsets (step 1), the `.debug_line` is
          coherent (names dwarf_coherent.rs, not std glue), and the DWARF
          addresses are CODE-section-relative (≤ code_size, confirmed 0x03..0x21
          for a 33-byte code section) — i.e. the op_offset→DWARF normalization is
          a single code-base subtraction. So step 3 (compose) is now UNBLOCKED:
          the remaining work is the join itself (ARM-text-offset → op-index via
          source_line → op_offset → minus code-base → DWARF row → file:line),
          frozen-safe as an analysis until step 4 emits.
        - step (3) COMPOSE LANDED 2026-06-22: the wasm half of the join —
          op-index → source line — is `synth_core::dwarf_line::op_offsets_to_source`
          (pure, plain-data, no gimli/backend; unwired ⇒ frozen-safe). It
          normalizes each op's MODULE-relative `op_offsets` byte into the
          CODE-relative DWARF space (`op_offset - code_base`, code_base = the code
          section payload start) and takes the covering line-table row.
          EMPIRICALLY confirmed on dwarf_coherent.wasm: code_base = 0x70 (112),
          and op_offset - 112 reproduces the DWARF addresses exactly (axpy op0
          115→0x3, clampi op0 126→0xe). Unit tests (covering-row lookup, before
          first-row, before code-base) + dwarf_compose_step3.rs join the real
          fixture's op_offsets × parsed .debug_line and assert ops resolve to the
          fixture's own source lines (axpy/clampi + inlined-intrinsic lines), with
          the entry-op→entry-row normalization check. REMAINING for step 3→4: the
          ARM-text-offset → op-index half is just `ArmInstruction.source_line`
          (trivial once the backend stream is available); step 4 emits the
          composed table as non-ALLOC `.debug_line` (the byte-touching-but-DWARF-
          additive step, .text still bit-identical).
        - step (4) EMIT-LOGIC DE-RISKED 2026-06-22 (frozen-safe spike): the
          read→compose→EMIT→read loop closes faithfully. dwarf_emit_roundtrip_step4.rs
          composes synth's op-index→line table on dwarf_coherent.wasm, emits it as
          a full minimal DWARF via gimli::write (DEV-dep, default `write` feature
          on), reads it back via gimli::read, and asserts every address resolves
          to the same source line — i.e. synth's composed mapping survives emission
          as debugger-readable DWARF. Test-only ⇒ zero production change, no output
          ELF, frozen fixtures untouched. So the emit FORMAT is proven; the GATED
          remainder of step 4 is: gimli as a PRODUCTION dep (+ MODULE.bazel pin),
          wiring the section into the ELF builder with real ARM text offsets
          (ArmInstruction.source_line → op-index → op_offset−code_base → line),
          and host-link survival — the deliberate v0.12.0 release step (step 5
          oracle then asserts .text byte-identical to the no-DWARF build). NOT an
          idle-tick increment.
        - step (5a) MACHINE-OFFSET CAPTURE landed (PR A, v0.12.0 in progress):
          the encoder gap is closed — `compile_wasm_to_arm` now captures a
          `LineMap = Vec<(machine_offset, wasm_op_index)>` (synth-core backend.rs)
          during the encode loop (`code.len()` immediately before each `encode()`;
          the trailing literal pool and in-place LDR patch don't shift earlier
          offsets), carried on `CompiledFunction.line_map`. Purely additive: the
          map is never serialized, so `.text` is byte-identical (the existing
          differential fixtures + `test_line_map_is_wellformed_dbg001` assert
          monotonic in-bounds offsets and deterministic, unperturbed code). ARM
          only; RISC-V carries an empty map (follow-up).
        - step (5b) EMIT landed (PR B #429, a89ef28, v0.12.0 in progress):
          gimli is now a PRODUCTION dep of synth-core (Cargo.toml + the
          hand-written `crates/BUILD.bazel` synth-core `deps` — from_cargo makes
          `@crates//:gimli` available but the manual rust_library must list it;
          cargo passed locally while Bazel reddened E0433 until fix 63c510f).
          `--debug-line` (clap flag, EXPERIMENTAL caveat) gates emission: when set
          AND the input wasm carries `.debug_line`, synth reads the input rows
          (`read_input_dwarf_line`), composes addr→source via the captured
          `line_map`, and emits a FULL DWARF unit (DW_TAG_compile_unit with
          DW_AT_stmt_list → `.debug_line`, so a normal `dwarf.units()` walk reads
          it — not just a bare `DebugLine` program). Three oracles
          (dwarf_debug_line_emit_394.rs): additive-on-dwarf-input (byte-compares
          .text/.data/.bss, asserts `.debug_*` flag-gated), no-op-on-nodwarf-input
          (whole-.o identical), and resolves-arm-addr-to-source (walks the normal
          unit path, 110 in-range rows → non-zero lines). Frozen fixtures
          untouched. KNOWN GAP closed by step 5c: emitted `.debug_*` addresses are
          `.text`-base-0 with NO relocations, so they are CORRECT in the object
          but WRONG on a linked image — a `--debug-line` consumer (jess, actively
          Renode/silicon-debugging gust, the plausible first consumer) would get
          silently-wrong source lines after host-link. The v0.12.0 TAG is HELD for
          step 5c (advisor-confirmed: PR B in main is default-off + frozen-safe, so
          it banks the work at zero risk; the tag waits for relocations).
        - step (5c) RELOCATIONS LANDED (PR C #430, merged 9a34c8d; SHIPS in
          v0.12.0): C1 generalized elf_builder's `.rel.text`-ONLY machinery to
          PER-SECTION REL tables (`extra_relocations` + `add_section_relocations`;
          `.rel.debug_*`, REL in-place addend); byte-identical when off — the
          frozen gust whole-`.o` no-op oracle is the end-to-end proof, and
          cabi_arena_realloc_linkability_418 `.rel.text` stays byte-identical.
          C2: a custom gimli `write::Writer` (`RelocWriter`) overrides ONLY
          `write_address`, so just the two `.text` references (line program
          `DW_LNE_set_address` + CU `DW_AT_low_pc`) become `R_ARM_ABS32` against a
          global `__synth_text_base` (st_shndx=.text, value 0); internal DWARF
          cross-refs stay concrete (do NOT use gimli's blanket `RelocateWriter`).
          Addend 0 ⇒ `.debug_*` bytes byte-identical to PR B. Oracle
          `rel_debug_relocations_shift_addresses_to_correct_line_394` applies the
          reloc at a NONZERO base and asserts every row shifts by exactly the base
          with its source line preserved; CONFIRMED end-to-end with a real
          `arm-none-eabi-ld -Ttext=0x08000000` link (readelf decodedline → correct
          lines). FAST-FOLLOW: `__synth_text_base` is global ⇒ linking >1
          `--debug-line` object collides (fails LOUD); local-STT_SECTION fix is
          blocked by the hardcoded `.symtab` sh_info=1 — jumps priority iff a
          consumer links multiple synth objects. GOTCHA recorded: dependabot #436
          (gimli 0.31→0.33, `LineProgram::new` 5→6 args) broke main after PR C
          merged textually-clean on a stale base; fixed in #439.
    status: implemented
    tags: [toolchain, dwarf, debuggability, elf, meld-coordination, feature-loop, release-v0.12.0, synth-394]
    links:
      - type: derives-from
        target: VCR-001
      - type: constrained-by
        target: VCR-RA-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        Tier 1: a synth-compiled ELF from a DWARF-carrying wasm, loaded in
        gdb/lldb (or Renode) against the target, stops at the correct SOURCE line
        on a PC breakpoint and shows a file:line backtrace; `.text` byte-identical
        to the no-DWARF build (DWARF additive, non-loadable) ⇒ all frozen fixtures
        unchanged. Tier 2: a local variable resolves to its register/stack
        location at a breakpoint, validated once the VCR-RA value→location map
        exists.

  - id: VCR-COV-001
    type: sw-req
    title: "MC/DC source-to-object traceability: synth's branch folding changes witness's decision set (synth #396)"
    description: >
      synth #396: witness measures MC/DC by instrumenting WASM branches, but
      synth's WASM→ARM lowering CHANGES the branch set, so the WASM-level MC/DC
      does not 1:1 represent the OBJECT code's structural coverage (DO-178C
      6.4.4.2 / ISO 26262 ASIL D source-to-object obligation). Three directions,
      all present in synth today (select→cmov, the #390 pass-4 compare→br_if
      fusion, i64-compare, br_table):
        (1) FOLD to predication — a WASM decision becomes branchless (no PC
            branch). SAFE: WASM-level MC/DC stays authoritative; the object code
            realizes the same decision via a flag, no untraceable branch.
        (2) ELIMINATE a provably-constant branch — one side unreachable ⇒ MC/DC
            infeasible by construction. Needs JUSTIFICATION, and scry's
            constant-condition/reachability analysis is the sound evidence that
            the dead side is justified-deactivated, not a coverage hole.
        (3) SPLIT into N object branches (i64 cmp → cmp/bne/cmp; br_table →
            ladder) — compiler-INTRODUCED branches. Needs object-level MC/DC OR a
            faithful-implementation argument that the source decision's vectors
            cover them. The one direction that genuinely ADDS obligations.
      FIX = the SAME provenance spine as VCR-DBG-001 (#394): synth emits a
      decision-provenance map per WASM decision (br_if/select/if/br_table) →
      {1:1 branch | folded-predication | eliminated-constant(+scry evidence) |
      split-into-N}. One mechanism (the source_line threading already present),
      two consumers — the debugger (DWARF) and a coverage reconciler (witness).
      The reconciler keeps WASM MC/DC authoritative for (1), marks scry-proven
      dead branches justified for (2), flags (3) for object coverage.
      Coordinate with witness (consume the map) + scry (dead-branch evidence,
      ties to VCR-RA-010 / scry#51).
    status: proposed
    tags: [toolchain, mcdc, structural-coverage, do-178c, witness-coordination, scry, traceability, synth-396]
    links:
      - type: derives-from
        target: VCR-001
      - type: refines
        target: VCR-DBG-001
      - type: constrained-by
        target: VCR-RA-010
      # scry FEAT-023 / REQ-012 (shipped v1.13.0, 2026-06-20): per-program-point
      # `operand_stack: Vec<AbstractValue>`. A decision's CONDITION values live on
      # the operand stack, so this is the granularity the MC/DC reconciler needs
      # to classify a folded/eliminated branch precisely (synth#396 / witness#109).
      - type: traces-to
        target: scry:REQ-012
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        A synth-compiled module's witness MC/DC truth table reconciles against
        the ARM object code via the decision-provenance map: every WASM decision
        is classified (folded / eliminated / split / 1:1); folded decisions keep
        their WASM-level obligation; scry-proven-dead branches are marked
        justified-infeasible (not gaps); split decisions either get object-level
        MC/DC or a recorded faithful-implementation argument. No object branch is
        untraceable to a source decision. Frozen fixtures bit-identical (the map
        is emitted metadata, not a codegen change).

  - id: VCR-DMA-001
    type: sw-req
    title: Volatile DMA segment — loads/stores in a marked range not cached or reordered
    description: >
      An integrator can mark a segment of the fused linear memory as VOLATILE —
      the DMA transfer window. During a DMA-owned window an external agent (the
      DMA engine, which gale models as a Component-Model `own<buffer>` handoff,
      gale#124) rewrites the segment out-of-band, so synth must treat that byte
      range `[base, base+len)` as volatile: a load or store whose address falls
      inside a marked range must NOT be cached, hoisted, common-subexpression-
      eliminated, or reordered across the transfer boundary — each access
      re-materializes its address and re-issues the memory operation. gale's
      decision DD-DMA-REGION-001 places the DMA buffer in a dedicated shared
      segment precisely so the range is concrete and verifier-visible.

      PHASE 1 (LANDED — flag + plumbing + traceability): synth accepts
      `--volatile-segment <base>:<len>` (hex or decimal, repeatable), parses it
      into `CompileConfig.volatile_segments` (crates/synth-core/src/backend.rs),
      and threads it to codegen.

      PHASE 2 (LANDED — the codegen back-off, #543): the optimizer's
      address-caching passes HONOR the ranges. (a) The #468 base-CSE /
      const-address-fold (`SYNTH_BASE_CSE`, `optimizer_bridge::plan_base_cse`)
      excludes any const-address access whose 4-byte window intersects a marked
      range from its fold set — the access keeps its verbatim per-access
      materialize-and-access codegen while accesses outside the range still fold
      (surgical, per-access). Dynamic (statically-unknown) addresses were never
      fold candidates, so they always stay verbatim — the conservative stance.
      (b) const-CSE (`SYNTH_CONST_CSE`, both the bridge-level cache and
      `liveness::apply_const_cse`) declines WHOLESALE while any range is marked:
      a cached constant cannot be classified address-vs-data at that level, so
      every constant is re-materialized at each occurrence (conservative v1).
      Nothing else on the pipeline deletes, forwards, or reorders a linear-memory
      access (IR CSE deliberately never CSEs MemLoads; DCE removes only
      unreachable blocks; the frame-slot passes are SP-relative-only, and linmem
      is never a frame slot), so every marked access is issued verbatim, in
      program order. Empty ranges (the default) change nothing by construction —
      the frozen-codegen byte gate holds untouched. Oracles:
      crates/synth-cli/tests/volatile_segment_phase2_543.rs (red→green byte
      lattice, red-confirmed against pre-change main) and
      scripts/repro/volatile_segment_543_differential.py (unicorn-vs-wasmtime:
      ranges preserve RESULTS, only access patterns change).

      Deferred follow-up: honoring a wasm custom-section convention meld emits
      (so the range travels with the module) in addition to the explicit CLI
      flag (#543 option 2).
    status: implemented
    tags: [dma, volatile, memory, codegen, const-cse, base-cse, gale-integration, synth-543, phase-2]
    links:
      - type: derives-from
        target: VCR-001
      - type: constrained-by
        target: VCR-RA-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        Tracks GitHub issue #543 (see description + `synth-543` tag).
        Phase 1 (met): `--volatile-segment 0x20001000:4096` parses into
        `CompileConfig.volatile_segments` with base=0x20001000 and len=4096;
        malformed input (`--volatile-segment garbage`) is rejected with a
        non-zero exit and a descriptive error; on the DEFAULT configuration a
        compile WITH the flag is `.text`-byte-identical to one WITHOUT it.
        Phase 2 (met): const-CSE and the #468 base-CSE decline for accesses
        overlapping a marked range — the red→green byte-lattice oracle
        (volatile_segment_phase2_543.rs: folded < window < baseline .text, and
        a full-coverage range byte-identical to the lever never firing) FAILS
        on pre-change main and passes after; the unicorn-vs-wasmtime
        differential (volatile_segment_543_differential.py) proves the ranges
        preserve results in all four build modes; every marked access is issued
        verbatim in program order (no pass deletes/forwards/reorders linmem
        accesses). No frozen fixture uses the flag, so no re-freeze was needed
        (frozen anchors pass untouched).

  # ---------------------------------------------------------------------------
  # Scalar f32 hard-float (GI-FPU-002) — NOT DEFINED HERE.
  #
  # PR #705 recorded the phase-1 f32 delivery by declaring a SECOND `GI-FPU-002`
  # artifact at this point in the file. The id was already defined in
  # artifacts/gale-integration.yaml (its namespace home — GI-002 -> GI-FPU-001 ->
  # GI-FPU-002 -> GI-FPU-VER-001 form one chain there), so rivet loaded one over
  # the other and reported `status: proposed` for a requirement the README and
  # CHANGELOG both report as met (#369 closed, f32 v0.41 / f64 v0.43, VFP
  # spilling v0.53). This file is the single source of truth for the VCR-*
  # program's roadmap status, not for the GI-* gale-integration requirements.
  #
  # The delivery evidence was merged into the single GI-FPU-002 in
  # artifacts/gale-integration.yaml, which now carries `status: implemented`.
  # ---------------------------------------------------------------------------

  # ---------------------------------------------------------------------------
  # Track D — schedulability: sound static WCET bound (#778)
  # ---------------------------------------------------------------------------

  - id: VCR-WCET-001
    type: sys-verification
    title: "Sound static per-function WCET bound (--emit-wcet) — phase 3 inter-procedural composition landed"
    description: >
      --emit-wcet emits a SOUND static per-function worst-case cycle bound
      (synth-wcet-v1 sidecar) as gale spar's T3/T4 C_i input — a proven ceiling,
      never a DWT observation. The bound is CONDITIONAL on a zero-wait-state
      in-order Cortex-M3/M4 pipeline (recorded in the sidecar precondition); the
      per-op worst cases are MAX over {M3,M4} from an EXHAUSTIVE no-wildcard cycle
      table (crates/synth-backend/src/wcet.rs), pinned sound-critical in
      claims.yaml (SYNTH-WCET-CYCLE-MODEL). SOUNDNESS = decline > guess: anything
      uncertain LOUD-DECLINES with a machine reason rather than emit a number it
      cannot defend.

      Phase 1 (v0.46): loop-free functions = EXACT conservative sum (every insn
      once, both arms of every if). Phase 2 (v0.47): canonical const-bound counted
      loops PROVEN by a symbolic walk over the final stream (wcet_loops.rs);
      --wcet-hints (synth-wcet-hints-v1) is an UNTRUSTED scry seam verified against
      synth's own derived trip and rejected with machine reasons otherwise.

      Phase 3 (v0.48, THIS entry): INTER-PROCEDURAL COMPOSITION over the DIRECT
      call graph. A caller containing a direct BL func_N to a LOCAL bounded callee
      is now BOUNDED (was a blanket `call` decline): total(f) = own_cycles(f) +
      Σ_site multiplier(site) × total(callee), composed callee-first over the
      acyclic graph (crates/synth-backend/src/wcet_compose.rs, a PURE memoized DFS
      over per-function intermediates — never re-touches the instruction streams,
      so trivially frozen-safe). own_cycles prices each direct BL at the
      branch-with-link overhead BL_BLX_CALL_OVERHEAD_CYCLES = 4 (MAX over {M3,M4}:
      both TRMs time BL/BLX as 1+P, P the pipeline refill 1..3, worst case 1+3=4 —
      the same branch-with-refill class the table already prices for taken
      Bx/BOffset/BCondOffset; the callee's own return is counted in the callee's
      bound so no return penalty is added). The per-site multiplier is the call
      site's PROVEN execution count, so a callee invoked inside a proven counted
      loop is counted trip× — never once (the #1 composition soundness trap, killed
      by construction).

      NAMED RESIDUAL DECLINES (decline-honesty, nothing deleted — moved onto what
      is not provably composable):
        - RECURSION: any cycle in the direct call graph (self- or mutual) declines
          `recursion` on every function on/reaching the cycle — an upper cycle
          bound cannot be composed from a recursive graph.
        - INDIRECT CALL: Blx <reg> / call_indirect / function-pointer dispatch
          (__meld_dispatch_import) declines `indirect-call` — callee not statically
          known.
        - EXTERNAL/IMPORT: a direct BL to a symbol with no per-function body in the
          module (an import under --relocatable) declines `call`.
        - PROPAGATION: a caller whose bounded body directly calls a declined callee
          declines `callee-unbounded` — a decline travels UP the graph.

      Data-dependent loops, non-canonical shapes, i64 software div/rem, and
      non-M3/M4 cores (incl. the ambiguous -eabihf M4F/M7 triple) still
      LOUD-DECLINE unchanged. Frozen-safe (.text byte-identical, frozen 10/10;
      the Bl/Blx op_cost change is WCET-path-only). Richer hint certificates
      (data-dependent bounds, scry) remain the named follow-up.

    links:
      - type: verifies
        target: VCR-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        crates/synth-cli/tests/wcet_bound_gate.rs (CI-gated, cargo test +
        explicit ci.yml step): compiles REAL .wat fixtures and asserts on the
        sidecar. Phase-3 additions — direct_call_chain_composes_exact_bounds
        (leaf 19 / mid 51 / root 136 EXACT literals + instr floor + root covers
        both mid-calls), direct_call_inside_proven_loop_counts_callee_per_trip
        (callee counted 10× under a proven trip-10 loop; bound ≥ 10×leaf + trip
        floor), self_recursion_declines_with_recursion_reason,
        mutual_recursion_declines_both, indirect_call_declines_with_indirect_reason,
        declined_callee_propagates_up_as_callee_unbounded,
        external_import_call_declines_with_call_reason. 8 pure-composer unit tests
        in wcet_compose.rs (chain/diamond/loop-multiplier/self+mutual+transitive
        recursion/propagation/external). claims.yaml pins
        BL_BLX_CALL_OVERHEAD_CYCLES = 4 (SYNTH-WCET-CYCLE-MODEL); claim_check green.
        Frozen anchors 10/10 untouched (WCET is a byte-invisible sidecar).

  - id: VCR-WCET-002
    type: sys-verification
    title: "WCET bounded self-recursion via a verified depth-hint (#778 phase 4 / #49)"
    description: >
      Phase 4 (#49) CONVERTS the phase-3 `recursion` decline for exactly ONE
      provably-sound shape, keeping every other recursion a LOUD decline (the
      decline is MOVED, never deleted — the v0.46 doctrine). SOUNDNESS = decline >
      guess: a depth × per-frame bound is emitted only when synth can PROVE the
      recursion cannot exceed the derived depth for ANY i32 input.

      THE PROVABLE SHAPE (crates/synth-backend/src/wcet_recursion.rs): a
      SINGLE-self-call chain (exactly one BL to the function's own func_<idx>,
      executed at most once per frame — loop multiplier 1) whose controlling value
      is ENTRY-INDEPENDENTLY bounded by a mask: m = (param & K) ∈ [0,K] for any
      runtime param. The base guard and the recursive argument read the SAME masked
      quantity (identical base register + mask constant); the argument is m − step
      (const step); and the self-call is proven CONTROL-DEPENDENT on the guard (the
      guard's taken target is a base block that does NOT contain the self-call, so
      the self-call is unreachable when the guard fires — this is what stops the
      dangerous (base−step)&K re-mask from diverging). The guard→self-call arg
      region must ALSO be STRAIGHT-LINE + SINGLE-ENTRY (no branch inside it, no
      branch targeting into it) so the decrement is provably UNCONDITIONAL — a
      conditional decrement (gated on a second guard) would let a runtime path skip
      it and recurse unbounded while the linear walk still saw m−step. synth then
      DERIVES its own maximum depth via the loop trip machinery
      (wcet_loops::exit_index, evaluated at BOTH init endpoints 0 and mask — the max
      is the entry-independent worst case regardless of step direction;
      wrap/divisibility-safe; Eq/Ne base guards restricted to step ±1), and the
      composer folds the certified self-edge as (max_depth+1) × frame_cost instead
      of declining. The +1 counts the BASE frame (runs own_cycles, no self-call);
      omitting it undercounts by one frame → the fold is pinned sound-critical in
      claims.yaml (SYNTH-WCET-CYCLE-MODEL).

      THE HINT SEAM (untrusted oracle + sound checker, no scry dependency): a
      --wcet-hints `recursion_depth` entry only GATES consumption (a bound this
      consequential is opt-in, mirroring the equality-exit loop-hint gate). The
      emitted depth is ALWAYS synth's DERIVED ceiling, never the raw hint. Rejected
      with machine reasons otherwise: a hint below the derived depth →
      `hint-below-derived-depth`; a shape synth cannot prove →
      `hint-unverifiable-recursion`.

      NAMED RESIDUAL DECLINES (decline-honesty, nothing deleted):
        - TREE recursion (≥2 self-calls per frame, e.g. fib): depth × per-frame
          would under-count the exponential frame tree → reject
          `hint-unverifiable-recursion` (the single-self-call gate is the direct
          guard against this fatal class).
        - UNCAPPED countdown (recursive arg is a raw runtime param, no mask):
          runtime-unbounded at one end of i32 (negative entries diverge) → reject
          `hint-unverifiable-recursion`.
        - MUTUAL / INDIRECT recursion: the certificate exempts only a function's OWN
          self-edge; a distinct cross-function cycle still declines `recursion`.

      Frozen-safe: .text byte-identical (frozen 10/10; the only codegen-adjacent
      change is a new current_func_index config field, byte-invisible). Richer
      recursion certificates (clamp-bounded controlling values, data-dependent
      depths, scry-supplied bounds) and inter-procedural recursion composition are
      named follow-ups.

    links:
      - type: verifies
        target: VCR-001
      - type: refines
        target: VCR-WCET-001
    fields:
      req-type: functional
      priority: should
      verification-criteria: >
        crates/synth-cli/tests/wcet_bound_gate.rs (CI-gated, cargo test + explicit
        ci.yml step) — 5 phase-4 fixtures: masked_recursion_correct_hint_converts_to_bound
        (BOUNDED, derived max_depth 15 / frame_count 16 / 752 cyc EXACT literal +
        frame floor; emitted depth is DERIVED not the raw hint),
        masked_recursion_unhinted_still_declines (the decline the seam converts —
        non-vacuity), masked_recursion_too_low_hint_rejected_red_first
        (hint 3<15 → declined + hint-below-derived-depth, RED-FIRST),
        tree_recursion_two_self_calls_rejected_even_with_hint (fib → declined +
        hint-unverifiable-recursion — the fib-trap guard),
        uncapped_countdown_recursion_hint_rejected_unverifiable,
        conditional_decrement_recursion_rejected_unverifiable (the decrement is
        gated on a SECOND guard over the raw param → a path skips it → unbounded;
        the straight-line/single-entry region check REJECTS it — the adversarial
        guard against modeling a conditional decrement as unconditional),
        mutual_recursion_stays_declined_even_with_hint. 3 pure-composer unit tests
        in wcet_compose.rs (certified self folds depth frames / folds non-self
        callee per-frame / a distinct mutual cycle STILL declines). Execution-side
        cross-check: scripts/repro/wcet_phase4_49_recursion_soundness.py under
        unicorn — md(0xFFFFFFFF) and md(0x7FFFFFFF) each execute 267 machine insns
        across all 16 frames ≤ 752 cyc (entry-independent, the mask soundness
        empirically confirmed). claims.yaml pins the (max_depth+1) frame fold;
        claim_check green. Frozen anchors 10/10 untouched.