If It Walks Like an Arbitrage: Protocol-Agnostic Detection with Decidable Structural Equivalence

Motivation

• Arbitrage and flash-loan attacks create diverse, nested fund-flow structures whose transaction-level explanation and strategy equivalence remain unresolved.Arbitrage bots exploit transient AMM price inefficiencies within atomic transactions, while similar mechanics enable flash-loan attacks.Source: §1 · p. 1

Related work

• Unlike pattern catalogs, aggregate token graphs, and learned labels, the approach preserves transfer structure while avoiding protocol-specific assumptions.DeFiRanger, graph methods, classifiers, richer representations, and survey findings [17] motivate this gap.Source: §1 · p. 2

Canonical structural substrate

• The system reduces execution traces to unique canonical forms, making fund-flow structural equivalence decidable under terminating and confluent rewriting.Detection and family classification become queries over the canonical-form substrate.Source: §1 · p. 2

Detection

• Arbitrage cycles emerge at fixpoint rather than being searched explicitly, with positive-profit canonical cycles yielding sound classifications and diagnostic transfer chains.The method also captures flash-loan arbitrages without lending-specific logic.Source: §1 · pp. 2–3

Representation and portability

• A sender-enriched AST distinguishes swaps from relays through call hierarchy, using standard token and WETH ABIs without protocol-specific knowledge across Arbitrum and BSC.Each transfer carries a sender field derived from the call hierarchy, and the same binary is used on both chains.Source: §1 · p. 3

Evaluation

• The evaluation covers 220 000 Ethereum blocks against Eigenphi and 1 000 shared blocks in a three-way comparison with ArbiNet.The Rocq sources, evaluation pipeline, and binaries are publicly available.Source: §1 · p. 3

2.1 Ethereum Execution Model

• Ethereum transactions may invoke nested smart-contract calls, producing hierarchical execution traces that record call frames, side effects, and emitted logs.Internal CALL, DELEGATECALL, and STATICCALL operations form the call tree preserved by the EVM trace.Source: §2.1 · p. 3
• Transfers are represented uniformly as source, destination, amount or identifier, token type, and enclosing-call sender, distinguishing externally orchestrated swaps from relays.DELEGATECALL preserves the caller context, allowing proxy interactions to be handled correctly; fungible amounts contribute to profit calculations.Source: §2.1 · p. 3

2.3 Transfer Graphs and Cash Flow Trees

• The cash flow tree mirrors the EVM call stack, preserving sibling relationships that rewriting uses to link transfers into chains and identify closing cycles.Transfer-graph edges capture value movement, while AST nesting captures the contract invocations that produced those transfers.Source: §2.3 · p. 4
• An arbitrage cycle returns to its origin, matches endpoint tokens under token equivalence, and has strictly positive net balance in the cycle token.ETH and WETH may be treated as equivalent at cycle boundaries, while other token pairs require strict equality.Source: §2.3 · p. 5

2.4 Pipeline Overview

• The pipeline decodes raw traces into annotated cash flow trees, then performs pure in-memory fixpoint rewriting, profit computation, and classification.Only decoding accesses external ABI and OSINT sources; OSINT enrichment is attached but not consumed by detection.Source: Figure 2 · p. 4, §2.4 · p. 5

3 Detection Algorithm

• The algorithm identifies arbitrage as a positive-balance transfer cycle, obtained by repeatedly rewriting the AST until a unique canonical form is reached.The process chains, merges, annotates, and connects transfers; tx𝑅’s parallel paths converge into a +0.0023 WETH cycle.Source: §3 · p. 6, §3.3 · p. 12

3.1 From Traces to ASTs

• The first phase builds a call-nesting AST whose leaves represent decoded value movements, then trims structural noise and degenerate zero-value transfers.The AST preserves one leaf per transfer and retains only subtrees containing leaves, reducing tx𝑅 to twelve transfer leaves.Source: §3.1 · pp. 6–8

3.2 Manipulation of the AST Leaves

