feat: remove unary trick in decomposition and constraints polishing

barretenberg/cpp/pil/vm2/bc_hashing.pil

@@ -14,12 +14,12 @@ include "poseidon2_hash.pil";
 // Finally, we copy through a lookup/permutation based on the selector these field elements
 // to here (bc_hashing.pil) and then proceed to hashing.
 
-//   pc_index | bytecode_id | packed_field | incremental_hash |   output_hash      | latch | 
+//   pc_index | bytecode_id | packed_field | incremental_hash |   output_hash      | latch |
 // -----------+-------------+--------------+------------------+--------------------+--------
 //      0     |      0      |     0xabc    |        len       | H(0xabc,len) = 0x2 |   0
 //     31     |      0      |     0x123    |        0x2       | H(0x123,0x2) = 0x3 |   0
 //     62     |      0      |     0x62d    |        0x3       | H(0x62d,0x3) = end |   1
-//     0      |      1      |     0x4ab    |        len       | H(0x4ab,len) = 0x5 |   0  
+//     0      |      1      |     0x4ab    |        len       | H(0x4ab,len) = 0x5 |   0
 //     31     |      1      |     0x21f    |        0x5       | H(0x21f,0x5) = 0x6 |   0
 //     62     |      2      |     0x12a    |        0x6       | H(0x12a,0x6) = 0x9 |   0
 //     93     |      2      |     0x982    |        0x9       | H(0x982,0x9) = end |   1
@@ -40,29 +40,39 @@ namespace bc_hashing;
 
     pol commit sel;
     sel * (1 - sel) = 0;
-    
+
     // Skippable
     #[skippable_if]
-    sel + latch = 0;
-
+    sel = 0;
+
+    // If the current row is not active, then there are no more active rows after that.
+    // Note that sel cannot be activated in the first row as sel' is defined.
+    // As a consequence, if a row is activated (sel == 1) somewhere in this sub-trace, then
+    // the activated rows start from the second row and are contiguous.
+    #[TRACE_CONTINUITY]
+    (1 - precomputed.first_row) * (1 - sel) * sel' = 0;
+
     // Triggers the lookup to the address derivation subtrace, signifies the row that contains the final bytecode hash for this id
     // The sequencer can decide where to put this latch.
     pol commit latch;
     latch * (1 - latch) = 0;
-    // Latch and first_row are NAND
-    latch * precomputed.first_row = 0;
 
-    // Given both latch and first_row are boolean and they are linked by the NAND condition, the LATCH_CONDITION is boolean
+    // latch == 1 ==> sel == 1
+    #[SEL_TOGGLED_AT_LATCH]
+    latch * (1 - sel) = 0;
+
+    // Given both latch and first_row are boolean and that latch cannot be activated at first row (sel would have
+    // to be activated which is impossible on first row.), LATCH_CONDITION is a boolean.
     pol LATCH_CONDITION = latch + precomputed.first_row;
-    
+
     // The start of a new bytecode id and new set of hashing runs. Needs to be a committed column as it is used in the lookup
     pol commit start;
     start * (1 - start) = 0;
 
     // If the current row is a latch or the first row, the next row should be a start (if it's active)
     #[START_AFTER_LATCH]
     sel' * (start' - LATCH_CONDITION) = 0;
-    
+
     // Used as part of the lookup into bytecode decomposition
     pol commit pc_index;
     // The PC increments by 31 each row as long as the row is not latched, in which case the next pc is zero
@@ -71,25 +81,25 @@ namespace bc_hashing;
 
     pol commit bytecode_id;
     #[ID_CONSISTENCY]
