pub struct PermutationCheckBus {
pub index: BusIndex,
}Expand description
A PermutationCheckBus bus is used to establish that two multi-sets of values are equal.
Soundness requires that both the total number of messages sent and received over the bus per message is at most the field characteristic.
Fields§
§index: BusIndexImplementations§
Source§impl PermutationCheckBus
impl PermutationCheckBus
pub const fn new(index: BusIndex) -> Self
Sourcepub fn send<AB, E>(
&self,
builder: &mut AB,
message: impl IntoIterator<Item = E>,
enabled: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
pub fn send<AB, E>(
&self,
builder: &mut AB,
message: impl IntoIterator<Item = E>,
enabled: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
Send a message.
Caller must constrain enabled to be boolean.
Sourcepub fn receive<AB, E>(
&self,
builder: &mut AB,
message: impl IntoIterator<Item = E>,
enabled: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
pub fn receive<AB, E>(
&self,
builder: &mut AB,
message: impl IntoIterator<Item = E>,
enabled: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
Receive a message.
Caller must constrain enabled to be boolean.
Sourcepub fn send_or_receive<AB, E>(
&self,
builder: &mut AB,
interaction_type: PermutationInteractionType,
message: impl IntoIterator<Item = E>,
enabled: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
pub fn send_or_receive<AB, E>(
&self,
builder: &mut AB,
interaction_type: PermutationInteractionType,
message: impl IntoIterator<Item = E>,
enabled: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
Send or receive determined by interaction_type.
Caller must constrain enabled to be boolean.
Sourcepub fn interact<AB, E>(
&self,
builder: &mut AB,
message: impl IntoIterator<Item = E>,
direction: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
pub fn interact<AB, E>(
&self,
builder: &mut AB,
message: impl IntoIterator<Item = E>,
direction: impl Into<AB::Expr>,
)where
AB: InteractionBuilder,
E: Into<AB::Expr>,
Send or receive a message determined by the expression direction.
Direction = 1 means send, direction = -1 means receive, and direction = 0 means disabled.
Caller must constrain that direction is in {-1, 0, 1}.
Trait Implementations§
Source§impl Clone for PermutationCheckBus
impl Clone for PermutationCheckBus
Source§fn clone(&self) -> PermutationCheckBus
fn clone(&self) -> PermutationCheckBus
Returns a duplicate of the value. Read more
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source. Read moreSource§impl Debug for PermutationCheckBus
impl Debug for PermutationCheckBus
Source§impl PartialEq for PermutationCheckBus
impl PartialEq for PermutationCheckBus
impl Copy for PermutationCheckBus
impl Eq for PermutationCheckBus
impl StructuralPartialEq for PermutationCheckBus
Auto Trait Implementations§
impl Freeze for PermutationCheckBus
impl RefUnwindSafe for PermutationCheckBus
impl Send for PermutationCheckBus
impl Sync for PermutationCheckBus
impl Unpin for PermutationCheckBus
impl UnwindSafe for PermutationCheckBus
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
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> 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 more