Computational

{-# OPTIONS --safe #-}

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

module Ledger.Dijkstra.Specification.Entities.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 Ledger.Dijkstra.Specification.Entities govStructure
open import Ledger.Dijkstra.Specification.Gov govStructure

open import Ledger.Dijkstra.Specification.Certs.Properties.Computational 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 RewardAddress

open GovVote

module Computational-CERTS = Computational Computational-CERTS

instance
  Computational-ENTITIES : Computational _⊢_⇀⦇_,ENTITIES⦈_ String
  Computational-ENTITIES = record {go}
    where
      module go (Γ : CertEnv) (s₀ : CertState) (dCerts : List DCert)
                (let module Γ = CertEnv Γ
                     refresh  = mapPartial (isGovVoterDRep ∘ voter) (fromList Γ.votes)
                     refreshedDReps  = mapValueRestricted (const (Γ.epoch  + Γ.pp .PParams.drepActivity)) (DRepsOf s₀) refresh
                     wdrlCreds       = mapˢ stake (dom Γ.wdrls)
                     ddCreds         = mapˢ stake (dom Γ.directDeposits)
                ) where

        s₁ : CertState
        s₁ = $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4750}{\htmlId{1682}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1178}{\htmlId{1695}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3944}{\htmlId{1700}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1178}{\htmlId{1714}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#1989}{\htmlId{1719}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#2345}{\htmlId{1736}{\htmlClass{Function}{\text{Γ.wdrls}}}}\, \,\htmlId{1744}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3723}{\htmlId{1745}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1178}{\htmlId{1755}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{1757}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3268}{\htmlId{1761}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{1772}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4068}{\htmlId{1773}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1178}{\htmlId{1782}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{1784}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}
               \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4176}{\htmlId{1805}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1178}{\htmlId{1814}{\htmlClass{Bound}{\text{s₀}}}}\,
               \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1366}{\htmlId{1836}{\htmlClass{Bound}{\text{refreshedDReps}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3385}{\htmlId{1870}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1178}{\htmlId{1882}{\htmlClass{Bound}{\text{s₀}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3268}{\htmlId{1904}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{1915}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4284}{\htmlId{1916}{\htmlClass{Field}{\text{GStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1178}{\htmlId{1925}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{1927}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \end{pmatrix}$

        computeProof : ComputationResult String (∃-syntax (_⊢_⇀⦇_,ENTITIES⦈_ Γ s₀ dCerts))
        computeProof with ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (VoteDelegsOf s₀)
                          × wdrlCreds ⊆ dom (RewardsOf s₀)
                          × (∀[ (addr , amt) ∈ Γ.wdrls ˢ ] amt ≤ maybe id  (lookupᵐ? (RewardsOf s₀) (stake addr)))
                          ¿ | Computational-CERTS.computeProof Γ s₁ dCerts
        ... | no ¬p | _ = failure ""
        ... | yes _ | failure e = failure e
        ... | yes (p₁ , p₂ , p₃) | success (s₂ , p)
          with ¿ ddCreds ⊆ dom (RewardsOf s₂) ¿
        ... | no ¬p = failure ""
        ... | yes p₄ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p , p₄)))

        completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ dCerts ,ENTITIES⦈ s' → map proj₁ computeProof ≡ success s'
        completeness s' (ENTITIES (p₁ , p₂ , p₃ , p , p₄))
          with ¿ filterˢ isKeyHash wdrlCreds ⊆ dom (VoteDelegsOf s₀)
               × wdrlCreds ⊆ dom (RewardsOf s₀)
               × (∀[ (addr , amt) ∈ Γ.wdrls ˢ ] amt ≤ maybe id  (lookupᵐ? (RewardsOf s₀) (stake addr)))
               ¿ | Computational-CERTS.computeProof Γ s₁ dCerts | Computational-CERTS.completeness _ _ _ _ p
        ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃))
        ... | yes _ | failure e | ()
        ... | yes (p₁ , p₂ , p₃) | success (s₂ , p) | refl
          with ¿ ddCreds ⊆ dom (RewardsOf s₂) ¿ 
        ... | no ¬p  = ⊥-elim (¬p p₄)
        ... | yes p₄ = refl