Zones, locations and observations¶
A zone answers where an object belongs. A location can say more: which host contains it, which position it occupies in an ordered deck, or which part of the play area it occupies. Neither answer alone determines who may inspect it or whether its abilities are active.
For the initial construction of those relationships, read zones and setup. For identity across movement, read objects and lifetime.
Describe membership before moving anything¶
The reference profile has seat-specific decks, hands, discard piles and objective areas, together with shared play, bank, set-aside and removed zones. “Seat-specific” describes association; it does not mean that every such zone has the same visibility rule.
At the zone-partition level, inGameIds is the chosen universe of identifiers and occupants maps every admitted zone instance to a set of identifiers. Authorization, reveal requirements and the responsible instruction are separate inputs. Physical ownership, current control and effect execution can name different seats; none is a blanket visibility grant. A membership update constrains its own changes, while completion of the containing instruction needs its own boundary.
Every identifier belongs somewhere, and no identifier belongs to two different zones:
reference-profile · input revision 2 · CC0 1.0
ZonePartition4(inGameIds, occupants) ==
/\ DOMAIN occupants = ZoneInstances4
/\ UNION {occupants[z] : z \in ZoneInstances4} = inGameIds
/\ \A a,b \in ZoneInstances4 : a # b => occupants[a] \intersect occupants[b] = {}Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The function’s domain is consequential. Supplying a map that omits a currently empty zone is different from supplying that zone with an empty occupant set. Deck order is another input: a set of deck occupants cannot identify the next card to draw.
Read the complete move relation¶
An atomic move checks membership, authorization and any required prior reveal before constructing the new partition:
reference-profile · input revision 2 · CC0 1.0
AtomicZoneMove4(inGameIds, before, after, id, source, destination,
movementAuthorized, revealRequired, revealedBeforeMove) ==
/\ source \in ZoneInstances4 /\ destination \in ZoneInstances4 /\ source # destination
/\ ZonePartition4(inGameIds,before) /\ id \in before[source]
/\ movementAuthorized /\ (revealRequired => revealedBeforeMove)
/\ after = [z \in ZoneInstances4 |-> IF z = source THEN before[z] \ {id}
ELSE IF z = destination THEN before[z] \cup {id} ELSE before[z]]
/\ ZonePartition4(inGameIds,after)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The source and destination must be different admitted zone instances. The moved identifier must be in the source before the step. Its removal and addition occur in one relation, and every other zone’s occupant set is preserved. The relation checks the partition again afterward.
As an authored example, suppose object 11 is in SideA’s hand, object 12 is in play, and all other occupant sets are empty. With the required permission, moving 11 to play produces an empty hand and play occupants {11, 12}. Leaving 11 in the hand as well does not satisfy the relation. This is a worked partition update, not a retained trace.
This operator redistributes identifiers within a fixed universe. It does not implement object renewal. A full operation that ends one object’s lifetime and creates a successor must separately relate its old and new object tables and their occupancy projections. Applying this small relation alone is not a proof of that larger operation.
A false guard supplies no allowed successor under this action. An implementation should reject such a request without applying a partial move; implementation conformance is a separate claim from the formal relation.
Keep order where it carries information¶
A deck sequence requires distinct identifiers. Its contents must be preserved when it is reordered. Changing the order needs the relevant direction or search context; retaining the same order is allowed. A search-completion contract additionally requires the supplied shuffle to have occurred. A hand projection can discard sequence positions while retaining membership and cardinality.
Follow DeckSequenceValid4, DeckReorder4 and HandSetupProjection4 for these separate operations. Their inputs are typed sequences or sets of identifiers, not interchangeable containers or arbitrary text strings.
An object’s location also takes hosting into account. ObjectLocation4 chooses a host reference before a deck position or ordinary zone location. Hosting and deployment remain separate facts: placing an object on a host does not establish an deployment unless the relevant relation says so.
Determine the observer’s view explicitly¶
The default look rule depends on the zone class, face, viewer and controller:
reference-profile · input revision 2 · CC0 1.0
DefaultZoneLook4(zone, face, viewer, controller) ==
CASE ZoneClass4(zone) = "Hidden" -> FALSE
[] ZoneClass4(zone) = "Secret" -> viewer = controller
[] ZoneClass4(zone) = "SchemaAtom128" -> face = "Up" \/ viewer = controller
[] OTHER -> FALSEDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
The default grants no deck-content view. A hand is visible to its controller. Other admitted zone classes use their face/controller conditions. Dedicated contracts refine these defaults for discard piles, set-aside groups and explicit grants; consult the exact zone rule when an instruction crosses one of those boundaries.
A deck’s size may be available while its identities and order remain hidden. A set-aside group’s count may be public without identifying its cards. A player-facing observation should project only the permitted information, rather than exposing the full internal object table and asking the player to ignore it.
Track temporary custody by the responsible procedure¶
Set-aside objects carry a transit record with their origin, effect instance, owning ability and any protected cleanup obligation. SetAsideTrackingValid4 requires every current set-aside object to have matching tracking information. A temporary group cannot be reconstructed reliably from face or current zone alone.
The observation of its exit can depend on the observing ability. SetAsideExitView4 can report the temporary zone to a qualifying observer and the recorded origin to another. That is an explicit observation contract, not an assertion that the underlying object occupies both zones.
The bank, set-aside and removed zones are inactive by default in this profile. Removed objects also have a restricted interaction gate. Open information about a removed card does not grant permission to move it back into ordinary play.
Composition and evidence limits¶
Movement authorization, required reveal, location legality and temporary look grants are supplied or checked by different contracts. Owner, current controller and effect executor must be passed in their correct roles. A successful membership update does not establish those providers or complete the containing instruction.
Schema and setup evidence records the selected zone/type inputs, observations and review status. Operations evidence concerns procedures that use them. Read each result’s actual carrier and bounds: a finite fixture or a well-shaped example does not prove correspondence for arbitrary label strings or every possible zone-changing effect.