Properties

{-# OPTIONS --safe #-}

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

module Ledger.Conway.Specification.Gov.Properties
  (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.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Conway.Specification.Gov.Actions govStructure hiding (yes; no)
open import Ledger.Conway.Specification.Ratify txs

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 (action 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.Conway.Specification.Gov.Actions.html#1511}{\htmlId{1561}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Specification.Gov.Properties.html#1533}{\htmlId{1580}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.html#1542}{\htmlId{1586}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.html#1551}{\htmlId{1592}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$)
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1476}{\htmlId{1622}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{1640}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1511}{\htmlId{1691}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Specification.Gov.Properties.html#1710}{\htmlId{1710}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.html#1716}{\htmlId{1716}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.html#1722}{\htmlId{1722}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ = yes (new , rem , q , refl)
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1546}{\htmlId{1780}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1798}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{1849}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\htmlId{1867}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1616}{\htmlId{1918}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\htmlId{1936}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1651}{\htmlId{1987}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\htmlId{2005}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ = no λ()
  isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1686}{\htmlId{2056}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{2074}{\htmlClass{Symbol}{\text{\_}}}\,               \end{pmatrix}$ = no λ()

  hasPrev : ∀ x v → Dec (∃[ v' ] x .action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{2151}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.html#2132}{\htmlId{2163}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$ × pvCanFollow v' v)
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1476}{\htmlId{2220}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{2238}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$} v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1511}{\htmlId{2288}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{2306}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$} v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1546}{\htmlId{2356}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{2374}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$} v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{2424}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Specification.Gov.Properties.html#2442}{\htmlId{2442}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$} v = case pvCanFollow? {v'} {v} of λ where
    (yes p) → yes (-, refl , p)
    (no ¬p) → no  (λ where (_ , refl , h) → ¬p h)
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1616}{\htmlId{2604}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{2620}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1651}{\htmlId{2669}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,  \\ \,\htmlId{2685}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} v = no λ ()
  hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1686}{\htmlId{2734}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,          \\ \,\htmlId{2750}{\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.Conway.Specification.Gov.Actions.html#1476}{\htmlId{2923}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{2941}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1511}{\htmlId{2998}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{3016}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1546}{\htmlId{3073}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{3091}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1581}{\htmlId{3148}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\href{Ledger.Conway.Specification.Gov.Properties.html#3166}{\htmlId{3166}{\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) 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.Conway.Specification.Gov.Actions.html#1616}{\htmlId{3725}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{3741}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1651}{\htmlId{3798}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,  \\ \,\htmlId{3814}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$}} = Dec-⊤
    validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1686}{\htmlId{3871}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,          \\ \,\htmlId{3887}{\htmlClass{Symbol}{\text{\_}}}\,  \end{pmatrix}$}} = Dec-⊤

  isRegistered? : ∀ Γ v → Dec (isRegistered Γ v)
  isRegistered? _ (CC   , _) = ¿ _ ∈ _ ¿
  isRegistered? _ (DRep , _) = ¿ _ ∈ _ ¿
  isRegistered? _ (SPO  , _) = ¿ _ ∈ _ ¿

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

      module GoVote sig where
        open GovVote sig

        computeProof = case lookupActionId pparams (proj₁ voter) gid epoch s ,′ isRegistered? (proj₁ Γ) 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' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV⦈ s' → map proj₁ computeProof ≡ success s'
        completeness s' (GOV-Vote {ast = ast} (mem , cV , reg , ¬expired))
          with lookupActionId pparams (proj₁ voter) gid epoch s | isRegistered? (proj₁ Γ) 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 GovProposal prop
          renaming (action to a; deposit to d; policy to p; returnAddr to addr; prevAction to prev)
        open PParams pparams hiding (a)

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

        H = ¿ actionWellFormed a
            × actionValid rewardCreds p ppolicy epoch a
            × d ≡ govActionDeposit
            × validHFAction prop s enactState
            × hasParent' enactState s (a .gaType) prev
            × NetworkIdOf addr ≡ NetworkId
            × CredentialOf addr ∈ rewardCreds ¿
            ,′ isUpdateCommittee a

        computeProof = case H of λ where
          (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , regReturn) , yes (new , rem , q , refl)) →
            case ¿ ∀[ e ∈ range new ] epoch < 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 {_} {_} {_} {_} {_} {_} {_} {_} {_} {a .gaData} (wf , av , dep , vHFA , en , goodAddr , returnReg))
          (no ¬p , _) → failure (genErrors ¬p)

        completeness : ∀ s' → Γ ⊢ 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 ] epoch < 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' → Γ ⊢ 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 s es} → getHash (s .prevAction) ≡ getHashES es (s .action .gaType)
  → 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 (s .action .gaType) | getHash (s .prevAction)
    ... | just x | just x' with refl <- just-injective eq =
      [ (aid , x) ] , proj₁ ≡ᵉ.refl , All.[] ∷ [] , inj₁ (refl , refl)
    ... | just x | nothing = case eq of λ ()
    ... | nothing | _ = _