Stage-3 REQ-8: reconstruction default-on — the per-clause trust migration (#350) - #91
Merged
maxine-at-forecast merged 3 commits intoJun 26, 2026
Conversation
…tion (#350)
The actual trust flip: where a `@bv` obligation is reconstruction-supported,
its clause `trust:` migrates from solver(z3 QF_BV) to the kernel-checked form,
at the SAME rung (L4) — trust-base-only, no verdict/rung changes. Default-ON
(no flag); builds ON REQ-7 (#349), does not rebuild the exporter or BvModel.
The fragment-support check keys on RENDERABILITY (the reconstruction-supported
set IS what `lean_smt_export` renders without `SmtExportError`):
* `lean_smt_export::clause_reconstruction_supported(expr, fragment)` =
`render_goal(obligation).is_ok()` — QF_LIA + arith/cmp QF_BV (`+`/`-`/`*`,
unsigned cmp, connectives) supported; bitwise/shift/rotate refused. The
renderable fragment's axiom-cleanliness is discharged once, statically, by
REQ-7's AC-8 (committed SmtExport.lean + the kernel-checked BvModel
faithfulness) — not re-run per clause.
* `engine::bv_kernel_checked_trust_profile()` — the migrated base: the
lean-smt reconstruction over the bounded-int model + the kernel-checked
`BvModel.frmInt_iff_frmBV` faithfulness; z3 no longer load-bearing; the
named pretty-printer residual (#356). `trust_is_kernel_checked` +
`KERNEL_CHECKED_TRUST_MARKER` key the audit split (nlsat relax counts too).
* `check::bv_proved_obl` grows a `clause_expr` param (both fn + lemma
callers); a supported clause -> kernel-checked trust, an unsupported one
keeps solver(z3), labeled as today (F-J). The engine tag stays `bitvector`
— only the orthogonal trust axis moves. `mix64` is the AC-9 same-item
split: `a+b==b+a` migrates, `a^b^b==a` stays solver-trusted.
* `audit::ResidualTrust` — the residual-trust statement aggregating the
kernel-checked-vs-solver split, naming the still-solver-trusted clauses +
the standing F-J fragments (bitwise/shift/rotate + the EPR-stratified
rel/array residual, named not migrated since the reconstruction fragment
excludes uninterpreted atoms). Additive (`skip_serializing_if = None`,
gated on `!bv_shadows.is_empty()`) so the v1 / nlsat goldens stay
byte-identical.
Tests: 3 unit (fragment-support split, the pure `bv_proved_obl` migration, the
audit aggregation + v1-absent gate) + 2 e2e in bv_lowering (the mix64 cert-level
trust split, the audit residual-trust statement). Full bv_lowering suite (16) +
audit/review/check/nlsat conformance green; doc-drift clean; AC boxes flip at G3
(REQ-9), not here, per stage-3 convention.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…0, #357) Adversarial review (#357) found: the bv route runs NO vacuity detection. A `@bv` clause is discharged as `req ⇒ clause`, so an UNSATISFIABLE `req` proves every clause vacuously — the §10 anti-Goodhart gaming vector the v1 cage rejects as `VacuousPrecondition`. The bv mutation gate masks this only for RESULT-REFERENCING clauses (every mutant survives → WeakContract); a param-only `@bv` clause or a `@bv` LEMMA (no body → no mutation) certified L4 — and, post-REQ-8, carried a KERNEL-CHECKED trust label — on a vacuous proof (the cert even recorded `vacuous_precondition: false`). The bv route newly permits param-only `ens` clauses (mix64's lemma needs it) and opened a vacuity path it never guarded; the trust flip stamped it kernel-checked. Fix: `BitVectorEngine::req_satisfiable` SAT-checks `req` at the clause's own width (consistent with the discharge's rendering, so never a width artifact); `bv_fn_cert`/`bv_lemma_cert` reject `VacuousPrecondition` when it is UNSAT (`None`/undecidable falls through — conservative, never a false rejection). Regression test forge/tests/bv_vacuity_gate.rs pins both the lemma and the param-only fn. Satisfiable-req cases unaffected (mix64, real lemmas, nowrap all still L4). Full forge suite green (verus+z3+full spine); clippy -D warnings + rustfmt 1.95.0 clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
req_satisfiable (bitvector.rs) + the vacuity gate (check.rs) drift the docs governing them. Content-sha refresh. Governed REQs unchanged. 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-8 — the trust flip. Closes #350. Child of the Stage-3 tree (umbrella xl #342 / gh #80; spec REQ-8 / AC-9). Includes the adversarial-review fix (#357).
What ships — the migration
Where a clause is reconstruction-supported, its
trust:migratessolver(z3) → kernel-checked, default-on, same rung (trust-base only, no verdict/level change):clause_reconstruction_supported = render_goal.is_ok()(renderability; axiom-cleanliness discharged by REQ-7 AC-8 + the kernel-provenBvModelfaithfulness).bitvector; nlsat is also kernel-grounded).BvModel.frmInt_iff_frmBV/tv_equiv_faithful+ the named string-emission residual (#356).solver(z3); EPR-stratified rel/array (the G2 residual) named not migrated (structurally outside the fragment, F-J).forge auditgains aresidual_truststatement aggregating the split (gated on!bv_shadows.is_empty()→ v1 audit goldens byte-identical).AC-9 verified:
mix64is the same-item split —a+b==b+a→ kernel-checked,a^b^b==a(bitwise) → solver(z3); the audit names 2 kernel-checked / 2 solver-trusted.Adversarial review (#357) — one finding, fixed
A pre-flip adversarial pass found the bv route ran no vacuity detection: a
@bvclause discharges asreq ⇒ clause, so an unsatisfiablereqproves it vacuously. The mutation gate masked this only for result-referencing clauses; a param-only clause or a@bvlemma certified L4 + kernel-checked on a vacuous proof. Fixed (d5c3ddf4):req_satisfiableSAT-checksreqat the clause width →VacuousPreconditionreject when UNSAT. Regression testbv_vacuity_gate.rs. Every other dimension came back clean (fragment refusal airtight, render ops correct, multiplication axiom-clean, faithfulness kernel-proven, Timeout≠Proved).Verification (full env)
Full
forgesuite green (verus + z3 + full Lean spine); clippy-D warnings+ rustfmt 1.95.0 clean; v1 goldens byte-identical;make doc-driftexit 0. AC boxes flip at G3 (REQ-9), per stage-3 convention.