Updated Transaction Snark Statement

[nholland94]

As part of making the network secure against transaction pool DDoS attacks once zkApps are introduced to the network, we are splitting up transaction application within a block into 2 distinct phases. In the first phase, we apply normal signed commands in their entirety, and we apply the fee payer portion of zkApps commands. Once we are done with that phase, we take the ledger we achieved and use that to attempt to apply all of the account updates from each of the zkApps commands, skipping the command entirely if any of the account updates fail.

At the transaction snark level, this is modeled as if we are modifying 2 ledgers in parallel: the first pass ledger and the second pass ledger. The sequencing of building these ledgers and associated witnesses correctly are done outside of the snark, but from within the snark we must treat the ledger applications as if they are happening at the same time. This brings some unique challenges to our transaction snark statements, and requires us to expand the statements to not only support parallel ledgers we apply to, but also to ensure that the sequence second phase ledgers are properly connected to the final first phase ledger achieved by a transaction within a given block.

This writeup describes what those changes are, explains why they are necessary, and reviews the new merge rules necessary to reason about these statements safely.

This is an open discussion and is up for review. Please point out any discrepancies you find so we can address them.

Reviewing the old statement

To review the current transaction snark statement format, a transaction snark statement attests to a valid transition from a source ledger to a target ledger, as transitioned by a set of proven transaction applications. We can represent a transaction snark statement with the syntax S -> T to represent that the source ledger S has been taken to the target ledger T, as attested to by the associated snark proof.

New statement

With the updated fee payment model for zkapps, transaction snark statements must now reason about 2 separate passes of ledger transitions rather than just a single ledger transition. The data flow of these ledger transitions is split up over a series of individual base snark statements, which can even span across multiple trees of the transaction parallel scan state. We can represent these 2 ledger transitions with the syntax (S1 -> T1, S2 -> T2), where the first transition takes S1 to T1, and the second transition takes S2 to T2.

A sequence of transaction snark statements attesting to 2 parallel transitions on ledgers at the same time need to eventually pair up to ensure that the sequences join together correctly. Concretely, each pair of transitions (S1 -> T1, S2 -> T2) has an inherent assumption that there exists some transition that brings T1 -> S2 so that eventually we can build a transition taking S1 -> T2, making the ledger transition across multiple proof statements finally whole. It is, however, possible that we can have 2 of these assumption at once, in the case where we have merged together 2 transaction snark statements from 2 different incomplete sequences of parallel ledger transitions. For this reason, the new transaction snark statements must track 2 assumptions regarding what ledgers will eventually connect the 2 parallel ledger transitions together: a lower assumption, and an upper assumption. We syntactically represent the entire new transaction snark statement as [X, Y] (S1 -> T1, S2 -> T2) to represent that the parallel ledger transitions hold assumptions X and Y as the ledgers which will eventually glue the 2 sets of transitions together.

This is rather confusing to think about, so I will attempt to describe this in a slightly simpler way. With the parallel ledger application scheme, for the entire sequence of transactions included in a single block, the transaction snark statement of the entire sequence would be [0, 0] (A -> C, C -> E). This statement shows that the first pass starts with ledger A and gives us ledger C, and that the second pass starts with ledger C and gives us ledger E, so the statement as a whole attests to the transition of ledger A to ledger E. There are no assumption necessary in this statement because the target of the first pass is equal to the source of the second pass. When we represent the base statements of transactions within this sequence, however, we take on an assumption. Let's take the base statement for the first transaction in the sequence as an example: [C, C] (A -> B, C -> D). This transaction statement can only attest to the ledger transitions done by this transaction to each of the parallel ledgers, but cannot attest that the ledger achieved in total by the end of the first pass is the ledger that was used to start the second pass. As such, it takes on an assumption for C, stating that C must eventually be matched as the target/source pair for each of the ledger passes.

In this case, we are only looking at statements within a single sequence of transactions, so the lower and upper assumptions are always the same. However, in the parallel scan state, we may end up merging statements together which both have assumptions from different transaction sequences, which is when we will use both the lower and upper assumptions. For instance, we we merge a statement on the left containing an assumption [X, X] into a statement on the right containing an assumption [Y, Y], then we will get a statement containing both assumptions [X, Y]. In this situation, we are looking to satisfy a pending assumption of a ledger X on the left hand side, and a pending assumption of ledger Y on the right hand side.

