{-# 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


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


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


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


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'