Added code comments and documentation to markovian model

analysis/markov/Linleios.lean

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

analysis/markov/Linleios/Evolve.lean

@@ -11,6 +11,9 @@ open Lean.ToJson (toJson)
 open Std (HashMap)
 
 
+/--
+Try to forge an RB in this substep, given the state and environment.
+-/
 def forgeRb {env : Environment} (state : State) : Outcomes :=
   let state' :=
     {
@@ -23,6 +26,9 @@ def forgeRb {env : Environment} (state : State) : Outcomes :=
   , ({state' with hasRb := false, canCertify := false}, 1 - p)
   ]
 
+/--
+Try to include a certificate in the latest RB being forged in this substep, given the state and environment.
+-/
 def certify {env : Environment} (state : State) : Outcomes :=
   if state.hasRb && state.canCertify
     then let p := env.pSpacingOkay
@@ -32,6 +38,9 @@ def certify {env : Environment} (state : State) : Outcomes :=
          ]
     else [(state, 1)]
 
+/--
+Try to forge an EB in this substep, given the state and environment.
+-/
 def forgeEb {env : Environment} (state : State) : Outcomes :=
   if state.hasRb
     then let p := 1 - env.pLate
@@ -41,6 +50,9 @@ def forgeEb {env : Environment} (state : State) : Outcomes :=
          ]
     else [(state, 1)]
 
+/--
+Try to vote for an EB in this substep, given the state and environment.
+-/
 def vote {env : Environment} (state : State) : Outcomes :=
   if state.hasRb
     then let p := env.pQuorum
@@ -50,13 +62,22 @@ def vote {env : Environment} (state : State) : Outcomes :=
          ]
     else [(state, 1)]
 
+/--
+Step forward to the next potential block.
+-/
 def step {env : Environment} : List (State → Outcomes) :=
   [@forgeRb env, @certify env, @forgeEb env, @vote env]
 
 
+/--
+Discard probabilities below the specified threshold.
+-/
 def prune (ε : Float) : Probabilities → Probabilities :=
   HashMap.filter (fun _ p => p > ε)
 
+/--
+Evolve state probabilities on step forward according the a transition function.
+-/
 def evolve (transition : State → Outcomes) : Probabilities → Probabilities :=
   HashMap.fold
     (
@@ -68,19 +89,32 @@ def evolve (transition : State → Outcomes) : Probabilities → Probabilities :
     )
     ∅
 
+/--
+Chain a sequence of transitions sequentially, evolving probabilities.
+-/
 def chain (transitions : List (State → Outcomes)) : Probabilities → Probabilities :=
   match transitions with
   | [] => id
   | (t :: ts) => chain ts ∘ evolve t
 
+/--
+Simulate the specified number of potential blocks, given a starting set of probabilities.
+-/
 def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat → Probabilities
 | 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
     (
@@ -90,13 +124,19 @@ def ebDistribution : Probabilities → HashMap Nat Probability :=
     )
     ∅
 
+/--
+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 :=
@@ -106,6 +146,9 @@ def rbEfficiency (states : Probabilities) : Float :=
       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 :=
@@ -115,6 +158,9 @@ def ebEfficiency (states : Probabilities) : Float :=
       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

analysis/markov/Linleios/Probability.lean

@@ -2,18 +2,30 @@
 import Linleios.Util
 
 
+/--
+Number of stake pools.
+-/
 def nPools : Nat := 2500
 
+/--
+Compute a realistic stake distribution for the specified number of pools.
+-/
 def stakeDistribution (nPools : Nat) : List Float :=
   (List.range nPools).map (fun k => ((k + 1).toFloat / nPools.toFloat)^10 - (k.toFloat / nPools.toFloat)^10)
 
+/--
+Determine the distribution parameter that achieves the specified committee size.
+-/
 private def calibrateCommittee(committeeSize : Float) : Float :=
   let stakes : List Float := stakeDistribution nPools
   let f (m : Float) : Float :=
     let ps : List Float := stakes.map (fun s => 1 - Float.exp (- m * s))
     ps.sum - committeeSize
   bisectionSearch f committeeSize nPools.toFloat 0.5 10
 
+/--
+Compute the mean and standard deviation of the committee size, given the probability of a successful vote and a target committee size.
+-/
 private def committeeDistribution (pSuccessfulVote committeeSize : Float) : Float × Float :=
   let stakes : List Float := stakeDistribution nPools
   let m := calibrateCommittee committeeSize
