Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 | ||||
| * | Make a minor modification to the README | Son Ho | 2024-01-31 | 1 | -2/+2 |
| | | |||||
| * | Add instructions on using files generated by the Lean backend | Zyad Hassan | 2024-01-29 | 1 | -1/+11 |
|/ | |||||
* | Merge pull request #66 from AeneasVerif/son/lean | Son HO | 2024-01-27 | 5 | -92/+174 |
|\ | | | | | Improve the Lean backend | ||||
| * | Add some lemmas to the Lean backend | Son Ho | 2024-01-27 | 1 | -4/+14 |
| | | |||||
| * | Fix a minor issue with the progress tactic | Son Ho | 2024-01-27 | 2 | -82/+112 |
| | | |||||
| * | Improve the Lean backend | Son Ho | 2024-01-26 | 5 | -10/+52 |
|/ | |||||
* | Merge pull request #65 from AeneasVerif/son/fix_loops | Son HO | 2024-01-25 | 21 | -526/+886 |
|\ | | | | | Fix an issue with loops | ||||
| * | Update a decreases clause | Son Ho | 2024-01-25 | 1 | -0/+5 |
| | | |||||
| * | Make a minor modification | Son Ho | 2024-01-25 | 1 | -2/+2 |
| | | |||||
| * | Update the flake.lock | Son Ho | 2024-01-25 | 1 | -24/+24 |
| | | |||||
| * | Regenerate the files | Son Ho | 2024-01-25 | 13 | -314/+379 |
| | | |||||
| * | Fix a minor issue when values are moved in the loops | Son Ho | 2024-01-25 | 6 | -188/+478 |
|/ | |||||
* | Merge pull request #64 from AeneasVerif/son/merge_back | Son HO | 2023-12-23 | 162 | -10694/+20870 |
|\ | | | | | Merge the forward/backward functions | ||||
| * | Update the Makefile | Son Ho | 2023-12-23 | 1 | -1/+6 |
| | | |||||
| * | Update the flake.lock | Son Ho | 2023-12-23 | 1 | -21/+21 |
| | | |||||
| * | Fix an issue in External_FunsExternal.v | Son Ho | 2023-12-23 | 1 | -15/+3 |
| | | |||||
| * | Fix an issue when deconstructing tuples in Coq | Son Ho | 2023-12-23 | 3 | -7/+10 |
| | | |||||
| * | Regenerate the files | Son Ho | 2023-12-23 | 35 | -327/+183 |
| | | |||||
| * | Update the micro-passes | Son Ho | 2023-12-23 | 1 | -77/+94 |
| | | |||||
| * | Improve the micro passes to eliminate pattern `let f := fun x => g x` | Son Ho | 2023-12-23 | 4 | -54/+67 |
| | | |||||
| * | Update the flake.nix and the ci.yml | Son Ho | 2023-12-23 | 2 | -1/+16 |
| | | |||||
| * | Fix a minor issue in the Lean tests | Son Ho | 2023-12-23 | 1 | -14/+3 |
| | | |||||
| * | Update the proof of the hashmap in Lean | Son Ho | 2023-12-23 | 1 | -100/+44 |
| | | |||||
| * | Regenerate the test files and add the fstar-split tests | Son Ho | 2023-12-22 | 106 | -8265/+15092 |
| | | |||||
| * | Fix minor issues | Son Ho | 2023-12-22 | 6 | -38/+186 |
| | | |||||
| * | Fix the models for core::mem::replace | Son Ho | 2023-12-22 | 3 | -3/+3 |
| | | |||||
| * | Update the computation of the effect info for the loops | Son Ho | 2023-12-22 | 1 | -46/+95 |
| | | |||||
| * | Fix the output type of the loops backward functions | Son Ho | 2023-12-22 | 5 | -46/+65 |
| | | |||||
| * | Fix a minor issue with the extraction of loops when merging the fwd/back ↵ | Son Ho | 2023-12-22 | 1 | -11/+19 |
| | | | | | | | | functions | ||||
| * | Annotate the bound vars in the lambdas for Coq | Son Ho | 2023-12-22 | 3 | -293/+267 |
| | | |||||
| * | Start pushing files from the fstar-split test folder | Son Ho | 2023-12-22 | 6 | -0/+1637 |
| | | |||||
| * | Fix a minor extraction issue | Son Ho | 2023-12-22 | 1 | -1/+1 |
| | | |||||
| * | Regenerate some of the NoNestedBorrows tests | Son Ho | 2023-12-22 | 3 | -546/+474 |
| | |