summaryrefslogtreecommitdiff
path: root/backends (follow)
Commit message (Collapse)AuthorAgeFilesLines
* isabelle: more correct u32 typeisabellestuebinm2024-07-041-3/+11
| | | | | | (I'd have to figure out how to do the code equation stuff to make this type actually usable the way nat is, but it should behave correctly in proofs)
* had some fun writing an IsabelleHOL backendstuebinm2024-06-293-0/+85
| | | | | | | (do not actually use this, most things are broken, and the primitives lib barely exists and is simply incorrect. But it is enough to create syntax-correct Isabelle code for relatively simply rust code, as long as it does not contain any uses of traits)
* Bump Lean to v4.9.0rc3 (#261)Son HO2024-06-253-4/+2
|
* Do some cleanup in the Lean backend (#257)Son HO2024-06-227-22/+69
|
* Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO2024-06-227-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
* Add some proofs for the Lean backend (#255)Son HO2024-06-219-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>
* Make a minor cleanupSon Ho2024-06-171-9/+11
|
* Merge branch 'son/update-lean' into has-int-predSon Ho2024-06-1718-283/+414
|\
| * Update the Lean dependenciesSon Ho2024-06-171-4/+4
| |
| * Start updating Lean to 4.9.0-rc2Son Ho2024-06-142-4/+4
| |
| * Update the testsSon Ho2024-06-131-5/+0
| |
| * Update Lean to v4.9.0-rc1Son Ho2024-06-1315-139/+172
| |
| * Fix more issues with the scalar notationsSon Ho2024-06-131-15/+29
| |
| * Fix more issuesSon Ho2024-06-133-16/+22
| |
| * Fix a proofSon Ho2024-06-131-1/+1
| |
| * Merge branch 'main' into son/scalars2Son HO2024-06-131-1/+1
| |\
| | * Merge branch 'main' into prop-has-imp-sortSon HO2024-06-125-45/+118
| | |\
| | * | feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa2024-06-111-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| * | | Add an exampleSon Ho2024-06-121-0/+3
| | | |
| * | | Update the scalar notations in LeanSon Ho2024-06-123-102/+109
| | |/ | |/|
| * | Revert "Update the scalar notation for the Lean backend"Son Ho2024-06-121-25/+25
| | | | | | | | | | | | This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
| * | Revert "Update CoreConvertNum.lean"Son Ho2024-06-121-22/+22
| | | | | | | | | | | | This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb.
| * | Update CoreConvertNum.leanSon Ho2024-06-121-22/+22
| | |
| * | Update the scalar notation for the Lean backendSon Ho2024-06-121-25/+25
| | |
| * | Deactivate the coercion from Nat to ScalarSon Ho2024-06-122-0/+17
| | |
| * | Slightly simplify the progress tacticSon Ho2024-06-121-8/+4
| | |
| * | Add wrappers around the rewriterSon Ho2024-06-121-0/+61
| | |
| * | Add the Simp.Config to the simp wrappersSon Ho2024-06-124-37/+36
| |/
* / backends/lean: introduce `HasIntPred` automationRyan Lahfa2024-06-122-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>
* feat: add small pieces of max theoryRyan Lahfa2024-05-241-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>
* Update scalar_tac to use omega instead of linarithSon Ho2024-05-244-104/+82
|
* Fix an issue in the progress tacticSon Ho2024-05-211-0/+13
|
* feat(backends/lean): make `max`-related coercions nicerRyan Lahfa2024-05-211-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>
* Merge pull request #164 from RaitoBezarius/ofnat_scalarSon HO2024-05-141-0/+5
|\ | | | | | | feat(backend/lean): Raw Lean literals can be parsed into scalars automatically
| * feat(backend/lean): Raw Lean literals can be parsed into scalars automaticallyRyan Lahfa2024-04-301-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>
* | backends/lean: repair definition of `core.mem.replace`Ryan Lahfa2024-05-131-1/+4
|/ | | | | | Oops, it is supposed to do something with the second argument! Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Update the backend and ExtractBuiltin.mlSon Ho2024-04-253-1/+14
|
* Merge branch 'main' into core-option-unwrapSon Ho2024-04-253-0/+154
|\
| * Update the tests for ExternalSon Ho2024-04-252-0/+150
| |
| * Merge branch 'main' into option-takeSon Ho2024-04-251-0/+15
| |\
| * | compiler: map `core::mem::swap` to the pure swapRyan Lahfa2024-04-241-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>
| * | compiler: map `core::option::Option::take` to identity functionRyan Lahfa2024-04-171-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>
* | | Add core::option::unwrap builtinZyad Hassan2024-04-243-5/+13
| |/ |/|
* | feat(backends/lean): scalars form a linear orderRyan Lahfa2024-04-231-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>
* lean: scalars form a preorderRyan Lahfa2024-04-121-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>
* Add more definitions to the Lean librarySon Ho2024-04-124-0/+127
|
* Reorganize the files in the Lean backend a bitSon Ho2024-04-125-241/+266
|
* Start adding integer functions to the Lean librarySon Ho2024-04-123-3/+266
|
* Fix a proofSon Ho2024-04-121-1/+0
|
* Update the core.num.checked_* definitionsSon Ho2024-04-121-31/+233
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 11:53:50 +0000