Event resolution

instant-and-turn-boundary

Applies for every adoption

An instant is one moment the game treats as simultaneous. A turn boundary the adoption can construct is an instant like any other; where there is no turn boundary, that clause asserts nothing.

Given

events at one moment Instance treats as simultaneous, including a turn boundary where the adoption has one

When

• the moment is resolved

Then

• all events belong to one instant and follow one lifecycle
• a constructed turn boundary is handled as an instant like any other; where no turn boundary exists, that clause asserts nothing

Diagnostics

• Instance-instant-trace

waiting-active-and-first-boundary

Applies for every adoption

A waiting event is accepted but has not begun. An active event is applying ordered effects. Every active event visits an effect boundary before its first effect.

Given

an accepted event before and during resolution

When

• the event enters the waiting set and is selected

Then

• before selection it is recorded as a waiting event that has not begun
• during ordered effect application it is recorded as the active event
• the active event visits an effect boundary before its first effect

Diagnostics

• Instance-waiting-set
• Instance-event-trace

ending-event-records-nothing

Applies for every adoption

Each ending event the adoption can construct follows the ordinary event lifecycle but records no outcome when it resolves. Only step 15 records an outcome, after the waiting set is empty. Where none exists, this test asserts nothing.

Given

each ending event the adoption can construct whose effects make an ending condition hold

When

• the ending event resolves and the instant later reaches settlement

Then

• resolving the ending event records no match outcome
• an outcome is recorded only after the waiting set is empty at step 15
• the ending record distinguishes event resolution from outcome recording
• where no ending event exists, this test asserts nothing

Diagnostics

• Instance-event-trace
• Instance-ending-record

file-order-never-decides-resolution

Applies for every adoption

Changing container order or document order without changing declarations never changes event resolution. Rank, a rank tie, and within-class order decide the sequence; document order never does. Step 5 says container order in the adoption file never selects an event.

Given

two equivalent Instance adoption documents whose container order or document order differs, with the same recorded random inputs where a declared random order is used

When

• the same instant is resolved from the same pre-instant state under each document

Then

• the two runs select and resolve the same events in the same declared order
• no event order is taken from container order or document order

Diagnostics

• Instance-order-trace
• Instance-settlement-report

rejection-case-nothing-changes

Applies when row result is Nothing changes.

Row.id overrides or repeats the default with nothing-changes: it creates no event, changes no game state, spends no cost, and advances no clock because of the rejection. Row.declared in identifies the case; the test names the address and restates nothing from it.

Given

a proposal that meets the rejection case at Row.declared in

When

• the proposal is checked from a recorded pre-attempt state

Then

• the proposal ends without creating an event
• no game state changes, no cost is spent, and no clock advances because of the rejection
• the proposal log distinguishes this rejection from an accepted action that later produces no effect

Diagnostics

• Instance-proposal-log
• Instance-state-before-after

rejection-case-cost-taken

Applies when row result is Cost taken.

Row.id rejects and applies the complete declared cost once, creates no event, produces no action effect, and advances no clock because of the rejection. Row.declared in identifies the case; the test names the address and restates nothing from it.

Given

a proposal that meets the rejection case at Row.declared in with a distinguishable complete declared cost

When

• the proposal is checked

Then

• the proposal ends without creating an event
• the complete declared cost is applied once, no action effect is produced, and no clock advances because of the rejection
• the proposal log distinguishes rejection with cost from acceptance followed by failure

Diagnostics

• Instance-proposal-log
• Instance-cost-log

rejection-case-clock-advances

Applies when row result is Clock advances.

Row.id rejects, spends no cost, produces no action effect, and advances once the clock selected by Row.clock rule declared in. The test demands that observable consequence, names the address, and restates nothing from it or Row.declared in.

Given

a proposal that meets the rejection case at Row.declared in and a distinguishable clock state governed at Row.clock rule declared in

When

• the proposal is checked

Then

• the proposal ends without creating an event
• the clock selected by Row.clock rule declared in advances once, no cost is applied, and no action effect is produced
• the proposal log distinguishes this rejection-driven advance from independently advancing time

Diagnostics

• Instance-proposal-log
• Instance-clock-trace

rejection-case-cost-and-clock

Applies when row result is Cost and clock.

Row.id rejects, applies the complete declared cost once, advances once the clock selected by Row.clock rule declared in, and produces no action effect. The test names both addresses and restates nothing from them.

Given

a proposal that meets the rejection case at Row.declared in, its complete declared cost, and a distinguishable clock state governed at Row.clock rule declared in

When

• the proposal is checked

Then

• the proposal ends without creating an event
• the complete declared cost is applied once and the clock selected by Row.clock rule declared in advances once
• no action effect is produced and the proposal log distinguishes rejection from acceptance

Diagnostics

• Instance-proposal-log
• Instance-cost-log
• Instance-clock-trace

rejection-case-derates-and-enters-lifecycle

Applies when row result is Derate.

Row.id accepts a scaled action rather than rejecting it. Row.scale rule declared in supplies the scale; the accepted action creates one payload once and continues through the event lifecycle. The test names both addresses and restates nothing from them.

Given

a proposal that meets the case at Row.declared in and can be scaled by Row.scale rule declared in

When

• the proposal is checked and the accepted event settles

Then

• the scale rule at Row.scale rule declared in produces the action's complete scaled effect and cost
• the proposal is recorded as accepted rather than rejected, creates one payload once, and continues through the event lifecycle
• the proposal log distinguishes the accepted scaled action from a rejected action

Diagnostics

• Instance-proposal-log
• Instance-event-trace
• Instance-cost-log

rejection-default-applies-without-row

Applies when Rejected action effect is Nothing changes or Cost taken or Not applicable.

Bind text

Given

Bind given

When

• the proposal is checked

Then

• Bind result

Diagnostics

• Instance-proposal-log
• Instance-cost-log
• Instance-clock-trace

rejection-is-repeatable-from-identical-state

Applies for every adoption

The same proposal rejected from an identical pre-attempt state produces the same result. The comparison resets the whole pre-attempt state; it does not repeat from state changed by an earlier attempt.

Given

two executions of each rejecting proposal the adoption can construct from identical recorded pre-attempt states

When

• the proposal is checked in each execution

Then

• both executions produce the same rejection result and the same recorded cost and clock consequence
• the comparison starts from identical pre-attempt state rather than the state left by the first execution
• where no rejecting proposal exists, this test asserts nothing

