feat: PIL relations modifications for bc decomposition

barretenberg/cpp/pil/vm2/bc_decomposition.pil

@@ -1,9 +1,14 @@
+include "precomputed.pil";
+
 // This file owns the bytecode columns, and other helper columns.
 // TODO: This does NOT support empty bytecode.
-// TODO: Fully constrain.
+// TODO: Fully constrain. In particular, the last bytecode of the trace might be truncated
+//       and not finish with last_of_contract being activated. We expect this to be constrained
+//       by bytecode hashing.
 namespace bc_decomposition;
 
 pol commit sel;
+sel * (1 - sel) = 0;
 // No relations will be checked if this identity is satisfied.
 #[skippable_if]
 sel = 0;
@@ -12,22 +17,57 @@ sel = 0;
 // This includes the "current byte" and the WINDOW_SIZE - 1 lookahead bytes.
 pol WINDOW_SIZE = 36;
 
+// Internal bytecode identifier which is defined in bc_retrieval.pil
 pol commit id;
 // pc counts from 0 to bytecode_length - 1.
 pol commit pc;
 // bytes_remaining counts from bytecode_length to 1.
 pol commit bytes_remaining;
 
-// TODO: Constrain pc is increasing until contract switch.
-// TODO: Constrain bytes_remaining is decreasing until contract switch.
-// TODO: Constrain bytes_remaining = 1 iff contract switch.
-// This column should be 1 iff the contract is switching.
+// This column should be 1 iff the contract is switching, i.e., this row is the last one
+// of a contract bytecode. This is equivalent to bytes_remaining == 1.
 pol commit last_of_contract;
 last_of_contract * (1 - last_of_contract) = 0;
 
 // This is the most important column. It contains the bytecode one byte at a time on each row.
 // If the TX uses several bytecodes, they should go one after the other in this column.
 pol commit bytes;
