synth v0.52.0

What's Changed

• chore(deps): bump wasm-encoder from 0.253.0 to 0.254.0 by @dependabot[bot] in #861
• chore(deps): bump dependabot/fetch-metadata from 2 to 3 by @dependabot[bot] in #862
• chore(deps): bump pulseengine/rivet from 0.28.0 to 0.30.0 by @dependabot[bot] in #863
• chore(deps): bump ordeal from 0.9.1 to 0.16.1 by @dependabot[bot] in #864
• fix(main): restore BvTerm::Urem arms for ordeal 0.16.1 + latent ord_bv panic + hold 0.x-minor dependabot bumps by @avrabe in #866
• feat(#867): ISA-model adequacy — counted simplified-model trusted base + model-coverage complement by @avrabe in #870

Full Changelog: v0.51.0...v0.52.0

synth v0.51.0

What's Changed

• test(#850): harden 9 differential oracles to read ELF .symtab, not disasm text by @avrabe in #853
• feat(#851): aarch64 non-param locals — zero-init stack slots, copy-semantics get/set/tee by @avrabe in #856
• feat(#851): aarch64 linear-memory load/store lowering + gale's acceptance gate by @avrabe in #855
• chore(release): v0.51.0 — aarch64 runs real WASM modules (#851) + oracle hardening (#850) by @avrabe in #860

Full Changelog: v0.50.1...v0.51.0

synth v0.50.1

What's Changed

• fix(#846): recover gpio-thin +44 B — flip shift-mask-elide default-on by @avrabe in #847

Full Changelog: v0.50.0...v0.50.1

synth v0.50.0

What's Changed

• feat(VCR-WASM-001): wire i64 add/sub/mul/and/or/xor into exec_wasm_instr — close the op-level-only residual (#242) by @avrabe in #820
• feat(#815): VCR-RA-003 RV32 register-allocation validator (RV32 analogue of the ARM gate) by @avrabe in #821
• chore(deps): bump pulseengine/rivet from 0.26.0 to 0.28.0 by @dependabot[bot] in #822
• chore(deps): bump actions/setup-node from 6 to 7 by @dependabot[bot] in #823
• chore(deps): bump actions/setup-python from 6 to 7 by @dependabot[bot] in #824
• chore(deps): bump ordeal from 0.9.1 to 0.12.0 by @dependabot[bot] in #825
• chore(deps): bump wasmparser from 0.253.0 to 0.254.0 by @dependabot[bot] in #827
• chore(deps): bump scry-sai-core from 3.2.1 to 3.2.4 by @dependabot[bot] in #828
• chore(deps): bump anyhow from 1.0.103 to 1.0.104 by @dependabot[bot] in #830
• chore(deps): bump serde_json from 1.0.150 to 1.0.151 by @dependabot[bot] in #833
• chore(deps): bump wit-component from 0.252.0 to 0.254.0 by @dependabot[bot] in #834
• fix(ci): repair red main — Cargo.lock wasmparser dedup + ordeal 0.12 BvTerm::Urem by @avrabe in #836
• chore(deps): bump wat from 1.252.0 to 1.254.0 by @dependabot[bot] in #835
• chore(deps): bump thiserror from 2.0.18 to 2.0.19 by @dependabot[bot] in #829
• chore(deps): bump wit-parser from 0.253.0 to 0.254.0 by @dependabot[bot] in #832
• chore(deps): bump wast from 253.0.0 to 254.0.0 by @dependabot[bot] in #826
• chore(deps): bump bitflags from 2.13.0 to 2.13.1 by @dependabot[bot] in #831
• fix(#837): lower frame-backing i64/f64 VALUE param across a call by @avrabe in #840
• VCR-DEC-001: whole-function graph-colouring allocator spike (flag-off, #242) by @avrabe in #843
• ci: auto-merge patch/minor Dependabot bumps, hold majors for review by @avrabe in #838
• feat(rv32): close memory.size/memory.grow parity gaps (VCR-SEL-005, #223/#232/#242) by @avrabe in #841
• feat(verify): model i64.rem_u/rem_s with native BvTerm::Urem/bvsrem (was havoc) by @avrabe in #844
• feat(aarch64): void-block control flow — block/br/br_if (#538) by @avrabe in #842
• WCET phase 5 (#778): data-dependent masked-ceiling loop certificates by @avrabe in #839
• chore(release): v0.50.0 — cross-backend verified core + the allocator endgame begins by @avrabe in #845

Full Changelog: v0.49.0...v0.50.0

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