Merging rules

$[\emptyset,\emptyset](L_1{\to}L_2,L_2{\to}L_3) \cup [\emptyset,\emptyset](L_3{\to}L_4,L_4{\to}L_5) \triangleq [\emptyset,\emptyset](L_1{\to}L_3,L_3{\to}L_5)$
$[\emptyset,\emptyset](L_1{\to}L_2,L_2{\to}L_3) \cup [X,X](L_3{\to}L_4,L_5{\to}L_6) \triangleq [X,X](L_1{\to}L_4,L_5{\to}L_6)$
$[X,X](L_1{\to}L_2,L_3{\to}L_4) \cup [\emptyset,\emptyset](L_4{\to}L_5,L_5{\to}L_6) \triangleq [X,X](L_1{\to}L_2,L_3{\to}L_6)$
$[X,X](L_1{\to}L_2,X{\to}L_3)\cup[X,X](L_2{\to}X,L_3{\to}L_4) \triangleq [\emptyset,\emptyset](L_1{\to}X,X{\to}L_4)$
$[X,X](S_1{\to}T_1,S_2{\to}T_2)\cup[Y,Y](S_1'{\to}T_1',S_2'{\to}T_2') \triangleq [X,Y](S_1{\to}T_1',S_2{\to}T_2')$
$[X,X](L_1{\to}L_2,X{\to}L_4)\cup[X,Y](L_2{\to}L_3,L_4{\to}L_5) \triangleq [Y,Y](L_1{\to}L_3,Y{\to}L_5)$
$[X,Y](L_1{\to}L_2,L_3{\to}L_4)\cup[Y,Y](L_2{\to}Y,L_4{\to}L_5) \triangleq [X,X](L_1{\to}X,L_3{\to}L_5)$

Open question: is a merge rule needed for the case $[X,Y](..,..)\cup[Y,Z](..,..)$?

A simple example

A: [L3,L3] (L1→L2, L3→L4)
B: [L3,L3] (L2→L3, L4→L5)
C: [L7,L7] (L5→L6, L7→L8)
D: [L7,L7] (L6→L7, L8→L9)

• An assumption X can be erased if X = T1 = S2

A∪B: [0,0] (L1→L3, L3→L5)
C∪D: [0,0] (L5→L7,L7→L9)

• Assumption bounds can be extended only if X1 = X2

B∪C: [L3,L7] (L2→L6, L4→L8)
Here we assume: L3→L4,L6→L7.

• Assumption bounds can be shrunk when merging statements across block boundaries

A∪(B∪C): [L3,L3] (L1→L2, L3→L4) ∪ [L3,L7] (L2→L6, L4→L8) = [L7,L7] (L1→L6,L7→L8)
Here we assume: L6→L7.
We proved that L3→L4 because $A[S2] = L3 \land A[T2] = (B∪C)[T2]$

(B∪C)∪D: [L3,L7] (L2→L6, L4→L8) ∪ [L7,L7] (L6→L7, L8→L9) = [L3,L3] (L2→L3, L4→L9)
Here we assume: L3→L4.
We proved that L6→L7.

Implications in the blockchain state and blockchain snark

Because transaction sequences for a single block can span across more than one tree of the parallel scan state, the blockchain state must now fold over the transaction snark statements emitted from the staged ledger, and the blockchain snark must use the transaction snark statement merge rules to constrain what the next emitted statement is allowed to be. To facilitate this, we will add a new field to the blockchain state which stores the last emitted transaction snark scan statement.

Lightweight proof and pseudocode by Matthew

@mrmr1993 was kind enough to write up a lightweight proof attesting to the fact that the described method of updating the transaction snark statement is correct. The rules for merging were written independently of this proof, so please check this for discrepancies against the documented merge rules.

