# Masquerade: Simple and Lightweight Transaction Reordering Mitigation in
Blockchains

Arti Vedula<EMAIL_ADDRESS>0000-0002-2465-352X The Ohio State
UniversityColumbusOhioUSA43210 ,  Shaileshh Bojja Venkatakrishnan
<EMAIL_ADDRESS>The Ohio State UniversityColumbusOhioUSA43210
and  Abhishek Gupta<EMAIL_ADDRESS>The Ohio State
UniversityColumbusOhioUSA43210

###### Abstract.

Blockchains offer strong security gurarantees, but cannot protect users
against the ordering of transactions. Players such as miners, bots and
validators can reorder various transactions and reap significant profits,
called the Maximal Extractable Value (MEV). In this paper, we propose an MEV
aware protocol design called Masquerade, and show that it will increase user
satisfaction and confidence in the system. We propose a strict per-transaction
level of ordering to ensure that a transaction is committed either way even if
it is revealed. In this protocol, we introduce the notion of a ”token” to
mitigate the actions taken by an adversary in an attack scenario. Such tokens
can be purchased voluntarily by users, who can then choose to include the
token numbers in their transactions. If the users include the token in their
transactions, then our protocol requires the block-builder to order the
transactions strictly according to token numbers. We show through extensive
simulations that this reduces the probability that the adversaries can benefit
from MEV transactions as compared to existing current practices.

##  1\. Introduction

Blockchains offer a decentralized and transparent platform for recording
transactions with strong security guarantees. Originally conceived as a
payment system, in recent years smart contracts in blockchains have enabled
the development of a plethora of decentralized applications (dapps) in myriad
service sectors. Among these, dapps developed for financial use cases—such as
lending and borrowing, stablecoins, exchanges, insurance etc.—have emerged as
a popular alternative to centralized financial institutions. Colloquially
referred to as de-fi (for decentralized finance), financial smart contracts
are projected to grow to a half a trillion market (def, 2023).

Concurrent with the growth of defi dapps, transaction reordering attacks have
become commonplace in blockchains. This is when a malicious actor attempts to
confirm its own transaction ahead of a victim transaction on the blockchain
after observing the victim transaction. A frontrunning attack is problematic
to the victim as it can unfairly diminish the value earned by the victim in
the transaction. For example, a victim looking to purchase tokens available at
a lower-than-market price at a decentralized exchange may not get that price
if the attacker purchases those tokens first. Unfortunately, blockchains by
design facilitate transaction reordering attacks: unconfirmed transactions
submitted by users are publicly visible in a ‘mempool’ and transactions can be
prioritized for confirmation by increasing their transaction fees.

Outside of financially hurting a victim, reordering attacks can seriously
affect the security of the blockchain consensus protocol especially in proof-
of-stake systems. It is reported that in 2022 alone more than 300 million
dollars were unfairly gained through reordering attacks (mev, 2023). With such
fortune at stake, it is feasible for an attacker to bribe block proposers to
act in an unethical way or even deviate from protocol (Chitra and Kulkarni,
2022).

Preventing transaction reordering attacks has therefore become an active area
of research with several mitigation techniques proposed so far (Yang et al.,
2022). In practice, Ethereum has favored an approach where transaction order
is determined by (trusted) third-party entities called builders. A builder
collects transactions from end-users, orders them within a block and sends the
block to a proposer for inclusion within the blockchain. Separating out the
functionalities of ordering transactions in a block (building) and publishing
a block (proposing) protects block proposers from being influenced to
rearrange transactions. However, reordering attacks still very much happen at
the builder level. We note that not all builders practice or tolerate
reordering attacks, but a vast majority of them do.

In our work we present Masquerade, a simple and lightweight solution to
preventing transaction reordering in blockchains. The key idea in Masquerade
is the use of a token-number system (as at a takeout restaurant or the
drivers’ license agency) for deciding transaction ordering. In Masquerade, a
user first purchases a token with an assigned token number for a refundable
fee. Subsequently the user can use this token to make a transaction.
Transactions are ordered in the block in an increasing order of the token
numbers of tokens associated with transactions. Once a token is used with a
transaction, the funds paid for purchasing the token are returned to the user.

The key intuition for why Masquerade works is that at the time of a token
purchase, an attacker has no way of knowing what the purchased token will be
used for in the future. An attacker is therefore forced to purchase as many
tokens as possible, which places a significant financial stress on the
attacker. Under a formal model of the system, if the total funds available to
an attacker is a fraction $\sigma<1$ of the total funds available to honest
users, we show that the fraction of transactions that can be front run is at
most $\sigma$. Moreover, Masquerade guarantees that attacker to user wealth
ratio diminishes over time making the fraction of transactions front run
asymptotically go to zero. Experiments on synthetic and real-world transaction
data support our theoretical observations. We also note that Masquerade is
robust to transaction reordering attacks occurring on token-purchase
transactions submitted by users.

Deploying Masquerade in practice requires minimal changes to the consensus
protocol—blocks must be verified to ensure transactions are in increasing
order of their token numbers. Issuance and maintenance of tokens can be easily
implemented as a smart contract. In contrast, existing proposals enforcing
some notion of a fair-ordering of transactions (Kelkar et al., 2020, 2021;
Zhang et al., 2020; Cachin et al., 2022), or a commit-then-reveal scheme
(Khalil et al., 2019; Bentov et al., 2019; Zhang et al., 2022; Malkhi and
Szalachowski, 2022) require either significant changes to the consensus
algorithm, rely on complex cryptographic primitives or a trusted party
(Heimbach and Wattenhofer, 2022b). Masquerade can also be implemented as an
opt-in system in which only users seeking protection against reordering
attacks participate. In summary, the contributions of this paper are:

  * •

We propose a simple, lightweight solution that uses a token-based ordering
mechanism for mitigating transaction reordering attacks in blockchains such as
Ethereum.

  * •

We rigorously show performance of Masquerade under a theoretical model.

  * •

We evaluate Masquerade experimentally using a variety of synthetic and real-
world data to corraborate our theoretical results.

##  2\. Background

###  2.1. Maximal Extractable Value (MEV)

With a push towards decentralization, there has been an increase in
decentralized finance (DeFi) protocols that are run by smart contracts with
individual users simply interacting with them. These are permissionless,
transparent and eliminate the need for a central authority. DeFi services such
as Uniswap(Adams et al., 2021), Compound(Yang et al., 2022),
MakerDAO(Brennecke et al., 2022) etc are based on open protocols and
Decentralized Applications(DApps) and aim to recreate traditional financial
systems and services without the need for a centralized authority. In DeFi
dapps, the order in which transactions are executed play a very important role
in profits gained by users of this system. Profits obtained by bad actors
through transaction reordering attacks is called as maximal extractable value
(MEV). MEV profits are in the millions of dollars today. As a result, front
running victim transactions is a very lucrative option.

In centralized finance markets (CeFi) such as Binance(noa, 2023a),
CoinBase(Kazerani et al., 2017), Kraken (Pichl and Kaizoji, 2017) etc,
transaction ordering is strictly monitored by an authority, and adversaries
are punished. A major problem with these CeFi protocols is that the users are
required to relinquish control of their assets to the service provider and
trust the operator while transacting. A canonical example of a DeFi app is a
decentralized exchange (DEX), which is a platforms that allows trading through
smart contracts on the blockchain. DEX transactions are particularly
susceptible to front running attacks by adversaries, as there is a lack of any
regulatory body that can punish these malpractices. Further, clients who have
been manipulated by this exchange have no way of recovering their lost wealth.

An Automated Market Maker(AMM) is a smart contract used in DEXs to facilitate
the trading of digital assets without the need for traditional order books or
other intermediaries. These AMMs use some predetermined formulas to determine
the prices of assets based on their supply and demand within a liquidity pool.
AMMs were introduced as an alternative to traditional order book exchanges,
where buyers and sellers interact directly to set the prices of assets. An AMM
contains a liquidity pool of atleast two assets, where it allows users to
deposit an asset and withdraw the other based on the determined exchange
value. One of the most commonly used AMMs is the Constant Product Market
Maker(CPMM) algorithm. This algorithm is used in DEXs like Uniswap(Adams et
al., 2021) and PancakeSwap(noa, 2023c). In the CPMM algorithm, the product of
the quantities of two assets in a pool remains constant, which helps determine
the price when one asset is traded for another. Simply, if an exchange has $x$
and $y$ units of currency in their reserve, $xy=k$ denotes the price of the
asset using the exchange.

###  2.2. MEV Attacks

Currently, in blockchains such as Ethereum, adversaries frequently monitor the
mempool to search for a certain kind of MEV transactions which would yield
reward at the expense of increased cost to the user. We explain three major
attacks, benefits to the adversary, and the cost to the user below.

  1. (1)

Sandwich Attack: In this case, an attacker attempts to monitor mempool for
pending transactions trading large assets that may cause price fluctuations.
Let a user transaction be $\texttt{txn}_{u}$ that is exchanging currency
$C_{1}$ to $C_{2}$, denoted by $C_{1}\xrightarrow[]{}C_{2}$. An attacker $a$
then submits two transactions, say $\texttt{txn}_{a}$ and
$\texttt{txn}_{a}^{\prime}$, with the same transaction amount as the user $u$.
In $\texttt{txn}_{a}$, the attacker exchanges $C_{1}\xrightarrow{}C_{2}$, and
in $\texttt{txn}_{a}^{\prime}$ exchanges $C_{2}\xrightarrow[]{}C_{1}$. A
sandwich attack happens if $\texttt{txn}_{a}$, $\texttt{txn}_{u}$ and
$\texttt{txn}_{a}^{\prime}$ are included in the same block $\mathcal{B}$ and
in this order.

  2. (2)

Arbitrage MEV: An arbitrage occurs when users are trading assets across
different exchanges. Let a user transaction be $\texttt{txn}_{u}$ that is
trading $\alpha_{u}$ amount of currency $C_{1}$ with fiat money across two
different exchanges $E_{1}$ and $E_{2}$ with different exchange rates
$P_{C_{1},E_{1}}$ and $P_{C_{1},E_{2}}$, respectively. A successful arbitrage
occurs if price $\alpha_{u}P_{C_{1},E_{1}}+g_{u}<\alpha_{u}P_{C_{1},E_{2}}$,
for gas fees $g_{u}$. In this case, the attacker $a$ monitors the public
mempool for an arbitrage opportunity and attempts to front-run
$\texttt{txn}_{u}$ with $\texttt{txn}_{a}$ with $\alpha_{a}=\alpha_{u}$, gas
fee $g_{a}>g_{u}$, so that
$\alpha_{a}P_{C_{1},E_{1}}+g_{a}<\alpha_{a}P_{C_{1},E_{2}}$. In this case, the
arbitrage benefit to the user is diminished and the adversary gains from
front-running such a transaction.

  3. (3)

Liquidation MEV: A liquidation attack occurs on a loan taken out by a user.
Let a user borrow $\alpha_{C_{1}}$ units of currency $C_{1}$, for a price of
$\alpha_{C_{1}}C_{1}$. The user in exchange offers a collateral of units
$\alpha_{C_{2}}$ of currency $C_{2}$ for a price of
$\alpha_{C_{2}}C_{2}\geq\alpha_{C_{1}}C_{1}$. This attack occurs, when the
collateral $\alpha_{C_{2}}C_{2}$ no longer covers the value of the debt. Let
the exchange rate at the time of borrowing be $C_{2}=\beta_{r}C_{1}$. For the
loan to be healthy, $\beta>1$. Due to price fluctuations, it is possible that
$\frac{\alpha_{C_{2}}C_{2}}{\alpha_{C_{1}}C_{1}}<1$ which means that the loan
is now under-collateralized. At this time, the collateral is available to
users to purchase at a low rate. An adversary now frontruns the purchase of
the collateral $\alpha_{C_{2}}C_{2}$, and is able to accrue a profit on this
transaction by selling it later at a higher price.

###  2.3. MEV Mitigation: Status Quo

Ethereum uses a proposer-builder separation architecture for mitigating the
negative impacts of MEV on blockchain security (Heimbach et al., 2023). Under
this architecture, the process for the formation of a block is as follows.
Users submit transactions either by broadcasting publicly over the blockchain
network, or by sending privately to a third-party reputable entity called a
builder (Flashbots, BeaverBuild, Builder0x69, BloXroute etc.). Transactions
made include an appropriate amount of transaction fees depending on the
priority desired for the transaction. The builder collects transactions and
orders them to create a candidate block which it then advertises to the
proposer of that time slot. Builder strive to construct blocks with high
aggregate transaction fees, as a portion of the transactions fees goes to the
builder. Competing builders advertise blocks to the proposer. The proposes
chooses the block containing the most amount of fees for publication on the
blockchain.

