Property-based tests for markovian model (#609)

* Switched to using lakefile.lean instead of lakefile.toml
* Moved source files to src/
* Tidied up function definitions
* Property-based tests
* Fixed LSpec dependency
* Clarified definition of `pLate`
* Refactored file organization
* Implemented FA sortition

Author: bwbush

.gitignore

@@ -29,3 +29,4 @@ _build
 /simulation/docs/_minted-sim-realism/
 /data/simulation/*.trace.json
 /data/simulation/*.array.schema.json
+node_modules/

analysis/markov/Linleios/Probability.lean

@@ -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

analysis/markov/ReadMe.md

@@ -21,10 +21,20 @@
    "inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/argumentcomputer/LSpec",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "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",

analysis/markov/lake-manifest.json

@@ -0,0 +1,43 @@
+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⟩,
+    -- disables automatic implicit arguments
+    ⟨`autoImplicit, false⟩,
+    -- suppresses the checkBinderAnnotations error/warning
+    ⟨`checkBinderAnnotations, false⟩,
+  ]
+  moreServerOptions := #[
+    ⟨`trace.debug, true⟩,
+  ]
+
+lean_lib «Linleios» where
+  srcDir := "src"
+
+@[default_target]
+lean_exe «linleios» where
+  root := `Main
+  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" @ "24cceb69c20fadca0fd3acabe39fa9270dfb47e6"
+
+require Parser from git
+  "https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
+
+require Cli from git
+  "https://github.com/mhuisi/lean4-cli" @ "v4.20.0"

analysis/markov/lakefile.lean

@@ -1,4 +1,5 @@
 import Linleios.Evolve
+import Linleios.Metrics
 
 /-!
 # Linleios: a Markovian model of Linear Leios

analysis/markov/lakefile.toml

@@ -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,67 +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.values.sum
-
-/--
-Compute the distribution of EB counts.
--/
-def ebDistribution : Probabilities → HashMap Nat Probability :=
-  HashMap.fold
-    (
-      fun acc state p =>
-        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 + ρ)

analysis/markov/Linleios.lean renamed to analysis/markov/src/Linleios.lean

@@ -0,0 +1,74 @@
+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)
+
+
+/--
+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 + ρ)

analysis/markov/Linleios/Evolve.lean renamed to analysis/markov/src/Linleios/Evolve.lean

@@ -0,0 +1,55 @@
+
+import Linleios.Util
+
+
+/--
+Number of stake pools.
+-/
+def nPools : Nat := 2500
+
+/--
+Sortition results.
+-/
+structure Sortition where
+  stake : Float
+  probability : Float
+deriving Repr
+
+/--
+Fait Accompli sortition.
+-/
+def faSortition (nPools n : Nat) : List Sortition :=
+  let S (i : Nat) := ((nPools - i + 1).toFloat / nPools.toFloat)^10 - ((nPools - i).toFloat / nPools.toFloat)^10
+  let ρ (i : Nat) := 1 - ((nPools - i).toFloat / nPools.toFloat)^10
+  let test (n i : Nat) : Bool := (1 - S i / ρ i)^2 < (n - i).toFloat / (n - i + 1).toFloat
+  let i := (List.range nPools).map $ Add.add 1
+  let ⟨ persistent , nonpersistent ⟩ := i.partition $ test n
+  let ρStar := ρ $ persistent.length + 1
+  let persistent' := persistent.map $ fun i ↦ {stake := S i, probability := 1}
+  let nonpersistent' :=
+    nonpersistent.map $ fun i ↦
+      let Si := S i
+      {stake := Si, probability := Si / ρStar}
+  persistent' ++ nonpersistent'
+
+/--
+Compute the mean and standard deviation of the committee size, given the probability of a successful vote and a target committee size.
+-/
+def voteDistribution (pSuccessfulVote : Float) (committeeSize : Nat) : Float × Float :=
+  let sortition := faSortition nPools committeeSize
+  let μ := (sortition.map $ fun s ↦ let p := s.probability * pSuccessfulVote; s.stake * p).sum
+  let σ := (sortition.map $ fun s ↦ let p := s.probability * pSuccessfulVote; (s.stake * s.stake * p * (1 - p))).sum.sqrt
+  ⟨ μ , σ ⟩
+
+/--
+Compute the probability of a quorum, given the probability of a successful vote, the target committee size, and the quorum fraction.
+-/
+def pQuorum (pSuccessfulVote committeeSize τ : Float) : Float :=
+  let ⟨ μ , σ ⟩ := voteDistribution pSuccessfulVote committeeSize.toUInt64.toNat
+  1 - cdfGaussian τ μ σ
+
+/--
+Compute a realistic stake distribution for the specified number of pools.
+-/
+def stakeDistribution (nPools : Nat) : List Float :=
+  (faSortition nPools 700).map Sortition.stake