开发标准

本页面是面向开发者的标准索引。它链接了现有的真值来源文档，并说明了必须更新这些文档的时机。

本页面是面向开发者的标准索引。它链接了现有的真值来源文档，并说明了必须更新这些文档的时机。

​

真值来源

主题	权威文档
文档地图	docs/INDEX.md
已确定的架构和路线图决策	docs/decisions.md
已接受的产品 / 目标方向	docs/rfcs/0001-multichain-platform.md, docs/rfcs/0002-target-implementation-design.md
可移植 IR 与运行时/能力降级	docs/portable-ir.md, docs/rfcs/0003-portable-ir-and-runtime.md
规范的能力 id 与支持矩阵	docs/capability-registry.md
目标生命周期与各目标注释	docs/targets/README.md, 以及具体的 docs/targets/*.md 注释
EVM 基准详情	docs/targets/evm.md, Examples/Evm/README.md
共享的跨目标 Counter 场景	docs/shared-scenario.md
执行积压工作与验收标准	docs/implementation-backlog.md
验证命令与工具先决条件	docs/validation-gates.md
中文叙述 / 策略文档	docs/zh/*.md；它们必须与英文工程文档保持一致，且不得引入独立的工程策略

​

RFC 与决策策略

• RFC 以 Draft 开始。
• 只有当决策记录在 docs/decisions.md 中且链接文档已对齐（符合 docs/rfcs/README.md 第 7-8 行）时，RFC 才会变为 Accepted。
• 被取代的立场记录在 docs/decisions.md 的 Superseded Positions 下。
• 除非相应的决策已存在于 docs/decisions.md 中，否则不要在此任务中更改 RFC 状态。

​

更改代码之前

1. 阅读 docs/INDEX.md。
2. 阅读 docs/decisions.md 以及相关的 RFC/目标注释。
3. 如果更改涉及公共 CLI 标志、目标 id、能力 id、制品字段、验证命令、目标生命周期阶段或示例合约行为，请在同一次更改中更新最近的真值来源文档。
4. 运行 docs/validation-gates.md 中与所触及边界匹配的窄门。

​

命令运行器规范

• 根目录 justfile 是面向开发者的命令目录，用于常见本地工作流，例如 just build、just check、just evm-smoke abi-scalar 和 just evm-all。
• 将较长的目标 harness、生成的测试工程、validator 和特定目标的 shell 逻辑保留在 scripts/ 中；justfile recipe 应组合这些脚本，而不是内联 它们的实现。
• CI 应调用与本地常见门禁相同的 just recipe，同时在有助于定位失败时保留独立 的 GitHub Actions 步骤。
• 添加面向用户或 CI 覆盖的 smoke 脚本时，应在同一次更改中添加或更新匹配的 just recipe/list 入口。
• 文档可以用 just 命令展示常见工作流，但当某个脚本是验证门禁的权威实现时， 目标文档仍应命名底层脚本。

​

分支与目标策略

• 目标、链或后端 spike 应由目录和 target id 表示，而不是由长期 feature branch 表示。
• 触及下列真值来源文件的更改，必须以独立、可 review 的 PR 落到 main， 不应批量夹带在某条链分支里：
  • ProofForge/IR/*
  • ProofForge/Target/*
  • ProofForge/Contract/{Spec,Intent,Source}*
  • docs/capability-registry.md
  • docs/decisions.md
  • docs/portable-ir.md
• 链分支合并后，应 retire 对应 remote branch；从那一刻起 trunk 拥有该 target。

​

i18n 规则

• Feature branch 和 chain branch 不应修改 docs/zh/*.zh.md 或 scripts/i18n/manifest.json。
• Translation sync（scripts/translate-docs.py）只在 main 上运行，并且应在英文 真值来源文档稳定后再运行。

​

Lean 包规范

• Lean 工具链是来自 lean-toolchain 的 leanprover/lean4:v4.31.0。
• 基础构建门禁是 lake build。
• 当前库根为 ProofForge、ProofForge.Evm、ProofForge.Compiler.Yul.AST、ProofForge.Compiler.Yul.Printer 以及来自 lakefile.lean 第 7-14 行的 ProofForge.Compiler.LCNF.EmitYul。
• 可执行文件为 proof-forge，根位于 ProofForge.Cli，包含来自 lakefile.lean 第 16-19 行的 supportInterpreter := true。
• 新编译的 Lean 模块必须由现有根导入或添加到 Lake 根中，文档才能声称它们是包的一部分。

​

当前 EVM 规范

• EVM 合约导入 ProofForge.Evm 和 open Lean.Evm。
• 导出的合约入口使用 @[export l_<Contract>_<method>]，且必须匹配 --method CLI 标志或同级的 .evm-methods 文件。
• EVM 文档中的能力名称必须重用 docs/capability-registry.md id：events.emit、crosscall.invoke、account.explicit、storage.pda、crosscall.cpi。不要引入替代 id，例如 events.log、cross_call.contract 或 account.container。

​

计划行为标签

任何未在此仓库中实现的任务命令、目标、制品字段或验证路径必须标记为 Planned 或 Research，不得写为当前行为。