Diagnostics

• Instance-proposal-log
• Instance-state-before-after

accepted-proposal-creates-one-event

Applies for every adoption

An accepted proposal creates one payload once and enters its declared event class at its due instant. Where it has an ordinary cost, that cost commits once at the point its rule names; otherwise the cost clause asserts nothing. The payload captures every value that must survive later source loss; where no such loss can occur, that observation asserts nothing.

Given

a valid proposal with distinguishable payload values, event class, due instant, and an ordinary cost where its Fixed rule declares one

When

• the proposal is accepted and its event is admitted
• where the adoption can construct later source loss, the source becomes unavailable before a captured value is used

Then

• where an ordinary cost is declared, it is committed once at the point its Fixed game rule names; otherwise the cost clause asserts nothing
• one event payload is created once and enters its declared event class at its due instant
• the payload contains every value required to survive later source loss, while uncaptured state is read only when an effect resolves
• where later source loss cannot be constructed, the payload-survival observation asserts nothing

Diagnostics

• Instance-proposal-log
• Instance-cost-log
• Instance-waiting-set
• Instance-event-trace

new-event-uses-one-admission-path

Applies for every adoption

After an instant opens, a valid declared interrupt enters only through the interrupt path. Every other newly created event due now follows caused-events. An unavailable branch asserts nothing, and no event uses both paths.

Given

events created after an instant opens, including valid declared interrupts and other new events where the adoption can construct them

When

• each new event is admitted

Then

• an event backed by a valid interrupts row enters only through the interrupt path and is governed by interrupt-entry
• every other new event due now follows caused-events
• a branch the adoption cannot construct asserts nothing and no event uses both paths

Diagnostics

• Instance-proposal-log
• Instance-interrupt-report
• Instance-caused-event-report

lowest-eligible-rank-resolves-first

Applies for every adoption

At every selection, the lowest eligible rank resolves first without changing the selected event's payload. Where no instant has two eligible ranks, the comparison asserts nothing. Step 4 selects the lowest eligible rank; step 5 selects within the class without changing the payload.

Given

each instant the adoption can construct with eligible waiting events from at least two declared ranks

When

• the next waiting event is selected repeatedly

Then

• each selection comes from the lowest rank that is eligible at that selection
• selection does not change the selected event's payload
• where no instant has two eligible ranks, the comparison asserts nothing

Diagnostics

• Instance-waiting-set
• Instance-order-trace

event-class-never-passes-lower-rank

Applies for every adoption

An event of Row.id at rank Row.rank never resolves before an eligible lower-rank event in the same instant. Where the adoption cannot construct that pairing, the test asserts nothing.

Given

an eligible Row.id event and an eligible event of a lower declared rank in the same instant

When

• the waiting set is selected

Then

• the lower-rank event is selected before the Row.id event
• where no lower-rank event is eligible with Row.id, this test asserts nothing

Diagnostics

• Instance-waiting-set
• Instance-order-trace

within-class-stable-index

Applies when row order is Stable index.

Within Row.class id, lower Row.index name resolves first. Where the row names a second index, equal first numbers resolve by it; otherwise equal first numbers cannot arise or cannot change the result.

Given

two eligible Row.class id events with different Row.index name values, plus equal first values where the row names a second index and the adoption can construct them

When

• their within-class order is selected

Then

• the event with the lower Row.index name resolves first
• where the row names a second index, equal first numbers resolve by the lower second number; otherwise equal first numbers cannot arise or cannot change the result
• the order trace distinguishes selection by stable index from selection by rank or container order

Diagnostics

• Instance-order-trace

within-class-arrival-order

Applies when row order is Arrival order.

Within Row.class id, earlier admission resolves first, and admission order remains stable for the complete instant.

Given

two eligible Row.class id events admitted at distinguishable times in one instant

When

• their within-class order is selected more than once during the instant

Then

• the earlier admitted event resolves first
• admission order remains stable for the complete instant and never changes with container order

Diagnostics

• Instance-proposal-log
• Instance-order-trace

within-class-map-reading-order

Applies when row order is Map reading order.

Within Row.class id, the grid at Row.grid declared in supplies its own first row and first column. The first row resolves first, then the first column. The test names the address and restates nothing from it.

Given

eligible Row.class id events in different rows and columns of the grid cited at Row.grid declared in

When

• their within-class order is selected

Then

• the event in the grid's own first row resolves first and, within one row, the event in its own first column resolves first
• the order trace attributes the result to map reading order rather than container order

Diagnostics

• Instance-order-trace

within-class-clockwise-order

Applies when row order is Clockwise.

Within Row.class id, the grid at Row.grid declared in supplies the centre, first direction, and clockwise sense. Clockwise angle orders the events, and lower Row.index name breaks equal angle and distance. The test names the address and restates nothing from it.

Given

eligible Row.class id events around the centre and first direction of the grid at Row.grid declared in, including equal angle and distance

When

• their within-class order is selected

Then

• events resolve by clockwise angle from the grid's centre and first direction
• equal angle and distance resolve by lower Row.index name
• the order trace attributes the result to clockwise order and its stable-index tie-break

Diagnostics

• Instance-order-trace

within-class-no-visible-order

Applies when row order is No visible order.

Row.class id exposes no within-class order: no event observes another of that class, and every permitted order yields the same game state and player-facing result. If two cannot be ready together, the comparison asserts nothing.

Given

every permitted execution order of eligible Row.class id events from the same pre-instant state

When

• the instant settles under each permitted order

Then

• no Row.class id event observes another event of that class during the instant
• every permitted order produces the same game state and player-facing result
• where two such events cannot be ready together, the comparison asserts nothing

Diagnostics

• Instance-order-trace
• Instance-settlement-report

within-class-declared-random-order

Applies when row order is Declared random.

Within Row.class id, the random rule at Row.rule declared in produces one total order for the instant; container order never decides it. The test demands the produced order and restates nothing from the cited rule.

Given

eligible Row.class id events and recorded random inputs for the rule at Row.rule declared in

When

• the rule produces their within-class order

Then

• one total order is produced for the instant and the events resolve in it
• container order never selects or changes the result
• the order trace records the cited rule and the order it produced

Diagnostics

• Instance-order-trace
• Instance-random-record

within-class-game-rule-order

Applies when row order is Game rule.

Within Row.class id, Row.rule declared in produces one total deterministic order; container order never decides it. The test demands the produced order and restates nothing from the cited rule.

