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
/
fstar
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2023-12-13
Update the extraction to handle casts between integers/bools
Son Ho
1
-0
/
+4
2023-11-29
Add support for more bitwise operations and update the extraction
Son Ho
1
-8
/
+159
2023-11-21
Update more names
Son Ho
1
-16
/
+16
2023-11-21
Update the standard libraries
Son Ho
1
-28
/
+28
2023-11-09
Update the failing proofs
Son Ho
1
-1
/
+17
2023-10-27
Regenerate some of the F* test files
Son Ho
1
-2
/
+19
2023-10-26
Update Primitives.fst
Son Ho
1
-48
/
+318
2023-10-22
Add more support for numeric operations, xor, rotate
Jonathan Protzenko
1
-1
/
+22
2023-10-13
Update Primitives.fst
Son Ho
1
-0
/
+3
2023-09-07
Fix some issues
Son Ho
1
-10
/
+37
2023-08-04
Fix issues with the extraction and extend the primitive libraries for Coq and F*
Son Ho
1
-0
/
+75
2023-02-03
Do not unfold the monadic lets for the generated F* code
Son Ho
1
-1
/
+3
2022-11-16
Make minor modifications to the extraction
Son Ho
1
-10
/
+14
2022-11-14
Add a `-use-fuel` option
Son Ho
1
-0
/
+3
2022-11-14
Make [Result::Failure] type an [Error] parameter
Son Ho
2
-14
/
+65
2022-11-11
Move the fstar files to the new backends directory
Son Ho
1
-0
/
+287