[Dijkstra] resolve ambiguity: visibility of reference inputs

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.