Computational
{-# OPTIONS --safe #-}
open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov.Base
module Ledger.Conway.Specification.Certs.Properties.Computational (gs : _) (open GovStructure gs) where
open import Data.Maybe.Properties
open import Relation.Nullary.Decidable
open import Tactic.ReduceDec
open import Algebra using (CommutativeMonoid)
open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no)
open import Ledger.Conway.Specification.Certs gs
open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ)
open import Axiom.Set.Properties th
open import Relation.Binary using (IsEquivalence)
open Computational ⦃...⦄
open import stdlib-meta.Tactic.GenError using (genErrors)
open CertState
open GovVote using (voter)
instance
Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String
Computational-DELEG .computeProof de stᵈ =
let open DelegEnv de; open DState stᵈ in
λ where
(delegate c mv mc d) → case ¿ (c ∉ dom rewards → d ≡ pparams .PParams.keyDeposit)
× (c ∈ dom rewards → d ≡ 0)
× mv ∈ mapˢ (just ∘ vDelegCredential) delegatees ∪
fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] )
× mc ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
¿ of λ where
(yes p) → success (-, DELEG-delegate p)
(no ¬p) → failure (genErrors ¬p)
(dereg c d) → case ¿ (c , 0) ∈ rewards ¿ of λ where
(yes p) → success (-, DELEG-dereg p)
(no ¬p) → failure (genErrors ¬p)
(reg c d) → case ¿ c ∉ dom rewards
× (d ≡ pparams .PParams.keyDeposit ⊎ d ≡ 0)
¿ of λ where
(yes p) → success (-, DELEG-reg p)
(no ¬p) → failure (genErrors ¬p)
_ → failure "Unexpected certificate in DELEG"
Computational-DELEG .completeness de stᵈ (delegate c mv mc d)
s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom (DState.rewards stᵈ) → d ≡ DelegEnv.pparams de .PParams.keyDeposit)
× (c ∈ dom (DState.rewards stᵈ) → d ≡ 0)
× mv ∈ mapˢ (just ∘ vDelegCredential) (DelegEnv.delegatees de) ∪ fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] )
× mc ∈ mapˢ just (dom (DelegEnv.pools de)) ∪ ❴ nothing ❵
¿) p .proj₂ = refl
Computational-DELEG .completeness de stᵈ (dereg c d) _ (DELEG-dereg p)
rewrite dec-yes (¿ (c , 0) ∈ (DState.rewards stᵈ) ¿) p .proj₂ = refl
Computational-DELEG .completeness de stᵈ (reg c d) _ (DELEG-reg p)
rewrite dec-yes (¿ c ∉ dom (DState.rewards stᵈ) × (d ≡ DelegEnv.pparams de .PParams.keyDeposit ⊎ d ≡ 0) ¿) p .proj₂ = refl
Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String
Computational-POOL .computeProof _ stᵖ (regpool c _) = success (-, POOL-regpool)
Computational-POOL .computeProof _ _ (retirepool c e) = success (-, POOL-retirepool)
Computational-POOL .computeProof _ _ _ = failure "Unexpected certificate in POOL"
Computational-POOL .completeness _ stᵖ (regpool c _) _ POOL-regpool = refl
Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl
Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String
Computational-GOVCERT .computeProof ce stᵍ (regdrep c d _) =
let open CertEnv ce; open PParams pp in
case ¿ (d ≡ drepDeposit × c ∉ dom (GState.dreps stᵍ))
⊎ (d ≡ 0 × c ∈ dom (GState.dreps stᵍ)) ¿ of λ where
(yes p) → success (-, GOVCERT-regdrep p)
(no ¬p) → failure (genErrors ¬p)
Computational-GOVCERT .computeProof _ stᵍ (deregdrep c _) =
let open GState stᵍ in
case c ∈? dom dreps of λ where
(yes p) → success (-, GOVCERT-deregdrep p)
(no ¬p) → failure (genErrors ¬p)
Computational-GOVCERT .computeProof ce stᵍ (ccreghot c _) =
let open CertEnv ce; open GState stᵍ in
case ¿ ((c , nothing) ∉ ccHotKeys ˢ) × c ∈ coldCreds ¿ of λ where
(yes p) → success (-, GOVCERT-ccreghot p)
(no ¬p) → failure (genErrors ¬p)
Computational-GOVCERT .computeProof _ _ _ = failure "Unexpected certificate in GOVCERT"
Computational-GOVCERT .completeness ce stᵍ
(regdrep c d _) _ (GOVCERT-regdrep p)
rewrite dec-yes
¿ (let open CertEnv ce; open PParams pp; open GState stᵍ in
(d ≡ drepDeposit × c ∉ dom dreps) ⊎ (d ≡ 0 × c ∈ dom dreps))
¿ p .proj₂ = refl
Computational-GOVCERT .completeness _ stᵍ
(deregdrep c _) _ (GOVCERT-deregdrep p)
rewrite dec-yes (c ∈? dom (GState.dreps stᵍ)) p .proj₂ = refl
Computational-GOVCERT .completeness ce stᵍ
(ccreghot c _) _ (GOVCERT-ccreghot p)
rewrite dec-yes (¿ (((c , nothing) ∉ (GState.ccHotKeys stᵍ) ˢ) × c ∈ CertEnv.coldCreds ce) ¿) p .proj₂ = refl
Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String
Computational-CERT .computeProof ce cs dCert
with computeProof $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#4070}{\htmlId{5124}{\htmlClass{Field}{\text{CertEnv.pp}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#5088}{\htmlId{5135}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4398}{\htmlId{5140}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\htmlId{5153}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4754}{\htmlId{5154}{\htmlClass{Field}{\text{pState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#5091}{\htmlId{5161}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5163}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5167}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5171}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4566}{\htmlId{5172}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\htmlId{5185}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4774}{\htmlId{5186}{\htmlClass{Field}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#5091}{\htmlId{5193}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5195}{\htmlClass{Symbol}{\text{))}}}\, \end{pmatrix}$ (dState cs) dCert
| computeProof (CertEnv.pp ce) (pState cs) dCert | computeProof ce (gState cs) dCert
... | success (_ , h) | _ | _ = success (-, CERT-deleg h)
... | failure _ | success (_ , h) | _ = success (-, CERT-pool h)
... | failure _ | failure _ | success (_ , h) = success (-, CERT-vdel h)
... | failure e₁ | failure e₂ | failure e₃ = failure $
"DELEG: " <> e₁ <> "\nPOOL: " <> e₂ <> "\nVDEL: " <> e₃
Computational-CERT .completeness ce cs
dCert@(delegate c mv mc d) cs' (CERT-deleg h)
with computeProof $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#4070}{\htmlId{5819}{\htmlClass{Field}{\text{CertEnv.pp}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#5739}{\htmlId{5830}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4398}{\htmlId{5835}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\htmlId{5848}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4754}{\htmlId{5849}{\htmlClass{Field}{\text{pState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#5742}{\htmlId{5856}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5858}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5862}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5866}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4566}{\htmlId{5867}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\htmlId{5880}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4774}{\htmlId{5881}{\htmlClass{Field}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#5742}{\htmlId{5888}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5890}{\htmlClass{Symbol}{\text{))}}}\, \end{pmatrix}$ (dState cs) dCert | completeness _ _ _ _ h
... | success _ | refl = refl
Computational-CERT .completeness ce cs
dCert@(reg c d) cs' (CERT-deleg h)
with computeProof $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#4070}{\htmlId{6074}{\htmlClass{Field}{\text{CertEnv.pp}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#6005}{\htmlId{6085}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4398}{\htmlId{6090}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\htmlId{6103}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4754}{\htmlId{6104}{\htmlClass{Field}{\text{pState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#6008}{\htmlId{6111}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6113}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6117}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6121}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4566}{\htmlId{6122}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\htmlId{6135}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4774}{\htmlId{6136}{\htmlClass{Field}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#6008}{\htmlId{6143}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6145}{\htmlClass{Symbol}{\text{))}}}\, \end{pmatrix}$ (dState cs) dCert | completeness _ _ _ _ h
... | success _ | refl = refl
Computational-CERT .completeness ce cs
dCert@(dereg c _) cs' (CERT-deleg h)
with computeProof $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#4070}{\htmlId{6331}{\htmlClass{Field}{\text{CertEnv.pp}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#6260}{\htmlId{6342}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4398}{\htmlId{6347}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\htmlId{6360}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4754}{\htmlId{6361}{\htmlClass{Field}{\text{pState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#6263}{\htmlId{6368}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6370}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6374}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6378}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4566}{\htmlId{6379}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\htmlId{6392}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4774}{\htmlId{6393}{\htmlClass{Field}{\text{gState}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#6263}{\htmlId{6400}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6402}{\htmlClass{Symbol}{\text{))}}}\, \end{pmatrix}$ (dState cs) dCert | completeness _ _ _ _ h
... | success _ | refl = refl
Computational-CERT .completeness ce cs
dCert@(regpool c poolParams) cs' (CERT-pool h)
with completeness _ _ _ _ h
... | refl = refl
Computational-CERT .completeness ce cs
dCert@(retirepool c e) cs' (CERT-pool h)
with completeness _ _ _ _ h
... | refl = refl
Computational-CERT .completeness ce cs
dCert@(regdrep c d an)
cs' (CERT-vdel h)
with computeProof ce (gState cs) dCert | completeness _ _ _ _ h
... | success _ | refl = refl
Computational-CERT .completeness ce cs
dCert@(deregdrep c _) cs' (CERT-vdel h)
with computeProof ce (gState cs) dCert | completeness _ _ _ _ h
... | success _ | refl = refl
Computational-CERT .completeness ce cs
dCert@(ccreghot c mkh) cs' (CERT-vdel h)
with computeProof ce (gState cs) dCert | completeness _ _ _ _ h
... | success _ | refl = refl
Computational-PRE-CERT : Computational _⊢_⇀⦇_,PRE-CERT⦈_ String
Computational-PRE-CERT .computeProof ce cs _ =
let open CertEnv ce; open PParams pp
open GState (gState cs); open DState (dState cs)
refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList votes)
refreshedDReps = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh
in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
× mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
(yes p) → success (-, CERT-pre p)
(no ¬p) → failure (genErrors ¬p)
Computational-PRE-CERT .completeness ce st _ st' (CERT-pre p)
rewrite let dState = CertState.dState st; open DState dState in
dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
× mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
p .proj₂ = refl
Computational-POST-CERT : Computational _⊢_⇀⦇_,POST-CERT⦈_ String
Computational-POST-CERT .computeProof ce cs tt = success ( cs' , CERT-post)
where
dreps : DReps
dreps = GState.dreps (gState cs)
validVoteDelegs : VoteDelegs
validVoteDelegs = (VoteDelegsOf cs) ∣^ ( mapˢ vDelegCredential (dom dreps) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )
cs' : CertState
cs' = $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#8617}{\htmlId{8820}{\htmlClass{Function}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#2193}{\htmlId{8838}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#8507}{\htmlId{8852}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#2028}{\htmlId{8857}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#8507}{\htmlId{8867}{\htmlClass{Bound}{\text{cs}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#5098}{\htmlId{8874}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#8507}{\htmlId{8883}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#5206}{\htmlId{8888}{\htmlClass{Field}{\text{GStateOf}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.Computational.html#8507}{\htmlId{8897}{\htmlClass{Bound}{\text{cs}}}}\, \end{pmatrix}$
Computational-POST-CERT .completeness ce cs _ cs' CERT-post = refl
Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
Computational-CERTS = it