Merge pull request #579 from input-output-hk/specs/shelley/tt-gen-deleg

Issue #565 genesis delegation map header stability
IntersectMBO · Jun 24, 2019 · bc11049 · bc11049
2 parents ce55adb + 5a037da
commit bc11049
Show file tree

Hide file tree

Showing 5 changed files with 55 additions and 13 deletions.
diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex
@@ -1505,6 +1505,7 @@ \subsection{Byron to Shelley Transition}
                             \emptyset \\
                             \emptyset \\
                             \emptyset \\
+                            \emptyset \\
                             \fun{dms}~\var{ds} \\
                           \end{array}
                         \right) \\

diff --git a/shelley/chain-and-ledger/formal-spec/delegation.tex b/shelley/chain-and-ledger/formal-spec/delegation.tex
@@ -196,6 +196,7 @@ \subsection{Delegation Transitions}
         pool to which is delegates.
       \item $\var{ptrs}$ maps stake keys to the position of the registration certificate
         in the blockchain. This is needed to lookup the stake hashkey of a pointer address.
+      \item $\var{fdms}$ future genesis keys delegations.
       \item $\var{dms}$ maps genesis keys to the cold key delegates.
     \end{itemize}
   \item $\PState$ keeps track of the stake pool information:
@@ -230,6 +231,7 @@ \subsection{Delegation Transitions}
       \var{rewards} & \AddrRWD \mapsto \Coin & \text{rewards}\\
       \var{delegations} & \HashKey_{stake} \mapsto \HashKey_{pool} & \text{delegations}\\
       \var{ptrs} & \Ptr \mapsto \HashKey & \text{pointer to hashkey}\\
+      \var{fdms} & (\Slot\times\VKeyGen) \mapsto \VKey & \text{future genesis key delegations}\\
       \var{dms} & \VKeyGen \mapsto \VKey & \text{genesis key delegations}\\
     \end{array}\right)
     \\
@@ -331,7 +333,8 @@ \subsection{Delegation Rules}
     There is a precondition that the genesis key is already in the mapping $\var{dms}$.
     Genesis delegation causes the following state transformation:
     \begin{itemize}
-      \item The genesis delegation relation is updated with the new pair.
+      \item The future genesis delegation relation is updated with the new delegate
+        to be adopted in $\SlotsPrior$-many slots.
     \end{itemize}
 \end{itemize}
 
@@ -359,6 +362,7 @@ \subsection{Delegation Rules}
         \var{rewards} \\
         \var{delegations} \\
         \var{ptrs} \\
+        \var{fdms} \\
         \var{dms} \\
       \end{array}
       \right)
@@ -369,6 +373,7 @@ \subsection{Delegation Rules}
         \varUpdate{\var{rewards}} & \varUpdate{\union} & \varUpdate{\{\addrRw \var{hk} \mapsto 0\}}\\
         \var{delegations} \\
         \varUpdate{\var{ptrs}} & \varUpdate{\union} & \varUpdate{\{ptr \mapsto \var{hk}\}} \\
+        \var{fdms} \\
         \var{dms} \\
       \end{array}
       \right)
@@ -393,6 +398,7 @@ \subsection{Delegation Rules}
         \var{rewards} \\
         \var{delegations} \\
         \var{ptrs} \\
+        \var{fdms} \\
         \var{dms} \\
       \end{array}
       \right)
@@ -403,6 +409,7 @@ \subsection{Delegation Rules}
         \varUpdate{\{\addrRw \var{hk}\}} & \varUpdate{\subtractdom} & \varUpdate{\var{rewards}} \\
         \varUpdate{\{\var{hk}\}} & \varUpdate{\subtractdom} & \varUpdate{\var{delegations}} \\
         \varUpdate{\{ptr\}} & \varUpdate{\subtractdom} & \varUpdate{\var{ptrs}} \\
+        \var{fdms} \\
         \var{dms} \\
       \end{array}
       \right)
@@ -426,6 +433,7 @@ \subsection{Delegation Rules}
         \var{rewards} \\
         \var{delegations} \\
         \var{ptrs} \\
