test(pipe-exec): tx_filter⟷revm 差分预言机 (difftx)#399
Conversation
新增机制驱动的差分测试预言机，机械化验证核心不变式
**tx_filter ⊇ revm 交易级校验**：任何被 tx_filter 放行、却被 revm 以
InvalidTransaction 拒绝的交易，都会在 lib.rs:1323 的 executor.execute().unwrap()
处 panic = 停链 DoS。两侧预言机喂同一 (tx, sender, 种子状态)，revm 侧走真实
pinned revm 的 evm.transact。
- Tier-1（单 tx 字段级）：覆盖 revm 全 32 个 InvalidTransaction 变体，12 个
live crafter 经断言确认能真触发 revm 拒绝；当前 0 gap（证明 filter 是字段级
超集）。matrix_has_no_gap 作为 CI 门；no_gap_gate_is_non_vacuous 防止空过。
- Tier-2（多 tx 顺序执行差分）：确定性在进程内复现已知 7702 停链——filter 放行
[tx0,tx1] 两笔，但执行 tx0 的 7702 委托码 CREATE 把账户 A 的 nonce 二次抬升，
tx1 执行期 NonceTooLow{tx:1,state:2} → 停链。等价于 gnode attack 7702-halt。
仅新增测试/差分入口（difftx feature 门控的 difftx 模块 + difftx 二进制），
不改任何生产逻辑；tx_filter.rs 保持不变。
跑法：cargo run -p reth-pipe-exec-layer-ext-v2 --features difftx --bin difftx
（exit 3 = 发现 gap）。
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 463bc30ffe
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| filter_admit: false, | ||
| revm_reject: false, | ||
| revm_variant: Some(reason.to_string()), | ||
| is_gap: false, |
There was a problem hiding this comment.
These note rows are included in variant_matrix() but hard-code filter_admit, revm_reject, and is_gap to false, so matrix_has_no_gap can never fail for any variant routed through note_cases. In the revm-bump scenario this oracle is supposed to gate (for example, a forward-watch variant becoming reachable), CI will still report zero gaps unless someone first rewrites the note into a live case, making the matrix a false negative rather than a mechanical superset check.
Useful? React with 👍 / 👎.
| assert!( | ||
| out.revm_reject, | ||
| "用例 {} 未能让 revm 拒绝（revm_variant={:?}）—— crafter 需修正", | ||
| case.name, out.revm_variant |
There was a problem hiding this comment.
This coverage test only asserts that revm rejected the transaction, not that it rejected with the variant named by the case. If a fixture trips an earlier validation after a gas, balance, or fork-setting tweak, the test still passes and the matrix row is labeled as covering the intended variant while actually exercising a different one; please assert out.revm_variant matches case.name for the live cases.
Useful? React with 👍 / 👎.
在 difftx 差分预言机上扩两根杠杆,把「攻击面」从单一不变式 + 手搓输入 放大到「多预言机 + 量产生成」: - difftx_exec（新预言机类,feature difftx_exec):serial(revm 顺序执行, WrapExecutor) ⟷ grevm(并行执行,GrevmExecutor) 执行差分。同一批交易、 逐字节相同的种子状态分别过两个后端,diff BundleState(state/contracts/ state_size)+ receipts。任何背离 = 共识 state-fork(节点对状态分歧 → 链 分裂),一类静态分析看不出、只有真跑才现形的致命 bug。 实测:5 baseline + 4 对抗块(RAW/WAW 同槽、同发送者 nonce 链、同收款人 余额 WAW、nonce+storage 混合)全部 serial==grevm,grevm 正确串行化了依赖, 未发现 fork。附带发现并 pin 一处良性非共识差异:raw reverts 的块内顺序 + 尾部空块不同(reverts 不入 state root),故按 Address→AccountRevert 语义 比对(仍抓内容回归)。 - difftx_fuzz(仅测试期,proptest):把 difftx 的 12 个手搓单笔 + 1 条序列 升级成对整个字段空间的 property 搜索——单笔(类型/nonce/gas/fee/value/ initcode 跨 EIP-3860 边界/chain_id/access-list)、多笔序列、7702 授权列表 (alloy_signer_local 真实签名,受控 authority;auth 数/chain_id/nonce match+1+gap+MAX/自赞助/重复 authority)。 实测:各 64 例 + 非空门,filter⊇revm 不变式全程成立,未发现新 gap —— 证明该超集在搜索空间内是完整的(不止 12 个手搓点)。 仅新增测试/差分入口(feature 门控),不改任何生产逻辑。 跑法:cargo test -p reth-pipe-exec-layer-ext-v2 --features difftx_exec --lib difftx （14 tests）;cargo run --features difftx_exec --bin difftx_exec（exit 3=有背离）。 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ddf4f416fe
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| .zip(case.senders.iter()) | ||
| .map(|(tx, sender)| { | ||
| let mut raw = Vec::new(); | ||
| tx.encode_2718(&mut raw); |
There was a problem hiding this comment.
When a difftx_exec case diverges, this artifact tells operators to submit raw_2718_hex, but those bytes still contain the dummy Signature::test_signature() used by the fixtures while the oracle itself bypasses recovery via RecoveredBlock::new_unhashed(..., case.senders.clone()). On a live node the sender is recovered from the raw signature instead of the JSON sender, so the transaction will run from a different account than the seeded fixture and the repro will either fail nonce/balance checks or exercise a different block; please either sign with the fixture sender keys or emit a replay format that preserves explicit senders.
Useful? React with 👍 / 👎.
| "addr": format!("{}", s.addr), | ||
| "balance": format!("{}", s.info.balance), | ||
| "nonce": s.info.nonce, | ||
| "has_code": s.info.code.is_some(), |
There was a problem hiding this comment.
For any divergence in the code-dependent cases (for example the delegated 7702 baseline or the RAW/WAW storage adversarial case), the artifact only records has_code and drops the actual bytecode and storage from SeedAccount. The reproduction steps ask operators to preseed the accounts, but this JSON no longer contains enough state to reconstruct the block that the oracle executed, so those artifacts cannot reproduce the reported fork; include the code bytes/code hash and storage values instead of only a boolean.
Useful? React with 👍 / 👎.
| let mut serial = fresh_serial_executor(chain_spec.clone(), cache.clone()); | ||
| let mut grevm = fresh_grevm_executor(chain_spec, cache); | ||
|
|
||
| let serial_res = serial.execute(&block); |
There was a problem hiding this comment.
For blocks that call Gravity's custom precompile addresses, both executors here run without the apply_custom_precompiles setup that the production path performs before user transaction execution, so the oracle compares two non-production executions and can report equality for a block whose real Gravity execution depends on BLS/randomness/mint native code. Please apply the same precompile set to both serial and grevm before executing, or explicitly exclude those addresses from this oracle's scope.
Useful? React with 👍 / 👎.
把 difftx_fuzz 的量产生成能力接到 difftx_exec 的执行差分上:proptest 生成 6 类并行执行 hazard 的对抗块,逐块过串行 revm 与 grevm 双后端,断言 `!diverged`(无共识 state-fork)且 `serial_ok == grevm_ok`(无单侧 panic/Err)。 这是把生成器接到执行差分上的最强 hunt——搜静态看不出的 silent fork。 hazard 类(各自 proptest 策略,共 144 例):存储 RAW/WAW 同/异槽、同发送者 nonce 链交织、同收款人余额 WAW、CREATE + CREATE2 同 salt 地址碰撞、7702 委托 账户被多笔触碰、SELFDESTRUCT 同受益人余额 WAW。 实测:144 例 + 非空门全绿,**未发现 serial↔grevm 背离或非对称停链**—— grevm 的并行调度在这些依赖形态下与串行 revm 逐字节一致。一旦 proptest 最小化 出 diverged 反例即为真实 fork/halt 发现(不 allowlist,让测试大声失败)。 仅测试期 harness(difftx_exec feature 门控),不改任何生产逻辑。 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 35d7d73b06
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| )), | ||
| ); | ||
| } | ||
| mk(false, None) |
There was a problem hiding this comment.
For Prague blocks that emit EIP-7685 requests, production fills requests_hash from the executor output in calculate_roots (execute/src/lib.rs:1432), but this oracle returns mk(false, None) after comparing only bundle state, receipts, and gas. If serial and grevm produce different BlockExecutionResult.requests while state/receipts/gas match, this reports no divergence even though the payload header/request stream would fork; please compare so.result.requests against go.result.requests before the success return.
Useful? React with 👍 / 👎.
| assert!( | ||
| both_ok > 0, |
There was a problem hiding this comment.
Because both_ok is aggregated across all strategies, one executable sample from any generator lets this pass even if, for example, the create or eip7702 strategy has degenerated into producing only blocks where both backends return Err. In that case the corresponding property tests can pass vacuously on serial_ok == grevm_ok == false and stop exercising fork detection for that hazard class; track a per-strategy success and fail with the strategy name instead.
Useful? React with 👍 / 👎.
在 difftx 上再加两类 Gravity 特有面的不变式预言机(feature 门控,不改生产逻辑): - difftx_precompile(feature difftx_precompile):mint / randomness 自定义 precompile。三条不变式全绿:①caller 门无绕过(非授权 caller——含差一位地址 ——干净 Err 且不铸币,授权 caller 精确铸 amount);②畸形输入(空/短/超长/错 func-id/gas 不足/amount=MAX)永不 panic(precompile panic=全网停链); ③把 mint precompile 经 apply_custom_precompiles 装进两后端后,serial ⟷ grevm 逐字节一致——含理想路径:授权 caller 字节码 CALL mint 直改 journal,后续 tx 花掉铸出的余额,两后端一致 ⇒ grevm 正确把 precompile 的直写当读写依赖追踪, 未 fork。 - difftx_2935(feature difftx_2935):EIP-2935 / BLOCKHASH。①exec-time BLOCKHASH(探针合约 SSTORE 进 slot 再读,取执行器实际喂给 EVM 的值,非 RPC 视图)在 N-1/N-2/N-128/N-256 上 serial==grevm 且等于规范 hash;②用**生产 结构体** RawBlockViewProvider 造截断窗口(<256 对),确认合法 in-256-window 但落在环外的块号 block_hash_ref 返回 BlockTooOld(block_view_storage/mod.rs :201/272)——**在真实代码上证实了红队记录的截断窗口前置条件**;存储层返回 Err(不 panic),完整 exec→panic 链(真 provider + warm-restart)如实记为需 pipe_test/集群复现,未伪造。 净结论:两类自定义面在当前 main 上均未发现新缺口(gating 稳、无 panic、无 serial≠grevm);2935 截断窗口风险在存储层被证实可达。 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 55c1bd598f
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| assert!( | ||
| tx1_admitted, | ||
| "经验事实：filter 未放行 tx1（filter_admitted={:?}）—— 该路径已被 filter 关闭，不是开放 gap", |
There was a problem hiding this comment.
When the difftx feature tests are run, this assertion makes the test pass only if the filter still admits tx1 in the known 7702 nonce-race gap, and the following assertion requires the execution-time NonceTooLow gap to be present. That inverts the CI signal: the suite is green while the chain-halt condition is still open and turns red once the filter is fixed; please make this a failing invariant (exec_gaps empty) or mark it as an ignored/manual reproducer.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 413648cb02
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| fn mint_custom_precompiles() -> Arc<Vec<(Address, DynPrecompile)>> { | ||
| Arc::new(vec![(NATIVE_MINT_PRECOMPILE_ADDR, create_mint_token_precompile())]) |
There was a problem hiding this comment.
When this helper is used by run_precompile_exec_diff, the block executor is configured with only the mint precompile, but production user-block execution gets its executor precompiles from custom_precompiles_for_ordered_block (lib.rs:569-602), which installs BLS/randomness, while mint is only passed to transact_system_txn for system transactions (lib.rs:955-960). This means the authorized-mint-then-spend case is exercising a user-transaction path that production cannot take, and the actual BLS/randomness custom-precompile path can still fork without this oracle covering it; please build the harness from the production precompile set or route mint through the system-transaction path it uses in production.
Useful? React with 👍 / 👎.
| /// 且至少存在让 revm 拒绝的用例（`revm_reject` 可达 true）。若 builder 造出的交易全被某一侧硬拒， | ||
| /// 上面的 `!is_gap` 断言会平凡通过而失去意义——本测试把这两半可达性钉死。 | ||
| #[test] | ||
| fn fuzz_generators_are_non_vacuous() { |
There was a problem hiding this comment.
This non-vacuity test only proves the single-transaction generator can produce one admitted tx and one revm rejection; it never samples seq_case_strategy or seq_7702_auth_strategy. If those sequence generators drift so their fee/gas/nonce/auth choices are all filtered out, run_seq_case returns an empty exec_gaps set without executing any admitted transaction, so both sequence properties above pass vacuously while the TOCTOU/auth-list surfaces stop being tested; add an admitted/executed sample check for each sequence generator.
Useful? React with 👍 / 👎.
1 participant
背景
Gravity「先共识排序、后执行」模型下，执行器无法从单笔交易的
revm::InvalidTransaction错误恢复——crates/pipe-exec-layer-ext-v2/execute/src/lib.rs:1323的executor.execute(&block).unwrap_or_else(|err| panic!(...))会直接 panic 整个进程 = 停链 DoS。因此tx_filter::filter_invalid_txs必须是 revm 交易级校验的超集（superset）：漏掉任何一个 revmInvalidTransaction变体 = 一条能被放行、却在 executor panic 的交易。本 PR 新增一个机制驱动的差分测试预言机，把这个不变式从「手维护的文档矩阵」变成机械可验证 + CI 门控的东西，并能确定性复现已知的 7702 停链。
做了什么
只新增测试 / 差分入口（
difftxfeature 门控），不改任何生产逻辑——tx_filter.rs及其它生产文件保持 pristine。src/difftx.rs—— 差分预言机模块（featuredifftx下的pub mod）。两侧预言机喂同一 (tx, sender, 种子 CacheDB)；revm 侧走真实 pinned revm 的evm.transact，只把EVMError::Transaction(InvalidTransaction)记为拒绝。is_gap = filter_admit && revm_reject。src/bin/difftx.rs—— 命令行工具：跑矩阵 + 7702 自检，对每个 gap 写出gnode可复现的 tx.json 制品，有 gap 时 exit 3。Cargo.toml：[features] difftx+ 门控的[[bin]] difftx；lib.rs：一行#[cfg(feature="difftx")] pub mod difftx。Tier-1 —— 单 tx 字段级差分矩阵
覆盖 revm（
revm-context-interface-10.2.0）全部 32 个InvalidTransaction变体，其中 12 个有 live crafter 并经断言确认能真触发 revm 拒绝。当前 0 gap——这正是期望结果：机械证明 filter 是字段级完全超集。matrix_has_no_gap作为 CI 门：任何未来 revm bump 重新打开一个变体缺口都会立刻变红。no_gap_gate_is_non_vacuous反-vacuity 门：证明filter_admit能取到true（合法交易两侧都放行），使「0 gap」不是某侧被硬编成 false 的假象。Tier-2 —— 多 tx 顺序执行差分（执行诱导 TOCTOU 自检）
把
[tx0, tx1]整块过 filter，再把放行集顺序、逐笔提交地过真实 revm，抓「被 filter 放行、却在执行期被 revm 拒绝」的交易。在进程内确定性复现已知的 7702 停链（等价gnode attack 7702-halt）：state: 2证明执行 tx0（F→A）时 A 的 7702 委托码运行了CREATE，把 A 的 nonce 从 1 二次抬到 2——超出 filter「每 tx +1」模型，故 tx1（nonce 1）执行期NonceTooLow→ 停链。filter 的顺序 sim 覆盖了 authorization-list 的 nonce 抬升（audit#822），但不覆盖执行诱导的这一类——该 gap 真实且当前 OPEN。怎么跑
7/7 测试绿；fmt(nightly) + clippy 在新文件上干净；默认（无 feature）构建不变。
🤖 Generated with Claude Code