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 ../../lib/nat.bend as N
6	import ./core.bend as K
7	
8	# The byte-level ChaCha20 / HChaCha20 / XChaCha20 of src/crypto/chacha/
9	# against spec/crypto/chacha.bend, for every key, nonce, counter and byte
10	# list, and every number of double rounds.
11	
12	# ---------------------------------------------------------------- bytes to words
13	
14	law words_eq:
15	  for +xs: List<&2, U32>
16	  {I.words(xs) == R.words(xs) : List<&2, U32>}
17	
18	def words_eq(xs):
19	  match xs:
20	    case Nil{}: {==}
21	    case b0 <> Nil{}: {==}
22	    case b0 <> b1 <> Nil{}: {==}
23	    case b0 <> b1 <> b2 <> Nil{}: {==}
24	    case b0 <> b1 <> b2 <> b3 <> rest:
25	      %Equal.sym(List<&2, U32>, I.words(rest), R.words(rest), words_eq(rest)) :
26	        {I.word(b0, b1, b2, b3) <> _ == R.word(b0, b1, b2, b3) <> R.words(rest) : List<&2, U32>}
27	      {==}
28	
29	law key_eq:
30	  for +ws: List<&2, U32>
31	  {I.key_words(ws) == I.K{R.get(ws, 0n), R.get(ws, 1n), R.get(ws, 2n), R.get(ws, 3n), R.get(ws, 4n), R.get(ws, 5n), R.get(ws, 6n), R.get(ws, 7n)} : I.Key}
32	
33	def key_eq(ws):
34	  match ws:
35	    case Nil{}: {==}
36	    case w0 <> Nil{}: {==}
37	    case w0 <> w1 <> Nil{}: {==}
38	    case w0 <> w1 <> w2 <> Nil{}: {==}
39	    case w0 <> w1 <> w2 <> w3 <> Nil{}: {==}
40	    case w0 <> w1 <> w2 <> w3 <> w4 <> Nil{}: {==}
41	    case w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> Nil{}: {==}
42	    case w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> w6 <> Nil{}: {==}
43	    case w0 <> w1 <> w2 <> w3 <> w4 <> w5 <> w6 <> w7 <> rest: {==}
44	
45	law nonce_eq:
46	  for +ws: List<&2, U32>
47	  {I.nonce_words(ws) == I.N{R.get(ws, 0n), R.get(ws, 1n), R.get(ws, 2n)} : I.Nonce}
48	
49	def nonce_eq(ws):
50	  match ws:
51	    case Nil{}: {==}
52	    case w0 <> Nil{}: {==}
53	    case w0 <> w1 <> Nil{}: {==}
54	    case w0 <> w1 <> w2 <> rest: {==}
55	
56	# The four HChaCha20 nonce words.
57	law hnonce_eq:
58	  for +ws: List<&2, U32>
59	  {[I.at(ws, 0n), I.at(ws, 1n), I.at(ws, 2n), I.at(ws, 3n)] == [R.get(ws, 0n), R.get(ws, 1n), R.get(ws, 2n), R.get(ws, 3n)] : List<&2, U32>}
60	
61	def hnonce_eq(ws):
62	  match ws:
63	    case Nil{}: {==}
64	    case w0 <> Nil{}: {==}
65	    case w0 <> w1 <> Nil{}: {==}
66	    case w0 <> w1 <> w2 <> Nil{}: {==}
67	    case w0 <> w1 <> w2 <> w3 <> rest: {==}
68	
69	# ---------------------------------------------------------------- states
70	
71	law state_eq:
72	  for +ks: List<&2, U32>
73	  for +c: U32
74	  for +ns: List<&2, U32>
75	  {K.vec(I.state(I.key_words(ks), c, I.nonce_words(ns))) == R.state(ks, c, ns) : List<&2, U32>}
76	
77	def state_eq(ks, c, ns):
78	  %Equal.sym(I.Key, I.key_words(ks), I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, key_eq(ks)) :
79	    {K.vec(I.state(_, c, I.nonce_words(ns))) == R.state(ks, c, ns) : List<&2, U32>}
80	  %Equal.sym(I.Nonce, I.nonce_words(ns), I.N{R.get(ns, 0n), R.get(ns, 1n), R.get(ns, 2n)}, nonce_eq(ns)) :
81	    {K.vec(I.state(I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, c, _)) == R.state(ks, c, ns) : List<&2, U32>}
82	  {==}
83	
84	law hstate_eq:
85	  for +ks: List<&2, U32>
86	  for +ns: List<&2, U32>
87	  {K.vec(I.hstate(I.key_words(ks), ns)) == R.hstate(ks, ns) : List<&2, U32>}
88	
89	def hsl(+k0: U32, +k1: U32, +k2: U32, +k3: U32, +k4: U32, +k5: U32, +k6: U32, +k7: U32, l: List<&2, U32>) -> List<&2, U32>:
90	  match l:
91	    case n0 <> n1 <> n2 <> n3 <> rest: R.hstate([k0, k1, k2, k3, k4, k5, k6, k7], [n0, n1, n2, n3])
92	    case _: Nil{}
93	
94	def hstate_eq(ks, ns):
95	  %Equal.sym(I.Key, I.key_words(ks), I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, key_eq(ks)) :
96	    {K.vec(I.hstate(_, ns)) == R.hstate(ks, ns) : List<&2, U32>}
97	  Equal.trans(List<&2, U32>,
98	    K.vec(I.hstate(I.K{R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n)}, ns)),
99	    hsl(R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n), [I.at(ns, 0n), I.at(ns, 1n), I.at(ns, 2n), I.at(ns, 3n)]),
100	    R.hstate(ks, ns),
101	    {==},
102	    Equal.cong(List<&2, U32>, List<&2, U32>, l => hsl(R.get(ks, 0n), R.get(ks, 1n), R.get(ks, 2n), R.get(ks, 3n), R.get(ks, 4n), R.get(ks, 5n), R.get(ks, 6n), R.get(ks, 7n), l),
103	      [I.at(ns, 0n), I.at(ns, 1n), I.at(ns, 2n), I.at(ns, 3n)], [R.get(ns, 0n), R.get(ns, 1n), R.get(ns, 2n), R.get(ns, 3n)], hnonce_eq(ns)))
104	
105	# ---------------------------------------------------------------- block
106	
107	law body_correct:
108	  for +r: Nat
109	  for +kb: List<&2, U32>
110	  for +c: U32
111	  for +nb: List<&2, U32>
112	  {I.keystream(r, I.key(kb), c, I.nonce(nb)) == R.block_body(r, kb, c, nb) : List<&2, U32>}
113	
114	def sblock(+r: Nat, +s: List<&2, U32>) -> List<&2, U32>:
115	  R.serialize(R.add_words(s, R.inner_blocks(r, s)))
116	
117	def body_correct(r, kb, c, nb):
118	  +S = I.state(I.key_words(I.words(kb)), c, I.nonce_words(I.words(nb)))
119	  Equal.trans(List<&2, U32>, C.bytes(C.block(r, S)), sblock(r, K.vec(S)), R.block_body(r, kb, c, nb),
120	    K.block_correct(r, S),
121	    Equal.trans(List<&2, U32>, sblock(r, K.vec(S)), sblock(r, R.state(I.words(kb), c, I.words(nb))), R.block_body(r, kb, c, nb),
122	      Equal.cong(List<&2, U32>, List<&2, U32>, l => sblock(r, l), K.vec(S), R.state(I.words(kb), c, I.words(nb)), state_eq(I.words(kb), c, I.words(nb))),
123	      Equal.trans(List<&2, U32>, sblock(r, R.state(I.words(kb), c, I.words(nb))), sblock(r, R.state(R.words(kb), c, I.words(nb))), R.block_body(r, kb, c, nb),
124	        Equal.cong(List<&2, U32>, List<&2, U32>, l => sblock(r, R.state(l, c, I.words(nb))), I.words(kb), R.words(kb), words_eq(kb)),
125	        Equal.cong(List<&2, U32>, List<&2, U32>, l => sblock(r, R.state(R.words(kb), c, l)), I.words(nb), R.words(nb), words_eq(nb)))))
126	
127	law keystream_correct:
128	  for +r: Nat
129	  for +kb: List<&2, U32>
130	  for +c: U32
131	  for +nb: List<&2, U32>
132	  {I.keystream(r, I.key(kb), c, I.nonce(nb)) == R.block_rounds(r, kb, c, nb) : List<&2, U32>}
133	
134	def keystream_correct(r, kb, c, nb):
135	  match kb:
136	    case Nil{}: body_correct(r, Nil{}, c, nb)
137	    case b <> rest: body_correct(r, b <> rest, c, nb)
138	
139	law block_rounds_correct:
140	  for +r: Nat
141	  for +kb: List<&2, U32>
142	  for +c: U32
143	  for +nb: List<&2, U32>
144	  {I.block_rounds(r, kb, c, nb) == R.block_rounds(r, kb, c, nb) : List<&2, U32>}
145	
146	def block_rounds_correct(r, kb, c, nb):
147	  match kb:
148	    case Nil{}: body_correct(r, Nil{}, c, nb)
149	    case b <> rest: body_correct(r, b <> rest, c, nb)
150	
151	# 64 keystream bytes.
152	law bytes_length:
153	  for +s: C.State
154	  {List.length(&2, U32, C.bytes(s)) == 64n : Nat}
155	
156	def bytes_length(s):
157	  match s:
158	    case C.S{a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15}: {==}
159	
160	law block_length:
161	  for +r: Nat
162	  for +kb: List<&2, U32>
163	  for +c: U32
164	  for +nb: List<&2, U32>
165	  {List.length(&2, U32, R.block_rounds(r, kb, c, nb)) == 64n : Nat}
166	
167	def block_length(r, kb, c, nb):
168	  %keystream_correct(r, kb, c, nb) : {List.length(&2, U32, _) == 64n : Nat}
169	  bytes_length(C.block(r, I.state(I.key(kb), c, I.nonce(nb))))
170	
171	# ---------------------------------------------------------------- stream
172	
173	law xor_front_eq:
174	  for +ks: List<&2, U32>
175	  for +xs: List<&2, U32>
176	  {I.xor_front(ks, xs) == R.xor_bytes(R.prefix(List.length(&2, U32, ks), xs), ks) : List<&2, U32>}
177	
178	def xor_front_eq(ks, xs):
179	  match ks xs:
180	    case Nil{} _: {==}
181	    case k <> kt Nil{}: {==}
182	    case k <> kt x <> xt:
183	      %Equal.sym(List<&2, U32>, I.xor_front(kt, xt), R.xor_bytes(R.prefix(List.length(&2, U32, kt), xt), kt), xor_front_eq(kt, xt)) :
184	        {U32.xor(x, k) <> _ == U32.xor(x, k) <> R.xor_bytes(R.prefix(List.length(&2, U32, kt), xt), kt) : List<&2, U32>}
185	      {==}
186	
187	law skip_eq:
188	  for +n: Nat
189	  for +xs: List<&2, U32>
190	  {I.skip(n, xs) == R.suffix(n, xs) : List<&2, U32>}
191	
192	def skip_eq(n, xs):
193	  match n xs:
194	    case 0n _: {==}
195	    case 1n+p Nil{}: {==}
196	    case 1n+p x <> rest: skip_eq(p, rest)
197	
198	law take_eq:
199	  for +n: Nat
200	  for +xs: List<&2, U32>
201	  {I.take(n, xs) == R.prefix(n, xs) : List<&2, U32>}
202	
203	def take_eq(n, xs):
204	  match n xs:
205	    case 0n _: {==}
206	    case 1n+p Nil{}: {==}
207	    case 1n+p x <> rest:
208	      %Equal.sym(List<&2, U32>, I.take(p, rest), R.prefix(p, rest), take_eq(p, rest)) : {x <> _ == x <> R.prefix(p, rest) : List<&2, U32>}
209	      {==}
210	
211	# One block of the stream: the XORed front is the spec's.
212	law front_correct:
213	  for +r: Nat
214	  for +kb: List<&2, U32>
215	  for +c: U32
216	  for +nb: List<&2, U32>
217	  for +xs: List<&2, U32>
218	  {I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), xs) == R.xor_bytes(R.prefix(64n, xs), R.block_rounds(r, kb, c, nb)) : List<&2, U32>}
219	
220	def front_correct(r, kb, c, nb, xs):
221	  +ks = I.keystream(r, I.key(kb), c, I.nonce(nb))
222	  Equal.trans(List<&2, U32>, I.xor_front(ks, xs), R.xor_bytes(R.prefix(List.length(&2, U32, ks), xs), ks), R.xor_bytes(R.prefix(64n, xs), R.block_rounds(r, kb, c, nb)),
223	    xor_front_eq(ks, xs),
224	    Equal.trans(List<&2, U32>, R.xor_bytes(R.prefix(List.length(&2, U32, ks), xs), ks), R.xor_bytes(R.prefix(64n, xs), ks), R.xor_bytes(R.prefix(64n, xs), R.block_rounds(r, kb, c, nb)),
225	      Equal.cong(Nat, List<&2, U32>, n => R.xor_bytes(R.prefix(n, xs), ks), List.length(&2, U32, ks), 64n, bytes_length(C.block(r, I.state(I.key(kb), c, I.nonce(nb))))),
226	      Equal.cong(List<&2, U32>, List<&2, U32>, l => R.xor_bytes(R.prefix(64n, xs), l), ks, R.block_rounds(r, kb, c, nb), keystream_correct(r, kb, c, nb))))
227	
228	law stream_correct:
229	  for +fuel: Nat
230	  for +xs: List<&2, U32>
231	  for +r: Nat
232	  for +kb: List<&2, U32>
233	  for +c: U32
234	  for +nb: List<&2, U32>
235	  {I.stream(fuel, xs, r, I.key(kb), c, I.nonce(nb)) == R.encrypt_blocks(R.blocks(fuel, xs), r, kb, c, nb) : List<&2, U32>}
236	
237	def stream_correct(fuel, xs, r, kb, c, nb):
238	  match fuel xs:
239	    case 0n _: {==}
240	    case 1n+p Nil{}: {==}
241	    case 1n+p x <> xt:
242	      +c1 = U32.add(c, 1)
243	      +ih = stream_correct(p, R.suffix(64n, x <> xt), r, kb, c1, nb)
244	      +fr = front_correct(r, kb, c, nb, x <> xt)
245	      +sk = skip_eq(64n, x <> xt)
246	      %Equal.sym(List<&2, U32>, I.skip(64n, x <> xt), R.suffix(64n, x <> xt), sk) :
247	        {List.append(&2, U32, I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), x <> xt), I.stream(p, _, r, I.key(kb), c1, I.nonce(nb))) == R.encrypt_blocks(R.blocks(1n+p, x <> xt), r, kb, c, nb) : List<&2, U32>}
248	      %Equal.sym(List<&2, U32>, I.stream(p, R.suffix(64n, x <> xt), r, I.key(kb), c1, I.nonce(nb)), R.encrypt_blocks(R.blocks(p, R.suffix(64n, x <> xt)), r, kb, c1, nb), ih) :
249	        {List.append(&2, U32, I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), x <> xt), _) == R.encrypt_blocks(R.blocks(1n+p, x <> xt), r, kb, c, nb) : List<&2, U32>}
250	      %Equal.sym(List<&2, U32>, I.xor_front(I.keystream(r, I.key(kb), c, I.nonce(nb)), x <> xt), R.xor_bytes(R.prefix(64n, x <> xt), R.block_rounds(r, kb, c, nb)), fr) :
251	        {List.append(&2, U32, _, R.encrypt_blocks(R.blocks(p, R.suffix(64n, x <> xt)), r, kb, c1, nb)) == R.encrypt_blocks(R.blocks(1n+p, x <> xt), r, kb, c, nb) : List<&2, U32>}
252	      {==}
253	
254	law encrypt_correct:
255	  for +r: Nat
256	  for +kb: List<&2, U32>
257	  for +c: U32
258	  for +nb: List<&2, U32>
259	  for +pt: List<&2, U32>
260	  {I.encrypt_rounds(r, kb, c, nb, pt) == R.encrypt_rounds(r, kb, c, nb, pt) : List<&2, U32>}
261	
262	def encrypt_correct(r, kb, c, nb, pt):
263	  stream_correct(List.length(&2, U32, pt), pt, r, kb, c, nb)
264