repository: added AutoCorrode submodule

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.

In this initial commit, we add AutoCorrode as a Git submodule and create a
single example theory file containing proofs of transliterated C functions from
poly.c in mlkem-native.  A dedicate Makefile for Isabelle proofs is also
provided with targets to open Isabelle/jEdit for interactive proof and also for
batch building.

Signed-off-by: Dominic Mulligan <dominic.p.mulligan@gmail.com>

Author: DominicPM

.github/workflows/all.yml

@@ -51,6 +51,14 @@ jobs:
     needs: [ base, nix ]
     uses: ./.github/workflows/cbmc.yml
     secrets: inherit
+  isabelle:
+    name: Isabelle
+    permissions:
+      contents: 'read'
+      id-token: 'write'
+    needs: [ base ]
+    uses: ./.github/workflows/isabelle.yml
+    secrets: inherit
   oqs_integration:
     name: libOQS
     permissions:

.github/workflows/isabelle.yml

@@ -0,0 +1,35 @@
+# Copyright (c) The mlkem-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: Isabelle
+permissions:
+  contents: read
+on:
+  workflow_call:
+  workflow_dispatch:
+
+jobs:
+  isa-proofs:
+    name: isa-proofs
+    runs-on: ubuntu-latest
+    container:
+      image: makarius/isabelle:Isabelle2025-2
+      options: --user root
+
+    steps:
+      - name: Checkout mlkem-native
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          submodules: recursive
+
+      - name: Checkout AFP mirror
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          repository: isabelle-prover/mirror-afp-2025-1
+          path: AutoCorrode/dependencies/afp
+
+      - name: Install build tooling
+        run: apt-get update -qq && apt-get install -y -qq make > /dev/null
+
+      - name: Build Isabelle proofs
+        run: make -C isa-proofs build ISABELLE_HOME=/home/isabelle/Isabelle/bin

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "AutoCorrode"]
+	path = AutoCorrode
+	url = https://github.com/awslabs/AutoCorrode

AutoCorrode

@@ -102,3 +102,24 @@ See [CONTRIBUTING.md](CONTRIBUTING.md) for instructions on how to setup and use
 ### Running the HOL-Light proofs
 
 Once you are in the `nix` shell or have all tools setup by hand, use `./scripts/tests hol_light` (or just `tests hol_light` in the `nix` shell) to re-check the HOL-Light proofs. Note that depending on the function, they will take a long time. See `tests hol_light --help` for details on the command line options, and [proofs/hol_light](proofs/hol_light) for more details on the HOL-Light proofs in general.
+
+## Isabelle (AutoCorrode)
+
+### Prerequisites
+
+To run the Isabelle proofs in [`isa-proofs`](isa-proofs), you need Isabelle2025-2 and the AFP mirror used by AutoCorrode (containing `Word_Lib` and `Isabelle_C`).
+
+### Running the Isabelle proofs
+
+From the repository root:
+
+```bash
+make -C isa-proofs setup-afp   # optional helper to clone mirror-afp-2025-1
+make -C isa-proofs build
+```
+
+To open jEdit with all required session directories configured:
+
+```bash
+make -C isa-proofs jedit
+```