Trait Objective 

pub auto trait Objective { }

An assertion whose meaning is independent of this thread’s view.

Since Objective refers to ghost objects whose memory is objective, Rust’s Unique<T> (and therefore Box<T>, Vec<T>, …) are therefore objective.

Implementors

impl !Objective for NotObjective

impl<T> Objective for AtView<T>

impl<T: Objective> Objective for EndBorrow<T>

impl<T: Objective> Objective for FullBorrow<T>

Auto implementors

impl Objective for CancelLocalUpdateUnit

impl Objective for PositiveReal

impl Objective for Real

impl Objective for Id

impl Objective for Int

impl Objective for Nat

impl Objective for Positive

impl Objective for PeanoInt

impl Objective for PtrDeepModel

impl Objective for AcqRel

impl Objective for Acquire

impl Objective for None

impl Objective for Relaxed

impl Objective for Release

impl Objective for SeqCst

impl Objective for AtomicBool

impl Objective for AtomicI8

impl Objective for AtomicI16

impl Objective for AtomicI32

impl Objective for AtomicI64

impl Objective for AtomicIsize

impl Objective for AtomicU8

impl Objective for AtomicU16

impl Objective for AtomicU32

impl Objective for AtomicU64

impl Objective for AtomicUsize

impl Objective for AcquireSyncView

impl Objective for ReleaseSyncView

impl Objective for SyncView

impl Objective for Namespace

impl Objective for Lifetime

impl Objective for LifetimeDead

impl Objective for LifetimeToken

impl<'a> Objective for Tokens<'a>

impl<'a, T> Objective for PtrLive<'a, T>

where T: Objective,

impl<'scope, 'env> Objective for Scope<'scope, 'env>

impl<A, B> Objective for Mapping<A, B>

where A: ?Sized,

impl<C> Objective for Perm<C>

where <C as PermTarget>::PermPayload: Objective, C: ?Sized,

impl<C, T, Load, Store> Objective for Committer<C, T, Load, Store>

where C: Objective, T: Objective, Load: Objective, Store: Objective,

impl<I, F> Objective for MapInv<I, F>

where I: Objective, F: Objective, <I as Iterator>::Item: Objective,

impl<K, V> Objective for FMap<K, V>

where K: Objective, V: Objective,

impl<K, V> Objective for creusot_std::logic::fmap::Iter<K, V>

where K: Objective, V: Objective,

impl<K, V> Objective for FMapInsertLocalUpdate<K, V>

where K: Objective, V: Objective,

impl<R> Objective for OpLocalUpdate<R>

where R: Objective,

impl<R> Objective for View<R>

where <R as ViewRel>::Frag: Objective, <R as ViewRel>::Auth: Objective,

impl<R> Objective for ViewUpdateInsert<R>

where <R as ViewRel>::Auth: Objective, <R as ViewRel>::Frag: Objective,

impl<R> Objective for ViewUpdateRemove<R>

where <R as ViewRel>::Auth: Objective,

impl<R> Objective for Authority<R>

where R: Objective,

impl<R> Objective for Fragment<R>

where R: Objective,

impl<R> Objective for Resource<R>

where R: Objective,

impl<R, Choice> Objective for ViewUpdate<R, Choice>

impl<T> Objective for PermCell<T>

where T: Objective + ?Sized,

impl<T> Objective for PredCell<T>

where T: Objective + ?Sized,

impl<T> Objective for Subset<T>

where T: Objective,

impl<T> Objective for Ag<T>

where T: Objective,

impl<T> Objective for AuthViewRel<T>

where T: Objective,

impl<T> Objective for Excl<T>

where T: Objective,

impl<T> Objective for ExclUpdate<T>

where T: Objective,

impl<T> Objective for creusot_std::logic::seq::Iter<T>

where T: Objective,

impl<T> Objective for Seq<T>

where T: Objective,

impl<T> Objective for FSet<T>

where T: Objective,

impl<T> Objective for Set<T>

where T: Objective + ?Sized,

impl<T> Objective for Snapshot<T>

where T: Objective + ?Sized,

impl<T> Objective for AtomicPtr<T>

where T: Objective,

impl<T> Objective for AtomicInvariant<T>

where T: Objective,

impl<T> Objective for AtomicInvariantSC<T>

where T: Objective,

impl<T> Objective for NonAtomicInvariant<T>

where T: Objective,

impl<T> Objective for Ghost<T>

where T: Objective + ?Sized,

impl<T> Objective for GhostShared<T>

where T: Objective,

impl<T, U> Objective for Sum<T, U>

where T: Objective, U: Objective,

impl<U> Objective for AuthUpdate<U>

where U: Objective,

impl<U> Objective for OptionLocalUpdate<U>

where U: Objective,

impl<U> Objective for OptionUpdate<U>

where U: Objective,

impl<U> Objective for SumLocalUpdateL<U>

where U: Objective,

impl<U> Objective for SumLocalUpdateR<U>

where U: Objective,

impl<U> Objective for SumUpdateL<U>

where U: Objective,

impl<U> Objective for SumUpdateR<U>

where U: Objective,