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

Related Docs

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