Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970// examples of using `CheckedU32` and `CheckedU64`use vstd::prelude::*;use vstd::arithmetic::overflow::*;
verus! {
fn checked_u64_constants(){ let w = CheckedU64::new(0xFFFFFFFFFFFFFFFF); let x = w.add_value(1); assert(x.is_overflowed()); assert(x.view() == 0x10000000000000000);
let y = CheckedU64::new(0x8000000000000000); let z = y.mul_value(2); assert(z.is_overflowed()); assert(z.view() == 0x10000000000000000);}
fn checked_u64_calculations(a: u64, b: u64, c: u64, d: u64) -> (result: Option<u64>) ensures match result { Some(v) => v == a * b + c * d, None => a * b + c * d > u64::MAX, }{ let a_times_b = CheckedU64::new(a).mul_value(b); let c_times_d = CheckedU64::new(c).mul_value(d); let sum_of_products = a_times_b.add_checked(&c_times_d); if sum_of_products.is_overflowed() { assert(a * b + c * d > u64::MAX); None } else { let i: u64 = sum_of_products.unwrap(); assert(i == a * b + c * d); Some(i) }}
fn checked_u32_constants(){ let w = CheckedU32::new(0xFFFFFFFF); let x = w.add_value(9); assert(x.is_overflowed()); assert(x.view() == 0x100000008);
let y = CheckedU32::new(0x40000000); let z = y.mul_value(8); assert(z.is_overflowed()); assert(z.view() == 0x200000000);}
fn checked_u32_calculations(a: u32, b: u32, c: u32, d: u32, e: u32) -> (result: Option<u32>) ensures match result { Some(v) => v == a * b + c * d + e, None => a * b + c * d + e > u32::MAX, }{ let a_times_b = CheckedU32::new(a).mul_value(b); let c_times_d = CheckedU32::new(c).mul_value(d); let sum_of_products = a_times_b.add_checked(&c_times_d); let f = sum_of_products.add_value(e); f.to_option()}
} // verus!fn main() {}