@@ -22,6 +34,9 @@ private def committeeDistribution (pSuccessfulVote committeeSize : Float) : Floa
   let σ := (ps.map (fun p => 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 ⟨ μ , σ ⟩ := committeeDistribution pSuccessfulVote committeeSize
   1 - cdfGaussian (τ * committeeSize) μ σ

analysis/markov/Linleios/Types.lean

@@ -7,20 +7,44 @@ import Linleios.Probability
 open Std (HashMap)
 
 
+/--
+Represent probabilities as floating-point numbers.
+-/
 abbrev Probability := Float
 
-
+/--
+The constant parameters used for computing transitions.
+-/
 structure Environment where
+  /-- The active slot coefficient. -/
   activeSlotCoefficient : Probability
+  /-- The $L_\text{hdr}$ protocol parameter. -/
   Lheader : Nat
+  /-- The $L_\text{vote}$ protocol parameter. -/
   Lvote : Nat
+  /-- The $L_\text{diff}$ protocol parameter. -/
   Ldiff : Nat
+  /-- The probability that an RB occurs long enough after the previous RB so that an EB can be certified. -/
   pSpacingOkay : Probability
+  /-- The per-step quorum probability. -/
   pQuorum : Probability
+  /-- The probability that the EB and transaction data arrives too late to compute the ledger. -/
   pLate : Probability
+  /-- The fraction of adversarial stake. -/
   fAdversary : Float
 deriving Repr
 
+/--
+Create an environment.
+
+- `activeSlotCoefficient`: the active slot coefficient
+- `committeeSize`: the mean committee size
+- `τ`: the quorum fraction
+- `pRbHeaderArrives`: the probability that an RB header arrives before $L_\text{hdr}$ slots
+- `pEBValidates`: the probability that an EB is validated before $3 L_\text{hdr} + L_\text{vote} + L_\text{diff}$ slots
+- `pEbUnvalidated`: the probability that the EB and transaction data arrives too late to compute the ledger
+- `fAdversary`: the fraction of adversarial stake
+-/
 def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committeeSize τ pRbHeaderArrives pEbValidates pEbUnvalidated fAdversary : Float) : Environment :=
   {
     activeSlotCoefficient := activeSlotCoefficient
@@ -34,14 +58,25 @@ def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committee
   }
 
 
+/--
+The state of the chain's evolution.
+-/
 structure State where
+  /-- The number of potential RB oppurtunities. -/
   clock : Nat
+  /-- The number of RBs actually forged. -/
   rbCount : Nat
+  /-- The number of EBs certified. -/
   ebCount : Nat
+  /-- Whether an RB was forged in the current step. -/
   hasRb : Bool
+  /-- Whether an EB could be certified in the current step. -/
   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
@@ -50,11 +85,16 @@ theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0
   rfl
 
 
+/--
+The active states and their probabilities.
+-/
 def Probabilities := HashMap State Probability
 deriving Repr, EmptyCollection
 
 instance : Inhabited Probabilities where
   default := (∅ : Probabilities).insert Inhabited.default 1
 
 
+/--
+An outcome is a list of new states and their probabilities. -/
 abbrev Outcomes := List (State × Probability)

analysis/markov/Linleios/Util.lean

@@ -1,4 +1,7 @@
 
+/--
+The error function.
+-/
 partial def erf (x : Float) : Float :=
   if x < 0
     then - erf (- x)
@@ -12,9 +15,15 @@ partial def erf (x : Float) : Float :=
       let t := 1 / (1 + p * x)
       1 - (a₁ * t + a₂ * t^2 + a₃ * t^3 + a₄ * t^4 + a₅ * t^5) * Float.exp (- x^2)
 
+/--
+The CDF for a normal distribution.
+-/
 def cdfGaussian (x μ σ : Float) : Float :=
   (1 + erf ((x - μ) / σ / Float.sqrt 2)) / 2
 
+/--
+A bisection search.
+-/
 def bisectionSearch (f : Float → Float) (low high : Float) (ε : Float) (maxIter : Nat) : Float :=
   match maxIter with
   | 0 => (low + high) / 2

analysis/markov/docbuild/.gitignore

@@ -0,0 +1 @@
+.lake

analysis/markov/docbuild/ReadMe.md

@@ -0,0 +1,7 @@
+# Building the documentation
+
+See https://github.com/leanprover/doc-gen4/tree/v4.24.0 for detailed instructions.
+
+1.  In this folder, execute `MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4`.
+2.  Also in this folder, execute `lake build Linleios:docs`.
+3.  View the documentation at `./.lake/doc/index.html`.