vstd/arithmetic/internals/
div_internals.rs

1//! This file contains proofs related to division. 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/DivInternals.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
19#[cfg(verus_keep_ghost)]
20use super::super::super::arithmetic::internals::general_internals::is_le;
21#[cfg(verus_keep_ghost)]
22use super::super::super::arithmetic::internals::mod_internals::{
23    lemma_mod_induction_forall,
24    lemma_mod_induction_forall2,
25    mod_auto,
26    lemma_mod_auto,
27    lemma_mod_basics,
28};
29use super::super::super::arithmetic::internals::mod_internals_nonlinear;
30#[cfg(verus_keep_ghost)]
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 recursively computes the quotient resulting from
37/// dividing two numbers `x` and `d`, in the case where `d > 0`
38#[verifier::opaque]
39pub open spec fn div_pos(x: int, d: int) -> int
40    recommends
41        d > 0,
42    decreases
43            (if x < 0 {
44                d - x
45            } else {
46                x
47            }),
48    when d > 0
49{
50    if x < 0 {
51        -1 + div_pos(x + d, d)
52    } else if x < d {
53        0
54    } else {
55        1 + div_pos(x - d, d)
56    }
57}
58
59/// This function recursively computes the quotient resulting from
60/// dividing two numbers `x` and `d`. It's only meaningful when `d !=
61/// 0`, of course.
62#[verifier::opaque]
63pub open spec fn div_recursive(x: int, d: int) -> int
64    recommends
65        d != 0,
66{
67    // reveal(div_pos);
68    if d > 0 {
69        div_pos(x, d)
70    } else {
71        -1 * div_pos(x, -1 * d)
72    }
73}
74
75/// Proof of basic properties of integer division when the divisor is
76/// the given positive integer `n`
77pub proof fn lemma_div_basics(n: int)
78    requires
79        n > 0,
80    ensures
81        (n / n) == 1 && -((-n) / n) == 1,
82        forall|x: int| 0 <= x < n <==> #[trigger] (x / n) == 0,
83        forall|x: int| #[trigger] ((x + n) / n) == x / n + 1,
84        forall|x: int| #[trigger] ((x - n) / n) == x / n - 1,
85{
86    lemma_mod_auto(n);
87    lemma_mod_basics(n);
88    div_internals_nonlinear::lemma_small_div();
89    div_internals_nonlinear::lemma_div_by_self(n);
90    assert forall|x: int| #[trigger] (x / n) == 0 implies 0 <= x < n by {
91        mod_internals_nonlinear::lemma_fundamental_div_mod(x, n);
92    }
93}
94
95/// This function says that for any `x` and `y`, there are two
96/// possibilities for the sum `x % n + y % n`: (1) It's in the range
97/// `[0, n)` and `(x + y) / n == x / n + y / n`. (2) It's in the range
98/// `[n, n + n)` and `(x + y) / n = x / n + y / n + 1`.
99pub open spec fn div_auto_plus(n: int) -> bool {
100    forall|x: int, y: int|
101        #![trigger ((x + y) / n)]
102        {
103            let z = (x % n) + (y % n);
104            ((0 <= z < n && ((x + y) / n) == x / n + y / n) || (n <= z < n + n && ((x + y) / n) == x
105                / n + y / n + 1))
106        }
107}
108
109/// This function says that for any `x` and `y`, there are two
110/// possibilities for the difference `x % n - y % n`: (1) It's in the
111/// range `[0, n)` and `(x - y) / n == x / n - y / n`. (2) It's in the
112/// range `[-n, 0)` and `(x - y) / n = x / n - y / n - 1`.
113pub open spec fn div_auto_minus(n: int) -> bool {
114    forall|x: int, y: int|
115        #![trigger ((x - y) / n)]
116        {
117            let z = (x % n) - (y % n);
118            ((0 <= z < n && ((x - y) / n) == x / n - y / n) || (-n <= z < 0 && ((x - y) / n) == x
119                / n - y / n - 1))
120        }
121}
122
123/// This function states various properties of integer division when
124/// the denominator is `n`, including the identity property, a fact
125/// about when quotients are zero, and facts about adding and
126/// subtracting integers over this common denominator
127pub open spec fn div_auto(n: int) -> bool
128    recommends
129        n > 0,
130{
131    &&& mod_auto(n)
132    &&& (n / n == -((-n) / n) == 1)
133    &&& forall|x: int| 0 <= x < n <==> #[trigger] (x / n) == 0
134    &&& div_auto_plus(n)
135    &&& div_auto_minus(n)
136}
137
138/// Proof of `div_auto_plus(n)`, not exported publicly because it's
139/// just used as part of [`lemma_div_auto`] to prove `div_auto(n)`
140proof fn lemma_div_auto_plus(n: int)
141    requires
142        n > 0,
143    ensures
144        div_auto_plus(n),
145{
146    lemma_mod_auto(n);
147    lemma_div_basics(n);
148    assert forall|x: int, y: int|
149        {
150            let z = (x % n) + (y % n);
151            ((0 <= z < n && #[trigger] ((x + y) / n) == x / n + y / n) || (n <= z < n + n && ((x
152                + y) / n) == x / n + y / n + 1))
153        } by {
154        let f = |xx: int, yy: int|
155            {
156                let z = (xx % n) + (yy % n);
157                ((0 <= z < n && ((xx + yy) / n) == xx / n + yy / n) || (n <= z < 2 * n && ((xx + yy)
158                    / n) == xx / n + yy / n + 1))
159            };
160        assert forall|i: int, j: int|
161            {
162                // changing this from j + n to mod's addition speeds up the verification
163                // otherwise you need higher rlimit
164                // might be a good case for profilers
165                &&& (j >= 0 && #[trigger] f(i, j) ==> f(i, add1(j, n)))
166                &&& (i < n && f(i, j) ==> f(i - n, j))
167                &&& (j < n && f(i, j) ==> f(i, j - n))
168                &&& (i >= 0 && f(i, j) ==> f(i + n, j))
169            } by {
170            assert(((i + n) + j) / n == ((i + j) + n) / n);
171            assert((i + (j + n)) / n == ((i + j) + n) / n);
172            assert(((i - n) + j) / n == ((i + j) - n) / n);
173            assert((i + (j - n)) / n == ((i + j) - n) / n);
174        }
175        assert forall|i: int, j: int| 0 <= i < n && 0 <= j < n implies #[trigger] f(i, j) by {
176            assert(((i + n) + j) / n == ((i + j) + n) / n);
177            assert((i + (j + n)) / n == ((i + j) + n) / n);
178            assert(((i - n) + j) / n == ((i + j) - n) / n);
179            assert((i + (j - n)) / n == ((i + j) - n) / n);
180        }
181        lemma_mod_induction_forall2(n, f);
182        assert(f(x, y));
183    }
184}
185
186/// Proof of `div_auto_mius(n)`, not exported publicly because it's
187/// just used as part of [`lemma_div_auto`] to prove `div_auto(n)`
188#[verifier::spinoff_prover]
189proof fn lemma_div_auto_minus(n: int)
190    requires
191        n > 0,
192    ensures
193        div_auto_minus(n),
194{
195    lemma_mod_auto(n);
196    lemma_div_basics(n);
197    assert forall|x: int, y: int|
198        {
199            let z = (x % n) - (y % n);
200            ((0 <= z < n && #[trigger] ((x - y) / n) == x / n - y / n) || (-n <= z < 0 && ((x - y)
201                / n) == x / n - y / n - 1))
202        } by {
203        let f = |xx: int, yy: int|
204            {
205                let z = (xx % n) - (yy % n);
206                ((0 <= z < n && ((xx - yy) / n) == xx / n - yy / n) || (-n <= z < 0 && (xx - yy) / n
207                    == xx / n - yy / n - 1))
208            };
209        assert forall|i: int, j: int|
210            {
211                &&& (j >= 0 && #[trigger] f(i, j) ==> f(i, add1(j, n)))
212                &&& (i < n && f(i, j) ==> f(sub1(i, n), j))
213                &&& (j < n && f(i, j) ==> f(i, sub1(j, n)))
214                &&& (i >= 0 && f(i, j) ==> f(add1(i, n), j))
215            } by {
216            assert(((i + n) - j) / n == ((i - j) + n) / n);
217            assert((i - (j - n)) / n == ((i - j) + n) / n);
218            assert(((i - n) - j) / n == ((i - j) - n) / n);
219            assert((i - (j + n)) / n == ((i - j) - n) / n);
220        }
221        assert forall|i: int, j: int| 0 <= i < n && 0 <= j < n implies #[trigger] f(i, j) by {
222            assert(((i + n) - j) / n == ((i - j) + n) / n);
223            assert((i - (j - n)) / n == ((i - j) + n) / n);
224            assert(((i - n) - j) / n == ((i - j) - n) / n);
225            assert((i - (j + n)) / n == ((i - j) - n) / n);
226        }
227        lemma_mod_induction_forall2(n, f);
228        assert(f(x, y));
229    }
230}
231
232/// Proof of `div_auto(n)`, which expresses many useful properties of
233/// division when the denominator is the given positive integer `n`.
234pub proof fn lemma_div_auto(n: int)
235    requires
236        n > 0,
237    ensures
238        div_auto(n),
239{
240    lemma_mod_auto(n);
241    lemma_div_basics(n);
242    assert forall|x: int| 0 <= x < n <==> #[trigger] (x / n) == 0 by {
243        lemma_div_basics(n);
244    }
245    assert((0 + n) / n == 1);
246    assert((0 - n) / n == -1);
247    lemma_div_auto_plus(n);
248    lemma_div_auto_minus(n);
249}
250
251/// This utility function helps prove a mathematical property by
252/// induction. The caller supplies an integer predicate, proves the
253/// predicate holds in certain base cases, and proves correctness of
254/// inductive steps both upward and downward from the base cases. This
255/// lemma invokes induction to establish that the predicate holds for
256/// the given arbitrary input `x`.
257///
258/// `f`: The integer predicate
259///
260/// `n`: Upper bound on the base cases. Specifically, the caller
261/// establishes `f(i)` for every value `i` satisfying `is_le(0, i) &&
262/// i < n`.
263///
264/// `x`: The desired case established by this lemma. Its postcondition
265/// thus includes `f(x)`.
266///
267/// To prove inductive steps upward from the base cases, the caller
268/// must establish that, for any `i`, `is_le(0, i) && f(i) ==> f(i +
269/// n)`. `is_le(0, i)` is just `0 <= i`, but written in a functional
270/// style so that it can be used where functional triggers are
271/// required.
272///
273/// To prove inductive steps downward from the base cases, the caller
274/// must establish that, for any `i`, `is_le(i + 1, n) && f(i) ==> f(i
275/// - n)`. `is_le(i + 1, n)` is just `i + 1 <= n`, but written in a
276/// functional style so that it can be used where functional triggers
277/// are required.
278pub proof fn lemma_div_induction_auto(n: int, x: int, f: spec_fn(int) -> bool)
279    requires
280        n > 0,
281        div_auto(n) ==> {
282            &&& (forall|i: int| #[trigger] is_le(0, i) && i < n ==> f(i))
283            &&& (forall|i: int| #[trigger] is_le(0, i) && f(i) ==> f(i + n))
284            &&& (forall|i: int| #[trigger] is_le(i + 1, n) && f(i) ==> f(i - n))
285        },
286    ensures
287        div_auto(n),
288        f(x),
289{
290    lemma_div_auto(n);
291    assert(forall|i: int| is_le(0, i) && i < n ==> f(i));
292    assert(forall|i: int| is_le(0, i) && #[trigger] f(i) ==> #[trigger] f(add1(i, n)));
293    assert(forall|i: int| is_le(i + 1, n) && #[trigger] f(i) ==> #[trigger] f(sub1(i, n)));
294    assert forall|i: int| 0 <= i < n implies #[trigger] f(i) by {
295        assert(f(i)) by {
296            assert(forall|i: int| is_le(0, i) && i < n ==> f(i));
297            assert(is_le(0, i) && i < n);
298        };
299    };
300    lemma_mod_induction_forall(n, f);
301    assert(f(x));
302}
303
304/// This utility function helps prove a mathematical property by
305/// induction. The caller supplies an integer predicate, proves the
306/// predicate holds in certain base cases, and proves correctness of
307/// inductive steps both upward and downward from the base cases. This
308/// lemma invokes induction to establish that the predicate holds for
309/// all integer values.
310///
311/// `f`: The integer predicate
312///
313/// `n`: Upper bound on the base cases. Specifically, the caller
314/// establishes `f(i)` for every value `i` satisfying `is_le(0, i) &&
315/// i < n`.
316///
317/// To prove inductive steps upward from the base cases, the caller
318/// must establish that, for any `i`, `is_le(0, i) && f(i) ==> f(i +
319/// n)`. `is_le(0, i)` is just `0 <= i`, but written in a functional
320/// style so that it can be used where functional triggers are
321/// required.
322///
323/// To prove inductive steps downward from the base cases, the caller
324/// must establish that, for any `i`, `is_le(i + 1, n) && f(i) ==> f(i
325/// - n)`. `is_le(i + 1, n)` is just `i + 1 <= n`, but written in a
326/// functional style so that it can be used where functional triggers
327/// are required.
328pub proof fn lemma_div_induction_auto_forall(n: int, f: spec_fn(int) -> bool)
329    requires
330        n > 0,
331        div_auto(n) ==> {
332            &&& (forall|i: int| #[trigger] is_le(0, i) && i < n ==> f(i))
333            &&& (forall|i: int| #[trigger] is_le(0, i) && f(i) ==> f(i + n))
334            &&& (forall|i: int| #[trigger] is_le(i + 1, n) && f(i) ==> f(i - n))
335        },
336    ensures
337        div_auto(n),
338        forall|i| #[trigger] f(i),
339{
340    assert(div_auto(n)) by {
341        lemma_div_induction_auto(n, 0, f);
342    }
343    assert forall|i| #[trigger] f(i) by {
344        lemma_div_induction_auto(n, i, f);
345    }
346}
347
348} // verus!