RQ-59-STARTFN (#1046): the (start ...) section was silently discarded by ALL THREE backends — decode it and refuse loudly; fourth silent drop (globals inits, #1052) found and filed

[avrabe]

A FOURTH silent drop was found and FILED first — it outranks this fix

#1052 — the ARM plain-relocatable path silently drops nonzero GLOBAL INITIALIZERS, and it is OUTSIDE the documented embedder contract (verdict + executed repro below). Filed with the repro executed on the v0.59 tree per the RQ-59-DATASEG lane's open-observation handoff. The element-segment sibling observation resolves the other way: inside the contract, language quoted below.

---

Closes the third silent drop of the session: all three backends discarded the (start ...) section — the decoder had no Payload::StartSection arm at all, so the section fell through the catch-all. #1041 (data segments), #1046 (this), #1048 (i64-shift operand): synth accepted input, discarded part of its semantics, and reported success.

Start-function INVOCATION is deliberately NOT this artifact — it is a capability question (the self-contained Reset_Handler could call it before any export; the relocatable contract would need an exported init hook). This PR is the honest-frontier minimum: refuse loudly, the #851/#1049 house shape.

Rivet: RQ-59-STARTFN — the artifact entry lives on PR #1050 (plan/v59-i64shift-startfn), not yet on main; this branch is off main and does not duplicate it.

Red-first transcript

Before (main, 18a4786) — the filed repro ((start $init) writes 42 to memory 0; wasmtime get() == 42):

$ synth compile start_repro.wat --all-exports --relocatable --target cortex-m4 -o start_arm.o
INFO Found 1 exported functions: 'get' (index 1)      # $init never compiled
INFO Generated 431 byte ELF file
ARM exit=0                                            # no warning, no mention of start
# same on -b riscv -t rv32imac (exit 0) and -b aarch64 (exit 0)

After (this branch):

$ synth compile start_repro.wat --all-exports --relocatable --target cortex-m4 -o start_arm.o
Error: module declares a start function (function index 0), but no synth backend invokes it —
the (start ...) section's instantiation-time initialization (WASM Core §4.5.5: it runs before
any export is callable) would silently never run, and every export would read state the start
function was supposed to establish; refusing (#1046). Start-function invocation is a documented
capability follow-on; until it lands, remove the (start ...) section and perform the
initialization through an export your embedder calls first.
ARM exit=1

Same refusal on ARM self-contained, cortex-r5 (A32), RISC-V, AArch64, the single-function path, and the WAST merge path.

The assertion shape is the point (commit 1, red on its parent): the test asserts a non-zero exit + a reason string naming the start section — it deliberately does NOT assert "the start function was not called", which was already true on the broken behaviour and would have been vacuously green. All 7 refusal tests failed on main; the start-free control passed throughout; all 8 pass now.

No escape hatch — deliberately unlike #1049's --embedder-data-init: the start function's CODE is not in the artifact (reachability walks exports only), so there is nothing an embedder could call. A (start) naming an exported function still refuses (nothing invokes it at instantiation; test pins this).

Verdict on the two open RQ-59-DATASEG observations

1. Nonzero global initializers on the plain relocatable path — OUTSIDE the contract. Fourth silent drop. Filed as #1052.

Executed repro: (global $g (mut i32) (i32.const 42)) + global.get export, --relocatable --target cortex-m4 → exit 0, and the whole object is push {r4,lr}; ldr.w r0,[r9]; pop {r4,pc} — 0x2A appears nowhere in the ELF, no .data, no __synth_globals. wasmtime: 42.

What the contract actually documents is the BASE, not the values: the selector says "R9 = globals base"; the only relocatable-path globals harness (i64_globals_643_differential.py) maps "a zeroed scratch region" and annotates it "# zeroed globals table (inits are 0)" — correct only because that fixture's inits ARE zero. There is no sentence anywhere assigning initializer evaluation to the embedder — contrast the data-segment sentence that exists ("the embedder populates its init segments", multi_segment_static_data_differential.py). Every other path handles inits explicitly: ARM self-contained materializes them at reset (#649 — which treated exactly this class as a BUG), --native-pointer-abi ships them as .data, aarch64 ships __synth_globals ("explicitly NOT preconditions: synth EMITS both" — FEATURE_MATRIX), RV32 loud-skips. The plain relocatable path alone neither ships, nor declines, nor documents.

2. Active element-segment table images — INSIDE the contract. call_indirect_594_differential.py: "ArmOp::CallIndirect contract (same as the Thumb-2 path): R11 holds the function-pointer table base; entry i is a 4-byte code address. The harness builds that table with func_0's address"; encoder: "Table base setup must be done by caller/runtime." The table entries are final linked code addresses that cannot exist in an ET_REL object as runtime-RAM contents; the object exports every func_N the segments name (verified on the executed elem repro: func_0, func_1, pick all in the symtab), and the embedder holds the module's segment layout. Building the table is the integrator's documented step. (One-line residual noted in #1052: the #676 type-id sidecar's structural-class-id derivation rule is documented only in wasm_decoder.rs doc comments.)

Decoder section class sweep (decode_wasm_module)

Section	Status	Loud?
Type / Import / Function / Table / Memory / Global / Export / Element / Data (active) / Code	handled	n/a
Start	was DISCARDED SILENTLY — the #1046 defect	now recorded + refused (this PR)
Data, active non-const offset	recorded reason	refused: aarch64 #851; ARM relocatable via PR #1049
Data, passive	no record kept	op-guarded: memory.init/data.drop hit convert_operator → None → per-function LOUD-SKIP with the op named (#369 lane) — semantics unreachable without the ops
Element, passive/declared/non-const	recorded as statically-unverifiable	call_indirect guard declines; targets still enter reachability
Tag (exception handling)	no arm, silently ignored	op-guarded: throw/try/... loud-skip per function via the same #369 lane — a tag with no using op is inert
DataCount	no arm	safe: pure validation metadata (count only), zero runtime semantics
Custom (non-name, non-wsc.facts)	ignored	safe by spec: custom sections are non-semantic
Version / CodeSectionStart / End	structural	n/a
Component-model payloads (ModuleSection, ComponentStartSection, ...)	no arms	probed: a (component) binary ERRORS ("No exported functions found in module") — not silent, but the diagnostic is misleading; components route through synth-frontend. Residual, not a drop

The defect class was specifically: a section whose semantics are reachable with NO operator involvement (start, active data, global inits) — those are invisible to the #369 op-level loud-skip lane and need section-level handling. Start was the last unhandled one in this decoder; global inits (#1052) are its sibling one layer up (decoded but never emitted on one path).

Harness impact

0 harnesses/fixtures affected. Swept three ways: grep -E '\(start[[:space:]]+[$0-9]' over all .wat/.wast/.rs/.py (only this PR's own test), a binary scan of all 21 in-repo .wasm files for section id 8 (none), and the full workspace suite (green). EXPECTED_DECLINES (#992) unchanged — it keys on scripts/repro/*.wat, none of which carry (start). No escape-hatch flag needed (and none would be honest — see above). Frozen anchors: emitted bytes for start-free modules are untouched (the guard only fires on Some); all frozen-fixture differentials in the suite pass. synth verify (analysis, no artifact) is deliberately not gated, matching #1041's compile-only scope.

Gates

• cargo fmt --all clean; cargo clippy --workspace --all-targets -- -D warnings green
• cargo test --workspace TRUE exit 0 (147 suites ok, 0 failures)
• python3 scripts/claim_check.py claims.yaml 50/50; python3 scripts/model_coverage_audit.py --check ok (separate runs)
• 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 baseline)
• Commits signed

Refs #1046. Fourth-drop filing: #1052.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!