Skip to content

Commit fb63910

Browse files
bwbushbwbush
committed
Added CLI
1 parent 4895480 commit fb63910

File tree

4 files changed

+108
-25
lines changed

4 files changed

+108
-25
lines changed

‎analysis/markov/Linleios.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1 @@
1-
21
import Linleios.Evolve

‎analysis/markov/Main.lean‎

Lines changed: 57 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,33 @@
11

2+
import Cli
23
import Linleios
4+
import Parser.Char.Numeric
5+
import Parser.Stream
36

7+
open Cli
48

5-
def env : Environment := makeEnvironment 0.05 0.95 0.90 600 0.75 1 4 7
69

7-
def sn := simulate env default 1e-6 25
10+
instance : ParseableType Float where
11+
name := "Float"
12+
parse? x := match (Parser.Char.ASCII.parseFloat : SimpleParser Substring Char Float).run x with
13+
| .ok _ y => some y
14+
| _ => none
815

9-
def main : IO Unit :=
16+
17+
def runMarkovCmd (p : Parsed) : IO UInt32 :=
1018
do
19+
let activeSlotCoefficient : Float := p.flag! "active-slot-coefficient" |>.as! Float
20+
let Lheader : Nat := p.flag! "l-header" |>.as! Nat
21+
let Lvote : Nat := p.flag! "l-vote" |>.as! Nat
22+
let Ldiff : Nat := p.flag! "l-diff" |>.as! Nat
23+
let committeeSize : Nat := p.flag! "committee-size" |>.as! Nat
24+
let τ : Float := p.flag! "quorum-fraction" |>.as! Float
25+
let pRbHeaderArrives : Float := p.flag! "p-rb-header-arrives" |>.as! Float
26+
let pEbValidates : Float := p.flag! "p-eb-validates" |>.as! Float
27+
let ε : Float := p.flag! "tolerance" |>.as! Float
28+
let rbCount : Nat := p.flag! "rb-count" |>.as! Nat
29+
let env := makeEnvironment activeSlotCoefficient pRbHeaderArrives pEbValidates committeeSize.toFloat τ Lheader Lvote Ldiff
30+
let sn := simulate env default ε rbCount
1131
let print {α : Type} [Repr α] (x : α) : IO Unit := IO.println (reprPrec x 0).pretty
1232
IO.println ""
1333
print sn
@@ -17,3 +37,37 @@ def main : IO Unit :=
1737
print $ ebEfficiency sn
1838
IO.println ""
1939
print $ 1 - totalProbability sn
40+
pure 0
41+
42+
def markovCmd : Cmd := `[Cli|
43+
markovCmd VIA runMarkovCmd; ["0.0.1"]
44+
"Run a Markov simulation of Linear Leios."
45+
FLAGS:
46+
"active-slot-coefficient" : Float ; "The active slot coefficient for RBs, in probability per slot."
47+
"l-header" : Nat ; "L_header protocol parameter, in slots."
48+
"l-vote" : Nat ; "L_vote protocol parameter, in slots."
49+
"l-diff" : Nat ; "L_diff protocol parameter, in slots."
50+
"committee-size" : Nat ; "Expected number of voters in the committee."
51+
"quorum-fraction" : Float ; "τ protocol parameter, in %/100."
52+
"p-rb-header-arrives" : Float ; "Probability that the RB header arrives before L_header."
53+
"p-eb-validates" : Float ; "Probability that the EB is fully validated before 3 L_header + L_vote."
54+
"tolerance" : Float ; "Discard states with less than this probability."
55+
"rb-count" : Nat ; "Number of RBs to simulate."
56+
EXTENSIONS:
57+
author "bwbush";
58+
defaultValues! #[
59+
("active-slot-coefficient", "0.05")
60+
, ("l-header" , "1" )
61+
, ("l-vote" , "4" )
62+
, ("l-diff" , "7" )
63+
, ("committee-size" , "600" )
64+
, ("quorum-fraction" , "0.75")
65+
, ("p-rb-header-arrives" , "0.95")
66+
, ("p-eb-validates" , "0.90")
67+
, ("tolerance" , "1e-9")
68+
, ("rb-count" , "100" )
69+
]
70+
]
71+
72+
def main (args : List String) : IO UInt32 :=
73+
markovCmd.validate args

‎analysis/markov/lake-manifest.json‎

Lines changed: 41 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,27 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url": "https://github.com/leanprover-community/mathlib4",
4+
[{"url": "https://github.com/mhuisi/lean4-cli",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "",
8+
"rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
9+
"name": "Cli",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "v4.20.0",
12+
"inherited": false,
13+
"configFile": "lakefile.toml"},
14+
{"url": "https://github.com/fgdorais/lean4-parser",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "",
18+
"rev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
19+
"name": "Parser",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
22+
"inherited": false,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/mathlib4",
525
"type": "git",
626
"subDir": null,
727
"scope": "leanprover-community",
@@ -11,6 +31,26 @@
1131
"inputRev": "v4.20.0",
1232
"inherited": false,
1333
"configFile": "lakefile.lean"},
34+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "",
38+
"rev": "45c426d1cb016fcb4fcbe043f1cd2d97acb2dbc3",
39+
"name": "UnicodeBasic",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.lean"},
44+
{"url": "https://github.com/leanprover-community/batteries",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "",
48+
"rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
49+
"name": "batteries",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "main",
52+
"inherited": true,
53+
"configFile": "lakefile.toml"},
1454
{"url": "https://github.com/leanprover-community/plausible",
1555
"type": "git",
1656
"subDir": null,
@@ -70,26 +110,6 @@
70110
"manifestFile": "lake-manifest.json",
71111
"inputRev": "master",
72112
"inherited": true,
73-
"configFile": "lakefile.toml"},
74-
{"url": "https://github.com/leanprover-community/batteries",
75-
"type": "git",
76-
"subDir": null,
77-
"scope": "leanprover-community",
78-
"rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
79-
"name": "batteries",
80-
"manifestFile": "lake-manifest.json",
81-
"inputRev": "main",
82-
"inherited": true,
83-
"configFile": "lakefile.toml"},
84-
{"url": "https://github.com/leanprover/lean4-cli",
85-
"type": "git",
86-
"subDir": null,
87-
"scope": "leanprover",
88-
"rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
89-
"name": "Cli",
90-
"manifestFile": "lake-manifest.json",
91-
"inputRev": "main",
92-
"inherited": true,
93113
"configFile": "lakefile.toml"}],
94114
"name": "linleios",
95115
"lakeDir": ".lake"}

‎analysis/markov/lakefile.toml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,16 @@ name = "mathlib"
1919
scope = "leanprover-community"
2020
version = "git#v4.20.0"
2121

22+
[[require]]
23+
name = "Parser"
24+
git = "https://github.com/fgdorais/lean4-parser"
25+
rev = "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
26+
27+
[[require]]
28+
name = "Cli"
29+
git = "https://github.com/mhuisi/lean4-cli"
30+
rev = "v4.20.0"
31+
2232
[lean]
2333
server-options = [
2434
["checkBinderAnnotations", "false"],

0 commit comments

Comments
 (0)