Skip to content

fix(cf): #500 optimized-path forward-branch shapes fixed-or-declined; #498 estimator gap allowlist emptied (#242) - #641

Merged
avrabe merged 2 commits into
mainfrom
fix/500-498-optimized-cf-estimator
Jul 8, 2026
Merged

avrabe merged 2 commits into
mainfrom
fix/500-498-optimized-cf-estimator

Conversation

@avrabe

@avrabe avrabe commented Jul 8, 2026

Copy link
Copy Markdown
Contributor

Closes #500. Advances #498. Part of epic #242 (VCR-ORACLE / Track C honest-degradation discipline).

Salvage provenance: this lane's implementation was authored in the lane-500-498 worktree by a session that hit its limit with the work uncommitted. Committed as-found (commit 1), then assessed against the contract, verified end-to-end, and repaired where verification demanded (commit 2: a stale test expectation + lint). All red/green evidence below was produced fresh on this branch.

Rebase note for lane-377: this branch touches arm_encoder.rs, instruction_selector.rs, optimizer_bridge.rs — lane-377 overlaps these files and will rebase over this PR.

#500 — per-shape verdict table

Every shape from the issue (plus the two the class implies), pinned by the new execution differential scripts/repro/cf_shapes_500_differential.py (cf_shapes_500.wat, unicorn vs wasmtime, memory bit-compare, both branch directions):

