Merge a421532 into 2b09709

barretenberg/cpp/pil/avm/gadgets/poseidon2.pil

@@ -9,9 +9,20 @@ namespace poseidon2(256);
     // Selector is boolean
     sel_poseidon_perm * (1 - sel_poseidon_perm) = 0;
 
+    // Selector for if values are read from memory or already loaded in registers
+    pol commit sel_poseidon_perm_mem_op;
+    sel_poseidon_perm_mem_op * (1 - sel_poseidon_perm_mem_op) = 0;
+    pol commit sel_poseidon_perm_immediate;
+    sel_poseidon_perm_immediate * (1 - sel_poseidon_perm_immediate) = 0;
+
+    // If poseidon perm is active, it must be either a mem op or immediate but not both
+    sel_poseidon_perm * (1 - sel_poseidon_perm_mem_op + sel_poseidon_perm_immediate) = 0;
+    // If inactive the mem op or immediate selectors must be 0
+    (1 - sel_poseidon_perm) * (sel_poseidon_perm_mem_op + sel_poseidon_perm_immediate) = 0;
+
     // No relations will be checked if this identity is satisfied.
     #[skippable_if]
-    sel_poseidon_perm = 0;
+    sel_poseidon_perm * sel_poseidon_perm_mem_op * sel_poseidon_perm_immediate = 0;
 
     // The initial mem address for inputs or output
     pol commit input_addr;
@@ -28,16 +39,16 @@ namespace poseidon2(256);
     pol commit mem_addr_write_c;
     pol commit mem_addr_write_d;
 
-    // Accessed read / write addresses are contiguous blocks
-    sel_poseidon_perm * (mem_addr_read_a - input_addr) = 0;
-    sel_poseidon_perm * (mem_addr_read_b - (input_addr + 1)) = 0;
-    sel_poseidon_perm * (mem_addr_read_c - (input_addr + 2)) = 0;
-    sel_poseidon_perm * (mem_addr_read_d - (input_addr + 3)) = 0;
+    // Accessed read / write addresses are contiguous blocks ( would be nice if we could use sel_poseidon * sel_mem_op)
+    sel_poseidon_perm_mem_op * (mem_addr_read_a - input_addr) = 0;
+    sel_poseidon_perm_mem_op * (mem_addr_read_b - (input_addr + 1)) = 0;
+    sel_poseidon_perm_mem_op * (mem_addr_read_c - (input_addr + 2)) = 0;
+    sel_poseidon_perm_mem_op * (mem_addr_read_d - (input_addr + 3)) = 0;
 
-    sel_poseidon_perm * (mem_addr_write_a - output_addr) = 0;
-    sel_poseidon_perm * (mem_addr_write_b - (output_addr + 1)) = 0;
-    sel_poseidon_perm * (mem_addr_write_c - (output_addr + 2)) = 0;
-    sel_poseidon_perm * (mem_addr_write_d - (output_addr + 3)) = 0;
+    sel_poseidon_perm_mem_op * (mem_addr_write_a - output_addr) = 0;
+    sel_poseidon_perm_mem_op * (mem_addr_write_b - (output_addr + 1)) = 0;
+    sel_poseidon_perm_mem_op * (mem_addr_write_c - (output_addr + 2)) = 0;
+    sel_poseidon_perm_mem_op * (mem_addr_write_d - (output_addr + 3)) = 0;
 
     // The input values are represented by a_0, a_1, a_2, a_3
     pol commit a_0;
