Add functional correctness proofs for AArch64-optimized NTT and invNTT in HOL Light

.github/workflows/ci.yml

@@ -370,7 +370,6 @@ jobs:
           acvp: false
           nix-shell: ${{ matrix.compiler.shell }}
           cflags: "-std=c17"
-  # The purpose of this job is to test non-default yet valid configurations
   config_variations:
     name: Non-standard configurations
     needs: [quickcheck, quickcheck-windows, quickcheck-c90, quickcheck-lib, examples, lint, lint-markdown-link]

.github/workflows/hol_light.yml

@@ -0,0 +1,37 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: HOL-Light
+permissions:
+  contents: read
+on:
+  push:
+    branches: ["main"]
+    # Only run upon changes to AArch64 NTT or invNTT
+    paths:
+     - 'proofs/hol_light/arm/**/*.S'
+  pull_request:
+    branches: ["main"]
+    paths:
+      # Only run upon changes to AArch64 NTT or invNTT
+      - 'proofs/hol_light/arm/**/*.S'
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  hol_light_proofs:
+    strategy:
+      matrix:
+        proof: [mlkem_ntt,mlkem_intt]
+    name: HOL Light proof for ${{ matrix.proof }}.S
+    runs-on: pqcp-arm64
+    if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      - uses: ./.github/actions/setup-shell
+        with:
+          gh_token: ${{ secrets.GITHUB_TOKEN }}
+          nix-shell: 'hol_light'
+          script: |
+            make -C proofs/hol_light/arm mlkem/${{ matrix.proof }}.correct

flake.nix

