The Claim Layer: Capabilities, Architecture & Contracts

The claim layer lets you state your intention — what each part of your program may do, how it is shaped, and what it must guarantee — as a thin set of declarations that the compiler enforces on every build. You ratify the claims; the compiler holds every line of code to them, including the lines you didn't write yourself.

It has zero runtime cost in release builds — capabilities, architecture, pure, and noalloc never exist at runtime in any build, and contracts are erased from release binaries (verified byte-identical, see §8).

This page is the complete how-to, from the five-minute quick start to a fully worked example.

Contents

1. Five-minute quick start
2. The claims at a glance
3. Capabilities — what code may do
4. Architecture — what code may import
5. Contracts — what code must guarantee
6. pure and noalloc — one-word method claims · strict arena — the one claim on a block
7. A complete worked example
8. What it costs
9. Working with AI agents
10. Diagnostics reference
11. Limits & FAQ

1. Five-minute quick start

In any existing project (a directory with a Build.sj):

Step 1 — declare capabilities. Add one key to Build.sj:

// flat pairwise (package-or-dependency, grants) — same shape as `dependencies`
static final String[] capabilities = {
    "myapp", "net, fs.read",
};

Step 2 — check. superj check. If a package performs an effect it has no grant for, you get a located, actionable error:

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.

Step 3 — see what you actually use.

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

Tighten until granted equals used. That's least privilege, as a one-line diff. Everything else on this page is elaboration.

The one rule to understand: the moment the capabilities key exists — even empty — the project flips to default-deny: any package not listed holds no capabilities. No key = unrestricted (the pre-claim-layer behavior). There is no partial mode.

2. The claims at a glance

3. Capabilities

3.1 The nine grants

Two of these are not enforced the way the rest are, and it is better to know that than to infer it from a passing build:

• console is declared but not yet enforced. System.out.*/System.err.* lower to printf/fprintf as codegen intrinsics, not as native method declarations, so they never appear as native calls in the pass that attributes effects. The grant is part of the model and the design decision is recorded; the enforcement needs the intrinsics to carry an attribution. So a package that prints without holding console compiles today.
• ffi is checked at declaration time, not at the call site: a package without it cannot declare native methods at all, which is why every native reaching the effect pass is either SDK (exempt) or declared somewhere that held ffi.

MemoryMapped needs two grants because it is two things: raw non-arena memory (memory.direct) and a file it maps (fs.read, plus fs.write when the mapping is writable — a writable mapping changes file contents with no write() call anywhere). The one-argument MemoryMapped(path) is read-only; the two- and three-argument forms count as writable.

