Local Pessimistic Proofs and Cross-Chain Consistency Checks

[bpfarmer]

[DRAFT]

I'd like to propose a change to how we calculate the pessimistic proof (this was largely inspired by Carlos Matallana's idea to generate local pessimistic proofs) that is designed to achieve the following:

1. Allow each chain to compute the pessimistic proof entirely locally.
2. Make computing the pessimistic proof more efficient.
3. Effectively get asynchronous cross-chain interop checks for free, and synchronous with a small change to the bridge smart contract and zkEVM prover.

(1) is very important because it removes complexity from the agglayer. The agglayer no longer needs to compute local balance trees for all chains at each epoch. We can calculate pessimistic proofs per chain and simplify the recursive aggregation step to combine these proofs before settlement to Ethereum. Generating per-chain pessimistic proofs without relying on global state also makes individually settling / force-including chains on L1 much simpler

The proposed scheme was described in more detail here: https://hackmd.io/YZ-AeAR2QXS4e_wOYD6NBQ but the basic intuition is that right now we're proving the statement: for each chain X, the pessimistic proof guarantees that after applying every asset transfer in every LET to X, its token balances are {b_i} where b_i are (token_address, balance) pairs.

This is actually a stronger statement than we need to prove. It suffices to show that for all chains X_j the balances b_{j,i} are non-negative after applying some subset of all asset transfers with destination chain X_j.

To give an example, suppose that there's some shitchain spamming tokens and making giant LETs depositing to many chains. Right now, the pessimistic proof needs to calculate the impact on every single chain, even when these tokens won't be claimed on nearly any of these chains, because the spammer cannot pay tx fees. Instead, the pessimistic proof should only apply asset transfers to destination chains when those transfers are claimed. Since each destination chain has the claim data available, pessimistic proofs can be computed entirely locally.

Here's some pseudo-code for the local version of the pessimistic proof (forgive me, I haven't written code in like 3 years, please don't hesitate to change while implementing):

pub struct Claim {
  pub sending_chain: ChainId
  pub local_exit_root: LocalExitRoot
  pub merkle_path: LocalExitTreePath /// Inclusion proof in a LocalExitTree
  pub token_info: TokenInfo
  pub token_amount: u256
}

pub struct NullifierSet<Hasher> { /// Hasher should be AFH, though maybe keccak for prototyping
  pub chain: ChainId /// The chain that is maintaining this nullifier set
  pub claim_bit_mask: HashMap<ChainId, ClaimBitMask> /// The claim bit mask is a data structure that maps each index of an external LocalExitTree to 1 if an asset transfer has been claimed at that position, and 0 otherwise.

  pub root: NullifierSetRoot /// Really just a u256 or vec of field elements I believe
}

/// I know that we're implementing this differently w/ FullProofOutput as a generic - this is just to illustrate
pub struct PessimisticProof {
  /// Private/Non-Deterministic inputs
  pub claims: Vec<Claim>
  pub withdrawals: Vec<Withdrawal>
  pub local_balance_tree: LocalBalanceTree<Hasher>
  pub nullifier_set: NullifierSet<Hasher>

  ///Public Inputs
  pub batch: Batch
  pub local_exit_root: LocalExitRoot /// This is the local exit root for the chain generating the pessimistic proof (PP chain), generated after the latest batch
  pub local_balance_tree_root: BalanceTreeRoot /// The local balance tree root for the PP chain
  pub nullifier_set_root: NullifierSetRoot /// The nullifier set root for the PP chain
  pub claimed_local_exit_roots: Vec<LocalExitRoot> /// Vec of all LocalExitRoots included in claims
}

