Glossary and Notation Index
This page defines shared terms and symbols used across the documentation and paper-aligned pages. It serves as the stable lookup for terminology and notation.
Core Terms
| Term | Meaning | Primary Docs |
|---|---|---|
| coherence | Session-wide compatibility invariant between local type state, buffers, and global structure. | Theory, Theorem Program |
| harmony | Projection and protocol evolution commute under declared premises. | Theory, Theorem Program |
| projection | Mapping from global choreography to per-role local session types. | Choreographic Projection Patterns |
| local type | Per-role protocol view used for runtime typing and progression. | Theory, Session Lifecycle |
| effect handler | Runtime boundary that interprets protocol-machine or choreography actions. | Choreography Effect Handlers, Effect Handlers and Session Types |
| theorem-pack | Lean-exported capability inventory used by runtime admission gates. | Lean Verification, Capability Admission |
| capability taxonomy | The four first-class protocol-critical capability classes: admission, ownership, evidence, transition. | Capability Model, Authority Language Surface |
| admission | Runtime gate process that checks contracts and capability evidence. | Capability Admission |
| ownership capability | Runtime host authority token carrying owner label, generation, and scope. | Effect Handlers and Session Types, Session Lifecycle |
| evidence | Typed proof object or witness consumed by protocol-critical authority flow. | Authority Language Surface |
| receipt | Single-use transfer or handoff proof emitted by an explicit ownership/delegation path. | Session Lifecycle, Authority Language Surface |
| finalization subsystem | The explicit runtime/Lean model that classifies observed, authoritative, materialized, canonical, invalidated, and rejected semantic paths. | Protocol Machine Architecture, Capability Model |
| canonical handle | Non-forgeable runtime reference proving a materialized/publication path is consumable as canonical truth. | Authority Language Surface, Capability Model |
| transition artifact | Receipt, handoff, or reconfiguration/runtime-upgrade object that carries explicit transfer or cutover authority. | Capability Model, Authority Language Surface |
| linear binding | Binding that the compiler requires to be consumed exactly once. | Choreographic DSL, Authority Language Surface |
Result | Built-in success/failure sum form with Ok and Err. | Choreographic DSL |
Maybe | Built-in optional-value sum form with Just and Nothing. | Choreographic DSL |
| effect declaration | Nominal choreography declaration for one typed external host interface. | Authority Language Surface |
uses clause | Protocol-level declaration of which named effect interfaces may be invoked. | Authority Language Surface |
| timeout branch | Protocol-visible timeout/cancellation construct with explicit alternate branches. | Choreographic DSL, Authority Language Surface |
| ownership epoch | Generation used to invalidate stale owner handles after transfer or scope attenuation. | Session Lifecycle |
| canonical ingress | Sanctioned host event entry path such as topology_events, send_decision, handle_recv, or step. | Effect Handlers and Session Types |
| stale-owner rejection | Fail-closed behavior when a prior ownership capability is reused after transfer or attenuation. | Effect Handlers and Session Types, Session Lifecycle |
| envelope | Declared refinement boundary for higher-concurrency and profile-scoped behavior. | Protocol Machine Architecture, Rust-Lean Bridge and Parity |
| determinism profile | Runtime trace-equivalence contract mode such as Full or Replay. | Protocol Machine Architecture, Rust-Lean Bridge and Parity |
| communication replay mode | Transport replay-consumption policy: off, sequence, or nullifier. | Protocol Machine Architecture, Session Lifecycle |
| communication nullifier | Domain-separated digest of canonical communication identity used for one-time receive consumption checks. | Protocol Machine Architecture, Session Lifecycle |
| consumption root | Deterministic accumulator root over communication replay-consumption state. | Protocol Machine Architecture, Rust-Lean Bridge and Parity |
| protocol machine | Single-thread execution engine (ProtocolMachine) that runs projected local types with session type monitoring. | Protocol Machine Architecture |
| guest runtime | Telltale-owned driver (GuestRuntime) instantiated around the protocol machine for simulation and runtime integration. | Protocol Machine Architecture, API Reference |
| effect handler | Host-runtime boundary trait (EffectHandler) implemented by embedders and simulators. | Effect Handlers and Session Types, API Reference |
| semantic object | Typed introspection record (such as OperationInstance, OutstandingEffect, CanonicalHandle) maintained by the protocol machine for audit and replay. | Protocol Machine Architecture, API Reference |
| typed outcome | Structured success/failure result at the effect boundary using EffectResult and EffectFailure rather than raw strings. | Capability Model, Authority Language Surface |
| content addressing | Cryptographic identity scheme (ContentId) for protocol artifacts enabling deduplication and integrity checks. | API Reference |
| nominal effect interface | Named effect declaration (effect Name) that makes host dependencies explicit and typed at the language level. | Authority Language Surface, Capability Model |
| conservation framework | The organizing design principle: all semantically meaningful behavior is expressed in terms of six conserved quantities. | Conservation Framework |
| evidence (conserved property) | The integrity of what has been established. Witnesses, proofs, and attestations are its concrete forms. | Conservation Framework |
| authority (conserved property) | The exclusivity of who may act. Ownership is its concrete form. | Conservation Framework |
| identity (conserved property) | The definiteness of object references across retries, effects, and handoffs. | Conservation Framework |
| commitment (conserved property) | The account of outstanding obligations. Outstanding effects are its concrete form. | Conservation Framework |
| structure (conserved property) | The essential shape of the protocol. Multiparty session types are its concrete form. | Conservation Framework, Theory |
| premise (conserved property) | The explicitness of environmental assumptions. Failure models and fairness assumptions are its concrete forms. | Conservation Framework |
| erasure principle | Behavior not part of the conserved quantities is not part of the programming model. | Conservation Framework |
| reduction principle | All runtime behavior must reduce to the conservation framework. | Conservation Framework |
| region | Locality and framing domain for structured coordination with lifecycle, authority, and observation boundaries. | Conservation Framework |
| semantic core objects | The closed set of protocol-visible objects: Region, OperationInstance, OutstandingEffect, SemanticHandoff, AuthoritativeRead, ObservedRead, MaterializationProof, CanonicalHandle, ProgressContract. | Conservation Framework, Protocol Machine Architecture |
Symbol and Notation Index
| Symbol or Form | Meaning | Primary Docs |
|---|---|---|
G | Global protocol type. | Theory |
L or LocalTypeR | Local role protocol type. | Theory, Protocol-Machine Bytecode Instructions |
project(G, R) | Projection of global type G for role R. | Theory, Choreographic Projection Patterns |
μX. ... X | Recursive protocol form with bound variable X. | Theory |
⊕{...} | Internal choice at the selecting endpoint. | Theory |
&{...} | External choice at the receiving endpoint. | Theory |
!T.S | Send T, then continue as S. | Theory |
?T.S | Receive T, then continue as S. | Theory |
end | Session termination state. | Theory |
Consume | Recursive receiver-side trace alignment kernel used in coherence proofs. | Theory, Theorem Program |
n = 1 | Canonical single-step concurrency regime for exact parity. | Protocol Machine Architecture, Rust-Lean Bridge and Parity |
n > 1 | Higher-concurrency regime admitted under envelope and premise-scoped constraints. | Protocol Machine Architecture, Rust-Lean Bridge and Parity |
Full, ModuloEffects, ModuloCommutativity, Replay | Runtime determinism profiles. | Protocol Machine Architecture, Rust-Lean Bridge and Parity |
off, sequence, nullifier | Communication replay-consumption modes. | Protocol Machine Architecture, Session Lifecycle |
telltale.comm.identity.v1 | Domain-separation tag for canonical communication identity schema. | Protocol Machine Architecture |
case ... of | Exhaustive sum-pattern branching over forms such as Result and Maybe. | Choreographic DSL, Authority Language Surface |
let x = check Effect.op(args) | Typed external query binding that later lowers to the protocol-machine effect boundary. | Choreographic DSL, Authority Language Surface |
effect Name | Nominal effect-interface declaration. | Authority Language Surface |
protocol P uses Runtime, Audit | Protocol declaration naming its allowed effect interfaces. | Authority Language Surface |
timeout 5s R at ... on timeout => ... on cancel => ... | Protocol-visible timeout and cancellation branch form. | Choreographic DSL, Authority Language Surface |
Notation Consistency Rules
Use one symbol for one concept in a local section. Reintroduce symbols when crossing between theory and runtime notation. Prefer existing symbols from this index unless precision requires a different one.