Inspection procedures and observations¶
An inspection has two levels. The outer procedure determines the location, candidate choices and stopping policy. Each selected object can then receive an individual inspection procedure with its own current-target, visibility, option, completion and return conditions.
Read traversal and inspection for the guided path and zones for membership and look permissions. The ordinary profile is asymmetric: SideB inspects admitted SideA card objects. Other behavior requires the relevant explicit contract.
Bind the current object and location¶
An individual frame records its positive occurrence identifier, object, captured location, source zone, caller, containing inspection and traversal identifiers, encounter ancestry, and work flags. Its target guard checks the current table instead of relying on a physical name:
reference-profile · input revision 2 · CC0 1.0
ItemInspectionTargetPresent7(a,objects) ==
IF a.object \notin DOMAIN objects THEN FALSE
ELSE objects[a.object].form = "Card" /\ objects[a.object].side = "SideA" /\ objects[a.object].loc = a.originLocDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
The guard requires that the same current object remains a SideA card at the captured location. It does not allocate or follow a successor. A composed movement relation is responsible for keeping object, zone and location representations consistent.
An authored example is a frame bound to object 11 at location L. A later valid movement can remove 11 and create 12, or change the location associated with 11. The old presence test then fails. Copying the physical card identifier into the successor does not preserve the old inspection reference. This example is a guard illustration, not a retained checker trace.
Owner, controller, chooser and instruction executor are separate inputs. A physical owner’s association with the card does not decide every current look permission or authorize an intermediate operation.
Derive candidates before accepting a choice¶
The outer inspection takes a typed frame, current objects, relevant ordered deck, location/capacity facts and prohibition information. Its candidate derivation applies those inputs to the current state. A previously displayed candidate set is not automatically valid after child work changes that state.
Selection readiness has its own guards:
reference-profile · input revision 2 · CC0 1.0
InspectionSelectionReady7(b) ==
b.active /\ ~b.complete /\ b.step = "ProcedureCode1404a82ab3ee" /\ ~b.selectionPending /\ b.currentItemInspectionId = 0 /\
(RandomLimitApplies7(b) => b.limitSet) /\
(b.kind = "SchemaAtom018" => b.archivesPrepared) /\ SelectionWithinPolicy7(b.policy,Len(b.choices))Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The procedure must be active, at its selection step and free of an unfinished prior choice or child inspection. The appropriate random limit or discard-location preparation must also have been completed, and the choice count must remain within the policy.
The result is not permission to present every internal object identifier to a player. InspectionPresentation7 separates specifically offered choices from the random offer for the relevant concealed location. The random-result and exceptional-choice providers still have to establish their respective authority.
Hosting does not automatically add every hosted child to an inspection menu. Candidate derivation uses the relevant location relationships and restrictions. An object’s existence in the table is weaker than membership in the current candidate set.
Keep selection history and actual inspection history distinct¶
A recorded choice prevents the same current object from being chosen again under that inspection’s choice contract. Actual inspection history instead records the individual begin event and its occurrence identity.
RecordActualItemInspection7 requires that actual begin event and associates it with the relevant turn and containing procedures. A selection cancelled before beginning does not acquire an actual inspection merely because its identifier appeared in the choice sequence.
This distinction matters for limits and conditions that count different things. A count of choices, a count of begun inspections and a count of unique physical cards are not interchangeable summaries.
Grant visibility for the active bound procedure¶
ItemInspectionLookGrant7 grants a look while the child is active, incomplete and still attached to its target. Its SideA/SideB branches preserve the profile’s concealed-deck distinction. Other lawful viewers and an actual reveal-to-both instruction are separate contributions to the viewer set.
The source zone captured by the frame is meaningful to that rule. A caller must not replace it with whichever current zone makes a broader permission convenient. Likewise, a past look grant is not automatically a current grant for another object or location.
The inspection’s internal state may retain more information than a participant can see. A visible count or an offered random choice should not expose the underlying candidate identities through explanatory payloads.
Resolve permitted intermediate work¶
The intermediate stage offers its particular payable and legal options, with any applicable mandatory-choice restrictions. It is not an unrestricted paid-ability window. The subsequent objective-transfer stage separately distinguishes inapplicability, declined additional cost, inability and an admitted transfer procedure.
Payment, actual legality and completion of the chosen procedure are supplied or connected through their own contracts. Marking an option used does not immediately mark all its reactions complete. The parent frame must retain the corresponding resolving flags until that work has finished.
Movement or an authorized containing-procedure end can complete an active inspection early. An inspection cancelled before its begin event follows a different path. Normal completion, early completion and cancellation should not be made indistinguishable by an application-level success Boolean.
Complete the outer procedure and its return¶
The outer selection loop waits for its selected instruction and child return, then reevaluates candidates and the stopping policy. Completing its body does not by itself release its caller:
reference-profile · input revision 2 · CC0 1.0
ReturnInspectionToCaller7(before,after,actualInspectionEndWindowsAndCheckpointComplete,caller) ==
/\ before.complete /\ ~before.returned /\ ~before.selectionPending /\ before.currentItemInspectionId = 0
/\ actualInspectionEndWindowsAndCheckpointComplete /\ caller = before.caller
/\ after = [before EXCEPT !.returned = TRUE]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The return requires the completed frame, no unresolved selected child, the matching caller and actual completion of end windows/checkpoint work. A delayed inspection also needs its recorded release event and current permission to start; deferral does not establish those facts in advance.
The traversal and inspection evidence identifies selected configurations, actual outcomes and provider assumptions. Frame and assertion checks establish their stated cases. They do not establish every selection policy, random implementation, card-specific effect or unrestricted source transformation.