vstd/arithmetic/
power2.rs

1//! This file contains proofs related to powers of 2. These are part
2//! 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/Power2.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::prelude::*;
16
17verus! {
18
19#[cfg(verus_keep_ghost)]
20use super::power::{
21    pow,
22    lemma_pow0,
23    lemma_pow_positive,
24    lemma_pow_adds,
25    lemma_pow_strictly_increases,
26    lemma_pow_subtracts,
27};
28
29/// This function computes 2 to the power of the given natural number `e`.
30/// Note that the called function `pow` is opaque so the SMT solver doesn't waste time
31/// repeatedly recursively unfolding it.
32pub open spec fn pow2(e: nat) -> nat {
33    pow(2, e) as nat
34}
35
36/// Returns true if the given integer is a power of 2 (defined recursively).
37#[verifier::opaque]
38pub open spec fn is_pow2(n: int) -> bool
39    decreases n,
40{
41    if n <= 0 {
42        false
43    } else if n == 1 {
44        true
45    } else {
46        n % 2 == 0 && is_pow2(n / 2)
47    }
48}
49
50/// Returns true if the given integer is a power of 2
51/// (defined by existential quantification in terms of `pow`).
52pub open spec fn is_pow2_exists(n: int) -> bool {
53    exists|i: nat| pow(2, i) == n
54}
55
56/// Proof that the recursive and existential specifications for `is_pow2` are equivalent.
57pub broadcast proof fn is_pow2_equiv(n: int)
58    ensures
59        #![trigger is_pow2(n)]
60        #![trigger is_pow2_exists(n)]
61        is_pow2(n) <==> is_pow2_exists(n),
62{
63    if is_pow2(n) {
64        assert(is_pow2_exists(n)) by {
65            is_pow2_equiv_forward(n);
66        }
67    }
68    if is_pow2_exists(n) {
69        assert(is_pow2(n)) by {
70            broadcast use lemma_pow_positive;
71
72            is_pow2_equiv_reverse(n);
73        }
74    }
75}
76
77proof fn is_pow2_equiv_forward(n: int)
78    requires
79        is_pow2(n),
80    ensures
81        is_pow2_exists(n),
82    decreases n,
83{
84    reveal(is_pow2);
85    reveal(pow);
86
87    if n == 1 {
88        broadcast use lemma_pow0;
89
90        assert(pow(2, 0) == n);
91    } else {
92        is_pow2_equiv_forward(n / 2);
93        let exp = choose|i: nat| pow(2, i) == n / 2;
94        assert(pow(2, exp + 1) == 2 * pow(2, exp));
95    }
96}
97
98proof fn is_pow2_equiv_reverse(n: int)
99    requires
100        n > 0,
101        is_pow2_exists(n),
102    ensures
103        is_pow2(n),
104    decreases n,
105{
106    reveal(is_pow2);
107    reveal(pow);
108
109    let exp = choose|i: nat| pow(2, i) == n;
110
111    if exp == 0 {
112        broadcast use lemma_pow0;
113
114    } else {
115        assert(pow(2, (exp - 1) as nat) == n / 2);
116        is_pow2_equiv_reverse(n / 2);
117    }
118}
119
120/// Proof that 2 to the power of any natural number (specifically,
121/// `e`) is positive.
122pub broadcast proof fn lemma_pow2_pos(e: nat)
123    ensures
124        #[trigger] pow2(e) > 0,
125{
126    lemma_pow_positive(2, e);
127}
128
129/// Proof that `pow2(e)` is equivalent to `pow(2, e)`.
130pub broadcast proof fn lemma_pow2(e: nat)
131    ensures
132        #[trigger] pow2(e) == pow(2, e) as int,
133    decreases e,
134{
135    reveal(pow);
136    if e != 0 {
137        lemma_pow2((e - 1) as nat);
138    }
139}
140
141/// Proof relating 2^e to 2^(e-1).
142pub broadcast proof fn lemma_pow2_unfold(e: nat)
143    requires
144        e > 0,
145    ensures
146        #[trigger] pow2(e) == 2 * pow2((e - 1) as nat),
147{
148    reveal(pow);
149    lemma_pow2(e);
150    lemma_pow2((e - 1) as nat);
151}
152
153/// Proof that `2^(e1 + e2)` is equivalent to `2^e1 * 2^e2`.
154pub broadcast proof fn lemma_pow2_adds(e1: nat, e2: nat)
155    ensures
156        #[trigger] pow2(e1 + e2) == pow2(e1) * pow2(e2),
157{
158    lemma_pow2(e1);
159    lemma_pow2(e2);
160    lemma_pow2(e1 + e2);
161    lemma_pow_adds(2, e1, e2);
162}
163
164/// Proof that, as long as `e1 <= e2`, `2^(e2 - e1)` is equivalent to `2^e2 / 2^e1`.
165pub broadcast proof fn lemma_pow2_subtracts(e1: nat, e2: nat)
166    requires
167        e1 <= e2,
168    ensures
169        #[trigger] pow2((e2 - e1) as nat) == pow2(e2) / pow2(e1) > 0,
170{
171    lemma_pow2(e1);
172    lemma_pow2(e2);
173    lemma_pow2((e2 - e1) as nat);
174    lemma_pow_subtracts(2, e1, e2);
175}
176
177/// Proof that if `e1 < e2` then `2^e1 < 2^e2`.
178pub broadcast proof fn lemma_pow2_strictly_increases(e1: nat, e2: nat)
179    requires
180        e1 < e2,
181    ensures
182        #[trigger] pow2(e1) < #[trigger] pow2(e2),
183{
184    lemma_pow2(e1);
185    lemma_pow2(e2);
186    lemma_pow_strictly_increases(2, e1, e2);
187}
188
189/// Proof establishing the concrete values for all powers of 2 from 0 to 32 and also 2^64.
190pub proof fn lemma2_to64()
191    ensures
192        pow2(0) == 0x1,
193        pow2(1) == 0x2,
194        pow2(2) == 0x4,
195        pow2(3) == 0x8,
196        pow2(4) == 0x10,
197        pow2(5) == 0x20,
198        pow2(6) == 0x40,
199        pow2(7) == 0x80,
200        pow2(8) == 0x100,
201        pow2(9) == 0x200,
202        pow2(10) == 0x400,
203        pow2(11) == 0x800,
204        pow2(12) == 0x1000,
205        pow2(13) == 0x2000,
206        pow2(14) == 0x4000,
207        pow2(15) == 0x8000,
208        pow2(16) == 0x10000,
209        pow2(17) == 0x20000,
210        pow2(18) == 0x40000,
211        pow2(19) == 0x80000,
212        pow2(20) == 0x100000,
213        pow2(21) == 0x200000,
214        pow2(22) == 0x400000,
215        pow2(23) == 0x800000,
216        pow2(24) == 0x1000000,
217        pow2(25) == 0x2000000,
218        pow2(26) == 0x4000000,
219        pow2(27) == 0x8000000,
220        pow2(28) == 0x10000000,
221        pow2(29) == 0x20000000,
222        pow2(30) == 0x40000000,
223        pow2(31) == 0x80000000,
224        pow2(32) == 0x100000000,
225        pow2(64) == 0x10000000000000000,
226{
227    reveal(pow);
228    #[verusfmt::skip]
229    assert(
230        pow2(0) == 0x1 &&
231        pow2(1) == 0x2 &&
232        pow2(2) == 0x4 &&
233        pow2(3) == 0x8 &&
234        pow2(4) == 0x10 &&
235        pow2(5) == 0x20 &&
236        pow2(6) == 0x40 &&
237        pow2(7) == 0x80 &&
238        pow2(8) == 0x100 &&
239        pow2(9) == 0x200 &&
240        pow2(10) == 0x400 &&
241        pow2(11) == 0x800 &&
242        pow2(12) == 0x1000 &&
243        pow2(13) == 0x2000 &&
244        pow2(14) == 0x4000 &&
245        pow2(15) == 0x8000 &&
246        pow2(16) == 0x10000 &&
247        pow2(17) == 0x20000 &&
248        pow2(18) == 0x40000 &&
249        pow2(19) == 0x80000 &&
250        pow2(20) == 0x100000 &&
251        pow2(21) == 0x200000 &&
252        pow2(22) == 0x400000 &&
253        pow2(23) == 0x800000 &&
254        pow2(24) == 0x1000000 &&
255        pow2(25) == 0x2000000 &&
256        pow2(26) == 0x4000000 &&
257        pow2(27) == 0x8000000 &&
258        pow2(28) == 0x10000000 &&
259        pow2(29) == 0x20000000 &&
260        pow2(30) == 0x40000000 &&
261        pow2(31) == 0x80000000 &&
262        pow2(32) == 0x100000000 &&
263        pow2(64) == 0x10000000000000000
264    ) by(compute_only);
265}
266
267/// Proof establishing the concrete values for all powers of 2 from 33 to 64.
268/// This lemma is separated from `lemma2_to64()` to avoid a stack overflow issue
269/// while executing ./tools/docs.sh.
270pub proof fn lemma2_to64_rest()
271    ensures
272        pow2(33) == 0x200000000,
273        pow2(34) == 0x400000000,
274        pow2(35) == 0x800000000,
275        pow2(36) == 0x1000000000,
276        pow2(37) == 0x2000000000,
277        pow2(38) == 0x4000000000,
278        pow2(39) == 0x8000000000,
279        pow2(40) == 0x10000000000,
280        pow2(41) == 0x20000000000,
281        pow2(42) == 0x40000000000,
282        pow2(43) == 0x80000000000,
283        pow2(44) == 0x100000000000,
284        pow2(45) == 0x200000000000,
285        pow2(46) == 0x400000000000,
286        pow2(47) == 0x800000000000,
287        pow2(48) == 0x1000000000000,
288        pow2(49) == 0x2000000000000,
289        pow2(50) == 0x4000000000000,
290        pow2(51) == 0x8000000000000,
291        pow2(52) == 0x10000000000000,
292        pow2(53) == 0x20000000000000,
293        pow2(54) == 0x40000000000000,
294        pow2(55) == 0x80000000000000,
295        pow2(56) == 0x100000000000000,
296        pow2(57) == 0x200000000000000,
297        pow2(58) == 0x400000000000000,
298        pow2(59) == 0x800000000000000,
299        pow2(60) == 0x1000000000000000,
300        pow2(61) == 0x2000000000000000,
301        pow2(62) == 0x4000000000000000,
302        pow2(63) == 0x8000000000000000,
303        pow2(64) == 0x10000000000000000,
304{
305    reveal(pow);
306    #[verusfmt::skip]
307    assert(
308        pow2(33) == 0x200000000 &&
309        pow2(34) == 0x400000000 &&
310        pow2(35) == 0x800000000 &&
311        pow2(36) == 0x1000000000 &&
312        pow2(37) == 0x2000000000 &&
313        pow2(38) == 0x4000000000 &&
314        pow2(39) == 0x8000000000 &&
315        pow2(40) == 0x10000000000 &&
316        pow2(41) == 0x20000000000 &&
317        pow2(42) == 0x40000000000 &&
318        pow2(43) == 0x80000000000 &&
319        pow2(44) == 0x100000000000 &&
320        pow2(45) == 0x200000000000 &&
321        pow2(46) == 0x400000000000 &&
322        pow2(47) == 0x800000000000 &&
323        pow2(48) == 0x1000000000000 &&
324        pow2(49) == 0x2000000000000 &&
325        pow2(50) == 0x4000000000000 &&
326        pow2(51) == 0x8000000000000 &&
327        pow2(52) == 0x10000000000000 &&
328        pow2(53) == 0x20000000000000 &&
329        pow2(54) == 0x40000000000000 &&
330        pow2(55) == 0x80000000000000 &&
331        pow2(56) == 0x100000000000000 &&
332        pow2(57) == 0x200000000000000 &&
333        pow2(58) == 0x400000000000000 &&
334        pow2(59) == 0x800000000000000 &&
335        pow2(60) == 0x1000000000000000 &&
336        pow2(61) == 0x2000000000000000 &&
337        pow2(62) == 0x4000000000000000 &&
338        pow2(63) == 0x8000000000000000 &&
339        pow2(64) == 0x10000000000000000
340    ) by(compute_only);
341}
342
343} // verus!
vstd/arithmetic/power2.rs

vstd/arithmetic/
power2.rs
