Object operations¶
Moving a card to play, playing it, deploying it and swapping its location can leave similar-looking boards. They can still be different operations: they admit different inputs, preserve different identities, create different events and return control at different boundaries.
Read objects and lifetime for current references and successors, resources and payment for atomic payment, and priority and completion for the caller’s obligation to wait.
Identify the request and its responsible procedure¶
An operation receives an object table, relevant ordered zones and a procedure frame. The frame records an occurrence identifier, actor, caller and stage, with operation-specific choices and completion flags. Object identifiers and occurrence identifiers serve different purposes: one names a current object, the other names this particular attempt or event.
The physical card’s owner comes from metadata. The current controller can differ from that owner. The actor carrying out an authorized instruction can differ again; the effect’s executor is supplied by the ability context. Destination and observation rules must use the appropriate role rather than a single catch-all “player” value.
The relation also needs typed inputs: finite identifier sets, sequences where order matters, maps with the required fields, and explicit authorization/payment/completion facts. It checks local guards and permitted changes. It does not infer every permission or interpret arbitrary ability text. Record updates frame their record; a composed state must also constrain unrelated components.
Record what actually occurred¶
The movement contract distinguishes a completed or modified operation from one that was prevented, impossible, replaced by another named operation, or had no effect:
reference-profile · input revision 2 · CC0 1.0
MovementOccurred8(kind,disposition,actualInstructionResolved) ==
kind \in CardMovements8 /\ actualInstructionResolved /\ disposition \in {"Complete","ModifiedEffects"}Definition and resolved references · Exact module download · Source bundle and reproduction instructions
A request is not enough to record an occurrence. The instruction must have resolved, and its disposition must be one that counts as this movement. The history relation also requires a fresh positive occurrence identifier.
As an authored example, two requests both intend to move an object into a discard pile. One completes as a retirement operation; another is prevented before that operation occurs. Their final location information cannot replace the occurrence history, and the prevented request does not receive the completed movement event. This is an explanation of the disposition contract, not a retained trace or a general replacement interpreter.
Direct relocation plans also distinguish an explicitly directed destination from such named operations as drawing, playing or deploying. Reusing a destination helper does not make those procedures interchangeable.
Allocate successors when the contract ends an identity¶
Batch transfers can consume current object identifiers and create fresh successors. The successor map covers exactly the sources, uses previously unused positive identifiers and does not merge two sources:
reference-profile · input revision 2 · CC0 1.0
FreshSuccessors8(sources,successors,usedIds) ==
/\ DOMAIN successors = sources
/\ {successors[id] : id \in sources} \subseteq (Nat \ {0}) \ usedIds
/\ Cardinality({successors[id] : id \in sources}) = Cardinality(sources)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
For an authored example, source identifiers {11, 12} may map to fresh successors 21 and 22 when both are outside the used-identifier set. Mapping both sources to 21 fails the distinctness condition. Reusing 11 as its own supposedly fresh successor fails when 11 is already recorded as used.
That test is one part of the larger transfer relation. The object table must also remove the old rows, add the required successor rows, preserve unaffected rows and satisfy the destination-specific postconditions. An old reference does not become a reference to its successor unless another contract explicitly follows that relationship.
A draw has temporary custody before its return¶
A positive draw batch fixes effective counts, removes the relevant deck prefixes and tracks the drawn objects in a temporary set-aside group. Draw reactions and their children run before the surviving group transfers into its owners’ hands. A current look grant or an ability-specific observation determines who can inspect those objects while the batch is pending.
The temporary zone is therefore not a public reveal of all drawn identities. Nor does a general-purpose observer necessarily see the same movement path as the ability that refers to this batch. Follow the zone reference for transit ownership and exit observations.
A zero effective draw uses a separate completion branch with no drawn-card event. It should not be simulated by creating and immediately returning an empty positive batch.
Deployment, play and activation retain their own gates¶
Deployment can involve staging, destination choice, legality/capacity work, payment, a cost barrier and final placement. Staging is not yet deployment. A played card follows a different sequence: placement, cost work, activation of its played abilities, resolution and cleanup. Deployment does not imply activation, and a play procedure does not make its source a deployed card.
The ordinary play-type gate admits Plan cards for SideA and Action cards for SideB. Deployment has different type and face gates; special authorization is needed for the exceptional cases admitted by those gates. The shared destination of play does not erase these profile-specific distinctions.
Both procedures need to distinguish a locally completed result from permission to return to the caller. The play return relation makes that boundary explicit:
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 frame must be complete, its return must not already have happened, the caller must match, and the separate instruction’s ending reactions must have finished. A stage or balance alone does not discharge those conditions.
Follow a search through its remaining obligations¶
Finding cards can end the search’s selection stage while shuffle, condition marking and return work remain. A later instruction to play or install a found card needs the search return contract as well as its own procedure. Search visibility is granted to the searching actor for the relevant zone and stage; it is not blanket permission to reveal every inspected identity.
The instruction reference develops these completion and provider boundaries. The operations evidence records which assertions and finite procedures were actually checked. An associated model does not imply that every operation, input shape or consequential branch has been exercised, and these contracts do not constitute a complete gameplay interpreter.