Epic: reach and beat native codegen — proof-carrying specialization as the mechanism (VCR-*)

[avrabe]

Reworked 2026-08-13. The previous body framed this as "replace the
patch-accreting selector and allocator", listed six VCR items, and left all
six unchecked since June while every one of them shipped work. That framing
had two problems: it described internal machinery rather than an outcome
anyone outside can check, and its checklist understated reality badly enough
to mislead. This version states the outcome, the measured position, and the
mechanism — and keeps the residuals that are actually open.

The goal

Match native code generation, and beat it where a verified compiler can do
something an unverified one cannot.

That second clause is the whole thesis, and it is not aspiration — it is
already measured.

Where we actually stand (artifacts/parity-benchmark.md, regenerable)

Bare-metal Thumb-2, .text bytes, synth AOT vs native C/Rust at -Os:

kernel	synth default	native ref	ratio
gust_poll	724 B	208 B (rustc/LLVM)	3.48×
gust_mix (Q8)	32 B	12 B	2.67×
flat_flight	384 B	180 B (gcc -Os)	2.13×
falcon_axis (f32/VFP)	72 B	44 B (gcc -Os)	1.64×
gust_mix clamp	84 B	26 B gcc / 12 B LLVM floor	3.23×

So on the default path we are 1.6×–3.5× larger than native. That is the
honest headline and it should stay at the top of this issue until it moves.

But the mechanism that closes it is already demonstrated

With a proven premise supplied as a certificate, the same kernels:

kernel	synth + proven premise	native ref	ratio
gust_mix clamp (ch ∈ [524,1524])	14 B	26 B gcc / 12 B LLVM floor	0.54×
gust_poll bounds (slot ∈ [0,63])	104 B	104 B unguarded floor	1.00×

Read those two rows carefully, because they are the argument for this whole
programme:

• 0.54× — synth beats gcc -Os and lands within 2 bytes of the LLVM floor.
• 1.00× — the software bounds-guard tax is eliminated ENTIRELY. The guarded
  build equals the unguarded build. Not reduced. Gone.

An unverified compiler cannot do this. LLVM cannot elide a bounds check it
cannot prove is redundant, and it has no way to accept a proof from outside.
synth can, because the elision is discharged by a certificate
(SYNTH_FACT_SPEC, ordeal-certified) rather than assumed. Verification is not
a tax we pay for safety — it is the thing that lets us go faster than the
alternative.

Therefore the strategy is not "optimize harder"

Chasing LLVM's peephole quality on the unproven path is a losing race against
decades of engineering. The winning line is to widen the set of premises we
can prove and consume, so more code takes the 0.54× path instead of the 3.48×
one.

Everything below is scored against that.

Tracks

A — Consume more proofs (the differentiator). VCR-PERF-002 fact-spec
(#494) is the shipped mechanism; the clamp and bounds rows above are its
results. Open: widen the provable-premise classes, and close the loop with
scry so premises arrive automatically rather than by hand.

B — Close the default-path gap (the floor). The 1.6×–3.5× is mostly
allocator and selector quality. VCR-RA-001 (Belady spilling) is verified and
default-on; the remaining line is the allocator endgame — replace greedy
with graph-colouring / optimal-spill (VCR-DEC-001/002), with VCR-RA-003 as
the acceptance oracle. This is the one item on the old checklist with
substantial work genuinely remaining.

C — Semantics you can audit (the moat). VCR-SEL-001 (Rocq-discharged
selector DSL, shipped default-on), VCR-ISA-001 (Sail-generated ARM model,
generate-don't-mirror since #667), VCR-WASM-001 (WasmCert-Coq source
semantics). These are what make Track A sound rather than merely fast.

D — Instruments that cannot lie (the discipline). VCR-ORACLE-001 and the
oracle-wiring ratchet. The recurring finding across v0.53–v0.56 is that defects
concentrate in checkers, and that a check insensitive to the failure it exists
to detect is worse than no check. Every claim above is regenerable or it does
not count.

The honest gaps

• Cycles are unmeasured. Every cycles cell in the benchmark reads
  OPEN — gale silicon (DWT). The size story is real and the speed story is
  unproven. Do not let this issue drift into claiming performance parity on
  the strength of byte counts.
• The default path is still 1.6×–3.5×. Track A moves work off it; Track B
  lowers it. Neither is finished.
• SYNTH_FACT_SPEC rows carry ordeal ADMITs (2 for clamp, 8 for bounds).
  That is disclosed in the benchmark and is a real residual, not a footnote.

Status of the original six (graded, not ticked)

Detail and evidence in the audit comment;
values from the CI-gated claims.yaml, not from greps.

• VCR-RA-001 — done, verified and default-on
• VCR-SEL-001 — substantially done, increments 1–4 default-on, 50 rules
• VCR-ISA-001 — substantially done, Sail bridge + generate-don't-mirror
• VCR-WASM-001 — substantially done, phases 1+2
• VCR-ORACLE-001 — first deliverable done
• VCR-VER-001 — demonstrated, evidence in scripts/repro/vcr_ver_001_gate.md

Not closing them individually here; use Refs #242, never closes, so this
umbrella keeps its remaining items.

What "done" means for this epic

Not "all six ticked". This closes when the default path is within ~1.2× of
native on the benchmark kernels, the proven-premise path stays at or below 1.0×,
and cycles are MEASURED rather than OPEN. Until then it stays open with the
numbers at the top kept current.

[avrabe]

VCR-RA-001 — step 1 landed as PR #243. Register def/use + liveness foundation (crates/synth-synthesis/src/liveness.rs): reg_effect(&ArmOp) (precise scalar def/use) + local_dead_defs() (sound dead-store detection, the generic form of #221). Pure analysis, not wired into codegen → fixtures bit-identical (control_step ORACLE PASS), 269 lib tests + 7 new. Next on VCR-RA-001: CFG-aware liveness → interference graph over virtual registers (pre-allocation pressure) → spill-under-pressure (removes the exhaustion hard-fail that forces the cost-gates).

[avrabe]

VCR-RA-001 — step 2 (PR #245): redundant-constant detection (const-CSE analysis). redundant_const_defs() — the forward dual of local_dead_defs; flags constant materializations whose value is already resident. Reproduces gale's measured flat_flight waste (#209): the 6× #0x7e clamp → 5 redundant. Pure detection, not wired in; 274 lib tests, control_step ORACLE PASS. The two halves of gale's #1 lever are now both detectable (dead-store + redundant-const); the transform (keep clamp bounds resident) migrates in with the allocator.