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

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


languages : Tx ℓ → UTxO → ℙ Language
languages tx utxo = ∅ -- TODO

allowedLanguages : Tx ℓ → UTxO → ℙ Language
allowedLanguages tx utxo = ∅ -- TODO


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

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

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

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

         p1Scripts : ℙ P1Script
         p1Scripts = proj₁ (Γ .globalScripts)

         p2Scripts : ℙ P2Script
         p2Scripts = proj₂ (Γ .globalScripts)

         neededScriptHashes  : ℙ ScriptHash
         neededScriptHashes  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo₀ txBody)

         neededVKeyHashes : ℙ KeyHash
         neededVKeyHashes = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo₀ txBody)

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

    in
    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
    ∙  ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
    ∙  neededVKeyHashes ⊆ witsKeyHashes
    ∙  neededScriptHashes ⊆ mapˢ hash p1Scripts ∪ mapˢ hash p2Scripts
    ∙  neededDataHashes ⊆ dom (Γ .globalData)
    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
    ∙  txADhash ≡ map hash txAuxData
    ∙ Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s'
      ────────────────────────────────
      Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s'

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

  UTXOW :
    let
         open Tx tx
         open TxBody txBody
         open TxWitnesses txWitnesses
         open UTxOEnv

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

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

         p1Scripts : ℙ P1Script
         p1Scripts = proj₁ (Γ .globalScripts)

         p2Scripts : ℙ P2Script
         p2Scripts = proj₂ (Γ .globalScripts)

         neededScriptHashes  : ℙ ScriptHash
         neededScriptHashes  = mapPartial (isScriptObj  ∘ proj₂) (credsNeeded utxo₀ txBody)

         neededVKeyHashes : ℙ KeyHash
         neededVKeyHashes = mapPartial (isKeyHashObj ∘ proj₂) (credsNeeded utxo₀ txBody)

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

    in
    ∙  ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ
    ∙  ∀[ s ∈ p1Scripts ] (hash s ∈ neededScriptHashes → validP1Script witsKeyHashes txVldt s)
    ∙  neededVKeyHashes ⊆ witsKeyHashes
    ∙  neededScriptHashes ⊆ mapˢ hash p1Scripts ∪ mapˢ hash p2Scripts
    ∙  neededDataHashes ⊆ dom (Γ .globalData)
    ∙  languages tx utxo ⊆ allowedLanguages tx utxo
    ∙  txADhash ≡ map hash txAuxData
    ∙  Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s'
      ────────────────────────────────
      Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'