From f9713f73cb445bb8ce85bd176ef9bf3618800f0a Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 18 Jan 2022 20:15:16 -0500 Subject: [PATCH 1/4] babbage spec - singe VRF check --- eras/babbage/formal-spec/introduction.tex | 1 - eras/babbage/formal-spec/remove-overlay.tex | 67 +++++++++++++++++++++ 2 files changed, 67 insertions(+), 1 deletion(-) diff --git a/eras/babbage/formal-spec/introduction.tex b/eras/babbage/formal-spec/introduction.tex index 093dc2ecc6c..d8e3fba0293 100644 --- a/eras/babbage/formal-spec/introduction.tex +++ b/eras/babbage/formal-spec/introduction.tex @@ -3,7 +3,6 @@ \section{Introduction} Currently still todo: \begin{itemize} -\item Single VRF check \item Reward calculation wart fixes \item Adjust TxInfo \item Update minUTxO diff --git a/eras/babbage/formal-spec/remove-overlay.tex b/eras/babbage/formal-spec/remove-overlay.tex index d4925d8ce5c..447557f33bc 100644 --- a/eras/babbage/formal-spec/remove-overlay.tex +++ b/eras/babbage/formal-spec/remove-overlay.tex @@ -8,12 +8,23 @@ \newcommand{\PrtclState}{\type{PrtclState}} \newcommand{\PrtclEnv}{\type{PrtclEnv}} \newcommand{\PoolDistr}{\type{PoolDistr}} +\newcommand{\BHBody}{\type{BHBody}} +\newcommand{\HashHeader}{\type{HashHeader}} +\newcommand{\HashBBody}{\type{HashBBody}} +\newcommand{\BlockNo}{\type{BlockNo}} +\newcommand{\Proof}{\type{Proof}} +\newcommand{\OCert}{\type{OCert}} \newcommand{\bheader}[1]{\fun{bheader}~\var{#1}} +\newcommand{\verifyVrf}[4]{\fun{verifyVrf}_{#1} ~ #2 ~ #3 ~#4} +\newcommand{\slotToSeed}[1]{\fun{slotToSeed}~ \var{#1}} +\newcommand{\XOR}{\mathsf{XOR}} \section{Removal of the Overlay Schedule} The overlay schedule was only used during the early days of the Shelley ledger, and can be safely removed. First, the protocol parameter $\var{d}$ is removed, and any functions that use it are reduced to the case $\var{d} = 0$. The function $\fun{mkApparentPerformance}$ is reduced to one of its branches, and its first argument is dropped. It is only used in the definition of $\fun{rewardOnePool}$, which needs to be adjusted accordingly. +Additionally, the block header body now contains a single VRF value to be used for both the leader check and the block nonce. + \begin{figure}[htb] \begin{align*} & \fun{mkApparentPerformance} \in \unitInterval \to \N \to \N \to \Q \\ @@ -62,6 +73,62 @@ \section{Removal of the Overlay Schedule} \newpage Finally, the $\mathsf{PRTCL}$ STS needs to be adjusted. To retire the $\mathsf{OVERLAY}$ STS, we inline the definition of its 'decentralized' case and drop all the unnecessary variables from its environment. It is invoked in $\mathsf{CHAIN}$, which needs to be adjusted accordingly. +As there is now only a singe VRF check, slight modifications are needed for the definition of the block header body \text{BHBody} type and the function \text{vrfChecks}. The Shelley era accessor functions $\fun{bleader}$ and $\fun{bnonce}$ are replaced with new functions. + +\begin{figure*}[htb] + % + \emph{Block Header Body} + % + \begin{equation*} + \BHBody = + \left( + \begin{array}{r@{~\in~}lr} + \var{prev} & \HashHeader^? & \text{hash of previous block header}\\ + \var{vk} & \VKey & \text{block issuer}\\ + \var{vrfVk} & \VKey & \text{VRF verification key}\\ + \var{blockno} & \BlockNo & \text{block number}\\ + \var{slot} & \Slot & \text{block slot}\\ + \hldiff{\var{vrfRes}} & \hldiff{\Seed} & \hldiff{\text{VRF result value}}\\ + \var{prf} & \Proof & \text{vrf proof}\\ + \var{bsize} & \N & \text{size of the block body}\\ + \var{bhash} & \HashBBody & \text{block body hash}\\ + \var{oc} & \OCert & \text{operational certificate}\\ + \var{pv} & \ProtVer & \text{protocol version}\\ + \end{array} + \right) + \end{equation*} + % + \emph{New Accessor Function} + \begin{equation*} + \begin{array}{r@{~\in~}l} + \fun{bVrfRes} & \BHBody \to \Seed \\ + \fun{bVrfProof} & \BHBody \to \Proof \\ + \end{array} + \end{equation*} + % + \emph{New Helper Functions} + \begin{align*} + & \fun{bleader} \in \BHBody \to \Seed \\ + & \fun{bleader}~(\var{bhb}) = (\fun{hash}~``TEST") ~\XOR~ (\fun{bVrfRes}~\var{bhb})\\ + \\ + & \fun{bnonce} \in \BHBody \to \Seed \\ + & \fun{bnonce}~(\var{bhb}) = (\fun{hash}~``NONCE") ~\XOR~ (\fun{bVrfRes}~\var{bhb})\\ + \\ + & \fun{vrfChecks} \in \Seed \to \BHBody \to \Bool \\ + & \fun{vrfChecks}~\eta_0~\var{bhb} = + \verifyVrf{\Seed}{\var{vrfK}}{(\slotToSeed{slot}~\XOR~\eta_0)}{(\var{value},~\var{proof}}) \\ + & ~~~~\where \\ + & ~~~~~~~~~~\var{slot} \leteq \bslot{bhb} \\ + & ~~~~~~~~~~\var{vrfK} \leteq \fun{bvkvrf}~\var{bhb} \\ + & ~~~~~~~~~~\var{value} \leteq \fun{bVrfRes}~\var{bhb} \\ + & ~~~~~~~~~~\var{proof} \leteq \fun{bVrfProof}~\var{bhb} \\ + \end{align*} + % + \caption{Block Definitions} + \label{fig:defs:blocks} +\end{figure*} + + \begin{figure} \emph{Protocol environments} \begin{equation*} From dbd9bd7e71caa18d75f006fc8d3351c4de1ed70f Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Tue, 18 Jan 2022 21:20:59 -0500 Subject: [PATCH 2/4] babbage spec - forgo reward prefilter fixes Shelley errata 17.2 --- eras/babbage/formal-spec/babbage-changes.tex | 5 ++ eras/babbage/formal-spec/introduction.tex | 1 - eras/babbage/formal-spec/references.bib | 10 ++-- eras/babbage/formal-spec/rewards.tex | 51 ++++++++++++++++++++ 4 files changed, 61 insertions(+), 6 deletions(-) create mode 100644 eras/babbage/formal-spec/rewards.tex diff --git a/eras/babbage/formal-spec/babbage-changes.tex b/eras/babbage/formal-spec/babbage-changes.tex index 459ead70e41..77e770b01fe 100644 --- a/eras/babbage/formal-spec/babbage-changes.tex +++ b/eras/babbage/formal-spec/babbage-changes.tex @@ -366,5 +366,10 @@ \include{transactions} \include{utxo} \include{remove-overlay} +\include{rewards} + +\addcontentsline{toc}{section}{References} +\bibliographystyle{plainnat} +\bibliography{references} \end{document} diff --git a/eras/babbage/formal-spec/introduction.tex b/eras/babbage/formal-spec/introduction.tex index d8e3fba0293..d44aae2f183 100644 --- a/eras/babbage/formal-spec/introduction.tex +++ b/eras/babbage/formal-spec/introduction.tex @@ -3,7 +3,6 @@ \section{Introduction} Currently still todo: \begin{itemize} -\item Reward calculation wart fixes \item Adjust TxInfo \item Update minUTxO \end{itemize} diff --git a/eras/babbage/formal-spec/references.bib b/eras/babbage/formal-spec/references.bib index d5f40f97981..6aa0141b3b4 100644 --- a/eras/babbage/formal-spec/references.bib +++ b/eras/babbage/formal-spec/references.bib @@ -12,7 +12,7 @@ @misc{delegation_design author = {Philipp Kant and Lars Br\"unjes and Duncan Coutts}, title = {{Design Specification for Delegation and Incentives in Cardano}}, year = {2018}, - url = {https://github.com/input-output-hk/cardano-ledger-specs/tree/master/docs/delegation_design_spec}, + url = {https://github.com/input-output-hk/cardano-ledger/tree/master/docs/delegation_design_spec}, } @article{chimeric, @@ -51,7 +51,7 @@ @misc{shelley_spec author = {{Formal Methods Team, IOHK}}, title = {{A Formal Specification of the Cardano Ledger}}, year = {2019}, - url = {https://github.com/input-output-hk/cardano-ledger-specs/tree/master/eras/shelley/formal-spec/ledger-spec.tex} + url = {https://hydra.iohk.io/job/Cardano/cardano-ledger-specs/shelleyLedgerSpec/latest/download-by-type/doc-pdf/ledger-spec} } @misc{shelley_ma_spec, @@ -59,7 +59,7 @@ @misc{shelley_ma_spec author = {{Formal Methods Team, IOHK}}, title = {{A Formal Specification of the Cardano Ledger with a Native Multi-Asset Implementation}}, year = {2019}, - url = {https://github.com/input-output-hk/cardano-ledger-specs/tree/master/eras/shelley-ma/formal-spec/shelley-ma.tex} + url = {https://github.com/input-output-hk/cardano-ledger/tree/master/eras/shelley-ma/formal-spec/shelley-ma.tex} } @misc{ouroboros, @@ -86,7 +86,7 @@ @misc{formal_multicur author = {{Plutus Team, Ledger Team, IOHK}}, title = {{A Formal Specification of a UTxO Ledger with Scripts and Multi-Currency}}, year = {2019}, -url = {https://github.com/input-output-hk/cardano-ledger-specs/blob/master/eras/shelley/formal-spec/scripts-multicurrency.tex} +url = {https://github.com/input-output-hk/cardano-ledger/blob/master/eras/shelley/formal-spec/scripts-multicurrency.tex} } @misc{multi_sig, @@ -94,7 +94,7 @@ @misc{multi_sig author = {{Formal Methods Team, IOHK}}, title = {{A Formal Specification of a Multi-Signature Scheme using Scripts}}, year = {2019}, - url = {https://github.com/input-output-hk/cardano-ledger-specs/blob/master/eras/shelley/formal-spec/multi-sig.tex} + url = {https://github.com/input-output-hk/cardano-ledger/blob/master/eras/shelley/formal-spec/multi-sig.tex} } @misc{non_int, diff --git a/eras/babbage/formal-spec/rewards.tex b/eras/babbage/formal-spec/rewards.tex new file mode 100644 index 00000000000..b5a22fef89a --- /dev/null +++ b/eras/babbage/formal-spec/rewards.tex @@ -0,0 +1,51 @@ +\newcommand{\Stake}{\type{Stake}} +\newcommand{\mReward}[4]{\fun{r_{member}}~ \var{#1}~ \var{#2}~ \var{#3}~ {#4}} +\newcommand{\lReward}[4]{\fun{r_{operator}}~ \var{#1}~ \var{#2}~ \var{#3}~ {#4}} + +\section{Forgo Reward Calculation Prefilter} + +The reward calculation no longer filters out the unregistered stake +credentials when creating a reward update. As in the Shelley era, though, +they are still filtered on the epoch boundary when the reward update is applied. +This addresses errata 17.2 in the Shelley ledger specification \cite{shelley_spec}[17.2]. +The change consists of removing the line +$$\var{addrs_{rew}}\restrictdom{\var{potentialRewards}}$$ +from the $\fun{rewardOnePool}$ function. + +\begin{figure}[htb] + \emph{Calculation to reward a single stake pool} + % + \begin{align*} + & \fun{rewardOnePool} \in \PParams \to \Coin \to \N \to \N \to \PoolParam\\ + & ~~~\to \Stake \to \Q \to \Q \to \Coin \to (\AddrRWD \mapsto \Coin) \\ + & \fun{rewardOnePool}~\var{pp}~\var{R}~\var{n}~\var{\overline{N}}~\var{pool}~\var{stake}~{\sigma}~{\sigma_a}~\var{tot} = + \var{rewards}\\ + & ~~~\where \\ + & ~~~~~~~\var{ostake} = \sum_{\substack{ + hk_\mapsto c\in\var{stake}\\ + hk\in(\fun{poolOwners}~\var{pool})\\ + }} c \\ + & ~~~~~~~\var{pledge} = \fun{poolPledge}~pool \\ + & ~~~~~~~p_{r} = \var{pledge} / \var{tot} \\ + & ~~~~~~~maxP = + \begin{cases} + \fun{maxPool}~\var{pp}~\var{R}~\sigma~\var{p_r}& + \var{pledge} \leq \var{ostake}\\ + 0 & \text{otherwise.} + \end{cases} \\ + & ~~~~~~~\var{appPerf} = \mkApparentPerformance{(\fun{d}~pp)}{\sigma_a}{n}{\overline{N}} \\ + & ~~~~~~~\var{poolR} = \floor{\var{appPerf}\cdot\var{maxP}} \\ + & ~~~~~~~\var{mRewards} = \\ + & ~~~~~~~~~~\left\{ + \addrRw~hk\mapsto\mReward{poolR}{pool}{\frac{c}{tot}}{\sigma} + ~\Big\vert~ + hk\mapsto c\in\var{stake},~~hk \not\in(\fun{poolOwners}~\var{pool}) + \right\}\\ + & ~~~~~~~\var{lReward} = \lReward{poolR}{pool}{\frac{\var{ostake}}{tot}}{\sigma} \\ + & ~~~~~~~\var{rewards} = + \var{mRewards} \cup + \{(\fun{poolRAcnt}~\var{pool})\mapsto\var{lReward}\} \\ + \end{align*} + \caption{The Reward Calculation} + \label{fig:functions:reward-calc} +\end{figure} From dc3ed99c4f4a7a96fe4d6bf80731134485e966cc Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Thu, 20 Jan 2022 16:27:46 -0500 Subject: [PATCH 3/4] fixup! babbage spec - forgo reward prefilter --- eras/babbage/formal-spec/rewards.tex | 30 ++++------------------------ 1 file changed, 4 insertions(+), 26 deletions(-) diff --git a/eras/babbage/formal-spec/rewards.tex b/eras/babbage/formal-spec/rewards.tex index b5a22fef89a..782f5b297bc 100644 --- a/eras/babbage/formal-spec/rewards.tex +++ b/eras/babbage/formal-spec/rewards.tex @@ -1,6 +1,4 @@ \newcommand{\Stake}{\type{Stake}} -\newcommand{\mReward}[4]{\fun{r_{member}}~ \var{#1}~ \var{#2}~ \var{#3}~ {#4}} -\newcommand{\lReward}[4]{\fun{r_{operator}}~ \var{#1}~ \var{#2}~ \var{#3}~ {#4}} \section{Forgo Reward Calculation Prefilter} @@ -10,7 +8,7 @@ \section{Forgo Reward Calculation Prefilter} This addresses errata 17.2 in the Shelley ledger specification \cite{shelley_spec}[17.2]. The change consists of removing the line $$\var{addrs_{rew}}\restrictdom{\var{potentialRewards}}$$ -from the $\fun{rewardOnePool}$ function. +from the last line of the $\fun{rewardOnePool}$ function. \begin{figure}[htb] \emph{Calculation to reward a single stake pool} @@ -21,31 +19,11 @@ \section{Forgo Reward Calculation Prefilter} & \fun{rewardOnePool}~\var{pp}~\var{R}~\var{n}~\var{\overline{N}}~\var{pool}~\var{stake}~{\sigma}~{\sigma_a}~\var{tot} = \var{rewards}\\ & ~~~\where \\ - & ~~~~~~~\var{ostake} = \sum_{\substack{ - hk_\mapsto c\in\var{stake}\\ - hk\in(\fun{poolOwners}~\var{pool})\\ - }} c \\ - & ~~~~~~~\var{pledge} = \fun{poolPledge}~pool \\ - & ~~~~~~~p_{r} = \var{pledge} / \var{tot} \\ - & ~~~~~~~maxP = - \begin{cases} - \fun{maxPool}~\var{pp}~\var{R}~\sigma~\var{p_r}& - \var{pledge} \leq \var{ostake}\\ - 0 & \text{otherwise.} - \end{cases} \\ - & ~~~~~~~\var{appPerf} = \mkApparentPerformance{(\fun{d}~pp)}{\sigma_a}{n}{\overline{N}} \\ - & ~~~~~~~\var{poolR} = \floor{\var{appPerf}\cdot\var{maxP}} \\ - & ~~~~~~~\var{mRewards} = \\ - & ~~~~~~~~~~\left\{ - \addrRw~hk\mapsto\mReward{poolR}{pool}{\frac{c}{tot}}{\sigma} - ~\Big\vert~ - hk\mapsto c\in\var{stake},~~hk \not\in(\fun{poolOwners}~\var{pool}) - \right\}\\ - & ~~~~~~~\var{lReward} = \lReward{poolR}{pool}{\frac{\var{ostake}}{tot}}{\sigma} \\ - & ~~~~~~~\var{rewards} = + & ~~~~~~~\ldots \\ + & ~~~~~~~\hldiff{\var{rewards}} = \var{mRewards} \cup \{(\fun{poolRAcnt}~\var{pool})\mapsto\var{lReward}\} \\ \end{align*} - \caption{The Reward Calculation} + \caption{Reward Calculation Helper Function} \label{fig:functions:reward-calc} \end{figure} From 68c4d9389b74aa84fb814f6e39c63868e146bc71 Mon Sep 17 00:00:00 2001 From: Jared Corduan Date: Mon, 24 Jan 2022 11:06:36 -0500 Subject: [PATCH 4/4] fixup! babbage spec - forgo reward prefilter --- eras/babbage/formal-spec/introduction.tex | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/eras/babbage/formal-spec/introduction.tex b/eras/babbage/formal-spec/introduction.tex index d44aae2f183..2da244e394e 100644 --- a/eras/babbage/formal-spec/introduction.tex +++ b/eras/babbage/formal-spec/introduction.tex @@ -21,5 +21,8 @@ \section{Introduction} \item Add inline datums in the UTxO \item Add reference scripts \item Add transaction fields for specifying and returning collateral -\item Remove the protocol parameter $\var{d}$ and the overlay schedule +\item Remove the protocol parameters $\var{d}$ and $\var{extraEntropy}$ +\item Remove the overlay schedule +\item Block headers to only include a single VRF value and proof +\item Remove the pre-filtering of unregistered stake credentials in the reward calculation \end{itemize}