# Mempool^2

> Mempool with ~~'sublists'~~ 'sublets', partioned non-gossiping pools for transactions privately sent, of transaction envelope type, etc

[TOC]

## Motivation


> fig, 1


> fig, 2

## Semantics

> Nonce Values are Arbitrarily Chosen
>
|Symbol|Description|Semantics|
|---|---|---|
|N|Normal Transaction|Standard transaction with base gas price (e.g. 3 Gwei)|
|P|Parent Transaction|Transaction with gas price < 12000, nonce = 0|
|C|Child Transaction|Transaction with value ≤ 10000, dependent on parent, with parent gas price < 12000|
|O|Other Transaction|Transaction with value > 10000 or dependent on a parent with gas price ≥ 12000|
|F|Future Transaction|Transaction with nonce = 10000, placed in the queued area|
|E|Empty Slot|Unused capacity in the transaction pool|
|R|Replacement Transaction|Transaction with gas price ≥ 12000, nonce = 0, replacing another transaction|

## Grammar Definition

$$ G = (V, Σ, R, S) $$

$$ V = {S, PoolState, QueuedState, PendingState, ParentSeq, ChildSeq} $$

$$ Σ = {N, P, C, O, F, E, R} $$

$$ S = PoolState $$

### Sublet State Transition Rules

PoolState → QueuedState PendingState
QueuedState → F* | ε
PendingState → N* ParentSeq* E*
ParentSeq → P ChildSeq | R ChildSeq
ChildSeq → C* | O* | C* O* | ε

Where:

- `*` indicates zero or more occurrences
- `ε` represents an empty string (no symbols)

## Transaction System Integrity Rules

These rules govern the admission and eviction of transactions within the sublet (and greater mempool) to maintain consistency and integrity.

> [!NOTE]
> This formalization intends to ensure that once valid transactions are accepted, the system maintains a consistent state regardless of subsequent invalid transaction attempts.

### Admission Rules

| Rule | Description | Logical Form |
| ---- | ------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------- |
| 1 | No admission of future transaction | $\forall tx [\text{Future}(tx) \rightarrow \neg \text{Admit}(tx)]$ |
| 2 | No admission of invalid transaction | $\forall tx [\neg \text{Valid}(tx) \rightarrow \neg \text{Admit}(tx)]$ |
| 3 | No admission of tx of the same sender | $\forall tx_1, tx_2 [\text{Sender}(tx_1) = \text{Sender}(tx_2) \wedge \text{InSystem}(tx_1) \rightarrow \neg \text{Admit}(tx_2)]$ |

### Eviction Rules

|Rule|Description|Logical Form|
|---|---|---|
|4|No eviction of valid tx by future/invalid tx|$\forall tx_1, tx_2 [\text{Valid}(tx_1) \wedge (\text{Future}(tx_2) \vee \neg \text{Valid}(tx_2)) \rightarrow \neg \text{CanEvict}(tx_2, tx_1)]$|
|5|No eviction of valid tx that transforms existing valid tx into future or invalid|$\forall tx_1, tx_2 [(\text{InSystem}(tx_1) \wedge \text{InSystem}(tx_2) \wedge \text{Valid}(tx_1) \wedge \text{Valid}(tx_2) \wedge \text{Depends}(tx_2, tx_1)) \rightarrow \neg(\exists \text{action} [\text{Evict}(tx_1) \wedge (\text{Transforms}(tx_1, tx_2, \text{Future}) \vee \text{Transforms}(tx_1, tx_2, \neg \text{Valid}))])]$|

> [!NOTE]
> Rule 5 is the most complex and ensures that the transaction dependency graph remains consistent.

### Transaction Predicate Definitions

- $\text{Valid}(tx)$: Transaction $tx$ is valid
- $\text{Future}(tx)$: Transaction $tx$ is future-dated
- $\text{InSystem}(tx)$: Transaction $tx$ is currently in the system
- accepted
- pending
- $\text{Depends}(tx_1, tx_2)$: Transaction $tx_2$ depends on transaction $tx_1$
- $\text{Evict}(tx)$: The action of evicting transaction $tx$
- $\text{Transforms}(tx_1, tx_2, \text{property})$: Removing $tx_1$ changes $tx_2$'s property

The complete formalization:

$$\forall tx_1, tx_2 [(\text{InSystem}(tx_1) \wedge \text{InSystem}(tx_2) \wedge \text{Valid}(tx_1) \wedge \text{Valid}(tx_2) \wedge \text{Depends}(tx_2, tx_1)) \rightarrow \neg(\exists \text{action} [\text{Evict}(tx_1) \wedge (\text{Transforms}(tx_1, tx_2, \text{Future}) \vee \text{Transforms}(tx_1, tx_2, \neg \text{Valid}))])]$$

## Formal Transaction Constraint Rules

The design of these rules is to realize the following set of requirements:

