Capability Model

This page is the canonical reference for Telltale’s first-class protocol-critical capability model.

The model is intentionally narrow. It covers protocol-critical authority, evidence, finalization, handoff, and reconfiguration/runtime-upgrade semantics. It does not define a general-purpose application authorization framework.

Scope Boundary

In scope:

• protocol-critical capability semantics that change protocol-visible truth
• replay-visible evidence and finalization objects
• ownership and receipt/handoff/reconfiguration transition artifacts
• theorem-pack and runtime admission gates

Out of scope:

General host application authorization is out of scope.

• arbitrary user/resource policy languages
• product-specific auth delegation systems unrelated to protocol semantics
• host-only policy decisions that cannot be modeled as typed Rust/Lean objects

Four Capability Classes

The canonical Rust boundary is rust/machine/src/capabilities.rs. The canonical Lean boundary is lean/Runtime/Proofs/CapabilityModel.lean together with the theorem-pack and conservation proof surfaces.

Canonical Lifecycle States

Not every class uses every lifecycle state. For example, ownership uses issued, invalidated, expired, and rejected, while transition artifacts commonly use issued, committed, rolled_back, rejected, and invalidated.

Finalization State Machine

Finalization is the explicit bridge from protocol observation to canonical truth.

The key runtime/Lean objects are:

• ProtocolMachineFinalization
• FinalizationPath
• FinalizationReadClass
• FinalizationStage

Observed input never becomes canonical directly. It must pass through the explicit authoritative/materialization/publication path.

Language Mapping

Runtime upgrade and reconfiguration are first-class transition semantics in the runtime and Lean model, but they are not choreography DSL statements today.

Runtime Meaning

The runtime uses one canonical lifecycle audit and one canonical semantic-object bundle:

• ProtocolMachine::capability_lifecycle_audit_log()
• ThreadedGuestRuntime::capability_lifecycle_audit_log()
• ProtocolMachine::semantic_objects()
• ProtocolMachine::protocol_machine_finalization()

Timeout expiry is modeled strictly: the runtime stores and later expires the exact issued TimeoutWitness, rather than reconstructing expiry from a bare clock map later.

Transfer/handoff and runtime upgrade/reconfiguration are also explicit. They emit typed transition artifacts rather than relying on hidden host-local state.

ProtocolMachineConfig.host_contract_assertions is a typed HostContractMode. The default Enforced mode checks handler identity stability, deterministic topology-event ordering, and transfer-event audit coverage before those host-supplied facts are accepted into the machine. The RelaxedTestOnly mode is reserved for targeted tests that intentionally violate those contracts. It is rejected with DeterminismMode::Full.

Lean and Bridge Surfaces

The Lean model exports this surface through:

• lean/Runtime/Proofs/CapabilityModel.lean
• lean/Runtime/Tests/ProtocolMachineRunner.lean

The strict Rust↔Lean correspondence lane checks the capability/finalization surface through:

• rust/bridge/tests/capability_model_correspondence.rs
• toolkit/xtask/src/checks/lean_bridge_strict.rs

That lane keeps canonical vs invalidated finalization paths and committed-cutover vs rolled-back runtime-upgrade artifacts executable and claim-visible.

Scope Decision Criteria

A concern is eligible to move into the protocol-machine/effect/DSL boundary when all of the following hold:

1. It changes protocol-critical behavior rather than only presentation or app-internal behavior.
2. It can be represented as typed outcomes, evidence, receipts, or obligations rather than opaque host internals.
3. It is observable at the replay/audit/effect-trace boundary.
4. The protocol machine can enforce or validate it at a meaningful boundary.
5. Lean/Rust correspondence can model it without inventing a separate host-language semantics.

A concern should stay host-only when any of the following hold:

1. It is mainly UI/view/reduction logic.
2. It depends on implementation-specific nondeterministic runtime internals rather than typed protocol observations.
3. It cannot be expressed as typed evidence/outcomes without dragging in a general-purpose application semantics.
4. It is not part of the safety-visible or replay-visible protocol interface.

Classification

Host Runtime Disposal Boundary

Targeted close and reap is an operation of the exclusively owned Rust runtime. Its acknowledgment proves retirement of execution custody after any owned worker scope completes. The compact summary grants no admission, ownership, evidence, or transition capability and cannot authorize a protocol outcome. Application owners retain their protocol terminal publication and authenticated evidence obligations. Session Lifecycle defines the runtime retirement contract. Rust-Lean Parity records the host-lifecycle scope.

Related Docs

• Capability Admission
• Authority Language Surface
• Protocol Machine Architecture
• Verification Inventory

Typed Invocation Acceptance

A host response is an observation until the machine accepts it against the original request. Register state may change only for a successful outcome with the exact response family required by that request. Failure and blocked outcomes cannot authorize a state update by attaching a success-shaped payload. A malformed successful outcome is a failed contract, not a successful publication or a successful child in effect composition. The raw exchange remains available as an observation.

Nominal authority invocation additionally requires a declared operation, role-scoped execution under its actual session owner and generation, typed arguments and outcome, and one live continuation. Unknown declarations, stale owners, duplicate completion and invalidated continuations must fail before publication or continuation advancement. The generic runtime.step boundary does not yet implement this nominal contract. Naming an action is not dispatch or proof that the contract was checked.