diff --git a/README.md b/README.md index 45cba63..7ef171d 100644 --- a/README.md +++ b/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: diff --git a/Shakefile.hs b/Shakefile.hs index 430c9c4..3989cdb 100644 --- a/Shakefile.hs +++ b/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" diff --git a/flake.nix b/flake.nix index 254094c..2d4ccc4 100644 --- a/flake.nix +++ b/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 + ''; + }; }; }; } diff --git a/src/Hydra/Protocol/Figures/SM-abort.pdf b/src/Hydra/Protocol/Figures/SM-abort.pdf deleted file mode 100644 index 71fe0e0..0000000 Binary files a/src/Hydra/Protocol/Figures/SM-abort.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/SM-abort.svg b/src/Hydra/Protocol/Figures/SM-abort.svg new file mode 100644 index 0000000..b2fa67d --- /dev/null +++ b/src/Hydra/Protocol/Figures/SM-abort.svg @@ -0,0 +1,664 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/SM-close.pdf b/src/Hydra/Protocol/Figures/SM-close.pdf deleted file mode 100644 index 93eb89f..0000000 Binary files a/src/Hydra/Protocol/Figures/SM-close.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/SM-close.svg b/src/Hydra/Protocol/Figures/SM-close.svg new file mode 100644 index 0000000..35cc61d --- /dev/null +++ b/src/Hydra/Protocol/Figures/SM-close.svg @@ -0,0 +1,233 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/SM-collect.pdf b/src/Hydra/Protocol/Figures/SM-collect.pdf deleted file mode 100644 index 5d06952..0000000 Binary files a/src/Hydra/Protocol/Figures/SM-collect.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/SM-collect.svg b/src/Hydra/Protocol/Figures/SM-collect.svg new file mode 100644 index 0000000..adb537b --- /dev/null +++ b/src/Hydra/Protocol/Figures/SM-collect.svg @@ -0,0 +1,615 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/SM-contest.pdf b/src/Hydra/Protocol/Figures/SM-contest.pdf deleted file mode 100644 index 2476ba8..0000000 Binary files a/src/Hydra/Protocol/Figures/SM-contest.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/SM-contest.svg b/src/Hydra/Protocol/Figures/SM-contest.svg new file mode 100644 index 0000000..ea5c4d0 --- /dev/null +++ b/src/Hydra/Protocol/Figures/SM-contest.svg @@ -0,0 +1,451 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/SM-fanout.pdf b/src/Hydra/Protocol/Figures/SM-fanout.pdf deleted file mode 100644 index f6d28a2..0000000 Binary files a/src/Hydra/Protocol/Figures/SM-fanout.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/SM-fanout.svg b/src/Hydra/Protocol/Figures/SM-fanout.svg new file mode 100644 index 0000000..ff24362 --- /dev/null +++ b/src/Hydra/Protocol/Figures/SM-fanout.svg @@ -0,0 +1,406 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/SM-init-commit.pdf b/src/Hydra/Protocol/Figures/SM-init-commit.pdf deleted file mode 100644 index 7ca2c4b..0000000 Binary files a/src/Hydra/Protocol/Figures/SM-init-commit.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/SM-init-commit.svg b/src/Hydra/Protocol/Figures/SM-init-commit.svg new file mode 100644 index 0000000..e5eba2e --- /dev/null +++ b/src/Hydra/Protocol/Figures/SM-init-commit.svg @@ -0,0 +1,703 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/abortTx.pdf b/src/Hydra/Protocol/Figures/abortTx.pdf deleted file mode 100644 index 3846492..0000000 Binary files a/src/Hydra/Protocol/Figures/abortTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/abortTx.svg b/src/Hydra/Protocol/Figures/abortTx.svg new file mode 100644 index 0000000..2863b1b --- /dev/null +++ b/src/Hydra/Protocol/Figures/abortTx.svg @@ -0,0 +1,731 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/closeTx.pdf b/src/Hydra/Protocol/Figures/closeTx.pdf deleted file mode 100644 index fc619aa..0000000 Binary files a/src/Hydra/Protocol/Figures/closeTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/closeTx.svg b/src/Hydra/Protocol/Figures/closeTx.svg new file mode 100644 index 0000000..2b2308b --- /dev/null +++ b/src/Hydra/Protocol/Figures/closeTx.svg @@ -0,0 +1,243 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/collectComTx.pdf b/src/Hydra/Protocol/Figures/collectComTx.pdf deleted file mode 100644 index 87b7112..0000000 Binary files a/src/Hydra/Protocol/Figures/collectComTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/collectComTx.svg b/src/Hydra/Protocol/Figures/collectComTx.svg new file mode 100644 index 0000000..637b705 --- /dev/null +++ b/src/Hydra/Protocol/Figures/collectComTx.svg @@ -0,0 +1,793 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/commitTx.pdf b/src/Hydra/Protocol/Figures/commitTx.pdf deleted file mode 100644 index cff578b..0000000 Binary files a/src/Hydra/Protocol/Figures/commitTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/commitTx.svg b/src/Hydra/Protocol/Figures/commitTx.svg new file mode 100644 index 0000000..f694615 --- /dev/null +++ b/src/Hydra/Protocol/Figures/commitTx.svg @@ -0,0 +1,600 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/contestTx.pdf b/src/Hydra/Protocol/Figures/contestTx.pdf deleted file mode 100644 index 6de0c17..0000000 Binary files a/src/Hydra/Protocol/Figures/contestTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/contestTx.svg b/src/Hydra/Protocol/Figures/contestTx.svg new file mode 100644 index 0000000..738a46a --- /dev/null +++ b/src/Hydra/Protocol/Figures/contestTx.svg @@ -0,0 +1,258 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/decrementTx.pdf b/src/Hydra/Protocol/Figures/decrementTx.pdf deleted file mode 100644 index d1e6f29..0000000 Binary files a/src/Hydra/Protocol/Figures/decrementTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/decrementTx.svg b/src/Hydra/Protocol/Figures/decrementTx.svg new file mode 100644 index 0000000..0536d2c --- /dev/null +++ b/src/Hydra/Protocol/Figures/decrementTx.svg @@ -0,0 +1,451 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/deposit-tx.pdf b/src/Hydra/Protocol/Figures/deposit-tx.pdf deleted file mode 100644 index 43de659..0000000 Binary files a/src/Hydra/Protocol/Figures/deposit-tx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/deposit-tx.svg b/src/Hydra/Protocol/Figures/deposit-tx.svg new file mode 100644 index 0000000..18278ae --- /dev/null +++ b/src/Hydra/Protocol/Figures/deposit-tx.svg @@ -0,0 +1,292 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/fanoutTx.pdf b/src/Hydra/Protocol/Figures/fanoutTx.pdf deleted file mode 100644 index 8648b27..0000000 Binary files a/src/Hydra/Protocol/Figures/fanoutTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/fanoutTx.svg b/src/Hydra/Protocol/Figures/fanoutTx.svg new file mode 100644 index 0000000..51a4b5e --- /dev/null +++ b/src/Hydra/Protocol/Figures/fanoutTx.svg @@ -0,0 +1,191 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/head-protocol-states.typ b/src/Hydra/Protocol/Figures/head-protocol-states.typ new file mode 100644 index 0000000..6255195 --- /dev/null +++ b/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 +})) + diff --git a/src/Hydra/Protocol/Figures/incrementTx.pdf b/src/Hydra/Protocol/Figures/incrementTx.pdf deleted file mode 100644 index e33c633..0000000 Binary files a/src/Hydra/Protocol/Figures/incrementTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/incrementTx.svg b/src/Hydra/Protocol/Figures/incrementTx.svg new file mode 100644 index 0000000..ce96c59 --- /dev/null +++ b/src/Hydra/Protocol/Figures/incrementTx.svg @@ -0,0 +1,740 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/initTx.pdf b/src/Hydra/Protocol/Figures/initTx.pdf deleted file mode 100644 index a04f516..0000000 Binary files a/src/Hydra/Protocol/Figures/initTx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/initTx.svg b/src/Hydra/Protocol/Figures/initTx.svg new file mode 100644 index 0000000..b07a661 --- /dev/null +++ b/src/Hydra/Protocol/Figures/initTx.svg @@ -0,0 +1,645 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/recover-tx.pdf b/src/Hydra/Protocol/Figures/recover-tx.pdf deleted file mode 100644 index b226844..0000000 Binary files a/src/Hydra/Protocol/Figures/recover-tx.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/recover-tx.svg b/src/Hydra/Protocol/Figures/recover-tx.svg new file mode 100644 index 0000000..a995ddc --- /dev/null +++ b/src/Hydra/Protocol/Figures/recover-tx.svg @@ -0,0 +1,281 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Figures/state-transition_cropped.pdf b/src/Hydra/Protocol/Figures/state-transition_cropped.pdf deleted file mode 100644 index c64d33e..0000000 Binary files a/src/Hydra/Protocol/Figures/state-transition_cropped.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/utxo-graph.pdf b/src/Hydra/Protocol/Figures/utxo-graph.pdf deleted file mode 100644 index dafea2f..0000000 Binary files a/src/Hydra/Protocol/Figures/utxo-graph.pdf and /dev/null differ diff --git a/src/Hydra/Protocol/Figures/utxo-graph.svg b/src/Hydra/Protocol/Figures/utxo-graph.svg new file mode 100644 index 0000000..10d0c6e --- /dev/null +++ b/src/Hydra/Protocol/Figures/utxo-graph.svg @@ -0,0 +1,523 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/Hydra/Protocol/Introduction.lagda.typ b/src/Hydra/Protocol/Introduction.lagda.typ new file mode 100644 index 0000000..1c234b1 --- /dev/null +++ b/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. diff --git a/src/Hydra/Protocol/Introduction.tex b/src/Hydra/Protocol/Introduction.tex deleted file mode 100644 index 080dff0..0000000 --- a/src/Hydra/Protocol/Introduction.tex +++ /dev/null @@ -1,31 +0,0 @@ -\section{Introduction} -This document specifies the 'Coordinated Hydra Head' protocol to be implemented -as the first version of Hydra Head on Cardano - \textbf{Hydra HeadV1}. The -protocol is derived from variants described in the original paper -\cite{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. \todo{Add: network specification (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~\cite{hydra-repo}. -\textcolor{red}{Red} sections indicate that they are currently not covered or -missing in the implementation, where \textcolor{blue}{blue} parts mean a -difference in how it is realized. - -First, a high-level overview of the protocol and how it differs from legacy -variants of the Head protocol is given in Section~\ref{sec:overview}. Relevant -definitions and notations are introduced in Section~\ref{sec:prel}, while -Section~\ref{sec:setup} describes protocol setup and assumptions. Then, the -actual on-chain transactions of the protocol are defined in -Section~\ref{sec:on-chain}, before the off-chain protocol part specifies -behavior of Hydra parties off-chain and ties the knot with on-chain transactions -in Section~\ref{sec:offchain}. At last, Section~\ref{sec:security} gives the -security definition, properties and proofs for the Coordinated Head protocol. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: diff --git a/src/Hydra/Protocol/Macros.typ b/src/Hydra/Protocol/Macros.typ new file mode 100644 index 0000000..f30d6d0 --- /dev/null +++ b/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") diff --git a/src/Hydra/Protocol/Main.lagda b/src/Hydra/Protocol/Main.lagda deleted file mode 100644 index c748034..0000000 --- a/src/Hydra/Protocol/Main.lagda +++ /dev/null @@ -1,39 +0,0 @@ -\documentclass[11pt, titlepage]{article} - -\include{preamble} -\include{macros} - -\title{\Large \textbf{Hydra HeadV1 Specification: Coordinated Head protocol}\\[2ex] DRAFT} -\author{ - Sebastian Nagel \texttt{sebastian.nagel@iohk.io} \and - Sasha Bogicevic \texttt{sasha.bogicevic@iohk.io} \and - Franco Testagrossa \texttt{franco.testagrossa@iohk.io} \and - Daniel Firth \texttt{daniel.firth@iohk.io} - % NOTE: add yourself -} -\begin{document} -\maketitle - -\newpage - -\tableofcontents - -\begin{code}[hide] -module Hydra.Protocol.Main where - -open import Hydra.Protocol.Throwaway -\end{code} - -\input{Hydra/Protocol/Introduction} -\input{Hydra/Protocol/Overview} -\input{Hydra/Protocol/Preliminaries} -\input{Hydra/Protocol/Setup} -\input{Hydra/Protocol/OnChain} -\input{Hydra/Protocol/OffChain} -\input{Hydra/Protocol/Security} -\input{Hydra/Protocol/Throwaway} - -\bibliographystyle{plain} -\bibliography{short} - -\end{document} diff --git a/src/Hydra/Protocol/Main.lagda.typ b/src/Hydra/Protocol/Main.lagda.typ new file mode 100644 index 0000000..d257464 --- /dev/null +++ b/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") diff --git a/src/Hydra/Protocol/OffChain.tex b/src/Hydra/Protocol/OffChain.lagda.typ similarity index 98% rename from src/Hydra/Protocol/OffChain.tex rename to src/Hydra/Protocol/OffChain.lagda.typ index 6165bdc..53048b1 100644 --- a/src/Hydra/Protocol/OffChain.tex +++ b/src/Hydra/Protocol/OffChain.lagda.typ @@ -1,14 +1,17 @@ -\section{Off-Chain Protocol}\label{sec:offchain} += Off-Chain Protocol + 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: +*/ diff --git a/src/Hydra/Protocol/OnChain.tex b/src/Hydra/Protocol/OnChain.lagda.typ similarity index 83% rename from src/Hydra/Protocol/OnChain.tex rename to src/Hydra/Protocol/OnChain.lagda.typ index 1a62b8b..b7783aa 100644 --- a/src/Hydra/Protocol/OnChain.tex +++ b/src/Hydra/Protocol/OnChain.lagda.typ @@ -1,5 +1,7 @@ -\clearpage -\section{On-chain Protocol}\label{sec:on-chain} += On-chain Protocol + + +/* \todo{Update figures} \todo{Open problem: ensure abort is always possible. e.g. by individual aborts or undoing commits} @@ -21,16 +23,15 @@ \section{On-chain Protocol}\label{sec:on-chain} \noindent The head protocol defines one minting policy script and three validator scripts: -\begin{itemize} - \item $\muHead$ governs minting of state and participation tokens in +- $\muHead$ governs minting of state and participation tokens in $\mtxInit{}$ and burning of these tokens in $\mtxAbort{}$ and $\mtxFanout{}$. - \item $\nuInitial$ controls how UTxOs are committed to the head in +- $\nuInitial$ controls how UTxOs are committed to the head in $\mtxCommit{}$ or when the head initialization is aborted via $\mtxAbort{}$. - \item $\nuCommit$ controls the collection of committed UTxOs into the head in +- $\nuCommit$ controls the collection of committed UTxOs into the head in $\mtxCollect$ or that funds are reimbursed in an $\mtxAbort{}$. - \item $\nuHead$ represents the main protocol state machine logic and ensures +- $\nuHead$ represents the main protocol state machine logic and ensures contract continuity throughout $\mtxCollect{}$, $\mtxDecrement{}$, \red{\mtxIncrement{},} $\mtxClose{}$, $\mtxContest{}$ and $\mtxFanout{}$. @@ -38,15 +39,18 @@ \section{On-chain Protocol}\label{sec:on-chain} \noindent \red{The deposit protocol defines one validator script: \begin{itemize} - \item $\nuDeposit$ controls that \mtxDeposit{} transaction output is +- $\nuDeposit$ controls that \mtxDeposit{} transaction output is claimed correctly into a head via \mtxIncrement{} or recovered after the deadline has passed in a \mtxRecover{} transaction. \end{itemize} } +*/ -\subsection{Init transaction}\label{sec:init-tx} +== Init transaction + -The \mtxInit{} transaction creates a head instance and establishes the initial +/* +The $txInit$ transaction creates a head instance and establishes the initial state of the protocol and is shown in Figure~\ref{fig:initTx}. The head instance is represented by the unique currency identifier $\cid$ created by minting tokens using the $\muHead$ minting policy script which is parameterized @@ -59,72 +63,60 @@ \subsection{Init transaction}\label{sec:init-tx} \centering \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/initTx.pdf} \caption{\mtxInit{} transaction spending a seed UTxO, and producing the head - output in state $\stInitial$ and initial outputs for each participant.}\label{fig:initTx} + output in state $sans("stInitial")$ and initial outputs for each participant.}\label{fig:initTx} \end{figure} \noindent Two kinds of tokens are minted: -\begin{itemize} - \item A single \emph{State Thread (ST)} token marking the head output. This +- A single \emph{State Thread (ST)} token marking the head output. This output contains the state of the protocol on-chain and the token ensures contract continuity. The token name is the well known string \texttt{HydraHeadV1}, i.e. $\st = \{\cid \mapsto \texttt{HydraHeadV1} \mapsto 1\}$. - \item One \emph{Participation Token (PT)} per participant +- One \emph{Participation Token (PT)} per participant $i \in \{1 \dots |\hydraKeys| \}$ to be used for authenticating further transactions and to ensure every participant can commit and cannot be censored. The token name is the participant's verification key hash $\keyHash_{i} = \hash(\msVK_{i})$ of the verification key as received during protocol setup, i.e. $\pt_{i} = \{\cid \mapsto \keyHash_{i} \mapsto 1\}$. -\end{itemize} \noindent Consequently, the \mtxInit{} transaction -\begin{itemize} - \item has at least input $\seed$, - \item mints the state thread token $\st$, and one $\pt$ for each of the $|\hydraKeys|$ +- has at least input $\seed$, +- mints the state thread token $\st$, and one $\pt$ for each of the $|\hydraKeys|$ participants with policy $\cid$, - \item has $|\hydraKeys|$ initial outputs $o_{\mathsf{initial}_{i}}$ with datum $\datumInitial{} = \cid$, - \item has one head output +- has $|\hydraKeys|$ initial outputs $o_{\mathsf{initial}_{i}}$ with datum $\datumInitial{} = \cid$, +- has one head output $o_{\mathsf{head}}$, which captures the initial state of the protocol in the datum \[ - \datumHead = (\stInitial,\cid',\seed',\hydraKeys,\cPer) + \datumHead = (sans("stInitial"),\cid',\seed',\hydraKeys,\cPer) \] where - \begin{mitemize} - \item $\stInitial$ is a state identifier, - \item $\cid'$ is the unique currency id of this instance, - \item $\seed'$ is the output reference parameter of $\muHead$, - \item $\hydraKeys$ are the off-chain multi-signature keys from the setup - phase, - \item $\cPer$ is the contestation period. - \end{mitemize} -\end{itemize} + - sans("stInitial")$ is a state identifier, + - $\cid'$ is the unique currency id of this instance, + - $\seed'$ is the output reference parameter of $\muHead$, + - $\hydraKeys$ are the off-chain multi-signature keys from the setup + phase, + - $\cPer$ is the contestation period. \noindent The $\muHead(\seed)$ minting policy is the only script that verifies init transactions and can be redeemed with either a $\mathsf{Mint}$ or $\mathsf{Burn}$ redeemer: -\begin{itemize} - \item When evaluated with the $\mathsf{Mint}$ redeemer, - \begin{menumerate} - \item The seed output is spent in this transaction. This guarantees uniqueness of the policy $\cid$ because the EUTxO ledger ensures that $\seed$ cannot be spent twice in the same chain. +- When evaluated with the $\mathsf{Mint}$ redeemer, + - The seed output is spent in this transaction. This guarantees uniqueness of the policy $\cid$ because the EUTxO ledger ensures that $\seed$ cannot be spent twice in the same chain. $(\seed, \cdot) \in \txInputs$ - \item All entries of $\txMint$ are of this policy and of single quantity $\forall \{c \mapsto \cdot \mapsto q\} \in \txMint : c = \cid \land q = 1$ - \item Right number of tokens are minted $|\txMint| = |\hydraKeys| + 1$ + - All entries of $\txMint$ are of this policy and of single quantity $\forall \{c \mapsto \cdot \mapsto q\} \in \txMint : c = \cid \land q = 1$ + - Right number of tokens are minted $|\txMint| = |\hydraKeys| + 1$ % TODO: |\txMint| may not be clear to the reader, maybe combine with item above, but be more explicit. - \item State token is sent to the head validator $\st \in \valHead$ % TODO: fact that it is goverend by nuHead is a bit implicit here. - \item \textcolor{blue}{The correct number of initial outputs are present $|(\cdot, \nuInitial, \cdot) \in \txOutputs| = |\hydraKeys|$} + - State token is sent to the head validator $\st \in \valHead$ % TODO: fact that it is goverend by nuHead is a bit implicit here. + - \textcolor{blue}{The correct number of initial outputs are present $|(\cdot, \nuInitial, \cdot) \in \txOutputs| = |\hydraKeys|$} % XXX: this is implied by the ledger, so can be removed - \item All participation tokens are sent to the initial validator as an initial output $\forall i \in [1 \dots |\hydraKeys|] : \{\cid \mapsto \cdot \mapsto 1\} \in \valInitial{i}$ - \item The $\datum_{\mathsf{head}}$ contains own currency id $\cid = \cid'$ and the right seed reference $\seed = \seed'$ - \item All initial outputs have a $\cid$ as their datum: $\forall i \in [1 \dots |\hydraKeys|] : \cid = \datumInitial{i}$ - \end{menumerate} - \item When evaluated with the $\mathsf{Burn}$ redeemer,\todo{move to abort/fanout?} - \begin{menumerate} - \item All tokens for this policy in $\txMint$ need to be of negative quantity + - All participation tokens are sent to the initial validator as an initial output $\forall i \in [1 \dots |\hydraKeys|] : \{\cid \mapsto \cdot \mapsto 1\} \in \valInitial{i}$ + - The $\datum_{\mathsf{head}}$ contains own currency id $\cid = \cid'$ and the right seed reference $\seed = \seed'$ + - All initial outputs have a $\cid$ as their datum: $\forall i \in [1 \dots |\hydraKeys|] : \cid = \datumInitial{i}$ +- When evaluated with the $\mathsf{Burn}$ redeemer,\todo{move to abort/fanout?} + - All tokens for this policy in $\txMint$ need to be of negative quantity $\forall \{\cid \mapsto \cdot \mapsto q\} \in \txMint : q < 0$. - \end{menumerate} -\end{itemize} \noindent \textbf{Important:} The $\muHead$ minting policy only ensures uniqueness of $\cid$, that the right amount of tokens have been minted and sent @@ -136,9 +128,12 @@ \subsection{Init transaction}\label{sec:init-tx} correct verification key hashes are used in the $\pt$s and the initial state is consistent with parameters agreed during setup. See the initialTx behavior in Figure~\ref{fig:off-chain-prot} for details about these checks.\\ +*/ -\subsection{Commit Transaction}\label{sec:commit-tx} +== Commit Transaction + +/* A \mtxCom{} transaction may be submitted by each participant $\forall i \in \{1 \dots |\hydraKeys|\}$ to commit some UTxO into the head or acknowledge to not commit anything. The transaction is depicted in @@ -183,9 +178,12 @@ \subsection{Commit Transaction}\label{sec:commit-tx} committed output, and producing a commit output.}\label{fig:commitTx} \end{figure} \todo{update with multiple commits} +*/ -\subsection{Abort Transaction}\label{sec:abort-tx} +== Abort Transaction + +/* The \mtxAbort{} transaction (see Figure~\ref{fig:abortTx}) allows a party to abort the creation of a head and consists of \begin{itemize} @@ -222,10 +220,10 @@ \subsection{Abort Transaction}\label{sec:abort-tx} $\redeemerHead = (\mathsf{abort}, m)$, where $m$ is the number of outputs to reimburse, and checks: \begin{menumerate} - \item State is advanced from $\datumHead \sim \stInitial$ to terminal state - $\stFinal$: + \item State is advanced from $\datumHead \sim sans("stInitial")$ to terminal state + $sans("stFinal")$: \[ - (\stInitial,\cid,\seed,\hydraKeys,\cPer) \xrightarrow[m]{\stAbort} \stFinal. + (sans("stInitial"),\cid,\seed,\hydraKeys,\cPer) \xrightarrow[m]{\stAbort} sans("stFinal"). \] \item All UTxOs committed into the head are reimbursed exactly as they were committed. This is done by comparing hashes of serialised representations of @@ -245,14 +243,17 @@ \subsection{Abort Transaction}\label{sec:abort-tx} \begin{figure} \centering \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/abortTx.pdf} - \caption{\mtxAbort{} transaction spending the $\stInitial$ state head + \caption{\mtxAbort{} transaction spending the $sans("stInitial")$ state head output and collecting all initial and commit outputs, which get reimbursed by outputs $o_{1} \dots o_{m}$. Note that each $\pt$ may be in either, an initial or commit output.}\label{fig:abortTx} \end{figure} +*/ -\subsection{CollectCom Transaction}\label{sec:collect-tx} +== CollectCom Transaction + +/* \noindent The \mtxCCom{} transaction (Figure~\ref{fig:collectComTx}) collects all the committed UTxOs to the same head. It has \begin{itemize} @@ -267,11 +268,11 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx} \noindent The state-machine validator $\nuHead$ is spent with $\redeemerHead = \mathsf{collect}$ and checks: \begin{menumerate} - \item State is advanced from $\datumHead \sim \stInitial$ to - $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeys,\cPer$ stay + \item State is advanced from $\datumHead \sim sans("stInitial")$ to + $\datumHead' \sim sans("stOpen")$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stInitial,\cid,\seed,\hydraKeys,\cPer) \xrightarrow{\stCollect} (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) + (sans("stInitial"),\cid,\seed,\hydraKeys,\cPer) \xrightarrow{\stCollect} (sans("stOpen"),\cid,\hydraKeys,\cPer,v,\eta) \] where snapshot version is initialized as $v = 0$. \item Commits are collected in $\eta$ @@ -322,14 +323,16 @@ \subsection{CollectCom Transaction}\label{sec:collect-tx} \begin{figure} \centering \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/collectComTx.pdf} - \caption{\mtxCCom{} transaction spending the head output in $\stInitial$ + \caption{\mtxCCom{} transaction spending the head output in $sans("stInitial")$ state and collecting from multiple commit outputs into a single - $\stOpen$ head output.}\label{fig:collectComTx} + $sans("stOpen")$ head output.}\label{fig:collectComTx} \end{figure} +*/ +== Deposit Transaction + -\subsection{\red{Deposit Transaction}}\label{sec:deposit-tx} - +/* \noindent The \mtxDeposit{} transaction initiates a (incremental) commit by locking funds in $\nuDeposit$ for later collection by the head protocol. Any transaction paying to $\nuDeposit$ is a \mtxDeposit{} transaction as there is no @@ -374,9 +377,12 @@ \subsection{\red{Deposit Transaction}}\label{sec:deposit-tx} \caption{\mtxDeposit{} transaction spending multiple UTxO into a deposit output.}\label{fig:depositTx} \end{figure} +*/ -\subsection{\red{Recover Transaction}}\label{sec:recover-tx} +== Recover Transaction + +/* \noindent If a \mtxDeposit{} transaction output (see~\ref{sec:deposit-tx}) was not collected into a head by an \mtxIncrement{} transaction~\ref{sec:increment-tx}, the \mtxRecover{} transaction @@ -409,9 +415,11 @@ \subsection{\red{Recover Transaction}}\label{sec:recover-tx} \caption{\mtxRecover{} transaction restoring UTxO of a deposit output.}\label{fig:recoverTx} \end{figure} +*/ +== Increment Transaction + -\subsection{\red{Increment Transaction}}\label{sec:increment-tx} - +/* \noindent The \mtxIncrement{} transaction (Figure~\ref{fig:incrementTx}) allows a participant to add a \mtxDeposit{} output~\ref{sec:deposit-tx} to an already open head using a snapshot that approves inclusion. Consequently this @@ -446,11 +454,11 @@ \subsection{\red{Increment Transaction}}\label{sec:increment-tx} $\txOutRef_{\mathsf{deposit}}$ points to the claimed deposit. The validator checks: \begin{menumerate} - \item State is advanced from $\datumHead \sim \stOpen$ to - $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$ + \item State is advanced from $\datumHead \sim sans("stOpen")$ to + $\datumHead' \sim sans("stOpen")$, parameters $\cid,\hydraKeysAgg,\nop,\cPer$ stay unchanged and the new state is governed again by $\nuHead$: \[ - (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v,\eta) \xrightarrow[\xi, s, \txOutRef_{\mathsf{increment}}]{\mathsf{increment}} (\stOpen,\cid,\hydraKeysAgg,\nop,\cPer,v',\eta') + (sans("stOpen"),\cid,\hydraKeysAgg,\nop,\cPer,v,\eta) \xrightarrow[\xi, s, \txOutRef_{\mathsf{increment}}]{\mathsf{increment}} (sans("stOpen"),\cid,\hydraKeysAgg,\nop,\cPer,v',\eta') \] \item New version $v'$ is incremented correctly \[ @@ -486,9 +494,12 @@ \subsection{\red{Increment Transaction}}\label{sec:increment-tx} \caption{\mtxIncrement{} transaction spending an open head output, producing a new head output which includes the new UTxO.}\label{fig:incrementTx} \end{figure} +*/ -\subsection{Decrement Transaction}\label{sec:decrement-tx} +== Decrement Transaction + +/* \noindent The \mtxDecrement{} transaction (Figure~\ref{fig:decrementTx}) allows a party to remove a UTxO from an already open head and consists of: @@ -505,11 +516,11 @@ \subsection{Decrement Transaction}\label{sec:decrement-tx} used snapshot number and $m$ is the number of outputs to distribute. The validator checks: \begin{menumerate} - \item State is advanced from $\datumHead \sim \stOpen$ to - $\datumHead' \sim \stOpen$, parameters $\cid,\hydraKeys,\cPer$ stay + \item State is advanced from $\datumHead \sim sans("stOpen")$ to + $\datumHead' \sim sans("stOpen")$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\xi, s, m]{\mathsf{decrement}} (\stOpen,\cid,\hydraKeys,\cPer,v',\eta') + (sans("stOpen"),\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\xi, s, m]{\mathsf{decrement}} (sans("stOpen"),\cid,\hydraKeys,\cPer,v',\eta') \] \item New version $v'$ is incremented correctly \[ @@ -539,9 +550,12 @@ \subsection{Decrement Transaction}\label{sec:decrement-tx} \caption{\mtxDecrement{} transaction spending an open head output, producing a new head output and multiple decommitted outputs.}\label{fig:decrementTx} \end{figure} +*/ -\subsection{Close Transaction}\label{sec:close-tx} +== Close Transaction + +/* In order to close a head, a head member may post the \mtxClose{} transaction (see Figure~\ref{fig:closeTx}). This transaction has \begin{itemize} @@ -553,18 +567,18 @@ \subsection{Close Transaction}\label{sec:close-tx} \begin{figure} \centering \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/closeTx.pdf} - \caption{\mtxClose{} transaction spending the $\stOpen$ head output and producing a $\stClosed$ head output.}\label{fig:closeTx} + \caption{\mtxClose{} transaction spending the $sans("stOpen")$ head output and producing a $sans("stClosed")$ head output.}\label{fig:closeTx} \end{figure} \noindent The state-machine validator $\nuHead$ is spent with $\redeemerHead = (\mathsf{close}, \mathsf{CloseType})$, where $\mathsf{CloseType}$ is a hint against which open state to close and checks: \begin{menumerate} - \item State is advanced from $\datumHead \sim \stOpen$ to - $\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeys,\cPer$ + \item State is advanced from $\datumHead \sim sans("stOpen")$ to + $\datumHead' \sim sans("stClosed")$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\mathsf{CloseType}]{\stClose} (\stClosed,\cid,\hydraKeys,\cPer,v',s',\eta', \eta_\Delta', \contesters,\Tfinal) + (sans("stOpen"),\cid,\hydraKeys,\cPer,v,\eta) \xrightarrow[\mathsf{CloseType}]{\stClose} (sans("stClosed"),\cid,\hydraKeys,\cPer,v',s',\eta', \eta_\Delta', \contesters,\Tfinal) \] \item Last known open state version is recorded in closed state \[ @@ -668,10 +682,13 @@ \subsection{Close Transaction}\label{sec:close-tx} \] \end{menumerate} -\subsection{Contest Transaction}\label{sec:contest-tx} +*/ +== Contest Transaction + +/* The \mtxContest{} transaction (see Figure~\ref{fig:contestTx}) is posted by a -party to prove the currently $\stClosed$ state is not the latest one. This +party to prove the currently $sans("stClosed")$ state is not the latest one. This transaction has \begin{itemize} \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, @@ -681,19 +698,19 @@ \subsection{Contest Transaction}\label{sec:contest-tx} \begin{figure} \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/contestTx.pdf} - \caption{\mtxContest{} transaction spending the $\stClosed$ head output and - producing a different $\stClosed$ head output.}\label{fig:contestTx} + \caption{\mtxContest{} transaction spending the $sans("stClosed")$ head output and + producing a different $sans("stClosed")$ head output.}\label{fig:contestTx} \end{figure} \noindent The state-machine validator $\nuHead$ is spent with $\redeemerHead = (\mathsf{contest}, \mathsf{ContestType})$, where $\mathsf{ContestType}$ is a hint how to verify the snapshot and checks: \begin{menumerate} - \item State is advanced from $\datumHead \sim \stOpen$ to - $\datumHead' \sim \stClosed$, parameters $\cid,\hydraKeys,\cPer$ + \item State is advanced from $\datumHead \sim sans("stOpen")$ to + $\datumHead' \sim sans("stClosed")$, parameters $\cid,\hydraKeys,\cPer$ stay unchanged and the new state is governed again by $\nuHead$ \[ - (\stClosed,\cid,\hydraKeys,\cPer,v,s,\eta,\eta_{\Delta},\contesters,\Tfinal) \xrightarrow[\mathsf{ContestType}]{\stContest} (\stClosed,\cid,\hydraKeys,\cPer,v',s',\eta',\eta_{\Delta}',\contesters',\Tfinal') + (sans("stClosed"),\cid,\hydraKeys,\cPer,v,s,\eta,\eta_{\Delta},\contesters,\Tfinal) \xrightarrow[\mathsf{ContestType}]{\stContest} (sans("stClosed"),\cid,\hydraKeys,\cPer,v',s',\eta',\eta_{\Delta}',\contesters',\Tfinal') \] \item Last known open state version stays recorded in closed state @@ -793,9 +810,11 @@ \subsection{Contest Transaction}\label{sec:contest-tx} \txMint = \varnothing \] \end{menumerate} +*/ +== Fan-Out Transaction + -\subsection{Fan-Out Transaction}\label{sec:fanout-tx} - +/* Once the contestation phase is over, a head may be finalized by posting a \mtxFanout{} transaction (see Figure~\ref{fig:fanoutTx}), which distributes UTxOs from the head according to the latest state. It consists of @@ -810,18 +829,18 @@ \subsection{Fan-Out Transaction}\label{sec:fanout-tx} \begin{figure} \centering \includegraphics[width=0.8\textwidth]{Hydra/Protocol/Figures/fanoutTx.pdf} - \caption{\mtxFanout{} transaction spending the $\stClosed$ head output and + \caption{\mtxFanout{} transaction spending the $sans("stClosed")$ head output and distributing funds with outputs $o_{1} \dots o_{m}$.}\label{fig:fanoutTx} \end{figure} \noindent The state-machine validator $\nuHead$ is spent with $\redeemerHead = (\mathsf{fanout}, m, n)$, where $m$ and $n$ are -outputs to distribute from the $\stClosed$ state, and checks: +outputs to distribute from the $sans("stClosed")$ state, and checks: \begin{menumerate} - \item State is advanced from $\datumHead \sim \stClosed$ to terminal state - $\stFinal$: % XXX: What does this actually mean? + \item State is advanced from $\datumHead \sim sans("stClosed")$ to terminal state + $sans("stFinal")$: % XXX: What does this actually mean? \[ - (\stClosed,\cid,\hydraKeys,\cPer,v, s,\eta,\eta_{\Delta},\contesters,\Tfinal) \xrightarrow[m,n]{\stFanout} \stFinal + (sans("stClosed"),\cid,\hydraKeys,\cPer,v, s,\eta,\eta_{\Delta},\contesters,\Tfinal) \xrightarrow[m,n]{\stFanout} sans("stFinal") \] \item The first $m$ outputs are distributing funds according to $\eta$. That is, the outputs exactly correspond to the UTxO canonically combined $U^{\#}$ (see @@ -848,8 +867,4 @@ \subsection{Fan-Out Transaction}\label{sec:fanout-tx} \end{menumerate} \FloatBarrier{} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: +*/ diff --git a/src/Hydra/Protocol/Overview.tex b/src/Hydra/Protocol/Overview.lagda.typ similarity index 62% rename from src/Hydra/Protocol/Overview.tex rename to src/Hydra/Protocol/Overview.lagda.typ index 57b5633..b91bff7 100644 --- a/src/Hydra/Protocol/Overview.tex +++ b/src/Hydra/Protocol/Overview.lagda.typ @@ -1,8 +1,12 @@ -\section{Protocol Overview}\label{sec:overview} += Protocol Overview + + +#import "Macros.typ": stInitial, stOpen, stClosed, stFinal +#import "Macros.typ": txCommit, txCollectCom, txDecrement The Hydra Head protocol provides functionality to lock a set of UTxOs on a -blockchain, referred to as the \emph{mainchain}, and evolve it inside a -so-called off-chain \emph{head}, independently of the mainchain. At any point, +blockchain, referred to as the _mainchain_, and evolve it inside a +so-called off-chain _head_, independently of the mainchain. At any point, the head can be closed with the effect that the locked set of UTxOs on the mainchain is replaced by the latest set of UTxOs inside the head. The protocol guarantees full wealth preservation: no generation of funds can happen off-chain @@ -12,48 +16,47 @@ \section{Protocol Overview}\label{sec:overview} under good conditions, thereby reducing latency and increasing throughput. At the same time, the head protocol provides the same capabilities as the mainchain by reusing the same ledger model and transaction formats --- making the protocol -``isomorphic''. +*isomorphic*. -\subsection{Opening the head} +== Opening the head To create a head-protocol instance, any party may take the role of an -\emph{initiator} and ask other parties, the \emph{head members}, to participate +_initiator_ and ask other parties, the _head members_, to participate in the head by exchanging public keys and agreeing on other protocol parameters. These public keys are used for both, the authentication of head-related on-chain transactions that are restricted to head members (e.g., a non-member is not allowed to close the head) and for signing off-chain transactions in the head. -The initiator then establishes the head by submitting an \emph{initial} +The initiator then establishes the head by submitting an _initial_ transaction to the mainchain that contains the Hydra protocol parameters and -mints special \emph{participation tokens (PT)} identifying the head members. The -\emph{initial} transaction also initializes a state machine (see -Fig.~\ref{fig:head-protocol-states}) that manages the ``transfer'' of UTxOs into -the head and back. The state machine comprises the four states: $\stInitial$, -$\stOpen$, $\stClosed$, and $\stFinal$. A \emph{state thread token (ST)} minted -in \emph{initial} marks the head output and ensures contract -continuity~\cite{eutxo}. +mints special _participation tokens (PT)_ identifying the head members. The +_initial_ transaction also initializes a state machine (see +@figure:head-protocol-states) that manages the ``transfer'' of UTxOs into +the head and back. The state machine comprises the four states: $stInitial$, +$stOpen$, $stClosed$, and $stFinal$. A _state thread token (ST)_ minted +in _initial_ marks the head output and ensures contract continuity @eutxo. -\input{Hydra/Protocol/Figures/head-protocol-states} +#include("Figures/head-protocol-states.typ") Once the initial transaction appears on the mainchain, establishing the initial -state $\stInitial$, each head member can attach a \mtxCom{} transaction, which +state $stInitial$, each head member can attach a $txCommit$ transaction, which locks (on the mainchain) the UTxOs that the party wants to commit to the head, or deliberately acknowledges to commit nothing. -The commit transactions are subsequently collected by the \mtxCCom{} transaction -causing a transition from $\stInitial$ to $\stOpen$. Once the $\stOpen$ state is +The commit transactions are subsequently collected by the $txCollectCom$ transaction +causing a transition from $stInitial$ to $stOpen$. Once the $stOpen$ state is confirmed, the head members start running the off-chain head protocol, which evolves the initial UTxO set (the union over all UTxOs committed by all head members) independently of the mainchain. For the case where some head members -fail to post a \mtxCom{} transaction, the head can be aborted by going directly -from $\stInitial$ to $\stFinal$. +fail to post a $txCommit$ transaction, the head can be aborted by going directly +from $stInitial$ to $stFinal$. -\subsection{The Coordinated Head protocol} +== The Coordinated Head protocol The actual Head protocol starts after the initialization phase with an initial -set of UTxOs that is identical to the UTxOs locked on-chain via the \mtxCom{} -and \mtxCCom{} transactions. +set of UTxOs that is identical to the UTxOs locked on-chain via the $txCommit$ +and $txCollectCom$ transactions. The protocol processes off-chain transactions by distributing them between participants, while each party maintains their view of the local UTxO state. That is, the current @@ -62,8 +65,8 @@ \subsection{The Coordinated Head protocol} To confirm transactions and allow for distribution of the resulting UTxO set without needing the whole transaction history, snapshots are created by the -protocol participants. The initial snapshot $U_{0}$ corresponds to the initial -UTxO set, while snapshots thereafter $\Uset_1,\Uset_2,\ldots$ are created with +protocol participants. The initial snapshot $U_0$ corresponds to the initial +UTxO set, while snapshots thereafter $\U_1,\U_2,dots$ are created with monotonically increasing snapshot numbers. For this, the next snapshot leader (round-robin) requests his view of a new confirmed state to be @@ -81,62 +84,58 @@ \subsection{The Coordinated Head protocol} transactions that have been processed into it as the snapshot's multi-signature is now evidence that this state once existed during the head evolution. -\subsubsection{Updating an open head} +=== Updating an open head Besides processing ``normal'' transactions, participants can also request to withdraw some UTxO they can spend from the Head and make it available on main -chain via a \mtxDecrement{}~\ref{sec:decrement-tx} transaction --- the overall process is also called -``decommit''. +chain via a $txDecrement)$ @sec:decrement-tx transaction --- the overall process is also called +``decommit``. +/* -\red{The inverse of locking more UTxO on the mainchain and making it available - within the head is called (incremental) ``commit''. First, anyone may create a - deposit of one or more UTxO using a \mtxDeposit{}~\ref{sec:deposit-tx} +#text(red)[The inverse of locking more UTxO on the mainchain and making it available + within the head is called (incremental) ``commit``. First, anyone may create a + deposit of one or more UTxO using a $sans("txDeposit")$ @sec:deposit-tx transaction. The head participants will observe this deposit and, once settled, request off-chain agreement to include the deposited UTxO in the form - of a snapshot. With that agreement, an \mtxIncrement{}~\ref{sec:increment-tx} + of a snapshot. With that agreement, an $sans("txIncrement")$ @sec:increment-tx transaction can be created and used to update the head state on the mainchain. A deadline is associated with the deposit, which ensures that the UTxO is locked up long enough to be safely consumed into the head without risk of double spending. Should a deposit have not been picked up in time, a - \mtxRecover{}~\ref{sec:recover-tx} transaction allows anyone to unlock the - original UTxO.} - -\subsection{Closing the head} + $sans("txRecover")$ @sec:recover-tx transaction allows anyone to unlock the + original UTxO.]) +*/ +=== Closing the head The head protocol is designed to allow any head member at any point in time to produce, without interaction, a certificate to close the head. This certificate is created from the latest confirmed, multi-signed snapshot. Using this -certificate, the head member may ``force close'' the head by advancing the -mainchain state machine to the $\stClosed$ state. +certificate, the head member may ''force close'' the head by advancing the +mainchain state machine to the $stClosed$ state. -Once in $\stClosed$, the state machine grants parties a contestation period, +Once in $stClosed$, the state machine grants parties a contestation period, during which parties may contest the closure by posting the certificate of a newer snapshot on-chain in a contest transaction. Contesting leads back to the -state $\stClosed$ and each party can contest at most once. After the -contestation period has elapsed, the state machine may proceed to the $\stFinal$ +state $stClosed$ and each party can contest at most once. After the +contestation period has elapsed, the state machine may proceed to the $stFinal$ state. The state machine enforces that the outputs of the transaction leading to -$\stFinal$ correspond exactly to the latest UTxO set seen during the +$stFinal$ correspond exactly to the latest UTxO set seen during the contestation period. -\subsection{Differences} -% TODO More details on what was in orig paper? +== Differences + +//% TODO More details on what was in orig paper? + In the Coordinated Head protocol, off-chain consensus is simplified by not having transactions confirmed concurrently to the snapshots (and to each other) but having the snapshot leader propose, in their snapshot, a set of transactions for explicit confirmation. The parties' views of confirmed transactions thus progress in sync with each other (once per confirmed snapshot), thus simplifying the close/contest procedure on the mainchain. Also, there is no need for -conflict resolution as in Appendix~B of~\cite{hydrahead20}. In summary, the -differences to the original Head protocol in~\cite{hydrahead20} are: - -\begin{itemize} - \item No hanging transactions due to `coordination'. - \item No acknowledgement nor confirmation of transactions. - \item No confirmation message for snapshots (two-round local confirmation). - \item Allow for \red{incremental commits and} decommits while head is open. -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: +conflict resolution as in Appendix~B of @hydrahead20. In summary, the +differences to the original Head protocol in @hydrahead20 are: + +- No hanging transactions due to _coordination_. +- No acknowledgement nor confirmation of transactions. +- No confirmation message for snapshots (two-round local confirmation). +- Allow for #(text(red)[incremental commits and]) decommits while head is open. diff --git a/src/Hydra/Protocol/Preliminaries.lagda.typ b/src/Hydra/Protocol/Preliminaries.lagda.typ new file mode 100644 index 0000000..1156a34 --- /dev/null +++ b/src/Hydra/Protocol/Preliminaries.lagda.typ @@ -0,0 +1,243 @@ += Preliminaries + + +#import("Macros.typ"): todo +#import("Macros.typ"): msSetup, msParams, msVK, msSign, msKeyGen, msSK + +This section introduces notation and other preliminaries used in the remainder +of the specification. + +== Notation + +The specification uses set-notation based approach while also inspired +by @eutxo-2 and @eutxo. Values $a$ are in a set $a in cal("A")$, +also indicated as being of some type $a : cal("A")$, and multidimensional values are +tuples drawn from a $*$ product of multiple sets, e.g. +$(a,b) in (cal("A") * cal("B"))$. An empty set is indicated by +$emptyset$ and sets may be enumerated using $\{a_1 dots a_n\}$ notation. The $=$ operator means +equality and $arrow.l$ is explicit assignment of a variable or value to one +or more variables. Projection is used to access the elements of a tuple, e.g. +${(a,b)}^arrow.b = a$. Functions are morphisms mapping from one set to another +$x : cal("A") arrow.r f(x) : cal("B")$, where function +application of a function $f$ to an argument $x$ is written as $f(x)$. + +Furthermore, given a set $cal("A")$, let +- $cal("A")^? = cal("A") union suit.diamond$ denotes an option: a value from $cal("A")$ or no value at all indicated by $bot$, +- $cal("A")^n$ be the set of all n-sized sequences over $cal("A")$, +- $cal("A")^! = union.big_(i=1)^(n in NN) cal("A")^i$ be the set of non-empty sequences over $cal("A")$, and +- $cal("A")^* = union.big_(i=0)^(n in NN) cal("A")^i$ be the set of all sequences over $cal("A")$. + +With this, we further define: + +- $BB = {mono("false"), mono("true")}$ are boolean values +- $NN$ are natural numbers ${0, 1, 2, dots}$ +- $ZZ$ are integer numbers ${dots, -2, -1, 0, 1, 2, dots}$ +- $bb(H) = union.big_{n=0}^infinity {0,1}^8n$ denotes a arbitrary string of bytes +- $sans("concat") : bb(H)^* arrow.r bb(H)$ is concatenating bytes, we also use operator $plus.circle.big$ for this +- $sans("hash") : x arrow.r bb(H)$ denotes a collision-resistant hashing function and $x^\#$ indicates the hash of $x$ +- $sans("bytes") : x arrow.r bb(H)s$ denotes an invertible serialisation function mapping arbitrary data to bytes +- $a || b = sans("concat")(bb(H)(a), bb(H)(b))$ is an operator which concatenates the $bb(H)(b)$ to the $bb(H)(a)$ +- Lists of values $l in cal("A")^{*}$ are written as $l = [x_1, dots, x_n]$. + Empty lists are denoted by $[]$, the $i$th element $x_i$ is also written $l[i]$ and the length of the list is $|l| = n$. + An underscore is also used to indicate a list of values $underline(x) = l$. + Projection on lists are mapped to their elements, i.e. $underline(x)^arrow.b = [x_1^arrow.b, dots, x_n^arrow.b]$. +- $sans("sortOn") : i arrow.r cal("A")^* arrow.r cal("A")^*$ does sort a list of values on the $i$th projection. +- $sans("Bytes")$ is a universal data type of nested sums and products built up recursively from the base types of $ZZ$ and $bb(H)$. + +== Public key multi-signature scheme + + +#todo("move/merge with protocol setup and make concrete") + +A multisignature scheme is a set of algorithms where +- $msSetup$ generates public parameters $msParams$, such that +- $(msVK,msSK) arrow.l msKeyGen(msParams)$ can be used to generate fresh key pairs, +/* +- $msSig arrow.l msSig (msParams),msSK(msMsg))$ signs a message $sans("msMsg")$ using key $sans("msSK")$, +- $sans("mCVK") arrow.l sans("msCombVK")(sans("msParams"),sans("msVK")L)$ aggregates a list of verification keys $sans("msVK")L$ into a single, aggregate key $sans("mCVK")$, +- $sans("msCSig") arrow.l \msComb(sans("msParams"),sans("msMsg"),sans("msVK")L,sans("msSig")L)$ aggregates a list of signatures $sans("msSig")L$ about message $m$ into a single, aggregate signature~$sans("msCSig")$. +- $\msVfy(sans("msParams"),sans("mCVK"),sans("msMsg"),sans("msCSig")) in BB$ verifies an aggregate signature $sans("msCSig")$ of message $sans("msMsg")$ under an aggregate verification key $sans("mCVK")$. + +The security definition of a multisignature scheme +from @itakura1983public,CCS:MicOhtRey01 guarantees that, if $sans("mCVK")$ is +produced from a tuple of verification keys $sans("msVK")L$ via $sans("msCombVK")$, then no +aggregate signature $sans("msCSig")$ can pass verification +$\msVfy(sans("mCVK"),sans("msMsg"),sans("msCSig"))$ unless all honest parties holding keys in +$sans("msVK")L$ signed $m$. + +Note that in the following, we make the parameter~$sans("msParams")$ implicit and leave +out the $ver$ suffix for verification key such that $k = k^ver$ for better +readability. + +== Extended UTxO} + + +The Hydra Head protocol is specified to work on the so-called Extended UTxO (EUTxO) ledgers +like Cardano. + +The basis for EUTxO is Bitcoin's UTxO ledger +model @formal-model-of-bitcoin-transactions,Zahnentferner18-UTxO. +Intuitively, it arranges transactions in a directed acyclic graph, such as the +one in @fig:utxo-graph, where boxes represent transactions with +(red) inputs to the left and (black) outputs to the right. A dangling +(unconnected) output is an \emph{unspent transaction output (UTxO)} --- there +are two UTxOs in the figure. + +#figure( + image("Figures/utxo-graph.svg", width: 50%), + caption: [ + Example of a plain UTxO graph + ] + ) + + +The following paragraphs will give definitions of the UTxO model and it's +extension to support scripting (EUTxO) suitable for this Hydra Head protocol +specification. For a more detailed introduction to the EUTxO ledger model, +see @eutxo,@eutxo-2 and @utxo-ma. + +=== Values + +/* +\begin{definition}[Values] + Values are sets that keep track of how many units of which tokens of which + currency are available. Given a finitely supported function $\mapsto$, that + maps keys to monoids, a value is the set of such mappings over currencies + (minting policy identifiers), over a mapping of token names $t$ to + quantities $q$: + \[ + \val in \tyValue = (c : bb(H) \mapsto (t : bb(H) \mapsto q : ZZ)) + \] + \noindent where addition of values is defined as $+$ and $\varnothing$ is the empty value. +\end{definition} + +For example, the value $\{c_{1} \mapsto \{t_1 \mapsto 1, t_2 \mapsto 1\}\}$ +contains tokens $t_1$ and $t_2$ of currency $c_{1}$ and addition merges +currencies and token names naturally: +\begin{align*} + & \{c_{1} \mapsto \{t_1 \mapsto 1, t_2 \mapsto 1\}\} \\ + + \ & \{c_{1} \mapsto \{t_{2} \mapsto 1, t_3 \mapsto 1\}, c_{2} \mapsto \{ t_{1} \mapsto 2\}\} \\ + = \ & \{c_{1} \mapsto \{t_1 \mapsto 1, t_2 \mapsto 2, t_3 \mapsto 1\}, c_{2} \mapsto \{ t_{1} \mapsto 2\}\} \ . +\end{align*} + +While the above definition should be sufficient for the purpose of this +specification, a full definition for finitely supported functions and values as +used here can be found in~\cite{utxo-ma}. To further improve readability, we +define the following shorthands: +- $\{t_1, \ldots, t_n\} :: c$ for a set positive single quantity assets + $\{c \mapsto \{t_1 \mapsto 1, \ldots, t_n \mapsto 1\}\}$, +- ${\{t_1, \ldots, t_n\}}^{-1} :: c$ for a set of negative single quantity assets + $\{c \mapsto \{t_1 \mapsto -1, \ldots, t_n \mapsto -1\}\}$, + +- $\{c \mapsto t \mapsto q\}$ for the value entry $\{c \mapsto \{t \mapsto q\}\}$, +- $\{c \mapsto \cdot \mapsto q \}$ for any asset with currency $c$ and + quantity $q$ irrespective of token name. + +\subsubsection{Scripts} + +Validator scripts are called \emph{phase-2} scripts in the Cardano Ledger +specification (see~\cite{ledger-alonzo-spec} for a formal treatment of these). Scripts +are used for multiple purposes, but most often (and sufficient for this +specification) as a \emph{spending} or \emph{minting} policy script. + +\begin{definition}[Minting Policy Script] + A script $\mu in cal(M)$ governing whether a value can be minted (or + burned), is a pure function with type + \[ + \mu in cal(M) = (\rho : sans("Bytes")) arrow.r (\txContext : \tyContext) arrow.r BB, + \] + where $\rho in sans("Bytes")$ is the redeemer provided as part of the transaction + being validated and $\txContext in \tyContext$ is the validation + context. +\end{definition} + +\begin{definition}[Spending Validator Script] + A validator script $\nu in \mathcal{V}$ governing whether an output can be + spent, is a pure function with type + \[ + \nu in \mathcal{V} = (\delta : sans("Bytes")) arrow.r (\rho : sans("Bytes")) arrow.r (\txContext : \tyContext) arrow.rBB, + \] + where $\delta in sans("Bytes")$ is the datum available at the output to be spent, + $\rho in sans("Bytes")$ is the redeemer data provided as part of the transaction + being validated, and $\txContext in \tyContext$ is the validation + context. +\end{definition} + +\subsubsection{Transactions} +arrow.rdo{actual transactions $\mathcal{T}$ are not defined} + +We define EUTxO inputs, outputs and transactions as they are available to +scripts and just enough to specify the behavior of the Hydra validator scripts. +For example outputs addresses and datums are much more complicated in the full +ledger model~\cite{eutxo-2, ledger-shelley-spec}. + +\begin{definition}[Outputs] + An output $o in \txOutputs$ stores some value $\val in \tyValue$ at some address, + defined by the hash of a validator script $\nu^{\#} in bb(H) = \hash(\nu in \mathcal{V})$, + and may store (reference) some data $\delta in sans("Bytes")$: + \[ + o in \txOutputs = (\val : \tyValue \times \nu^{\#} : bb(H) \times \delta : sans("Bytes")) + \] +\end{definition} + +\begin{definition}[Output references] + An output reference $\txOutRef in \tyOutRef$ points to an output of a + transaction, using a transaction id (that is, a hash of the transaction body) + and the output index within that transaction. + \[ + \txOutRef in \tyOutRef = (bb(H) \times NN) + \] +\end{definition} + +\begin{definition}[Inputs] + A transaction input $i in \txInputs$ is an output reference + $\txOutRef in \tyOutRef$ with a corresponding redeemer $\rho in sans("Bytes")$: + \[ + i in \txInputs = (\txOutRef : \tyOutRef \times \rho : sans("Bytes")) + \] +\end{definition} + +\begin{definition}[Validation Context] + A validation context $\txContext in \tyContext$ is a view on the transaction + to be validated: + \[ + \txContext in \tyContext = (\tyInputs \times \tyOutputs \times \tyValue \times \mathcal{S}^{\leftrightarrow} \times \mathcal{K}) + \] + where $\txInputs in \tyInputs$ is a \textbf{set} of inputs, + $\txOutputs in \tyOutputs$ is a \textbf{list} of outputs, + $\txMint in \tyValue$ is the minted (or burned) value, + $(\txValidityMin, \txValidityMax) in \tyValidity$ are the lower and upper + validity bounds where $\txValidityMin <= \txValidityMax$, and + $\txKeys in \mathcal{K}$ is the set of verification keys which signed the + transaction. + % TODO: \tyValidity undefined, define time, periods and intervals? +\end{definition} + +Informally, scripts are evaluated by the ledger when it applies a transaction to +its current state to yield a new ledger state (besides checking the transaction +integrity, signatures and ledger rules). Each validator script referenced by +an output is passed its arguments drawn from the output it locks and the +transaction context it is executed in. The transaction is valid if and only if +all scripts validate, i.e. $\mu(\rho, \txContext) = \true$ and +$\nu(\delta, \rho, \txContext) = \true$. + +=== State machines and graphical notation + +State machines in the EUTxO ledger model are commonly described using the +\emph{constraint emitting machine (CEM)} formalism~\cite{eutxo}, e.g.~the +original paper describes the Hydra Head protocol using this +notation~\cite{hydrahead20}. Although inspired by CEMs, this specification uses +a more direct representation of individual transactions to simplify description +of non-state-machine transactions and help translation to concrete +implementations on Cardano. The structure of the state machine is enforced +on-chain through \emph{scripts} which run as part of the ledger's validation of +a transaction (see Section~\ref{sec:eutxo}). For each protocol transaction, the +specification defines the structure of the transaction and enumerates the +transaction constraints enforced by the scripts ($\cemTxCon$ in the CEM +formalism). + +% TODO: Create example, maybe using the collectComTx, but with generic labels +% and point out that state input/outputs do represent a transition in the +% statemachine from s' to s' etc. +TODO{Add an example graph with a legend} +*/ diff --git a/src/Hydra/Protocol/Preliminaries.tex b/src/Hydra/Protocol/Preliminaries.tex deleted file mode 100644 index c221a61..0000000 --- a/src/Hydra/Protocol/Preliminaries.tex +++ /dev/null @@ -1,258 +0,0 @@ -\clearpage -\section{Preliminaries}\label{sec:prel} - -This section introduces notation and other preliminaries used in the remainder -of the specification. - -\subsection{Notation} - -The specification uses set-notation based approach while also inspired -by~\cite{eutxo-2}~and~\cite{eutxo}. Values $a$ are in a set $a \in \mathcal{A}$, -also indicated as being of some type $a : \mathcal{A}$, and multidimensional values are -tuples drawn from a $\times$ product of multiple sets, e.g. -$(a,b) \in (\mathcal{A} \times \mathcal{B})$. An empty set is indicated by -$\emptyset$ and sets may be enumerated using $\{a_1 \dots a_n\}$ notation. The $=$ operator means -equality and $\gets$ is explicit assignment of a variable or value to one -or more variables. Projection is used to access the elements of a tuple, e.g. -${(a,b)}^{\downarrow1} = a$. Functions are morphisms mapping from one set to another -$x : \mathcal{A} \to f(x) : \mathcal{B}$, where function -application of a function $f$ to an argument $x$ is written as $f(x)$. \\ - -\noindent Furthermore, given a set $\mathcal{A}$, let -\begin{itemize} - \item $\mathcal{A}^? = \mathcal{A} \cup \Diamond$ denotes an option: a value from $\mathcal{A}$ or no value at all indicated by $\bot$, - \item $\mathcal{A}^n$ be the set of all n-sized sequences over $\mathcal{A}$, - \item $\mathcal{A}^! = \bigcup_{i=1}^{n \in \tyNatural} \mathcal{A}^{i}$ be the set of non-empty sequences over $\mathcal{A}$, and - \item $\mathcal{A}^* = \bigcup_{i=0}^{n \in \tyNatural} \mathcal{A}^{i}$ be - the set of all sequences over $\mathcal{A}$. -\end{itemize} - -\noindent With this, we further define: -\begin{itemize} - \item $\tyBool = \{\false, \true\}$ are boolean values - \item $\tyNatural$ are natural numbers $\{0, 1, 2, \ldots\}$ - \item $\tyInteger$ are integer numbers $\{\ldots, -2, -1, 0, 1, 2, \ldots\}$ - \item $\tyBytes = \bigcup_{n=0}^{\inf}{\{0,1\}}^{8n}$ denotes a arbitrary - string of bytes - \item $\concat : \tyBytes^* \to \tyBytes$ is concatenating bytes, we also use operator $\bigoplus$ for this - \item $\hash : x \to \tyBytes$ denotes a collision-resistant - hashing function and $x^{\#}$ indicates the hash of $x$ - \item $\bytes : x \to \tyBytes$ denotes an invertible serialisation function - mapping arbitrary data to bytes - \item $a || b = \concat(\bytes(a), \bytes(b))$ is an operator which concatenates the $\bytes(b)$ to the $\bytes(a)$ - \item Lists of values $l \in \mathcal{A}^{*}$ are written as - $l = [x_{1}, \ldots, x_{n}]$. Empty lists are denoted by $[]$, the $i$th - element $x_{i}$ is also written $l[i]$ and the length of the list is - $|l| = n$. An underscore is also used to indicate a list of values - $\underline{x} = l$. Projection on lists are mapped to their elements, - i.e. - $\underline{x}^{\downarrow1} = [x_{1}^{\downarrow1}, \dots, x_{n}^{\downarrow1}]$. - \item $\sortOn : i \to \mathcal{A}^{*} \to \mathcal{A}^{*}$ does sort a list of - values on the $i$th projection. - \item $\tyData$ is a universal data type of nested sums and products built up - recursively from the base types of $\tyInteger$ and $\tyBytes$. -\end{itemize} - -\subsection{Public key multi-signature scheme}\label{sec:multisig} -% TODO: move/merge with protocol setup and make concrete -\noindent A multisignature scheme is a set of algorithms where -\begin{itemize} - \item $\msSetup$ generates public parameters $\msParams$, such that - \item $(\msVK,\msSK) \gets \msKeyGen(\msParams)$ can be used to generate fresh - key pairs, - \item $\msSig \gets \msSign(\msParams,\msSK,\msMsg)$ signs a message $\msMsg$ - using key $\msSK$, - \item $\msCVK \gets \msCombVK(\msParams,\msVKL)$ aggregates a list of - verification keys $\msVKL$ into a single, aggregate key $\msCVK$, - \item $\msCSig \gets \msComb(\msParams,\msMsg,\msVKL,\msSigL)$ aggregates a - list of signatures $\msSigL$ about message $m$ into a single, aggregate - signature~$\msCSig$. - \item $\msVfy(\msParams,\msCVK,\msMsg,\msCSig) \in \tyBool$ verifies an aggregate - signature $\msCSig$ of message $\msMsg$ under an aggregate verification - key $\msCVK$. -\end{itemize} - -The security definition of a multisignature scheme -from~\cite{itakura1983public,CCS:MicOhtRey01} guarantees that, if $\msCVK$ is -produced from a tuple of verification keys $\msVKL$ via $\msCombVK$, then no -aggregate signature $\msCSig$ can pass verification -$\msVfy(\msCVK,\msMsg,\msCSig)$ unless all honest parties holding keys in -$\msVKL$ signed $m$. - -Note that in the following, we make the parameter~$\msParams$ implicit and leave -out the $ver$ suffix for verification key such that $k = k^{ver}$ for better -readability. - -\subsection{Extended UTxO}\label{sec:eutxo} -The Hydra Head protocol is specified to work on the so-called Extended UTxO (EUTxO) ledgers -like Cardano. - -The basis for EUTxO is Bitcoin's UTxO ledger -model~\cite{formal-model-of-bitcoin-transactions,Zahnentferner18-UTxO}. -Intuitively, it arranges transactions in a directed acyclic graph, such as the -one in Figure~\ref{fig:utxo-graph}, where boxes represent transactions with -(red) inputs to the left and (black) outputs to the right. A dangling -(unconnected) output is an \emph{unspent transaction output (UTxO)} --- there -are two UTxOs in the figure. - -\begin{figure}[h] - \centering - \includegraphics[width=0.5\textwidth]{Hydra/Protocol/Figures/utxo-graph.pdf} - \caption{Example of a plain UTxO graph}\label{fig:utxo-graph} -\end{figure} - -The following paragraphs will give definitions of the UTxO model and it's -extension to support scripting (EUTxO) suitable for this Hydra Head protocol -specification. For a more detailed introduction to the EUTxO ledger model, -see~\cite{eutxo},~\cite{eutxo-2}~and~\cite{utxo-ma}. - -\subsubsection{Values} - -\begin{definition}[Values] - Values are sets that keep track of how many units of which tokens of which - currency are available. Given a finitely supported function $\mapsto$, that - maps keys to monoids, a value is the set of such mappings over currencies - (minting policy identifiers), over a mapping of token names $t$ to - quantities $q$: - \[ - \val \in \tyValue = (c : \tyBytes \mapsto (t : \tyBytes \mapsto q : \tyInteger)) - \] - \noindent where addition of values is defined as $+$ and $\varnothing$ is the empty value. -\end{definition} - -For example, the value $\{c_{1} \mapsto \{t_1 \mapsto 1, t_2 \mapsto 1\}\}$ -contains tokens $t_1$ and $t_2$ of currency $c_{1}$ and addition merges -currencies and token names naturally: -\begin{align*} - & \{c_{1} \mapsto \{t_1 \mapsto 1, t_2 \mapsto 1\}\} \\ - + \ & \{c_{1} \mapsto \{t_{2} \mapsto 1, t_3 \mapsto 1\}, c_{2} \mapsto \{ t_{1} \mapsto 2\}\} \\ - = \ & \{c_{1} \mapsto \{t_1 \mapsto 1, t_2 \mapsto 2, t_3 \mapsto 1\}, c_{2} \mapsto \{ t_{1} \mapsto 2\}\} \ . -\end{align*} - -While the above definition should be sufficient for the purpose of this -specification, a full definition for finitely supported functions and values as -used here can be found in~\cite{utxo-ma}. To further improve readability, we -define the following shorthands: -\begin{itemize} - \item $\{t_1, \ldots, t_n\} :: c$ for a set positive single quantity assets - $\{c \mapsto \{t_1 \mapsto 1, \ldots, t_n \mapsto 1\}\}$, - \item ${\{t_1, \ldots, t_n\}}^{-1} :: c$ for a set of negative single quantity assets - $\{c \mapsto \{t_1 \mapsto -1, \ldots, t_n \mapsto -1\}\}$, - - \item $\{c \mapsto t \mapsto q\}$ for the value entry $\{c \mapsto \{t \mapsto q\}\}$, - \item $\{c \mapsto \cdot \mapsto q \}$ for any asset with currency $c$ and - quantity $q$ irrespective of token name. -\end{itemize} - -\subsubsection{Scripts} - -Validator scripts are called \emph{phase-2} scripts in the Cardano Ledger -specification (see~\cite{ledger-alonzo-spec} for a formal treatment of these). Scripts -are used for multiple purposes, but most often (and sufficient for this -specification) as a \emph{spending} or \emph{minting} policy script. - -\begin{definition}[Minting Policy Script] - A script $\mu \in \mathcal{M}$ governing whether a value can be minted (or - burned), is a pure function with type - \[ - \mu \in \mathcal{M} = (\rho : \tyData) \to (\txContext : \tyContext) \to\tyBool, - \] - where $\rho \in \tyData$ is the redeemer provided as part of the transaction - being validated and $\txContext \in \tyContext$ is the validation - context. -\end{definition} - -\begin{definition}[Spending Validator Script] - A validator script $\nu \in \mathcal{V}$ governing whether an output can be - spent, is a pure function with type - \[ - \nu \in \mathcal{V} = (\delta : \tyData) \to (\rho : \tyData) \to (\txContext : \tyContext) \to\tyBool, - \] - where $\delta \in \tyData$ is the datum available at the output to be spent, - $\rho \in \tyData$ is the redeemer data provided as part of the transaction - being validated, and $\txContext \in \tyContext$ is the validation - context. -\end{definition} - -\subsubsection{Transactions} -\todo{actual transactions $\mathcal{T}$ are not defined} - -We define EUTxO inputs, outputs and transactions as they are available to -scripts and just enough to specify the behavior of the Hydra validator scripts. -For example outputs addresses and datums are much more complicated in the full -ledger model~\cite{eutxo-2, ledger-shelley-spec}. - -\begin{definition}[Outputs] - An output $o \in \txOutputs$ stores some value $\val \in \tyValue$ at some address, - defined by the hash of a validator script $\nu^{\#} \in \tyBytes = \hash(\nu \in \mathcal{V})$, - and may store (reference) some data $\delta \in \tyData$: - \[ - o \in \txOutputs = (\val : \tyValue \times \nu^{\#} : \tyBytes \times \delta : \tyData) - \] -\end{definition} - -\begin{definition}[Output references] - An output reference $\txOutRef \in \tyOutRef$ points to an output of a - transaction, using a transaction id (that is, a hash of the transaction body) - and the output index within that transaction. - \[ - \txOutRef \in \tyOutRef = (\tyBytes \times \mathbb{N}) - \] -\end{definition} - -\begin{definition}[Inputs] - A transaction input $i \in \txInputs$ is an output reference - $\txOutRef \in \tyOutRef$ with a corresponding redeemer $\rho \in \tyData$: - \[ - i \in \txInputs = (\txOutRef : \tyOutRef \times \rho : \tyData) - \] -\end{definition} - -\begin{definition}[Validation Context] - A validation context $\txContext \in \tyContext$ is a view on the transaction - to be validated: - \[ - \txContext \in \tyContext = (\tyInputs \times \tyOutputs \times \tyValue \times \mathcal{S}^{\leftrightarrow} \times \mathcal{K}) - \] - where $\txInputs \in \tyInputs$ is a \textbf{set} of inputs, - $\txOutputs \in \tyOutputs$ is a \textbf{list} of outputs, - $\txMint \in \tyValue$ is the minted (or burned) value, - $(\txValidityMin, \txValidityMax) \in \tyValidity$ are the lower and upper - validity bounds where $\txValidityMin <= \txValidityMax$, and - $\txKeys \in \mathcal{K}$ is the set of verification keys which signed the - transaction. - % TODO: \tyValidity undefined, define time, periods and intervals? -\end{definition} - -Informally, scripts are evaluated by the ledger when it applies a transaction to -its current state to yield a new ledger state (besides checking the transaction -integrity, signatures and ledger rules). Each validator script referenced by -an output is passed its arguments drawn from the output it locks and the -transaction context it is executed in. The transaction is valid if and only if -all scripts validate, i.e. $\mu(\rho, \txContext) = \true$ and -$\nu(\delta, \rho, \txContext) = \true$. - -\subsubsection{State machines and graphical notation} - -State machines in the EUTxO ledger model are commonly described using the -\emph{constraint emitting machine (CEM)} formalism~\cite{eutxo}, e.g.~the -original paper describes the Hydra Head protocol using this -notation~\cite{hydrahead20}. Although inspired by CEMs, this specification uses -a more direct representation of individual transactions to simplify description -of non-state-machine transactions and help translation to concrete -implementations on Cardano. The structure of the state machine is enforced -on-chain through \emph{scripts} which run as part of the ledger's validation of -a transaction (see Section~\ref{sec:eutxo}). For each protocol transaction, the -specification defines the structure of the transaction and enumerates the -transaction constraints enforced by the scripts ($\cemTxCon$ in the CEM -formalism). - -% TODO: Create example, maybe using the collectComTx, but with generic labels -% and point out that state input/outputs do represent a transition in the -% statemachine from s' to s' etc. -\todo{Add an example graph with a legend} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: diff --git a/src/Hydra/Protocol/Security.tex b/src/Hydra/Protocol/Security.lagda.typ similarity index 97% rename from src/Hydra/Protocol/Security.tex rename to src/Hydra/Protocol/Security.lagda.typ index ac26a94..33121c9 100644 --- a/src/Hydra/Protocol/Security.tex +++ b/src/Hydra/Protocol/Security.lagda.typ @@ -1,7 +1,13 @@ -\section{Security (WIP --- Iteration 1)}\label{sec:security} -\todo{The security analysis is still \textbf{sketchy}, with the goal to make it more formal in upcoming iterations} += Security (WIP --- Iteration 1) + -\todo{Add security experiment} +#import "Macros.typ": todo + +#todo("The security analysis is still \textbf{sketchy}, with the goal to make it more formal in upcoming iterations") + +#todo("Add security experiment") + +/* \noindent Adversaries: \begin{mdescription} @@ -202,8 +208,4 @@ \subsection{Proofs} $\bigcup_{p_i\in\Hcont}\Tbar_i\subseteq\bigcap_{p_i\in\honest}\That_i$, and completeness follows. \end{proof} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: +*/ diff --git a/src/Hydra/Protocol/Setup.lagda.typ b/src/Hydra/Protocol/Setup.lagda.typ new file mode 100644 index 0000000..5b2dfef --- /dev/null +++ b/src/Hydra/Protocol/Setup.lagda.typ @@ -0,0 +1,38 @@ += Protocol Setup + + +In order to create a head-protocol instance, an initiator invites a set of +participants (the initiator being one of them) to join by announcing to them the +protocol parameters. + +- For on-chain transaction authentication (Cardano) purposes, each party + $\P_i$ generates a corresponding key pair $(sans("msVK")_i,sans("msSK")_i)$ + and sends their verification key $(sans("msVK")_i$ to all other parties. In + the case of Cardano, these are Ed25519 keys. + +- For off-chain signing (Hydra) purposes, a very basic multisignature scheme (MS, as defined in Section~\ref{sec:multisig}) based on EdDSA using Ed25519 keys is used: + - $sans("msKeyGen")$ is Ed25519 key generation (requires no parameters) + - $sans("msSign")$ creates an EdDSA signature + - $sans("msCombVK")$ is concatenation of verification keys into an ordered list + - $sans("msComb")$ is concatenation of signatures into an ordered list + - $sans("msVfy")$ verifies the "aggregate" signature by verifying each individual EdDSA signature under the corresponding Ed25519 verification key + + To help distinguish on- and off-chain key sets, Cardano verification + keys are written $sans("cardanoKey")$, while Hydra verification keys are + indicated as $sans("hydraKey")$ for the remainder of this document. + + % TODO: Move this and previous bullet point into the preliminary section, or all multi-sig definition here? + + - Each party $\P_i$ generates a hydra key pair and sends their hydra verification key to all other parties. + + - Each party $\P_i$ computes the aggregate key from the received verification keys, stores the aggregate key, + their signing key as well as the number of participants $\nop$. + + - Each party establishes pairwise communication channels to all other parties. That is, every network message received from a specific party is checked for (channel) authentication. It is the implementer’s duty to find a suitable authentication process for the communication channels. + + - All parties agree on a contestation period $sans("cPer")$. + +If any of the above fails (or the party does not agree to join the head in the +first place), the party aborts the initiation protocol and ignores any further +action. Finally, at least one of the participants posts the \mtxInit{} transaction +onchain as described next in @on-chain. diff --git a/src/Hydra/Protocol/Setup.tex b/src/Hydra/Protocol/Setup.tex deleted file mode 100644 index 9d6e3ea..0000000 --- a/src/Hydra/Protocol/Setup.tex +++ /dev/null @@ -1,46 +0,0 @@ -\clearpage -\section{Protocol Setup}\label{sec:setup} -In order to create a head-protocol instance, an initiator invites a set of -participants (the initiator being one of them) to join by announcing to them the -protocol parameters. - -\begin{itemize} - \item For on-chain transaction authentication (Cardano) purposes, each party - $\party_i$ generates a corresponding key pair $(\msVK_{i},\msSK_{i})$ - and sends their verification key $\msVK_{i}$ to all other parties. In - the case of Cardano, these are Ed25519 keys. - - \item For off-chain signing (Hydra) purposes, a very basic multisignature scheme (MS, as defined in Section~\ref{sec:multisig}) based on EdDSA using Ed25519 keys is used: - \begin{itemize} - \item $\msKeyGen$ is Ed25519 key generation (requires no parameters) - \item $\msSign$ creates an EdDSA signature - \item $\msCombVK$ is concatenation of verification keys into an ordered list - \item $\msComb$ is concatenation of signatures into an ordered list - \item $\msVfy$ verifies the "aggregate" signature by verifying each individual EdDSA signature under the corresponding Ed25519 verification key - \end{itemize} - - To help distinguish on- and off-chain key sets, Cardano verification - keys are written $\cardanoKey$, while Hydra verification keys are - indicated as $\hydraKey$ for the remainder of this document. - - % TODO: Move this and previous bullet point into the preliminary section, or all multi-sig definition here? - - \item Each party $\party_i$ generates a hydra key pair and sends their hydra verification key to all other parties. - - \item Each party $\party_i$ computes the aggregate key from the received verification keys, stores the aggregate key, - their signing key as well as the number of participants $\nop$. - - \item Each party establishes pairwise communication channels to all other parties. That is, every network message received from a specific party is checked for (channel) authentication. It is the implementer’s duty to find a suitable authentication process for the communication channels. - - \item All parties agree on a contestation period $\cPer$. -\end{itemize} - -If any of the above fails (or the party does not agree to join the head in the -first place), the party aborts the initiation protocol and ignores any further -action. Finally, at least one of the participants posts the \mtxInit{} transaction -onchain as described next in Section~\ref{sec:on-chain}. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: diff --git a/src/Hydra/Protocol/Throwaway.lagda b/src/Hydra/Protocol/Throwaway.lagda.typ similarity index 98% rename from src/Hydra/Protocol/Throwaway.lagda rename to src/Hydra/Protocol/Throwaway.lagda.typ index 12379f9..636101b 100644 --- a/src/Hydra/Protocol/Throwaway.lagda +++ b/src/Hydra/Protocol/Throwaway.lagda.typ @@ -1,9 +1,7 @@ -\section{Throwaway Examples} - -\subsection{Script Verification Example} += Throwaway These are here for reference as we convert the LaTex spec into Agda. -\begin{code} +``` open import Ledger.Prelude hiding (fromList; ε); open Computational open import ScriptVerification.Prelude @@ -211,12 +209,10 @@ f = on Init from Client , do _ : f ≡ success "foo" _ = refl +``` -\end{code} - -\subsubsection{Variables} -\begin{code} - +== Variables +``` open import Agda.Builtin.Nat public using (zero; suc) renaming (Nat to ℕ) @@ -234,5 +230,4 @@ variable 𝓛^ : UTxO 𝓣^ : List Tx tx𝜔 : Maybe Tx - -\end{code} +``` diff --git a/src/conf.typ b/src/conf.typ new file mode 100644 index 0000000..89b5090 --- /dev/null +++ b/src/conf.typ @@ -0,0 +1,24 @@ +#let conf( + title: none, + authors: (), + abstract: [], + doc, +) = { + + set align(center+horizon) + text(17pt, title) + + let count = authors.len() + let ncols = calc.min(count, 3) + grid( + columns: (1fr,) * ncols, + row-gutter: 24pt, + ..authors.map(author => [ + #author.name \ + #link("mailto:" + author.email) + ]), + ) + + set align(left+top) + doc +} diff --git a/src/fonts/StrippedJuliaMono-Black.ttf b/src/fonts/StrippedJuliaMono-Black.ttf deleted file mode 100644 index 080a723..0000000 Binary files a/src/fonts/StrippedJuliaMono-Black.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-BlackItalic.ttf b/src/fonts/StrippedJuliaMono-BlackItalic.ttf deleted file mode 100644 index 9000cdb..0000000 Binary files a/src/fonts/StrippedJuliaMono-BlackItalic.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-Bold.ttf b/src/fonts/StrippedJuliaMono-Bold.ttf deleted file mode 100644 index f511031..0000000 Binary files a/src/fonts/StrippedJuliaMono-Bold.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-BoldItalic.ttf b/src/fonts/StrippedJuliaMono-BoldItalic.ttf deleted file mode 100644 index 8819465..0000000 Binary files a/src/fonts/StrippedJuliaMono-BoldItalic.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-BoldLatin.ttf b/src/fonts/StrippedJuliaMono-BoldLatin.ttf deleted file mode 100644 index 6f20507..0000000 Binary files a/src/fonts/StrippedJuliaMono-BoldLatin.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-ExtraBold.ttf b/src/fonts/StrippedJuliaMono-ExtraBold.ttf deleted file mode 100644 index b9dfb47..0000000 Binary files a/src/fonts/StrippedJuliaMono-ExtraBold.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-ExtraBoldItalic.ttf b/src/fonts/StrippedJuliaMono-ExtraBoldItalic.ttf deleted file mode 100644 index 8b4a741..0000000 Binary files a/src/fonts/StrippedJuliaMono-ExtraBoldItalic.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-Light.ttf b/src/fonts/StrippedJuliaMono-Light.ttf deleted file mode 100644 index 3ab4e9d..0000000 Binary files a/src/fonts/StrippedJuliaMono-Light.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-LightItalic.ttf b/src/fonts/StrippedJuliaMono-LightItalic.ttf deleted file mode 100644 index de68148..0000000 Binary files a/src/fonts/StrippedJuliaMono-LightItalic.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-Medium.ttf b/src/fonts/StrippedJuliaMono-Medium.ttf deleted file mode 100644 index 623a3fc..0000000 Binary files a/src/fonts/StrippedJuliaMono-Medium.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-MediumItalic.ttf b/src/fonts/StrippedJuliaMono-MediumItalic.ttf deleted file mode 100644 index 2018692..0000000 Binary files a/src/fonts/StrippedJuliaMono-MediumItalic.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-Regular.ttf b/src/fonts/StrippedJuliaMono-Regular.ttf deleted file mode 100644 index 408c4b2..0000000 Binary files a/src/fonts/StrippedJuliaMono-Regular.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-RegularItalic.ttf b/src/fonts/StrippedJuliaMono-RegularItalic.ttf deleted file mode 100644 index 2ac8165..0000000 Binary files a/src/fonts/StrippedJuliaMono-RegularItalic.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-RegularLatin.ttf b/src/fonts/StrippedJuliaMono-RegularLatin.ttf deleted file mode 100644 index 1b3dfaa..0000000 Binary files a/src/fonts/StrippedJuliaMono-RegularLatin.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-SemiBold.ttf b/src/fonts/StrippedJuliaMono-SemiBold.ttf deleted file mode 100644 index ffb42ec..0000000 Binary files a/src/fonts/StrippedJuliaMono-SemiBold.ttf and /dev/null differ diff --git a/src/fonts/StrippedJuliaMono-SemiBoldItalic.ttf b/src/fonts/StrippedJuliaMono-SemiBoldItalic.ttf deleted file mode 100644 index b2d161e..0000000 Binary files a/src/fonts/StrippedJuliaMono-SemiBoldItalic.ttf and /dev/null differ diff --git a/src/macros.tex b/src/macros.tex deleted file mode 100644 index d8dca6b..0000000 --- a/src/macros.tex +++ /dev/null @@ -1,697 +0,0 @@ -% Hydra Macros -% -% Contains a subset of the original hydra papers, but still a lot of unused things. - -% === Misc === - -\newcommand{\red}[1]{\textcolor{red}{#1}} -\newcommand{\blue}[1]{\textcolor{blue}{#1}} - -\newcommand{\md}{\textsf{-}} - -\newcommand{\fst}[1]{#1^{\text{st}}} -\newcommand{\snd}[1]{#1^{\text{nd}}} -\newcommand{\trd}[1]{#1^{\text{rd}}} -\newcommand{\ith}[1]{#1^{\text{th}}} - -\newcommand{\eps}{\varepsilon} -\newcommand{\mc}{\mathcal} - -\DeclareMathOperator*{\argmax}{arg\,max} -\DeclareMathOperator*{\argmin}{arg\,min} - -% === General === -\newcommand{\ol}[1]{\overline{#1}} - -\newcommand{\true}{\mathtt{true}} -\newcommand{\false}{\mathtt{false}} - -\newcommand{\spara}{k} - -\newcommand{\nop}{n} -\newcommand{\party}{\mathsf p} -\newcommand{\parties}{\mathcal{P}} - -\newcommand{\adv}{\ensuremath{\mathcal{A}}} -\newcommand{\att}{\adv} -\newcommand{\advLive}{\ensuremath{\mathcal{A}}_{\mathsf L}} - -\newcommand{\propName}{\textsc} - -\newcommand{\hout}[1]{h_{\mathsf{out},#1}} -\newcommand{\hrest}{h_{\mathsf{rest}}} - -\newcommand{\es}{\eps} - - -% === Theorem Environments === - -\newtheoremstyle{putaneffinperiod}% name of the style to be used -{\topsep}% measure of space to leave above the theorem. E.g.: 3pt -{\topsep}% measure of space to leave below the theorem. E.g.: 3pt -{\itshape}% name of font to use in the body of the theorem -{0pt}% measure of space to indent -{\bfseries}% name of head font -{.}% punctuation between head and body -{1em}% space after theorem head; " " = normal interword space -{\thmname{#1}\thmnumber{ #2}\thmnote{ (#3)}} -\theoremstyle{putaneffinperiod} - -\newtheorem{theorem}{Theorem} -% \numberwithin{theorem}{chapter} -\newtheorem{lemma}[theorem]{Lemma} -\newtheorem{corollary}[theorem]{Corollary} -\newtheorem{proposition}[theorem]{Proposition} -\newtheorem{claim}[theorem]{Claim} -\newtheorem{definition}{Definition} -% \numberwithin{definition}{chapter} -\newtheorem{invariant}{Invariant} -\newtheorem{axiom}[theorem]{Axiom} -\newtheorem{postulate}{Postulate} -\theoremstyle{definition} -\newtheorem{example}{Example} -\newtheorem{construction}{Construction} - - -% === Transactions === - -\newcommand{\tyBool}{\mathbb{B}} -\newcommand{\tyNatural}{\mathbb{N}} -\newcommand{\tyInteger}{\mathbb{Z}} -\newcommand{\tyData}{\mathsf{Data}} -\newcommand{\tyBytes}{\mathbb{H}} - -\newcommand{\datum}{\delta} % a datum -\newcommand{\redeemer}{\rho} % a redeemer - -\newcommand{\txContext}{\gamma} % validation context -\newcommand{\tyContext}{\Gamma} % type of contexts - -\newcommand{\val}{\mathsf{val}} % a value -\newcommand{\tyValue}{\mathsf{Val}} % type of values - -\newcommand{\tx}{\mathrm{tx}} -\newcommand{\txA}{\mathrm{txA}} -\newcommand{\txB}{\mathrm{txB}} -\newcommand{\validTx}{\mathsf{valid\md{}tx}} -\newcommand{\applytx}{\circ} -\newcommand{\Reach}{\mathsf{Reach}} - -\newcommand{\txTx}{\mathit{tx}} % transaction value -\newcommand{\txTxTy}{\mathit{Tx}} % transaction type -\newcommand{\txCIdTy}{\mathit{CId}} % currency identifier type -\newcommand{\txTokenTy}{\mathit{Token}} % currency token type -\newcommand{\txKeys}{\kappa} % (public) keys signing the tx -\newcommand{\tyKeys}{\mathcal{K}^*} % type of keys -\newcommand{\txOutRef}{\phi} % output reference -\newcommand{\tyOutRef}{\Phi} % type of output references -\newcommand{\txInputs}{\mathcal{I}} % set of inputs -\newcommand{\tyInputs}{\mathcal{I}^*} % type of input sets -\newcommand{\txOutputs}{\mathcal{O}} % list of outputs -\newcommand{\tyOutputs}{\mathcal{O}^*} % type of output lists -\newcommand{\txMint}{\mathsf{mint}} % minted value -\newcommand{\ID}{\mathsf{ID}} -\newcommand{\txIdx}{\mathit{txIdx}} -\newcommand{\txValidityMin}{t_{\mathsf{min}}} -\newcommand{\txValidityMax}{t_{\mathsf{max}}} -\newcommand{\tyValidity}{\mathcal{S}^{\leftrightarrow}} % type of validity intervals - -% other times and periods -\newcommand{\cPer}{T} -\newcommand{\Tfinal}{t_{\mathsf{final}}} - -\newcommand{\txIpend}{i_{\mathsf{pend}}} -\newcommand{\txIpendSet}{I_{\mathsf{pend}}} - -\newcommand{\Tset}{T} -\newcommand{\Uset}{U} -\newcommand{\Uinit}{\Uset_{0}} -\newcommand{\Ufinal}{\Uset_{\mathsf{final}}} - -\newcommand{\recordUTxO}{\mathsf{recordUTxO}} - -% === Multisignatures === - -\newcommand{\ms}{\mathsf{MS}} - -\newcommand{\msSetup}{\mathsf{MS\md{}Setup}} -\newcommand{\msKeyGen}{\mathsf{MS\md{}KG}} -\newcommand{\msSign}{\mathsf{MS\md{}Sign}} -\newcommand{\msVfy}{\mathsf{MS\md{}Verify}} -\newcommand{\msComb}{\mathsf{MS\md{}ASig}} -\newcommand{\msCombVK}{\mathsf{MS\md{}AVK}} -\newcommand{\msCombVfy}{\mathsf{MS\md{}AVerify}} - -\newcommand{\msParams}{\Pi} -\newcommand{\msSig}{\sigma} -\newcommand{\msSigL}{\overline{\sigma}} -\newcommand{\msCSig}{\tilde\sigma} -\newcommand{\msVK}{k^{ver}} -\newcommand{\msCVK}{\tilde{k}} -\newcommand{\msVKL}{\overline{k}} -\newcommand{\msSK}{k^{sig}} -\newcommand{\msMsg}{m} - -\newcommand{\initial}[1]{\dot{#1}} -%\newcommand{\chain}[1]{\dot{#1}} -\newcommand{\sVK}{k_{\pu}} -\newcommand{\sVKI}[1]{k_{#1,\pu}} -\newcommand{\sVKII}[1]{\initial{k}_{#1,\pu}} -\newcommand{\sSK}{k_{\pr}} -\newcommand{\sSKI}[1]{k_{#1,\pr}} -\newcommand{\sSKII}[1]{\initial{k}_{#1,\pr}} - -% === State Machines === - -\newcommand{\cemS}{S_{\textsc{cem}}} -\newcommand{\cemI}{I_{\textsc{cem}}} -\newcommand{\cemIn}{i_{\textsc{cem}}} -\newcommand{\cemOut}{o_{\textsc{cem}}} -\newcommand{\cemValidator}{\nu_{\textsc{cem}}} -\newcommand{\cemDatum}{\datum_{\textsc{cem}}} -\newcommand{\cemRedeemer}{\redeemer_{\textsc{cem}}} -\newcommand{\cemFinal}{\mathit{final}_{\textsc{cem}}} -\newcommand{\cemStep}{\mathit{step}_{\textsc{cem}}} -\newcommand{\cemStepRel}[4]{{#1}\overset{#2}\longrightarrow(#3, #4)} -\newcommand{\cemTxCon}{\tx^\equiv} - -\newcommand{\cid}{\mathsf{cid}} % head id / currency id -\newcommand{\did}{\mathsf{did}} % deposit id - -\newcommand{\st}{\mathsf{ST}} -\newcommand{\pt}{\mathsf{PT}} -\newcommand{\dt}{\mathsf{DT}} - -% == Transactions == - -\newcommand{\mtxInit}{\textit{init}} -\newcommand{\mtxCom}{\textit{commit}} -\newcommand{\mtxCommit}{\textit{commit}} -\newcommand{\mtxCCom}{\textit{collectCom}} -\newcommand{\mtxCollect}{\textit{collectCom}} -\newcommand{\mtxDeposit}{\textit{deposit}} -\newcommand{\mtxRecover}{\textit{recover}} -\newcommand{\mtxIncrement}{\textit{increment}} -\newcommand{\mtxDecrement}{\textit{decrement}} -\newcommand{\mtxAbort}{\textit{abort}} -\newcommand{\mtxClose}{\textit{close}} -\newcommand{\mtxContest}{\textit{contest}} -\newcommand{\mtxFinalize}{\textit{finalize}} -\newcommand{\mtxFanout}{\textit{fanout}} -\newcommand{\mtxSplit}{\textit{split}} -\newcommand{\mtxCSN}{\textit{collectSN}} -\newcommand{\mtxCHT}{\textit{collectHT}} -\newcommand{\mtxSN}{\textit{SN}} -\newcommand{\mtxHT}{\textit{HT}} - -% == States == - -\newcommand{\stInitial}{\mathsf{initial}} -\newcommand{\stOpen}{\mathsf{open}} -\newcommand{\stClosed}{\mathsf{closed}} -\newcommand{\stSnap}{\mathsf{newestSN}} -\newcommand{\stFinal}{\mathsf{final}} - -\newcommand{\seed}{\txOutRef_{\mathsf{seed}}} -\newcommand{\hMT}{h_{\mathsf{MT}}} -\newcommand{\piMT}{\pi_{\mathsf{MT}}} -\newcommand{\contesters}{\mathcal{C}} - - -% == Inputs == - -\newcommand{\stCollect}{\mathsf{collect}} -\newcommand{\stClose}{\mathsf{close}} -\newcommand{\stContest}{\mathsf{contest}} -\newcommand{\stFanout}{\mathsf{fanout}} -\newcommand{\stAbort}{\mathsf{abort}} - - -% == Validators,values,datums,redeemers == - -\newcommand{\muHead}{\mu_\mathsf{head}} -\newcommand{\nuHead}{\nu_\mathsf{head}} -\newcommand{\valHead}{\val_{\mathsf{head}}} -\newcommand{\datumHead}{\datum_{\mathsf{head}}} -\newcommand{\redeemerHead}{\redeemer_{\mathsf{head}}} - -\newcommand{\nuInitial}{\nu_{\mathsf{initial}}} -\newcommand{\valInitial}[1]{\val_{\mathsf{initial}_{#1}}} -\newcommand{\datumInitial}[1]{\datum_{\mathsf{initial}_{#1}}} -\newcommand{\redeemerInitial}[1]{\redeemer_{\mathsf{initial}_{#1}}} - -\newcommand{\nuCommit}{\nu_{\mathsf{commit}}} -\newcommand{\valCommit}[1]{\val_{\mathsf{commit}_{#1}}} -\newcommand{\datumCommit}[1]{\datum_{\mathsf{commit}_{#1}}} -\newcommand{\redeemerCommit}[1]{\redeemer_{\mathsf{commit}_{#1}}} - -\newcommand{\nuDeposit}{\nu_\mathsf{deposit}} -\newcommand{\valDeposit}{\val_{\mathsf{deposit}}} -\newcommand{\datumDeposit}{\datum_{\mathsf{deposit}}} -\newcommand{\redeemerDeposit}{\redeemer_{\mathsf{deposit}}} - -\newcommand{\nuSnap}{\nu_\mathsf{SN}} -\newcommand{\nuNewname}{\nu_\mathsf{newestSN}} -\newcommand{\nuHang}{\nu_\mathsf{HT}} -\newcommand{\nuFinal}{\nu_\mathsf{final}} - - -% === Head Protocol === - -% == Algorithms == - -\newcommand{\HP}{\mathsf{HP}} -\newcommand{\hpSetup}{\mathsf{Setup}} -\newcommand{\hpKG}{\mathsf{KeyGen}} -\newcommand{\hpAgg}{\mathsf{Agg}} -\newcommand{\hpProt}{\mathsf{Prot}} - - -% == Protocol == - -\newcommand{\hpInit}{\mathtt{init}} -\newcommand{\hpNew}{\mathtt{newTx}} -\newcommand{\hpSeen}{\mathtt{seen}} -\newcommand{\hpConf}{\mathtt{conf}} -\newcommand{\hpSnap}{\mathtt{snap}} -\newcommand{\hpClose}{\mathtt{close}} -\newcommand{\hpCont}{\mathtt{cont}} -\newcommand{\hpFO}{\mathtt{fanOut}} -\newcommand{\hpRD}{\mathtt{reqDec}} - - -% == Variables == -\newcommand{\pu}{\mathsf{ver}} -\newcommand{\pr}{\mathsf{sig}} - - -\newcommand{\hpParams}{\Sigma} -\newcommand{\hpPu}{K_{\pu}} -\newcommand{\hpPuv}{\underline{K}_\pu} -\newcommand{\hpPui}[1]{K_{\pu,#1}} -\newcommand{\hpPr}{K_{\pr}} -\newcommand{\hpPri}[1]{K_{\pr,#1}} - -\newcommand{\hydraKey}{k_{\mathsf{H}}} % Single hydra verification key -\newcommand{\hydraKeys}{\underline{k}_{\mathsf{H}}} % List of hydra keys -\newcommand{\hydraKeysAgg}{\tilde{k}_{\mathsf{H}}} % Aggregated hydra key -\newcommand{\hydraSigningKey}{\msSK_\mathsf{H}} -\newcommand{\cardanoKey}{k_\mathsf{C}} % Single cardano verification keys -\newcommand{\cardanoKeys}{\underline{k}_\mathsf{C}} % List of cardano keys -\newcommand{\cardanoSigningKey}{\msSK_\mathsf{C}} -\newcommand{\keyHash}{k^{\#}} % Some verification key hash - -\newcommand{\hpPuvInit}{\initial{\underline{K}}_\pu} - -\newcommand{\hydraKeysAggchain}{\hydraKeysAgg^{\mathsf{chain}}} -\newcommand{\hydraKeysAgginit}{\hydraKeysAgg^{\mathsf{setup}}} - -%\newcommand{\initial}{\mathsf{init}} -\newcommand{\daPuII}[1]{\initial{K}_{#1,\pu}} -\newcommand{\daPrII}[1]{\initial{K}_{#1,\pr}} -%\newcommand{\sVKI}{\mathsf{vk}^{\initial}} -%\newcommand{\sSKI}{\mathsf{sk}^{\initial}} - -\newcommand{\cardanoKeysinit}{\initial{\underline{k}}_\pu} - - -\newcommand{\hatv}{\hat v} -\newcommand{\barv}{\bar v} -\newcommand{\hats}{\hat s} -\newcommand{\bars}{\bar s} -\newcommand{\barsigma}{\bar{\sigma}} -\newcommand{\hatSigma}{\hat{\Sigma}} -\newcommand{\hatmU}{\hat {\mathcal U}} -\newcommand{\barmU}{\bar {\mathcal U}} -\newcommand{\mL}{{\mathcal L}} -\newcommand{\hatmL}{\hat {\mathcal L}} -\newcommand{\barmL}{\bar {\mathcal L}} -\newcommand{\mT}{{\mathcal T}} -\newcommand{\hatmT}{\hat {\mathcal T}} -\newcommand{\hatmDT}{\Delta\hat {\mathcal T}} -\newcommand{\hatmR}{\hat {\mathcal R}} -\newcommand{\mH}{{\mathcal H}} - -\newcommand{\TR}{T_{\mathsf R}} -\newcommand{\tTR}{\tilde T_{\mathsf R}} -\newcommand{\tR}{\tilde R} - -\newcommand{\hpSigs}{S} - -\newcommand{\txo}{\mathsf{tx}} - -% == Commands == - -\newcommand{\hpRG}{\mathtt{req}} -\newcommand{\hpAG}{\mathtt{ack}} -\newcommand{\hpCG}{\mathtt{conf}} - -\newcommand{\hpRT}{\mathtt{reqTx}} -\newcommand{\hpAT}{\mathtt{ackTx}} -\newcommand{\hpCT}{\mathtt{confTx}} - -\newcommand{\hpNS}{\mathtt{newSn}} -\newcommand{\hpRS}{\mathtt{reqSn}} -\newcommand{\hpRI}{\mathtt{reqInc}} -\newcommand{\hpAS}{\mathtt{ackSn}} -\newcommand{\hpCS}{\mathtt{confSn}} - - -% == Functions == - -\newcommand{\hash}{\mathsf{hash}} -\newcommand{\bytes}{\mathsf{bytes}} -\newcommand{\concat}{\mathsf{concat}} -\newcommand{\sortOn}{\mathsf{sortOn}} -\newcommand{\combine}{\mathsf{combine}} - -\newcommand{\Txo}{\mathsf{txObj}} -\newcommand{\Sno}{\mathsf{snObj}} -\newcommand{\ApplyMax}{\mathsf{uApplyMax}} - -\newcommand{\hpLdr}{\mathsf{leader}} -\newcommand{\hpMT}{\mathsf{maxTxos}} - -\newcommand{\conf}{\mathsf{conflict}} -\newcommand{\confTx}{\mathsf{conflict\md{}tx}} - - -% == Projectors == - -\newcommand{\hpProj}{_{\downarrow (\tx,\msCSig)}} -\newcommand{\hpProjT}{_{\downarrow (\tx)}} -\newcommand{\hpProjH}{_{\downarrow (\hash)}} -\newcommand{\hpProjSig}{_{\downarrow (\msCSig)}} -\newcommand{\hpProjHs}{_{\downarrow (\hash,\msCSig)}} -\newcommand{\hpProjSo}{_{\downarrow (s,\outputset)}} -\newcommand{\hpProjSos}{_{\downarrow (s,\outputset,\msCSig)}} - -\renewcommand{\hpProj}{^{\downarrow (\tx,\msCSig)}} -\renewcommand{\hpProjT}{^{\downarrow (\tx)}} -\renewcommand{\hpProjH}{^{\downarrow (\hash)}} -\renewcommand{\hpProjSig}{^{\downarrow (\msCSig)}} -\renewcommand{\hpProjHs}{^{\downarrow (\hash,\msCSig)}} -\renewcommand{\hpProjSo}{^{\downarrow (s,\outputset)}} -\renewcommand{\hpProjSos}{^{\downarrow (s,\outputset,\msCSig)}} - - -% == Security == - -\newcommand{\Ttilde}{\tilde{T}} -\newcommand{\That}{\hat{T}} -\newcommand{\Tbar}{\bar{T}} -\renewcommand{\Ttilde}{\tilde{S}} -\renewcommand{\That}{\hat{S}} -\renewcommand{\Tbar}{\bar{C}} -\newcommand{\Snapbar}{\bar{\Sigma}} - -\newcommand{\TxNewAll}{{\cal N}} - -\newcommand{\Hcont}{H_{\mathsf{cont}}} -\newcommand{\honest}{\mathcal H} -\newcommand{\contSet}{\mathcal C} -\newcommand{\Cchain}{C_{\mathsf{chain}}} -\newcommand{\USN}[1]{\mathrm{SN}_{#1}} -\newcommand{\setSN}[1]{\tilde T_{#1}} -\newcommand{\curSN}[1]{\mathrm{SN}_{\mathsf{cur},#1}} - -\newcommand{\INV}[1]{\mathsf{INV}_{#1}} - -\newcommand{\atti}[1]{^{(#1)}} - -% === Mediator Protocol === -\newcommand{\gcClientNewHead}{\mathtt{clientNewHead}} -\newcommand{\gcClientTx}{\mathtt{clientTx}} -\newcommand{\gcClientClose}{\mathtt{closeTx}} -\newcommand{\gcChainInitial}{\mathtt{initialTx}} -\newcommand{\gcChainCollectCom}{\mathtt{collectComTx}} -\newcommand{\gcChainClose}{\mathtt{closeTx}} -\newcommand{\gcChainContest}{\mathtt{contestTx}} -\newcommand{\gcChainFanout}{\mathtt{fanoutTx}} -\newcommand{\gcChainAbort}{\mathtt{abortTx}} -\newcommand{\gcChainCommit}{\mathtt{commitTx}} -\newcommand{\gcChainInitialTO}{\mathtt{chainInitialTimeOut}} -\newcommand{\gcChainClosedTO}{\mathtt{chainClosedTimeOut}} - -\newcommand{\gcChainRef}{\mathsf{chain}} -\newcommand{\gcClientRef}{\mathsf{client}} -\newcommand{\gcHeadRef}{\mathsf{head}} -\newcommand{\gcChainPost}{\mathsf{postTx}} -\newcommand{\gcUTXOset}{\mathsf{UTxOs}} -\SetKw{Call}{call} - - -% === On-Chain Verification === - -% == Algorithms and Oracles == - -\newcommand{\ocvInitial}{\mathsf{Initial}} -\newcommand{\ocvFinalize}{\mathsf{Finalize}} -\newcommand{\ocvClose}{\mathsf{Close}} -\newcommand{\ocvContest}{\mathsf{Contest}} -\newcommand{\ocvFinal}{\mathsf{Final}} - -\newcommand{\ocvIncrement}{\mathsf{Increment}} -\newcommand{\ocvDecrement}{\mathsf{Decrement}} - -\newcommand{\ocvSnapshot}{\mathsf{Snapshot}} -\newcommand{\ocvValidSnap}{\mathsf{ValidSN}} -\newcommand{\ocvValidHang}{\mathsf{ValidHT}} - -\newcommand{\ocvClaim}{\mathsf{Claim}} -\newcommand{\ocvAllocate}{\mathsf{Allocate}} -\newcommand{\ocvFanout}{\mathsf{Fanout}} - -\SetKwFor{OocvInitial}{$\ocvInitial$}{}{enddo} -\SetKwFor{OocvFinalize}{$\ocvFinalize$}{}{enddo} -\SetKwFor{OocvClose}{$\ocvClose$}{}{enddo} -\SetKwFor{OocvContest}{$\ocvContest$}{}{enddo} -\SetKwFor{OocvFinal}{$\ocvFinal$}{}{enddo} - -\SetKwFor{OocvClaim}{$\ocvClaim$}{}{enddo} -\SetKwFor{OocvAllocate}{$\ocvAllocate$}{}{enddo} -\SetKwFor{OocvFanout}{$\ocvFanout$}{}{enddo} - - -% == Variables == - -\newcommand{\hInit}{\hash_{\mathsf{init}}} -\newcommand{\imax}{i_{\mathsf{max}}} -\newcommand{\symFinal}{\mathtt{final}} - - -% == Functions == - -\newcommand{\applicable}{\mathsf{applicable}} - - -% === Algorithms === - -% == Misc == - -% \setlength{\algomargin}{0em} - - -% == Boxes == - -\newenvironment{algobox}[1]% -{ - \begin{tabularx}{\textwidth}{X c X} - \hline - \rowcolor{gray!20} - & \textbf{#1} & \\ - \hline - \end{tabularx} - - \vspace{-1.5em} - - \begin{center} - } - { - \end{center} - - \vspace{-1.5em} - - \begin{tabularx}{\textwidth}{X c X} - \hline - \end{tabularx} - - \vspace{0.5em} -} - -\newenvironment{walgo}[1]% -{ - \begin{minipage}{#1\linewidth} - \begingroup - \begin{algorithm}[H] - } - { - \end{algorithm} - \endgroup - \end{minipage} -} - - -% == Keywords == - -\SetKwFor{Check}{check}{}{enddo} - - -% == DA Game == - -%\newcommand{\algoskip}{\vspace{2pt}} - -\SetKwIF{If}{ElseIf}{Else}{if}{}{else if}{else}{end if} -\SetKwFor{For}{for}{}{end for} - -\SetKwFor{On}{on}{}{enddo} -\SetKwFor{Function}{function}{}{enddo} -\SetKwFor{PFunction}{public function}{}{enddo} -\SetKw{Out}{output} -\SetKw{Req}{require} -\SetKwFor{ForA}{for all}{}{enddo} -\SetKwFor{While}{while}{}{enddo} -\SetKwFor{Wait}{wait}{}{enddo} -\SetKw{KwWait}{wait} % without body -\SetKw{IfI}{if} -\SetKw{ThenI}{then} -\SetKw{ElsI}{else} -\SetKw{FiI}{fi} - -\newcommand{\daPID}{\mathsf{ID}} - -\newcommand{\daGlobal}{\Sigma} -\newcommand{\daPu}{K_{\pu}} -\newcommand{\daPuV}{\bar K_{\pu}} -\newcommand{\daPuI}[1]{K_{#1,\pu}} -\newcommand{\daPr}{K_{\pr}} -\newcommand{\daPrI}[1]{K_{#1,\pr}} - -\newcommand{\daCInit}{\mathtt{init}} -\newcommand{\daCNew}{\mathtt{new}} -\newcommand{\daCSeen}{\mathtt{seen}} -\newcommand{\daCConf}{\mathtt{conf}} -\newcommand{\daCCert}{\mathtt{cert}} -\newcommand{\daCComp}{\mathtt{comp}} - -\SetKw{New}{new} -\SetKw{KwOn}{on} -\SetKw{Send}{send} -\SetKw{Multi}{multicast} -\SetKw{PostTx}{postTx} -\newcommand{\Store}{\mathsf{store}} -\newcommand{\Sign}{\mathsf{sign}} -\newcommand{\Combine}{\mathsf{sigCombine}} -\newcommand{\Verify}{\mathsf{SigVerify}} -\newcommand{\Complete}{\mathsf{Complete}} - -\newcommand{\hyPu}{\msCVK} -\newcommand{\hyPr}{\msSK} - - -% === Merkle-Patricia Trees === - -% == Misc == - -\newcommand{\MPTalph}{A} - -% == Algorithms == - -\newcommand{\MPTInit}{\mathsf{MPT\md{}Init}} -\newcommand{\MPTHash}{\mathsf{MPT\md{}Hash}} -\newcommand{\MPTMemb}{\mathsf{MPT\md{}Memb}} - -\newcommand{\MPTBuild}{\mathsf{MPT\md{}Build}} -\newcommand{\MPTPath}{\mathsf{MPT\md{}Path}} - - -% == Hash Computations == - -\newcommand{\MPTverMemb}{\mathsf{MPT\md{}VfyMemb}} -\newcommand{\MPTcompRA}{\mathsf{MPT\md{}CompRA}} -\newcommand{\MPTcompSpl}{\mathsf{MPT\md{}CompSpl}} - - -% == Helpers == - -\newcommand{\CP}{\mathsf{CP}} -\newcommand{\RP}{\mathsf{RP}} -\newcommand{\Proj}{\mathsf{Proj}} -\newcommand{\Sum}{\mathsf{Sum}} -\newcommand{\Size}{\mathsf{Size}} - - -% == Oracles == - -\SetKwFor{MPTAInit}{\sf MPT-Init}{}{enddo} - -\SetKwBlock{MPTAHash}{\sf MPT-Hash}{enddo} -\SetKwFor{MPTAMemb}{\sf MPT-Memb}{}{enddo} - -\SetKwFor{MPTABuild}{\sf MPT-Build}{}{enddo} -\SetKwFor{MPTAPath}{\sf MPT-Path}{}{enddo} - - -% == Variables == - -\newcommand{\MPTroot}{h_{\mathsf{root}}} -\newcommand{\MPTnodes}{N} -\newcommand{\MPTpre}{\mathsf{pre}} -\newcommand{\MPTnode}{\mathsf{node}} -\newcommand{\MPTleaf}{\mathsf{leaf}} -\newcommand{\MPTkey}{k} -\newcommand{\MPTvalue}{v} -\newcommand{\MPTaux}{\mathsf{aux}} -\newcommand{\MPTsplit}{\mathsf{split}} - - - - -% == MF == -\newcommand{\mf}[1]{{\color{red} {#1}}} -% \newcommand{\mfold}[1]{{\color{red}\sout{#1}}} -% \newcommand{\mfreplace}[2]{{\color{red}\sout{#1} {#2}}} -\newcommand{\symdif}{\stackrel{\cdot}{\cup}} -\newcommand{\defeq}{\stackrel{\triangle}{=}} -\newcommand{\sigmaterial}{\Phi} - -\newcommand{\dparagraph}[1]{\smallskip\noindent\textbf{#1}} - -\newcommand{\pvspace}{\vspace{8pt}} - - - -% == Affiliations == - -\newcommand*\sameaffil[1][\value{footnote}]{\footnotemark[#1]} - - -% == Narrow Itemize == -\newenvironment{sitemize}[1] % -{\itemize\setlength\itemsep{0em}} % -{\enditemize} - -\newenvironment{senumerate} % -{\enumerate\setlength\itemsep{0em}} % -{\endenumerate} - -\newenvironment{sdescription} % -{\description\setlength\itemsep{0em}} % -{\enddescription} - -\newenvironment{mitemize} % -{\itemize\setlength\itemsep{0.25em}} % -{\enditemize} - -\newenvironment{menumerate} % -{\enumerate\setlength\itemsep{0.25em}} % -{\endenumerate} - -\newenvironment{mdescription} % -{\description\setlength\itemsep{0.25em}} % -{\enddescription} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: diff --git a/src/preamble.tex b/src/preamble.tex deleted file mode 100644 index 700140d..0000000 --- a/src/preamble.tex +++ /dev/null @@ -1,71 +0,0 @@ -% Common packages and settings -% Many things here are from the original hydra paper or from the formal-ledger-specifications - -\usepackage{amsfonts,amsmath,amssymb,amsthm} -\usepackage[normalem]{ulem} % temporary for strikeout math -\usepackage{enumerate} -\usepackage[shortlabels,inline]{enumitem} -\usepackage{wrapfig} - -\usepackage[lined,noend]{algorithm2e} -\usepackage{tabularx} -\usepackage{colortbl} -\usepackage{adjustbox} -\DontPrintSemicolon - -\PassOptionsToPackage{hyphens}{url} -\usepackage{fullpage} -\usepackage{hyperref} -\usepackage{xcolor} -\usepackage{xifthen} -% Keep figures in same section -\usepackage[section]{placeins} -\usepackage{pifont} -\usepackage{multirow} -\usepackage{tikz} -\usetikzlibrary{automata, arrows} -\usepackage{pgfplots} -\usepackage[framemethod=tikz]{mdframed} % and thus tikz -\usepackage[font=small]{caption} -\usepackage[many]{tcolorbox} % for COLORED BOXES - -\usepackage{authblk} - -% footnotes in table and tabular -\usepackage{footnote} -\makesavenoteenv{tabular} -\makesavenoteenv{table} -\makesavenoteenv{figure} - -\usepackage{stmaryrd} % fancy double square brackets -\usepackage{todonotes} - -\setcounter{tocdepth}{2} % Override LLNCS - -% Highlighted agda code -\usepackage[links]{agda} - -% Use a font that works well with agda -% NOTE: Vendored from formal-ledger-specifications -\usepackage{fontspec} -\newcommand\agdaFont{StrippedJuliaMono} -\newcommand\agdaFontOptions{ -Path=fonts/, -Extension=.ttf, -UprightFont=*-Regular, -BoldFont=*-Bold, -ItalicFont=*-RegularItalic, -BoldItalicFont=*-BoldItalic, -Scale=0.80 -} -\newfontfamily{\AgdaSerifFont}{\agdaFont}[\agdaFontOptions] -\newfontfamily{\AgdaSansSerifFont}{\agdaFont}[\agdaFontOptions] -\newfontfamily{\AgdaTypewriterFont}{\agdaFont}[\agdaFontOptions] -\renewcommand{\AgdaFontStyle}[1]{{\AgdaSansSerifFont{}#1}} -\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaSansSerifFont{}#1}} -\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}} -\renewcommand{\AgdaCommentFontStyle}[1]{{\AgdaTypewriterFont{}#1}} -\renewcommand{\AgdaBoundFontStyle}[1]{{\emph{\AgdaTypewriterFont{}#1}}} - -% Also use unicode compatible math fonts -\usepackage{unicode-math} diff --git a/src/short.bib b/src/short.bib index 495628a..cd24894 100644 --- a/src/short.bib +++ b/src/short.bib @@ -4,19 +4,6 @@ %% %------------------------------------------------------------------------------- -@InProceedings{CCS:MicOhtRey01, - author = "Silvio Micali and Kazuo Ohta and Leonid Reyzin", - title = "Accountable-Subgroup Multisignatures: Extended Abstract", - pages = "245--254", - editor = ccs01ed, - booktitle = ccs01name, - address = ccs01addr, - month = ccs01month, - publisher = ccspub, - year = 2001, - doi = "10.1145/501983.502017", -} - @article{Zahnentferner18-UTxO, Author = {Joachim Zahnentferner}, Bibsource = {dblp computer science bibliography, https://dblp.org},