Skip to content

v0.43.0 — isolation + verification closure

Choose a tag to compare

View all tags
@avrabe avrabe released this 15 Jul 13:34
· 444 commits to main since this release
v0.43.0
6c23833
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Seven-lane hub — the strongest soundness release in the series. Each lane's oracle re-verified by the coordinator before merge; a cold-agent clean-room review gated the tag (it caught a release-branch base error — the #752 fix was rebased in and re-verified before publish).

Headlines

  • #73 CLOSED — the last i32 division admit discharged. div_s INT_MIN/-1 is now Qed against the branch-taking executor, via a genuine model fix (the old overflow guard tested the raw representative; the theorem was false as stated). i32 division admits = 0 (473 Qed / 5 Admitted remain: 2 Compilation.v, 1 CorrectnessSimple.v, 2 ArmRefinement.v).
  • The trap-preservation VC is LIVE (#166). translation_validator now DERIVES the ARM trap condition from a branch-taking guarded executor and routes partial ops through it mandatorily — a guard-stripped / inverted / wrong-register lowering fails validation. Live for 5 classes: i32 div/rem, unreachable, i32 load/store, i32.trunc_f32, call_indirect. i64 div/rem and trunc_f64 remain unit-gated (disclosed, not live). The derived gate immediately caught #752 and ordeal#72.
  • Multi-memory phase 1 (#406). N wasm memories → N distinct native base regions (relocatable path); Model A, MPU/PMP-protectable. Single-memory byte-identical; every unsupported combination a typed loud-decline.
  • Falcon float story complete (#369). Call-boundary marshalling + f64 hard-float params + the f64 op tail (VRINT rounding, VMINNM/VMAXNM, copysign, demote, converts).

Fixed — six latent soundness bugs the hub's own instrumentation surfaced

  • #740: Thumb-2 B<cond>.W (T3) halved every conditional branch over 254 bytes (LLVM-cross-checked fix + out-of-range loud-decline).
  • #752: software bounds guard wrapped at the address-space top, letting top-of-memory multi-byte accesses escape the OOB trap (SUB-from-bound guard, ARM + RV32).
  • #746: i64/wide static-region accesses above sp_init were baked, not relocated (gale's dissolve unblock).
  • Three latent VFP bugs caught before f64 shipped: f32.copysign R0-clobber, f64 VCVT signed/unsigned base swap, in-place trunc VCVT home corruption.

Changed

  • Proof-carrying bounds-check elision (#494 × #390): under a loom-proven ValueRange premise the software bounds guard is proven dead and elided (ordeal-certified) — gust_poll guarded path 232 → 104 B, bit-identical to the unguarded floor. Opt-in, flag-off byte-identical.

Gates: pin sweep incl. npm, claim gate 18/18, frozen anchors 10/10, bazel test //coq:verify_proofs green, cold review CONFIRMED all nine claims post-rebase.

Assets 13
Loading