Migrate the specification prose from LaTeX to Typst

Replace the LaTeX/TikZ/SVG spec sources with a literate-Typst tree
rendered by Typst:

- Prose, notation macros, and native cetz/fletcher diagrams replace the
  .tex sources, TikZ/SVG figures, and the stripped JuliaMono fonts.
- build.sh renders the .lagda.typ tree with Typst (+ the notation-tooltip
  postprocess); the Shakefile/LaTeX toolchain is removed.
- The @Preview diagram packages (cetz, fletcher, oxifmt) are supplied at
  pinned versions from nixpkgs via `typst.withPackages`
  (TYPST_PACKAGE_CACHE_PATH), keeping the build hermetic without vendoring
  them into the repo.
- Dev shell and `just spec` use the same wrapped typst.

The literate sources carry only prose here; the Agda code blocks, the
standalone reference modules, and the Agda typecheck/lint stage are added
in the following change, so the formalisation appendix is empty for now.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: noonio

flake.lock

@@ -15,6 +15,11 @@
     mithril.url = "github:input-output-hk/mithril/2617.0";
     nixpkgs.follows = "haskellNix/nixpkgs";
     nixpkgs-2411.url = "github:NixOS/nixpkgs/nixos-24.11";
+    # For typst >= 0.14.1 only: the main pin's typst 0.14.0 emits the PDF
+    # named-destination name tree unsorted (typst#7248), which kills internal
+    # section links in spec-compliant viewers. Drop when the main nixpkgs pin
+    # ships typst >= 0.14.1.
+    nixpkgs-2511.url = "github:NixOS/nixpkgs/nixos-25.11";
     nix-npm-buildpackage.url = "github:serokell/nix-npm-buildpackage";
     process-compose-flake.url = "github:Platonic-Systems/process-compose-flake";
     rust-accumulator.url = "github:cardano-scaling/rust-accumulator";

flake.nix

@@ -117,3 +117,10 @@ lint PKG="all":
       -Wmissing-deriving-strategies \
       -Wredundant-constraints \
       -Wunused-packages"
+
+# Needs agda + typst (both in the nix dev shell); mirrors `nix build .#spec` but
+# runs in place for fast iteration.
+#
+# Agda typechecks the literate-Typst sources, then Typst renders spec/_build/hydra-spec.pdf.
+spec:
+  spec/build.sh

justfile

@@ -10,9 +10,10 @@
       compiler = "ghc967";
       inputMap = { "https://intersectmbo.github.io/cardano-haskell-packages" = inputs.CHaP; };
       pkgs-2411 = import inputs.nixpkgs-2411 { inherit system; };
+      pkgs-2511 = import inputs.nixpkgs-2511 { inherit system; };
     in
     {
-      _module.args = { inherit compiler inputMap pkgs-2411; };
+      _module.args = { inherit compiler inputMap pkgs-2411 pkgs-2511; };
       legacyPackages = pkgs // hsPkgs;
     };
 }

nix/configuration.nix

