[Dijkstra] UTXOS and UTXO Rules by williamdemeo · Pull Request #1021 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-01-08T05:04:46Z

Description

Plan (tentative)

This PR will close issue #1007 by

introducing batch helpers in Ledger/Dijkstra/Specification/Utxo.lagda.md:
- batch collection/verification (getSubTxScripts, batchP2Inputs, batchScriptsOk)
introduce level-parameterized versions of produced and consumed
making UTXOS a 2-branch relation: success vs failure

What we want UTXOS to decide:
- ok = batchScriptsOk txTop
- flag = Tx.isValid txTop (top-level only)
Then:
- require flag ≡ ok (so the transaction's claimed validity matches the ledger's batch execution result)
- branch on ok
- Success branch (commit)
  
  In the success constructor:
  - apply the normal batch effects (UTxO update, fees accounting, deposits/gov/etc)
  - enforce batch POV using level-parameterized produced/consumed (sums across txTop and all subTxs)
  - enforce fee rule: only top-level fee counts (already true by shape; still make it explicit in the accounting)
- Failure branch (collateral + nothing else)
  
  In the failure constructor:
  - Apply only collateral collection using CollateralInputsOf txTop
  - Don't apply any other UTxO changes from the batch (no outputs, no withdrawals, no cert effects, etc.)
  - Update fees by collateral amount (Q: how does ledger collect collateral? Does it go to fees? treasury?)

Notes

I needed the 2-UTxO parameterization (utxoSpend₀ vs utxoRefView) in some places, but
utxoRefView is still just a place holder until we start tracking sub-level change of utxo state. TODO: address this once #1005 is finalized.

Copilot-generated Description

This pull request introduces significant enhancements and refactoring to the Dijkstra ledger specification, focusing on fee calculation, transaction structure, script/data handling, and guard credential support. The changes improve modularity, clarify batch and mempool semantics, and generalize script/data management for the Dijkstra era.

Fee Calculation Refactoring and Generalization

Added a new src/Ledger/Dijkstra/Specification/Fees.lagda.md module, mirroring the Conway fee calculation but parameterized over protocol parameters and script structures for flexibility. The scriptsCost function now directly takes protocol parameters and script size, improving clarity and generality. [1] [2] [3]
Updated imports and usage of scriptsCost in both Conway and Dijkstra modules to match the new parameterization. [1] [2]

Transaction Structure and Guard Credential Support

Extended the transaction type to include a txSize field and clarified the semantics of txGuards and txRequiredTopLevelGuards, supporting both keys and scripts as guards for top-level and subtransactions. [1] [2] [3] [4]
Added a HasSize-Tx instance for transactions.

Script and Data Handling Refactor

Refactored script/data lookup and collection functions to operate over unified sets of scripts and data, removing the separation of P1/P2 scripts in favor of a single Script type. [1] [2] [3] [4]
Rewrote helper functions for extracting scripts and data from transactions and UTxOs, clarifying batch vs. mempool views, and improving composability.

Script Validation and Guards

Updated script validation logic to account for guard credentials, ensuring guards are included in the credential set needed for script execution and validation.
Refactored collectP2ScriptsWithContext and related functions to use extra data pools and unified script sets, ensuring correct precedence and context for script validation. [1] [2] [3]

Documentation and Minor Improvements

Improved documentation and comments throughout, clarifying the rationale behind changes and batch/mempool distinctions. [1] [2]

These changes collectively modernize the Dijkstra ledger specification, making it more modular, extensible, and aligned with recent protocol improvements.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

Copilot

Pull request overview

This PR implements batch-level validity checking for the UTXOS rule in the Dijkstra specification, addressing issues #1006 and #1007. It introduces a two-branch UTXOS relation that handles both successful script execution (applying all batch effects) and failed execution (collecting only collateral).

Key changes include:

Introduction of batch-level script validation with batchScriptsOk and preservation of value checking via batchPOV
Two-branch UTXOS rule with success/failure paths based on script execution results
Refactoring of the Fees module to be parameterized by protocol parameters

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 7 comments.

Show a summary per file