Given

eligible Row.class id events whose order is governed at Row.rule declared in

When

• their within-class order is selected

Then

• the cited rule produces one total deterministic order and the events resolve in it
• container order never selects or changes the result
• the order trace records the cited rule and produced order

Diagnostics

• Instance-order-trace

rank-tie-stable-index

Applies when row tie break is Stable index.

At rank Row.rank, Row.id produces one total order over Row.class ids with lower Row.index name first. Where the row names a second index, equal first numbers resolve by it; otherwise equal first numbers cannot arise or cannot change the result.

Given

eligible events of the classes listed by Row.class ids at shared rank Row.rank with different Row.index name values, plus equal first values where the row names a second index

When

• the shared-rank order is selected

Then

• one total order over all events of all listed classes is produced with lower Row.index name first
• where the row names a second index, equal first numbers resolve by the lower second number; otherwise equal first numbers cannot arise or cannot change the result
• the order trace distinguishes the rank tie from ordinary within-class selection

Diagnostics

• Instance-order-trace

rank-tie-arrival-order

Applies when row tie break is Arrival order.

At rank Row.rank, Row.id produces one total order over Row.class ids with earlier admission first, and admission order stays stable for the instant.

Given

events of the classes listed by Row.class ids admitted at distinguishable times at shared rank Row.rank

When

• the shared-rank order is selected

Then

• one total order over all events of all listed classes is produced with earlier admission first
• admission order remains stable for the complete instant

Diagnostics

• Instance-proposal-log
• Instance-order-trace

rank-tie-map-reading-order

Applies when row tie break is Map reading order.

For Row.id, the grid at Row.grid declared in supplies its own first row and first column and produces one total order over Row.class ids. The test names the address and restates nothing from it.

Given

eligible events of Row.class ids in different rows and columns of the grid at Row.grid declared in

When

• the shared-rank order is selected

Then

• one total order over all events of all listed classes follows the grid's own first row and then its own first column
• the order trace distinguishes the rank tie from container order

Diagnostics

• Instance-order-trace

rank-tie-clockwise-order

Applies when row tie break is Clockwise.

For Row.id, Row.grid declared in supplies the centre, first direction, and clockwise sense for one total order over Row.class ids; lower Row.index name breaks equal angle and distance. The test names the address and restates nothing from it.

Given

eligible events of Row.class ids around the centre and first direction of Row.grid declared in, including equal angle and distance

When

• the shared-rank order is selected

Then

• one total order over all events of all listed classes follows clockwise angle from the grid's centre and first direction
• equal angle and distance resolve by lower Row.index name

Diagnostics

• Instance-order-trace

rank-tie-no-visible-order

Applies when row tie break is No visible order.

For Row.id, any total order over Row.class ids is permitted only because no tied event observes another and every permitted order yields the same state and player-facing result. An unavailable pairing asserts nothing.

Given

every permitted total order of eligible events from Row.class ids at rank Row.rank

When

• the instant settles under each permitted order

Then

• no event in the tied classes observes another tied event during the instant
• every permitted total order produces the same game state and player-facing result
• where events from two listed classes cannot be ready together, that comparison asserts nothing

Diagnostics

• Instance-order-trace
• Instance-settlement-report

rank-tie-declared-random-order

Applies when row tie break is Declared random.

For Row.id, the random rule at Row.rule declared in produces one total order over Row.class ids; container order never decides it. The test demands the produced order and restates nothing from the cited rule.

Given

eligible events of Row.class ids and recorded random inputs for Row.rule declared in

When

• the shared-rank order is selected

Then

• the cited rule produces one total order over all listed classes for the instant and the events resolve in it
• container order never selects or changes the result

Diagnostics

• Instance-order-trace
• Instance-random-record

rank-tie-game-rule-order

Applies when row tie break is Game rule.

For Row.id, Row.rule declared in produces one total deterministic order over Row.class ids; container order never decides it. The test demands the produced order and restates nothing from the cited rule.

Given

eligible events of Row.class ids governed at Row.rule declared in

When

• the shared-rank order is selected

Then

• the cited rule produces one total deterministic order over all listed classes and the events resolve in it
• container order never selects or changes the result

Diagnostics

• Instance-order-trace

general-within-class-order

Applies when Within class order is Stable index or Arrival order or Map reading order or Clockwise or No visible order or Declared random.

For every class without a class row and without a shared rank, Bind order. Where no such class or pair exists, this test asserts nothing.

Given

each event class with no within-class-rules row and no shared rank

When

• two events of that class are ready together where the adoption can construct them

Then

• Bind order
• where no such class or pair exists, this test asserts nothing

Diagnostics

• Instance-order-trace
• Instance-settlement-report

presentation-never-holds-event

Applies when Presentation timing is Never.

Row.event class events never wait for Row.presentation cue. Row.declared in names the cue rule; the test names the address and restates nothing from it.

Given

a selected Row.event class event while Row.presentation cue is unfinished

When

• presentation waiting is checked

Then

• the event is admitted immediately and never waits for the cue
• the instant's order and game timing are unchanged by that cue

Diagnostics

• Instance-order-trace
• Instance-presentation-trace

presentation-delay-holds-following-events

Applies when Presentation timing is May delay.

An unfinished Row.presentation cue holds Row.event class and every event behind it until the cue finishes; none passes it, and the instant cannot close. Row.declared in names the cue rule; the test names the address and restates nothing from it.

Given

a selected Row.event class event with unfinished Row.presentation cue and a later eligible event

When

• the cue remains unfinished and then finishes under Row.declared in

Then

• the selected event and every event behind it remain held until the cue finishes
• no later event passes it, and the held event then resumes with its original payload
• the instant remains open while the event is held

Diagnostics

• Instance-waiting-set
• Instance-presentation-trace
• Instance-order-trace

presentation-delay-skips-only-held-event

Applies when Presentation timing is May delay and reorder.

While Row.presentation cue is unfinished, only the selected Row.event class event is skipped; later eligible events pass it, its original payload remains, and the instant cannot close. Row.declared in names the cue rule; the test names the address and restates nothing from it.

Given

a selected Row.event class event with unfinished Row.presentation cue and a later eligible event

When

• presentation waiting skips the selected event and the cue later finishes under Row.declared in

Then

