Determinism & replay

Suspension and catch-up

suspension-and-catch-up-1

Tests included

This contract defines the behaviour of progress while the game is closed: an energy refill, a crop timer, or a daily reward.

It decides what your energy refill or crop timer does while the game is closed, and what the player sees on return.

Use in your game

Opens the authoring tool with this contract added and its questions unanswered. Or download the ZIP and add it later.

What is in the ZIP

The ZIP holds the contract and its acceptance tests. In the authoring tool, choose Add contract and pick this ZIP. If you keep your design as files, put them in contracts/ and fill in the answers there.

Questions

Up to 6 questions. Some appear only after earlier answers.

  1. What happens while the game stays open in the background?
  2. What appears before ordinary play resumes?
  3. Can the player change the clock that measures time away?
  4. If the player moves the device clock backward, which state does the game keep?
  5. Does the game explain the backward clock result?
  6. Several calendar boundaries passed while the game was away. Which ones count on return?

Try the answers

Pick answers to see which rules and tests apply. Nothing is saved here: the ZIP and the authoring tool start unanswered.

What happens while the game stays open in the background?

Choices for What happens while the game stays open in the background?
Background time uses the same suspension rules as closed time. Ten minutes in another tab refills energy like ten minutes with the game closed.

The lifecycle treats the background interval as a suspension interval. Ordinary updates do not also apply that interval.

Ordinary play continues in the background. A browser farm keeps growing crops while the player uses another tab.

The ordinary update path continues, including platform throttling. Foregrounding adds no catch-up for the same interval.

The open game stays still, and away progress starts only after closing. A crop timer pauses in the app switcher but advances after the app closes.

The open-background interval receives neither ordinary updates nor catch-up.

Why this is asked

An open game may use away handling, keep playing, or stay still until it closes. The same time must never count twice.

What appears before ordinary play resumes?

Choices for What appears before ordinary play resumes?
No separate return surface appears. A match-3 game simply shows that three lives are ready.

The lifecycle adds no player-facing return surface. Existing game displays may show the settled state after ordinary play resumes. Developer or diagnostic instrumentation that is not player-facing is out of scope.

Existing displays show the change before play resumes. A life counter ticks from two lives to five on the map screen.

At least one existing player-facing display presents the affected state during return settlement.

A return surface names each result. An idle game shows energy gained and coins waiting for collection.

A player-facing return surface identifies each affected row and its settled result.

A return surface also explains the calculation. A factory screen shows six hours away, its energy ceiling, and the final gain.

The return surface reports elapsed time, applicable limits, amount rules, fidelity, and settled results.

Why this is asked

Changed state may speak for itself, animate before play, or appear in a return summary.

Can the player change the clock that measures time away?

Asked when
the clock list has at least one row.
If not asked
No clock row exists, so this adoption measures no elapsed suspension time.
Choices for Can the player change the clock that measures time away?
The game reads a clock from the device. Moving a phone clock forward by two hours gives an idle mine two more measured hours.

The elapsed interval comes from a clock the player can change through device settings. Both backward-clock questions are asked.

The game reads a clock outside device settings. Changing a phone clock does not refill a match-3 life sooner.

The elapsed interval comes from a clock the player cannot change through device settings. The backward-clock questions are not asked.

Why this is asked

The player can move a device clock through settings. A protected clock stays outside those settings, though the service behind it can correct it.

If the player moves the device clock backward, which state does the game keep?

Asked when
Clock source is Device clock.
If not asked
No device clock is read, either because no clock row exists or because the clock is protected, so no rollback anchor is selected. A protected-clock resync may still move its reading backward; the lifecycle then keeps the loaded state.
Choices for If the player moves the device clock backward, which state does the game keep?
The game returns to the state captured when suspension began. An idle mine returns to the ore count recorded when the app closed.

Every in-scope local item is restored from the suspension snapshot. Elapsed time for this interval is zero.

The game returns to the latest state accepted by a trusted rule. An online workshop returns to its last server-confirmed stock count.

The one rollback rule supplies a trusted state and matching clock reading. The current suspension interval contributes zero elapsed time.

The game keeps the state loaded at return but adds no away change. A newer cloud save from another device keeps its crops.

No state is restored by this contract. The loaded return state remains, and elapsed time for this interval is zero. That state may be newer than the suspension snapshot because of a cloud save, a second device, or a mid-session autosave.

Why this is asked

Zero elapsed time does not say which saved state survives a backward clock. The anchor prevents duplicate or reversed gains.

Does the game explain the backward clock result?

Asked when
Clock source is Device clock.
If not asked
No device clock is read, either because no clock row exists or because the clock is protected, so no player-caused clock-change notice is selected. A protected-clock resync may still produce zero elapsed time.
Choices for Does the game explain the backward clock result?
The game adds no clock-change notice. A life refill stays unchanged without a pop-up.

The lifecycle adds no player-facing explanation for the backward-clock branch.

The game explains that the clock change blocked away time. An idle game shows a short clock-change message beside unchanged energy.

The lifecycle presents a player-facing clock-change explanation after the anchor is applied and before ordinary play resumes.

Why this is asked

The same backward-clock outcome can be silent or visible to the player.

Several calendar boundaries passed while the game was away. Which ones count on return?

Asked when
the calendar boundaries list has at least one row.
If not asked
No calendar boundary is tracked, so return settlement creates no calendar crossing.
Choices for Several calendar boundaries passed while the game was away. Which ones count on return?
Every crossed boundary settles in time order. A farm processes Friday, Saturday, and Sunday crop resets separately.

The lifecycle inserts every crossed boundary into the return timeline in ascending time order.

Only the latest crossed boundary settles. A daily reward calendar opens on today's entry without granting missed days.

The lifecycle inserts only the latest crossed boundary for each calendar row and omits earlier crossings.

All crossings become one return event. A weekly shop refreshes once and receives the number of missed weeks.

The lifecycle inserts one return-time event per calendar row, carrying that row's number and span of crossed boundaries.

Why this is asked

A daily or weekly rule may run for every crossing, only the latest one, or one combined return event.

Lists8 lists

Some settings are lists of rows.

A reference points to a number or a rule in your design. For a number, use its address in your tuning. For a rule, use its file and heading, such as 02-mechanics.md#recovery. Each field's description says what it needs.

Clock

clock

The elapsed-time rule for this behaviour family. At most one row is valid.

An empty list means: No elapsed suspension time is measured by this adoption.

Each row is: id, clock-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required A stable name for the elapsed clock, such as away-clock.
clock-declared-in reference Required The game rule naming the reading, its unit, and when it is sampled.

Fixed items

fixed-items

State that remains at its suspension anchor until ordinary play resumes.

An empty list means: No covered state is fixed by suspension.

Each row is: id, state-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required The state item in game language, such as round-score or player-position.
state-declared-in reference Required The game rule that identifies the complete state held fixed.

Catch up items

catch-up-items

State calculated from elapsed time when the suspension interval returns.

An empty list means: No covered state is calculated from missed time on return.

Each row is: id, state-declared-in, away-amount, amount-rule-declared-in, catch-up-fidelity, fidelity-rule-declared-in, away-limit, limit-rule-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required The state item in game language, such as energy, crops, or lives.
state-declared-in reference Required The game rule identifying the state, its ordinary changes, and its unit.
away-amount choice: same-as-playing, reduced, away-rule Required The amount earned from equal elapsed time: the ordinary amount, a lower amount, or an amount from a separate away rule. An energy refill may keep its normal one point per minute.
amount-rule-declared-in reference Present when row away amount is Reduced or Away rule. The rule for the lower or separate away amount. It states the complete amount calculation and its unit. Only the cited rule binds this row; uncited game prose does not.
catch-up-fidelity choice: every-missed-update, larger-steps, one-derived-change Required How missed play changes this state between calendar events: every missed update, larger catch-up steps, or one derived change. A crop may replay every growth tick while a life refill may derive one total.
fidelity-rule-declared-in reference Present when row catch up fidelity is Larger steps or One derived change. The rule naming step size and order, or the rule deriving the single return change. It distributes the promised amount and does not change it. Only the cited rule binds this row; uncited game prose does not.
away-limit choice: whole-interval, time-limit, less-after-a-point, state-ceiling Required How much time or gain is allowed away: all time, a hard time stop, a lower amount past a point, or a state ceiling. A normal full-energy maximum is a valid state ceiling. A maximum that limits away gain is declared here as a state ceiling, not left under whole-interval.
limit-rule-declared-in reference Present when row away limit is Time limit or Less after a point or State ceiling. The time point, later amount rule, or state ceiling. A state ceiling may be the same maximum that applies during ordinary play. Only the cited rule binds this row; uncited game prose does not.

