vstd/arithmetic/
div_mod.rs

1//! This file contains proofs related to integer division (`/`) and
2//! remainder aka mod (`%`). These are part of the math standard library.
3//!
4//! It's based on the following file from the Dafny math standard
5//! library:
6//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy`.
7//! That file has the following copyright notice:
8//! /*******************************************************************************
9//! * Original: Copyright (c) Microsoft Corporation *
10//! SPDX-License-Identifier: MIT * * Modifications and Extensions:
11//! Copyright by the contributors to the Dafny Project *
12//! SPDX-License-Identifier: MIT
13//! *******************************************************************************/
14use 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
49/*****************************************************************************
50* Division
51*****************************************************************************/
52
53/// Proof that, for the case of `x / d`, division using `/` is
54/// equivalent to a recursive definition of division.
55pub 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
66/// Proof that the quotient of an integer divided by itself is 1,
67/// specifically that `d / d == 1`.
68pub 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
77/// Proof that 0 divided by a nonzero integer is 0, specifically `0 / d == 0`.
78pub 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
87/// Proof establishing basic properties of division using `x`: 0
88/// divided by `x` is 0; `x` divided by 1 is itself; and `x` divided
89/// by itself is 1.
90pub 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
102/// Proof for basic property that 0 divided by `x` is 0.
103pub 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
110/// Proof for basic property that `x` divided by 1 is `x`.
111pub broadcast proof fn lemma_div_basics_2(x: int)
112    ensures
113        #[trigger] (x / 1) == x,
114{
115    lemma_div_basics(x);
116}
117
118/// Proof for basic property that `x` divided by `x` is 1.
119pub 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
126/// Proof that dividing any non-negative integer by a positive integer is non-zero.
127pub 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
133/// Proof that the quotient produced by dividing any non-negative integer `x`
134/// by a positive integer `y` is at most `x`.
135pub 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
153/// Proof that if a dividend is a whole number, the divisor is a
154/// natural number, and their quotient is 0, then the dividend is
155/// smaller than the divisor.
156pub 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
165/// Proof that division of a positive integer by a positive integer
166/// less than or equal to it is nonzero. Specifically,
167/// given that `x >= d`, we can conclude that `x / d > 0`.
168pub 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
182/// Proof that given two fractions with the same numerator, the order
183/// of the fractions is determined by the denominators. However, if
184/// the numerator is 0, the fractions are equal regardless of the
185/// denominators' values. Specifically, given that `1 <= y <= z`, we
186/// know `x / y >= x / z`.
187pub 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
211/// Proof that a number gets strictly smaller when divided by a number
212/// greater than one. Specifically, `x / d < x`.
213pub 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
224/// Proof that, given `r == a % d + b % d - (a + b) % d`, `r` can also
225/// be expressed as `d * ((a + b) / d) - d * (a / d) - d * (b / d)`.
226pub 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
239/// Proof that dividing a whole number by a natural number will result
240/// in a quotient that is greater than or equal to 0. Specifically,
241/// `x / d >= 0`.
242pub 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
258/// Proof that dividing a number then adding 1 gives the same result
259/// as adding the divisor and then doing the division. Specifically,
260/// `1 + (x / d)` is equal to `(d + x) / d`.
261pub 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
271/// Proof that dividing a number then subtracting 1 gives the same result
272/// as subtracting the divisor and then doing the division. Specifically,
273/// `-1 + (x / d)` is equal to `(-d + x) / d`.
274pub 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
284/// Proof that dividing any non-negative integer less than `d` by `d`
285/// produces a quotient of 0.
286pub 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
295/// Proof that dividing any non-negative integer by a larger integer
296/// produces a quotient of 0.
297pub 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
306/// Proof that numerical order is preserved when dividing two seperate
307/// integers by a common positive divisor. Specifically, given that
308/// `z > 0` and `x <= y`, we know `x / z <= y / z`.
309pub 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
335/// Proof that dividing an integer by 2 or more results in a quotient
336/// that is smaller than the original dividend. Specifically, `x / d < x`.
337pub 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
347/// Proof that dividing an integer by 1 or more results in a quotient
348/// that is less than or equal to the original dividend. Specifically,
349/// `x / d <= x`.
350pub 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
360/// Proof that a natural number x divided by a larger natural number
361/// gives a remainder equal to x. Specifically, because `x < m`, we
362/// know `x % m == x`.
363pub 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
373/// The remainder of a nonnegative integer `x` divided by the product of two positive integers
374/// `y` and `z` is equivalent to dividing `x` by `y`, dividing the quotient by `z`, multiplying
375/// the remainder by `y`, and then adding the product to the remainder of `x` divided by `y`.
376/// In mathematical terms, `(x % (y * z)) == y * ((x / y) % z) + x % y`.
377pub 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            // comparison op can't be chained in calc!
427            // assert forall is also not avaialable in calc!
428            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
439/// Proof that the difference between a nonnegative integer `x` and a
440/// positive integer `d` must be strictly less than the quotient of
441/// `x` divided by `d` and then multiplied by `d`.
442pub 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
455/// Proof that the division of a nonnegative integer `x` by a positive
456/// integer `d` multiplied by `d` is less than or equal to the value
457/// of `x`.
458pub 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
470/// Proof that the difference between a nonnegative integer `x` and
471/// the division of `x` by a positive integer `d` multiplied by `d` is
472/// lower bounded (inclusively) by 0 and upper bounded (exclusively)
473/// by `d`.
474pub 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
486/// Proof of the fundamental theorem of division and modulo, namely
487/// that `x` can be expressed as `d` times the quotient `x / d` plus
488/// the remainder `x % d`.
489pub 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
500/// Proof that dividing `x` by `c * d` is equivalent to first dividing
501/// `x` by `c` and then dividing the result by `d`.
502pub 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
598/// Proof that multiplying an integer by a fraction is equivalent to
599/// multiplying the fraction's numerator by the integer. Specifically,
600/// `x * (y / z) == (x * y) / z`.
601pub 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
629/// Proof that for a positive integer `d`, if `a - a % d` is less than
630/// or equal to `b` and `b` is less than `a + d - a % d`, then the
631/// quotient of `a` divided by `d` is equivalent to the quotient of
632/// `b` divided by `d`.
633///
634/// In other words, if `a` and `b` occur between the same two
635/// multiples of `d`, then their quotient with `d` is equivalent.
636pub 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
655/// Proof that common factors from the dividend and divisor of a
656/// modulus operation can be factored out. Specifically,
657/// `(b * x) % (b * c) == b * (x % c)`.
658pub 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
692/// Proof that multiplying the numerator and denominator by an integer
693/// does not change the quotient. Specifically,
694/// `a / d == (x * a) / (x * d)`.
695pub 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
719/// Proof that, since `a % d == 0` and `0 <= r < d`, we can conclude
720/// `a == d * (a + r) / d`.
721pub 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
735/// Proof that, since `0 <= b < d`, we have `(d * x + b) / d == x`.
736pub 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
772/// Proof that multiplying an integer by a common numerator and
773/// denominator results in the original integer. Specifically,
774/// `(d * x) / d == x`.
775pub 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
785/// Proof that multiplying a whole number by a common numerator and
786/// denominator results in the original integer. Specifically,
787/// `(b * d) / d == b`.
788pub 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
801/// Proof that a dividend that is a positive multiple of a divisor
802/// will always yield a greater quotient than a smaller dividend.
803/// Specifically, `x / z < y / z` because `y == m * z` and `x < y`.
804pub 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
825/// Proof that if an integer is less than or equal to the product of
826/// two other integers, then the quotient with one of them will be
827/// less than or equal to the other of them. Specifically, because
828/// `a <= b * c`, we know `a / b <= c`.
829pub 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
843/// Proof that if an integer is less than the product of two other
844/// integers, then the quotient with one of them will be less than the
845/// other. Specifically, because `a < b * c`, we know `a / b < c`.
846pub 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
869/// Proof that adding an integer to a fraction is equivalent to adding
870/// that integer times the denominator to the numerator. Specifically,
871/// `x / d + j == (x + j * d) / d`.
872pub 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
896/// Proof that, for nonnegative integer `a` and positive integers `b` and `c`,
897/// the remainder of `b * (a / b)` divided by `b * c` is less than or equal to `b * (c - 1)`.
898/// This accounts for the rounding down that occurs in integer division.
899pub 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
933/*******************************************************************************
934* Modulus
935*******************************************************************************/
936
937/// Proof that computing the modulus using `%` is equivalent to
938/// computing it with a recursive definition of modulus. Specifically,
939/// `x % m` is equivalent in that way.
940pub 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
998/// Proof that any integer divided by itself produces a remainder of 0.
999pub 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
1008/// Proof that performing `(x % m) % m` gives the same result as simply perfoming `x % m`.
1009pub 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
1023/// Proof that the remainder of any division will be less than the divisor's value.
1024pub 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
1038/// Proof that when natural number `x` is divided by natural number
1039/// `m`, the remainder will be less than or equal to `x`.
1040pub 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
1049/// Proof that if `x % m` is zero and `x` is positive, then `x >= m`.
1050pub 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/// Proof that multiplying by a number then dividing by that same
1063/// number produces a remainder of 0. Specifically, `(x * m) % m == 0`.
1064#[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
1079/// Proof that adding the divisor to the dividend doesn't change the
1080/// remainder. Specifically, `(m + b) % m == b % m`.
1081pub 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
1090/// Proof that subtracting the divisor from the dividend doesn't
1091/// change the remainder. Specifically, `(-m + b) % m == b % m`.
1092pub 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/// Proof that adding any multiple of the divisor to the dividend will produce the
1102/// same remainder. In other words, `(m * a + b) % m == b % m`.
1103#[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
1124/// Proof that modulo distributes over subtraction if the subtracted value is
1125/// less than or equal to the modulo of the number it's being subtracted from.
1126/// Specifically, because `0 <= s <= x % d`, we can conclude that
1127/// `x % d - s % d == (x - s) % d`.
1128pub 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
1139/// Proof that modulo distributes over addition, provided you do an
1140/// extra modulo after adding the remainders. Specifically,
1141/// `((x % m) + (y % m)) % m == (x + y) % m`.
1142pub 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
1152/// Proof that describes an expanded and succinct version of modulus
1153/// operator in relation to addition. Specifically,
1154/// `(x + (y % m)) % m == (x + y) % m`.
1155pub 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
1165/// Proof that modulo distributes over subtraction provided you do an
1166/// extra modulo operation after subtracting the remainders.
1167/// Specifically, `((x % m) - (y % m)) % m == (x - y) % m`.
1168pub 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
1178/// Proof that describes an expanded and succinct version of modulus
1179/// operator in relation to subtraction. Specifically,
1180/// `(x - (y % m)) % m == (x - y) % m`.
1181pub 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
1191/// Proof of two properties of the sum of two remainders with the same dividend:
1192/// 1) `a % d + b % d == (a + b) % d + d * ((a % d + b % d) / d)`.
1193/// 2) `(a % d + b % d) < d ==> a % d + b % d == (a + b) % d`.
1194pub 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/// Proof that the remainder when dividing integer `x` by positive
1208/// integer `d` is equivalent to the remainder of `x * (1 - d)` by
1209/// `d`.
1210#[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
1231/// This proof isn't exported from this module. It's just used in
1232/// the proof of [`lemma_fundamental_div_mod_converse`].
1233proof 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
1264/// This proof isn't exported from this module. It's just used in
1265/// the proof of [`lemma_fundamental_div_mod_converse`].
1266proof 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
1303/// Proof of the converse of the fundamental property of division and modulo.
1304/// Specifically, if we know `0 <= r < d` and `x == q * d + r`, then we
1305/// know that `r` is the remainder `x % d`.
1306pub 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
1319/// Proof of the converse of the fundamental property of division and modulo.
1320/// Specifically, if we know `0 <= r < d` and `x == q * d + r`, then we
1321/// know that `q` is the quotient `x / d`.
1322pub 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
1335/// Proof of the converse of the fundamental property of division and modulo.
1336/// Specifically, if we know `0 <= r < d` and `x == q * d + r`, then we
1337/// know that `q` is the quotient `x / d` and `r` is the remainder `x % d`.
1338pub 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
1356/// Proof that the remainder, when natural number `x` is divided by
1357/// positive integer `m`, is less than `m`.
1358pub 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
1368/// Proof that when integer `x` is divided by positive integer `m`,
1369/// the remainder is nonegative and less than `m`.
1370pub 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
1379/// Proof that the remainder when `x * y` is divided by `m` is
1380/// equivalent to the remainder when `(x % m) * y` is divided by `m`.
1381pub 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
1391/// Proof that the remainder when `x * y` is divided by `m` is
1392/// equivalent to the remainder when `x * (y % m)` is divided by `m`.
1393pub 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
1403/// Proof of various properties about modulo equivalence with respect
1404/// to multiplication, specifically various expressions that `(x * y)
1405/// % m` is equivalent to.
1406pub 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
1419/// Proof that modulo distributes over multiplication, provided you do
1420/// an extra modulo operation after multiplying the remainders. Specifically,
1421/// `(x % m) * (y % m) % m == (x * y) % m`.
1422pub 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
1431/// Proof that `x` and `y` are congruent modulo `m` if and only if `x
1432/// - y` is congruent to 0 modulo `m`. In other words, `x % m == y % m
1433/// <==> (x - y) % m == 0`.
1434///
1435/// Note: The Dafny standard library uses the triggers `x % m, y % m`
1436/// for the broadcasted forall quantifier. But this can lead to a trigger loop,
1437/// so we don't do that here.
1438pub 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
1448/// This function says that `x` is congruent to `y` modulo `m` if and
1449/// only if their difference `x - y` is congruent to 0 modulo `m`.
1450pub 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
1457/// Proof that if `is_mod_equivalent` holds for `x`, `y`, and `m`,
1458/// then it holds for `x * z`, `y * z`, and `m`.
1459pub 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
1472/// Proof that multiplying the divisor by a positive number can't
1473/// decrease the remainder. Specifically, because `k > 0`, we have
1474/// `x % d <= x % (d * k)`.
1475pub 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
1521/// Proof that the remainder when `x` is divided by `a * b`, taken
1522/// modulo `a`, is equivalent to `x` modulo `a`. That is,
1523/// `(x % (a * b)) % a == x % a`.
1524pub 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
1563/// Proof that `(x % y) % (y * z) < y`.
1564pub 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
1587/// Proof of the validity of an expanded form of the modulus operation.
1588/// Specifically, `x % (y * z) == y * ((x / y) % z) + x % y`.
1589pub 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} // verus!