{-# OPTIONS --safe #-}

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

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

open import Ledger.Dijkstra.Specification.Utxo txs abs
open import Ledger.Dijkstra.Specification.Script.Validation txs abs
import Data.List.Relation.Unary.Any as L
import Data.List.Relation.Unary.All as L

private variable
  ℓ     : TxLevel
  A     : Type
  Γ     : A
  s s'  : UTxOState
  txTop : TopLevelTx
  txSub : SubLevelTx


UsesBootstrapAddress : UTxO → Tx ℓ → Type
UsesBootstrapAddress utxo tx
  = ∃[ o ∈ (range txOuts) ∪ range (utxo ∣ (txIns ∪ referenceInputs)) ] isBootstrapAddr (proj₁ o)
  where
    open Tx tx; open TxBody txBody

module _ (tx : TopLevelTx) where
  open Tx tx
  open TxBody txBody

  module _ (utxo : UTxO) where
    HasInlineDatum : TxOut → Type
    HasInlineDatum txout = Is-just (txOutToDatum txout)

    UsesV2Features : Type
    UsesV2Features = ∃[ o ∈ (range txOuts) ∪ range (utxo ∣ (txIns ∪ referenceInputs)) ] HasInlineDatum o

  data UsesV3Features : Set where
    hasVotes     : ¬ (Is-[] txGovVotes)     → UsesV3Features
    hasProposals : ¬ (Is-[] txGovProposals) → UsesV3Features
    hasDonation  : NonZero txDonation       → UsesV3Features
    hasTreasure  : Is-just currentTreasury  → UsesV3Features

  data UsesV4Features : Set where
    hasSubtransactions  : ¬ (Is-[] txSubTransactions) → UsesV4Features
    hasGuards           : ¬ (Is-∅ txGuards)           → UsesV4Features


module _ {tx : TopLevelTx} where
  open Tx tx
  open TxBody txBody

  instance
    Dec-UsesV3Features : UsesV3Features tx ⁇
    Dec-UsesV3Features .dec
      with ¿ ¬ (Is-[] txGovVotes) ¿ | ¿ ¬ (Is-[] txGovProposals) ¿
         | ¿ NonZero txDonation   ¿ | ¿ Is-just currentTreasury  ¿
    ... | yes p | _ | _ | _ = yes (hasVotes p)
    ... | _ | yes p | _ | _ = yes (hasProposals p)
    ... | _ | _ | yes p | _ = yes (hasDonation p)
    ... | _ | _ | _ | yes p = yes (hasTreasure p)
    ... | no p₁ | no p₂ | no p₃ | no p₄
      = no λ { (hasVotes x) → p₁ x ; (hasProposals x) → p₂ x ; (hasDonation x) → p₃ x ; (hasTreasure x) → p₄ x}

module _ {tx : TopLevelTx} where
  open Tx tx
  open TxBody txBody

  instance
    Dec-UsesV4Features : UsesV4Features tx ⁇
    Dec-UsesV4Features .dec
      with ¿ ¬ (Is-[] txSubTransactions) ¿ | ¿ ¬ (Is-∅ txGuards) ¿
    ... | yes p | _ = yes (hasSubtransactions p)
    ... | _ | yes p = yes (hasGuards p)
    ... | no p₁ | no p₂
      = no λ { (hasSubtransactions x) → p₁ x ; (hasGuards x) → p₂ x}


languages :  ℙ P2Script → ℙ Language
languages p2Scripts = mapˢ language p2Scripts

allowedLanguagesLegacyMode : TopLevelTx → UTxO → ℙ Language
allowedLanguagesLegacyMode tx utxo =
  if UsesV3Features tx
    then fromList (PlutusV3 ∷ [])
    else
  if UsesV2Features tx utxo
    then fromList (PlutusV3 ∷ PlutusV2 ∷ [])
    else fromList (PlutusV3 ∷ PlutusV2 ∷ PlutusV1 ∷ [])


data _⊢_⇀⦇_,SUBUTXOW⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where

  SUBUTXOW :
    let
         open Tx txSub
         open TxBody txBody
         open TxWitnesses txWitnesses
         open UTxOEnv

         utxo₀ = UTxOOf Γ
         utxo  = UTxOOf s

         vKeyHashesProvided : ℙ KeyHash
         vKeyHashesProvided = mapˢ hash (dom vKeySigs)

         scriptsProvided : ℙ Script
         scriptsProvided = ScriptPoolOf Γ

         dataProvided : ℙ Data
         dataProvided = range (DataPoolOf Γ)

         credentialsNeeded : ℙ Credential
         credentialsNeeded = mapˢ proj₂ (credsNeeded utxo₀ txSub)

         vKeyHashesNeeded : ℙ KeyHash
         vKeyHashesNeeded = mapPartial isKeyHashObj credentialsNeeded

         scriptHashesNeeded : ℙ ScriptHash
         scriptHashesNeeded = mapPartial isScriptObj credentialsNeeded

         scriptsNeeded : ℙ Script
         scriptsNeeded = filterˢ (λ s → hash s ∈ scriptHashesNeeded) scriptsProvided

         p1ScriptsNeeded : ℙ P1Script
         p1ScriptsNeeded = mapPartial toP1Script scriptsNeeded

         p2ScriptsNeeded : ℙ P2Script
         p2ScriptsNeeded = mapPartial toP2Script scriptsNeeded

         dataHashesNeeded : ℙ DataHash
         dataHashesNeeded =
           mapPartial (λ txOut@(a , _ , d , _) →
                           do sh ← isScriptObj (payCred a)
                              _  ← lookupHash sh p2ScriptsNeeded
                              d >>= isInj₂)
                      (range (utxo₀ ∣ txIns))

    in
    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
    ∙  ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided txVldt s
    ∙  vKeyHashesNeeded ⊆ vKeyHashesProvided
    ∙  scriptHashesNeeded ⊆ mapˢ hash scriptsProvided
    ∙  dataHashesNeeded ⊆ mapˢ hash dataProvided
    ∙  languages p2ScriptsNeeded ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ ❴ PlutusV4 ❵ -- (1)
    ∙  txADhash ≡ map hash txAuxData
    ∙  Γ ⊢ s ⇀⦇ txSub ,SUBUTXO⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ txSub ,SUBUTXOW⦈ s'


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


  UTXOW-normal :
    let
         open Tx txTop
         open TxBody txBody
         open TxWitnesses txWitnesses
         open UTxOEnv

         utxo₀ = Γ .utxo₀
         utxo  = s .UTxOState.utxo

         vKeyHashesProvided : ℙ KeyHash
         vKeyHashesProvided = mapˢ hash (dom vKeySigs)

         scriptsProvided : ℙ Script
         scriptsProvided = ScriptPoolOf Γ

         dataProvided : ℙ Data
         dataProvided = range (DataPoolOf Γ)

         credentialsNeeded : ℙ Credential
         credentialsNeeded = mapˢ proj₂ (credsNeeded utxo₀ txTop)

         vKeyHashesNeeded : ℙ KeyHash
         vKeyHashesNeeded = mapPartial isKeyHashObj credentialsNeeded

         scriptHashesNeeded : ℙ ScriptHash
         scriptHashesNeeded = mapPartial isScriptObj credentialsNeeded

         scriptsNeeded : ℙ Script
         scriptsNeeded = filterˢ (λ s → hash s ∈ scriptHashesNeeded) scriptsProvided

         p1ScriptsNeeded : ℙ P1Script
         p1ScriptsNeeded = mapPartial toP1Script scriptsNeeded

         p2ScriptsNeeded : ℙ P2Script
         p2ScriptsNeeded = mapPartial toP2Script scriptsNeeded

         dataHashesNeeded : ℙ DataHash
         dataHashesNeeded =
           mapPartial (λ txOut@(a , _ , d , _) →
                           do sh ← isScriptObj (payCred a)
                              _  ← lookupHash sh p2ScriptsNeeded
                              d >>= isInj₂)
                      (range (utxo₀ ∣ txIns))

    in
    ∙  (UsesBootstrapAddress utxo₀ txTop → Is-∅ p2ScriptsNeeded) -- (2)
    ∙  RequiredGuardsInTopLevel txTop -- (3)
    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
    ∙  ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided txVldt s
    ∙  vKeyHashesNeeded ⊆ vKeyHashesProvided
    ∙  scriptHashesNeeded ⊆ mapˢ hash scriptsProvided
    ∙  dataHashesNeeded ⊆ mapˢ hash dataProvided
    ∙  languages p2ScriptsNeeded ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ ❴ PlutusV4 ❵ -- (1)
    ∙  txADhash ≡ map hash txAuxData
    ∙  (Γ , false) ⊢ s ⇀⦇ txTop ,UTXO⦈ s'
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ txTop ,UTXOW⦈ s'


  UTXOW-legacy :
    let
         open Tx txTop
         open TxBody txBody
         open TxWitnesses txWitnesses
         open UTxOEnv

         utxo₀ = UTxOOf Γ
         utxo  = UTxOOf s

         vKeyHashesProvided : ℙ KeyHash
         vKeyHashesProvided = mapˢ hash (dom vKeySigs)

         scriptsProvided : ℙ Script
         scriptsProvided = witnessScripts txTop
                           ∪ spendScripts txTop utxo₀
                           ∪ referenceScripts txTop utxo₀

         dataProvided : ℙ Datum
         dataProvided = getTxData txTop utxo₀

         credentialsNeeded : ℙ Credential
         credentialsNeeded = mapˢ proj₂ (credsNeeded utxo₀ txTop)

         vKeyHashesNeeded : ℙ KeyHash
         vKeyHashesNeeded = mapPartial isKeyHashObj credentialsNeeded

         scriptHashesNeeded : ℙ ScriptHash
         scriptHashesNeeded = mapPartial isScriptObj credentialsNeeded

         scriptsNeeded : ℙ Script
         scriptsNeeded = filterˢ (λ s → hash s ∈ scriptHashesNeeded) scriptsProvided

         p1ScriptsNeeded : ℙ P1Script
         p1ScriptsNeeded = mapPartial toP1Script scriptsNeeded

         p2ScriptsNeeded : ℙ P2Script
         p2ScriptsNeeded = mapPartial toP2Script scriptsNeeded

         dataHashesNeeded : ℙ DataHash
         dataHashesNeeded =
           mapPartial (λ txOut@(a , _ , d , _) →
                           do sh ← isScriptObj (payCred a)
                              _  ← lookupHash sh p2ScriptsNeeded
                              d >>= isInj₂)
                      (range (utxo₀ ∣ txIns))
    in
    ∙  ∃[ s ∈ p2ScriptsNeeded ]
         language s ∈ fromList (PlutusV1 ∷ PlutusV2 ∷ PlutusV3 ∷ []) -- (1)
    ∙  ¬ (UsesBootstrapAddress utxo₀ txTop) -- (3)
    ∙  Is-∅ (GuardsOf txTop) -- (4)
    ∙  RequiredGuardsInTopLevel txTop -- (4)
    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
    ∙  ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided txVldt s
    ∙  vKeyHashesNeeded ⊆ vKeyHashesProvided
    ∙  scriptHashesNeeded ⊆ mapˢ hash scriptsProvided
    ∙  dataHashesNeeded ⊆ mapˢ hash dataProvided
    ∙  languages p2ScriptsNeeded ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ allowedLanguagesLegacyMode txTop utxo -- (2)
    ∙  txADhash ≡ map hash txAuxData
    ∙  (Γ , true) ⊢ s ⇀⦇ txTop ,UTXO⦈ s'
      ────────────────────────────────
      Γ ⊢ s ⇀⦇ txTop ,UTXOW⦈ s'


unquoteDecl UTXOW-normal-premises = genPremises UTXOW-normal-premises (quote UTXOW-normal)
unquoteDecl UTXOW-legacy-premises = genPremises UTXOW-legacy-premises (quote UTXOW-legacy)
unquoteDecl SUBUTXOW-premises = genPremises SUBUTXOW-premises (quote SUBUTXOW)
pattern SUBUTXOW-⋯ p₁ p₂ p₃ p₄ p₅ p₆ p₇ h = SUBUTXOW (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , h)