• only the held event is skipped and selection returns to the waiting set
• the later eligible event resolves before it, while the held event keeps its original payload
• the held event becomes eligible when the cue finishes and the instant remains open until it resolves

Diagnostics

• Instance-waiting-set
• Instance-presentation-trace
• Instance-order-trace

unnamed-event-has-no-presentation-wait

Applies for every adoption

A selected event named by no presentation-driven-events row never waits for a cue of its own; where the adoption answers may-delay and it stands behind a held event, it waits with that event; otherwise it is admitted at once. Where every selected class has a row, this test asserts nothing. This follows the presentation-timing option semantics and step 6.

Given

each selected event class not named by a presentation-driven-events row

When

• presentation waiting is checked

Then

• the event never waits for a cue of its own; where the adoption answers may-delay and it stands behind a held event, it waits with that event; otherwise it is admitted at once
• where every selected class is named by a presentation row, this test asserts nothing

Diagnostics

• Instance-presentation-trace
• Instance-order-trace

terminal-collision-rows-cover-ending-pairs

Applies for every adoption

This declaration check reads the adoption and its Fixed ending rules, not the running game. A terminal-collisions row must exist for every win-and-loss pair that can meet at one instant; the collection's when-empty sentence supplies the empty direction. A constructible pair with no row is a defect this test fails by construction; where no pair can meet, the check asserts nothing.

Given

the Instance adoption and the ending pairs its Fixed rules can construct, not the running game

When

• a reviewer compares every pair with terminal-collisions

Then

• a terminal-collisions row exists for every pair that can produce a win and a loss at the same instant
• the terminal-collisions when-empty sentence supplies the empty direction
• a constructible pair with no row is a defect this test fails by construction; where no pair can meet, this check asserts nothing

Diagnostics

• Instance-declaration-record
• Instance-ending-record

same-target-rows-cover-removal-collisions

Applies for every adoption

This declaration check reads the adoption and its Fixed removal rules, not the running game. A same-target-cases or same-target-exceptions row must exist for every target kind with a same-instant removal collision; the row sets' when-empty sentences supply the empty direction. A constructible target kind with no row is a defect this test fails by construction; where none can occur, the check asserts nothing. This says nothing about a shared target with no removal.

Given

the Instance adoption and the target-removal cases its Fixed rules can construct, not the running game

When

• a reviewer compares every target kind with same-target-cases and same-target-exceptions

Then

• a same-target-cases or same-target-exceptions row exists for every target kind for which two events can each remove one target at one instant
• the two row sets' when-empty sentences supply the empty direction
• a constructible target kind with no row is a defect this test fails by construction; where no such collision can occur, this check asserts nothing

Diagnostics

• Instance-declaration-record
• Instance-collision-report

caused-event-rows-cover-due-now-causes

Applies for every adoption

This declaration check reads the adoption and its Fixed cause rules, not the running game. A caused-event-kinds row must exist for every non-interrupt event caused due in the same instant; the collection's when-empty sentence supplies the empty direction. A constructible due-now caused event with no row is a defect this test fails by construction; where none exists, the check asserts nothing.

Given

the Instance adoption and the non-interrupt event causes its Fixed rules can construct, not the running game

When

• a reviewer compares every newly caused due-now kind with caused-event-kinds

Then

• a caused-event-kinds row exists for every non-interrupt event caused due in the same instant
• the caused-event-kinds when-empty sentence supplies the empty direction
• a constructible due-now caused event with no row is a defect this test fails by construction; where no such event exists, this check asserts nothing

Diagnostics

• Instance-declaration-record
• Instance-caused-event-report

interrupt-rows-cover-stops-and-replacements

Applies for every adoption

This declaration check reads the adoption and its Fixed interaction rules, not the running game. An interrupts row must exist for every event that stops or replaces another after selection, including before its first effect; the collection's when-empty sentence supplies the empty direction. A constructible stopping or replacement interaction with no row is a defect this test fails by construction; where none exists, the check asserts nothing.

Given

the Instance adoption and the event interactions its Fixed rules can construct after resolution starts, not the running game

When

• a reviewer compares every stopping or replacement interaction with interrupts

Then

• an interrupts row exists for every event that stops or replaces another after selection, including before its first effect
• the interrupts when-empty sentence supplies the empty direction
• a constructible stopping or replacement interaction with no row is a defect this test fails by construction; where no such interaction exists, this check asserts nothing

Diagnostics

• Instance-declaration-record
• Instance-interrupt-report

same-target-general-resolution

Applies when Two events one target is Only first resolves or All resolve one ending or All resolve each ending.

For Row.target kind, Bind result. Row.declared in identifies the collision case; the test names the address and restates nothing from it.

Given

two events in one instant that can each remove one Row.target kind under Row.declared in

When

• their collision group resolves

Then

• Bind result
• the collision report distinguishes this result from an orphan result or an ordinary event with no effect

Diagnostics

• Instance-collision-report
• Instance-event-trace

same-target-exception-resolution

Applies when row resolution is Only first resolves or All resolve one ending or All resolve each ending.

Row.target kind is an exception: Bind result. The row replaces the general answer only for this target kind. Row.declared in identifies the collision; the test names the address and restates nothing from it.

Given

two events in one instant that can each remove one Row.target kind under Row.declared in

When

• their collision group resolves

Then

• Bind result
• this row replaces the general answer only for Row.target kind
• the collision report distinguishes this result from an orphan result

Diagnostics

• Instance-collision-report
• Instance-event-trace

collision-precedes-orphan-check

Applies for every adoption

For each same-target collision group the adoption can construct, grouping settles before the orphan check and removal inside it never orphans another member. Under all-resolve-one-ending, the target stays live for members and for a non-member that resolves before the group ends. An unavailable case asserts nothing.

Given

each same-target collision group the adoption can construct, plus each non-member event that can resolve before deferred removal

When

• the group is settled and source and target availability are checked

Then

• the same-target decision is settled before the general orphan check
• removal inside the group never turns another group member into an orphan
• under all-resolve-one-ending, the target remains live for group members and any non-member that resolves before the group ends
• where no such group or non-member exists, the corresponding clause asserts nothing

Diagnostics

• Instance-collision-report
• Instance-orphan-report
• Instance-event-trace

orphan-override-resolves-what-remains

Applies when row resolution is Resolves what remains.

For Row.id, a missing Bind object leaves the captured payload in place. Only effects needing that object are skipped; every independent effect resolves. Row.declared in identifies the case; the test names the address and restates nothing from it.

