Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add semicolon 1 #2

Draft
wants to merge 8 commits into
base: next
Choose a base branch
from
30 changes: 15 additions & 15 deletions air-script/tests/aux_trace/aux_trace.air
Original file line number Diff line number Diff line change
@@ -1,36 +1,36 @@
def AuxiliaryAir

trace_columns {
main: [a, b, c]
aux: [p0, p1]
main: [a, b, c],
aux: [p0, p1],
}

public_inputs {
stack_inputs: [16]
stack_inputs: [16],
}

random_values {
rand: [2]
rand: [2],
}

boundary_constraints {
enf a.first = 1
enf b.first = 1
enf a.first = 1;
enf b.first = 1;

enf p0.first = 1
enf p0.last = 1
enf p0.first = 1;
enf p0.last = 1;

# auxiliary boundary constraint with a random value
enf p1.first = $rand[0]
enf p1.last = 1
enf p1.first = $rand[0];
enf p1.last = 1;
}

integrity_constraints {
enf a' = b + a * b * c
enf b' = c + a'
enf c = a + b
enf a' = b + a * b * c;
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])
enf p0' = p0 * (a + $rand[0] + b + $rand[1]);
enf p1 = p1' * (c + $rand[0]);
}
10 changes: 5 additions & 5 deletions air-script/tests/binary/binary.air
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
def BinaryAir

trace_columns {
main: [a, b]
main: [a, b],
}

public_inputs {
stack_inputs: [16]
stack_inputs: [16],
}

boundary_constraints {
enf a.first = 0
enf a.first = 0;
}

integrity_constraints {
enf a^2 - a = 0
enf b^2 - b = 0
enf a^2 - a = 0;
enf b^2 - b = 0;
}
44 changes: 22 additions & 22 deletions air-script/tests/bitwise/bitwise.air
Original file line number Diff line number Diff line change
@@ -1,58 +1,58 @@
def BitwiseAir

public_inputs {
stack_inputs: [16]
stack_inputs: [16],
}

trace_columns {
main: [s, a, b, a0, a1, a2, a3, b0, b1, b2, b3, zp, z, dummy]
main: [s, a, b, a0, a1, a2, a3, b0, b1, b2, b3, zp, z, dummy],
}

periodic_columns {
k0: [1, 0, 0, 0, 0, 0, 0, 0]
k1: [1, 1, 1, 1, 1, 1, 1, 0]
k0: [1, 0, 0, 0, 0, 0, 0, 0],
k1: [1, 1, 1, 1, 1, 1, 1, 0],
}

boundary_constraints {
# This is a dummy trace column to satisfy requirement of at least one boundary constraint.
enf dummy.first = 0
enf dummy.first = 0;
}

