vstd 0.0.0-2026-04-20-1748

//! This file contains proofs related to powers of 2. These are part
//! of the math standard library.
//!
//! It's based on the following file from the Dafny math standard library:
//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Power2.dfy`.
//! That file has the following copyright notice:
//! /*******************************************************************************
//! *  Original: Copyright (c) Microsoft Corporation
//! *  SPDX-License-Identifier: MIT
//! *
//! *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
//! *  SPDX-License-Identifier: MIT
//! *******************************************************************************/
#[allow(unused_imports)]
use super::super::prelude::*;

verus! {

#[cfg(verus_keep_ghost)]
use super::power::{
    pow,
    lemma_pow0,
    lemma_pow_positive,
    lemma_pow_adds,
    lemma_pow_strictly_increases,
    lemma_pow_subtracts,
};

/// This function computes 2 to the power of the given natural number `e`.
/// Note that the called function `pow` is opaque so the SMT solver doesn't waste time
/// repeatedly recursively unfolding it.
pub open spec fn pow2(e: nat) -> nat {
    pow(2, e) as nat
}

/// Returns true if the given integer is a power of 2 (defined recursively).
#[verifier::opaque]
pub open spec fn is_pow2(n: int) -> bool
    decreases n,
{
    if n <= 0 {
        false
    } else if n == 1 {
        true
    } else {
        n % 2 == 0 && is_pow2(n / 2)
    }
}

/// Returns true if the given integer is a power of 2
/// (defined by existential quantification in terms of `pow`).
pub open spec fn is_pow2_exists(n: int) -> bool {
    exists|i: nat| pow(2, i) == n
}

/// Proof that the recursive and existential specifications for `is_pow2` are equivalent.
pub broadcast proof fn is_pow2_equiv(n: int)
    ensures
        #![trigger is_pow2(n)]
        #![trigger is_pow2_exists(n)]
        is_pow2(n) <==> is_pow2_exists(n),
{
    if is_pow2(n) {
        assert(is_pow2_exists(n)) by {
            is_pow2_equiv_forward(n);
        }
    }
    if is_pow2_exists(n) {
        assert(is_pow2(n)) by {
            broadcast use lemma_pow_positive;

            is_pow2_equiv_reverse(n);
        }
    }
}

proof fn is_pow2_equiv_forward(n: int)
    requires
        is_pow2(n),
    ensures
        is_pow2_exists(n),
    decreases n,
{
    reveal(is_pow2);
    reveal(pow);

    if n == 1 {
        broadcast use lemma_pow0;

        assert(pow(2, 0) == n);
    } else {
        is_pow2_equiv_forward(n / 2);
        let exp = choose|i: nat| pow(2, i) == n / 2;
        assert(pow(2, exp + 1) == 2 * pow(2, exp));
    }
}

proof fn is_pow2_equiv_reverse(n: int)
    requires
        n > 0,
        is_pow2_exists(n),
    ensures
        is_pow2(n),
    decreases n,
{
    reveal(is_pow2);
    reveal(pow);

    let exp = choose|i: nat| pow(2, i) == n;

    if exp == 0 {
        broadcast use lemma_pow0;

    } else {
        assert(pow(2, (exp - 1) as nat) == n / 2);
        is_pow2_equiv_reverse(n / 2);
    }
}

/// Proof that 2 to the power of any natural number (specifically,
/// `e`) is positive.
pub broadcast proof fn lemma_pow2_pos(e: nat)
    ensures
        #[trigger] pow2(e) > 0,
{
    lemma_pow_positive(2, e);
}

/// Proof that `pow2(e)` is equivalent to `pow(2, e)`.
pub broadcast proof fn lemma_pow2(e: nat)
    ensures
        #[trigger] pow2(e) == pow(2, e) as int,
    decreases e,
{
    reveal(pow);
    if e != 0 {
        lemma_pow2((e - 1) as nat);
    }
}

/// Proof relating 2^e to 2^(e-1).
pub broadcast proof fn lemma_pow2_unfold(e: nat)
    requires
        e > 0,
    ensures
        #[trigger] pow2(e) == 2 * pow2((e - 1) as nat),
{
    reveal(pow);
    lemma_pow2(e);
    lemma_pow2((e - 1) as nat);
}

/// Proof that `2^(e1 + e2)` is equivalent to `2^e1 * 2^e2`.
pub broadcast proof fn lemma_pow2_adds(e1: nat, e2: nat)
    ensures
        #[trigger] pow2(e1 + e2) == pow2(e1) * pow2(e2),
{
    lemma_pow2(e1);
    lemma_pow2(e2);
    lemma_pow2(e1 + e2);
    lemma_pow_adds(2, e1, e2);
}

/// Proof that, as long as `e1 <= e2`, `2^(e2 - e1)` is equivalent to `2^e2 / 2^e1`.
pub broadcast proof fn lemma_pow2_subtracts(e1: nat, e2: nat)
    requires
        e1 <= e2,
    ensures
        #[trigger] pow2((e2 - e1) as nat) == pow2(e2) / pow2(e1) > 0,
{
    lemma_pow2(e1);
    lemma_pow2(e2);
    lemma_pow2((e2 - e1) as nat);
    lemma_pow_subtracts(2, e1, e2);
}

/// Proof that if `e1 < e2` then `2^e1 < 2^e2`.
pub broadcast proof fn lemma_pow2_strictly_increases(e1: nat, e2: nat)
    requires
        e1 < e2,
    ensures
        #[trigger] pow2(e1) < #[trigger] pow2(e2),
{
    lemma_pow2(e1);
    lemma_pow2(e2);
    lemma_pow_strictly_increases(2, e1, e2);
}

/// Proof establishing the concrete values for all powers of 2 from 0 to 32 and also 2^64.
pub proof fn lemma2_to64()
    ensures
        pow2(0) == 0x1,
        pow2(1) == 0x2,
        pow2(2) == 0x4,
        pow2(3) == 0x8,
        pow2(4) == 0x10,
        pow2(5) == 0x20,
        pow2(6) == 0x40,
        pow2(7) == 0x80,
        pow2(8) == 0x100,
        pow2(9) == 0x200,
        pow2(10) == 0x400,
        pow2(11) == 0x800,
        pow2(12) == 0x1000,
        pow2(13) == 0x2000,
        pow2(14) == 0x4000,
        pow2(15) == 0x8000,
        pow2(16) == 0x10000,
        pow2(17) == 0x20000,
        pow2(18) == 0x40000,
        pow2(19) == 0x80000,
        pow2(20) == 0x100000,
        pow2(21) == 0x200000,
        pow2(22) == 0x400000,
        pow2(23) == 0x800000,
        pow2(24) == 0x1000000,
        pow2(25) == 0x2000000,
        pow2(26) == 0x4000000,
        pow2(27) == 0x8000000,
        pow2(28) == 0x10000000,
        pow2(29) == 0x20000000,
        pow2(30) == 0x40000000,
        pow2(31) == 0x80000000,
        pow2(32) == 0x100000000,
        pow2(64) == 0x10000000000000000,
{
    reveal(pow);
    #[verusfmt::skip]
    assert(
        pow2(0) == 0x1 &&
        pow2(1) == 0x2 &&
        pow2(2) == 0x4 &&
        pow2(3) == 0x8 &&
        pow2(4) == 0x10 &&
        pow2(5) == 0x20 &&
        pow2(6) == 0x40 &&
        pow2(7) == 0x80 &&
        pow2(8) == 0x100 &&
        pow2(9) == 0x200 &&
        pow2(10) == 0x400 &&
        pow2(11) == 0x800 &&
        pow2(12) == 0x1000 &&
        pow2(13) == 0x2000 &&
        pow2(14) == 0x4000 &&
        pow2(15) == 0x8000 &&
        pow2(16) == 0x10000 &&
        pow2(17) == 0x20000 &&
        pow2(18) == 0x40000 &&
        pow2(19) == 0x80000 &&
        pow2(20) == 0x100000 &&
        pow2(21) == 0x200000 &&
        pow2(22) == 0x400000 &&
        pow2(23) == 0x800000 &&
        pow2(24) == 0x1000000 &&
        pow2(25) == 0x2000000 &&
        pow2(26) == 0x4000000 &&
        pow2(27) == 0x8000000 &&
        pow2(28) == 0x10000000 &&
        pow2(29) == 0x20000000 &&
        pow2(30) == 0x40000000 &&
        pow2(31) == 0x80000000 &&
        pow2(32) == 0x100000000 &&
        pow2(64) == 0x10000000000000000
    ) by(compute_only);
}

/// Proof establishing the concrete values for all powers of 2 from 33 to 64.
/// This lemma is separated from `lemma2_to64()` to avoid a stack overflow issue
/// while executing ./tools/docs.sh.
pub proof fn lemma2_to64_rest()
    ensures
        pow2(33) == 0x200000000,
        pow2(34) == 0x400000000,
        pow2(35) == 0x800000000,
        pow2(36) == 0x1000000000,
        pow2(37) == 0x2000000000,
        pow2(38) == 0x4000000000,
        pow2(39) == 0x8000000000,
        pow2(40) == 0x10000000000,
        pow2(41) == 0x20000000000,
        pow2(42) == 0x40000000000,
        pow2(43) == 0x80000000000,
        pow2(44) == 0x100000000000,
        pow2(45) == 0x200000000000,
        pow2(46) == 0x400000000000,
        pow2(47) == 0x800000000000,
        pow2(48) == 0x1000000000000,
        pow2(49) == 0x2000000000000,
        pow2(50) == 0x4000000000000,
        pow2(51) == 0x8000000000000,
        pow2(52) == 0x10000000000000,
        pow2(53) == 0x20000000000000,
        pow2(54) == 0x40000000000000,
        pow2(55) == 0x80000000000000,
        pow2(56) == 0x100000000000000,
        pow2(57) == 0x200000000000000,
        pow2(58) == 0x400000000000000,
        pow2(59) == 0x800000000000000,
        pow2(60) == 0x1000000000000000,
        pow2(61) == 0x2000000000000000,
        pow2(62) == 0x4000000000000000,
        pow2(63) == 0x8000000000000000,
        pow2(64) == 0x10000000000000000,
{
    reveal(pow);
    #[verusfmt::skip]
    assert(
        pow2(33) == 0x200000000 &&
        pow2(34) == 0x400000000 &&
        pow2(35) == 0x800000000 &&
        pow2(36) == 0x1000000000 &&
        pow2(37) == 0x2000000000 &&
        pow2(38) == 0x4000000000 &&
        pow2(39) == 0x8000000000 &&
        pow2(40) == 0x10000000000 &&
        pow2(41) == 0x20000000000 &&
        pow2(42) == 0x40000000000 &&
        pow2(43) == 0x80000000000 &&
        pow2(44) == 0x100000000000 &&
        pow2(45) == 0x200000000000 &&
        pow2(46) == 0x400000000000 &&
        pow2(47) == 0x800000000000 &&
        pow2(48) == 0x1000000000000 &&
        pow2(49) == 0x2000000000000 &&
        pow2(50) == 0x4000000000000 &&
        pow2(51) == 0x8000000000000 &&
        pow2(52) == 0x10000000000000 &&
        pow2(53) == 0x20000000000000 &&
        pow2(54) == 0x40000000000000 &&
        pow2(55) == 0x80000000000000 &&
        pow2(56) == 0x100000000000000 &&
        pow2(57) == 0x200000000000000 &&
        pow2(58) == 0x400000000000000 &&
        pow2(59) == 0x800000000000000 &&
        pow2(60) == 0x1000000000000000 &&
        pow2(61) == 0x2000000000000000 &&
        pow2(62) == 0x4000000000000000 &&
        pow2(63) == 0x8000000000000000 &&
        pow2(64) == 0x10000000000000000
    ) by(compute_only);
}

} // verus!