| Commit message (Expand) | Author | Age | Files | Lines |
... | |
| * | | | Extract the trait decl methods | Son Ho | 2023-09-03 | 2 | -34/+54 |
| * | | | Make progress registering the trait decl method names | Son Ho | 2023-09-03 | 2 | -31/+93 |
| * | | | Do more cleanup | Son Ho | 2023-09-03 | 3 | -9/+9 |
| * | | | Add the keep_fwd field in TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 4 | -35/+42 |
| * | | | Update TranslateCore.pure_fun_translation | Son Ho | 2023-09-03 | 5 | -34/+33 |
| * | | | Update the type TranslateCore.fun_and_loops | Son Ho | 2023-09-03 | 4 | -34/+35 |
| * | | | Make progress on extracting trait decls and merge gen_ctx and extraction_ctx | Son Ho | 2023-09-03 | 3 | -98/+219 |
| * | | | Register the names for the trait decls | Son Ho | 2023-09-03 | 2 | -14/+154 |
| * | | | Make more progress | Son Ho | 2023-09-03 | 3 | -24/+67 |
| * | | | Make progress on the extraction | Son Ho | 2023-09-03 | 3 | -61/+221 |
| * | | | Make progress on the extraction | Son Ho | 2023-09-03 | 6 | -21/+264 |
| * | | | Make progress on the extraction | Son Ho | 2023-09-03 | 6 | -52/+138 |
| * | | | Improve the collision detection | Son Ho | 2023-09-03 | 1 | -16/+54 |
| * | | | Make good progress on Extract.ml | Son Ho | 2023-09-01 | 2 | -224/+237 |
| * | | | Update PureMicroPasses | Son Ho | 2023-09-01 | 2 | -44/+19 |
| * | | | Compute the normalized trait types maps and update Interpreter | Son Ho | 2023-09-01 | 6 | -70/+206 |
| * | | | Implement the normalization functions in AssociatedTypes | Son Ho | 2023-09-01 | 5 | -14/+335 |
| * | | | Make progress on Extract and ExtractBase | Son Ho | 2023-08-31 | 3 | -52/+132 |
| * | | | Update TranslateCore and factor out some definitions in PrintPure | Son Ho | 2023-08-31 | 2 | -42/+42 |
| * | | | Finish updating SymbolicToPure.ml | Son Ho | 2023-08-31 | 4 | -115/+212 |
| * | | | Start adding support for traits | Son Ho | 2023-08-31 | 31 | -776/+1258 |
| * | | | Regenerate the array tests | Son Ho | 2023-08-18 | 3 | -0/+25 |
| * | | | Add tests which use const generics as values | Son Ho | 2023-08-18 | 5 | -2/+17 |
| * | | | Update following the introduction of ConstantExpr | Son Ho | 2023-08-18 | 16 | -143/+220 |
| * | | | Make a minor modification | Son Ho | 2023-08-17 | 1 | -11/+0 |
| | * | | 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 |
| |/ /
|/| | |
|
| | * | Prove that Vec is inhabited | Son Ho | 2023-09-18 | 1 | -0/+4 |
| | * | Simplify some lemmas and prove that the scalars and Vec are inhabited | Son Ho | 2023-09-18 | 2 | -9/+10 |
| |/
|/| |
|
* | | Merge pull request #37 from AeneasVerif/son_tuto | Son HO | 2023-09-18 | 8 | -71/+691 |
|\ \ |
|
| * | | 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 |
|\ \
| |/
|/| |
|
| * | 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 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 README | Son Ho | 2023-08-09 | 1 | -20/+21 |
| * | Regenerate the test files | Son Ho | 2023-08-08 | 18 | -1463/+1465 |