The Protocol typeclass

.github/workflows/lean_action_ci.yml

@@ -12,3 +12,5 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: "src"

src/CsprConsensus.lean

@@ -1,3 +1,4 @@
 -- This module serves as the root of the `CsprConsensusFormal` library.
 -- Import modules here that should be built as part of the library.
-import «CsprConsensus».Basic
+import «CsprConsensus».Network
+import «CsprConsensus».Protocol

src/CsprConsensus/Network.lean

@@ -0,0 +1,36 @@
+import Mathlib.Data.Set.Finite
+
+class StateId (α : Type) extends Inhabited α, BEq α, Repr α, Fintype α
+
+variable {α : Type} [StateId α] [αFintype : Fintype α]
+
+structure Node where
+  id : α
+deriving Inhabited, DecidableEq
+
+theorem Node.mk_injective : @Function.Injective α  (@Node α) Node.mk := by apply Node.mk.inj
+def Node.mkEmbedding : Function.Embedding α (@Node α) := Function.Embedding.mk Node.mk Node.mk_injective
+
+instance nodeFintype : Fintype (@Node α) where
+  elems := Finset.map Node.mkEmbedding αFintype.elems
+  complete := by
+    intro x
+    apply Finset.mem_map.mpr
+    simp [Node.mkEmbedding]
+    exists x.id
+    apply And.intro
+    · apply αFintype.complete
+    · rfl
+
+structure Nodes where
+  collection : Set (@Node α)
+  collectionFintype : Fintype collection
+  invariant : (@Set.toFinset _ collection collectionFintype).card > 3
+
+def Nodes.card (nodes : @Nodes α) : Nat := (@Set.toFinset _ nodes.collection nodes.collectionFintype).card
+
+structure Network where
+  nodes : @Nodes α
+  faultTolerance : Nat
+  invariant : nodes.card > 3 * faultTolerance
+def Network.quorumSize (net : @Network α) : Nat := 1 + (net.nodes.card + net.faultTolerance) / 2

src/CsprConsensus/Protocol.lean

@@ -0,0 +1,23 @@
+import CsprConsensus.Network
+
+class Value (β : Type) extends Inhabited β, BEq β, Repr β
+
+class Protocol (β : Type) [Value β] where
+  input : @Network α → @Node α → Option β
+  output : @Network α -> @Node α -> Option β
+  is_correct : @Network α -> @Node α -> Prop
+  /-- continuation for eventual properties -/
+  eventually : (@Network α -> Prop) -> Prop
+  /-- If any correct node outputs v, every corect node will eventually output v -/
+  agreement : forall (net : @Network α) (n1 n2 : @Node α) (v : β),
+    is_correct net n1 -> is_correct net n2 ->
+    @output α net n1 = some v ->
+    @eventually α (fun _ => @output α net n2 = some v)
+
+instance BoolValue : Value Bool := by constructor
+
+class WBA extends Protocol Bool where
+  /-- If the correct nodes output b, more than q - f correct validators had input b -/
+  validity : 1 = 1 := by rfl -- TODO
+  /-- If more than q correct validators have input b, the correct nodes eventually output b -/
+  weak_termination : 1 = 1 := by rfl -- TODO

src/lake-manifest.json

@@ -65,11 +65,21 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a3e5a2839960926e0b846c1b6c9e711fc66c03e7",
+   "rev": "0a717792814730b6a63765a4bb194368ee23b173",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/cspr-rad/lean-test",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b41a35a3a35c85dbac64a9a6d54724563cc20b5c",
+   "name": "leantest",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«cspr-consensus»",
  "lakeDir": ".lake"}

src/lakefile.lean

@@ -5,7 +5,7 @@ require mathlib from git
   "https://github.com/leanprover-community/mathlib4"
 
 require leantest from git
-  "https://github.com/cspr-rad/leantest"
+  "https://github.com/cspr-rad/lean-test"
 
 package «cspr-consensus» where
   -- add package configuration options here