Cardano Updates

+  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₀.

+  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

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

+  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 <[email protected]>

---------

Co-authored-by: William DeMeo <[email protected]>
Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: williamdemeo <[email protected]>

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 <[email protected]>

+  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

+  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

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

* Refactor P2Scripts tests in Script.Validation

* Add a premise about txrdmrs to the UTXOW rule

+  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

clean up and correct consumed/produced accounting

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

clean up documnetation prose in Utxo module

+  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 <[email protected]>

---------

Co-authored-by: William DeMeo <[email protected]>
Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: williamdemeo <[email protected]>

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 <[email protected]>

+  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₀.

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

(This is the final/cleanup commit.)

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

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>