UTxO

(Dijkstra skeleton)

This is a minimal skeleton of the Dijkstra-era UTxO transition system.

It exists primarily to host phase-1 structural checks that are specific to Dijkstra (CIP-0118 / CIP-0112), without yet committing to the full batch semantics (issue #1007) or phase-2 execution model (issue #1006).

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Abstract
open import Ledger.Dijkstra.Specification.Transaction

module Ledger.Dijkstra.Specification.Utxo
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Dijkstra.Specification.Certs govStructure
open import Ledger.Dijkstra.Specification.Script.Validation txs abs

Environments and states

record UTxOEnv : Type where
  field
    slot             : Slot
    pparams          : PParams
    treasury         : Treasury
    utxo₀            : UTxO
    isTopLevelValid  : Bool
    globalScripts    : ℙ P1Script × ℙ P2Script
    globalData       : DataHash ⇀ Datum

The utxo₀ field of UTxOEnv is introduced in the Dijkstra era; it denotes a snapshot of the UTxO before any subtransactions of a batch are applied.

record UTxOState : Type where
  field
    utxo       : UTxO
    fees       : Fees
    deposits   : Deposits
    donations  : Donations

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) ])

private variable
  Γ : UTxOEnv
  s s' : UTxOState
  tx : TopLevelTx
  stx : SubLevelTx

UTXOS

(skeleton/stub)

UTXOS will eventually process the batch (top-level tx + its subTxs) and handle phase-2 success/failure behavior. For now it is merely a hook point.

data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
  UTXOS-stub :
    ────────────────────────────────
    Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s

The UTXO Transition System

New in Dijkstra

The CIP (TODO: add reference) states:

All inputs of all transactions in a single batch must be contained in the UTxO set before any of the batch transactions are applied. This ensures that operation of scripts is not disrupted, for example, by temporarily duplicating thread tokens, or falsifying access to assets via flash loans. In the future, this may be up for reconsideration.

This is achieved by the following precondition in the UTXO.{AgdaDatatype} and SUBUTXO.{AgdaDatatype} rules:

1. The set of spending inputs must exist in the UTxO before applying the transaction (or partially applying any part of it).

data _⊢_⇀⦇_,SUBUTXO⦈_ : UTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where

  SUBUTXO :

    ∙ SpendInputsOf tx ≢ ∅
    ∙ SpendInputsOf tx ⊆ dom (UTxOOf Γ)                           -- (1)
    ∙ SpendInputsOf tx ⊆ dom (UTxOOf s)
    ∙ ReferenceInputsOf tx ⊆ dom (UTxOOf s)
      ────────────────────────────────
      Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'

data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where

  UTXO :

    ∙ SpendInputsOf tx ≢ ∅
    ∙ SpendInputsOf tx ⊆ dom (UTxOOf Γ)                           -- (1)
    ∙ SpendInputsOf tx ⊆ dom (UTxOOf s)
    ∙ ReferenceInputsOf tx ⊆ dom (UTxOOf s)
    ∙ requiredTopLevelGuardsSatisfied tx (SubTransactionsOf tx)   -- (2)
    ∙ Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'
      ────────────────────────────────
      Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'

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