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 the `sub`, `add`, and `barrett_reduction`
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.

Note for the time being there is no "inhabitant" or "model" of this machine
model, which is kept axiomatic.  As a consequence there is a small chance that
this model cannot actually be realized by an explicit construction.  Providing a
model is future work, and will be entirely straightforward.

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

@@ -66,6 +66,8 @@ interactive theorem prover and the [s2n-bignum](https://github.com/awslabs/s2n-b
 relevant parts of the Arm and x86 architectures). See [proofs/hol_light](proofs/hol_light) for details.
 The x86_64 FIPS-202 (Keccak) backend is still in C intrinsics and not yet covered by proof.
 
+Selected C/functional components are also verified in [Isabelle/HOL](https://isabelle.in.tum.de/) using AutoCorrode. See [proofs/isabelle](proofs/isabelle).
+
 ## Security
 
 All assembly in mlkem-native is constant-time in the sense that it is free of secret-dependent control flow, memory access,

README.md

@@ -11,3 +11,7 @@ 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 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).

proofs/README.md

@@ -0,0 +1,185 @@
+theory Common
+  imports MLKEM_Poly_Definitions "Micro_C_Examples.C_While_Examples"
+begin
+
+section \<open>Abstract polynomial arithmetic\<close>
+
+text \<open>We model mlkem-native polynomials abstractly as fixed-size coefficient
+  lists over the integers. This gives a clean mathematical specification
+  independent of machine word sizes.\<close>
+
+abbreviation MLKEM_N :: nat where
+  \<open>MLKEM_N \<equiv> 256\<close>
+
+type_synonym int_poly = \<open>int list\<close>
+
+definition poly_add_int :: \<open>int_poly \<Rightarrow> int_poly \<Rightarrow> int_poly\<close> where
+  \<open>poly_add_int ps qs = map2 (+) ps qs\<close>
+
+definition poly_sub_int :: \<open>int_poly \<Rightarrow> int_poly \<Rightarrow> int_poly\<close> where
+  \<open>poly_sub_int ps qs = map2 (-) ps qs\<close>
+
+subsection \<open>Barrett reduction\<close>
+
+abbreviation MLKEM_Q :: int where
+  \<open>MLKEM_Q \<equiv> 3329\<close>
+
+definition barrett_reduce_int :: \<open>int \<Rightarrow> int\<close> where
+  \<open>barrett_reduce_int a = a - ((20159 * a + 2^25) div 2^26) * MLKEM_Q\<close>
+
+lemma barrett_reduce_mod:
+  shows \<open>barrett_reduce_int a mod MLKEM_Q = a mod MLKEM_Q\<close>
+unfolding barrett_reduce_int_def by algebra
+
+section \<open>Concrete types and refinement\<close>
+
+text \<open>
+  Refinement relation: a concrete @{typ c_mlk_poly} refines an abstract
+  @{typ int_poly} when its coefficient list has the correct length and its
+  signed interpretation matches the abstract polynomial.
+\<close>
+definition refines_mlk_poly :: \<open>c_mlk_poly \<Rightarrow> int_poly \<Rightarrow> bool\<close> where
+  \<open>refines_mlk_poly cp ap \<longleftrightarrow>
+    length (c_mlk_poly_coeffs cp) = MLKEM_N \<and>
+    List.map sint (c_mlk_poly_coeffs cp) = ap\<close>
+
+text \<open>
+  No-overflow condition: the mathematical sum of each coefficient pair
+  fits in a signed 16-bit integer. This is required both for the C code
+  to not abort (since @{const c_signed_add} checks for overflow) and for
+  the refinement to integer arithmetic to hold.
+\<close>
+definition no_overflow_add :: \<open>int_poly \<Rightarrow> int_poly \<Rightarrow> bool\<close> where
+  \<open>no_overflow_add ps qs \<longleftrightarrow>
+    (\<forall>i < min (length ps) (length qs).
+      ps ! i + qs ! i \<in> {-(2^15) ..< 2^15})\<close>
+
+definition no_overflow_sub :: \<open>int_poly \<Rightarrow> int_poly \<Rightarrow> bool\<close> where
+  \<open>no_overflow_sub ps qs \<longleftrightarrow>
+    (\<forall>i < min (length ps) (length qs).
+      ps ! i - qs ! i \<in> {-(2^15) ..< 2^15})\<close>
+
+text \<open>
+  The concrete (word-level) result of polynomial addition — internal helper
+  for proofs.
+\<close>
+definition poly_add_c :: \<open>c_mlk_poly \<Rightarrow> c_mlk_poly \<Rightarrow> c_mlk_poly\<close> where
+  \<open>poly_add_c p q = update_c_mlk_poly_coeffs
+    (\<lambda>_. map2 (+) (c_mlk_poly_coeffs p) (c_mlk_poly_coeffs q)) p\<close>
+
+subsection \<open>Refinement lemmas\<close>
+
+lemma sint_plus_no_overflow:
+    fixes a b :: \<open>'l::{len} sword\<close>
+  assumes \<open>sint a + sint b \<in> {-(2^(LENGTH('l) - 1)) ..< 2^(LENGTH('l) - 1)}\<close>
+    shows \<open>sint (a + b) = sint a + sint b\<close>
+using assms by (intro signed_arith_sint) (auto simp: word_size)
+
+lemma sint_minus_no_overflow:
+    fixes a b :: \<open>'l::{len} sword\<close>
+  assumes \<open>sint a - sint b \<in> {-(2^(LENGTH('l) - 1)) ..< 2^(LENGTH('l) - 1)}\<close>
+    shows \<open>sint (a - b) = sint a - sint b\<close>
+using assms by (intro signed_arith_sint) (auto simp: word_size)
+
+text \<open>
+  The key refinement theorem: under the no-overflow condition, the concrete
+  word-level addition produces a result that refines the abstract integer sum.
+\<close>
+lemma poly_add_c_refines:
+  assumes \<open>refines_mlk_poly p ap\<close>
+      and \<open>refines_mlk_poly q aq\<close>
+      and \<open>no_overflow_add ap aq\<close>
+    shows \<open>refines_mlk_poly (poly_add_c p q) (poly_add_int ap aq)\<close>
+using assms by (auto simp add: c_mlk_poly.record_simps map2_map_map word_size refines_mlk_poly_def
+  poly_add_c_def poly_add_int_def no_overflow_add_def intro!: nth_equalityI sint_plus_no_overflow)
+
+subsection \<open>Auxiliary Lemmas\<close>
+
+lemma nth_map2:
+  assumes \<open>i < length xs\<close>
+      and \<open>i < length ys\<close>
+    shows \<open>map2 f xs ys ! i = f (xs ! i) (ys ! i)\<close>
+using assms by (induction xs arbitrary: i ys) (auto simp: less_Suc_eq_0_disj split: list.splits)
+
+lemma inv_list_step:
+  assumes \<open>n < length xs\<close>
+      and \<open>n < length ys\<close>
+      and \<open>length xs = length ys\<close>
+    shows \<open>(take n (map2 f xs ys) @ drop n xs)[n := f (xs ! n) (ys ! n)] =
+              take (Suc n) (map2 f xs ys) @ drop (Suc n) xs\<close>
+proof -
+  let ?zs = \<open>map2 f xs ys\<close>
+  from assms have ln: \<open>n < length ?zs\<close>
+    by simp
+  from assms have zn: \<open>?zs ! n = f (xs ! n) (ys ! n)\<close>
+    by (simp add: nth_map2)
+  from assms have drop_eq: \<open>drop n xs = xs ! n # drop (Suc n) xs\<close>
+    by (metis Cons_nth_drop_Suc)
+  have \<open>(take n ?zs @ drop n xs)[n := ?zs ! n] = take n ?zs @ (drop n xs)[0 := ?zs ! n]\<close>
+    using ln by (simp add: list_update_append)
+  also have \<open>\<dots> = take n ?zs @ ?zs ! n # drop (Suc n) xs\<close>
+    using drop_eq by simp
+  also have \<open>\<dots> = take (Suc n) ?zs @ drop (Suc n) xs\<close>
+    using ln by (simp add: take_Suc_conv_app_nth)
+  finally show ?thesis
+    using zn by simp
+qed
+
+lemma no_overflow_add_bounds:
+  assumes \<open>refines_mlk_poly vr ar\<close>
+      and \<open>refines_mlk_poly vb ab\<close>
+      and \<open>no_overflow_add ar ab\<close> \<open>i < MLKEM_N\<close>
+    shows \<open>sint (c_mlk_poly_coeffs vr ! i) + sint (c_mlk_poly_coeffs vb ! i) < 2 ^ 15\<close>
+      and \<open>- (2 ^ 15) \<le> sint (c_mlk_poly_coeffs vr ! i) + sint (c_mlk_poly_coeffs vb ! i)\<close>
+proof -
+  from assms(1) have lr: \<open>length (c_mlk_poly_coeffs vr) = MLKEM_N\<close>
+          and mr: \<open>List.map sint (c_mlk_poly_coeffs vr) = ar\<close>
+    unfolding refines_mlk_poly_def by auto
+  from assms(2) have lb: \<open>length (c_mlk_poly_coeffs vb) = MLKEM_N\<close>
+          and mb: \<open>List.map sint (c_mlk_poly_coeffs vb) = ab\<close>
+    unfolding refines_mlk_poly_def by auto
+  have \<open>ar ! i + ab ! i \<in> {-(2^15) ..< 2^15}\<close>
+    using assms(3,4) lr lb mr mb unfolding no_overflow_add_def by auto
+  moreover have \<open>ar ! i = sint (c_mlk_poly_coeffs vr ! i)\<close>
+    using mr lr assms(4) by (simp add: nth_map[symmetric])
+  moreover have \<open>ab ! i = sint (c_mlk_poly_coeffs vb ! i)\<close>
+    using mb lb assms(4) by (simp add: nth_map[symmetric])
+  ultimately show \<open>sint (c_mlk_poly_coeffs vr ! i) + sint (c_mlk_poly_coeffs vb ! i) < 2 ^ 15\<close>
+          and \<open>- (2 ^ 15) \<le> sint (c_mlk_poly_coeffs vr ! i) + sint (c_mlk_poly_coeffs vb ! i)\<close>
+    by auto
+qed
+
+lemma no_overflow_sub_bounds:
+  assumes \<open>refines_mlk_poly vr ar\<close>
+      and \<open>refines_mlk_poly vb ab\<close>
+      and \<open>no_overflow_sub ar ab\<close> \<open>i < MLKEM_N\<close>
+    shows \<open>sint (c_mlk_poly_coeffs vr ! i) - sint (c_mlk_poly_coeffs vb ! i) < 2 ^ 15\<close>
+      and \<open>- (2 ^ 15) \<le> sint (c_mlk_poly_coeffs vr ! i) - sint (c_mlk_poly_coeffs vb ! i)\<close>
+proof -
+  from assms(1) have lr: \<open>length (c_mlk_poly_coeffs vr) = MLKEM_N\<close>
+          and mr: \<open>List.map sint (c_mlk_poly_coeffs vr) = ar\<close>
+    unfolding refines_mlk_poly_def by auto
+  from assms(2) have lb: \<open>length (c_mlk_poly_coeffs vb) = MLKEM_N\<close>
+          and mb: \<open>List.map sint (c_mlk_poly_coeffs vb) = ab\<close>
+    unfolding refines_mlk_poly_def by auto
+  have \<open>ar ! i - ab ! i \<in> {-(2^15) ..< 2^15}\<close>
+    using assms(3,4) lr lb mr mb unfolding no_overflow_sub_def by auto
+  moreover have \<open>ar ! i = sint (c_mlk_poly_coeffs vr ! i)\<close>
+    using mr lr assms(4) by (simp add: nth_map[symmetric])
+  moreover have \<open>ab ! i = sint (c_mlk_poly_coeffs vb ! i)\<close>
+    using mb lb assms(4) by (simp add: nth_map[symmetric])
+  ultimately show \<open>sint (c_mlk_poly_coeffs vr ! i) - sint (c_mlk_poly_coeffs vb ! i) < 2 ^ 15\<close>
+          and \<open>- (2 ^ 15) \<le> sint (c_mlk_poly_coeffs vr ! i) - sint (c_mlk_poly_coeffs vb ! i)\<close>
+    by auto
+qed
+
+lemma MLKEM_N_sub_step [simp]:
+  assumes \<open>k < MLKEM_N\<close>
+    shows \<open>MLKEM_N - k = Suc (255 - k)\<close>
+using assms by simp
+
+lemma mlkem_rev_index_bound [simp]:
+  shows \<open>255 - k < MLKEM_N\<close>
+by simp
+
+end

proofs/isabelle/Common.thy

@@ -0,0 +1,12 @@
+theory MLKEM_Functional_Correctness
+  imports
+    MLKEM_Poly_Functional_Correctness
+begin
+
+text \<open>
+  Top-level entry point for \<^verbatim>\<open>mlkem-native\<close> functional-correctness proofs.
+
+  Intentionally empty, barring imports.
+\<close>
+
+end

proofs/isabelle/MLKEM_Functional_Correctness.thy

@@ -0,0 +1,35 @@
+theory MLKEM_Machine_Model
+  imports "Micro_C_Examples.Simple_C_Functions"
+begin
+
+text \<open>
+  Machine-model assumptions used by generated \<^verbatim>\<open>mlkem-native\<close> C definitions.
+  Types are extracted first so locale assumptions can depend on the generated
+  C record/datatype names.
+\<close>
+
+micro_c_file manifest: "generated/manifests/poly.types.manifest" "generated/c/poly.pre.c"
+
+locale c_mlk_machine_model =
+    reference reference_types +
+    ref_c_mlk_poly: reference_allocatable reference_types _ _ _ _ _ _ _ c_mlk_poly_prism +
+    ref_c_uint: reference_allocatable reference_types _ _ _ _ _ _ _ c_uint_prism +
+    ref_c_int: reference_allocatable reference_types _ _ _ _ _ _ _ c_int_prism +
+    ref_c_short: reference_allocatable reference_types _ _ _ _ _ _ _ c_short_prism
+  for reference_types :: \<open>'s::{sepalg} \<Rightarrow> 'addr \<Rightarrow> 'gv \<Rightarrow> c_abort \<Rightarrow> 'i prompt \<Rightarrow>
+        'o prompt_output \<Rightarrow> unit\<close>
+  and c_mlk_poly_prism :: \<open>('gv, c_mlk_poly) prism\<close>
+  and c_uint_prism :: \<open>('gv, c_uint) prism\<close>
+  and c_int_prism :: \<open>('gv, c_int) prism\<close>
+  and c_short_prism :: \<open>('gv, c_short) prism\<close>
+begin
+
+adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_mlk_poly.new
+adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_uint.new
+adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_int.new
+adhoc_overloading store_reference_const \<rightleftharpoons> ref_c_short.new
+adhoc_overloading store_update_const \<rightleftharpoons> update_fun
+
+end
+
+end