babbage spec - two todo items

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}

eras/babbage/formal-spec/introduction.tex

@@ -3,8 +3,6 @@ \section{Introduction}
 Currently still todo:
 
 \begin{itemize}
-\item Single VRF check
-\item Reward calculation wart fixes
 \item Adjust TxInfo
 \item Update minUTxO
 \end{itemize}
@@ -23,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}

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,15 +51,15 @@ @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,
   label = {CdoLedger},
   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,15 +86,15 @@ @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,
   label = {CdoMSIG},
   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,

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*}

eras/babbage/formal-spec/rewards.tex

@@ -0,0 +1,29 @@
+\newcommand{\Stake}{\type{Stake}}
+
+\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 last line of 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 \\
+          & ~~~~~~~\ldots \\
+          & ~~~~~~~\hldiff{\var{rewards}} =
+               \var{mRewards} \cup
+               \{(\fun{poolRAcnt}~\var{pool})\mapsto\var{lReward}\} \\
+  \end{align*}
+  \caption{Reward Calculation Helper Function}
+  \label{fig:functions:reward-calc}
+\end{figure}