From 20817063a58b789f81becc731008ce46c19d6c41 Mon Sep 17 00:00:00 2001 From: tohrnii <100405913+tohrnii@users.noreply.github.com> Date: Tue, 15 Nov 2022 05:26:30 +0000 Subject: [PATCH 1/3] add DS_Store to gitignore --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index 3f1702566..7c83be929 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,9 @@ # will have compiled files and executables /target/ +# Remove system config files generated by mac os +**/.DS_Store + # Remove Cargo.lock from gitignore if creating an executable, leave it for libraries # More information here https://doc.rust-lang.org/cargo/guide/cargo-toml-vs-cargo-lock.html Cargo.lock From f3ffa21bf937e2c9f1413de6db40f53fa2202a90 Mon Sep 17 00:00:00 2001 From: tohrnii <100405913+tohrnii@users.noreply.github.com> Date: Tue, 15 Nov 2022 05:28:09 +0000 Subject: [PATCH 2/3] refactor(examples): refactor bitwise air constraints to have currently supported syntax --- examples/bitwise.air | 61 +++++++++++++++++++++++++++++++++++++++++ examples/pub_inputs.air | 24 ++++++++++++++++ 2 files changed, 85 insertions(+) create mode 100644 examples/bitwise.air create mode 100644 examples/pub_inputs.air diff --git a/examples/bitwise.air b/examples/bitwise.air new file mode 100644 index 000000000..1d74a749b --- /dev/null +++ b/examples/bitwise.air @@ -0,0 +1,61 @@ +def BitwiseAir + +public_inputs: + stack_inputs: [16] + +trace_columns: + 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] + +boundary_constraints: + # This is a dummy trace column to satisfy requirement of at least one boundary constraint. + enf dummy.first = 0 + +transition_constraints: + # Enforce that selector must be binary + enf s^2 - s = 0 + + # Enforce that selector should stay the same throughout the cycle. + 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 + + # 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 + # 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 + + # 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 + + # Enforce that in the first row, the aggregated output value of the previous row should be 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 + + # 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 + # operation applied to the row's set of bits of a and b. The entire constraint must also be + # multiplied by the operation selector flag to ensure it is only applied for the appropriate + # operation. The constraint for AND is enforced when s = 0 and the constraint for XOR is + # 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 \ No newline at end of file diff --git a/examples/pub_inputs.air b/examples/pub_inputs.air new file mode 100644 index 000000000..786f5854e --- /dev/null +++ b/examples/pub_inputs.air @@ -0,0 +1,24 @@ +def PubInputsAir + +trace_columns: + main: [a, b, c, d] + +public_inputs: + program_hash: [4] + stack_inputs: [4] + stack_outputs: [20] + overflow_addrs: [4] + +boundary_constraints: + enf a.first = stack_inputs[0] + enf b.first = stack_inputs[1] + enf c.first = stack_inputs[2] + enf d.first = stack_inputs[3] + + enf a.last = stack_outputs[0] + enf b.last = stack_outputs[1] + enf c.last = stack_outputs[2] + enf d.last = stack_outputs[3] + +transition_constraints: + enf a' = b + c From 1d5c67077e51470cdd68aaa6d3c4232bd3bb08ba Mon Sep 17 00:00:00 2001 From: tohrnii <100405913+tohrnii@users.noreply.github.com> Date: Fri, 25 Nov 2022 11:26:01 +0000 Subject: [PATCH 3/3] test: add bitwise air constraints with currently supported syntax --- .../tests/bitwise}/bitwise.air | 0 air-script/tests/bitwise/bitwise.rs | 102 ++++++++++++++++++ air-script/tests/main.rs | 10 ++ examples/pub_inputs.air | 24 ----- 4 files changed, 112 insertions(+), 24 deletions(-) rename {examples => air-script/tests/bitwise}/bitwise.air (100%) create mode 100644 air-script/tests/bitwise/bitwise.rs delete mode 100644 examples/pub_inputs.air diff --git a/examples/bitwise.air b/air-script/tests/bitwise/bitwise.air similarity index 100% rename from examples/bitwise.air rename to air-script/tests/bitwise/bitwise.air diff --git a/air-script/tests/bitwise/bitwise.rs b/air-script/tests/bitwise/bitwise.rs new file mode 100644 index 000000000..3d9ed4409 --- /dev/null +++ b/air-script/tests/bitwise/bitwise.rs @@ -0,0 +1,102 @@ +use winter_air::{Air, AirContext, Assertion, AuxTraceRandElements, EvaluationFrame, ProofOptions as WinterProofOptions, TransitionConstraintDegree, TraceInfo}; +use winter_math::{fields, ExtensionOf, FieldElement}; +use winter_utils::{collections, ByteWriter, Serializable}; + +pub struct PublicInputs { + stack_inputs: [Felt; 16], +} + +impl PublicInputs { + pub fn new(stack_inputs: [Felt; 16]) -> Self { + Self { stack_inputs } + } +} + +impl Serializable for PublicInputs { + fn write_into(&self, target: &mut W) { + target.write(self.stack_inputs.as_slice()); + } +} + +pub struct BitwiseAir { + context: AirContext, + stack_inputs: [Felt; 16], +} + +impl BitwiseAir { + pub fn last_step(&self) -> usize { + self.trace_length() - self.context().num_transition_exemptions() + } +} + +impl Air for BitwiseAir { + type BaseField = Felt; + type PublicInputs = PublicInputs; + + fn context(&self) -> &AirContext { + &self.context + } + + fn new(trace_info: TraceInfo, public_inputs: PublicInputs, options: WinterProofOptions) -> Self { + let main_degrees = vec![TransitionConstraintDegree::new(2), TransitionConstraintDegree::with_cycles(1, vec![8]), TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2), TransitionConstraintDegree::new(2), TransitionConstraintDegree::with_cycles(1, vec![8]), TransitionConstraintDegree::with_cycles(1, vec![8]), TransitionConstraintDegree::with_cycles(1, vec![8]), TransitionConstraintDegree::with_cycles(1, vec![8]), TransitionConstraintDegree::with_cycles(1, vec![8]), TransitionConstraintDegree::with_cycles(1, vec![8]), TransitionConstraintDegree::new(3)]; + let aux_degrees = Vec::new(); + let num_main_assertions = 1; + let num_aux_assertions = 0; + + let context = AirContext::new_multi_segment( + trace_info, + main_degrees, + aux_degrees, + num_main_assertions, + num_aux_assertions, + options, + ) + .set_num_transition_exemptions(2); + Self { context, stack_inputs: public_inputs.stack_inputs } + } + + fn get_periodic_column_values(&self) -> Vec> { + vec![vec![Felt::new(1), Felt::new(0), Felt::new(0), Felt::new(0), Felt::new(0), Felt::new(0), Felt::new(0), Felt::new(0)], vec![Felt::new(1), Felt::new(1), Felt::new(1), Felt::new(1), Felt::new(1), Felt::new(1), Felt::new(1), Felt::new(0)]] + } + + fn get_assertions(&self) -> Vec> { + let mut result = Vec::new(); + result.push(Assertion::single(13, 0, Felt::new(0))); + result + } + + fn get_aux_assertions>(&self, aux_rand_elements: &AuxTraceRandElements) -> Vec> { + let mut result = Vec::new(); + result + } + + fn evaluate_transition>(&self, frame: &EvaluationFrame, periodic_values: &[E], result: &mut [E]) { + let current = frame.current(); + let next = frame.next(); + result[0] = (current[0]).exp(E::PositiveInteger::from(2_u64)) - (current[0]) - (E::from(0_u64)); + result[1] = (periodic_values[1]) * (next[0] - (current[0])) - (E::from(0_u64)); + result[2] = (current[3]).exp(E::PositiveInteger::from(2_u64)) - (current[3]) - (E::from(0_u64)); + result[3] = (current[4]).exp(E::PositiveInteger::from(2_u64)) - (current[4]) - (E::from(0_u64)); + result[4] = (current[5]).exp(E::PositiveInteger::from(2_u64)) - (current[5]) - (E::from(0_u64)); + result[5] = (current[6]).exp(E::PositiveInteger::from(2_u64)) - (current[6]) - (E::from(0_u64)); + result[6] = (current[7]).exp(E::PositiveInteger::from(2_u64)) - (current[7]) - (E::from(0_u64)); + result[7] = (current[8]).exp(E::PositiveInteger::from(2_u64)) - (current[8]) - (E::from(0_u64)); + result[8] = (current[9]).exp(E::PositiveInteger::from(2_u64)) - (current[9]) - (E::from(0_u64)); + result[9] = (current[10]).exp(E::PositiveInteger::from(2_u64)) - (current[10]) - (E::from(0_u64)); + result[10] = (periodic_values[0]) * (current[1] - (((E::from(2_u64)).exp(E::PositiveInteger::from(0_u64))) * (current[3]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(1_u64))) * (current[4]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(2_u64))) * (current[5]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(3_u64))) * (current[6]))) - (E::from(0_u64)); + result[11] = (periodic_values[0]) * (current[2] - (((E::from(2_u64)).exp(E::PositiveInteger::from(0_u64))) * (current[7]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(1_u64))) * (current[8]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(2_u64))) * (current[9]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(3_u64))) * (current[10]))) - (E::from(0_u64)); + result[12] = (periodic_values[1]) * (next[1] - ((current[1]) * (E::from(16_u64)) + ((E::from(2_u64)).exp(E::PositiveInteger::from(0_u64))) * (current[3]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(1_u64))) * (current[4]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(2_u64))) * (current[5]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(3_u64))) * (current[6]))) - (E::from(0_u64)); + result[13] = (periodic_values[1]) * (next[2] - ((current[2]) * (E::from(16_u64)) + ((E::from(2_u64)).exp(E::PositiveInteger::from(0_u64))) * (current[7]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(1_u64))) * (current[8]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(2_u64))) * (current[9]) + ((E::from(2_u64)).exp(E::PositiveInteger::from(3_u64))) * (current[10]))) - (E::from(0_u64)); + result[14] = (periodic_values[0]) * (current[11]) - (E::from(0_u64)); + result[15] = (periodic_values[1]) * (current[12] - (next[11])) - (E::from(0_u64)); + result[16] = (E::from(1_u64) - (current[0])) * (current[12] - ((current[11]) * (E::from(16_u64)) + (((E::from(2_u64)).exp(E::PositiveInteger::from(0_u64))) * (current[3])) * (current[7]) + (((E::from(2_u64)).exp(E::PositiveInteger::from(1_u64))) * (current[4])) * (current[8]) + (((E::from(2_u64)).exp(E::PositiveInteger::from(2_u64))) * (current[5])) * (current[9]) + (((E::from(2_u64)).exp(E::PositiveInteger::from(3_u64))) * (current[6])) * (current[10]))) + (current[0]) * (current[12] - ((current[11]) * (E::from(16_u64)) + ((E::from(2_u64)).exp(E::PositiveInteger::from(0_u64))) * (current[3] + current[7] - (((E::from(2_u64)) * (current[3])) * (current[7]))) + ((E::from(2_u64)).exp(E::PositiveInteger::from(1_u64))) * (current[4] + current[8] - (((E::from(2_u64)) * (current[4])) * (current[8]))) + ((E::from(2_u64)).exp(E::PositiveInteger::from(2_u64))) * (current[5] + current[9] - (((E::from(2_u64)) * (current[5])) * (current[9]))) + ((E::from(2_u64)).exp(E::PositiveInteger::from(3_u64))) * (current[6] + current[10] - (((E::from(2_u64)) * (current[6])) * (current[10]))))) - (E::from(0_u64)); + } + + fn evaluate_aux_transition(&self, main_frame: &EvaluationFrame, aux_frame: &EvaluationFrame, _periodic_values: &[F], aux_rand_elements: &AuxTraceRandElements, result: &mut [E]) + where F: FieldElement, + E: FieldElement + ExtensionOf, + { + let current = aux_frame.current(); + let next = aux_frame.next(); + } +} \ No newline at end of file diff --git a/air-script/tests/main.rs b/air-script/tests/main.rs index f5c8fdf1b..a9d29ef6a 100644 --- a/air-script/tests/main.rs +++ b/air-script/tests/main.rs @@ -55,3 +55,13 @@ fn system() { let expected = expect_file!["system/system.rs"]; expected.assert_eq(&generated_air); } + +#[test] +fn bitwise() { + let generated_air = Test::new("tests/bitwise/bitwise.air".to_string()) + .transpile() + .unwrap(); + + let expected = expect_file!["bitwise/bitwise.rs"]; + expected.assert_eq(&generated_air); +} diff --git a/examples/pub_inputs.air b/examples/pub_inputs.air deleted file mode 100644 index 786f5854e..000000000 --- a/examples/pub_inputs.air +++ /dev/null @@ -1,24 +0,0 @@ -def PubInputsAir - -trace_columns: - main: [a, b, c, d] - -public_inputs: - program_hash: [4] - stack_inputs: [4] - stack_outputs: [20] - overflow_addrs: [4] - -boundary_constraints: - enf a.first = stack_inputs[0] - enf b.first = stack_inputs[1] - enf c.first = stack_inputs[2] - enf d.first = stack_inputs[3] - - enf a.last = stack_outputs[0] - enf b.last = stack_outputs[1] - enf c.last = stack_outputs[2] - enf d.last = stack_outputs[3] - -transition_constraints: - enf a' = b + c