Given

a waiting and then active Row.event class event whose required Bind object becomes unavailable under Row.declared in

When

• availability is checked before the first effect and at every later effect boundary

Then

• the event keeps its captured payload and skips only effects requiring the missing object
• every independent remaining effect resolves in declared order
• the orphan report distinguishes this route from cancellation and from an event that independently had no applicable effect

Diagnostics

• Instance-orphan-report
• Instance-event-trace

orphan-override-is-cancelled

Applies when row resolution is Is cancelled.

For Row.id, losing the required Bind object removes a waiting event or discards an active event's remaining effects. Committed costs and effects remain. Row.declared in identifies the case; the test names the address and restates nothing from it.

Given

waiting and active Row.event class events whose required Bind object becomes unavailable under Row.declared in

When

• availability is checked before the first effect and at every later effect boundary

Then

• a waiting event is removed and an active event discards every remaining effect
• no committed cost or effect is restored
• the orphan report distinguishes cancellation from resolving what remains and from an event that independently produced no effect

Diagnostics

• Instance-orphan-report
• Instance-event-trace
• Instance-cost-log

orphan-default-row

Applies when Orphaned events is Resolves what remains or Is cancelled and row resolution is Default.

Row.id selects the adoption default for a missing Bind object: the event Bind result. Row.declared in identifies the case; the test names the address and restates nothing from it.

Given

a waiting and then active Row.event class event whose required Bind object becomes unavailable under Row.declared in

When

• availability is checked before the first effect and at every later effect boundary

Then

• the event Bind result
• the orphan report identifies use of the adoption default and distinguishes its observable result from the other route

Diagnostics

• Instance-orphan-report
• Instance-event-trace
• Instance-cost-log

undeclared-orphan-is-invalid

Applies for every adoption

This declaration check reads the adoption, not the running game. Every event that can lose a required source or target has an orphan-cases row. Outside those rows, missing-object behavior is invalid rather than implied and is a defect this test fails by construction. Where no event can become an orphan, this test asserts nothing.

Given

each event that can lose a required source or target while waiting or resolving

When

• a reviewer compares that case with orphan-cases before the build is audited

Then

• every such case has a matching orphan-cases row
• a missing object outside those rows is an invalid adoption and receives no implied cancellation or remaining-effects result
• an undeclared case is a defect this test fails by construction; where no event can lose a required object, this test asserts nothing

Diagnostics

• Instance-orphan-report
• Instance-declaration-record

active-event-commits-effects-in-order

Applies for every adoption

An active event visits the boundary before its first effect, applies effects in its Fixed rule's order, and commits each effect before the next boundary. If no multi-effect event exists, the between-effects observation asserts nothing.

Given

an eligible event with two or more ordered effects where the adoption can construct one

When

• the event becomes active and applies its effects

Then

• the event visits the boundary before its first effect
• effects are applied in the order stated by the event's Fixed game rule
• each effect commits before the next declared boundary is visited
• where no multi-effect event exists, the between-effects observation asserts nothing

Diagnostics

• Instance-event-trace
• Instance-interrupt-report

interrupt-stops-original

Applies when Interrupt entry is Before next effect or After current effect or At normal rank and row result is Stop original.

For an active Row.active class event whose Row.boundary granularity boundaries are named at Row.declared in, Row.id creates one valid Row.interrupt class interrupt offered at a named boundary and Bind entry. Where the interrupt enters at a boundary of the active event, event order selects one valid interrupt, the active event advances only to permitted boundaries while it waits, and the interrupt passes through steps 6 to 11 before changing that event; where it joins the next instant instead, the active event runs to completion in this one. Then Bind result. A presentation skip returns to the interrupted boundary; where none is possible, that clause asserts nothing. Row.declared in supplies validity and the finite chain; the test names the address and restates nothing from it.

Given

an active Row.active class event whose Row.boundary granularity boundaries are named at Row.declared in, and a valid Row.interrupt class interrupt offered at one of them

When

• the valid interrupt is discovered, selected, and resolved

Then

• one interrupt event is created through the interrupt path and Bind entry
• where the interrupt enters at a boundary of the active event: when several interrupts are valid, event rank, the shared-rank order, and then within-class order select one; the active event advances only to boundaries Row.declared in permits while it waits; and the interrupt passes through presentation waiting, collision grouping, orphan checks, and its own boundaries before changing that event
• where the interrupt joins the next instant instead, the active event runs to completion in this one
• Bind result
• only one selected interrupt resolves at a time and the report distinguishes a valid interrupt from an invalid offer
• where presentation skips the interrupt, control returns to the interrupted event's boundary rather than step 4; where no such skip is possible, this clause asserts nothing

Diagnostics

• Instance-interrupt-report
• Instance-event-trace
• Instance-cost-log

interrupt-replaces-remaining-effects

Applies when Interrupt entry is Before next effect or After current effect or At normal rank and row result is Replace remaining effects.

For an active Row.active class event whose Row.boundary granularity boundaries are named at Row.declared in, Row.id creates one valid Row.interrupt class interrupt offered at a named boundary and Bind entry. Where the interrupt enters at a boundary of the active event, event order selects one valid interrupt, the active event advances only to permitted boundaries while it waits, and the interrupt passes through steps 6 to 11 before changing that event; where it joins the next instant instead, the active event runs to completion in this one. Then Bind result. A presentation skip returns to the interrupted boundary; where none is possible, that clause asserts nothing. The test names both addresses and restates nothing from them.

Given

an active Row.active class event whose Row.boundary granularity boundaries are named at Row.declared in, and a valid Row.interrupt class interrupt offered at one of them

When

• the valid interrupt is discovered, selected, and resolved

Then

• one interrupt event is created through the interrupt path and Bind entry
• where the interrupt enters at a boundary of the active event: when several interrupts are valid, event rank, the shared-rank order, and then within-class order select one; the active event advances only to boundaries Row.declared in permits while it waits; and the interrupt passes through presentation waiting, collision grouping, orphan checks, and its own boundaries before changing that event
• where the interrupt joins the next instant instead, the active event runs to completion in this one
• Bind result
• only one selected interrupt resolves at a time, and the report distinguishes replacement from an invalid offer
• where presentation skips the interrupt, control returns to the interrupted event's boundary rather than step 4; where no such skip is possible, this clause asserts nothing

Diagnostics

• Instance-interrupt-report
• Instance-event-trace
• Instance-cost-log