1. Maintains temporal consistency
2. Preserves system validity
3. Prevents double-submission
4. Protects valid transactions
5. Maintains transaction dependencies

v No admission of future transaction.
v No admission of invalid transaction.
v No admission of tx of the same sender
Ø No eviction of valid tx by future/invalid tx.
Ø No eviction of valid tx that transforms existing valid tx into future or invalid.

> - "v" represents admission rules (what transactions can enter the system)
> - "Ø" represents eviction rules (what transactions can't be removed from the system)

### No admission of future transaction

"No admission of future transaction": This rule means that transactions with timestamps in the 'far' future cannot be admitted into the system. Think of it like a bank refusing to process a check dated next month. The system maintains temporal consistency by only accepting transactions that could logically occur at the current time.

### No admission of invalid transaction

"No admission of invalid transaction": The system must reject any transaction that violates its validity rules. For example, if someone tries to spend money they don't have or execute a smart contract with incorrect parameters, that transaction would be rejected immediately. This maintains the system's integrity by preventing corrupt or malformed transactions from entering.

### No admission of tx of the same sender

"No admission of tx of the same sender": This rule prevents double-submission from the same sender. It's similar to how a bank wouldn't process two identical checks from the same person. The system ensures that a sender can't have multiple pending transactions, which helps prevent double-spending and maintains transaction ordering.

> This assumes a normal nonce scheme, e.g. no consideration for a 'bitmap' style nonce mechanism

### No eviction of valid tx by future/invalid tx

"No eviction of valid tx by future/invalid tx": This rule protects valid transactions that are already in the system. Even if future-dated or invalid transactions somehow enter the system, they cannot cause the removal of legitimate transactions. This is like ensuring that a valid bank transfer can't be cancelled by an invalid one that comes later.

### No eviction of valid tx that transforms existing valid tx into future or invalid

"No eviction of valid tx that transforms existing valid tx into future or invalid": This is the most complex rule. It prevents the removal of valid transactions that, if removed, would make other valid transactions become future-dated or invalid. For example, if Transaction A creates an account and Transaction B spends from it, you can't remove Transaction A because that would make Transaction B invalid. This maintains the consistency of transaction chains and prevents cascade failures.

---

> Work in Progress

## Sublets: Transaction pool partitions

This EIP proposes how miners can partition transactions into disjoint sets that can be safely executed in parallel, and how full nodes should process and validate these transactions.

## Specification

### Basic Definitions

Let us define the following:

- $T = {t_1, t_2, ..., t_n}$ is the set of all transactions in a block
- $K$ is the set of all possible state keys in the Ethereum state trie
- For any transaction $t \in T$:
- $R(t) \subseteq K$ is the set of keys that $t$ reads
- $W(t) \subseteq K$ is the set of keys that $t$ writes
- $S(t)$ is the sender address of transaction $t$
- $G(t)$ is the gas consumed by transaction $t$

### Transaction Connectivity Relation

We define a binary relation $C \subseteq T \times T$ where $(t_i, t_j) \in C$ if and only if $t_i$ and $t_j$ are related. This relation is defined as:

$(t_i, t_j) \in C \iff (W(t_i) \cap W(t_j) \neq \emptyset) \lor (W(t_i) \cap R(t_j) \neq \emptyset) \lor (R(t_i) \cap W(t_j) \neq \emptyset) \lor (S(t_i) = S(t_j))$

Two transactions are related if any of the following conditions are true:

- They both write to at least one common key
- One transaction writes to a key that the other transaction reads
- They have the same sender address (as they modify the same nonce)

### Connectivity Relation

The connectivity relation $C$ has the following qualities:

- **Symmetricity**: $\forall t_i, t_j \in T: (t_i, t_j) \in C \iff (t_j, t_i) \in C$
- **Reflexivity**: $\forall t \in T: (t, t) \in C$

We define the *connectivity closure* of a transaction $t$ as: $CL(t) = {t' \in T | (t, t') \in C}$

Similarly, for any set of transactions $S \subseteq T$, we define: $CL(S) = {t' \in T | \exists t \in S: (t, t') \in C}$

## Sublist

### Definitions and Constraints

A valid partitioning of the transaction set $T$ consists of sublists $P_1, P_2, ..., P_N, S$ such that:

1. $P_1 \cup P_2 \cup ... \cup P_N \cup S = T$ (all transactions are included)
2. $P_i \cap P_j = \emptyset$ for all $i \neq j$ (sublists are disjoint)
3. $P_i \cap S = \emptyset$ for all $i$ (parallel and sequential sublists are disjoint)
4. For all $i \neq j$ and for all $t_a \in P_i$ and $t_b \in P_j$, $(t_a, t_b) \notin C$ (transactions in different parallel sublists are not connected)
5. For all $i$, $\sum_{t \in P_i} G(t) \leq \text{parallelSublistGasLimit}$ (gas limit constraint for parallel sublists)
6. $\sum_{t \in S} G(t) \leq \text{sequentialSublistGasLimit}$ (gas limit constraint for sequential sublist)

