1	import Base
2	import ../../../../src/math/u64.bend as W
3	import ../../../../src/math/random/chacha8/block.bend as B
4	import ../../../../spec/math/random/chacha8rand.bend as S
5	import ./rounds.bend as R
6	
7	# The ChaCha8Rand block and group of src/math/random/chacha8/block.bend are
8	# C2SP's (spec/math/random/chacha8rand.bend) for every key and counter.
9	
10	# n double rounds, the model of the implementation's dr(dr(dr(dr(x))))
11	def drs(n: Nat, v: B.Vector) -> B.Vector:
12	  match n:
13	    case 0n:
14	      v
15	    case 1n+p:
16	      drs(p, B.dr(v))
17	
18	def drs_correct(+n: Nat, +v: B.Vector) -> {R.vec(drs(n, v)) == S.double_rounds(n, R.vec(v)) : List<&2, U32>}:
19	  match n:
20	    case 0n:
21	      {==}
22	    case 1n+p:
23	      Equal.trans(List<&2, U32>, R.vec(drs(p, B.dr(v))), S.double_rounds(p, R.vec(B.dr(v))), S.double_rounds(p, S.double_round(R.vec(v))),
24	        drs_correct(p, B.dr(v)),
25	        Equal.cong(List<&2, U32>, List<&2, U32>, x => S.double_rounds(p, x), R.vec(B.dr(v)), S.double_round(R.vec(v)), R.dr_correct(v)))
26	
27	# the eight rounds on the initial state
28	def rounds_correct(+k: B.Key, +ctr: U32) -> {R.vec(B.dr(B.dr(B.dr(B.dr(B.init(k, ctr)))))) == S.double_rounds(4n, S.initial(S.key_list(k), ctr)) : List<&2, U32>}:
29	  Equal.trans(List<&2, U32>, R.vec(drs(4n, B.init(k, ctr))), S.double_rounds(4n, R.vec(B.init(k, ctr))), S.double_rounds(4n, S.initial(S.key_list(k), ctr)),
30	    drs_correct(4n, B.init(k, ctr)),
31	    Equal.cong(List<&2, U32>, List<&2, U32>, x => S.double_rounds(4n, x), R.vec(B.init(k, ctr)), S.initial(S.key_list(k), ctr), R.init_correct(k, ctr)))
32	
33	# THEOREM: the implementation's block is C2SP's block ctr
34	def block_correct(+k: B.Key, +ctr: U32) -> {R.vec(B.block(k, ctr)) == S.c2sp_block(S.key_list(k), ctr) : List<&2, U32>}:
35	  +v = B.dr(B.dr(B.dr(B.dr(B.init(k, ctr)))))
36	  Equal.trans(List<&2, U32>, R.vec(B.finish(k, v)), S.subtract(S.add_words(R.vec(v), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), S.initial(S.key_list(k), ctr)), ctr),
37	    R.finish_correct(k, v, ctr),
38	    Equal.trans(List<&2, U32>, S.subtract(S.add_words(R.vec(v), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), R.vec(B.init(k, ctr))), ctr), S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), S.initial(S.key_list(k), ctr)), ctr),
39	      Equal.cong(List<&2, U32>, List<&2, U32>, x => S.subtract(S.add_words(x, R.vec(B.init(k, ctr))), ctr), R.vec(v), S.double_rounds(4n, S.initial(S.key_list(k), ctr)), rounds_correct(k, ctr)),
40	      Equal.cong(List<&2, U32>, List<&2, U32>, x => S.subtract(S.add_words(S.double_rounds(4n, S.initial(S.key_list(k), ctr)), x), ctr), R.vec(B.init(k, ctr)), S.initial(S.key_list(k), ctr), R.init_correct(k, ctr))))
41	
42	# THEOREM: the implementation's group is C2SP's four permuted blocks ctr ..
43	# ctr + 3, read as little-endian 64-bit words
44	def group_correct(+k: B.Key, +ctr: U32) -> {B.group(k, ctr) == S.words64(S.group(S.key_list(k), ctr)) : List<&2, W.U64>}:
45	  +b0 = B.block(k, ctr)
46	  +b1 = B.block(k, U32.add(ctr, 1))
47	  +b2 = B.block(k, U32.add(ctr, 2))
48	  +b3 = B.block(k, U32.add(ctr, 3))
49	  +kl = S.key_list(k)
50	  %block_correct(k, ctr) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, _, S.c2sp_block(kl, U32.add(ctr, 1)), S.c2sp_block(kl, U32.add(ctr, 2)), S.c2sp_block(kl, U32.add(ctr, 3)))) : List<&2, W.U64>}
51	  %block_correct(k, U32.add(ctr, 1)) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, R.vec(b0), _, S.c2sp_block(kl, U32.add(ctr, 2)), S.c2sp_block(kl, U32.add(ctr, 3)))) : List<&2, W.U64>}
52	  %block_correct(k, U32.add(ctr, 2)) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, R.vec(b0), R.vec(b1), _, S.c2sp_block(kl, U32.add(ctr, 3)))) : List<&2, W.U64>}
53	  %block_correct(k, U32.add(ctr, 3)) : {B.group(k, ctr) == S.words64(S.interleave(16n, 0n, R.vec(b0), R.vec(b1), R.vec(b2), _)) : List<&2, W.U64>}
54	  R.interleave_correct(b0, b1, b2, b3)