index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tests
/
fstar
/
rename_attribute
/
Primitives.fst
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2024-06-18
Support for renaming using the rename attribute in charon (#239)
Escherichia
1
-0
/
+0
2024-04-25
Update the backend and ExtractBuiltin.ml
Son Ho
1
-0
/
+6
2024-04-25
Update the tests for External
Son Ho
1
-0
/
+75
2024-04-04
Rename Result.ret as Result.ok in the backends
Son Ho
1
-28
/
+28
2024-03-08
Update the Makefile and remove the split files for F*
Son Ho
1
-0
/
+0
2023-12-22
Fix minor issues
Son Ho
1
-1
/
+20
2023-12-22
Fix the models for core::mem::replace
Son Ho
1
-1
/
+1
2023-12-22
Update the library for F*
Son Ho
1
-83
/
+28
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
1
-14
/
+18
2022-11-11
Move the fstar files to the new backends directory
Son Ho
1
-0
/
+0
2022-11-11
Make the Nix build work
Son Ho
1
-0
/
+0
2022-11-10
Make a minor cleanup
Son Ho
1
-3
/
+4
2022-10-27
Reorganize a bit the project
Son Ho
1
-0
/
+0
2022-09-22
Update fstar/Primitives.fst
Son HO
1
-1
/
+1
2022-06-30
Traduct globals body separately (WIP)
Sidney Congard
1
-0
/
+3
2022-05-15
Add a pass to cleanup the deconstructed ADTs and fix a small issue
Son Ho
1
-1
/
+1
2022-05-15
Treat integer casts in a general manner
Son Ho
1
-0
/
+4
2022-02-11
Make good progress on the proofs of hashmap
Son Ho
1
-14
/
+14
2022-02-10
Make progress on the proofs of HashMap
Son Ho
1
-4
/
+4
2022-02-10
Update Primitives.fst
Son Ho
1
-1
/
+10
2022-02-09
Add definitions to Primitives.fst and start on improving/fixing the
Son Ho
1
-0
/
+49
2022-02-07
Make more minor modifications
Son Ho
1
-1
/
+3
2022-02-07
Make minor modifications to Primitives.fst
Son Ho
1
-1
/
+2
2022-02-04
Work on decomposition of monadic let-bindings for F*
Son Ho
1
-0
/
+10
2022-02-03
Make mor modifications
Son Ho
1
-0
/
+3
2022-02-03
Make minor modifications
Son Ho
1
-1
/
+1
2022-02-03
Rename Assumed.fst to Primitives.fst and make progress on that
Son Ho
1
-0
/
+205