Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221use super::super::prelude::*;use core::marker::PointeeSized;
use verus as verus_skip_verusfmt;verus_skip_verusfmt! {
#[verifier::external_trait_specification]pub trait ExTuple { type ExternalTraitSpecificationFor: core::marker::Tuple;}
#[verifier::external_trait_specification]pub trait ExFnOnce<Args: core::marker::Tuple> { type ExternalTraitSpecificationFor: core::ops::FnOnce<Args>;
type Output;}
#[verifier::external_trait_specification]pub trait ExFnMut<Args: core::marker::Tuple>: FnOnce<Args> { type ExternalTraitSpecificationFor: core::ops::FnMut<Args>;}
#[verifier::external_trait_specification]pub trait ExFn<Args: core::marker::Tuple>: FnMut<Args> { type ExternalTraitSpecificationFor: core::ops::Fn<Args>;}
#[verifier::external_trait_specification]pub trait ExDeref: PointeeSized { type ExternalTraitSpecificationFor: core::ops::Deref;
type Target: ?Sized;
fn deref(&self) -> &Self::Target;}
#[verifier::external_trait_specification]pub trait ExDerefMut: core::ops::Deref + PointeeSized { type ExternalTraitSpecificationFor: core::ops::DerefMut;
fn deref_mut(&mut self) -> &mut Self::Target;}
#[verifier::external_trait_specification]#[verifier::external_trait_extension(IndexSpec via IndexSpecImpl)]pub trait ExIndex<Idx> where Idx: ?Sized { type ExternalTraitSpecificationFor: core::ops::Index<Idx>;
type Output: ?Sized;
// NOTE: this used as a precondition for both `Index` and `IndexMut`, // since both share the same `s[i]` syntax. spec fn index_req(&self, index: &Idx) -> bool;
fn index(&self, index: Idx) -> (output: &Self::Output) where Idx: Sized requires self.index_req(&index), ;}
#[verifier::external_trait_specification]pub trait ExIndexMut<Idx>: core::ops::Index<Idx> where Idx: ?Sized { type ExternalTraitSpecificationFor: core::ops::IndexMut<Idx>;
fn index_mut(&mut self, index: Idx) -> (output: &mut Self::Output) where Idx: Sized requires self.index_req(&index), ;}
#[verifier::external_trait_specification]pub trait ExInteger: Copy { type ExternalTraitSpecificationFor: Integer;}
#[verifier::external_trait_specification]pub trait ExSpecOrd<Rhs> { type ExternalTraitSpecificationFor: SpecOrd<Rhs>;}
#[cfg(not(verus_verify_core))]#[verifier::external_trait_specification]pub trait ExAllocator { type ExternalTraitSpecificationFor: core::alloc::Allocator;}
#[verifier::external_trait_specification]pub trait ExFreeze: PointeeSized { type ExternalTraitSpecificationFor: core::marker::Freeze;}
#[verifier::external_trait_specification]pub trait ExHash: PointeeSized { type ExternalTraitSpecificationFor: core::hash::Hash;}
#[verifier::external_trait_specification]pub trait ExPtrPointee: PointeeSized { type ExternalTraitSpecificationFor: core::ptr::Pointee;
type Metadata: Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze;}
#[verifier::external_trait_specification]pub trait ExBorrow<Borrowed> where Borrowed: ?Sized { type ExternalTraitSpecificationFor: core::borrow::Borrow<Borrowed>;}
#[verifier::external_trait_specification]pub trait ExStructural { type ExternalTraitSpecificationFor: Structural;}
// Since this trait involves the unstable library feature `const_destruct`,// we only enable it when verifying core#[cfg(verus_verify_core)]#[verifier::external_trait_specification]trait ExDestruct: PointeeSized { type ExternalTraitSpecificationFor: core::marker::Destruct;}
#[verifier::external_trait_specification]pub trait ExMetaSized { type ExternalTraitSpecificationFor: core::marker::MetaSized;}
pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T) ensures *final(a) == *old(b), *final(b) == *old(a), opens_invariants none no_unwind;
#[verifier::external_type_specification]pub struct ExOrdering(core::cmp::Ordering);
#[verifier::external_type_specification]#[verifier::accept_recursive_types(V)]#[verifier::ext_equal]pub struct ExOption<V>(core::option::Option<V>);
#[verifier::external_type_specification]#[verifier::accept_recursive_types(T)]#[verifier::reject_recursive_types_in_ground_variants(E)]pub struct ExResult<T, E>(core::result::Result<T, E>);
// I don't really expect this to be particularly useful;// this is mostly here because I wanted an easy way to test// the combination of external_type_specification & external_body// in a cross-crate context.#[verifier::external_type_specification]#[verifier::external_body]pub struct ExDuration(core::time::Duration);
#[verifier::external_type_specification]#[verifier::accept_recursive_types(V)]pub struct ExPhantomData<V: PointeeSized>(core::marker::PhantomData<V>);
pub assume_specification[ core::intrinsics::likely ](b: bool) -> (c: bool) ensures c == b,;
pub assume_specification[ core::intrinsics::unlikely ](b: bool) -> (c: bool) ensures c == b,;
pub assume_specification<T, F: FnOnce() -> T>[ bool::then ](b: bool, f: F) -> (ret: Option<T>) requires b ==> f.requires(()), ensures if b { ret.is_some() && f.ensures((), ret.unwrap()) } else { ret.is_none() },;
pub assume_specification<T> [core::hint::must_use] (value: T) -> (ret: T) ensures ret == value,;
pub assume_specification [core::panicking::panic] (s: &'static str) -> ! requires false,;
pub assume_specification [core::panicking::panic_fmt] (s: core::fmt::Arguments<'_>) -> ! requires false,;
// Called by `assert_eq!` and `assert_ne!`; not external_body, since the macros construct an `AssertKind`#[verifier::external_type_specification]pub struct ExAssertKind(core::panicking::AssertKind);
pub assume_specification<T, U>[ core::panicking::assert_failed::<T, U> ]( kind: core::panicking::AssertKind, left: &T, right: &U, args: Option<core::fmt::Arguments<'_>>,) -> ! where T: core::fmt::Debug + ?Sized, U: core::fmt::Debug + ?Sized, requires false,;
} // verus!
#[verifier::external_type_specification]#[verifier::external_body]#[verifier::accept_recursive_types(T)]pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);