1	# Generated by tools/generators/sha512_gen.py; do not edit by hand.
2	import Base
3	import ../../../src/crypto/sha512/types.bend as T
4	import ../../../src/crypto/sha512/core.bend as C
5	import ../../../spec/crypto/sha512.bend as F
6	
7	# src/crypto/sha512/core.bend refines spec/crypto/sha512.bend, the structure
8	# of proofs/crypto/sha/conformance.bend (SHA-256) at 64-bit words: one round
9	# and the feedforward are equal after opening every word into its halves;
10	# the rolling window computes the spec's recurrence over the reverse history;
11	# a block's rounds, the blocks, the parsing and the padding follow by
12	# induction, each short tail by enumeration.
13	
14	law step_correct:
15	  for +s: T.State
16	  for +k: T.Lane
17	  for +w: T.Lane
18	  {C.step(s, k, w) == F.step(s, k, w) : T.State}
19	
20	def step_correct(s, k, w):
21	  match s k w:
22	    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.W{kh, kl} T.W{wh, wl}:
23	      {==}
24	
25	law feedforward_correct:
26	  for +x: T.State
27	  for +y: T.State
28	  {C.feedforward(x, y) == F.feedforward(x, y) : T.State}
29	
30	def feedforward_correct(x, y):
31	  match x y:
32	    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}} T.H{T.W{ih, il}, T.W{jh, jl}, T.W{kh, kl}, T.W{lh, ll}, T.W{mh, ml}, T.W{nh, nl}, T.W{oh, ol}, T.W{ph, pl}}:
33	      {==}
34	
35	law next_correct:
36	  for +a: T.Lane
37	  for +b: T.Lane
38	  for +c: T.Lane
39	  for +d: T.Lane
40	  for +e: T.Lane
41	  for +f: T.Lane
42	  for +g: T.Lane
43	  for +h: T.Lane
44	  for +i: T.Lane
45	  for +j: T.Lane
46	  for +k: T.Lane
47	  for +l: T.Lane
48	  for +m: T.Lane
49	  for +n: T.Lane
50	  for +o: T.Lane
51	  for +p: T.Lane
52	  for +rest: List<&2, T.Lane>
53	  {C.next(b, g, o, p) == F.recurrence(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest) : T.Lane}
54	
55	def next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest):
56	  match b g o p:
57	    case T.W{bh, bl} T.W{gh, gl} T.W{oh, ol} T.W{ph, pl}:
58	      {==}
59	
60	law window_rounds_correct:
61	  for +q: Nat
62	  for +a: T.Lane
63	  for +b: T.Lane
64	  for +c: T.Lane
65	  for +d: T.Lane
66	  for +e: T.Lane
67	  for +f: T.Lane
68	  for +g: T.Lane
69	  for +h: T.Lane
70	  for +i: T.Lane
71	  for +j: T.Lane
72	  for +k: T.Lane
73	  for +l: T.Lane
74	  for +m: T.Lane
75	  for +n: T.Lane
76	  for +o: T.Lane
77	  for +p: T.Lane
78	  for +rest: List<&2, T.Lane>
79	  for +ks: List<&2, T.Lane>
80	  for +s: T.State
81	  {C.window_rounds(q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) == F.rounds(ks, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(s) : T.State}
82	
83	def window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s):
84	  match q ks:
85	    case 0n Nil{}:
86	      {==}
87	    case 0n x <> xt:
88	      {==}
89	    case 1n+r Nil{}:
90	      {==}
91	    case 1n+r x <> xt:
92	      %next_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest) :
93	        {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
94	          F.rounds(xt, F.extension(r, _ <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(F.step(s, x, _)) : T.State}
95	      %step_correct(s, x, C.next(b, g, o, p)) :
96	        {C.window_rounds(1n+r, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
97	          F.rounds(xt, F.extension(r, C.next(b, g, o, p) <> a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest))(_) : T.State}
98	      window_rounds_correct(r, C.next(b, g, o, p), a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p <> rest, xt,
99	        C.step(s, x, C.next(b, g, o, p)))
100	
101	law block_rounds_correct:
102	  for +ws: List<&2, T.Lane>
103	  for +q: Nat
104	  for +a: T.Lane
105	  for +b: T.Lane
106	  for +c: T.Lane
107	  for +d: T.Lane
108	  for +e: T.Lane
109	  for +f: T.Lane
110	  for +g: T.Lane
111	  for +h: T.Lane
112	  for +i: T.Lane
113	  for +j: T.Lane
114	  for +k: T.Lane
115	  for +l: T.Lane
116	  for +m: T.Lane
117	  for +n: T.Lane
118	  for +o: T.Lane
119	  for +p: T.Lane
120	  for +rest: List<&2, T.Lane>
121	  for +ks: List<&2, T.Lane>
122	  for +s: T.State
123	  {C.block_rounds(ws, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, ks, s) ==
124	    F.rounds(ks, List.append(&2, T.Lane, ws, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(s) : T.State}
125	
126	def block_rounds_correct(ws, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s):
127	  match ws ks:
128	    case Nil{} _:
129	      window_rounds_correct(q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, ks, s)
130	    case w <> wt Nil{}:
131	      {==}
132	    case w <> wt x <> xt:
133	      %step_correct(s, x, w) :
134	        {C.block_rounds(w <> wt, q, C.Win{a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p}, x <> xt, s) ==
135	          F.rounds(xt, List.append(&2, T.Lane, wt, F.extension(q, a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest)))(_) : T.State}
136	      block_rounds_correct(wt, q, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, rest, xt, C.step(s, x, w))
137	
138	law compress16_correct:
139	  for +a: T.Lane
140	  for +b: T.Lane
141	  for +c: T.Lane
142	  for +d: T.Lane
143	  for +e: T.Lane
144	  for +f: T.Lane
145	  for +g: T.Lane
146	  for +h: T.Lane
147	  for +i: T.Lane
148	  for +j: T.Lane
149	  for +k: T.Lane
150	  for +l: T.Lane
151	  for +m: T.Lane
152	  for +n: T.Lane
153	  for +o: T.Lane
154	  for +p: T.Lane
155	  for +q: Nat
156	  for +ks: List<&2, T.Lane>
157	  for +s: T.State
158	  {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == F.compress(F.schedule(q, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]), ks, s) : T.State}
159	
160	def compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s):
161	  +r = F.rounds(ks, List.append(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], F.extension(q, List.reverse(&2, T.Lane, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]))))(s)
162	  %feedforward_correct(s, r) : {C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) == _ : T.State}
163	  Equal.cong(T.State, T.State, t => C.feedforward(s, t),
164	    C.block_rounds([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, C.Win{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s), r,
165	    block_rounds_correct([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a, Nil{}, ks, s))
166	
167	law blocks_correct:
168	  for +ws: List<&2, T.Lane>
169	  for +q: Nat
170	  for +ks: List<&2, T.Lane>
171	  for +s: T.State
172	  {C.blocks(ws, q, ks, s) == F.blocks(F.schedules(ws, q), ks)(s) : T.State}
173	
174	def blocks_correct(ws, q, ks, s):
175	  match ws:
176	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
177	      %compress16_correct(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s) :
178	        {C.blocks(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest, q, ks, s) == F.blocks(F.schedules(rest, q), ks)(_) : T.State}
179	      blocks_correct(rest, q, ks, C.compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s))
180	    case Nil{}:
181	      {==}
182	    case a <> Nil{}:
183	      {==}
184	    case a <> b <> Nil{}:
185	      {==}
186	    case a <> b <> c <> Nil{}:
187	      {==}
188	    case a <> b <> c <> d <> Nil{}:
189	      {==}
190	    case a <> b <> c <> d <> e <> Nil{}:
191	      {==}
192	    case a <> b <> c <> d <> e <> f <> Nil{}:
193	      {==}
194	    case a <> b <> c <> d <> e <> f <> g <> Nil{}:
195	      {==}
196	    case a <> b <> c <> d <> e <> f <> g <> h <> Nil{}:
197	      {==}
198	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> Nil{}:
199	      {==}
200	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> Nil{}:
201	      {==}
202	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> Nil{}:
203	      {==}
204	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> Nil{}:
205	      {==}
206	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> Nil{}:
207	      {==}
208	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> Nil{}:
209	      {==}
210	    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> Nil{}:
211	      {==}
212	
213	law lanes_correct:
214	  for +bytes: List<&2, U32>
215	  {C.lanes(bytes) == F.words(bytes) : List<&2, T.Lane>}
216	
217	def lanes_correct(bytes):
218	  match bytes:
219	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:
220	      %lanes_correct(rest) :
221	        {C.lanes(b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest) == T.W{F.decode(b0, b1, b2, b3), F.decode(b4, b5, b6, b7)} <> _ : List<&2, T.Lane>}
222	      {==}
223	    case Nil{}:
224	      {==}
225	    case b0 <> Nil{}:
226	      {==}
227	    case b0 <> b1 <> Nil{}:
228	      {==}
229	    case b0 <> b1 <> b2 <> Nil{}:
230	      {==}
231	    case b0 <> b1 <> b2 <> b3 <> Nil{}:
232	      {==}
233	    case b0 <> b1 <> b2 <> b3 <> b4 <> Nil{}:
234	      {==}
235	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> Nil{}:
236	      {==}
237	    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> Nil{}:
238	      {==}
239	
240	law zeros_correct:
241	  for +r: Nat
242	  for +fits: Bool
243	  {C.zeros_if(r, fits) == F.zero_count_if(r, fits) : Nat}
244	
245	def zeros_correct(r, fits):
246	  match fits:
247	    case True{}:
248	      {==}
249	    case False{}:
250	      {==}
251	
252	law suffix_correct:
253	  for +n: Nat
254	  {C.suffix(n) == F.padding_suffix(n) : List<&2, U32>}
255	
256	def suffix_correct(n):
257	  %zeros_correct(Nat.mod(n, 128n), Nat.is_le(Nat.mod(n, 128n), 111n)) :
258	    {C.suffix(n) == 128 <> List.append(&2, U32, List.replicate(U32, _, 0), F.length_field(n)) : List<&2, U32>}
259	  {==}
260	
261	law digest_correct:
262	  for +s: T.State
263	  {C.digest_bytes(s) == F.digest_octets(F.digest(s)) : List<&2, U32>}
264	
265	def digest_correct(s):
266	  match s:
267	    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}:
268	      {==}
269	
270	law digest_length:
271	  for +s: T.State
272	  {List.length(&2, U32, C.digest_bytes(s)) == 64n : Nat}
273	
274	def digest_length(s):
275	  match s:
276	    case T.H{T.W{ah, al}, T.W{bh, bl}, T.W{ch, cl}, T.W{dh, dl}, T.W{eh, el}, T.W{fh, fl}, T.W{gh, gl}, T.W{hh, hl}}:
277	      {==}
278	
279	law constants_correct:
280	  {C.round_constants() == F.constants() : List<&2, T.Lane>}
281	
282	def constants_correct():
283	  {==}
284	
285	law initial_correct:
286	  {C.initial() == F.initial() : T.State}
287	
288	def initial_correct():
289	  {==}
290	
291	law sha512_correct:
292	  for +bytes: List<&2, U32>
293	  {C.sha512(bytes) == F.sha512_bytes(bytes) : List<&2, U32>}
294	
295	def sha512_correct(bytes):
296	  +n = List.length(&2, U32, bytes)
297	  %suffix_correct(n) :
298	    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(F.words(
299	      List.append(&2, U32, bytes, _)), 64n), F.constants())(F.initial()))) : List<&2, U32>}
300	  +padded = List.append(&2, U32, bytes, C.suffix(n))
301	  %lanes_correct(padded) :
302	    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(_, 64n), F.constants())(F.initial()))) : List<&2, U32>}
303	  %Equal.sym(List<&2, T.Lane>, C.round_constants(), F.constants(), constants_correct()) :
304	    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), _)(F.initial()))) : List<&2, U32>}
305	  %Equal.sym(T.State, C.initial(), F.initial(), initial_correct()) :
306	    {C.sha512(bytes) == F.digest_octets(F.digest(F.blocks(F.schedules(C.lanes(padded), 64n), C.round_constants())(_))) : List<&2, U32>}
307	  %blocks_correct(C.lanes(padded), 64n, C.round_constants(), C.initial()) :
308	    {C.sha512(bytes) == F.digest_octets(F.digest(_)) : List<&2, U32>}
309	  digest_correct(C.blocks(C.lanes(padded), 64n, C.round_constants(), C.initial()))