Skip to content

Commit ee7c200

Browse files
carlostomecarlostome
committed
Add UTXOW preconditions
1 parent 457901c commit ee7c200

File tree

6 files changed

+166
-48
lines changed

6 files changed

+166
-48
lines changed

‎src/Ledger/Dijkstra/Specification/Ledger.lagda.md‎

Lines changed: 35 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
---
1+
--
22
source_branch: master
33
source_path: src/Ledger/Dijkstra/Specification/Ledger.lagda
44
---
@@ -46,7 +46,10 @@ record SubLedgerEnv : Type where
4646
pparams : PParams
4747
enactState : EnactState
4848
treasury : Treasury
49-
isValid : Bool
49+
utxo₀ : UTxO
50+
isTopLevelValid : Bool
51+
globalScripts : ℙ Script
52+
globalData : DataHash ⇀ Datum
5053
5154
record LedgerEnv : Type where
5255
field
@@ -172,6 +175,7 @@ private variable
172175
Γ : LedgerEnv
173176
s s' s'' : LState
174177
utxoState utxoState' : UTxOState
178+
utxo₀ : UTxO
175179
govState govState' : GovState
176180
certState certState' : CertState
177181
stx : SubLevelTx
@@ -181,33 +185,36 @@ private variable
181185
enactState : EnactState
182186
treasury : Treasury
183187
isTopLevelValid : Bool
188+
globalScripts : ℙ Script
189+
globalData : DataHash ⇀ Datum
184190
```
185191
-->
186192

187193
```agda
188194
data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LState → SubLevelTx → LState → Type where
189195
SUBLEDGER-V :
190-
let txb = stx .txBody
196+
let txb = stx .txBody
197+
191198
```
192199
<!--
193200
```agda
194-
open TxBody txb
201+
open TxBody txb
195202
```
196203
-->
197204
```agda
198205
in
199206
∙ isTopLevelValid ≡ true
200-
∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
207+
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , globalScripts , globalData ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
201208
∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
202209
∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
203210
────────────────────────────────
204-
⟦ slot , ppolicy , pp , enactState , treasury , isTopLevelValid ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState' , govState' , certState' ⟧
211+
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , globalScripts , globalData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState' , govState' , certState' ⟧
205212
206213
SUBLEDGER-I :
207214
∙ isTopLevelValid ≡ false
208-
∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
215+
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , globalScripts , globalData ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
209216
────────────────────────────────
210-
⟦ slot , ppolicy , pp , enactState , treasury , isTopLevelValid ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState , govState , certState ⟧
217+
⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , globalScripts , globalData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState , govState , certState ⟧
211218
212219
_⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LState → List SubLevelTx → LState → Type
213220
_⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
@@ -227,6 +234,14 @@ private variable
227234
data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState → Type where
228235
LEDGER-V :
229236
let txb = tx .txBody
237+
238+
utxo₀ = UTxOOf utxoState
239+
240+
globalScripts : ℙ Script
241+
globalScripts = ∅ -- TODO
242+
243+
globalData : DataHash ⇀ Datum
244+
globalData = ∅ -- TODO
230245
```
231246
<!--
232247
```agda
@@ -236,15 +251,23 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState
236251
```agda
237252
in
238253
∙ isValid tx ≡ true
239-
∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState' , govState' , certState' ⟧
240-
∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
254+
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isValid tx , globalScripts , globalData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState' , govState' , certState' ⟧
255+
∙ ⟦ slot , pp , treasury , utxo₀ , isValid tx , globalScripts , globalData ⟧ ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
241256
∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState' ⇀⦇ txCerts ,CERTS⦈ certState''
242257
∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
243258
────────────────────────────────
244259
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState'' , govState'' , certState'' ⟧
245260
246261
LEDGER-I :
247262
let txb = tx .txBody
263+
264+
utxo₀ = UTxOOf utxoState
265+
266+
globalScripts : ℙ Script
267+
globalScripts = ∅ -- TODO
268+
269+
globalData : DataHash ⇀ Datum
270+
globalData = ∅ -- TODO
248271
```
249272
<!--
250273
```agda
@@ -254,8 +277,8 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState
254277
```agda
255278
in
256279
∙ isValid tx ≡ false
257-
∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState , govState , certState ⟧
258-
∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
280+
∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isValid tx , globalScripts , globalData ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState , govState , certState ⟧
281+
∙ ⟦ slot , pp , treasury , utxo₀ , isValid tx , globalScripts , globalData ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
259282
────────────────────────────────
260283
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState' , govState , certState ⟧
261284
```

‎src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -156,12 +156,12 @@ credsNeededMinusCollateral txb = a ∪ b ∪ c ∪ d ∪ e
156156
e = mapPartial (λ p → if PolicyOf p then (λ {sh} → just (Propose p , ScriptObj sh)) else nothing)
157157
(fromList (GovProposalsOf txb))
158158
159-
credsNeeded : (ℓ : TxLevel) → UTxO → (TxBody ℓ) → ℙ (ScriptPurpose × Credential)
160-
credsNeeded TxLevelTop utxo txb = credsNeededMinusCollateral txb
159+
credsNeeded : {ℓ : TxLevel} → UTxO → (TxBody ℓ) → ℙ (ScriptPurpose × Credential)
160+
credsNeeded {TxLevelTop} utxo txb = credsNeededMinusCollateral txb
161161
∪ mapˢ (λ (i , o) → (Spend i , payCred (proj₁ o))) ((utxo ∣ (txIns ∪ collateralInputs)) ˢ)
162162
where open TxBody txb
163163
164-
credsNeeded TxLevelSub utxo txb = credsNeededMinusCollateral txb
164+
credsNeeded {TxLevelSub} utxo txb = credsNeededMinusCollateral txb
165165
∪ mapˢ (λ (i , o) → (Spend i , payCred (proj₁ o))) ((utxo ∣ txIns) ˢ)
166166
where open TxBody txb
167167

‎src/Ledger/Dijkstra/Specification/Transaction.lagda.md‎

Lines changed: 6 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -404,6 +404,9 @@ This section collects some unimportant but useful helper and accessor functions.
404404
txinsScript : ℙ TxIn → UTxO → ℙ TxIn
405405
txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))
406406
407+
txOutToScript : TxOut → Maybe Script
408+
txOutToScript (_ , _ , _ , s) = s
409+
407410
refScripts : Tx txLevel → UTxO → List Script
408411
refScripts tx utxo =
409412
mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) $ setToList (range (utxo ∣ (txIns ∪ refInputs)))
@@ -414,26 +417,9 @@ This section collects some unimportant but useful helper and accessor functions.
414417
where open Tx; open TxWitnesses
415418
416419
lookupScriptHash : ScriptHash → Tx txLevel → UTxO → Maybe Script
417-
lookupScriptHash sh tx utxo =
418-
if sh ∈ mapˢ proj₁ (m ˢ) then
419-
just (lookupᵐ m sh)
420-
else
421-
nothing
422-
where m = setToMap (mapˢ < hash , id > (txscripts tx utxo))
423-
424-
getSubTxScripts : SubLevelTx → ℙ (TxId × ScriptHash)
425-
getSubTxScripts subtx = mapˢ (λ hash → (TxIdOf subtx , hash)) (ScriptHashes subtx)
426-
where
427-
ScriptHashes : Tx TxLevelSub → ℙ ScriptHash
428-
ScriptHashes tx = -- `txRequiredTopLevelGuards`
429-
mapPartial (isScriptObj ∘ proj₁) -- has key creds too, but only
430-
(TxBody.txRequiredTopLevelGuards (TxBodyOf tx)) -- `ScriptObj hash` contributes
431-
-- a phase-2 script hash.
432-
433-
getTxScripts : {ℓ : TxLevel} → Tx ℓ → ℙ (TxId × ScriptHash)
434-
getTxScripts {TxLevelSub} = getSubTxScripts
435-
getTxScripts {TxLevelTop} =
436-
concatMapˢ getSubTxScripts ∘ fromList ∘ TxBody.txSubTransactions ∘ TxBodyOf
420+
lookupScriptHash sh tx utxo = lookupHash sh (txscripts tx utxo)
421+
422+
-- TODO: implement the actual evolving `utxoRefView` (issue #1006)
437423
```
438424

