Skip to content

The silent-miscompile evidence behind the #1093 decline is not a CI oracle — the guard survives, its justification does not #1097

Description

@avrabe

The evidence for v0.61's worst finding so far is not a CI oracle

#1093 was reported as a panic. Sweeping the class found the same root cause in a shape that does not panic — it compiles, exits 0, and returns an uninitialized register:

(func (export "ipe") (param i32) (result i32)
  (i32.const 7)
  (if (param i32) (result i32) (local.get 0)
    (then (i32.const 42) (i32.add))))   ;; no else

Emitted on the direct ARM path before #1096:

movw r1, #7        <- the block PARAMETER
cmp  r0, #0
beq  +8            <- false path skips the then-branch
add  r3, r1, #42   <- r3 written ONLY on the true path
mov  r0, r3        <- result = r3

r3 is never written on the false path. wasmtime gives 7. RV32 block (param..)+br_if and loop (param..)+back-edge are the same shape.

The gap

#1096 makes the whole class decline, and that is the right fix. But the demonstration — the unicorn-vs-wasmtime differential that proved these three shapes returned wrong answers — lives in a lane scratchpad. It is not in scripts/repro/, not CI-wired, and not counted by the oracle-wiring floors.

So the artifact that survives is: a guard, plus tests asserting the guard declines. Nothing in the repo any longer demonstrates why the decline is mandatory rather than conservative. A future contributor looking to "improve reach" by lowering parameter-taking block types has the decline in front of them and no executable evidence of what it is protecting against — and the honest-sounding move ("this construct is simple, let's support it") is exactly how the miscompile comes back.

This is the inverse of the usual failure. Normally a check exists and points at the wrong thing; here the check is right and the evidence for its necessity was thrown away after use.

Proposed

Promote the lane's differential into scripts/repro/ as a permanent, CI-wired oracle with a non-vacuity floor (# ci-checks: emulations >= N, the scripts/oracle_run.py convention), pinned red-first against the pre-#1096 binary:

  • it must show the three silent shapes returning wrong values on the old code, and
  • the guard declining them on current main.

That makes the decline's justification reproducible rather than archival, and it gives any future multi-value lowering work an acceptance oracle it must pass before the guard can be relaxed — which is the only safe way to eventually remove it.

Related: #1093, #1096. Same discipline as the wcet_phase*_soundness.py cross-checks and the expansion_canary_gate_1021.py negative-control tiers — the evidence for a refusal is as much an artifact as the refusal.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions