summaryrefslogtreecommitdiff
path: root/tests/hashmap/Hashmap.Properties.fst (unfollow)
Commit message (Expand)AuthorFilesLines
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
2022-02-12Make more progress on the proofsSon Ho1-7/+34
2022-02-12Make more progressSon Ho1-2/+12
2022-02-12Make more progress on the proofsSon Ho1-7/+83
2022-02-12Make good progress on proving the implications between the invariantsSon Ho1-73/+57
2022-02-12Add commentsSon Ho1-21/+113
2022-02-12Prove the important lemma about hash_map_move_element_s_flatSon Ho1-31/+32
2022-02-12Make progress on the move_elements proof and add some commentsSon Ho1-11/+190
2022-02-12Remove an admitSon Ho1-1/+7
2022-02-12Make good progress on the second level of refinements forSon Ho1-11/+272
2022-02-12Make minor modifications to Hashmap.Properties.fstSon Ho1-8/+12
2022-02-12Prove the refinment lemma for move_elementsSon Ho1-35/+43
2022-02-12Start working on move_elementsSon Ho1-14/+45
2022-02-12Prove the refinment lemma for hash_map_move_elements_from_listSon Ho1-20/+27
2022-02-12Start making progress on move_elements_from_listSon Ho1-24/+105
2022-02-11Perform some renamings in the hashmap exampleSon Ho1-50/+51
2022-02-11Make minor modificationsSon Ho1-188/+46
2022-02-11Prove some high-level lemmas about find after insertSon Ho1-2/+69
2022-02-11Finish the proof of [hash_map_insert_no_resize_fwd_back_le]Son Ho1-2/+36
2022-02-11Make good progress on proving the refinement lemma forSon Ho1-5/+178
2022-02-11Cleanup and reorganize the proofsSon Ho1-301/+293
2022-02-11Finish proving the lemmas about [insert_in_list_back]Son Ho1-9/+92
2022-02-11Make more progress on the proofs of hashmapSon Ho1-2/+66
2022-02-11Make good progress on the proofs of hashmapSon Ho1-90/+618
2022-02-10Make progress on the hashmap proofsSon Ho1-1/+219
2022-02-10Make progress on the proofs of HashMapSon Ho1-6/+141
2022-02-10Make minor progressSon Ho1-2/+12
2022-02-10Start working on HashMap.Properties.fstSon Ho1-0/+235
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 06:04:44 +0000