@@ -24,20 +24,28 @@
         in
         {
           packages.cbmc = util.cbmc;
+          packages.hol_light = pkgs.callPackage ./nix/hol_light { };
+          packages.s2n_bignum = pkgs.callPackage ./nix/s2n_bignum { };
 
           devShells.default = util.wrapShell util.mkShell {
             packages =
               util.core { } ++
               util.linters ++
               builtins.attrValues
                 {
-                  inherit (config.packages) cbmc;
+                  inherit (config.packages) cbmc hol_light s2n_bignum;
                   inherit (pkgs)
                     direnv
                     nix-direnv;
                 };
           };
 
+          devShells.hol_light = util.wrapShell util.mkShell {
+            packages = builtins.attrValues {
+              inherit (config.packages) hol_light s2n_bignum;
+            };
+          };
+
           devShells.ci = util.wrapShell util.mkShell { packages = util.core { cross = false; }; };
           devShells.ci-cross = util.wrapShell util.mkShell { packages = util.core { }; };
           devShells.ci-cbmc = util.wrapShell util.mkShell { packages = util.core { cross = false; } ++ [ config.packages.cbmc ]; };

nix/hol_light/0005-Fix-hollight-path.patch

@@ -0,0 +1,33 @@
+# SPDX-License-Identifier: Apache-2.0
+diff --git a/hol_4.14.sh b/hol_4.14.sh
+index 0fa0f64..313133e 100755
+--- a/hol_4.14.sh
++++ b/hol_4.14.sh
+@@ -5,7 +5,7 @@ export HOLLIGHT_DIR=__DIR__
+
+ if [ "$#" -eq 1 ]; then
+   if [ "$1" == "-pp" ]; then
+-    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
++    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I ${HOLLIGHT_DIR} pa_j.cmo"
+     exit 0
+   elif [ "$1" == "-dir" ]; then
+     echo "${HOLLIGHT_DIR}"
+diff --git a/hol_4.sh b/hol_4.sh
+index be55568..259ecae 100755
+--- a/hol_4.sh
++++ b/hol_4.sh
+@@ -5,7 +5,7 @@ export HOLLIGHT_DIR=__DIR__
+
+ if [ "$#" -eq 1 ]; then
+   if [ "$1" == "-pp" ]; then
+-    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo"
++    echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "${HOLLIGHT_DIR}" pa_j.cmo"}
+     exit 0
+   elif [ "$1" == "-dir" ]; then
+     echo "${HOLLIGHT_DIR}"
+@@ -27,4 +27,4 @@ if [ -d "${HOLLIGHT_DIR}/_opam" ]; then
+   eval $(opam env --switch "${HOLLIGHT_DIR}/" --set-switch)
+ fi
+
+-${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I `camlp5 -where` camlp5o.cma -init ${HOLLIGHT_DIR}/hol.ml -safe-string -I ${HOLLIGHT_DIR}
++${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I $(camlp5 -where) camlp5o.cma -init ${HOLLIGHT_DIR}/hol.ml -safe-string -I ${HOLLIGHT_DIR}

nix/hol_light/default.nix

@@ -0,0 +1,29 @@
+# SPDX-License-Identifier: Apache-2.0
+
+{ hol_light, fetchFromGitHub, writeText, ... }:
+hol_light.overrideAttrs (old: {
+  setupHook = writeText "setup-hook.sh" ''
+    export HOLDIR="$1/lib/hol_light"
+    export HOLLIGHT_DIR="$1/lib/hol_light"
+  '';
+  version = "unstable-2024-12-22";
+  src = fetchFromGitHub {
+    owner = "jrh13";
+    repo = "hol-light";
+    rev = "28e4aed1019a56fab869f752695a67a4164dd2ee";
+    hash = "sha256-Z14pED3oaz30Zp1Ue58KA5srlZc31WyDE8h9tJwCAcI=";
+  };
+  patches = [ ./0005-Fix-hollight-path.patch ];
+  propagatedBuildInputs = old.propagatedBuildInputs ++ old.nativeBuildInputs;
+  buildPhase = ''
+    HOLLIGHT_USE_MODULE=1 make hol.sh
+    patchShebangs hol.sh
+    HOLLIGHT_USE_MODULE=1 make
+  '';
+  installPhase = ''
+    mkdir -p "$out/lib/hol_light"
+    cp -a . $out/lib/hol_light
+    sed "s^__DIR__^$out/lib/hol_light^g; s^__USE_MODULE__^1^g" hol_4.14.sh > hol.sh
+    mv hol.sh $out/lib/hol_light/
+  '';
+})

nix/s2n_bignum/0001-fix-script-path.patch

@@ -0,0 +1,72 @@
+# SPDX-License-Identifier: Apache-2.0
+diff --git a/tools/build-proof.sh b/tools/build-proof.sh
+index 39d72433..d10c3244 100755
+--- a/tools/build-proof.sh
++++ b/tools/build-proof.sh
+@@ -1,6 +1,7 @@
+ #!/bin/bash
++ROOT="$(realpath "$(dirname "$0")"/../)"
+ if [ "$#" -ne 3 ]; then
+-  echo "../tools/build-proof.sh <.ml file path> <hol.sh> <output .native path>"
++  echo "${ROOT}/tools/build-proof.sh <.ml file path> <hol.sh> <output .native path>"
+   echo "This script builds HOL Light proof using OCaml native compiler and puts the "
+   echo "output binary at <output .native path>."
+   exit 1
+@@ -9,14 +10,11 @@ fi
+ # Return the exit code if any statement fails
+ set -e
+
+-s2n_bignum_arch=$(basename "$(pwd)")
+-
+-cd ..
+-
+-ml_path_noarch=$1
+-ml_path=${s2n_bignum_arch}/${ml_path_noarch}
++ml_path="$1"
+ hol_sh_cmd=$2
+-output_path=${s2n_bignum_arch}/$3
++output_path=$3
++output_dir=$(dirname "$output_path")
++[ -d "$output_dir" ] || mkdir -p "$output_dir"
+
+ export HOLLIGHT_DIR="$(dirname ${hol_sh_cmd})"
+ if [ ! -f "${HOLLIGHT_DIR}/hol_lib.cmxa" ]; then
+@@ -34,7 +32,7 @@ echo "Generating a template .ml that loads the file...: ${template_ml}"
+  echo "check_axioms ();;") >> ${template_ml}
+
+ spec_found=0
+-for spec in $(./tools/collect-specs.sh ${s2n_bignum_arch} ${ml_path_noarch}) ; do
++for spec in $("${ROOT}"/tools/collect-specs.sh "$(dirname "${ml_path}")" "${ml_path}"); do
+   echo "Printf.printf \"val ${spec} : thm = %s\n\" (string_of_thm ${spec});;"
+   spec_found=1
+ done >> ${template_ml}
+@@ -51,7 +49,7 @@ fi
+ inlined_prefix="$(mktemp)"
+ inlined_ml="${inlined_prefix}.ml"
+ inlined_cmx="${inlined_prefix}.cmx"
+-ocaml ${HOLLIGHT_DIR}/inline_load.ml ${template_ml} ${inlined_ml}
++(cd "$ROOT" && ocaml "${HOLLIGHT_DIR}"/inline_load.ml "${template_ml}" "${inlined_ml}")
+
+ # Give a large stack size.
+ OCAMLRUNPARAM=l=2000000000 \
+diff --git a/tools/collect-specs.sh b/tools/collect-specs.sh
+index a29aa6c8..784e0af3 100755
+--- a/tools/collect-specs.sh
++++ b/tools/collect-specs.sh
+@@ -6,14 +6,12 @@ if [ "$#" -ne 1 ] && [ "$#" -ne 2 ]; then
+   exit 1
+ fi
+
+-s2n_bignum_arch=$1
+ if [ "$#" -eq 2 ]; then
+   filepat="$2"
+ else
+-  filepat="*.ml"
++  filepat="$1"
+ fi
+-cd $s2n_bignum_arch > /dev/null
+
+ # An env. var for sorting
+ export LC_ALL=C
+-grep 'let [A-Z_0-9]*_SUBROUTINE_CORRECT' ${filepat} | cut -f2 -d' ' | sort
++grep -r 'let [A-Z_0-9]*_SUBROUTINE_CORRECT' ${filepat} | cut -f2 -d' ' | sort

nix/s2n_bignum/default.nix

@@ -0,0 +1,21 @@
+# SPDX-License-Identifier: Apache-2.0
+{ stdenv, fetchFromGitHub, writeText, ... }:
+stdenv.mkDerivation rec {
+  pname = "s2n_bignum";
+  version = "90cb5e35a823efee15cde72f0237af39a9bf7371";
+  src = fetchFromGitHub {
+    owner = "jargh";
+    repo = "s2n-bignum-dev";
+    rev = "${version}";
+    hash = "sha256-6uDvLG04h8IKYln612wG/aXPsCB9k8Zsh/cE2Y980tQ=";
+  };
+  setupHook = writeText "setup-hook.sh" ''
+    export S2N_BIGNUM_DIR="$1"
+  '';
+  patches = [ ./0001-fix-script-path.patch ];
+  dontBuild = true;
+  installPhase = ''
+    mkdir -p $out
+    cp -a . $out/
+  '';
+}

proofs/hol_light/.gitignore

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

proofs/hol_light/arm/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 arm/Makefile in s2n-bignum.
+# - Remove all s2n-bignum proofs and tutorial, add mlkem-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_ARM ?= $(SRC)/arm
+
+# Add explicit language input parameter to cpp, otherwise the use of #n for
+# numeric literals in ARM 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 -I$(SRC)/include $(SYMBOL_HIDING) -xassembler-with-cpp -
+else
+PREPROCESS=$(CC) -E -I$(SRC)/include $(SYMBOL_HIDING) -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 ARM8 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 arm64" 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-aarch64-linux-gnu
+
+ifeq ($(ARCHTYPE_RESULT),aarch64)
+ASSEMBLE=as
+OBJDUMP=objdump -d
+else
+ifeq ($(ARCHTYPE_RESULT),arm64)
+ASSEMBLE=as
+OBJDUMP=objdump -d
+else
+ifeq ($(OSTYPE_RESULT),Darwin)
+ASSEMBLE=as -arch arm64
+OBJDUMP=otool -tvV
+else
+ASSEMBLE=aarch64-linux-gnu-as
+OBJDUMP=aarch64-linux-gnu-objdump -d
+endif
+endif
+endif
+
+OBJ = mlkem/mlkem_ntt.o mlkem/mlkem_intt.o
+
+# According to
+# https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,
+# x18 should not be used for Apple platforms. Check this using grep.
+$(OBJ): %.o : %.S
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	cat $< | $(PREPROCESS) | $(SPLIT) | grep -v -E '^\s+.quad\s+0x[0-9a-f]+$$' | $(ASSEMBLE) -o $@ -
+	$(OBJDUMP) $@ | ( ( ! grep --ignore-case -E 'w18|[^0]x18' ) || ( rm $@ ; exit 1 ) )
+	cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
+
+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 native binaries of HOL Light proofs
+
+proofs/simulator.native: $(SRC_ARM)/proofs/simulator.ml
+	$(Q)[ -d $(@D) ] || mkdir -p $(@D)
+	$(SRC)/tools/build-proof.sh $(SRC_ARM)/proofs/simulator.ml "$(HOLLIGHT)" "$@"
+
+.SECONDEXPANSION:
+%.native: proofs/$$(*F).ml %.o ; $(SRC)/tools/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 .
+
+.PHONY: proofs build_proofs run_proofs sematest clean
+
+# 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_ARM)/proofs/simulator_iclasses.ml $(SRC_ARM)/proofs/simulator.native
+	$(SRC)/tools/run-sematest.sh arm $(NUM_CORES_FOR_SEMATEST)