diff --git a/shelley-ma/formal-spec/epoch.tex b/shelley-ma/formal-spec/epoch.tex index ae38aeb9ff..b7996d826e 100644 --- a/shelley-ma/formal-spec/epoch.tex +++ b/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*} diff --git a/shelley/chain-and-ledger/formal-spec/delegation.tex b/shelley/chain-and-ledger/formal-spec/delegation.tex index 0bbe60e601..d29d0328b9 100644 --- a/shelley/chain-and-ledger/formal-spec/delegation.tex +++ b/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} } { diff --git a/shelley/chain-and-ledger/formal-spec/epoch.tex b/shelley/chain-and-ledger/formal-spec/epoch.tex index cccfcd1846..9210c4759c 100644 --- a/shelley/chain-and-ledger/formal-spec/epoch.tex +++ b/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} \\ ~ \\ diff --git a/shelley/chain-and-ledger/formal-spec/frontmatter.tex b/shelley/chain-and-ledger/formal-spec/frontmatter.tex index 64f9783e3b..c6d90c5edc 100644 --- a/shelley/chain-and-ledger/formal-spec/frontmatter.tex +++ b/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}} diff --git a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex b/shelley/chain-and-ledger/formal-spec/ledger-spec.tex index 1559676c43..dfac8bcebb 100644 --- a/shelley/chain-and-ledger/formal-spec/ledger-spec.tex +++ b/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} diff --git a/shelley/chain-and-ledger/formal-spec/non-integral.tex b/shelley/chain-and-ledger/formal-spec/non-integral.tex deleted file mode 100644 index b005498381..0000000000 --- a/shelley/chain-and-ledger/formal-spec/non-integral.tex +++ /dev/null @@ -1,121 +0,0 @@ -\section{Non-Integral Calculations} -\label{sec:non-integr-calc} - -In the ledger there are several cases where non-integral calculations are -required, particularly calculations relating to delegation transitions. - -\subsection{Types of Non-Integral Calculations} -\label{sec:types-non-integral} - -The specification employs non-integral calculations for different mathematical -operations. Table~\ref{tab:func-non-integral} shows the function and transition -rules that use non-integral calculations and which type. - -\begin{table}[ht] - \centering - \begin{tabular}{lccccc} - \toprule - name & page & multiplication & division & exponential function & exponentiation \\ - \midrule - \fun{refund} - & \pageref{fig:functions:deposits-refunds} & \checkmark & & \checkmark & \\ - \fun{maxPool} - & \pageref{fig:functions:rewards} & \checkmark & \checkmark && \\ - \fun{poolReward} - & \pageref{fig:functions:rewards} & \checkmark & & & - \\ - \fun{r_{operator}} - & \pageref{fig:functions:reward-splitting} & \checkmark & \checkmark &&\\ - \fun{r_{member}} - & \pageref{fig:functions:reward-splitting} & \checkmark & \checkmark - &&\\ - \fun{rewardOnePool} - & \pageref{fig:functions:reward-calc} & \checkmark & \checkmark &&\\ - \fun{RUPD} - &\pageref{fig:rules:reward-update} & \checkmark &&& \\ - \bottomrule - \end{tabular} - \caption{Functions with Non-Integral Calculation} - \label{tab:func-non-integral} -\end{table} - -The transcendental exponential function is used in reward and refund calculation -to model the decay of the deposit values. The pool reward uses exponentiation to -calculate a pool's ranking. - -The domain for the exponential function are the non-negative reals, more -precisely the distribution parameter $\lambda \in (0, \infty)$ multiplied by a -discrete non-negative duration $\delta$. - -The domain of the base of the exponentiation in $\fun{poolReward}$ are the -non-negative reals resulting from the calculation in $\fun{movingAvg}$, the -exponent $\gamma$ is a constant taken from the protocol parameters. - -\subsection{Implementation of Non-Integer Calculations} -\label{sec:impl-non-integ} - -The large part consists of multiplication and division which can easily be done -using fractional arithmetic to the desired precision. The precision necessary is -bounded by the ability to represent a single lovelace in all calculations. - -\subsubsection{Function Simplification} -\label{sec:funct-simpl} - -The transcendental function $e^{x}$ can be approximated using different -approaches, depending on the desired accuracy. In general, one uses the -exponential laws $e^{x} = 1/e^{-x}$ and -$e^{x} = \left(e^{\frac{x}{n}} \right)^{n}, n \in \mathbb{N}$ to reduce the -approximation to the unit interval and apply fast integral exponentiation -afterwards. - -Exponentiation is implemented using the law -$a^{b} = e^{\ln(a^{b})}= e^{b\ln(a)}$. This therefore requires being able to -calculate $e^{x}$ and $\ln(x)$. The the natural logarithm can -be approximated using different approaches, again, depending on the desired -accuracy. Most approximations work for $\ln(x), x \in [1, c)$ with some $c > -1$. One then uses the law $\log_{b}(x) = \log_{b}(\frac{x}{b^{n}}b^{n})$ where -$n \in \mathbb{N}$ is chosen in such a way that $\frac{x}{b^{n}} \in [1, -c)$. Using this, one can separate the calculation of the integral and decimal -part as follows: - -\begin{equation*} - \log_{b}(\frac{x}{b^{n}}b^{n})=\log_{b}(b^{n}) + \log_{b}(\frac{x}{b^{n}})= - n + \log(\frac{x}{b^{n}}) -\end{equation*} - -\subsubsection{Properties of Function Approximation} -\label{sec:prop-funct-appr-1} - -There are several properties that approximations of the transcendental functions -are expected to have. In the following let $\ln'(x)$ be the approximation of -$\ln(x)$, $\exp'(x)$ be the approximation of $e^{x}$ and $x\star y$ the approximation -of $x^{y}$. - -\begin{property}[\textbf{monotonicity}] - \label{prop:monotone} - Both $\exp'$ and $\ln'$ must be monotone on their respective domains. -\end{property} - -In order to guarantee correctness of the approximations, we also require that -the mathematical laws are fulfilled. For some small $\epsilon > 0$, define -$x \approx y \Leftrightarrow \lvert x - y\rvert < \epsilon$. - -\begin{property}[\textbf{Mathematical Laws}] - \label{prop:ln-laws} - The following mathematical laws state the requirements for the approximations - of the $\ln'$ and $\exp'$ function: - \begin{itemize} - \item $\ln'(x\cdot y) \approx \ln'(x) + \ln'(y)$ - \item $\ln'(x\star y) \approx y\cdot \ln'(x)$ - \item $\ln'(\exp'(x)) \approx \exp'(\ln'(x)) \approx x$ - \item $x, y \in [0,1] \implies x \star y \in [0, 1]$ - \item $x, y, z \in [0,1], x > 0 \implies - (z\star\frac{1}{x})\star y \approx (z\star y)\star\frac{1}{x}$ - \item $\exp'(x + y) \approx \exp'(x) \cdot \exp'(y)$ - \end{itemize} -\end{property} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "ledger-spec" -%%% End: diff --git a/shelley/chain-and-ledger/formal-spec/properties.tex b/shelley/chain-and-ledger/formal-spec/properties.tex index cd0bf0ac36..fab129b440 100644 --- a/shelley/chain-and-ledger/formal-spec/properties.tex +++ b/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} diff --git a/shelley/chain-and-ledger/formal-spec/protocol-parameters.tex b/shelley/chain-and-ledger/formal-spec/protocol-parameters.tex index 32ce180171..34cd6486ae 100644 --- a/shelley/chain-and-ledger/formal-spec/protocol-parameters.tex +++ b/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}\\ diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex index 67d7f12841..06ec389dc1 100644 --- a/shelley/chain-and-ledger/formal-spec/utxo.tex +++ b/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) }