{-# OPTIONS --safe #-}
open import Ledger.Conway.Specification.Gov.Base
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)
open import Ledger.Core.Specification.ProtocolVersion
module Ledger.Conway.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.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Gov govStructure
open import Ledger.Conway.Specification.Gov.Actions govStructure hiding (yes; no)
open import Ledger.Conway.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 (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#748}{\htmlId{1640}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1658}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#1612}{\htmlId{1659}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#1621}{\htmlId{1665}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#1630}{\htmlId{1671}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1672}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$)
isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#710}{\htmlId{1701}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{1722}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ()
isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#748}{\htmlId{1774}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{1795}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#1796}{\htmlId{1796}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#1802}{\htmlId{1802}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#1808}{\htmlId{1808}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{1809}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ = yes (new , rem , q , refl)
isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#786}{\htmlId{1867}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{1888}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ()
isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#824}{\htmlId{1940}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\htmlId{1961}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ()
isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#862}{\htmlId{2013}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{2034}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ()
isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#900}{\htmlId{2086}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\htmlId{2107}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = no λ()
isUpdateCommittee $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#938}{\htmlId{2159}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{2180}{\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.Conway.Specification.Gov.Actions.html#824}{\htmlId{2575}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#2556}{\htmlId{2593}{\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.Conway.Specification.Gov.Actions.html#710}{\htmlId{2885}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{2907}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} _ v = no λ ()
hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#748}{\htmlId{2960}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{2982}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} _ v = no λ ()
hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#786}{\htmlId{3035}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{3057}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} _ v = no λ ()
hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#824}{\htmlId{3110}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#3132}{\htmlId{3132}{\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.Conway.Specification.Gov.Actions.html#862}{\htmlId{3292}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{3314}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} _ v = no λ ()
hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#900}{\htmlId{3367}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\htmlId{3389}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} _ v = no λ ()
hasPrev record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#938}{\htmlId{3442}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{3464}{\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#710}{\htmlId{3641}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\, \\ \,\htmlId{3663}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#748}{\htmlId{3719}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{3741}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#786}{\htmlId{3797}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{3819}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#824}{\htmlId{3875}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.Computational.html#3897}{\htmlId{3897}{\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.Conway.Specification.Gov.Actions.html#862}{\htmlId{4462}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{4484}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#900}{\htmlId{4540}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\htmlId{4562}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
validHFAction? {record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#938}{\htmlId{4618}{\htmlClass{InductiveConstructor}{\text{Info}}}}\, \\ \,\htmlId{4640}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$}} = Dec-⊤
isRegistered? : ∀ Γ v → Dec (isRegistered Γ v)
isRegistered? _ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#423}{\htmlId{4726}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\htmlId{4733}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = ¿ _ ∈ _ ¿
isRegistered? _ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#426}{\htmlId{4771}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\htmlId{4778}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = ¿ _ ∈ _ ¿
isRegistered? _ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#431}{\htmlId{4816}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\htmlId{4823}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = ¿ _ ∈ _ ¿
open GovVoter
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 (gvRole 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 (gvRole 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 (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 (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 | _ = _