summaryrefslogtreecommitdiff
path: root/tests/hashmap (unfollow)
Commit message (Expand)AuthorFilesLines
2022-09-27Fix MakefilesJonathan Protzenko1-11/+10
2022-09-22Regenerate the translated filesSon Ho1-1/+1
2022-08-10Corrected translation without using functions, remaining bug in hashmap trans...Sidney Congard3-10/+17
2022-06-27Update the MakefilesSon Ho1-4/+1
2022-06-20Add makefiles to test the F* filesSon Ho1-0/+51
2022-06-20Remove a commentSon Ho1-189/+0
2022-05-15Regenerate the F* filesSon Ho2-36/+33
2022-05-15Treat integer casts in a general mannerSon Ho1-0/+4
2022-05-06Update the extraction to set the fuel to 1 in the Z3 optionsSon Ho3-3/+3
2022-05-01Regenerate some of the test filesSon Ho1-4/+2
2022-04-21Regenerate the test filesSon Ho1-27/+29
2022-04-20Regenerate the test filesSon Ho1-47/+48
2022-03-05Make an update in the hash mapSon Ho1-4/+2
2022-03-04Generate hashmap_on_diskSon Ho1-0/+62
2022-03-03Change the extension of the serialized files to .llbcSon Ho1-25/+25
2022-02-24Update the way function names are handledSon Ho1-25/+25
2022-02-23Improve variable name generationSon Ho1-39/+40
2022-02-23Inline more let-bindings and improve formattingSon Ho1-72/+68
2022-02-23Improve the code generation by inlining more let-bindingsSon Ho1-108/+90
2022-02-14Update the comments in Hashmap.Properties.fstiSon Ho1-6/+23
2022-02-14Make minor modificationsSon Ho1-3/+4
2022-02-14Make minor modificationsSon Ho1-3/+4
2022-02-14Add more comments and reveal in the .fsti a non-overloading lemma forSon Ho2-28/+101
2022-02-14Make minor modificationsSon Ho1-1/+1
2022-02-14Add a .fsti for Hashmap.PropertiesSon Ho2-53/+296
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 Ho3-43/+376
2022-02-13Start tracking the automatically generated/copied files for hashmapSon Ho3-0/+963
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