Mempool^2

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

• Mempool^2
  • Motivation
  • Semantics
  • Grammar Definition
    • Sublet State Transition Rules
  • Transaction System Integrity Rules
    • Admission Rules
    • Eviction Rules
    • Transaction Predicate Definitions
  • Formal Transaction Constraint Rules
    • No admission of future transaction
    • No admission of invalid transaction
    • 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
  • Sublets: Transaction pool partitions
  • Specification
    • Basic Definitions
    • Transaction Connectivity Relation
    • Connectivity Relation
  • Sublist
    • Definitions and Constraints
    • Sublist Execution
    • 🚧 Transaction Partitioning
    • 🚧 'Partioned' Block Gas Limit and Blob Limit
    • Sublist Field
  • Appendix
    • PreStateAccount
    • Ethereum State Transition Object

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,\Sigma ,R,S)$$

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

$$\Sigma =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	$\mathrm{\forall }tx[\text{Future}(tx)\to \mathrm{\neg }\text{Admit}(tx)]$
2	No admission of invalid transaction	$\mathrm{\forall }tx[\mathrm{\neg }\text{Valid}(tx)\to \mathrm{\neg }\text{Admit}(tx)]$
3	No admission of tx of the same sender	$\mathrm{\forall }t{x}_1,t{x}_2[\text{Sender}(t{x}_1)=\text{Sender}(t{x}_2)\wedge \text{InSystem}(t{x}_1)\to \mathrm{\neg }\text{Admit}(t{x}_2)]$

Eviction Rules

Rule	Description	Logical Form
4	No eviction of valid tx by future/invalid tx	$\mathrm{\forall }t{x}_1,t{x}_2[\text{Valid}(t{x}_1)\wedge (\text{Future}(t{x}_2)\vee \mathrm{\neg }\text{Valid}(t{x}_2))\to \mathrm{\neg }\text{CanEvict}(t{x}_2,t{x}_1)]$
5	No eviction of valid tx that transforms existing valid tx into future or invalid	$\mathrm{\forall }t{x}_1,t{x}_2[(\text{InSystem}(t{x}_1)\wedge \text{InSystem}(t{x}_2)\wedge \text{Valid}(t{x}_1)\wedge \text{Valid}(t{x}_2)\wedge \text{Depends}(t{x}_2,t{x}_1))\to \mathrm{\neg }(\mathrm{\exists }\text{action}[\text{Evict}(t{x}_1)\wedge (\text{Transforms}(t{x}_1,t{x}_2,\text{Future})\vee \text{Transforms}(t{x}_1,t{x}_2,\mathrm{\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}(t{x}_1,t{x}_2)$: Transaction
  $t{x}_2$ depends on transaction
  $t{x}_1$
• $\text{Evict}(tx)$: The action of evicting transaction
  $tx$
• $\text{Transforms}(t{x}_1,t{x}_2,\text{property})$: Removing
  $t{x}_1$ changes
  $t{x}_2$'s property

The complete formalization:

$$\mathrm{\forall }t{x}_1,t{x}_2[(\text{InSystem}(t{x}_1)\wedge \text{InSystem}(t{x}_2)\wedge \text{Valid}(t{x}_1)\wedge \text{Valid}(t{x}_2)\wedge \text{Depends}(t{x}_2,t{x}_1))\to \mathrm{\neg }(\mathrm{\exists }\text{action}[\text{Evict}(t{x}_1)\wedge (\text{Transforms}(t{x}_1,t{x}_2,\text{Future})\vee \text{Transforms}(t{x}_1,t{x}_2,\mathrm{\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⟺(W(t_i)\cap W(t_j)\ne \mathrm{\varnothing })\vee (W(t_i)\cap R(t_j)\ne \mathrm{\varnothing })\vee (R(t_i)\cap W(t_j)\ne \mathrm{\varnothing })\vee (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:
  $\mathrm{\forall }{t}_i,t_j\in T:(t_i,t_j)\in C⟺(t_j,t_i)\in C$
• Reflexivity:
  $\mathrm{\forall }t\in T:(t,t)\in C$

We define the connectivity closure of a transaction

$t$ as:

$CL(t)=t^{\prime }\in T|(t,t^{\prime })\in C$

Similarly, for any set of transactions

$S\subseteq T$, we define:

$CL(S)=t^{\prime }\in T|\mathrm{\exists }t\in S:(t,t^{\prime })\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=\mathrm{\varnothing }$ for all
   $i\ne j$ (sublists are disjoint)
3. $P_i\cap S=\mathrm{\varnothing }$ for all
   $i$ (parallel and sequential sublists are disjoint)
4. For all
   $i\ne 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)\le \text{parallelSublistGasLimit}$ (gas limit constraint for parallel sublists)
6. $\sum _{t\in S}G(t)\le \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\stackrel{P_i}{\to }{\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\ne j$,
  ${\sigma }_0\stackrel{P_i}{\to }{\sigma }_i$ and
  ${\sigma }_0\stackrel{P_j}{\to }{\sigma }_j$ modify disjoint portions of the state
• Therefore, there exists a state
  ${\sigma }_P$ such that
  ${\sigma }_0\stackrel{P_1\cup P_2\cup ...\cup P_N}{\to }{\sigma }_P$
• Finally,
  ${\sigma }_P\stackrel{S}{\to }{\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.