Claim 层：capabilities、architecture 与 contracts

Claim 层让你把意图 — 程序的每个部分可以做什么、它如何被塑形、它必须保证什么 — 表达为一组薄声明，编译器在每次构建时强制执行。你批准 claims；编译器让每一行代码都对它们负责，包括你自己没写的那些行。

它在 release 构建中零运行时开销 — capabilities、architecture、pure、noalloc 在任何构建中都不存在于运行时，contracts 从 release 二进制中被擦除（已验证逐字节相同，见 §8）。

本页是完整操作指南，从五分钟快速开始到一个完全的实例。

目录

1. 五分钟快速开始
2. claims 速览
3. Capabilities — 代码可以做什么
4. Architecture — 代码可以 import 什么
5. Contracts — 代码必须保证什么
6. pure 与 noalloc — 单词级方法 claim
7. 一个完整的实例
8. 它的代价
9. 与 AI agent 协作
10. 诊断参考
11. 限制与 FAQ

1. 五分钟快速开始

在任何已有项目（一个带 Build.sj 的目录）中：

第 1 步 — 声明 capabilities。 在 Build.sj 中加一个键：

// 扁平成对（包或依赖，授权），与 `dependencies` 形状相同
static final String[] capabilities = {
    "myapp", "net, fs.read",
};

第 2 步 — 检查。 superj check。如果一个包执行了它没有授权的效果，你会得到一个有定位、可操作的错误：

src/util/Fetch.sj:14:9: error[E_CAP_DENIED]: package `util` performs `net`
(native sj_UnixGateway_openUdpSocket) but holds no `net` grant.
Grants for util: (none). Add "util", "net" to Build.sj capabilities,
or remove the call.

第 3 步 — 看你实际用了什么。

$ superj capabilities
package            granted        used
myapp              net, fs.read   net
warning: myapp granted fs.read, never used — consider removing

收紧直到 granted 等于 used。这就是最小权限，一次一行的 diff。本页其余都是展开说明。

理解这一条规则： capabilities 键存在的瞬间 — 即使是空的 — 项目就翻转为默认拒绝：任何未列出的包都不持有任何 capability。没有该键 = 不受限（claim 层之前的行为）。没有部分模式。

2. claims 速览

3. Capabilities

3.1 七个授权

纯计算 — Math、集合、String、解析、缓冲区上的加密 — 不被任何东西门控，不需要授权。ffi 比看起来更重要：没有它的包不能声明 native 方法，因此不能创造检查器不知道的效果。

3.2 声明授权

在 Build.sj 中，扁平成对条目 — 与 dependencies 形状相同。键是你的项目包名或依赖名；值是逗号分隔的授权（空字符串 = 纯）：

static final String[] capabilities = {
    "payments.app", "net, fs.read",
    "httpkit",      "net",
    "jsonlib",      "",
    // payments.model, payments.wire: 未列出 = 无 capability。
};

用 "" 列出与不列出一个包是同一回事（无授权）；当你想让审查记录写明"刻意保持纯"时显式列出它。

依赖不能自我授权。 授权只存在于你的 Build.sj 中。依赖自身文件内的任何东西都不能扩大它在你的程序内部可以做什么。当你升级一个依赖，它突然需要一个之前不需要的效果时，你的构建以 E_CAP_DENIED 停下，直到你授权它 — 刻意地、以一个可审查的一行 diff。这就是供应链检查点按设计工作的样子。

3.3 检查发生（与不发生）的地方

检查在效果点：源码包含 capability 门控调用的那个包必须持有授权。

• payments.app 调用 httpkit 的公开 API 不需要自己持有 net — httpkit 持有它。授权不可传递。
• SDK（sj.*）豁免：import sj.http 不是效果；从你的包进入网络才是。
• 全程序：检查器看到每条调用边（依赖从源码编译），所以答案是完整的，不是启发式的。

要同时控制谁可以到达一个持有效果的包，把 capabilities 与 architecture（§4）配对 — 一个没有 net 授权、也没有到任何持有 net 的包的 import 路径的包，根本无法造成网络 I/O。

3.4 最小权限报告

