Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge pull request #53 from AeneasVerif/son/casts | Son HO | 2023-12-14 | 26 | -219/+381 |
|\ | | | | | Add support for casts between integers and booleans | ||||
| * | 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 |
|/ | |||||
* | Merge pull request #52 from AeneasVerif/son/matches | Son HO | 2023-12-13 | 2 | -4/+7 |
|\ | | | | | Make the otherwise branch in the LLBC match statements optional | ||||
| * | Update the flake.lock | Son Ho | 2023-12-13 | 1 | -3/+3 |
| | | |||||
| * | Update the interpreter to handle optional otherwise branches | Son Ho | 2023-12-13 | 1 | -1/+4 |
|/ | |||||
* | Merge pull request #51 from AeneasVerif/son_merge_back2 | Son HO | 2023-12-13 | 9 | -780/+1696 |
|\ | | | | | Improve the `pspec` attribute and the `divergent` encoding | ||||
| * | 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 |
|\ \ | | | | | | | Move most of the substitution functions to Charon | ||||
| * | | 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 ↵ | Son Ho | 2023-12-12 | 1 | -31/+81 |
| | | | | | | | | get{M,F}VarIds | ||||
| * | 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 |
|\ | | | | | Allow the extraction of structures as tuples | ||||
| * | 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 |
| | | |||||
| * | Update the micro passes to inline deconstruction of tuples with one field | Son Ho | 2023-12-07 | 1 | -6/+34 |
| | | |||||
| * | Fix minor issues when extracting a structure with one field as a tuple | Son Ho | 2023-12-07 | 2 | -21/+45 |
| | | |||||
| * | Use a better syntax when extracting tuple types (structures with unnamed fields) | Son Ho | 2023-12-07 | 10 | -199/+347 |
| | | |||||
| * | Remove the type sv_kind ("symbolic value kind") | Son Ho | 2023-12-05 | 8 | -158/+63 |
| | | |||||
* | | Merge pull request #38 from AeneasVerif/son_fixes2 | Son HO | 2023-12-05 | 3 | -9/+14 |
|\ \ | |/ |/| | Simplify and add some lemmas | ||||
| * | Merge branch 'main' into son_fixes2 | Son Ho | 2023-12-05 | 231 | -20668/+36799 |
| |\ | |/ |/| | |||||
* | | Merge pull request #48 from AeneasVerif/son_closures | Son HO | 2023-12-05 | 37 | -891/+1315 |
|\ \ | | | | | | | Prepare support for function pointers and closures | ||||
| * | | Update the flake.lock | Son Ho | 2023-12-05 | 1 | -36/+36 |
| | | | |||||
| * | | Print error messages when the command line arguments are invalid | Son Ho | 2023-12-05 | 1 | -10/+40 |
| | | | |||||
| * | | Fix a minor issue with the use of const generics | Son Ho | 2023-12-05 | 6 | -13/+40 |
| | | | |||||
| * | | Update following changes in Charon | Son Ho | 2023-12-05 | 32 | -826/+1176 |
| | | | |||||
| * | | Update the code following changes in the NameMatcher | Son Ho | 2023-11-29 | 4 | -6/+23 |
|/ / | |||||
* | | Merge pull request #39 from AeneasVerif/afromher_shifts | Son HO | 2023-11-29 | 26 | -95/+2000 |
|\ \ | | | | | | | Add support for bitshifts | ||||
| * | | Update the flake.lock | Son Ho | 2023-11-29 | 1 | -9/+9 |
| | | | |||||
| * | | Regenerate the other files | Son Ho | 2023-11-29 | 14 | -56/+1570 |
| | | | |||||
| * | | Generate the Bitwise test files | Son Ho | 2023-11-29 | 3 | -0/+107 |
| | | | |||||
| * | | Fix a minor issue with the extraction | Son Ho | 2023-11-29 | 1 | -4/+5 |
| | | | |||||
| * | | Add support for more bitwise operations and update the extraction | Son Ho | 2023-11-29 | 6 | -28/+302 |
| | | | |||||
| * | | Merge branch 'main' into afromher_shifts | Son Ho | 2023-11-29 | 228 | -20545/+34347 |
| |\ \ | |/ / |/| | |