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
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 seven grants

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

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
  at payments.model.Ledger.transfer (Ledger.sj:41)

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.

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() 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.
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:

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.