vstd/arithmetic/
power.rs

Help
1//! This file contains proofs related to exponentiation. These are
2//! part of 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/Power.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//! *******************************************************************************/
14use super::super::calc_macro::*;
15#[allow(unused_imports)]
16use super::super::prelude::*;
17
18verus! {
19
20use super::super::arithmetic::div_mod::*;
21#[cfg(verus_keep_ghost)]
22use super::super::arithmetic::internals::general_internals::{is_le};
23#[cfg(verus_keep_ghost)]
24use super::super::arithmetic::mul::{
25    lemma_mul_inequality,
26    lemma_mul_nonnegative,
27    lemma_mul_strictly_increases,
28    lemma_mul_left_inequality,
29    group_mul_basics,
30    lemma_mul_increases,
31    lemma_mul_is_commutative,
32    group_mul_is_distributive,
33    lemma_mul_is_associative,
34};
35#[cfg(verus_keep_ghost)]
36use super::internals::mul_internals::{group_mul_properties_internal, lemma_mul_induction_auto};
37#[cfg(verus_keep_ghost)]
38use super::super::math::{sub as sub1};
39
40/// This function performs exponentiation recursively, to compute `b`
41/// to the power of a natural number `e`.
42#[verifier::opaque]
43pub open spec fn pow(b: int, e: nat) -> int
44    decreases e,
45{
46    if e == 0 {
47        1
48    } else {
49        b * pow(b, (e - 1) as nat)
50    }
51}
52
53/// Proof that the given integer `b` to the power of 0 is 1.
54pub broadcast proof fn lemma_pow0(b: int)
55    ensures
56        #[trigger] pow(b, 0) == 1,
57{
58    reveal(pow);
59}
60
61/// Proof that the given integer `b` to the power of 1 is `b`.
62pub broadcast proof fn lemma_pow1(b: int)
63    ensures
64        #[trigger] pow(b, 1) == b,
65{
66    calc! {
67        (==)
68        pow(b, 1); {
69            reveal(pow);
70        }
71        b * pow(b, 0); {
72            lemma_pow0(b);
73        }
74        b * 1; {
75            broadcast use group_mul_basics;
76
77        }
78        b;
79    }
80}
81
82/// Proof that 0 to the power of the given positive integer `e` is 0.
83pub broadcast proof fn lemma0_pow(e: nat)
84    requires
85        e > 0,
86    ensures
87        #[trigger] pow(0, e) == 0,
88    decreases e,
89{
90    reveal(pow);
91    broadcast use group_mul_basics;
92
93    if e != 1 {
94        lemma0_pow((e - 1) as nat);
95    }
96}
97
98/// Proof that 1 to the power of the given natural number `e` is 1.
99pub broadcast proof fn lemma1_pow(e: nat)
100    ensures
101        #[trigger] pow(1, e) == 1,
102    decreases e,
103{
104    reveal(pow);
105    broadcast use group_mul_basics;
106
107    if e != 0 {
108        lemma1_pow((e - 1) as nat);
109    }
110}
111
112/// Proof that taking the given number `x` to the power of 2 produces `x * x`.
113pub broadcast proof fn lemma_square_is_pow2(x: int)
114    ensures
115        #[trigger] pow(x, 2) == x * x,
116{
117    reveal_with_fuel(pow, 3);
118}
119
120/// Proof that taking the given positive integer `b` to the power of
121/// the given natural number `n` produces a positive result.
122pub broadcast proof fn lemma_pow_positive(b: int, e: nat)
123    requires
124        b > 0,
125    ensures
126        0 < #[trigger] pow(b, e),
127{
128    // dafny does not need to reveal
129    reveal(pow);
130    broadcast use {lemma_mul_increases, lemma_pow0};
131
132    lemma_mul_induction_auto(e as int, |u: int| 0 <= u ==> 0 < pow(b, u as nat));
133}
134
135/// Proof that taking an integer `b` to the power of the sum of two
136/// natural numbers `e1` and `e2` is equivalent to multiplying `b` to
137/// the power of `e1` by `b` to the power of `e2`.
138pub broadcast proof fn lemma_pow_adds(b: int, e1: nat, e2: nat)
139    ensures
140        #[trigger] pow(b, e1 + e2) == pow(b, e1) * pow(b, e2),
141    decreases e1,
142{
143    if e1 == 0 {
144        calc! {
145            (==)
146            pow(b, e1) * pow(b, e2); {
147                lemma_pow0(b);
148            }
149            1 * pow(b, e2); {
150                broadcast use group_mul_basics;
151
152            }
153            pow(b, 0 + e2);
154        }
155    } else {
156        calc! {
157            (==)
158            pow(b, e1) * pow(b, e2); {
159                reveal(pow);
160            }
161            (b * pow(b, (e1 - 1) as nat)) * pow(b, e2); {
162                broadcast use lemma_mul_is_associative;
163
164            }
165            b * (pow(b, (e1 - 1) as nat) * pow(b, e2)); {
166                lemma_pow_adds(b, (e1 - 1) as nat, e2);
167            }
168            b * pow(b, (e1 - 1 + e2) as nat); {
169                reveal(pow);
170            }
171            pow(b, e1 + e2);
172        }
173    }
174}
175
176/// Proof that if `e1 >= e2`, then `b` to the power of `e1` is equal
177/// to the product of `b` to the power of `e1 - e2` and `b` to the
178/// power of `e2`.
179pub broadcast proof fn lemma_pow_sub_add_cancel(b: int, e1: nat, e2: nat)
180    requires
181        e1 >= e2,
182    ensures
183        #[trigger] pow(b, (e1 - e2) as nat) * pow(b, e2) == pow(b, e1),
184    decreases e1,
185{
186    lemma_pow_adds(b, (e1 - e2) as nat, e2);
187}
188
189/// Proof that, as long as `e1 <= e2`, taking a positive integer `b`
190/// to the power of `e2 - e1` is equivalent to dividing `b` to the
191/// power of `e2` by `b` to the power of `e1`.
192pub broadcast proof fn lemma_pow_subtracts(b: int, e1: nat, e2: nat)
193    requires
194        b > 0,
195        e1 <= e2,
196    ensures
197        pow(b, e1) > 0,
198        #[trigger] pow(b, (e2 - e1) as nat) == pow(b, e2) / pow(b, e1) > 0,
199{
200    broadcast use lemma_pow_positive;
201
202    calc! {
203        (==)
204        pow(b, e2) / pow(b, e1); {
205            lemma_pow_sub_add_cancel(b, e2, e1);
206        }
207        pow(b, (e2 - e1) as nat) * pow(b, e1) / pow(b, e1); {
208            lemma_div_by_multiple(pow(b, (e2 - e1) as nat), pow(b, e1));
209        }
210        pow(b, (e2 - e1) as nat);
211    }
212}
213
214/// Proof that `a` to the power of `b * c` is equal to the result of
215/// taking `a` to the power of `b`, then taking that to the power of
216/// `c`.
217pub broadcast proof fn lemma_pow_multiplies(a: int, b: nat, c: nat)
218    ensures
219        0 <= b * c,
220        #[trigger] pow(pow(a, b), c) == pow(a, b * c),
221    decreases c,
222{
223    lemma_mul_nonnegative(b as int, c as int);
224    if c == 0 {
225        broadcast use group_mul_basics;
226
227        calc! {
228            (==)
229            pow(a, (b * c) as nat); {
230                lemma_pow0(a);
231            }
232            1; {
233                lemma_pow0(pow(a, b));
234            }
235            pow(pow(a, b), c);
236        }
237    } else {
238        calc! {
239            (==)
240            b * c - b; {
241                broadcast use group_mul_basics;
242
243            }
244            b * c - b * 1; {
245                broadcast use group_mul_is_distributive;
246
247            }
248            b * (c - 1);
249        }
250        lemma_mul_nonnegative(b as int, c - 1);
251        assert(0 <= b * c - b);
252        calc! {
253            (==)
254            pow(a, b * c); {}
255            pow(a, (b + b * c - b) as nat); {
256                lemma_pow_adds(a, b, (b * c - b) as nat);
257            }
258            pow(a, b) * pow(a, (b * c - b) as nat); {}
259            pow(a, b) * pow(a, (b * (c - 1)) as nat); {
260                lemma_pow_multiplies(a, b, (c - 1) as nat);
261            }
262            pow(a, b) * pow(pow(a, b), (c - 1) as nat); {
263                reveal(pow);
264            }
265            pow(pow(a, b), c);
266        }
267    }
268}
269
270/// Proof that `a * b` to the power of `e` is equal to the product of
271/// `a` to the power of `e` and `b` to the power of `e`.
272pub broadcast proof fn lemma_pow_distributes(a: int, b: int, e: nat)
273    ensures
274        #[trigger] pow(a * b, e) == pow(a, e) * pow(b, e),
275    decreases e,
276{
277    reveal(pow);
278    broadcast use group_mul_basics;
279
280    if e >= 1 {
281        calc! {
282            (==)
283            pow(a * b, e); {
284                reveal(pow);
285            }
286            (a * b) * pow(a * b, (e - 1) as nat); {
287                lemma_pow_distributes(a, b, (e - 1) as nat);
288            }
289            (a * b) * (pow(a, (e - 1) as nat) * pow(b, (e - 1) as nat)); {
290                broadcast use {lemma_mul_is_associative, lemma_mul_is_commutative};
291
292                assert((a * b * pow(a, (e - 1) as nat)) * pow(b, (e - 1) as nat) == (a * pow(
293                    a,
294                    (e - 1) as nat,
295                ) * b) * pow(b, (e - 1) as nat));
296            }
297            (a * pow(a, (e - 1) as nat)) * (b * pow(b, (e - 1) as nat)); {
298                reveal(pow);
299            }
300            pow(a, e) * pow(b, e);
301        }
302    }
303}
304
305pub broadcast group group_pow_properties {
306    lemma_pow0,
307    lemma_pow1,
308    lemma_pow_distributes,
309    lemma_pow_adds,
310    lemma_pow_sub_add_cancel,
311    group_mul_properties_internal,
312    lemma_mul_increases,
313    lemma_mul_strictly_increases,
314}
315
316/// Proof of various useful properties of [`pow`] (exponentiation)
317proof fn lemma_pow_properties_prove_pow_auto()
318    ensures
319        forall|x: int| pow(x, 0) == 1,
320        forall|x: int| #[trigger] pow(x, 1) == x,
321        forall|x: int, y: int| y == 0 ==> #[trigger] pow(x, y as nat) == 1,
322        forall|x: int, y: int| y == 1 ==> #[trigger] pow(x, y as nat) == x,
323        forall|x: int, y: int| 0 < x && 0 < y ==> x <= #[trigger] (x * y as nat),
324        forall|x: int, y: int| 0 < x && 1 < y ==> x < #[trigger] (x * y as nat),
325        forall|x: int, y: nat, z: nat| #[trigger] pow(x, y + z) == pow(x, y) * pow(x, z),
326        forall|x: int, y: nat, z: nat|
327            y >= z ==> #[trigger] pow(x, (y - z) as nat) * pow(x, z) == pow(x, y),
328        forall|x: int, y: nat, z: nat| #[trigger] pow(x * y, z) == pow(x, z) * pow(y as int, z),
329{
330    reveal(pow);
331    broadcast use group_pow_properties;
332
333}
334
335/// Proof that a number greater than 1 raised to a power strictly
336/// increases as the power strictly increases. Specifically, given
337/// that `b > 1` and `e1 < e2`, we can conclude that `pow(b, e1) <
338/// pow(b, e2)`.
339pub broadcast proof fn lemma_pow_strictly_increases(b: nat, e1: nat, e2: nat)
340    requires
341        1 < b,
342        e1 < e2,
343    ensures
344        #[trigger] pow(b as int, e1) < #[trigger] pow(b as int, e2),
345{
346    let f = |e: int| 0 < e ==> pow(b as int, e1) < pow(b as int, (e1 + e) as nat);
347    assert forall|i: int| (#[trigger] is_le(0, i) && f(i)) implies f(i + 1) by {
348        calc! {
349            (<=)
350            pow(b as int, (e1 + i) as nat); (<=) {
351                lemma_pow_positive(b as int, (e1 + i) as nat);
352                lemma_mul_left_inequality(pow(b as int, (e1 + i) as nat), 1, b as int);
353            }
354            pow(b as int, (e1 + i) as nat) * b; (<=) {
355                lemma_pow1(b as int);
356            }
357            pow(b as int, (e1 + i) as nat) * pow(b as int, 1); (<=) {
358                lemma_pow_adds(b as int, (e1 + i) as nat, 1nat);
359            }
360            pow(b as int, (e1 + i + 1) as nat);
361        }
362        assert(0 < i ==> pow(b as int, e1) < pow(b as int, (e1 + i) as nat));
363        if (i == 0) {
364            assert(pow(b as int, e1) < pow(b as int, (e1 + 1) as nat)) by {
365                reveal(pow);
366                assert(pow(b as int, e1) < b * pow(b as int, e1)) by {
367                    // cannot be replaced to lemma_pow_auto()
368                    assert(pow(b as int, e1) > 0) by {
369                        broadcast use lemma_pow_positive;
370
371                    }
372                    lemma_mul_strictly_increases(b as int, pow(b as int, e1));
373                };
374            };
375        }
376        assert(f(i + 1));
377    }
378    lemma_mul_induction_auto(e2 - e1, f);
379}
380
381/// Proof that a positive number raised to a power increases as the
382/// power increases. Specifically, since `e1 <= e2`, we know `pow(b,
383/// e1) <= pow(b, e2)`.
384pub broadcast proof fn lemma_pow_increases(b: nat, e1: nat, e2: nat)
385    requires
386        b > 0,
387        e1 <= e2,
388    ensures
389        #[trigger] pow(b as int, e1) <= #[trigger] pow(b as int, e2),
390{
391    if e1 != e2 {
392        if b > 1 {
393            lemma_pow_strictly_increases(b, e1, e2);
394        } else {
395            lemma1_pow(e1);
396            lemma1_pow(e2);
397        }
398    }
399}
400
401/// Proof that if an exponentiation result strictly increases when the
402/// exponent changes, then the change is an increase. Specifically, if
403/// we know `pow(b, e1) < pow(b, e2)`, then we can conclude `e1 < e2`.
404pub broadcast proof fn lemma_pow_strictly_increases_converse(b: nat, e1: nat, e2: nat)
405    requires
406        b > 0,
407        #[trigger] pow(b as int, e1) < #[trigger] pow(b as int, e2),
408    ensures
409        e1 < e2,
410{
411    if e1 >= e2 {
412        lemma_pow_increases(b, e2, e1);
413        assert(false);
414    }
415}
416
417/// Proof that if the exponentiation of a number greater than 1
418/// doesn't decrease when the exponent changes, then the change isn't
419/// a decrease. Specifically, given that `b > 1` and `pow(b, e1) <=
420/// pow(b, e2)`, we can conclude that `e1 <= e2`.
421pub broadcast proof fn lemma_pow_increases_converse(b: nat, e1: nat, e2: nat)
422    requires
423        1 < b,
424        #[trigger] pow(b as int, e1) <= #[trigger] pow(b as int, e2),
425    ensures
426        e1 <= e2,
427{
428    if e1 > e2 {
429        lemma_pow_strictly_increases(b, e2, e1);
430        assert(false);
431    }
432}
433
434/// Proof that `(b^(xy))^z = (b^x)^(yz)`, given that `x * y` and `y *
435/// z` are nonnegative and `b` is positive.
436pub broadcast proof fn lemma_pull_out_pows(b: nat, x: nat, y: nat, z: nat)
437    requires
438        b > 0,
439    ensures
440        0 <= x * y,
441        0 <= y * z,
442        #[trigger] pow(pow(b as int, x * y), z) == pow(pow(b as int, x), y * z),
443{
444    lemma_mul_nonnegative(x as int, y as int);
445    lemma_mul_nonnegative(y as int, z as int);
446    lemma_pow_positive(b as int, x);
447    calc! {
448        (==)
449        pow(pow(b as int, x * y), z); {
450            lemma_pow_multiplies(b as int, x, y);
451        }
452        pow(pow(pow(b as int, x), y), z); {
453            lemma_pow_multiplies(pow(b as int, x), y, z);
454        }
455        pow(pow(b as int, x), y * z);
456    }
457}
458
459/// Proof that if `e2 <= e1` and `x < pow(b, e1)`, then dividing `x`
460/// by `pow(b, e2)` produces a result less than `pow(b, e1 - e2)`.
461pub proof fn lemma_pow_division_inequality(x: nat, b: nat, e1: nat, e2: nat)
462    requires
463        b > 0,
464        e2 <= e1,
465        x < pow(b as int, e1),
466    ensures
467        pow(b as int, e2) > 0,
468        // also somewhat annoying that division operator needs explicit type casting
469        // because the divisor and dividend need to have the same type
470        #[trigger] (x as int / pow(b as int, e2)) < #[trigger] pow(b as int, (e1 - e2) as nat),
471{
472    broadcast use lemma_pow_positive;
473
474    assert(x as int / pow(b as int, e2) >= pow(b as int, (e1 - e2) as nat) ==> false) by {
475        if x as int / pow(b as int, e2) >= pow(b as int, (e1 - e2) as nat) {
476            lemma_mul_inequality(
477                pow(b as int, (e1 - e2) as nat),
478                x as int / pow(b as int, e2),
479                pow(b as int, e2),
480            );
481            lemma_fundamental_div_mod(x as int, pow(b as int, e2));
482            broadcast use {lemma_mul_is_commutative, group_mod_properties};
483
484            lemma_pow_adds(b as int, (e1 - e2) as nat, e2);
485        }
486    };
487}
488
489/// Proof that `pow(b, e)` modulo `b` is 0.
490pub broadcast proof fn lemma_pow_mod(b: nat, e: nat)
491    requires
492        b > 0,
493        e > 0,
494    ensures
495        #[trigger] pow(b as int, e) % b as int == 0,
496{
497    reveal(pow);
498    assert(pow(b as int, e) % b as int == (b * pow(b as int, (e - 1) as nat)) % b as int);
499    assert((b * pow(b as int, (e - 1) as nat)) % b as int == (pow(b as int, (e - 1) as nat) * b)
500        % b as int) by {
501        broadcast use lemma_mul_is_commutative;
502
503    };
504    assert((pow(b as int, (e - 1) as nat) * b) % b as int == 0) by {
505        broadcast use lemma_pow_positive;
506
507        lemma_mod_multiples_basic(pow(b as int, (e - 1) as nat), b as int);
508    };
509    // TODO
510    // TO BE DiSCUSSED, suprisingly, the calculational proof saying the same thing does not work
511    // calc! {
512    // (==)
513    // pow(b as int, e) % b as int; {}
514    // (b * pow(b as int, (e - 1) as nat)) % b as int;
515    // { broadcast use lemma_mul_is_associative; }
516    // (pow(b as int, (e - 1) as nat) * b) % b as int;
517    // {
518    //     lemma_pow_positive_auto();
519    //     lemma_mod_multiples_basic(pow(b as int, (e - 1) as nat) , b as int);
520    // }
521    // 0;
522    // }
523}
524
525/// Proof that exponentiation then modulo produces the same result as
526/// doing the modulo first, then doing the exponentiation, then doing
527/// the modulo again. Specifically, `((b % m)^e) % m == b^e % m`.
528pub broadcast proof fn lemma_pow_mod_noop(b: int, e: nat, m: int)
529    requires
530        m > 0,
531    ensures
532        #[trigger] pow(b % m, e) % m == pow(b, e) % m,
533    decreases e,
534{
535    reveal(pow);
536    broadcast use group_mod_properties;
537
538    if e > 0 {
539        calc! {
540            (==)
541            pow(b % m, e) % m; {}
542            ((b % m) * pow(b % m, (e - 1) as nat)) % m; {
543                lemma_mul_mod_noop_general(b, pow(b % m, (e - 1) as nat), m);
544            }
545            ((b % m) * (pow(b % m, (e - 1) as nat) % m) % m) % m; {
546                lemma_pow_mod_noop(b, (e - 1) as nat, m);
547            }
548            ((b % m) * (pow(b, (e - 1) as nat) % m) % m) % m; {
549                lemma_mul_mod_noop_general(b, pow(b, (e - 1) as nat), m);
550            }
551            (b * (pow(b, (e - 1) as nat)) % m) % m; {}
552            (b * (pow(b, (e - 1) as nat))) % m; {}
553            pow(b, e) % m;
554        }
555    }
556}
557
558} // verus!
vstd/arithmetic/power.rs

vstd/arithmetic/
power.rs
