prysm-pulse/tools/specs-checker/data/specs/phase0/weak-subjectivity.md
Victor Farazdagi 3d3b9d1217
Spec checker tool (#8722)
* Add specdocs static code analyzer

* docs pulling script

* update content pulling script

* add test

* better parsing of incoming docs

* update test

* implements analyzer

* separate tool

* remove analyzer code

* cleanup

* deep source fixes

* untrack raw specs files

* add back phase0 defs

* update spec texts

* re-arrange code

* updated spec list

* cleanup

* more comments and readme

* add merkle proofs specs

* add extra.md

* mark wrong length issue

* update readme

* update readme

* remove non-def snippets

* update comment

* check numrows

* ignore last empty line

Co-authored-by: Raul Jordan <raul@prysmaticlabs.com>
2021-04-15 14:54:07 +00:00

45 lines
2.0 KiB
Markdown

```python
def compute_weak_subjectivity_period(state: BeaconState) -> 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
"""
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:
ws_period += (
3 * N * D * t // (200 * Delta * (T - t))
)
return ws_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
assert ws_state.latest_block_header.state_root == ws_checkpoint.root
assert compute_epoch_at_slot(ws_state.slot) == ws_checkpoint.epoch
ws_period = compute_weak_subjectivity_period(ws_state)
ws_state_epoch = compute_epoch_at_slot(ws_state.slot)
current_epoch = compute_epoch_at_slot(get_current_slot(store))
return current_epoch <= ws_state_epoch + ws_period
```