vstd/arithmetic/internals/
mod_internals.rs

1//! This file contains proofs related to modulo. These are internal
2//! functions used within the math standard library.
3//!
4//! It's based on the following file from the Dafny math standard library:
5//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternals.dfy`.
6//! That file has the following copyright notice:
7//! /*******************************************************************************
8//! *  Original: Copyright (c) Microsoft Corporation
9//! *  SPDX-License-Identifier: MIT
10//! *
11//! *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
12//! *  SPDX-License-Identifier: MIT
13//! *******************************************************************************/
14#[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/// This function performs the modulus operation recursively.
37#[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
58/// This utility function helps prove a mathematical property by
59/// induction. The caller supplies an integer predicate, proves the
60/// predicate holds in certain base cases, and proves correctness of
61/// inductive steps both upward and downward from the base cases. This
62/// lemma invokes induction to establish that the predicate holds for
63/// all possible inputs.
64///
65/// `f`: The integer predicate
66///
67/// `n`: Upper bound on the base cases. Specifically, the caller
68/// establishes `f(i)` for every value `i` satisfying `0 <= i < n`.
69///
70/// To prove inductive steps upward from the base cases, the caller
71/// must establish that, for any `i >= 0`, `f(i) ==> f(add1(i, n))`.
72/// `add1(i, n)` is just `i + n`, but written in a functional style
73/// so that it can be used where functional triggers are required.
74///
75/// To prove inductive steps downward from the base cases, the caller
76/// must establish that, for any `i < n`, `f(i) ==> f(sub1(i, n))`.
77/// `sub1(i, n)` is just `i - n`, but written in a functional style
78/// so that it can be used where functional triggers are required.
79pub 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
93/// This utility function helps prove a mathematical property of a
94/// pair of integers by induction. The caller supplies a predicate
95/// over a pair of integers, proves the predicate holds in certain
96/// base cases, and proves correctness of inductive steps both upward
97/// and downward from the base cases. This lemma invokes induction to
98/// establish that the predicate holds for all possible inputs.
99///
100/// `f`: The integer predicate
101///
102/// `n`: Upper bound on the base cases. Specifically, the caller
103/// establishes `f(i, j)` for every pair of values `i, j` satisfying
104/// `0 <= i < n` and `0 <= j < n`.
105///
106/// To prove inductive steps from the base cases, the caller must
107/// establish that:
108///
109/// 1) For any `i >= 0`, `f(i, j) ==> f(add1(i, n), j)`. `add1(i, n)`
110/// is just `i + n`, but written in a functional style so that it can
111/// be used where functional triggers are required.
112///
113/// 2) For any `j >= 0`, `f(i, j) ==> f(i, add1(j, n))`
114///
115/// 3) For any `i < n`, `f(i) ==> f(sub1(i, n))`. `sub1(i, n)` is just
116/// `i - n`, but written in a functional style so that it can be used
117/// where functional triggers are required.
118///
119/// 4) For any `j < n`, `f(j) ==> f(i, sub1(j, n))`.
120pub 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/// Proof that when dividing, adding the denominator to the numerator
144/// increases the result by 1. Specifically, for the given `n` and `x`,
145/// `(x + n) / n == x / n + 1`.
146#[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
168/// Proof that when dividing, subtracting the denominator from the numerator
169/// decreases the result by 1. Specifically, for the given `n` and `x`,
170/// `(x - n) / n == x / n - 1`.
171pub 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/// Proof that when dividing, adding the denominator to the numerator
193/// doesn't change the remainder. Specifically, for the given `n` and
194/// `x`, `(x + n) % n == x % n`.
195#[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
225/// Proof that when dividing, subtracting the denominator from the
226/// numerator doesn't change the remainder. Specifically, for the
227/// given `n` and `x`, `(x - n) % n == x % n`.
228pub 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;  // OBSERVE
238
239    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
251/// Proof that for the given `n` and `x`, `x % n == x` if and only if
252/// `0 <= x < n`.
253pub 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
267/// Proof of basic properties of the division given the divisor `n`:
268///
269/// 1) Adding the denominator to the numerator increases the quotient
270/// by 1 and doesn't change the remainder.
271///
272/// 2) Subtracting the denominator from the numerator decreases the
273/// quotient by 1 and doesn't change the remainder.
274///
275/// 3) The numerator is the same as the result if and only if the
276/// numerator is in the half-open range `[0, n)`.
277pub 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
305/// Proof that if `x == q * r + n` and `0 <= r < n`, then `q == x / n`
306/// and `r == x % n`. Essentially, this is the converse of the
307/// fundamental theorem of division and modulo.
308pub 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
342/// This function says that for any `x` and `y`, there are two
343/// possibilities for the sum `x % n + y % n`: (1) It's in the range
344/// `[0, n)` and it's equal to `(x + y) % n`. (2) It's in the range
345/// `[n, n + n)` and it's equal to `(x + y) % n + n`.
346pub 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
358/// This function says that for any `x` and `y`, there are two
359/// possibilities for the difference `x % n - y % n`: (1) It's in the
360/// range `[0, n)` and it's equal to `(x - y) % n`. (2) It's in the
361/// range `[-n, 0)` and it's equal to `(x + y) % n - n`.
362pub 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
374/// This function states various useful properties about the modulo
375/// operator when the divisor is `n`.
376pub 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
387/// Proof of `mod_auto(n)`, which states various useful properties
388/// about the modulo operator when the divisor is the positive number
389/// `n`
390pub 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 {  // xr - yr < 0
436            lemma_quotient_and_remainder(x - y, xq - yq - 1, xr - yr + n, n);
437        }
438    }
439}
440
441/// This utility function helps prove a mathematical property by
442/// induction. The caller supplies an integer predicate, proves the
443/// predicate holds in certain base cases, and proves correctness of
444/// inductive steps both upward and downward from the base cases. This
445/// lemma invokes induction to establish that the predicate holds for
446/// the given arbitrary input `x`.
447///
448/// `f`: The integer predicate
449///
450/// `n`: Upper bound on the base cases. Specifically, the caller
451/// establishes `f(i)` for every value `i` satisfying `is_le(0, i) &&
452/// i < n`.
453///
454/// `x`: The desired case established by this lemma. Its postcondition
455/// thus includes `f(x)`.
456///
457/// To prove inductive steps upward from the base cases, the caller
458/// must establish that, for any `i`, `is_le(0, i) && f(i) ==> f(i +
459/// n)`. `is_le(0, i)` is just `0 <= i`, but written in a functional
460/// style so that it can be used where functional triggers are
461/// required.
462///
463/// To prove inductive steps downward from the base cases, the caller
464/// must establish that, for any `i`, `is_le(i + 1, n) && f(i) ==> f(i
465/// - n)`. `is_le(i + 1, n)` is just `i + 1 <= n`, but written in a
466/// functional style so that it can be used where functional triggers
467/// are required.
468pub 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
491/// This utility function helps prove a mathematical property by
492/// induction. The caller supplies an integer predicate, proves the
493/// predicate holds in certain base cases, and proves correctness of
494/// inductive steps both upward and downward from the base cases. This
495/// lemma invokes induction to establish that the predicate holds for
496/// all integer values.
497///
498/// `f`: The integer predicate
499///
500/// `n`: Upper bound on the base cases. Specifically, the caller
501/// establishes `f(i)` for every value `i` satisfying `is_le(0, i) &&
502/// i < n`.
503///
504/// To prove inductive steps upward from the base cases, the caller
505/// must establish that, for any `i`, `is_le(0, i) && f(i) ==> f(i +
506/// n)`. `is_le(0, i)` is just `0 <= i`, but written in a functional
507/// style so that it can be used where functional triggers are
508/// required.
509///
510/// To prove inductive steps downward from the base cases, the caller
511/// must establish that, for any `i`, `is_le(i + 1, n) && f(i) ==> f(i
512/// - n)`. `is_le(i + 1, n)` is just `i + 1 <= n`, but written in a
513/// functional style so that it can be used where functional triggers
514/// are required.
515pub 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} // verus!