Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308/// This file defines structs `CheckedU8`, `CheckedU16`, etc. and/// their associated methods to handle `u8`, `u16`, etc. values that/// can overflow. Each struct includes a ghost value representing the/// true value (not subject to overflow), so that the `view` function/// can provide the true value.////// It's a fully verified library, i.e., it contains no trusted code.////// Here are some examples using `CheckedU64`. (See/// `examples/overflow.rs` for more examples, including/// ones for the analogous `CheckedU32`.)////// ```/// fn test1()/// {/// 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 test2(a: u64, b: u64, c: u64, d: u64) -> (e: Option<u64>)/// ensures/// match e {/// 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)/// }/// }/// ```#[allow(unused_imports)]use super::super::prelude::*;#[allow(unused_imports)]use super::super::view::View;#[allow(unused_imports)]#[cfg(verus_keep_ghost)]use super::mul::{lemma_mul_by_zero_is_zero, lemma_mul_inequality, lemma_mul_is_commutative};#[allow(unused_imports)]use super::*;macro_rules! checked_uint_gen { // This macro should be instantiated with the following parameters: // // $uty - The name of the `std` unsigned integer, e.g., `u64` // $cty - The name of the checked struct to create, e.g., `CheckedU64` ($uty: ty, $cty: ty) => { verus! {
/// This struct represents a `$uty` value that can overflow. The `i` field /// is a ghost value that represents the true value, while the `v` field /// is `None` when the value has overflowed and `Some(x)` when the value /// `x` fits in a `$uty`. pub struct $cty { i: Ghost<nat>, v: Option<$uty>, }
/// The view of an `$cty` instance is the true value of the instance. impl View for $cty { type V = nat;
closed spec fn view(&self) -> nat { self.i@ } }
impl Clone for $cty { /// Clones the `$cty` instance. /// Ensures the cloned instance has the same value as the original. exec fn clone(&self) -> (result: Self) ensures result@ == self@ { proof { use_type_invariant(self); } Self{ i: self.i, v: self.v } } }
impl $cty { /// This is the internal type invariant for an `$cty`. /// It ensures the key invariant that relates `i` and `v`. #[verifier::type_invariant] spec fn well_formed(self) -> bool { match self.v { Some(v) => self.i@ == v, None => self.i@ > $uty::MAX, } }
/// Creates a new `$cty` instance from a `$uty` value. /// Ensures the internal representation matches the provided value. pub closed spec fn spec_new(v: $uty) -> $cty { $cty{ i: Ghost(v as nat), v: Some(v) } }
/// Creates a new `$cty` instance from a `$uty` value. /// Ensures the internal representation matches the provided value. #[verifier::when_used_as_spec(spec_new)] pub exec fn new(v: $uty) -> (result: Self) ensures result@ == v, { Self{ i: Ghost(v as nat), v: Some(v) } }
/// Creates a new `$cty` instance with an overflowed value. /// Requires the provided value to be greater than `$uty::MAX`. /// Ensures the internal representation matches the provided value. pub exec fn new_overflowed(Ghost(i): Ghost<int>) -> (result: Self) requires i > $uty::MAX, ensures result@ == i, { Self{ i: Ghost(i as nat), v: None } }
/// Checks if the `$cty` instance is overflowed. /// Returns true if the value is greater than `$uty::MAX`. pub open spec fn spec_is_overflowed(&self) -> bool { self@ > $uty::MAX }
/// Checks if the `$cty` instance is overflowed. /// Returns true if the value is greater than `$uty::MAX`. #[verifier::when_used_as_spec(spec_is_overflowed)] pub exec fn is_overflowed(&self) -> (result: bool) ensures result == self.spec_is_overflowed() { proof { use_type_invariant(self) } self.v.is_none() }
/// Unwraps the `$cty` instance to get the `$uty` value. /// Requires the instance to not be overflowed. /// Ensures the returned value matches the internal representation. pub exec fn unwrap(&self) -> (result: $uty) requires !self.is_overflowed(), ensures result == self@, { proof { use_type_invariant(self) } self.v.unwrap() }
/// Converts the `$cty` instance to an `Option<$uty>`. /// Ensures the returned option matches the internal representation. pub exec fn to_option(&self) -> (result: Option<$uty>) ensures match result { Some(v) => self@ == v && v <= $uty::MAX, None => self@ > $uty::MAX, } { proof { use_type_invariant(self); } self.v }
/// Adds a `$uty` value to the `$cty` instance. /// Ensures the resulting value matches the sum of /// the internal representation and the provided /// value. #[inline] pub exec fn add_value(&self, v2: $uty) -> (result: Self) ensures result@ == self@ + v2, { proof { use_type_invariant(&self); } let i: Ghost<nat> = Ghost((&self@ + v2) as nat); match self.v { Some(v1) => Self{ i, v: v1.checked_add(v2) }, None => Self{ i, v: None }, } }
/// Adds another `$cty` instance to the current /// instance. Ensures the resulting value matches /// the sum of the internal representations of /// both instances. #[inline] pub exec fn add_checked(&self, v2: &$cty) -> (result: Self) ensures result@ == self@ + v2@, { proof { use_type_invariant(self); use_type_invariant(v2); } match v2.v { Some(n) => self.add_value(n), None => { let i: Ghost<nat> = Ghost((self@ + v2@) as nat); Self{ i, v: None } } } }
/// Multiplies the `$cty` instance by a `$uty` /// value. Ensures the resulting value matches the /// product of the internal representation and the /// provided value. #[inline] pub exec fn mul_value(&self, v2: $uty) -> (result: Self) ensures result@ == self@ as int * v2 as int, { proof { use_type_invariant(self); } let i: Ghost<nat> = Ghost((self@ * v2) as nat); match self.v { Some(n1) => Self{ i, v: n1.checked_mul(v2) }, None => { if v2 == 0 { assert(i@ == 0) by { lemma_mul_by_zero_is_zero(self@ as int); } Self{ i, v: Some(0) } } else { assert(self@ * v2 >= self@ * 1 == self@) by { lemma_mul_inequality(1, v2 as int, self@ as int); lemma_mul_is_commutative(self@ as int, v2 as int); } Self{ i, v: None } } }, } }
/// Multiplies the `$cty` instance by another `$cty` instance. /// Ensures the resulting value matches the product of the internal /// representations of both instances. #[inline] pub exec fn mul_checked(&self, v2: &Self) -> (result: Self) ensures result@ == self@ as int * v2@ as int, { proof { use_type_invariant(self); use_type_invariant(v2); } let i: Ghost<nat> = Ghost((self@ * v2@) as nat); match v2.v { Some(n) => self.mul_value(n), None => { match self.v { Some(n1) => { if n1 == 0 { assert(i@ == 0) by { lemma_mul_by_zero_is_zero(v2@ as int); } Self{ i, v: Some(0) } } else { assert(self@ * v2@ >= 1 * v2@ == v2@) by { lemma_mul_inequality(1, self@ as int, v2@ as int); } Self{ i, v: None } } }, None => { assert(self@ * v2@ > $uty::MAX) by { lemma_mul_inequality(1, self@ as int, v2@ as int); } Self{ i, v: None } }, } } } } } } };}
checked_uint_gen!(u8, CheckedU8);checked_uint_gen!(u16, CheckedU16);checked_uint_gen!(u32, CheckedU32);checked_uint_gen!(u64, CheckedU64);checked_uint_gen!(u128, CheckedU128);checked_uint_gen!(usize, CheckedUsize);