开发指南

如何使用 ProofForge 开发——从环境准备到物化可移植程序。

本指南说明如何用 ProofForge（proof-forge-next）写一份可移植业务程序，并物化到具体链。编译器做的是代码生成 + 语义检查，不是链上 VM、密钥托管或默认网络执行器。

从编写可移植程序到使用显式 --target 物化。构建无网络或密钥副作用；deploy / prove / verify 保持为显式命令。

1. 心智模型

01
写一份 program … where
源码不声明「合约 / 电路 / zkVM」类别。state、init、entry、view 描述业务语义。
02
编译器推导 requirements
Parse → Typed → Semantic → ProgramRequirements。Source/Typed/Semantic 层不按 TargetId 分支（INV-001）。
03
显式 --target 物化
SupportClaim 精确匹配。能保持语义则 materialize；不能则稳定诊断拒绝，禁止 best-effort 降级。
04
制品在边界内
OutputSet + provenance。packager / runtime / 网络在编译器边界之外。

2. 环境

安装 Lean，版本见仓库根目录 lean-toolchain（文档以 Lean 4.31 族为准）。
克隆 DaviRain-Su/proof_forge，在仓库根使用 just 与 lake。
首次建议跑通门禁，确认本机产品路径健康：

just dev-check
just ci

历史名称 just governance-check / just release-check 当前 justfile 未注册，不能执行或声称通过。

3. 写程序

最小可运行例子（与仓库 Examples/Counter.lean 同构）：

import ProofForgeV2
open ProofForgeV2.Language

program Counter where
  state count : UInt64

  init(initial : UInt64) do
    count := initial

  entry increment(delta : UInt64) : UInt64 do
    count := count + delta
    return count

  view get() : UInt64 do
    return count

state

持久状态字段。标量、聚合、容器能否在目标链 lower，见矩阵。

init

初始化入口，建立初始状态。

entry

可变业务操作（有状态迁移）。

view

只读查询面。部分 target 对 computed view 仍 fail-closed。

4. 构建

CLI 需要显式 --module（canonical identity）与 --target。示例：

lake env .lake/build/bin/proof-forge-next build \
  Examples/Counter.lean \
  --module Examples.Counter \
  --target solana -o build/counter-solana

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 build \
  Examples/Counter.lean \
  --module Examples.Counter \
  --target aleo -o build/counter-aleo

lake env .lake/build/bin/proof-forge-next inspect build/counter-aleo --json

选哪个 target、各链成熟度差异见「开放名单」；op 级对照见「目标矩阵」；Aleo 细节见「Aleo 专区」。

5. Fail-closed 行为

若程序使用了目标链无法等价物化的能力（例如在 Aleo 上使用 emit / sync call，或在错误 field 曲线上），编译器会拒绝，并给出稳定诊断——不会静默降级到「差不多能跑」的旧路径。

这是有意设计：多链物化只改制品与编码，不改整数语义、状态迁移、回滚、调用顺序、授权与披露语义。

6. 不要预期什么

不会自动部署到主网或测试网（deploy 为显式、边界外操作）。
不会把工程 runtime 差分（Anvil / Mollusk / sandbox）说成 formal 证明已完成。
形式化轨道（业务稳定后的 preservation 等）仍在进行，见「开放名单 · 形式化」。
Aleo 当前无 snarkVM prove/deploy 产品门；Noir 无 prove/verify。

7. Solana 进阶（可选）

仓库提供离线 proof-forge-solana-client 与 TransferSol 本地真实调用路径（不访问 RPC、不读钱包）：

just solana-client-test
just solana-transfer-sol-build
just solana-transfer-sol-offline
just solana-transfer-sol-local

这是 engineering self-consistency / runtime observation，不是 signed provenance 或 mainnet 证据。

8. MCP

远程边缘仅做 guidance。编译、私钥与 broadcast 仍在开发机，通过 stdio MCP 或 pf CLI 完成。

MCP →

下一步

开放名单 →feature 矩阵 →Aleo 专区 →MCP →