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_ 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>.
Traits§
- Deep
View Clone - Cloned objects have the same deep view
- Exec
Spec Eq - Spec for the executable version of equality.
- 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 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 Unwrap - Traits for Option methods
Spec for executable version of
Option::unwrap. - 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). - ToOwned
- ToRef
ToRefandToOwnedare almost the same trait but separated to avoid type inference ambiguities.
Type Aliases§
- Spec
String - We use this special alias to tell the
exec_spec_verifiedandexec_spec_unverifiedmacros to compileSeq<char>toStringinstead ofVec<char>.