| Commit message (Expand) | Author | Age | Files | Lines |
... | |
| * | Update the Makefile | Son Ho | 2023-12-23 | 1 | -1/+6 |
| * | Update the flake.lock | Son Ho | 2023-12-23 | 1 | -21/+21 |
| * | Fix an issue in External_FunsExternal.v | Son Ho | 2023-12-23 | 1 | -15/+3 |
| * | Fix an issue when deconstructing tuples in Coq | Son Ho | 2023-12-23 | 3 | -7/+10 |
| * | Regenerate the files | Son Ho | 2023-12-23 | 35 | -327/+183 |
| * | Update the micro-passes | Son Ho | 2023-12-23 | 1 | -77/+94 |
| * | Improve the micro passes to eliminate pattern `let f := fun x => g x` | Son Ho | 2023-12-23 | 4 | -54/+67 |
| * | Update the flake.nix and the ci.yml | Son Ho | 2023-12-23 | 2 | -1/+16 |
| * | Fix a minor issue in the Lean tests | Son Ho | 2023-12-23 | 1 | -14/+3 |
| * | Update the proof of the hashmap in Lean | Son Ho | 2023-12-23 | 1 | -100/+44 |
| * | Regenerate the test files and add the fstar-split tests | Son Ho | 2023-12-22 | 106 | -8265/+15092 |
| * | Fix minor issues | Son Ho | 2023-12-22 | 6 | -38/+186 |
| * | Fix the models for core::mem::replace | Son Ho | 2023-12-22 | 3 | -3/+3 |
| * | Update the computation of the effect info for the loops | Son Ho | 2023-12-22 | 1 | -46/+95 |
| * | Fix the output type of the loops backward functions | Son Ho | 2023-12-22 | 5 | -46/+65 |
| * | Fix a minor issue with the extraction of loops when merging the fwd/back func... | Son Ho | 2023-12-22 | 1 | -11/+19 |
| * | Annotate the bound vars in the lambdas for Coq | Son Ho | 2023-12-22 | 3 | -293/+267 |
| * | Start pushing files from the fstar-split test folder | Son Ho | 2023-12-22 | 6 | -0/+1637 |
| * | Fix a minor extraction issue | Son Ho | 2023-12-22 | 1 | -1/+1 |
| * | Regenerate some of the NoNestedBorrows tests | Son Ho | 2023-12-22 | 3 | -546/+474 |
| * | Add an option to split the fwd/back functions and fix a minor issue | Son Ho | 2023-12-22 | 4 | -10/+33 |
| * | Update the library for Coq | Son Ho | 2023-12-22 | 1 | -74/+42 |
| * | Update the library for F* | Son Ho | 2023-12-22 | 7 | -3/+895 |
| * | Update the Lean standard library | Son Ho | 2023-12-22 | 5 | -81/+38 |
| * | Slightly update the formatting of the do blocks | Son Ho | 2023-12-22 | 1 | -24/+26 |
| * | Fix an issue when merging the fwd/back functions of trait methods | Son Ho | 2023-12-22 | 4 | -19/+57 |
| * | Improve the pure micro passes | Son Ho | 2023-12-21 | 2 | -3/+46 |
| * | Fix issues when extracting stateful functions | Son Ho | 2023-12-21 | 2 | -41/+40 |
| * | Fix several issues | Son Ho | 2023-12-21 | 3 | -81/+151 |
| * | Improve PureMicroPasses.filter_useless to simplify the matches | Son Ho | 2023-12-21 | 1 | -1/+14 |
| * | Use indices starting at 1 to make variable names unique at code gen | Son Ho | 2023-12-21 | 1 | -1/+1 |
| * | Implement a micro-pass to simplify the let-bindings | Son Ho | 2023-12-21 | 1 | -0/+78 |
| * | Simplify the type of the merged fwd/back functions | Son Ho | 2023-12-21 | 5 | -46/+153 |
| * | Update the formatting of comments | Son Ho | 2023-12-21 | 1 | -8/+6 |
| * | Filter the useless backward functions | Son Ho | 2023-12-21 | 1 | -75/+145 |
| * | Update SymbolicToPure.ml for the loops | Son Ho | 2023-12-21 | 1 | -96/+125 |
| * | Remove some asserts which are now useless | Son Ho | 2023-12-21 | 3 | -8/+4 |
| * | Fix some issues in SymbolicToPure | Son Ho | 2023-12-21 | 1 | -25/+26 |
| * | Fix a minor issue | Son Ho | 2023-12-21 | 1 | -2/+5 |
| * | Make good progress on merging the fwd/back functions | Son Ho | 2023-12-21 | 8 | -87/+274 |
| * | Reset Config.return_back_funs to false | Son Ho | 2023-12-19 | 1 | -1/+1 |
| * | Remove SymbolicToPure.bs_ctx.loop_backward_outputs | Son Ho | 2023-12-19 | 2 | -33/+15 |
| * | Simplify SymbolicToPure.bs_ctx.{backward_outputs, loop_backward_outputs} | Son Ho | 2023-12-19 | 2 | -100/+70 |
| * | Remove the backwards field from SymbolicToPure.call_info | Son Ho | 2023-12-18 | 1 | -15/+5 |
| * | Fix a minor mistake in SymbolicToPure | Son Ho | 2023-12-18 | 3 | -11/+15 |
| * | Add some comments | Son Ho | 2023-12-18 | 1 | -16/+31 |
| * | Rename some definitions | Son Ho | 2023-12-18 | 15 | -140/+139 |
| * | Do not register the names of the back funs if they are merged with the fwd funs | Son Ho | 2023-12-18 | 1 | -3/+8 |
| * | Update the README | Son Ho | 2023-12-18 | 1 | -1/+2 |
| * | Make progress on updating the code | Son Ho | 2023-12-15 | 3 | -200/+134 |