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.Data.Maybe open import stdlib-meta.Tactic.GenError using (genErrors) import Data.Maybe.Relation.Unary.Any as M import Data.Maybe.Relation.Unary.All as M open GovStructure govStructure open RewardAddress open Inverse open Computational ⦃...⦄ private lookupᵐ?? : {K V : Type} → ⦃ _ : DecEq K ⦄ → (m : K ⇀ V) (k : K) → Dec (Any (λ (k' , _) → k ≡ k') (m ˢ)) lookupᵐ?? m k = any? (λ { _ → ¿ _ ¿ }) (m ˢ) 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 md) → case lookupᵐ?? (DepositsOf ds) c of λ where (yes ((_ , d) , _ , _)) → case ¿ (c , 0) ∈ (RewardsOf ds) × (c , d) ∈ (DepositsOf ds) × (md ≡ nothing ⊎ md ≡ just d) ¿ of λ where (yes q) → success (-, DELEG-dereg q) (no ¬q) → failure (genErrors ¬q) (no ¬p) → failure (genErrors ¬p) _ → 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 nothing) _ (DELEG-dereg {d = d} h@(p , q , r)) with lookupᵐ?? (DepositsOf ds) c ... | (yes ((_ , d') , s₂ , refl)) rewrite dec-yes (¿ (c , 0) ∈ (RewardsOf ds) × (c , d') ∈ (DepositsOf ds) × (nothing ≡ nothing {A = ℕ} ⊎ nothing ≡ just d') ¿) (p , s₂ , inj₁ refl) .proj₂ = refl Computational-DELEG .completeness _ ds (dereg c nothing) _ (DELEG-dereg h@(p , q , r)) | (no ¬s) = ⊥-elim (¬s (_ , q , refl)) Computational-DELEG .completeness _ ds (dereg c (just d)) _ (DELEG-dereg h@(p , q , inj₂ refl)) with lookupᵐ?? (DepositsOf ds) c ... | (yes ((_ , d') , q' , refl)) rewrite dec-yes (¿ (c , 0) ∈ (RewardsOf ds) × (c , d') ∈ (DepositsOf ds) × (just d ≡ nothing {A = ℕ} ⊎ just d ≡ just d') ¿) (p , q' , inj₂ (cong just (proj₂ (DepositsOf ds) q q'))) .proj₂ = refl ... | (no ¬s) = ⊥-elim (¬s (_ , q , refl)) Computational-POOL : Computational _⊢_⇀⦇_,POOL⦈_ String Computational-POOL .computeProof _ stᵖ (regpool c _) with ¿ Is-just (lookupᵐ? (PoolsOf stᵖ) c) ¿ ... | yes p = success (-, (POOL-rereg p)) ... | no ¬p = success (-, (POOL-reg (¬Is-just↔Is-nothing _ .to ¬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 ¿ Is-just (lookupᵐ? (PoolsOf stᵖ) c) ¿ ... | yes p' = ⊥-elim (¬Is-just↔Is-nothing _ .from p p') ... | no _ = refl Computational-POOL .completeness _ stᵖ (regpool c _) _ (POOL-rereg p) with ¿ Is-just (lookupᵐ? (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 ∈ CertEnv.coldCreds 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 ∈ CertEnv.coldCreds 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{6149}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6113}{\htmlId{6159}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3501}{\htmlId{6164}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6116}{\htmlId{6172}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6177}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6181}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5421}{\htmlId{6182}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6116}{\htmlId{6190}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6192}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ (DStateOf cs) dCert | computeProof (PParamsOf ce) (PStateOf cs) dCert | computeProof ce (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{6830}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6750}{\htmlId{6840}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3501}{\htmlId{6845}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6753}{\htmlId{6853}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6858}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6862}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5421}{\htmlId{6863}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6753}{\htmlId{6871}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{6873}{\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{7069}{\htmlClass{Field}{\text{PParamsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#6998}{\htmlId{7079}{\htmlClass{Bound}{\text{ce}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3501}{\htmlId{7084}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7001}{\htmlId{7092}{\htmlClass{Bound}{\text{cs}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{7097}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7101}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5421}{\htmlId{7102}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.Properties.Computational.html#7001}{\htmlId{7110}{\htmlClass{Bound}{\text{cs}}}}\,\,\htmlId{7112}{\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 Γ (CertState.gState cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERT .completeness Γ cs dCert@(deregdrep c _) cs' (CERT-gov h) with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERT .completeness Γ cs dCert@(ccreghot c mkh) cs' (CERT-gov h) with computeProof Γ (CertState.gState cs) dCert | completeness _ _ _ _ h ... | success _ | refl = refl Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String Computational-CERTS = it