diff --git a/cli/src/services/mod.rs b/cli/src/services/mod.rs index 76d3c43e..6e1656d2 100644 --- a/cli/src/services/mod.rs +++ b/cli/src/services/mod.rs @@ -28,6 +28,8 @@ pub mod help; pub mod hooks; pub mod lifecycle; pub mod local_db; +#[allow(dead_code)] +pub mod mutation_trace; pub mod observability; pub mod output_format; pub mod parse; diff --git a/cli/src/services/mutation_trace/mod.rs b/cli/src/services/mutation_trace/mod.rs new file mode 100644 index 00000000..51dc24a6 --- /dev/null +++ b/cli/src/services/mutation_trace/mod.rs @@ -0,0 +1,162 @@ +//! Pure Rust domain representation for the refinement of the verified +//! `spec/mutation_cursor.qnt` mutation-cursor protocol. +//! +//! This module defines the protocol's domain/state types, pure accessors, +//! `prepare`/`commitAttempt` transition logic for all four boundary kinds, +//! attribution derivation, mutation-event materialization, snapshot-failure +//! taint, database-failure external taint, scope abandonment, and recovery +//! with an explicit observed-tree input. This completes the action set the +//! plan scoped for `protocol.rs`. +//! +//! No Git, database, filesystem, environment, network, async, or lock I/O is +//! performed here. +//! The module is not yet wired into any hook, command, or database call +//! site: that integration, along with the `coordinator.rs` (imperative +//! shell), `git_snapshot.rs` (isolated Git snapshot capture), and `store.rs` +//! (DB-backed CAS persistence) seams the target architecture will grow into, +//! is left for later work. This layout leaves those three seams as the +//! natural home for: `coordinator.rs` loading/persisting state and supplying +//! the observed-tree inputs `prepare`/`recover` take as explicit parameters; +//! `git_snapshot.rs` capturing and diffing worktree trees; and `store.rs` +//! implementing the CAS-transactional persistence and runtime scope +//! materialization contract described in +//! `context/cli/mutation-trace-protocol.md`. +//! +//! # Quint refinement matrix +//! +//! This module refines `spec/mutation_cursor.qnt`. The table below is +//! auditable against that file: for every relevant Quint element it names +//! the element, whether it is verification-only model instrumentation or a +//! semantic property, its Rust counterpart (if any), its classification, and +//! the concrete test or mechanism backing a non-verification-only +//! classification. A property is classified `verification-only` only when it +//! has no production semantic meaning beyond restating the consistency of +//! the omitted instrumentation itself — never merely because Quint happens +//! to state it using a history variable. +//! +//! ## Verification-only model instrumentation +//! +//! These concrete Quint checkpoint types and history/counter variables exist +//! only to state or prove properties against the finite, enumerated Quint +//! model. `ProtocolState` does not materialize any of them, and no +//! production Rust equivalent exists, unless a future adapter needs one for +//! another reason: `CursorCheckpoint`, `ProtocolCheckpoint`, +//! `ScopeCheckpoint`, `AbandonCheckpoint`, `StartCheckpoint`, +//! `RecoveryCheckpoint`, `DurableProtocolCheckpoint`, and the variables +//! `cursorHistory`, `protocolHistory`, `scopeHistory`, `abandonHistory`, +//! `startHistory`, `recoveryHistory`, `taintHistory`, `evidenceAttempts`, +//! `scopeStartCount`, `everTerminal`. +//! +//! Several Quint invariants exist solely to check the internal consistency +//! of that instrumentation (for example, that two checkpoints for the same +//! worktree/revision are equal, or that a history contains an entry matching +//! current state) rather than to state a fact about production behavior; +//! these are classified `verification-only` alongside the instrumentation +//! they describe: `CursorHistoryUniquePerWorktreeRevision`, +//! `CursorHistoryHasCurrentState`, `ProtocolHistoryUniquePerWorktreeRevision`, +//! `ProtocolHistoryHasCurrentState`, `ScopeHistoryUniquePerWorktreeRevision`, +//! `AbandonHistoryUniquePerWorktreeRevisionScope`, and the witness invariants +//! `HasExclusiveEvidence`/`HasContendedEvidence`/`HasUnscopedEvidence`/ +//! `HasRejectedAttempt` (reachability checks over the finite model, not +//! production properties). +//! +//! A verification-only **data structure** is not the same thing as a +//! verification-only **invariant**: `AbandonCreatesRebaselineRequirement`, +//! `MutationEventsMatchCursorHistory`, and +//! `MutationEventsCrossOnlyTrustworthyProtocolStates` are all *stated* using +//! the history variables above, but each proves a fact this module's +//! production transitions must actually uphold, so all three are classified +//! below as semantic properties, not verification-only. +//! +//! Quint's finite `SCOPES`/`WORKTREES` universes and `init`'s eager +//! population of every `ScopeState`/`WorktreeState` are **external adapter +//! responsibility**: this refinement's `ScopeId`/`WorktreeId` spaces are +//! unbounded runtime strings, so scope/worktree identity is materialized at +//! runtime by the future `coordinator.rs`/`store.rs` layer rather than at +//! protocol startup (see the "Runtime scope materialization" assumption +//! recorded in the plan and in `context/cli/mutation-trace-protocol.md`). +//! +//! ## Semantic properties +//! +//! | Quint element | Rust counterpart | Classification | Backing mechanism | +//! |---|---|---|---| +//! | `CursorRevisionConsistent` | `WorktreeState::revision: u64` | enforced by Rust type | `u64` cannot represent a negative revision | +//! | `AbandonCreatesRebaselineRequirement` | `abandon` | preserved by transition tests | `abandon_transitions_a_live_scope_without_moving_the_cursor_or_changing_identity` proves, in one assertion set, that abandoning sets `Abandoned`+`needs_rebaseline`, leaves the cursor untouched, advances revision by exactly one, and leaves `mutation_events` equal to its pre-abandon value (no evidence emitted for the abandonment revision) | +//! | `FailureKindMatchesTaint` | `WorktreeState::{tainted, failure_kind}` | preserved by transition tests | `taint`/`recover` always set both fields together; `taint_changes_exactly_tainted_failure_kind_and_revision`, `recover_from_snapshot_taint_abandons_live_scopes_and_rebaselines_cursor` | +//! | `TerminalScopesStayTerminal` | `ScopeStatus::{Closed, Abandoned}` | preserved by transition tests | `scope_started_at_most_once_and_stays_terminal_after_a_real_close`, `start_on_a_scope_abandoned_via_a_real_transition_never_reactivates_it` (terminal state reached via real transitions, then re-attempted) | +//! | `ScopeStartedAtMostOnce` | `commit`'s `Start`/`observes` gate | preserved by transition tests | `scope_started_at_most_once_and_stays_terminal_after_a_real_close` | +//! | `DatabaseFailureDoesNotMutateDurableProtocolState` | `database_failure` | preserved by transition tests | `database_failure_changes_exactly_external_taint` | +//! | `ExternalTaintNeverStrengthensAttribution` | `attribution_for` | preserved by transition tests | `attribution_for_is_ineligible_unscoped_when_worktree_is_externally_tainted_even_with_an_active_scope` | +//! | `RecoveryClearsExternalTaintOnlyAfterBaseline` | `recover` | preserved by transition tests | `recover_from_external_taint_abandons_live_scopes_and_clears_external_taint`, `database_failure_then_recover_clears_external_taint_and_rebaselines_cursor` (cursor rebaseline and `external_taint` clearing happen in the same transition) | +//! | `ScopeActorIdentityIsStable` | `ScopeState::actor_kind` | preserved by transition tests + external adapter responsibility | `abandon_transitions_a_live_scope_without_moving_the_cursor_or_changing_identity`; a future adapter must reject a conflicting `actor_kind` for an existing `ScopeId` rather than overwrite it | +//! | `NoNoopMutationEvents` | `commit`'s `changed` gate | preserved by transition tests | `commit_emits_no_mutation_event_for_a_no_op_tree_change` | +//! | `MutationEventsHavePositiveRevision` | `MutationEvent::revision` | preserved by transition tests | `commit` always sets a `MutationEvent`'s revision to the same checked `advanced_revision` (`revision.checked_add(1)`, never `0`) it writes to the worktree; `commit_emits_exactly_one_mutation_event_with_correct_attribution_boundary_and_revision_for_a_real_change` | +//! | `MutationEventUniquePerWorktreeRevision` | `ProtocolState::mutation_events` | preserved by transition tests | one `commit` call inserts at most one event, tagged with the freshly advanced revision, which strictly increases; `attribution_transitions_from_contended_to_exclusive_across_a_close_boundary` produces three events at three distinct revisions | +//! | `MutationFailureKindMatchesTaint` | `MutationEvent::{tainted, failure_kind}` | preserved by transition tests | copied verbatim from the pre-transition `WorktreeState` in `ResolvedAttempt::apply`, so `FailureKindMatchesTaint` carries over | +//! | `MutationEventsMatchCursorHistory` | `ResolvedAttempt::apply`'s `MutationEvent` construction | implemented directly + preserved by transition tests | `apply` derives `before_tree`/`after_tree`/`revision` from the same prepared attempt and the same `advanced_revision` the worktree update itself uses — they cannot diverge by construction; `commit_emits_exactly_one_mutation_event_with_correct_attribution_boundary_and_revision_for_a_real_change`, `attribution_transitions_from_contended_to_exclusive_across_a_close_boundary` (three events at three distinct revisions, each matching its own commit's before/after tree) | +//! | `MutationEventsCrossOnlyTrustworthyProtocolStates` | `commit`'s `changed` gate (`observed_change && !needs_rebaseline`) | implemented directly + preserved by transition tests | `changed` — the sole gate for `MutationEvent` construction — is `false` whenever the pre-transition worktree has `needs_rebaseline: true`, independent of whether a real tree change was observed; `needs_rebaseline_suppresses_mutation_event_even_when_commit_observes_a_real_tree_change` proves `commit` reaches `accepted && observes && observed_change` and still emits no event and leaves the cursor unmoved | +//! | `NeedsRebaselineSuppressesAttribution` | `attribution_for` | preserved by transition tests | `attribution_for_is_ineligible_unscoped_when_worktree_needs_rebaseline_even_with_an_active_scope` | +//! | `AttributionMatchesObservedScopes` | `attribution_for` | preserved by transition tests | `attribution_for_is_ai_exclusive_for_exactly_one_live_scope`, `attribution_for_is_ai_contended_for_multiple_live_scopes`, `attribution_for_is_ineligible_unscoped_when_no_scope_is_live` | +//! | `AiExclusiveRequiresExactlyOneActiveScope` | `Attribution::AiExclusive(ScopeId)` | implemented directly + preserved by transition tests | `Attribution::AiExclusive(ScopeId)` does not itself make an inconsistent scope count unrepresentable (a caller could construct it with any `ScopeId`); the guarantee comes from `attribution_for`'s own algorithm, which only reaches its `AiExclusive` branch when `live.len() == 1`, wrapping that exact scope; `attribution_for_is_ai_exclusive_for_exactly_one_live_scope` | +//! | `AiContendedRequiresMultipleActiveScopes` | `Attribution::AiContended` | preserved by transition tests | `attribution_for_is_ai_contended_for_multiple_live_scopes` | +//! | `RejectedAttemptsDoNotCommitEvidence` | `commit`'s rejection path | preserved by transition tests | rejection returns before the `changed`/`mutation_events` step is ever reached; `rejected_attempts_do_not_commit_evidence_across_a_mixed_accept_reject_sequence`, `competing_prepared_attempts_the_second_to_commit_is_rejected_by_cas`, `taint_invalidates_a_prepared_attempt_via_stale_revision` | +//! | `StartDoesNotAbandonExistingScopes` | `commit`'s `Start` scope transition | preserved by transition tests | only the boundary's own `scope_id` entry is ever written; `start_does_not_abandon_existing_scopes_multi_scope_sequence` | +//! +//! Five properties in the table above (`AbandonCreatesRebaselineRequirement`, +//! `MutationEventsMatchCursorHistory`, +//! `MutationEventsCrossOnlyTrustworthyProtocolStates`, +//! `RejectedAttemptsDoNotCommitEvidence`, `StartDoesNotAbandonExistingScopes`) +//! are stated in Quint using history variables (`abandonHistory`/ +//! `protocolHistory`/`cursorHistory`/`scopeHistory`, `evidenceAttempts`, +//! `startHistory`/`scopeHistory` respectively) but are classified +//! production-semantic, not `verification-only`: the instrumentation itself +//! is omitted, but the fact each one states — no evidence is emitted for an +//! abandonment revision, an emitted event's before/after tree and revision +//! always match the transition that produced it, no evidence crosses a +//! `needs_rebaseline` boundary, no rejected attempt's boundary contributes a +//! `MutationEvent`, and starting one scope never mutates another — is a real +//! guarantee this module's `commit`/`abandon` must uphold, independently +//! verified by the named tests above without needing the history variables +//! themselves. A verification-only *mechanism* never by itself demotes the +//! *property* it was used to prove. +//! +//! ## Bounded-integer revision refinement +//! +//! Quint's `revision: int` (`spec/mutation_cursor.qnt:39`) is an unbounded +//! integer; this refinement's `WorktreeState::revision: u64` is not. Every +//! action that advances a worktree's revision — `commit`, `taint`, +//! `abandon`, `recover` — routes through the private `next_revision` +//! (`revision.checked_add(1)`) helper in `protocol.rs` rather than a raw +//! `+ 1`, so a worktree already at `revision: u64::MAX` cannot be advanced +//! and cannot wrap to `0`. `taint`/`abandon`/`recover` always advance +//! revision when they execute, so each treats the headroom check as an +//! additional guarded no-op alongside their existing existence/precondition +//! guards, verified by `taint_does_not_wrap_revision_at_u64_max`, +//! `abandon_does_not_wrap_revision_at_u64_max`, and +//! `recover_does_not_wrap_revision_at_u64_max`, each starting from +//! `revision: u64::MAX` and proving the action is a no-op rather than a +//! wrap. +//! +//! `commit`'s `accepted` gate requires headroom only when this commit would +//! actually advance the worktree's revision: a non-`Flush` boundary always +//! advances revision when accepted, and a `Flush` advances revision only +//! when it observes a real tree change, so headroom is required for +//! non-`Flush` commits and for a `Flush` with an observed change, but *not* +//! for a `Flush` that observes no change — that commit may still succeed at +//! `revision: u64::MAX`, matching Quint's `commitAttempt`, since nothing +//! about it needs to advance. A rejected (would-be-overflowing) attempt is +//! rejected exactly like a stale one, with no cursor movement, scope +//! transition, processed-`EventKey` insertion, or `MutationEvent`. This +//! headroom guard has no Quint counterpart — Quint's `revision` never needs +//! one — so it is a Rust-only refinement precondition, verified by +//! `commit_that_would_advance_is_rejected_at_u64_max` (a commit that would +//! advance revision is rejected at `u64::MAX`) and +//! `no_change_flush_commits_at_u64_max_without_advancing_revision` (a +//! no-change `Flush` still commits successfully at `u64::MAX`, with revision +//! unchanged). + +pub mod protocol; +pub mod types; + +#[cfg(test)] +mod tests; diff --git a/cli/src/services/mutation_trace/protocol.rs b/cli/src/services/mutation_trace/protocol.rs new file mode 100644 index 00000000..0bddc0c4 --- /dev/null +++ b/cli/src/services/mutation_trace/protocol.rs @@ -0,0 +1,578 @@ +//! Pure transition logic for the mutation-cursor protocol. +//! +//! Refines `liveScopesOn`/`attributionFor` (`spec/mutation_cursor.qnt:265-301`), +//! `mkMutationEvent` (`spec/mutation_cursor.qnt:303-323`), +//! `prepareAvailable`/`prepare`/`commitAttempt` +//! (`spec/mutation_cursor.qnt:417-661`), and +//! `taintHealthy`/`taint`/`recordDatabaseFailure`/`databaseFailure` +//! (`spec/mutation_cursor.qnt:663-737`), `abandonLiveScope`/`abandon` +//! (`spec/mutation_cursor.qnt:739-805`), and `recoverNeeded`/`recover` +//! (`spec/mutation_cursor.qnt:807-886`). Every function here takes and +//! returns plain [`super::types::ProtocolState`] values; none performs Git, +//! database, filesystem, environment, network, async, or lock I/O. + +use std::collections::BTreeSet; + +use super::types::{ + boundary_event_key, boundary_scope, boundary_worktree, is_advance, is_close, is_flush, is_hook, + is_start, AttemptId, AttemptState, AttemptStatus, Attribution, Boundary, FailureKind, + MutationEvent, ProtocolState, ScopeId, ScopeState, ScopeStatus, TreeId, WorktreeId, + WorktreeState, +}; + +/// Advances a worktree revision counter by one, refusing to wrap past +/// `u64::MAX`. +/// +/// Quint's `revision: int` (`spec/mutation_cursor.qnt:39`) is an unbounded +/// integer; this refinement's `revision: u64` is not, so every action that +/// advances a worktree's revision — [`commit`], [`taint`], [`abandon`], and +/// [`recover`] — routes through this single checked helper rather than a raw +/// `+ 1`, so the same bounded-integer refinement guard applies uniformly +/// everywhere the counter can move. `None` signals that advancing would wrap, +/// which every caller treats as a guarded no-op/rejection rather than ever +/// wrapping the counter or committing partial state. +fn next_revision(revision: u64) -> Option { + revision.checked_add(1) +} + +/// The live scopes belonging to `worktree`, read from `state`. Refines +/// `liveScopesOn` (`spec/mutation_cursor.qnt:265-269`). +/// +/// The Quint function filters a fixed `SCOPES` universe by +/// `worktreeId == worktree and isLive(status)`. This refinement's `ScopeId` +/// space is unbounded (see `types.rs`'s module doc comment), so it filters +/// the known `state.scopes` map by the same predicate instead. +pub fn live_scopes_on(state: &ProtocolState, worktree: &WorktreeId) -> BTreeSet { + state + .scopes + .iter() + .filter(|(_, scope_state)| scope_state.worktree_id == *worktree && scope_state.is_live()) + .map(|(scope_id, _)| scope_id.clone()) + .collect() +} + +/// The mutation-evidence attribution for `worktree`, read from `state`. +/// Refines `attributionFor` (`spec/mutation_cursor.qnt:285-301`). +/// +/// `IneligibleUnscoped` when the worktree is unhealthy, externally tainted, +/// needs rebaseline, or has no live scopes; `AiExclusive` for exactly one +/// live scope; `AiContended` for more than one. An unresolvable worktree (no +/// durable state) also yields `IneligibleUnscoped`, matching the "no live +/// scopes" case, since the Quint model's `worktree` always resolves within +/// its finite domain and has no equivalent missing case to refine. +pub fn attribution_for(state: &ProtocolState, worktree: &WorktreeId) -> Attribution { + let live = live_scopes_on(state, worktree); + let unhealthy = state + .worktrees + .get(worktree) + .is_none_or(|w| w.failure_kind != FailureKind::Healthy || w.needs_rebaseline); + + if unhealthy || state.external_taint.contains(worktree) || live.is_empty() { + Attribution::IneligibleUnscoped + } else if live.len() == 1 { + Attribution::AiExclusive(live.into_iter().next().expect("live has exactly one scope")) + } else { + Attribution::AiContended + } +} + +/// Prepares `attempt` against `boundary`, snapshotting the worktree's current +/// `revision`/`cursor_tree` as the attempt's CAS baseline and `observed_tree` +/// as its target `after_tree`. Refines `prepareAvailable`/`prepare` +/// (`spec/mutation_cursor.qnt:417-453`). +/// +/// `observed_tree` corresponds to Quint's `worktreeTrees.get(worktree)`: the +/// currently observed tree at the boundary's resolved worktree, supplied by +/// the caller rather than read internally, since the pure kernel performs no +/// Git I/O. +/// +/// A no-op (refining Quint's `stutter`) when `attempt` already exists with a +/// status other than `Available`, when the boundary's worktree cannot be +/// resolved (an unregistered scope for a hook boundary), or when that +/// worktree has no durable state. +pub fn prepare( + state: &ProtocolState, + attempt: AttemptId, + boundary: Boundary, + observed_tree: TreeId, +) -> ProtocolState { + let already_underway = state + .attempts + .get(&attempt) + .is_some_and(|existing| existing.status != AttemptStatus::Available); + if already_underway { + return state.clone(); + } + + let Some(worktree) = boundary_worktree(&boundary, &state.scopes) else { + return state.clone(); + }; + let Some(worktree_state) = state.worktrees.get(&worktree) else { + return state.clone(); + }; + + let mut next = state.clone(); + next.attempts.insert( + attempt, + AttemptState { + status: AttemptStatus::Prepared, + boundary, + expected_revision: worktree_state.revision, + before_tree: worktree_state.cursor_tree.clone(), + after_tree: observed_tree, + }, + ); + next +} + +/// The computed evaluation flags `commitAttempt` derives before applying its +/// state transition, exposed for callers that need them without +/// reconstructing them from the returned state. +#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)] +#[allow(clippy::struct_excessive_bools)] +pub struct CommitEvaluation { + /// `fresh`: the attempt was `Prepared` against a CAS baseline + /// (`expected_revision`/`before_tree`) that still matches the worktree's + /// current `revision`/`cursor_tree`, the worktree is not externally + /// tainted, and, for hook boundaries, the event has not already been + /// processed. + pub accepted: bool, + /// Whether this boundary observes live protocol state for its scope + /// (`Start` requires `NeverSeen`, `Advance` requires live, `Close` + /// accepts `NeverSeen` or live, `Flush` is always `true`). + pub observes: bool, + /// `accepted and observes and before_tree != after_tree`. + pub observed_change: bool, + /// `observed_change and not needs_rebaseline`. Gates whether [`commit`] + /// materializes a `MutationEvent` for this attempt. + pub changed: bool, + /// `accepted and (not is_flush(boundary) or observed_change)`. + pub advances_revision: bool, +} + +/// The result of evaluating and committing one prepared attempt: the +/// evaluation flags plus the resulting protocol state. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct CommitOutcome { + pub evaluation: CommitEvaluation, + pub state: ProtocolState, +} + +/// Evaluates and commits `attempt`, refining `commitAttempt` +/// (`spec/mutation_cursor.qnt:455-661`) for all four boundary kinds +/// (`Start`/`Advance`/`Close`/`Flush`) in one pass. +/// +/// On rejection (`accepted == false`), only the attempt's own status moves to +/// `Rejected` (or stays as-is if it was never `Prepared`); no other durable +/// state changes, so a rejected or stale attempt never advances the +/// revision, moves the cursor, marks its event processed, or emits mutation +/// evidence. +/// +/// On acceptance, applies scope lifecycle transitions +/// (`NeverSeen`→`Active` on an accepted, observing `Start`; →`Closed` on an +/// accepted, observing `Close`), cursor advancement (`after_tree` when +/// `observes and not needs_rebaseline`, otherwise unchanged), revision +/// advancement and the attempt's `Committed` status, processed-event-key +/// recording for hook boundaries, and — when `changed` — materializes exactly +/// one `MutationEvent` (refining `mkMutationEvent`, +/// `spec/mutation_cursor.qnt:303-323`) whose `active_scopes`/`attribution` +/// are computed by [`live_scopes_on`]/[`attribution_for`] against the +/// **pre-transition** state passed into this call, exactly as `commitAttempt` +/// computes `live`/`attribution` before applying `nextScope` +/// (`spec/mutation_cursor.qnt:484-485` precede the `nextScope` `val` at line +/// 530): a `Start` boundary's emitted event never attributes the mutation to +/// the scope it is about to activate, and a `Close` boundary's emitted event +/// still attributes to the scope it is about to close. +/// +/// A no-op (evaluation flags all `false`, state unchanged) when `attempt` has +/// no prepared record or its boundary's worktree cannot be resolved — an +/// attempt only reaches this state via [`prepare`], which already refuses to +/// prepare against an unresolvable worktree. +pub fn commit(state: &ProtocolState, attempt: &AttemptId) -> CommitOutcome { + let Some(resolved) = ResolvedAttempt::resolve(state, attempt) else { + return CommitOutcome { + evaluation: CommitEvaluation::default(), + state: state.clone(), + }; + }; + let evaluation = resolved.evaluate(state); + let state = resolved.apply(state, attempt, evaluation); + CommitOutcome { evaluation, state } +} + +/// The prepared attempt and its boundary's resolved worktree/scope context, +/// read once and shared by evaluation and application. +struct ResolvedAttempt { + planned: AttemptState, + boundary: Boundary, + worktree: WorktreeId, + worktree_state: WorktreeState, + scope_id: Option, +} + +impl ResolvedAttempt { + fn resolve(state: &ProtocolState, attempt: &AttemptId) -> Option { + let planned = state.attempts.get(attempt)?.clone(); + let boundary = planned.boundary.clone(); + let worktree = boundary_worktree(&boundary, &state.scopes)?; + let worktree_state = state.worktrees.get(&worktree)?.clone(); + let scope_id = boundary_scope(&boundary); + Some(Self { + planned, + boundary, + worktree, + worktree_state, + scope_id, + }) + } + + /// Refines the `fresh`/`observes`/`accepted`/`observedChange`/`changed`/ + /// `advancesRevision` computation at `spec/mutation_cursor.qnt:462-483`. + /// + /// `accepted` additionally requires revision headroom + /// ([`next_revision`]) — a Rust-only refinement guard with no Quint + /// counterpart, since Quint's `revision` is unbounded — but only when + /// this commit would actually advance the worktree's revision. + /// Non-`Flush` commits always advance revision when accepted, so they + /// always require headroom. A `Flush` advances revision only when it + /// observes a real tree change, so a fresh no-change `Flush` may still + /// commit at `revision: u64::MAX`, matching Quint: [`ResolvedAttempt::apply`] + /// never advances the revision for such a commit, so there is nothing + /// for the guard to protect there. + fn evaluate(&self, state: &ProtocolState) -> CommitEvaluation { + let current_scope = self + .scope_id + .as_ref() + .and_then(|scope_id| state.scopes.get(scope_id)); + + let fresh = self.planned.status == AttemptStatus::Prepared + && !state.external_taint.contains(&self.worktree) + && self.planned.expected_revision == self.worktree_state.revision + && self.planned.before_tree == self.worktree_state.cursor_tree + && (!is_hook(&self.boundary) + || boundary_event_key(&self.boundary) + .is_none_or(|key| !state.processed_events.contains(&key))); + let observes = if is_start(&self.boundary) { + current_scope.is_some_and(|s| s.status == ScopeStatus::NeverSeen) + } else if is_advance(&self.boundary) { + current_scope.is_some_and(super::types::ScopeState::is_live) + } else if is_close(&self.boundary) { + current_scope.is_some_and(|s| s.status == ScopeStatus::NeverSeen || s.is_live()) + } else { + true + }; + + let tree_changed = observes && self.planned.before_tree != self.planned.after_tree; + let would_advance_revision = !is_flush(&self.boundary) || tree_changed; + let has_revision_headroom = + !would_advance_revision || next_revision(self.worktree_state.revision).is_some(); + + let accepted = fresh && has_revision_headroom; + let observed_change = accepted && tree_changed; + let changed = observed_change && !self.worktree_state.needs_rebaseline; + let advances_revision = accepted && (!is_flush(&self.boundary) || observed_change); + + CommitEvaluation { + accepted, + observes, + observed_change, + changed, + advances_revision, + } + } + + /// Refines the accepted/rejected state transition at + /// `spec/mutation_cursor.qnt:503-660`. + fn apply( + &self, + state: &ProtocolState, + attempt: &AttemptId, + evaluation: CommitEvaluation, + ) -> ProtocolState { + let mut next = state.clone(); + + if !evaluation.accepted { + if let Some(entry) = next.attempts.get_mut(attempt) { + if entry.status == AttemptStatus::Prepared { + entry.status = AttemptStatus::Rejected; + } + } + return next; + } + + // `evaluate` already proved that advancing the worktree's revision + // cannot wrap whenever `advances_revision` is true; this recomputes + // the same checked value rather than trusting a stored flag, so this + // function has no raw `+ 1` of its own. When `advances_revision` is + // false (a fresh no-change `Flush`), no headroom was required or + // proved, so no next revision is computed at all. + let advanced_revision = if evaluation.advances_revision { + Some( + next_revision(self.worktree_state.revision) + .expect("advancing revision requires headroom, see `evaluate`"), + ) + } else { + None + }; + + // `observes` already encodes the exact scope-status guard + // `commitAttempt` repeats for its own scope transition (`NeverSeen` + // for `Start`, `NeverSeen` or live for `Close`), so reusing it here + // cannot diverge from the spec's separately-stated guard. + if let Some(scope_id) = &self.scope_id { + if is_start(&self.boundary) && evaluation.observes { + if let Some(entry) = next.scopes.get_mut(scope_id) { + entry.status = ScopeStatus::Active; + } + } else if is_close(&self.boundary) && evaluation.observes { + if let Some(entry) = next.scopes.get_mut(scope_id) { + entry.status = ScopeStatus::Closed; + } + } + } + + let next_cursor = if evaluation.observes && !self.worktree_state.needs_rebaseline { + self.planned.after_tree.clone() + } else { + self.worktree_state.cursor_tree.clone() + }; + + if let Some(advanced_revision) = advanced_revision { + next.worktrees.insert( + self.worktree.clone(), + WorktreeState { + cursor_tree: next_cursor, + revision: advanced_revision, + tainted: self.worktree_state.tainted, + failure_kind: self.worktree_state.failure_kind, + needs_rebaseline: self.worktree_state.needs_rebaseline, + }, + ); + } + + if is_hook(&self.boundary) { + if let Some(key) = boundary_event_key(&self.boundary) { + next.processed_events.insert(key); + } + } + + if evaluation.changed { + let revision = advanced_revision.expect("changed implies advances_revision"); + next.mutation_events.insert(MutationEvent { + worktree_id: self.worktree.clone(), + revision, + before_tree: self.planned.before_tree.clone(), + after_tree: self.planned.after_tree.clone(), + active_scopes: live_scopes_on(state, &self.worktree), + tainted: self.worktree_state.tainted, + failure_kind: self.worktree_state.failure_kind, + attribution: attribution_for(state, &self.worktree), + boundary: self.boundary.clone(), + }); + } + + if let Some(entry) = next.attempts.get_mut(attempt) { + entry.status = AttemptStatus::Committed; + } + + next + } +} + +/// Marks `worktree`'s Git snapshot capture as tainted by a snapshot failure. +/// Refines `taintHealthy`/`taint` (`spec/mutation_cursor.qnt:663-710`). +/// +/// Sets `tainted=true` and `failure_kind=SnapshotFailure`, advances +/// `revision` by one, and leaves `cursor_tree`/`needs_rebaseline` untouched. +/// A guarded no-op (refining Quint's `stutter`) when `worktree` is already +/// `tainted`, already in `external_taint`, has no durable state, or is +/// already at `revision: u64::MAX` (see [`next_revision`] — this last case +/// has no Quint counterpart either, since Quint's `revision` is unbounded). +/// +/// The missing-worktree case has no Quint counterpart: `WorktreeId` ranges +/// over the finite `WORKTREES` universe there, and `init` materializes a +/// `WorktreeState` for every member, so every `WorktreeId` already resolves. +/// This refinement's `WorktreeId` is an unbounded runtime value, so an +/// unknown worktree is unresolved kernel input rather than a state `taint` +/// may create — the same existence contract [`database_failure`] enforces. +pub fn taint(state: &ProtocolState, worktree: &WorktreeId) -> ProtocolState { + let Some(worktree_state) = state.worktrees.get(worktree) else { + return state.clone(); + }; + if worktree_state.tainted || state.external_taint.contains(worktree) { + return state.clone(); + } + let Some(next_rev) = next_revision(worktree_state.revision) else { + return state.clone(); + }; + + let mut next = state.clone(); + next.worktrees.insert( + worktree.clone(), + WorktreeState { + cursor_tree: worktree_state.cursor_tree.clone(), + revision: next_rev, + tainted: true, + failure_kind: FailureKind::SnapshotFailure, + needs_rebaseline: worktree_state.needs_rebaseline, + }, + ); + next +} + +/// Records a database failure for `worktree` by adding it to +/// `external_taint`. Refines `recordDatabaseFailure`/`databaseFailure` +/// (`spec/mutation_cursor.qnt:712-737`). +/// +/// Changes `external_taint` only; every other durable worktree/scope field +/// stays as it was. A guarded no-op (refining Quint's `stutter`) when +/// `worktree` is already in `external_taint` or has no durable state. +/// +/// Quint's `WorktreeId` ranges over the finite `WORKTREES` universe, and +/// `init` materializes a `WorktreeState` for every member, so +/// `recordDatabaseFailure` has no explicit existence guard because there is +/// no state for it to guard against — every `WorktreeId` already resolves. +/// This refinement's `WorktreeId` is an unbounded runtime value, so a +/// referenced worktree must already exist in `ProtocolState.worktrees` +/// before this action may operate on it; an unknown `WorktreeId` is +/// unresolved kernel input, not a worktree this action may bring into +/// existence, and keeping `external_taint` a subset of known worktrees +/// matches `taint`'s own existence guard. +pub fn database_failure(state: &ProtocolState, worktree: &WorktreeId) -> ProtocolState { + if !state.worktrees.contains_key(worktree) || state.external_taint.contains(worktree) { + return state.clone(); + } + + let mut next = state.clone(); + next.external_taint.insert(worktree.clone()); + next +} + +/// Abandons `scope`, ending its lifecycle. Refines `abandonLiveScope`/`abandon` +/// (`spec/mutation_cursor.qnt:739-805`). +/// +/// Transitions the scope to `Abandoned`, preserving its `actor_kind` and +/// `worktree_id` (scope identity stability), sets the owning worktree's +/// `needs_rebaseline=true`, advances `revision` by one, and leaves +/// `cursor_tree`/`tainted`/`failure_kind` untouched. A guarded no-op (refining +/// Quint's `stutter`) when the scope is not live — `NeverSeen`, `Closed`, and +/// `Abandoned` all stutter, so a terminal scope can never be reactivated or +/// abandoned again — when its worktree is externally tainted, or when its +/// worktree is already at `revision: u64::MAX` (see [`next_revision`]; no +/// Quint counterpart, since Quint's `revision` is unbounded). +/// +/// Quint's `abandon` resolves the owning worktree unconditionally from +/// `scopes.get(scope).worktreeId`, because the model's finite `SCOPES` +/// universe guarantees every `ScopeId` already has a `ScopeState`. This +/// refinement's `ScopeId` is an unbounded runtime value with no such +/// guarantee (see the runtime scope materialization contract in +/// `context/cli/mutation-trace-protocol.md`), so an unknown scope, or a scope +/// whose own `worktree_id` has no durable `WorktreeState`, is also a guarded +/// no-op — the same existence contract [`taint`]/[`database_failure`] +/// enforce. +pub fn abandon(state: &ProtocolState, scope: &ScopeId) -> ProtocolState { + let Some(scope_state) = state.scopes.get(scope) else { + return state.clone(); + }; + if !scope_state.is_live() || state.external_taint.contains(&scope_state.worktree_id) { + return state.clone(); + } + let Some(worktree_state) = state.worktrees.get(&scope_state.worktree_id) else { + return state.clone(); + }; + let Some(next_rev) = next_revision(worktree_state.revision) else { + return state.clone(); + }; + + let mut next = state.clone(); + next.worktrees.insert( + scope_state.worktree_id.clone(), + WorktreeState { + cursor_tree: worktree_state.cursor_tree.clone(), + revision: next_rev, + tainted: worktree_state.tainted, + failure_kind: worktree_state.failure_kind, + needs_rebaseline: true, + }, + ); + next.scopes.insert( + scope.clone(), + ScopeState { + status: ScopeStatus::Abandoned, + actor_kind: scope_state.actor_kind, + worktree_id: scope_state.worktree_id.clone(), + }, + ); + next +} + +/// Recovers `worktree`, re-baselining its cursor to the currently observed +/// tree and clearing its failure/rebaseline state. Refines +/// `recoverNeeded`/`recover` (`spec/mutation_cursor.qnt:807-886`). +/// +/// `observed_tree` corresponds to Quint's `worktreeTrees.get(worktree)`: the +/// currently observed tree, supplied by the caller rather than read +/// internally, since the pure kernel performs no Git I/O — the same +/// explicit-input contract [`prepare`] follows. +/// +/// Sets `cursor_tree=observed_tree`, `tainted=false`, +/// `failure_kind=Healthy`, `needs_rebaseline=false`, advances `revision` by +/// one, and removes `worktree` from `external_taint`. When the worktree was +/// `tainted` or externally tainted, every live scope on it is transitioned to +/// `Abandoned` (preserving `actor_kind`/`worktree_id`); a worktree recovering +/// only from `needs_rebaseline` preserves its live scopes untouched. +/// +/// A guarded no-op (refining Quint's `stutter`) when the worktree is already +/// healthy, not externally tainted, and does not need rebaseline; when +/// `worktree` has no durable state — the same existence contract +/// [`taint`]/[`database_failure`]/[`abandon`] enforce; or when `worktree` is +/// already at `revision: u64::MAX` (see [`next_revision`]; no Quint +/// counterpart, since Quint's `revision` is unbounded). +pub fn recover( + state: &ProtocolState, + worktree: &WorktreeId, + observed_tree: TreeId, +) -> ProtocolState { + let Some(worktree_state) = state.worktrees.get(worktree) else { + return state.clone(); + }; + let externally_tainted = state.external_taint.contains(worktree); + if !worktree_state.tainted && !externally_tainted && !worktree_state.needs_rebaseline { + return state.clone(); + } + let Some(next_rev) = next_revision(worktree_state.revision) else { + return state.clone(); + }; + + let abandon_live_scopes = worktree_state.tainted || externally_tainted; + + let mut next = state.clone(); + next.worktrees.insert( + worktree.clone(), + WorktreeState { + cursor_tree: observed_tree, + revision: next_rev, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: false, + }, + ); + next.external_taint.remove(worktree); + + if abandon_live_scopes { + for (scope_id, scope_state) in &state.scopes { + if scope_state.worktree_id == *worktree && scope_state.is_live() { + next.scopes.insert( + scope_id.clone(), + ScopeState { + status: ScopeStatus::Abandoned, + actor_kind: scope_state.actor_kind, + worktree_id: scope_state.worktree_id.clone(), + }, + ); + } + } + } + + next +} diff --git a/cli/src/services/mutation_trace/tests.rs b/cli/src/services/mutation_trace/tests.rs new file mode 100644 index 00000000..aa246e36 --- /dev/null +++ b/cli/src/services/mutation_trace/tests.rs @@ -0,0 +1,2309 @@ +use std::collections::{BTreeMap, BTreeSet}; + +use super::protocol::{ + abandon, attribution_for, commit, database_failure, live_scopes_on, prepare, recover, taint, + CommitOutcome, +}; +use super::types::*; + +fn worktree(id: &str) -> WorktreeId { + WorktreeId(id.to_string()) +} + +fn scope(id: &str) -> ScopeId { + ScopeId(id.to_string()) +} + +fn event(id: &str) -> EventId { + EventId(id.to_string()) +} + +fn tree(id: &str) -> TreeId { + TreeId(id.to_string()) +} + +fn attempt_id(id: &str) -> AttemptId { + AttemptId(id.to_string()) +} + +fn healthy_worktree(cursor_tree: TreeId, revision: u64) -> WorktreeState { + WorktreeState { + cursor_tree, + revision, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: false, + } +} + +fn scope_with_status(status: ScopeStatus, worktree_id: WorktreeId) -> ScopeState { + ScopeState { + status, + actor_kind: ActorKind::Codex, + worktree_id, + } +} + +fn start_boundary() -> Boundary { + Boundary::Start { + scope: scope("scope0"), + event: event("event0"), + } +} + +fn advance_boundary() -> Boundary { + Boundary::Advance { + scope: scope("scope0"), + event: event("event1"), + } +} + +fn close_boundary() -> Boundary { + Boundary::Close { + scope: scope("scope0"), + event: event("event2"), + } +} + +fn flush_boundary() -> Boundary { + Boundary::Flush { + worktree: worktree("wt0"), + } +} + +fn scopes() -> BTreeMap { + BTreeMap::from([ + ( + scope("scope0"), + ScopeState { + status: ScopeStatus::Active, + actor_kind: ActorKind::Codex, + worktree_id: worktree("wt0"), + }, + ), + ( + scope("scope1"), + ScopeState { + status: ScopeStatus::Active, + actor_kind: ActorKind::ClaudeCode, + worktree_id: worktree("wt1"), + }, + ), + ]) +} + +/// Prepares and immediately commits `attempt` against `boundary`, the shape +/// every state-sequence test below chains repeatedly. +fn prepare_and_commit( + state: &ProtocolState, + attempt: &AttemptId, + boundary: Boundary, + observed_tree: TreeId, +) -> CommitOutcome { + let prepared = prepare(state, attempt.clone(), boundary, observed_tree); + commit(&prepared, attempt) +} + +#[test] +fn is_live_holds_only_for_active() { + assert!(!is_live(ScopeStatus::NeverSeen)); + assert!(is_live(ScopeStatus::Active)); + assert!(!is_live(ScopeStatus::Closed)); + assert!(!is_live(ScopeStatus::Abandoned)); +} + +#[test] +fn is_terminal_holds_only_for_closed_or_abandoned() { + assert!(!is_terminal(ScopeStatus::NeverSeen)); + assert!(!is_terminal(ScopeStatus::Active)); + assert!(is_terminal(ScopeStatus::Closed)); + assert!(is_terminal(ScopeStatus::Abandoned)); +} + +#[test] +fn scope_state_accessors_mirror_stored_fields() { + let state = ScopeState { + status: ScopeStatus::Active, + actor_kind: ActorKind::Codex, + worktree_id: worktree("wt1"), + }; + assert_eq!(state.scope_worktree(), worktree("wt1")); + assert_eq!(state.scope_actor(), ActorKind::Codex); + assert!(state.is_live()); + assert!(!state.is_terminal()); +} + +#[test] +fn boundary_worktree_looks_up_the_scope_named_by_the_boundary() { + let scopes = scopes(); + + // Start/Advance/Close all name scope0, which the map assigns to wt0. + // The presence of scope1 on a different worktree must not affect this. + assert_eq!( + boundary_worktree(&start_boundary(), &scopes), + Some(worktree("wt0")) + ); + assert_eq!( + boundary_worktree(&advance_boundary(), &scopes), + Some(worktree("wt0")) + ); + assert_eq!( + boundary_worktree(&close_boundary(), &scopes), + Some(worktree("wt0")) + ); +} + +#[test] +fn boundary_worktree_is_keyed_by_the_boundarys_own_scope_id() { + // A boundary naming a different scope resolves to that scope's own + // worktree, proving the lookup is keyed by the boundary's ScopeId rather + // than an arbitrary caller-supplied worktree. + let scopes = scopes(); + let boundary = Boundary::Start { + scope: scope("scope1"), + event: event("event0"), + }; + assert_eq!(boundary_worktree(&boundary, &scopes), Some(worktree("wt1"))); +} + +#[test] +fn boundary_worktree_is_none_for_a_scope_missing_from_the_map() { + let scopes = scopes(); + let boundary = Boundary::Start { + scope: scope("missing_scope"), + event: event("event0"), + }; + assert_eq!(boundary_worktree(&boundary, &scopes), None); +} + +#[test] +fn boundary_worktree_resolves_directly_for_flush_ignoring_the_scope_map() { + let empty_scopes = BTreeMap::new(); + assert_eq!( + boundary_worktree(&flush_boundary(), &empty_scopes), + Some(worktree("wt0")) + ); +} + +#[test] +fn boundary_scope_and_event_are_none_only_for_flush() { + for boundary in [start_boundary(), advance_boundary(), close_boundary()] { + assert!(boundary_scope(&boundary).is_some()); + assert!(boundary_event(&boundary).is_some()); + assert!(boundary_event_key(&boundary).is_some()); + } + assert_eq!(boundary_scope(&flush_boundary()), None); + assert_eq!(boundary_event(&flush_boundary()), None); + assert_eq!(boundary_event_key(&flush_boundary()), None); +} + +#[test] +fn boundary_event_key_pairs_the_boundarys_own_scope_and_event() { + let key = boundary_event_key(&start_boundary()).expect("start boundary has an event key"); + assert_eq!(key.scope_id, scope("scope0")); + assert_eq!(key.event_id, event("event0")); +} + +#[test] +fn is_hook_holds_for_start_advance_close_but_not_flush() { + assert!(is_hook(&start_boundary())); + assert!(is_hook(&advance_boundary())); + assert!(is_hook(&close_boundary())); + assert!(!is_hook(&flush_boundary())); +} + +#[test] +fn boundary_kind_predicates_are_mutually_exclusive() { + let boundaries = [ + start_boundary(), + advance_boundary(), + close_boundary(), + flush_boundary(), + ]; + for boundary in &boundaries { + let flags = [ + is_start(boundary), + is_advance(boundary), + is_close(boundary), + is_flush(boundary), + ]; + assert_eq!( + flags.iter().filter(|flag| **flag).count(), + 1, + "exactly one predicate should hold for {boundary:?}" + ); + } + assert!(is_start(&boundaries[0])); + assert!(is_advance(&boundaries[1])); + assert!(is_close(&boundaries[2])); + assert!(is_flush(&boundaries[3])); +} + +#[test] +fn worktree_state_and_attempt_state_construct_and_compare() { + let a = WorktreeState { + cursor_tree: tree("tree0"), + revision: 0, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: false, + }; + let b = a.clone(); + assert_eq!(a, b); + + let attempt = AttemptState { + status: AttemptStatus::Available, + boundary: start_boundary(), + expected_revision: 0, + before_tree: tree("tree0"), + after_tree: tree("tree1"), + }; + assert_eq!(attempt.status, AttemptStatus::Available); + assert_eq!(attempt.expected_revision, 0); +} + +#[test] +fn mutation_event_carries_attribution_and_active_scopes() { + let mut active_scopes = std::collections::BTreeSet::new(); + active_scopes.insert(scope("scope0")); + + let mutation_event = MutationEvent { + worktree_id: worktree("wt0"), + revision: 1, + before_tree: tree("tree0"), + after_tree: tree("tree1"), + active_scopes: active_scopes.clone(), + tainted: false, + failure_kind: FailureKind::Healthy, + attribution: Attribution::AiExclusive(scope("scope0")), + boundary: close_boundary(), + }; + + assert_eq!(mutation_event.active_scopes, active_scopes); + assert_eq!( + mutation_event.attribution, + Attribution::AiExclusive(scope("scope0")) + ); +} + +/// Final semantic check: proves the lookup is keyed by each boundary's own +/// `scope`, with no parameter through which a caller can independently +/// inject a worktree for a hook boundary. +#[test] +fn boundary_worktree_final_semantic_check() { + let scopes = scopes(); + + let start_scope0 = Boundary::Start { + scope: scope("scope0"), + event: event("event0"), + }; + assert_eq!( + boundary_worktree(&start_scope0, &scopes), + Some(worktree("wt0")) + ); + + let start_scope1 = Boundary::Start { + scope: scope("scope1"), + event: event("event0"), + }; + assert_eq!( + boundary_worktree(&start_scope1, &scopes), + Some(worktree("wt1")) + ); +} + +#[test] +fn prepare_then_commit_accepts_a_fresh_start_and_activates_the_scope() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + start_boundary(), + tree("tree1"), + ); + let prepared_attempt = prepared + .attempts + .get(&attempt_id("attempt0")) + .expect("attempt was prepared"); + assert_eq!(prepared_attempt.status, AttemptStatus::Prepared); + assert_eq!(prepared_attempt.expected_revision, 0); + assert_eq!(prepared_attempt.before_tree, tree("tree0")); + assert_eq!(prepared_attempt.after_tree, tree("tree1")); + + let outcome = commit(&prepared, &attempt_id("attempt0")); + assert!(outcome.evaluation.accepted); + assert!(outcome.evaluation.observes); + assert!(outcome.evaluation.observed_change); + assert!(outcome.evaluation.changed); + assert!(outcome.evaluation.advances_revision); + + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Committed + ); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active + ); + let committed_worktree = outcome.state.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(committed_worktree.revision, 1); + assert_eq!(committed_worktree.cursor_tree, tree("tree1")); + assert!(outcome.state.processed_events.contains(&EventKey { + scope_id: scope("scope0"), + event_id: event("event0"), + })); +} + +#[test] +fn commit_transitions_scope_to_closed_on_an_accepted_observing_close() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + close_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.accepted); + assert!(outcome.evaluation.observes); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Closed + ); + assert_eq!( + outcome + .state + .worktrees + .get(&worktree("wt0")) + .unwrap() + .cursor_tree, + tree("tree1") + ); +} + +#[test] +fn commit_rejects_a_stale_revision_attempt_without_mutating_state() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 1)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + state.attempts.insert( + attempt_id("attempt0"), + AttemptState { + status: AttemptStatus::Prepared, + boundary: start_boundary(), + expected_revision: 0, + before_tree: tree("tree0"), + after_tree: tree("tree1"), + }, + ); + let before = state.clone(); + + let outcome = commit(&state, &attempt_id("attempt0")); + + assert!(!outcome.evaluation.accepted); + assert!(!outcome.evaluation.observed_change); + assert!(!outcome.evaluation.advances_revision); + assert_eq!(outcome.state.worktrees, before.worktrees); + assert_eq!(outcome.state.scopes, before.scopes); + assert_eq!(outcome.state.processed_events, before.processed_events); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +#[test] +fn commit_rejects_a_stale_before_tree_attempt_without_mutating_state() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree_current"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + state.attempts.insert( + attempt_id("attempt0"), + AttemptState { + status: AttemptStatus::Prepared, + boundary: start_boundary(), + expected_revision: 0, + before_tree: tree("tree_stale"), + after_tree: tree("tree1"), + }, + ); + let before = state.clone(); + + let outcome = commit(&state, &attempt_id("attempt0")); + + assert!(!outcome.evaluation.accepted); + assert_eq!(outcome.state.worktrees, before.worktrees); + assert_eq!(outcome.state.scopes, before.scopes); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +#[test] +fn commit_rejects_a_replayed_event_key_without_mutating_state() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + state.processed_events.insert(EventKey { + scope_id: scope("scope0"), + event_id: event("event0"), + }); + state.attempts.insert( + attempt_id("attempt0"), + AttemptState { + status: AttemptStatus::Prepared, + boundary: start_boundary(), + expected_revision: 0, + before_tree: tree("tree0"), + after_tree: tree("tree1"), + }, + ); + let before = state.clone(); + + let outcome = commit(&state, &attempt_id("attempt0")); + + assert!(!outcome.evaluation.accepted); + assert_eq!(outcome.state.worktrees, before.worktrees); + assert_eq!(outcome.state.scopes, before.scopes); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +#[test] +fn commit_rejects_an_externally_tainted_worktree_even_with_a_fresh_revision_and_before_tree() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + state.external_taint.insert(worktree("wt0")); + state.attempts.insert( + attempt_id("attempt0"), + AttemptState { + status: AttemptStatus::Prepared, + boundary: start_boundary(), + expected_revision: 0, + before_tree: tree("tree0"), + after_tree: tree("tree1"), + }, + ); + + let outcome = commit(&state, &attempt_id("attempt0")); + + assert!(!outcome.evaluation.accepted); + assert_eq!( + outcome + .state + .worktrees + .get(&worktree("wt0")) + .unwrap() + .revision, + 0 + ); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::NeverSeen + ); +} + +#[test] +fn accepted_but_non_observing_start_on_an_already_active_scope_advances_revision_without_moving_cursor_or_scope( +) { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + start_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.accepted); + assert!(!outcome.evaluation.observes); + assert!(!outcome.evaluation.observed_change); + assert!(!outcome.evaluation.changed); + assert!(outcome.evaluation.advances_revision); + + let committed_worktree = outcome.state.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(committed_worktree.revision, 1); + assert_eq!(committed_worktree.cursor_tree, tree("tree0")); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active + ); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Committed + ); + assert!(outcome.state.processed_events.contains(&EventKey { + scope_id: scope("scope0"), + event_id: event("event0"), + })); +} + +#[test] +fn accepted_but_non_observing_advance_on_a_never_seen_scope_advances_revision_without_moving_cursor( +) { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + advance_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.accepted); + assert!(!outcome.evaluation.observes); + assert!(!outcome.evaluation.changed); + assert!(outcome.evaluation.advances_revision); + assert_eq!( + outcome + .state + .worktrees + .get(&worktree("wt0")) + .unwrap() + .cursor_tree, + tree("tree0") + ); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::NeverSeen + ); +} + +#[test] +fn accepted_but_non_observing_close_on_a_terminal_scope_advances_revision_without_reactivating_it() +{ + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Abandoned, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + close_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.accepted); + assert!(!outcome.evaluation.observes); + assert!(!outcome.evaluation.changed); + assert!(outcome.evaluation.advances_revision); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Abandoned + ); +} + +#[test] +fn flush_does_not_advance_revision_on_a_no_op_tree_unlike_hook_boundaries() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + flush_boundary(), + tree("tree0"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.accepted); + assert!(outcome.evaluation.observes); + assert!(!outcome.evaluation.observed_change); + assert!(!outcome.evaluation.changed); + assert!(!outcome.evaluation.advances_revision); + + let worktree_state = outcome.state.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(worktree_state.revision, 0); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Committed + ); +} + +#[test] +fn flush_advances_revision_when_it_observes_a_real_tree_change() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + flush_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.accepted); + assert!(outcome.evaluation.observed_change); + assert!(outcome.evaluation.advances_revision); + let worktree_state = outcome.state.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(worktree_state.revision, 1); + assert_eq!(worktree_state.cursor_tree, tree("tree1")); +} + +#[test] +fn live_scopes_on_filters_by_worktree_and_liveness() { + let mut state = ProtocolState::default(); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.scopes.insert( + scope("scope1"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + state.scopes.insert( + scope("scope2"), + scope_with_status(ScopeStatus::Active, worktree("wt1")), + ); + + let live = live_scopes_on(&state, &worktree("wt0")); + assert_eq!(live, BTreeSet::from([scope("scope0")])); +} + +#[test] +fn attribution_for_is_ineligible_unscoped_when_no_scope_is_live() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + + assert_eq!( + attribution_for(&state, &worktree("wt0")), + Attribution::IneligibleUnscoped + ); +} + +#[test] +fn attribution_for_is_ai_exclusive_for_exactly_one_live_scope() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + assert_eq!( + attribution_for(&state, &worktree("wt0")), + Attribution::AiExclusive(scope("scope0")) + ); +} + +#[test] +fn attribution_for_is_ai_contended_for_multiple_live_scopes() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.scopes.insert( + scope("scope1"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + assert_eq!( + attribution_for(&state, &worktree("wt0")), + Attribution::AiContended + ); +} + +#[test] +fn attribution_for_is_ineligible_unscoped_when_worktree_has_a_snapshot_failure_even_with_an_active_scope( +) { + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 0, + tainted: true, + failure_kind: FailureKind::SnapshotFailure, + needs_rebaseline: false, + }, + ); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + assert_eq!( + attribution_for(&state, &worktree("wt0")), + Attribution::IneligibleUnscoped + ); +} + +#[test] +fn attribution_for_is_ineligible_unscoped_when_worktree_is_externally_tainted_even_with_an_active_scope( +) { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.external_taint.insert(worktree("wt0")); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + assert_eq!( + attribution_for(&state, &worktree("wt0")), + Attribution::IneligibleUnscoped + ); +} + +#[test] +fn attribution_for_is_ineligible_unscoped_when_worktree_needs_rebaseline_even_with_an_active_scope() +{ + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 0, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: true, + }, + ); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + assert_eq!( + attribution_for(&state, &worktree("wt0")), + Attribution::IneligibleUnscoped + ); +} + +#[test] +fn commit_emits_no_mutation_event_for_a_no_op_tree_change() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + start_boundary(), + tree("tree0"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(!outcome.evaluation.changed); + assert!(outcome.state.mutation_events.is_empty()); +} + +#[test] +fn commit_emits_exactly_one_mutation_event_with_correct_attribution_boundary_and_revision_for_a_real_change( +) { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + // Advance never changes the scope set, so the pre- and post-transition + // live scopes are identical: attribution is unambiguously AiExclusive. + let prepared = prepare( + &state, + attempt_id("attempt0"), + advance_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.changed); + assert_eq!(outcome.state.mutation_events.len(), 1); + let event = outcome.state.mutation_events.iter().next().unwrap(); + assert_eq!(event.worktree_id, worktree("wt0")); + assert_eq!(event.revision, 1); + assert_eq!(event.before_tree, tree("tree0")); + assert_eq!(event.after_tree, tree("tree1")); + assert_eq!(event.boundary, advance_boundary()); + assert_eq!(event.attribution, Attribution::AiExclusive(scope("scope0"))); + assert_eq!(event.active_scopes, BTreeSet::from([scope("scope0")])); +} + +#[test] +fn commit_start_on_a_never_seen_scope_that_also_observes_a_change_excludes_the_newly_activated_scope_from_attribution( +) { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + start_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.changed); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active + ); + assert_eq!(outcome.state.mutation_events.len(), 1); + let event = outcome.state.mutation_events.iter().next().unwrap(); + assert_eq!(event.attribution, Attribution::IneligibleUnscoped); + assert!(event.active_scopes.is_empty()); +} + +#[test] +fn commit_close_on_the_sole_live_scope_that_also_observes_a_change_still_counts_it_as_live_in_attribution( +) { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + close_boundary(), + tree("tree1"), + ); + let outcome = commit(&prepared, &attempt_id("attempt0")); + + assert!(outcome.evaluation.changed); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Closed + ); + assert_eq!(outcome.state.mutation_events.len(), 1); + let event = outcome.state.mutation_events.iter().next().unwrap(); + assert_eq!(event.attribution, Attribution::AiExclusive(scope("scope0"))); + assert_eq!(event.active_scopes, BTreeSet::from([scope("scope0")])); +} + +#[test] +fn taint_changes_exactly_tainted_failure_kind_and_revision() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 3)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = taint(&state, &worktree("wt0")); + + let tainted = next.worktrees.get(&worktree("wt0")).unwrap(); + assert!(tainted.tainted); + assert_eq!(tainted.failure_kind, FailureKind::SnapshotFailure); + assert_eq!(tainted.revision, 4); + assert_eq!(tainted.cursor_tree, tree("tree0")); + assert!(!tainted.needs_rebaseline); + + assert_eq!(next.scopes, state.scopes); + assert_eq!(next.external_taint, state.external_taint); + assert_eq!(next.processed_events, state.processed_events); + assert_eq!(next.attempts, state.attempts); + assert_eq!(next.mutation_events, state.mutation_events); +} + +#[test] +fn taint_is_a_no_op_when_already_tainted() { + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 0, + tainted: true, + failure_kind: FailureKind::SnapshotFailure, + needs_rebaseline: false, + }, + ); + + let next = taint(&state, &worktree("wt0")); + + assert_eq!(next, state); +} + +#[test] +fn taint_is_a_no_op_when_externally_tainted() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.external_taint.insert(worktree("wt0")); + + let next = taint(&state, &worktree("wt0")); + + assert_eq!(next, state); +} + +#[test] +fn taint_is_a_no_op_for_an_unknown_worktree() { + let state = ProtocolState::default(); + + let next = taint(&state, &worktree("unknown")); + + assert_eq!(next, state); + assert!(!next.worktrees.contains_key(&worktree("unknown"))); +} + +#[test] +fn database_failure_changes_exactly_external_taint() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 3)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = database_failure(&state, &worktree("wt0")); + + assert_eq!(next.external_taint, BTreeSet::from([worktree("wt0")])); + assert_eq!(next.worktrees, state.worktrees); + assert_eq!(next.scopes, state.scopes); + assert_eq!(next.processed_events, state.processed_events); + assert_eq!(next.attempts, state.attempts); + assert_eq!(next.mutation_events, state.mutation_events); +} + +#[test] +fn database_failure_is_a_no_op_when_already_externally_tainted() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.external_taint.insert(worktree("wt0")); + + let next = database_failure(&state, &worktree("wt0")); + + assert_eq!(next, state); +} + +#[test] +fn database_failure_is_a_no_op_for_an_unknown_worktree() { + let state = ProtocolState::default(); + + let next = database_failure(&state, &worktree("unknown")); + + assert_eq!(next, state); + assert!(!next.external_taint.contains(&worktree("unknown"))); +} + +#[test] +fn abandon_transitions_a_live_scope_without_moving_the_cursor_or_changing_identity() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 3)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + let abandoned = next.scopes.get(&scope("scope0")).unwrap(); + assert_eq!(abandoned.status, ScopeStatus::Abandoned); + assert_eq!(abandoned.actor_kind, ActorKind::Codex); + assert_eq!(abandoned.worktree_id, worktree("wt0")); + + let owning_worktree = next.worktrees.get(&worktree("wt0")).unwrap(); + assert!(owning_worktree.needs_rebaseline); + assert_eq!(owning_worktree.revision, 4); + assert_eq!(owning_worktree.cursor_tree, tree("tree0")); + assert!(!owning_worktree.tainted); + assert_eq!(owning_worktree.failure_kind, FailureKind::Healthy); + + assert_eq!(next.external_taint, state.external_taint); + assert_eq!(next.processed_events, state.processed_events); + assert_eq!(next.attempts, state.attempts); + assert_eq!(next.mutation_events, state.mutation_events); +} + +#[test] +fn abandon_preserves_other_live_scopes_on_the_same_worktree() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.scopes.insert( + scope("scope1"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + assert_eq!( + next.scopes.get(&scope("scope1")), + state.scopes.get(&scope("scope1")) + ); +} + +#[test] +fn abandon_is_a_no_op_for_a_never_seen_scope() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + assert_eq!(next, state); +} + +#[test] +fn abandon_is_a_no_op_for_an_already_closed_scope() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Closed, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + assert_eq!(next, state); +} + +#[test] +fn abandon_is_a_no_op_for_an_already_abandoned_scope() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Abandoned, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + assert_eq!(next, state); +} + +#[test] +fn abandon_is_a_no_op_for_a_live_scope_on_an_externally_tainted_worktree() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.external_taint.insert(worktree("wt0")); + + let next = abandon(&state, &scope("scope0")); + + assert_eq!(next, state); +} + +#[test] +fn abandon_succeeds_for_a_live_scope_on_a_snapshot_tainted_worktree() { + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 3, + tainted: true, + failure_kind: FailureKind::SnapshotFailure, + needs_rebaseline: false, + }, + ); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + let abandoned = next.scopes.get(&scope("scope0")).unwrap(); + assert_eq!(abandoned.status, ScopeStatus::Abandoned); + assert_eq!(abandoned.actor_kind, ActorKind::Codex); + assert_eq!(abandoned.worktree_id, worktree("wt0")); + + let owning_worktree = next.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(owning_worktree.revision, 4); + assert_eq!(owning_worktree.cursor_tree, tree("tree0")); + assert!(owning_worktree.tainted); + assert_eq!(owning_worktree.failure_kind, FailureKind::SnapshotFailure); + assert!(owning_worktree.needs_rebaseline); + + assert_eq!(next.external_taint, state.external_taint); + assert_eq!(next.processed_events, state.processed_events); + assert_eq!(next.attempts, state.attempts); + assert_eq!(next.mutation_events, state.mutation_events); +} + +#[test] +fn abandon_is_a_no_op_for_an_unknown_scope() { + let state = ProtocolState::default(); + + let next = abandon(&state, &scope("unknown")); + + assert_eq!(next, state); + assert!(!next.scopes.contains_key(&scope("unknown"))); +} + +#[test] +fn abandon_is_a_no_op_when_the_scopes_worktree_has_no_durable_state() { + let mut state = ProtocolState::default(); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + assert_eq!(next, state); +} + +#[test] +fn recover_from_snapshot_taint_abandons_live_scopes_and_rebaselines_cursor() { + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 3, + tainted: true, + failure_kind: FailureKind::SnapshotFailure, + needs_rebaseline: false, + }, + ); + state + .worktrees + .insert(worktree("wt1"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.scopes.insert( + scope("scope1"), + scope_with_status(ScopeStatus::Closed, worktree("wt0")), + ); + state.scopes.insert( + scope("scope2"), + scope_with_status(ScopeStatus::Active, worktree("wt1")), + ); + + let next = recover(&state, &worktree("wt0"), tree("tree1")); + + let recovered = next.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(recovered.cursor_tree, tree("tree1")); + assert_eq!(recovered.revision, 4); + assert!(!recovered.tainted); + assert_eq!(recovered.failure_kind, FailureKind::Healthy); + assert!(!recovered.needs_rebaseline); + assert_eq!( + next.worktrees.get(&worktree("wt1")), + state.worktrees.get(&worktree("wt1")) + ); + + assert_eq!( + next.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Abandoned + ); + assert_eq!( + next.scopes.get(&scope("scope0")).unwrap().worktree_id, + worktree("wt0") + ); + assert_eq!( + next.scopes.get(&scope("scope1")), + state.scopes.get(&scope("scope1")) + ); + assert_eq!( + next.scopes.get(&scope("scope2")), + state.scopes.get(&scope("scope2")) + ); + + assert_eq!(next.external_taint, state.external_taint); + assert_eq!(next.processed_events, state.processed_events); + assert_eq!(next.attempts, state.attempts); + assert_eq!(next.mutation_events, state.mutation_events); +} + +#[test] +fn recover_from_external_taint_abandons_live_scopes_and_clears_external_taint() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 2)); + state.external_taint.insert(worktree("wt0")); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = recover(&state, &worktree("wt0"), tree("tree1")); + + let recovered = next.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(recovered.cursor_tree, tree("tree1")); + assert_eq!(recovered.revision, 3); + assert!(!recovered.tainted); + assert_eq!(recovered.failure_kind, FailureKind::Healthy); + assert!(!recovered.needs_rebaseline); + + assert!(!next.external_taint.contains(&worktree("wt0"))); + assert_eq!( + next.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Abandoned + ); +} + +#[test] +fn recover_with_only_needs_rebaseline_preserves_live_scopes() { + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 1, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: true, + }, + ); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = recover(&state, &worktree("wt0"), tree("tree1")); + + let recovered = next.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(recovered.cursor_tree, tree("tree1")); + assert_eq!(recovered.revision, 2); + assert!(!recovered.tainted); + assert_eq!(recovered.failure_kind, FailureKind::Healthy); + assert!(!recovered.needs_rebaseline); + + assert_eq!( + next.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active + ); + assert_eq!(next.scopes, state.scopes); +} + +#[test] +fn recover_is_a_no_op_on_an_already_healthy_worktree_with_no_rebaseline_need() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + + let next = recover(&state, &worktree("wt0"), tree("tree1")); + + assert_eq!(next, state); +} + +#[test] +fn recover_is_a_no_op_for_an_unknown_worktree() { + let state = ProtocolState::default(); + + let next = recover(&state, &worktree("unknown"), tree("tree1")); + + assert_eq!(next, state); + assert!(!next.worktrees.contains_key(&worktree("unknown"))); +} + +// T07: cross-action state-sequence tests. Each of the eight scenarios below +// is required by the plan; none is a single-action test already covered by +// T01-T06. + +#[test] +fn attribution_transitions_from_contended_to_exclusive_across_a_close_boundary() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.scopes.insert( + scope("scope1"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + // Both scopes are live: an Advance observing a real change is AiContended. + let step_a = prepare_and_commit( + &state, + &attempt_id("attempt_a"), + Boundary::Advance { + scope: scope("scope0"), + event: event("event_a"), + }, + tree("tree1"), + ); + assert!(step_a.evaluation.changed); + let event_a = step_a + .state + .mutation_events + .iter() + .find(|e| e.revision == 1) + .expect("advance emitted a mutation event at revision 1"); + assert_eq!(event_a.attribution, Attribution::AiContended); + assert_eq!( + event_a.active_scopes, + BTreeSet::from([scope("scope0"), scope("scope1")]) + ); + + // Close also observes a change; because commitAttempt computes live + // scopes *before* nextScope closes scope0, this still emits AiContended, + // not AiExclusive. + let step_b = prepare_and_commit( + &step_a.state, + &attempt_id("attempt_b"), + Boundary::Close { + scope: scope("scope0"), + event: event("event_b"), + }, + tree("tree2"), + ); + assert!(step_b.evaluation.changed); + assert_eq!( + step_b.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Closed + ); + let event_b = step_b + .state + .mutation_events + .iter() + .find(|e| e.revision == 2) + .expect("close emitted a mutation event at revision 2"); + assert_eq!(event_b.attribution, Attribution::AiContended); + assert_eq!( + event_b.active_scopes, + BTreeSet::from([scope("scope0"), scope("scope1")]) + ); + + // Now only scope1 is live: the next observed change is where AiExclusive + // first appears. + let step_c = prepare_and_commit( + &step_b.state, + &attempt_id("attempt_c"), + Boundary::Advance { + scope: scope("scope1"), + event: event("event_c"), + }, + tree("tree3"), + ); + assert!(step_c.evaluation.changed); + let event_c = step_c + .state + .mutation_events + .iter() + .find(|e| e.revision == 3) + .expect("advance emitted a mutation event at revision 3"); + assert_eq!( + event_c.attribution, + Attribution::AiExclusive(scope("scope1")) + ); + assert_eq!(event_c.active_scopes, BTreeSet::from([scope("scope1")])); +} + +#[test] +fn taint_then_recover_abandons_live_scopes_and_rebaselines_cursor() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let tainted = taint(&state, &worktree("wt0")); + let tainted_worktree = tainted.worktrees.get(&worktree("wt0")).unwrap(); + assert!(tainted_worktree.tainted); + assert_eq!(tainted_worktree.failure_kind, FailureKind::SnapshotFailure); + assert_eq!(tainted_worktree.revision, 1); + + let recovered = recover(&tainted, &worktree("wt0"), tree("tree1")); + let recovered_worktree = recovered.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(recovered_worktree.cursor_tree, tree("tree1")); + assert_eq!(recovered_worktree.revision, 2); + assert!(!recovered_worktree.tainted); + assert_eq!(recovered_worktree.failure_kind, FailureKind::Healthy); + assert!(!recovered_worktree.needs_rebaseline); + assert_eq!( + recovered.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Abandoned + ); +} + +#[test] +fn database_failure_then_recover_clears_external_taint_and_rebaselines_cursor() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + + let failed = database_failure(&state, &worktree("wt0")); + assert!(failed.external_taint.contains(&worktree("wt0"))); + assert_eq!( + failed.worktrees.get(&worktree("wt0")), + state.worktrees.get(&worktree("wt0")) + ); + + let recovered = recover(&failed, &worktree("wt0"), tree("tree1")); + assert!(!recovered.external_taint.contains(&worktree("wt0"))); + let recovered_worktree = recovered.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(recovered_worktree.cursor_tree, tree("tree1")); + assert_eq!(recovered_worktree.revision, 1); + assert!(!recovered_worktree.tainted); + assert_eq!(recovered_worktree.failure_kind, FailureKind::Healthy); + assert!(!recovered_worktree.needs_rebaseline); +} + +#[test] +fn abandon_then_needs_rebaseline_only_recovery_preserves_a_second_live_scope() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.scopes.insert( + scope("scope1"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let abandoned = abandon(&state, &scope("scope0")); + let abandoned_worktree = abandoned.worktrees.get(&worktree("wt0")).unwrap(); + assert!(abandoned_worktree.needs_rebaseline); + assert!(!abandoned_worktree.tainted); + assert_eq!( + abandoned.scopes.get(&scope("scope1")).unwrap().status, + ScopeStatus::Active + ); + + let recovered = recover(&abandoned, &worktree("wt0"), tree("tree1")); + let recovered_worktree = recovered.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(recovered_worktree.cursor_tree, tree("tree1")); + assert!(!recovered_worktree.needs_rebaseline); + assert_eq!( + recovered.scopes.get(&scope("scope1")).unwrap().status, + ScopeStatus::Active, + "a needsRebaseline-only recovery must preserve a still-live scope" + ); + assert_eq!( + recovered.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Abandoned + ); +} + +#[test] +fn replay_of_a_committed_event_key_is_rejected_without_mutating_state() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let first = prepare_and_commit( + &state, + &attempt_id("attempt_first"), + start_boundary(), + tree("tree1"), + ); + assert!(first.evaluation.accepted); + + // The CAS baseline is fresh (matches the post-commit worktree state); + // only the replayed EventKey (scope0/event0, same as `start_boundary`) + // should cause rejection. + let before = first.state.clone(); + let replay = prepare_and_commit( + &first.state, + &attempt_id("attempt_replay"), + start_boundary(), + tree("tree2"), + ); + + assert!(!replay.evaluation.accepted); + assert_eq!(replay.state.worktrees, before.worktrees); + assert_eq!(replay.state.scopes, before.scopes); + assert_eq!(replay.state.mutation_events, before.mutation_events); + assert_eq!( + replay + .state + .attempts + .get(&attempt_id("attempt_replay")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +#[test] +fn stale_attempt_prepared_before_an_intervening_flush_commit_is_rejected_without_advancing_revision_or_moving_cursor( +) { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + // Prepare the eventual stale attempt first, baselined at revision 0. + let prepared_stale = prepare( + &state, + attempt_id("attempt_stale"), + start_boundary(), + tree("tree_target"), + ); + + // An unrelated Flush commits and advances the worktree before the + // prepared attempt above is ever committed. + let intervened = prepare_and_commit( + &prepared_stale, + &attempt_id("attempt_flush"), + flush_boundary(), + tree("tree_mid"), + ); + assert!(intervened.evaluation.accepted); + assert_eq!( + intervened + .state + .worktrees + .get(&worktree("wt0")) + .unwrap() + .revision, + 1 + ); + + let before = intervened.state.clone(); + let outcome = commit(&intervened.state, &attempt_id("attempt_stale")); + + assert!(!outcome.evaluation.accepted); + assert!(!outcome.evaluation.advances_revision); + assert_eq!(outcome.state.worktrees, before.worktrees); + assert_eq!(outcome.state.scopes, before.scopes); + assert_eq!(outcome.state.mutation_events, before.mutation_events); + assert_eq!(outcome.state.processed_events, before.processed_events); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt_stale")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +#[test] +fn competing_prepared_attempts_the_second_to_commit_is_rejected_by_cas() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + + // Both A and B are prepared against the same revision-0 baseline. + let prepared_a = prepare( + &state, + attempt_id("attempt_a"), + flush_boundary(), + tree("tree_a"), + ); + let prepared_both = prepare( + &prepared_a, + attempt_id("attempt_b"), + flush_boundary(), + tree("tree_b"), + ); + + let outcome_a = commit(&prepared_both, &attempt_id("attempt_a")); + assert!(outcome_a.evaluation.accepted); + let worktree_after_a = outcome_a.state.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!(worktree_after_a.revision, 1); + assert_eq!(worktree_after_a.cursor_tree, tree("tree_a")); + + let before = outcome_a.state.clone(); + let outcome_b = commit(&outcome_a.state, &attempt_id("attempt_b")); + + assert!(!outcome_b.evaluation.accepted); + assert_eq!(outcome_b.state.worktrees, before.worktrees); + assert_eq!(outcome_b.state.mutation_events, before.mutation_events); + assert_eq!( + outcome_b + .state + .attempts + .get(&attempt_id("attempt_b")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +#[test] +fn taint_invalidates_a_prepared_attempt_via_stale_revision() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let prepared = prepare( + &state, + attempt_id("attempt0"), + start_boundary(), + tree("tree1"), + ); + let tainted = taint(&prepared, &worktree("wt0")); + assert_eq!( + tainted + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Prepared, + "taint does not touch attempt state directly" + ); + + let before = tainted.clone(); + let outcome = commit(&tainted, &attempt_id("attempt0")); + + assert!(!outcome.evaluation.accepted); + assert_eq!(outcome.state.worktrees, before.worktrees); + assert_eq!(outcome.state.scopes, before.scopes); + assert_eq!(outcome.state.mutation_events, before.mutation_events); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +// T07: invariant-style tests, named to mirror the Quint invariants this +// module refines. Each reaches its precondition through real transitions +// rather than a manually constructed state, per the task's own requirement. + +#[test] +fn scope_started_at_most_once_and_stays_terminal_after_a_real_close() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let started = prepare_and_commit( + &state, + &attempt_id("attempt_start"), + start_boundary(), + tree("tree1"), + ); + assert_eq!( + started.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active + ); + + // ScopeStartedAtMostOnce: a second Start (fresh EventKey) on an + // already-Active scope is accepted-but-non-observing and does not + // re-run activation. + let restarted = prepare_and_commit( + &started.state, + &attempt_id("attempt_restart"), + Boundary::Start { + scope: scope("scope0"), + event: event("event_restart"), + }, + tree("tree2"), + ); + assert!(restarted.evaluation.accepted); + assert!(!restarted.evaluation.observes); + assert_eq!( + restarted.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active + ); + assert_eq!( + restarted + .state + .worktrees + .get(&worktree("wt0")) + .unwrap() + .cursor_tree, + tree("tree1"), + "a non-observing restart must not move the cursor" + ); + + let closed = prepare_and_commit( + &restarted.state, + &attempt_id("attempt_close"), + Boundary::Close { + scope: scope("scope0"), + event: event("event_close"), + }, + tree("tree3"), + ); + assert_eq!( + closed.state.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Closed + ); + + // TerminalScopesStayTerminal: a Start against the now-Closed scope + // cannot reactivate it. + let reopen_attempt = prepare_and_commit( + &closed.state, + &attempt_id("attempt_reopen"), + Boundary::Start { + scope: scope("scope0"), + event: event("event_reopen"), + }, + tree("tree4"), + ); + assert!(!reopen_attempt.evaluation.observes); + assert_eq!( + reopen_attempt + .state + .scopes + .get(&scope("scope0")) + .unwrap() + .status, + ScopeStatus::Closed + ); +} + +#[test] +fn start_on_a_scope_abandoned_via_a_real_transition_never_reactivates_it() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let started = prepare_and_commit( + &state, + &attempt_id("attempt_start"), + start_boundary(), + tree("tree1"), + ); + let abandoned = abandon(&started.state, &scope("scope0")); + assert_eq!( + abandoned.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Abandoned + ); + + let reopen_attempt = prepare_and_commit( + &abandoned, + &attempt_id("attempt_reopen"), + Boundary::Start { + scope: scope("scope0"), + event: event("event_reopen"), + }, + tree("tree2"), + ); + assert!(!reopen_attempt.evaluation.observes); + assert_eq!( + reopen_attempt + .state + .scopes + .get(&scope("scope0")) + .unwrap() + .status, + ScopeStatus::Abandoned + ); +} + +#[test] +fn start_does_not_abandon_existing_scopes_multi_scope_sequence() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + state.scopes.insert( + scope("scope1"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + let scope0_before = state.scopes.get(&scope("scope0")).unwrap().clone(); + + let outcome = prepare_and_commit( + &state, + &attempt_id("attempt_start"), + Boundary::Start { + scope: scope("scope1"), + event: event("event0"), + }, + tree("tree1"), + ); + + assert_eq!( + outcome.state.scopes.get(&scope("scope1")).unwrap().status, + ScopeStatus::Active + ); + assert_eq!( + outcome.state.scopes.get(&scope("scope0")).unwrap(), + &scope0_before, + "starting scope1 must not alter the already-active scope0" + ); +} + +#[test] +fn rejected_attempts_do_not_commit_evidence_across_a_mixed_accept_reject_sequence() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), 0)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + + let prepared_start = prepare( + &state, + attempt_id("attempt_start"), + start_boundary(), + tree("tree1"), + ); + let prepared_both = prepare( + &prepared_start, + attempt_id("attempt_advance"), + Boundary::Advance { + scope: scope("scope0"), + event: event("event_advance"), + }, + tree("tree2"), + ); + + let accepted = commit(&prepared_both, &attempt_id("attempt_start")); + assert!(accepted.evaluation.accepted); + assert!(accepted.evaluation.changed); + + let rejected = commit(&accepted.state, &attempt_id("attempt_advance")); + assert!(!rejected.evaluation.accepted); + assert_eq!( + rejected + .state + .attempts + .get(&attempt_id("attempt_advance")) + .unwrap() + .status, + AttemptStatus::Rejected + ); + + // RejectedAttemptsDoNotCommitEvidence: the rejected Advance must not have + // added any mutation evidence beyond what the accepted Start produced. + assert_eq!( + rejected.state.mutation_events, + accepted.state.mutation_events + ); + assert_eq!(rejected.state.mutation_events.len(), 1); +} + +// T07 post-review correction: `needsRebaseline` must suppress mutation +// evidence even when `commit` genuinely observes a real tree change +// (`MutationEventsCrossOnlyTrustworthyProtocolStates`). + +#[test] +fn needs_rebaseline_suppresses_mutation_event_even_when_commit_observes_a_real_tree_change() { + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 0, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: true, + }, + ); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let outcome = prepare_and_commit( + &state, + &attempt_id("attempt0"), + Boundary::Advance { + scope: scope("scope0"), + event: event("event0"), + }, + tree("tree1"), + ); + + assert!(outcome.evaluation.accepted); + assert!(outcome.evaluation.observes); + assert!(outcome.evaluation.observed_change); + assert!( + !outcome.evaluation.changed, + "needs_rebaseline must suppress mutation evidence even though a real change was observed" + ); + + let committed_worktree = outcome.state.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!( + committed_worktree.cursor_tree, + tree("tree0"), + "cursor must not move while needs_rebaseline is set" + ); + assert!(committed_worktree.needs_rebaseline); + assert!( + outcome.state.mutation_events.is_empty(), + "no MutationEvent may be emitted while needs_rebaseline is set" + ); +} + +// T07 post-review correction: Quint's `revision: int` is unbounded; this +// refinement's `revision: u64` is not, so every revision-advancing action +// must refuse to wrap past `u64::MAX` rather than commit partial or wrapped +// state. + +// A commit that would advance revision is rejected at `u64::MAX`: headroom +// is required for advancement, not for acceptance in general. Paired with +// `no_change_flush_commits_at_u64_max_without_advancing_revision` below, +// which proves the other half — a commit that would NOT advance revision +// (a no-change `Flush`) is accepted at `u64::MAX`. +#[test] +fn commit_that_would_advance_is_rejected_at_u64_max() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), u64::MAX)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::NeverSeen, worktree("wt0")), + ); + let before = state.clone(); + + let outcome = prepare_and_commit( + &state, + &attempt_id("attempt0"), + start_boundary(), + tree("tree1"), + ); + + assert!( + !outcome.evaluation.accepted, + "a commit that would advance revision past u64::MAX must be rejected, not wrapped" + ); + assert_eq!(outcome.state.worktrees, before.worktrees); + assert_eq!(outcome.state.scopes, before.scopes); + assert_eq!(outcome.state.processed_events, before.processed_events); + assert_eq!(outcome.state.mutation_events, before.mutation_events); + assert_eq!( + outcome + .state + .worktrees + .get(&worktree("wt0")) + .unwrap() + .revision, + u64::MAX, + "revision must never wrap to 0" + ); + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Rejected + ); +} + +// T07 post-review correction: the first checked-u64 guard required revision +// headroom for every accepted commit, even a no-change `Flush` that would +// not advance revision. Quint's `commitAttempt` accepts and commits that +// case without advancing revision, so a fresh no-change `Flush` at +// `revision: u64::MAX` must commit successfully rather than being rejected +// for headroom it does not need. +#[test] +fn no_change_flush_commits_at_u64_max_without_advancing_revision() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), u64::MAX)); + let before = state.clone(); + + let outcome = prepare_and_commit( + &state, + &attempt_id("attempt0"), + flush_boundary(), + tree("tree0"), + ); + + assert!(outcome.evaluation.accepted); + assert!(outcome.evaluation.observes); + assert!(!outcome.evaluation.observed_change); + assert!(!outcome.evaluation.changed); + assert!( + !outcome.evaluation.advances_revision, + "a no-change Flush must not advance revision even when accepted" + ); + + assert_eq!( + outcome + .state + .attempts + .get(&attempt_id("attempt0")) + .unwrap() + .status, + AttemptStatus::Committed + ); + + let committed_worktree = outcome.state.worktrees.get(&worktree("wt0")).unwrap(); + assert_eq!( + committed_worktree.revision, + u64::MAX, + "revision must stay at u64::MAX; a no-change Flush requires no headroom" + ); + assert_eq!(committed_worktree.cursor_tree, tree("tree0")); + assert_eq!( + outcome.state.worktrees.get(&worktree("wt0")).unwrap(), + before.worktrees.get(&worktree("wt0")).unwrap(), + "the worktree must be otherwise unchanged" + ); + + assert!( + outcome.state.mutation_events.is_empty(), + "no MutationEvent may be emitted for a no-change Flush" + ); + assert_eq!(outcome.state.processed_events, before.processed_events); + assert_eq!(outcome.state.scopes, before.scopes); + assert_eq!(outcome.state.external_taint, before.external_taint); +} + +#[test] +fn taint_does_not_wrap_revision_at_u64_max() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), u64::MAX)); + + let next = taint(&state, &worktree("wt0")); + + assert_eq!( + next, state, + "taint must be a no-op rather than wrap revision" + ); + assert_eq!( + next.worktrees.get(&worktree("wt0")).unwrap().revision, + u64::MAX + ); + assert!(!next.worktrees.get(&worktree("wt0")).unwrap().tainted); +} + +#[test] +fn abandon_does_not_wrap_revision_at_u64_max() { + let mut state = ProtocolState::default(); + state + .worktrees + .insert(worktree("wt0"), healthy_worktree(tree("tree0"), u64::MAX)); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = abandon(&state, &scope("scope0")); + + assert_eq!( + next, state, + "abandon must be a no-op rather than wrap revision" + ); + assert_eq!( + next.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active, + "the scope must not be abandoned if doing so cannot be recorded safely" + ); + assert_eq!( + next.worktrees.get(&worktree("wt0")).unwrap().revision, + u64::MAX + ); +} + +#[test] +fn recover_does_not_wrap_revision_at_u64_max() { + let mut state = ProtocolState::default(); + state.worktrees.insert( + worktree("wt0"), + WorktreeState { + cursor_tree: tree("tree0"), + revision: u64::MAX, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: true, + }, + ); + state.scopes.insert( + scope("scope0"), + scope_with_status(ScopeStatus::Active, worktree("wt0")), + ); + + let next = recover(&state, &worktree("wt0"), tree("tree1")); + + assert_eq!( + next, state, + "recover must be a no-op rather than wrap revision, even though needs_rebaseline would otherwise trigger it" + ); + assert_eq!( + next.worktrees.get(&worktree("wt0")).unwrap().revision, + u64::MAX + ); + assert!( + next.worktrees + .get(&worktree("wt0")) + .unwrap() + .needs_rebaseline + ); + assert_eq!( + next.scopes.get(&scope("scope0")).unwrap().status, + ScopeStatus::Active + ); +} diff --git a/cli/src/services/mutation_trace/types.rs b/cli/src/services/mutation_trace/types.rs new file mode 100644 index 00000000..30a781c5 --- /dev/null +++ b/cli/src/services/mutation_trace/types.rs @@ -0,0 +1,299 @@ +//! Pure domain types for the mutation-cursor protocol. +//! +//! Refines `spec/mutation_cursor.qnt:2-117` (state types) and +//! `spec/mutation_cursor.qnt:151-245` (pure accessors). The Quint model uses +//! finite enumerated identities (`WT0`/`Scope0`/...) as bounded verification +//! domains only; `spec/mutation_cursor.md` states production code "must +//! support larger and unbounded identifier spaces". This module therefore +//! refines every identity type as an opaque wrapper over an owned string +//! rather than a fixed enum, and carries no Git/DB/filesystem/environment/ +//! network/lock/async dependency. + +/// Durable identity of a worktree. Refines `WorktreeId` (`spec/mutation_cursor.qnt:2`). +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct WorktreeId(pub String); + +/// Durable identity of an AI scope/session. Refines `ScopeId` (`spec/mutation_cursor.qnt:4`). +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct ScopeId(pub String); + +/// Identity of a captured worktree tree snapshot. Refines `TreeId` (`spec/mutation_cursor.qnt:5`). +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct TreeId(pub String); + +/// Identity of a hook delivery event. Refines `EventId` (`spec/mutation_cursor.qnt:6-17`). +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct EventId(pub String); + +/// Identity of a speculative attempt. Refines `AttemptId` (`spec/mutation_cursor.qnt:17`). +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct AttemptId(pub String); + +/// Replay/idempotency identity for a hook delivery, scoped by `ScopeId` and +/// `EventId`. Refines `EventKey` (`spec/mutation_cursor.qnt:18-21`). +#[derive(Clone, Debug, Eq, Hash, Ord, PartialEq, PartialOrd)] +pub struct EventKey { + pub scope_id: ScopeId, + pub event_id: EventId, +} + +/// The harness that owns a scope. Unlike the identity types above, this is a +/// real closed set (every supported harness), not a bounded verification +/// domain, so it stays a fixed enum. Refines `ActorKind` (`spec/mutation_cursor.qnt:3`). +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub enum ActorKind { + ClaudeCode, + Codex, + OpenCode, + Pi, +} + +/// Snapshot-failure state of a worktree. Refines `FailureKind` (`spec/mutation_cursor.qnt:22`). +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)] +pub enum FailureKind { + Healthy, + SnapshotFailure, +} + +/// Lifecycle status of a scope. Refines `ScopeStatus` (`spec/mutation_cursor.qnt:24`). +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub enum ScopeStatus { + NeverSeen, + Active, + Closed, + Abandoned, +} + +/// Lifecycle status of a speculative attempt. Refines `AttemptStatus` (`spec/mutation_cursor.qnt:25`). +#[derive(Clone, Copy, Debug, Eq, PartialEq)] +pub enum AttemptStatus { + Available, + Prepared, + Committed, + Rejected, +} + +/// Mutation-evidence attribution for a worktree. Refines `Attribution` +/// (`spec/mutation_cursor.qnt:26-29`). +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd)] +pub enum Attribution { + IneligibleUnscoped, + AiExclusive(ScopeId), + AiContended, +} + +/// A hook or flush boundary at which the protocol may transition state. +/// Refines `Boundary` (`spec/mutation_cursor.qnt:31-35`), field-for-field: +/// `Start`/`Advance`/`Close` carry only `scope`/`event`, exactly like the +/// Quint constructors, and `Flush` carries only `worktree`. +/// +/// A hook variant deliberately carries no independent `worktree` field. The +/// Quint model's `boundaryWorktree` never stores a worktree either — it +/// derives one from `scopeWorktree(data.scope)`. Storing a worktree directly +/// on the boundary would let a value claim a worktree inconsistent with its +/// own scope's true (durable, assigned-for-life) worktree, a state the +/// Quint type cannot represent. See [`boundary_worktree`] for how this +/// refinement resolves a hook boundary's worktree without that field. +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd)] +pub enum Boundary { + Start { scope: ScopeId, event: EventId }, + Advance { scope: ScopeId, event: EventId }, + Close { scope: ScopeId, event: EventId }, + Flush { worktree: WorktreeId }, +} + +/// Durable per-worktree cursor and failure state. Refines `WorktreeState` +/// (`spec/mutation_cursor.qnt:37-43`). +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct WorktreeState { + pub cursor_tree: TreeId, + pub revision: u64, + pub tainted: bool, + pub failure_kind: FailureKind, + pub needs_rebaseline: bool, +} + +/// Durable per-scope lifecycle state. Refines `ScopeState` (`spec/mutation_cursor.qnt:45-49`). +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct ScopeState { + pub status: ScopeStatus, + pub actor_kind: ActorKind, + pub worktree_id: WorktreeId, +} + +/// Transient speculative-attempt state. Refines `AttemptState` (`spec/mutation_cursor.qnt:51-57`). +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct AttemptState { + pub status: AttemptStatus, + pub boundary: Boundary, + pub expected_revision: u64, + pub before_tree: TreeId, + pub after_tree: TreeId, +} + +/// Durable mutation evidence emitted by a committed attempt. Refines +/// `MutationEvent` (`spec/mutation_cursor.qnt:99-109`). +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd)] +pub struct MutationEvent { + pub worktree_id: WorktreeId, + pub revision: u64, + pub before_tree: TreeId, + pub after_tree: TreeId, + pub active_scopes: std::collections::BTreeSet, + pub tainted: bool, + pub failure_kind: FailureKind, + pub attribution: Attribution, + pub boundary: Boundary, +} + +/// A scope is eligible to contribute to attribution. Refines `isLive` +/// (`spec/mutation_cursor.qnt:167`). +pub fn is_live(status: ScopeStatus) -> bool { + status == ScopeStatus::Active +} + +/// A scope has ended and can never be reactivated. Refines `isTerminal` +/// (`spec/mutation_cursor.qnt:169-170`). +pub fn is_terminal(status: ScopeStatus) -> bool { + matches!(status, ScopeStatus::Closed | ScopeStatus::Abandoned) +} + +impl ScopeState { + /// The worktree this scope belongs to. Refines `scopeWorktree` + /// (`spec/mutation_cursor.qnt:151-157`). + /// + /// The Quint function is a pure `match` over `ScopeId` only because the + /// model's identity enum has a fixed, static worktree partition + /// (`Scope0`/`Scope1`/`Scope2` always belong to `WT0`, `Scope3` always to + /// `WT1`). This refinement's `ScopeId` is an opaque, dynamically created + /// identifier with no such static partition (see the module doc + /// comment), so the only faithful source for a scope's worktree is its + /// own durable state — the same fact the Quint model also carries on + /// `ScopeState.worktreeId`, kept consistent with the static function by + /// construction at scope-creation time. + pub fn scope_worktree(&self) -> WorktreeId { + self.worktree_id.clone() + } + + /// The harness that owns this scope. Refines `scopeActor` + /// (`spec/mutation_cursor.qnt:159-165`). + pub fn scope_actor(&self) -> ActorKind { + self.actor_kind + } + + /// Refines `isLive` applied to this scope's status. + pub fn is_live(&self) -> bool { + is_live(self.status) + } + + /// Refines `isTerminal` applied to this scope's status. + pub fn is_terminal(&self) -> bool { + is_terminal(self.status) + } +} + +/// The worktree a boundary applies to. Refines `boundaryWorktree` +/// (`spec/mutation_cursor.qnt:172-178`). +/// +/// For `Start`/`Advance`/`Close`, the function reads the `ScopeId` from the +/// boundary and resolves that exact key in the supplied protocol scope +/// state, mirroring how the Quint function derives the result from +/// `scopeWorktree(data.scope)` rather than from an independently stored +/// value (see the [`Boundary`] doc comment). It does not accept an arbitrary +/// `ScopeState` alongside the boundary: the boundary's own `ScopeId` is the +/// only key ever used to look one up, so no caller can supply a worktree +/// inconsistent with the boundary's scope. The result is `None` when that +/// key is absent from `scopes` (for example, an unknown or not-yet-created +/// scope). +/// +/// For `Flush`, the worktree is carried directly by the boundary and +/// `scopes` is not consulted. +pub fn boundary_worktree( + boundary: &Boundary, + scopes: &std::collections::BTreeMap, +) -> Option { + match boundary { + Boundary::Flush { worktree } => Some(worktree.clone()), + Boundary::Start { scope, .. } + | Boundary::Advance { scope, .. } + | Boundary::Close { scope, .. } => scopes.get(scope).map(ScopeState::scope_worktree), + } +} + +/// The scope a boundary applies to, or `None` for a `Flush` boundary, which +/// carries no scope. Refines `boundaryScope` (`spec/mutation_cursor.qnt:180-186`); +/// `None` replaces the Quint model's arbitrary `Scope0` placeholder default. +pub fn boundary_scope(boundary: &Boundary) -> Option { + match boundary { + Boundary::Start { scope, .. } + | Boundary::Advance { scope, .. } + | Boundary::Close { scope, .. } => Some(scope.clone()), + Boundary::Flush { .. } => None, + } +} + +/// The event a boundary applies to, or `None` for a `Flush` boundary, which +/// carries no event. Refines `boundaryEvent` (`spec/mutation_cursor.qnt:188-194`); +/// `None` replaces the Quint model's arbitrary `Event0` placeholder default. +pub fn boundary_event(boundary: &Boundary) -> Option { + match boundary { + Boundary::Start { event, .. } + | Boundary::Advance { event, .. } + | Boundary::Close { event, .. } => Some(event.clone()), + Boundary::Flush { .. } => None, + } +} + +/// The replay identity of a boundary, or `None` for a `Flush` boundary. +/// Refines `boundaryEventKey` (`spec/mutation_cursor.qnt:196-202`). +pub fn boundary_event_key(boundary: &Boundary) -> Option { + match (boundary_scope(boundary), boundary_event(boundary)) { + (Some(scope_id), Some(event_id)) => Some(EventKey { scope_id, event_id }), + _ => None, + } +} + +/// A boundary is a hook delivery (`Start`/`Advance`/`Close`), not a `Flush`. +/// Refines `isHook` (`spec/mutation_cursor.qnt:204-210`). +pub fn is_hook(boundary: &Boundary) -> bool { + !matches!(boundary, Boundary::Flush { .. }) +} + +/// Refines `isStart` (`spec/mutation_cursor.qnt:212-216`). +pub fn is_start(boundary: &Boundary) -> bool { + matches!(boundary, Boundary::Start { .. }) +} + +/// Refines `isAdvance` (`spec/mutation_cursor.qnt:218-222`). +pub fn is_advance(boundary: &Boundary) -> bool { + matches!(boundary, Boundary::Advance { .. }) +} + +/// Refines `isClose` (`spec/mutation_cursor.qnt:224-228`). +pub fn is_close(boundary: &Boundary) -> bool { + matches!(boundary, Boundary::Close { .. }) +} + +/// Refines `isFlush` (`spec/mutation_cursor.qnt:230-234`). +pub fn is_flush(boundary: &Boundary) -> bool { + matches!(boundary, Boundary::Flush { .. }) +} + +/// The protocol's full durable-plus-transient state. Refines the top-level +/// state variables `worktrees`/`scopes`/`externalTaint`/`processedEvents`/ +/// `attempts`/`mutationEvents` (`spec/mutation_cursor.qnt:2-14`). +/// +/// Quint's verification-only histories (`cursorHistory`, `protocolHistory`, +/// `scopeHistory`, `abandonHistory`, `startHistory`, `recoveryHistory`, +/// `taintHistory`, `evidenceAttempts`, `scopeStartCount`, `everTerminal`) are +/// not represented here; they exist only to state invariants over the +/// verified spec and have no role in the protocol's own behavior. +#[derive(Clone, Debug, Default, Eq, PartialEq)] +pub struct ProtocolState { + pub worktrees: std::collections::BTreeMap, + pub scopes: std::collections::BTreeMap, + pub external_taint: std::collections::BTreeSet, + pub processed_events: std::collections::BTreeSet, + pub attempts: std::collections::BTreeMap, + pub mutation_events: std::collections::BTreeSet, +} diff --git a/context/cli/mutation-trace-protocol.md b/context/cli/mutation-trace-protocol.md new file mode 100644 index 00000000..7e29ed62 --- /dev/null +++ b/context/cli/mutation-trace-protocol.md @@ -0,0 +1,250 @@ +# Mutation-cursor protocol module (`mutation_trace`) + +Pure Rust refinement of the verified `spec/mutation_cursor.qnt` protocol, living +at `cli/src/services/mutation_trace/`. It is not yet wired into any hook, +command, or database call site; that integration is out of scope for the +`mutation-cursor-protocol-kernel` plan and is left for a later plan. + +## Current state + +Domain types, `prepare`/`commit` transition logic, attribution/mutation-event +materialization, snapshot-failure/database-failure taint actions, scope +abandonment, and recovery are all implemented. `types.rs` defines the +protocol's state (including the `ProtocolState` aggregate) and pure +accessors; `protocol.rs` implements `prepare` and `commit` (all four boundary +kinds — `Start`/`Advance`/`Close`/`Flush` — in one pass, refining +`prepareAvailable`/`prepare`/`commitAttempt`), `live_scopes_on`/ +`attribution_for` (refining `liveScopesOn`/`attributionFor`), +`taint`/`database_failure` (refining +`taintHealthy`/`taint`/`recordDatabaseFailure`/`databaseFailure`), `abandon` +(refining `abandonLiveScope`/`abandon`), and `recover` (refining +`recoverNeeded`/`recover`). Cross-action sequence/invariant tests and a +module-level Quint refinement matrix (`mod.rs`) close out the +`mutation-cursor-protocol-kernel` plan's task stack (T01-T07). Registered in +`cli/src/services/mod.rs` with `#[allow(dead_code)]`, matching the existing +precedent for modules not yet consumed by production call sites +(`bash_policy`, `repository_identity`, `agent_trace_export`). + +`commit` materializes exactly one `MutationEvent` into `mutation_events` when +`changed` is true, with `active_scopes`/`attribution` computed by +`live_scopes_on`/`attribution_for` against the state as it existed *before* +the same call's own scope-lifecycle transition — a `Start` boundary's emitted +event never attributes the mutation to the scope it is about to activate, and +a `Close` boundary's emitted event still attributes to the scope it is about +to close. + +## Module layout + +- `mod.rs` — public module boundary and module-level doc comment. +- `types.rs` — state/domain types and pure accessors (`ProtocolState`, + `WorktreeState`, `ScopeState`, `AttemptState`, `MutationEvent`, `Boundary`, + `Attribution`, and the identity/status/failure-kind types they compose + from). +- `protocol.rs` — pure transition logic: `prepare` (refining + `prepareAvailable`/`prepare`) and `commit` (refining `commitAttempt`), + returning a `CommitOutcome` that pairs the resulting `ProtocolState` with a + `CommitEvaluation` (`accepted`/`observes`/`observed_change`/`changed`/ + `advances_revision`); `live_scopes_on` and `attribution_for` (refining + `liveScopesOn`/`attributionFor`), each callable standalone or via `commit`'s + internal `MutationEvent` materialization; `taint` (refining + `taintHealthy`/`taint`), `database_failure` (refining + `recordDatabaseFailure`/`databaseFailure`), `abandon` (refining + `abandonLiveScope`/`abandon`), and `recover` (refining + `recoverNeeded`/`recover`, taking the currently observed tree as an + explicit `TreeId` parameter), each a guarded no-op action independent of + `prepare`/`commit`. +- `tests.rs` — `#[cfg(test)]` coverage for the current slice, sibling to + `mod.rs`. + +See [mutation-trace-revision-refinement.md](mutation-trace-revision-refinement.md) +for the Quint `int` → Rust `u64` worktree-revision refinement all four enforce. + +The module performs no Git, database, filesystem, environment, network, +async, or lock I/O: `types.rs` and `protocol.rs` only ever receive and +return plain domain values — `prepare` takes the currently observed tree as +an explicit `TreeId` parameter rather than reading Git itself; `commit` +operates on the tree already captured in the prepared `AttemptState` +(`before_tree`/`after_tree`) and takes no tree input of its own. + +## Refinement decisions vs. the Quint model + +`spec/mutation_cursor.md` states the model's enumerated identities +(`WorktreeId`/`ScopeId`/`TreeId`/`EventId`/`AttemptId`) are bounded +verification domains only, and that "production code must support larger and +unbounded identifier spaces." This module refines each as an opaque +`String`-wrapping newtype rather than a fixed enum. + +Two consequences follow from that choice: + +- The Quint functions `scopeWorktree`/`scopeActor` are pure `match` tables + only because the model's `ScopeId` enum is pre-associated with a fixed + worktree/actor. Since `ScopeState` already carries `worktree_id`/ + `actor_kind` fields, this module refines them as accessor methods on + `ScopeState` instead of a lookup over `ScopeId`. +- `Boundary::Start`/`Advance`/`Close` carry only `scope`/`event`, exactly + like the Quint constructors (`spec/mutation_cursor.qnt:31-35`) — no + independent `worktree` field, so a boundary can never claim a worktree + inconsistent with its own scope's true assignment, a state the Quint type + cannot represent. `boundary_worktree(boundary, scopes: &BTreeMap)` resolves a hook boundary's worktree by reading the `ScopeId` + out of the boundary and looking up that exact key in `scopes`, mirroring + how `commitAttempt`/`prepareAvailable` (`spec/mutation_cursor.qnt:418,458`) + resolve it from `scopeWorktree(data.scope)` rather than from the boundary + itself. The Rust refinement does not accept an arbitrary `ScopeState` + alongside a boundary: the boundary's own `ScopeId` is the only key ever + used to look one up, preserving the Quint relationship + `scopeWorktree(boundary.scope)`. The result is `None` when that key is + absent from `scopes`; `Flush` carries its worktree directly and does not + consult `scopes` at all. +- `boundary_scope`/`boundary_event`/`boundary_event_key` return + `Option<_>` (`None` for `Flush`) rather than mirroring the Quint model's + arbitrary `Scope0`/`Event0` placeholder default. + +`ActorKind` and `FailureKind` stay fixed Rust enums: unlike the identity +types, they represent real, closed sets (supported harnesses; snapshot +health), not bounded verification domains. + +## Runtime scope materialization + +The Quint model's `SCOPES` universe is finite: `init` populates every +possible `ScopeId` with a `ScopeState` up front (`scopes' = +SCOPES.mapBy(scope => { status: NeverSeen, actorKind: scopeActor(scope), +worktreeId: scopeWorktree(scope) })`), so by the time any boundary is +evaluated, `scopeActor`/`scopeWorktree` already resolve for that scope — its +identity is a static fact of the model, not something a transition +establishes. + +This module's `ScopeId` is an unbounded runtime string (see "Refinement +decisions" above), so `ProtocolState.scopes` cannot be prepopulated with +every possible scope the way `init` does. Materializing a newly observed +scope's durable identity — `status: NeverSeen`, its `actor_kind`, and its +`worktree_id` — is therefore an **adapter/store responsibility, not a +protocol transition**: + +- Quint: a finite universe means every `ScopeState` value already exists at + `init`. +- Rust production: an unbounded identifier space means `ScopeState` is + lazily materialized by the persistence/adapter layer *before* the scope's + `ScopeId` is ever passed into `prepare`/`commit`. + +Before invoking the pure protocol with a hook boundary (`Start`/`Advance`/ +`Close`) that references a `ScopeId`, the surrounding coordinator/store +projection must ensure that scope already exists in `ProtocolState.scopes`. +`prepare`/`commit` do not infer identity from hook context, command type, or +any other heuristic: they never choose a default worktree, choose a default +actor, or synthesize a new `NeverSeen` scope. `boundary_worktree` returning +`None` for an unregistered scope, and `prepare`/`commit`'s resulting no-op, +are exactly this boundary — a missing `ScopeId` is unresolved protocol +input, not a scope the protocol may create. + +### Identity immutability + +Once a `ScopeId` is materialized, its `actor_kind` and `worktree_id` are +immutable identity facts for the lifetime of that scope. Only lifecycle +`status` transitions, exactly as the protocol already governs: + +```text +NeverSeen -> Active -> Closed +NeverSeen -> Closed +Active -> Abandoned +``` + +If a future adapter observes an existing `ScopeId` with a conflicting +`actor_kind` or `worktree_id`, that is an identity/protocol error to reject +and report — never a record to silently overwrite. This is the concrete +adapter-side half of `ScopeActorIdentityIsStable` (`spec/mutation_cursor.qnt`); +the protocol-side half is that no transition in `protocol.rs` ever writes +`actor_kind`/`worktree_id` (only `status` fields change). + +### Missing scope vs. `NeverSeen` scope + +These are not equivalent: + +- A **missing** `ScopeId` (absent from `ProtocolState.scopes`) means its + identity has not been materialized — invalid/unresolved protocol input. +- An **existing** `ScopeState { status: NeverSeen, .. }` is a known, + materialized scope identity that simply has not yet had an accepted + `Start`. + +The production entry path never calls `prepare`/`commit` with the first +case; the no-op behavior for a missing scope is a defensive kernel property, +not a path the coordinator is expected to exercise. + +## Runtime worktree materialization + +The same representation/refinement boundary applies to `WorktreeId`, one +level up from scope identity, and governs `taint`/`database_failure`/ +`abandon`/`recover`: + +- **Quint**: `WorktreeId` ranges over the finite `WORKTREES` universe, and + `init` materializes a `WorktreeState` for every member up front — every + `WorktreeId` already resolves before any action runs. This is why + `recordDatabaseFailure` (`spec/mutation_cursor.qnt:712-737`) states no + explicit worktree-existence guard: there is no state for it to guard + against. That omission is a fact about the closed, pre-populated Quint + domain, not evidence that an arbitrary unknown worktree is valid protocol + input. +- **Rust production**: `WorktreeId` is an unbounded opaque runtime string, so + `ProtocolState.worktrees` contains only worktrees a future coordinator/ + store layer has actually materialized. Every pure protocol action requires + its target `WorktreeId` to already exist in `ProtocolState.worktrees`; an + unknown `WorktreeId` is invalid/unresolved kernel input and causes a + defensive no-op, exactly as an unregistered `ScopeId` does for `prepare`/ + `commit`. The pure kernel never creates a `WorktreeState`, infers one, or + synthesizes a worktree from context. + +A **missing** `WorktreeId` (absent from `ProtocolState.worktrees`) is not +equivalent to a **healthy** `WorktreeState` (`tainted: false`, +`failure_kind: Healthy`, ...): the former means the protocol has no +materialized state for that identity at all, while the latter means the +identity is known and currently healthy. `taint`, `database_failure`, +`abandon`, and `recover` all enforce this distinction with the same existence +guard — `abandon` resolves it through the referenced scope's own materialized +`worktree_id` rather than taking a `WorktreeId` directly — which keeps +`external_taint ⊆ ProtocolState.worktrees` an invariant of every state this +module can produce, since `database_failure` is the sole path that inserts +into `external_taint`. + +Future responsibility split (mirrors "Runtime scope materialization" above): +the coordinator/store layer resolves/materializes worktree identity/state and +loads a `ProtocolState`; `protocol.rs` only transitions already-known ones. + +## Target end-state architecture + +The plan's file split anticipates three later seams this module does not yet +implement, recorded here so a later plan does not rediscover the layout: + +```mermaid +flowchart LR + coordinator["coordinator.rs\n(imperative shell:\nDB load, Git snapshot,\nCAS/retry, persist)"] + protocol["protocol.rs\n(pure transitions —\nprepare/commit/attribution/\ntaint/abandon/recover\nall implemented)"] + git_snapshot["git_snapshot.rs\n(isolated Git object store,\ntemporary index, tree capture/diff)"] + store["store.rs\n(cursor/revision, scopes,\nprocessed events, mutation\nevidence, CAS transaction)"] + + coordinator --> protocol + coordinator --> git_snapshot + coordinator --> store +``` + +Each seam's responsibility, once built: + +- **`coordinator.rs`** — receives hook/session identity, resolves the scope's + actor/worktree identity, asks `store.rs` to load or materialize the scope, + obtains a `ProtocolState`, and calls the pure protocol. +- **`store.rs`** — loads durable scope records; atomically creates a new + scope record as `NeverSeen` when appropriate; never remaps `actor_kind`/ + `worktree_id` for an existing `ScopeId` (see "Runtime scope + materialization" above). +- **`protocol.rs`** — assumes referenced scopes are already represented in + `ProtocolState.scopes`; validates and transitions lifecycle state only. + +`protocol.rs` stays free of any Git object, DB row, or CAS transaction concept +even with its full action set implemented; `coordinator.rs`/`git_snapshot.rs`/ +`store.rs` are not created by this plan. + +## Authoritative source + +`spec/mutation_cursor.qnt` (verified Quint model) and `spec/mutation_cursor.md` +(model-boundary/implementation-refinement notes) remain authoritative; doc +comments cite concrete spec line ranges per type/function. See +`context/plans/mutation-cursor-protocol-kernel.md` for build-out status. diff --git a/context/cli/mutation-trace-revision-refinement.md b/context/cli/mutation-trace-revision-refinement.md new file mode 100644 index 00000000..c2b966c3 --- /dev/null +++ b/context/cli/mutation-trace-revision-refinement.md @@ -0,0 +1,102 @@ +# Bounded revision refinement (`mutation_trace`) + +Part of the [mutation-cursor protocol module](mutation-trace-protocol.md). This file +covers one specific refinement gap between the Quint model and its Rust kernel: +worktree revision counters. + +## The gap + +`spec/mutation_cursor.qnt` models a worktree's `revision` as `int` +(`spec/mutation_cursor.qnt:39`) — an unbounded integer with no upper limit. The Rust +refinement uses `WorktreeState::revision: u64`. Every action that advances a +worktree's revision by one — `commit`, `taint`, `abandon`, `recover` — must therefore +handle the one case Quint's model cannot even express: a worktree already at +`revision: u64::MAX`. + +A raw `revision + 1` at that boundary wraps to `0` in release-mode Rust, which would +silently violate `MutationEventsHavePositiveRevision`, +`MutationEventUniquePerWorktreeRevision`, and every CAS-freshness assumption built on +revision monotonically increasing. + +## The refinement + +`protocol.rs` defines a private helper: + +```rust +fn next_revision(revision: u64) -> Option { + revision.checked_add(1) +} +``` + +Every revision-advancing site routes through it instead of a raw `+ 1`: + +- **`commit`** — revision headroom is required only for transitions that actually + advance the revision: + + ```text + commit: + non-Flush -> headroom required + Flush with observed change -> headroom required + Flush with no observed change -> no headroom required, even at u64::MAX + + taint / abandon / recover: + always advance when they execute -> headroom always required + ``` + + `ResolvedAttempt::evaluate` computes `would_advance_revision` (`!is_flush(boundary) || + tree_changed`) before deciding `accepted`, and only requires + `next_revision(worktree_state.revision).is_some()` when `would_advance_revision` is + true. A non-`Flush` boundary always advances revision when accepted, so it always + needs headroom. A `Flush` advances revision only when it observes a real tree change + (`advances_revision = accepted && (!is_flush(boundary) || observed_change)`), so a + fresh no-change `Flush` may commit at `revision: u64::MAX` — matching Quint's + `commitAttempt`, which accepts and commits that case without advancing revision. An + attempt that *would* overflow is rejected exactly like a stale one: no cursor + movement, no scope-lifecycle transition, no processed-`EventKey` insertion, no + `MutationEvent`. This decision is made before `ResolvedAttempt::apply` ever touches + state, so `commit` never discovers an overflow partway through applying a transition. + `apply` computes the checked `advanced_revision` only when `evaluation.advances_revision` + is true (`None` otherwise), reuses it for the worktree update, and reuses it again for + any emitted `MutationEvent`'s revision field — `changed` can only be true when + `advances_revision` is also true, so that reuse never has to synthesize a revision + for a non-advancing commit. +- **`taint`**, **`abandon`**, **`recover`** — each treats `next_revision` returning + `None` as an additional guarded no-op, alongside their existing existence/ + precondition guards (unknown worktree, already-tainted, non-live scope, and so on). + +## Why guard instead of document a precondition + +An earlier revision of the refinement matrix stated this only as an assumption +("callers must keep revision `< u64::MAX`") rather than enforcing it. That is unsound: +nothing in the type system or the pure kernel's own logic would have caught a caller +violating it, and a wrap is silent — no panic, no rejected attempt, just a `revision` +that jumps to `0` and re-enables CAS checks that should have stayed permanently stale. +Checked arithmetic makes the boundary executable instead of assumed. + +## Test coverage + +`tests.rs` has one no-wrap test per unconditionally-advancing action, each starting +from `revision: u64::MAX` and proving the guard holds rather than wrapping: + +- `taint_does_not_wrap_revision_at_u64_max` +- `abandon_does_not_wrap_revision_at_u64_max` +- `recover_does_not_wrap_revision_at_u64_max` + +`commit` gets two tests, together encoding that headroom is required for +advancement, not for acceptance in general: + +- `commit_that_would_advance_is_rejected_at_u64_max` — a `Start` boundary (always + advances revision when accepted) at `revision: u64::MAX` is rejected, not wrapped. +- `no_change_flush_commits_at_u64_max_without_advancing_revision` — a `Flush` + boundary observing no tree change at `revision: u64::MAX` commits successfully, + with `revision` staying at `u64::MAX` and no `MutationEvent` emitted. + +## Adapter responsibility + +In practice a worktree revision reaching `u64::MAX` is not expected to happen; this +guard exists so that if it ever did, the pure kernel fails safely (a guarded no-op or +rejection) rather than silently corrupting cursor/CAS state. No coordinator/store +behavior is implied by this file beyond passing through whatever the pure kernel +returns — a future adapter that observes a stuck (non-advancing) worktree at +`u64::MAX` would need its own operational response, which is out of scope for the +protocol kernel itself. diff --git a/context/context-map.md b/context/context-map.md index 5aaa2a05..ee598f9e 100644 --- a/context/context-map.md +++ b/context/context-map.md @@ -23,6 +23,8 @@ Feature/domain context: - `context/cli/config-precedence-contract.md` (implemented `sce config` show/validate command contract, deterministic `flags > env > config file > defaults` resolution order, focused `config/resolver.rs` ownership for config discovery/merge/runtime precedence plus default-discovered invalid-file degradation, focused `config/render.rs` ownership for `show`/`validate` text+JSON output construction, canonical `$schema` acceptance for startup-loaded `sce/config.json` files, shared auth-key env/config/optional baked-default support starting with `workos_client_id`, shared runtime resolution for flat logging observability keys including config-file/default `log_to_file`, `log_dir` / `SCE_LOG_DIR` with `/sce/logs` defaulting plus config-file/default-only positive `log_file_retention_limit`, config-file-only `agent_trace.repository_id`/`agent_trace.repository_remote` repository-identity keys with default remote `origin`, default-enabled `agent_trace.auto_sync` boolean resolution with explicit-false opt-out for the post-commit trigger boundary, the catalog-derived `integrations.optional_workflows` optional-workflow selection key, JSON-pointer-prefixed schema-validation errors, canonical Pkl-generated `sce/config.json` schema ownership plus CLI embedding/reuse contract including `policies.attribution_hooks.enabled` default-true/explicit-false opt-out metadata, config-file selection order, `show` provenance output, and trimmed `validate` output contract) - `context/cli/capability-traits.md` (current broad CLI capability seam in `cli/src/services/capabilities.rs`, including `FsOps`/`StdFsOps`, `GitOps`/`ProcessGitOps`, git root/hooks resolution behavior, compile-time-typed borrowed AppContext wiring with associated-type narrow capability accessors plus `ContextWithRepoRoot` repo-root-scoped context derivation, generic command execution bounds, and test-only unimplemented stubs; current service internals do not consume fs/git traits until later lifecycle migration tasks) - `context/cli/service-lifecycle.md` (current compile-safe lifecycle seam in `cli/src/services/lifecycle.rs`, including default no-op `ServiceLifecycle` diagnose/fix/setup methods against narrow `HasRepoRoot`, lifecycle-owned health/fix/setup result types with generic setup messages, doctor/setup adapter boundaries, the static `LifecycleProvider` enum catalog/dispatcher, hook/config/local_db/auth_db/agent_trace_db lifecycle providers including setup-time repository-scoped Agent Trace DB initialization plus checkout identity diagnostics, implemented doctor aggregation over diagnose/fix providers, and implemented setup aggregation over `setup` providers in order config → local_db → auth_db → agent_trace_db → hooks when requested) +- `context/cli/mutation-trace-protocol.md` (pure, dependency-free `cli/src/services/mutation_trace/` refinement of the verified `spec/mutation_cursor.qnt` mutation-cursor protocol: the full pure action set — `prepare`/`commit` transition logic, attribution/mutation-event materialization, snapshot-failure/database-failure taint actions, scope abandonment, and recovery with an explicit observed-tree input — plus cross-action sequence/invariant tests and a module-level Quint refinement matrix are all complete (`types.rs`, `protocol.rs`, `mod.rs`, `tests.rs`, registered with `#[allow(dead_code)]`); opaque-newtype identity refinement decisions vs. the Quint model's bounded enums, and the `coordinator.rs`/`git_snapshot.rs`/`store.rs` target end-state seams this layout leaves room for but does not create; not yet wired into any hook, command, or database call site) +- `context/cli/mutation-trace-revision-refinement.md` (the Quint `revision: int` → Rust `WorktreeState::revision: u64` bounded-integer refinement: the private `next_revision` checked-arithmetic helper `commit`/`taint`/`abandon`/`recover` all route through instead of a raw `+ 1`, so a worktree at `revision: u64::MAX` is a guarded no-op/rejection rather than a silent wrap to `0`) - `context/sce/cli-exit-code-contract.md` (stable class-based `sce` process exit-code contract in `cli/src/app.rs`, so automation can branch on failure category without parsing error text) - `context/sce/cli-error-code-taxonomy.md` (stable user-facing `SCE-ERR-*` diagnostic code classes rendered by `cli/src/app.rs`, complementing the numeric exit-code classes) - `context/sce/cli-stdout-stderr-contract.md` (implemented stream contract in `cli/src/app.rs`: command payloads on stdout only, redacted diagnostics on stderr) diff --git a/context/overview.md b/context/overview.md index 637ad8b8..686911f3 100644 --- a/context/overview.md +++ b/context/overview.md @@ -2,7 +2,7 @@ This repository maintains shared assistant configuration for OpenCode, Claude, Pi, and Codex from a single canonical Pkl authoring source. One typed workflow catalog owns the six workflows' shared identity and target routing metadata, while canonical workflow/phase modules own behavior and migrated package-local documents, and target renderers own formatting. Generated target layouts are ephemeral: repository builds consume a pre-Cargo generated payload through `SCE_CLI_GENERATED_INPUT_DIR`, crates.io and Flatpak stage packaging-only fallbacks, and `config/.opencode`, `config/.claude`, `config/.pi`, `config/.agents`, and the generated SCE config schema are not committed. The catalog also marks a workflow `optional` — currently only `brownfield` — which changes nothing about generation and is projected into a generated `config/optional-workflows.json` manifest for install-time consumers. `nix run .#pkl-check-generated` preserves its exact 141-path artifact, metadata/package, phase-reference, internal-reference, optional-workflow-manifest, workflow-orchestration, OpenCode-permission, required-path, and forbidden-path checks while delegating deterministic payload production and inventories to the shared generated-input producer; `nix flake check` runs the same contract. The target matrix contains one manual OpenCode profile plus Claude, Pi, and Codex; the former automated OpenCode profile has been removed. A fourth Pkl renderer, `config/pkl/renderers/codex-content.pkl`, also consumes the same canonical workflow composition to emit skills-only Codex output under `config/.agents/skills/**` (no per-target frontmatter, matching Pi, and no command/prompt layer). Each of the six catalog workflow skills (not `sce-decision`, which has no user-facing entrypoint on any target) additionally carries a Codex-only `agents/openai.yaml`, rendered by `config/pkl/renderers/codex-metadata.pkl` from the shared catalog's `title`/`description` plus an authored `default_prompt`, with `policy.allow_implicit_invocation: false` so these stateful lifecycle workflows activate only from explicit `$sce-` invocation or Codex's `/skills` discovery, never from conversational relevance alone. The Codex renderer also emits a Codex hook registration file (`config/.codex/hooks.json`) and its fail-open install-guidance hook script (`config/.codex/hooks/run-sce-or-show-install-guidance.sh`), both routing every registered lifecycle event through the single command `sce hooks codex`; the generated command resolves the Git root at invocation time and safely invokes the helper from nested cwd or spaced repository paths, failing open silently when Git-root resolution fails. `sce setup --codex` (and `--all`) now installs it as a fourth `SetupTarget`; setup merges the user-owned `.codex/hooks.json` through the shared structural Codex hook-config service, preserving unrelated valid handlers and rejecting malformed or Codex-invalid documents before the atomic swap. `sce doctor` diagnoses that file per required registration (`PresentAndCurrent`/`Missing`/`Stale`, or `Malformed` for the whole document) rather than by whole-document equality, and separately reports whether Codex has actually marked each structurally current registration trusted by reading (never writing) Codex's own `$CODEX_HOME/config.toml` hook-trust state; `sce doctor --fix` repairs structurally unhealthy registrations through the same merge service but never touches trust state (see `context/sce/doctor-human-text-contract.md`). `sce hooks codex` now exists as a typed dispatcher (`cli/src/services/hooks/codex/`): it parses the raw hook JSON into a `CodexHookEvent` and classifies `(hook_event_name, tool_name)` into `UserPromptSubmit`, `Stop`, `PreToolUse(Bash)`, `PostToolUse(apply_patch)`, or a fail-open `NoOp` fallthrough covering every other combination — including `apply_patch` under `PreToolUse`. `UserPromptSubmit` and `Stop` each capture one `messages`/`parts` row (`role="user"`/`role="assistant"`) into the repository Agent Trace DB under the idempotent `cx_` session prefix, `PreToolUse(Bash)` delegates to the existing Bash policy engine, and `PostToolUse(apply_patch)` parses Codex's own `apply_patch` text, resolves paths from the event `cwd` against the real Git root into safe repository-relative paths, normalizes Add/Update evidence into an SCE unified diff under deterministic event-scoped synthetic line identities derived from `tool_use_id`, and persists it as one `diff_traces` row when non-empty (see `context/sce/codex-integration-runtime.md`) — while invalid cwd/path resolution and malformed STDIN payloads fail open with empty stdout, reported model IDs are preserved without fabricated provider prefixes, and missing/blank apply_patch sessions produce no evidence. Delete-File operations and Bash-triggered filesystem mutations remain untracked for Codex. -It also includes a Rust CLI (`sce`) for Shared Context Engineering workflows: auth, config inspection, setup, doctor, Agent Trace hooks and synchronization, bash-policy evaluation, and repository-scoped Agent Trace storage infrastructure. See `context/architecture.md` for module-level boundaries and `context/context-map.md` for the full domain file index. +It also includes a Rust CLI (`sce`) for Shared Context Engineering workflows: auth, config inspection, setup, doctor, Agent Trace hooks and synchronization, bash-policy evaluation, and repository-scoped Agent Trace storage infrastructure. See `context/architecture.md` for module-level boundaries and `context/context-map.md` for the full domain file index. A new pure, dependency-free `cli/src/services/mutation_trace/` module now exists as a Rust refinement of the verified `spec/mutation_cursor.qnt` mutation-cursor protocol; it currently carries domain types and the full pure action set — `prepare`/`commit` transition logic, attribution/mutation-event materialization, snapshot-failure/database-failure taint actions, scope abandonment, and recovery with an explicit observed-tree input — is registered with `#[allow(dead_code)]`, and is not yet wired into any hook, command, or database call site (see `context/cli/mutation-trace-protocol.md`). The generated `/next-task` workflow persists task-level context-synchronization lifecycle state in each plan (`pending`, `synced`, or `blocked`) so unresolved task synchronization debt survives a session boundary and gates new implementation. Successful `/next-task` execution hands task synchronization an explicit, pre-edit-Git-baseline-relative changed-file list plus implementation, verification, done-check, plan-update, and context-impact evidence, recorded directly on the completed task (`Completed`, `Files changed`, `Result`, `Verify`, `Context impact`, `Context synchronization`); the five-file root context pass remains mandatory. A later-session sync-debt retry reads that same completed task record directly from the plan by plan path and task ID, with no separate persisted synchronization handoff. `/validate` is validation-only: it runs final checks, writes the Validation Report, and reports `validated`, `failed`, or `blocked` without plan-level context synchronization. diff --git a/context/plans/mutation-cursor-protocol-kernel.md b/context/plans/mutation-cursor-protocol-kernel.md new file mode 100644 index 00000000..dd04bf8c --- /dev/null +++ b/context/plans/mutation-cursor-protocol-kernel.md @@ -0,0 +1,1112 @@ +# Plan: mutation-cursor-protocol-kernel + +## Change summary + +Establish a pure, dependency-free Rust refinement of the verified `spec/mutation_cursor.qnt` +protocol under a new `cli/src/services/mutation_trace` module, split as `mod.rs` (public module +boundary), `types.rs` (state/domain types), `protocol.rs` (pure transition logic), and +`tests.rs`. The module represents the protocol's state as an explicit `ProtocolState` aggregate +(`worktrees`, `scopes`, `external_taint`, `processed_events`, `attempts`, `mutation_events`) over +the existing leaf types (`WorktreeState`, `ScopeState`, `AttemptState`), its pure transitions +(prepare/commit evaluation for `Start`/`Advance`/`Close`/`Flush` boundaries, attribution +derivation, snapshot-failure taint, database-failure external taint, scope abandonment, and +recovery — the last two taking the currently observed tree as an explicit input rather than +reading Git themselves), and its result/attribution/mutation-event types, with deterministic +tests that mirror the spec's invariants. This is new behavior: no Rust implementation of this +protocol exists today, and the module performs no Git, database, filesystem, environment, +network, or lock I/O. `coordinator.rs`, `git_snapshot.rs`, and `store.rs` — the imperative-shell +orchestration, isolated Git snapshot capture, and DB-backed CAS persistence seams in the target +end-state architecture — are acknowledged as the layout the protocol module will grow into, but +are not created in this PR; `protocol.rs` is not wired into any existing hook, command, or +database call site. That integration is explicitly out of scope and left for a later plan. + +This revision reshapes the T02-T07 task stack after a review of the first pass: it makes the +`accepted`/`observes`/`observedChange`/`changed`/`advancesRevision` distinction in `commitAttempt` +explicit per task (they are not equivalent — an accepted-but-non-observing hook still advances +the revision without moving the cursor), moves all four boundary kinds' commit evaluation +(including `Flush`) into one task instead of splitting `Flush` semantics across tasks, adds the +`externalTaint` freshness guard explicitly, requires attribution/mutation-event materialization +to use the *pre-transition* live-scope set exactly as `commitAttempt` computes it (before +`nextScope` is applied), and replaces "at least three" multi-action sequence tests with a +requirement to cover every named scenario. It does not change the module's scope, file layout, or +non-goals. + +## Acceptance criteria + +- [x] AC1: The mutation-cursor protocol module has an explicit Rust home under + `cli/src/services/mutation_trace` with zero Git/DB/filesystem/environment/network/ + async/lock I/O in its pure transition logic, and operates over an explicit `ProtocolState` + aggregate (`worktrees`/`scopes`/`external_taint`/`processed_events`/`attempts`/ + `mutation_events`) rather than free-floating leaf values. + - Validate: `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` returns nothing; manual inspection of imports and the `ProtocolState` type. +- [x] AC2: `Start`/`Advance`/`Close` hook boundaries and the non-hook `Flush` boundary compute + `accepted`/`observes`/`observedChange`/`changed`/`advancesRevision` and transition scope + status and worktree cursor/revision exactly as `commitAttempt` specifies + (`spec/mutation_cursor.qnt:455-661`), including CAS freshness rejection + (`expectedRevision`/`beforeTree` mismatch), the `externalTaint` freshness guard, and replay + rejection via processed `EventKey`s. An accepted-but-non-observing hook (for example a + fresh `Start` on an already-`Active` scope, or an invalid `Advance`/`Close`) still advances + the revision and records the event as processed while the cursor and scope remain + unchanged; `Flush`'s `advancesRevision` requires `observedChange`, unlike hook boundaries + whose `advancesRevision` follows from `accepted` alone. `prepare` takes the currently + observed tree as an explicit input parameter rather than obtaining it itself. + - Validate: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` +- [x] AC3: Attribution (`IneligibleUnscoped`/`AiExclusive`/`AiContended`, + `spec/mutation_cursor.qnt:285-301`) and mutation-event emission match `commitAttempt`'s + `changed` gate exactly (`observedChange and not needsRebaseline`), computed from the + *pre-transition* live-scope set exactly as `commitAttempt` computes `live`/`attribution` + before applying `nextScope` — a `Start` boundary's emitted event never attributes the + mutation to the scope it is about to activate, and a `Close` boundary's emitted event still + attributes to the scope it is about to close — including the `Flush` boundary and + failure/taint/`needsRebaseline` attribution overrides. + - Validate: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` +- [x] AC4: Snapshot-failure taint (`taintHealthy`/`taint`, `spec/mutation_cursor.qnt:663-710`) + changes only `tainted`/`failureKind`/`revision`; database failure + (`recordDatabaseFailure`/`databaseFailure`, `spec/mutation_cursor.qnt:712-737`) changes + only `externalTaint`. Neither ever changes the cursor. + - Validate: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` +- [x] AC5: Abandonment (`abandonLiveScope`/`abandon`, `spec/mutation_cursor.qnt:739-805`) is + terminal, sets `needsRebaseline`, never moves the cursor, and preserves the scope's + `actor_kind` and `worktree_id` (scope identity stability); a terminal scope can never be + reactivated or abandoned again, and abandoning a `NeverSeen`, `Closed`, or `Abandoned` + (non-live) scope is a no-op. + - Validate: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` +- [x] AC6: Recovery (`recoverNeeded`/`recover`, `spec/mutation_cursor.qnt:807-886`), given the + currently observed tree as an explicit input rather than reading Git itself, re-baselines + the cursor to that observed tree and clears taint/`needsRebaseline`/`externalTaint`, + abandoning live scopes only on the taint/`externalTaint` recovery path and preserving them + on the `needsRebaseline`-only path. + - Validate: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` +- [x] AC7: No rejected or stale attempt ever advances the revision, moves the cursor, or emits + mutation evidence, across multi-action sequences. + - Validate: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` (sequence/invariant tests from T07) +- [x] AC8: The formal specification stays untouched and green, and no existing production code + path calls the new module. + - Validate: `git diff --stat spec/mutation_cursor.qnt` is empty; `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` finds no call sites; `nix run .#quint -- typecheck spec/mutation_cursor.qnt && nix run .#quint -- test spec/mutation_cursor.qnt` + +### Full validation + +- `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml` +- `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` +- `cargo fmt --manifest-path cli/Cargo.toml -- --check` +- `nix run .#quint -- typecheck spec/mutation_cursor.qnt` +- `nix run .#quint -- test spec/mutation_cursor.qnt` + +### Context sync + +- `context/context-map.md` (new domain-file entry for the mutation-cursor protocol module) +- `context/cli/mutation-trace-protocol.md` (new domain file: `mutation_trace` module + responsibility and file layout, Quint refinement scope, explicit "not yet wired into + production" status, and the target end-state directory layout — `coordinator.rs`, + `git_snapshot.rs`, `store.rs` as the seams later PRs will fill in — so later plans have a + recorded architecture to build against instead of rediscovering it) +- `context/overview.md` (brief mention: new pure protocol module exists, not yet integrated) + +## Task context synchronization lifecycle + +Persist this field in every plan; this is durable plan state, not chat state: + +- **Task context synchronization:** every task carries `pending | synced | blocked`. + A completed task must be `synced` before another task can start or the plan can + finish. +- For `blocked`, record **Blocker**, **Required action**, and **Retry condition** beside the + status. Never infer `synced` from conversation history; write every lifecycle transition to + the plan file. + +## Constraints and non-goals + +- **In scope:** `cli/src/services/mutation_trace/` (new module: `mod.rs`, `types.rs`, + `protocol.rs`, `tests.rs`), `cli/src/services/mod.rs` (module registration only). +- **Out of scope:** `spec/mutation_cursor.qnt` / `spec/mutation_cursor.md` (read-only, + authoritative — no edits); `cli/src/services/agent_trace.rs`, + `cli/src/services/agent_trace_db/`, `cli/src/services/hooks/**` (no behavior changes — these + remain untouched); `coordinator.rs`, `git_snapshot.rs`, `store.rs` (the imperative-shell + orchestration, isolated Git snapshot capture, and DB-backed CAS persistence seams of the + target architecture — acknowledged in context but not created); any Git, SQLite, filesystem, + or hook wiring; a Quint-driven property-based testing harness; the `SCE_LAST_ACCEPTED_COMMIT` + file or any cursor-persistence adapter. +- **Constraints:** no new Cargo dependencies (`cli/Cargo.toml` has no `proptest`/`quickcheck` + today, and the request itself discourages adding dependency churn for this PR); the protocol + core stays synchronous with no `tokio`, `Arc>`, `RwLock<_>`, or file locks; follow + repository domain-type and test-module conventions (see `cli/src/services/patch.rs`: plain + enums/structs, `#[cfg(test)] mod tests;` sibling file) and the `#[allow(dead_code)]` + precedent for modules not yet consumed by production call sites (`agent_trace_export`, + `bash_policy`, `repository_identity` in `cli/src/services/mod.rs`); `types.rs` and + `protocol.rs` stay free of any reference to `coordinator.rs`/`git_snapshot.rs`/`store.rs` + concerns (Git objects, DB rows, CAS transactions) — the protocol layer only ever receives and + returns plain domain values, including the observed-tree inputs to `prepare` and `recover`, + which are plain `TreeId` values supplied by the caller. +- **Non-goal:** wiring this protocol into any hook, command, or database layer; Git/SQLite/ + filesystem adapters for its inputs; a full Rust-vs-Quint model/PBT test harness; implementing + `coordinator.rs`, `git_snapshot.rs`, or `store.rs`. + +## Assumptions + +- The request's illustrative Quint-concept examples (generation capture/consumption, + `AI`/`Human`/`SkipConcurrent`/`AlreadyProcessed`/`NoMutation`/`PrePublishFailure`/ + `PublishFailure`/`AnchorFailure`/`CursorFailure` result branches, `Begin`/`End` agent scopes, + base/next cursor boundaries) describe an earlier or hypothetical shape of the protocol. The + current `spec/mutation_cursor.qnt` on `main` models a different, more evolved state machine: + `WorktreeId`/`ScopeId`/`TreeId` CAS-based cursor commits (`worktrees.revision`/`cursorTree`), + a `NeverSeen`/`Active`/`Closed`/`Abandoned` scope lifecycle, `tainted`/`externalTaint`/ + `needsRebaseline` failure/recovery state, and `IneligibleUnscoped`/`AiExclusive`/ + `AiContended` attribution. Per the request's own instruction ("If the Quint file has changed + since this prompt was written, follow the current file"), this plan is authored against the + actual current spec, and every task below cites concrete `spec/mutation_cursor.qnt` line + ranges rather than the request's illustrative names. +- `cli/src/commands/hooks/event_processing.rs`, named in the request as an inspection target, + does not exist in this repository — there is no `cli/src/commands` directory at all. Hook + dispatch instead lives under `cli/src/services/hooks/` (e.g. `mod.rs`, `command.rs`, + `codex/`). This plan treats that directory as the equivalent inspection target and leaves it + unmodified per the non-goals above. +- No `proptest`/`quickcheck`-family dependency exists in `cli/Cargo.toml` today. Per the + request's own guidance not to add dependency/infrastructure churn to claim PBT coverage, this + plan shapes the API for later property testing (plain functions over explicit state/input/ + outcome types) without adding a new test dependency now. +- Module location and name: `cli/src/services/mutation_trace/` (not `mutation_cursor`, per + user correction), registered in `cli/src/services/mod.rs` with `#[allow(dead_code)]`, + matching the existing precedent for modules not yet consumed by production call sites. The + spec file itself stays `spec/mutation_cursor.qnt`/`.md` — only the Rust module is renamed; + the plan's line-range citations against the spec are unaffected. Internal PR-1 file split is + `mod.rs` / `types.rs` / `protocol.rs` / `tests.rs`, matching the user-supplied target + architecture; `coordinator.rs` (imperative shell: DB load, Git snapshot, call protocol, + CAS/retry, persist), `git_snapshot.rs` (isolated Git object store / temporary index / tree + capture and diff), and `store.rs` (protocol persistence interface: cursor/revision, scopes, + processed events, mutation evidence, CAS transaction) are the later-PR seams this layout + leaves room for, and are recorded in the new context file but not created here. +- `ProtocolState` (T02) is a plain aggregate of the existing leaf types keyed by their identity + newtypes (`BTreeMap`, `BTreeMap`, + `BTreeSet` for `external_taint`, `BTreeSet` for `processed_events`, + `BTreeMap` for `attempts`, `BTreeSet` for + `mutation_events`), mirroring the Quint state machine's top-level `worktrees`/`scopes`/ + `externalTaint`/`processedEvents`/`attempts`/`mutationEvents` variables + (`spec/mutation_cursor.qnt:2-14`). Quint's verification-only histories (`cursorHistory`, + `protocolHistory`, `scopeHistory`, `abandonHistory`, `startHistory`, `recoveryHistory`, + `taintHistory`, `evidenceAttempts`, `scopeStartCount`, `everTerminal`) are not represented in + `ProtocolState`; T07's refinement matrix records them as verification-only. + `BTreeMap`/`BTreeSet` are chosen over `HashMap`/`HashSet` for deterministic iteration order in + tests, matching the repository's existing `BTreeMap` usage in `cli/src/services/patch.rs`. +- `prepare` and `recover` take the currently observed tree as an explicit `TreeId` parameter + (`prepare(state, attempt, boundary, observed_tree)`, `recover(state, worktree, observed_tree)`) + rather than reading it internally, because the pure kernel must not perform Git I/O; the + observed tree corresponds to Quint's `worktreeTrees.get(worktree)`, which a future + `git_snapshot.rs`/`coordinator.rs` adapter will supply from real Git state. +- **Runtime scope materialization is an adapter/store responsibility, not a protocol + transition.** The Quint model's `SCOPES` universe is finite and every `ScopeState` entry is + created by `init` (`scopes' = SCOPES.mapBy(scope => { status: NeverSeen, actorKind: + scopeActor(scope), worktreeId: scopeWorktree(scope) })`), so `scopeActor`/`scopeWorktree` + already resolve for any `ScopeId` before any boundary is evaluated. This refinement's + `ScopeId` is an unbounded runtime string (see the identity-refinement assumption above), so + `ProtocolState.scopes` cannot be prepopulated the way `init` does. Before the surrounding + coordinator/store projection calls `prepare` with a hook boundary (`Start`/`Advance`/`Close`) + referencing a `ScopeId`, it must ensure that scope already exists in `ProtocolState.scopes` + with its durable identity — `status: NeverSeen`, the correct `actor_kind`, and the correct + `worktree_id`. Once a `ScopeId` exists, its `actor_kind`/`worktree_id` association is + immutable for the lifetime of that scope: the pure protocol never invents, remaps, or + implicitly materializes scope identity, and a future adapter that observes an existing + `ScopeId` with a conflicting `actor_kind`/`worktree_id` must treat that as an + identity/protocol error rather than silently overwriting the record. A missing `ScopeId` is + therefore not equivalent to a `NeverSeen` one: a missing entry means identity has not been + materialized (invalid/unresolved protocol input, which `prepare`/`commit` already handle as a + no-op — see T02's Result), while an existing `ScopeState { status: NeverSeen, .. }` is a known, + materialized scope identity that simply has not yet had an accepted `Start`. Once built, + `coordinator.rs` receives hook/session identity, resolves the scope's actor/worktree identity, + asks `store.rs` to load or materialize the scope, obtains a `ProtocolState`, and calls the + pure protocol; `store.rs` loads durable scope records and atomically creates a new one as + `NeverSeen` when appropriate, but never remaps `actor_kind`/`worktree_id` for an existing + `ScopeId`; `protocol.rs` assumes referenced scopes are already represented and only validates/ + transitions lifecycle state (see `context/cli/mutation-trace-protocol.md`, "Runtime scope + materialization", for the full contract). Future `coordinator.rs`/`store.rs` integration tests + (not implemented by this plan) must cover: a new scope's materialization producing exactly + `{ status: NeverSeen, actor_kind, worktree_id }`; idempotent re-materialization of an + already-known identical `(ScopeId, actor_kind, worktree_id)` never resetting an `Active`/ + `Closed`/`Abandoned` scope back to `NeverSeen`; rejection of a conflicting `actor_kind` for an + existing `ScopeId`; rejection of a conflicting `worktree_id` for an existing `ScopeId`; and + preservation of lifecycle status across identity materialization/checking in every case. + +## Task stack + +- [x] T01: `Establish mutation-trace module skeleton and pure domain types` (status:done) + - Task ID: T01 + - Scope: In — create `cli/src/services/mutation_trace/` with `mod.rs` (public module + boundary) and `types.rs`; register the module in `cli/src/services/mod.rs` with + `#[allow(dead_code)]`; define Rust types in `types.rs` refining `WorktreeId`, `ScopeId`, + `TreeId`, `EventId`, `AttemptId`, `EventKey`, `FailureKind`, `ScopeStatus`, `AttemptStatus`, + `Attribution`, `Boundary`, `WorktreeState`, `ScopeState`, `AttemptState`, and + `MutationEvent` (`spec/mutation_cursor.qnt:2-117`); pure constructors/accessors mirroring + `scopeWorktree`, `scopeActor`, `isLive`, `isTerminal`, `boundaryWorktree`, `boundaryScope`, + `boundaryEvent`, `boundaryEventKey`, `isHook`/`isStart`/`isAdvance`/`isClose`/`isFlush` + (`spec/mutation_cursor.qnt:151-245`); add a `tests.rs` skeleton wired via + `#[cfg(test)] mod tests;` in `mod.rs`. Out — commit/prepare transition logic (T02), + attribution/mutation-event derivation (T03), taint/failure/abandon/recovery actions + (T04-T06), `coordinator.rs`/`git_snapshot.rs`/`store.rs` (not this plan). + - Dependencies: none + - Done when: the module compiles, exposes the listed types with no Git/DB/FS/env/network/ + lock/async imports, and each type/free function carries a doc comment naming its Quint + counterpart. + - Verify: `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml`; `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace`. + - Context synchronization: synced + - Completed: 2026-08-26 + - Files changed: + - `cli/src/services/mod.rs` (registered `pub mod mutation_trace;` with `#[allow(dead_code)]`) + - `cli/src/services/mutation_trace/mod.rs` (new; module doc comment corrected post-review, see below) + - `cli/src/services/mutation_trace/types.rs` (new; corrected post-review, see below) + - `cli/src/services/mutation_trace/tests.rs` (new; corrected post-review, see below) + - Result: Added the `mutation_trace` module skeleton with all state/domain types + (`WorktreeId`/`ScopeId`/`TreeId`/`EventId`/`AttemptId`/`EventKey`/`ActorKind`/ + `FailureKind`/`ScopeStatus`/`AttemptStatus`/`Attribution`/`Boundary`/`WorktreeState`/ + `ScopeState`/`AttemptState`/`MutationEvent`) and pure accessors + (`is_live`/`is_terminal`/`ScopeState::scope_worktree`/`ScopeState::scope_actor`/ + `boundary_worktree`/`boundary_scope`/`boundary_event`/`boundary_event_key`/`is_hook`/ + `is_start`/`is_advance`/`is_close`/`is_flush`), each with a doc comment naming its Quint + counterpart and line range. No production call site references the module. One approved + local design decision remains (recorded in Assumptions below): identity types + (`WorktreeId`/`ScopeId`/`TreeId`/`EventId`/`AttemptId`) are opaque `String`-wrapping + newtypes rather than the Quint model's fixed enums. + **Post-review correction 1 (PR #238 review):** the original `Boundary` shape gave + `Start`/`Advance`/`Close` an independent `worktree: WorktreeId` field so + `boundary_worktree` could stay a pure function of `Boundary` alone. This was unfaithful: + the Quint `Boundary` type (`spec/mutation_cursor.qnt:31-35`) never stores a worktree for a + hook boundary — `boundaryWorktree` always derives it from `scopeWorktree(data.scope)` — and + `spec/mutation_cursor.qnt:418,458` confirm `commitAttempt`/`prepareAvailable` resolve + `worktree` from the boundary before any scope lookup, so a stored worktree that could + diverge from the boundary's own scope would let a caller act on the wrong worktree's state, + a state the Quint type cannot represent. Fixed: `Boundary::Start`/`Advance`/`Close` now + carry only `scope`/`event`, field-for-field with the Quint constructors; `Flush` is + unchanged. + **Post-review correction 2 (PR #238 review):** correction 1's + `boundary_worktree(boundary, scope: Option<&ScopeState>)` still let a caller pass an + arbitrary `ScopeState` alongside the boundary with no proof it belonged to the boundary's + own `scope` — a test literally constructed `Boundary::Start { scope: scope0, .. }` alongside + an unrelated `ScopeState { worktree_id: wt1, .. }` and got `wt1` back. Fixed: the signature + is now `boundary_worktree(boundary, scopes: &BTreeMap)`; for + `Start`/`Advance`/`Close` it reads the `ScopeId` out of the boundary and looks up that exact + key in `scopes` (returning `None` when the key is absent), so the boundary's own scope is + the only key ever used — no parameter lets a caller inject a worktree independent of it. + `Flush` is unaffected (it carries its own worktree and ignores `scopes`). `tests.rs` was + rewritten: the misleading `boundary_worktree_reflects_the_scopes_own_worktree_not_a_guess` + test (which had proved the bug) was replaced with tests keyed off a two-scope map spanning + two worktrees, proving each hook boundary resolves via its own `scope` regardless of what + else is in the map, that a missing scope yields `None`, and that `Flush` ignores the map + entirely. `mod.rs`'s module doc comment was also reworded to drop task/plan references + (repository convention: source comments should not cite the current task, fix, or PR). + - Verify outcomes: + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed. + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 14/14 tests (10 original + 3 from correction 1 + 1 net add from correction 2's rewrite). + - `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` — + no matches (AC1 spot-check). + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` — passed, no warnings. + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed, no diff. + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed. + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed. + - `git diff -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty (spec untouched). + - Context impact: Classification: minor. A new, currently-unreferenced module exists under + `cli/src/services/`; no existing behavior, hook, or command changed. Context synchronized + in the same session as implementation: `context/cli/mutation-trace-protocol.md` (new domain + file), `context/context-map.md` (new entry), and `context/overview.md` (one-sentence + mention) were all updated at T01 completion; this correction pass updated the domain file's + description of the `boundary_worktree` refinement to match the keyed-lookup design. + +- [x] T02: `Implement the protocol aggregate state, explicit observation inputs, and prepare/commit evaluation for every boundary` (status:done) + - Task ID: T02 + - Scope: In — + - In `types.rs`, define the `ProtocolState` aggregate (`worktrees`, `scopes`, + `external_taint`, `processed_events`, `attempts`, `mutation_events`) described in + Assumptions, mirroring the Quint state machine's top-level state variables + (`spec/mutation_cursor.qnt:2-14`). Verification-only Quint histories are not represented. + - In `protocol.rs`, `prepare` refining `prepareAvailable`/`prepare` + (`spec/mutation_cursor.qnt:417-453`), taking the currently observed tree as an explicit + `TreeId` input (e.g. `prepare(state, attempt, boundary, observed_tree)`) rather than + reading it internally; `observed_tree` corresponds to Quint's + `worktreeTrees.get(worktree)` at the boundary's resolved worktree. + - In `protocol.rs`, a commit-evaluation function refining `commitAttempt` + (`spec/mutation_cursor.qnt:455-661`) for **all four** boundary kinds (`Start`, `Advance`, + `Close`, `Flush`) in one pass: compute `accepted` (`fresh`: prepared status, worktree not + in `external_taint`, `expectedRevision == revision`, `beforeTree == cursorTree`, and for + hook boundaries the `EventKey` not already in `processed_events`), `observes` (`Start` + requires `NeverSeen`; `Advance` requires live; `Close` accepts `NeverSeen` or live; + `Flush` is always `true`), `observedChange` (`accepted and observes and beforeTree != + afterTree`), `changed` (`observedChange and not needsRebaseline` — expose this as a + computed flag but do **not** construct a `MutationEvent` from it; that is T03's job), and + `advancesRevision` (`accepted and (not isFlush(boundary) or observedChange)`); apply scope + lifecycle transitions (`NeverSeen`→`Active` on accepted `Start`, →`Closed` on accepted + `Close`), cursor advancement (`afterTree` when `observes and not needsRebaseline`, + otherwise unchanged), attempt status transitions (`Prepared`→`Committed` on `accepted`, + →`Rejected` otherwise), and processed-`EventKey` recording for accepted hook boundaries. + - Tests land in `tests.rs`. + - Out — attribution derivation and `MutationEvent` materialization (T03); taint/ + database-failure/abandon/recovery actions (T04-T06). + - Dependencies: T01 + - Done when: + - a state-sequence test proves prepare→commit accepts a fresh `Start`, rejects a + stale-revision or stale-`beforeTree` attempt without mutating worktree/scope/cursor + state, rejects a replayed `EventKey`, rejects an attempt whose worktree is in + `external_taint` even with a fresh revision/`beforeTree`, and transitions scope status + correctly for `Start` and `Close`; + - a test proves an accepted-but-non-observing hook — a fresh `Start` on an already-`Active` + scope, and the equivalent invalid `Advance`/`Close` cases — results in: attempt → + `Committed`, event key → processed, revision → increments, cursor → unchanged, scope → + unchanged, and `changed` is `false`; + - a test proves `Flush`'s `advancesRevision` is `false` when `observedChange` is `false` + (a no-op tree), distinguishing it from hook boundaries whose `advancesRevision` follows + from `accepted` alone. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace`. + - Context synchronization: synced + - Completed: 2026-08-26 + - Files changed: + - `cli/src/services/mutation_trace/types.rs` (added `ProtocolState`; added `Ord`/`PartialOrd` + derives to `FailureKind`, `Attribution`, `Boundary`, `MutationEvent` so `MutationEvent` can + live in a `BTreeSet`) + - `cli/src/services/mutation_trace/protocol.rs` (new; `prepare`, `commit`, `CommitEvaluation`, + `CommitOutcome`, and the private `ResolvedAttempt` helper) + - `cli/src/services/mutation_trace/mod.rs` (registered `pub mod protocol;`; module doc comment + updated to reflect that transition logic now exists) + - `cli/src/services/mutation_trace/tests.rs` (11 new tests for `prepare`/`commit`; added + `attempt_id`/`healthy_worktree`/`scope_with_status` builders) + - Result: Implemented `ProtocolState` (`worktrees`/`scopes`/`external_taint`/`processed_events`/ + `attempts`/`mutation_events`) and, in `protocol.rs`, `prepare` (refining + `prepareAvailable`/`prepare`, taking the observed tree as an explicit `TreeId` parameter) and + `commit` (refining `commitAttempt`) for all four boundary kinds in one pass. `commit` is split + into a private `ResolvedAttempt` helper (`resolve`/`evaluate`/`apply`) to stay under Clippy's + line-count lint; `evaluate` returns a `CommitEvaluation` (`accepted`/`observes`/ + `observed_change`/`changed`/`advances_revision`) that `apply` and T03 both consume, so + `changed` is exposed as a computed flag without constructing a `MutationEvent` — `commit` + leaves `mutation_events` untouched, as scoped. The scope-transition guards for `Start`/`Close` + reuse `evaluate`'s own `observes` flag rather than re-deriving the same `NeverSeen`/live check + a second time, since the two are provably identical per `commitAttempt`'s own definition of + `observes`. `prepare` and `commit` are no-ops (state unchanged, evaluation flags all `false`) + when the boundary's worktree cannot be resolved (an unregistered scope for a hook boundary) or + has no durable state — an attempt only reaches `commit` via a successful `prepare`, which + already refuses to prepare against an unresolvable worktree, so this is a defensive default + rather than a path any required test exercises. No production call site references the + module. + **Post-review clarification (PR #238 review):** `prepare(Start/Advance/Close)` requires the + referenced `ScopeId` to already exist in `ProtocolState.scopes`; unknown scopes are not + materialized by the protocol. This is intentional, not a gap — runtime scope materialization + is an adapter/store responsibility, not a protocol transition (see Assumptions: "Runtime + scope materialization is an adapter/store responsibility, not a protocol transition"). No + code changed for this clarification: the existing `prepare`/`commit` no-op behavior for an + unresolvable worktree (an unregistered scope for a hook boundary), described above, already + matches this contract exactly; only the contract itself was made explicit. + - Verify outcomes: + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 25/25 tests (14 from T01 + 11 new: fresh `Start` activation, `Close` scope transition, stale + revision/`beforeTree` rejection, replay rejection, external-taint rejection, three + accepted-but-non-observing cases — `Start` on `Active`, `Advance` on `NeverSeen`, `Close` on + `Abandoned` — and two `Flush` cases proving `advancesRevision` requires `observedChange` + unlike hook boundaries). + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed. + - `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` — no + matches (AC1 spot-check). + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` + — passed after splitting `commit` (`too_many_lines`), allowing + `clippy::struct_excessive_bools` on `CommitEvaluation` (precedented at + `cli/src/services/setup/mod.rs:194`), and replacing a redundant closure with a method + reference. + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed, no diff (after running + `cargo fmt`). + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed. + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed. + - `git diff --stat -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty (spec + untouched). + - `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` — no + matches (AC8 spot-check). + - Context impact: Classification: domain. `protocol.rs` is new pure transition logic added to an + already-unreferenced module; no existing behavior, hook, or command changed. Synchronized in + the same session as implementation: `context/cli/mutation-trace-protocol.md` (Current + state/Module layout/target-architecture sections updated to describe `protocol.rs`'s + `prepare`/`commit`), `context/context-map.md` (summary line updated), and `context/overview.md` + (one-line mention corrected) — all three were stale, describing the module as types-only. + `context/architecture.md`, `context/glossary.md`, and `context/patterns.md` were verified and + found not contradicted; no edit needed. No qualifying architecture decision. + +- [x] T03: `Implement attribution and mutation-event materialization from pre-transition live scopes` (status:done) + - Task ID: T03 + - Scope: In — in `protocol.rs`, a pure function refining `attributionFor` + (`spec/mutation_cursor.qnt:285-301`) computing `IneligibleUnscoped`/`AiExclusive(scope)`/ + `AiContended` from live scopes plus worktree `failureKind`/`externalTaint`/ + `needsRebaseline`; wire `MutationEvent` construction (refining `mkMutationEvent`, + `spec/mutation_cursor.qnt:303-323`) into T02's commit evaluation, gated by the `changed` + flag T02 already computes. Compute `live`/`attribution` from the **pre-transition** scope + set exactly as `commitAttempt` computes them — before `nextScope` is applied + (`spec/mutation_cursor.qnt:484-485` precede the `nextScope` `val` at line 530): a `Start` + boundary's emitted event never attributes the mutation to the scope it is about to + activate (that scope is not yet counted as live), and a `Close` boundary's emitted event + still attributes to the scope it is about to close (that scope is still counted as live). + Tests land in `tests.rs`. Out — taint/failure/abandon/recovery state changes (T04-T06); no + new commit boundary or `Flush` semantics (already covered by T02). + - Dependencies: T02 + - Done when: tests prove zero/one/multiple pre-transition live scopes map to the three + attribution variants; an unhealthy `failureKind`/external taint/`needsRebaseline` forces + `IneligibleUnscoped` even with active scopes; a no-op tree change emits no mutation event; a + real change emits exactly one event carrying the correct attribution/boundary/revision; a + `Start` on a `NeverSeen` scope that also observes a change emits an event whose attribution + excludes the newly-activated scope; a `Close` on the sole live scope that also observes a + change emits an event whose attribution still counts that scope as live. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace`. + - Context synchronization: synced + - Completed: 2026-08-26 + - Files changed: + - `cli/src/services/mutation_trace/protocol.rs` (added `live_scopes_on`, `attribution_for`; + wired `MutationEvent` materialization into `ResolvedAttempt::apply`, gated by + `evaluation.changed`; updated `commit`/`CommitEvaluation` doc comments to reflect that + mutation-event materialization is now implemented, and dropped stale `T03`-referencing + comment text per repository convention) + - `cli/src/services/mutation_trace/tests.rs` (11 new tests: `live_scopes_on` filtering; + `attribution_for`'s zero/one/multiple-live-scope and + unhealthy/externally-tainted/needs-rebaseline-forces-`IneligibleUnscoped` cases; `commit` + emitting no event on a no-op tree change, exactly one event with correct + attribution/boundary/revision on a real change via `Advance` (which does not itself alter + the scope set), `Start` on `NeverSeen` excluding the newly-activated scope from + attribution, and `Close` on the sole live scope still counting it as live) + - Result: Added `live_scopes_on(state, worktree)` (refining `liveScopesOn`, + `spec/mutation_cursor.qnt:265-269`, filtering the known `state.scopes` map by + `worktree_id`/`is_live()` since this refinement has no fixed `SCOPES` universe to filter) and + `attribution_for(state, worktree)` (refining `attributionFor`, + `spec/mutation_cursor.qnt:285-301`) to `protocol.rs`, both `pub` so `tests.rs` can exercise + them directly as pure functions. Wired `MutationEvent` construction (refining + `mkMutationEvent`, `spec/mutation_cursor.qnt:303-323`) into `ResolvedAttempt::apply`, + inserted into `next.mutation_events` when `evaluation.changed`, computed by calling + `live_scopes_on`/`attribution_for` against `apply`'s own `state: &ProtocolState` parameter — + the pre-transition state `commit` passes through unmutated, since `apply` clones it into + `next` and only ever mutates `next` — matching `commitAttempt`'s own `live`/`attribution` + computation at `spec/mutation_cursor.qnt:484-485`, which precedes the `nextScope` `val` at + line 530. No new fields were added to `CommitEvaluation`; `changed` (already computed by T02) + is the sole gate, per the task's own scope. No production call site references the module. + - Verify outcomes: + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 36/36 tests (25 from T01+T02 + 11 new). + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed. + - `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` — + no matches (AC1 spot-check). + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` + — passed, no warnings. + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed, no diff (after running + `cargo fmt`). + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed. + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed. + - `git diff --stat -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty (spec + untouched, AC8 spot-check). + - `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` — no + matches (AC8 spot-check). + - Context impact: Classification: domain. `attribution_for`/`live_scopes_on`/mutation-event + materialization are new pure logic added to an already-unreferenced module; no existing + behavior, hook, or command changed. + +- [x] T04: `Implement snapshot-failure taint and database-failure external-taint actions` (status:done) + - Task ID: T04 + - Scope: In — in `protocol.rs`, pure transitions refining `taintHealthy`/`taint` + (`spec/mutation_cursor.qnt:663-710`) and `recordDatabaseFailure`/`databaseFailure` + (`spec/mutation_cursor.qnt:712-737`): taint sets `tainted=true`, + `failureKind=SnapshotFailure`, advances revision, leaves `cursorTree`/`needsRebaseline` + untouched, and is a guarded no-op when already tainted or externally tainted; database + failure adds the worktree to `externalTaint` only, touching no other durable worktree/scope + field, and is a guarded no-op when already externally tainted; tests land in `tests.rs`. + Out — abandonment (T05), recovery (T06). + - Dependencies: T02 (taint/database-failure semantics do not depend on attribution or + mutation-event materialization) + - Done when: tests prove `taint` changes exactly `tainted`/`failureKind`/`revision` and + nothing else, `databaseFailure` changes exactly `externalTaint` and leaves every other + durable worktree/scope field equal to before, and both actions are no-ops on an + already-tainted/already-externally-tainted worktree. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace`. + - Context synchronization: synced + - Completed: 2026-08-26 + - Files changed: + - `cli/src/services/mutation_trace/protocol.rs` (added `taint`, `database_failure`; updated + module doc comment to cite `spec/mutation_cursor.qnt:663-737`) + - `cli/src/services/mutation_trace/tests.rs` (7 new tests: `taint` field-exact-diff, + already-tainted/externally-tainted/unknown-worktree no-ops; `database_failure` + field-exact-diff, already-externally-tainted/unknown-worktree no-ops; imported + `database_failure`/`taint`) + - Result: Added `taint(state, worktree)` (refining `taintHealthy`/`taint`, + `spec/mutation_cursor.qnt:663-710`) and `database_failure(state, worktree)` (refining + `recordDatabaseFailure`/`databaseFailure`, `spec/mutation_cursor.qnt:712-737`) to + `protocol.rs`. `taint` and `database_failure` both require a known worktree in + `ProtocolState`. For known worktrees they refine the Quint actions exactly: `taint` sets + `tainted=true`/`failure_kind=SnapshotFailure`, advances `revision` by one, and leaves + `cursor_tree`/`needs_rebaseline` unchanged; `database_failure` inserts the worktree into + `external_taint` and touches nothing else. For unknown runtime `WorktreeId` values the Rust + kernel defensively stutters, because that state is outside Quint's finite initialized + domain: Quint's `WorktreeId` ranges over the finite `WORKTREES` universe and `init` + materializes a `WorktreeState` for every member, so `recordDatabaseFailure` has no explicit + worktree-existence guard because every `WorktreeId` already resolves there — that omission + is not evidence that arbitrary unknown worktrees are valid Quint input, it is a consequence + of `WorktreeId` being a closed, pre-populated domain. This refinement's `WorktreeId` is an + unbounded runtime string, so that implicit precondition becomes an explicit runtime/kernel + contract: both actions are a guarded no-op (state returned unchanged) when the worktree is + already `tainted` (taint only)/already in `external_taint`, or has no durable state, + matching the same defensive-no-op convention `prepare`/`commit` already use for an + unresolvable worktree and keeping `external_taint ⊆ ProtocolState.worktrees` an invariant of + every state this module can produce. Neither function reads or writes `scopes`, + `processed_events`, `attempts`, or `mutation_events`. No production call site references the + module. + **Post-review correction (PR #238 review):** the original `database_failure` had no + worktree-existence guard, so `database_failure(state, &WorktreeId("unknown"))` against a + state with no `"unknown"` entry in `ProtocolState.worktrees` inserted `"unknown"` into + `external_taint` anyway — a state with no Quint counterpart, since Quint's `WorktreeId` has + no "unknown" case to represent. The original Result text's claim that "Quint's + `recordDatabaseFailure` has no worktree-existence precondition" was accurate about the Quint + source but misleadingly read as license for the same gap in the refinement; it described a + fact about the finite Quint domain, not a rule to carry over into the unbounded Rust one. + Fixed: `database_failure` now returns `state.clone()` unchanged when + `!state.worktrees.contains_key(worktree)`, before its existing `external_taint.contains` + check, matching `taint`'s existing unknown-worktree guard exactly. `taint`'s implementation + already had the correct behavior; only its test coverage and doc comment were extended to + state the rationale explicitly. Normal T04 semantics for a known worktree are unchanged by + this correction. + - Verify outcomes: + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 43/43 tests (36 from T01-T03 + 5 original T04 + 2 from the post-review correction: + `taint_is_a_no_op_for_an_unknown_worktree`, + `database_failure_is_a_no_op_for_an_unknown_worktree`). + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed. + - `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` — + no matches (AC1 spot-check). + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` + — passed, no warnings. + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed, no diff. + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed. + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed. + - `git diff --stat -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty (spec + untouched, AC8 spot-check). + - `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` — no + matches (AC8 spot-check). + - Manual review of every `external_taint` mutation site in `protocol.rs` confirms + `database_failure` is the sole insertion path and is now existence-guarded, so no test or + code path can produce `external_taint` containing a `WorktreeId` absent from + `ProtocolState.worktrees`. + - Context impact: Classification: domain. `taint`/`database_failure` are new pure logic added + to an already-unreferenced module; no existing behavior, hook, or command changed. The + post-review correction is a refinement-boundary fix to already-domain-classified logic, not + a new classification. + +- [x] T05: `Implement scope abandonment` (status:done) + - Task ID: T05 + - Scope: In — in `protocol.rs`, a pure transition refining `abandonLiveScope`/`abandon` + (`spec/mutation_cursor.qnt:739-805`): transitions a live scope to `Abandoned`, sets the + owning worktree's `needsRebaseline=true`, advances revision, leaves `cursorTree` untouched, + records the scope as terminal, preserves the scope's `actor_kind` and `worktree_id` + unchanged (scope identity stability), and is a guarded no-op for any non-live scope — + Quint's guard is "not live", so `NeverSeen`, `Closed`, and `Abandoned` all stutter — or for + a live scope on an externally tainted worktree; tests land in `tests.rs`. `abandon` resolves + its owning worktree through the referenced scope's own materialized `ScopeState.worktree_id` + (per the runtime worktree materialization contract in + `context/cli/mutation-trace-protocol.md`), so that worktree must also already exist in + `ProtocolState.worktrees` — an unknown scope or a scope whose worktree is unresolvable is a + guarded no-op, matching `taint`/`database_failure`'s existence guard rather than inventing a + separate contract. Out — recovery (T06). + - Dependencies: T04 + - Done when: tests prove abandoning a live scope sets `Abandoned`+`needsRebaseline` without + moving the cursor and without changing `actor_kind`/`worktree_id`; abandoning a `NeverSeen` + scope is a no-op; abandoning an already-terminal (`Closed`/`Abandoned`) scope is a no-op + (never reactivates a terminal scope); abandoning a live scope on an externally tainted + worktree is a no-op. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace`. + - Context synchronization: synced + - Completed: 2026-08-26 + - Files changed: + - `cli/src/services/mutation_trace/protocol.rs` (added `abandon`; updated module doc comment + to cite `spec/mutation_cursor.qnt:739-805`; added `ScopeState` to the `types` import) + - `cli/src/services/mutation_trace/tests.rs` (9 new tests: live-scope abandonment field-exact + diff, preservation of a second live scope on the same worktree, `NeverSeen`/`Closed`/ + `Abandoned` no-ops, externally-tainted-worktree no-op, a snapshot-tainted-worktree success + case, unknown-scope no-op, and a no-op when the scope's own worktree has no durable state; + imported `abandon`) + - `cli/src/services/mutation_trace/mod.rs` (post-completion correction: module doc comment + updated to list scope abandonment as implemented; see below) + - Result: Added `abandon(state, scope)` to `protocol.rs`, refining `abandonLiveScope`/`abandon` + (`spec/mutation_cursor.qnt:739-805`). Resolves the scope's `ScopeState`; guards (returning + `state.clone()` unchanged) when the scope is unknown, not live (`NeverSeen`, `Closed`, or + `Abandoned` all stutter, so a terminal scope can never be reactivated or abandoned again), on + an externally tainted worktree, or when the scope's own `worktree_id` has no durable + `WorktreeState` — this last case has no Quint counterpart (the model's finite `SCOPES` + universe guarantees every referenced worktree already resolves) and follows the same + existence-guard convention `taint`/`database_failure` established in T04. On a live, + non-externally-tainted scope: advances the owning worktree's `revision` by one, sets + `needs_rebaseline=true`, leaves `cursor_tree`/`tainted`/`failure_kind` unchanged, and sets the + scope to `Abandoned` while copying its existing `actor_kind`/`worktree_id` forward unchanged + (scope identity stability). No other scope, `external_taint`, `processed_events`, `attempts`, + or `mutation_events` entry is touched. No production call site references the module. + + **Abandonment is blocked by `external_taint`, not by snapshot taint.** A snapshot-tainted + worktree (`tainted=true`, `failure_kind=SnapshotFailure`) may still abandon an `Active` scope; + the transition preserves `tainted=true`/`failure_kind=SnapshotFailure` unchanged while setting + `needs_rebaseline=true` and advancing `revision`, exactly as Quint's `abandon` guard states — + it checks `not(isLive(...)) or externalTaint.contains(...)` only, with no `tainted` guard. + `SnapshotFailure` is degraded snapshot state; `external_taint` is the hard barrier that blocks + abandonment. This distinction is now covered by an explicit regression test (below) so it + cannot be accidentally lost. + + **Post-completion cleanup (PR #238 follow-up):** `mod.rs`'s module doc comment still read + "Scope abandonment and recovery are not yet implemented," stale after this task implemented + `abandon`. Fixed to list scope abandonment as implemented and state only recovery remains, + preserving the existing no-I/O and not-yet-wired language. Added + `abandon_succeeds_for_a_live_scope_on_a_snapshot_tainted_worktree` to `tests.rs`, proving a + snapshot-tainted (but not externally tainted) worktree still permits abandonment with taint + fields preserved; the existing + `abandon_is_a_no_op_for_a_live_scope_on_an_externally_tainted_worktree` test was left + unchanged, so the two tests together encode snapshot-taint-allows/external-taint-blocks as a + durable pair. No protocol behavior changed — `abandon`'s guard already matched the Quint + source exactly; this cleanup corrected stale documentation and closed a test-coverage gap. + - Verify outcomes: + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 52/52 tests (43 from T01-T04 + 9 new). + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed. + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` + — passed, no warnings. + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed, no diff. + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed. + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed. + - `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` — + no matches (AC1 spot-check). + - `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` — no + matches (AC8 spot-check). + - `git diff --stat -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty (spec + untouched, AC8 spot-check). + - Context impact: Classification: domain. `abandon` is new pure logic added to an + already-unreferenced module; no existing behavior, hook, or command changed. + +- [x] T06: `Implement recovery with an explicit observed-tree input` (status:done) + - Task ID: T06 + - Scope: In — in `protocol.rs`, a pure transition refining `recoverNeeded`/`recover` + (`spec/mutation_cursor.qnt:807-886`), taking the currently observed tree as an explicit + `TreeId` input (e.g. `recover(state, worktree, observed_tree)`) rather than obtaining it + itself — the core must not ambiguously "get the current tree"; that is the future Git + adapter's responsibility. Re-baselines `cursorTree` to `observed_tree`, clears + `tainted`/`failureKind`/`needsRebaseline`/`externalTaint`, advances revision, and abandons + every live scope on the worktree only when recovering from `tainted` or external taint — a + healthy worktree with only `needsRebaseline` set preserves its live scopes; guarded no-op + when the worktree is healthy, not externally tainted, and does not need rebaseline; also a + guarded no-op when `worktree` itself is absent from `ProtocolState.worktrees` (the same + runtime worktree materialization contract T04/T05 already follow — see + `context/cli/mutation-trace-protocol.md`); tests land in `tests.rs`. Out — none remaining; + this completes the action set. + - Dependencies: T05 + - Done when: tests prove taint/external-taint recovery abandons every live scope on that + worktree while a `needsRebaseline`-only recovery preserves them, both paths clear + `externalTaint`/`tainted`/`failureKind`/`needsRebaseline` and rebaseline the cursor to + `observed_tree`; recovery is a no-op on an already-healthy worktree with no rebaseline need; + and recovery is a no-op when `worktree` is unknown to `ProtocolState.worktrees`. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace`. + - Context synchronization: synced + - Completed: 2026-08-26 + - Files changed: + - `cli/src/services/mutation_trace/protocol.rs` (added `recover`; updated module doc comment + to cite `spec/mutation_cursor.qnt:807-886`) + - `cli/src/services/mutation_trace/tests.rs` (5 new tests: taint-recovery abandons live + scopes and rebaselines cursor while preserving a different-worktree scope and a + terminal same-worktree scope untouched; external-taint recovery abandons live scopes and + clears `external_taint`; `needsRebaseline`-only recovery preserves live scopes; no-op on + an already-healthy worktree with no rebaseline need; no-op for an unknown worktree; + imported `recover`) + - `cli/src/services/mutation_trace/mod.rs` (module doc comment updated to state recovery is + implemented, dropping "Recovery is not yet implemented") + - Result: Added `recover(state, worktree, observed_tree)` to `protocol.rs`, refining + `recoverNeeded`/`recover` (`spec/mutation_cursor.qnt:807-886`), taking the currently observed + tree as an explicit `TreeId` parameter rather than obtaining it itself, matching the same + explicit-input contract `prepare` already follows. Guards (returning `state.clone()` + unchanged) when `worktree` has no durable state (the same existence-guard convention + `taint`/`database_failure`/`abandon` established) or when the worktree is already healthy, + not externally tainted, and does not need rebaseline. On a worktree that does need recovery: + sets `cursor_tree=observed_tree`, `tainted=false`, `failure_kind=Healthy`, + `needs_rebaseline=false`, advances `revision` by one, and removes `worktree` from + `external_taint`. Whether recovery abandons live scopes is computed once, before mutation, as + `worktree_state.tainted || externally_tainted` (both read from the pre-transition state), so a + worktree recovering only from `needs_rebaseline` preserves every live scope on it untouched, + while a taint- or external-taint-recovering worktree transitions every one of its live scopes + to `Abandoned`, preserving each scope's `actor_kind`/`worktree_id` (scope identity stability). + Only scopes belonging to the recovered worktree are touched; scopes on other worktrees and + already-terminal scopes on the same worktree are left exactly as they were. This completes the + action set the plan scoped for `protocol.rs`; T07 (cross-action sequence/invariant tests and + the refinement matrix) is the only remaining task. No production call site references the + module. + - Verify outcomes: + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 57/57 tests (52 from T01-T05 + 5 new). + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed. + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` + — passed, no warnings. + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed, no diff (after running + `cargo fmt`). + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed. + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed. + - `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` — no + matches (AC1 spot-check). + - `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` — no + matches (AC8 spot-check). + - `git diff --stat -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty (spec + untouched, AC8 spot-check). + - Context impact: Classification: domain. `recover` is new pure logic added to an + already-unreferenced module; no existing behavior, hook, or command changed. + +- [x] T07: `Add cross-action state-sequence and invariant tests, and the Quint refinement matrix` (status:done) + - Task ID: T07 + - Scope: In — in `tests.rs`, complete state-machine sequence tests spanning multiple actions; + every scenario below is required, not "at least three": + 1. Two scopes `Active` on the same worktree, with a mutation observed while both are live + producing `AiContended` evidence; then a `Close` boundary reduces live scopes to one — + because `Close`'s own commit computes `live`/`attribution` from the **pre-close** live + set, if that same `Close` also observes a mutation it still emits `AiContended` evidence, + not `AiExclusive`; a subsequent mutation observed after the close, with exactly one live + scope remaining, is where `AiExclusive` evidence first appears. + 2. Taint → recover (abandons live scopes, rebaselines cursor). + 3. Database failure → recover (clears external taint, rebaselines cursor). + 4. Abandon → `needsRebaseline` → recover-with-preserved-survivors (a second, still-live + scope on the same worktree survives a `needsRebaseline`-only recovery). + 5. Replay of a committed `EventKey` (rejected, no state change). + 6. Stale-attempt rejection (stale revision or `beforeTree`) never advances revision, moves + the cursor, or emits evidence. + 7. Competing prepared attempts (a real CAS race, not a manually constructed stale + `AttemptState`): `prepare` two attempts `A`/`B` against the same worktree at revision 0; + `commit(A)` is accepted (`Committed`, revision → 1); `commit(B)` is then rejected because + its `expected_revision` (0) no longer matches the worktree's revision (1) — revision stays + 1, the cursor is unchanged by `B`, and `B` emits no evidence. + 8. Taint invalidates a prepared attempt: `prepare(A)` at revision `R`; `taint(worktree)` + advances the worktree to revision `R + 1`; `commit(A)` is then rejected as stale (its + `expected_revision` no longer matches) — no cursor movement and no evidence from `A`. This + is a cross-action consequence of Quint's snapshot-failure taint semantics, not something a + single-action test can show. + Invariant-style tests named to mirror the Quint invariants this module refines + (`CursorRevisionConsistent`, `FailureKindMatchesTaint`, `TerminalScopesStayTerminal`, + `DatabaseFailureDoesNotMutateDurableProtocolState`, + `ExternalTaintNeverStrengthensAttribution`, `RecoveryClearsExternalTaintOnlyAfterBaseline`, + `NoNoopMutationEvents`, `AiExclusiveRequiresExactlyOneActiveScope`, + `AiContendedRequiresMultipleActiveScopes`, `RejectedAttemptsDoNotCommitEvidence` — + `spec/mutation_cursor.qnt:1041-1274`); in `mod.rs`, a module-level rustdoc refinement matrix + classifying every relevant Quint action/result/invariant this module refines — including + `ScopeActorIdentityIsStable`, `ScopeStartedAtMostOnce`, `MutationEventsHavePositiveRevision`, + `MutationEventUniquePerWorktreeRevision`, `MutationFailureKindMatchesTaint`, + `AttributionMatchesObservedScopes`, `NeedsRebaselineSuppressesAttribution`, + `StartDoesNotAbandonExistingScopes`. + + **The matrix must classify Quint verification variables/checkpoint ledgers separately from + the semantic invariants stated over them — a verification-only data structure is not the + same thing as a verification-only invariant.** Model instrumentation may be verification-only; + the protocol property proved with that instrumentation may still be a required production + invariant, so a property's classification is never inferred solely from the fact that Quint + happens to state it using a history variable. Two categories, classified independently: + + - **Verification-only model instrumentation** — the concrete Quint checkpoint types and + history/counter variables that exist only to state or prove properties, with no Rust + production equivalent: `CursorCheckpoint`, `ProtocolCheckpoint`, `ScopeCheckpoint`, + `AbandonCheckpoint`, `StartCheckpoint`, `RecoveryCheckpoint`, + `DurableProtocolCheckpoint`, and the variables `cursorHistory`/`protocolHistory`/ + `scopeHistory`/`abandonHistory`/`startHistory`/`recoveryHistory`/`taintHistory`/ + `evidenceAttempts`/`scopeStartCount`/`everTerminal`. Each of these is classified + `verification-only / intentionally omitted` in the matrix, since `ProtocolState` does not + materialize Quint's histories, unless a future production adapter turns out to need a + direct equivalent for another reason. + - **Semantic properties expressed using that instrumentation** — classified independently, + by what the Rust code actually does, into: implemented directly, enforced by Rust type, + preserved by transition tests, verification-only / intentionally omitted, or external + adapter responsibility. At minimum: + - `TerminalScopesStayTerminal` (Quint mechanism: `everTerminal`) — **preserved by + transition tests**: `Closed`/`Abandoned` are terminal, and no Rust transition may move + either back to `NeverSeen` or `Active`. Require a test that reaches a terminal state + through real transitions and then exercises a later boundary against it to prove it + cannot reactivate — not merely constructing a terminal `ScopeState` and inspecting it. + - `ScopeStartedAtMostOnce` (Quint mechanism: `scopeStartCount`) — **preserved by + transition tests**: only `Start` on `NeverSeen` activates a scope; require a sequence + proving a second `Start` (fresh `EventKey`) on an already-`Active` scope is + accepted-but-non-observing and the scope remains `Active`, and that `Start` on a + terminal (`Closed`/`Abandoned`) scope never reactivates it. + - `RejectedAttemptsDoNotCommitEvidence` (Quint mechanism: `evidenceAttempts`) — + **preserved by transition tests**: rejected, stale, replayed, and external-taint-rejected + attempts must not emit `MutationEvent` evidence; tested once T03 exists. + - `StartDoesNotAbandonExistingScopes` (Quint mechanism: `startHistory`/`scopeHistory`) — + **preserved by transition tests**: starting one scope must not alter another + already-active scope; require an actual multi-scope sequence, not an isolated single-scope + test. + - `RecoveryClearsExternalTaintOnlyAfterBaseline` (Quint mechanism: + `recoveryHistory`/`cursorHistory`) — **preserved by transition tests**: recovery + establishes `observed_tree` as the new cursor baseline in the same pure transition that + clears `external_taint`; the histories are omitted, but the semantic ordering/effect + remains a required test. + - `DatabaseFailureDoesNotMutateDurableProtocolState` (Quint mechanism: + `taintHistory`/`durableProtocolStateFor`) — **preserved by transition tests**: + `database_failure` changes only `external_taint` and leaves every other durable + worktree/scope field unchanged. + - `ScopeActorIdentityIsStable` — **preserved by transition tests + external adapter + responsibility** (already established, preserved here): no transition in `protocol.rs` + ever mutates `actor_kind`/`worktree_id`, and future scope materialization must reject a + conflicting identity rather than overwrite it. + + Quint's finite `SCOPES` universe and its `init`-time `ScopeState` population classify as + **external adapter responsibility**: the Rust refinement's unbounded `ScopeId` space means + scope identity is materialized at runtime by the future coordinator/store layer rather than + at protocol startup (see Assumptions: "Runtime scope materialization"). + + Make the matrix auditable: for each entry, name the Quint element, whether it is + instrumentation or a semantic property, its Rust counterpart (if any), its classification, + and the concrete test or enforcement mechanism that backs a non-verification-only + classification — a markdown table is one reasonable way to do this, but any rustdoc layout + that carries the same information per entry satisfies the requirement. Add a short note on + the `coordinator.rs`/`git_snapshot.rs`/`store.rs` seams this layout leaves for later PRs. + Out — none; this is the closing task. + - Dependencies: T06 + - Done when: + 1. all eight named multi-action sequence tests exist and pass; + 2. every named semantic invariant has an explicit Rust enforcement classification + (implemented directly, enforced by Rust type, preserved by transition tests, external + adapter responsibility, or verification-only / intentionally omitted) backed by a named + test or mechanism; + 3. verification-only model instrumentation (the checkpoint types and history/counter + variables listed above) is classified separately from the semantic invariants stated + using it; + 4. no semantic property is classified verification-only merely because Quint states it using + a history/checkpoint variable — a property lands there only when it truly has no + production semantic meaning; + 5. the module doc comment contains a refinement matrix that names the concrete Rust test or + enforcement mechanism for each production-semantic invariant, auditable against + `spec/mutation_cursor.qnt`, including Quint's finite `SCOPES`/`init` population as + external adapter responsibility and `ScopeActorIdentityIsStable` as jointly preserved by + transition tests and external adapter responsibility. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace`; `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings`; `cargo fmt --manifest-path cli/Cargo.toml -- --check`. + - Context synchronization: synced + - Completed: 2026-08-26 + - Files changed: + - `cli/src/services/mutation_trace/tests.rs` (12 new tests: the 8 required cross-action + sequences — contended-to-exclusive attribution transition across a `Close`, taint→recover, + database-failure→recover, abandon→needsRebaseline-only-recover-preserves-a-survivor, replay + of a committed `EventKey`, a stale attempt invalidated by an intervening `Flush` commit, + competing prepared attempts resolved by CAS, and taint invalidating a prepared attempt — plus + 4 invariant-named tests (`ScopeStartedAtMostOnce`+`TerminalScopesStayTerminal` via a real + start→restart→close→reopen-attempt sequence, `TerminalScopesStayTerminal` via a real + abandon→reopen-attempt sequence, `StartDoesNotAbandonExistingScopes` via a two-scope + sequence, and `RejectedAttemptsDoNotCommitEvidence` via a mixed accept/reject sequence); + added a `prepare_and_commit` test helper used throughout) + - `cli/src/services/mutation_trace/mod.rs` (module doc comment extended with the Quint + refinement matrix: verification-only model instrumentation classified separately from + semantic properties, each semantic property's Rust counterpart/classification/backing test + named in a table, and a note on the `coordinator.rs`/`git_snapshot.rs`/`store.rs` seams; + corrected post-review, see below) + - `cli/src/services/mutation_trace/protocol.rs` (post-review correction: added the private + `next_revision` checked-arithmetic helper and routed `commit`/`taint`/`abandon`/`recover` + through it instead of a raw `revision + 1`; see below) + - Result: Added the plan's 8 required multi-action state-sequence tests and 4 invariant-named + tests to `tests.rs`, all reaching their preconditions through real `prepare`/`commit`/`taint`/ + `database_failure`/`abandon`/`recover` transitions rather than manually constructed state, + using a new `prepare_and_commit` helper to keep the sequences readable. Scenario 1 chains + Advance→Close→Advance on a two-scope worktree to prove `Close`'s own commit computes + attribution from the pre-close live-scope set (still `AiContended` even though it is about to + close one of the two live scopes), with `AiExclusive` appearing only once a strictly later + commit observes just one remaining live scope. Scenarios 2-4 chain + `taint`/`database_failure`/`abandon` into `recover`, proving live-scope abandonment on the + taint/external-taint paths and live-scope preservation on the `needsRebaseline`-only path. + Scenario 5 reaches a processed `EventKey` via a real prior commit before replaying it (unlike + T02's single-action replay test, which seeds `processed_events` directly). Scenario 6 + invalidates a prepared attempt via an unrelated intervening `Flush` commit (distinct from + scenarios 7-8's mechanisms). Scenario 7 prepares two attempts against the same baseline and + shows the second is rejected by CAS once the first commits — a real race, not a constructed + stale `AttemptState`. Scenario 8 shows `taint` advancing the worktree revision stales an + already-prepared attempt. The 4 invariant-named tests close the gap T07 explicitly called out: + T02-era tests proved `TerminalScopesStayTerminal`/`ScopeStartedAtMostOnce` by constructing a + terminal/active `ScopeState` directly, where the new tests reach `Closed`/`Abandoned` through + real `Start`→`Close`/`abandon` transitions and then prove a subsequent `Start` cannot + reactivate the scope; a new two-scope sequence proves starting one scope leaves an unrelated + already-active scope's `ScopeState` byte-for-byte unchanged; a mixed accept/reject sequence + proves the rejected attempt contributes no `MutationEvent` beyond what the accepted one + produced. `mod.rs`'s module doc comment gained a full refinement matrix per the task's two- + category requirement: a verification-only instrumentation list (the checkpoint types, history/ + counter variables, and the invariants that only restate consistency of that instrumentation + itself, plus the model's witness/reachability invariants), and a semantic-properties table + naming, for every property in the task's own "at minimum" list plus the remaining named + invariants from `spec/mutation_cursor.qnt:1041-1274` this module has production-relevant + coverage for, its Rust counterpart, classification, and the concrete backing test — reusing + existing T01-T06 tests as evidence where they already cover a property (e.g. + `DatabaseFailureDoesNotMutateDurableProtocolState`, + `RecoveryClearsExternalTaintOnlyAfterBaseline`, `ScopeActorIdentityIsStable`, + `ExternalTaintNeverStrengthensAttribution`, `NeedsRebaselineSuppressesAttribution`, + `AttributionMatchesObservedScopes`) rather than duplicating coverage, and citing the new T07 + tests where the task required a real-transition sequence that did not previously exist. The + matrix explicitly separates two invariants (`RejectedAttemptsDoNotCommitEvidence`, + `StartDoesNotAbandonExistingScopes`) that Quint states via history variables but that remain + production-semantic in this module, per the task's own warning against inferring + verification-only status merely from the presence of a history variable. Quint's finite + `SCOPES`/`WORKTREES`/`init` population is recorded as external adapter responsibility, and + `ScopeActorIdentityIsStable` as jointly preserved-by-tests-and-external-adapter-responsibility, + matching the task's explicit requirement. No production call site references the module. This + completes the task stack the plan scoped for `cli/src/services/mutation_trace/`. + + **Post-review correction (PR #238 review):** the original refinement matrix and one algorithm + detail had three defects. + + First, three semantic invariants (`AbandonCreatesRebaselineRequirement`, + `MutationEventsMatchCursorHistory`, `MutationEventsCrossOnlyTrustworthyProtocolStates`) were + misclassified `verification-only`, having been placed there because Quint states them using + history/checkpoint variables (`abandonHistory`/`protocolHistory`/`cursorHistory`/ + `scopeHistory`), not because the properties themselves lack production meaning — the exact + "verification-only data structure ≠ verification-only invariant" distinction the task's own + instructions required. All three were moved into the semantic-properties table: the first is + backed by `abandon_transitions_a_live_scope_without_moving_the_cursor_or_changing_identity` + (already asserted `mutation_events` unchanged, so no new test was needed); the second is backed + by existing T03/T07 tests since `apply` derives an emitted event's `before_tree`/`after_tree`/ + revision from the same values the worktree update itself uses; the third needed a new direct + regression test, `needs_rebaseline_suppresses_mutation_event_even_when_commit_observes_a_real_tree_change`, + since no existing test drove `commit`'s full `accepted && observes && observed_change` path + against a `needs_rebaseline` worktree to prove `changed` still comes out `false` and no cursor + movement or `MutationEvent` results. + + Second, `AiExclusiveRequiresExactlyOneActiveScope` was classified "enforced by Rust type", + which is false: `Attribution::AiExclusive(ScopeId)` does not itself make an inconsistent scope + count unrepresentable — a caller can construct it with any `ScopeId` regardless of + `ProtocolState.scopes`. The guarantee is algorithmic (`attribution_for` only reaches that + branch when `live.len() == 1`), so the classification was corrected to "implemented directly + + preserved by transition tests". A full audit of the matrix found no other row making an + unsound "enforced by Rust type" claim. + + Third, every revision-advancing transition (`commit`, `taint`, `abandon`, `recover`) used a raw + `worktree_state.revision + 1`, silently assuming a Rust `u64` can always refine Quint's + unbounded `revision: int`. At `revision == u64::MAX` this would wrap to `0` in release mode, + violating `MutationEventsHavePositiveRevision`/`MutationEventUniquePerWorktreeRevision`/CAS + freshness reasoning. Fixed with checked arithmetic rather than a documented precondition: added + a private `next_revision(revision: u64) -> Option` (`revision.checked_add(1)`) in + `protocol.rs`, and routed all four actions through it. `commit`'s `evaluate` now folds + `next_revision(...).is_some()` into `accepted` unconditionally (so an overflow behaves exactly + like a stale/rejected attempt — no cursor movement, scope transition, processed-`EventKey` + insertion, or `MutationEvent` — decided before `apply` ever touches state, per the "no partial + commit" requirement); `apply` computes the checked `advanced_revision` once and reuses it for + both the worktree update and any emitted `MutationEvent`'s revision field, removing the + remaining raw `+ 1` there too. `taint`/`abandon`/`recover` each gained the same guard as an + additional no-op precondition alongside their existing existence/precondition guards. Four new + tests (`commit_does_not_wrap_revision_at_u64_max`, `taint_does_not_wrap_revision_at_u64_max`, + `abandon_does_not_wrap_revision_at_u64_max`, `recover_does_not_wrap_revision_at_u64_max`) each + start from `revision: u64::MAX` and prove the action is a no-op (a rejection, for `commit`) + rather than a wrap. The matrix gained a new "Bounded-integer revision refinement" section + documenting this as a Rust-only refinement precondition with no Quint counterpart. A manual + audit of every `revision + 1`/`.revision + 1` occurrence in `cli/src/services/mutation_trace/` + after this correction found none remaining; all five sites (the worktree update and mutation- + event revision inside `commit`'s `apply`, plus one each in `taint`/`abandon`/`recover`) now go + through `next_revision`. + - Verify outcomes: + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 74/74 tests (57 from T01-T06 + 12 from T07's first pass + 5 from this correction: 1 direct + `needs_rebaseline`/`MutationEventsCrossOnlyTrustworthyProtocolStates` regression test and 4 + revision-overflow no-op/rejection tests). + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` + — passed clean on this correction (first pass required switching the new + `prepare_and_commit` test helper's `attempt` parameter from by-value to `&AttemptId` for + `clippy::needless_pass_by_value`; this correction introduced no new clippy findings). + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed after running `cargo fmt` + (several new multi-line expressions in this correction's new tests needed re-wrapping). + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed (implied by the + test run above). + - `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` — no + matches (AC1 spot-check). + - `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` — no + matches (AC8 spot-check). + - `git diff --stat -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty (spec + untouched, AC8 spot-check). + - Manual audit: `grep -n "revision + 1" cli/src/services/mutation_trace/*.rs` — no matches + outside a doc-comment prose mention (updated to describe the new checked helper); every + revision-advancing site now calls `next_revision`. + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed. + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed. + - Context impact: Classification: domain. New tests and an expanded module-doc refinement matrix + were added to an already-unreferenced, already-domain-classified module; the post-review + correction's `next_revision` checked-arithmetic helper is a small refinement-boundary fix to + already-domain-classified logic (matching T04's precedent), not a new classification — no + existing behavior, hook, or command outside the module changed. Context synchronized in the + same session as this correction: `context/cli/mutation-trace-protocol.md` (bounded-revision + pointer added, kept at exactly 250 lines by tightening nearby prose) and a new focused domain + file, `context/cli/mutation-trace-revision-refinement.md` (the Quint `int` → Rust `u64` + worktree-revision refinement, `next_revision`, and the four overflow tests), linked from both + the protocol domain file and `context/context-map.md`. `context/overview.md`, + `context/architecture.md`, `context/glossary.md`, and `context/patterns.md` were verified and + found not contradicted; this is an internal, file-scoped refinement detail, not repository-wide + terminology, so no root-file edit or glossary entry was warranted. This is also the plan's + closing implementation task: the full `mutation_trace` module (`mod.rs`/`types.rs`/`protocol.rs`/ + `tests.rs`) described in the plan's Change summary now exists, tested, and documented, with no + wiring into any hook, command, or database call site, matching AC8 and the plan's own + non-goals. + + - Post-review correction (second pass): the first checked-u64 correction over-constrained + commit acceptance by requiring revision headroom unconditionally. Quint's no-change `Flush` + is accepted without revision advancement, so the Rust guard was narrowed to only commits that + would actually advance revision. Added a regression test for a no-change `Flush` at + `u64::MAX` committing successfully with revision unchanged. + + `ResolvedAttempt::evaluate` now computes `would_advance_revision` (`!is_flush(boundary) || + tree_changed`) before deciding `accepted`, and only requires + `next_revision(worktree_state.revision).is_some()` when that flag is true — a non-`Flush` + always advances revision when accepted, so it always needs headroom; a `Flush` needs headroom + only when it also observes a real tree change. `ResolvedAttempt::apply` now computes + `advanced_revision` as `Option`, `Some` only when `evaluation.advances_revision` is true, + and updates the worktree only in that case, so a no-change `Flush` leaves the worktree + (cursor, revision, everything) completely untouched instead of panicking on an unconditional + `next_revision(...).expect(...)`. The `MutationEvent` revision field unwraps + `advanced_revision` with `.expect("changed implies advances_revision")`, sound because + `changed` can only be true when `observed_change` (hence `advances_revision`) is also true. + The existing `commit_does_not_wrap_revision_at_u64_max` test was renamed to + `commit_that_would_advance_is_rejected_at_u64_max` for clarity (unchanged logic — a `Start` + boundary always advances revision when accepted, so it is still correctly rejected at + `u64::MAX`); a new `no_change_flush_commits_at_u64_max_without_advancing_revision` test proves + the paired case: a `Flush` observing no tree change at `revision: u64::MAX` is accepted, + committed, and leaves the worktree's revision at `u64::MAX` with no `MutationEvent`. Together + the two tests encode that headroom is required for advancement, not for acceptance in general. + Updated the stale "unconditional" wording in `protocol.rs`'s `evaluate` rustdoc, `mod.rs`'s + bounded-integer refinement section, and + `context/cli/mutation-trace-revision-refinement.md` to describe the conditional guard. + - Verify outcomes (post-review correction): + - `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` — passed, + 75/75 tests (74 from the first pass + 1 net add: one test renamed, one new test added). + - `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` — passed. + - `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` + — passed clean. + - `cargo fmt --manifest-path cli/Cargo.toml -- --check` — passed. + - `nix run .#quint -- typecheck spec/mutation_cursor.qnt` — passed (spec untouched). + - `nix run .#quint -- test spec/mutation_cursor.qnt` — passed (spec untouched). + - `git diff --stat -- spec/mutation_cursor.qnt spec/mutation_cursor.md` — empty. + - `grep -Rni "unconditional" cli/src/services/mutation_trace context/cli/mutation-trace-revision-refinement.md context/plans/mutation-cursor-protocol-kernel.md` + — no remaining claim that commit revision headroom is required unconditionally (this note's + own prose describing the *old, corrected* behavior is the only remaining match, by design). + +## Open questions + +None. The request pre-authorizes following the current `spec/mutation_cursor.qnt` over its own +illustrative examples, which resolves the one substantive doubt (see Assumptions); the module's +value and scope are otherwise well-specified and not duplicated by any existing code. The +`coordinator.rs`/`git_snapshot.rs`/`store.rs` roadmap is recorded as context for later plans +rather than as work here, consistent with this plan's own non-goals. This revision's task +reshaping (T02 absorbing `Flush` commit evaluation, T03's pre-transition live-scope requirement, +T04's dependency correction, T05's `NeverSeen` no-op case, T06's explicit `observed_tree` +parameter, and T07's full-scenario/refinement-matrix requirements) was fully specified by the +user, leaving nothing to ask. + +## Validation Report + +**Status:** validated +**Date:** 2026-08-26 + +### Commands run + +- `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml` -> exit 0 (680 passed; 0 failed) +- `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` -> exit 0 (clean, no warnings) +- `cargo fmt --manifest-path cli/Cargo.toml -- --check` -> exit 0 (no diff) +- `nix run .#quint -- typecheck spec/mutation_cursor.qnt` -> exit 0 (typechecks) +- `nix run .#quint -- test spec/mutation_cursor.qnt` -> exit 0 (mutation_cursor test suite passed) +- `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` -> exit 0 (75 passed; 0 failed) +- `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` -> exit 1 (no matches) +- `git diff --stat spec/mutation_cursor.qnt` -> exit 0 (empty; spec untouched) +- `grep -rn "mutation_trace" cli/src/services/hooks cli/src/services/agent_trace.rs` -> exit 1 (no matches) + +### Success-criteria verification + +- [x] AC1: pure module has no Git/DB/FS/env/network/async/lock I/O and an explicit `ProtocolState` aggregate -> forbidden-import grep returned no matches; manual inspection of `mod.rs`/`types.rs`/`protocol.rs` imports found only `std::collections::{BTreeMap, BTreeSet}`; `ProtocolState` at `cli/src/services/mutation_trace/types.rs:292-299` has exactly the fields `worktrees`/`scopes`/`external_taint`/`processed_events`/`attempts`/`mutation_events` +- [x] AC2: hook/`Flush` boundary commit evaluation matches `commitAttempt` exactly -> `mutation_trace` test suite (75/75) includes T02's prepare/commit, accepted-but-non-observing, and `Flush`-vs-hook `advancesRevision` tests, all passing +- [x] AC3: attribution/mutation-event emission from pre-transition live scopes -> T03's `mutation_trace` tests (live-scope/attribution variants, `Start`/`Close` pre-transition cases) pass within the same 75/75 run +- [x] AC4: snapshot-failure taint and database-failure external-taint field-exact scoping -> T04's `mutation_trace` tests (field-exact diffs, no-op guards) pass within the same run +- [x] AC5: abandonment terminality, identity stability, and no-op cases -> T05's `mutation_trace` tests pass within the same run +- [x] AC6: recovery re-baselining and conditional live-scope abandonment -> T06's `mutation_trace` tests pass within the same run +- [x] AC7: rejected/stale attempts never advance revision, move the cursor, or emit evidence across sequences -> T07's cross-action sequence and invariant-named tests pass within the same run +- [x] AC8: spec untouched and green, no production call site -> `git diff --stat spec/mutation_cursor.qnt` empty, `grep` for `mutation_trace` in `cli/src/services/hooks`/`agent_trace.rs` found nothing, and both Quint commands passed + +### Failed checks and follow-ups + +- None. + +### Residual risks + +- None identified.