1	import Base
2	import ../../../../src/math/u64.bend as W
3	import ../../../../src/math/random/chacha8/block.bend as B
4	import ../../../../src/math/random/chacha8.bend as C8
5	import ../../../../spec/math/random/chacha8rand.bend as S
6	import ../../../../spec/math/random/source.bend as SRC
7	import ./block.bend as PB
8	
9	# The ChaCha8 generator of src/math/random/chacha8.bend produces C2SP's
10	# stream (spec/math/random/chacha8rand.bend) for every key: its state (key,
11	# next group, unread words of the current group) stands for the words left
12	# of the current iteration and the key of the next one.
13	
14	def app(xs: List<&2, W.U64>, ys: List<&2, W.U64>) -> List<&2, W.U64>:
15	  match xs:
16	    case Nil{}:
17	      ys
18	    case Con{x, rest}:
19	      Con{x, app(rest, ys)}
20	
21	def drop64(n: Nat, xs: List<&2, W.U64>) -> List<&2, W.U64>:
22	  match n xs:
23	    case 0n _:
24	      xs
25	    case 1n+p Nil{}:
26	      []
27	    case 1n+p Con{x, rest}:
28	      drop64(p, rest)
29	
30	# the outputs of the current iteration after the groups already produced
31	def rest(+kl: List<&2, U32>, p: C8.Phase) -> List<&2, W.U64>:
32	  match p:
33	    case C8.G0{}:
34	      []
35	    case C8.G1{}:
36	      drop64(32n, S.words64(S.output(kl)))
37	    case C8.G2{}:
38	      drop64(64n, S.words64(S.output(kl)))
39	    case C8.G3{}:
40	      drop64(96n, S.words64(S.output(kl)))
41	
42	# the key of the iteration after them
43	def nk(+kl: List<&2, U32>, p: C8.Phase) -> List<&2, U32>:
44	  match p:
45	    case C8.G0{}:
46	      kl
47	    case C8.G1{}:
48	      S.next_key(kl)
49	    case C8.G2{}:
50	      S.next_key(kl)
51	    case C8.G3{}:
52	      S.next_key(kl)
53	
54	def gw(+k: B.Key, +c: U32) -> List<&2, W.U64>:
55	  S.words64(S.group(S.key_list(k), c))
56	
57	# the invariant: from state C{k, p, buf} the generator outputs buf, the rest
58	# of the iteration keyed by k, then C2SP's stream from the next key
59	def inv(+n: Nat, +k: B.Key, +buf: List<&2, W.U64>, +p: C8.Phase) -> {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.C{k, p, buf}) == S.stream_go(n, app(buf, rest(S.key_list(k), p)), nk(S.key_list(k), p)) : List<&2, W.U64>}:
60	  match n:
61	    case 0n:
62	      {==}
63	    case 1n+m:
64	      match buf:
65	        case Con{x, t}:
66	          Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{x, l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, p, t}), S.stream_go(m, app(t, rest(S.key_list(k), p)), nk(S.key_list(k), p)), inv(m, k, t, p))
67	        case Nil{}:
68	          match p:
69	            case C8.G0{}:
70	              %Equal.sym(List<&2, W.U64>, B.group(k, 0), gw(k, 0), PB.group_correct(k, 0)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})))} == S.stream_go(1n+m, [], S.key_list(k)) : List<&2, W.U64>}
71	              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 0)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G1{}, S.tail(gw(k, 0))}), S.stream_go(m, app(S.tail(gw(k, 0)), rest(S.key_list(k), C8.G1{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 0)), C8.G1{}))
72	            case C8.G1{}:
73	              %Equal.sym(List<&2, W.U64>, B.group(k, 4), gw(k, 4), PB.group_correct(k, 4)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G1{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
74	              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 4)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G2{}, S.tail(gw(k, 4))}), S.stream_go(m, app(S.tail(gw(k, 4)), rest(S.key_list(k), C8.G2{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 4)), C8.G2{}))
75	            case C8.G2{}:
76	              %Equal.sym(List<&2, W.U64>, B.group(k, 8), gw(k, 8), PB.group_correct(k, 8)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G2{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
77	              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 8)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G3{}, S.tail(gw(k, 8))}), S.stream_go(m, app(S.tail(gw(k, 8)), rest(S.key_list(k), C8.G3{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 8)), C8.G3{}))
78	            case C8.G3{}:
79	              %Equal.sym(List<&2, W.U64>, B.group(k, 12), gw(k, 12), PB.group_correct(k, 12)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.last(_))), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.last(_))))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G3{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
80	              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 12)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), C8.G0{}, S.tail(List.take(&2, W.U64, gw(k, 12), 28n))}), S.stream_go(m, app(S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), []), S.key_list(C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)))), inv(m, C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), C8.G0{}))
81	
82	# THEOREM: the generator keyed by k outputs C2SP's ChaCha8Rand stream keyed
83	# by k's eight words, for every key and every number of outputs
84	def stream(+n: Nat, +k: B.Key) -> {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)) == S.stream(n, S.key_list(k)) : List<&2, W.U64>}:
85	  inv(n, k, [], C8.G0{})