+        \var{fdms} \\
         \var{dms} \\
       \end{array}
       \right)
@@ -437,6 +445,7 @@ \subsection{Delegation Rules}
         \varUpdate{\var{delegations}} & \varUpdate{\unionoverrideRight}
                                       & \varUpdate{\{\var{hk} \mapsto \dpool c\}} \\
         \var{ptrs} \\
+        \var{fdms} \\
         \var{dms} \\
       \end{array}
       \right)
@@ -449,6 +458,8 @@ \subsection{Delegation Rules}
       \var{c}\in \DCertGen
       & (\var{gkey},~\var{vk})\leteq\fun{genDel}~{c}
       & \var{gkey}\in\dom{dms}
+      \\
+      s'\leteq\var{slot}+\SlotsPrior
     }
     {
       \begin{array}{r}
@@ -462,6 +473,7 @@ \subsection{Delegation Rules}
         \var{rewards} \\
         \var{delegations} \\
         \var{ptrs} \\
+        \var{fdms} \\
         \var{dms} \\
       \end{array}
       \right)
@@ -472,8 +484,9 @@ \subsection{Delegation Rules}
         \var{rewards} \\
         \var{delegations} \\
         \var{ptrs} \\
-        \varUpdate{\var{dms}} & \varUpdate{\unionoverrideRight}
-                              & \varUpdate{\{\var{gkey} \mapsto \var{vk}\}} \\
+        \varUpdate{\var{fdms}} & \varUpdate{\unionoverrideRight}
+                               & \varUpdate{\{(\var{s'},~\var{gkey}) \mapsto \var{vk}\}} \\
+        \var{dms} \\
       \end{array}
       \right)
     }
@@ -831,6 +844,10 @@ \subsection{Delegation and Pool Combined Rules}
     The base case triggers the following state transformation:
     \begin{itemize}
       \item Reward accounts are set to zero for each corresponding withdrawal.
+      \item The genesis key delegation mapping is updated accourding to the future delegation
+        mapping. For each genesis key, we take the most recent delegation in $\var{fdms}$
+        that is past the current slot.
+      \item The future genesis key delegation has any items past the current slots removed.
     \end{itemize}
   \item The inductive case, when the list is non-empty, is captured by \cref{eq:delegs-induct}.
     It constructs a certificate pointer given the current slot and transaction index,
@@ -853,28 +870,49 @@ \subsection{Delegation and Pool Combined Rules}
       \var{wdrls} \subseteq \var{rewards}
       \\
       \var{rewards'} \leteq \var{rewards} \unionoverrideRight \{(w, 0) \mid w \in \dom \var{wdrls}\}
+      \\~\\
+      \var{curr}\leteq
+      \left\{
+        (\var{s},~\var{gkey})\mapsto\var{vkey}\in\var{fdms}
+        ~\mathrel{\Bigg|}~
+        {
+          \begin{array}{r}
+            \var{s}\geq\var{slot}\\
+            \var{s}=\max\{s'~\mid~(s',~\var{gkey})\in\dom{\var{fdms}}\}
+          \end{array}
+        }
+      \right\}
+      \\
+      \var{dms'}\leteq
+      \{
+        \var{gkey}\mapsto\var{vkey}
+        ~\mid~
+        (\var{s},~\var{gkey})\mapsto\var{vkey}\in\var{curr}
+      \}
     }
     {
       \left(
-      \begin{array}{r}
+      \begin{array}{c}
         \var{slot} \\
         \var{txIx} \\
         \var{pp} \\
       \end{array}
     \right)
       \vdash
       \left(
-      \begin{array}{r}
+      \begin{array}{c}
         \left(
         \begin{array}{r}
           \var{stkeys} \\
           \var{rewards} \\
           \var{delegations} \\
           \var{ptrs} \\
+          \var{fdms} \\
+          \var{dms} \\
         \end{array}
         \right) \\~\\
         \left(
-        \begin{array}{r}
+        \begin{array}{c}
           \var{stpools} \\
           \var{poolParams} \\
           \var{retiring} \\
@@ -885,17 +923,19 @@ \subsection{Delegation and Pool Combined Rules}
       \right)
       \trans{delegs}{\epsilon}
       \left(
-      \begin{array}{r}
+      \begin{array}{c}
         \left(
-        \begin{array}{r}
+        \begin{array}{c}
           \var{stkeys} \\
           \varUpdate{\var{rewards'}} \\
           \var{delegations} \\
           \var{ptrs} \\
+          \varUpdate{\var{fdms}\setminus\var{curr}} \\
+          \varUpdate{\var{dms}\unionoverrideRight\var{dms'}} \\
         \end{array}
         \right) \\~\\
         \left(
-        \begin{array}{r}
+        \begin{array}{c}
           \var{stpools} \\
           \var{poolParams} \\
           \var{retiring} \\

diff --git a/shelley/chain-and-ledger/formal-spec/epoch.tex b/shelley/chain-and-ledger/formal-spec/epoch.tex
@@ -281,7 +281,8 @@ \subsection{Stake Distribution Calculation}
       & \fun{stakeDistr}~{utxo}~{dstate}~{pstate} =
       (\dom{\var{activeDelegs}})\restrictdom\left(\fun{aggregate_{+}}~\var{stakeRelation}\right)\\
       & \where \\
-      & ~~~~ (\var{stkeys},~\var{rewards},~\var{delegations},~\var{ptrs},~\wcard) = \var{dstate} \\
+      & ~~~~ (\var{stkeys},~\var{rewards},~\var{delegations},~\var{ptrs},~\wcard,~\wcard)
+        = \var{dstate} \\
       & ~~~~ (\var{stpools},~\wcard,~\wcard,~\wcard,~\wcard) = \var{pstate} \\
       & ~~~~ \var{stakeRelation} = \left(
         \left(\fun{stakeHK_b}^{-1}\cup\left(\fun{addrPtr}\circ\var{ptr}\right)^{-1}\right)
@@ -397,7 +398,7 @@ \subsection{Snapshot Transition}
       {
       \begin{array}{r@{~\leteq~}l}
         (\var{utxo},~\var{deposits},~\var{fees},~\wcard) & \var{utxoSt}\\
-        (\var{stkeys},~\wcard,~\var{delegations},~\wcard,~\wcard) & \var{dstate}\\
+        (\var{stkeys},~\wcard,~\var{delegations},~\wcard,~\wcard,~\wcard) & \var{dstate}\\
         (\var{stpools},~\var{poolParams},~\wcard,~\wcard) & \var{pstate}\\
         \var{stake} & \stakeDistr{utxo}{dstate}{pstate} \\
         \var{slot} & \firstSlot{e} \\

diff --git a/shelley/chain-and-ledger/formal-spec/ledger.tex b/shelley/chain-and-ledger/formal-spec/ledger.tex
@@ -73,7 +73,7 @@ \section{Ledger State Transition}
       dpstate \trans{\hyperref[fig:rules:delegation-sequence]{delegs}}{\var{tx}} dpstate'
       \\~\\
       (\var{dstate}, \var{pstate}) \leteq \var{dpstate'} \\
-      (\var{stkeys}, \_, \_, \_, \var{dms}) \leteq \var{dstate} \\
+      (\var{stkeys}, \_, \_, \_, \_, \var{dms}) \leteq \var{dstate} \\
       (\var{stpools}, \_, \_, \_) \leteq \var{pstate} \\
       \\~\\
       \left({

diff --git a/weekly-reports/2019-06-14/milestone.org b/weekly-reports/2019-06-14/milestone.org
@@ -2,6 +2,6 @@
 ** TODO Update the formal spec with the new update mechanism.
    - [X] Issue #448
 ** TODO Update the formal spec to get the new header validation properties.
-   - [ ] Issue #565
+   - [X] Issue #565
 ** TODO update executable spec with changes not affected by changes to the update mechanism.
    - [ ] Issue #TBD