Fixing #3089, and some unifier fixes #3091
Merged
+472
−294
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
mtzguido
added a commit
to mtzguido/mitls-fstar
that referenced
this pull request
Nov 13, 2023
This stopped working after making the unifier reduce primops (FStarLang/FStar#3091), as it has no knowledge of arithmetic (except for the treatment of literals and negation). Hence, a problem like `3 =?= n+1` fails.
|
Actually it does lead to one regression: project-everest/mitls-fstar#258 |
|
I rebased the PR and removed point (2). The only failure caused by this fact is in a use of the canonicalization tactic ( |
The unifier must handle equating two concrete universe levels (among other things), as we already do for embedded terms and other constants. Make it so for all lazy terms that have a "faithful" representation.
Taken from Vale
One can use SMTQuery for that.
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.
#3089 revealed that the unifier is not using primops for its normalization to WHNF, but I believe it should. While it is using primops in some localized places (see e.g.
let equalaround line 4176), it's not the case for thewhnffunction called incompress_tprob. AddingPrimopsthere fixes the problem in #3089, but uncovers two other issues due to the extra normalization:1- We are not handling equality of universe values (causing a regression in FStar.Reflection.Typing), or other lazy opaque terms. I fixed by this making the unifier expand lazy terms to their representation, as long as this is sound, i.e. if the repr is complete. This is case for universes, fixing this issue.
2- The unifier cannot match
N(a literal) with- X(a negation, i.e. an application of op_Minus). I made this work by rewriting the problem into-N(still a literal) andX. This was uncovered by a failing tactic in Vale code. I've added an F* test for it now.Everest came back green locally.