> ## 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.

# Authoring Model

> ProofForge 不应该要求应用开发者直接编写 ContractSpec 对象。

ProofForge 不应该要求应用开发者直接编写 `ContractSpec` 对象。
`ContractSpec` 是编译器内部边界：源码语法会降低到它，target routing 会消费它，
后端再从对应 IR 和 target-extension metadata 打印目标制品。

## 层次

当前栈里有三层 authoring layer：

| 层                                     | 状态                                                      | 作用                                                                                                                                                          |
| ------------------------------------- | ------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------- |
| Lean embedded SDK / `contract_source` | 已实现的 v1 embedded source syntax                          | 当前 authoring surface。它让仓库能用 Lean 语法表达 portable state、entrypoint、event、arithmetic、SDK intent，以及 Solana account/PDA/CPI declaration，而不用手写 `ContractSpec` 字符串。 |
| Legacy `.learn` parser                | 已实现 v0 standalone parser 与 CLI compatibility entrypoint | 兼容性/冒烟输入，会降低到同一个编译器内部 `ContractSpec` / `TokenSpec` 边界；它不应该继续长成第二套产品语言。                                                                                      |
| `ContractSpec` / IR                   | 编译器内部制品                                                 | 进入 target routing、capability check、backend lowering、AST/printer stage、manifest、IDL、client 和 deployable package 的稳定边界。                                       |

当前仓库的预期用户体验是 Lean-first：开发者使用 Lean 语法和 SDK helper，
编译器再把这些值降低到 `ContractSpec`、`TokenSpec`、portable IR 和
target-extension plan。独立 `.learn` parser 仍有价值，因为它能从文件输入验证同一个
lowering 边界，但新的 SDK 工作应该优先落在 Lean/SDK 层。
`proof-forge --learn --target <id>` 和 `proof-forge --learn-token --target <id>`
因此是 legacy CLI path：它们复用同一个编译器内部边界，而不是定义一套新的产品语言。

因此，带有较多字符串的 `ContractSpec` 与 Builder 示例应被看作编译器 fixture，
不是产品 surface。它们描述的是源码经过 parsing、capability routing 和
target-extension expansion 后交给编译器消费的同一个程序形状。应用开发者应越来越多
看到 Lean SDK 语法和 typed helper；测试可以继续保留 Builder 与 `.learn` fixture
作为已评审的等价输入。

编译器内部的 source AST 和 IR 边界在 parsing 之后用字符串保存 identifier 是正常的；
这不是 authoring model。产品方向是用户编写 Lean SDK 语法，typed helper 尽量先检查
名称和引用，然后编译器才把这些名称物化到 `ContractSpec`、manifest、IDL、client 和
backend AST 里。

## 源码原则

* Portable contract 应表达业务逻辑，而不是 target-specific deployment detail。
* Target-specific capability 应通过 typed SDK form 请求，而不是 raw string plumbing。
* Chain dispatch 属于 build configuration 和 target routing。只要某个 target
  能提供等价能力，源码就应该保持可复用。
* Solana account/PDA/CPI declaration 这类 target extension 可以出现在 source
  中，但前提是合约确实需要 chain-native semantics。这些 extension 会降低为
  target metadata 和 helper action；除非多个链家族共享同一语义形态，否则不进入
  portable IR constructor。
* 真实协议字节可以继续使用 literal string，例如 PDA literal seed。account、
  owner、capability name、method 或 deployment configuration 不应该主要靠字符串表达。

## 当前语法边界

`ProofForge.Contract.Source` 是当前可执行的 Lean syntax layer，覆盖：

* portable scalar state；
* 带 typed parameter 的 entrypoint 和 query；
* local binding、assignment、return、event emission 和 checked arithmetic syntax；
* Solana allocator selection；
* Solana account constraint，包括 writable 和 signer declaration；
* Solana PDA declaration 和 derivation statement；
* Solana System Program `transfer` 与 `create_account` CPI declaration 和
  invocation statement；
* Solana SPL Token `transfer_checked`、`mint_to`、`burn`、`approve`、`revoke`
  和 `set_authority` CPI declaration 和 invocation statement；
* Solana log、return-data、compute-unit、memory、crypto 和 sysvar helper
  statement。

