§05 — Callback Capability Propagation

Context

Per approved proposal §5. BLOCKED: cannot begin implementation until capability-propagation-completion-proposal.md ships. That draft documents three infrastructure gaps (LLVM/AOT capability support stubbed, stateful handlers partial, marker capability enforcement partial) — any one of them would make §05’s compile-time verification unsound.

When the blocker clears, the following subsections execute.

§05.1 — Unblock verification

Verify capability-propagation-completion has landed:
- LLVM/AOT capability lowering is shipped (check compiler/ori_llvm/ for uses handling).
- Stateful handler(state: S) { ... } fully implemented in eval + LLVM.
- Marker capability E1250 propagation enforced at the type-check layer.
If any gap remains, STOP; file a bug per CLAUDE.md §Bug Handling — ZERO DEFERRAL and escalate via AskUserQuestion.

§05.2 — Grammar + parser

Grammar production (ships with §08):

callback_type = "(" param_list ")" "->" type [ "uses" cap_list ] .

Parser accepts uses on callback parameter function types (currently parsed but not propagated).
AST: callback parameter types carry an optional cap_list field.

§05.3 — Subset verification at registration

In ori_types/src/check/capabilities/ (new file or extension to existing module), add fn check_callback_subset(registered_fn: &FunctionSig, callback_param: &CallbackType) -> Result<(), Diagnostic>.
Rule: registered_fn.uses ⊆ callback_param.uses. Set difference → E4019 listing the missing capabilities on the callback parameter.
Applies to every call site that passes an Ori function to a callback parameter. Detected via call-argument type-checking.

§05.4 — Handler-based capability provision at registration

When the C library provides capabilities via a callback argument (e.g., uv_timer_start passes a handle that exposes Clock), the user can write:
```
with Clock = uv_handle_clock(handle) in {
    uv_timer_start(handle: handle, cb: on_tick, ...)
}
```
The existing with Cap = handler in mechanism handles this — §05 does not add new machinery, only validates the subset check against the with-in-provided scope.

§05.5 — Matrix tests

Failing tests FIRST: a program registering a callback that uses Print when the callback parameter type declares only uses Clock → MUST emit E4019.
Matrix:
- Subset position: uses {} ⊆ uses {Clock} (OK) / uses {Clock} ⊆ uses {Clock} (OK) / uses {Clock, Logger} ⊆ uses {Clock} (E4019 — Logger missing) / uses {Clock} ⊆ uses {} (E4019 — all missing) = 4 cells.
- Callback parameter forms: explicit callback type with uses / callback type without uses (strictest default) / extern function returning a callback type (propagation) = 3 cells.
- with…in provision: capability provided via with-in AT the call site → subset check passes; capability NOT provided → E4019 = 2 cells.
Semantic pin: a compilable uv_timer_start example with on_tick uses Clock and a matching callback parameter compiles clean AND emits the callback registration through the capability-aware lowering (FileCheck for the correct LLVM IR shape once capability-propagation-completion ships).
Negative pin: any cell where the subset fails MUST emit E4019 at compile time.

§05.6 — Documentation

Update spec §26-ffi.md with §05 surface (co-commit with §08).
Update .claude/rules/ori-syntax.md Deep FFI section with callback uses propagation.

Completion Checklist

§05.R — Third Party Review Findings

None.