1	import Base
2	import ../../../../src/math/u64.bend as W
3	import ../../../../src/math/random/chacha8.bend as C8
4	import ../../../../src/math/random/chacha8/block.bend as B
5	import ../../../../spec/math/random/chacha8rand.bend as S
6	import ../../../../spec/math/random.bend as SRM
7	import ./stream.bend as CS
8	import ../../../../spec/math/random/source.bend as SRC
9	
10	# A seed is 32 bytes below 256, read as eight little-endian words; any other
11	# list is rejected.
12	
13	def bytes_eq(+bs: List<&2, U32>) -> {C8.all_bytes(bs) == S.bytes_ok(bs) : Bool}:
14	  match bs:
15	    case Nil{}:
16	      {==}
17	    case Con{+b, +rest}:
18	      Equal.cong(Bool, Bool, z => Bool.and(U32.is_lt(b, 256), z), C8.all_bytes(rest), S.bytes_ok(rest), bytes_eq(rest))
19	
20	def seeded_ok(+n: Nat, +seed: List<&2, U32>) -> {SRM.map_outputs(n, C8.lift(C8.key_of(seed))) == SRM.map_stream(n, S.key_if(seed, Nat.is_eq(S.length(seed), 32n))) : Maybe<&2, List<&2, W.U64>>}:
21	  match seed:
22	    case Nil{}:
23	      {==}
24	    case Con{+a0, +r0}:
25	      match r0:
26	        case Nil{}:
27	          {==}
28	        case Con{+a1, +r1}:
29	          match r1:
30	            case Nil{}:
31	              {==}
32	            case Con{+a2, +r2}:
33	              match r2:
34	                case Nil{}:
35	                  {==}
36	                case Con{+a3, +r3}:
37	                  match r3:
38	                    case Nil{}:
39	                      {==}
40	                    case Con{+b0, +r4}:
41	                      match r4:
42	                        case Nil{}:
43	                          {==}
44	                        case Con{+b1, +r5}:
45	                          match r5:
46	                            case Nil{}:
47	                              {==}
48	                            case Con{+b2, +r6}:
49	                              match r6:
50	                                case Nil{}:
51	                                  {==}
52	                                case Con{+b3, +r7}:
53	                                  match r7:
54	                                    case Nil{}:
55	                                      {==}
56	                                    case Con{+c0, +r8}:
57	                                      match r8:
58	                                        case Nil{}:
59	                                          {==}
60	                                        case Con{+c1, +r9}:
61	                                          match r9:
62	                                            case Nil{}:
63	                                              {==}
64	                                            case Con{+c2, +r10}:
65	                                              match r10:
66	                                                case Nil{}:
67	                                                  {==}
68	                                                case Con{+c3, +r11}:
69	                                                  match r11:
70	                                                    case Nil{}:
71	                                                      {==}
72	                                                    case Con{+d0, +r12}:
73	                                                      match r12:
74	                                                        case Nil{}:
75	                                                          {==}
76	                                                        case Con{+d1, +r13}:
77	                                                          match r13:
78	                                                            case Nil{}:
79	                                                              {==}
80	                                                            case Con{+d2, +r14}:
81	                                                              match r14:
82	                                                                case Nil{}:
83	                                                                  {==}
84	                                                                case Con{+d3, +r15}:
85	                                                                  match r15:
86	                                                                    case Nil{}:
87	                                                                      {==}
88	                                                                    case Con{+e0, +r16}:
89	                                                                      match r16:
90	                                                                        case Nil{}:
91	                                                                          {==}
92	                                                                        case Con{+e1, +r17}:
93	                                                                          match r17:
94	                                                                            case Nil{}:
95	                                                                              {==}
96	                                                                            case Con{+e2, +r18}:
97	                                                                              match r18:
98	                                                                                case Nil{}:
99	                                                                                  {==}
100	                                                                                case Con{+e3, +r19}:
101	                                                                                  match r19:
102	                                                                                    case Nil{}:
103	                                                                                      {==}
104	                                                                                    case Con{+f0, +r20}:
105	                                                                                      match r20:
106	                                                                                        case Nil{}:
107	                                                                                          {==}
108	                                                                                        case Con{+f1, +r21}:
109	                                                                                          match r21:
110	                                                                                            case Nil{}:
111	                                                                                              {==}
112	                                                                                            case Con{+f2, +r22}:
113	                                                                                              match r22:
114	                                                                                                case Nil{}:
115	                                                                                                  {==}
116	                                                                                                case Con{+f3, +r23}:
117	                                                                                                  match r23:
118	                                                                                                    case Nil{}:
119	                                                                                                      {==}
120	                                                                                                    case Con{+g0, +r24}:
121	                                                                                                      match r24:
122	                                                                                                        case Nil{}:
123	                                                                                                          {==}
124	                                                                                                        case Con{+g1, +r25}:
125	                                                                                                          match r25:
126	                                                                                                            case Nil{}:
127	                                                                                                              {==}
128	                                                                                                            case Con{+g2, +r26}:
129	                                                                                                              match r26:
130	                                                                                                                case Nil{}:
131	                                                                                                                  {==}
132	                                                                                                                case Con{+g3, +r27}:
133	                                                                                                                  match r27:
134	                                                                                                                    case Nil{}:
135	                                                                                                                      {==}
136	                                                                                                                    case Con{+h0, +r28}:
137	                                                                                                                      match r28:
138	                                                                                                                        case Nil{}:
139	                                                                                                                          {==}
140	                                                                                                                        case Con{+h1, +r29}:
141	                                                                                                                          match r29:
142	                                                                                                                            case Nil{}:
143	                                                                                                                              {==}
144	                                                                                                                            case Con{+h2, +r30}:
145	                                                                                                                              match r30:
146	                                                                                                                                case Nil{}:
147	                                                                                                                                  {==}
148	                                                                                                                                case Con{+h3, +r31}:
149	                                                                                                                                  match r31:
150	                                                                                                                                    case Nil{}:
151	                                                                                                                                      +k = {B.K{C8.le32(a0, a1, a2, a3), C8.le32(b0, b1, b2, b3), C8.le32(c0, c1, c2, c3), C8.le32(d0, d1, d2, d3), C8.le32(e0, e1, e2, e3), C8.le32(f0, f1, f2, f3), C8.le32(g0, g1, g2, g3), C8.le32(h0, h1, h2, h3)} : B.Key}
152	                                                                                                                                      Equal.cong(List<&2, W.U64>, Maybe<&2, List<&2, W.U64>>, l => Some{l}, SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)), S.stream(n, S.key_list(k)), CS.stream(n, k))
153	                                                                                                                                    case Con{x, rr}:
154	                                                                                                                                      {==}
155	
156	def seeded_c(+n: Nat, +seed: List<&2, U32>, +b: Bool) -> {SRM.map_outputs(n, C8.seed_ok(seed, b)) == SRM.map_stream(n, S.key_if(seed, Bool.and(b, Nat.is_eq(S.length(seed), 32n)))) : Maybe<&2, List<&2, W.U64>>}:
157	  match b:
158	    case False{}:
159	      {==}
160	    case True{}:
161	      seeded_ok(n, seed)
162	
163	# THEOREM (ChaCha8.seeded)
164	def seeded(+n: Nat, +seed: List<&2, U32>) -> SRM.ChaCha8.seeded(n, seed):
165	  %Equal.sym(Bool, C8.all_bytes(seed), S.bytes_ok(seed), bytes_eq(seed)) : {SRM.map_outputs(n, C8.seed_ok(seed, _)) == SRM.map_stream(n, S.key_if(seed, Bool.and(S.bytes_ok(seed), Nat.is_eq(S.length(seed), 32n)))) : Maybe<&2, List<&2, W.U64>>}
166	  seeded_c(n, seed, S.bytes_ok(seed))