diff --git a/flake.lock b/flake.lock index 5059be0501c..2afe961e058 100644 --- a/flake.lock +++ b/flake.lock @@ -687,6 +687,24 @@ "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": 1712014858, "narHash": "sha256-sB4SWl2lX95bExY2gMFG5HIzvva5AVMJd4Igm+GpZNw=", @@ -806,6 +824,22 @@ "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": { @@ -1414,6 +1448,26 @@ "type": "indirect" } }, + "hydra-spec": { + "inputs": { + "flake-parts": "flake-parts_2", + "formal-ledger": "formal-ledger", + "nixpkgs": "nixpkgs_11" + }, + "locked": { + "lastModified": 1721145821, + "narHash": "sha256-qLvyFe+V+q8+gsKTSZw/FJdwCG9kJ7TzDkVcLyO/8I4=", + "owner": "cardano-scaling", + "repo": "hydra-formal-specification", + "rev": "0f0a88a76dc56efac4f9ee3c56d356bfe0e4edcc", + "type": "github" + }, + "original": { + "owner": "cardano-scaling", + "repo": "hydra-formal-specification", + "type": "github" + } + }, "hydra_2": { "inputs": { "nix": "nix_2", @@ -1487,7 +1541,7 @@ "iohk-nix": { "inputs": { "blst": "blst_2", - "nixpkgs": "nixpkgs_11", + "nixpkgs": "nixpkgs_12", "secp256k1": "secp256k1_2", "sodium": "sodium_2" }, @@ -1621,8 +1675,8 @@ "mithril": { "inputs": { "crane": "crane_2", - "flake-parts": "flake-parts_2", - "nixpkgs": "nixpkgs_12", + "flake-parts": "flake-parts_3", + "nixpkgs": "nixpkgs_13", "treefmt-nix": "treefmt-nix" }, "locked": { @@ -1759,7 +1813,7 @@ }, "nix-npm-buildpackage": { "inputs": { - "nixpkgs": "nixpkgs_13" + "nixpkgs": "nixpkgs_14" }, "locked": { "lastModified": 1686315622, @@ -2157,6 +2211,18 @@ } }, "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": { "dir": "lib", "lastModified": 1711703276, @@ -2255,6 +2321,21 @@ } }, "nixpkgs_11": { + "locked": { + "lastModified": 1718717814, + "narHash": "sha256-xB7AzKY4BP7yypo6g+sk1tnVK54sBIJMeEBB5CdbhT4=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "88af533d8ae8d1e7e4648decf7817ebff91abf56", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "type": "github" + } + }, + "nixpkgs_12": { "locked": { "lastModified": 1684171562, "narHash": "sha256-BMUWjVWAUdyMWKk0ATMC9H0Bv4qAV/TXwwPUvTiC5IQ=", @@ -2270,7 +2351,7 @@ "type": "github" } }, - "nixpkgs_12": { + "nixpkgs_13": { "locked": { "lastModified": 1714091391, "narHash": "sha256-68n3GBvlm1MIeJXadPzQ3v8Y9sIW3zmv8gI5w5sliC8=", @@ -2286,7 +2367,7 @@ "type": "github" } }, - "nixpkgs_13": { + "nixpkgs_14": { "locked": { "lastModified": 1653917367, "narHash": "sha256-04MsJC0g9kE01nBuXThMppZK+yvCZECQnUaZKSU+HJo=", @@ -2680,6 +2761,7 @@ "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 caaea1dbd4c..667b828f398 100644 --- a/flake.nix +++ b/flake.nix @@ -19,6 +19,7 @@ cardano-node.url = "github:intersectmbo/cardano-node/8.11.0-pre"; mithril.url = "github:input-output-hk/mithril/2418.1"; nix-npm-buildpackage.url = "github:serokell/nix-npm-buildpackage"; + hydra-spec.url = "github:cardano-scaling/hydra-formal-specification"; }; outputs = @@ -120,7 +121,7 @@ packages = hydraPackages // (if pkgs.stdenv.isLinux then (prefixAttrs "docker-" hydraImages) else { }) // - { spec = import ./spec { inherit pkgs; }; }; + { spec = inputs.hydra-spec.packages.${system}.default; }; checks = let lu = inputs.lint-utils.linters.${system}; in { hlint = lu.hlint { src = self; hlint = pkgs.hlint; }; diff --git a/spec/.envrc b/spec/.envrc deleted file mode 100644 index aef781f7d49..00000000000 --- a/spec/.envrc +++ /dev/null @@ -1 +0,0 @@ -use flake .#spec diff --git a/spec/.gitignore b/spec/.gitignore deleted file mode 100644 index 70d834fd32a..00000000000 --- a/spec/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -/main.* -!/main.tex -/.auctex-auto/ diff --git a/spec/README.md b/spec/README.md deleted file mode 100644 index 3f0f35ec54d..00000000000 --- a/spec/README.md +++ /dev/null @@ -1,27 +0,0 @@ -# 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 deleted file mode 100644 index 35fb12ec038..00000000000 --- a/spec/acmart.cls +++ /dev/null @@ -1,2922 +0,0 @@ -%% -%% 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 deleted file mode 100644 index 1130baae567..00000000000 --- a/spec/default.nix +++ /dev/null @@ -1,15 +0,0 @@ -{ 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 deleted file mode 100644 index 89c616496f0..00000000000 --- a/spec/fig_SM_states_basic.tex +++ /dev/null @@ -1,24 +0,0 @@ -\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 {\red{$\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 deleted file mode 100644 index 70129603c4b..00000000000 --- a/spec/fig_offchain_prot.tex +++ /dev/null @@ -1,231 +0,0 @@ -\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$ \; - \red{$\bar{\mc S} \gets \Sno(0, 0, \Uinit, \emptyset, \bot)$ \;} - \red{$\hatv, \hats \gets 0$ \;} - $\hatmT \gets \emptyset$ \; - \red{$\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,\red{\hatv,}\bar{\mc S}.s+1, \hatmT, \red{\tx_{\omega}})$ \; - } - } - } - - \vspace{12pt} - - %%% REQ SN - \On{$(\hpRS,\red{v,}s,\mT_{\mathsf{req}}, \red{\tx_{\omega}})$ from $\party_j$}{ - \Req{$\red{v = \hatv ~ \land} ~ s = \hats + 1 ~ \land ~ \hpLdr(s) = j$} \; - \Wait{$\hats = \bar{\mc S}.s$}{ - \red{\Req{$\bar{\mc S}.U \applytx \tx_{\omega} \not= \bot$}} \; - \red{$U_{\mathsf{active}} \gets \bar{\mc S}.U \applytx \tx_{\omega}$} \; - \Req{$\red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}} \not= \bot$} \; - $U \gets \red{U_{\mathsf{active}}} \applytx \mT_{\mathsf{req}}$ \; - % XXX: why +1? ̂s ← s would be clearer here - $\hats \gets \bar{\mc S}.s + 1$ \; - % TODO: DRY message creation - $\eta \gets \combine(U)$ \; - % TODO: handwavy combine/outputs here - $\red{\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 || \red{v ||} \hats || \eta \red{|| \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 - \red{\On{$(\mathtt{reqDec},\tx)$ from $\party_j$}{ - \Wait{$\tx_\omega = \bot ~ \land ~ \hatmL \applytx \tx \not= \bot$}{ - $\hatmL \gets \hatmL \setminus \mathsf{inputs}(\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 - \red{\On{$(\mathtt{decrementTx}, U_{\omega}, v)$ from chain}{ - \If{$\mathsf{outputs}(\tx_{\omega}) = U_{\omega}$}{ - $\tx_{\omega} \gets \bot$ \; - $\hatv \gets v$ \; - % TODO: always snapshot? not strictly needed (to clear pending decommits)? - \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} - - %%% 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)$ \; - % TODO: tx_ω undefined (else) case - $\red{\eta_{\omega} \gets \combine(\mathsf{outputs}(\tx_{\omega}))}$ \; - - \Req{} $\msVfy(\hydraKeysAgg, (\cid || \red{\hatv ||} \hats || \eta \red{|| \eta_{\omega}}), \msCSig)$ \; - % create confirmed snapshot for later reference - $\bar{\mc S} \gets \Sno(\hatv, \hats, \hatmU, \hatmT \red{, \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)$ \; - \red{\If{$\tx_{\omega} \ne \bot$}{ - $\PostTx{}~(\mtxDecrement, \hatv, \hats, \eta, \eta_{\omega})$ \; - \red{$\Out (\hpConf,\tx_{\omega})$ \;} - }} - % issue snapshot if we are leader - \If{$\hpLdr(s+1) = i \land \hatmT \neq \emptyset$}{ - \Multi{} $(\hpRS,\red{\hatv},\bar{\mc S}.s+1, \hatmT, \red{\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)$ \; - \red{$\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \;} - $\xi \gets \bar{\mc S}.\sigma$ \; - $\PostTx{}~(\mtxClose, \red{\bar{\mc S}.v}, \bar{\mc S}.s, \eta, \red{\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)$ \; - \red{$\eta_\omega \gets \combine(\mathsf{outputs}(\bar{\mc S}.\tx_\omega))$ \;} - $\xi \gets \bar{\mc S}.\sigma$ \; - $\PostTx{}~(\mtxContest, \red{\bar{\mc S}.v}, \bar{\mc S}.s, \eta, \red{\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 deleted file mode 100644 index 71fe0e056f4..00000000000 Binary files a/spec/figures/SM-abort.pdf and /dev/null differ diff --git a/spec/figures/SM-close.pdf b/spec/figures/SM-close.pdf deleted file mode 100644 index 93eb89f2f8f..00000000000 Binary files a/spec/figures/SM-close.pdf and /dev/null differ diff --git a/spec/figures/SM-collect.pdf b/spec/figures/SM-collect.pdf deleted file mode 100644 index 5d069520ab0..00000000000 Binary files a/spec/figures/SM-collect.pdf and /dev/null differ diff --git a/spec/figures/SM-contest.pdf b/spec/figures/SM-contest.pdf deleted file mode 100644 index 2476ba8d7e5..00000000000 Binary files a/spec/figures/SM-contest.pdf and /dev/null differ diff --git a/spec/figures/SM-fanout.pdf b/spec/figures/SM-fanout.pdf deleted file mode 100644 index f6d28a24f28..00000000000 Binary files a/spec/figures/SM-fanout.pdf and /dev/null differ diff --git a/spec/figures/SM-init-commit.pdf b/spec/figures/SM-init-commit.pdf deleted file mode 100644 index 7ca2c4b8a68..00000000000 Binary files a/spec/figures/SM-init-commit.pdf and /dev/null differ diff --git a/spec/figures/abortTx.pdf b/spec/figures/abortTx.pdf deleted file mode 100644 index 3846492866d..00000000000 Binary files a/spec/figures/abortTx.pdf and /dev/null differ diff --git a/spec/figures/closeTx.pdf b/spec/figures/closeTx.pdf deleted file mode 100644 index 123f79def42..00000000000 Binary files a/spec/figures/closeTx.pdf and /dev/null differ diff --git a/spec/figures/collectComTx.pdf b/spec/figures/collectComTx.pdf deleted file mode 100644 index 87b71129219..00000000000 Binary files a/spec/figures/collectComTx.pdf and /dev/null differ diff --git a/spec/figures/commitTx.pdf b/spec/figures/commitTx.pdf deleted file mode 100644 index cff578ba2aa..00000000000 Binary files a/spec/figures/commitTx.pdf and /dev/null differ diff --git a/spec/figures/contestTx.pdf b/spec/figures/contestTx.pdf deleted file mode 100644 index 716af0bf58c..00000000000 Binary files a/spec/figures/contestTx.pdf and /dev/null differ diff --git a/spec/figures/decrementTx.pdf b/spec/figures/decrementTx.pdf deleted file mode 100644 index 6b854be0f55..00000000000 Binary files a/spec/figures/decrementTx.pdf and /dev/null differ diff --git a/spec/figures/fanoutTx.pdf b/spec/figures/fanoutTx.pdf deleted file mode 100644 index 855417a4024..00000000000 Binary files a/spec/figures/fanoutTx.pdf and /dev/null differ diff --git a/spec/figures/initTx.pdf b/spec/figures/initTx.pdf deleted file mode 100644 index a04f5168cd0..00000000000 Binary files a/spec/figures/initTx.pdf and /dev/null differ diff --git a/spec/figures/state-transition_cropped.pdf b/spec/figures/state-transition_cropped.pdf deleted file mode 100644 index c64d33e8079..00000000000 Binary files a/spec/figures/state-transition_cropped.pdf and /dev/null differ diff --git a/spec/figures/utxo-graph.pdf b/spec/figures/utxo-graph.pdf deleted file mode 100644 index dafea2f3c8f..00000000000 Binary files a/spec/figures/utxo-graph.pdf and /dev/null differ diff --git a/spec/intro.tex b/spec/intro.tex deleted file mode 100644 index 080dff021d9..00000000000 --- a/spec/intro.tex +++ /dev/null @@ -1,31 +0,0 @@ -\section{Introduction} -This document specifies the 'Coordinated Hydra Head' protocol to be implemented -as the first version of Hydra Head on Cardano - \textbf{Hydra HeadV1}. The -protocol is derived from variants described in the original paper -\cite{hydrahead20}, but was further simplified to make a first implementation on -Cardano possible. - -Note that the format and scope of this document is (currently) also inspired by -the paper and hence does not include a definition of the networking protocols or -concrete message formats. \todo{Add: network specification (message formats)} It -is structured similarly, but focuses on a single variant, and avoids -indirections and unnecessary generalizations. The document is kept in sync with -the reference implementation available on Github~\cite{hydra-repo}. -\textcolor{red}{Red} sections indicate that they are currently not covered or -missing in the implementation, where \textcolor{blue}{blue} parts mean a -difference in how it is realized. - -First, a high-level overview of the protocol and how it differs from legacy -variants of the Head protocol is given in Section~\ref{sec:overview}. Relevant -definitions and notations are introduced in Section~\ref{sec:prel}, while -Section~\ref{sec:setup} describes protocol setup and assumptions. Then, the -actual on-chain transactions of the protocol are defined in -Section~\ref{sec:on-chain}, before the off-chain protocol part specifies -behavior of Hydra parties off-chain and ties the knot with on-chain transactions -in Section~\ref{sec:offchain}. At last, Section~\ref{sec:security} gives the -security definition, properties and proofs for the Coordinated Head protocol. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: diff --git a/spec/macros.tex b/spec/macros.tex deleted file mode 100644 index 44143dbb49b..00000000000 --- a/spec/macros.tex +++ /dev/null @@ -1,764 +0,0 @@ -% ==== 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 deleted file mode 100644 index 4cbbd5ac164..00000000000 --- a/spec/main.tex +++ /dev/null @@ -1,74 +0,0 @@ -\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 deleted file mode 100644 index 0b5a6d39cf5..00000000000 --- a/spec/offchain.tex +++ /dev/null @@ -1,332 +0,0 @@ -\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 - \red{\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 - \red{\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 \red{$\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 \red{$\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 \red{$\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{handwavy; 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$, \red{seen head state version $\hatv = 0$}, as -well as snapshot number $\hats = 0$. \red{No commit transaction is pending -$\tx_{\omega} = \bot$ and} the initial snapshot object is defined accordingly -$\bar{\mc S} \gets \Sno(0, 0, \Uinit, \emptyset, \red{\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. \\ - -\red{\dparagraph{$\hpRD$.}\quad Upon receiving request $(\hpRD,\tx)$, the - transaction is checked against the \emph{local} ledger state. If decommit is - not applicable yet, the protocol does $\KwWait$ to retry later and eventually - emmits an error message that another decommit is in flight. In case there is - no decommit in flight and party is the leader then $\hpRS$ is - emmitted containing the decommit transaction $\tx_{\omega}$.} \\ - -\red{\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 is used for future - snapshots by - setting $\hatv = v$. This is required as 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,\red{v,}s,\mT_{\mathsf{req}}, \red{\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 receiver $\party_i$ checks that \red{$v$ refers to the current - open state version}\todo{wait or require?}, $s$ is the next snapshot number -and that party $\party_j$ is responsible for leading its creation.\todo{define - $\hpLdr$} Party $\party_i$ has to $\KwWait$ until the previous snapshot is -confirmed ($\bar{\mc S}.s = \hats$). \red{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 spent 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 \red{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), \red{and $\eta_{\omega}$ derived from commit 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 \red{(using the same 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 \red{, \tx_{\omega}})$ and storing -the multi-signature $\msCSig$ in it for later reference. \red{In case there is a pending - decommit, any participant 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 -\todo{add version here also}$\Delta \gets (\hats, \bar{\mc S}.s, \bar{\mc S}.sigma, \hatmU, \barmU, \hatSigma, \hatmL, \hatmT)$ 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 deleted file mode 100644 index 65523f685b9..00000000000 --- a/spec/onchain.tex +++ /dev/null @@ -1,620 +0,0 @@ -\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{}$, \red{$\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{}$, \red{$\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,\red{v,}\eta) - \] - \red{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})) - \] - % TODO: mention in off-chain that it is limited what we can fan out, so size - % & complexity of U needs to be contained, especially off-chain. - 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{\red{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 \todo{Decrement redeemer doesn't contain snapshot number} 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$ -\todo{Open datum should contain snapshot number} - \[ - (\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}, \red{\mathsf{CloseType}})$, where -\red{$\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,\red{v,}\eta) \xrightarrow[\red{\mathsf{CloseType}}]{\stClose} (\stClosed,\cid,\hydraKeys,\cPer,\red{v',s',\eta',\eta_{\Delta}'},\contesters,\Tfinal) - \] - - \item \red{Last known open state version is recorded in closed state - \[ - v' = v - \] - } - - \item \red{Based on the redeemer $\mathsf{CloseType} = \mathsf{Initial} \cup (\mathsf{Current}, \xi) \cup (\mathsf{Outdated}, \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{Current}$: 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. - % TODO: put more into the redeemer to simplify? - \todo{this is hard to understand} - \item $\mathsf{Outdated}$: 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}, \red{\mathsf{ContestType}})$, where -\red{$\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,\red{v,s,\eta,\eta_{\Delta}},\contesters,\Tfinal) \xrightarrow[\red{\mathsf{ContestType}}]{\stContest} (\stClosed,\cid,\hydraKeys,\cPer,\red{v',s',\eta',\eta_{\Delta}'},\contesters',\Tfinal') - \] - - \item \red{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 \red{Based on the redeemer $\mathsf{ContestType} = (\mathsf{Current}, \xi) \cup (\mathsf{Outdated}, \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{Current}$: 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{Outdated}$: 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\red{+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\red{, n})$, where $m$ \red{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,\red{v, s,}\eta,\red{\eta_{\Delta}},\contesters,\Tfinal) \xrightarrow[m\red{,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})) - \] - \red{\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 deleted file mode 100644 index 3b65d20d5c5..00000000000 --- a/spec/overview.tex +++ /dev/null @@ -1,126 +0,0 @@ -\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. - -\red{Besides processing ``normal'' transactions, participants can also request - to take some UTxO they can spend out of the Head and make it available on 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). - \red{\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 deleted file mode 100644 index 9602d3f822a..00000000000 --- a/spec/prel.tex +++ /dev/null @@ -1,258 +0,0 @@ -\clearpage -\section{Preliminaries}\label{sec:prel} - -This section introduces notation and other preliminaries used in the remainder -of the specification. - -\subsection{Notation} - -The specification uses set-notation based approach while also inspired -by~\cite{eutxo-2}~and~\cite{eutxo}. Values $a$ are in a set $a \in \mathcal{A}$, -also indicated as being of some type $a : \mathcal{A}$, and multidimensional values are -tuples drawn from a $\times$ product of multiple sets, e.g. -$(a,b) \in (\mathcal{A} \times \mathcal{B})$. An empty set is indicated by -$\emptyset$ and sets may be enumerated using $\{a_1 \dots a_n\}$ notation. The $=$ operator means -equality and $\gets$ is explicit assignment of a variable or value to one -or more variables. Projection is used to access the elements of a tuple, e.g. -${(a,b)}^{\downarrow1} = a$. Functions are morphisms mapping from one set to another -$x : \mathcal{A} \to f(x) : \mathcal{B}$, where function -application of a function $f$ to an argument $x$ is written as $f(x)$. \\ - -\noindent Furthermore, given a set $\mathcal{A}$, let -\begin{itemize} - \item $\mathcal{A}^? = \mathcal{A} \cup \Diamond$ denotes an option: a value from $\mathcal{A}$ or no value at all indicated by $\bot$, - \item $\mathcal{A}^n$ be the set of all n-sized sequences over $\mathcal{A}$, - \item $\mathcal{A}^! = \bigcup_{i=1}^{n \in \tyNatural} \mathcal{A}^{i}$ be the set of non-empty sequences over $\mathcal{A}$, and - \item $\mathcal{A}^* = \bigcup_{i=0}^{n \in \tyNatural} \mathcal{A}^{i}$ be - the set of all sequences over $\mathcal{A}$. -\end{itemize} - -\noindent With this, we further define: -\begin{itemize} - \item $\tyBool = \{\false, \true\}$ are boolean values - \item $\tyNatural$ are natural numbers $\{0, 1, 2, \ldots\}$ - \item $\tyInteger$ are integer numbers $\{\ldots, −2, −1, 0, 1, 2, \ldots\}$ - \item $\tyBytes = \bigcup_{n=0}^{\inf}{\{0,1\}}^{8n}$ denotes a arbitrary - string of bytes - \item $\concat : \tyBytes^* \to \tyBytes$ is concatenating bytes, we also use operator $\bigoplus$ for this - \item $\hash : x \to \tyBytes$ denotes a collision-resistant - hashing function and $x^{\#}$ indicates the hash of $x$ - \item $\bytes : x \to \tyBytes$ denotes an invertible serialisation function - mapping arbitrary data to bytes - \item $a || b = \concat(\bytes(a), \bytes(b))$ is an operator which concatenates the $\bytes(b)$ to the $\bytes(a)$ - \item Lists of values $l \in \mathcal{A}^{*}$ are written as - $l = [x_{1}, \ldots, x_{n}]$. Empty lists are denoted by $[]$, the $i$th - element $x_{i}$ is also written $l[i]$ and the length of the list is - $|l| = n$. An underscore is also used to indicate a list of values - $\underline{x} = l$. Projection on lists are mapped to their elements, - i.e. - $\underline{x}^{\downarrow1} = [x_{1}^{\downarrow1}, \dots, x_{n}^{\downarrow1}]$. - \item $\sortOn : i \to \mathcal{A}^{*} \to \mathcal{A}^{*}$ does sort a list of - values on the $i$th projection. - \item $\tyData$ is a universal data type of nested sums and products built up - recursively from the base types of $\tyInteger$ and $\tyBytes$. -\end{itemize} - -\subsection{Public key multi-signature scheme}\label{sec:multisig} -% TODO: move/merge with protocol setup and make concrete -\noindent A multisignature scheme is a set of algorithms where -\begin{itemize} - \item $\msSetup$ generates public parameters $\msParams$, such that - \item $(\msVK,\msSK) \gets \msKeyGen(\msParams)$ can be used to generate fresh - key pairs, - \item $\msSig \gets \msSign(\msParams,\msSK,\msMsg)$ signs a message $\msMsg$ - using key $\msSK$, - \item $\msCVK \gets \msCombVK(\msParams,\msVKL)$ aggregates a list of - verification keys $\msVKL$ into a single, aggregate key $\msCVK$, - \item $\msCSig \gets \msComb(\msParams,\msMsg,\msVKL,\msSigL)$ aggregates a - list of signatures $\msSigL$ about message $m$ into a single, aggregate - signature~$\msCSig$. - \item $\msVfy(\msParams,\msCVK,\msMsg,\msCSig) \in \tyBool$ verifies an aggregate - signature $\msCSig$ of message $\msMsg$ under an aggregate verification - key $\msCVK$. -\end{itemize} - -The security definition of a multisignature scheme -from~\cite{itakura1983public,CCS:MicOhtRey01} guarantees that, if $\msCVK$ is -produced from a tuple of verification keys $\msVKL$ via $\msCombVK$, then no -aggregate signature $\msCSig$ can pass verification -$\msVfy(\msCVK,\msMsg,\msCSig)$ unless all honest parties holding keys in -$\msVKL$ signed $m$. - -Note that in the following, we make the parameter~$\msParams$ implicit and leave -out the $ver$ suffix for verification key such that $k = k^{ver}$ for better -readability. - -\subsection{Extended UTxO}\label{sec:eutxo} -The Hydra Head protocol is specified to work on the so-called Extended UTxO (EUTxO) ledgers -like Cardano. - -The basis for EUTxO is Bitcoin's UTxO ledger -model~\cite{formal-model-of-bitcoin-transactions,Zahnentferner18-UTxO}. -Intuitively, it arranges transactions in a directed acyclic graph, such as the -one in Figure~\ref{fig:utxo-graph}, where boxes represent transactions with -(red) inputs to the left and (black) outputs to the right. A dangling -(unconnected) output is an \emph{unspent transaction output (UTxO)} --- there -are two UTxOs in the figure. - -\begin{figure}[h] - \centering - \includegraphics[width=0.5\textwidth]{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 deleted file mode 100644 index ac26a9480c7..00000000000 --- a/spec/security.tex +++ /dev/null @@ -1,209 +0,0 @@ -\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 deleted file mode 100644 index 9d6e3ea4a22..00000000000 --- a/spec/setup.tex +++ /dev/null @@ -1,46 +0,0 @@ -\clearpage -\section{Protocol Setup}\label{sec:setup} -In order to create a head-protocol instance, an initiator invites a set of -participants (the initiator being one of them) to join by announcing to them the -protocol parameters. - -\begin{itemize} - \item For on-chain transaction authentication (Cardano) purposes, each party - $\party_i$ generates a corresponding key pair $(\msVK_{i},\msSK_{i})$ - and sends their verification key $\msVK_{i}$ to all other parties. In - the case of Cardano, these are Ed25519 keys. - - \item For off-chain signing (Hydra) purposes, a very basic multisignature scheme (MS, as defined in Section~\ref{sec:multisig}) based on EdDSA using Ed25519 keys is used: - \begin{itemize} - \item $\msKeyGen$ is Ed25519 key generation (requires no parameters) - \item $\msSign$ creates an EdDSA signature - \item $\msCombVK$ is concatenation of verification keys into an ordered list - \item $\msComb$ is concatenation of signatures into an ordered list - \item $\msVfy$ verifies the "aggregate" signature by verifying each individual EdDSA signature under the corresponding Ed25519 verification key - \end{itemize} - - To help distinguish on- and off-chain key sets, Cardano verification - keys are written $\cardanoKey$, while Hydra verification keys are - indicated as $\hydraKey$ for the remainder of this document. - - % TODO: Move this and previous bullet point into the preliminary section, or all multi-sig definition here? - - \item Each party $\party_i$ generates a hydra key pair and sends their hydra verification key to all other parties. - - \item Each party $\party_i$ computes the aggregate key from the received verification keys, stores the aggregate key, - their signing key as well as the number of participants $\nop$. - - \item Each party establishes pairwise communication channels to all other parties. That is, every network message received from a specific party is checked for (channel) authentication. It is the implementer’s duty to find a suitable authentication process for the communication channels. - - \item All parties agree on a contestation period $\cPer$. -\end{itemize} - -If any of the above fails (or the party does not agree to join the head in the -first place), the party aborts the initiation protocol and ignores any further -action. Finally, at least one of the participants posts the \mtxInit{} transaction -onchain as described next in Section~\ref{sec:on-chain}. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "main" -%%% End: diff --git a/spec/short.bib b/spec/short.bib deleted file mode 100644 index e4e7a769920..00000000000 --- a/spec/short.bib +++ /dev/null @@ -1,122 +0,0 @@ -%% 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 -}