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.

Sign up for GitHub

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): constrain sha256 #11048

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

feat(avm): constrain sha256 #11048

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
375 changes: 368 additions & 7 deletions barretenberg/cpp/pil/avm/gadgets/sha256.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,373 @@
include "sha256_params.pil";
namespace sha256(256);

// Memory ops
pol commit state_offset;
pol commit input_offset;
pol commit output_offset;

// Initial state values loaded from state_offset;
pol commit init_a;
pol commit init_b;
pol commit init_c;
pol commit init_d;
pol commit init_e;
pol commit init_f;
pol commit init_g;
pol commit init_h;

// Output state values to be written to memory, the need to be "limbed" since it's addition modulo 2^32
// We could re-use the init columns but we need to reverse the round orders.
// Only the output_X_rhs is written to memory
pol commit output_a_lhs;
pol commit output_a_rhs;
pol commit output_b_lhs;
pol commit output_b_rhs;
pol commit output_c_lhs;
pol commit output_c_rhs;
pol commit output_d_lhs;
pol commit output_d_rhs;
pol commit output_e_lhs;
pol commit output_e_rhs;
pol commit output_f_lhs;
pol commit output_f_rhs;
pol commit output_g_lhs;
pol commit output_g_rhs;
pol commit output_h_lhs;
pol commit output_h_rhs;


// Control flow
pol commit clk;

// Selector for Radix Operation
pol commit sel_sha256_compression;
sel_sha256_compression * (1 - sel_sha256_compression) = 0;
// Selector for Sha256Compression Operation
pol commit sel;
sel * (1 - sel) = 0;
// These are needed while we can't use constant values in lookups.
// For the XOR lookups
pol commit xor_sel;
perform_round * (xor_sel - 2) = 0;
Copy link
Contributor

Choose a reason for hiding this comment

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

We should introduce constant for op_id of OR, AND, XOR and use it instead of hardcoded '2'.

// For the AND lookups
pol commit and_sel;
and_sel = 0;
Copy link
Contributor

Choose a reason for hiding this comment

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

Same as above.
Maybe add a note that, once we support constant in a tuple member of a lookup, we will not need to define this column anymore.


// Start Row
pol commit start;
start * (1 - start) = 0;
// If the current row is latched and the next row is "on", the next row is the start of the new computation
start' - (latch * sel') = 0;

// Selector to stop after 64 rounds
pol commit latch;
latch * (1 - latch) = 0;

// We perform a compression operation if we are not at a latched row
pol commit perform_round;
perform_round - (sel * (1 - latch)) = 0;
// Temp while we don't have the lookups enabled
pol commit dummy_zero;
dummy_zero = 0;
pol LAST = sel * latch;

