update weak subjectivity calculations (#4923)

Weak subjectivity logic (`--weak-subjectivity-checkpoint`) was outdated.
Updated to latest specs, also taking into account total active balance.

See https://github.com/ethereum/consensus-specs/pull/2190

beacon_chain/spec/datatypes/base.nim

@@ -125,6 +125,26 @@ template maxSize*(n: int) {.pragma.}
 # - ambiguous calls, in particular for chronicles, with static enums
 # - broke the compiler in SSZ and nim-serialization
 
+type
+  Wei* = UInt256
+  Gwei* = uint64
+  Ether* = distinct uint64
+
+template ethAmountUnit*(typ: type) {.dirty.} =
+  # Arithmetic
+  func `+`*(x, y: typ): typ {.borrow.}
+  func `-`*(x, y: typ): typ {.borrow.}
+  func `*`*(x: typ, y: distinctBase(typ)): typ {.borrow.}
+  func `*`*(x: distinctBase(typ), y: typ): typ {.borrow.}
+
+  # Arithmetic, changing type
+  func `div`*(x, y: typ): distinctBase(typ) {.borrow.}
+
+  # Comparison
+  func `<`*(x, y: typ): bool {.borrow.}
+
+ethAmountUnit Ether
+
 type
   # https://github.com/ethereum/consensus-specs/blob/v1.3.0-rc.5/specs/phase0/beacon-chain.md#custom-types
   Eth2Domain* = array[32, byte]
@@ -167,9 +187,6 @@ type
     ## The `SubnetId` type is constrained to values in the range
     ## `[0, ATTESTATION_SUBNET_COUNT)` during initialization.
 
-  Wei* = UInt256
-  Gwei* = uint64
-
   # BitVector[4] in the spec, ie 4 bits which end up encoded as a byte for
   # SSZ / hashing purposes
   JustificationBits* = distinct uint8

beacon_chain/spec/helpers.nim

@@ -26,6 +26,11 @@ import
 export
   eth2_merkleization, forks, rlp, ssz_codec
 
+func toEther*(gwei: Gwei): Ether =
+  # https://github.com/ethereum/consensus-specs/blob/v1.3.0/specs/phase0/weak-subjectivity.md#constants
+  const ETH_TO_GWEI = 1_000_000_000
+  (gwei div ETH_TO_GWEI).Ether
+
 type
   ExecutionWithdrawal = eth_types.Withdrawal
   ExecutionBlockHeader = eth_types.BlockHeader

beacon_chain/spec/weak_subjectivity.nim

@@ -8,35 +8,59 @@
 {.push raises: [].}
 
 import
-  ./datatypes/base, ./forks, ./helpers
+  ./datatypes/base, ./beaconstate, ./forks, ./helpers
 
-const
-  SAFETY_DECAY* = 10'u64
+# https://github.com/ethereum/consensus-specs/blob/v1.3.0/specs/phase0/weak-subjectivity.md#configuration
+const SAFETY_DECAY* = 10'u64
 
-# https://github.com/ethereum/consensus-specs/blob/v1.0.1/specs/phase0/weak-subjectivity.md#calculating-the-weak-subjectivity-period
+# https://github.com/ethereum/consensus-specs/blob/v1.3.0/specs/phase0/weak-subjectivity.md#compute_weak_subjectivity_period
 func compute_weak_subjectivity_period(
-    cfg: RuntimeConfig, state: ForkedHashedBeaconState): uint64 =
-  var weak_subjectivity_period = cfg.MIN_VALIDATOR_WITHDRAWABILITY_DELAY
-  let validator_count =
-    get_active_validator_indices_len(state, get_current_epoch(state))
-  if validator_count >= cfg.MIN_PER_EPOCH_CHURN_LIMIT * cfg.CHURN_LIMIT_QUOTIENT:
-    weak_subjectivity_period += SAFETY_DECAY * cfg.CHURN_LIMIT_QUOTIENT div (2 * 100)
-  else:
-    weak_subjectivity_period +=
-      SAFETY_DECAY * validator_count div (2 * 100 * cfg.MIN_PER_EPOCH_CHURN_LIMIT)
-  return weak_subjectivity_period
+    cfg: RuntimeConfig, state: ForkyBeaconState): uint64 =
+  ## Returns the weak subjectivity period for the current ``state``.
+  ## This computation takes into account the effect of:
+  ##     - validator set churn
+  ##       (bounded by ``get_validator_churn_limit()`` per epoch), and
+  ##     - validator balance top-ups
+  ##       (bounded by ``MAX_DEPOSITS * SLOTS_PER_EPOCH`` per epoch).
+  ## A detailed calculation can be found at:
+  ## https://github.com/runtimeverification/beacon-chain-verification/blob/master/weak-subjectivity/weak-subjectivity-analysis.pdf
+  var
+    cache: StateCache
+    ws_period = cfg.MIN_VALIDATOR_WITHDRAWABILITY_DELAY
+  let
+    N = get_active_validator_indices_len(state, get_current_epoch(state))
+    t = (get_total_active_balance(state, cache) div N).toEther
+  const T = MAX_EFFECTIVE_BALANCE.toEther
+  let delta = cfg.get_validator_churn_limit(state, cache)
+  const
+    Delta = MAX_DEPOSITS * SLOTS_PER_EPOCH
+    D = SAFETY_DECAY
 
-# https://github.com/ethereum/consensus-specs/blob/v1.3.0/specs/phase0/weak-subjectivity.md#checking-for-stale-weak-subjectivity-checkpoint
+  if T * (200 + 3 * D) < t * (200 + 12 * D):
+    let
+      epochs_for_validator_set_churn =
+        N * (t * (200 + 12 * D) - T * (200 + 3 * D)) div
+          (600 * delta * (2 * t + T))
+      epochs_for_balance_top_ups =
+        N * (200 + 3 * D) div (600 * Delta)
+    ws_period += max(epochs_for_validator_set_churn, epochs_for_balance_top_ups)
+  else:
+    ws_period += 3 * N * D * t div (200 * Delta * (T - t))
+
+  ws_period
+
+# https://github.com/ethereum/consensus-specs/blob/v1.3.0/specs/phase0/weak-subjectivity.md#is_within_weak_subjectivity_period
 func is_within_weak_subjectivity_period*(cfg: RuntimeConfig, current_slot: Slot,
                                          ws_state: ForkedHashedBeaconState,
                                          ws_checkpoint: Checkpoint): bool =
-  # Clients may choose to validate the input state against the input Weak Subjectivity Checkpoint
+  ## Clients may choose to validate the input state against the input Weak Subjectivity Checkpoint
   doAssert getStateField(ws_state, latest_block_header).state_root ==
     ws_checkpoint.root
   doAssert epoch(getStateField(ws_state, slot)) == ws_checkpoint.epoch
 
   let
-    ws_period = compute_weak_subjectivity_period(cfg, ws_state)
+    ws_period = withState(ws_state):
+      cfg.compute_weak_subjectivity_period(forkyState.data)
     ws_state_epoch = epoch(getStateField(ws_state, slot))
     current_epoch = epoch(current_slot)