[Dijkstra] Make ScriptPurpose.Guard and IndexOfGuard carry a Credential (#1011)

* Add helpers for grouping top-level guard requests

* Fix prose explaining CIP 118.

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

* update CHANGELOG

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

Co-authored-by: Copilot <[email protected]>

* change txRequiredTopLevelGuards type from list to set

   agreeing with Carlos' observation/suggestion

* changed nomenclature

   Agreeing with Carlos' suggestion to avoid "request."

* convert code comments to (literate) documentation

* Add `requiredTopLevelGuardsSatisfied` predicate.

* Add initial versions of Utxo and Utxow modules

   + a minimal `UTXOS` rule as a stub/hook (so `UTXO` can call something),
   + a minimal `UTXO` rule with just the new phase-1 premise (plus an explicit "calls UTXOS"),
   + a minimal `UTXOW`; just a wrapper over `UTXO` for now.

* Make `ScriptPurpose.Guard` carry a `Credential`

   Key idea:

   +  Keep `txGuards` as a set **for now**.
   +  Define an ordered view `guardsList : List Credential` via `setToList`.
   +  Make `indexOfGuard` operate on that list.
   +  Let `rdptr` compute the `Ix` using `indexOfGuard`.

   For the "required top-level guards requested by subTxs" (i.e., `txRequiredTopLevelGuards` requests), we don't need a new ScriptPurpose constructor yet, because:

   +  phase-1 ensures those requested credentials are contained in top-level `txGuards`
   +  the later work (#1004 / #1006) will decide how to construct TxInfo / datum arguments for running those guard scripts batch-wide

---------

Co-authored-by: Copilot <[email protected]>

Author: williamdemeo

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

@@ -12,13 +12,13 @@ open import Ledger.Dijkstra.Specification.Certs govStructure
 
 record indexOf : Type where
   field
-    indexOfDCert          : DCert              → List DCert             → Maybe Ix
-    indexOfRewardAddress  : RewardAddress      → Withdrawals            → Maybe Ix
-    indexOfTxIn           : TxIn               → ℙ TxIn                 → Maybe Ix
-    indexOfPolicyId       : ScriptHash         → ℙ ScriptHash           → Maybe Ix
-    indexOfVote           : GovVoter           → List GovVoter          → Maybe Ix
-    indexOfProposal       : GovProposal        → List GovProposal       → Maybe Ix
-    indexOfGuard          : TxId × ScriptHash  → ℙ (TxId × ScriptHash)  → Maybe Ix
+    indexOfDCert          : DCert          → List DCert        → Maybe Ix
+    indexOfRewardAddress  : RewardAddress  → Withdrawals       → Maybe Ix
+    indexOfTxIn           : TxIn           → ℙ TxIn            → Maybe Ix
+    indexOfPolicyId       : ScriptHash     → ℙ ScriptHash      → Maybe Ix
+    indexOfVote           : GovVoter       → List GovVoter     → Maybe Ix
+    indexOfProposal       : GovProposal    → List GovProposal  → Maybe Ix
+    indexOfGuard          : Credential     → List Credential   → Maybe Ix
 
 record AbstractFunctions : Type where
   field txScriptFee     : Prices → ExUnits → Fees

src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md

@@ -22,30 +22,36 @@ open import Ledger.Dijkstra.Specification.Certs govStructure
 
 ```agda
 data ScriptPurpose : Type where
-  Cert     : DCert               → ScriptPurpose
-  Rwrd     : RewardAddress       → ScriptPurpose
-  Mint     : ScriptHash          → ScriptPurpose
-  Spend    : TxIn                → ScriptPurpose
-  Vote     : GovVoter            → ScriptPurpose
-  Propose  : GovProposal         → ScriptPurpose
-  Guard    : (TxId × ScriptHash) → ScriptPurpose
+  Cert     : DCert          → ScriptPurpose
+  Rwrd     : RewardAddress  → ScriptPurpose
+  Mint     : ScriptHash     → ScriptPurpose
+  Spend    : TxIn           → ScriptPurpose
+  Vote     : GovVoter       → ScriptPurpose
+  Propose  : GovProposal    → ScriptPurpose
+  Guard    : Credential     → ScriptPurpose
 ```
 
+Note that `Guard c` always indexes into *the current `tx`'s* `txGuards`:
+
++  if `tx : TopLevelTx`, it indexes into the top-level guard set's list-view;
++  if `tx : SubLevelTx`, it indexes into the subTx's guard set's list-view.
+
 <!--
 ```agda
 private variable
   ℓ : TxLevel
 
 rdptr : (Tx ℓ) → ScriptPurpose → Maybe (RedeemerPtr ℓ)
 rdptr tx = λ where
-  (Cert h)              → map (Cert    ,_) $ indexOfDCert          h txCerts
-  (Rwrd h)              → map (Reward  ,_) $ indexOfRewardAddress  h txWithdrawals
-  (Mint h)              → map (Mint    ,_) $ indexOfPolicyId       h (policies mint)
-  (Spend h)             → map (Spend   ,_) $ indexOfTxIn           h txIns
-  (Vote h)              → map (Vote    ,_) $ indexOfVote           h (map GovVote.voter txGovVotes)
-  (Propose h)           → map (Propose ,_) $ indexOfProposal       h txGovProposals
-  (Guard h)             → map (Guard   ,_) $ indexOfGuard          h (getTxScripts tx)
- where open TxBody (TxBodyOf tx)
+  (Cert h)     → map (Cert     ,_) $ indexOfDCert          h txCerts
+  (Rwrd h)     → map (Reward   ,_) $ indexOfRewardAddress  h txWithdrawals
+  (Mint h)     → map (Mint     ,_) $ indexOfPolicyId       h (policies mint)
+  (Spend h)    → map (Spend    ,_) $ indexOfTxIn           h txIns
+  (Vote h)     → map (Vote     ,_) $ indexOfVote           h (map GovVote.voter txGovVotes)
+  (Propose h)  → map (Propose  ,_) $ indexOfProposal       h txGovProposals
+  (Guard c)    → map (Guard    ,_) $ indexOfGuard          c (setToList txGuards)
+    where open TxBody (TxBodyOf tx)
+
 -- getSubTxScripts : TopLevelTx → ℙ (TxId × ScriptHash)
 
 indexedRdmrs : (Tx ℓ) → ScriptPurpose → Maybe (Redeemer × ExUnits)