> ## 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 如何通过可移植 IR 和 capability 路由把 Lean 合约源码降级为链原生制品

## 分层

ProofForge 由五层组成：

```mermaid theme={null}
flowchart TB
  subgraph authoring ["作者层（用户面，链中立）"]
    SDK["Lean SDK<br/>contract_source / Contract Intent API"]
    TOK["Token SDK<br/>TokenSpec"]
    LEARN[".learn 解析器<br/>（冻结的兼容层）"]
  end
  subgraph core ["编译器私有核心"]
    SPEC["ContractSpec"]
    IR["可移植 IR<br/>+ AllocatorConfig + 所有权规则"]
    SEM["IR 语义 + 形式化锚点<br/>（FV 路线图）"]
  end
  subgraph routing ["目标路由（--target）"]
    REG["Target registry<br/>profile + allocator 绑定"]
    CAP["Capability 检查<br/>拒绝不支持的 intent"]
    EXT["Target Extension SDK<br/>Solana 账户/PDA/CPI 等"]
  end
  subgraph backends ["后端"]
    EVM["EVM<br/>Plan → Yul → solc"]
    SOL["Solana<br/>sBPF asm → ELF"]
    NEAR["NEAR<br/>EmitWat → WAT → wasm"]
    PSY["Psy/DPN<br/>.psy → Dargo"]
    ALEO["Aleo<br/>Leo package"]
    CFW["CF Workers<br/>TypeScript"]
  end
  subgraph artifacts ["制品与验证"]
    ART["bytecode/ELF/wasm/circuit + ABI/IDL<br/>artifact + deploy manifest + TS client"]
    GATES["门禁：Lean 测试 · testkit<br/>Foundry · Mollusk/Surfpool · 离线宿主 · dargo/leo"]
  end
  SDK --> SPEC
  TOK --> SPEC
  LEARN --> SPEC
  SPEC --> IR
  IR --- SEM
  IR --> CAP
  REG --> CAP
  EXT --> CAP
  CAP --> EVM & SOL & NEAR & PSY & ALEO & CFW
  EVM & SOL & NEAR & PSY & ALEO & CFW --> ART
  ART --> GATES
```

## 作者层

* **Contract Intent API** — 默认 SDK 表面：state、entrypoint、event、
  caller/value 访问、checked 算术、断言和证明，不需要 import 目标链模块。
* **Target Extension SDK** — 合约确实需要链原生语义时显式引入（Solana
  账户/PDA/CPI、allocator 选择等）。扩展通过 capability id 和 target
  metadata 降级，绝不给可移植 IR 增加仅单链使用的 constructor（D-027）。
* **Target adapter** — 每个链家族的 ABI、打包、测试运行器和部署逻辑；
  `--target` 选择 adapter，不支持的 intent 在产出制品前被拒绝（D-028）。

## 模块命名

* **Lake module：** `ProofForge.Evm`（合约文件中 import）。
* **Lean namespace：** `Lean.Evm`（示例中 `open Lean.Evm`）。

这一拆分来自 Lean fork 迁移。统一重命名到 `ProofForge.*` 命名空间已列入
backlog（Workstream 24），因为 `Lean.Evm` 会遮蔽 Lean 编译器自身的 `Lean`
命名空间。

## 深入阅读

<CardGroup cols={2}>
  <Card title="作者模型" icon="pen-to-square" href="/zh/concepts/authoring-model">
    Learn source、contract\_source 与内部 ContractSpec 边界。
  </Card>

  <Card title="可移植 IR" icon="diagram-project" href="/zh/concepts/portable-ir">
    IR 规范和阶段 1 验收标准。
  </Card>

  <Card title="能力注册表" icon="puzzle-piece" href="/zh/concepts/capability-registry">
    规范的 capability id 和逐 target 支持矩阵。
  </Card>

  <Card title="RFC 0002" icon="file-lines" href="/zh/rfcs/0002-target-implementation-design">
    目标实现设计 RFC。
  </Card>
</CardGroup>