Implemented adversarial stake

Author: bwbush

analysis/markov/Linleios/Evolve.lean

@@ -11,28 +11,36 @@ open Lean.ToJson (toJson)
 open Std (HashMap)
 
 
-def certify {env : Environment} (state : State) : Outcomes :=
+def forge {env : Environment} (state : State) : Outcomes :=
   let state' :=
     {
       state with
-      rbCount := state.rbCount + 1
-      canCertify := true
+      clock := state.clock + 1
     }
+  let p := 1 - env.fAdversary
+  [
+    ({state' with rbCount := state.rbCount + 1}, p)
+  , (state', 1 - p)
+  ]
+
+def certify {env : Environment} (state : State) : Outcomes :=
+  let p := env.pSpacingOkay * (1 - env.fAdversary)
   if state.canCertify
     then [
-           ⟨{state' with ebCount := state.ebCount + 1}, env.pSpacingOkay⟩
-         , ⟨state', 1 - env.pSpacingOkay⟩
+           ⟨{state with ebCount := state.ebCount + 1}, p⟩
+         , ⟨state, 1 - p⟩
          ]
-    else [(state', 1)]
+    else [(state, 1)]
 
 def vote {env : Environment} (state : State) : Outcomes :=
+  let p := env.pQuorum * (1 - env.fAdversary)
   [
-    (state, env.pQuorum)
-  , ({state with canCertify := false}, 1 - env.pQuorum)
+    ({state with canCertify := true}, p)
+  , ({state with canCertify := false}, 1 - p)
   ]
 
 def step {env : Environment} : List (State → Outcomes) :=
-  [@certify env, @vote env]
+  [@forge env, @certify env, @vote env]
 
 
 def prune (ε : Float) : Probabilities → Probabilities :=
@@ -75,10 +83,10 @@ def ebDistributionJson : Probabilities → Json :=
   Json.mkObj ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩) ∘ HashMap.toList ∘ ebDistribution
 
 def ebEfficiency (states : Probabilities) : Float :=
-  let rbCount := states.keys.head!.rbCount
+  let clock := states.keys.head!.clock
   let ebCount :=
     HashMap.fold
       (fun acc state p =>acc + state.ebCount.toFloat * p)
       0
       states
-  ebCount / (rbCount.toFloat - 1)
+  ebCount / (clock.toFloat - 1)

analysis/markov/Linleios/Types.lean

@@ -17,25 +17,31 @@ structure Environment where
   Ldiff : Nat
   pSpacingOkay : Probability
   pQuorum : Probability
+  fAdversary : Float
+deriving Repr
 
-def makeEnvironment (activeSlotCoefficient pRbHeaderArrives pEbValidates committeeSize τ : Float) (Lheader Lvote Ldiff : Nat) : Environment :=
+def makeEnvironment (activeSlotCoefficient pRbHeaderArrives pEbValidates committeeSize τ fAdversary : Float) (Lheader Lvote Ldiff : Nat) : Environment :=
   {
     activeSlotCoefficient := activeSlotCoefficient
     Lheader := Lheader
     Lvote := Lvote
     Ldiff := Ldiff
     pSpacingOkay := (1 - activeSlotCoefficient).pow (3 * Lheader + Lvote + Ldiff - 1).toFloat
     pQuorum := pQuorum (pRbHeaderArrives * pEbValidates) committeeSize τ
+    fAdversary := fAdversary
   }
 
 
 structure State where
+  clock : Nat
   rbCount : Nat
   ebCount : Nat
   canCertify : Bool
 deriving Repr, BEq, Hashable, Inhabited
 
-theorem genesis : (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
+theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
+  constructor
+  rfl
   constructor
   rfl
   rfl

analysis/markov/Main.lean

@@ -25,9 +25,10 @@ def runMarkovCmd (p : Parsed) : IO UInt32 :=
     let τ : Float := p.flag! "quorum-fraction" |>.as! Float
     let pRbHeaderArrives : Float := p.flag! "p-rb-header-arrives" |>.as! Float
     let pEbValidates : Float := p.flag! "p-eb-validates" |>.as! Float
+    let fAdversary : Float := p.flag! "adversary-fraction" |>.as! Float
     let ε : Float := p.flag! "tolerance" |>.as! Float
     let rbCount : Nat := p.flag! "rb-count" |>.as! Nat
-    let env := makeEnvironment activeSlotCoefficient pRbHeaderArrives pEbValidates committeeSize.toFloat τ Lheader Lvote Ldiff
+    let env := makeEnvironment activeSlotCoefficient pRbHeaderArrives pEbValidates committeeSize.toFloat τ fAdversary Lheader Lvote Ldiff
     let sn := simulate env default ε rbCount
     if p.hasFlag "output-file"
       then IO.FS.writeFile (p.flag! "output-file" |>.as! String) (Json.pretty $ ebDistributionJson sn)
@@ -47,8 +48,9 @@ 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."
     "tolerance"               : Float  ; "Discard states with less than this probability."
-    "rb-count"                : Nat    ; "Number of RBs to simulate."
+    "rb-count"                : Nat    ; "Number of potential RBs to simulate."
     "output-file"             : String ; "Path to the JSON output file for the EB distribution."
   EXTENSIONS:
     defaultValues! #[
@@ -60,6 +62,7 @@ def markov : Cmd := `[Cli|
     , ("quorum-fraction"        , "0.75")
     , ("p-rb-header-arrives"    , "0.95")
     , ("p-eb-validates"         , "0.90")
+    , ("adversary-fraction"     , "0"   )
     , ("tolerance"              , "1e-8")
     , ("rb-count"               , "100" )
     ]