JAR: Join-Accumulate Refine

4.11. Tickets🔗

🔗def
Jar.K_MAX_TICKETS [j : Jar.JarConfig] : Nat
Jar.K_MAX_TICKETS [j : Jar.JarConfig] :
  Nat

K_MAX_TICKETS via JarConfig.

🔗def
Jar.dynamicTicketsPerValidator [j : Jar.JarConfig]
  (pendingValidatorCount : Nat) : Nat
Jar.dynamicTicketsPerValidator
  [j : Jar.JarConfig]
  (pendingValidatorCount : Nat) : Nat

Dynamic N_TICKETS: ceil(2*E / len(pendingset')) for variable validators. More tickets per validator when fewer validators, to fill the accumulator. GP#514 §safrole.

🔗def
Jar.activeCoreCount.{u_1} [j : Jar.JarConfig] {α : Type u_1}
  (validators : Array α) : Nat
Jar.activeCoreCount.{u_1}
  [j : Jar.JarConfig] {α : Type u_1}
  (validators : Array α) : Nat

Active core count: C for fixed validators, len(validators)/3 for variable. GP#514: only the first len(κ)/3 cores are active.