-    sel * (1 - LATCH_CONDITION) * (bytecode_id' - bytecode_id) = 0;
+    (1 - LATCH_CONDITION) * (bytecode_id' - bytecode_id) = 0;
 
     pol commit packed_field;
     #[GET_PACKED_FIELD]
     sel { pc_index, bytecode_id, packed_field }
-    in 
+    in
     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
     pol commit incremental_hash;
-    
+
     // 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 }
     in
     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]
@@ -98,8 +108,26 @@ namespace bc_hashing;
 
     // 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;
-
-
+    (1 - LATCH_CONDITION) * (incremental_hash' - output_hash) = 0;
 
 
+    // #########################################################################################
+    //                           Proof Sketch
+    // #########################################################################################
+    // We want to show that the output_hash at a row with latch == 1 correctly enforces that it
+    // is the result of hashing the bytes of a given bytecode identified by bytecode_id.
+    // Thanks to #[TRACE_CONTINUITY] and #[SEL_TOGGLED_AT_LATCH], we have the guarantee that
+    // the rows above the final output_hash are activated. If they are activated, then
+    // bytecode_id is maintained and pc_index decrements by 31 when we move to the top.
+    // From #[START_AFTER_LATCH], we have the guarantee that we cannot meet a row with
+    // latch == 1 before we meet start == 1 when we go up. This shows that bytecode_id,
+    // pc_index, and incremental_hash evolution did not deviate from the happy path. When
+    // we reach a row with start == 1 (we know we must reach one thanks to #[START_AFTER_LATCH]
+    // enforces it on the second row.), then #[IV_IS_LEN] implies that pc_index and incremental_hash
+    // are correctly initialized. Note also that thanks #[TRACE_CONTINUITY] and #[GET_PACKED_FIELD]
+    // we retrieved packed_field at the right pc_index from bc_decomposition sub-trace.
+    // We remark that before reaching another latch, a prover might add additional rows without
+    // latch on top of the start or even add a row with start == 1. This does not have any security
+    // impact as what matters is the guarantee to have a correct initialization at start. What is
+    // more, having a row without latch on top of the start would mean that a Poseidon2 pre-image
+    // for a small integer (bytes_remaining) must have been found.

barretenberg/cpp/pil/vm2/bc_retrieval.pil

@@ -78,5 +78,9 @@ pol commit siloed_address;
 // Note: we don't need to silo and check the class id because the deployer contract guarrantees
 // that if a contract instance exists, the class has been registered.
 
+// TODO: To ensure byetcode_id unicity inside of bc_decomposition.pil, we will have to introduce
+// a permutation of the form: sel_XXX {bytecode_id} is bc_decomposition.last_of_contract {bc_decomposition.id}
+// sel_XXX will have to be picked so that it selects a bytecode_id iff it has an entry in bc_decomposition
+
 // Dummy relation to make codegen work.
-sel = sel;
+sel = sel;

barretenberg/cpp/pil/vm2/merkle_check.pil

@@ -56,9 +56,9 @@ namespace merkle_check;
     sel = 0;
 
     // If the current row is not active, then there are no more active rows after that.
-    // (not enforced for the first row)
-    // Gives guarantee that once the trace activates, it is contiguous (sel == 1) all the
-    // way until the last ever active row. After that point, sel == 1 for all remaining rows.
+    // Note that sel cannot be activated in the first row as sel' is defined.
+    // As a consequence, if a row is activated (sel == 1) somewhere in this sub-trace, then
+    // the activated rows start from the second row and are contiguous.
     #[TRACE_CONTINUITY]
     (1 - precomputed.first_row) * (1 - sel) * sel' = 0;
 

barretenberg/cpp/pil/vm2/precomputed.pil

@@ -33,15 +33,6 @@ pol constant power_of_2;
 pol constant sel_sha256_compression;
 pol constant sha256_compression_round_constant;
 
-// Unary representation of a number, from 0 to 64.
-// Example: 0 -> 0
-//          1 -> 1
-//          2 -> 11
-//          3 -> 111
-// You get it. It can be extended up to 254 bits if needed.
-pol constant sel_unary;
-pol constant as_unary;
-
 // A mapping between a non-FF MemoryTag value and their respective byte lengths:
 // {U1: 1, U8: 1, U16: 2, ... , U128: 16}
 // The enum values of MemoryTag are present in column clk.

barretenberg/cpp/src/barretenberg/vm/avm/trace/deserialization.hpp

@@ -8,9 +8,8 @@
 
 namespace bb::avm_trace {
 
-// Possible types for an instruction's operand in its wire format. (Keep in sync with TS code.
-// See avm/serialization/instruction_serialization.ts).
-// Note that the TAG enum value is not supported in TS and is parsed as UINT8.
+// Possible types for an instruction's operand in its wire format.
+// The counterpart TS file is: avm/serialization/instruction_serialization.ts.
 // INDIRECT is parsed as UINT8 where the bits represent the operands that have indirect mem access.
 enum class OperandType : uint8_t { INDIRECT8, INDIRECT16, TAG, UINT8, UINT16, UINT32, UINT64, UINT128, FF };
 

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/bc_decomposition.test.cpp

@@ -340,5 +340,21 @@ TEST(BytecodeDecompositionConstrainingTest, NegativeWrongPacking)
                               "BC_DECOMPOSITION_REPACKING");
 }
 
+// Negative test where sel_packed == 1 and sel == 0
+TEST(BytecodeDecompositionConstrainingTest, NegativeSelPackedNotSel)
+{
+    TestTraceContainer trace;
+    trace.set(0,
+              { {
+                  { C::bc_decomposition_sel_packed, 1 },
+                  { C::bc_decomposition_sel, 1 },
+              } });
+
+    check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_TOGGLED_AT_PACKED);
+    trace.set(C::bc_decomposition_sel, 0, 0); // Mutate to wrong value
+    EXPECT_THROW_WITH_MESSAGE(check_relation<bc_decomposition>(trace, bc_decomposition::SR_SEL_TOGGLED_AT_PACKED),
+                              "SEL_TOGGLED_AT_PACKED");
+}
+
 } // namespace
 } // namespace bb::avm2::constraining

