fix(#944): verified machine-readable origins for compiler-introduced object branches — the 9 were never unattributed, the real 33 now are attributed

[avrabe]

#944 — the 9 "object branches with no WASM origin": triage, attribution, gate

The premise was false — in a good way

Reproducing the count from the committed evidence (pulseengine/gale benches/gust/drivers/mcdc/evidence/switch-thin.{witness,provenance}.json, joined exactly as witness object-disposition does, on (func_index, instruction_offset)) gives exactly the 9 keys from the issue — and every one of them is a provenance entry for a real source WASM op, not an object branch without origin:

#	func	off	function	source op	kind in map	object realization
1	6	740	wit_bindgen::rt::cabi_realloc	br	preserved	unconditional B @ 0x4e
2	12	929	…fsm::Guest>::tick	br	preserved	unconditional B @ 0xea
3	16	1251	…fsm::Guest>::run_switch	br	preserved	unconditional B @ 0xdc
4	16	1292	…fsm::Guest>::run_switch	select	folded-predication	predicated IT-move @ 0x11c — no branch at all
5	16	1357	…fsm::Guest>::run_switch	br	preserved	unconditional B @ 0x18c
6	23	1842	…fsm::Guest>::mark_resumed	select	folded-predication	predicated IT-move @ 0x12e
7	24	1960	_export_mark_swapped_cabi wrapper	br	preserved	unconditional B @ 0xe0
8	25	2145	…fsm::Guest>::current_window	select	folded-predication	predicated IT-move @ 0x13e
9	28	2166	(function with no instrumentable branch)	br	preserved	unconditional B @ 0x2

Category verdict: none of the 9 is a miscompile, and none is even an unattributed compiler-introduced branch. They are 6 unconditional brs and 3 selects folded to predication — source ops synth's map records faithfully, which witness never instruments (its manifest carries only br_if / br_table_target / br_table_default / if_then / if_else). only_in_synth in witness's reconciler means "synth entry with no witness branch record"; its hardcoded divergence text — "(object branch witness never instrumented)" — is what turned "uninstrumented br/select" into "object branch with no source", and the issue's framing followed from that message. The 9→8→4 movement across the source variants in the follow-up comment tracks which br/select source ops survive each source-level simplification — consistent, and the "irreducible 4" are the br/select ops in cabi_realloc and the export wrappers. Witness-side classification (filter/label only_in_synth by the op field synth already emits) is witness#109 territory.

The REAL unattributed population — and its attribution

The genuinely compiler-introduced conditional branches on switch-thin are the 33 resolved: false entries in object_cond_branches (invisible to witness's join, surfaced only with a free-text guessing note). All 33 trace, via the encode-time line_map, to memory.fill / memory.copy lowerings. Reproduced and disassembly-verified on current main (ELF bytes via pyelftools+capstone, never synth disasm text), per introducing op:

introducing op	branches	verified shape	verdict
memory.fill	1	loop bound test (cmp; bhs, zero-trip safe)	(a) serves fill count semantics
memory.copy	3	overlap-direction test (cmp dst,src; bhi) + forward and backward copy-loop bound tests	(a) serves memmove overlap semantics
i32.div_s	3	div-by-zero guard + INT_MIN/-1 overflow guard pair, each skipping a udf	(a) WASM trap semantics
i32.div_u / i32.rem_s / i32.rem_u	1 each	div-by-zero guard	(a) WASM trap semantics
if	1	the decision's own conditional branch	not introduced at all — a source decision v1 mis-bucketed

Probed-and-clean on the same path (no cond branches emitted): call_indirect, memory.grow, i64 div/rem (software), i64 shifts/clz/eqz/compares. No category (b) — no branch that should not exist — was found anywhere in this lane.

What this PR changes

• crates/synth-core/src/provenance.rs
  • ObjectCondBranch gains an additive origin field (absent when None; witness's serde ignores unknown fields, wire format stays synth-provenance-v1): a kebab-case machine-readable origin derived from the op the branch's line_map entry traces to — never guessed. Closed, disassembly-verified vocabulary: bulk-memory-fill-loop, bulk-memory-copy-loop, division-trap-guard.
  • An introduced branch whose op family is NOT in the verified map stays origin: None with the op named in the note — unexplained-but-declared beats a confident wrong label (the issue's own follow-up demonstrated the plausible label being wrong).
  • if is now a covered source decision ("If" preserved entry; its conditional branch resolves). Bonus for the witness join: witness does instrument if_then/if_else, so covered if entries can now match instead of falling into no-provenance.
• scripts/repro/provenance_introduced_944.wat + crates/synth-cli/tests/provenance_introduced_origin_944.rs — the gate:
  • unattributed floor = 0 on the fixture: every object conditional branch either resolves to a source decision or carries a named origin;
  • no excuse-widening: exact per-origin counts pinned (1 fill + 3 copy + 3/1/1/1 division) and a closed origin vocabulary — reaching 0 by blanket-labeling turns it red;
  • mutation-verified red-first: unmapping MemoryCopy → 3 UNATTRIBUTED panics; blanket-labeling (_ => Some("division-trap-guard")) trips the synth-core negative-control unit test.

No CHANGELOG/version/status.json changes (release-hub constraint). No doc-claim changes; claim_check stays 43/43.

Closes #944.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

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

Files with missing lines	Patch %	Lines
crates/synth-core/src/provenance.rs	98.94%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!