-
Notifications
You must be signed in to change notification settings - Fork 1
/
Utils.thy
117 lines (93 loc) · 4.23 KB
/
Utils.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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
theory Utils
imports Unsigned Types Invariants
begin
context verified_con
begin
function range where
"range (start :: nat) stop 0 = []" |
"range (start :: nat) stop (Suc n) = (if start \<ge> stop then [] else start # (range (start + (Suc n)) stop (Suc n)))"
apply auto
by (case_tac b; clarsimp)
termination
apply (relation "measure(\<lambda>(i::nat,j, k). (j - i + 1))")
apply (auto)[1]
apply (clarsimp)
by simp
definition enumerate :: "'b list \<Rightarrow> (u64 \<times> 'b) list" where
"enumerate l \<equiv> zip (map nat_to_u64 [0..<length l]) l"
definition safe_sum :: "u64 list \<Rightarrow> (u64, 'a) cont" where
"safe_sum s \<equiv> foldrM word_unsigned_add ( s) 0"
definition var_list_index :: "'b VariableList \<Rightarrow> u64 \<Rightarrow> ('b, 'a) cont" where
"var_list_index l i \<equiv>
if i < var_list_len l then
return (var_list_inner l ! u64_to_nat i)
else
fail"
definition var_list_update :: "'b \<Rightarrow> 'b VariableList \<Rightarrow> u64 \<Rightarrow> ('b VariableList, 'a) cont" where
"var_list_update e l i \<equiv>
if i < var_list_len l then
return ( VariableList (list_update (var_list_inner l) (u64_to_nat i) e))
else
fail"
definition var_list_inner :: "'b VariableList \<Rightarrow> 'b list" where
"var_list_inner l \<equiv> case l of VariableList inner \<Rightarrow> inner"
definition vector_inner :: "'b Vector \<Rightarrow> 'b list" where
"vector_inner l \<equiv> case l of Vector inner \<Rightarrow> inner"
definition unsafe_var_list_index :: "'b VariableList \<Rightarrow> u64 \<Rightarrow> 'b" where
"unsafe_var_list_index l i \<equiv> (var_list_inner l ! unat i) "
definition vector_index :: "'b Vector \<Rightarrow> u64 \<Rightarrow> ('b, 'a) cont" where
"vector_index v i \<equiv>
if i < vector_len v then
return (vector_inner v ! u64_to_nat i)
else
fail"
definition vector_update :: "'b \<Rightarrow> 'b Vector \<Rightarrow> u64 \<Rightarrow> ('b Vector, 'a) cont" where
"vector_update e l i \<equiv>
if i < vector_len l then
return (Vector (list_update (vector_inner l) (u64_to_nat i) e))
else
fail"
definition unsafe_vector_index :: "'b Vector \<Rightarrow> u64 \<Rightarrow> 'b" where
"unsafe_vector_index v i \<equiv> (vector_inner v ! (unat i))"
definition shift_and_clear_bitvector :: "Config \<Rightarrow> Bitvector \<Rightarrow> Bitvector" where
"shift_and_clear_bitvector c bv \<equiv>
Bitvector ([False] @ take (u64_to_nat (JUSTIFICATION_BITS_LENGTH c) - 1) (bitvector_inner bv))"
definition bitvector_update :: "Bitvector \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> Bitvector" where
"bitvector_update bv i v \<equiv> Bitvector (list_update (bitvector_inner bv) i v)"
definition bitvector_all :: "Bitvector \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
"bitvector_all bv start end \<equiv>
list_all (\<lambda>x. x) (take (end - start) (drop start (bitvector_inner bv)))"
function integer_squareroot_aux :: "u64 \<Rightarrow> u64 \<Rightarrow> u64 \<Rightarrow> ((u64 \<times> u64), 'a) cont" where
"integer_squareroot_aux x y n =
(if y \<ge> x then
return (x, y)
else do {
offset <- n \\ y;
y' \<leftarrow> y .+ offset;
integer_squareroot_aux y (y' div 2) n
})"
by auto
termination
apply (relation "measure (\<lambda>(x,y,n). unat x)") unfolding word_add_def
apply (clarsimp)
apply (subst in_measure, clarify)
apply (clarsimp)
by (simp add: unat_mono)
(* https://github.com/ethereum/consensus-specs/blob/dev/specs/phase0/beacon-chain.md#integer_squareroot *)
definition integer_squareroot :: "u64 \<Rightarrow> (u64, 'a) cont" where
"integer_squareroot n = do {
let x = n;
x_plus_1 \<leftarrow> x .+ 1;
y \<leftarrow> x_plus_1 \\ 2;
(x', _) \<leftarrow> integer_squareroot_aux x y n;
return x'
}"
definition is_eligible_for_activation_queue :: "Validator \<Rightarrow> bool" where
"is_eligible_for_activation_queue val \<equiv>
activation_eligibility_epoch_f val = FAR_FUTURE_EPOCH \<and>
effective_balance_f val = MAX_EFFECTIVE_BALANCE"
(* Opaque definition, we do not actually implement hashing *)
definition hash_tree_root :: "'b \<Rightarrow> Hash256" where
"hash_tree_root x \<equiv> undefined"
end
end