WIP: typst

README.md

@@ -14,7 +14,7 @@ nix build
 
 In a nix shell (`nix develop` or using `nix-direnv`) you can type check:
 ```sh
-agda src/Hydra/Protocol/Main.lagda
+agda src/Hydra/Protocol/Main.lagda.typ
 ```
 
 or build the PDF iteratively:

Shakefile.hs

@@ -13,29 +13,14 @@ main = shakeArgs shakeOptions{shakeFiles="_build"} $ do
       removeFilesAfter "_build" ["//*"]
 
     "_build/hydra-spec" <.> "pdf" %> \out -> do
-      assets <- getDirectoryFiles "src" ["//*.sty", "Hydra/Protocol/Figures/*.pdf", "//*.bib", "//*.ttf"]
-      need ["_build/latex" </> c | c <- assets]
+      assets <- getDirectoryFiles "src" ["//*.sty", "//*.pdf", "//*.bib", "//*.ttf", "//*.typ"]
+      need ["_build/src" </> c | c <- assets]
+      cmd_ $ "typst compile --root _build _build/src/Hydra/Protocol/Main.lagda.typ " <> out
 
-      srcs <- getDirectoryFiles "src" ["//*.lagda", "//*.tex"]
-      need ["_build/latex" </> c -<.> "tex" | c <- srcs]
-
-      cmd_ (Cwd "_build/latex") "latexmk -xelatex -shell-escape -halt-on-error Hydra/Protocol/Main.tex"
-      cmd_ "cp _build/latex/Main.pdf _build/hydra-spec.pdf"
-
-    -- Copy assets
-    forM ["sty", "pdf", "bib", "ttf"] $ \ext ->
-      ("_build/latex//*." <> ext)  %> \out -> do
+    forM ["typ", "sty", "pdf", "bib", "ttf"] $ \ext ->
+      ("_build//*." <> ext)  %> \out -> do
         let src = "src" </> dropDirectory1 (dropDirectory1 out)
         copyFile' src out
 
-    -- Copy or compile from lagda files
-    "_build/latex//*.tex"  %> \out -> do
-      let src = "src" </> dropDirectory1 (dropDirectory1 out)
-      b <- doesFileExist src
-      if b then do
-        need [src]
-        copyFile' src out
-      else do
-        let src = "src" </> dropDirectory1 (dropDirectory1 (out -<.> "lagda"))
-        need [src]
-        cmd_ $ "agda --transliterate --latex --latex-dir _build/latex " <> src
+    phony "check" $ do
+      cmd_ $ "agda src/Hydra/Protocol/Main.lagda.typ" 

flake.nix

@@ -40,7 +40,7 @@
               nativeBuildInputs = with pkgs; [
                 (agdaPackages.withPackages agdaLibraries)
                 (haskellPackages.ghcWithPackages (p: [ p.shake ]))
-                texlive.combined.scheme-full
+                typst
               ];
               meta = { };
               src = ./.;
@@ -53,8 +53,23 @@
               '';
             };
 
+
             default = packages.hydra-spec-pdf;
+
           };
+            checks.typecheck = agdaPackages.mkDerivation {
+              pname = "hydra-spec-typecheck";
+              version = "0.0.1";
+              nativeBuildInputs = with pkgs; [
+                (agdaPackages.withPackages agdaLibraries)
+                (haskellPackages.ghcWithPackages (p: [ p.shake ]))
+              ];
+              meta = { };
+              src = ./.;
+              buildPhase = ''
+                shake check
+              '';
+            };
         };
     };
 }

src/Hydra/Protocol/Figures/head-protocol-states.typ

@@ -0,0 +1,8 @@
+#import "@preview/cetz:0.3.1"
+
+#figure(
+ cetz.canvas({
+  import cetz.draw: *
+  // Your drawing code goes here
+}))
+<figure:head-protocol-states>

src/Hydra/Protocol/Introduction.lagda.typ

@@ -0,0 +1,23 @@
+= Introduction
+
+
+This document specifies the 'Coordinated Hydra Head' protocol to be implemented
+as the first version of Hydra Head on Cardano - *Hydra HeadV1*. The protocol is
+derived from variants described in the original paper @hydrahead20, but was
+further simplified to make a first implementation on Cardano possible.
+
+Note that the format and scope of this document is (currently) also inspired by
+the paper and hence does not include a definition of the networking protocols
+or concrete message formats. It is structured similarly, but focuses on a
+single variant, and avoids indirections and unnecessary generalizations. The
+document is kept in sync with the reference implementation available on Github
+@hydra-repo.
+
+First, a high-level overview of the protocol and how it differs from legacy
+variants of the Head protocol is given in @sec:overview. Relevant definitions and
+notations are introduced in @prel, while @setup describes protocol setup and
+assumptions. Then, the actual on-chain transactions of the protocol are defined
+in @on-chain, before the off-chain protocol part specifies behavior of Hydra
+parties off-chain and ties the knot with on-chain transactions in @offchain. At
+last, @security gives the security definition, properties and proofs for the
+Coordinated Head protocol.