A grant is required whether your package calls a native directly or reaches one through an SDK method, at any depth (#3362). File.mkdirs() needs fs.write even though it is ordinary SuperJ code over the native mkdir, and NioAdapter.open() needs net because it reaches UnixGateway's socket natives. The compiler derives this from the SDK's own call graph when the SDK is built and ships the result, so the answer is the same on every edition. Before #3350 only the first was checked, so MemoryMapped and DirectArray were gated by nothing at all — and wrapping a reader (new BufferedReader(new FileReader(p))) escaped the fs.read that bare FileReader required. If you are upgrading, packages that use these types now need the grants this table lists.

Pure computation — Math, collections, String, parsing, crypto over buffers — is gated by nothing and needs no grant. ffi matters more than it looks: a package without it cannot declare native methods, so it cannot create effects the checker doesn't know about.

3.2 Declaring grants

In Build.sj, flat pairwise entries — the same shape as dependencies. Keys are your project package names or dependency names; values are comma-separated grants (empty string = pure):

static final String[] capabilities = {
    "payments.app", "net, fs.read",
    "httpkit",      "net",
    "jsonlib",      "",
    // payments.model, payments.wire: unlisted = no capabilities.
};

Listing a package with "" and not listing it mean the same thing (no grants); list it explicitly when you want the review record to say "pure on purpose."

Dependencies cannot self-grant. Grants live only in your Build.sj. Nothing inside a dependency's own files can widen what it may do inside your program. When you bump a dependency and it suddenly needs an effect it didn't need before, your build stops with E_CAP_DENIED until you grant it — deliberately, in a reviewable one-line diff. That is the supply-chain checkpoint working as designed.

3.3 Where the check happens (and doesn't)

The check is at the effect site: the package whose source contains the capability-gated call must hold the grant.

• payments.app calling httpkit's public API does not need net itself — httpkit holds it. Grants are non-transitive.
• The SDK (sj.*) is exempt: importing sj.http is not the effect; calling into the network from your package is.
• Whole-program: the checker sees every call edge (dependencies are compiled from source), so the answer is complete, not heuristic.

To also control who may reach an effect-holding package, pair capabilities with architecture (§4) — a package with no net grant and no import path to any net-holding package cannot cause network I/O at all.

3.4 The least-privilege report

superj capabilities (from the project directory) prints the effective grant map and the granted-vs-used delta:

$ 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

Run it after any significant change. A never used warning is an envelope wider than its contents — attack surface carried for free. If the manifest has no capabilities key it prints no capabilities declared — project is unrestricted and exits 0.

3.5 Single-file compiles (no Build.sj)

For one-off superj compile runs, the same map can be passed directly:

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

Semicolon-separated pkg=caps entries, caps comma-separated. Passing --capabilities "" still flips to default-deny. --architecture takes the same format. In a project, prefer the manifest — the build system passes the flags for you.

4. Architecture

4.1 Declaring the shape

One key, same pairwise shape: (package, allowed-imports) where allowed imports are project packages and dependency names:

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

Complete or absent. If the key exists, every project package must have an entry — a missing package is a manifest error. A half-declared architecture is a half-true diagram, so partial declaration is not representable. (sj.* imports are always permitted and never listed.)

An import — or fully-qualified use — outside a package's allow-list is rejected at check time:

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

"Fully-qualified use" means every position a class name can appear in, not just the ones that look like calls. A field, local, parameter or return type, a throws type, a catch type, a cast or instanceof target, a type argument at any depth, a type-parameter bound — and new pkg.C(), pkg.C.stat(), extends/implements. Type positions were the gap #3922 closed: writing the boundary crossing as a type rather than as a call compiled clean, so a package whose allow-list was empty could hold a live reference into any package in the project as long as it never spelled pkg.C.method(...). A boundary that only one syntax respects is not a boundary, so the enforcement follows the name wherever it is written.

4.2 Seeing the real graph

$ superj topology

prints the dependency graph derived from source — always available, declared or not — and, when architecture is declared, the declared view alongside. Expect the first run on an existing codebase to be educational: fix the graph or fix the declaration, and from that commit on the architecture cannot drift silently — a violating import does not compile.

4.3 The shape that pays

Structure packages by effect, not by feature: a pure core (domain logic, no grants, imports nothing or nearly so) and a thin effectful edge (the one package holding net/fs.*/exec). The pure core becomes freely regenerable and cheap to trust; the dangerous surface becomes small enough to actually read line-by-line. If a package needs a scary grant, the first move is to make that package smaller.

5. Contracts

5.1 requires and ensures

Clauses sit between the signature and the body. requires is checked at entry; ensures at every return, where result names the return value (typed as the return type):

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

Multiple requires/ensures clauses are allowed; each is checked independently and reported by its own text.

5.2 invariant

A class member; the expression may use the instance's fields and pure methods:

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

Checked at constructor exit and every public/protected method exit — never on private/internal calls, never on static methods. So a private helper may pass through a temporarily-invalid state; what's guaranteed is that the object is valid whenever control returns across its public boundary.

5.3 assert

Java's syntax, inside any body:

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

5.4 Contract expressions must be pure

Any method called inside a requires/ensures/invariant/assert expression must be pure (§6) — otherwise error[E_CONTRACT_IMPURE] at compile time. This is not pedantry: a contract with side effects would make checked and release builds behave differently, which is the one thing the claim layer exists to prevent. In practice this means: give your classes small pure accessors (balanceCents(), size()) and write contracts in terms of those.

5.5 What happens on violation

In checked builds, a violated clause throws ContractViolation, naming the clause and the source location:

ContractViolation: ensures result == cents in payments.model.Ledger.transfer at src/model/Ledger.sj:41

(#3257 corrected this example to the text actually emitted. It carries the same four things the two-line form promised — type, clause text, package-qualified Class.method, and file:line — on one line, which greps and log-ships better. It said ensures clause 1 at :41 when the ticket was filed: no clause text, no method, and a line number with no file.)

(#3923: the clause carries the author's own spacing, so the quoted text matches the source and greps against it — requires helper(x) < 5, not requires helper ( x ) < 5. It is reconstructed from the tokens' recorded columns, with two normalisations a one-line message forces: a run of spaces collapses to one, and a clause spanning source lines joins with one space.)

A ContractViolation is a bug report, not a recoverable condition — it means the code no longer does what its signature promises. Fix the code (or, after genuine reflection, the claim); don't catch it.

5.6 When contracts run

Contracts are on by default — superj build, superj run, superj test, and the golden gates all check them, so your entire test corpus exercises every clause from the day you write it. They are erased in release: superj build --release compiles them out entirely (the release profile passes --no-contracts; you can pass it yourself on any compile to opt out). There is deliberately no runtime toggle — a release binary either carries no checks or it isn't a release binary.

5.7 Nullness at a method boundary

SuperJ has no Optional type and no @Nullable/@NonNull annotation. Nullness at a method boundary is expressed with the contract clauses above — one line at the signature, checked in dev/test builds, erased in release:

// A lookup that never returns null:
Node find(int key) ensures result != null { ... }

// A lookup that may return null (the caller must check):
Node maybeFind(int key) { ... }

// A method that demands a non-null argument:
void use(Node n) requires n != null { ... }

This covers the cross-method case: a caller who ignores a documented null return and passes the value to a requires n != null method is caught in every checked run. What it does not do is compile-check a direct dereference of a maybe-null local (n.key where n came from maybeFind and was not guarded) — that is a local defect, visible in the body you are already reading, and a flow-sensitive checker for it is recorded as a parking-lot item in the design rather than shipped today. The honest guidance: return null for "not found" (not an exception — see the language reference on exception handling), and guard it at the call site before dereferencing.

6. pure and noalloc

Two method modifiers, checked at compile time by whole-program reachability, costing nothing at runtime in any build. They compose: public pure noalloc long bestBid() is the strongest two-word signature in the language.

pure — this method reaches no capability-gated effect, writes no static field, and calls only pure methods. Arena allocation is allowed (allocation is not an observable effect). Violation: error[E_IMPURE].

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

Use it on domain logic and on anything a contract needs to call. It's also the strongest single-word documentation a reader can get.

noalloc — this method allocates nothing: no new, no string concatenation, no allocation-reaching native, on any path — and calls only noalloc methods. Violation: error[E_NOALLOC], at the allocating expression:

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

The transitivity is the point: one noalloc on your steady-state entry point pins the entire call tree beneath it. The generated "quick fix" that formats a log string three calls down does not compile. Mark the hot-path root, and keep warmup/reconnect paths (which may allocate freely) outside it.

noalloc is a mechanism claim, not a timing claim — it proves nothing can regress your allocation profile silently; your own benchmark suite remains the measurement of actual nanoseconds.

6.1 strict arena — the one claim on a block

pure and noalloc are claims about a method. strict arena is a claim about a block: nothing allocated inside it outlives it. Violation: error[E_ARENA_ESCAPE], at the escaping allocation.

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

It exists because a plain arena block is a hint, not a claim. A value that outlives the block is placed somewhere longer-lived and the program remains correct — so the block reclaims whatever happens to die in it and silently not the rest. In the shape where nothing dies in it, that measured 12.6× peak RSS (82.9 MB against 6.6 MB over 2.5M allocations) while compiling clean and running correctly. Until strict, this was the only assertion about memory in the language that degraded instead of failing.

The threshold is deliberately different from the W_ARENA_NO_SAVINGS warning you get on a plain block. That warning fires only when every allocation escapes, because a block that scopes ten temporaries and escapes one result is the intended idiom. Under strict, any escape is an error — you have said it must not happen. So strict also catches the regression the warning cannot: a correctly-scoped block that someone adds one cache.put(...) to next year, which still scopes the other nine and therefore stays quiet.

Like pure and noalloc it is opt-in, and for a reason worth understanding rather than working around. Region inference is conservative in one direction: it promotes any allocation it cannot prove dies in the block. So a strict block can reject code that would in fact have been safe, and opting in is how you accept that trade for a block whose reclamation you actually care about — rather than having it imposed on every block in the program.

strict is a contextual keyword: recognized only immediately before arena. A variable, field or method named strict still compiles.

One thing worth knowing before you switch it on:

• The verdict does not depend on your edition. Every SDK ships a summary of what its own methods retain (<sdk>/build/escape-summaries.txt), so an archive build (--sdk-path, the default) and a whole-program build (--sdk-source) judge the same strict block the same way, and superj check agrees with build. Before #3361 the archive build had no such summary and assumed every SDK method kept whatever you passed it, so the same source was accepted by one edition and rejected by another — a claim has to be a property of your program, not of which tarball you installed.

7. A complete worked example

A minimal claimed project you can type in and try. Layout:

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: unlisted = pure.
    };

    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());
    }
}