##  3\. Model

We consider time is divided in to discrete rounds, with one block produced
during each round. Our model consists of two actors, a user and an adversary
as described in the following.

User: The user in our model represents collectively all honest users in the
system. The essence of our results does not change even if we explicitly
consider multiple users in the model. We assume the user is honest and follows
protocol. The user seeks to make MEV transactions without getting front run to
maximize its profits. We define an “MEV transaction” as a DeFi transaction
from which value can be extracted by the adversary through a reordering
attack. The user is interested in making at most one MEV transaction each
round. The profit gained by the user upon making a MEV transaction
successfully (i.e., without getting front run) and the profits lost when a
front running attack happens are discussed in §3.1 below. At the beginning of
the experiment, the user has a net wealth of $W_{u}[0]$.

Adversary: The adversary in our model is an entity that seeks to make profit
by attacking the user’s MEV transactions. We primarily consider front running
attacks in our work, though the results extend to back running and sandwich
attacks as well. During an MEV attack, the adversary gains precisely the value
lost by the user on the transaction. At the beginning of the experiment, we
assume the adversary has a net wealth of $W_{a}[0]$. We assume the total
wealth $W_{a}[0]$ of the adversary is lower than the total wealth of the user
$W[0]$ initially by a factor of $\sigma<1$. This is a reasonable assumption,
as the security of Proof-of-Stake consensus followed by Ethereum relies on
such an assumption as well. For any round $r$, we let $W_{u}[r],W_{a}[r]$
respectively denote the total wealth of the user and adversary respectively at
the beginning of round $r$. Note that since the user can make at most one MEV
transaction each round, the adversary can also front run at most one MEV
transaction each round. We do not consider regular (i.e., non-MEV)
transactions made by the user or the adversary in our model. The adversary has
complete knowledge of the internal state of the user at any time. Unless the
proposed consensus protocol prohibits it, the adversary can front run any
transaction submitted by the user during a round with its own transaction.

The blockchain network also contains builders, relays and validators, but for
our problem we do not consider them to be an essential part of the network
dynamics, and omit their roles. We define a transaction as
$\texttt{txn}_{u}[r]$ for a transaction made by a user at round $r$, and
$\texttt{txn}_{a}[r]$ for a transaction made by an adversary.

###  3.1. Rewards

We assume that the profit made by an honest user on an MEV transaction is
$\eta$, of which he loses $f\eta$ if an adversary manages to front run the
transaction. In practice, users can specify a slippage parameter to control
their MEV loss which relates to the $f$ in our model (Heimbach and
Wattenhofer, 2022a). Thus, the rewards to the user and the adversary,
respectively, $h_{u}[r],h_{a}[r]$ in round $r$ can be defined as follows:

(1) $\displaystyle h_{u}[r]$ $\displaystyle=\begin{cases}\eta-f\eta&\text{if
MEV transaction is front run}\\\ \eta&\text{otherwise},\end{cases}$ (2)
$\displaystyle h_{a}[r]$ $\displaystyle=\begin{cases}f\eta&\text{if MEV
transaction is front run}\\\ 0&\text{otherwise}.\end{cases}$

We ignore the costs incurred by gas fees to the user and the adversary. In
today’s Ethereum (referred to as “current protocol” in the paper), we assume a
user’s MEV transaction always get front run which leads to a profit of
$\eta-f\eta$ per round for the user. This is a reasonable assumption, as a
user today either issues its transaction publicly and gets attacked, or issues
its transaction privately to a builder by paying hefty fees. Either way the
value the user rightfully must gain in the transaction is lost in today’s
Ethereum. After $R$ rounds, the total wealth accumulated by the user and the
adversary in the current protocol from MEV transactions is given by:

(3) $\displaystyle W_{u}$ $\displaystyle=W_{u}[0]+\sum_{r=1}^{R}h_{u}[r]$ (4)
$\displaystyle=W_{u}[0]+(\eta-f\eta)R$ (5) $\displaystyle W_{a}$
$\displaystyle=W_{a}[0]+\sum_{r=1}^{R}h_{a}[r]$ (6)
$\displaystyle=W_{a}[0]+f\eta R$

Thus, we see that an honest user is losing out on atleast $f\eta R$ profits on
having made an MEV transaction every round for $R$ rounds. In the real world
scenario, they end up losing even more money when multiple MEV transactions
are part of a block.

###  3.2. Problem Statement

Our objective is to design a transaction ordering protocol that prevents MEV
attacks and maximizes the total wealth of the after $R$ rounds. Or,
equivalently, we would like to reduce the fraction of transactions that are
successfully attacked by the adversary. The solution space we explore must
obey the following constraints. First, we do not want to introduce any
significant modifications to the consensus protocol keeping in mind the
difficulties involved in implementation. Any solution we propose must be
implementable with just a few lines of code, either at the consensus or
execution layers. We also avoid use of computationally expensive cryptographic
algorithms due to their complexity of implementation. Finally, we would like
our method to be resistant to attacks without the usage of any trusted third
parties.

##  4\. Proposed Transaction Ordering Protocol

We introduce our transaction ordering protocol, called Masquerade, which is a
decentralized protocol with minimal changes to the current consensus protocol
and no reliance on external trusted parties. In our protocol, we modify a
percentage of transactions $\texttt{txn}_{u},\texttt{txn}_{a}$ to include a
new parameter called ”token number” with them. These transactions will then be
ordered strictly according to the token number accompanying the transaction.
As a result, even if the content of the MEV transaction is made aware to an
attacker, they are unable to frontrun it without the relevant token number
required to actually frontrun the transaction.

We add two new kinds of transactions called ”token purchase transaction” and
”tokenized transaction” that we will describe in more detail below:

###  4.1. Token Purchase Transaction

A token purchase transaction is simply a transaction that the user makes in
order to receive token number $T$ that can be used for future transactions. A
single token purchase transaction can be used to specify any number of tokens
desired, as long as sufficient funds are available for the token. A single
token purchase costs $y$ units. A token purchase transaction is considered
successful, if it has been included as a part of the main chain. A user, or
adversary cannot specify the token number they would like to purchase. Token
numbers are issued independently, by a token issuing algorithm. If a user uses
a valid token, to make a valid tokenized transaction, the token is considered
to be spent, and the cost of purchasing that particular token $y$ is refunded
back to the user. Each token can only be used once, but a token that has been
purchased once never expires, and can be used in the future.

###  4.2. Tokenized Transaction

A tokenized transaction for round $r$,
$\texttt{txn}_{u}[r],\texttt{txn}_{a}[r]$ is a transaction that is accompanied
by a valid token number $T_{u}[r],T_{a}[r]$ for the user and adversary
respectively. A valid token number is one, that has been confirmed and
included on the main chain in the previous rounds $r-1$. A user can only use
valid tokens to make a tokenized transaction. Tokenized transactions are
strictly ordered in ascending order, with transaction $\texttt{txn}_{u}[r]$
being executed earlier than $\texttt{txn}_{a}[r]$, if $T_{u}[r]<T_{a}[r]$.
Further, all tokenized transactions precede non-tokenized transactions.

The process of formation of the block now follows the following procedure:

  * •

At the beginning of the round, a user can take the following actions:

    * –

all users can make non-tokenized regular transactions or non-tokenized MEV
transactions.

    * –

users can make the desired token purchase requests.

    * –

users can use previously purchased tokens to make tokenized MEV transactions,
or tokenized regular transansactions.

  * •

All transactions are verified to ensure they are valid.

  * •

The validator for round $r$ then collects $N$ valid tokenized transactions,
and orders them based on token numbers. A tokenized transaction
$\texttt{txn}_{u}[r]$ is strictly ordered before $\texttt{txn}_{a}[r]$ if
$T_{u}[r]<T_{a}[r]$.

  * •

The validator also collects non-tokenized transactions and creates a block
based on the highest rewards that can be extracted.

  * •

Finally, at the end of the round, the validator updates the state of the
Blockchain and publishes the block.

It is important to note, here, that the token purchase transaction, like any
other transaction, has the ability to get attacked. An adversary is able to
frontrun an honest user’s token purchase transaction, to get a lower token
number than the user.

###  4.3. Rewards for the proposed protocol

During round $r$, there are only $l$ tokens available that can be purchased.
We assume a reasonable, fixed user policy $\pi_{u}$ and adversary policy
$\pi_{a}$. We would like to find the maximum possible reward that can be
achieved by the adversary in a fixed user policy scenario, which is strictly
less than what the adversary gains in the current scenario. Let the user and
adversary each purchase $\mathsf{X}_{u}[r],\mathsf{X}_{a}[r]$ number of tokens
respectively. As each token costs $y$ units, the total costs incurred by them
is $y\mathsf{X}_{u}[r],y\mathsf{X}_{a}[r]$ Let each block only allow $N$
tokenized transactions.

Let us define $\mathsf{M}_{u}[r]$ to be a function that defines whether an MEV
transaction is made by a user or not i.e

(7) $\mathsf{M}_{u}[r]=\begin{cases}1&\text{if MEV transaction is made}\\\
0&\text{otherwise}\end{cases}$

Similarly, we define $\mathsf{M}_{a}[r]$ to be a function that defines whether
an MEV transaction is attacked by an adversary or not i.e

(8) $\mathsf{M}_{a}[r]=\begin{cases}1&\text{if MEV transaction is attacked}\\\
0&\text{otherwise}\end{cases}$

Let us define $\mathsf{F}_{r}$ to be a function that defines whether an MEV
transaction made by the user is frontrun or not i.e

(9) $\mathsf{F}_{r}=\begin{cases}1&\text{if MEV transaction is frontrun}\\\
0&\text{otherwise}\end{cases}$

The rewards to the user and the adversary $h_{u}[r],h_{a}[r]$ in round $r$ can
be defined as follows:

(10) $h_{u}[r]=\begin{cases}-y\mathsf{X}_{u}[r]+\eta-f\eta+y&\text{if MEV
transaction is frontrun}\\\
-y\mathsf{X}_{u}[r]+\eta+y&\text{otherwise}\end{cases}$ (11)
$h_{a}[r]=\begin{cases}-y\mathsf{X}_{a}[r]+f\eta+y&\text{if MEV transaction is
frontrun}\\\ -y\mathsf{X}_{a}[r]&\text{otherwise}\end{cases}$

Now, both the user and adversary start with an initial wealth
$W_{u}[0],W_{a}[0]$. If, we assume that each block has only a single MEV
transaction, after $R$ rounds, the maximum wealth that can be accumulated by
both the user and the adversary from MEV transactions are:

$\displaystyle W_{u}$ $\displaystyle=W_{u}[0]+\max\sum_{r=1}^{R}h_{u}[r]$ (12)
$\displaystyle=W_{u}[0]+\max\sum_{r=1}^{R}\eta-f\eta\mathsf{F}_{r}+y\mathsf{M}_{u}[r]-y\mathsf{X}_{u}[r]$

$\displaystyle W_{a}$ $\displaystyle=W_{a}[0]+\max\sum_{r=1}^{R}h_{a}[r]$ (13)
$\displaystyle=W_{a}[0]+\max\sum_{r=1}^{R}(f\eta+y)\mathsf{F}_{r}-y\mathsf{X}_{a}[r]$

We now introduce a randomly chosen fixed user policy $\pi_{u}$, as shown in
Algorithm 1. At the end of each round, a user purchases a single token, which
depletes their wealth. When the threshold of this wealth is less than a small
threshold $\tau$, the user begins to spend their tokens. This ensures that
there is sufficient time for user to collect tokens to spend so that they are
not frontrun by adversary tokens. Finally, the user will always take the MEV
opportunity presented to them as long as they have an appropriate token. We
assume that an adversary can simply frontrun any non-tokenized transactions.
As a result, the user solely makes tokenized MEV transactions. Further, as the
user is not aware of any tokens that are held by the adversary, they always
use their lowest available token.

Algorithm 1 User Policy $\pi_{u}$

1:Inputs: $W_{u}[r],y,\tau$, $\tilde{H}_{u}[r]\subseteq\tilde{H}[r]$

2:if $W_{u}[r]>y$ then

3: $\mathsf{X}_{u}[r]=1$

4:end if

5:if $W_{u}[r]\leq\tau$ then

6: $M_{u}[r]=1$

7: $T_{u}[r]=\tilde{H}_{u}[r]$

