I3311 — Generated sequences of episode events never move an episode in a way its transition table forbids

✕BLOKOVÁNO vlna 3 · p2 · profil implementation · bezpečné paralelně

Part of the-session-domain-is-written-once — The session lifecycle is written by the typed domain, and the shell only parses and renders.

Cíl

Add proptest harnesses over session::state and session::store: random sequences of open, checkpoint, handover, close, duplicate close, reconnect and recovery keep every invariant of EpisodeState::may_move_to, a closed episode is never active again without an explicit resume, and a record round-trips through its serialisation.

Proč

apps/majordomus-cli/src/session/state.rs:102 holds the whole transition table in one place (EpisodeState::may_move_to; Episode::may_move_to in episode.rs delegates to it) and the cutover proposed in ADR 0047 (status proposed; I3141-I3144) is about to route every shell writer through it. The crate already runs proptest for the mesh journal, protocol and state (src/mesh/*.rs, tests/properties.rs), but nothing under src/session or tests/session_domain.rs is property-tested, so the cutover is guarded only by example cases. The 2026-09-06 lifecycle brief asked for state-machine tests of exactly these invariants. Sources: chatgpt-majordomus:c049#4.

Aktuální stav

At 707a04c no proptest names session, episode or lifecycle (grep -rln proptest apps/majordomus-cli/src apps/majordomus-cli/tests lists mesh, served, quality, integration, deploy, economics and tests/properties.rs only). Case 220_exactly_once_close and tests/session_domain.rs hold exactly-once close by example over the incident's shapes; no generated sequence is tried.

Cílový stav

The session domain's invariants are stated once as properties and hold for any generated sequence, before and after the cutover.

Rozsah

• apps/majordomus-cli/tests/properties.rs
• apps/majordomus-cli/tests/session_domain.rs

Mimo rozsah

• Changing the transition table
• Mesh journal properties, which exist
• Editing apps/majordomus-cli/src/session: the harness drives the domain's public API (session::{EpisodeState, Machine, SessionStore}); a violation it finds is reported against I3141-I3144, which own those files, not fixed here

Závislosti

• I3142✕BLOCKED An episode opens through the typed domain and records the task and issue it began on

Kritéria přijetí

• A property generates event sequences and asserts every applied move is one may_move_to allows
• Duplicate close and duplicate open are idempotent under any interleaving the harness generates
• A closed episode never reads active unless a resume event was generated
• A record serialised and parsed back is equal, for any generated record

Validace

• cargo test --manifest-path apps/majordomus-cli/Cargo.toml --test properties
• cargo test --manifest-path apps/majordomus-cli/Cargo.toml --test session_domain

Požadované důkazy

• test_episode_lifecycle_properties

Důkazy

Nic nezaznamenáno. Za každým tokenem výše musí stát příkaz nebo artefakt, než lze tento úkol dokončit; vyprávění se odmítá.

Časová osa

zahájeno

—

ověřeno

—

dokončeno

—

Tato tři pole, důkazy výše a stav závislostí jsou vše, z čeho se stav skládá. Neexistuje žádné pole stavu, které by s nimi mohlo být v rozporu.

Canonical record: .ai/repo/project/issues/I3311.yaml. Read it back with majordomus plan show I3311.