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::*;
1617verus! {
1819#[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};
3536/// 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{
50if x < 0 {
51 -1 + div_pos(x + d, d)
52 } else if x < d {
530
54} else {
551 + div_pos(x - d, d)
56 }
57}
5859/// 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);
68if d > 0 {
69 div_pos(x, d)
70 } else {
71 -1 * div_pos(x, -1 * d)
72 }
73}
7475/// 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}
9495/// 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{
103let 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}
108109/// 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{
117let 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}
122123/// 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}
137138/// 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 {
150let 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 {
154let f = |xx: int, yy: int|
155 {
156let 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}
185186/// 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 {
199let 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 {
203let f = |xx: int, yy: int|
204 {
205let 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}
231232/// 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}
250251/// 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}
303304/// 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}
347348} // verus!