Module authority 

Authority derivation: the least Grant a program provably needs, and what a change did to it.

trust answers “does this effect fit that grant?”. This answers the other direction — what grant does this code require? — which is a question only an effect system can answer soundly. The declared effect rows are a static over-approximation of every path through the body, and crate::check_program has already rejected any row that lies about its body, so folding those rows into a grant yields authority the program cannot exceed. A dynamic trace reports what one run touched; this reports what every run could.

Two consequences fall out, and both are processes rather than checks:

• A sandbox can be derived instead of written. The fold is minimal by construction — the level on a dimension is the join over the effects that touch it — so nothing in the result is there because someone was being careful. Authority::minimality_witness makes that checkable rather than claimed: for each dimension it names the effect that the next rank down would reject.
• A change has an authority delta. diff classifies two derivations as Verdict::Widening, Verdict::Narrowing or Verdict::Unchanged. A source diff says what the code now does; this says what it may now reach, which is the reviewable form of the same change.

The honest limits, stated once

The trust lattice ranks three dimensions. Plenty of effects sit outside it — env, sql, approval, chat, kv — because effect_requirement maps them to no dimension, so no grant refuses them. A grant-only comparison would therefore show nothing when a program starts reading environment variables. Authority::off_lattice and AuthorityDiff::off_lattice_added report them separately: present in the review, while being honest that no perimeter is what stops them.

Network reach has a second limit. std.net.get carries a bare [net] — its URL is a runtime value — so the type level binds no host. Authority::unscoped_net records that, and the static answer narrows to “may reach the network at all”; which host is a perimeter question. Consumers must not narrow an egress allowlist against a derivation carrying it.

Structs

Authority

The authority a program requires, derived from its own types.

AuthorityDiff

The authority delta between two versions of a program — the artifact a reviewer reads next to the source diff.

DimensionDelta

One dimension’s movement between two derivations.

MinimalityWitness

One dimension’s proof that the derived level is not a rank too generous: at lowered_to, rejected_effect no longer type-checks.

Enums

Verdict

How a change moved a program’s authority.

Functions

derive_from_effects

Derive the least authority an EffectSet requires.

diff

Compare two derivations.

next_level_down

The level one rank below level on dim, or None if level is already the bottom of that dimension’s ladder.