> ## Documentation Index > Fetch the complete documentation index at: https://gradiences.mintlify.site/llms.txt > Use this file to discover all available pages before exploring further. # ProofForge 架构评审（2026-07） > 本文是一次面向仓库现状的架构评审，评审对象是统一 SDK 输入 + 平台路由到多链 本文是一次面向仓库现状的架构评审，评审对象是"统一 SDK 输入 + 平台路由到多链" 这条主线，以及当前 main / Solana / NEAR 等分支的维护方式。定位与 [可行性分析](/zh/feasibility-analysis) 相同：原生中文分析文档，不是工程权威源。 落地到工程策略的结论应回写英文文档（`docs/decisions.md`、相关 RFC）。 ## 一、总体结论 **架构方向是对的，不需要推翻。** "链中立的 Contract Intent API 作为唯一用户 输入 → ContractSpec / 可移植 IR → capability 路由与检查 → 各链 target adapter 产出工件"这一分层（D-028、RFC 0001/0003、[authoring-model](/zh/concepts/authoring-model)） 是当前多链合约领域里合理的做法，且比 Reach / Solang 这类先例多了 Lean 证明 这一差异化能力。D-027（CPI/PDA 留在 Solana 扩展层，不进可移植 IR）和 "能力不支持就拒绝编译、不做静默降级"的原则也都是正确的取舍。 **当前真正的风险不在架构设计，而在架构正在被分支模式瓦解。** 统一 IR、 capability registry、target registry 是整个架构的"宪法"，但它们目前在 4 个以上长期分支里各自演进。如果不先收敛分支模式，后面每合并一条链， 都要在语义层面（而不只是文本层面）重新对齐一次 IR，代价会随分支数量 和存活时间超线性增长。 下面按优先级展开。 ## 二、现状盘点（2026-07-02） 先修正一下口头模型与仓库实际状态的差异： | 分支 | 口头模型 | 实际状态 | | -------------------------------- | ----------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | | `main` | "EVM" | 已包含 EVM + Solana（sBPF asm 后端、Token SDK、Learn 路由）+ Psy/DPN。Solana 大部分工作已在 `4eab50e` 合入 | | `DaviRain-Su/solana-supprot` | "正在更新的 Solana 分支" | 只剩 2 个未合并提交（Pinocchio 参考资料），基本已完成使命 | | `DaviRain-Su/lookdown` | "Near 分支" | 领先 main 115 个提交、落后 40 个。包含整个 Wasm/NEAR 后端（EmitWat、near-sandbox 冒烟、offline host runtime），**并且修改了共享核心**：`ProofForge/IR/Contract.lean`（新增 `release` 语句）、新增 `IR/Allocator.lean`、`IR/Ownership.lean`、`IR/Semantics.lean`，修改 `Target/Registry.lean`（TargetProfile 增加 allocator 字段）、`docs/capability-registry.md`、`docs/decisions.md` | | `DaviRain-Su/aleo-support` | — | 领先 104、落后 37。含 Leo 后端与 EVM chain-profile 元数据，同样改了 capability registry 与 decisions.md | | `DaviRain-Su/cloudflare-support` | — | 领先 109、落后 3。含 TypeScript/Workers 后端，改了 `Target/Registry.lean` 与 capability registry | 由此得到两个观察： 1. "主分支 = EVM、每条链一个分支"的模型已经和事实不符：main 实际上已经是 多目标主干（EVM + Solana + Psy）。这恰好说明主干化是可行的，Solana 的 合入就是先例。 2. 共享核心文件（`ProofForge/IR/*`、`ProofForge/Target/*`、 `docs/capability-registry.md`、`docs/decisions.md`、 `scripts/i18n/manifest.json`）在每条链分支上都被独立修改。这些文件在 development-standards 里被定义为"单一权威源"，但现实中存在多个互相 分叉的版本。`lookdown` 与 `cloudflare-support` 都改了 `Target/Registry.lean`，`lookdown` / `aleo` / `cloudflare` 三条分支都改了 capability registry——这不是普通的合并冲突，而是架构契约本身在分叉。 ## 三、判断 1：统一 SDK 输入的思路成立，但要把"三层"说死 "把输入统一成一个 SDK，通过平台路由到各链"的思路与仓库现有设计 （D-028 的 Contract Intent API）是一致的，成立。需要固化的是三层边界， 避免任何一层越位： ```text theme={null} 第 1 层 Contract Intent API（唯一的默认用户面） 链中立：state / entry / query / event / 算术 / 断言 / caller / value 第 2 层 Target Extension SDK（显式选择进入，链原生语义） Solana 账户/PDA/CPI、未来的 Move resource、Wasm host 特性 第 3 层 ContractSpec / 可移植 IR（编译器私有边界，用户永远不直接写） ``` 三条护栏： * 第 1 层新增构造的门槛保持 D-027 的标准：至少两个目标家族共享相同语义 形状才进可移植层，否则进第 2 层。 * 第 2 层必须是"显式引入"的（import / 声明可见），不能悄悄混进默认面。 目前 `contract_source` 里 Solana 声明与可移植声明在同一语法块内，建议在 文档和 lint 层面明确：出现目标扩展声明的合约，编译非该目标时报错信息 要指向"这是 Solana 扩展"而不是一般性失败。 * 第 3 层的字符串化表示（ContractSpec）不对用户暴露， [authoring-model](/zh/concepts/authoring-model) 已写明，维持即可。 ### 命名问题必须尽早解决 现在仓库里同时存在三个高度易混的名字： * **Lean**：语言本身； * **`Lean.Evm`**：SDK 的 Lean 命名空间——与 Lean 编译器自身的 `Lean` 核心命名空间冲突，README 也承认这是迁移遗留（"until a rename is scheduled"）。这个 rename 应该真正排期，建议统一到 `ProofForge.*`； * **Learn**：遗留 `.learn` DSL 与 `--learn` / `--learn-token` CLI 路径。 如果对外把统一 SDK 命名为 "LEAN"，会同时撞上"Lean 语言"（搜索引擎和社区 沟通无法区分）和 "Learn"（内部一字之差）。建议： 1. 对外品牌用 **ProofForge SDK**（或另起一个不与 Lean/Learn 谐音的名字）， 文档中"用 Lean 语言编写"作为定语出现，而不是 SDK 名。 2. `.learn` 维持 authoring-model 已定的"遗留兼容层"定位，并真正冻结 （见判断 5）。 ## 四、判断 2（最高优先级）：分支模式必须从"每链一分支"改为主干开发 ### 问题 长期链分支的成本结构： * 架构契约分叉：可移植 IR 的构造子集合、capability id 集合、TargetProfile 结构体字段在不同分支上各自演进。`lookdown` 给 IR 加了 allocator 抽象和 `release` 语句，main 这边 Solana 工作给 ContractSpec/Token 层加了大量 东西，两边都动了对方看不见的"共享地基"。合并时的冲突是语义级的： 例如 allocator 抽象进入 `Target/Registry.lean` 后，Solana 的 bump allocator 选择（main 已有 `Tests/SolanaAllocator.lean`）要不要收编 到同一抽象下，这类问题在分支上无人裁决。 * 权威文档失真：decisions.md 声称是"settled decisions"，但 `lookdown` 上的 D-029+（EmitWat canonical、冻结 Rust v0 等决策）main 上根本看不到。 评审者在 main 上读到的"全局架构状态"是错的。 * i18n 摩擦放大：每条分支都会触碰 `scripts/i18n/manifest.json` 的 sha256 和 `docs/zh/*.zh.md`，这些文件几乎保证合并冲突。 ### 建议的目标模式 **"链"是目录和 target id，不是分支。** 仓库结构已经天然支持这一点： `ProofForge/Backend//`、`docs/targets/.md`、 `scripts//`、target registry 按 id 注册、capability 检查在编译期 拒绝不支持的目标。未完成的后端完全可以带着 Research/Experimental 生命周期 标签住在 main 上，不影响 EVM/Solana 的稳定性——Psy 后端已经是这么做的。 具体规则建议（可回写进 `docs/development-standards.md`）： 1. **共享核心只在 main 演进**：`ProofForge/IR/*`、`ProofForge/Target/*`、 `ProofForge/Contract/*`（Spec/Intent/Source 层）、 `docs/capability-registry.md`、`docs/decisions.md`、`docs/portable-ir.md` 的任何修改，必须以独立小 PR 直接进 main，不允许搭在链功能分支里长期 携带。链分支发现需要改 IR 时，先把 IR 改动拆出来单独合入。 2. **功能分支短命化**：分支只承载一个可合并的增量（一个 backend 里程碑、 一个 capability、一组冒烟测试），以"落后 main 不超过一次日常 rebase 的 量"为健康标准。像 lookdown 这种 115/40 的分叉不再出现。 3. **CI 目标矩阵按需触发**：main 上按改动路径触发对应链的冒烟 （`ProofForge/Backend/Solana/**` → Solana 冒烟），保证多后端共存不拖慢 EVM 迭代。 4. **i18n 同步只在 main 做**：翻译脚本与 manifest 更新作为 main 上的独立 提交/定期任务，分支一律不碰 `docs/zh/` 与 manifest。 ### 存量分支的收敛次序 1. `solana-supprot`：把剩余 2 个 Pinocchio 参考提交合入 main，关闭分支。 2. `lookdown`（NEAR）：**先拆核心、后拆后端**。 a. 把 `IR/Allocator`、`IR/Ownership`、`IR/Semantics`、`IR/Contract` 的 `release` 语句、`Target/Registry` 的 allocator 字段，作为一组 "IR/registry 演进" PR 先行进 main（此时要顺带裁决：Solana 的 allocator 选择是否收编到同一抽象）；同步把 lookdown 上的 decisions/capability-registry 增量合回权威文档。 b. 再把 EmitWat 后端、NEAR 冒烟、offline host runtime 作为 `wasm-near`（Experimental）合入 main。 3. `aleo-support` / `cloudflare-support`：按同样"先核心后后端"的方式处理， 或者如果暂不打算推进，至少把其中对 decisions.md / capability-registry 的修改摘回 main，让权威文档恢复权威。 ## 五、判断 3：目标数量需要收敛出一条"证明主线" `docs/targets/` 下已有 15+ 个 docs-first research 目标，而真正有产出物的 后端是 EVM（成熟）、Solana（接近）、Psy（受限子集）、NEAR（在分支上）。 research 文档本身成本低、有价值，但要避免两个副作用： * 每新增一个 research 目标都在 decisions.md / capability registry 里加行， 放大上面的分支冲突面； * 稀释"跨链可移植性已被证明"这一核心叙事。 建议：把 **EVM + Solana + NEAR 三个目标家族跑通同一个 shared scenario （Counter，进而 ValueVault）** 定义为当前阶段的唯一"完成"标准（对应 Phase 4 的第一个实例），在此之前新的 research 目标只做文档、不动注册表 和 capability 文件。三家族覆盖了三种截然不同的执行模型（EVM 槽存储 / Solana 账户 / Wasm host），足以证明 Intent API 抽象成立；证明成立之后再 铺第 4、第 5 个家族，边际成本会低得多。 ## 六、判断 4：EVM 存在两条并行管线，需要给出归宿 当前 EVM 有两条到 Yul 的路径： 1. 历史路径：Lean 原生合约（`ProofForge.Evm` / `@[export]`）→ LCNF → `EmitYul` → Yul。这是 Phase 0 基线，也是 `--evm-bytecode` 的主路径。 2. 新路径：`contract_source` / Learn → ContractSpec → EVM Plan （`Backend/Evm/Plan.lean`，RFC 0004）→ Yul。 两条管线長期并存会让 "EVM 支持什么" 没有单一答案（能力集合、golden 文件、 冒烟脚本都要 ×2）。既然平台叙事的输入面是 Intent API，建议在 RFC 0004 里 明确：**ContractSpec → Plan → Yul 是产品管线，LCNF → EmitYul 降级为 "Lean 原生实验路径"**，它的存在理由（直接编译带证明的 Lean 函数体）单独 陈述，且不再要求与产品管线保持特性对齐。什么时候淘汰可以不急着定， 但"谁是产品路径"要先定。 ## 七、判断 5：Learn 的"冻结"要执行到位 [authoring-model](/zh/concepts/authoring-model) 已明确 `.learn` 是遗留兼容层、 "不应长成第二门产品语言"。但 main 最近的提交序列（Learn source CLI emission、Learn token target plans、Learn signer/CPI 约束、Learn reference diagnostics）显示新特性仍在 Learn 解析器上先行或同步扩张。这与文档的 定位相反，且每个 Learn 语法扩展都是未来要偿还的兼容债。 建议一条硬规则：**新能力必须先落在 Lean SDK（`contract_source` / Token SDK helpers），`.learn` 只在需要等价性回归时跟进，且不再新增只有 Learn 才有的语法。** 如果 Learn 的真实用途是"给非 Lean 用户一个轻量入口"， 那它就不是遗留层而是第二产品面，需要用一篇 RFC 把这个定位变更说清楚—— 二者取其一，不要维持现在的模糊状态。 ## 八、小项清单 * `Lean.Evm` 命名空间与 Lean 核心 `Lean` 命名空间冲突，rename 到 `ProofForge.*` 应排期（见判断 1）。 * `solana-supprot` 分支名拼写（supprot）——收敛该分支时顺带消灭。 * `docs/targets/solana-sbf.md` 已是历史别名，INDEX 已标注，保持即可； 新文档不要再引用旧 id。 * TokenSpec 的多链 Token SDK（RFC 0006）方向正确：EVM 出 ERC-20 合约、 Solana 出 SPL/Token-2022 计划而非伪 ERC-20 合约，这正是"路由到不同 执行模型"而非"翻译语法"的正确示范，值得作为对外解释架构的样例。 * Cloudflare Workers 后端（TypeScript 目标）与"区块链目标"的注册表语义 不同（无共识、无链上状态），若要保留，建议在 target registry 里给它 一个独立 family 或明确标注为演示性目标，避免稀释 capability 语义。 ## 九、行动清单（按优先级） > 本清单已落入工程 backlog。P0 的分支收敛已于 2026-07-02 执行完成： > `solana-supprot`、`lookdown`（NEAR）、`aleo-support`、`cloudflare-support` > 已全部合入 main，决策撞号已重编号（NEAR → D-029/030/031，Aleo → D-032， > Cloudflare → D-033），`release` 语义冲突已在 EVM/Leo/TS 消费者中修复。 > 剩余跟进见 [implementation-backlog.md 的 Workstream 24](/zh/reference/implementation-backlog) > （Architecture Convergence Follow-ups），形式化验证任务见 Workstream 25 与 > [formal-verification.md](/zh/concepts/formal-verification)。 1. **P0 收敛分支**：合入 `solana-supprot` 残余；按"先 IR/registry、后 后端"两步合入 `lookdown`；把 aleo/cloudflare 分支上的 decisions / capability-registry 增量摘回 main。 2. **P0 立规**：在 `docs/development-standards.md` 增补"共享核心只在 main 演进 + 功能分支短命化 + i18n 只在 main 同步"三条规则，并记入 decisions.md。 3. **P1 定名**：确定对外 SDK 名称（建议 ProofForge SDK），排期 `Lean.Evm` → `ProofForge.*` rename，冻结 Learn 语法面。 4. **P1 定管线**：RFC 0004 中明确 ContractSpec→Plan→Yul 为 EVM 产品管线。 5. **P2 定阶段目标**：以"EVM + Solana + NEAR 跑通同一 shared scenario"为 当前阶段唯一完成标准；此前 research 目标只加文档、不动注册表。 以上第 1、2 项完成后，"统一 LEAN（ProofForge）SDK 输入 → 平台路由多链" 这条主线在组织层面才真正成立；第 3–5 项决定它对外是否讲得清楚。