Utxow

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Core.Specification.Crypto
open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Conformance.Utxow
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where
open import Ledger.Conway.Conformance.Utxo txs abs
open import Ledger.Conway.Specification.Script.Validation txs abs
open import Ledger.Conway.Specification.Certs govStructure

private
  module L where
    open import Ledger.Conway.Specification.Utxow txs abs public
    open import Ledger.Conway.Specification.Utxo txs abs public

data

  _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type

private variable
  Γ : UTxOEnv
  s s' : UTxOState
  tx : Tx

data _⊢_⇀⦇_,UTXOW⦈_ where

  UTXOW-inductive :
    let open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits
        open UTxOState s
        witsKeyHashes       = mapˢ hash (dom vkSigs)
        witsScriptHashes    = mapˢ hash scripts
        refScriptHashes     = mapˢ hash (refScripts tx utxo)
        neededScriptHashes  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo txb)
        neededVKeyHashes    = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo txb)
                              ∪ reqSignerHashes
        txdatsHashes        = mapˢ hash txdats
        inputsDataHashes    = mapPartial (λ txout → if txOutToP2Script utxo tx txout
                                                     then txOutToDataHash txout
                                                     else nothing) (range (utxo ∣ txIns))
        refInputsDataHashes = mapPartial txOutToDataHash (range (utxo ∣ refInputs))
        outputsDataHashes   = mapPartial txOutToDataHash (range txOuts)
        nativeScripts       = mapPartial toP1Script (txscripts tx utxo)
        scriptRdrptrs       =
          mapPartial
            (λ (sp , c) → if credentialToP2Script utxo tx c
                          then rdptr txb sp
                          else nothing)
            (credsNeeded utxo txb)
    in
    ∙  ∀[ (vk , σ) ∈ vkSigs ] isSigned vk (txidBytes txId) σ
    ∙  ∀[ s ∈ nativeScripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
    ∙  neededVKeyHashes ⊆ witsKeyHashes
    ∙  neededScriptHashes - refScriptHashes ≡ᵉ witsScriptHashes
    ∙  inputsDataHashes ⊆ txdatsHashes
    ∙  txdatsHashes ⊆ inputsDataHashes ∪ outputsDataHashes ∪ refInputsDataHashes
    ∙  dom txrdmrs ≡ᵉ scriptRdrptrs
    ∙  L.languages tx utxo neededScriptHashes ⊆
         dom (PParams.costmdls (PParamsOf Γ)) ∩ L.allowedLanguages tx utxo
    ∙  ∀[ txOut ∈ range (utxo ∣ txIns) ] L.TxOutSpendable-PlutusV1 utxo tx txOut
    ∙  ∀[ txOut ∈ range (utxo ∣ txIns) ] L.TxOutSpendable-PlutusV2 utxo tx txOut
    ∙  txADhash ≡ map hash txAD
    ∙  scriptIntegrityHash ≡
         L.hashScriptIntegrity
           (UTxOEnv.pparams Γ)
           (L.languages tx utxo neededScriptHashes)
           txrdmrs
           txdats
    ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'

pattern UTXOW-inductive⋯ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉ p₁₀ p₁₁ p₁₂ h
      = UTXOW-inductive (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , h)
pattern UTXOW⇒UTXO x = UTXOW-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ x

unquoteDecl UTXOW-inductive-premises =
  genPremises UTXOW-inductive-premises (quote UTXOW-inductive)