Several small spec changes for audits

shelley-ma/formal-spec/epoch.tex

@@ -62,7 +62,7 @@ \section{Rewards and the Epoch Boundary}
         \left(\fun{stakeCred_b}^{-1}\cup\left(\fun{addrPtr}\circ\var{ptr}\right)^{-1}\right)
         \circ\left(\hldiff{\fun{utxoAda}}~{\var{utxo}}\right)
         \right)
-        \cup \left(\fun{stakeCred_r}^{-1}\circ\var{rewards}\right) \\
+        \cup \var{rewards} \\
       & ~~~~ \var{activeDelegs} =
                (\dom{rewards}) \restrictdom \var{delegations} \restrictrange (\dom{poolParams})
   \end{align*}

shelley/chain-and-ledger/formal-spec/delegation.tex

@@ -157,7 +157,7 @@ \subsection{Delegation Definitions}
       \fun{genesisDeleg} & \DCertGen \to (\KeyHashGen,~\KeyHash,~\KeyHash_{vrf})
                                             & \text{genesis delegation}
       \\
-      \fun{moveRewards} & \DCertMir \to (\StakeCredential \mapsto \Coin)
+      \fun{credCoinMap} & \DCertMir \to (\StakeCredential \mapsto \Coin)
                                             & \text{moved inst. rewards}
       \\
       \fun{mirPot} & \DCertMir \to \MIRPot & \text{pot for inst. rewards}
@@ -592,7 +592,7 @@ \subsection{Delegation Rules}
       slot < \fun{firstSlot}~((\epoch{slot}) + 1) - \fun{StabilityWindow}\\
       (\var{irReserves},~\var{irTreasury})\leteq\var{i_{rwd}}
       &
-      \var{combinedR}\leteq\var{irReserves}\unionoverrideRight(\fun{moveRewards}~\var{c}) \\
+      \var{combinedR}\leteq(\fun{credCoinMap}~\var{c})\unionoverrideLeft\var{irReserves} \\
       \sum\limits_{\wcard\mapsto\var{val}\in\var{combinedR}} val \leq\var{reserves}
     }
     {
@@ -636,7 +636,7 @@ \subsection{Delegation Rules}
       slot < \fun{firstSlot}~((\epoch{slot}) + 1) - \fun{StabilityWindow}\\
       (\var{irReserves},~\var{irTreasury})\leteq\var{i_{rwd}}
       &
-      \var{combinedT}\leteq\var{irTreasury}\unionoverrideRight(\fun{moveRewards}~\var{c}) \\
+      \var{combinedT}\leteq(\fun{credCoinMap}~\var{c})\unionoverrideLeft\var{irTreasury} \\
       \sum\limits_{\wcard\mapsto\var{val}\in\var{combinedT}} val \leq\var{treasury}
     }
     {

shelley/chain-and-ledger/formal-spec/epoch.tex

@@ -376,7 +376,7 @@ \subsection{Stake Distribution Calculation}
         \left(\fun{stakeCred_b}^{-1}\cup\left(\fun{addrPtr}\circ\var{ptr}\right)^{-1}\right)
         \circ\left(\range{\var{utxo}}\right)
         \right)
-        \cup \left(\fun{stakeCred_r}^{-1}\circ\var{rewards}\right) \\
+        \cup \var{rewards} \\
       & ~~~~ \var{activeDelegs} =
                (\dom{rewards}) \restrictdom \var{delegations} \restrictrange (\dom{poolParams}) \\
   \end{align*}
