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#6243}{\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#2912}{\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#6022}{\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#5303}{\htmlId{1960}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{1971}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#6367}{\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#6475}{\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#5420}{\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#5303}{\htmlId{2103}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{2114}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#6583}{\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#888}{\htmlId{2761}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#924}{\htmlId{2771}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#962}{\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#888}{\htmlId{3871}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#924}{\htmlId{3881}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#962}{\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 startingAccountBalanceIntervals = StartingBalanceIntervalsOf 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{5424}{\htmlClass{Field}{\text{VoteDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5437}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6243}{\htmlId{5442}{\htmlClass{Field}{\text{StakeDelegsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5456}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#2912}{\htmlId{5461}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4909}{\htmlId{5478}{\htmlClass{Bound}{\text{withdrawals}}}}\, \,\htmlId{5490}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#6022}{\htmlId{5491}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5501}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{5503}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5303}{\htmlId{5507}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{5518}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#6367}{\htmlId{5519}{\htmlClass{Field}{\text{DStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5528}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{5530}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6475}{\htmlId{5551}{\htmlClass{Field}{\text{PStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5560}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4654}{\htmlId{5582}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5420}{\htmlId{5616}{\htmlClass{Field}{\text{CCHotKeysOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5628}{\htmlClass{Bound}{\text{s₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5303}{\htmlId{5650}{\htmlClass{Field}{\text{DepositsOf}}}}\, \,\htmlId{5661}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#6583}{\htmlId{5662}{\htmlClass{Field}{\text{GStateOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Entities.Properties.Computational.html#4439}{\htmlId{5671}{\htmlClass{Bound}{\text{s₀}}}}\,\,\htmlId{5673}{\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) ∙ dom startingAccountBalanceIntervals ⊆ dom Γ.rewards₀ ∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? Γ.rewards₀ c)) interval) ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#654}{\htmlId{6953}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#690}{\htmlId{6963}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#728}{\htmlId{6970}{\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₇ , 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 , 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 , 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) ∙ dom startingAccountBalanceIntervals ⊆ dom Γ.rewards₀ ∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? Γ.rewards₀ c)) interval) ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Entities.html#654}{\htmlId{8768}{\htmlClass{Function}{\text{Γ.epoch}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#690}{\htmlId{8778}{\htmlClass{Function}{\text{Γ.pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Entities.html#728}{\htmlId{8785}{\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₇ , p₈ , p₉)) ... | yes _ | failure e | () ... | yes _ | success (s₂ , p) | refl with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿ ... | no ¬p = ⊥-elim (¬p p₁₀) ... | yes _ = refl