| Commit message (Expand) | Author | Age | Files | Lines |
* | 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 |
| * | Reorganize a bit | Son Ho | 2023-12-11 | 3 | -94/+49 |
| * | Reactivate the sanity checks for the progress tactic | Son Ho | 2023-12-11 | 3 | -26/+24 |
| * | Update the progress tactic to use discrimination trees | Son Ho | 2023-12-08 | 3 | -272/+175 |
| * | Start working on a version of Diverge.FixI more suited to higher-order functions | Son Ho | 2023-12-07 | 3 | -67/+510 |
| * | Reorganize a bit | Son Ho | 2023-12-07 | 3 | -65/+94 |
| * | Update the flake.lock | Son Ho | 2023-12-07 | 1 | -3/+3 |
|/ |
|
* | Merge pull request #49 from AeneasVerif/son_merge_back | Son HO | 2023-12-07 | 24 | -427/+616 |
|\ |
|
| * | Update the flake.lock | Son Ho | 2023-12-07 | 1 | -18/+18 |
| * | Regenerate the tests | Son Ho | 2023-12-07 | 6 | -32/+110 |
| * | Fix the extraction of the empty type | Son Ho | 2023-12-07 | 1 | -12/+18 |