{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Specification.Properties
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Chain txs abs
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Prelude


isCredDeposit : DepositPurpose → Type
isCredDeposit (CredentialDeposit x) = ⊤
isCredDeposit _ = ⊥


instance
  isCredDeposit? : isCredDeposit ⁇¹
  isCredDeposit? {CredentialDeposit x} = ⁇ (yes tt)
  isCredDeposit? {PoolDeposit x} = ⁇ (no λ ())
  isCredDeposit? {DRepDeposit x} = ⁇ (no λ ())
  isCredDeposit? {GovActionDeposit x} = ⁇ (no λ ())


isGADeposit : DepositPurpose → Type
isGADeposit (GovActionDeposit x) = ⊤
isGADeposit _ = ⊥


instance
  isGADeposit? : isGADeposit ⁇¹
  isGADeposit? {CredentialDeposit x} = ⁇ (no λ ())
  isGADeposit? {PoolDeposit x} = ⁇ (no λ ())
  isGADeposit? {DRepDeposit x} = ⁇ (no λ ())
  isGADeposit? {GovActionDeposit x} = ⁇ (yes tt)


activeDReps : Epoch → NewEpochState → ℙ Credential
activeDReps currentEpoch s = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) (DRepsOf s))


instance
  _ : IsSet Block Tx
  _ = record { toSet = fromList ∘ Block.ts }

  _ : IsSet TxBody GovProposal
  _ = record { toSet = fromList ∘ TxBody.txprop }


validBlockIn : ChainState → Block → Type
validBlockIn s b = ∃[ s' ] _ ⊢ s ⇀⦇ b ,CHAIN⦈ s'

validBlock : Block → Type
validBlock b = ∃[ s ] validBlockIn s b

validTxIn₁ : ChainState → Tx → Type
validTxIn₁ s tx = ∃[ b ] tx ∈ b × validBlockIn s b


module _ (s : ChainState) (slot : Slot) where

  open ChainState s; open NewEpochState newEpochState
  open EpochState epochState; open EnactState es


  private
    ledgerEnv = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Properties.html#1839}{\htmlId{1992}{\htmlClass{Bound}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#549}{\htmlId{1999}{\htmlClass{Function}{\text{constitution}}}}\, \,\htmlId{2012}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{2013}{\htmlClass{Field}{\text{proj₁}}}}\, \,\htmlId{2019}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#650}{\htmlId{2020}{\htmlClass{Field}{\text{proj₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#654}{\htmlId{2028}{\htmlClass{Function}{\text{pparams}}}}\, \,\htmlId{2036}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{2037}{\htmlClass{Field}{\text{proj₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#1745}{\htmlId{2045}{\htmlClass{Function}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.PParams.html#775}{\htmlId{2050}{\htmlClass{Field}{\text{Acnt.treasury}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#1672}{\htmlId{2064}{\htmlClass{Function}{\text{acnt}}}}\, \end{pmatrix}$

  validTxIn₂ : Tx → Type
  validTxIn₂ tx = ∃[ ls' ] ledgerEnv ⊢ ls ⇀⦇ tx ,LEDGER⦈ ls'

validTx₁ : Tx → Type
validTx₁ tx = ∃[ s ] validTxIn₁ s tx