mutation-trace: Allow no-change Flush commits at max revision

Revision headroom is only required when a commit will advance the worktree,
so a no-change `Flush` can commit at `u64::MAX` without wrapping or being
rejected.

Compute whether the boundary would advance before applying the checked revision
guard, and only derive the next revision for advancing commits. Add regression
coverage for both the rejected advancing case and the accepted no-change case.

Co-authored-by: SCE <sce@crocoder.dev>

Author: davidabram

cli/src/services/mutation_trace/mod.rs

@@ -128,19 +128,32 @@
 //! `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`. `commit`'s `accepted` gate folds this check in
-//! unconditionally (a would-be-overflowing attempt is rejected exactly like
-//! a stale one, with no cursor movement, scope transition, processed-
-//! `EventKey` insertion, or `MutationEvent`); `taint`/`abandon`/`recover`
-//! treat it as an additional guarded no-op alongside their existing
-//! existence/precondition guards. This has no Quint counterpart — Quint's
-//! `revision` never needs such a guard — so it is a Rust-only refinement
-//! precondition, verified by `commit_does_not_wrap_revision_at_u64_max`,
-//! `taint_does_not_wrap_revision_at_u64_max`,
+//! 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 (or, for `commit`,
-//! a rejection) rather than a wrap.
+//! `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;

cli/src/services/mutation_trace/protocol.rs

@@ -229,15 +229,16 @@ impl ResolvedAttempt {
     /// Refines the `fresh`/`observes`/`accepted`/`observedChange`/`changed`/
     /// `advancesRevision` computation at `spec/mutation_cursor.qnt:462-483`.
     ///
-    /// `accepted` additionally requires the worktree's revision to have
-    /// headroom to advance ([`next_revision`]) — a Rust-only refinement
-    /// guard with no Quint counterpart, since Quint's `revision` is
-    /// unbounded. This is deliberately unconditional on whether the
-    /// boundary would actually advance the revision (a `Flush` observing no
-    /// change would not), because [`ResolvedAttempt::apply`] must never
-    /// discover a would-be overflow after `accepted` was already decided;
-    /// keeping the guard uniform here means every accepted commit is proven
-    /// safe to advance before any state is touched.
+    /// `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
@@ -260,9 +261,14 @@ impl ResolvedAttempt {
         } else {
             true
         };
-        let accepted = fresh && next_revision(self.worktree_state.revision).is_some();
-        let observed_change =
-            accepted && observes && self.planned.before_tree != self.planned.after_tree;
+
+        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);
 
@@ -294,12 +300,20 @@ impl ResolvedAttempt {
             return next;
         }
 
-        // `accepted` already proved (in `evaluate`) that advancing the
-        // worktree's revision cannot wrap; this recomputes the same checked
-        // value rather than trusting a stored flag, so this function has no
-        // raw `+ 1` of its own.
-        let advanced_revision = next_revision(self.worktree_state.revision)
-            .expect("accepted requires revision headroom, see `evaluate`");
+        // `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`
@@ -323,7 +337,7 @@ impl ResolvedAttempt {
             self.worktree_state.cursor_tree.clone()
         };
 
-        if evaluation.advances_revision {
+        if let Some(advanced_revision) = advanced_revision {
             next.worktrees.insert(
                 self.worktree.clone(),
                 WorktreeState {
@@ -343,9 +357,10 @@ impl ResolvedAttempt {
         }
 
         if evaluation.changed {
+            let revision = advanced_revision.expect("changed implies advances_revision");
             next.mutation_events.insert(MutationEvent {
                 worktree_id: self.worktree.clone(),
-                revision: advanced_revision,
+                revision,
                 before_tree: self.planned.before_tree.clone(),
                 after_tree: self.planned.after_tree.clone(),
                 active_scopes: live_scopes_on(state, &self.worktree),

cli/src/services/mutation_trace/tests.rs

@@ -2105,8 +2105,13 @@ fn needs_rebaseline_suppresses_mutation_event_even_when_commit_observes_a_real_t
 // 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_does_not_wrap_revision_at_u64_max() {
+fn commit_that_would_advance_is_rejected_at_u64_max() {
     let mut state = ProtocolState::default();
     state
         .worktrees
@@ -2153,6 +2158,68 @@ fn commit_does_not_wrap_revision_at_u64_max() {
     );
 }
 
+// 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();