RQ-59-GLOBALINIT (#1052): ARM relocatable path REFUSES global initializers it does not materialize — the fourth silent drop, plus teeth for the harness that was green over it

[avrabe]

Closes the fourth silent drop of the #1041 class: the ARM plain --relocatable path silently discarded nonzero global initializers — compiled exit 0, 0x2A nowhere in the ELF, wrong value at runtime. The fix is the house refusal (#851 / #1049 / #1053 shape). Materializing the initializers on this path is capability work (v0.60, alongside VCR-REACH-002) and is explicitly NOT this artifact — this PR is the honest-frontier minimum plus the harness that should have caught it.

Rivet: RQ-59-GLOBALINIT (artifact entry on PR #1056, plan/v59-globalinit; this branch is off main and does not duplicate it).

Red-first transcript

Before (origin/main) — the filed repro, executed:

$ synth compile globals_repro.wat --all-exports --relocatable --target cortex-m4 -o glob_arm.o
INFO Generated 431 byte ELF file
exit=0                                 # no warning, no mention of the initializer
$ objdump -s glob_arm.o
Contents of section .text:
 0000 10b5d9f8 000010bd            # push {r4,lr}; ldr.w r0,[r9]; pop {r4,pc}
# 0x2A appears NOWHERE in the ELF — no .data, no __synth_globals

wasmtime: get() == 42. The object returns whatever the embedder left at R9.

After (this branch):

$ synth compile globals_repro.wat --all-exports --relocatable --target cortex-m4 -o glob_arm.o
Error: module declares 1 global initializer(s) whose value(s) do not reach the emitted
object (global 0 = (i32.const 42)) — the ARM relocatable path does not materialize
global initializers (the R9 globals table is embedder-mapped, and the documented
contract assigns only the table BASE to the embedder, never initializer evaluation),
so every global.get would silently read whatever the embedder's memory happens to
hold; refusing (#1052). Compile self-contained (drop --relocatable; the Cortex-M
image materializes global initializers at reset, #649), use --native-pointer-abi
with a linear memory (the __synth_globals region ships the init values as .data,
#237), or pass --embedder-global-init to declare that your embedder evaluates the
module's global initializers and seeds the R9 table before any export runs.
Shipping the initializer image on this path is a documented capability follow-on (v0.60).
exit=1

The assertion shape is the point (commit 1, red on its parent): the tests assert a non-zero exit + a reason string naming the global initializers. They deliberately do NOT assert "the initializer value is absent from the object" — that was already true on the broken behaviour and would have been vacuously green, which is exactly how this bug survived. 6 refusal tests red on main (nonzero i32, nonzero i64, non-const init expr, cortex-m4 + cortex-r5, import-forced ET_REL, --native-pointer-abi without memory); 4 green controls passed throughout; all 11 pass now.

The contract language, re-verified (not inherited from the finding lane)

• crates/synth-synthesis/src/instruction_selector/select_with_stack.rs:5545: "Load global value from globals table (R9 = globals base)." — the BASE register, nothing more. Same at :5629 and in contracts.rs ("R9: globals base pointer").
• scripts/repro/multi_segment_static_data_differential.py:20: "and the embedder populates its init segments (the object carries no ROM image on this path)" — the data-segment sentence that made ARM --relocatable SILENTLY DROPS active data segments — exit 0, no bytes, no warning (explains gale#278 state(0)=255) #1041 a refusal-with-flag exists for data segments only. A repo-wide grep for any sentence assigning global-initializer evaluation to the embedder finds none.
• README:119: "R9-based globals" — mechanism, not init ownership.

So: outside the contract, confirmed. Every other path ships the inits (--native-pointer-abi #237, aarch64 #851), materializes them at reset (self-contained — #649 fixed exactly this class there as a BUG), or loud-skips (RV32 #643). The plain relocatable path alone did none of the three.

The guard

Predicate is "does the initial VALUE reach the object", not "which flag was passed" (in build_relocatable_elf, after emit_wasm_data is known):

• nonzero i32.const / i64.const init on the plain (R9-table) path → refuse;
• non-const integer init expr (e.g. global.get of an imported global) → refuse on every ET_REL path — no path materializes an unknown value (the native .data slot would ship a silent 0);
• --native-pointer-abi without a linear memory, when code carries a __synth_globals relocation → refuse: no region is emitted, so pre-fix the object shipped an undefined __synth_globals and no init image (loud at host link by default, so not filed as a fifth silent drop — but the same guard closes it at compile time). With NO such relocation the declared global is inert (no globals surface in the object) and the compile is allowed;
• all-zero const inits → never refuse (a zeroed embedder table IS their correct initial state — the thumb-2: i64 global.set/global.get truncate to 32 bits (high word silently dropped) #643 fixture and every zeroed-scratch harness stay green);
• float/v128 globals → untouched, they remain the GI-FPU-001 (arm backend uses soft-float for all f32/f64 — hardware FPU never used (cortex-m4f/m7/m7dp identical); blocks REQ-PIX-001 hard-float #369)/thumb-2: SIMD (v128) ops silently dropped to no-ops on cortex-m3 (no SIMD hw) — wrong result / unwritten memory instead of honest rejection (#554 class) #680 loud-skip lane (their access never emits, so a dropped init is unobservable through generated code). A new WasmGlobal::float_or_v128 field lets the guard tell integer-None (silent-drop class) from float-None (covered lane) — slot_bytes alone cannot (4 = i32 OR f32).

--embedder-global-init is the explicit escape hatch (the #952/#1049 shape). Bytes identical either way, pinned by test: the flagged nonzero-init object is asserted byte-identical to a zero-init twin's unflagged object — the init value reaches no emitted byte, which is precisely the contract the flag acknowledges. Frozen anchors: unmoved (refusal only; full frozen_codegen_bytes suite green).

The strengthened harness, and proof it has teeth

Why the bug survived: the sole relocatable-path globals harness (i64_globals_643_differential.py) maps a zeroed region annotated # zeroed globals table (inits are 0), and its fixture's inits ARE 0 — it structurally could not distinguish "initializers written" from "initializers were all zero anyway". Same weak-checker family as #1055 ("before FIRST read") and #1054 ("may clobber it freely").

Strengthened (check_nonzero_init_contract_1052, new fixture globals_init_1052.wat with inits 42 and 0x1122334455667788), three legs:

1. refusal — plain --relocatable must exit non-zero naming the global initializers;
2. contract — with --embedder-global-init the harness acts as the acknowledged embedder: it seeds the R9 table from the module's own initial values, read back through wasmtime's exported globals (the VCR-VER-003 served-vs-runtime shape — no second hardcoded copy), then the execution differential must agree with wasmtime;
3. non-vacuity — the SAME object on a zeroed table must diverge from wasmtime; if it ever stops diverging, the fixture has gone vacuous and the harness fails itself.

Teeth proven by execution against the pre-fix compiler (origin/main sources, rebuilt):

=== #1052 nonzero-initializer contract (plain --relocatable) ===
  [BUG] refusal: exit=0 reason missing/unnamed (SILENT-DROP: compiled exit 0)
  [BUG] --embedder-global-init compile failed: For more information, try '--help'.
ORACLE: FAIL (2 divergences)

Against the fixed compiler: all legs pass (seeded get_a=0x2a, get_b_lo=0x55667788, get_b_hi=0x11223344; zeroed-table get_a -> 0x0 DIVERGES). The original #643 sections and its ci-checks: emulations >= 28 floor are untouched (the new legs only add emulations).

Affected-harness count (measured, not assumed — and re-measured)

First measurement said "2 tests in 1 file" and was wrong: cargo test stops at the first failing binary, so the first run's failure list was truncated. The honest number comes from --no-fail-fast plus executing every CI synth compile invocation extracted from ci.yml against the fixed binary. Measured fallout, all converted per the #1049 shape (default refuses; the flag acknowledges; bytes identical):

• 9 cargo test files (~28 tests): cabi_arena_bind_418, cmp_select_fusion_census, cmp_select_two_move_coverage, dwarf_debug_line_emit_394, flag_flip_wave_242, frozen_codegen_bytes, recovery_stats_242, shift_mask_elide_686, spill_baseline_pressure_390 — all compile frozen SP-global fixtures as harness-embedders and gain --embedder-global-init. frozen_codegen_bytes passing again with the flag IS the frozen-anchor proof: the bit-identical oracle is green, so no emitted byte moved.
• 2 python harnesses: arm_corpus_sweep_973.py (globs the whole corpus; ~25 nonzero-init fixtures; compile count restored to 150/162 over its 144 floor) and gpio_thin_846_differential.py (loom-emitted $__stack_pointer; its runner maps R9 itself). Each carries the same acknowledgment comment multi_segment_static_data got for ARM --relocatable SILENTLY DROPS active data segments — exit 0, no bytes, no warning (explains gale#278 state(0)=255) #1041.
• 3 CI compile steps in ci.yml (flight-seam ×2, control-step, call_6_7args) — verified by re-running all 37 unique CI compile invocations: 0 refusals, 0 other failures after.
• 1 test fixed by guard ORDER, not a flag: shadow_stack_size_without_region_refuses_739 expects the more specific --shadow-stack-size: static ABOVE sp_init is baked at its 1MB linmem offset, not re-based → OOB read in shrunk layout (post-link oracle wrongly passes) #739 flag-honesty message; the ARM plain-relocatable path silently drops nonzero GLOBAL INITIALIZERS — no init image, no decline, no documented embedder obligation (4th silent drop of the #1041 class) #1052 guard now runs after it.
• 1 over-refusal found and refined away: call_5args.wat-shape fixtures (--native-pointer-abi, no linear memory, globals declared but never accessed — no __synth_globals relocation, no region) are INERT: the object has no globals surface at all, so nothing can ever read the dropped value. The guard allows them; a module that DOES access globals with no region still refuses (pinned by test). On the plain path this refinement is impossible (R9 accesses carry no relocation) and presence-based refusal stands, matching ARM --relocatable SILENTLY DROPS active data segments — exit 0, no bytes, no warning (explains gale#278 state(0)=255) #1041.

(#1049 found ~30 affected, #1053 found 0 — this one measured ~30 across 9 test files + 2 harnesses + 3 CI steps.)

Gates

• cargo fmt --all clean; cargo clippy --workspace --all-targets -- -D warnings exit 0
• cargo test --workspace exit 0 (true exit code, unpiped)
• python3 scripts/claim_check.py claims.yaml: 50/50 hold; python3 scripts/model_coverage_audit.py --check: ok
• rivet validate: FAIL (50 errors) — identical count to main (rivet externals are declared against a volume that does not exist — the federated half of the trace graph is never validated #1012, pre-existing)
• Frozen anchors unmoved; EXPECTED_DECLINES (fix(#973): ARM select on an i64-comparison returns the then-arm — and an ARM leg for the corpus CI never compiled #992) untouched

Refs #1052

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 98.14815% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	98.00%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

[avrabe]

[coordinator] Holding this PR — it reddens VCR-DEC-001 graph-alloc spike differential (#242, thumb2), and the failure is real, not environmental.

All 9 required contexts are SUCCESS, so this would have merged under a count-based rule. It is held because the failing check is not on the advisory allowlist (only codecov* is).

Diagnosis

The failing job is titled trap-semantics oracle (#665 unreachable + #666 rem_s), but no trap oracle failed — the job name is just its title. 40 oracles pass, then:

step 41  FAILURE  Run VCR-DEC-001 graph-alloc spike differential (#242, thumb2)
step 45  FAILURE  Differential evidence ledger (#910)      <- downstream of 41

All four trap oracles reproduce GREEN locally on this branch, each at its non-vacuity floor exactly: 8/8, 8/8, 28/28, 49/49 emulations.

Baseline comparison — this is a regression, not pre-existing

Same script, same command, same host, main vs this branch:

MAIN    ORACLE-EVIDENCE ... mode=compiles floor=27 measured=27 compiles=27 exit=0
BRANCH  ORACLE-EVIDENCE ... mode=compiles floor=27 measured=27 compiles=27 exit=1

Both met the floor — the branch ran the work and the assertions failed.

What actually breaks

Six fixtures now refuse to compile, on this PR's own new refusal:

control_step.wasm      COMPILE FAIL: module declares 1 global initializer(s) whose
flight_seam.wasm       value(s) do not reach the emitted object (global 0 = (i32.const 655…
flight_seam_flat.wasm
gust_kernel.wasm
sret_decide.wasm
msgq_put_359.wasm

And the consequence is worse than six failures. The oracle's own output:

== diverging fixtures: 0 (must be ≥ 2 for increment-2 non-vacuity) ==
  VACUOUS: no fixture's bytes changed — the join colouring (increment 2)
  no longer reaches this corpus.

The refused fixtures were exactly the ones exercising the join colouring. So the refusal does not merely break compiles — it hollows out an unrelated allocator oracle, which then correctly refuses to pass rather than reporting a green vacuous run. That is the #910 non-vacuity design doing its job, and the reason this must not be merged and patched afterwards.

The refusal is right; the collision is what needs deciding

Nothing here argues against the refusal. Silently dropping (global (mut i32) (i32.const 65535)) is a miscompile, and #1052 is a real defect. The question is what these six fixtures should do now, and it is the same question #1049 already answered for data segments.

Options, in the order I'd rank them:

1. Escape hatch, matching the house style — the --embedder-data-init shape from RQ-59-DATASEG (#1041): ARM relocatable path REFUSES active data segments it does not materialize — silent drop becomes a loud decline #1049 (and A declined export exits 0 with the symbol simply absent — the decline is honest to stderr but invisible to the build system #952's --allow-skipped-exports): an explicit flag declaring the embedder populates globals, changing no emitted byte. The allocator differential passes it, keeps its fixtures, and keeps its teeth. This is the third use of a pattern already established twice.
2. Zero the fixtures' globals — cheapest, but verify the fixtures still exercise the join colouring afterwards. If they don't, this trades a red oracle for a vacuous one, which is strictly worse and is the failure mode this repo has found in five consecutive releases.
3. Update the oracle's expectations — only if 1 and 2 are both wrong; a differential that expects a compile failure has stopped being a differential.

Option 2 needs an explicit "still non-vacuous" demonstration, not an assertion.

Reproduce

python3 scripts/oracle_run.py scripts/repro/vcr_dec_001_graph_alloc_differential.py ./target/debug/synth

(Trap for anyone reproducing: do not redirect CARGO_TARGET_DIR — the scripts hardcode ./target/debug/synth. Symlink target at your scratch dir and mkdir -p it first, or every oracle "fails" with FileNotFoundError and measured=0. The non-vacuity floor is what makes that mistake visible.)

Everything else on this PR looks good — the refusal test and the extended i64_globals_643_differential both pass locally, and the latter carries its own teeth check (zeroed-table get_a -> 0x0 DIVERGES from wasmtime).