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

[dbanks12]

Link to DD.

Relevant sections from the discard DD

TX trace columns

• phase: the phase of the current row
• is_revertible: is this row in a revertible phase (revertible insertions, app logic or teardown)
• is_padded: boolean representing whether this row is an empty row as a placeholder for a skipped phase.
• failure/ reverted: this TX row fails in some way (enqueued call fails or insertion fails due to limit reached or nullifier collision.
  • Currently named reverted in the TX trace which is probably fine because there is no distinction between error and revert in TX.
• discard: this context or one of its ancestors fails. All side effects should be discarded.

TX trace constraints

1. discard is a boolean
2. During non-revertible phases (startup, non-revertible insertions, setup, and fee-payment/cleanup phases), failure and discard must remain 0. These phases cannot fail at the top level.
   1. Note: nested calls can fail in the execution trace, but top-level setup calls must not fail. The TX trace only sees top-level failures.
3. A row that fails must discard. In other words, if failure == 1, then discard == 1 must hold true.
4. By default, the value of discard is propagated to the next row.
5. The constraint that propagates discard to the next row is lifted if any one of the following conditions are met:
   1. The next row is the first row after setup (is_revertible == 0 && is_revertible’ == 1).
      1. Note that here we define the last row of setup as the last non-revertible row before a revertible row.
   2. This row is a failure (reverted == 1).
   3. Note: the propagation constraint is not lifted at the end of app logic and teardown. Instead, we rely on the constraint that the non-revertible phases after teardown cannot discard. So, if discard == 1 is propagated past teardown because it was 1 and teardown does not fail, the constraint will fail (item 2 above) that disallows discarding during non-revertible phases. Together, these constraints enforce that if discard is set for teardown, teardown must fail, in which case propagation is lifted and discard can be reset to 0 for the following non-revertible phases.
6. For an enqueued call row, its context_id is used as the key for a lookup to the execution trace to retrieve failure.
7. For filler/padding rows representing empty phases, we make the following assumptions:
   1. The normal propagation/other constraints listed above still hold
   2. A padding row cannot fail/revert.
   3. is_revertible is constrained to be correct even for padding rows (so app-logic padding should have is_revertible == 1.
   4. After a failure occurs in revertible insertions or app-logic, there will be no “padding” rows after the failure. The trace will jump straight to teardown on the row directly following the failure.

TX tracegen

For TX tracegen, we need a preprocessing phase similar to execution because in order to populate discard, we need to figure out whether a failure occurs later in the current phase (or phase grouping), or in some later phase.

The preprocessing phase should figure out:

1. r_insertion_or_app_logic_failure: (boolean) did revertible insertions or app logic fail
2. teardown_failure: (boolean) did teardown fail

Then we populate discard for each phase as follows:

1. For revertible insertions and app logic:
   1. discard = r_insertion_or_app_logic_failure || teardown_failure
2. For teardown:
   1. Note: if revertible insertions or app logic fail, we still proceed to teardown.
   2. discard = teardown_failure

# What phases fail
for r in 0..tx_events.length:
    if r.reverted:
        if r.phase == REVERTIBLES || r.phase == APP_LOGIC:
            r_insertion_or_app_logic_failure = true
        else if r.phase == TEARDOWN:
            teardown_failure = true

for r in 0..tx_events.length:
  e = tx_events[r]
  row = rows[r]

  if e.phase == NONREVERTIBLES || SETUP || FEE_PAYMENT:
    row.discard = 0
  else if e.phase == REVERTIBLES || e.phase == APP_LOGIC:
    row.discard = r_insertion_or_app_logic_failure || teardown_failure
  else if e.phase == TEARDOWN:
    row.discard = teardown_failure

[dbanks12]

• feat: enable avm proving test for public token operations #16389
• feat!: avm bugfix of erroneous tag error in tracegen on div by 0 #16388
• feat!: misc avm bugfixes - old msm opcode and missing revert opcode #16387
• feat!: constrain discarding of side-effects for tx-level operations in AVM #16258 👈 (View in Graphite)
• feat!: use bytecode hash as bytecode ID to deduplicate bytecode hashing, instruction fetching, bc decomp #15977
• fix!: some missing context stuff in the AVM Cpp #16247
• next

This stack of pull requests is managed by Graphite. Learn more about stacking.

[dbanks12]

Could live in tx.pil. I opted to throw it in a virtual file as I did with execution discard.

[dbanks12]

I opted to add phase to the context like this. There are probably other ways. Phase is (and already was) needed for execution tracegen of discard, but we were just hardcoding it to APP LOGIC before.

[sirasistant]

sad

[sirasistant]

This looks like the mix of two strategies to set discard? or am i missing something?

[sirasistant]

Also we can probably compute discard outside of the for, since discard only needs to be computed once per phase I think

[dbanks12]

hmm i think you're right on both accounts. I'll clean up.

[dbanks12]

cleaned it up to only use the first approach, and moved that to the start of the outer "buckets" loop so it only happens once per-phase.

[sirasistant]

cool will recheck

[netlify]

✅ Deploy Preview for barretenberg ready!

Name	Link
🔨 Latest commit	e59c72f
🔍 Latest deploy log	https://app.netlify.com/projects/barretenberg/deploys/689e546b17c0d5000846a4a3
😎 Deploy Preview	https://deploy-preview-16258--barretenberg.netlify.app
📱 Preview on mobile	Toggle QR Code... Use your smartphone camera to open QR code link.

---

To edit notification comments on pull requests, go to your Netlify project configuration.