Continuous items

continuous-items

State that continued under another authority while the local game was suspended.

An empty list means: No covered state continued elsewhere during suspension.

Each row is: id, state-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required The state item in game language, such as skill-training or life-service.
state-declared-in reference Required The external or protected rule that continued the state and supplies its return reading.

Choice items

choice-items

State whose away behaviour is selected by a setting, platform, unlock, or other game rule.

An empty list means: No covered state selects between away behaviours at runtime.

Each row is: id, choice-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required The state item in game language, such as harvest-mode.
choice-declared-in reference Required The game rule naming both possible behaviours, their complete data, the condition selecting one, and the time at which the selection is made.

Return rewards

return-rewards

Rewards created by catch-up or a crossed calendar boundary, then delivered or left for the player to claim.

An empty list means: Return settlement creates no separately delivered reward.

Each row is: id, reward-declared-in, destination-declared-in, delivery, claim-declared-in, expires-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required The reward in game language, such as offline-coins or daily-gift.
reward-declared-in reference Required The game rule deriving the reward and identifying its source settlement.
destination-declared-in reference Required The destination rule that accepts the complete reward or leaves it pending.
delivery choice: automatic, player-claims Required Whether this reward enters its destination automatically or waits on a return surface for the player to claim it. A player-claims reward requires a return-display answer that supplies a return surface: return-summary or detailed-return-summary.
claim-declared-in reference Present when row delivery is Player claims. The player event that claims this pending reward from the return surface.
expires-declared-in reference Optional The optional rule naming when an unclaimed reward expires and is removed. Omission means an unclaimed reward never expires.

Calendar boundaries

calendar-boundaries

Daily, weekly, seasonal, or other calendar boundaries that may pass during suspension.

An empty list means: Return settlement creates no calendar crossing.

Each row is: id, boundary-declared-in, settlement-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required The boundary in game language, such as daily-reset or new-week.
boundary-declared-in reference Required The rule naming the calendar, time zone, boundary test, exact crossing time, and what happens when local civil time skips or repeats a boundary.
settlement-declared-in reference Required The game rule that receives each selected crossing and states its immediate effects.

Rollback rules

rollback-rules

The trusted checkpoint rule used by the backward-clock checkpoint answer. Exactly one row under last-trusted-checkpoint; no row under any other anchor, a protected clock, or no clock.

An empty list means: No trusted checkpoint is used as a backward-clock anchor.

Each row is: id, trusted-state-declared-in.

Every field
FieldKindWhen it appearsMeaning
id string Required A stable name for the trusted checkpoint rule.
trusted-state-declared-in reference Required The rule that supplies one coherent state snapshot and its matching trusted clock reading.

For builders

Exact mechanism wording and 80 pack tests

Exact mechanism wording

This is the one normative authority for suspension state, elapsed time, catch-up, calendar crossings, return rewards, and report order. Questions and rows supply choices and game rules to this lifecycle; they do not define a second sequence.

A suspension interval begins at game closure, or at the earlier open-background transition selected by counts-as-away, and ends at return processing, at the return clock reading when a clock row exists. A suspension snapshot contains every in-scope local item and the starting clock reading. A return timeline is the ordered elapsed span, split at the calendar crossings selected by the calendar answer. A pending reward has been created but not accepted by its destination.

An unclaimed reward with an expiry rule is removed at its cited deadline. The lifecycle checks that deadline at return and immediately before a claim.

### Suspend

1. Closing the game always begins a suspension interval. Route an earlier open-background transition through while-in-the-background. counts-as-away begins the interval at that transition. keeps-playing continues ordinary play and creates no return catch-up for background time. waits-until-closed holds state unchanged until closure begins the interval. 2. When an interval begins, capture one coherent suspension snapshot before any covered state can change. If a clock row exists, read its starting value in the same batch; the interval's starting value is the higher of that reading and the committed anchor from the previous return, so time below the anchor is never replayed. A protected authority may keep changing a continuous-items row after the snapshot. 3. Hold every fixed and catch-up item at its snapshot state. A choice row resolves its cited selection at the time named by that rule. A selected continuous branch stays under its cited authority; other selected branches follow their matching lifecycle paths.

### While away

4. Local catch-up items do not advance visibly while ordinary updates are stopped. The interval records clock reach only; settlement waits for return. 5. Continuous items keep changing under their cited authority. This lifecycle neither predicts those changes nor duplicates them locally. 6. Calendar crossings are discovered from the cited calendar and clock. They are not settled yet. Return processing selects and orders them.

### Return

7. If a clock row exists, read the return clock once. A non-negative interval uses the suspension snapshot and the elapsed difference. Any negative protected-clock interval counts as zero elapsed with the loaded state retained, because a service resync can move even a protected clock back; skip steps 9–11 and continue at step 12. That skipped interval creates no return reward. Without a clock row, local catch-up and calendar crossings are absent; continue with the unchanged fixed state at step 12. 8. If a device clock reads earlier, apply backward-clock-anchor before any catch-up. Restore the suspension snapshot, restore the cited trusted checkpoint, or keep the loaded return state. The current interval then has zero elapsed time. A skipped interval creates no return reward. Apply the selected clock notice, skip steps 9–11, and continue at step 12. 9. Build one calendar return timeline and one pass timeline for each catch-up row. A calendar row admits the full non-negative measured interval because it declares no away limit. For a catch-up row, this lifecycle derives the admitted span from the row's declared limit for crossing selection only; that derivation is not the limit application step 10 assigns, and a state-dependent ceiling discovers its endpoint during the chronological pass. Crossings inside that admitted span settle against the row, and crossings beyond it do not. A state-dependent ceiling discovers its endpoint during the chronological pass, so no later crossing enters that row's pass. A catch-up row's limit does not cancel an independent calendar event: the row shape declares no such link, and the event settles once on the calendar timeline. every-crossing-in-order keeps all remaining crossings in ascending time order. latest-crossing-only keeps the last remaining crossing for each calendar row. one-combined-crossing creates one return-time event per calendar row with its count and span. Row order breaks a tie between equal timestamps before Event resolution receives them. 10. Compute each catch-up row's segments as step 11 hands them over, keeping amount separate from fidelity; step 11 owns the ordering. same-as-playing defines the ordinary amount for equal elapsed time; reduced and away-rule use only their cited amount rule. Under every-missed-update, this lifecycle applies the away limit as a per-segment clip and then feeds only the remaining missed updates to the game rules. Under larger-steps, the cited fidelity rule receives the amount and limit, owns both the larger-step distribution and the limit, and returns the ordered changes. Under one-derived-change, the cited fidelity rule receives the amount and limit, owns the limit, and returns one change. The lifecycle does not re-apply a limit owned by a cited fidelity rule. When away-rule and one-derived-change compose, the amount rule defines the total and the fidelity rule distributes it. 11. Settle each selected calendar event once through settlement-declared-in. For every catch-up row containing that crossing, settle the preceding segment first, then the event's immediate effect, then the following segment. The row's clip already excluded later crossings, so this order cannot re-admit time or events beyond its limit. Reports keep the same segment-then-event-then-segment order. 12. Check every existing pending reward's cited deadline at return. An expired unclaimed reward is removed at that deadline. A pending reward is in-scope local state and survives this and later suspensions until the player claims it or its cited deadline expires. 13. Read every continuous item once. Apply each selected choice branch once. Create each return reward from its cited source settlement; a reward row with no settled source produces nothing. A skipped interval therefore creates no return reward. Check a new reward's cited deadline at return. Offer an automatic reward to its destination in reward-row order. A player-claims reward remains pending until its cited claim event. Destination refusal keeps the same pending reward, and a refused automatic reward is offered again at each later return until its destination accepts it or its cited deadline removes it. 14. Present return-display after settled state and pending rewards are known. A clock explanation precedes the general return surface. Existing displays used by visible-before-resume update before ordinary play. A claim event checks the cited deadline before offering its reward. An expired unclaimed reward is removed; each accepted reward is reported once. 15. Commit the final local state and the next suspension anchor together. On every return the committed anchor is never lower than the previous one. After any backward-clock return, commit the highest of the suspension reading, the return reading, and any trusted-checkpoint reading as the next suspension anchor, retaining the trusted state under that anchor, so repeated clock rollback cannot replay time below the prior anchor. Resume ordinary updates only after all automatic return changes and every required pre-resume display have settled. A later player claim is a new event and never repeats catch-up.

