index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
*
Regenerate the betree example for Lean
Son Ho
2023-10-26
1
-40
/
+39
*
Regenerate several test files for Lean
Son Ho
2023-10-26
4
-122
/
+132
*
Improve the handling of saved function effects in ExtractBuiltin.ml
Son Ho
2023-10-26
2
-24
/
+44
*
Regenerate the array files for Lean
Son Ho
2023-10-26
2
-111
/
+103
*
Make progress on fixing the extraction
Son Ho
2023-10-26
2
-72
/
+88
*
Improve ExtractBuiltin.ml
Son Ho
2023-10-26
2
-46
/
+57
*
Make progress on fixing the extraction for Lean
Son Ho
2023-10-26
5
-220
/
+180
*
Fix more issues at extraction and factor out defs in ExtractBuiltin
Son Ho
2023-10-26
2
-266
/
+166
*
Regenerate the hashmap files
Son Ho
2023-10-25
2
-86
/
+133
*
Make the hashmap files typecheck again in Lean
Son Ho
2023-10-25
12
-2775
/
+2778
*
Regenerate the Lean array test
Son Ho
2023-10-25
1
-169
/
+150
*
Fix some issues at extraction and add builtins
Son Ho
2023-10-25
11
-61
/
+546
*
Fix some issues to make the array test succeed again
Son Ho
2023-10-25
2
-16
/
+44
*
Remove the warning for loops
Son Ho
2023-10-25
1
-8
/
+0
*
Update following the addition of raw pointers
Son Ho
2023-10-25
12
-17
/
+77
*
Handle properly the builtin, non fallible functions
Son Ho
2023-10-24
5
-26
/
+62
*
Merge branch 'son_traits' into son_traits_types
Son Ho
2023-10-24
3
-8
/
+50
|
\
|
*
Merge branch 'son_traits_arrow' into protz_numeric
Son Ho
2023-10-24
16
-100
/
+163
|
|
\
|
*
|
Add more support for numeric operations, xor, rotate
Jonathan Protzenko
2023-10-22
3
-8
/
+50
*
|
|
Start taking into account non-fallible functions like core::mem::replace
Son Ho
2023-10-24
3
-75
/
+79
*
|
|
Fix minor issues
Son Ho
2023-10-24
2
-6
/
+6
*
|
|
Fix an issue coming from the modification for the opaque signatures
Son Ho
2023-10-24
1
-12
/
+7
*
|
|
Fix a printing issue with scalar values
Son Ho
2023-10-24
1
-3
/
+5
*
|
|
Filter some type arguments for the builtin types/functions
Son Ho
2023-10-24
4
-10
/
+87
*
|
|
Remove the possibility of generating opaque module signatures
Son Ho
2023-10-24
4
-330
/
+111
*
|
|
Add support for builtin trait implementations
Son Ho
2023-10-24
4
-20
/
+80
*
|
|
Fix various issues with the builtins
Son Ho
2023-10-24
4
-122
/
+234
*
|
|
Add definitions in for the Lean Primitives library
Son Ho
2023-10-24
3
-0
/
+57
*
|
|
Add some debugging information
Son Ho
2023-10-24
1
-0
/
+7
*
|
|
Deactivate the concrete interpreter tests
Son Ho
2023-10-24
1
-2
/
+2
*
|
|
Make progress on handling the builtins
Son Ho
2023-10-23
4
-154
/
+270
*
|
|
Remove some assumed types and add more support for builtin definitions
Son Ho
2023-10-23
24
-808
/
+763
|
|
/
|
/
|
*
|
Start updating to handle function pointers
Son Ho
2023-10-20
16
-100
/
+163
|
/
*
Refold the scalar types when applying progress
Son Ho
2023-10-17
4
-16
/
+91
*
Implement tactics for termination proofs which involve arithmetic
Son Ho
2023-10-17
4
-21
/
+37
*
Merge branch 'main' into son_traits and fix some issues
Son Ho
2023-10-16
18
-107
/
+780
|
\
|
*
Merge pull request #41 from AeneasVerif/son-readme
Son HO
2023-10-05
1
-0
/
+2
|
|
\
|
|
*
Add a mention to the Zulip in the README
Son Ho
2023-10-05
1
-0
/
+2
|
|
/
|
*
Merge pull request #37 from AeneasVerif/son_tuto
Son HO
2023-09-18
8
-71
/
+691
|
|
\
|
|
*
Update the README
Son Ho
2023-09-18
1
-0
/
+2
|
|
*
Cleanup the tutorial a bit
Son Ho
2023-09-18
1
-80
/
+110
|
|
*
Add notations for the Isize.ofInt, etc.
Son Ho
2023-09-18
1
-0
/
+16
|
|
*
Make minor modifications to the tutorial
Son Ho
2023-09-18
1
-3
/
+2
|
|
*
Add arithmetic lemmas in Scalar.lean
Son Ho
2023-09-18
1
-12
/
+179
|
|
*
Make progress on the tutorial
Son Ho
2023-09-18
1
-3
/
+66
|
|
*
Start writing a tutorial
Son Ho
2023-09-18
2
-0
/
+298
|
|
*
Improve scalar_tac
Son Ho
2023-09-18
3
-56
/
+36
|
|
*
Fix an issue when loading the saved theorem maps for the progress tactic
Son Ho
2023-09-18
2
-3
/
+68
|
|
/
|
*
Merge pull request #36 from AeneasVerif/update_lean
Son HO
2023-09-14
11
-69
/
+95
|
|
\
|
|
*
Fix the hashmap proofs in Lean
Son Ho
2023-09-14
5
-29
/
+41
[next]