List of all items

Structs

• cell::PermCell
• cell::PermCellOwn
• cell::PredCell
• ghost::Ghost
• ghost::PtrOwn
• ghost::local_invariant::LocalInvariant
• ghost::local_invariant::Namespace
• ghost::local_invariant::Tokens
• ghost::resource::Resource
• ghost::resource::fmap_view::Authority
• ghost::resource::fmap_view::Fragment
• invariant::Subset
• logic::FMap
• logic::Id
• logic::Int
• logic::Mapping
• logic::Set
• logic::fset::FSet
• logic::ra::agree::Ag
• logic::ra::auth::AuthUpdate
• logic::ra::auth::AuthViewRel
• logic::ra::excl::Excl
• logic::ra::excl::ExclUpdate
• logic::ra::fmap::FMapInsertLocalUpdate
• logic::ra::option::OptionUpdate
• logic::ra::prod::ProdLocalUpdate
• logic::ra::prod::ProdUpdate
• logic::ra::sum::SumLocalUpdateL
• logic::ra::sum::SumLocalUpdateR
• logic::ra::sum::SumUpdateL
• logic::ra::sum::SumUpdateR
• logic::ra::view::View
• logic::ra::view::ViewUpdate
• logic::ra::view::ViewUpdateInsert
• logic::ra::view::ViewUpdateRemove
• logic::real::Real
• logic::seq::Seq
• logic::seq::SeqIter
• logic::seq::SeqIterRef
• peano::PeanoInt
• snapshot::Snapshot
• std::iter::MapInv
• std::ptr::PtrDeepModel

Enums

• logic::ra::sum::Sum

Traits

• ghost::FnGhost
• ghost::Plain
• ghost::local_invariant::LocalInvariantExt
• ghost::local_invariant::Protocol
• invariant::InhabitedInvariant
• invariant::Invariant
• logic::WellFounded
• logic::ops::AddLogic
• logic::ops::DivLogic
• logic::ops::Fin
• logic::ops::IndexLogic
• logic::ops::MulLogic
• logic::ops::NegLogic
• logic::ops::NthBitLogic
• logic::ops::RemLogic
• logic::ops::SubLogic
• logic::ord::OrdLogic
• logic::ra::RA
• logic::ra::UnitRA
• logic::ra::update::LocalUpdate
• logic::ra::update::Update
• logic::ra::view::ViewRel
• model::DeepModel
• model::View
• prelude::Clone
• prelude::Default
• prelude::PartialEq
• resolve::Resolve
• std::char::CharExt
• std::clone::Clone
• std::cmp::PartialEq
• std::default::Default
• std::iter::ClonedExt
• std::iter::CopiedExt
• std::iter::DoubleEndedIteratorSpec
• std::iter::EnumerateExt
• std::iter::FilterExt
• std::iter::FilterMapExt
• std::iter::FromIteratorSpec
• std::iter::FusedIterator
• std::iter::IteratorSpec
• std::iter::MapExt
• std::iter::RevExt
• std::iter::SkipExt
• std::iter::TakeExt
• std::iter::ZipExt
• std::ops::FnExt
• std::ops::FnMutExt
• std::ops::FnOnceExt
• std::ops::RangeBounds
• std::ops::RangeInclusiveExt
• std::option::OptionExt
• std::ptr::PointerExt
• std::ptr::SizedPointerExt
• std::ptr::SlicePointerExt
• std::slice::SliceExt
• std::slice::SliceIndexSpec

Macros

• ghost::local_invariant::declare_namespace
• logic::ord::ord_laws_impl
• macros::extern_spec
• macros::ghost
• macros::ghost_let
• macros::pearlite
• macros::proof_assert
• macros::snapshot
• ord_laws_impl
• std::vec::vec
• vec

Attribute Macros

• macros::bitwise_proof
• macros::builtin
• macros::check
• macros::ensures
• macros::erasure
• macros::invariant
• macros::logic
• macros::maintains
• macros::opaque
• macros::open_inv_result
• macros::requires
• macros::trusted
• macros::variant

Derive Macros

• model::DeepModel
• prelude::Clone
• prelude::DeepModel
• prelude::Default
• prelude::PartialEq
• std::clone::Clone
• std::cmp::PartialEq
• std::default::Default

Functions

• invariant::inv

Type Aliases

• logic::ra::auth::Auth