Skip to content

Commit 7e91a84

Browse files
bwbushbwbush
committed
Refactored file organization
1 parent 4629cb4 commit 7e91a84

File tree

4 files changed

+92
-69
lines changed

4 files changed

+92
-69
lines changed

‎analysis/markov/src/Linleios.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import Linleios.Evolve
2+
import Linleios.Metrics
23

34
/-!
45
# Linleios: a Markovian model of Linear Leios

‎analysis/markov/src/Linleios/Evolve.lean‎

Lines changed: 0 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,9 @@
11

22
import Std.Data.HashMap
3-
import Batteries.Lean.HashMap
4-
import Lean.Data.Json.FromToJson
53

64
import Linleios.Types
75

86

9-
open Lean (Json)
10-
open Lean.ToJson (toJson)
117
open Std (HashMap)
128

139

@@ -104,68 +100,3 @@ def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat →
104100
| 0 => start
105101
| n + 1 => let state' := prune ε $ chain (@step env) start
106102
simulate env state' ε n
107-
108-
109-
/--
110-
Compute the total probabilities of a set of states.
111-
-/
112-
def totalProbability (states : Probabilities) : Probability :=
113-
states.fold (Function.const State ∘ Add.add) 0
114-
115-
/--
116-
Compute the distribution of EB counts.
117-
-/
118-
def ebDistribution : Probabilities → HashMap Nat Probability :=
119-
HashMap.fold
120-
(
121-
fun acc state p =>
122-
-- FIXME: Rewrite using `Function.const`.
123-
HashMap.mergeWith (fun _ => Add.add) acc
124-
$ singleton ⟨ state.ebCount , p ⟩
125-
)
126-
∅
127-
128-
/--
129-
Format the distribution of EB counts as JSON.
130-
-/
131-
def ebDistributionJson : Probabilities → Json :=
132-
Json.mkObj
133-
∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩)
134-
∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst))
135-
∘ HashMap.toList
136-
∘ ebDistribution
137-
138-
/--
139-
Compute the RB efficiency, given a set of states.
140-
-/
141-
def rbEfficiency (states : Probabilities) : Float :=
142-
let clock := states.keys.head!.clock
143-
let rbCount :=
144-
HashMap.fold
145-
(fun acc state p =>acc + state.rbCount.toFloat * p)
146-
0
147-
states
148-
rbCount / clock.toFloat
149-
150-
/--
151-
Compute the EB efficiency, given a set of states.
152-
-/
153-
def ebEfficiency (states : Probabilities) : Float :=
154-
let clock := states.keys.head!.clock
155-
let ebCount :=
156-
HashMap.fold
157-
(fun acc state p =>acc + state.ebCount.toFloat * p)
158-
0
159-
states
160-
ebCount / (clock.toFloat - 1)
161-
162-
/--
163-
Compute the overall efficiency, give a set of states.
164-
-/
165-
def efficiency (states : Probabilities) : Float :=
166-
let rb := rbEfficiency states
167-
let eb := ebEfficiency states
168-
let rbSize := 0.9
169-
let ebSize := 12.0
170-
let ρ := ebSize / rbSize
171-
(rb * (1 - eb) + ρ * eb) / (1 + ρ)

‎analysis/markov/src/Linleios/Metrics.lean‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
import Std.Data.HashMap
2+
import Batteries.Lean.HashMap
3+
import Lean.Data.Json.FromToJson
4+
5+
import Linleios.Types
6+
7+
import Linleios.Probability
8+
import Linleios.Evolve
9+
10+
open Lean (Json)
11+
open Lean.ToJson (toJson)
12+
open Std (HashMap)
13+
14+
15+
/--
16+
Compute the total probabilities of a set of states.
17+
-/
18+
def totalProbability (states : Probabilities) : Probability :=
19+
states.fold (Function.const State ∘ Add.add) 0
20+
21+
/--
22+
Compute the distribution of EB counts.
23+
-/
24+
def ebDistribution : Probabilities → HashMap Nat Probability :=
25+
HashMap.fold
26+
(
27+
fun acc state p =>
28+
-- FIXME: Rewrite using `Function.const`.
29+
HashMap.mergeWith (fun _ => Add.add) acc
30+
$ singleton ⟨ state.ebCount , p ⟩
31+
)
32+
∅
33+
34+
/--
35+
Format the distribution of EB counts as JSON.
36+
-/
37+
def ebDistributionJson : Probabilities → Json :=
38+
Json.mkObj
39+
∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩)
40+
∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst))
41+
∘ HashMap.toList
42+
∘ ebDistribution
43+
44+
/--
45+
Compute the RB efficiency, given a set of states.
46+
-/
47+
def rbEfficiency (states : Probabilities) : Float :=
48+
let clock := states.keys.head!.clock
49+
let rbCount :=
50+
HashMap.fold
51+
(fun acc state p =>acc + state.rbCount.toFloat * p)
52+
0
53+
states
54+
rbCount / clock.toFloat
55+
56+
/--
57+
Compute the EB efficiency, given a set of states.
58+
-/
59+
def ebEfficiency (states : Probabilities) : Float :=
60+
let clock := states.keys.head!.clock
61+
let ebCount :=
62+
HashMap.fold
63+
(fun acc state p =>acc + state.ebCount.toFloat * p)
64+
0
65+
states
66+
ebCount / (clock.toFloat - 1)
67+
68+
/--
69+
Compute the overall efficiency, give a set of states.
70+
-/
71+
def efficiency (states : Probabilities) : Float :=
72+
let rb := rbEfficiency states
73+
let eb := ebEfficiency states
74+
let rbSize := 0.9
75+
let ebSize := 12.0
76+
let ρ := ebSize / rbSize
77+
(rb * (1 - eb) + ρ * eb) / (1 + ρ)
78+
79+
80+
#eval ebEfficiency (simulate {(default : Environment) with pLate := 0.1} default 0 30)
81+
#eval (0.95^13 * 0.9)
82+
83+
#eval makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0.1
84+
#eval ebEfficiency (simulate (makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0.1) default 0 30)
85+
#eval (0.95^13 * 0.9)

‎analysis/markov/src/Linleios/Types.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,12 @@ def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committee
5757
fAdversary := fAdversary
5858
}
5959

60+
/--
61+
A perfect honest environment with the recommended protocol parameters.
62+
-/
63+
instance : Inhabited Environment where
64+
default := makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0
65+
6066

6167
/--
6268
The state of the chain's evolution.

0 commit comments

Comments
 (0)