-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathkeccak.lem
202 lines (155 loc) · 6.52 KB
/
keccak.lem
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
(*
Copyright 2016 Sami Mäkelä
Licensed under the Apache License; Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing; software
distributed under the License is distributed on an "AS IS" BASIS;
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND; either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
open import Pervasives
open import Word
open import Word8
import Evm
(*
definition "rotl64 (x :: 64 word) n = (word_rotl n x :: 64 word)"
*)
type word64 = int64
val rotl64 : word64 -> nat -> word64
let rotl64 w n = (w lsr (64 - n)) lor (w lsl n)
val big : word64
let big = 1 lsl 63
val keccakf_randc : list word64
let keccakf_randc = [
0X0000000000000001; 0X0000000000008082; 0X000000000000808a lor big;
0X0000000080008000 lor big; 0X000000000000808b; 0X0000000080000001;
0X0000000080008081 lor big; 0X0000000000008009 lor big; 0X000000000000008a;
0X0000000000000088; 0X0000000080008009; 0X000000008000000a;
0X000000008000808b; 0X000000000000008b lor big; 0X0000000000008089 lor big;
0X0000000000008003 lor big; 0X0000000000008002 lor big; 0X0000000000000080 lor big;
0X000000000000800a; 0X000000008000000a lor big; 0X0000000080008081 lor big;
0X0000000000008080 lor big; 0X0000000080000001; 0X0000000080008008 lor big
]
val keccakf_rotc : list nat
let keccakf_rotc = [
1; 3; 6; 10; 15; 21; 28; 36; 45; 55; 2; 14;
27; 41; 56; 8; 25; 43; 62; 18; 39; 61; 20; 44
]
val keccakf_piln : list nat
let keccakf_piln = [
10; 7; 11; 17; 18; 3; 5; 16; 8; 21; 24; 4;
15; 23; 19; 13; 12; 2; 20; 14; 22; 9; 6; 1
]
val get : list word64 -> nat -> word64
let get lst n = match index lst n with
| Just x -> x
| Nothing -> 0
end
val get_n : list nat -> nat -> nat
let get_n lst n = match index lst n with
| Just x -> x
| Nothing -> 0
end
val set : list word64 -> nat -> word64 -> list word64
let set lst n w =
if List.length lst < n then lst ++ genlist (fun _ -> 0) (List.length lst - n - 1) ++ [w]
else take (n-1) lst ++ [w] ++ drop (n+1) lst
val theta1 : nat -> list word64 -> word64
let theta1 i st =
(get st i) lxor
(get st (i + 5)) lxor
(get st (i + 10)) lxor
(get st (i + 15)) lxor
(get st (i + 20))
val theta_t : nat -> list word64 -> word64
let theta_t i bc =
(get bc ((i + 4) mod 5)) lxor (rotl64 (get bc ((i + 1) mod 5)) 1)
val theta : list word64 -> list word64
let theta st =
let bc = genlist (fun i -> theta1 i st) 5 in
let t = genlist (fun i -> theta_t i bc) 5 in
genlist (fun ji -> (get st ji) lxor (get t (ji mod 5))) 25
val rho_pi_inner : nat -> word64 * list word64 -> word64 * list word64
let rho_pi_inner i t_st =
let j = get_n keccakf_piln i in
let bc = get (snd t_st) j in
(bc, set (snd t_st) j (rotl64 (fst t_st) (get_n keccakf_rotc i)))
val rho_pi_changes : nat -> word64 * list word64 -> word64 * list word64
let rho_pi_changes i t_st = foldr rho_pi_inner t_st (genlist (fun x -> x) i)
val rho_pi : list word64 -> list word64
let rho_pi st = snd (rho_pi_changes 24 (get st 1, st))
val chi_for_j : list word64 -> list word64
let chi_for_j st_slice =
genlist (fun i -> (get st_slice i) lxor ((lnot (get st_slice ((i + 1) mod 5))) land (get st_slice ((i + 2) mod 5)))) 5
val filterI : forall 'a. list 'a -> (nat -> bool) -> list 'a
let filterI lst pred =
List.map fst (filter (fun p -> pred (snd p)) (zip lst (genlist (fun i -> i) (length lst))))
val chi : list word64 -> list word64
let chi st =
List.concat (genlist (fun j -> chi_for_j (filterI st (fun i -> j * 5 <= i && i <= j*5 + 5))) 5)
val iota : nat -> list word64 -> list word64
let iota r st = set st 0 (get st 0 lxor get keccakf_randc r)
val for_inner : nat -> list word64 -> list word64
let for_inner r st = iota r (chi (rho_pi (theta st)))
let keccakf_rounds : nat = 24
type byte = word8
val apply : forall 'a. ('a -> 'a) -> nat -> 'a -> 'a
let rec apply f n acc = match n with
| 0 -> acc
| n+1 -> f (apply f n acc)
end
val boolListFromWord64 : word64 -> list bool
let boolListFromWord64 w = snd (apply (fun (w,lst) -> (w lsr 1, (w land 1 = 0) :: lst)) 64 (w, []))
val boolListFromWord8 : word8 -> list bool
let boolListFromWord8 w = snd (apply (fun (w,lst) -> (w lsr 1, (w land 1 = 0) :: lst)) 8 (w, []))
val word_rsplit_aux : list bool -> nat -> list byte
let rec word_rsplit_aux lst n = match n with
| 0 -> []
| n+1 -> word8FromBoollist (take 8 lst) :: word_rsplit_aux (drop 8 lst) n
end
declare termination_argument word_rsplit_aux = automatic
val word_rsplit : word64 -> list byte
let word_rsplit w = word_rsplit_aux (boolListFromWord64 w) 8
declare isabelle target_rep function word_rsplit = `word_rsplit`
val word64FromBoollist : list bool -> word64
let rec word64FromBoollist lst = match lst with
| true :: lst -> 1 + 2 * word64FromBoollist lst
| false :: lst -> 2 * word64FromBoollist lst
| [] -> 0
end
val word_rcat : list byte -> word64
let word_rcat lst = word64FromBoollist (List.concat (map boolListFromWord8 lst))
val invert_endian : word64 -> word64
let invert_endian w = word_rcat (reverse (word_rsplit w))
val keccakf : list word64 -> list word64
let keccakf st = foldr for_inner st (genlist (fun i -> i) keccakf_rounds)
let mdlen : nat = 256 div 8
let rsiz : nat = 200 - mdlen * 2
val word8_to_word64 : byte -> word64
let word8_to_word64 w = int64FromNat (word8ToNat w)
val update_byte : byte -> nat -> list word64 -> list word64
let update_byte i p st = set st (p div 8) ((get st (p div 8)) lxor ((word8_to_word64 i) lsl (8 * (p mod 8))))
val sha3_update : list byte -> nat -> list word64 -> nat * list word64
let sha3_update lst pos st = match lst with
| [] -> (pos, st)
| c :: rest ->
if (pos <= rsiz) then sha3_update rest (pos + 1) (update_byte c pos st)
else sha3_update rest 0 (keccakf (update_byte c pos st))
end
val keccak_final : nat -> list word64 -> list byte
let keccak_final p st =
let st0 = update_byte 0X01 p st in
let st1 = update_byte 0X80 (rsiz - 1) st0 in
let st2 = take 4 (keccakf st1) in
List.concat (map (fun x -> reverse (word_rsplit x)) st2)
let initial_st : list word64 = genlist (fun _ -> 0) 25
let initial_pos : nat = 0
val keccak' : list byte -> list byte
let keccack' input =
let mid = sha3_update input initial_pos initial_st in
keccak_final (fst mid) (snd mid)
val keccak : list byte -> Evm.uint
let keccak input = Evm.word_of_bytes (keccak' input)