Going to clean this up later, but for now, the idea is that the pessimistic proof first applies all claims that are provided by the PP chain (the chain generating the proof) to the Local Balance Tree. Ie something like (I've forgotten how to write Rust):

claims.iter().map(|claim|
  /// Need to verify that:
  /// - each asset transfer is currently unclaimed in the nullifier set
  /// - that the claim's merkle path is correct and matches the claim's LocalExitRoot
  /// - that the claim's destination chain ID matches the PP Chain's Chain ID
  local_balance_tree.apply_claim(claim) /// Adds the amount of tokens in the claim to the local balance tree
  /// Then we update the nullifier set to record each claim
)

/// We verify that the calculated Nullfier Set Root is consistent with nullifier_set_root included as a public input

/// We map claims to a vector of local_exit_roots included in each claim and then verify that this vector matches the public input 
/// claimed_local_exit_roots

From here, we can infer from the batch the previous frontier of the PP chain's local exit tree, and then extract all new asset_transfers included in the PP chains local exit tree. We then deduct each asset transfer from the chain's local balance tree.

/// Need to first verify that the set of withdrawals is consistent with the updated LocalExitRoot included as a public input
withdrawals.iter().map(|withdrawal|
  local_balance_tree.apply_withdrawal(withdrawal) /// Deducts the withdrawal from the local balance tree
)
/// Alternatively we could calculate aggregate withdrawals for each token and apply them to the local balance tree
/// We verify that the calculated LocalBalanceRoot matches local_balance_root

Now we have a locally-generated pessimistic proof, but we still have to verify that claimed_local_exit_roots are valid. This can be done by the agglayer. The Agglayer can recursively aggregate all locally-generated pessimistic proofs and merge the set of claimed_local_exit_roots, before verifying that each is valid as part of the final proof step.

The nice thing is that this is the cross-chain consistency / interop proof. We allow chains to cryptographically guarantee that they cannot depend on invalid or inconsistent LERs. To guarantee this property for synchronous message passing, we can modify the bridge contract, as described here: https://hackmd.io/Cn5NqzC2TJ6dVg9AtmFOUw

[pgebheim]

Great writeup and this meets my intuitions based upon the discussions with Carlos, Jesus, and shared sequencing teams.

Question: what DA guarantees do we need for the agglayer to verify that the claimed_local_exit_roots are valid?

[krlosMata]

PP pseudo-code

• I have written a pseudo-code of the steps that the PP needs to do --> https://hackmd.io/eJUpSKhkQHudBS48BEXrow?view#Pseudo-code

• Seems pretty much aligned with yours @bpfarmer , expect for the claimed_local_exit_roots or the selectedGER.

• There is a glossary at the beginning of the doc, https://hackmd.io/eJUpSKhkQHudBS48BEXrow?view#Glossary, just if any naming is different xD

• pseudo-code:

// public inputs
const oldLER
const oldLBR
const oldNullifierRoot

const hashBridgeExits
const hashImportedBridgeExits
const selectedGER
const networkID

// public outputs
const newLER
const newLBR
const newNullifierRoot

// Section A: Verify `hashbBridgeExits`
const bridgeExits = [bridgeExit_0, bridgeExit_1, ..., bridgeExit_N-1]; // private input
assert(keccak256(bridgeExits), hashBridgeExits);

// Section B: Apply `bridgeExits` to `oldLER`
let currentLER = oldLER;
for (let i = 0; i < bridgeExits.length; i++) {
    currentLER = smt.add(currentLER, bridgeExits[i]); // returns the new root
}
assert(newLER, currentLER);

// Section C: apply bridgeExits to LBR and store balance to check at the very end
const checkBalances = []; // unique identified by originTokenAddress & originTokenNetworkID
let currentLBR = oldLBR;
for (let i = 0; i < bridgeExits.length; i++) {
    const singleBridgeExit = bridgeExits[i];
    if (singleBridgeExit.originNetworkID == networkID) {
        continue; // skip since asset it is originally from this chain
    }
    
    if (singleBridgeExit.leafType == MESSAGE_TYPE) {
        continue; // skip since it is message type, not asset type
    }
    
    // add pair originTokenAddress & originTokenNetworkID
    checkBalances.push(singleBridgeExit.originTokenAddress & singleBridgeExit.originTokenNetworkID;
    // extract value from the LBR
    currentLBR = smt.updateLeafBridgeExits(currentLBR, singleBridgeExit); // this function decrease token balance base on (originNetworkID, originAddress, amount)
}

// Section D: Verify `hashImportedBridgeExits`
const importedBridgeExits = [importedBridgeExit_0, importedBridgeExit_1, ..., importedBridgeExit_N-1]; // private input
assert(keccak256(importedBridgeExits), hashImportedBridgeExits)

// Section E: group importedBridges by its originNetworkID
const mappingIBByNetworkID = {}; // IB --> Imported Bridges
for (let i = 0; i < importedBridgeExits.lenght; i++) {
    const singleImportedBridgeExit = importedBridgeExits[i];
    if (mappingIBByNetworkID[singleImportedBridgeExit.originNetworkID] == undefined) {
        mappingIBByNetworkID[singleImportedBridgeExit.originNetworkID] = [];    
    }
    mappingIBByNetworkID[singleImportedBridgeExit.originNetworkID].push(singleImportedBridgeExit);
}

// section F: for each networkID, verify the LER that is going to be used against the selectedGER
const networkIDLERMap = { // private input
      "0": "0xAA...BB",
      "1": "0xCC...DD",
      ...
      "N-1": "0xEE...FF",
};

for (let i = 0; i < Object.keys(mappingIBByNetworkID).length; i++) {
    const networkID = Object.keys(mappingIBByNetworkID)[i];
    const singleLER = networkIDLERMap[networkID];
    const smtProof = [0x00...01, 0x00...02, ...]; // private input
    const isIncluded = verifySMTProof(selectedGER, singleLER, smtProof); // return true/false
    assert(isIncluded, true);
}

// section G: verify importedBridges exists on its corresponding LER
for (let i = 0; i < Object.keys(mappingIBByNetworkID).length; i++) {
    const networkID = Object.keys(mappingIBByNetworkID)[i];
    const LERNetworkID = networkIDLERMap[networkID];
    
    // get all importedBirdges for that networkID and verify them
    for (let j = 0; j < mappingIBByNetworkID[networkID].lenght; j++) {
         const singleImportedBridgeExit = mappingIBByNetworkID[networkID][j];
         const smtProof = [0x00...01, 0x00...02, ...]; // private input
         const isIncluded = verifySMTProof(LERNetworkID, singleImportedBridgeExit, smtProof); // return true/false
         assert(isIncluded, true)
    }
}

// section H: add importedBridges on the LBR
const currentNullifierRoot = oldNullifierRoot;
for (let i = 0; i < importedBridgeExits.length; i++) {
    const singleImportedBridgeExit = importedBridgeExits[i];
    
    if (singleImportedBridgeExit.leafType == MESSAGE_TYPE) {
        continue; // skip since it is message type, not asset type
    }
    
    if (singleImportedBridgeExit.destinationNetworkID != networkID) {
        continue; // skip since it does not affect this networkID
    }

    // verify it has not been nullified
    const isClaimed = smt.readValue(oldNullifierRoot, singleImportedBridgeExit); // uses index & networkID from the bridgeExit
    if (isClaimed == true) {
        continue; // jump to the next one, since it has been claimed
    }
    
    // add it to the LBR
    // extract value from the LBR
    currentLBR = smt.updateLeafBridgeExits(currentLBR, singleImportedBridgeExit); // this function adds token balance base on (originNetworkID, originAddress, amount)
    // update nullifierRoot
    currentNullifierRoot = smt.updateNullifierTree(currentNullifierRoot, singleImportedBridgeExit); // uses index & networkID from the bridgeExit
}

assert(newLBR, currentLBR);
assert(newNullifierRoot, currentNullifierRoot);

// section I: verify there is not negative value for all the decreasing balances in the LBR
for (let i = 0; i < checkBalances.length; i++) {
     const balance = smt.readValue(currentLBR, checkBalances[i]); // gets value from a certain originAddress # originNetworkID   
     assert (balance > 0);
}

claimed_local_exit_roots

Now we have a locally-generated pessimistic proof, but we still have to verify that claimed_local_exit_roots are valid. This can be done by the agglayer. The Agglayer can recursively aggregate all locally-generated pessimistic proofs and merge the set of claimed_local_exit_roots, before verifying that each is valid as part of the final proof step

Question: what DA guarantees do we need for the agglayer to verify that the claimed_local_exit_roots are valid?

There are several options to do that verification, each one with its trade-offs. I will try to summarize all three approaches that I can think of:

aggLayer to verify at top level proof the claimed_local_exit_roots

this is your approach

• this implies the aggLayer to make a proof of every LER present claimed_local_exit_roots (used when importing the bridges)
• The aggLayer then can settle each PP on-chain by proving at higher level two proofs: the PP & the claimed_local_exit_roots inclusion
• This implies to have a single input on-chain with all the previous GER, so you can prove all the claimed_local_exit_roots

Pros

• PP locally does not care about proving the claimed_local_exit_roots
• reuse data that has been used in your chain: LER for each claim & merkle_path

Cons

• join two proofs into a top level proof
• the chain cannot submit the PP by themselves

selectedGER

this is what is written in my pseudo-code

• selectedGER is a GER that exist on L1
• all the pub struct Claim are not checked against its own LER, but all of them are checked against the selectedGER.
  • if a claim has been done in GER_i...the GER_i+1 also has that claim
• Therefore, you know all the claims that has been done in your chain (call them importedBridgeExits)
  • you can query the bridge-service to give you the merkle_path against the selectedGER so you can prove them

Pros

• fully PP generated locally
• simplifies aggLayer at first stage
• easy to add like forcedPP on the mid-term

Cons

• depends on the bridge-service (although I can imagine the aggLayer to provide that data)

L1InfoTree

kind of an hybrid

• Turns out that we have a data structure on L1 that holds all historical GER. It is the L1InfoTree
• It is an append-only MT of fixed 32 levels (same tree as the GER) that contains:
  • key: index
  • value: GER_i (more data inside, but for simplicity, just consider the GER)
• So we can validate all the claimed_local_exit_roots inside the PP built by the chain

Pros

• reuse data that has been used in your chain: LER for each claim & merkle_path
• fully PP generated locally
• simplifies aggLayer at first stage
• data needed to verify GER - LER in the L1InfoRoot is already tracked by the bridge-service

Cons

• it may add complexity since it uses the L1InfoRoot

[bpfarmer]

Great writeup and this meets my intuitions based upon the discussions with Carlos, Jesus, and shared sequencing teams.

Question: what DA guarantees do we need for the agglayer to verify that the claimed_local_exit_roots are valid?

There's no DA guarantee required - "claimed_local_exit_root = valid" <=> the local exit root included in a previous GET or the current GET being built.

[bpfarmer]

Nice writeup @krlosMata !

There are several options to do that verification, each one with its trade-offs. I will try to summarize all three approaches that I can think of:

What I would propose is a mixture of the first and the third approaches. For the happy path, where the chain doesn't need to force-include on L1, it can submit a vector of claimed_local_exit_roots to the AL, and the AL can prove inclusion in previous GERs or the current GER.

This point (proving inclusion in the current GER) is really important, as it's what allows us to have low-latency interop (we can allow chains to claim from LETs before they're even included in a GET by the AL).

The force-include path would be allowing chains to submit another proof to L1 showing that the claimed LERs are consistent with the L1InfoRoot.

[krlosMata]

Let me write down all the necessary steps taking account your 1-3 approach:

• Step 1: chain_A to get from itself: bridgeExits and importedBridgeExits
• Step 2: Send them to aggLayer
• Step 3: aggLayer to have L1InfoRoot data (so it can prove all used claimed_local_exit_root)
• Step 4: aggLayer to build PP
• Step 5: aggLayer to send PP to L1

sequenceDiagram
    participant chain_A
    participant aggLayer
    participant L1
    Note over chain_A: All bridgeExits <br/> from oldLER to newLER
    chain_A->>chain_A: Sign bridgeExits
    Note over chain_A: All claims (importedBridgeExits) <br/> from oldLER to newLER
    chain_A->>chain_A: Sign importedBridgeExits
    chain_A->>aggLayer: Certificate (data needed to build the PP)
    note over aggLayer: Build PP <br/> check PP consistency
    aggLayer->>L1: PP

Loading

As far as I understood this would be the data flow. Let me know if I'm missing something.

Some comments:

• aggLayer to maintain the LBT and the nullifierTree for each chain
  • each chain could also have a copy of them or the chain is the only to have them (and the chain send merkle paths necessary to the aggLayer)
• It will allow low-latency interoperability. I think this feature should not be taken into account in the very first stage of the PP since it adds complexity to the aggLayer. The design takes into account that, but I would say that it is for future aggLayer versions
  • If this is not taken into account in the first version, the approach 3 also will satisfy the needs for the very first version of the PP and maybe simplifies even more the aggLayer since all the work is done at chain level
• Approach 2 (selectedGER) reduces the PP since does not need to prove any claimed_LER
  • could this be an upper limit on numbers of claimed_LER to prove ?

[bpfarmer]

Thanks @krlosMata - few thoughts on this.

aggLayer to maintain the LBT and the nullifierTree for each chain

I would actually argue that the chain should maintain the LBT and NullifierSet. In this mode, we have a clean separation of what the agglayer does (maintains the L1InfoRoot and proves validity of LERs) and what's required for each chain to generate a PP.

It's not strictly required that the chain itself will generate a PP - it could be a service that we expose, but I think that it makes sense to separate this from the AL itself, as we can remove the requirement that AL nodes store LBT and NullifierSets.

It will allow low-latency interoperability. I think this feature should not be taken into account in the very first stage of the PP since it adds complexity to the aggLayer.

The nice thing is that it doesn't need to add any complexity. If we use the approach where PPs don't specify a GER, but the LER -> GER inclusion is proved at the final step, then we get the cross-chain consistency check for free. There are further protocol changes (allowing claims on the EVM with just LERs, not the GER) but all that's required by the AL for cross-chain consistency is to prove that LERs are valid.

[krlosMata]

I would actually argue that the chain should maintain the LBT and NullifierSet.

• 100% agree. Just with the bridgeExits and the importedBridgeExits you can build the LBT and the nullifierTree, so both the chain and the aggLayer could store them.
• If the aggLayer is totally agnostic to those trees, the chain must submit the merke-paths to the aggLayer to build the PP
  • I would say that it simplifies the data flow, in this first stage, if the aggLayer is the one that has all the LBT and the nulifierTree for every chain

It's not strictly required that the chain itself will generate a PP

• I think it is a "nice to have" feature at this first stage xD
• It futures stages I can see
  • each chain to build its own PP, chain_A_pp
  • sends to the aggLayer (it receives from multiples chains, chain_A_pp, chain_B_pp, ..., chain_Z_pp)
  • aggLayer build a proof of multiples LER inclusion in the L1InfoTree, proof_inclusion_LERs
  • aggLayer to build a proof that proves proof_inclusion_LERs & chain_A_pp & ... & chain_Z_pp

The nice thing is that it doesn't need to add any complexity

somehow the chain needs to know the other chain LER, so some sort of communication is needed and if we split the proofs it kinda add more complexity at this first stage

[bpfarmer]

Cool, I think that we mainly agree on everything

I would say that it simplifies the data flow, in this first stage, if the aggLayer is the one that has all the LBT and the nulifierTree for every chain

I'm just wondering if we can separate this from the main agglayer repo, as it's functionality that we don't strictly need. We could have a separate PP-generator service that could be run by the chain itself or by some other party.

somehow the chain needs to know the other chain LER, so some sort of communication is needed and if we split the proofs it kinda add more complexity at this first stage

The chain will have all of the LERs though - they'll be provided by users or builders during the claims process. The chain doesn't really care if the LER is old or new (for fast interop) - it can handle them all the same.

The main changes for fast interop would be in the zkEVM proof - instead of accepting a GER, chains could specify a set of LERs to process claims on.

[pgebheim]

I think it would make sense to split this out into a library with go, rust bindings as well as a service that can run as a sidecar for EVM chains.

We can then ask other folks to port this to svm, movevm etc.

[bpfarmer]

a library with go, rust bindings as well as a service that can run as a sidecar for EVM chains...port this to svm, movevm, etc

I don't think that any contract or VM changes should be required for this. We should be able to have a single implementation of a service written in Rust that can query or receive local LET and claim/deposit data to generate the proof. The LBT and Nullifier Set are generated entirely from the LET and claims/deposits.

[krlosMata]

I'm just wondering if we can separate this from the main agglayer repo, as it's functionality that we don't strictly need. We could have a separate PP-generator service that could be run by the chain itself or by some other party

yep, it can be separated. This is convenient to compute proofs in a stateless server (the service does not know anything about the LBT and the nullifierTree). This will imply high amount of data to be transferred to the service (merkle-paths basically) so it could have a delay associated with data transfer.

The chain will have all of the LERs though - they'll be provided by users or builders during the claims process. The chain doesn't really care if the LER is old or new (for fast interop) - it can handle them all the same

true. chain_A can read chain_B LERs produced by inspecting the bridge SC or provided by users.

The main changes for fast interop would be in the zkEVM proof - instead of accepting a GER, chains could specify a set of LERs to process claims on.

That is a huge change in the zkEVM proofs as well as in the Bridge L2 SC. It would need every chain to update its SC and its Verifier (forkID) (all chains do not need to update at the same time though...which is good).
I'm just thinking another viable solution. Make the update of the GER deterministic in L1. Say chain_A wants to update its LER_A. It chooses from which GER (mainnetExitRoot & rollupExitRoot) the LER_A is updated.
This will not imply updating all zkEVM chains and its Verifier...but only the rollupManager.sol and how the new GER is computed.
thoughts on this topic @invocamanman ?

[invocamanman]

• I think that separate the service as the first approach will be the most easy-straightforward path to implement it

• I understand that for fast interop will be in future steps, and it requires the aggLayer and some coordination. We can redefine later if we make a proof of some LERs inclusion, or we make some kind of "order/coordination" when submitting proofs

[bpfarmer]

true. chain_A can read chain_B LERs produced by inspecting the bridge SC or provided by users.

I guess one thing that I wasn't considering here is that the chain should ideally still have a way to verify that the LER provided by users is authenticated by a chain. In the short term we can just rely on an indexing service to do this, or expose an AL endpoint.

[bpfarmer]

@krlosMata @invocamanman - I think the argument for changing the protocol to use LERs instead of GERs for claims would be to support something like this more easily: https://hackmd.io/Cn5NqzC2TJ6dVg9AtmFOUw

Even for async messaging, we'd love to be able to interoperate at lower latency than AL epoch times (before a GER is generated).

[invocamanman]

I agree to make LER inclusions, it's closer to the final AL