pub struct Widths { /* private fields */ }Expand description
How wide each thing in one rule is.
A rule is written at one width, the one its pattern’s opcode names, and the terms inside it
may say another: (value.i64 x) under an add.i32 is a thirty two bit add of two sixty four
bit registers, which is the shape every sext, zext and trunc in a lowering has. What a
name stands at is fixed by the pattern, because the pattern is where a name is bound, and
everywhere else reads it from here.
A bounded proof asks the same rule at a narrower width, and that scales every width in the rule by one ratio rather than flattening them all to one number. A rule that converts between widths still converts between widths when it is asked at eight bits, which it would not do if the narrow width were simply substituted everywhere.
Implementations§
Source§impl Widths
impl Widths
Sourcepub fn of(pattern: &Term) -> Widths
pub fn of(pattern: &Term) -> Widths
The widths one rule’s pattern fixes, at the width the rule is written in.
Sourcepub fn at(pattern: &Term, asked: u32) -> Widths
pub fn at(pattern: &Term, asked: u32) -> Widths
The same, scaled to a width somebody asked for. This is what a bounded proof is made of.
Sourcepub fn natural(&self) -> u32
pub fn natural(&self) -> u32
The width the rule is written in, which is the one it will run at.
Sourcepub fn names(&self) -> impl Iterator<Item = (&str, u32)>
pub fn names(&self) -> impl Iterator<Item = (&str, u32)>
Every name the pattern binds and how wide it is, sorted.
Sorted rather than in the order the pattern binds them, because the query is something a test pins and a diff is easier to read than it is to regenerate.
Sourcepub fn with(&self, name: &str, sort: Sort) -> Widths
pub fn with(&self, name: &str, sort: Sort) -> Widths
These widths and one more name, which is how the replacement’s own meaning gets a width
once it has been substituted into the specification for (result).
A replacement that computes a memory is recorded as one, so that the specification which reads it back is checked against a memory rather than against a number of bits nobody meant.
Sourcepub fn byte(&self) -> u32
pub fn byte(&self) -> u32
How wide a byte is here, scaled like everything else.
A bounded proof asks a rule in narrower bitvectors, and a byte narrows with them. It has to: the bytes a load puts together have to add up to the value the load produces, and a value that has been scaled and bytes that have not do not add up to anything.