Skip to content

Commit

Permalink
implemented BoundaryConstraints struct
Browse files Browse the repository at this point in the history
  • Loading branch information
irakliyk committed Apr 4, 2022
1 parent 5fdf515 commit 18036e9
Show file tree
Hide file tree
Showing 37 changed files with 934 additions and 602 deletions.
8 changes: 7 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -176,8 +176,14 @@ impl Air for WorkAir {
// constraints don't match, an error will be thrown in the debug mode, but in release
// mode, an invalid proof will be generated which will not be accepted by any verifier.
let degrees = vec![TransitionConstraintDegree::new(3)];

// We also need to specify the exact number of assertions we will place against the
// execution trace. This number must be the same as the number of items in a vector
// returned from the get_assertions() method below.
let num_assertions = 2;

WorkAir {
context: AirContext::new(trace_info, degrees, options),
context: AirContext::new(trace_info, degrees, num_assertions, options),
start: pub_inputs.start,
result: pub_inputs.result,
}
Expand Down
14 changes: 7 additions & 7 deletions air/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -39,10 +39,10 @@ Keep in mind is that since transition constraints define algebraic relations, th
#### Constraint degrees
One of the main factors impacting proof generation time and proof size is the maximum degree of transition constraints. The higher is this degree, the larger our blowup factor needs to be. Usually, we want to keep this degree as low as possible - e.g. under 4 or 8. To accurately describe degrees of your transition constraints, keep the following in mind:

* All trace registers have degree `1`.
* When multiplying trace registers together, the degree increases by `1`. For example, if our constraint involves multiplication of two registers, the degree of this constraint will be `2`. We can describe this constraint using `TransitionConstraintDegree` struct as follows: `TransitionConstraintDegree::new(2)`.
* All trace columns have degree `1`.
* When multiplying trace columns together, the degree increases by `1`. For example, if our constraint involves multiplication of two columns, the degree of this constraint will be `2`. We can describe this constraint using `TransitionConstraintDegree` struct as follows: `TransitionConstraintDegree::new(2)`.
* Degrees of periodic columns depend on the length of their cycles, but in most cases, these degrees are very close to `1`.
* To describe a degree of a constraint involving multiplication of trace registers and periodic columns, use the `with_cycles()` constructor of `TransitionConstraintDegree` struct. For example, if our constraint involves multiplication of one trace register and one periodic column with a cycle of 32 steps, the degree can be described as: `TransitionConstraintDegree::with_cycles(1, vec![32])`.
* To describe a degree of a constraint involving multiplication of trace columns and periodic columns, use the `with_cycles()` constructor of `TransitionConstraintDegree` struct. For example, if our constraint involves multiplication of one trace column and one periodic column with a cycle of 32 steps, the degree can be described as: `TransitionConstraintDegree::with_cycles(1, vec![32])`.

In general, multiplications should be used judiciously - though, there are ways to ease this restriction a bit (check out [mulfib8](../examples/src/fibonacci/mulfib8/air.rs) example).

Expand All @@ -51,14 +51,14 @@ Assertions are used to specify that a valid execution trace of a computation mus

To define assertions for your computation, you'll need to implement `get_assertions()` function of the `Air` trait. Every computation must have at least one assertion. Assertions can be of the following types:

* A single assertion - such assertion specifies that a single cell of an execution trace must be equal to a specific value. For example: *value in register 0, step 0, must be equal to 1*.
* A periodic assertion - such assertion specifies that values in a given register at specified intervals should be equal to some values. For example: *values in register 0, steps 0, 8, 16, 24 etc. must be equal to 2*.
* A sequence assertion - such assertion specifies that values in a given register at specific intervals must be equal to a sequence of provided values. For example: *values in register 0, step 0 must be equal to 1, step 8 must be equal to 2, step 16 must be equal to 3 etc.*
* A single assertion - such assertion specifies that a single cell of an execution trace must be equal to a specific value. For example: *value in column 0, step 0, must be equal to 1*.
* A periodic assertion - such assertion specifies that values in a given column at specified intervals should be equal to some values. For example: *values in column 0, steps 0, 8, 16, 24 etc. must be equal to 2*.
* A sequence assertion - such assertion specifies that values in a given column at specific intervals must be equal to a sequence of provided values. For example: *values in column 0, step 0 must be equal to 1, step 8 must be equal to 2, step 16 must be equal to 3 etc.*

For more information on how to define assertions see the [assertions](src/air/assertions/mod.rs) module and check out the examples in the [examples crate](../examples).

### Periodic values
Sometimes, it may be useful to define a column in an execution trace which contains a set of repeating values. For example, let's say we have a register which contains value 1 on every 4th step, and 0 otherwise. Such a column can be described with a simple periodic sequence of `[1, 0, 0, 0]`.
Sometimes, it may be useful to define a column in an execution trace which contains a set of repeating values. For example, let's say we have a column which contains value 1 on every 4th step, and 0 otherwise. Such a column can be described with a simple periodic sequence of `[1, 0, 0, 0]`.

To define such columns for your computation, you can override `get_periodic_column_values()` method of the `Air` trait. The values of the periodic columns at a given step of the computation will be supplied to the `evaluate_transition()` method via the `periodic_values` parameter.

Expand Down
85 changes: 41 additions & 44 deletions air/src/air/assertions/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,19 +25,19 @@ const NO_STRIDE: usize = 0;

/// An assertion made against an execution trace.
///
/// An assertion is always placed against a single register of an execution trace, but can cover
/// 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 register
/// 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 register must be equal
/// 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 register are equal
/// 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 register must
/// 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.
///
Expand All @@ -47,7 +47,7 @@ const NO_STRIDE: usize = 0;
/// this linear complexity should be negligible.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Assertion<E: FieldElement> {
pub(super) register: usize,
pub(super) column: usize,
pub(super) first_step: usize,
pub(super) stride: usize,
pub(super) values: Vec<E>,
Expand All @@ -58,40 +58,40 @@ impl<E: FieldElement> Assertion<E> {
// --------------------------------------------------------------------------------------------
/// Returns an assertion against a single cell of an execution trace.
///
/// The returned assertion requires that the value in the specified `register` at the specified
/// The returned assertion requires that the value in the specified `column` at the specified
/// `step` is equal to the provided `value`.
pub fn single(register: usize, step: usize, value: E) -> Self {
pub fn single(column: usize, step: usize, value: E) -> Self {
Assertion {
register,
column,
first_step: step,
stride: NO_STRIDE,
values: vec![value],
}
}

/// Returns an single-value assertion against multiple cells of a single register.
/// Returns an single-value assertion against multiple cells of a single column.
///
/// The returned assertion requires that values in the specified `register` must be equal to
/// 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 periodic(register: usize, first_step: usize, stride: usize, value: E) -> Self {
validate_stride(stride, first_step, register);
pub fn periodic(column: usize, first_step: usize, stride: usize, value: E) -> Self {
validate_stride(stride, first_step, column);
Assertion {
register,
column,
first_step,
stride,
values: vec![value],
}
}

/// Returns a multi-value assertion against multiple cells of a single register.
/// Returns a multi-value assertion against multiple cells of a single column.
///
/// The returned assertion requires that values in the specified `register` must be equal to
/// 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.
///
Expand All @@ -100,21 +100,21 @@ impl<E: FieldElement> Assertion<E> {
/// * `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 sequence(register: usize, first_step: usize, stride: usize, values: Vec<E>) -> Self {
validate_stride(stride, first_step, register);
pub fn sequence(column: usize, first_step: usize, stride: usize, values: Vec<E>) -> Self {
validate_stride(stride, first_step, column);
assert!(
!values.is_empty(),
"invalid assertion for register {}: number of asserted values must be greater than zero",
register
"invalid assertion for column {}: number of asserted values must be greater than zero",
column
);
assert!(
values.len().is_power_of_two(),
"invalid assertion for register {}: number of asserted values must be a power of two, but was {}",
register,
"invalid assertion for column {}: number of asserted values must be a power of two, but was {}",
column,
values.len()
);
Assertion {
register,
column,
first_step,
stride: if values.len() == 1 { NO_STRIDE } else { stride },
values,
Expand All @@ -124,9 +124,9 @@ impl<E: FieldElement> Assertion<E> {
// PUBLIC ACCESSORS
// --------------------------------------------------------------------------------------------

/// Returns index of the register against which this assertion is placed.
pub fn register(&self) -> usize {
self.register
/// Returns index of the column against which this assertion is placed.
pub fn column(&self) -> usize {
self.column
}

/// Returns the first step of the execution trace against which this assertion is placed.
Expand Down Expand Up @@ -170,9 +170,9 @@ impl<E: FieldElement> Assertion<E> {

/// Checks if this assertion overlaps with the provided assertion.
///
/// Overlap is defined as asserting a value for the same step in the same register.
/// Overlap is defined as asserting a value for the same step in the same column.
pub fn overlaps_with(&self, other: &Assertion<E>) -> bool {
if self.register != other.register {
if self.column != other.column {
return false;
}
if self.first_step == other.first_step {
Expand All @@ -182,7 +182,7 @@ impl<E: FieldElement> Assertion<E> {
return false;
}

// at this point we know that assertions are for the same register but they start
// at this point we know that assertions are for the same column but they start
// on different steps and also have different strides

if self.first_step < other.first_step {
Expand All @@ -208,11 +208,8 @@ impl<E: FieldElement> Assertion<E> {

/// Panics if the assertion cannot be placed against an execution trace of the specified width.
pub fn validate_trace_width(&self, trace_width: usize) -> Result<(), AssertionError> {
if self.register >= trace_width {
return Err(AssertionError::TraceWidthTooShort(
self.register,
trace_width,
));
if self.column >= trace_width {
return Err(AssertionError::TraceWidthTooShort(self.column, trace_width));
}
Ok(())
}
Expand Down Expand Up @@ -309,12 +306,12 @@ impl<E: FieldElement> Assertion<E> {
// =================================================================================================

/// We define ordering of assertions to be first by stride, then by first_step, and finally by
/// register in ascending order.
/// column in ascending order.
impl<E: FieldElement> Ord for Assertion<E> {
fn cmp(&self, other: &Self) -> Ordering {
if self.stride == other.stride {
if self.first_step == other.first_step {
self.register.partial_cmp(&other.register).unwrap()
self.column.partial_cmp(&other.column).unwrap()
} else {
self.first_step.partial_cmp(&other.first_step).unwrap()
}
Expand All @@ -332,7 +329,7 @@ impl<E: FieldElement> PartialOrd for Assertion<E> {

impl<E: FieldElement> Display for Assertion<E> {
fn fmt(&self, f: &mut Formatter) -> core::fmt::Result {
write!(f, "(register={}, ", self.register)?;
write!(f, "(column={}, ", self.column)?;
match self.stride {
0 => write!(f, "step={}, ", self.first_step)?,
_ => {
Expand All @@ -351,24 +348,24 @@ impl<E: FieldElement> Display for Assertion<E> {
// HELPER FUNCTIONS
// =================================================================================================

fn validate_stride(stride: usize, first_step: usize, register: usize) {
fn validate_stride(stride: usize, first_step: usize, column: usize) {
assert!(
stride.is_power_of_two(),
"invalid assertion for register {}: stride must be a power of two, but was {}",
register,
"invalid assertion for column {}: stride must be a power of two, but was {}",
column,
stride
);
assert!(
stride >= MIN_STRIDE_LENGTH,
"invalid assertion for register {}: stride must be at least {}, but was {}",
register,
"invalid assertion for column {}: stride must be at least {}, but was {}",
column,
MIN_STRIDE_LENGTH,
stride
);
assert!(
first_step < stride,
"invalid assertion for register {}: first step must be smaller than stride ({} steps), but was {}",
register,
"invalid assertion for column {}: first step must be smaller than stride ({} steps), but was {}",
column,
stride,
first_step
);
Expand Down
Loading

0 comments on commit 18036e9

Please sign in to comment.