(*
We have a series of transactions that perform the transitions
T_1 : (l_1, l_{k+1}) -> (l_2,     l_{k+2})
T_2 : (l_2, l_{k+2}) -> (l_3,     l_{k+3})
..
T_k : (l_k, l_{k+k}) -> (l_{k+1}, l_{k+k+1})
and some further transactions in a subsequent block that perform the transitions
T_{k+1} : (l_{k+k+1}, l_{k+k+n+1}}) -> (l_{k+k+2},  l_{k+k+n+2})
T_{k+2} : (l_{k+k+2}, l_{k+k+n+2}}) -> (l_{k+k+3},  l_{k+k+n+3})
..
T_{k+n} : (l_{k+k+n}, l_{k+k+n+n}) -> (l_{k+k+n+1}, l_{k+k+n+n+1})
We can label these (first_source, second_source) -> (first_target, second_target)
We can also add 3 more 'virtual' ledger hashes: (block_first_source, block_mid, block_second_target)
* When we merge a statement with T_1, we need to have
  - block_first_source_{0}
  - block_mid_{0}
  available to make sure that we started and continued in the right place
* When we merge a statement with T_k, we need to have
  - block_mid_{0}
  - block_second_target_{0}
  available to make sure that we paused and finished in the right place
* When we merge a statement with T_{k+1}, we need to have
  - block_first_source_{1} = block_second_target{0}
  - block_mid_{1}
  available to make sure that we started and continued in the right place
* When we merge a statement with T_{k+n}, we need to have
  - block_mid_{1}
  - block_second_target_{1}
  available to make sure that we paused and finished in the right place
Where there are 2 partial blocks split across 2 sub-trees, we need to store
* block_first_source_{0}, block_mid_{0} to merge with an incoming left tree containing the beginning of the first block
* block_second_target_{1}, block_mid_{1} to merge with an incoming left tree containing the beginning of the first block
Thus, in order to merge the blocks, we need (block_first_source, block_mid, block_second_target) of both the first and last block in the merge.
(I think this works?!)
Probably also need to track the correctness of each check somewhere (so T_1 checks first, mid; T_k checks mid, last; T_{k+1} checks first, mid; T_{k+n} checks mid, last), and then merging across blocks throws away the middle one as long as all of its checks were successful.
I suppose this needs to be mediated by a block number.
===== Simplification =====
Equivalently, we can label each transaction with a pair of 'block_mid' values:
T_1 : (l_1, l_{k+1}, l_{k+1}) -> (l_2,     l_{k+2}, l_{k+1})
T_2 : (l_2, l_{k+2}, l_{k+1}) -> (l_3,     l_{k+3}, l_{k+1})
..
T_k : (l_k, l_{k+k}, l_{k+1}) -> (l_{k+1}, l_{k+k+1}, l_{k+1})
where the subsequent block contains
T_{k+1} : (l_{k+k+1}, l_{k+k+n+1}}, l_{k+k+n+1}) -> (l_{k+k+2},  l_{k+k+n+2}, l_{k+k+n+1})
T_{k+2} : (l_{k+k+2}, l_{k+k+n+2}}, l_{k+k+n+1}) -> (l_{k+k+3},  l_{k+k+n+3}, l_{k+k+n+1})
..
T_{k+n} : (l_{k+k+n}, l_{k+k+n+n}, l_{k+k+n+1}) -> (l_{k+k+n+1}, l_{k+k+n+n+1}, l_{k+k+n+1})
When we merge any set of transactions from within a single block, we will get a statement:
T_i ... T_j : (l_i, l_{k+i}, l_{k+1}) -> (l_{j+1}, l_{k+j+1}, l_{k+1})
which we can build using the normal composition rules.
We label these entries (first_source, second_source, block_source) -> (first_target, second_target, block_target).
The complication comes where we merge statements that span multiple blocks. Consider a merge of the following:
LEFT: (first_source_l, second_source_l, block_source_l) -> (first_target_l, second_target_l, block_target_l)
RIGHT: (first_source_r, second_source_r, block_source_r) -> (first_target_r, second_target_r, block_target_r)
There are two possibilities:
* block_target_l = block_source_r
  We treat this as encoding that the block containing the last transaction of LEFT is the same as the block containing the first transaction of RIGHT.
  We can again merge this using the normal rules, if we make the (deferred) assumption that the other possibility handles the 'end' checks:
  TRANSITION: (first_source_l, second_source_l, block_source_l) -> (first_target_r, second_target_r, block_target_r)
  Check that:
  - first_target_l = first_source_r
  - second_target_l = second_source_r
  - block_target_l = block_source_r
    + NB: This is one of our assumptions in choosing this possibility, so can be elided in practice.
