Adding Zippers implementation and verification, and some benchmarks #116
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
implementation seems done, now working on the proof
|
@samuelchassot do you want to rebase and merge? |
Yes, let's do it! |
vkuncak
pushed a commit
that referenced
this pull request
Jan 18, 2025
…116) * add sbt project with plugin * move regex to an sbt project * original version * working on the memoisation * not working * add longMap + work on cache * for now issue with illegal capturing * to specific, not working but almost * working on memoised regex * working * cached version proven * working examples * new hashmap without ordering * add new lemmas in ListMaps for forall * Formally verified cache for regex * add removeUselessConcat simplification for regex + equivalence proof * add a simplification function that is sound * working on regex * as symlink * ensuring as method and not infix * implementation of Zippers (with List for Set, I'm changing to Set to try) * continue working on zippers implementation seems done, now working on the proof * working on zipper * remove chassot pacakge, obsolete * finalise merge * add hashset symlink * add a few imports * start to migrate to sets * continue replacing list by set * Move to Stainless Set, passing tests * working on zippers * working * remove useless imports * work on zippers * add some lemmas about flatmap * add getwitness for sets * working on zppier * working * change to ghost * change Context to be a class with invariant to emulate refinement types * Prove that the derivation of zippers is associative * working on zipper proof * proving stuff * proving equivalence of base cases * add generalisations of union and concat to base regex * work on regex * revert the generalised regex * add generalised union and concat as method * matchRGenUnionSpec and matchRGenConcatSpec * working on zipper proof * working on Zipper theorem * working on zipper proof * working on big proof direct induction - not working for star * working on zipper proof * working on the zipper proof * working on zipper * proved lemmaConcatZipperMatchesStringThenFindConcatDefined * working on zipper proof, almost done * working on zipper proof, almost done * done proving ZIPERRR :D * clean up * Add main regex matching function to use zipper, rename theorem * add benchmark + memoisation as extern for flatmap * add verification for memoisation * add benchmarks and some results * update CI * debug ci * debug ci * debug * ci * add memoised matching using Zipper to regex * benchmark + typo * rename for future benchmark analysis * benchmark data * remove one main test * new benchmark * typo * fix the ci --------- Co-authored-by: Samuel Chassot <samuel@tsf-476-wpa-1-098.epfl.ch>
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.
No description provided.