superj capabilities（从项目目录）打印生效的授权映射与 已授权-已使用 差额：

$ superj capabilities
package            granted        used
payments.app       net, fs.read   net
httpkit (dep)      net            net
payments.model     -              -
warning: payments.app granted fs.read, never used — consider removing

在重大改动后运行它。一个 never used 警告是一个比其内容更宽的信封 — 白白携带的攻击面。如果清单没有 capabilities 键，它打印 no capabilities declared — project is unrestricted 并以退出码 0 退出。

3.5 单文件编译（无 Build.sj）

对于一次性 superj compile 运行，同一映射可直接传入：

superj compile src/app/Main.sj --sdk-source $SJ_HOME/sdk/sj \
    --capabilities "app=net,fs.read;model="

分号分隔的 pkg=caps 条目，caps 逗号分隔。传入 --capabilities "" 仍翻转为默认拒绝。--architecture 接受相同格式。在项目中，优先用清单 — 构建系统为你传这些标志。

4. Architecture

4.1 声明形状

一个键，相同的成对形状：(包, 允许的 import)，允许的 import 是项目包与依赖名：

static final String[] architecture = {
    "payments.model", "",
    "payments.wire",  "payments.model",
    "payments.app",   "payments.model, payments.wire, httpkit, jsonlib",
};

完整或不存在。 如果该键存在，每个项目包都必须有条目 — 缺失的包是清单错误。半声明的 architecture 是半真实的图，因此部分声明不可表达。（sj.* import 总是被允许，永不列出。）

一个包的允许列表之外的 import — 或全限定使用 — 在检查时被拒绝：

src/payments/model/Account.sj:3:1: error[E_ARCH_DENIED]: package
`payments.model` imports `payments.wire` but its architecture entry
allows only: (none).

4.2 看到真实的图

$ superj topology

打印从源码推导出的依赖图 — 总是可用，无论是否声明 — 并在声明了 architecture 时，把声明的视图并排显示。预期对已有代码库的首次运行会有教育意义：修图或修声明，从那次提交起 architecture 就不会悄悄漂移 — 违规的 import 不编译。

4.3 划算的形状

按效果而非特性组织包：一个纯核心（领域逻辑、无授权、不 import 或几乎不 import）加一个薄的有效果的边缘（那一个持有 net/fs.*/exec 的包）。纯核心变得可自由再生且廉价可信；危险表面小到真的可以逐行读。如果一个包需要一个吓人的授权，第一个动作是让那个包更小。

5. Contracts

5.1 requires 与 ensures

子句位于签名与 body 之间。requires 在入口检查；ensures 在每个返回点检查，其中 result 命名返回值（类型为返回类型）：

public long transfer(Account from, Account to, long cents)
    requires cents > 0
    requires from.balanceCents() >= cents
    ensures  result == cents
{
    ...
}

允许多个 requires/ensures 子句；每个独立检查，由各自文本报告。

5.2 invariant

类成员；表达式可使用实例的字段与 pure 方法：

public class Account {
    private long balanceCents;
    invariant balanceCents >= 0;
    ...
}

在构造器退出与每个 public/protected 方法退出时检查 — 从不在私有/内部调用上，从不在静态方法上。因此私有 helper 可以经过暂时无效的状态；所保证的是，只要控制流越过其公开边界返回，对象就是有效的。

5.3 assert

Java 语法，在任何 body 内：

assert idx >= 0;
assert idx >= 0 : "index underflow";

5.4 contract 表达式必须 pure

任何在 requires/ensures/invariant/assert 表达式内调用的方法必须是 pure（§6）— 否则编译时 error[E_CONTRACT_IMPURE]。这不是吹毛求疵：带副作用的 contract 会让 checked 构建与 release 构建表现不同，而这正是 claim 层要防止的那件事。实践上这意味着：给你的类小的 pure 访问器（balanceCents()、size()），并用它们来写 contract。

5.5 违规时发生什么

在 checked 构建中，被违反的子句抛出 ContractViolation，命名子句与源码位置：

ContractViolation: ensures result == cents
  at payments.model.Ledger.transfer (Ledger.sj:41)