File	Description
`src/Ledger/Dijkstra/Specification/Utxo.lagda.md`	Implements batch-level UTXOS rule with success/failure branches, batch operations, and UTxO state transitions
`src/Ledger/Dijkstra/Specification/Transaction.lagda.md`	Adds level-dependent and level-independent type classes for transaction components, adds `txSize` field to `Tx`
`src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md`	Updates references from `ValueOf` to `MintedValueOf` for consistency
`src/Ledger/Conway/Specification/Fees.lagda.md`	Refactors module to take protocol parameters as module parameter; changes `scriptsCost` signature from `PParams → ℕ → Coin` to `ℕ → Coin`
`src/Ledger/Conway/Specification/Utxo.lagda.md`	Updates import statement for `scriptsCost` (but not all call sites)
`src/Ledger/Conway/Conformance/Utxo.agda`	Updates import statement for `scriptsCost` (but not all call sites)

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

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

src/Ledger/Conway/Specification/Utxo.lagda.md

src/Ledger/Conway/Conformance/Utxo.agda

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

Copilot · 2026-01-09T04:02:00Z

@williamdemeo I've opened a new pull request, #1023, to work on those changes. Once the pull request is ready, I'll request review from you.

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

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

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

carlostome · 2026-01-27T12:07:16Z

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

+                              ∪ txOutData tx
+
+  getAllScripts : TopLevelTx → UTxO → UTxO → ℙ Script
+  getAllScripts txTop utxo₀ utxoₙ =


I don't think both views are needed here (since CIP-0172) is likely to be accepted.

carlostome · 2026-01-27T12:07:30Z

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

+                 (fromList (SubTransactionsOf txTop))
+
+  getAllData : TopLevelTx → UTxO → UTxO → ℙ Datum
+  getAllData txTop utxo₀ utxoₙ =


Same as previous comment.

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

carlostome · 2026-01-27T12:10:05Z

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

+subtransaction originally supplied it.  The intent is that the ledger rules can validate
+all scripts in the a without recomputing per-subtransaction script/data availability.


I don't understand the last phrase.

carlostome · 2026-01-27T12:30:06Z

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

+    ∙ minfee pp utxo txTop ≤ TxFeesOf txTop
+    ∙ consumed Γ ≡ produced
+    ∙ SizeOf txTop ≤ maxTxSize pp
+    -- ∙ refScriptsSize utxo tx ≤ pp .maxRefScriptSizePerTx     -- TODO: Dijkstra analog


This will probably have to be checked at the top-level against those scripts coming from reference inputs outside of the batch. I added an issue about this (we can do it in a separate PR)

carlostome

LGTM!

