summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Scalar.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Do some cleanup in the Lean backend (#257)Son HO2024-06-221-1/+8
|
* Add some proofs for the Lean backend (#255)Son HO2024-06-211-5/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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>
* Update Lean to v4.9.0-rc1Son Ho2024-06-131-12/+12
|
* Update the scalar notations in LeanSon Ho2024-06-121-102/+21
|
* Revert "Update the scalar notation for the Lean backend"Son Ho2024-06-121-25/+25
| | | | This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
* Update the scalar notation for the Lean backendSon Ho2024-06-121-25/+25
|
* Deactivate the coercion from Nat to ScalarSon Ho2024-06-121-0/+7
|
* 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>
* 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>
* 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>
* Add core::option::unwrap builtinZyad Hassan2024-04-241-5/+0
|
* 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-121-0/+63
|
* Reorganize the files in the Lean backend a bitSon Ho2024-04-121-239/+0
|
* Start adding integer functions to the Lean librarySon Ho2024-04-121-0/+255
|
* Fix a proofSon Ho2024-04-121-1/+0
|
* Update the core.num.checked_* definitionsSon Ho2024-04-121-31/+233
|
* Merge branch 'son/clean' into checked-opsSon Ho2024-04-111-76/+85
|\
| * Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-111-3/+14
| |\
| | * Fix the coerce notation for scalars and update some lemmasSon Ho2024-04-041-4/+15
| | |
| * | Rename Result.ret as Result.ok in the backendsSon Ho2024-04-041-73/+71
| |/
* / Add builtins for some checked ops such as checked_addZyad Hassan2024-04-031-0/+29
|/
* Remove some commentsSon Ho2024-03-081-31/+0
|
* Update the handling of notations like #u32 or #isizeSon Ho2024-03-081-67/+101
|
* Update the notation for heterogeneous negationSon Ho2024-03-081-3/+12
|
* Introduce a notation for constant scalars in match patternsSon Ho2024-03-071-0/+29
|
* Cleanup a bit Scalar.leanSon Ho2024-02-091-198/+198
|
* Fix more proofsSon Ho2024-02-021-56/+55
|
* Add some lemmas to the Lean backendSon Ho2024-01-271-4/+14
|
* Improve the Lean backendSon Ho2024-01-261-0/+11
|
* Update the extraction to handle casts between integers/boolsSon Ho2023-12-131-0/+4
|
* Update the progress tactic to use discrimination treesSon Ho2023-12-081-63/+63
|
* Merge branch 'main' into son_fixes2Son Ho2023-12-051-26/+143
|\
| * Add support for more bitwise operations and update the extractionSon Ho2023-11-291-2/+40
| |
| * Merge branch 'main' into son_traits and fix some issuesSon Ho2023-10-161-28/+198
| |\
| * | Improve formatting of scalars in LeanSon Ho2023-10-161-0/+15
| | |
| * | Fix some issuesSon Ho2023-09-071-24/+24
| | |
| * | Map some globals like u32::MAX to standard definitionsSon Ho2023-09-071-0/+42
| | |
* | | Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho2023-09-181-0/+3
| |/ |/|
* | Add notations for the Isize.ofInt, etc.Son Ho2023-09-181-0/+16
| |
* | Add arithmetic lemmas in Scalar.leanSon Ho2023-09-181-12/+179
| |
* | Improve scalar_tacSon Ho2023-09-181-51/+16
|/
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-041-9/+2
|
* Make progress on the proofs of the hashmapSon Ho2023-07-251-4/+43
|
* Make progress on the hashmap propertiesSon Ho2023-07-251-21/+27
|
* Add fine-grained lemmas for the arithmetic operationsSon Ho2023-07-201-7/+130
|
* Add arithmetic spec lemmasSon Ho2023-07-191-6/+161
|
* Start proving theorems for primitive definitionsSon Ho2023-07-171-0/+1
|
* Reorganize the Lean backendSon Ho2023-07-171-0/+507
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 09:27:12 +0000