Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344//! 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!