Skip to content

[Dijkstra] batch-aware collectP2ScriptsWithContext #1015

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
williamdemeo merged 8 commits into from
Jan 13, 2026
Merged

[Dijkstra] batch-aware collectP2ScriptsWithContext #1015

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
0bd0262
Fix prose explaining CIP 118.
williamdemeo Dec 19, 2025
5e6773b
update CHANGELOG
williamdemeo Dec 19, 2025
cca73aa
add `TxInfo.txInfoSubTxs` field
williamdemeo Dec 21, 2025
176ac49
clean up txInfoForPurpose
williamdemeo Jan 9, 2026
97d3bad
[Dijkstra] Fix collectP2ScriptsWithContext: TxLevel-indexed txInfo + …
williamdemeo Dec 22, 2025
b655c74
improvements
williamdemeo Jan 9, 2026
d480c57
remove duplicates
williamdemeo Jan 9, 2026
ca47549
cleanup and explain two utxo arguments
williamdemeo Jan 13, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/Ledger/Dijkstra/Specification/Abstract.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ module Ledger.Dijkstra.Specification.Abstract (txs : TransactionStructure) where
open import Ledger.Prelude
open TransactionStructure txs
open import Ledger.Dijkstra.Specification.Certs govStructure
open import Ledger.Dijkstra.Specification.Script.ScriptPurpose txs


