| 统一 testkit 场景 | just testkit | Rust/Cargo；来自 lean-toolchain 的 Lean 工具链；EVM bytecode 分支需要 solc；ValueVault EVM 分支的 Contract SDK selector hydration 需要 Foundry cast；Solana/Mollusk 分支可选依赖 sbpf 和 solana-keygen | RFC 0007 testkit 会发现 testkit/scenarios/counter.toml 和 testkit/scenarios/value-vault.toml，通过 Lean 发射 WAT fixture 并在确定性的 runtime/offline-host wasmtime NEAR host 上运行；当所需 EVM 工具可用时，发射 EVM runtime bytecode 与 artifact metadata，并在进程内 revm 上运行覆盖到的场景；如果 Solana 工具链可用，还会发射 Solana sBPF assembly/manifest/artifact metadata、构建 sBPF ELF，并通过 mollusk-svm 运行有状态场景；同时校验 scenario-declared artifact expectation，包括 Counter 在 Wasm/NEAR WAT、EVM Yul 和 Solana assembly/manifest 上的 golden source equality、ValueVault 在 Wasm/NEAR WAT、EVM Yul 以及 Solana sBPF assembly/manifest 上的 golden equality、结构化 JSON/TOML metadata/manifest path 断言（包括存在性、缺失性、类型、非空，以及 array/object/table/string length 检查）、EVM deploy manifest schema 检查、针对生成 artifact path/byte-size/SHA-256 entry 的 JSON metadata file-reference 检查、内嵌 Solana IDL metadata 的 cross-artifact JSON equality，以及 ValueVault IDL/client shape 检查；最后校验每个 target 的返回期望，并对已执行 target 断言规范化 observable trace parity | live NEAR sandbox 部署、live EVM RPC/deployment 行为、Surfpool/Web3 Solana 部署行为、替换所有旧的逐目标 smoke 脚本、event/log/gas/compute-budget parity |
| Lean 包构建 | lake build | 来自 lean-toolchain 的 Lean 工具链 | 库根节点通过类型检查且 proof-forge 链接成功 | 生成的 Yul/字节码有效性、外部工具、运行时行为 |
| 目标注册表冒烟测试 | lake env lean --run Tests/TargetRegistry.lean | 来自 lean-toolchain 的 Lean 工具链 | 目标注册表将 evm 暴露为 compiler target，同时让 robinhood-chain-testnet 和 anvil-local 等 EVM-compatible chain profile 只作为 lookup-only deployment profile 存在 | 交易广播、实时 RPC 或 explorer 可达性、wallet 集成 |
| EVM 语义计划冒烟测试 | just evm-plan | 来自 lean-toolchain 的 Lean 工具链 | EVM semantic plan 会从 target 已解析的 CapabilityPlan 构建，拒绝非 EVM target plan，并在 Yul 生成前校验 storage layout、scalar storage slot、map value slot、nested map value slot、map presence slot、map assign-op helper 需求以及计划出的 helper 需求 | ABI dispatch、event、crosscall、constructor metadata、artifact metadata 完全归入 ModulePlan、solc 验收、字节码、运行时行为、更广泛的 aggregate storage planning |
| Solana light gates | just solana-light | 来自 lean-toolchain 的 Lean 工具链；python3；portable ValueVault EVM selector-hydration/Yul 分支可选依赖 cast；其 strict-assembly 与 EVM bytecode metadata 分支可选依赖 solc 加 cast；Solana SDK build 分支可选依赖 sbpf 和 solana-keygen | Solana target diagnostics、SDK metadata、SDK manifest、生成的 Solana IDL 与 TypeScript client artifacts、Counter 和 portable ValueVault 的 Contract Source Syntax v1 routing/render checks、Learn source lowering equivalence，以及针对 CPI/PDA/state helper 错误的 Learn reference diagnostics、typed account declaration metadata、CPI packing、log lowering、target routing、portable ValueVault Learn-source CLI emission 到 EVM Yul 与 Solana sBPF assembly/manifest/IDL/client artifact metadata、token spec、return-data/compute-units SDK helpers、Counter sBPF golden assembly/manifest diff、control-flow/assertion assembly emission、SDK extension artifact metadata、CI-safe Pinocchio System/SPL Token reference-equivalence suite，以及存在 sbpf 时的 canned sBPF emission | 完整 Mollusk runtime 覆盖、Surfpool/Web3 部署冒烟、公共 validator 部署、Solana transaction UX、live Pinocchio dual-deploy equivalence |
| Token SDK plan smoke | just learn-token-smoke | 来自 lean-toolchain 的 Lean 工具链；python3；EVM bytecode 分支可选依赖 solc；Web3.js validation 可选依赖 Node 和 npm | 验证 legacy .learn token 路径会进入 Lean TokenSpec 边界；存在 solc 时发射 ERC-20 Yul/bytecode metadata；发射结构化 Solana SPL Token 与 Token-2022 plan JSON；检查 mint/ATA/mint_to/transfer_checked/approve/burn/revoke/authority-change plan entry；检查 Token-2022 transfer-fee extension routing 和 withheld-fee collection plan entry；存在 Node/npm 时用 @solana/spl-token / @solana/web3.js instruction builder 离线验证 Solana plan | 所有 token plan variant 的 Surfpool live 执行、真实 token balance、公共 validator 部署、wallet UX、生成 wrapper/transfer-hook program |
| Solana token plan Surfpool/Web3.js smoke | just solana-token-plan-web3 | 来自 lean-toolchain 的 Lean 工具链；python3；surfpool；Solana CLI 和 solana-keygen；Node；npm | 发射结构化 SPL Token plan，启动 Surfpool，通过 @solana/spl-token 创建 mint 和 associated token account，mint initial supply，执行计划中的 mint_to、transfer_checked、approve、burn、revoke 和 mint-authority set_authority，再通过 Web3.js 读取验证 token balance、supply、delegate state 和 authority revoke | Token-2022 extension 行为、生成 wrapper/transfer-hook program、公共 validator 部署、wallet UX |
| Solana Token-2022 transfer-fee Surfpool/Web3.js smoke | just solana-token-2022-transfer-fee-web3 | 来自 lean-toolchain 的 Lean 工具链；python3；surfpool；Solana CLI 和 solana-keygen；Node；npm | 发射结构化 Token-2022 transfer-fee plan，启动 Surfpool，初始化带 TransferFeeConfig 的 mint，创建 Token-2022 associated token accounts，mint initial supply，执行 TransferCheckedWithFee，验证 source balance、recipient net balance 和 recipient withheld fee，直接从 token account withdraw withheld fee；然后执行第二次 transfer，harvest withheld fee 到 mint，再从 mint withdraw，并通过 Web3.js 验证 fee receiver balance 与已清空的 withheld amount | confidential transfer setup、transfer-hook routing、生成 wrapper/transfer-hook program、公共 validator 部署、wallet UX |
| Solana Token-2022 non-transferable Surfpool/Web3.js smoke | just solana-token-2022-non-transferable-web3 | 来自 lean-toolchain 的 Lean 工具链；python3；surfpool；Solana CLI 和 solana-keygen；Node；npm | 从 Lean .lean token fixture 发射结构化 Token-2022 plan，启动 Surfpool，初始化带 NonTransferable 的 mint，创建 Token-2022 associated token accounts，mint initial supply，验证 mint/account extension，证明 TransferChecked 会以 Transfer is disabled for this mint 被拒绝，然后 burn token 并验证 balance 与 supply | confidential transfer setup、transfer-hook routing、生成 wrapper/transfer-hook program、公共 validator 部署、wallet UX |
| Solana PDA Web3.js derivation smoke | just solana-pda-web3 | 来自 lean-toolchain 的 Lean 工具链；Node；npm | 发射 Solana SDK Vault artifact，读取 PDA typedSeeds，并用 @solana/web3.js 的 PublicKey.findProgramAddressSync 和 PublicKey.createProgramAddressSync 校验 literal/account/bump descriptor 语义；同时覆盖本地 UTF-8 与 instruction-parameter seed descriptor resolver | live deployment 或 transaction execution；SPL Token CPI 行为 |
| Solana System CPI Surfpool/Web3.js smoke | just solana-system-cpi-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 System Program transfer CPI ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用程序，验证 recipient lamports 按请求数增加，并验证 program-owned state account 记录了同一 lamports 值 | System create-account CPI、SPL Token CPI 行为、公共 validator 部署、Rust/Pinocchio 等价性 |
| Solana System create_account CPI Surfpool/Web3.js smoke | just solana-system-create-account-cpi-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 System Program create_account CPI ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用，验证新建 account 的 owner/space/lamports，并验证 program-owned state account 记录了请求的 lamports 和 space | SPL Token CPI 行为、公共 validator 部署、live Rust/Pinocchio 等价性 |
| Solana SPL Token transfer_checked CPI Surfpool/Web3.js smoke | just solana-spl-token-transfer-cpi-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 SPL Token transfer_checked CPI ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/spl-token 创建 mint 和 token accounts，通过 @solana/web3.js 调用生成程序，验证 source/destination token balance，并验证 program-owned state account 记录了请求的 amount | 更广泛的 SPL Token/Token-2022 覆盖、公共 validator 部署、live Rust/Pinocchio 等价性 |
| Solana SPL Token ops CPI Surfpool/Web3.js smoke | just solana-spl-token-ops-cpi-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 SPL Token mint_to/burn/approve/revoke CPI ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/spl-token 创建 mint 和 token accounts，通过 @solana/web3.js 调用生成程序，验证 mint supply 与 token balance 变化，验证 delegate allowance 后再 revoke 清空，并验证 program-owned state account 记录所有请求值 | Token-2022 extension 行为、公共 validator 部署 |
| Solana SPL Token authority CPI Surfpool/Web3.js smoke | just solana-spl-token-authority-cpi-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 SPL Token set_authority CPI ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/spl-token 创建 mint，通过 @solana/web3.js 调用生成程序，验证 mint authority 已转移到请求的新 authority，并验证 program-owned state account 记录 marker | Token-2022 extension 行为、公共 validator 部署 |
| Solana Pinocchio reference-equivalence suite | just solana-pinocchio-reference-equivalence | 来自 lean-toolchain 的 Lean 工具链；python3；设置 PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 时可选依赖 cargo | 运行下面五个 CI-safe Pinocchio reference-equivalence smoke，并已纳入 just solana-light / 默认 CI build-test job | live dual-deploy equivalence、Pinocchio reference ELF 构建 |
| Solana Pinocchio System transfer reference-equivalence smoke | just solana-pinocchio-system-transfer-equivalence | 来自 lean-toolchain 的 Lean 工具链；python3；设置 PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 时可选依赖 cargo | emit 生成的 System Program transfer CPI source/artifact metadata，并将 instruction ABI、account order、signer/writable requirement、CPI metadata 和 lamports state write contract 与 references/solana/pinocchio/system-transfer 下 checked-in Pinocchio reference manifest/source 对比 | 构建/部署 Pinocchio reference ELF，并让 ProofForge/reference programs 通过同一个 Web3.js harness 对比 |
| Solana Pinocchio System create_account reference-equivalence smoke | just solana-pinocchio-system-create-account-equivalence | 来自 lean-toolchain 的 Lean 工具链；python3；设置 PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 时可选依赖 cargo | emit 生成的 System Program create_account CPI source/artifact metadata，并将 instruction ABI、account order、signer/writable requirement、CPI metadata、lamports/space/owner layout 和双字段 state-write contract 与 references/solana/pinocchio/system-create-account 下 checked-in Pinocchio reference manifest/source 对比；可选 Cargo check 会用 pinocchio-system typecheck 该 reference | 构建/部署 Pinocchio create_account reference ELF，并让 ProofForge/reference programs 通过同一个 Web3.js harness 对比 |
| Solana Pinocchio SPL Token transfer reference-equivalence smoke | just solana-pinocchio-spl-token-transfer-equivalence | 来自 lean-toolchain 的 Lean 工具链；python3；设置 PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 时可选依赖 cargo | emit 生成的 SPL Token transfer_checked CPI source/artifact metadata，并将 instruction ABI、account order、signer/writable requirement、CPI metadata、decimals/amount layout 和 amount state-write contract 与 references/solana/pinocchio/spl-token-transfer 下 checked-in Pinocchio reference manifest/source 对比；可选 Cargo check 会用 pinocchio-token typecheck 该 reference | 构建/部署 Pinocchio SPL Token reference ELF，并让 ProofForge/reference programs 通过同一个 Web3.js harness 对比 |
| Solana Pinocchio SPL Token ops reference-equivalence smoke | just solana-pinocchio-spl-token-ops-equivalence | 来自 lean-toolchain 的 Lean 工具链；python3；设置 PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 时可选依赖 cargo | emit 生成的 SPL Token mint_to/burn/approve/revoke CPI source/artifact metadata，并将四个 instruction ABI、共享 account order、signer/writable requirement、CPI metadata、SPL Token instruction layout 和 state-write contract 与 references/solana/pinocchio/spl-token-ops 下 checked-in Pinocchio reference manifest/source 对比；可选 Cargo check 会用 pinocchio-token typecheck 该 reference | 构建/部署 Pinocchio SPL Token ops reference ELF，并让 ProofForge/reference programs 通过同一个 Web3.js harness 对比 |
| Solana Pinocchio SPL Token authority reference-equivalence smoke | just solana-pinocchio-spl-token-authority-equivalence | 来自 lean-toolchain 的 Lean 工具链；python3；设置 PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 时可选依赖 cargo | emit 生成的 SPL Token set_authority CPI source/artifact metadata，并将 instruction ABI、account order、signer/writable requirement、CPI metadata、SetAuthority instruction layout 和 marker state-write contract 与 references/solana/pinocchio/spl-token-authority 下 checked-in Pinocchio reference manifest/source 对比；可选 Cargo check 会用 pinocchio-token typecheck 该 reference | 构建/部署 Pinocchio SPL Token authority reference ELF，并让 ProofForge/reference programs 通过同一个 Web3.js harness 对比 |
| Solana Pinocchio System transfer live-equivalence smoke | just solana-pinocchio-system-transfer-live-equivalence | 来自 lean-toolchain 的 Lean 工具链；带 Solana rustc/platform-tools 的 cargo-build-sbf；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建 ProofForge System transfer CPI ELF 和 checked-in Pinocchio reference ELF，将两个程序部署到同一个 Surfpool instance，用同一个 Web3.js transfer scenario 分别调用，并对比 recipient lamport delta 和 state 记录值 | 在 Solana rustc 可稳定安装后纳入 CI；将 Pinocchio 对比扩展到 Token-2022 和更广 SPL helper 覆盖；just solana-pinocchio-install-sbf-tools 可修复缺失/损坏的 platform-tools |
| Solana Pinocchio System create_account live-equivalence smoke | just solana-pinocchio-system-create-account-live-equivalence | 来自 lean-toolchain 的 Lean 工具链；带 Solana rustc/platform-tools 的 cargo-build-sbf；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建 ProofForge System create_account CPI ELF 和 checked-in Pinocchio reference ELF，将两个程序部署到同一个 Surfpool instance，用同一个 Web3.js create-account scenario 分别调用，并对比 lamports/space 以及 state 记录值 | 在 Solana rustc 可稳定安装后纳入 CI；将 Pinocchio 对比扩展到 Token-2022 和更广 SPL helper 覆盖；just solana-pinocchio-install-sbf-tools 可修复缺失/损坏的 platform-tools |
| Solana Pinocchio SPL Token transfer live-equivalence smoke | just solana-pinocchio-spl-token-transfer-live-equivalence | 来自 lean-toolchain 的 Lean 工具链；带 Solana rustc/platform-tools 的 cargo-build-sbf；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建 ProofForge SPL Token transfer_checked CPI ELF 和 checked-in Pinocchio reference ELF，将两个程序部署到同一个 Surfpool instance，用同一个 Web3.js token-transfer scenario 分别调用，并对比 token balance delta 和 state 记录值 | 在 Solana rustc 可稳定安装后纳入 CI；将 Pinocchio 对比扩展到 Token-2022 和更广 SPL helper 覆盖；just solana-pinocchio-install-sbf-tools 可修复缺失/损坏的 platform-tools |
| Solana Pinocchio SPL Token ops live-equivalence smoke | just solana-pinocchio-spl-token-ops-live-equivalence | 来自 lean-toolchain 的 Lean 工具链；带 Solana rustc/platform-tools 的 cargo-build-sbf；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建 ProofForge SPL Token mint_to/burn/approve/revoke CPI ELF 和 checked-in Pinocchio reference ELF，将两个程序部署到同一个 Surfpool instance，用同一个 Web3.js token-ops scenario 分别调用，并对比 mint/burn/approve/revoke token effect 和 state 记录值 | 在 Solana rustc 可稳定安装后纳入 CI；将 Pinocchio 对比扩展到 Token-2022 和剩余 SPL helper 覆盖；just solana-pinocchio-install-sbf-tools 可修复缺失/损坏的 platform-tools |
| Solana Pinocchio SPL Token authority live-equivalence smoke | just solana-pinocchio-spl-token-authority-live-equivalence | 来自 lean-toolchain 的 Lean 工具链；带 Solana rustc/platform-tools 的 cargo-build-sbf；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建 ProofForge SPL Token set_authority CPI ELF 和 checked-in Pinocchio reference ELF，将两个程序部署到同一个 Surfpool instance，用同一个 Web3.js mint-authority transfer scenario 分别调用，并对比 mint authority 与 state marker | 在 Solana rustc 可稳定安装后纳入 CI；将 Pinocchio 对比扩展到 Token-2022 和剩余 SPL helper 覆盖；just solana-pinocchio-install-sbf-tools 可修复缺失/损坏的 platform-tools |
| Solana log/event Surfpool/Web3.js smoke | just solana-log-event-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 events.emit/Solana log-extension ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用生成程序，验证 sol_log_64_ transaction logs 包含稳定 event tag 和 scalar field value，验证 program-owned state account 记录了同一个值，验证 sol_log_pubkey 会记录 state account 的 base58 pubkey，并验证 sol_log_data 会为 state bytes 产出 base64 Program data: payload | Anchor-compatible discriminator/Borsh event serialization、indexed events、sol_log_ payload、历史索引保证 |
| Solana Clock sysvar Surfpool/Web3.js smoke | just solana-clock-sysvar-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 contextRead checkpointId ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用生成程序，验证 sol_get_clock_sysvar 将 Clock.slot 记录进 program-owned state，并与 transaction slot metadata 对比 | 更丰富的 Clock fields、公共 validator 部署 |
| Solana Rent sysvar Surfpool/Web3.js smoke | just solana-rent-sysvar-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 Solana-only sysvar target-extension ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用生成程序，验证 sol_get_rent_sysvar 将 Rent.lamports_per_byte_year 记录进 program-owned state，并与 Rent sysvar account data 对比 | 更多 Rent fields、公共 validator 部署 |
| Solana EpochSchedule sysvar Surfpool/Web3.js smoke | just solana-epoch-schedule-sysvar-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 Solana-only sysvar target-extension ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用生成程序，验证 sol_get_epoch_schedule_sysvar 将当前 RPC 暴露的 5 个 EpochSchedule 字段记录进 program-owned state，并与 RPC getEpochSchedule() 对比 | 更多 Clock/Rent 字段、generic account-passed sysvar 读取、公共 validator 部署 |
| Solana EpochRewards sysvar Surfpool/Web3.js smoke | just solana-epoch-rewards-sysvar-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 Solana-only sysvar target-extension ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用生成程序，验证 sol_get_epoch_rewards_sysvar 将当前 EpochRewards scalar/word-view 字段记录进 program-owned state，并与 EpochRewards sysvar account data 对比 | 更多 Clock/Rent 字段、generic account-passed sysvar 读取、公共 validator 部署 |
| Solana LastRestartSlot sysvar Surfpool/Web3.js smoke | just solana-last-restart-slot-sysvar-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 Solana-only sysvar target-extension ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用生成程序，验证 feature-gated LastRestartSlot.last_restart_slot 读取已通过 sol_get_sysvar lowering，并与 LastRestartSlot sysvar account data 对比 | 其他 sysvars、公共 validator 部署、cluster feature activation 差异 |
| Solana memory syscall Surfpool/Web3.js smoke | just solana-memory-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 runtime.memory ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用 set_source 和 copy_compare_fill，并验证 program-owned account bytes 证明 sol_memcpy_、sol_memmove_、sol_memcmp_ 和 sol_memset_ 已执行 | 更广泛的 account/data packing helper、Rust/Pinocchio 等价性 |
| Solana return-data/compute Surfpool/Web3.js smoke | just solana-return-data-compute-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 runtime.return_data/runtime.compute_units ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用，借助 simulation returnData 验证 sol_set_return_data，通过 empty read 与同一条 instruction 内 set/get roundtrip 验证 sol_get_return_data，验证 sol_remaining_compute_units 写入非零 state value，并验证 sol_log_compute_units_ 产出 compute-unit log | CPI return-value 处理、u64 之外的 typed return payload、public-validator feature 差异 |
| Solana SHA-256/Keccak-256/Blake3 syscall Surfpool/Web3.js smoke | just solana-crypto-hash-web3 | 来自 lean-toolchain 的 Lean 工具链；surfpool；Solana CLI 和 solana-keygen；sbpf；Node；npm | 构建生成的 Solana-only crypto.hash ELF，启动 Surfpool，用 solana program deploy --use-rpc 部署，通过 @solana/web3.js 调用 set_preimage、hash_preimage、keccak_preimage 和 blake3_preimage，并验证 account 中保存的 digest 与同一 preimage bytes 的 Node SHA-256 和 @noble/hashes Keccak-256/Blake3 一致 | portable Expr.hash 路由、Rust/Pinocchio 等价性 |
| Yul 生成冒烟测试 | lake env proof-forge --root . -o build/counter.yul Examples/Evm/Contracts/Counter.lean | 已构建 proof-forge | Lean 前端/LCNF 将简单合约降级为 Yul | solc 验收、ABI 调度、EVM 运行时行为 |
| Yul 到字节码冒烟测试 | solc --strict-assembly build/counter.yul --bin | PATH 上的 solc | 生成的 Yul 被 solc 接受 | 运行时语义或方法调度 |
| 单个 EVM 字节码编译 | lake env proof-forge --evm-bytecode --root . --module contract --artifact-output build/evm/Counter.proof-forge-artifact.json -o build/evm/Counter.bin Examples/Evm/Contracts/Counter.lean | solc、cast、python3 和 Examples/Evm/Contracts/Counter.evm-methods | Lean -> Yul -> solc -> 带有选择器生成的 runtime bytecode、可部署 .init.bin creation bytecode、proof-forge-artifact.json metadata，以及 proof-forge-deploy.json initcode manifest；manifest 中的 initcode header 会复制并返回引用的 runtime bytecode；--evm-chain-profile <id> 还会把已知 EVM chain profile 写入 deploy manifest，但不广播交易；--evm-constructor-param <name:type> 会记录静态 word constructor ABI schema；--evm-constructor-arg <name=value> 会 ABI-encode 支持的静态 word typed value；--evm-constructor-args-hex <hex> 会记录并追加一段 ABI-encoded constructor-argument tail | 运行时行为、gas、详尽的 ABI 正确性、dynamic constructor ABI types、签名/原始交易生成、真实交易广播 |
| EVM 示例编译 | scripts/evm/build-examples.sh | cast、solc、python3、lake env proof-forge；可选 PROOF_FORGE_BIN、CONTRACTS_DIR、EVM_OUT_DIR | 每个带有兄弟 .evm-methods 的 .lean 合约都编译为可复现 Yul、.bin 和 .init.bin，diff 生成的 Yul 与已跟踪的 SDK 示例 golden fixture，并校验 EVM metadata hash、initcode hash/header/runtime 关联、deploy-manifest hash、source/module 信息、solc 信息、SDK method selector/function，以及必需的 Solidity method signature | 运行时行为；没有 .evm-methods 的合约会被脚本跳过 |
| Learn token ERC-20 VM 冒烟测试 | just learn-token-evm-vm | 来自 lean-toolchain 的 Lean 工具链；solc；Node；npm | 解析 Examples/Learn/ProofToken.learn，通过 proof-forge --learn-token --target evm 发射 ERC-20 Yul、creation bytecode 和 artifact metadata，在 EthereumJS VM 中部署生成的 creation bytecode，然后验证 totalSupply、decimals、balanceOf、transfer、approve、allowance、transferFrom、可选 burn、可选 mint、Transfer/Approval topic，以及余额不足时的 revert 行为 | live RPC 部署、gas accounting、wallet UX、更强的 mint access-control policy |
| EVM 运行时冒烟测试 | scripts/evm/foundry-smoke.sh | forge、cast、solc；可选 EVM_OUT_DIR、EVM_FORGE_DIR | Foundry 执行为 Counter、ArrayExample、SimpleToken 和 VerifiedVault 生成的 runtime bytecode，也会通过 EVM create 执行生成的 Counter .init.bin，并包含 revert 检查 | 形式化证明覆盖、跨目标等效性、实时 RPC 部署、详尽的边界覆盖 |
| EVM Anvil 部署冒烟测试 | scripts/evm/anvil-deploy-smoke.sh | anvil、cast、solc、python3；可选 EVM_ANVIL_CHAIN_ID、EVM_ANVIL_CHAIN_PROFILE、EVM_ANVIL_PORT、EVM_ANVIL_RUN_DIR、EVM_ANVIL_CONSTRUCTOR_ARG、EVM_ANVIL_CONSTRUCTOR_ARGS_HEX、EVM_ANVIL_CONSTRUCTOR_PARAM | 启动本地 Anvil 链，默认用 deterministic typed initial=123 constructor input、initial:uint256 constructor ABI schema，以及 chain id 31337 的 anvil-local chain profile 重新生成 Counter initcode，校验带 signature 的 Counter method metadata 和带 profile 的 deploy metadata，通过 cast send --create 部署生成的 Counter .init.bin，在 Counter.proof-forge-deploy-run.json 中记录 constructor ABI schema、constructor args、creation receipt、creation transaction JSON、chain profile 和 deployed address，验证 creation transaction input 等于生成的 initcode，验证 profile chain id 匹配实际本地链，验证 deployed runtime code 等于 Counter.bin，通过 JSON-RPC 运行 Counter get/set/increment/decrement，并用 scripts/evm/validate-deploy-run.py 校验 deploy-run artifact | live public RPC 部署、explorer verification、wallet UX、dynamic constructor ABI types、长期运行链状态 |
| EVM ABI ScalarProbe IR 冒烟测试 | scripts/evm/abi-scalar-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR U64、U32 和 Bool ABI 参数降级为 Yul 函数参数和 dispatcher calldata load，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 selector entrypoints 与 Yul/bytecode hash 的 EVM metadata，校验 robinhood-chain-testnet、chain id 46630 的 chain-profile-aware deploy manifest，并通过 Foundry 校验有效调用和 malformed calldata revert | 聚合 ABI 参数/返回、storage 行为、实时 RPC 部署 |
| EVM AssertProbe IR 冒烟测试 | scripts/evm/assert-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR assert 和 assert_eq 降级为 Yul revert guard，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 assertions.check 的 EVM metadata，并通过 Foundry 校验成功路径和断言失败 revert | 丰富 revert data、表达式类型检查 |
| EVM AssignmentProbe IR 冒烟测试 | scripts/evm/assignment-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 可变标量 local 和 local assignment 降级为 Yul let 与 :=，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验 selector entrypoints 与 artifact hash metadata，并通过 Foundry 校验赋值结果和 bool guard 失败 revert | 聚合赋值路径、storage path 赋值路径 |
| EVM AssignOpProbe IR 冒烟测试 | scripts/evm/assign-op-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 复合赋值支持可变 U32/U64 local 和 U64 标量 storage，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 storage.scalar 的 EVM metadata，通过 Foundry 校验 U64/U32 返回值，并用 vm.load 校验原始标量 storage，同时验证未知 selector revert | 聚合赋值 target、raw EVM word 操作之外的 checked overflow 语义 |
| EVM ConditionalProbe IR 冒烟测试 | scripts/evm/conditional-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 语句级 if/else 降级为 Yul switch block，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 storage.scalar、control.conditional、assertions.check 的 EVM metadata，并通过 Foundry 校验 then/else storage 更新结果和未知 selector revert；分支内早退由 EvmLoopProbe 覆盖 | 更多控制流分析 |
| EVM LoopProbe IR 冒烟测试 | scripts/evm/loop-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR boundedFor 降为带静态边界的 Yul for loop，分支内和 loop 内早退会降为返回值赋值后跟 Yul leave；生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 生成 runtime bytecode，metadata 包含 storage.scalar、control.conditional 和 control.bounded_loop，Foundry 校验 loop 更新后的 storage、原始 storage slot、早退返回值/effect，以及未知 selector revert | 动态 loop 边界、break/continue、更多控制流分析 |
| EVM ContextProbe IR 冒烟测试 | scripts/evm/context-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR context read 降级为 Yul caller()、address() 和 number()，nativeValue 降级为 Yul callvalue()，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 caller.sender、account.explicit、env.block、value.native 的 EVM metadata，并通过 Foundry vm.prank/vm.roll 校验运行时 context 值、通过 probe.call{value: ...} 校验原生 value 和未知 selector revert | 当前 portable userId/contractId/checkpointId 之外的 context 字段、地址宽度类型校验 |
| EVM EventProbe IR 冒烟测试 | scripts/evm/event-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR eventEmit 降为 Yul log1，eventEmitIndexed 降为 Yul log2/log3/log4，其中 topic0 = keccak256(Solidity-style event signature)，U64/Bool/U32/Hash indexed scalar field 进入 topic，U64/Bool/U32/Hash scalar 非 indexed field 进入 32-byte word data，扁平 struct / scalar fixed-array / fixed-array-of-flat-struct 非 indexed field 会从 local value 和 storage read 展开为 ABI-style data word，支持的 aggregate indexed field 会对展开后的 ABI-style word 执行 keccak256 作为 topic；生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 生成 runtime bytecode，metadata 包含 events.emit，并校验 abi.events 中的 signature、topic0、indexed/data field、展开后的 word type 和 topic/data encoding，Foundry recorded logs 校验 emitter/topic/data，包括 TypedScalarEvent(bool,uint32,bytes32)、PairEvent((uint64,uint64))、StoragePairEvent((uint64,uint64))、StorageArrayEvent(uint64[2])、ArrayEvent(uint64[2])、PairArrayEvent((uint64,uint64)[2])、StoragePairArrayEvent((uint64,uint64)[2])、IndexedTypedScalar(bool,uint32,bytes32,uint64)、IndexedPair((uint64,uint64),uint64)、IndexedStoragePair((uint64,uint64),uint64)、IndexedTwoValues(uint64,uint64,uint64)、IndexedThreeValues(uint64,uint64,uint64,uint64)、IndexedStorageArray(uint64[2],uint64)、IndexedArray(uint64[2],uint64)、IndexedStoragePairArray((uint64,uint64)[2],uint64) 和 IndexedPairArray((uint64,uint64)[2],uint64)，并验证 malformed Bool/U32 calldata 和未知 selector revert | 更完整的 event declaration、不支持的嵌套 aggregate indexed shape、超过 3 个 topic 的 indexed field |
| EVM CrosscallProbe IR 冒烟测试 | scripts/evm/crosscall-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR crosscallInvoke、crosscallInvokeTyped、crosscallInvokeValueTyped、crosscallInvokeStaticTyped、crosscallInvokeDelegateTyped、crosscallCreate 和 crosscallCreate2 降为按 arity、返回类型、value 模式、static 模式、delegate 模式和 creation 模式区分的 Yul helper，打包 selector/scalar-word、扁平 aggregate，以及 leaf 为 scalar word 或扁平 struct 的嵌套 fixed-array 参数，执行同步 EVM call、staticcall、delegatecall、create 或 create2，可选转发 U64 call value，在调用失败、返回数据过短或 creation 返回零地址时 revert，解码 scalar 和 entrypoint 直接返回的 aggregate return word，对 scalar 与 aggregate 返回中的 Bool/U32 word 做范围 guard，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 crosscall.invoke 和所有 CrosscallProbe entrypoint 的 EVM metadata，并通过 Foundry 校验 U64 零/一/二参数调用、Bool/U32/Hash typed 调用、扁平 struct/scalar fixed-array/fixed-array-of-flat-struct/leaf 为 scalar 或扁平 struct 的 nested fixed-array typed-call 参数、normal/value/static/delegate 模式下扁平 struct/scalar fixed-array/fixed-array-of-flat-struct/leaf 为 scalar 或扁平 struct 的 nested fixed-array aggregate typed return、normal/value/static/delegate 模式下的 aggregate Bool/U32 malformed-return guard、native value 转发到 payable callee、带 value 的扁平和嵌套 scalar/flat-struct aggregate 参数、U64 read-only staticcall 返回、Bool/U32/Hash static typed return、static 扁平和嵌套 scalar/flat-struct aggregate 参数、非法 static Bool/U32 return guard、static context 状态写入失败、caller-storage delegatecall 读写、Bool/U32/Hash delegate typed return、delegate 扁平和嵌套 scalar/flat-struct aggregate 参数、非法 delegate Bool/U32 return guard、固定 init-code create 部署、确定性 create2 地址校验、deployed-runtime 调用、非法 typed return 和 revert 路径 | Artifact-linked creation code、动态 constructor 参数、非扁平 nested aggregate leaf、variable-length 返回数据 |
| EVM ExpressionProbe IR 冒烟测试 | scripts/evm/expression-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR scalar expression 直接降为 Yul，覆盖 U64/U32 arithmetic、U64 exponentiation、U64/U32 bitwise 和 shift、predicate、boolean operator、scalar literal、不可变 local read、支持的 cast、单 word return 和 assertion guard；生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 编译，metadata 包含 assertions.check，Foundry 校验运行时返回值、U32/Bool calldata guard、malformed calldata revert 和未知 selector revert | raw EVM word operation 之外的 checked overflow 语义、array/struct/ABI probe 覆盖的聚合 expression |
| EVM HashProbe IR 冒烟测试 | scripts/evm/hash-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR Hash 值降为单 word EVM bytes32 ABI/storage 值，hash4 与 hashValue 将四个 limb 打包为一个 word，hash 与 hash_two_to_one 降为 Yul keccak256 helper，生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 生成 bytecode，metadata 包含 crypto.hash 和 storage.scalar，Foundry 校验 ABI bytes32 参数/返回与原始标量 storage slot，并验证未知 selector revert | 聚合 hash 输入、地址宽度类型校验 |
| EVM MapProbe IR 冒烟测试 | scripts/evm/map-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR Map<U64, U64, N> storage 通过 Solidity-style keccak256(key, slot) value mapping slot 和 ProofForge 管理的 contains presence slot 降级，匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 storage.scalar、storage.map、assertions.check 的 EVM metadata，并通过 Foundry 校验 get/set/insert/contains 返回值、value 为零但 present 的 key、单段和嵌套连续 mapKey storage path 的 read、write 和复合赋值、vm.load 原始 value/presence slot 和未知 selector revert | typed word map 由 EvmTypedMapProbe 覆盖、array/struct storage path、混合 map/aggregate storage path |
| EVM TypedMapProbe IR 冒烟测试 | scripts/evm/typed-map-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR Map<K, V, N> storage 对 word key/value 类型（U32、Bool、Hash 和已有 U64）通过 Solidity-style keccak256(key, slot) value mapping slot 和 ProofForge 管理的 contains presence slot 降级；生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 编译，metadata 包含 storage.scalar、storage.map 和 assertions.check，Foundry 校验 U32/Bool/Hash map read/write、typed contains、previous-value return、原始 value/presence mapping slot、U32/Bool calldata guard、单段 mapKey storage-path read/write、U32 map-path 复合赋值、带 dispatcher range guard 的 U32 嵌套 mapKey path read/write/复合赋值，以及未知 selector revert | 非 word 或 aggregate map key/value 形态、混合 map/aggregate storage path |
| EVM StorageArrayProbe IR 冒烟测试 | scripts/evm/storage-array-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR U64 固定 storage array 降为连续 EVM storage slot，并带运行时 index bounds check；单段 index storage path 会降为同一个 slot helper，用于 read/write/compound assignment；fixed-array ABI return 可以由 storage element read 组装；匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 storage.scalar、storage.array、data.fixed_array 的 EVM metadata，并通过 Foundry 校验 lifecycle/read/write/path/aggregate 返回值、vm.load 原始 slot layout、越界 index revert 和未知 selector revert | U32/Bool/Hash storage array 由 EvmTypedStorageProbe 覆盖、local fixed-array value 和更广的聚合 ABI 行为由 EvmAbiAggregateProbe 覆盖、嵌套 index storage path、struct |
| EVM TypedStorageProbe IR 冒烟测试 | scripts/evm/typed-storage-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR Bool scalar storage 和 U32/Bool/Hash 固定 storage array 降为连续 EVM word slot，并带运行时 index bounds check；生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 编译，metadata 包含 storage.scalar、storage.array、data.fixed_array 和 assertions.check，Foundry 校验原始 slot layout、ABI Bool/Hash 返回、U32 calldata range guard、typed storage-path read/write、U32 storage-path 复合赋值、越界 revert 和未知 selector | 非 word storage 元素、嵌套 index storage path、struct array 由 EvmStorageStructProbe 覆盖、typed map 由 EvmTypedMapProbe 覆盖 |
| EVM StorageStructProbe IR 冒烟测试 | scripts/evm/storage-struct-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 扁平 scalar storage struct 降为每字段一个 EVM slot，whole scalar storage struct read/write 会展开到这些字段 slot，并且 whole write 会快照 RHS 字段；扁平 struct 固定 storage array 降为连续字段展开 slot 并带运行时 index bounds check；scalar field 和 array index+field storage path 会降为同一 slot 公式用于 read/write/compound assignment；fixed-array-of-flat-struct ABI return 可以由 storage field read 组装；生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 编译，metadata 包含 storage.scalar、storage.array、data.fixed_array 和 data.struct，Foundry 校验 U64/Bool/U32/Hash 字段、whole storage struct read/write、storage-backed ABI struct return、storage-backed fixed-array-of-struct return、原始 slot layout、越界 revert 和未知 selector | 嵌套 struct field、非扁平 struct storage |
| EVM ArrayValueProbe IR 冒烟测试 | scripts/evm/array-value-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 不可变和可变 local fixed-array value 会降为每个元素一个 Yul local；fixed-array literal 以及静态/动态 index read 可确定性 lowering；静态/动态 local 元素赋值和数字复合赋值会更新展开后的 local；静态和动态嵌套 scalar local fixed-array read 会降为确定性 leaf local 和 nested getter helper；静态和动态嵌套 scalar leaf 赋值/复合赋值会降为直接赋值或嵌套 switch block；whole-local 和 whole-nested fixed-array assignment 会先快照 RHS 元素再写回；匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 data.fixed_array 和 assertions.check 的 EVM metadata，并通过 Foundry 校验 U64/U32/Bool/Hash 返回值、可变元素写入、嵌套动态读写越界 revert 和未知 selector revert | ABI 聚合行为由 EvmAbiAggregateProbe 覆盖、leaf 非 scalar 的嵌套 array |
| EVM StructArrayValueProbe IR 冒烟测试 | scripts/evm/struct-array-value-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 扁平 struct local fixed array 会降为每个 element field 一个 Yul local；field(arrayGet(localArray, index), name) 支持静态和动态字段读取；可变 struct-array 字段赋值和数字复合赋值会通过静态赋值或动态 switch 更新展开后的 local；从另一个 local struct array 或 struct-array literal 做 whole local assignment 时，会先快照 RHS 字段再写回目标字段；匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，metadata 包含 data.fixed_array、data.struct 和 assertions.check，Foundry 校验 U64/U32/Bool/Hash-backed 返回值、自引用 RHS 快照行为、动态越界 index revert 和未知 selector revert | 嵌套 array、嵌套 struct、ABI 聚合行为由 EvmAbiAggregateProbe 覆盖 |
| EVM StructValueProbe IR 冒烟测试 | scripts/evm/struct-value-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 扁平不可变和可变 local struct value 会降为每个字段一个 Yul local；struct literal 和 field access 针对 U64/U32/Bool/Hash 字段可确定性 lowering；静态 local 字段赋值和数字复合赋值会更新展开后的 local；whole-local struct assignment 会先快照 RHS 字段再写回；匹配 golden Yul，通过 solc --strict-assembly 生成 runtime bytecode，校验包含 data.struct 和 assertions.check 的 EVM metadata，并通过 Foundry 校验 U64/U32/Bool/Hash 返回值、可变字段写入和未知 selector revert | 嵌套 struct、storage struct 行为由 EvmStorageStructProbe 覆盖、ABI 聚合行为由 EvmAbiAggregateProbe 覆盖、struct array |
| EVM AbiAggregateProbe IR 冒烟测试 | scripts/evm/abi-aggregate-ir-smoke.sh | forge、solc、python3、来自 lean-toolchain 的 Lean 工具链 | Portable IR 扁平静态 struct、fixed-array 和嵌套标量 fixed-array ABI 参数会展开为连续 calldata word，扁平 struct fixed array 会按 tuple-array ABI word 展开，U32 和 Bool 聚合 word 会带 dispatcher range guard，Hash 聚合 leaf 会在扁平 struct 和 fixed array 内降为 Solidity bytes32 word，扁平 struct/fixed-array 返回（包括嵌套标量 fixed array、扁平 struct fixed array、HashPair struct 和 Hash fixed array）会编码为多 word ABI return data；生成的 Yul 匹配 golden fixture，通过 solc --strict-assembly 编译，metadata 包含 data.fixed_array、data.struct 和结构化 abi.entrypoints selector signature 及 calldata/return word layout，并通过 cast sig 和 --expect-entrypoint-abi 校验；Foundry 校验聚合调用/返回、包括短 bytes32[2] calldata 在内的 malformed calldata revert，以及未知 selector revert | 动态聚合 ABI 值、超出 EvmStorageArrayProbe 和 EvmStorageStructProbe 已覆盖的固定 word array 与扁平 struct array 的更广 storage-backed aggregate ABI return、超出扁平 word 聚合的复杂 ABI tuple；typed crosscall aggregate 行为由 EvmCrosscallProbe 覆盖 |
| EVM 诊断冒烟测试 | scripts/evm/diagnostic-smoke.sh | 来自 lean-toolchain 的 Lean 工具链 | 不支持或格式错误的 EVM IR 形态在 Yul 生成前以显式诊断失败，包括缺少 selector、Unit/零长度 array 和非扁平 struct field 等不支持 ABI 值、控制流路径缺少返回、Hash/U64 类型错配、array/struct/event surface、无效 bounded-loop 范围、crosscall target/method/argument 类型错误、typed crosscall 参数/返回中 leaf 为非扁平 struct 的嵌套 fixed-array 不支持、带 value crosscall 的 call value/return 类型错误以及 leaf 为非扁平 struct 的嵌套 fixed-array 不支持、static/delegate crosscall 中 leaf 为非扁平 struct 的嵌套 fixed-array 不支持、create/create2 value、salt 和 init-code hex 格式错误、不支持的 map 形态、statement 位置的 contains、格式错误的赋值/复合赋值类型和 target、storage path 复合赋值的表达式位置/嵌套路径误用，以及 effect 表达式/语句位置误用（包括 statement 位置的 context read）。它还会检查 EVM constructor CLI 诊断，包括不支持的 dynamic ABI type、缺失或重复的 typed value、typed/raw constructor argument source 混用、整数溢出，以及 address 过短等格式错误的 static-word value。 | 完整 unsupported surface 覆盖、solc 行为、Foundry 运行时行为、制品 metadata |
| EVM IR 覆盖清单 | scripts/evm/check-ir-coverage-manifest.py | python3 | Tests/EvmCoverage.tsv 为 ProofForge/IR/Contract.lean 中每个 portable IR constructor 记录 EVM 是否 lowered、validated、unsupported 或 structural | 行为正确性、solc 行为、Foundry 运行时行为、制品生成 |
| Psy Counter IR 冒烟测试 | scripts/psy/counter-smoke.sh | PATH 上的 dargo；python3；macOS arm64 上 psyup install 0.1.0 已知可用 | Counter portable IR 降级为 .psy，匹配 golden fixture，通过 dargo test --file，通过 dargo compile 生成非空 DPN JSON，通过 dargo execute 返回 result_vm: [2]，生成非空 ABI JSON，写出 proof-forge-deploy.json，并在 proof-forge-artifact.json 中记录和校验 metadata/deploy manifest 的 hash、能力和执行结果 | 上游压缩 genesis deploy JSON、真实 Psy node/prover 行为、更广泛 IR 覆盖 |
| Psy ContextProbe IR 冒烟测试 | scripts/psy/context-smoke.sh | PATH 上的 dargo；python3；macOS arm64 上 psyup install 0.1.0 已知可用 | 非 Counter Psy IR 降级参数和 context reads，匹配 golden fixture，通过 dargo test --file，生成非空 DPN JSON 和 ABI JSON，通过 dargo execute 返回 result_vm: [15]，写出 proof-forge-deploy.json，并在 proof-forge-artifact.json 中记录和校验 metadata/deploy manifest | maps、arrays、hashes、上游压缩 genesis deploy JSON、真实 Psy node/prover 行为 |
| Psy HashProbe IR 冒烟测试 | scripts/psy/hash-smoke.sh | PATH 上的 dargo；python3；macOS arm64 上 psyup install 0.1.0 已知可用 | Psy IR 将 Hash、typed hash let-bindings、hash 和 hash_two_to_one 降级为 .psy，匹配 golden fixture，通过 dargo test --file，生成非空 DPN JSON 和 ABI JSON，通过 dargo execute 返回预期四 Felt hash 输出，写出 proof-forge-deploy.json，并在 proof-forge-artifact.json 中记录和校验 metadata/deploy manifest | maps、storage maps、上游压缩 genesis deploy JSON、真实 Psy node/prover 行为 |
| CI 基线 | .github/workflows/ci.yml build-test 任务 | GitHub Actions Ubuntu、just 1.48.0、elan、Foundry stable、solc 0.8.30 | 清洁环境下的 just build、just target-registry、just evm-plan、just solana-light、just docs-check、Wasm-NEAR 诊断冒烟、Wasm-NEAR/EmitWat IR 覆盖清单、IR ownership 规则、Wasm-NEAR 形式语义锚点、EmitWat offline host 冒烟、just psy-golden-sources、Psy 诊断、Psy IR 覆盖清单、EVM 诊断、EVM IR 覆盖清单、EVM ABI ScalarProbe/AssertProbe/AssignmentProbe/AssignOpProbe/ConditionalProbe/LoopProbe/ContextProbe/EventProbe/CrosscallProbe/ExpressionProbe/HashProbe/MapProbe/TypedMapProbe/StorageArrayProbe/StorageStructProbe/TypedStorageProbe/ArrayValueProbe/StructArrayValueProbe/StructValueProbe/AbiAggregateProbe IR 冒烟测试、EVM metadata/deploy-manifest 校验、EVM 编译、Foundry 冒烟测试和 Anvil deploy smoke。CI 会保留独立的 GitHub Actions 步骤用于定位失败，但每个常见门禁都通过根目录 justfile recipe 调用。 | 可选 Dargo 目标冒烟测试、非 Ubuntu 行为 |
| Aleo Counter IR 冒烟测试 | scripts/aleo/counter-smoke.sh | PATH 上的 leo CLI（已测试 4.0.2）；python3；来自 lean-toolchain 的 Lean 工具链 | Portable IR Counter 降级为 Leo 4.0 程序，含 @noupgrade constructor 和 fn ... -> Final entry point，匹配 Examples/Aleo/Counter.golden.leo，leo build 生成 main.aleo 和 abi.json，leo test 通过，proof-forge-artifact.json schema 校验通过 | private records、transitions、proofs、直接 Aleo Instructions、devnet 部署、跨目标等价性、独立 .avm 文件 |
| Aleo PureMath IR 冒烟测试 | scripts/aleo/pure-math-smoke.sh | PATH 上的 leo CLI（已测试 4.0.2）；python3；来自 lean-toolchain 的 Lean 工具链 | 带参数的纯函数、if/else、boundedFor、assign、assignOp、assert 降级为 Leo 4.0 程序，匹配 Examples/Aleo/PureMath.golden.leo，leo build 生成 main.aleo 和 abi.json，leo test 通过，proof-forge-artifact.json schema 校验通过 | 带参数的状态写入口、非局部赋值目标、动态循环边界、独立 .avm 文件 |