8:else

9: $M_{u}[r]=0$

10: $T_{u}[r]=\infty$

11:end if

The adversary policy $\pi_{a}$ on the other hand, is more powerful. As a worst
case scenario, we assume that the adversary has full control over the token
number assignment, and may reorder the token purchase transactions as they
please. Thus, the adversary is aware of all tokens that the user has. We also
allow the adversary to monitor user transactions, and the ability to frontrun
these transactions. Since the user only makes tokenized MEV transactions, the
adversary is able to frontrun these transactions, if they have tokens that are
smaller in number than user tokens. This policy is detailed in Algorithm 2.
The adversary can choose any policy, however we show in Section 5, that this
indeed is the best policy that can be taken.

Algorithm 2 Adversary Policy $\pi_{a}$

1:Inputs: $y,W_{a}[r],T_{u}[r],M_{u}[r],\tilde{H}_{a}[r]\subseteq\tilde{H}[r]$

2:$\mathsf{X}_{a}[r]=\lfloor\frac{W_{a}[r]}{y}\rfloor$

3:if $M_{u}[r]=1$ then

4: if $T_{u}[r]<\infty$ then

5: $T_{a}[r]=\max T\in\tilde{H}_{a}[r]$ s.t. $T<T_{u}[r]$

6: else

7: $T_{a}[r]=\infty$

8: end if

9: $M_{a}[r]=0$

10: $T_{a}[r]=\infty$

11:end if

##  5\. Analysis

To ease analysis, we divide time in to epochs as defined in the following. The
first epoch begins at round $r=0$ and ends when the user has completed the
initial token purchasing as in Algorithm 1. Equivalently, the first epoch
lasts until the user’s wealth $W_{u}[r]$ drops below threshold $\tau$. Each
subsequent epoch begins immediately after the epoch prior to it ends. An epoch
ends when the following two conditions are satisfied:

  1. (1)

the user has utilized all of the tokens purchased in the previous epoch;

  2. (2)

the available wealth $W_{u}[r]$ of the user drops below $\tau$.

The above conditions lead to a well-defined notion of an epoch as the user
always utilizes the earliest available token for a MEV transaction. Tokens in
one epoch, therefore, are completely utilized before tokens in the next epoch
are utilized. We also define a terminal epoch in which parties utilize tokens
from the previous epoch, but make no new token purchases during the epoch. The
game ends after the terminal epoch. We assume the game lasts for $k>0$ epochs.
Restricting the game to $k$ epochs captures the intuition that in practice, a
player is interested in optimizing her rewards over a fixed time horizon,
e.g., the lifespan of the player, the next five years etc. Note that our
definition of an epoch is tied to the user’s behavior described in Algorithm
1. The definition is independent of the adversary’s behavior.

Let $\tilde{H}[e]$ be the set of tokens purchased by either the user or the
adversary during epoch $e$. Further, let
$\tilde{H}_{u}[e]\subseteq\tilde{H}[e]$ and
$\tilde{H}_{a}[e]\subseteq\tilde{H}[e]$ be the tokens purchased by the user
and adversary, respectively, during $e$. $\tilde{W}_{a}[e]$ and
$\tilde{W}_{u}[e]$ denote, respectively, the total wealth of the adversary and
user at the end of epoch $e$. The total wealth of a party includes the wealth
available for spending and the funds locked up in the form of tokens. We call
a policy $\pi_{a}$ followed by the adversary as balanced if the following
holds true.

Figure 1. Illustration of token purchases with time.

###### Property 1 (Balanced policy).

An adversary policy $\pi_{a}$ is balanced if for each non-terminal epoch $e$,
there exists an injective mapping
$m_{e}:\tilde{H}_{a}[e]\rightarrow\tilde{H}_{u}[e]$ such that $m_{e}(T)>T$ for
all $T\in\tilde{H}_{a}[e]$ and
$|\tilde{H}_{a}[e]|=\lfloor\tilde{W}_{a}[e]/y\rfloor$.

With a balanced policy, an adversary can successfully utilize each purchased
token to front run some victim transaction. The adversary also maximally
utilizes its wealth to purchase tokens. We call a specific epoch $e$ as
balanced if there exists an injective mapping
$m_{e}:\tilde{H}_{a}[e]\rightarrow\tilde{H}_{u}[e]$ such that $m_{e}(T)>T$ for
all $T\in\tilde{H}_{a}[e]$ and
$|\tilde{H}_{a}[e]|=\lfloor\tilde{W}_{a}[e]/y\rfloor$. We now show that the
adversary policy $\pi_{a}$ described in Algorithm 2 is balanced.

###### Theorem 1.

For $W_{a}[0]<\sigma W_{u}[0]$ where $0<\sigma<\frac{1}{2}$ is a security
parameter, $f<\frac{1-\sigma-\epsilon}{1+\sigma}$, and
$W_{a}[0]>\frac{y^{2}}{\eta\epsilon}$ where
$\epsilon<(yf+f^{2}\eta)/(\eta(1-f))$ is a parameter and $\tau<\epsilon
W_{u}[0]$ the adversary’s policy $\pi_{a}$ as described in Algorithm 2 is
balanced.

###### Proof.

The proof is by induction. During the initial epoch, the adversary purchases
$\lfloor W_{a}[0]/y\rfloor$ tokens first following which the user purchases
$\lceil(W_{u}[0]-\tau)/y\rceil$ tokens as per the adversary policy $\pi_{a}$
and user policy $\pi_{u}$ in Algorithm 1. By assumptions in Theorem,
$W_{a}[0]<\sigma W_{u}[0]<\frac{W_{u}[0]}{2}$ and therefore $\lfloor
W_{a}[0]/y\rfloor<\lceil(W_{u}[0]-\tau)/y\rceil$. The injective mapping
$m_{0}:\tilde{H}_{a}[0]\rightarrow\tilde{H}_{u}[0]$ can simply be
$m_{0}(i)=\lfloor W_{a}[0]/y\rfloor+i$ for all $1\leq i\leq\lfloor
W_{a}[0]/y\rfloor$. The total wealth of the user $\tilde{W}_{u}[0]$ and
adversary $\tilde{W}_{a}[0]$ at the end of the initial epoch are still
$W_{u}[0]$ and $W_{a}[0]$ respectively.

Now, consider an epoch $e$ that is not the initial or the terminal epoch.
Supposing the previous epoch $e-1$ is balanced, i.e., satisfies the property
that there exists an injective function
$m_{e-1}:\tilde{H}_{a}[e-1]\rightarrow\tilde{H}_{u}[e-1]$ with $m_{e-1}(T)>T$
for all $T\in\tilde{H}_{a}[e-1]$. Also suppose the mapping $m_{e-1}$ is such
that there are at least $c\lceil\tilde{W}_{a}[e-1]/y\rceil$ user tokens at the
end of epoch $e-1$ without a preimage in $m_{e-1}$ where
$c>(f+\epsilon)/(1-f-\epsilon)$, i.e.,

(14)
$\displaystyle|\\{T^{\prime}\in\tilde{H}_{u}[e-1]:T^{\prime}>\max_{T:T\in\tilde{W}_{a}[e-1]}m_{e-1}(T)\\}|>c\left\lceil\frac{\tilde{W}_{a}[e-1]}{y}\right\rceil.$

Equation (14) implies there exist at least $c\lceil\tilde{W}_{a}[e-1]/y\rceil$
user transactions that are not front run in the end of epoch $e$. Further,
suppose that the total wealth of the parties are such that
$\tilde{W}_{a}[e-1]<\sigma\tilde{W}_{u}[e-1]$. We will show that there exists
an injective function $m_{e}:\tilde{H}_{a}[e]\rightarrow\tilde{H}_{u}[e]$ with
$m_{e}(T)>T$ for all $T\in\tilde{H}_{a}[e]$ and
$\tilde{W}_{a}[e]<\sigma\tilde{W}_{u}[e]$.

There are $\lfloor\tilde{W}_{a}[e-1]/y\rfloor$ tokens purchased by the
adversary during epoch $e-1$. Since epoch $e-1$ is balanced, during epoch $e$
the adversary can use each of its tokens in $e-1$ to successfully front run
transactions. After each successful front running attack, the adversary
replaces its used token in epoch $e-1$ by purchasing a new token in epoch $e$.
We call such a token the adversary purchases as a replacement token.
Additionally, the adversary can use the profits gained from front running to
purchase tokens whenever the adversary’s balance exceeds $y$. We call such a
token as a bonus token. Note that after each transaction the user submits, the
user also purchases a replacement token and possibly bonus tokens. We define
replacement token and bonus token for the user analogous to those for the
adversary. Per our model, the replacement and bonus tokens of the adversary
are purchased before the replacement and bonus tokens of the user after each
front running attack.

To construct an injective mapping for epoch $e$, first note that the
replacement token purchased by the adversary after each successful front run
can be mapped to the replacement token purchased by the user after the front
run. Thus, $\lfloor\tilde{W}_{a}[e-1]/y\rfloor$ of the adversary’s tokens can
be mapped to higher tokens in epoch $e$. However, in addition to replacement
tokens the adversary also purchases $\lfloor\lfloor\tilde{W}_{a}[e-1]/y\rfloor
f\eta/y\rfloor$ bonus tokens in epoch $e$, which need to be mapped. For this,
consider round $r^{*}$ when the last front run attack is performed by the
adversary in epoch $e$. We observe that, by policy $\pi_{a}$ all of the
adversary’s bonus tokens are purchased by round $r^{*}+1$ in epoch $e$ (Figure
1). Transactions submitted by the user after round $r^{*}$ are not attacked.
By assumption, at least $\lceil\tilde{W}_{a}[e-1]/y\rceil$ transactions are
submitted by the user after round $r^{*}+1$. Each of those transactions
generate a reward of $\eta$ for the user. Therefore, the user is able to
purchase at least $\lfloor\lceil\tilde{W}_{a}[e-1]/y\rceil(y+\eta)/y\rfloor$
tokens at the end of epoch $e$. To complete our mapping, we map the
$\lfloor\lfloor\tilde{W}_{a}[e-1]/y\rfloor f\eta/y\rfloor$ bonus tokens of the
adversary to the first $\lfloor\lfloor\tilde{W}_{a}[e-1]/y\rfloor
f\eta/y\rfloor$ user tokens purchased after round $r^{*}$. This is possible
since

$\displaystyle\epsilon$
$\displaystyle<\frac{yf+f^{2}\eta}{\eta(1-f)}\Rightarrow\frac{\eta\epsilon+f\eta}{y+\eta}<\frac{f}{1-f}\Rightarrow\frac{\frac{y^{2}}{\tilde{W}_{a}[e-1]}+f\eta}{y+\eta}<\frac{f}{1-f}$
$\displaystyle\Rightarrow\frac{\frac{y^{2}}{\tilde{W}_{a}[e-1]}+f\eta}{y+\eta}$
$\displaystyle<c\Rightarrow y^{2}<\tilde{W}_{a}[e-1](cy+c\eta-f\eta)$
$\displaystyle\Rightarrow\tilde{W}_{a}[e-1]f\eta$
$\displaystyle<c\tilde{W}_{a}[e-1](y+\eta)-y^{2}\Rightarrow\frac{\tilde{W}_{a}[e-1]f\eta}{y^{2}}<\frac{c\tilde{W}_{a}[e-1](y+\eta)}{y^{2}}-1$
(15) $\displaystyle\Rightarrow\lfloor\lfloor\tilde{W}_{a}[e-1]/y\rfloor
f\eta/y\rfloor$ $\displaystyle<\lfloor
c\lceil\tilde{W}_{a}[e-1]/y\rceil(y+\eta)/y\rfloor.$

Thus, we have showed the existence of an injective mapping
$m_{e}:\tilde{H}_{a}[e]\rightarrow\tilde{H}_{u}[e]$ with $m_{e}(T)>T$ for all
$T\in\tilde{H}_{a}[e]$.

The number of user tokens at the end of epoch $e$ who which a preimage on
$m_{e}$ does not exist is at least
$\lfloor\lceil\tilde{W}_{a}[e-1]/y\rceil(y+\eta)/y\rfloor-\lfloor\lfloor\tilde{W}_{a}[e-1]/y\rfloor
f\eta/y\rfloor$. In the following we show that this quantity is at least
$\lceil\tilde{W}_{a}[e]/y\rceil$. We have

$\displaystyle\frac{f+\epsilon}{1-f-\epsilon}$ $\displaystyle<c$
$\displaystyle\Rightarrow\frac{f+\frac{y^{2}}{\tilde{\eta
W_{a}[e-1]}}}{1-f-\frac{y^{2}}{\eta\tilde{W}_{a}[e-1]}}$ $\displaystyle<c$
$\displaystyle\Rightarrow f\eta+\frac{y^{2}}{\tilde{W_{a}[e-1]}}$
$\displaystyle<c\eta(1-f)-\frac{cy^{2}}{\tilde{W}_{a}[e-1]}$
$\displaystyle\Rightarrow cy+cf\eta+\frac{cy^{2}}{\tilde{W}_{a}[e-1]}$
$\displaystyle<cy+c\eta-\frac{y^{2}}{\tilde{W_{a}[e-1]}}-f\eta$
$\displaystyle\Rightarrow
c\frac{\tilde{W}_{a}[e-1]}{y}\left(1+\frac{f\eta}{y}\right)+c$
$\displaystyle<\frac{c\tilde{W}_{a}[e-1](y+\eta)}{y^{2}}-1-\frac{\tilde{W}_{a}[e-1]f\eta}{y^{2}}$
$\displaystyle\Rightarrow c\frac{\tilde{W}_{a}[e]}{y}+c$
$\displaystyle<\frac{c\tilde{W}_{a}[e-1](y+\eta)}{y^{2}}-1-\frac{\tilde{W}_{a}[e-1]f\eta}{y^{2}}$
$\displaystyle\Rightarrow c\tilde{W}_{a}[e]/y+c$
$\displaystyle<c\lceil\tilde{W}_{a}[e-1]/y\rceil(y+\eta)/y-1-\lfloor\tilde{W}_{a}[e-1]/y\rfloor
f\eta/y$ (16) $\displaystyle\Rightarrow c\lceil\tilde{W}_{a}[e]/y\rceil$
$\displaystyle<\lfloor
c\lceil\tilde{W}_{a}[e-1]/y\rceil(y+\eta)/y\rfloor-\lfloor\lfloor\tilde{W}_{a}[e-1]/y\rfloor
f\eta/y\rfloor$

It only remains to show that $\tilde{W}_{a}[e]<\sigma\tilde{W}_{u}[e]$. We
have,

$\displaystyle\frac{\tilde{W}_{a}[e-1]+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor
f\eta}{\tilde{W}_{u}[e-1]+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor(1-f)\eta+\left(\left\lceil\frac{\tilde{W}_{u}[e-1]-\tau}{y}\right\rceil-\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor\right)\eta}<\sigma$
$\displaystyle\Leftarrow\frac{\tilde{W}_{a}[e-1]+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor
f\eta}{\tilde{W}_{u}[e-1]+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor(1-f)\eta+\left(\left\lceil\frac{\tilde{W}_{u}[e-1]-\tau}{y}\right\rceil-\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor\right)\eta}<\frac{\tilde{W}_{a}[e-1]}{\tilde{W}_{u}[e-1]}$
$\displaystyle\Leftarrow\frac{\tilde{W}_{a}[e-1]+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor
f\eta}{\tilde{W}_{a}[e-1]}<\frac{\tilde{W}_{u}[e-1]+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor(1-f)\eta+\left(\left\lceil\frac{\tilde{W}_{u}[e-1]-\tau}{y}\right\rceil-\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor\right)\eta}{\tilde{W}_{u}[e-1]}$
$\displaystyle\Leftarrow\frac{\tilde{W}_{a}[e-1]+\frac{\tilde{W}_{a}[e-1]}{y}f\eta}{\tilde{W}_{a}[e-1]}<\frac{\tilde{W}_{u}[e-1]+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor(1-f)\eta+\left(\frac{\tilde{W}_{u}[e-1]-\tau}{y}-\frac{\tilde{W}_{a}[e-1]}{y}\right)\eta}{\tilde{W}_{u}[e-1]}$
$\displaystyle\Leftarrow
1+\frac{f\eta}{y}<1+\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor\frac{(1-f)\eta}{\tilde{W}_{u}[e-1]}+\frac{1-\frac{\tau}{\tilde{W}_{u}[e-1]}}{y}\eta-\frac{\tilde{W}_{a}[e-1]}{\tilde{W}_{u}[e-1]y}\eta$
$\displaystyle\Leftarrow\frac{f\eta}{y}+\frac{\sigma\eta}{y}<\left\lfloor\frac{\tilde{W}_{a}[e-1]}{y}\right\rfloor\frac{(1-f)\eta}{\tilde{W}_{u}[e-1]}+\frac{1-\frac{\tau}{\tilde{W}_{u}[e-1]}}{y}\eta$
$\displaystyle\Leftarrow\frac{f\eta}{y}+\frac{\sigma\eta}{y}<\left(\frac{\tilde{W}_{a}[e-1]}{y}-1\right)\frac{(1-f)\eta}{\tilde{W}_{u}[e-1]}+\frac{1-\frac{\tau}{\tilde{W}_{u}[e-1]}}{y}\eta$
$\displaystyle\Leftarrow
f+\sigma<\frac{(\tilde{W}_{a}[e-1]-y)(1-f)}{\tilde{W}_{u}[e-1]}+1-\frac{\tau}{\tilde{W}_{u}[e-1]}$
$\displaystyle\Leftarrow
f\left(1+\frac{\tilde{W}_{a}[e-1]-y}{\tilde{W}_{u}[e-1]}\right)<\frac{\tilde{W}_{a}[e-1]-y}{\tilde{W}_{u}[e-1]}-\sigma+1-\frac{\tau}{\tilde{W}_{u}[e-1]}$
$\displaystyle\Leftarrow
f\left(1+\sigma-\frac{y}{\tilde{W}_{u}[e-1]}\right)<\frac{\tilde{W}_{a}[e-1]-y}{\tilde{W}_{u}[e-1]}-\sigma+1-\frac{\tau}{\tilde{W}_{u}[e-1]}$
$\displaystyle\Leftarrow
f\left(1+\sigma-\frac{y}{\tilde{W}_{u}[e-1]}\right)<-\sigma+1-\frac{\tau}{\tilde{W}_{u}[e-1]}$
$\displaystyle\Leftarrow
f<\frac{1-\sigma-\frac{\tau}{\tilde{W}_{u}[e-1]}}{1+\sigma-\frac{y}{\tilde{W}_{u}[e-1]}}$
(17) $\displaystyle\Leftarrow f<\frac{1-\sigma-\epsilon}{1+\sigma}$

where we have used $\tilde{W}_{a}[e-1]>y^{2}/(\eta\epsilon)>y$ and
$\tau<\epsilon\tilde{W}_{u}[e-1]$.

The proof follows by induction. ∎

###### Lemma 1.

The total wealth of an adversary, following $\pi_{a}$, after $k$ epochs is
upper bounded as

(18) $\displaystyle\tilde{W}_{a}[k]\leq
W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{k}.$

###### Proof.

The total wealth of the adversary at the end of the initial epoch,
$\tilde{W}_{a}[0]$, is $W_{a}[0]$. Under policy $\pi_{a}$, the adversary is
able to front run $\lfloor\tilde{W}_{a}[0]/y\rfloor$ many user transactions in
the first epoch. Therefore, the total wealth of the adversary at the end of
the first epoch is (under what assumptions?)

(19)
$\displaystyle\tilde{W}_{a}[1]=W_{a}[0]+\left\lfloor\frac{W_{a}[0]}{y}\right\rfloor
f\eta\leq W_{a}[0]\left(1+\frac{f\eta}{y}\right).$

From Equation (19), the total wealth of the adversary at the end of the second
epoch is at most

(20) $\displaystyle\tilde{W}_{a}[2]\leq
W_{a}[0]\left(1+\frac{f\eta}{y}\right)+\left\lfloor\frac{W_{a}[0]\left(1+\frac{f\eta}{y}\right)}{y}\right\rfloor
f\eta\leq W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{2}.$

Continuing this way, the total wealth of the adversary at the of the $k$-th
epoch is at most

(21) $\displaystyle\tilde{W}_{a}[k]\leq
W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{k}.$

∎

###### Lemma 2.

The total wealth of the user at the end of $k$ epochs is lower bounded as

(22) $\displaystyle\tilde{W}_{u}[k]\geq
W_{u}[0]\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{k}-\frac{\tau\eta}{y}\left(\frac{\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{k}-1}{\left(\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)}\right).$

###### Proof.

Next, the total wealth of the user at the end of the initial epoch is
$W_{u}[0]$. During the first epoch, the user makes
$\left\lceil\frac{W_{u}[0]-\tau}{y}\right\rceil$ transactions bringing
$\left\lceil\frac{W_{u}[0]-\tau}{y}\right\rceil\eta$ additional value in to
the system. From Equation (19), the total wealth of the user at the end of the
first epoch is

$\displaystyle\tilde{W}_{u}[1]$ $\displaystyle\geq
W_{u}[0]+W_{a}[0]+\left\lceil\frac{W_{u}[0]-\tau}{y}\right\rceil\eta-
W_{a}[0]\left(1+\frac{f\eta}{y}\right)$ $\displaystyle\geq
W_{u}[0]+W_{a}[0]+\left(\frac{W_{u}[0]-\tau}{y}\right)\eta-
W_{a}[0]\left(1+\frac{f\eta}{y}\right)$
$\displaystyle=W_{u}[0]\left(1+\frac{\eta}{y}\right)-W_{a}[0]\frac{f\eta}{y}-\frac{\tau\eta}{y}$
$\displaystyle\geq
W_{u}[0]\left(1+\frac{\eta}{y}\right)-W_{u}[0]\sigma\frac{f\eta}{y}-\frac{\tau\eta}{y}$
(23) $\displaystyle=W_{u}[0]\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)-\frac{\tau\eta}{y}.$

Similarly, the total wealth of the user at the end of the second epoch is

$\displaystyle\tilde{W}_{u}[2]$
$\displaystyle\geq\tilde{W}_{u}[1]+\tilde{W}_{a}[1]+\left\lceil\frac{\tilde{W}_{u}[1]-\tau}{y}\right\rceil\eta-\tilde{W}_{a}[1]\left(1+\frac{f\eta}{y}\right)$
$\displaystyle\geq\tilde{W}_{u}[1]\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)-\frac{\tau\eta}{y}$ (24) $\displaystyle\geq
W_{u}[0]\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{2}-\frac{\tau\eta}{y}\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}+1\right).$

Repeating the above for $k$ times, we have

(25) $\displaystyle\tilde{W}_{u}[k]\geq
W_{u}[0]\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{k}-\frac{\tau\eta}{y}\left(\frac{\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{k}-1}{\left(\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)}\right).$

∎

###### Theorem 3.

Over epochs, the percentage of user transactions front run in each epoch goes
to zero.

###### Proof.

The number of user transactions front run during epoch $e$ is
$\lfloor\tilde{W}_{a}[e-1]/y\rfloor$. The total number of transactions made by
the user during epoch $e$ is $\lceil(\tilde{W}_{u}[e]-\tau)/y\rceil$. Since
each of the adversary’s tokens can be used to front run a transaction, the
fraction of transactions that are front run during the epoch is given by

(26)
$\displaystyle\frac{\lfloor\tilde{W}_{a}[e-1]/y\rfloor}{\lceil(\tilde{W}_{u}[e-1]-\tau)/y\rceil}\leq\frac{\tilde{W}_{a}[e-1]/y}{(\tilde{W}_{u}[e-1]-\tau)/y}=\frac{\tilde{W}_{a}[e-1]}{(\tilde{W}_{u}[e-1]-\tau)}.$

From Lemma 1 and 2 we have the percentage of front run transactions as at most

(27)
$\displaystyle\frac{W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{e-1}}{W_{u}[0]\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{e-1}-\frac{\tau\eta}{y}\left(\frac{\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{e-1}-1}{\left(\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)}\right)-\tau}.$

Taking limit of Equation (27) as $e\rightarrow\infty$, we have