src/Hydra/Protocol/Macros.typ

@@ -0,0 +1,30 @@
+#let DejaVuSans(msg) = text(font:"DejaVu Sans")[#msg]
+
+#let todo(msg) = {
+  [#text(fill: red, weight: "bold", size: 12pt)[TODO #msg]]
+}
+
+#let stInitial = DejaVuSans("stInitial")
+#let stOpen = DejaVuSans("stOpen")
+#let stClosed = DejaVuSans("stClosed")
+#let stFinal = DejaVuSans("stFinal")
+
+#let txAbort = DejaVuSans("abort")
+#let txClose = DejaVuSans("close")
+#let txCollectCom = DejaVuSans("collectCom")
+#let txCommit = DejaVuSans("commit")
+#let txContest = DejaVuSans("contest")
+#let txDecrement = DejaVuSans("decrement")
+#let txDeposit = DejaVuSans("deposit")
+#let txFanout = DejaVuSans("fanout")
+#let txFinalize = DejaVuSans("finalize")
+#let txIncrement = DejaVuSans("increment")
+#let txInit = DejaVuSans("init")
+#let txRecover = DejaVuSans("recover")
+
+#let msSetup = DejaVuSans("MS-Setup")
+#let msParams = DejaVuSans("MS-Params")
+#let msKeyGen = DejaVuSans("MS-KeyGen")
+#let msSign = DejaVuSans("MS-Sign")
+#let msVK = DejaVuSans("MS-VK")
+#let msSK = DejaVuSans("MS-SK")

src/Hydra/Protocol/Main.lagda.typ

@@ -0,0 +1,53 @@
+#import "../../conf.typ": conf
+#set heading(numbering: "1.")
+#show heading: set block(spacing: 1.5em)
+#set block(below: 1.5em)
+#show: conf.with(
+  title: [
+    Hydra Head V1 Specification: Coordinated Head Protocol
+  ],
+  authors: (
+    (
+      name: "Sebastian Nagel",
+      email: "sebastian.nagel@iohk.io",
+    ),
+    (
+      name: "Sasha Bogicevic",
+      email: "sasha.bogicevic@iohk.io",
+    ),
+    (
+      name: "Franco Testagrossa",
+      email: "franco.testagrossa@iohk.io",
+    ),
+    (
+      name: "Daniel Firth",
+      email: "daniel.firth@iohk.io",
+    ),
+  )
+)
+
+/*
+```
+module Hydra.Protocol.Main where
+
+import Hydra.Protocol.Throwaway
+```
+*/
+
+#pagebreak()
+#include "Introduction.lagda.typ"
+#pagebreak()
+#include "Overview.lagda.typ"
+#pagebreak()
+#include "Preliminaries.lagda.typ"
+#pagebreak()
+#include "Setup.lagda.typ"
+#pagebreak()
+#include "OnChain.lagda.typ"
+#pagebreak()
+#include "OffChain.lagda.typ"
+#pagebreak()
+#include "Security.lagda.typ"
+#pagebreak()
+
+#bibliography("../../short.bib")

src/Hydra/Protocol/OffChain.tex → src/Hydra/Protocol/OffChain.lagda.typ

@@ -1,14 +1,17 @@
-\section{Off-Chain Protocol}\label{sec:offchain}
+= Off-Chain Protocol
+<offchain>
 
 This section describes the actual Coordinated Hydra Head protocol, an even more
-simplified version of the original publication~\cite{hydrahead20}. See the
-protocol overview in Section~\ref{sec:overview} for an introduction and notable
+simplified version of the original publication @hydrahead20. See the
+protocol overview in @sec:overview for an introduction and notable
 changes to the original protocol. While the on-chain part already describes the
 full life-cycle of a Hydra head on-chain, this section completes the picture by
 defining how the protocol behaves off-chain and notably the relationship between
 on- and off-chain semantics. Participants of the protocol are also called Hydra
 head members, parties or simply protocol actors. The protocol is specified as a
 reactive system that processes three kinds of inputs:
+
+/*
 \begin{enumerate}
   \item On-chain protocol transactions as introduced in
   Section~\ref{sec:on-chain}, which are posted to the mainchain and can be
@@ -353,8 +356,4 @@ \subsection{Rollbacks and protocol changes}\label{sec:rollbacks}
 \input{Hydra/Protocol/Figures/offchain-protocol}
 
 \todo{In figure: $\combine$ on UTxO slightly different than on commits}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "main"
-%%% End:
+*/