Add hol-server for programmatic HOL Light communication

flake.nix

@@ -81,7 +81,7 @@
           devShells.default = util.mkShell {
             packages = builtins.attrValues
               {
-                inherit (config.packages) linters cbmc hol_light s2n_bignum slothy toolchains_native;
+                inherit (config.packages) linters cbmc hol_light s2n_bignum slothy toolchains_native hol_server;
                 inherit (pkgs)
                   direnv
                   nix-direnv
@@ -101,17 +101,18 @@
           };
 
           devShells.avr = util.mkShell (import ./nix/avr { inherit pkgs; });
+          packages.hol_server = util.hol_server.hol_server_start;
           devShells.hol_light = (util.mkShell {
-            packages = builtins.attrValues { inherit (config.packages) linters hol_light s2n_bignum; };
+            packages = builtins.attrValues { inherit (config.packages) linters hol_light s2n_bignum hol_server; };
           }).overrideAttrs (old: { shellHook = holLightShellHook; });
           devShells.hol_light-cross = (util.mkShell {
-            packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum; };
+            packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum hol_server; };
           }).overrideAttrs (old: { shellHook = holLightShellHook; });
           devShells.hol_light-cross-aarch64 = (util.mkShell {
-            packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum; };
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum hol_server; };
           }).overrideAttrs (old: { shellHook = holLightShellHook; });
           devShells.hol_light-cross-x86_64 = (util.mkShell {
-            packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum; };
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum hol_server; };
           }).overrideAttrs (old: { shellHook = holLightShellHook; });
           devShells.ci = util.mkShell {
             packages = builtins.attrValues { inherit (config.packages) linters toolchains_native; };

nix/hol_light/hol-server.sh

@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+#
+# HOL Light server for programmatic communication
+# Based on https://github.com/monadius/hol_server
+#
+# Usage: hol-server [port]
+
+set -e
+
+PORT=${1:-2012}
+
+# These are replaced by nix
+HOL_LIGHT_DIR="@hol_light@/lib/hol_light"
+HOL_SERVER_SRC="@hol_server_src@"
+
+# cd to x86_64 proofs directory if in mldsa-native repo
+PROOF_DIR="$(git rev-parse --show-toplevel 2>/dev/null)/proofs/hol_light/x86_64"
+[ -d "$PROOF_DIR" ] && cd "$PROOF_DIR"
+
+echo "Starting HOL Light server on port $PORT..."
+
+{
+  # Load required libraries for server2.ml
+  echo '#directory "+unix";;'
+  echo '#directory "+threads";;'
+  echo '#load "unix.cma";;'
+  echo '#load "threads.cma";;'
+
+  # Load the server using #use (not loads) for proper evaluation
+  echo "#use \"$HOL_SERVER_SRC/server2.ml\";;"
+
+  # Start the server
+  echo "start ~single_connection:false $PORT;;"
+
+  # Keep stdin open for the server to continue running
+  cat
+} | exec "$HOL_LIGHT_DIR/hol.sh"

nix/hol_light/hol_server.nix

@@ -0,0 +1,27 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+# HOL Light server for programmatic communication
+# Based on https://github.com/monadius/hol_server
+{ fetchFromGitHub, runCommand, hol_light' }:
+
+let
+  hol_server_src = fetchFromGitHub {
+    owner = "monadius";
+    repo = "hol_server";
+    rev = "vscode";
+    hash = "sha256-o98ule5uuazm36+ppsvX2KCbtVbVwzHxGboUhbbrPCQ=";
+  };
+
+  hol_server_start = runCommand "hol-server" { } ''
+    mkdir -p $out/bin
+    substitute ${./hol-server.sh} $out/bin/hol-server \
+      --replace-fail "@hol_light@" "${hol_light'}" \
+      --replace-fail "@hol_server_src@" "${hol_server_src}"
+    chmod +x $out/bin/hol-server
+  '';
+
+in
+{
+  inherit hol_server_src hol_server_start;
+}

nix/util.nix

@@ -101,6 +101,7 @@ rec {
 
   valgrind_varlat = pkgs.callPackage ./valgrind { };
   hol_light' = pkgs.callPackage ./hol_light { };
+  hol_server = pkgs.callPackage ./hol_light/hol_server.nix { inherit hol_light'; };
   s2n_bignum = pkgs.callPackage ./s2n_bignum { };
   slothy = pkgs.callPackage ./slothy { };
   m55-an547 = pkgs.callPackage ./m55-an547-arm-none-eabi { };

proofs/hol_light/README.md

@@ -0,0 +1,47 @@
+[//]: # (SPDX-License-Identifier: CC-BY-4.0)
+
+# HOL Light functional correctness proofs
+
+This directory contains functional correctness proofs for x86_64 assembly routines
+used in mldsa-native. The proofs 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 [x86_64/proofs/](x86_64/proofs). Each file
+contains the byte code being verified, as well as the specification that is being proved.
+
+## Reproducing the proofs
+
+To reproduce the proofs, enter the nix shell via
+
+```bash
+nix develop .#hol_light --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 may take hours even on powerful machines.
+
+## Interactive proof development
+
+For interactive proof development, start the HOL Light server:
+
+```bash
+hol-server [port]  # default port is 2012
+```
+
+Then use the [HOL Light extension for VS Code](https://marketplace.visualstudio.com/items?itemName=monadius.hol-light-simple)
+to connect and send commands interactively.
+
+Alternatively, send commands using netcat:
+
+```bash
+echo '1+1;;' | nc -w 5 127.0.0.1 2012
+```
+
+## What is covered?
+
+- x86_64 forward NTT: [mldsa_ntt.S](x86_64/mldsa/mldsa_ntt.S)