• Leaf manipulation chains adjacent different-token transfers, lifts reduced subtrees, merges parallel paths, and normalizes mint/burn and wrap/unwrap flows for protocol-agnostic processing.Mint and burn pairs become token-mint or token-burn chains that can participate in later cycle connection.Source: §3.2 · pp. 8, 10, 11

3.3 Manipulation of the AST Nodes

• Node manipulation chains same-token pass-throughs, merges compatible chains, annotates closed cycles, and connects complementary open chains at a fixpoint.Termination occurs within at most 3n−2 passes, while wide sibling sets approach the O(n^2) worst case.Source: §3.3 · pp. 11–12

3.4 Leftover Recovery and Profit Calculation

• After cycle reduction, validation removes economically non-positive arbitrages, while leftover recovery reconstructs distant round-trips before profit calculation.Specular and complementary matching capture flash-loan borrow/repay patterns; unmatched or undecoded transfers remain leftovers and may make profit incomplete.Source: §3.4 · pp. 12–13

3.5 Classification

• Classification computes gross and net token balances, returning Arbitrage only when a cycle exists, no leftovers remain, and the final balance is unambiguously positive.Otherwise the system conservatively returns Warning; token equivalence is parameterized as an arbitrary boolean relation and supports native/wrapped-token cycles.Source: §3.5 · pp. 14–15
• Arbitrage verdicts require a closed, token-matched, positive cycle with no leftovers; otherwise verdict-determining conditions downgrade results to Warning or reject them.Warnings diagnose incomplete decoding or deliberately unsupported mixed-sign cross-token valuation, while explanatory reasons do not gate the decision.Source: §3.5 · p. 15, §3.6 · p. 16

3.6 Formal Properties

• All five theorems and the uniqueness corollary are mechanized in Rocq with 157 lemmas, 8 theorems, 4 corollaries, 5 564 lines, and 0 Admitted.The computable step function supports extraction of a verified reference implementation, while the proofs use 10 Parameters and 0 axioms.Source: §3.6 · pp. 15, 17
• The rewriting system preserves original transfers, reaches normal form in at most 3n−2 passes for an initial AST with n leaves, and is sound for arbitrage labels.Every resulting chain corresponds to walks in the original transfer graph, every transfer appears in the initial AST, and an arbitrage classification implies positive net change.Source: §3.6 · pp. 15–16
• Deterministic trace-order rewriting yields a unique normal form, with confluence and uniqueness established for every initial AST.The deterministic step function resolves overlapping rewrite sites; the least and greatest fixpoints therefore coincide.Source: §3.6 · pp. 16–17
• Structural equivalence induced by R1–R15 is decidable by reducing both ASTs to normal forms and testing syntactic equality.The procedure is linear in the reduced normal-form size after normalization and polynomial overall.Source: §3.6 · p. 17

4 Implications of Decidability

• Every transaction reduces to a unique canonical form, so structural predicates over cycles, chains, leftovers, and their nesting inherit decidable procedures.Queries can use normalization, syntactic equality, skeleton maps, finite set membership, and finite delta-map inspection without changing the rewriting kernel.Source: §4 · p. 18, §4.4 · pp. 22–23

4.1 Structural Equivalence by Example

• Reduce-and-compare decides equivalence: tx𝑅 and tx𝑆 share a star topology but differ in arity, while skeleton abstraction places them in the same parametric family.The examples use three versus six parallel sub-chains and show that canonical forms support mechanical comparison even for large nested traces.Source: §4.1 · p. 20, §4.4 · p. 24

4.2 A Context-Free Grammar for Strategy Families

• A context-free grammar characterizes exactly the star-convergent arbitrage normal forms whose parallel branches share a convergence token and return to the hub.The grammar’s characterization is bidirectional, and new strategy families require productions over the existing canonical-form vocabulary rather than rewriting changes.Source: §4.2 · pp. 20–21

4.3 Extending the Grammar: Flash-Loan Wrappers

• Flash-loan wrappers extend the grammar with leftover-cycle nodes while preserving the rewriting kernel; membership is decidable in linear time under the hub-token condition.The flash-loan family contains 51% of exclusive confirmed detections, and the illustrated form combines a star cycle with LC(weth, 14 175.71).Source: §4.3 · pp. 21–22

