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 · strict arena — 块上的那一条 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 九个授权

其中两个的强制方式与其余不同；与其从一个通过的构建里去推断，不如直接知道这一点：

• console 已声明但尚未强制。 System.out.*/System.err.* 作为代码生成的内建操作（intrinsics）下沉为 printf/fprintf，而不是作为 native 方法声明，因此在归因效果的 pass 里它们从不以 native 调用的形式出现。该授权是模型的一部分，设计决定已记录在案；要强制执行，需要这些内建携带归因。所以今天，一个没持有 console 却在打印的包照样编译。
• ffi 在声明时检查，而非在调用点：没有它的包根本无法声明 native 方法，这正是为什么到达效果 pass 的每个 native 要么是 SDK（豁免），要么声明在某处持有 ffi 的地方。

MemoryMapped 需要两个授权，因为它是两样东西：裸的非 arena 内存（memory.direct）与它所映射的文件（fs.read，映射可写时再加 fs.write — 可写映射无需任何 write() 调用就能改变文件内容）。单参数的 MemoryMapped(path) 是只读的；两参与三参形式视为可写。

无论你的包直接调用一个 native，还是经由某个 SDK 方法以任意深度到达它，都需要授权（#3362）。File.mkdirs() 需要 fs.write，尽管它只是原生 mkdir 之上的普通 SuperJ 代码；NioAdapter.open() 需要 net，因为它到达 UnixGateway 的套接字 native。编译器在构建 SDK 时从 SDK 自己的调用图推导出这一点并随 SDK 发布结果，所以答案在每个 edition 上都相同。在 #3350 之前只检查前者，因此 MemoryMapped 与 DirectArray 完全不受门控 — 而且包装一个 reader（new BufferedReader(new FileReader(p))）能逃过裸 FileReader 所要求的 fs.read。如果你正在升级，使用这些类型的包现在需要本表所列的授权。

纯计算 — 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).

“全限定使用”指类名能出现的每一个位置，而不只是那些看起来像调用的位置。字段、局部变量、参数或返回类型、throws 类型、catch 类型、cast 或 instanceof 目标、任意深度的类型实参、类型参数约束 — 以及 new pkg.C()、pkg.C.stat()、extends/implements。类型位置正是 #3922 所关闭的缺口：把跨界写成类型而非调用可以干净编译，于是一个允许列表为空的包，只要从不拼写 pkg.C.method(...)，就能持有指向项目中任何包的活引用。只被一种语法尊重的边界不是边界，所以强制执行跟随名字，无论它写在哪里。

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 in payments.model.Ledger.transfer at src/model/Ledger.sj:41

（#3257 把本示例修正为实际发出的文本。它把两行形式所承诺的同样四样东西 — 类型、子句文本、包限定的 Class.method、file:line — 放到一行上，这对 grep 与日志采集更友好。工单提交时它是 ensures clause 1 at :41：没有子句文本、没有方法、只有不带文件的行号。）

（#3923：子句携带作者自己的空格，因此被引用的文本与源码一致、可以对源码 grep — 是 requires helper(x) < 5，而不是 requires helper ( x ) < 5。它从各 token 记录的列重建，并带有两处单行消息所强制的归一化：连续空格折叠为一个，跨源码行的子句以一个空格相连。）

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 — 它证明不会有东西悄悄让你的分配画像回归；你自己的基准套件仍是实际纳秒的度量。

6.1 strict arena — 块上的那一条 claim

pure 与 noalloc 是关于方法的 claim。strict arena 是关于块的 claim：块内分配的任何东西都不比它活得久。违规：error[E_ARENA_ESCAPE]，在逃逸的分配处。

strict arena tmp {
    Buffer b = new Buffer(1024);   // dies here — fine
    cache.put(k, new Entry(r));    // error[E_ARENA_ESCAPE]
}

它存在的原因是：普通 arena 块是一个提示，不是 claim。一个比块活得久的值会被放到某个更长寿的位置，程序依然正确 — 于是块回收碰巧死在它里面的东西，而对其余的静默不管。在没有任何东西死在它里面的那种形状下，实测峰值 RSS 12.6 倍（2.5M 次分配中 82.9 MB 对 6.6 MB），同时干净编译、正确运行。在 strict 出现之前，这是该语言中唯一一个以退化而非失败来表现的内存断言。

它的阈值刻意不同于你在普通块上得到的 W_ARENA_NO_SAVINGS 警告。那个警告只在每一个分配都逃逸时才触发，因为一个圈住十个临时量、逃逸一个结果的块正是预期的惯用法。在 strict 之下，任何逃逸都是错误 — 你已经说过它不应发生。所以 strict 还能抓住那个警告抓不住的回归：一个作用域圈得正确的块，明年有人往里加了一个 cache.put(...)，它仍然圈住其余九个、因此保持安静。

与 pure、noalloc 一样，它是可选加入（opt-in）的，而这个理由值得理解、而不是绕过。区域推断只朝一个方向保守：它会把任何它无法证明死在块内的分配提升出去。所以 strict 块可能拒绝事实上安全的代码，而选择加入，就是你在为一个你真正在乎其回收的块接受这笔交换 — 而不是让它被强加给程序中的每个块。

strict 是一个上下文关键字：只在紧邻 arena 之前被识别。名为 strict 的变量、字段或方法照样编译。

打开它之前，有一件事值得知道：

• 判定不取决于你的 edition。 每个 SDK 都附带一份其自身方法各自保留什么的摘要（<sdk>/build/escape-summaries.txt），因此归档构建（--sdk-path，默认）与全程序构建（--sdk-source）对同一个 strict 块判定一致，且 superj check 与 build 意见一致。在 #3361 之前，归档构建没有这份摘要，并假设每个 SDK 方法都保留你传给它的东西，于是同一份源码被一个 edition 接受、被另一个拒绝 — claim 必须是你的程序的属性，而不是你装了哪个 tarball 的属性。

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 — 纯核心够不到外部世界，无论有什么代码落进去。（裸的 new sj.net.UnixGateway() 本身不会触发 — 构造器没有 native 调用，只有 openUdpSocket() 这类实例方法才到达被门控的效果。）
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. 诊断参考

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

上面每个码都由 superj check 报告，包括 E_ARENA_ESCAPE（#3360 阶段 2）— 对它，check 只在程序确实包含 strict arena 块时才运行区域推断。

运行时，仅 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 清单。