Turn procedures and ending conditions¶
The turn contracts separate ownership of time from permission to act. A valid turn has one owner, a phase from that owner’s sequence and a positive identifier. A complete turn procedure additionally establishes the order of formal events, decisions, reactions and handoff.
For the guided path, read turns and ending. For ordinary option priority and matching returns, read priority and completion.
Inputs and layers of state¶
TurnFrameValid5 expects a record with owner, phase, id, formalBegun, formalEnded and begunCounts. The owner is one of the two profile seats, the identifier is positive, the flags are Boolean and begun counts are nonnegative integers indexed by both seats.
A procedure frame adds its current step and decision state. An action frame adds cost/effect status and any nested structure awaiting return. These records answer different questions. Neither an object’s controller nor an effect’s executor becomes the turn owner merely by taking an authorized opportunity.
The contracts consume supplied facts about actual timing, payment and completion. Those facts must come from the containing procedure or provider. A formal relation that accepts actualStepIncludingReactionsComplete checks how that fact is used; it does not prove the provider computed it correctly. Observation rules also remain in force during every phase: turn ownership does not make a private hand or deck public.
Formal begin is an event with a counted occurrence¶
The begin relation requires a valid frame, clear begin/end flags, an actual formal-begin step and the matching event set. It changes the begin flag and the owner’s begun count together:
reference-profile · input revision 2 · CC0 1.0
TurnFormalBegin5(before, after, atActualFormalBeginStep, events) ==
/\ TurnFrameValid5(before) /\ ~before.formalBegun /\ ~before.formalEnded
/\ atActualFormalBeginStep /\ events = {TurnBeginEvent5(before)}
/\ after = [before EXCEPT !.formalBegun = TRUE,!.begunCounts[before.owner] = @+1]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
Opening a frame and formally beginning its turn are therefore distinct. The event carries the turn identifier, so a consumer can distinguish successive occurrences even when the same seat becomes active again.
The after-record is an EXCEPT update. It preserves that record’s other fields. It says nothing by itself about unrelated object tables, resource balances or pending windows in a larger state; the caller must frame those components or update them through their own relations.
A valid record is also weaker than a valid history. The detailed procedure wrappers associate each step with the appropriate formal flag and completion check. A caller should not treat frame validity as permission to jump to any phase it contains.
Actions wait for their cost boundary and exact child¶
An action starts only in its owner’s action phase, at an actual permitted action window, after its costs are paid and while no other action is resolving. Its initial status records that cost reactions are still due.
reference-profile · input revision 2 · CC0 1.0
ActionEffectsBegin5(before,after,costCheckpointAndReactionsDrained) ==
/\ before.status = "CostReactions" /\ costCheckpointAndReactionsDrained
/\ after = [before EXCEPT !.status = "Effects"]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
Only a drained cost checkpoint/reaction boundary advances that frame into effects. Nested work then records a concrete structure identifier. ActionNestedReturn5 compares the completed identifier with the recorded one before restoring the effects stage.
For an authored example, let an action wait for child 31. A completion receipt for child 32 does not satisfy that return. When child 31 actually completes, the action can return to effects; only after all remaining effects resolve can it become complete. This illustrates a guard, not a trace taken from a checker.
The action’s complete status is the advance condition for its caller. Completion of one child, exhaustion of a balance, or a participant’s pass is not an alternative proof of that status.
Ending a phase does not perform every ending step¶
The reference profile has separate ordinary and explicitly directed phase-ending paths. A directed end can close the current action-phase opportunities and make checkpoint work due. It still has to pass its ending checkpoint and reaction-drain relations before entering discard.
At discard, the effective maximum hand size is an input. The ordinary discard relation chooses the required batch, updates membership and arrival faces, and records its event when there is a nonempty batch. A skipped discard step and a negative-limit ending check have different branches. They should not be collapsed into a generic “discard until legal” loop.
TurnFormalEnd5 marks the formal end at its actual boundary. TurnHandoff5 additionally requires the old turn procedure to be complete. Handoff opens the other seat’s next frame, clears its formal flags and preserves begun counts; the next formal begin occurs later.
Objective totals and game outcomes are separate¶
The object kernel sums objective points in a seat’s objective area and identifies seats meeting its fixed threshold:
reference-profile · input revision 2 · CC0 1.0
ObjectiveWinners(t) == {p \in Players : Points(t, p) >= 7}Definition and resolved references · Exact module download · Source bundle and reproduction instructions
This kernel uses seven as its threshold. It is a particular reference-profile rule, not a parameterized statement about all objective games. The characteristic contracts separately describe the effective point inputs and which objects contribute in a objective area.
DoCheckpoint combines current objective winners with supplied simultaneous winners at a ready checkpoint. It records the outcome and clears the checkpoint obligation. Its ordering tests winners before the ordinary pending-retirement branch. A consumer must preserve that boundary rather than infer the result from any intermediate counter change.
DoFatal handles its stated damage, discard-step and required-draw conditions under a supplied valid-procedure guard. A negative effective hand limit is relevant at the actual discard boundary; an empty deck is relevant to the specified required draw. Merely observing one of those values elsewhere does not establish the same ending event.
What the finite evidence can establish¶
The turns and objectives evidence identifies the actual model configurations, exact observations and bounds. A prepared assertion selector can establish the stated calculations for supplied cases. A transition driver can explore its admitted turn/action branches. Neither model class automatically establishes every provider, every branch of every associated operator, unrestricted label transformations, or eventual termination of all play.
These contracts give useful local obligations for a composed implementation: preserve event identity, require matching child returns, finish phase work before handoff, and evaluate each ending at its own boundary. Each obligation still needs the surrounding state, typed inputs and provider conformance that make it meaningful.