From c37941ada8c07b20d231c1fb60df9ac15f667c99 Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Thu, 30 Oct 2025 12:03:33 -0600
Subject: [PATCH 01/11] Switched to using lakefile.lean instead of
 lakefile.toml

---
 .gitignore                    |  1 +
 analysis/markov/lakefile.lean | 22 +++++++++++++++++++++
 analysis/markov/lakefile.toml | 36 -----------------------------------
 3 files changed, 23 insertions(+), 36 deletions(-)
 create mode 100644 analysis/markov/lakefile.lean
 delete mode 100644 analysis/markov/lakefile.toml

diff --git a/.gitignore b/.gitignore
index fa980dfaa..113f59ecc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,3 +29,4 @@ _build
 /simulation/docs/_minted-sim-realism/
 /data/simulation/*.trace.json
 /data/simulation/*.array.schema.json
+node_modules/
diff --git a/analysis/markov/lakefile.lean b/analysis/markov/lakefile.lean
new file mode 100644
index 000000000..587b9674d
--- /dev/null
+++ b/analysis/markov/lakefile.lean
@@ -0,0 +1,22 @@
+
+import Lake
+
+open Lake DSL
+
+package «linleios» where
+
+lean_lib «Linleios» where
+
+@[default_target]
+lean_exe «linleios» where
+  root := `Main
+  supportInterpreter := false
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4" @ "v4.20.0"
+
+require Parser from git
+  "https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
+
+require Cli from git
+  "https://github.com/mhuisi/lean4-cli" @ "v4.20.0"
diff --git a/analysis/markov/lakefile.toml b/analysis/markov/lakefile.toml
deleted file mode 100644
index b2a3c08ff..000000000
--- a/analysis/markov/lakefile.toml
+++ /dev/null
@@ -1,36 +0,0 @@
-name = "linleios"
-version = "0.1.0"
-keywords = ["math"]
-defaultTargets = ["linleios"]
-
-[[lean_lib]]
-name = "Linleios"
-
-[[lean_exe]]
-name = "linleios"
-root = "Main"
-
-[leanOptions]
-pp.unicode.fun = true # pretty-prints `fun a ↦ b`
-autoImplicit = false
-
-[[require]]
-name = "mathlib"
-scope = "leanprover-community"
-version = "git#v4.20.0"
-
-[[require]]
-name = "Parser"
-git = "https://github.com/fgdorais/lean4-parser"
-rev = "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
-
-[[require]]
-name = "Cli"
-git = "https://github.com/mhuisi/lean4-cli"
-rev = "v4.20.0"
-
-[lean]
-server-options = [
-  ["checkBinderAnnotations", "false"],
-  ["diagnostics", "true"]
-]

From 8df0408212c5e7d98939a88cc3b6d19641a1bfe5 Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Thu, 30 Oct 2025 12:06:21 -0600
Subject: [PATCH 02/11] Moved source files to src/

---
 analysis/markov/lakefile.lean                       | 2 ++
 analysis/markov/{ => src}/Linleios.lean             | 0
 analysis/markov/{ => src}/Linleios/Evolve.lean      | 0
 analysis/markov/{ => src}/Linleios/Probability.lean | 0
 analysis/markov/{ => src}/Linleios/Types.lean       | 0
 analysis/markov/{ => src}/Linleios/Util.lean        | 0
 analysis/markov/{ => src}/Main.lean                 | 0
 7 files changed, 2 insertions(+)
 rename analysis/markov/{ => src}/Linleios.lean (100%)
 rename analysis/markov/{ => src}/Linleios/Evolve.lean (100%)
 rename analysis/markov/{ => src}/Linleios/Probability.lean (100%)
 rename analysis/markov/{ => src}/Linleios/Types.lean (100%)
 rename analysis/markov/{ => src}/Linleios/Util.lean (100%)
 rename analysis/markov/{ => src}/Main.lean (100%)

diff --git a/analysis/markov/lakefile.lean b/analysis/markov/lakefile.lean
index 587b9674d..347460408 100644
--- a/analysis/markov/lakefile.lean
+++ b/analysis/markov/lakefile.lean
@@ -6,10 +6,12 @@ open Lake DSL
 package «linleios» where
 
 lean_lib «Linleios» where
+  srcDir := "src"
 
 @[default_target]
 lean_exe «linleios» where
   root := `Main
+  srcDir := "src"
   supportInterpreter := false
 
 require mathlib from git
diff --git a/analysis/markov/Linleios.lean b/analysis/markov/src/Linleios.lean
similarity index 100%
rename from analysis/markov/Linleios.lean
rename to analysis/markov/src/Linleios.lean
diff --git a/analysis/markov/Linleios/Evolve.lean b/analysis/markov/src/Linleios/Evolve.lean
similarity index 100%
rename from analysis/markov/Linleios/Evolve.lean
rename to analysis/markov/src/Linleios/Evolve.lean
diff --git a/analysis/markov/Linleios/Probability.lean b/analysis/markov/src/Linleios/Probability.lean
similarity index 100%
rename from analysis/markov/Linleios/Probability.lean
rename to analysis/markov/src/Linleios/Probability.lean
diff --git a/analysis/markov/Linleios/Types.lean b/analysis/markov/src/Linleios/Types.lean
similarity index 100%
rename from analysis/markov/Linleios/Types.lean
rename to analysis/markov/src/Linleios/Types.lean
diff --git a/analysis/markov/Linleios/Util.lean b/analysis/markov/src/Linleios/Util.lean
similarity index 100%
rename from analysis/markov/Linleios/Util.lean
rename to analysis/markov/src/Linleios/Util.lean
diff --git a/analysis/markov/Main.lean b/analysis/markov/src/Main.lean
similarity index 100%
rename from analysis/markov/Main.lean
rename to analysis/markov/src/Main.lean

From 3d3323b2b58acab0bb669e415439bf0d9a8ddedd Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Thu, 30 Oct 2025 12:26:06 -0600
Subject: [PATCH 03/11] Restored some options to lake file

---
 analysis/markov/lakefile.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/analysis/markov/lakefile.lean b/analysis/markov/lakefile.lean
index 347460408..8f9863ee2 100644
--- a/analysis/markov/lakefile.lean
+++ b/analysis/markov/lakefile.lean
@@ -4,6 +4,16 @@ import Lake
 open Lake DSL
 
 package «linleios» where
+  version := StdVer.mk (SemVerCore.mk 0 1 0) ""
+  leanOptions := #[
+    -- pretty-prints `fun a ↦ b`
+    ⟨`pp.unicode.fun, true⟩,
+    -- disables automatic implicit arguments
+    ⟨`autoImplicit, false⟩,
+  ]
+  moreServerOptions := #[
+    ⟨`trace.debug, true⟩,
+  ]
 
 lean_lib «Linleios» where
   srcDir := "src"

From e6b39b88d2f86a5f573e205cee235fcf484a21bf Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Thu, 30 Oct 2025 14:27:25 -0600
Subject: [PATCH 04/11] Tidied up function definitions

---
 analysis/markov/src/Linleios/Evolve.lean |  3 ++-
 analysis/markov/src/Linleios/Types.lean  | 12 +-----------
 2 files changed, 3 insertions(+), 12 deletions(-)

diff --git a/analysis/markov/src/Linleios/Evolve.lean b/analysis/markov/src/Linleios/Evolve.lean
index 39e25d049..e6de7fe47 100644
--- a/analysis/markov/src/Linleios/Evolve.lean
+++ b/analysis/markov/src/Linleios/Evolve.lean
@@ -110,7 +110,7 @@ def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat →
 Compute the total probabilities of a set of states.
 -/
 def totalProbability (states : Probabilities) : Probability :=
-  states.values.sum
+  states.fold (Function.const State ∘ Add.add) 0
 
 /--
 Compute the distribution of EB counts.
@@ -119,6 +119,7 @@ def ebDistribution : Probabilities → HashMap Nat Probability :=
   HashMap.fold
     (
       fun acc state p =>
+        -- FIXME: Rewrite using `Function.const`.
         HashMap.mergeWith (fun _ => Add.add) acc
           $ singleton ⟨ state.ebCount , p ⟩
     )
diff --git a/analysis/markov/src/Linleios/Types.lean b/analysis/markov/src/Linleios/Types.lean
index 0cc4df299..e23876262 100644
--- a/analysis/markov/src/Linleios/Types.lean
+++ b/analysis/markov/src/Linleios/Types.lean
@@ -74,17 +74,6 @@ structure State where
   canCertify : Bool
 deriving Repr, BEq, Hashable, Inhabited
 
-/--
-The genesis state starts when zero counts.
--/
-theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
-  constructor
-  rfl
-  constructor
-  rfl
-  rfl
-
-
 /--
 The active states and their probabilities.
 -/
@@ -92,6 +81,7 @@ def Probabilities := HashMap State Probability
 deriving Repr, EmptyCollection
 
 instance : Inhabited Probabilities where
+  -- TODO: Rewrite using `Singleton.singleton`.
   default := (∅ : Probabilities).insert Inhabited.default 1
 
 

From 694b3a9de0862d3321ac6ad1dd2c98292365cac5 Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Thu, 30 Oct 2025 14:27:40 -0600
Subject: [PATCH 05/11] Work in progress on property-based tests

---
 analysis/markov/lake-manifest.json    | 10 ++++++++++
 analysis/markov/lakefile.lean         |  9 ++++++++-
 analysis/markov/src/LinleiosTest.lean | 24 ++++++++++++++++++++++++
 3 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 analysis/markov/src/LinleiosTest.lean

diff --git a/analysis/markov/lake-manifest.json b/analysis/markov/lake-manifest.json
index e8e8006b8..f0b3272d6 100644
--- a/analysis/markov/lake-manifest.json
+++ b/analysis/markov/lake-manifest.json
@@ -21,6 +21,16 @@
    "inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/argumentcomputer/LSpec.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d2bbbfa61a82ac199a5e852aa375acffd9a3b3f1",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
diff --git a/analysis/markov/lakefile.lean b/analysis/markov/lakefile.lean
index 8f9863ee2..58a214a45 100644
--- a/analysis/markov/lakefile.lean
+++ b/analysis/markov/lakefile.lean
@@ -1,10 +1,10 @@
-
 import Lake
 
 open Lake DSL
 
 package «linleios» where
   version := StdVer.mk (SemVerCore.mk 0 1 0) ""
+  testDriver := "linleios_test"
   leanOptions := #[
     -- pretty-prints `fun a ↦ b`
     ⟨`pp.unicode.fun, true⟩,
@@ -24,9 +24,16 @@ lean_exe «linleios» where
   srcDir := "src"
   supportInterpreter := false
 
+lean_exe «linleios_test» where
+  root := `LinleiosTest
+  srcDir := "src"
+
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4" @ "v4.20.0"
 
+require LSpec from git
+  "https://github.com/argumentcomputer/LSpec.git"
+
 require Parser from git
   "https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
 
diff --git a/analysis/markov/src/LinleiosTest.lean b/analysis/markov/src/LinleiosTest.lean
new file mode 100644
index 000000000..71318e658
--- /dev/null
+++ b/analysis/markov/src/LinleiosTest.lean
@@ -0,0 +1,24 @@
+import Linleios
+import Std.Data.HashMap
+
+open Std.HashMap (singleton_eq_insert)
+
+
+/--
+The genesis state starts with zero counts.
+-/
+theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
+  constructor
+  rfl
+  constructor
+  rfl
+  rfl
+
+/-
+The initial probability is unity.
+-/
+#guard totalProbability (default : Probabilities) == 1
+
+
+def main : IO Unit :=
+  pure ()

From dc50f42d626951e568566c9d6ae3f89741e1eb6f Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Fri, 31 Oct 2025 10:07:30 -0600
Subject: [PATCH 06/11] Fixed LSpec dependency

---
 analysis/markov/lake-manifest.json | 8 ++++----
 analysis/markov/lakefile.lean      | 4 +++-
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/analysis/markov/lake-manifest.json b/analysis/markov/lake-manifest.json
index f0b3272d6..9ce246de9 100644
--- a/analysis/markov/lake-manifest.json
+++ b/analysis/markov/lake-manifest.json
@@ -21,20 +21,20 @@
    "inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/argumentcomputer/LSpec.git",
+  {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d2bbbfa61a82ac199a5e852aa375acffd9a3b3f1",
+   "rev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
+   "scope": "",
    "rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
diff --git a/analysis/markov/lakefile.lean b/analysis/markov/lakefile.lean
index 58a214a45..130e4e351 100644
--- a/analysis/markov/lakefile.lean
+++ b/analysis/markov/lakefile.lean
@@ -10,6 +10,8 @@ package «linleios» where
     ⟨`pp.unicode.fun, true⟩,
     -- disables automatic implicit arguments
     ⟨`autoImplicit, false⟩,
+    -- suppresses the checkBinderAnnotations error/warning
+    ⟨`checkBinderAnnotations, false⟩,
   ]
   moreServerOptions := #[
     ⟨`trace.debug, true⟩,
@@ -32,7 +34,7 @@ require mathlib from git
   "https://github.com/leanprover-community/mathlib4" @ "v4.20.0"
 
 require LSpec from git
-  "https://github.com/argumentcomputer/LSpec.git"
+  "https://github.com/argumentcomputer/LSpec" @ "24cceb69c20fadca0fd3acabe39fa9270dfb47e6"
 
 require Parser from git
   "https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"

From 67558d65177043ad6fc69fbca49c18af7177e080 Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Fri, 31 Oct 2025 13:50:58 -0600
Subject: [PATCH 07/11] Work in progress on property-based tests

---
 analysis/markov/src/LinleiosTest.lean | 144 +++++++++++++++++++++++++-
 1 file changed, 141 insertions(+), 3 deletions(-)

diff --git a/analysis/markov/src/LinleiosTest.lean b/analysis/markov/src/LinleiosTest.lean
index 71318e658..5da0621ed 100644
--- a/analysis/markov/src/LinleiosTest.lean
+++ b/analysis/markov/src/LinleiosTest.lean
@@ -1,9 +1,13 @@
 import Linleios
+import LSpec
 import Std.Data.HashMap
 
+open LSpec
 open Std.HashMap (singleton_eq_insert)
 
 
+-- Lemmas, in lieu of tests
+
 /--
 The genesis state starts with zero counts.
 -/
@@ -14,11 +18,145 @@ theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0
   rfl
   rfl
 
-/-
-The initial probability is unity.
+
+-- Generators
+
+structure RangedNat (lo hi : Nat) where
+  value: Nat
+deriving Repr
+
+instance {lo hi : Nat} : SlimCheck.Shrinkable (RangedNat lo hi) where
+  shrink _ := []
+
+instance {lo hi : Nat} : SlimCheck.SampleableExt (RangedNat lo hi) :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    RangedNat.mk <$> SlimCheck.Gen.choose Nat lo hi
+
+instance : SlimCheck.Random Float where
+  randomR lo hi :=
+    do
+      let res := 1000
+      let lo' := (lo * res).ceil.toUInt16.toNat
+      let hi' := (hi * res).floor.toUInt16.toNat
+      let i ← SlimCheck.Random.randomR lo' hi'
+      pure $ i.toFloat / res
+
+structure RangedFloat (lo hi : Float) where
+  value: Float
+deriving Repr
+
+instance {lo hi : Float} : SlimCheck.Shrinkable (RangedFloat lo hi) where
+  shrink _ := []
+
+instance {lo hi : Float} : SlimCheck.SampleableExt (RangedFloat lo hi) :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    RangedFloat.mk <$> SlimCheck.Gen.choose Float lo hi
+
+instance : SlimCheck.Shrinkable Environment where
+  shrink _ := []
+
+instance : SlimCheck.SampleableExt Environment :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    do
+      let Lheader : Nat ← SlimCheck.Gen.choose Nat 1 3
+      let Lvote ← SlimCheck.Gen.choose Nat 2 6
+      let Ldiff ← SlimCheck.Gen.choose Nat 0 8
+      let activeSlotCoefficient : Float ← SlimCheck.Gen.choose Float 0.01 0.05
+      let committeeSize ← SlimCheck.Gen.choose Nat 100 800
+      let τ ← SlimCheck.Gen.choose Float 0.51 0.99
+      let pRbHeaderArrives ← SlimCheck.Gen.choose Float 0.90 1.00
+      let pEbValidates ← SlimCheck.Gen.choose Float 0.85 1.00
+      let pEbUnvalidated ← SlimCheck.Gen.choose Float 0.00 0.15
+      let fAdversary ← SlimCheck.Gen.choose Float 0.00 0.49
+      pure $
+        makeEnvironment
+          Lheader Lvote Ldiff
+          activeSlotCoefficient
+          committeeSize.toFloat τ
+          pRbHeaderArrives pEbValidates pEbUnvalidated
+          fAdversary
+
+instance : SlimCheck.Shrinkable State where
+  shrink _ := []
+
+instance : SlimCheck.SampleableExt State :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    do
+      let clock ← SlimCheck.Gen.choose Nat 0 1000
+      let rbCount ← SlimCheck.Gen.choose Nat 0 clock
+      let ebCount ← SlimCheck.Gen.choose Nat 0 rbCount
+      let hasRb ← SlimCheck.Gen.chooseAny Bool
+      let canCertify ← Bool.and hasRb <$> SlimCheck.Gen.chooseAny Bool
+      pure $ State.mk clock rbCount ebCount hasRb canCertify
+
+
+-- Property-based tests.
+
+/--
+Tolerance for floating-point operations.
 -/
-#guard totalProbability (default : Probabilities) == 1
+private def ε := 1e-6
 
+/--
+Check that a probability is close to unity.
+-/
+private def nearUnity (x : Float) : Bool := (x - 1).abs < ε
 
+/--
+Check that the total outcome is near unity.
+-/
+private def outcomeNearUnity (os : Outcomes) : Bool :=
+  nearUnity $  os.foldl (fun acc sp ↦ acc + sp.snd) 0
+
+#lspec
+    group "Probabilities" (
+      test "Initial probability is unity" (
+        totalProbability (default : Probabilities) == 1
+      )
+    )
+  $ group "Stake distribution" (
+      check "Stake fractions are positive" (
+        ∀ nPools : RangedNat 500 5000,
+        ((stakeDistribution nPools.value).map (fun x ↦ decide $ x > 0)).and
+      )
+    $ check "Stake fractions sum to unity" (
+        ∀ nPools : RangedNat 500 5000,
+        (nearUnity $ (stakeDistribution nPools.value).sum)
+      )
+    )
+  $ group "Quorum" (
+      check "All voters vote and all votes are received" (
+        ∀ τ : RangedFloat 1 999,
+        ∀ committeeSize : RangedNat 100 nPools,
+        (nearUnity $ pQuorum 1 committeeSize.value.toFloat τ.value)
+      )
+    )
+  $ group "Conservation of probability" (
+      check "Forging RB" (
+        ∀ env : Environment,
+        ∀ state : State,
+        (outcomeNearUnity $ @forgeRb env state)
+      )
+    $ check "Certifying" (
+        ∀ env : Environment,
+        ∀ state : State,
+        (outcomeNearUnity $ @certify env state)
+      )
+    $ check "Forging EB" (
+        ∀ env : Environment,
+        ∀ state : State,
+        (outcomeNearUnity $ @forgeEb env state)
+      )
+    $ check "Voting" (
+        ∀ env : Environment,
+        ∀ state : State,
+        (outcomeNearUnity $ @vote env state)
+      )
+    )
+
+
+/--
+Testing is done elsewhere in this file.
+-/
 def main : IO Unit :=
   pure ()

From c9df1a29b2e18c1ae84cddc30eb7f6a3beab4894 Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Fri, 31 Oct 2025 15:54:40 -0600
Subject: [PATCH 08/11] Test for simulation probabilities

---
 analysis/markov/src/LinleiosTest.lean | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/analysis/markov/src/LinleiosTest.lean b/analysis/markov/src/LinleiosTest.lean
index 5da0621ed..0a407f2da 100644
--- a/analysis/markov/src/LinleiosTest.lean
+++ b/analysis/markov/src/LinleiosTest.lean
@@ -126,8 +126,8 @@ private def outcomeNearUnity (os : Outcomes) : Bool :=
     )
   $ group "Quorum" (
       check "All voters vote and all votes are received" (
-        ∀ τ : RangedFloat 1 999,
-        ∀ committeeSize : RangedNat 100 nPools,
+        ∀ τ : RangedFloat 0.51 0.80,
+        ∀ committeeSize : RangedNat 100 800,
         (nearUnity $ pQuorum 1 committeeSize.value.toFloat τ.value)
       )
     )
@@ -152,9 +152,13 @@ private def outcomeNearUnity (os : Outcomes) : Bool :=
         ∀ state : State,
         (outcomeNearUnity $ @vote env state)
       )
+    $ check "Simulation" (
+        ∀ env : Environment,
+        ∀ steps : RangedNat 0 30,
+        (nearUnity ∘ totalProbability $ simulate env default 0 steps.value)
+      )
     )
 
-
 /--
 Testing is done elsewhere in this file.
 -/

From 4629cb416416b86bd0b3c1f2ef10084896beca1d Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Mon, 3 Nov 2025 08:01:26 -0700
Subject: [PATCH 09/11] Clarified definition of `pLate`

---
 analysis/markov/ReadMe.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/analysis/markov/ReadMe.md b/analysis/markov/ReadMe.md
index c7c26dd88..03ccb9860 100644
--- a/analysis/markov/ReadMe.md
+++ b/analysis/markov/ReadMe.md
@@ -54,7 +54,7 @@ Provided that a quorum of votes have endorsed the EB, the following conditions a
 Provided that an honest RB exists, an EB can be forged if the node has received the previous EB and computed the ledger state.
 
 - Because of their membership in the previous vote, a fraction $n_\text{comm} / n_\text{pools}$ of the pools have already updated their ledger state.
-- Of the pools not having voted on the block we define $p_\text{late}$ as the probability that the EB has arrived too late to compute the ledger state needed to produce the next EB.
+- We define $p_\text{late}$ as the probability that the EB has arrived too late to compute the ledger state needed to produce the next EB.
 
 
 ### Substep 4: Vote

From 7e91a84e45bc4d38e957f9f372f6965aae24754e Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Mon, 3 Nov 2025 08:17:48 -0700
Subject: [PATCH 10/11] Refactored file organization

---
 analysis/markov/src/Linleios.lean         |  1 +
 analysis/markov/src/Linleios/Evolve.lean  | 69 ------------------
 analysis/markov/src/Linleios/Metrics.lean | 85 +++++++++++++++++++++++
 analysis/markov/src/Linleios/Types.lean   |  6 ++
 4 files changed, 92 insertions(+), 69 deletions(-)
 create mode 100644 analysis/markov/src/Linleios/Metrics.lean

diff --git a/analysis/markov/src/Linleios.lean b/analysis/markov/src/Linleios.lean
index c48d5238b..1ca2b148b 100644
--- a/analysis/markov/src/Linleios.lean
+++ b/analysis/markov/src/Linleios.lean
@@ -1,4 +1,5 @@
 import Linleios.Evolve
+import Linleios.Metrics
 
 /-!
 # Linleios: a Markovian model of Linear Leios
diff --git a/analysis/markov/src/Linleios/Evolve.lean b/analysis/markov/src/Linleios/Evolve.lean
index e6de7fe47..62cf2b4e0 100644
--- a/analysis/markov/src/Linleios/Evolve.lean
+++ b/analysis/markov/src/Linleios/Evolve.lean
@@ -1,13 +1,9 @@
 
 import Std.Data.HashMap
-import Batteries.Lean.HashMap
-import Lean.Data.Json.FromToJson
 
 import Linleios.Types
 
 
-open Lean (Json)
-open Lean.ToJson (toJson)
 open Std (HashMap)
 
 
@@ -104,68 +100,3 @@ def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat →
 | 0     => start
 | n + 1 => let state' := prune ε $ chain (@step env) start
            simulate env state' ε n
-
-
-/--
-Compute the total probabilities of a set of states.
--/
-def totalProbability (states : Probabilities) : Probability :=
-  states.fold (Function.const State ∘ Add.add) 0
-
-/--
-Compute the distribution of EB counts.
--/
-def ebDistribution : Probabilities → HashMap Nat Probability :=
-  HashMap.fold
-    (
-      fun acc state p =>
-        -- FIXME: Rewrite using `Function.const`.
-        HashMap.mergeWith (fun _ => Add.add) acc
-          $ singleton ⟨ state.ebCount , p ⟩
-    )
-    ∅
-
-/--
-Format the distribution of EB counts as JSON.
--/
-def ebDistributionJson : Probabilities → Json :=
-  Json.mkObj
-    ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩)
-    ∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst))
-    ∘ HashMap.toList
-    ∘ ebDistribution
-
-/--
-Compute the RB efficiency, given a set of states.
--/
-def rbEfficiency (states : Probabilities) : Float :=
-  let clock := states.keys.head!.clock
-  let rbCount :=
-    HashMap.fold
-      (fun acc state p =>acc + state.rbCount.toFloat * p)
-      0
-      states
-  rbCount / clock.toFloat
-
-/--
-Compute the EB efficiency, given a set of states.
--/
-def ebEfficiency (states : Probabilities) : Float :=
-  let clock := states.keys.head!.clock
-  let ebCount :=
-    HashMap.fold
-      (fun acc state p =>acc + state.ebCount.toFloat * p)
-      0
-      states
-  ebCount / (clock.toFloat - 1)
-
-/--
-Compute the overall efficiency, give a set of states.
--/
-def efficiency (states : Probabilities) : Float :=
-  let rb := rbEfficiency states
-  let eb := ebEfficiency states
-  let rbSize := 0.9
-  let ebSize := 12.0
-  let ρ := ebSize / rbSize
-  (rb * (1 - eb) + ρ * eb) / (1 + ρ)
diff --git a/analysis/markov/src/Linleios/Metrics.lean b/analysis/markov/src/Linleios/Metrics.lean
new file mode 100644
index 000000000..869a6bd64
--- /dev/null
+++ b/analysis/markov/src/Linleios/Metrics.lean
@@ -0,0 +1,85 @@
+import Std.Data.HashMap
+import Batteries.Lean.HashMap
+import Lean.Data.Json.FromToJson
+
+import Linleios.Types
+
+import Linleios.Probability
+import Linleios.Evolve
+
+open Lean (Json)
+open Lean.ToJson (toJson)
+open Std (HashMap)
+
+
+/--
+Compute the total probabilities of a set of states.
+-/
+def totalProbability (states : Probabilities) : Probability :=
+  states.fold (Function.const State ∘ Add.add) 0
+
+/--
+Compute the distribution of EB counts.
+-/
+def ebDistribution : Probabilities → HashMap Nat Probability :=
+  HashMap.fold
+    (
+      fun acc state p =>
+        -- FIXME: Rewrite using `Function.const`.
+        HashMap.mergeWith (fun _ => Add.add) acc
+          $ singleton ⟨ state.ebCount , p ⟩
+    )
+    ∅
+
+/--
+Format the distribution of EB counts as JSON.
+-/
+def ebDistributionJson : Probabilities → Json :=
+  Json.mkObj
+    ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩)
+    ∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst))
+    ∘ HashMap.toList
+    ∘ ebDistribution
+
+/--
+Compute the RB efficiency, given a set of states.
+-/
+def rbEfficiency (states : Probabilities) : Float :=
+  let clock := states.keys.head!.clock
+  let rbCount :=
+    HashMap.fold
+      (fun acc state p =>acc + state.rbCount.toFloat * p)
+      0
+      states
+  rbCount / clock.toFloat
+
+/--
+Compute the EB efficiency, given a set of states.
+-/
+def ebEfficiency (states : Probabilities) : Float :=
+  let clock := states.keys.head!.clock
+  let ebCount :=
+    HashMap.fold
+      (fun acc state p =>acc + state.ebCount.toFloat * p)
+      0
+      states
+  ebCount / (clock.toFloat - 1)
+
+/--
+Compute the overall efficiency, give a set of states.
+-/
+def efficiency (states : Probabilities) : Float :=
+  let rb := rbEfficiency states
+  let eb := ebEfficiency states
+  let rbSize := 0.9
+  let ebSize := 12.0
+  let ρ := ebSize / rbSize
+  (rb * (1 - eb) + ρ * eb) / (1 + ρ)
+
+
+#eval ebEfficiency (simulate {(default : Environment) with pLate := 0.1} default 0 30)
+#eval (0.95^13 * 0.9)
+
+#eval makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0.1
+#eval ebEfficiency (simulate (makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0.1) default 0 30)
+#eval (0.95^13 * 0.9)
diff --git a/analysis/markov/src/Linleios/Types.lean b/analysis/markov/src/Linleios/Types.lean
index e23876262..c8503672e 100644
--- a/analysis/markov/src/Linleios/Types.lean
+++ b/analysis/markov/src/Linleios/Types.lean
@@ -57,6 +57,12 @@ def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committee
     fAdversary := fAdversary
   }
 
+/--
+A perfect honest environment with the recommended protocol parameters.
+-/
+instance : Inhabited Environment where
+  default := makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0
+
 
 /--
 The state of the chain's evolution.

From 3e62adb42c190ff57939cce5ed91b261dd709e0a Mon Sep 17 00:00:00 2001
From: Brian W Bush <brian.bush@iohk.io>
Date: Mon, 3 Nov 2025 08:42:08 -0700
Subject: [PATCH 11/11] Added efficiency tests

---
 analysis/markov/src/Linleios/Metrics.lean | 11 ----
 analysis/markov/src/LinleiosTest.lean     | 70 ++++++++++++++++++++---
 2 files changed, 62 insertions(+), 19 deletions(-)

diff --git a/analysis/markov/src/Linleios/Metrics.lean b/analysis/markov/src/Linleios/Metrics.lean
index 869a6bd64..6056b01e8 100644
--- a/analysis/markov/src/Linleios/Metrics.lean
+++ b/analysis/markov/src/Linleios/Metrics.lean
@@ -4,9 +4,6 @@ import Lean.Data.Json.FromToJson
 
 import Linleios.Types
 
-import Linleios.Probability
-import Linleios.Evolve
-
 open Lean (Json)
 open Lean.ToJson (toJson)
 open Std (HashMap)
@@ -75,11 +72,3 @@ def efficiency (states : Probabilities) : Float :=
   let ebSize := 12.0
   let ρ := ebSize / rbSize
   (rb * (1 - eb) + ρ * eb) / (1 + ρ)
-
-
-#eval ebEfficiency (simulate {(default : Environment) with pLate := 0.1} default 0 30)
-#eval (0.95^13 * 0.9)
-
-#eval makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0.1
-#eval ebEfficiency (simulate (makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0.1) default 0 30)
-#eval (0.95^13 * 0.9)
diff --git a/analysis/markov/src/LinleiosTest.lean b/analysis/markov/src/LinleiosTest.lean
index 0a407f2da..e811d6071 100644
--- a/analysis/markov/src/LinleiosTest.lean
+++ b/analysis/markov/src/LinleiosTest.lean
@@ -97,10 +97,15 @@ Tolerance for floating-point operations.
 -/
 private def ε := 1e-6
 
+/--
+Check that a probability is near a specified value.
+-/
+private def nearValue (value x : Float) : Bool := (x - value).abs < ε
+
 /--
 Check that a probability is close to unity.
 -/
-private def nearUnity (x : Float) : Bool := (x - 1).abs < ε
+private def nearUnity : Float → Bool := nearValue 1
 
 /--
 Check that the total outcome is near unity.
@@ -121,43 +126,92 @@ private def outcomeNearUnity (os : Outcomes) : Bool :=
       )
     $ check "Stake fractions sum to unity" (
         ∀ nPools : RangedNat 500 5000,
-        (nearUnity $ (stakeDistribution nPools.value).sum)
+        nearUnity $ (stakeDistribution nPools.value).sum
       )
     )
   $ group "Quorum" (
       check "All voters vote and all votes are received" (
         ∀ τ : RangedFloat 0.51 0.80,
         ∀ committeeSize : RangedNat 100 800,
-        (nearUnity $ pQuorum 1 committeeSize.value.toFloat τ.value)
+        nearUnity $ pQuorum 1 committeeSize.value.toFloat τ.value
       )
     )
   $ group "Conservation of probability" (
       check "Forging RB" (
         ∀ env : Environment,
         ∀ state : State,
-        (outcomeNearUnity $ @forgeRb env state)
+        outcomeNearUnity $ @forgeRb env state
       )
     $ check "Certifying" (
         ∀ env : Environment,
         ∀ state : State,
-        (outcomeNearUnity $ @certify env state)
+        outcomeNearUnity $ @certify env state
       )
     $ check "Forging EB" (
         ∀ env : Environment,
         ∀ state : State,
-        (outcomeNearUnity $ @forgeEb env state)
+        outcomeNearUnity $ @forgeEb env state
       )
     $ check "Voting" (
         ∀ env : Environment,
         ∀ state : State,
-        (outcomeNearUnity $ @vote env state)
+        outcomeNearUnity $ @vote env state
       )
     $ check "Simulation" (
         ∀ env : Environment,
         ∀ steps : RangedNat 0 30,
-        (nearUnity ∘ totalProbability $ simulate env default 0 steps.value)
+        nearUnity ∘ totalProbability $ simulate env default 0 steps.value
       )
     )
+  $ group "EB distribution" (
+      check "Total probability is unity" (
+        ∀ env : Environment,
+        ∀ steps : RangedNat 0 30,
+        let states := simulate env default 0 steps.value
+        let ebDist := ebDistribution states
+        nearUnity $ ebDist.values.sum
+      )
+    )
+  $ group "Efficiency" (
+      group "RB efficiency" (
+        check "Honest environment" (
+          ∀ steps : RangedNat 1 30,
+          let states := simulate default default 0 steps.value
+          nearUnity $ rbEfficiency states
+        )
+      $ check "Adversarial environment" (
+          ∀ fAdversary : RangedFloat 0.01 0.49,
+          let env := {(default : Environment) with fAdversary := fAdversary.value}
+          let states := simulate env default 0 30
+          nearValue (1 - fAdversary.value) $ rbEfficiency states
+        )
+      )
+    $ group "EB efficiency" (
+        check "Ideal environment" (
+          let states := simulate default default 0 30
+          nearValue (0.95^13) $ ebEfficiency states
+        )
+      $ check "Quorum failure" (
+          ∀ τ : RangedFloat 0.90 1.00,
+          let env := makeEnvironment 1 4 7 0.05 600 τ.value 1 1 0 0
+          let states := simulate env default 0 30
+          nearValue (0.95^13 * env.pQuorum) $ ebEfficiency states
+        )
+      $ check "Late EB validation" (
+          ∀ pLate : RangedFloat 0.01 0.99,
+          let env := {(default : Environment) with pLate := pLate.value}
+          let states := simulate env default 0 30
+          nearValue (0.95^13 * (1 - pLate.value)) $ ebEfficiency states
+        )
+      $ check "Adversarial environment" (
+          ∀ fAdversary : RangedFloat 0.01 0.49,
+          let env := {(default : Environment) with fAdversary := fAdversary.value}
+          let states := simulate env default 0 30
+          nearValue (0.95^13 * (1 - fAdversary.value)^2) $ ebEfficiency states
+        )
+      )
+    )
+
 
 /--
 Testing is done elsewhere in this file.