Run it:

$ superj run
withdrew 30, balance 70

Now break each claim and watch it defend itself:

1. Violate a contract — in withdraw, change the body to balance = balance - cents - 1; and superj run: ContractViolation: invariant balance >= 0 (drain the account) or a failed ensures — the business rule catches the off-by-one your tests might not.
2. Violate the architecture — add import payments.app.Main; to Ledger.sj: error[E_ARCH_DENIED]: package payments.model imports payments.app ... — layering enforced at compile time.
3. Violate a capability — add a new sj.net.UnixGateway().openUdpSocket() call inside payments.model: error[E_CAP_DENIED]: package payments.model performs net ... holds no net grant — the pure core cannot reach the world, no matter what code lands in it. (Bare new sj.net.UnixGateway() on its own does not fire — the constructor has no native call, only the instance methods like openUdpSocket() reach the gated effect.)
4. Ship it — superj build --release: all contracts erased; the binary is byte-identical to one built from source with no clauses at all.

8. What it costs

"Erased" is verified, not asserted: the erasure gate diffs the LLVM IR of a release build against the same program with every clause deleted from source and requires them byte-identical. The SEDA latency bench runs against the release build as a regression gate — the claim layer is invisible where your latency budget lives. Invariants are checked at public boundaries only (not per-call), so checked-build cost is proportional to boundary crossings, not call volume.