invalid-interrupt-does-not-enter

Applies when Interrupt entry is Before next effect or After current effect or At normal rank.

An interrupt of Row.interrupt class offered outside the validity window named at Row.declared in, or at a point that is not one of the Row.boundary granularity boundaries, creates no interrupt event. The active Row.active class event advances unchanged, and the interrupt report distinguishes the invalid offer from a valid interrupt that was not selected. Where the adoption cannot construct an invalid offer, this test asserts nothing.

Given

an interrupt of Row.interrupt class offered outside the validity window named at Row.declared in, or at a point that is not one of the Row.boundary granularity boundaries

When

• the interrupt offer is checked

Then

• no interrupt event is created
• the active Row.active class event advances unchanged
• the interrupt report distinguishes an invalid offer from a valid interrupt that was not selected
• where the adoption cannot construct an invalid offer, this test asserts nothing

Diagnostics

• Instance-interrupt-report
• Instance-event-trace

caused-event-follows-declared-route

Applies when Caused events is Resolves now or Waits for its place or Next instant.

Row.id creates one caused event of class Row.event class once; it Bind route, and no chain runs past the bound named at Row.declared in. The test names the address and restates nothing from it.

Given

an effect that causes Row.id due now under the finite chain rule at Row.declared in

When

• the causing effect commits and the caused event is admitted

Then

• one caused event of class Row.event class is created once and Bind route
• no chain runs past the bound named at Row.declared in
• the caused-event report distinguishes this accepted route from rejection and from an interrupt

Diagnostics

• Instance-caused-event-report
• Instance-event-trace
• Instance-waiting-set

active-event-finishes-and-loop-continues

Applies for every adoption

Finishing an active event applies any due deferred removal, records each selected consequence once, removes the event, and returns to step 4. The instant drains the waiting set and waits for any held cue; unavailable branches assert nothing.

Given

each active event, including a collision-group member where the adoption can construct one

When

• the active event finishes

Then

• any deferred target removal due at that point is applied and each selected consequence is recorded once
• the event is removed from the waiting set and selection returns to step 4
• the instant continues until the waiting set is empty, waiting for a cited cue when only presentation-held events remain
• where no deferred removal or held event exists, the corresponding clause asserts nothing

Diagnostics

• Instance-event-trace
• Instance-waiting-set
• Instance-collision-report

single-ending-records-after-waiting-set-empties

Applies for every adoption

After the waiting set is empty, a single ending that holds in final settled state is recorded once through the game's cited ending rule. Earlier ending-event resolution and class rank do not record or override it. If no single ending can hold, this test asserts nothing.

Given

each instant the adoption can construct whose final settled state makes one ending hold outside every declared terminal collision

When

• the waiting set becomes empty and step 15 runs

Then

• the game's cited ending rule records that ending once from final settled state
• no earlier ending-event resolution or class rank records or overrides it
• where no such single ending can hold, this test asserts nothing

Diagnostics

• Instance-waiting-set
• Instance-ending-record

terminal-collision-follows-precedence

Applies when Terminal precedence is Loss only or Win only or Both recorded.

When Row.win condition and Row.loss condition both hold in final settled state, Row.id Bind ending, regardless of rank or detection order. Row.declared in identifies the pair; the test names the address and restates nothing from it.

Given

an instant whose final settled state makes Row.win condition and Row.loss condition both hold under Row.declared in

When

• the waiting set becomes empty and step 15 reads the pair

Then

• the lifecycle Bind ending
• the result is unchanged by event rank or the order in which the two conditions were detected
• the ending record distinguishes this terminal collision from single-ending recording

Diagnostics

• Instance-ending-record
• Instance-settlement-report

instant-commits-state-and-next-waiting-set-together

Applies for every adoption

Step 16 commits final state and the next-instant waiting set together. No event from a closed instant can re-enter it. Where there is no next-instant event, that membership observation asserts nothing.

Given

an instant with distinguishable final state and next-instant waiting events where the adoption can construct them

When

• step 16 closes the instant

Then

• the final state and next-instant waiting set commit together
• no event from the closed instant later re-enters it
• where no next-instant event exists, its membership observation asserts nothing

Diagnostics

• Instance-instant-trace
• Instance-waiting-set

settlement-report-carries-lifecycle-fields

Applies for every adoption

Every settlement report carries the instant, event id, class, rank, tie-break when used, within-class order, source and target availability, applied effects, interrupt and replacement when present, caused-event destination, removal result, and terminal result when present. An unavailable optional circumstance asserts nothing.

Given

each event settled by Instance, with optional tie, interrupt, replacement, caused event, removal, and terminal result where present

When

• its settlement report is read

Then

• the report carries instant, event id, class, rank, tie-break when used, within-class order, source and target availability, effects applied, interrupt and replacement when present, caused-event destination, removal result, and terminal result when present
• an optional circumstance the adoption cannot construct asserts nothing

Diagnostics

• Instance-settlement-report

within-class-row-class-join

Applies for every adoption

This declaration check reads the adoption, not the running game. Row.class id must name exactly one event class in this adoption. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document, not the running game

When

• a reviewer compares Row.class id with event-classes ids

Then

• Row.class id names exactly one event-classes row in this adoption; any other shape is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

presentation-row-class-join

Applies for every adoption

This declaration check reads the adoption, not the running game. Row.event class must name exactly one event class in this adoption. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document, not the running game

When

• a reviewer compares Row.event class with event-classes ids

Then

• Row.event class names exactly one event-classes row in this adoption; any other shape is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

caused-row-class-join

Applies for every adoption

This declaration check reads the adoption, not the running game. Row.event class must name exactly one event class in this adoption. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document, not the running game

When

• a reviewer compares Row.event class with event-classes ids

Then

• Row.event class names exactly one event-classes row in this adoption; any other shape is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

orphan-row-class-join

Applies for every adoption

This declaration check reads the adoption, not the running game. Row.event class must name exactly one event class in this adoption. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document, not the running game

When

• a reviewer compares Row.event class with event-classes ids

Then

• Row.event class names exactly one event-classes row in this adoption; any other shape is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

interrupt-active-class-join

Applies for every adoption

This declaration check reads the adoption, not the running game. Row.active class must name exactly one event class in this adoption. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document, not the running game

When

• a reviewer compares Row.active class with event-classes ids

Then

• Row.active class names exactly one event-classes row in this adoption; any other shape is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