4.4 From Detection to Query Language

• The query language treats canonical forms as an intermediate representation, making five structural queries decidable and allowing abstractions such as skeleton equality to define strategy families.The present paper empirically instantiates only arbitrage detection; richer delta-based predicates remain decidable, while systematic abstraction design is future work.Source: §4.4 · pp. 22, 24

5.1 Dataset and Baseline

• Across 220,000 Ethereum blocks, Argos flags 790,593 transactions using only standard ERC/WETH events and call hierarchy, against Eigenphi’s 649,790 protocol-informed flags.The evaluation releases per-transaction verdicts and uses full execution traces, while no public independently annotated ground truth exists.Source: §5.1 · p. 25

5.2 Detection Accuracy

• Confirmed detections achieve 87.2% Eigenphi agreement, while probable, attempted, and uncertain tiers achieve 70.8%, 39.5%, and 21.0%, respectively.The monotonic agreement gradient emerged from the diagnostic tiers rather than being engineered.Source: §5.2 · pp. 25–26

5.3 Manual Validation

• Manual validation finds zero false positives among 100 jointly confirmed and 100 Argos-only confirmed transactions, with 99 of 100 Argos-only samples genuine arbitrages.Argos-only confirmed cases are larger and more flash-loan-heavy, with median eight hops versus five and 51% versus 2% involving flash loans.Source: §5.3 · p. 26

5.4 Comparison with ArbiNet

• ArbiNet’s 81% overlap is a lower bound after a three-year training gap; baseline-exclusive detections often contain inner cycles or cross-token routes rather than missed arbitrages.Argos requires no retraining, whereas ArbiNet misses arbitrages involving routing contracts absent from its 2022 training data and produces false positives on batch settlement protocols.Source: §5.4 · p. 27

5.5 Topology and Performance

• The system recovers 245,497 attempted arbitrages, while 89.1% of transactions reduce to one cycle and the rewriting algorithm runs in 0.07 ms median.The full pipeline including decoding, but excluding trace retrieval, runs in 0.25 ms median and 2.24 ms at P95.Source: §5.5 · pp. 27, 29

5.6 Synthesis

• 83.5% agreement with Eigenphi, 81% coverage of ArbiNet, and 60,199 exclusive confirmed detections establish strong benchmark overlap while revealing substantial additional activity.On the ArbiNet subset, Argos also covers 92% of Eigenphi’s detections; comparisons are framed as intersystem agreement because no independent per-transaction ground truth exists.Source: §5.2 · p. 26, §5.4 · p. 27, §5.6 · p. 29
• 99.2% of detections, or 784,446, come from the formally guaranteed fixpoint, while the post-fixpoint promotion path contributes the remaining 0.8%.The promotion rule addresses cycles traversed by the transaction sender under specific token and leftover conditions, and produced zero observed misfires in sampled confirmed-tier transactions.Source: §5 · p. 25, §5.6 · p. 29

Scope of prior measurement

• Existing work measures MEV using known protocol signatures and misses cross-protocol composability, while canonical structural analysis addresses arbitrage through protocol-agnostic normalization.Qin et al. measured $540M over 32 months as a lower bound, and Zhou et al. identified composability as a recurring gap across 181 DeFi incidents totaling $3.24B.Source: §6 · p. 29

Graph-based detectors

• Aggregate token-graph methods scale to millions of arbitrages but lose per-transaction execution context, and flat cycles can mistake yield harvesting for price exploitation.Call hierarchies preserve the context needed to refine cycles and distinguish genuine arbitrage from cyclic non-arbitrage flows.Source: §6 · pp. 29–30

Protocol-specific detectors

• Protocol-specific catalogs identify DeFi actions but require handcrafted, per-protocol extensions and provide no formal guarantees.The rewriting system instead covers shared structural patterns across protocols, including split-and-merge and lending-based arbitrages, without manual extension.Source: §6 · p. 30

