Hol-Light: Add Hol-light proof framework and Forward NTT proof

Add HOL-Light framework with NTT proof. This includes:
- list_proofs.sh, build-proof.sh, dump_bytecode.ml utilities
- mldsa-specs.ml and mldsa-utils.ml to support HOL-Light proofs
- HOL-Light proof for ML-DSA x86 AVX2 NTT in mldsa_ntt.ml
- Addition of hol_light to scripts/tests to wrap and run proofs
- READMEs for usage descriptions

Signed-off-by: Jake Massimo <jakemas@amazon.com>

Author: jakemas

flake.nix

@@ -100,8 +100,8 @@
           }).overrideAttrs (old: {
             shellHook = ''
               export PATH=$PWD/scripts:$PATH
-              # Set PROOF_DIR_ARM based on where we entered the shell
-              export PROOF_DIR_ARM="$PWD/proofs/hol_light/arm"
+              # Set proof directory for x86_64
+              export PROOF_DIR_X86_64="$PWD/proofs/hol_light/x86_64"
             '';
           });
           devShells.ci = util.mkShell {

nix/hol_light/0005-Configure-hol-sh-for-mldsa-native.patch

@@ -21,10 +21,10 @@ index 1311255..8b2bc36 100755
 +SITELIB=$(dirname $(ocamlfind query findlib 2>/dev/null) 2>/dev/null)
 +
 +# Set HOLLIGHT_LOAD_PATH to include S2N_BIGNUM_DIR and mldsa-native proofs
-+export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_ARM}:${HOLLIGHT_LOAD_PATH}"
++export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_X86_64}:${HOLLIGHT_LOAD_PATH}"
 +
 +# Change to mldsa-native proofs directory if set, so define_from_elf can find object files
-+[ -n "${PROOF_DIR_ARM}" ] && cd "${PROOF_DIR_ARM}"
++[ -n "${PROOF_DIR_X86_64}" ] && cd "${PROOF_DIR_X86_64}"
 +
 +${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOL_ML_PATH} -I ${HOLLIGHT_DIR} ${SITELIB:+-I "$SITELIB"}
 diff --git a/hol_4.sh b/hol_4.sh

nix/s2n_bignum/default.nix

