pub struct ManualProof<H = ()> { /* private fields */ }Expand description
A hand-written human proof of the correctness property.
To create a manual proof, use the manual_proof! macro, which takes in a doc comment
explaining why the property holds.
Manual proofs are not trusted by the simulator, which still explores the guarded
non-determinism. H is the simulator hook payload (like crate::nondet::NonDet) so a
commutativity proof can carry an ordering hook for scripting that exploration.
Trait Implementations§
Source§impl<T, B: Boundedness> CommutativeProof<T, B> for ManualProof<Option<OrderingHook<T, B>>>
impl<T, B: Boundedness> CommutativeProof<T, B> for ManualProof<Option<OrderingHook<T, B>>>
Source§fn register_proof(&self, _expr: &Expr)
fn register_proof(&self, _expr: &Expr)
Registers the expression with the proof mechanism. Read more
Source§fn take_hook(&mut self) -> Option<OrderingHook<T, B>>
fn take_hook(&mut self) -> Option<OrderingHook<T, B>>
Takes the simulator ordering hook attached to this proof, if any.
Source§impl<T, B: Boundedness> CommutativeProof<T, B> for ManualProof
impl<T, B: Boundedness> CommutativeProof<T, B> for ManualProof
Source§fn register_proof(&self, _expr: &Expr)
fn register_proof(&self, _expr: &Expr)
Registers the expression with the proof mechanism. Read more
Source§fn take_hook(&mut self) -> Option<OrderingHook<T, B>>
fn take_hook(&mut self) -> Option<OrderingHook<T, B>>
Takes the simulator ordering hook attached to this proof, if any.
impl ConsistencyProof for ManualProof
Source§impl IdempotentProof for ManualProof
impl IdempotentProof for ManualProof
Source§fn register_proof(&self, _expr: &Expr)
fn register_proof(&self, _expr: &Expr)
Registers the expression with the proof mechanism. Read more
Source§impl MonotoneProof for ManualProof
impl MonotoneProof for ManualProof
Source§fn register_proof(&self, _expr: &Expr)
fn register_proof(&self, _expr: &Expr)
Registers the expression with the proof mechanism. Read more
Source§impl OrderPreservingProof for ManualProof
impl OrderPreservingProof for ManualProof
Source§fn register_proof(&self, _expr: &Expr)
fn register_proof(&self, _expr: &Expr)
Registers the expression with the proof mechanism. Read more
Auto Trait Implementations§
impl<H> Freeze for ManualProof<H>where
H: Freeze,
impl<H> RefUnwindSafe for ManualProof<H>where
H: RefUnwindSafe,
impl<H> Send for ManualProof<H>where
H: Send,
impl<H> Sync for ManualProof<H>where
H: Sync,
impl<H> Unpin for ManualProof<H>where
H: Unpin,
impl<H> UnsafeUnpin for ManualProof<H>where
H: UnsafeUnpin,
impl<H> UnwindSafe for ManualProof<H>where
H: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self> ⓘ
fn instrument(self, span: Span) -> Instrumented<Self> ⓘ
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self> ⓘ
fn into_either(self, into_left: bool) -> Either<Self, Self> ⓘ
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self> ⓘ
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self> ⓘ
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreCreates a shared type from an unshared type.