Updated instructions and example in readme file

Author: bwbush

analysis/markov/Linleios/Evolve.lean

@@ -80,7 +80,11 @@ def ebDistribution : Probabilities → HashMap Nat Probability :=
     ∅
 
 def ebDistributionJson : Probabilities → Json :=
-  Json.mkObj ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩) ∘ HashMap.toList ∘ ebDistribution
+  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
 
 def rbEfficiency (states : Probabilities) : Float :=
   let clock := states.keys.head!.clock

analysis/markov/Main.lean

@@ -50,7 +50,7 @@ def markov : Cmd := `[Cli|
     "quorum-fraction"         : Float  ; "τ protocol parameter, in %/100."
     "p-rb-header-arrives"     : Float  ; "Probability that the RB header arrives before L_header."
     "p-eb-validates"          : Float  ; "Probability that the EB is fully validated before 3 L_header + L_vote."
-    "adversary-fraction"      : Float  ; "Fraction of stake that is adversarial."
+    "adversary-fraction"      : Float  ; "Fraction of stake that is adversarial: the adversary never produces RBs or EBs and never votes."
     "tolerance"               : Float  ; "Discard states with less than this probability."
     "rb-count"                : Nat    ; "Number of potential RBs to simulate."
     "output-file"             : String ; "Path to the JSON output file for the EB distribution."

analysis/markov/ReadMe.md

@@ -7,68 +7,86 @@ This Markovian model of Linear Leios computes the probability of EB certificatio
 
 The `linleios` program executes the Markov model for EB production in Linear Leios. The protocol parameters and network characteristic are specified as flags on the command line. The program outputs the following information:
 
-- The efficiency of EB production, defined as the expected number of certified EBs per RB, on `/dev/stdout`.
+- The efficiencies, on `/dev/stdout`.
+    - RB efficiency: the fraction of possible RBs that were actually produced.
+    - EB efficiency: the fraction of possible EBs that were actually produced.
+    - Efficiency: the fraction o possible payload bytes that were actual produced.
 - The "missing probability" resulting from the finite-resolution arithmetic of the computations, on `/dev/stderr`.
 - Optionally, a JSON file containing the probabilities of the given number of certified EBs.
 
+```bash
+lake exe linleios \
+  --l-header 1 \
+  --l-vote 4 \
+  --l-diff 5 \
+  --committee-size 600 \
+  --quorum-fraction 0.80 \
+  --p-rb-header-arrives 0.95 \
+  --p-eb-validates 0.85 \
+  --rb-count 100 \
+  --adversary-fraction 0.1 \
+  --output-file tmp.json
+```
+
 ```console
-$ lake exe linleios --l-header 1 --l-vote 4 --l-diff 5 --committee-size 600 --quorum-fraction 0.80 --p-rb-header-arrives 0.95 --p-eb-validates 0.85 --rb-count 100 --output-file tmp.json                                         
-
-Efficiency: 0.358416
-Missing probability: 0.000001
-
-$ json2yaml tmp.json
-
-'61': 0
-'60': 0
-'59': 1e-06
-'58': 2e-06
-'57': 5e-06
-'56': 1.2e-05
-'55': 2.8e-05
-'54': 6.2e-05
-'53': 0.00013
-'52': 0.000263
-'51': 0.00051
-'50': 0.00095
-'49': 0.0017
-'48': 0.002924
-'47': 0.004832
-'46': 0.00767
-'45': 0.011695
-'44': 0.017128
-'43': 0.024091
-'42': 0.032532
-'41': 0.042169
-'40': 0.052455
-'39': 0.062599
-'38': 0.071642
-'37': 0.0786
-'36': 0.082632
-'35': 0.083203
-'34': 0.080197
-'33': 0.073954
-'32': 0.065202
-'31': 0.054925
-'30': 0.044172
-'29': 0.033887
-'28': 0.024777
-'27': 0.017248
-'26': 0.011419
-'25': 0.007182
-'24': 0.004285
-'23': 0.002422
-'22': 0.001295
-'21': 0.000654
-'20': 0.000311
-'19': 0.000139
-'18': 5.8e-05
-'17': 2.3e-05
-'16': 8e-06
-'15': 3e-06
-'14': 1e-06
-'13': 0
-'12': 0
+RB efficiency: 0.899977
+EB efficiency: 0.290308
+Overall efficiency: 0.331256
+Missing probability: 0.000028
+```
+
+```bash
+jq 'to_entries | sort_by(.key | tonumber) | from_entries' tmp.json
+```
+
+```json
+{
+  "8": 0,
+  "9": 0.000001,
+  "10": 0.000003,
+  "11": 0.000012,
+  "12": 0.000036,
+  "13": 0.0001,
+  "14": 0.000251,
+  "15": 0.000582,
+  "16": 0.001251,
+  "17": 0.0025,
+  "18": 0.004659,
+  "19": 0.008126,
+  "20": 0.013297,
+  "21": 0.020463,
+  "22": 0.02968,
+  "23": 0.040648,
+  "24": 0.052656,
+  "25": 0.064622,
+  "26": 0.07524,
+  "27": 0.083218,
+  "28": 0.087538,
+  "29": 0.087673,
+  "30": 0.083686,
+  "31": 0.076199,
+  "32": 0.066239,
+  "33": 0.055015,
+  "34": 0.043687,
+  "35": 0.03319,
+  "36": 0.024137,
+  "37": 0.016812,
+  "38": 0.011221,
+  "39": 0.00718,
+  "40": 0.004405,
+  "41": 0.002593,
+  "42": 0.001464,
+  "43": 0.000794,
+  "44": 0.000413,
+  "45": 0.000206,
+  "46": 0.000098,
+  "47": 0.000045,
+  "48": 0.000019,
+  "49": 0.000008,
+  "50": 0.000003,
+  "51": 0.000001,
+  "52": 0
+}
 ```
 
 
@@ -83,7 +101,6 @@ Run a Markov simulation of Linear Leios.
 USAGE:
     markov [FLAGS]
 
-FLAGS:
     -h, --help                         Prints this message.
     --version                          Prints the version.
     --active-slot-coefficient : Float  The active slot coefficient for RBs, in
@@ -104,10 +121,13 @@ FLAGS:
     --p-eb-validates : Float           Probability that the EB is fully
                                        validated before 3 L_header + L_vote.
                                        [Default: `0.90`]
+    --adversary-fraction : Float       Fraction of stake that is adversarial:
+                                       the adversary never produces RBs or EBs
+                                       and never votes. [Default: `0`]
     --tolerance : Float                Discard states with less than this
                                        probability. [Default: `1e-8`]
-    --rb-count : Nat                   Number of RBs to simulate. [Default:
-                                       `100`]
+    --rb-count : Nat                   Number of potential RBs to simulate.
+                                       [Default: `100`]
     --output-file : String             Path to the JSON output file for the EB
                                        distribution.
 ```