$\displaystyle\lim_{e\rightarrow\infty}\frac{W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{e-1}}{W_{u}[0]\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{e-1}-\frac{\tau\eta}{y}\left(\frac{\left(1+\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)^{e-1}-1}{\left(\frac{\eta}{y}-\frac{\sigma
f\eta}{y}\right)}\right)-\tau}$ $\displaystyle=$
$\displaystyle\lim_{e\rightarrow\infty}\frac{W_{a}[0]}{W_{u}[0]\left(\frac{y+\eta-\sigma
f\eta}{y+f\eta}\right)^{e-1}-\frac{\tau}{1-\sigma
f}\left(\left(\frac{y+\eta-\sigma
f\eta}{y+f\eta}\right)^{e-1}-\frac{y^{e-1}}{(y+f\eta)^{e-1}}\right)-\frac{\tau
y^{e-1}}{(y+f\eta)^{e-1}}}$ (28) $\displaystyle=$
$\displaystyle\lim_{e\rightarrow\infty}\frac{W_{a}[0]}{\left(W_{u}[0]-\frac{\tau}{1-\sigma
f}\right)\left(\frac{y+\eta-\sigma
f\eta}{y+f\eta}\right)^{e-1}+\frac{\tau}{1-\sigma
f}\frac{y^{e-1}}{(y+f\eta)^{e-1}}-\frac{\tau y^{e-1}}{(y+f\eta)^{e-1}}}=0,$

since $y+\eta-\sigma f\eta>y+f\eta\iff f<1/(1+\sigma)$ which is true, and
$W_{u}[0]>\tau/(1-\sigma f)$. ∎

###### Theorem 4.

The total wealth earned by the adversary after $k$ epochs under policy
$\pi_{a}$ is at most a factor $\frac{y}{y-\eta\epsilon}$ away from the total
reward under any optimal policy.

(Proof in Appendix A)

##  6\. Experiments

We perform extensive experiments in order to show the results of the tokenized
transaction protocol under different conditions. The experiments are performed
by fixing user policy as described in Algorithm 1 and intelligent adversary
policy, as per Algorithm 2. We run the experiment for 10000 rounds and use the
following values of $f=0.8,\eta=100$ for our simulations. We assume that only
a single MEV transaction is included in the block. The user starts with an
initial wealth of $w_{\texttt{USER}}=1000\$$ and the adversary starts with
$\frac{w_{\texttt{USER}}}{2}$. $y=80$ is our chosen token cost.

###  6.1. Transaction Models

We compare the results of our experiment, to the current status-quo, that
contains transactions that are being ordered by a relay such as flashbots, and
provided to a validator. Here, $f=1$, since the transactions are always
attacked by the adversary. We also compare our results to an ideal scenario,
where no MEV transaction is attacked. We use the final wealth of the user as
an indicator to determine the long term feasibility of our policy. We also
consider the percentage of transactions that are frontrun by the adversary, in
order to track the mitigation of the MEVs from our method. We consider the
wealth of all parties in the system based on the following model
configurations:

  * •

Constant $\eta$: This state is when each block only has a single MEV
transaction, and the user and adversary gain a constant, deterministic reward
$\eta$ for making this transaction. If an adversary attacks the transaction,
they earn a constant reward of $f\eta$, while the user earns $\eta-f\eta$.

  * •

Stochastic $\eta$: This state is when each block has a single MEV transaction,
but the user and adversary gain a reward that is stochastic.

  * •

Fatal frontrunning: While making MEV transactions, there are some attacks that
cannot be blocked if they are frontrun, this is called fatal frontrunning. In
this case, we include Type 1 and Type 2 transactions, where Type 1 are those
transactions that can be protected (such as swaps), and Type 2 are those that
cannot (such as arbitrage attacks and liquidation).

  * •

Real world $\eta$: In this case, we consider real values of MEV profits that
have been extracted from the Ethereum blockchain.

###  6.2. Tokenization on constant $\eta$

In this case, we consider the wealth gained by the user and the adversary
based on constant $\eta=100$, as shown in Figure 2. We see in Figure 2, that
the total user wealth, while using Masquerade is comparable to the ideal
scenario, one in which the adversary does not exist. The status-quo represents
the current protocol, where all MEV transactions are frontrun by the
adversary. We see, that on average, only 30% of transactions are attacked,
which is a significant improvement, compared to all transactions being
attacked by adversary. We see, that when the user waits for a certain period
of time, they are able to beat the adversary and protect their transaction.

Figure 2. (a) Shows the percentage of transactions successfully attacked by the adversary every 1000 rounds. (b) The accumulation of the wealth of users and the adversaries when using Masquerade (our method) v/s the current status quo. Method | Wealth of User | Wealth of Adversary | % Frontrun | % Backrun
---|---|---|---|---
| Initial | Final | Initial | Final |  |
Status Quo | 1000 | 103840.0 | 500 | 411560.0 | 100 | 100
Token MEV | 1000 | 390240.0 | 500 | 125160.0 | 29.81 | 30.90
Ideal case | 1000 | 515400.0 | 0 | 0 | 0 | 0
Table 1. Improvements in transaction unstealibility using tokens

###  6.3. Tokenization on stochastic $\eta$

In this case, we consider the wealth gained by the user and the adversary for
a stochastic $\eta$ based on samples drawn from a Gaussian distribution, as
shown in Figure 3. We also consider a heavy tailed Cauchy distribution as
shown in Figure 3. This is a more interesting case, as the value earned by
stealing the transaction is vastly different. The adversary now, no longer can
predict what value each MEV transaction that can be potentially made in the
future holds. They are only aware of current token request transactions, and
tokenized MEV transactions. Now, the adversary has to carefully decide if they
would like to use their best token to attack the current tokenized MEV
transaction, or wait in case a better prospect in the future shows up. If the
adversary chooses not to attack, the user benefits directly. If the adversary
attacks, they may lose out on a future transaction. To capture this, we
consider simple modifications to Algorithm 1 where the user decides to use
their lowest token if the value of $\eta>100$, and second lowest token
otherwise. Similarly, in Algorithm 2, the adversary decides whether to use
their best token in the current round, or the next.

Figure 3. The user and adversary wealths for stochastic values of eta, drawn
from Gaussian and Cauchy distributions

Here too, we see that our algorithm performs quite well, improving the user’s
wealth compared to current status quo. We also see that the adversary is
unable to attack all transactions, and even misses out on crucial, high value
MEVs. The challenge for the adversary here, lies in guessing the most
profitable transactions, and being able to attack them successfully. If the
adversary waits for too long in a phase without using tokens, then the
adversary misses out on purchasing early tokens in the next phase. The user in
the next phase can generally exploit this and use later tokens for low value
transactions and early tokens for high value transactions. We can consider
several other efficient user policies in this case.

###  6.4. Fatal frontrunning attacks

In a fatal frontrunning attack, the attacker’s transaction executes while the
user’s transaction fails. This happens mostly in case of arbitrages, or loan
liquidations. If the user discovers an arbitrage opportunity and issues a
transaction, the adversary can observe the user’s transaction, duplicate it,
and issue its own transaction with a higher gas fee. In this case, the
adversary’s transaction executes, while the user receives no profit. No matter
what slippage the user specifies, the adversary has gained the full profit.
This leads us to two types of transactions, the first kind, or type 1
transactions, which involve exchanges that can be controlled with $f,\eta$,
and type 2 transactions, that are fatal, such as liquidation attacks and
arbitrage attacks. Creating an MEV transaction is a computationally expensive
operation for the user. The more compute the user can afford, the higher value
MEV transactions they can find. Thus, here, if the user sees that they are not
getting adequate rewards for the compute spent, the user would try to find
computationally cheaper MEV transactions, which for our experiments is
equivalent to low $\eta$ transactions. Thus, for type 2 transactions, the user
only engages with small $\eta$.

We ran our experiment on attacks that include fatal frontrunning attacks, and
we see that in such cases, we are able to only prevent a very small percentage
of these attacks, however even so, the total wealth obtained by the user
remains better than compared to the status quo. For fatal frontrunning attacks
that happened about 50% of the time, users get successfully attacked 70% of
the time. This number decreased when we slightly modified Algorithm 1. In this
case, the user only engaged with $\eta<100$ for type 2 transactions, and thus,
the percentage of frontruns decreased significantly. In Figure 4, we include
fatal frontrunning attacks both 50% and 30% of the time, and observe that
users are able to increase their wealth successfully.

Figure 4. The wealth of the adversary, when including fatal frontrunning
attacks (a)50% and (b)30% of the time, for f=0.1,0.8 and 0.9.

###  6.5. Tokenization on real-world MEV rewards

Here, we consider the real world MEV values that we have extracted from the
Ethereum blockchain. We use a similar procedure as when $\eta$ is stochastic.
Here too, we see that masquerade performs better than current practices.
Figure 5 shows the total wealth of the users in this system, along with
successful attacks.

Figure 5. Masquerade performs quite well even on real world Ethereum data

###  6.6. Token Epochs

For ease in analysis, we consider an alternate arrangement of the current
proposed model, as described in Section 5, where we separate the token
purchase and token spending into epochs. We can see that this process of
separating the token purchase and spend into phases is the same as our method,
where the tokens are purchased and spent continuously, over the course of a
number of rounds, as visualized in Figure 6.

Figure 6. Here, we see that the user wealth and the adversary wealth are equal
at different rounds/epochs, they are simply shifted, and their difference is
constant.

We observe that the continuous token purchase lags by a number of rounds. This
is because in the continuous case we also consider the possibility of a user
wanting to make non-MEV transactions, and the adversary does not attack these
transactions. As a result, there is a slight delay in reaching the same
amounts of wealth. However, they are essentially the same.

###  6.7. Ablation studies

We perform multiple ablation studies using different token conditions, such as
different token costs, expiration of the tokens, scenarios where the token
cost is unable to be returned to the users and the adversaries in the
following scenarios:

####  6.7.1. Token Costs

We consider different scenarios for token costs, ranging from extremely cheap
tokens, to extremely expensive tokens. As the tokens are eventually returned
to the users in the system, the token costs do not influence total wealth of
the system. If the tokens are cheaper, more users will be able to afford them,
whereas if the tokens are expensive, fewer users can afford them, which
reduces the number of tokenized transactions that can be made in a single
round. As a result, the adversary is able to manipulate this result due to all
users being able to afford only small number of tokens. We see that even when
starting with a small sum of wealth, the adversary is unable to frontrun or
backrun the user, when the token costs are reasonably priced.

####  6.7.2. Token with Expiration

In this case, the tokens expire after a set number of rounds. If the user does
not use these tokens within the set limit, they expire and the users are
unable to recoup the costs spent on the token. As a consequence of this, we
observe that it is generally in best interest of the user and adversary to not
hoard tokens and spend tokens before they expire.

####  6.7.3. Token with no Refund

In this case, a user will not receive a refund when they make a tokenized
transaction. Here, the token costs need to be cheap in order to incentivize
users to make tokenized transactions.

##  7\. Related Work

Common types of MEVs include frontrunning, backrunning and sandwich attacks.
An adversary is generally able to frontrun the transaction by listing a higher
transaction fee, so that their transaction is executed before the honest user.
Backrunning involves a similar strategy, except the adversary’s transaction is
placed immediately after the user. Sometimes, an adversary can place a pair of
transactions, right before and right after the user transaction, which can
lead to an artificial manipulation of asset prices, resulting in profit at the
cost of the user.

These MEVs, pose a significant threat to users, cause network congestion and
may even lead to centralization without appropriate mitigation strategies. So
far, there have been efforts to introduce countermeasures to MEVs. In this
section, we list the most popular solutions to MEV as follows:

  * •

MEV Auction Platforms: These MEV auction platforms are commonly used in post-
merge Ethereum. Generally, the idea here is that there exist builders such as
Flashbots(noa, 2023b), BloXroute(Klarman et al., 2018), MEV-Boost(Yang et al.,
2022) who assemble blocks with transactions they receive from users, the
public mempool as well as the ones the builder itself inserts to generate MEV.
A user is allowed to specify their transaction ordering preferences to miners
in exchange for compensation. These assembled blocks are then submitted to a
block proposer, with some promised profits. This is a ”commit-and-reveal”
strategy, i.e the proposer is unable to see the order of the transactions or
block contents, they can only look at the promised profit and some other
metadata. The block proposer then selects the block they wish to propose. MEV
auction platforms attempt to create a more competitive and efficient
environment for users to have control over how their transactions are ordered
and to capture some of the value that would otherwise go to miners. These
platforms can be beneficial for users who want to ensure their transactions
are executed in a specific way or who want to benefit from MEV themselves. A
key issue with this method is the reliance on a ”trusted builder”, though
theoretically, any builder can be part of the network.

  * •