9. Working with AI agents

The claim layer is designed to be the harness an AI writes code inside. Practical consequences:

• The claims are the spec. Point the agent at the contracts and the manifest, not at prose. ensures clauses are its objective function; capability and architecture rows are hard walls it cannot generate through; E_* codes and ContractViolation messages are stable, machine-parseable feedback for its retry loop.
• Review the claim diff, not the code diff. If a change touches no claims and the gates are green, the intention held — merge. If it needs a new grant, a new import edge, or a weakened ensures, that one-line claim change is exactly the thing deserving your attention, and the compiler has already found it for you.
• Let dependency bumps interrogate themselves. A dep that newly needs fs.read stops the build. "Why does a JSON library read files now?" is the review question, surfaced automatically, before merge.

10. Diagnostics reference

All codes are stable — branch on the code, never the prose:

Every code above is reported by superj check, including E_ARENA_ESCAPE (#3360 phase 2) — for which check runs region inference only when the program actually contains a strict arena block.

Runtime, checked builds only: ContractViolation — clause text + source location.

11. Limits & FAQ

Are contracts proofs? No — they are checked claims: verified on every executed path in every checked run (which includes your whole test suite), not proven over all inputs. Their strength against adversarial input scales with the corpus your gates feed them.

Can I scope fs.write to a directory? Not yet — grants are package-coarse. The working pattern: isolate the granted code in the smallest possible package (§4.3) and give that package the line-level review it deserves.

Package A calls B, and B does network I/O. Does A need net? No. Grants are checked at the effect site (§3.3). If you also want to stop A from reaching B, say so in architecture — the two compose.

Do invariants run on private methods or statics? No — constructor exit and public/protected method exit only (§5.2). Private helpers may pass through intermediate states.

How do I turn contracts off temporarily? --no-contracts on any compile. Release builds do it automatically. Don't ship a "checked" production build for safety — that's what the gates are for; release means erased.

What does adopting this cost on an existing project? Nothing until you add a key. Adopt in order: capabilities first (one key, instant default-deny, run superj capabilities and tighten), architecture second (expect the first superj topology to teach you something), contracts third (money paths and core types only — don't annotate the world; noise is what this layer exists to remove).

See also

• The Build System — the Build.sj manifest this page's keys live in.