[Dijkstra] resolve ambiguity: visibility of reference inputs (#1014)

*  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

*  Adapt `txOutToP2Script` to two utxo views.

   Also highlight that `getDatum` gets the datum of the spent output (look up `txin` in the UTxO; if the output stores a datum hash, look it up in `DataOf tx`). It's a spending-input datum lookup (not a reference-input datum lookup).

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

*  Add preliminary check that txIns exist in the UTxO prior to any changes

---------

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

Author: 3 people

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

@@ -181,6 +181,7 @@ private variable
   enactState            : EnactState
   treasury              : Treasury
   isTopLevelValid       : Bool
+  utxo₀                 : UTxO
 ```
 -->
 
@@ -197,15 +198,15 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LState → SubLevelTx → LSt
 ```agda
     in
       ∙ isTopLevelValid ≡ true
-      ∙ ⟦ slot , pp , treasury ⟧  ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
+      ∙ ⟦ slot , pp , treasury , utxo₀ ⟧  ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState'
       ∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
       ∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury , isTopLevelValid ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState' , govState' , certState' ⟧
 
   SUBLEDGER-I :
       ∙ isTopLevelValid ≡ false
-      ∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
+      ∙ ⟦ slot , pp , treasury , utxo₀ ⟧ ⊢ utxoState ⇀⦇ stx ,SUBUTXOW⦈ utxoState
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury , isTopLevelValid ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState , govState , certState ⟧
 
@@ -237,7 +238,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState 
     in
       ∙ isValid tx ≡ true
       ∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions ,SUBLEDGERS⦈ ⟦ utxoState' , govState' , certState' ⟧
-      ∙ ⟦ slot , pp , treasury ⟧  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
+      ∙ ⟦ slot , pp , treasury , utxo₀ ⟧  ⊢ utxoState' ⇀⦇ tx ,UTXOW⦈ utxoState''
       ∙ ⟦ epoch slot , pp , txGovVotes , txWithdrawals , allColdCreds govState enactState ⟧ ⊢ certState' ⇀⦇ txCerts ,CERTS⦈ certState''
       ∙ ⟦ txId , epoch slot , pp , ppolicy , enactState , certState' , dom (RewardsOf certState) ⟧ ⊢ {- rmOrphanDRepVotes certState' -} govState ⇀⦇ txgov txb ,GOVS⦈ govState'
       ────────────────────────────────
@@ -255,7 +256,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState 
     in
       ∙ isValid tx ≡ false
       ∙ ⟦ slot , ppolicy , pp , enactState , treasury , isValid tx ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ txSubTransactions  ,SUBLEDGERS⦈ ⟦ utxoState , govState , certState ⟧
-      ∙ ⟦ slot , pp , treasury ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
+      ∙ ⟦ slot , pp , treasury , utxo₀ ⟧ ⊢ utxoState ⇀⦇ tx ,UTXOW⦈ utxoState'
       ────────────────────────────────
       ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState , govState , certState ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState' , govState , certState ⟧
 ```

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

@@ -58,9 +58,10 @@ indexedRdmrs : (Tx ℓ) → ScriptPurpose → Maybe (Redeemer × ExUnits)
 indexedRdmrs tx sp = maybe (λ x → lookupᵐ? txRedeemers x) nothing (rdptr tx sp)
   where open Tx tx; open TxWitnesses txWitnesses
 
+-- Datum lookup for spent outputs (Spend txin). Uses initial UTxO snapshot, utxoSpend₀.
 getDatum : Tx ℓ → UTxO → ScriptPurpose → Maybe Datum
-getDatum tx utxo (Spend txin) =
-  do (_ , _ , just d , _) ← lookupᵐ? utxo txin where
+getDatum tx utxoSpend₀ (Spend txin) =
+  do (_ , _ , just d , _) ← lookupᵐ? utxoSpend₀ txin where
                             (_ , _ , nothing , _) → nothing
      case d of λ where
        (inj₁ d) → just d
@@ -125,20 +126,19 @@ txInfo TxLevelSub utxo tx =
 
 txInfoForPurpose : (ℓ : TxLevel) → UTxO → Tx ℓ → ScriptPurpose → TxInfo
 
+-- subtransactions: never get subTx infos (even if the ScriptPurpose is Guard).
+txInfoForPurpose TxLevelSub utxo tx _ = txInfo TxLevelSub utxo tx
 
-txInfoForPurpose TxLevelSub utxo tx sp = txInfo TxLevelSub utxo tx
-  -- SubTx scripts never get subTx infos (even if their ScriptPurpose is Guard).
-
+-- top-level transactions:
 txInfoForPurpose TxLevelTop utxo tx sp with sp
--- Top-level scripts:
--- · guard scripts see subTx infos
+   -- · guard scripts see subTx infos
 ... | Guard _ =  record base { txInfoSubTxs = just subInfos }
                  where
                  base : TxInfo
                  base = txInfo TxLevelTop utxo tx
                  subInfos : List SubTxInfo
                  subInfos = map (txInfo TxLevelSub utxo) (SubTransactionsOf tx)
--- · other top-level scripts see no subTx infos
+   -- · other top-level scripts see no subTx infos
 ... | _ = txInfo TxLevelTop utxo tx
 ```
 
