synth v0.49.0

What's Changed

• feat(#77,#80): platform space-consistency invariant + P3 async error-context.drop lowering by @avrabe in #810
• feat(#782): sound ARM32 i64 trunc_sat via branch-free FP decompose — falcon skip 4→0 by @avrabe in #812
• feat(#778): WCET phase 4 — bounded self-recursion via a verified depth-hint by @avrabe in #813
• fix(#761): separate R9 globals base from linmem page — kill the self-contained --cortex-m alias by @avrabe in #811
• proof(#242): VCR-WASM-001 i64 transcription batch — 22 ops, 536→585 Qed by @avrabe in #814
• test(vcr-sel-005): universe-complete cross-backend op-parity gate — surface 16 silent ARM/RV32 op-gaps (#242, #223, #232) by @avrabe in #816
• feat(#242): VCR-RA-003 phase 2 — across-CALL + across-JOIN allocation validation (whole-function) by @avrabe in #817
• chore(release): v0.49.0 — phase-2 frontier + falcon to zero by @avrabe in #818

Full Changelog: v0.48.0...v0.49.0

synth v0.48.0

What's Changed

• fix(#782b): float select + explicit float return — the 'integer popped f32' class is not pressure, it's the clamp idiom (+2 adversarial finds) by @avrabe in #801
• feat(#798): RV32 active data segments SHIP — .wasm_data records + linker placement + startup copy, read-back hard gate by @avrabe in #802
• feat(#782a): implement the WASM trunc_sat family — nontrapping saturating float→int (i32 forms on ARM32, all 8 on aarch64) by @avrabe in #803
• docs(claims): claim-surface extension — machine-derived status.json + badges, generated FEATURE_MATRIX, repo-metadata pin, README link tripwire, roadmap-doc deletion (#48-surface) by @avrabe in #804
• fix(claims): regenerate status.json + FEATURE_MATRIX for #803 trunc_sat ops (main is red) by @avrabe in #805
• feat(#242): VCR-WASM-001 phase 3 — extra-coq-package hook landed (dep-pending on unfree CompCert) by @avrabe in #806
• feat(#242): VCR-RA-003 unconditional register-allocation validator (bounded straight-line + spill/callee-saved) by @avrabe in #808
• feat(#778): WCET phase 3 — inter-procedural composition over the direct call graph by @avrabe in #807
• chore(release): v0.48.0 — real modules, verified allocator by @avrabe in #809

Full Changelog: v0.47.0...v0.48.0

synth v0.47.0

What's Changed

• feat(aarch64): milestone 4 — sound trapping float→int trunc + NaN-correct min/max + copysign (#538) by @avrabe in #790
• fix(#791): const-only-body exports return caller residue — Opcode::Const never set last_result_vreg by @avrabe in #794
• feat(#778): WCET phase 2 — statically-proven loop trip counts + the --wcet-hints sound-checker seam by @avrabe in #793
• feat(#275 finale): self-contained --cortex-m call_indirect — PC-relative flash funcref table (converts the #717 loud-decline) by @avrabe in #792
• VCR-WASM-001 phase 2: WasmCert-Coq real-dep feasibility verdict + 19-op i32 refinement batch (49 Qed) by @avrabe in #796
• feat(#418): bind cabi-arena-realloc natively on the self-contained dissolve — synthesized in-module arena allocator by @avrabe in #799
• feat(#777): VCR-VER-003 phase 2 — span validation + self-contained ROM-image gate + RV32 coverage by @avrabe in #797
• chore(release): v0.47.0 — close the loops by @avrabe in #800

Full Changelog: v0.46.0...v0.47.0

synth v0.46.1

Full Changelog: v0.46.0...v0.46.1

synth v0.46.0

What's Changed

• test(#275): execution gate for the self-contained reachable call graph by @avrabe in #784
• feat(#777): VCR-VER-003 — per-compilation static-data addressing validation (the #757 miscompile class made unrepresentable) by @avrabe in #785
• feat(#778): sound static per-function WCET bound (--emit-wcet, synth-wcet-v1) by @avrabe in #786
• proof(#166): close verify-what-ships proof residuals — 2 admits discharged, 3 pinned as honest T3 by @avrabe in #788
• feat(aarch64): milestone 3 — scalar floating point (#538) by @avrabe in #787
• chore(release): v0.46.0 — qualification depth + capability breadth by @avrabe in #789

Full Changelog: v0.45.2...v0.46.0

synth v0.45.2

What's Changed

• fix(#776): aarch64 rotl clobbers a computed rotate operand (silent wrong result) by @avrabe in #781
• chore(release): v0.45.2 — #776 aarch64 rotl clobber soundness fix by @avrabe in #783

Full Changelog: v0.45.1...v0.45.2

synth v0.45.1

What's Changed

• fix(#757): overlapping active data segments bind reloc to the wrong segment — silent miscompile on gale's fused node by @avrabe in #779
• chore(release): v0.45.1 — #757 soundness fix (overlapping-segment reloc miscompile) by @avrabe in #780

Full Changelog: v0.45.0...v0.45.1

synth v0.45.0

What's Changed

• feat(#538): aarch64 backend milestone 2 — full i32+i64 integer ALU (7→50 ops) by @avrabe in #769
• feat(#494): const-divisor rem_u identity elision — a proof-carrying 12x beat over clang -Os by @avrabe in #770
• feat(VCR-WASM-001): anchor WASM source semantics on WasmCert-Coq — i32.add bridge (bounded first increment) by @avrabe in #771
• investigate(#757): 7 faithful RawVec-grow+memmove reconstructions — all GREEN (bug needs gale's module; NO FIX) by @avrabe in #772
• feat(VCR-ISA-001): extend generate-not-mirror Rocq ISA model to nine i64 pseudo-ops (41→50) by @avrabe in #773
• feat(#396): synth-provenance-v1 branch-transformation map + reconciliation gate (VCR-DEC-003) by @avrabe in #774
• chore(release): v0.45.0 — the Mega-Hub epic (all 3 North-Star tracks) by @avrabe in #775

Full Changelog: v0.44.0...v0.45.0

synth v0.44.0

What's Changed

• test(dwarf): independent-parser gate via llvm-dwarfdump on emitted DWARF (#394) by @avrabe in #763
• v0.44.0 Lane B: #406 multi-segment static-data coverage + honest MPU-isolation decline by @avrabe in #764
• v0.44.0 Lane D: #390 redundant-store elimination in forward_stack_reloads (gust_poll 724→716 B) by @avrabe in #765
• feat(VCR-ISA-001): extend generate-not-mirror Rocq ISA model to i32.eqz (40→41) by @avrabe in #767
• feat(#756): i64 div/rem + i32.trunc_f64 into the LIVE trap validator (VCR-VER-002 Lane A) by @avrabe in #766
• chore(release): v0.44.0 — five-lane hub (live trap classes, verified-selector 40→41, multi-mem coverage, size win, DWARF gate) by @avrabe in #768

Full Changelog: v0.43.1...v0.44.0

synth v0.43.1

What's Changed

• fix(#758): self-contained --cortex-m ships active (data) segments (crt0 ROM→RAM copy) by @avrabe in #759
• investigate(#757): disprove the wide-static-copy triage mechanism + THM_CALL-aware oracle (NO FIX — #757 stays open) by @avrabe in #760
• chore(release): v0.43.1 — self-contained data soundness fix (#758) + differential hardening by @avrabe in #762

Full Changelog: v0.43.0...v0.43.1