Computational

{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base
open import Ledger.Dijkstra.Specification.Transaction using (TransactionStructure)

module Ledger.Dijkstra.Specification.Gov.Properties.Computational
  (txs : _) (open TransactionStructure txs using (govStructure))
  (open GovStructure govStructure hiding (epoch)) where

open import Ledger.Prelude hiding (Any; any?)

open import Axiom.Set.Properties

open import Ledger.Core.Specification.ProtocolVersion
open import Ledger.Dijkstra.Specification.Enact govStructure
open import Ledger.Dijkstra.Specification.Gov govStructure
open import Ledger.Dijkstra.Specification.Certs govStructure
open import Ledger.Dijkstra.Specification.Gov.Actions govStructure hiding (yes; no)
open import Ledger.Dijkstra.Specification.Ratify govStructure

import Data.List.Membership.Propositional as P
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.All using (all?; All)
open import Data.List.Relation.Unary.Any hiding (map)
open import Data.List.Relation.Unary.Unique.Propositional
open import Data.Maybe.Properties
open import Relation.Binary using (IsEquivalence)

open import Tactic.Defaults
open import stdlib-meta.Tactic.GenError

open Equivalence
open GovActionState
open Inverse

lookupActionId :
  (pparams  : PParams)
  (role     : GovRole)
  (aid      : GovActionID)
  (epoch    : Epoch)
  (s        : GovState)
  → Dec (Any ( λ (aid' , ast) →  aid ≡ aid'
                                 × canVote pparams (GovActionOf ast) role
                                 × ¬ (expired epoch ast) ) s)

lookupActionId pparams role aid epoch =
  let  instance _ = λ {e ga} → ⁇ (expired? e ga)
  in   any? λ _ → ¿ _ ¿


private
  isUpdateCommittee : (a : GovAction)
    → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{1935}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1953}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#1907}{\htmlId{1954}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#1916}{\htmlId{1960}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#1925}{\htmlId{1966}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1967}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$)
  -- (new , rem , q) : (Credential ⇀ Epoch) × ℙ Credential × ℚ

  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{2060}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,       \\ \,\htmlId{2081}{\htmlClass{Symbol}{\text{\_}}}\,                \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{2133}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,    \\ \,\htmlId{2154}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#2155}{\htmlId{2155}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#2161}{\htmlId{2161}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#2167}{\htmlId{2167}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{2168}{\htmlClass{Symbol}{\text{)}}}\,  \end{pmatrix}$ = yes (new , rem , q , refl)
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{2226}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,    \\ \,\htmlId{2247}{\htmlClass{Symbol}{\text{\_}}}\,                \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{2299}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,    \\ \,\htmlId{2320}{\htmlClass{Symbol}{\text{\_}}}\,                \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{2372}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,      \\ \,\htmlId{2393}{\htmlClass{Symbol}{\text{\_}}}\,                \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{2445}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\htmlId{2466}{\htmlClass{Symbol}{\text{\_}}}\,                \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{2518}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,               \\ \,\htmlId{2539}{\htmlClass{Symbol}{\text{\_}}}\,                \end{pmatrix}$ = no λ()

  pvFollows : ∀ v' ver v → Dec (if pvCanFollowMajor v' ver
                                   then pvCanFollowMinor v v'
                                   else pvCanFollow v v')
  pvFollows v' ver v with ¿ pvCanFollowMajor v' ver ¿
  ... | yes p = ¿ pvCanFollowMinor v v' ¿
  ... | no ¬p = ¿ pvCanFollow v v' ¿

  hasPrev : ∀ x ver v → Dec (∃[ v' ] x .action ≡ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{2934}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#2915}{\htmlId{2952}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$
                                                      × (if pvCanFollowMajor v' ver
                                                            then pvCanFollowMinor v v'
                                                            else pvCanFollow v v'))
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{3244}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{3266}{\htmlClass{Symbol}{\text{\_}}}\,   \end{pmatrix}$} _ v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{3319}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{3341}{\htmlClass{Symbol}{\text{\_}}}\,   \end{pmatrix}$} _ v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{3394}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{3416}{\htmlClass{Symbol}{\text{\_}}}\,   \end{pmatrix}$} _ v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{3469}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#3491}{\htmlId{3491}{\htmlClass{Bound}{\text{v'}}}}\,  \end{pmatrix}$} ver v
    with pvFollows v' ver v
  ... | yes p = yes (v' , refl , p)
  ... | no ¬p = no (λ where (_ , refl , h) → ¬p h)
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{3651}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{3673}{\htmlClass{Symbol}{\text{\_}}}\,   \end{pmatrix}$} _ v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{3726}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\htmlId{3748}{\htmlClass{Symbol}{\text{\_}}}\,   \end{pmatrix}$} _ v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{3801}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{3823}{\htmlClass{Symbol}{\text{\_}}}\,   \end{pmatrix}$} _ v = no λ ()