@@ -171,12 +171,10 @@ credsNeeded TxLevelSub utxo txb = credsNeededMinusCollateral txb
 txOutToDataHash : TxOut → Maybe DataHash
 txOutToDataHash (_ , _ , d , _) = d >>= isInj₂
 
-txOutToP2Script
-  : UTxO → (Tx ℓ)
-  → TxOut → Maybe P2Script
-txOutToP2Script utxo tx (a , _) =
+txOutToP2Script : UTxO → UTxO → (Tx ℓ) → TxOut → Maybe P2Script
+txOutToP2Script utxoSpend₀ utxoRefView tx (a , _) =
   do sh ← isScriptObj (payCred a)
-     s  ← lookupScriptHash sh tx utxo
+     s  ← lookupScriptHash sh tx utxoSpend₀ utxoRefView
      toP2Script s
 -- opaque
 --   collectP2ScriptsWithContext

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

@@ -60,7 +60,7 @@ can include required top-level guards (the `txRequiredTopLevelGuards`{.AgdaField
 
 To that end, we define two auxiliary functions that will aid in
 specifying which record fields of a transaction body are present at
-each `TxLevel`{.agdatype}:
+each `TxLevel`{.AgdaDatatype}:
 
 ```agda
 InTopLevel : TxLevel → Type → Type
@@ -73,7 +73,7 @@ InSubLevel TxLevelTop _ = ⊤
 ```
 
 These functions discriminate on an argument of type
-`TxLevel`{.agdatype} and either act as the identity function on types
+`TxLevel`{.AgdaDatatype} and either act as the identity function on types
 or as the constant function that returns the unit type.
 
 <!--
@@ -291,6 +291,14 @@ could be either of them.
     field TxIdOf    : A → TxId
   open HasTxId    ⦃...⦄ public
 
+  record HasSpendInputs {a} (A : Type a) : Type a where
+    field SpendInputsOf : A → ℙ TxIn
+  open HasSpendInputs ⦃...⦄ public
+
+  record HasReferenceInputs {a} (A : Type a) : Type a where
+    field ReferenceInputsOf : A → ℙ TxIn
+  open HasReferenceInputs ⦃...⦄ public
+
   record HasFees? {a} (A : Type a) : Type a where
     field FeesOf? : A → Maybe Fees
   open HasFees? ⦃...⦄ public
@@ -339,6 +347,18 @@ could be either of them.
     HasWithdrawals-Tx : HasWithdrawals (Tx txLevel)
     HasWithdrawals-Tx .WithdrawalsOf = WithdrawalsOf ∘ TxBodyOf
 
+    HasSpendInputs-TxBody : HasSpendInputs (TxBody txLevel)
+    HasSpendInputs-TxBody .SpendInputsOf = TxBody.txIns
+
+    HasSpendInputs-Tx : HasSpendInputs (Tx txLevel)
+    HasSpendInputs-Tx .SpendInputsOf = SpendInputsOf ∘ TxBodyOf
+
+    HasReferenceInputs-TxBody : HasReferenceInputs (TxBody txLevel)
+    HasReferenceInputs-TxBody .ReferenceInputsOf = TxBody.refInputs
+
+    HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
+    HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf
+
     HasValue-TxBody : HasValue (TxBody txLevel)
     HasValue-TxBody .ValueOf = TxBody.mint
 
@@ -403,23 +423,36 @@ This section collects some unimportant but useful helper and accessor functions.
 
   txinsScript : ℙ TxIn → UTxO → ℙ TxIn
   txinsScript txins utxo = txins ∩ dom (proj₁ (scriptOuts utxo))
+```
+
+In the Dijkstra era, *spending* inputs must exist in the initial UTxO snapshot, while
+*reference* inputs may see earlier outputs, so we need two UTxO views:
 
-  refScripts : Tx txLevel → UTxO → List Script
-  refScripts tx utxo =
-    mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) $ setToList (range (utxo ∣ (txIns ∪ refInputs)))
-    where open Tx; open TxBody (TxBodyOf tx)
++ `utxoSpend₀`{.AgdaBound}, the initial snapshot, used for `txIns`{.AgdaField},
++ `utxoRefView`{.AgdaBound}, the evolving view, used for `refInputs`{.AgdaField}.
 
-  txscripts : Tx txLevel → UTxO → ℙ Script
-  txscripts tx utxo = scripts (tx .txWitnesses) ∪ fromList (refScripts tx utxo)
+Thus functions like `refScripts`{.AgdaFunction}, `txscripts`{.AgdaFunction},
+and `lookupScriptHash`{.AgdaFunction} (defined below) will take *two* UTxO arguments.
+
+```agda
+  refScripts : Tx txLevel → UTxO → UTxO → List Script
+  refScripts tx utxoSpend₀ utxoRefView =
+    mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) ( setToList (range (utxoSpend₀ ∣ txIns))
+                                       ++ setToList (range (utxoRefView ∣ refInputs))
+                                     )
+    where open Tx tx; open TxBody (TxBodyOf tx)
+
+  txscripts : Tx txLevel → UTxO → UTxO → ℙ Script
+  txscripts tx utxoSpend₀ utxoRefView =
+    scripts (tx .txWitnesses) ∪ fromList (refScripts tx utxoSpend₀ utxoRefView)
     where open Tx; open TxWitnesses
 
-  lookupScriptHash : ScriptHash → Tx txLevel → UTxO → Maybe Script
-  lookupScriptHash sh tx utxo =
-    if sh ∈ mapˢ proj₁ (m ˢ) then
-      just (lookupᵐ m sh)
-    else
-      nothing
-    where m = setToMap (mapˢ < hash , id > (txscripts tx utxo))
+  lookupScriptHash : ScriptHash → Tx txLevel → UTxO → UTxO → Maybe Script
+  lookupScriptHash sh tx utxoSpend₀ utxoRefView =
+    if sh ∈ mapˢ proj₁ (m ˢ) then just (lookupᵐ m sh) else nothing
+    where m = setToMap (mapˢ < hash , id > (txscripts tx utxoSpend₀ utxoRefView))
+
+  -- TODO: implement the actual evolving `utxoRefView` (issue #1006)
 
   getSubTxScripts : SubLevelTx → ℙ (TxId × ScriptHash)
   getSubTxScripts subtx = mapˢ (λ hash → (TxIdOf subtx , hash)) (ScriptHashes subtx)
@@ -520,6 +553,14 @@ The Dijkstra era introduces *nested transactions* (a single top-level transactio
 that contains a list of sub-transactions) and *guards* (CIP-0112 / CIP-0118).  As a
 result, several checks that were "per-transaction" in Conway become *batch-aware*.
 
+**Design Note** (CIP-0118: spending inputs vs reference inputs).
+For Dijkstra batches, we distinguish *spending inputs* from *reference inputs*.
+All spending inputs across the whole batch must exist in the initial UTxO snapshot
+(mempool safety).  Reference inputs may additionally point to outputs of **preceding
+subtransactions in the batch order**.  Therefore reference-script/datum lookup is
+performed against an *evolving, tentative UTxO view* (prefix-applied), used only for
+lookup/validation, while *ledger state is committed only if the full batch succeeds*.
+
 ### Key points
 
 1.  **No further nesting**
@@ -537,17 +578,17 @@ result, several checks that were "per-transaction" in Conway become *batch-aware
 
 3.  **Batch-wide phase-2 evaluation**
 
-    Phase-2 (Plutus) validation is performed **once**
-    for the whole batch (mempool safety), even though script inputs/contexts are
-    constructed from both sub- and top-level components.
+    Phase-2 (Plutus) validation is performed *once* for the whole batch (mempool
+    safety), even though script inputs/contexts are constructed from both sub- and
+    top-level components.
 
 4.  **Guards are credentials**
 
     A transaction body may specify *guards* as a set of *credentials* (key or
     script).  This is distinct from the legacy "required signer" key hashes used for
     phase-1 key-witness checking and native/timelock scripts.
 
-5.  **Required top-level guards are requests (list-like)**
+5.  **Required top-level guards are requests**
 
     Sub-transaction bodies may include a list of "required top-level guard" requests
     (credential plus optional datum).  Ledger phase-1 checks must ensure that the
@@ -581,28 +622,6 @@ result, several checks that were "per-transaction" in Conway become *batch-aware
     referenced are defined by the UTxO rules.)
 
 
-<!--
-The following text previously appeared in item 4.
-
-> All scripts are shared across all transactions within a single batch, so
-> attaching one script to either a sub- or a top-level-transaction allows other
-> transactions to run it without also including it in its own scripts.  This
-> includes reference scripts that are sourced from the outputs to which reference
-> inputs point in the UTxO.  These referenced UTxO entries could be outputs of
-> preceding transactions in the batch.
-
-> Datums (from reference inputs and from other transactions) are also shared in
-> this way.  As before, only the datums fixed by the executing transaction are
-> included in the `TxInfo`{.AgdaRecord} constructed for its scripts, however, now
-> they don't necessarily have to be attached to that transaction.
-
-I've removed these two paragraphs for now because I'm not sure they're accurate.
-I've replaced them with an explanation that removes the 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," and punts the exact constraint to the UTxO rules
-(where I think it belongs).
--->
-
 [^1]:  See CIP 0118; once finalized and merged, CIP 0118 will appear in the
        main branch of [the CIP repository][CIPs]; until then, it can be found
        at <https://github.com/polinavino/CIPs/tree/polina/CIP0118/CIP-0118>.

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

@@ -41,6 +41,7 @@ record UTxOEnv : Type where
     slot      : Slot
     pparams   : PParams
     treasury  : Treasury
+    utxo₀     : UTxO
 
 record UTxOState : Type where
   field
@@ -53,9 +54,14 @@ record UTxOState : Type where
 <!--
 ```agda
 instance
+  HasUTxO-UTxOEnv : HasUTxO UTxOEnv
+  HasUTxO-UTxOEnv .UTxOOf = UTxOEnv.utxo₀
+
+  HasUTxO-UTxOState : HasUTxO UTxOState
+  HasUTxO-UTxOState .UTxOOf = UTxOState.utxo
+
   unquoteDecl HasCast-UTxOEnv HasCast-UTxOState = derive-HasCast
-    ( (quote UTxOEnv   , HasCast-UTxOEnv  ) ∷
-    [ (quote UTxOState , HasCast-UTxOState) ])
+    ((quote UTxOEnv , HasCast-UTxOEnv  ) ∷ (quote UTxOState , HasCast-UTxOState) ∷ [])
 ```
 -->
 
@@ -83,40 +89,40 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState
     Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s
 ```
 
-## UTXO
+## The <span class="AgdaDatatype">UTXO</span> Transition System {#sec:the-utxo-transition-system}
+
+### New in Dijkstra
 
-(skeleton with the new phase-1 check)
+1. The set of spending inputs must exist in the UTxO _before_ applying the
+transaction (or partially applying any part of it). TODO: Add link to CIP once its finalized.
 
-This is the intended home of Dijkstra "phase-1 structural checks."
 
 ```agda
 data _⊢_⇀⦇_,SUBUTXO⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where
 
   SUBUTXO :
-    let txb    = Tx.txBody tx
-        subTxs = TxBody.txSubTransactions txb
-    in
+
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'
 
 data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
 
   UTXO :
-    let txb    = Tx.txBody tx
-        subTxs = TxBody.txSubTransactions txb
-    in
-    ∙ requiredTopLevelGuardsSatisfied tx subTxs
+
+    ∙ SpendInputsOf tx ≢ ∅
+    ∙ SpendInputsOf tx ⊆ dom (UTxOOf Γ)                           -- (1)
+    ∙ ReferenceInputsOf tx ⊆ dom (UTxOOf s)
+    ∙ requiredTopLevelGuardsSatisfied tx (SubTransactionsOf tx)   -- (2)
     ∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
 ```
 
-**Note.** The premise `requiredTopLevelGuardsSatisfied tx subTxs`
-is explicitly a **phase-1** condition (CIP-0118): every guard credential requested by
-subTx bodies must appear in the top-level `txGuards` set.
+**Notes**.
 
-A couple of details to notice:
+1.  The set of spending inputs must exist in the UTxO *before* applying the
+    transaction (or partially applying any part of it).
 
-- `txb` is computed via `Tx.txBody tx` (no reliance on `TxBodyOf` instances).
-- `UTXOS-stub` returns the **same** state (so we can typecheck
-  everything without inventing semantics prematurely).
+2.  The premise `requiredTopLevelGuardsSatisfied tx subTxs` is explicitly a
+    phase-1 condition (CIP-0118): every guard credential requested by subtransaction
+    bodies must appear in the top-level `txGuards` set.