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
12 changes: 8 additions & 4 deletions barretenberg/cpp/pil/vm2/bc_decomposition.pil
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ sel = 0;

// Size of the sliding window.
// This includes the "current byte" and the WINDOW_SIZE - 1 lookahead bytes.
pol WINDOW_SIZE = 36;
pol WINDOW_SIZE = 37;

// Internal bytecode identifier which is defined in bc_retrieval.pil
pol commit id;
Expand Down Expand Up @@ -79,7 +79,8 @@ pol commit bytes_pc_plus_1, bytes_pc_plus_2, bytes_pc_plus_3, bytes_pc_plus_4, b
bytes_pc_plus_16, bytes_pc_plus_17, bytes_pc_plus_18, bytes_pc_plus_19, bytes_pc_plus_20,
bytes_pc_plus_21, bytes_pc_plus_22, bytes_pc_plus_23, bytes_pc_plus_24, bytes_pc_plus_25,
bytes_pc_plus_26, bytes_pc_plus_27, bytes_pc_plus_28, bytes_pc_plus_29, bytes_pc_plus_30,
bytes_pc_plus_31, bytes_pc_plus_32, bytes_pc_plus_33, bytes_pc_plus_34, bytes_pc_plus_35;
bytes_pc_plus_31, bytes_pc_plus_32, bytes_pc_plus_33, bytes_pc_plus_34, bytes_pc_plus_35,
bytes_pc_plus_36;

// DECOMPOSITION DOES NOT GO OVER THE END OF THE BYTECODE
//
Expand Down Expand Up @@ -152,7 +153,8 @@ pol commit sel_pc_plus_1, sel_pc_plus_2, sel_pc_plus_3, sel_pc_plus_4, sel_pc_pl
sel_pc_plus_16, sel_pc_plus_17, sel_pc_plus_18, sel_pc_plus_19, sel_pc_plus_20,
sel_pc_plus_21, sel_pc_plus_22, sel_pc_plus_23, sel_pc_plus_24, sel_pc_plus_25,
sel_pc_plus_26, sel_pc_plus_27, sel_pc_plus_28, sel_pc_plus_29, sel_pc_plus_30,
sel_pc_plus_31, sel_pc_plus_32, sel_pc_plus_33, sel_pc_plus_34, sel_pc_plus_35;
sel_pc_plus_31, sel_pc_plus_32, sel_pc_plus_33, sel_pc_plus_34, sel_pc_plus_35,
sel_pc_plus_36;

// Remark: We should investigate whether a lookup with 35 precomputed columns might be more efficient.
sel_pc_plus_1 * (1 - sel_pc_plus_1) = 0;
Expand Down Expand Up @@ -190,6 +192,7 @@ sel_pc_plus_32 * (1 - sel_pc_plus_32) = 0;
sel_pc_plus_33 * (1 - sel_pc_plus_33) = 0;
sel_pc_plus_34 * (1 - sel_pc_plus_34) = 0;
sel_pc_plus_35 * (1 - sel_pc_plus_35) = 0;
sel_pc_plus_36 * (1 - sel_pc_plus_36) = 0;

#[BC_DEC_UNARY_RECONSTRUCTION]
sel * (/*sel_pc_plus_0*/ 2**0 + sel_pc_plus_1 * 2**1 + sel_pc_plus_2 * 2**2 + sel_pc_plus_3 * 2**3 + sel_pc_plus_4 * 2**4 +
Expand All @@ -199,7 +202,7 @@ sel * (/*sel_pc_plus_0*/ 2**0 + sel_pc_plus_1 * 2**1 + sel_pc_plus_2 * 2**2
sel_pc_plus_20 * 2**20 + sel_pc_plus_21 * 2**21 + sel_pc_plus_22 * 2**22 + sel_pc_plus_23 * 2**23 + sel_pc_plus_24 * 2**24 +
sel_pc_plus_25 * 2**25 + sel_pc_plus_26 * 2**26 + sel_pc_plus_27 * 2**27 + sel_pc_plus_28 * 2**28 + sel_pc_plus_29 * 2**29 +
sel_pc_plus_30 * 2**30 + sel_pc_plus_31 * 2**31 + sel_pc_plus_32 * 2**32 + sel_pc_plus_33 * 2**33 + sel_pc_plus_34 * 2**34 +
sel_pc_plus_35 * 2**35 - bytes_to_read_unary) = 0;
sel_pc_plus_35 * 2**35 + sel_pc_plus_36 * 2**36 - bytes_to_read_unary) = 0;

