Work in progress on probability of quorum

Author: bwbush

analysis/markov/Linleios/Evolve.lean

@@ -8,26 +8,40 @@ open Std (HashMap)
 abbrev Probability := Float
 
 
+def approxCommittee (committeeSize : Float) : Float × Float :=
+  let nPools : Nat := 2500
+  let stakes : List Float := (List.range nPools).map (fun k => ((k + 1).toFloat / nPools.toFloat)^10 - (k.toFloat / nPools.toFloat)^10)
+  let ps : List Float := stakes.map (fun s => 1 - Float.exp (- committeeSize * s))
+  let μ : Float := ps.sum
+  let σ := (ps.map (fun p => p * (1 - p))).sum.sqrt
+  ⟨ μ , σ ⟩
+
+
 structure Environment where
   activeSlotCoefficient : Probability
   Lheader : Nat
   Lvote : Nat
   Ldiff : Nat
   pSpacingOkay : Probability
+  pRbHeaderArrives : Probability
+  pEbValidates : Probability
 
-def makeEnvironment (activeSlotCoefficient : Float) (Lheader Lvote Ldiff : Nat) : Environment :=
+def makeEnvironment (activeSlotCoefficient pRbHeaderArrives pEbValidates : Float) (Lheader Lvote Ldiff : Nat) : Environment :=
   {
     activeSlotCoefficient := activeSlotCoefficient
     Lheader := Lheader
     Lvote := Lvote
     Ldiff := Ldiff
     pSpacingOkay := (1 - activeSlotCoefficient).pow (3 * Lheader + Lvote + Ldiff - 1).toFloat
+    pRbHeaderArrives := pRbHeaderArrives
+    pEbValidates := pEbValidates
   }
 
 
 structure State where
   rbCount : Nat
   ebCount : Nat
+  canCertify : Bool
 deriving Repr, BEq, Hashable, Inhabited
 
 example : (default : State).rbCount = 0 := rfl
@@ -42,27 +56,34 @@ instance : Inhabited Probabilities where
   default := (∅ : Probabilities).insert Inhabited.default 1
 
 
-def forge {env : Environment} (state : State) : List (State × Probability) :=
+abbrev Outcomes := List (State × Probability)
+
+
+def forge {env : Environment} (state : State) : Outcomes :=
+  let state' :=
+    {
+      state with
+      rbCount := state.rbCount + 1
+      canCertify := true
+    }
+  if state.canCertify
+    then [
+           ⟨{state' with ebCount := state.ebCount + 1}, env.pSpacingOkay⟩
+         , ⟨state', 1 - env.pSpacingOkay⟩
+         ]
+    else [(state', 1)]
+
+def validate {env : Environment} (state : State) : Outcomes :=
   [
-    ⟨
-      {
-        state with
-        rbCount := state.rbCount + 1
-      }
-    , 1 - env.pSpacingOkay
-    ⟩
-  , ⟨
-      {
-        state with
-        rbCount := state.rbCount + 1
-        ebCount := state.ebCount + 1
-      }
-    , env.pSpacingOkay
-    ⟩
+    (state, env.pRbHeaderArrives * env.pEbValidates)
+  , ({state with canCertify := false}, 1 - env.pRbHeaderArrives * env.pEbValidates)
   ]
 
+def step {env : Environment} : List (State → Outcomes) :=
+  [@forge env, @validate env]
+
 
-def evolve (transition : State → List (State × Probability)) : Probabilities → Probabilities :=
+def evolve (transition : State → Outcomes) : Probabilities → Probabilities :=
   HashMap.fold
     (
       fun acc state p =>
@@ -73,12 +94,18 @@ def evolve (transition : State → List (State × Probability)) : Probabilities
     )
     ∅
 
-def simulate (transition : State → List (State × Probability)) (start : Probabilities) : Nat → Probabilities
-  | 0     => start
-  | n + 1 => simulate transition (evolve transition start) n
+def chain (transitions : List (State → Outcomes)) : Probabilities → Probabilities :=
+  match transitions with
+  | [] => id
+  | (t :: ts) => chain ts ∘ evolve t
+
+def simulate (env : Environment) (start : Probabilities) : Nat → Probabilities
+| 0     => start
+| n + 1 => let state' := chain (@step env) start
+           simulate env state' n
 
 def prune (ε : Float) : Probabilities → Probabilities :=
-  HashMap.filter (fun _ p => p ≥ ε)
+  HashMap.filter (fun _ p => p > ε)
 
 def totalProbability (states : Probabilities) : Probability :=
   states.values.sum

analysis/markov/Main.lean

@@ -2,14 +2,14 @@
 import Linleios
 
 
-def env : Environment := makeEnvironment 0.05 1 4 7
+def env : Environment := makeEnvironment 0.05 0.95 0.90 1 4 7
 
 def s0 : Probabilities := default
-def sn := simulate (@forge env) s0 50
+def sn := simulate env s0 10
 def pn := totalProbability sn
 
 def main : IO Unit :=
   do
-    let print {α : Type} [Repr α]  (x : α) : IO Unit := IO.println $ (reprPrec x 0).pretty
-    print sn
+    let print {α : Type} [Repr α] (x : α) : IO Unit := IO.println (reprPrec x 0).pretty
+    print $ prune 0 sn
     print pn

analysis/sims/kernels.nix

@@ -33,6 +33,7 @@ in
       igraph
       lubridate
       mongolite
+      poibin
       quantreg
       RPostgres
       R_utils