fix(runtime,verify): single-owner simulation delivery (ARN-236)

[rita-aga]

Summary

Implements ADR-0177 for ARN-236: simulation no longer has competing delayed-message ownership paths.

Studied origin/codex/arn-236-simulation-delayed-delivery (PR #387 used ADR-0171; this PR renumbers to 0177 to avoid concurrent ADR collisions).

Contract

1. SimScheduler::tick advances logical time and enqueues due messages only (no clone return).
2. drain_ready(budget) is the sole ownership transfer; cycle-fair BTreeMap actor order + FIFO per mailbox.
3. Terminal tick flushes every message already due (budgeted batches, no time advance).
4. Integration callbacks are iterative, budgeted (reaction_budget_per_tick), and fallible — rejection fails the run.
5. Runtime and verifier share the same consuming driver API.

Tests (RED→GREEN)

• Scheduler: exactly-once delayed delivery across seeds; budgeted drain; mailbox budget fail-fast.
• Runtime actor system: callback failure invalidates run; final-tick multi-batch drain; shared reaction budget.
• Verifier simulation: delayed message due on final tick delivered; batch-over-budget terminal flush.

Local verification

cargo test -p temper-runtime --lib scheduler::   # 50 passed
cargo test -p temper-verify --lib simulation::   # 9 passed

CI on this PR: Compile & Lint, Tests, DST matrix — green.

Residual

• Parallel codex PR fix(runtime,verify): make simulation delivery single-owner (ARN-236) #387 covers the same fix under ADR-0171; prefer this branch’s ADR-0177 numbering if both land, or close one as duplicate.
• No merge per arena instructions.

Greptile Summary

This PR implements ADR-0177, eliminating the competing delayed-message ownership paths in the simulation layer. SimScheduler::tick now only enqueues due messages into per-actor mailboxes; drain_ready(budget) is the single ownership-transfer point, using cycle-fair BTreeMap iteration and FIFO-per-mailbox order. The terminal tick flushes all remaining ready messages across budgeted batches, and integration-callback reactions share one budget counter per tick across those batches.

• core.rs: tick() returns void; new drain_ready, has_ready_messages, and with_mailbox_budget API added with pre-assertions and deterministic actor ordering.
• sim_actor_system.rs: refactored into sub-modules (callbacks, invariant_eval, random_budget, recording); adds random_in_flight_actions tracking, execution_errors field, and shared-budget drain loop; SimActorResult::all_invariants_held now also requires execution_errors.is_empty().
• temper-verify/simulation.rs: parallel refactor using the same drain_ready / in-flight pattern with terminal-tick flush; adds message_batch_budget to SimConfig.

Confidence Score: 5/5

The changes are fully self-contained to the deterministic simulation layer with no production runtime paths affected; the new drain and budget logic is correctly implemented and exercised by targeted tests.

The single-owner contract is cleanly enforced: tick() is write-only to mailboxes and drain_ready() is the exclusive consumer, removing the previous dual-path hazard. The cycle-fair BTreeMap draining, in-flight reservation accounting, shared reaction budget on terminal ticks, and callback-error invalidation all check out. The test suite covers each new behavior including exactly-once delivery across 16 seeds, terminal multi-batch flush, and shared-budget exhaustion. No logic errors were found in the changed code.

No files require special attention beyond the already-noted ADR status field left as Proposed.

Important Files Changed

Filename	Overview
crates/temper-runtime/src/scheduler/core.rs	Refactored tick() to return void (mailboxes only) and added drain_ready(budget) as the sole ownership-transfer API; added cycle-fair BTreeMap draining via next_mailbox_index and per-actor mailbox budget assertions; logic is correct and well-tested
crates/temper-runtime/src/scheduler/sim_actor_system.rs	Major restructuring: splits into sub-modules, adds random_in_flight_actions tracking, moves to drain_ready loop with shared reaction budget per tick, terminal-tick flush until has_ready_messages() false; has_violations() doc updated as follow-up to prior review
crates/temper-runtime/src/scheduler/sim_actor_system/callbacks.rs	New module: SimIntegrationResponses, SimExecutionError, and the deliver_integration_callbacks / schedule_integration_callbacks / invalidate_callback_cascade methods extracted cleanly from the monolith; reaction-budget check and error recording are correct
crates/temper-runtime/src/scheduler/sim_actor_system/invariant_eval.rs	Extracted evaluate_spec_assert; the OrderingConstraint branch was rewritten using is_none_or — semantics are identical to the original if let Some(arr) else { true } pattern
crates/temper-verify/src/simulation.rs	Parallel refactor: same drain_ready / in-flight pattern, terminal-tick flush, drop accounting; adds message_batch_budget to SimConfig; no reaction budget needed here as verifier has no integration callbacks
crates/temper-runtime/src/scheduler/core/tests.rs	New test file covering exactly-once delayed delivery across 16 seeds, budgeted drain, cycle-fair ordering, and mailbox budget fail-fast; thorough and targeted
crates/temper-runtime/src/scheduler/sim_actor_system/tests.rs	New test file covering callback-failure invalidation, terminal-tick multi-batch drain, shared reaction budget on final tick, and run-record equality; all target precisely the new behaviors
crates/temper-verify/src/simulation/tests.rs	New test file: delayed-message final-tick delivery, batch-over-budget terminal flush, multi-seed reproducibility — all ported and extended from the old inline tests plus two new targeted cases
crates/temper-runtime/src/scheduler/sim_actor_system/random_budget.rs	Tiny helper extracting reserve / release with clear assertion messages; correct and well-placed
crates/temper-runtime/src/scheduler/sim_actor_system/recording.rs	Extracts result_snapshot() and run_random_recorded(); all_invariants_held now correctly requires both violations.is_empty() AND execution_errors.is_empty()
docs/adrs/0177-single-owner-simulation-delivery.md	ADR status remains Proposed while shipping implementation; prior review flagged this — left unaddressed in current diff

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[outer tick loop] --> B["scheduler.send(actor, action) + reserve in_flight"]
    B --> C["scheduler.tick() — advance time, enqueue due msgs to mailboxes"]
    C --> D["process dropped_log — release in_flight for drops"]
    D --> E["reactions = 0, begin drain loop"]
    E --> F["drain_ready(message_batch_budget) — cycle-fair BTreeMap pop_front"]
    F --> G{messages returned?}
    G -->|yes| H["release in_flight per msg, apply_action, schedule callbacks"]
    H --> I["deliver_integration_callbacks(&mut reactions) — shared budget across all batches"]
    I --> J{callback error?}
    J -->|yes| K["break simulation — execution_errors recorded"]
    J -->|no| L{terminal tick AND has_ready_messages?}
    G -->|none| L
    L -->|yes, flush remaining| F
    L -->|no| M[next tick]
    M --> A

Loading

%%{init: {'theme': 'base', 'themeVariables': {"darkMode": true, "background": "#0d1117", "primaryColor": "#21262d", "primaryTextColor": "#e6edf3", "primaryBorderColor": "#8b949e", "lineColor": "#8b949e", "textColor": "#e6edf3", "edgeLabelBackground": "#161b22", "actorBkg": "#21262d", "actorBorder": "#8b949e", "actorTextColor": "#e6edf3", "actorLineColor": "#8b949e", "signalColor": "#8b949e", "signalTextColor": "#e6edf3", "noteBkgColor": "#373320", "noteBorderColor": "#d4a72c", "noteTextColor": "#f0e6c0", "labelBoxBkgColor": "#21262d", "labelBoxBorderColor": "#8b949e", "labelTextColor": "#e6edf3", "loopTextColor": "#e6edf3", "activationBkgColor": "#30363d", "activationBorderColor": "#8b949e"}}}%%
flowchart TD
    A[outer tick loop] --> B["scheduler.send(actor, action) + reserve in_flight"]
    B --> C["scheduler.tick() — advance time, enqueue due msgs to mailboxes"]
    C --> D["process dropped_log — release in_flight for drops"]
    D --> E["reactions = 0, begin drain loop"]
    E --> F["drain_ready(message_batch_budget) — cycle-fair BTreeMap pop_front"]
    F --> G{messages returned?}
    G -->|yes| H["release in_flight per msg, apply_action, schedule callbacks"]
    H --> I["deliver_integration_callbacks(&mut reactions) — shared budget across all batches"]
    I --> J{callback error?}
    J -->|yes| K["break simulation — execution_errors recorded"]
    J -->|no| L{terminal tick AND has_ready_messages?}
    G -->|none| L
    L -->|yes, flush remaining| F
    L -->|no| M[next tick]
    M --> A

Loading

_{Reviews (3): Last reviewed commit: "fix(runtime): address review on simulati..." | Re-trigger Greptile}

Context used:

• Context used - CLAUDE.md (source)
• Context used - AGENTS.md (source)

[rita-aga]

Grok independent review — PR #400 (ARN-236 / ADR-0177)

Scope: Single-owner simulation delivery — SimScheduler::tick enqueues only; drain_ready is the sole ownership transfer; terminal tick flushes due batches; callback rejection fails the run; DST for exactly-once delayed delivery.

What was done well

• Removes the classic dual-owner bug: tick used to clone into mailboxes and return a processable Vec, so drivers could double-process or drop work depending on which path they believed.
• drain_ready(message_budget) is starvation-aware (cyclic lexicographic actor order, FIFO per actor, budgeted) and tested for once-only ownership transfer and multi-seed no-loss under delayed delivery.
• Terminal tick flush (while has_ready_messages on the final tick) is the right answer to “due at horizon must not be discarded”; ordinary ticks stay single-batch so exploration remains budgeted.
• Callbacks move to a budgeted iterative cascade (reaction_budget_per_tick shared across terminal batches); rejection records SimExecutionError and invalidates the run — success is no longer “invariants held while the driver lied.”
• Both in-repo drivers migrate together (runtime SimActorSystem + temper-verify simulation); call-site config fields updated across platform/reference DST harnesses. ADR rollback policy correctly requires joint revert.
• Module split (callbacks, invariant_eval, random_budget, recording, core/tests) improves readability without changing the DST contract surface much.

Findings

Important (should fix / watch)

1. receive remains a second consumer
   Docs say drivers should prefer drain_ready, but receive still pops a mailbox without advancing the shared fairness cursor. A future driver that mixes receive and drain_ready can reintroduce ordering skew (not double delivery of the same message, but fairness/order drift). Consider #[doc(hidden)], deprecation, or routing receive through the same index state for tests-only.

2. Per-actor ready mailbox budget = max_ticks
   Fail-fast is TigerStyle-correct and covered by a should_panic test. Under dense delayed fan-in to one actor, max_ticks may be a tight retention bound relative to message_batch_budget / multi-actor action counts. If CI ever panics on “ready mailbox budget exhausted” in heavy DST, derive budget from max_ticks * max_actions_per_actor (or similar) rather than silently raising defaults.

Suggestions (nice to have)

3. Empty mailbox keys linger in the BTreeMap after drain; drain_ready may walk empty actors until empty_mailboxes_seen trips. Cheap cleanup of empty queues would shrink the actor_ids snapshot on long runs.

4. all_invariants_held now means “invariants ∧ no execution errors”
   Name is slightly misleading for callers that only checked the bool. Field + docs help; a rename or distinct run_succeeded later would be clearer.

5. Random-mode primary apply_action errors still appear discarded with let _ = on delivered messages, while callback failures invalidate. Confirm that is intentional exploration semantics (failed transitions as model outcomes) vs an incomplete migration of error surfaces.

Plan alignment

Matches ADR-0177 readiness gates: single owner, deterministic drain order, terminal flush, callback failure visibility, joint driver migration. DST compliance (BTreeMap/BinaryHeap/VecDeque, no wall clock) holds.

Verdict

Solid structural fix to simulation delivery ownership with strong tests on exactly-once drain, terminal flush, and callback budget failure. Residuals are API footguns and budget calibration, not a return of silent message loss on the migrated paths.

Verdict: PASS

[rita-aga]

@greptile review

[rita-aga]

ARENA SHIPPABLE · Grok · 2026-07-14 11:57 PDT

PR: #400
HEAD: 683e95cf94b9 · branch grok/arn-236-sim-delayed-delivery
Linear: ARN-236 · ADR: 0177
Merge: nothing (arena rules)

Checklist

Gate	Evidence
RED→GREEN	on branch history
Independent same-model review	Verdict: PASS posted on PR
Greptile	requested after PASS
Local tests	targeted suite green before push
CI	GitHub Actions on head

Summary

single-owner sim delivery

[rita-aga]

@greptile review

[rita-aga]

@greptile review

[rita-aga]

Greptile P2s already landed: loop var is tick (not _tick); ADR-0177 Status is Accepted.