-
Notifications
You must be signed in to change notification settings - Fork 158
/
update.tex
278 lines (254 loc) · 9.44 KB
/
update.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
\section{Update Proposal Mechanism}
\label{sec:update}
The $\mathsf{PPUP}$ transition is responsible for the federated governance model in Shelley.
The governance process includes a mechanism for core nodes to propose and vote on
protocol parameter updates. In this chapter we
outline rules for genesis keys \textit{proposing} protocol parameter updates.
For rules regarding the \textit{adoption} of protocol
parameter updates, see Section~\ref{sec:pparam-update}.
This chapter does not discuss authentication of update proposals.
The signature for the keys in the proposal will be checked in the
$\mathsf{UTXOW}$ transition, which checks all the necessary witnesses
for a transaction, see Section\ref{sec:witnesses-shelley}.
\textbf{Genesis Key Delegations.} The environment for the protocol parameter
update transition contains the value $\var{genDelegs}$,
which is a finite map indexed by genesis key hashes,
and which maps to a pair consisting of a delegate key hash
(corresponding to the cold key used for producing blocks) and
a VRF key hash.
During the Byron era, the genesis nodes are all
already delegated to some $\KeyHash$, and these delegations are inherited
through the Byron-Shelley transition (see Section~\ref{sec:byron-to-shelley}).
The VRF key hashes in this mapping will be new to the Shelley era.
The delegations mapping can be updated as described in
Section~\ref{sec:delegation-shelley},
but there is no mechanism for them to un-delegate or for the keys to which they delegate
to retire (unlike regular stake pools).
The types $\ProposedPPUpdates$ and $\Update$ were defined in
Figure~\ref{fig:defs:utxo-shelley}.
The update proposal type $\Update$ is a pair of $\ProposedPPUpdates$ and $\Epoch$.
The epoch in the update specifies the epoch in which the proposal is valid.
$\ProposedPPUpdates$ is a finite maps which is indexed by the hashes of the keys of
entities proposing the given updates, $\KeyHashGen$.
We use the abstract type $\KeyHashGen$ to represent hashes of genesis
(public verification) keys, which have type $\VKeyGen$.
Genesis keys are the keys belonging to the federated
nodes running the Cardano system currently (also referred to as core nodes).
The regular user verification keys are of a type $\VKey$, distinct from the
genesis key type, $\VKeyGen$. Similarly, the type hashes of these
are distinct, $\KeyHash$ and $\KeyHashGen$ respectively.
Currently, updates can only be proposed and voted on by the owners of the genesis keys.
The process of decentralization will result in the core nodes gradually giving up
some of their privileges and responsibilities to the network,
eventually give them \textit{all} up.
The update proposal mechanism will not be decentralized in the Shelley era, however.
For more on the decentralization process, see Section~\ref{sec:new-epoch-trans}.
\subsection{Protocol Parameter Update Proposals}
\label{sec:pp-proposals}
The transition type $\mathsf{PPUP}$ is for proposing updates to protocol
parameters, see Figure \ref{fig:ts-types:pp-update} (for the corresponding rules,
see Figure \ref{fig:rules:pp-update}).
The signal for this transition is an optional update.
Protocol updates for the current epoch are only allowed up until
($2\cdot\StabilityWindow$)-many slots before the end of the epoch.
The reason for this involves how we safely predict hard forks.
Changing the protocol version can result in a hard fork, and we would like an
entire stability period between when we know that a hard fork will necessarily happen
and when the current epoch ends.
Protocol updates can still be submitted during the last
($2\cdot\StabilityWindow$)-many slots of the epoch, but they must
be marked for the following epoch.
The transition $\mathsf{PPUP}$ has three rules:
\begin{itemize}
\item PP-Update-Empty : No new updates were proposed, do nothing.
\item PP-Update-Current : Some new updates $\var{up}$ were proposed
for the current epoch, and the current slot is not too far into the epoch.
Add these to the existing proposals using a right override. That is, if a genesis key
has previously submitted an update proposal, replace it with its new
proposal in $\var{pup}$.
\item PP-Update-Future : Some new updates $\var{up}$ were proposed
for the next epoch, and the current slot is near the end of the epoch.
Add these to the existing future proposals using a right override. That is, if a genesis key
has previously submitted a future update proposal, replace it with its new
proposal in $\var{pup}$.
The future update proposals will become update proposals on the next epoch,
provided they contain no proposals for a protocol version which cannot follow
from the current protocol version.
See the $\mathsf{NEWPP}$ transition in Figure~\ref{fig:rules:new-proto-param},
and the function $\fun{updatePpup}$ from Figure~\ref{fig:ts-types:new-proto-param}.
\end{itemize}
This rule has the following predicate failures:
\begin{enumerate}
\item In the case that the epoch number in the signal is not appropriate for the
slot in the current epoch, there is a \emph{PPUpdateWrongEpoch} failure.
\item In the case of \var{pup} being non-empty, if the check $\dom pup \subseteq
\dom genDelegs$ fails, there is a \emph{NonGenesisUpdate} failure as only genesis keys
can be used in the protocol parameter update.
\item If a protocol parameter update in \var{pup} contains a proposal for a
protocol version which cannot follow from the current protocol version,
there is a \emph{PVCannotFollow} failure.
Note that $\fun{pvCanFollow}$ is defined in Figure~\ref{fig:ts-types:pp-update}.
\end{enumerate}
\begin{figure}[htb]
\emph{Derived types}
\begin{equation*}
\begin{array}{lclr}
\GenesisDelegation
& ~=~
& \KeyHashGen\mapsto(\KeyHash\times\KeyHash_{vrf})
& \text{genesis delegations} \\
\end{array}
\end{equation*}
%
\emph{Protocol Parameter Update environment}
%
\begin{equation*}
\PPUpdateState =
\left(
\begin{array}{r@{~\in~}lr}
\var{pup} & \ProposedPPUpdates & \text{current proposals}\\
\var{fpup} & \ProposedPPUpdates & \text{future proposals}\\
\end{array}
\right)
\end{equation*}
%
\begin{equation*}
\PPUpdateEnv =
\left(
\begin{array}{r@{~\in~}lr}
\var{slot} & \Slot & \text{current slot}\\
\var{pp} & \PParams & \text{protocol parameters}\\
\var{genDelegs} & \GenesisDelegation
& \text{genesis key delegations} \\
\end{array}
\right)
\end{equation*}
%
\emph{Protocol Parameter Update transitions}
\begin{equation*}
\_ \vdash
\var{\_} \trans{ppup}{\_} \var{\_}
\subseteq \powerset (
\PPUpdateEnv \times \PPUpdateState \times \Update^? \times \PPUpdateState)
\end{equation*}
%
\emph{Helper Functions}
\begin{align*}
& \fun{pvCanFollow} \in \ProtVer \to \ProtVer \to \Bool\\
& \fun{pvCanFollow}~(m,~n)~(m',~n') = \\
& ~~~~(m + 1, 0) = (m', n') \lor (m, n + 1) = (m', n')
\end{align*}
%
\caption{Protocol Parameter Update Transition System Types}
\label{fig:ts-types:pp-update}
\end{figure}
\begin{figure}[htb]
\begin{equation}\label{eq:pp-update-Empty}
\inference[PP-Update-Empty]
{
\var{up} = \Nothing
}
{
\begin{array}{r}
\var{slot}\\
\var{pp}\\
\var{genDelegs}\\
\end{array}
\vdash
\left(
\begin{array}{r}
\var{pup_s} \\
\var{fpup_s}
\end{array}
\right)
\trans{ppup}{up}
\left(
\begin{array}{r}
\var{pup_s} \\
\var{fpup_s}
\end{array}
\right)
}
\end{equation}
\nextdef
\begin{equation}\label{eq:update-nonempty-current}
\inference[PP-Update-Current]
{
(\var{pup},~\var{e})\leteq\var{up}
&
\dom{pup}\subseteq\dom{genDelegs}
\\
\forall\var{ps}\in\range{pup},~
\var{pv}\mapsto\var{v}\in\var{ps}\implies\fun{pvCanFollow}~(\fun{pv}~\var{pp})~\var{v}
\\
\var{slot} < \fun{firstSlot}~((\epoch{slot}) + 1) - 2\cdot\StabilityWindow
\\
\epoch{slot} = e
}
{
\begin{array}{c}
\var{slot}\\
\var{pp}\\
\var{genDelegs}\\
\end{array}
\vdash
\left(
\begin{array}{c}
\var{pup_s} \\
\var{fpup_s}
\end{array}
\right)
\trans{ppup}{up}
\left(
\begin{array}{c}
\varUpdate{pup_s\unionoverrideRight pup} \\
\var{fpup_s}
\end{array}
\right)
}
\end{equation}
\nextdef
\begin{equation}\label{eq:update-nonempty-future}
\inference[PP-Update-Future]
{
(\var{pup},~\var{e})\leteq\var{up}
&
\dom{pup}\subseteq\dom{genDelegs}
\\
\forall\var{ps}\in\range{pup},~
\var{pv}\mapsto\var{v}\in\var{ps}\implies\fun{pvCanFollow}~(\fun{pv}~\var{pp})~\var{v}
\\
\var{slot} \geq \fun{firstSlot}~((\epoch{slot}) + 1) - 2\cdot\StabilityWindow
\\
(\epoch{slot}) +1 = e
}
{
\begin{array}{c}
\var{slot}\\
\var{pp}\\
\var{genDelegs}\\
\end{array}
\vdash
\left(
\begin{array}{c}
\var{pup_s} \\
\var{fpup_s}
\end{array}
\right)
\trans{ppup}{up}
\left(
\begin{array}{c}
\var{pup_s} \\
\varUpdate{fpup_s\unionoverrideRight pup} \\
\end{array}
\right)
}
\end{equation}
\caption{Protocol Parameter Update Inference Rules}
\label{fig:rules:pp-update}
\end{figure}
\clearpage
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: