Skip to content

Commit

Permalink
feat: add parsing of random values section
Browse files Browse the repository at this point in the history
  • Loading branch information
Fumuran committed Jan 30, 2023
1 parent 1acc36a commit 52c0aa1
Show file tree
Hide file tree
Showing 8 changed files with 36 additions and 32 deletions.
6 changes: 3 additions & 3 deletions air-script/tests/aux_trace/aux_trace.air
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,6 @@ integrity_constraints:
enf b' = c + a'
enf c = a + b

# integrity constraints against the auxiliary trace with random values
enf p0' = p0 * (a + $rand[0] + b + $rand[1])
enf p1 = p1' * (c + $rand[0])
# integrity constraints against the auxiliary trace
enf p0' = p0 * (a + b)
enf p1 = p1' * c
4 changes: 2 additions & 2 deletions air-script/tests/aux_trace/aux_trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ impl Air for AuxiliaryAir {
{
let current = aux_frame.current();
let next = aux_frame.next();
result[0] = next[0] - ((current[0]) * (current[0] + aux_rand_elements.get_segment_elements(0)[0] + current[1] + aux_rand_elements.get_segment_elements(0)[1]));
result[1] = current[1] - ((next[1]) * (current[2] + aux_rand_elements.get_segment_elements(0)[0]));
result[0] = next[0] - ((current[0]) * (current[0] + current[1]));
result[1] = current[1] - ((next[1]) * (current[2]));
}
}
4 changes: 2 additions & 2 deletions air-script/tests/variables/variables.air
Original file line number Diff line number Diff line change
Expand Up @@ -35,5 +35,5 @@ integrity_constraints:
# c = a * b when s = 1.
enf s * (c - a * b) = o[0][0] - o[0][1] - o[1][0]

# the auxiliary column contains the product of values of c offset by a random value.
enf p' = p * (c + $rand[0])
# the auxiliary column contains the product of values of c.
enf p' = p * c
2 changes: 1 addition & 1 deletion air-script/tests/variables/variables.rs
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,6 @@ impl Air for VariablesAir {
{
let current = aux_frame.current();
let next = aux_frame.next();
result[0] = next[0] - ((current[0]) * (current[3] + aux_rand_elements.get_segment_elements(0)[0]));
result[0] = next[0] - ((current[0]) * (current[3]));
}
}
1 change: 1 addition & 0 deletions parser/src/ast/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ pub struct Source(pub Vec<SourceSection>);
/// - PeriodicColumns: Periodic columns are each represented by a fixed-size array with all of its
/// elements specified. The array length is expected to be a power of 2, but this is not checked
/// during parsing.
/// - RandomValues: Random Values represent the randomness sent by the Verifier
/// - BoundaryConstraints: Boundary Constraints to be enforced on the boundaries of columns defined
/// in the TraceCols section. Currently there are two types of boundaries, First and Last
/// representing the first and last rows of the column.
Expand Down
31 changes: 17 additions & 14 deletions parser/src/ast/random_values.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ use super::Identifier;
// ================================================================================================

/// Declaration of random values for an AIR. Random values colud be represented by a named
/// identifier which is used to identify a fixed size array of length `size` and empty `values`
/// vector or by named identifier which is used to identify a `values` [RandomValue] vector and \
/// zero `size` field.
/// identifier which is used to identify a fixed size array of length `size` and empty `bindings`
/// vector or by named identifier which is used to identify a `bindings` [RandBinding] vector and
/// its `size` field.
///
/// # Examples
///
Expand All @@ -15,34 +15,36 @@ use super::Identifier;
/// ```airscript
/// random_values:
/// rand: [15]
///
/// ```
///
/// created [RandomValues] instance will look like
///
/// `RandomValues{name: "rand", size: 15, values: []}`
/// `RandomValues{name: "rand", size: 15, bindings: []}`
///
/// If random values declared in form
///
/// ```airscript
/// random_values:
/// rand: [a, b[12]]
///
/// ```
///
/// created [RandomValues] instance will look like
///
/// `RandomValues{name: "rand", size: 0, values: [RandomValue{name: "a", size: 1}, RandomValue{name: "b", size: 12}]}`
/// `RandomValues{name: "rand", size: 2, bindings: [RandBinding{name: "a", size: 1}, RandBinding{name: "b", size: 12}]}`
#[derive(Debug, Eq, PartialEq)]
pub struct RandomValues {
name: Identifier,
size: usize,
values: Vec<RandomValue>,
bindings: Vec<RandBinding>,
}

