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
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
Copy Markdown
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]
Comment thread
jeanmon marked this conversation as resolved.
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;
Comment thread
fcarreiro marked this conversation as resolved.

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