Instruction execution and return¶
An instruction asks a procedure to perform work and then return control. It needs more than a destination and a Boolean success flag. The contract must identify the admitted request, current targets, applicable permissions, actual result, events, remaining child work and the caller that is allowed to resume.
Read object operations for the guided path and priority and completion for the surrounding return protocol.
Establish inputs and roles before evaluating a relation¶
Object inputs are finite tables indexed by current object identifiers. Selection inputs are sets; deck and ordering inputs are sequences of typed identifiers. Frame and receipt inputs are records with the fields read by their operators. An ill-shaped record or an out-of-domain lookup can be an evaluation error, rather than a convenient FALSE result. The stated input carrier is part of the contract.
The physical owner, current controller, instruction actor and effect executor have separate roles. Ownership can determine a return destination; control can determine eligibility or a look grant; an explicitly supplied executor determines who performs an effect. Authorization must come from the containing rule or provider and cannot be inferred solely from any one of those roles.
Each procedure frame records its stage and caller. Its guards admit individual transitions; its updates specify what changes locally. The larger model must frame other state and connect supplied completion receipts to actual work. Observation rules remain in force while a procedure is suspended or returning.
Interpret partial feasibility explicitly¶
The small instruction-parts helper distinguishes carrying out feasible parts from an all-or-nothing feasibility condition:
reference-profile · input revision 2 · CC0 1.0
InstructionParts(ifAble, requested, feasible) ==
IF ifAble /\ feasible # requested THEN {} ELSE feasible \cap requestedDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
Here the caller supplies the requested and feasible sets. With the ifAble mode set, disagreement between those sets yields no parts. Otherwise the result is their intersection. The helper does not compute feasibility and does not describe rollback of changes already made by another procedure.
For an authored example, let requested parts be {1, 2} and feasible parts {1}. The ordinary projection returns {1}; the ifAble projection returns {}. These integers stand for instruction parts in this explanation. The example is neither a retained execution nor a claim that every compound instruction uses this helper.
Target existence and target eligibility are additional questions. A live identifier alone does not establish an allowed target, and a target selected earlier may cease to name a current object. Follow objects and lifetime for references across renewal.
Treat payment and its completion receipt as separate inputs¶
Play and deployment consume transaction records tied to the specific procedure and current object. They check the inherent cost part, supplied amount legality and whether the transaction says all applicable costs were paid. A cost barrier then waits for the matching transaction and required checkpoint/reaction work.
Zero payment and an absent or ignored component remain distinct. In particular, the procedure uses whether something was actually paid to determine its checkpoint obligation. The arithmetic and atomic-payment example in costs explains why a balance difference cannot supply that fact.
These relations are consumers of payment evidence, not a complete evaluator of all cost sources or permission-changing effects. Replacing a supplied transaction with TRUE in a fixture removes an implementation responsibility from that fixture; it does not establish the responsibility in a larger system.
Tie child completion to the correct occurrence¶
A play ability-completion receipt binds its play identifier and current object, requires all owned timing structures to have returned, and includes the procedure’s own end triggers:
reference-profile · input revision 2 · CC0 1.0
PlayAbilitiesCompletion8(f,receipt) ==
/\ receipt.playId = f.id /\ receipt.object = f.object /\ receipt.allPlayAbilitiesResolved
/\ receipt.ownedTimingIds \subseteq receipt.returnedTimingIds /\ receipt.ownEndTriggersResolvedDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
An authored example is a frame that owns child timing identifiers {31, 32}. A receipt listing only {31} as returned does not satisfy the subset requirement. Matching the child set still does not excuse a wrong play identifier, wrong object or unfinished own end triggers. The receipt has to satisfy the complete relation.
That relation checks the receipt’s consistency. It does not independently execute the children or prove that a receipt provider reported their completion truthfully. A model that supplies those records has a narrower scope than a connected scheduler that produces them from its own state transitions.
Keep cleanup, completion and return distinct¶
A played source may remain in play, leave play during resolution, become hosted or converted, require ordinary retirement, or carry a specifically authorized retention effect. Its cleanup contract selects among those cases and checks the associated receipts. The visible board alone is not a substitute for that disposition.
Once the play frame is complete, return still has its own guards:
reference-profile · input revision 2 · CC0 1.0
ReturnPlayToCaller8(before,after,actualSeparateInstructionAndEndingReactionsComplete,caller) ==
/\ before.complete /\ ~before.returned /\ caller = before.caller /\ actualSeparateInstructionAndEndingReactionsComplete
/\ after = [before EXCEPT !.returned = TRUE]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The same pattern appears in draw and deployment returns, with their additional obligations. ReturnDrawToCaller8 waits for the procedure-end checkpoint and reactions. ReturnDeployToCaller8 also checks verification and any required activation processing. A batch must not open its next separate instruction before the prior instruction has returned under the relevant relation.
Preserve the search and arrangement boundaries¶
A search frame can mark its selection complete while still owing a deck shuffle, condition marking and a matching return. SearchFoundActionAllowed8 requires that return, condition processing and any deck shuffle before the found-card follow-up may begin. Permission to reveal a found card is another explicit input; finding it does not automatically grant that permission.
Arrangement can change order without changing membership. A more involved arrangement may temporarily set cards aside, record origins and create fresh object successors on transfer. Those steps need the same lifetime and observation discipline as a draw. A local swap helper that preserves every other object row is not a blanket permission to exchange arbitrary objects or bypass destination restrictions.
Read the evidence at the provider boundary¶
The operations evidence gives the selected model inputs, actual results, comparison scope and remaining limits. A prepared assertion selector can evaluate supplied cases. A transition driver can explore its own payment, timing and cleanup branches. Association of a contract with a model does not prove that every contract branch was reached.
The relevant questions for a larger composition are concrete: who supplies authorization, who computes feasible selections, who records payment, who owns child work, and which observation may see temporary objects? The contracts make these joins explicit, but do not by themselves provide every supplier, a universal carrier-preservation proof or a complete rules engine.