Every catch-up report carries the interval start and end readings, elapsed time admitted, row id, amount branch, fidelity branch, limit reached, before state, after state, and calendar crossing that split the segment when present. A backward-clock report also carries the selected anchor when one was selected, and whether a notice appeared when the notice question applies. A return-reward report carries its source, destination, delivery, pending, accepted, or expired status, deadline when present, and claim event when present.

Verification pack

sha256:d1ec8edb7c86cda9f923cacba4a1d4a0c6c4af5ee4302842865d39636cd8a81d

The format calls an adoption with its matching pack Checked: the tests travel with it, but a game has not necessarily passed them. Without the pack the adoption is Promised: the builder still owes the chosen behavior.

80 pack tests

Placeholders are filled from the adoption's answers, values, rows, and verification inputs.

a suspension interval has one beginning and one return

suspension-interval-boundaries

scenarioonce

Applies for every adoption

A suspension interval begins once, Bind interval start, and ends once at return processing, at the return clock reading where a clock row exists. The interval contains no time outside those boundaries.

Given

a covered close-and-return cycle after the selected background handling

When
  • the lifecycle records the interval boundaries
Then
  • the suspension interval begins once, Bind interval start, and ends once at return processing, at the return clock reading where a clock row exists
  • no time before its beginning or after its end enters that interval
Diagnostics
  • Instance-suspension-interval
the suspension snapshot is one coherent starting state

suspension-snapshot-vocabulary

scenarioonce

Applies for every adoption

The suspension snapshot is one coherent starting state for every in-scope local item. Where this adoption has a clock row, the starting reading is captured in the same batch; without one, that clause asserts nothing.

Given

distinguishable values for every in-scope local item when a suspension interval begins

When
  • the suspension snapshot is captured
Then
  • the snapshot contains the same-instant starting value of every in-scope local item
  • where a clock row exists, its starting reading belongs to the same snapshot batch; without a clock row, the reading clause asserts nothing
Diagnostics
  • Instance-suspension-snapshot
Row.id stays pending until acceptance or expiry

pending-reward-vocabulary-and-expiry

scenarioper return-rewards row

Applies for every adoption

A created Row.id reward is pending until its destination accepts it. Without an expiry rule, an unclaimed reward never expires.

Given

a created Row.id reward that its destination has not accepted

When
  • Bind returns
Then
  • the reward is pending while it has been created but not accepted
  • without an expiry rule, an unclaimed reward never expires
Diagnostics
  • Instance-reward-report
Row.id is removed when its cited deadline expires

expiry-deadline-enforced

scenarioper return-rewards row

Applies for every adoption

An unclaimed Row.id reward is removed at the deadline named at Bind expiry address, checked at return and immediately before its claim event. The expired reward is reported once as expired, and a claim after the deadline delivers nothing.

Given

an unclaimed Row.id reward before, at, and after the deadline named at Bind expiry address

When
  • the deadline is checked at return and immediately before its claim event
Then
  • the unclaimed reward is removed at that deadline
  • the expired reward is reported once as expired
  • a claim after the deadline delivers nothing
Diagnostics
  • Instance-reward-report
  • Instance-return-display-trace
background time begins the suspension interval

background-counts-as-away

scenarioonce

Applies when While in the background is Counts as away.

The background transition begins the suspension interval. Ordinary updates do not also apply that interval, so the same time is counted once.

Given

the game open with distinguishable covered state before it enters the background

When
  • the background transition occurs and the game later returns
Then
  • the suspension interval begins at the background transition
  • ordinary updates do not also apply any time in that interval
Diagnostics
  • Instance-suspension-interval
  • Instance-return-timeline
background time stays on the ordinary update path

background-keeps-playing

scenarioonce

Applies when While in the background is Keeps playing.

Ordinary updates continue in the background, including platform throttling. Foregrounding adds no catch-up for that same interval.

Given

the game open in the background with observable ordinary updates

When
  • a background interval passes under the platform's actual update schedule and the game returns to the foreground
Then
  • ordinary updates continue, including any platform throttling
  • foregrounding adds no catch-up for the same interval
Diagnostics
  • Instance-background-update-trace
  • Instance-return-timeline
background state waits until closure

background-waits-until-closed

scenarioonce

Applies when While in the background is Waits until closed.

The open-background interval receives neither ordinary updates nor catch-up. Covered state stays unchanged until closure begins the suspension interval.

Given

the game open in the background with distinguishable covered state

When
  • a background interval passes, the game returns to the foreground, and a later closure occurs
Then
  • the open-background interval receives neither ordinary updates nor catch-up
  • the covered state stays unchanged until closure begins the suspension interval
Diagnostics
  • Instance-background-update-trace
  • Instance-suspension-snapshot
closure begins an interval and captures one snapshot

closure-captures-one-snapshot

scenarioonce

Applies for every adoption

Closing always begins a suspension interval. One coherent suspension snapshot is captured before covered local state can change, and the same time never follows two paths.

Given

a game closure with distinguishable covered state

When
  • closure begins a suspension interval
Then
  • one coherent suspension snapshot is captured before any covered local state can change
  • the same time is never applied by two lifecycle paths
Diagnostics
  • Instance-suspension-snapshot
  • Instance-suspension-interval
Row.id starts at the higher available reading

clock-starting-reading

scenarioper clock row

Applies for every adoption

Row.id is read in the suspension snapshot batch from Row.clock declared in. The interval starts at the higher of that reading and the committed anchor, so time below the anchor is never replayed.

Given

a committed anchor and a starting reading supplied by Row.clock declared in

When
  • the suspension snapshot and starting reading are captured in one batch
Then
  • the interval starts from the higher of the sampled reading and the committed anchor
  • time below the committed anchor is never replayed
Diagnostics
  • Instance-clock-readings
  • Instance-suspension-snapshot
Row.id stays at its suspension snapshot state

fixed-item-held-at-snapshot

scenarioper fixed-items row

Applies for every adoption

Row.id remains at the complete state named by Row.state declared in from the suspension snapshot until ordinary play resumes.

Given

Row.id at a distinguishable state when suspension begins

When
  • the game is away and then completes return processing
Then
  • Row.id remains at its suspension snapshot state until ordinary play resumes
Diagnostics
  • Instance-suspension-snapshot
  • Instance-fixed-state-trace
Row.id waits at its suspension snapshot state

catch-up-item-held-at-snapshot

scenarioper catch-up-items row

Applies for every adoption

Row.id remains at its suspension snapshot state while away. Local catch-up does not appear before return settlement.

Given

Row.id at a distinguishable state when suspension begins

When
  • the suspension interval is still away
Then
  • Row.id remains at its suspension snapshot state and shows no local catch-up advance
Diagnostics
  • Instance-suspension-snapshot
  • Instance-catch-up-trace
Row.id resolves its cited selection

choice-item-resolves-selection

scenarioper choice-items row

Applies for every adoption

Row.id resolves the selection at the time named by Row.choice declared in, and the selected branch follows its matching lifecycle path. This test asserts nothing about branch data beyond what the citation is required to name.

