Expand description
This module provides runtime utilities for the compiled
executable code of verus_builtin_macros::exec_spec_verified
and verus_builtin_macros::exec_spec_unverified.
Macros§
- exec_
spec_ type - exec_
spec_ unverified - Automatically compiles spec items to exec items, but without proofs of functional correctness.
This means that,iIn contrast to
exec_spec_verified!, all specifications on compiled executable code generated byexec_spec_unverified!are trusted. - exec_
spec_ verified - Automatically compiles spec items to exec items, with proofs of functional correctness.
Structs§
- Exec
Multiset Multiset<T>is compiled toExecMultiset<T>.
Enums§
- Exec
MemContents MemContents<T>is compiled toExecMemContents<T>
Traits§
- Deep
View Clone - Cloned objects have the same deep view
- Exec
Spec Fixed Width Arith - Exec
Spec Index - Spec for executable version of
Seqandstrindexing. - Exec
Spec Len - Spec for executable version of
len. - Exec
Spec MapDom - Spec for executable version of
Map::dom. - Exec
Spec MapEmpty - Traits for Map methods
Spec for executable version of
Map::empty. - Exec
Spec MapGet - Spec for executable version of
Map::get. - Exec
Spec MapIndex - Spec for executable version of
Mapindexing. - Exec
Spec MapInsert - Spec for executable version of
Map::insert. - Exec
Spec MapRemove - Spec for executable version of
Map::remove. - Exec
Spec MemContents - Traits for MemContents methods
Spec for executable versions of
MemContents::is_init,MemContents::is_uninit, andMemContents::value. - Exec
Spec Multiset Add - Spec for executable version of
Multiset::add. - Exec
Spec Multiset Count - Spec for executable version of
Multiset::count. - Exec
Spec Multiset Empty - Spec for executable version of
Multiset::empty. - Exec
Spec Multiset Singleton - Spec for executable version of
Multiset::singleton. - Exec
Spec Multiset Sub - Spec for executable version of
Multiset::sub. - Exec
Spec Option Arrow - Exec
Spec Option Unwrap - Traits for Option methods
Spec for executable version of
Option::unwrap. - Exec
Spec Result Arrow - Exec
Spec SeqAdd - Spec for executable version of
Seq::add. - Exec
Spec SeqContains - Spec for executable version of
Seq::contains. - Exec
Spec SeqDrop First - Spec for executable version of
Seq::drop_first. - Exec
Spec SeqDrop Last - Spec for executable version of
Seq::drop_last. - Exec
Spec SeqEmpty - Spec for executable version of
Seq::empty. - Exec
Spec SeqFirst - Spec for executable version of
Seq::first. - Exec
Spec SeqIndex Of - Spec for executable version of
Seq::index_of. - Exec
Spec SeqIndex OfFirst - Spec for executable version of
Seq::index_of_first. - Exec
Spec SeqIndex OfLast - Spec for executable version of
Seq::index_of_last. - Exec
Spec SeqIs Prefix Of - Spec for executable version of
Seq::is_prefix_of. - Exec
Spec SeqIs Suffix Of - Spec for executable version of
Seq::is_suffix_of. - Exec
Spec SeqLast - Spec for executable version of
Seq::last. - Exec
Spec SeqPush - Spec for executable version of
Seq::push. - Exec
Spec SeqSkip - Spec for executable version of
Seq::skip. - Exec
Spec SeqSubrange - Spec for executable version of
Seq::subrange. - Exec
Spec SeqTake - Spec for executable version of
Seq::take. - Exec
Spec SeqTo Multiset - Spec for executable version of
Seq::to_multiset. - Exec
Spec SeqUpdate - Spec for executable version of
Seq::update. - Exec
Spec SetContains - Spec for executable version of
Set::contains. - Exec
Spec SetDifference - Spec for executable version of
Set::difference. - Exec
Spec SetEmpty - Traits for Set methods
Spec for executable version of
Set::empty. - Exec
Spec SetInsert - Spec for executable version of
Set::insert. - Exec
Spec SetIntersect - Spec for executable version of
Set::intersect. - Exec
Spec SetRemove - Spec for executable version of
Set::remove. - Exec
Spec SetUnion - Spec for executable version of
Set::union. - Exec
Spec Type - Any spec types used in
exec_spec_verifiedorexec_spec_unverifiedmacros must implement this trait to indicate the corresponding exec type (owned and borrowed versions). - Obeys
Deep Eq - Types whose Rust equality (
==) decides deep-view equality. - ToOwned
- ToRef
ToRefandToOwnedare almost the same trait but separated to avoid type inference ambiguities.
Functions§
Type Aliases§
- Spec
String - We use this special alias to tell the
exec_spec_verifiedandexec_spec_unverifiedmacros to compileSeq<char>toStringinstead ofVec<char>.