-
Notifications
You must be signed in to change notification settings - Fork 1
/
Config.thy
93 lines (71 loc) · 2.48 KB
/
Config.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
theory Config
imports Main Types
begin
definition GENESIS_EPOCH :: Epoch where
"GENESIS_EPOCH = Epoch 0"
definition TIMELY_SOURCE_FLAG_INDEX :: nat where
"TIMELY_SOURCE_FLAG_INDEX = 0"
definition TIMELY_TARGET_FLAG_INDEX :: nat where
"TIMELY_TARGET_FLAG_INDEX = 1"
definition TIMELY_HEAD_FLAG_INDEX :: nat where
"TIMELY_HEAD_FLAG_INDEX = 2"
definition TIMELY_SOURCE_WEIGHT :: u64 where
"TIMELY_SOURCE_WEIGHT = 14"
definition TIMELY_TARGET_WEIGHT :: u64 where
"TIMELY_TARGET_WEIGHT = 26"
definition TIMELY_HEAD_WEIGHT :: u64 where
"TIMELY_HEAD_WEIGHT = 14"
definition SYNC_REWARD_WEIGHT :: u64 where
"SYNC_REWARD_WEIGHT = 2"
definition PROPOSER_WEIGHT :: u64 where
"PROPOSER_WEIGHT = 8"
definition WEIGHT_DENOMINATOR :: u64 where
"WEIGHT_DENOMINATOR = 64"
definition PARTICIPATION_FLAG_WEIGHTS :: "u64 list" where
"PARTICIPATION_FLAG_WEIGHTS = [
TIMELY_SOURCE_WEIGHT,
TIMELY_TARGET_WEIGHT,
TIMELY_HEAD_WEIGHT
]"
definition INACTIVITY_PENALTY_QUOTIENT_ALTAIR :: u64 where
"INACTIVITY_PENALTY_QUOTIENT_ALTAIR = 50331648"
record Config =
SLOTS_PER_HISTORICAL_ROOT :: u64
HISTORICAL_ROOTS_LIMIT :: u64
EPOCHS_PER_ETH1_VOTING_PERIOD :: u64
SLOTS_PER_EPOCH :: u64
VALIDATOR_REGISTRY_LIMIT :: u64
EPOCHS_PER_HISTORICAL_VECTOR :: u64
EPOCHS_PER_SLASHINGS_VECTOR :: u64
JUSTIFICATION_BITS_LENGTH :: u64
SYNC_COMMITTEE_SIZE :: u64
EFFECTIVE_BALANCE_INCREMENT :: u64
BASE_REWARD_FACTOR :: u64
MIN_EPOCHS_TO_INACTIVITY_PENALTY :: u64
INACTIVITY_SCORE_BIAS :: u64
INACTIVITY_SCORE_RECOVERY_RATE :: u64
MIN_VALIDATOR_WITHDRAWABILITY_DELAY :: u64
CHURN_LIMIT_QUOTIENT :: u64
MIN_PER_EPOCH_CHURN_LIMIT :: u64
EJECTION_BALANCE :: u64
definition PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX :: u64 where
"PROPORTIONAL_SLASHING_MULTIPLIER_BELLATRIX = undefined"
definition SLOTS_PER_ETH1_VOTING_PERIOD :: "Config \<Rightarrow> u64" where
"SLOTS_PER_ETH1_VOTING_PERIOD c \<equiv> EPOCHS_PER_ETH1_VOTING_PERIOD c * SLOTS_PER_EPOCH c"
definition
"HYSTERESIS_QUOTIENT \<equiv> 4 :: u64"
definition
"HYSTERESIS_DOWNWARD_MULTIPLIER \<equiv> 1 :: u64"
definition
"HYSTERESIS_UPWARD_MULTIPLIER \<equiv> 5 :: u64"
definition
"MAX_EFFECTIVE_BALANCE \<equiv> undefined :: u64"
definition
"NUM_FLAG_INDICES \<equiv> undefined :: u64"
definition
"EPOCHS_PER_SYNC_COMMITTEE_PERIOD \<equiv> undefined :: u64"
definition FAR_FUTURE_EPOCH :: Epoch where
"FAR_FUTURE_EPOCH = Epoch (-1)"
definition MAX_SEED_LOOKAHEAD :: Epoch where
"MAX_SEED_LOOKAHEAD = undefined"
end