Skip to content

v0.39.0 — f32 hard-float, verified DSL shipped by default, +2 division admits

Choose a tag to compare

View all tags
@avrabe avrabe released this 10 Jul 22:15
· 574 commits to main since this release
v0.39.0
7533c98
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

A seven-lane feature hub — scalar f32 hard-float reaches Cortex-M4F, the verified selector DSL ships as the DEFAULT selection path, two more #73 division admits fall, wit-bindgen buffers unblock, npm distribution lands, and the flaky Z3 release-blocker is killed. Gated by the claim-check gate (17/17) plus an independent cold-agent claim review.

Added

  • f32 hard-float reachable on thumb-2 (#619/#369, GI-FPU-002 phase 1): the VFP encoder was unreachable (no direct-selector float arms; blind VFP allocator). Now a real VFP value stack + AAPCS-VFP homing + CPACR enable, FPU-gated, honest-reject on M0/M3. f32 arith/compare/trunc/convert/const/param — 48/48 bit-exact vs wasmtime; two latent VCVT/CPACR bugs fixed. f64 held for phase 2.
  • npm CLI wrapper (#426): dependency-free, checksum-verified against the cosign-signed SHA256SUMS before extract.

Changed

  • SYNTH_SEL_DSL default-ON (#242): the verified selector DSL is now the SHIPPED path for its 40 Rocq-proved ops — byte-invisible (anchors 10/10, 88/88 fixtures identical vs opt-out). North-Star milestone.
  • Z3 CI links system libz3 (#553): kills the flaky build.rs download (blocked releases twice); ~1m41s vs ~16 min; default build stays z3-free.

Fixed

  • Two more #73 division admits (#242): i32.rem_s + i32.rem_u proven against exec_program_br; i32.div_s held honestly. 472 Qed / 6 Admitted (was 470/8).
  • --native-pointer-abi statics down-shift (#678): zero-init BSS statics rebase into the shrunk reservation — unblocks wit-bindgen buffer nodes.
  • Estimator allowlist verified empty (#498) + acceptance-criterion regression test.

Falsification: wrong if any shipped .text diverges from wasmtime on exercised inputs, a frozen anchor drifts without refreeze, claim_check derives counts differing from docs, or the f32 differential diverges on covered FPU targets — all CI-gated.

Platform binaries attach ~10 min after the tag.

🤖 Generated with Claude Code

Assets 13
Loading