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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

williamdemeo merged 8 commits into master from 1005-dijkstra-cip-0118-ambiguity-visibility-of-reference-inputs

Jan 12, 2026

+101 −77

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

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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

-Original file line number
+Diff line change
@@ Expand Up @@
     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
@@ Expand All / @@ -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.
     <!--
@@ Expand Down Expand Up / @@ -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
@@ Expand Down Expand Up / @@ -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
@@ Expand Down Expand Up @@
       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)
@@ Expand Down Expand Up @@
     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
 .  **No further nesting**
@@ Expand All @@
 .  **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.
 .  **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.
-.  **Required top-level guards are requests (list-like)**
+.  **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
@@ Expand Down Expand Up @@
         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

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!