spec/crypto/sha.bend

bend-collections-laws-crypto@1.0.0.0 · 196 lines · 35 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as Types
3
4# Executable specification of the byte-oriented SHA-256 algorithm in FIPS 180-4.
5# Only the neutral state representation is shared with the implementation.
6# No implementation arithmetic, padding, schedule, table, or hash is called.
7# Base U32 has the required modulo-2^32 arithmetic and logical bit operations.
8
9def initial() -> Types.State:
10  Types.H{1779033703, 3144134277, 1013904242, 2773480762,
11    1359893119, 2600822924, 528734635, 1541459225}
12
13# FIPS 4.1.2: ROR_n(x) = SHR_n(x) OR SHL_(32-n)(x).
14def rotate(+x: U32, +n: Nat) -> U32:
15  U32.or(U32.shrn(x, n), U32.shln(x, Nat.sub(32n, n)))
16
17def sigma0(+x: U32) -> U32:
18  U32.xor(U32.xor(rotate(x, 7n), rotate(x, 18n)), U32.shrn(x, 3n))
19
20def sigma1(+x: U32) -> U32:
21  U32.xor(U32.xor(rotate(x, 17n), rotate(x, 19n)), U32.shrn(x, 10n))
22
23def sum0(+x: U32) -> U32:
24  U32.xor(U32.xor(rotate(x, 2n), rotate(x, 13n)), rotate(x, 22n))
25
26def sum1(+x: U32) -> U32:
27  U32.xor(U32.xor(rotate(x, 6n), rotate(x, 11n)), rotate(x, 25n))
28
29def ch(+x: U32, y: U32, z: U32) -> U32:
30  U32.xor(U32.and(x, y), U32.and(U32.not(x), z))
31
32def maj(+x: U32, +y: U32, +z: U32) -> U32:
33  U32.xor(U32.xor(U32.and(x, y), U32.and(x, z)), U32.and(y, z))
34
35# A base-256 representation, most significant digit first, of fixed width.
36def octets(width: Nat, +n: Nat) -> List<&2, U32>:
37  match width:
38    case 0n:
39      Nil{}
40    case 1n+p:
41      List.append(&2, U32, octets(p, Nat.div(n, 256n)),
42        [U32.from_nat(Nat.mod(n, 256n))])
43
44# 8*n = 256*(n/32) + 8*(n mod 32); avoids overflowing runtime Nat.
45def length_field(+n: Nat) -> List<&2, U32>:
46  List.append(&2, U32, octets(7n, Nat.div(n, 32n)),
47    [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])
48
49# FIPS padding: a remainder of 0..55 leaves room in this block;
50# a remainder of 56..63 needs another block. No modular shortcut is used.
51def zero_count_if(r: Nat, fits: Bool) -> Nat:
52  match fits:
53    case True{}:
54      Nat.sub(55n, r)
55    case False{}:
56      Nat.sub(119n, r)
57
58def zero_count(+r: Nat) -> Nat:
59  zero_count_if(r, Nat.is_le(r, 55n))
60
61def padding_suffix(+n: Nat) -> List<&2, U32>:
62  128 <> List.append(&2, U32,
63    List.replicate(U32, zero_count(Nat.mod(n, 64n)), 0), length_field(n))
64
65def pad(+bytes: List<&2, U32>) -> List<&2, U32>:
66  List.append(&2, U32, bytes, padding_suffix(List.length(&2, U32, bytes)))
67
68def decode(a: U32, b: U32, c: U32, d: U32) -> U32:
69  U32.or(U32.or(U32.or(U32.shln(U32.and(a, 255), 24n),
70    U32.shln(U32.and(b, 255), 16n)), U32.shln(U32.and(c, 255), 8n)), U32.and(d, 255))
71
72def words(bytes: List<&2, U32>) -> List<&2, U32>:
73  match bytes:
74    case a <> b <> c <> d <> rest:
75      decode(a, b, c, d) <> words(rest)
76    case _:
77      Nil{}
78
79# In reverse history, index j denotes W[t-1-j]. Only valid indices are
80# reached for the actual 16-word input blocks; default zero makes nth total.
81def nth(history: List<&2, U32>, index: Nat) -> U32:
82  match history index:
83    case Nil{} _:
84      0
85    case w <> rest 0n:
86      w
87    case w <> rest 1n+p:
88      nth(rest, p)
89
90# The FIPS recurrence names prior words by lags 2, 7, 15 and 16.
91def previous(history: List<&2, U32>, lag: Nat) -> U32:
92  nth(history, Nat.sub(lag, 1n))
93
94def recurrence(+history: List<&2, U32>) -> U32:
95  (sigma1(previous(history, 2n)) + previous(history, 7n)
96    + sigma0(previous(history, 15n)) + previous(history, 16n) : U32)
97
98def extension(rounds: Nat, +history: List<&2, U32>) -> List<&2, U32>:
99  match rounds:
100    case 0n:
101      Nil{}
102    case 1n+p:
103      +w = recurrence(history)
104      w <> extension(p, w <> history)
105
106# Standard SHA-256 instantiates extra=48, extending the initial 16 to 64.
107def schedule(extra: Nat, +block: List<&2, U32>) -> List<&2, U32>:
108  List.append(&2, U32, block, extension(extra, List.reverse(&2, U32, block)))
109
110def schedules(ws: List<&2, U32>, +extra: Nat) -> List<&2, List<&2, U32>>:
111  match ws:
112    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
113      schedule(extra, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]) <> schedules(rest, extra)
114    case _:
115      Nil{}
116
117def prepare(bytes: List<&2, U32>, extra: Nat) -> List<&2, List<&2, U32>>:
118  schedules(words(pad(bytes)), extra)
119
120def step(s: Types.State, k: U32, w: U32) -> Types.State:
121  Types.H{+a, +b, +c, d, +e, +f, +g, h} = s
122  +t1 = (h + sum1(e) + ch(e, f, g) + k + w : U32)
123  t2 = (sum0(a) + maj(a, b, c) : U32)
124  Types.H{(t1 + t2 : U32), a, b, c, (d + t1 : U32), e, f, g}
125
126def rounds(ks: List<&2, U32>, ws: List<&2, U32>) -> Types.State -> Types.State:
127  match ks ws:
128    case Nil{} _:
129      s => s
130    case k <> kt Nil{}:
131      s => s
132    case k <> kt w <> wt:
133      next = rounds(kt, wt)
134      s => next(step(s, k, w))
135
136def feedforward(x: Types.State, y: Types.State) -> Types.State:
137  Types.H{a, b, c, d, e, f, g, h} = x
138  Types.H{i, j, k, l, m, n, o, p} = y
139  Types.H{(a + i : U32), (b + j : U32), (c + k : U32), (d + l : U32),
140    (e + m : U32), (f + n : U32), (g + o : U32), (h + p : U32)}
141
142def compress(ws: List<&2, U32>, ks: List<&2, U32>, +s: Types.State) -> Types.State:
143  feedforward(s, rounds(ks, ws)(s))
144
145def blocks(prepared: List<&2, List<&2, U32>>, +ks: List<&2, U32>) -> Types.State -> Types.State:
146  match prepared:
147    case Nil{}:
148      s => s
149    case block <> rest:
150      next = blocks(rest, ks)
151      s => next(compress(block, ks, s))
152
153def digest(s: Types.State) -> List<&2, U32>:
154  Types.H{a, b, c, d, e, f, g, h} = s
155  [a, b, c, d, e, f, g, h]
156
157def hash(bytes: List<&2, U32>, extra: Nat, ks: List<&2, U32>) -> List<&2, U32>:
158  digest(blocks(prepare(bytes, extra), ks)(initial()))
159
160# FIPS 180-4 section 4.2.2, transcribed separately from the implementation.
161def constants() -> List<&2, U32>:
162  [1116352408, 1899447441, 3049323471, 3921009573,
163   961987163, 1508970993, 2453635748, 2870763221,
164   3624381080, 310598401, 607225278, 1426881987,
165   1925078388, 2162078206, 2614888103, 3248222580,
166   3835390401, 4022224774, 264347078, 604807628,
167   770255983, 1249150122, 1555081692, 1996064986,
168   2554220882, 2821834349, 2952996808, 3210313671,
169   3336571891, 3584528711, 113926993, 338241895,
170   666307205, 773529912, 1294757372, 1396182291,
171   1695183700, 1986661051, 2177026350, 2456956037,
172   2730485921, 2820302411, 3259730800, 3345764771,
173   3516065817, 3600352804, 4094571909, 275423344,
174   430227734, 506948616, 659060556, 883997877,
175   958139571, 1322822218, 1537002063, 1747873779,
176   1955562222, 2024104815, 2227730452, 2361852424,
177   2428436474, 2756734187, 3204031479, 3329325298]
178
179def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
180  hash(bytes, 48n, constants())
181
182# FIPS digest serialization: most significant octet of each word first.
183def word_octets(+w: U32) -> List<&2, U32>:
184  [U32.and(U32.shrn(w, 24n), 255),
185   U32.and(U32.shrn(w, 16n), 255),
186   U32.and(U32.shrn(w, 8n), 255), U32.and(w, 255)]
187
188def digest_octets(ws: List<&2, U32>) -> List<&2, U32>:
189  match ws:
190    case Nil{}:
191      Nil{}
192    case w <> tail:
193      List.append(&2, U32, word_octets(w), digest_octets(tail))
194
195def sha256_bytes(bytes: List<&2, U32>) -> List<&2, U32>:
196  digest_octets(sha256(bytes))