1	import Base
2	import ./sha.bend as FIPS
3	
4	# Executable specification of HMAC-SHA256: RFC 2104 section 2, in the
5	# step-by-step form of FIPS 198-1 section 4, over the FIPS 180-4 SHA-256
6	# specification spec/crypto/sha.bend (after HACL*'s Spec.HMAC). Nothing of
7	# the implementation (src/crypto/mac.bend) or of the SHA-256 implementation
8	# is used. Bytes are U32 values 0..255, as everywhere in the library.
9	
10	# B, the block size of SHA-256 in bytes, and L, its output size.
11	def block_len() -> Nat:
12	  64n
13	
14	def hash_len() -> Nat:
15	  32n
16	
17	# RFC 2104: ipad = the byte 0x36 repeated B times, opad = 0x5C repeated B times.
18	def ipad() -> U32:
19	  54
20	
21	def opad() -> U32:
22	  92
23	
24	def hash(bytes: List<&2, U32>) -> List<&2, U32>:
25	  FIPS.sha256_bytes(bytes)
26	
27	# FIPS 198-1 steps 1-3: a key of exactly B bytes is K0 itself; a longer key
28	# is hashed first (K0 = H(K) || zeros); a shorter one is zero-padded to B.
29	def shorten_if(+key: List<&2, U32>, fits: Bool) -> List<&2, U32>:
30	  match fits:
31	    case True{}:
32	      key
33	    case False{}:
34	      hash(key)
35	
36	def shorten(+key: List<&2, U32>) -> List<&2, U32>:
37	  shorten_if(key, Nat.is_le(List.length(&2, U32, key), block_len()))
38	
39	def zero_pad(+k: List<&2, U32>) -> List<&2, U32>:
40	  List.append(&2, U32, k,
41	    List.replicate(U32, Nat.sub(block_len(), List.length(&2, U32, k)), 0))
42	
43	def k0(+key: List<&2, U32>) -> List<&2, U32>:
44	  zero_pad(shorten(key))
45	
46	# Byte-wise exclusive or of K0 with a pad byte (steps 4 and 7).
47	def xor_pad(ks: List<&2, U32>, +pad: U32) -> List<&2, U32>:
48	  match ks:
49	    case Nil{}:
50	      Nil{}
51	    case k <> rest:
52	      U32.xor(k, pad) <> xor_pad(rest, pad)
53	
54	# HMAC(K, text) = H((K0 ^ opad) || H((K0 ^ ipad) || text))   (steps 4-9).
55	def hmac(+key: List<&2, U32>, text: List<&2, U32>) -> List<&2, U32>:
56	  +k = k0(key)
57	  hash(List.append(&2, U32, xor_pad(k, opad()),
58	    hash(List.append(&2, U32, xor_pad(k, ipad()), text))))