pub trait CommutativeProof<T, B: Boundedness>: Sealed<T, B> {
// Required methods
fn register_proof(&self, expr: &Expr);
fn take_hook(&mut self) -> Option<OrderingHook<T, B>>;
}Expand description
A trait for proof mechanisms that can validate commutativity.
T and B name the element type and boundedness of the stream the commutative
function consumes. The simulator does not trust commutativity proofs — it still
explores the input ordering — so a proof may carry an OrderingHook for scripting
that exploration, surfaced through Self::take_hook.
Required Methods§
Sourcefn register_proof(&self, expr: &Expr)
fn register_proof(&self, expr: &Expr)
Registers the expression with the proof mechanism.
This should not perform any blocking analysis; it is only intended to record the expression for later processing.
Sourcefn 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.
Dyn Compatibility§
This trait is dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".