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