-
Notifications
You must be signed in to change notification settings - Fork 12
/
Transaction.lagda
214 lines (178 loc) · 6.36 KB
/
Transaction.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
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
\section{Transactions}
\label{sec:transactions}
\begin{code}[hide]
{-# OPTIONS --safe #-}
--------------------------------------------------------------------------------
-- NOTE: Everything in this module is part of TransactionStructure
--------------------------------------------------------------------------------
module Ledger.Transaction where
import Data.Maybe.Base as M
open import Ledger.Prelude renaming (filterᵐ to filter)
open import Ledger.Crypto
open import Ledger.Types.Epoch
open import Ledger.Types.GovStructure
import Ledger.PParams
import Ledger.Script
import Ledger.GovernanceActions
import Ledger.Deleg
import Ledger.TokenAlgebra
import Ledger.Address
open import Tactic.Derive.DecEq
open import MyDebugOptions
open import Relation.Nullary.Decidable using (⌊_⌋)
data Tag : Set where
Spend Mint Cert Rewrd Vote Propose : Tag
unquoteDecl DecEq-Tag = derive-DecEq ((quote Tag , DecEq-Tag) ∷ [])
record TransactionStructure : Set₁ where
field
\end{code}
Transactions are defined in Figure~\ref{fig:defs:transactions}. A
transaction is made up of a transaction body, a collection of
witnesses and some optional auxiliary data. Some key ingredients in
the transaction body are:
\begin{itemize}
\item A set of transaction inputs, each of which identifies an output from a previous transaction.
A transaction input consists of a transaction id and an index to uniquely identify the output.
\item An indexed collection of transaction outputs.
The \TxOut type is an address paired with a coin value.
\item A transaction fee. This value will be added to the fee pot.
\item The size and the hash of the serialized form of the transaction that was included in the block.
\end{itemize}
\begin{figure*}[h]
\emph{Abstract types}
\begin{code}
Ix TxId AuxiliaryData : Set
\end{code}
\begin{code}[hide]
⦃ DecEq-Ix ⦄ : DecEq Ix
⦃ DecEq-TxId ⦄ : DecEq TxId
adHashingScheme : isHashableSet AuxiliaryData
open isHashableSet adHashingScheme renaming (THash to ADHash) public
field globalConstants : _
open GlobalConstants globalConstants public
field crypto : _
open Crypto crypto public
open Ledger.TokenAlgebra ScriptHash public
open Ledger.Address Network KeyHash ScriptHash public
field epochStructure : _
open EpochStructure epochStructure public
open Ledger.Script crypto epochStructure public
field scriptStructure : _
open ScriptStructure scriptStructure public
open Ledger.PParams crypto epochStructure scriptStructure public
field govParams : _
open GovParams govParams public
field tokenAlgebra : TokenAlgebra
open TokenAlgebra tokenAlgebra public
field txidBytes : TxId → Ser
networkId : Network
govStructure : GovStructure
govStructure = record
-- TODO: figure out what to do with the hash
{ TxId = TxId; Network = Network; DocHash = ADHash
; crypto = crypto
; epochStructure = epochStructure
; scriptStructure = scriptStructure
; govParams = govParams
}
open Ledger.GovernanceActions govStructure hiding (Vote; yes; no; abstain) public
open Ledger.Deleg govStructure public
\end{code}
\begin{NoConway}
\emph{Derived types}
\begin{code}
TxIn = TxId × Ix
TxOut = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script
UTxO = TxIn ⇀ TxOut
Wdrl = RwdAddr ⇀ Coin
RdmrPtr = Tag × Ix
ProposedPPUpdates = KeyHash ⇀ PParamsUpdate
Update = ProposedPPUpdates × Epoch
\end{code}
\end{NoConway}
\emph{Transaction types}
\begin{AgdaMultiCode}
\begin{code}
record TxBody : Set where
field txins : ℙ TxIn
refInputs : ℙ TxIn
txouts : Ix ⇀ TxOut
txfee : Coin
mint : Value
txvldt : Maybe Slot × Maybe Slot
txcerts : List DCert
txwdrls : Wdrl
txvote : List GovVote
txprop : List GovProposal
txdonation : Coin
txup : Maybe Update
txADhash : Maybe ADHash
netwrk : Maybe Network
txsize : ℕ
txid : TxId
collateral : ℙ TxIn
reqSigHash : ℙ KeyHash
scriptIntHash : Maybe ScriptHash
\end{code}
\begin{NoConway}
\begin{code}
record TxWitnesses : Set where
field vkSigs : VKey ⇀ Sig
scripts : ℙ Script
txdats : DataHash ⇀ Datum
txrdmrs : RdmrPtr ⇀ Redeemer × ExUnits
scriptsP1 : ℙ P1Script
scriptsP1 = mapPartial isInj₁ scripts
record Tx : Set where
field body : TxBody
wits : TxWitnesses
isValid : Bool
txAD : Maybe AuxiliaryData
\end{code}
\end{NoConway}
\end{AgdaMultiCode}
\caption{Transactions and related types}
\label{fig:defs:transactions}
\end{figure*}
\begin{NoConway}
\begin{figure*}[h]
\begin{code}
getValue : TxOut → Value
getValue (_ , v , _) = v
TxOutʰ = Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe ScriptHash
txOutHash : TxOut → TxOutʰ
txOutHash (a , v , d , s) = a , (v , (d , M.map hash s))
getValueʰ : TxOutʰ → Value
getValueʰ (_ , v , _) = v
txinsVKey : ℙ TxIn → UTxO → ℙ TxIn
txinsVKey txins utxo = txins ∩ dom (utxo ↾' (isVKeyAddr ∘ proj₁))
scriptOuts : UTxO → UTxO
scriptOuts utxo = filter (λ (_ , addr , _) → isScriptAddr addr) utxo
txinsScript : ℙ TxIn → UTxO → ℙ TxIn
txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))
refScripts : Tx → UTxO → ℙ Script
refScripts tx utxo =
mapPartial (proj₂ ∘ proj₂ ∘ proj₂) (range (utxo ∣ (txins ∪ refInputs)))
where open Tx; open TxBody (tx .body)
txscripts : Tx → UTxO → ℙ Script
txscripts tx utxo = scripts (tx .wits) ∪ refScripts tx utxo
where open Tx; open TxWitnesses
lookupScriptHash : ScriptHash → Tx → UTxO → Maybe Script
lookupScriptHash sh tx utxo =
if sh ∈ mapˢ proj₁ (m ˢ) then
just (lookupᵐ m sh)
else
nothing
where m = setToHashMap (txscripts tx utxo)
\end{code}
\caption{Functions related to transactions}
\label{fig:defs:transaction-funs}
\end{figure*}
\end{NoConway}
\begin{code}[hide]
isP2Script : Script → Bool
isP2Script = is-just ∘ isInj₂
instance
HasCoin-TxOut : HasCoin TxOut
HasCoin-TxOut .getCoin = coin ∘ proj₁ ∘ proj₂
\end{code}