| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | Add a nix derivation for the Coq proofs | Son Ho | 2022-11-16 | 4 | -7/+25 |
* | Do not introduce match on the fuel for non-recursive functions | Son Ho | 2022-11-16 | 6 | -678/+527 |
* | Automatically generate the Makefile and _CoqProject files in the tests subdir... | Son Ho | 2022-11-16 | 17 | -15/+53 |
* | Add the aeneas-verify-fstar derivation | Son Ho | 2022-11-16 | 8 | -17/+159 |
* | Generate record field projectors for Coq | Son Ho | 2022-11-16 | 13 | -778/+843 |
* | Change the name of the generated Coq modules | Son Ho | 2022-11-16 | 12 | -43/+43 |
* | Improve formatting | Son Ho | 2022-11-16 | 19 | -682/+707 |
* | Remove some comments from Hashmap.Properties.fst | Son Ho | 2022-11-16 | 1 | -60/+0 |
* | Make minor modifications to the extraction | Son Ho | 2022-11-16 | 12 | -74/+97 |
* | Update the flake.lock | Son Ho | 2022-11-14 | 1 | -3/+3 |
* | Extract the Polonius examples in Coq | Son Ho | 2022-11-14 | 10 | -15/+2132 |
* | Generate Coq code for `hashmap` and `hashmap_on_disk` | Son Ho | 2022-11-14 | 11 | -0/+2264 |
* | Add a `-use-fuel` option | Son Ho | 2022-11-14 | 20 | -56/+333 |
* | Regenerate the files and fix the proofs | Son Ho | 2022-11-14 | 21 | -1088/+1159 |
* | Make [Result::Failure] type an [Error] parameter | Son Ho | 2022-11-14 | 15 | -62/+195 |
* | Improve the formatting of [if then else] expressions | Son Ho | 2022-11-14 | 3 | -101/+94 |
* | Reactivate the option -test-trans-unis for Coq | Son Ho | 2022-11-14 | 2 | -3/+4 |
* | Improve the formatting of the generated code | Son Ho | 2022-11-14 | 7 | -69/+107 |
* | Implement a pass to decompose nested patterns in let-bindings | Son Ho | 2022-11-14 | 5 | -59/+179 |
* | Make minor modifications | Son Ho | 2022-11-14 | 4 | -20/+1 |
* | Make good progress on the Coq backend | Son Ho | 2022-11-14 | 29 | -500/+3043 |
* | Reorganize the project to prepare for new backends | Son Ho | 2022-11-14 | 50 | -35/+36 |
* | Udpate flake.lock | Son Ho | 2022-11-11 | 1 | -3/+3 |
* | Fix some issues with the comments | Son Ho | 2022-11-11 | 8 | -22/+19 |
* | Make a minor modification | Son Ho | 2022-11-11 | 1 | -1/+1 |
* | Update the nix flake | Son Ho | 2022-11-11 | 2 | -4/+4 |
* | Make minor modifications to the tests and regenerate the .fst files | Son Ho | 2022-11-11 | 3 | -19/+19 |
* | Move the fstar files to the new backends directory | Son Ho | 2022-11-11 | 3 | -4/+8 |
* | Run `make nix update` | Son Ho | 2022-11-11 | 1 | -3/+3 |
* | Run `nix flake update` | Son Ho | 2022-11-11 | 1 | -3/+3 |
* | Update the .gitignore | Son Ho | 2022-11-11 | 1 | -0/+6 |
* | Add a `bin` folder | Son Ho | 2022-11-11 | 4 | -9/+24 |
* | Make the Nix build work | Son Ho | 2022-11-11 | 5 | -33/+101 |
* | nix | Paul-Nicolas Madelaine | 2022-11-11 | 2 | -0/+211 |
* | Make a minor modification | Son Ho | 2022-11-10 | 1 | -1/+0 |
* | Factor out the symbolic execution for the forward/backward translations | Son Ho | 2022-11-10 | 5 | -92/+77 |
* | Make a minor cleanup | Son Ho | 2022-11-10 | 10 | -61/+63 |
* | Implement a Config.ml file which groups all the global options in references | Son Ho | 2022-11-10 | 17 | -496/+392 |
* | Implement the generation of stateful backward functions (controlled by an opt... | Son Ho | 2022-11-10 | 21 | -239/+3285 |
* | Update the way function names are handled in Pure | Son Ho | 2022-11-10 | 8 | -142/+162 |
* | Reorganize branching symbolic expansions to prepare for the join operation | Son Ho | 2022-11-10 | 12 | -104/+184 |
* | Reorganize the symoblic expansions to separate the branching/non-branching ones | Son Ho | 2022-11-10 | 3 | -72/+95 |
* | Update `switch` to have a specific treatment of ADTs | Son Ho | 2022-11-10 | 9 | -196/+207 |
* | Update some comments | Son Ho | 2022-11-07 | 2 | -14/+14 |
* | Rename "inactivated borrows" to "reserved borrows" | Son Ho | 2022-11-07 | 12 | -89/+91 |
* | Add a note in the README | Son Ho | 2022-11-07 | 1 | -0/+6 |
* | Add some .mli files | Son Ho | 2022-11-07 | 16 | -381/+642 |
* | Update InterpreterBorrows | Son Ho | 2022-11-07 | 1 | -70/+35 |
* | Add ids to the dummy variables | Son Ho | 2022-11-07 | 9 | -93/+139 |
* | Remove the argument [end_borrows] from prepare_lplace and drop_outer_loans_at... | Son Ho | 2022-11-07 | 3 | -52/+24 |