/
utxo.tex
705 lines (645 loc) · 29.8 KB
/
utxo.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
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
\section{UTxO}
\label{sec:utxo}
A key constraint that must always be satisfied as a result and precondition of
a valid ledger state transition is called the \textit{general accounting
property}, or the \textit{preservation of value} condition. Every piece of
software that is a part of the implementation of the
Cardano cryptocurrency must function in such a way as to not result in
a violation of this rule.
If this condition is not satisfied, it is an indicator of
incorrect accounting, potentially due to
malicious disruption or a bug.
The preservation of value is expressed as an equality that uses values in
the ledger state and the environment, as well as the values in the body of
the signal transaction.
We have defined the rules of the delegation protocol in a way that should
consistently satisfy the preservation of value. In the future, we hope to
give a formally-verified proof that every \textit{valid} ledger state satisfies
this property.
In this section, we discuss the relevant accounting that needs to be done
as a result of processing a transaction, i.e.~the deposits for all certificates,
transaction fees, transaction withdrawals and refunds for individual
deregistration, so that we may keep track of whether the preservation of
value is satisfied. Stake pool retirement refunds are not triggered by a
transaction (but rather, happen at the epoch boundary) and are therefore
not considered in our state change rules invoked due to a signal transaction.
Note that when a transaction is issued by a wallet to be applied to the ledger
state (i.e.~processed), the rules in this section are defined in such a way that it is impossible to
apply only some parts of a transaction (e.g.~only certain certificates).
Every part of the transaction must be valid and it must be live, otherwise
it is ignored entirely. It is the wallet's responsibility to inform the user
that a transaction failed to be processed.
\subsection{UTxO Transitions}
\label{sec:utxo-trans}
Figure~\ref{fig:functions:utxo} defines functions needed for the UTxO transition system.
See Figure~\ref{fig:defs:utxo-shelley} for most of the definitions used in the transition system.
\begin{itemize}
\item
The function $\fun{outs}$ creates unspent outputs generated by a transaction, so that
they can be added to the ledger state. For each output in the transaction,
$\fun{outs}$ maps the transaction id and output index to the output.
\item
The $\fun{ubalance}$ function calculates sum total of all the coin in a given UTxO.
\item
The $\fun{wbalance}$ function calculates the total sum of all the reward withdrawals in a
transaction.
\item The calculation $\fun{consumed}$ gives the value consumed by the
transaction $\var{tx}$ in the context of the protocol parameters, the
current UTxO on the ledger and the registered stake credentials. This
calculation is a sum of all coin in the inputs of $\var{tx}$, reward
withdrawals and stake credential deposit refunds. Some of the definitions
used in this function will be defined in Section~\ref{sec:deps-refunds}. In
particular, $\fun{keyRefunds}$ is defined in
Figure~\ref{fig:functions:deposits-refunds} and $\StakeCreds$ is defined in
Figure~\ref{fig:delegation-defs}.
\item The calculation $\fun{produced}$ gives the value produced by the transaction $\var{tx}$
in the context of the protocol parameters and the registered stake pools.
This calculation is a sum of all coin in the outputs of $\var{tx}$,
the transaction fee and all needed deposits.
Some of the definitions used in this function will be defined in
Section~\ref{sec:deps-refunds}.
In particular, $\fun{deposits}$ is defined in Figure~\ref{fig:functions:deposits-refunds}
and $\StakePools$ is defined in Figure~\ref{fig:delegation-defs}.
\end{itemize}
For a transaction and a given ledger state, the preservation of value property holds
exactly when the results of $\fun{consumed}$ equal the results of $\fun{produced}$.
Moreover, when the property holds, value is only moved between transaction outputs,
the reward accounts, the fee pot and the deposit pot.
Note that the $\fun{produced}$ function takes the registered stake pools ($\var{stpools}$)
as a parameter only in order to determine which pool registration certificates are
new (and thus require a deposit) and which ones are updates.
Registration will be discussed more in Section~\ref{sec:delegation-shelley}.
\begin{figure}[htb]
\begin{align*}
& \fun{outs} \in \Tx \to \UTxO
& \text{tx outputs as UTxO} \\
& \fun{outs} ~ \var{tx} =
\left\{
(\fun{txid} ~ \var{tx}, \var{ix}) \mapsto \var{txout} ~
\middle|
\var{ix} \mapsto \var{txout} \in \txouts{tx}
\right\}
\nextdef
& \fun{ubalance} \in \UTxO \to \Coin
& \text{UTxO balance} \\
& \fun{ubalance} ~ utxo = \sum_{(~\wcard ~ \mapsto (\wcard, ~c)) \in \var{utxo}} c
\nextdef
& \fun{wbalance} \in \Wdrl \to \Coin
& \text{withdrawal balance} \\
& \fun{wbalance} ~ ws = \sum_{(\wcard\mapsto c)\in\var{ws}} c
\nextdef
& \fun{consumed} \in \PParams \to \UTxO \to \StakeCreds \to \Tx \to \Coin
& \text{value consumed} \\
& \consumed{pp}{utxo}{stkCreds}{tx} = \\
& ~~\ubalance{(\txins{tx} \restrictdom \var{utxo})} +
\fun{wbalance}~(\fun{txwdrls}~{tx}) \\
& ~~ + \keyRefunds{pp}{stkCreds}{tx} \\
\nextdef
& \fun{produced} \in \PParams \to \StakePools \to \Tx \to \Coin
& \text{value produced} \\
& \fun{produced}~\var{pp}~\var{stpools}~\var{tx} = \\
&~~\ubalance{(\outs{tx})}
+ \txfee{tx} + \deposits{pp}{stpools}~{(\txcerts{tx})}\\
\end{align*}
\caption{Functions used in UTxO rules}
\label{fig:functions:utxo}
\end{figure}
\clearpage
The types for the UTxO transition are given in Figure~\ref{fig:ts-types:utxo-shelley}.
The environment, $\UTxOEnv$, consists of:
\begin{itemize}
\item The current slot.
\item The protocol parameters.
\item The registered stake credentials (which will be explained in
Section~\ref{sec:delegation-shelley}, Figure~\ref{fig:delegation-defs}).
\item The registered stake pools
(also explained in Section~\ref{sec:delegation-shelley},
Figure~\ref{fig:delegation-defs}).
\item The genesis key delegation mapping.
\end{itemize}
The current slot and registrations are needed for the refund calculations
described in Section~\ref{sec:deps-refunds}.
The state needed for the UTxO transition $\UTxOState$, consists of:
\begin{itemize}
\item The current UTxO.
\item The deposit pot.
\item The fee pot.
\item The update state (see Figure~\ref{fig:ts-types:update}).
\end{itemize}
The signal for the UTxO transition is a transaction.
\begin{figure}[htb]
\emph{UTxO environment}
\begin{equation*}
\UTxOEnv =
\left(
\begin{array}{r@{~\in~}lr}
\var{slot} & \Slot & \text{current slot}\\
\var{pp} & \PParams & \text{protocol parameters}\\
\var{stkCreds} & \StakeCreds & \text{stake credential}\\
\var{stpools} & \StakePools & \text{stake pool}\\
\var{genDelegs} & \KeyHashGen\mapsto\KeyHash & \text{genesis key delegations} \\
\end{array}
\right)
\end{equation*}
%
\emph{UTxO States}
\begin{equation*}
\UTxOState =
\left(
\begin{array}{r@{~\in~}lr}
\var{utxo} & \UTxO & \text{UTxO}\\
\var{deposits} & \Coin & \text{deposits pot}\\
\var{fees} & \Coin & \text{fee pot}\\
\var{ups} & \UpdateState & \text{update state}\\
\end{array}
\right)
\end{equation*}
%
\emph{UTxO transitions}
\begin{equation*}
\_ \vdash
\var{\_} \trans{utxo}{\_} \var{\_}
\subseteq \powerset (\UTxOEnv \times \UTxOState \times \Tx \times \UTxOState)
\end{equation*}
%
\caption{UTxO transition-system types}
\label{fig:ts-types:utxo-shelley}
\end{figure}
The UTxO transition system is given in Figure~\ref{fig:rules:utxo-shelley}.
Rule~\ref{eq:utxo-inductive-shelley} specifies the conditions under which a transaction can
be applied to a particular $\UTxOState$ in environment $\UTxOEnv$:
The transition contains the following predicates:
\begin{itemize}
\item
The transaction is live (the current slot is less than its time to live).
\item
The transaction has at least one input.
The global uniqueness of transaction inputs prevents replay attacks.
By requiring that all transactions spend at least one input,
the entire transaction is safe from such attacks.
A delegation certificate by itself, for example, does not have this property.
\item
The fee paid by the transaction has to be greater than or equal to the minimum fee,
which is based on the size of the transaction.
A user or wallet might choose to create a fee larger than necessary
in exchange for a faster processing time.
\item
Each input spent in the transaction must be in the set of unspent
outputs.
\item
The \textit{preservation of value} property must hold.
In other words, the amount of value produced by the transaction must be the same as
the amount consumed.
\item
The $\mathsf{UPDATE}$ transition is successful.
\item
The coin value of each new output must be non-negative.
\item
The transaction size must be below the allowed maximum.
Note that there is an implicit max transaction size given by the max block size,
and that if we wished to allow a transaction to be as large as will fit in a block, this
check would not be needed.
Being able to limit the size below that of the block, however, gives us some
control over how transactions will be packed into the blocks.
\end{itemize}
If all the predicates are satisfied, the state is updated as follows:
\begin{itemize}
\item Update the UTxO:
\begin{itemize}
\item Remove from the UTxO all the $(\var{txin}, \var{txout})$ pairs
associated with the $\var{txins}$'s in the $\var{inputs}$ list of $\var{tx}$.
\item Add all the $\var{outputs}$ of $\var{tx}$ to the
UTxO, associated with the $\fun{txid}~\var{tx}$
\end{itemize}
\item Add all new deposits to the deposit pot and subtract all refunds.
\item Add the transaction fee to the fee pot. Additionally, for any refund
returned by this transaction, add the amount of the original deposit
which has decayed to the fee pot.
The amount decayed will depend on the time to live of the transaction
and will be explained further in Section~\ref{sec:deps-refunds}.
\item Update the current update proposals.
\end{itemize}
The accounting for the reward withdrawals is not done in this transition system.
The rewards are tracked with the delegation state and will
be removed in the final delegation transition, see ~\ref{eq:delegs-base}.
Note here that output entries for both the deposit refunds and the rewards
withdrawals must be included in the body of the transaction
carrying the deregistration certificates (requesting these refunds) and the
reward requests. It is the job
of the wallet to calculate the value of these refunds and withdrawals and
generate the correct outputs to include in the outputs list of $\var{tx}$ such
that applying this transaction results in a
valid ledger update adding correct amounts of coin to the right addresses.
The approach of including refunds and rewards directly in the $outputs$ gives
great flexibility to the management of the coin value obtained from these
accounts, i.e.~it can be directed to any address. However, it means there is no
direct link between the $wdrls$ requests (similarly for the key deregistration
certificate addresses and refund amounts) and the $outputs$. We verify that
the included outputs are correct and authorized through the preservation of value condition
and witnessing the transaction. The combination of the
preservation of value and witnessing, described in Section~\ref{sec:witnesses-shelley},
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
accounts where a reward is accumulated to a specific address.
Note that the $\var{refunded}$ and $\var{decayed}$ values added together give what the
full, non-decayed refund for all the key deregistration certificates in $\var{tx}$
would be and this total value is always removed from the $\var{deposits}$
amount on the ledger. The $\var{refunded}$ amount is returned to the certificate
author and the $\var{decayed}$ amount is transferred over to $\var{fees}$
(this allows the ledger to adhere to the preservation of value).
Note also that the reason only the decayed value of requested refunds
from \textit{this epoch} is transferred to fees is that at the epoch
boundary, the total decayed value for the whole epoch for both the individual
and pool deposits is transferred into the fees (independent of refund
requests).
\begin{figure}[htb]
\begin{equation}\label{eq:utxo-inductive-shelley}
\inference[UTxO-inductive]
{ \txttl tx \geq \var{slot}
& \txins{tx} \neq \emptyset
& \minfee{pp}{tx} \leq \txfee{tx}
& \txins{tx} \subseteq \dom \var{utxo}
\\
\consumed{pp}{utxo}{stkCreds}{rewards}~{tx} = \produced{pp}{stpools}~{tx}
\\
~
\\
{
\begin{array}{r}
\var{slot} \\
\var{pp} \\
\var{genDelegs} \\
\end{array}
}
\vdash \var{ups} \trans{\hyperref[fig:rules:update]{up}}{\fun{txup}~\var{tx}} \var{ups'}
\\
~
\\
\forall (\_\mapsto (\_, c)) \in \txouts{tx}, c \geq 0
\\
\fun{txsize}~{tx}\leq\fun{maxTxSize}~\var{pp}
\\
~
\\
\var{refunded} \leteq \keyRefunds{pp}{stkCreds}~{tx}
\\
\var{decayed} \leteq \decayedTx{pp}{stkCreds}~{tx}
\\
\var{depositChange} \leteq
\deposits{pp}~{stpools}~{(\txcerts{tx})} - (\var{refunded} + \var{decayed})
}
{
\begin{array}{r}
\var{slot}\\
\var{pp}\\
\var{stkCreds}\\
\var{stpools}\\
\var{genDelegs}\\
\end{array}
\vdash
\left(
\begin{array}{r}
\var{utxo} \\
\var{deposits} \\
\var{fees} \\
\var{ups}\\
\end{array}
\right)
\trans{utxo}{tx}
\left(
\begin{array}{r}
\varUpdate{(\txins{tx} \subtractdom \var{utxo}) \cup \outs{tx}} \\
\varUpdate{\var{deposits} + \var{depositChange}} \\
\varUpdate{\var{fees} + \txfee{tx} + \var{decayed}} \\
\varUpdate{ups'}\\
\end{array}
\right)
}
\end{equation}
\caption{UTxO inference rules}
\label{fig:rules:utxo-shelley}
\end{figure}
The UTXO rule has five predicate failures:
\begin{itemize}
\item In the case of any input not being valid, there is a \emph{BadInput}
failure.
\item In the case of the current slot being greater than the time-to-live of the
current transaction, there is an \emph{Expired} failure.
\item In the case of an empty input set, there is a \emph{InputSetEmpty} failure,
in order to prevent replay attacks.
\item If the fees are smaller than the minimal transaction fees, there is a
\emph{FeeTooSmall} failure.
\item If the transaction does not correctly conserve the balance, there is a
\emph{ValueNotConserved} failure.
\end{itemize}
\clearpage
\subsection{Deposits and Refunds}
\label{sec:deps-refunds}
Deposits are described in appendix B.2 of the delegation design document
\cite{delegation_design}. These deposit functions were used above in the UTxO
transition,~\ref{sec:utxo-trans}. Deposits are used for stake credential
registration and pool registration certificates, which will be explained in
Section~\ref{sec:delegation-shelley}. In particular, the function
$\cwitness{}$, which gets the certificate witness from a certificate, will be
defined later. Figure~\ref{fig:functions:deposits-refunds} defines the deposit
and refund functions.
\begin{itemize}
\item The function $\fun{deposits}$ returns the total deposits that have to be
made by a transaction. This calculation is based on the protocol parameters.
Specifically, for a given transaction, it sums up the values of the stake
credential deposits and the stake pool deposits. Those certificates which are
updates of stake pool parameters of already registered pool keys should not
(and are, in fact, not allowed to) make a deposit.
\item The function $\fun{refund}$ calculates the deposit refund with an exponential decay.
\item The function $\fun{keyRefund}$, calculates the refund for an individual
stake credential registration deposit, based on the slot when it was created
and the slot passed to the function. The creation slot should always exist
in the map $\var{stkCreds}$ passed to the function and this would be a good
property to prove about the transition system.
\item The function $\fun{keyRefunds}$, in turn, uses $\fun{keyRefund}$ to calculate
the total value to be refunded to all individual key deregistration certificate authors
in a transaction.
It is important to note here that instead of the \textit{current} slot number,
the time to live of $\var{tx}$ is passed to the $\fun{certRefunds}$ function
within the summation in $\fun{keyRefunds}$. The reason for this is that the
refunds for any key deregistration certificates are, in fact, included in
the $\var{tx}$ itself --- meaning that the coin value of the refund must be
explicitly specified in the outputs of the transaction. So,
the value of the included refund must be calculated before this transaction
is ever processed and be the same \textit{no matter when} the $\var{tx}$
\textit{is actually processed} in order to allow the system to continue to
satisfy the general accounting property.
It is impossible to predict the exact slot number in which $\var{tx}$ will be processed,
but it will be some time before slot number $\fun{txttl}~\var{tx}$. So, this is the slot
number value used in both the calculation to generate the refund coin value in the outputs
of $\var{tx}$ and in the general accounting property equation.
Note also that
$\fun{keyRefunds}$ calculates the total individual refunds for a transaction
based on \textit{current} protocol parameters. This means that any deposits
made prior to a change will be different from their corresponding
(decayed) refunds in the case of key deregistration after a change in
protocol parameters. Constants may only change at the epoch boundary and
ensuring there are always sufficient funds for all
refunds in the $\var{deposits}$ pool is part of the protocol constant
change transition, described in Section~\ref{sec:epoch}.
The protocol parameters are not
expected to change often and using the current ones for the calculation
is a deliberate simplification choice, which does not introduce any inconsistencies
into the system rules or properties. In particular, the general accounting
property is not violated.
\end{itemize}
Figure~\ref{fig:functions:deposits-decay} defines the decays functions.
\begin{itemize}
\item The function $\fun{decayedKey}$ calculates how much of a stake credential
deposit has decayed since the last epoch. Again, this is done using the time
to live of the transaction (and not the current slot, as explained above). At
the epoch boundaries, decayed portions of deposits are moved to the reward
pot, so between epochs we need only account for what has decayed since the
last epoch. The value is calculated by subtracting the refund calculation
based at the epoch boundary from the refund calculation based at the time to
live of the transaction.
\item The function $\fun{decayedTx}$ calculates the total decayed deposits associated
with all the refunds in a given transaction. This function was used earlier in the
UTxO transition in Figure~\ref{fig:rules:utxo-shelley}.
\end{itemize}
Recall that the stake pool retirement refunds are issued not when a certificate
scheduling the retirement is processed, but at the epoch boundary for which
the retirement is scheduled. The decayed value over the full previous epoch is
also accounted for at the boundary change. For details of this accounting, see
Section~\ref{sec:epoch}.
\begin{figure}[htb]
\begin{align*}
& \fun{deposits} \in \PParams \to \StakePools \to \seqof{\DCert} \to \Coin
& \text{total deposits for transaction} \\
& \fun{deposits}~{pp}~{stpools}~{certs} = \\
& \sum\limits_{c\in\var{certs} \cap \DCertRegKey}(\fun{keyDeposit}~pp)
+ \sum\limits_{\substack{
c\in\var{certs}\cap\DCertRegPool \\ (\cwitness{c})\notin \var{stpools}}}
(\fun{poolDeposit}~pp)
\nextdef
& \fun{refund} \in \Coin \to \unitInterval \to \posReals \to \Duration \to \Coin
& \text{refund calculation} \\
& \refund{\dval}{d_{\min}}{\lambda}{\delta} =
\floor*{
\dval \cdot
\left(d_{\min}+(1-d_{\min})\cdot e^{-\lambda\cdot\delta}\right)}
\nextdef
& \fun{keyRefund} \in \Coin \to \unitInterval \to \posReals \to \\
& ~~~~~\StakeCreds \to \Slot \to \DCertDeRegKey \to \Coin
& \text{key refund for a certificate} \\
& \keyRefund{\dval}{d_{\min}}{\lambda}{stkCreds}{slot}{c} =\\
& ~~~~~\begin{cases}
0 & \text{if}~\cwitness c \notin \dom stkCreds \\
\refund{\dval}{d_{\min}}{\lambda}{\delta}
& \text{otherwise}
\end{cases}\\
&
\begin{array}{lr@{~=~}l}
\where
&\delta & \slotminus{slot}{(stkCreds~(\cwitness c))}\\
\end{array}\\
\nextdef
& \fun{keyRefunds} \in \PParams \to \StakeCreds \to \Tx \to \Coin
& \text{key refunds for a transaction} \\
& \keyRefunds{pp}{stkCreds}{tx} =\\
& ~~~~~ \sum\limits_{\substack{c \in (\txcerts{tx} \\ \cap \DCertDeRegKey)}}
\keyRefund{\dval}{d_{\min}}{\lambda}{stkCreds}{(\txttl{tx})}{c}\\
&
\begin{array}{lr@{~=~}l}
\where \\
& \dval & \fun{keyDeposit}~\var{pp}\\
& d_{\min} & \fun{keyMinRefund}~\var{pp}\\
& \lambda & \fun{keyDecayRate}~\var{pp}\\
\end{array}\\
\end{align*}
\caption{Functions used in Deposits - Refunds}
\label{fig:functions:deposits-refunds}
\end{figure}
\begin{figure}[htb]
\begin{align*}
& \fun{decayedKey} \in
\PParams \to \StakeCreds \to \Slot \to \DCertDeRegKey \to \Coin
& \text{decayed since epoch} \\
& \decayedKey{pp}{stkCreds}{cslot}{c} =\\
& \begin{cases}
0 & \text{if}~\cwitness c \notin \dom stkCreds\\
\var{epochRefund} - \var{currentRefund}
& \text{otherwise}
\end{cases}\\
&
\begin{array}{lr@{~=~}l}
\where
& \var{created} & \var{stkCreds}~(\cwitness~\var{c}) \\
& \var{start} & \mathsf{max}~(\fun{firstSlot}~(\epoch{cslot}))~created \\
& \var{epochRefund} & \keyRefund{\dval}{d_{\min}}{\lambda}{stkCreds}{start}{c} \\
& \var{currentRefund} & \keyRefund{\dval}{d_{\min}}{\lambda}{stkCreds}{cslot}{c} \\
& \dval & \fun{keyDeposit}~\var{pp}\\
& d_{\min} & \fun{keyMinRefund}~\var{pp}\\
& \lambda & \fun{keyDecayRate}~\var{pp}\\
\end{array}\\
\nextdef
& \fun{decayedTx} \in \PParams \to \StakeCreds \to \Tx \to \Coin
& \text{decayed deposit portions} \\
& \decayedTx{pp}{stkCreds}{tx} =\\
& \sum\limits_{\substack{c \in (\txcerts{tx} \\ \cap \DCertDeRegKey)}}
\decayedKey{pp}{stkCreds}{(\txttl{tx})}{c}\\
\end{align*}
\caption{Functions used in Deposits - Decay}
\label{fig:functions:deposits-decay}
\end{figure}
\clearpage
\subsection{Witnesses}
\label{sec:witnesses-shelley}
The purpose of witnessing is make sure that the intended action is authorized by
the holder of the signing key, providing replay protection as a consequence.
Replay prevention is an inherent property of UTxO type accounting
since transaction IDs are unique and we require all transaction to
consume at least one input.
A transaction is witnessed by a signature and a verification key corresponding
to this signature. The witnesses, together with the transaction body, form a
full transaction. Every witness in a transaction signs the transaction body.
Moreover, the witnesses are represented as finite maps from verification keys to
signatures, so that any key that is required to sign a transaction only provides
a single witness. This means that, for example, a transaction which includes a
delegation certificate and a reward withdrawal corresponding to the same stake
credential still only includes one signature.
Figure~\ref{fig:functions-witnesses} defines the function which
gathers all the (hashes of) verification keys needed to witness a given transaction.
This consists of:
\begin{itemize}
\item payment keys for outputs being spent
\item stake credentials for reward withdrawals
\item stake credentials for delegation certificates (except \DCertMir{} and \DCertRegKey{})
\item delegates of the genesis keys for any protocol parameter updates
\item stake credentials for the pool owners in a pool registration certificate
\end{itemize}
\begin{figure}[htb]
\begin{align*}
& \fun{propWits} \in \Update \to (\KeyHashGen\mapsto\VKey) \to \powerset{\KeyHash}
& \text{hashkeys for proposals} \\
& \fun{propWits}~(\var{pup},~\var{aup})~\var{genDelegs} = \\
& ~~\left\{
\hashKey{vkey}
\mid
\var{gkey}\mapsto\var{vkey}\in
\left(\left(\dom{\var{pup}}\cup\dom{\var{aup}}\right)\restrictdom\var{genDelegs}\right)
\right\}
\end{align*}
\begin{align*}
& \hspace{-0.8cm}\fun{certWitsNeeded} \Tx \to \powerset{\Credential}
& \text{certificates with witnesses} \\
& \hspace{-0.8cm}\fun{certWitsNeeded}~\var{tx} = \\
& \bigcup\{\cwitness{c} \mid c \in \txcerts{tx} \setminus (\DCertRegKey\cup\DCertMir)\}
\end{align*}
\begin{align*}
& \hspace{-0.8cm}\fun{witsVKeyNeeded} \in \UTxO \to \Tx \to (\KeyHashGen\mapsto\VKey) \to
\powerset{\KeyHash}
& \text{required key hashes} \\
& \hspace{-0.8cm}\fun{witsVKeyNeeded}~\var{utxo}~\var{tx}~\var{genDelegs} = \\
& ~~\{ \fun{paymentHK}~a \mid i \mapsto (a, \wcard) \in \var{utxo},~i\in\fun{txinsVKey}~{tx} \} \\
\cup & ~~
\{\fun{stakeCred_r}~a\mid a\mapsto \wcard \in \AddrRWDVKey
\restrictdom \txwdrls{tx}\}\\
\cup & ~~\fun{certWitsNeeded}~{tx} \\
\cup & ~~\fun{propWits}~(\fun{txup}~\var{tx})~\var{genDelegs} \\
\cup & ~~\bigcup_{\substack{c \in \txcerts{tx} \\ ~c \in\DCertRegPool}} \fun{poolOwners}~{c}
\end{align*}
\begin{align*}
& \hspace{-1cm}\fun{scriptsNeeded} \in \UTxO \to \Tx \to
\powerset{\HashScr}
& \text{required script hashes} \\
& \hspace{-1cm}\fun{scriptsNeeded}~\var{utxo}~\var{tx} = \\
& ~~\{ \fun{validatorHash}~a \mid i \mapsto (a, \wcard) \in \var{utxo},\\
& ~~~~~i\in\fun{txinsScript}~{(\fun{txins~\var{tx}})}~{utxo}\} \\
\cup & ~~\{ \fun{stakeCred_{r}}~\var{a} \mid a \in \dom (\AddrRWDScr
\restrictdom \fun{txwdrls}~\var{tx}) \} \\
\cup & ~~(\AddrScr \cap \fun{certWitsNeeded}~{tx})
\end{align*}
\caption{Functions used in witness rule}
\label{fig:functions-witnesses}
\end{figure}
The UTxOW transition system adds witnessing to the previous UTxO transition system.
Figure~\ref{fig:ts-types:utxow-shelley} defines the type for this transition.
\begin{figure}
\emph{UTxO with witness transitions}
\begin{equation*}
\var{\_} \vdash
\var{\_} \trans{utxow}{\_} \var{\_}
\subseteq \powerset (\UTxOEnv \times \UTxOState \times \Tx \times \UTxOState)
\end{equation*}
\caption{UTxO with witness transition-system types}
\label{fig:ts-types:utxow-shelley}
\end{figure}
Figure~\ref{fig:rules:utxow-shelley} defines UTxOW transition.
It has two predicates:
\begin{itemize}
\item Every signature in the transaction is a valid signature of the transaction body.
\item The set of (hashes of) verification keys given by the transaction is exactly
the set of needed (hashes of) verification keys.
\end{itemize}
If the predicates are satisfied, the state is transitioned by the UTxO transition rule.
\begin{figure}
\begin{equation}
\label{eq:utxo-witness-inductive-shelley}
\inference[UTxO-wit]
{
(utxo, \wcard, \wcard) \leteq \var{utxoSt} \\
\var{witsKeyHashes} \leteq \{\fun{hashKey}~\var{vk} \vert \var{vk} \in
\dom (\txwitsVKey{tx}) \}\\~\\
\forall \var{hs} \mapsto \var{validator} \in \fun{txwitsScript}~{tx},\\
\fun{hashScript}~\var{validator} = \var{hs} \wedge
\fun{validateScript}~\var{validator}~\var{tx}\\~\\
\fun{scriptsNeeded}~\var{utxo}~\var{tx} = \dom (\fun{txwitsScript}~{tx})
\\~\\
\forall \var{vk} \mapsto \sigma \in \txwitsVKey{tx},
\mathcal{V}_{\var{vk}}{\serialised{\txbody{tx}}}_{\sigma} \\
\fun{witsVKeyNeeded}~{utxo}~{tx}~{genDelegs} \subseteq witsKeyHashes
\\~\\
genSig \leteq
\left\{
\fun{hashKey}~gkey \vert gkey \in\dom{genDelegs}
\right\}
\cap
\var{witsKeyHashes}
\\
\left\{
c\in\txcerts{tx}~\cap\DCertMir
\right\} \neq\emptyset \implies \vert genSig\vert \geq \Quorum \wedge
\fun{d}~\var{pp} > 0
\\~\\
{
\begin{array}{r}
\var{slot}\\
\var{pp}\\
\var{stkCreds}\\
\var{stpools}\\
\var{genDelegs}\\
\end{array}
}
\vdash \var{utxoSt} \trans{\hyperref[fig:rules:utxo-shelley]{utxo}}{tx}
\var{utxoSt'}\\
}
{
\begin{array}{r}
\var{slot}\\
\var{pp}\\
\var{stkCreds}\\
\var{stpools}\\
\var{genDelegs}\\
\end{array}
\vdash \var{utxoSt} \trans{utxow}{tx} \varUpdate{\var{utxoSt'}}
}
\end{equation}
\caption{UTxO with witnesses inference rules}
\label{fig:rules:utxow-shelley}
\end{figure}
The UTXOW rule has two predicate failures:
\begin{itemize} %TODO: add multi-sig script failure predicates
\item In the case of an incorrect witness, there is a \emph{InvalidWitnesses}
failure.
\item In the case of a missing witness, there is a \emph{MissingVKeyWitnesses}
failure.
\end{itemize}
\clearpage