Machine-learning approaches

• ArbiNet provides ABI-free binary labels, whereas this system reconstructs transfer chains, calculates profit, reports diagnostic reasons, and offers mechanized formal guarantees.Section 5.4 supplies a quantitative comparison on 1 000 shared blocks.Source: §6 · p. 30

Formal methods

• Canonical forms partition realized transactions, while formal-methods alternatives enumerate attacks from specifications or replay observed strategies; bridging to Clockwork Finance remains open.KEVM formalizes EVM bytecode semantics, whereas this work abstracts above bytecode to typed transfers.Source: §6 · p. 30

Execution semantics

• The approach operates at execution-semantic level, addressing composability across transactions and chains and the structural incompleteness of transfer graphs for beneficiary attribution.Cao et al. [39] advocate execution-semantic analysis, which this approach already provides.Source: §6 · p. 30

Contribution

• The system makes arbitrage one query over a canonical-form substrate with mechanized structural soundness and decidable equivalence, addressing tradeoffs among coverage, granularity, and explainability.Materwala et al. identify these three dimensions as a central tradeoff in existing detectors.Source: §6 · p. 30

7 Limitations

• Decoder coverage is an open empirical limitation: missing transfers reduce recall but do not compromise soundness.The theorems apply only to transfers emitted by the decoder; measuring decoder coverage is outside the paper’s scope.Source: §7 · p. 30
• Single-transaction traces cannot detect cross-transaction, bridge-routed cross-chain, or non-atomic arbitrage strategies.Heimbach et al. attribute 25%+ of DEX volume to non-atomic flows pairing on-chain swaps with off-chain CEX trades; block-level canonical analysis is a proposed next step.Source: §7 · p. 30
• The evaluation covers only one 30-day window, and no public historical MEV label datasets support cross-regime comparison.Source: §7 · p. 30

• 60 199 exclusive confirmed detections and 245 497 failed attempts emerged across 220 000 blocks, while the structural approach matched a production platform in coverage.The results also show that 99.2% of detections come from the formal core and are sound by construction.Source: §8 · p. 31
• Every Ethereum transaction reduces under R1–R15 to a unique canonical form, making structural equivalence of fund flows decidable.Termination and confluence support uniqueness, and all five properties were mechanized in Rocq with zero Admitted obligations.Source: §8 · p. 31
• The EVM call hierarchy and a sender field derived from CALL/DELEGATECALL let arbitrage cycles emerge from a fixpoint rather than protocol-specific searches.Canonicalization remains the primary output for both the formal core and the 0.8% outside it, supporting universal auditability.Source: §8 · p. 31
• The same binary extends to Arbitrum and BNB Smart Chain with only configuration changes, while new predicates and rule extensions could target attacks beyond arbitrage.Decidable equivalence could also support unlabeled MEV taxonomies and clustering, but complete soundness still presupposes an a-priori universe of arbitrage topologies.Source: §8 · p. 31

Data sources

• The evaluation analyzes publicly available Ethereum transactions without collecting private data, involving human subjects, or interacting with live markets; therefore, no IRB/ERB approval was required.Transactions, traces, and transfer events are recorded on a public, permissionless blockchain.Source: Ethical Considerations · p. 33

Dual-use risk

• The system’s confirmed-transaction outputs could aid strategy reverse engineering, but opportunities are already executed, information is otherwise public, and no operational MEV infrastructure is provided.The output includes transfer chains, profit calculations, and pool identifiers; extraction also requires mempool monitoring, gas optimization, and sub-second execution.Source: Ethical Considerations · p. 33

Privacy and de-anonymization

• Address enrichment uses public OSINT metadata, but detection relies only on transfer tuples and call hierarchy, and the released dataset excludes labels, balances, and entity identifiers.The authors acknowledge that combining verdicts with external sources could still contribute to de-anonymization of pseudonymous actors.Source: Ethical Considerations · p. 33

Classification neutrality

