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.String as S open GovStructure govStructure open RewardAddress open Computational ⦃...⦄ open StakePoolParams open PoolEnv open PParams private instance _ = IsBLSUnique? 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 ¿ IsVRFUnique (poolParams .vrf) (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∙ IsBLSUnique (proj₁ <$> poolParams .bls) (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ | dec ⦃ IsValidBLSPoP? {poolParams .bls} ⦄ ... | yes (q₁ , q₂ , q₃ , q₄) | yes r = success (-, POOL-rereg (p , q₁ , q₂ , r , q₃ , q₄)) ... | yes (q₁ , q₂ , q₃ , q₄) | no ¬r = failure (genErrors ¬r) ... | no ¬q | no ¬r = failure (genErrors ¬q S.++ genErrors ¬r) ... | no ¬q | yes _ = failure (genErrors ¬q) Computational-POOL .computeProof Γ stᵖ (regpool c poolParams) | no ¬p with ¿ IsVRFUnique (poolParams .vrf) (PoolsOf stᵖ) (FuturePoolsOf stᵖ) ∙ IsBLSUnique (proj₁ <$> poolParams .bls) (PoolsOf stᵖ) (FuturePoolsOf stᵖ) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ | dec ⦃ IsValidBLSPoP? {poolParams .bls} ⦄ ... | yes (q₁ , q₂ , q₃ , q₄) | yes r = success (-, POOL-reg (¬p , q₁ , q₂ , r , q₃ , q₄)) ... | yes (q₁ , q₂ , q₃ , q₄) | no ¬r = failure (genErrors ¬r) ... | no ¬q | no ¬r = failure (genErrors ¬q S.++ genErrors ¬r) ... | no ¬q | yes _ = 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₁ , q₂ , r , q₃ , q₄)) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ ... | yes r = ⊥-elim (p r) ... | no ¬q with ¿ IsVRFUnique (poolParams .vrf) (PoolsOf stᵖ) (FuturePoolsOf stᵖ) ∙ IsBLSUnique (proj₁ <$> (poolParams .bls)) (PoolsOf stᵖ) (FuturePoolsOf stᵖ) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ | dec ⦃ IsValidBLSPoP? {poolParams .bls} ⦄ ... | yes _ | yes _ = refl ... | yes _ | no ¬r = ⊥-elim (¬r r) ... | no ¬s | yes _ = ⊥-elim (¬s (q₁ , q₂ , q₃ , q₄)) ... | no ¬s | no _ = ⊥-elim (¬s (q₁ , q₂ , q₃ , q₄)) Computational-POOL .completeness Γ stᵖ (regpool c poolParams) _ (POOL-rereg (p , q₁ , q₂ , r , q₃ , q₄)) with ¿ IsPoolRegistered (PoolsOf stᵖ) c ¿ ... | no ¬r = ⊥-elim (¬r p) ... | yes _ with ¿ IsVRFUnique (poolParams .vrf) (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∙ IsBLSUnique (proj₁ <$> poolParams .bls) (PoolsOf stᵖ ∣ ❴ c ❵ ᶜ) (FuturePoolsOf stᵖ ∣ ❴ c ❵ ᶜ) ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId ∙ Γ .pp .minPoolCost ≤ poolParams .cost ¿ | dec ⦃ IsValidBLSPoP? {poolParams .bls} ⦄ ... | yes _ | yes _ = refl ... | yes _ | no ¬r = ⊥-elim (¬r r) ... | no ¬s | yes _ = ⊥-elim (¬s (q₁ , q₂ , q₃ , q₄)) ... | no ¬s | no _ = ⊥-elim (¬s (q₁ , q₂ , q₃ , 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#7759}{\htmlId{7725}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7689}{\htmlId{7735}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5677}{\htmlId{7740}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7692}{\htmlId{7748}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{7753}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7757}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{7758}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7692}{\htmlId{7766}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{7768}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert | computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6810}{\htmlId{7818}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7689}{\htmlId{7826}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#7759}{\htmlId{7831}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7689}{\htmlId{7841}{\htmlClass{Bound}{\text{ce}}}}\, \end{pmatrix}$ (PStateOf cs) dCert | computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6810}{\htmlId{7892}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7689}{\htmlId{7900}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#7759}{\htmlId{7905}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7689}{\htmlId{7915}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5546}{\htmlId{7920}{\htmlClass{Field}{\text{ColdCredentialsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7689}{\htmlId{7938}{\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#7759}{\htmlId{8460}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8380}{\htmlId{8470}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5677}{\htmlId{8475}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8383}{\htmlId{8483}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{8488}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8492}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{8493}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8383}{\htmlId{8501}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{8503}{\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#7759}{\htmlId{8699}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8628}{\htmlId{8709}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5677}{\htmlId{8714}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8631}{\htmlId{8722}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{8727}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8731}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{8732}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8631}{\htmlId{8740}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{8742}{\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#6810}{\htmlId{8948}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8867}{\htmlId{8956}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#7759}{\htmlId{8961}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#8867}{\htmlId{8971}{\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#6810}{\htmlId{9167}{\htmlClass{Field}{\text{EpochOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#9092}{\htmlId{9175}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.PParams.html#7759}{\htmlId{9180}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#9092}{\htmlId{9190}{\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