Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
| | | |||||
| * | Update the tuples notations | Son Ho | 2024-03-08 | 3 | -51/+81 |
| | | |||||
| * | Remove some comments | Son Ho | 2024-03-08 | 1 | -31/+0 |
| | | |||||
| * | Update the handling of notations like #u32 or #isize | Son Ho | 2024-03-08 | 4 | -70/+104 |
| | | |||||
| * | Regenerate the test files | Son Ho | 2024-03-08 | 5 | -46/+46 |
| | | |||||
| * | Update the code generation | Son Ho | 2024-03-08 | 2 | -7/+6 |
| | | |||||
| * | Update the notation for heterogeneous negation | Son Ho | 2024-03-08 | 1 | -3/+12 |
| | | |||||
| * | Introduce a notation for constant scalars in match patterns | Son Ho | 2024-03-07 | 1 | -0/+29 |
| | | |||||
| * | Add a notation for tuple field accesses in Lean | Son Ho | 2024-03-07 | 1 | -0/+51 |
|/ | |||||
* | Merge pull request #73 from AeneasVerif/son/demo | Son HO | 2024-02-11 | 17 | -220/+3696 |
|\ | | | | | Add some demo files | ||||
| * | Remove a file which shouldn't have been added | Son Ho | 2024-02-09 | 1 | -49/+0 |
| | | |||||
| * | Cleanup a bit Scalar.lean | Son Ho | 2024-02-09 | 1 | -198/+198 |
| | | |||||
| * | Update the flake.lock | Son Ho | 2024-02-09 | 1 | -21/+21 |
| | | |||||
| * | Add some missing files | Son Ho | 2024-02-09 | 4 | -0/+128 |
| | | |||||
| * | Add some demo files | Son Ho | 2024-02-09 | 12 | -1/+3398 |
|/ | |||||
* | Merge pull request #68 from AeneasVerif/son/update_lean | Son HO | 2024-02-03 | 45 | -1246/+851 |
|\ | | | | | Update Lean to v4.6.0-rc1 | ||||
| * | Fix minor issues | Son Ho | 2024-02-03 | 2 | -10/+10 |
| | | |||||
| * | Update the flake.lock | Son Ho | 2024-02-02 | 1 | -18/+18 |
| | | |||||
| * | Update the .gitignore files | Son Ho | 2024-02-02 | 2 | -2/+4 |
| | | |||||
| * | Rename and regenerate some files | Son Ho | 2024-02-02 | 22 | -960/+516 |
| | | |||||
| * | Make progress on fixing the tests | Son Ho | 2024-02-02 | 1 | -13/+13 |
| | | |||||
| * | Start fixing the tests | Son Ho | 2024-02-02 | 9 | -83/+101 |
| | | |||||
| * | Fix more proofs | Son Ho | 2024-02-02 | 3 | -13/+16 |
| | | |||||
| * | Fix more proofs | Son Ho | 2024-02-02 | 1 | -56/+55 |
| | | |||||
| * | Update lean to v4.6.0-rc1 and start fixing the proofs | Son Ho | 2024-02-02 | 8 | -93/+120 |
|/ | |||||
* | Merge pull request #67 from zhassan-aws/lean-steps | Son HO | 2024-02-01 | 1 | -1/+11 |
|\ | | | | | Add instructions on using files generated by the Lean backend |