Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 27 additions & 17 deletions barretenberg/cpp/pil/avm/gadgets/poseidon2.pil
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,16 @@ namespace poseidon2(256);
// Selector is boolean
sel_poseidon_perm * (1 - sel_poseidon_perm) = 0;

// If this selector is on, we will read/write the input/outpu values from/to memory
pol commit sel_poseidon_perm_mem_op;
sel_poseidon_perm_mem_op * (1 - sel_poseidon_perm_mem_op) = 0;
// This is used by the bytecode hashing trace where the inputs are not stored in memory
pol commit sel_poseidon_perm_immediate;
sel_poseidon_perm_immediate * (1 - sel_poseidon_perm_immediate) = 0;

// If inactive the mem op and immediate selectors must be 0
sel_poseidon_perm = sel_poseidon_perm_mem_op + sel_poseidon_perm_immediate;

// No relations will be checked if this identity is satisfied.
#[skippable_if]
sel_poseidon_perm = 0;
Expand All @@ -30,16 +40,16 @@ namespace poseidon2(256);
// Space Id
pol commit space_id;

// 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 @@ -55,43 +65,43 @@ namespace poseidon2(256);

// ==== READ MEM OPS =====
#[PERM_POS_MEM_READ_A]
sel_poseidon_perm {clk, space_id, mem_addr_read_a, a_0, main.zeroes}
sel_poseidon_perm_mem_op {clk, 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, space_id, mem_addr_read_b, a_1, main.zeroes}
sel_poseidon_perm_mem_op {clk, 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, space_id, mem_addr_read_c, a_2, main.zeroes}
sel_poseidon_perm_mem_op {clk, 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, space_id, mem_addr_read_d, a_3, main.zeroes}
sel_poseidon_perm_mem_op {clk, 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, space_id, mem_addr_write_a, b_0, sel_poseidon_perm}
sel_poseidon_perm_mem_op {clk, 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, space_id, mem_addr_write_b, b_1, sel_poseidon_perm}
sel_poseidon_perm_mem_op {clk, 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, space_id, mem_addr_write_c, b_2, sel_poseidon_perm}
sel_poseidon_perm_mem_op {clk, 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, space_id, mem_addr_write_d, b_3, sel_poseidon_perm}
sel_poseidon_perm_mem_op {clk, 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
89 changes: 89 additions & 0 deletions barretenberg/cpp/pil/avm/gadgets/poseidon2_full.pil
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
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 field elements
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;
end_poseidon * (1 - end_poseidon) = 0;
// 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;
execute_poseidon_perm * (1 - execute_poseidon_perm) = 0;
// 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) * execute_poseidon_perm;
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/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 @@ -290,7 +290,6 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.main_sel_op_sload.set_if_valid_index(i, rows[i].main_sel_op_sload);
polys.main_sel_op_sstore.set_if_valid_index(i, rows[i].main_sel_op_sstore);
polys.main_sel_op_static_call.set_if_valid_index(i, rows[i].main_sel_op_static_call);
polys.main_sel_op_storage_address.set_if_valid_index(i, rows[i].main_sel_op_storage_address);
polys.main_sel_op_sub.set_if_valid_index(i, rows[i].main_sel_op_sub);
polys.main_sel_op_timestamp.set_if_valid_index(i, rows[i].main_sel_op_timestamp);
polys.main_sel_op_transaction_fee.set_if_valid_index(i, rows[i].main_sel_op_transaction_fee);
Expand Down Expand Up @@ -618,6 +617,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 @@ -629,6 +652,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.poseidon2_space_id.set_if_valid_index(i, rows[i].poseidon2_space_id);
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);
Expand Down
Loading