Skip to content

fix(#970): count a CONDITIONALLY-written parameter as a parameter — ARM + RV32 uninitialised-stack-slot leak - #974

Merged
avrabe merged 4 commits into
mainfrom
fix/count-params-arm-rv32-970
Aug 14, 2026
Merged

fix(#970): count a CONDITIONALLY-written parameter as a parameter — ARM + RV32 uninitialised-stack-slot leak#974
avrabe merged 4 commits into
mainfrom
fix/count-params-arm-rv32-970

Conversation

@avrabe

@avrabe avrabe commented Aug 14, 2026

Copy link
Copy Markdown
Contributor

Closes #970.

The correction first: ARM does not fail the way #970 predicted

#970 read ARM's failure off a disassembly listing and expected cw_call(0, 42)
to return param 0's value — an ordinary wrong value — because the demoted
local's str looked like it sat at the branch merge point. Executing it
says otherwise. The beq jumps past the store (capstone-verified on
cb80e60c, --target cortex-m4 --relocatable):

push.w {r4, r5, r6, r7, r8, lr}
sub.w  sp, sp, #8
cmp    r0, #0
beq    +8            ; -> the ldr, skipping the store below
movw   r1, #5
str.w  r1, [sp]      ; INSIDE the then-arm, not at the merge point
ldr.w  r2, [sp]      ; <- on the fall-through path this slot was NEVER written
mov    r0, r2

So ARM has the same uninitialised-frame-slot read as RV32 — the same
information-disclosure shape, and on the plain shape, not only the call one.
This is exactly why the lane executed ARM separately instead of generalising
RV32's evidence.

Red-first, per backend, by execution

Both harnesses poison two distinct words so the mechanism is proven rather
than inferred: every stack word below the entry SP is 0xDEADBEEF, every
argument register the signature does not use is 0xFEEDFACE. "Read an
uninitialised slot" and "read the wrong argument register" therefore cannot be
confused. Measured on cb80e60c:

backend red green memory-poison leaks (red)
ARM Thumb-2 22/38 38/38 12
RV32 22/38 38/38 12
BUG cond_write_param(0x0, 0x2a):       want=0x0000002a got=0xdeadbeef  <- POISON
BUG cw_call(0x0, 0xabcdef01):          want=0xabcdef01 got=0xdeadbeef  <- POISON
BUG cw_last_of_three(0x0, 0x3, 0x4):   want=0x00000007 got=0xdeadbef2
BUG cw_high_param(0x0,...,0x1000,0x2000): want=0x00003000 got=0xdeadceef
ok  cw_loop / guard_* (all 22)         — read-first order already correct here

The failures are exactly the 16 cw_* fall-through vectors; every guard_*
case (the #457 zero-init local, both-arms writes, unconditional write, plain
params) is green in both states, so the differentials are sensitive to the
conditional-write class specifically and not to codegen churn.

The fix

With a declared param count in hand the bound is
min(referenced_locals(ops), declared) — the highest local index the body
touches, clamped by the signature — not the read-first count_params heuristic
capped by it. The old rule was exact in only one direction: the clamp stops a
read-before-write non-param local from being homed in an argument register
(#457), but taking the max over reads only demoted a param written on
one arm of an if. And because the demoted local's first access is a write,
the #457 zero-init skipped it too — hence the uninitialised slot rather than a
zero.

min (not a plain declared override) keeps the leniency for a body that only
touches the first few of many declared params.

referenced_locals moves to synth_core::wasm_op, next to
rewrite_memory_grow_zero and for the same stated reason: #851 landed a private
copy in the aarch64 backend, and shipping two more would make three copies of
one three-line rule that must agree. All three backends now share one
definition
; the aarch64 copy is deleted.

Negative control — run both ways, independently

reverted line ARM oracle RV32 oracle
ARM only FAIL 22/38, 12 leaks PASS 38/38
RV32 only PASS 38/38 FAIL 22/38, 12 leaks

Reverting one backend's bound reds only that backend's oracle. The two are
independent evidence, not one measurement reported twice.

Floors — measured, not computed

scripts/oracle_run.py reports emulations=38 for each harness, so each
declares # ci-checks: emulations >= 38 — the measured count exactly. The new
CI job closes with the #910 ledger at --min-oracles 2, so deleting or skipping
either step reds the job rather than quietly shrinking what CI asserts.

The summed --min-emulation-floor is deliberately not ratcheted: it is a
floor, the measured total rises 295,773 → 295,849 (both measured by running
oracle_wiring_check.py with and without the two new files) against a pinned
minimum of 295,726, and with several v0.57 lanes adding oracles in parallel a
single shared total is a fan-in conflict. Ratchet it once at release assembly,
together with the ORACLE_WIRING.md table (already stale at 295,621) and both
claims.yaml text pins.

Blast radius

Every scripts/repro/*.wat compiled for both backends (310 fixture ×
backend compilations), sha256 of .text diffed before/after. Exactly three
fixtures change
, and no RV32 output changes at all except the new fixture:

fixture change
cond_write_param_970.wat (arm + rv32) the new fixture — the fix
aarch64_param_homing_851.wat (arm) 366 → 348 B; contains the same cond_write_param shapes, now smaller (demoted-local frame slots become param registers)
rv32_cmp_select_472.wat (arm) 466 → 466 B, temp renumbering only. Its clamp declares 2 params but references only $a, so the count goes 1 → 2 and temps start at r2 instead of r1. Executed vs wasmtime: identical 44/49 before and after

cond_write_param itself now lowers to 16 bytes with no frame at all
(cmp r0,#0 / beq / movw r2,#5 / mov r1,r2 / mov r0,r1) — the param stays in
its register.

The one place this change widens rather than narrows behaviour is a >4-param
ARM signature. Verified it lands where it should: cw_high_param reads indices
4 and 5 from [sp,#0x18] / [sp,#0x1c] after a push of 6 registers with
frame_size = 0, i.e. frame_size + 24 + nsaa — the caller's frame, the
AAPCS incoming-stack-argument area, not a local slot.

Named residual, deliberately NOT closed

current_func_param_count == None still uses the read-first heuristic. It is
unreachable from the CLI (which always supplies a declared count) but reachable
via the direct compile_function API. Not closed here, on purpose: with no
declared count a write-first index is genuinely ambiguous — a param whose
incoming value is dead, or a non-param local — and both readings can be wrong.
Picking one is a compile_function API-contract decision, not a bug fix, and
inventing a bound to close a gap is the recurring burn this repo has taken
three releases running. It is documented as an honest residual on
CompileConfig::current_func_param_count and on each backend's helper.

Found in passing, filed separately: #973

The byte-identity sweep compiled rv32_cmp_select_472.wat for ARM, which
nothing in CI does, and turned up an unrelated pre-existing ARM miscompile:
a select whose condition is an i64 comparison and whose arms are computed
values always returns the then-arm — the else-arm's register is spilled and
reloaded with the then-arm's value, so both it arms move the same register.
Confirmed independent of this lane: the same 44/49 vectors match wasmtime on
binaries built before and after the #970 fix, with the identical five
failures. Filed as #973 with a minimal repro; not fixed here.

Gates

Each run without a pipe, exit code captured directly:

  • cargo test --workspacerc=0, 2787 passed / 0 failed
  • cargo clippy --workspace --all-targets -- -D warningsrc=0
  • cargo fmt --checkrc=0
  • python3 scripts/claim_check.py claims.yamlrc=0, 43/43 claims hold
  • python3 scripts/oracle_wiring_check.py --min-emulation-floor 295726rc=0,
    161 wired / 7 manual / 0 unwired / 0 undeclared

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe and others added 4 commits August 14, 2026 15:44
…am-write miscompile (ARM + RV32)

`count_params` counts only local indices READ BEFORE WRITTEN in LINEAR op
order, so a parameter written on ONE arm of an `if` is demoted to a non-param
local and its incoming argument value is forgotten. Because its first access
is a write, the #457 read-before-write zero-init skips it too — the
fall-through path reads an UNINITIALISED frame slot.

`cond_write_param_970.wat` carries eight `cw_*` shapes whose HIGHEST referenced
local index is written before it is read (if / tee / br_if / loop / call
result / 3-param / 6-param), plus five `guard_*` shapes the fix must NOT change
(the #457 zero-init local, both-arms writes, unconditional write, plain params).

Two DISTINCT poison words make the mechanism provable rather than inferred:
every stack word below the entry SP is 0xDEADBEEF, every unused argument
register is 0xFEEDFACE. Both harnesses resolve their own in-module call
relocations in-process (R_ARM_THM_CALL / R_RISCV_CALL) so no external linker is
needed, and read symbols from the ELF .symtab, never `synth disasm` text.

MEASURED RED on cb80e60, both backends 22/38 with 12 memory-poison leaks:

  BUG cond_write_param(0x0, 0x2a): want=0x0000002a got=0xdeadbeef  <- POISON
  ok  cond_write_param(0x1, 0x2a): want=0x00000005 got=0x00000005

ARM's symptom is NOT what #970 predicted, and this is why it had to be
executed rather than read off a listing: #970 expected `cw_call(0, 42)` to
return param 0's value, reading the demoted local's `str` as sitting at the
branch merge point. It does not — `beq` jumps PAST it (capstone-verified), so
ARM has the SAME uninitialised-slot leak as RV32, on the plain shape too.

Floors are the MEASURED emulation counts (38 each, via scripts/oracle_run.py),
not derived from the case-list length.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…M + RV32)

With a declared param count in hand, every backend's bound is now
`min(referenced_locals(ops), declared)` — the highest local index the body
touches, clamped by the signature — not the READ-FIRST `count_params`
heuristic capped by it.

The old rule was exact in only one direction. The clamp stops a
read-before-write NON-PARAM local from being homed in an argument register
(#457), but taking the max over READS ONLY demoted a PARAM written on one arm
of an `if`: in linear op order its first access is a write. The demoted local
then also missed the #457 zero-init (which only covers read-before-write
locals), so the arm that does NOT write it read an UNINITIALISED frame slot.

Measured under unicorn with the sub-SP stack poisoned, both backends leaked
previous-frame bytes rather than returning the incoming argument:

  ARM  cond_write_param(0, 0x2a): want=0x2a got=0xdeadbeef   22/38 -> 38/38
  RV32 cond_write_param(0, 0x2a): want=0x2a got=0xdeadbeef   22/38 -> 38/38

`min` (not a plain `declared` override) preserves the leniency for a body that
only touches the first few of many declared params.

`referenced_locals` moves to `synth_core::wasm_op`, next to
`rewrite_memory_grow_zero` and for the same reason: #851 landed a private copy
in the aarch64 backend, and shipping two more would make three copies of one
three-line rule that must agree. The aarch64 copy is deleted in favour of the
shared one, so all three backends now share one definition.

ARM also grows an `effective_num_params` helper mirroring the RV32 one, so the
rule is unit-testable rather than inline; `has_rbw_local` is restated as
`inferred > declared` directly instead of relying on the (unchanged) algebra
`num_params < inferred_params`.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
A new job runs the ARM Thumb-2 and RV32 differentials and closes with the
#910 evidence ledger at `--min-oracles 2`, so deleting or skipping either step
leaves the ledger short and reds the job rather than quietly shrinking what CI
asserts.

Step names are QUOTED — an unquoted GitHub Actions step name containing " #" is
truncated by YAML at the comment marker, which is why 14 other steps in this
file display as a bare "Run" in the Actions UI (#851 noted the same).

The summed `--min-emulation-floor` is deliberately NOT ratcheted here: it is a
FLOOR (direction up), the two new oracles raise the measured total from 295,773
to 295,849 against a pinned minimum of 295,726, and with several v0.57 lanes
adding oracles in parallel a single shared total is a fan-in conflict. Ratchet
it once at release assembly, together with the ORACLE_WIRING.md table (already
at a stale 295,621) and both claims.yaml text pins.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ced_locals

`referenced_locals` is now a `use` alias of the `synth_core` item, so the two
`[\`referenced_locals\`]` links in this file resolved to the import rather than
to a local definition. `count_params` itself is still live — it is the `None`
arm of the param-count match, the documented honest residual.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@codecov

codecov Bot commented Aug 14, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit df8c626 into main Aug 14, 2026
109 of 110 checks passed
@avrabe
avrabe deleted the fix/count-params-arm-rv32-970 branch August 14, 2026 15:59
avrabe added a commit that referenced this pull request Aug 14, 2026
…e 4 shipped (#979)

Two things. The re-grades are bookkeeping; the back-fill is a finding.

RE-GRADED to `implemented` (work merged on main):
  RQ-57-COUNTPARAMS  #970  (#974)   ARM+RV32 conditional-param miscompile
  RQ-57-GPIO         #846  (#976)   gpio-thin 502 -> 494 B
  RQ-57-ARMSEM       #923  (#975)   ArmSemantics no-oped 87 of 222 ops
  RQ-57-MCDC         #912  (#978)   MC/DC over synth's own decision logic

RQ-57-BACKFILL: the back-fill was NOT performed, on evidence.

263 of 288 artifacts carry no `release:`. The prescribed derivation — "the
first tag containing the artifact" — RUNS FINE (0 undecidable, 24 distinct
tags) and answers the WRONG QUESTION. It yields when an artifact ENTERED THE
PLAN; `release:` means the release the work is TARGETED AT or SHIPPED IN.

The file supplied its own control case, which is what settles it:

  VCR-RA-001, hand-set          release: v0.24.0   <- when the work shipped
  VCR-RA-001, mechanical rule   v0.11.30           <- introducing commit's tag

It is the ONLY artifact in verified-codegen-roadmap.yaml that already carried a
`release:`, and the rule contradicts it. Sweeping the other 32 would have
written 32 false values with the one correct value sitting beside them as the
disproof.

Scale, had it been applied blindly: 190 of the 263 resolve to v0.1.1 — the
initial import, i.e. the standing requirement base (architecture, stakeholder
and system requirements, component model, target platforms). Tagging those
v0.1.1 asserts the whole foundational base was targeted at the first tag, and
makes "what is in v0.1.1?" return 190 artifacts including work that shipped
forty releases later. That is the corruption of the readiness query this
artifact exists to prevent — so the artifact's own guardrail ("stays
unassigned rather than guessed", the #911 lesson applied to planning data)
decides it.

CONVENTION, now documented in docs/release-process.md so the absence stops
being re-filed as an unfinished chore:
  * per-release plan artifacts carry `release:` (they are work items; they do)
  * standing artifacts carry it ONLY where the shipping release is known, as
    VCR-RA-001 does
  * setting it on a standing artifact is a per-artifact judgement with
    CHANGELOG evidence, never a sweep

A missing `release:` is a justified state. A wrong one is worse than a missing
one.

rivet: 50 errors / 166 warnings before AND after — unchanged. claim_check 43/43.

Refs #912


Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Aug 14, 2026
* chore(release): v0.57.0 assembly — "the checkers were the defects"

Nine artifacts. In five of them the bug was in the machinery that checks the
compiled code, not in the compiled code:

  #975  ArmSemantics silently no-oped 87 of 222 ops — a Rocq-proved,
        default-on rotl rule was "validated" by a model that executed neither
        of its instructions
  #976  the gpio differential CANNOT discriminate the miscompile it guards —
        complementary conditions, so no input to that driver can
  #969  writes_sp claimed exhaustiveness over a wildcard absorbing 175 of 222
  #967  the "9 unattributed branches" were manufactured by witness's own
        hardcoded divergence text
  #979  the prescribed release: back-fill would have written 32 false entries,
        with the one correct pre-existing value beside them as the disproof

The unifying property is that each of those checks COULD NOT FAIL. This
release makes them able to fail and proves it by making them fail on purpose.

Also fixed, and the most severe item: #974 — a conditionally-written parameter
was demoted to a zero-init local on ARM and RISC-V. Exit 0, no decline, wrong
code; on RISC-V it reads an UNINITIALISED stack slot (0xDEADBEEF under a
poisoned stack), an information-disclosure shape. ARM behaves identically —
which the issue predicted otherwise, and only execution settled.

Release surfaces, all four swept and checker-confirmed at 0.57.0:
  Cargo.toml [workspace.package] + 10 path-dep pins
  MODULE.bazel, npm/package.json, Cargo.lock (cargo metadata)
  scripts/check_version_pins.py: OK

Derived artifacts regenerated (--emit-status): artifacts/status.json,
docs/status/FEATURE_MATRIX.md. Claim gate: 43/43.

Open by design, named not hidden: #973 (ARM select miscompile, found only
because a lane compiled ARM fixtures — which CI never does), #977 (ELF-magic
flake, second sighting), #938 (breaking object 0.x-minor bump, auto-merge
disabled), #912 (open with four remaining: items).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* fix(release): act on the v0.57.0 cold review — 8 accuracy defects, 4 of them mine

Cold review of the assembled release. Nothing blocked the tag; everything below
is accuracy. Four of the eight were errors in the CHANGELOG I had just written,
which is the reason the review exists.

THE GENERALIZABLE FINDING, and it is pointed given this release's theme:
`check_generated_fresh` byte-compares the RENDERED FEATURE_MATRIX against the
TEMPLATE. `render_feature_matrix` only substitutes `{{...}}` fields, so the gate
proves the render is faithful to the template — and NEVER that the template is
faithful to the code. Every stale number below lives in template prose no
substitution touches. In a release titled "the checkers were the defects", that
is the checker that cannot fail. Three independent stale numbers survived a
green 43/43.

USER-FACING FALSE, verified by compiling rather than by reading:
  FEATURE_MATRIX listed "writing a PARAM local in a LEAF function" as a LOUD
  DECLINE on aarch64. #971 shipped exactly that. A leaf `local.set` on a param
  compiles: 32 bytes of machine code, exit 0. Also corrected in the same row:
  homing is no longer non-leaf-only, and the float-param decline widened with
  it. Fixed in the TEMPLATE (the render is generated) + regen.

MY CHANGELOG ERRORS:
  * "145 of the 175 pre-declined / 30 reachable" matched no partition. The
    shipped source (wcet_loops.rs:1232) says 142 give up with `true`, leaving
    33. Re-derived: 142/33. Corrected.
  * "demoted to a zero-initialised local" is wrong for the two backends the
    entry is about — zero-init is gated on first-access-being-a-READ, and in
    the cond-write shape the first access IS the write, so nothing initialises
    the slot. That is WHY it reads poison; the old wording made an
    information-disclosure bug sound like a benign wrong value, and contradicted
    the entry's own next sentence.
  * "Nine artifacts" — there are ten, and RQ-57-DOCSWEEP (#946/#968) had NO
    CHANGELOG entry at all despite touching CLAUDE.md, coq/STATUS.md,
    PROJECT_STATUS.md, the matrix template and eight source files. Added.
  * "Five in-tree oracles took that opt-in" — eight scripts plus three Rust
    tests. All eight carry floors, but `i64_param_518_riscv_loudskip`'s is
    `compiles >= 1`, which is a floor and NOT the "tight" one the paragraph
    claimed for the set. Named rather than folded into the claim.

STALE COUNTS (the template-prose class above):
  ORACLE_WIRING.md, the matrix template and claims.yaml all said "137 oracles /
  295,621 emulator entries". Re-derived independently — and the reviewer's
  number and mine agree exactly: 144 oracles / 296,059. Both `count-min` pins
  moved 137 -> 144 with them (same `emulations >=` pattern, two sibling claims);
  the pinned verbatim texts moved too, or the ledger would have gone red
  against its own corrected doc.

REVERSE STALENESS (a doc calling SHIPPED work missing):
  `synth verify` declines shift rules citing "SMT modeling of the variable-shift
  register encoding is an open gap". #975 CLOSED that gap — it modelled
  LslReg/LsrReg/AsrReg/RorReg as Rm<7:0> (ARMv7-M A7.7.68/70/12/117) and moved
  five lowerings Invalid -> Verified. Both comments corrected to say what is
  true: the modelling gap is closed, the remaining decline is a WIRING residual.
  Behaviour deliberately unchanged — rewiring the rule table is a
  verification-surface change, not release assembly. Filed as #981.

ARTIFACT:
  RQ-57-PROVGAP still asserted "9 object branches with no WASM origin" as fact
  while its own PR disproved it. Outcome recorded, as RQ-57-BACKFILL already did.

  docs/architecture/CRATE_STRUCTURE.md said 18 crates; there are 19. A
  RECURRENCE — PROJECT_STATUS.md cites this exact drift as why it was gutted in
  the #946 sweep, and one file over it was live again.

Gates after: claim_check 43/43, check_version_pins OK at 0.57.0,
cargo check -p synth-cli rc=0.

Refs #980, #981

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* style: rustfmt the #975 decline-reason comment (indent 14 -> 12)

My own miss: I ran cargo check on the edited file but not cargo fmt, and
Format is a required context. The comment content is unchanged — only the
indentation rustfmt wanted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

count_params silently demotes a CONDITIONALLY-written parameter to a zero-init local — ARM + RISC-V miscompile (aarch64 instance fixed in #851)

1 participant