pq-code-package · mkannwischer · Jun 2, 2026
@@ -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
@@ -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; };
           };

@@ -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 <https://isabelle.in.tum.de/> 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
+```
@@ -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:

@@ -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
 

@@ -0,0 +1,5 @@
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+# Isabelle build output
+output/
+neon_ntt_autoformalized.pdf
@@ -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