…Txs` + Remove contradiction between "ref inputs may refer to earlier tx outputs in the batch" vs "all inputs must exist before applying any tx in the batch." The new text punts the exact constraint to the UTxO rules (where it belongs). + Fix Plutus bullet (old "nor earlier versions" reads like "no Plutus at all"). + Align fees with current Agda (`txFee : InTopLevel …`), but leave room for later CIP-driven updates. + Introduce subTx info type (using an alias for `TxInfo` for now). + Extend `TxInfo` with field `txInfoSubTxs : Maybe (List SubTxInfo)`. + Define a purpose-built builder: + Top-level Guard scripts ⇒ `txInfoSubTxs = just (...)` + Everything else ⇒ `txInfoSubTxs = nothing` + SubTx scripts ⇒ always `nothing` (even for `Guard` at sub level) + Explain two utxo arguments + Clean up txInfoForPurpose

+ Add batch-level coin mint constraint to prevent Ada forgery (#1023) + Initial plan and improvements + Add batchMintedCoin constraint to prevent Ada forgery + Add documentation for batchMintedCoin security constraint + Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> --------- Co-authored-by: William DeMeo <williamdemeo@gmail.com> Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: williamdemeo <3528228+williamdemeo@users.noreply.github.com> remove duplicate typeclass instance address PR change requests fix UTXOS and UTXO rules Update src/Ledger/Dijkstra/Specification/Utxo.lagda.md Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

clean up and correct consumed/produced accounting

+ fix collectP2ScriptsWithContext + Fix some bugs in Dijkstra Transaction module. + `TxOut` is 4-tuple: `(Addr × Value × Maybe (Datum ⊎ DataHash) × Maybe Script)` + `UTxO.balance` uses `txOutHash`, so if that's malformed, `balance` and minfee-related code will silently go wrong or fail to typecheck. + The doc note "reference inputs may come from earlier outputs (prefix-applied)" is outdated; ∵ Carlos' CIP, we want an order-independent `utxoView`. + Fix bugs in Utxo module + `collectP2ScriptsWithContext` now sees batch-shared scripts (witness inputs + ref inputs + outputs across all transactions in the batch). + datum-by-hash lookup (`getDatum ... (inj₂ h)`) now has an `extraData` pool containing everything in the batch view, hashed into a map, plus `Γ.globalData`. + no cyclic dependency: `Utxo` computes the batch wiring; `Script.Validation` remains generic. + Clean up Utxo module, removing redundancies + `Γ.globalScripts` is already batch-scoped via `getAllScripts tx utxo₀` (top + subs). + `Γ.globalData` is already batch-scoped via `getAllData tx utxo₀` (top + subs) and then hashed into a map. + `collectP2ScriptsWithContext` (still) unions `txDataMap tx` with `extraData` (so tx-local witness data take precedence).

+ changed globalScripts type; fixed Transaction docs + revise doc prose in Utxo module + rebase fixes + rewrite premises of UTXO rule + **No overlapping spends across subtransactions and top-level tx**: add explicit pairwise-disjointness premise for batch spending inputs. + **Reference-script/self-usable-output concern**: move reference-input validation to batch output view so reference inputs may point to outputs from full batch (including its own outputs), while keeping spending inputs mempool-safe against utxo₀.

+ Guard scripts should be collected and executed with `ScriptPurpose = Guard...` and receive txInfoSubTxs as txInfoForPurpose intends. + Fix utxo (snapshot vs batch) view semantics Previously allScripts` and `allData` could not "see" scripts/datums that are only available via reference inputs that point into batch outputs, because referenceOut utxo₀ tx would miss those outputs. At the same time, we don't want to accidentally make spend-side lookups consult a larger view than utxo₀. To fix this, we now split the UTxO used for spend-side vs reference-side extraction, and compute globalScripts/globalData using: + spend-side view = utxo₀ (mempool-safety) + reference-side view = utxoView = utxo₀ ∪ˡ batchOuts txTop to resolve reference inputs to batch outputs (and to get order-agnostic script sharing if we want it) + spendOut and thus spendScripts/spendData are forced to consult utxo₀. So even if utxoₙ contains batch outputs, spend-side extraction doesn't silently "prefer" batch outputs. + Reference scripts/datums that are only available on batch outputs can now be resolved when reference inputs point to them because referenceOut sees utxoRefView. + improve ergonomics + clean up documentation + add more UTXO premises

Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

clean up documnetation prose in Utxo module

Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

(This is the final/cleanup commit.)

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from 1814828 to b6f0a59 Compare January 8, 2026 05:27

williamdemeo self-assigned this Jan 8, 2026

williamdemeo added the era: dijkstra label Jan 8, 2026

williamdemeo added this to Dijkstra formal spec Jan 8, 2026

williamdemeo added the nested transactions label Jan 8, 2026

williamdemeo changed the title ~~Add support for batch-level validity checking~~ [Dijkstra] UTXOS Rule with batch-level validity checking Jan 8, 2026

williamdemeo moved this to In Progress in Dijkstra formal spec Jan 8, 2026

williamdemeo marked this pull request as ready for review January 8, 2026 06:51

williamdemeo requested a review from Copilot January 8, 2026 06:51

Copilot started reviewing on behalf of williamdemeo January 8, 2026 06:51 View session

Copilot AI reviewed Jan 8, 2026

View reviewed changes

williamdemeo force-pushed the 1006-dijkstra-batch-aware-collectp2scriptswithcontext branch from 4a690a6 to 2890db5 Compare January 9, 2026 03:06

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from 4e0a472 to b796416 Compare January 9, 2026 03:33

Copilot AI mentioned this pull request Jan 9, 2026

Add batch-level coin mint constraint to prevent Ada forgery #1023

Merged

williamdemeo force-pushed the 1006-dijkstra-batch-aware-collectp2scriptswithcontext branch from b0da3a6 to a60af70 Compare January 9, 2026 05:52

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from e43ee89 to 4f543af Compare January 9, 2026 05:54

williamdemeo marked this pull request as draft January 9, 2026 06:20

williamdemeo force-pushed the 1006-dijkstra-batch-aware-collectp2scriptswithcontext branch from a60af70 to e5e912f Compare January 9, 2026 15:01

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from 03fc211 to 9c88f5c Compare January 9, 2026 15:03

