From ca31bc35784e7e751549bc0f804be23b201f4e16 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Tue, 2 Jun 2026 22:30:47 +0800 Subject: [PATCH] Nix: add isabelle devShell and CI build of the Isabelle proofs Add a `nix develop .#isabelle` shell that provides Isabelle (2025-2, pulled from nixpkgs-unstable via the overlay), a TeX distribution for the NeonNTT PDF, and exports ISABELLE_VERSION, ISABELLE_DIR, and ISABELLE_HOME so the proofs/isabelle Makefiles work without manual configuration. Drive both Isabelle developments through that shell in CI. Standardize on Isabelle2025-2 across the Makefiles, docs, and the isabelle.yml Docker images, and add a top-level proofs/isabelle/README.md documenting how to obtain Isabelle; the per-development READMEs now refer to it for installation. Signed-off-by: Matthias J. Kannwischer --- .github/workflows/isabelle.yml | 19 +++++++++- flake.nix | 20 ++++++++++ proofs/isabelle/README.md | 58 +++++++++++++++++++++++++++++ proofs/isabelle/compress/Makefile | 2 +- proofs/isabelle/compress/README.md | 22 +++-------- proofs/isabelle/neon_ntt/.gitignore | 5 +++ proofs/isabelle/neon_ntt/README.md | 13 +++---- 7 files changed, 112 insertions(+), 27 deletions(-) create mode 100644 proofs/isabelle/README.md create mode 100644 proofs/isabelle/neon_ntt/.gitignore diff --git a/.github/workflows/isabelle.yml b/.github/workflows/isabelle.yml index fb64913b4..51a8fe030 100644 --- a/.github/workflows/isabelle.yml +++ b/.github/workflows/isabelle.yml @@ -11,7 +11,7 @@ on: jobs: compress: runs-on: ubuntu-latest - container: makarius/isabelle:Isabelle2025-1 + container: makarius/isabelle:Isabelle2025-2 steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - name: Build Compress session @@ -22,7 +22,7 @@ jobs: container: # arm64 image variant; "_X11_Latex" is required because the NeonNTT # ROOT builds a PDF document. - image: makarius/isabelle:Isabelle2025-1_ARM_X11_Latex + image: makarius/isabelle:Isabelle2025-2_ARM_X11_Latex options: --user root steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -51,3 +51,18 @@ jobs: run: | python3 model/conformance/run.py edge python3 model/conformance/run.py random -n 50000 + nix_shell: + name: Isabelle proofs (nix shell) + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + with: + fetch-depth: 0 + - uses: ./.github/actions/setup-shell + with: + gh_token: ${{ secrets.GITHUB_TOKEN }} + nix-shell: 'isabelle' + - name: Build Compress proof + run: nix develop .#isabelle -c make -C proofs/isabelle/compress + - name: Build NeonNTT proof + run: nix develop .#isabelle -c make -C proofs/isabelle/neon_ntt diff --git a/flake.nix b/flake.nix index 7c85971b2..c298ea9f4 100644 --- a/flake.nix +++ b/flake.nix @@ -65,6 +65,7 @@ clang_22 = pkgs-unstable.clang_22; gcc16 = pkgs-unstable.gcc16; zig_0_16 = pkgs-unstable.zig; + isabelle = pkgs-unstable.isabelle; }) ]; }; @@ -123,6 +124,25 @@ devShells.slothy = util.mkShell { packages = builtins.attrValues { inherit (config.packages) slothy linters toolchains_native; }; }; + + + devShells.isabelle = (util.mkShell { + # texlive provides lualatex for the NeonNTT PDF document. + packages = [ + pkgs.isabelle + (pkgs.texlive.combine { + inherit (pkgs.texlive) + scheme-medium hyperxmp ifmtarg sectsty lastpage floatrow titlesec; + }) + ]; + }).overrideAttrs (old: { + shellHook = (old.shellHook or "") + '' + export ISABELLE_VERSION="Isabelle${pkgs.isabelle.version}" + export ISABELLE_DIR="${pkgs.isabelle}" + export ISABELLE_HOME="${pkgs.isabelle}/bin" + ''; + }); + devShells.cross = util.mkShell { packages = builtins.attrValues { inherit (config.packages) linters toolchains; }; }; diff --git a/proofs/isabelle/README.md b/proofs/isabelle/README.md new file mode 100644 index 000000000..5ec5a6454 --- /dev/null +++ b/proofs/isabelle/README.md @@ -0,0 +1,58 @@ +[//]: # (SPDX-License-Identifier: CC-BY-4.0) + +# Isabelle/HOL Proofs + +This directory collects the Isabelle/HOL developments shipped with +`mldsa-native`: + +- [`compress/`](compress) — Barrett-division proofs for ML-DSA's `Decompose`. +- [`neon_ntt/`](neon_ntt) — formalisation of the modular-arithmetic kernels + from the "Neon NTT" paper. + +Each subdirectory has its own `README.md` and `Makefile` describing how to +build that particular development. This page only covers how to obtain +Isabelle itself. + +## Installing Isabelle + +Both developments need the `isabelle` tool. The subdirectory Makefiles locate +it via three variables: + +- `ISABELLE_HOME` — the directory containing the `isabelle` binary. +- `ISABELLE_DIR` — the distribution root (queried as `$(ISABELLE_DIR)/bin/isabelle`). +- `ISABELLE_VERSION` — the version string, e.g. `Isabelle2025-2`. + +By default these point at the macOS `Isabelle2025-2.app` install layout. On +other platforms, or for a different version, override them on the `make` +command line. + +### Official release (recommended) + +Download Isabelle from and install it following +the platform instructions there. The developments above are tested with +`Isabelle2025-2`. +Then either put the `isabelle` binary on your `PATH`, or point the Makefile +variables at your install, e.g.: + +``` +make ISABELLE_VERSION=Isabelle2025-2 \ + ISABELLE_HOME=/path/to/Isabelle2025-2/bin +``` + +### nix shell + +The flake provides an `isabelle` devShell that pulls Isabelle from nixpkgs and +exports `ISABELLE_VERSION`, `ISABELLE_HOME`, and `ISABELLE_DIR` for you: + +``` +nix develop .#isabelle +``` + +It also bundles the TeX distribution that Isabelle needs to typeset the +NeonNTT PDF, so the subdirectory Makefiles work without any further +configuration: + +``` +cd proofs/isabelle/neon_ntt && make +cd proofs/isabelle/compress && make +``` diff --git a/proofs/isabelle/compress/Makefile b/proofs/isabelle/compress/Makefile index 69db7363c..595333bad 100644 --- a/proofs/isabelle/compress/Makefile +++ b/proofs/isabelle/compress/Makefile @@ -1,7 +1,7 @@ # Copyright (c) The mldsa-native project authors # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT -ISABELLE_VERSION ?= Isabelle2025 +ISABELLE_VERSION ?= Isabelle2025-2 ISABELLE_HOME ?= /Applications/$(ISABELLE_VERSION).app/bin all: diff --git a/proofs/isabelle/compress/README.md b/proofs/isabelle/compress/README.md index 5c8ff389b..b8feb7e88 100644 --- a/proofs/isabelle/compress/README.md +++ b/proofs/isabelle/compress/README.md @@ -12,31 +12,19 @@ Isabelle/HOL proofs for the Barrett division used in ML-DSA's `Decompose` routin ## Building -Assuming the `isabelle` binary is in your PATH, you can build via. +See [../README.md](../README.md) for how to obtain Isabelle. With the +`isabelle` binary on your `PATH`, build via ``` isabelle build -D . ``` -Tested with Isabelle2025.1 and Isabelle2025.2. +Alternatively, use the provided [Makefile](Makefile): -Alternatively, you can use the provided [Makefile](Makefile). Use - -``` -make jedit ``` - -to start an interactive proof session in Isabelle/jEdit, and - +make jedit # interactive proof session in Isabelle/jEdit +make # build the proofs from the command line ``` -make -``` - -to build the proofs from the command line. - -To use the Makefile, you need to set the `ISABELLE_VERSION` to your -Isabelle version, and `ISABELLE_HOME` to the full path of the directory -containing the `isabelle` binary. ## Limitation diff --git a/proofs/isabelle/neon_ntt/.gitignore b/proofs/isabelle/neon_ntt/.gitignore new file mode 100644 index 000000000..98de64ccf --- /dev/null +++ b/proofs/isabelle/neon_ntt/.gitignore @@ -0,0 +1,5 @@ +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +# Isabelle build output +output/ +neon_ntt_autoformalized.pdf diff --git a/proofs/isabelle/neon_ntt/README.md b/proofs/isabelle/neon_ntt/README.md index b4a915405..6d9b14987 100644 --- a/proofs/isabelle/neon_ntt/README.md +++ b/proofs/isabelle/neon_ntt/README.md @@ -81,10 +81,10 @@ and conformance testing of the word model against actual hardware. ## Prerequisites -- [Isabelle/HOL](https://isabelle.in.tum.de/) (tested with `Isabelle2025-2`; - CI builds against the - [`makarius/isabelle:Isabelle2025-1_ARM_X11_Latex`](https://hub.docker.com/r/makarius/isabelle) - Docker image). +- Isabelle/HOL — see [../README.md](../README.md) for installation (tested + with `Isabelle2025-2`). CI builds against the + [`makarius/isabelle:Isabelle2025-2_ARM_X11_Latex`](https://hub.docker.com/r/makarius/isabelle) + Docker image. - A TeX distribution providing `luacode.sty` (loaded transitively by `iacrtrans` → `hyperref` → `hyperxmp`). On Debian/Ubuntu this is `texlive-luatex`; the Isabelle macOS app already bundles it. @@ -101,9 +101,8 @@ make # build PDF make jedit # open Asm_Montgomery.thy in Isabelle/jEdit ``` -The Makefile defaults assume the macOS `Isabelle2025-2.app` install layout. -On other platforms, set `ISABELLE_HOME` to the directory containing the -`isabelle` binary (and `ISABELLE_VERSION` if your version differs). +See [../README.md](../README.md) for how to obtain Isabelle and point the +Makefile at it. The default build is heavily abridged — auxiliary lemmas and most proof bodies are elided via Isabelle document tags. A full-proof build can be