| Commit message (Expand) | Author | Age | Files | Lines |
... | |
| * | 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 |
| * | Make progress on propagating the changes | Son Ho | 2023-12-15 | 6 | -97/+72 |
| * | Minor fix | Son Ho | 2023-12-15 | 1 | -2/+2 |
| * | Make good progress on updating SymbolicToPure | Son Ho | 2023-12-15 | 5 | -42/+226 |
| * | Make progress on updating SymbolicToPure | Son Ho | 2023-12-15 | 1 | -57/+112 |
| * | Make progress on generalizing the signature information | Son Ho | 2023-12-15 | 5 | -218/+253 |
| * | Make minor modifications | Son Ho | 2023-12-15 | 2 | -79/+38 |
| * | Make progress on generated merged fwd/back functions | Son Ho | 2023-12-14 | 2 | -28/+32 |
| * | Merge remote-tracking branch 'origin/main' into son/merge_back | Son Ho | 2023-12-14 | 26 | -219/+381 |
| |\
| |/
|/| |
|
* | | Merge pull request #53 from AeneasVerif/son/casts | Son HO | 2023-12-14 | 26 | -219/+381 |
|\ \ |
|
| * | | Update the flake.lock | Son Ho | 2023-12-13 | 1 | -9/+9 |
| * | | Regenerate the test files | Son Ho | 2023-12-13 | 16 | -183/+265 |
| * | | Update the extraction to handle casts between integers/bools | Son Ho | 2023-12-13 | 9 | -27/+107 |
|/ / |
|
| * | Start updating Pure.fun_sig_info to handle merged forward and backward functions | Son Ho | 2023-12-14 | 4 | -27/+128 |
| * | Make a minor modification in a comment | Son Ho | 2023-12-13 | 1 | -1/+1 |
| * | Merge remote-tracking branch 'origin/main' into son/merge_back | Son Ho | 2023-12-13 | 1 | -3/+3 |
| |\
| |/
|/| |
|
* | | Merge pull request #52 from AeneasVerif/son/matches | Son HO | 2023-12-13 | 2 | -4/+7 |
|\ \ |
|
| * | | Update the flake.lock | Son Ho | 2023-12-13 | 1 | -3/+3 |
| | * | Update Pure.fun_sig_info | Son Ho | 2023-12-13 | 7 | -68/+129 |
| | * | Merge branch 'son/matches' into son/merge_back | Son Ho | 2023-12-13 | 1 | -1/+4 |
| | |\
| | |/
| |/| |
|
| * | | Update the interpreter to handle optional otherwise branches | Son Ho | 2023-12-13 | 1 | -1/+4 |
|/ / |
|
| * | Add the num_fwd_inputs_no_fuel_no_state field in Pure.fun_sig | Son Ho | 2023-12-13 | 3 | -5/+13 |
|/ |
|
* | Merge pull request #51 from AeneasVerif/son_merge_back2 | Son HO | 2023-12-13 | 9 | -780/+1696 |
|\ |
|
| * | Merge remote-tracking branch 'origin/main' into son_merge_back2 | Son Ho | 2023-12-13 | 2 | -336/+22 |
| |\
| |/
|/| |
|
* | | Merge pull request #50 from AeneasVerif/son/substs | Son HO | 2023-12-12 | 2 | -336/+22 |
|\ \ |
|
| * | | Update the flake.lock | Son Ho | 2023-12-12 | 1 | -21/+21 |
| * | | Move most of the substitution functions to Charon | Son Ho | 2023-12-12 | 1 | -315/+1 |
|/ / |
|
| * | Inline the let-bindings in the validity proofs | Son Ho | 2023-12-12 | 1 | -7/+40 |
| * | Fix a minor issue with the divergent encoding | Son Ho | 2023-12-12 | 1 | -53/+80 |
| * | Fix minor issues with the divergence encoding | Son Ho | 2023-12-12 | 1 | -14/+5 |
| * | Make progress on supporting higher-order divergent functions | Son Ho | 2023-12-12 | 2 | -53/+95 |
| * | Implement a map-reduce visitor for expressions and fix issues with get{M,F}Va... | Son Ho | 2023-12-12 | 1 | -31/+81 |
| * | Update the validity proofs for higher-order functions | Son Ho | 2023-12-11 | 2 | -11/+96 |
| * | Start working on higher-order examples for Diverge | Son Ho | 2023-12-11 | 4 | -218/+355 |
| * | Cleanup a bit | Son Ho | 2023-12-11 | 1 | -16/+47 |
| * | Update Diverge/Elab.lean to use the more general FixII definitions | Son Ho | 2023-12-11 | 3 | -195/+387 |