Given

each selection condition named at Row.choice declared in in otherwise matching runs

When
  • the cited rule reaches its named selection time
Then
  • the selected branch follows its matching lifecycle path
  • the test asserts nothing about the branch's data beyond what Row.choice declared in is required to name
Diagnostics
  • Instance-choice-trace
  • Instance-return-timeline
Row.id stays under its cited authority

continuous-item-stays-with-authority

scenarioper continuous-items row

Applies for every adoption

Row.id remains under the authority at Row.state declared in after the snapshot. Its return reading comes from that authority, not from a local prediction.

Given

Row.id with distinguishable local snapshot and authority readings

When
  • the cited authority changes the item after suspension begins
Then
  • the return reading comes from the authority named at Row.state declared in rather than a local prediction
Diagnostics
  • Instance-continuous-state-trace
Row.id records reach and settles only on return

catch-up-waits-for-return

scenarioper catch-up-items row

Applies for every adoption

While ordinary updates are stopped, Row.id shows no visible local advance. The interval records reach only, and settlement waits for return.

Given

ordinary updates stopped with Row.id at its suspension snapshot state

When
  • the suspension interval advances and then return processing begins
Then
  • the away interval records clock reach only and shows no visible local advance
  • Row.id begins settlement only during return processing
Diagnostics
  • Instance-clock-readings
  • Instance-catch-up-trace
Row.id is neither predicted nor duplicated locally

continuous-item-is-not-predicted

scenarioper continuous-items row

Applies for every adoption

The cited authority continues Row.id. This lifecycle neither predicts that change nor duplicates it locally.

Given

an authority-side change to Row.id during suspension

When
  • local processing observes the away interval and later returns
Then
  • local processing neither predicts the authority's change nor applies a duplicate change
Diagnostics
  • Instance-continuous-state-trace
Row.id crossings are discovered before settlement

calendar-crossings-wait-for-return

scenarioper calendar-boundaries row

Applies for every adoption

Crossings for Row.id are discovered from Row.boundary declared in and the clock. They do not settle until return processing selects and orders them.

Given

a non-negative suspension interval that crosses Row.id

When
  • the clock reaches each crossing named by Row.boundary declared in and return has not begun
Then
  • the crossings are discovered from the cited calendar and clock
  • none settles before return processing selects and orders it
Diagnostics
  • Instance-calendar-report
  • Instance-return-timeline
the no-clock return path continues from fixed state

no-clock-return-path

scenarioonce

Applies for every adoption

Without a clock row, this adoption measures no elapsed time, performs no local catch-up, creates no calendar crossing, and continues from unchanged fixed state at step 12. Where a clock row exists, this test asserts nothing.

Given

the Instance adoption document and a return from suspension

When
  • return processing checks whether a clock row exists
Then
  • without a clock row, this adoption measures no elapsed time, performs no local catch-up, creates no calendar crossing, and continues from unchanged fixed state at step 12
  • where a clock row exists, this test asserts nothing
Diagnostics
  • Instance-return-timeline
  • Instance-fixed-state-trace
the no-calendar path creates no crossing

no-calendar-row-creates-no-crossing

scenarioonce

Applies for every adoption

Without a calendar-boundaries row, return settlement creates no calendar crossing. Where a row exists, this test asserts nothing.

Given

the Instance adoption document and a return from suspension

When
  • return processing checks whether a calendar-boundaries row exists
Then
  • without a calendar-boundaries row, return settlement creates no calendar crossing
  • where a calendar-boundaries row exists, this test asserts nothing
Diagnostics
  • Instance-calendar-report
  • Instance-return-timeline
Row.id accepts forward time and skips negative time

protected-clock-return-paths

scenarioper clock row

Applies when Clock source is Protected clock.

A non-negative Row.id interval uses the suspension snapshot and elapsed difference. A negative protected-clock interval keeps the loaded state, records zero elapsed time, skips steps 9 to 11, and creates no return reward. Device settings do not control this reading, so no rollback anchor or player-caused clock-change notice is selected.

Given

two returns using Row.id, one with a non-negative difference and one after a protected-clock resync produces a negative difference

When
  • the return reading is sampled once in each run
Then
  • the non-negative run uses the suspension snapshot and the elapsed difference and proceeds through steps 9 to 11
  • the negative run keeps the loaded state, records zero elapsed time, skips steps 9 to 11, and creates no return reward
  • changing device settings does not change the reading supplied by this protected clock
  • no rollback anchor or player-caused clock-change notice is selected; the protected-clock resync branch keeps the loaded state
Diagnostics
  • Instance-clock-readings
  • Instance-return-timeline
  • Instance-reward-report
Row.id uses the device-clock difference on an ordinary return

device-clock-non-negative-return

scenarioper clock row

Applies when Clock source is Device clock.

On a non-negative return, Row.id uses the elapsed difference from the device clock. Moving that clock forward changes the measured interval before row limits are applied.

Given

two otherwise matching returns using Row.id, with one device clock moved forward by a known amount and both return readings non-negative

When
  • each return reading is sampled once
Then
  • each run uses its suspension snapshot and its device-clock elapsed difference
  • the moved-clock run's admitted measured interval differs by the known device-clock amount before row limits are applied
Diagnostics
  • Instance-clock-readings
  • Instance-return-timeline
Row.id restores the suspension snapshot after a backward reading

device-clock-restores-suspension-snapshot

scenarioper clock row

Applies when Clock source is Device clock and Backward clock anchor is Suspension snapshot.

A backward Row.id reading restores every in-scope local item from the suspension snapshot before catch-up. The interval records zero elapsed time, skips steps 9 to 11, and creates no return reward.

Given

a loaded return state distinguishable from the suspension snapshot and a return reading from Row.id earlier than its start

When
  • the backward-clock anchor is applied before catch-up
Then
  • every in-scope local item is restored from the suspension snapshot
  • the interval records zero elapsed time, skips steps 9 to 11, and creates no return reward
Diagnostics
  • Instance-clock-readings
  • Instance-suspension-snapshot
  • Instance-return-timeline
  • Instance-reward-report
Row.id restores the trusted checkpoint after a backward reading

device-clock-restores-trusted-checkpoint

scenarioper clock row

Applies when Clock source is Device clock and Backward clock anchor is Last trusted checkpoint.

A backward Row.id reading restores the coherent trusted checkpoint supplied by the adoption's one rollback-rules row before catch-up. The interval records zero elapsed time, skips steps 9 to 11, and creates no return reward.

Given

a loaded return state distinguishable from the one coherent state and matching reading supplied by the adoption's one rollback-rules row, and a Row.id return reading earlier than its start

When
  • the backward-clock anchor is applied before catch-up
Then
  • the cited trusted checkpoint state is restored
  • the interval records zero elapsed time, skips steps 9 to 11, and creates no return reward
Diagnostics
  • Instance-clock-readings
  • Instance-rollback-trace
  • Instance-return-timeline
  • Instance-reward-report
Row.id keeps the loaded return state after a backward reading

device-clock-keeps-return-state

scenarioper clock row

Applies when Clock source is Device clock and Backward clock anchor is Keep return state.

A backward Row.id reading keeps the loaded return state and restores nothing through this contract. The interval records zero elapsed time, skips steps 9 to 11, and creates no return reward.

Given

a loaded return state distinguishable from the suspension snapshot and a Row.id return reading earlier than its start

When
  • the backward-clock anchor is applied before catch-up
Then
  • this contract restores no state and keeps the loaded return state
  • the interval records zero elapsed time, skips steps 9 to 11, and creates no return reward
Diagnostics
  • Instance-clock-readings
  • Instance-return-state-trace
  • Instance-return-timeline
  • Instance-reward-report
a backward device clock adds no explanation

backward-clock-notice-silent

scenarioonce

Applies when Backward clock notice is Silent.

After the selected anchor is applied, the lifecycle adds no player-facing clock-change explanation.

Given

a backward device-clock return

When
  • the selected anchor has been applied and return processing continues
Then
  • the lifecycle adds no player-facing clock-change explanation
