feat(Core): nat/pos counterexample support via UF+axioms re-query#1439
Open
kondylidou wants to merge 1 commit into
Open
feat(Core): nat/pos counterexample support via UF+axioms re-query#1439kondylidou wants to merge 1 commit into
kondylidou wants to merge 1 commit into
Conversation
Add candidate-model propagation and axiom-drop re-query so nat/pos verification failures surface concrete counterexamples instead of stopping at `unknown`. Key changes: - SMTUtils: parse cvc5 candidate model on `unknown` result; use actual user-variable SMT terms (from estate.functions) in incremental solver get-value calls instead of boolean assumption IDs, so nat/pos variable values are retrievable - Verifier: preserve `unknown (some m)` payload across SMT.Result.merge; extract candidate model from `unknown (some m)` in getObligationResult; add VCResult.hasValidityUnknown (weaker gate than isUnknown, catches satisfiableValidityUnknown outcomes from nat VCs with bridge axioms); add requeryDropAxioms parameter to verify — strips named axiom assumes from oblProgram and re-runs unknown obligations so the solver can certify a counterexample unimpeded by universally-quantified bridge axioms - VerifierProofs: update merge_kind proof for new unknown×unknown model-preserving branches - lake-manifest: bump StrataDDM to 4ea13cd (adds @[noExponent] arg-level format marker needed by Strata/DL/SMT/DDMTransform/Parse.lean) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
github-actions
Bot
added
Waiting-For-Review
Core
dependencies
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.
Enables concrete counterexamples for nat/pos verification failures.
When cvc5 returns
unknownwith a candidate model (as it does when quantifiedbridge axioms prevent certification), the candidate model is now preserved
through
SMT.Result.mergeand extracted ingetObligationResultfor display.A new
requeryDropAxiomsparameter toverifystrips bridge axiomassumestatements from obligation procedures and re-runs unknown obligations, letting
the solver return a certified
sat(counterexample) unimpeded by the universals.Changes
SMTUtils.lean— parse cvc5 candidate model onunknownverdict; useactual user-variable SMT terms (via
estate.functions) in incrementalget-valuecalls instead of boolean assumption IDs so nat/pos values areretrievable
Verifier.lean— preserveunknown (some m)payload acrossSMT.Result.merge; extract candidate models fromunknown (some m)ingetObligationResult; addVCResult.hasValidityUnknown(weaker gate thanisUnknown, catchessatisfiableValidityUnknownoutcomes from nat VCs withbridge axioms); add
requeryDropAxioms+ re-query pass toverifyVerifierProofs.lean— updatemerge_kindproof for newunknown×unknownmodel-preserving brancheslake-manifest.json— bump StrataDDM to4ea13cd(adds@[noExponent]arg-level format marker, fixing a build regression in
DDMTransform/Parse.lean)