diff --git a/flake.nix b/flake.nix index 6a7a4e35c..22fce2885 100644 --- a/flake.nix +++ b/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; }; diff --git a/nix/hol_light/hol-server.sh b/nix/hol_light/hol-server.sh new file mode 100644 index 000000000..7d1ca52dd --- /dev/null +++ b/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" diff --git a/nix/hol_light/hol_server.nix b/nix/hol_light/hol_server.nix new file mode 100644 index 000000000..6568e89ed --- /dev/null +++ b/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; +} diff --git a/nix/util.nix b/nix/util.nix index 5b53e60d4..5a116ac38 100644 --- a/nix/util.nix +++ b/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 { }; diff --git a/proofs/hol_light/README.md b/proofs/hol_light/README.md new file mode 100644 index 000000000..1bf064db1 --- /dev/null +++ b/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)