repository: added AutoCorrode submodule

DominicPM · DominicPM · commit c8981cb24c82 · 2026-02-27T17:41:15.000Z
AutoCorrode is a separation logic framework developed by AWS for use in the
verification of the Nitro Isolation Engine.  Originally targetting Rust, a new
frontend for C11 has recently been added using an established Isabelle library,
Isabelle/C, for parsing.  C code can be embedded both in Isabelle theory files
for reasoning about, or code can be loaded from .c files, parsed, and processed
into Isabelle definitions automatically (post preprocessing with cpp).

The C frontend is still a work-in-progress, but has sufficiently advanced enough
that material from the poly.c file from mlkem-native can now be verified using
an abstract specification and weakest-precondition style reasoning.  See the
file Mlkem_Native_Examples.thy for these proofs.

Signed-off-by: Dominic Mulligan &lt;dominic.p.mulligan@gmail.com&gt;
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "AutoCorrode"]
+	path = AutoCorrode
+	url = https://github.com/awslabs/AutoCorrode
diff --git a/AutoCorrode b/AutoCorrode
@@ -0,0 +1 @@
+Subproject commit 093a55bb16de8a71a646e653540c68340ab767fb

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+[submodule "AutoCorrode"]`
	`2`	`+ path = AutoCorrode`
	`3`	`+ url = https://github.com/awslabs/AutoCorrode`