• The system classifies cyclic profitable fund flows structurally, without distinguishing beneficial arbitrage from exploitative extraction; intent interpretation remains with the analyst.This neutrality is deliberate and identified as an open research direction.Source: Ethical Considerations · p. 33

Open Science

• The release provides formal proofs, three evaluation data files, a 25-script pipeline, Dockerized detection binaries, and raw traces sufficient to reproduce verdicts, figures, and tables.Raw traces cover 1 000 blocks from each evaluation range; reproducing the full 220K-block dataset requires an Ethereum archive node with debug_ traceTransaction.Source: Open Science · pp. 33–34

A AMM Pricing and Arbitrage Condition

• The detector is insensitive to AMM pricing invariants because diverse pool types expose standard transfer events; rules R1 and R5 handle multi-token pools, vaults, singleton routers, and hooks without modification.This covers constant-product, concentrated-liquidity, StableSwap, weighted pools, and newer designs such as Curve v2, Solidly/Velodrome, and Algebra.Source: A AMM Pricing and Arbitrage Condition · p. 35

B Proofs

• The five core theorems are fully mechanized in Rocq, with 5,564 lines, 157 lemmas, 8 theorems, 4 corollaries, and 0 admitted obligations or axioms.The development uses 15 rewrite rules plus lifting, with R16 represented by the validated_arbitrage predicate; the Rocq scripts are the authoritative reference.Source: B Proofs · p. 36

B.1 Proof of Theorem 3.1 (Preservation)

• Preservation is proved by induction: chaining, lifting, merging, and cycle connection retain walk correspondence, so reduced closed nodes faithfully represent arbitrage cycles using only trace-graph edges.Merged nodes represent sets of walks, while delta-map aggregation and closure conditions preserve the economic arbitrage interpretation.Source: §B.1 · pp. 37–38

B.2 Proof of Theorem 3.2 (Termination)

• Termination follows from lexicographic decrease of μ(T) = (u(T), c(T)), where labeling decreases u and merging decreases c without increasing either component.The mechanized additive bound is at most 3n−2 non-trivial passes, derived from u(T_0) ≤ n and c(T_0) ≤ 2n−2.Source: §B.2 · pp. 38–39
• The fixpoint converges in a finite number of k passes.This establishes practical termination of the iterative procedure.Source: §B.2 · p. 40
• The number of passes k grows with maximum width, measured by sibling count.Wider groups of sibling calls require more passes.Source: §B.2 · p. 40
• Convergence depends on call-frame width rather than hierarchy depth.The depth of the call hierarchy does not determine the practical pass count.Source: §B.2 · p. 40

Proof of Soundness

• Algorithm 4 returns Arbitrage if and only if cycles exist, no leftovers remain, gross and net balances are positive, and neither balance is mixed.Strict priority prevents Arbitrage when no_cycles, leftovers, final_neg, or final_mixed is present.Source: §B.3 · pp. 40–41
• The proof concludes that every Arbitrage verdict contains a closed, token-matched, economically positive cycle compliant with Definition 2.5 and grounded in original transfer-graph edges.The five conditions establish structural validity, economic profitability, and complete value attribution without hidden flows.Source: §B.3 · pp. 40–41
• Soundness guarantees no false positives for Arbitrage, but genuine arbitrages may receive Warning when leftovers exist or balances are mixed.The converse implication does not hold.Source: §B.3 · p. 41

Delta consistency

• When token equivalence spans multiple tokens, economically correct profit sums deltas across the equivalence neighborhood rather than checking one token alone.The mechanized core handles strict token equality, while post-fixpoint promotion handles equivalent native-wrapped pairs.Source: §B.3 · p. 41

Mechanized boundary

• The mechanized core formally exposes closure, endpoint correspondence, walk decomposition, original-edge inclusion, and positive gross delta for every surfaced Arbitrage cycle.These invariants are inherited through rewrite traces and discharge the structural portion of Definition 2.5; net profitability follows from delta decomposition.Source: §B.3 · pp. 41–42

Step 1: Chaining

