selectedGER Vs l1InfoRoot

[krlosMata]

Note: Previous discussion can be found in --> #107 (comment)

@invocamanman pointed out a concern regarding how to get the data from a SC Bridge claimAsset when this called in an internal call. Get information it is not then straightforward, since a trace needs to be analyze in order to get the smtProofs used.

Given that trade-off and the rest of them mentioned on the previous thread --> #107 (comment)
it is still worth the l1InfoTree or the selectedGER ?

In my view, even if:

• the proof gets larger because all the claimed_local_exit_roots needs to be verified against the L1InfoRoot
• get data when a event claimAsset is triggered via an internal call is tricky

it is worth to use the l1InfoTree because:

• aligned with medium-long term view to separate proofs
• avoids dependency on the bridges-service on other networks
• reuses all claimAsset data

@invocamanman @HarryTmetic @pgebheim

[bpfarmer]

I agree on the l1InfoTree approach. I think that aligning the protocol as much as possible from a data-flow perspective (not making the PP proof generation sync with a GER) makes the most sense to me.

It may also be good to spec out how we want to prove LER inclusion into GERs for the case in which chains are producing many LERs in a single epoch. I think that this should be straightforward with an update proof, but ideally we want to allow chains to produce an LER, sign it, send a message to another chain, and then continue producing more LERs, within a single epoch.

[bpfarmer]

Hi @invocamanman agree 100% on proving the inclusion of "intermediate" LERs.

I agree that the LER_Tree approach works and is a natural solution for this.

However, suppose that chains are producing a bunch of intermediate LERs on each block, but only one GER is created for each epoch. Wouldn't it be possible to prove inclusion of these intermediate LERs in the final LER that's included in the GER? It's a bit awkward because it's an SMT, but I think that it should be possible with O(log(n)) nodes.

With this approach, we could combine both - we could have the PP have LERs (not a GER) as public inputs, but then prove inclusion of all LERs in the latest GER. This would give us the final version of the PP, and a simple additional proof for the LER -> GER inclusion.

The advantage of this approach is that we wouldn't need to change the GER structure in the short term, or add another L1InfoRoot-type structure to the AL.

Does that make sense?

[bpfarmer]

Adding a bit more detail here - the way to prove inclusion of a previous LER_A in a future LER_B would be to:

• Prove that a particular node is a frontier node in LER_A at index k by showing that the right-adjacent leaf has a value of zero in LER_A.
• Generate the inclusion path P of the k-th node in LER_A.
• Generate the inclusion path P' of the k-th node in LER_B.
• Show that entries of P mapping to completed subtrees in LER_A are also contained in P'. Need to go back and think through this, but I think that it suffices to binary-decompose k, pad to 32 bits and reverse the bit order. Call this array of bits B. Verify P[i] = P'[i] for index i where B[i] = 1.
• EDIT probably simpler to just look at the pivot entry in each path. Anywhere where the provided node is a left node must match in the two paths.

This actually simplifies the protocol quite a bit. We'll have per-chain PPs and then an aggregation step where we aggregate all of the PPs. This step will merge the lists of LERs from all of the PPs (and delete duplicates) and then show their inclusion in the created GER.

It feels like this is a clean approach! 😁

[bpfarmer]

Follow-up: this does require that chains or the proving service would submit LERs and also the LER-diff proof as described above to the AL for each block, so that the PP can generate these proofs. This wouldn't be signed but would be metadata included in the Certificate.

[invocamanman]

Hey!
Yes i totally agree this does makes sense and seems a clear approach ^^
P[i] = P'[i] for index i where B[i] = 1 and think it should be 0 right, 0 are the left nodes right? ( just to check if i understood correctly!?)
But nice one!!! didn't think about it was pretty easy to proof inclusion of one merkle tree into another just with 2 merkle proofs.

Will think little bit more through it tho, but i think it could work ^^^

[bpfarmer]

Yes! I was dumb and thought that we needed to binary-decompose k but we can already identify the left nodes (and binary decomposition) based on the pivot (L/R) information from the path P. If B is a binary decomposition then it's where B[i]=1 but if B encodes the set of pivots then I think it's reversed (B[i]=0) - 0 maps to the left node.

[krlosMata]

Just a point on the L1InfoTree...since it provides all the history of GER, you can access chain LER_i and LER_i+1. Therefore, you can access all intermediate LERs if you know all the bridgeExits that happen in that chain for that specific LER change, i to i+1.
For rollups, data is on L1. For other chains, they need to be available via aggLayer

[bpfarmer]

I think that this approach of proving inclusion in the GER is better than L1InfoRoot for two reasons:

• I think it reduces verification cost on L1 because we don't need to look up historical LERs, though maybe that's marginal.
• As @invocamanman noted and I have mentioned elsewhere, we need to be able to access LERs at a greater level of granularity than we get in the L1InfoRoot. Imagine that a chain produces blocks every 250ms but the AggLayer produces a GER every 30 minutes. We'd like to be able to allow chains to use the LERs produced in the blocks rather than waiting 30 minutes for interop.

For rollups, data is on L1. For other chains, they need to be available via aggLayer

I don't think that the AL needs to handle DA but I could be misunderstanding. I think that we assume that from the perspective of the PP, the witness for a claim (or ImportedBridgeExit) is provided by a user to the chain operator, and then the DA of the chain's LER is guaranteed by whatever method the chain uses. For a rollup, it's on L1, for a validium, it's guaranteed by the DAC.

[bpfarmer]

@krlosMata I think this is mostly my fault - I misunderstood and thought you meant that we would verify all LER -> GER inclusion on L1, rather than use the L1InfoRoot in the PP 😞

[krlosMata]

I did not explain myself properly and back then, it was less clear.
Both approaches were good also, each one with its trade-offs.

[HarryTmetic]

It looks like we're starting to dive into a new topic. To keep this discussion focused on its original purpose, I've opened a new discussion (#119) thread where we can continue this nice tangent!

[HarryTmetic]

Closing this discussion since the selectedGER option was chosen.

[HarryTmetic]

Update: pivot to the l1InfoRoot approach in order to trim the interactions cdk <> agglayer
cf. https://hackmd.io/kFxTeOaERgKldVhR0bQvOA?view

cc: @arnaubennassar