Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Fix a minor issue | Son Ho | 2024-03-18 | 1 | -1/+3 |
| | |||||
* | Regenerate the test files | Son Ho | 2024-03-18 | 6 | -66/+297 |
| | |||||
* | Update extract_trait_impl | Son Ho | 2024-03-18 | 1 | -7/+23 |
| | |||||
* | Fix the extraction of trait constants | Son Ho | 2024-03-18 | 2 | -35/+22 |
| | |||||
* | Regenerate the constants tests and update Primitives/Base.lean | Son Ho | 2024-03-18 | 4 | -55/+101 |
| | |||||
* | Make good progress on adding generics to global constants | Son Ho | 2024-03-18 | 8 | -47/+172 |
| | |||||
* | Merge pull request #91 from AeneasVerif/son/hax | Son HO | 2024-03-17 | 16 | -101/+75 |
|\ | | | | | Prepare the merge in hax | ||||
| * | Update the flake.lock | Son Ho | 2024-03-17 | 1 | -21/+21 |
| | | |||||
| * | Fix a minor issue | Son Ho | 2024-03-17 | 1 | -1/+1 |
| | | |||||
| * | Make minor updates | Son Ho | 2024-03-17 | 3 | -7/+14 |
| | | |||||
| * | Fix a small issue ollowing updates in Charon | Son Ho | 2024-03-17 | 1 | -3/+8 |
| | | |||||
| * | Update following changes in Charon | Son Ho | 2024-03-17 | 11 | -72/+34 |
|/ | |||||
* | Merge pull request #88 from AeneasVerif/son/clashes | Son HO | 2024-03-11 | 37 | -703/+825 |
|\ | | | | | Improve the name generation for code extraction | ||||
| * | Update the flake.lock | Son Ho | 2024-03-11 | 1 | -12/+12 |
| | | |||||
| * | Regenerate the test files | Son Ho | 2024-03-11 | 14 | -244/+227 |
| | | |||||
| * | Simplify the generated names | Son Ho | 2024-03-11 | 1 | -14/+25 |
| | | |||||
| * | Update the generated files | Son Ho | 2024-03-11 | 15 | -380/+389 |
| | | |||||
| * | Update tests/Makefile | Son Ho | 2024-03-11 | 1 | -1/+1 |
| | | |||||
| * | Update the generation of names | Son Ho | 2024-03-11 | 7 | -39/+57 |
| | | |||||
| * | Update a builtin name | Son Ho | 2024-03-11 | 1 | -1/+1 |
| | | |||||
| * | Update the builtin name patterns | Son Ho | 2024-03-10 | 1 | -23/+66 |
| | | |||||
| * | Update the name generation and add CLI to print external pat names | Son Ho | 2024-03-10 | 7 | -48/+106 |
|/ | |||||
* | Merge pull request #85 from AeneasVerif/son/fix_loops3 | Son HO | 2024-03-09 | 28 | -350/+1185 |
|\ | | | | | Fix some issues with the loops | ||||
| * | Update the flake.lock | Son Ho | 2024-03-09 | 1 | -24/+24 |
| | | |||||
| * | Regenerate the test files | Son Ho | 2024-03-09 | 10 | -0/+420 |
| | | |||||
| * | Fix an issue with the divergent encoding | Son Ho | 2024-03-09 | 1 | -3/+27 |
| | | |||||
| * | Fix some issues | Son Ho | 2024-03-08 | 2 | -9/+10 |
| | | |||||
| * | Add some comments | Son Ho | 2024-03-08 | 2 | -9/+12 |
| | | |||||
| * | Fix an issue in PureMicroPasses.filter_loop_inputs | Son Ho | 2024-03-08 | 1 | -13/+43 |
| | | |||||
| * | Simplify the contexts before symbolically evaluating loops | Son Ho | 2024-03-08 | 4 | -2/+137 |
| | | |||||
| * | Fix a last issue | Son Ho | 2024-03-08 | 2 | -51/+110 |
| | | |||||
| * | Fix an issue with the loops | Son Ho | 2024-03-08 | 1 | -1/+7 |
| | | |||||
| * | Make progress on fixing the loops | Son Ho | 2024-03-08 | 8 | -31/+70 |
| | | |||||
| * | Fix a small issue with the loops | Son Ho | 2024-03-08 | 2 | -7/+19 |
| | | |||||
| * | Fix some issues with the loops | Son Ho | 2024-03-08 | 3 | -140/+206 |
| | | |||||
| * | Do not fail in end_abstraction_aux if the abs disappeared | Son Ho | 2024-03-08 | 2 | -64/+80 |
| | | |||||
| * | Add logging information | Son Ho | 2024-03-08 | 3 | -0/+24 |
| | | |||||
| * | Update Print.ml | Son Ho | 2024-03-08 | 1 | -8/+8 |
|/ | |||||
* | Merge pull request #83 from AeneasVerif/son/backs | Son HO | 2024-03-08 | 76 | -18929/+705 |
|\ | | | | | Remove the option to split the forward/backward functions | ||||
| * | Update the workers | Son Ho | 2024-03-08 | 1 | -1/+0 |
| | | |||||
| * | Update the flake.nix | Son Ho | 2024-03-08 | 1 | -14/+5 |
| | | |||||
| * | Remove the split test files for F* | Son Ho | 2024-03-08 | 55 | -16239/+0 |
| | | |||||
| * | Update the Makefile and remove the split files for F* | Son Ho | 2024-03-08 | 5 | -952/+4 |
| | | |||||
| * | Make progress on propagating the changes | Son Ho | 2024-03-08 | 14 | -949/+259 |
| | | |||||
| * | Remove the option to split fwd/back functions and update SymbolicToPure | Son Ho | 2024-03-08 | 5 | -776/+439 |
|/ | |||||
* | Merge pull request #82 from AeneasVerif/son/switch | Son HO | 2024-03-08 | 20 | -173/+352 |
|\ | | | | | Improve tuple projections and matches over integers in Lean | ||||
| * | Update the code generated for tuple projectors | Son Ho | 2024-03-08 | 4 | -19/+48 |
| | | |||||
| * | Fix tuple indexing for Lean backend | Zyad Hassan | 2024-03-08 | 3 | -6/+35 |
| | | |||||
| * | Update the generation of constant bodies for Lean | Son Ho | 2024-03-08 | 6 | -28/+26 |
| | | |||||
| * | Update the tuples syntax | Son Ho | 2024-03-08 | 1 | -1/+3 |
| | |