Enum haybale_pitchfork::secret::BV [−][src]
pub enum BV {
Public(BV<Rc<Btor>>),
Secret {
btor: BtorRef,
width: u32,
symbol: Option<String>,
},
PartiallySecret {
secret_mask: Vec<bool>,
data: BV<Rc<Btor>>,
symbol: Option<String>,
},
}
Expand description
A wrapper around boolector::BV
which can represent either public or secret
data.
Variants
Secret
values are opaque because we don’t care about their actual value, only how they are used.
PartiallySecret
values have some secret and some not-secret bits.
Currently we make just a best-effort attempt to handle these; for now,
some functions may just fall back on treating the entire value as
Secret
.
Fields of PartiallySecret
secret_mask: Vec<bool>
A vector the length of the PartiallySecret
value’s bitwidth, where each
true
indicates that the corresponding position in the PartiallySecret
is secret, and likewise false
indicates public.
secret_mask[0]
corresponds to the bit at position 0, which is the
rightmost (least-significant) bit.
data: BV<Rc<Btor>>
A BV
, which must have bitwidth exactly equal to the length of
secret_mask
.
In positions where secret_mask
is false
, this gives the value of
the public bits.
In positions where secret_mask
is true
, the data here is invalid
and should not be used for anything.
symbol: Option<String>
Implementations
Trait Implementations
Saturating addition, unsigned. The result will be the same as normal addition, except that if the operation would (unsigned) overflow, the maximum value (for that bitwidth) is returned instead. Read more
Saturating addition, signed. The result will be the same as normal addition, except that if the operation would (signed) overflow for being too positive / too negative, the largest / smallest signed value respectively (for that bitwidth) is returned instead. Read more
Saturating subtraction, unsigned. The result will be the same as normal subtraction, except that if the operation would overflow (result in a negative number), zero is returned instead. Read more
Saturating subtraction, signed. The result will be the same as normal subtraction, except that if the operation would (signed) overflow for being too positive / too negative, the largest / smallest signed value respectively (for that bitwidth) is returned instead. Read more
Zero-extend a BV
to the specified number of bits.
The input BV
can be already the desired size (in which case this function is a no-op)
or smaller (in which case this function will extend),
but not larger (in which case this function will panic). Read more
Sign-extend a BV
to the specified number of bits.
The input BV
can be already the desired size (in which case this function is a no-op)
or smaller (in which case this function will extend),
but not larger (in which case this function will panic). Read more
Auto Trait Implementations
Blanket Implementations
Mutably borrows from an owned value. Read more