1#[allow(unused_imports)]
15use super::super::super::prelude::*;
16
17verus! {
18
19use super::super::super::arithmetic::internals::general_internals::*;
20use super::super::super::arithmetic::mul::*;
21#[cfg(verus_keep_ghost)]
22use super::mul_internals::group_mul_properties_internal;
23#[cfg(verus_keep_ghost)]
24use super::super::super::arithmetic::internals::mul_internals_nonlinear;
25#[cfg(verus_keep_ghost)]
26use super::super::super::arithmetic::internals::mod_internals_nonlinear::{
27 lemma_fundamental_div_mod,
28 lemma_mod_range,
29 lemma_small_mod,
30};
31#[cfg(verus_keep_ghost)]
32use super::super::super::arithmetic::internals::div_internals_nonlinear;
33#[cfg(verus_keep_ghost)]
34use super::super::super::math::{add as add1, sub as sub1};
35
36#[verifier::opaque]
38pub open spec fn mod_recursive(x: int, d: int) -> int
39 recommends
40 d > 0,
41 decreases
42 (if x < 0 {
43 (d - x)
44 } else {
45 x
46 }),
47 when d > 0
48{
49 if x < 0 {
50 mod_recursive(d + x, d)
51 } else if x < d {
52 x
53 } else {
54 mod_recursive(x - d, d)
55 }
56}
57
58pub proof fn lemma_mod_induction_forall(n: int, f: spec_fn(int) -> bool)
80 requires
81 n > 0,
82 forall|i: int| 0 <= i < n ==> #[trigger] f(i),
83 forall|i: int| i >= 0 && #[trigger] f(i) ==> #[trigger] f(add1(i, n)),
84 forall|i: int| i < n && #[trigger] f(i) ==> #[trigger] f(sub1(i, n)),
85 ensures
86 forall|i| #[trigger] f(i),
87{
88 assert forall|i: int| #[trigger] f(i) by {
89 lemma_induction_helper(n, f, i);
90 };
91}
92
93pub proof fn lemma_mod_induction_forall2(n: int, f: spec_fn(int, int) -> bool)
121 requires
122 n > 0,
123 forall|i: int, j: int| 0 <= i < n && 0 <= j < n ==> #[trigger] f(i, j),
124 forall|i: int, j: int| i >= 0 && #[trigger] f(i, j) ==> #[trigger] f(add1(i, n), j),
125 forall|i: int, j: int| j >= 0 && #[trigger] f(i, j) ==> #[trigger] f(i, add1(j, n)),
126 forall|i: int, j: int| i < n && #[trigger] f(i, j) ==> #[trigger] f(sub1(i, n), j),
127 forall|i: int, j: int| j < n && #[trigger] f(i, j) ==> #[trigger] f(i, sub1(j, n)),
128 ensures
129 forall|i: int, j: int| #[trigger] f(i, j),
130{
131 assert forall|x: int, y: int| #[trigger] f(x, y) by {
132 assert forall|i: int| 0 <= i < n implies #[trigger] f(i, y) by {
133 let fj = |j| f(i, j);
134 lemma_mod_induction_forall(n, fj);
135 assert(fj(y));
136 };
137 let fi = |i| f(i, y);
138 lemma_mod_induction_forall(n, fi);
139 assert(fi(x));
140 };
141}
142
143#[verifier::spinoff_prover]
147pub proof fn lemma_div_add_denominator(n: int, x: int)
148 requires
149 n > 0,
150 ensures
151 (x + n) / n == x / n + 1,
152{
153 lemma_fundamental_div_mod(x, n);
154 lemma_fundamental_div_mod(x + n, n);
155 let zp = (x + n) / n - x / n - 1;
156 assert(0 == n * zp + ((x + n) % n) - (x % n)) by {
157 broadcast use group_mul_properties_internal;
158
159 };
160 if (zp > 0) {
161 lemma_mul_inequality(1, zp, n);
162 }
163 if (zp < 0) {
164 lemma_mul_inequality(zp, -1, n);
165 }
166}
167
168pub proof fn lemma_div_sub_denominator(n: int, x: int)
172 requires
173 n > 0,
174 ensures
175 (x - n) / n == x / n - 1,
176{
177 lemma_fundamental_div_mod(x, n);
178 lemma_fundamental_div_mod(x - n, n);
179 let zm = (x - n) / n - x / n + 1;
180 assert(0 == n * zm + ((x - n) % n) - (x % n)) by {
181 broadcast use group_mul_properties_internal;
182
183 }
184 if (zm > 0) {
185 lemma_mul_inequality(1, zm, n);
186 }
187 if (zm < 0) {
188 lemma_mul_inequality(zm, -1, n);
189 }
190}
191
192#[verifier::spinoff_prover]
196pub proof fn lemma_mod_add_denominator(n: int, x: int)
197 requires
198 n > 0,
199 ensures
200 (x + n) % n == x % n,
201{
202 lemma_fundamental_div_mod(x, n);
203 lemma_fundamental_div_mod(x + n, n);
204 let zp = (x + n) / n - x / n - 1;
205 assert(n * zp == n * ((x + n) / n - x / n) - n) by {
206 assert(n * (((x + n) / n - x / n) - 1) == n * ((x + n) / n - x / n) - n) by {
207 broadcast use group_mul_is_commutative_and_distributive;
208
209 };
210 };
211 assert(0 == n * zp + ((x + n) % n) - (x % n)) by {
212 broadcast use group_mul_properties_internal;
213
214 }
215 if (zp > 0) {
216 lemma_mul_inequality(1, zp, n);
217 } else if (zp < 0) {
218 lemma_mul_inequality(zp, -1, n);
219 } else {
220 broadcast use group_mul_properties_internal;
221
222 }
223}
224
225pub proof fn lemma_mod_sub_denominator(n: int, x: int)
229 requires
230 n > 0,
231 ensures
232 (x - n) % n == x % n,
233{
234 lemma_fundamental_div_mod(x, n);
235 lemma_fundamental_div_mod(x - n, n);
236 let zm = (x - n) / n - x / n + 1;
237 broadcast use group_mul_is_distributive; assert(0 == n * zm + ((x - n) % n) - (x % n)) by {
240 broadcast use group_mul_properties_internal;
241
242 }
243 if (zm > 0) {
244 lemma_mul_inequality(1, zm, n);
245 }
246 if (zm < 0) {
247 lemma_mul_inequality(zm, -1, n);
248 }
249}
250
251pub proof fn lemma_mod_below_denominator(n: int, x: int)
254 requires
255 n > 0,
256 ensures
257 0 <= x < n <==> x % n == x,
258{
259 assert forall|x: int| 0 <= x < n <==> #[trigger] (x % n) == x by {
260 if (0 <= x < n) {
261 lemma_small_mod(x as nat, n as nat);
262 }
263 lemma_mod_range(x, n);
264 }
265}
266
267pub proof fn lemma_mod_basics(n: int)
278 requires
279 n > 0,
280 ensures
281 forall|x: int| #[trigger] ((x + n) % n) == x % n,
282 forall|x: int| #[trigger] ((x - n) % n) == x % n,
283 forall|x: int| #[trigger] ((x + n) / n) == x / n + 1,
284 forall|x: int| #[trigger] ((x - n) / n) == x / n - 1,
285 forall|x: int| 0 <= x < n <==> #[trigger] (x % n) == x,
286{
287 assert forall|x: int| #[trigger] ((x + n) % n) == x % n by {
288 lemma_mod_add_denominator(n, x);
289 };
290 assert forall|x: int| #[trigger] ((x - n) % n) == x % n by {
291 lemma_mod_sub_denominator(n, x);
292 assert((x - n) % n == x % n);
293 };
294 assert forall|x: int| #[trigger] ((x + n) / n) == x / n + 1 by {
295 lemma_div_add_denominator(n, x);
296 };
297 assert forall|x: int| #[trigger] ((x - n) / n) == x / n - 1 by {
298 lemma_div_sub_denominator(n, x);
299 };
300 assert forall|x: int| 0 <= x < n <==> #[trigger] (x % n) == x by {
301 lemma_mod_below_denominator(n, x);
302 };
303}
304
305pub proof fn lemma_quotient_and_remainder(x: int, q: int, r: int, n: int)
309 requires
310 n > 0,
311 0 <= r < n,
312 x == q * n + r,
313 ensures
314 q == x / n,
315 r == x % n,
316 decreases
317 (if q > 0 {
318 q
319 } else {
320 -q
321 }),
322{
323 lemma_mod_basics(n);
324 if q > 0 {
325 mul_internals_nonlinear::lemma_mul_is_distributive_add(n, q - 1, 1);
326 broadcast use lemma_mul_is_commutative;
327
328 assert(q * n + r == (q - 1) * n + n + r);
329 lemma_quotient_and_remainder(x - n, q - 1, r, n);
330 } else if q < 0 {
331 lemma_mul_is_distributive_sub(n, q + 1, 1);
332 broadcast use lemma_mul_is_commutative;
333
334 assert(q * n + r == (q + 1) * n - n + r);
335 lemma_quotient_and_remainder(x + n, q + 1, r, n);
336 } else {
337 div_internals_nonlinear::lemma_small_div();
338 assert(r / n == 0);
339 }
340}
341
342pub open spec fn mod_auto_plus(n: int) -> bool
347 recommends
348 n > 0,
349{
350 forall|x: int, y: int|
351 {
352 let z = (x % n) + (y % n);
353 ((0 <= z < n && #[trigger] ((x + y) % n) == z) || (n <= z < n + n && ((x + y) % n) == z
354 - n))
355 }
356}
357
358pub open spec fn mod_auto_minus(n: int) -> bool
363 recommends
364 n > 0,
365{
366 forall|x: int, y: int|
367 {
368 let z = (x % n) - (y % n);
369 ((0 <= z < n && #[trigger] ((x - y) % n) == z) || (-n <= z < 0 && ((x - y) % n) == z
370 + n))
371 }
372}
373
374pub open spec fn mod_auto(n: int) -> bool
377 recommends
378 n > 0,
379{
380 &&& (n % n == 0 && (-n) % n == 0)
381 &&& (forall|x: int| #[trigger] ((x % n) % n) == x % n)
382 &&& (forall|x: int| 0 <= x < n <==> #[trigger] (x % n) == x)
383 &&& mod_auto_plus(n)
384 &&& mod_auto_minus(n)
385}
386
387pub proof fn lemma_mod_auto(n: int)
391 requires
392 n > 0,
393 ensures
394 mod_auto(n),
395{
396 lemma_mod_basics(n);
397 broadcast use group_mul_properties_internal;
398
399 assert forall|x: int, y: int|
400 {
401 let z = (x % n) + (y % n);
402 ((0 <= z < n && #[trigger] ((x + y) % n) == z) || (n <= z < n + n && ((x + y) % n) == z
403 - n))
404 } by {
405 let xq = x / n;
406 let xr = x % n;
407 lemma_fundamental_div_mod(x, n);
408 assert(x == xq * n + xr);
409 let yq = y / n;
410 let yr = y % n;
411 lemma_fundamental_div_mod(y, n);
412 assert(y == yq * n + yr);
413 if xr + yr < n {
414 lemma_quotient_and_remainder(x + y, xq + yq, xr + yr, n);
415 } else {
416 lemma_quotient_and_remainder(x + y, xq + yq + 1, xr + yr - n, n);
417 }
418 }
419 assert forall|x: int, y: int|
420 {
421 let z = (x % n) - (y % n);
422 ((0 <= z < n && #[trigger] ((x - y) % n) == z) || (-n <= z < 0 && ((x - y) % n) == z
423 + n))
424 } by {
425 let xq = x / n;
426 let xr = x % n;
427 lemma_fundamental_div_mod(x, n);
428 assert(x == n * (x / n) + (x % n));
429 let yq = y / n;
430 let yr = y % n;
431 lemma_fundamental_div_mod(y, n);
432 assert(y == yq * n + yr);
433 if xr - yr >= 0 {
434 lemma_quotient_and_remainder(x - y, xq - yq, xr - yr, n);
435 } else { lemma_quotient_and_remainder(x - y, xq - yq - 1, xr - yr + n, n);
437 }
438 }
439}
440
441pub proof fn lemma_mod_induction_auto(n: int, x: int, f: spec_fn(int) -> bool)
469 requires
470 n > 0,
471 mod_auto(n) ==> {
472 &&& (forall|i: int| #[trigger] is_le(0, i) && i < n ==> f(i))
473 &&& (forall|i: int| #[trigger] is_le(0, i) && f(i) ==> f(i + n))
474 &&& (forall|i: int| #[trigger] is_le(i + 1, n) && f(i) ==> f(i - n))
475 },
476 ensures
477 mod_auto(n),
478 f(x),
479{
480 lemma_mod_auto(n);
481 assert(forall|i: int| is_le(0, i) && #[trigger] f(i) ==> #[trigger] f(add1(i, n)));
482 assert(forall|i: int| is_le(i + 1, n) && #[trigger] f(i) ==> #[trigger] f(sub1(i, n)));
483 assert forall|i: int| 0 <= i < n implies #[trigger] f(i) by {
484 assert(forall|i: int| is_le(0, i) && i < n ==> f(i));
485 assert(is_le(0, i) && i < n);
486 };
487 lemma_mod_induction_forall(n, f);
488 assert(f(x));
489}
490
491pub proof fn lemma_mod_induction_auto_forall(n: int, f: spec_fn(int) -> bool)
516 requires
517 n > 0,
518 mod_auto(n) ==> {
519 &&& (forall|i: int| #[trigger] is_le(0, i) && i < n ==> f(i))
520 &&& (forall|i: int| #[trigger] is_le(0, i) && f(i) ==> f(i + n))
521 &&& (forall|i: int| #[trigger] is_le(i + 1, n) && f(i) ==> f(i - n))
522 },
523 ensures
524 mod_auto(n),
525 forall|i| #[trigger] f(i),
526{
527 assert(mod_auto(n)) by {
528 lemma_mod_induction_auto(n, 0, f);
529 }
530 assert forall|i| #[trigger] f(i) by {
531 lemma_mod_induction_auto(n, i, f);
532 }
533}
534
535}