williamdemeo force-pushed the 1006-dijkstra-batch-aware-collectp2scriptswithcontext branch from e5e912f to 1f7ea3b Compare January 9, 2026 15:05

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from 9c88f5c to 975c125 Compare January 9, 2026 15:05

williamdemeo removed this from Dijkstra formal spec Jan 9, 2026

williamdemeo force-pushed the 1006-dijkstra-batch-aware-collectp2scriptswithcontext branch from 1f7ea3b to 4c2836d Compare January 10, 2026 00:14

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from 975c125 to c181b8e Compare January 10, 2026 00:14

williamdemeo force-pushed the 1006-dijkstra-batch-aware-collectp2scriptswithcontext branch from 4c2836d to d480c57 Compare January 12, 2026 16:31

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from 227116d to 14efc44 Compare January 12, 2026 17:00

williamdemeo mentioned this pull request Jan 13, 2026

[Dijkstra] batch-aware collectP2ScriptsWithContext #1015

Merged

4 tasks

williamdemeo force-pushed the 1006-dijkstra-batch-aware-collectp2scriptswithcontext branch from bff46ee to ca47549 Compare January 13, 2026 05:47

Base automatically changed from 1006-dijkstra-batch-aware-collectp2scriptswithcontext to master January 13, 2026 05:55

williamdemeo requested a review from carlostome January 23, 2026 05:20

williamdemeo changed the title ~~[Dijkstra] WIP - UTXOS Rule with batch-level validity checking~~ [Dijkstra] UTXO and UTXO Rules Jan 23, 2026

williamdemeo changed the title ~~[Dijkstra] UTXO and UTXO Rules~~ [Dijkstra] UTXOS and UTXO Rules Jan 23, 2026

carlostome reviewed Jan 23, 2026

View reviewed changes

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch 2 times, most recently from 7ce5bef to ccf6e71 Compare January 24, 2026 18:16

carlostome reviewed Jan 26, 2026

View reviewed changes

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from f92c3bb to 9674590 Compare January 27, 2026 04:47

williamdemeo requested a review from carlostome January 27, 2026 04:48

carlostome reviewed Jan 27, 2026

View reviewed changes

carlostome approved these changes Jan 27, 2026

View reviewed changes

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from 5b375dd to affba86 Compare January 28, 2026 04:36

williamdemeo and others added 13 commits January 27, 2026 21:51

Address PR review comments.

9d78ad2

clean up and correct consumed/produced accounting

fix accidental deletion during rebase

186e83a

Apply suggestions from code review

b96f3be

Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

add remaining premises of Dijkstra UTXO rule

73f7be7

clean up documnetation prose in Utxo module

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

f889ba3

Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

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

1ba2168

Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

simplify (and demodularize) Phase-2 module

40044e4

[Dijkstra] UTXOS and UTXO rules

07e3894

(This is the final/cleanup commit.)

williamdemeo force-pushed the 1007-dijkstra-utxos-batch-level-validity branch from affba86 to 07e3894 Compare January 28, 2026 04:51

williamdemeo merged commit 338cc3c into master Jan 28, 2026
2 of 3 checks passed

williamdemeo deleted the 1007-dijkstra-utxos-batch-level-validity branch January 28, 2026 05:09

carlostome mentioned this pull request Jan 29, 2026

[Dijkstra] Phase-1 transaction-wise validation checks #1017

Closed

1 task

williamdemeo mentioned this pull request Feb 4, 2026

[Dijkstra] collectP2ScriptsWithContext pass as argument the set of all scripts #1034

Closed

		subtransaction originally supplied it. The intent is that the ledger rules can validate
		all scripts in the a without recomputing per-subtransaction script/data availability.

Conversation

williamdemeo commented Jan 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Plan (tentative)

Notes

Copilot-generated Description

Checklist

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI commented Jan 9, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carlostome Jan 27, 2026

Choose a reason for hiding this comment

Uh oh!

carlostome Jan 27, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

carlostome Jan 27, 2026

Choose a reason for hiding this comment

Uh oh!

williamdemeo Jan 28, 2026

Choose a reason for hiding this comment

Uh oh!

carlostome Jan 27, 2026

Choose a reason for hiding this comment

Uh oh!

carlostome left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

williamdemeo commented Jan 8, 2026 •

edited

Loading