| Commit message (Collapse) | Author | Files | Lines | ||
|---|---|---|---|---|---|
| 2024-06-25 | Bump Lean to v4.9.0rc3 (#261) | Son HO | 3 | -4/+2 | |
| 2024-06-22 | Do some cleanup in the Lean backend (#257) | Son HO | 7 | -22/+69 | |
| 2024-06-22 | Improve `scalar_tac` and `scalar_decr_tac` (#256) | Son HO | 7 | -50/+155 | |
| * Fix an issue in a proof of the hashmap * Improve scalar_decr_tac * Improve the error message of scalar_tac and add the missing Termination.lean | |||||
| 2024-06-21 | Add some proofs for the Lean backend (#255) | Son HO | 9 | -40/+125 | |
| * Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan> | |||||
| 2024-06-17 | Make a minor cleanup | Son Ho | 1 | -9/+11 | |
| 2024-06-17 | Update the Lean dependencies | Son Ho | 1 | -4/+4 | |
| 2024-06-14 | Start updating Lean to 4.9.0-rc2 | Son Ho | 2 | -4/+4 | |
| 2024-06-13 | Update the tests | Son Ho | 1 | -5/+0 | |
| 2024-06-13 | Update Lean to v4.9.0-rc1 | Son Ho | 15 | -139/+172 | |
| 2024-06-13 | Fix more issues with the scalar notations | Son Ho | 1 | -15/+29 | |
| 2024-06-13 | Fix more issues | Son Ho | 3 | -16/+22 | |
| 2024-06-13 | Fix a proof | Son Ho | 1 | -1/+1 | |
| 2024-06-12 | Add an example | Son Ho | 1 | -0/+3 | |
| 2024-06-12 | Update the scalar notations in Lean | Son Ho | 3 | -102/+109 | |
| 2024-06-12 | Revert "Update the scalar notation for the Lean backend" | Son Ho | 1 | -25/+25 | |
| This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933. | |||||
| 2024-06-12 | Revert "Update CoreConvertNum.lean" | Son Ho | 1 | -22/+22 | |
| This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb. | |||||
| 2024-06-12 | Update CoreConvertNum.lean | Son Ho | 1 | -22/+22 | |
| 2024-06-12 | Update the scalar notation for the Lean backend | Son Ho | 1 | -25/+25 | |
| 2024-06-12 | Deactivate the coercion from Nat to Scalar | Son Ho | 2 | -0/+17 | |
| 2024-06-12 | Slightly simplify the progress tactic | Son Ho | 1 | -8/+4 | |
| 2024-06-12 | Add wrappers around the rewriter | Son Ho | 1 | -0/+61 | |
| 2024-06-12 | Add the Simp.Config to the simp wrappers | Son Ho | 4 | -37/+36 | |
| 2024-06-12 | backends/lean: introduce `HasIntPred` automation | Ryan Lahfa | 2 | -8/+38 | |
| `HasIntPred` enable generation of facts based on specific terms in the context rather than their types, e.g. if the "length of a list" occurs in the context, generate the fact 0 ≤ length of that list, which can be further used for `scalar_tac` automation to discharge bounds goals. The aim is to use it to simplify various height related computations, e.g. whenever "height of a (left ; right) tree" is encountered, generate "height left < height of a (left ; right) tree", etc. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-06-11 | feat: `PropHasImp` can have `Sort u` as premisses | Ryan Lahfa | 1 | -1/+1 | |
| This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-05-24 | feat: add small pieces of max theory | Ryan Lahfa | 1 | -0/+39 | |
| `0#ty` is neutral for `max` for unsigned integers. Without the `Fact` instances, those theorems are not as automatic as they could be. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-05-24 | Update scalar_tac to use omega instead of linarith | Son Ho | 4 | -104/+82 | |
| 2024-05-21 | Fix an issue in the progress tactic | Son Ho | 1 | -0/+13 | |
| 2024-05-21 | feat(backends/lean): make `max`-related coercions nicer | Ryan Lahfa | 1 | -0/+12 | |
| Situations where you have `coe (max a b) = max (coe a) (coe b)` are often stuck during verification because of the lack of this theorem. With this theorem, `push_cast` works as intended and normalizes even further. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-05-13 | backends/lean: repair definition of `core.mem.replace` | Ryan Lahfa | 1 | -1/+4 | |
| Oops, it is supposed to do something with the second argument! Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-04-30 | feat(backend/lean): Raw Lean literals can be parsed into scalars automatically | Ryan Lahfa | 1 | -0/+5 | |
| We can use coercion to go to integers, build a scalar out of an int via unification and let the user clear up bounds or let Lean decide them. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-04-25 | Update the backend and ExtractBuiltin.ml | Son Ho | 1 | -1/+1 | |
| 2024-04-24 | Add core::option::unwrap builtin | Zyad Hassan | 3 | -5/+13 | |
| 2024-04-24 | compiler: map `core::mem::swap` to the pure swap | Ryan Lahfa | 1 | -0/+2 | |
| In the pure functional model, `swap` is mostly about borrow checking and should simplify to the pure swap in our backends. Other backends than Lean are not done in this commit. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-04-23 | feat(backends/lean): scalars form a linear order | Ryan Lahfa | 1 | -0/+15 | |
| More than c1c33de8, actually, scalars form a linear order with a decidable ≤ operation which is induced by the integer (Z) model. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-04-17 | compiler: map `core::option::Option::take` to identity function | Ryan Lahfa | 1 | -0/+2 | |
| `take` in a pure functional model is the identity function and everything related to borrow checking is handled by the forward/backward mechanism. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-04-12 | lean: scalars form a preorder | Ryan Lahfa | 1 | -0/+10 | |
| Via the canonical injection, we can easily define an induced preorder on scalars and inherit all nice properties. It's useful to reason on specific scalar preorders w.r.t. Ordering, see the binary search tree verification example. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-04-12 | Add more definitions to the Lean library | Son Ho | 4 | -0/+127 | |
| 2024-04-12 | Reorganize the files in the Lean backend a bit | Son Ho | 5 | -241/+266 | |
| 2024-04-12 | Start adding integer functions to the Lean library | Son Ho | 3 | -3/+266 | |
| 2024-04-12 | Fix a proof | Son Ho | 1 | -1/+0 | |
| 2024-04-12 | Update the core.num.checked_* definitions | Son Ho | 1 | -31/+233 | |
| 2024-04-05 | Update the lean toolchain and fix the proofs | Son Ho | 9 | -20/+12 | |
| 2024-04-04 | Rename Result.ret as Result.ok in the backends | Son Ho | 8 | -217/+215 | |
| 2024-04-04 | Fix the coerce notation for scalars and update some lemmas | Son Ho | 1 | -4/+15 | |
| 2024-04-03 | Add builtins for some checked ops such as checked_add | Zyad Hassan | 1 | -0/+29 | |
| 2024-03-25 | backend(/tests)/lean: 4.6.0-rc1 → 4.6.1 | Ryan Lahfa | 1 | -1/+1 | |
| 4.6.0 has been released in https://github.com/leanprover/lean4/releases/tag/v4.6.0 Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr> | |||||
| 2024-03-18 | Fix a minor issue | Son Ho | 1 | -1/+3 | |
| 2024-03-18 | Regenerate the constants tests and update Primitives/Base.lean | Son Ho | 1 | -1/+1 | |
| 2024-03-09 | Fix an issue with the divergent encoding | Son Ho | 1 | -3/+27 | |
| 2024-03-08 | Fix tuple indexing for Lean backend | Zyad Hassan | 1 | -1/+1 | |
 |
index : aeneas | |
| aeneas rust verifier with a hacky Isabelle backend |
| summaryrefslogtreecommitdiff |