src/hub_sha/sha256.bend

mylsm-lsm-store@0.6.0.1 · 398 lines · 44 definitions

1# Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f
2# (src/crypto/sha/sha256.bend), byte-identical. See core.bend header.
3import Base
4import mylsm-lsm-store@0.6.0.1/src/hub_sha/core.bend as Core
5import mylsm-lsm-store@0.6.0.1/src/hub_sha/state.bend as S
6import bend-kit-bytes@0.3.2.0/bytes.bend as Packed
7import mylsm-lsm-store@0.6.0.1/src/coordinator/QueuePolicy.bend as QueuePolicy
8
9# Describes failures while enforcing the streaming hash input bound.
10type StreamError is Data:
11  ResourceLimit{}
12
13# Retains the compressed hash state and one incomplete block.
14type Stream is Type:
15  Stream{compressed: S.State, tail: Packed.Bytes, total: Nat}
16
17# The core refinement theorem quantifies over every constant table.
18# Instantiate the verified core with the FIPS 180-4 constants.
19def constants() -> List<&2, U32>:
20  [1116352408, 1899447441, 3049323471, 3921009573,
21   961987163, 1508970993, 2453635748, 2870763221,
22   3624381080, 310598401, 607225278, 1426881987,
23   1925078388, 2162078206, 2614888103, 3248222580,
24   3835390401, 4022224774, 264347078, 604807628,
25   770255983, 1249150122, 1555081692, 1996064986,
26   2554220882, 2821834349, 2952996808, 3210313671,
27   3336571891, 3584528711, 113926993, 338241895,
28   666307205, 773529912, 1294757372, 1396182291,
29   1695183700, 1986661051, 2177026350, 2456956037,
30   2730485921, 2820302411, 3259730800, 3345764771,
31   3516065817, 3600352804, 4094571909, 275423344,
32   430227734, 506948616, 659060556, 883997877,
33   958139571, 1322822218, 1537002063, 1747873779,
34   1955562222, 2024104815, 2227730452, 2361852424,
35   2428436474, 2756734187, 3204031479, 3329325298]
36
37# SHA-256 for the reference octet-list input.
38def sha256(bytes: List<&2, U32>) -> List<&2, U32>:
39  Core.sha256(bytes)
40
41# Convert ASCII text to the reference octet-list input.
42def ascii(text: String) -> List<&2, U32>:
43  Core.ascii(text)
44
45# Format eight digest words as lowercase hexadecimal.
46def hex(ws: List<&2, U32>) -> String:
47  Core.hex(ws)
48
49# Big-endian octets, represented as U32 values in 0..255.
50def digest_bytes(ws: List<&2, U32>) -> List<&2, U32>:
51  match ws:
52    case Nil{}:
53      Nil{}
54    case +w <> tail:
55      U32.and(U32.shrn(w, 24n), 255) <>
56      U32.and(U32.shrn(w, 16n), 255) <>
57      U32.and(U32.shrn(w, 8n), 255) <>
58      U32.and(w, 255) <> digest_bytes(tail)
59
60# Return the reference digest as eight big-endian octets per word.
61def sha256_bytes(bytes: List<&2, U32>) -> List<&2, U32>:
62  digest_bytes(sha256(bytes))
63
64# Compress one packed block using sixteen transient big-endian words. The file
65# buffer stays packed; no per-byte List is constructed for complete blocks.
66def packed.compress(words: List<&2, U32>, state: S.State) -> S.State:
67  match words:
68    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}:
69      Core.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 48n, state)
70    case _:
71      state
72
73# Read complete 64-byte blocks directly through a bounded package cursor.
74def packed.blocks(
75  remaining: Nat,
76  in_block: Nat,
77  pair: Packed.Cursor & Maybe<&2, U32>,
78  acc: List<&2, U32>,
79  state: S.State
80) -> Packed.Cursor & S.State:
81  match remaining:
82    case 0n:
83      match pair:
84        case (cursor, _):
85          (cursor, state)
86    case 1n:
87      match in_block:
88        case 0n:
89          match pair:
90            case (cursor, _):
91              (cursor, state)
92        case 1n:
93          match pair:
94            case (cursor, Some{word}):
95              (cursor, packed.compress(List.reverse(&2, U32, word <> acc), state))
96            case (cursor, None{}):
97              (cursor, state)
98        case 1n+more:
99          match pair:
100            case (cursor, _):
101              (cursor, state)
102    case 1n+more:
103      match in_block:
104        case 0n:
105          match pair:
106            case (cursor, _):
107              (cursor, state)
108        case 1n:
109          match pair:
110            case (cursor, Some{word}):
111              packed.blocks(more, 16n, Packed.Cursor.u32be(cursor), Nil{},
112                packed.compress(List.reverse(&2, U32, word <> acc), state))
113            case (cursor, None{}):
114              (cursor, state)
115        case 1n+left:
116          match pair:
117            case (cursor, Some{word}):
118              packed.blocks(more, left, Packed.Cursor.u32be(cursor), word <> acc, state)
119            case (cursor, None{}):
120              (cursor, state)
121
122# Read the remaining fewer than 64 bytes for the existing constant-space tail
123# padding routines. This list is bounded by 63 octets, regardless of file size.
124def packed.tail(
125  remaining: Nat,
126  pair: Packed.Cursor & Maybe<&2, U32>,
127  acc: List<&2, U32>
128) -> Packed.Cursor & List<&2, U32>:
129  match remaining:
130    case 0n:
131      match pair:
132        case (cursor, _):
133          (cursor, List.reverse(&2, U32, acc))
134    case 1n:
135      match pair:
136        case (cursor, Some{byte}):
137          (cursor, List.reverse(&2, U32, byte <> acc))
138        case (cursor, None{}):
139          (cursor, Nil{})
140    case 1n+more:
141      match pair:
142        case (cursor, Some{byte}):
143          packed.tail(more, Packed.Cursor.u8(cursor), byte <> acc)
144        case (cursor, None{}):
145          (cursor, Nil{})
146
147def packed.finish.tail(total: U32, pair: Packed.Cursor & List<&2, U32>, state: S.State) -> S.State:
148  match pair:
149    case (_, tail):
150      Core.finish_n(tail, U32.to_nat(total), 48n, state)
151
152def packed.final.tail(total: U32, tail_len: Nat, cursor: Packed.Cursor, state: S.State) -> S.State:
153  match tail_len:
154    case 0n:
155      packed.finish.tail(total, (cursor, Nil{}), state)
156    case 1n+more:
157      packed.finish.tail(total, packed.tail(1n+more, Packed.Cursor.u8(cursor), Nil{}), state)
158
159def packed.final(total: U32, tail_len: Nat, cursor: Packed.Cursor, state: S.State) -> List<&2, U32>:
160  Core.digest(packed.final.tail(total, tail_len, cursor, state))
161
162def packed.after_blocks(total: U32, tail_len: Nat, pair: Packed.Cursor & S.State) -> List<&2, U32>:
163  match pair:
164    case (cursor, state):
165      packed.final(total, tail_len, cursor, state)
166
167def packed.start.blocks(+total: U32, cursor: Packed.Cursor, blocks: Nat, +tail_len: Nat) -> List<&2, U32>:
168  match blocks:
169    case 0n:
170      packed.final(total, tail_len, cursor, Core.initial())
171    case 1n+more:
172      packed.after_blocks(total, tail_len,
173        packed.blocks(((1n+more) * 16n : Nat), 16n, Packed.Cursor.u32be(cursor), Nil{}, Core.initial()))
174
175def packed.start(+total: U32, cursor: Packed.Cursor) -> List<&2, U32>:
176  packed.start.blocks(total, cursor,
177    Nat.div(U32.to_nat(total), 64n), Nat.mod(U32.to_nat(total), 64n))
178
179# SHA-256 directly over packed bytes. Full blocks are read as sixteen u32be
180# words; only the final 0..63 octets use the existing tail padding interface.
181def sha256_packed(bytes: Packed.Bytes) -> List<&2, U32>:
182  match bytes:
183    case Packed.Bytes{+len, buf}:
184      packed.start(len, Packed.Cursor.new(Packed.Bytes{len, buf}))
185
186def packed.digest.finish.bytes(pair: Packed.Bytes & U32) -> Packed.Bytes:
187  match pair:
188    case (bytes, _):
189      bytes
190
191def packed.digest.finish(pair: Packed.Cursor & Bool) -> Packed.Bytes:
192  match pair:
193    case (cursor, _):
194      packed.digest.finish.bytes(Packed.Cursor.finish(cursor))
195
196def packed.digest.words(words: List<&2, U32>, pair: Packed.Cursor & Bool) -> Packed.Bytes:
197  match words:
198    case Nil{}:
199      packed.digest.finish(pair)
200    case word <> rest:
201      match pair:
202        case (cursor, _) :
203          packed.digest.words(rest, Packed.Cursor.put.u32be(cursor, word))
204
205# Return the SHA-256 digest as packed bytes in canonical big-endian order.
206def sha256_packed_bytes(bytes: Packed.Bytes) -> Packed.Bytes:
207  packed.digest.words(sha256_packed(bytes),
208    (Packed.Cursor.new(Packed.Bytes{32, Packed.alloc(32)}), True{}))
209
210def stream.empty.bytes() -> Packed.Bytes:
211  Packed.Bytes{0, Packed.alloc(0)}
212
213def stream.initial() -> Stream:
214  Stream{Core.initial(), stream.empty.bytes(), 0n}
215
216def stream.clone.bytes(+len: U32, copies: Array<U32> & Array<U32>) -> Packed.Bytes & Packed.Bytes:
217  match copies:
218    case (left, right):
219      (Packed.Bytes{len, left}, Packed.Bytes{len, right})
220
221def stream.clone.tail(
222  +compressed: S.State,
223  totals: Nat & Nat,
224  copies: Packed.Bytes & Packed.Bytes
225) -> Stream & Stream:
226  match totals:
227    case (left_total, right_total):
228      match copies:
229        case (left_tail, right_tail):
230          (Stream{compressed, left_tail, left_total},
231            Stream{compressed, right_tail, right_total})
232
233def stream.clone.parts(
234  +compressed: S.State,
235  totals: Nat & Nat,
236  tail: Packed.Bytes
237) -> Stream & Stream:
238  match tail:
239    case Packed.Bytes{+len, buf}:
240      stream.clone.tail(compressed, totals,
241        stream.clone.bytes(len, Packed.copy.bytes(len, buf,
242          Packed.alloc(len), 0, 0)))
243
244def stream.clone(state: Stream) -> Stream & Stream:
245  match state:
246    case Stream{compressed, tail, +total}:
247      stream.clone.parts(compressed, QueuePolicy.nat.clone.pair(total), tail)
248
249def stream.length(pair: Packed.Bytes & U32) -> U32:
250  match pair:
251    case (_, size): size
252
253def stream.count(pair: Packed.Cursor & S.State) -> S.State:
254  match pair:
255    case (_, compressed): compressed
256
257def stream.compress(bytes: Packed.Bytes, compressed: S.State) -> S.State:
258  match bytes:
259    case Packed.Bytes{+len, buf}:
260      stream.count(packed.blocks(
261        Nat.mul(Nat.div(U32.to_nat(len), 64n), 16n), 16n,
262        Packed.Cursor.u32be(Packed.Cursor.new(Packed.Bytes{len, buf})),
263        Nil{}, compressed))
264
265def stream.tail.result.sliced(
266  +compressed: S.State,
267  complete: Packed.Bytes,
268  pair: Packed.Bytes & Packed.Bytes,
269  total: Nat
270) -> Result<&1, &1, StreamError, Stream>:
271  match pair:
272    case (_, tail):
273      Done{Stream{stream.compress(complete, compressed), tail, total}}
274def stream.tail.result(
275  +compressed: S.State,
276  joined: Packed.Bytes,
277  complete: Packed.Bytes,
278  full_length: Nat,
279  remainder: Nat,
280  total: Nat
281) -> Result<&1, &1, StreamError, Stream>:
282  stream.tail.result.sliced(compressed, complete,
283    Packed.slice(joined, U32.from_nat(full_length), U32.from_nat(remainder)),
284    total)
285def stream.result.sliced(
286  +compressed: S.State,
287  pair: Packed.Bytes & Packed.Bytes,
288  full_length: Nat,
289  remainder: Nat,
290  total: Nat
291) -> Result<&1, &1, StreamError, Stream>:
292  match pair:
293    case (retained, complete):
294      stream.tail.result(compressed, retained, complete, full_length,
295        remainder, total)
296
297def stream.result.lengths(
298  +compressed: S.State,
299  joined: Packed.Bytes,
300  lengths: Nat & Nat,
301  remainder: Nat,
302  total: Nat
303) -> Result<&1, &1, StreamError, Stream>:
304  match lengths:
305    case (for_slice, for_result):
306      stream.result.sliced(compressed,
307        Packed.slice(joined, 0, U32.from_nat(for_slice)), for_result,
308        remainder, total)
309def stream.result(
310  +compressed: S.State,
311  joined: Packed.Bytes,
312  tail_length: Nat & Nat,
313  total: Nat
314) -> Result<&1, &1, StreamError, Stream>:
315  match tail_length:
316    case (full_length, remainder):
317      stream.result.lengths(compressed, joined,
318        QueuePolicy.nat.clone.pair(full_length), remainder, total)
319def stream.joined.measured(
320  +compressed: S.State,
321  measured: Packed.Bytes & U32,
322  input_length: U32,
323  total: Nat
324) -> Result<&1, &1, StreamError, Stream>:
325  match measured:
326    case (joined, size):
327      +length = U32.to_nat(size)
328      +remainder = Nat.mod(length, 64n)
329      stream.result(compressed, joined,
330        (Nat.sub(length, remainder), remainder),
331        Nat.add(total, U32.to_nat(input_length)))
332def stream.joined(
333  +compressed: S.State,
334  tail: Packed.Bytes,
335  incoming: Packed.Bytes,
336  input_length: U32,
337  total: Nat
338) -> Result<&1, &1, StreamError, Stream>:
339  stream.joined.measured(compressed,
340    Packed.length(Packed.concat([tail, incoming])), input_length, total)
341
342def stream.update.checked(
343  +compressed: S.State,
344  tail: Packed.Bytes,
345  incoming: Packed.Bytes,
346  input_length: U32,
347  total: Nat,
348  valid: Bool
349) -> Result<&1, &1, StreamError, Stream>:
350  match valid:
351    case False{}: Fail{ResourceLimit{}}
352    case True{}:
353      stream.joined(compressed, tail, incoming, input_length, total)
354
355def stream.update.state.lengths(
356  +compressed: S.State,
357  tail: Packed.Bytes,
358  incoming: Packed.Bytes,
359  lengths: Nat & Nat,
360  totals: Nat & Nat
361) -> Result<&1, &1, StreamError, Stream>:
362  match lengths:
363    case (for_update, for_limit):
364      match totals:
365        case (for_update_total, for_limit_total):
366          stream.update.checked(compressed, tail, incoming,
367            U32.from_nat(for_update), for_update_total,
368            Nat.is_le(Nat.add(for_limit_total, for_limit), 4294967295n))
369
370def stream.update.state(
371  state: Stream,
372  input: Packed.Bytes & U32
373) -> Result<&1, &1, StreamError, Stream>:
374  match state:
375    case Stream{compressed, tail, +total}:
376      match input:
377        case (incoming, input_length):
378          stream.update.state.lengths(compressed, tail, incoming,
379            QueuePolicy.nat.clone.pair(U32.to_nat(input_length)),
380            QueuePolicy.nat.clone.pair(total))
381
382def stream.update(
383  state: Stream,
384  incoming: Packed.Bytes
385) -> Result<&1, &1, StreamError, Stream>:
386  stream.update.state(state, Packed.length(incoming))
387
388def stream.finish.words(state: Stream) -> List<&2, U32>:
389  match state:
390    case Stream{compressed, tail, total}:
391      match tail:
392        case Packed.Bytes{+len, buf}:
393          Core.digest(packed.final.tail(U32.from_nat(total), U32.to_nat(len),
394            Packed.Cursor.new(Packed.Bytes{len, buf}), compressed))
395
396def stream.finish(state: Stream) -> Packed.Bytes:
397  packed.digest.words(stream.finish.words(state),
398    (Packed.Cursor.new(Packed.Bytes{32, Packed.alloc(32)}), True{}))