Skip to content

v0.42.0 — trap-preservation VC + float completion + parity benchmark

Choose a tag to compare

View all tags
@avrabe avrabe released this 15 Jul 04:54
· 452 commits to main since this release
v0.42.0
cc3f6d9
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, each lane its own gated PR (#736–#744), all independently re-verified + a cold-agent clean-room review before tag.

Fixed (soundness)

  • Static above sp_init no longer silently miscompiles under --shadow-stack-size (#739/#744). Sub-word load/store arms baked the offset as an un-relocated immediate — invisible to the #678 rebase AND to the in-range oracle, which only walked relocations (a vacuous gate). Both fixed: the arms now relocate, and the oracle scans encoded text for surviving baked static constants and refuses loudly. #383/#678/#707 regressions green.
  • f64 comparisons would have returned stale-flag garbage — the #712 flag-clobber found in encode_thumb_f64_compare and fixed before f64 shipped (#741).
  • Mixed-pool parameter backing stored the wrong register under interleaved int/float signatures (#741).

Added

  • Trap-preservation is a provable obligation (VCR-VER-002 Phases A+B, #166, ordeal#59). synth-verify consumes ordeal 0.9.1's trap module: div/rem, memory OOB (symbolic bound), call_indirect (bounds ∨ null-slot ∨ type, with a closed-world compile-time-discharge mode), unreachable, and all six float→int trunc variants (validated against a 31-row boundary table incl. 2³¹ traps / −2³¹ in-range). The red-first gate proves every trap-DROPPING lowering is caught (Sat + counterexample) and every preserving one accepted (Unsat, LRAT re-checked). Scope, precisely: this is the VC library + red-first unit gate for all classes; live translation-validator wiring exists for div/rem (reject-direction-sound structural check) — wiring the remaining classes is the named follow-on.
  • The falcon float story completes (#719, #369 phase 2). f32 live across calls spills/rehomes; scalar f64 on cortex-m7dp (const/promote/arith/compare/load/store/across-call). 187/187 f32 + 126/126 f64 bit-exact vs wasmtime, CI-gated. Float-signature call marshalling and f64 params decline loudly — the named next increment.
  • The Rocq selector model is generated, not mirrored (VCR-ISA-001 #667). VcrSelRules.v defines rule_X := Gen.rule_X from the table the compiler ships; a selector change breaks the matching correctness proof. Proof count 472 — recounted from 512: the 40 interim reflexivity lemmas were retired as vacuous once the hand-written mirror was gone; no correctness proofs were lost, and none were added.
  • Reproducible wasm-AOT vs native-C parity benchmark (#735/#737). Measured bytes, pinned toolchains, one falsification command per row. Headline, precisely conditioned: gust_mix clamp under a loom-proven value-range premise compiles to 14 B vs 26 B measured arm-none-eabi-gcc -Os (0.54×) — the unspecialized number is 84 B, the LLVM floor row (12 B) is cited, and every cycle cell is OPEN pending silicon (DWT). The honest gaps are in the same table: gust_poll 3.48×, flat_flight 2.54×, falcon-f32 1.64×.
  • Redundant-mask elision (#494/#736): gust_kernel 34→20 B, ordeal-certified per elision, sound decline without the premise.

Changed

  • gust_poll 740→724 B (#390/#743): conditional-branch-transparent stack-reload forwarding; corpus 26 shrink / 0 grow; refreeze ritual done in order; opt-out pinned. Pre-existing #740 filed with an anti-vacuous xfail.

Gates: pin sweep incl. npm, claim gate 18/18, frozen anchors 10/10, cold review: all eight release claims CONFIRMED.

Assets 13
Loading