ProofForge

EVM

Yul + 锁定 solc 0.8.34 · Anvil 工程差分

目标

evm

族

合约虚拟机

轨道

accepted Phase 1

成熟度

Yul + 锁定 solc 0.8.34 · Anvil 工程差分

主制品

Yul + solc bytecode (.bin / .abi)

工具锁定

solc 0.8.34 + Anvil 0.3.0（双 profile：默认 + cancun）

可部署

true

Feature 清单

本目标的产品面计数（工程词汇，不是营销分数）。

12

合计

9

已支持

1

部分

1

显式拒绝

1

缺失

跨链对照：目标矩阵

执行模型

账户 + storage

持久 storage 槽；message-call 语义；gas 与原子回滚。

Anvil 工程门

G4 脚本跑 Counter/TipJar/TokenJar/EnvRead 语料——不是 formal Reference↔Anvil。

pf.assets 绑定

产品路径含 native deposit/transfer、token.transfer、balanceOfSelf 环境读。

体积诚实

大型 Token creation bytecode 可超 EIP-3860；不能单凭此声称主网可部署。

制品

文件角色
*.yul / *.bin / *.abi.json主制品
proof-forge.output.v1闭包

Feature 列表

今天能 lower 什么、显式拒绝什么、仍缺失什么。

流水线与工具

Target-owned EvmPlan → Yul → 锁定 solc。

3/4 已支持

  • SUPPORTED

    EvmPlan / materializeResult

    基于 CompiledSemanticV1 的 planFromCapability；无 alpha residual 路径。

  • SUPPORTED

    锁定 solc finalize

    EvmSolc

    solc --strict-assembly 验收；缺工具按 profile 干净跳过或 fail-closed。

  • SUPPORTED

    Anvil 差分（G4）

    G4

    工程 init/mutate/overflow/emit 语料——不是 formal D4/TST。

  • MISSING

    Formal Reference↔Anvil

    未闭合；不得把 Anvil 绿灯写成 formal 完成。

状态与类型

各 target 中最宽的标量/聚合面之一。

3/4 已支持

  • SUPPORTED

    多宽度 UInt/Int + UInt128/256

    窄/宽 body 子集，含 EVM-only 宽整数。

  • SUPPORTED

    Field bn254

    mod-p 域算术通道。

  • SUPPORTED

    Struct/Enum/Array/Map/Bytes/Option/String

    Map cap-8 UInt64 + Principal 键试点；Bytes N×UInt8；Option UInt64 状态；String match N-A1。

  • FAIL-CLOSED

    Option 参数 / 嵌套 Option

    Option UInt64 状态试点之外仍 fail-closed。

副作用与资产

emit/revert、context 键、static-QN 调用、pf.assets。

3/4 已支持

  • SUPPORTED

    emit / bare revert / assert

    产品路径；语料含 Anvil 日志观察。

  • SUPPORTED

    contextRead（时间/高度/caller）

    ADR-0025 / S1-S2

    版本化键；未知键 FC。caller = u32le(20)||CALLER。

  • PARTIAL

    externalCall / schedule（static QN）

    对 path-hash 地址真实 CALL 桩；部署地址绑定未闭合。

  • SUPPORTED

    pf.assets native + token + balanceOfSelf

    ADR-0029/0030

    TipJar/TokenJar/EnvRead 产品 + Anvil 腿。transferAsync 仍 FC。

Profile

evm-yul-solc-0.8.34-v1

默认锁定 solc 路径；无 ambient --evm-version。

evm-yul-solc-0.8.34-cancun-v1

同 solc 引脚加 --evm-version cancun；runtime 用 Anvil --hardfork cancun。

构建

# EVM (after tool root materialize)
just toolchains-provision-external
just toolchains-materialize-external "$PWD/build/dev-tool-root"
PROOF_FORGE_TOOL_ROOT="$PWD/build/dev-tool-root" \
  lake env .lake/build/bin/proof-forge-next build \
    Examples/Counter.lean \
    --module Examples.Counter \
    --target evm -o build/counter-evm

lake env .lake/build/bin/proof-forge-next inspect build/counter-evm --json
开放名单 →目标矩阵 →