diff --git a/.github/workflows/ci-nix.yaml b/.github/workflows/ci-nix.yaml index a2b51ca3762..499a2e4aa00 100644 --- a/.github/workflows/ci-nix.yaml +++ b/.github/workflows/ci-nix.yaml @@ -276,14 +276,14 @@ jobs: - name: ❄ Build specification PDF run: | - nix build .#spec && cp result/*.pdf . + nix build .#spec && cp result/*.pdf spec/ - name: 💾 Upload specification uses: actions/upload-artifact@v4 with: name: hydra-spec path: | - *.pdf + ./spec/*.pdf documentation: name: Documentation diff --git a/flake.lock b/flake.lock index cfb41b83c51..f02ed5f5a96 100644 --- a/flake.lock +++ b/flake.lock @@ -617,24 +617,6 @@ "inputs": { "nixpkgs-lib": "nixpkgs-lib_2" }, - "locked": { - "lastModified": 1717285511, - "narHash": "sha256-iKzJcpdXih14qYVcZ9QC9XuZYnPc6T8YImb6dX166kw=", - "owner": "hercules-ci", - "repo": "flake-parts", - "rev": "2a55567fcf15b1b1c7ed712a2c6fadaec7412ea8", - "type": "github" - }, - "original": { - "owner": "hercules-ci", - "repo": "flake-parts", - "type": "github" - } - }, - "flake-parts_3": { - "inputs": { - "nixpkgs-lib": "nixpkgs-lib_3" - }, "locked": { "lastModified": 1719994518, "narHash": "sha256-pQMhCCHyQGRzdfAkdJ4cIWiw+JNuWsTX7f0ZYSyz0VY=", @@ -742,22 +724,6 @@ "type": "github" } }, - "formal-ledger": { - "flake": false, - "locked": { - "lastModified": 1718812337, - "narHash": "sha256-3zAxfOEs/Ff5g13493iZGGhcvYaSOJNkQLN/G3/AhiY=", - "owner": "IntersectMBO", - "repo": "formal-ledger-specifications", - "rev": "6129d97a0419f8d920e3ed63e192f34cbaf65cc6", - "type": "github" - }, - "original": { - "owner": "IntersectMBO", - "repo": "formal-ledger-specifications", - "type": "github" - } - }, "ghc-8.6.5-iohk": { "flake": false, "locked": { @@ -1406,26 +1372,6 @@ "type": "indirect" } }, - "hydra-spec": { - "inputs": { - "flake-parts": "flake-parts_2", - "formal-ledger": "formal-ledger", - "nixpkgs": "nixpkgs_9" - }, - "locked": { - "lastModified": 1722417654, - "narHash": "sha256-PY37f8ecHsHK0dOKZHu7PjEFAt6IW/n/vMyHmXhFibQ=", - "owner": "cardano-scaling", - "repo": "hydra-formal-specification", - "rev": "035baae43c438cb37dc3cb20654ee0b740141a6e", - "type": "github" - }, - "original": { - "owner": "cardano-scaling", - "repo": "hydra-formal-specification", - "type": "github" - } - }, "hydra_2": { "inputs": { "nix": "nix_2", @@ -1474,7 +1420,7 @@ "iohk-nix": { "inputs": { "blst": "blst_2", - "nixpkgs": "nixpkgs_10", + "nixpkgs": "nixpkgs_9", "secp256k1": "secp256k1_2", "sodium": "sodium_2" }, @@ -1638,8 +1584,8 @@ "mithril": { "inputs": { "crane": "crane", - "flake-parts": "flake-parts_3", - "nixpkgs": "nixpkgs_11", + "flake-parts": "flake-parts_2", + "nixpkgs": "nixpkgs_10", "treefmt-nix": "treefmt-nix" }, "locked": { @@ -1743,7 +1689,7 @@ }, "nix-npm-buildpackage": { "inputs": { - "nixpkgs": "nixpkgs_12" + "nixpkgs": "nixpkgs_11" }, "locked": { "lastModified": 1686315622, @@ -2109,18 +2055,6 @@ } }, "nixpkgs-lib_2": { - "locked": { - "lastModified": 1717284937, - "narHash": "sha256-lIbdfCsf8LMFloheeE6N31+BMIeixqyQWbSr2vk79EQ=", - "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz" - }, - "original": { - "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/eb9ceca17df2ea50a250b6b27f7bf6ab0186f198.tar.gz" - } - }, - "nixpkgs-lib_3": { "locked": { "lastModified": 1719876945, "narHash": "sha256-Fm2rDDs86sHy0/1jxTOKB1118Q0O3Uc7EC0iXvXKpbI=", @@ -2213,22 +2147,6 @@ } }, "nixpkgs_10": { - "locked": { - "lastModified": 1684171562, - "narHash": "sha256-BMUWjVWAUdyMWKk0ATMC9H0Bv4qAV/TXwwPUvTiC5IQ=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "55af203d468a6f5032a519cba4f41acf5a74b638", - "type": "github" - }, - "original": { - "owner": "nixos", - "ref": "release-22.11", - "repo": "nixpkgs", - "type": "github" - } - }, - "nixpkgs_11": { "locked": { "lastModified": 1720571246, "narHash": "sha256-nkUXwunTck+hNMt2wZuYRN+jf2ySRjKTzI0fo5TDH78=", @@ -2244,7 +2162,7 @@ "type": "github" } }, - "nixpkgs_12": { + "nixpkgs_11": { "locked": { "lastModified": 1653917367, "narHash": "sha256-04MsJC0g9kE01nBuXThMppZK+yvCZECQnUaZKSU+HJo=", @@ -2368,15 +2286,16 @@ }, "nixpkgs_9": { "locked": { - "lastModified": 1718717814, - "narHash": "sha256-xB7AzKY4BP7yypo6g+sk1tnVK54sBIJMeEBB5CdbhT4=", + "lastModified": 1684171562, + "narHash": "sha256-BMUWjVWAUdyMWKk0ATMC9H0Bv4qAV/TXwwPUvTiC5IQ=", "owner": "nixos", "repo": "nixpkgs", - "rev": "88af533d8ae8d1e7e4648decf7817ebff91abf56", + "rev": "55af203d468a6f5032a519cba4f41acf5a74b638", "type": "github" }, "original": { "owner": "nixos", + "ref": "release-22.11", "repo": "nixpkgs", "type": "github" } @@ -2515,7 +2434,6 @@ "flake-parts": "flake-parts", "haskellNix": "haskellNix_2", "hls": "hls", - "hydra-spec": "hydra-spec", "iohk-nix": "iohk-nix", "lint-utils": "lint-utils", "mithril": "mithril", diff --git a/flake.nix b/flake.nix index 35449b57755..f797d58d92c 100644 --- a/flake.nix +++ b/flake.nix @@ -21,7 +21,6 @@ cardano-node.url = "github:intersectmbo/cardano-node/9.1.0"; mithril.url = "github:input-output-hk/mithril/2428.0"; nix-npm-buildpackage.url = "github:serokell/nix-npm-buildpackage"; - hydra-spec.url = "github:cardano-scaling/hydra-formal-specification"; }; outputs = @@ -131,7 +130,9 @@ packages = hydraPackages // (if pkgs.stdenv.isLinux then (prefixAttrs "docker-" hydraImages) else { }) // { - spec = inputs.hydra-spec.packages.${system}.default; + spec = import ./spec { + inherit pkgs; + }; }; process-compose."demo" = import ./nix/hydra/demo.nix { inherit system pkgs inputs self; diff --git a/spec/.envrc b/spec/.envrc new file mode 100644 index 00000000000..aef781f7d49 --- /dev/null +++ b/spec/.envrc @@ -0,0 +1 @@ +use flake .#spec diff --git a/spec/.gitignore b/spec/.gitignore new file mode 100644 index 00000000000..70d834fd32a --- /dev/null +++ b/spec/.gitignore @@ -0,0 +1,3 @@ +/main.* +!/main.tex +/.auctex-auto/ diff --git a/spec/README.md b/spec/README.md new file mode 100644 index 00000000000..3f0f35ec54d --- /dev/null +++ b/spec/README.md @@ -0,0 +1,27 @@ +# Hydra Specification + +The Hydra Head protocol is specified in the single document built from this +directory. + +We use LaTeX to write the specification and used to compose this on +[overleaf](www.overleaf.com). Going forward, any changes to the specification +should follow the common pull request rules as set out in our [contribution +guidelines](../CONTRIBUTING.md). + +The [Overleaf documentation](https://www.overleaf.com/learn) does provide a good +introduction to LaTeX syntax and functions to get started. + +## Building + +You can use `nix` to build a PDF from the LaTeX files using + +``` shell +nix build .#spec +``` + +which will write the PDF into `result/hydra-spec.pdf`. + +Alternatively, you would need to have a LaTeX distribution installed (e.g. +`texlive`) and produce a PDF output using `pdflatex` etc. The [LaTeX +wikibook](https://en.wikibooks.org/wiki/LaTeX/Basics#Building_a_document) might +be helpful to set things up. diff --git a/spec/acmart.cls b/spec/acmart.cls new file mode 100644 index 00000000000..35fb12ec038 --- /dev/null +++ b/spec/acmart.cls @@ -0,0 +1,2922 @@ +%% +%% This is file `acmart.cls', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% acmart.dtx (with options: `class') +%% +%% IMPORTANT NOTICE: +%% +%% For the copyright see the source file. +%% +%% Any modified versions of this file must be renamed +%% with new filenames distinct from acmart.cls. +%% +%% For distribution of the original source see the terms +%% for copying and modification in the file acmart.dtx. +%% +%% This generated file may be distributed as long as the +%% original source files, as listed above, are part of the +%% same distribution. (The sources need not necessarily be +%% in the same archive or directory.) +%% \CharacterTable +%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +%% Digits \0\1\2\3\4\5\6\7\8\9 +%% Exclamation \! Double quote \" Hash (number) \# +%% Dollar \$ Percent \% Ampersand \& +%% Acute accent \' Left paren \( Right paren \) +%% Asterisk \* Plus \+ Comma \, +%% Minus \- Point \. Solidus \/ +%% Colon \: Semicolon \; Less than \< +%% Equals \= Greater than \> Question mark \? +%% Commercial at \@ Left bracket \[ Backslash \\ +%% Right bracket \] Circumflex \^ Underscore \_ +%% Grave accent \` Left brace \{ Vertical bar \| +%% Right brace \} Tilde \~} +\NeedsTeXFormat{LaTeX2e} +\ProvidesClass{acmart} +[2020/02/22 v1.70 Typesetting articles for the Association for Computing Machinery] +\def\@classname{acmart} +\InputIfFileExists{acmart-preload-hook.tex}{% + \ClassWarning{\@classname}{% + I am loading acmart-preload-hook.tex. You are fully responsible + for any problems from now on.}}{} +\RequirePackage{xkeyval} +\RequirePackage{xstring} +\define@choicekey*+{acmart.cls}{format}[\ACM@format\ACM@format@nr]{% + manuscript, acmsmall, acmlarge, acmtog, sigconf, siggraph, + sigplan, sigchi, sigchi-a}[manuscript]{}{% + \ClassError{\@classname}{The option format must be manuscript, + acmsmall, acmlarge, acmtog, sigconf, siggraph, + sigplan, sigchi or sigchi-a}} +\def\@DeclareACMFormat#1{\DeclareOptionX{#1}{\setkeys{acmart.cls}{format=#1}}} +\@DeclareACMFormat{manuscript} +\@DeclareACMFormat{acmsmall} +\@DeclareACMFormat{acmlarge} +\@DeclareACMFormat{acmtog} +\@DeclareACMFormat{sigconf} +\@DeclareACMFormat{siggraph} +\@DeclareACMFormat{sigplan} +\@DeclareACMFormat{sigchi} +\@DeclareACMFormat{sigchi-a} +\ExecuteOptionsX{format} +\define@boolkey+{acmart.cls}[@ACM@]{screen}[true]{% + \if@ACM@screen + \PackageInfo{\@classname}{Using screen mode}% + \else + \PackageInfo{\@classname}{Not using screen mode}% + \fi}{\PackageError{\@classname}{The option screen can be either true or + false}} +\ExecuteOptionsX{screen=false} +\define@boolkey+{acmart.cls}[@ACM@]{urlbreakonhyphens}[true]{% + \if@ACM@urlbreakonhyphens + \PackageInfo{\@classname}{Using breaking urls on hyphens}% + \else + \PackageInfo{\@classname}{Not breaking urls on hyphens}% + \fi}{\PackageError{\@classname}{The option urlbreakonhyphens can be either true or + false}} +\ExecuteOptionsX{urlbreakonhyphens=true} +\define@boolkey+{acmart.cls}[@ACM@]{acmthm}[true]{% + \if@ACM@acmthm + \PackageInfo{\@classname}{Requiring acmthm}% + \else + \PackageInfo{\@classname}{Suppressing acmthm}% + \fi}{\PackageError{\@classname}{The option acmthm can be either true or + false}} +\ExecuteOptionsX{acmthm=true} +\define@boolkey+{acmart.cls}[@ACM@]{review}[true]{% + \if@ACM@review + \PackageInfo{\@classname}{Using review mode}% + \AtBeginDocument{\@ACM@printfoliostrue}% + \else + \PackageInfo{\@classname}{Not using review mode}% + \fi}{\PackageError{\@classname}{The option review can be either true or + false}} +\ExecuteOptionsX{review=false} +\define@boolkey+{acmart.cls}[@ACM@]{authorversion}[true]{% + \if@ACM@authorversion + \PackageInfo{\@classname}{Using authorversion mode}% + \else + \PackageInfo{\@classname}{Not using authorversion mode}% + \fi}{\PackageError{\@classname}{The option authorversion can be either true or + false}} +\ExecuteOptionsX{authorversion=false} +\define@boolkey+{acmart.cls}[@ACM@]{nonacm}[true]{% + \if@ACM@nonacm + \PackageInfo{\@classname}{Using nonacm mode}% + \AtBeginDocument{\@ACM@printacmreffalse}% + % in 'nonacm' mode we disable the "ACM Reference Format" + % printing by default, but this can be re-enabled by the + % user using \settopmatter{printacmref=true} + \else + \PackageInfo{\@classname}{Not using nonacm mode}% + \fi}{\PackageError{\@classname}{The option nonacm can be either true or + false}} +\ExecuteOptionsX{nonacm=false} +\define@boolkey+{acmart.cls}[@ACM@]{balance}[true]{}{% + \PackageError{\@classname}{The option balance can be either true or + false}} +\ExecuteOptionsX{balance} +\define@boolkey+{acmart.cls}[@ACM@]{natbib}[true]{% + \if@ACM@natbib + \PackageInfo{\@classname}{Explicitly selecting natbib mode}% + \else + \PackageInfo{\@classname}{Explicitly deselecting natbib mode}% + \fi}{\PackageError{\@classname}{The option natbib can be either true or + false}} +\ExecuteOptionsX{natbib=true} +\define@boolkey+{acmart.cls}[@ACM@]{anonymous}[true]{% + \if@ACM@anonymous + \PackageInfo{\@classname}{Using anonymous mode}% + \else + \PackageInfo{\@classname}{Not using anonymous mode}% + \fi}{\PackageError{\@classname}{The option anonymous can be either true or + false}} +\ExecuteOptionsX{anonymous=false} +\define@boolkey+{acmart.cls}[@ACM@]{timestamp}[true]{% + \if@ACM@timestamp + \PackageInfo{\@classname}{Using timestamp mode}% + \else + \PackageInfo{\@classname}{Not using timestamp mode}% + \fi}{\PackageError{\@classname}{The option timestamp can be either true or + false}} +\ExecuteOptionsX{timestamp=false} +\define@boolkey+{acmart.cls}[@ACM@]{authordraft}[true]{% + \if@ACM@authordraft + \PackageInfo{\@classname}{Using authordraft mode}% + \@ACM@timestamptrue + \@ACM@reviewtrue + \else + \PackageInfo{\@classname}{Not using authordraft mode}% + \fi}{\PackageError{\@classname}{The option authordraft can be either true or + false}} +\ExecuteOptionsX{authordraft=false} +\def\ACM@fontsize{} +\DeclareOptionX{9pt}{\edef\ACM@fontsize{\CurrentOption}} +\DeclareOptionX{10pt}{\edef\ACM@fontsize{\CurrentOption}} +\DeclareOptionX{11pt}{\edef\ACM@fontsize{\CurrentOption}} +\DeclareOptionX{12pt}{\edef\ACM@fontsize{\CurrentOption}} +\DeclareOptionX{draft}{\PassOptionsToClass{\CurrentOption}{amsart}} +\DeclareOptionX{*}{\PassOptionsToClass{\CurrentOption}{amsart}} +\ProcessOptionsX +\ClassInfo{\@classname}{Using format \ACM@format, number \ACM@format@nr} +\newif\if@ACM@manuscript +\newif\if@ACM@journal +\newif\if@ACM@journal@bibstrip +\newif\if@ACM@sigchiamode +\ifnum\ACM@format@nr=5\relax % siggraph + \ClassWarning{\@classname}{The format siggraph is now obsolete. + I am switching to sigconf.} + \setkeys{acmart.cls}{format=sigconf} +\fi +\ifnum\ACM@format@nr=0\relax + \@ACM@manuscripttrue +\else + \@ACM@manuscriptfalse +\fi +\@ACM@sigchiamodefalse +\ifcase\ACM@format@nr +\relax % manuscript + \@ACM@journaltrue +\or % acmsmall + \@ACM@journaltrue +\or % acmlarge + \@ACM@journaltrue +\or % acmtog + \@ACM@journaltrue +\or % sigconf + \@ACM@journalfalse +\or % siggraph + \@ACM@journalfalse + \or % sigplan + \@ACM@journalfalse + \or % sigchi + \@ACM@journalfalse +\or % sigchi-a + \@ACM@journalfalse + \@ACM@sigchiamodetrue +\fi +\if@ACM@journal + \@ACM@journal@bibstriptrue +\else + \@ACM@journal@bibstripfalse +\fi +\ifx\ACM@fontsize\@empty + \ifcase\ACM@format@nr + \relax % manuscript + \def\ACM@fontsize{9pt}% + \or % acmsmall + \def\ACM@fontsize{10pt}% + \or % acmlarge + \def\ACM@fontsize{10pt}% + \or % acmtog + \def\ACM@fontsize{9pt}% + \or % sigconf + \def\ACM@fontsize{9pt}% + \or % siggraph + \def\ACM@fontsize{9pt}% + \or % sigplan + \def\ACM@fontsize{10pt}% + \or % sigchi + \def\ACM@fontsize{10pt}% + \or % sigchi-a + \def\ACM@fontsize{10pt}% + \fi +\fi +\ClassInfo{\@classname}{Using fontsize \ACM@fontsize} +\LoadClass[\ACM@fontsize, reqno]{amsart} +\RequirePackage{microtype} +\RequirePackage{etoolbox} +\RequirePackage{booktabs} +\RequirePackage{refcount} +\RequirePackage{totpages} +\RequirePackage{environ} +\if@ACM@manuscript +\RequirePackage{setspace} +\onehalfspacing +\fi +\RequirePackage{textcase} +\if@ACM@natbib + \RequirePackage{natbib} + \renewcommand{\bibsection}{% + \section*{\refname}% + \phantomsection\addcontentsline{toc}{section}{\refname}% + } + \renewcommand{\bibfont}{\bibliofont} + \renewcommand\setcitestyle[1]{ + \@for\@tempa:=#1\do + {\def\@tempb{round}\ifx\@tempa\@tempb + \renewcommand\NAT@open{(}\renewcommand\NAT@close{)}\fi + \def\@tempb{square}\ifx\@tempa\@tempb + \renewcommand\NAT@open{[}\renewcommand\NAT@close{]}\fi + \def\@tempb{angle}\ifx\@tempa\@tempb + \renewcommand\NAT@open{$<$}\renewcommand\NAT@close{$>$}\fi + \def\@tempb{curly}\ifx\@tempa\@tempb + \renewcommand\NAT@open{\{}\renewcommand\NAT@close{\}}\fi + \def\@tempb{semicolon}\ifx\@tempa\@tempb + \renewcommand\NAT@sep{;}\fi + \def\@tempb{colon}\ifx\@tempa\@tempb + \renewcommand\NAT@sep{;}\fi + \def\@tempb{comma}\ifx\@tempa\@tempb + \renewcommand\NAT@sep{,}\fi + \def\@tempb{authoryear}\ifx\@tempa\@tempb + \NAT@numbersfalse\fi + \def\@tempb{numbers}\ifx\@tempa\@tempb + \NAT@numberstrue\NAT@superfalse\fi + \def\@tempb{super}\ifx\@tempa\@tempb + \NAT@numberstrue\NAT@supertrue\fi + \def\@tempb{nobibstyle}\ifx\@tempa\@tempb + \let\bibstyle=\@gobble\fi + \def\@tempb{bibstyle}\ifx\@tempa\@tempb + \let\bibstyle=\@citestyle\fi + \def\@tempb{sort}\ifx\@tempa\@tempb + \def\NAT@sort{\@ne}\fi + \def\@tempb{nosort}\ifx\@tempa\@tempb + \def\NAT@sort{\z@}\fi + \def\@tempb{compress}\ifx\@tempa\@tempb + \def\NAT@cmprs{\@ne}\fi + \def\@tempb{nocompress}\ifx\@tempa\@tempb + \def\NAT@cmprs{\z@}\fi + \def\@tempb{sort&compress}\ifx\@tempa\@tempb + \def\NAT@sort{\@ne}\def\NAT@cmprs{\@ne}\fi + \def\@tempb{mcite}\ifx\@tempa\@tempb + \let\NAT@merge\@ne\fi + \def\@tempb{merge}\ifx\@tempa\@tempb + \@ifnum{\NAT@merge<\tw@}{\let\NAT@merge\tw@}{}\fi + \def\@tempb{elide}\ifx\@tempa\@tempb + \@ifnum{\NAT@merge<\thr@@}{\let\NAT@merge\thr@@}{}\fi + \def\@tempb{longnamesfirst}\ifx\@tempa\@tempb + \NAT@longnamestrue\fi + \def\@tempb{nonamebreak}\ifx\@tempa\@tempb + \def\NAT@nmfmt#1{\mbox{\NAT@up#1}}\fi + \expandafter\NAT@find@eq\@tempa=\relax\@nil + \if\@tempc\relax\else + \expandafter\NAT@rem@eq\@tempc + \def\@tempb{open}\ifx\@tempa\@tempb + \xdef\NAT@open{\@tempc}\fi + \def\@tempb{close}\ifx\@tempa\@tempb + \xdef\NAT@close{\@tempc}\fi + \def\@tempb{aysep}\ifx\@tempa\@tempb + \xdef\NAT@aysep{\@tempc}\fi + \def\@tempb{yysep}\ifx\@tempa\@tempb + \xdef\NAT@yrsep{\@tempc}\fi + \def\@tempb{notesep}\ifx\@tempa\@tempb + \xdef\NAT@cmt{\@tempc}\fi + \def\@tempb{citesep}\ifx\@tempa\@tempb + \xdef\NAT@sep{\@tempc}\fi + \fi + }% + \NAT@@setcites + } + \renewcommand\citestyle[1]{% + \ifcsname bibstyle@#1\endcsname% + \csname bibstyle@#1\endcsname\let\bibstyle\@gobble% + \else% + \@latex@error{Undefined `#1' citestyle}% + \fi + }% +\fi +\newcommand{\bibstyle@acmauthoryear}{% + \setcitestyle{% + authoryear,% + open={[},close={]},citesep={;},% + aysep={},yysep={,},% + notesep={, }}} +\newcommand{\bibstyle@acmnumeric}{% + \setcitestyle{% + numbers,sort&compress,% + open={[},close={]},citesep={,},% + notesep={, }}} +\if@ACM@natbib +\citestyle{acmnumeric} +\fi +\def\@startsection#1#2#3#4#5#6{% + \if@noskipsec \leavevmode \fi + \par + \@tempskipa #4\relax + \@afterindenttrue + \ifdim \@tempskipa <\z@ + \@tempskipa -\@tempskipa \@afterindentfalse + \fi + \if@nobreak + \everypar{}% + \else + \addpenalty\@secpenalty\addvspace\@tempskipa + \fi + \@ifstar + {\@ssect{#3}{#4}{#5}{#6}}% + {\@dblarg{\@sect{#1}{#2}{#3}{#4}{#5}{#6}}}} +\def\@sect#1#2#3#4#5#6[#7]#8{% + \edef\@toclevel{\ifnum#2=\@m 0\else\number#2\fi}% + \ifnum #2>\c@secnumdepth + \let\@svsec\@empty + \else + \refstepcounter{#1}% + \protected@edef\@svsec{\@seccntformat{#1}\relax}% + \fi + \@tempskipa #5\relax + \ifdim \@tempskipa>\z@ + \begingroup + #6{% + \@hangfrom{\hskip #3\relax\@svsec}% + \interlinepenalty \@M #8\@@par}% + \endgroup + \csname #1mark\endcsname{#7}% + \ifnum #2>\c@secnumdepth \else + \@tochangmeasure{\csname the#1\endcsname}% + \fi + \addcontentsline{toc}{#1}{% + \ifnum #2>\c@secnumdepth \else + \protect\numberline{\csname the#1\endcsname}% + \fi + #7}% + \else + \def\@svsechd{% + #6{\hskip #3\relax + \@svsec #8}% + \csname #1mark\endcsname{#7}% + \ifnum #2>\c@secnumdepth \else + \@tochangmeasure{\csname the#1\endcsname\space}% + \fi + \addcontentsline{toc}{#1}{% + \ifnum #2>\c@secnumdepth \else + \protect\numberline{\csname the#1\endcsname}% + \fi + #7}}% + \fi + \@xsect{#5}} +\def\@xsect#1{% + \@tempskipa #1\relax + \ifdim \@tempskipa>\z@ + \par \nobreak + \vskip \@tempskipa + \@afterheading + \else + \@nobreakfalse + \global\@noskipsectrue + \everypar{% + \if@noskipsec + \global\@noskipsecfalse + {\setbox\z@\lastbox}% + \clubpenalty\@M + \begingroup \@svsechd \endgroup + \unskip + \@tempskipa #1\relax + \hskip -\@tempskipa + \else + \clubpenalty \@clubpenalty + \everypar{}% + \fi}% + \fi + \ignorespaces} +\def\@seccntformat#1{\csname the#1\endcsname\quad} +\def\@ssect#1#2#3#4#5{% + \@tempskipa #3\relax + \ifdim \@tempskipa>\z@ + \begingroup + #4{% + \@hangfrom{\hskip #1}% + \interlinepenalty \@M #5\@@par}% + \endgroup + \else + \def\@svsechd{#4{\hskip #1\relax #5}}% + \fi + \@xsect{#3}} +\def\@starttoc#1#2{\begingroup\makeatletter + \setTrue{#1}% + \par\removelastskip\vskip\z@skip + \@startsection{section}\@M\z@{\linespacing\@plus\linespacing}% + {.5\linespacing}{\centering\contentsnamefont}{#2}% + \@input{\jobname.#1}% + \if@filesw + \@xp\newwrite\csname tf@#1\endcsname + \immediate\@xp\openout\csname tf@#1\endcsname \jobname.#1\relax + \fi + \global\@nobreakfalse \endgroup + \addvspace{32\p@\@plus14\p@}% +} +\def\l@section{\@tocline{1}{0pt}{1pc}{2pc}{}} +\def\l@subsection{\@tocline{2}{0pt}{1pc}{3pc}{}} +\def\l@subsubsection{\@tocline{2}{0pt}{1pc}{5pc}{}} +\def\@makefntext{\noindent\@makefnmark} +\if@ACM@sigchiamode +\long\def\@footnotetext#1{\marginpar{% + \reset@font\small + \interlinepenalty\interfootnotelinepenalty + \protected@edef\@currentlabel{% + \csname p@footnote\endcsname\@thefnmark + }% + \color@begingroup + \@makefntext{% + \rule\z@\footnotesep\ignorespaces#1\@finalstrut\strutbox}% + \color@endgroup}}% +\fi +\long\def\@mpfootnotetext#1{% + \global\setbox\@mpfootins\vbox{% + \unvbox\@mpfootins + \reset@font\footnotesize + \hsize\columnwidth + \@parboxrestore + \protected@edef\@currentlabel + {\csname p@mpfootnote\endcsname\@thefnmark}% + \color@begingroup\centering + \@makefntext{% + \rule\z@\footnotesep\ignorespaces#1\@finalstrut\strutbox}% + \color@endgroup}} +\def\@makefnmark{\hbox{\@textsuperscript{\normalfont\@thefnmark}}} +\let\@footnotemark@nolink\@footnotemark +\let\@footnotetext@nolink\@footnotetext +\RequirePackage[bookmarksnumbered,unicode]{hyperref} +\pdfstringdefDisableCommands{% + \def\addtocounter#1#2{}% + \def\unskip{}% + \def\textbullet{- }% + \def\textrightarrow{ -> }% + \def\footnotemark{}% +} +\urlstyle{rm} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge +\or % acmtog +\or % sigconf +\or % siggraph +\or % sigplan + \urlstyle{sf} +\or % sigchi +\or % sigchi-a + \urlstyle{sf} +\fi +\AtEndPreamble{% + \if@ACM@urlbreakonhyphens + \def\do@url@hyp{\do\-}% + \fi + \if@ACM@screen + \hypersetup{colorlinks, + linkcolor=ACMPurple, + citecolor=ACMPurple, + urlcolor=ACMDarkBlue, + filecolor=ACMDarkBlue} + \else + \hypersetup{hidelinks} + \fi + \hypersetup{pdflang={en}, + pdfdisplaydoctitle}} +\if@ACM@natbib + \let\citeN\cite + \let\cite\citep + \let\citeANP\citeauthor + \let\citeNN\citeyearpar + \let\citeyearNP\citeyear + \let\citeNP\citealt + \DeclareRobustCommand\citeA + {\begingroup\NAT@swafalse + \let\NAT@ctype\@ne\NAT@partrue\NAT@fullfalse\NAT@open\NAT@citetp}% + \providecommand\newblock{}% +\else + \AtBeginDocument{% + \let\shortcite\cite% + \providecommand\citename[1]{#1}} +\fi +\newcommand\shortcite[2][]{% + \ifNAT@numbers\cite[#1]{#2}\else\citeyearpar[#1]{#2}\fi} +\def\bibliographystyle#1{% + \ifx\@begindocumenthook\@undefined\else + \expandafter\AtBeginDocument + \fi + {\if@filesw + \immediate\write\@auxout{\string\bibstyle{#1}}% + \fi}} +\RequirePackage{graphicx} +\RequirePackage[prologue]{xcolor} +\definecolor[named]{ACMBlue}{cmyk}{1,0.1,0,0.1} +\definecolor[named]{ACMYellow}{cmyk}{0,0.16,1,0} +\definecolor[named]{ACMOrange}{cmyk}{0,0.42,1,0.01} +\definecolor[named]{ACMRed}{cmyk}{0,0.90,0.86,0} +\definecolor[named]{ACMLightBlue}{cmyk}{0.49,0.01,0,0} +\definecolor[named]{ACMGreen}{cmyk}{0.20,0,1,0.19} +\definecolor[named]{ACMPurple}{cmyk}{0.55,1,0,0.15} +\definecolor[named]{ACMDarkBlue}{cmyk}{1,0.58,0,0.21} +\if@ACM@authordraft + \RequirePackage{draftwatermark} + \SetWatermarkFontSize{0.5in} + \SetWatermarkColor[gray]{.9} + \SetWatermarkText{\parbox{12em}{\centering + Unpublished working draft.\\ + Not for distribution.}} +\fi +\RequirePackage{geometry} +\ifcase\ACM@format@nr +\relax % manuscript + \geometry{letterpaper,head=13pt, + marginparwidth=6pc,heightrounded}% +\or % acmsmall + \geometry{twoside=true, + includeheadfoot, head=13pt, foot=2pc, + paperwidth=6.75in, paperheight=10in, + top=58pt, bottom=44pt, inner=46pt, outer=46pt, + marginparwidth=2pc,heightrounded + }% +\or % acmlarge + \geometry{twoside=true, head=13pt, foot=2pc, + paperwidth=8.5in, paperheight=11in, + includeheadfoot, + top=78pt, bottom=114pt, inner=81pt, outer=81pt, + marginparwidth=4pc,heightrounded + }% +\or % acmtog + \geometry{twoside=true, head=13pt, foot=2pc, + paperwidth=8.5in, paperheight=11in, + includeheadfoot, columnsep=24pt, + top=52pt, bottom=75pt, inner=52pt, outer=52pt, + marginparwidth=2pc,heightrounded + }% +\or % sigconf + \geometry{twoside=true, head=13pt, + paperwidth=8.5in, paperheight=11in, + includeheadfoot, columnsep=2pc, + top=57pt, bottom=73pt, inner=54pt, outer=54pt, + marginparwidth=2pc,heightrounded + }% +\or % siggraph + \geometry{twoside=true, head=13pt, + paperwidth=8.5in, paperheight=11in, + includeheadfoot, columnsep=2pc, + top=57pt, bottom=73pt, inner=54pt, outer=54pt, + marginparwidth=2pc,heightrounded + }% +\or % sigplan + \geometry{twoside=true, head=13pt, + paperwidth=8.5in, paperheight=11in, + includeheadfoot=false, columnsep=2pc, + top=1in, bottom=1in, inner=0.75in, outer=0.75in, + marginparwidth=2pc,heightrounded + }% +\or % sigchi + \geometry{twoside=true, head=13pt, + paperwidth=8.5in, paperheight=11in, + includeheadfoot, columnsep=2pc, + top=66pt, bottom=73pt, inner=54pt, outer=54pt, + marginparwidth=2pc,heightrounded + }% +\or % sigchi-a + \geometry{twoside=false, head=13pt, + paperwidth=11in, paperheight=8.5in, + includeheadfoot, marginparsep=72pt, + marginparwidth=170pt, columnsep=20pt, + top=72pt, bottom=72pt, left=314pt, right=72pt + }% + \@mparswitchfalse + \reversemarginpar +\fi +\setlength\parindent{10\p@} +\setlength\parskip{\z@} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge +\or % acmtog + \setlength\parindent{9\p@}% +\or % sigconf +\or % siggraph +\or % sigplan +\or % sigchi +\or % sigchi-a +\fi +\setlength\normalparindent{\parindent} +\def\copyrightpermissionfootnoterule{\kern-3\p@ + \hrule \@width \columnwidth \kern 2.6\p@} +\RequirePackage{manyfoot} +\SelectFootnoteRule[2]{copyrightpermission} +\DeclareNewFootnote{authorsaddresses} +\SelectFootnoteRule[2]{copyrightpermission} +\DeclareNewFootnote{copyrightpermission} +\def\footnoterule{\kern-3\p@ + \hrule \@width 4pc \kern 2.6\p@} +\def\endminipage{% + \par + \unskip + \ifvoid\@mpfootins\else + \vskip\skip\@mpfootins + \normalcolor + \unvbox\@mpfootins + \fi + \@minipagefalse + \color@endgroup + \egroup + \expandafter\@iiiparbox\@mpargs{\unvbox\@tempboxa}} +\def\@textbottom{\vskip \z@ \@plus 1pt} +\let\@texttop\relax +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge +\or % acmtog + \flushbottom +\or % sigconf + \flushbottom +\or % siggraph + \flushbottom +\or % sigplan + \flushbottom +\or % sigchi + \flushbottom +\or % sigchi-a +\fi +\RequirePackage{iftex} +\ifPDFTeX +\input{glyphtounicode} +\pdfglyphtounicode{f_f}{FB00} +\pdfglyphtounicode{f_f_i}{FB03} +\pdfglyphtounicode{f_f_l}{FB04} +\pdfglyphtounicode{f_i}{FB01} +\pdfglyphtounicode{t_t}{0074 0074} +\pdfglyphtounicode{f_t}{0066 0074} +\pdfglyphtounicode{T_h}{0054 0068} +\pdfgentounicode=1 +\fi +\RequirePackage{cmap} +\newif\if@ACM@newfonts +\@ACM@newfontstrue +\IfFileExists{libertine.sty}{}{\ClassWarning{\@classname}{You do not + have the libertine package installed. Please upgrade your + TeX}\@ACM@newfontsfalse} +\IfFileExists{zi4.sty}{}{\ClassWarning{\@classname}{You do not + have the zi4 package installed. Please upgrade your + TeX}\@ACM@newfontsfalse} +\IfFileExists{newtxmath.sty}{}{\ClassWarning{\@classname}{You do not + have the newtxmath package installed. Please upgrade your + TeX}\@ACM@newfontsfalse} +\if@ACM@newfonts + \RequirePackage[T1]{fontenc} +\ifxetex + \RequirePackage[tt=false]{libertine} + \setmonofont{inconsolata} +\else + \RequirePackage[tt=false, type1=true]{libertine} +\fi +\RequirePackage[varqu]{zi4} +\RequirePackage[libertine]{newtxmath} +\fi +\let\liningnums\@undefined +\AtEndPreamble{% + \DeclareTextFontCommand{\liningnums}{\libertineLF}} +\if@ACM@sigchiamode + \renewcommand{\familydefault}{\sfdefault} +\fi +\newif\if@Description@present +\@Description@presenttrue +\newif\if@undescribed@images +\@undescribed@imagesfalse +\newcommand\Description[2][]{\global\@Description@presenttrue\ignorespaces} +\AtEndDocument{\if@undescribed@images + \ClassWarningNoLine{\@classname}{Some images may lack descriptions}\fi} +\AtBeginEnvironment{figure}{\@Description@presentfalse + \let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} +\AtBeginEnvironment{figure*}{\@Description@presentfalse + \let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} +\AtEndEnvironment{figure}{\if@Description@present\else + \global\@undescribed@imagestrue + \ClassWarning{\@classname}{A possible image without description}\fi} +\AtEndEnvironment{figure*}{\if@Description@present\else + \global\@undescribed@imagestrue + \ClassWarning{\@classname}{A possible image without description}\fi} +\AtBeginEnvironment{table}{\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} +\AtBeginEnvironment{table*}{\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} +\AtBeginEnvironment{algorithm}{\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} +\AtBeginEnvironment{algorithm*}{\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} +\AtBeginEnvironment{lstlisting}{\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} +\AtBeginEnvironment{lstlisting*}{\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig} + +\RequirePackage{caption, float} +\captionsetup[table]{position=top} +\if@ACM@journal + \captionsetup{labelfont={sf, small}, + textfont={sf, small}, margin=\z@} + \captionsetup[figure]{name={Fig.}} +\else + \captionsetup{labelfont={bf}, + textfont={bf}, labelsep=colon, margin=\z@} + \ifcase\ACM@format@nr + \relax % manuscript + \or % acmsmall + \or % acmlarge + \or % acmtog + \or % sigconf + \or % siggraph + \captionsetup{textfont={it}} + \or % sigplan + \captionsetup{labelfont={bf}, + textfont={normalfont}, labelsep=period, margin=\z@} + \or % sigchi + \captionsetup[figure]{labelfont={bf, small}, + textfont={bf, small}} + \captionsetup[table]{labelfont={bf, small}, + textfont={bf, small}} + \or % sigchi-a + \captionsetup[figure]{labelfont={bf, small}, + textfont={bf, small}} + \captionsetup[table]{labelfont={bf, small}, + textfont={bf, small}} + \fi +\fi +\newfloat{sidebar}{}{sbar} +\floatname{sidebar}{Sidebar} +\renewenvironment{sidebar}{\Collect@Body\@sidebar}{} +\long\def\@sidebar#1{\bgroup\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig\captionsetup{type=sidebar}% + \marginpar{\small#1}\egroup} +\newenvironment{marginfigure}{\Collect@Body\@marginfigure}{} +\long\def\@marginfigure#1{\bgroup + \let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig + \captionsetup{type=figure}% + \marginpar{\@Description@presentfalse\centering + \small#1\if@Description@present\else + \global\@undescribed@imagestrue + \ClassWarning{\@classname}{A possible image without description} + \fi}% + \egroup} +\newenvironment{margintable}{\Collect@Body\@margintable}{} +\long\def\@margintable#1{\bgroup\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig\captionsetup{type=table}% + \marginpar{\centering\small#1}\egroup} +\newdimen\fulltextwidth +\fulltextwidth=\dimexpr(\textwidth+\marginparwidth+\marginparsep) +\if@ACM@sigchiamode +\def\@dblfloat{\bgroup\let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig\columnwidth=\fulltextwidth + \let\@endfloatbox\@endwidefloatbox + \def\@fpsadddefault{\def\@fps{tp}}% + \@float} +\fi +\if@ACM@sigchiamode +\def\end@dblfloat{% + \end@float\egroup} +\fi +\def\@endwidefloatbox{% + \par\vskip\z@skip + \@minipagefalse + \outer@nobreak + \egroup + \color@endbox + \global\setbox\@currbox=\vbox{\moveleft + \dimexpr(\fulltextwidth-\textwidth)\box\@currbox}% + \wd\@currbox=\textwidth +} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge +\or % acmtog +\or % sigconf +\or % siggraph +\or % sigplan +\def\labelenumi{\theenumi.} +\def\labelenumii{\theenumii.} +\def\labelenumiii{\theenumiii.} +\def\labelenumiv{\theenumiv.} +\or % sigchi +\or % sigchi-a +\fi +\newdimen\@ACM@labelwidth +\AtBeginDocument{% + \setlength\labelsep{4pt} + \setlength{\@ACM@labelwidth}{6.5pt} + + %% First-level list: when beginning after the first line of an + %% indented paragraph or ending before an indented paragraph, labels + %% should not hang to the left of the preceding/following text. + \setlength\leftmargini{\z@} + \addtolength\leftmargini{\parindent} + \addtolength\leftmargini{2\labelsep} + \addtolength\leftmargini{\@ACM@labelwidth} + + %% Second-level and higher lists. + \setlength\leftmarginii{\z@} + \addtolength\leftmarginii{0.5\labelsep} + \addtolength\leftmarginii{\@ACM@labelwidth} + \setlength\leftmarginiii{\leftmarginii} + \setlength\leftmarginiv{\leftmarginiii} + \setlength\leftmarginv{\leftmarginiv} + \setlength\leftmarginvi{\leftmarginv} + \@listi} +\newskip\listisep +\listisep\smallskipamount +\def\@listI{\leftmargin\leftmargini + \labelwidth\leftmargini \advance\labelwidth-\labelsep + \listparindent\z@ + \topsep\listisep} +\let\@listi\@listI +\def\@listii{\leftmargin\leftmarginii + \labelwidth\leftmarginii \advance\labelwidth-\labelsep + \topsep\z@skip} +\def\@listiii{\leftmargin\leftmarginiii + \labelwidth\leftmarginiii \advance\labelwidth-\labelsep} +\def\@listiv{\leftmargin\leftmarginiv + \labelwidth\leftmarginiv \advance\labelwidth-\labelsep} +\def\@listv{\leftmargin\leftmarginv + \labelwidth\leftmarginv \advance\labelwidth-\labelsep} +\def\@listvi{\leftmargin\leftmarginvi + \labelwidth\leftmarginvi \advance\labelwidth-\labelsep} +\renewcommand{\descriptionlabel}[1]{\upshape\bfseries #1} +\renewenvironment{description}{\list{}{% + \labelwidth\@ACM@labelwidth + \let\makelabel\descriptionlabel}% +}{ + \endlist +} +\let\enddescription=\endlist % for efficiency +\newif\if@ACM@maketitle@typeset +\@ACM@maketitle@typesetfalse +\define@choicekey*+{ACM}{acmJournal}[\@journalCode\@journalCode@nr]{% + CIE,% + CSUR,% + DGOV,% + DTRAP,% + HEALTH,% + IMWUT,% + JACM,% + JDIQ,% + JEA,% + JERIC,% + JETC,% + JOCCH,% + PACMCGIT,% + PACMHCI,% + PACMPL,% + POMACS,% + TAAS,% + TACCESS,% + TACO,% + TALG,% + TALLIP,% + TAP,% + TCPS,% + TDS,% + TEAC,% + TECS,% + TELO,% + THRI,% + TIIS,% + TIOT,% + TISSEC,% + TIST,% + TKDD,% + TMIS,% + TOCE,% + TOCHI,% + TOCL,% + TOCS,% + TOCT,% + TODAES,% + TODS,% + TOG,% + TOIS,% + TOIT,% + TOMACS,% + TOMM,% + TOMPECS,% + TOMS,% + TOPC,% + TOPS,% + TOPLAS,% + TOS,% + TOSEM,% + TOSN,% + TQC,% + TRETS,% + TSAS,% + TSC,% + TSLP,% + TWEB,% + FACMP% +}{% +\ifcase\@journalCode@nr +\relax % CIE + \def\@journalName{ACM Computers in Entertainment}% + \def\@journalNameShort{ACM Comput. Entertain.}% + \def\@permissionCodeOne{1544-3574}% +\or % CSUR + \def\@journalName{ACM Computing Surveys}% + \def\@journalNameShort{ACM Comput. Surv.}% + \def\@permissionCodeOne{0360-0300}% +\or % DGOV + \def\@journalName{Digital Government: Research and Practice}% + \def\@journalNameShort{Digit. Gov. Res. Pract.}% + \def\@permissionCodeOne{2639-0175}% +\or % DTRAP + \def\@journalName{Digital Threats: Research and Practice}% + \def\@journalNameShort{Digit. Threat. Res. Pract.}% + \def\@permissionCodeOne{2576-5337}% +\or % HEALTH + \def\@journalName{ACM Transactions on Computing for Healthcare}% + \def\@journalNameShort{ACM Trans. Comput. Healthcare}% + \def\@permissionCodeOne{2637-8051}% +\or % IMWUT + \def\@journalName{Proceedings of the ACM on Interactive, Mobile, + Wearable and Ubiquitous Technologies}% + \def\@journalNameShort{Proc. ACM Interact. Mob. Wearable Ubiquitous Technol.}% + \def\@permissionCodeOne{2474-9567}% + \@ACM@screentrue + \PackageInfo{\@classname}{Using screen mode due to \@journalCode}% +\or % JACM + \def\@journalName{Journal of the ACM}% + \def\@journalNameShort{J. ACM}% + \def\@permissionCodeOne{0004-5411}% +\or % JDIQ + \def\@journalName{ACM Journal of Data and Information Quality}% + \def\@journalNameShort{ACM J. Data Inform. Quality}% + \def\@permissionCodeOne{1936-1955}% +\or % JEA + \def\@journalName{ACM Journal of Experimental Algorithmics}% + \def\@journalNameShort{ACM J. Exp. Algor.}% + \def\@permissionCodeOne{1084-6654}% +\or % JERIC + \def\@journalName{ACM Journal of Educational Resources in Computing}% + \def\@journalNameShort{ACM J. Edu. Resources in Comput.}% + \def\@permissionCodeOne{1073-0516}% +\or % JETC + \def\@journalName{ACM Journal on Emerging Technologies in Computing Systems}% + \def\@journalNameShort{ACM J. Emerg. Technol. Comput. Syst.}% + \def\@permissionCodeOne{1550-4832}% +\or % JOCCH + \def\@journalName{ACM Journal on Computing and Cultural Heritage}% + \def\@journalNameShort{ACM J. Comput. Cult. Herit.}% +\or % PACMCGIT + \def\@journalName{Proceedings of the ACM on Computer Graphics and Interactive Techniques}% + \def\@journalNameShort{Proc. ACM Comput. Graph. Interact. Tech.}% + \def\@permissionCodeOne{2577-6193}% + \@ACM@screentrue + \PackageInfo{\@classname}{Using screen mode due to \@journalCode}% +\or % PACMHCI + \def\@journalName{Proceedings of the ACM on Human-Computer Interaction}% + \def\@journalNameShort{Proc. ACM Hum.-Comput. Interact.}% + \def\@permissionCodeOne{2573-0142}% + \@ACM@screentrue + \PackageInfo{\@classname}{Using screen mode due to \@journalCode}% +\or % PACMPL + \def\@journalName{Proceedings of the ACM on Programming Languages}% + \def\@journalNameShort{Proc. ACM Program. Lang.}% + \def\@permissionCodeOne{2475-1421}% + \@ACM@screentrue + \PackageInfo{\@classname}{Using screen mode due to \@journalCode}% +\or % POMACS + \def\@journalName{Proceedings of the ACM on Measurement and Analysis of Computing Systems}% + \def\@journalNameShort{Proc. ACM Meas. Anal. Comput. Syst.}% + \def\@permissionCodeOne{2476-1249}% + \@ACM@screentrue + \PackageInfo{\@classname}{Using screen mode due to \@journalCode}% +\or % TAAS + \def\@journalName{ACM Transactions on Autonomous and Adaptive Systems}% + \def\@journalNameShort{ACM Trans. Autonom. Adapt. Syst.}% + \def\@permissionCodeOne{1556-4665}% +\or % TACCESS + \def\@journalName{ACM Transactions on Accessible Computing}% + \def\@journalNameShort{ACM Trans. Access. Comput.}% + \def\@permissionCodeOne{1936-7228}% +\or % TACO + \def\@journalName{ACM Transactions on Architecture and Code Optimization}% + \def\@journalNameShort{ACM Trans. Arch. Code Optim.}% +\or % TALG + \def\@journalName{ACM Transactions on Algorithms}% + \def\@journalNameShort{ACM Trans. Algor.}% + \def\@permissionCodeOne{1549-6325}% +\or % TALLIP + \def\@journalName{ACM Transactions on Asian and Low-Resource Language Information Processing}% + \def\@journalNameShort{ACM Trans. Asian Low-Resour. Lang. Inf. Process.}% + \def\@permissionCodeOne{2375-4699}% +\or % TAP + \def\@journalName{ACM Transactions on Applied Perception}% +\or % TCPS + \def\@journalName{ACM Transactions on Cyber-Physical Systems}% +\or % TDS + \def\@journalName{ACM/IMS Transactions on Data Science}% + \def\@journalNameShort{ACM/IMS Trans. Data Sci.}% + \def\@permissionCodeOne{2577-3224}% +\or % TEAC + \def\@journalName{ACM Transactions on Economics and Computation}% +\or % TECS + \def\@journalName{ACM Transactions on Embedded Computing Systems}% + \def\@journalNameShort{ACM Trans. Embedd. Comput. Syst.}% + \def\@permissionCodeOne{1539-9087}% +\or % TELO + \def\@journalName{ACM Transactions on Evolutionary Learning}% + \def\@journalNameShort{ACM Trans. Evol. Learn.}% + \def\@permissionCodeOne{2688-3007}% +\or % THRI + \def\@journalName{ACM Transactions on Human-Robot Interaction}% + \def\@journalNameShort{ACM Trans. Hum.-Robot Interact.}% + \def\@permissionCodeOne{2573-9522}% +\or % TIIS + \def\@journalName{ACM Transactions on Interactive Intelligent Systems}% + \def\@journalNameShort{ACM Trans. Interact. Intell. Syst.}% + \def\@permissionCodeOne{2160-6455}% +\or % TIOT + \def\@journalName{ACM Transactions on Internet of Things}% + \def\@journalNameShort{ACM Trans. Internet Things}% + \def\@permissionCodeOne{2577-6207}% +\or % TISSEC + \def\@journalName{ACM Transactions on Information and System Security}% + \def\@journalNameShort{ACM Trans. Info. Syst. Sec.}% + \def\@permissionCodeOne{1094-9224}% +\or % TIST + \def\@journalName{ACM Transactions on Intelligent Systems and Technology}% + \def\@journalNameShort{ACM Trans. Intell. Syst. Technol.}% + \def\@permissionCodeOne{2157-6904}% +\or % TKDD + \def\@journalName{ACM Transactions on Knowledge Discovery from Data}% + \def\@journalNameShort{ACM Trans. Knowl. Discov. Data.}% + \def\@permissionCodeOne{1556-4681}% +\or % TMIS + \def\@journalName{ACM Transactions on Management Information Systems}% + \def\@journalNameShort{ACM Trans. Manag. Inform. Syst.}% + \def\@permissionCodeOne{2158-656X}% +\or % TOCE + \def\@journalName{ACM Transactions on Computing Education}% + \def\@journalNameShort{ACM Trans. Comput. Educ.}% + \def\@permissionCodeOne{1946-6226}% +\or % TOCHI + \def\@journalName{ACM Transactions on Computer-Human Interaction}% + \def\@journalNameShort{ACM Trans. Comput.-Hum. Interact.}% + \def\@permissionCodeOne{1073-0516}% +\or % TOCL + \def\@journalName{ACM Transactions on Computational Logic}% + \def\@journalNameShort{ACM Trans. Comput. Logic}% + \def\@permissionCodeOne{1529-3785}% +\or % TOCS + \def\@journalName{ACM Transactions on Computer Systems}% + \def\@journalNameShort{ACM Trans. Comput. Syst.}% + \def\@permissionCodeOne{0734-2071}% +\or % TOCT + \def\@journalName{ACM Transactions on Computation Theory}% + \def\@journalNameShort{ACM Trans. Comput. Theory}% + \def\@permissionCodeOne{1942-3454}% +\or % TODAES + \def\@journalName{ACM Transactions on Design Automation of Electronic Systems}% + \def\@journalNameShort{ACM Trans. Des. Autom. Electron. Syst.}% + \def\@permissionCodeOne{1084-4309}% +\or % TODS + \def\@journalName{ACM Transactions on Database Systems}% + \def\@journalNameShort{ACM Trans. Datab. Syst.}% + \def\@permissionCodeOne{0362-5915}% +\or % TOG + \def\@journalName{ACM Transactions on Graphics}% + \def\@journalNameShort{ACM Trans. Graph.}% + \def\@permissionCodeOne{0730-0301} +\or % TOIS + \def\@journalName{ACM Transactions on Information Systems}% + \def\@permissionCodeOne{1046-8188}% +\or % TOIT + \def\@journalName{ACM Transactions on Internet Technology}% + \def\@journalNameShort{ACM Trans. Internet Technol.}% + \def\@permissionCodeOne{1533-5399}% +\or % TOMACS + \def\@journalName{ACM Transactions on Modeling and Computer Simulation}% + \def\@journalNameShort{ACM Trans. Model. Comput. Simul.}% +\or % TOMM + \def\@journalName{ACM Transactions on Multimedia Computing, Communications and Applications}% + \def\@journalNameShort{ACM Trans. Multimedia Comput. Commun. Appl.}% + \def\@permissionCodeOne{1551-6857}% + \def\@permissionCodeTwo{0100}% +\or % TOMPECS + \def\@journalName{ACM Transactions on Modeling and Performance Evaluation of Computing Systems}% + \def\@journalNameShort{ACM Trans. Model. Perform. Eval. Comput. Syst.}% + \def\@permissionCodeOne{2376-3639}% +\or % TOMS + \def\@journalName{ACM Transactions on Mathematical Software}% + \def\@journalNameShort{ACM Trans. Math. Softw.}% + \def\@permissionCodeOne{0098-3500}% +\or % TOPC + \def\@journalName{ACM Transactions on Parallel Computing}% + \def\@journalNameShort{ACM Trans. Parallel Comput.}% + \def\@permissionCodeOne{1539-9087}% +\or % TOPS + \def\@journalName{ACM Transactions on Privacy and Security}% + \def\@journalNameShort{ACM Trans. Priv. Sec.}% + \def\@permissionCodeOne{2471-2566}% +\or % TOPLAS + \def\@journalName{ACM Transactions on Programming Languages and Systems}% + \def\@journalNameShort{ACM Trans. Program. Lang. Syst.}% + \def\@permissionCodeOne{0164-0925}% +\or % TOS + \def\@journalName{ACM Transactions on Storage}% + \def\@journalNameShort{ACM Trans. Storage}% + \def\@permissionCodeOne{1553-3077}% +\or % TOSEM + \def\@journalName{ACM Transactions on Software Engineering and Methodology}% + \def\@journalNameShort{ACM Trans. Softw. Eng. Methodol.}% + \def\@permissionCodeOne{1049-331X}% +\or % TOSN + \def\@journalName{ACM Transactions on Sensor Networks}% + \def\@journalNameShort{ACM Trans. Sensor Netw.}% + \def\@permissionCodeOne{1550-4859}% +\or % TQC + \def\@journalName{ACM Transactions on Quantum Computing}% + \def\@journalNameShort{ACM Trans. Quantum Comput.}% + \def\@permissionCodeOne{2643-6817}% +\or % TRETS + \def\@journalName{ACM Transactions on Reconfigurable Technology and Systems}% + \def\@journalNameShort{ACM Trans. Reconfig. Technol. Syst.}% + \def\@permissionCodeOne{1936-7406}% +\or % TSAS + \def\@journalName{ACM Transactions on Spatial Algorithms and Systems}% + \def\@journalNameShort{ACM Trans. Spatial Algorithms Syst.}% + \def\@permissionCodeOne{2374-0353}% +\or % TSC + \def\@journalName{ACM Transactions on Social Computing}% + \def\@journalNameShort{ACM Trans. Soc. Comput.}% + \def\@permissionCodeOne{2469-7818}% +\or % TSLP + \def\@journalName{ACM Transactions on Speech and Language Processing}% + \def\@journalNameShort{ACM Trans. Speech Lang. Process.}% + \def\@permissionCodeOne{1550-4875}% +\or % TWEB + \def\@journalName{ACM Transactions on the Web}% + \def\@journalNameShort{ACM Trans. Web}% + \def\@permissionCodeOne{1559-1131}% +\else % FACMP, a dummy journal + \def\@journalName{Forthcoming ACM Publication}% + \def\@journalNameShort{ACM Forthcoming}% + \def\@permissionCodeOne{XXXX-XXXX}% +\fi +\ClassInfo{\@classname}{Using journal code \@journalCode}% +}{% + \ClassError{\@classname}{Incorrect journal #1}% +}% +\def\acmJournal#1{\setkeys{ACM}{acmJournal=#1}% + \global\@ACM@journal@bibstriptrue} +\def\@journalCode@nr{0} +\def\@journalName{}% +\def\@journalNameShort{\@journalName}% +\def\@permissionCodeOne{XXXX-XXXX}% +\def\@permissionCodeTwo{}% +\newcommand\acmConference[4][]{% + \gdef\acmConference@shortname{#1}% + \gdef\acmConference@name{#2}% + \gdef\acmConference@date{#3}% + \gdef\acmConference@venue{#4}% + \ifx\acmConference@shortname\@empty + \gdef\acmConference@shortname{#2}% + \fi + \global\@ACM@journal@bibstripfalse +} +\if@ACM@journal\else +\acmConference[Conference'17]{ACM Conference}{July 2017}{Washington, + DC, USA}% +\fi +\def\acmBooktitle#1{\gdef\@acmBooktitle{#1}} +\acmBooktitle{Proceedings of \acmConference@name + \ifx\acmConference@name\acmConference@shortname\else + \ (\acmConference@shortname)\fi} +\def\@editorsAbbrev{(Ed.)} +\def\@acmEditors{} +\def\editor#1{\ifx\@acmEditors\@empty + \gdef\@acmEditors{#1}% + \else + \gdef\@editorsAbbrev{(Eds.)}% + \g@addto@macro\@acmEditors{\and#1}% +\fi} +\def\subtitle#1{\def\@subtitle{#1}} +\subtitle{} +\newcount\num@authorgroups +\num@authorgroups=0\relax +\newcount\num@authors +\num@authors=0\relax +\newif\if@insideauthorgroup +\@insideauthorgroupfalse +\renewcommand\author[2][]{% + \IfSubStr{#2}{,}{\ClassWarning{\@classname}{Do not put several + authors in the same \string\author\space macro!}}{}% + \global\advance\num@authors by 1\relax + \if@insideauthorgroup\else + \global\advance\num@authorgroups by 1\relax + \global\@insideauthorgrouptrue + \fi + \ifx\addresses\@empty + \if@ACM@anonymous + \gdef\addresses{\@author{Anonymous Author(s)% + \ifx\@acmSubmissionID\@empty\else\\Submission Id: + \@acmSubmissionID\fi}}% + \gdef\authors{Anonymous Author(s)}% + \else + \gdef\addresses{\@author{#2}}% + \gdef\authors{#2}% + \fi + \else + \if@ACM@anonymous\else + \g@addto@macro\addresses{\and\@author{#2}}% + \g@addto@macro\authors{\and#2}% + \fi + \fi + \if@ACM@anonymous + \ifx\shortauthors\@empty + \gdef\shortauthors{Anon. + \ifx\@acmSubmissionID\@empty\else Submission Id: + \@acmSubmissionID\fi}% + \fi + \else + \def\@tempa{#1}% + \ifx\@tempa\@empty + \ifx\shortauthors\@empty + \gdef\shortauthors{#2}% + \else + \g@addto@macro\shortauthors{\and#2}% + \fi + \else + \ifx\shortauthors\@empty + \gdef\shortauthors{#1}% + \else + \g@addto@macro\shortauthors{\and#1}% + \fi + \fi + \fi} +\newcommand{\affiliation}[2][]{% + \global\@insideauthorgroupfalse + \if@ACM@anonymous\else + \g@addto@macro\addresses{\affiliation{#1}{#2}}% + \fi} +\define@boolkey+{@ACM@affiliation@}[@ACM@affiliation@]{obeypunctuation}% +[true]{}{\ClassError{\@classname}{The option obeypunctuation can be either true or false}} +\def\additionalaffiliation#1{\authornote{\@additionalaffiliation{#1}}} +\def\@additionalaffiliation#1{\bgroup + \def\position##1{\ignorespaces}% + \def\institution##1{##1\ignorespaces}% + \def\department{\@ifnextchar[{\@department}{\@department[]}}% + \def\@department[##1]##2{\unskip, ##2\ignorespaces}% + \let\streetaddress\position + \let\city\position + \let\state\position + \let\postcode\position + \let\country\position + Also with #1\unskip.\egroup} +\renewcommand{\email}[2][]{% + \IfSubStr{#2}{,}{\ClassWarning{\@classname}{Do not put several + addresses in the same \string\email\space macro!}}{}% + \if@ACM@anonymous\else + \g@addto@macro\addresses{\email{#1}{#2}}% + \fi} +\def\orcid#1{\unskip\ignorespaces} +\def\authorsaddresses#1{\def\@authorsaddresses{#1}} +\authorsaddresses{\@mkauthorsaddresses} +\def\@titlenotes{} +\def\titlenote#1{% + \g@addto@macro\@title{\footnotemark}% + \if@ACM@anonymous + \g@addto@macro\@titlenotes{% + \stepcounter{footnote}\footnotetext{Title note}}% + \else + \g@addto@macro\@titlenotes{\stepcounter{footnote}\footnotetext{#1}}% + \fi} +\def\@subtitlenotes{} +\def\subtitlenote#1{% + \g@addto@macro\@subtitle{\footnotemark}% + \if@ACM@anonymous + \g@addto@macro\@subtitlenotes{% + \stepcounter{footnote}\footnotetext{Subtitle note}}% + \else + \g@addto@macro\@subtitlenotes{% + \stepcounter{footnote}\footnotetext{#1}}% + \fi} +\def\@authornotes{} +\def\authornote#1{% + \if@ACM@anonymous\else + \g@addto@macro\addresses{\@authornotemark}% + \g@addto@macro\@authornotes{% + \stepcounter{footnote}\footnotetext{#1}}% + \fi} +\newcommand\authornotemark[1][\relax]{% + \ifx#1\relax\relax\relax + \g@addto@macro\addresses{\@authornotemark}% + \else + \g@addto@macro\addresses{\@@authornotemark{#1}}% + \fi} +\def\acmVolume#1{\def\@acmVolume{#1}} +\acmVolume{1} +\def\acmNumber#1{\def\@acmNumber{#1}} +\acmNumber{1} +\def\acmArticle#1{\def\@acmArticle{#1}} +\acmArticle{} +\def\acmArticleSeq#1{\def\@acmArticleSeq{#1}} +\acmArticleSeq{\@acmArticle} +\def\acmYear#1{\def\@acmYear{#1}} +\acmYear{\the\year} +\def\acmMonth#1{\def\@acmMonth{#1}} +\acmMonth{\the\month} +\def\@acmPubDate{\ifcase\@acmMonth\or + January\or February\or March\or April\or May\or June\or + July\or August\or September\or October\or November\or + December\fi~\@acmYear} +\def\acmPrice#1{\def\@acmPrice{#1}} +\acmPrice{15.00} +\def\acmSubmissionID#1{\def\@acmSubmissionID{#1}} +\acmSubmissionID{} +\def\acmISBN#1{\def\@acmISBN{#1}} +\acmISBN{978-x-xxxx-xxxx-x/YY/MM} +\def\acmDOI#1{\def\@acmDOI{#1}} +\acmDOI{10.1145/nnnnnnn.nnnnnnn} +\newif\if@ACM@badge +\@ACM@badgefalse +\newlength\@ACM@badge@width +\setlength\@ACM@badge@width{5pc} +\newlength\@ACM@title@width +\newlength\@ACM@badge@skip +\setlength\@ACM@badge@skip{1pc} +\newcommand\acmBadgeR[2][]{\@ACM@badgetrue + \def\@acmBadgeR@url{#1}% + \def\@acmBadgeR@image{#2}} +\def\@acmBadgeR@url{} +\def\@acmBadgeR@image{} +\newcommand\acmBadgeL[2][]{\@ACM@badgetrue + \def\@acmBadgeL@url{#1}% + \def\@acmBadgeL@image{#2}} +\def\@acmBadgeL@url{} +\def\@acmBadgeL@image{} +\def\startPage#1{\def\@startPage{#1}} +\startPage{} +\def\terms#1{\ClassWarning{\@classname}{The command \string\terms{} is + obsolete. I am going to ignore it}} +\def\keywords#1{\def\@keywords{#1}} +\let\@keywords\@empty +\AtEndDocument{\if@ACM@nonacm\else\ifx\@keywords\@empty + \ifnum\getrefnumber{TotPages}>2\relax + \ClassWarningNoLine{\@classname}{ACM keywords are mandatory + for papers over two pages}% + \fi\fi\fi} +\renewenvironment{abstract}{\Collect@Body\@saveabstract}{} +\long\def\@saveabstract#1{\if@ACM@maketitle@typeset + \ClassError{\@classname}{Abstract must be defined before maketitle + command. Please move it!}\fi + \long\gdef\@abstract{#1}} +\@saveabstract{} +\long\def\@lempty{} +\define@boolkey+{@ACM@topmatter@}[@ACM@]{printccs}[true]{% + \if@ACM@printccs + \ClassInfo{\@classname}{Printing CCS}% + \else + \ClassInfo{\@classname}{Suppressing CCS}% + \fi}{\ClassError{\@classname}{The option printccs can be either true or false}} +\define@boolkey+{@ACM@topmatter@}[@ACM@]{printacmref}[true]{% + \if@ACM@printacmref + \ClassInfo{\@classname}{Printing bibformat}% + \else + \ClassInfo{\@classname}{Suppressing bibformat}% + \fi}{\ClassError{\@classname}{The option printacmref can be either true or false}} +\AtEndDocument{\if@ACM@nonacm\else\if@ACM@printacmref\else + \ifnum\getrefnumber{TotPages}>1\relax + \ClassWarningNoLine{\@classname}{ACM reference format is mandatory + for papers over one page}% + \fi\fi\fi} +\define@boolkey+{@ACM@topmatter@}[@ACM@]{printfolios}[true]{% + \if@ACM@printfolios + \ClassInfo{\@classname}{Printing folios}% + \else + \ClassInfo{\@classname}{Suppressing folios}% + \fi}{\ClassError{\@classname}{The option printfolios can be either true or false}} +\define@cmdkey{@ACM@topmatter@}[@ACM@]{authorsperrow}[0]{% + \IfInteger{#1}{\ClassInfo{\@classname}{Setting authorsperrow to + #1}}{\ClassWarning{\@classname}{The parameter authorsperrow must be + numerical. Ignoring the input #1}\gdef\@ACM@authorsperrow{0}}} +\def\settopmatter#1{\setkeys{@ACM@topmatter@}{#1}} +\settopmatter{printccs=true, printacmref=true} +\if@ACM@manuscript + \settopmatter{printfolios=true} +\else + \if@ACM@journal + \settopmatter{printfolios=true} + \else + \settopmatter{printfolios=false} + \fi +\fi +\settopmatter{authorsperrow=0} +\def\@received{} +\newcommand\received[2][]{\def\@tempa{#1}% + \ifx\@tempa\@empty + \ifx\@received\@empty + \gdef\@received{Received #2}% + \else + \g@addto@macro{\@received}{; revised #2}% + \fi + \else + \ifx\@received\@empty + \gdef\@received{#1 #2}% + \else + \g@addto@macro{\@received}{; #1 #2}% + \fi + \fi} +\AtEndDocument{% + \ifx\@received\@empty\else + \par\bigskip\noindent\small\normalfont\@received\par + \fi} +\RequirePackage{comment} +\excludecomment{CCSXML} +\let\@concepts\@empty +\newcounter{@concepts} +\newcommand\ccsdesc[2][100]{% + \ccsdesc@parse#1~#2~~\ccsdesc@parse@end} +\def\textrightarrow{$\rightarrow$} +\def\ccsdesc@parse#1~#2~#3~{% + \stepcounter{@concepts}% + \expandafter\ifx\csname CCS@General@#2\endcsname\relax + \expandafter\gdef\csname CCS@General@#2\endcsname{\textbullet\ + \textbf{#2}}% + \expandafter\gdef\csname CCS@Punctuation@#2\endcsname{; }% + \expandafter\gdef\csname CCS@Specific@#2\endcsname{}% + \g@addto@macro{\@concepts}{\csname CCS@General@#2\endcsname + \csname CCS@Punctuation@#2\endcsname + \csname CCS@Specific@#2\endcsname}% + \fi + \ifx#3\relax\relax\else + \expandafter\gdef\csname CCS@Punctuation@#2\endcsname{ + \textrightarrow\ }% + \expandafter\g@addto@macro\expandafter{\csname CCS@Specific@#2\endcsname}{% + \addtocounter{@concepts}{-1}% + \ifnum#1>499\textbf{#3}\else + \ifnum#1>299\textit{#3}\else + #3\fi\fi\ifnum\value{@concepts}=0.\else; \fi}% + \fi +\ccsdesc@parse@finish} +\AtEndDocument{\if@ACM@nonacm\else\ifx\@concepts\@empty\relax + \ifnum\getrefnumber{TotPages}>2\relax + \ClassWarningNoLine{\@classname}{CCS concepts are mandatory + for papers over two pages}% + \fi\fi\fi} +\def\ccsdesc@parse@finish#1\ccsdesc@parse@end{} +\newif\if@printcopyright +\@printcopyrighttrue +\newif\if@printpermission +\@printpermissiontrue +\newif\if@acmowned +\@acmownedtrue +\define@choicekey*{ACM@}{acmcopyrightmode}[% + \acm@copyrightinput\acm@copyrightmode]{none,% + acmcopyright,acmlicensed,rightsretained,% + usgov,usgovmixed,cagov,cagovmixed,licensedusgovmixed,% + licensedcagov,licensedcagovmixed,othergov,licensedothergov,% + iw3c2w3,iw3c2w3g}{% + \@printpermissiontrue + \@printcopyrighttrue + \@acmownedtrue + \ifnum\acm@copyrightmode=0\relax % none + \@printpermissionfalse + \@printcopyrightfalse + \@acmownedfalse + \fi + \ifnum\acm@copyrightmode=2\relax % acmlicensed + \@acmownedfalse + \fi + \ifnum\acm@copyrightmode=3\relax % rightsretained + \@acmownedfalse + \AtBeginDocument{\acmPrice{}}% + \fi + \ifnum\acm@copyrightmode=4\relax % usgov + \@printpermissiontrue + \@printcopyrightfalse + \@acmownedfalse + \AtBeginDocument{\acmPrice{}}% + \fi + \ifnum\acm@copyrightmode=6\relax % cagov + \@acmownedfalse + \fi + \ifnum\acm@copyrightmode=8\relax % licensedusgovmixed + \@acmownedfalse + \fi + \ifnum\acm@copyrightmode=9\relax % licensedcagov + \@acmownedfalse + \fi + \ifnum\acm@copyrightmode=10\relax % licensedcagovmixed + \@acmownedfalse + \fi + \ifnum\acm@copyrightmode=11\relax % othergov + \@acmownedtrue + \fi + \ifnum\acm@copyrightmode=12\relax % licensedothergov + \@acmownedfalse + \fi + \ifnum\acm@copyrightmode=13\relax % iw3c2w3 + \@acmownedfalse + \AtBeginDocument{\acmPrice{}}% + \fi + \ifnum\acm@copyrightmode=14\relax % iw3c2w3g + \@acmownedfalse + \AtBeginDocument{\acmPrice{}}% + \fi} +\def\setcopyright#1{\setkeys{ACM@}{acmcopyrightmode=#1}} +\setcopyright{acmcopyright} +\def\@copyrightowner{% + \ifcase\acm@copyrightmode\relax % none + \or % acmcopyright + Association for Computing Machinery. + \or % acmlicensed + Copyright held by the owner/author(s). Publication rights licensed to + ACM\@. + \or % rightsretained + Copyright held by the owner/author(s). + \or % usgov + \or % usgovmixed + Association for Computing Machinery. + \or % cagov + Crown in Right of Canada. + \or %cagovmixed + Association for Computing Machinery. + \or %licensedusgovmixed + Copyright held by the owner/author(s). Publication rights licensed to + ACM\@. + \or % licensedcagov + Crown in Right of Canada. Publication rights licensed to + ACM\@. + \or %licensedcagovmixed + Copyright held by the owner/author(s). Publication rights licensed to + ACM\@. + \or % othergov + Association for Computing Machinery. + \or % licensedothergov + Copyright held by the owner/author(s). Publication rights licensed to + ACM\@. + \or % ic2w3www + IW3C2 (International World Wide Web Conference Committee), published + under Creative Commons CC-BY~4.0 License. + \or % ic2w3wwwgoogle + IW3C2 (International World Wide Web Conference Committee), published + under Creative Commons CC-BY-NC-ND~4.0 License. + \fi} +\def\@formatdoi#1{\url{https://doi.org/#1}} +\def\@copyrightpermission{% + \ifcase\acm@copyrightmode\relax % none + \or % acmcopyright + Permission to make digital or hard copies of all or part of this + work for personal or classroom use is granted without fee provided + that copies are not made or distributed for profit or commercial + advantage and that copies bear this notice and the full citation on + the first page. Copyrights for components of this work owned by + others than ACM must be honored. Abstracting with credit is + permitted. To copy otherwise, or republish, to post on servers or to + redistribute to lists, requires prior specific permission + and\hspace*{.5pt}/or a fee. Request permissions from + permissions@acm.org. + \or % acmlicensed + Permission to make digital or hard copies of all or part of this + work for personal or classroom use is granted without fee provided + that copies are not made or distributed for profit or commercial + advantage and that copies bear this notice and the full citation on + the first page. Copyrights for components of this work owned by + others than the author(s) must be honored. Abstracting with credit + is permitted. To copy otherwise, or republish, to post on servers + or to redistribute to lists, requires prior specific permission + and\hspace*{.5pt}/or a fee. Request permissions from + permissions@acm.org. + \or % rightsretained + Permission to make digital or hard copies of part or all of this work + for personal or classroom use is granted without fee provided that + copies are not made or distributed for profit or commercial advantage + and that copies bear this notice and the full citation on the first + page. Copyrights for third-party components of this work must be + honored. For all other uses, contact the + owner\hspace*{.5pt}/author(s). + \or % usgov + This paper is authored by an employee(s) of the United States + Government and is in the public domain. Non-exclusive copying or + redistribution is allowed, provided that the article citation is + given and the authors and agency are clearly identified as its + source. + \or % usgovmixed + ACM acknowledges that this contribution was authored or co-authored + by an employee, contractor, or affiliate of the United States + government. As such, the United States government retains a + nonexclusive, royalty-free right to publish or reproduce this + article, or to allow others to do so, for government purposes only. + \or % cagov + This article was authored by employees of the Government of Canada. + As such, the Canadian government retains all interest in the + copyright to this work and grants to ACM a nonexclusive, + royalty-free right to publish or reproduce this article, or to allow + others to do so, provided that clear attribution is given both to + the authors and the Canadian government agency employing them. + Permission to make digital or hard copies for personal or classroom + use is granted. Copies must bear this notice and the full citation + on the first page. Copyrights for components of this work owned by + others than the Canadian Government must be honored. To copy + otherwise, distribute, republish, or post, requires prior specific + permission and\hspace*{.5pt}/or a fee. Request permissions from + permissions@acm.org. + \or % cagovmixed + ACM acknowledges that this contribution was co-authored by an + affiliate of the national government of Canada. As such, the Crown + in Right of Canada retains an equal interest in the copyright. + Reprints must include clear attribution to ACM and the author's + government agency affiliation. Permission to make digital or hard + copies for personal or classroom use is granted. Copies must bear + this notice and the full citation on the first page. Copyrights for + components of this work owned by others than ACM must be honored. + To copy otherwise, distribute, republish, or post, requires prior + specific permission and\hspace*{.5pt}/or a fee. Request permissions + from permissions@acm.org. + \or % licensedusgovmixed + Publication rights licensed to ACM\@. ACM acknowledges that this + contribution was authored or co-authored by an employee, contractor + or affiliate of the United States government. As such, the + Government retains a nonexclusive, royalty-free right to publish or + reproduce this article, or to allow others to do so, for Government + purposes only. + \or % licensedcagov + This article was authored by employees of the Government of Canada. + As such, the Canadian government retains all interest in the + copyright to this work and grants to ACM a nonexclusive, + royalty-free right to publish or reproduce this article, or to allow + others to do so, provided that clear attribution is given both to + the authors and the Canadian government agency employing them. + Permission to make digital or hard copies for personal or classroom + use is granted. Copies must bear this notice and the full citation + on the first page. Copyrights for components of this work owned by + others than the Canadian Government must be honored. To copy + otherwise, distribute, republish, or post, requires prior specific + permission and\hspace*{.5pt}/or a fee. Request permissions from + permissions@acm.org. + \or % licensedcagovmixed + Publication rights licensed to ACM\@. ACM acknowledges that this + contribution was authored or co-authored by an employee, contractor + or affiliate of the national government of Canada. As such, the + Government retains a nonexclusive, royalty-free right to publish or + reproduce this article, or to allow others to do so, for Government + purposes only. + \or % othergov + ACM acknowledges that this contribution was authored or co-authored + by an employee, contractor or affiliate of a national government. As + such, the Government retains a nonexclusive, royalty-free right to + publish or reproduce this article, or to allow others to do so, for + Government purposes only. + \or % licensedothergov + Publication rights licensed to ACM\@. ACM acknowledges that this + contribution was authored or co-authored by an employee, contractor + or affiliate of a national government. As such, the Government + retains a nonexclusive, royalty-free right to publish or reproduce + this article, or to allow others to do so, for Government purposes + only. + \or % iw3c2w3 + This paper is published under the Creative Commons Attribution~4.0 + International (CC-BY~4.0) license. Authors reserve their rights to + disseminate the work on their personal and corporate Web sites with + the appropriate attribution. + \or % iw3c2w3g + This paper is published under the Creative Commons + Attribution-NonCommercial-NoDerivs~4.0 International + (CC-BY-NC-ND~4.0) license. Authors reserve their rights to + disseminate the work on their personal and corporate Web sites with + the appropriate attribution. + \fi} +\def\copyrightyear#1{\def\@copyrightyear{#1}} +\copyrightyear{\@acmYear} +\def\@teaserfigures{} +\newenvironment{teaserfigure}{\Collect@Body\@saveteaser}{} +\long\def\@saveteaser#1{\g@addto@macro\@teaserfigures{\@teaser{#1}}} +\renewcommand{\thanks}[1]{% + \@ifnotempty{#1}{% + \if@ACM@anonymous + \g@addto@macro\thankses{\thanks{A note}}% + \else + \g@addto@macro\thankses{\thanks{#1}}% + \fi}} +\newbox\mktitle@bx +\def\maketitle{% + \@ACM@maketitle@typesettrue + \if@ACM@anonymous + % Anonymize omission of \author-s + \ifnum\num@authorgroups=0\author{}\fi + \fi + \begingroup + \let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig + \let\@footnotemark\@footnotemark@nolink + \let\@footnotetext\@footnotetext@nolink + \renewcommand\thefootnote{\@fnsymbol\c@footnote}% + \hsize=\textwidth + \def\@makefnmark{\hbox{\@textsuperscript{\@thefnmark}}}% + \@mktitle\if@ACM@sigchiamode\else\@mkauthors\fi\@mkteasers + \@printtopmatter + \if@ACM@sigchiamode\@mkauthors\fi + \setcounter{footnote}{0}% + \def\@makefnmark{\hbox{\@textsuperscript{\normalfont\@thefnmark}}}% + \@titlenotes + \@subtitlenotes + \@authornotes + \let\@makefnmark\relax + \let\@thefnmark\relax + \let\@makefntext\noindent + \ifx\@empty\thankses\else + \footnotetextauthorsaddresses{% + \def\par{\let\par\@par}\parindent\z@\@setthanks}% + \fi + \ifx\@empty\@authorsaddresses\else + \if@ACM@anonymous\else + \if@ACM@journal@bibstrip + \footnotetextauthorsaddresses{% + \def\par{\let\par\@par}\parindent\z@\@setauthorsaddresses}% + \fi + \fi + \fi + \if@ACM@nonacm\else\footnotetextcopyrightpermission{% + \if@ACM@authordraft + \raisebox{-2ex}[\z@][\z@]{\makebox[0pt][l]{\large\bfseries + Unpublished working draft. Not for distribution.}}% + \color[gray]{0.9}% + \fi + \parindent\z@\parskip0.1\baselineskip + \if@ACM@authorversion\else + \if@printpermission\@copyrightpermission\par\fi + \fi + \if@ACM@manuscript\else + \if@ACM@journal@bibstrip\else % Print the conference information + {\itshape \acmConference@shortname, \acmConference@date, \acmConference@venue}\par + \fi + \fi + \if@printcopyright + \copyright\ \@copyrightyear\ \@copyrightowner\\ + \else + \@copyrightyear.\ + \fi + \if@ACM@manuscript + Manuscript submitted to ACM\\ + \else + \if@ACM@authorversion + This is the author's version of the work. It is posted here for + your personal use. Not for redistribution. The definitive Version + of Record was published in + \if@ACM@journal@bibstrip + \emph{\@journalName}% + \else + \emph{\@acmBooktitle}% + \fi + \ifx\@acmDOI\@empty + . + \else + , \@formatdoi{\@acmDOI}. + \fi\\ + \else + \if@ACM@nonacm\else + \if@ACM@journal@bibstrip + \@permissionCodeOne/\@acmYear/\@acmMonth-ART\@acmArticle + \ifx\@acmPrice\@empty\else\ \$\@acmPrice\fi\\ + \@formatdoi{\@acmDOI}% + \else % Conference + \ifx\@acmISBN\@empty\else ACM~ISBN~\@acmISBN + \ifx\@acmPrice\@empty.\else\dots\$\@acmPrice\fi\\\fi + \ifx\@acmDOI\@empty\else\@formatdoi{\@acmDOI}\fi% + \fi + \fi + \fi + \fi} + \fi + \endgroup + \setcounter{footnote}{0}% + \@mkabstract + \if@ACM@printccs + \ifx\@concepts\@empty\else\bgroup + {\@specialsection{CCS Concepts}% + \noindent\@concepts\par}\egroup + \fi + \fi + \ifx\@keywords\@empty\else\bgroup + {\if@ACM@journal + \@specialsection{Additional Key Words and Phrases}% + \else + \@specialsection{Keywords}% + \fi + \noindent\@keywords}\par\egroup + \fi + \andify\authors + \andify\shortauthors + \global\let\authors=\authors + \global\let\shortauthors=\shortauthors + \if@ACM@printacmref + \@mkbibcitation + \fi + \hypersetup{% + pdfauthor={\authors}, + pdftitle={\@title}, + pdfsubject={\@concepts}, + pdfkeywords={\@keywords}, + pdfcreator={LaTeX with acmart + \csname ver@acmart.cls\endcsname\space + and hyperref + \csname ver@hyperref.sty\endcsname}}% + \global\@topnum\z@ % this prevents floats from falling + % at the top of page 1 + \global\@botnum\z@ % we do not want them to be on the bottom either + \@printendtopmatter + \@afterindentfalse + \@afterheading +} +\def\@specialsection#1{% + \ifcase\ACM@format@nr + \relax % manuscript + \par\medskip\small\noindent#1: % + \or % acmsmall + \par\medskip\small\noindent#1: % + \or % acmlarge + \par\medskip\small\noindent#1: % + \or % acmtog + \par\medskip\small\noindent#1: % + \or % sigconf + \section*{#1}% + \or % siggraph + \section*{#1}% + \or % sigplan + \noindentparagraph*{#1:~}% + \or % sigchi + \section*{#1}% + \or % sigchi-a + \section*{#1}% + \fi +} +\def\@printtopmatter{% + \ifx\@startPage\@empty + \gdef\@startPage{1}% + \else + \setcounter{page}{\@startPage}% + \fi + \thispagestyle{firstpagestyle}% + \noindent + \ifcase\ACM@format@nr + \relax % manuscript + \box\mktitle@bx\par + \or % acmsmall + \box\mktitle@bx\par + \or % acmlarge + \box\mktitle@bx\par + \or % acmtog + \twocolumn[\box\mktitle@bx]% + \or % sigconf + \twocolumn[\box\mktitle@bx]% + \or % siggraph + \twocolumn[\box\mktitle@bx]% + \or % sigplan + \twocolumn[\box\mktitle@bx]% + \or % sigchi + \twocolumn[\box\mktitle@bx]% + \or % sigchi-a + \par\box\mktitle@bx\par\bigskip + \if@ACM@badge + \marginpar{\noindent + \ifx\@acmBadgeL@image\@empty\else + \href{\@acmBadgeL@url}{% + \includegraphics[width=\@ACM@badge@width]{\@acmBadgeL@image}}% + \hskip\@ACM@badge@skip + \fi + \ifx\@acmBadgeR@image\@empty\else + \href{\@acmBadgeR@url}{% + \includegraphics[width=\@ACM@badge@width]{\@acmBadgeR@image}}% + \fi}% + \fi + \fi +} +\def\@mktitle{% + \ifcase\ACM@format@nr + \relax % manuscript + \@mktitle@i + \or % acmsmall + \@mktitle@i + \or % acmlarge + \@mktitle@i + \or % acmtog + \@mktitle@i + \or % sigconf + \@mktitle@iii + \or % siggraph + \@mktitle@iii + \or % sigplan + \@mktitle@iii + \or % sigchi + \@mktitle@iii + \or % sigchi-a + \@mktitle@iv + \fi +} +\def\@titlefont{% + \ifcase\ACM@format@nr + \relax % manuscript + \LARGE\sffamily\bfseries + \or % acmsmall + \LARGE\sffamily\bfseries + \or % acmlarge + \LARGE\sffamily\bfseries + \or % acmtog + \Huge\sffamily + \or % sigconf + \Huge\sffamily\bfseries + \or % siggraph + \Huge\sffamily\bfseries + \or % sigplan + \Huge\bfseries + \or % sigchi + \Huge\sffamily\bfseries + \or % sigchi-a + \Huge\bfseries + \fi} +\def\@subtitlefont{\normalsize + \ifcase\ACM@format@nr + \relax % manuscript + \mdseries + \or % acmsmall + \mdseries + \or % acmlarge + \mdseries + \or % acmtog + \LARGE + \or % sigconf + \LARGE\mdseries + \or % siggraph + \LARGE\mdseries + \or % sigplan + \LARGE\mdseries + \or % sigchi + \LARGE\mdseries + \or % sigchi-a + \mdseries + \fi} +\def\@mktitle@i{\hsize=\textwidth + \@ACM@title@width=\hsize + \ifx\@acmBadgeL@image\@empty\else + \advance\@ACM@title@width by -\@ACM@badge@width + \advance\@ACM@title@width by -\@ACM@badge@skip + \fi + \ifx\@acmBadgeR@image\@empty\else + \advance\@ACM@title@width by -\@ACM@badge@width + \advance\@ACM@title@width by -\@ACM@badge@skip + \fi + \setbox\mktitle@bx=\vbox{\noindent\@titlefont + \ifx\@acmBadgeL@image\@empty\else + \raisebox{-.5\baselineskip}[\z@][\z@]{\href{\@acmBadgeL@url}{% + \includegraphics[width=\@ACM@badge@width]{\@acmBadgeL@image}}}% + \hskip\@ACM@badge@skip + \fi + \parbox[t]{\@ACM@title@width}{\raggedright + \@titlefont\noindent + \@title + \ifx\@subtitle\@empty\else + \par\noindent{\@subtitlefont\@subtitle} + \fi}% + \ifx\@acmBadgeR@image\@empty\else + \hskip\@ACM@badge@skip + \raisebox{-.5\baselineskip}[\z@][\z@]{\href{\@acmBadgeR@url}{% + \includegraphics[width=\@ACM@badge@width]{\@acmBadgeR@image}}}% + \fi + \par\bigskip}}% +\def\@mktitle@iii{\hsize=\textwidth + \setbox\mktitle@bx=\vbox{\@titlefont\centering + \@ACM@title@width=\hsize + \if@ACM@badge + \advance\@ACM@title@width by -2\@ACM@badge@width + \advance\@ACM@title@width by -2\@ACM@badge@skip + \parbox[b]{\@ACM@badge@width}{\strut + \ifx\@acmBadgeL@image\@empty\else + \raisebox{-.5\baselineskip}[\z@][\z@]{\href{\@acmBadgeL@url}{% + \includegraphics[width=\@ACM@badge@width]{\@acmBadgeL@image}}}% + \fi}% + \hskip\@ACM@badge@skip + \fi + \parbox[t]{\@ACM@title@width}{\centering\@titlefont + \@title + \ifx\@subtitle\@empty\else + \par\noindent{\@subtitlefont\@subtitle} + \fi + }% + \if@ACM@badge + \hskip\@ACM@badge@skip + \parbox[b]{\@ACM@badge@width}{\strut + \ifx\@acmBadgeR@image\@empty\else + \raisebox{-.5\baselineskip}[\z@][\z@]{\href{\@acmBadgeR@url}{% + \includegraphics[width=\@ACM@badge@width]{\@acmBadgeR@image}}}% + \fi}% + \fi + \par\bigskip}}% +\def\@mktitle@iv{\hsize=\textwidth + \setbox\mktitle@bx=\vbox{\raggedright\leftskip5pc\@titlefont + \noindent\leavevmode\leaders\hrule height 2pt\hfill\kern0pt\par + \noindent\@title + \ifx\@subtitle\@empty\else + \par\noindent\@subtitlefont\@subtitle + \fi + \par\bigskip}}% +\newbox\@ACM@commabox +\def\@ACM@addtoaddress#1{% + \ifvmode\else + \if@ACM@affiliation@obeypunctuation\else + \setbox\@ACM@commabox=\hbox{, }% + \unskip\cleaders\copy\@ACM@commabox\hskip\wd\@ACM@commabox + \fi\fi + #1} +\def\streetaddress#1{\unskip\ignorespaces} +\def\postcode#1{\unskip\ignorespaces} +\if@ACM@journal + \def\position#1{\unskip\ignorespaces} + \def\institution#1{\unskip~#1\ignorespaces} + \def\city#1{\unskip\ignorespaces} + \def\state#1{\unskip\ignorespaces} + \newcommand\department[2][0]{\unskip\ignorespaces} + \def\country#1{\if@ACM@affiliation@obeypunctuation\else, \fi#1\ignorespaces} +\else + \def\position#1{\if@ACM@affiliation@obeypunctuation#1\else#1\par\fi}% + \def\institution#1{\if@ACM@affiliation@obeypunctuation#1\else#1\par\fi}% + \newcommand\department[2][0]{\if@ACM@affiliation@obeypunctuation + #2\else#2\par\fi}% + \let\city\@ACM@addtoaddress + \let\state\@ACM@addtoaddress + \let\country\@ACM@addtoaddress +\fi +\def\@mkauthors{\begingroup + \hsize=\textwidth + \ifcase\ACM@format@nr + \relax % manuscript + \@mkauthors@i + \or % acmsmall + \@mkauthors@i + \or % acmlarge + \@mkauthors@i + \or % acmtog + \@mkauthors@i + \or % sigconf + \@mkauthors@iii + \or % siggraph + \@mkauthors@iii + \or % sigplan + \@mkauthors@iii + \or % sigchi + \@mkauthors@iii + \or % sigchi-a + \@mkauthors@iv + \fi + \endgroup +} +\def\@authorfont{\Large\sffamily} +\def\@affiliationfont{\normalsize\normalfont} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall + \def\@authorfont{\large\sffamily} + \def\@affiliationfont{\small\normalfont} +\or % acmlarge +\or % acmtog + \def\@authorfont{\LARGE\sffamily} + \def\@affiliationfont{\large} +\or % sigconf + \def\@authorfont{\LARGE} + \def\@affiliationfont{\large} +\or % siggraph + \def\@authorfont{\normalsize\normalfont} + \def\@affiliationfont{\normalsize\normalfont} +\or % sigplan + \def\@authorfont{\Large\normalfont} + \def\@affiliationfont{\normalsize\normalfont} +\or % sigchi + \def\@authorfont{\bfseries} + \def\@affiliationfont{\mdseries} +\or % sigchi-a + \def\@authorfont{\bfseries} + \def\@affiliationfont{\mdseries} +\fi +\def\@typeset@author@line{% + \andify\@currentauthors\par\noindent + \@currentauthors\def\@currentauthors{}% + \ifx\@currentaffiliations\@empty\else + \andify\@currentaffiliations + \unskip, {\@currentaffiliations}\par + \fi + \def\@currentaffiliations{}} +\def\@mkauthors@i{% + \def\@currentauthors{}% + \def\@currentaffiliations{}% + \global\let\and\@typeset@author@line + \def\@author##1{% + \ifx\@currentauthors\@empty + \gdef\@currentauthors{\@authorfont\MakeTextUppercase{##1}}% + \else + \g@addto@macro{\@currentauthors}{\and\MakeTextUppercase{##1}}% + \fi + \gdef\and{}}% + \def\email##1##2{}% + \def\affiliation##1##2{% + \def\@tempa{##2}\ifx\@tempa\@empty\else + \ifx\@currentaffiliations\@empty + \gdef\@currentaffiliations{% + \setkeys{@ACM@affiliation@}{obeypunctuation=false}% + \setkeys{@ACM@affiliation@}{##1}% + \@affiliationfont##2}% + \else + \g@addto@macro{\@currentaffiliations}{\and + \setkeys{@ACM@affiliation@}{obeypunctuation=false}% + \setkeys{@ACM@affiliation@}{##1}##2}% + \fi + \fi + \global\let\and\@typeset@author@line}% + \global\setbox\mktitle@bx=\vbox{\noindent\box\mktitle@bx\par\medskip + \noindent\addresses\@typeset@author@line + \par\medskip}% +} +\newbox\author@bx +\newdimen\author@bx@wd +\newskip\author@bx@sep +\author@bx@sep=1pc\relax +\def\@typeset@author@bx{\bgroup\hsize=\author@bx@wd + \def\and{\par}\normalbaselines + \global\setbox\author@bx=\vtop{\if@ACM@sigchiamode\else\centering\fi + \@authorfont\@currentauthors\par\@affiliationfont + \@currentaffiliation}\egroup + \box\author@bx\hspace{\author@bx@sep}% + \gdef\@currentauthors{}% + \gdef\@currentaffiliation{}} +\def\@mkauthors@iii{% + \author@bx@wd=\textwidth\relax + \advance\author@bx@wd by -\author@bx@sep\relax + \ifnum\@ACM@authorsperrow>0\relax + \divide\author@bx@wd by \@ACM@authorsperrow\relax + \else + \ifcase\num@authorgroups + \relax % 0? + \or % 1=one author per row + \or % 2=two authors per row + \divide\author@bx@wd by \num@authorgroups\relax + \or % 3=three authors per row + \divide\author@bx@wd by \num@authorgroups\relax + \or % 4=two authors per row (!) + \divide\author@bx@wd by 2\relax + \else % three authors per row + \divide\author@bx@wd by 3\relax + \fi + \fi + \advance\author@bx@wd by -\author@bx@sep\relax + \gdef\@currentauthors{}% + \gdef\@currentaffiliation{}% + \def\@author##1{\ifx\@currentauthors\@empty + \gdef\@currentauthors{\par##1}% + \else + \g@addto@macro\@currentauthors{\par##1}% + \fi + \gdef\and{}}% + \def\email##1##2{\ifx\@currentaffiliation\@empty + \gdef\@currentaffiliation{\bgroup + \mathchardef\UrlBreakPenalty=10000\nolinkurl{##2}\egroup}% + \else + \g@addto@macro\@currentaffiliation{\par\bgroup + \mathchardef\UrlBreakPenalty=10000\nolinkurl{##2}\egroup}% + \fi}% + \def\affiliation##1##2{\ifx\@currentaffiliation\@empty + \gdef\@currentaffiliation{% + \setkeys{@ACM@affiliation@}{obeypunctuation=false}% + \setkeys{@ACM@affiliation@}{##1}##2}% + \else + \g@addto@macro\@currentaffiliation{\par + \setkeys{@ACM@affiliation@}{obeypunctuation=false}% + \setkeys{@ACM@affiliation@}{##1}##2}% + \fi + \global\let\and\@typeset@author@bx +}% + \hsize=\textwidth + \global\setbox\mktitle@bx=\vbox{\noindent + \box\mktitle@bx\par\medskip\leavevmode + \lineskip=1pc\relax\centering\hspace*{-1em}% + \addresses\let\and\@typeset@author@bx\and\par\bigskip}} +\def\@mkauthors@iv{% + \author@bx@wd=\columnwidth\relax + \advance\author@bx@wd by -\author@bx@sep\relax + \ifnum\@ACM@authorsperrow>0\relax + \divide\author@bx@wd by \@ACM@authorsperrow\relax + \else + \ifcase\num@authorgroups + \relax % 0? + \or % 1=one author per row + \else % 2=two authors per row + \divide\author@bx@wd by 2\relax + \fi + \fi + \advance\author@bx@wd by -\author@bx@sep\relax + \gdef\@currentauthors{}% + \gdef\@currentaffiliation{}% + \def\@author##1{\ifx\@currentauthors\@empty + \gdef\@currentauthors{\par##1}% + \else + \g@addto@macro\@currentauthors{\par##1}% + \fi + \gdef\and{}}% + \def\email##1##2{\ifx\@currentaffiliation\@empty + \gdef\@currentaffiliation{\nolinkurl{##2}}% + \else + \g@addto@macro\@currentaffiliation{\par\nolinkurl{##2}}% + \fi}% + \def\affiliation##1##2{\ifx\@currentaffiliation\@empty + \gdef\@currentaffiliation{% + \setkeys{@ACM@affiliation@}{obeypunctuation=false}% + \setkeys{@ACM@affiliation@}{##1}##2}% + \else + \g@addto@macro\@currentaffiliation{\par + \setkeys{@ACM@affiliation@}{obeypunctuation=false}% + \setkeys{@ACM@affiliation@}{##1}##2}% + \fi + \global\let\and\@typeset@author@bx}% + \bgroup\hsize=\columnwidth + \par\raggedright\leftskip=\z@ + \lineskip=1pc\noindent + \addresses\let\and\@typeset@author@bx\and\par\bigskip\egroup} +\def\@mkauthorsaddresses{% + \ifnum\num@authors>1\relax + Authors' \else Author's \fi + \ifnum\num@authorgroups>1\relax + addresses: \else address: \fi + \bgroup + \def\streetaddress##1{\unskip, ##1}% + \def\postcode##1{\unskip, ##1}% + \def\position##1{\unskip\ignorespaces}% + \def\institution##1{\unskip, ##1}% + \def\city##1{\unskip, ##1}% + \def\state##1{\unskip, ##1}% + \renewcommand\department[2][0]{\unskip\@addpunct, ##2}% + \def\country##1{\unskip, ##1}% + \def\and{\unskip; }% + \def\@author##1{##1}% + \def\email##1##2{\unskip, \nolinkurl{##2}}% + \addresses + \egroup} +\AtEndDocument{\if@ACM@nonacm\else\if@ACM@journal + \ifx\@authorsaddresses\@empty + \ClassWarningNoLine{\@classname}{Authors' + addresses are mandatory for ACM journals}% + \fi\fi\fi} +\def\@setaddresses{} +\def\@authornotemark{\g@addto@macro\@currentauthors{\footnotemark\relax}} +\def\@@authornotemark#1{\g@addto@macro\@currentauthors{\footnotemark[#1]}} +\def\@mkteasers{% + \ifx\@teaserfigures\@empty\else + \def\@teaser##1{\par\bigskip\bgroup + \captionsetup{type=figure}##1\egroup\par} + \global\setbox\mktitle@bx=\vbox{\noindent\box\mktitle@bx\par + \noindent\@Description@presentfalse + \@teaserfigures\par\if@Description@present\else + \global\@undescribed@imagestrue + \ClassWarning{\@classname}{A possible image without + description}\fi + \medskip}% + \fi} +\def\@mkabstract{\bgroup + \ifx\@abstract\@lempty\else + {\phantomsection\addcontentsline{toc}{section}{Abstract}% + \if@ACM@journal + \everypar{\setbox\z@\lastbox\everypar{}}\small + \else + \section*{\abstractname}% + \fi + \ignorespaces\@abstract\par}% + \fi\egroup} +\def\@mkbibcitation{\bgroup + \let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig + \def\@pages@word{\ifnum\getrefnumber{TotPages}=1\relax page\else pages\fi}% + \def\footnotemark{}% + \def\\{\unskip{} \ignorespaces}% + \def\footnote{\ClassError{\@classname}{Please do not use footnotes + inside a \string\title{} or \string\author{} command! Use + \string\titlenote{} or \string\authornote{} instead!}}% + \def\@article@string{\ifx\@acmArticle\@empty{\ }\else, + Article~\@acmArticle\ \fi}% + \par\medskip\small\noindent{\bfseries ACM Reference Format:}\par\nobreak + \noindent\bgroup + \def\\{\unskip{}, \ignorespaces}\authors\egroup. \@acmYear. \@title + \ifx\@subtitle\@empty. \else: \@subtitle. \fi + \if@ACM@nonacm\else + % The 'nonacm' option disables 'printacmref' by default, + % and the present \@mkbibcitation definition is never used + % in this case. The conditional remains useful if the user + % explicitly sets \settopmatter{printacmref=true}. + \if@ACM@journal@bibstrip + \textit{\@journalNameShort} + \@acmVolume, \@acmNumber \@article@string (\@acmPubDate), + \ref{TotPages}~\@pages@word. + \else + In \textit{\@acmBooktitle}% + \ifx\@acmEditors\@empty\textit{.}\else + \andify\@acmEditors\textit{, }\@acmEditors~\@editorsAbbrev.% + \fi\ + ACM, New York, NY, USA% + \@article@string\unskip, \ref{TotPages}~\@pages@word. + \fi + \fi + \ifx\@acmDOI\@empty\else\@formatdoi{\@acmDOI}\fi +\par\egroup} +\def\@printendtopmatter{% + \let\@vspace\@vspace@orig + \let\@vspacer\@vspacer@orig + \par\bigskip + \let\@vspace\@vspace@acm + \let\@vspacer\@vspacer@acm + } +\def\@setthanks{\long\def\thanks##1{\par##1\@addpunct.}\thankses} +\def\@setauthorsaddresses{\@authorsaddresses\unskip\@addpunct.} +\RequirePackage{fancyhdr} +\let\ACM@ps@plain\ps@plain +\let\ACM@ps@myheadings\ps@myheadings +\let\ACM@ps@headings\ps@headings +\def\ACM@restore@pagestyle{% + \let\ps@plain\ACM@ps@plain + \let\ps@myheadings\ACM@ps@myheadings + \let\ps@headings\ACM@ps@headings} +\AtBeginDocument{\ACM@restore@pagestyle} +\if@ACM@review + \newsavebox{\ACM@linecount@bx} + \newlength\ACM@linecount@bxht + \newcount\ACM@linecount + \ACM@linecount\@ne\relax + \def\ACM@mk@linecount{% + \savebox{\ACM@linecount@bx}[4em][t]{\parbox[t]{4em}{\normalfont + \normalsize + \setlength{\ACM@linecount@bxht}{0pt}% + \loop{\color{red}\scriptsize\the\ACM@linecount}\\ + \global\advance\ACM@linecount by \@ne + \addtolength{\ACM@linecount@bxht}{\baselineskip}% + \ifdim\ACM@linecount@bxht<\textheight\repeat + {\color{red}\scriptsize\the\ACM@linecount}\hfill + \global\advance\ACM@linecount by \@ne}}} +\fi +\def\ACM@linecountL{% + \if@ACM@review + \ACM@mk@linecount + \begin{picture}(0,0)% + \put(-26,-22){\usebox{\ACM@linecount@bx}}% + \end{picture}% + \fi} +\def\ACM@linecountR{% + \if@ACM@review + \ifcase\ACM@format@nr + \relax % manuscript + \relax + \or % acmsmall + \relax + \or % acmlarge + \relax + \or % acmtog + \ACM@mk@linecount + \or % sigconf + \ACM@mk@linecount + \or % siggraph + \ACM@mk@linecount + \or % sigplan + \ACM@mk@linecount + \or % sigchi + \ACM@mk@linecount + \or % sigchi-a + \ACM@mk@linecount + \fi + \begin{picture}(0,0)% + \put(20,-22){\usebox{\ACM@linecount@bx}}% + \end{picture}% + \fi} +\if@ACM@timestamp + % Subtracting 30 from \time gives us the effect of rounding down despite + % \numexpr rounding to nearest + \newcounter{ACM@time@hours} + \setcounter{ACM@time@hours}{\numexpr (\time - 30) / 60 \relax} + \newcounter{ACM@time@minutes} + \setcounter{ACM@time@minutes}{\numexpr \time - \theACM@time@hours * 60 \relax} + \newcommand\ACM@timestamp{% + \footnotesize% + \ifx\@acmSubmissionID\@empty\relax\else + Submission ID: \@acmSubmissionID.{ }% + \fi + \the\year-\two@digits{\the\month}-\two@digits{\the\day}{ }% + \two@digits{\theACM@time@hours}:\two@digits{\theACM@time@minutes}{. }% + Page \thepage\ of \@startPage--\pageref*{TotPages}.% + } +\fi +\def\@shortauthors{% + \if@ACM@anonymous + Anon. + \ifx\@acmSubmissionID\@empty\else Submission Id: \@acmSubmissionID\fi + \else\shortauthors\fi} +\def\@headfootfont{\sffamily\footnotesize} +\AtBeginDocument{% +\fancypagestyle{standardpagestyle}{% + \fancyhf{}% + \renewcommand{\headrulewidth}{\z@}% + \renewcommand{\footrulewidth}{\z@}% + \def\@acmArticlePage{% + \ifx\@acmArticle\empty% + \if@ACM@printfolios\thepage\fi% + \else% + \@acmArticle\if@ACM@printfolios:\thepage\fi% + \fi% + }% + \if@ACM@journal@bibstrip + \ifcase\ACM@format@nr + \relax % manuscript + \fancyhead[LE]{\ACM@linecountL\if@ACM@printfolios\thepage\fi}% + \fancyhead[RO]{\if@ACM@printfolios\thepage\fi}% + \fancyhead[RE]{\@shortauthors}% + \fancyhead[LO]{\ACM@linecountL\shorttitle}% + \if@ACM@nonacm\else% + \fancyfoot[RO,LE]{\footnotesize Manuscript submitted to ACM} + \fi% + \or % acmsmall + \fancyhead[LE]{\ACM@linecountL\@headfootfont\@acmArticlePage}% + \fancyhead[RO]{\@headfootfont\@acmArticlePage}% + \fancyhead[RE]{\@headfootfont\@shortauthors}% + \fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}% + \if@ACM@nonacm\else% + \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No. + \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}% + \fi + \or % acmlarge + \fancyhead[LE]{\ACM@linecountL\@headfootfont + \@acmArticlePage\quad\textbullet\quad\@shortauthors}% + \fancyhead[LO]{\ACM@linecountL}% + \fancyhead[RO]{\@headfootfont + \shorttitle\quad\textbullet\quad\@acmArticlePage}% + \if@ACM@nonacm\else% + \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No. + \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}% + \fi + \or % acmtog + \fancyhead[LE]{\ACM@linecountL\@headfootfont + \@acmArticlePage\quad\textbullet\quad\@shortauthors}% + \fancyhead[LO]{\ACM@linecountL}% + \fancyhead[RE]{\ACM@linecountR}% + \fancyhead[RO]{\@headfootfont + \shorttitle\quad\textbullet\quad\@acmArticlePage\ACM@linecountR}% + \if@ACM@nonacm\else% + \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No. + \@acmNumber, Article \@acmArticle. Publication date: \@acmPubDate.}% + \fi + \else % Proceedings + \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}% + \fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}% + \fancyhead[RE]{\@headfootfont\@shortauthors\ACM@linecountR}% + \if@ACM@nonacm\else% + \fancyhead[LE]{\ACM@linecountL\@headfootfont\footnotesize + \acmConference@shortname, + \acmConference@date, \acmConference@venue}% + \fancyhead[RO]{\@headfootfont + \acmConference@shortname, + \acmConference@date, \acmConference@venue\ACM@linecountR}% + \fi + \fi + \else % Proceedings + \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}% + \fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}% + \fancyhead[RE]{\@headfootfont\@shortauthors\ACM@linecountR}% + \if@ACM@nonacm\else% + \fancyhead[LE]{\ACM@linecountL\@headfootfont + \acmConference@shortname, + \acmConference@date, \acmConference@venue}% + \fancyhead[RO]{\@headfootfont + \acmConference@shortname, + \acmConference@date, \acmConference@venue\ACM@linecountR}% + \fi + \fi + \if@ACM@sigchiamode + \fancyheadoffset[L]{\dimexpr(\marginparsep+\marginparwidth)}% + \fi + \if@ACM@timestamp + \fancyfoot[LO,RE]{\ACM@timestamp} + \fi +}% +\pagestyle{standardpagestyle} +} +\newdimen\@folio@wd +\@folio@wd=\z@ +\newdimen\@folio@ht +\@folio@ht=\z@ +\newdimen\@folio@voffset +\@folio@voffset=\z@ +\def\@folio@max{1} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall + \@folio@wd=45.75pt\relax + \@folio@ht=1.25in\relax + \@folio@voffset=.2in\relax + \def\@folio@max{8} +\or % acmlarge + \@folio@wd=43.25pt\relax + \@folio@ht=79pt\relax + \@folio@voffset=.55in\relax + \def\@folio@max{10} +\fi +\def\@folioblob{\@tempcnta=0\@acmArticleSeq\relax + \ifnum\@tempcnta=0\relax\else + \loop + \ifnum\@tempcnta>\@folio@max\relax + \advance\@tempcnta by - \@folio@max + \repeat + \advance\@tempcnta by -1\relax + \@tempdima=\@folio@ht\relax + \multiply\@tempdima by \the\@tempcnta\relax + \advance\@tempdima by -\@folio@voffset\relax + \begin{picture}(0,0) + \makebox[\z@]{\raisebox{-\@tempdima}{% + \rlap{% + \raisebox{-0.45\@folio@ht}[\z@][\z@]{% + \rule{\@folio@wd}{\@folio@ht}}}% + \parbox{\@folio@wd}{% + \centering + \textcolor{white}{\LARGE\sffamily\bfseries\@acmArticle}}}} + \end{picture}\fi} + +\AtBeginDocument{% +\fancypagestyle{firstpagestyle}{% + \fancyhf{}% + \renewcommand{\headrulewidth}{\z@}% + \renewcommand{\footrulewidth}{\z@}% + \if@ACM@journal@bibstrip + \ifcase\ACM@format@nr + \relax % manuscript + \fancyhead[L]{\ACM@linecountL}% + \fancyfoot[RO,LE]{\if@ACM@printfolios\small\thepage\fi}% + \if@ACM@nonacm\else% + \fancyfoot[RE,LO]{\footnotesize Manuscript submitted to ACM}% + \fi% + \or % acmsmall + \if@ACM@nonacm\else% + \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No. + \@acmNumber, Article \@acmArticle. Publication date: + \@acmPubDate.}% + \fi% + \fancyhead[LE]{\ACM@linecountL\@folioblob}% + \fancyhead[LO]{\ACM@linecountL}% + \fancyhead[RO]{\@folioblob}% + \fancyheadoffset[RO,LE]{0.6\@folio@wd}% + \or % acmlarge + \if@ACM@nonacm\else% + \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No. + \@acmNumber, Article \@acmArticle. Publication date: + \@acmPubDate.}% + \fi% + \fancyhead[RO]{\@folioblob}% + \fancyhead[LE]{\ACM@linecountL\@folioblob}% + \fancyhead[LO]{\ACM@linecountL}% + \fancyheadoffset[RO,LE]{1.4\@folio@wd}% + \or % acmtog + \if@ACM@nonacm\else% + \fancyfoot[RO,LE]{\footnotesize \@journalNameShort, Vol. \@acmVolume, No. + \@acmNumber, Article \@acmArticle. Publication date: + \@acmPubDate.}% + \fi% + \fancyhead[L]{\ACM@linecountL}% + \fancyhead[R]{\ACM@linecountR}% + \else % Conference proceedings + \fancyhead[L]{\ACM@linecountL}% + \fancyhead[R]{\ACM@linecountR}% + \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}% + \fi + \else + \fancyhead[L]{\ACM@linecountL}% + \fancyhead[R]{\ACM@linecountR}% + \fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}% + \fi + \if@ACM@timestamp + \ifnum\ACM@format@nr=0\relax % Manuscript + \fancyfoot[LO,RE]{\ACM@timestamp\quad + \if@ACM@nonacm\else + \footnotesize Manuscript submitted to ACM + \fi} + \else + \fancyfoot[LO,RE]{\ACM@timestamp} + \fi + \fi +}} +\def\ACM@NRadjust#1{% + \begingroup + \expandafter\ifx\csname Sectionformat\endcsname\relax + % do nothing when \Sectionformat is unknown + \def\next{\endgroup #1}% + \else + \def\next{\endgroup + \let\realSectionformat\Sectionformat + \def\ACM@sect@format@{#1}% + \let\Sectionformat\ACM@NR@adjustedSectionformat + %% next lines added 2018-06-17 to ensure section number is styled + \let\real@adddotafter\@adddotafter + \let\@adddotafter\ACM@adddotafter + #1{}% imposes the styles, but nullifies \MakeUppercase + \let\@adddotafter\real@adddotafter + }% + \fi \next +} +\def\ACM@NR@adjustedSectionformat#1#2{% + \realSectionformat{\ACM@sect@format{#1}}{#2}% + \let\Sectionformat\realSectionformat} +\DeclareRobustCommand{\ACM@sect@format}{\ACM@sect@format@} +\def\ACM@sect@format@null#1{#1} +\let\ACM@sect@format@\ACM@sect@format@null +\AtBeginDocument{% + \expandafter\ifx\csname LTX@adddotafter\endcsname\relax + \let\LTX@adddotafter\@adddotafter + \fi +} +\def\ACM@adddotafter#1{\ifx\relax#1\relax\else\LTX@adddotafter{#1}\fi} +\renewcommand\section{\@startsection{section}{1}{\z@}% + {-.75\baselineskip \@plus -2\p@ \@minus -.2\p@}% + {.25\baselineskip}% + {\ACM@NRadjust\@secfont}} +\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% + {-.75\baselineskip \@plus -2\p@ \@minus -.2\p@}% + {.25\baselineskip}% + {\ACM@NRadjust\@subsecfont}} +\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% + {-.5\baselineskip \@plus -2\p@ \@minus -.2\p@}% + {-3.5\p@}% + {\ACM@NRadjust{\@subsubsecfont\@adddotafter}}} +\renewcommand\paragraph{\@startsection{paragraph}{4}{\parindent}% + {-.5\baselineskip \@plus -2\p@ \@minus -.2\p@}% + {-3.5\p@}% + {\ACM@NRadjust{\@parfont\@adddotafter}}} +\newcommand\noindentparagraph{\@startsection{paragraph}{4}{\z@}% + {-.5\baselineskip \@plus -2\p@ \@minus -.2\p@}% + {-3.5\p@}% + {\ACM@NRadjust{\@parfont}}} + +\renewcommand\part{\@startsection{part}{9}{\z@}% + {-10\p@ \@plus -4\p@ \@minus -2\p@}% + {4\p@}% + {\ACM@NRadjust\@parfont}} +\def\section@raggedright{\@rightskip\@flushglue + \rightskip\@rightskip + \leftskip\z@skip + \parindent\z@} +\def\@secfont{\sffamily\bfseries\section@raggedright\MakeTextUppercase} +\def\@subsecfont{\sffamily\bfseries\section@raggedright} +\def\@subsubsecfont{\sffamily\itshape} +\def\@parfont{\itshape} +\setcounter{secnumdepth}{3} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge + \def\@secfont{\sffamily\large\section@raggedright\MakeTextUppercase} + \def\@subsecfont{\sffamily\large\section@raggedright} +\or % acmtog + \def\@secfont{\sffamily\large\section@raggedright\MakeTextUppercase} + \def\@subsecfont{\sffamily\large\section@raggedright} +\or % sigconf + \def\@secfont{\bfseries\Large\section@raggedright\MakeTextUppercase} + \def\@subsecfont{\bfseries\Large\section@raggedright} +\or % siggraph + \def\@secfont{\sffamily\bfseries\Large\section@raggedright\MakeTextUppercase} + \def\@subsecfont{\sffamily\bfseries\Large\section@raggedright} +\or % sigplan + \def\@secfont{\bfseries\Large\section@raggedright} + \def\@subsecfont{\bfseries\section@raggedright} + \def\@subsubsecfont{\bfseries\section@raggedright} + \def\@parfont{\bfseries\itshape} + \def\@subparfont{\itshape} +\or % sigchi + \setcounter{secnumdepth}{1} + \def\@secfont{\sffamily\bfseries\section@raggedright\MakeTextUppercase} + \def\@subsecfont{\sffamily\bfseries\section@raggedright} +\or % sigchi-a + \setcounter{secnumdepth}{0} + \def\@secfont{\sffamily\bfseries\section@raggedright\MakeTextUppercase} + \def\@subsecfont{\sffamily\bfseries\section@raggedright} +\fi +\def\@adddotafter#1{#1\@addpunct{.}} +\def\@addspaceafter#1{#1\@addpunct{\enspace}} +\providecommand*\@dotsep{4.5} +\def\@acmplainbodyfont{\itshape} +\def\@acmplainindent{\parindent} +\def\@acmplainheadfont{\scshape} +\def\@acmplainnotefont{\@empty} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge +\or % acmtog +\or % sigconf +\or % siggraph +\or % sigplan + \def\@acmplainbodyfont{\itshape} + \def\@acmplainindent{\z@} + \def\@acmplainheadfont{\bfseries} + \def\@acmplainnotefont{\normalfont} +\or % sigchi +\or % sigchi-a +\fi +\newtheoremstyle{acmplain}% + {.5\baselineskip\@plus.2\baselineskip + \@minus.2\baselineskip}% space above + {.5\baselineskip\@plus.2\baselineskip + \@minus.2\baselineskip}% space below + {\@acmplainbodyfont}% body font + {\@acmplainindent}% indent amount + {\@acmplainheadfont}% head font + {.}% punctuation after head + {.5em}% spacing after head + {\thmname{#1}\thmnumber{ #2}\thmnote{ {\@acmplainnotefont(#3)}}}% head spec +\def\@acmdefinitionbodyfont{\normalfont} +\def\@acmdefinitionindent{\parindent} +\def\@acmdefinitionheadfont{\itshape} +\def\@acmdefinitionnotefont{\@empty} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge +\or % acmtog +\or % sigconf +\or % siggraph +\or % sigplan + \def\@acmdefinitionbodyfont{\normalfont} + \def\@acmdefinitionindent{\z@} + \def\@acmdefinitionheadfont{\bfseries} + \def\@acmdefinitionnotefont{\normalfont} +\or % sigchi +\or % sigchi-a +\fi +\newtheoremstyle{acmdefinition}% + {.5\baselineskip\@plus.2\baselineskip + \@minus.2\baselineskip}% space above + {.5\baselineskip\@plus.2\baselineskip + \@minus.2\baselineskip}% space below + {\@acmdefinitionbodyfont}% body font + {\@acmdefinitionindent}% indent amount + {\@acmdefinitionheadfont}% head font + {.}% punctuation after head + {.5em}% spacing after head + {\thmname{#1}\thmnumber{ #2}\thmnote{ {\@acmdefinitionnotefont(#3)}}}% head spec +\theoremstyle{acmplain} +\AtEndPreamble{% + \if@ACM@acmthm + \theoremstyle{acmplain} + \@ifundefined{theorem}{% + \newtheorem{theorem}{Theorem}[section] + }{} + \@ifundefined{conjecture}{% + \newtheorem{conjecture}[theorem]{Conjecture} + }{} + \@ifundefined{proposition}{% + \newtheorem{proposition}[theorem]{Proposition} + }{} + \@ifundefined{lemma}{% + \newtheorem{lemma}[theorem]{Lemma} + }{} + \@ifundefined{corollary}{% + \newtheorem{corollary}[theorem]{Corollary} + }{} + \theoremstyle{acmdefinition} + \@ifundefined{example}{% + \newtheorem{example}[theorem]{Example} + }{} + \@ifundefined{definition}{% + \newtheorem{definition}[theorem]{Definition} + }{} + \fi + \theoremstyle{acmplain} +} +\def\@proofnamefont{\scshape} +\def\@proofindent{\indent} +\ifcase\ACM@format@nr +\relax % manuscript +\or % acmsmall +\or % acmlarge +\or % acmtog +\or % sigconf +\or % siggraph +\or % sigplan + \def\@proofnamefont{\itshape} + \def\@proofindent{\noindent} +\or % sigchi +\or % sigchi-a +\fi +\renewenvironment{proof}[1][\proofname]{\par + \pushQED{\qed}% + \normalfont \topsep6\p@\@plus6\p@\relax + \trivlist + \item[\@proofindent\hskip\labelsep + {\@proofnamefont #1\@addpunct{.}}]\ignorespaces +}{% + \popQED\endtrivlist\@endpefalse +} +\AtEndPreamble{% + \if@ACM@balance + \ifcase\ACM@format@nr + \relax % manuscript + \global\@ACM@balancefalse + \or % acmsmall + \global\@ACM@balancefalse + \or % acmlarge + \global\@ACM@balancefalse + \or % acmtog + \RequirePackage{balance}% + \or % sigconf + \RequirePackage{balance}% + \or % siggraph + \RequirePackage{balance}% + \or % sigplan + \RequirePackage{balance}% + \or % sigchi + \RequirePackage{balance}% + \or % sigchi-a + \global\@ACM@balancefalse + \fi + \fi +} +\AtEndDocument{% + \if@ACM@balance + \if@twocolumn + \balance + \fi\fi} +\newcommand\acksname{Acknowledgments} +\specialcomment{acks}{% + \begingroup + \section*{\acksname} + \phantomsection\addcontentsline{toc}{section}{\acksname} +}{% + \endgroup +} +\def\grantsponsor#1#2#3{#2} +\newcommand\grantnum[3][]{#3% + \def\@tempa{#1}\ifx\@tempa\@empty\else\space(\url{#1})\fi} +\AtEndPreamble{% +\if@ACM@screen + \includecomment{screenonly} + \excludecomment{printonly} +\else + \excludecomment{screenonly} + \includecomment{printonly} +\fi +\if@ACM@anonymous + \excludecomment{anonsuppress} + \excludecomment{acks} +\else + \includecomment{anonsuppress} +\fi} +\newcommand\showeprint[2][arxiv]{% + \def\@tempa{#1}% + \ifx\@tempa\@empty\def\@tempa{arxiv}\fi + \def\@tempb{arxiv}% + \ifx\@tempa\@tempb + arXiv:\href{https://arxiv.org/abs/#2}{#2}\else arXiv:#2% + \fi} +\let\@vspace@orig=\@vspace +\let\@vspacer@orig=\@vspacer +\apptocmd{\@vspace}{\ClassWarning{\@classname}{\string\vspace\space should + only be used to provide space above/below surrounding + objects}}{}{} +\apptocmd{\@vspacer}{\ClassWarning{\@classname}{\string\vspace\space should + only be used to provide space above/below surrounding + objects}}{}{} +\let\@vspace@acm=\@vspace +\let\@vspacer@acm=\@vspacer +\let\ACM@origbaselinestretch\baselinestretch +\AtEndDocument{\ifx\baselinestretch\ACM@origbaselinestretch\else + \ClassError{\@classname}{An attempt to redefine + \string\baselinestretch\space detected. Please do not do this for + ACM submissions!}\fi} +\normalsize\normalfont\frenchspacing +\endinput +%% +%% End of file `acmart.cls'. diff --git a/spec/default.nix b/spec/default.nix new file mode 100644 index 00000000000..1130baae567 --- /dev/null +++ b/spec/default.nix @@ -0,0 +1,15 @@ +{ pkgs }: + +pkgs.stdenvNoCC.mkDerivation rec { + name = "hydra-spec"; + src = ./.; + buildInputs = [ + pkgs.texlive.combined.scheme-full + ]; + phases = [ "unpackPhase" "buildPhase" ]; + buildPhase = '' + latexmk -pdf ${./main.tex} + mkdir -p $out + mv *-main.pdf $out/${name}.pdf + ''; +} diff --git a/spec/fig_SM_states_basic.tex b/spec/fig_SM_states_basic.tex new file mode 100644 index 00000000000..e60fb8fe6cc --- /dev/null +++ b/spec/fig_SM_states_basic.tex @@ -0,0 +1,24 @@ +\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 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: diff --git a/spec/fig_offchain_prot.tex b/spec/fig_offchain_prot.tex new file mode 100644 index 00000000000..944278f4730 --- /dev/null +++ b/spec/fig_offchain_prot.tex @@ -0,0 +1,229 @@ +\begin{figure*}[t!] + + \def\sfact{0.8} + \centering + \begin{algobox}{Coordinated Hydra Head} + \medskip + \begin{tabular}{c} + %%% Initializing the head + \begin{tabular}{cc} + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.6} + %%% INIT + \On{$(\hpInit)$ from client}{ + $n \gets |\hydraKeys^{setup}|$ \; + $\hydraKeysAgg \gets \msCombVK(\hydraKeys^{setup})$ \; + $\cardanoKeys \gets \cardanoKeys^{setup}$\; + $\cPer \gets \cPer^{setup}$ \; + $\PostTx{}~(\mtxInit, \nop, \hydraKeysAgg,\cardanoKeys,\cPer)$ \; + } + \vspace{12pt} + + \On{$(\gcChainInitial, \cid, \seed, \nop, \hydraKeysAgg, \cardanoKeys^{\#}, \cPer)$ from chain}{ + \Req{} $\hydraKeysAgg=\msCombVK(\hydraKeys^{setup})$\; + \Req{} $\cardanoKeys^{\#}= [ \hash(k)~|~\forall k \in \cardanoKeys^{setup}]$\; + \Req{} $\cPer=\cPer^{setup}$\; + \Req{} $\cid = \hash(\muHead(\seed))$ \; + } + \end{walgo} + } + & + + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.6} + \On{$(\gcChainCommit, j, U)$ from chain}{ + $C_j \gets U $ + + \If{$\forall k \in [1..n]: C_k \neq \undefined$}{ + $\eta \gets \combine([C_1 \dots C_n])$ \; + $\PostTx{}~(\mtxCCom, \eta)$ \; + } + } + + \vspace{12pt} + + \On{$(\gcChainCollectCom, \eta_{0})$ from chain}{ + % Implictly means that all commits will defined as we cannot miss a commit (by assumption) + $\Uinit \gets \bigcup_{j=1}^{n} U_j$ \; + % $\Out~(\hpSnap,(0,U_0))$ \; + $\hatmL \gets \Uinit$ \; + $\bar{\mc S} \gets \blue{\Sno(0, 0, \Uinit, \emptyset, \bot)}$ \; + $\hatv, \hats \gets 0$ \; + $\hatmT \gets \emptyset$ \; + $\tx_{\omega} \gets \bot$ \; + } + + \end{walgo} + } + \end{tabular} + + \\ + \multicolumn{1}{l}{\line(1,0){490}} + \\ + + %%% Open head + \begin{tabular}{c@{}c} + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.65} + + %%% REQ TX + \On{$(\hpRT,\tx)$ from $\party_j$}{ + \Wait{$\hatmL \applytx \tx \neq \bot$}{ + $\hatmL \gets \hatmL\applytx\tx$ \; + $\hatmT \gets \hatmT \cup \{\tx\}$ \; + % issue snapshot if we are leader + \If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{ + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT, \tx_{\omega})$ \; + } + } + } + + \vspace{12pt} + + %%% REQ SN + \On{$(\hpRS,v,s,\mT_{\mathsf{req}}, \tx_{\omega})$ from $\party_j$}{ + \Req{$v = \hatv ~ \land ~ s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; + \Wait{$\hats = \bar{\mc S}.s$}{ + \Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$} \; + $U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \tx_{\omega} \setminus \mathsf{outputs(\tx_{\omega})}$ \; + \Req{$U_{\mathsf{active}} \applytx \mT_{\mathsf{req}} \not= \bot$} \; + $U \gets U_{\mathsf{active}} \applytx \mT_{\mathsf{req}}$ \; + $\hats \gets s$ \; + % TODO: DRY message creation + $\eta \gets \combine(U)$ \; + % TODO: handwavy combine/outputs here + $\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))$ \; + % NOTE: WE could make included transactions auditable by adding + % a merkle tree root to the (signed) snapshot data \eta + $\msSig_i \gets \msSign(\hydraSigningKey, (\cid || v || \hats || \eta || \eta_{\omega}))$ \; + $\hatSigma \gets \emptyset$ \; + $\Multi{}~(\hpAS,\hats,\msSig_i)$ \; + $\forall \tx \in \mT_{\mathsf{req}}: \Out~(\hpSeen,\tx)$ \; + % TODO: Should we inform users if we drop a transaction? + % XXX: This is a bit verbose for the spec + $\hatmL \gets U$ \; + $X\gets\hatmT$ \; + $\hatmT\gets\emptyset$ \; + \For{$\tx\in X : \hatmL\applytx \tx \not=\bot$}{ + $\hatmT\gets\hatmT\cup\{\tx\}$ \; + $\hatmL\gets\hatmL\applytx \tx$ \; + } + } + } + \end{walgo} + } & + + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.7} + %%% REC DEC + \On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{ + \Wait{$\tx_\omega = \bot ~ \land ~ \hatmL \applytx \tx \not= \bot$}{ + $\hatmL \gets \hatmL \applytx \tx \setminus \mathsf{outputs}(\tx)$ \; + $\tx_\omega \gets \tx$ \; + % issue snapshot if we are leader + \If{$\hats = \bar{\mc S}.s \land \hpLdr(\bar{\mc S}.s + 1) = i$}{ + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1,\hatmT, \tx_{\omega})$ \; + } + } + } + + \vspace{12pt} + + %%% DECREMENT + \On{$(\mathtt{decrementTx}, U_{\omega}, v)$ from chain}{ + \If{$\mathsf{outputs}(\tx_{\omega}) = U_{\omega}$}{ + $\tx_{\omega} \gets \bot$ \; + $\hatv \gets v$ \; + } + } + + \vspace{12pt} + + %%% ACK SN + \On{$(\hpAS,s,\msSig_j)$ from $\party_j$}{ + \Req{} $s \in \{\hats,\hats+1\}$ \; + \Wait{$\hats=s$}{ + \Req{} $(j, \cdot) \notin \hatSigma$ \; + $\hatSigma[j] \gets \sigma_{j}$ \; + \If{$\forall k \in [1..n]: (k,\cdot) \in \hatSigma$}{ + % TODO: MS-ASig used different than in the preliminaries + $\msCSig \gets \msComb(\hydraKeys^{setup}, \hatSigma)$ \; + + % TODO: DRY message creation + $\eta \gets \combine(\hatmU)$ \; + $\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))$ \; + + % NOTE: Implementation differs here and + % below as it stores seen version in seen + % snapshot and uses that to verify + \Req{} $\msVfy(\hydraKeysAgg, (\cid || \blue{\hatv ||} \hats || \eta || \eta_{\omega}), \msCSig)$ \; + % create confirmed snapshot for later reference + \blue{$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT , \tx_{\omega})$ \;} + $\bar{\mc S}.\sigma \gets \msCSig$ \; + + %$\Out~(\hpSnap,(\bar{\mc S}.s,\bar{\mc S}.U))$ \; + $\forall \tx \in \mT_{\mathsf{req}} : \Out (\hpConf,\tx)$ \; + \If{${\bar S}.\tx_{\omega} \ne \bot$}{ + $\PostTx{}~(\mtxDecrement, \hatv, \hats, \eta, \eta_{\omega})$ \; + % NOTE: Needed for security? + \blue{$\Out (\hpConf,\tx_{\omega})$ \;} + } + % issue snapshot if we are leader + \If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{ + \Multi{} $(\hpRS,\hatv,\bar{\mc S}.s+1, \hatmT, \tx_{\omega})$ \; + } + } + } + } + \end{walgo} + } + \end{tabular} + + \\ + \multicolumn{1}{l}{\line(1,0){490}} + \\ + + %%% Closing the head + \begin{tabular}{c c} + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.6} + % CLOSE from client + \On{$(\hpClose)$ from client}{ + $\eta \gets \combine(\bar{\mc S}.U)$ \; + $\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \; + $\xi \gets \bar{\mc S}.\sigma$ \; + % XXX: \hatv needed to distinguish between CloseType redeemer, explain how exactly? + $\PostTx{}~(\mtxClose, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta, \eta_{\omega}, \xi)$ \; + } + \end{walgo} + } + & + \adjustbox{valign=t,scale=\sfact}{ + \begin{walgo}{0.6} + \On{$(\gcChainClose, \eta) \lor (\gcChainContest, s_{c}, \eta)$ from chain}{ + \If{$\bar{\mc S}.s > s_{c}$}{ + $\eta \gets \combine(\bar{\mc S}.U)$ \; + $\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \; + $\xi \gets \bar{\mc S}.\sigma$ \; + % XXX: \hatv needed to distinguish between CloseType redeemer, explain how exactly? + $\PostTx{}~(\mtxContest, \hatv, \bar{\mc S}.v, \bar{\mc S}.s, \eta, \eta_{\omega}, \xi)$ \; + } + } + \end{walgo} + } + \end{tabular} + \end{tabular} + \bigskip + \end{algobox} + + \caption{Head-protocol machine for the \emph{coordinated head} from the perspective of party $\party_i$.}\label{fig:off-chain-prot} + + +\end{figure*} + + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/spec/figures/SM-abort.pdf b/spec/figures/SM-abort.pdf new file mode 100644 index 00000000000..71fe0e056f4 Binary files /dev/null and b/spec/figures/SM-abort.pdf differ diff --git a/spec/figures/SM-close.pdf b/spec/figures/SM-close.pdf new file mode 100644 index 00000000000..93eb89f2f8f Binary files /dev/null and b/spec/figures/SM-close.pdf differ diff --git a/spec/figures/SM-collect.pdf b/spec/figures/SM-collect.pdf new file mode 100644 index 00000000000..5d069520ab0 Binary files /dev/null and b/spec/figures/SM-collect.pdf differ diff --git a/spec/figures/SM-contest.pdf b/spec/figures/SM-contest.pdf new file mode 100644 index 00000000000..2476ba8d7e5 Binary files /dev/null and b/spec/figures/SM-contest.pdf differ diff --git a/spec/figures/SM-fanout.pdf b/spec/figures/SM-fanout.pdf new file mode 100644 index 00000000000..f6d28a24f28 Binary files /dev/null and b/spec/figures/SM-fanout.pdf differ diff --git a/spec/figures/SM-init-commit.pdf b/spec/figures/SM-init-commit.pdf new file mode 100644 index 00000000000..7ca2c4b8a68 Binary files /dev/null and b/spec/figures/SM-init-commit.pdf differ diff --git a/spec/figures/abortTx.pdf b/spec/figures/abortTx.pdf new file mode 100644 index 00000000000..3846492866d Binary files /dev/null and b/spec/figures/abortTx.pdf differ diff --git a/spec/figures/closeTx.pdf b/spec/figures/closeTx.pdf new file mode 100644 index 00000000000..123f79def42 Binary files /dev/null and b/spec/figures/closeTx.pdf differ diff --git a/spec/figures/collectComTx.pdf b/spec/figures/collectComTx.pdf new file mode 100644 index 00000000000..87b71129219 Binary files /dev/null and b/spec/figures/collectComTx.pdf differ diff --git a/spec/figures/commitTx.pdf b/spec/figures/commitTx.pdf new file mode 100644 index 00000000000..cff578ba2aa Binary files /dev/null and b/spec/figures/commitTx.pdf differ diff --git a/spec/figures/contestTx.pdf b/spec/figures/contestTx.pdf new file mode 100644 index 00000000000..262d6d596d5 Binary files /dev/null and b/spec/figures/contestTx.pdf differ diff --git a/spec/figures/decrementTx.pdf b/spec/figures/decrementTx.pdf new file mode 100644 index 00000000000..6b854be0f55 Binary files /dev/null and b/spec/figures/decrementTx.pdf differ diff --git a/spec/figures/fanoutTx.pdf b/spec/figures/fanoutTx.pdf new file mode 100644 index 00000000000..8648b27895d Binary files /dev/null and b/spec/figures/fanoutTx.pdf differ diff --git a/spec/figures/initTx.pdf b/spec/figures/initTx.pdf new file mode 100644 index 00000000000..a04f5168cd0 Binary files /dev/null and b/spec/figures/initTx.pdf differ diff --git a/spec/figures/state-transition_cropped.pdf b/spec/figures/state-transition_cropped.pdf new file mode 100644 index 00000000000..c64d33e8079 Binary files /dev/null and b/spec/figures/state-transition_cropped.pdf differ diff --git a/spec/figures/utxo-graph.pdf b/spec/figures/utxo-graph.pdf new file mode 100644 index 00000000000..dafea2f3c8f Binary files /dev/null and b/spec/figures/utxo-graph.pdf differ diff --git a/spec/intro.tex b/spec/intro.tex new file mode 100644 index 00000000000..080dff021d9 --- /dev/null +++ b/spec/intro.tex @@ -0,0 +1,31 @@ +\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/spec/macros.tex b/spec/macros.tex new file mode 100644 index 00000000000..44143dbb49b --- /dev/null +++ b/spec/macros.tex @@ -0,0 +1,764 @@ +% ==== 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 === +\newcommand{\undefined}{\mathrm{undef}} + + +% === Misc === + +\newcommand{\algoskip}{\vspace{4pt}} + +\newcommand{\ignore}[1]{} + +\newcommand{\red}[1]{\textcolor{red}{#1}} +\newcommand{\blue}[1]{\textcolor{blue}{#1}} + +\newcommand{\TODO}[1]{ + \if\relax\detokenize{#1}\relax + \textcolor{red}{TODO} + \else + \textcolor{red}{ {#1}} + \fi +} + +\newcommand{\fail}{\mbox{fail}} + +% from https://www.overleaf.com/latex/examples/simple-stylish-box-design/stzmmcshxdng +\definecolor{main}{HTML}{5989cf} % setting main color to be used +\definecolor{sub}{HTML}{cde4ff} % setting sub color to be used +\newtcolorbox{boxM}{ + fontupper = \color{white}, + rounded corners, + arc = 6pt, + colback = main!80, + colframe = main, + boxrule = 0pt, + bottomrule = 4.5pt, + enhanced, + fuzzy shadow = {0pt}{-3pt}{-0.5pt}{0.5pt}{black!35} +} + +% In figures, this makes algorithms work with option [H] despite +% double-column format +% https://tex.stackexchange.com/questions/82271/multiple-algorithm2e-algorithms-in-two-column-documents +\makeatletter +\newcommand{\removelatexerror}{\let\@latex@error\@gobble} +\makeatother + +\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{\st}{\mathsf{ST}} +\newcommand{\pt}{\mathsf{PT}} + +% == Transactions == + +\newcommand{\mtxInit}{\textit{init}} +\newcommand{\mtxCom}{\textit{commit}} +\newcommand{\mtxCommit}{\textit{commit}} +\newcommand{\mtxCCom}{\textit{collectCom}} +\newcommand{\mtxCollect}{\textit{collectCom}} +\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{\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{\hpDecommit}{\mathtt{decommit}} +\newcommand{\hpClose}{\mathtt{close}} +\newcommand{\hpCont}{\mathtt{cont}} +\newcommand{\hpFO}{\mathtt{fanOut}} + +\ignore{ + \newcommand{\obj}{\Omega} + + \newcommand{\certreq}{\ensuremath{\mathtt{sigReq}}} + \newcommand{\certack}{\ensuremath{\mathtt{sigAck}}} + \newcommand{\certconf}{\ensuremath{\mathtt{sigConf}}} + + \newcommand{\abortreq}{\ensuremath{\mathsf{abortReq}}} + + \newcommand{\init}{\mathbf{Init}} + \newcommand{\gencert}{\mathbf{GenCert}} + + \newcommand{\txobj}{\mathsf{txo}} + \newcommand{\genobj}{\mathsf{obj}} + \newcommand{\genset}{\mathsf{ObjSet}} + \newcommand{\gentxobj}{\mathsf{GenTxObj}} + \newcommand{\stateobj}{\ensuremath{u}} + \newcommand{\ack}{\mathsf{ack}} +} + +% == 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{\hpRD}{\mathtt{reqDec}} +\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 + \removelatexerror% Nullify \@latex@error + \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}} +\newcommand{\First}{\mathsf{First}} + + +% == 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/spec/main.tex b/spec/main.tex new file mode 100644 index 00000000000..4cbbd5ac164 --- /dev/null +++ b/spec/main.tex @@ -0,0 +1,74 @@ +\documentclass[11pt]{article} + +\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 + +% Fix display of - in numbers +\DeclareUnicodeCharacter{2212}{\textendash} + +\include{macros} + +\begin{document} + +\title{\Large \textbf{Hydra HeadV1 Specification: Coordinated Head protocol}\\[2ex] DRAFT} +\author{Sebastian Nagel sebastian.nagel@iohk.io} +% NOTE: add yourself + +\maketitle + +\input{intro} +\input{overview} + +\input{prel} +\input{setup} +\input{onchain} +\clearpage +\input{offchain} + +% NOTE: Provided by researchers (keep up-to-date) +\clearpage +\input{security} + +\clearpage +\bibliographystyle{plain} +\bibliography{short} + +\end{document} diff --git a/spec/offchain.tex b/spec/offchain.tex new file mode 100644 index 00000000000..f6cfc220998 --- /dev/null +++ b/spec/offchain.tex @@ -0,0 +1,330 @@ +\section{Off-Chain Protocol}\label{sec:offchain} + +This section describes the actual Coordinated Hydra Head protocol, an even more +simplified version of the original publication~\cite{hydrahead20}. See the +protocol overview in Section~\ref{sec:overview} for an introduction and notable +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 + observed by all actors: + \begin{itemize} + \item $\mathtt{initialTx}$: initiates a head + \item $\mathtt{commitTx}$: commits UTxO to an initializing head + \item $\mathtt{collectComTx}$: opens a head + \item $\mathtt{decrementTx}$: removes UTxO from an open head + \item $\mathtt{closeTx}$: closes a head + \item $\mathtt{contestTx}$: contests a closed head + % NOTE: fanout not mentioned because not needed in off-chain protocol + % description + \end{itemize} + \item Off-chain network messages sent between protocol actors (parties): + \begin{itemize} + \item $\hpRT$: to request a transaction to be included in the next snapshot + \item $\hpRD$: to request exclusion of UTxO via a decommit transaction + \item $\hpRS$: to request a snapshot to be created \& signed by every head member + \item $\hpAS$: to acknowledge a snapshot by replying with their signatures + \end{itemize} + \item Commands issued by the participants themselves or on behalf of end-users and clients + \begin{itemize} + \item $\hpInit$: to start initialization of a head + \item $\hpClose$: to request closure of an open head + \end{itemize} +\end{enumerate} + +% TODO: define states and e.g. that newTx not possible when closed? state diagram? + +The behavior is fully specified in Figure~\ref{fig:off-chain-prot}, while the +following paragraphs introduce notation, explain variables and walk-through the +protocol flow. + +\subsection{Assumptions} + +On top of the statements of the protocol setup in Section~\ref{sec:setup}, the +off-chain protocol logic relies on these assumptions: +\todo{move/merge with protocol setup?} +\begin{itemize} + \item Every network message received from a specific party is checked for + authentication. An implementation of the specification needs to find a + suitable means of authentication, either on the communication channel + or for individual messages. Unauthenticated messages must be dropped. + \item The head protocol gets correctly (and with completeness) notified about + observed transactions on-chain belonging to the respective head + instance. + % TODO: Mention multiple heads? + % \item The specification covers only a single instance of a Hydra head. + % However, some implementations may choose to track multiple instances. As + % multiple Hydra heads might exist on the same blockchain, it is vital + % that they do not interfere and the specification will take special care + % to ensure this. + \item All inputs are processed to completion, i.e.\ run-to-completion semantics + and no preemption. + \item Inputs are deduplicated. That is, any two identical inputs must not lead + to multiple invocations of the handling semantics. + \item Given the specification, inputs may pile up forever and implementations + need to consider these situations (i.e.\ potential for DoS). A valid reaction + to this would be to just drop these inputs. Note that, from a security standpoint, + these situations are identical to a non-collaborative peer and closing the head + is also a possible reaction. + \item The lifecycle of a Hydra head on-chain does not cross (hard fork) + protocol update boundaries. Note that these inputs are announced in + advance hence it should be possible for implementations to react in such + a way as to expedite closing of the head before such a protocol update. + This further assumes that the contestation period parameter is picked + accordingly.\todo{Treat this also in a dedicated section like rollbacks} +\end{itemize} + +\subsection{Notation} +\todo{missing:, apply tx} +\begin{itemize} + \item $\KwOn~event$ specifies how the protocol reacts on a given input $event$. + Further information may be available from the constituents of $event$ + and origin of the input. + \item $\Req~p$ means that boolean expression $p \in \tyBool$ must be satisfied + for the further execution of a routine, while discontinued on $\neg p$. + A conservative protocol actor could interpret this as a reason to close + the head. + \item $\KwWait~p$ is a non-blocking wait for boolean predicate $p \in \tyBool$ + to be satisfied. On $\neg p$, the execution of the routine is stopped, + queued, and reactivated at latest when $p$ is satisfied. + \item $\Multi{}~msg$ means that a message $msg$ is (channel-) authenticated + and sent to all participants of this head, including the sender. + \item $\PostTx{}~tx$ has a party create transaction $tx$, potentially from + some data, and submit it on-chain. See Section~\ref{sec:on-chain} for + individual transaction details. + \item $\Out{}~event$ signals an observation of $event$, which is used in the + security definition and proofs of Section~\ref{sec:security}. This + keyword can be ignored when implementing the protocol. +\end{itemize} + +\subsection{Variables} + +Besides parameters agreed in the protocol setup (see Section~\ref{sec:setup}), a +party's local state consists of the following variables: + +\begin{itemize} + \item $\hatv$: Last seen open state version. + \item $\hats$: Sequence number of latest seen snapshot. + \item $\hatSigma \in {(\tyNatural \times \tyBytes)}^{*}$: Accumulator of + signatures of the latest seen snapshot, indexed by parties. + \item $\hatmL$: UTxO set representing the local ledger state resulting from + applying $\hatmT$ to $\bar{S}.U$ to validate requested transactions. + \item $\hatmT \in \mT^{*}$: List of transactions applied locally and pending + inclusion in a snapshot (if this party is the next leader). + \item $\tx_{\omega} \in \mathcal{T}^{?}$: Pending decommit transaction, whose outputs are to be decommitted from the head. May be $\bot$ if nothing to decommit. + \item $\bar{\mc S}$: Snapshot object of the latest confirmed snapshot which contains: + \begin{center} + \begin{tabular}{|l|l|}\hline + $\bar{\mc S}.v$ & snapshot version \\ \hline + $\bar{\mc S}.s$ & snapshot number \\ \hline + $\bar{\mc S}.T$ & set of transactions relating this snapshot to its predecessor \\ \hline + $\bar{\mc S}.U$ & snapshotted UTxO set \\ \hline + $\bar{\mc S}.\tx_{\omega}$ & optional decommit transaction \\ \hline + $\bar{\mc S}.\sigma$ & multisignature \\ \hline + \end{tabular} + \end{center} + The function $\Sno(v,n,T,U,\tx_{\omega})$ initializes a snapshot object with no multi-signature set. + \todo{add types?} +\end{itemize} + +\subsection{Protocol flow} + +\subsubsection{Initializing the head} + +\dparagraph{$\hpInit$.}\quad Before a head can be initialized, all parties need +to exchange and agree on protocol parameters during the protocol setup phase +(see Section~\ref{sec:setup}), so we can assume the public Cardano keys +$\cardanoKeys^{setup}$, Hydra keys $\hydraKeysAgg^{setup}$, as well as the +contestation period $\cPer^{setup}$ are available. One of the clients then can +start head initialization using the $\hpInit$ command, which will result in an +$\mtxInit$ transaction being posted. \\ + +\dparagraph{$\mathtt{initialTx}$.}\quad All parties will receive this $\mtxInit$ +transaction and validate announced parameters against the pre-agreed $setup$ +parameters, as well as the structure of the transaction and the minting policy +used. This is a vital step to ensure the initialized Head is valid, which +cannot be checked completely on-chain (see also Section~\ref{sec:init-tx}). \\ + +\dparagraph{$\mathtt{commitTx}$.}\quad As each party $p_{j}$ posts a +$\mtxCommit$ transaction, the protocol records observed committed UTxOs of each +party $C_j$. With all committed UTxOs known, the $\eta$-state is created (as +defined in Section~\ref{sec:collect-tx}) and the $\mtxCollect$ transaction is +posted. Note that while each participant may post this transaction, only one of +them will be included in the blockchain as the mainchain ledger prevents double +spending. Should any party want to abort, they would post an $\mtxAbort$ +transaction and the protocol would end at this point.\\ + +\dparagraph{$\mathtt{collectComTx}$.}\quad Upon observing the $\mtxCollect$ +transaction, the parties compute $\Uinit \gets \bigcup_{j=1}^{n} C_j$ using previously +observed $C_j$ and initialize $\hatmL = \Uinit$. The seen transaction set is +initialized empty $\hatmT = \emptyset$, seen head state version $\hatv = 0$, as +well as snapshot number $\hats = 0$. No commit transaction is pending +$\tx_{\omega} = \bot$ and the initial snapshot object is defined accordingly +$\bar{\mc S} \gets \blue{\Sno(0, 0, \Uinit, \emptyset, \bot)}$. + +\subsubsection{Processing transactions off-chain} + +Transactions are announced and captured in so-called snapshots. Parties generate +snapshots in a strictly sequential round-robin manner. The party responsible for +issuing the $\ith i$ snapshot is the \emph{leader} of the $\ith i$ snapshot. +Leader selection is round-robin per the $\hydraKeys$ from the protocol setup. +While the frequency of snapshots in the general Head protocol~\cite{hydrahead20} +was configurable, the Coordinated Head protocol does specify a snapshot to be +created after each transaction.\\ + +\dparagraph{$\hpRT$.}\quad Upon receiving request $(\hpRT,\tx)$, the transaction is +applied to the \emph{local} ledger state $\hatmL \applytx \tx$. If not +applicable yet, the protocol does $\KwWait$ to retry later or eventually marks +this transaction as invalid (see assumption about events piling up). After +applying and if there is no current snapshot in flight ($\hats = \bar{\mc S}.s$) and the +receiving party $\party_{i}$ is the next snapshot +leader, a message to request snapshot signatures $\hpRS$ is sent. \\ + +\dparagraph{$\hpRD$.}\quad Upon receiving request $(\hpRD,\tx)$, the transaction is +checked against the \emph{local} ledger state. If decommit is not applicable yet +or another decommit is still pending, the protocol does $\KwWait$ to retry later or +eventually marks the decommit as invalid. In case there is no snapshot in flight +and party is the leader then a snapshot request $\hpRS$ is +sent containing the decommit transaction $\tx_{\omega}$. \\ + +\dparagraph{$\mathtt{decrementTx}$.}\quad Upon observing the \mtxDecrement{} +transaction, which removed outputs $U_{\omega}$ from the head, the corresponding +decommit transaction is cleared and the observed version $v$ is used for future +snapshots by +setting $\hatv \gets v$. Note that the version of the open head state is incremented on each \mtxDecrement{} transaction as described in Section~\ref{sec:decrement-tx} \\ + +\dparagraph{$\hpRS$.}\quad Upon receiving request +$(\hpRS,v,s,\mT_{\mathsf{req}}, \tx_{\omega})$\footnote{Snapshot requests + with only transaction identifiers are possible too if all parties keep an + index of previously seen transactions and their identifiers.} from party +$\party_j$, the receiving $\party_i$ $\Req$s that $v$ refers to the current +open state version, $s$ is the next snapshot number +and that party $\party_j$ is responsible for leading its creation.\todo{define + $\hpLdr$} Party $\party_i$ may has to $\KwWait$ until the previous snapshot is +confirmed ($\bar{\mc S}.s = \hats$). If the decommit transaction $\tx_{\omega}$ +is not $\bot$, the transaction is $\Req$d to be applicable to the last confirmed +UTxO set $\bar{\mc S}.U$ and decommitted transaction outputs must be removed, yielding the still +active UTxO set $U_{\mathsf{active}}$. Then, all requested transactions +$\mT_{\mathsf{req}}$ are $\Req$d to be applicable to $U_{\mathsf{active}}$, +otherwise the snapshot is rejected as invalid. Only then, $\party_i$ increments +their seen-snapshot counter $\hats$, resets the signature accumulator +$\hatSigma$, and computes the UTxO set of the new local snapshot as +$U \gets U_{\mathsf{active}} \applytx \mT_{\mathsf{req}}$. Then, $\party_i$ +creates a signature $\msSig_i$ using their signing key $\hydraSigningKey$ on a +message comprised by the $\cid$, the new snapshot number $\hats$, the new $\eta$ +resulting from canonically combining $U$ (see Section~\ref{sec:close-tx} for +details), and $\eta_{\omega}$ derived from decommit transaction $\tx_{\omega}$ outputs. +The signature is sent to all head members via message $(\hpAS,\hats,\msSig_i)$. +Finally, the local ledger state $\hatmL$ and pending transaction set $\hatmT$ +get pruned by re-applying all locally pending transactions $\hatmT$ to the just +requested snapshot's UTxO set iteratively and +ultimately yielding a ``pruned'' version of $\hatmT$ and $\hatmL$. \\ + +\dparagraph{$\hpAS$.}\quad Upon receiving acknowledgment $(\hpAS,s,\msSig_j)$, all +participants $\Req$ that it is from an expected snapshot (either the last seen +$\hats$ or + 1), potentially $\KwWait$ for the corresponding $\hpRS$ such that +$\hats = s$ and $\Req$ that the signature is not yet included in $\hatSigma$. +They store the received signature in the signature accumulator $\hatSigma$, and +if the signature from each party has been collected, $\party_i$ aggregates the +multisignature $\msCSig$ and $\Req$ it to be valid (constructing the signed message +as in $\hpRS$). If everything is fine, the snapshot can be considered +confirmed by creating the snapshot object +$\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT , \tx_{\omega})$ and storing +the multi-signature $\msCSig$ in it for later reference. In case there is a pending +decommit, any participant\todo{Shouldn't the decommitting party do this?} can now submit a \mtxDecrement{} transaction by +providing the just confirmed snapshot with its digests of the active UTxO set +$\eta$ and the to be removed UTxO set $\eta_{\omega}$. Similar to the $\hpRT$, if +$\party_i$ is the next snapshot leader and there are already transactions to +snapshot in $\hatmT$, a corresponding $\hpRS$ is distributed. + +\subsubsection{Closing the head} + +\dparagraph{$\hpClose$.}\quad In order to close a head, a client issues the +$\hpClose$ input which uses the latest confirmed snapshot $\bar{\mc S}$ to +create the new $\eta$-state from the last confirmed UTxO set, the digest of +to-decommit UTxO set $\eta_{\omega}$, and the certifiate $\xi$ using the corresponding +multi-signature. With these, the $\mtxClose$ transaction can be constructed and +posted. See Section~\ref{sec:close-tx} for details about this transaction. \\ + +\dparagraph{$\mathtt{closeTx}/\mathtt{contestTx}$.}\quad When a party observes +the head getting closed or contested, the $\eta$-state extracted from the +\mtxClose{} or \mtxContest{} transaction represents the latest head status that +has been aggregated on-chain so far (by a sequence of \mtxClose{} and +\mtxContest{} transactions). If the last confirmed (off-chain) snapshot is newer +than the observed (on-chain) snapshot number $s_{c}$, an updated $\eta$-state +and certificate $\xi$ is constructed posted in a \mtxContest{} transaction (see +Section~\ref{sec:contest-tx}). + +\subsection{Rollbacks and protocol changes}\label{sec:rollbacks} +The overall life-cycle of the Head protocol is driven by on-chain inputs (see +introduction of Section~\ref{sec:offchain}) which stem from observing +transactions on the mainchain. Most blockchains, however, do only provide +\emph{eventual} consistency. The consensus algorithm ensures a consistent view +of the history of blocks and transactions between all parties, but this +so-called \emph{finality} is only achieved after some time and the local view of +the blockchain history may change until that point. + +On Cardano with it's Ouroboros consensus algorithm, this means that any local +view of the mainchain may not be the longest chain and a node may switch to a +longer chain, onto another fork. This other version of the history may not +include what was previously observed and hence, any tracking state needs to be +updated to this ``new reality''. Practically, this means that an observer of the +blockchain sees a \emph{rollback} followed by rollforwards. +% TODO: mention the trade-off about waiting for finality when opening the head +% vs. issue and mark transactions as confirmed on the L2 if they were not in case +% the head opening get's rolled back and not retransmitted. + +For the Head protocol, this means that chain events like $\mathtt{closeTx}$ may +be observed a second time. Hence, it is crucial, that the local state of the +Hydra protocol is kept in sync and also rolled back accordingly to be able to +observe and react to these events the right way, e.g.\ correctly contesting this +$\mathtt{closeTx}$ if need be. +% TODO: mention that contestation deadline will stay the same and hence the +% contestation period will need to be picked long enough to reduce the risk of +% not being able to contest anymore after a rollback. + +The rollback handling can be specified fully orthogonal on top of the nominal +protocol behavior, if the chain provides strictly monotonically increasing +points $p$ on each chain event via a new or wrapped $\mathtt{rollforward}$ +event and $\mathtt{rollback}$ event with the point to which a rollback happened:\\ + +\dparagraph{$\mathtt{rollforward}$.}\quad On every chain event that is paired or +wrapped in a rollforward event $(\mathtt{rollback},p)$ with point $p$, protocol +participants store their head state indexed by this point in a history +$\Omega$ of states $\Delta \gets (\hatv, \hats, \hatmU, \hatSigma, \hatmL, \hatmT, \bar{\mc S})$ and $\Omega' = (p, \Delta) \cup \Omega$. \\ + +\dparagraph{$\mathtt{rollback}$.}\quad On a rollback +$(\mathtt{rollback},p_{rb})$ to point $p_{rb}$, the corresponding head state +$\Delta$ need to be retrieved from $\Omega$, with the maximal point +$p \leq p_{rb}$, and all entries in $\Omega$ with $p > p_{rb}$ get removed. \\ + +This will essentially reset the local head state to the right point and allow +the protocol to progress through the life-cycle normally. Most stages of the +life-cycle are unproblematic if they are rolled back, as long as the protocol +logic behaves as in the nominal case. + +A rollback ``past open'' is a special situation though. When a Head is open and +snapshots have been signed, but then a $\mtxCollect$ and one or more +$\mtxCommit$ transactions were rolled back, a bad actor could choose to commit a +different UTxO and open the Head with a different initial UTxO set, while the +already signed snapshots would still be (cryptographically) valid. To mitigate +this, all signatures on snapshots need to incorporate the initial UTxO set by +including $\eta_{0}$. \todo{version-counting is less powerfull} +% FIXME: \eta_0 not compatible with versioning scheme +\todo{Expand to rollbacks in presence of decrements} + +\todo{Write about contestation deadline vs. rollbacks} + +\input{fig_offchain_prot} + +\todo{In figure: $\combine$ on UTxO slightly different than on commits} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/spec/onchain.tex b/spec/onchain.tex new file mode 100644 index 00000000000..4dd23a7792a --- /dev/null +++ b/spec/onchain.tex @@ -0,0 +1,610 @@ +\clearpage +\section{On-chain Protocol}\label{sec:on-chain} +% FIXME: update all figures: removed n and decrement changes +\todo{Update figures} + +\todo{Open problem: ensure abort is always possible. e.g. by individual aborts or undoing commits} +\todo{Open problem: ensure fanout is always possible, e.g. by limiting complexity of $U_0$} + +The following sections describe the the \emph{on-chain} protocol controlling the +life-cycle of a Hydra head, which can be intuitively described as a state +machine (see Figure~\ref{fig:SM_states_basic}). Each transition in this state +machine is represented and caused by a corresponding Hydra protocol transaction +on-chain: $\mtxInit{}$, $\mtxCom{}$, $\mtxAbort{}$, $\mtxCollect{}$, +$\mtxDecrement{}$, $\mtxClose{}$, $\mtxContest{}$, and $\mtxFanout{}$. + +% TODO: Could include a combined overview, slightly more detailed than Figure 1 +% of the transaction trace for the full life cycle maybe? + +\noindent The protocol defines one minting policy script and three validator scripts: +\begin{itemize} + \item $\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 + $\mtxCommit{}$ or when the head initialiazation is aborted via + $\mtxAbort{}$. + \item $\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 + contract continuity throughout $\mtxCollect{}$, $\mtxDecrement{}$, + $\mtxClose{}$, $\mtxContest{}$ and $\mtxFanout{}$. +\end{itemize} + +\subsection{Init transaction}\label{sec:init-tx} + +The \mtxInit{} 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 +by a single output reference parameter $\seed \in \tyOutRef$: +\[ + \cid = \hash(\muHead(\seed)) +\] + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{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} +\end{figure} + +\noindent Two kinds of tokens are minted: +\begin{itemize} + \item 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 + $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|$ + participants with policy $\cid$, + \item has $|\hydraKeys|$ initial outputs $o_{\mathsf{initial}_{i}}$ with datum $\datumInitial{} = \cid$, + \item has one head output + $o_{\mathsf{head}}$, which captures + the initial state of the protocol in the datum + \[ + \datumHead = (\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} + +\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: +% TODO: mint redeemer conflicts with mint field +\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. + $(\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$ + % 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|$} + % 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, + \begin{menumerate} + \item 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 +to $\nuHead$ and $\nuInitial$ respectively, while these validators in turn +ensure continuity of the contract. However, it is \textbf{crucial} that all head +members check that head output always contains an $\st$ token of policy $\cid$ +which satisfies $\cid = \hash(\muHead(\seed))$. The $\seed$ from a head datum +can be used to determine this. Also, head members should verify whether the +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} + +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 +Figure~\ref{fig:commitTx} and has the following structure: +\begin{itemize} + \item One input spending from $\nuInitial$ with datum $\datumInitial{}$, + where value $\valInitial{i}$ holds a $\pt_i$, and the redeemer + $\redeemerInitial{} \in \tyOutRef^{*}$ is a list of output + references to be committed, + \item zero or more inputs with reference $\txOutRef_{\mathsf{committed}_{j}}$ + spending output $o_{\mathsf{committed}_{j}}$ with + $\val_{\mathsf{committed}_{j}}$, + \item one output paying to $\nuCommit$ with value $\valCommit{i}$ and datum $\datumCommit{}$. +\end{itemize} + +\noindent The $\nuInitial$ validator with $\datumInitial{} = \cid$ and +$\redeemerInitial{} = \underline{\txOutRef}_{\mathsf{committed}}$ ensures that: +\begin{menumerate} + \item All committed value is in the output + $\valCommit{i} \supseteq \valInitial{i} \cup (\bigcup_{j=1}^{m} \val_{\mathsf{committed}_{j}})$ + \footnote{The $\supseteq$ is important for real world situations where the values + might not be exactly equal due to ledger constraints (i.e. to ensure a + minimum value on outputs).} + \item Currency id and committed outputs are recorded in the output datum + $\datumCommit{} = (\cid, C_{i})$, where + $C_{i} = \forall j \in \{1 \dots m\} : [(\txOutRef_{\mathsf{committed}_{j}},\bytes(o_{\mathsf{committed}_{j}}))]$ + is a list of all committed UTxO recorded as tuples on-chain. + \item Transaction is signed by the right participant + $\exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valInitial{} \Rightarrow \keyHash_{i} \in \txKeys$ + \item No minting or burning $\txMint = \varnothing$ +\end{menumerate} + +\noindent The $\nuCommit$ validator ensures the output is collected by either a +\mtxCCom{} in Section~\ref{sec:collect-tx} or \mtxAbort{} in +Section~\ref{sec:abort-tx} transaction of the on-chain state machine, selected +by the appropriate redeemer. + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{figures/commitTx.pdf} + \caption{\mtxCom{} transaction spending an initial output and a single + committed output, and producing a commit output.}\label{fig:commitTx} +\end{figure} +\todo{update with multiple commits} + +\subsection{Abort Transaction}\label{sec:abort-tx} + +The \mtxAbort{} transaction (see Figure~\ref{fig:abortTx}) allows a +party to abort the creation of a head and consists of +\begin{itemize} + \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, + \item $\forall i \in \{1 \dots |\hydraKeys|\}$ inputs either + \begin{itemize} + \item spending from $\nuInitial$ with with $\pt_{i} \in \valInitial{i}$ and $\datumInitial{i} = \cid$, or + \item spending from $\nuCommit$ with with $\pt_{i} \in \valCommit{i}$ and $\datumCommit{i} = (\cid, C_{i})$, + \end{itemize} + \item outputs $o_{1} \dots o_{m}$ to redistribute already committed UTxOs. +\end{itemize} + +Note that \mtxAbort{} represents a final transition of the state +machine and hence there is no state machine output. + +\noindent Each spent $\nuInitial$ validator with $\datumInitial{i} = \cid$ and $\redeemerInitial{i} = \mathsf{abort}$ ensures that: +\begin{menumerate} + \item The state token of currency $\cid$ is getting burned $\{\st \mapsto -1\} \subseteq \txMint$. +\end{menumerate} + +\noindent Each spent $\nuCommit$ validator with $\datumCommit{i} = (\cid,\cdot)$ and $\redeemerCommit{i} = \mathsf{abort}$ ensures that: +\begin{menumerate} + \item The state token of currency $\cid$ is getting burned $\{\st \mapsto -1\} \subseteq \txMint$. +\end{menumerate} + +\noindent The $\muHead(\seed)$ minting policy governs the burning of tokens via +redeemer $\mathsf{burn}$ that: +\begin{menumerate} + \item All tokens in $\txMint$ need to be of negative quantity + $\forall \{\cid \mapsto \cdot \mapsto q\} \in \txMint : q < 0$. +\end{menumerate} + +\noindent The state-machine validator $\nuHead$ is spent with +$\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$: + \[ + (\stInitial,\cid,\seed,\hydraKeys,\cPer) \xrightarrow[m]{\stAbort} \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 + the $m$ reimbursing outputs $o_{1} \dots o_{m}$\footnote{Only the first $m$ + outputs are used for reimbursing, while more outputs may be present in the + transaction, e.g for returning change.} with the canonically combined + committed UTxOs in $C_{i}$: + \[ + \hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) = \combine([C_{i} ~ | ~ \forall [1 \dots |\hydraKeys|], C_{i} \neq \bot]) + \] + + \item Transaction is signed by a participant $\exists \{\cid \mapsto \keyHash_{i} \mapsto -1\} \in \txMint \Rightarrow \keyHash_{i} \in \txKeys$. + \item All tokens are burnt + $|\{\cid \mapsto \cdot \mapsto -1\} \in \txMint| = |\hydraKeys| + 1$. +\end{menumerate} + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{figures/abortTx.pdf} + \caption{\mtxAbort{} transaction spending the $\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} + +\noindent The \mtxCCom{} transaction (Figure~\ref{fig:collectComTx}) collects +all the committed UTxOs to the same head. It has +\begin{itemize} + \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, + \item $\forall i \in \{1 \dots |\hydraKeys|\}$ inputs spending commit outputs + $(\valCommit{i}, \nuCommit, \datumCommit{i})$ with $\pt_{i} \in \valCommit{i}$ + and $\datumCommit{i} = (\cid, C_{i})$, and + \item one output paying to $\nuHead$ with value $\valHead'$ and + datum $\datumHead'$. +\end{itemize} + +\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 + unchanged and the new state is governed again by $\nuHead$ + \[ + (\stInitial,\cid,\seed,\hydraKeys,\cPer) \xrightarrow{\stCollect} (\stOpen,\cid,\hydraKeys,\cPer,v,\eta) + \] + where snapshot version is initialized as $v = 0$. + \item Commits are collected in $\eta$ + \[ + \eta = U^{\#} = \combine([C_{1}, \dots, C_{n}]) + \] + where $n = |\hydraKeys|$ and + \[ + \combine(\underline{C}) = \hash(\mathsf{concat}({\sortOn(1, \mathsf{concat}(\underline{C}))}^{\downarrow2})) + \] + That is, given a list of committed UTxO $\underline{C}$, where each element is + a list of output references and the serialised representation of what was + committed, $\combine$ first concatenates all commits together, sorts this list + by the output references, concatenates all bytes and hashes the + result\footnote{Sorting is required to ensure a canonical representation which + can also be reproduced from the UTxO set later in the fanout.}. + + \item All committed value captured and no value is extracted + \[ + \valHead' = \valHead \cup (\bigcup_{i=1}^{n} \valCommit{i}) + \] + \item Every participant had the chance to commit, by checking all tokens are + present in output\footnote{This is sufficient as a Head participant would + check off-chain whether a Head is initialized correctly with the right + number of tokens.} + % NOTE: Implemented slightly different as we would only count PTs and = n + \[ + |\{\cid \rightarrow . \rightarrow 1\} \in \valHead'| = |\hydraKeys| + 1 + \] + \item Transaction is signed by a participant + \[ + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valCommit{i} \Rightarrow \keyHash_{i} \in \txKeys + \] + \item No minting or burning + \[ + \txMint = \varnothing + \] +\end{menumerate} + +\noindent Each spent $\nuCommit$ validator with $\datumCommit{i} = (\cid,\cdot)$ and $\redeemerCommit{i} = \mathsf{collect}$ ensures that: +\begin{menumerate} + \item The state token of currency $\cid$ is present in the output value + \[ + \st \in \valHead' + \] +\end{menumerate} + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{figures/collectComTx.pdf} + \caption{\mtxCCom{} transaction spending the head output in $\stInitial$ + state and collecting from multiple commit outputs into a single + $\stOpen$ head output.}\label{fig:collectComTx} +\end{figure} + +\subsection{Decrement Transaction}\label{sec:decrement-tx} + +\noindent The \mtxDecrement{} transaction (Figure~\ref{fig:DecrementTx}) allows +a party to remove a UTxO from an already open head and consists of: + +\begin{itemize} + \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, + \item one output paying to $\nuHead$ with value $\valHead'$ and + datum $\datumHead'$, + \item one or more decommit outputs $o_{2} \dots o_{m+1}$. +\end{itemize} + +\noindent The state-machine validator $\nuHead$ is spent with +$\redeemerHead = (\mathsf{decrement}, \xi, s, m)$, where $\xi$ is a multi-signature of +the decrement snapshot which authorizes removal of some UTxO, $s$ is the +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 + 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') + \] + \item New version $v'$ is incremented correctly + \[ + v' = v + 1 + \] + \item $\xi$ is a valid multi-signature of the currency id $\cid$, the current state version $v$, and the new state $\eta'$ + \[ + \msVfy(\hydraKeys,(\cid || v || s || \eta' || \eta_{\omega}),\xi) = \true + \] + where snapshot number $s$ is provided through the redeemer and $\eta_{\omega}$ must be the digest of all removed UTxO + \[ + \eta_{\omega} = U^{\#}_{\omega} = \hash(\bigoplus_{j=2}^{m+1} \bytes(o_{j})) + \] + \item The value in the head output is decreased accordingly + \todo{Redundant to above? Only check $\valHead' < \valHead$?} + \[ + \valHead' \cup (\bigcup_{j=2}^{m+1} \val_{o_{j}}) = \valHead + \] + \item Transaction is signed by a participant + \todo{Allow anyone to do decrements?} + \[ + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valHead' \Rightarrow \keyHash_{i} \in \txKeys + \] +\end{menumerate} + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{figures/decrementTx.pdf} + \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} + +In order to close a head, a head member may post the \mtxClose{} transaction +(see Figure~\ref{fig:closeTx}). This transaction has +\begin{itemize} + \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, + \item one output paying to $\nuHead$ with value $\valHead'$ and + datum $\datumHead'$. +\end{itemize} + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{figures/closeTx.pdf} + \caption{\mtxClose{} transaction spending the $\stOpen$ head output and producing a $\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$ + 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) + \] + + \item Last known open state version is recorded in closed state + \[ + v' = v + \] + + \item Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup (\mathsf{Unused}, \xi) \cup (\mathsf{Used}, \xi, \eta_{\omega})$, where $\xi$ is a multi-signature of the closing snapshot and $\eta_{\omega}$ is a digest of the UTxO to decommit, three cases are distinguished: + \begin{menumerate} + \item $\mathsf{Initial}$: The initial snapshot is used to close the head and open state was not updated. No signatures are available and it suffices to check + \[ + v = 0 + \] + \[ + s' = 0 + \] + \[ + \eta' = \eta + \] + \item $\mathsf{Unused}$: Closing snapshot refers to current state version $v$ and any UTxO to decommit need to be present in the closed state too. + \[ + \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true + \] + which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided. + \item $\mathsf{Used}$: Closing snapshot refers the previous state $v - 1$ and any UTxO to decommit of the closing snapshot must not be recorded in the closed state. + \[ + \eta_{\Delta}' = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true + \] + where $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}. + \end{menumerate} + % TODO: detailed CDDL definition of msg + + \item Initializes the set of contesters + \[ + \contesters = \emptyset + \] + This allows the closing party to also contest and is required for use + cases where pre-signed, valid in the future, close transactions are + used to delegate head closing. + + \item Correct contestation deadline is set + \[ + \Tfinal = \txValidityMax + T + \] + \item Transaction validity range is bounded by + \[ + \txValidityMax - \txValidityMin \leq T + \] + to ensure the contestation deadline $\Tfinal$ is at most $2*T$ in the future. + \item Value in the head is preserved + \[ + \valHead' = \valHead + \] + \item Transaction is signed by a participant + \[ + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valCommit{i} \Rightarrow \keyHash_{i} \in \txKeys + \] + \item No minting or burning + \[ + \txMint = \varnothing + \] +\end{menumerate} + +\subsection{Contest Transaction}\label{sec:contest-tx} + +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 +transaction has +\begin{itemize} + \item one input spending from $\nuHead$ holding the $\st$ with $\datumHead$, + \item one output paying to $\nuHead$ with value $\valHead'$ and + datum $\datumHead'$. +\end{itemize} + +\begin{figure} + \centering \includegraphics[width=0.8\textwidth]{figures/contestTx.pdf} + \caption{\mtxContest{} transaction spending the $\stClosed$ head output and + producing a different $\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$ + 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') + \] + + \item Last known open state version stays recorded in closed state + \[ + v' = v + \] + + \item Contested snapshot number $s'$ is higher than the currently stored snapshot number $s$ + \[ + s' > s + \] + + \item Based on the redeemer $\mathsf{ContestType} = (\mathsf{Unused}, \xi) \cup (\mathsf{Used}, \xi, \eta_{\omega})$, where $\xi$ is a multi-signature of the contesting snapshot and $\eta_{\omega}$ is a digest of the UTxO to decommit, two cases are distinguished: + \begin{menumerate} + \item $\mathsf{Unused}$: Contesting snapshot refers to the current state version $v$ and any UTxO to decommit need to be present in the closed state too. + \[ + \msVfy(\hydraKeys,(\cid || v || s' || \eta' || \eta_{\Delta}'),\xi) = \true + \] + which implies $\eta_{\Delta}' = \eta_{\omega}$ while $\eta_{\omega}$ does not need to be provided. + \item $\mathsf{Used}$: Contesting snapshot refers the previous state version $v - 1$ and any UTxO to decommit must not be recorded in the closed state. + \[ + \eta_{\Delta}' = \bot + \] + \[ + \msVfy(\hydraKeys,(\cid || v - 1 || s' || \eta' || \eta_{\omega}),\xi) = \true + \] + where $\eta_{\omega}$ is provided by the redeemer\footnote{$\eta_{\omega}$ needs to be provided to verify the signature, but is otherwise not relevant for the closed state}. + \end{menumerate} + % TODO: detailed CDDL definition of msg + + \item The single signer $\{\keyHash\} = \txKeys$ has not already contested and is added to the set of contesters + \[ + \keyHash \notin \contesters + \] + \[ + \contesters' = \contesters \cup \keyHash + \] + \item Transaction is posted before deadline + \[ + \txValidityMax \leq \Tfinal + \] + \item Contestation deadline is updated correctly to + \[ + \Tfinal' = \left\{\begin{array}{ll} + \Tfinal & \mathrm{if} ~ |\contesters'| = n, \\ + \Tfinal + T & \mathrm{otherwise.} + \end{array}\right. + \] + \item Value in the head is preserved + \[ + \valHead' = \valHead + \] + \item Transaction is signed by a participant + \[ + \exists \{\cid \mapsto \keyHash_{i} \mapsto 1\} \in \valCommit{i} \Rightarrow \keyHash_{i} \in \txKeys + \] + \item No minting or burning + \[ + \txMint = \varnothing + \] +\end{menumerate} + +\subsection{Fan-Out Transaction} + +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 +\begin{itemize} + \item one input spending from $\nuHead$ holding the $\st$, and + \item outputs $o_{1} \dots o_{m+n}$ to distribute UTxOs. +\end{itemize} + +Note that \mtxFanout{} represents a final transition of the state machine and +hence there is no state machine output. + +\begin{figure} + \centering + \includegraphics[width=0.8\textwidth]{figures/fanoutTx.pdf} + \caption{\mtxFanout{} transaction spending the $\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: +\begin{menumerate} + \item State is advanced from $\datumHead \sim \stClosed$ to terminal state + $\stFinal$: % XXX: What does this actually mean? + \[ + (\stClosed,\cid,\hydraKeys,\cPer,v, s,\eta,\eta_{\Delta},\contesters,\Tfinal) \xrightarrow[m,n]{\stFanout} \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 + Section~\ref{sec:collect-tx}): + \[ + \eta = U^{\#} = \hash(\bigoplus_{j=1}^{m} \bytes(o_{j})) + \] + \item The following $n$ outputs are distributing funds according to + $\eta_{\Delta}$. That is, the outputs exactly correspond to the UTxO canonically + combined $U^{\#}_{\Delta}$ (see Section~\ref{sec:collect-tx}): + \[ + \eta_{\Delta} = U^{\#}_{\Delta} = \hash(\bigoplus_{j=m}^{m+n} \bytes(o_{j})) + \] + \item Transaction is posted after contestation deadline $\txValidityMin > \Tfinal$. + \item All tokens are burnt + $|\{\cid \mapsto \cdot \mapsto -1\} \in \txMint| = n + 1$. +\end{menumerate} + +\noindent The $\muHead(\seed)$ minting policy governs the burning of tokens via +redeemer $\mathsf{burn}$ that: +\begin{menumerate} + \item All tokens in $\txMint$ need to be of negative quantity + $\forall \{\cid \mapsto \cdot \mapsto q\} \in \txMint : q < 0$. +\end{menumerate} + +\FloatBarrier{} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/spec/overview.tex b/spec/overview.tex new file mode 100644 index 00000000000..05d70cf4b1a --- /dev/null +++ b/spec/overview.tex @@ -0,0 +1,125 @@ +\section{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{fig_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$. + + +\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 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 +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. + +Besides processing normal transactions, participants can also request to take +UTxO they can spend out of the Head and make it available on the main chain +using a \mtxDecrement{} transaction --- the whole process is called decommit. + +\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). + \item Allow for incremental decommits while head is open. +\end{itemize} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "main" +%%% End: diff --git a/spec/prel.tex b/spec/prel.tex new file mode 100644 index 00000000000..9602d3f822a --- /dev/null +++ b/spec/prel.tex @@ -0,0 +1,258 @@ +\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]{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/spec/security.tex b/spec/security.tex new file mode 100644 index 00000000000..ac26a9480c7 --- /dev/null +++ b/spec/security.tex @@ -0,0 +1,209 @@ +\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} + +\todo{Add security experiment} +\noindent Adversaries: + +\begin{mdescription} +\item[Active Adversary.] An \emph{active adversary} $\adv$ has full control + over the protocol, i.e., he is fully unrestricted in the above\todo{above this section there is no security game} security game. + + \item[Network Adversary.] A \emph{network adversary} $\adv_\emptyset$ does not corrupt + any head parties, eventually delivers all sent network messages + (i.e., does not drop any messages), and does not cause the $\hpClose$ event. + Apart from this restriction, the adversary can act arbitrarily in the above experiment. +\end{mdescription} + +\noindent Random variables: + +\begin{mitemize} +\item $\That_i$: the set of transactions $\tx$ for which party $\party_i$, + \emph{while uncorrupted}, output $(\hpSeen,\tx)$; + +\item $\Tbar_i$: the set of transactions $\tx$ for which party $\party_i$, + \emph{while uncorrupted}, output $(\hpConf,\tx)$; + +\item $\Snapbar_i$: latest snapshot $(s,U)$ that party + $\party_i$ performed \emph{while uncorrupted}: output $(\hpSnap,(s,U))$; + +\item $\Hcont$: the set of (at the time) uncorrupted parties who produced + $\xi$ upon close/contest request and $\xi$ was applied to + correct~$\eta$; and + +\item $\honest$: the set of parties that remain uncorrupted. +\end{mitemize} + + +\noindent Security conditions / events: + +\begin{itemize} +\item \propName{Consistency (Head)}: In presence of an active adversary, the + following condition holds at any point in time: + For all $i,j$, + $\Uinit \circ (\Tbar_i \cup \Tbar_j) \not= \bot$, i.e., no two + uncorrupted parties see conflicting transactions confirmed. + + \item \propName{Oblivious Liveness (Head)}: + Consider any protocol execution in presence of a network adversary wherein + the head does not get closed for a sufficiently long period of time, and consider + an honest party $p_i$ who enters transaction $\tx$ by executing $(\hpNew,\tx)$ \emph{each time after having finished a snapshot}. + + Then the following eventually holds: + $\tx \in \bigcap_{i\in[n]} \Tbar_i\ \vee\ % + \forall i: \Uinit \circ (\Tbar_i\cup\{\tx\}) = \bot$, + i.e., every party will observe the transaction confirmed or every party + will observe the transaction in conflict with their confirmed transactions.\footnote{ + In particular, \emph{liveness} expresses that the protocol makes progress + under reasonable network conditions if no head parties get corrupted. + } + +\item \propName{Soundness (Chain)}: In presence of an active adversary, + the following condition is satisfied: + $\exists \Ttilde \subseteq \bigcap_{i \in \honest} \That_i : \Ufinal + = \Uinit \circ \Ttilde\not=\bot$, i.e., the final UTxO set results + from applying a set of transactions to $U_0$ that have been seen by + all honest parties (wheras each such transaction applies conforming to the ledger rules). +\item \propName{Completeness (Chain)}: In presence of an active adversary, + the following condition holds: For $\Ttilde$ as above, + $\bigcup_{p_i \in \Hcont} \Tbar_i \subseteq \Ttilde$, i.e., all + transactions seen as confirmed by an honest party at the end of the + protocol are considered. +\end{itemize} + +Note that the original version of the coordinated head satisfies a stronger version of liveness which is important for the 'user experience' in the protocol: +\begin{itemize} + \item \propName{Liveness (Head)}: + Consider any protocol execution in presence of a network adversary wherein + the head does not get closed for a sufficiently long period of time, and consider + an honest party $p_i$ who enters transaction $\tx$ by executing $(\hpNew,\tx)$. + + Then the following eventually holds: + $\tx \in \bigcap_{i\in[n]} \Tbar_i\ \vee\ % + \forall i: \Uinit \circ (\Tbar_i\cup\{\tx\}) = \bot$, + i.e., every party will observe the transaction confirmed or every party + will observe the transaction in conflict with their confirmed transactions.\footnote{ + In particular, \emph{liveness} expresses that the protocol makes progress + under reasonable network conditions if no head parties get corrupted. + } +\end{itemize} + + +\subsection{Proofs} + +\paragraph{Consistency.} + +\begin{lemma}[Consistency] + \label{lem:consistency} + The coordinated head protocol satisfies the \propName{Consistency} property. +\end{lemma} +\begin{proof} + Observe that $\Tbar_i\cup\Tbar_j\subseteq\That_i$ since no + transaction can be confirmed without every honest party signing off + on it. Since parties do not sign conflicting transactions + (see $\hpRS$, `wait'), we have + $\Uinit\applytx\Tbar_i\neq\bot$, + $\Uinit\applytx\Tbar_j\neq\bot$, and + $\Uinit\applytx\That_i\neq\bot$. Thus, since $\Tbar_i\cup\Tbar_j\subseteq\That_i$ + it follows that + $\Uinit\applytx(\Tbar_i\cup\Tbar_j)\neq\bot$ +\end{proof} + +\paragraph{Oblivious Liveness.} +For all lemmas towards oblivious liveness, we assume the presence of a network adversary, and that the head does not get closed for a sufficiently +long period of time. +We call this the \emph{liveness condition}. + +\begin{lemma}\label{lem:reqconf} + Under the liveness condition, any snapshot issued as $(\hpRS,s,T)$ will eventually be confirmed + in the sense that every party holds a valid mulisignature on it. +\end{lemma} +\begin{proof} + Consider a party $p_i$ receiving message $(\hpRS,s,T)$. We demonstrate that $p_i$ executes + the code past the `wait' instruction of the $\hpRS$ routine. + + \begin{itemize} + \item Passing the `require' guard: + Note that the snapshot leader sends the request only if $\hats=\bars$, and for $s=\hats+1$. + Thus, $\hats_i=\hats$ since $p_i$ has already signed the snapshot for $\hats$. The `require' + guard is thus satisfied for $p_i$. + + \item Passing the `wait' guard: + Since the snapshot leader sees $\hats=\bars$, also $p_i$ will eventually see $\hats_i=\bars_i$. Furthermore, since all leaders are honest, it holds that $\hatmU\applytx\mT_{res}\not=\bot$ by construction. + \end{itemize} + + This implies that every party will eventually sign and acknowledge the newly created snapshot. + Finally, the `require' and `wait' guards of the $\hpAS$ code will be passed by every party + since an $\hpAS$ for snapshot number $s$ can only be received for $s\in\{\hats,\hats+1\}$ + as an acknowledgement can only be received for the current snapshot being worked on by $p_i$ + or a snapshot that is one step ahead---implying that everybody will hold a valid multisignature + on the snapshot in consideration. +\end{proof} + +\begin{lemma}[Eternal snapshot confirmation]\label{lem:eternal} + Under the liveness condition, as long as new transactions are issued, for any $k>0$, every party eventually confirms + a snapshot with sequence number $s=k$. +\end{lemma} +\begin{proof} + By Lemma~\ref{lem:reqconf}, any requested snapshot eventually gets confirmed, implying + that the next leader observes $\hats=\bars$ and thus, in turn, issues a new snapshot. + Thus, for any $k$, a snapshot is eventually confirmed. +\end{proof} + +\begin{lemma}[Oblivious Liveness] + \label{lem:liveness} + The coordinated head protocol satisfies the \propName{Oblivious Liveness} property. +\end{lemma} +\begin{proof} + Consider the first point in time where a transaction $\tx$ enters the system by some party $p_i$ + issuing $(\hpNew,\tx)$, and consider the next point in time + $t$ when $p_i$ issues a snapshot. + + By Lemma~\ref{lem:eternal}, this snapshot will eventually be issued and confirmed by all parties. + + \medskip + + Let $\hatmT$ be the transactions to be considered by $p_i$'s snapshot: $\hatmL=\barmU\applytx\hatmT$ + where $\barmU$ is the snapshot prior to $p_i$'s. Since $p_i$ issues + $(\hpRT,\tx)$ after each snapshot, we have that, either, + \begin{itemize} + \item $\tx\in\hatmT$, in which case $\tx \in \bigcap_{i\in[n]} \Tbar_i$ after everybody has completed this snapshot, or, + \item $\tx\notin\hatmT$, in which case $\hatmL\applytx\tx=\bot$ ($\tx$ is still in the wait queue of $(\hpRT,\tx)$. After everybody has completed this snapshot, it thus holds that $\forall i: \Uinit\applytx\Tbar_i=\hatmL$, and thus, that + $\forall i: \Uinit\applytx(\Tbar_i\cup\{\tx\})=\bot$. + \end{itemize} + In both cases, the lemma follows. +\end{proof} + +\paragraph{Soundness and completeness.} + +\begin{lemma}[Soundness] + \label{lem:soundness} + The basic head protocol satisfies the \propName{Soundness} property. +\end{lemma} + +\begin{proof} + Let $T$ be the set of transactions such that $\Ufinal=U_0\applytx T$. + Since $\Ufinal$ is multi-signed, it holds that $T\subseteq\That_i$ + ($T$ is \emph{seen}) by every honest party in the head. + Furthermore, since honest signatures are only issued for valid transaction, + $\Ufinal\not=\bot$ (i.e., $\Ufinal$ is a valid state), and soundness + follows. +\end{proof} + + +\begin{lemma}[Completeness] + \label{lem:completeness} + The basic head protocol satisfies the \propName{Completeness} + property. +\end{lemma} +\begin{proof} + Consider all parties $p_i\in\Hcont$. Since the close/contest process + finally accepts the latest multi-signed snapshot, it holds that + $\Ufinal.s \geq \max_{p_i\in\Hcont}(\bars_i)$, and thus that + $\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/spec/setup.tex b/spec/setup.tex new file mode 100644 index 00000000000..9d6e3ea4a22 --- /dev/null +++ b/spec/setup.tex @@ -0,0 +1,46 @@ +\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/spec/short.bib b/spec/short.bib new file mode 100644 index 00000000000..e4e7a769920 --- /dev/null +++ b/spec/short.bib @@ -0,0 +1,122 @@ +%% LaTeX2e file `main.bib' +%% generated by the `filecontents' environment +%% from source `main' on 2020/01/09. +%% +%------------------------------------------------------------------------------- + +@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}, + Biburl = {https://dblp.org/rec/bib/journals/iacr/Zahnentferner18a}, + Journal = {{IACR} Cryptology ePrint Archive}, + Pages = 469, + Timestamp = {Tue, 14 Aug 2018 17:08:11 +0200}, + Title = {An Abstract Model of {UTxO}-based Cryptocurrencies with + Scripts}, + Url = {https://eprint.iacr.org/2018/469}, + Volume = 2018, + Year = 2018, + Bdsk-Url-1 = {https://eprint.iacr.org/2018/469} +} + +@inproceedings{eutxo, + Author = {Manuel M. T. Chakravarty and James Chapman and Kenneth + MacKenzie and Orestis Melkonian and Michael Peyton Jones and + Philip Wadler}, + Booktitle = {4th Workshop on Trusted Smart Contracts}, + Note = + {\url{http://fc20.ifca.ai/wtsc/WTSC2020/WTSC20_paper_25.pdf}}, + Title = {The Extended {UTxO} Model}, + Year = 2020 +} + +@misc{eutxo-2, + title = {Extended {UTXO-2} model}, + note = + {\url{https://github.com/hydra-supplementary-material/eutxo-spec/blob/master/extended-utxo-specification.pdf}} +} + +@inproceedings{formal-model-of-bitcoin-transactions, + Author = {Nicola Atzei and Massimo Bartoletti and Stefano Lande and + Roberto Zunino}, + Bibsource = {dblp computer science bibliography, https://dblp.org}, + Biburl = {https://dblp.org/rec/bib/conf/fc/AtzeiBLZ18}, + Booktitle = {Financial Cryptography and Data Security - 22nd + International Conference, {FC} 2018, Nieuwpoort, + Cura{\c{c}}ao, February 26 - March 2, 2018, Revised Selected + Papers}, + Doi = {10.1007/978-3-662-58387-6\_29}, + Pages = {541--560}, + Timestamp = {Fri, 30 Aug 2019 11:18:49 +0200}, + Title = {A Formal Model of {Bitcoin} Transactions}, + Url = {https://doi.org/10.1007/978-3-662-58387-6\_29}, + Year = 2018, + Bdsk-Url-1 = {https://doi.org/10.1007/978-3-662-58387-6%5C_29} +} + +@misc{hydra-repo, + title = {Hydra repository}, + note = {\url{https://github.com/cardano-scaling/hydra}} +} + +@article{hydrahead20, + title = {Hydra: Fast isomorphic state channels}, + author = {Chakravarty, Manuel MT and Coretti, Sandro and Fitzi, + Matthias and Gazi, Peter and Kant, Philipp and Kiayias, + Aggelos and Russell, Alexander}, + journal = {Cryptology ePrint Archive}, + year = 2020 +} + +@misc{hydraspec22, + title = {Hydra {Head} {V1} Formal Specification}, + author = {IOG}, + howpublished = + {\url{https://docs.google.com/document/d/1XQ0C7Ko3Ifo5a4TOcW1fDT8gMYryB54PCEgOiFaAwGE}}, + year = 2022 +} + +@article{itakura1983public, + Author = {Itakura, Kazuharu and Nakamura, Katsuhiro}, + Journal = {NEC Research \& Development}, + Number = 71, + Pages = {1--8}, + Title = {A public-key cryptosystem suitable for digital + multisignatures}, + Year = 1983 +} + +@misc{ledger-alonzo-spec, + title = {A Formal Specification of the Cardano Ledger integrating + Plutus Core}, + note = + {\url{https://github.com/input-output-hk/cardano-ledger/releases/latest/download/alonzo-ledger.pdf}} +} + +@misc{ledger-shelley-spec, + title = {A Formal Specification of the Cardano Ledger}, + note = + {\url{https://github.com/input-output-hk/cardano-ledger/releases/latest/download/shelley-ledger.pdf}} +} + +@inproceedings{utxo-ma, + title = {UTXOma: UTXO with Multi-Asset Support}, + author = {Manuel M. T. Chakravarty and James Chapman and Kenneth M. + Mackenzie and Orestis Melkonian and Jann and M{\"u}ller and + Michael Peyton Jones and Polina Vinogradova and Philip Wadler + and Joachim and Zahnentferner}, + year = 2020 +}