Catalogues, current entries and captured authority¶
A catalogue describes definitions that this model is prepared to recognize. A current registry selects definitions that are present now. A permission set determines which rule sources are active. A captured context records the particular revision used by a procedure. These values answer different questions, even when a small example gives them the same members.
Read availability and lifetime for the pending-instance story, and abilities and use for the execution boundaries that consume these contexts.
Establish the supported input profile¶
This registry binding accepts a finite catalogue indexed by positive natural numbers. Each row carries its kind, native identifier, source and structured definition. The supported row kinds are paid and conditional abilities. Sources in this binding are rule sources: the object component is zero and the rule label is a real source label rather than the distinguished no-value tag.
That is a material restriction. The broader ability contracts also describe object sources, departure holds and persistent or lingering mechanisms. Their existence does not widen this binding automatically. Here the ledger-domain guard requires empty hold and effect maps, and the derived activity context supplies empty persistent and lingering memberships. A host using those broader mechanisms needs their own compatible binding and evidence.
The catalogue validates row structure and uniqueness within each kind:
reference-profile · input revision 2 · CC0 1.0
CatalogValidSA(catalog) ==
IF ~IsFunctionValueSA(catalog) THEN FALSE
ELSE IF ~IsFiniteSet(DOMAIN catalog) THEN FALSE
ELSE IF ~(\A key \in DOMAIN catalog : IsNaturalValueSA(key)) THEN FALSE
ELSE IF ~(DOMAIN catalog \subseteq Nat \ {0}) THEN FALSE
ELSE IF ~(\A key \in DOMAIN catalog : RowValidSA(catalog[key])) THEN FALSE
ELSE \A a,b \in DOMAIN catalog :
IF catalog[a].kind=catalog[b].kind THEN (catalog[a].nativeId=catalog[b].nativeId => a=b) ELSE TRUEDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
Native identifiers follow the kind-specific definition shape. They need not be interchangeable with the positive catalogue keys. Retaining both allows a use record to identify a catalogue entry while a procedure continues to use the definition’s own identifier.
An authored example starts with catalogue keys 21 and 22. Assigning the same native identifier to two paid rows violates the within-kind uniqueness condition. Giving a conditional row a value that merely prints like a paid identifier does not establish that their definitions have the same kind, source or instruction structure. This example explains the guards; it is not a retained trace.
Presence preserves the admitted row¶
The current registry is a function whose domain is a subset of the catalogue domain. Membership selects an existing row; it does not authorize rewriting that row’s definition in place.
reference-profile · input revision 2 · CC0 1.0
RegistryValidSA(catalog,currentRegistry) ==
IF ~CatalogValidSA(catalog) THEN FALSE
ELSE IF ~IsFunctionValueSA(currentRegistry) THEN FALSE
ELSE IF ~(\A key \in DOMAIN currentRegistry : IsNaturalValueSA(key)) THEN FALSE
ELSE IF ~(DOMAIN currentRegistry \subseteq DOMAIN catalog) THEN FALSE
ELSE \A key \in DOMAIN currentRegistry :
IF ~RowValidSA(currentRegistry[key]) THEN FALSE
ELSE IF currentRegistry[key].kind # catalog[key].kind THEN FALSE
ELSE currentRegistry[key]=catalog[key]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
For the authored keys above, withdrawing key 21 removes its current entry while leaving the catalogue available for provenance checks. Restoring that entry selects the same catalogue row. A changed definition needs an explicitly justified update outside this subset relation.
Presence also differs from permission. A current row can name a rule that is not in the current permission set. The derived ability activity calculation then uses the permission relationship; merely retaining the row does not make the ability active or legal to choose. Affordability, target legality and timing are still separate checks.
Build views from one basis¶
A basis contains a revision, current registry, objects and rule permissions. BasisValidSA checks the registry relationship and limits permission labels to sources represented by the catalogue. It does not prove that every supplied object row is a complete game state or that every permission change was authorized by an outer game rule.
MinimalCaptureSA preserves the basis fields needed to identify the captured context. The paid view and conditional snapshot are derived from that basis and the supplied ledger, rather than assembled from unrelated revisions.
The conditional snapshot contains the current conditional definitions, present identifiers, objects, activity context and activity epochs. The paid view includes the corresponding paid presence, rule-source activity and relevant turn uses. The template supplies other context fields; its existence is an input obligation, not evidence that those fields were discovered or verified by this module.
The capture is a historical binding. After the basis changes, an earlier capture still identifies what was used then. It does not assert current availability. A procedure that needs current permission must consult the appropriate current-state contract.
Keep use history joined to the definition¶
A use ledger must explain which catalogue entry and procedure produced each use. UseProvenanceValidSA ties together the domains of use records, turn-use records and the catalogue index. It checks the procedure’s definition, source, controller, instance and turn against that entry.
This joins more than matching counters. An authored example has a use for instance 51, with source rule PermissionA and turn 8. An index pointing that use to an unrelated row cannot be repaired by giving the new row the same total use count. The source, definition, instance and turn relationships must still agree. Withdrawing a current entry likewise does not authorize deleting or relabelling its historical use.
Physical owner, ability controller and executing procedure remain distinct concepts. In this profile the catalogue definition supplies the controller checked by use provenance. The object map does not make ownership a substitute for that controller, and a caller receiving a context is not thereby authorized to act for either seat.
Admit the derived context at its actual boundary¶
The conditional admission relation combines the basis checks, use provenance and exact binding:
reference-profile · input revision 2 · CC0 1.0
AdmitConditionalSnapshotSA(catalog,basis,ledger,uses,turnUses,index,procedures,template,view,capture) ==
IF ~BasisValidSA(catalog,basis) THEN FALSE
ELSE IF ~UseProvenanceValidSA(catalog,uses,turnUses,index,procedures) THEN FALSE
ELSE ConditionalBindingSA(catalog,basis,ledger,template,view,capture)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
AdmitPaidContextSA applies the corresponding paid-entry binding. Both consume supplied values; neither is a discovery service for arbitrary definitions or a parser for source prose.
The structural guards also have an implementation boundary. Some reflection tests inspect the pinned TLC value printer to reject incompatible input shapes before applying selectors. Their use in this finite profile should not be read as a theorem about every possible TLA+ value or a portable serialization format.
Finally, a complete internal snapshot is not a seat observation. It can contain definitions, object data and provenance that the host must filter before exposing an interface to a player. Registry membership alone grants no viewing permission.
The registry and lifecycle evidence records the checked fixtures, publication changes and controls associated with this binding. Finite graph correspondence and source correspondence retain their stated carriers and provider assumptions. They do not establish an unrestricted registry implementation or automatic support for every object-sourced ability.