ContractViolation 是一个 bug 报告，不是可恢复状态 — 它意味着代码不再做其签名所承诺的。修代码（或经过深思熟虑后，修 claim）；不要捕获它。

5.6 contract 何时运行

contract 默认开启 — superj build、superj run、superj test 以及 golden gate 都会检查它们，因此你的整个测试语料从你写它的那天起就练习每个子句。它们在 release 中被擦除：superj build --release 完全把它们编译掉（release profile 传入 --no-contracts；你可以在任何 compile 上自己传入以退出）。刻意没有运行时开关 — 一个 release 二进制要么不携带检查，要么它不是 release 二进制。

5.7 方法边界的空性

SuperJ 没有 Optional 类型，也没有 @Nullable/@NonNull 注解。方法边界的空性用上面的 contract 子句表达 — 签名处一行，在 dev/test 构建中检查，在 release 中擦除：

// 一个永不返回 null 的查找：
Node find(int key) ensures result != null { ... }

// 一个可能返回 null 的查找（调用者必须检查）：
Node maybeFind(int key) { ... }

// 一个要求非 null 参数的方法：
void use(Node n) requires n != null { ... }

这覆盖了跨方法的情形：一个忽略文档化的 null 返回、把值传给 requires n != null 方法的调用者，在每次 checked 运行中都会被捕获。它不做的是对 maybe-null 局部的直接解引用（n.key，其中 n 来自 maybeFind 且未被守卫）做编译检查 — 那是一个局部缺陷，在你正读的 body 中可见，对其的流敏感检查器在设计中被记录为待办项，而非今天发布。诚实指引：对"未找到"返回 null（不是异常 — 见语言参考中的异常处理），并在解引用前于调用点守卫它。

6. pure 与 noalloc

两个方法修饰符，由全程序可达性在编译时检查，在任何构建中运行时零开销。它们可组合：public pure noalloc long bestBid() 是语言中用两个词能写出的最强签名。

pure — 此方法不触及任何 capability 门控效果、不写静态字段、只调用 pure 方法。允许 arena 分配（分配不是可观察效果）。违规：error[E_IMPURE]。

public pure long square(long n) { return n * n; }

用在领域逻辑上，以及任何 contract 需要调用的东西上。它也是读者能获得的最强单词文档。

noalloc — 此方法不分配任何东西：无 new、无字符串拼接、无到达分配的 native，任何路径上 — 且只调用 noalloc 方法。违规：error[E_NOALLOC]，在分配表达式处：

public noalloc void onQuote(Quote q)
    requires q.priceTicks() > 0
{ ... }

传递性是关键：在你的稳态入口点上加一个 noalloc 就钉住了其下的整棵调用树。 那个在三层调用之下格式化日志字符串的"快速修复"不编译。标记热路径根，把预热/重连路径（可以自由分配）放在它之外。

noalloc 是一个机制 claim，不是时序 claim — 它证明不会有东西悄悄让你的分配画像回归；你自己的基准套件仍是实际纳秒的度量。

7. 一个完整的实例

一个你可以照着输入并尝试的最小 claimed 项目。布局：

payments/
  Build.sj
  src/payments/model/Ledger.sj
  src/payments/app/Main.sj

Build.sj：

public class Build {
    static final String name  = "payments";
    static final String entry = "payments.app.Main";

    static final String[] capabilities = {
        "payments.app", "env",
        // payments.model: 未列出 = 纯。
    };

    static final String[] architecture = {
        "payments.model", "",
        "payments.app",   "payments.model",
    };
}

src/payments/model/Ledger.sj：

package payments.model;

public class Ledger {
    private long balance;
    invariant balance >= 0;

    public Ledger(long initial)
        requires initial >= 0
    {
        balance = initial;
    }

    pure public long balanceCents() { return balance; }

    public long withdraw(long cents)
        requires cents > 0
        requires cents <= this.balanceCents()
        ensures  result == cents
    {
        balance = balance - cents;
        return cents;
    }
}

src/payments/app/Main.sj：

package payments.app;

import payments.model.Ledger;