439425
CIP-0118 models "required top-level guards" as a list of requirements coming

‎src/Ledger/Dijkstra/Specification/Utxo.lagda.md‎

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,13 @@ open import Ledger.Dijkstra.Specification.Script.Validation txs abs
3838
```agda
3939
record UTxOEnv : Type where
4040
field
41-
slot : Slot
42-
pparams : PParams
43-
treasury : Treasury
41+
slot : Slot
42+
pparams : PParams
43+
treasury : Treasury
44+
utxo₀ : UTxO
45+
isTopLevelValid : Bool
46+
globalRefInputsScripts : ℙ Script
47+
globalData : DataHash ⇀ Datum
4448
4549
record UTxOState : Type where
4650
field
@@ -56,6 +60,9 @@ instance
5660
unquoteDecl HasCast-UTxOEnv HasCast-UTxOState = derive-HasCast
5761
( (quote UTxOEnv , HasCast-UTxOEnv ) ∷
5862
[ (quote UTxOState , HasCast-UTxOState) ])
63+
64+
HasUTxO-UTxOState : HasUTxO UTxOState
65+
HasUTxO-UTxOState .HasUTxO.UTxOOf = UTxOState.utxo
5966
```
6067
-->
6168

‎src/Ledger/Dijkstra/Specification/Utxow.lagda.md‎

