vstd/arithmetic/
logarithm.rs

1//! This file contains proofs related to integer logarithms. These are
2//! part of the math standard library.
3//!
4//! It's based on the following file from the Dafny math standard
5//! library:
6//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Logarithm.dfy`.
7//! That file has the following copyright notice:
8//! /*******************************************************************************
9//! * Original: Copyright (c) Microsoft Corporation *
10//! SPDX-License-Identifier: MIT * * Modifications and Extensions:
11//! 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
19use super::super::calc_macro::*;
20#[cfg(verus_keep_ghost)]
21use super::div_mod::{
22    lemma_div_pos_is_pos,
23    lemma_div_decreases,
24    lemma_div_is_ordered,
25    lemma_div_multiples_vanish,
26};
27#[cfg(verus_keep_ghost)]
28use super::super::math::{div as div1};
29#[cfg(verus_keep_ghost)]
30use super::super::arithmetic::mul::{lemma_mul_increases, lemma_mul_is_commutative};
31#[cfg(verus_keep_ghost)]
32use super::super::arithmetic::power::{pow, lemma_pow_positive};
33
34/// This function recursively defines the integer logarithm. It's only
35/// meaningful when the base of the logarithm `base` is greater than 1,
36/// and when the value whose logarithm is taken, `pow`, is non-negative.
37#[verifier::opaque]
38pub open spec fn log(base: int, pow: int) -> int
39    recommends
40        base > 1,
41        pow >= 0,
42    decreases pow,
43{
44    // In Dafny, we can invoke lemmas in functions to establish
45    // termination. Here in Verus, instead, we add the second
46    // conditions `pow / base >= pow` and `pow / base < 0` to show
47    // termination.
48    if pow < base || pow / base >= pow || pow / base < 0 {
49        0
50    } else {
51        1 + log(base, pow / base)
52    }
53}
54
55/// Proof that since `pow` is less than `base`, its logarithm in that base is 0.
56pub proof fn lemma_log0(base: int, pow: int)
57    requires
58        base > 1,
59        0 <= pow < base,
60    ensures
61        log(base, pow) == 0,
62{
63    reveal(log);
64}
65
66/// Proof that since `pow` is greater than or equal to `base`, its
67/// logarithm in that base is 1 more than the logarithm of `pow /
68/// base`.
69pub broadcast proof fn lemma_log_s(base: int, pow: int)
70    requires
71        base > 1,
72        pow >= base,
73    ensures
74        #![trigger log(base, div1(pow, base))]
75        pow / base >= 0,
76        log(base, pow) == 1 + log(base, pow / base),
77{
78    broadcast use {lemma_div_pos_is_pos, lemma_div_decreases};
79
80    reveal(log);
81}
82
83/// Proof that the integer logarithm is always nonnegative. Specifically,
84/// `log(base, pow) >= 0`.
85pub proof fn lemma_log_nonnegative(base: int, pow: int)
86    requires
87        base > 1,
88        0 <= pow,
89    ensures
90        log(base, pow) >= 0,
91    decreases pow,
92{
93    reveal(log);
94    if !(pow < base || pow / base >= pow || pow / base < 0) {
95        lemma_log_nonnegative(base, pow / base);
96    }
97}
98
99/// Proof that since `pow1` is less than or equal to `pow2`, the
100/// integer logarithm of `pow1` in base `base` is less than or equal
101/// to that of `pow2`.
102pub proof fn lemma_log_is_ordered(base: int, pow1: int, pow2: int)
103    requires
104        base > 1,
105        0 <= pow1 <= pow2,
106    ensures
107        log(base, pow1) <= log(base, pow2),
108    decreases pow1,
109{
110    reveal(log);
111    if pow2 < base {
112        assert(log(base, pow1) == 0 == log(base, pow2));
113    } else if pow1 < base {
114        assert(log(base, pow1) == 0);
115        lemma_log_nonnegative(base, pow2);
116    } else {
117        broadcast use {lemma_div_pos_is_pos, lemma_div_is_ordered, lemma_div_decreases};
118
119        lemma_log_is_ordered(base, pow1 / base, pow2 / base);
120    }
121}
122
123/// Proof that the integer logarithm of `pow(base, n)` in base `base` is `n`.
124pub proof fn lemma_log_pow(base: int, n: nat)
125    requires
126        base > 1,
127    ensures
128        log(base, pow(base, n)) == n,
129    decreases n,
130{
131    if n == 0 {
132        reveal(pow);
133        reveal(log);
134    } else {
135        let n_minus_1: nat = (n - 1) as nat;
136        lemma_pow_positive(base, n);
137        calc! {
138            (==)
139            log(base, pow(base, n)); (==) {
140                reveal(pow);
141            }
142            log(base, base * pow(base, n_minus_1)); (==) {
143                lemma_pow_positive(base, n_minus_1);
144                lemma_mul_increases(pow(base, n_minus_1), base);
145                lemma_mul_is_commutative(pow(base, n_minus_1), base);
146                lemma_log_s(base, base * pow(base, n_minus_1));
147            }
148            1 + log(base, (base * pow(base, n_minus_1)) / base); (==) {
149                lemma_div_multiples_vanish(pow(base, n_minus_1), base);
150            }
151            1 + log(base, pow(base, n_minus_1)); (==) {
152                lemma_log_pow(base, n_minus_1);
153            }
154            1 + (n - 1);
155        }
156    }
157}
158
159} // verus!
vstd/arithmetic/logarithm.rs

vstd/arithmetic/
logarithm.rs
