index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
backends
/
lean
/
Base
/
Primitives
/
Scalar.lean
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
*
Update the scalar notation for the Lean backend
Son Ho
2024-06-12
1
-25
/
+25
*
Deactivate the coercion from Nat to Scalar
Son Ho
2024-06-12
1
-0
/
+7
*
feat: add small pieces of max theory
Ryan Lahfa
2024-05-24
1
-0
/
+39
*
feat(backends/lean): make `max`-related coercions nicer
Ryan Lahfa
2024-05-21
1
-0
/
+12
*
feat(backend/lean): Raw Lean literals can be parsed into scalars automatically
Ryan Lahfa
2024-04-30
1
-0
/
+5
*
Add core::option::unwrap builtin
Zyad Hassan
2024-04-24
1
-5
/
+0
*
feat(backends/lean): scalars form a linear order
Ryan Lahfa
2024-04-23
1
-0
/
+15
*
lean: scalars form a preorder
Ryan Lahfa
2024-04-12
1
-0
/
+10
*
Add more definitions to the Lean library
Son Ho
2024-04-12
1
-0
/
+63
*
Reorganize the files in the Lean backend a bit
Son Ho
2024-04-12
1
-239
/
+0
*
Start adding integer functions to the Lean library
Son Ho
2024-04-12
1
-0
/
+255
*
Fix a proof
Son Ho
2024-04-12
1
-1
/
+0
*
Update the core.num.checked_* definitions
Son Ho
2024-04-12
1
-31
/
+233
*
Merge branch 'son/clean' into checked-ops
Son Ho
2024-04-11
1
-76
/
+85
|
\
|
*
Merge remote-tracking branch 'origin/main' into son/clean
Son Ho
2024-04-11
1
-3
/
+14
|
|
\
|
|
*
Fix the coerce notation for scalars and update some lemmas
Son Ho
2024-04-04
1
-4
/
+15
|
*
|
Rename Result.ret as Result.ok in the backends
Son Ho
2024-04-04
1
-73
/
+71
|
|
/
*
/
Add builtins for some checked ops such as checked_add
Zyad Hassan
2024-04-03
1
-0
/
+29
|
/
*
Remove some comments
Son Ho
2024-03-08
1
-31
/
+0
*
Update the handling of notations like #u32 or #isize
Son Ho
2024-03-08
1
-67
/
+101
*
Update the notation for heterogeneous negation
Son Ho
2024-03-08
1
-3
/
+12
*
Introduce a notation for constant scalars in match patterns
Son Ho
2024-03-07
1
-0
/
+29
*
Cleanup a bit Scalar.lean
Son Ho
2024-02-09
1
-198
/
+198
*
Fix more proofs
Son Ho
2024-02-02
1
-56
/
+55
*
Add some lemmas to the Lean backend
Son Ho
2024-01-27
1
-4
/
+14
*
Improve the Lean backend
Son Ho
2024-01-26
1
-0
/
+11
*
Update the extraction to handle casts between integers/bools
Son Ho
2023-12-13
1
-0
/
+4
*
Update the progress tactic to use discrimination trees
Son Ho
2023-12-08
1
-63
/
+63
*
Merge branch 'main' into son_fixes2
Son Ho
2023-12-05
1
-26
/
+143
|
\
|
*
Add support for more bitwise operations and update the extraction
Son Ho
2023-11-29
1
-2
/
+40
|
*
Merge branch 'main' into son_traits and fix some issues
Son Ho
2023-10-16
1
-28
/
+198
|
|
\
|
*
|
Improve formatting of scalars in Lean
Son Ho
2023-10-16
1
-0
/
+15
|
*
|
Fix some issues
Son Ho
2023-09-07
1
-24
/
+24
|
*
|
Map some globals like u32::MAX to standard definitions
Son Ho
2023-09-07
1
-0
/
+42
*
|
|
Simplify some lemmas and prove that the scalars and Vec are inhabited
Son Ho
2023-09-18
1
-0
/
+3
|
|
/
|
/
|
*
|
Add notations for the Isize.ofInt, etc.
Son Ho
2023-09-18
1
-0
/
+16
*
|
Add arithmetic lemmas in Scalar.lean
Son Ho
2023-09-18
1
-12
/
+179
*
|
Improve scalar_tac
Son Ho
2023-09-18
1
-51
/
+16
|
/
*
Start adding support for Arrays/Slices in the Lean library
Son Ho
2023-08-04
1
-9
/
+2
*
Make progress on the proofs of the hashmap
Son Ho
2023-07-25
1
-4
/
+43
*
Make progress on the hashmap properties
Son Ho
2023-07-25
1
-21
/
+27
*
Add fine-grained lemmas for the arithmetic operations
Son Ho
2023-07-20
1
-7
/
+130
*
Add arithmetic spec lemmas
Son Ho
2023-07-19
1
-6
/
+161
*
Start proving theorems for primitive definitions
Son Ho
2023-07-17
1
-0
/
+1
*
Reorganize the Lean backend
Son Ho
2023-07-17
1
-0
/
+507