• Chaining is deterministic because call-frame structure and swap-pair uniqueness permit at most one compatible sibling partner, making greedy closest-first selection order-independent.Separate EVM calls create separate AST subtrees, while each swap contributes a uniquely identifiable token-qualified pair within a call.Source: §B.4 · pp. 42–43

Step 2: Lifting

• Lifting is deterministic because liftability depends only on tree structure, independent subtrees commute, and nested nodes must be lifted bottom-up.The set of liftable nodes is uniquely determined by the current tree state.Source: §B.4 · p. 43

Step 3: Merging and connection

• Merging and cycle connection converge to the same normal form because parallel-path aggregation is associative and commutative, while the fixpoint eventually applies every compatible rule.Different intermediate orderings preserve the same edges, walks, and delta-map sums after convergence.Source: §B.4 · p. 43

Full pipeline

• Each pipeline stage produces a unique output from its input, so the final reduced AST and verdict are uniquely determined by the execution trace.The full pipeline combines deterministic AST construction, leaf and node manipulation, delta validation, and classification.Source: §B.4 · p. 44

Mechanized proof

• Rocq mechanization derives confluence by induction over deterministic derivations and well-foundedness, yielding a unique reachable normal form ∃!T_f.The computable step function is deterministic, and the constructively proved well-founded measure supplies termination.Source: §B.4 · p. 44

Remarks

• Property 1 prevents critical pairs by selecting one rule per redex through trace order, while Theorem 3.4 remains valid for any fixed router instantiation.Different router sets may induce different normal forms, but convergence and uniqueness are unaffected by the chosen fixed set.Source: §B.4 · p. 44

B.5 Proof of Theorem 3.6 (Decidable equivalence)

• Decidable equivalence follows because every term has a unique normal form, and computing that form followed by syntactic tree equality decides the word problem.Termination bounds normalization by at most 3n−2 steps, while confluence ensures uniqueness.Source: §B.5 · p. 45
• The equivalence proof identifies joinability with equality of normal forms in both directions, establishing the decision procedure for ≡_R.Confluence reduces any common reduct to the unique normal forms, and equal normal forms provide a common reduct.Source: §B.5 · p. 45
• Every arbitrage-labeled canonical chain is a closed walk in the transfer graph, but the inclusion is strict because graph cycles need not satisfy R14’s structural endpoint condition.The yield-harvest witness contains eight closed transfer-graph walks, none meeting R14’s τ_in = τ_out requirement.Source: §B.5 · p. 45

B.6 Rocq Trust Base

• The Rocq theorems are parametric over opaque address and token types, boolean classification predicates, and any supplied net-positive cost model.The deployment well-formedness condition for token equivalence is not a theorem precondition, and attempted arbitrages are characterized as structurally defined cycles with net_positive returning false.Source: §B.6 · p. 45
• The extracted Phase-3 kernel is covered by declarative rewrite sequences under the invariant that every child chain is labeled before merging.Annotation passes map to cascaded rewrite applications, while merging maps to a merge rewrite followed by relabeling.Source: §B.6 · p. 46

C Forensic Case Studies

• The reduced AST provides a readable, protocol-independent account of transaction behavior across three forensic cases.The cases include a token-migration arbitrage invisible to a flat graph, a 17,912 WETH arbitrage missed by Eigenphi with a three-hop route and 73% builder bribe, and a structurally rejected yield harvest.Source: C Forensic Case Studies · p. 46

C.1 A Stablecoin Migration Exploit

• The stablecoin case reduces to 10 chain nodes, including two arbitrage cycles, and connects agEUR, EURe, EUROC, and WETH flows into the main route.The fixpoint connects agEUR → EURe → EUROC → agEUR, while the remaining chains represent swaps, residual sale, unwrap, and token burn.Source: §C.1 · p. 46
• The migration exploit nets 2,413 EURe because old-contract EURe is retained while post-migration tokens continue through the cycle.The algorithm detects the positive EURe delta from differing entry and exit amounts without knowing that a migration occurred.Source: §C.1 · pp. 46–47
• The stablecoin transaction uses a 2,413.95 agEUR Balancer flash loan whose borrow and repayment collapse into one leftover cycle.The confirmed arbitrage has two cycles, zero leftovers, and a positive final balance, with gross deltas of +2,413.39 EURe and +0.000636 ETH against −0.000182 ETH gas.Source: §C.1 · p. 47