Shape wat main (086968a) Verdict on this branch
A ifelse nested block + br_if + br (desugared if/else) OK (already fixed by #483) stays on optimized path, correct
B seqblocks two sibling blocks, each br_if-exited OK (already fixed by #483) stays on optimized path, correct
C real_ifelse real if/else construct MISCOMPILE — If/Else Nop'd, BOTH arms executed (real_ifelse(1) stored the else-arm's 400) honest decline at optimize_full → direct selector, correct
C′ real_if if with no else, content after join MISCOMPILE — then-arm executed unconditionally (real_if(0) stored 55) honest decline → direct selector, correct
D br_func function-level br (depth = implicit function body) MISCOMPILE — saturating_sub clamped onto the outermost block's end; post-block code still ran (br_func(1) also stored 88) honest decline on optimized path; direct selector fixed (function-level br = full return: result→R0, frame dealloc, pop {r4-r8,pc} — old direct arm emitted a bare bx lr, skipping the epilogue)
E early_ret non-tail return MISCOMPILE — return dropped to Nop, fell through (early_ret(1) also stored 111) honest decline on optimized path → direct selector's Return arm, correct

Also in the class, no repro shape reaches it today but pinned defensively:

  • unresolvable branch target in ir_to_arm's resolution pass: a missing label used to be skipped silently, leaving the offset-0 placeholder → br_if landed on the very next instruction (the literal Optimized (non-relocatable) path miscompiles block/br_if: branch target lands mid-instruction #483-class bug). Now declines loudly.
  • direct selector function-level br_if = conditional return (BEQ over the return sequence; stack peeked, not popped, so the fall-through path keeps its operands live; reload-before-CMP so a spill reload can't sit between CMP and Bcc).

Red → green (full outputs in the harness, SYNTH=<binary> python scripts/repro/cf_shapes_500_differential.py):

=== baseline main (086968a) ===         === with fix ===
FAIL real_ifelse(1,)  mem (16, 44, 144)  OK   (all 14 cases)
FAIL real_if(0,)      mem (20, 0, 55)    ORACLE: PASS
FAIL br_func(1,)      mem (32, 0, 88)
FAIL early_ret(1,)    mem (40, 0, 111)
ORACLE: FAIL (4)

resolved_branch_geometry (#604/#607) discipline is respected: the geometry mapper sizes resolved streams via estimate_arm_byte_size, and the new far-branch decline guarantees every surviving numeric branch fits the 2-byte short form — so the estimator's new offset-sensitivity agrees with the layout the bridge actually froze, and no shipped stream's geometry shifts (frozen fixtures bit-identical, below).

#498 — estimator gap allowlist: 2 → 0

The estimator_encoder_agreement oracle's KNOWN_GAP machinery is deleted; every case now asserts exact agreement.

Former gap Was Closed by
BOffset/BCondOffset far ("structural survivor") est 2 / enc 4 — chicken-and-egg: estimator runs pre-resolution on the offset-0 placeholder estimator now mirrors the encoder's short/.w range split (B.N imm11 / B.N imm8 → 2, else 4); the bridge's resolution pass declines any displacement outgrowing the short form its offset table assumed (previously a silent latent layout-shift miscompile for large functions) — the chicken-and-egg resolved by refusing the egg, loudly
Mov negative imm ("encoder-side survivor") est 4 / enc 2 wrong-value — signed *imm <= 255 emitted MOVS Rd, #(imm & 0xFF) for negative imm; MOVW truncated >0xFFFF encoder splits on the unsigned value: imm8 MOVS / imm16 MOVW / full-width MOVW+MOVT (8 bytes); estimator mirrors the three-way split. No emitter produces the wide shape today (both selectors materialize wide constants as explicit Movw/Movt or Movw+Mvn), so shipped bytes are unchanged — verified by the frozen anchors

New agreement cases: BOffset_far, BCondOffset_far, BCondOffset_far_neg, Mov_imm_neg, Mov_imm_wide.

Test repair (commit 2)

optimized_path_declines_functions_with_calls asserted optimize_full succeeds on fib then ir_to_arm declines (#188) — but fib contains a real if/else, which now declines earlier. Split the pin: a straight-line local-call stream isolates the #188 ir_to_arm decline; the fib body pins the new #500 optimize_full decline (optimized_path_declines_real_if_else).

Verification (re-run in full after rebasing onto #636, which touches the same three files)

  • cf_shapes_500_differential.py: baseline main FAIL (4) → this branch PASS (14/14)
  • estimator_encoder_agreement: ok (allowlist empty, exact agreement everywhere)
  • cargo test -p synth-cli --test frozen_codegen_bytes: 10/10 ok — shipped .text untouched
  • cargo test --workspace: green
  • cargo fmt --check + cargo clippy --workspace --all-targets -- -D warnings: clean

🤖 Generated with Claude Code

avrabe and others added 2 commits July 8, 2026 11:37
…ap allowlist emptied

Salvaged work-in-progress from an interrupted session (agent hit its session
limit at 198 tool uses with these changes uncommitted in the lane-500-498
worktree); committed as-found before verification.

#500 (per-shape, #483 class):
- optimizer_bridge wasm_to_ir: function-level br/br_if (depth reaches the
  implicit function body) now DECLINES loudly (checked_sub, not the silent
  saturating_sub clamp onto the outermost block / bogus id 0)
- optimizer_bridge wasm_to_ir: non-tail `return` declines (was silently
  dropped -> fall-through executed post-return code)
- optimizer_bridge optimize_full: a real if/else surviving the select-idiom
  preprocessing declines (was Nop'd -> both arms executed unconditionally)
- optimizer_bridge ir_to_arm resolution: a branch whose target id has no
  emitted label declines loudly (was skipped -> offset-0 placeholder landed
  mid-shape, the #483-class miscompile)
- direct selector: function-level br == return (full epilogue: result to R0,
  frame dealloc, pop {r4-r8,pc}) instead of the old bare `bx lr` /
  outermost-block clamp; function-level br_if = conditional return (BEQ over
  the return sequence, stack peeked not popped so the fall-through stays live)

#498 (estimator<->encoder agreement, allowlist emptied):
- estimator: BOffset/BCondOffset offset-sensitive (mirrors the encoder's
  short/.w range split); bridge resolution declines displacements that
  outgrow the 2-byte form its offset table assumed (latent layout-shift
  miscompile for large functions)
- encoder: Mov imm splits on the UNSIGNED value (imm8 MOVS / imm16 MOVW /
  full-width MOVW+MOVT) — retires the wrong-value 2-byte MOVS #(imm&0xFF)
  for negative imm and the truncated MOVW above 0xFFFF; estimator mirrors
- estimator_encoder_agreement oracle: KNOWN_GAP machinery removed, every
  case now asserts exact agreement

Refs #500 #498 #242

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…rm decline

The fib-based regression test asserted optimize_full SUCCEEDS then ir_to_arm
declines (#188) — but fib contains a real if/else, which now declines earlier
at optimize_full (#500). Split the pin: a straight-line local-call stream
isolates the #188 ir_to_arm decline; the fib body pins the #500 optimize_full
decline. Plus fmt + a clippy doc-lazy-continuation fix.

Refs #500 #188

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@codecov

codecov Bot commented Jul 8, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 82.84519% with 41 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-synthesis/src/optimizer_bridge.rs 78.12% 21 Missing ⚠️
crates/synth-synthesis/src/instruction_selector.rs 85.29% 20 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit a1541c0 into main Jul 8, 2026
29 of 30 checks passed
@avrabe
avrabe deleted the fix/500-498-optimized-cf-estimator branch July 8, 2026 11:14
avrabe added a commit that referenced this pull request Jul 8, 2026
…nonzero facts (#636/#638/#639/#640/#641) (#644)

Pin sweep 0.32.1 -> 0.33.0 + CHANGELOG.

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Jul 10, 2026
…cross a popcnt body (#242) (#700)

#498's estimator gaps (Cmn/Adds/Subs high-reg, Popcnt, i64 long-seqs) and the
neg-imm/wide MOV encoder-value bug were all closed by #555/#641: the
`estimator_encoder_agreement` oracle's KNOWN_GAP allowlist is EMPTY and passes
with exact per-op agreement. This adds the acceptance-criterion regression the
issue names but that no test exercised: a `block`/`br_if` whose body spans a
mis-sizable op (`popcnt`, 86 bytes) BETWEEN the conditional branch and its
target.

The test lowers the shape on the real optimized path (`optimize_full` +
`ir_to_arm`), re-encodes every resulting `ArmOp` with the real Thumb-2 encoder,
and asserts (1) the shape stays on the optimized path with Popcnt + a resolved
BCondOffset present, (2) estimator == encoder length op-for-op, and (3) the
resolved br_if displacement lands on a REAL instruction boundary PAST the popcnt
body. Injecting the pre-#498 `popcnt => 2` estimate makes the branch resolve to
offset 0 (into the middle of the popcnt) and the test fails — confirming teeth.

Test-only: no emitted bytes change; frozen anchors 10/10 untouched.

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Optimized path: br_if to a forward block end still unresolved for if/else and sequential-block shapes (#483 class, broader)

1 participant