// Constrain shifted columns.
bytes_pc_plus_1 = sel_pc_plus_1 * bytes';
Expand Down Expand Up @@ -237,6 +240,7 @@ bytes_pc_plus_32 = sel_pc_plus_32 * bytes_pc_plus_31';
bytes_pc_plus_33 = sel_pc_plus_33 * bytes_pc_plus_32';
bytes_pc_plus_34 = sel_pc_plus_34 * bytes_pc_plus_33';
bytes_pc_plus_35 = sel_pc_plus_35 * bytes_pc_plus_34';
bytes_pc_plus_36 = sel_pc_plus_36 * bytes_pc_plus_35';

// For bytecode hashing, we need to re-pack 31 bytes at some PCs into a field.
// We will have a selector for the PCs that are packed. This only needs to happen
Expand Down
148 changes: 100 additions & 48 deletions barretenberg/cpp/pil/vm2/instr_fetching.pil
Original file line number Diff line number Diff line change
Expand Up @@ -7,71 +7,123 @@ pol commit sel;
#[skippable_if]
sel = 0;

sel * (1 - sel) = 0;

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

// bytecode[pc] to bytecode[pc + 35]
// bytecode[pc] to bytecode[pc + 36]
pol commit bd0, bd1, bd2, bd3, bd4,
bd5, bd6, bd7, bd8, bd9, bd10,
bd11, bd12, bd13, bd14, bd15,
bd16, bd17, bd18, bd19, bd20,
bd21, bd22, bd23, bd24, bd25,
bd26, bd27, bd28, bd29, bd30,
bd31, bd32, bd33, bd34, bd35;
bd31, bd32, bd33, bd34, bd35,
bd36;

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

// Helper possible formats.
// TODO: dummy for now.
pol commit fmt_3_op_u8;
pol commit exec_opcode;

// Bring in the bytes from the bytecode columns.
// #[LOOKUP_BYTES]
// sel {
// pc,
// bytecode_id,
// bd0, bd1, bd2, bd3, bd4,
// bd5, bd6, bd7, bd8, bd9, bd10,
// bd11, bd12, bd13, bd14, bd15,
// bd16, bd17, bd18, bd19, bd20,
// bd21, bd22, bd23, bd24, bd25,
// bd26, bd27, bd28, bd29, bd30,
// bd31, bd32, bd33, bd34, bd35
// } in bc_decomposition.sel {
// bc_decomposition.pc,
// bc_decomposition.id,
// bc_decomposition.bytes_pc_plus_0, 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, bc_decomposition.bytes_pc_plus_15,
// bc_decomposition.bytes_pc_plus_16, bc_decomposition.bytes_pc_plus_17, bc_decomposition.bytes_pc_plus_18, bc_decomposition.bytes_pc_plus_19, bc_decomposition.bytes_pc_plus_20,
// bc_decomposition.bytes_pc_plus_21, bc_decomposition.bytes_pc_plus_22, bc_decomposition.bytes_pc_plus_23, bc_decomposition.bytes_pc_plus_24, bc_decomposition.bytes_pc_plus_25,
// bc_decomposition.bytes_pc_plus_26, bc_decomposition.bytes_pc_plus_27, bc_decomposition.bytes_pc_plus_28, bc_decomposition.bytes_pc_plus_29, bc_decomposition.bytes_pc_plus_30,
// bc_decomposition.bytes_pc_plus_31, bc_decomposition.bytes_pc_plus_32, bc_decomposition.bytes_pc_plus_33, bc_decomposition.bytes_pc_plus_34, bc_decomposition.bytes_pc_plus_35
// }
#[BYTES_FROM_BC_DEC]
sel {
pc,
bytecode_id,
bd0, bd1, bd2, bd3, bd4,
bd5, bd6, bd7, bd8, bd9,
bd10, bd11, bd12, bd13, bd14,
bd15, bd16, bd17, bd18, bd19,
bd20, bd21, bd22, bd23, bd24,
bd25, bd26, bd27, bd28, bd29,
bd30, bd31, bd32, bd33, bd34,
bd35, bd36
} in
bc_decomposition.sel {
bc_decomposition.pc,
bc_decomposition.id,
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,
bc_decomposition.bytes_pc_plus_15, bc_decomposition.bytes_pc_plus_16, bc_decomposition.bytes_pc_plus_17, bc_decomposition.bytes_pc_plus_18, bc_decomposition.bytes_pc_plus_19,
bc_decomposition.bytes_pc_plus_20, bc_decomposition.bytes_pc_plus_21, bc_decomposition.bytes_pc_plus_22, bc_decomposition.bytes_pc_plus_23, bc_decomposition.bytes_pc_plus_24,
bc_decomposition.bytes_pc_plus_25, bc_decomposition.bytes_pc_plus_26, bc_decomposition.bytes_pc_plus_27, bc_decomposition.bytes_pc_plus_28, bc_decomposition.bytes_pc_plus_29,
bc_decomposition.bytes_pc_plus_30, bc_decomposition.bytes_pc_plus_31, bc_decomposition.bytes_pc_plus_32, bc_decomposition.bytes_pc_plus_33, bc_decomposition.bytes_pc_plus_34,
bc_decomposition.bytes_pc_plus_35, bc_decomposition.bytes_pc_plus_36
};

