Amended 2026-10-04. The law stands, the mechanism below is gone. evaluate_exec, reduce_exec, admitted_literal_paths and the deny_basenames carve dimension no longer exist: the in-process guard and the kernel read one compiled table, ExecRules, the guard through ExecRules::verdict and the kernel through ExecRules::kernel, a rule list ordered so that last-match-wins equals the guard’s precedence. The projection is rendered from the very table that admitted the launch (Admitted), so there is nothing left to defer to and no differential test to keep; two property tests pin the meet and the render instead. A bare deny is still a final-component veto in Seatbelt. See exec-rules and exec-carriers; since 2026-10-06 the table is the generic Table<ExecScope> (one-table-two-instances).

The exec projection defers admission to the gate

The OS exec projection’s admit decision is the in-process gate’s verdict, queried once per nameable command — not a second, parallel derivation of it. Two enforcers (capability-enforcement) mean two folds (exec-authority-partitioned): the check fold evaluate_exec threads a subject through the stack to a yes/no, and the projection fold reduce_exec materialises the closed region set macOS Seatbelt tests subjects against. They are dual, and stay two. But the projection half had been re-deriving admission on its own, and the derivation was lossy.

The silo fold lost cross-shape admission

A layer admits a command two ways — a literal key (git, /usr/bin/git) or a covering allow-dir (/usr/bin/) — so admission inside one layer is literal OR dir. reduce_exec composed the stack by intersecting the two shapes in separate silos: literals ∩ literals, dirs ∩ dirs. That loses any admission that crosses shapes. With layer A = {git: Allow} (literal) and layer B = {/usr/bin: Allow} (dir), asked about /usr/bin/git:

• the check fold says admit — A via the literal, B via the dir, met;
• the silo projection collapsed both halves to empty → Restricted { allow_paths: [], allow_dirs: [] } → Seatbelt denied a spawn the in-process gate had already run.

Fail-closed (the stricter surface won, no escalation), but a real functional inconsistency: a nested grant { exec: [git: allow] } under a session that granted /usr/bin by directory ran in-ral and died under the macOS sandbox. The structural lattice laws were all tested; this semantic law — enforcing the projection agrees with enforcing the stack — was neither stated nor tested, which is why it slipped.

The fix: enumerate the names, ask the gate

admitted_literal_paths (then core/src/capability/sandbox.rs; the fold is now SandboxProjection::of) draws candidates from the raw union of every layer’s literal keys — not a meet-folded map — resolves each to the absolute path the OS names, and keeps it only where evaluate_exec admits its natural invocation (allow-narrow = key + resolved path; deny-broad adds the resolved basename, so a sibling git: Deny still vetoes). The dir dimension still materialises as intersected subpaths. So the projection admits a path only where the gate does, by construction.

This does not collapse the two folds — 260602’s duct-tape objection stands: there is no shared subject-free intermediate, and Subcommands still flattens onto the coarser path-level lattice (Allowed(_) → list the path; the OS layer cannot gate argv). The materialisation fold simply invokes the query fold over the finite candidate set instead of paraphrasing it. meet_literal_exec had no other caller and is now private.

Bare-name denies project by basename, not by resolved path

A bare git: Deny is basename-scoped in the gate: it vetoes the name wherever it resolves. Projecting it as one PATH-resolved literal left the deny reachable through a covering allow-dir by an interpreter the gate never sees (sh -c git), and lost entirely when the name resolved somewhere other than its runtime path. Denied literals now split by shape:

• absolute (/usr/bin/git: Deny) → deny_paths, a path literal;
• bare (git: Deny) → deny_basenames, rendered as a (deny process-exec (regex #"/git$")) final-path-component match — path-agnostic, no PATH dependence, exec-scoped only (the gate’s basename veto never denies reads).

The three carve dimensions — deny_paths / deny_dirs / deny_basenames — now mirror the three shapes the exec veto takes. This retires the older framing that per-name denies inside an admitted dir were solely the in-process gate’s job; the OS layer enforces them too, closing that slice of the interpreter-bypass class.

What stays approximate, safely

Capabilities::meet — the pre-mash that folds several profiles into one session ceiling before any command exists (exarch) — keeps the silo fold and stays fail-closed. Its exactness would need to resolve a name against a covering dir, and it has no resolver and no subject; no representation makes git ∧ /usr/bin exact without one. So a name meant to survive a directory-only ceiling is written as its absolute path there. This is the one place the surfaces still differ, and only ever in the safe direction.

The safe direction is now a CI-enforced invariant: a differential conservatism test (grant_policy.rs) asserts the projection never admits a resolved path the gate denies, over adversarial two-layer stacks — including a nested-basename case a single PATH-resolved literal would have missed. A functional regression test asserts the cross-shape literal reaches allow_paths and the gate agrees.

See also capability-enforcement, exec-authority-partitioned, capability-carriers, two-enforcers; map capabilities. docs/SPEC.md §12.