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 more F* files
Son Ho
2023-10-27
18
-1549
/
+1427
|
*
|
|
Fix a minor issue and regenerate some F* test files
Son Ho
2023-10-27
10
-602
/
+646
|
*
|
|
Regenerate some of the F* test files
Son Ho
2023-10-27
19
-440
/
+549
|
*
|
|
Make minor modifications and update the array test for F*
Son Ho
2023-10-26
6
-188
/
+200
|
*
|
|
Update Primitives.fst
Son Ho
2023-10-26
8
-318
/
+2757
|
*
|
|
Fix some issues and regenerate the HashmapMain example for Lean
Son Ho
2023-10-26
5
-106
/
+147
|
*
|
|
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
|
/
/
/
/
|
*
|
|
Improve formatting of scalars in Lean
Son Ho
2023-10-16
2
-23
/
+25
|
*
|
|
Fix a small issue
Son Ho
2023-10-16
2
-13
/
+53
|
*
|
|
Update Primitives.fst
Son Ho
2023-10-13
1
-0
/
+3
|
*
|
|
Add support for array repeat
Son Ho
2023-10-13
1
-26
/
+7
|
*
|
|
Add sup
Son Ho
2023-10-13
9
-4
/
+91
|
*
|
|
Slightly improve formatting of the generated code
Son Ho
2023-10-06
2
-11
/
+16
[prev]
[next]