HOL-Light: Add HOL-Light proof framework and x86 AVX2 NTT proof

.github/workflows/hol_light.yml

@@ -0,0 +1,114 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+name: HOL-Light
+permissions:
+  contents: read
+on:
+  push:
+    branches: ["main"]
+    paths:
+     - '.github/workflows/hol_light.yml'
+     - 'proofs/hol_light/x86_64/Makefile'
+     - 'proofs/hol_light/x86_64/**/*.S'
+     - 'proofs/hol_light/x86_64/**/*.ml'
+     - 'nix/hol_light/*'
+     - 'nix/s2n_bignum/*'
+  pull_request:
+    branches: ["main"]
+    paths:
+      - '.github/workflows/hol_light.yml'
+      - 'proofs/hol_light/x86_64/Makefile'
+      - 'proofs/hol_light/x86_64/**/*.S'
+      - 'proofs/hol_light/x86_64/**/*.ml'
+      - 'nix/hol_light/*'
+      - 'nix/s2n_bignum/*'
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  # The proofs also check that the byte code is up to date,
+  # but we use this as a fast path to not even start the proofs
+  # if the byte code needs updating.
+  hol_light_bytecode:
+    name: HOL-Light bytecode check
+    runs-on: pqcp-x64
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            autogen --update-hol-light-bytecode --dry-run
+  hol_light_interactive:
+    name: HOL-Light interactive shell test
+    runs-on: pqcp-x64
+    needs: [ hol_light_bytecode ]
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            # Load base infrastructure and specs to validate HOL-Light environment
+            # When we have smaller/faster proofs, we can run them here instead:
+            # make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
+            # echo 'needs "proofs/mldsa_ntt.ml";;' | hol.sh
+            echo 'needs "x86/proofs/base.ml";; needs "proofs/mldsa_specs.ml";; #quit;;' | hol.sh
+  hol_light_proofs:
+    needs: [ hol_light_bytecode ]
+    strategy:
+      fail-fast: false
+      matrix:
+        proof:
+          # Dependencies on {name}.{S,ml} are implicit
+          - name: mldsa_ntt
+            needs: ["mldsa_specs.ml", "mldsa_utils.ml"]
+    name: HOL Light proof for ${{ matrix.proof.name }}.S
+    runs-on: pqcp-x64
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
+        with:
+          fetch-depth: 0
+      - name: Get changed files
+        id: changed-files
+        uses: tj-actions/changed-files@24d32ffd492484c1d75e0c0b894501ddb9d30d62 # v47.0.0
+      - name: Check if dependencies changed
+        id: check_run
+        shell: bash
+        run: |
+          run_needed=0
+          changed_files="${{ steps.changed-files.outputs.all_changed_files }}"
+          dependencies="${{ join(matrix.proof.needs, ' ') }} ${{ format('{0}.S {0}.ml', matrix.proof.name) }}"
+          for changed in $changed_files; do
+            for needs in $dependencies; do
+               if [[ "$changed" == *"$needs" ]]; then
+                 run_needed=1
+               fi
+            done
+          done
+
+          # Always re-run upon change to nix files for HOL-Light
+          if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86_64/Makefile"* ]]; then
+            run_needed=1
+          fi
+
+          echo "run_needed=${run_needed}" >> $GITHUB_OUTPUT
+      - uses: ./.github/actions/setup-shell
+        if: |
+          steps.check_run.outputs.run_needed == '1'
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            tests hol_light -p ${{ matrix.proof.name }} --verbose

BIBLIOGRAPHY.md

@@ -228,6 +228,7 @@ source code and documentation.
   - [mldsa/src/native/x86_64/src/rej_uniform_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_avx2.c)
   - [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c)
   - [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
+  - [proofs/hol_light/x86_64/mldsa/mldsa_ntt.S](proofs/hol_light/x86_64/mldsa/mldsa_ntt.S)
 
 ### `Round3_Spec`
 

README.md

@@ -43,6 +43,13 @@ make test
 
 We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to prove absence of various classes of undefined behaviour in C, including out of bounds memory accesses and integer overflows. The proofs cover all C code in [mldsa/src/*](mldsa) and [mldsa/src/fips202/*](mldsa/src/fips202) involved in running mldsa-native with its C backend. See [proofs/cbmc](proofs/cbmc) for details.
 
+HOL-Light functional correctness proofs can be found in [proofs/hol_light/x86_64](proofs/hol_light/x86_64). So far, the following functions have been proven correct:
+
+- x86_64 NTT [ntt.S](mldsa/src/native/x86_64/src/ntt.S)
+
+
+These proofs are utilizing the verification infrastructure in [s2n-bignum](https://github.com/awslabs/s2n-bignum).
+
 ## Security
 
 All assembly in mldsa-native is constant-time in the sense that it is free of secret-dependent control flow, memory access,

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