interrupt-class-join

Applies for every adoption

This declaration check reads the adoption, not the running game. Row.interrupt class must name exactly one event class in this adoption. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document, not the running game

When

• a reviewer compares Row.interrupt class with event-classes ids

Then

• Row.interrupt class names exactly one event-classes row in this adoption; any other shape is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

rank-tie-rows-match-shared-ranks

Applies for every adoption

This declaration check reads the adoption, not the running game. Shared ranks and rank-ties rows must match one-for-one. Each comma-separated class-ids string lists every and only event class at that rank; the class-ids description requires each id to be listed once. Any other shape is a defect this test fails by construction; with no shared rank and no row, the check asserts nothing.

Given

the Instance adoption document, not the running game

When

• a reviewer groups event-classes rows by rank and compares the groups with rank-ties rows

Then

• every rank shared by two or more event classes has exactly one rank-ties row, and every rank-ties row names a rank shared by at least two event classes
• each rank-ties class-ids string lists every and only event-classes id at that rank; the class-ids description requires each id to be listed once
• any other shape is a defect this test fails by construction; when no rank is shared and no rank-ties row exists, this check asserts nothing

Diagnostics

• Instance-declaration-record

tied-classes-have-no-within-class-row

Applies for every adoption

This declaration check reads the adoption, not the running game. A class already ordered by a rank-ties row must have no within-class-rules row. An inert class row is a defect this test fails by construction; with no rank tie, the check asserts nothing.

Given

the Instance adoption document, not the running game

When

• a reviewer compares every class named by rank-ties with within-class-rules class-id fields

Then

• no event class named by a rank-ties row has a within-class-rules row
• a matching class row is inert and is a defect this test fails by construction; with no rank tie, this check asserts nothing

Diagnostics

• Instance-declaration-record

same-target-kinds-do-not-overlap

Applies for every adoption

This declaration check reads the adoption, not the running game. same-target-cases and same-target-exceptions must not name the same target kind. An overlap is a defect this test fails by construction; with either set empty, the comparison asserts nothing.

Given

the Instance adoption document, not the running game

When

• a reviewer compares target-kind across same-target-cases and same-target-exceptions

Then

• no target kind is named in both row sets
• any overlap is a defect this test fails by construction; when either set is empty, the cross-set comparison asserts nothing

Diagnostics

• Instance-declaration-record

only-first-needs-visible-order

Applies for every adoption

This declaration check reads the adoption, not the running game. Every event class that can supply two events to a collision resolved by only-first-resolves, through the general answer or a same-target-exceptions row, must have a visible class-row, rank-tie, or general order. A no-visible-order path or any other shape is a defect this test fails by construction; where no target kind uses only-first-resolves, the check asserts nothing. The only-first-resolves semantics supplies this duty.

Given

the Instance adoption document, not the running game

When

• a reviewer finds every event class that can supply two events to a collision resolved by only-first-resolves through the general answer or a same-target-exceptions row

Then

• every such class has a visible order: a within-class-rules row whose order is not no-visible-order, a rank-ties row whose tie-break is not no-visible-order, or a general within-class-order answer other than no-visible-order
• any other shape is a defect this test fails by construction; where no target kind is resolved by only-first-resolves, this check asserts nothing

Diagnostics

• Instance-declaration-record

same-target-exception-differs-from-general

Applies when Two events one target is Only first resolves or All resolve one ending or All resolve each ending.

This declaration check reads the adoption, not the running game. No same-target-exceptions row may repeat the general two-events-one-target answer. An inert exception is a defect this test fails by construction; with no exception row, the check asserts nothing. The same-target-exceptions description supplies this duty.

Given

the Instance adoption document, not the running game

When

• a reviewer compares every same-target-exceptions resolution with the general two-events-one-target answer

Then

• no same-target-exceptions row names the same resolution as the general answer
• an inert exception is a defect this test fails by construction; with no exception row, this check asserts nothing

Diagnostics

• Instance-declaration-record

stable-index-second-index-duty

Applies for every adoption

This declaration check reads the adoption and its Fixed event rules, not the running game. Every stable-index class row or rank tie must name a second index or belong to a class or tied group that cannot produce equal first numbers that change the result. Any other shape is a defect this test fails by construction; with no stable-index row, the check asserts nothing.

Given

the Instance adoption document and its Fixed event rules, not the running game

When

• a reviewer checks every within-class-rules row and every rank-ties row using stable-index

Then

• every such row either names a second index or belongs to a class or tied group that cannot produce equal first numbers that change the result
• any other shape is a defect this test fails by construction; with no stable-index row, this check asserts nothing

Diagnostics

• Instance-declaration-record

visible-tie-needs-class-row

Applies for every adoption

This declaration check reads the adoption and its Fixed event rules, not the running game. A class that can have a visible tie outside a rank tie must have a within-class-rules row when the general answer is stable-index, map-reading-order, clockwise, or declared-random. Any other shape is a defect this test fails by construction; for arrival-order or no-visible-order, or with no such class, the check asserts nothing.

Given

the Instance adoption document and the event classes its Fixed rules can tie visibly, not the running game

When

• a reviewer compares each such class outside a rank tie with within-class-rules and the general within-class-order answer

Then

• every class that can have a visible tie and is not in a rank tie has a within-class-rules row when the general answer needs named data: stable-index, map-reading-order, clockwise, or declared-random
• any other shape is a defect this test fails by construction; where the general answer is arrival-order or no-visible-order, or no such class exists, this check asserts nothing

Diagnostics

• Instance-declaration-record

rejection-default-citations-have-rows

Applies when Rejected action effect is Derate or Clock advances or Cost and clock.

This declaration check reads the adoption, not the running game. Every rejecting case under this default must have a rejection-cases row carrying Bind duty. A missing row or citation is a defect this test fails by construction; if no rejecting case exists, the check asserts nothing.

Given

the Instance adoption document and every proposal case that can take the selected default, not the running game

When

• a reviewer compares those cases with rejection-cases rows

Then

• every case that can take the selected default has a rejection-cases row carrying Bind duty
• a missing row or citation is a defect this test fails by construction; where no rejecting case exists, this check asserts nothing

Diagnostics

• Instance-declaration-record

event-class-list-is-complete

Applies for every adoption

