feat!: constrain discarding of side-effects for tx-level operations in AVM

barretenberg/cpp/pil/vm2/execution/discard.pil

@@ -1,8 +1,12 @@
-// Discarding on error in execution
-
-// This is a virtual gadget, which is part of the execution trace.
-// This subtrace is focused on managing the changes to the discard and dying_context_id columns.
-namespace execution;
+/**
+ * Discarding on error in execution.
+ *
+ * Design Document: https://docs.google.com/document/d/1xz5sZSxTu841K8uvnT8U-nO2X5ZjY8o0TjOYKfT9b6o
+ *
+ * This subtrace is focused on managing the changes to the discard and dying_context_id columns.
+ * It is a virtual gadget, which is part of the execution trace.
+ */
+namespace execution; // virtual to execution.pil
 
     // No relations will be checked if this identity is satisfied.
     #[skippable_if]

barretenberg/cpp/pil/vm2/tx.pil

@@ -4,6 +4,7 @@ include "precomputed.pil";
 include "trees/note_hash_tree_check.pil";
 include "poseidon2_hash.pil";
 include "tx_context.pil";
+include "tx_discard.pil";
 
 // Refer to https://excalidraw.com/#json=XcT7u7Ak5rZhWqT51KwTW,VPI-Q1D7hW8_lYhf6V4bNg for a visual guide to the tx trace.
 // The tx trace manages the various phases that a transaction will undergo while it is being executed.
@@ -75,9 +76,6 @@ namespace tx;
     // If reverted == 1, is_revertible must be 1
     reverted * (1 - is_revertible) = 0;
 
-    // TODO: Constrain
-    pol commit discard;
-
     // Control flow
     pol commit read_pi_offset; // index in public inputs to read data from -> Revisit!
     pol commit read_pi_length_offset; // index in public inputs to read lengths from
@@ -228,6 +226,7 @@ namespace tx;
     // should_process_call_request {
     //     context_id,
     //     next_context_id,
+    //     discard,
     //     msg_sender,
     //     contract_addr,
     //     fee,
@@ -255,6 +254,7 @@ namespace tx;
     // execution.enqueued_call_start {
     //     execution.context_id,
     //     execution.next_context_id,
+    //     execution.discard,
     //     execution.msg_sender,
     //     execution.contract_address,
     //     execution.transaction_fee,
@@ -287,6 +287,7 @@ namespace tx;
     //    context_id,
     //    next_context_id,
     //    reverted,
+    //    discard,
     //    // Tree State
     //    next_note_hash_tree_root,
     //    next_note_hash_tree_size,
@@ -310,6 +311,7 @@ namespace tx;
     //    execution.context_id,
     //    execution.next_context_id,
     //    execution.sel_error,
+    //    execution.discard,
     //    // Tree State
     //    execution.note_hash_tree_root,
     //    execution.note_hash_tree_size,
@@ -373,7 +375,7 @@ namespace tx;
         precomputed.zero,
         sel_revertible_append_note_hash,
         prev_num_note_hashes_emitted,
-        discard,
+        discard, // from tx_discard.pil virtual trace
         next_note_hash_tree_root
     } in
     note_hash_tree_check.write {
@@ -416,7 +418,7 @@ namespace tx;
         prev_nullifier_tree_root,
         next_nullifier_tree_root,
         prev_nullifier_tree_size,
-        discard,
+        discard, // from tx_discard.pil virtual trace
         prev_num_nullifiers_emitted,
         precomputed.zero
     } in
@@ -457,6 +459,7 @@ namespace tx;
     pol commit should_l2_l1_msg_append;
     // A msg emit must be written to PI if it didn't revert, and is not discard.
     should_try_l2_l1_msg_append * ((1 - reverted) * (1 - discard) - should_l2_l1_msg_append) = 0;
+    // discard is from tx_discard.pil virtual trace
 
     should_l2_l1_msg_append * (constants.AVM_PUBLIC_INPUTS_AVM_ACCUMULATED_DATA_L2_TO_L1_MSGS_ROW_IDX + prev_num_l2_to_l1_messages - write_pi_offset) = 0;
 

barretenberg/cpp/pil/vm2/tx_discard.pil

@@ -0,0 +1,48 @@
+/**
+ * Discarding on error for tx-level operations.
+ *
+ * Design Document: https://docs.google.com/document/d/1xz5sZSxTu841K8uvnT8U-nO2X5ZjY8o0TjOYKfT9b6o
+ *
+ * This subtrace is focused on managing the changes to the discard column.
+ * It is a virtual gadget, which is part of the execution trace.
+ *
+ * 1. Propagate discard by default.
+ * 2. Discard and reverted must be 0 for all rows of startup, non-revertibles, setup, fee-payment/tree-padding/cleanup.
+ * 3. If reverted is 1, discard must be 1.
+ * 4. Lift/relax propagation only in either of the following two scenarios:
+ *    * A revert is encountered.
+ *    * End of setup is encountered.
+ */
+namespace tx; // virtual to tx.pil
+    // No relations will be checked if this identity is satisfied.
+    #[skippable_if]
+    sel = 0; // from tx.pil.
+
+    pol commit discard;
+    discard * (1 - discard) = 0;
+
+    // If discard == 1, is_revertible must be 1
+    // Can ONLY discard during revertible phases (revertible insertions, app-logic, teardown)
+    #[CAN_ONLY_DISCARD_IN_REVERTIBLE_PHASES]
+    discard * (1 - is_revertible) = 0;
+
+    // If failure == 1, discard must be 1
+    #[FAILURE_MUST_DISCARD]
+    reverted * (1 - discard) = 0;
+
+    // By default, discard's value is propagated to the next row.
+    // Lift/relax propagation of discard to the next row if:
+    // 1. A failure (reverted == 1) occurs in the current row.
+    // 2. This row is the last row of SETUP.
+    //
+    // We can know that this row is the "last row of setup" iff:
+    // a. The current row is NOT revertible: `is_revertible == 0`
+    // b. AND the next row _is_ revertible: `is_revertible' == 1`
+
+    pol LAST_ROW_OF_SETUP = (1 - is_revertible) * (is_revertible');
+    pol PROPAGATE_DISCARD = (1 - LAST_ROW_OF_SETUP) * (1 - reverted);
+
+    // If propagate_discard == 1, discard' = discard.
+    #[DISCARD_PROPAGATION]
+    sel * PROPAGATE_DISCARD * (discard' - discard) = 0;
+

barretenberg/cpp/src/barretenberg/api/api_avm.cpp

@@ -43,7 +43,7 @@ void avm_prove(const std::filesystem::path& inputs_path, const std::filesystem::
     bool res = avm.verify(proof, inputs.publicInputs, vk);
     info("verification: ", res ? "success" : "failure");
     if (!res) {
-        throw std::runtime_error("Generated proof is invalid!1!!1");
+        throw std::runtime_error("Generated proof is invalid!!!!!");
     }
 }