@@ -53,43 +64,43 @@ namespace poseidon2(256);
 
     // ==== READ MEM OPS =====
     #[PERM_POS_MEM_READ_A]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_read_a, a_0, main.zeroes}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_read_a, a_0, main.zeroes}
     is
     mem.sel_op_poseidon_read_a {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 
     #[PERM_POS_MEM_READ_B]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_read_b, a_1, main.zeroes}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_read_b, a_1, main.zeroes}
     is
     mem.sel_op_poseidon_read_b {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 
     #[PERM_POS_MEM_READ_C]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_read_c, a_2, main.zeroes}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_read_c, a_2, main.zeroes}
     is
     mem.sel_op_poseidon_read_c {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 
     #[PERM_POS_MEM_READ_D]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_read_d, a_3, main.zeroes}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_read_d, a_3, main.zeroes}
     is
     mem.sel_op_poseidon_read_d {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 
     //// ==== WRITE MEM OPS =====
     #[PERM_POS_MEM_WRITE_A]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_write_a, b_0, sel_poseidon_perm}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_write_a, b_0, sel_poseidon_perm}
     is
     mem.sel_op_poseidon_write_a {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 
     #[PERM_POS_MEM_WRITE_B]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_write_b, b_1, sel_poseidon_perm}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_write_b, b_1, sel_poseidon_perm}
     is
     mem.sel_op_poseidon_write_b {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 
     #[PERM_POS_MEM_WRITE_C]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_write_c, b_2, sel_poseidon_perm}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_write_c, b_2, sel_poseidon_perm}
     is
     mem.sel_op_poseidon_write_c {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 
     #[PERM_POS_MEM_WRITE_D]
-    sel_poseidon_perm {clk, main.space_id, mem_addr_write_d, b_3, sel_poseidon_perm}
+    sel_poseidon_perm_mem_op {clk, main.space_id, mem_addr_write_d, b_3, sel_poseidon_perm}
     is
     mem.sel_op_poseidon_write_d {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw};
 

barretenberg/cpp/pil/avm/gadgets/poseidon2_full.pil

@@ -0,0 +1,87 @@
+include "./poseidon2.pil";
+
+// Performs the poseidon2 full hash
+// It is **mostly** well-constrained
+namespace poseidon2_full(256);
+    pol commit clk;
+    // These are the inputs to be hashed this round, we hash chunks of 3
+    pol commit input_0;
+    pol commit input_1;
+    pol commit input_2;
+
+    // Output of the hash it is matched with the result of the last permutation round;
+    pol commit output;
+
+    pol commit sel_poseidon;
+    sel_poseidon * (1 - sel_poseidon) = 0;
+    sel_poseidon = execute_poseidon_perm + end_poseidon;
+    pol TWOPOW64 = 18446744073709551616;
+
+    pol commit input_len;
+    // Only used at the start of a new poseidon2 hash
+    pol IV = TWOPOW64 * input_len;
+
+    // Start of a poseidon2 computation
+    pol commit start_poseidon;
+    start_poseidon * (1 - start_poseidon) = 0;
+    // When we end a poseidon, the next row must naturally have a start_poseidon
+    sel_poseidon' * (1 - main.sel_first) * (start_poseidon' - end_poseidon) = 0;
+
+    // We track the num of rounds remaining, excluding the first round that has to be performed by the start_poseidon selector.
+    // We use the padded length to calculate the num of rounds to perform and the unpadded length is used in the IV.
+    pol commit num_perm_rounds_rem;
+    pol commit padding;
+    // Padding can either be 0, 1 or 2
+    padding * (padding - 1) * (padding - 2) = 0;
+    pol PADDED_LEN = input_len + padding;
+    start_poseidon * ((num_perm_rounds_rem + 1) * 3 - PADDED_LEN) = 0;
+
+
+    // The row with the final result of the poseidon computation
+    pol commit end_poseidon;
+    // The final result of the output of the hash should match the output from the last permutation (b_0)
+    end_poseidon * (output - b_0) = 0;
+    pol commit num_perm_rounds_rem_inv;
+    // end_poseidon == 1 when the num_perm_rounds_rem == 0
+    sel_poseidon * (num_perm_rounds_rem * (end_poseidon * (1 - num_perm_rounds_rem_inv) + num_perm_rounds_rem_inv) - 1 + end_poseidon) = 0;
+
+    // We perform the "squeeze" / perm operation until end_poseidon
+    pol commit execute_poseidon_perm;
+    // The squeeze and end_poseidon selector must be mutually exclusive
+    sel_poseidon * (1 - end_poseidon - execute_poseidon_perm) = 0;
+    // Need an additional helper that holds the inverse of the num_perm_rounds_rem;
+    // If we still have rounds to perform, the num_perm_rounds_rem is decremented
+    execute_poseidon_perm * (num_perm_rounds_rem' - num_perm_rounds_rem + 1) = 0;
+
+
+    // The input values are represented by a_0, a_1, a_2, a_3
+    // This most definitely could be simplified to a lower degree check
+    // the next perm input is constrained to be the previous perm output + the new values to be hashed.
+    // This occurs when we execute_poseidon_perm = 1 and we are not the start or the end of the poseidon perm
+    pol NEXT_INPUT_IS_PREV_OUTPUT_SEL = execute_poseidon_perm' * (1 - start_poseidon) * (1 - end_poseidon);
+    pol commit a_0;
+    start_poseidon * (a_0 - input_0) = 0;
+    sel_poseidon * NEXT_INPUT_IS_PREV_OUTPUT_SEL * (a_0' - b_0 - input_0') = 0;
+    pol commit a_1;
+    start_poseidon * (a_1 - input_1) = 0;
+    sel_poseidon * NEXT_INPUT_IS_PREV_OUTPUT_SEL * (a_1' - b_1 - input_1') = 0;
+    pol commit a_2;
+    start_poseidon * (a_2 - input_2) = 0;
+    sel_poseidon * NEXT_INPUT_IS_PREV_OUTPUT_SEL * (a_2' - b_2 - input_2') = 0;
+    pol commit a_3;
+    start_poseidon * (a_3 - IV) = 0; // IV is placed in the last slot if this is the start
+    sel_poseidon * NEXT_INPUT_IS_PREV_OUTPUT_SEL * (a_3' - b_3) = 0;
+
+    // Output value represented by b_0
+    pol commit b_0;
+    pol commit b_1;
+    pol commit b_2;
+    pol commit b_3;
+
+    #[PERM_POS2_FIXED_POS2_PERM]
+    sel_poseidon {clk, a_0, a_1, a_2, a_3, b_0, b_1, b_2, b_3}
+    is
+    poseidon2.sel_poseidon_perm_immediate
+        { poseidon2.clk, poseidon2.a_0, poseidon2.a_1, poseidon2.a_2, poseidon2.a_3,
+          poseidon2.b_0, poseidon2.b_1, poseidon2.b_2, poseidon2.b_3 };
+

barretenberg/cpp/pil/avm/main.pil

@@ -9,6 +9,7 @@ include "fixed/powers.pil";
 include "gadgets/conversion.pil";
 include "gadgets/sha256.pil";
 include "gadgets/poseidon2.pil";
+include "gadgets/poseidon2_full.pil";
 include "gadgets/keccakf1600.pil";
 include "gadgets/pedersen.pil";
 include "gadgets/mem_slice.pil";

barretenberg/cpp/src/barretenberg/crypto/poseidon2/poseidon2.cpp

@@ -44,4 +44,4 @@ typename Poseidon2<Params>::FF Poseidon2<Params>::hash_buffer(const std::vector<
 }
 
 template class Poseidon2<Poseidon2Bn254ScalarFieldParams>;
-} // namespace bb::crypto
+} // namespace bb::crypto

barretenberg/cpp/src/barretenberg/vm/avm/generated/circuit_builder.cpp

@@ -624,6 +624,30 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
                 polys.poseidon2_b_2.set_if_valid_index(i, rows[i].poseidon2_b_2);
                 polys.poseidon2_b_3.set_if_valid_index(i, rows[i].poseidon2_b_3);
                 polys.poseidon2_clk.set_if_valid_index(i, rows[i].poseidon2_clk);
+                polys.poseidon2_full_a_0.set_if_valid_index(i, rows[i].poseidon2_full_a_0);
+                polys.poseidon2_full_a_1.set_if_valid_index(i, rows[i].poseidon2_full_a_1);
+                polys.poseidon2_full_a_2.set_if_valid_index(i, rows[i].poseidon2_full_a_2);
+                polys.poseidon2_full_a_3.set_if_valid_index(i, rows[i].poseidon2_full_a_3);
+                polys.poseidon2_full_b_0.set_if_valid_index(i, rows[i].poseidon2_full_b_0);
+                polys.poseidon2_full_b_1.set_if_valid_index(i, rows[i].poseidon2_full_b_1);
+                polys.poseidon2_full_b_2.set_if_valid_index(i, rows[i].poseidon2_full_b_2);
+                polys.poseidon2_full_b_3.set_if_valid_index(i, rows[i].poseidon2_full_b_3);
+                polys.poseidon2_full_clk.set_if_valid_index(i, rows[i].poseidon2_full_clk);
+                polys.poseidon2_full_end_poseidon.set_if_valid_index(i, rows[i].poseidon2_full_end_poseidon);
+                polys.poseidon2_full_execute_poseidon_perm.set_if_valid_index(
+                    i, rows[i].poseidon2_full_execute_poseidon_perm);
+                polys.poseidon2_full_input_0.set_if_valid_index(i, rows[i].poseidon2_full_input_0);
+                polys.poseidon2_full_input_1.set_if_valid_index(i, rows[i].poseidon2_full_input_1);
+                polys.poseidon2_full_input_2.set_if_valid_index(i, rows[i].poseidon2_full_input_2);
+                polys.poseidon2_full_input_len.set_if_valid_index(i, rows[i].poseidon2_full_input_len);
+                polys.poseidon2_full_num_perm_rounds_rem.set_if_valid_index(i,
+                                                                            rows[i].poseidon2_full_num_perm_rounds_rem);
+                polys.poseidon2_full_num_perm_rounds_rem_inv.set_if_valid_index(
+                    i, rows[i].poseidon2_full_num_perm_rounds_rem_inv);
+                polys.poseidon2_full_output.set_if_valid_index(i, rows[i].poseidon2_full_output);
+                polys.poseidon2_full_padding.set_if_valid_index(i, rows[i].poseidon2_full_padding);
+                polys.poseidon2_full_sel_poseidon.set_if_valid_index(i, rows[i].poseidon2_full_sel_poseidon);
+                polys.poseidon2_full_start_poseidon.set_if_valid_index(i, rows[i].poseidon2_full_start_poseidon);
                 polys.poseidon2_input_addr.set_if_valid_index(i, rows[i].poseidon2_input_addr);
                 polys.poseidon2_mem_addr_read_a.set_if_valid_index(i, rows[i].poseidon2_mem_addr_read_a);
                 polys.poseidon2_mem_addr_read_b.set_if_valid_index(i, rows[i].poseidon2_mem_addr_read_b);
@@ -635,6 +659,10 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
                 polys.poseidon2_mem_addr_write_d.set_if_valid_index(i, rows[i].poseidon2_mem_addr_write_d);
                 polys.poseidon2_output_addr.set_if_valid_index(i, rows[i].poseidon2_output_addr);
                 polys.poseidon2_sel_poseidon_perm.set_if_valid_index(i, rows[i].poseidon2_sel_poseidon_perm);
+                polys.poseidon2_sel_poseidon_perm_immediate.set_if_valid_index(
+                    i, rows[i].poseidon2_sel_poseidon_perm_immediate);
+                polys.poseidon2_sel_poseidon_perm_mem_op.set_if_valid_index(i,
+                                                                            rows[i].poseidon2_sel_poseidon_perm_mem_op);
                 polys.range_check_alu_rng_chk.set_if_valid_index(i, rows[i].range_check_alu_rng_chk);
                 polys.range_check_clk.set_if_valid_index(i, rows[i].range_check_clk);
                 polys.range_check_cmp_hi_bits_rng_chk.set_if_valid_index(i, rows[i].range_check_cmp_hi_bits_rng_chk);