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 cs (regdrep c d _) = case ¿ d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf cs) ⊎ d ≡ 0 × c ∈ dom (DRepsOf cs) ¿ of λ where (yes p) → success (-, GOVCERT-regdrep p) (no ¬p) → failure (genErrors ¬p) Computational-GOVCERT .computeProof ce cs (deregdrep c d) = case ¿ c ∈ dom (DRepsOf cs) × (c , d) ∈ (DepositsOf (GStateOf cs)) ¿ of λ where (yes p) → success (-, GOVCERT-deregdrep p) (no ¬p) → failure (genErrors ¬p) Computational-GOVCERT .computeProof ce cs (ccreghot c _) = case ¿ ((c , nothing) ∉ CCHotKeysOf cs ˢ) × 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 cs (regdrep c d _) _ (GOVCERT-regdrep p) rewrite dec-yes ¿ (d ≡ PParams.drepDeposit (PParamsOf ce) × c ∉ dom (DRepsOf cs)) ⊎ (d ≡ 0 × c ∈ dom (DRepsOf cs)) ¿ p .proj₂ = refl Computational-GOVCERT .completeness _ cs (deregdrep c d) _ (GOVCERT-deregdrep p) rewrite dec-yes ¿ c ∈ dom (DRepsOf cs) × (c , d) ∈ (DepositsOf (GStateOf cs)) ¿ p .proj₂ = refl Computational-GOVCERT .completeness ce cs (ccreghot c _) _ (GOVCERT-ccreghot p) rewrite dec-yes ¿ (c , nothing) ∉ CCHotKeysOf cs ˢ × 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{4924}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4888}{\htmlId{4934}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4286}{\htmlId{4939}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4891}{\htmlId{4947}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4952}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4956}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{4957}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4891}{\htmlId{4965}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{4967}{\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{5076}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4888}{\htmlId{5084}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5406}{\htmlId{5089}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4888}{\htmlId{5099}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4155}{\htmlId{5104}{\htmlClass{Field}{\text{ColdCredentialsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#4888}{\htmlId{5122}{\htmlClass{Bound}{\text{ce}}}}\, \end{pmatrix}$ 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{5644}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5564}{\htmlId{5654}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4286}{\htmlId{5659}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5567}{\htmlId{5667}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5672}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5676}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{5677}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5567}{\htmlId{5685}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5687}{\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{5883}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5812}{\htmlId{5893}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4286}{\htmlId{5898}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5815}{\htmlId{5906}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{5911}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{5915}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{5916}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#5815}{\htmlId{5924}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{5926}{\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 (regdrep c d an) _ (CERT-gov (GOVCERT-regdrep p)) rewrite dec-yes ¿ (d ≡ PParams.drepDeposit (PParamsOf Γ) × c ∉ dom (DRepsOf cs)) ⊎ (d ≡ 0 × c ∈ dom (DRepsOf cs)) ¿ p .proj₂ = refl Computational-CERT .completeness Γ cs (deregdrep c d) _ (CERT-gov (GOVCERT-deregdrep p)) rewrite dec-yes ¿ c ∈ dom (DRepsOf cs) × (c , d) ∈ (DepositsOf (GStateOf cs)) ¿ p .proj₂ = refl Computational-CERT .completeness Γ cs (ccreghot c mc) _ (CERT-gov (GOVCERT-ccreghot p)) rewrite dec-yes ¿ (c , nothing) ∉ CCHotKeysOf cs ˢ × c ∈ ColdCredentialsOf Γ ¿ p .proj₂ = refl Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String Computational-CERTS = it