Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(avm): full poseidon2 #9141

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
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
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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you elaborate a bit more? This sentence is not super clear.

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;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As there is no use of sel_poseidon_perm_immediate in this file, I would mention that the selector is used in poseidon2_full.pil

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can actually replace both relations by a single one:
sel_poseidon_perm = sel_poseidon_perm_mem_op + sel_poseidon_perm_immediate

Then later #[skippable_if] becomes simply:
sel_poseidon_perm = 0

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"... the mem op or immediate" ... I think you meant "... the mem op and immediate"

(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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// These are the inputs to be hashed this round, we hash chunks of 3
// 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;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// Output of the hash it is matched with the result of the last permutation round;
// 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;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did not see boolean constraints for execute_poseidon_perm nor for end_poseidon. Could this be an issue?
If you add these boolean constraints, then the mutual exclusion will follow from sel_poseidon definition.

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;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Exclusion on first execution row feels strange. Do not we start the first poseidon hash here?
Also, after the last poseidon hash, we also toggle the start_poseidon selector, which is also unexpected.

Maybe you can removed this constraint and writing a comment about the fact that input_len, start_poseidon need to be properly constrained.


// 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);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you add the multiplicative term "sel_poseidon" as part of NEXT_INPUT_IS_PREV_OUTPUT_SEL, it would be a bit more efficient and more readable in the next relations.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Feels more natural to replace "(1 - end_poseidon)" by "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/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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nitpick: convention that we keep an empty line before end of namespace

} // 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
Loading