Skip to content

v0.31.0 — verified selector rules, facts ingestion, RV promo flip, z3-free default

Choose a tag to compare

View all tags
@avrabe avrabe released this 08 Jul 00:54
· 539 commits to main since this release
v0.31.0
f1aac4c
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

The first Rocq-verified selector rules land (VCR-SEL-001 increment 1); the proof-carrying-specialization pipeline opens (wsc.facts ingestion, #494 phase 1); RV32 local promotion ships default-on with a measured never-grow model (the #601 hold lifts); the default build drops its last C++ dependency.

Added

  • VCR-SEL-001 increment 1 (#623, epic #242): declarative rule table for i32 add/sub/mul/and/or/xor + rotl, generated Rust lowerings committed to the tree, one T1 theorem per rule with a Qed-coverage check that fails the //coq build on any gap. Behind SYNTH_SEL_DSL (default OFF, OFF ≡ baseline byte-identical).
  • wsc.facts ingestion (#624, VCR-PERF-002 phase 1): fail-safe schema-v1 parser threaded into CompileConfig; zero codegen change; the clamp-elision consumer is phase 2.

Changed (byte-changing on RV32, deliberate)

  • SYNTH_RV_LOCAL_PROMO default-ON (#626/#627): heuristic profitability replaced by measurement — a promoted lowering is kept only when its emitted bytes don't exceed the unpromoted baseline. Corpus: 10 shrink / 0 grow (flight_algo −32 B, accum −68 B); all 11 RV32 execution differentials green on the new default bytes; RV32 goldens promo-neutral by hash; =0 opt-out CI-gated.
  • static-link-z3 out of the default build (#621, #553): cargo test --workspace with no C++ toolchain (ordeal engine, 139/139); Z3 stays as the feature-gated differential oracle (SYNTH_SOLVER_DIFF=1).

Documentation

  • README North-Star + CLAUDE.md refreshed to post-v0.30 reality (#625).

🤖 Generated with Claude Code

Assets 13
Loading