* block_target_l != block_source r
  By our assumption above, we treat this as a merge where the last transaction of LEFT is from a different block from the first transaction of RIGHT. (Otherwise, we would be in the previous 'possibility'.)
  Using the layout above, this means that
  - the values of (first_target_l, second_target_l, block_target_l) will come from the right side of T_k
  - the vaues of (first_source_r, second_source_r, block_source_r) will come from the left side of T_{k+1}
  TRANSITION: (first_source_l, second_source_l, block_source_l) -> (first_target_r, second_target_r, block_target_r)
  Check that:
  - first_target_l = block_target_l
    + that is, T_k ended its first ledger where we expected it to for the block
  - second_target_l = first_source_r
    + that is, T_{k+1} started from the ledger after T_k finished
  - second_source_r = block_source_r
    + that is, T_{k+1} started its second ledger where we expected it to for the block
By recursively applying these rules, the only boundaries that we do not check are that
* the very first transaction in the ledger proof started its second ledger at the expected point for its block
  - we would expect this to be block_source in a well-formed statement
* the very last transaction in the ledger proof finished its first ledger at the expected point for its block
  - we would expect this to be block_target in a well-formed statement
Thus, in the blockchain snark, it is sufficient to check
* second_source = block_source
* first_target = block_target
In total then, we can construct a merge on a type
*)
type statement =
  { first_pass_tree_source : ledger
  ; first_pass_tree_target : ledger
  ; second_pass_tree_source : ledger
  ; second_pass_tree_target : ledger
  ; end_of_first_pass_and_beginning_of_second_pass_left : ledger
  ; end_of_first_pass_and_beginning_of_second_pass_right : ledger }
by computing
  fun (left : statement) (right : statement) ->
    let is_same_block_at_shared_boundary =
      Ledger.equal
        left.end_of_first_pass_and_beginning_of_second_pass_right
        right.end_of_first_pass_and_beginning_of_second_pass_left
    in
    (* Continuity of first pass, or first pass finished correctly. *)
    Ledger.assert_equal
      left.first_pass_tree_target
      (if is_same_block_at_shared_boundary then
         right.first_pass_tree_source
       else
         left.end_of_first_pass_and_beginning_of_second_pass_right) ;
    (* Continuity of second pass, or second pass started correctly. *)
    Ledger.assert_equal
      right.second_pass_tree_source
      (if is_same_block_at_shared_boundary then
         left.second_pass_tree_target
       else
         right.end_of_first_pass_and_beginning_of_second_pass_left) ;
    (* No-op, or check that the end of the second pass on the left transitioned
       into the beginning of the first pass on the right, in the case of a
       block boundary.
    *)
    Ledger.assert_equal
      left.second_pass_tree_target
      (if is_same_block_at_shared_boundary then
         left.second_pass_tree_target
       else
         right.first_pass_tree_source) ;
    { first_pass_tree_source = left.first_pass_tree_source
    ; first_pass_tree_target = right.first_pass_tree_target
    ; second_pass_tree_source = left.second_pass_tree_source
    ; second_pass_tree_target = right.second_pass_tree_target
    ; end_of_first_pass_and_beginning_of_second_pass_left =
        left.end_of_first_pass_and_beginning_of_second_pass_left
    ; end_of_first_pass_and_beginning_of_second_pass_right =
        right.end_of_first_pass_and_beginning_of_second_pass_right }

[bkase]

Can you clarify in the prose what the two parallel ledgers correspond to earlier in the doc? Is it that the first ledger reflects only the first pass with the fees and legacy transactions and the second pass does all the zkapp account updates assuming that the first ledger pass has already been completed? I was able to infer this from the rest of the presentation but it could be more clear to save the next person reading some time I think.

It is, however, possible that we can have 2 of these assumption at once, in the case where we have merged together 2 transaction snark statements from 2 different incomplete sequences of parallel ledger transitions. For this reason, the new transaction snark statements must track 2 assumptions regarding what ledgers will eventually connect the 2 parallel ledger transitions together: a lower assumption, and an upper assumption.

I don’t fully understand why this happens. Can you be more specific about the case where this happens?

Assuming that this does happen:

I didn’t follow the presentation in the prose, but in the code snippet comment, using the subscripts and naming the extra carrying information as the “block midpoint” elucidated this for me. I like this representation, I think it’s a good way to think about the problem. Everything is clear for me up to here:

* block_target_l != block_source r
  By our assumption above, we treat this as a merge where the last transaction of LEFT is from a different block from the first transaction of RIGHT. (Otherwise, we would be in the previous 'possibility'.)
  Using the layout above, this means that
  - the values of (first_target_l, second_target_l, block_target_l) will come from the right side of T_k
  - the vaues of (first_source_r, second_source_r, block_source_r) will come from the left side of T_{k+1}
  TRANSITION: (first_source_l, second_source_l, block_source_l) -> (first_target_r, second_target_r, block_target_r)
  Check that:
  - first_target_l = block_target_l
    + that is, T_k ended its first ledger where we expected it to for the block
  - second_target_l = first_source_r
    + that is, T_{k+1} started from the ledger after T_k finished
  - second_source_r = block_source_r
    + that is, T_{k+1} started its second ledger where we expected it to for the block
By recursively applying these rules, the only boundaries that we do not check are that
* the very first transaction in the ledger proof started its second ledger at the expected point for its block
  - we would expect this to be block_source in a well-formed statement
* the very last transaction in the ledger proof finished its first ledger at the expected point for its block
  - we would expect this to be block_target in a well-formed statement
Thus, in the blockchain snark, it is sufficient to check
* second_source = block_source
* first_target = block_target
In total then, we can construct a merge on a type

Why are these checks exhausted and why do these rules reduce recursively except in this extra case? I’ll also follow up with @mrmr1993 in person tomorrow and either myself or maybe he will clarify.

[psteckler]

As part of making the network secure against transaction pool DDoS attacks

Why do the two phases help?

[L-as]

I'm looking at https://github.com/MinaProtocol/MIPs/blob/main/MIPS/mip-zkapps.md and trying to understand the reasoning.
The given example seems like it's possible without zkApps too? Why is it different from submitting a non-zkApp transaction that drains the account with a higher fee?

[L-as]

Cardano doesn't take fees for failed transactions (that are honestly made (assuming no bugs)). You can always DoS the network without paying fees by sending invalid proofs/signatures/data.

[nholland94]

Sending invalid proofs or signatures only allows you to DoS individual nodes, which can mitigate the attack by banning the nodes that are sending those transactions on the gossip network. The class of DoS vulnerabilities this is addresses is where an attacker can fill a pool up with transactions that become immediately invalidated when a prior transaction is applied. In such a setup, and attacker can censor regular user transactions from the network by filling the pool up with high fee transactions that are invalidated by a single low fee transaction that is at the beginning of the sequence, meaning they do not pay any fees, and the network has not recourse to ban the node since they are acting in accordance with the network's rules.

In the future, I'd like to explore alternative approaches to make the transaction pool resilient to these attacks without this added complexity to transaction application, but designing such a pool is a non-trivial problem and will require quite a bit of R&D.

[L-as]

@nholland94 bkase explained this to me, and I disagree that it will require a lot of R&D. You can reuse the Bitcoin node's algorithm almost perfectly, because Mina's ledger is more UTXO-model like than account-model like. I already explained how you would adapt it, but I would be interested in describing the scheme to you. I don't think the status quo is good, not just from a complexity view, but from a UX view. Failed transactions should never take fees. Most Ethereum-like blockchains wildly violate this principle, but it is a good principle, and Mina's mostly deterministic design means you can uphold it.

I can just copy-paste the arguments here but it is on the #mina-protocol-support slack connect.

[tizoc]

@nholland94 One question regarding the transaction pool part, shouldn't the by-sender queue length be limited? (to a value smaller than 128)

Otherwise I would be able to send thousands of transactions and only be charged for the fee needed to pay the ones that got included in the block (which are fewer than 128), with the remaining thousands being invalidated after that block. Additionally, with thousands of transactions in the pool, if I send a replacement transaction with a low nonce (that is in the valid range) I will trigger a revalidation of thousands of transactions in the pool, right?

(edit: Already got answers from Deepthi and Matthew on slack)

[L-as]

Bump @nholland94 this is still an issue

[L-as]

I don't believe this two-pass systems solves any issues if you use a Bitcoin-like mempool.
I will likely make an MIP for it later.