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 ⦃...⦄ open StakePoolParams open PoolEnv open PParams 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 poolParams) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ Computational-POOL .computeProof Γ stᵖ (regpool c poolParams) | yes p with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∪ range (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ))) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ ... | yes q = success (-, POOL-rereg (p , q)) ... | no ¬q = failure (genErrors ¬q) Computational-POOL .computeProof Γ stᵖ (regpool c poolParams) | no ¬p with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ) ∪ range (FuturePoolsOf stᵖ))) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ ... | yes q = success (-, (POOL-reg (¬p , q))) ... | no ¬q = failure (genErrors ¬q) Computational-POOL .computeProof Γ stᵖ (retirepool c e') with ¿ IsPoolRegistered (PoolsOf stᵖ) c ∙ Γ .epoch < e' ∙ e' ≤ Γ .epoch + Γ .pp .Emax ¿ ... | yes p = success (-, POOL-retirepool p) ... | no ¬q = failure (genErrors ¬q) Computational-POOL .computeProof _ stᵖ _ = failure "Unexpected certificate in POOL" Computational-POOL .completeness Γ stᵖ (regpool c poolParams) _ (POOL-reg (p , q)) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ ... | yes r = ⊥-elim (p r) ... | no ¬r with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ) ∪ range (FuturePoolsOf stᵖ))) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ ... | yes _ = refl ... | no ¬s = ⊥-elim (¬s q) Computational-POOL .completeness Γ stᵖ (regpool c poolParams) _ (POOL-rereg (p , q)) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ ... | no ¬r = ⊥-elim (¬r p) ... | yes r with ¿ ¬ (poolParams .vrf ∈ mapˢ vrf (range (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∪ range (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ))) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ ... | yes _ = refl ... | no ¬s = ⊥-elim (¬s q) Computational-POOL .completeness Γ stᵖ (retirepool c e) _ (POOL-retirepool p) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ∙ Γ .epoch < e ∙ e ≤ Γ .epoch + Γ .pp .Emax ¿ ... | yes _ = refl ... | no ¬q = ⊥-elim (¬q p) 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#5447}{\htmlId{6518}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6482}{\htmlId{6528}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4398}{\htmlId{6533}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6485}{\htmlId{6541}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6546}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6550}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{6551}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6485}{\htmlId{6559}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6561}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert | computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5530}{\htmlId{6611}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6482}{\htmlId{6619}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5447}{\htmlId{6624}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6482}{\htmlId{6634}{\htmlClass{Bound}{\text{ce}}}}\, \end{pmatrix}$ (PStateOf cs) dCert | computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5530}{\htmlId{6685}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6482}{\htmlId{6693}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5447}{\htmlId{6698}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6482}{\htmlId{6708}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4267}{\htmlId{6713}{\htmlClass{Field}{\text{ColdCredentialsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6482}{\htmlId{6731}{\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#5447}{\htmlId{7253}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7173}{\htmlId{7263}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4398}{\htmlId{7268}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7176}{\htmlId{7276}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{7281}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7285}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{7286}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7176}{\htmlId{7294}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{7296}{\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#5447}{\htmlId{7492}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7421}{\htmlId{7502}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4398}{\htmlId{7507}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7424}{\htmlId{7515}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{7520}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7524}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{7525}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7424}{\htmlId{7533}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{7535}{\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 $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5530}{\htmlId{7741}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7660}{\htmlId{7749}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5447}{\htmlId{7754}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7660}{\htmlId{7764}{\htmlClass{Bound}{\text{ce}}}}\, \end{pmatrix}$ (PStateOf cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERT .completeness ce cs dCert@(retirepool c e) cs' (CERT-pool h) with computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#5530}{\htmlId{7960}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7885}{\htmlId{7968}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#5447}{\htmlId{7973}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7885}{\htmlId{7983}{\htmlClass{Bound}{\text{ce}}}}\, \end{pmatrix}$ (PStateOf cs) dCert | completeness _ _ _ _ h ... | success _ | 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