Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573//! Helper utilities used by the `verus_state_machines_macros` codegen.#![allow(unused_imports)]#![doc(hidden)]
use super::imap::*;use super::iset::*;use super::map::*;use super::pervasive::*;use super::prelude::*;use super::seq::*;use super::set::*;
#[cfg_attr(verus_keep_ghost, verifier::external_body)] /* vattr */#[cfg_attr(verus_keep_ghost, verifier::accept_recursive_types(T))]pub struct SyncSendIfSyncSend<T> { _sync_send: super::prelude::SyncSendIfSyncSend<T>,}
#[cfg_attr(verus_keep_ghost, verifier::verus_macro)]impl<T> Clone for SyncSendIfSyncSend<T> { #[cfg_attr(verus_keep_ghost, verifier::external_body)] fn clone(&self) -> Self { SyncSendIfSyncSend { _sync_send: self._sync_send.clone() } }}
impl<T> Copy for SyncSendIfSyncSend<T> {}
#[cfg_attr(verus_keep_ghost, verifier::external_body)] /* vattr */pub struct NoCopy { _no_copy: super::prelude::NoCopy,}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_safety(b: bool) { requires( #[verifier::custom_err("unable to prove assertion safety condition")] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_let_pattern(b: bool) { requires( #[verifier::custom_err("unable to prove safety condition that the pattern matches")] /* vattr */ b, ); ensures(b);}
// SpecialOps
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: to add a value Some(_), field must be None before the update" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_set(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: to add a singleton set, the value must not be in the set before the update" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_iset(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: to add a singleton iset, the value must not be in the iset before the update" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_bool(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: to add a value `true`, field must be `false` before the update" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the given key must be absent from the map before the update" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the given key must be absent from the imap before the update" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_persistent_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: if the key is already in the map, its existing value must agree with the provided value" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_persistent_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: if the key is already in the imap, its existing value must agree with the provided value" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_add_persistent_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: if the previous value is Some(_), then this existing value must agree with the newly provided value" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_withdraw_option(b: bool) { requires(b); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_deposit_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: to deposit a value into Some(_), the field must be None before the deposit" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_guard_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the value being guarded must be stored" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_withdraw_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the value to be withdrawn must be stored at the given key before the withdraw" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_withdraw_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the value to be withdrawn must be stored at the given key before the withdraw" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_deposit_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the given key must be absent from the map before the deposit" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_deposit_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the given key must be absent from the imap before the deposit" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_guard_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the value being guarded must be stored at the given key" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_guard_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the value being guarded must be stored at the given key" )] /* vattr */ b, ); ensures(b);}
// SpecialOps (with general element)
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the optional values being composed cannot both be Some(_)" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_set(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the sets being composed must be disjoint" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_iset(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the isets being composed must be disjoint" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_bool(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the boolean values being composed cannot both be `true`" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the key domains of the maps being composed must be disjoint" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the key domains of the imaps being composed must be disjoint" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_persistent_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the maps being composed must agree on their values for any key in both domains" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_persistent_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the imaps being composed must agree on their values for any key in both domains" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_add_persistent_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: if the previous value and the newly added values are both Some(_), then their values must agree" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_withdraw_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the optional value to be withdrawn must be stored before the withdraw" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_deposit_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the optional values being composed cannot both be Some(_)" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_guard_option(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the value being guarded must be stored" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_withdraw_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the map being withdrawn must be a submap of the stored map" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_withdraw_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the imap being withdrawn must be a submap of the stored imap" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_deposit_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the key domains of the maps being composed must be disjoint" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_deposit_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the key domains of the imaps being composed must be disjoint" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_guard_map(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the map being guarded must be a submap of the stored map" )] /* vattr */ b, ); ensures(b);}
#[cfg(verus_keep_ghost)]#[verifier::proof]pub fn assert_general_guard_imap(b: bool) { requires( #[verifier::custom_err( "unable to prove inherent safety condition: the imap being guarded must be a submap of the stored imap" )] /* vattr */ b, ); ensures(b);}
// used by the `update field[idx] = ...;` syntax//// note: the built-in rust trait IndexMut doesn't work here// (because these functions need to be 'spec' code, and IndexMut uses a &mut to do its job)// perhaps we'll make our own trait for this purpose some day, but regardless, this suffices// for our purposes
verus! {
#[doc(hidden)]pub open spec fn nat_max(a: nat, b: nat) -> nat { if a > b { a } else { b }}
#[doc(hidden)]impl<A> Seq<A> { #[verifier::inline] pub open spec fn update_at_index(self, i: int, a: A) -> Self recommends 0 <= i < self.len(), { self.update(i, a) }}
#[doc(hidden)]impl<K, V> Map<K, V> { // note that despite the name, this is allowed to insert #[verifier::inline] pub open spec fn update_at_index(self, k: K, v: V) -> Self { self.insert(k, v) }}
#[doc(hidden)]impl<K, V> IMap<K, V> { // note that despite the name, this is allowed to insert #[verifier::inline] pub open spec fn update_at_index(self, k: K, v: V) -> Self { self.insert(k, v) }}
#[doc(hidden)]#[verifier::inline]pub open spec fn opt_is_none<V>(a: Option<V>) -> bool { a is None}
#[doc(hidden)]#[verifier::inline]pub open spec fn opt_ge<V>(a: Option<V>, b: Option<V>) -> bool { b is Some ==> a == b}
#[doc(hidden)]#[verifier::inline]pub open spec fn opt_add<V>(a: Option<V>, b: Option<V>) -> Option<V> { if b is Some { b } else { a }}
#[doc(hidden)]#[verifier::inline]pub open spec fn opt_agree<V>(a: Option<V>, b: Option<V>) -> bool { a is Some && b is Some ==> a->0 == b->0}
#[doc(hidden)]#[verifier::inline]pub open spec fn opt_sub<V>(a: Option<V>, b: Option<V>) -> Option<V> { if b is Some { Option::None } else { a }}
} // verus!