Much cleaner strings with index_extensionality (and for Seq and ImmutableArray) that does not create a new eq. #3598
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
…ableArray) that does not create a new eq.
|
Interestingly this checkin left around some file references in my next branch (from master) that appeared in test. What's the right way to clean up test? make clean; make -j20; make -j20 ci did not do the job. |
nikswamy
reviewed
Dec 12, 2024
ulib/FStar.String.Base.fsti
Outdated
| (forall (i: nat{i < pos}). index s1 i = index s2 i)) | ||
|
|
||
| let streq_upto_min s1 s2 (pos: int{pos < (min (strlen s1) (strlen s2))}) = | ||
| (forall (i: nat{i < (pos - 1)}). index s1 i = index s2 i) |
There was a problem hiding this comment.
The minus 1 here looks suspicious.
nikswamy
reviewed
Dec 12, 2024
ulib/FStar.String.Match.fsti
Outdated
| Tot (o : (option (pos: nat{pos <= (min (strlen s1) (strlen s2))})) { | ||
| (None? o ==> strlen s1 = strlen s2 /\ streq_upto s1 s2 (strlen s1)) /\ | ||
| (Some? o ==> | ||
| streq_upto_min s1 s2 ((Some?.v o) - 1) /\ |
There was a problem hiding this comment.
Especially given an additional -1 here
… in streq_upto_min. Did not affect the proofs.
|
Thank you it was indeed bogus to use a -1 there when pos means the index (not exclusive). |
|
And now, no -1s. |
|
I take that back, build issues not detecting a bug, the LSP was passing things that the command line is catching. I'll get this fixed. |
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.
Here is a much cleaner FStar.Strings.* which proves index_extensionality instead of defining a new eq.
Once I had it there, I also proved it for Seq and ImmutableArray.
The biggest question that I have, due to FStar.String.fsti being implemented only in FStar_String.ml I had to make
this FStar.String.{Base,Properties} which must be separately included ONLY for the new lemmas and functions.
FStar.String.Match contains first_diff as we are sure to end up adding some string matching someday.
There are two test files, one validation time, Test.FStar.String and one runtime that mere prints Test.FStar.String.TestMain
as with interfaces some functionality can not be tested at assert time. When Final is ready we might move the runtime tests
to that, once it is accepted.