A fix in Core, revealed by FStarLang/pulse#100 #3326
Merged
Conversation
This file contains 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
This was not checking that `p` is constantly true, which is unsound. See FStarLang/pulse#100.
The Core fix change the shape of some guards, and the goal is slightly different. Do some normalization to get it to how it was before and also a test without a tactic.
mtzguido
added a commit
to mtzguido/pulse
that referenced
this pull request
Jun 25, 2024
Fixed by F* patch (FStarLang/FStar#3326)
mtzguido
added a commit
to mtzguido/pulse
that referenced
this pull request
Jun 25, 2024
After fixing FStarLang#100 (see also FStarLang/FStar#3326) this now fails to match a goal of shape A.pts_to ha.tmp (reveal #(Seq.seq U8.t) ?u) since in the context we have A.pts_to ha.tmp (reveal #(Seq.lseq U8.t 32) _) To fix this, just avoid the use of `lseq` and use pure predicates instead. Requires a tiny change to the blake2b assumed API.
|
Hi @TWal, could you maybe try this PR in your projects to see if there's an impact? Asking since the only regression this caused (besides a tiny one in Pulse) was in the #2756 repro, which you filed. It looks like it could just be a bit of extra noise and only affecting the repro, but would be good if you can confirm. |
|
My projects still work with this PR! |
|
Hi, I can confirm my project also still works with this PR! |
|
Thank you both! |
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.
When checking equality via Core between
x:t{p}andt, we were completely ignoring the refinement. We need to add a guard to check that it is constantly true. Also add a local regression test.Fixes FStarLang/pulse#100