Skip to content

Commit 238a79d

Browse files
committed
Documented model
1 parent d8ed09b commit 238a79d

File tree

5 files changed

+155
-80
lines changed

5 files changed

+155
-80
lines changed

analysis/markov/Linleios/Evolve.lean

Lines changed: 23 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -11,36 +11,47 @@ open Lean.ToJson (toJson)
1111
open Std (HashMap)
1212

1313

14-
def forge {env : Environment} (state : State) : Outcomes :=
14+
def forgeRb {env : Environment} (state : State) : Outcomes :=
1515
let state' :=
1616
{
1717
state with
1818
clock := state.clock + 1
1919
}
2020
let p := 1 - env.fAdversary
2121
[
22-
({state' with rbCount := state.rbCount + 1}, p)
23-
, (state', 1 - p)
22+
({state' with hasRb := true, rbCount := state.rbCount + 1}, p)
23+
, ({state' with hasRb := false, canCertify := false}, 1 - p)
2424
]
2525

2626
def certify {env : Environment} (state : State) : Outcomes :=
27-
let p := env.pSpacingOkay * (1 - env.fAdversary)
28-
if state.canCertify
29-
then [
27+
if state.hasRb && state.canCertify
28+
then let p := env.pSpacingOkay
29+
[
3030
⟨{state with ebCount := state.ebCount + 1}, p⟩
3131
, ⟨state, 1 - p⟩
3232
]
3333
else [(state, 1)]
3434

35+
def forgeEb {env : Environment} (state : State) : Outcomes :=
36+
if state.hasRb
37+
then let p := 1 - env.pLate
38+
[
39+
({state with canCertify := true}, p)
40+
, ({state with canCertify := false}, 1 - p)
41+
]
42+
else [(state, 1)]
43+
3544
def vote {env : Environment} (state : State) : Outcomes :=
36-
let p := env.pQuorum * (1 - env.fAdversary)
37-
[
38-
({state with canCertify := true}, p)
39-
, ({state with canCertify := false}, 1 - p)
40-
]
45+
if state.hasRb
46+
then let p := env.pQuorum
47+
[
48+
(state, p)
49+
, ({state with canCertify := false}, 1 - p)
50+
]
51+
else [(state, 1)]
4152

4253
def step {env : Environment} : List (State → Outcomes) :=
43-
[@forge env, @certify env, @vote env]
54+
[@forgeRb env, @certify env, @forgeEb env, @vote env]
4455

4556

4657
def prune (ε : Float) : Probabilities → Probabilities :=

analysis/markov/Linleios/Types.lean

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,17 +17,19 @@ structure Environment where
1717
Ldiff : Nat
1818
pSpacingOkay : Probability
1919
pQuorum : Probability
20+
pLate : Probability
2021
fAdversary : Float
2122
deriving Repr
2223

23-
def makeEnvironment (activeSlotCoefficient pRbHeaderArrives pEbValidates committeeSize τ fAdversary : Float) (Lheader Lvote Ldiff : Nat) : Environment :=
24+
def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committeeSize τ pRbHeaderArrives pEbValidates pEbUnvalidated fAdversary : Float) : Environment :=
2425
{
2526
activeSlotCoefficient := activeSlotCoefficient
2627
Lheader := Lheader
2728
Lvote := Lvote
2829
Ldiff := Ldiff
2930
pSpacingOkay := (1 - activeSlotCoefficient).pow (3 * Lheader + Lvote + Ldiff - 1).toFloat
30-
pQuorum := pQuorum (pRbHeaderArrives * pEbValidates) committeeSize τ
31+
pQuorum := pQuorum (pRbHeaderArrives * pEbValidates * (1 - fAdversary)) committeeSize τ
32+
pLate := pEbUnvalidated * (1 - committeeSize / nPools.toFloat)
3133
fAdversary := fAdversary
3234
}
3335

@@ -36,6 +38,7 @@ structure State where
3638
clock : Nat
3739
rbCount : Nat
3840
ebCount : Nat
41+
hasRb : Bool
3942
canCertify : Bool
4043
deriving Repr, BEq, Hashable, Inhabited
4144

analysis/markov/Main.lean

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,10 +25,11 @@ def runMarkovCmd (p : Parsed) : IO UInt32 :=
2525
let τ : Float := p.flag! "quorum-fraction" |>.as! Float
2626
let pRbHeaderArrives : Float := p.flag! "p-rb-header-arrives" |>.as! Float
2727
let pEbValidates : Float := p.flag! "p-eb-validates" |>.as! Float
28+
let pLateDiffusion : Float := p.flag! "p-late-diffusion" |>.as! Float
2829
let fAdversary : Float := p.flag! "adversary-fraction" |>.as! Float
2930
let ε : Float := p.flag! "tolerance" |>.as! Float
3031
let rbCount : Nat := p.flag! "rb-count" |>.as! Nat
31-
let env := makeEnvironment activeSlotCoefficient pRbHeaderArrives pEbValidates committeeSize.toFloat τ fAdversary Lheader Lvote Ldiff
32+
let env := makeEnvironment Lheader Lvote Ldiff activeSlotCoefficient committeeSize.toFloat τ pRbHeaderArrives pEbValidates pLateDiffusion fAdversary
3233
let sn := simulate env default ε rbCount
3334
if p.hasFlag "output-file"
3435
then IO.FS.writeFile (p.flag! "output-file" |>.as! String) (Json.pretty $ ebDistributionJson sn)
@@ -50,6 +51,7 @@ def markov : Cmd := `[Cli|
5051
"quorum-fraction" : Float ; "τ protocol parameter, in %/100."
5152
"p-rb-header-arrives" : Float ; "Probability that the RB header arrives before L_header."
5253
"p-eb-validates" : Float ; "Probability that the EB is fully validated before 3 L_header + L_vote."
54+
"p-late-diffusion" : Float ; "Probability than a RB producer hasn't validated the previous EB."
5355
"adversary-fraction" : Float ; "Fraction of stake that is adversarial: the adversary never produces RBs or EBs and never votes."
5456
"tolerance" : Float ; "Discard states with less than this probability."
5557
"rb-count" : Nat ; "Number of potential RBs to simulate."
@@ -64,6 +66,7 @@ def markov : Cmd := `[Cli|
6466
, ("quorum-fraction" , "0.75")
6567
, ("p-rb-header-arrives" , "0.95")
6668
, ("p-eb-validates" , "0.90")
69+
, ("p-late-diffusion" , "0.05")
6770
, ("adversary-fraction" , "0" )
6871
, ("tolerance" , "1e-8")
6972
, ("rb-count" , "100" )

analysis/markov/ReadMe.md

Lines changed: 123 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,85 @@
1-
# Markov-model simulation for Linear Leios
1+
# Markovian simulation of Linear Leios
2+
3+
This Markovian simulation of Linear Leios computes the probability of EB certifications as RBs are produced.
24

3-
This Markovian model of Linear Leios computes the probability of EB certifications as RBs are produced.
45

56
## Contents
67

7-
- [Approach](#approach)
8+
- [Model](#model)
89
- [Parameters](#parameters)
910
- [Example](#example)
1011
- [Usage](#usage)
1112
- [Building](#building)
1213

1314

14-
## Approach
15+
## Model
16+
17+
The protocol state is represented by three quantities.
18+
19+
- The number of RBs that have been produced.
20+
- The number of EBs that have been produced.
21+
- Whether an honest RB was produced.
22+
- Whether a certificate is ready for inclusion in the next RB.
23+
24+
Time is tracked in terms of block-forging opportunties instead of in terms of slots.
25+
26+
Transitions occur in several substeps:
27+
28+
1. *Forge RB:* create a new RB.
29+
2. *Certify:* include a certificate in the RB.
30+
3. *Forge EB:* create a new EB.
31+
4. *Vote:* cast votes to reach a quorum.
32+
33+
34+
### Substep 1: Forge RB
35+
36+
The adversarial model assumes that adversaries obstain from producing RBs, EBs, and votes. Let $f_\text{adv}$ be the fraction of stake held by the adversary. Two transitions are possible:
37+
38+
- *Forge a new RB:* probability $1 - f_\text{adv}$.
39+
- *Abstain from forging a new RB:* probability $f_\text{adv}$.
40+
41+
42+
### Substep 2: Certify
43+
44+
Provided that a quorum of votes have endorsed the EB, the following conditions are required for certifying it in the RB that was just forged.
45+
46+
- *RB spacing:* The previous RB must have been forged at least $3 L_\text{hdr} + L_\text{vote} + L_\text{diff}$ slots previously.
47+
- The distribution of gaps between RBs follows the negative-binomial distribution.
48+
- *Quorum:* The voting yielded a quorum.
49+
- *Not an adversary:* There is no RB if an adversary is the designated block producer.
50+
51+
52+
### Substep 3: Forge EB
53+
54+
Provided that an honest RB exists, an EB can be forged if the node has received the previous EB and computed the ledger state.
55+
56+
- 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.
57+
- 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.
58+
59+
60+
### Substep 4: Vote
61+
62+
Obtaining a successful quorum of votes is distributed according to bernoulli trials where the expected number of successes is the mean committee size and the success probabilities of individual pools accord with the stake distribution. Those success probabilities are modified in several ways:
1563

16-
(to be written)
64+
- *Adversaries do not vote:* probability $f_\text{adv}$.
65+
- *RB header arrives within $L_\text{hdr}$ slots:* probability $p_\text{rb}$.
66+
- *EB is fully validated within $3 L_\text{hdr} + L_\text{vote}$ slots*: probability $p_\text{eb}$.
1767

1868

1969
## Parameters
2070

21-
| Symbol | Flag | Default | Description |
22-
|-----------------|-------------------------|--------:|-------------------------------------------------------------------------------------|
23-
| $L_\text{hdr}$ | `--l-header` | 1 | Constraint on header diffusion time. |
24-
| $L_\text{vote}$ | `--l-vote` | 4 | Constraint on voting time. |
25-
| $L_\text{diff}$ | `--l-diff` | 7 | Constraint on diffusion time. |
26-
| $m$ | `--committee-size` | 600 | Number of members on the voting committee. |
27-
| $\tau$ | `--quorum-fraction` | 0.75 | Stake-weighted fraction of committee's votes required to produce a certificate. |
28-
| $p_\text{rb}$ | `--p-rb-header-arrives` | 0.95 | Probability that the RB header arrives at the node before $L_\text{hdr}$ seconds. |
29-
| $p_\text{eb}$ | `--p-eb-validates` | 0.90 | Probability that the EB is fully validated before $3 L_\text{hdr} + L_\text{vote}$. |
30-
| $f_\text{adv}$ | `--adversary-fraction` | 0.00 | Fraction of stake held by adversaries. |
71+
| Symbol | Flag | Default | Description |
72+
|------------------|-------------------------|--------:|------------------------------------------------------------------------------------------------------|
73+
| $L_\text{hdr}$ | `--l-header` | 1 | Constraint on header diffusion time. |
74+
| $L_\text{vote}$ | `--l-vote` | 4 | Constraint on voting time. |
75+
| $L_\text{diff}$ | `--l-diff` | 7 | Constraint on diffusion time. |
76+
| $n_\text{comm}$ | | 2500 | Number of stakepools (constant). |
77+
| $n_\text{pools}$ | `--committee-size` | 600 | Number of members on the voting committee. |
78+
| $\tau$ | `--quorum-fraction` | 0.75 | Stake-weighted fraction of committee's votes required to produce a certificate. |
79+
| $p_\text{rb}$ | `--p-rb-header-arrives` | 0.95 | Probability that the RB header arrives at a node before $L_\text{hdr}$ seconds. |
80+
| $p_\text{eb}$ | `--p-eb-validates` | 0.90 | Probability that the EB is fully validated by a node before $3 L_\text{hdr} + L_\text{vote}$. |
81+
| $p_\text{late}$ | `--p-late-diffusion` | 0.05 | Probability that an RB producer hasn't yet validated the EB by the time they need to forge their RB. |
82+
| $f_\text{adv}$ | `--adversary-fraction` | 0.00 | Fraction of stake held by adversaries. |
3183

3284

3385
## Example
@@ -49,17 +101,18 @@ lake exe linleios \
49101
--committee-size 600 \
50102
--quorum-fraction 0.80 \
51103
--p-rb-header-arrives 0.95 \
52-
--p-eb-validates 0.85 \
104+
--p-eb-validates 0.95 \
105+
--p-late-diffusion 0.05 \
53106
--rb-count 100 \
54107
--adversary-fraction 0.1 \
55108
--output-file tmp.json
56109
```
57110

58111
```console
59-
RB efficiency: 0.899977
60-
EB efficiency: 0.290308
61-
Overall efficiency: 0.331256
62-
Missing probability: 0.000028
112+
RB efficiency: 0.899974
113+
EB efficiency: 0.313049
114+
Overall efficiency: 0.352469
115+
Missing probability: 0.000030
63116
```
64117

65118
```bash
@@ -68,51 +121,53 @@ jq 'to_entries | sort_by(.key | tonumber) | from_entries' tmp.json
68121

69122
```console
70123
{
71-
"8": 0,
72-
"9": 0.000001,
73-
"10": 0.000003,
74-
"11": 0.000012,
75-
"12": 0.000036,
76-
"13": 0.0001,
77-
"14": 0.000251,
78-
"15": 0.000582,
79-
"16": 0.001251,
80-
"17": 0.0025,
81-
"18": 0.004659,
82-
"19": 0.008126,
83-
"20": 0.013297,
84-
"21": 0.020463,
85-
"22": 0.02968,
86-
"23": 0.040648,
87-
"24": 0.052656,
88-
"25": 0.064622,
89-
"26": 0.07524,
90-
"27": 0.083218,
91-
"28": 0.087538,
92-
"29": 0.087673,
93-
"30": 0.083686,
94-
"31": 0.076199,
95-
"32": 0.066239,
96-
"33": 0.055015,
97-
"34": 0.043687,
98-
"35": 0.03319,
99-
"36": 0.024137,
100-
"37": 0.016812,
101-
"38": 0.011221,
102-
"39": 0.00718,
103-
"40": 0.004405,
104-
"41": 0.002593,
105-
"42": 0.001464,
106-
"43": 0.000794,
107-
"44": 0.000413,
108-
"45": 0.000206,
109-
"46": 0.000098,
110-
"47": 0.000045,
111-
"48": 0.000019,
112-
"49": 0.000008,
113-
"50": 0.000003,
114-
"51": 0.000001,
115-
"52": 0
124+
"10": 0,
125+
"11": 0.000003,
126+
"12": 0.00001,
127+
"13": 0.000031,
128+
"14": 0.000081,
129+
"15": 0.000196,
130+
"16": 0.00044,
131+
"17": 0.000919,
132+
"18": 0.001799,
133+
"19": 0.003308,
134+
"20": 0.005731,
135+
"21": 0.009381,
136+
"22": 0.014533,
137+
"23": 0.021353,
138+
"24": 0.029805,
139+
"25": 0.039585,
140+
"26": 0.050095,
141+
"27": 0.060484,
142+
"28": 0.069757,
143+
"29": 0.07693,
144+
"30": 0.081208,
145+
"31": 0.082129,
146+
"32": 0.079641,
147+
"33": 0.074106,
148+
"34": 0.066214,
149+
"35": 0.056847,
150+
"36": 0.04692,
151+
"37": 0.037253,
152+
"38": 0.028464,
153+
"39": 0.020939,
154+
"40": 0.014837,
155+
"41": 0.010129,
156+
"42": 0.006664,
157+
"43": 0.004227,
158+
"44": 0.002586,
159+
"45": 0.001525,
160+
"46": 0.000868,
161+
"47": 0.000476,
162+
"48": 0.000252,
163+
"49": 0.000128,
164+
"50": 0.000063,
165+
"51": 0.00003,
166+
"52": 0.000013,
167+
"53": 0.000005,
168+
"54": 0.000002,
169+
"55": 0.000001,
170+
"56": 0
116171
}
117172
```
118173

@@ -150,6 +205,9 @@ USAGE:
150205
--p-eb-validates : Float Probability that the EB is fully
151206
validated before 3 L_header + L_vote.
152207
[Default: `0.90`]
208+
--p-late-diffusion : Float Probability than a RB producer hasn't
209+
validated the previous EB. [Default:
210+
`0.05`]
153211
--adversary-fraction : Float Fraction of stake that is adversarial:
154212
the adversary never produces RBs or EBs
155213
and never votes. [Default: `0`]
2.45 KB
Loading

0 commit comments

Comments
 (0)