From 0972c7ccb1464bae1d6f0f3ddba88be3302908b3 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 28 Mar 2024 10:03:55 +0000 Subject: [PATCH] WIP - PIL relation --- barretenberg/cpp/pil/avm/avm_alu.pil | 15 ++++++++++++--- barretenberg/cpp/pil/avm/avm_main.pil | 4 ++-- .../relations/generated/avm/avm_alu.hpp | 4 +++- .../relations/generated/avm/declare_views.hpp | 1 + .../relations/generated/avm/perm_main_alu.hpp | 6 +++++- .../vm/generated/avm_circuit_builder.hpp | 6 ++++-- .../src/barretenberg/vm/generated/avm_flavor.hpp | 13 +++++++++++-- .../barretenberg/vm/generated/avm_verifier.cpp | 2 ++ 8 files changed, 40 insertions(+), 11 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_alu.pil b/barretenberg/cpp/pil/avm/avm_alu.pil index 974b4a03871..ffacf752bd7 100644 --- a/barretenberg/cpp/pil/avm/avm_alu.pil +++ b/barretenberg/cpp/pil/avm/avm_alu.pil @@ -17,6 +17,7 @@ namespace avm_alu(256); pol commit op_div; pol commit op_not; pol commit op_eq; + pol commit op_cast; pol commit alu_sel; // Predicate to activate the copy of intermediate registers to ALU table. // Instruction tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) copied from Main table @@ -58,7 +59,7 @@ namespace avm_alu(256); pol commit cf; // Compute predicate telling whether there is a row entry in the ALU table. - alu_sel = op_add + op_sub + op_mul + op_not + op_eq; + alu_sel = op_add + op_sub + op_mul + op_not + op_eq + op_cast; // ========= Type Constraints ============================================= // TODO: Range constraints @@ -163,7 +164,6 @@ namespace avm_alu(256); #[ALU_MULTIPLICATION_FF] ff_tag * op_mul * (ia * ib - ic) = 0; - // We need 2k bits to express the product (a*b) over the integer, i.e., for type uk // we express the product as sum_k (u8 is an exception as we need 8-bit registers) @@ -264,4 +264,13 @@ namespace avm_alu(256); #[ALU_OP_EQ] op_eq * (DIFF * (ic * (1 - op_eq_diff_inv) + op_eq_diff_inv) - 1 + ic) = 0; - + // ========= CAST Operation Constraints =============================== + // We handle the input ia independently of its tag, i.e., we suppose it can take + // any value between 0 and p-1. + // We decompose the input ia in 8-bit/16-bit limbs and prove that the decomposition + // sums up to ia over the integers (i.e., no modulo p wrapping). To prove this, + // we perform a "school subtraction" (borrowing) over 128-bit limbs. + // The input I is written I = I_l + I_h * 2^128 and the field order P = P_l + P_h * 2^128. + // The school subtraction result is D = D_l + D_h * 2^128 and we prove the correctness + // through: P_l - I_l - CF * 2^128 == D_l AND P_h - I_h + CF == D_h + // where CF is a carry/borrowing bit. CF == 1 <==> P_l < I_l. diff --git a/barretenberg/cpp/pil/avm/avm_main.pil b/barretenberg/cpp/pil/avm/avm_main.pil index 000922aa323..5330594b92c 100644 --- a/barretenberg/cpp/pil/avm/avm_main.pil +++ b/barretenberg/cpp/pil/avm/avm_main.pil @@ -271,10 +271,10 @@ namespace avm_main(256); #[PERM_MAIN_ALU] alu_sel {clk, ia, ib, ic, sel_op_add, sel_op_sub, - sel_op_mul, sel_op_eq, sel_op_not, alu_in_tag} + sel_op_mul, sel_op_eq, sel_op_not, sel_op_cast, alu_in_tag} is avm_alu.alu_sel {avm_alu.clk, avm_alu.ia, avm_alu.ib, avm_alu.ic, avm_alu.op_add, avm_alu.op_sub, - avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.in_tag}; + avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.op_cast, avm_alu.in_tag}; // Based on the boolean selectors, we derive the binary op id to lookup in the table; // TODO: Check if having 4 columns (op_id + 3 boolean selectors) is more optimal that just using the op_id // but with a higher degree constraint: op_id * (op_id - 1) * (op_id - 2) diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp index ef98385518f..010381797ba 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -15,6 +15,7 @@ template struct Avm_aluRow { FF avm_alu_ic{}; FF avm_alu_in_tag{}; FF avm_alu_op_add{}; + FF avm_alu_op_cast{}; FF avm_alu_op_eq{}; FF avm_alu_op_eq_diff_inv{}; FF avm_alu_op_mul{}; @@ -102,7 +103,8 @@ template class avm_aluImpl { Avm_DECLARE_VIEWS(0); auto tmp = (avm_alu_alu_sel - - ((((avm_alu_op_add + avm_alu_op_sub) + avm_alu_op_mul) + avm_alu_op_not) + avm_alu_op_eq)); + (((((avm_alu_op_add + avm_alu_op_sub) + avm_alu_op_mul) + avm_alu_op_not) + avm_alu_op_eq) + + avm_alu_op_cast)); tmp *= scaling_factor; std::get<0>(evals) += tmp; } diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp index 7d4e2705863..1b961f153f8 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -13,6 +13,7 @@ [[maybe_unused]] auto avm_alu_ic = View(new_term.avm_alu_ic); \ [[maybe_unused]] auto avm_alu_in_tag = View(new_term.avm_alu_in_tag); \ [[maybe_unused]] auto avm_alu_op_add = View(new_term.avm_alu_op_add); \ + [[maybe_unused]] auto avm_alu_op_cast = View(new_term.avm_alu_op_cast); \ [[maybe_unused]] auto avm_alu_op_div = View(new_term.avm_alu_op_div); \ [[maybe_unused]] auto avm_alu_op_eq = View(new_term.avm_alu_op_eq); \ [[maybe_unused]] auto avm_alu_op_eq_diff_inv = View(new_term.avm_alu_op_eq_diff_inv); \ diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp index c2381690795..3cf79157474 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp @@ -12,7 +12,7 @@ namespace bb { class perm_main_alu_permutation_settings { public: // This constant defines how many columns are bundled together to form each set. - constexpr static size_t COLUMNS_PER_SET = 10; + constexpr static size_t COLUMNS_PER_SET = 11; /** * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the @@ -59,6 +59,7 @@ class perm_main_alu_permutation_settings { in.avm_main_sel_op_mul, in.avm_main_sel_op_eq, in.avm_main_sel_op_not, + in.avm_main_sel_op_cast, in.avm_main_alu_in_tag, in.avm_alu_clk, in.avm_alu_ia, @@ -69,6 +70,7 @@ class perm_main_alu_permutation_settings { in.avm_alu_op_mul, in.avm_alu_op_eq, in.avm_alu_op_not, + in.avm_alu_op_cast, in.avm_alu_in_tag); } @@ -105,6 +107,7 @@ class perm_main_alu_permutation_settings { in.avm_main_sel_op_mul, in.avm_main_sel_op_eq, in.avm_main_sel_op_not, + in.avm_main_sel_op_cast, in.avm_main_alu_in_tag, in.avm_alu_clk, in.avm_alu_ia, @@ -115,6 +118,7 @@ class perm_main_alu_permutation_settings { in.avm_alu_op_mul, in.avm_alu_op_eq, in.avm_alu_op_not, + in.avm_alu_op_cast, in.avm_alu_in_tag); } }; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp index aef3bcb97c6..fa0bdf5eec0 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp @@ -43,6 +43,7 @@ template struct AvmFullRow { FF avm_alu_ic{}; FF avm_alu_in_tag{}; FF avm_alu_op_add{}; + FF avm_alu_op_cast{}; FF avm_alu_op_div{}; FF avm_alu_op_eq{}; FF avm_alu_op_eq_diff_inv{}; @@ -205,8 +206,8 @@ class AvmCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; - static constexpr size_t num_fixed_columns = 152; - static constexpr size_t num_polys = 133; + static constexpr size_t num_fixed_columns = 162; + static constexpr size_t num_polys = 143; std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -233,6 +234,7 @@ class AvmCircuitBuilder { polys.avm_alu_ic[i] = rows[i].avm_alu_ic; polys.avm_alu_in_tag[i] = rows[i].avm_alu_in_tag; polys.avm_alu_op_add[i] = rows[i].avm_alu_op_add; + polys.avm_alu_op_cast[i] = rows[i].avm_alu_op_cast; polys.avm_alu_op_div[i] = rows[i].avm_alu_op_div; polys.avm_alu_op_eq[i] = rows[i].avm_alu_op_eq; polys.avm_alu_op_eq_diff_inv[i] = rows[i].avm_alu_op_eq_diff_inv; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp index ddcae915059..6436694d4f5 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp @@ -46,11 +46,11 @@ class AvmFlavor { using RelationSeparator = FF; static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2; - static constexpr size_t NUM_WITNESS_ENTITIES = 131; + static constexpr size_t NUM_WITNESS_ENTITIES = 141; static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES; // We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for // the unshifted and one for the shifted - static constexpr size_t NUM_ALL_ENTITIES = 152; + static constexpr size_t NUM_ALL_ENTITIES = 162; using Relations = std::tuple, Avm_vm::avm_binary, @@ -106,6 +106,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -249,6 +250,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -398,6 +400,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -562,6 +565,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -726,6 +730,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -992,6 +997,7 @@ class AvmFlavor { Base::avm_alu_ic = "AVM_ALU_IC"; Base::avm_alu_in_tag = "AVM_ALU_IN_TAG"; Base::avm_alu_op_add = "AVM_ALU_OP_ADD"; + Base::avm_alu_op_cast = "AVM_ALU_OP_CAST"; Base::avm_alu_op_div = "AVM_ALU_OP_DIV"; Base::avm_alu_op_eq = "AVM_ALU_OP_EQ"; Base::avm_alu_op_eq_diff_inv = "AVM_ALU_OP_EQ_DIFF_INV"; @@ -1151,6 +1157,7 @@ class AvmFlavor { Commitment avm_alu_ic; Commitment avm_alu_in_tag; Commitment avm_alu_op_add; + Commitment avm_alu_op_cast; Commitment avm_alu_op_div; Commitment avm_alu_op_eq; Commitment avm_alu_op_eq_diff_inv; @@ -1310,6 +1317,7 @@ class AvmFlavor { avm_alu_ic = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_in_tag = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_add = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + avm_alu_op_cast = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_div = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_eq = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_eq_diff_inv = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -1474,6 +1482,7 @@ class AvmFlavor { serialize_to_buffer(avm_alu_ic, Transcript::proof_data); serialize_to_buffer(avm_alu_in_tag, Transcript::proof_data); serialize_to_buffer(avm_alu_op_add, Transcript::proof_data); + serialize_to_buffer(avm_alu_op_cast, Transcript::proof_data); serialize_to_buffer(avm_alu_op_div, Transcript::proof_data); serialize_to_buffer(avm_alu_op_eq, Transcript::proof_data); serialize_to_buffer(avm_alu_op_eq_diff_inv, Transcript::proof_data); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp index 6d3b53cc4cd..bcebe0334c6 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp @@ -61,6 +61,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) commitments.avm_alu_ic = transcript->template receive_from_prover(commitment_labels.avm_alu_ic); commitments.avm_alu_in_tag = transcript->template receive_from_prover(commitment_labels.avm_alu_in_tag); commitments.avm_alu_op_add = transcript->template receive_from_prover(commitment_labels.avm_alu_op_add); + commitments.avm_alu_op_cast = + transcript->template receive_from_prover(commitment_labels.avm_alu_op_cast); commitments.avm_alu_op_div = transcript->template receive_from_prover(commitment_labels.avm_alu_op_div); commitments.avm_alu_op_eq = transcript->template receive_from_prover(commitment_labels.avm_alu_op_eq); commitments.avm_alu_op_eq_diff_inv =