Stage-3 REQ-7: the Rust→Lean obligation exporter (QF_LIA + QF_BV) (#349) - #90
Merged
maxine-at-forecast merged 3 commits intoJun 24, 2026
Conversation
Build the automated Rust→Lean obligation exporter that closes the Tier-3
hand-translation gap `lean/Thermite/SmtDemo.lean` left open. New
`forge/src/lean_smt_export.rs` renders a Thermite predicate `Expr` into a Lean
`Prop` and emits the translation-validation goal `(P_prod) ⟺ (P_ref) := by smt`
+ a `#print axioms` probe, over two fragments: QF_LIA scalar (over `Int`) and
QF_BV (over the range-bounded integer machine-model). `reference_normalize`
supplies the independent reference encoding; `forge smt-export [<file>]
[--out <path>]` is the CLI surface. The committed `lean/Thermite/SmtExport.lean`
is the exporter's verbatim output (golden-tested, root-imported, kernel-checked
by `lake build`).
AC-8: all three exported theorems (1 QF_LIA + 2 QF_BV) discharge `by smt` and
`#print axioms` ⊆ {propext, Classical.choice, Quot.sound} — no sorryAx, no Smt
oracle, no Lean.ofReduceBool.
Key finding (recorded in z3-demotion.md): at the pinned lean-smt rev every
`BitVec`-typed `by smt` goal — even a pure unsigned comparison — bit-blasts
through the upstream `Smt/Reconstruct/BitVec/Bitblast.lean` `sorry` and pulls
`sorryAx`. The reconstruction-supported QF_BV encoding is therefore the
bounded-integer machine-model (bv var → Int with 0 ≤ x < 2^N, wrap → `% 2^N`,
unsigned cmp → Int cmp), which is kernel-clean; the literal BitVec render (the
artifact REQ-8 replays) stays the documented residual.
Scope: exporter only (REQ-8 owns reconstruction default-on + the render_bv_prop
faithfulness obligation). No change to the REQ-1..6 bv route. AC checkboxes flip
at G3 per the stage-3 convention. Re-pinned cli.md + workspace.md (doc-drift
CURRENT).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Discharge the REQ-8 `render_bv_prop` faithfulness obligation in our OWN Lean spine,
without depending on lean-smt's (stalled, 18-mo-dormant) literal QF_BV reconstruction.
The exporter renders a `@bvN` clause over the bounded-integer machine-model (not
`BitVec N`, whose `smt` reconstruction bit-blasts through an upstream `sorry` — every
BitVec goal pulls sorryAx, and the root cause is lean-smt's `reconstructRewrite` total
stub + a partial `BV_BITBLAST_STEP`, so closing the one `eq_eq_beq` sorry is necessary
but not sufficient).
`lean/Thermite/BvModel.lean` proves the model faithful instead:
- `Tm`/`Frm` mirror the exporter's `render_term`/`render_prop` fragment arm-for-arm;
- `tmBV`/`frmBV` give the genuine fixed-width `BitVec N` semantics; `tmInt`/`frmInt`
give the bounded-integer model the exporter emits (`% 2^N`, unsigned cmp as Int cmp);
- `frmInt_iff_frmBV`: the two denotations agree under the `toNat` valuation;
- `tv_equiv_faithful`: so the exporter's `by smt`-reconstructed int-model `(P_prod) ↔
(P_ref)` certifies the genuine bit-vector clauses.
All three theorems are KERNEL-CHECKED, `#print axioms` ⊆ {propext, Classical.choice,
Quot.sound}, and Mathlib/Smt-FREE — so unlike `Thermite.SmtExport` this runs in CI via
`scripts/lean-axiom-probe.sh` (added as a build target + in-file `#print axioms`, the
SubstKit convention; promoting `tv_equiv_faithful` into the gated THEOREMS list is the
REQ-8/G3 trust-flip action). Combined with the exporter's int-model `↔`, a `@bv`
clause's truth is kernel-grounded end to end with no solver in the trust base for the
renderable fragment.
The Rust-emitter ⟷ Lean-AST correspondence stays inspection-tier (as for the whole
exporter). Completing lean-smt's literal QF_BV reconstruction remains an open UPSTREAM
task, no longer load-bearing for us.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ernel faithfulness (#349) REQ-7 materially changed REQ-8's foundation, so record it in the decision record for REQ-8 to inherit accurately: - cvc5's LITERAL BitVec `by smt` reconstruction pulls sorryAx (the upstream Bitblast.lean sorry) — so the exporter renders QF_BV over a bounded-integer machine model (var→Int 0≤x<2^N, wrap→%2^N, unsigned cmp→Int cmp), which discharges axiom-clean. Verified on all 3 shipped theorems. - Reconstruction-support = QF_LIA + the arithmetic/comparison QF_BV subset; bitwise/shift/rotate is REFUSED (SmtExportError) and stays solver-trusted (F-J) — mix64's xor/rotate clauses included. REQ-8's fragment check keys here. - render_bv_prop faithfulness is largely DISCHARGED, not deferred: BvModel.lean kernel-proves the bounded-int model ⇔ BitVec semantics (axiom-clean). REQ-8's residual narrows to the two string-emission legs (#356). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stage-3 REQ-7 — the automated Rust→Lean obligation exporter, the reconstruction half's foundation. Closes #349 (+ #356, the faithfulness metatheorem). Child of the Stage-3 tree (umbrella xl #342 / gh #80; spec REQ-7 / AC-8).
What ships
forge/src/lean_smt_export.rs+ theforge smt-exportCLI: renders a per-clause obligation to thesmt-dischargeable Lean goal(P_prod) ⟺ (P_ref), closingSmtDemo.lean's Tier-3 hand-translation gap.reference_normalizeis the independent reference encoding.lean/Thermite/SmtExport.lean— the exporter's verbatim output (golden-tested: the committed file ISforge smt-export's output), root-imported and lake-build kernel-checked.The snag, and the sound workaround
cvc5's literal
BitVec Nreconstruction pullssorryAxat the pinned lean-smt7d1d8239— everyBitVec-typedby smtgoal (even a pure comparison) bit-blasts through the upstreamSmt/Reconstruct/BitVec/Bitblast.leansorry(thez3-demotion.mdwall). So the exporter renders QF_BV over a bounded-integer machine model (bvNvar →Intwith0 ≤ x < 2^N; wrap op →% 2^N; unsigned cmp →Intcmp), whichsmtdischarges via clean linear-arith reconstruction.This is proven faithful, not asserted.
lean/Thermite/BvModel.lean(#356) is a kernel-checked, Mathlib-free, core-BitVec-only metatheorem —tmInt_eq_toNat,frmInt_iff_frmBV,tv_equiv_faithful— proving the bounded-int model ⇔BitVecsemantics. So therender_bv_propsemantic faithfulness REQ-8 was to own is largely discharged; the residual narrows to the two string-emission legs.Scope (honest)
Reconstruction-support = QF_LIA + the arithmetic/comparison QF_BV subset (
+ - *, unsigned compares, logical connectives). The bitwise/shift/rotate subset has no cleanIntencoding and hits theBitVecsorry— the exporter refuses it (SmtExportError, a named skip, never a silent mis-encode), somix64'sa^b^b==aand the rotate lemma stay solver-trusted (F-J). REQ-8's fragment-support check keys on exactly this split.Verification (independently re-run by the orchestrator)
#print axioms = [propext, Classical.choice, Quot.sound]— nosorryAxdespite the upstream Bitblastsorrybeing in the dep graph.lake build Thermite.BvModel, core-only, inlean-axiom-probe.sh).forge smt-exportgolden matches the committedSmtExport.lean; fullforgesuite green (verus+z3+spine, no REQ-1..6 regressions); clippy-D warnings+ rustfmt 1.95.0 clean;make doc-driftexit 0.The 3rd commit is an orchestrator note in the design doc's decision record recording this as-built approach for REQ-8. AC boxes flip at G3 per stage-3 convention.