(sigil grant)

Capability Grants: the Value and the Algebra

An immutable authority value and the two operations that compare and narrow it. This module is PURE: it performs no filesystem access, no process access, and no I/O of any kind. It compares resource PATTERNS structurally.

What a grant is

A grant is an immutable set of facets. A facet is a three-element list (kind mode resource), and a facet is a PERMISSION — absence is denial. There is no "off" facet; a grant that does not mention pty denies pty.

(import (sigil grant))

(define g (grant-from-specs '("fs:rw:/work" "exec:allowlist:git,ls")))
(grant-covers? g (grant-from-specs '("fs:ro:/work/src")))  ; => #t
(grant-covers? g (grant-from-specs '("fs:rw:/etc")))       ; => #f

The partial order and the meet

(grant-covers? big small) is the partial order "has at least as much authority as": true iff every facet of small is permitted by some facet of big. (empty-grant) is the bottom — covered by everything, permitting nothing. (grant-allow-all) is the top.

(attenuate g narrowing) is the meet: the greatest grant covered by both. (grant-covers? g (attenuate g narrowing)) holds for ALL inputs — attenuation can never widen. This is the property every consumer of this module leans on.

grant=? is defined as MUTUAL COVERING, not as structural equality, and the choice is load-bearing rather than stylistic. An equality DERIVED from the partial order cannot disagree with the partial order. A structural equality can, and would then make a true law ("attenuate is idempotent") read false for reasons that have nothing to do with authority — a different facet ordering, or a redundant facet that is subsumed by another one. The laws in this module are claims about authority, so they are stated in the authority ordering.

Purity, and why it is not a style preference

(sigil system grant) canonicalises paths with realpath when a grant is constructed and again when a target is checked. This module deliberately does NOT. Two reasons:

1. The property tests are only meaningful over pure functions.
2. The browser/wasm target has no filesystem to canonicalise against. A grant algebra that touched the filesystem could not run there at all.

Canonicalising a concrete path against a grant, and anchoring a grant to a directory that exists, are the CHECK site's job and stay in the system profile. This module is the vocabulary they share.

Facet grammar

connect and listen are SEPARATE authorities: neither covers the other, and a grant that means "all networking" must hold both.

Resources are compared LITERALLY — this module never canonicalises. What a resource may contain is therefore constrained at construction so that the value space and the spec grammar agree (see "The spec string is an interchange format" below):

• fs paths must be absolute and may not contain a . or .. component. They MAY contain : and , — neither can split them, and realpath preserves a comma, so an ordinary directory like /home/u/Music/Artist, The must stay grantable.
• exec allowlist commands may not be empty, nor contain , or :. This is the ONLY kind where a comma is a delimiter: the exec tail genuinely splits on it.
• import prefixes may not contain :. A , is allowed — the branch takes the prefix whole, so a comma cannot split it either.
• a net host is a literal host or exactly *, and contains no /. *.io and x.io/path are both refused rather than silently taken as literal hosts matching nothing. / is structural here: it appears only in the :// scheme separator.

The test for whether a character must be refused is NOT "does the grammar use it". It is: CAN THIS CHARACTER CAUSE A VALUE TO BE READ AS MORE THAN ONE THING? Write that down before adding a facet kind, because the naive reading forbids too much and gets the two cases below backwards.

A character that is merely STRUCTURAL cannot inject: it defines what a component is, so the worst it causes is inexpressibility, not authority appearing out of nothing. Those are different defects and only the second is what §5.1a exists to stop.

Three characters are therefore deliberately carryable:

• : in an fs path. The fs branch rejoins everything after the mode, so fs:ro:/home/u/a:b is a single path and round-trips as one. The suite asserts this rather than assuming it. A naive reading would forbid : here and be wrong.
• , in an fs path or an import prefix. Neither branch splits on it — fs rejoins the tail, import takes the prefix whole. The first version of this module refused it everywhere, and that broke a real configuration: realpath preserves a comma, so a grant over /home/u/Music/Artist, The stopped being expressible. The comma is a delimiter in the exec allowlist tail, and in the env-var surface that packs a spec LIST into one string (t-deb92a) — borrowing another layer's delimiter is not this module's job, and doing so cost a working grant.
• . in an import prefix. It is the component separator, so it cannot produce an unintended component — it produces the intended ones.

ASSUMPTION, with its expiry condition, because it is an assumption and not a fact: no library-name component contains a literal dot. That holds today because a dot is not legal in those symbols. If Sigil ever admits a dot into a library-name component, this grammar becomes ambiguous and the import kind needs a different separator — it does not degrade gracefully, so check this before assuming it still holds.

The spec string is an interchange format, not a pretty-printer

Consumers persist a grant with grant->specs and reload it with grant-from-specs, so a resource whose text contains one of the grammar's own delimiters is an INJECTION — and in a capability system, injection means authority appearing out of nothing. The case that forced the rule above: an exec command "a,b" unparses to exec:allowlist:a,b, which re-parses as the TWO commands a and b. The original grant permitted neither, so the round trip WIDENED it, and the reloaded grant was not even a lower bound of the original. Such values are refused at construction rather than escaped: no real command name contains a comma, and a loud refusal when the grant is built beats a silent re-interpretation when it is loaded.

The round trip is therefore required to preserve AUTHORITY, not just to produce a string that parses — (grant=? g (grant-from-specs (grant->specs g))) for every g, which the suite asserts over its whole corpus.

Spec strings

Every spec string (sigil system grant) accepts today parses here to the same authority, and unparses back:

• fs:ro:<path> / fs:rw:<path> — the path may itself contain :
• exec:full
• exec:allowlist:<cmd>,<cmd>,... — argv[0], matched EXACTLY
• pty:on

Added by this module:

• net:connect:<pattern> / net:listen:<pattern> — the pattern may itself contain :, so net:connect:https://codeberg.org:443 parses. An IPv6 literal must be bracketed ([::1], [::1]:8080); an unbracketed host containing : is refused rather than guessed at.
• import:full / import:prefix:<dotted-prefix> — a library name is rendered dot-joined, so (sigil fs) is "sigil.fs" and the prefix "sigil" covers it. This rests on an assumption with an expiry condition; it is stated once, above, under "carryable".
• eval:on
• ffi:on

Two properties that are easy to lose and expensive to lose

Component-safe prefixes. /a/bc is NOT under /a/b. A bare string prefix test would say it is.

argv[0]-exact exec matching. An allowlist entry "git" permits argv[0] "git" and NOT "/tmp/evil/git". Matching on the basename would let any attacker-controlled binary of the same name through. To allow an absolute path, grant that exact path.

Named extension point: argv-exact

This module constrains exec by argv[0] only. Constraining the WHOLE command line — (exec (argv-exact "git" "status")), permitting git status and denying git push — is a third exec mode, added alongside full and allowlist rather than replacing either. The facet shape (kind mode resource) already carries it: mode argv-exact, resource the argv list. It belongs with the enforcement work that knows a process's real argv, not here.