summaryrefslogtreecommitdiff
path: root/tests/fstar-split/hashmap/Hashmap.Properties.fst (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-22Regenerate the test files and add the fstar-split testsSon Ho1-0/+0
2023-11-09Update the failing proofsSon Ho1-824/+824
2023-02-03Update the hashmap and regenerateSon Ho1-10/+9
2023-02-03Fix an issue with the names of the loop decreases clausesSon Ho1-8/+8
2023-02-03Improve the order of the loop input parametersSon Ho1-14/+14
2023-02-03Regenerate the hashmap code and update the proofsSon Ho1-20/+20
2022-11-16Remove some comments from Hashmap.Properties.fstSon Ho1-60/+0
2022-11-14Regenerate the files and fix the proofsSon Ho1-130/+130
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-0/+0
2022-06-20Remove a commentSon Ho1-189/+0
2022-02-14Add more comments and reveal in the .fsti a non-overloading lemma forSon Ho1-18/+57
2022-02-14Add a .fsti for Hashmap.PropertiesSon Ho1-53/+82
2022-02-13Make minor modifications and stabilize an arithmetic proofSon Ho1-57/+9
2022-02-13Make progress on map_sSon Ho1-0/+6
2022-02-13Start working on the specs we will reveal in the .fstiSon Ho1-18/+78
2022-02-13Make minor modificationsSon Ho1-9/+20
2022-02-13Add some commentsSon Ho1-3/+12
2022-02-13Do more cleaningSon Ho1-147/+141
2022-02-13Do more cleanupSon Ho1-173/+132
2022-02-13Do more cleanup and work on stabilizing an arithmetic proofSon Ho1-42/+10
2022-02-13Start cleaning upSon Ho1-188/+20
2022-02-13Prove the lemma [hash_map_is_assoc_list_lem]Son Ho1-7/+148
2022-02-13State and prove the final lemma about remove'backSon Ho1-0/+23
2022-02-13Make good progress on the invariant proofs for remove'backSon Ho1-18/+132
2022-02-13Prove the refinement lemma for remove'backSon Ho1-12/+137
2022-02-13Prove the lemma for remove'fwdSon Ho1-13/+90
2022-02-13Make minor modifications, cleanup and fix a proofSon Ho1-20/+115
2022-02-13Make minor modificationsSon Ho1-4/+4
2022-02-13Prove the lemma for [get_mut'back]Son Ho1-1/+33
2022-02-13Add an invariant proof for insert_no_fail_sSon Ho1-24/+36
2022-02-13Make progress on get_mut'backSon Ho1-11/+20
2022-02-13Cleanup a bitSon Ho1-6/+4
2022-02-13Add [contains_key], make progress on the proofs for [contains_key],Son Ho1-43/+329
2022-02-13Make a minor modificationSon Ho1-0/+2
2022-02-13Make minor modificationsSon Ho1-0/+6
2022-02-13Prove the lemmas for [insert]Son Ho1-0/+62
2022-02-13Make more progress on the proofsSon Ho1-3/+26
2022-02-13Make more progress on the proofsSon Ho1-4/+41
2022-02-13Make more progress on the proof of try_resizeSon Ho1-2/+25
2022-02-13Make more progress on the proofs of try_resizeSon Ho1-2/+16
2022-02-13Make good progress on the lemmas for try_resizeSon Ho1-82/+93
2022-02-12Make progress on the hash map proofsSon Ho1-2/+75
2022-02-12Start working on try_resizeSon Ho1-2/+103
2022-02-12Finish another proofSon Ho1-9/+83
2022-02-12Update some commentsSon Ho1-3/+3
2022-02-12Add some commentsSon Ho1-1/+8
2022-02-12Add some commentsSon Ho1-22/+23
2022-02-12Make minor updates and fix an unstable proofSon Ho1-28/+85
2022-02-12Make minor modificationsSon Ho1-0/+1
2022-02-12Make more progress on the proofsSon Ho1-4/+12
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 03:09:00 +0000