fix(#740): Thumb-2 B<cond>.W (T3) halved the branch offset — wide conditional branches landed mid-shape

[avrabe]

Closes #740. Part of the #242 Track-C validation lane (v0.43.0 hub, Lane E).

Root cause

The encoder, not the selector. The direct selector's label/branch resolution computes the halfword displacement correctly for the loop-inside-block shape; the bug was in the Thumb-2 encoder's 32-bit B<cond>.W (encoding T3) arm in crates/synth-backend/src/arm_encoder.rs, which packed halfword_offset >> 1 into imm6:imm11. Per ARMv7-M the branch byte offset is SignExtend(S:J2:J1:imm6:imm11:'0') — the 20-bit field S:J2:J1:imm6:imm11 is the signed halfword offset — so every conditional branch spanning > 254 bytes jumped to half its intended displacement.

On gust_poll (#740) the loop-head empty-budget br_if 1 (;@2;) was the only wide conditional in the function: it landed after the first transition call instead of at the block-@2 join, producing the spurious state+0x34 write plus spurious transition/mix calls on a round that must not touch memory. Narrow (16-bit) B<cond> encodings were unaffected — which is exactly why the short-range CF differentials (#483/#497/#500/#508/#509) never caught it, and why every other br_if @2 in gust_poll (all narrow) landed correctly.

Fix

Pack the halfword offset directly into S:J2:J1:imm6:imm11 (mirroring the correct T4 unconditional arm), and loud-decline offsets outside the signed 20-bit T3 range instead of emitting a truncated branch. Bytes cross-checked against the llvm disassembler (bne.w #0x224 = f040 8112).

Red → green

• New oracle scripts/repro/brif_outer_740_differential.py + brif_outer_740.wat: minimal loop-inside-block shape — loop-head br_if to the outer block end + a two-level br_if exit, padded past the 254-byte span so both encode wide; non-tail return keeps it on the DIRECT path (optimized declines, Optimized path: br_if to a forward block end still unresolved for if/else and sequential-block shapes (#483 class, broader) #500 — same path as gust_poll). Return value and a linear-memory window vs wasmtime, 6 cases. RED pre-fix (5/6 FAIL), GREEN with the fix (6/6). Anti-vacuous: hard-fails if poll ever stops containing a 32-bit T3 conditional branch. CI-wired into the emulation-differential job.
• xfail promotion: the anti-vacuous direct path: br_if exiting an outer block from inside a loop lands mid-shape — gust_poll empty-budget round mutates state it must never touch #740 xfail in gust_spill_fwd_390_differential.py fired (FIXD) the moment the divergence disappeared, as designed; the two zero-state rows are promoted to strict — return AND full state window match wasmtime in all three lever configs (default, SYNTH_NO_STACK_FWD=1, SYNTH_SPILL_REALLOC=0). Full harness PASS.
• Encoder unit test test_encode_thumb_bcond_wide_t3_halfword_offset_740: forward + backward wide offsets, narrow encoding byte-identical, out-of-range → loud Err.

Frozen status

Frozen anchors 10/10 bit-identical (frozen_codegen_bytes) — the fixtures contain no wide conditional branches, so no refreeze. All existing CF differentials green: block_brif_483, br_table_507, br_table_value_509, cf_shapes_500, control_step (13/13).

cargo fmt --check, cargo clippy --workspace --all-targets -- -D warnings, cargo test -p synth-cli -p synth-synthesis (61/61 targets) all green.

🤖 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!