Diagnostics
  • Instance-return-display-trace
a backward device clock is explained before the return surface

backward-clock-notice-explain

scenarioonce

Applies when Backward clock notice is Explain.

After the selected anchor is applied, one player-facing clock-change explanation appears before ordinary play and before any general return surface.

Given

a backward device-clock return

When
  • the selected anchor has been applied and return processing continues
Then
  • one player-facing clock-change explanation appears after the anchor and before ordinary play
  • the explanation precedes any general return surface
Diagnostics
  • Instance-return-display-trace
Row.id supplies one state and matching trusted reading

rollback-reading-protects-next-anchor

scenarioper rollback-rules row

Applies for every adoption

Row.id supplies one coherent snapshot and matching reading from Row.trusted state declared in. After rollback, that trusted reading is offered to the anchor commit beside the suspension and return readings.

Given

the coherent state snapshot and matching reading supplied at Row.trusted state declared in

When
  • a backward-clock return restores that checkpoint and commits the next anchor
Then
  • the restored state and trusted reading remain paired
  • that trusted reading is the one offered to the anchor commit beside the suspension and return readings
Diagnostics
  • Instance-rollback-trace
  • Instance-anchor-commit
a backward return commits an anchor that cannot replay earlier time

backward-return-anchor-is-monotonic

scenarioonce

Applies when Clock source is Device clock.

After a backward-clock return under any anchor, step 15 commits the highest of the suspension reading, the return reading, and any trusted-checkpoint reading. A second rollback replays no time below it.

Given

a backward-clock return under the selected anchor followed by a second rollback

When
  • return processing commits the next suspension anchor
Then
  • after the first return the committed anchor is the highest of the suspension reading, the return reading, and any trusted-checkpoint reading
  • the second rollback replays no time below that committed anchor
Diagnostics
  • Instance-clock-readings
  • Instance-anchor-commit
  • Instance-rollback-trace
Row.id settles an ordinary non-negative interval

non-negative-catch-up-settles

scenarioper catch-up-items row

Applies for every adoption

A non-negative interval settles Row.id from the suspension snapshot and elapsed difference. The trace distinguishes this accepted interval from a skipped or zero-length one.

Given

Row.id at a distinguishable suspension snapshot state and a non-negative elapsed difference

When
  • return processing builds this row's pass timeline
Then
  • Row.id settles from the suspension snapshot and elapsed difference
  • the return trace distinguishes this accepted interval from a skipped or zero-length interval
Diagnostics
  • Instance-return-timeline
  • Instance-catch-up-trace
Row.id admits the whole measured interval

whole-interval-limit

scenarioper catch-up-items row

Applies when row away limit is Whole interval.

Row.id admits the full measured interval before amount and fidelity are applied; Bind limit owner.

Given

two non-negative measured intervals for Row.id, one twice the length of the other

When
  • return processing derives each admitted span
Then
  • each full measured interval is admitted before amount and fidelity are applied
  • Bind limit owner
Diagnostics
  • Instance-return-timeline
  • Instance-catch-up-report
Row.id admits no time past its cited point

time-limit

scenarioper catch-up-items row

Applies when row away limit is Time limit.

For Row.id, the derived admitted span ends at Row.limit rule declared in and admits no later crossing; Bind limit owner. The test names the address and restates nothing from it.

Given

two returns for Row.id, one ending at the point named by Row.limit rule declared in and one continuing past it

When
  • the declared limit is applied and the admitted span is derived
Then
  • the derived admitted span ends at the cited point and admits no later crossing for this row
  • Bind limit owner
  • the test names Row.limit rule declared in and restates nothing from it
Diagnostics
  • Instance-return-timeline
  • Instance-catch-up-report
Row.id uses its later amount rule past the cited point

less-after-a-point-limit

scenarioper catch-up-items row

Applies when row away limit is Less after a point.

Time past Row.limit rule declared in remains admitted for Row.id; Bind limit owner. The test names the address and restates nothing from it.

Given

an interval for Row.id with distinguishable gain before and after the point at Row.limit rule declared in

When
  • the declared limit is applied and the admitted span is derived
Then
  • time past the point remains admitted
  • Bind limit owner
  • the test names Row.limit rule declared in and restates nothing from it
Diagnostics
  • Instance-return-timeline
  • Instance-catch-up-report
Row.id stops at its cited state ceiling

state-ceiling-limit

scenarioper catch-up-items row

Applies when row away limit is State ceiling.

Row.id stops at the ceiling at Row.limit rule declared in; Bind limit owner. Where the citation says the ordinary-play maximum applies, that is the ceiling used here. The test names the address and restates nothing from it.

Given

a settlement for Row.id whose amount would move the state below, to, and past the ceiling at Row.limit rule declared in

When
  • the declared limit is applied and the admitted span is derived
Then
  • the row reaches but never passes that ceiling
  • Bind limit owner
  • where the citation says the same ceiling applies during ordinary play, that ordinary maximum is the one used here
  • the test names Row.limit rule declared in and restates nothing from it
Diagnostics
  • Instance-return-timeline
  • Instance-catch-up-report
Row.id uses the ordinary amount for equal time

same-as-playing-amount

scenarioper catch-up-items row

Applies when row away amount is Same as playing.

For equal elapsed time, Row.id uses the ordinary-play amount. Fidelity and limits remain separate decisions in the report.

Given

matching ordinary-play and admitted-away segments for Row.id with equal elapsed time and the same starting state

When
  • the amount for each segment is computed before fidelity is applied
Then
  • both segments define the same ordinary amount
  • fidelity and limits remain separate recorded decisions
Diagnostics
  • Instance-catch-up-report
Row.id uses only its cited reduced amount rule

reduced-amount

scenarioper catch-up-items row

Applies when row away amount is Reduced.

Row.id uses only the reduced amount from Row.amount rule declared in before fidelity is applied. The test names the address and restates nothing from it.

Given

an admitted segment for Row.id and the complete amount calculation at Row.amount rule declared in

When
  • the amount is computed before fidelity is applied
Then
  • the row receives only the reduced amount produced by that citation
  • the test names Row.amount rule declared in and restates nothing from it
Diagnostics
  • Instance-catch-up-report
Row.id uses only its cited away amount rule

away-rule-amount

scenarioper catch-up-items row

Applies when row away amount is Away rule.

Row.id receives only the total produced by the away rule at Row.amount rule declared in; the row's declared limit then applies to that total as its owner decides. The test names the address and restates nothing from it.

Given

an admitted segment for Row.id and the complete amount calculation at Row.amount rule declared in

When
  • the amount is computed before fidelity is applied
Then
  • the row receives only the total produced by the away rule at Row.amount rule declared in; the row's declared limit then applies to that total as its owner decides
  • the test names Row.amount rule declared in and restates nothing from it
Diagnostics
  • Instance-catch-up-report
Row.id clips each segment by its limit, where one applies

every-missed-update-fidelity

scenarioper catch-up-items row

Applies when row catch up fidelity is Every missed update.

For Row.id, where the row's limit bites, the lifecycle clips each segment by it and then feeds only the remaining missed updates to the game rules. Where the limit is whole-interval, nothing is clipped and every missed update is fed to the game rules.

Given

a pass for Row.id with distinguishable segment edges

When
  • the lifecycle hands each segment to settlement
Then
  • where the row's limit bites, the lifecycle clips the segment by it before feeding only the remaining missed updates to the game rules
  • where the limit is whole-interval, nothing is clipped and every missed update is fed to the game rules
  • the trace contains no update beyond the admitted segment
Diagnostics
  • Instance-return-timeline
  • Instance-catch-up-trace
Row.id gives amount and limit to its larger-step rule

larger-steps-fidelity

scenarioper catch-up-items row

Applies when row catch up fidelity is Larger steps.

Row.fidelity rule declared in receives the separately computed amount and declared limit for Row.id, owns their larger-step distribution and limit, and returns the ordered changes. The lifecycle does not re-apply the limit. The test names the address and restates nothing from it.

Given

the separately computed amount and declared limit for Row.id

When
  • both are handed to Row.fidelity rule declared in
