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

Blocker: the proofs should go to proofs/isabelle

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

+  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

+  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

+  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

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

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

Add the DominicPM/AutoCorrode fork as a submodule.

…inement Add MLKEM_Spec.thy with core mathematical specifications (barrett_reduce_int, montgomery_reduce_int, fqmul_int, polynomial operations) and MLKEM_Refinement.thy with the refinement relation connecting C word types to abstract integers.

Add MLKEM_Zetas.thy with precomputed 128 Montgomery-form twiddle factors and their bound and divisibility properties.

Add MLKEM_NTT_Spec.thy and MLKEM_InvNTT_Spec.thy with butterfly, inner loop, middle loop, layer, and outer loop structure, plus bound propagation and overflow safety lemmas.

Add MLKEM_NTT_Correctness.thy with the 7-tier proof establishing that forward and inverse NTT compose to scaling by 2^16 mod q. Final theorems: poly_ntt_invntt_tomont and poly_invntt_tomont_ntt.

Add MLKEM_FC_Scalar.thy with contracts for barrett_reduce, poly_add, poly_sub, value_barrier, cast helpers, ct_sel, and ct_cmask.

…eduction Add MLKEM_FC_Montgomery.thy with contracts for montgomery_reduce, fqmul, and scalar_signed_to_unsigned_q.

…oops Add MLKEM_FC_PolyLoop.thy with contracts for poly_tomont, poly_reduce, and mulcache_compute (both _c inner loops and wrappers).

Add MLKEM_FC_NTT.thy with contracts for ntt_butterfly_block, ntt_layer, poly_ntt_c, and poly_ntt.

Add MLKEM_FC_InvNTT.thy with contracts for invntt_layer, poly_invntt_tomont_c, and poly_invntt_tomont.

… remove monolithic files Update ROOT with PDF output, document sections, and theory ordering. Update Makefile with build/pdf/clean targets. Add document/root.tex with LaTeX preamble. Update imports in MLKEM_Functional_Correctness.thy, MLKEM_Machine_Model.thy, and MLKEM_Poly_Definitions.thy. Remove superseded monolithic Common.thy and MLKEM_Poly_Functional_Correctness.thy.

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

DominicPM force-pushed the autocorrode-submodule branch from f3e0453 to 27ec4ff Compare March 17, 2026 22:29

DominicPM force-pushed the autocorrode-submodule branch from 27ec4ff to 13343ba Compare March 24, 2026 23:38

DominicPM added 11 commits March 25, 2026 21:11

proofs/isabelle: add AutoCorrode submodule

1a06a7f

Add the DominicPM/AutoCorrode fork as a submodule.

proofs/isabelle: add NTT zeta factor table and properties

00a4982

Add MLKEM_Zetas.thy with precomputed 128 Montgomery-form twiddle factors and their bound and divisibility properties.

proofs/isabelle: add forward and inverse NTT abstract specifications

fa0daf9

Add MLKEM_NTT_Spec.thy and MLKEM_InvNTT_Spec.thy with butterfly, inner loop, middle loop, layer, and outer loop structure, plus bound propagation and overflow safety lemmas.

proofs/isabelle: prove NTT/inverse-NTT are two-sided inverses mod q

d4d4645

Add MLKEM_NTT_Correctness.thy with the 7-tier proof establishing that forward and inverse NTT compose to scaling by 2^16 mod q. Final theorems: poly_ntt_invntt_tomont and poly_invntt_tomont_ntt.

proofs/isabelle: add C functional correctness proofs for scalar helpers

4236224

Add MLKEM_FC_Scalar.thy with contracts for barrett_reduce, poly_add, poly_sub, value_barrier, cast helpers, ct_sel, and ct_cmask.

proofs/isabelle: add C functional correctness proofs for Montgomery r…

4ac46e6

…eduction Add MLKEM_FC_Montgomery.thy with contracts for montgomery_reduce, fqmul, and scalar_signed_to_unsigned_q.

proofs/isabelle: add C functional correctness proofs for polynomial l…

fdd11d7

…oops Add MLKEM_FC_PolyLoop.thy with contracts for poly_tomont, poly_reduce, and mulcache_compute (both _c inner loops and wrappers).

proofs/isabelle: add C functional correctness proof of forward NTT

58ad228

Add MLKEM_FC_NTT.thy with contracts for ntt_butterfly_block, ntt_layer, poly_ntt_c, and poly_ntt.

proofs/isabelle: add C functional correctness proof of inverse NTT

e907b75

Add MLKEM_FC_InvNTT.thy with contracts for invntt_layer, poly_invntt_tomont_c, and poly_invntt_tomont.

DominicPM force-pushed the autocorrode-submodule branch from 13343ba to e9bc583 Compare March 25, 2026 21:31

mkannwischer self-assigned this Apr 2, 2026


		### 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