1	# Generated by tools/generators/chacha_gen.py; do not edit.
2	# The unrolled ChaCha core refines the list-based RFC 8439 specification.
3	#
4	# vec(s) is the RFC state list of a record state, one projection per entry,
5	# so that the list has its shape even when the state is abstract. One double
6	# round is compared with inner_block on a destructured state (both sides
7	# normalize to the same sixteen words); the round count is then an induction,
8	# so the theorems hold for every number of double rounds (ChaCha20, ChaCha8,
9	# ChaCha12 alike).
10	import Base
11	import ../../../src/crypto/chacha/core.bend as C
12	import ../../../spec/crypto/chacha.bend as R
13	
14	def p0(s: C.State) -> U32:
15	  match s:
16	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a0
17	
18	def p1(s: C.State) -> U32:
19	  match s:
20	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a1
21	
22	def p2(s: C.State) -> U32:
23	  match s:
24	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a2
25	
26	def p3(s: C.State) -> U32:
27	  match s:
28	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a3
29	
30	def p4(s: C.State) -> U32:
31	  match s:
32	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a4
33	
34	def p5(s: C.State) -> U32:
35	  match s:
36	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a5
37	
38	def p6(s: C.State) -> U32:
39	  match s:
40	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a6
41	
42	def p7(s: C.State) -> U32:
43	  match s:
44	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a7
45	
46	def p8(s: C.State) -> U32:
47	  match s:
48	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a8
49	
50	def p9(s: C.State) -> U32:
51	  match s:
52	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a9
53	
54	def p10(s: C.State) -> U32:
55	  match s:
56	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a10
57	
58	def p11(s: C.State) -> U32:
59	  match s:
60	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a11
61	
62	def p12(s: C.State) -> U32:
63	  match s:
64	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a12
65	
66	def p13(s: C.State) -> U32:
67	  match s:
68	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a13
69	
70	def p14(s: C.State) -> U32:
71	  match s:
72	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a14
73	
74	def p15(s: C.State) -> U32:
75	  match s:
76	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: a15
77	
78	def vec(+s: C.State) -> List<&2, U32>:
79	  [p0(s), p1(s), p2(s), p3(s), p4(s), p5(s), p6(s), p7(s), p8(s), p9(s), p10(s), p11(s), p12(s), p13(s), p14(s), p15(s)]
80	
81	law double_round_correct:
82	  for +s: C.State
83	  {vec(C.double_round(s)) == R.inner_block(vec(s)) : List<&2, U32>}
84	
85	def double_round_correct(s):
86	  match s:
87	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
88	
89	law rounds_correct:
90	  for +n: Nat
91	  for +s: C.State
92	  {vec(C.rounds(n, s)) == R.inner_blocks(n, vec(s)) : List<&2, U32>}
93	
94	def rounds_correct(n, s):
95	  match n:
96	    case 0n: {==}
97	    case 1n+p:
98	      Equal.trans(List<&2, U32>,
99	        vec(C.rounds(p, C.double_round(s))),
100	        R.inner_blocks(p, vec(C.double_round(s))),
101	        R.inner_blocks(p, R.inner_block(vec(s))),
102	        rounds_correct(p, C.double_round(s)),
103	        Equal.cong(List<&2, U32>, List<&2, U32>, l => R.inner_blocks(p, l), vec(C.double_round(s)), R.inner_block(vec(s)), double_round_correct(s)))
104	
105	law add_correct:
106	  for +a: C.State
107	  for +b: C.State
108	  {vec(C.add(a, b)) == R.add_words(vec(a), vec(b)) : List<&2, U32>}
109	
110	def add_correct(a, b):
111	  match a b:
112	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15} C.S{b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11,b12,b13,b14,b15}: {==}
113	
114	law bytes_correct:
115	  for +s: C.State
116	  {C.bytes(s) == R.serialize(vec(s)) : List<&2, U32>}
117	
118	def bytes_correct(s):
119	  match s:
120	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}
121	
122	# The block function with n double rounds, serialized, is the RFC's.
123	law block_correct:
124	  for +n: Nat
125	  for +s: C.State
126	  {C.bytes(C.block(n, s)) == R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))) : List<&2, U32>}
127	
128	def block_correct(n, s):
129	  Equal.trans(List<&2, U32>, C.bytes(C.block(n, s)), R.serialize(vec(C.add(s, C.rounds(n, s)))), R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))),
130	    bytes_correct(C.add(s, C.rounds(n, s))),
131	    Equal.trans(List<&2, U32>, R.serialize(vec(C.add(s, C.rounds(n, s)))), R.serialize(R.add_words(vec(s), vec(C.rounds(n, s)))), R.serialize(R.add_words(vec(s), R.inner_blocks(n, vec(s)))),
132	      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.serialize(l), vec(C.add(s, C.rounds(n, s))), R.add_words(vec(s), vec(C.rounds(n, s))), add_correct(s, C.rounds(n, s))),
133	      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.serialize(R.add_words(vec(s), l)), vec(C.rounds(n, s)), R.inner_blocks(n, vec(s)), rounds_correct(n, s))))
134	
135	law init_correct:
136	  for +k0: U32
137	  for +k1: U32
138	  for +k2: U32
139	  for +k3: U32
140	  for +k4: U32
141	  for +k5: U32
142	  for +k6: U32
143	  for +k7: U32
144	  for +c: U32
145	  for +n0: U32
146	  for +n1: U32
147	  for +n2: U32
148	  {vec(C.init(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2)) == R.state([k0, k1, k2, k3, k4, k5, k6, k7], c, [n0, n1, n2]) : List<&2, U32>}
149	
150	def init_correct(k0, k1, k2, k3, k4, k5, k6, k7, c, n0, n1, n2):
151	  {==}
152	
153	law hinit_correct:
154	  for +k0: U32
155	  for +k1: U32
156	  for +k2: U32
157	  for +k3: U32
158	  for +k4: U32
159	  for +k5: U32
160	  for +k6: U32
161	  for +k7: U32
162	  for +n0: U32
163	  for +n1: U32
164	  for +n2: U32
165	  for +n3: U32
166	  {vec(C.hinit(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3)) == R.hstate([k0, k1, k2, k3, k4, k5, k6, k7], [n0, n1, n2, n3]) : List<&2, U32>}
167	
168	def hinit_correct(k0, k1, k2, k3, k4, k5, k6, k7, n0, n1, n2, n3):
169	  {==}
170	
171	law hbytes_correct:
172	  for +s: C.State
173	  {C.hbytes(s) == R.serialize([R.get(vec(s), 0n), R.get(vec(s), 1n), R.get(vec(s), 2n), R.get(vec(s), 3n), R.get(vec(s), 12n), R.get(vec(s), 13n), R.get(vec(s), 14n), R.get(vec(s), 15n)]) : List<&2, U32>}
174	
175	def hbytes_correct(s):
176	  match s:
177	    case C.S{a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15}: {==}