发表机构
Functori（Functori公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出了基于Rocq实现的可判定资金流结构等价性方法，将其应用于协议无关的套利检测，在以太坊及Arbitrum、BSC上的评估显示其检测精度高且覆盖广。
AI 中文摘要
以太坊交易具有规范结构形式，每个执行轨迹构建为按调用帧嵌套分组的代币转移抽象语法树，通过包含15条规则的收敛项重写系统归约为唯一规范形式。该系统具有终止性、可靠性和收敛性，由此产生的资金流结构等价性是可判定的，所有五个性质均在Rocq中实现且无承认义务。规范形式使资金流的结构问题可判定，为策略家族分类、机器人指纹识别和基于等价性的归因开辟了道路。本文将规范形式应用于套利检测：循环在不动点处出现并可从规范形式中读取，无需协议特定模式。该流程仅依赖标准ERC代币和WETH ABI，无协议特定事件，因此同一二进制文件可在Arbitrum和BSC上未修改运行。我们在220000个以太坊区块上针对Eigenphi（生产级MEV平台）进行评估，在1000个共享区块上针对ArbiNet（GNN分类器）进行评估。系统产生469801个确认检测和245497个尝试套利；在所有检测中，它与Eigenphi的一致性为83.5%，覆盖ArbiNet的81%，同时呈现60199个独家确认检测。99.2%的检测仅由不动点产生，且按构造可靠；对500笔交易的手动验证发现，确认层级无误报；对200个Eigenphi独家检测的法医重新分析发现，63.5%在规范形式中无循环，9.0%有不动点检测到但我们的保守分类器未检测到的循环。
英文摘要
Whether a transaction performed an arbitrage, and by which route, is a question asked of its execution trace after the fact. We conjecture that such traces admit a normal form on which questions of this kind become queries, and we test it by building one and putting it to work. Each trace becomes an abstract syntax tree of token transfers, grouped by call- frame nesting. A term rewriting system of 16 rules reduces it. Rewriting terminates and carries exactly the transfers of the trace, whichever order the rules fire in. Under a deterministic kernel scanning the EVM-fixed trace order, every trace has a unique normal form, and the structural equivalence this induces on fund flows is decidable. Preservation, termination, soundness, uniqueness and decidability are mechanized in Rocq with zero admitted obligations. We report arbitrage detection in full: cycles emerge at the fixpoint and are read off the normal form with no protocol-specific patterns. Detection is the query we evaluate at scale; structural equivalence is a second query. The pipeline depends only on the standard ERC token and WETH ABIs, so the same binary runs unmodified on Arbitrum and BSC. We evaluate on two arbitrary block ranges, analysed in full with no transaction excluded: 220 000 Ethereum blocks against EigenPhi, a widely used MEV detection platform, and 1 000 shared blocks against ArbiNet, a graph neural network classifier. These are the only tools and label sets in this domain we were able to reuse. We report 469 801 confirmed arbitrages, overlapping 83.5% with EigenPhi and 81% with ArbiNet, together with 245 497 attempted arbitrages and 60 199 confirmed detections EigenPhi does not report. 99.2% follow from the fixpoint alone and are sound over the decoded transfers, and manual validation of 500 transactions finds no false positive among the confirmed.
