Skip to content

Commit 44095d7

Browse files
carlostomecarlostome
committed
Add UTXOW preconditions
1 parent 42eeaeb commit 44095d7

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 & 13 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,34 +185,36 @@ private variable
181185
enactState : EnactState
182186
treasury : Treasury
183187
isTopLevelValid : Bool
184-
utxo₀ : UTxO
188+
globalScripts : ℙ Script
189+
globalData : DataHash ⇀ Datum
185190
```
186191
-->
187192

188193
```agda
189194
data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LState → SubLevelTx → LState → Type where
190195
SUBLEDGER-V :
191-
let txb = stx .txBody
196+
let txb = stx .txBody
197+
192198
```
193199
<!--
194200
```agda
195-
open TxBody txb
201+
open TxBody txb
196202
```
197203
-->
198204
```agda
199205
in
200206
∙ isTopLevelValid ≡ true
201-
∙ ⟦ slot , pp , treasury , utxo₀ ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
207+
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , globalScripts , globalData ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
202208
∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
203209
∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
204210
────────────────────────────────
205-
⟦ 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' ⟧
206212
207213
SUBLEDGER-I :
208214
∙ isTopLevelValid ≡ false
209-
∙ ⟦ slot , pp , treasury , utxo₀ ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
215+
∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , globalScripts , globalData ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
210216
────────────────────────────────
211-
⟦ 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 ⟧
212218
213219
_⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LState → List SubLevelTx → LState → Type
214220
_⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_}
@@ -228,6 +234,14 @@ private variable
228234
data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState → Type where
229235
LEDGER-V :
230236
let txb = tx .txBody
237+
238+
utxo₀ = UTxOOf utxoState
239+
240+
globalScripts : ℙ Script
241+
globalScripts = ∅ -- TODO
242+
243+
globalData : DataHash ⇀ Datum
244+
globalData = ∅ -- TODO
231245
```
232246
<!--
233247
```agda
@@ -237,15 +251,23 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState
237251
```agda
238252
in
239253
∙ isValid tx ≡ true
240-
∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState' , govState' , certState' ⟧
241-
∙ ⟦ slot , pp , treasury , utxo₀ ⟧ ⊢ 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''
242256
∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState' ⇀⦇ txCerts ,CERTS⦈ certState''
243257
∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
244258
────────────────────────────────
245259
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState'' , govState'' , certState'' ⟧
246260
247261
LEDGER-I :
248262
let txb = tx .txBody
263+
264+
utxo₀ = UTxOOf utxoState
265+
266+
globalScripts : ℙ Script
267+
globalScripts = ∅ -- TODO
268+
269+
globalData : DataHash ⇀ Datum
270+
globalData = ∅ -- TODO
249271
```
250272
<!--
251273
```agda
@@ -255,8 +277,8 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState
255277
```agda
256278
in
257279
∙ isValid tx ≡ false
258-
∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState , govState , certState ⟧
259-
∙ ⟦ slot , pp , treasury , utxo₀ ⟧ ⊢ 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'
260282
────────────────────────────────
261283
⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState' , govState , certState ⟧
262284
```

‎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: 4 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -435,6 +435,9 @@ Thus functions like `refScripts`{.AgdaFunction}, `txscripts`{.AgdaFunction},
435435
and `lookupScriptHash`{.AgdaFunction} (defined below) will take *two* UTxO arguments.
436436

437437
```agda
438+
txOutToScript : TxOut → Maybe Script
439+
txOutToScript (_ , _ , _ , s) = s
440+
438441
refScripts : Tx txLevel → UTxO → UTxO → List Script
439442
refScripts tx utxoSpend₀ utxoRefView =
440443
mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) ( setToList (range (utxoSpend₀ ∣ txIns))
@@ -448,25 +451,9 @@ and `lookupScriptHash`{.AgdaFunction} (defined below) will take *two* UTxO argum
448451
where open Tx; open TxWitnesses
449452
450453
lookupScriptHash : ScriptHash → Tx txLevel → UTxO → UTxO → Maybe Script
451-
lookupScriptHash sh tx utxoSpend₀ utxoRefView =
452-
if sh ∈ mapˢ proj₁ (m ˢ) then just (lookupᵐ m sh) else nothing
453-
where m = setToMap (mapˢ < hash , id > (txscripts tx utxoSpend₀ utxoRefView))
454+
lookupScriptHash sh tx utxoSpend₀ utxoRefView = lookupHash sh (txscripts tx utxoSpend₀ utxoRefView)
454455
455456
-- TODO: implement the actual evolving `utxoRefView` (issue #1006)
456-
457-
getSubTxScripts : SubLevelTx → ℙ (TxId × ScriptHash)
458-
getSubTxScripts subtx = mapˢ (λ hash → (TxIdOf subtx , hash)) (ScriptHashes subtx)
459-
where
460-
ScriptHashes : Tx TxLevelSub → ℙ ScriptHash
461-
ScriptHashes tx = -- `txRequiredTopLevelGuards`
462-
mapPartial (isScriptObj ∘ proj₁) -- has key creds too, but only
463-
(TxBody.txRequiredTopLevelGuards (TxBodyOf tx)) -- `ScriptObj hash` contributes
464-
-- a phase-2 script hash.
465-
466-
getTxScripts : {ℓ : TxLevel} → Tx ℓ → ℙ (TxId × ScriptHash)
467-
getTxScripts {TxLevelSub} = getSubTxScripts
468-
getTxScripts {TxLevelTop} =
469-
concatMapˢ getSubTxScripts ∘ fromList ∘ TxBody.txSubTransactions ∘ TxBodyOf
470457
```
471458

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

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

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +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
44-
utxo₀ : UTxO
41+
slot : Slot
42+
pparams : PParams
43+
treasury : Treasury
44+
utxo₀ : UTxO
45+
isTopLevelValid : Bool
46+
globalRefInputsScripts : ℙ Script
47+
globalData : DataHash ⇀ Datum
4548
4649
record UTxOState : Type where
4750
field
@@ -61,7 +64,11 @@ instance
6164
HasUTxO-UTxOState .UTxOOf = UTxOState.utxo
6265
6366
unquoteDecl HasCast-UTxOEnv HasCast-UTxOState = derive-HasCast
64-
((quote UTxOEnv , HasCast-UTxOEnv ) ∷ (quote UTxOState , HasCast-UTxOState) ∷ [])
67+
( (quote UTxOEnv , HasCast-UTxOEnv ) ∷
68+
[ (quote UTxOState , HasCast-UTxOState) ])
69+
70+
HasUTxO-UTxOState : HasUTxO UTxOState
71+
HasUTxO-UTxOState .HasUTxO.UTxOOf = UTxOState.utxo
6572
```
6673
-->
6774

‎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)