Skip to content

Commit d79f6ad

Browse files
avrabeclaude
andauthored
docs(vcr): record that #490 (systemic optimized-path callee-saved clobber) blocks the non-leaf prologue lever (#428, #490, #242) (#492)
The roadmap's non-leaf thin-forwarder entry described the lever as the next buildable piece. Implementing it this session revealed its 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 with no saving push, so even the silicon-validated `control_step` clobbers r4/r6/r8 (masked because it is top-level / callers fall back to the pushing direct selector). That is a systemic base-selector ABI bug (#490), latent in the self-contained optimized path (gale ships `--relocatable`, which uses the register-preserving direct selector), that BLOCKS this lever's flip. Updates the trace so the lever's blocked-by relationship is recorded (not a gate surprise): the lever stays unmerged on `wip/nonleaf-prologue-blocked-on-leaf-clobber` (its differential is the #490 repro) until the systemic fix lands. Docs-only, frozen-safe; rivet validate clean (0 non-xref errors). Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 397c6bf commit d79f6ad

1 file changed

Lines changed: 21 additions & 0 deletions

File tree

artifacts/verified-codegen-roadmap.yaml

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -575,6 +575,27 @@ artifacts:
575575
`br_if`->predicated-branch half of the cmp->select item (split candidate).
576576
All three are SEPARATE gated steps (flag-off -> differential -> silicon),
577577
never an idle-tick increment.
578+
LEVER IMPLEMENTED, BLOCKED ON A BASE-SELECTOR CLOBBER (2026-06-25, #490): the
579+
non-leaf prologue lever was implemented flag-off (relax `elide_dead_frame` +
580+
`shrink_callee_saved_saves` across DIRECT calls; 9 unit tests:
581+
even-count/8-byte-aligned push, keeps callee-saved held across a call,
582+
declines on indirect/non-8/live-frame). Its execution differential then
583+
proved the shrink's soundness is NON-LOCAL — pruning a forwarder's save-set
584+
is only correct if every callee preserves r4-r8, which the OPTIMIZED PATH
585+
does not: `alloc_i32_scratch` hands out the callee-saved [R4..R8] pool to
586+
every function with a scratch temp and the path emits NO callee-saved push,
587+
so even the silicon-validated `control_step` clobbers r4/r6/r8 (masked only
588+
because it is top-level / its callers fall back to the pushing direct
589+
selector). This is a SYSTEMIC base-selector ABI bug (#490), not a small-leaf
590+
special case — the scratch pool is shared, so fixing it (push-what-you-use in
591+
the optimized path) re-freezes control_step/filter_step and needs gale
592+
re-validation. NOT a live miscompile in shipped firmware (gale ships
593+
`--relocatable`, which uses the direct selector that preserves r4-r8
594+
correctly); it is a latent optimized-path violation that BLOCKS this lever's
595+
flip. The lever stays unmerged (branch wip/nonleaf-prologue-blocked-on-leaf-clobber,
596+
the differential = repro) until #490 lands. This is a "correctness from
597+
construction" item (the north star itself) and gates the perf lever
598+
downstream of it.
578599
status: approved
579600
tags: [oracle, differential, coverage, mcdc, validation, track-c, riscv]
580601
links:

0 commit comments

Comments
 (0)