public class Main {
    public static void main(String[] args) {
        Ledger l = new Ledger(100);
        long got = l.withdraw(30);
        System.out.println("withdrew " + got + ", balance " + l.balanceCents());
    }
}

运行：

$ superj run
withdrew 30, balance 70

现在打破每个 claim 并看它如何自保：

1. 违反 contract — 在 withdraw 中，把 body 改为 balance = balance - cents - 1; 然后 superj run：ContractViolation: invariant balance >= 0（掏空账户）或一个失败的 ensures — 业务规则捕获了你的测试可能捕获不到的 off-by-one。
2. 违反 architecture — 向 Ledger.sj 加 import payments.app.Main;：error[E_ARCH_DENIED]: package payments.model imports payments.app ... — 分层在编译时强制。
3. 违反 capability — 在 payments.model 内加一个 new sj.net.UnixGateway() 调用：error[E_CAP_DENIED]: package payments.model performs net ... holds no net grant — 纯核心够不到外部世界，无论有什么代码落进去。
4. 发布它 — superj build --release：所有 contract 被擦除；该二进制与一个从无子句源码构建的二进制逐字节相同。

8. 它的代价

"被擦除"是经验证的，不是断言的：擦除门把一个 release 构建的 LLVM IR 与把每个子句从源码删除后的同一程序 diff，并要求它们逐字节相同。SEDA 延迟基准针对 release 构建作为回归门运行 — claim 层在你延迟预算所在之处是不可见的。invariant 仅在公开边界检查（非每次调用），因此 checked 构建代价与边界穿越次数成正比，而非调用量。

9. 与 AI agent 协作

Claim 层被设计成 AI 在其中写代码的harness。实际后果：

• claims 就是规格。 把 agent 指向 contract 与清单，而非散文。ensures 子句是它的目标函数；capability 与 architecture 行是它无法穿透的硬墙；E_* 码与 ContractViolation 消息是稳定的、机器可解析的反馈，供其重试循环使用。
• 审查 claim diff，而非代码 diff。 如果一个改动不触及 claim 且 gate 全绿，意图保持 — 合并。如果它需要新授权、新 import 边或被弱化的 ensures，那行 claim 改动正是值得你注意的东西，而编译器已经替你找到了它。
• 让依赖升级自我审问。 一个新需要 fs.read 的依赖会停住构建。"为什么一个 JSON 库现在要读文件？"就是审查问题，在合并前自动浮现。

10. 诊断参考

所有码都是稳定的 — 按码分支，绝不按散文：

运行时，仅 checked 构建：ContractViolation — 子句文本 + 源码位置。

11. 限制与 FAQ

contract 是证明吗？ 不是 — 它们是被检查的 claim：在每次 checked 运行的每条执行路径上验证（包括你的整个测试套件），而非在所有输入上证明。它们对对抗性输入的强度随你的 gate 喂给它们的语料而增长。

我能把 fs.write 限定到一个目录吗？ 暂不能 — 授权是包粒度的。可行模式：把被授权的代码隔离到尽可能小的包中（§4.3），并给它那个包它应得的逐行审查。

包 A 调用 B，B 做网络 I/O。A 需要 net 吗？ 不需要。授权在效果点检查（§3.3）。如果你想同时阻止 A 到达 B，在 architecture 中说明 — 两者组合。

invariant 在私有方法或静态方法上运行吗？ 不 — 仅构造器退出与 public/protected 方法退出（§5.2）。私有 helper 可以经过中间状态。

我怎么临时关闭 contract？ 在任何 compile 上加 --no-contracts。Release 构建自动如此。不要发布一个"checked"的生产构建来保证安全 — 那是 gate 的职责；release 意味着擦除。

在已有项目上采纳这要付出什么？ 直到你加一个键，什么都不付出。按顺序采纳：先 capabilities（一个键、即时默认拒绝、运行 superj capabilities 并收紧），再 architecture（预期首次 superj topology 会教你点什么），最后 contract（只对资金路径与核心类型 — 不要给整个世界加注解；噪音正是这一层要消除的东西）。

参见

• 构建系统 — 本页这些键所在的 Build.sj 清单。