From 5c59c23617f834e783bc68a8686e650f8b418da6 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Mon, 8 Oct 2018 10:43:17 -0400 Subject: [PATCH 1/5] initial draft for scripts and multicurrency --- specs/scripts/latex/Makefile | 42 ++ specs/scripts/latex/references.bib | 14 + specs/scripts/latex/scripts-multicurrency.tex | 410 ++++++++++++++++++ specs/scripts/latex/shell.nix | 24 + 4 files changed, 490 insertions(+) create mode 100644 specs/scripts/latex/Makefile create mode 100644 specs/scripts/latex/references.bib create mode 100644 specs/scripts/latex/scripts-multicurrency.tex create mode 100644 specs/scripts/latex/shell.nix diff --git a/specs/scripts/latex/Makefile b/specs/scripts/latex/Makefile new file mode 100644 index 00000000000..9633d733a5d --- /dev/null +++ b/specs/scripts/latex/Makefile @@ -0,0 +1,42 @@ +## +## Makefile for a specification of the delegation rules, based on: +## +## https://tex.stackexchange.com/questions/40738/how-to-properly-make-a-latex-project +## + +# Document name +DOCNAME = scripts-multicurrency + +# You want latexmk to *always* run, because make does not have all the info. +# Also, include non-file targets in .PHONY so they are run regardless of any +# file of the given name existing. +.PHONY: $(DOCNAME).pdf all clean + +# The first rule in a Makefile is the one executed by default ("make"). It +# should always be the "all" rule, so that "make" and "make all" are identical. +all: $(DOCNAME).pdf + +## +## CUSTOM BUILD RULES +## + + +## +## MAIN LATEXMK RULE +## + +# -pdf tells latexmk to generate PDF directly (instead of DVI). +# -pdflatex="" tells latexmk to call a specific backend with specific options. +# -use-make tells latexmk to call make for generating missing files. + +# -interaction=nonstopmode keeps the pdflatex backend from stopping at a +# missing file reference and interactively asking you for an alternative. + +$(DOCNAME).pdf: $(DOCNAME).tex + latexmk -pdf -pdflatex="pdflatex -interaction=nonstopmode" -use-make $(DOCNAME).tex + +watch: $(DOCNAME).tex + latexmk -pvc -pdf -pdflatex="pdflatex -interaction=nonstopmode" -use-make $(DOCNAME).tex + +clean: + latexmk -CA diff --git a/specs/scripts/latex/references.bib b/specs/scripts/latex/references.bib new file mode 100644 index 00000000000..9656f1fea4d --- /dev/null +++ b/specs/scripts/latex/references.bib @@ -0,0 +1,14 @@ +@article{utxo_scripts, + author = {Joachim Zahnentferner}, + title = {An Abstract Model of UTxO-based Cryptocurrencies with Scripts}, + journal = {Cryptology ePrint Archive, Report 2018/469}, + year = {2018}, + url = {https://eprint.iacr.org/2018/469}, +} + +@article{multi_currency, + author = {Joachim Zahnentferner}, + title = {Multi-Currency Ledgers}, + journal = {??}, + year = {2018}, +} diff --git a/specs/scripts/latex/scripts-multicurrency.tex b/specs/scripts/latex/scripts-multicurrency.tex new file mode 100644 index 00000000000..4aba18f101a --- /dev/null +++ b/specs/scripts/latex/scripts-multicurrency.tex @@ -0,0 +1,410 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[margin=2.5cm]{geometry} +\usepackage{microtype} +\usepackage{mathpazo} % nice fonts +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{latexsym} +\usepackage{mathtools} +\usepackage{stmaryrd} +\usepackage{extarrows} +\usepackage{slashed} +\usepackage[colon]{natbib} +\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes} +\usepackage[unicode=true,pdftex,pdfa]{hyperref} +\usepackage[capitalise,noabbrev,nameinlink]{cleveref} +\hypersetup{ + pdftitle={A Formal Specification of a UTxO Ledger with Scripts and Multi-Currency}, + breaklinks=true, + bookmarks=true, + colorlinks=false, + linkcolor={blue}, + citecolor={blue}, + urlcolor={blue}, + linkbordercolor={white}, + citebordercolor={white}, + urlbordercolor={white} +} +\usepackage{float} +\floatstyle{boxed} +\restylefloat{figure} + +%% +%% Package `semantic` can be used for writing inference rules. +%% +\usepackage{semantic} +%% Setup for the semantic package +\setpremisesspace{20pt} + +\DeclareMathOperator{\dom}{dom} +\DeclareMathOperator{\range}{range} + +%% +%% TODO: we should package this +%% +\newcommand{\powerset}[1]{\mathbb{P}~#1} +\newcommand{\restrictdom}{\lhd} +\newcommand{\subtractdom}{\mathbin{\slashed{\restrictdom}}} +\newcommand{\restrictrange}{\rhd} +\newcommand{\union}{\cup} +\newcommand{\unionoverride}{\mathbin{\underrightarrow\cup}} +\newcommand{\uniondistinct}{\uplus} +\newcommand{\var}[1]{\mathit{#1}} +\newcommand{\fun}[1]{\mathsf{#1}} +\newcommand{\type}[1]{\mathsf{#1}} +\newcommand{\signed}[2]{\llbracket #1 \rrbracket_{#2}} +\newcommand{\size}[1]{\left| #1 \right|} +\newcommand{\trans}[2]{\xlongrightarrow[\textsc{#1}]{#2}} +\newcommand{\seqof}[1]{#1^{*}} +\newcommand{\nextdef}{\\[1em]} + +%% +%% Types +%% +\newcommand{\Tx}{\type{Tx}} +\newcommand{\UTxO}{\type{UTxO}} +\newcommand{\Value}{\type{Value}} +% Adding witnesses +\newcommand{\TxIn}{\type{TxIn}} +\newcommand{\TxOut}{\type{TxOut}} +\newcommand{\VKey}{\type{VKey}} +\newcommand{\Sig}{\type{Sig}} +\newcommand{\Data}{\type{Data}} +\newcommand{\Hash}{\type{Hash}} + +% Scripts +\newcommand{\ScrEval}[1]{[\![ #1 ]\!]} + +%% +%% Functions +%% +\newcommand{\txins}[1]{\fun{txins}\ \var{#1}} +\newcommand{\txouts}[1]{\fun{txouts}\ \var{#1}} +\newcommand{\values}[1]{\fun{values}\ #1} +\newcommand{\balance}[1]{\fun{balance}\ \var{#1}} +% Adding witnesses... +\newcommand{\inputs}[1]{\fun{inputs}\ \var{#1}} +\newcommand{\witnesses}[1]{\fun{witnesses}\ \var{#1}} +\newcommand{\verify}[3]{\fun{verify} ~ #1 ~ #2 ~ #3} +\newcommand{\serialised}[1]{\llbracket \var{#1} \rrbracket} +\newcommand{\addr}[1]{\fun{addr}\ \var{#1}} +\newcommand{\hash}[1]{\fun{hash}\ \var{#1}} +\newcommand{\inout}[3]{\var{#1}\mapsto_{#2}\var{#3}} +% Adding ledgers... +\newcommand{\utxo}[1]{\fun{utxo}\ #1} + +\begin{document} + +\title{A Formal Specification of a \\ + UTxO Ledger with Scripts and Multi-Currency} + +\author{} + +%\date{} + +\maketitle + +\begin{abstract} + This documents specifies the rules for a multi-currency UTxO ledger with scripts, as described in \cite{multi_currency} and \cite{utxo_scripts}. +\end{abstract} + +\tableofcontents +\listoffigures + +\section{Types} + +[TODO explain scripts, figure 1]. +\todo{these scripts probably also need to take a transaction} + +[TODO explain basic types, figure 2]. + +[TODO explain basic UTxO operations, figure 3]. + +[TODO explain ledger state, figure 4]. + +[TODO explain Mutli-currency operations]. + +\begin{figure} +\emph{Scripts} +% +\begin{equation*} +\begin{array}{r@{~\in~}l@{~,~}r@{~:~}l} + \var{validator} +& \type{Script} +& \ScrEval{validator} +& \type{LedgerState} \mapsto \type{T} \mapsto \type{Bool} +\\ + \var{redeemer} +& \type{Script} +& \ScrEval{redeemer} +& \type{LedgerState} \mapsto \type{T} +\end{array} +\end{equation*} +\caption{Scripts} +\label{fig:scripts} +\end{figure} + + +\begin{figure} + +\emph{Primitive types} +% +\begin{equation*} +\begin{array}{r@{~\in~}lr} + \var{txid} +& \type{TxId} +& \text{transaction id} +\\ + ix +& \type{Ix} +& \text{index} +\\ + \var{addr} +& \type{Addr} +& \text{address} +\\ + curr +& \type{Currency} +& \text{currency identifier} +\\ + qty +& \type{Quantity} +& \text{currency quantity} +\end{array} +\end{equation*} + +% +\emph{Derived types} +% +\begin{equation*} +\begin{array}{r@{~=~}lc@{}r@{~\in~}l} + \type{Value} +& \type{Currency} \mapsto \type{Quantity} +& +& (\var{curr}, \var{qty}) +& \type{Value} +\\ + \type{TxIn} +& \type{TxId} \times \type{Ix} \times \type{Script} \times \type{Script} +& +& (\var{txid}, \var{ix}, \var{validator}, \var{redeemer}) +& \type{TxIn} +\\ + \type{TxOut} +& \type{Addr} \times \type{Value} +& +& (\var{addr}, v) +& \type{TxOut} +\\ + \type{UTxO} +& \type{TxIn} \mapsto \type{TxOut} +& +& \var{txin} \mapsto \var{txout} \in \var{utxo} +& \type{UTxO} +\\ + \type{Create} +& \type{Optional} (\type{Currency} \times \type{Script}) +& +& (\var{currency}, \var{validator}) +& \type{Create} +\\ + \type{Forge} +& \type{Value} \times (\type{Currency} \mapsto \type{Script}) +& +& (\var{value}, \var{curr} \mapsto \var{redeemer}) +& \type{Forge} +\\ + \type{Tx} +& \powerset{\type{TxIn}} \times (\type{Ix} \mapsto + \type{TxOut}) \times \type{Forge} \times \type{Value} +& +& (\var{txins}, \var{txouts}, \var{forge}, \var{fee}) +& \type{Tx} +\end{array} +\end{equation*} +% +\emph{Functions} +% +\begin{equation*} +\begin{array}{lr} + \fun{txid} \in \type{Tx} \to \type{TxId} +& \text{compute transaction id} +\\ + \fun{hash} \in \type{Script} \to \type{Addr} +& \text{compute script address} +\\ + \fun{forged} \in \type{Tx} \to \type{Value} +& \text{the forged multi-currency in a transaction} +\\ + \fun{fee} \in \type{Tx} \to \type{Value} +& \text{the fees in a transaction} +\end{array} +\end{equation*} + +\caption{Basic Definitions} +\label{fig:basic_definitions} +\end{figure} + + +\begin{figure} +\begin{align*} +& \fun{txins} \in \type{Tx} \to \powerset{\type{TxIn}} +& \text{transaction inputs} \\ +& \fun{txins} ~ (\var{txins}, \_, \_, \_) = \var{txins} +\\[1em] +& \fun{txouts} \in \type{Tx} \to \type{UTxO} +& \text{transaction outputs as UTxO} \\ +& \fun{txouts} ~ \var{tx} = + \left\{ (\fun{txid} ~ \var{tx}, \var{ix}) \mapsto \var{txout} ~ + \middle| \begin{array}{l@{~}c@{~}l} + (\_, \var{txouts},\_, \_) & = & \var{tx} \\ + \var{ix} \mapsto \var{txout} & \in & \var{txouts} + \end{array} + \right\} +\\[1em] +& \fun{outRefs} \in \type{Tx} \to \powerset({\type{TxId} \times \type{Ix}}) +& \text{Output References} \\ + & \fun{outRefs} ~ (\var{txins}, \_, \_, \_) + = \left\{ (id, ix) \middle| (id, ix, \_, \_) \in txins\right\} +\\[1em] +& \fun{balance} \in \type{UTxO} \to \type{Value} +& \text{UTxO balance} \\ +& \fun{balance} ~ utxo = \sum_{(\_ ~ \mapsto (\_, v)) \in \var{utxo}} v +\end{align*} +\caption{Operations on transactions and UTxOs} +\label{fig:auxiliary_ops} +\end{figure} + + +\begin{figure} + +\emph{Ledger State} +% +\begin{equation*} +\begin{array}{r@{~\in~}lr} +utxo & \type{UTxO} & \text{unspent outputs} +\\ +currencies & \type{Currency} \mapsto \type{Script} + & \text{created currencies with policies} +\\ +totalMinted & \type{Value} & \text{total currency minted} +\\ +slot & \type{Slot} & \text{current slot} + +\end{array} +\end{equation*} +% +\emph{Initial Ledger State} +% +\begin{equation*} +\begin{array}{llllll} +utxo = \emptyset + & currencies = \emptyset + & totalMinted = \vec{0} + & slot = 0 +\end{array} +\end{equation*} + +\caption{Ledger State (Delegation in Isolation)} +\label{fig:delegation_ledger_state} +\end{figure} + +\section{Validation} + +\begin{figure} +\emph{Valid Inputs} +% +\begin{equation*} +\txins{tx} \subseteq \dom \var{utxo} +\end{equation*} + +\emph{Preservation of Value} +% +\begin{equation*} +balance (\txouts tx) + (\fun{fee}\ tx) + = balance (\txins tx \restrictdom utxo) + (\fun{forged} ~ tx) +\end{equation*} + +\emph{No Double Spend} +% +\begin{equation*} +\lvert \txins tx \rvert = \lvert \fun{outRefs} ~ tx\rvert +\end{equation*} + +\emph{Scripts Validate} +% +\begin{equation*} +\forall i\in(\txins tx), + \ScrEval{i.validator} + \left(ledgerState, \ScrEval{i.redeemer}\left(ledgerState\right)\right) = True +\end{equation*} + +\emph{Authorized} +% +\begin{equation*} +\forall i\in(\txins tx), + \fun{hash}(i.validator) = (utxo ~ i).addr +\end{equation*} + +\emph{Forge Obeys Policy} +% +\begin{equation*} +\forall c\in(tx.forge.value), + \ScrEval{currencies[c]} + \left(ledgerState, \ScrEval{tx.forge.proof[c]}\left(ledgerState\right)\right) = True +\end{equation*} + +\emph{Create Only New Currencies} +% +\begin{equation*} +tx.create.currency \notin currencies +\end{equation*} + +\caption{Validation Rules} +\label{fig:validation_rules} +\end{figure} + +\section{Disabling Multi-Currency} + +If we want to disable multi-currency, we can remove the validation rules: ``Forge Obeys Policy" and ``Create Only New Currencies", +and add: +\begin{figure} +\emph{Only ADA} +% +\begin{equation*} +tx.create.currency = \mathsf{ADA} +\end{equation*} + +\caption{Only ADA Rule} +\label{fig:validation_rules} +\end{figure} + +\todo[inline]{We need to think carefully about how to handle similar names, +like ``ada", ``Ada", and ``ADA".} + +\section{Disabling Scripts} + +WIP - We should probably make two types of addresses, pay-to-pubkey addresses and script addresses. +The pay-to-pubkey addresses will work similiarly to the validation rules defined above, with the +following changes: + +``Scripts Validate" becomes a specific validatior/redeemer pair, where $\mathsf{validator}$ checks a +digital signature and $\mathsf{redeemer}$ is the constant function returning the signature of the +transaction body. + +``Authorized" is nearly the same, except we hash the stake key instead of the validator script. + +``No Double Spend" is no longer needed. + +\section{Extended UTxO} + +The main documentation is \href{https://github.com/input-output-hk/plutus/tree/master/docs/extended-utxo}{here}. +Do we only need to add the data script to TxOut? +$$ \type{TxOut} = \type{Addr} \times \type{Value} \times \type{Script} $$ +How is this more expressive than what we already have? + +\addcontentsline{toc}{section}{References} +\bibliographystyle{plainnat} +\bibliography{references} + +\end{document} diff --git a/specs/scripts/latex/shell.nix b/specs/scripts/latex/shell.nix new file mode 100644 index 00000000000..1766e33273f --- /dev/null +++ b/specs/scripts/latex/shell.nix @@ -0,0 +1,24 @@ +with (import {}); +stdenv.mkDerivation { + name = "docsEnv"; + buildInputs = [ (texlive.combine { + inherit (texlive) + scheme-small + + # libraries + stmaryrd lm-math amsmath + extarrows cleveref semantic + + # font libraries `mathpazo` seems to depend on palatino, but it isn't pulled. + mathpazo palatino microtype + + # libraries for marginal notes + xargs todonotes + + # build tools + latexmk + + ; + }) + ]; +} From fb3365865c53d86eb96ca91a7e1e5ac62630a975 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 9 Oct 2018 09:38:53 -0400 Subject: [PATCH 2/5] fixup! initial draft for scripts and multicurrency --- specs/scripts/latex/scripts-multicurrency.tex | 269 ++++++++++-------- 1 file changed, 158 insertions(+), 111 deletions(-) diff --git a/specs/scripts/latex/scripts-multicurrency.tex b/specs/scripts/latex/scripts-multicurrency.tex index 4aba18f101a..1cefff73e7a 100644 --- a/specs/scripts/latex/scripts-multicurrency.tex +++ b/specs/scripts/latex/scripts-multicurrency.tex @@ -16,7 +16,6 @@ \hypersetup{ pdftitle={A Formal Specification of a UTxO Ledger with Scripts and Multi-Currency}, breaklinks=true, - bookmarks=true, colorlinks=false, linkcolor={blue}, citecolor={blue}, @@ -29,13 +28,6 @@ \floatstyle{boxed} \restylefloat{figure} -%% -%% Package `semantic` can be used for writing inference rules. -%% -\usepackage{semantic} -%% Setup for the semantic package -\setpremisesspace{20pt} - \DeclareMathOperator{\dom}{dom} \DeclareMathOperator{\range}{range} @@ -61,37 +53,41 @@ %% %% Types %% -\newcommand{\Tx}{\type{Tx}} -\newcommand{\UTxO}{\type{UTxO}} +\newcommand{\Bool}{\type{Bool}} +\newcommand{\Slot}{\type{Slot}} +\newcommand{\Script}{\type{Script}} +\newcommand{\TxId}{\type{TxId}} +\newcommand{\Ix}{\type{Ix}} +\newcommand{\Addr}{\type{Addr}} +\newcommand{\Currency}{\type{Currency}} +\newcommand{\Quantity}{\type{Quantity}} \newcommand{\Value}{\type{Value}} -% Adding witnesses \newcommand{\TxIn}{\type{TxIn}} \newcommand{\TxOut}{\type{TxOut}} -\newcommand{\VKey}{\type{VKey}} -\newcommand{\Sig}{\type{Sig}} -\newcommand{\Data}{\type{Data}} -\newcommand{\Hash}{\type{Hash}} +\newcommand{\UTxO}{\type{UTxO}} +\newcommand{\Create}{\type{Create}} +\newcommand{\Forge}{\type{Forge}} +\newcommand{\TxBody}{\type{TxBody}} +\newcommand{\Tx}{\type{Tx}} +%% % Scripts -\newcommand{\ScrEval}[1]{[\![ #1 ]\!]} +%% +\newcommand{\ScriptEval}[1]{[\![ #1 ]\!]} %% %% Functions %% +\newcommand{\scriptValidate}[3]{\fun{scriptValidate} ~ \var{#1} ~ \var{#2} ~ \var{#3}} +\newcommand{\txid}[1]{\fun{txid}\ \var{#1}} \newcommand{\txins}[1]{\fun{txins}\ \var{#1}} \newcommand{\txouts}[1]{\fun{txouts}\ \var{#1}} -\newcommand{\values}[1]{\fun{values}\ #1} -\newcommand{\balance}[1]{\fun{balance}\ \var{#1}} -% Adding witnesses... -\newcommand{\inputs}[1]{\fun{inputs}\ \var{#1}} -\newcommand{\witnesses}[1]{\fun{witnesses}\ \var{#1}} -\newcommand{\verify}[3]{\fun{verify} ~ #1 ~ #2 ~ #3} -\newcommand{\serialised}[1]{\llbracket \var{#1} \rrbracket} -\newcommand{\addr}[1]{\fun{addr}\ \var{#1}} \newcommand{\hash}[1]{\fun{hash}\ \var{#1}} -\newcommand{\inout}[3]{\var{#1}\mapsto_{#2}\var{#3}} -% Adding ledgers... -\newcommand{\utxo}[1]{\fun{utxo}\ #1} +\newcommand{\forged}[1]{\fun{forged}\ \var{#1}} +\newcommand{\forgeReedemers}[1]{\fun{forgeReedemers}\ \var{#1}} +\newcommand{\fee}[1]{\fun{fee}\ \var{#1}} +\newcommand{\created}[1]{\fun{forged}\ \var{#1}} +\newcommand{\outRefs}[1]{\fun{outRefs}\ \var{#1}} \begin{document} @@ -105,7 +101,7 @@ \maketitle \begin{abstract} - This documents specifies the rules for a multi-currency UTxO ledger with scripts, as described in \cite{multi_currency} and \cite{utxo_scripts}. +This documents specifies the rules for a multi-currency UTxO ledger with scripts, as described in \cite{multi_currency} and \cite{utxo_scripts}. \end{abstract} \tableofcontents @@ -113,14 +109,16 @@ \section{Types} -[TODO explain scripts, figure 1]. -\todo{these scripts probably also need to take a transaction} +[TODO explain scripts, \cref{fig:scripts}]. +\todo{these scripts probably also need to take some of the data in transaction} -[TODO explain basic types, figure 2]. +[TODO explain basic types, \cref{fig:basic_definitions}]. -[TODO explain basic UTxO operations, figure 3]. +[TODO explain basic UTxO operations, \cref{fig:auxiliary_ops}]. -[TODO explain ledger state, figure 4]. +[TODO explain validation, \cref{fig:validation_rules}]. + +[TODO explain ledger state, \cref{fig:ledger_state}]. [TODO explain Mutli-currency operations]. @@ -130,16 +128,29 @@ \section{Types} \begin{equation*} \begin{array}{r@{~\in~}l@{~,~}r@{~:~}l} \var{validator} -& \type{Script} -& \ScrEval{validator} -& \type{LedgerState} \mapsto \type{T} \mapsto \type{Bool} +& \Script +& \ScriptEval{validator} +& \type{LedgerState} \mapsto \type{R} \mapsto \Bool \\ \var{redeemer} -& \type{Script} -& \ScrEval{redeemer} -& \type{LedgerState} \mapsto \type{T} +& \Script +& \ScriptEval{redeemer} +& \type{LedgerState} \mapsto \type{R} \end{array} \end{equation*} + +~ ~ ~ \text{where} \type{R} + \text{is an arbitrary type, but must be the same for each validator/redeemer pair.} +\\ + +\emph{Script Operations} +\begin{align*} +& \fun{scriptValidate} \in + \type{LedgerState} \times \Script \times \Script \mapsto \Bool \\ +& \scriptValidate{st}{validator}{redeemer} = +\ScriptEval{validator} \left(st, \ScriptEval{redeemer}\left(st\right)\right) +\end{align*} + \caption{Scripts} \label{fig:scripts} \end{figure} @@ -152,23 +163,23 @@ \section{Types} \begin{equation*} \begin{array}{r@{~\in~}lr} \var{txid} -& \type{TxId} +& \TxId & \text{transaction id} \\ ix -& \type{Ix} +& \Ix & \text{index} \\ \var{addr} -& \type{Addr} +& Addr & \text{address} \\ curr -& \type{Currency} +& \Currency & \text{currency identifier} \\ qty -& \type{Quantity} +& \Quantity & \text{currency quantity} \end{array} \end{equation*} @@ -178,48 +189,53 @@ \section{Types} % \begin{equation*} \begin{array}{r@{~=~}lc@{}r@{~\in~}l} - \type{Value} -& \type{Currency} \mapsto \type{Quantity} + \Value +& \Currency \mapsto \Quantity & & (\var{curr}, \var{qty}) -& \type{Value} +& \Value \\ - \type{TxIn} -& \type{TxId} \times \type{Ix} \times \type{Script} \times \type{Script} + \TxIn +& \TxId \times \Ix \times \Script \times \Script & & (\var{txid}, \var{ix}, \var{validator}, \var{redeemer}) -& \type{TxIn} +& \TxIn \\ - \type{TxOut} -& \type{Addr} \times \type{Value} + \TxOut +& \Addr \times \Value & & (\var{addr}, v) -& \type{TxOut} +& \TxOut \\ - \type{UTxO} -& \type{TxIn} \mapsto \type{TxOut} + \UTxO +& \TxIn \mapsto \TxOut & & \var{txin} \mapsto \var{txout} \in \var{utxo} -& \type{UTxO} +& \UTxO \\ - \type{Create} -& \type{Optional} (\type{Currency} \times \type{Script}) + \Create +& \type{Optional} (\Currency \times \Script) & & (\var{currency}, \var{validator}) -& \type{Create} +& \Create \\ - \type{Forge} -& \type{Value} \times (\type{Currency} \mapsto \type{Script}) + \Forge +& \Value \times (\Currency \mapsto \Script) & & (\var{value}, \var{curr} \mapsto \var{redeemer}) -& \type{Forge} +& \Forge \\ - \type{Tx} -& \powerset{\type{TxIn}} \times (\type{Ix} \mapsto - \type{TxOut}) \times \type{Forge} \times \type{Value} + \TxBody +& \powerset{\TxIn} \times (\Ix \mapsto \TxOut) & -& (\var{txins}, \var{txouts}, \var{forge}, \var{fee}) -& \type{Tx} +& (\var{txins}, \var{txouts}) +& \TxBody +\\ + \Tx +& \TxBody \times \Forge \times \Value \times \Create +& +& (\var{txbody}, \var{forge}, \var{fee}, \var{create}) +& \Tx \end{array} \end{equation*} % @@ -227,17 +243,11 @@ \section{Types} % \begin{equation*} \begin{array}{lr} - \fun{txid} \in \type{Tx} \to \type{TxId} + \fun{txid} \in \Tx \to \TxId & \text{compute transaction id} \\ - \fun{hash} \in \type{Script} \to \type{Addr} + \fun{hash} \in \Script \to \Addr & \text{compute script address} -\\ - \fun{forged} \in \type{Tx} \to \type{Value} -& \text{the forged multi-currency in a transaction} -\\ - \fun{fee} \in \type{Tx} \to \type{Value} -& \text{the fees in a transaction} \end{array} \end{equation*} @@ -248,28 +258,44 @@ \section{Types} \begin{figure} \begin{align*} -& \fun{txins} \in \type{Tx} \to \powerset{\type{TxIn}} +& \fun{txins} \in \Tx \to \powerset{\TxIn} & \text{transaction inputs} \\ -& \fun{txins} ~ (\var{txins}, \_, \_, \_) = \var{txins} +& \fun{txins} ~ ((\var{txins}, \_), \_, \_, \_) = \var{txins} \\[1em] -& \fun{txouts} \in \type{Tx} \to \type{UTxO} +& \fun{txouts} \in \Tx \to \UTxO & \text{transaction outputs as UTxO} \\ & \fun{txouts} ~ \var{tx} = \left\{ (\fun{txid} ~ \var{tx}, \var{ix}) \mapsto \var{txout} ~ \middle| \begin{array}{l@{~}c@{~}l} - (\_, \var{txouts},\_, \_) & = & \var{tx} \\ + ((\_, \var{txouts}),\_, \_, \_) & = & \var{tx} \\ \var{ix} \mapsto \var{txout} & \in & \var{txouts} \end{array} \right\} \\[1em] -& \fun{outRefs} \in \type{Tx} \to \powerset({\type{TxId} \times \type{Ix}}) +& \fun{outRefs} \in \Tx \to \powerset({\TxId \times \Ix}) & \text{Output References} \\ - & \fun{outRefs} ~ (\var{txins}, \_, \_, \_) - = \left\{ (id, ix) \middle| (id, ix, \_, \_) \in txins\right\} +& \fun{outRefs} ~ ((\var{txins}, \_), \_, \_, \_) += \left\{ (id, ix) \middle| (id, ix, \_, \_) \in txins\right\} \\[1em] -& \fun{balance} \in \type{UTxO} \to \type{Value} +& \fun{balance} \in \UTxO \to \Value & \text{UTxO balance} \\ & \fun{balance} ~ utxo = \sum_{(\_ ~ \mapsto (\_, v)) \in \var{utxo}} v +\\[1em] +& \fun{created} \in \Tx \to \Create +& \text{created currency} \\ +& \fun{created} ~ (\_, \_, \_, create) = \var{create} +\\[1em] +& \fun{forged} \in \Tx \to \Value +& \text{the forged multi-currency} \\ +& \fun{forged} ~ (\_, (value, \_), \_, \_) = \var{value} +\\[1em] +& \fun{forgeReedemers} \in \Tx \to \Script +& \text{redeemer scripts for forging} \\ +& \fun{forgeReedemers} ~ ( \_, (\_, \var{redeemers}), \_, \_) = reedemers +\\[1em] +& \fun{fee} \in \Tx \to \Value +& \text{the fees in a transaction} \\ +& \fun{fee} ~ (\_, \_, fee, \_) = \var{fee} \end{align*} \caption{Operations on transactions and UTxOs} \label{fig:auxiliary_ops} @@ -282,14 +308,14 @@ \section{Types} % \begin{equation*} \begin{array}{r@{~\in~}lr} -utxo & \type{UTxO} & \text{unspent outputs} +utxo & \UTxO & \text{unspent outputs} \\ -currencies & \type{Currency} \mapsto \type{Script} - & \text{created currencies with policies} +currencies & \Currency \mapsto \Script + & \text{currencies with policies} \\ -totalMinted & \type{Value} & \text{total currency minted} +totalMinted & \Value & \text{total currency minted} \\ -slot & \type{Slot} & \text{current slot} +slot & \Slot & \text{current slot} \end{array} \end{equation*} @@ -305,11 +331,12 @@ \section{Types} \end{array} \end{equation*} -\caption{Ledger State (Delegation in Isolation)} -\label{fig:delegation_ledger_state} +\caption{Ledger State} +\label{fig:ledger_state} \end{figure} \section{Validation} +See figure \cref{fig:validation_rules} \begin{figure} \emph{Valid Inputs} @@ -321,62 +348,81 @@ \section{Validation} \emph{Preservation of Value} % \begin{equation*} -balance (\txouts tx) + (\fun{fee}\ tx) - = balance (\txins tx \restrictdom utxo) + (\fun{forged} ~ tx) +balance (\txouts tx) + (\fee tx) + = balance (\txins tx \restrictdom utxo) + (\forged tx) \end{equation*} \emph{No Double Spend} % \begin{equation*} -\lvert \txins tx \rvert = \lvert \fun{outRefs} ~ tx\rvert +\lvert \txins tx \rvert = \lvert \outRefs tx\rvert \end{equation*} \emph{Scripts Validate} % \begin{equation*} -\forall i\in(\txins tx), - \ScrEval{i.validator} - \left(ledgerState, \ScrEval{i.redeemer}\left(ledgerState\right)\right) = True +\forall (\_, \_, validator, redeemer)\in(\txins tx), +~ \scriptValidate{state}{validator}{redeemer} \end{equation*} \emph{Authorized} % \begin{equation*} -\forall i\in(\txins tx), - \fun{hash}(i.validator) = (utxo ~ i).addr + \forall (\_, \_, validator, \_)\in(\txins tx), + (i \mapsto (addr, \_)) \in \var{utxo} \land \hash validator = addr \end{equation*} \emph{Forge Obeys Policy} % \begin{equation*} -\forall c\in(tx.forge.value), - \ScrEval{currencies[c]} - \left(ledgerState, \ScrEval{tx.forge.proof[c]}\left(ledgerState\right)\right) = True +\begin{array}{c} +\forall c\in(\forged tx), \\ +\exists policy, (c, policy) \in \var{currencies} \\ +\exists reedemer, (c, reedemer) \in \forgeReedemers tx \\ +\scriptValidate{state}{policy}{redeemer} +\end{array} \end{equation*} \emph{Create Only New Currencies} % \begin{equation*} -tx.create.currency \notin currencies +\created tx = (curr, policy), curr \notin \dom currencies \end{equation*} \caption{Validation Rules} \label{fig:validation_rules} \end{figure} +\section{State Transformations} +See figure \cref{fig:state_transitions} + +\begin{figure} +\begin{equation*} + \begin{array}{rcl} + \var{utxo} & & (\txins tx \subtractdom \var{utxo}) \union \txouts tx \\ + \var{currencies} & \longrightarrow & \var{currencies} \union (\created tx) \\ + \var{totalMinted} & & \var{totalMinted} + (\forged tx)\\ + \var{slot} & & \var{slot} \\ + \end{array} +\end{equation*} + +\caption{State transition} +\label{fig:state_transitions} +\end{figure} + \section{Disabling Multi-Currency} -If we want to disable multi-currency, we can remove the validation rules: ``Forge Obeys Policy" and ``Create Only New Currencies", -and add: +If we want to disable multi-currency, we can remove the ``Forge Obeys Policy" rule and +add \cref{fig:only_ada_rule} \begin{figure} \emph{Only ADA} % \begin{equation*} -tx.create.currency = \mathsf{ADA} +\created tx = (curr, policy), curr = \mathsf{ADA} \end{equation*} \caption{Only ADA Rule} -\label{fig:validation_rules} +\label{fig:only_ada_rule} \end{figure} \todo[inline]{We need to think carefully about how to handle similar names, @@ -388,9 +434,9 @@ \section{Disabling Scripts} The pay-to-pubkey addresses will work similiarly to the validation rules defined above, with the following changes: -``Scripts Validate" becomes a specific validatior/redeemer pair, where $\mathsf{validator}$ checks a -digital signature and $\mathsf{redeemer}$ is the constant function returning the signature of the -transaction body. +"Scripts Validate" becomes a specific validator/redeemer pair, where $\mathsf{validator}$ checks a +digital signature and $\mathsf{redeemer}$ is the constant function returning a signature of the +part of transaction (perhaps $\outRefs tx$?). ``Authorized" is nearly the same, except we hash the stake key instead of the validator script. @@ -399,8 +445,9 @@ \section{Disabling Scripts} \section{Extended UTxO} The main documentation is \href{https://github.com/input-output-hk/plutus/tree/master/docs/extended-utxo}{here}. -Do we only need to add the data script to TxOut? -$$ \type{TxOut} = \type{Addr} \times \type{Value} \times \type{Script} $$ +We need to add the data script to TxOut: +$$ \TxOut = \Addr \times \Value \times \Script $$ +We also need to provide the validator script with more information. Is the $\TxBody$ enough? How is this more expressive than what we already have? \addcontentsline{toc}{section}{References} From 28c18c1a7dcc3c7e721156f97e6ca7849879ed37 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 9 Oct 2018 15:36:30 -0400 Subject: [PATCH 3/5] fixup! initial draft for scripts and multicurrency --- specs/scripts/latex/references.bib | 8 + specs/scripts/latex/scripts-multicurrency.tex | 165 ++++++++++++------ 2 files changed, 119 insertions(+), 54 deletions(-) diff --git a/specs/scripts/latex/references.bib b/specs/scripts/latex/references.bib index 9656f1fea4d..b45114dc8f2 100644 --- a/specs/scripts/latex/references.bib +++ b/specs/scripts/latex/references.bib @@ -1,3 +1,11 @@ +@article{chimeric, + author = {Joachim Zahnentferner}, + title = {Chimeric Ledgers: Translating and Unifying UTXO-based and Account-based Cryptocurrencies}, + journal = {Cryptology ePrint Archive, Report 2018/262}, + year = {2018}, + url = {https://eprint.iacr.org/2018/262}, +} + @article{utxo_scripts, author = {Joachim Zahnentferner}, title = {An Abstract Model of UTxO-based Cryptocurrencies with Scripts}, diff --git a/specs/scripts/latex/scripts-multicurrency.tex b/specs/scripts/latex/scripts-multicurrency.tex index 1cefff73e7a..c7c1446110e 100644 --- a/specs/scripts/latex/scripts-multicurrency.tex +++ b/specs/scripts/latex/scripts-multicurrency.tex @@ -101,26 +101,48 @@ \maketitle \begin{abstract} -This documents specifies the rules for a multi-currency UTxO ledger with scripts, as described in \cite{multi_currency} and \cite{utxo_scripts}. +This documents specifies the rules for a multi-currency UTxO ledger with scripts, +as described in \cite{multi_currency} and \cite{utxo_scripts}. \end{abstract} \tableofcontents \listoffigures -\section{Types} - -[TODO explain scripts, \cref{fig:scripts}]. -\todo{these scripts probably also need to take some of the data in transaction} - -[TODO explain basic types, \cref{fig:basic_definitions}]. - -[TODO explain basic UTxO operations, \cref{fig:auxiliary_ops}]. - -[TODO explain validation, \cref{fig:validation_rules}]. - -[TODO explain ledger state, \cref{fig:ledger_state}]. - -[TODO explain Mutli-currency operations]. +\section{Introduction} + +A model of a UTxO ledger utilizing an abstract authorization mechanism is +described in \cite{utxo_scripts}. The authorization mechanism involves a +scripting language, which we leave unspecified and refer to as $\Script$. +This model is an extension of the model described in \cite{chimeric}, +which includes account based transactions in addition to UTxO transactions. +We do not include account transactions in this specification. + +The model described in \cite{utxo_scripts} was further generalized in +\cite{multi_currency} to support using multiple currencies on the same ledger. + +In what follows, we describe the multi-currency UTxO ledger model using +mostly set theory, we state validation rules that determine whether a transaction +is valid for a given ledger state, and finally we define the state transformation +that a valid transaction has on the state. + +\section{Scripts} + +We use an abstract scripting language $\Scripts$ to generalize authorization +mechanisms such as pay-to-pubkey-hash. +In pay-to-pubkey-hash, an address is the hash of a public key. +UTxO held by that address are authorized by providing the public key +and a digital signature. +Similarly, in the generalized script model, an address +is the hash of a verification script, and the redeemer script +plays the role of the digital signature. +UTxO held by script addresses are authorized by providing both the validator +and redeemer script. Analogously to checking a digital signature, +the authorization succeeds if the redeemer scripts provides evidence to +that causes the validator script to return true. +This is made precise in \cref{fig:scripts}. + +\todo[inline]{These scripts probably also need to take some of the data +from the validating transaction} \begin{figure} \emph{Scripts} @@ -154,7 +176,27 @@ \section{Types} \caption{Scripts} \label{fig:scripts} \end{figure} - +\section{Multi-Currency} + +Multi-currency is explained in detail in \cite{multi_currency}, but here we give some +brief details. The main idea is to replace the currency quantity type with a (finite) +mapping from currency names to quantity. The understanding is that currencies not in +a given mapping are assumed to have value 0 (the additive identity). Previous operations +on the quantity type, such as addition and less-than, are now performed coordinate-wise +on the new type. We write $\vec{0}$ for the empty map/value. + +\section{Basic Types and Operations} + +The basic types and operations for this specification are given +in \cref{fig:basic_definitions}. Transaction inputs are references to +previous unspent outputs, together with the scripts needed to authorize it. +Outputs are the pair of an address (the hash of a validator script) and a +multi-currency value. A transaction is a collection of inputs and outputs, +together with other data for creating new currencies, minting currency, +and paying fees. Currency is authorized to be minted using the same +mechanism of validator and redeemer scripts. +Other needed operations on transactions and UTxO are given in +\cref{fig:auxiliary_ops}. \begin{figure} @@ -301,45 +343,30 @@ \section{Types} \label{fig:auxiliary_ops} \end{figure} +\section{Validation and Ledger State} -\begin{figure} - -\emph{Ledger State} -% -\begin{equation*} -\begin{array}{r@{~\in~}lr} -utxo & \UTxO & \text{unspent outputs} -\\ -currencies & \Currency \mapsto \Script - & \text{currencies with policies} -\\ -totalMinted & \Value & \text{total currency minted} -\\ -slot & \Slot & \text{current slot} - -\end{array} -\end{equation*} -% -\emph{Initial Ledger State} -% -\begin{equation*} -\begin{array}{llllll} -utxo = \emptyset - & currencies = \emptyset - & totalMinted = \vec{0} - & slot = 0 -\end{array} -\end{equation*} +Validation is the determination that a transaction is permitted to be appended +to the ledger, and hence manipulate the state of the ledger. +The data in the ledger state is given by \cref{fig:ledger_state}. +Though $\var{totalMinted}$ and $\var{slot}$ do not appear to be used in this specification, +they are important since they are used by the validator scripts. +For example, expirations can be implemented using $\var{slot}$, and a currency's +policy may depend on $\var{totalMinted}$. -\caption{Ledger State} -\label{fig:ledger_state} -\end{figure} +The ledger state is defined inductively. +The initial state is defined in \cref{fig:ledger_state}. +\todo{Should we hard code $\mathsf{ADA}$ and the corresponding +monetary policy into the initial ledger state?} +Given a transaction and a ledger state, first we check that +the transaction is valid. +To be valid, it must pass every test given in \cref{fig:validation_rules}. +Note that these rules depend only on the transaction and the ledger state. +If a transaction is valid for a given ledger state, it is then +applied using the state transformation rule given in \cref{fig:state_transition}. -\section{Validation} -See figure \cref{fig:validation_rules} \begin{figure} -\emph{Valid Inputs} +\emph{Valid Transactions (for a given Ledger State)} % \begin{equation*} \txins{tx} \subseteq \dom \var{utxo} @@ -393,8 +420,38 @@ \section{Validation} \label{fig:validation_rules} \end{figure} -\section{State Transformations} -See figure \cref{fig:state_transitions} + +\begin{figure} + +\emph{Ledger State} +% +\begin{equation*} +\begin{array}{r@{~\in~}lr} +utxo & \UTxO & \text{unspent outputs} +\\ +currencies & \Currency \mapsto \Script + & \text{currencies with policies} +\\ +totalMinted & \Value & \text{total currency minted} +\\ +slot & \Slot & \text{current slot} + +\end{array} +\end{equation*} +\emph{Initial Ledger State} +% +\begin{equation*} +\begin{array}{llllll} +utxo = \emptyset + & currencies = \emptyset + & totalMinted = \vec{0} + & slot = 0 +\end{array} +\end{equation*} + +\caption{Ledger State} +\label{fig:ledger_state} +\end{figure} \begin{figure} \begin{equation*} @@ -407,7 +464,7 @@ \section{State Transformations} \end{equation*} \caption{State transition} -\label{fig:state_transitions} +\label{fig:state_transition} \end{figure} \section{Disabling Multi-Currency} @@ -431,7 +488,7 @@ \section{Disabling Multi-Currency} \section{Disabling Scripts} WIP - We should probably make two types of addresses, pay-to-pubkey addresses and script addresses. -The pay-to-pubkey addresses will work similiarly to the validation rules defined above, with the +The pay-to-pubkey addresses will work similarly to the validation rules defined above, with the following changes: "Scripts Validate" becomes a specific validator/redeemer pair, where $\mathsf{validator}$ checks a From 9b923c972b578f9e80405b3eeaaaf9f61f89efe5 Mon Sep 17 00:00:00 2001 From: Damian Nadales Date: Wed, 10 Oct 2018 09:32:15 +0200 Subject: [PATCH 4/5] Fix compilation errors . [skip ci] --- specs/scripts/latex/scripts-multicurrency.tex | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/specs/scripts/latex/scripts-multicurrency.tex b/specs/scripts/latex/scripts-multicurrency.tex index c7c1446110e..88f5c8f9944 100644 --- a/specs/scripts/latex/scripts-multicurrency.tex +++ b/specs/scripts/latex/scripts-multicurrency.tex @@ -127,7 +127,7 @@ \section{Introduction} \section{Scripts} -We use an abstract scripting language $\Scripts$ to generalize authorization +We use an abstract scripting language $\Script$ to generalize authorization mechanisms such as pay-to-pubkey-hash. In pay-to-pubkey-hash, an address is the hash of a public key. UTxO held by that address are authorized by providing the public key @@ -160,11 +160,9 @@ \section{Scripts} & \type{LedgerState} \mapsto \type{R} \end{array} \end{equation*} - -~ ~ ~ \text{where} \type{R} - \text{is an arbitrary type, but must be the same for each validator/redeemer pair.} -\\ - +% ~ ~ ~ \text{where} \type{R} +% \text{is an arbitrary type, but must be the same for each validator/redeemer pair.} +%\\ \emph{Script Operations} \begin{align*} & \fun{scriptValidate} \in From 787a5c74b9428073d5841000348e8e75f72c1de1 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Wed, 10 Oct 2018 10:34:27 -0400 Subject: [PATCH 5/5] fixup! initial draft for scripts and multicurrency --- specs/scripts/latex/scripts-multicurrency.tex | 103 ++++++++++++------ 1 file changed, 72 insertions(+), 31 deletions(-) diff --git a/specs/scripts/latex/scripts-multicurrency.tex b/specs/scripts/latex/scripts-multicurrency.tex index 88f5c8f9944..3d23f0d9ec9 100644 --- a/specs/scripts/latex/scripts-multicurrency.tex +++ b/specs/scripts/latex/scripts-multicurrency.tex @@ -28,6 +28,13 @@ \floatstyle{boxed} \restylefloat{figure} +%% +%% Package `semantic` can be used for writing inference rules. +%% +\usepackage{semantic} +%% Setup for the semantic package +\setpremisesspace{20pt} + \DeclareMathOperator{\dom}{dom} \DeclareMathOperator{\range}{range} @@ -80,13 +87,14 @@ %% \newcommand{\scriptValidate}[3]{\fun{scriptValidate} ~ \var{#1} ~ \var{#2} ~ \var{#3}} \newcommand{\txid}[1]{\fun{txid}\ \var{#1}} +\newcommand{\inputAddr}[1]{\fun{inputAddr}\ \var{#1}} \newcommand{\txins}[1]{\fun{txins}\ \var{#1}} \newcommand{\txouts}[1]{\fun{txouts}\ \var{#1}} \newcommand{\hash}[1]{\fun{hash}\ \var{#1}} \newcommand{\forged}[1]{\fun{forged}\ \var{#1}} \newcommand{\forgeReedemers}[1]{\fun{forgeReedemers}\ \var{#1}} \newcommand{\fee}[1]{\fun{fee}\ \var{#1}} -\newcommand{\created}[1]{\fun{forged}\ \var{#1}} +\newcommand{\created}[1]{\fun{created}\ \var{#1}} \newcommand{\outRefs}[1]{\fun{outRefs}\ \var{#1}} \begin{document} @@ -121,7 +129,7 @@ \section{Introduction} \cite{multi_currency} to support using multiple currencies on the same ledger. In what follows, we describe the multi-currency UTxO ledger model using -mostly set theory, we state validation rules that determine whether a transaction +mostly set theory, we state validation rules that determine whether a transaction is valid for a given ledger state, and finally we define the state transformation that a valid transaction has on the state. @@ -160,15 +168,19 @@ \section{Scripts} & \type{LedgerState} \mapsto \type{R} \end{array} \end{equation*} -% ~ ~ ~ \text{where} \type{R} -% \text{is an arbitrary type, but must be the same for each validator/redeemer pair.} -%\\ +~ ~ ~ \text{where $\ScriptEval{script}$ is the pure function denoted +by $script\in\Script$,} + +~ ~ ~ \text{and $\type{R}$ is an arbitrary type, but must be the +same for each validator/redeemer pair.} +\\ +\\ \emph{Script Operations} \begin{align*} & \fun{scriptValidate} \in - \type{LedgerState} \times \Script \times \Script \mapsto \Bool \\ + \type{LedgerState} \mapsto \Script \mapsto \Script \mapsto \Bool \\ & \scriptValidate{st}{validator}{redeemer} = -\ScriptEval{validator} \left(st, \ScriptEval{redeemer}\left(st\right)\right) +\ScriptEval{validator} ~ state \left(\ScriptEval{redeemer} state\right) \end{align*} \caption{Scripts} @@ -193,7 +205,7 @@ \section{Basic Types and Operations} together with other data for creating new currencies, minting currency, and paying fees. Currency is authorized to be minted using the same mechanism of validator and redeemer scripts. -Other needed operations on transactions and UTxO are given in +Other needed operations on transactions and UTxO are given in \cref{fig:auxiliary_ops}. \begin{figure} @@ -302,6 +314,11 @@ \section{Basic Types and Operations} & \text{transaction inputs} \\ & \fun{txins} ~ ((\var{txins}, \_), \_, \_, \_) = \var{txins} \\[1em] +& \fun{inputAddr} \in \TxIn \to \Addr +& \text{address for an input} \\ +& \fun{inputAddr} ~ (\_, \_, validator, \_) += \hash validator +\\[1em] & \fun{txouts} \in \Tx \to \UTxO & \text{transaction outputs as UTxO} \\ & \fun{txouts} ~ \var{tx} = @@ -361,29 +378,37 @@ \section{Validation and Ledger State} Note that these rules depend only on the transaction and the ledger state. If a transaction is valid for a given ledger state, it is then applied using the state transformation rule given in \cref{fig:state_transition}. +\todo[inline]{There is a subtlety here involving in the order in which these rules are applied. +If the UTxO update rule (\cref{eq:utxo-update}) is applied to a transaction before the +currency creation rule (\cref{eq:create-currency}), +then a currency cannot be both created and forged in the same transaction.} +Note that two rules from \cite{multi_currency} do not appear in \cref{fig:validation_rules}, +namely ``creator has enough money" and ``fee is non-negative". +In a model without account transactions, as we have here, we do not need additive +inverses and can assume that all quantities are nonnegative. \begin{figure} -\emph{Valid Transactions (for a given Ledger State)} +\emph{Valid-Inputs} % \begin{equation*} \txins{tx} \subseteq \dom \var{utxo} \end{equation*} -\emph{Preservation of Value} +\emph{Preservation-of-Value} % \begin{equation*} balance (\txouts tx) + (\fee tx) = balance (\txins tx \restrictdom utxo) + (\forged tx) \end{equation*} -\emph{No Double Spend} +\emph{No-Double-Spend} % \begin{equation*} \lvert \txins tx \rvert = \lvert \outRefs tx\rvert \end{equation*} -\emph{Scripts Validate} +\emph{Scripts-Validate} % \begin{equation*} \forall (\_, \_, validator, redeemer)\in(\txins tx), @@ -393,22 +418,22 @@ \section{Validation and Ledger State} \emph{Authorized} % \begin{equation*} - \forall (\_, \_, validator, \_)\in(\txins tx), - (i \mapsto (addr, \_)) \in \var{utxo} \land \hash validator = addr + \forall i\in(\txins tx), + (i \mapsto (addr, \_)) \in \var{utxo} \land \inputAddr i = addr \end{equation*} -\emph{Forge Obeys Policy} +\emph{Forge-Obeys-Policy} % \begin{equation*} \begin{array}{c} \forall c\in(\forged tx), \\ -\exists policy, (c, policy) \in \var{currencies} \\ -\exists reedemer, (c, reedemer) \in \forgeReedemers tx \\ +\exists policy, (c \mapsto policy) \in \var{currencies} \\ +\exists reedemer, (c \mapsto reedemer) \in \forgeReedemers tx \\ \scriptValidate{state}{policy}{redeemer} \end{array} \end{equation*} -\emph{Create Only New Currencies} +\emph{Create-Only-New-Currencies} % \begin{equation*} \created tx = (curr, policy), curr \notin \dom currencies @@ -452,23 +477,39 @@ \section{Validation and Ledger State} \end{figure} \begin{figure} -\begin{equation*} - \begin{array}{rcl} - \var{utxo} & & (\txins tx \subtractdom \var{utxo}) \union \txouts tx \\ - \var{currencies} & \longrightarrow & \var{currencies} \union (\created tx) \\ - \var{totalMinted} & & \var{totalMinted} + (\forged tx)\\ - \var{slot} & & \var{slot} \\ - \end{array} -\end{equation*} - -\caption{State transition} -\label{fig:state_transition} + \centering + \begin{equation}\label{eq:utxo-update} + \inference[update-UTxO] + { + \text{Valid-Inputs} & \text{Preservation-of-Value} & \text{No-Double-Spend} \\ + \text{Scripts-Validate} & \text{Authorized} & \text{Forge-Obeys-Policy} + } + { + \begin{array}{rcl} + \var{utxo} & & (\txins tx \subtractdom \var{utxo}) \union \txouts tx \\ + \var{totalMinted} & \trans{}{tx} & \var{totalMinted} + (\forged tx)\\ + \end{array} + } + \end{equation} + + \begin{equation}\label{eq:create-currency} + \inference[create-currency] + { + \text{Create-Only-New-Currencies} + } + { + \var{currencies} \trans{}{tx} \var{currencies} \union (\created tx) + } + \end{equation} + + \caption{State Transitions} + \label{fig:state_transition} \end{figure} \section{Disabling Multi-Currency} If we want to disable multi-currency, we can remove the ``Forge Obeys Policy" rule and -add \cref{fig:only_ada_rule} +add \cref{fig:only_ada_rule} \begin{figure} \emph{Only ADA} % @@ -481,7 +522,7 @@ \section{Disabling Multi-Currency} \end{figure} \todo[inline]{We need to think carefully about how to handle similar names, -like ``ada", ``Ada", and ``ADA".} +like ``ada", ``Ada", and ``ADA". Allow only uppercase (lowercase)? No unicode?} \section{Disabling Scripts}