1	import Base
2	import ../../../src/crypto/chacha/core.bend as C
3	import ../../../src/crypto/chacha/chacha20.bend as I
4	import ../../../spec/crypto/chacha.bend as R
5	import ./core.bend as K
6	import ./stream.bend as T
7	
8	# HChaCha20 and XChaCha20 against spec/crypto/chacha.bend: HChaCha20 for
9	# every number of double rounds, then at twenty rounds; XChaCha20 composed
10	# from HChaCha20 and the ChaCha20 stream.
11	
12	
13	def hout(+l: List<&2, U32>) -> List<&2, U32>:
14	  R.serialize([R.get(l, 0n), R.get(l, 1n), R.get(l, 2n), R.get(l, 3n), R.get(l, 12n), R.get(l, 13n), R.get(l, 14n), R.get(l, 15n)])
15	
16	law hbody_correct:
17	  for +r: Nat
18	  for +kb: List<&2, U32>
19	  for +nb: List<&2, U32>
20	  {I.hchacha_body(r, kb, nb) == R.hchacha_body(r, kb, nb) : List<&2, U32>}
21	
22	def hbody_correct(r, kb, nb):
23	  +H = I.hstate(I.key_words(I.words(kb)), I.words(nb))
24	  Equal.trans(List<&2, U32>, C.hbytes(C.rounds(r, H)), hout(K.vec(C.rounds(r, H))), R.hchacha_body(r, kb, nb),
25	    K.hbytes_correct(C.rounds(r, H)),
26	    Equal.trans(List<&2, U32>, hout(K.vec(C.rounds(r, H))), hout(R.inner_blocks(r, K.vec(H))), R.hchacha_body(r, kb, nb),
27	      Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(l), K.vec(C.rounds(r, H)), R.inner_blocks(r, K.vec(H)), K.rounds_correct(r, H)),
28	      Equal.trans(List<&2, U32>, hout(R.inner_blocks(r, K.vec(H))), hout(R.inner_blocks(r, R.hstate(I.words(kb), I.words(nb)))), R.hchacha_body(r, kb, nb),
29	        Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(R.inner_blocks(r, l)), K.vec(H), R.hstate(I.words(kb), I.words(nb)), T.hstate_eq(I.words(kb), I.words(nb))),
30	        Equal.trans(List<&2, U32>, hout(R.inner_blocks(r, R.hstate(I.words(kb), I.words(nb)))), hout(R.inner_blocks(r, R.hstate(R.words(kb), I.words(nb)))), R.hchacha_body(r, kb, nb),
31	          Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(R.inner_blocks(r, R.hstate(l, I.words(nb)))), I.words(kb), R.words(kb), T.words_eq(kb)),
32	          Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(R.inner_blocks(r, R.hstate(R.words(kb), l))), I.words(nb), R.words(nb), T.words_eq(nb))))))
33	
34	law hchacha_rounds_correct:
35	  for +r: Nat
36	  for +kb: List<&2, U32>
37	  for +nb: List<&2, U32>
38	  {I.hchacha_rounds(r, kb, nb) == R.hchacha_rounds(r, kb, nb) : List<&2, U32>}
39	
40	def hchacha_rounds_correct(r, kb, nb):
41	  match kb:
42	    case Nil{}: hbody_correct(r, Nil{}, nb)
43	    case b <> rest: hbody_correct(r, b <> rest, nb)
44	
45	law hchacha20_correct:
46	  for +kb: List<&2, U32>
47	  for +nb: List<&2, U32>
48	  {I.hchacha20_unchecked(kb, nb) == R.hchacha20(kb, nb) : List<&2, U32>}
49	
50	def hchacha20_correct(kb, nb):
51	  hchacha_rounds_correct(10n, kb, nb)
52	
53	law xencrypt_correct:
54	  for +kb: List<&2, U32>
55	  for +c: U32
56	  for +nb: List<&2, U32>
57	  for +pt: List<&2, U32>
58	  {I.xencrypt_unchecked(kb, c, nb, pt) == R.xencrypt(kb, c, nb, pt) : List<&2, U32>}
59	
60	def xenc(+kb: List<&2, U32>, +c: U32, +sub: List<&2, U32>, +nn: List<&2, U32>, +pt: List<&2, U32>) -> List<&2, U32>:
61	  R.encrypt_rounds(10n, sub, c, 0 <> 0 <> 0 <> 0 <> nn, pt)
62	
63	def xencrypt_correct(kb, c, nb, pt):
64	  +sub = I.hchacha20_unchecked(kb, I.take(16n, nb))
65	  Equal.trans(List<&2, U32>, I.encrypt_rounds(10n, sub, c, 0 <> 0 <> 0 <> 0 <> I.skip(16n, nb), pt), xenc(kb, c, sub, I.skip(16n, nb), pt), R.xencrypt(kb, c, nb, pt),
66	    T.encrypt_correct(10n, sub, c, 0 <> 0 <> 0 <> 0 <> I.skip(16n, nb), pt),
67	    Equal.trans(List<&2, U32>, xenc(kb, c, sub, I.skip(16n, nb), pt), xenc(kb, c, sub, R.suffix(16n, nb), pt), R.xencrypt(kb, c, nb, pt),
68	      Equal.cong(List<&2, U32>, List<&2, U32>, l => xenc(kb, c, sub, l, pt), I.skip(16n, nb), R.suffix(16n, nb), T.skip_eq(16n, nb)),
69	      Equal.trans(List<&2, U32>, xenc(kb, c, sub, R.suffix(16n, nb), pt), xenc(kb, c, R.hchacha20(kb, I.take(16n, nb)), R.suffix(16n, nb), pt), R.xencrypt(kb, c, nb, pt),
70	        Equal.cong(List<&2, U32>, List<&2, U32>, l => xenc(kb, c, l, R.suffix(16n, nb), pt), sub, R.hchacha20(kb, I.take(16n, nb)), hchacha20_correct(kb, I.take(16n, nb))),
71	        Equal.cong(List<&2, U32>, List<&2, U32>, l => xenc(kb, c, R.hchacha20(kb, l), R.suffix(16n, nb), pt), I.take(16n, nb), R.prefix(16n, nb), T.take_eq(16n, nb)))))