opaque
  unfolding validHFAction isRegistered

  instance
    validHFAction? : ∀ {p s e} → validHFAction p s e ⁇
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1049}{\htmlId{4000}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,        \\ \,\htmlId{4022}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1087}{\htmlId{4078}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\,     \\ \,\htmlId{4100}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1125}{\htmlId{4156}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\,     \\ \,\htmlId{4178}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1163}{\htmlId{4234}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\,     \\ \,\href{Ledger.Dijkstra.Specification.Gov.Properties.Computational.html#4256}{\htmlId{4256}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ; prevAction = prev }} {s} {record { pv = (v' , aid') }}
      with aid' ≟ prev ×-dec pvCanFollow? {v} {v'} | any? (λ (aid , x) → aid ≟ prev ×-dec hasPrev x v' v) s
    ... | yes p' | _ = ⁇ yes (inj₁ p')
    ... | no _ | yes p' with ((aid , x) , x∈xs , (refl , v , h)) ← P.find p' = ⁇ yes (inj₂
      (x , v , to ∈-fromList x∈xs , h))
    ... | no ¬p₁ | no ¬p₂ = ⁇ no λ
      { (inj₁ x) → ¬p₁ x
      ; (inj₂ (s , v , (h₁ , h₂ , h₃))) → ¬p₂ $
        ∃∈-Any ((prev , s) , (from ∈-fromList h₁ , refl , (v , h₂ , h₃))) }
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1201}{\htmlId{4821}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,       \\ \,\htmlId{4843}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1239}{\htmlId{4899}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\,  \\ \,\htmlId{4921}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1277}{\htmlId{4977}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,                \\ \,\htmlId{4999}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤

  isRegistered? : ∀ Γ v → Dec (isRegistered Γ v)
  isRegistered? _ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#851}{\htmlId{5085}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\htmlId{5092}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = ¿ _ ∈ _ ¿
  isRegistered? _ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#854}{\htmlId{5130}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\htmlId{5137}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = ¿ _ ∈ _ ¿
  isRegistered? _ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#859}{\htmlId{5175}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\htmlId{5182}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = ¿ _ ∈ _ ¿

open GovVoter

instance
  Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_ String
  Computational-GOV = record {Go} where
    module Go (Γk : GovEnv × ℕ) (s : GovState) where
      Γ : GovEnv
      Γ = proj₁ Γk

      k : ℕ
      k = proj₂ Γk

      module GoVote sig where
        open GovVote sig

        computeProof = case lookupActionId (PParamsOf Γ) (gvRole voter) gid (EpochOf Γ) s ,′ isRegistered? Γ voter of λ where
            (yes p , yes p') → case Any↔ .from p of λ where
              (_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp))
            (yes _ , no ¬p) → failure (genErrors ¬p)
            (no ¬p , _    ) → failure (genErrors ¬p)

        completeness : ∀ s' → (Γ , k) ⊢ s ⇀⦇ inj₁ sig ,GOV⦈ s' → map proj₁ computeProof ≡ success s'
        completeness s' (GOV-Vote {ast = ast} (mem , cV , reg , ¬expired))
          with lookupActionId (PParamsOf Γ) (gvRole voter) gid (EpochOf Γ) s | isRegistered? Γ voter
        ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬expired)))
        ... | yes _ | no ¬p = ⊥-elim $ ¬p reg
        ... | yes p | yes q with Any↔ .from p
        ... | ((_ , ast') , mem , refl , cV) = refl

      module GoProp prop where
        open PParams (PParamsOf Γ)

        instance
          Dec-actionWellFormed = actionWellFormed?
          Dec-actionValid = actionValid?
        {-# INCOHERENT Dec-actionWellFormed #-}
        {-# INCOHERENT Dec-actionValid #-}

        H = ¿ actionWellFormed (GovActionOf prop)
            × actionValid (RewardCredentialsOf Γ) (PolicyOf prop) (GovEnv.ppolicy Γ) (EpochOf Γ) (GovActionOf prop)
            × (DepositOf prop) ≡ govActionDeposit
            × validHFAction prop s (EnactStateOf Γ)
            × hasParent' (EnactStateOf Γ) s ((GovActionOf prop) .gaType) (GovProposal.prevAction prop)
            × NetworkIdOf (RewardAddressOf prop) ≡ NetworkId
            × CredentialOf (RewardAddressOf prop) ∈ (RewardCredentialsOf Γ) ¿
            ,′ isUpdateCommittee (GovActionOf prop)

        pattern gov-propose  {zz} xx = GOV-Propose {_} {_} {_} {_} {_} {_} {_} {_} {_} {zz} xx
        -- The inferred variables in both cases below are
        -- { Γ } { RewardAddressOf prop } { GovActionOf prop } { AnchorOf prop } { PolicyOf prop } { DepositOf prop } { (GovProposal.prevAction prop) } { s } { k }

        computeProof = case H of λ where
          (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , regReturn) , yes (new , rem , q , refl)) →
            case ¿ ∀[ e ∈ range new ] (EpochOf Γ) < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
              (yes newOk) → success (-, gov-propose {(new , rem , q)} (wf , av , dep , vHFA , en , goodAddr , regReturn))
              (no ¬p)     → failure (genErrors ¬p)
          (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , returnReg) , no notNewComm) → success
            (-, gov-propose {(GovActionOf prop) .gaData} (wf , av , dep , vHFA , en , goodAddr , returnReg))
          (no ¬p , _) → failure (genErrors ¬p)

        completeness : ∀ s' → (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV⦈ s' → map proj₁ computeProof ≡ success s'
        completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H
        ... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , HasParent' en , goodAddr))
        ... | (yes (_ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl
        ... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl))
          rewrite dec-yes ¿ ∀[ e ∈ range new ] (EpochOf Γ) < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl

      computeProof : (sig : GovVote ⊎ GovProposal) → _
      computeProof (inj₁ s) = GoVote.computeProof s
      computeProof (inj₂ s) = GoProp.computeProof s

      completeness : ∀ sig s' → (Γ , k) ⊢ s ⇀⦇ sig ,GOV⦈ s' → _
      completeness (inj₁ s) = GoVote.completeness s
      completeness (inj₂ s) = GoProp.completeness s

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

allEnactable-singleton : {aid : GovActionID} {s : GovActionState} {es : EnactState}
  → getHash (GovActionState.prevAction s) ≡ getHashES es (GovActionTypeOf s)
  → allEnactable es [ (aid , s) ]
allEnactable-singleton {aid} {s} {es} eq = helper All.∷ All.[]
  where
    module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence th)

    helper : enactable es (getAidPairsList [ (aid , s) ]) (aid , s)
    helper with getHashES es (GovActionTypeOf s) | getHash (GovActionState.prevAction s)
    ... | just x | just x' with refl <- just-injective eq =
      [ (aid , x) ] , proj₁ ≡ᵉ.refl , All.[] ∷ [] , inj₁ (refl , refl)
    ... | just x | nothing = case eq of λ ()
    ... | nothing | _ = _