{-# 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 Algebra.Morphism              using (module MonoidMorphisms; IsMagmaHomomorphism)
open import Data.Integer as ℤ             using (ℤ)
open import Data.List.Relation.Unary.All  using (All)
import Data.Nat as ℕ
open import Data.Nat.Properties           hiding (_≟_)
open import Data.String.Base              using () renaming (_++_ to _+ˢ_)

open import Prelude; open Equivalence
open import Ledger.Prelude hiding (≤-trans; ≤-antisym; All); open Properties

open import Tactic.Cong                 using (cong!)
open import Tactic.EquationalReasoning  using (module ≡-Reasoning)
open import stdlib-meta.Tactic.MonoidSolver.NonNormalising using (solve-macro)
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 Ledger.Dijkstra.Specification.Certs govStructure
open import Relation.Binary.PropositionalEquality

instance
--   _ = TokenAlgebra.Value-CommutativeMonoid tokenAlgebra
--   _ = +-0-monoid
  _ = Functor-ComputationResult

instance
  Computational-SUBUTXO : Computational _⊢_⇀⦇_,SUBUTXO⦈_ String
  Computational-SUBUTXO = record {go} where
    module go where

      computeProof : (Γ : SubUTxOEnv) (s : UTxOState) (txSub : SubLevelTx) → ComputationResult String (Σ UTxOState (_⊢_⇀⦇_,SUBUTXO⦈_ Γ s txSub))
      computeProof Γ s txSub
        with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
      ... | false | [ refl ]
        with ¿ SpendInputsOf txSub ≢ ∅
             × inInterval (SlotOf Γ) (ValidIntervalOf txSub)
             × MaybeNetworkIdOf txSub ~ just NetworkId ¿
      ... | (yes p) = success ($\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#3454}{\htmlId{1998}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{2005}{\htmlClass{Bound}{\text{s}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{2009}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{2016}{\htmlClass{Bound}{\text{s}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{2020}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{2032}{\htmlClass{Bound}{\text{s}}}\, \end{pmatrix}$ , SUBUTXO {txSub = txSub} p)
      ... | (no ¬p) = failure (genErrors ¬p)
      computeProof Γ s txSub | true | [ refl ]
        with ¿ SpendInputsOf txSub ≢ ∅
             × inInterval (SlotOf Γ) (ValidIntervalOf txSub)
             × MaybeNetworkIdOf txSub ~ just NetworkId ¿
      ... | (yes p) = success ($\begin{pmatrix} \,\htmlId{2347}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#3454}{\htmlId{2348}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\htmlId{2355}{\htmlClass{Bound}{\text{s}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2357}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#7179}{\htmlId{2359}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\htmlId{2373}{\htmlClass{Bound}{\text{txSub}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2379}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{2380}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{2382}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#4377}{\htmlId{2385}{\htmlClass{Function}{\text{outs}}}}\, \,\htmlId{2390}{\htmlClass{Bound}{\text{txSub}}}\, \\ \,\href{Ledger.Prelude.Base.html#669}{\htmlId{2398}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\htmlId{2405}{\htmlClass{Bound}{\text{s}}}\, \\ \,\href{Ledger.Prelude.Base.html#554}{\htmlId{2409}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{2421}{\htmlClass{Bound}{\text{s}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2423}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#554}{\htmlId{2425}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\htmlId{2437}{\htmlClass{Bound}{\text{txSub}}}\, \end{pmatrix}$ , SUBUTXO {txSub = txSub} p)
      ... | (no ¬p) = failure (genErrors ¬p)


      completeness : (Γ : SubUTxOEnv) (s : UTxOState) (txSub : SubLevelTx) → ∀ s' → Γ ⊢ s ⇀⦇ txSub ,SUBUTXO⦈ s' → map proj₁ (computeProof Γ s txSub) ≡ success s'
      completeness Γ s txSub s' (SUBUTXO p)
        with IsTopLevelValidFlagOf Γ | inspect IsTopLevelValidFlagOf Γ
      ... | false | [ refl ]
        with ¿ SpendInputsOf txSub ≢ ∅
             × inInterval (SlotOf Γ) (ValidIntervalOf txSub)
             × MaybeNetworkIdOf txSub ~ just NetworkId ¿
      ... |  (yes p) = refl
      ... |  (no ¬p) = ⊥-elim (¬p p)
      completeness Γ s txSub s' (SUBUTXO p) | true  | [ refl ]
        with ¿ SpendInputsOf txSub ≢ ∅
             × inInterval (SlotOf Γ) (ValidIntervalOf txSub)
             × MaybeNetworkIdOf txSub ~ just NetworkId ¿
      ... |  (yes p) = refl
      ... |  (no ¬p) = ⊥-elim (¬p p)