Zones and setup¶
Before a transition can move a card, the model needs to say which card it is, where it is, and which parts of its state each participant may inspect. Setup establishes those facts. It is a procedure with ordered choices and a definite handoff into the first turn.
This chapter uses a two-seat reference profile, with seats named SideA and SideB. Their procedures are asymmetric. Begin with values and state for records, sets and sequences, and objects and lifetime for the difference between a physical card and a current object reference.
Choose the representation before the operation¶
A deck is an ordered sequence of card identifiers. Its first element and its last element are different positions. A hand can be projected to a set when position has no meaning. The zone reference explains how those representations meet.
Setup also takes a metadata table and an active profile for each seat. Metadata supplies such facts as ownership, side and kind. Those facts are inputs; finding an identifier in a deck does not derive them. Profile and deck legality require their own checks, including any supplied policy.
Ownership, current control and the executor of an effect are separate roles. A setup step must use the appropriate role for its choices and permissions. Its full internal metadata also differs from a seat’s observation: owning a deck does not automatically grant a view of its contents. The stage guards and supplied choices below describe local changes and completion boundaries; the containing procedure remains responsible for effect interpretation and unrelated state.
Use sequences of typed card identifiers for deck operations. An arbitrary text string is not a substitute for a deck. A label’s spelling and a sequence’s elements have different roles, even where a tool offers operations on both.
Give setup an explicit state¶
The setup state records its current stage, profiles, decks, hands, extra cards, balances, redraw history and whether the game has begun. Initially, hands and balances are empty, the shared bank is not ready, and no seat is the active player.
reference-profile · input revision 2 · CC0 1.0
SetupStart(profiles, decks, extras) ==
[stage |-> "PlaceProfiles",
profile |-> profiles,
profileFace |-> [p \in SetupPlayers |-> "Up"],
profileFront |-> [p \in SetupPlayers |-> TRUE],
deck |-> decks,
hand |-> [p \in SetupPlayers |-> <<>>],
extras |-> extras,
pool |-> [p \in SetupPlayers |-> 0],
redrawn |-> {},
bankReady |-> FALSE,
gameStarted |-> FALSE,
activePlayer |-> SetupNoPlayer]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
SetupStart constructs that record from its inputs. It does not itself establish that the supplied profiles or decks are legal. The surrounding model must apply the relevant validation contracts to those inputs.
The state separates “a profile is on the table” from “the game has started.” Default activity depends on the latter as well as an object’s zone, face and kind. Applying an ability early because its source is visible would confuse those conditions.
Progress through work, choices and supplied effects¶
The standard route names stages for profile placement, each seat’s profile effects, bank creation, initial units, shuffle, opening hands and redraw decisions. It then reaches the before-first-turn boundary and begins with SideA active. The standard relation advances through the profile-effect slots; it does not execute arbitrary profile text. Actual effect work needs its enclosing procedure or supplied override. The ordinary unit-taking step gives each seat five units.
The exact transition is available as SetupStandardNext. Some stages only advance the stage field; others update balances, deck order or hand membership. A record update using EXCEPT preserves the other components of that record. It does not silently preserve variables outside the record: a composed model must constrain those too.
A witness supplies choices such as the shuffled deck or a redraw decision. The setup contract checks the relevant relationship between the before and after values. It does not claim that the witness came from a fair random source or that every supplied effect has been interpreted by this module.
Shuffle without changing the contents¶
The permutation relation preserves sequence length and the multiplicity of each element:
reference-profile · input revision 2 · CC0 1.0
SetupPermutation(before, after) ==
/\ Len(before) = Len(after)
/\ \A x \in SetupRange(before) \cup SetupRange(after) :
SetupMultiplicity(before, x) = SetupMultiplicity(after, x)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
As an authored example, a deck segment <<11, 12, 13>> may be reordered to <<13, 11, 12>>. Replacing it with <<13, 11, 11>> is not a permutation: one identifier was duplicated and another disappeared. This example explains the relation; it is not a retained checker trace or a shuffle-quality result.
At the ordinary opening draw, the first five elements move to the hand and the remaining suffix stays in the deck. A redraw recombines that seat’s deck and hand, requires a permutation, and deals a new first five. The recorded redraw set prevents using the same redraw opportunity again along this route. Profile effects and any authorized departures still need their explicit contracts.
Keep an override inside its boundary¶
A supplied override may change the details of a setup step. It must still produce the required successor stage:
reference-profile · input revision 2 · CC0 1.0
SetupNext(before, after, witness, override(_, _, _)) ==
/\ after.stage = SetupSuccessor(before.stage)
/\ IF witness.overrideRequired
THEN override(before, after, witness)
ELSE SetupStandardNext(before, after, witness)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The override parameter is a relation supplied by the enclosing model. Selecting it is not proof that an arbitrary alternative setup is legal. Its own record shape, permissions, effects and frame conditions need review. Likewise, a stage marker is not evidence that the work associated with that stage has actually completed in an implementation.
Separate ownership, control, execution and visibility¶
Ownership comes from the physical card’s metadata. Card control depends on its current situation: an object in play uses its placement information, while an objective in a seat’s objective area is controlled there. The controller of an ability and the executor of its effect may be specified separately. Follow SetupCardController and SetupEffectExecutor for those decisions.
None of those roles alone grants permission to read a hidden deck. A participant can own a deck and know its size without receiving its ordered contents. Hand visibility, explicit look grants and temporary set-aside permissions belong to the appropriate observation contracts. The metadata table used by the formal model must not be copied wholesale into a participant’s observation.
The schema and setup evidence identifies the selected inputs, model classes, bounds and review status. A prepared assertion about a setup relation and an explored transition driver answer different questions. Neither establishes unrestricted correspondence for arbitrary strings, every possible setup effect, or a complete game implementation.
Continue with turns and ending, or use characteristics to see how metadata becomes a context-dependent value.