Add hol-server for programmatic HOL Light communication

Integrates hol_server (https://github.com/monadius/hol_server) to enable
TCP-based communication with HOL Light. This allows sending commands
programmatically via netcat or the VS Code extension.

Usage: hol-server [port]  # default port is 2012

Update documentation accordingly.

- Ported from pq-code-package/mldsa-native#883

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

flake.nix

@@ -1,3 +1,5 @@
+# Copyright (c) The mlkem-native project authors
+# Copyright (c) The mldsa-native project authors
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
 {
@@ -80,25 +82,26 @@
           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
                   zig_0_13;
               } ++ pkgs.lib.optionals (!pkgs.stdenv.isDarwin) [ config.packages.valgrind_varlat ];
           };
 
+          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 gcc-arm-embedded; };
+            packages = builtins.attrValues { inherit (config.packages) linters toolchains hol_light s2n_bignum gcc-arm-embedded 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 gcc-arm-embedded; };
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_aarch64 hol_light s2n_bignum gcc-arm-embedded 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 gcc-arm-embedded; };
+            packages = builtins.attrValues { inherit (config.packages) linters toolchain_x86_64 hol_light s2n_bignum gcc-arm-embedded 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,40 @@
+#!/usr/bin/env bash
+# Copyright (c) The mldsa-native project authors
+# Copyright (c) The mlkem-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 proofs directory if in mlkem-native repo
+PROOF_DIR="$(git rev-parse --show-toplevel 2>/dev/null)/proofs/hol_light"
+[ -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,28 @@
+# Copyright (c) The mldsa-native project authors
+# Copyright (c) The mlkem-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

@@ -1,3 +1,5 @@
+# Copyright (c) The mlkem-native project authors
+# Copyright (c) The mldsa-native project authors
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
 { pkgs, cbmc, bitwuzla, z3 }:
@@ -100,6 +102,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

@@ -77,6 +77,23 @@ will build and run the proofs. Note that this make take hours even on powerful m
 
 For convenience, you can also use `tests hol_light` which wraps the `make` invocation above; see `tests hol_light --help`.
 
+## 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?
 
 All AArch64 assembly routines used in mlkem-native are covered. Those are: