Information, conversions and supplied iteration¶
Some mechanisms change how a state is interpreted rather than opening a new action window. Information facts determine which values a seat may observe at a snapshot. A conversion changes an object’s effective properties while its retention condition holds. A detected loop can consume an explicitly supplied iteration witness. Each mechanism needs a typed context and a completion boundary before a surrounding procedure can rely on its result.
This page develops three examples from the additional contracts. It is a reading path into selected mechanisms, rather than an assertion that every interaction in the family has the same input domain. Read values and state, objects and lifetime and object operations for the underlying distinctions.
Derive a view from facts at one snapshot¶
An information fact contains a value, a set of viewers and a snapshot identifier. The catalogue can hold more than either seat may observe. A player’s current view selects facts that both name that player as a viewer and belong to the current snapshot:
reference-profile · input revision 2 · CC0 1.0
PlayerInformationView102(facts,player,currentSnapshot) ==
[id \in {i \in DOMAIN facts : player \in facts[i].viewers /\ facts[i].snapshot=currentSnapshot} |-> facts[id].value]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
An authored example has fact 31 with value 4, viewers {SideA}, and snapshot 9. At snapshot 9, SideA receives that value through this view and SideB does not. At snapshot 10, the old row is excluded until an appropriate current fact is supplied. This is a filter example, not a retained model execution.
Snapshot exclusion says what belongs to the current authoritative view. It does not assert that a person has forgotten a previous observation. Remembered open choices and current facts have explicit inputs; a host must choose the observation and memory interface that its research question requires.
Viewing grants also depend on object identity and location. CurrentLookViewers102 selects grants whose object, zone and location match the current object. A grant for an earlier lifetime or an earlier location is not a universal permission to follow the physical item after movement. Default zone visibility, controller-sensitive visibility and live grants are separate contributors to the resulting fact.
The supplied objects, controller map, live grants and remembered choices form the context. A complete internal catalogue is therefore not an acceptable observation payload merely because it is useful to an invariant checker.
Distinguish observation from a communicated claim¶
ObserveCurrentInformation102 appends an authoritative observation only for a current fact and a permitted viewer. CommunicateInformation102 records a claim in a transcript while preserving the underlying truth state.
For open information, the communication relation requires the claimed value to agree with the fact. Its hidden-information branch does not impose that equality. Receiving a claim consequently does not turn it into a newly authorized observation or modify the fact itself. A policy or interface that wishes to distinguish claims from authoritative observations must retain that distinction in its own data.
This boundary is relevant even in a two-seat model with no language processing. The formal relation handles typed values and roles. It does not interpret the meaning of arbitrary messages or establish what an opponent believes.
Retain converted properties only across the allowed boundary¶
A conversion record identifies its mode, physical item, creator, owner and gained properties. The objective mode and counter mode have different retention tests:
reference-profile · input revision 2 · CC0 1.0
ConversionRetained101(c,oldZone,newZone) ==
IF c.mode="Objective" THEN oldZone \in SetupObjectiveZones /\ newZone \in SetupObjectiveZones ELSE oldZone=newZoneDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
In the objective branch, both old and new zones must be score zones. In the counter branch, retention requires equal zones. The physical owner’s identity remains part of the conversion record; controller, host and current form require their own state relationships.
An authored example uses a valid counter conversion in zone StoreA. Moving between two locations within that same zone satisfies this retention test. Moving to StoreB does not. The predicate itself says whether the gained properties remain applicable; it does not perform either move or prove that a chosen destination is legal.
ConversionExitPost101 describes the exit result with a fresh successor object, the same physical item and owner, restored printed properties and appropriate retirement or removal evidence. Unaffected object rows are preserved. Reusing the old object identifier or silently keeping its converted properties would fail to describe that exit.
Hosting is a relationship to a current object. Restoring an ordinary card form clears hosting and deployed status in this exit contract; a broader movement procedure must still account for dependent objects and the checkpoints they create. The creator of a conversion is not automatically its owner, controller or cleanup executor.
Consume a detected loop with a witness¶
The mandatory-loop relation starts with an already detected loop frame. It takes a natural iteration count, a sequence of intermediate game values and an explicit two-state iteration operator:
reference-profile · input revision 2 · CC0 1.0
ResolveMandatoryLoop101(frame,afterFrame,beforeGame,afterGame,count,witness,Iteration(_,_)) ==
/\ frame.kind="Mandatory" /\ frame.phase="Detected" /\ frame.resolver \in SetupPlayers
/\ count \in Nat /\ Len(witness)=count+1
/\ witness[1]=beforeGame /\ witness[count+1]=afterGame
/\ \A i \in 1..count : Iteration(witness[i],witness[i+1])
/\ afterFrame=[frame EXCEPT !.phase="Ended",!.iterations=count]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
An authored example chooses count 2. The witness must have three entries, beginning at the supplied before state and ending at the supplied after state. The iteration relation must hold from entry one to two and from entry two to three. A sequence of plausible-looking endpoints without those two checks is insufficient. For count zero, the single witness entry binds both endpoints.
The frame identifies a resolver seat and must already be in the detected mandatory phase. The relation records that this resolution ended with the chosen count. It neither detects arbitrary loops nor calculates the iteration relation from natural-language instructions. Optional loops use a separate disposition contract with their own traversal and prohibition inputs.
Preserve batch and caller boundaries¶
Additional mechanisms can create work that an outer ability or checkpoint must await. For example, DamageBatchReadyForConditionals104 requires the completed batch, matching completion event and final object state before presenting that boundary to conditional processing. A partial selection or an intermediate object map cannot stand in for that completed batch.
The surrounding host must bind provider facts such as permissions, current metadata, legal destinations, batch effects and iteration semantics to the intended snapshot and procedure. Each relation constrains its explicit before and after values; a composed action must also frame the rest of its state and preserve the caller relationships described in checkpoints.
The abilities and additional mechanisms evidence identifies the actual selector cases, transition drivers and controls. The worked examples on this page explain the contracts independently of those traces. They make no claim that every parameter choice, mechanism interaction or branch has been reached by a retained finite model.