You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Fail honestly, never guess: out-of-layout local emitted a guessed frame offset instead of a loud error #378
[synth maintainer side — issue-hunt loop] Honesty-hardening, found via the oracle-gate cleanup pass.
Principle
synth's stated contract is never emit plausible-but-wrong output — GI-FPU-001 (decoder → loud-skip, not silent-drop), #180/#185 (encoder Ok-or-Err, never corrupt), and the defensive-panic pattern. Three sites violated it.
The shortcut
select_with_stack's LocalGet/LocalSet/LocalTee handlers, when a local index is absent from the computed frame layout, fell through to a guessed stack offset:
}else{// Local not in layout (shouldn't happen for valid wasm,// but fall back to legacy behaviour for compatibility).
addr:MemAddr::imm(Reg::SP,(*local_idx asi32 - 4)*4),// GUESS}
(local_idx-4)*4 is the old pre-#204/#223 frame layout. Under the current compute_local_layout (#223), this guess is wrong — so if the branch ever fires (a layout-computation bug, or malformed wasm that slipped validation), it silently emits a load/store to the wrong stack slot instead of failing. Same silent-miscompile class as the decoder _ => None (#369/#374) and the encoder index-drop (#206).
Fix
Replace the guess with a loud Err (loud-skips the function), naming the local index — the GI-FPU-001 contract.
Verification (frozen — no behavior change for valid input)
The branch is dead on valid input (every local a valid module declares is in the layout), so:
the three frozen fixtures stay bit-identical (control_step 0x00210A55, flight_seam 0x07FDF307, div_const 338/338);
the full workspace test suite is green and no test triggers the new Err — confirming the path was genuinely unreachable, i.e. dead defensive code that could only ever have silently miscompiled.
No measured cycle/size delta (which is why it isn't an oracle-gate cleanup filing) — this is a correctness/honesty hardening: converting a latent silent-miscompile into a loud failure. One reversible change, three symmetric sites.
Activity
fix(#378): fail honestly on out-of-layout local — never guess a frame…
fix: encode_operand2 fails honestly on un-encodable ARM32 immediate (…
chore(release): v0.11.50 — #382 large load/store offset + #378/#381 h…
#383: --shadow-stack-size flag + VCR-MEM-001 design (honest-Err scaff…
test(vcr-oracle): pin the #518 cross-backend contrast — RV32 loud-ski…
fix(encoder): T3 ADD.W raw-imm packing — ADDW (T4) for offsets 0x100.…