Then
  • the cited rule owns the larger-step distribution and the limit and returns the ordered changes
  • the lifecycle does not re-apply that limit
  • the test names Row.fidelity rule declared in and restates nothing from it
Diagnostics
  • Instance-catch-up-trace
  • Instance-catch-up-report
Row.id gives amount and limit to its one-change rule

one-derived-change-fidelity

scenarioper catch-up-items row

Applies when row catch up fidelity is One derived change.

Row.fidelity rule declared in receives the separately computed amount and declared limit for Row.id, owns the limit, and returns one change. The lifecycle applies it once and does not re-apply the limit. The test names the address and restates nothing from it.

Given

the separately computed amount and declared limit for Row.id

When
  • both are handed to Row.fidelity rule declared in
Then
  • the cited rule owns the limit and returns one change
  • the lifecycle applies that change once and does not re-apply the limit
  • the test names Row.fidelity rule declared in and restates nothing from it
Diagnostics
  • Instance-catch-up-trace
  • Instance-catch-up-report
Row.id keeps amount and one-change distribution separate

away-rule-one-change-composition

scenarioper catch-up-items row

Applies when row away amount is Away rule and row catch up fidelity is One derived change.

For Row.id, Row.amount rule declared in defines the total and Row.fidelity rule declared in distributes it as one change. The test names both addresses and restates nothing from them.

Given

an admitted span for Row.id

When
  • Row.amount rule declared in computes the total and Row.fidelity rule declared in distributes it
Then
  • the amount rule defines the total and the fidelity rule returns its one distributed change
  • neither rule silently takes the other's duty
  • the test names both addresses and restates nothing from them
Diagnostics
  • Instance-catch-up-report
Row.id settles every crossing in ascending order

calendar-every-crossing-in-order

scenarioper calendar-boundaries row

Applies when Crossed calendar boundaries is Every crossing in order.

Row.id admits the full non-negative interval, keeps every crossing in ascending time order, and settles each once through Row.settlement declared in.

Given

a non-negative interval with at least two distinguishable Row.id crossings

When
  • the calendar return timeline is built and settled
Then
  • the calendar row admits the full measured interval and keeps every crossing in ascending time order
  • each crossing settles once through Row.settlement declared in
Diagnostics
  • Instance-return-timeline
  • Instance-calendar-report
Row.id settles only its latest crossing

calendar-latest-crossing-only

scenarioper calendar-boundaries row

Applies when Crossed calendar boundaries is Latest crossing only.

Row.id admits the full non-negative interval, keeps only its latest crossing, omits earlier ones, and settles the selected crossing once through Row.settlement declared in.

Given

a non-negative interval with at least two distinguishable Row.id crossings

When
  • the calendar return timeline is built and settled
Then
  • the calendar row admits the full measured interval, keeps its latest crossing, and omits its earlier crossings
  • the selected crossing settles once through Row.settlement declared in
Diagnostics
  • Instance-return-timeline
  • Instance-calendar-report
Row.id combines its crossings into one return event

calendar-one-combined-crossing

scenarioper calendar-boundaries row

Applies when Crossed calendar boundaries is One combined crossing.

Row.id admits the full non-negative interval and becomes one return-time event carrying the crossing count and span. That event settles once through Row.settlement declared in.

Given

a non-negative interval with at least two distinguishable Row.id crossings

When
  • the calendar return timeline is built and settled
Then
  • the calendar row admits the full measured interval and creates one return-time event carrying the crossing count and span
  • that event settles once through Row.settlement declared in
Diagnostics
  • Instance-return-timeline
  • Instance-calendar-report
row order breaks equal-timestamp ties

segments-events-and-ties-stay-ordered

scenarioonce

Applies for every adoption

Row order breaks equal-timestamp ties before Event resolution receives them. Where no equal-timestamp tie is constructible, this test asserts nothing.

Given

equal-timestamp calendar events where the adoption can construct them

When
  • the return timeline orders the events before settlement
Then
  • row order breaks an equal-timestamp tie before Event resolution receives the events
  • where no equal-timestamp tie is constructible, this test asserts nothing
Diagnostics
  • Instance-return-timeline
  • Instance-calendar-report
  • Instance-catch-up-report
a crossing inside the admitted span for Row.id settles in order

crossing-inside-admitted-span-settles-in-order

scenarioper catch-up-items row

Applies when Crossed calendar boundaries is Every crossing in order or Latest crossing only or One combined crossing.

For Row.id: Bind order; Bind beyond. The row's limit does not cancel the independent calendar event, which settles once on the calendar timeline.

Given

selected calendar crossings and the admitted span for Row.id

When
  • the return timeline is settled and reported
Then
  • Bind order
  • Bind beyond
  • the limit for Row.id does not cancel the independent calendar event, which settles once on the calendar timeline
Diagnostics
  • Instance-return-timeline
  • Instance-calendar-report
  • Instance-catch-up-report
Row.id is created only from its cited source settlement

return-reward-created-from-source

scenarioper return-rewards row

Applies for every adoption

Row.id is created once only when the source settlement at Row.reward declared in settles. No source means no reward, including on a skipped interval. A pending reward survives later suspensions.

Given

two returns for Row.id, one where its cited source settles and one where it does not, plus a later suspension while a created reward remains pending

When
  • step 13 creates return rewards and the later suspension completes
Then
  • the settled-source run creates Row.id once from Row.reward declared in
  • the run with no settled source creates nothing, so a skipped interval creates no reward
  • a pending Row.id survives later suspensions until accepted or expired
Diagnostics
  • Instance-reward-report
  • Instance-return-timeline
Row.id is offered automatically in reward-row order

automatic-reward-delivery

scenarioper return-rewards row

Applies when row delivery is Automatic.

A created Row.id reward is offered once to Row.destination declared in in reward-row order. Acceptance reaches that destination and is reported once. Under step 13, destination refusal keeps the same pending reward, and it is offered again at each later return until its destination accepts it.

Given

two returns where the cited source creates Row.id, with its destination accepting in one run and refusing in the other

When
  • automatic rewards are offered in reward-row order
Then
  • Row.id is offered once to Row.destination declared in in its row position
  • acceptance reaches that destination once and is reported once
  • destination refusal keeps the same pending reward, and it is offered again at each later return until its destination accepts it
Diagnostics
  • Instance-reward-report
Row.id stays pending until its cited claim event

player-claims-reward-delivery

scenarioper return-rewards row

Applies when row delivery is Player claims.

Row.id remains pending until the event at Row.claim declared in offers it to Row.destination declared in after checking any cited deadline. Acceptance delivers it once; refusal keeps the same pending reward. A later claim never repeats catch-up.

Given

a created Row.id, one accepted claim and one destination refusal in distinguishable runs

When
  • the event at Row.claim declared in checks any cited deadline and offers the reward to Row.destination declared in
Then
  • before that event the reward remains pending
  • the accepted claim delivers it once and reports acceptance once
  • destination refusal keeps the same pending reward
  • a later claim is a new event and never repeats catch-up
Diagnostics
  • Instance-reward-report
  • Instance-return-display-trace
Row.id applies its authority reading once

continuous-item-read-once-at-return

scenarioper continuous-items row

Applies for every adoption

At return, Row.id is read once from its cited authority and applied once. Ordinary play resumes without a second local jump.

Given

a distinguishable authority reading for Row.id at return

When
  • step 13 reads continuous items
Then
  • the authority reading is taken once and applied once
  • ordinary play resumes without a second local jump
Diagnostics
  • Instance-continuous-state-trace
Row.id applies its selected branch once

choice-item-applied-once-at-return

scenarioper choice-items row

Applies for every adoption

At return, Row.id applies its selected branch once. This test asserts nothing about branch data beyond what Row.choice declared in is required to name.

Given

a resolved selection for Row.id at return

When
  • step 13 applies the selected branch
Then
  • the selected branch is applied once
  • the test asserts nothing about branch data beyond what Row.choice declared in is required to name
Diagnostics
  • Instance-choice-trace
return adds no player-facing surface

state-only-return-display

