ch:effect-capabilities: ch:effect-capabilities

Problem, result, and invariant. Implement the chapter’s finite distinction between operation presence and handler authority. Keep operation names, handler identities, runtime labels, authorities, handler stacks, closure classes, a small Effekt source, and a small System-$\mathsf{Xi}$ target separate. The observable result is the ten-case report in Appendix E. The central invariant is conditional on validation: in a stack with pairwise distinct active identities and labels, every successful authorized request reaches the unique frame whose identity, operation, and label match its authority. A second-class closure may not escape its capability scope, and a capability may not be used outside its active label.

Representation. Use distinct nominal datatypes for operation names, handler identities, labels, and authorities. A handler frame stores all three identifying components and a visible result tag. A request is authorized by an explicit identity and label, dynamically searched by operation name, or tunneled toward one identity. A closure records its authority and whether it is first or second class. Begin every public operation by validating that identities and labels are unique. Invalid stacks return a validation error; first-match lookup is never allowed to masquerade as uniqueness. One shorter alternative uses a single string domain for operation names, handler identities, and labels, with dispatch by string equality. It is shorter, but then accidental capture and the name-only-authority mutation are indistinguishable from correct behavior, so the oracle cannot separate them.

First complete version. Start with two same-operation frames, $$h_{\mathsf{outer}}=(\mathsf{Tick},{\ell }_{\mathsf{outer}},42),h_{\mathsf{inner}}=(\mathsf{Tick},{\ell }_{\mathsf{inner}},7),$$ with the inner frame dynamically nearer. Authorized search compares handler identity, operation, and label; naive search compares only operation names. The first complete run must therefore report both an outer authorized result and an inner accidental-capture result. Add the equal-name/distinct-identity case immediately: equality of operation strings must not grant authority.

Closures and label scope. Store the outer authority in a first-class closure and invoke it after an abstraction-boundary marker. The nearer inner handler remains irrelevant. Then add a second-class closure and reject its attempted escape. A separate scope check compares the authority label with the active runtime label; a same-operation handler at a different label is insufficient. These are finite observations of the System-$\mathsf{Xi}$ boundary, not its proof theory.

Finite translation and tunnelling. Give the source handler node an explicit identity and label. Validate both source identities and labels for uniqueness, then translate by copying those supplied names into the capability environment and target syntax. The translator does not allocate or establish freshness on its own; validation establishes the finite precondition. Inspect one accepted translation, one identity-only duplicate, and one distinct-identity/same-label duplicate.

For tunnelling, search by the requested handler identity. The search may cross an intervening same-operation frame and stops only at the matching identity. Thus the tunneled case returns the outer result while naive dynamic lookup on the same validated stack returns the inner result.

Five failing versions. Replay the mutations in MUTATIONS.md separately:

1. compare operation names instead of identities in authorized dispatch;

2. implement tunnelling by nearest-name lookup;

3. allow a second-class closure to escape;

4. skip active-stack validation; and

5. skip source validation before translation.

All five mutants still parse and typecheck. The two validation cases each conjoin an identity-only negative input with a label-only negative input, so removing either freshness comparison is observable. Each mutant flips a permanent case; the exact stdout oracle and typed acceptance error expose the defect.

Acceptance test. Run the four PATH-based commands from Appendix E. Require all ten named PASS lines, the final

All 10 Chapter 32 corpus cases passed.

and audit output []. Replay each recorded mutation, require kappa test and kappa run to fail, restore the accepted corpus hash, and rerun the four accepted commands.

Mathematical boundary. The artifact illustrates handler identity, validation, label scope, second-class escape, finite syntax translation, and tunnelling. It proves none of System-$\mathsf{Xi}$ progress or preservation, the complete Effekt translation, effect safety, tunnelling parametricity, type safety, logical soundness, or compiler correctness.