summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/Scalar.lean (unfollow)
Commit message (Collapse)AuthorFilesLines
2024-06-22Do some cleanup in the Lean backend (#257)Son HO1-1/+8
2024-06-21Add some proofs for the Lean backend (#255)Son HO1-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>
2024-06-13Update Lean to v4.9.0-rc1Son Ho1-12/+12
2024-06-12Update the scalar notations in LeanSon Ho1-102/+21
2024-06-12Revert "Update the scalar notation for the Lean backend"Son Ho1-25/+25
This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
2024-06-12Update the scalar notation for the Lean backendSon Ho1-25/+25
2024-06-12Deactivate the coercion from Nat to ScalarSon Ho1-0/+7
2024-05-24feat: add small pieces of max theoryRyan Lahfa1-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-21feat(backends/lean): make `max`-related coercions nicerRyan Lahfa1-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-04-30feat(backend/lean): Raw Lean literals can be parsed into scalars automaticallyRyan Lahfa1-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-24Add core::option::unwrap builtinZyad Hassan1-5/+0
2024-04-23feat(backends/lean): scalars form a linear orderRyan Lahfa1-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-12lean: scalars form a preorderRyan Lahfa1-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-12Add more definitions to the Lean librarySon Ho1-0/+63
2024-04-12Reorganize the files in the Lean backend a bitSon Ho1-239/+0
2024-04-12Start adding integer functions to the Lean librarySon Ho1-0/+255
2024-04-12Fix a proofSon Ho1-1/+0
2024-04-12Update the core.num.checked_* definitionsSon Ho1-31/+233
2024-04-04Rename Result.ret as Result.ok in the backendsSon Ho1-73/+71
2024-04-04Fix the coerce notation for scalars and update some lemmasSon Ho1-4/+15
2024-04-03Add builtins for some checked ops such as checked_addZyad Hassan1-0/+29
2024-03-08Remove some commentsSon Ho1-31/+0
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho1-67/+101
2024-03-08Update the notation for heterogeneous negationSon Ho1-3/+12
2024-03-07Introduce a notation for constant scalars in match patternsSon Ho1-0/+29
2024-02-09Cleanup a bit Scalar.leanSon Ho1-198/+198
2024-02-02Fix more proofsSon Ho1-56/+55
2024-01-27Add some lemmas to the Lean backendSon Ho1-4/+14
2024-01-26Improve the Lean backendSon Ho1-0/+11
2023-12-13Update the extraction to handle casts between integers/boolsSon Ho1-0/+4
2023-12-08Update the progress tactic to use discrimination treesSon Ho1-63/+63
2023-11-29Add support for more bitwise operations and update the extractionSon Ho1-2/+40
2023-10-16Improve formatting of scalars in LeanSon Ho1-0/+15
2023-09-18Simplify some lemmas and prove that the scalars and Vec are inhabitedSon Ho1-0/+3
2023-09-18Add notations for the Isize.ofInt, etc.Son Ho1-0/+16
2023-09-18Add arithmetic lemmas in Scalar.leanSon Ho1-12/+179
2023-09-18Improve scalar_tacSon Ho1-51/+16
2023-09-07Fix some issuesSon Ho1-24/+24
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-0/+42
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho1-9/+2
2023-07-25Make progress on the proofs of the hashmapSon Ho1-4/+43
2023-07-25Make progress on the hashmap propertiesSon Ho1-21/+27
2023-07-20Add fine-grained lemmas for the arithmetic operationsSon Ho1-7/+130
2023-07-19Add arithmetic spec lemmasSon Ho1-6/+161
2023-07-17Start proving theorems for primitive definitionsSon Ho1-0/+1
2023-07-17Reorganize the Lean backendSon Ho1-218/+10
2023-07-17Move a definitionSon Ho1-0/+3
2023-07-12Make the `by inlit` implicitSon Ho1-8/+7
2023-07-12Improve the handling of arithmetic boundsSon Ho1-111/+117
2023-07-12Finish a first version of the progress tacticSon Ho1-24/+65
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 11:23:44 +0000