### Sublist Execution

1. Let $\sigma_0$ be the initial state before any transaction executes
2. Let $\sigma_{seq}$ be the final state after all transactions execute sequentially
3. Let $\sigma_{par}$ be the final state after parallel execution of the partition

For a parallel sublist $P_i$, let $\sigma_0 \xrightarrow{P_i} \sigma_i$ denote the state transition from the initial state $\sigma_0$ to state $\sigma_i$ after executing all transactions in $P_i$.

Then, due to the connectivity constraints, we can prove:

- For any two parallel sublists $P_i$ and $P_j$ where $i \neq j$, $\sigma_0 \xrightarrow{P_i} \sigma_i$ and $\sigma_0 \xrightarrow{P_j} \sigma_j$ modify disjoint portions of the state
- Therefore, there exists a state $\sigma_P$ such that $\sigma_0 \xrightarrow{P_1 \cup P_2 \cup ... \cup P_N} \sigma_P$
- Finally, $\sigma_P \xrightarrow{S} \sigma_{par} = \sigma_{seq}$

### 🚧 Transaction Partitioning

Transactions in a block are divided into `N+1` sublists:

- The first `N` sublists (called "parallel sublists") are executed in parallel
- The last sublist (called the "sequential sublist") is executed after all parallel sublists have completed

### 🚧 'Partioned' Block Gas Limit and Blob Limit

> [!CAUTION]
> Under Consideration

Each sublist has its own gas limit value and blob transaction limit. The current block `gasLimit` constant is replaced with three new constants:

- `parallelSublistGasLimit`: the gas limit for a parallel sublist
- `sequentialSublistGasLimit`: the gas limit for a sequential sublist
- `blobSublistLimit`: the limit for blob submissions to a sublist

Both values are initially set to `(block gas limit / (N+1))`.

### Sublist Field

> Can we add a 'SideCar' field (like the BlobSideCar data attached) that contains an array of unsigned integers that indicates where each sublist ends in the transaction list.

---

## Appendix

### **PreStateAccount**

Represents an account's state before execution.

- **Properties**:
- `balance` (`ConfusedHexType`): The account's balance.
- `code` (`HexMaybePrefixOrEmpty`): The account's deployed smart contract code.
- `nonce` (`ConfusedHexType`): The transaction nonce.
- `storage` (`object`):
- Keys match the regex pattern `^0x[0-9a-f]+`.
- Values are of type `HexData`, representing storage values.

- **Constraints**:
- `balance`, `code`, and `nonce` are **required**.
- `storage` does **not** allow additional properties outside the defined pattern.

### **Ethereum State Transition Object**
Each key in the object represents an Ethereum transaction's state.

- **Properties**:
- `_metadata` (`Metadata`): Metadata about the transaction.
- `env` (`object`): Describes the current execution environment.
- **Properties**:
- `currentCoinbase` (`HexData`): Miner address, Alias ETHERBASE.
- `currentDifficulty` (`ConfusedHexType`): Block difficulty.
- `currentGasLimit` (`ConfusedHexType`): Maximum gas allowed per block.
- `currentNumber` (`ConfusedHexType`): Current block number.
- `currentTimestamp` (`ConfusedHexType`): Block timestamp.

- **Constraints**:
- All properties are **required**.

- `exec` (`object`): Defines current transaction execution details.
- **Properties**:
- `address` (`AddressMaybePrefixOrEmpty`): Contract address.
- `caller` (`AddressMaybePrefixOrEmpty`): Transaction sender.
- `code` (`HexMaybePrefixOrEmpty`): Smart contract bytecode.
- `data` (`HexDataOrEmpty`): Input data payload.
- `gas` (`IntegerOrEmptyOrConfusedHex`): Gas limit.
- `gasPrice` (`IntegerOrEmptyOrConfusedHex`): Gas price per unit.
- `origin` (`AddressMaybePrefixOrEmpty`): Original transaction sender.
- `value` (`IntegerOrEmptyOrConfusedHex`): ETH value transferred.

- **Constraints**:
- All properties are **required**.

- `gas` (`IntegerOrEmptyOrConfusedHex`): Total gas used.
- `logs` (`HexDataOrEmpty`): Transaction logs.
- `out` (`HexDataOrEmpty`): Transaction output.
- `pre` (`object`): Pre-execution account state.
- **Pattern Properties**:
- Keys match `^0x[0-9a-f]*` (Ethereum addresses).
- Values are of type `PreStateAccount`.
- `post` (`object`): Post-execution account state.
- **Pattern Properties**:
- Keys match `^0x[0-9a-f]*` (Ethereum addresses).
- Values are of type `PreStateAccount`.

- **Constraints**:
- `_info`, `env`, and `exec` are **required**.
- `pre` and `post` states must conform to `PreStateAccount`.