[avrabe]

Gives a --relocatable embedder the one number the object has never carried: how much native stack a call into an export can consume.

The failure this is about

cpetig's export returned an answer bit-identical to wasmtime, every time, and then corrupted an unrelated RTOS pointer. It overran its NuttX task stack while the linear-memory guard bands above and below stayed untouched. A --relocatable object tells the embedder how much linear memory to reserve and nothing at all about stack, so the region gets guessed — and guessing low fails silently, with a plausible result.

The reporter's proposed mechanism was unsound as stated

"If --emit-wcet already walks the call graph, the same traversal would yield the depth."

The traversal is right — memoized DFS, cycle detection, honest declines. The arithmetic is not. wcet_compose weights each callee by its proven execution count, so a callee invoked 1000× inside a loop would be charged 1000× the stack it uses. Stack depth is a MAX over the call tree, never a trip-weighted sum. And over-reporting isn't the safe direction: an embedder told 2 MB for a 2.3 KB requirement stops believing the number.

The decline set isn't reusable either. WcetDecline carries Loop, LoopedExpansion, UnmodeledOp, UnresolvedBranch — none affects stack depth, because a loop body reuses one frame every trip. A data-dependent loop is WCET-unbounded and perfectly stack-bounded. Riding on it would have refused a bound for most real modules, the reporter's control loop included. So this is a sibling pass sharing only the DFS shape.

Three ways to count, measured on a committed fixture

stack_depth_branch_1341.wat — top calls a and b; both call leaf:

method	bytes	vs truth
(a) the reporter's sum(sub sp)	96	under by 24 (20%) — the dangerous direction
(b) naive sum of every frame	176	over by 46%
(c) truth: max over root-to-leaf paths	120	—

(a) misses three things. The prologue moves SP in up to three steps — push.w {r4-r8,lr} (24 B, always), vpush {d8-d15} (64 B, conditional), sub sp — and sub sp is emitted only when frame_size > 0, so leaf consumes 8 B while being invisible to that grep. The immediate is also hex: #0x20 is 32, and a #[0-9]+ regex reads it as 0. That one isn't hypothetical — the first measuring command written for this lane had exactly that bug and printed "sum: 0".

The figure depends on the link mode, and that's legitimate

The oracle's first version asserted --relocatable and self-contained builds report the same number. They don't: 8/64/64/120 vs 16/72/72/128 on one fixture. --relocatable forces the direct selector (#197); the optimized prologue costs 8 more bytes per frame. The number belongs to the build you ship, so the oracle now asserts the two paths agree on which functions are boundable and lets the figures differ.

Evidence — and the oracle found two of its author's errors

• scripts/repro/stack_depth_1341.py, CI-wired, 6 emulations, proven red-first against the pre-feature binary (rc=1, "unexpected argument --emit-stack-depth").
• Both bounded fixtures: reported 128 B vs measured peak 128 B — slack zero. The bound isn't merely sound, it's exact.
• call_indirect was declining with the wrong reason. It reaches the stream as ldr rN,[pc,#..] + blx rN, not a CallIndirect pseudo-op, so the catch-all called it unknown-sp-move — safe, and wrong: that tells an embedder the walker got confused rather than that their call graph is unresolvable.
• The oracle also demanded too much: it required that nothing in an unboundable module be bounded, when that module's leaves are perfectly boundable and only the export matters. Both corrections are written into the script, not quietly applied.
• 7 synth-backend unit tests, including composition_takes_the_max_over_branches_not_the_sum — the one that catches a regression to the WCET composer's arithmetic.

What is NOT claimed

#1341 asked for two things and this ships one. The depth is reported (sidecar + compile line); it is not recorded in the object as an ELF note, so a build step must read a file beside the .o rather than the .o itself. That's weaker than asked, and it's stated as the follow-up it is. The documentation half was already met before this work — docs/embedder-abi-relocatable-arm.md already said the embedder owns stack placement and size; what was missing was a number.

The reporter's own module is an issue attachment, so their 1984/4032 B bracketing stays [REPORTER-ONLY] and is not restated as re-derived.

Housekeeping done deliberately

• Mutant ledger re-anchored proactively (the v0.70 lesson, applied instead of rediscovered): this diff inserts lines in arm_backend.rs above five pinned sites. reanchor moved 14 sites by exactly +8, 0 not found, mutants/controls/ci_subset/UNTESTED all unchanged — re-located, never re-baselined.
• The unicorn job's --min-oracles floor moves 6 → 7. It now runs 7 oracles; leaving the floor would let this one be deleted silently — the RQ-70-WINDOWVAC class.

Verification

cargo fmt --check rc=0, clippy --workspace --all-targets -D warnings rc=0, cargo test --workspace 168 suites / 0 failures; claim_check 75/75, status_evidence / check_version_pins / oracle_wiring / artifact_citation all rc=0.

Refs #1341

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 73.68421% with 80 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-core/src/stack_depth.rs	0.00%	38 Missing ⚠️
crates/synth-cli/src/main.rs	29.16%	34 Missing ⚠️
crates/synth-backend/src/stack_depth.rs	96.07%	8 Missing ⚠️

📢 Thoughts on this report? Let us know!