Added AutoCorrode submodule, a reasoning framework for Rust and C in Isabelle/HOL by DominicPM · Pull Request #1590 · pq-code-package/mlkem-native

DominicPM · 2026-02-27T17:45:25Z

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.

(Note I am one of @hanno-becker's colleagues at AWS and have discussed this with him prior to opening the PR.)

mkannwischer

Thanks you very much @DominicPM! I'm excited to see progress toward verifiying the correctness of the C parts of this code base.

Could you share a bit more what your plan is with this? Are you planning to to verify large parts of the code base or is this more a PoC and you are planning to leave it at that?

I have a couple of comments below - mostly questions to help me better understand how things should be done, as I am not very familiar with AutoCorrode (yet).
There are a few blockers (marked as such) - for the rest I don't mind merging it first and improving in a follow-up.

mkannwischer · 2026-02-28T04:06:35Z

proofs/isabelle/MLKEM_Poly_Functional_Correctness.thy

Blocker: the proofs should go to proofs/isabelle

mkannwischer · 2026-02-28T04:07:51Z

isa-proofs/Example.thy

+  imports "Micro_C_Examples.Simple_C_Functions" "Micro_C_Examples.C_While_Examples"
+begin
+
+section \<open>Abstract polynomial arithmetic\<close>


I'd like to get some better idea on how we should structure the proofs in the long term. For HOL-light and CBMC, we commonly have one file/folder for each verified functions + some common code separately.
Is this also the structure we should follow for Isabelle?

We could structure it that way, yes. Isabelle checks theory files in parallel, so this would probably speed up proof checking as well.

mkannwischer · 2026-02-28T04:08:49Z

isa-proofs/Example.thy

+  void mlk_poly_add(mlk_poly *r, const mlk_poly *b)
+  {
+    unsigned i;
+    for (i = 0; i < 256; i++)
+    {
+      /* The preconditions imply that the addition stays within int16_t. */
+      r->coeffs[i] = (int16_t)(r->coeffs[i] + b->coeffs[i]);
+    }
+  }


I wonder how we can ensure this stays in sync with the C code. Do you have an idea how that should be done?

I implemented a micro_c_file command in AutoCorrode which can import a (preprocessed) C file directly. The material above is just an example. The imagined flow is MLKEM Sources → Preprocessor → Load into Isabelle via dedicated theory files, and then combined with proofs in separate theories, per the discussion above.

Nice, that sounds great.

mkannwischer · 2026-02-28T04:09:17Z

isa-proofs/Example.thy

+  typedef struct {
+    int16_t coeffs[256];
+  } mlk_poly;


Is there a mechanism to move some shared code elsewhere so we do not have to duplicate it over an over?

Yes, theories can import other theories and build on top of them in Isabelle, reusing the material.

mkannwischer · 2026-02-28T04:10:35Z

.gitmodules

Blocker: Dependencies should be imported via nix, not a gitsubmodule. I can help set that up if needed.
Ideally, I would want to have the isabelle installation also installed via nix, so developers can just type nix develop .#isabelle and they get all dependencies need. For now we can assume an issabelle installation though.

mkannwischer · 2026-02-28T04:12:33Z

BUILDING.md

+
+### 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`).


Blocker (unless a nix setup is infeasible for a good reason):
How do I install the AFP Mirror?
This suggests that we really should do the nix setup already, as we don't want developers to have to go through a multi-step installation process just to get proofs reproduced.

DominicPM · 2026-02-28T09:04:32Z

Could you share a bit more what your plan is with this? Are you planning to to verify large parts of the code base or is this more a PoC and you are planning to leave it at that?

Ideally, we verify all of the C code in the codebase using this, or at least as much as possible modulo any deficiencies in AutoCorrode (which we can iron out as we find them).

DominicPM · 2026-02-28T21:50:29Z

@mkannwischer I've reworked this material and made some changes to upstream AutoCorrode to better support this work. The latest changeset does not address all of your review comments—there is still a submodule, for example which I have not yet addressed—but this now provides a much more realistic picture of how any such verification effort would proceed. In particular:

MLKEM_Poly_Definitions.thy now imports the add, sub, and barrett_reduction functions directly from the poly.c preprocessed source file into Isabelle with no manual embedding of the source code into an Isabelle theory file. Note that this file is autogenerated from a template file. To support this autogeneration there's a small amount of boilerplate machinery in the form of a units file which indicates which files we are interested in translating, and a "manifest" which is used by a Python script and the AutoCorrode machinery itself to identify the types and functions we are interested in verifying. The general split between these is: Python is used to filter out material that AutoCorrode cannot support (e.g. __builtin_darwin types on Apple hardware), whilst AutoCorrode handles everything else itself.
MLKEM_Machine_Model sets up the "machine model" used in the proof, in particular the model of memory. At the moment, AutoCorrode uses a particular model of memory which is based around a notion of "global value". This requires that every type that we wish to store in memory (or mutate, or similar) is registered as being mutable. (Modifying this memory model to something more realistic is a long-term goal in AutoCorrode, but has not been done yet.) As a result of this, the extraction process is two-phased, with types needing to be extracted first in order to define the memory model, which in turn is then used to constrain polymorphic variables appearing in the types of the C embeddings in MLKEM_Poly_Definitions.thy. Note at present this machine model is axiomatic: there is no model construction of the model proving that the axioms are non-contradictory. This is future work, but entirely straightforward.
Common.thy contains common material, namely an abstract type of polynomials defined in terms of HOL's (mathematical) integers, operations on them, and an explicit refinement relation between these mathematical polynomials and the concrete machine-word realised polynomials manipulated by mlkem-native.
MLKEM_Poly_Functional_Correctness.thy contains the functional correctness proofs proper. These are phrased in terms of pre/postcondition function contracts, setting up an explicit refinement between the concrete polynomials inputted to and outputted by a function, and an abstract definition of the behaviour of the function. Essentially, the proofs assert that each poly.c function "makes a step" in accordance with a pure HOL function describing its behaviour. As AutoCorrode uses total correctness reasoning, as a corollary, each function is also memory safe, free from undefined behaviour, and terminates on all inputs (up-to modelling assumptions and correctness of our rendering of the C semantics).

The rest of the material supports this autogeneration pipeline.

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>

DominicPM requested a review from a team as a code owner February 27, 2026 17:45

DominicPM force-pushed the autocorrode-submodule branch from c8981cb to c4035e1 Compare February 27, 2026 22:57

mkannwischer requested changes Feb 28, 2026

View reviewed changes

mkannwischer added the needs-mldsa-native-port label Feb 28, 2026

DominicPM force-pushed the autocorrode-submodule branch from c4035e1 to 0012a8f Compare February 28, 2026 21:34

DominicPM force-pushed the autocorrode-submodule branch 3 times, most recently from 5ae28eb to c2188c1 Compare March 7, 2026 19:51

hanno-becker force-pushed the autocorrode-submodule branch from c2188c1 to f3e0453 Compare March 11, 2026 03:15


		### 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`).

Conversation

DominicPM commented Feb 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mkannwischer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

DominicPM commented Feb 28, 2026

Uh oh!

DominicPM commented Feb 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

DominicPM commented Feb 27, 2026 •

edited

Loading