Repository navigation
gen_smt_vcs: translate bvudiv as smtUDiv; refuse VCs the denotation does not cover - #1490
Open
kondylidou wants to merge 8 commits into
Open
kondylidou wants to merge 8 commits into
kondylidou wants to merge 8 commits into
Conversation
shigoel
reviewed
Oct 18, 2026
Split Term.hasDatatypeOp into mutually recursive helpers over List Term and List (List Term), as substituteTermIS does in Denote.lean, so it is structurally recursive instead of partial. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
joscoh
approved these changes
Oct 26, 2026
shigoel
approved these changes
Oct 26, 2026
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Oct 26, 2026
Contributor
Author
|
@shigoel @joscoh thanks for the approvals. The PR was ejected from the merge queue because the PR Import step failed (StrataPrImport-Prod:eb5d2281-759b-41e7-acb1-37e41c2205fb). The public checks all passed on the queue commit a710081, so I can't see what broke. Could you check the internal build log? If it is a real failure, my guess is something internal relies on one of the two intended changes here. gen_smt_vcs now refuses VCs that contain datatype operations instead of producing a goal, and bvudiv now denotes BitVec.smtUDiv instead of Lean's division. Happy to adjust once I know which, and if it was transient, could you re-queue it? |
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
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.
Fixes #1488.
gen_smt_vcsclosessmtVCsCorrect pwith a per-theorem axiom stating that its goals imply the denotation of the VCs, so every goal must carry the denotation's meaning. Two places where it did not:bvudivwas translated to Lean's/(x / 0 = 0) but denoted asBitVec.smtUDiv(x / 0is all ones). It is now translated asBitVec.smtUDiv. An audit oftranslateQueryagainstdenoteTerm, operator by operator, found no other mismatch.denoteTermhas no case for datatype operations, andSanitizedContext.toCoredrops the datatype fields, so the "datatypes not supported" guard never fired. For any VC over a datatype the denotation isnone,smtVCsCorrectisFalse, and the axiom proved it.createGoalnow fails with an error on such a VC instead of creating a goal. Boole'sgen_smt_vcs_boolegoes through the same function.Test
GenSMTVCsDenotation.lean:bvudivby zero proved with its SMT-LIB meaning (the issue's reproduction now stops at its first step, since the goal isx.smtUDiv 0#8 = 0#8), and a datatype program pinned to the refusal error.Not changed: the bridge axiom itself. #1480 is blocked until datatypes have a denotation.