{-# OPTIONS --safe #-}

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

module Ledger.Dijkstra.Specification.Utxo.Properties.Computational
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Prelude
open import Ledger.Prelude
open import stdlib-meta.Tactic.GenError using (genErrors)

open import Ledger.Dijkstra.Specification.Utxo txs abs
open import Ledger.Dijkstra.Specification.Script.Validation txs abs
open import Relation.Binary.PropositionalEquality
import Data.Sum.Relation.Unary.All as Sum

open PParams

instance
  _ = Functor-ComputationResult

instance


  Computational-SUBUTXO : Computational _⊢_⇀⦇_,SUBUTXO⦈_ String


  Computational-SUBUTXO = record {go} where
    module go (Γ : SubUTxOEnv) (s₀ : UTxOState) (txSub : SubLevelTx)
      (let H , ⁇ H? = SUBUTXO-premises {txSub = txSub} {Γ = Γ} {s₀ = s₀})
      where

      computeProof : ComputationResult String (Σ UTxOState (_⊢_⇀⦇_,SUBUTXO⦈_ Γ s₀ txSub))
      computeProof
        with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
      ... | false | [ refl ]
        with H?
      ... | (yes p) = success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#3768}{\htmlId{1226}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#844}{\htmlId{1233}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{1238}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#844}{\htmlId{1245}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{1250}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#844}{\htmlId{1262}{\htmlClass{Bound}{\text{s₀}}}}\, \end{pmatrix}$ , SUBUTXO {txSub = txSub} p)
      ... | (no ¬p) = failure "genErrors" -- (genErrors ¬p)
      computeProof | true | [ refl ]
        with H?
      ... | (yes p) = success ( $\begin{pmatrix} \,\htmlId{1443}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3768}{\htmlId{1444}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#844}{\htmlId{1451}{\htmlClass{Bound}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1454}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7630}{\htmlId{1456}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#861}{\htmlId{1470}{\htmlClass{Bound}{\text{txSub}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{1476}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{1477}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{1479}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4821}{\htmlId{1482}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#861}{\htmlId{1487}{\htmlClass{Bound}{\text{txSub}}}}\,

                                \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{1528}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#844}{\htmlId{1535}{\htmlClass{Bound}{\text{s₀}}}}\,
                                \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{1572}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#844}{\htmlId{1584}{\htmlClass{Bound}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{1587}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{1589}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.Properties.Computational.html#861}{\htmlId{1601}{\htmlClass{Bound}{\text{txSub}}}}\,
                                \end{pmatrix}$
                              , SUBUTXO {txSub = txSub} p
                              )
      ... | (no ¬p) = failure "genErrors" -- (genErrors ¬p)


      completeness : ∀ s₁ → Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXO⦈ s₁ → map proj₁ computeProof ≡ success s₁
      completeness s₁ (SUBUTXO p)
        with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
      ... | false | [ refl ]
        with H?
      ... | (yes p) = refl
      ... | (no ¬p) = ⊥-elim (¬p p)
      completeness s₁ (SUBUTXO p) | true  | [ refl ]
        with H?
      ... | (yes p) = refl
      ... | (no ¬p) = ⊥-elim (¬p p)


  Computational-UTXOS : Computational _⊢_⇀⦇_,UTXOS⦈_ String


  Computational-UTXOS = MkComputational computeProof completeness
    where
      --------------------------------------------------------------------------
      -- computeProof for UTXOS
      --------------------------------------------------------------------------
      computeProof : (Γ : UTxOEnv) (_ : ⊤) (txTop : TopLevelTx)
        → ComputationResult String (Σ ⊤ (Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈_))

      computeProof Γ _ txTop
        with ¿ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop ¿
      ... | yes p = success (tt , UTXOS p)
      ... | no ¬p = failure (genErrors ¬p)

      --------------------------------------------------------------------------
      -- completeness for UTXOS
      --------------------------------------------------------------------------
      completeness : (Γ : UTxOEnv) (_ : ⊤) (txTop : TopLevelTx) (_ : ⊤)
        → Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈ tt
        → (map proj₁ $ computeProof Γ _ txTop) ≡ success tt

      completeness Γ _ txTop _ (UTXOS p)
        with ¿ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop ¿
      ... | yes p = refl
      ... | no ¬p = ⊥-elim (¬p p)



  Computational-UTXO : Computational _⊢_⇀⦇_,UTXO⦈_ String


  Computational-UTXO = record {go} where
    module go (Γ,legacyMode : UTxOEnv × Bool) (s₀ : UTxOState) (txTop : TopLevelTx)
      (let H , ⁇ H? = UTXO-premises {txTop = txTop} {Γ = proj₁ Γ,legacyMode} {s₀ = s₀} {legacyMode = proj₂ Γ,legacyMode})
      where

      module UTXOS = Computational Computational-UTXOS

      computeProof : ComputationResult String (∃[ s₁ ] Γ,legacyMode ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ s₁)
      computeProof
        with IsValidFlagOf txTop | inspect IsValidFlagOf txTop
      ... | false | [ refl ]
        with H?
      ... | (no ¬p) = failure "UTXO" -- (genErrors ¬p)
      ... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)
        with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop
      ... | success h  = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , proj₂ h))
      ... | failure ¬h = failure "UTXOS"
      computeProof | true | [ refl ]
        with H?
      ... | (no ¬p) = failure "UTXO" -- (genErrors ¬p)
      ... | yes (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)
        with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop
      ... | success h  = success (-, UTXO (p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈ , proj₂ h))
      ... | failure ¬h = failure "UTXOS"

      completeness : ∀ s₁ → Γ,legacyMode ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ s₁ → map proj₁ computeProof ≡ success s₁
      completeness s₁ (UTXO-⋯ p₀  p₁  p₂  p₃  p₄  p₅  p₆  p₇  p₈  p₉  p₁₀  p₁₁  p₁₂  p₁₃  p₁₄  p₁₅  p₁₆  p₁₇  p₁₈ h)
        with IsValidFlagOf txTop | inspect IsValidFlagOf txTop
      ... | false | [ refl ]
        with H?
      ... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)))
      ... | yes _
        with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop | UTXOS.completeness _ _ _ _ h
      ... | success h | refl = refl
      completeness s₁ (UTXO-⋯ p₀  p₁  p₂  p₃  p₄  p₅  p₆  p₇  p₈  p₉  p₁₀  p₁₁  p₁₂  p₁₃  p₁₄  p₁₅  p₁₆  p₁₇  p₁₈ h) | true | [ refl ]
        with H?
      ... | no ¬p = ⊥-elim (¬p ((p₀ , p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉ , p₁₀ , p₁₁ , p₁₂ , p₁₃ , p₁₄ , p₁₅ , p₁₆ , p₁₇ , p₁₈)))
      ... | yes _
        with UTXOS.computeProof (Γ,legacyMode .proj₁) tt txTop | UTXOS.completeness _ _ _ _ h
      ... | success h | refl = refl