Cardano Updates

Signed-off-by: Chris Gianelloni <[email protected]>

Signed-off-by: Roland Kuhn <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>

Signed-off-by: Chris Gianelloni <[email protected]>

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.

Guard scripts should be collected and executed with `ScriptPurpose =
Guard...` and receive txInfoSubTxs as txInfoForPurpose intends.

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

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

clean up and correct consumed/produced accounting

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

+ 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

+ clean up txInfoForPurpose
+ clean up and explain two utxo arguments
+ clean up txInfoForPurpose