tests: Add mutation cursor Quint Connect replays

Exercise the remaining deterministic scenarios and guarded no-op regressions through the real Rust protocol, then compare generated Quint traces against the model across 500 samples. This expands MBT coverage without changing production protocol behavior.

Plan: mutation-cursor-quint-connect, T05

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

Author: davidabram

.github/workflows/quint.yml

@@ -40,7 +40,7 @@ jobs:
             exit 0
           fi
 
-          if git diff --name-only "$BASE_SHA" "$HEAD_SHA" | grep -Eq '(\.qnt$|^\.github/workflows/quint\.yml$|^\.github/workflows/quint-deep-verify\.yml$|^flake\.nix$|^flake\.lock$)'; then
+          if git diff --name-only "$BASE_SHA" "$HEAD_SHA" | grep -Eq '(\.qnt$|^cli/src/services/mutation_trace/mbt/|^cli/src/services/mutation_trace/protocol\.rs$|^cli/src/services/mutation_trace/types\.rs$|^cli/Cargo\.toml$|^cli/Cargo\.lock$|^\.github/workflows/quint\.yml$|^\.github/workflows/quint-deep-verify\.yml$|^flake\.nix$|^flake\.lock$)'; then
             echo "quint=true" >> "$GITHUB_OUTPUT"
           else
             echo "quint=false" >> "$GITHUB_OUTPUT"
@@ -55,7 +55,9 @@ jobs:
     needs: detect
     if: needs.detect.outputs.quint == 'true'
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    # The Quint Connect Nix check compiles the CLI crate, so this needs more
+    # headroom than the pure-Quint steps alone required.
+    timeout-minutes: 30
     steps:
       - name: Harden the runner (Audit all outbound calls)
         uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0
@@ -78,7 +80,11 @@ jobs:
         run: nix run .#quint -- typecheck spec/mutation_cursor.qnt
 
       - name: Run Quint tests
-        run: nix run .#quint -- test spec/mutation_cursor.qnt
+        # `quint test` without `--match` silently selects zero tests (exit 0,
+        # no output) on this spec instead of running every named `run`
+        # scenario — matching every top-level `test...`-named `run` is the
+        # explicit selection that actually exercises them.
+        run: nix run .#quint -- test spec/mutation_cursor.qnt --match '^test.*'
 
       - name: Randomized Quint safety check
         run: >
@@ -89,6 +95,13 @@ jobs:
           --max-samples=5000
           --max-steps=20
 
+      - name: Quint Connect model-based tests (Nix-pinned Rust + Quint)
+        # The entire MBT invocation goes through this Nix check rather than
+        # `cargo test` on the runner's own Cargo, so both the Rust toolchain
+        # and the Quint binary come from the repository's pinned flake
+        # inputs, never a second, unpinned Rust installation.
+        run: nix build .#checks.x86_64-linux.mutation-trace-quint-connect --print-build-logs
+
   gate:
     name: Quint gate
     if: always()

cli/src/services/mutation_trace/mbt/tests.rs

@@ -1,6 +1,6 @@
 //! Deterministic Quint Connect replays through the real `protocol.rs`.
 
-use quint_connect::quint_test;
+use quint_connect::{quint_run, quint_test};
 
 use super::driver::MutationCursorDriver;
 
@@ -20,3 +20,119 @@ use super::driver::MutationCursorDriver;
 fn mutation_cursor_transports_non_default_arguments() -> impl Driver {
     MutationCursorDriver::default()
 }
+
+/// Replays `testStartObservesBeforeActivation`: the freshness-boundary
+/// semantics for a `Start` observation.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testStartObservesBeforeActivation"
+)]
+fn mutation_cursor_start_observes_before_activation() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Replays `testCloseObservesBeforeDeactivation`.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testCloseObservesBeforeDeactivation"
+)]
+fn mutation_cursor_close_observes_before_deactivation() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Replays `testContendedIntervalsRemainAiContended`.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testContendedIntervalsRemainAiContended"
+)]
+fn mutation_cursor_contended_intervals_remain_ai_contended() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Replays `testNoChangeHookReplayCannotStealFutureChange`.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testNoChangeHookReplayCannotStealFutureChange"
+)]
+fn mutation_cursor_no_change_hook_replay_cannot_steal_future_change() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Replays `testConcurrentObservationsHaveOneWinner`.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testConcurrentObservationsHaveOneWinner"
+)]
+fn mutation_cursor_concurrent_observations_have_one_winner() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Replays `testTaintInvalidatesPreparedObservation`.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testTaintInvalidatesPreparedObservation"
+)]
+fn mutation_cursor_taint_invalidates_prepared_observation() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Replays `testRecoveryEstablishesBaseline`.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testRecoveryEstablishesBaseline"
+)]
+fn mutation_cursor_recovery_establishes_baseline() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Replays `testClosedScopeCannotReactivate`.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testClosedScopeCannotReactivate"
+)]
+fn mutation_cursor_closed_scope_cannot_reactivate() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Guarded-no-op regression: replays
+/// `testMbtGuardedPrepareInvokesRealPrepare`
+/// (`init.then(prepare(Attempt0, Start(...))).then(prepare(Attempt0,
+/// Advance(...)))`), where the second `prepare` guards because `Attempt0` is
+/// no longer `Available`. A passing replay proves the driver still calls
+/// `protocol::prepare` on the guarded step — dispatch is on the `MbtAction`
+/// variant Quint recorded, never skipped because Quint's own state happened
+/// not to change — and independently reaches the same no-op outcome.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testMbtGuardedPrepareInvokesRealPrepare"
+)]
+fn mutation_cursor_guarded_prepare_invokes_real_prepare() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Guarded-no-op regression: replays
+/// `testMbtGuardedRecoverInvokesRealRecover` (`init.then(recover(WT0))`),
+/// where `recover` guards because `WT0` is neither tainted, externally
+/// tainted, nor needing rebaseline. A passing replay proves the driver still
+/// calls `protocol::recover` on the guarded step and independently reaches
+/// the same no-op outcome.
+#[quint_test(
+    spec = "../spec/mutation_cursor.qnt",
+    test = "testMbtGuardedRecoverInvokesRealRecover"
+)]
+fn mutation_cursor_guarded_recover_invokes_real_recover() -> impl Driver {
+    MutationCursorDriver::default()
+}
+
+/// Generated-trace refinement: replays Quint-generated randomized
+/// traces through the real `protocol.rs`, comparing `ModelState` against
+/// Quint's semantic state after every step. Reproducible with a fixed
+/// `QUINT_SEED`.
+#[quint_run(
+    spec = "../spec/mutation_cursor.qnt",
+    max_samples = 500,
+    max_steps = 30
+)]
+fn mutation_cursor_generated_traces_refine_rust_protocol() -> impl Driver {
+    MutationCursorDriver::default()
+}