Skip to content

Commit

Permalink
feat(avm): full poseidon2
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyasRidhuan committed Oct 10, 2024
1 parent 662b61e commit 787b8ae
Show file tree
Hide file tree
Showing 27 changed files with 1,359 additions and 554 deletions.
47 changes: 29 additions & 18 deletions barretenberg/cpp/pil/avm/gadgets/poseidon2.pil
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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};

Expand Down
87 changes: 87 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/poseidon2_full.pil
Original file line number Diff line number Diff line change
@@ -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 };

1 change: 1 addition & 0 deletions barretenberg/cpp/pil/avm/main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
Expand Down
Loading

0 comments on commit 787b8ae

Please sign in to comment.