scenarioonce

Applies when Return display is State only.

The lifecycle adds no player-facing return surface. Existing game displays can show settled state after ordinary play resumes; developer and diagnostic instrumentation is out of scope.

Given

a completed return settlement

When
  • ordinary play resumes
Then
  • the lifecycle adds no player-facing return surface
  • developer or diagnostic instrumentation is out of scope
Diagnostics
  • Instance-return-display-trace
settled state is visible before ordinary play

visible-before-resume-return-display

scenarioonce

Applies when Return display is Visible before resume.

After settled state and pending rewards are known, at least one existing player-facing display presents the affected state before ordinary play resumes. Any clock explanation comes first.

Given

a return that affects at least one covered row

When
  • settled state and pending rewards are known
Then
  • at least one existing player-facing display presents the affected state before ordinary play resumes
  • where a clock explanation applies, it precedes this display update
Diagnostics
  • Instance-return-display-trace
the return surface names each affected row and result

return-summary-display

scenarioonce

Applies when Return display is Return summary.

After settled state and pending rewards are known, the return surface identifies each affected row and its settled result. Any clock explanation comes first.

Given

a return with distinguishable affected rows

When
  • settled state and pending rewards are known
Then
  • the player-facing return surface identifies each affected row and its settled result
  • where a clock explanation applies, it precedes the return surface
Diagnostics
  • Instance-return-display-trace
the return surface explains each affected result

detailed-return-summary-display

scenarioonce

Applies when Return display is Detailed return summary.

After settled state and pending rewards are known, the return surface identifies each affected row and reports elapsed time, applicable limits, amount rules, fidelity, and settled results. Any clock explanation comes first.

Given

a return with distinguishable affected rows

When
  • settled state and pending rewards are known
Then
  • the player-facing return surface identifies each affected row and reports elapsed time, applicable limits, amount rules, fidelity, and settled results
  • where a clock explanation applies, it precedes the return surface
Diagnostics
  • Instance-return-display-trace
final state and the next anchor commit together

final-state-and-anchor-commit-together

scenarioonce

Applies for every adoption

Final local state and the next suspension anchor commit together where an anchor exists; without one, that clause asserts nothing. Where an anchor exists, step 15 requires it never to be lower than the previous one on any return. Ordinary updates resume only after automatic return changes and required pre-resume displays settle.

Given

a completed return with final local state and, where they exist, distinguishable automatic changes and required pre-resume displays

When
  • return processing reaches step 15
Then
  • final local state and the next suspension anchor commit together where an anchor exists; without one, the anchor clause asserts nothing
  • where an anchor exists, the committed anchor is never lower than the previous one on any return, as step 15 requires
  • ordinary updates resume only after every automatic return change and required pre-resume display has settled
Diagnostics
  • Instance-anchor-commit
  • Instance-return-display-trace
empty row sets create no suspension work

empty-row-sets-create-nothing

scenarioonce

Applies for every adoption

An empty fixed-items set fixes no covered state; an empty catch-up-items set calculates no covered state from missed time on return; an empty continuous-items set means no covered state continued elsewhere; an empty choice-items set selects no away behaviour at runtime; an empty return-rewards set creates no separately delivered reward; and an empty rollback-rules set uses no trusted checkpoint as a backward-clock anchor. Where a row exists, that clause asserts nothing.

Given

the Instance adoption document and its optionally empty row sets

When
  • the lifecycle follows each row set's declared empty consequence
Then
  • where fixed-items is empty, no covered state is fixed by suspension; where a row exists, this clause asserts nothing
  • where catch-up-items is empty, no covered state is calculated from missed time on return; where a row exists, this clause asserts nothing
  • where continuous-items is empty, no covered state continued elsewhere during suspension; where a row exists, this clause asserts nothing
  • where choice-items is empty, no covered state selects between away behaviours at runtime; where a row exists, this clause asserts nothing
  • where return-rewards is empty, return settlement creates no separately delivered reward; where a row exists, this clause asserts nothing
  • where rollback-rules is empty, no trusted checkpoint is used as a backward-clock anchor; where a row exists, this clause asserts nothing
Diagnostics
  • Instance-declaration-record
  • Instance-return-timeline
the catch-up report for Row.id carries the lifecycle fields

catch-up-report-fields

scenarioper catch-up-items row

Applies for every adoption

Each catch-up report for Row.id records the interval readings, admitted elapsed time, row, amount, fidelity, limit, before and after state, and any crossing that split the segment.

Given

each catch-up report produced for Row.id

When
  • a reviewer reads the report
Then
  • each report records interval start and end readings, elapsed time admitted, row id, amount branch, fidelity branch, limit reached, before state, after state, and the calendar crossing that split the segment when present
Diagnostics
  • Instance-catch-up-report
each backward-clock report records its selected response

backward-clock-report-fields

scenarioonce

Applies when Clock source is Device clock or Protected clock.

A backward-clock report records its selected anchor when one was selected and whether a notice appeared when that question applies. Where no such report exists, this test asserts nothing.

Given

each backward-clock report produced by Instance

When
  • a reviewer reads the report
Then
  • the report records the selected anchor when one was selected and whether a notice appeared when the notice question applies
  • where this adoption produces no backward-clock report, this test asserts nothing
Diagnostics
  • Instance-clock-readings
  • Instance-anchor-commit
the return-reward report for Row.id carries its delivery fields

return-reward-report-fields

scenarioper return-rewards row

Applies for every adoption

A return-reward report for Row.id records source, destination, delivery, status, any deadline, and any claim event.

Given

each return-reward report produced for Row.id

When
  • a reviewer reads the report
Then
  • the report records source, destination, delivery, pending, accepted, or expired status, deadline when present, and claim event when present
Diagnostics
  • Instance-reward-report
declaration check: last-trusted-checkpoint has exactly one rollback row

trusted-checkpoint-row-shape

scenarioonce

Applies when Backward clock anchor is Last trusted checkpoint.

This declaration check reads the adoption and cites the rollback-rules description, not the running game. Under last-trusted-checkpoint, exactly one rollback-rules row must exist. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document and the rollback-rules description, not the running game

When
  • a reviewer counts rollback-rules rows
Then
  • exactly one rollback-rules row exists
  • any other shape is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: rollback rows exist only for last-trusted-checkpoint

rollback-row-only-for-trusted-checkpoint

scenarioonce

Applies for every adoption

This declaration check reads the adoption and cites the rollback-rules description, not the running game. A rollback-rules row is legal only under the last-trusted-checkpoint anchor; that anchor's exactly-one duty is checked separately. A protected clock, another anchor, or an adoption with no clock row must have none, and an adoption with no clock row answers no anchor. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document and the rollback-rules description, not the running game

When
  • a reviewer compares its clock source, backward-clock anchor when answered, and rollback-rules rows
Then
  • a protected clock and each device-clock anchor other than last-trusted-checkpoint have no rollback-rules row
  • an adoption with no clock row answers no anchor and has no rollback-rules row
  • under last-trusted-checkpoint this check asserts nothing because the exactly-one check owns that shape
  • any other shape is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: clock has at most one row

at-most-one-clock-row

scenarioonce

Applies for every adoption

This declaration check reads the adoption, not the running game. Clock has at most one row. More than one is a defect this test fails by construction. With no row, the check asserts nothing about elapsed time.

Given

the Instance adoption document, not the running game

When
  • a reviewer counts clock rows
Then
  • the clock collection has zero or one row
  • more than one row is a defect this test fails by construction; with no clock row, the count duty still passes and this check asserts nothing about elapsed time
Diagnostics
  • Instance-declaration-record
declaration check: rollback-rules has at most one row

at-most-one-rollback-row

scenarioonce

Applies for every adoption

This declaration check reads the adoption, not the running game. Rollback-rules has at most one row. More than one is a defect this test fails by construction. With no row, the check asserts nothing about a trusted checkpoint.

Given

the Instance adoption document, not the running game

When
  • a reviewer counts rollback-rules rows
Then
  • the rollback-rules collection has zero or one row
  • more than one row is a defect this test fails by construction; with no rollback row, this check asserts nothing about a trusted checkpoint
