fix(metaverifier): run termCheck and precondElim phases in Core.genVCs - #1471
Open
kondylidou wants to merge 8 commits into
Open
kondylidou wants to merge 8 commits into
kondylidou wants to merge 8 commits into
Conversation
kondylidou
added a commit
to strata-org/Strata-Boole
that referenced
this pull request
Sep 6, 2026
…ate!/take!/drop! - dalek_sum_of_slice: `scalars : Sequence Scalar` and `Scalar := Sequence int` (bytes as ints read with the total `Sequence.select!`; `bytes_are_u8` states the [u8; 32] typing facts). No Map, no useArrayTheory. 23 cvc5 obligations, strict `all_goals smt` closes every Lean goal. Header documents each encoding choice and the differences from the verus-boogie translation. - Verify.lean: lower Core's total sequence operations (`Sequence.select!`, `update!`, `take!`, `drop!`), which the grammar already parsed; regression test StrataBooleTest/seq_unsafe_ops.lean, imported from the test root. - mutual_recursion: with Strata's Core.genVCs now emitting termination and well-formedness VCs, the Lean example hits the SMT→Lean bridge's missing datatype support (strata-org/Strata#1472); pin the named error via #guard_msgs so it flips when the bridge learns datatypes. - lakefile/manifest: TEMPORARY path dependency on ~/Developer/Strata carrying strata-org/Strata#1471 (Core.genVCs runs termCheck + precondElim). Revert to git main + `lake update Strata` once #1471 is merged. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Contributor
Author
Contributor
|
Can you start by making the CI happy? |
Contributor
Author
the ci is not failing on one of my changes. Found 2 files without proper copyright header: But I can fix them :) |
Contributor
Author
|
@fabiomadge can you maybe rerun the ci first, maybe it was already fixed with the new commits |
Contributor
|
Right, this CI probably didn't run on these changes... |
Contributor
Author
|
@fabiomadge header still missing. should I fix that here? |
Contributor
|
As you wish. I'll get on it, but it'll take a couple of hours until you can rebase. |
Contributor
Author
|
@fabiomadge fixed |
`Core.genVCs` (the reflection path behind `gen_smt_vcs` / `gen_smt_vcs_boole`)
ran only the loop phases before `preSymbolicEvalPipelinePhases`. The full
`Core.verify` pipeline also runs `termCheckPipelinePhase` and
`precondElimPipelinePhase` (transformPipelinePhases). Without the latter, any
program declaring a function with a `requires` clause made
`ObligationExtraction.extractObligations` fail ("function ... still carries a
precondition; run precondition elimination before extracting obligations"),
which `genVCs` turned into `none` and the tactic reported as
"Failed to generate VCs" with no further detail.
Add both phases, in the order the full pipeline uses, ahead of the loop
phases. Besides unblocking such programs, `gen_smt_vcs` now yields the same
well-formedness (function precondition) and termination obligations that
`Core.verify` emits, so the Lean-side certificate covers what the SMT path
checks.
Add a regression test with a `requires`-carrying function used in a
procedure body; before this change the tactic produced no goals for it.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…ate it `createGoal` reported only "Error translating query". Since the tactic must fail rather than drop an obligation it cannot state (dropping would weaken the bridge axiom's premise), report which VC failed and the bridge error, so users can tell what the Lean certificate does not cover. Typical trigger: termination/well-formedness VCs that mention a datatype sort, which the bridge does not yet declare. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
fabiomadge
force-pushed
the
fix/gen-vcs-precond-termcheck
branch
from
September 9, 2026 09:55
285ea85 to
32b24ae
Compare
joscoh
reviewed
Sep 9, 2026
| `Core.genVCs` (the reflection path behind `gen_smt_vcs`) used to skip that | ||
| phase, so `extractObligations` rejected the program ("function ... still | ||
| carries a precondition") and the tactic reported "Failed to generate VCs". | ||
| This test pins the fix: the goals below include the well-formedness check |
Contributor
There was a problem hiding this comment.
This is a bit of a strange comment for a proof of all_goals grind. If we stopped generating the well-formedness check, how would we notice?
Contributor
Author
There was a problem hiding this comment.
it wouldn't have. I checked: if precondElim still runs but stops emitting the call-site assert, all_goals grind passes happily. Switched to closing each obligation by name, which fails with "Case tag set_r_calls_safeDiv_0 not found" in that case, and with "unsolved goals" if an unexpected obligation appears. set_r_calls_safeDiv_0 is the one this PR is actually about, the check that safeDiv's requires holds at its call site in halve.
Review feedback: with `all_goals grind` the test cannot notice a dropped well-formedness check — it closes whatever goals happen to be there. Confirmed empirically: making `precondElim` still run but stop emitting the call-site assert leaves VC generation succeeding with that obligation gone, and `all_goals grind` still passes. Closing each obligation by name fails in that case with "Case tag `set_r_calls_safeDiv_0` not found", and with "unsolved goals" if an unexpected obligation appears, so the test pins the obligation set in both directions. `set_r_calls_safeDiv_0` is the obligation this PR is about: the check that `safeDiv`'s `requires` holds at its call site in `halve`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
This branch has not been deployed
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
4 participants
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.
Problem
Core.genVCs— the reflection path behind thegen_smt_vcstactic (andStrata-Boole's
gen_smt_vcs_boole) — ran only the loop phases(
insertLoopInvariantAsserts,loopElim) beforepreSymbolicEvalPipelinePhases.The full
Core.verifypipeline (transformPipelinePhases) additionally runstermCheckPipelinePhaseandprecondElimPipelinePhase.Without
precondElimPipelinePhase, any program that declares a function with arequiresclause makesObligationExtraction.extractObligationsfail withgenVCsmaps that tonone, and the tactic reports only "Failed to generateVCs", so the cause was invisible to users.
Fix
Add
termCheckPipelinePhaseandprecondElimPipelinePhaseto thegenVCsphase list, ahead of the loop phases, in the order
transformPipelinePhasesuses. Both require only
.noCFGBodies, which Boole/Core programs alreadysatisfy at that point;
precondElimestablishes.noPrecondsFromFuncs, whichextractObligationsexpects. Imports for the two modules added.Besides unblocking such programs,
gen_smt_vcsnow yields the samewell-formedness (function-precondition) and termination obligations that
Core.verifyemits, so the Lean-side certificate covers what the SMT pathchecks. Programs with recursive functions or
requires-carrying functions willtherefore see additional goals from the tactic.