1use super::super::calc_macro::*;
15#[allow(unused_imports)]
16use super::super::prelude::*;
17
18verus! {
19
20#[allow(unused_imports)]
21#[cfg(verus_keep_ghost)]
22use super::super::arithmetic::internals::div_internals::{
23 div_recursive,
24 lemma_div_induction_auto,
25 div_auto,
26 div_pos,
27 lemma_div_auto,
28};
29use super::super::arithmetic::internals::div_internals_nonlinear as DivINL;
30#[cfg(verus_keep_ghost)]
31use super::super::arithmetic::internals::mod_internals::{
32 lemma_div_add_denominator,
33 lemma_mod_auto,
34 mod_recursive,
35};
36use super::super::arithmetic::internals::mod_internals_nonlinear as ModINL;
37#[cfg(verus_keep_ghost)]
38use super::internals::mul_internals::{
39 group_mul_properties_internal,
40 lemma_mul_induction,
41 lemma_mul_induction_auto,
42};
43#[cfg(verus_keep_ghost)]
44use super::super::arithmetic::internals::general_internals::{is_le};
45#[cfg(verus_keep_ghost)]
46use super::super::math::{add as add1, sub as sub1, div as div1};
47use super::super::arithmetic::mul::*;
48
49pub broadcast proof fn lemma_div_is_div_recursive(x: int, d: int)
56 requires
57 0 < d,
58 ensures
59 div_recursive(x, d) == #[trigger] (x / d),
60{
61 reveal(div_recursive);
62 reveal(div_pos);
63 lemma_div_induction_auto(d, x, |u: int| div_recursive(u, d) == u / d);
64}
65
66pub proof fn lemma_div_by_self(d: int)
69 requires
70 d != 0,
71 ensures
72 d / d == 1,
73{
74 DivINL::lemma_div_by_self(d);
75}
76
77pub proof fn lemma_div_of0(d: int)
79 requires
80 d != 0,
81 ensures
82 0 as int / d == 0,
83{
84 DivINL::lemma_div_of0(d);
85}
86
87pub proof fn lemma_div_basics(x: int)
91 ensures
92 x != 0 as int ==> 0 as int / x == 0,
93 x / 1 == x,
94 x != 0 ==> x / x == 1,
95{
96 if (x != 0) {
97 lemma_div_by_self(x);
98 lemma_div_of0(x);
99 }
100}
101
102pub broadcast proof fn lemma_div_basics_1(x: int)
104 ensures
105 x != 0 as int ==> #[trigger] (0int / x) == 0,
106{
107 lemma_div_basics(x);
108}
109
110pub broadcast proof fn lemma_div_basics_2(x: int)
112 ensures
113 #[trigger] (x / 1) == x,
114{
115 lemma_div_basics(x);
116}
117
118pub broadcast proof fn lemma_div_basics_3(x: int)
120 ensures
121 x != 0 ==> #[trigger] (x / x) == 1,
122{
123 lemma_div_basics(x);
124}
125
126pub broadcast proof fn lemma_div_basics_4(x: int, y: int)
128 ensures
129 x >= 0 && y > 0 ==> #[trigger] (x / y) >= 0,
130{
131}
132
133pub broadcast proof fn lemma_div_basics_5(x: int, y: int)
136 ensures
137 x >= 0 && y > 0 ==> #[trigger] (x / y) <= x,
138{
139 assert forall|x: int, y: int| x >= 0 && y > 0 implies 0 <= #[trigger] (x / y) <= x by {
140 lemma_div_pos_is_pos(x, y);
141 lemma_div_is_ordered_by_denominator(x, 1, y);
142 };
143}
144
145pub broadcast group group_div_basics {
146 lemma_div_basics_1,
147 lemma_div_basics_2,
148 lemma_div_basics_3,
149 lemma_div_basics_4,
150 lemma_div_basics_5,
151}
152
153pub broadcast proof fn lemma_small_div_converse(x: int, d: int)
157 ensures
158 0 <= x && 0 < d && #[trigger] (x / d) == 0 ==> x < d,
159{
160 assert forall|x: int, d: int| 0 <= x && 0 < d && #[trigger] (x / d) == 0 implies x < d by {
161 lemma_div_induction_auto(d, x, |u: int| 0 <= u && 0 < d && u / d == 0 ==> u < d);
162 }
163}
164
165pub proof fn lemma_div_non_zero(x: int, d: int)
169 requires
170 x >= d > 0,
171 ensures
172 #[trigger] (x / d) > 0,
173{
174 broadcast use lemma_div_pos_is_pos;
175
176 if x / d == 0 {
177 broadcast use lemma_small_div_converse;
178
179 }
180}
181
182pub broadcast proof fn lemma_div_is_ordered_by_denominator(x: int, y: int, z: int)
188 requires
189 0 <= x,
190 1 <= y <= z,
191 ensures
192 #[trigger] (x / y) >= #[trigger] (x / z),
193 decreases x,
194{
195 reveal(div_recursive);
196 reveal(div_pos);
197 broadcast use lemma_div_is_div_recursive;
198
199 assert(forall|u: int, d: int|
200 #![trigger div_recursive(u, d)]
201 #![trigger div1(u, d)]
202 d > 0 ==> div_recursive(u, d) == div1(u, d));
203 if (x < z) {
204 lemma_div_is_ordered(0, x, y);
205 } else {
206 lemma_div_is_ordered(x - z, x - y, y);
207 lemma_div_is_ordered_by_denominator(x - z, y, z);
208 }
209}
210
211pub broadcast proof fn lemma_div_is_strictly_smaller(x: int, d: int)
214 requires
215 0 < x,
216 1 < d,
217 ensures
218 #[trigger] (x / d) < x,
219 decreases x,
220{
221 lemma_div_induction_auto(d, x, |u: int| 0 < u ==> u / d < u);
222}
223
224pub broadcast proof fn lemma_dividing_sums(a: int, b: int, d: int, r: int)
227 requires
228 0 < d,
229 r == a % d + b % d - (a + b) % d,
230 ensures
231 #![trigger (d * ((a + b) / d) - r), (d * (a / d) + d * (b / d))]
232 d * ((a + b) / d) - r == d * (a / d) + d * (b / d),
233{
234 ModINL::lemma_fundamental_div_mod(a + b, d);
235 ModINL::lemma_fundamental_div_mod(a, d);
236 ModINL::lemma_fundamental_div_mod(b, d);
237}
238
239pub broadcast proof fn lemma_div_pos_is_pos(x: int, d: int)
243 requires
244 0 <= x,
245 0 < d,
246 ensures
247 0 <= #[trigger] (x / d),
248{
249 lemma_div_auto(d);
250 assert(div_auto(d));
251 let f = |u: int| 0 <= u ==> u / d >= 0;
252 assert forall|i: int| #[trigger] is_le(0, i) && f(i) implies f(i + d) by {
253 assert(i / d >= 0);
254 };
255 lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u / d >= 0);
256}
257
258pub broadcast proof fn lemma_div_plus_one(x: int, d: int)
262 requires
263 0 < d,
264 ensures
265 #![trigger (1 + x / d), ((d + x) / d)]
266 1 + x / d == (d + x) / d,
267{
268 lemma_div_auto(d);
269}
270
271pub broadcast proof fn lemma_div_minus_one(x: int, d: int)
275 requires
276 0 < d,
277 ensures
278 #![trigger (-1 + x / d), ((-d + x) / d)]
279 -1 + x / d == (-d + x) / d,
280{
281 lemma_div_auto(d);
282}
283
284pub proof fn lemma_basic_div_specific_divisor(d: int)
287 requires
288 0 < d,
289 ensures
290 forall|x: int| 0 <= x < d ==> #[trigger] (x / d) == 0,
291{
292 lemma_div_auto(d);
293}
294
295pub broadcast proof fn lemma_basic_div(x: int, d: int)
298 requires
299 0 <= x < d,
300 ensures
301 #[trigger] (x / d) == 0,
302{
303 lemma_basic_div_specific_divisor(d);
304}
305
306pub broadcast proof fn lemma_div_is_ordered(x: int, y: int, z: int)
310 requires
311 x <= y,
312 0 < z,
313 ensures
314 #[trigger] (x / z) <= #[trigger] (y / z),
315{
316 lemma_div_auto(z);
317 let f = |xy: int| xy <= 0 ==> (xy + y) / z <= y / z;
318 assert forall|i: int| #[trigger] is_le(i + 1, z) && f(i) implies f(i - z) by {
319 if (i - z <= 0) {
320 assert(f(i));
321 assert(i <= 0 ==> (i + y) / z <= y / z);
322 if (i > 0) {
323 assert(z > 0);
324 assert(i <= z);
325 assert(((i + y) - z) / z <= y / z);
326 } else {
327 assert((i + y) / z <= y / z);
328 }
329 assert((i - z + y) / z <= y / z);
330 }
331 };
332 lemma_div_induction_auto(z, x - y, |xy: int| xy <= 0 ==> (xy + y) / z <= y / z);
333}
334
335pub broadcast proof fn lemma_div_decreases(x: int, d: int)
338 requires
339 0 < x,
340 1 < d,
341 ensures
342 #[trigger] (x / d) < x,
343{
344 lemma_div_induction_auto(d, x, |u: int| 0 < u ==> u / d < u);
345}
346
347pub broadcast proof fn lemma_div_nonincreasing(x: int, d: int)
351 requires
352 0 <= x,
353 0 < d,
354 ensures
355 #[trigger] (x / d) <= x,
356{
357 lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u / d <= u);
358}
359
360pub proof fn lemma_small_mod(x: nat, m: nat)
364 requires
365 x < m,
366 0 < m,
367 ensures
368 x % m == x,
369{
370 ModINL::lemma_small_mod(x, m);
371}
372
373pub broadcast proof fn lemma_breakdown(x: int, y: int, z: int)
378 requires
379 0 <= x,
380 0 < y,
381 0 < z,
382 ensures
383 #![trigger y * z, x % (y * z), y * ((x / y) % z) + x % y]
384 0 < y * z,
385 (x % (y * z)) == y * ((x / y) % z) + x % y,
386{
387 broadcast use lemma_mul_strictly_positive;
388
389 lemma_div_pos_is_pos(x, y);
390 calc! {
391 (<)
392 (y * (x / y)) % (y * z) + (x % y) % (y * z); (<=) {
393 lemma_part_bound1(x, y, z);
394 }
395 y * (z - 1) + (x % y) % (y * z); (<) {
396 lemma_part_bound2(x, y, z);
397 }
398 y * (z - 1) + y; (==) {
399 broadcast use group_mul_basics;
400
401 }
402 y * (z - 1) + y * 1; (==) {
403 broadcast use group_mul_is_distributive;
404
405 }
406 y * (z - 1 + 1); (==) {}
407 y * z;
408 }
409 calc! {
410 (==)
411 x % (y * z); {
412 ModINL::lemma_fundamental_div_mod(x, y);
413 }
414 (y * (x / y) + x % y) % (y * z); {
415 broadcast use group_mod_properties;
416
417 assert(0 <= x % y);
418 lemma_mul_nonnegative(y, x / y);
419 assert((y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z);
420 lemma_mod_adds(y * (x / y), x % y, y * z);
421 }
422 (y * (x / y)) % (y * z) + (x % y) % (y * z); {
423 broadcast use {group_mod_properties, lemma_mul_is_commutative};
424
425 lemma_mul_increases(z, y);
426 assert((x % y) < y && y <= (y * z));
429 lemma_small_mod((x % y) as nat, (y * z) as nat);
430 assert((x % y) % (y * z) == x % y);
431 }
432 (y * (x / y)) % (y * z) + x % y; {
433 lemma_truncate_middle(x / y, y, z);
434 }
435 y * ((x / y) % z) + x % y;
436 }
437}
438
439pub broadcast proof fn lemma_remainder_upper(x: int, d: int)
443 requires
444 0 <= x,
445 0 < d,
446 ensures
447 #![trigger (x - d), (x / d * d)]
448 x - d < x / d * d,
449{
450 broadcast use group_mul_properties_internal;
451
452 lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u - d < u / d * d);
453}
454
455pub broadcast proof fn lemma_remainder_lower(x: int, d: int)
459 requires
460 0 <= x,
461 0 < d,
462 ensures
463 x >= #[trigger] (x / d * d),
464{
465 broadcast use group_mul_properties_internal;
466
467 lemma_div_induction_auto(d, x, |u: int| 0 <= u ==> u >= u / d * d);
468}
469
470pub broadcast proof fn lemma_remainder(x: int, d: int)
475 requires
476 0 <= x,
477 0 < d,
478 ensures
479 0 <= #[trigger] (x - (x / d * d)) < d,
480{
481 broadcast use group_mul_properties_internal;
482
483 lemma_div_induction_auto(d, x, |u: int| 0 <= u - u / d * d < d);
484}
485
486pub broadcast proof fn lemma_fundamental_div_mod(x: int, d: int)
490 requires
491 d != 0,
492 ensures
493 x == #[trigger] (d * (x / d) + (x % d)),
494{
495 assert(x == d * (x / d) + (x % d)) by {
496 ModINL::lemma_fundamental_div_mod(x, d);
497 }
498}
499
500pub broadcast proof fn lemma_div_denominator(x: int, c: int, d: int)
503 requires
504 0 <= x,
505 0 < c,
506 0 < d,
507 ensures
508 c * d != 0,
509 #[trigger] ((x / c) / d) == x / (c * d),
510{
511 lemma_mul_strictly_positive(c, d);
512 let r = x % (c as int * d as int);
513 lemma_div_pos_is_pos(r, c as int);
514 if (r / c as int >= d) {
515 ModINL::lemma_fundamental_div_mod(r, c as int);
516 lemma_mul_inequality(d as int, r / c as int, c as int);
517 lemma_mul_is_commutative(d, c);
518 }
519 assert(r / (c as int) < d);
520 lemma_fundamental_div_mod_converse(r / c, d, 0, r / c);
521 assert((r / c as int) % d as int == r / c as int);
522 lemma_fundamental_div_mod(r, c);
523 assert(c * (r / c) + r % c == r);
524 assert(c * ((r / c as int) % d as int) + r % c as int == r);
525 let k = x / (c as int * d as int);
526 lemma_fundamental_div_mod(x, c * d);
527 assert(x == (c * d) * (x / (c * d)) + x % (c * d));
528 assert(r == x - (c * d) * (x / (c * d)));
529 assert(r == x - (c * d) * k);
530 calc! {
531 (==)
532 c * ((x / c) % d) + x % c; {
533 broadcast use lemma_mul_is_commutative;
534
535 lemma_mod_multiples_vanish(-k, x / c, d);
536 }
537 c * ((x / c + (-k) * d) % d) + x % c; {
538 lemma_hoist_over_denominator(x, (-k) * d, c as nat);
539 }
540 c * (((x + (((-k) * d) * c)) / c) % d) + x % c; {
541 lemma_mul_is_associative(-k, d, c);
542 }
543 c * (((x + ((-k) * (d * c))) / c) % d) + x % c; {
544 lemma_mul_unary_negation(k, d * c);
545 }
546 c * (((x + (-(k * (d * c)))) / c) % d) + x % c; {
547 lemma_mul_is_associative(k, d, c);
548 }
549 c * (((x + (-(k * d * c))) / c) % d) + x % c; {}
550 c * (((x - k * d * c) / c) % d) + x % c; {
551 broadcast use {lemma_mul_is_associative, lemma_mul_is_commutative};
552
553 }
554 c * ((r / c) % d) + x % c; {}
555 c * (r / c) + x % c; {
556 lemma_fundamental_div_mod(r, c);
557 assert(r == c * (r / c) + r % c);
558 lemma_mod_mod(x, c, d);
559 assert(r % c == x % c);
560 }
561 r; {
562 broadcast use {group_mod_properties, lemma_mod_is_mod_recursive};
563
564 }
565 r % (c * d); {}
566 (x - (c * d) * k) % (c * d); {
567 lemma_mul_unary_negation(c * d, k);
568 }
569 (x + (c * d) * (-k)) % (c * d); {
570 lemma_mod_multiples_vanish(-k, x, c * d);
571 }
572 x % (c * d);
573 }
574 assert(c * (x / c) + x % c - r == c * (x / c) - c * ((x / c) % d) ==> x - r == c * (x / c) - c
575 * ((x / c) % d)) by {
576 lemma_fundamental_div_mod(x, c);
577 };
578 assert(c * (x / c) + x % c - r == c * (x / c) - c * ((x / c) % d));
579 assert(x - r == c * (x / c) - c * ((x / c) % d));
580 assert((x / c) / d == x / (c * d)) by {
581 lemma_fundamental_div_mod(x / c, d);
582 assert(d * ((x / c) / d) == x / c - ((x / c) % d));
583 lemma_fundamental_div_mod(x, c * d);
584 assert(x == (c * d) * (x / (c * d)) + (x % (c * d)));
585 lemma_mul_is_distributive_sub(c, x / c, (x / c) % d);
586 assert(c * (d * ((x / c) / d)) == c * (x / c) - c * ((x / c) % d));
587 lemma_mul_is_associative(c, d, (x / c) / d);
588 assert((c * d) * ((x / c) / d) == c * (x / c) - c * ((x / c) % d));
589 assert((c * d) * ((x / c) / d) == x - r);
590 assert((c * d) * ((x / c) / d) == (c * d) * (x / (c * d)));
591 lemma_mul_equality_converse(c * d, (x / c) / d, x / (c * d));
592 }
593 assert(c * d != 0) by {
594 assert(0 < c * d);
595 }
596}
597
598pub broadcast proof fn lemma_mul_hoist_inequality(x: int, y: int, z: int)
602 requires
603 0 <= x,
604 0 < z,
605 ensures
606 #![trigger (x * (y / z)), ((x * y) / z)]
607 x * (y / z) <= (x * y) / z,
608{
609 calc! {
610 (==)
611 (x * y) / z; (==) {
612 lemma_fundamental_div_mod(y, z);
613 }
614 (x * (z * (y / z) + y % z)) / z; (==) {
615 broadcast use group_mul_is_distributive;
616
617 }
618 (x * (z * (y / z)) + x * (y % z)) / z;
619 }
620 assert((x * (z * (y / z)) + x * (y % z)) / z >= x * (y / z)) by {
621 broadcast use {group_mod_properties, lemma_mul_is_associative, lemma_mul_is_commutative};
622
623 lemma_mul_nonnegative(x, y % z);
624 lemma_div_is_ordered(x * (z * (y / z)), x * (z * (y / z)) + x * (y % z), z);
625 lemma_div_multiples_vanish(x * (y / z), z);
626 };
627}
628
629pub broadcast proof fn lemma_indistinguishable_quotients(a: int, b: int, d: int)
637 requires
638 0 < d,
639 0 <= a - a % d <= b < a + d - a % d,
640 ensures
641 #![trigger (a / d), (b / d)]
642 a / d == b / d,
643{
644 lemma_div_induction_auto(
645 d,
646 a - b,
647 |ab: int|
648 {
649 let u = ab + b;
650 0 <= u - u % d <= b < u + d - u % d ==> u / d == b / d
651 },
652 );
653}
654
655pub proof fn lemma_truncate_middle(x: int, b: int, c: int)
659 requires
660 0 <= x,
661 0 < b,
662 0 < c,
663 ensures
664 #![trigger (b * (x % c))]
665 0 < b * c,
666 (b * x) % (b * c) == b * (x % c),
667{
668 broadcast use {lemma_mul_strictly_positive, lemma_mul_nonnegative};
669
670 calc! {
671 (==)
672 b * x; {
673 ModINL::lemma_fundamental_div_mod(b * x, b * c);
674 }
675 (b * c) * ((b * x) / (b * c)) + (b * x) % (b * c); {
676 lemma_div_denominator(b * x, b, c);
677 }
678 (b * c) * (((b * x) / b) / c) + (b * x) % (b * c); {
679 broadcast use lemma_mul_is_commutative;
680
681 lemma_div_by_multiple(x, b);
682 }
683 (b * c) * (x / c) + (b * x) % (b * c);
684 }
685 assert(b * x == (b * c) * (x / c) + b * (x % c)) by {
686 ModINL::lemma_fundamental_div_mod(x, c);
687 broadcast use {group_mul_is_distributive, lemma_mul_is_associative};
688
689 };
690}
691
692pub broadcast proof fn lemma_div_multiples_vanish_quotient(x: int, a: int, d: int)
696 requires
697 0 < x,
698 0 <= a,
699 0 < d,
700 ensures
701 #![trigger a / d, x * a, x * d]
702 0 < x * d,
703 a / d == (x * a) / (x * d),
704{
705 lemma_mul_strictly_positive(x, d);
706 calc! {
707 (==)
708 (x * a) / (x * d); {
709 lemma_mul_nonnegative(x, a);
710 lemma_div_denominator(x * a, x, d);
711 }
712 ((x * a) / x) / d; {
713 lemma_div_multiples_vanish(a, x);
714 }
715 a / d;
716 }
717}
718
719pub broadcast proof fn lemma_round_down(a: int, r: int, d: int)
722 requires
723 0 < d,
724 a % d == 0,
725 0 <= r < d,
726 ensures
727 #![trigger (d * ((a + r) / d))]
728 a == d * ((a + r) / d),
729{
730 broadcast use group_mul_properties_internal;
731
732 lemma_div_induction_auto(d, a, |u: int| u % d == 0 ==> u == d * ((u + r) / d));
733}
734
735pub broadcast proof fn lemma_div_multiples_vanish_fancy(x: int, b: int, d: int)
737 requires
738 0 < d,
739 0 <= b < d,
740 ensures
741 #![trigger (d * x + b) / d]
742 (d * x + b) / d == x,
743{
744 let f = |u: int| (d * u + b) / d == u;
745 assert(f(0)) by {
746 lemma_div_auto(d);
747 }
748 assert forall|i: int| i >= 0 && #[trigger] f(i) implies #[trigger] f(add1(i, 1)) by {
749 assert(d * (i + 1) + b == d * i + b + d) by {
750 assert(d * (i + 1) == d * i + d) by {
751 lemma_mul_is_distributive_add(d, i, 1);
752 lemma_mul_basics(d);
753 }
754 }
755 super::internals::div_internals::lemma_div_basics(d);
756 }
757 assert forall|i: int| i <= 0 && #[trigger] f(i) implies #[trigger] f(sub1(i, 1)) by {
758 assert(d * (i - 1) + b == d * i + b - d) by {
759 assert(d * (i - 1) == d * i - d) by {
760 lemma_mul_is_distributive_sub(d, i, 1);
761 lemma_mul_basics(d);
762 }
763 }
764 super::internals::div_internals::lemma_div_basics(d);
765 }
766 broadcast use group_mul_properties_internal;
767
768 lemma_mul_induction(f);
769 assert(f(x));
770}
771
772pub broadcast proof fn lemma_div_multiples_vanish(x: int, d: int)
776 requires
777 0 < d,
778 ensures
779 #![trigger (d * x) / d]
780 (d * x) / d == x,
781{
782 lemma_div_multiples_vanish_fancy(x, 0, d);
783}
784
785pub broadcast proof fn lemma_div_by_multiple(b: int, d: int)
789 requires
790 0 <= b,
791 0 < d,
792 ensures
793 #![trigger ((b * d) / d)]
794 (b * d) / d == b,
795{
796 lemma_div_multiples_vanish(b, d);
797 broadcast use group_mul_properties_internal;
798
799}
800
801pub broadcast proof fn lemma_div_by_multiple_is_strongly_ordered(x: int, y: int, m: int, z: int)
805 requires
806 x < y,
807 y == m * z,
808 0 < z,
809 ensures
810 #![trigger x / z, m * z, y / z]
811 x / z < y / z,
812{
813 lemma_mod_multiples_basic(m, z);
814 lemma_div_induction_auto(
815 z,
816 y - x,
817 |yx: int|
818 {
819 let u = yx + x;
820 x < u && u % z == 0 ==> x / z < u / z
821 },
822 );
823}
824
825pub broadcast proof fn lemma_multiply_divide_le(a: int, b: int, c: int)
830 requires
831 0 < b,
832 a <= b * c,
833 ensures
834 #![trigger a / b, b * c]
835 a / b <= c,
836{
837 lemma_mod_multiples_basic(c, b);
838 let f = |i: int| 0 <= i && (i + a) % b == 0 ==> a / b <= (i + a) / b;
839 lemma_div_induction_auto(b, b * c - a, f);
840 lemma_div_multiples_vanish(c, b);
841}
842
843pub broadcast proof fn lemma_multiply_divide_lt(a: int, b: int, c: int)
847 requires
848 0 < b,
849 a < b * c,
850 ensures
851 #![trigger a / b, b * c]
852 a / b < c,
853{
854 assert(((b * c - a) + a) % b == 0 ==> a / b < ((b * c - a) + a) / b) by {
855 let f = |i: int| 0 < i && (i + a) % b == 0 ==> a / b < (i + a) / b;
856 lemma_div_induction_auto(b, b * c - a, f);
857 }
858 assert(b * c == c * b) by {
859 lemma_mul_is_commutative(b, c);
860 }
861 assert((b * c) % b == 0) by {
862 lemma_mod_multiples_basic(c, b);
863 }
864 assert((b * c) / b == c) by {
865 lemma_div_multiples_vanish(c, b);
866 }
867}
868
869pub broadcast proof fn lemma_hoist_over_denominator(x: int, j: int, d: nat)
873 requires
874 0 < d,
875 ensures
876 #![trigger x / d as int + j]
877 x / d as int + j == (x + j * d) / d as int,
878{
879 let dd = d as int;
880 let q = x / dd;
881 let r = x % dd;
882 assert(x == dd * q + r) by {
883 lemma_fundamental_div_mod(x, dd);
884 }
885 assert(j * dd == dd * j) by {
886 lemma_mul_is_commutative(j, dd);
887 }
888 assert(x + j * dd == dd * (q + j) + r) by {
889 lemma_mul_is_distributive_add(dd, q, j);
890 }
891 assert((x + j * dd) / dd == q + j) by {
892 lemma_fundamental_div_mod_converse(x + j * d, dd, q + j, r);
893 }
894}
895
896pub broadcast proof fn lemma_part_bound1(a: int, b: int, c: int)
900 requires
901 0 <= a,
902 0 < b,
903 0 < c,
904 ensures
905 #![trigger (b * (a / b) % (b * c))]
906 0 < b * c,
907 (b * (a / b) % (b * c)) <= b * (c - 1),
908{
909 lemma_mul_strictly_positive(b, a / b);
910 lemma_mul_strictly_positive(b, c);
911 lemma_mul_strictly_positive(b, c - 1);
912 calc! {
913 (==)
914 b * (a / b) % (b * c); {
915 ModINL::lemma_fundamental_div_mod(b * (a / b), b * c);
916 }
917 b * (a / b) - (b * c) * ((b * (a / b)) / (b * c)); {
918 broadcast use lemma_mul_is_associative;
919
920 }
921 b * (a / b) - b * (c * ((b * (a / b)) / (b * c))); {
922 broadcast use group_mul_is_distributive;
923
924 }
925 b * ((a / b) - (c * ((b * (a / b)) / (b * c))));
926 }
927 assert(b * (a / b) % (b * c) <= b * (c - 1)) by {
928 broadcast use {lemma_mul_is_commutative, lemma_mul_inequality};
929
930 };
931}
932
933pub broadcast proof fn lemma_mod_is_mod_recursive(x: int, m: int)
941 requires
942 m > 0,
943 ensures
944 mod_recursive(x, m) == #[trigger] (x % m),
945 decreases
946 (if x < 0 {
947 -x + m
948 } else {
949 x
950 }),
951{
952 reveal(mod_recursive);
953 if x < 0 {
954 calc! {
955 (==)
956 mod_recursive(x, m); {}
957 mod_recursive(x + m, m); {
958 lemma_mod_is_mod_recursive(x + m, m);
959 }
960 (x + m) % m; {
961 lemma_add_mod_noop(x, m, m);
962 }
963 ((x % m) + (m % m)) % m; {
964 broadcast use {lemma_mod_self_0, lemma_mod_twice};
965
966 }
967 (x % m) % m; {
968 broadcast use {lemma_mod_self_0, lemma_mod_twice};
969
970 }
971 x % m;
972 }
973 } else if x < m {
974 lemma_small_mod(x as nat, m as nat);
975 } else {
976 calc! {
977 (==)
978 mod_recursive(x, m); {}
979 mod_recursive(x - m, m); {
980 lemma_mod_is_mod_recursive(x - m, m);
981 }
982 (x - m) % m; {
983 lemma_sub_mod_noop(x, m, m);
984 }
985 ((x % m) - (m % m)) % m; {
986 broadcast use {lemma_mod_self_0, lemma_mod_twice};
987
988 }
989 (x % m) % m; {
990 broadcast use {lemma_mod_self_0, lemma_mod_twice};
991
992 }
993 x % m;
994 }
995 }
996}
997
998pub broadcast proof fn lemma_mod_self_0(m: int)
1000 requires
1001 m > 0,
1002 ensures
1003 #[trigger] (m % m) == 0,
1004{
1005 lemma_mod_auto(m);
1006}
1007
1008pub broadcast proof fn lemma_mod_twice(x: int, m: int)
1010 requires
1011 m > 0,
1012 ensures
1013 #[trigger] ((x % m) % m) == x % m,
1014{
1015 lemma_mod_auto(m);
1016}
1017
1018pub broadcast group group_mod_basics {
1019 lemma_mod_self_0,
1020 lemma_mod_twice,
1021}
1022
1023pub broadcast proof fn lemma_mod_division_less_than_divisor(x: int, m: int)
1025 requires
1026 m > 0,
1027 ensures
1028 0 <= #[trigger] (x % m) < m,
1029{
1030 lemma_mod_auto(m);
1031}
1032
1033pub broadcast group group_mod_properties {
1034 group_mod_basics,
1035 lemma_mod_division_less_than_divisor,
1036}
1037
1038pub broadcast proof fn lemma_mod_decreases(x: nat, m: nat)
1041 requires
1042 0 < m,
1043 ensures
1044 #[trigger] (x % m) <= x,
1045{
1046 lemma_mod_auto(m as int);
1047}
1048
1049pub broadcast proof fn lemma_mod_is_zero(x: nat, m: nat)
1051 requires
1052 x > 0 && m > 0,
1053 #[trigger] (x % m) == 0,
1054 ensures
1055 x >= m,
1056{
1057 if (x < m) {
1058 lemma_small_mod(x, m);
1059 }
1060}
1061
1062#[verifier::spinoff_prover]
1065pub broadcast proof fn lemma_mod_multiples_basic(x: int, m: int)
1066 requires
1067 m > 0,
1068 ensures
1069 #[trigger] ((x * m) % m) == 0,
1070{
1071 lemma_mod_auto(m);
1072 broadcast use group_mul_properties_internal;
1073
1074 let f = |u: int| (u * m) % m == 0;
1075 lemma_mul_induction(f);
1076 assert(f(x));
1077}
1078
1079pub broadcast proof fn lemma_mod_add_multiples_vanish(b: int, m: int)
1082 requires
1083 0 < m,
1084 ensures
1085 (m + b) % m == #[trigger] (b % m),
1086{
1087 lemma_mod_auto(m);
1088}
1089
1090pub broadcast proof fn lemma_mod_sub_multiples_vanish(b: int, m: int)
1093 requires
1094 0 < m,
1095 ensures
1096 (-m + b) % m == #[trigger] (b % m),
1097{
1098 lemma_mod_auto(m);
1099}
1100
1101#[verifier::spinoff_prover]
1104pub broadcast proof fn lemma_mod_multiples_vanish(a: int, b: int, m: int)
1105 requires
1106 0 < m,
1107 ensures
1108 #[trigger] ((m * a + b) % m) == b % m,
1109 decreases
1110 (if a > 0 {
1111 a
1112 } else {
1113 -a
1114 }),
1115{
1116 lemma_mod_auto(m);
1117 broadcast use group_mul_properties_internal;
1118
1119 let f = |u: int| (m * u + b) % m == b % m;
1120 lemma_mul_induction(f);
1121 assert(f(a));
1122}
1123
1124pub broadcast proof fn lemma_mod_subtraction(x: nat, s: nat, d: nat)
1129 requires
1130 0 < d,
1131 0 <= s <= x % d,
1132 ensures
1133 #![trigger ((x - s) % d as int)]
1134 x % d - s % d == (x - s) % d as int,
1135{
1136 lemma_mod_auto(d as int);
1137}
1138
1139pub broadcast proof fn lemma_add_mod_noop(x: int, y: int, m: int)
1143 requires
1144 0 < m,
1145 ensures
1146 #![trigger (x + y) % m]
1147 ((x % m) + (y % m)) % m == (x + y) % m,
1148{
1149 lemma_mod_auto(m);
1150}
1151
1152pub broadcast proof fn lemma_add_mod_noop_right(x: int, y: int, m: int)
1156 requires
1157 0 < m,
1158 ensures
1159 #![trigger (x + y) % m]
1160 (x + (y % m)) % m == (x + y) % m,
1161{
1162 lemma_mod_auto(m);
1163}
1164
1165pub broadcast proof fn lemma_sub_mod_noop(x: int, y: int, m: int)
1169 requires
1170 0 < m,
1171 ensures
1172 #![trigger (x - y) % m]
1173 ((x % m) - (y % m)) % m == (x - y) % m,
1174{
1175 lemma_mod_auto(m);
1176}
1177
1178pub broadcast proof fn lemma_sub_mod_noop_right(x: int, y: int, m: int)
1182 requires
1183 0 < m,
1184 ensures
1185 #![trigger ((x - y) % m)]
1186 (x - (y % m)) % m == (x - y) % m,
1187{
1188 lemma_mod_auto(m);
1189}
1190
1191pub broadcast proof fn lemma_mod_adds(a: int, b: int, d: int)
1195 requires
1196 0 < d,
1197 ensures
1198 #![trigger ((a + b) % d)]
1199 a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d),
1200 (a % d + b % d) < d ==> a % d + b % d == (a + b) % d,
1201{
1202 broadcast use group_mul_properties_internal;
1203
1204 lemma_div_auto(d);
1205}
1206
1207#[verifier::spinoff_prover]
1211pub proof fn lemma_mod_neg_neg(x: int, d: int)
1212 requires
1213 0 < d,
1214 ensures
1215 x % d == (x * (1 - d)) % d,
1216{
1217 broadcast use group_mul_properties_internal;
1218
1219 assert((x - x * d) % d == x % d) by {
1220 let f = |i: int| (x - i * d) % d == x % d;
1221 assert(f(0) && (forall|i: int| i >= 0 && #[trigger] f(i) ==> #[trigger] f(add1(i, 1))) && (
1222 forall|i: int| i <= 0 && #[trigger] f(i) ==> #[trigger] f(sub1(i, 1)))) by {
1223 lemma_mod_auto(d);
1224 };
1225 lemma_mul_induction(f);
1226 assert(f(x));
1227 }
1228
1229}
1230
1231proof fn lemma_fundamental_div_mod_converse_helper_1(u: int, d: int, r: int)
1234 requires
1235 d != 0,
1236 0 <= r < d,
1237 ensures
1238 u == (u * d + r) / d,
1239 decreases
1240 if u >= 0 {
1241 u
1242 } else {
1243 -u
1244 },
1245{
1246 if u < 0 {
1247 lemma_fundamental_div_mod_converse_helper_1(u + 1, d, r);
1248 lemma_div_add_denominator(d, u * d + r);
1249 lemma_mul_is_distributive_add_other_way(d, u + 1, -1);
1250 assert(u == (u * d + r) / d);
1251 } else if u == 0 {
1252 DivINL::lemma_small_div();
1253 assert(u == 0 ==> u * d == 0) by (nonlinear_arith);
1254 assert(u == (u * d + r) / d);
1255 } else {
1256 lemma_fundamental_div_mod_converse_helper_1(u - 1, d, r);
1257 lemma_div_add_denominator(d, (u - 1) * d + r);
1258 lemma_mul_is_distributive_add_other_way(d, u - 1, 1);
1259 assert(u * d + r == (u - 1) * d + r + d);
1260 assert(u == (u * d + r) / d);
1261 }
1262}
1263
1264proof fn lemma_fundamental_div_mod_converse_helper_2(u: int, d: int, r: int)
1267 requires
1268 d != 0,
1269 0 <= r < d,
1270 ensures
1271 r == (u * d + r) % d,
1272 decreases
1273 if u >= 0 {
1274 u
1275 } else {
1276 -u
1277 },
1278{
1279 if u < 0 {
1280 lemma_fundamental_div_mod_converse_helper_2(u + 1, d, r);
1281 lemma_mod_add_multiples_vanish(u * d + r, d);
1282 lemma_mul_is_distributive_add_other_way(d, u + 1, -1);
1283 assert(u * d == (u + 1) * d + (-1) * d);
1284 assert(u * d + r == (u + 1) * d + r - d);
1285 assert(r == (u * d + r) % d);
1286 } else if u == 0 {
1287 assert(u == 0 ==> u * d == 0) by (nonlinear_arith);
1288 if d > 0 {
1289 lemma_small_mod(r as nat, d as nat);
1290 } else {
1291 lemma_small_mod(r as nat, (-d) as nat);
1292 }
1293 assert(r == (u * d + r) % d);
1294 } else {
1295 lemma_fundamental_div_mod_converse_helper_2(u - 1, d, r);
1296 lemma_mod_add_multiples_vanish((u - 1) * d + r, d);
1297 lemma_mul_is_distributive_add_other_way(d, u - 1, 1);
1298 assert(u * d + r == (u - 1) * d + r + d);
1299 assert(r == (u * d + r) % d);
1300 }
1301}
1302
1303pub broadcast proof fn lemma_fundamental_div_mod_converse_mod(x: int, d: int, q: int, r: int)
1307 requires
1308 d != 0,
1309 0 <= r < d,
1310 x == #[trigger] (q * d + r),
1311 ensures
1312 r == #[trigger] (x % d),
1313{
1314 lemma_fundamental_div_mod_converse_helper_1(q, d, r);
1315 assert(q == (q * d + r) / d);
1316 lemma_fundamental_div_mod_converse_helper_2(q, d, r);
1317}
1318
1319pub broadcast proof fn lemma_fundamental_div_mod_converse_div(x: int, d: int, q: int, r: int)
1323 requires
1324 d != 0,
1325 0 <= r < d,
1326 x == #[trigger] (q * d + r),
1327 ensures
1328 q == #[trigger] (x / d),
1329{
1330 lemma_fundamental_div_mod_converse_helper_1(q, d, r);
1331 assert(q == (q * d + r) / d);
1332 lemma_fundamental_div_mod_converse_helper_2(q, d, r);
1333}
1334
1335pub proof fn lemma_fundamental_div_mod_converse(x: int, d: int, q: int, r: int)
1339 requires
1340 d != 0,
1341 0 <= r < d,
1342 x == q * d + r,
1343 ensures
1344 r == x % d,
1345 q == x / d,
1346{
1347 lemma_fundamental_div_mod_converse_mod(x, d, q, r);
1348 lemma_fundamental_div_mod_converse_div(x, d, q, r);
1349}
1350
1351pub broadcast group group_fundamental_div_mod_converse {
1352 lemma_fundamental_div_mod_converse_mod,
1353 lemma_fundamental_div_mod_converse_div,
1354}
1355
1356pub broadcast proof fn lemma_mod_pos_bound(x: int, m: int)
1359 requires
1360 0 <= x,
1361 0 < m,
1362 ensures
1363 0 <= #[trigger] (x % m) < m,
1364{
1365 lemma_mod_auto(m);
1366}
1367
1368pub broadcast proof fn lemma_mod_bound(x: int, m: int)
1371 requires
1372 0 < m,
1373 ensures
1374 0 <= #[trigger] (x % m) < m,
1375{
1376 ModINL::lemma_mod_range(x, m);
1377}
1378
1379pub broadcast proof fn lemma_mul_mod_noop_left(x: int, y: int, m: int)
1382 requires
1383 0 < m,
1384 ensures
1385 (x % m) * y % m == #[trigger] (x * y % m),
1386{
1387 lemma_mod_auto(m);
1388 lemma_mul_induction_auto(y, |u: int| (x % m) * u % m == x * u % m);
1389}
1390
1391pub broadcast proof fn lemma_mul_mod_noop_right(x: int, y: int, m: int)
1394 requires
1395 0 < m,
1396 ensures
1397 x * (y % m) % m == #[trigger] ((x * y) % m),
1398{
1399 lemma_mod_auto(m);
1400 lemma_mul_induction_auto(x, |u: int| u * (y % m) % m == (u * y) % m);
1401}
1402
1403pub broadcast proof fn lemma_mul_mod_noop_general(x: int, y: int, m: int)
1407 requires
1408 0 < m,
1409 ensures
1410 ((x % m) * y) % m == (x * y) % m,
1411 (x * (y % m)) % m == (x * y) % m,
1412 ((x % m) * (y % m)) % m == #[trigger] ((x * y) % m),
1413{
1414 lemma_mul_mod_noop_left(x, y, m);
1415 lemma_mul_mod_noop_right(x, y, m);
1416 lemma_mul_mod_noop_right(x % m, y, m);
1417}
1418
1419pub broadcast proof fn lemma_mul_mod_noop(x: int, y: int, m: int)
1423 requires
1424 0 < m,
1425 ensures
1426 (x % m) * (y % m) % m == #[trigger] ((x * y) % m),
1427{
1428 lemma_mul_mod_noop_general(x, y, m);
1429}
1430
1431pub broadcast proof fn lemma_mod_equivalence(x: int, y: int, m: int)
1439 requires
1440 0 < m,
1441 ensures
1442 #![trigger (x - y) % m]
1443 x % m == y % m <==> (x - y) % m == 0,
1444{
1445 lemma_mod_auto(m);
1446}
1447
1448pub open spec fn is_mod_equivalent(x: int, y: int, m: int) -> bool
1451 recommends
1452 m > 0,
1453{
1454 x % m == y % m <==> (x - y) % m == 0
1455}
1456
1457pub broadcast proof fn lemma_mod_mul_equivalent(x: int, y: int, z: int, m: int)
1460 requires
1461 m > 0,
1462 is_mod_equivalent(x, y, m),
1463 ensures
1464 #[trigger] is_mod_equivalent(x * z, y * z, m),
1465{
1466 lemma_mul_mod_noop_left(x, z, m);
1467 lemma_mul_mod_noop_left(y, z, m);
1468 lemma_mod_equivalence(x, y, m);
1469 lemma_mod_equivalence(x * z, y * z, m);
1470}
1471
1472pub broadcast proof fn lemma_mod_ordering(x: int, k: int, d: int)
1476 requires
1477 1 < d,
1478 0 < k,
1479 ensures
1480 0 < d * k,
1481 x % d <= #[trigger] (x % (d * k)),
1482{
1483 lemma_mul_strictly_increases(d, k);
1484 calc! {
1485 (==)
1486 x % d + d * (x / d); {
1487 lemma_fundamental_div_mod(x, d);
1488 }
1489 x; {
1490 lemma_fundamental_div_mod(x, d * k);
1491 }
1492 x % (d * k) + (d * k) * (x / (d * k)); {
1493 broadcast use lemma_mul_is_associative;
1494
1495 }
1496 x % (d * k) + d * (k * (x / (d * k)));
1497 }
1498 calc! {
1499 (==)
1500 x % d; {
1501 broadcast use group_mod_properties;
1502
1503 }
1504 (x % d) % d; {
1505 lemma_mod_multiples_vanish(x / d - k * (x / (d * k)), x % d, d);
1506 }
1507 (x % d + d * (x / d - k * (x / (d * k)))) % d; {
1508 broadcast use lemma_mul_is_distributive_sub;
1509
1510 }
1511 (x % d + d * (x / d) - d * (k * (x / (d * k)))) % d; {}
1512 (x % (d * k)) % d;
1513 }
1514 assert((x % (d * k)) % d <= x % (d * k)) by {
1515 broadcast use group_mod_properties;
1516
1517 lemma_mod_decreases((x % (d * k)) as nat, d as nat);
1518 };
1519}
1520
1521pub broadcast proof fn lemma_mod_mod(x: int, a: int, b: int)
1525 requires
1526 0 < a,
1527 0 < b,
1528 ensures
1529 #![trigger (x % (a * b)) % a, x % a]
1530 0 < a * b,
1531 (x % (a * b)) % a == x % a,
1532{
1533 broadcast use lemma_mul_strictly_positive;
1534
1535 calc! {
1536 (==)
1537 x; {
1538 lemma_fundamental_div_mod(x, a * b);
1539 }
1540 (a * b) * (x / (a * b)) + x % (a * b); {
1541 broadcast use lemma_mul_is_associative;
1542
1543 }
1544 a * (b * (x / (a * b))) + x % (a * b); {
1545 lemma_fundamental_div_mod(x % (a * b), a);
1546 }
1547 a * (b * (x / (a * b))) + a * (x % (a * b) / a) + (x % (a * b)) % a; {
1548 broadcast use group_mul_is_distributive;
1549
1550 }
1551 a * (b * (x / (a * b)) + x % (a * b) / a) + (x % (a * b)) % a;
1552 }
1553 broadcast use {group_mod_properties, lemma_mul_is_commutative};
1554
1555 lemma_fundamental_div_mod_converse(
1556 x,
1557 a,
1558 b * (x / (a * b)) + x % (a * b) / a,
1559 (x % (a * b)) % a,
1560 );
1561}
1562
1563pub broadcast proof fn lemma_part_bound2(x: int, y: int, z: int)
1565 requires
1566 0 <= x,
1567 0 < y,
1568 0 < z,
1569 ensures
1570 y * z > 0,
1571 #[trigger] (x % y) % #[trigger] (y * z) < y,
1572{
1573 broadcast use {
1574 lemma_mul_strictly_positive,
1575 group_mod_properties,
1576 lemma_mul_is_commutative,
1577 lemma_mul_increases,
1578 };
1579
1580 assert(x % y < y);
1581 assert(y <= y * z);
1582 assert(0 <= x % y < y * z);
1583 lemma_small_mod((x % y) as nat, (y * z) as nat);
1584 assert((x % y) % (y * z) == x % y);
1585}
1586
1587pub broadcast proof fn lemma_mod_breakdown(x: int, y: int, z: int)
1590 requires
1591 0 <= x,
1592 0 < y,
1593 0 < z,
1594 ensures
1595 #![trigger x % (y * z)]
1596 y * z > 0,
1597 x % (y * z) == y * ((x / y) % z) + x % y,
1598{
1599 broadcast use lemma_mul_strictly_positive;
1600
1601 lemma_div_pos_is_pos(x, y);
1602 assert(0 <= x / y);
1603 assert((y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z) by {
1604 lemma_part_bound1(x, y, z);
1605 lemma_part_bound2(x, y, z);
1606 broadcast use {group_mul_basics, group_mul_is_distributive};
1607
1608 };
1609 calc! {
1610 (==)
1611 x % (y * z); {
1612 lemma_fundamental_div_mod(x, y);
1613 }
1614 (y * (x / y) + x % y) % (y * z); {
1615 broadcast use group_mod_properties;
1616
1617 assert(0 <= x % y);
1618 lemma_mul_nonnegative(y, x / y);
1619 assert((y * (x / y)) % (y * z) + (x % y) % (y * z) < y * z);
1620 lemma_mod_adds(y * (x / y), x % y, y * z);
1621 }
1622 (y * (x / y)) % (y * z) + (x % y) % (y * z); {
1623 broadcast use {group_mod_properties, lemma_mul_is_commutative};
1624
1625 lemma_mul_increases(z, y);
1626 assert(x % y < y && y <= y * z);
1627 lemma_small_mod((x % y) as nat, (y * z) as nat);
1628 assert((x % y) % (y * z) == x % y);
1629 }
1630 (y * (x / y)) % (y * z) + x % y; {
1631 lemma_truncate_middle(x / y, y, z);
1632 }
1633 y * ((x / y) % z) + x % y;
1634 }
1635}
1636
1637}