docs: add compression circuit outline (#4599)

Fixes #4558.

Adds a section to the yellow-paper on message compression circuits for L1 -> L2 message following #4250

yarn-project/circuits.js/src/structs/aggregation_object.ts

@@ -6,7 +6,7 @@ import { UInt32, Vector } from './shared.js';
 import { G1AffineElement } from './verification_key.js';
 
 /**
- * Contains the aggregated proof of all the previous kernel iterations.
+ * Contains the aggregated elements to be used as public inputs for delayed final verification.
  *
  * See barretenberg/cpp/src/barretenberg/stdlib/recursion/aggregation_state/native_aggregation_state.hpp
  * for more context.

yellow-paper/docs/l1-smart-contracts/index.md

@@ -33,13 +33,20 @@ def process(block: ProvenBlock, proof: Proof):
     assert self.outbox.insert(
         block_number, 
         header.content_commitment.out_hash, 
-        header.content_commitment.tx_tree_height
+        header.content_commitment.tx_tree_height + math.ceil(log2(MAX_NEW_L2_TO_L1_MSGS_PER_TX))
     )
     self.archive = block.archive
 
     emit BlockProcessed(block_number)
 ```
 
+:::info Why `math.ceil(log2(MAX_NEW_L2_TO_L1_MSGS_PER_TX))`?
+The argument to the `insert` function is the `outbox` is the heigh of the message tree.
+Since every transaction can hold more than 1 message, it might add multiple layers to the tree.
+For a binary tree, the number of extra layers to add is computed as `math.ceil(log2(MAX_NEW_L2_TO_L1_MSGS_PER_TX))`.
+Currently, `MAX_NEW_L2_TO_L1_MSGS_PER_TX = 2` which means that we are simply adding 1 extra layer. 
+:::
+
 While the `ProvenBlock` must be published and available for nodes to build the state of the rollup, we can build the validating light node (the contract) such that as long as the node can be _convinced_ that the data is available we can progress the state. 
 This means our light node can be built to only require a subset of the `ProvenBlock` to be published to Ethereum L1 as calldata and use a different data availability layer for most of the block body.
 Namely, we need the cross-chain messages to be published to L1, but the rest of the block body can be published to a different data availability layer.
@@ -112,17 +119,16 @@ class StateTransitioner:
         archive: Fr,
         proof: Proof
     ):
-        assert self.AVAILABILITY_ORACLE.is_available(txs_hash)
+        assert self.AVAILABILITY_ORACLE.is_available(header.content_commitment.txs_hash)
         assert self.validate_header(header)
-        assert self.archive == header.last_archive
-        assert VERIFIER.verify(header, block.archive, proof)
-        assert self.INBOX.consume() == header.in_hash
+        assert VERIFIER.verify(header, archive, proof)
+        assert self.INBOX.consume() == header.content_commitment.in_hash
         assert self.OUTBOX.insert(
             block_number, 
             header.content_commitment.out_hash, 
-            header.content_commitment.tx_tree_height
+            header.content_commitment.tx_tree_height + math.ceil(log2(MAX_NEW_L2_TO_L1_MSGS_PER_TX))
         )
-        self.archive = block.archive
+        self.archive = archive
         emit BlockProcessed(block_number)
 
     def validate_header(
@@ -287,10 +293,7 @@ As mentioned earlier, this is done to ensure that the messages are not used to D
 Since we will be building the tree on L1, we need to use a gas-friendly hash-function such as SHA256. 
 However, as we need to allow users to prove inclusion in this tree, we cannot just insert the SHA256 tree into the rollup state, it requires too many constraints to be used by most small users. 
 Therefore, we need to "convert" the tree into a tree using a more snark-friendly hash.
-This part is done in a to-be-defined circuit.
-:::info TODO
-Write about the `MessageCompression` circuits
-:::
+This part is done in the [tree parity circuits](./../rollup-circuits/tree-parity.md).
 
 Furthermore, to build the tree on L1, we need to put some storage on L1 such that the insertions don't need to provide a lot of merkle-related data which could be cumbersome to do and prone to race-conditions. 
 For example two insertions based on inclusion paths that are created at the same time will invalidate each other. 
@@ -423,6 +426,7 @@ class Outbox:
     inclusion_proof: bytes[]
   ):
     leaf = message.hash_to_field()
+    assert msg_sender == message.recipient.actor
     assert merkle_verify(
       self.roots[root_index].root,
       self.roots[root_index].height,
@@ -466,9 +470,7 @@ Also, some of the conditions are repetitions of what we saw earlier from the [st
   - The `(sender|recipient).version` MUST be the version of the state transitioner (the version of the L2 specified in the L1 contract)
   - The `content` MUST fit within a field element
   - For L1 to L2 messages:
-    - The `deadline` MUST be in the future, `> block.timestamp`
     - The `secretHash` MUST fit in a field element
-    - The caller MAY append a `fee` to incentivize the sequencer to pick up the message
 - **Moving tree roots**:
   - Moves MUST be atomic:
     - Any message that is inserted into an outbox MUST be consumed from the matching inbox

yellow-paper/docs/rollup-circuits/index.md

@@ -4,22 +4,31 @@ title: Rollup Circuits
 
 ## Overview
 
-Together with the [validating light node](../l1-smart-contracts/index.md) the rollup circuits must ensure that incoming blocks are valid, that state is progressed correctly and that anyone can rebuild the state.
-
-To support this, we construct a single proof for the entire block, which is then verified by the validating light node. 
-This single proof is constructed by recursively merging proofs together in a binary tree structure. 
-This structure allows us to keep the workload of each individual proof small, while making it very parallelizable. 
+Together with the [validating light node](../l1-smart-contracts/index.md), the rollup circuits must ensure that incoming blocks are valid, that state is progressed correctly, and that anyone can rebuild the state.
+
+To support this, we construct a single proof for the entire block, which is then verified by the validating light node.
+This single proof consist of three main components:
+It has **two** sub-trees for transactions, and **one** tree for L1 to L2 messages. 
+The two transaction trees are then merged into a single proof and combined with the roots of the message tree to form the final proof and output.
+Each of these trees are built by recursively combining proofs from a lower level of the tree.
+This structure allows us to keep the workload of each individual proof small, while making it very parallelizable.
 This works very well for the case where we want many actors to be able to participate in the proof generation.
 
-The tree structure is outlined below, but the general idea is that we have a tree where all the leaves are transactions (kernel proofs) and through $\log(n)$ steps we can then "compress" them down to just a single root proof. 
-Note that we have two different types of "merger" circuit, namely:
+Note that we have two different types of "merger" circuits, depending on what they are combining. 
+
+For transactions we have:
+- The `merge` rollup
+  - Merges two `base` rollup proofs OR two `merge` rollup proofs
+- The `root` rollup
+  - Merges two `merge` rollup proofs
 
-- The merge rollup
-  - Merges two base rollup proofs OR two merge rollup proofs
-- The root rollup
-  - Merges two merge rollup proofs
+And for the message parity we have:
+- The `root` circuit
+  - Merges `N` `root` or `leaf` proofs
+- The `leaf` circuit
+  - Merges `N` l1 to l2 messages in a subtree 
 
-In the diagram the size of the tree is limited for show, but a larger tree will have more layers of merge rollups proofs. 
+In the diagram the size of the tree is limited for demonstration purposes, but a larger tree would have more layers of merge rollups proofs. 
 Circles mark the different types of proofs, while squares mark the different circuit types.
 
 ```mermaid
@@ -77,6 +86,54 @@ graph BT
     style K1 fill:#1976D2;
     style K2 fill:#1976D2;
     style K3 fill:#1976D2;
+
+    R --> R_c
+
+    R((RootParity))
+
+    T0[LeafParity]
+    T1[LeafParity]
+    T2[LeafParity]
+    T3[LeafParity]
+
+    T0_P((RootParity 0))
+    T1_P((RootParity 1))
+    T2_P((RootParity 2))
+    T3_P((RootParity 3))
+
+    T4[RootParity]
+
+    I0 --> T0
+    I1 --> T1
+    I2 --> T2
+    I3 --> T3
+
+    T0 --> T0_P
+    T1 --> T1_P
+    T2 --> T2_P
+    T3 --> T3_P
+
+    T0_P --> T4
+    T1_P --> T4
+    T2_P --> T4
+    T3_P --> T4
+
+    T4 --> R
+
+    I0((MSG 0-3))
+    I1((MSG 4-7))
+    I2((MSG 8-11))
+    I3((MSG 12-15))
+
+    style R fill:#1976D2;
+    style T0_P fill:#1976D2;
+    style T1_P fill:#1976D2;
+    style T2_P fill:#1976D2;
+    style T3_P fill:#1976D2;
+    style I0 fill:#1976D2;
+    style I1 fill:#1976D2;
+    style I2 fill:#1976D2;
+    style I3 fill:#1976D2;
 ```
 
 To understand what the circuits are doing and what checks they need to apply it is useful to understand what data is going into the circuits and what data is coming out.
@@ -314,37 +371,41 @@ class MergeRollupInputs {
 MergeRollupInputs *-- ChildRollupData: left
 MergeRollupInputs *-- ChildRollupData: right
 
+class LeafParityInputs {
+    msgs: List~Fr[2]~
+}
+
+class ParityPublicInputs {
+    aggregation_object: AggregationObject
+    sha_root: Fr[2]
+    converted_root: Fr
+}
+
+class RootParityInputs {
+    children: List~ParityPublicInputs~
+}
+RootParityInputs *-- ParityPublicInputs: children
+
+class RootParityInput {
+    proof: Proof
+    public_inputs: ParityPublicInputs
+}
+RootParityInput *-- ParityPublicInputs: public_inputs
+
 class RootRollupInputs {
-    l1_to_l2_roots: MessageCompressionBaseOrMergePublicInputs
+    l1_to_l2_roots: RootParityInput
     l1_to_l2_msgs_sibling_path: List~Fr~
     parent: Header,
     parent_sibling_path: List~Fr~
     archive_sibling_path: List~Fr~
     left: ChildRollupData
     right: ChildRollupData
 }
-RootRollupInputs *-- MessageCompressionBaseOrMergePublicInputs: l1_to_l2_roots
+RootRollupInputs *-- RootParityInput: l1_to_l2_roots
 RootRollupInputs *-- ChildRollupData: left
 RootRollupInputs *-- ChildRollupData: right
 RootRollupInputs *-- Header : parent
 
-class MessageCompressionBaseInputs {
-    l1_to_l2_msgs: List~Fr~
-}
-
-class MessageCompressionBaseOrMergePublicInputs {
-    sha_root: Fr[2]
-    converted_root: Fr
-}
-
-class MessageCompressionMergeInputs {
-    left: MessageCompressionBaseInputs
-    right: MessageCompressionBaseInputs
-}
-MessageCompressionMergeInputs *-- MessageCompressionBaseOrMergePublicInputs: left
-MessageCompressionMergeInputs *-- MessageCompressionBaseOrMergePublicInputs: right
-
-
 class RootRollupPublicInputs {
     aggregation_object: AggregationObject
     archive: Snapshot

yellow-paper/docs/rollup-circuits/root-rollup.md

@@ -131,21 +131,37 @@ class ChildRollupData {
 }
 ChildRollupData *-- BaseOrMergeRollupPublicInputs: public_inputs
 
-class MessageCompressionBaseOrMergePublicInputs {
+
+class LeafParityInputs {
+    msgs: List~Fr[2]~
+}
+
+class ParityPublicInputs {
+    aggregation_object: AggregationObject
     sha_root: Fr[2]
     converted_root: Fr
 }
 
+class RootParityInputs {
+    children: List~ParityPublicInputs~
+}
+RootParityInputs *-- ParityPublicInputs: children
+
+class RootParityInput {
+    proof: Proof
+    public_inputs: ParityPublicInputs
+}
+RootParityInput *-- ParityPublicInputs: public_inputs
 class RootRollupInputs {
-    l1_to_l2_roots: MessageCompressionBaseOrMergePublicInputs
+    l1_to_l2_roots: RootParityInput
     l1_to_l2_msgs_sibling_path: List~Fr~
     parent: Header,
     parent_sibling_path: List~Fr~
     archive_sibling_path: List~Fr~
     left: ChildRollupData
     right: ChildRollupData
 }
-RootRollupInputs *-- MessageCompressionBaseOrMergePublicInputs: l1_to_l2_roots
+RootRollupInputs *-- RootParityInput: l1_to_l2_roots
 RootRollupInputs *-- ChildRollupData: left
 RootRollupInputs *-- ChildRollupData: right
 RootRollupInputs *-- Header : parent
@@ -162,7 +178,7 @@ RootRollupPublicInputs *--Header : header
 
 ```python
 def RootRollupCircuit(
-    l1_to_l2_roots: MessageCompressionBaseOrMergePublicInputs,
+    l1_to_l2_roots: RootParityInput,
     l1_to_l2_msgs_sibling_path: List[Fr],
     parent: Header,
     parent_sibling_path: List[Fr],
@@ -172,6 +188,7 @@ def RootRollupCircuit(
 ) -> RootRollupPublicInputs:
     assert left.proof.is_valid(left.public_inputs)
     assert right.proof.is_valid(right.public_inputs)
+    assert l1_to_l2_roots.proof.verify(l1_to_l2_roots.public_inputs)
 
     assert left.public_inputs.constants == right.public_inputs.constants
     assert left.public_inputs.end == right.public_inputs.start
@@ -191,7 +208,7 @@ def RootRollupCircuit(
     # Update the l1 to l2 msg tree
     l1_to_l2_msg_tree = merkle_insertion(
         parent.state.l1_to_l2_message_tree,
-        l1_to_l2_roots.converted_root,
+        l1_to_l2_roots.public_inputs.converted_root,
         l1_to_l2_msgs_sibling_path,
         L1_TO_L2_SUBTREE_HEIGHT,
         L1_To_L2_HEIGHT
@@ -202,7 +219,7 @@ def RootRollupCircuit(
         content_commitment: ContentCommitment(
             tx_tree_height = left.public_inputs.height_in_block_tree + 1,
             txs_hash = SHA256(left.public_inputs.txs_hash | right.public_inputs.txs_hash),
-            in_hash = l1_to_l2_roots.sha_root,
+            in_hash = l1_to_l2_roots.public_inputs.sha_root,
             out_hash = SHA256(left.public_inputs.out_hash | right.public_inputs.out_hash),
         ),
         state = StateReference(