@@ -4,14 +4,20 @@
 
 { self, ... }: {
 
-  perSystem = { pkgs, hsPkgs, compiler, self', inputs', ... }:
+  perSystem = { pkgs, hsPkgs, compiler, self', inputs', pkgs-2511, ... }:
     let
       # Clean nixpkgs (no haskell.nix / nix-npm-buildpackage overlays). The
       # overlaid `pkgs` routes node packages through nix-npm-buildpackage,
       # which fails to build playwright-test, so take it from upstream instead.
       cleanPkgs = inputs'.nixpkgs.legacyPackages;
 
       buildInputs = [
+        # For working on the formal specification (typst render + the
+        # annotate-notation.py tooltip postprocess, see spec/build.sh). The
+        # wrapped typst carries the pinned @preview diagram packages via
+        # TYPST_PACKAGE_CACHE_PATH, same as the nix build (see nix/hydra/spec.nix).
+        self'.packages.spec-typst
+        (pkgs-2511.python3.withPackages (ps: [ ps.pymupdf ]))
         # To compile hydra scripts
         pkgs.aiken
         pkgs.cabal-fmt
@@ -88,6 +94,10 @@
 
         CREATE_MISSING_GOLDEN = 1;
 
+        # Code font for the spec PDF; spec/build.sh passes it to typst
+        # (`just spec`), mirroring the hermetic `nix build .#spec`.
+        JULIAMONO_FONT_DIR = "${pkgs.julia-mono}/share/fonts/truetype";
+
         # Force a UTF-8 locale because many Haskell programs and tests
         # assume this.
         LANG = "en_US.UTF-8";

nix/hydra/shell.nix

@@ -1,36 +1,86 @@
-{ self, inputs, ... }: {
+{ self, ... }: {
 
-  perSystem = { pkgs, pkgs-2411, ... }:
+  perSystem = { config, pkgs, pkgs-2511, ... }:
     let
-      agdaPackages = pkgs-2411.callPackage "${self}/spec/pkgs/initial-packages.nix" {
-        inherit (pkgs-2411.haskellPackages) Agda;
-        nixpkgs = inputs.nixpkgs-2411;
+      # Typst with the spec's diagram packages (@preview/cetz, fletcher, oxifmt)
+      # pinned from nixpkgs and supplied via the wrapper's
+      # TYPST_PACKAGE_CACHE_PATH, so the build stays hermetic without vendoring
+      # them into the repo. typst >= 0.14.1 (0.14.0 emits the PDF
+      # named-destination name tree unsorted, typst#7248, killing internal
+      # section links in viewers that binary-search it per spec: pdf.js, PDFium,
+      # macOS Preview).
+      spec-typst = pkgs-2511.typst.withPackages (p: [
+        p.cetz_0_3_4
+        p.fletcher_0_5_8
+        p.oxifmt_0_2_1
+      ]);
+
+      # The Typst render, WITHOUT the notation-tooltip postprocess
+      # (ANNOTATE_NOTATION=skip, see build.sh stage 3). Internal: consume
+      # packages.spec, which adds the tooltips.
+      #
+      # The postprocess runs as the separate seconds-long derivation below so
+      # this minutes-long, disk-heavy build shares no build window with the
+      # python closure: a busy builder's mid-build auto-GC (observed on the
+      # aarch64-darwin CI builders, where no sandbox bind-mount keeps a
+      # collected path alive for a running build) once collected a late-used
+      # python package out from under the final build step. Inputs are
+      # re-validated when each derivation starts, so splitting shrinks the
+      # exposure of the python environment from the whole render to seconds.
+      spec-rendered = pkgs.stdenv.mkDerivation {
+        pname = "hydra-spec-unannotated.pdf";
+        version = "0.0.1";
+        nativeBuildInputs = [
+          config.packages.spec-typst
+        ];
+        meta = { };
+        src = "${self}/spec";
+        # build.sh renders the literate-Typst sources with Typst (no
+        # LaTeX/Inkscape toolchain needed). --ignore-system-fonts keeps Typst
+        # reproducible: only the fonts bundled with Typst plus JuliaMono from
+        # nixpkgs (code blocks, wired through JULIAMONO_FONT_DIR, see build.sh)
+        # are used.
+        JULIAMONO_FONT_DIR = "${pkgs.julia-mono}/share/fonts/truetype";
+        ANNOTATE_NOTATION = "skip";
+        buildPhase = ''
+          export HOME=$TMPDIR
+          bash build.sh
+        '';
+        installPhase = ''
+          mkdir $out
+          cp _build/hydra-spec.pdf $out/hydra-spec.pdf
+        '';
       };
-      agdaLibraries = with agdaPackages; [
-        abstract-set-theory
-        formal-ledger
-        standard-library
-        standard-library-classes
-        standard-library-meta
-      ];
     in
     {
-      packages.spec = agdaPackages.mkDerivation {
+      # Typst with the spec's diagram packages, reused by the spec build and
+      # exposed so the dev shell can offer the same `typst` for working on the spec.
+      packages.spec-typst = spec-typst;
+
+      # The publishable spec PDF: the render above plus the notation hover
+      # tooltips (build.sh stage 3, split out - see the spec-rendered comment).
+      packages.spec = pkgs.stdenv.mkDerivation {
         pname = "hydra-spec.pdf";
         version = "0.0.1";
-        nativeBuildInputs = with pkgs; [
-          (agdaPackages.withPackages agdaLibraries)
-          (haskellPackages.ghcWithPackages (p: [ p.shake ]))
-          inkscape
-          texlive.combined.scheme-full
+        nativeBuildInputs = [
+          # for annotate-notation.py (stamps the tooltips, needs PyMuPDF)
+          (pkgs-2511.python3.withPackages (ps: [ ps.pymupdf ]))
         ];
         meta = { };
-        src = "${self}/spec";
-        buildPhase = "shake";
+        dontUnpack = true;
+        buildPhase = ''
+          python3 ${self}/spec/annotate-notation.py \
+            ${spec-rendered}/hydra-spec.pdf hydra-spec.pdf
+        '';
         installPhase = ''
           mkdir $out
-          cp _build/hydra-spec.pdf $out/hydra-spec.pdf
+          cp hydra-spec.pdf $out/hydra-spec.pdf
         '';
       };
+
+      # Gate the spec on PRs: `nix flake check`, `just check` (nix-fast-build over
+      # .#checks) and selfci all build the flake checks. Reuses the derivation
+      # above, so this adds no duplicate compilation.
+      checks.spec = config.packages.spec;
     };
 }

nix/hydra/spec.nix

@@ -0,0 +1,2 @@
+_build/
+*.agdai

spec/.gitignore

@@ -1,25 +1,89 @@
 # hydra-formal-specification
 
-Agda specification for the hydra-protocol.
+Literate-Agda + Typst specification for the hydra-protocol.
+
+For an overview of the approach (the trust story, extraction pipeline and
+agreement tests), see the developer docs page `docs/docs/dev/agda.md`
+("Agda formalisation" on the docs site).
+
+The prose, math and figures are written in [Typst](https://typst.app); the source
+files are literate Typst (`.lagda.typ`) so that Agda code blocks are type-checked.
+Code fences render as follows (see `src/template.typ`):
+
+- ` ```agda ` blocks are type-checked by Agda **and** shown in the PDF (collected
+  into the Agda appendix, grouped under the section they support; the body prose
+  links there in place).
+- bare ` ``` ` blocks (module declarations, imports, proof bodies whose
+  statements are shown separately) are type-checked but hidden.
 
 ## Building
 
-To produce the specification PDF in `result/`:
+To produce the specification PDF (via `nix build .#spec`):
 
 ```
-nix build
+nix build .#spec
 ```
 
+The PDF is written to `result/hydra-spec.pdf`.
+
 ## Developing / writing
 
-In a nix shell (`nix develop` or using `nix-direnv`) you can type check:
+In a nix shell (`nix develop` or using `nix-direnv`) you can type-check the Agda:
+
 ```sh
-agda src/Hydra/Protocol/Main.lagda
+agda src/Hydra/Protocol/Main.lagda.typ
 ```
 
-or build the PDF iteratively:
-``` sh
-shake
+or build the PDF iteratively with the build script (Agda typecheck +
+`check-refs.sh` + `check-trust-ledger.sh` + Typst render + a tooltip
+post-process, `annotate-notation.py`: invisible hover annotations giving the
+definition of each notation symbol; skip it with `ANNOTATE_NOTATION=skip`):
+
+```sh
+./build.sh
 ```
 
-with the specification PDF available in `_build/hydra-spec.pdf`.
+with the specification PDF available in `_build/hydra-spec.pdf`. The script
+needs `JULIAMONO_FONT_DIR` (the code font); the nix dev shell exports it, so
+run it from `nix develop` (or set it to a directory containing the JuliaMono
+TTFs). Typst >= 0.14.1 is required (0.14.0 emits the PDF's named-destination
+table unsorted, typst#7248, which leaves internal section links dead in
+spec-compliant viewers); the dev shell and `nix build .#spec` provide a
+suitable typst.
+
+## Keeping the spec and the code in sync
+
+The machine-checked chain is: the `*Valid` bundles in the literate spec imply
+the decidable reference checkers (`Reference.agda`, proved in
+`ReferenceBridge.agda`), the checkers are extracted to Haskell
+(`hydra-agda/`, committed output regenerated by `hydra-agda/regenerate.sh`),
+and the extracted checkers are differentially tested against the real
+validators (`hydra-tx` `HeadValidatorAgreement`) and node logic (`hydra-node`
+off-chain agreement tests). Two flake checks gate all of this at PR time:
+`checks.spec` (the full spec build, including the consistency lints) and
+`checks.hydra-agda-generated` (fails if the committed extraction output is
+stale against the `.agda` sources).
+
+When you change something, the places to update:
+
+- **On-chain validator behaviour** (`hydra-plutus`, `deposit.ak`): update the
+  transaction's section and `*Valid` bundle in
+  `src/Hydra/Protocol/OnChain.lagda.typ`; if the changed condition is
+  decidable, mirror it in `Reference.agda`, prove the bundle implies it in
+  `ReferenceBridge.agda`, run `hydra-agda/regenerate.sh`, expose it in the
+  `hydra-agda` shim, and extend the `HeadValidatorAgreement` family. New
+  mocks/postulates in the bridge fail `check-trust-ledger.sh` until its
+  trust-ledger table and `EXPECTED_*` lists are updated.
+- **Off-chain node behaviour** (`hydra-node` `HeadLogic`): update the §6
+  handler arms in `src/Hydra/Protocol/OffChain.lagda.typ` (and the protocol
+  figure if the visible behaviour changed); mirror decidable decisions in
+  `OffChainReference.agda` and bind them against the real handler in the
+  `hydra-node` agreement tests.
+- **Datum/state shape**: `HeadDatum` in `OnChain.lagda.typ` plus the diagrams
+  (`src/diagrams.typ` `state-fields`); `check-refs.sh` fails on constructor
+  drift, but the per-state field *tuples* it does not compare, so eyeball the
+  rendered figures.
+- **Discrepancies**: record anything found between the spec and the
+  implementation in the PR description or an issue; the differential layer's
+  trusted base (injected mocks and encoding/faithfulness postulates) is
+  enumerated and drift-checked by `check-trust-ledger.sh`.