Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
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
1 change: 1 addition & 0 deletions barretenberg/cpp/pil/avm/constants_gen.pil
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ namespace constants;
pol START_EMIT_NULLIFIER_WRITE_OFFSET = 207;
pol START_EMIT_L2_TO_L1_MSG_WRITE_OFFSET = 223;
pol START_EMIT_UNENCRYPTED_LOG_WRITE_OFFSET = 225;
pol AVM_PC_SIZE_IN_BITS = 32;
pol GRUMPKIN_ONE_X = 1;
pol GRUMPKIN_ONE_Y = 17631683881184975370165255887551781615748388533673675138860;
pol GENERATOR_INDEX__NOTE_HASH_NONCE = 2;
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/pil/vm2/address_derivation.pil
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ namespace address_derivation;
in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };

#[SALTED_INITIALIZATION_HASH_POSEIDON2_1]
sel { deployer_addr, precomputed.zero, precomputed.zero, salted_init_hash}
sel { deployer_addr, precomputed.zero, precomputed.zero, salted_init_hash }
in poseidon2_hash.end { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };


Expand Down
14 changes: 7 additions & 7 deletions barretenberg/cpp/pil/vm2/bc_hashing.pil
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,9 @@ namespace bc_hashing;

pol commit packed_field;
#[GET_PACKED_FIELD]
sel {pc_index, bytecode_id, packed_field}
sel { pc_index, bytecode_id, packed_field }
in
bc_decomposition.sel_packed {bc_decomposition.pc, bc_decomposition.id, bc_decomposition.packed_field};
bc_decomposition.sel_packed { bc_decomposition.pc, bc_decomposition.id, bc_decomposition.packed_field };

// This tracks the incremental bytecode hash after the i-th input
// The first incremental hash of each new bytecode_id is the length of the bytecode
Expand All @@ -86,16 +86,16 @@ namespace bc_hashing;
// At the start of a new bytecode hash, the initial incremental hash has to be the length of the bytecode
// Note the looked up PC = 0 (enforced by the PC_INCREMENTS relation), i.e. the initial incremental hash value == bytecode length
#[IV_IS_LEN]
start {pc_index, bytecode_id, incremental_hash}
start { pc_index, bytecode_id, incremental_hash }
in
bc_decomposition.sel_packed {bc_decomposition.pc, bc_decomposition.id, bc_decomposition.bytes_remaining};
bc_decomposition.sel_packed { bc_decomposition.pc, bc_decomposition.id, bc_decomposition.bytes_remaining };

// Start Hashing, Poseidon2(packed_field, running_hash)
pol commit output_hash;
#[POSEIDON2_HASH]
sel {packed_field, incremental_hash, output_hash}
in poseidon2_hash.sel {poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.output};
sel { packed_field, incremental_hash, output_hash }
in poseidon2_hash.sel { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.output };

// The output hash has to be incremental_hash of the next row (unless it's latched)
#[CHAIN_OUTPUT_TO_INCR]
sel' * (1 - LATCH_CONDITION) * (incremental_hash' - output_hash) = 0;
Expand Down
8 changes: 4 additions & 4 deletions barretenberg/cpp/pil/vm2/bitwise.pil
Original file line number Diff line number Diff line change
Expand Up @@ -92,14 +92,14 @@ last * (acc_ic - ic_byte) = 0;
(acc_ic - ic_byte - 256 * acc_ic') * (1 - last) = 0;

#[INTEGRAL_TAG_LENGTH]
start {tag, ctr}
start { tag, ctr }
in
precomputed.sel_integral_tag {precomputed.clk, precomputed.integral_tag_length};
precomputed.sel_integral_tag { precomputed.clk, precomputed.integral_tag_length };

#[BYTE_OPERATIONS]
sel {op_id, ia_byte, ib_byte, ic_byte}
sel { op_id, ia_byte, ib_byte, ic_byte }
in
precomputed.sel_bitwise {precomputed.bitwise_op_id, precomputed.bitwise_input_a, precomputed.bitwise_input_b, precomputed.bitwise_output};
precomputed.sel_bitwise { precomputed.bitwise_op_id, precomputed.bitwise_input_a, precomputed.bitwise_input_b, precomputed.bitwise_output };

// TODOs: See two following paragraphs

Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/pil/vm2/class_id_derivation.pil
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ namespace class_id_derivation;
in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };

#[CLASS_ID_POSEIDON2_1]
sel { public_bytecode_commitment, precomputed.zero, precomputed.zero, class_id}
sel { public_bytecode_commitment, precomputed.zero, precomputed.zero, class_id }
in poseidon2_hash.end { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output };