Lines changed: 108 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,7 @@ source_branch: master
33
source_path: src/Ledger/Dijkstra/Specification/Utxow.lagda.md
44
---
55

6-
# UTxOW (Dijkstra skeleton)
7-
8-
This is a **minimal skeleton** of the Dijkstra-era witnessing layer.
9-
10-
It currently acts as a wrapper around `UTXO`, mirroring Conway's shape, but without
11-
committing to full witnessing checks yet.
6+
# UTxOW
127

138
<!--
149
```agda
@@ -24,30 +19,133 @@ module Ledger.Dijkstra.Specification.Utxow
2419
where
2520
2621
open import Ledger.Dijkstra.Specification.Utxo txs abs
22+
open import Ledger.Dijkstra.Specification.Script.Validation txs abs
2723
2824
private variable
25+
ℓ : TxLevel
2926
Γ : UTxOEnv
3027
s s' : UTxOState
3128
tx : TopLevelTx
3229
stx : SubLevelTx
3330
```
3431
-->
3532

33+
```agda
34+
languages : Tx ℓ → UTxO → ℙ Language
35+
languages tx utxo = ∅ -- TODO
36+
37+
allowedLanguages : Tx ℓ → UTxO → ℙ Language
38+
allowedLanguages tx utxo = ∅ -- TODO
39+
```
40+
3641
```agda
3742
data _⊢_⇀⦇_,SUBUTXOW⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where
3843
3944
SUBUTXOW :
45+
let
46+
open Tx tx
47+
open TxBody txBody
48+
open TxWitnesses txWitnesses
49+
open UTxOEnv
50+
51+
utxo₀ = Γ .utxo₀
52+
utxo = s .UTxOState.utxo
53+
54+
witsKeyHashes : ℙ KeyHash
55+
witsKeyHashes = mapˢ hash (dom vKeySigs)
56+
57+
allScripts : ℙ Script
58+
allScripts =
59+
( scripts -- (1) scripts from witnesses
60+
∪ mapPartial txOutToScript
61+
( range (utxo₀ ∣ txIns) -- (2) scripts from transaction inputs
62+
∪ range (utxo ∣ refInputs) -- (3) scripts from reference inputs
63+
)
64+
∪ Γ .globalRefInputsScripts -- (4) scripts from global reference inputs
65+
)
66+
67+
p1Scripts : ℙ P1Script
68+
p1Scripts = mapPartial toP1Script allScripts
69+
70+
p2Scripts : ℙ P2Script
71+
p2Scripts = mapPartial toP2Script allScripts
72+
73+
neededScriptHashes : ℙ ScriptHash
74+
neededScriptHashes = mapPartial (isScriptObj ∘ proj₂) (credsNeeded utxo₀ txBody)
75+
76+
neededVKeyHashes : ℙ KeyHash
77+
neededVKeyHashes = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo₀ txBody)
78+
79+
neededDataHashes : ℙ DataHash
80+
neededDataHashes = mapPartial (λ txOut@(a , _ , d , _) → do sh ← isScriptObj (payCred a)
81+
_ ← lookupHash sh p2Scripts
82+
d >>= isInj₂)
83+
(range (utxo₀ ∣ txIns))
84+
85+
in
86+
∙ ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
87+
∙ ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
88+
∙ neededVKeyHashes ⊆ witsKeyHashes
89+
∙ neededScriptHashes ⊆ mapˢ hash allScripts
90+
∙ neededDataHashes ⊆ dom (Γ .globalData)
91+
∙ languages tx utxo ⊆ allowedLanguages tx utxo
92+
∙ txADhash ≡ map hash txAuxData
4093
∙ Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'
4194
────────────────────────────────
4295
Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s'
4396
4497
data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
4598
4699
UTXOW :
47-
∙ Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
100+
let
101+
open Tx tx
102+
open TxBody txBody
103+
open TxWitnesses txWitnesses
104+
open UTxOEnv
105+
106+
utxo₀ = Γ .utxo₀
107+
utxo = s .UTxOState.utxo
108+
109+
witsKeyHashes : ℙ KeyHash
110+
witsKeyHashes = mapˢ hash (dom vKeySigs)
111+
112+
allScripts : ℙ Script
113+
allScripts =
114+
( scripts -- (1) scripts from witnesses
115+
∪ mapPartial txOutToScript
116+
( range (utxo₀ ∣ txIns) -- (2) scripts from transaction inputs
117+
∪ range (utxo ∣ refInputs) -- (3) scripts from reference inputs
118+
)
119+
∪ Γ .globalRefInputsScripts -- (4) scripts from global reference inputs
120+
)
121+
122+
p1Scripts : ℙ P1Script
123+
p1Scripts = mapPartial toP1Script allScripts
124+
125+
p2Scripts : ℙ P2Script
126+
p2Scripts = mapPartial toP2Script allScripts
127+
128+
neededScriptHashes : ℙ ScriptHash
129+
neededScriptHashes = mapPartial (isScriptObj ∘ proj₂) (credsNeeded utxo₀ txBody)
130+
131+
neededVKeyHashes : ℙ KeyHash
132+
neededVKeyHashes = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo₀ txBody)
133+
134+
neededDataHashes : ℙ DataHash
135+
neededDataHashes = mapPartial (λ txOut@(a , _ , d , _) → do sh ← isScriptObj (payCred a)
136+
_ ← lookupHash sh p2Scripts
137+
d >>= isInj₂)
138+
(range (utxo₀ ∣ txIns))
139+
140+
in
141+
∙ ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
142+
∙ ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
143+
∙ neededVKeyHashes ⊆ witsKeyHashes
144+
∙ neededScriptHashes ⊆ mapˢ hash allScripts
145+
∙ neededDataHashes ⊆ dom (Γ .globalData)
146+
∙ languages tx utxo ⊆ allowedLanguages tx utxo
147+
∙ txADhash ≡ map hash txAuxData
148+
∙ Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
48149
────────────────────────────────
49150
Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
50151
```
51-
52-
This file intentionally contains **no** additional premises yet. As Dijkstra witnessing
53-
evolves, this is where signature / script / datum / language constraints can be added.

‎src/Ledger/Prelude.lagda.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -86,4 +86,8 @@ module Filter where
8686
filter : ∀ {a} {p} {A : Type a} → (P : Pred A p) → ⦃ P ⁇¹ ⦄ → List A → List A
8787
filter P = Data.List.filter ¿ P ¿¹
8888
89+
lookupHash : ∀ {T H : Type} ⦃ _ : DecEq H ⦄ ⦃ _ : Hashable T H ⦄ → H → ℙ T → Maybe T
90+
lookupHash h s =
91+
if h ∈ mapˢ proj₁ (m ˢ) then just (lookupᵐ m h) else nothing
92+
where m = setToMap (mapˢ < hash , id > s)
8993
```

0 commit comments

Comments
 (0)