Plain tex (#6)

* Rearrange, rename library to hydra-protocol

* Allow plain tex files

* Initial import of overview section

README.md

@@ -1,3 +1,9 @@
 # hydra-formal-specification
 
 Agda specification for the hydra-protocol.
+
+## Building
+
+```
+nix build
+```

flake.nix

@@ -19,45 +19,70 @@
       ];
       perSystem = { pkgs, ... }:
         let
-          agdaPackages = pkgs.callPackage ./initial-packages.nix { Agda = pkgs.haskellPackages.Agda; nixpkgs = inputs.nixpkgs; };
+          agdaPackages = pkgs.callPackage ./nix/initial-packages.nix { Agda = pkgs.haskellPackages.Agda; nixpkgs = inputs.nixpkgs; };
+          buildInputs = with agdaPackages;
+            [
+              formal-ledger
+              standard-library
+              standard-library-classes
+              standard-library-meta
+            ];
         in
         rec {
           packages = {
-            hydra-agda-spec = agdaPackages.mkDerivation {
-              pname = "hydra-formal-specification";
+            hydra-protocol-typecheck = agdaPackages.mkDerivation {
+              pname = "hydra-protocol-typecheck";
               version = "0.0.1";
-              src = ./.;
-              buildInputs = with agdaPackages; [ standard-library standard-library-classes standard-library-meta formal-ledger ];
+              src = ./hydra-protocol;
+              inherit buildInputs;
+              meta = { };
+              buildPhase = ''
+                agda Hydra/Protocol/Main.lagda
+              '';
+              installPhase = ''
+                mkdir $out
+                echo "Success" > $out/result
+              '';
+            };
+
+            hydra-protocol-transliterate = agdaPackages.mkDerivation {
+              pname = "hydra-protocol-transliterate";
+              version = "0.0.1";
+              src = ./hydra-protocol;
+              inherit buildInputs;
               meta = { };
               buildPhase = ''
                 mkdir latex
                 cp ${inputs.formal-ledger}/src/latex/* latex/ -r
-                agda --latex --latex-dir latex Hydra/Protocol/Main.lagda
                 find . -name '*.lagda' | xargs -I{} agda --transliterate --latex --latex-dir latex {}
+                find . -name '*.tex' | xargs -I{} ${pkgs.rsync}/bin/rsync -rR {} latex/
               '';
               installPhase = ''
                 mkdir $out
                 cp -r latex/* $out/
               '';
             };
 
-            default = pkgs.stdenv.mkDerivation {
-              pname = "hydra-formal-specification";
+            hydra-protocol-pdf = pkgs.stdenv.mkDerivation {
+              pname = "hydra-protocol.pdf";
               version = "0.0.1";
-              src = ./.;
               nativeBuildInputs = with pkgs; [
                 texlive.combined.scheme-full
+                packages.hydra-protocol-transliterate 
               ];
-              buildInputs = [ packages.hydra-agda-spec ];
+              src = ./.;
               buildPhase = ''
-                cp ${packages.hydra-agda-spec}/* -r .
+                cp ${packages.hydra-protocol-transliterate}/* -r .
                 HOME=./. latexmk -xelatex Hydra/Protocol/Main.tex
               '';
               installPhase = ''
                 mkdir $out
                 cp Main.pdf $out/hydra-protocol.pdf
               '';
             };
+
+            default = packages.hydra-protocol-pdf;
+
           };
         };
     };

hydra-protocol/Hydra/Protocol/Figures/SM_States_Basic.tex

@@ -0,0 +1,25 @@
+\begin{figure}[t!]
+  \centering
+  \begin{tikzpicture}[>=stealth,auto,node distance=2.8cm, initial text=$\mathsf{init}$, every
+    state/.style={text width=10mm, text height=2mm, align=center}]
+    \node[state, initial] (initial) {$\stInitial$};
+    \node[state] (open) [above right of=initial] {$\stOpen$};
+    \node[state] (closed) [right of=open] {$\stClosed$};
+    \node[state] (final) [below right of=closed] {$\stFinal$};
+
+    \path[->] (initial) edge [bend left=20] node {$\stCollect$} (open);
+    \path[->] (open) edge [bend left=20] node {$\stClose$} (closed);
+    \path[->] (open) edge [loop above] node {$\mathsf{increment}$} (open);
+    \path[->] (open) edge [loop below] node {$\mathsf{decrement}$} (open);
+    \path[->] (closed) edge [bend left=20] node {$\stFanout$} (final);
+    \path[->] (closed) edge [loop above] node {$\stContest$} (closed);
+    \path[->] (initial) edge [bend right=20] node {$\stAbort$} (final);
+  \end{tikzpicture}
+
+  \caption{Mainchain state diagram for this version of the Hydra protocol.}\label{fig:SM_states_basic}
+\end{figure}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End:

Hydra/Protocol/Introduction.lagda → hydra-protocol/Hydra/Protocol/Introduction.tex

@@ -24,7 +24,3 @@ \chapter{Introduction}
 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.
-
-\begin{code}[hide]
-module Hydra.Protocol.Introduction where
-\end{code}

hydra-protocol/Hydra/Protocol/Macros.tex

@@ -0,0 +1,81 @@
+% ==== Hydra Macros ====
+
+% NOTE: New macro file; please copy and keep organized macros from
+% macros_old.tex as needed.  Hopefully, this will result in tidier
+% macros file.
+%
+% Index:
+% - Misc
+% - General
+% - Theorem Environments
+% - Multisignatures
+% - Transactions
+% - State Machines
+% - Head Protocol
+% - On-Chain Verification
+% - Algorithms
+% - Merkle-Patricia Trees
+
+% === engineering ===
+
+\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{\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}}
+
+
+\newcommand{\mtxInit}{\textit{init}}
+\newcommand{\mtxCom}{\textit{commit}}
+\newcommand{\mtxCommit}{\textit{commit}}
+\newcommand{\mtxCCom}{\textit{collectCom}}
+\newcommand{\mtxCollect}{\textit{collectCom}}
+\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}}
+
+\newcommand{\Tset}{T}
+\newcommand{\Uset}{U}
+\newcommand{\Uinit}{\Uset_{0}}
+\newcommand{\Ufinal}{\Uset_{\mathsf{final}}}

Hydra/Protocol/Main.lagda → hydra-protocol/Hydra/Protocol/Main.lagda

@@ -3,8 +3,35 @@
 \usepackage{etoolbox}
 \usepackage{lipsum}
 \usepackage{todonotes}
+\usepackage{polytable}
+
+\usepackage[many]{tcolorbox}
+\usepackage{amsfonts,amsmath,amssymb,amsthm}
+\usepackage[normalem]{ulem} % temporary for strikeout math
+\usepackage{environ}
+\usepackage{enumerate}
+\usepackage[shortlabels,inline]{enumitem}
+\usepackage{wrapfig}
+\usepackage[lined,noend]{algorithm2e}
+\usepackage{tabularx}
+\usepackage{colortbl}
+\usepackage{adjustbox}
+\usepackage{fullpage}
+\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
 
 \include{preamble}
+\include{Hydra/Protocol/Macros}
 
 \setcounter{secnumdepth}{5}
 \setcounter{tocdepth}{1}
@@ -21,6 +48,7 @@
 \titleformat{\chapter}[block]
   {\normalfont\huge\bfseries}{}{0pt}{\hspace*{-\titleindent}}
 
+
 \titleformat{\section}
   {\normalfont\Large\bfseries}{\llap{\parbox{\titleindent}{\thesection\hfill}}}{0em}{}
 
@@ -64,11 +92,11 @@ Date: \today
 \begin{code}[hide]
 module Hydra.Protocol.Main where
 
-open import Hydra.Protocol.Introduction
 open import Hydra.Protocol.Throwaway
 \end{code}
 
 \input{Hydra/Protocol/Introduction}
+\input{Hydra/Protocol/Overview}
 \input{Hydra/Protocol/Throwaway}
 
 \end{document}

hydra-protocol/Hydra/Protocol/Overview.tex

@@ -0,0 +1,121 @@
+\chapter{Protocol Overview}\label{sec:overview}
+
+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,
+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
+(inside a head) and no responsive honest party involved in a head can ever lose
+any funds other than by consenting to give them away. In exchange for decreased
+liveness guarantees (stop any time), it can essentially proceed at network speed
+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".
+
+\subsection{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
+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}
+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:SM_states_basic}) 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}.
+
+\input{Hydra/Protocol/Figures/SM_States_Basic}
+
+Once the initial transaction appears on the mainchain, establishing the initial
+state $\stInitial$, each head member can attach a \mtxCom{} 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
+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$ \todo{increment / decrement}.
+
+
+\subsection{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.
+
+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
+set of UTxOs evolved from the initial UTxO set by applying transactions as they
+are received from the other parties.
+
+To confirm transactions and allow for an on-chain decommit 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
+monotonically increasing snapshot numbers.
+
+For this, the next snapshot leader (round-robin) requests his view of a new confirmed state to be
+signed by all participants as a new snapshot. The leader does not need to send his local state,
+but only indicate, by hashes, the set of transactions to be included in order to
+obtain the to-be-snapshotted UTxO set.
+
+The other participants sign the snapshot as soon as they have (also) seen the
+transactions that are to be processed on top of its preceding snapshot: a
+party's local state is always ahead of the latest confirmed snapshot.
+
+Signatures are broadcast and aggregated by each party. When all signature parts
+of the multi-signature are received and verified, a snapshot is considered
+confirmed. As a consequence, a participant can safely delete (if wished) all
+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.
+
+\subsection{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 snapshot, specifically from its snapshot
+number and the respective multisignature. Using this 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,
+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. The state machine enforces that the outputs of
+the transaction leading to $\stFinal$ correspond exactly to the latest UTxO set
+seen during the contestation period.
+
+\subsection{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).
+    \todo{increment / decrement extension}
+\end{itemize}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End:

hydra-formal-specification.agda-lib → hydra-protocol/hydra-protocol.agda-lib

@@ -1,4 +1,4 @@
-name: hydra-formal-specification
+name: hydra-protocol
 depend:
   formal-ledger
   standard-library