r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope
On this page

Availability and lifetime

A definition can remain known after it is no longer available. A pending occurrence can be lost even if that same definition becomes available again. Work that already crossed its detachment boundary can have different continuation rules from either case.

Read abilities and use for definitions, instances and use records, and objects and lifetime for object references. This chapter separates present availability, historical capture and the lifetime of an individual procedure.

Start with four different records

The normalized registry profile uses a catalog of known definitions, a current registry selecting admitted catalog rows, a basis containing the current revision and rule permissions, and a ledger containing recognized instances and activity epochs. Current snapshots combine those inputs with the information needed by the consuming ability procedure.

Identifiers have different jobs: a catalog key selects a definition row; a native ability identifier identifies that row’s definition; an instance identifier names a particular recognized occurrence. The source, controller and executor are also distinct from the physical owner of any object involved.

This registry binding is deliberately specific: its admitted rows use normalized rule sources, and its ledger-domain guard requires empty hold/effect registries. The broader ability kernel has object-source, departure-hold and persistent-effect mechanisms, but that does not widen this particular admission predicate automatically.

An activity publication changes an admitted entry or rule permission, advances the basis revision and supplies a different snapshot. The observation pipeline must still project only the participant’s lawful information. An internal basis or captured snapshot is not automatically a player-facing view.

Capture an occurrence with its activity epoch

A recognized conditional instance records its definition key, a copy of the definition, its checkpoint and occurrence, and the activity epoch at recognition. These values let the model ask whether that same pending occurrence is still current.

The ledger update applies currentness to pending instances:

reference-profile · input revision 2 · CC0 1.0

ConditionalActivityLedger96(before,definitions,snapshot) ==
 [before EXCEPT !.instances=[id \in DOMAIN @ |->
    IF @[id].status="Pending" /\ ~ConditionalInstanceCurrent96(@[id],definitions,snapshot)
    THEN [@[id] EXCEPT !.status="Lost"] ELSE @[id]]]

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

If its definition disappears, differs from the captured copy, becomes inactive or has a different activity epoch, a pending instance becomes lost. Other statuses are not turned into lost by this particular update. That distinction matters for work that has already begun resolution.

ConditionalInstanceCurrent96 is a conjunction of these conditions. Finding the same identifier in a new registry is only one part of the test.

Make loss and restoration observable

The publication epoch relation detects active-to-inactive loss and increments the corresponding definition’s epoch. It also advances an activity serial when the publication contains a loss:

reference-profile · input revision 2 · CC0 1.0

PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot) ==
 LET lost==ConditionalActivityLosses96(beforeSnapshot,candidateSnapshot)
     keys==DOMAIN before.activationEpoch \cup DOMAIN beforeSnapshot.definitions \cup DOMAIN candidateSnapshot.definitions
 IN [candidate EXCEPT
   !.activationEpoch=[key \in keys |-> (IF key \in DOMAIN before.activationEpoch THEN before.activationEpoch[key] ELSE 0)+(IF key \in lost THEN 1 ELSE 0)],
   !.activationSerial=before.activationSerial+(IF lost={} THEN 0 ELSE 1)]

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

As an authored example, pending instance 31 can capture definition key k at epoch 4. A valid permission withdrawal makes that definition inactive and advances its epoch to 5. The pending instance is marked lost and removed from its window’s pending set. Restoring permission later does not change instance 31 back into a pending occurrence. A new qualifying occurrence would need its own recognition and instance identity.

This example is a reading of the loss/restoration mechanism, not a retained trace. It also assumes the appropriate supplied snapshot and publication inputs. The epoch relation does not independently discover every activity change in an external application.

Update windows as well as the instance ledger

A window’s pending set and the instance ledger must agree. When activity reconciliation changes a pending instance to lost, the window update removes it from pending and records the loss disposition. Leaving the old identifier selectable in the window would preserve an invalid opportunity even if the ledger had been updated correctly.

Follow SyncConditionalWindows96 for this join. It does not erase the captured recognition or pretend that the occurrence never existed. The history can explain why an opportunity was once pending and why it can no longer be selected.

Detachment changes continuation, not target identity

A paid ability can detach after its matching trigger cost is paid. A conditional ability can detach when its resolution legitimately begins. These boundaries permit some already-started work to continue under a captured definition while current source availability changes.

That does not make every old object reference valid forever. The detached source-target helper still requires a current object at the captured source zone:

reference-profile · input revision 2 · CC0 1.0

DetachedSourceTarget9(frame,objects,target) ==
 /\ frame.detached /\ frame.source.kind = "Object"
 /\ target = frame.source.object /\ target \in DOMAIN objects
 /\ objects[target].zone = frame.sourceZone

Definition and resolved references · Exact module download · Source bundle and reproduction instructions

For an authored example, a detached procedure referring to source object 11 cannot satisfy this helper with successor 12 merely because both describe the same physical card. Its instructions, targets and checkpoints retain their own currentness and permission checks. Detachment is not a general permission to bypass them.

The rule-source registry profile has no physical source object for this helper. Keep that profile’s permission-withdrawal example separate from the broader object-source targeting example.

Retain history without treating it as current authority

A historical capture preserves the basis used by an earlier decision. A current snapshot can legitimately disagree with it after publication. Replacing the earlier capture with the latest registry would erase the very loss or restoration the model is intended to explain.

Conversely, a captured definition is not sufficient authority to offer a new ability now. New admission must pass the current registry, activity, legality and timing checks. The registry reference explains how the normalized context is built and admitted.

The registry and lifecycle evidence names the actual finite configurations, observation comparisons and domain limits. Matching selected lifecycle cases does not establish every activity provider or every possible object/source representation. Continue with composition and assumptions to see how these records join payment, instruction and checkpoint work.