Time-based Ordering Solutions: These solutions rely on establishing a certain
order in transactions, they establish a set of properties that the transaction
needs to satisfy in order to be part of the block. An example of this class of
solutions is Hedera(Baird et al., 2019), that uses median to establish the
timestamp of the received transaction. Fair ordering means that
$\texttt{txn}_{u}$ is executed before $\texttt{txn}_{a}$ if the median
received time of $\texttt{txn}_{u}$¡median received time of
$\texttt{txn}_{a}$. A problem of using median timestamps in this way, is that
it is susceptible to manipulation by adversary. Other examples of receive-
order fairness are Themis(Kelkar et al., 2021) and Aequitas(Kelkar et al.,
2020) which consider that if atleast $\gamma$ of the nodes receive transaction
$\texttt{txn}_{u}$ before $\texttt{txn}_{a}$, then $\texttt{txn}_{u}$ can be
included no later than $\texttt{txn}_{a}$. Wendy(Kursawe, 2020) uses relative
fairness to approach this issue. Their solution, is that if there exists some
time $t$ at which all honest nodes have seen transaction $\texttt{txn}_{u}$,
and they then saw transaction $\texttt{txn}_{a}$ after $t$, then
$\texttt{txn}_{u}$ is executed before $\texttt{txn}_{a}$. These class of
solutions pose a risk to the users based on latencies of nodes.

  * •

Content-agnostic Ordering: These class of solutions do not impose a constraint
on the ordering of the transactions, as long as the ordering is independent of
the content of these transactions. Most of these algorithms generally encrypt
all transactions, or use a trusted third party in order to hide the
transactions. They then wait for these transactions to be committed on to the
Blockchain, and finally provide the secret key in order to reveal the
transaction, and ensure validity etc. An example of this is TEX(Khalil et al.,
2019), which is used in a proof of work situation, where the user encrypts
their transaction using timelock puzzles, with the understanding that the
attacker cannot solve the puzzles faster than the user. This uses a trusted
custodian, and thus requires users to regularly check in to make sure the
custodian is not misbehaving. Tesseract(Bentov et al., 2019) requires the user
to trust additional secure hardware called TEE (Trusted Execution
Environment), which is responsible for encrypting the transactions and
releasing them after they have been committed to the block. Most of these
solutions remove ordering privileges from the miners, but result in additional
trust assumptions that may reduce the decentralization in the network.

##  8\. Conclusion

In this paper, we have shown that the utility obtained by the tokenization
system is better than the current utility, and we have suggested a possible
reform to the system without the need of a trusted builder or proposer. The
token system is a very powerful way for the user to be able to trick the
adversary in the real world, as an adversary is faced with the choice of
spending their token or saving it for a later transaction that may of may not
provide a better value. An adversary only has the information that a token has
been purchased, and is unable to decipher which token can be used for which
transaction, until it is too late. We have shown a huge improvement in the
transaction unstealability for a user in the system, thus improving the
overall fairness in the network. One of the major drawbacks of Masquerade, is
that it does not completely eliminate the presence of MEV attacks. To a large
extent, our algorithm prevents user losses, and stops transaction order
manipulation by removing a significant amount of miner privileges, however,
blind frontrunning is still possible in the system. An extension to the
project involves looking for lightweight, scalable solutions that can build on
top of Masquerade in order to completely eliminate MEV attacks. One possible
extension to this project also is to include dynamic behaviors by the
adversary and user in response to current policies.

## References

  * (1)
  * noa (2023a) 2023a.  Binance - Cryptocurrency Exchange for Bitcoin, Ethereum & Altcoins.  https://www.binance.com
  * def (2023) 2023\.  Decentralized Finance Market to Surge.  https://finance.yahoo.com/news/decentralized-finance-market-surge-usd-131500988.html
  * noa (2023b) 2023b.  Flashbots.  https://www.flashbots.net
  * mev (2023) 2023\.  MEV Outlook 2023.  https://eigenphi.substack.com/p/mev-outlook-2023#:~:text=In%202022%2C%20the%20total%20MEV,%2472.8%20billion%20contributed%20by%20bots
  * noa (2023c) 2023c.  Pancake Swap - Cryptocurrency Exchange for Ethereum.  https://pancakeswap.finance/
  * Adams et al. (2021) Hayden Adams, Noah Zinsmeister, Moody Salem, River Keefer, and Dan Robinson. 2021.  Uniswap v3 core.  _Tech. rep., Uniswap, Tech. Rep._ (2021).
  * Baird et al. (2019) Leemon Baird, Mance Harmon, and Paul Madsen. 2019\.  Hedera: A public hashgraph network & governing council.  _White Paper_ 1 (2019), 9–10.
  * Bentov et al. (2019) Iddo Bentov, Yan Ji, Fan Zhang, Lorenz Breidenbach, Philip Daian, and Ari Juels. 2019\.  Tesseract: Real-time cryptocurrency exchange using trusted hardware. In _Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security_. 1521–1538.
  * Brennecke et al. (2022) Martin Brennecke, Tobias Guggenberger, Benjamin Schellinger, and Nils Urbach. 2022.  The de-central bank in decentralized finance: a case study of MakerDAO.  (2022).
  * Cachin et al. (2022) Christian Cachin, Jovana Mićić, Nathalie Steinhauer, and Luca Zanolini. 2022.  Quick order fairness. In _International Conference on Financial Cryptography and Data Security_. Springer, 316–333.
  * Chitra and Kulkarni (2022) Tarun Chitra and Kshitij Kulkarni. 2022.  Improving proof of stake economic security via mev redistribution. In _Proceedings of the 2022 ACM CCS Workshop on Decentralized Finance and Security_. 1–7.
  * Heimbach et al. (2023) Lioba Heimbach, Lucianna Kiffer, Christof Ferreira Torres, and Roger Wattenhofer. 2023.  Ethereum’s Proposer-Builder Separation: Promises and Realities.  _arXiv preprint arXiv:2305.19037_ (2023).
  * Heimbach and Wattenhofer (2022a) Lioba Heimbach and Roger Wattenhofer. 2022a.  Eliminating sandwich attacks with the help of game theory. In _Proceedings of the 2022 ACM on Asia Conference on Computer and Communications Security_. 153–167.
  * Heimbach and Wattenhofer (2022b) Lioba Heimbach and Roger Wattenhofer. 2022b.  Sok: Preventing transaction reordering manipulations in decentralized finance.  _arXiv preprint arXiv:2203.11520_ (2022).
  * Kazerani et al. (2017) Ali Kazerani, Domenic Rosati, and Brian Lesser. 2017\.  Determining the usability of bitcoin for beginners using change tip and coinbase. In _Proceedings of the 35th ACM International Conference on the Design of Communication_. 1–5.
  * Kelkar et al. (2021) Mahimna Kelkar, Soubhik Deb, Sishan Long, Ari Juels, and Sreeram Kannan. 2021.  Themis: Fast, strong order-fairness in byzantine consensus.  _Cryptology ePrint Archive_ (2021).
  * Kelkar et al. (2020) Mahimna Kelkar, Fan Zhang, Steven Goldfeder, and Ari Juels. 2020.  Order-fairness for byzantine consensus. In _Advances in Cryptology–CRYPTO 2020: 40th Annual International Cryptology Conference, CRYPTO 2020, Santa Barbara, CA, USA, August 17–21, 2020, Proceedings, Part III 40_. Springer, 451–480.
  * Khalil et al. (2019) Rami Khalil, Arthur Gervais, and Guillaume Felley. 2019\.  Tex-a securely scalable trustless exchange.  _Cryptology ePrint Archive_ (2019).
  * Klarman et al. (2018) Uri Klarman, Soumya Basu, Aleksandar Kuzmanovic, and Emin Gün Sirer. 2018.  bloxroute: A scalable trustless blockchain distribution network whitepaper.  _IEEE Internet of Things Journal_ (2018).
  * Kursawe (2020) Klaus Kursawe. 2020\.  Wendy, the good little fairness widget: Achieving order fairness for blockchains. In _Proceedings of the 2nd ACM Conference on Advances in Financial Technologies_. 25–36.
  * Malkhi and Szalachowski (2022) Dahlia Malkhi and Pawel Szalachowski. 2022.  Maximal extractable value (mev) protection on a dag.  _arXiv preprint arXiv:2208.00940_ (2022).
  * Pichl and Kaizoji (2017) Lukáš Pichl and Taisei Kaizoji. 2017.  Volatility analysis of bitcoin.  _Quantitative Finance and Economics_ 1, 4 (2017), 474–485.
  * Yang et al. (2022) Sen Yang, Fan Zhang, Ken Huang, Xi Chen, Youwei Yang, and Feng Zhu. 2022\.  Sok: Mev countermeasures: Theory and practice.  _arXiv preprint arXiv:2212.05111_ (2022).
  * Zhang et al. (2022) Haoqian Zhang, Louis-Henri Merino, Vero Estrada-Galinanes, and Bryan Ford. 2022.  Flash freezing flash boys: Countering blockchain front-running. In _2022 IEEE 42nd International Conference on Distributed Computing Systems Workshops (ICDCSW)_. IEEE, 90–95.
  * Zhang et al. (2020) Yunhao Zhang, Srinath Setty, Qi Chen, Lidong Zhou, and Lorenzo Alvisi. 2020.  Byzantine ordered consensus without byzantine oligarchy. In _14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)_. 633–649.

##  Appendix A Proof of Theorem 4

###### Proof.

Supposing $W$ is the total wealth of adversary at the end of an epoch $e$
under any policy $\pi$. The total wealth of the adversary at the end of epoch
$e+1$ under $\pi$ is at most $W+\frac{W}{y}f\eta$. Hence, the total wealth of
adversary at end of $k$ epochs is at most
$W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{k}$ under $\pi$.

Now, since $\pi_{a}$ is a balanced policy

(29)
$\displaystyle\tilde{W}_{a}[1]=W_{a}[0]+\left\lfloor\frac{W_{a}[0]}{y}\right\rfloor
f\eta\geq W_{a}[0]\left(1+\frac{f\eta}{y}\right)-f\eta.$

Similarly,

(30)
$\displaystyle\tilde{W}_{a}[2]\geq\tilde{W}_{a}[1]\left(1+\frac{f\eta}{y}\right)-f\eta\geq
W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{2}-f\eta\left(1+\frac{f\eta}{y}+1\right).$

Repeating $k$ times, we have

$\displaystyle\tilde{W}_{a}[k]\geq
W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{k}-f\eta\frac{\left(1+\frac{f\eta}{y}\right)^{k}-1}{\frac{f\eta}{y}}$
(31)
$\displaystyle=W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{k}-y\left(1+\frac{f\eta}{y}\right)^{k}+y.$

Therefore the ratio between total wealth achieved under $\pi_{a}$ and the
upper bound is

(32)
$\displaystyle\lim_{k\rightarrow\infty}\frac{W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{k}}{W_{a}[0]\left(1+\frac{f\eta}{y}\right)^{k}-y\left(1+\frac{f\eta}{y}\right)^{k}+y}=\frac{W_{a}[0]}{W_{a}[0]-y}\leq\frac{y}{y-\eta\epsilon}k$

where the last inequality is due to $W_{a}[0]>y^{2}/(\eta\epsilon)$. ∎


# Proof of Irvine’s Conjecture via Mechanized Guessing

Jeffrey Shallit111Research supported by NSERC grant 2018-04118.
School of Computer Science
University of Waterloo
Waterloo, ON N2L 3G1
Canada
<EMAIL_ADDRESS>
###### Abstract

We prove a recent conjecture of Sean A. Irvine about a nonlinear recurrence,
using mechanized guessing and verification. The theorem-prover Walnut plays a
large role in the proof.

Key words: Irvine’s conjecture, Gutkovskiy’s sequence, numeration system,
morphism, automaton, Walnut, nonlinear recurrence, automatic sequence,
combinatorial game, subword complexity, critical exponent.

##  1 Introduction

Mathematicians have long used intelligent guessing of a problem’s solution,
followed by rigorous verification (for example, by induction), to prove
theorems. In this note I show how to do this, at least in some cases, using a
simple algorithm to infer a finite automaton from empirical data. Once a
candidate automaton is inferred, a rigorous proof of its correctness can be
supplied by using Walnut, a theorem-prover for automatic sequences [8, 10].

On May 24 2017 Ilya Gutkovskiy proposed the following nonlinear recurrence as
sequence A286389 in the OEIS (On-Line Encyclopedia of Integer Sequences) [11]:

$g_{n}=\begin{cases}0,&\text{if $n=0$;}\\\ n-g_{\lfloor
g_{n-1}/2\rfloor},&\text{otherwise.}\end{cases}$ (1)

The first few values of this sequence, which we call Gutkovskiy’s sequence,
are given in Table 1. This recurrence is a variation on similar sequences
originally discussed by Hofstadter [7, p. 137].

