Under a grant

Status: measured, and it falsifies a sentence in reach.md §5.2.

README.md and authority.md both say authority --output json gives the report “for a supervisor checking it against a grant”. No supervisor had ever been asked. This takes lex-os’s real grant and tries to write the check.

One of its three dimensions is enforceable and cancho is finer than the grant asks. Two are not enforceable at all. And the field reach.md §5.2 offers as covering the difference is a proof about names and a heuristic about domains — six lines defeat it.

1. The two shapes

lex-os’s grant, from demo/manifest.json:

"grant": { "filesystem": "Full", "network": "Allowlist", "exec": "Full" },
"egress": ["results.demo.internal:443"]

Three dimensions and a host allowlist. A cancho authority report, for examples/cut/:

{
  "effects": ["args", "err_write", "heap", "io_read", "io_write"],
  "labels": [{ "name": "args", "argument": null }, ...],
  "foreign_symbols": []
}

The question is whether a supervisor holding the first can decide the second.

2. One dimension at a time

The two no’s are one no. Here is examples/serve/, which binds a TCP port, listens, accepts a connection and answers HTTP:

{
  "effects": ["args", "ffi"],
  "labels": [{ "name": "args", "argument": null },
             { "name": "ffi",  "argument": "libc" }]
}

A program that runs a network server reports args and ffi. The row is not wrong — reach.md §5 argues that correctly, and the argument holds: the row is exact about what the program was granted, which is a C library. It is silent about the network because libc is not an authority domain.

What is new here is the consequence. Against a grant that says network: None, this report is not merely coarse. It is unable to refuse, and the only cancho program in this repository that touches the network is the one it cannot refuse.

3. The symbol list is a proof about names

reach.md §5.2 offers the foreign symbol list as what covers the difference, and says a supervisor reading socket, bind, listen, accept

“knows it is being asked to run a server, and knows it without trusting a word the program says about itself.”

The first half is right and the second half is not. Six lines:

extern fn syscall[&f](ffi: &f Ffi("libc"), n: int, a: int, b: int, c: int)
    -> [ffi("libc")] int;
...
r = syscall(f, 41, 2, 1, 0);        // SYS_socket, AF_INET, SOCK_STREAM

It type-checks. Its report:

{ "effects": ["ffi"], "foreign_symbols": ["syscall"] }

Neither field says network, and the program opens a socket.

The list is sound about what it claims: every foreign call needs a declaration, so foreign_symbols is exactly the set of foreign names reachable from main, and that is a proof in the same way the row is. The step that is not a proof is the next one — from a name to a domain. socket suggests a socket because C’s authors named it that, and the declaration in a cancho program is written by the program’s author, who may choose syscall, or a wrapper, or a name from a library whose domains nobody has enumerated.

So: a proof about names, a heuristic about domains. Against a cooperative program the heuristic is informative and worth having. Against the threat model lex-os exists for — “the agent is not trusted” — a heuristic is not a wall.

§5.2 is corrected in place.

4. The diagnosis, in one sentence

Every capability in this language bounds what it authorises, except one.

reach.md §5 says this as a limit on narrowing. It is larger than that: Ffi(lib) is the one capability whose label does not bound what it authorises, and every authority domain the language has not yet named is reachable through it under a single grant.

That is also why the filesystem row above is the one that works. filesystem.md §2 took files out of libc and made them builtins under Fs(p), and the reason the grant’s filesystem dimension is enforceable today is that someone already did the thing §5.1 describes for sockets.

5. What this promotes

reach.md §6 carries “sockets as builtins under Net(host)” as an open row, and §5.1 frames the argument as a question of taste — “a host is a thing worth narrowing to” — with the honest note that adding Net without taking sockets out of libc would produce a row that lies.

That framing was right and is now incomplete. The row is the prerequisite for cancho code running under a lex-os grant at all, because two of that grant’s three dimensions cannot be decided without it. It is not “the row should be finer”. It is “the row cannot answer the question the runtime asks”.

The roadmap’s lex-os join moves accordingly: it is not blocked on a compiler integration, and the supervisor does not need to embed the cancho front end — authority --output json is already the right interface and filesystem already works through it. It is blocked on the effect vocabulary, which has one label where the grant has three dimensions.

5.1 And the report now fails closed (#75)

Until Net exists, the report can at least stop being calm about what it cannot see. An outside audit proposed it and it is the cheapest correct thing available:

{
  "bounded": false,
  "effects": ["args", "ffi"],
  "labels": [
    { "name": "args", "argument": null,   "bounded": true },
    { "name": "ffi",  "argument": "libc", "bounded": false }
  ],
  ...
}

bounded is the first field, so it is the one a consumer that reads nothing else reads, and it is false whenever any reachable label fails to name its own domain — which today means exactly ffi. The prose report opens with UNBOUNDED and marks the label.

What this does and does not change:

• A supervisor that refuses on bounded: false now refuses examples/serve/ under any grant, including one where it would have been allowed. That is the point of failing closed: the default is safe, and admitting a particular unbounded program is a decision about that program, which the report should not make on the supervisor’s behalf.
• It does not make the network enforceable. It makes the absence of enforcement impossible to miss. Net is still §5’s prerequisite.
• The foreign symbol list stays, for the supervisor that does decide to read further — §3’s heuristic, now clearly labelled as one.

6. What this does not say

• Not that the report is broken. It is exact about what it claims, and the filesystem dimension is enforceable more precisely than the grant can express. What it cannot do, it cannot do for a reason that is written down.
• Superseded in part by foreign-authority.md. bounded: false is now accompanied by unbounded_by, the exact scope:symbol pairs it is made of, so a supervisor decides over symbols and a CI pin diffs an added one; bounded keeps the meaning given in §5.1. The “proof about names, heuristic about domains” of §3 stands unchanged: the report still cannot say what a symbol does. That document also closes a hole this one missed: an extern fn with no Ffi at all was accepted and reported bounded: true.
• Not that foreign_symbols should go. It is the best available signal and reach.md §5.2’s first half stands. What changes is the sentence claiming it needs no trust.
• Not a lex-os change. Nothing here asks that repository for anything; the gap is on this side, and so is the fix.
• Not that syscall is a hole to be plugged. Refusing that one name would be theatre — the next spelling is a wrapper. The hole is Ffi(lib)’s width, not any symbol’s name.
• The symbol list is reachability-pruned now. authority.md §3 found it briefly was not: Program::externs lists every extern fn declared in the compiled unit, and until this was fixed that meant every one, not only the ones a reachable call site actually calls — surfaced once a program (examples/fetch/fetch.cho) imported a package declaring more than it calls. cancho-ir::reachable_externs closed it: the report is now exactly what main reaches, the same promise §3 above already made for effects.

7. The suite