{-# OPTIONS --safe #-}

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

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


module _ (o : TxOut) where
  d = proj₁ (proj₂ (proj₂ o))
  data HasInlineDatum : Set where
    InlineDatum  : ∀ {d'} → d ≡ just (inj₁ d') → HasInlineDatum

instance
  Dec-HasInlineDatum : ∀ {o} → HasInlineDatum o ⁇
  Dec-HasInlineDatum {_ , _ , just (inj₁ x) , _} = ⁇ yes (InlineDatum refl)
  Dec-HasInlineDatum {_ , _ , just (inj₂ x) , _} = ⁇ no λ where
    (InlineDatum x) → case x of λ ()
  Dec-HasInlineDatum {_ , _ , nothing , _} = ⁇ no λ where
    (InlineDatum x) → case x of λ ()

module _ (txb : TxBody) (let open TxBody txb) where
  data UsesV3Features : Set where
    HasVotes : txvote ≢ [] → UsesV3Features
    HasProps : txprop ≢ [] → UsesV3Features
    HasDonation : txdonation ≢  → UsesV3Features
    HasTreasury : curTreasury ≢ nothing → UsesV3Features

instance
  Dec-UsesV3Features : ∀ {txb} → UsesV3Features txb ⁇
  Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = zero ; curTreasury = nothing }}
    = ⁇ no λ where (HasVotes x)    → x refl
                   (HasProps x)    → x refl
                   (HasDonation x) → x refl
                   (HasTreasury x) → x refl
  Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = zero ; curTreasury = just x }}
    = ⁇ yes (HasTreasury (λ ()))
  Dec-UsesV3Features {record { txvote = [] ; txprop = [] ; txdonation = suc txdonation }}
    = ⁇ yes (HasDonation (λ ()))
  Dec-UsesV3Features {record { txvote = [] ; txprop = x ∷ txprop }} = ⁇ yes (HasProps (λ ()))
  Dec-UsesV3Features {record { txvote = x ∷ txvote }} = ⁇ yes (HasVotes (λ ()))

languages : Tx → UTxO → ℙ Language
languages tx utxo = mapPartial getLanguage (txscripts tx utxo)
  where
    getLanguage : Script → Maybe Language
    getLanguage (inj₁ _) = nothing
    getLanguage (inj₂ s) = just (language s)



allowedLanguages : Tx → UTxO → ℙ Language
allowedLanguages tx utxo =
  if (∃[ o ∈ os ] isBootstrapAddr (proj₁ o))
    then ∅
  else if UsesV3Features txb
    then fromList (PlutusV3 ∷ [])
  else if ∃[ o ∈ os ] HasInlineDatum o
    then fromList (PlutusV2 ∷ PlutusV3 ∷ [])
  else
    fromList (PlutusV1 ∷ PlutusV2 ∷ PlutusV3 ∷ [])
  where
    txb = tx .Tx.body; open TxBody txb
    os = range (outs txb) ∪ range (utxo ∣ (txins ∪ refInputs))


data


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


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

open UTxOState

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


  UTXOW-inductive :
    let  utxo                                = s .utxo


         open Tx tx renaming (body to txb); open TxBody txb; open TxWitnesses wits


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


    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
    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
    ∙  txADhash ≡ map hash txAD
    ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'


pattern UTXOW-inductive⋯ p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ h
      = UTXOW-inductive (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)