[lifecycle-RSK] RSK-02: Extend the bounded model-check to the kernel #1792

Tracking

• Epic: [lifecycle-RSK] Run-state kernel #1790
• Size: 1 SP
• Blocked by: [lifecycle-RSK] RSK-01: Add the pure run-state kernel module #1791
• Cross-link: [lifecycle-P8] Verification and traceability platform #1696
• Design doc: docs/architecture/task-lifecycle-target-architecture.md (not yet on main)
• Ticket plan: docs/architecture/task-lifecycle-run-state-kernel-tickets.md (not yet on main)

Context

The persisted reducers have a bounded model-check in CI. The kernel is a new checked submodel. It must join the suite under the same contract so an illegal state cannot regress.

Developer Notes

• Add scripts/check-run-state-kernel.ts beside the existing checkers.
• Assert the invariants from the design doc in every reachable state.
• On a violation, print the shortest counterexample trace (task-lifecycle-model.md, introduction).
• Meet the suite contract (scripts/check-task-lifecycle.ts:25-27, 228-252): reachability of every event, named landmarks, a declared state budget, unseen-successor detection, and interleaved event sources.
• Add landmarks for: abort during a pending approval inside a live stream, an ask after the stream ends, abandon after the stream ends, dispose after completion, a stream failure cleanup followed by a new stream, and resume that starts a stream without user input.
• Require the stale askSettled no-op after a superseded ask as a reachable action with its own action name, for example askSettledStale. It leaves the state unchanged, so it cannot be a state landmark, and the checker keys action reachability by the name before (.
• Record the boundary mapping to the cleanup model from the design doc. Do not re-prove abort and dispose settlement.
• Add the checker to pnpm lifecycle:model-check.

Exit criteria: pnpm lifecycle:model-check runs the kernel checker in CI and passes the full contract.

Reversibility: the checker is additive.