src/crypto/blake/blake2b/sized.bend

bend-collections-laws-crypto@1.0.0.0 · 88 lines · 13 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend as B
4
5# BLAKE2b with a digest length nn in 1..64 bytes (RFC 7693 section 2.5: the
6# parameter block's first byte is nn), unkeyed, over a list of bytes (U32
7# values below 256). Argon2 (RFC 9106) uses it for H^T and H'. The blocks are
8# compressed by the proved BLAKE2b-512 implementation of blake2b.bend; only
9# the initial chaining value and the digest length differ.
10
11# Four little-endian bytes as one word.
12def word(+b0: U32, +b1: U32, +b2: U32, +b3: U32) -> U32:
13  U32.or(U32.or(b0, U32.shln(b1, 8n)), U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n)))
14
15# The bytes packed four per word, the last word zero-padded.
16def words(bs: List<&2, U32>) -> List<&2, U32>:
17  match bs:
18    case Nil{}:
19      Nil{}
20    case b0 <> Nil{}:
21      [word(b0, 0, 0, 0)]
22    case b0 <> b1 <> Nil{}:
23      [word(b0, b1, 0, 0)]
24    case b0 <> b1 <> b2 <> Nil{}:
25      [word(b0, b1, b2, 0)]
26    case b0 <> b1 <> b2 <> b3 <> rest:
27      word(b0, b1, b2, b3) <> words(rest)
28
29def fill(ws: List<&2, U32>, +i: U32, a: Array<U32>) -> Array<U32>:
30  match ws:
31    case Nil{}:
32      a
33    case w <> rest:
34      fill(rest, U32.inc(i), Array.set(U32, a, i, w))
35
36def pw(k: Nat) -> Nat:
37  match k:
38    case 0n:
39      1n
40    case 1n+p:
41      Nat.double(pw(p))
42
43# The smallest d >= k with 2^d >= n.
44def depth_go(fuel: Nat, +n: Nat, +d: Nat, done: Bool) -> Nat:
45  match fuel done:
46    case _ True{}:
47      d
48    case 0n False{}:
49      d
50    case 1n+f False{}:
51      depth_go(f, n, 1n+d, Nat.is_le(n, pw(1n+d)))
52
53def depth(+n: Nat) -> Nat:
54  depth_go(32n, n, 0n, Nat.is_le(n, 1n))
55
56# The packed array of the bytes.
57def pack(bs: List<&2, U32>) -> Array<U32>:
58  +ws = words(bs)
59  fill(ws, 0, Array.new(U32, depth(List.length(&2, U32, ws)), 0))
60
61# h[0] ^= 0x01010000 ^ nn: the parameter block of an unkeyed hash with nn bytes.
62def initial(+nn: U32) -> T.Chain:
63  T.H{T.W{U32.xor(4089235720, U32.or(16842752, nn)), 1779033703}, T.W{2227873595, 3144134277}, T.W{4271175723, 1013904242}, T.W{1595750129, 2773480762}, T.W{2917565137, 1359893119}, T.W{725511199, 2600822924}, T.W{4215389547, 528734635}, T.W{327033209, 1541459225}}
64
65def le(+w: U32) -> List<&2, U32>:
66  [U32.and(w, 255), U32.and(U32.shrn(w, 8n), 255), U32.and(U32.shrn(w, 16n), 255), U32.shrn(w, 24n)]
67
68def lane_bytes(l: T.Lane) -> List<&2, U32>:
69  match l:
70    case T.W{lo, hi}:
71      List.append(&2, U32, le(lo), le(hi))
72
73# The 64 little-endian bytes of the chaining value.
74def chain_bytes(h: T.Chain) -> List<&2, U32>:
75  match h:
76    case T.H{h0, h1, h2, h3, h4, h5, h6, h7}:
77      List.concat(&2, U32, [lane_bytes(h0), lane_bytes(h1), lane_bytes(h2), lane_bytes(h3), lane_bytes(h4), lane_bytes(h5), lane_bytes(h6), lane_bytes(h7)])
78
79# The chaining value after every block: dd - 1 = (ll - 1) div 128 full blocks,
80# then the last one (RFC 7693 section 3.3).
81def chain(+nn: Nat, a: Array<U32>, +ll: Nat) -> T.Chain:
82  +n = Nat.div(Nat.sub(ll, 1n), 128n)
83  B.blocks(n, 0, Nat.sub(ll, Nat.mul(n, 128n)), T.C{0, 0, 0, 0}, (a, initial(U32.from_nat(nn))))
84
85# BLAKE2b with an nn-byte digest (1 <= nn <= 64) of the bytes.
86def hash(+nn: Nat, +bs: List<&2, U32>) -> List<&2, U32>:
87  +ll = List.length(&2, U32, bs)
88  List.take(&2, U32, chain_bytes(chain(nn, pack(bs), ll)), nn)