record indexOf : Type where
Expand All @@ -26,4 +27,5 @@ record AbstractFunctions : Type where
indexOfImp : indexOf
runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool
scriptSize : Script → ℕ
valContext : TxInfo → ScriptPurpose → Data
```
59 changes: 59 additions & 0 deletions src/Ledger/Dijkstra/Specification/Script/ScriptPurpose.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
---
source_branch: master
source_path: src/Ledger/Dijkstra/Specification/Script/ScriptPurpose.lagda.md
---

# Script Purpose {#sec:script-purpose}

<!--
```agda
{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Transaction

module Ledger.Dijkstra.Specification.Script.ScriptPurpose (txs : TransactionStructure) where

open import Ledger.Prelude
open TransactionStructure txs
open import Ledger.Dijkstra.Specification.Certs govStructure
```
-->

```agda
data ScriptPurpose : Type where
Cert : DCert → ScriptPurpose
Rwrd : RewardAddress → ScriptPurpose
Mint : ScriptHash → ScriptPurpose
Spend : TxIn → ScriptPurpose
Vote : GovVoter → ScriptPurpose
Propose : GovProposal → ScriptPurpose
Guard : Credential → ScriptPurpose
```

Note that `Guard c` always indexes into *the current `tx`'s* `txGuards`:

+ if `tx : TopLevelTx`, it indexes into the top-level guard set's list-view;
+ if `tx : SubLevelTx`, it indexes into the subTx's guard set's list-view.

```agda
mutual
record TxInfo : Type where
inductive
field
realizedInputs : UTxO
txOuts : Ix ⇀ TxOut
txFee : Maybe Fees
mint : Value
txCerts : List DCert
txWithdrawals : Withdrawals
txVldt : Maybe Slot × Maybe Slot
vkKey : ℙ KeyHash -- native/phase-1/timelock signers
txGuards : ℙ Credential -- CIP-0112/0118 guards (required by tx body)
txData : ℙ Datum
txId : TxId
txInfoSubTxs : Maybe (List SubTxInfo)

SubTxInfo : Type
SubTxInfo = TxInfo

```
112 changes: 38 additions & 74 deletions src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,24 +17,11 @@ module Ledger.Dijkstra.Specification.Script.Validation

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Certs govStructure
```
-->

```agda
data ScriptPurpose : Type where
Cert : DCert → ScriptPurpose
Rwrd : RewardAddress → ScriptPurpose
Mint : ScriptHash → ScriptPurpose
Spend : TxIn → ScriptPurpose
Vote : GovVoter → ScriptPurpose
Propose : GovProposal → ScriptPurpose
Guard : Credential → ScriptPurpose
open import Ledger.Dijkstra.Specification.Abstract txs
open import Ledger.Dijkstra.Specification.Script.ScriptPurpose txs
```

Note that `Guard c` always indexes into *the current `tx`'s* `txGuards`:

+ if `tx : TopLevelTx`, it indexes into the top-level guard set's list-view;
+ if `tx : SubLevelTx`, it indexes into the subTx's guard set's list-view.
-->

<!--
```agda
Expand All @@ -60,38 +47,17 @@ indexedRdmrs tx sp = maybe (λ x → lookupᵐ? txRedeemers x) nothing (rdptr tx

-- Datum lookup for spent outputs (Spend txin). Uses initial UTxO snapshot, utxoSpend₀.
getDatum : Tx ℓ → UTxO → ScriptPurpose → Maybe Datum
getDatum tx utxoSpend₀ (Spend txin) =
do (_ , _ , just d , _) ← lookupᵐ? utxoSpend₀ txin where
getDatum tx utxo₀ (Spend txin) =
do (_ , _ , just d , _) ← lookupᵐ? utxo₀ txin where
(_ , _ , nothing , _) → nothing
case d of λ where
(inj₁ d) → just d
(inj₂ h) → lookupᵐ? (setToMap (mapˢ < hash , id > (DataOf tx))) h
getDatum tx utxo _ = nothing
getDatum tx utxo₀ _ = nothing
```
-->

```agda
mutual
record TxInfo : Type where
inductive
field
realizedInputs : UTxO
txOuts : Ix ⇀ TxOut
txFee : Maybe Fees
mint : Value
txCerts : List DCert
txWithdrawals : Withdrawals
txVldt : Maybe Slot × Maybe Slot
vkKey : ℙ KeyHash -- native/phase-1/timelock signers
txGuards : ℙ Credential -- CIP-0112/0118 guards (required by tx body)
txData : ℙ Datum
txId : TxId
txInfoSubTxs : Maybe (List SubTxInfo)

SubTxInfo : Type
SubTxInfo = TxInfo


txInfo : (ℓ : TxLevel) → UTxO → Tx ℓ → TxInfo

txInfo TxLevelTop utxo tx =
Expand Down Expand Up @@ -145,15 +111,13 @@ txInfoForPurpose TxLevelTop utxo tx sp with sp
<!--
```agda
credsNeededMinusCollateral : {ℓ : TxLevel} → TxBody ℓ → ℙ (ScriptPurpose × Credential)
credsNeededMinusCollateral txb = a ∪ b ∪ c ∪ d ∪ e
where
a b c d e : ℙ (ScriptPurpose × Credential)
a = mapˢ (λ a → (Rwrd a , CredentialOf a)) (dom ∣ WithdrawalsOf txb ∣)
b = mapPartial (λ c → (Cert c ,_) <$> cwitness c) (fromList (DCertsOf txb))
c = mapˢ (λ x → (Mint x , ScriptObj x)) (policies (ValueOf txb))
d = mapPartial (λ v → if isGovVoterCredential v then (λ {c} → just (Vote v , c)) else nothing)
credsNeededMinusCollateral txb =
mapˢ (λ a → (Rwrd a , CredentialOf a)) (dom ∣ WithdrawalsOf txb ∣)
∪ mapPartial (λ c → (Cert c ,_) <$> cwitness c) (fromList (DCertsOf txb))
∪ mapˢ (λ x → (Mint x , ScriptObj x)) (policies (MintedValueOf txb))
∪ mapPartial (λ v → if isGovVoterCredential v then (λ {c} → just (Vote v , c)) else nothing)
(fromList (map GovVoterOf (GovVotesOf txb)))
e = mapPartial (λ p → if PolicyOf p then (λ {sh} → just (Propose p , ScriptObj sh)) else nothing)
∪ mapPartial (λ p → if PolicyOf p then (λ {sh} → just (Propose p , ScriptObj sh)) else nothing)
(fromList (GovProposalsOf txb))

credsNeeded : (ℓ : TxLevel) → UTxO → (TxBody ℓ) → ℙ (ScriptPurpose × Credential)
Expand All @@ -165,38 +129,38 @@ credsNeeded TxLevelSub utxo txb = credsNeededMinusCollateral txb
∪ mapˢ (λ (i , o) → (Spend i , payCred (proj₁ o))) ((utxo ∣ txIns) ˢ)
where open TxBody txb

--valContext : TxInfo → ScriptPurpose → Data
--valContext txinfo sp = toData (txinfo , sp)

txOutToDataHash : TxOut → Maybe DataHash
txOutToDataHash (_ , _ , d , _) = d >>= isInj₂

txOutToP2Script : UTxO → UTxO → (Tx ℓ) → TxOut → Maybe P2Script
txOutToP2Script utxoSpend₀ utxoRefView tx (a , _) =
txOutToP2Script utxo₀ utxoRefView tx (a , _) =
do sh ← isScriptObj (payCred a)
s ← lookupScriptHash sh tx utxoSpend₀ utxoRefView
s ← lookupScriptHash sh tx utxo₀ utxoRefView
toP2Script s
-- opaque
-- collectP2ScriptsWithContext
-- : PParams → (Tx ℓ) → UTxO
-- → List (P2Script × List Data × ExUnits × CostModel)
-- collectP2ScriptsWithContext pp tx utxo
-- = setToList
-- $ mapPartial (λ (sp , c) → if isScriptObj c
-- then (λ {sh} → toScriptInput sp sh)
-- else nothing)
-- $ credsNeeded utxo (TxBodyOf tx)
-- where
-- toScriptInput
-- : ScriptPurpose → ScriptHash
-- → Maybe (P2Script × List Data × ExUnits × CostModel)
-- toScriptInput sp sh =
-- do s ← lookupScriptHash sh tx utxo
-- p2s ← toP2Script s
-- (rdmr , exunits) ← indexedRdmrs tx sp
-- let data' = maybe [_] [] (getDatum tx utxo sp) ++ rdmr ∷ [ valContext (txInfo (language p2s) pp utxo tx) sp ]
-- costModel = PParams.costmdls pp
-- just (p2s , data' , exunits , costModel)

opaque
collectP2ScriptsWithContext
: {ℓ : TxLevel} → PParams → (Tx ℓ) → UTxO → UTxO
→ List (P2Script × List Data × ExUnits × CostModel)
collectP2ScriptsWithContext {ℓ} pp tx utxoSpend₀ utxoRefView
= setToList $ mapPartial ( λ (sp , c) → if isScriptObj c
then (λ {sh} → toScriptInput sp sh)
else nothing )
$ credsNeeded ℓ utxoSpend₀ (TxBodyOf tx)
-- use initial utxo snapshot ^^here^^ to inspect `txIns` (collateral spend side)
where
toScriptInput
: ScriptPurpose → ScriptHash
→ Maybe (P2Script × List Data × ExUnits × CostModel)
toScriptInput sp sh =
do s ← lookupScriptHash sh tx utxoSpend₀ utxoRefView
Copy link
Collaborator

@carlostome carlostome Jan 12, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not particularly happy about the namings utxoSpend₀ utxoRefView.
In utxoSpend₀ the subscript 0 suggests (to me) is a snapshot of the original utxo while the suffix RefView in utxoRefView suggest the same.
For simplicity I'd suggest keeping utxo for the utxo in the state and maybe utxo₀ for the snapshot before subtransactions are applied.

Copy link
Member Author

@williamdemeo williamdemeo Jan 12, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, that sounds good. The idea behind the current names is that the subscript 0 refers to the origin utxo, while RefView is the evolving one that the reference scripts see... but I'm fine with your proposed naming scheme, too.

Copy link
Member Author

@williamdemeo williamdemeo Jan 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll rename utxoSpend₀ → utxo₀ (pre-batch snapshot used for spending-input inspection + realizedInputs) and keep utxoRefView (ref-input lookup view, potentially evolving to include earlier-prefix outputs).

Copy link
Member Author

@williamdemeo williamdemeo Jan 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see an obvious way to avoid having two utxo arguments in the script functions defined near the bottom of the Transactions module. I agree it would be nicer if we could bind these utxos to a UTxOEnv and a UTxOState, but the functions are defined in the Transaction module and used in the Scripts.Validation module, before the UTxOEnv and UTxOState types are even defined.

p2s ← toP2Script s
(rdmr , exunits) ← indexedRdmrs tx sp
let data' = maybe [_] [] (getDatum tx utxoSpend₀ sp)
++ rdmr ∷ [ valContext (txInfoForPurpose ℓ utxoSpend₀ tx sp) sp ]
-- use initial utxo snapshot ^^here^^ so spending
-- inputs/realized inputs don't see prefix outputs
just (p2s , data' , exunits , PParams.costmdls pp)

evalP2Scripts : List (P2Script × List Data × ExUnits × CostModel) → Bool
evalP2Scripts = all (λ (s , d , eu , cm) → runPLCScript cm s eu d)
Expand Down
Loading