proofs/crypto/sha/padding.bend
bend-collections@1.0.0.0 · 253 lines · 1 definition
1import Base
2import bend-collections@1.0.0.0/spec/crypto/sha.bend as F
3
4
5
6law zeros_correct:
7 for r: Nat
8 {Nat.mod(Nat.sub(119n, r), 64n) == F.zero_count(r) : Nat}
9
10def 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 {==}