[Dijkstra] resolve ambiguity: visibility of reference inputs

[williamdemeo]

Description

Stacked PR. The branch for this PR should be rebased on master once PR #1012 is merged.

This PR closes issue #1005 by adopting the following interpretation and approach in the Dijkstra spec, resolving the apparent ambiguity in the CIP and matches the "preceding Tx outputs" intent:

1. Spending inputs (i.e., the ones that are actually consumed) must be present in the initial UTxO snapshot for the batch (the "mempool safety" constraint).

2. Reference inputs are allowed to refer to:

   • entries in the initial UTxO, or
   • outputs produced by earlier subTxs in the batch order (the "preceding transactions" carve-out).

3. Reference lookup uses an evolving (tentative) UTxO view, computed by applying prior subtransaction effects for lookup only (still no commitment to change state until the batch succeeds).

This makes the two CIP statements mentioned in Issue #1005 simultaneously true by reading "inputs" as "spending inputs," while still enabling the specific "ref scripts from preceding outputs" behavior the CIP explicitly mentions.

Moreover, we change type signatures where necessary to allow for the two UTxO views:

• utxoSpend₀, the initial (static) UTxO;
• utxoRefView, the evolving UTxO.

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 resolves the ambiguity in the Dijkstra specification (issue #1005) regarding the visibility of reference inputs in batch transactions. It establishes a clear distinction between spending inputs (which must exist in the initial UTxO snapshot) and reference inputs (which may additionally point to outputs from preceding sub-transactions in the batch).

Key changes:

• Introduce two UTxO views: utxoSpend₀ (initial snapshot) and utxoRefView (evolving view for reference lookups)
• Update transaction body structure to replace txRequiredGuards with txGuards and add reqSignerHashes field
• Extend TxInfo with txInfoSubTxs field and introduce purpose-specific txInfoForPurpose function
• Add minimal UTXO and UTXOW skeleton transition systems for Dijkstra phase-1 checks

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/Ledger/Dijkstra/Specification/Utxow.lagda.md	New skeleton wrapper around UTXO transition for witnessing layer
src/Ledger/Dijkstra/Specification/Utxo.lagda.md	New skeleton UTXO transition with phase-1 guard satisfaction check
src/Ledger/Dijkstra/Specification/Transaction.lagda.md	Major updates: dual UTxO views, renamed guard fields, updated function signatures, comprehensive validity documentation
src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md	Updated ScriptPurpose, TxInfo structure with guards/subTxs, dual UTxO parameters for script lookups
src/Ledger/Dijkstra/Specification/Abstract.lagda.md	Updated indexOfGuard signature to use Credential and List Credential
src/Ledger/Dijkstra/Specification.lagda.md	Added module imports for new Utxo and Utxow specifications
src/Ledger/Conway/Specification/Utxow.lagda.md	Fixed source_path metadata from .lagda to .lagda.md
src/Ledger/Conway/Specification/Utxo.lagda.md	Added missing metadata header
CHANGELOG.md	Documented all semantic changes to transaction structure and validation

---

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

[carlostome]

LGTM!