proofs: added AutoCorrode/C proofs of a subset of poly.c functionality

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 define a pipeline which takes MLKEM .c and .h files and autogenerates
AutoCorrode/C definitions.  Setting this up correctly requires some care: C11
files must first be preprocessed using the C preprocessor, the relevant
definitions and supporting types that we are interested in verifying must be
filtered out from the resulting generated code, and any feature that we cannot
support (e.g. __darwin_builtin types, when running on an Apple machine) must be
filtered out.  To do this we use a series of "manifest" files which identify the
functions we are interested in working with, which is processed by dedicated
Python script files and the `micro_c_translate` command in Isabelle.

Using the pipeline above, we extract all of the functions and supporting types
from `poly.{c, h}` and the supporting `verify.{c, h}` file, specify them, and
verify them with respect to a series of pre/postcondition specifications
using Weakest Precondition-style reasoning.  To do this, we define a machine
"locale" or "interface" setting up the memory model of the AutoCorrode/C
library.  This presents a bit of a chicken-and-egg situation, as the
AutoCorrode/C memory model requires knowledge of any types that will be mutated,
however translated C functions must be defined within the scope of the machine
model in order to constrain the types of memory addresses and memory values.
As a result of this, extraction of C code proceeds in two stages, with the
first stage extracting types alone, prior to the definition of the machine and
used to define it, which is then used further when extracting C functions.

The machine model is instantiated with a concrete model, demonstrating that the
axioms describing the machine are consistent, and opening the door to execute
the translated C code via Isabelle's code-generation mechanism for conformance
testing.

Note that the more complex functions in this changeset are still a
work-in-progress, including the NTT.

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:
+  isabelle-proofs:
+    name: proofs/isabelle
+    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 proofs/isabelle 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 [`proofs/isabelle`](proofs/isabelle), 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 proofs/isabelle setup-afp   # optional helper to clone mirror-afp-2025-1
+make -C proofs/isabelle build
+```
+
+To open jEdit with all required session directories configured:
+
+```bash
+make -C proofs/isabelle jedit
+```

BUILDING.md

@@ -71,6 +71,8 @@ relevant parts of the Arm and x86 architectures). See [proofs/hol_light](proofs/
 **NOTE:** Formal Verification is never absolute. See [SOUNDNESS.md](SOUNDNESS.md) for a detailed analysis of the scope, assumptions and risks of the formal verification
 efforts around mlkem-native.
 
+Selected C/functional components are also verified in [Isabelle/HOL](https://isabelle.in.tum.de/) using AutoCorrode. See [proofs/isabelle](proofs/isabelle).
+
 ## Security
 
 All AArch64 and x86_64 assembly in mlkem-native is formally proved in [HOL Light](https://github.com/jrh13/hol-light) to be free of secret-dependent control flow,

README.md

@@ -10,4 +10,8 @@ We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to
 
 ## Assembly verification: HOL-Light
 
-We use the [HOL-Light](https://github.com/jrh13/hol-light) interactive theorem prover alongside the verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum) to show the functional correctness of all AArch64 and x86_64 assembly in mlkem-native at the object-code level. See [proofs/hol_light](hol_light).
+We use the [HOL-Light](https://github.com/jrh13/hol-light) interactive theorem prover alongside the verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum) to show the functional correctness of all AArch64 assembly and all x86_64 ML-KEM arithmetic assembly in mlkem-native at the object-code level. See [proofs/hol_light](hol_light).
+
+## C/functional verification in Isabelle (AutoCorrode)
+
+We use [Isabelle/HOL](https://isabelle.in.tum.de/) together with [AutoCorrode](https://github.com/awslabs/AutoCorrode) to translate and verify selected C implementations and their refinement lemmas. See [proofs/isabelle](isabelle).