Skip to content

v0.32.0 — proof-carrying specialization fires (#494 phase 2)

Choose a tag to compare

View all tags
@avrabe avrabe released this 08 Jul 02:39
· 534 commits to main since this release
v0.32.0
09c9a33
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Proof-carrying specialization fires for the first time (VCR-PERF-002 phase 2): a loom-proven value range makes clamp branches provably dead, and synth deletes them — every elision admitted only on an ordeal LRAT-certificate UNSAT, discharged before emission.

Added

  • SYNTH_FACT_SPEC value-range clamp elision (#629, default OFF). Symbolic QF_BV walk attaches wsc.facts premises; every no-else if…end whose condition is UNSAT under the premises is deleted with its proven-pure condition slice. Sat/Unknown/budget/impure/untracked → loud decline to the general lowering. gust_mix under ch ∈ [524,1524]: 84 B/28 insns → 14 B/6 insns. 1001/1001 in-bounds differential; wrong-bound red demonstrated then declined with a Sat counterexample; new fact-spec-oracle CI job; frozen anchors 10/10; facts-absent and flag-off byte-identical by construction.

Phase 3 = gale silicon re-measure vs the 0.45× floor (the #494 kill-criterion).

🤖 Generated with Claude Code

Assets 13
Loading