-
Notifications
You must be signed in to change notification settings - Fork 0
/
keccak.melo
304 lines (268 loc) · 12.7 KB
/
keccak.melo
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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
provide keccak224
provide keccak256
provide keccak384
provide keccak512
provide shake128
provide shake256
provide sha3_224
provide sha3_256
provide sha3_384
provide sha3_512
provide b2v
provide n2b_8
provide v2b
provide v2b_256
type LaneStr = %[8] # a lane as a bytestring with length 8
type LaneNat = U64 # a lane as a 64-bit Nat
type Sheet = [LaneNat; 5]
type StateLanes = [Sheet; 5]
type State = %[200]
type U8 = {0..255}
type U64 = {0..18446744073709551615}
# ROtate Left 64: rotates 64-bit Nat, n, b bits to the left
def rol64(n: Nat, b: Nat) =
(n << (b % 64) | n >> (64 - (b % 64))) & 18446744073709551615
# Loads a byte vector of length 8 into a 64-bit Nat
def load64(lane_str: LaneStr) =
unsafe let idx = 0 :: {0..7} in
let lane_nat = 0 :: LaneNat in
loop 8 do
lane_nat <- (lane_nat + (lane_str[idx] << (idx * 8))) :! LaneNat;
idx <- (idx + 1) :! {0..7}
return lane_nat
# Stores a 64-bit Nat into a bytestring of length 8
def store64(lane_nat: LaneNat) =
unsafe let idx = 0 :: {0..7} in
let lane_str = "" :! LaneStr in
loop 8 do
lane_str <- (lane_str ++ n2b_8(((lane_nat >> (idx * 8)) % 256) :! U8)) :! LaneStr;
idx <- (idx + 1) :! {0..7}
return lane_str
# Converts State type to StateLanes type
def to_lanes(state: State) =
unsafe let accum = [] :! StateLanes in
let accum_inner = [] :! Sheet in
let x = 0 :: {0..4} in
let y = 0 :: {0..4} in
loop 5 do
accum_inner <- [] :! Sheet;
accum_inner <- loop 5 do
accum_inner <- (accum_inner ++ [load64(unsafe_bslice(state, 8 * (x + 5 * y), 8 * (x + 5 * y) + 8) :! %[8])]) :! Sheet;
y <- (y + 1) :! {0..4}
return accum_inner;
accum <- (accum ++ [accum_inner]) :! StateLanes;
x <- (x + 1) :! {0..4};
return accum
# Returns the C sheet which is necessary for computing the D sheet
def c(lanes: StateLanes) =
unsafe for x in range(5) fold c = [] :! Sheet with (c ++ [
for sheet in lanes[x :! {0..4}] fold accum = 0 :: LaneNat with (accum ^ sheet) :! LaneNat
]) :! Sheet
# Returns the D sheet which is necessary for computing the θ step of the permutation
def d(c: Sheet) =
unsafe for x in range(5) fold d = [] :! Sheet with (d ++ [vref(c, (x + 4) % 5) ^ rol64(vref(c, (x + 1) % 5), 1)]) :! Sheet
# θ step of permutation
def theta(lanes: StateLanes) =
unsafe let c = c(lanes) in
let d = d(c) in
let new_lanes = [] :! StateLanes in
let sheet = [] :! Sheet in
let x = 0 :: {0..4} in
let y = 0 :: {0..4} in
loop 5 do
new_lanes <- (new_lanes ++ loop 5 do
sheet <- (sheet ++ [(lanes[x][y] ^ d[x])]) :! Sheet;
y <- (y + 1) :! {0..4}
return [sheet]) :! StateLanes;
x <- (x + 1) :! {0..4}
return new_lanes
# ρ and π steps of permutation
def rho_and_pi(lanes: StateLanes) =
unsafe let x = 1 :: {0..4} in
let y = 0 :: {0..4} in
let temp_x = 0 :: {0..4} in
let t = 0 :: {0..24} in
let curr_lane = lanes[x][y] in
let temp_lane = 0 :! LaneNat in
loop 24 do
temp_x <- x;
x <- y;
y <- ((2 * temp_x + 3 * y) % 5) :! {0..4};
temp_lane <- curr_lane;
curr_lane <- lanes[x][y];
lanes <- lanes[x => lanes[x][y => rol64(temp_lane, (t + 1) * (t + 2) / 2) :! LaneNat]];
t <- (t + 1) :! {0..23}
return lanes
# Returns the T sheet which is necessary for computing the χ step of the permutation
def t(lanes: StateLanes, y: {0..4}) =
[sheet[y] for sheet in lanes]
# χ step of permutation
def chi(lanes: StateLanes) =
unsafe let y = 0 :: {0..4} in
let x = 0 :: {0..4} in
let t = [] :! Sheet in
loop 5 do
t <- t(lanes, y);
lanes <- loop 5 do
lanes <- lanes[x => lanes[x][y => (t[x] ^ ((~vref(t, (x + 1) % 5)) & vref(t, (x + 2) % 5))) :! LaneNat]];
x <- (x + 1) :! {0..4}
return lanes;
y <- (y + 1) :! {0..4}
return lanes
# ι step of permutation
def iota(lanes: StateLanes, r: U8) =
unsafe let j = 0 :: Nat in
loop 7 do
r <- (((r << 1) ^ ((r >> 7) * 113)) % 256) :! U8;
lanes <- if r & 2 then lanes[0 => lanes[0][0 => (lanes[0][0] ^ (1 << ((1 << j) - 1))) :! LaneNat]] else lanes;
j <- j + 1
return [lanes] ++ [r]
# Keccak-f1600 permutation on lanes
def keccak_f1600_on_lanes(lanes: StateLanes) =
unsafe let r = 1 :: U8 in
let lanes_and_r = [] :! [StateLanes, U8] in
loop 24 do
lanes_and_r <- iota(chi(rho_and_pi(theta(lanes))), r);
lanes <- lanes_and_r[0];
r <- lanes_and_r[1]
return lanes
# Keccak-f1600 permutation on state
def keccak_f1600(state: State) =
unsafe let lanes = keccak_f1600_on_lanes(to_lanes(state)) in
let x = 0 :: {0..4} in
let y = 0 :: {0..4} in
let b = 0 :: {0..7} in
loop 5 do
state <- loop 5 do
state <- loop 8 do
state <- bupdate(state, 8 * (x + 5 * y) + b, store64(lanes[x][y])[b] :! U8);
b <- (b + 1) :! {0..7}
return state;
y <- (y + 1) :! {0..4}
return state;
x <- (x + 1) :! {0..4}
return state
# Returns the smaller of two Nats
def min(x: Nat, y: Nat): Nat =
if x > y then y else x
# Utility function for converting U8 to %[1]
def n2b_8(n: U8) =
[
x"00", x"01", x"02", x"03", x"04", x"05", x"06", x"07", x"08", x"09", x"0a", x"0b", x"0c", x"0d", x"0e", x"0f",
x"10", x"11", x"12", x"13", x"14", x"15", x"16", x"17", x"18", x"19", x"1a", x"1b", x"1c", x"1d", x"1e", x"1f",
x"20", x"21", x"22", x"23", x"24", x"25", x"26", x"27", x"28", x"29", x"2a", x"2b", x"2c", x"2d", x"2e", x"2f",
x"30", x"31", x"32", x"33", x"34", x"35", x"36", x"37", x"38", x"39", x"3a", x"3b", x"3c", x"3d", x"3e", x"3f",
x"40", x"41", x"42", x"43", x"44", x"45", x"46", x"47", x"48", x"49", x"4a", x"4b", x"4c", x"4d", x"4e", x"4f",
x"50", x"51", x"52", x"53", x"54", x"55", x"56", x"57", x"58", x"59", x"5a", x"5b", x"5c", x"5d", x"5e", x"5f",
x"60", x"61", x"62", x"63", x"64", x"65", x"66", x"67", x"68", x"69", x"6a", x"6b", x"6c", x"6d", x"6e", x"6f",
x"70", x"71", x"72", x"73", x"74", x"75", x"76", x"77", x"78", x"79", x"7a", x"7b", x"7c", x"7d", x"7e", x"7f",
x"80", x"81", x"82", x"83", x"84", x"85", x"86", x"87", x"88", x"89", x"8a", x"8b", x"8c", x"8d", x"8e", x"8f",
x"90", x"91", x"92", x"93", x"94", x"95", x"96", x"97", x"98", x"99", x"9a", x"9b", x"9c", x"9d", x"9e", x"9f",
x"a0", x"a1", x"a2", x"a3", x"a4", x"a5", x"a6", x"a7", x"a8", x"a9", x"aa", x"ab", x"ac", x"ad", x"ae", x"af",
x"b0", x"b1", x"b2", x"b3", x"b4", x"b5", x"b6", x"b7", x"b8", x"b9", x"ba", x"bb", x"bc", x"bd", x"be", x"bf",
x"c0", x"c1", x"c2", x"c3", x"c4", x"c5", x"c6", x"c7", x"c8", x"c9", x"ca", x"cb", x"cc", x"cd", x"ce", x"cf",
x"d0", x"d1", x"d2", x"d3", x"d4", x"d5", x"d6", x"d7", x"d8", x"d9", x"da", x"db", x"dc", x"dd", x"de", x"df",
x"e0", x"e1", x"e2", x"e3", x"e4", x"e5", x"e6", x"e7", x"e8", x"e9", x"ea", x"eb", x"ec", x"ed", x"ee", x"ef",
x"f0", x"f1", x"f2", x"f3", x"f4", x"f5", x"f6", x"f7", x"f8", x"f9", x"fa", x"fb", x"fc", x"fd", x"fe", x"ff",
][n]
# Utility function for functional updates of bytestrings
def bupdate<$n>(bstr: %[$n + 1], update_idx: {0..$n}, byte: U8) =
unsafe let idx = 0 :: {0..$n} in
let updated_str = "" :! %[$n +1] in
loop $n + 1 do
updated_str <- (updated_str ++ if idx == update_idx then n2b_8(byte) else n2b_8(bstr[idx])) :! %[$n + 1];
idx <- (idx + 1) :! {0..$n}
return updated_str
# Keccak sponge function which has as a building block the Keccak-f1600 permutation
def keccak<$r, $n, $o>(bitrate: {$r * 8}, capacity: {0..1592}, input: %[$n + 1], delim_suffix: U8, output_len: {$o}) =
unsafe if !(capacity + bitrate == 1600) then fail! else
let state = x"0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000" :: State in
let byterate = bitrate / 8 in
let input_len = blen(input) in
let offset = 0 :: {0..$n} in
let blk_size = 0 :: {0..$r * 8} in
let i = 0 :: {0..199} in
let offset_state_blksize = [] :! [{0..$n}, State, {0..$r * 8}] in
let state_and_blksize = loop $n + 1 do
blk_size <- if offset < input_len then min(input_len - offset, byterate) :! {0..$r * 8} else blk_size;
state <- if offset < input_len
then loop $r * 8 do
state <- if i < blk_size then bupdate(state, i, (state[i] ^ input[(offset + i) :! {0..$n}]) :! U8) else state;
i <- (i + 1) :! {0..199}
return state
else state;
offset_state_blksize <- if offset < input_len
then loop 1 do
offset <- (offset + blk_size) :! {0..$n};
state <- if blk_size == byterate then keccak_f1600(state) else state;
blk_size <- if blk_size == byterate then 0 else blk_size
return [offset] ++ [state] ++ [blk_size]
else [offset] ++ [state] ++ [blk_size];
offset <- offset_state_blksize[0];
state <- offset_state_blksize[1];
blk_size <- offset_state_blksize[2]
return [state, blk_size] in
let state = state_and_blksize[0] in
let blk_size = state_and_blksize[1] in
let state = bupdate(state, blk_size :! {0..199}, (state[blk_size :! {0..199}] ^ delim_suffix) :! U8) in
let state = if !((delim_suffix & 128) == 0) && (blk_size == byterate - 1) then keccak_f1600(state) else state in
let state = bupdate(state, (byterate - 1) :! {0..199}, (state[(byterate - 1) :! {0..199}] ^ 128) :! U8) in
let state = keccak_f1600(state) in
let output = "" :! %[$o] in
let accum = "" :! %[$r] in
let i = 0 :: {0..$r} in
loop $o do
accum <- "" :! %[$r];
blk_size <- if output_len > 0 then min(output_len, byterate) :! {0..$r} else blk_size;
output <- if output_len > 0
then (output ++ loop $o do
accum <- if i < blk_size then (accum ++ n2b_8(state[i :! {0..199}])) :! %[$r] else accum;
i <- (i + 1) :! {0..$r}
return accum) :! %[$o]
else output;
output_len <- if output_len > 0 then (output_len - blk_size) :! {$o} else output_len;
return output
# Converts byte vectors of length 32 into byte strings
def v2b_256(vec: [U8; 32]) =
n2b(for byte in enumerate(vec) fold accum = 0 :: Nat with accum + (byte[1] << (8 * (31 - byte[0]))))
# Converts byte vectors of arbitrary length into byte strings
def v2b<$n>(bvec: [U8; $n]) =
unsafe for byte in bvec fold bstr = x"" :! %[$n] with (bstr ++ n2b_8(byte)) :! %[$n]
# Converts byte strings of arbitrary length into byte vectors
def b2v<$n>(bstr: %[$n]) =
unsafe for i in range($n) fold bvec = [] :! [U8; $n] with (bvec ++ [(bstr :! %[$n + 1])[i :! {0..$n}]]) :! [U8; $n]
## The first six of the following interfaces belong to the SHA-3 family of cryptographic hash
## algorithms as standardized by the NIST on August 5, 2015.
# Extendable output function (XOF) with 128 bits of security
def shake128<$n, $o>(input: %[$n + 1], output_len: {$o}) =
keccak<$n = $n>(1344, 256, input, 31, output_len)
# Extendable output function (XOF) with 256 bits of security
def shake256<$n, $o>(input: %[$n + 1], output_len: {$o}) =
keccak<$n = $n>(1088, 512, input, 31, output_len)
# 28-byte output SHA-3 hashing function
def sha3_224<$n>(input: %[$n + 1]) =
keccak<$n = $n>(1152, 448, input, 6, 28)
# 32-byte output SHA-3 hashing function
def sha3_256<$n>(input: %[$n + 1]) =
keccak<$n = $n>(1088, 512, input, 6, 32)
# 48-byte output SHA-3 hashing function
def sha3_384<$n>(input: %[$n + 1]) =
keccak<$n = $n>(832, 768, input, 6, 48)
# 64-byte output SHA-3 hashing function
def sha3_512<$n>(input: %[$n + 1]) =
keccak<$n = $n>(576, 1024, input, 6, 64)
## The last 4 interfaces use the Keccak hashing algorithm as originally submitted to the NIST
## competition before the padding changes in 2015. Ethereum was created in 2013 and as such still
## uses this version of Keccak.
# 28-byte output Keccak hashing function
def keccak224<$n>(input: %[$n + 1]) =
keccak<$n = $n>(1152, 448, input, 1, 28)
# 32-byte output Keccak hashing function
def keccak256<$n>(input: %[$n + 1]) =
keccak<$n = $n>(1088, 512, input, 1, 32)
# 48-byte output Keccak hashing function
def keccak384<$n>(input: %[$n + 1]) =
keccak<$n = $n>(832, 768, input, 1, 48)
# 64-byte output Keccak hashing function
def keccak512<$n>(input: %[$n + 1]) =
keccak<$n = $n>(576, 1024, input, 1, 64)