Composition and assumptions¶
A collection of correct local relations is not yet a connected procedure. Composition has to connect the same payment, object state, window, checkpoint and caller across those relations. A receipt that is valid for another occurrence cannot establish the boundary this caller is waiting for.
Read turns and ending, object operations, abilities and use and availability and lifetime for the components. This chapter follows the bounded connected action profile and the assumptions it makes explicit.
Decide what each component owns¶
The connected state records the action frame, payment and native-operation records, object state, current timing stack, checkpoint frames, ability ledger, snapshots and return histories. These are typed maps, sequences and records with different identifiers; a single stage label cannot replace their relationships.
The acting seat, object controller, ability controller and effect executor can differ. A component that receives an internal object table does not thereby gain permission to publish it to a participant. Observation projection remains a separate obligation at every join.
Some facts are produced by another modeled component. Other facts are supplied: applicable permission, effect interpretation, target feasibility or an outer scheduling decision. A connected contract should say which is which before relying on a Boolean completion or legality input.
Connect payment to its own checkpoint¶
The action-paid predicate requires its reservation, native commitment and matching cost-checkpoint drain, then checks the resulting action-point state:
reference-profile · input revision 2 · CC0 1.0
AActionPaid(q) ==
/\ AReservation(q) /\ ANativeCommitted(q) /\ AActionCostDrained(q,ACostCaller(q))
/\ q.actionPointWorld=[q.payment.after EXCEPT !.checkpointDue=FALSE] /\ q.costDrainedDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
This is a predicate over connected records, not a command that pays costs. The amount alone is insufficient. A successful payment from another transaction or window cannot stand in for the recorded reservation, and a checkpoint merely being complete does not establish that it belongs to this payment.
As an authored example, transaction 21 can be associated with action 31 and checkpoint 41. A valid completion receipt from checkpoint 42 is still the wrong receipt if the recorded cost caller requires 41. This illustrates identity matching; it is not a retained model execution or a statement that these illustrative numbers are the driver’s fixed constants.
Do not resume while a child is still owned¶
An action can delegate to traversal, inspection or ability work. The caller must record the child’s identity and consume the matching return exactly where its continuation is allowed. Completion of a sibling or merely removing a child window is insufficient.
The connected return record carries the option, transaction, payment and child-completion conditions together:
reference-profile · input revision 2 · CC0 1.0
AActionReturn(q) ==
LET w==WindowTop9(q.stack)
trigger==[tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
allTriggerCostsPaid |-> AActionPaid(q),costCheckpointAndReactionsDrained |-> AActionCostDrained(q,ACostCaller(q))]
IN [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> 200,
triggerPayment |-> trigger,allCostsPaid |-> AActionPaid(q),optionComplete |-> ActionReadyToContinue5(q.action),
childrenReturned |-> "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete,
reactionsDrained |-> AActionCostDrained(q,ACostCaller(q)) /\ "SchemaAtom138" \in q.consumed /\ q.control.returned /\ q.control.traversal.complete]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The record is not self-authenticating because it has the expected field names. Its consumers compare the fields with the active window and underlying records. A composed model must also preserve unrelated state while each component performs its local transition.
The checkpoint reference follows the deeper boundary: recognition, mechanical work, reaction windows and the actual return to a caller are distinct stages.
Publish a completion as one occurrence¶
The action’s completed frame, its native completion record, the event representing completion and the recorded occurrence must agree:
reference-profile · input revision 2 · CC0 1.0
ACompletionCommitted(q) ==
IF q.nativeCompletion=EmptyT11 THEN FALSE ELSE
/\ q.completionCommitCount=1 /\ q.nativeCompletion.operationId=2
/\ q.nativeCompletion.before.status="Effects" /\ q.nativeCompletion.after=[q.nativeCompletion.before EXCEPT !.status="Complete"]
/\ q.nativeCompletion.after=q.action /\ q.nativeCompletion.windowId=q.NeutralValue00003.opened.id
/\ q.nativeCompletion.turnId=q.flow.turn.id /\ q.nativeCompletion.phaseId=q.actionPhaseId
/\ q.completionEvent.nativeCompletion=q.nativeCompletion /\ q.completionEvent.rawEvent=[tag |-> "OriginalActionCompletes",actionId |-> q.action.id]
/\ q.rawEvents[q.nativeCompletion.rawIndex]={q.completionEvent.rawEvent}
/\ q.completionOccurrence.actualEvent=q.completionEvent /\ q.completionOccurrence.nativeCompletion=q.nativeCompletionDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
The broader ACompletionSafety property also constrains the completion-event collection. One recorded commit does not imply that exactly one event was published.
For an authored example, suppose the designated completion event has identifier 51. A publication collection containing both 51 and an additional 52 does not satisfy a contract requiring the designated singleton, even if a separate commit counter remains one. This example explains the distinction between commitment and publication; it is not presented as a quoted checker trace.
A useful negative control changes one of these joins while keeping the rest of the scenario meaningful. Its intended invariant and actual diagnostic matter more than the fact that the tool returned a nonzero exit.
Keep the outer schedule visible¶
The connected driver chooses which step is available next and requires matching return guards at its boundaries. It is a concrete finite profile, not a universal scheduler for every possible instruction combination. The driver can make source and checkpoint behavior inspectable without providing every external permission or effect evaluator.
Its ASpec includes the initial condition, allowed next-state relation, stuttering and an explicit fairness condition. Fairness is an assumption about enabled progress. A safety invariant about matching receipts does not prove that every provider responds, that every play terminates, or that an external engine follows the same schedule.
The distinction also affects testing. A prepared selector can evaluate supplied assertions. A transition driver can expose an actual path through connected state. An explored finite graph can establish its stated bounded result; it cannot establish all unmodeled providers or every branch of every associated operator.
Read an assumption as an interface obligation¶
A supplied authorization should identify the source and operation it authorizes. A supplied payment record should identify the committed transaction. A supplied completion receipt should identify the owner and child work it discharges. A snapshot should identify the revision and observation point from which its facts were derived.
Those interfaces are useful because they can later be connected to executable providers and checked independently. Treating every supplied fact as automatically true would conceal the responsibilities that remain outside the model.
The composition evidence records the exact selected sources, configurations, actual outcomes, counterexamples and scope. This chapter does not infer later composition support or a complete gameplay implementation from the bounded profile. Its central reading task is to follow one obligation from creation through its matching discharge, while keeping the remaining provider and observation assumptions visible.