Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Add Lean extraction of shl/shr | Aymeric Fromherz | 2023-09-22 | 1 | -1/+3 |
| | |||||
* | Allow bitshifts with any pair of integer types | Aymeric Fromherz | 2023-09-22 | 1 | -1/+5 |
| | |||||
* | Add support for Shl/Shr typechecking in InterpreterExpressions | Aymeric Fromherz | 2023-09-22 | 1 | -1/+4 |
| | |||||
* | Merge pull request #37 from AeneasVerif/son_tuto | Son HO | 2023-09-18 | 8 | -71/+691 |
|\ | | | | | Tutorial for the Lean backend | ||||
| * | Update the README | Son Ho | 2023-09-18 | 1 | -0/+2 |
| | | |||||
| * | Cleanup the tutorial a bit | Son Ho | 2023-09-18 | 1 | -80/+110 |
| | | |||||
| * | Add notations for the Isize.ofInt, etc. | Son Ho | 2023-09-18 | 1 | -0/+16 |
| | | |||||
| * | Make minor modifications to the tutorial | Son Ho | 2023-09-18 | 1 | -3/+2 |
| | | |||||
| * | Add arithmetic lemmas in Scalar.lean | Son Ho | 2023-09-18 | 1 | -12/+179 |
| | | |||||
| * | Make progress on the tutorial | Son Ho | 2023-09-18 | 1 | -3/+66 |
| | | |||||
| * | Start writing a tutorial | Son Ho | 2023-09-18 | 2 | -0/+298 |
| | | |||||
| * | Improve scalar_tac | Son Ho | 2023-09-18 | 3 | -56/+36 |
| | | |||||
| * | Fix an issue when loading the saved theorem maps for the progress tactic | Son Ho | 2023-09-18 | 2 | -3/+68 |
|/ | |||||
* | Merge pull request #36 from AeneasVerif/update_lean | Son HO | 2023-09-14 | 11 | -69/+95 |
|\ | | | | | Update the version of Lean and fix a bug in the progress tactic | ||||
| * | Fix the hashmap proofs in Lean | Son Ho | 2023-09-14 | 5 | -29/+41 |
| | | |||||
| * | Fix panic issues with the progress tactic | Son Ho | 2023-09-14 | 1 | -3/+5 |
| | | |||||
| * | Update to Lean 4.0.0 and fix some broken proofs | Son Ho | 2023-09-14 | 7 | -38/+50 |
|/ | |||||
* | Merge pull request #34 from AeneasVerif/son_update_rustc | Son HO | 2023-08-09 | 18 | -41/+41 |
|\ | | | | | Update rustc to nightly-2023-06-02 | ||||
| * | Update the nix flake | Son Ho | 2023-08-09 | 1 | -18/+18 |
| | | |||||
| * | Update the nix flake and regenerate the code | Son Ho | 2023-08-09 | 18 | -26/+26 |
| | | |||||
* | | Merge pull request #33 from AeneasVerif/son_refactor | Son HO | 2023-08-09 | 23 | -1495/+1513 |
|\| | | | | | Update the code following Charon's refactor | ||||
| * | Update the README | Son Ho | 2023-08-09 | 1 | -20/+21 |
| | | |||||
| * | Regenerate the test files | Son Ho | 2023-08-08 | 18 | -1463/+1465 |
| | | |||||
| * | Update the code following a refactor on Charon's side | Son Ho | 2023-08-08 | 4 | -12/+27 |
|/ | |||||
* | Merge pull request #32 from AeneasVerif/son_arrays | Son HO | 2023-08-07 | 110 | -1184/+5804 |
|\ | | | | | Add support for arrays/slices and const generics | ||||
| * | Update the flake.lock | Son Ho | 2023-08-07 | 1 | -40/+58 |
| | | |||||
| * | Regenerate the test files | Son Ho | 2023-08-07 | 6 | -60/+550 |
| | | |||||
| * | Change some fun id names to use "Mut"/"Shared" as a suffix | Son Ho | 2023-08-07 | 5 | -66/+66 |
| | | |||||
| * | Fix a heart beat issue in a Lean proof | Son Ho | 2023-08-04 | 1 | -0/+4 |
| | | |||||
| * | Add an option to not override Hashmap.lean | Son Ho | 2023-08-04 | 4 | -3/+16 |
| | | |||||
| * | Generate the array test files for Coq and F* | Son Ho | 2023-08-04 | 12 | -0/+1560 |
| | | |||||
| * | Update the Makefile and regenerate the test files | Son Ho | 2023-08-04 | 28 | -63/+637 |
| | | |||||
| * | Fix issues with the extraction and extend the primitive libraries for Coq and F* | Son Ho | 2023-08-04 | 5 | -32/+151 |
| | | |||||
| * | Add a forgotten file | Son Ho | 2023-08-04 | 1 | -0/+1 |
| | | |||||
| * | Generate the Array example in Lean | Son Ho | 2023-08-04 | 2 | -0/+295 |
| | | |||||
| * | Make minor modifications | Son Ho | 2023-08-04 | 4 | -9/+9 |
| | | |||||
| * | Add SliceLen as a primitive function and make minor adjustments | Son Ho | 2023-08-04 | 6 | -77/+100 |
| | | |||||
| * | Add the UtilsBase.lean file | Son Ho | 2023-08-04 | 1 | -0/+10 |
| | | |||||
| * | Start adding support for Arrays/Slices in the Lean library | Son Ho | 2023-08-04 | 9 | -49/+692 |
| | | |||||
| * | Fix an issue with the extraction of aggregated arrays | Son Ho | 2023-08-03 | 10 | -180/+320 |
| | | |||||
| * | Make a minor formatting modification for Lean | Son Ho | 2023-08-03 | 15 | -1/+15 |
| | | |||||
| * | Update the Makefile to add the array test | Son Ho | 2023-08-03 | 1 | -1/+16 |
| | | |||||
| * | Fix issues | Son Ho | 2023-08-03 | 11 | -57/+140 |
| | | |||||
| * | Make minor modifications | Son Ho | 2023-08-02 | 3 | -16/+29 |
| | | |||||
| * | Add the function signatures in Assumed.ml | Son Ho | 2023-08-02 | 1 | -0/+143 |
| | | |||||
| * | Make more progress | Son Ho | 2023-08-02 | 2 | -75/+186 |
| | | |||||
| * | Make progress | Son Ho | 2023-08-02 | 5 | -53/+80 |
| | | |||||
| * | Make progress | Son Ho | 2023-08-02 | 14 | -76/+178 |
| | | |||||
| * | Make progress | Son Ho | 2023-08-02 | 7 | -164/+232 |
| | | |||||
| * | Make progress proapagating the changes | Son Ho | 2023-08-02 | 25 | -273/+407 |
| | |