Then, on July 20 2022, Sean A. Irvine observed that this sequence seemed to be
given by the partial sums of the sequence A285431, which is the fixed point of
the morphism $h$, where $h(1)=110$ and $h(0)=11$. We denote the sequence
A285431 by $(k_{n})_{n\geq 1}$, in honor of its proposer, Clark Kimberling.
The first few values of the sequence A285431 are also given in Table 1; In
order to maintain the indexing given in the OEIS, we define $k_{0}=0$. More
precisely, then, Irvine’s conjecture is that $g_{n}=\sum_{1\leq i\leq
n}k_{i}$.

$n$ | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11
---|---|---|---|---|---|---|---|---|---|---|---|---
$g_{n}$ | 0 | 1 | 2 | 2 | 3 | 4 | 4 | 5 | 6 | 7 | 8 | 8
$k_{n}$ | 0 | 1 | 1 | 0 | 1 | 1 | 0 | 1 | 1 | 1 | 1 | 0
Table 1: First few values of $g_{n}$.

In this note we prove Irvine’s conjecture, as well as a number of related
results.

All the needed Walnut code to verify the claims of the paper is available on
the author’s website, https://cs.uwaterloo.ca/~shallit/papers.html.

##  2 From a morphism to a numeration system

We start with the morphism $h:1\rightarrow 110$, $0\rightarrow 11$ that
generates OEIS sequence A285431. Define $K_{n}=h^{n}(1)$, so that $K_{0}=1$,
$K_{1}=110$, $K_{2}=11011011$, and so forth.

######  Proposition 1.

For $n\geq 2$ we have $K_{n}=K_{n-1}K_{n-1}K_{n-2}K_{n-2}$.

###### Proof.

By induction on $n$. The base cases of $n=0,1$ are trivial. Otherwise assume
$n\geq 2$. Then

$\displaystyle K_{n}$
$\displaystyle=h^{n}(1)=h^{n-1}(h(1))=h^{n-1}(1)h^{n-1}(1)h^{n-1}(0)$
$\displaystyle=K_{n-1}K_{n-1}h^{n-2}(11)=K_{n-1}K_{n-1}K_{n-2}K_{n-2}.$

∎

Since each $K_{i}$ is the prefix of $K_{i+1}$, it follows that there is a
unique limiting infinite word ${\bf k}=k_{1}k_{2}k_{3}\cdots=1101101111\cdots$
of which all the $K_{i}$ are prefixes. Furthermore, Proposition 1 shows that
$\bf k$ is a “generalized automatic sequence” as studied in [9], and hence
there is a numeration system associated with it, where $k_{n}$ can be computed
by a finite automaton taking, as inputs, the representation of $n$ in this
numeration system.

We now explain how this is done. Define ${\cal K}_{n}=|K_{n}|$, so that ${\cal
K}_{0}=1$, ${\cal K}_{1}=3$, ${\cal K}_{2}=8$, and in general ${\cal
K}_{n}=2{\cal K}_{n-1}+2{\cal K}_{n-2}$. This two-term linear recurrence is
sequence A028859 in the OEIS (and also A155020 shifted by one).

We now build a numeration system, which we call $K$-representation, out of the
sequence $({\cal K}_{i})_{i\geq 0}$. We represent every natural number as a
sum $\sum_{0\leq i\leq t}a_{i}{\cal K}_{i}$, where
$a_{i}\in\Sigma_{3}:=\\{0,1,2\\}$. Furthermore we associate a ternary word
$a_{t}\cdots a_{0}$ with the corresponding sum, as follows: $[a_{t}\cdots
a_{0}]_{K}=\sum_{0\leq i\leq t}a_{i}{\cal K}_{i}$. Notice that words are
written “backwards” so the most significant digit is at the left.

Evidently numbers could have multiple representations in this system as we
have described it so far. For example $[22]_{K}=8=[100]_{K}$. In order to get
a unique, canonical representation, we impose the restriction
$a_{i}a_{i+1}\not=22$. This is in analogy with a similar restriction for the
Zeckendorf (or Fibonacci) numeration system. We let $(n)_{K}$ denote this
canonical representation for $n$. Table 2 gives the first few representations
in this numeration system. Notice that the canonical representation for $0$ is
$\epsilon$, the empty string.

$n$ | $(n)_{K}$
---|---
0 | $\epsilon$
1 | 1
2 | 2
3 | 10
4 | 11
5 | 12
6 | 20
7 | 21
8 | 100
9 | 101
10 | 102
Table 2: Representation for the first few numbers.

It is now easy to see that the greedy algorithm produces the canonical
representation [4]. Furthermore, it is easy to see that there is a finite
automaton that takes, as input, a string $x$ over the alphabet $\Sigma_{3}$,
and accepts if and only if $x$ is a canonical representation. It is depicted
in Figure 1. (We routinely omit useless states without comment.)

Figure 1: Automaton accepting canonical representations.

Some of the sequences we study in this paper were previously studied by
Fraenkel and co-authors [5, 1], in the context of some variations on Wythoff’s
game. These authors already found the numeration system we described here.
Also see [3]. Our main contribution is to combine the use of automata theory
with the numeration system.

##  3 An incrementer automaton for $K$-representations

We claim that we can go from the $K$-representation of $n$ to that of $n+1$ as
follows: if the last digit is $0$, add one to it. If the last digit is $1$,
add one to it, except in the case that the representation ends with
$a(21)^{i}$, for $a\in\\{0,1\\}$, in which case the representation of $n+1$
ends in $(a+1)0^{2i}$ instead. If the last two digits are $a2$, for
$a\in\\{0,1\\}$, then the last two digits of $n+1$ are $(a+1)0$. Verification
of this is straightforward and is left to the reader.

A synchronized automaton ‘incr’ implementing these rules is depicted in Figure
2. The meaning of “synchronized” here is that the DFA takes the canonical
$K$-representations of $n$ and $x$ in parallel as input, and accepts if
$x=n+1$.

Figure 2: Incrementer automaton for $K$-representations.

##  4 An adder automaton for $K$-representation

The next step is to build an “adder” for $K$-representations. This is a
synchronized automaton that takes, in parallel, the canonical
$K$-representations of integers $x,y,z$, and accepts if and only if $x+y=z$.
The existence of this automaton for our numeration system follows from very
general results of Frougny and Solomyak [6].

However, in this case it is actually easier to just “guess” the automaton from
empirical data, and then verify its correctness. The method of guessing is
based on the Myhill-Nerode theorem from formal language theory, and is
explained, for example, in [10].

Once we have an automaton that we believe is an adder, we can verify its
correctness by induction by checking the following conditions.

  * (i)

$\forall x,y\ \exists z\ \operatorname{add}(x,y,z)$ (adder is well-defined)

  * (ii)

$\forall x,y,z,w\
(\operatorname{add}(x,y,z)\,\wedge\,\operatorname{add}(x,y,w))\implies z=w$
(adder represents a function)

  * (iii)

$\forall x,y,z\ \operatorname{add}(x,y,z)\iff\operatorname{add}(y,x,z)$
(commutative law)

  * (iv)

$\forall x,y,z,t\ (\exists r\
\operatorname{add}(x,y,r)\,\wedge\,\operatorname{add}(r,z,t))\iff(\exists s\
\operatorname{add}(y,z,s)\,\wedge\,\operatorname{add}(x,s,t))$ (associative
law)

  * (v)

$\forall x\ \operatorname{add}(x,0,x)$ (base case of induction)

  * (vi)

$\forall x,y\ \operatorname{add}(x,1,y)\iff\operatorname{incr}(x,y)$
(induction step).

Our candidate adder had $42$ states. To verify its correctness, we use the
following straightforward implementation of the conditions above.

    eval check_i "?msd_kim Ax,y Ez $add(x,y,z)":
    eval check_ii "?msd_kim Ax,y,z,w ($add(x,y,z) & $add(x,y,w)) => z=w":
    eval check_iii "?msd_kim Ax,y,z $add(x,y,z) <=> $add(y,x,z)":
    eval check_iv "?msd_kim Ax,y,z,t (Er $add(x,y,r) & $add(r,z,t)) <=>
       (Es $add(y,z,s) & $add(x,s,t))":
    eval checkv "?msd_kim Ax $add(x,0,x)":
    eval checkvi "?msd_kim Ax,y $add(x,1,y) <=> $incr(x,y)":

and Walnut returns TRUE for all six statements. The correctness of the adder
now follows.

We briefly comment on the syntax of Walnut commands. Here A and E represent the universal and existential quantifiers $\forall$ and $\exists$, respectively. The jargon ?msd_kim means to interpret the statements using the $K$-numeration system. The symbol & means logical “and”, | means logical “or”, ~ is logical negation, => is implication, and <=> represents iff. The command def defines an automaton, eval evaluates truth or falsity, and reg converts a regular expression to an automaton.

##  5 The Kimberling sequence

Define $k^{\prime}_{n}=k_{n+1}$ for $n\geq 0$. It is now easy to create a DFAO
(deterministic finite automaton with output) computing the sequence
$(k^{\prime}_{n})_{n\geq 0}$, by associating states of the DFAO with letters
of the alphabet, and transitions with images of those letters, as explained in
[9]. It is depicted in Figure 3.

Figure 3: DFAO computing $k^{\prime}_{n}$.

This DFAO takes a canonical $K$-representation of $n$ as input, and outputs
(as the last state reached) the value of $k^{\prime}_{n}$. In Walnut this is
represented by the file KP.txt, as follows:

    msd_kim

    0 1
    0 -> 0
    1 -> 0
    2 -> 1

    1 0
    0 -> 0
    1 -> 0

Once we have this DFAO, we can get a DFAO for $(k_{n})_{n\geq 0}$ simply by
shifting the index.

    def kks "?msd_kim KP[n-1]=@1":
    combine K kks:

The resulting DFAO is depicted in Figure 4.

Figure 4: DFAO for the sequence $\bf k$.

We can now verify that this automaton actually does compute the Kimberling
sequence. We can do this by induction, by verifying that

${\bf k}[1..{\cal K}_{n}]={\bf k}[1..{\cal K}_{n-1}]\ {\bf k}[1..{\cal
K}_{n-1}]\ {\bf k}[1..{\cal K}_{n-2}]\ {\bf k}[1..{\cal K}_{n-2}].$

To do so, we use the following Walnut code:

    reg isk msd_kim "0*10*":
    reg pair msd_kim msd_kim "[0,0]*[1,0][0,1][0,0]*":
    eval checkk1 "?msd_kim At,x ($isk(x) & t>=1 & t<=x) => K[t+x]=K[t]":
    eval checkk2 "?msd_kim At,x,y ($pair(x,y) & t>=1 & t<=y) => K[t+2*x]=K[t]":
    eval checkk3 "?msd_kim At,x,y ($pair(x,y) & t>=1 & t<=y) => K[t+2*x+y]=K[t]":

Here $\operatorname{isk}(x)$ asserts that $x={\cal K}_{n}$ for some $n\geq 1$,
and $\operatorname{pair}(x,y)$ asserts that $x={\cal K}_{n+1}$ and $y={\cal
K}_{n}$ for some $n\geq 1$.

##  6 Synchronized automaton for Gutkovskiy’s sequence

The last piece of the puzzle we need is a synchronized DFA computing
Gutkovskiy’s sequence A286389. To find this automaton we once again guess it
from empirical data, and then verify it using Eq. (1).

The guessed $17$-state automaton is called ‘gut’. To verify its correctness we
use the following Walnut code:

    eval check1 "?msd_kim An Ex $gut(n,x)":
    eval check2 "?msd_kim An,x,y ($gut(n,x) & $gut(n,y)) => x=y":
    eval check3 "?msd_kim $gut(0,0) & An,x,y,z (n>=1 & $gut(n,x) &
       $gut(n-1,y) & $gut(y/2,z)) => x+z=n":

Thus our automaton correctly computes Gutkovskiy’s sequence.

##  7 Proof of Irvine’s conjecture

We now have everything we need to prove Irvine’s conjecture.

######  Theorem 2.

For $n\geq 0$ we have $g_{n}=\sum_{1\leq i\leq n}k_{i}$.

###### Proof.

We use the following Walnut code:

    eval check "?msd_kim An K[n]=@1 <=> (Ex $gut(n-1,x) & $gut(n,x+1))":

and Walnut returns TRUE. ∎

##  8 Some related sequences

We now turn to three related sequences; for $n\geq 1$ the first two give the
$n$’th positions of the ones (resp., zeros) in the sequence $\bf k$. We call
them $A_{n}$ and $B_{n}$, respectively. The third sequence, called $Q_{n}$,
has a more complicated definition:

