Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687#[allow(unused_imports)]use verus_builtin::*;#[allow(unused_imports)]use verus_builtin_macros::*;
verus! {
// ANCHOR: bound_checkingproof fn bound_check(x: u32, y: u32, z: u32) requires x <= 8, y <= 8,{ assert(x * y <= 100) by (nonlinear_arith) requires x <= 10, y <= 10;
assert(x * y <= 1000);}// ANCHOR_END: bound_checking
// ANCHOR: bound_checking_funcproof fn bound_check2(x: u32, y: u32, z: u32) by (nonlinear_arith) requires x <= 8, y <= 8, ensures x * y <= 64{ }// ANCHOR_END: bound_checking_func
// ANCHOR: de_morganproof fn de_morgan_auto() by (bit_vector) ensures forall|a: u32, b: u32| #[trigger] (!(a & b)) == !a | !b, forall|a: u32, b: u32| #[trigger] (!(a | b)) == !a & !b,{}// ANCHOR_END: de_morgan
// ANCHOR: bitvector_easyfn test_passes(b: u32) { assert(b & 7 == b % 8) by (bit_vector); assert(b & 0xff < 0x100) by (bit_vector);}// ANCHOR_END: bitvector_easy
/*// ANCHOR: bitvector_failfn test_fails(x: u32, y: u32) requires x == y{ assert(x & 3 == y & 3) by(bit_vector); // Fails}// ANCHOR_END: bitvector_fail*/
// ANCHOR: bitvector_successfn test_success(x: u32, y: u32) requires x == y,{ assert(x & 3 == y & 3) by (bit_vector) requires x == y, ; // now x == y is available for the bit_vector proof}// ANCHOR_END: bitvector_success
// ANCHOR: bitvector_spec_fnspec fn get_bit(val: u32, index: u32) -> bool { 0x1u32 & (val >> index) == 1}
fn test_get_bit() { assert(get_bit(128u32, 7)) by (bit_vector);}// ANCHOR_END: bitvector_spec_fn
fn main() {}
} // verus!