| Commit message (Expand) | Author | Age | Files | Lines |
... | |
* | Make good progress on updating SymbolicToPure | Son Ho | 2023-02-03 | 14 | -312/+877 |
* | Add a `Loop` node in the pure AST | Son Ho | 2023-02-03 | 10 | -15/+97 |
* | Introduce new loop ids in Pure and keep track of the number of loops in a fun... | Son Ho | 2023-02-03 | 7 | -37/+69 |
* | Add loop ids to the pure functions identifiers | Son Ho | 2023-02-03 | 8 | -37/+80 |
* | Compute the SCCs of the functions to extract in Translate.ml | Son Ho | 2023-02-03 | 6 | -125/+183 |
* | Reorganize Translate.ml | Son Ho | 2023-02-03 | 1 | -165/+183 |
* | Implement ReorderDecls.ml | Son Ho | 2023-02-03 | 3 | -1/+152 |
* | Add an SCC.ml file for strongly connected components | Son Ho | 2023-02-03 | 5 | -3/+236 |
* | Make progress on Interpreter.ml | Son Ho | 2023-02-03 | 12 | -129/+293 |
* | Merge loop abs so that there is one abs per function input region group | Son Ho | 2023-02-03 | 5 | -54/+387 |
* | Make minor modifications | Son Ho | 2023-02-03 | 3 | -38/+63 |
* | Add detailed explanations in InterpreterLoops.ml | Son Ho | 2023-02-03 | 1 | -39/+405 |
* | Implement [match_ctx_with_target] | Son Ho | 2023-02-03 | 3 | -80/+635 |
* | End some borrows preemptively when computing loop joins | Son Ho | 2023-02-03 | 1 | -3/+14 |
* | Update the comments in Values and make minor modifications | Son Ho | 2023-02-03 | 7 | -120/+213 |
* | Remove the meta-value field from AMutBorrow | Son Ho | 2023-02-03 | 10 | -136/+144 |
* | Update a comment | Son Ho | 2023-02-03 | 1 | -1/+4 |
* | Remove the APrimitive variant from the avalues | Son Ho | 2023-02-03 | 7 | -25/+3 |
* | Remove the meta-values from the shared and reserved borrow values | Son Ho | 2023-02-03 | 15 | -162/+163 |
* | Make more fixes | Son Ho | 2023-02-03 | 2 | -86/+222 |
* | Make some fixes | Son Ho | 2023-02-03 | 5 | -33/+231 |
* | Make progress on checking that two environments are equivalent | Son Ho | 2023-02-03 | 3 | -177/+561 |
* | Improve some visitors and ctx_merge_regions | Son Ho | 2023-02-03 | 4 | -42/+76 |
* | Make minor modifications | Son Ho | 2023-02-03 | 2 | -1/+11 |
* | Improve merge_abstractions | Son Ho | 2023-02-03 | 3 | -6/+91 |
* | Improve the value visitors and some substitution functions | Son Ho | 2023-02-03 | 3 | -23/+54 |
* | Make more progress on the joins | Son Ho | 2023-02-03 | 1 | -142/+127 |
* | Make progress on the fixed point computation | Son Ho | 2023-02-03 | 6 | -400/+381 |
* | Make progress on the environment matches | Son Ho | 2023-02-03 | 8 | -34/+279 |
* | Make more progress | Son Ho | 2023-02-03 | 1 | -61/+102 |
* | Make progress on environment matches and joins | Son Ho | 2023-02-03 | 7 | -240/+1104 |
* | Make progress on environments matches and joins | Son Ho | 2023-02-03 | 5 | -74/+563 |
* | Start implementing support for loops | Son Ho | 2023-02-03 | 20 | -265/+1567 |
* | 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 |