$Q_{n}=\begin{cases}n,&\text{if $n\leq 1$;}\\\ Q_{m},&\text{if $n=Q_{m}+2m$
and there is }\\\ &\text{exactly one $i<n$ with $Q_{i}=Q_{m}$;}\\\ \text{least
positive integer not in $Q_{1},\ldots,Q_{n-1}$},&\text{otherwise.}\end{cases}$
(2)

It is sequence A026366 in the OEIS.

$n$ | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$A_{n}$ | 0 | 1 | 2 | 4 | 5 | 7 | 8 | 9 | 10 | 12 | 13 | 15 | 16 | 17 | 18 | 20
$B_{n}$ | 0 | 3 | 6 | 11 | 14 | 19 | 22 | 25 | 28 | 33 | 36 | 41 | 44 | 47 | 50 | 55
$Q_{n}$ | 0 | 1 | 2 | 1 | 3 | 4 | 2 | 5 | 6 | 7 | 8 | 3 | 9 | 10 | 4 | 11
Table 3: First few values of $A_{n}$, $B_{n}$, and $Q_{n}$.

Once again we can guess synchronized automata computing these functions and
verify that they are correct. The guessed automaton for $A_{n}$ has $23$
states, the guessed automaton for $B_{n}$ has $24$ states, and the guessed
automaton for $Q_{n}$ has 45 states. We call them ‘aa’, ‘bb’, and ‘qq’,
respectively.

We now verify correctness of $A$ and $B$:

    eval check_A_1 "?msd_kim An Ex $aa(n,x)":
    eval check_A_2 "?msd_kim An,x,y ($aa(n,x) & $aa(n,y)) => x=y":
    eval check_A_3 "?msd_kim Ax (En n>=1 & $aa(n,x)) <=> K[x]=@1":
    eval check_A_4 "?msd_kim An,x,y ($aa(n,x) & $aa(n+1,y)) => x<y":
    eval check_B_1 "?msd_kim An Ex $bb(n,x)":
    eval check_B_2 "?msd_kim An,x,y ($bb(n,x) & $bb(n,y)) => x=y":
    eval check_B_3 "?msd_kim Ax (En  $bb(n,x)) <=> K[x]=@0":
    eval check_B_4 "?msd_kim An,x,y ($bb(n,x) & $bb(n+1,y)) => x<y":

and Walnut returns TRUE for all of these.

To verify correctness of $Q$, we need to verify its definition:

    def occurs_once_in "?msd_kim (Ei,x i>=1 & i<n & $qq(i,x) & $qq(m,x)) &
       (~Ei,j,x i>=1 & i<j & j<n & $qq(i,x) & $qq(j,x) & $qq(m,x))":
    # true if Q_m occurs exactly once in Q_0, Q_1, ..., Q_{n-1}

    def occurs_in "?msd_kim Ei,y i<n & $qq(i,y) & $qq(i,x)":
    # true if x occurs in Q_0, ..., Q_{n-1}

    def least_not_in "?msd_kim (~$occurs_in(n,x)) &
       (Az (~$occurs_in(n,z)) => z>=x)":
    # true if x is the least integer not in Q_1, ..., Q_{n-1}

    eval check_Q_1 "?msd_kim An Ex $qq(n,x)":
    eval check_Q_2 "?msd_kim An,x,y ($qq(n,x) & $qq(n,y)) => x=y":
    eval check_Q_3 "?msd_kim Am,n,y,z (1<=m & m<n & $occurs_once_in(m,n) &
       $qq(m,y) & n=y+2*m & $qq(n,z)) => y=z":
    eval check_Q_4 "?msd_kim An,y ($qq(n,y) & ~(Em 1<=m & m<n &
       $occurs_once_in(m,n))) => $least_not_in(n,y)":

So indeed our automaton computes $Q_{n}$ correctly.

If we look at OEIS sequence A026367, we see that its description says
(essentially) “least $t$ such that $Q_{t}=n$”. This allows use to verify that
A026367 is in fact $A_{n}$, as follows:

    def check_A_5 "?msd_kim An,t $aa(n,t) => $qq(t,n) & Au (u<t) => ~$qq(u,n)":

Similarly, if we look at OEIS sequence A026368, we see that its description
says (essentially) “greatest $t$ such that $Q_{t}=n$”. We can then verify that
A026368 is in fact $B_{n}$, as follows:

    def check_B_5 "?msd_kim An,t $bb(n,t) => $qq(t,n) & Au (u>t) => ~$qq(u,n)":

In particular, we have proved Neil Sloane’s observation that “A026368 appears
to be [the] complement[ary] sequence of A026367 ”.

We can easily verify the observation of Fokkink, Ortega, and Rust [3] that
$B_{n}=2A_{n}+n$ for $n\geq 0$:

    eval check_FOR "?msd_kim An,x,y ($aa(n,x) & $bb(n,y)) => y=2*x+n":

and Walnut returns TRUE.

Finally, Fokkink, Ortega, and Rust [3] left the following as an open problem,
which we can turn into a theorem.

######  Theorem 3.

For all $n$ we have $A_{B_{n}}\in\\{A_{n}+B_{n}-1,A_{n}+B_{n}\\}$.

###### Proof.

We use the following Walnut code:

    eval check_FOR_2 "?msd_kim An,t,x,y ($aa(n,t) & $bb(n,x) & $aa(x,y)) =>
       (y=t+x|y+1=t+x)":

and Walnut returns TRUE. ∎

######  Remark 4.

Furthermore we could, if it were desired, give a DFAO that computes, for each
input $n$, which of the two alternatives in Theorem 3 holds.

Similarly we can prove, for example, that
$B_{A_{n}}-A_{n}-B_{n}\in\\{-3,-2,-1,0,1\\}$.

##  9 Subword complexity

Recall that the subword complexity function $\rho(n)$ counts the number of
distinct factors of length $n$ of an infinite word. In this section we compute
this function for $\bf k$.

Call a factor $w$ of an infinite binary word $\bf x$ right-special if both
$w0$ and $w1$ appear in $\bf x$. For binary words we know that
$\rho(n+1)-\rho(n)$ counts the number of length-$n$ right-special factors.

Walnut formulas for special factors are given in [10, §8.8.6]. Adapting them
to our situation, we have the following code:

    def keqfac "?msd_kim At (t<n) => K[i+t]=K[j+t]":
    def kisrs "?msd_kim Ej $keqfac(i,j,n) & K[i+n]!=K[j+n]":
    eval nothree "?msd_kim Ei,j,k,n $kisrs(i,n) & $kisrs(j,n) & $kisrs(k,n) &
       ~$keqfac(i,j,n) & ~$keqfac(j,k,n) & ~$keqfac(i,k,n)":
    def hastwo "?msd_kim Ei,j $kisrs(i,n) & $kisrs(j,n) & ~$keqfac(i,j,n)":

Here

  * •

keqfac asserts that ${\bf k}[i..i+n-1]={\bf k}[j..j+n-1]$;

  * •

kisrs asserts that ${\bf k}[i..i+n-1]$ is a right-special factor;

  * •

nothree asserts that there is no $n$ for which $\bf k$ has three or more
distinct right-special factors of length $n$;

  * •

hastwo accepts precisely those $n$ for which $\bf k$ has exactly two distinct
right-special factors of length $n$.

The automaton created by ‘hastwo’ is displayed in Figure 5.

Figure 5: Automaton accepting those $n$ for which $\bf k$ has exactly two
distinct right-special factors of length $n$.

We can now prove the following theorem.

######  Theorem 5.

The infinite word $\bf k$ has exactly two distinct right-special factors of
length $n$ if and only if there exists $i\geq 0$ such that one of the
following holds:

  * •

$x\leq n<x+{\cal K}_{2i}$, where $x={\cal K}_{1}+{\cal K}_{3}+\cdots+{\cal
K}_{2i+1}$;

  * •

$y\leq n<y+{\cal K}_{2i+1}$, where $y={\cal K}_{0}+{\cal K}_{2}+\cdots+{\cal
K}_{2i+2}$.

###### Proof.

We use the following Walnut code:

    reg ul msd_kim msd_kim "[0,0]*[1,1][0,1]([1,1][0,0])*(()|[1,1]":
    eval check_sw "?msd_kim An $hastwo(n) <=> Ex,y $ul(x,y) & x<=n & n<y":

and Walnut returns TRUE. ∎

######  Corollary 6.

We have $\limsup_{n\geq 1}\rho(n)/n=(30+\sqrt{3})/23\doteq 1.37965438$ and
$\liminf_{n\geq 1}\rho(n)/n=(3+\sqrt{3})/4\doteq 1.1830127$.

##  10 Critical exponents

Recall that we say $p\geq 1$ is a period of a finite word $x=x[1..n]$ if
$x[i]=x[i+p]$ for $1\leq i\leq n-p$. The exponent of a finite word $x$ is the
length of $x$ divided by its shortest period. Finally, the critical exponent
of an infinite word $\bf z$ is the supremum, over all finite nonempty factors
$x$ of $\bf z$, of the exponent of $x$.

######  Theorem 7.

The critical exponent of $\bf k$ is $(2\sqrt{3}+12)/3\doteq 5.1547$.

###### Proof.

Since the basic ideas have already been covered elsewhere in detail [10, pp.
148–150], we just sketch them here. We create Walnut formulas for the shortest
period of a factor of $\bf k$, and then obtain the corresponding longest words
with the given period. Then we restrict to those factors of exponent at least
$5$. The resulting automaton, computed by ‘klong5’, accepts pairs of the form
$(n,p)=([121(01)^{i}0]_{K},[10(00)^{i}0]_{K})$ and
$(n,p)=([121(01)^{i}02]_{K},[10(00)^{i}00]_{K})$. Routine work with two-term
linear recurrences then gives the result.

    def kperi "?msd_kim p>0 & p<=n & Aj (j>=i & j+p<i+n) => K[j]=K[j+p]":
    def klper "?msd_kim $kperi(i,n,p) & (Aq (q>=1 & q<p) => ~$kperi(i,n,q))":
    def kleastp "?msd_kim Ei,n n>=1 & $klper(i,n,p)":
    def klongest "?msd_kim (Ei $klper(i,n,p)) &
       (Ar,i $klper(i,r,p) => r<=n)":
    def klong5 "?msd_kim $klongest(n,p) & n>5*p":

∎

## Acknowledgments

I thank Michel Dekking for telling me about his paper [2], and in particular
its Remark 9.

## References

  * [1] S. Artstein-Avidan, A. S. Fraenkel, and V. T. Sós.  A two-parameter family of an extension of Beatty sequences.  Discrete Math. 308 (2008), 4578–4588.
  * [2] F. M. Dekking.  On Hofstadter’s $G$-sequence.  Arxiv preprint arXiv:2307.01471 [math.CO], July 25 2023. Available at https://arxiv.org/abs/2307.01471.
  * [3] R. Fokkink, G. F. Ortega, and D. Rust.  Corner the empress.  Arxiv preprint arXiv:2204.11805 [math.CO], December 8 2022. Available at https://arxiv.org/abs/2204.11805.
  * [4] A. S. Fraenkel.  Systems of numeration.  Amer. Math. Monthly 92 (1985), 105–114.
  * [5] A. S. Fraenkel.  Heap games, numeration systems and sequences.  Ann. Combin. 2 (1998), 197–210.
  * [6] C. Frougny and B. Solomyak.  On representation of integers in linear numeration systems.  In M. Pollicott and K. Schmidt, editors, Ergodic Theory of $\mathbb{Z}^{d}$ Actions (Warwick, 1993–1994), Vol. 228 of London Mathematical Society Lecture Note Series, pp. 345–368. Cambridge University Press, 1996.
  * [7] D. R. Hofstadter.  Gödel, Escher, Bach: an Eternal Golden Braid. Basic Books, 1979.
  * [8] H. Mousavi.  Automatic theorem proving in Walnut.  Arxiv preprint arXiv:1603.06017 [cs.FL], available at http://arxiv.org/abs/1603.06017, 2016.
  * [9] J. Shallit.  A generalization of automatic sequences.  Theoret. Comput. Sci. 61 (1988), 1–16.
  * [10] J. Shallit.  The Logical Approach to Automatic Sequences: Exploring Combinatorics on Words with Walnut, Vol. 482 of London Math. Soc. Lecture Notes Series.  Cambridge University Press, 2022.
  * [11] N. J. A. Sloane et al.  The On-Line Encyclopedia of Integer Sequences.  Electronic resource available at https://oeis.org, 2023.