Skip to content

Commit 31db4a0

Browse files
avrabeclaude
andauthored
docs(vcr): record the optimizer_bridge/selector frontier second arc + the #509 negative result (#242) (#510)
Appends a dated slice to VCR-ORACLE-001's history covering the 2026-06-26 second arc: #496 (R12-exhaustion decline-to-direct, PR #502), #503 (AAPCS stack-arg cap-lift, shipped v0.16.0, PR #504), #507 (optimized-path br_table decline, PR #508), each with its new CI execution oracle (r12-spill-496, stack-args-503, br-table-507). Most importantly it records #509 as a LOAD-BEARING NEGATIVE RESULT so the decline-to-direct shortcut is not re-attempted: the direct selector (the shipped --relocatable path) drops the carried value of a value-returning br/br_if/ br_table-direct, and the shortcut cannot fix it because the IR carries no block-result arity (WasmOp::Block is a unit variant) — a non-empty-vstack decline can't distinguish a carried result from an unwound void-target value, so it over-refuses valid code. This is the sharpest evidence yet for VCR-SEL-001's selector-collapse motivation (the hand-written selectors lack the structured block-arity model a verified DSL carries by construction); the real fix is arity-threading, cross-cutting and silicon-gated. Docs-only, behavior-frozen by construction: frozen byte gate bit-identical; rivet validate non-xref ERROR count 0 (unchanged 49/75/0 baseline). Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent ed3e48c commit 31db4a0

1 file changed

Lines changed: 45 additions & 0 deletions

File tree

artifacts/verified-codegen-roadmap.yaml

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -634,6 +634,51 @@ artifacts:
634634
register-exhausting i32 folds silently miscompiled (no spill, no decline).
635635
All four are SEPARATE gated steps (flag-off / differential / silicon as
636636
applicable), never idle-tick increments.
637+
FRONTIER ADVANCED + A LOAD-BEARING NEGATIVE RESULT (2026-06-26, second arc,
638+
#496/#503/#507/#509): three of the cluster LANDED, each with a new CI
639+
execution oracle, and a fourth mapped the hard boundary of the
640+
decline-to-direct pattern. #496 RESOLVED (PR #502, `988ea3b`): the optimized
641+
path's `alloc_i32_scratch` borrowed R12/IP (the encoder's indexed-load base
642+
scratch, #212) on R4-R8 exhaustion → collision miscompile (control_step
643+
execution-faulted `add ip,ip,ip`=2×base; flight_seam_flat wrong values); fix
644+
flags exhaustion via a Cell and DECLINES the whole function to the direct
645+
selector (which spills), gated by `r12_spill_496_differential.py` (both
646+
silicon fixtures, default path, execute == wasmtime). #503 RESOLVED + SHIPPED
647+
v0.16.0 (PR #504, `8e917a2`): the SHIPPED `--relocatable` direct selector
648+
SKIPPED functions needing the AAPCS stack-arg path beyond a conservative cap
649+
(>8 scalar params, or a call passing >8 args) — 3 falcon helpers dropped; the
650+
incoming/outgoing stack-arg machinery was already generic, so the fix lifts
651+
the `>8` caps and leans on the existing 12-bit `[sp,#imm]` guards, unblocking
652+
2 of 3 (func_57/58); the 64-bit stack-param case stays refused. Gated by
653+
`stack_args_503_differential.py` (sum10/sum25-reading-param-24/outgoing/
654+
combined, all == wasmtime). This is the first SHIPPED-path member of the
655+
cluster, hence the v0.16.0 minor (the optimized-path-only #490/#483/#496/#507
656+
ride along, no individual tags). #507 RESOLVED (PR #508, `ed3e48c`): the
657+
optimized path DROPPED `br_table` during wasm→IR (no `cmp`, selector never
658+
loaded → all arms fell through); since the drop precedes `ir_to_arm`, the fix
659+
detects `br_table` on the RAW wasm op stream in `arm_backend` and forces the
660+
direct selector (#496-pattern), gated by `br_table_507_differential.py`
661+
(void seq/shared shapes × every selector). #509 — NEGATIVE RESULT, the
662+
load-bearing one: the DIRECT selector (so the SHIPPED `--relocatable` path)
663+
ALSO drops the carried value of a value-returning branch — `br`/`br_if`/
664+
`br_table`-direct to a result-typed block returns 0 for the dispatched arm
665+
(`pick(0)=0` vs wasmtime 10). The #507 decline-to-direct shortcut DOES NOT
666+
WORK here and must not be re-attempted: the IR carries no block-result arity
667+
(`WasmOp::Block` is a UNIT variant; the decoder tracks none), so a
668+
"non-empty vstack at the branch ⇒ decline" heuristic cannot distinguish a
669+
CARRIED result from an UNWOUND void-target value (`i32.const 1; br 2` to a
670+
VOID block is legal WASM that compiles correctly today), and the decline
671+
over-refuses valid code (broke 4 selector tests, 3 plain-`Br`). Trading a
672+
latent miscompile for a latent regression is not progress, and no shipped
673+
artifact hits it today (gust's `br_table` is void-dispatch) — so #509 is
674+
BACKGROUND priority and requires the REAL fix: thread block-result arity
675+
(decoder → `WasmOp::Block`/`Loop`/`If` → selector) + a result-register
676+
convention generalizing the #313 if/else reconciliation to labeled-block
677+
branches. That is precisely VCR-SEL-001's "(ii) collapse the selector
678+
accretion into one verified source" — the value-carry boundary is the
679+
sharpest evidence yet that the hand-written selectors lack the structured
680+
block-arity model a verified DSL would carry by construction. Cross-cutting,
681+
byte-changing, silicon-gated — never an idle-tick increment.
637682
status: approved
638683
tags: [oracle, differential, coverage, mcdc, validation, track-c, riscv]
639684
links:

0 commit comments

Comments
 (0)