Struct winter_verifier::Assertion

pub struct Assertion<E>where
    E: FieldElement,{ /* private fields */ }

An assertion made against an execution trace.

An assertion is always placed against a single column of an execution trace, but can cover multiple steps and multiple values. Specifically, there are three kinds of assertions:

1. Single assertion - which requires that a value in a single cell of an execution trace is equal to the specified value.
2. Periodic assertion - which requires that values in multiple cells of a single column are equal to the specified value. The cells must be evenly spaced at intervals with lengths equal to powers of two. For example, we can specify that values in a column must be equal to 0 at steps 0, 8, 16, 24, 32 etc. Steps can also start at some offset - e.g., 1, 9, 17, 25, 33 is also a valid sequence of steps.
3. Sequence assertion - which requires that multiple cells in a single column are equal to the values from the provided list. The cells must be evenly spaced at intervals with lengths equal to powers of two. For example, we can specify that values in a column must be equal to a sequence 1, 2, 3, 4 at steps 0, 8, 16, 24. That is, value at step 0 should be equal to 1, value at step 8 should be equal to 2 etc.

Note that single and periodic assertions are succinct. That is, a verifier can evaluate them very efficiently. However, sequence assertions have liner complexity in the number of asserted values. Though, unless many thousands of values are asserted, practical impact of this linear complexity should be negligible.

Implementations

impl<E> Assertion<E>where
    E: FieldElement,

pub fn single(column: usize, step: usize, value: E) -> Assertion<E>

Returns an assertion against a single cell of an execution trace.

The returned assertion requires that the value in the specified column at the specified step is equal to the provided value.

pub fn periodic(
    column: usize,
    first_step: usize,
    stride: usize,
    value: E
) -> Assertion<E>

Returns an single-value assertion against multiple cells of a single column.

The returned assertion requires that values in the specified column must be equal to the specified value at steps which start at first_step and repeat in equal intervals specified by stride.

Panics

Panics if:

• stride is not a power of two, or is smaller than 2.
• first_step is greater than stride.

pub fn sequence(
    column: usize,
    first_step: usize,
    stride: usize,
    values: Vec<E, Global>
) -> Assertion<E>

Returns a multi-value assertion against multiple cells of a single column.

The returned assertion requires that values in the specified column must be equal to the provided values at steps which start at first_step and repeat in equal intervals specified by stride until all values have been consumed.

Panics

Panics if:

• stride is not a power of two, or is smaller than 2.
• first_step is greater than stride.
• values is empty or number of values in not a power of two.

pub fn column(&self) -> usize

Returns index of the column against which this assertion is placed.

pub fn first_step(&self) -> usize

Returns the first step of the execution trace against which this assertion is placed.

For single value assertions this is equivalent to the assertion step.

pub fn stride(&self) -> usize

Returns the interval at which the assertion repeats in the execution trace.

For single value assertions, this will be 0.

pub fn values(&self) -> &[E]

Returns asserted values.

For single value and periodic assertions this will be a slice containing one value.

pub fn is_single(&self) -> bool

Returns true if this is a single-value assertion (one value, one step).

pub fn is_periodic(&self) -> bool

Returns true if this is a periodic assertion (one value, many steps).

pub fn is_sequence(&self) -> bool

Returns true if this is a sequence assertion (many values, many steps).

pub fn overlaps_with(&self, other: &Assertion<E>) -> bool

Checks if this assertion overlaps with the provided assertion.

Overlap is defined as asserting a value for the same step in the same column.

pub fn validate_trace_width(
    &self,
    trace_width: usize
) -> Result<(), AssertionError>

Panics if the assertion cannot be placed against an execution trace of the specified width.

pub fn validate_trace_length(
    &self,
    trace_length: usize
) -> Result<(), AssertionError>

Checks if the assertion is valid against an execution trace of the specified length.

Errors

Returns an error if:

• trace_length is not a power of two.
• For single assertion, first_step >= trace_length.
• For periodic assertion, stride > trace_length.
• For sequence assertion, num_values * stride != trace_length;

pub fn apply<F>(&self, trace_length: usize, f: F)where
    F: FnMut(usize, E),

Executes the provided closure for all possible instantiations of this assertions against a execution trace of the specified length.

Panics

Panics if the specified trace length is not valid for this assertion.

pub fn get_num_steps(&self, trace_length: usize) -> usize

Returns the number of steps against which this assertion will be applied given an execution trace of the specified length.

• For single-value assertions, this will always be one.
• For periodic assertions this will be equal to trace_length / stride.
• For sequence assertions this will be equal to the number of asserted values.

Panics

Panics if the specified trace length is not valid for this assertion.

Trait Implementations

impl<E> Clone for Assertion<E>where
    E: Clone + FieldElement,

fn clone(&self) -> Assertion<E>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<E> Debug for Assertion<E>where
    E: Debug + FieldElement,

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<E> Display for Assertion<E>where
    E: FieldElement,

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<E> Ord for Assertion<E>where
    E: FieldElement,

We define ordering of assertions to be first by stride, then by first_step, and finally by column in ascending order.

fn cmp(&self, other: &Assertion<E>) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Selfwhere
    Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Selfwhere
    Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Selfwhere
    Self: Sized + PartialOrd<Self>,

Restrict a value to a certain interval.

impl<E> PartialEq<Assertion<E>> for Assertion<E>where
    E: PartialEq<E> + FieldElement,

fn eq(&self, other: &Assertion<E>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<E> PartialOrd<Assertion<E>> for Assertion<E>where
    E: FieldElement,

fn partial_cmp(&self, other: &Assertion<E>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

This method tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

This method tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

This method tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl<E> Eq for Assertion<E>where
    E: Eq + FieldElement,

impl<E> StructuralEq for Assertion<E>where
    E: FieldElement,

impl<E> StructuralPartialEq for Assertion<E>where
    E: FieldElement,