Fix Boole tests after merge#1209
Merged
Merged
Conversation
atomb
approved these changes
May 22, 2026
shigoel
approved these changes
May 22, 2026
PROgram52bc
reviewed
May 22, 2026
Contributor
PROgram52bc
left a comment
PROgram52bc
left a comment
There was a problem hiding this comment.
I left some hand-written comments based on agent feedbacks.
| | .seq_of_bv8 _ ⟨_, vs⟩ | .seq_of_bv16 _ ⟨_, vs⟩ | .seq_of_bv32 _ ⟨_, vs⟩ | ||
| | .seq_of_bv64 _ ⟨_, vs⟩ | .seq_of_int _ ⟨_, vs⟩ => do | ||
| let vals ← vs.toList.mapM toCoreExpr | ||
| return vals.foldl (fun acc v => mkCoreApp Core.seqBuildOp [acc, v]) Core.seqEmptyOp |
Contributor
There was a problem hiding this comment.
I think here it still uses the default Core.seqEmptyOp as an initial value, and could lead to missing type information if vals is empty.
| function Seq_lib_filter (s : Sequence bv32, p : bv32 -> bool) : Sequence bv32; | ||
| function Seq_lib_sort_by (s : Sequence bv32, less : bv32 -> bv32 -> bool) : Sequence bv32; | ||
| function Seq_lib_to_set (s : Sequence bv32) : Set bv32; | ||
| function Set_finite (s : Set bv32) : bool; |
Contributor
There was a problem hiding this comment.
Since they are no longer polymorphic, maybe renaming to something like Set_finite_bv32 (and similarly for the above) makes more sense?
Contributor
PROgram52bc
pushed a commit
that referenced
this pull request
May 22, 2026
…oding Resolves conflict in StrataTest/Languages/Boole/FeatureRequests/sha256_compact_indexed.lean. Base (#1209) independently fixed the seqEmpty type-loss in Verify.lean / Factory.lean and made the SHA256 example monomorphic with extra invariants/preconditions, so its expected #guard_msgs output is the post-fix version (all pass). With the program now monomorphic and concretely typed, this PR's callSiteTypeSubst / SMTEncoder ftvar fallback are no-ops on this test, and base's expected output is the correct merged result. Took base's `/-- info:` block verbatim; build verified.
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.
This is a temporary PR to fix the Boole tests after the merge with
main. This PR does 3 main things:sha256_compact_indexedmonomorphic, since the SMT backend does not support polymorphism (resulting from the newly produced preconditions for sequence indexing)Sequence.emptywas lost in the translation to Core, which also resulted in polymorphic precondition proof obligations that hit errors. For example,v:=Sequence.select(Sequence.empty_int, 0);generated0 < Sequence.length (Sequence.empty), which lost the information thatSequence.emptywas instantiated at typeint.