aeneas - aeneas rust verifier with a hacky Isabelle backend

	Commit message (Collapse)	Author	Files	Lines
2024-07-04	isabelle: more correct u32 typeisabelle	stuebinm	1	-3/+11
	(I'd have to figure out how to do the code equation stuff to make this type actually usable the way nat is, but it should behave correctly in proofs)
2024-06-29	had some fun writing an IsabelleHOL backend	stuebinm	3	-0/+85
	(do not actually use this, most things are broken, and the primitives lib barely exists and is simply incorrect. But it is enough to create syntax-correct Isabelle code for relatively simply rust code, as long as it does not contain any uses of traits)