`ProofForge.Contract.Token` 是当前 token SDK planning 边界。Lean-authored
`TokenSpec` 会在 EVM 上路由为 ERC-20，在 Solana 上路由为结构化 SPL Token /
Token-2022 deployment plan。Solana plan 会记录 mint account 创建、associated
token account、`mint_to`、`transfer_checked`、`approve`、`burn`、`revoke`、
authority change、Token-2022 extension 初始化、Token-2022 transfer-fee
collection flow（direct withheld-fee withdraw，以及 harvest-to-mint 后再从
mint withdraw），以及 non-transferable token 初始化（拒绝 `TransferChecked`，
但仍允许 burn），以及 Web3.js 或 client generation 需要的 Solana program id。

`ProofForge.Contract.Learn` 仍会解析 `Examples/Learn/` 下 checked-in 的
`.learn` 示例，生成一个小型 source AST，并将该 AST 降低到 `contract_source`
共用的 `ContractSpec`/portable IR 边界。CLI 可以通过 `--target evm` 把
`.learn` 输入路由到 EVM bytecode metadata，也可以通过
`--target solana-sbpf-asm` 路由到 Solana sBPF assembly package。parser 目前覆盖
portable scalar/event 子集，以及第一批 Solana
target-extension form：account、PDA derivation、System Program
transfer/create-account CPI，以及 SPL Token transfer、mint、burn、approve 和
revoke CPI。它也支持带 selector 的 entrypoint，例如
`entry mint selector "04"(amount: u64)`，因此 Solana instruction tag 可以在
Learn 源码中表达，而不是只存在于 Builder fixture。Learn statement 现在也覆盖
Solana pubkey/data log、return-data set/get，以及 remaining-compute-unit read/log
helper。同一 source 层也覆盖 Solana memory helper、SHA-256、Keccak-256、BLAKE3
hash helper，以及 Clock、Rent、EpochSchedule、EpochRewards 和 LastRestartSlot
fixture coverage 所需的 sysvar/context read。
Learn lowering 也会在发射 `ContractSpec` 之前校验已声明的 Solana CPI/PDA
引用、已声明的 CPI account 引用、CPI writable/signer 要求、signer seed，以及 helper
state/account 引用，因此剩余带字符串的 identifier 属于被检查过的编译器数据，而不是未检查的
用户面对 spec plumbing。
`ProofForge.Contract.Token.Learn` 会单独解析
`Examples/Learn/ProofToken.learn` 与 `Examples/Learn/FeeToken.learn` 这样的
Learn token intent source。`--learn-token --target evm` 现在会发射 ERC-20
Yul、bytecode 和 artifact metadata，并使用标准 ERC-20 selector 以及
Transfer/Approval topic；`--learn-token --target solana-sbpf-asm` 会发射 SPL
Token plan，并在 `transfer_fee` 这类功能需要 Token Extensions 时自动切到
Token-2022。这个 CLI path 复用 `TokenSpec`，因此输出的是和 Lean-authored token
spec 相同的结构化 SPL Token / Token-2022 plan。

`ProofForge.Contract.Examples.ValueVault` 这样的示例应被理解为 v1 Lean source
example，而不是第二套 `.learn` grammar 的过渡区。对应的 `.learn` 文件是 legacy
compatibility example，用于证明 lowering equivalence。

## Target Routing

构建 target 决定 lowering path：

```text theme={null}
Lean SDK syntax / contract_source
  -> source AST
  -> ContractSpec / portable IR
  -> target resolver + capability routing
  -> target semantic AST
  -> printer / assembler / package emitter
```

对 Solana 来说，target extension 会挂接 account schema、PDA seed、CPI layout、
IDL、client 和 sBPF assembly helper。对 EVM 来说，routing 会派生 ABI selector、
Yul、bytecode、ABI metadata 和 deployment file。当合约本身是 portable 时，源码作者
不应该手动切换这些内部实现细节。

## 下一步实现

1. 新的 SDK Alpha/Beta 工作继续落在 Lean SDK 语法和编译器内部 planning layer；
   legacy `.learn` 输入只在兼容性测试有用时复用这些层。
2. 逐步用 typed account、owner、program 和 capability reference 替代 Lean helper
   中带字符串的 Solana declaration，同时只在编译器制品内部保留字符串名称。
3. 随着 Wasm、Move 和其他 target 后端从 routing plan 走到 package emitter，
   继续扩展 target package emission。