Computational
{-# OPTIONS --safe #-} open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure) module Ledger.Dijkstra.Specification.Certs.Properties.Computational (govStructure : GovStructure) where open import Ledger.Prelude open import Ledger.Dijkstra.Specification.Gov.Actions govStructure hiding (yes; no) open import Ledger.Dijkstra.Specification.Certs govStructure open import stdlib-meta.Tactic.GenError using (genErrors) import Data.Maybe.Relation.Unary.Any as M open GovStructure govStructure open RewardAddress open Computational ⦃...⦄ instance Computational-DELEG : Computational _⊢_⇀⦇_,DELEG⦈_ String Computational-DELEG .computeProof de ds = λ where (delegate c mv mc d) → case ¿ (c ∉ dom (RewardsOf ds) → d ≡ DelegEnv.pparams de .PParams.keyDeposit) × (c ∈ dom (RewardsOf ds) → d ≡ 0) × mv ∈ mapˢ (just ∘ vDelegCredential) (DelegEnv.delegatees de) ∪ fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] ) × mc ∈ mapˢ just (dom (DelegEnv.pools de)) ∪ ❴ nothing ❵ ¿ of λ where (yes p) → success (-, DELEG-delegate p) (no ¬p) → failure (genErrors ¬p) (dereg c d) → case ¿ (c , 0) ∈ (RewardsOf ds) × (c , d) ∈ (DepositsOf ds) ¿ of λ where (yes q) → success (-, DELEG-dereg q) (no ¬q) → failure (genErrors ¬q) _ → failure "Unexpected certificate in DELEG" Computational-DELEG .completeness de ds (delegate c mv mc d) s' (DELEG-delegate p) rewrite dec-yes (¿ (c ∉ dom (RewardsOf ds) → d ≡ DelegEnv.pparams de .PParams.keyDeposit) × (c ∈ dom (RewardsOf ds) → 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 _ ds (dereg c d) _ (DELEG-dereg (p , q)) with ¿ (c , 0) ∈ (RewardsOf ds) × (c , d) ∈ (DepositsOf ds) ¿ ... | yes p = refl ... | no ¬p = ⊥-elim (¬p (p , q)) Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String Computational-POOL .computeProof _ stᵖ (regpool c _) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ ... | yes p = success (-, (POOL-rereg p)) ... | no ¬p = success (-, (POOL-reg ¬p)) Computational-POOL .computeProof _ stᵖ (retirepool c e) = success (-, POOL-retirepool) Computational-POOL .computeProof _ stᵖ _ = failure "Unexpected certificate in POOL" Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-reg p) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ ... | yes p' = ⊥-elim (p p') ... | no _ = refl Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-rereg p) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ ... | yes _ = refl ... | no ¬p = ⊥-elim (¬p p) Computational-POOL .completeness _ _ (retirepool _ _) _ POOL-retirepool = refl Computational-GOVCERT : Computational _⊢_⇀⦇_,GOVCERT⦈_ String Computational-GOVCERT .computeProof ce gs (regdrep c d _) = case ¿ d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf gs) ⊎ d ≡ 0 × c ∈ dom (DRepsOf gs) ¿ of λ where (yes p) → success (-, GOVCERT-regdrep p) (no ¬p) → failure (genErrors ¬p) Computational-GOVCERT .computeProof ce gs (deregdrep c d) = case ¿ c ∈ dom (DRepsOf gs) × (c , d) ∈ (DepositsOf gs) ¿ of λ where (yes p) → success (-, GOVCERT-deregdrep p) (no ¬p) → failure (genErrors ¬p) Computational-GOVCERT .computeProof ce gs (ccreghot c _) = case ¿ ((c , nothing) ∉ CCHotKeysOf gs ˢ) × c ∈ ColdCredentialsOf ce ¿ 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 gs (regdrep c d _) _ (GOVCERT-regdrep p) rewrite dec-yes ¿ (d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf gs)) ⊎ (d ≡ 0 × c ∈ dom (DRepsOf gs)) ¿ p .proj₂ = refl Computational-GOVCERT .completeness _ gs (deregdrep c d) _ (GOVCERT-deregdrep p) rewrite dec-yes ¿ c ∈ dom (DRepsOf gs) × (c , d) ∈ (DepositsOf gs) ¿ p .proj₂ = refl Computational-GOVCERT .completeness ce gs (ccreghot c _) _ (GOVCERT-ccreghot p) rewrite dec-yes ¿ (c , nothing) ∉ CCHotKeysOf gs ˢ × c ∈ ColdCredentialsOf ce ¿ p .proj₂ = refl Computational-CERT : Computational _⊢_⇀⦇_,CERT⦈_ String Computational-CERT .computeProof ce cs dCert with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PParams.html#5406}{\htmlId{4902}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4866}{\htmlId{4912}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4286}{\htmlId{4917}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4869}{\htmlId{4925}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4930}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4934}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{4935}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4869}{\htmlId{4943}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{4945}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert | computeProof (PParamsOf ce) (PStateOf cs) dCert | computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5296}{\htmlId{5054}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4866}{\htmlId{5062}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5406}{\htmlId{5067}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4866}{\htmlId{5077}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4155}{\htmlId{5082}{\htmlClass{Field}{\text{ColdCredentialsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4866}{\htmlId{5100}{\htmlClass{Bound}{\text{ce}}}}\, \end{pmatrix}$ (GStateOf cs) dCert ... | success (_ , h) | _ | _ = success (-, CERT-deleg h) ... | failure _ | success (_ , h) | _ = success (-, CERT-pool h) ... | failure _ | failure _ | success (_ , h) = success (-, CERT-gov h) ... | failure e₁ | failure e₂ | failure e₃ = failure $ "DELEG: " <> e₁ <> "\nPOOL: " <> e₂ <> "\nGOV: " <> e₃ Computational-CERT .completeness ce cs dCert@(delegate c mv mc d) cs' (CERT-deleg h) with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.PParams.html#5406}{\htmlId{5633}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5553}{\htmlId{5643}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4286}{\htmlId{5648}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5556}{\htmlId{5656}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5661}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5665}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{5666}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5556}{\htmlId{5674}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5676}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf 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.Dijkstra.Specification.PParams.html#5406}{\htmlId{5872}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5801}{\htmlId{5882}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4286}{\htmlId{5887}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5804}{\htmlId{5895}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5900}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5904}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{5905}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5804}{\htmlId{5913}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5915}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERT .completeness ce cs dCert@(regpool c poolParams) cs' (CERT-pool h) with computeProof (CertEnv.pp ce) (CertState.pState cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERT .completeness ce cs dCert@(retirepool c e) cs' (CERT-pool h) with completeness _ _ _ _ h ... | refl = refl Computational-CERT .completeness Γ cs dCert@(regdrep c _ _) cs' (CERT-gov h) with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5296}{\htmlId{6469}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6397}{\htmlId{6477}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5406}{\htmlId{6481}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6397}{\htmlId{6491}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4155}{\htmlId{6495}{\htmlClass{Field}{\text{ColdCredentialsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6397}{\htmlId{6513}{\htmlClass{Bound}{\text{Γ}}}}\, \end{pmatrix}$ (CertState.gState cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERT .completeness Γ cs dCert@(deregdrep c _) cs' (CERT-gov h) with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5296}{\htmlId{6709}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6637}{\htmlId{6717}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5406}{\htmlId{6721}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6637}{\htmlId{6731}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4155}{\htmlId{6735}{\htmlClass{Field}{\text{ColdCredentialsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6637}{\htmlId{6753}{\htmlClass{Bound}{\text{Γ}}}}\, \end{pmatrix}$ (CertState.gState cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERT .completeness Γ cs dCert@(ccreghot c mkh) cs' (CERT-gov h) with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5296}{\htmlId{6950}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6877}{\htmlId{6958}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5406}{\htmlId{6962}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6877}{\htmlId{6972}{\htmlClass{Bound}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4155}{\htmlId{6976}{\htmlClass{Field}{\text{ColdCredentialsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6877}{\htmlId{6994}{\htmlClass{Bound}{\text{Γ}}}}\, \end{pmatrix}$ (CertState.gState cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String Computational-CERTS = it