1	import Base
2	import ./hmac.bend as HMAC
3	
4	# Executable specification of HKDF-SHA256, RFC 5869 section 2, over the
5	# HMAC specification spec/crypto/hmac.bend (after HACL*'s Spec.HKDF).
6	# Nothing of the implementation (src/crypto/kdf.bend) is used.
7	
8	def hash_len() -> Nat:
9	  32n
10	
11	# RFC 5869: L <= 255*HashLen.
12	def max_length() -> Nat:
13	  8160n
14	
15	# 2.2 Step 1: Extract. PRK = HMAC-Hash(salt, IKM). An absent salt is HashLen
16	# zero bytes; an empty salt gives the same HMAC key block (both are padded
17	# with zeros to the block size), so passing [] means "not provided".
18	def extract(+salt: List<&2, U32>, ikm: List<&2, U32>) -> List<&2, U32>:
19	  HMAC.hmac(salt, ikm)
20	
21	# 2.3 Step 2: Expand. T(0) = empty string; for i = 1..N,
22	#   T(i) = HMAC-Hash(PRK, T(i-1) | info | the octet i).
23	# t_blocks(n, prk, info, T(i), i) is T(i+1) | ... | T(i+n).
24	def t_blocks(n: Nat, +prk: List<&2, U32>, +info: List<&2, U32>, prev: List<&2, U32>, +i: Nat) -> List<&2, U32>:
25	  match n:
26	    case 0n:
27	      Nil{}
28	    case 1n+p:
29	      +t = HMAC.hmac(prk, List.append(&2, U32, prev,
30	        List.append(&2, U32, info, [U32.from_nat(1n+i)])))
31	      List.append(&2, U32, t, t_blocks(p, prk, info, t, 1n+i))
32	
33	# N = ceil(L/HashLen).
34	def block_count(+len: Nat) -> Nat:
35	  Nat.div(Nat.add(len, 31n), hash_len())
36	
37	# OKM = the first L octets of T = T(1) | T(2) | ... | T(N).
38	def okm(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> List<&2, U32>:
39	  List.take(&2, U32, t_blocks(block_count(len), prk, info, Nil{}, 0n), len)
40	
41	# Expand is defined for L <= 255*HashLen only.
42	def expand_if(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat, ok: Bool) -> Maybe<&2, List<&2, U32>>:
43	  match ok:
44	    case True{}:
45	      Some{okm(prk, info, len)}
46	    case False{}:
47	      None{}
48	
49	def expand(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> Maybe<&2, List<&2, U32>>:
50	  expand_if(prk, info, len, Nat.is_le(len, max_length()))
51	
52	def hkdf(+salt: List<&2, U32>, ikm: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> Maybe<&2, List<&2, U32>>:
53	  expand(extract(salt, ikm), info, len)