+
+// sel is set to 1 if and only if bytes_remaining != 0 (i.e., sel == 0 iff bytes_remaining == 0)
+// This is checked by following relation and utilising inverse of bytes_remaining: bytes_rem_inv
+pol commit bytes_rem_inv;
+
+// Remark: Depending on how bytecode hashing constraints work, we might remove this relation.
+#[BC_DEC_SEL_BYTES_REM_NON_ZERO]
+bytes_remaining * ((1 - sel) * (1 - bytes_rem_inv) + bytes_rem_inv) - sel = 0;
+
+// We prove that the trace is contiguous, i.e., as soon as sel == 0 on a given row
+// then all subsequent rows have sel == 0.
+(1 - precomputed.first_row) * (1 - sel) * sel' = 0;
+
+// last_of_contract == 1 iff bytes_remaining - 1 == 0
+// We need the helper column for the inverse of bytes_remaining - 1
+pol commit bytes_rem_min_one_inv;
+
+#[BC_DEC_LAST_CONTRACT_BYTES_REM_ONE]
+sel * ((bytes_remaining - 1) * (last_of_contract * (1 - bytes_rem_min_one_inv) + bytes_rem_min_one_inv) + last_of_contract - 1) = 0;
+
+// Initialization of pc per bytecode to zero
+#[BC_DEC_PC_ZERO_INITIALIZATION]
+(precomputed.first_row + last_of_contract) * pc' = 0;
+
+// pc evolution (increment within bytecode)
+#[BC_DEC_PC_INCREMENT]
+sel * (1 - last_of_contract) * (pc' - pc - 1) = 0;
+
+// bytes_remaining evolution (decrement within bytecode)
+#[BC_DEC_BYTES_REMAINING_DECREMENT]
+sel * (1 - last_of_contract) * (bytes_remaining' - bytes_remaining + 1) = 0;
+
+// TODO: Clarify the need for maintaining the bytecode id constant within a given contract
+#[BC_DEC_ID_CONSTANT]
+sel * (1 - last_of_contract) * (id' - id) = 0;
+
 // This constrains that the bytes are in the range 0 to 255.
 #[LOOKUP_BYTECODE_BYTES_ARE_BYTES]
 sel { bytes } in precomputed.sel_range_8 { precomputed.clk };
@@ -57,7 +97,7 @@ pol commit bytes_pc_plus_1, bytes_pc_plus_2, bytes_pc_plus_3, bytes_pc_plus_4, b
 // That only the first three bytes are valid. NB: Using this unary trick saves us from doing
 // WINDOW_SIZE+ lookups and we only do 1 lookup.
 //
-// (3) Then we will expand that uniary representation into a set of WINDOW_SIZE selectors. This is done
+// (3) Then we will expand that unary representation into a set of WINDOW_SIZE selectors. This is done
 // via the usual reconstruction technique.
 //
 // (4) Then we apply the selectors to the bytes_pc_plus_n columns.
@@ -79,37 +119,87 @@ pol commit bytes_pc_plus_1, bytes_pc_plus_2, bytes_pc_plus_3, bytes_pc_plus_4, b
 pol commit bytes_to_read;
 pol commit sel_overflow_correction_needed;
 sel_overflow_correction_needed * (1 - sel_overflow_correction_needed) = 0;
-// We need to constrain bytes_to_read = min(WINDOW_SIZE, bytes_remaining). First we do...
-#[BYTECODE_OVERFLOW_CORRECTION_VALUE]
+// We need to constrain bytes_to_read = min(WINDOW_SIZE, bytes_remaining) which is equal to
+// bytes_remaining if bytes_remaining <= WINDOW_SIZE and WINDOW_SIZE otherwise.
+
+// Absolute value of WINDOW_SIZE - bytes_remaining
+pol commit abs_diff;
+// Remark: The factor sel in relation below is only required to use the skippable mechanism.
+// sel_overflow_correction_needed = 1 if bytes_remaining < WINDOW_SIZE and
+// sel_overflow_correction_needed = 0 if bytes_remaining > WINDOW_SIZE
+#[BC_DEC_ABS_DIFF]
+sel * (2 * sel_overflow_correction_needed * (WINDOW_SIZE - bytes_remaining) - WINDOW_SIZE + bytes_remaining - abs_diff) = 0;
+
+// We prove that the abs_diff is positive (and therefore sel_overflow_correction_needed correct) over the integers
+// using a range check over 16 bits. We know that WINDOWS_SIZE fits into 16 bits and bytes_remaining cannot be larger
+// than the trace size 2^21 (and bytecode hashing/validation could not pass). This provides guarantee that
+// abs_diff cannot be the result of an underflow. This would be only possible for bytes_remaining being very close
+// to the field order.
+#[LOOKUP_BYTECODE_REMAINING_ABS_DIFF_U16]
+sel { abs_diff } in precomputed.sel_range_16 { precomputed.clk };
+
+#[BC_DEC_OVERFLOW_CORRECTION_VALUE]
 sel * ((1 - sel_overflow_correction_needed) * (bytes_to_read - WINDOW_SIZE) + sel_overflow_correction_needed * (bytes_to_read - bytes_remaining)) = 0;
-// And then we do sel_overflow_correction_needed = 1 iff bytes_remaining < WINDOW_SIZE.
-// #[LOOKUP_BYTECODE_REMAINING_U16]
-// sel_overflow_correction_needed { bytes_remaining - WINDOW_SIZE } in precomputed.sel_u16 { precomputed.clk }
 
 pol commit bytes_to_read_unary;
 #[LOOKUP_BYTECODE_TO_READ_UNARY]
 sel { bytes_to_read, bytes_to_read_unary } in precomputed.sel_unary { precomputed.clk, precomputed.as_unary };
 
 // We don't need sel_pc_plus_0 because we always read the current byte.
-pol commit sel_pc_plus_0, sel_pc_plus_1, sel_pc_plus_2, sel_pc_plus_3, sel_pc_plus_4,
-           sel_pc_plus_5, sel_pc_plus_6, sel_pc_plus_7, sel_pc_plus_8, sel_pc_plus_9,
-           sel_pc_plus_10, sel_pc_plus_11, sel_pc_plus_12, sel_pc_plus_13, sel_pc_plus_14,
-           sel_pc_plus_15, 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;
-
-#[BYTECODE_UNARY_RECONSTRUCTION]
-bytes_to_read_unary = 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  +
-                             sel_pc_plus_5  * 2**5  + sel_pc_plus_6  * 2**6  + sel_pc_plus_7  * 2**7  + sel_pc_plus_8  * 2**8  + sel_pc_plus_9  * 2**9  +
-                             sel_pc_plus_10 * 2**10 + sel_pc_plus_11 * 2**11 + sel_pc_plus_12 * 2**12 + sel_pc_plus_13 * 2**13 + sel_pc_plus_14 * 2**14 +
-                             sel_pc_plus_15 * 2**15 + sel_pc_plus_16 * 2**16 + sel_pc_plus_17 * 2**17 + sel_pc_plus_18 * 2**18 + sel_pc_plus_19 * 2**19 +
-                             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);
-// Note: the above relation constrains the selectors to be binary when taken together with the lookup into unary.
+pol commit sel_pc_plus_1, sel_pc_plus_2, sel_pc_plus_3, sel_pc_plus_4, sel_pc_plus_5,
+           sel_pc_plus_6, sel_pc_plus_7, sel_pc_plus_8, sel_pc_plus_9, sel_pc_plus_10,
+           sel_pc_plus_11, sel_pc_plus_12, sel_pc_plus_13, sel_pc_plus_14, sel_pc_plus_15,
+           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;
+
+// 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;
+sel_pc_plus_2 * (1 - sel_pc_plus_2) = 0;
+sel_pc_plus_3 * (1 - sel_pc_plus_3) = 0;
+sel_pc_plus_4 * (1 - sel_pc_plus_4) = 0;
+sel_pc_plus_5 * (1 - sel_pc_plus_5) = 0;
+sel_pc_plus_6 * (1 - sel_pc_plus_6) = 0;
+sel_pc_plus_7 * (1 - sel_pc_plus_7) = 0;
+sel_pc_plus_8 * (1 - sel_pc_plus_8) = 0;
+sel_pc_plus_9 * (1 - sel_pc_plus_9) = 0;
+sel_pc_plus_10 * (1 - sel_pc_plus_10) = 0;
+sel_pc_plus_11 * (1 - sel_pc_plus_11) = 0;
+sel_pc_plus_12 * (1 - sel_pc_plus_12) = 0;
+sel_pc_plus_13 * (1 - sel_pc_plus_13) = 0;
+sel_pc_plus_14 * (1 - sel_pc_plus_14) = 0;
+sel_pc_plus_15 * (1 - sel_pc_plus_15) = 0;
+sel_pc_plus_16 * (1 - sel_pc_plus_16) = 0;
+sel_pc_plus_17 * (1 - sel_pc_plus_17) = 0;
+sel_pc_plus_18 * (1 - sel_pc_plus_18) = 0;
+sel_pc_plus_19 * (1 - sel_pc_plus_19) = 0;
+sel_pc_plus_20 * (1 - sel_pc_plus_20) = 0;
+sel_pc_plus_21 * (1 - sel_pc_plus_21) = 0;
+sel_pc_plus_22 * (1 - sel_pc_plus_22) = 0;
+sel_pc_plus_23 * (1 - sel_pc_plus_23) = 0;
+sel_pc_plus_24 * (1 - sel_pc_plus_24) = 0;
+sel_pc_plus_25 * (1 - sel_pc_plus_25) = 0;
+sel_pc_plus_26 * (1 - sel_pc_plus_26) = 0;
+sel_pc_plus_27 * (1 - sel_pc_plus_27) = 0;
+sel_pc_plus_28 * (1 - sel_pc_plus_28) = 0;
+sel_pc_plus_29 * (1 - sel_pc_plus_29) = 0;
+sel_pc_plus_30 * (1 - sel_pc_plus_30) = 0;
+sel_pc_plus_31 * (1 - sel_pc_plus_31) = 0;
+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;
+
+#[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  +
+       sel_pc_plus_5  * 2**5  + sel_pc_plus_6  * 2**6  + sel_pc_plus_7  * 2**7  + sel_pc_plus_8  * 2**8  + sel_pc_plus_9  * 2**9  +
+       sel_pc_plus_10 * 2**10 + sel_pc_plus_11 * 2**11 + sel_pc_plus_12 * 2**12 + sel_pc_plus_13 * 2**13 + sel_pc_plus_14 * 2**14 +
+       sel_pc_plus_15 * 2**15 + sel_pc_plus_16 * 2**16 + sel_pc_plus_17 * 2**17 + sel_pc_plus_18 * 2**18 + sel_pc_plus_19 * 2**19 +
+       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;
 
 // Constrain shifted columns.
 bytes_pc_plus_1 = sel_pc_plus_1 * bytes';

barretenberg/cpp/pil/vm2/bc_retrieval.pil

@@ -6,6 +6,8 @@ pol commit sel;
 #[skippable_if]
 sel = 0;
 
+// This id is generated at runtime starting from zero and incremented by 1.
+// The primary source of bytecode_id is this sub-trace.
 pol commit bytecode_id;
 pol commit err;  // some error occurred.
 pol commit address;  // contract address.

barretenberg/cpp/pil/vm2/instr_fetching.pil

@@ -37,7 +37,7 @@ pol commit fmt_3_op_u8;
 //     pc,
 //     bytecode_id,
 //     bd0, bd1, bd2, bd3, bd4,
-//     bd5, bd7, bd8, bd9, bd10,
+//     bd5, bd6, bd7, bd8, bd9, bd10,
 //     bd11, bd12, bd13, bd14, bd15,
 //     bd16, bd17, bd18, bd19, bd20,
 //     bd21, bd22, bd23, bd24, bd25,
@@ -47,7 +47,7 @@ pol commit fmt_3_op_u8;
 //     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_7, bc_decomposition.bytes_pc_plus_8, bc_decomposition.bytes_pc_plus_9, bc_decomposition.bytes_pc_plus_10,
+//     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,