barretenberg/cpp/src/barretenberg/vm2/constraining/relations/bc_hashing.test.cpp

@@ -178,6 +178,22 @@ TEST(BytecodeHashingConstrainingTest, NegativeChainOutput)
                               "CHAIN_OUTPUT_TO_INCR");
 }
 
+// Negative test where latch == 1 and sel == 0
+TEST(BytecodeHashingConstrainingTest, NegativeLatchNotSel)
+{
+    TestTraceContainer trace;
+    trace.set(0,
+              { {
+                  { C::bc_hashing_latch, 1 },
+                  { C::bc_hashing_sel, 1 },
+              } });
+
+    check_relation<bc_hashing>(trace, bc_hashing::SR_SEL_TOGGLED_AT_LATCH);
+    trace.set(C::bc_hashing_sel, 0, 0); // Mutate to wrong value
+    EXPECT_THROW_WITH_MESSAGE(check_relation<bc_hashing>(trace, bc_hashing::SR_SEL_TOGGLED_AT_LATCH),
+                              "SEL_TOGGLED_AT_LATCH");
+}
+
 TEST(BytecodeHashingConstrainingTest, NegativeBytecodeInteraction)
 {
     TestTraceContainer trace({

barretenberg/cpp/src/barretenberg/vm2/generated/flavor_variables.hpp

@@ -44,11 +44,11 @@
 namespace bb::avm2 {
 
 struct AvmFlavorVariables {
-    static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 47;
-    static constexpr size_t NUM_WITNESS_ENTITIES = 942;
+    static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 45;
+    static constexpr size_t NUM_WITNESS_ENTITIES = 903;
     static constexpr size_t NUM_SHIFTED_ENTITIES = 135;
     static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES;
-    static constexpr size_t NUM_ALL_ENTITIES = 1124;
+    static constexpr size_t NUM_ALL_ENTITIES = 1083;
 
     // Need to be templated for recursive verifier
     template <typename FF_>
@@ -92,7 +92,6 @@ struct AvmFlavorVariables {
         lookup_address_derivation_salted_initialization_hash_poseidon2_1_relation<FF_>,
         lookup_bc_decomposition_abs_diff_is_u16_relation<FF_>,
         lookup_bc_decomposition_bytes_are_bytes_relation<FF_>,
-        lookup_bc_decomposition_bytes_to_read_as_unary_relation<FF_>,
         lookup_bc_hashing_get_packed_field_relation<FF_>,
         lookup_bc_hashing_iv_is_len_relation<FF_>,
         lookup_bc_hashing_poseidon2_hash_relation<FF_>,