1 change: 1 addition & 0 deletions barretenberg/cpp/pil/vm2/constants_gen.pil
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ namespace constants;
pol START_EMIT_NULLIFIER_WRITE_OFFSET = 207;
pol START_EMIT_L2_TO_L1_MSG_WRITE_OFFSET = 223;
pol START_EMIT_UNENCRYPTED_LOG_WRITE_OFFSET = 225;
pol AVM_PC_SIZE_IN_BITS = 32;
pol GRUMPKIN_ONE_X = 1;
pol GRUMPKIN_ONE_Y = 17631683881184975370165255887551781615748388533673675138860;
pol GENERATOR_INDEX__NOTE_HASH_NONCE = 2;
Expand Down
119 changes: 95 additions & 24 deletions barretenberg/cpp/pil/vm2/instr_fetching.pil
Copy link
Contributor

Choose a reason for hiding this comment

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

I skimmed through it and looks a lot better now. I'll let @IlyasRidhuan check the error cascading :)

Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
include "bc_decomposition.pil";
include "range_check.pil";

namespace instr_fetching;

Expand All @@ -11,8 +12,63 @@ sel * (1 - sel) = 0;

pol commit pc;
pol commit bytecode_id;
// TODO: How do we handle parsing errors?
// pol commit parsing_err;

// pc out-of-range error boolean
pol commit pc_out_of_range;
pc_out_of_range * (1 - pc_out_of_range) = 0;

// Instruction out-of-range error boolean (happens iff instr_size > bytes_to_read)
pol commit instr_out_of_range;
instr_out_of_range * (1 - instr_out_of_range) = 0;

// opcode is out-of-range error boolean
pol commit opcode_out_of_range; // copied from precomputed.pil

// If any error occurs, we toggle the following boolean:
pol commit parsing_err;
parsing_err = 1 - (1 - pc_out_of_range) * (1 - instr_out_of_range) * (1 - opcode_out_of_range);
// parsing_err is a boolean by definition (followed from above formula)

// Retrieved from bc_decomposition.pil
pol commit bytes_to_read;

// Retrieved from bc_decomposition.pil based on bytecode_id with pc == 0
pol commit bytecode_size;

// Absolute difference variant where we compute:
// bytes_to_read - instr_size if instr_size <= bytes_to_read
// instr_size - bytes_to_read - 1 if instr_size > bytes_to_read (instr_out_of_range == 1)
pol commit instr_abs_diff;

// From the following relation, we have: instr_abs_diff >= 0 ==> [instr_size > bytes_to_read <==> instr_out_of_range == 1]
#[INSTR_OUT_OF_RANGE_TOGGLE]
instr_abs_diff = (2 * instr_out_of_range - 1) * (instr_size - bytes_to_read) - instr_out_of_range;

#[INSTR_ABS_DIFF_POSITIVE]
sel { instr_abs_diff } in precomputed.sel_range_8 { precomputed.clk };

// We have to enforce that: pc < bytecode_size <==> pc_out_of_range == 0
// We use same trick as above by using an absolute difference value.

// pc - bytecode_size if bytecode_size <= pc
// bytecode_size - pc - 1 if bytecode_size > pc
pol commit pc_abs_diff;
#[PC_OUT_OF_RANGE_TOGGLE]
pc_abs_diff = sel * ((2 * pc_out_of_range - 1) * (pc - bytecode_size) - 1 + pc_out_of_range);

// TODO: Remove this one once we support constant in lookup tuples
// A column with the value 32 at each row.
pol commit thirty_two;

// pc_abs_diff is 32-bit long (pc is uint32_t)
// Use constant AVM_PC_SIZE_IN_BITS once we support constants in lookup tuples.
#[PC_ABS_DIFF_POSITIVE]
sel { pc_abs_diff, thirty_two } in range_check.sel { range_check.value, range_check.rng_chk_bits };

// The size of the bytecode is bytes_remaining at pc == 0.
#[BYTECODE_SIZE_FROM_BC_DEC]
sel { bytecode_id, precomputed.zero, bytecode_size } in
bc_decomposition.sel { bc_decomposition.id, bc_decomposition.pc, bc_decomposition.bytes_remaining };

// bytecode[pc] to bytecode[pc + 36]
pol commit bd0, bd1, bd2, bd3, bd4,
Expand All @@ -24,19 +80,17 @@ pol commit bd0, bd1, bd2, bd3, bd4,
bd31, bd32, bd33, bd34, bd35,
bd36;

pol commit indirect;
// Operands.
pol commit op1, op2, op3, op4, op5, op6, op7;
// Wire to execution opcodes translation.
pol commit exec_opcode;