// Counter
pol NUM_ROUNDS = 64;
pol commit rounds_remaining;
start * (rounds_remaining - NUM_ROUNDS) + perform_round * (rounds_remaining - rounds_remaining' - 1) = 0;
pol commit round_count;
sel * (round_count - (NUM_ROUNDS - rounds_remaining)) = 0;
pol commit rounds_remaining_inv;
// latch == 1 when the rounds_remaining == 0
sel * (rounds_remaining * (latch * (1 - rounds_remaining_inv) + rounds_remaining_inv) - 1 + latch) = 0;

// Hash Values
pol commit a;
pol commit b;
pol commit c;
pol commit d;
pol commit e;
pol commit f;
pol commit g;
pol commit h;

// ========== COMPUTE W =============
// w is only computed on the 16th round (as 0-15 are populated from the input)
// s0 := (w[i-15] rightrotate 7) xor (w[i-15] rightrotate 18) xor (w[i-15] rightshift 3)
// s1 := (w[i-2] rightrotate 17) xor (w[i-2] rightrotate 19) xor (w[i-2] rightshift 10)
// w[i] := w[i-16] + s0 + w[i-7] + s1

// Computing the w values for each round requires the 16th, 15th, 7th and 2nd previous w values (i - 16, i - 15, i - 7 and i - 2)
// To store this in the vm, we track 16 columns that are added to by each row and we denote the following
// helper_w0 = i - 16, helper_w1 = i - 15, helper_w9 = i - 7, helper_w14 = i - 2, helper_w15 = i - 1

pol commit helper_w0, helper_w1, helper_w2, helper_w3;
pol commit helper_w4, helper_w5, helper_w6, helper_w7;
pol commit helper_w8, helper_w9, helper_w10, helper_w11;
pol commit helper_w12, helper_w13, helper_w14, helper_w15;

perform_round * (helper_w0' - helper_w1) = 0;
perform_round * (helper_w1' - helper_w2) = 0;
perform_round * (helper_w2' - helper_w3) = 0;
perform_round * (helper_w3' - helper_w4) = 0;
perform_round * (helper_w4' - helper_w5) = 0;
perform_round * (helper_w5' - helper_w6) = 0;
perform_round * (helper_w6' - helper_w7) = 0;
perform_round * (helper_w7' - helper_w8) = 0;
perform_round * (helper_w8' - helper_w9) = 0;
perform_round * (helper_w9' - helper_w10) = 0;
perform_round * (helper_w10' - helper_w11) = 0;
perform_round * (helper_w11' - helper_w12) = 0;
perform_round * (helper_w12' - helper_w13) = 0;
perform_round * (helper_w13' - helper_w14) = 0;
perform_round * (helper_w14' - helper_w15) = 0;
// The last value is given the currently computed w value
perform_round * (helper_w15' - w) = 0;

// Message Schedule Array, in the first row
pol commit w;
// These are for rounds > 15
pol COMPUTED_W = helper_w0 + w_s_0 + helper_w9 + w_s_1;
pol commit computed_w_lhs;
pol commit computed_w_rhs;
perform_round * ((computed_w_lhs * 2**32 + computed_w_rhs) - COMPUTED_W) = 0;
pol commit is_input_round;// TODO: Constrain this
perform_round * (w - (is_input_round * helper_w0 + (1 - is_input_round) * computed_w_rhs)) = 0;


// ========== Compute w_s0 ===================
// w[i-15] `rotr` 7
pol commit w_15_rotr_7;
pol commit lhs_w_7;
pol commit rhs_w_7;
perform_round * (helper_w1 - (lhs_w_7 * 2**7 + rhs_w_7)) = 0;
perform_round * (w_15_rotr_7 - (rhs_w_7 * 2**25 + lhs_w_7)) = 0;
// w[i-15] `rotr` 18
pol commit w_15_rotr_18;
pol commit lhs_w_18;
pol commit rhs_w_18;
perform_round * (helper_w1 - (lhs_w_18 * 2**18 + rhs_w_18)) = 0;
perform_round * (w_15_rotr_18 - (rhs_w_18 * 2**14 + lhs_w_18)) = 0;
// w[i-15] `rightshift` 3
pol commit w_15_rshift_3;
pol commit lhs_w_3;
pol commit rhs_w_3;
perform_round * (helper_w1 - (lhs_w_3 * 2**3 + rhs_w_3)) = 0;
perform_round * (w_15_rshift_3 - lhs_w_3) = 0;
// s0 := (w[i-15] `rotr` 7) `xor` (w[i-15] `rotr` 18) `xor` (w[i-15] `rightshift` 3)
pol commit w_15_rotr_7_xor_w_15_rotr_18;
#[LOOKUP_W_S_0_XOR_0]
dummy_zero {w_15_rotr_7, w_15_rotr_18, w_15_rotr_7_xor_w_15_rotr_18, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit w_s_0;
#[LOOKUP_W_S_0_XOR_1]
dummy_zero {w_15_rotr_7_xor_w_15_rotr_18, w_15_rshift_3, w_s_0, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

// ========== Compute w_s1 ===================
// w[i-2] `rotr` 17
pol commit w_2_rotr_17;
pol commit lhs_w_17;
pol commit rhs_w_17;
perform_round * (helper_w14 - (lhs_w_17 * 2**17 + rhs_w_17)) = 0;
perform_round * (w_2_rotr_17 - (rhs_w_17 * 2**15 + lhs_w_17)) = 0;
// w[i-2] `rotr` 19
pol commit w_2_rotr_19;
pol commit lhs_w_19;
pol commit rhs_w_19;
perform_round * (helper_w14 - (lhs_w_19 * 2**19 + rhs_w_19)) = 0;
perform_round * (w_2_rotr_19 - (rhs_w_19 * 2**13 + lhs_w_19)) = 0;
// w[i-2] `rightshift` 10
pol commit w_2_rshift_10;
pol commit lhs_w_10;
pol commit rhs_w_10;
perform_round * (helper_w14 - (lhs_w_10 * 2**10 + rhs_w_10)) = 0;
perform_round * (w_2_rshift_10 - lhs_w_10) = 0;
// s1 := (w[i-2] `rotr` 17) `xor` (w[i-2] `rotr` 19) `xor` (w[i-2] `rightshift` 10)
pol commit w_2_rotr_17_xor_w_2_rotr_19;
#[LOOKUP_W_S_1_XOR_0]
dummy_zero {w_2_rotr_17, w_2_rotr_19, w_2_rotr_17_xor_w_2_rotr_19, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit w_s_1;
#[LOOKUP_W_S_1_XOR_1]
dummy_zero {w_2_rotr_17_xor_w_2_rotr_19, w_2_rshift_10, w_s_1, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

// ========== START OF COMPRESSION BLOCK ==================

// ====== Computing S1 ====================
// e `rotr` 6
pol commit e_rotr_6;
pol commit lhs_e_6;
pol commit rhs_e_6;
perform_round * (e - (lhs_e_6 * 2**6 + rhs_e_6)) = 0;
perform_round * (e_rotr_6 - (rhs_e_6 * 2**26 + lhs_e_6)) = 0;
// e `rotr` 11
pol commit e_rotr_11;
pol commit lhs_e_11;
pol commit rhs_e_11;
perform_round * (e - (lhs_e_11 * 2**11 + rhs_e_11)) = 0;
perform_round * (e_rotr_11 - (rhs_e_11 * 2**21 + lhs_e_11)) = 0;
// e `rotr` 25
pol commit e_rotr_25;
pol commit lhs_e_25;
pol commit rhs_e_25;
perform_round * (e - (lhs_e_25 * 2**25 + rhs_e_25)) = 0;
perform_round * (e_rotr_25 - (rhs_e_25 * 2**7 + lhs_e_25)) = 0;

// pol S_1 = (E_0 `rotr` 6) `xor` (E_0 `rotr` 11) `xor` (E_0 `rotr` 25);

pol commit e_rotr_6_xor_e_rotr_11;
#[LOOKUP_S_1_XOR_0]
dummy_zero {e_rotr_6, e_rotr_11, e_rotr_6_xor_e_rotr_11, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit s_1;
#[LOOKUP_S_1_XOR_1]
dummy_zero {e_rotr_6_xor_e_rotr_11, e_rotr_25, s_1, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

// ==== COMPUTING CH ===========
// pol CH_0 = (E_0 `and` F_0) `xor` ((`not` E_0) `and` G_0);
pol commit e_and_f;

#[LOOKUP_CH_AND_0]
dummy_zero {e, f, e_and_f, and_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit not_e;
perform_round * (e + not_e - (2**32 - 1)) = 0;

pol commit not_e_and_g;
#[LOOKUP_CH_AND_1]
dummy_zero {not_e, g, not_e_and_g, and_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit ch;
#[LOOKUP_CH_XOR]
dummy_zero {e_and_f, not_e_and_g, ch, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

// ===== COMPUTING TMP 1 ===========
// Lookup round constants
pol commit round_constant;
#[LOOKUP_ROUND_CONSTANT]
dummy_zero {round_count, round_constant}
in
binary.start {sha256_params_lookup.table_round_index, sha256_params_lookup.table_round_constant};

pol TMP_1 = h + s_1 + ch + round_constant + w;

// ===== S0 ==================
// pol S_0_0 = (A_0 `rotr` 2) `xor` (A_0 `rotr` 13) `xor` (A_0 `rotr` 22);
// a `rotr` 2
pol commit a_rotr_2;
pol commit lhs_a_2;
pol commit rhs_a_2;
perform_round * (a - (lhs_a_2 * 2**2 + rhs_a_2)) = 0;
perform_round * (a_rotr_2 - (rhs_a_2 * 2**30 + lhs_a_2)) = 0;
// a `rotr` 13
pol commit a_rotr_13;
pol commit lhs_a_13;
pol commit rhs_a_13;
perform_round * (a - (lhs_a_13 * 2**13 + rhs_a_13)) = 0;
perform_round * (a_rotr_13 - (rhs_a_13 * 2**19 + lhs_a_13)) = 0;
// a `rotr` 22
pol commit a_rotr_22;
pol commit lhs_a_22;
pol commit rhs_a_22;
perform_round * (a - (lhs_a_22 * 2**22 + rhs_a_22)) = 0;
perform_round * (a_rotr_22 - (rhs_a_22 * 2**10 + lhs_a_22)) = 0;
// (A_0 `rotr` 2) `xor` (A_0 `rotr` 13)
pol commit a_rotr_2_xor_a_rotr_13;
#[LOOKUP_S_0_XOR_0]
dummy_zero {a_rotr_2, a_rotr_13, a_rotr_2_xor_a_rotr_13, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit s_0;
#[LOOKUP_S_0_XOR_1]
dummy_zero {a_rotr_2_xor_a_rotr_13, a_rotr_22, s_0, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

// ====== Computing Maj =========
// pol MAJ_0 = (A_0 `and` B_0) `xor` (A_0 `and` C_0) `xor` (B_0 `and` C_0);
pol commit a_and_b;
#[LOOKUP_MAJ_AND_0]
dummy_zero {a, b, a_and_b, and_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit a_and_c;
#[LOOKUP_MAJ_AND_1]
dummy_zero {a, c, a_and_c, and_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit b_and_c;
#[LOOKUP_MAJ_AND_2]
dummy_zero {b, c, b_and_c, and_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit a_and_b_xor_a_and_c;
#[LOOKUP_MAJ_XOR_0]
dummy_zero {a_and_b, a_and_c, a_and_b_xor_a_and_c, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

pol commit maj;
#[LOOKUP_MAJ_XOR_1]
dummy_zero {a_and_b_xor_a_and_c, b_and_c, maj, xor_sel}
in
binary.start {binary.acc_ia, binary.acc_ib, binary.acc_ic, binary.op_id};

// ==== Compute TMP 2 ====
pol NEXT_A = s_0 + maj + TMP_1;

pol commit next_a_lhs;
pol commit next_a_rhs;
perform_round * ((next_a_lhs * 2**32 + next_a_rhs) - NEXT_A) = 0;

pol NEXT_E = d + TMP_1;

pol commit next_e_lhs;
pol commit next_e_rhs;
perform_round * ((next_e_lhs * 2**32 + next_e_rhs) - NEXT_E) = 0;

perform_round * (a' - next_a_rhs) = 0;
perform_round * (b' - a) = 0;
perform_round * (c' - b) = 0;
perform_round * (d' - c) = 0;
perform_round * (e' - next_e_rhs) = 0;
perform_round * (f' - e) = 0;
perform_round * (g' - f) = 0;
perform_round * (h' - g) = 0;

// These will all be arrays, but we just store the first element for permutation to the main trace for now
pol commit state;
pol commit input;
pol commit output;
// TODO: These constraints could be better - we might have to reverse the order of the rounds
pol OUT_A = a + init_a;
LAST * (OUT_A - (output_a_lhs * 2**32 + output_a_rhs)) = 0;
pol OUT_B = b + init_b;
LAST * (OUT_B - (output_b_lhs * 2**32 + output_b_rhs)) = 0;
pol OUT_C = c + init_c;
LAST * (OUT_C - (output_c_lhs * 2**32 + output_c_rhs)) = 0;
pol OUT_D = d + init_d;
LAST * (OUT_D - (output_d_lhs * 2**32 + output_d_rhs)) = 0;
pol OUT_E = e + init_e;
LAST * (OUT_E - (output_e_lhs * 2**32 + output_e_rhs)) = 0;
pol OUT_F = f + init_f;
LAST * (OUT_F - (output_f_lhs * 2**32 + output_f_rhs)) = 0;
pol OUT_G = g + init_g;
LAST * (OUT_G - (output_g_lhs * 2**32 + output_g_rhs)) = 0;
pol OUT_H = h + init_h;
LAST * (OUT_H - (output_h_lhs * 2**32 + output_h_rhs)) = 0;
Loading
Loading