Computational
{-# OPTIONS --safe #-} open import Ledger.Dijkstra.Specification.Transaction using (TransactionStructure) module Ledger.Dijkstra.Specification.Entities.Properties.Computational (txs : TransactionStructure) (open TransactionStructure txs) where open import Ledger.Prelude open import Ledger.Dijkstra.Specification.Certs govStructure open import Ledger.Dijkstra.Specification.Entities txs open import Ledger.Dijkstra.Specification.Gov govStructure open import Ledger.Dijkstra.Specification.Certs.Properties.Computational 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 RewardAddress open GovVote module Computational-CERTS = Computational Computational-CERTS instance Computational-SUBENTITIES : Computational _⊢_⇀⦇_,SUBENTITIES⦈_ String Computational-SUBENTITIES = record {go} where module go (Γ : SubEntitiesEnv) (s₀ : CertState) (txSub : SubLevelTx) (let module Γ = SubEntitiesEnv Γ refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txSub)) refreshedDReps = mapValueRestricted (const (Γ.epoch + Γ.pp .PParams.drepActivity)) (DRepsOf s₀) refresh withdrawals = WithdrawalsOf txSub withdrawalsCredentials = mapˢ stake (dom withdrawals) accountBalanceIntervals = BalanceIntervalsOf txSub directDeposits = DirectDepositsOf txSub directDepositsCredentials = mapˢ stake (dom directDeposits) ) where s₁ : CertState s₁ = $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4773}{\htmlId{1877}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1112}{\htmlId{1890}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4729}{\htmlId{1895}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1112}{\htmlId{1909}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#2911}{\htmlId{1914}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1458}{\htmlId{1931}{\htmlClass{Bound}{\text{withdrawals}}}}\, \,\htmlId{1943}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4508}{\htmlId{1944}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1112}{\htmlId{1954}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{1956}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3912}{\htmlId{1960}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{1971}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4853}{\htmlId{1972}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1112}{\htmlId{1981}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{1983}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4961}{\htmlId{2004}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1112}{\htmlId{2013}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1330}{\htmlId{2035}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4029}{\htmlId{2069}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1112}{\htmlId{2081}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3912}{\htmlId{2103}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{2114}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#5069}{\htmlId{2115}{\htmlClass{Field}{\text{GStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#1112}{\htmlId{2124}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{2126}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \end{pmatrix}$ computeProof : ComputationResult String (∃-syntax (_⊢_⇀⦇_,SUBENTITIES⦈_ Γ s₀ txSub)) computeProof with ¿ ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀ ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀) ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀) ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval) ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#887}{\htmlId{2761}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#923}{\htmlId{2771}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#961}{\htmlId{2778}{\htmlClass{Function}{\text{Γ.coldCredentials}}}}\, \end{pmatrix}$ s₁ (DCertsOf txSub) ... | no ¬p | _ = failure "" ... | yes _ | failure e = failure e ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p) with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿ ... | no ¬p = failure "" ... | yes p₇ = success (-, (SUBENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p , p₆ , p₇))) completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ txSub ,SUBENTITIES⦈ s' → map proj₁ computeProof ≡ success s' completeness s' (SUBENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p , p₆ , p₇)) with ¿ ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀ ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀) ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀) ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval) ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#887}{\htmlId{3871}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#923}{\htmlId{3881}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#961}{\htmlId{3888}{\htmlClass{Function}{\text{Γ.coldCredentials}}}}\, \end{pmatrix}$ s₁ (DCertsOf txSub) | Computational-CERTS.completeness _ _ _ _ p ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆)) ... | yes _ | failure e | () ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p) | refl with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿ ... | no ¬p = ⊥-elim (¬p p₇) ... | yes _ = refl Computational-ENTITIES : Computational _⊢_⇀⦇_,ENTITIES⦈_ String Computational-ENTITIES = record {go} where module go (Γ : EntitiesEnv) (s₀ : CertState) (txTop : TopLevelTx) (let module Γ = EntitiesEnv Γ refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop)) refreshedDReps = mapValueRestricted (const (Γ.epoch + Γ.pp .PParams.drepActivity)) (DRepsOf s₀) refresh withdrawalsSubTxs = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop) withdrawals = WithdrawalsOf txTop withdrawalsCredentials = mapˢ stake (dom withdrawals) accountBalanceIntervals = BalanceIntervalsOf txTop directDeposits = DirectDepositsOf txTop directDepositsCredentials = mapˢ stake (dom directDeposits) ) where s₁ : CertState s₁ = $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#4773}{\htmlId{5336}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5349}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4729}{\htmlId{5354}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5368}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#2911}{\htmlId{5373}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4909}{\htmlId{5390}{\htmlClass{Bound}{\text{withdrawals}}}}\, \,\htmlId{5402}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4508}{\htmlId{5403}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5413}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{5415}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3912}{\htmlId{5419}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{5430}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#4853}{\htmlId{5431}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5440}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{5442}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4961}{\htmlId{5463}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5472}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4654}{\htmlId{5494}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#4029}{\htmlId{5528}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5540}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#3912}{\htmlId{5562}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{5573}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#5069}{\htmlId{5574}{\htmlClass{Field}{\text{GStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5583}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{5585}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \end{pmatrix}$ computeProof : ComputationResult String (∃-syntax (_⊢_⇀⦇_,ENTITIES⦈_ Γ s₀ txTop)) computeProof with ¿ ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀) ∙ (Γ.legacyMode ≡ true → ∙ ∀[ (addr , amt) ∈ withdrawals ˢ ] amt ≡ maybe id 0 (lookupᵐ? (RewardsOf s₀) (stake addr)) ∙ ∀[ (addr , amt) ∈ withdrawalsSubTxs ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr))) ∙ (Γ.legacyMode ≡ false → ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀ ∙ ∀[ (addr , amt) ∈ (withdrawalsSubTxs ∪⁺ withdrawals) ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr))) ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀) ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval) ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#653}{\htmlId{6645}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#689}{\htmlId{6655}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#727}{\htmlId{6662}{\htmlClass{Function}{\text{Γ.coldCredentials}}}}\, \end{pmatrix}$ s₁ (DCertsOf txTop) ... | no ¬p | _ = failure "" ... | yes _ | failure e = failure e ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇) | success (s₂ , p) with ¿ ∙ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿ ... | no ¬p = failure "" ... | yes p₈ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈))) completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ txTop ,ENTITIES⦈ s' → map proj₁ computeProof ≡ success s' completeness s' (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈)) with ¿ ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀) ∙ (Γ.legacyMode ≡ true → ∙ ∀[ (addr , amt) ∈ withdrawals ˢ ] amt ≡ maybe id 0 (lookupᵐ? (RewardsOf s₀) (stake addr)) ∙ ∀[ (addr , amt) ∈ withdrawalsSubTxs ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr))) ∙ (Γ.legacyMode ≡ false → ∙ withdrawalsCredentials ⊆ dom Γ.rewards₀ ∙ ∀[ (addr , amt) ∈ (withdrawalsSubTxs ∪⁺ withdrawals) ˢ ] amt ≤ maybe id 0 (lookupᵐ? Γ.rewards₀ (stake addr))) ∙ dom accountBalanceIntervals ⊆ dom (RewardsOf s₀) ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval) ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#653}{\htmlId{8207}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#689}{\htmlId{8217}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#727}{\htmlId{8224}{\htmlClass{Function}{\text{Γ.coldCredentials}}}}\, \end{pmatrix}$ s₁ (DCertsOf txTop) | Computational-CERTS.completeness _ _ _ _ p ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇)) ... | yes _ | failure e | () ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p) | refl with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿ ... | no ¬p = ⊥-elim (¬p p₈) ... | yes _ = refl