1	import Base
2	import ../../../spec/crypto/sha.bend as F
3	
4	# Universal bridge from implementation modular padding to the FIPS piecewise rule.
5	# Every Nat is either one of 0..119 or 120+p. Each branch closes by reduction.
6	law zeros_correct:
7	  for r: Nat
8	  {Nat.mod(Nat.sub(119n, r), 64n) == F.zero_count(r) : Nat}
9	
10	def zeros_correct(r):
11	  match r:
12	    case 0n:
13	      {==}
14	    case 1n:
15	      {==}
16	    case 2n:
17	      {==}
18	    case 3n:
19	      {==}
20	    case 4n:
21	      {==}
22	    case 5n:
23	      {==}
24	    case 6n:
25	      {==}
26	    case 7n:
27	      {==}
28	    case 8n:
29	      {==}
30	    case 9n:
31	      {==}
32	    case 10n:
33	      {==}
34	    case 11n:
35	      {==}
36	    case 12n:
37	      {==}
38	    case 13n:
39	      {==}
40	    case 14n:
41	      {==}
42	    case 15n:
43	      {==}
44	    case 16n:
45	      {==}
46	    case 17n:
47	      {==}
48	    case 18n:
49	      {==}
50	    case 19n:
51	      {==}
52	    case 20n:
53	      {==}
54	    case 21n:
55	      {==}
56	    case 22n:
57	      {==}
58	    case 23n:
59	      {==}
60	    case 24n:
61	      {==}
62	    case 25n:
63	      {==}
64	    case 26n:
65	      {==}
66	    case 27n:
67	      {==}
68	    case 28n:
69	      {==}
70	    case 29n:
71	      {==}
72	    case 30n:
73	      {==}
74	    case 31n:
75	      {==}
76	    case 32n:
77	      {==}
78	    case 33n:
79	      {==}
80	    case 34n:
81	      {==}
82	    case 35n:
83	      {==}
84	    case 36n:
85	      {==}
86	    case 37n:
87	      {==}
88	    case 38n:
89	      {==}
90	    case 39n:
91	      {==}
92	    case 40n:
93	      {==}
94	    case 41n:
95	      {==}
96	    case 42n:
97	      {==}
98	    case 43n:
99	      {==}
100	    case 44n:
101	      {==}
102	    case 45n:
103	      {==}
104	    case 46n:
105	      {==}
106	    case 47n:
107	      {==}
108	    case 48n:
109	      {==}
110	    case 49n:
111	      {==}
112	    case 50n:
113	      {==}
114	    case 51n:
115	      {==}
116	    case 52n:
117	      {==}
118	    case 53n:
119	      {==}
120	    case 54n:
121	      {==}
122	    case 55n:
123	      {==}
124	    case 56n:
125	      {==}
126	    case 57n:
127	      {==}
128	    case 58n:
129	      {==}
130	    case 59n:
131	      {==}
132	    case 60n:
133	      {==}
134	    case 61n:
135	      {==}
136	    case 62n:
137	      {==}
138	    case 63n:
139	      {==}
140	    case 64n:
141	      {==}
142	    case 65n:
143	      {==}
144	    case 66n:
145	      {==}
146	    case 67n:
147	      {==}
148	    case 68n:
149	      {==}
150	    case 69n:
151	      {==}
152	    case 70n:
153	      {==}
154	    case 71n:
155	      {==}
156	    case 72n:
157	      {==}
158	    case 73n:
159	      {==}
160	    case 74n:
161	      {==}
162	    case 75n:
163	      {==}
164	    case 76n:
165	      {==}
166	    case 77n:
167	      {==}
168	    case 78n:
169	      {==}
170	    case 79n:
171	      {==}
172	    case 80n:
173	      {==}
174	    case 81n:
175	      {==}
176	    case 82n:
177	      {==}
178	    case 83n:
179	      {==}
180	    case 84n:
181	      {==}
182	    case 85n:
183	      {==}
184	    case 86n:
185	      {==}
186	    case 87n:
187	      {==}
188	    case 88n:
189	      {==}
190	    case 89n:
191	      {==}
192	    case 90n:
193	      {==}
194	    case 91n:
195	      {==}
196	    case 92n:
197	      {==}
198	    case 93n:
199	      {==}
200	    case 94n:
201	      {==}
202	    case 95n:
203	      {==}
204	    case 96n:
205	      {==}
206	    case 97n:
207	      {==}
208	    case 98n:
209	      {==}
210	    case 99n:
211	      {==}
212	    case 100n:
213	      {==}
214	    case 101n:
215	      {==}
216	    case 102n:
217	      {==}
218	    case 103n:
219	      {==}
220	    case 104n:
221	      {==}
222	    case 105n:
223	      {==}
224	    case 106n:
225	      {==}
226	    case 107n:
227	      {==}
228	    case 108n:
229	      {==}
230	    case 109n:
231	      {==}
232	    case 110n:
233	      {==}
234	    case 111n:
235	      {==}
236	    case 112n:
237	      {==}
238	    case 113n:
239	      {==}
240	    case 114n:
241	      {==}
242	    case 115n:
243	      {==}
244	    case 116n:
245	      {==}
246	    case 117n:
247	      {==}
248	    case 118n:
249	      {==}
250	    case 119n:
251	      {==}
252	    case 120n+p:
253	      {==}