integrity_constraints {
# Enforce that selector must be binary
enf s^2 - s = 0
enf s^2 - s = 0;

# Enforce that selector should stay the same throughout the cycle.
enf k1 * (s' - s) = 0
enf k1 * (s' - s) = 0;

# Enforce that input is decomposed into valid bits
enf a0^2 - a0 = 0
enf a1^2 - a1 = 0
enf a2^2 - a2 = 0
enf a3^2 - a3 = 0
enf b0^2 - b0 = 0
enf b1^2 - b1 = 0
enf b2^2 - b2 = 0
enf b3^2 - b3 = 0
enf a0^2 - a0 = 0;
enf a1^2 - a1 = 0;
enf a2^2 - a2 = 0;
enf a3^2 - a3 = 0;
enf b0^2 - b0 = 0;
enf b1^2 - b1 = 0;
enf b2^2 - b2 = 0;
enf b3^2 - b3 = 0;

# Enforce that the values in the column a in the first row should be the aggregation of the
# decomposed bit columns a0..a3.
enf k0 * (a - (2^0 * a0 + 2^1 * a1 + 2^2 * a2 + 2^3 * a3)) = 0
enf k0 * (a - (2^0 * a0 + 2^1 * a1 + 2^2 * a2 + 2^3 * a3)) = 0;
# Enforce that the values in the column b in the first row should be the aggregation of the
# decomposed bit columns b0..b3.
enf k0 * (b - (2^0 * b0 + 2^1 * b1 + 2^2 * b2 + 2^3 * b3)) = 0
enf k0 * (b - (2^0 * b0 + 2^1 * b1 + 2^2 * b2 + 2^3 * b3)) = 0;

# Enforce that for all rows in an 8-row cycle except for the last one, the values in a and b
# columns are increased by the values contained in the individual bit columns a and b.
enf k1 * (a' - (a * 16 + 2^0 * a0 + 2^1 * a1 + 2^2 * a2 + 2^3 * a3)) = 0
enf k1 * (b' - (b * 16 + 2^0 * b0 + 2^1 * b1 + 2^2 * b2 + 2^3 * b3)) = 0
enf k1 * (a' - (a * 16 + 2^0 * a0 + 2^1 * a1 + 2^2 * a2 + 2^3 * a3)) = 0;
enf k1 * (b' - (b * 16 + 2^0 * b0 + 2^1 * b1 + 2^2 * b2 + 2^3 * b3)) = 0;

# Enforce that in the first row, the aggregated output value of the previous row should be 0.
enf k0 * zp = 0
enf k0 * zp = 0;

# Enforce that for each row except the last, the aggregated output value must equal the
# previous aggregated output value in the next row.
enf k1 * (z - zp') = 0
enf k1 * (z - zp') = 0;

# Enforce that for all rows the value in the z column is computed by multiplying the previous
# output value (from the zp column in the current row) by 16 and then adding it to the bitwise
Expand All @@ -62,5 +62,5 @@ integrity_constraints {
# enforced when s = 1. Because the selectors for the AND and XOR operations are mutually
# exclusive, the constraints for different operations can be aggregated into the same result
# indices.
enf (1 - s) * (z - (zp * 16 + 2^0 * a0 * b0 + 2^1 * a1 * b1 + 2^2 * a2 * b2 + 2^3 * a3 * b3)) + s * (z - (zp * 16 + 2^0 * (a0 + b0 - 2 * a0 * b0) + 2^1 * (a1 + b1 - 2 * a1 * b1) + 2^2 * (a2 + b2 - 2 * a2 * b2) + 2^3 * (a3 + b3 - 2 * a3 * b3))) = 0
enf (1 - s) * (z - (zp * 16 + 2^0 * a0 * b0 + 2^1 * a1 * b1 + 2^2 * a2 * b2 + 2^3 * a3 * b3)) + s * (z - (zp * 16 + 2^0 * (a0 + b0 - 2 * a0 * b0) + 2^1 * (a1 + b1 - 2 * a1 * b1) + 2^2 * (a2 + b2 - 2 * a2 * b2) + 2^3 * (a3 + b3 - 2 * a3 * b3))) = 0;
}
40 changes: 20 additions & 20 deletions air-script/tests/constants/constants.air
Original file line number Diff line number Diff line change
@@ -1,34 +1,34 @@
def ConstantsAir

const A = 1
const B = [0, 1]
const C = [[1, 2], [2, 0]]
const A = 1;
const B = [0, 1];
const C = [[1, 2], [2, 0]];

trace_columns {
main: [a, b, c, d]
aux: [e, f, g]
main: [a, b, c, d],
aux: [e, f, g],
}

public_inputs {
program_hash: [4]
stack_inputs: [4]
stack_outputs: [20]
overflow_addrs: [4]
program_hash: [4],
stack_inputs: [4],
stack_outputs: [20],
overflow_addrs: [4],
}

boundary_constraints {
enf a.first = A
enf b.first = A + B[0] * C[0][1]
enf c.first = (B[0] - C[1][1]) * A
enf d.first = A + B[0] - B[1] + C[0][0] - C[0][1] + C[1][0] - C[1][1]
enf e.first = A + B[0] * C[0][1]
enf e.last = A - B[1] * C[0][0]
enf a.first = A;
enf b.first = A + B[0] * C[0][1];
enf c.first = (B[0] - C[1][1]) * A;
enf d.first = A + B[0] - B[1] + C[0][0] - C[0][1] + C[1][0] - C[1][1];
enf e.first = A + B[0] * C[0][1];
enf e.last = A - B[1] * C[0][0];
}

integrity_constraints {
enf a' = a + A
enf b' = B[0] * b
enf c' = (C[0][0] + B[0]) * c
enf e' = e + A + B[0] * C[0][1]
enf e = A + B[1] * C[1][1]
enf a' = a + A;
enf b' = B[0] * b;
enf c' = (C[0][0] + B[0]) * c;
enf e' = e + A + B[0] * C[0][1];
enf e = A + B[1] * C[1][1];
}
12 changes: 6 additions & 6 deletions air-script/tests/constraint_comprehension/cc_with_evaluators.air
Original file line number Diff line number Diff line change
@@ -1,22 +1,22 @@
def ConstraintComprehensionAir

ev are_equal([], [x, y]) {
enf x = y
enf x = y;
}

trace_columns {
main: [clk, fmp[2], ctx]
aux: [a, b, c[4], d[4]]
main: [clk, fmp[2], ctx],
aux: [a, b, c[4], d[4]],
}

public_inputs {
stack_inputs: [16]
stack_inputs: [16],
}

boundary_constraints {
enf c[2].first = 0
enf c[2].first = 0;
}

integrity_constraints {
enf are_equal([], [c, d]) for (c, d) in (c, d)
enf are_equal([], [c, d]) for (c, d) in (c, d);
}
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
def ConstraintComprehensionAir

trace_columns {
main: [clk, fmp[2], ctx]
aux: [a, b, c[4], d[4]]
main: [clk, fmp[2], ctx],
aux: [a, b, c[4], d[4]],
}

public_inputs {
stack_inputs: [16]
stack_inputs: [16],
}

boundary_constraints {
enf c[2].first = 0
enf c[2].first = 0;
}

integrity_constraints {
enf c = d for (c, d) in (c, d)
enf c = d for (c, d) in (c, d);
}
22 changes: 11 additions & 11 deletions air-script/tests/evaluators/evaluators.air
Original file line number Diff line number Diff line change
@@ -1,33 +1,33 @@
def EvaluatorsAir

ev are_unchanged([x, y, z]) {
enf x' = x
enf y' = y
enf z' = z
enf x' = x;
enf y' = y;
enf z' = z;
}

ev is_binary([x]) {
enf x^2 = x
enf x^2 = x;
}

ev are_all_binary([c[3]]) {
enf is_binary([c]) for c in c
enf is_binary([c]) for c in c;
}

trace_columns {
main: [b, c[3], d[3]]
main: [b, c[3], d[3]],
}

public_inputs {
stack_inputs: [16]
stack_inputs: [16],
}

boundary_constraints {
enf b.first = 0
enf b.first = 0;
}

integrity_constraints {
enf are_unchanged([b, c[1], d[2]])
enf is_binary([b])
enf are_all_binary([c])
enf are_unchanged([b, c[1], d[2]]);
enf is_binary([b]);
enf are_all_binary([c]);
}
40 changes: 20 additions & 20 deletions air-script/tests/functions/functions_complex.air
Original file line number Diff line number Diff line change
@@ -1,45 +1,45 @@
def FunctionsAir

fn get_multiplicity_flags(s0: felt, s1: felt) -> felt[4] {
return [!s0 & !s1, s0 & !s1, !s0 & s1, s0 & s1]
return [!s0 & !s1, s0 & !s1, !s0 & s1, s0 & s1];
}

fn fold_vec(a: felt[12]) -> felt {
return sum([x for x in a])
return sum([x for x in a]);
}

fn fold_scalar_and_vec(a: felt, b: felt[12]) -> felt {
let m = fold_vec(b)
let n = m + 1
let o = n * 2
return o
let m = fold_vec(b);
let n = m + 1;
let o = n * 2;
return o;
}

trace_columns {
main: [t, s0, s1, v, b[12]]
aux: [b_range]
main: [t, s0, s1, v, b[12]],
aux: [b_range],
}

public_inputs {
stack_inputs: [16]
stack_inputs: [16],
}

random_values {
alpha: [16]
alpha: [16],
}

boundary_constraints {
enf v.first = 0
enf v.first = 0;
}

integrity_constraints {
# let val = $alpha[0] + v
let f = get_multiplicity_flags(s0, s1)
let z = v^7 * f[3] + v^2 * f[2] + v * f[1] + f[0]
# let folded_value = fold_scalar_and_vec(v, b)
enf b_range' = b_range * (z * t - t + 1)
# enf b_range' = b_range * 2
let y = fold_scalar_and_vec(v, b)
# let c = fold_scalar_and_vec(t, b)
enf v' = y
# let val = $alpha[0] + v;
let f = get_multiplicity_flags(s0, s1);
let z = v^7 * f[3] + v^2 * f[2] + v * f[1] + f[0];
# let folded_value = fold_scalar_and_vec(v, b);
enf b_range' = b_range * (z * t - t + 1);
# enf b_range' = b_range * 2;
let y = fold_scalar_and_vec(v, b);
# let c = fold_scalar_and_vec(t, b);
enf v' = y;
}
Loading