[Dijkstra] batch-aware collectP2ScriptsWithContext

[williamdemeo]

Description

Stacked PR. (This PR should be rebased on and target master if PR #1014 is merged first.)

This PR closes issue #1006 by starting the Dijkstra-era refactor needed for batch-wide phase-2 evaluation.

This PR handles the collector refactor; the single call site is implemented in PR #1021.

Key change: collectP2ScriptsWithContext now takes two UTxO views:

• utxo₀ = the snapshot UTxO "before any of the batch transactions are applied" (this is explicitly a CIP-0118 requirement).
• utxoRef = the view used for reference-input lookup, which is allowed to include outputs from earlier subtransactions in the batch (also explicitly CIP-0118).

It also fixes context construction to use Dijkstra's TxLevel-indexed txInfo via txInfoForPurpose, rather than Conway's txInfo (language p2s) ... pattern.

Motivation

Dijkstra batches need to:

• build script inputs/contexts across subTxs + top-level,
• run a single batch-wide phase-2 evaluation at UTXOS,
• keep spending inputs pinned to the initial UTxO snapshot (mempool safety),
• allow reference lookup to use an evolving prefix-applied view (see design note in PR [Dijkstra] resolve ambiguity: visibility of reference inputs #1014).

This PR is an incremental step: it makes P2 collection ready to be called per-subTx with the correct UTxO parameters.

Changes

• Add {ℓ : TxLevel} and (utxo₀ utxoRef : UTxO) arguments to collectP2ScriptsWithContext.
• Use credsNeeded ℓ utxo₀ ... so spend-side input inspection remains snapshot-based.
• Thread both views through lookupScriptHash and txOutToP2Script.
• Build validation context using txInfoForPurpose ℓ utxo₀ tx sp (TxLevel-indexed).

Follow-ups (next commits / next PR)

• Define the batch-level collector that computes utxoRef per subTx prefix.
• Move to exactly one batch-wide evalP2Scripts call site at UTXOS.
• Specify failure behavior: no batch effects applied; collateral collected (top-level only).

---

Copilot-generated Description

This pull request introduces significant refactoring and abstraction improvements to the Dijkstra specification, focusing on transaction structure, script validation, and the handling of scripts and guards. The changes add new type classes for modular access to transaction components, refactor script and UTxO handling for clarity and extensibility, and move or abstract several definitions to improve code organization. These updates lay the groundwork for more robust, maintainable, and extensible formalizations of transaction and script validation logic.

Major abstraction and type class improvements:

• Introduced a suite of new type classes (e.g., HasTxBody, HasTxWitnesses, HasRedeemers, HasCollateralInputs, HasTxFees, HasSubTransactions, HasTopLevelGuards, HasIndexedOutputs, HasMintedValue, HasGuards, HasScripts) to provide modular, level-dependent and level-independent accessors for transaction components, replacing direct record field access throughout the codebase. [1] [2] [3] [4] [5] [6] [7]

• Added corresponding type class instances for Tx, TxBody, and TxWitnesses, ensuring seamless and consistent access to transaction data at both top-level and sub-level contexts. [1] [2] [3] [4]

Script and UTxO handling refactor:

• Refactored script and UTxO handling functions (e.g., refScripts, txscripts, lookupScriptHash, getSubTxScripts, getTxScripts) to use the new type classes and clarified the distinction between initial and evolving UTxO snapshots (utxo₀ and utxoRef), improving readability and correctness.

• Updated documentation and function signatures to reflect the new UTxO handling conventions and to clarify the use of two UTxO arguments for reference and spending inputs.

Script validation and context improvements:

• Moved the definition of ScriptPurpose and TxInfo to a new module (ScriptPurpose.lagda.md), and updated imports accordingly, centralizing script purpose logic. [1] [2] [3]

• Added the valContext function to the AbstractFunctions record, and used it in script validation to provide context data to scripts, improving the expressiveness and correctness of script evaluation. [1] [2]

Correctness and consistency fixes:

• Updated the credsNeededMinusCollateral function to use the new MintedValueOf accessor instead of the removed ValueOf, ensuring correct calculation of credentials needed for minting.

• Standardized variable naming and usage (e.g., utxo₀, utxoRef) across script validation and helper functions for consistency. [1] [2] [3] [4]

Guard and credential handling improvements:

• Refactored functions related to guard credentials and top-level guard satisfaction to use the new GuardsOf and TopLevelGuardsOf accessors, streamlining the logic for CIP-0118 compliance.

---

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 refactors the Dijkstra-era script validation infrastructure to support batch-wide phase-2 evaluation. The key change is making collectP2ScriptsWithContext batch-aware by introducing dual UTxO views: one for spending input inspection (pinned to the initial snapshot) and one for reference script/datum lookup (which will eventually use an evolving view).

• Introduced separate ScriptPurpose.lagda.md module to house ScriptPurpose, TxInfo, and SubTxInfo types
• Added txInfoForPurpose function that conditionally includes sub-transaction context for guard scripts at the top level
• Updated collectP2ScriptsWithContext to accept two UTxO parameters and thread them appropriately through script lookup and context construction

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
src/Ledger/Dijkstra/Specification/Script/ScriptPurpose.lagda.md	New module defining ScriptPurpose data type and TxInfo record with txInfoSubTxs field for guard scripts
src/Ledger/Dijkstra/Specification/Abstract.lagda.md	Imports ScriptPurpose module and adds valContext function to AbstractFunctions interface
src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md	Removes inline type definitions (moved to ScriptPurpose), updates collectP2ScriptsWithContext to use dual UTxO views, adds txInfoForPurpose for purpose-specific context construction

---

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

[carlostome]

LGTM with a minor comment (TB discussed)

[carlostome]

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.

[williamdemeo]

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.

[williamdemeo]

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

[williamdemeo]

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.