Ledger.Dijkstra.Specification.Certs.Properties.Computational

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)

module Ledger.Dijkstra.Specification.Certs.Properties.Computational
  (govStructure : GovStructure) where

open import Ledger.Prelude
open import Ledger.Dijkstra.Specification.Gov.Actions govStructure hiding (yes; no)
open import Ledger.Dijkstra.Specification.Certs govStructure

open import stdlib.Data.Maybe
open import stdlib-meta.Tactic.GenError using (genErrors)
import Data.Maybe.Relation.Unary.Any as M
import Data.Maybe.Relation.Unary.All as M

open GovStructure govStructure
open Inverse

open Computational ⦃...⦄

private
  lookupᵐ?? :
    {K V : Type} →
    ⦃ _ : DecEq K ⦄ →
    (m : K ⇀ V) (k : K) →
    Dec (Any (λ (k' , _) → k ≡ k') (m ˢ))
  lookupᵐ?? m k = any? (λ { _ → ¿ _ ¿ }) (m ˢ)

instance
  Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String
  Computational-DELEG .computeProof de ds =
    λ where
    (delegate c mv mc d) → case ¿ (c ∉ dom (RewardsOf ds) → d ≡ DelegEnv.pparams de .PParams.keyDeposit)
                                × (c ∈ dom (RewardsOf ds) → d ≡ 0)
                                × mv ∈ mapˢ (just ∘ vDelegCredential) (DelegEnv.delegatees de) ∪
                                    fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] )
                                × mc ∈ mapˢ just (dom (DelegEnv.pools de)) ∪ ❴ nothing ❵ ¿ of λ where
      (yes p) → success (-, DELEG-delegate p)
      (no ¬p) → failure (genErrors ¬p)
    (dereg c md) → case lookupᵐ?? (DepositsOf ds) c of λ where
      (yes ((_ , d) , _ , _)) →
        case
          ¿ (c , 0) ∈ (RewardsOf ds)
          × (c , d) ∈ (DepositsOf ds)
          × (md ≡ nothing ⊎ md ≡ just d)
          ¿ of λ where
            (yes q) → success (-, DELEG-dereg q)
            (no ¬q) → failure (genErrors ¬q)
      (no ¬p) → failure (genErrors ¬p)
    _ → failure "Unexpected certificate in DELEG"

  Computational-DELEG .completeness de ds (delegate c mv mc d)
    s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom (RewardsOf ds) → d ≡ DelegEnv.pparams de .PParams.keyDeposit)
                                           × (c ∈ dom (RewardsOf ds) → d ≡ 0)
                                           × mv ∈ mapˢ (just ∘ vDelegCredential) (DelegEnv.delegatees de) ∪
                                               fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] )
                                           × mc ∈ mapˢ just (dom (DelegEnv.pools de)) ∪ ❴ nothing ❵ ¿) p .proj₂ = refl
  Computational-DELEG .completeness _ ds (dereg c nothing) _ (DELEG-dereg {d = d} h@(p , q , r))
    with lookupᵐ?? (DepositsOf ds) c
  ... | (yes ((_ , d') , s₂ , refl)) rewrite dec-yes
          (¿ (c , 0) ∈ (RewardsOf ds)
           × (c , d') ∈ (DepositsOf ds)
           × (nothing ≡ nothing {A = ℕ} ⊎ nothing ≡ just d')
           ¿) (p , s₂ , inj₁ refl) .proj₂ = refl
  Computational-DELEG .completeness _ ds (dereg c nothing) _ (DELEG-dereg h@(p , q , r))
      | (no ¬s) = ⊥-elim (¬s (_ , q , refl))
  Computational-DELEG .completeness _ ds (dereg c (just d)) _ (DELEG-dereg h@(p , q , inj₂ refl))
    with lookupᵐ?? (DepositsOf ds) c
  ... | (yes ((_ , d') , q' , refl)) rewrite dec-yes
          (¿ (c , 0) ∈ (RewardsOf ds)
           × (c , d') ∈ (DepositsOf ds)
           × (just d ≡ nothing {A = ℕ} ⊎ just d ≡ just d')
           ¿) (p , q' , inj₂ (cong just (proj₂ (DepositsOf ds) q q'))) .proj₂ = refl
  ... | (no ¬s) = ⊥-elim (¬s (_ , q , refl))

  Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
  Computational-POOL .computeProof _ stᵖ (regpool c _)
    with ¿ Is-just (lookupᵐ? (PoolsOf stᵖ) c) ¿
  ... | yes p = success (-, (POOL-rereg p))
  ... | no ¬p = success (-, (POOL-reg (¬Is-just↔Is-nothing _ .to ¬p)))
  Computational-POOL .computeProof _ stᵖ (retirepool c e) = success (-, POOL-retirepool)
  Computational-POOL .computeProof _ stᵖ _ = failure "Unexpected certificate in POOL"
  Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-reg p)
    with ¿ Is-just (lookupᵐ? (PoolsOf stᵖ) c) ¿
  ... | yes p' = ⊥-elim (¬Is-just↔Is-nothing _ .from p p')
  ... | no _ = refl
  Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-rereg p)
    with ¿ Is-just (lookupᵐ? (PoolsOf stᵖ) c) ¿
  ... | yes _ = refl
  ... | no ¬p = ⊥-elim (¬p p)
  Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl

  Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
  Computational-GOVCERT .computeProof ce gs (regdrep c d _) =
    case ¿ d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf gs)
         ⊎ d ≡ 0 × c ∈ dom (DRepsOf gs) ¿ of λ where
      (yes p) → success (-, GOVCERT-regdrep p)
      (no ¬p) → failure (genErrors ¬p)
  Computational-GOVCERT .computeProof ce gs (deregdrep c d) =
    case ¿ c ∈ dom (DRepsOf gs) × (c , d) ∈  (DepositsOf gs) ¿ of λ where
      (yes p) → success (-, GOVCERT-deregdrep p)
      (no ¬p)  → failure (genErrors ¬p)
  Computational-GOVCERT .computeProof ce gs (ccreghot c _) =
    case ¿ ((c , nothing) ∉ CCHotKeysOf gs ˢ) × c ∈ CertEnv.coldCreds ce ¿ of λ where
      (yes p) → success (-, GOVCERT-ccreghot p)
      (no ¬p) → failure (genErrors ¬p)
  Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
  Computational-GOVCERT .completeness ce gs (regdrep c d _) _ (GOVCERT-regdrep p)
    rewrite dec-yes
      ¿  (d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf gs))
         ⊎ (d ≡ 0 × c ∈ dom (DRepsOf gs))
      ¿ p .proj₂ = refl
  Computational-GOVCERT .completeness _ gs (deregdrep c d) _ (GOVCERT-deregdrep p)
    rewrite dec-yes ¿ c ∈ dom (DRepsOf gs) × (c , d) ∈ (DepositsOf gs) ¿ p .proj₂ = refl
  Computational-GOVCERT .completeness ce gs (ccreghot c _) _ (GOVCERT-ccreghot p)
    rewrite dec-yes ¿ (c , nothing) ∉ CCHotKeysOf gs ˢ × c ∈ CertEnv.coldCreds ce ¿ p .proj₂ = refl

  Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
  Computational-CERT .computeProof ce cs dCert
    with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PParams.html#4415}{\htmlId{6005}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5969}{\htmlId{6015}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3051}{\htmlId{6020}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5972}{\htmlId{6028}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6033}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6037}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4981}{\htmlId{6038}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5972}{\htmlId{6046}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6048}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert
         | computeProof (PParamsOf ce) (PStateOf cs) dCert
         | computeProof ce (GStateOf cs) dCert

  ... | success (_ , h) | _               | _               = success (-, CERT-deleg h)
  ... | failure _       | success (_ , h) | _               = success (-, CERT-pool h)
  ... | failure _       | failure _       | success (_ , h) = success (-, CERT-gov h)
  ... | failure e₁      | failure e₂      | failure e₃      = failure $
    "DELEG: " <> e₁ <> "\nPOOL: " <> e₂ <> "\nGOV: " <> e₃
  Computational-CERT .completeness ce cs
    dCert@(delegate c mv mc d) cs' (CERT-deleg h)
    with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PParams.html#4415}{\htmlId{6686}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6606}{\htmlId{6696}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3051}{\htmlId{6701}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6609}{\htmlId{6709}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6714}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6718}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4981}{\htmlId{6719}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6609}{\htmlId{6727}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6729}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert
         | completeness _ _ _ _ h
  ... | success _ | refl = refl
  Computational-CERT .completeness ce cs
    dCert@(dereg c _) cs' (CERT-deleg h)
    with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PParams.html#4415}{\htmlId{6925}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6854}{\htmlId{6935}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3051}{\htmlId{6940}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6857}{\htmlId{6948}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6953}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6957}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4981}{\htmlId{6958}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6857}{\htmlId{6966}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6968}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert
         | completeness _ _ _ _ h
  ... | success _ | refl = refl
  Computational-CERT .completeness ce cs
    dCert@(regpool c poolParams) cs' (CERT-pool h)
    with computeProof (CertEnv.pp ce) (CertState.pState cs) dCert
    | completeness _ _ _ _ h
  ... | success _ | refl = refl
  Computational-CERT .completeness ce cs
    dCert@(retirepool c e) cs' (CERT-pool h)
    with completeness _ _ _ _ h
  ... | refl = refl
  Computational-CERT .completeness Γ cs
    dCert@(regdrep c _ _) cs' (CERT-gov h)
    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
  ... | success _ | refl = refl
  Computational-CERT .completeness Γ cs
    dCert@(deregdrep c _) cs' (CERT-gov h)
    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
  ... | success _ | refl = refl
  Computational-CERT .completeness Γ cs
    dCert@(ccreghot c mkh) cs' (CERT-gov h)
    with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h
  ... | success _ | refl = refl


  Computational-PRE-CERT : Computational _⊢_⇀⦇_,PRE-CERT⦈_ String
  Computational-PRE-CERT .computeProof ce cs _ =
    case ¿  filterˢ isKeyHash (mapˢ CredentialOf (dom (WithdrawalsOf ce))) ⊆ dom (VoteDelegsOf cs)
            × mapˢ CredentialOf (dom (WithdrawalsOf ce)) ⊆ dom (RewardsOf cs)
            × ∀[ (addr , amt) ∈ WithdrawalsOf ce ˢ ] amt ≤ maybe id 0 (lookupᵐ? (RewardsOf cs) (CredentialOf addr))  ¿
    of λ where
      (yes p) → success (-, CERT-pre p)
      (no ¬p) → failure (genErrors ¬p)

  Computational-PRE-CERT .completeness ce st _ st' (CERT-pre p) rewrite
    dec-yes ¿  filterˢ isKeyHash (mapˢ CredentialOf (dom (WithdrawalsOf ce))) ⊆ dom (VoteDelegsOf st)
               × mapˢ CredentialOf (dom (WithdrawalsOf ce)) ⊆ dom (RewardsOf st)
               × ∀[ (addr , amt) ∈ WithdrawalsOf ce ˢ ] amt ≤ maybe id 0 (lookupᵐ? (RewardsOf st) (CredentialOf addr))  ¿
        p .proj₂ = refl

  Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
  Computational-POST-CERT .computeProof ce cs tt with ¿ dom (CertEnv.directDeposits ce) ⊆ dom (RewardsOf cs) ¿
  ... | (no ¬p) = failure (genErrors ¬p)
  ... | (yes p) = success (cs' , CERT-post p)
    where
      validVoteDelegs : VoteDelegs
      validVoteDelegs = VoteDelegsOf cs ∣^ (mapˢ vDelegCredential (dom (DRepsOf cs)) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )

      newRewards : Rewards
      newRewards = RewardsOf cs ∪⁺ CertEnv.directDeposits ce

      cs' : CertState
      cs' = $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#9184}{\htmlId{9481}{\htmlClass{Function}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3494}{\htmlId{9499}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\htmlId{9513}{\htmlClass{Bound}{\text{cs}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#9360}{\htmlId{9518}{\htmlClass{Function}{\text{newRewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2818}{\htmlId{9531}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{9542}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3618}{\htmlId{9543}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\htmlId{9552}{\htmlClass{Bound}{\text{cs}}}\,\,\htmlId{9554}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3726}{\htmlId{9560}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\htmlId{9569}{\htmlClass{Bound}{\text{cs}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3834}{\htmlId{9574}{\htmlClass{Field}{\text{GStateOf}}}}\, \,\htmlId{9583}{\htmlClass{Bound}{\text{cs}}}\, \end{pmatrix}$

  Computational-POST-CERT .completeness ce cs _ cs' (CERT-post p) with ¿ dom (CertEnv.directDeposits ce) ⊆ dom (RewardsOf cs) ¿
  ... | yes _ = refl
  ... | no ¬p = ⊥-elim (¬p p)

Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
Computational-CERTS = it