@@ -4,12 +4,12 @@
 { stdenv, fetchFromGitHub, writeText, ... }:
 stdenv.mkDerivation rec {
   pname = "s2n_bignum";
-  version = "1fcccc89cc7762ae5c56ec660f25b5f1358ba308";
+  version = "2ab2252b8505e58a7c3392f8ad823782032b61e7";
   src = fetchFromGitHub {
-    owner = "jargh";
-    repo = "s2n-bignum-dev";
+    owner = "awslabs";
+    repo = "s2n-bignum";
     rev = "${version}";
-    hash = "sha256-hSJ2WlrwVlTF3wSdMfdBbovBXMG5vltfPxp36hOMd5c=";
+    hash = "sha256-7lil3jAFo5NiyNOSBYZcRjduXkotV3x4PlxXSKt63M8=";
   };
   setupHook = writeText "setup-hook.sh" ''
     export S2N_BIGNUM_DIR="$1"

proofs/README.md

@@ -7,3 +7,7 @@ This directory contains material related to the formal verification of the sourc
 ## C verification: CBMC
 
 We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to show the absence of various classes of undefined behaviour in the mldsa-native C source, including out of bounds memory accesses and integer overflows. See [proofs/cbmc](cbmc), or the [proof_guide](https://github.com/pq-code-package/mlkem-native/blob/main/proofs/cbmc/proof_guide.md).
+
+## 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 various highly optimized assembly routines in mlkem-native at the object-code level. See [proofs/hol_light/x86_64](hol_light/x86_64).

proofs/hol_light/.gitignore

@@ -0,0 +1,4 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+**/*.o
+**/*.native
+**/*.correct

proofs/hol_light/x86_64/Makefile

@@ -0,0 +1,133 @@
+#############################################################################
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0
+#############################################################################
+
+#
+# This Makefile is derived from the Makefile x86/Makefile in s2n-bignum.
+# - Remove all s2n-bignum proofs and tutorial, add mldsa-native proofs
+# - Minor path modifications to support base theories from s2n-bignum
+#   to reside in a separate read-only directory
+#
+
+.DEFAULT_GOAL := run_proofs
+
+OSTYPE_RESULT=$(shell uname -s)
+ARCHTYPE_RESULT=$(shell uname -m)
+
+SRC ?= $(S2N_BIGNUM_DIR)
+SRC_X86 ?= $(SRC)/x86
+
+# Add explicit language input parameter to cpp, otherwise the use of #n for
+# numeric literals in x86 code is a problem when used inside #define macros
+# since normally that means stringization.
+#
+# Some clang-based preprocessors seem to behave differently, and get confused
+# by single-quote characters in comments, so we eliminate // comments first.
+
+ifeq ($(OSTYPE_RESULT),Darwin)
+PREPROCESS=sed -e 's/\/\/.*//' | $(CC) -E -xassembler-with-cpp -
+else
+PREPROCESS=$(CC) -E -xassembler-with-cpp -
+endif
+
+# Generally GNU-type assemblers are happy with multiple instructions on
+# a line, but we split them up anyway just in case.
+
+SPLIT=tr ';' '\n'
+
+# If actually on an x86_64 machine, just use the assembler (as). Otherwise
+# use a cross-assembling version so that the code can still be assembled
+# and the proofs checked against the object files (though you won't be able
+# to run code without additional emulation infrastructure). For the clang
+# version on OS X we just add the "-arch x86_64" option. For the Linux/gcc
+# toolchain we assume the presence of the special cross-assembler. This
+# can be installed via something like:
+#
+#  sudo apt-get install binutils-x86-64-linux-gnu
+
+ifeq ($(ARCHTYPE_RESULT),x86_64)
+ASSEMBLE=as
+OBJDUMP=objdump -d
+else
+ifeq ($(OSTYPE_RESULT),Darwin)
+ASSEMBLE=as -arch x86_64
+OBJDUMP=otool -tvV
+else
+ASSEMBLE=x86_64-linux-gnu-as
+OBJDUMP=x86_64-linux-gnu-objdump -d
+endif
+endif
+
+OBJ = mldsa/mldsa_ntt.o
+
+# Build object files from assembly sources
+$(OBJ): %.o : %.S
+	@echo "Preparing $@ ..."
+	@echo "AS: `$(ASSEMBLE) --version`"
+	@echo "OBJDUMP: `$(OBJDUMP) --version`"
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
+	# MacOS may generate relocations in non-text sections that break
+	# the object file parser in HOL-Light
+	strip $@
+
+clean:; rm -f */*.o */*/*.o */*.correct */*.native
+
+# Proof-related parts
+#
+# The proof files are all independent, though each one loads the
+# same common infrastructure "base.ml". So you can potentially
+# run the proofs in parallel for more speed, e.g.
+#
+#    nohup make -j 16 proofs &
+#
+# If you build hol-light yourself (see https://github.com/jrh13/hol-light)
+# in your home directory, and do "make" inside the subdirectory hol-light,
+# then the following HOLDIR setting should be right:
+
+HOLDIR?=$(HOLLIGHTDIR)
+HOLLIGHT:=$(HOLDIR)/hol.sh
+
+BASE?=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST))))
+
+PROOF_BINS = $(OBJ:.o=.native)
+PROOF_LOGS = $(OBJ:.o=.correct)
+
+# Build precompiled binary for dumping bytecodes
+proofs/dump_bytecode.native: proofs/dump_bytecode.ml $(OBJ)
+	./proofs/build-proof.sh $(BASE)/$< "$(HOLLIGHT)" "$@"
+
+# Build precompiled native binaries of HOL Light proofs
+
+.SECONDEXPANSION:
+%.native: proofs/$$(*F).ml %.o ; ./proofs/build-proof.sh $(BASE)/$< "$(HOLLIGHT)" "$@"
+
+# Run them and print the standard output+error at *.correct
+%.correct: %.native
+	$< 2>&1 | tee $@
+	@if (grep -i "error:\|exception:" "$@" >/dev/null); then  \
+		echo "$< had errors!";			          \
+		exit 1;					          \
+	else							  \
+		echo "$< OK";					  \
+	fi
+
+build_proofs: $(PROOF_BINS);
+run_proofs: build_proofs $(PROOF_LOGS);
+
+proofs: run_proofs ; $(SRC)/tools/count-proofs.sh .
+
+dump_bytecode: proofs/dump_bytecode.native
+	./$<
+
+.PHONY: proofs build_proofs run_proofs sematest clean dump_bytecode
+
+# Always run sematest regardless of dependency check
+FORCE: ;
+# Always use max. # of cores because in Makefile one cannot get the passed number of -j.
+# A portable way of getting the number of max. cores:
+# https://stackoverflow.com/a/23569003/1488216
+NUM_CORES_FOR_SEMATEST = $(shell getconf _NPROCESSORS_ONLN)
+sematest: FORCE $(OBJ) $(SRC_X86)/proofs/simulator_iclasses.ml $(SRC_X86)/proofs/simulator.native
+	$(SRC)/tools/run-sematest.sh x86 $(NUM_CORES_FOR_SEMATEST)

proofs/hol_light/x86_64/README.md

@@ -0,0 +1,99 @@
+[//]: # (SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0)
+
+# HOL Light functional correctness proofs
+
+This directory contains functional correctness proofs for all x86_64 assembly routines
+used in mldsa-native. The proofs were largely developed by John Harrison and Jake Massimo,
+and are written in the [HOL Light](https://hol-light.github.io/) theorem
+prover, utilizing the assembly verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum).
+
+Each function is proved in a separate `.ml` file in [proofs/](proofs). Each file
+contains the byte code being verified, as well as the specification that is being
+proved.
+
+## Primer
+
+Proofs are 'post-hoc' in the sense that HOL-Light/s2n-bignum operate on the final object code. In particular, the means by which the code was generated need not be trusted.
+
+Specifications are essentially [Hoare triples](https://en.wikipedia.org/wiki/Hoare_logic), with the noteworthy difference that the program is implicit as the content of memory at the PC; which is asserted to
+be the code under verification as part of the precondition. For example, the following is the specification of the `mldsa_ntt` function:
+
+```ocaml
+ (* For all (abbreviated by `!` in HOL):
+    - a: Polynomial coefficients pointer  
+    - zetas: NTT constants pointer
+    - x: Original polynomial coefficients
+    - pc: Current value of Program Counter (PC)
+    - stackpointer: Stack pointer
+    - returnaddress: Return address on the stack *)
+`!a zetas x pc stackpointer returnaddress.
+    (* Alignment and non-overlapping requirements *)
+    aligned 32 a /\
+    aligned 32 zetas /\
+    nonoverlapping (word pc,LENGTH mldsa_ntt_mc) (a, 1024) /\
+    nonoverlapping (word pc,LENGTH mldsa_ntt_mc) (zetas, 2496) /\
+    nonoverlapping (a, 1024) (zetas, 2496) /\
+    nonoverlapping (stackpointer,8) (a, 1024) /\
+    nonoverlapping (stackpointer,8) (zetas, 2496)
+    ==> ensures x86
+      (* Precondition *)
+      (\s. (* The memory at the current PC is the byte-code of mldsa_ntt() *)
+        bytes_loaded s (word pc) mldsa_ntt_mc /\
+        read RIP s = word pc /\
+        read RSP s = stackpointer /\
+        (* The return address is on the stack *)
+        read (memory :> bytes64 stackpointer) s = returnaddress /\
+        (* Arguments are passed via C calling convention *)
+        C_ARGUMENTS [a; zetas] s /\
+        (* NTT constants are properly loaded *)
+        wordlist_from_memory(zetas,624) s = MAP (iword: int -> 32 word) mldsa_complete_qdata /\
+        (* Input bounds checking *)
+        (!i. i < 256 ==> abs(ival(x i)) <= &8380416) /\
+        (* Give a name to the memory contents at the source pointer *)
+        !i. i < 256
+            ==> read(memory :> bytes32(word_add a (word(4 * i)))) s = x i)
+      (* Postcondition: Eventually we reach a state where ... *)
+      (\s.
+        (* The PC is the return address *)
+        read RIP s = returnaddress /\
+        (* Stack pointer is adjusted *)
+        read RSP s = word_add stackpointer (word 8) /\
+        (* The integers represented by the final memory contents
+         * are congruent to the ML-DSA forward NTT transformation
+         * of the original coefficients, modulo 8380417, with proper bounds *)
+        !i. i < 256
+            ==> let zi = read(memory :> bytes32(word_add a (word(4 * i)))) s in
+                (ival zi == mldsa_forward_ntt (ival o x) i) (mod &8380417) /\
+                abs(ival zi) <= &42035261)
+      (* Footprint: The program may modify (only) the ABI permitted registers
+       * and flags, stack pointer, and the memory contents at the source pointer. *)
+      (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
+       MAYCHANGE [memory :> bytes(a,1024)])`
+```
+
+## Reproducing the proofs
+
+To reproduce the proofs, enter the nix shell via
+
+```bash
+nix develop --experimental-features 'nix-command flakes'
+```
+
+from mldsa-native's base directory. Then
+
+```bash
+make -C proofs/hol_light/x86_64
+```
+
+will build and run the proofs. Note that this make take hours even on powerful machines.
+
+For convenience, you can also use `tests hol_light` which wraps the `make` invocation above; see `tests hol_light --help`.
+
+## What is covered?
+
+All x86_64 assembly routines used in mldsa-native are covered. Currently this includes:
+
+- ML-DSA Arithmetic:
+  * x86_64 forward NTT: [mldsa_ntt.S](mldsa/mldsa_ntt.S)
+
+The NTT function is optimized using AVX2 instructions and follows the s2n-bignum x86_64 assembly verification patterns.

proofs/hol_light/x86_64/list_proofs.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+#
+# This tiny script just lists the names of source files for which
+# we have a spec and proof in HOL-Light.
+
+ROOT=$(git rev-parse --show-toplevel)
+cd $ROOT
+ls -1 proofs/hol_light/x86_64/mldsa/*.S | cut -d '/' -f 5 | sed 's/\.S//'