-
Notifications
You must be signed in to change notification settings - Fork 12
/
Chain.lagda
116 lines (100 loc) · 3.56 KB
/
Chain.lagda
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
\section{Blockchain layer}
\begin{code}[hide]
{-# OPTIONS --safe #-}
open import Algebra
open import Data.Nat.Properties using (+-0-monoid)
open import Ledger.Prelude; open Equivalence
open import Ledger.Transaction
open import Ledger.Abstract
module Ledger.Chain
(txs : _) (open TransactionStructure txs)
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
where
open import Ledger.Ledger txs abs
open import Ledger.Ratify txs
open import Ledger.Utxo txs abs
open import Ledger.Epoch txs abs
open import Ledger.Zone txs abs
\end{code}
\begin{figure*}[h]
\begin{code}
record ChainState : Set where
field newEpochState : NewEpochState
record Block : Set where
field zns : List (List Tx)
slot : Slot
\end{code}
\caption{Definitions CHAIN transition system}
\end{figure*}
\begin{code}[hide]
private variable
s : ChainState
b : Block
ls' : LState
nes : NewEpochState
instance _ = +-0-monoid
-- TODO: do we still need this for anything?
maybePurpose : DepositPurpose → (DepositPurpose × Credential) → Coin → Maybe Coin
maybePurpose prps (prps' , _) c with prps ≟ prps'
... | yes _ = just c
... | no _ = nothing
maybePurpose-prop : ∀ {prps} {x} {y}
→ (m : (DepositPurpose × Credential) ⇀ Coin)
→ (x , y) ∈ dom ((mapMaybeWithKeyᵐ (maybePurpose prps) m) ˢ)
→ x ≡ prps
maybePurpose-prop {prps = prps} {x} {y} _ xy∈dom with to dom∈ xy∈dom
... | z , ∈mmwk with prps ≟ x | ∈-mapMaybeWithKey {f = maybePurpose prps} ∈mmwk
... | yes refl | _ = refl
filterPurpose : DepositPurpose → (DepositPurpose × Credential) ⇀ Coin → Credential ⇀ Coin
filterPurpose prps m = mapKeys proj₂ (mapMaybeWithKeyᵐ (maybePurpose prps) m)
{λ where x∈dom y∈dom refl → cong (_, _)
$ trans (maybePurpose-prop {prps = prps} m x∈dom)
$ sym (maybePurpose-prop {prps = prps} m y∈dom)}
govActionDeposits : LState → VDeleg ⇀ Coin
govActionDeposits ls =
let open LState ls; open CertState certState; open PState pState
open UTxOState utxoSt; open DState dState
in foldl _∪⁺_ ∅ $ setToList $
mapPartial
(λ where (gaid , record { returnAddr = record {stake = c} }) → do
vd ← lookupᵐ? voteDelegs c
dep ← lookupᵐ? deposits (GovActionDeposit gaid)
just ❴ vd , dep ❵ )
(fromList govSt)
calculateStakeDistrs : LState → StakeDistrs
calculateStakeDistrs ls =
let open LState ls; open CertState certState; open PState pState
open UTxOState utxoSt; open DState dState
spoDelegs = ∅ -- TODO
drepDelegs = ∅ -- TODO
in
record
{ stakeDistr = govActionDeposits ls
}
data
\end{code}
\begin{figure*}[h]
\begin{code}
_⊢_⇀⦇_,CHAIN⦈_ : ⊤ → ChainState → Block → ChainState → Set
\end{code}
\caption{Type of the CHAIN transition system}
\end{figure*}
\begin{code}[hide]
where
\end{code}
\begin{figure*}[h]
\begin{code}
CHAIN :
let open ChainState s; open Block b; open NewEpochState newEpochState
open EpochState epochState; open EnactState es
in
record { stakeDistrs = calculateStakeDistrs ls }
⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
→ ⟦ slot , constitution .proj₁ .proj₂ , pparams .proj₁ , es ⟧ˡᵉ
⊢ ls ⇀⦇ zns ,ZONES⦈ ls'
────────────────────────────────
_ ⊢ s ⇀⦇ b ,CHAIN⦈
record s { newEpochState = record nes { epochState = record epochState { ls = ls'} } }
\end{code}
\caption{CHAIN transition system}
\end{figure*}