@@ -591,9 +591,9 @@ \subsection{Pool Reaping Transition}
       \left(
         \begin{array}{r}
           \var{utxo} \\
-          \var{deposits} \\
+          \var{deposited} \\
           \var{fees} \\
-          \var{ups} \\
+          \var{ppup} \\
           ~ \\
           \var{treasury} \\
           \var{reserves} \\
@@ -614,11 +614,11 @@ \subsection{Pool Reaping Transition}
       \left(
         \begin{array}{rcl}
           \var{utxo} \\
-          \varUpdate{\var{deposits}}
+          \varUpdate{\var{deposited}}
           & \varUpdate{-}
           & \varUpdate{(\var{unclaimed} + \var{refunded})} \\
           \var{fees} \\
-          \var{ups} \\
+          \var{ppup} \\
           ~ \\
           \varUpdate{\var{treasury}} & \varUpdate{+} & \varUpdate{\var{unclaimed}} \\
           \var{reserves} \\
@@ -694,11 +694,11 @@ \subsection{Protocol Parameters Update Transition}
       & \fun{updatePpup} \in \UTxOState \to \PParams \to \UTxOState\\
       & \fun{updatePpup}~\var{utxoSt}~\var{pp} =
       \begin{cases}
-        (\var{utxo},\var{deposits},\var{fees},(\var{fpup},~\emptyset))
+        (\var{utxo},\var{deposited},\var{fees},(\var{fpup},~\emptyset))
         &
         \var{canFollow}
         \\
-        (\var{utxo},\var{deposits},\var{fees},(\emptyset,~\emptyset))
+        (\var{utxo},\var{deposited},\var{fees},(\emptyset,~\emptyset))
         &
         \text{otherwise} \\
       \end{cases}\\
@@ -707,7 +707,7 @@ \subsection{Protocol Parameters Update Transition}
         \forall\var{ps}\in\range{pup},~
         \var{pv}\mapsto\var{v}\in\var{ps}\implies\fun{pvCanFollow}~(\fun{pv}~\var{pp})~\var{v}
         \\
-      & ~~~~~~~(\var{utxo},\var{deposits},\var{fees},(\var{pup},~\var{fpup})) = \var{utxoSt} \\
+      & ~~~~~~~(\var{utxo},\var{deposited},\var{fees},(\var{pup},~\var{fpup})) = \var{utxoSt} \\
   \end{align*}
 \end{figure}
 
@@ -764,7 +764,7 @@ \subsection{Protocol Parameters Update Transition}
     {
       \var{pp_{new}}\neq\Nothing \\~\\
       {\begin{array}{rcl}
-         (\var{utxo},~\var{deposits},~\var{fees},~\var{pup}) & \leteq & \var{utxoSt} \\
+         (\var{utxo},~\var{deposited},~\var{fees},~\var{ppup}) & \leteq & \var{utxoSt} \\
          \var{(\var{rewards},~\wcard,~\wcard,~\wcard,~\wcard,~\var{i_{rwd}})} &
          \leteq & \var{dstate}\\
          \var{(\var{poolParams},~\wcard,~\wcard)} & \leteq & \var{pstate}\\
@@ -773,13 +773,13 @@ \subsection{Protocol Parameters Update Transition}
          \var{diff} & \leteq & \var{oblg_{cur}} - \var{oblg_{new}}\\
       \end{array}}
       \\~\\~\\
-      \var{oblg_{cur}} = \var{deposits} \\
+      \var{oblg_{cur}} = \var{deposited} \\
       \var{reserves} + \var{diff} \geq \sum\limits_{\wcard\mapsto\var{val}\in\var{i_{rwd}}} val \\
       \fun{maxTxSize}~\var{pp_{new}} + \fun{maxHeaderSize}~\var{pp_{new}} <
         \fun{maxBlockSize}~\var{pp_{new}}
       \\~\\
         \var{utxoSt'} \leteq
-        \left(\var{utxo},~\varUpdate{oblg_{new}},~\var{fees},~\var{pup}\right)
+        \left(\var{utxo},~\varUpdate{oblg_{new}},~\var{fees},~\var{ppup}\right)
       \\
       \var{utxoSt''} \leteq \fun{updatePpup}~\var{utxoSt'}~\var{pp_{new}}
       \\~\\
@@ -825,7 +825,6 @@ \subsection{Protocol Parameters Update Transition}
       \end{array}}\right)
       \\~\\~\\
       {\begin{array}{rcl}
-         (\var{utxo},~\var{deposits},~\var{fees},~\var{pup}) & \leteq & \var{utxoSt} \\
           \var{(\var{rewards},~\wcard,~\wcard,~\wcard,~\wcard,~\var{i_{rwd}})} &
           \leteq & \var{dstate}\\
          \var{(\var{poolParams},~\wcard,~\wcard)} & \leteq & \var{pstate}\\
@@ -1498,7 +1497,7 @@ \subsection{Reward Update Calculation}
           \var{retiring} \\
           ~ \\
           \var{utxo} \\
-          \var{deposits} \\
+          \var{deposited} \\
           \var{fees} \\
           \var{up} \\
           ~ \\
@@ -1524,7 +1523,7 @@ \subsection{Reward Update Calculation}
           \var{retiring} \\
           ~ \\
           \var{utxo} \\
-          \var{deposits} \\
+          \var{deposited} \\
           \varUpdate{\var{fees}+\Delta f} \\
           \var{up} \\
           ~ \\

shelley/chain-and-ledger/formal-spec/frontmatter.tex

@@ -30,6 +30,9 @@
           {Added an errata section,
            fixed a typo in leader check and in the LEDGERS rule index,
            and synced the reward calculation with the implementation}
+        \change{2021/06/17}{Jared Corduan}{FM (IOHK)}
+          {Allow the pool influence parameter $a_0$ to be zero,
+          remove all mentions of deposit decay, sync varibale names with code.}
       \end{changelog}
       \clearpage%
 \renewcommand{\thepage}{\arabic{page}}

shelley/chain-and-ledger/formal-spec/ledger-spec.tex

@@ -267,8 +267,6 @@
 \newcommand{\txttl}[1]{\fun{txttl}~ \var{#1}}
 \newcommand{\firstSlot}[1]{\fun{firstSlot}~ \var{#1}}
 \newcommand{\totalDeposits}[3]{\fun{totalDeposits}~ \var{#1} ~ \var{#2} ~ \var{#3}}
-\newcommand{\decayedKey}[4]{\fun{decayedKey}~ \var{#1}~ \var{#2}~ \var{#3}~ \var{#4}}
-\newcommand{\decayedTx}[3]{\fun{decayedTx}~ \var{#1}~ \var{#2}~ \var{#3}}
 \newcommand{\keyRefund}[6]{\fun{keyRefund}~ {#1}~{#2}~{#3}~\var{#4}~\var{#5}~\var{#6}}
 \newcommand{\refund}[4]{\fun{refund}~ \var{#1}~ \var{#2}~ {#3}~ {#4}}
 \newcommand{\keyRefunds}[2]{\fun{keyRefunds}~ \var{#1}~ \var{#2}}
@@ -363,7 +361,6 @@
 \include{software-updates}
 \include{sts-overview}
 \include{properties}
-\include{non-integral}
 \include{leader-value}
 \include{errata}
 

shelley/chain-and-ledger/formal-spec/properties.tex

@@ -575,21 +575,6 @@ \subsection{Properties of Numerical Calculations}
 state those properties and formulate them in a way that makes them usable in
 properties-based testing for validation in the executable spec.
 
-\begin{property}[\textbf{Minimal Refund}]
-  \label{prop:minimal-refund}
-
-  The function $\fun{refund}$ takes a value, a minimal percentage, a decay
-  parameter and a duration. It must guarantee that the refunded amount is within
-  the minimal refund (off-by-one for rounding / floor) and the original value.
-
-  \begin{multline*}
-    \forall d_{val} \in \mathbb{N}, d_{min} \in [0,1], \lambda \in (0, \infty),
-    \delta \in \mathbb{N} \\
-    \implies \max(0,d_{val}\cdot d_{min} - 1) \leq \floor*{d_{val}\cdot(d_{min} +
-      (1-d_{min})\cdot e^{-\lambda\cdot\delta})} \leq d_{val}
-  \end{multline*}
-\end{property}
-
 \begin{property}[\textbf{Maximal Pool Reward}]
   \label{prop:maximal-pool-reward}
 

shelley/chain-and-ledger/formal-spec/protocol-parameters.tex

@@ -83,11 +83,10 @@ \subsection{Updatable Protocol Parameters}
         \var{maxBlockSize} \mapsto \N & \PParams & \text{max block body size}\\
         \var{maxTxSize} \mapsto \N & \PParams & \text{max transaction size}\\
         \var{maxHeaderSize} \mapsto \N & \PParams & \text{max block header size}\\
-        \var{keyDecayRate} \mapsto \nonnegReals & \PParams & \text{stake credential decay rate}\\
         \var{poolDeposit} \mapsto \Coin & \PParams & \text{stake pool deposit}\\
         \var{E_{max}} \mapsto \Epoch & \PParams & \text{epoch bound on pool retirement}\\
         \var{n_{opt}} \mapsto \Npos & \PParams & \text{desired number of pools}\\
-        \var{a_0} \mapsto \posReals & \PParams & \text{pool influence}\\
+        \var{a_0} \mapsto \nonnegReals & \PParams & \text{pool influence}\\
         \tau \mapsto \unitInterval & \PParams & \text{treasury expansion}\\
         \rho \mapsto \unitInterval & \PParams & \text{monetary expansion}\\
         \var{d} \mapsto \{0,~1/100,~2/100,~\ldots,~1\} & \PParams & \text{decentralization parameter}\\

shelley/chain-and-ledger/formal-spec/utxo.tex

@@ -164,9 +164,9 @@ \subsection{UTxO Transitions}
     \left(
       \begin{array}{r@{~\in~}lr}
         \var{utxo} & \UTxO & \text{UTxO}\\
-        \var{deposits} & \Coin & \text{deposits pot}\\
+        \var{deposited} & \Coin & \text{deposits pot}\\
         \var{fees} & \Coin & \text{fee pot}\\
-        \var{pup} & \PPUpdateState & \text{proposed updates}\\
+        \var{ppup} & \PPUpdateState & \text{proposed updates}\\
       \end{array}
     \right)
   \end{equation*}
@@ -262,8 +262,8 @@ \subsection{UTxO Transitions}
 assures that the ledger state is updated correctly.
 
 The main difference, however, in how rewards and refunds work is that refunds
-come from a $\var{deposits}$ pool, which is a single coin value indicating
-the total decayed amount of all the deposits ever made, while rewards come from individual
+come from the $\var{deposited}$ pot, which is a single coin value indicating
+the sum of all the deposits, while rewards come from individual
 accounts where a reward is accumulated to a specific address.
 
 \begin{figure}[htb]
@@ -286,7 +286,7 @@ \subsection{UTxO Transitions}
           \var{genDelegs} \\
         \end{array}
       }
-      \vdash \var{pup} \trans{\hyperref[fig:rules:pp-update]{ppup}}{\fun{txup}~\var{tx}} \var{pup'}
+      \vdash \var{ppup} \trans{\hyperref[fig:rules:pp-update]{ppup}}{\fun{txup}~\var{tx}} \var{ppup'}
       \\
       ~
       \\
@@ -318,18 +318,18 @@ \subsection{UTxO Transitions}
       \left(
       \begin{array}{r}
         \var{utxo} \\
-        \var{deposits} \\
+        \var{deposited} \\
         \var{fees} \\
-        \var{pup}\\
+        \var{ppup}\\
       \end{array}
       \right)
       \trans{utxo}{tx}
       \left(
       \begin{array}{r}
         \varUpdate{(\txins{txb} \subtractdom \var{utxo}) \cup \outs{txb}}  \\
-        \varUpdate{\var{deposits} + \var{depositChange}} \\
+        \varUpdate{\var{deposited} + \var{depositChange}} \\
         \varUpdate{\var{fees} + \txfee{txb}} \\
-        \varUpdate{pup'}\\
+        \varUpdate{ppup'}\\
       \end{array}
       \right)
     }