Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
| |\ \ | |/ / |/| | | |||||
* | | | Merge pull request #47 from AeneasVerif/son_panics | Son HO | 2023-11-29 | 8 | -134/+155 |
|\ \ \ | | | | | | | | | Update following some changes in Charon | ||||
| * | | | Update flake.lock | Son Ho | 2023-11-29 | 1 | -30/+30 |
| | | | | |||||
| * | | | Regenerate the tests | Son Ho | 2023-11-29 | 4 | -89/+125 |
| | | | | |||||
| * | | | Regenerate the test files | Son Ho | 2023-11-29 | 3 | -15/+0 |
|/ / / | |||||
* | | | Merge pull request #46 from AeneasVerif/son_improves | Son HO | 2023-11-28 | 94 | -521/+917 |
|\ \ \ | | | | | | | | | Minor improvements for the extraction | ||||
| * | | | Update the flake.lock | Son Ho | 2023-11-27 | 1 | -18/+18 |
| | | | | |||||
| * | | | Fix the issues with the cross-references for OCaml doc | Son Ho | 2023-11-27 | 16 | -35/+35 |
| | | | | |||||
| * | | | Update a comment | Son Ho | 2023-11-27 | 1 | -1/+2 |
| | | | | |||||
| * | | | Update the way the Primitives file is copied | Son Ho | 2023-11-27 | 1 | -13/+20 |
| | | | | |||||
| * | | | Do not activate the sanity (invariant) checks by default | Son Ho | 2023-11-27 | 8 | -19/+16 |
| | | | | |||||
| * | | | Generate a dedicated file for the external types | Son Ho | 2023-11-27 | 46 | -90/+355 |
| | | | | |||||
| * | | | Update the generation of files for external definitions and regenerate the tests | Son Ho | 2023-11-27 | 21 | -33/+158 |
| | | | | |||||
| * | | | Regenerate the files | Son Ho | 2023-11-24 | 12 | -282/+259 |
| | | | | |||||
| * | | | Add the alloc::string::String type in the builtins | Son Ho | 2023-11-24 | 3 | -5/+16 |
| | | | | |||||
| * | | | Update a comment | Son Ho | 2023-11-24 | 1 | -2/+3 |
| | | | | |||||
| * | | | Make a minor fix | Son Ho | 2023-11-24 | 1 | -1/+1 |
| | | | | |||||
| * | | | Update some assumed type names/variants | Son Ho | 2023-11-24 | 2 | -34/+41 |
| | | | | |||||
| * | | | Improve the error messages for some name collisions | Son Ho | 2023-11-24 | 1 | -2/+4 |
| | | | | |||||
| * | | | Make a minor update in ExtractName.pattern_to_extract_name | Son Ho | 2023-11-24 | 1 | -1/+4 |
|/ / / |