Properties
{-# OPTIONS --safe #-} open import Ledger.Conway.Gov.Base open import Ledger.Conway.Transaction using (TransactionStructure) module Ledger.Conway.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.Enact govStructure open import Ledger.Conway.Gov txs open import Ledger.Conway.Gov.Actions govStructure hiding (yes; no) open import Ledger.Conway.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.Gov.Actions.html#1455}{\htmlId{1465}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Gov.Properties.html#1437}{\htmlId{1484}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Gov.Properties.html#1446}{\htmlId{1490}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Gov.Properties.html#1455}{\htmlId{1496}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$) isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1420}{\htmlId{1526}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1544}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ() isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{1595}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Gov.Properties.html#1614}{\htmlId{1614}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Gov.Properties.html#1620}{\htmlId{1620}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Gov.Properties.html#1626}{\htmlId{1626}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ = yes (new , rem , q , refl) isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1490}{\htmlId{1684}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1702}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ() isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{1753}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\htmlId{1771}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ() isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{1822}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{1840}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ() isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{1891}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\htmlId{1909}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ() isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1630}{\htmlId{1960}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{1978}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ() hasPrev : ∀ x v → Dec (∃[ v' ] x .action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{2055}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Gov.Properties.html#2036}{\htmlId{2067}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$ × pvCanFollow v' v) hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1420}{\htmlId{2124}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{2142}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} v = no λ () hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{2192}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{2210}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} v = no λ () hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1490}{\htmlId{2260}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{2278}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} v = no λ () hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{2328}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Gov.Properties.html#2346}{\htmlId{2346}{\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.Gov.Actions.html#1560}{\htmlId{2508}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{2524}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} v = no λ () hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{2573}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\htmlId{2589}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} v = no λ () hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1630}{\htmlId{2638}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{2654}{\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.Gov.Actions.html#1420}{\htmlId{2827}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{2845}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤ validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{2902}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{2920}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤ validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1490}{\htmlId{2977}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{2995}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤ validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{3052}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Gov.Properties.html#3070}{\htmlId{3070}{\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.Gov.Actions.html#1560}{\htmlId{3629}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{3645}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤ validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{3702}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\, \\ \,\htmlId{3718}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤ validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1630}{\htmlId{3775}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{3791}{\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 | _ = _