1	import Base
2	import ./types.bend as T
3	import ./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.
12	def 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.
16	def 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	
29	def 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	
36	def 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.
44	def 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	
53	def depth(+n: Nat) -> Nat:
54	  depth_go(32n, n, 0n, Nat.is_le(n, 1n))
55	
56	# The packed array of the bytes.
57	def 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.
62	def 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	
65	def 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	
68	def 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.
74	def 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).
81	def 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.
86	def 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)