// 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;
pol commit sel_op_dc_1;
pol commit sel_op_dc_2;
pol commit sel_op_dc_3;
pol commit sel_op_dc_4;
pol commit sel_op_dc_5;
pol commit sel_op_dc_6;
pol commit sel_op_dc_7;
pol commit sel_op_dc_8;
pol commit sel_op_dc_9;
pol commit sel_op_dc_10;
pol commit sel_op_dc_11;
pol commit sel_op_dc_12;
pol commit sel_op_dc_13;
pol commit sel_op_dc_14;
pol commit sel_op_dc_15;
pol commit sel_op_dc_16;
pol commit sel_op_dc_17;

// Get some info from the instruction information table.
// TODO: guard selector by error flag.
// #[LOOKUP_INSTRUCTION_INFO]
// sel {
// bd0, // wire opcode!
// ex_opcode,
// fmt_3_op_u8,
// } in instr_info.sel {
// instr_info.wire_opcode,
// instr_info.ex_opcode,
// instr_info.fmt_3_op_u8
// }
#[WIRE_INSTRUCTION_INFO]
sel {
bd0,
exec_opcode,
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.clk,
precomputed.exec_opcode,
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
};

// TODO: relations that translate single bytes to operands using formats.
// indirect = ...
// op0 = fmt_3_op_u8 * (bd0 + 2^8 * bd1 ...)
// op1 = ...
// 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_1 + sel_op_dc_6;

// Dummy relation to make codegen work.
sel = sel;
indirect = sel_op_dc_0 * (bd1 * 2**8 + bd2 * 2**0) + SEL_OP_DC_18 * (bd1 * 2**0);
op1 = sel_op_dc_0 * (bd3 * 2**8 + bd4 * 2**0) + sel_op_dc_1 * (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 = sel_op_dc_0 * (bd5 * 2**8 + bd6 * 2**0) + sel_op_dc_2 * (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 = sel_op_dc_0 * (bd7 * 2**8 + bd8 * 2**0) + sel_op_dc_3 * (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 = sel_op_dc_0 * (bd9 * 2**8 + bd10 * 2**0) + sel_op_dc_4 * (bd8 * 2**8 + bd9 * 2**0) + sel_op_dc_7 * (bd8 * 2**0);
op5 = sel_op_dc_0 * (bd11 * 2**8 + bd12 * 2**0);
op6 = sel_op_dc_5 * (bd13 * 2**8 + bd14 * 2**0);
op7 = sel_op_dc_5 * (bd15 * 2**8 + bd16 * 2**0);
31 changes: 30 additions & 1 deletion barretenberg/cpp/pil/vm2/precomputed.pil
Original file line number Diff line number Diff line change
Expand Up @@ -47,4 +47,33 @@ pol constant integral_tag_length; // Columns for the byte length 1,1,2,...,16;

// Remark: A potential optimization may consist in using sel_bitwise instead of sel_integral_mem_tag.
// However, it would extend this lookup table with pairs such as (0,0), (7,0), (8,0) which is
// not without any danger.
// not without any danger.


// Selectors for operands decomposition into bytes (required by instr_fetching.pil)
// This table is populated by a map generated by a cpp test defined in op_decomposition.test.cpp.
pol constant sel_op_dc_0;
pol constant sel_op_dc_1;
pol constant sel_op_dc_2;
pol constant sel_op_dc_3;
pol constant sel_op_dc_4;
pol constant sel_op_dc_5;
pol constant sel_op_dc_6;
pol constant sel_op_dc_7;
pol constant sel_op_dc_8;
pol constant sel_op_dc_9;
pol constant sel_op_dc_10;
pol constant sel_op_dc_11;
pol constant sel_op_dc_12;
pol constant sel_op_dc_13;
pol constant sel_op_dc_14;
pol constant sel_op_dc_15;
pol constant sel_op_dc_16;
pol constant sel_op_dc_17;

pol constant exec_opcode;

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