This declaration check reads the adoption and its Fixed event rules, not the running game. event-classes must cover every event due at an instant exactly once, must name event classes rather than simulation stages, and must invert authored numbers once when the game's source convention is higher-first. An omission, category error, or runtime reversal is a defect this test fails by construction.

Given

the Instance adoption and its Fixed event rules, not the running game

When

• a reviewer compares every event due at an instant with event-classes

Then

• every event due at an instant belongs to exactly one event-classes row
• a game whose source convention is higher-first has inverted its authored numbers once in event-classes rather than reversing them at runtime
• an omitted event class or a list of simulation stages presented as classes is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

event-class-citation-states-membership

Applies for every adoption

This declaration check reads the adoption and Row.declared in, not the running game. The citation must name Row.id, labelled Row.label in the game's own words, and the events belonging to it. Another meaning is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.declared in, not the running game

When

• a reviewer checks the citation's meaning

Then

• Row.declared in names Row.id, labelled Row.label in the game's own words, and the events belonging to it
• another meaning is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

within-class-grid-citation-duty

Applies when row order is Map reading order or Clockwise.

This declaration check reads the adoption and Row.grid declared in, not the running game. The citation must supply the order frame selected by Row.id. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.grid declared in, not the running game

When

• a reviewer checks the cited Grid and direction rule

Then

• the citation supplies the row's required first row and first column, or centre, first direction, and clockwise sense
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

within-class-rule-citation-duty

Applies when row order is Declared random or Game rule.

This declaration check reads the adoption and Row.rule declared in, not the running game. The citation must supply one complete total-order rule and never point back to this row. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.rule declared in, not the running game

When

• a reviewer checks the cited random or custom order rule

Then

• the citation supplies the complete draw or deterministic rule that produces one total order for the instant and never points back to this row
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

rank-tie-grid-citation-duty

Applies when row tie break is Map reading order or Clockwise.

This declaration check reads the adoption and Row.grid declared in, not the running game. The citation must supply the order frame selected by Row.id. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.grid declared in, not the running game

When

• a reviewer checks the cited Grid and direction rule

Then

• the citation supplies the row's required first row and first column, or centre, first direction, and clockwise sense
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

rank-tie-rule-citation-duty

Applies when row tie break is Declared random or Game rule.

This declaration check reads the adoption and Row.rule declared in, not the running game. The citation must supply one complete total-order rule and never point back to this row. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.rule declared in, not the running game

When

• a reviewer checks the cited random or custom order rule

Then

• the citation supplies the complete draw or deterministic rule that produces one total order for the instant and never points back to this row
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

rejection-scale-citation-duty

Applies when row result is Derate.

This declaration check reads the adoption and Row.scale rule declared in, not the running game. The citation must scale the complete effect and cost. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.scale rule declared in, not the running game

When

• a reviewer checks the cited scale rule

Then

• the citation supplies how the complete effect and cost are scaled
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

rejection-clock-citation-duty

Applies when row result is Clock advances or Cost and clock.

This declaration check reads the adoption and Row.clock rule declared in, not the running game. The citation must name exactly one advance caused by this rejection. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.clock rule declared in, not the running game

When

• a reviewer checks the cited clock or turn rule

Then

• the citation names exactly one clock advance caused by this rejection
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

presentation-cue-citation-duty

Applies for every adoption

This declaration check reads the adoption and Row.declared in, not the running game. The citation must relate the game timing of Row.event class to Row.presentation cue and show that the cue finishes in finite game or real time, keeping an instant from waiting forever. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.declared in, not the running game

When

• a reviewer checks the cited presentation rule

Then

• Row.declared in relates the game timing of Row.event class to Row.presentation cue and shows the cue finishes in finite game or real time, which is what keeps an instant from waiting forever
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

caused-event-citation-duty

Applies for every adoption

This declaration check reads the adoption and Row.declared in, not the running game. The citation must name the cause, the new Row.event class event, and the finite bound on repeated caused events. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.declared in, not the running game

When

• a reviewer checks the cited caused-event rule

Then

• Row.declared in names the cause, the new Row.event class event, and the finite bound on repeated caused events
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

interrupt-citation-duty

Applies for every adoption

This declaration check reads the adoption and Row.declared in, not the running game. The citation must name the validity window, the Row.boundary granularity effect boundaries, and the stop result. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.declared in, not the running game

When

• a reviewer checks the cited interrupt rule

Then

• Row.declared in names the validity window, the Row.boundary granularity effect boundaries, and the stop result
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

interrupt-replacement-citation-duty

Applies when row result is Replace remaining effects.

This declaration check reads the adoption and Row.replacement declared in, not the running game. The citation must state every replacement effect and its order. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.replacement declared in, not the running game

When

• a reviewer checks the cited replacement rule

Then

• Row.replacement declared in states every replacement effect and its order
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

orphan-case-citation-duty

Applies for every adoption

This declaration check reads the adoption and Row.declared in, not the running game. The citation must identify the case, when it applies, the captured payload, and the source or target requirement. A missing duty is a defect this test fails by construction. The test names the address and restates nothing from it.

Given

the Instance adoption and the prose at Row.declared in, not the running game

When

• a reviewer checks the cited orphan rule

Then

• Row.declared in identifies the case, when it applies, the captured payload, and the source or target requirement
• a missing duty is a defect this test fails by construction

Diagnostics

• Instance-declaration-record

resolution-holds

Applies for every adoption

Across Inputs scope, lower eligible ranks never resolve late, each tie and within-class order holds, each proposal follows its case or default, each accepted proposal creates one payload, each valid interrupt takes effect at its entry point, each caused event follows its route, each orphan follows its row, and each ending records once at step 15. An instant shared with another adoption asserts nothing here. A case the adoption cannot construct asserts nothing.

Holds

for every instant of the audited run that this adoption owns in full, every event resolved at or after every eligible lower-rank event; every rank tie and within-class selection followed its declared order; every rejection followed its matching case or default; every accepted proposal created one payload once; every valid interrupt entered at its declared point and took effect; every caused event was created once and followed its route; every orphan followed its row; every ending was recorded once at step 15; an instant shared with another adoption asserts nothing here; a case the adoption cannot construct asserts nothing

Seeds

Inputs seeds

Scope

Inputs scope

Diagnostics

• Instance-instant-trace
• Instance-proposal-log
• Instance-order-trace
• Instance-collision-report
• Instance-orphan-report
• Instance-interrupt-report
• Instance-ending-record
• Instance-settlement-report
• Instance-first-ordering-violation