impl RandomValues {
pub(crate) fn new(name: Identifier, size: usize, values: Vec<RandomValue>) -> Self {
Self { name, size, values }
pub(crate) fn new(name: Identifier, size: usize, bindings: Vec<RandBinding>) -> Self {
Self {
name,
size,
bindings,
}
}

pub fn name(&self) -> &str {
Expand All @@ -54,18 +56,19 @@ impl RandomValues {
self.size
}

pub fn values(&self) -> &Vec<RandomValue> {
&self.values
pub fn bindings(&self) -> &Vec<RandBinding> {
&self.bindings
}
}

/// Declaration of a random value used in [RandomValues]. It is represented by a named identifier and its size.
#[derive(Debug, Eq, PartialEq)]
pub struct RandomValue {
pub struct RandBinding {
name: Identifier,
size: usize,
}

impl RandomValue {
impl RandBinding {
pub(crate) fn new(name: Identifier, size: usize) -> Self {
Self { name, size }
}
Expand Down
10 changes: 5 additions & 5 deletions parser/src/parser/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use crate::{
boundary_constraints::{Boundary, BoundaryConstraint, BoundaryStmt},
integrity_constraints::{IntegrityConstraint, IntegrityStmt},
Constant, ConstantType, Expression, Identifier, Variable, VariableType,
RandomValues, RandomValue, Source, SourceSection, Trace, TraceCols, PublicInput,
RandomValues, RandBinding, Source, SourceSection, Trace, TraceCols, PublicInput,
PeriodicColumn, IndexedTraceAccess, NamedTraceAccess, MatrixAccess, VectorAccess
}, error::{Error, ParseError::{InvalidInt, InvalidTraceCols, MissingMainTraceCols,
InvalidConst, MissingBoundaryConstraint, MissingIntegrityConstraint}}, lexer::Token
Expand Down Expand Up @@ -129,12 +129,12 @@ RandomValues: RandomValues = {
RandValues: RandomValues = {
<name: Identifier> ":" <index: Index> => RandomValues::new(name, index, vec![]),
<name: Identifier> ":" "[" "]" => RandomValues::new(name, 0, vec![]),
<name: Identifier> ":" "[" <rand_vec: CommaElems<RandElem>> "]" => RandomValues::new(name, 0, rand_vec)
<name: Identifier> ":" "[" <rand_vec: CommaElems<RandElem>> "]" => RandomValues::new(name, rand_vec.iter().map(|v| v.size()).sum::<usize>(), rand_vec)
}

RandElem: RandomValue = {
<name: Identifier> => RandomValue::new(name, 1),
<name: Identifier> <index: Index> => RandomValue::new(name, index)
RandElem: RandBinding = {
<name: Identifier> => RandBinding::new(name, 1),
<name: Identifier> <index: Index> => RandBinding::new(name, index)
}

// BOUNDARY STATEMENTS
Expand Down
10 changes: 5 additions & 5 deletions parser/src/parser/tests/random_values.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use super::{build_parse_test, Identifier, RandomValue, RandomValues, Source, SourceSection::*};
use super::{build_parse_test, Identifier, RandBinding, RandomValues, Source, SourceSection::*};

// RANDOM VALUES
// ================================================================================================
Expand All @@ -23,11 +23,11 @@ fn random_values_ident_vector_custom_name() {
alphas: [a, b[12], c]";
let expected = Source(vec![RandomValues(RandomValues::new(
Identifier("alphas".to_string()),
0,
14,
vec![
RandomValue::new(Identifier("a".to_string()), 1),
RandomValue::new(Identifier("b".to_string()), 12),
RandomValue::new(Identifier("c".to_string()), 1),
RandBinding::new(Identifier("a".to_string()), 1),
RandBinding::new(Identifier("b".to_string()), 12),
RandBinding::new(Identifier("c".to_string()), 1),
],
))]);
build_parse_test!(source).expect_ast(expected);
Expand Down

0 comments on commit 52c0aa1

Please sign in to comment.