Diagnostics
  • Instance-declaration-record
declaration check: Row.id has a claim-capable return surface

player-claim-needs-return-surface

scenarioper return-rewards row

Applies when row delivery is Player claims.

This declaration check reads the adoption and cites the return-rewards delivery description, not the running game. A player-claims row such as Row.id requires return-summary or detailed-return-summary. State-only and visible-before-resume provide no return surface to claim from. Any other shape is a defect this test fails by construction.

Given

the Instance adoption document and the return-rewards delivery description, not the running game

When
  • a reviewer compares Row.id delivery with return-display
Then
  • return-display is return-summary or detailed-return-summary
  • state-only and visible-before-resume are defects for this player-claims row because they provide no return surface to claim from
  • any other shape is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's clock citation states its duty

clock-citation-duty

scenarioper clock row

Applies for every adoption

This declaration check reads the adoption and Row.clock declared in, not the running game. The citation must name Row.id's reading, unit, and sampling. 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 declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.clock declared in names the reading, its unit, and when it is sampled
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's state citation names complete fixed state

fixed-state-citation-duty

scenarioper fixed-items row

Applies for every adoption

This declaration check reads the adoption and Row.state declared in, not the running game. The citation must identify the complete state held fixed for 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.state declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.state declared in identifies the complete state held fixed for Row.id
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's state citation names ordinary changes and unit

catch-up-state-citation-duty

scenarioper catch-up-items row

Applies for every adoption

This declaration check reads the adoption and Row.state declared in, not the running game. The citation must identify Row.id, its ordinary changes, and its unit. 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.state declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.state declared in identifies Row.id, its ordinary changes, and its unit
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's amount citation states the complete amount and its unit

amount-rule-citation-duty

scenarioper catch-up-items row

Applies when row away amount is Reduced or Away rule.

This declaration check reads the adoption and Row.amount rule declared in, not the running game. The citation must state Bind amount duty for 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.amount rule declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.amount rule declared in states Bind amount duty for Row.id
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's fidelity citation states its distribution

fidelity-rule-citation-duty

scenarioper catch-up-items row

Applies when row catch up fidelity is Larger steps or One derived change.

This declaration check reads the adoption and Row.fidelity rule declared in, not the running game. The citation must state Bind fidelity duty for 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.fidelity rule declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.fidelity rule declared in states Bind fidelity duty for Row.id
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's limit citation states its complete boundary

limit-rule-citation-duty

scenarioper catch-up-items row

Applies when row away limit is Time limit or Less after a point or State ceiling.

This declaration check reads the adoption and Row.limit rule declared in, not the running game. The citation must state Bind limit duty for 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.limit rule declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.limit rule declared in states Bind limit duty for Row.id
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's state citation supplies its return reading

continuous-state-citation-duty

scenarioper continuous-items row

Applies for every adoption

This declaration check reads the adoption and Row.state declared in, not the running game. The citation must name the authority that continues Row.id and supplies its return reading. 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.state declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.state declared in names the external or protected rule that continues Row.id and supplies its return reading
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's choice citation states both paths and selection

choice-rule-citation-duty

scenarioper choice-items row

Applies for every adoption

This declaration check reads the adoption and Row.choice declared in, not the running game. The citation must name both behaviours, their complete data, the selector, and the selection time. It asserts nothing further about branch data. 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.choice declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.choice declared in names both possible behaviours, their complete data, the condition selecting one, and the selection time
  • the check asserts nothing about either branch's data beyond that declaration duty
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's reward citation states source and derivation

reward-rule-citation-duty

scenarioper return-rewards row

Applies for every adoption

This declaration check reads the adoption and Row.reward declared in, not the running game. The citation must identify Row.id's source settlement and complete derivation. 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.reward declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.reward declared in identifies the source settlement and complete derivation for Row.id
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's destination citation states acceptance

destination-rule-citation-duty

scenarioper return-rewards row

Applies for every adoption

This declaration check reads the adoption and Row.destination declared in, not the running game. The citation must state how the complete Row.id reward is accepted or left pending. 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.destination declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.destination declared in states how the complete Row.id reward is accepted or left pending
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's claim citation names one event

claim-rule-citation-duty

scenarioper return-rewards row

Applies when row delivery is Player claims.

This declaration check reads the adoption and Row.claim declared in, not the running game. The citation must name the player event that claims pending Row.id from the return surface. 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.claim declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.claim declared in names the player event that claims this pending Row.id from the return surface
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's expiry citation states one deadline

expiry-rule-citation-duty

scenarioper return-rewards row

Applies for every adoption

This declaration check reads the adoption and Bind expiry address, not the running game. The citation must state the deadline when an unclaimed reward is removed for 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 Bind expiry address, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Bind expiry address states the deadline when an unclaimed reward is removed
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's boundary citation states the calendar test

calendar-boundary-citation-duty

scenarioper calendar-boundaries row

Applies for every adoption

This declaration check reads the adoption and Row.boundary declared in, not the running game. The citation must state Row.id's calendar, time zone, boundary test, exact crossing time, and skipped or repeated civil-time behaviour. 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.boundary declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.boundary declared in names the calendar, time zone, boundary inclusion test, exact crossing time, and behaviour when local civil time skips or repeats a boundary
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's settlement citation states immediate effects

calendar-settlement-citation-duty

scenarioper calendar-boundaries row

Applies for every adoption

This declaration check reads the adoption and Row.settlement declared in, not the running game. The citation must state the immediate effects produced from each selected Row.id crossing. 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.settlement declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.settlement declared in states the immediate effects produced from each selected crossing
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id's trusted-state citation supplies a matched pair

trusted-state-citation-duty

scenarioper rollback-rules row

Applies for every adoption

This declaration check reads the adoption and Row.trusted state declared in, not the running game. The citation must supply one coherent state snapshot and matching trusted clock reading. 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.trusted state declared in, not the running game

When
  • a reviewer checks the citation's meaning
Then
  • Row.trusted state declared in supplies one coherent state snapshot and its matching trusted clock reading
  • a missing duty is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
declaration check: Row.id declares a state ceiling when one governs away gain

away-limit-declaration-is-visible

scenarioper catch-up-items row

Applies when row away limit is Whole interval.

This declaration check reads the adoption, cites the away-limit description, and considers an ordinary-play maximum declared elsewhere, not the running game. If that maximum also governs Row.id away gain, this row must declare state-ceiling and cite it. Otherwise the clause asserts nothing. A hidden governing ceiling is a defect this test fails by construction.

Given

the Instance adoption, the away-limit description, and an ordinary-play maximum declared elsewhere, not the running game

When
  • a reviewer checks whether an ordinary-play clamp is intended to stop Row.id away gain
Then
  • where that clamp governs away gain, this row declares state-ceiling and cites it; where no such clamp governs away gain, this clause asserts nothing
  • leaving a governing ceiling hidden behind whole-interval is a defect this test fails by construction
Diagnostics
  • Instance-declaration-record
suspension and catch-up hold for the whole run

suspension-holds

generalonce

Applies for every adoption

Across Inputs scope, no elapsed time is counted twice; each catch-up row follows its amount, fidelity, and limit; each selected crossing settles once in order; each reward reaches its destination or stays pending; skipped intervals create no reward; and the next anchor never falls below the prior one. A case this adoption cannot construct asserts nothing.

Holds

across every covered cycle, no elapsed time was counted twice; every catch-up row followed its amount, fidelity, and limit; every selected crossing settled once in its selected order; every created reward reached its destination or stayed pending as declared; every skipped interval created no reward; and each next anchor never fell below its prior anchor; a case the adoption cannot construct asserts nothing

Seeds

Inputs seeds

Scope

Inputs scope

Diagnostics
  • Instance-suspension-interval
  • Instance-return-timeline
  • Instance-catch-up-report
  • Instance-calendar-report
  • Instance-reward-report
  • Instance-anchor-commit
  • Instance-first-ordering-violation

Use this contract in your game ↑