Skip to content

Commit

Permalink
feat: use semicolons as statement terminators (#353)
Browse files Browse the repository at this point in the history
  • Loading branch information
sydhds authored Aug 12, 2024
1 parent 2ed3288 commit ea582d4
Show file tree
Hide file tree
Showing 67 changed files with 1,435 additions and 1,431 deletions.
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

0 comments on commit ea582d4

Please sign in to comment.