aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Expand)	Author	Files	Lines
2023-06-04	Start setting up the Nix derivation for HOL4	Son Ho	1	-4/+5
2023-06-04	Add a comment	Son Ho	1	-1/+5
2023-06-04	Finish the proofs of the hashmap	Son Ho	1	-463/+559
2023-06-04	Prove hash_map_insert_fwd_back_spec	Son Ho	1	-1/+59
2023-06-04	Make progress on the proofs of the hash map	Son Ho	1	-4/+619
2023-06-04	Make good progress on the proofs of the hashmap in HOL4	Son Ho	1	-46/+686
2023-06-04	Start working on the proofs of the hash map	Son Ho	1	-45/+172
2023-06-04	Make the theorems used by the progress tactic persistent	Son Ho	1	-9/+5
2023-06-04	Cleanup a bit the HOL4 backend and implement eval_conv	Son Ho	1	-1/+0
2023-06-04	Make more proofs about the hashmap proto	Son Ho	1	-0/+138
2023-06-04	Update the hashmap proofs and fix some tactics	Son Ho	1	-18/+178
2023-06-04	Start working on divDefLib for diverging definitions	Son Ho	1	-12/+2
2023-06-04	Reorganize the HOL4 files and fix some issues with the arithmetic proofs	Son Ho	1	-548/+2
2023-06-04	Make progress on the standard library for HOL4	Son Ho	1	-0/+679