| Commit message (Expand) | Author | Age | Files | Lines |
* | Make minor modifications | Son Ho | 2022-05-09 | 1 | -4/+6 |
* | Update the termination proofs of the betree | Son Ho | 2022-05-09 | 2 | -26/+110 |
* | Update the extraction to set the fuel to 1 in the Z3 options | Son Ho | 2022-05-06 | 16 | -16/+16 |
* | Make the betree work | Son Ho | 2022-05-06 | 3 | -368/+405 |
* | Regenerate the F* for external.rs | Son Ho | 2022-05-06 | 2 | -2/+2 |
* | Regenerate the F* files for the betree | Son Ho | 2022-05-06 | 1 | -38/+73 |
* | Regenerate the F* files for external.rs | Son Ho | 2022-05-06 | 1 | -2/+14 |
* | Generate F* files for the betree | Son Ho | 2022-05-06 | 6 | -0/+2230 |
* | Update the hashmap_on_disk example | Son Ho | 2022-05-05 | 4 | -771/+240 |
* | Regenerate the F* files for external.rs | Son Ho | 2022-05-05 | 1 | -2/+17 |
* | Regenerate the F* files for hashmap_main.rs | Son Ho | 2022-05-04 | 1 | -180/+241 |
* | Regenerate the F* files for the external.rs test | Son Ho | 2022-05-04 | 2 | -7/+46 |
* | Regenerate some of the test files | Son Ho | 2022-05-01 | 2 | -9/+8 |
* | Regenerate the test files | Son Ho | 2022-04-21 | 6 | -86/+93 |
* | Regenerate the test files | Son Ho | 2022-04-20 | 4 | -148/+149 |
* | Update the evaluation of matches for the cases where the scrutinee is a | Son Ho | 2022-04-20 | 1 | -0/+14 |
* | Regenerate a test file | Son Ho | 2022-04-20 | 1 | -0/+20 |
* | Regenerate Paper.fst | Son Ho | 2022-03-05 | 1 | -0/+16 |
* | Make an update in the hash map | Son Ho | 2022-03-05 | 2 | -9/+4 |
* | Make a minor modification | Son Ho | 2022-03-04 | 1 | -1/+1 |
* | Make minor modifications to hashmap_on_disk | Son Ho | 2022-03-04 | 1 | -9/+14 |
* | Make minor modifications | Son Ho | 2022-03-04 | 1 | -5/+5 |
* | Do the proofs about hashmap_on_disk | Son Ho | 2022-03-04 | 1 | -0/+300 |
* | Generate hashmap_on_disk | Son Ho | 2022-03-04 | 8 | -0/+1733 |
* | Make minor modifications to the variable names generation | Son Ho | 2022-03-04 | 1 | -1/+1 |
* | Commit the translation of external.rs | Son Ho | 2022-03-04 | 3 | -0/+88 |
* | Change the extension of the serialized files to .llbc | Son Ho | 2022-03-03 | 1 | -25/+25 |
* | Add the betree_nll.rs test | Son Ho | 2022-02-26 | 1 | -0/+41 |
* | Update the way function names are handled | Son Ho | 2022-02-24 | 1 | -25/+25 |
* | Improve variable name generation | Son Ho | 2022-02-23 | 2 | -47/+48 |
* | Inline more let-bindings and improve formatting | Son Ho | 2022-02-23 | 3 | -107/+92 |
* | Track the generated F* files from tests/misc | Son Ho | 2022-02-23 | 2 | -0/+666 |
* | Improve the code generation by inlining more let-bindings | Son Ho | 2022-02-23 | 1 | -108/+90 |
* | More stuff for the paper + interactive mode makefile | Jonathan Protzenko | 2022-02-17 | 1 | -0/+2 |
* | Update the comments in Hashmap.Properties.fsti | Son Ho | 2022-02-14 | 1 | -6/+23 |
* | Make minor modifications | Son Ho | 2022-02-14 | 1 | -3/+4 |
* | Make minor modifications | Son Ho | 2022-02-14 | 1 | -3/+4 |
* | Add more comments and reveal in the .fsti a non-overloading lemma for | Son Ho | 2022-02-14 | 2 | -28/+101 |
* | Make minor modifications | Son Ho | 2022-02-14 | 1 | -1/+1 |
* | Add a .fsti for Hashmap.Properties | Son Ho | 2022-02-14 | 2 | -53/+296 |
* | Make minor modifications and stabilize an arithmetic proof | Son Ho | 2022-02-13 | 1 | -57/+9 |
* | Make progress on map_s | Son Ho | 2022-02-13 | 1 | -0/+6 |
* | Start working on the specs we will reveal in the .fsti | Son Ho | 2022-02-13 | 1 | -18/+78 |
* | Make minor modifications | Son Ho | 2022-02-13 | 1 | -9/+20 |
* | Add some comments | Son Ho | 2022-02-13 | 1 | -3/+12 |
* | Do more cleaning | Son Ho | 2022-02-13 | 1 | -147/+141 |
* | Do more cleanup | Son Ho | 2022-02-13 | 1 | -173/+132 |
* | Do more cleanup and work on stabilizing an arithmetic proof | Son Ho | 2022-02-13 | 1 | -42/+10 |
* | Start cleaning up | Son Ho | 2022-02-13 | 1 | -188/+20 |
* | Prove the lemma [hash_map_is_assoc_list_lem] | Son Ho | 2022-02-13 | 1 | -7/+148 |