C.2 A 17,912 WETH Arbitrage That Eigenphi Misses

• 17,912 WETH gross profit and 4,824 ETH net to the EOA establish a confirmed arbitrage that Eigenphi misses.The operation routes ETH through BNT and AAVE into WETH, pays 13,088 ETH to the builder, and incurs 0.00005 ETH gas cost.Source: §C.2 · pp. 47–48
• The WETH case derives its full analysis from 6 ERC-20 transfers and 8 ETH value transfers, exposing the route, flash loan, builder bribe, and net profit.Its reduced AST contains two closed-loop chains, zero leftovers, and matched WETH entry and return flows.Source: §C.2 · pp. 47–48
• A 1,000× return exposes a price discrepancy at the AAVE/WETH pool along the three-hop ETH → BNT → AAVE → WETH route.The AST records the flows and profit, while the cause—such as a liquidity event, governance action, or manipulation—remains outside the algorithm’s scope.Source: §C.2 · pp. 47–48
• 13,088 ETH, or 73% of gross profit, goes to the block builder after a 14,175.71 WETH flash loan is reduced to a leftover cycle.The remaining 4,824 ETH goes to the EOA after the bot unwraps 17,912 WETH.Source: §C.2 · p. 48

C.3 A Yield Harvest That Looks Like an Arbitrage

• The complex trace contains 346 internal calls, depth 11, 24 ERC-20 transfers, and 11 tokens, but reduction starts from 31 leaves and finishes in 13 steps.The final tree contains eight closed-loop chain nodes plus leftover transfers and burns.Source: §C.3 · p. 48
• Eight reduced closed loops are independent swaps, reward sales, and LP unwraps; none satisfies R13 or R14 because input and output tokens differ.For example, CVX is converted through ETH into WETH, forming a closed address loop but not a token cycle.Source: §C.3 · pp. 48–49
• USDC flows form a funnel: 30,703 USDC and 107 USDC enter from pools, while 19,212 USDC reaches the EOA and 11,598 USDC reaches a vault wrapper.No USDC returns to its source pool, so the apparent multi-hop structure is not a cycle.Source: §C.3 · p. 49
• The transaction is not an arbitrage: no cycle satisfies τin = τout, gross balance is mixed, and net profit is negative.It burns LP tokens, claims CRV and CVX rewards, converts proceeds to USDC, and withdraws.Source: §C.3 · p. 49
• The AST preserves call hierarchy and token continuity that flat transfer graphs lose, enabling an auditable explanation for rejecting address-level cycles.A flat graph or GNN could flag shared-address cycles, whereas the AST separates pool interactions into independent subtrees.Source: §C.3 · p. 49
• The detector reaches the no-cycle verdict without recognizing Curve, Convex, crvUSD, frxUSD, or vault contracts, using only adjacency and token continuity.It processes 24 transfers and checks τin against τout for each of eight closed loops.Source: §C.3 · p. 49

D Cross-Chain Portability

• The rewriting system’s portability relies only on deterministic sequential EVM execution, and a smoke test ran unchanged on Arbitrum One and BNB Smart Chain.The test demonstrates model portability rather than serving as a cross-chain evaluation.Source: D Cross-Chain Portability · p. 50

D.1 Arbitrum

• 50 confirmed arbitrages and 952 warnings occurred among 23,250 Arbitrum transactions, with 4.3% flagged overall and 2.0 cycles per confirmed transaction.The lower rate than Ethereum reflects Arbitrum’s transaction mix, dominated by user-initiated swaps and transfers rather than MEV strategies.Source: §D.1 · p. 50
• Arbitrum’s representative two-swap transaction reduced to the same single annotated cycle and leftover extraction as Ethereum triangular arbitrages, despite chain-specific execution differences.Its mixed final balance caused a Warning because the algorithm could not assess overall profitability without a price oracle.Source: §D.1 · pp. 50–51

