Merge pull request #2190 from ethereum/update-ws-calc

Updated Weak Subjectivity Calculations

specs/phase0/weak-subjectivity.md

@@ -8,13 +8,17 @@
 
 - [Introduction](#introduction)
 - [Prerequisites](#prerequisites)
+- [Custom Types](#custom-types)
 - [Constants](#constants)
+- [Configuration](#configuration)
 - [Weak Subjectivity Checkpoint](#weak-subjectivity-checkpoint)
 - [Weak Subjectivity Period](#weak-subjectivity-period)
   - [Calculating the Weak Subjectivity Period](#calculating-the-weak-subjectivity-period)
+    - [`compute_weak_subjectivity_period`](#compute_weak_subjectivity_period)
 - [Weak Subjectivity Sync](#weak-subjectivity-sync)
   - [Weak Subjectivity Sync Procedure](#weak-subjectivity-sync-procedure)
   - [Checking for Stale Weak Subjectivity Checkpoint](#checking-for-stale-weak-subjectivity-checkpoint)
+    - [`is_within_weak_subjectivity_period`](#is_within_weak_subjectivity_period)
 - [Distributing Weak Subjectivity Checkpoints](#distributing-weak-subjectivity-checkpoints)
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
@@ -34,10 +38,22 @@ For more information about weak subjectivity and why it is required, please refe
 This document uses data structures, constants, functions, and terminology from
 [Phase 0 -- The Beacon Chain](./beacon-chain.md) and [Phase 0 -- Beacon Chain Fork Choice](./fork-choice.md).
 
+## Custom Types
+
+| Name | SSZ Equivalent | Description |
+|---|---|---|
+| `Ether` | `uint64` | an amount in Ether |
+
 ## Constants
 
-| Name           | Value        |
+| Name | Value |
-|----------------|--------------|
+|---|---|
+| `ETH_TO_GWEI` | `uint64(10**9)` |
+
+## Configuration
+
+| Name | Value |
+|---|---|
 | `SAFETY_DECAY` | `uint64(10)` |
 
 ## Weak Subjectivity Checkpoint
@@ -59,38 +75,64 @@ a safety margin of at least `1/3 - SAFETY_DECAY/100`.
 
 ### Calculating the Weak Subjectivity Period
 
-*Note*: `compute_weak_subjectivity_period()` is planned to be updated when a more accurate calculation is made.
+A detailed analysis of the calculation of the weak subjectivity period is made in [this report](https://github.com/runtimeverification/beacon-chain-verification/blob/master/weak-subjectivity/weak-subjectivity-analysis.pdf).
+
+*Note*: The expressions in the report use fractions, whereas eth2.0-specs uses only `uint64` arithmetic. The expressions have been simplified to avoid computing fractions, and more details can be found [here](https://www.overleaf.com/read/wgjzjdjpvpsd).
+
+*Note*: The calculations here use `Ether` instead of `Gwei`, because the large magnitude of balances in `Gwei` can cause an overflow while computing using `uint64` arithmetic operations. Using `Ether` reduces the magnitude of the multiplicative factors by an order of `ETH_TO_GWEI` (`= 10**9`) and avoid the scope for overflows in `uint64`.
+
+#### `compute_weak_subjectivity_period`
 
 ```python
 def compute_weak_subjectivity_period(state: BeaconState) -> uint64:
-    weak_subjectivity_period = MIN_VALIDATOR_WITHDRAWABILITY_DELAY
+    """
-    validator_count = len(get_active_validator_indices(state, get_current_epoch(state)))
+    Returns the weak subjectivity period for the current ``state``. 
-    if validator_count >= MIN_PER_EPOCH_CHURN_LIMIT * CHURN_LIMIT_QUOTIENT:
+    This computation takes into account the effect of:
-        weak_subjectivity_period += SAFETY_DECAY * CHURN_LIMIT_QUOTIENT // (2 * 100)
+        - 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
+    """
+    ws_period = MIN_VALIDATOR_WITHDRAWABILITY_DELAY
+    N = len(get_active_validator_indices(state, get_current_epoch(state)))
+    t = get_total_active_balance(state) // N // ETH_TO_GWEI
+    T = MAX_EFFECTIVE_BALANCE // ETH_TO_GWEI
+    delta = get_validator_churn_limit(state)
+    Delta = MAX_DEPOSITS * SLOTS_PER_EPOCH
+    D = SAFETY_DECAY
+
+    if T * (200 + 3 * D) < t * (200 + 12 * D):
+        epochs_for_validator_set_churn = (
+            N * (t * (200 + 12 * D) - T * (200 + 3 * D)) // (600 * delta * (2 * t + T))
+        )
+        epochs_for_balance_top_ups = (
+            N * (200 + 3 * D) // (600 * Delta)
+        )
+        ws_period += max(epochs_for_validator_set_churn, epochs_for_balance_top_ups)
     else:
-        weak_subjectivity_period += SAFETY_DECAY * validator_count // (2 * 100 * MIN_PER_EPOCH_CHURN_LIMIT)
+        ws_period += (
-    return weak_subjectivity_period
+            3 * N * D * t // (200 * Delta * (T - t))
+        )
+    
+    return ws_period
 ```
 
-*Details about the calculation*:
+A brief reference for what these values look like in practice ([reference script](https://gist.github.com/adiasg/3aceab409b36aa9a9d9156c1baa3c248)):
-- `100` appears in the denominator to get the actual percentage ratio from `SAFETY_DECAY`
-- For more information about other terms in this equation, refer to
-  [Weak Subjectivity in Eth2.0](https://notes.ethereum.org/@adiasg/weak-subjectvity-eth2)
 
-A brief reference for what these values look like in practice:
+| Safety Decay | Avg. Val. Balance (ETH) | Val. Count | Weak Sub. Period (Epochs) |
-
+| ---- | ---- | ---- | ---- |
-| `validator_count` | `weak_subjectivity_period` |
+| 10 | 28 | 32768 | 504 |
-| ----  | ---- |
+| 10 | 28 | 65536 | 752 |
-| 1024  | 268 |
+| 10 | 28 | 131072 | 1248 |
-| 2048  | 281 |
+| 10 | 28 | 262144 | 2241 |
-| 4096  | 307 |
+| 10 | 28 | 524288 | 2241 |
-| 8192  | 358 |
+| 10 | 28 | 1048576 | 2241 |
-| 16384 | 460 |
+| 10 | 32 | 32768 | 665 |
-| 32768 | 665 |
+| 10 | 32 | 65536 | 1075 |
-| 65536 | 1075 |
+| 10 | 32 | 131072 | 1894 |
-| 131072  | 1894 |
+| 10 | 32 | 262144 | 3532 |
-| 262144  | 3532 |
+| 10 | 32 | 524288 | 3532 |
-| 524288  | 3532 |
+| 10 | 32 | 1048576 | 3532 |
 
 ## Weak Subjectivity Sync
 
@@ -101,22 +143,28 @@ Clients should allow users to input a Weak Subjectivity Checkpoint at startup, a
 1. Input a Weak Subjectivity Checkpoint as a CLI parameter in `block_root:epoch_number` format,
   where `block_root` (an "0x" prefixed 32-byte hex string) and `epoch_number` (an integer) represent a valid `Checkpoint`.
   Example of the format:
+
 ```
 0x8584188b86a9296932785cc2827b925f9deebacce6d72ad8d53171fa046b43d9:9544
 ```
-2.  - *IF* `epoch_number > store.finalized_checkpoint.epoch`,
+
-      then *ASSERT* during block sync that block with root `block_root` is in the sync path at epoch `epoch_number`.
+2. Check the weak subjectivity requirements:
-      Emit descriptive critical error if this assert fails, then exit client process.
+    - *IF* `epoch_number > store.finalized_checkpoint.epoch`,
+          then *ASSERT* during block sync that block with root `block_root` is in the sync path at epoch `epoch_number`.
+          Emit descriptive critical error if this assert fails, then exit client process.
     - *IF* `epoch_number <= store.finalized_checkpoint.epoch`,
-      then *ASSERT* that the block in the canonical chain at epoch `epoch_number` has root `block_root`.
+          then *ASSERT* that the block in the canonical chain at epoch `epoch_number` has root `block_root`.
-      Emit descriptive critical error if this assert fails, then exit client process.
+          Emit descriptive critical error if this assert fails, then exit client process.
 
 ### Checking for Stale Weak Subjectivity Checkpoint
+
 Clients may choose to validate that the input Weak Subjectivity Checkpoint is not stale at the time of startup.
 To support this mechanism, the client needs to take the state at the Weak Subjectivity Checkpoint as
 a CLI parameter input (or fetch the state associated with the input Weak Subjectivity Checkpoint from some source).
 The check can be implemented in the following way:
 
+#### `is_within_weak_subjectivity_period`
+
 ```python
 def is_within_weak_subjectivity_period(store: Store, ws_state: BeaconState, ws_checkpoint: Checkpoint) -> bool:
     # Clients may choose to validate the input state against the input Weak Subjectivity Checkpoint
@@ -130,4 +178,5 @@ def is_within_weak_subjectivity_period(store: Store, ws_state: BeaconState, ws_c
 ```
 
 ## Distributing Weak Subjectivity Checkpoints
+
 This section will be updated soon.