1	import Base
2	import ../../../src/crypto/kdf.bend as KDF
3	import ../../../spec/crypto/hkdf.bend as Spec
4	
5	# The clauses of src/crypto/kdf.bend (HKDF-SHA256), proved in proof.bend.
6	# Every clause is for every salt, key material, info and length.
7	
8	# The specification's partial expand, as the implementation's result type.
9	def as_result(m: Maybe<&2, List<&2, U32>>) -> Result<&2, &2, KDF.KdfError, List<&2, U32>>:
10	  match m:
11	    case None{}:
12	      Fail{KDF.LengthTooLarge{}}
13	    case Some{okm}:
14	      Done{okm}
15	
16	# extract is RFC 5869 section 2.2 (HMAC-SHA256(salt, IKM)).
17	law Extract.correct:
18	  for +salt: List<&2, U32>
19	  for +ikm: List<&2, U32>
20	  {KDF.extract(salt, ikm) == Spec.extract(salt, ikm) : List<&2, U32>}
21	
22	# expand is RFC 5869 section 2.3, and fails exactly where it is undefined.
23	law Expand.correct:
24	  for +prk: List<&2, U32>
25	  for +info: List<&2, U32>
26	  for +len: Nat
27	  {KDF.expand(prk, info, len) == as_result(Spec.expand(prk, info, len)) : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
28	
29	law Expand.done:
30	  for +prk: List<&2, U32>
31	  for +info: List<&2, U32>
32	  for +len: Nat
33	  for +h: {Nat.is_le(len, 8160n) == True{} : Bool}
34	  {KDF.expand(prk, info, len) == Done{Spec.okm(prk, info, len)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
35	
36	law Expand.too_long:
37	  for +prk: List<&2, U32>
38	  for +info: List<&2, U32>
39	  for +len: Nat
40	  for +h: {Nat.is_le(len, 8160n) == False{} : Bool}
41	  {KDF.expand(prk, info, len) == Fail{KDF.LengthTooLarge{}} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
42	
43	# The output has the requested length.
44	law Expand.length:
45	  for +prk: List<&2, U32>
46	  for +info: List<&2, U32>
47	  for +len: Nat
48	  for +out: List<&2, U32>
49	  for +h: {KDF.expand(prk, info, len) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
50	  {List.length(&2, U32, out) == len : Nat}
51	
52	# A shorter output is a prefix of a longer one (same key and info).
53	law Expand.prefix:
54	  for +prk: List<&2, U32>
55	  for +info: List<&2, U32>
56	  for +a: Nat
57	  for +b: Nat
58	  for +out: List<&2, U32>
59	  for +hab: {Nat.is_le(a, b) == True{} : Bool}
60	  for +h: {KDF.expand(prk, info, b) == Done{out} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
61	  {KDF.expand(prk, info, a) == Done{List.take(&2, U32, out, a)} : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
62	
63	# hkdf is extract then expand.
64	law Hkdf.correct:
65	  for +salt: List<&2, U32>
66	  for +ikm: List<&2, U32>
67	  for +info: List<&2, U32>
68	  for +len: Nat
69	  {KDF.hkdf(salt, ikm, info, len) == as_result(Spec.hkdf(salt, ikm, info, len)) : Result<&2, &2, KDF.KdfError, List<&2, U32>>}
70	
71	# The specification's OKM (any length): L bytes, and prefixes of each other.
72	law Okm.length:
73	  for +prk: List<&2, U32>
74	  for +info: List<&2, U32>
75	  for +len: Nat
76	  {List.length(&2, U32, Spec.okm(prk, info, len)) == len : Nat}
77	
78	law Okm.prefix:
79	  for +prk: List<&2, U32>
80	  for +info: List<&2, U32>
81	  for +a: Nat
82	  for +b: Nat
83	  for +h: {Nat.is_le(a, b) == True{} : Bool}
84	  {Spec.okm(prk, info, a) == List.take(&2, U32, Spec.okm(prk, info, b), a) : List<&2, U32>}