One portable program source → controlled materialization for many execution platforms.
一份 portable 业务程序源码 → 多个执行平台的受控物化。
ProofForge V2 is a Lean 4 multi-target compiler (proof-forge-next): authors write a
single program … where program; the compiler infers semantic requirements, then
--target selects materialization for EVM, Solana, NEAR, Noir (and later platforms).
ProofForge V2 是用 Lean 4 实现的多目标编译器：作者只写统一的
program … where 源码；编译器从源码推导语义需求（requirements），再由
--target 选择 EVM / Solana / NEAR / Noir（及后续平台）的物化方式。
- 改 target 只能改制品与物化，不能改整数语义、状态迁移、回滚、调用顺序、 授权或信息披露语义。
- 无法保持语义时必须拒绝（稳定诊断），禁止 best-effort 降级或回退到旧路径。
- 编译器是 代码生成 + 语义检查工具，不是链上 VM、密钥托管或默认网络执行器。
仓库根目录即 V2 产品工程。旧版 ProofForge（v1）归档在 active/，
仅作研究参考，不是运行时依赖。
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# 安装 Lean（见 lean-toolchain）后：
just build
just test
# 或本地完整 gate（含 macOS hermetic 子集，见下文）
just ci # 可移植 Linux / GitHub CI 子集源码 不 声明 “合约 / 电路 / zkVM workload” 类别；类别由 --target 的物化决定，
且不得偷偷改业务语义。
权威文字规格：docs/02-architecture.md。
图源（Excalidraw + PNG）在 docs/diagrams/。
一份 portable program 源码，经 target-neutral 语义与 exact support 求解后，进入
目标自有 Plan/IR 与制品；外部 packager / runtime / 网络在编译器边界之外。
Syntax 只是入口树，不是领域语义：Parse → Preflight → Decode → Typed → Semantic →
Resolve → Materialize。失败 fail closed，禁止降级或 legacy fallback。
同一 Counter 语义；--target 只改变物化与制品编码。成熟度必须诚实标注
（runtime / plan-only / wasm / source-only）。
| 预览 | 源文件 | 说明 |
|---|---|---|
| PNG · Excalidraw | Requirements + SupportClaim 求解（fail closed） | |
| PNG · Excalidraw | Phase 1 vs design-only + 成熟度阶梯 | |
| PNG · Excalidraw | 根 = V2；active/ = v1 归档 |
|
| PNG · Excalidraw | 模块边界与禁止依赖 |
编辑白板：打开 excalidraw.com → Open 对应 .excalidraw →
导出 PNG 覆盖同名 0N-*.png。重新生成 JSON（会覆盖未备份手改）：
python3 scripts/generate-excalidraw-diagrams.pyAuthor / CI
│ Lean source + explicit --target / profiles
▼
proof-forge-next
├─ Lean Parser + portable decoder (+ Syntax preflight)
│ → Source.Program
├─ name / type / effect check
│ → Typed.Program
├─ target-neutral normalization
│ → Semantic.Program + ProgramRequirements
├─ Support resolver (exact SupportClaim, fail closed)
│ → ResolvedProgram target
├─ target Materializer
│ → target Plan → TargetIR
└─ emitter
→ OutputSet + provenance (atomic write)
│
├─ official packager / validator / local runtime
└─ deploy / prove / verify ← 仅显式命令，不隐式联网
前端直接使用 Lean 4 的 Syntax，但 不把 Lean AST 当作领域语义。CLI 只解析允许的
portable command，不 elaboration / 执行用户文件中的任意 Lean command。
关键不变量（摘要）：
| ID | 含义 |
|---|---|
| INV-001 | Source / Typed / Semantic 层不按 TargetId 分支 |
| INV-002 | target 只能做等价物化；否则拒绝 |
| INV-005 | 任一失败不得变成“成功”或 legacy fallback |
| INV-008 | build 无网络与密钥副作用；deploy/prove/verify 显式 |
| INV-010 | clean-room 不依赖 active/ 或旧 v1 路径 |
| Target | 角色 | 本阶段 | 证据状态（不得夸大） |
|---|---|---|---|
evm |
contract VM | Phase 1 | Counter bytecode + Anvil 初始化/increment/overflow；非完整 EVM 后端 |
solana |
explicit-account SVM | Phase 1 | typed .sbpf-plan + IDL；无 sBPF object / ELF / runtime |
near |
Wasm host | Phase 1 | raw-u64 Counter/Accumulator WAT/Wasm + wat2wasm；无 sandbox receipt |
noir |
circuit | Phase 1 | target-owned Plan / relation IR → .nr packages；无 Nargo/ACIR/proof/VK |
| CosmWasm / Soroban / ICP / OpenVM / Aleo / Psy | — | design / research | 仅档案与路线图，无 产品后端宣称 |
.
├── ProofForgeV2/ # 编译器（Core · Language · Targets · CLI）
├── Examples/ # 可编译示例程序
├── Tests/ # 单元 / 物化测试
├── docs/ # PRD · 架构 · 规格 · ADR · diagrams
├── scripts/ # CI · clean-room · toolchain · 文档检查
├── justfile # 本地与 CI 门禁入口
├── active/ # 归档的 v1 全树（研究 only）
└── AGENTS.md # 给 agent / 贡献者的控制面
| 想了解 | 打开 |
|---|---|
| 生命周期与权威索引 | docs/document-status.md |
| 文档导航 | docs/index.md |
| 产品需求 | docs/01-prd.md |
| 系统架构 | docs/02-architecture.md |
| 任务与验收 | docs/04-task-breakdown.md |
| 实现事实日志 | docs/06-implementation-log.md |
| Agent 工作协议 | AGENTS.md |
权威顺序： 已接受 ADR/PRD/架构/规格 → 可复现 gate/evidence → 当前代码与制品。
调研材料是证据输入，不会自动变成规范。
just docs-check # 文档控制面
just build # Lake: ProofForgeV2 + proof-forge-next
just test # proof-forge-next-tests
just ci # 可移植子集（GitHub / Woodpecker 使用）
just check # 完整本地 gate（含 macOS hermetic / 锁定工具链）
just v2-clean-room-alpha # clean-room 开发门禁（非正式 hermetic release）| 表面 | 命令 / 配置 | 宣称 |
|---|---|---|
| Hosted CI | .github/workflows/ci.yml、.woodpecker.yml → just ci |
Linux portable：docs + build/test + 负例 |
| Linux tool-root CI | .github/workflows/ci.yml 的 linux-tool-root lane |
linux 资产 provision/materialize/verify 与 host profile 生成/验证闭环；development 级，非 hermetic |
| 密钥扫描 | secret-scan workflow |
only-verified TruffleHog |
| 本地 hermetic | just check / v2-clean-room-alpha |
需 macOS host profile + darwin-arm64 锁定工具；不是 release EV |
ADR-0016 后工具链与 host 观察按平台拆分，两台机器都可以直接开发：
- 工具锁定按平台分文件：
toolchains.lock.json（darwin-arm64，字节冻结）与toolchains-linux-x86_64.lock.json（linux）；justfile按uname选择 tool root、锁定 git/python 与 Stage-0 分支，consumer 对跨平台文件互相拒绝。 just ci、just toolchains-*、just host-stage0-development在两个平台都可运行； linux 上 clean-room 沙箱（isolated-check/v2-clean-room-alpha）显式 fail closed （沙箱引擎仅 macOS，linux 化需独立任务）。- 两台机器都直接推
main：开工前git fetch && git status --short，分叉时合并 而非重写对方提交（证据/台账按 commit 哈希引用，rebase 会打断引用）。 - 任何
ProofForgeV2/**源码变更必须在同一变更集运行just sbom-package-files-refresh重新钉住supply-chain/lean-package-files.v1.json， 否则just ci的 SBOM 闭包检查以PF-SBOM-CLOSURE失败（双机通用）。 - 当前两台开发机均 不是 eligible host（darwin 机 SSV seal broken、Linux 机
SecureBoot disabled）：一切输出均为 development 级；eligible Stage-0 handoff 与
formal 入口在两台机器上都 fail closed。linux 机器成为 eligible 的条件：
固件启用 Secure Boot、system/distro 工具按 lock 精确固定后重新生成并登记
host profile（见
docs/adr/0016-cross-platform-host-profile-and-linux-eligibility.md）。
首次物化锁定工具（本地 hermetic，非普通 just ci）：
just toolchains-provision-lean
just toolchains-provision-externalV2 完成了文档/规格基线与 不可发布 的 alpha 骨架：独立 Lake、统一 DSL 入口、 Core 与四目标 materializer 的最小连通性。不等于 Phase 1 完成。
- Clean-room development gate 已可跑，但当前 host 可能
Sealed: Broken等， 不能当作正式 hermetic / release evidence。 - 详见实现日志与 document status；写 maturity 时以 代码 + 可复现 gate 为准。
| 项 | 位置 |
|---|---|
| 问题 / 讨论 | GitHub Issues |
| 贡献指南 | CONTRIBUTING.md |
| 安全报告 | SECURITY.md |
| 架构图 | docs/diagrams/ |
| Agent 协议 | AGENTS.md |
仓库 About 描述、Topics、Website 由 maintainer 在 GitHub 设置；Social preview
建议使用 docs/diagrams/01-architecture-overview.png（Settings → General → Social preview）。
Apache-2.0 — 见根目录 LICENSE。