D.2 BNB Smart Chain

• 88 confirmed arbitrages and 922 warnings were found among 38,126 covered BSC transactions, with 2.6% flagged overall and 1.2 cycles per confirmed transaction.The sample contained approximately 105,000 transactions, but 66,874 legacy transactions were outside decoder scope; warnings comprised 68% attempted arbitrages and 32% real cycles downgraded by leftovers.Source: §D.2 · p. 51
• The BSC confirmed case reduced to the same three-swap triangular canonical shape as Ethereum and Arbitrum, with R1 chaining and R14 annotation firing identically.The fixpoint found positive wbnb and zero leftovers, yielding a clean confirmed arbitrage.Source: §D.2 · p. 51

D.3 Implications

• Rewriting, sender enrichment, and cycle annotation transferred unchanged across Arbitrum and BSC, with the wrapped-asset address as the only chain-specific parameter.The validations span different consensus mechanisms, block times, and gas-pricing models.Source: §D.3 · p. 51
• Detection worked without OSINT pool names or protocol tags because the analysis layer reasons over token flows and sender fields rather than external metadata.This demonstrates separation between decoding and analysis.Source: §D.3 · p. 51
• Across all three chains, triangular, multi-hop, and batched arbitrages exhibited the same structures and were produced by the same R1 and R14 fixpoint rules.Only token addresses and pool contracts differed, indicating chain-agnostic MEV structure.Source: §D.3 · p. 52
• Porting beyond EVM would require only a new decoder: Solana SPL Token instructions and Cross-Program Invocations can supply equivalent transfers, call trees, and invoker fields.The rewriting rules, fixpoint, and formal properties would remain unchanged.Source: §D.3 · p. 52

Agreement

• Three transactions—0x4573, 0xf170, and 0x0fdc—form a high-confidence arbitrage consensus across ArbiNet, Eigenphi, and structural rewriting.The comparison covers a randomly chosen block containing 311 transactions; ArbiNet and the structural system each flag five arbitrages, while the structural system additionally flags one warning.Source: E ArbiNet Comparison: Case Study · p. 52

False positive

• The structural system rejects ArbiNet’s 0x8dc9 false positive because its two closed loops run from USDC to USDT, violating token-identity equivalence despite apparent stablecoin price equivalence.The reduced AST reports zero arbitrage cycles, whereas graph-topology classification may treat stablecoins as interchangeable.Source: E ArbiNet Comparison: Case Study · pp. 52–53, Table 3 · p. 53

False negatives

• +2.0 × 10−5 WETH profit is present in ArbiNet’s 0x4744 false negative, where the fixpoint identifies a WETH-to-ETH three-pool cycle that Eigenphi also confirms.ArbiNet misses the transaction because its routing contracts were absent from 2022 training data; a second cycle wraps ETH profit back to WETH.Source: E ArbiNet Comparison: Case Study · p. 53, Table 4 · p. 53
• +7.2 × 10−6 is the profit in ArbiNet’s 0x9d71 false negative, a Uniswap V4 triangular arbitrage whose ETH-to-WETH cycle the fixpoint detects.ArbiNet misses this case because the relevant contracts are post-2022; a second cycle unwraps the settlement.Source: E ArbiNet Comparison: Case Study · pp. 53–54, Table 5 · p. 54

Emergent swap identification

• The algorithm infers swaps from complementary ERC-20 Transfer events, recovering 6 transfers as three swaps, 3 as two, and 4 as two with mismatched boundary tokens.In another Curve and Uniswap V3 example, it recovers 10 swaps from transfers despite only four emitted swap events, making undeclared exchanges observable.Source: E ArbiNet Comparison: Case Study · p. 54

Summary

• The case study identifies three structural advantages: token identity filters false positives, fixpoint detection remains training-independent, and reduced ASTs explain constituent fund flows.These properties eliminate temporal degradation on unseen contracts while giving analysts a readable structural account.Source: E ArbiNet Comparison: Case Study · p. 54