pol commit instr_size_in_bytes;
// Source selector for lookups to bc_decomposition.pil and instruction specifications in precomputed.pil.
pol commit sel_opcode_defined;
// Toggled except when pc is out of range.
sel_opcode_defined = sel * (1 - pc_out_of_range);

// Bring in the bytes from the bytecode columns.
#[BYTES_FROM_BC_DEC]
sel {
pc,
sel_opcode_defined {
bytecode_id,
pc,
bytes_to_read,
bd0, bd1, bd2, bd3, bd4,
bd5, bd6, bd7, bd8, bd9,
bd10, bd11, bd12, bd13, bd14,
Expand All @@ -47,8 +101,9 @@ sel {
bd35, bd36
} in
bc_decomposition.sel {
bc_decomposition.pc,
bc_decomposition.id,
bc_decomposition.pc,
bc_decomposition.bytes_to_read,
bc_decomposition.bytes, bc_decomposition.bytes_pc_plus_1, bc_decomposition.bytes_pc_plus_2, bc_decomposition.bytes_pc_plus_3, bc_decomposition.bytes_pc_plus_4,
bc_decomposition.bytes_pc_plus_5, bc_decomposition.bytes_pc_plus_6, bc_decomposition.bytes_pc_plus_7, bc_decomposition.bytes_pc_plus_8, bc_decomposition.bytes_pc_plus_9,
bc_decomposition.bytes_pc_plus_10, bc_decomposition.bytes_pc_plus_11, bc_decomposition.bytes_pc_plus_12, bc_decomposition.bytes_pc_plus_13, bc_decomposition.bytes_pc_plus_14,
Expand All @@ -59,6 +114,12 @@ bc_decomposition.sel {
bc_decomposition.bytes_pc_plus_35, bc_decomposition.bytes_pc_plus_36
};

// Wire to execution opcodes translation.
pol commit exec_opcode;

// Instruction size in bytes
pol commit instr_size;

// Selectors for operands decomposition into bytes (copied from precomputed.pil)
// This table is populated by a map generated by a cpp test in op_decomposition.test.cpp.
pol commit sel_op_dc_0;
Expand All @@ -81,45 +142,55 @@ pol commit sel_op_dc_16;
pol commit sel_op_dc_17;

#[WIRE_INSTRUCTION_INFO]
sel {
sel_opcode_defined {
bd0,
opcode_out_of_range,
exec_opcode,
instr_size_in_bytes,
instr_size,
sel_op_dc_0, sel_op_dc_1, sel_op_dc_2, sel_op_dc_3,
sel_op_dc_4, sel_op_dc_5, sel_op_dc_6, sel_op_dc_7,
sel_op_dc_8, sel_op_dc_9, sel_op_dc_10, sel_op_dc_11,
sel_op_dc_12, sel_op_dc_13, sel_op_dc_14, sel_op_dc_15,
sel_op_dc_16, sel_op_dc_17
} in
precomputed.sel_range_wire_opcode {
precomputed.sel_range_8 {
precomputed.clk,
precomputed.opcode_out_of_range,
precomputed.exec_opcode,
precomputed.instr_size_in_bytes,
precomputed.instr_size,
precomputed.sel_op_dc_0, precomputed.sel_op_dc_1, precomputed.sel_op_dc_2, precomputed.sel_op_dc_3,
precomputed.sel_op_dc_4, precomputed.sel_op_dc_5, precomputed.sel_op_dc_6, precomputed.sel_op_dc_7,
precomputed.sel_op_dc_8, precomputed.sel_op_dc_9, precomputed.sel_op_dc_10, precomputed.sel_op_dc_11,
precomputed.sel_op_dc_12, precomputed.sel_op_dc_13, precomputed.sel_op_dc_14, precomputed.sel_op_dc_15,
precomputed.sel_op_dc_16, precomputed.sel_op_dc_17
};

pol commit indirect;

// Operands.
pol commit op1, op2, op3, op4, op5, op6, op7;

// We derive the operands only when no parsing error occurs. One might remove this gating but
// at a cost of some ugliness in the code (witgen would need a partially parsed instruction when
// the error instr_out_of_range is toggled).
// The following relations decomposing operands (indirect, op1, ...) into bytes were code-generated by
// a cpp test in op_decomposition.test.cpp.
// Remark: Upper-casing the alias needs to be edited manually (not code-generated)!
pol SEL_OP_DC_18 = sel_op_dc_2 + sel_op_dc_6;

#[INDIRECT_BYTES_DECOMPOSITION]
indirect = sel_op_dc_0 * (bd1 * 2**8 + bd2 * 2**0) + SEL_OP_DC_18 * (bd1 * 2**0);
indirect = (1 - parsing_err) * (sel_op_dc_0 * (bd1 * 2**8 + bd2 * 2**0) + SEL_OP_DC_18 * (bd1 * 2**0));
#[OP1_BYTES_DECOMPOSITION]
op1 = sel_op_dc_0 * (bd3 * 2**8 + bd4 * 2**0) + sel_op_dc_2 * (bd2 * 2**8 + bd3 * 2**0) + sel_op_dc_6 * (bd2 * 2**0) + sel_op_dc_15 * (bd1 * 2**24 + bd2 * 2**16 + bd3 * 2**8 + bd4 * 2**0);
op1 = (1 - parsing_err) * (sel_op_dc_0 * (bd3 * 2**8 + bd4 * 2**0) + sel_op_dc_2 * (bd2 * 2**8 + bd3 * 2**0) + sel_op_dc_6 * (bd2 * 2**0) + sel_op_dc_15 * (bd1 * 2**24 + bd2 * 2**16 + bd3 * 2**8 + bd4 * 2**0));
#[OP2_BYTES_DECOMPOSITION]
op2 = sel_op_dc_0 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_3 * (bd4 * 2**8 + bd5 * 2**0) + sel_op_dc_6 * (bd3 * 2**0) + sel_op_dc_8 * (bd4 * 2**0) + sel_op_dc_16 * (bd4 * 2**24 + bd5 * 2**16 + bd6 * 2**8 + bd7 * 2**0);
op2 = (1 - parsing_err) * (sel_op_dc_0 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_3 * (bd4 * 2**8 + bd5 * 2**0) + sel_op_dc_6 * (bd3 * 2**0) + sel_op_dc_8 * (bd4 * 2**0) + sel_op_dc_16 * (bd4 * 2**24 + bd5 * 2**16 + bd6 * 2**8 + bd7 * 2**0));
#[OP3_BYTES_DECOMPOSITION]
op3 = sel_op_dc_0 * (bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_4 * (bd6 * 2**8 + bd7 * 2**0) + sel_op_dc_9 * (bd5 * 2**248 + bd6 * 2**240 + bd7 * 2**232 + bd8 * 2**224 + bd9 * 2**216 + bd10 * 2**208 + bd11 * 2**200 + bd12 * 2**192 + bd13 * 2**184 + bd14 * 2**176 + bd15 * 2**168 + bd16 * 2**160 + bd17 * 2**152 + bd18 * 2**144 + bd19 * 2**136 + bd20 * 2**128 + bd21 * 2**120 + bd22 * 2**112 + bd23 * 2**104 + bd24 * 2**96 + bd25 * 2**88 + bd26 * 2**80 + bd27 * 2**72 + bd28 * 2**64 + bd29 * 2**56 + bd30 * 2**48 + bd31 * 2**40 + bd32 * 2**32 + bd33 * 2**24 + bd34 * 2**16 + bd35 * 2**8 + bd36 * 2**0) + sel_op_dc_10 * (bd5 * 2**120 + bd6 * 2**112 + bd7 * 2**104 + bd8 * 2**96 + bd9 * 2**88 + bd10 * 2**80 + bd11 * 2**72 + bd12 * 2**64 + bd13 * 2**56 + bd14 * 2**48 + bd15 * 2**40 + bd16 * 2**32 + bd17 * 2**24 + bd18 * 2**16 + bd19 * 2**8 + bd20 * 2**0) + sel_op_dc_11 * (bd5 * 2**56 + bd6 * 2**48 + bd7 * 2**40 + bd8 * 2**32 + bd9 * 2**24 + bd10 * 2**16 + bd11 * 2**8 + bd12 * 2**0) + sel_op_dc_12 * (bd5 * 2**24 + bd6 * 2**16 + bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_13 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_14 * (bd4 * 2**0) + sel_op_dc_17 * (bd6 * 2**0);
op3 = (1 - parsing_err) * (sel_op_dc_0 * (bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_4 * (bd6 * 2**8 + bd7 * 2**0) + sel_op_dc_9 * (bd5 * 2**248 + bd6 * 2**240 + bd7 * 2**232 + bd8 * 2**224 + bd9 * 2**216 + bd10 * 2**208 + bd11 * 2**200 + bd12 * 2**192 + bd13 * 2**184 + bd14 * 2**176 + bd15 * 2**168 + bd16 * 2**160 + bd17 * 2**152 + bd18 * 2**144 + bd19 * 2**136 + bd20 * 2**128 + bd21 * 2**120 + bd22 * 2**112 + bd23 * 2**104 + bd24 * 2**96 + bd25 * 2**88 + bd26 * 2**80 + bd27 * 2**72 + bd28 * 2**64 + bd29 * 2**56 + bd30 * 2**48 + bd31 * 2**40 + bd32 * 2**32 + bd33 * 2**24 + bd34 * 2**16 + bd35 * 2**8 + bd36 * 2**0) + sel_op_dc_10 * (bd5 * 2**120 + bd6 * 2**112 + bd7 * 2**104 + bd8 * 2**96 + bd9 * 2**88 + bd10 * 2**80 + bd11 * 2**72 + bd12 * 2**64 + bd13 * 2**56 + bd14 * 2**48 + bd15 * 2**40 + bd16 * 2**32 + bd17 * 2**24 + bd18 * 2**16 + bd19 * 2**8 + bd20 * 2**0) + sel_op_dc_11 * (bd5 * 2**56 + bd6 * 2**48 + bd7 * 2**40 + bd8 * 2**32 + bd9 * 2**24 + bd10 * 2**16 + bd11 * 2**8 + bd12 * 2**0) + sel_op_dc_12 * (bd5 * 2**24 + bd6 * 2**16 + bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_13 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_14 * (bd4 * 2**0) + sel_op_dc_17 * (bd6 * 2**0));
#[OP4_BYTES_DECOMPOSITION]
op4 = sel_op_dc_0 * (bd9 * 2**8 + bd10 * 2**0) + sel_op_dc_5 * (bd8 * 2**8 + bd9 * 2**0) + sel_op_dc_7 * (bd8 * 2**0);
op4 = (1 - parsing_err) * (sel_op_dc_0 * (bd9 * 2**8 + bd10 * 2**0) + sel_op_dc_5 * (bd8 * 2**8 + bd9 * 2**0) + sel_op_dc_7 * (bd8 * 2**0));
#[OP5_BYTES_DECOMPOSITION]
op5 = sel_op_dc_0 * (bd11 * 2**8 + bd12 * 2**0);
op5 = (1 - parsing_err) * (sel_op_dc_0 * (bd11 * 2**8 + bd12 * 2**0));
#[OP6_BYTES_DECOMPOSITION]
op6 = sel_op_dc_1 * (bd13 * 2**8 + bd14 * 2**0);
op6 = (1 - parsing_err) * (sel_op_dc_1 * (bd13 * 2**8 + bd14 * 2**0));
#[OP7_BYTES_DECOMPOSITION]
op7 = sel_op_dc_1 * (bd15 * 2**8 + bd16 * 2**0);
op7 = (1 - parsing_err) * (sel_op_dc_1 * (bd15 * 2**8 + bd16 * 2**0));
9 changes: 4 additions & 5 deletions barretenberg/cpp/pil/vm2/precomputed.pil
Original file line number Diff line number Diff line change
Expand Up @@ -75,12 +75,11 @@ pol constant sel_op_dc_16;
pol constant sel_op_dc_17;

pol constant exec_opcode;
pol constant instr_size_in_bytes;
pol constant instr_size; // Instruction size in bytes

// Toggle the rows which index (clk) is equal to a wire opcode
// Is used to lookup into the wire instruction spec table which contains the operand decomposition
// selectors as well as exec_opcode
pol constant sel_range_wire_opcode;
// Toggled at rows whose clk interpreted as a byte does not correspond to a valid wire opcode
// Toggled only up to clk = 255. (within range specified by sel_range_8)
pol constant opcode_out_of_range;

// Used for getting the number of safe limbs for a given radix.
// The selector is on for 1 < clk <= 256
Expand Down
4 changes: 2 additions & 2 deletions barretenberg/cpp/pil/vm2/range_check.pil
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
namespace range_check(256);
namespace range_check;
// Range check selector
pol commit sel;
sel * (1 - sel) = 0;
Expand Down Expand Up @@ -143,7 +143,7 @@ namespace range_check(256);

// This lookup does 2 things (1) Indirectly range checks dyn_rng_chk_bits to not have underflowed and (2) Simplified calculation of 2^dyn_rng_chk_bits
#[DYN_RNG_CHK_POW_2]
sel {dyn_rng_chk_bits, dyn_rng_chk_pow_2} in precomputed.sel_range_8 {precomputed.clk, precomputed.power_of_2};
sel { dyn_rng_chk_bits, dyn_rng_chk_pow_2 } in precomputed.sel_range_8 { precomputed.clk, precomputed.power_of_2 };
// NOTE: `sel_range_8` is chosen because it gives us rows [0, 256] which will give us all of the powers we need (plus many we don't need)

// Now we need to perform the dynamic range check itself
Expand Down
Loading
Loading