diff --git a/README.md b/README.md index ee2dbbd..ccbda0c 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,24 @@ -# ouroboros-praos-formal-spec +# An Agda formalization of the Ouroboros Praos consensus protocol + +## Overview + +This repository includes an Agda mechanization of the Ouroboros Praos consensus +protocol as specified in [[1]](#1). + +## Contents + +The repository contains the formalization of the consensus protocol and the corresponding safety proof, which are based on the work in [[2]](#2). ## Development -The repository provides a nix flake from which one can enter a development shell suitable for Agda using the following command: +You can enter a development shell suitable for Agda using the following command: ```bash -nix develop +nix-shell ``` +## References + +[1] David et al, Ouroboros Praos: An Adaptively-Secure, Semi-synchronous Proof-of-Stake Blockchain, _Advances in Cryptology – EUROCRYPT 2018 . EUROCRYPT 2018. Lecture Notes in Computer Science_, vol 10821, 2018. https://doi.org/10.1007/978-3-319-78375-8_3 + +[2] Thomsen and Spitters, Formalizing Nakamoto-Style Proof of Stake, _2021 IEEE 34th Computer Security Foundations Symposium (CSF)_, 2021. http://dx.doi.org/10.48550/arXiv.2007.12105 + diff --git a/default.nix b/default.nix index 823ed8c..04cb36a 100644 --- a/default.nix +++ b/default.nix @@ -16,24 +16,26 @@ let }; agdaStdlib = agdaPackages.standard-library.overrideAttrs (oldAttrs: { - version = "2.2"; + version = "2.3"; src = fetchFromGitHub { repo = "agda-stdlib"; owner = "agda"; - rev = "v2.2"; - hash = "sha256-/Fy5EOSbVNXt6Jq0yKSnlNPW4SYfn+eCTAYFnMZrbR0="; + rev = "v2.3"; + sha256 = "17w5vfn5pb2cgfs22zph3jfqnki52ja8y4zwyqj24zwf9rxairr4"; + url = "https://github.com/agda/agda-stdlib/archive/v2.3.tar.gz"; }; }); agdaStdlibClasses = agdaPackages.mkDerivation { inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; pname = "agda-stdlib-classes"; - version = "2.2.+"; + version = "2.3"; src = fetchFromGitHub { repo = "agda-stdlib-classes"; owner = "agda"; - rev = "aa62ce6348d39c554ef89487079871d5590e155e"; - sha256 = "sha256-I/g0BOdeAHVEtsfmPBICySOd6Jz5ymGUSE/G66EfHK8="; + rev = "v2.3"; + sha256 = "0bbgc3nf1b2v3wljrq7974z38apzzsdhfzc1fdmm4fsmnpglmb1m"; + url = "https://github.com/agda/agda-stdlib-classes/archive/v2.3.tar.gz"; }; meta = { }; libraryFile = "agda-stdlib-classes.agda-lib"; @@ -44,12 +46,13 @@ let agdaStdlibMeta = agdaPackages.mkDerivation { inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; pname = "agda-stdlib-meta"; - version = "2.2.+"; + version = "2.3"; src = fetchFromGitHub { repo = "agda-stdlib-meta"; owner = "agda"; - rev = "5ff853375180ef69f243ce72f2d3f6294bdb6aff"; - sha256 = "sha256-CNKEnDUToKEv+6Gaa8p5igLNpQDuasQ01JJLOXcU1bA="; + rev = "v2.3"; + sha256 = "1n41cfkahg2zzfm113dkqlh5m07rvm9jjh8ps50qi3cpkz203gla"; + url = "https://github.com/agda/agda-stdlib-meta/archive/v2.3.tar.gz"; }; meta = { }; libraryFile = "agda-stdlib-meta.agda-lib"; @@ -64,8 +67,9 @@ let src = fetchFromGitHub { repo = "agda-sets"; owner = "input-output-hk"; - rev = "f517d0d0c1ff1fd6dbac8b34309dea0e1aea6fc6"; - sha256 = "sha256-OsdDNNJp9NWDgDM0pDOGv98Z+vAS1U8mORWF7/B1D7k="; + rev = "31512b000317a577230e9ba5081b693801104851"; + sha256 = "1yj8a8r17y1pld87329cjvmfnha7ih5zan3wccc3sq661apr17l8"; + url = "https://github.com/input-output-hk/agda-sets/archive/31512b000317a577230e9ba5081b693801104851.tar.gz"; }; meta = { }; libraryFile = "abstract-set-theory.agda-lib"; @@ -76,17 +80,18 @@ let agdaIOGPrelude = agdaPackages.mkDerivation { inherit (locales) LANG LC_ALL LOCALE_ARCHIVE; pname = "agda-prelude"; - version = "2.0"; + version = ""; src = pkgs.fetchFromGitHub { repo = "iog-agda-prelude"; owner = "input-output-hk"; - rev = "main"; - sha256 = "sha256-PvfxcoK5MweXfdtbfDUTY23xsaAG093MbeX9fRac4sQ="; + rev = "e25670dcea694f321cbcd7a0bb704b82d5d7b266"; + sha256 = "1r2g7akia33yis8kgw398w0z484zry1q26739wcq6dfdyw7zb8v7"; + url = "https://github.com/input-output-hk/iog-agda-prelude/archive/e25670dcea694f321cbcd7a0bb704b82d5d7b266.tar.gz"; }; meta = { }; libraryFile = "iog-prelude.agda-lib"; everythingFile = "src/Everything.agda"; - buildInputs = [ agdaStdlib agdaStdlibClasses ]; + buildInputs = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta ]; }; deps = [ agdaStdlib agdaStdlibClasses agdaStdlibMeta agdaSets agdaIOGPrelude ]; diff --git a/nix/sources.json b/nix/sources.json index 4920120..c019bdb 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -5,10 +5,10 @@ "homepage": "", "owner": "NixOS", "repo": "nixpkgs", - "rev": "6c5963357f3c1c840201eda129a99d455074db04", - "sha256": "033fwpsm2a3f6sqr3qvy365sy3b89k13gczsa6m5xpz2axss02y9", + "rev": "5c004ab61f5c78e46a08270a66e1e5789c7e9d37", + "sha256": "0apjinygk0kn8gsixmp0l3yckdws6128a7ayygb8631mpglv73gr", "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/6c5963357f3c1c840201eda129a99d455074db04.tar.gz", + "url": "https://github.com/NixOS/nixpkgs/archive/5c004ab61f5c78e46a08270a66e1e5789c7e9d37.tar.gz", "url_template": "https://github.com///archive/.tar.gz" } } diff --git a/src/Data/List/Properties/Ext.agda b/src/Data/List/Properties/Ext.agda index 55b8055..fc72dd4 100644 --- a/src/Data/List/Properties/Ext.agda +++ b/src/Data/List/Properties/Ext.agda @@ -59,17 +59,17 @@ filter-∘-comm : (P? : Decidable P) (Q? : Decidable Q) → filter P? ∘ filter filter-∘-comm P? Q? [] = refl filter-∘-comm P? Q? (x ∷ xs) with ih ← filter-∘-comm P? Q? xs | does (P? x) in eqp | does (Q? x) in eqq ... | true | true rewrite eqp | eqq | ih = refl -... | true | false rewrite eqp | eqq | ih = refl -... | false | true rewrite eqp | eqq | ih = refl -... | false | false rewrite eqp | eqq | ih = refl +... | true | false rewrite eqq | ih = refl +... | false | true rewrite eqp | ih = refl +... | false | false rewrite ih = refl filter-∘-× : (P? : Decidable P) (Q? : Decidable Q) → filter (P? ∩? Q?) ≗ filter P? ∘ filter Q? filter-∘-× P? Q? [] = refl filter-∘-× P? Q? (x ∷ xs) with ih ← filter-∘-× P? Q? xs | does (P? x) in eqp | does (Q? x) in eqq -... | true | true rewrite eqp | eqq | ih = refl -... | true | false rewrite eqp | eqq | ih = refl -... | false | true rewrite eqp | eqq | ih = refl -... | false | false rewrite eqp | eqq | ih = refl +... | true | true rewrite eqp | ih = refl +... | true | false rewrite ih = refl +... | false | true rewrite eqp | ih = refl +... | false | false rewrite ih = refl filter-deduplicate-comm : ∀ ⦃ _ : DecEq A ⦄ {ℓ} {P : Pred A ℓ} {P? : Decidable P} → filter P? ∘ deduplicate _≟_ ≗ deduplicate _≟_ ∘ filter P? filter-deduplicate-comm [] = refl diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties/Ext.agda b/src/Data/List/Relation/Unary/AllPairs/Properties/Ext.agda index f67c2e1..16d474f 100644 --- a/src/Data/List/Relation/Unary/AllPairs/Properties/Ext.agda +++ b/src/Data/List/Relation/Unary/AllPairs/Properties/Ext.agda @@ -1,27 +1,20 @@ module Data.List.Relation.Unary.AllPairs.Properties.Ext where open import Level using (Level) -open import Function.Base using (_$_; _∘_) -open import Relation.Binary.PropositionalEquality.Core using (sym; subst) +open import Function.Base using (_∘_) +open import Relation.Binary.PropositionalEquality.Core using (subst) open import Relation.Binary.Core using (Rel) open import Data.Product using (proj₁; proj₂; _×_; _,_) -open import Data.List.Base using ([]; _∷_; _++_; _∷ʳ_; map) +open import Data.List.Base using ([]; _∷_; _++_; _∷ʳ_) open import Data.List.Properties using (++-identityʳ) open import Data.List.Relation.Unary.All as All using (All; []) -open import Data.List.Relation.Unary.All.Properties as All hiding (++⁻; map⁻) +open import Data.List.Relation.Unary.All.Properties as All hiding (++⁻) open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_) private variable - a b ℓ : Level - A B : Set a - --- TODO: Remove when upgrading to stdlib 2.3. -module _ {R : Rel A ℓ} {f : B → A} where - - map⁻ : ∀ {xs} → AllPairs R (map f xs) → AllPairs (λ x y → R (f x) (f y)) xs - map⁻ {[]} _ = [] - map⁻ {_ ∷ _} (x∉xs ∷ xs!) = All.map⁻ x∉xs ∷ map⁻ xs! + a ℓ : Level + A : Set a module _ {R : Rel A ℓ} where diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties/Ext.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties/Ext.agda index f1e510d..4d4661c 100644 --- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties/Ext.agda +++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties/Ext.agda @@ -42,11 +42,6 @@ private module _ {A : Set a} {B : Set b} where - -- TODO: Remove when upgrading to stdlib 2.3. - map⁻ : ∀ {f} → Congruent _≡_ _≡_ f → - ∀ {xs} → Unique (map f xs) → Unique xs - map⁻ = Setoid.map⁻ (setoid A) (setoid B) - map⁺-∈ : ∀ {xs} {f : A → B} → (∀ {x y} → x ∈ xs → y ∈ xs → f x ≡ f y → x ≡ y) → Unique xs → Unique (map f xs) map⁺-∈ inj [] = [] diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties/Ext.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties/Ext.agda index 1717a70..f1ad5c7 100644 --- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties/Ext.agda +++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties/Ext.agda @@ -2,29 +2,17 @@ module Data.List.Relation.Unary.Unique.Setoid.Properties.Ext where open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) -open import Relation.Nullary.Negation using (contraposition) open import Data.Product.Base using (_×_; _,_) -open import Data.List.Base using (map; _++_) +open import Data.List.Base using (_++_) open import Data.List.Relation.Unary.Unique.Setoid open import Data.List.Relation.Binary.Disjoint.Setoid -import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; map) -import Data.List.Relation.Unary.AllPairs.Properties.Ext as AllPairs using (map⁻; ++⁻) +import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs) +import Data.List.Relation.Unary.AllPairs.Properties.Ext as AllPairs using (++⁻) open import Data.List.Relation.Binary.Disjoint.Setoid.Properties.Ext using (AllAll⇒Disjoint) -open import Function.Definitions using (Congruent) private variable - a b ℓ ℓ₁ ℓ₂ : Level - --- TODO: Remove when upgrading to stdlib 2.3. -module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where - - open Setoid S renaming (_≈_ to _≈₁_) - open Setoid R renaming (_≈_ to _≈₂_) - - map⁻ : ∀ {f} → Congruent _≈₁_ _≈₂_ f → - ∀ {xs} → Unique R (map f xs) → Unique S xs - map⁻ cong fxs! = AllPairs.map (contraposition cong) (AllPairs.map⁻ fxs!) + a ℓ : Level module _ (S : Setoid a ℓ) where diff --git a/src/Prelude/AssocList/Properties/Ext.agda b/src/Prelude/AssocList/Properties/Ext.agda index d1ad7e5..54bc5a6 100644 --- a/src/Prelude/AssocList/Properties/Ext.agda +++ b/src/Prelude/AssocList/Properties/Ext.agda @@ -87,7 +87,7 @@ module _ ⦃ _ : DecEq K ⦄ where set-id-local : m ⁉ k ≡ just v → set ⦃ it ⦄ ⦃ Default-V ⦄ k v m ≡ m set-id-local {m} {k} p with k ∈ᵐ? m - ... | yes q rewrite dec-yes (k ∈ᵐ? m) q .proj₂ = updateAt-id-local m (L.First.index q) (×-≡,≡→≡ $ L.First.index-satisfied q ,′ (sym $ M.just-injective p)) + ... | yes q = updateAt-id-local m (L.First.index q) (×-≡,≡→≡ $ L.First.index-satisfied q ,′ (sym $ M.just-injective p)) ... | no _ = contradiction p λ() modify-modifies : ∀ {f : V → V} → m ⁉ k ≡ just v → modify k f m ⁉ k ≡ just (f v) diff --git a/src/Prelude/DecEq/Ext.agda b/src/Prelude/DecEq/Ext.agda deleted file mode 100644 index 20d1503..0000000 --- a/src/Prelude/DecEq/Ext.agda +++ /dev/null @@ -1,13 +0,0 @@ -module Prelude.DecEq.Ext where - -open import Function.Base using (_∋_) -open import Data.Maybe using (Maybe) -open import Prelude.DecEq using (DecEq) -open DecEq ⦃...⦄ - -instance - DecEq-Bool = DecEq _ ∋ record {DB} where import Data.Bool as DB - - DecEq-Maybe : ∀ {A : Set} ⦃ _ : DecEq A ⦄ → DecEq (Maybe A) - DecEq-Maybe ._≟_ = M.≡-dec _≟_ - where import Data.Maybe.Properties as M diff --git a/src/Properties/Base/BlockHistory.agda b/src/Properties/Base/BlockHistory.agda index 07b4877..33c03cd 100644 --- a/src/Properties/Base/BlockHistory.agda +++ b/src/Properties/Base/BlockHistory.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --allow-unsolved-metas #-} -- TODO: Remove when holes are filled - open import Protocol.Assumptions using (Assumptions) open import Protocol.Params using (Params) @@ -20,7 +18,8 @@ open import Protocol.Block ⦃ params ⦄ open import Protocol.Chain ⦃ params ⦄ open import Protocol.Message ⦃ params ⦄ open import Protocol.Network ⦃ params ⦄; open Envelope -open import Protocol.TreeType ⦃ params ⦄ +open import Protocol.Tree ⦃ params ⦄ +open import Protocol.Tree.Properties ⦃ params ⦄ open import Protocol.Semantics ⦃ params ⦄ ⦃ assumptions ⦄ open import Prelude.STS.Properties using (—[]→∗⇒—[]→∗ʳ; —[]→∗ʳ⇒—[]→∗; —[[]]→∗ʳ⇒≡; —[∷ʳ]→∗-split) open import Prelude.AssocList.Properties.Ext using (set-⁉; set-⁉-¬) @@ -507,8 +506,6 @@ opaque step* {_ ∷ mds} = L.SubS.⊆-trans (step* {mds}) (L.SubS.xs⊆x∷xs _ _) step (honestParty↑ {ls = ls} lsπ hp′π) with Params.winnerᵈ params {p′} {N‴ .clock} ... | ⁇ (no ¬isWinner) - rewrite - dec-no ¿ winner p′ (N‴ .clock) ¿ ¬isWinner = L.SubS.⊆-trans (L.SubS.filter⁺′ _ _ id (step* {N‴ .execOrder})) ih* where N‴⁺ : GlobalState @@ -523,7 +520,7 @@ opaque step* {[]} = L.SubS.⊆-refl step* {p* ∷ ps*} with honestyOf p* in hp* ... | corrupt = step* {ps*} - ... | honest rewrite hp* = let open L.SubS.⊆-Reasoning Block in begin + ... | honest = let open L.SubS.⊆-Reasoning Block in begin allBlocks (buildTree (blocks N‴⁺ p* ++ L.concatMap (blocks N‴⁺) (L.filter ¿ Honest ¿¹ ps*))) ⊆⟨ ≡ˢ⇒⊆×⊇ (allBlocksBuildTree-++ (blocks N‴⁺ p*) _) .proj₁ ⟩ allBlocks (buildTree (blocks N‴⁺ p*)) @@ -540,12 +537,12 @@ opaque eqBlocks : blocks N‴⁺ p* ≡ blocks N‴ p* eqBlocks with p* ≟ p′ ... | yes eq rewrite eq | lsπ | set-⁉ (N‴ .states) p′ ls = refl - ... | no neq rewrite lsπ | set-⁉-¬ (N‴ .states) p′ p* ls (≢-sym neq) = refl + ... | no neq rewrite set-⁉-¬ (N‴ .states) p′ p* ls (≢-sym neq) = refl tbksN‴⁺⊆tbksN‴ : allBlocks (buildTree (blocks N‴⁺ p*)) ⊆ˢ allBlocks (buildTree (blocks N‴ p*)) tbksN‴⁺⊆tbksN‴ rewrite eqBlocks = L.SubS.⊆-refl - ... | ⁇ (yes isWinner) rewrite lsπ = let open L.SubS.⊆-Reasoning Block in begin + ... | ⁇ (yes isWinner) = let open L.SubS.⊆-Reasoning Block in begin filter ¿ _≢ genesisBlock ¿¹ (allBlocks (honestTree N‴⁺)) ⊆⟨ L.SubS.filter⁺′ _ _ id $ step* {N‴ .execOrder} ⟩ filter ¿ _≢ genesisBlock ¿¹ (allBlocks (honestTree N‴) ++ [ nb ]) @@ -568,14 +565,14 @@ opaque N‴⁺ : GlobalState N‴⁺ = updateLocalState p′ (addBlock ls nb) N‴ - tnb : Tree + tnb : TreeImpl tnb = extendTree (ls .tree) nb blocksN‴⁺≡p′ : blocks N‴⁺ p′ ≡ allBlocks tnb blocksN‴⁺≡p′ rewrite set-⁉ (N‴ .states) p′ (addBlock ls nb) = refl blocksN‴⁺≢p′ : ∀ {p*} → p* ≢ p′ → blocks N‴ p* ≡ blocks N‴⁺ p* - blocksN‴⁺≢p′ {p*} p*≢p′ rewrite lsπ | set-⁉-¬ (N‴ .states) p′ p* (addBlock ls nb) (≢-sym p*≢p′) = refl + blocksN‴⁺≢p′ {p*} p*≢p′ rewrite set-⁉-¬ (N‴ .states) p′ p* (addBlock ls nb) (≢-sym p*≢p′) = refl step* : ∀ {ps*} → allBlocks (honestTree record N‴⁺ {execOrder = ps*}) @@ -584,7 +581,7 @@ opaque step* {[]} = L.SubS.xs⊆xs++ys _ _ step* {p* ∷ ps*} with honestyOf p* in hp* ... | corrupt = step* {ps*} - ... | honest rewrite hp* = let open L.SubS.⊆-Reasoning Block in begin + ... | honest = let open L.SubS.⊆-Reasoning Block in begin allBlocks (buildTree (blocks N‴⁺ p* ++ L.concatMap (blocks N‴⁺) (L.filter ¿ Honest ¿¹ ps*))) ⊆⟨ ≡ˢ⇒⊆×⊇ (allBlocksBuildTree-++ (blocks N‴⁺ p*) _) .proj₁ ⟩ allBlocks (buildTree (blocks N‴⁺ p*)) @@ -774,7 +771,7 @@ opaque step* (unknownParty↑ _ ) = ih* step* (honestParty↑ {ls = ls} lsπ hp) with Params.winnerᵈ params {p} {N‴ .clock} ... | ⁇ (no ¬isWinner) = ih* - ... | ⁇ (yes isWinner) rewrite lsπ | hp = nbₜ≤N′ₜ ∷ ih* + ... | ⁇ (yes isWinner) rewrite hp = nbₜ≤N′ₜ ∷ ih* where best : Chain best = bestChain (N‴ .clock ∸ 1) (ls .tree) @@ -1032,8 +1029,6 @@ opaque step*′ {[]} _ = ih′ step*′ {(m , _) ∷ mds} sub with bᵐ ← projBlock m | ¿ HonestBlock bᵐ ¿ ... | no ¬hbᵐ - rewrite - sym $ L.filter-reject ¿ HonestBlock ¿¹ {bᵐ} {honestBlockHistory (broadcastMsgsᶜ mds N‴)} ¬hbᵐ = step*′ {mds} sub ... | yes hbᵐ with bᵐ .slot + 2 * length (corruptSlotsInRange (sl′ + 1) (sl″ + 1))) + → ∀ {p₁ p₂ : Party} {ls₁ ls₂ : LocalState} + → Honest p₁ + → Honest p₂ + → N₁ .states ⁉ p₁ ≡ just ls₁ + → N₂ .states ⁉ p₂ ≡ just ls₂ + → let bc₁ = bestChain (N₁ .clock ∸ 1) (ls₁ .tree) + bc₂ = bestChain (N₂ .clock ∸ 1) (ls₂ .tree) + in prune k bc₁ ⪯ bc₂ +commonPrefixRephrased N₀↝⋆N₁ N₁↝⋆N₂ ffN₂ cfN₂ ¬adversaryAdvantage hp₁ hp₂ lsp₁ lsp₂ + with commonPrefix N₀↝⋆N₁ N₁↝⋆N₂ ffN₂ cfN₂ hp₁ hp₂ lsp₁ lsp₂ +... | inj₁ bc₁⪯bc₂ = bc₁⪯bc₂ +... | inj₂ adversaryAdvantage = + contradiction + adversaryAdvantage + (λ (sl′ , sl″ , h₁ , h₂ , h₃ , h₄) → + contradiction + (¬adversaryAdvantage {sl′} {sl″} (h₁ , h₂ , h₃)) + (Nat.≤⇒≯ h₄)) diff --git a/src/Properties/Safety/SingleRoundCommonPrefix.agda b/src/Properties/Safety/SingleRoundCommonPrefix.agda index ef69467..67f6096 100644 --- a/src/Properties/Safety/SingleRoundCommonPrefix.agda +++ b/src/Properties/Safety/SingleRoundCommonPrefix.agda @@ -11,9 +11,11 @@ open import Protocol.BaseTypes using (Slot) open import Protocol.Crypto ⦃ params ⦄ using (Hashable); open Hashable ⦃ ... ⦄ open import Protocol.Block ⦃ params ⦄ open import Protocol.Chain ⦃ params ⦄ +open import Protocol.Chain.Properties ⦃ params ⦄ open import Protocol.Message ⦃ params ⦄ open import Protocol.Network ⦃ params ⦄; open Envelope -open import Protocol.TreeType ⦃ params ⦄ +open import Protocol.Tree ⦃ params ⦄ +open import Protocol.Tree.Properties ⦃ params ⦄ open import Protocol.Semantics ⦃ params ⦄ ⦃ assumptions ⦄ open import Properties.Base.ForgingFree ⦃ params ⦄ ⦃ assumptions ⦄ open import Properties.Base.CollisionFree ⦃ params ⦄ ⦃ assumptions ⦄ @@ -168,8 +170,8 @@ adversaryHasAdvantage {N} N₀↝⋆N ffN cfN {p} {ls} hp lsp {c} {sl} c⊆fgb mb′IsJust′ : ∀ c′ → M.Is-just $ L.find ¿ HonestBlock ¿¹ (c′ ++ [ genesisBlock ]) mb′IsJust′ [] rewrite genesisHonesty = M.Any.just _ mb′IsJust′ (b″ ∷ c′) with ¿ HonestBlock b″ ¿ - ... | yes hb″ rewrite hb″ = M.Any.just _ - ... | no ¬hb″ rewrite dec-no ¿ HonestBlock b″ ¿ ¬hb″ = mb′IsJust′ c′ + ... | yes hb″ = M.Any.just _ + ... | no ¬hb″ = mb′IsJust′ c′ -- ... and we call it b′. In the following, we choose sl′ to be use b′. b′ = Block ∋ M.to-witness mb′IsJust @@ -1246,8 +1248,7 @@ singleRoundCommonPrefix {N} {k} N₀↝⋆N ffN cfN {p₁} {p₂} {ls₁} {ls₂ π2 : b .slot ≤ N .clock ∸ 1 + 0 π2 rewrite - Nat.+-suc (N .clock ∸ 1) 0 - | Nat.+-identityʳ (N .clock ∸ 1) + Nat.+-identityʳ (N .clock ∸ 1) = L.All.lookup (bestChainSlotBounded (ls .tree) (N .clock ∸ 1)) b∈bc Goal-◆ = λ ◆ → diff --git a/src/Protocol/Assumptions.agda b/src/Protocol/Assumptions.agda index 2838fed..3f83f1c 100644 --- a/src/Protocol/Assumptions.agda +++ b/src/Protocol/Assumptions.agda @@ -11,14 +11,14 @@ open import Protocol.Chain ⦃ params ⦄ open import Protocol.Crypto ⦃ params ⦄ using (Hashable) open import Protocol.Message ⦃ params ⦄ open import Protocol.Network ⦃ params ⦄ -open import Protocol.TreeType ⦃ params ⦄ +open import Protocol.Tree ⦃ params ⦄ open Hashable ⦃ ... ⦄ open Honesty open Envelope record Assumptions : Type₁ where field - Tree : Type + TreeImpl : Type AdversarialState : Type honestyOf : Party → Honesty txSelection : Slot → Party → Txs @@ -43,7 +43,7 @@ record Assumptions : Type₁ where ⦃ Hashable-Block ⦄ : Hashable Block ⦃ Default-Block ⦄ : Default Block - ⦃ TreeType-Tree ⦄ : TreeType Tree + ⦃ Tree-TreeImpl ⦄ : Tree TreeImpl ⦃ parties₀Uniqueness ⦄ : Unique parties₀ ⦃ parties₀HasHonest ⦄ : L.Any.Any ((_≡ honest) ∘ honestyOf) parties₀ ⦃ genesisBlockSlot ⦄ : genesisBlock .slot ≡ 0 @@ -89,5 +89,5 @@ record Assumptions : Type₁ where ∷-⊆ʰ {bs} {_} {b} bh p rewrite bh = L.SubS.⊆-trans (L.SubS.xs⊆x∷xs (honestBlocks bs) b) p instance - Default-Tree : Default Tree - Default-Tree .def = tree₀ + Default-TreeImpl : Default TreeImpl + Default-TreeImpl .def = tree₀ diff --git a/src/Protocol/Chain.agda b/src/Protocol/Chain.agda index 65f9d75..763f022 100644 --- a/src/Protocol/Chain.agda +++ b/src/Protocol/Chain.agda @@ -13,18 +13,7 @@ open import Protocol.Prelude open import Protocol.BaseTypes using (Slot) open import Protocol.Block ⦃ params ⦄ hiding (Block) open Hashable ⦃ ... ⦄ -open import Data.List.Relation.Binary.Suffix.Heterogeneous using (Suffix; here; there; _++ˢ_) -open import Data.List.Relation.Binary.Suffix.Heterogeneous.Properties using (++⁺; suffix?) -open import Data.List.Relation.Binary.Suffix.Homogeneous.Properties using (isPreorder) -open import Relation.Binary.Definitions using (Reflexive; Transitive) -open import Relation.Binary.Structures using (IsPreorder) -open import Relation.Binary.PropositionalEquality.Properties renaming (isPreorder to ≡-isPreorder) -open import Relation.Binary.Bundles using (Preorder) -import Relation.Binary.Reasoning.Preorder as ≲-Reasoning -open import Relation.Binary.Reasoning.Syntax -open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; ≡⇒Pointwise-≡; Pointwise-≡⇒≡) -open import Data.List.Properties.Ext using (≢[]⇒∷) -open import Data.List.Membership.Propositional.Properties.Ext using (x∈x∷xs) +open import Data.List.Relation.Binary.Suffix.Heterogeneous using (Suffix) genesisBlock : Block genesisBlock = it .def @@ -45,107 +34,6 @@ prune sl c = filter ((_≤? sl) ∘ slot) c _⪯_ : Rel Chain _ _⪯_ = Suffix _≡_ -⪯-isPreorder : IsPreorder (Pointwise _≡_) _⪯_ -⪯-isPreorder = isPreorder ≡-isPreorder - -⪯-preorder : Preorder _ _ _ -⪯-preorder = record - { isPreorder = ⪯-isPreorder - } - -⪯-refl : Reflexive _⪯_ -⪯-refl = PO.reflexive (≡⇒Pointwise-≡ refl) - where module PO = IsPreorder ⪯-isPreorder - -⪯-trans : Transitive _⪯_ -⪯-trans = PO.trans - where module PO = IsPreorder ⪯-isPreorder - -module ⪯-Reasoning where - - private module Base = ≲-Reasoning ⪯-preorder - - open Base public - hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼) - renaming (≲-go to ⪯-go; ≈-go to ≋-go) - - open ≲-syntax _IsRelatedTo_ _IsRelatedTo_ ⪯-go public - open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go public - -[]⪯ : ∀ {c : Chain} → [] ⪯ c -[]⪯ {[]} = ⪯-refl -[]⪯ {b ∷ c} = there ([]⪯ {c}) - -⪯-++ : ∀ (c₁ c₂ : Chain) → c₁ ⪯ (c₂ ++ c₁) -⪯-++ _ c₂ = c₂ ++ˢ ⪯-refl - -module _ where - - open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.Ext using (Suffix⇒Sublist) - import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset - open import Relation.Binary.PropositionalEquality.Properties using (setoid) - - ⪯⇒⊆ˢ : ∀ {c₁ c₂ : Chain} → c₁ ⪯ c₂ → c₁ ⊆ˢ c₂ - ⪯⇒⊆ˢ = Subset.Sublist⇒Subset (setoid _) ∘ Suffix⇒Sublist _≡_ - -open import Function.Bundles using (_⇔_; mk⇔; Equivalence) - -⪯∷⇔≡⊎⪯ : ∀ {c₁ c₂ : Chain} {b : Block} → c₁ ⪯ (b ∷ c₂) ⇔ (c₁ ≡ b ∷ c₂ ⊎ c₁ ⪯ c₂) -⪯∷⇔≡⊎⪯ {c₁} {c₂} {b} = mk⇔ to from - where - to : c₁ ⪯ (b ∷ c₂) → c₁ ≡ b ∷ c₂ ⊎ c₁ ⪯ c₂ - to (here c₁≐b∷c₂) = inj₁ (Pointwise-≡⇒≡ c₁≐b∷c₂) - to (there c₁⪯c₂) = inj₂ c₁⪯c₂ - - from : c₁ ≡ b ∷ c₂ ⊎ c₁ ⪯ c₂ → c₁ ⪯ (b ∷ c₂) - from (inj₁ c₁≡b∷c₂) = here (≡⇒Pointwise-≡ c₁≡b∷c₂) - from (inj₂ c₁⪯c₂) = there c₁⪯c₂ - -≢∷×⪯∷⇒⪯ : ∀ {c₁ c₂ : Chain} {b : Block} → c₁ ≢ b ∷ c₂ → c₁ ⪯ (b ∷ c₂) → c₁ ⪯ c₂ -≢∷×⪯∷⇒⪯ c₁≢b∷c₂ (here c₁≐b∷c₂) = contradiction (Pointwise-≡⇒≡ c₁≐b∷c₂) c₁≢b∷c₂ -≢∷×⪯∷⇒⪯ c₁≢b∷c₂ (there c₁⪯c₂) = c₁⪯c₂ - -⪯⇔∃ : ∀ {c₁ c₂ : Chain} → c₁ ⪯ c₂ ⇔ (∃[ c ] c ++ c₁ ≡ c₂) -⪯⇔∃ {c₁} {c₂} = mk⇔ to from - where - to : ∀ {c₁ c₂ : Chain} → c₁ ⪯ c₂ → ∃[ c ] c ++ c₁ ≡ c₂ - to (here c₁≐c₂) rewrite Pointwise-≡⇒≡ c₁≐c₂ = [] , refl - to {c₁} {b ∷ c₂} (there c₁⪯c₂) with to c₁⪯c₂ - ... | c , c++c₁≡c₂ = b ∷ c , cong (b ∷_) c++c₁≡c₂ - - from : ∀ {c₁ c₂ : Chain} → ∃[ c ] c ++ c₁ ≡ c₂ → c₁ ⪯ c₂ - from {c₁} {[]} (c , c++c₁≡[]) rewrite L.++-conicalʳ c c₁ c++c₁≡[] = []⪯ - from {c₁} {b ∷ c₂} (c , c++c₁≡b∷c₂) with c ≟ [] - ... | yes c≡[] = here $ ≡⇒Pointwise-≡ $ subst (λ ◆ → ◆ ++ c₁ ≡ b ∷ c₂) c≡[] c++c₁≡b∷c₂ - ... | no c≢[] with ≢[]⇒∷ c≢[] - ... | (_ , c′ , c≡_∷c′) = there $ from (c′ , L.∷-injective (subst (λ ◆ → ◆ ++ c₁ ≡ b ∷ c₂) c≡_∷c′ c++c₁≡b∷c₂) .proj₂) - -++-¬-⪯ : ∀ (c₁ : Chain) {c₂ : Chain} → c₂ ≢ [] → ¬ (c₂ ++ c₁) ⪯ c₁ -++-¬-⪯ c₁ {[]} []≢[] = contradiction refl []≢[] -++-¬-⪯ c₁ {b ∷ c₂} b∷c₂≢[] b+c₂+c₁⪯c₁ with ⪯⇔∃ .Equivalence.to b+c₂+c₁⪯c₁ -... | c′ , c′+b+c₂+c₁≡c₁ = contradiction (L.++-identityˡ-unique (c′ ++ b ∷ c₂) (sym $ trans (L.++-assoc c′ (b ∷ c₂) c₁) c′+b+c₂+c₁≡c₁)) (contraposition (L.++-conicalʳ c′ (b ∷ c₂)) λ ()) - -_⪯?_ : Decidable² _⪯_ -c₁ ⪯? c₂ = suffix? _≟_ c₁ c₂ - -prune-⪯-trans : ∀ {c₁ c₂ c₃ : Chain} {sl : Slot} → - prune sl c₁ ⪯ c₂ - → prune sl c₂ ⪯ c₃ - → prune sl c₁ ⪯ c₃ -prune-⪯-trans {c₁} {c₂} {c₃} {sl} c₁↯sl⪯c₂ c₂↯sl⪯c₃ - with ⪯⇔∃ .Equivalence.to c₁↯sl⪯c₂ | ⪯⇔∃ .Equivalence.to c₂↯sl⪯c₃ -... | c₄ , c₄+c₁↯sl≡c₂ | c₅ , c₅++c₂↯sl≡c₃ - = ⪯⇔∃ .Equivalence.from (c₅ ++ prune sl c₄ , [c₅+c₄↯sl]+c₁↯sl≡c₃) - where - [c₅+c₄↯sl]+c₁↯sl≡c₃ : (c₅ ++ prune sl c₄) ++ prune sl c₁ ≡ c₃ - [c₅+c₄↯sl]+c₁↯sl≡c₃ = let open ≡-Reasoning in begin - (c₅ ++ prune sl c₄) ++ prune sl c₁ ≡⟨ cong ((c₅ ++ prune sl c₄) ++_) (sym $ L.filter-idem _ c₁) ⟩ - (c₅ ++ prune sl c₄) ++ prune sl (prune sl c₁) ≡⟨ L.++-assoc c₅ _ _ ⟩ - c₅ ++ prune sl c₄ ++ prune sl (prune sl c₁) ≡⟨ cong (c₅ ++_) (sym $ L.filter-++ _ c₄ _) ⟩ - c₅ ++ prune sl (c₄ ++ prune sl c₁) ≡⟨ cong (λ ◆ → c₅ ++ prune sl ◆) c₄+c₁↯sl≡c₂ ⟩ - c₅ ++ prune sl c₂ ≡⟨ c₅++c₂↯sl≡c₃ ⟩ - c₃ ∎ - _⟵_ : Rel Block _ b ⟵ b′ = prev b ≡ hash b′ @@ -155,157 +43,16 @@ ProperlyLinked [] = ⊥ ProperlyLinked (b ∷ []) = b ≡ genesisBlock ProperlyLinked (b ∷ b′ ∷ bs) = b ⟵ b′ × ProperlyLinked (b′ ∷ bs) -{- -instance - - ProperlyLinked? : ProperlyLinked ⁇¹ - ProperlyLinked? {[]} .dec = no id - ProperlyLinked? {[ b ]} .dec = b ≟ genesisBlock - ProperlyLinked? {b ∷ b′ ∷ c} .dec = ¿ b ⟵ b′ ¿ ×-dec ProperlyLinked? {b′ ∷ c} .dec --} - -ProperlyLinked⇒≢[] : ∀ {c : Chain} → ProperlyLinked c → c ≢ [] -ProperlyLinked⇒≢[] {_ ∷ _} _ = λ () - -ProperlyLinked⇒gbIsHead : ∀ {c : Chain} → ProperlyLinked c → ∃[ c′ ] c′ L.∷ʳ genesisBlock ≡ c -ProperlyLinked⇒gbIsHead {[ b ]} b≡gb rewrite b≡gb = [] , refl -ProperlyLinked⇒gbIsHead {b ∷ b′ ∷ c} pl with ProperlyLinked⇒gbIsHead {b′ ∷ c} (pl .proj₂) -... | c′ , pl′ = b ∷ c′ , cong (b ∷_) pl′ - -ProperlyLinked-++⁻ : ∀ c {c′} → c′ ≢ [] → ProperlyLinked (c ++ c′) → ProperlyLinked c′ -ProperlyLinked-++⁻ [] {_} _ p2 = p2 -ProperlyLinked-++⁻ [ _ ] {[]} p1 _ = contradiction refl p1 -ProperlyLinked-++⁻ [ _ ] {_ ∷ _} _ p2 = p2 .proj₂ -ProperlyLinked-++⁻ (b ∷ b′ ∷ c) {c′} p1 p2 = ProperlyLinked-++⁻ (b′ ∷ c) {c′} p1 (p2 .proj₂) - -- NOTE: Similar to instantiating Data.List.Relation.Unary.Sorted.TotalOrder -- with ≤-isTotalOrder from from Data.Nat.Properties, but in our case we need -- < instead of ≤. open import Data.List.Relation.Unary.Linked DecreasingSlots = Linked _>ˢ_ -open import Data.List.Relation.Unary.AllPairs -open import Data.List.Relation.Unary.Linked.Properties using (Linked⇒AllPairs; AllPairs⇒Linked) -open import Data.List.Relation.Unary.AllPairs.Properties.Ext using (++⁻) - -++-DecreasingSlots : ∀ {c c′ : Chain} → DecreasingSlots (c ++ c′) → DecreasingSlots c × DecreasingSlots c′ × L.All.All (λ b → L.All.All (b >ˢ_) c′) c -++-DecreasingSlots {c} {c′} p with ++⁻ {xs = c} {ys = c′} $ Linked⇒AllPairs (λ {b b′ b″} → >ˢ-trans {b} {b′} {b″}) p -... | (p₁ , p₂ , p₃) = (AllPairs⇒Linked p₁ , AllPairs⇒Linked p₂ , p₃) - -∷-DecreasingSlots : ∀ {c : Chain} {b : Block} → DecreasingSlots (b ∷ c) → DecreasingSlots c × L.All.All (b >ˢ_) c -∷-DecreasingSlots {c} {b} p with ++-DecreasingSlots {c = [ b ]} {c′ = c} p -... | (_ , p₂ , p₃) = p₂ , L.All.head p₃ - -DecreasingSlots⇒UniqueSlots : ∀ {c : Chain} → DecreasingSlots c → Unique (L.map slot c) -DecreasingSlots⇒UniqueSlots {[]} _ = AllPairs.[] -DecreasingSlots⇒UniqueSlots {b ∷ c} ds[b∷c] with ∷-DecreasingSlots ds[b∷c] -... | ds[c] , b>ˢc = L.All.map⁺ (L.All.map Nat.>⇒≢ b>ˢc) AllPairs.∷ DecreasingSlots⇒UniqueSlots ds[c] - -nonAdjacentBlocksDecreasingSlots : ∀ {cₕ cₘ cₜ : Chain} {b₁ b₂ : Block} → - DecreasingSlots (cₕ ++ b₁ ∷ cₘ ++ b₂ ∷ cₜ) - → b₁ >ˢ b₂ -nonAdjacentBlocksDecreasingSlots {cₕ} {cₘ} {cₜ} {b₁} {b₂} dsπ = - dsπ ∶ - DecreasingSlots (cₕ ++ b₁ ∷ cₘ ++ b₂ ∷ cₜ) - |> proj₁ ∘ proj₂ ∘ ++-DecreasingSlots {cₕ} ∶ - DecreasingSlots (b₁ ∷ cₘ ++ b₂ ∷ cₜ) - |> proj₂ ∘ ∷-DecreasingSlots ∶ - L.All.All (b₁ >ˢ_) (cₘ ++ b₂ ∷ cₜ) - |> L.All.++⁻ʳ cₘ ∶ - L.All.All (b₁ >ˢ_) (b₂ ∷ cₜ) - |> L.All.head ∶ - b₁ >ˢ b₂ - where open import Function.Reasoning - -DecreasingSlots-∈ : ∀ {c c′ : Chain} {b b′ : Block} → DecreasingSlots (c ++ c′) → b ∈ c → b′ ∈ c′ → b >ˢ b′ -DecreasingSlots-∈ {c} {c′} {b} {b′} ds[c++c′] b∈c b′∈c′ with L.Mem.∈-∃++ b∈c | L.Mem.∈-∃++ b′∈c′ -... | cₕ , cₜ , c≡cₕ+b+cₜ | cₕ′ , cₜ′ , c′≡cₕ′+b′+cₜ′ = nonAdjacentBlocksDecreasingSlots ds - where - open ≡-Reasoning - - eq : (cₕ ++ b ∷ cₜ) ++ (cₕ′ ++ b′ ∷ cₜ′) ≡ cₕ ++ b ∷ (cₜ ++ cₕ′) ++ b′ ∷ cₜ′ - eq = begin - (cₕ ++ b ∷ cₜ) ++ (cₕ′ ++ b′ ∷ cₜ′) ≡⟨ L.++-assoc _ (b ∷ cₜ) _ ⟩ - cₕ ++ b ∷ (cₜ ++ (cₕ′ ++ b′ ∷ cₜ′)) ≡⟨ cong ((cₕ ++_) ∘ (b ∷_)) (sym $ L.++-assoc cₜ cₕ′ _) ⟩ - cₕ ++ b ∷ (cₜ ++ cₕ′) ++ b′ ∷ cₜ′ ∎ - - ds : DecreasingSlots (cₕ ++ b ∷ (cₜ ++ cₕ′) ++ b′ ∷ cₜ′) - ds rewrite c≡cₕ+b+cₜ | c′≡cₕ′+b′+cₜ′ | sym eq = ds[c++c′] - opaque _✓ : Pred Chain 0ℓ c ✓ = CorrectBlocks c × ProperlyLinked c × DecreasingSlots c - ✓⇒cb : ∀ {c : Chain} → c ✓ → CorrectBlocks c - ✓⇒cb (cb , _ , _) = cb - - ✓⇒ds : ∀ {c : Chain} → c ✓ → DecreasingSlots c - ✓⇒ds (_ , _ , ds) = ds - - ✓⇒≢[] : ∀ {c : Chain} → c ✓ → c ≢ [] - ✓⇒≢[] (_ , pl , _) = ProperlyLinked⇒≢[] pl - - ✓⇒gbIsHead : ∀ {c : Chain} → c ✓ → ∃[ c′ ] c′ L.∷ʳ genesisBlock ≡ c - ✓⇒gbIsHead (_ , pl , _) = ProperlyLinked⇒gbIsHead pl - - ✓-∷ : ∀ {b b′ : Block} {c : Chain} → (CorrectBlock b × b ⟵ b′ × b >ˢ b′ × (b′ ∷ c) ✓) ⇔ (b ∷ b′ ∷ c) ✓ - ✓-∷ {b} {b′} {c} = mk⇔ to from - where - to : CorrectBlock b × b ⟵ b′ × b >ˢ b′ × (b′ ∷ c) ✓ → (b ∷ b′ ∷ c) ✓ - to (cbb , b⟵b′ , b>b′ , cb[b′∷c] , pl[b′∷c] , ds[b′∷c]) = cbb ∷ cb[b′∷c] , (b⟵b′ , pl[b′∷c]) , b>b′ ∷ ds[b′∷c] - - from : ∀ {c : Chain} → (b ∷ b′ ∷ c) ✓ → CorrectBlock b × b ⟵ b′ × b >ˢ b′ × (b′ ∷ c) ✓ - from {[]} (cbb ∷ cb[b′] , (b⟵b′ , b′≡gb) , b>b′ ∷ ds[b′]) = cbb , b⟵b′ , b>b′ , (cb[b′] , b′≡gb , ds[b′]) - from {b″ ∷ c′} (cbb ∷ cb[b′∷b″∷c′] , (b⟵b′ , pl[b′∷b″∷c′]) , b>b′ ∷ ds[b′∷b″∷c′]) = cbb , b⟵b′ , b>b′ , (cb[b′∷b″∷c′] , pl[b′∷b″∷c′] , ds[b′∷b″∷c′]) - - open Function.Bundles.Equivalence using (from) - - ✓-++ʳ : ∀ {b : Block} {c c′ : Chain} → (c ++ b ∷ c′) ✓ → (b ∷ c′) ✓ - ✓-++ʳ {b} {[]} {c′} p = p - ✓-++ʳ {b} {[ b′ ]} {c′} p = from ✓-∷ p .proj₂ .proj₂ .proj₂ - ✓-++ʳ {b} {b′ ∷ b″ ∷ c} {c′} p = ✓-++ʳ {b} {b″ ∷ c} {c′} (from ✓-∷ p .proj₂ .proj₂ .proj₂) - - ✓⇒gb⪯ : ∀ {c : Chain} → c ✓ → [ genesisBlock ] ⪯ c - ✓⇒gb⪯ c✓ = let c′ , c′∷gb≡c = ✓⇒gbIsHead c✓ in subst ([ genesisBlock ] ⪯_) c′∷gb≡c $ ⪯-++ [ genesisBlock ] c′ - - tip-∈ : ∀ {c : Chain} → c ✓ → tip c ∈ c - tip-∈ {[]} p = contradiction p $ contraposition (✓⇒≢[] {[]}) (contradiction refl) - tip-∈ {b ∷ c} p = x∈x∷xs c - - pruneIdentity : ∀ {c : Chain} {b : Block} {sl : Slot} → - b .slot ≤ sl - → DecreasingSlots (b ∷ c) - → prune sl (b ∷ c) ≡ b ∷ c - pruneIdentity {c} {b} {sl} bₜ≤sl ds[b+c] - rewrite - L.filter-accept ((_≤? sl) ∘ slot) {x = b} {xs = c} bₜ≤sl - = cong (b ∷_) (goal p) - where - p : L.All.All (_>ˢ_ b) c - p = ∷-DecreasingSlots ds[b+c] .proj₂ - - goal : ∀ {c : Chain} → L.All.All (_>ˢ_ b) c → prune sl c ≡ c - goal {[]} _ = refl - goal {b′ ∷ c′} p = let open ≡-Reasoning in begin - prune sl (b′ ∷ c′) ≡⟨ L.filter-accept ((_≤? sl) ∘ slot) {x = b′} {xs = c′} b′ₜ≤sl ⟩ - b′ ∷ prune sl c′ ≡⟨ cong (b′ ∷_) ih ⟩ - b′ ∷ c′ ∎ - where - ih : prune sl c′ ≡ c′ - ih = goal {c′} (L.All.tail p) - - b′ₜ≤sl : b′ .slot ≤ sl - b′ₜ≤sl = Nat.<⇒≤ $ Nat.<-≤-trans (L.All.head p) bₜ≤sl - - prune-⪯ : ∀ {c : Chain} (sl : Slot) → DecreasingSlots c → prune sl c ⪯ c - prune-⪯ {[]} _ _ = ⪯-refl - prune-⪯ {b′ ∷ c′} sl ds[b′+c] with b′ .slot ≤? sl - ... | yes b′ₜ≤sl rewrite pruneIdentity b′ₜ≤sl ds[b′+c] = ⪯-refl - ... | no b′ₜ≰sl rewrite L.filter-reject ((_≤? sl) ∘ slot) {x = b′} {xs = c′} b′ₜ≰sl = ⪯-trans ih (⪯-++ c′ [ b′ ]) - where - ih : prune sl c′ ⪯ c′ - ih = prune-⪯ {c′} sl (∷-DecreasingSlots ds[b′+c] .proj₁) - {-# TERMINATING #-} -- TODO: Prove termination using `WellFounded`. chainFromBlock : Block → List Block → Chain @@ -348,15 +95,3 @@ chainFromBlock′ (suc n) b bs = chainFromBlock : Block → List Block → Chain chainFromBlock b bs = chainFromBlock′ (length bs) b bs --------} - -cfbStartsWithBlock : ∀ {b : Block} {bs : List Block} → chainFromBlock b bs ≢ [] → ∃[ bs′ ] chainFromBlock b bs ≡ b ∷ bs′ -cfbStartsWithBlock {b} {bs} cfbbs≢[] - with b == genesisBlock -... | true = [] , refl -... | false with ¿ b ⟵ genesisBlock ¿ᵇ -... | true = [ genesisBlock ] , refl -... | false with L.findᵇ (λ b″ → ¿ b ⟵ b″ ¿ᵇ) bs in eqf -... | nothing = contradiction refl cfbbs≢[] -... | just b′ with chainFromBlock b′ (L.filterᵇ (not ∘ (_== b′)) bs) in eqcfb -... | [] = contradiction refl cfbbs≢[] -... | b′′ ∷ bs′′ = b′′ ∷ bs′′ , refl diff --git a/src/Protocol/Chain/Properties.agda b/src/Protocol/Chain/Properties.agda index 8fe4b13..064e800 100644 --- a/src/Protocol/Chain/Properties.agda +++ b/src/Protocol/Chain/Properties.agda @@ -7,34 +7,301 @@ module Protocol.Chain.Properties where open import Protocol.Prelude +open import Protocol.BaseTypes using (Slot) open import Protocol.Block ⦃ params ⦄ open import Protocol.Chain ⦃ params ⦄ +open import Data.List.Relation.Unary.Linked +open import Data.List.Relation.Unary.Unique.Propositional.Properties using (map⁻) +open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; ≡⇒Pointwise-≡; Pointwise-≡⇒≡) +open import Data.List.Relation.Binary.Suffix.Homogeneous.Properties using (isPreorder) +open import Data.List.Relation.Binary.Suffix.Heterogeneous using (Suffix; here; there; _++ˢ_) +open import Data.List.Relation.Binary.Suffix.Heterogeneous.Properties using (suffix?) +open import Data.List.Properties.Ext using (≢[]⇒∷) +open import Data.List.Membership.Propositional.Properties.Ext using (x∈x∷xs) +open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.PropositionalEquality.Properties renaming (isPreorder to ≡-isPreorder) +open import Relation.Binary.Bundles using (Preorder) +open import Relation.Binary.Definitions using (Reflexive; Transitive) +import Relation.Binary.Reasoning.Preorder as ≲-Reasoning +open import Relation.Binary.Reasoning.Syntax open import Function.Bundles using (_⇔_; mk⇔; Equivalence) open Function.Bundles.Equivalence using (from; to) -open import Data.List.Relation.Unary.Linked -open import Data.List.Relation.Unary.Unique.Propositional.Properties.Ext using (map⁻) + +⪯-isPreorder : IsPreorder (Pointwise _≡_) _⪯_ +⪯-isPreorder = isPreorder ≡-isPreorder + +⪯-preorder : Preorder _ _ _ +⪯-preorder = record + { isPreorder = ⪯-isPreorder + } + +⪯-refl : Reflexive _⪯_ +⪯-refl = PO.reflexive (≡⇒Pointwise-≡ refl) + where module PO = IsPreorder ⪯-isPreorder + +⪯-trans : Transitive _⪯_ +⪯-trans = PO.trans + where module PO = IsPreorder ⪯-isPreorder + +module ⪯-Reasoning where + + private module Base = ≲-Reasoning ⪯-preorder + + open Base public + hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼) + renaming (≲-go to ⪯-go; ≈-go to ≋-go) + + open ≲-syntax _IsRelatedTo_ _IsRelatedTo_ ⪯-go public + open ≋-syntax _IsRelatedTo_ _IsRelatedTo_ ≋-go public + +[]⪯ : ∀ {c : Chain} → [] ⪯ c +[]⪯ {[]} = ⪯-refl +[]⪯ {b ∷ c} = there ([]⪯ {c}) + +⪯-++ : ∀ (c₁ c₂ : Chain) → c₁ ⪯ (c₂ ++ c₁) +⪯-++ _ c₂ = c₂ ++ˢ ⪯-refl + +module _ where + + open import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.Ext using (Suffix⇒Sublist) + import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset + open import Relation.Binary.PropositionalEquality.Properties using (setoid) + + ⪯⇒⊆ˢ : ∀ {c₁ c₂ : Chain} → c₁ ⪯ c₂ → c₁ ⊆ˢ c₂ + ⪯⇒⊆ˢ = Subset.Sublist⇒Subset (setoid _) ∘ Suffix⇒Sublist _≡_ + +open import Function.Bundles using (_⇔_; mk⇔; Equivalence) + +⪯∷⇔≡⊎⪯ : ∀ {c₁ c₂ : Chain} {b : Block} → c₁ ⪯ (b ∷ c₂) ⇔ (c₁ ≡ b ∷ c₂ ⊎ c₁ ⪯ c₂) +⪯∷⇔≡⊎⪯ {c₁} {c₂} {b} = mk⇔ to′ from′ + where + to′ : c₁ ⪯ (b ∷ c₂) → c₁ ≡ b ∷ c₂ ⊎ c₁ ⪯ c₂ + to′ (here c₁≐b∷c₂) = inj₁ (Pointwise-≡⇒≡ c₁≐b∷c₂) + to′ (there c₁⪯c₂) = inj₂ c₁⪯c₂ + + from′ : c₁ ≡ b ∷ c₂ ⊎ c₁ ⪯ c₂ → c₁ ⪯ (b ∷ c₂) + from′ (inj₁ c₁≡b∷c₂) = here (≡⇒Pointwise-≡ c₁≡b∷c₂) + from′ (inj₂ c₁⪯c₂) = there c₁⪯c₂ + +≢∷×⪯∷⇒⪯ : ∀ {c₁ c₂ : Chain} {b : Block} → c₁ ≢ b ∷ c₂ → c₁ ⪯ (b ∷ c₂) → c₁ ⪯ c₂ +≢∷×⪯∷⇒⪯ c₁≢b∷c₂ (here c₁≐b∷c₂) = contradiction (Pointwise-≡⇒≡ c₁≐b∷c₂) c₁≢b∷c₂ +≢∷×⪯∷⇒⪯ c₁≢b∷c₂ (there c₁⪯c₂) = c₁⪯c₂ + +⪯⇔∃ : ∀ {c₁ c₂ : Chain} → c₁ ⪯ c₂ ⇔ (∃[ c ] c ++ c₁ ≡ c₂) +⪯⇔∃ {c₁} {c₂} = mk⇔ to′ from′ + where + to′ : ∀ {c₁ c₂ : Chain} → c₁ ⪯ c₂ → ∃[ c ] c ++ c₁ ≡ c₂ + to′ (here c₁≐c₂) rewrite Pointwise-≡⇒≡ c₁≐c₂ = [] , refl + to′ {c₁} {b ∷ c₂} (there c₁⪯c₂) with to′ c₁⪯c₂ + ... | c , c++c₁≡c₂ = b ∷ c , cong (b ∷_) c++c₁≡c₂ + + from′ : ∀ {c₁ c₂ : Chain} → ∃[ c ] c ++ c₁ ≡ c₂ → c₁ ⪯ c₂ + from′ {c₁} {[]} (c , c++c₁≡[]) rewrite L.++-conicalʳ c c₁ c++c₁≡[] = []⪯ + from′ {c₁} {b ∷ c₂} (c , c++c₁≡b∷c₂) with c ≟ [] + ... | yes c≡[] = here $ ≡⇒Pointwise-≡ $ subst (λ ◆ → ◆ ++ c₁ ≡ b ∷ c₂) c≡[] c++c₁≡b∷c₂ + ... | no c≢[] with ≢[]⇒∷ c≢[] + ... | (_ , c′ , c≡_∷c′) = there $ from′ (c′ , L.∷-injective (subst (λ ◆ → ◆ ++ c₁ ≡ b ∷ c₂) c≡_∷c′ c++c₁≡b∷c₂) .proj₂) + +++-¬-⪯ : ∀ (c₁ : Chain) {c₂ : Chain} → c₂ ≢ [] → ¬ (c₂ ++ c₁) ⪯ c₁ +++-¬-⪯ c₁ {[]} []≢[] = contradiction refl []≢[] +++-¬-⪯ c₁ {b ∷ c₂} b∷c₂≢[] b+c₂+c₁⪯c₁ with ⪯⇔∃ .Equivalence.to b+c₂+c₁⪯c₁ +... | c′ , c′+b+c₂+c₁≡c₁ = contradiction (L.++-identityˡ-unique (c′ ++ b ∷ c₂) (sym $ trans (L.++-assoc c′ (b ∷ c₂) c₁) c′+b+c₂+c₁≡c₁)) (contraposition (L.++-conicalʳ c′ (b ∷ c₂)) λ ()) + +_⪯?_ : Decidable² _⪯_ +c₁ ⪯? c₂ = suffix? _≟_ c₁ c₂ + +prune-⪯-trans : ∀ {c₁ c₂ c₃ : Chain} {sl : Slot} → + prune sl c₁ ⪯ c₂ + → prune sl c₂ ⪯ c₃ + → prune sl c₁ ⪯ c₃ +prune-⪯-trans {c₁} {c₂} {c₃} {sl} c₁↯sl⪯c₂ c₂↯sl⪯c₃ + with ⪯⇔∃ .Equivalence.to c₁↯sl⪯c₂ | ⪯⇔∃ .Equivalence.to c₂↯sl⪯c₃ +... | c₄ , c₄+c₁↯sl≡c₂ | c₅ , c₅++c₂↯sl≡c₃ + = ⪯⇔∃ .Equivalence.from (c₅ ++ prune sl c₄ , [c₅+c₄↯sl]+c₁↯sl≡c₃) + where + [c₅+c₄↯sl]+c₁↯sl≡c₃ : (c₅ ++ prune sl c₄) ++ prune sl c₁ ≡ c₃ + [c₅+c₄↯sl]+c₁↯sl≡c₃ = let open ≡-Reasoning in begin + (c₅ ++ prune sl c₄) ++ prune sl c₁ ≡⟨ cong ((c₅ ++ prune sl c₄) ++_) (sym $ L.filter-idem _ c₁) ⟩ + (c₅ ++ prune sl c₄) ++ prune sl (prune sl c₁) ≡⟨ L.++-assoc c₅ _ _ ⟩ + c₅ ++ prune sl c₄ ++ prune sl (prune sl c₁) ≡⟨ cong (c₅ ++_) (sym $ L.filter-++ _ c₄ _) ⟩ + c₅ ++ prune sl (c₄ ++ prune sl c₁) ≡⟨ cong (λ ◆ → c₅ ++ prune sl ◆) c₄+c₁↯sl≡c₂ ⟩ + c₅ ++ prune sl c₂ ≡⟨ c₅++c₂↯sl≡c₃ ⟩ + c₃ ∎ + +{- +instance + + ProperlyLinked? : ProperlyLinked ⁇¹ + ProperlyLinked? {[]} .dec = no id + ProperlyLinked? {[ b ]} .dec = b ≟ genesisBlock + ProperlyLinked? {b ∷ b′ ∷ c} .dec = ¿ b ⟵ b′ ¿ ×-dec ProperlyLinked? {b′ ∷ c} .dec +-} + +ProperlyLinked⇒≢[] : ∀ {c : Chain} → ProperlyLinked c → c ≢ [] +ProperlyLinked⇒≢[] {_ ∷ _} _ = λ () + +ProperlyLinked⇒gbIsHead : ∀ {c : Chain} → ProperlyLinked c → ∃[ c′ ] c′ L.∷ʳ genesisBlock ≡ c +ProperlyLinked⇒gbIsHead {[ b ]} b≡gb rewrite b≡gb = [] , refl +ProperlyLinked⇒gbIsHead {b ∷ b′ ∷ c} pl with ProperlyLinked⇒gbIsHead {b′ ∷ c} (pl .proj₂) +... | c′ , pl′ = b ∷ c′ , cong (b ∷_) pl′ + +ProperlyLinked-++⁻ : ∀ c {c′} → c′ ≢ [] → ProperlyLinked (c ++ c′) → ProperlyLinked c′ +ProperlyLinked-++⁻ [] {_} _ p2 = p2 +ProperlyLinked-++⁻ [ _ ] {[]} p1 _ = contradiction refl p1 +ProperlyLinked-++⁻ [ _ ] {_ ∷ _} _ p2 = p2 .proj₂ +ProperlyLinked-++⁻ (b ∷ b′ ∷ c) {c′} p1 p2 = ProperlyLinked-++⁻ (b′ ∷ c) {c′} p1 (p2 .proj₂) + +open import Data.List.Relation.Unary.AllPairs +open import Data.List.Relation.Unary.Linked.Properties using (Linked⇒AllPairs; AllPairs⇒Linked) +open import Data.List.Relation.Unary.AllPairs.Properties.Ext using (++⁻) + +++-DecreasingSlots : ∀ {c c′ : Chain} → DecreasingSlots (c ++ c′) → DecreasingSlots c × DecreasingSlots c′ × L.All.All (λ b → L.All.All (b >ˢ_) c′) c +++-DecreasingSlots {c} {c′} p with ++⁻ {xs = c} {ys = c′} $ Linked⇒AllPairs (λ {b b′ b″} → >ˢ-trans {b} {b′} {b″}) p +... | (p₁ , p₂ , p₃) = (AllPairs⇒Linked p₁ , AllPairs⇒Linked p₂ , p₃) + +∷-DecreasingSlots : ∀ {c : Chain} {b : Block} → DecreasingSlots (b ∷ c) → DecreasingSlots c × L.All.All (b >ˢ_) c +∷-DecreasingSlots {c} {b} p with ++-DecreasingSlots {c = [ b ]} {c′ = c} p +... | (_ , p₂ , p₃) = p₂ , L.All.head p₃ + +DecreasingSlots⇒UniqueSlots : ∀ {c : Chain} → DecreasingSlots c → Unique (L.map slot c) +DecreasingSlots⇒UniqueSlots {[]} _ = AllPairs.[] +DecreasingSlots⇒UniqueSlots {b ∷ c} ds[b∷c] with ∷-DecreasingSlots ds[b∷c] +... | ds[c] , b>ˢc = L.All.map⁺ (L.All.map Nat.>⇒≢ b>ˢc) AllPairs.∷ DecreasingSlots⇒UniqueSlots ds[c] + +nonAdjacentBlocksDecreasingSlots : ∀ {cₕ cₘ cₜ : Chain} {b₁ b₂ : Block} → + DecreasingSlots (cₕ ++ b₁ ∷ cₘ ++ b₂ ∷ cₜ) + → b₁ >ˢ b₂ +nonAdjacentBlocksDecreasingSlots {cₕ} {cₘ} {cₜ} {b₁} {b₂} dsπ = + dsπ ∶ + DecreasingSlots (cₕ ++ b₁ ∷ cₘ ++ b₂ ∷ cₜ) + |> proj₁ ∘ proj₂ ∘ ++-DecreasingSlots {cₕ} ∶ + DecreasingSlots (b₁ ∷ cₘ ++ b₂ ∷ cₜ) + |> proj₂ ∘ ∷-DecreasingSlots ∶ + L.All.All (b₁ >ˢ_) (cₘ ++ b₂ ∷ cₜ) + |> L.All.++⁻ʳ cₘ ∶ + L.All.All (b₁ >ˢ_) (b₂ ∷ cₜ) + |> L.All.head ∶ + b₁ >ˢ b₂ + where open import Function.Reasoning + +DecreasingSlots-∈ : ∀ {c c′ : Chain} {b b′ : Block} → DecreasingSlots (c ++ c′) → b ∈ c → b′ ∈ c′ → b >ˢ b′ +DecreasingSlots-∈ {c} {c′} {b} {b′} ds[c++c′] b∈c b′∈c′ with L.Mem.∈-∃++ b∈c | L.Mem.∈-∃++ b′∈c′ +... | cₕ , cₜ , c≡cₕ+b+cₜ | cₕ′ , cₜ′ , c′≡cₕ′+b′+cₜ′ = nonAdjacentBlocksDecreasingSlots ds + where + open ≡-Reasoning + + eq : (cₕ ++ b ∷ cₜ) ++ (cₕ′ ++ b′ ∷ cₜ′) ≡ cₕ ++ b ∷ (cₜ ++ cₕ′) ++ b′ ∷ cₜ′ + eq = begin + (cₕ ++ b ∷ cₜ) ++ (cₕ′ ++ b′ ∷ cₜ′) ≡⟨ L.++-assoc _ (b ∷ cₜ) _ ⟩ + cₕ ++ b ∷ (cₜ ++ (cₕ′ ++ b′ ∷ cₜ′)) ≡⟨ cong ((cₕ ++_) ∘ (b ∷_)) (sym $ L.++-assoc cₜ cₕ′ _) ⟩ + cₕ ++ b ∷ (cₜ ++ cₕ′) ++ b′ ∷ cₜ′ ∎ + + ds : DecreasingSlots (cₕ ++ b ∷ (cₜ ++ cₕ′) ++ b′ ∷ cₜ′) + ds rewrite c≡cₕ+b+cₜ | c′≡cₕ′+b′+cₜ′ | sym eq = ds[c++c′] opaque unfolding _✓ + ✓⇒cb : ∀ {c : Chain} → c ✓ → CorrectBlocks c + ✓⇒cb (cb , _ , _) = cb + + ✓⇒ds : ∀ {c : Chain} → c ✓ → DecreasingSlots c + ✓⇒ds (_ , _ , ds) = ds + + ✓⇒≢[] : ∀ {c : Chain} → c ✓ → c ≢ [] + ✓⇒≢[] (_ , pl , _) = ProperlyLinked⇒≢[] pl + + ✓⇒gbIsHead : ∀ {c : Chain} → c ✓ → ∃[ c′ ] c′ L.∷ʳ genesisBlock ≡ c + ✓⇒gbIsHead (_ , pl , _) = ProperlyLinked⇒gbIsHead pl + + ✓-∷ : ∀ {b b′ : Block} {c : Chain} → (CorrectBlock b × b ⟵ b′ × b >ˢ b′ × (b′ ∷ c) ✓) ⇔ (b ∷ b′ ∷ c) ✓ + ✓-∷ {b} {b′} {c} = mk⇔ to′ from′ + where + to′ : CorrectBlock b × b ⟵ b′ × b >ˢ b′ × (b′ ∷ c) ✓ → (b ∷ b′ ∷ c) ✓ + to′ (cbb , b⟵b′ , b>b′ , cb[b′∷c] , pl[b′∷c] , ds[b′∷c]) = cbb ∷ cb[b′∷c] , (b⟵b′ , pl[b′∷c]) , b>b′ ∷ ds[b′∷c] + + from′ : ∀ {c : Chain} → (b ∷ b′ ∷ c) ✓ → CorrectBlock b × b ⟵ b′ × b >ˢ b′ × (b′ ∷ c) ✓ + from′ {[]} (cbb ∷ cb[b′] , (b⟵b′ , b′≡gb) , b>b′ ∷ ds[b′]) = cbb , b⟵b′ , b>b′ , (cb[b′] , b′≡gb , ds[b′]) + from′ {b″ ∷ c′} (cbb ∷ cb[b′∷b″∷c′] , (b⟵b′ , pl[b′∷b″∷c′]) , b>b′ ∷ ds[b′∷b″∷c′]) = cbb , b⟵b′ , b>b′ , (cb[b′∷b″∷c′] , pl[b′∷b″∷c′] , ds[b′∷b″∷c′]) + + open Function.Bundles.Equivalence using (from) + + ✓-++ʳ : ∀ {b : Block} {c c′ : Chain} → (c ++ b ∷ c′) ✓ → (b ∷ c′) ✓ + ✓-++ʳ {b} {[]} {c′} p = p + ✓-++ʳ {b} {[ b′ ]} {c′} p = from ✓-∷ p .proj₂ .proj₂ .proj₂ + ✓-++ʳ {b} {b′ ∷ b″ ∷ c} {c′} p = ✓-++ʳ {b} {b″ ∷ c} {c′} (from ✓-∷ p .proj₂ .proj₂ .proj₂) + + ✓⇒gb⪯ : ∀ {c : Chain} → c ✓ → [ genesisBlock ] ⪯ c + ✓⇒gb⪯ c✓ = let c′ , c′∷gb≡c = ✓⇒gbIsHead c✓ in subst ([ genesisBlock ] ⪯_) c′∷gb≡c $ ⪯-++ [ genesisBlock ] c′ + + tip-∈ : ∀ {c : Chain} → c ✓ → tip c ∈ c + tip-∈ {[]} p = contradiction p $ contraposition (✓⇒≢[] {[]}) (contradiction refl) + tip-∈ {b ∷ c} p = x∈x∷xs c + + pruneIdentity : ∀ {c : Chain} {b : Block} {sl : Slot} → + b .slot ≤ sl + → DecreasingSlots (b ∷ c) + → prune sl (b ∷ c) ≡ b ∷ c + pruneIdentity {c} {b} {sl} bₜ≤sl ds[b+c] + rewrite + L.filter-accept ((_≤? sl) ∘ slot) {x = b} {xs = c} bₜ≤sl + = cong (b ∷_) (goal p) + where + p : L.All.All (_>ˢ_ b) c + p = ∷-DecreasingSlots ds[b+c] .proj₂ + + goal : ∀ {c : Chain} → L.All.All (_>ˢ_ b) c → prune sl c ≡ c + goal {[]} _ = refl + goal {b′ ∷ c′} p = let open ≡-Reasoning in begin + prune sl (b′ ∷ c′) ≡⟨ L.filter-accept ((_≤? sl) ∘ slot) {x = b′} {xs = c′} b′ₜ≤sl ⟩ + b′ ∷ prune sl c′ ≡⟨ cong (b′ ∷_) ih ⟩ + b′ ∷ c′ ∎ + where + ih : prune sl c′ ≡ c′ + ih = goal {c′} (L.All.tail p) + + b′ₜ≤sl : b′ .slot ≤ sl + b′ₜ≤sl = Nat.<⇒≤ $ Nat.<-≤-trans (L.All.head p) bₜ≤sl + + prune-⪯ : ∀ {c : Chain} (sl : Slot) → DecreasingSlots c → prune sl c ⪯ c + prune-⪯ {[]} _ _ = ⪯-refl + prune-⪯ {b′ ∷ c′} sl ds[b′+c] with b′ .slot ≤? sl + ... | yes b′ₜ≤sl rewrite pruneIdentity b′ₜ≤sl ds[b′+c] = ⪯-refl + ... | no b′ₜ≰sl rewrite L.filter-reject ((_≤? sl) ∘ slot) {x = b′} {xs = c′} b′ₜ≰sl = ⪯-trans ih (⪯-++ c′ [ b′ ]) + where + ih : prune sl c′ ⪯ c′ + ih = prune-⪯ {c′} sl (∷-DecreasingSlots ds[b′+c] .proj₁) + [b]✓⇔b≡gb : ∀ {b : Block} → [ b ] ✓ ⇔ b ≡ genesisBlock - [b]✓⇔b≡gb = mk⇔ toπ fromπ + [b]✓⇔b≡gb = mk⇔ to′ from′ where - toπ : ∀ {b : Block} → [ b ] ✓ → b ≡ genesisBlock - toπ = proj₁ ∘ proj₂ + to′ : ∀ {b : Block} → [ b ] ✓ → b ≡ genesisBlock + to′ = proj₁ ∘ proj₂ - fromπ : ∀ {b : Block} → b ≡ genesisBlock → [ b ] ✓ - fromπ b≡gb rewrite b≡gb = genesisWinner ∷ [] , refl , [-] + from′ : ∀ {b : Block} → b ≡ genesisBlock → [ b ] ✓ + from′ b≡gb rewrite b≡gb = genesisWinner ∷ [] , refl , [-] [gb+c]✓⇔c≡[] : ∀ {c : Chain} → (genesisBlock ∷ c) ✓ ⇔ c ≡ [] - [gb+c]✓⇔c≡[] = mk⇔ toπ fromπ + [gb+c]✓⇔c≡[] = mk⇔ to′ from′ where - toπ : ∀ {c : Chain} → (genesisBlock ∷ c) ✓ → c ≡ [] - toπ {[]} _ = refl - toπ {b ∷ c} [gb∷b∷c]✓ = contradiction genesisBlockSlot (Nat.n>0⇒n≢0 $ Nat.m0⇒n≢0 $ Nat.m