Tidy up the safety proof

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
+

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 ];

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/<owner>/<repo>/archive/<rev>.tar.gz"
     }
 }

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

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
 

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 []           = []

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
 

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)

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 <? N .clock
                       ...   | yes bᵐₜ<Nₜ

src/Properties/Base/LocalState.agda

@@ -13,7 +13,7 @@ open import Protocol.Prelude
 open import Protocol.Crypto ⦃ params ⦄ using (Hashable); open Hashable ⦃ ... ⦄
 open import Protocol.Block ⦃ params ⦄
 open import Protocol.Chain ⦃ params ⦄
-open import Protocol.TreeType ⦃ params ⦄
+open import Protocol.Tree ⦃ params ⦄
 open import Protocol.Message ⦃ params ⦄
 open import Protocol.Network ⦃ params ⦄; open Envelope
 open import Protocol.Semantics ⦃ params ⦄ ⦃ assumptions ⦄

src/Properties/Base/Network.agda

@@ -73,12 +73,10 @@ opaque
           ...   | yes eᵣ≡p
                     rewrite
                       eϕ≡𝟘
-                    | L.filter-accept ¿ flip Immediate p ¿¹ {x = e} {xs = [≢𝟘,p′] es} (eϕ≡𝟘 , eᵣ≡p)
                       = cong (e ∷_) $ goal* es p≢p′
           ...   | no eᵣ≢p
                     rewrite
                       eϕ≡𝟘
-                    | L.filter-reject ¿ flip Immediate p ¿¹ {x = e} {xs = [≢𝟘,p′] es} (dec-de-morgan₂ (inj₂ eᵣ≢p))
                       = goal* es p≢p′
 
           goal : _ ⊢ N″ —[ p′ ]↓→ N′ → immediateMsgs p N′ ≡ immediateMsgs p N