diff --git a/.github/workflows/pr-ci.yml b/.github/workflows/pr-ci.yml index 38bceef9..d0eb1108 100644 --- a/.github/workflows/pr-ci.yml +++ b/.github/workflows/pr-ci.yml @@ -42,11 +42,11 @@ jobs: - name: Run flake checks run: | - time nix flake check --print-build-logs + time nix flake check --fallback --print-build-logs - name: Build and smoke-test native CLI run: | - time nix build .#sce --out-link result --print-build-logs + time nix build .#sce --fallback --out-link result --print-build-logs ./result/bin/sce --help ./result/bin/sce version @@ -78,4 +78,4 @@ jobs: - name: Build release package and audit portability run: | - time nix build .#ci-checks --out-link result-ci-checks --print-build-logs + time nix build .#ci-checks --fallback --out-link result-ci-checks --print-build-logs diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index d9639cb0..18395f89 100644 --- a/.github/workflows/quint.yml +++ b/.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/|^cli/src/services/mod\.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() diff --git a/cli/Cargo.lock b/cli/Cargo.lock index 293d3978..c20764e5 100644 --- a/cli/Cargo.lock +++ b/cli/Cargo.lock @@ -400,7 +400,7 @@ version = "0.69.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "271383c67ccabffb7381723dea0672a673f292304fcb45c01cc648c7a8d58088" dependencies = [ - "bitflags", + "bitflags 2.13.0", "cexpr", "clang-sys", "itertools 0.12.1", @@ -432,6 +432,12 @@ version = "0.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5e764a1d40d510daf35e07be9eb06e75770908c27d411ee6c92109c9840eaaf7" +[[package]] +name = "bitflags" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + [[package]] name = "bitflags" version = "2.13.0" @@ -539,6 +545,15 @@ dependencies = [ "rustc_version", ] +[[package]] +name = "bs58" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf88ba1141d185c399bee5288d850d63b8369520c1eafc32a0430b5b6c287bf4" +dependencies = [ + "tinyvec", +] + [[package]] name = "bumpalo" version = "3.20.3" @@ -646,6 +661,7 @@ dependencies = [ "iana-time-zone", "js-sys", "num-traits", + "serde", "wasm-bindgen", "windows-link", ] @@ -741,6 +757,15 @@ version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570" +[[package]] +name = "colored" +version = "3.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" +dependencies = [ + "windows-sys 0.61.2", +] + [[package]] name = "combine" version = "4.6.7" @@ -879,7 +904,7 @@ version = "0.29.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d8b9f2e4c67f833b660cdb0a3523065869fb35570177239812ed4c905aeff87b" dependencies = [ - "bitflags", + "bitflags 2.13.0", "crossterm_winapi", "derive_more", "document-features", @@ -978,6 +1003,27 @@ dependencies = [ "syn", ] +[[package]] +name = "dashu-base" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "993b95dc1b248e3f5747dcb017a41d6e75853a2e5ee4504f7d537c5b8dffdae4" + +[[package]] +name = "dashu-int" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49c05a0d5cb0b39fcc87c46432fdac24b90dce239857c7f6b798be4ffc3c42c6" +dependencies = [ + "cfg-if", + "dashu-base", + "num-modular", + "num-order", + "rustversion", + "serde", + "static_assertions", +] + [[package]] name = "data-encoding" version = "2.11.0" @@ -990,6 +1036,37 @@ version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c286de4e81ea2590afc24d754e0f83810c566f50a1388fa75ebd57928c0d9745" +[[package]] +name = "defmt" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2953bfe4f93bbd20cc71198842756f77d161884c99ebbabc41d80231ded88d1" +dependencies = [ + "bitflags 1.3.2", + "defmt-macros", +] + +[[package]] +name = "defmt-macros" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bad9c72e7ca2137e0dc3813245a0d282fd6daad32fd800af018306a9169b5fe8" +dependencies = [ + "defmt-parser", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "defmt-parser" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "10d60334b3b2e7c9d91ef8150abfb6fa4c1c39ebbcf4a81c2e346aad939fee3e" +dependencies = [ + "thiserror", +] + [[package]] name = "deranged" version = "0.5.8" @@ -1518,13 +1595,19 @@ dependencies = [ "futures-core", "futures-sink", "http", - "indexmap", + "indexmap 2.14.0", "slab", "tokio", "tokio-util", "tracing", ] +[[package]] +name = "hashbrown" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" + [[package]] name = "hashbrown" version = "0.16.1" @@ -1894,6 +1977,17 @@ dependencies = [ "icu_properties", ] +[[package]] +name = "indexmap" +version = "1.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99" +dependencies = [ + "autocfg", + "hashbrown 0.12.3", + "serde", +] + [[package]] name = "indexmap" version = "2.14.0" @@ -1902,6 +1996,8 @@ checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" dependencies = [ "equivalent", "hashbrown 0.17.1", + "serde", + "serde_core", ] [[package]] @@ -1933,7 +2029,7 @@ version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6654738b8024300cf062d04a1c13c10c8e2cea598ec1c47dc9b6641159429756" dependencies = [ - "bitflags", + "bitflags 2.13.0", "crossterm", "dyn-clone", "fuzzy-matcher", @@ -1965,7 +2061,7 @@ version = "0.7.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9080b15e63775b9a2ac7dca720f7050a8b955e092ea0f6020a4a80f69998cdc0" dependencies = [ - "bitflags", + "bitflags 2.13.0", "cfg-if", "libc", ] @@ -2017,12 +2113,77 @@ dependencies = [ "either", ] +[[package]] +name = "itf" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5d620b7b3d17650581da9208d1240baaff4ee33decff1c7782bdb9b4cab71c20" +dependencies = [ + "dashu-int", + "serde", + "serde_json", + "serde_with", +] + [[package]] name = "itoa" version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" +[[package]] +name = "jiff" +version = "0.2.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "668b7183bd07af9a4885f5c35b0cc5c83c4607a913c16b7e17291832910d2dcc" +dependencies = [ + "defmt", + "jiff-core", + "jiff-static", + "jiff-tzdb-platform", + "log", + "portable-atomic", + "portable-atomic-util", + "serde_core", + "windows-link", +] + +[[package]] +name = "jiff-core" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7feca88439efe53da3754500c1851dedf3cb36c524dd5cf8225cc0794de95d09" +dependencies = [ + "defmt", +] + +[[package]] +name = "jiff-static" +version = "0.2.35" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3a69dcb3a21cfb32ce1cd056169337ca284af0766dd766e7878819b251a49204" +dependencies = [ + "jiff-core", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "jiff-tzdb" +version = "0.1.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "142bd39932ad231f10513df9ab62661fead8719872150b7ad02a2df79f4e141e" + +[[package]] +name = "jiff-tzdb-platform" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "875a5a69ac2bab1a891711cf5eccbec1ce0341ea805560dcd90b7a2e925132e8" +dependencies = [ + "jiff-tzdb", +] + [[package]] name = "jni" version = "0.22.4" @@ -2484,6 +2645,21 @@ dependencies = [ "num-traits", ] +[[package]] +name = "num-modular" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd8e500409e6cd603b03e477c26a6caecdc27ac58979a53e881c75eafc079f44" + +[[package]] +name = "num-order" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "537b596b97c40fcf8056d153049eb22f481c17ebce72a513ec9286e4986d1bb6" +dependencies = [ + "num-modular", +] + [[package]] name = "num-rational" version = "0.4.2" @@ -2695,6 +2871,15 @@ version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "05c8b63e8d9609db387f0324918f81d68fe27748f084ef092fb35954d0539a85" +[[package]] +name = "portable-atomic-util" +version = "0.2.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2a106d1259c23fac8e543272398ae0e3c0b8d33c88ed73d0cc71b0f1d902618" +dependencies = [ + "portable-atomic", +] + [[package]] name = "potential_utf" version = "0.1.5" @@ -2828,6 +3013,35 @@ dependencies = [ "windows-sys 0.60.2", ] +[[package]] +name = "quint-connect" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67a4e156a3d4580b73eff41805d3237c909f96388158b3eed12afaa4f619d61c" +dependencies = [ + "anyhow", + "colored", + "itf", + "quint-connect-macros", + "rand 0.9.4", + "serde", + "serde_json", + "similar", + "tempfile", + "version_check", +] + +[[package]] +name = "quint-connect-macros" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "814c6e076fa655b78d7127fda492f3fa980b8827fda16c33d891b57c8ccd735f" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "quote" version = "1.0.46" @@ -2958,7 +3172,7 @@ version = "0.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed2bf2547551a7053d6fdfafda3f938979645c44812fbfcda098faae3f1a362d" dependencies = [ - "bitflags", + "bitflags 2.13.0", ] [[package]] @@ -3150,7 +3364,7 @@ version = "0.38.44" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fdb5bc1ae2baa591800df16c9ca78619bf65c0488b41b96ccec5d11220d8c154" dependencies = [ - "bitflags", + "bitflags 2.13.0", "errno", "libc", "linux-raw-sys 0.4.15", @@ -3163,7 +3377,7 @@ version = "1.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6fe4565b9518b83ef4f91bb47ce29620ca828bd32cb7e408f0062e9930ba190" dependencies = [ - "bitflags", + "bitflags 2.13.0", "errno", "libc", "linux-raw-sys 0.12.1", @@ -3275,6 +3489,30 @@ dependencies = [ "windows-sys 0.61.2", ] +[[package]] +name = "schemars" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4cd191f9397d57d581cddd31014772520aa448f65ef991055d7f61582c65165f" +dependencies = [ + "dyn-clone", + "ref-cast", + "serde", + "serde_json", +] + +[[package]] +name = "schemars" +version = "1.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "687274d293b6cdc6e73e0fee520bf2049650090d7164f87672d212a3c530cf4a" +dependencies = [ + "dyn-clone", + "ref-cast", + "serde", + "serde_json", +] + [[package]] name = "scoped-tls" version = "1.0.1" @@ -3312,7 +3550,7 @@ version = "3.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b7f4bc775c73d9a02cde8bf7b2ec4c9d12743edf609006c7facc23998404cd1d" dependencies = [ - "bitflags", + "bitflags 2.13.0", "core-foundation", "core-foundation-sys", "libc", @@ -3410,6 +3648,39 @@ dependencies = [ "serde", ] +[[package]] +name = "serde_with" +version = "3.22.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ee78f1fbe43ac4a0e47aadb3dbd357b69eb0d3793e948624cd03dd2750ab1c0a" +dependencies = [ + "base64", + "bs58", + "chrono", + "hex", + "indexmap 1.9.3", + "indexmap 2.14.0", + "jiff", + "schemars 0.9.0", + "schemars 1.2.2", + "serde_core", + "serde_json", + "serde_with_macros", + "time", +] + +[[package]] +name = "serde_with_macros" +version = "3.22.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8705578779c2b6bd90d84d66eb2e206b708b1a4d7b9f17641b293545bf1c7e46" +dependencies = [ + "darling", + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "sha1_smol" version = "1.0.1" @@ -3464,6 +3735,7 @@ dependencies = [ "keyring-core", "murmur3", "owo-colors 4.3.0", + "quint-connect", "rand 0.8.6", "reqwest", "serde", @@ -3557,6 +3829,12 @@ version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e3a9fe34e3e7a50316060351f37187a3f546bce95496156754b601a5fa71b76e" +[[package]] +name = "similar" +version = "2.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bbbb5d9659141646ae647b42fe094daf6c6192d1620870b449d9557f748b2daa" + [[package]] name = "simsimd" version = "6.5.16" @@ -3615,6 +3893,12 @@ version = "1.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596" +[[package]] +name = "static_assertions" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" + [[package]] name = "strsim" version = "0.11.1" @@ -4002,7 +4286,7 @@ version = "0.9.12+spec-1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cf92845e79fc2e2def6a5d828f0801e29a2f8acc037becc5ab08595c7d5e9863" dependencies = [ - "indexmap", + "indexmap 2.14.0", "serde_core", "serde_spanned", "toml_datetime 0.7.5+spec-1.1.0", @@ -4035,7 +4319,7 @@ version = "0.25.12+spec-1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2153edc6955a6c354fad8f5efd38b6a8769bdccf9fe50f8e1329f81b0baa5d7" dependencies = [ - "indexmap", + "indexmap 2.14.0", "toml_datetime 1.1.1+spec-1.1.0", "toml_parser", "winnow 1.0.3", @@ -4077,7 +4361,7 @@ version = "0.6.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4cfcf7e2740e6fc6d4d688b4ef00650406bb94adf4731e43c096c3a19fe40840" dependencies = [ - "bitflags", + "bitflags 2.13.0", "bytes", "futures-util", "http", @@ -4210,7 +4494,7 @@ dependencies = [ "arc-swap", "aristo", "bigdecimal", - "bitflags", + "bitflags 2.13.0", "branches", "bumpalo", "bytemuck", @@ -4295,7 +4579,7 @@ version = "0.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4ad90c0e6eea7ab131214804c70edad5372acecdcad8d4ccc75b0ded55b0df8f" dependencies = [ - "bitflags", + "bitflags 2.13.0", "memchr", "miette", "strum", diff --git a/cli/Cargo.toml b/cli/Cargo.toml index 990f1179..b5afec05 100644 --- a/cli/Cargo.toml +++ b/cli/Cargo.toml @@ -63,6 +63,9 @@ windows-native-keyring-store = "1" serde_json = "1" sha2 = "0.11" +[dev-dependencies] +quint-connect = "0.1.2" + [lints] workspace = true diff --git a/cli/src/services/mutation_trace/mbt/driver.rs b/cli/src/services/mutation_trace/mbt/driver.rs new file mode 100644 index 00000000..8fe3c2d4 --- /dev/null +++ b/cli/src/services/mutation_trace/mbt/driver.rs @@ -0,0 +1,230 @@ +//! MBT driver: connects Quint Connect's generated/replayed traces to the +//! real `protocol.rs` transition functions. +//! +//! [`MutationCursorDriver::step`] dispatches on the `MbtAction` variant Quint +//! recorded — never on a before/after state diff — and every arm +//! unconditionally calls the corresponding `protocol::*` function with the +//! transported arguments, including on an `MbtAction` variant Quint produced +//! from a guarded/no-op path (T02's `mbtStutterAs` instrumentation): the +//! driver has no way to distinguish that case from a real transition, and +//! must not try to, since replaying the guarded call and comparing the +//! resulting no-op state against Quint is the point of the regressions in +//! T05. + +use std::collections::{BTreeMap, BTreeSet}; + +use quint_connect::{switch, Config, Driver, Result, State, Step}; + +use super::super::protocol; +use super::super::types::{ + boundary_worktree, ActorKind, AttemptId, AttemptState, AttemptStatus, Boundary, FailureKind, + ProtocolState, ScopeId, ScopeState, ScopeStatus, TreeId, WorktreeId, WorktreeState, +}; +use super::model::{ + ModelState, WireAttemptId, WireBoundary, WireScopeId, WireTreeId, WireWorktreeId, +}; + +fn worktree(id: &str) -> WorktreeId { + WorktreeId(id.to_string()) +} + +fn scope(id: &str) -> ScopeId { + ScopeId(id.to_string()) +} + +fn tree(id: &str) -> TreeId { + TreeId(id.to_string()) +} + +fn attempt_id(id: &str) -> AttemptId { + AttemptId(id.to_string()) +} + +/// Replays a trace generated from/for `spec/mutation_cursor.qnt` through the +/// real `protocol.rs` functions. +/// +/// Holds exactly the state the plan authorizes: the pure protocol state +/// (refines `worktrees`/`scopes`/`externalTaint`/`processedEvents`/ +/// `attempts`/`mutationEvents`) plus `worktree_trees`, the driver-only +/// analogue of Quint's `worktreeTrees` var — the observed-tree input +/// `prepare`/`recover` take explicitly, since the pure kernel performs no Git +/// I/O. `MbtMutate` is the only action that touches `worktree_trees`; every +/// other action calls a `protocol::*` function, never reimplementing its +/// logic. +pub(super) struct MutationCursorDriver { + protocol: ProtocolState, + worktree_trees: BTreeMap, +} + +impl MutationCursorDriver { + /// Exactly `spec/mutation_cursor.qnt`'s `init`: both worktrees at + /// `Tree0`/revision `0`/healthy/no-rebaseline, all four scopes + /// `NeverSeen` with `scopeActor`'s fixed partition (`Scope0`/`Scope1` + /// Claude Code and `Scope2` Codex on `WT0`, `Scope3` `OpenCode` on `WT1`), + /// and all six attempts `Available` with the same placeholder + /// `Flush(WT0)`/revision `0`/`Tree0`/`Tree0` baseline Quint's `init` + /// assigns every `AttemptId`. + fn init() -> Self { + let wt0 = worktree("wt0"); + let wt1 = worktree("wt1"); + + let mut worktrees = BTreeMap::new(); + let mut worktree_trees = BTreeMap::new(); + for id in [&wt0, &wt1] { + worktrees.insert( + id.clone(), + WorktreeState { + cursor_tree: tree("tree0"), + revision: 0, + tainted: false, + failure_kind: FailureKind::Healthy, + needs_rebaseline: false, + }, + ); + worktree_trees.insert(id.clone(), tree("tree0")); + } + + let scope_partition: [(&str, &WorktreeId, ActorKind); 4] = [ + ("scope0", &wt0, ActorKind::ClaudeCode), + ("scope1", &wt0, ActorKind::ClaudeCode), + ("scope2", &wt0, ActorKind::Codex), + ("scope3", &wt1, ActorKind::OpenCode), + ]; + let mut scopes = BTreeMap::new(); + for (id, owning_worktree, actor_kind) in scope_partition { + scopes.insert( + scope(id), + ScopeState { + status: ScopeStatus::NeverSeen, + actor_kind, + worktree_id: owning_worktree.clone(), + }, + ); + } + + let mut attempts = BTreeMap::new(); + for id in [ + "attempt0", "attempt1", "attempt2", "attempt3", "attempt4", "attempt5", + ] { + attempts.insert( + attempt_id(id), + AttemptState { + status: AttemptStatus::Available, + boundary: Boundary::Flush { + worktree: wt0.clone(), + }, + expected_revision: 0, + before_tree: tree("tree0"), + after_tree: tree("tree0"), + }, + ); + } + + Self { + protocol: ProtocolState { + worktrees, + scopes, + external_taint: BTreeSet::new(), + processed_events: BTreeSet::new(), + attempts, + mutation_events: BTreeSet::new(), + }, + worktree_trees, + } + } + + fn mbt_init(&mut self) { + *self = Self::init(); + } + + fn mbt_mutate(&mut self, worktree: WorktreeId, tree: TreeId) { + self.worktree_trees.insert(worktree, tree); + } + + fn observed_tree(&self, worktree: &WorktreeId) -> TreeId { + self.worktree_trees + .get(worktree) + .cloned() + .expect("every worktree tracked since init has an observed tree") + } + + fn mbt_prepare(&mut self, attempt: AttemptId, boundary: Boundary) { + let worktree = boundary_worktree(&boundary, &self.protocol.scopes) + .expect("every boundary's scope is registered by init, matching Quint's static scopeWorktree partition"); + let observed_tree = self.observed_tree(&worktree); + self.protocol = protocol::prepare(&self.protocol, attempt, boundary, observed_tree); + } + + fn mbt_commit(&mut self, attempt: &AttemptId) { + self.protocol = protocol::commit(&self.protocol, attempt).state; + } + + fn mbt_taint(&mut self, worktree: &WorktreeId) { + self.protocol = protocol::taint(&self.protocol, worktree); + } + + fn mbt_database_failure(&mut self, worktree: &WorktreeId) { + self.protocol = protocol::database_failure(&self.protocol, worktree); + } + + fn mbt_abandon(&mut self, scope: &ScopeId) { + self.protocol = protocol::abandon(&self.protocol, scope); + } + + fn mbt_recover(&mut self, worktree: &WorktreeId) { + let observed_tree = self.observed_tree(worktree); + self.protocol = protocol::recover(&self.protocol, worktree, observed_tree); + } + + /// Refines the explicit top-level `stutter` action: no state change. + #[allow(clippy::unused_self)] + fn mbt_stutter(&self) {} +} + +impl Default for MutationCursorDriver { + fn default() -> Self { + Self::init() + } +} + +impl Driver for MutationCursorDriver { + type State = ModelState; + + fn config() -> Config { + Config { + state: &[], + nondet: &["mbtAction"], + } + } + + fn step(&mut self, step: &Step) -> Result { + switch!(step { + MbtInit => self.mbt_init(), + MbtMutate(worktree: WireWorktreeId, tree: WireTreeId) => + self.mbt_mutate(worktree.into(), tree.into()), + MbtPrepare(attempt: WireAttemptId, boundary: WireBoundary) => + self.mbt_prepare(attempt.into(), boundary.into()), + MbtCommit(attempt: WireAttemptId) => self.mbt_commit(&attempt.into()), + MbtTaint(worktree: WireWorktreeId) => self.mbt_taint(&worktree.into()), + MbtDatabaseFailure(worktree: WireWorktreeId) => + self.mbt_database_failure(&worktree.into()), + MbtAbandon(scope: WireScopeId) => self.mbt_abandon(&scope.into()), + MbtRecover(worktree: WireWorktreeId) => self.mbt_recover(&worktree.into()), + MbtStutter => self.mbt_stutter(), + }) + } +} + +impl State for ModelState { + fn from_driver(driver: &MutationCursorDriver) -> Result { + Ok(ModelState { + worktrees: driver.protocol.worktrees.clone(), + scopes: driver.protocol.scopes.clone(), + worktree_trees: driver.worktree_trees.clone(), + external_taint: driver.protocol.external_taint.clone(), + processed_events: driver.protocol.processed_events.clone(), + attempts: driver.protocol.attempts.clone(), + mutation_events: driver.protocol.mutation_events.clone(), + }) + } +} diff --git a/cli/src/services/mutation_trace/mbt/mod.rs b/cli/src/services/mutation_trace/mbt/mod.rs new file mode 100644 index 00000000..99e8c3d1 --- /dev/null +++ b/cli/src/services/mutation_trace/mbt/mod.rs @@ -0,0 +1,13 @@ +//! Model-based testing harness connecting the verified +//! `spec/mutation_cursor.qnt` model to the pure Rust refinement in +//! `super::protocol`/`super::types` via Quint Connect. +//! +//! Test-only (`#[cfg(test)]`, gated from `mutation_trace/mod.rs`): no +//! production code depends on this module, and it introduces no Git, +//! database, filesystem, environment, network, async, or lock I/O of its +//! own — every state transition is delegated to `super::protocol`'s pure +//! functions. + +mod driver; +mod model; +mod tests; diff --git a/cli/src/services/mutation_trace/mbt/model.rs b/cli/src/services/mutation_trace/mbt/model.rs new file mode 100644 index 00000000..1d145e75 --- /dev/null +++ b/cli/src/services/mutation_trace/mbt/model.rs @@ -0,0 +1,495 @@ +//! Comparable model state and Quint ITF wire types for the MBT harness. +//! +//! Quint Connect deserializes trace state via the [`itf`] wire format, where +//! sum types serialize as `{ tag, value }` records (see the `quint-connect` +//! crate README's "Enums" section). The `Wire*` types here mirror that exact +//! shape for every Quint type reachable from `spec/mutation_cursor.qnt`'s +//! comparable state, then convert into this crate's own domain types +//! (`super::super::types`) via `From` impls, so [`ModelState`] and the values +//! [`super::driver::MutationCursorDriver`] extracts stay expressed in the +//! same production types the rest of `mutation_trace` uses. +//! +//! [`WireModelState`] and every semantic `Wire*` record use +//! `#[serde(deny_unknown_fields)]`, so a new Quint state variable or record +//! field fails deserialization instead of being silently dropped. `spec/ +//! mutation_cursor.qnt`'s verification-only variables (`scopeStartCount`, +//! `everTerminal`, every `*History` set, `evidenceAttempts`, `mbtAction`) are +//! given explicit [`IgnoredAny`] fields on [`WireModelState`], so they are a +//! deliberate exclusion from the compared state rather than an accidental +//! one — adding a new Quint variable forces a choice between modeling it as +//! semantic state or classifying it here as verification-only. + +use std::collections::{BTreeMap, BTreeSet}; + +use serde::{de::IgnoredAny, Deserialize}; + +use super::super::types::{ + ActorKind, AttemptId, AttemptState, AttemptStatus, Attribution, Boundary, EventId, EventKey, + FailureKind, MutationEvent, ScopeId, ScopeState, ScopeStatus, TreeId, WorktreeId, + WorktreeState, +}; + +// --------------------------------------------------------------------- +// Finite identity wire types (`spec/mutation_cursor.qnt`'s unit sum types) +// --------------------------------------------------------------------- + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireWorktreeId { + WT0, + WT1, +} + +impl From for WorktreeId { + fn from(value: WireWorktreeId) -> Self { + WorktreeId( + match value { + WireWorktreeId::WT0 => "wt0", + WireWorktreeId::WT1 => "wt1", + } + .to_string(), + ) + } +} + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireScopeId { + Scope0, + Scope1, + Scope2, + Scope3, +} + +impl From for ScopeId { + fn from(value: WireScopeId) -> Self { + ScopeId( + match value { + WireScopeId::Scope0 => "scope0", + WireScopeId::Scope1 => "scope1", + WireScopeId::Scope2 => "scope2", + WireScopeId::Scope3 => "scope3", + } + .to_string(), + ) + } +} + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireTreeId { + Tree0, + Tree1, + Tree2, + Tree3, +} + +impl From for TreeId { + fn from(value: WireTreeId) -> Self { + TreeId( + match value { + WireTreeId::Tree0 => "tree0", + WireTreeId::Tree1 => "tree1", + WireTreeId::Tree2 => "tree2", + WireTreeId::Tree3 => "tree3", + } + .to_string(), + ) + } +} + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireEventId { + Event0, + Event1, + Event2, + Event3, + Event4, + Event5, + Event6, + Event7, + Event8, + Event9, +} + +impl From for EventId { + fn from(value: WireEventId) -> Self { + EventId( + match value { + WireEventId::Event0 => "event0", + WireEventId::Event1 => "event1", + WireEventId::Event2 => "event2", + WireEventId::Event3 => "event3", + WireEventId::Event4 => "event4", + WireEventId::Event5 => "event5", + WireEventId::Event6 => "event6", + WireEventId::Event7 => "event7", + WireEventId::Event8 => "event8", + WireEventId::Event9 => "event9", + } + .to_string(), + ) + } +} + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireAttemptId { + Attempt0, + Attempt1, + Attempt2, + Attempt3, + Attempt4, + Attempt5, +} + +impl From for AttemptId { + fn from(value: WireAttemptId) -> Self { + AttemptId( + match value { + WireAttemptId::Attempt0 => "attempt0", + WireAttemptId::Attempt1 => "attempt1", + WireAttemptId::Attempt2 => "attempt2", + WireAttemptId::Attempt3 => "attempt3", + WireAttemptId::Attempt4 => "attempt4", + WireAttemptId::Attempt5 => "attempt5", + } + .to_string(), + ) + } +} + +// --------------------------------------------------------------------- +// Enum wire types +// --------------------------------------------------------------------- + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireActorKind { + ClaudeCode, + Codex, + OpenCode, + Pi, +} + +impl From for ActorKind { + fn from(value: WireActorKind) -> Self { + match value { + WireActorKind::ClaudeCode => ActorKind::ClaudeCode, + WireActorKind::Codex => ActorKind::Codex, + WireActorKind::OpenCode => ActorKind::OpenCode, + WireActorKind::Pi => ActorKind::Pi, + } + } +} + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireFailureKind { + Healthy, + SnapshotFailure, +} + +impl From for FailureKind { + fn from(value: WireFailureKind) -> Self { + match value { + WireFailureKind::Healthy => FailureKind::Healthy, + WireFailureKind::SnapshotFailure => FailureKind::SnapshotFailure, + } + } +} + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireScopeStatus { + NeverSeen, + Active, + Closed, + Abandoned, +} + +impl From for ScopeStatus { + fn from(value: WireScopeStatus) -> Self { + match value { + WireScopeStatus::NeverSeen => ScopeStatus::NeverSeen, + WireScopeStatus::Active => ScopeStatus::Active, + WireScopeStatus::Closed => ScopeStatus::Closed, + WireScopeStatus::Abandoned => ScopeStatus::Abandoned, + } + } +} + +#[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag")] +pub(super) enum WireAttemptStatus { + Available, + Prepared, + Committed, + Rejected, +} + +impl From for AttemptStatus { + fn from(value: WireAttemptStatus) -> Self { + match value { + WireAttemptStatus::Available => AttemptStatus::Available, + WireAttemptStatus::Prepared => AttemptStatus::Prepared, + WireAttemptStatus::Committed => AttemptStatus::Committed, + WireAttemptStatus::Rejected => AttemptStatus::Rejected, + } + } +} + +// --------------------------------------------------------------------- +// Structured wire types +// --------------------------------------------------------------------- + +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(deny_unknown_fields)] +pub(super) struct WireScopeEvent { + pub scope: WireScopeId, + pub event: WireEventId, +} + +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag", content = "value")] +pub(super) enum WireBoundary { + Start(WireScopeEvent), + Advance(WireScopeEvent), + Close(WireScopeEvent), + Flush(WireWorktreeId), +} + +impl From for Boundary { + fn from(value: WireBoundary) -> Self { + match value { + WireBoundary::Start(data) => Boundary::Start { + scope: data.scope.into(), + event: data.event.into(), + }, + WireBoundary::Advance(data) => Boundary::Advance { + scope: data.scope.into(), + event: data.event.into(), + }, + WireBoundary::Close(data) => Boundary::Close { + scope: data.scope.into(), + event: data.event.into(), + }, + WireBoundary::Flush(worktree) => Boundary::Flush { + worktree: worktree.into(), + }, + } + } +} + +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(tag = "tag", content = "value")] +pub(super) enum WireAttribution { + IneligibleUnscoped, + AiExclusive(WireScopeId), + AiContended, +} + +impl From for Attribution { + fn from(value: WireAttribution) -> Self { + match value { + WireAttribution::IneligibleUnscoped => Attribution::IneligibleUnscoped, + WireAttribution::AiExclusive(scope) => Attribution::AiExclusive(scope.into()), + WireAttribution::AiContended => Attribution::AiContended, + } + } +} + +#[derive(Clone, Debug, Eq, PartialEq, Deserialize)] +#[serde(rename_all = "camelCase", deny_unknown_fields)] +pub(super) struct WireWorktreeState { + pub cursor_tree: WireTreeId, + pub revision: u64, + pub tainted: bool, + pub failure_kind: WireFailureKind, + pub needs_rebaseline: bool, +} + +impl From for WorktreeState { + fn from(value: WireWorktreeState) -> Self { + WorktreeState { + cursor_tree: value.cursor_tree.into(), + revision: value.revision, + tainted: value.tainted, + failure_kind: value.failure_kind.into(), + needs_rebaseline: value.needs_rebaseline, + } + } +} + +#[derive(Clone, Debug, Eq, PartialEq, Deserialize)] +#[serde(rename_all = "camelCase", deny_unknown_fields)] +pub(super) struct WireScopeState { + pub status: WireScopeStatus, + pub actor_kind: WireActorKind, + pub worktree_id: WireWorktreeId, +} + +impl From for ScopeState { + fn from(value: WireScopeState) -> Self { + ScopeState { + status: value.status.into(), + actor_kind: value.actor_kind.into(), + worktree_id: value.worktree_id.into(), + } + } +} + +#[derive(Clone, Debug, Eq, PartialEq, Deserialize)] +#[serde(rename_all = "camelCase", deny_unknown_fields)] +pub(super) struct WireAttemptState { + pub status: WireAttemptStatus, + pub boundary: WireBoundary, + pub expected_revision: u64, + pub before_tree: WireTreeId, + pub after_tree: WireTreeId, +} + +impl From for AttemptState { + fn from(value: WireAttemptState) -> Self { + AttemptState { + status: value.status.into(), + boundary: value.boundary.into(), + expected_revision: value.expected_revision, + before_tree: value.before_tree.into(), + after_tree: value.after_tree.into(), + } + } +} + +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(rename_all = "camelCase", deny_unknown_fields)] +pub(super) struct WireEventKey { + pub scope_id: WireScopeId, + pub event_id: WireEventId, +} + +impl From for EventKey { + fn from(value: WireEventKey) -> Self { + EventKey { + scope_id: value.scope_id.into(), + event_id: value.event_id.into(), + } + } +} + +#[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(rename_all = "camelCase", deny_unknown_fields)] +pub(super) struct WireMutationEvent { + pub worktree_id: WireWorktreeId, + pub revision: u64, + pub before_tree: WireTreeId, + pub after_tree: WireTreeId, + pub active_scopes: BTreeSet, + pub tainted: bool, + pub failure_kind: WireFailureKind, + pub attribution: WireAttribution, + pub boundary: WireBoundary, +} + +impl From for MutationEvent { + fn from(value: WireMutationEvent) -> Self { + MutationEvent { + worktree_id: value.worktree_id.into(), + revision: value.revision, + before_tree: value.before_tree.into(), + after_tree: value.after_tree.into(), + active_scopes: value.active_scopes.into_iter().map(Into::into).collect(), + tainted: value.tainted, + failure_kind: value.failure_kind.into(), + attribution: value.attribution.into(), + boundary: value.boundary.into(), + } + } +} + +// --------------------------------------------------------------------- +// Comparable model state +// --------------------------------------------------------------------- + +/// The comparable subset of `spec/mutation_cursor.qnt`'s state: every +/// variable named by AC5 (`worktrees`, `scopes`, `worktreeTrees`, +/// `externalTaint`, `processedEvents`, `attempts`, `mutationEvents`), +/// expressed in this crate's own domain types. Every other Quint variable is +/// verification-only and is dropped via an explicit [`IgnoredAny`] field on +/// [`WireModelState`], not by serde's default unknown-field handling — see +/// that type. +#[derive(Debug, Eq, PartialEq, Deserialize)] +#[serde(from = "WireModelState")] +pub struct ModelState { + pub worktrees: BTreeMap, + pub scopes: BTreeMap, + pub worktree_trees: BTreeMap, + pub external_taint: BTreeSet, + pub processed_events: BTreeSet, + pub attempts: BTreeMap, + pub mutation_events: BTreeSet, +} + +/// Mirrors every `var` in `spec/mutation_cursor.qnt`'s state, so adding a +/// new Quint variable without updating this struct fails deserialization +/// (`deny_unknown_fields`) instead of silently vanishing. Verification-only +/// variables are still accepted, but only via an explicit [`IgnoredAny`] +/// field — modeling a new Quint variable here as `IgnoredAny` is a +/// deliberate "not semantic state" decision, not an oversight. +#[derive(Deserialize)] +#[serde(rename_all = "camelCase", deny_unknown_fields)] +struct WireModelState { + // Semantic state: compared against Rust via `ModelState`. + worktrees: BTreeMap, + scopes: BTreeMap, + worktree_trees: BTreeMap, + external_taint: BTreeSet, + processed_events: BTreeSet, + attempts: BTreeMap, + mutation_events: BTreeSet, + + // Verification-only: present in Quint's state for the model checker, + // not part of the Rust refinement comparison. + scope_start_count: IgnoredAny, + ever_terminal: IgnoredAny, + cursor_history: IgnoredAny, + protocol_history: IgnoredAny, + scope_history: IgnoredAny, + abandon_history: IgnoredAny, + start_history: IgnoredAny, + recovery_history: IgnoredAny, + taint_history: IgnoredAny, + evidence_attempts: IgnoredAny, + mbt_action: IgnoredAny, +} + +impl From for ModelState { + fn from(value: WireModelState) -> Self { + ModelState { + worktrees: value + .worktrees + .into_iter() + .map(|(id, state)| (id.into(), state.into())) + .collect(), + scopes: value + .scopes + .into_iter() + .map(|(id, state)| (id.into(), state.into())) + .collect(), + worktree_trees: value + .worktree_trees + .into_iter() + .map(|(id, tree)| (id.into(), tree.into())) + .collect(), + external_taint: value.external_taint.into_iter().map(Into::into).collect(), + processed_events: value.processed_events.into_iter().map(Into::into).collect(), + attempts: value + .attempts + .into_iter() + .map(|(id, state)| (id.into(), state.into())) + .collect(), + mutation_events: value.mutation_events.into_iter().map(Into::into).collect(), + } + } +} diff --git a/cli/src/services/mutation_trace/mbt/tests.rs b/cli/src/services/mutation_trace/mbt/tests.rs new file mode 100644 index 00000000..a5b52106 --- /dev/null +++ b/cli/src/services/mutation_trace/mbt/tests.rs @@ -0,0 +1,163 @@ +//! Deterministic Quint Connect replays through the real `protocol.rs`. + +use quint_connect::{quint_run, quint_test}; + +use super::driver::MutationCursorDriver; + +/// Replays `testMbtDriverTransportsNonDefaultArguments` +/// (`spec/mutation_cursor.qnt`): `mutate(WT1, Tree3)` → +/// `prepare(Attempt5, Flush(WT1))` → `commitAttempt(Attempt5)`. Every value +/// here — worktree, tree, attempt, and boundary kind — differs from the +/// `WT0`/`Tree0`/`Tree1`/`Attempt0`/`Attempt1`/`Start`/`Advance`/`Close` +/// defaults the spec's other named scenarios use, so a passing replay proves +/// the driver transports the trace's actual concrete arguments into +/// `protocol::prepare`/`protocol::commit` rather than guessing or defaulting +/// them. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testMbtDriverTransportsNonDefaultArguments", + max_samples = 1 +)] +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", + max_samples = 1 +)] +fn mutation_cursor_start_observes_before_activation() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testCloseObservesBeforeDeactivation`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testCloseObservesBeforeDeactivation", + max_samples = 1 +)] +fn mutation_cursor_close_observes_before_deactivation() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testContendedIntervalsRemainAiContended`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testContendedIntervalsRemainAiContended", + max_samples = 1 +)] +fn mutation_cursor_contended_intervals_remain_ai_contended() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testNoChangeHookReplayCannotStealFutureChange`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testNoChangeHookReplayCannotStealFutureChange", + max_samples = 1 +)] +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", + max_samples = 1 +)] +fn mutation_cursor_concurrent_observations_have_one_winner() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testTaintInvalidatesPreparedObservation`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testTaintInvalidatesPreparedObservation", + max_samples = 1 +)] +fn mutation_cursor_taint_invalidates_prepared_observation() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testRecoveryEstablishesBaseline`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testRecoveryEstablishesBaseline", + max_samples = 1 +)] +fn mutation_cursor_recovery_establishes_baseline() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testClosedScopeCannotReactivate`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testClosedScopeCannotReactivate", + max_samples = 1 +)] +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", + max_samples = 1 +)] +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", + max_samples = 1 +)] +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() +} + +/// Coverage backstop: `test = "test.*"` is passed through unescaped into +/// `quint test`'s `--match` as `^test.*$`, so this replays every top-level +/// `test...`-named `run` in `spec/mutation_cursor.qnt` — not just the +/// individually named scenarios above — through the real `protocol.rs`. Each +/// matched `run` is deterministic, so `max_samples = 1`. This exists so a new +/// named Quint scenario is automatically exercised here without also +/// requiring a new hand-written Rust wrapper; the individually named tests +/// above stay for readable `cargo test` failure output on the scenarios +/// worth naming. +#[quint_test(spec = "../spec/mutation_cursor.qnt", test = "test.*", max_samples = 1)] +fn mutation_cursor_all_named_scenarios_refine_rust_protocol() -> impl Driver { + MutationCursorDriver::default() +} diff --git a/cli/src/services/mutation_trace/mod.rs b/cli/src/services/mutation_trace/mod.rs index 51dc24a6..5544f4aa 100644 --- a/cli/src/services/mutation_trace/mod.rs +++ b/cli/src/services/mutation_trace/mod.rs @@ -158,5 +158,8 @@ pub mod protocol; pub mod types; +#[cfg(test)] +mod mbt; + #[cfg(test)] mod tests; diff --git a/context/architecture.md b/context/architecture.md index ccfdb91c..d289b7e8 100644 --- a/context/architecture.md +++ b/context/architecture.md @@ -188,7 +188,7 @@ Investigations T08 (`turso default-features = false`) and T09 (isolating the with rationale in the benchmark doc. Final after-change numbers and remaining bottlenecks are captured in T11. -This phase establishes compile-safe extension seams with a dependency baseline (`anyhow`, `chrono`, `clap`, `clap_complete`, `dirs`, `hmac`, `inquire`, `jsonschema`, `keyring-core`, `murmur3`, `owo-colors`, `rand`, `reqwest`, `serde`, `serde_json`, `sha2`, `tokio`, `toml`, `tracing`, `turso`, `uuid`, plus target-specific keyring backends); no CLI dev-dependencies are currently declared. Per-user local Turso DB and Agent Trace DB bootstrap/health coverage now exist through setup/doctor flows; the user-invocable `sce sync` command is now fully implemented including rendering (see above), and broader runtime integrations remain deferred. +This phase establishes compile-safe extension seams with a dependency baseline (`anyhow`, `chrono`, `clap`, `clap_complete`, `dirs`, `hmac`, `inquire`, `jsonschema`, `keyring-core`, `murmur3`, `owo-colors`, `rand`, `reqwest`, `serde`, `serde_json`, `sha2`, `tokio`, `toml`, `tracing`, `turso`, `uuid`, plus target-specific keyring backends); `[dev-dependencies]` now carries `quint-connect`, dev/test-only, for the in-progress `mutation-cursor-quint-connect` model-based-testing harness. Per-user local Turso DB and Agent Trace DB bootstrap/health coverage now exist through setup/doctor flows; the user-invocable `sce sync` command is now fully implemented including rendering (see above), and broader runtime integrations remain deferred. ## SCE plan/code role boundary diff --git a/context/cli/mutation-trace-quint-connect.md b/context/cli/mutation-trace-quint-connect.md new file mode 100644 index 00000000..5e31ea01 --- /dev/null +++ b/context/cli/mutation-trace-quint-connect.md @@ -0,0 +1,250 @@ +# Quint Connect model-based testing (`mutation_trace::mbt`) + +`#[cfg(test)]`-only harness that continuously checks the pure Rust refinement +at [`cli/src/services/mutation_trace/protocol.rs`](mutation-trace-protocol.md) +against the verified `spec/mutation_cursor.qnt` model, using +[Quint Connect](https://github.com/informalsystems/quint-connect) (crate +`quint-connect` 0.1.2, `[dev-dependencies]`-only — never a production one). +It replaces the one-time manual translation the base protocol module was +reviewed against with a driver that replays real Quint traces through the +real `prepare`/`commit`/`taint`/`database_failure`/`abandon`/`recover` +functions and compares state after every step. It introduces no `store.rs`, +`coordinator.rs`, `git_snapshot.rs`, database, Git, filesystem, network, or +hook integration — `protocol.rs` stays exactly as pure as +[mutation-trace-protocol.md](mutation-trace-protocol.md) describes it. + +## Pipeline + +```mermaid +flowchart TD + action["Quint semantic action\n(mutate / prepare / commitAttempt / taint /\ndatabaseFailure / abandon / recover / stutter)"] + mbtAction["verification-only mbtAction: MbtAction\n(records the invoked operation + its arguments\non EVERY branch, including guarded no-ops)"] + connect["Quint Connect\n(generated random traces, or a named\ndeterministic `run` scenario)"] + driver["MutationCursorDriver::step\n(switch! dispatches on the MbtAction variant —\nnever on a before/after state diff)"] + protocol["real protocol::* call\n(prepare / commit / taint / database_failure /\nabandon / recover — never reimplemented)"] + modelstate["ModelState projection\n(worktrees / scopes / worktreeTrees /\nexternalTaint / processedEvents /\nattempts / mutationEvents)"] + compare["compared against Quint's own state\nafter every step"] + + action --> mbtAction --> connect --> driver --> protocol --> modelstate --> compare +``` + +Every action sets `mbtAction'` to its own variant on every branch, including +guarded/no-op ones, so the driver always knows which operation Quint +selected and dispatches to the matching `protocol::*` function +unconditionally — never inferring arguments from state, never skipping a +call because Quint's own state happened not to change. + +## Why `mbtAction` exists and is excluded from comparison + +Quint Connect needs a nondeterministic-choice path it can extract and hand to +the driver as a typed action (`Config { nondet: &["mbtAction"], state: &[] }` +in [`driver.rs`](../../cli/src/services/mutation_trace/mbt/driver.rs)). +`mbtAction: MbtAction` is a verification-only state variable added to +`spec/mutation_cursor.qnt` purely to carry that choice — never read by any +other action, invariant, or production logic, and never participating in +freshness, lifecycle, attribution, revisions, cursor movement, taint, +recovery, or mutation-evidence semantics. + +Because it is transport metadata, `mbtAction` has no field anywhere in the +`mbt/model.rs` wire types +([`WireModelState`](../../cli/src/services/mutation_trace/mbt/model.rs)). When +the full top-level Quint state record deserializes, `serde`'s default +unknown-field handling silently drops it — keeping it out of `ModelState`, +the struct actually compared against the driver's projected state. + +## Operation identity vs. `MbtStutter` + +`MbtAction` identifies the invoked operation and its concrete arguments, +never whether that invocation changed anything. `prepare`, `taint`, +`databaseFailure`, `abandon`, and `recover` each guard their real transition +and, on the guarded path, previously fell through to the spec's shared +top-level `stutter` action. Naively wiring `mbtAction' = MbtStutter` into +that shared path would have erased which operation was actually invoked and +silently stopped the MBT harness from exercising Rust's guard behavior on +exactly the paths where refinement bugs hide. + +Instead, a shared `mbtStutterAs(taken: MbtAction): bool` helper (identical to +the old `stutter` body, parameterized on the `MbtAction` to record) replaced +the inline field list `stutter` used to duplicate. Each guarded branch calls +`mbtStutterAs((...))` with its real arguments, leaving +every other semantic state assignment exactly as `stutter` already produced +it. `commitAttempt`'s own not-accepted path got the same treatment directly. +`stutter` itself is now `mbtStutterAs(MbtStutter)`, so `MbtStutter` is +reachable only from the explicit top-level `stutter` action — never as a +byproduct of another operation's internal guard branch. + +Two deterministic regressions in `mbt/tests.rs` prove this holds: replaying +`Attempt0` through `Start` then `Advance` (the second `prepare` guards since +the attempt is no longer `Available`) and replaying `recover(WT0)` from +`init` (guards immediately — nothing is tainted or needs rebaseline). Both +prove the driver still calls the real `protocol::prepare`/`protocol::recover` +function on the guarded step and independently reaches the same no-op +outcome Quint does. + +## Record-payload action encoding + +Quint Connect's custom sum-type decoder distinguishes a unit variant from a +record variant, so every argument-carrying `MbtAction` variant is a record — +even single-field ones (`MbtMutate({worktree, tree})`, +`MbtPrepare({attempt, boundary})`, `MbtCommit({attempt})`, +`MbtTaint({worktree})`, `MbtDatabaseFailure({worktree})`, +`MbtAbandon({scope})`, `MbtRecover({worktree})`) — and only the two truly +argument-free variants (`MbtInit`, `MbtStutter`) are bare, matching the +`itf`/`quint-connect` `#[serde(tag = "tag", content = "value")]` wire shape. +Its nondet-pick extraction (`extract_nondet_from_sum_type`) accepts a +`Value::Record` directly for both the top-level nondet-picked action and +nested record fields (e.g. `Boundary`'s `Start`/`Advance`/`Close` variants +nested inside `MbtPrepare`). + +## Finite ID mapping + +The Quint model's identity types (`WorktreeId`, `ScopeId`, `TreeId`, +`EventId`, `AttemptId`) are bounded enums (`WT0`/`WT1`, `Scope0`-`Scope3`, +`Tree0`-`Tree3`, `Event0`-`Event9`, `Attempt0`-`Attempt5`). `mbt/model.rs` +defines one `Wire*` enum per identity type mirroring those exact members, +each converting via `From` into this crate's own opaque `String`-wrapping +newtypes (e.g. `WireWorktreeId::WT0 -> WorktreeId("wt0")`) — the same +production types [mutation-trace-protocol.md](mutation-trace-protocol.md) +describes. This mapping exists only inside the test-only `mbt` module. + +## Comparable state + +`ModelState` (`mbt/model.rs`) holds exactly the fields AC5 named: + +- `worktrees: BTreeMap` +- `scopes: BTreeMap` +- `worktree_trees: BTreeMap` (refines `worktreeTrees` — + the driver-only observed-tree input, since the pure kernel does no Git I/O) +- `external_taint: BTreeSet` +- `processed_events: BTreeSet` +- `attempts: BTreeMap` +- `mutation_events: BTreeSet`, each with its full field set + +Every verification-only history the spec tracks for its own invariant +checking (`cursorHistory`, `protocolHistory`, `scopeHistory`, +`abandonHistory`, `startHistory`, `recoveryHistory`, `taintHistory`, +`evidenceAttempts`, `scopeStartCount`, `everTerminal`, `mbtAction`) has no +field in `ModelState` and is dropped the same way `mbtAction` is. + +## `randomPrepare` stays one `step` branch + +`step`'s eight top-level alternatives +(`randomMutate`/`randomPrepare`/`randomCommit`/`randomTaint`/`randomRecover`/ +`randomDatabaseFailure`/`randomAbandon`/`stutter`) are unchanged by this +harness. `prepare` unconditionally sets `mbtAction' = +MbtPrepare({attempt, boundary})` on both its accepted and guarded paths, and +`boundary` there is always the exact concrete `Boundary` value whichever of +`randomPrepare`'s five inner `any` alternatives fired — so the driver already +recovers which boundary kind Quint selected from the `MbtPrepare` variant +alone. No dedicated `PrepareKind`-style nondet choice was needed. + +## Driver and test coverage + +[`driver.rs`](../../cli/src/services/mutation_trace/mbt/driver.rs) defines +`MutationCursorDriver { protocol: ProtocolState, worktree_trees: +BTreeMap }`, an `init()` matching Quint's `init` exactly, +and `Driver::step` dispatching via `switch!` on every `MbtAction` variant. +Every arm unconditionally calls its `protocol::*` function with the +transported, converted arguments; `MbtMutate` alone doesn't call into +`protocol.rs` (it only updates `worktree_trees`); `MbtStutter` calls a +dedicated no-op method rather than being inlined. + +[`mbt/tests.rs`](../../cli/src/services/mutation_trace/mbt/tests.rs) wires: + +- One non-default-values smoke replay (`WT1`/`Tree3`/`Attempt5`/`Flush(WT1)`, + scenario `testMbtDriverTransportsNonDefaultArguments`), proving the driver + transports a trace's actual concrete arguments rather than guessing or + defaulting them. +- All eight named deterministic scenarios already defined in the spec + (`testStartObservesBeforeActivation`, `testCloseObservesBeforeDeactivation`, + `testContendedIntervalsRemainAiContended`, + `testNoChangeHookReplayCannotStealFutureChange`, + `testConcurrentObservationsHaveOneWinner`, + `testTaintInvalidatesPreparedObservation`, `testRecoveryEstablishesBaseline`, + `testClosedScopeCannotReactivate`) via `#[quint_test]`, expressed as the + same semantic-action call chains the spec already uses — no duplicated + scenario logic in Rust. +- The two guarded-no-op regressions (`testMbtGuardedPrepareInvokesRealPrepare`, + `testMbtGuardedRecoverInvokesRealRecover`). +- `mutation_cursor_generated_traces_refine_rust_protocol`, a + `#[quint_run(max_samples = 500, max_steps = 30)]` test comparing + `ModelState` against Quint's own state after every step across 500 + randomized traces up to 30 steps deep. Reproducible by fixing `QUINT_SEED` + and re-running — the same seed always regenerates the same trace set. + +## `u64` revision boundary + +`WorktreeState::revision` is Rust `u64`, refining Quint's unbounded `int` +(see [mutation-trace-revision-refinement.md](mutation-trace-revision-refinement.md) +for the full `next_revision` checked-arithmetic contract). This harness +replays real traces, so it incidentally exercises `next_revision`'s guarded +paths whenever a trace reaches them, but does not specifically target +`revision: u64::MAX` — Quint's unbounded `int` domain cannot represent or +generate traces toward that boundary. The dedicated no-wrap regressions in +`mutation-trace-revision-refinement.md` remain the sole targeted coverage for +it; this harness's coverage is incidental, not a substitute. + +## CI: two Nix checks, both need Quint + +`mutation_trace::mbt` is registered as an ordinary `#[cfg(test)] mod mbt;` +(gated behind `#[cfg(test)]` in `mutation_trace/mod.rs`), so it is compiled +and run by *any* `cargo test` over the CLI crate — including the pre-existing +generic `checks.cli-tests` in `flake.nix`, not only a dedicated focused +check: + +```text +checks.cli-tests + -> full `cargo test`, including mutation_trace::mbt + -> needs the pinned Quint binary on PATH + +checks.mutation-trace-quint-connect + -> focused `cargo test ... mutation_trace::mbt` only + -> needs the pinned Quint binary on PATH +``` + +Both checks list the Nix `quint` package in `nativeCheckInputs`. Quint's +presence alone is not sufficient, though: `quint run`/`quint test` resolve +the spec by a path relative to the `cli/` crate root +(`../spec/mutation_cursor.qnt`), and `craneLib.fileset.commonCargoSources` +only covers each crate's own Cargo-referenced sources, not files outside any +crate. `workspaceSrc`'s Nix fileset therefore lists the top-level `spec/` +directory explicitly; without it, the spec never reaches either check's +sandbox and every MBT test fails with an opaque `"Quint returned non-zero +code."` (`quint-connect`'s error formatting is `Display`-only, so the +underlying Quint stderr explaining *why* — file not found — never surfaces +in the Rust test panic). + +`checks.mutation-trace-quint-connect` follows the same `craneLib.cargoTest` +pattern as `cli-tests`/`cli-clippy`/`cli-fmt`, reusing the pinned +`rustToolchain`/`cargoArtifacts`, scoped via `cargoTestExtraArgs`, printing +`rustc`/`cargo`/`quint --version` in `preCheck`. Both checks are part of +ordinary `nix flake check` (not Linux-only); `.github/workflows/quint.yml` +additionally invokes the dedicated check directly (`nix build +.#checks.x86_64-linux.mutation-trace-quint-connect`) for fast, targeted +feedback without waiting on the full Nix CI matrix — the entire invocation +comes from Nix, never a second, unpinned Rust toolchain stitched together +with the runner's own Cargo. That workflow's change detector also watches +`cli/src/services/mutation_trace/mbt/**`, `.../protocol.rs`, `.../types.rs`, +`cli/Cargo.toml`, `cli/Cargo.lock` (`flake.nix`/`flake.lock` were already +watched), so a Rust-only refinement/driver change triggers Quint CI without +touching the spec. Its "Run Quint tests" step passes `--match '^test.*'` — +omitting `--match` silently selects zero tests on this spec rather than +running the named scenarios. + +## Non-goals + +- No production DB/Git/filesystem/coordinator/hook code: `grep -RnE + "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` + returns no matches. +- No second implementation of `protocol.rs`'s logic: every `MbtAction` arm + calls exactly one `protocol::*` function (or, for `MbtMutate`, mutates only + `worktree_trees`). +- `quint-connect` never appears under `[dependencies]`. + +## Authoritative source + +`spec/mutation_cursor.qnt` (verified Quint model, including the `MbtAction` +instrumentation and its guarded-branch identity-preserving refactor) and +[mutation-trace-protocol.md](mutation-trace-protocol.md) (the pure Rust +kernel this harness verifies) remain authoritative. See +`context/plans/mutation-cursor-quint-connect.md` for build-out status. diff --git a/context/context-map.md b/context/context-map.md index ee598f9e..f3e9ea72 100644 --- a/context/context-map.md +++ b/context/context-map.md @@ -25,6 +25,7 @@ Feature/domain context: - `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/cli/mutation-trace-quint-connect.md` (`#[cfg(test)]`-only Quint Connect model-based-testing harness in `cli/src/services/mutation_trace/mbt/` continuously checking `protocol.rs` against `spec/mutation_cursor.qnt`: the verification-only `mbtAction`/`MbtAction` record-payload transport excluded from comparison, the operation-identity-vs-`MbtStutter` distinction on guarded/no-op branches with its two deterministic regressions, finite ID mapping, the AC5 comparable-state field list, `randomPrepare` staying a single `step` branch, deterministic/generated (500×30, seed-reproducible) test coverage, and the two Nix checks — generic `checks.cli-tests` and dedicated `checks.mutation-trace-quint-connect` — that both require the pinned Quint binary plus the top-level `spec/` directory in `workspaceSrc`'s Nix fileset) - `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/glossary.md b/context/glossary.md index e43633ce..1748e523 100644 --- a/context/glossary.md +++ b/context/glossary.md @@ -72,7 +72,7 @@ - `top-level help visibility metadata`: Per-command `show_in_top_level_help` metadata in `cli/src/cli_schema.rs` that controls whether a known command appears in `sce`, `sce help`, and `sce --help` without affecting direct invocation; the current hidden top-level commands are `hooks` and `policy`, while `auth` is visible, and `cli/src/command_surface.rs` renders the curated top-level help list from that shared metadata. - `command loop`: The `clap` derive-based parser + dispatcher in `cli/src/cli_schema.rs`, `cli/src/services/parse/command_runtime.rs`, and `cli/src/app.rs` that routes `help`, `config`, `setup`, `doctor`, `auth`, `hooks`, `policy`, `sync`, `version`, and `completion`, executes implemented command flows, emits command-local help payloads for supported subcommand trees, and returns deterministic actionable errors for invalid invocation. - `RuntimeCommand seam`: Internal static command-execution abstraction in `cli/src/services/command_registry.rs` where clap-parsed commands are represented as a `RuntimeCommand` enum with variants for `Help`, `HelpText`, `Version`, `Completion`, `Auth`, `Config`, `Setup`, `Doctor`, `Hooks`, `Policy`, and `Sync`. The enum owns `name()` and `execute(...)` dispatch, delegating behavior to service-owned command payload structs while avoiding boxed `dyn RuntimeCommand` handles. Parsed request construction lives in `cli/src/services/parse/command_runtime.rs` when user-provided options or subcommands are required. -- `sce dependency baseline`: Current crate dependency set declared in `cli/Cargo.toml` (`anyhow`, `chrono`, `clap`, `clap_complete`, `dirs`, `hmac`, `indicatif`, `inquire`, `jsonschema`, `keyring-core`, `murmur3`, `owo-colors`, `rand`, `reqwest`, `serde`, `serde_json`, `sha2`, `tokio`, `tracing`, `turso`, `uuid`, plus target-specific keyring backends). No CLI dev-dependencies are currently declared, and the baseline is validated through normal compile/test coverage. +- `sce dependency baseline`: Current crate dependency set declared in `cli/Cargo.toml` (`anyhow`, `chrono`, `clap`, `clap_complete`, `dirs`, `hmac`, `indicatif`, `inquire`, `jsonschema`, `keyring-core`, `murmur3`, `owo-colors`, `rand`, `reqwest`, `serde`, `serde_json`, `sha2`, `tokio`, `tracing`, `turso`, `uuid`, plus target-specific keyring backends), validated through normal compile/test coverage. `[dev-dependencies]` now carries `quint-connect` (dev/test-only, for the in-progress mutation-cursor Quint Connect model-based-testing harness; see `context/plans/mutation-cursor-quint-connect.md`). - `progress reporter contract`: Library-independent, consumer-typed sync seam in `cli/src/services/sync/progress.rs` where `ProgressReporter` carries an arbitrary consumer event type, supports explicit successful finalization and closure-based collectors, and provides `NoopProgressReporter` for callers without human progress output. The sync-owned `SyncProgressEvent` in `cli/src/services/sync/sync.rs` carries lifecycle, accepted-batch, and stream-completion payloads for the four concurrent Agent Trace streams; `services::sync::progress` also owns the fixed `indicatif` terminal adapter and focused contract tests, while `sync/command.rs` selects text versus JSON behavior. No top-level `services::progress` module exists. - `local Turso adapter`: Module in `cli/src/services/local_db/mod.rs` that defines `LocalDbSpec` and exposes `LocalDb` as a `TursoDb` alias. It resolves the canonical local DB path with `local_db_path()`, currently declares zero migrations, and inherits retry-backed `new()`, `execute()`, `query()`, and `query_map()` behavior from the shared generic adapter. - `encrypted Turso adapter`: Generic adapter seam in `cli/src/services/db/mod.rs` exposed as `EncryptedTursoDb`, structurally parallel to `TursoDb` (connection, tokio runtime bridge, spec typing). Its constructor resolves the encryption key via `encryption_key::get_or_create_encryption_key(&db_path, db_name)`, which derives a Turso-compatible 64-character hex key from non-empty `SCE_AUTH_DB_ENCRYPTION_KEY` env-secret text before falling back to OS credential-store keyring get-or-create behavior; credential-store default registration is guarded by stable `OnceLock` plus an atomic in-progress flag so errors or panics leave initialization retryable without mutex poisoning. The adapter enables Turso local encryption with strict `aegis256` cipher selection through `turso::EncryptionOpts`, wraps encrypted local open/connect in the default DB connection-open retry policy, and runs embedded migrations after retry has produced a connection; the adapter also exposes retry-backed synchronous `execute`, `query`, `query_map`, and `run_migrations` helpers with `__sce_migrations` tracking parity. diff --git a/context/overview.md b/context/overview.md index 686911f3..726fb48f 100644 --- a/context/overview.md +++ b/context/overview.md @@ -16,7 +16,7 @@ The generated `/next-task` workflow persists task-level context-synchronization - **Attribution hooks:** enabled by default, gated by staged-diff AI-overlap preflight; `SCE_ATTRIBUTION_HOOKS_DISABLED` opt-out (see `context/sce/agent-trace-commit-msg-coauthor-policy.md`). - **Install channels:** repo-flake Nix, Cargo, npm, and source-built Flatpak (`dev.crocoder.sce`); Homebrew deferred (see `context/sce/cli-first-install-channels-contract.md`). -The CLI crate currently depends on `anyhow`, `chrono`, `clap`, `clap_complete`, `dirs`, `hmac`, `indicatif`, `inquire`, `jsonschema`, `keyring-core`, `murmur3`, `owo-colors`, `rand`, `reqwest`, `serde`, `serde_json`, `sha2`, `tokio`, `tracing`, `turso`, and `uuid`, with target-specific keyring backend dependencies for Linux/FreeBSD, macOS, and Windows. No CLI dev-dependencies are currently declared. +The CLI crate currently depends on `anyhow`, `chrono`, `clap`, `clap_complete`, `dirs`, `hmac`, `indicatif`, `inquire`, `jsonschema`, `keyring-core`, `murmur3`, `owo-colors`, `rand`, `reqwest`, `serde`, `serde_json`, `sha2`, `tokio`, `tracing`, `turso`, and `uuid`, with target-specific keyring backend dependencies for Linux/FreeBSD, macOS, and Windows. `quint-connect` is the CLI's first dev-only dependency, added for the in-progress `mutation-cursor-quint-connect` model-based-testing harness. Its command loop is implemented with `clap` derive-based argument parsing and `anyhow` error handling. Top-level help displays an ASCII art "SCE" banner with a per-column right-to-left color gradient (cyan to magenta when color is enabled, plain ASCII when disabled) above a slim command list without implemented/placeholder labels; `auth` is visible while `hooks` and `policy` remain directly invocable but hidden. The real top-level command catalog/help-visibility contract is centralized in `cli/src/cli_schema.rs` and consumed by `cli/src/command_surface.rs` for custom banner/help rendering plus known-command classification. The runtime includes implemented auth flows (`auth login|logout|whoami`), with authenticated whoami reading the Control Plane `GET /me` profile and rendering flat email/name/role/permissions/organization labels, optional names and missing values handled deterministically, and exact login guidance returned when logged out, alongside config inspection/validation, setup orchestration, doctor diagnosis/repair, attribution-only hooks, shell completion, and the top-level `sync` command. Parse-time command conversion plus run-time command handling flow through the internal `RuntimeCommand` seam in `cli/src/app.rs`. The current doctor presentation contract supersedes the earlier output-shape scaffolding wording above: human text uses the compact Environment/Repository/Integrations hierarchy with healthy rows collapsed and unhealthy branches expanded, while JSON retains complete path, identity, problem, and fix-result detail. See `context/sce/doctor-human-text-contract.md`. The command loop now enforces a stable exit-code contract in `cli/src/app.rs`: `2` parse failures, `3` invocation validation failures, `4` runtime failures, and `5` dependency startup failures. diff --git a/context/plans/mutation-cursor-quint-connect.md b/context/plans/mutation-cursor-quint-connect.md new file mode 100644 index 00000000..7a4ec8ad --- /dev/null +++ b/context/plans/mutation-cursor-quint-connect.md @@ -0,0 +1,1113 @@ +# Plan: mutation-cursor-quint-connect + +## Change summary + +Connects the verified `spec/mutation_cursor.qnt` model to the pure Rust kernel at +`cli/src/services/mutation_trace/protocol.rs` using Quint Connect model-based +testing, so that `protocol.rs` becomes a continuously checked refinement of the +Quint spec instead of a one-time manual translation. This extends the completed +`mutation-cursor-protocol-kernel` work (PR #238, branch `mutation-cursor`, head +`2a097408`) with a new `#[cfg(test)]`-only `mbt/` submodule: a driver that +replays Quint-generated and Quint `run`-scenario traces through the real +`prepare`/`commit`/`taint`/`database_failure`/`abandon`/`recover` functions and +compares projected Rust state against Quint state after every step. + +This is a **third revision** of the plan (PR #239), correcting one remaining +MBT-transport issue found in review, on top of two earlier rounds of +correction: + +- **Round 1** replaced a driver design that inferred action arguments from + state with a verification-only `MbtAction` transport type, and kept + `randomPrepare` a single top-level `step` branch instead of splitting it + into four. +- **Round 2** pinned CI to a repository Nix check carrying both the Rust + toolchain and the Quint binary, rather than the GitHub runner's Cargo. +- **Round 3 (this revision)** fixes two remaining `MbtAction` design gaps: + 1. Every argument-carrying `MbtAction` variant must use a record payload + (even single-field ones), not a bare scalar, to match Quint Connect's + custom sum-type action decoder (unit variant vs. record variant). + 2. `MbtAction` must record the **invoked operation and its arguments**, + never whether that invocation changed state. `prepare`, `taint`, + `databaseFailure`, `abandon`, and `recover` (spec lines + 450/707/734/801/882) all previously fell through to the shared `stutter` + action on their guarded/no-op path; naively wiring `mbtAction' = + MbtStutter` into that shared `stutter` action would erase which + operation was actually invoked, silently stop the MBT from exercising + Rust's guard behavior on exactly the paths where refinement bugs hide, + and misuse `MbtStutter` — which must mean only "the explicit top-level + `stutter` action was selected by `step`." + +The corrected pipeline: + +```text +semantic action (mutate/prepare/commitAttempt/taint/databaseFailure/abandon/recover) + ↓ (records its own invocation and arguments, on EVERY branch — + ↓ including a branch that itself performs no state change) +verification-only MbtAction transport (mbtAction: MbtAction) + ↓ +Quint Connect custom action/nondet trace + ↓ +Rust Driver::step (dispatches on the MbtAction variant, always calling + ↓ the real protocol.rs function — never skipped because the + ↓ expected Quint state happened not to change) +real protocol.rs call + ↓ +projected Rust ModelState, compared against Quint state every step +``` + +This plan does not implement production mutation tracing: no `store.rs`, +`coordinator.rs`, `git_snapshot.rs`, database, Git, filesystem, or hook +integration is added. It is a pure verification harness layered on top of the +already-pure `protocol.rs`. + +One documentation-target note from the original plan still applies: the +request names `context/plans/mutation-cursor-quint-connect.md` as the +architecture-doc output, but that path is this plan's own file — see +**Assumptions**. + +## Acceptance criteria + +- [x] AC1: `quint-connect` is a dev/test-only dependency of the CLI crate; no + production dependency changes. + - Validate: `grep -A3 '^\[dev-dependencies\]' cli/Cargo.toml` lists + `quint-connect`; it does not also appear under `[dependencies]`; + `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` passes. +- [x] AC2: every action reachable from Quint's randomized `step` (`init`, + `randomMutate`, `randomPrepare`, `randomCommit`, `randomTaint`, + `randomRecover`, `randomDatabaseFailure`, `randomAbandon`, `stutter`) is + recorded by the verification-only `MbtAction` transport with its concrete + arguments — on every branch of that action, including branches that produce + no state change — and the Rust driver dispatches on the `MbtAction` variant + to call the real `protocol.rs` functions for every transported invocation, + never reimplementing their logic, never inferring arguments from + before/after state, and never skipping the call because the expected state + happened not to change. + - Validate: inspection of `mbt/driver.rs` — each match arm on `MbtAction` + unconditionally calls exactly one + `protocol::{prepare,commit,taint,database_failure,abandon,recover}` + function with the transported arguments, mutates only `worktree_trees`, + or is a no-op (`MbtStutter` only); no independent scope/attempt/cursor + mutation logic exists in the driver, and no conditional skips a protocol + call based on predicted state change. +- [x] AC3: both the generated `#[quint_run]` trace and the deterministic + `#[quint_test]` runs transport concrete action arguments through the same + `MbtAction` mechanism; a scenario using non-default values demonstrably + carries them through unchanged. + - Validate: the T04 smoke scenario built from `mutate(WT1, Tree3)` → + `prepare(Attempt5, Flush(WT1))` → `commitAttempt(Attempt5)` passes, and + inspection/logging of the driver's received `MbtAction` values for that + run shows `WT1`, `Tree3`, `Attempt5`, and `Flush(WT1)` reaching the actual + `protocol::prepare`/`protocol::commit` calls unchanged. +- [x] AC4: a Quint-generated random trace, replayed through the real + `protocol.rs`, matches the Quint model's semantic state after every step + across the configured sample/step budget, and a failing/generated trace is + reproducible by `QUINT_SEED`. + - Validate: `mutation_cursor_generated_traces_refine_rust_protocol` + (`#[quint_run(max_samples = 500, max_steps = 30)]`) passes under the + Nix-pinned Quint Connect check (T06); running it twice with the same + explicit `QUINT_SEED=` reproduces the same outcome. +- [x] AC5: the comparable state includes every Quint variable named in the + request (`worktrees`, `scopes`, `worktreeTrees`, `externalTaint`, + `processedEvents`, `attempts`, `mutationEvents`, each `MutationEvent`'s full + field set, each attempt's full field set) and excludes every + verification-only history, including `mbtAction` itself (transport + metadata, not semantic state). + - Validate: inspection of `mbt/model.rs` DTOs against the included/excluded + field lists above; `grep -RnE + "mbtAction|cursorHistory|protocolHistory|scopeHistory|abandonHistory|startHistory|recoveryHistory|taintHistory|evidenceAttempts|scopeStartCount|everTerminal" + cli/src/services/mutation_trace/mbt/model.rs` returns no matches outside + comments explaining the exclusion. +- [x] AC6: at least the eight named deterministic Quint `run` scenarios + (`testStartObservesBeforeActivation`, `testCloseObservesBeforeDeactivation`, + `testContendedIntervalsRemainAiContended`, + `testNoChangeHookReplayCannotStealFutureChange`, + `testConcurrentObservationsHaveOneWinner`, + `testTaintInvalidatesPreparedObservation`, `testRecoveryEstablishesBaseline`, + `testClosedScopeCannotReactivate`) replay successfully through Rust via + `#[quint_test]`, expressed as the same semantic-action call chains already + used in the spec (no duplicated scenario logic in Rust). + - Validate: the Nix-pinned Quint Connect check (T06) passes and the eight + named test functions exist and are green. +- [x] AC7: the `MbtAction` instrumentation and the `randomPrepare` + observability change leave `verifyStep`, every listed pure action + (`prepare`, `prepareAvailable`, `commitAttempt`, `taint`, `recover`, + `databaseFailure`, `abandon`), invariant definitions, and existing + deterministic runs semantically unchanged; `step`'s top-level alternatives + remain the same eight branches (`randomMutate, randomPrepare, randomCommit, + randomTaint, randomRecover, randomDatabaseFailure, randomAbandon, stutter`) + rather than being replaced by four top-level prepare branches; the pure + Quint check suite stays green. + - Validate: `nix run .#quint -- typecheck spec/mutation_cursor.qnt`; + `nix run .#quint -- test spec/mutation_cursor.qnt`; `nix run .#quint -- + run spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore + SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20`; manual + diff of `step`'s alternative list before/after this plan's changes shows + the same eight top-level branch names. +- [x] AC8: CI runs the Quint Connect suite inside a Nix check that pins both + the repository Rust toolchain and the repository Quint binary — never the + GitHub runner's preinstalled Cargo — whenever either the Quint spec or the + Rust refinement/driver/Cargo files change, without weakening the existing + pure-Quint checks. Because `mutation_trace::mbt` is registered as an + ordinary `#[cfg(test)] mod mbt;`, it is also reached by the pre-existing + generic `checks.cli-tests` (the full `cargo test` run every `nix flake + check` already performs), so the pinned Quint binary must be available to + `cli-tests` as well as to the dedicated focused check — not the dedicated + check alone. + - Validate: inspection of the new `checks.mutation-trace-quint-connect` + definition (`craneLib.cargoTest`-based, reusing the repository + `rustToolchain`/`cargoArtifacts`, scoped to `mutation_trace::mbt` via + `cargoTestExtraArgs`, with the Nix `quint` package in + `nativeCheckInputs`) and confirmation that `checks.cli-tests` also lists + the Nix `quint` package in its `nativeCheckInputs`; confirmation that + `workspaceSrc`'s Nix fileset includes the top-level `spec/` directory + (`quint run`/`quint test` resolve `../spec/*.qnt` relative to the `cli/` + crate root, and `craneLib.fileset.commonCargoSources` alone does not + cover files outside any crate) — its prior absence caused every MBT test + to fail inside the Nix sandbox regardless of Quint's availability, with + the underlying Quint stderr swallowed by `quint-connect`'s + `panic!("{}", err)` `Display`-only formatting; `nix build + .#checks.x86_64-linux.cli-tests` and `nix build + .#checks.x86_64-linux.mutation-trace-quint-connect` both pass; inspection + of `.github/workflows/quint.yml` — the change-detector regex additionally + matches `cli/src/services/mutation_trace/mbt/**`, `.../protocol.rs`, + `.../types.rs`, `cli/Cargo.toml`, `cli/Cargo.lock` (`flake.nix`/ + `flake.lock` are already watched); a dedicated job step invokes the Nix + check rather than stitching together the Nix Quint binary with the + runner's own Cargo; the existing typecheck/test/randomized-safety steps + are present, and the `test` step now passes `--match '^test.*'` since + `quint test` without `--match` silently runs zero tests on this spec. +- [x] AC9: no production DB/Git/filesystem/coordinator/hook code is + introduced; the MBT harness is test-only and `protocol.rs` stays pure. + - Validate: `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" + cli/src/services/mutation_trace` returns no matches; + `mutation_trace/mod.rs` gates `mod mbt;` behind `#[cfg(test)]`. +- [x] AC10: the existing ~75 handwritten `mutation_trace` protocol tests, + Clippy, and formatting all continue to pass unmodified. + - Validate: `./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`. +- [x] AC11: every argument-carrying `MbtAction` variant uses a record payload + compatible with Quint Connect's current custom sum-type action decoder; + there are no bare-scalar-payload variants used for driver dispatch. + - Validate: inspection of `MbtAction`'s definition in + `spec/mutation_cursor.qnt` — every variant with arguments is a record + (`{ field: Type, ... }`, even single-field), and only truly + argument-free variants (`MbtInit`, `MbtStutter`) are bare. +- [x] AC12: `MbtAction` identifies the invoked semantic operation and its + arguments, never whether that invocation changed state — a guarded/no-op + `prepare` is still recorded as `MbtPrepare{...}`, a guarded/no-op + `taint`/`databaseFailure`/`abandon`/`recover`/`commitAttempt` is still + recorded as its own operation-specific variant, and `MbtStutter` is + produced only when `step` selects the explicit top-level `stutter` action + (never as a byproduct of another operation's internal guard branch). + - Validate: manual trace inspection of at least the two guarded-no-op + regressions added in T05 (see AC13) confirms the operation-specific + variant, not `MbtStutter`, appears at the guarded step. +- [x] AC13: at least two deterministic MBT regressions prove that a guarded + semantic no-op still invokes the corresponding Rust kernel operation rather + than being skipped: one `prepare` case (re-preparing an attempt that is no + longer `Available`) and one other guarded action (`recover` when recovery + is not needed, or `abandon` on a non-live scope). + - Validate: the two regression scenarios in T05 pass, each proving the + Rust driver called `protocol::prepare`/`protocol::recover` (or the + chosen alternative) on the guarded step and independently produced the + same no-op state Quint did. +- [x] AC14: the `stutter` action itself, and every guarded action that used + to fall through to it (`prepare`, `taint`, `databaseFailure`, `abandon`, + `recover`, and any analogous guarded path in `commitAttempt`), no longer + share a single "call `stutter`, which sets `mbtAction' = MbtStutter`" + implementation — each guarded branch sets its own operation-specific + `mbtAction` while still leaving all other semantic state unchanged exactly + as the pre-existing `stutter` action did. + - Validate: manual review of `spec/mutation_cursor.qnt`'s `prepare`, + `taint`, `databaseFailure`, `abandon`, `recover`, and `commitAttempt` + guarded branches (lines given in the Change summary are the pre-revision + locations; re-check at implementation time) confirms none of them + invokes the shared top-level `stutter` action directly; AC7's existing + Quint checks confirm this refactor changed no semantic state assignment. + +### Full validation + +- `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` +- `./scripts/run-cli-cargo.sh build --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 --match '^test.*'` (bare + `quint test` without `--match` silently selects zero tests on this spec) +- `nix run .#quint -- run spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20` +- `nix build .#checks..cli-tests` — the generic full-suite check, + which also reaches `mutation_trace::mbt` and therefore needs Quint pinned +- `nix build .#checks..mutation-trace-quint-connect` — the dedicated, + focused Nix-pinned Rust+Quint Quint Connect suite +- `nix flake check` where practical, since both checks above are wired into it +- `nix run .#regenerate-cargo-sources` followed by `git diff --stat packaging/flatpak/cargo-sources.json` (expect no further diff after T01 regenerates it) + +### Context sync + +- `context/cli/mutation-trace-quint-connect.md` (new — see Assumptions for why + this replaces the request's literal `context/plans/...` target) +- `context/cli/mutation-trace-protocol.md` (cross-link to the new doc if the + existing "Target end-state architecture" section should point at it) +- `context/context-map.md` (new domain-file entry) + +## 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:** `spec/mutation_cursor.qnt` (adding `MbtAction`/`mbtAction` + instrumentation with record payloads and operation-identity-preserving + guarded branches, and making `randomPrepare` observable, without changing + `step`'s top-level branch count); + `cli/src/services/mutation_trace/mbt/{mod.rs,model.rs,driver.rs,tests.rs}`; + the `#[cfg(test)] mod mbt;` registration in `mutation_trace/mod.rs`; + `cli/Cargo.toml` / `cli/Cargo.lock`; `packaging/flatpak/cargo-sources.json` + regeneration; a new Nix check pinning Rust+Quint for the MBT suite; + `.github/workflows/quint.yml`; + `context/cli/mutation-trace-quint-connect.md`; `context/context-map.md`. +- **Out of scope:** `store.rs`, `coordinator.rs`, `git_snapshot.rs`, + `worktree_guard.rs`, database migrations, CAS persistence, Git object + storage, hook wiring, Agent Trace evidence generation, runtime checkout + materialization, filesystem locking, external-taint marker persistence; + refactoring the CLI into a library crate; moving the existing ~75 handwritten + protocol tests; a second, duplicated set of MBT-only scenario definitions + when the existing deterministic `run` expressions can be reused directly. +- **Constraints:** Quint Connect is a dev-dependency only, never a production + one; CI must use the repository's pinned Nix `quint` binary and the + repository's pinned Nix Rust toolchain, never a globally-installed npm + Quint or the GitHub runner's default Cargo; `prepare`, `prepareAvailable`, + `commitAttempt`, `taint`, `recover`, `databaseFailure`, `abandon`, + invariant definitions, verification histories, and `verifyStep` must not + change semantics; existing Quint invariants/tests must not weaken; + `mbtAction` must never participate in freshness, lifecycle, attribution, + revisions, cursor movement, taint, recovery, mutation evidence, or + invariant truth; `randomPrepare` must remain a single top-level `step` + alternative; every argument-carrying `MbtAction` variant must be a record, + never a bare scalar; `mbtAction` must record the invoked operation and its + arguments on every branch of that operation, including guarded/no-op + branches — `MbtStutter` is reserved exclusively for the explicit top-level + `stutter` action selected by `step`, never for another operation's internal + no-op path. +- **Non-goal:** changing protocol semantics to make Quint Connect easier to + wire up; growing the MBT harness into a second implementation of + `protocol.rs`'s logic; changing the randomized simulation's top-level + action-selection distribution; collapsing a guarded operation's identity + into `MbtStutter` for convenience. + +## Assumptions + +- The request's target path for the architecture write-up, + `context/plans/mutation-cursor-quint-connect.md`, is this SCE plan's own + file (`context/plans/{plan_name}.md`; `context/context-map.md` records + `context/plans/` as "active plan execution artifacts, not durable history"). + Writing the architecture doc there would overwrite this plan's task-tracking + file mid-stack. T06 instead writes it to + `context/cli/mutation-trace-quint-connect.md`, mirroring the two existing + sibling docs for this exact module + (`context/cli/mutation-trace-protocol.md`, + `context/cli/mutation-trace-revision-refinement.md`) and linking it from + `context/context-map.md`. +- Adding `quint-connect` as a dev-dependency changes `cli/Cargo.lock`, which + the source-built Flatpak package vendors via a checked-in, CI-guarded + (`cargo-sources-parity`) mirror at `packaging/flatpak/cargo-sources.json` + (per `context/sce/flatpak-distribution-patterns.md` and `flake.nix`). T01 + regenerates that file via `nix run .#regenerate-cargo-sources` even though + the change request's own check list does not name it, because it is + required for "existing checks... continue passing" to actually hold in CI. +- `flake.nix` already defines a pinned `rustToolchain`/`craneLib` used by the + existing `cli-tests`/`cli-clippy`/`cli-fmt` checks (each a thin + `craneLib.cargoTest`/`cargoClippy`/`cargoFmt` wrapper reusing shared + `cargoArtifacts`). T06's new Quint Connect check follows this exact + established pattern — a `craneLib.cargoTest`-style derivation scoped to + `mutation_trace::mbt` with the Nix `quint` package added to its check + inputs — rather than assembling a bespoke Rust+Quint environment from + scratch. +- T01 confirmed `quint-connect` 0.1.2 (`github.com/informalsystems/quint-connect`, + Apache-2.0) and its `Driver`/`State` traits, `Config { state, nondet }` + transport configuration, and `#[quint_test]`/`#[quint_run]` + `switch!` + dispatch mechanism, against the upstream README and vendored crate source. + T04 subsequently confirmed the custom sum-type decoder accepts a + `Value::Record` directly for both the top-level nondet-picked `MbtAction` + and nested record fields, and proved record-payload action transport end to + end with the non-default `WT1` / `Tree3` / `Attempt5` / `Flush(WT1)` replay + — resolving AC11's record-payload rule with no fallback needed. +- T02 completed the guarded-operation audit across all six candidate actions + (not just the five that previously called the shared top-level `stutter`). + `prepare`, `taint`, `databaseFailure`, `abandon`, `recover`, and + `commitAttempt` each now set their own operation-specific `MbtAction` on + every guarded/no-op branch — via the shared `mbtStutterAs(taken: MbtAction)` + helper that replaced `stutter`'s inline field list — rather than falling + through to the shared top-level `stutter` action. `MbtStutter` is reachable + only from the explicit top-level `stutter` action, never from another + operation's guarded path. +- T03 confirmed no additional `PrepareKind`-style instrumentation is + required: `prepare` (T02) unconditionally sets `mbtAction' = + MbtPrepare({attempt, boundary})` on both its `prepareAvailable` and guarded + paths, and `boundary` there is always the exact concrete `Boundary` value + `randomPrepare`'s five inner `any` alternatives selected — already fully + observable to the driver. `randomPrepare` remains a single top-level `step` + alternative; `step`'s eight top-level branches are unchanged. +- PR #238 (`mutation-cursor`) remains the semantic base for this stacked PR. + +- PR #239 (`quint-connect`) has completed implementation. The durable task + state in this plan is the source of truth for implementation progress: + + - T01 complete: `quint-connect` dependency and packaging synchronization. + - T02 complete: operation-preserving `MbtAction` instrumentation. + - T03 complete: `randomPrepare` observability without structural change. + - T04 complete: Rust Quint Connect driver, model projection, ID mapping, + and non-default transport smoke replay. + - T05 complete: deterministic scenario replays, guarded-no-op regressions, + and generated 500×30 refinement testing with seed reproduction. + - T06 complete: generic `checks.cli-tests` and dedicated + `checks.mutation-trace-quint-connect` Nix checks, `.github/workflows/quint.yml` + wiring, and the `context/cli/mutation-trace-quint-connect.md` architecture + doc. + + T01-T06 are complete. Implementation and local validation are complete. + PR #239 is in final CI/review state. + + Do not encode PR #239's current head SHA or statements such as + "implementation has not started" as durable assumptions here. The branch head + is mutable and must be fetched from GitHub when executing or reviewing a task. + + PR #239 continues to target PR #238's `mutation-cursor` branch; verify the + current base/head relationship from GitHub whenever stack state matters. + +## Task stack + +- [x] T01: `Pin quint-connect as a CLI dev-dependency` (status:done) + - Task ID: T01 + - Scope: In — confirm the current `quint-connect` crate name/version and API + shape against the upstream README and + `connect/examples/two_phase_commit/mbt.rs`, including its custom + action/nondet `Config` mechanism for driver dispatch and exactly how its + decoder distinguishes unit vs. record action variants (needed by T02 and + T04); add it under `cli/Cargo.toml`'s `[dev-dependencies]`; update + `cli/Cargo.lock`; regenerate `packaging/flatpak/cargo-sources.json` via + `nix run .#regenerate-cargo-sources`. Out — any driver/model/test code; + Quint spec changes. + - Dependencies: none + - Done when: `quint-connect` appears only under `[dev-dependencies]`; + `cli/Cargo.lock` and `packaging/flatpak/cargo-sources.json` reflect the + new dependency with no further diff after regeneration; the CLI still + builds. + - Verify: `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml`; + `nix run .#regenerate-cargo-sources` then `git diff --stat + packaging/flatpak/cargo-sources.json` shows no residual diff. + - Completed: 2026-08-27 + - Files changed: `cli/Cargo.toml`, `cli/Cargo.lock`, + `nix/flatpak/cargo-sources.nix`, `packaging/flatpak/cargo-sources.json` + - Result: Added `quint-connect = "0.1.2"` (confirmed current via crates.io + API; matches the plan's placeholder guess) under a new + `[dev-dependencies]` section in `cli/Cargo.toml` — no change under + `[dependencies]`. `cargo build` regenerated `cli/Cargo.lock` with + `quint-connect`, `quint-connect-macros`, and transitive deps (`itf`, + `colored`, `similar`, `jiff`, `rand 0.9`, etc. — coexists fine with the + crate's own `rand 0.8`). Discovered that `nix run .#regenerate-cargo-sources` + is a no-op against a stale `Cargo.lock` unless the fixed-output + derivation's pinned `outputHash` in `nix/flatpak/cargo-sources.nix` is + bumped first (Nix reuses the existing store path for that hash and never + re-invokes the generator) — confirmed this is the established convention + via `git log`/`git show eb5e6154` (the prior Turso 0.7.0 bump did the same + hash-then-regenerate two-step). Set a dummy `outputHash`, captured the + real hash from the resulting Nix hash-mismatch error + (`sha256-p8fzi7KWNltCEopHvXFmswASt9ov7UWxh/XU8mGLgH0=`), wrote that in, + then regenerated `packaging/flatpak/cargo-sources.json` (351 added + lines, 6 `quint-connect`/`quint-connect-macros` entries); a second + regeneration run produced an identical file (idempotent). + API-shape research for T02/T04 (recorded for handoff, not itself + verified by T01's done-when): `quint-connect` 0.1.2 + (`github.com/informalsystems/quint-connect`, Apache-2.0) exposes + `Driver`/`State` traits, a `Config { state, nondet }` struct for + locating comparable state and nondet-action paths in nested Quint state, + and `#[quint_test(spec, test)]`/`#[quint_run(spec, max_samples, ...)]` + + `switch!(step { Variant(args) => ... })` for dispatch. Its generic sum-type + deserialization (`#[serde(tag = "tag", content = "value")]`) supports + unit, newtype/tuple, and record/struct variants, so `MbtAction`'s planned + all-record-payload design (AC11) is plausible — but neither shipped + example (`two_phase_commit`, `tictactoe`) actually uses a record/struct + action variant; both only exercise unit and bare-scalar tuple variants + (e.g. `SpontaneouslyPrepares(node)`, `MoveO(coordinate)`) via `switch!`. + Separately, the crate's `nondet`-path extraction (`extract_nondet_from_sum_type` + in `connect/src/trace/mod.rs`) specifically requires the picked value to + deserialize as a `Record` (or an empty tuple) — flag this for T02/T03 to + verify directly against a record-payload `MbtAction` before relying on it, + since it wasn't directly evidenced upstream. + - Verify outcomes: `./scripts/run-cli-cargo.sh build --manifest-path + cli/Cargo.toml` — passed (`Finished dev profile`); `nix run + .#regenerate-cargo-sources` then `git diff --stat + packaging/flatpak/cargo-sources.json` — passed, shows the new-dependency + diff with no further change on a second run; `nix build + .#checks.x86_64-linux.cargo-sources-parity` — passed (no diff reported). + - Context impact: Root context synchronized. + + Adding `quint-connect` introduced the CLI's first dev-only dependency, so + the dependency baseline references in: + + - `context/overview.md` + - `context/architecture.md` + - `context/glossary.md` + + were updated to distinguish production dependencies from the new + dev/test-only `quint-connect` dependency. + + Additionally, `context/sce/flatpak-distribution-patterns.md` was updated + with the fixed-output-hash regeneration procedure discovered while + refreshing `packaging/flatpak/cargo-sources.json`. + + These are documentation/context synchronization changes only; they + introduce no new runtime architecture or production interface. + - Context synchronization: synced + +- [x] T02: `Add operation-preserving MBT action-transport instrumentation to the spec` (status:done) + - Task ID: T02 + - Scope: In — `spec/mutation_cursor.qnt`: define a verification-only + `MbtAction` sum type where every argument-carrying variant is a record + payload, even single-field ones (`MbtInit`, `MbtMutate({worktree, + tree})`, `MbtPrepare({attempt, boundary})`, `MbtCommit({attempt})`, + `MbtTaint({worktree})`, `MbtDatabaseFailure({worktree})`, + `MbtAbandon({scope})`, `MbtRecover({worktree})`, and unit `MbtStutter`), + matching the exact unit-vs-record shape Quint Connect's current custom + action decoder expects (confirmed in T01); a verification-only + `mbtAction: MbtAction` state variable, never read by or participating in + any other rule. For `prepare`, `taint`, `databaseFailure`, `abandon`, + and `recover` — every one of which currently falls through to the shared + top-level `stutter` action on its guarded path — and for `commitAttempt` + if it has an analogous no-op path: refactor so the guarded/no-op branch + still sets `mbtAction'` to that operation's own variant with its real + arguments (e.g. `MbtPrepare({attempt, boundary})`) while leaving every + other semantic state assignment exactly as `stutter` already produces it + — do not let the guarded branch call the shared top-level `stutter` + action directly, since that would overwrite `mbtAction'` with + `MbtStutter` and erase which operation was invoked. Only the explicit + top-level `stutter` action (the one `step` itself can select) sets + `mbtAction' = MbtStutter`. Out — driver/Rust code; `randomPrepare`/`step` + structure (T03); the actual transition logic of `prepare`, + `prepareAvailable`, `commitAttempt`, `taint`, `recover`, + `databaseFailure`, `abandon`, invariant definitions, verification + histories, `verifyStep`. + - Dependencies: T01 + - Done when: `mbtAction` exists purely as instrumentation with the + record-payload shape above; every guarded/no-op invocation of `prepare`, + `taint`, `databaseFailure`, `abandon`, `recover` (and `commitAttempt` if + applicable) records its own operation-specific `MbtAction` rather than + `MbtStutter`; `MbtStutter` is reachable only from the explicit top-level + `stutter` action; none of this affects invariant truth, lifecycle, + attribution, revisions, cursor movement, taint, recovery, or mutation + evidence; typecheck, the Quint test suite, and the randomized + `verifyStep` safety run all stay green with unchanged invariant outcomes. + - Verify: `nix run .#quint -- typecheck spec/mutation_cursor.qnt`; + `nix run .#quint -- test spec/mutation_cursor.qnt`; `nix run .#quint -- + run spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore + SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20`; manual + diff of a known deterministic run's non-`mbtAction` semantic-variable + trace before/after this task, confirming no divergence; manual trace + inspection of one guarded `prepare` call and one guarded `recover` (or + `abandon`) call, confirming their operation-specific `MbtAction` — not + `MbtStutter` — is recorded. + - Completed: 2026-08-27 + - Files changed: `spec/mutation_cursor.qnt` + - Result: Added a verification-only `MbtAction` sum type (all argument- + carrying variants are records, even single-field ones — `MbtInit`, + `MbtMutate({worktree,tree})`, `MbtPrepare({attempt,boundary})`, + `MbtCommit({attempt})`, `MbtTaint({worktree})`, + `MbtDatabaseFailure({worktree})`, `MbtAbandon({scope})`, + `MbtRecover({worktree})`, unit `MbtStutter`) and a new `mbtAction: + MbtAction` state variable, assigned in every action, read by nothing else. + Replaced `stutter`'s inline field list with a new shared + `mbtStutterAs(taken: MbtAction): bool` action — identical to the old + `stutter` body except it takes the `MbtAction` to record as a parameter; + `stutter` itself is now `mbtStutterAs(MbtStutter)`. Audited all six + candidate actions per the plan's Assumptions: `prepare`, `taint`, + `databaseFailure`, `abandon`, and `recover` each had a guarded/no-op + branch that called the shared top-level `stutter` directly — each now + calls `mbtStutterAs((...))` instead, so the guarded + branch never overwrites `mbtAction'` with `MbtStutter`. `commitAttempt` + does have an analogous no-op path (the existing `not(accepted)` branch, + which never called `stutter` — it already inlined its own field list) — + both its not-accepted and accepted branches now additionally set + `mbtAction' = MbtCommit({attempt: attempt})`. No other field assignment + in any action changed (confirmed by `git diff`: every non-`mbtAction'` + line is unchanged context). `MbtStutter` is now reachable only from the + explicit top-level `stutter` action. `step`, `randomPrepare`, and every + other `random*` action were not touched (out of scope, deferred to T03). + A parameter named `action` in the new shared helper collided with the + `action` keyword and had to be renamed to `taken` — not itself a design + decision, just a naming fix required to typecheck. + - Verify outcomes: `nix run .#quint -- typecheck spec/mutation_cursor.qnt` + — passed, no errors. `nix run .#quint -- test spec/mutation_cursor.qnt` + — passed (exit 0, all existing `run` scenarios including the 8 named + deterministic ones still pass). `nix run .#quint -- run + spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore + SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20` — + "[ok] No violation found" (5000 traces, up to 21 steps). Manual diff of + the non-`mbtAction` semantic-variable assignments before/after this task + — `git diff spec/mutation_cursor.qnt` shows only added `mbtAction'` + lines and `stutter` → `mbtStutterAs(...)` call-site substitutions; no + other variable's assignment expression changed anywhere in the file, so + there is no divergence to check trace-by-trace. Manual trace inspection + of a guarded `prepare` (re-preparing `Attempt0` after it was already + committed), a guarded `recover` (on `WT0` with no taint/rebaseline + need), and a guarded `abandon` (on `Scope0` while still `NeverSeen`) — + added as temporary `run` scenarios appended to the spec, run with `quint + test --match 'tempTest.*'`, all 4 passed (including a control case + confirming the explicit top-level `stutter` action still records + `MbtStutter`), then removed before this commit; the working tree carries + only the permanent instrumentation, not the temporary scenarios. + - Context impact: none. Only `spec/mutation_cursor.qnt` changed, and the + change is purely additive/internal to the spec (a verification-only type, + state variable, and guarded-branch instrumentation never read by any + other action, invariant, or Rust code — no driver exists yet). It does + not alter the pure Rust refinement `context/cli/mutation-trace-protocol.md` + describes (that doc covers `prepare`/`commit`/etc. semantics, which this + task explicitly left unchanged and verified unchanged), and does not touch + the production-vs-dev dependency baseline `context/overview.md`, + `context/architecture.md`, and `context/glossary.md` already record for + the in-progress `mutation-cursor-quint-connect` harness (from T01). The + corrected-pipeline architecture write-up is explicitly deferred to T06 by + this plan's own scope, not skipped here. + - Context synchronization: synced + +- [x] T03: `Keep randomPrepare a single step alternative while making it Connect-observable` (status:done) + - Task ID: T03 + - Scope: In — `spec/mutation_cursor.qnt`'s `randomPrepare`/`step` only: + keep `randomPrepare` as one `step` branch (no four-way top-level split); + using T02's `mbtAction` output, determine whether the concrete selected + boundary is already fully visible to Quint Connect via the recorded + `MbtPrepare{attempt,boundary}` value, and add the smallest additional + instrumentation (e.g. a `PrepareKind`-style nondet choice, recorded + alongside `mbtAction` for observability only) only if that alone proves + insufficient. Out — the `MbtAction` type definition and guarded-branch + fix (T02, already done); driver code; any change to + `prepare`/`prepareAvailable`/`commitAttempt`/invariants/`verifyStep`. + - Dependencies: T02 + - Done when: `step`'s top-level alternatives are structurally the same + eight branches as the pre-existing baseline (`randomMutate, randomPrepare, + randomCommit, randomTaint, randomRecover, randomDatabaseFailure, + randomAbandon, stutter`); all four prepare boundary kinds remain reachable + from `randomPrepare`; the concrete boundary Quint selected for any given + `randomPrepare` firing is recoverable by the driver. + - Verify: `nix run .#quint -- typecheck spec/mutation_cursor.qnt`; + `nix run .#quint -- test spec/mutation_cursor.qnt`; `nix run .#quint -- + run spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore + SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20`; a + manual diff confirming `step`'s alternative list is unchanged from the + pre-refactor baseline (same eight names, no new top-level branches). + - Completed: 2026-08-27 + - Files changed: `spec/mutation_cursor.qnt` + - Result: Confirmed the smallest option (no structural change) is already + sufficient — no code change to `randomPrepare` or `step`. `prepare` + (T02) unconditionally sets `mbtAction' = MbtPrepare({attempt, boundary})` + on both its `prepareAvailable` path and its guarded `mbtStutterAs(...)` + path, and `boundary` there is always the exact concrete `Boundary` value + passed to whichever of `randomPrepare`'s five inner `any` alternatives + fired (`Start`/`Advance`/`Close` with concrete `scope`/`event`, or + `Flush` with a concrete `WorktreeId`). This means the driver, dispatching + on the `MbtAction::MbtPrepare` variant, already receives which boundary + kind was selected and its full concrete arguments — no dedicated + `PrepareKind`-style nondet choice is needed. T01's flagged open question + about Quint Connect's `extract_nondet_from_sum_type` requiring a + `Record`-shaped value applies to the top-level nondet-picked action type + (`MbtAction`, already all-record per AC11/T02), not to `Boundary` as a + nested field inside `MbtPrepare`'s record — decoding a nested field with + mixed record/bare-scalar variants (`Flush(WorktreeId)`) is an ordinary + serde adjacently-tagged-enum concern for T04's DTOs, unrelated to + Connect's nondet-extraction mechanism. Added a five-line comment above + `randomPrepare` documenting this conclusion (why it stays a single + branch with no extra instrumentation) so a future change doesn't + reintroduce a four-way split or redundant `PrepareKind` field. `step`'s + eight top-level alternatives and `randomPrepare`'s inner `any` block are + otherwise byte-for-byte unchanged (confirmed by `git diff`). + - Verify outcomes: `nix run .#quint -- typecheck spec/mutation_cursor.qnt` + — passed (exit 0, no errors). `nix run .#quint -- test + spec/mutation_cursor.qnt` — passed (exit 0). `nix run .#quint -- run + spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore + SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20` — + "[ok] No violation found" (5000 traces, up to 21 steps). Manual diff + (`git diff spec/mutation_cursor.qnt`) confirms the only change is the + added comment; `step`'s alternative list and `randomPrepare`'s body are + unchanged from the pre-task baseline. + - Context impact: none. Only `spec/mutation_cursor.qnt` changed, and the + change is a documentation-only comment above `randomPrepare` recording a + design conclusion — no state variable, action, invariant, or semantic + behavior was added or altered. `step`'s structure, `mbtAction`'s shape, + and every action's transition logic are exactly as T02 left them. No + driver or Rust code exists yet (T04), so there is nothing downstream to + resynchronize. + - Context synchronization: synced + +- [x] T04: `Build the MBT driver, ID mapping, and comparable model state` (status:done) + - Task ID: T04 + - Scope: In — + `cli/src/services/mutation_trace/mbt/{mod.rs,model.rs,driver.rs}`; + `#[cfg(test)] mod mbt;` registration in `mutation_trace/mod.rs`; + `MutationCursorDriver` (`protocol: ProtocolState` + + `worktree_trees: BTreeMap`); Quint Connect's custom + action/nondet configuration wired so the driver dispatches on `MbtAction` + variants (never on before/after state diffing); exact-Quint-`init` state + construction (both worktrees, all four scopes, all six attempts, matching + the request's literal initial values); the finite + WT/Scope/Tree/Event/Attempt ID mapping; the full `MbtAction` → + `protocol::*` call mapping (`MbtInit`, `MbtMutate` touching only + `worktree_trees`, `MbtPrepare`, `MbtCommit`, `MbtTaint`, + `MbtDatabaseFailure`, `MbtAbandon`, `MbtRecover`, `MbtStutter` as a + no-op) — every arm unconditionally calling its `protocol::*` function + with the transported arguments, including when the Quint side is + expected to stutter, since replaying the guarded call and comparing the + resulting no-op state against Quint is the point of the regressions in + T05; `ModelState`/`MutationEvent`/`Attempt` comparable DTOs + (`BTreeMap`/`BTreeSet`) covering worktrees/scopes/worktreeTrees/ + externalTaint/processedEvents/attempts/mutationEvents and excluding + `mbtAction` plus every other verification-only history; + `impl State for ModelState`; one deterministic + `#[quint_test]` smoke replay in `mbt/tests.rs` built from non-default + values (`mutate(WT1, Tree3)` → `prepare(Attempt5, Flush(WT1))` → + `commitAttempt(Attempt5)`) that demonstrably transports `WT1`, `Tree3`, + `Attempt5`, and `Flush(WT1)` from the Quint trace into the real + `protocol::prepare`/`protocol::commit` calls, proving the driver never + guesses arguments from defaults. Out — the remaining deterministic + scenario replays, the two guarded-no-op regressions, and the generated + simulation (T05). + - Dependencies: T01, T02, T03 + - Done when: the driver never reimplements protocol semantics, never + infers action arguments from state, and never skips a `protocol::*` call + because the expected Quint state is unchanged; the comparable state + matches AC5; the WT1/Tree3/Attempt5 smoke scenario passes and is + inspectable as proof of real argument transport. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml + mutation_trace::mbt` with the Nix `quint` binary on `PATH` (interim, ahead + of T06's dedicated check); `./scripts/run-cli-cargo.sh clippy + --manifest-path cli/Cargo.toml --all-targets -- -D warnings`; `cargo fmt + --manifest-path cli/Cargo.toml -- --check`. + - Completed: 2026-08-27 + - Files changed: `spec/mutation_cursor.qnt`, + `cli/src/services/mutation_trace/mod.rs`, + `cli/src/services/mutation_trace/mbt/mod.rs` (new), + `cli/src/services/mutation_trace/mbt/model.rs` (new), + `cli/src/services/mutation_trace/mbt/driver.rs` (new), + `cli/src/services/mutation_trace/mbt/tests.rs` (new) + - Result: Added `#[cfg(test)] mod mbt;` to `mutation_trace/mod.rs`. Built + the `mbt` submodule: `model.rs` defines ITF-wire mirror types (`Wire*`) + for every Quint identity/enum/record type reachable from the comparable + state — confirmed against the vendored `quint-connect` 0.1.2 and `itf` + 0.4.0 crate sources (available locally via the Nix store, since both are + dev-dependencies) that sum types deserialize as `{tag, value}` via + `#[serde(tag = "tag", content = "value")]` (README "Enums" section), + that unit-only sum types need no `content` attribute, and that + `quint-connect`'s nondet-pick extraction (`extract_nondet_from_sum_type`) + accepts a `Value::Record` directly — resolving T01's flagged uncertainty + about record-payload `MbtAction` variants: they work exactly as AC11 + designed, no fallback needed. Each `Wire*` type converts via `From` into + this crate's existing domain types (`types.rs`, untouched). `ModelState` + is `#[serde(from = "WireModelState")]`-deserializable and holds exactly + AC5's field list (`worktrees`, `scopes`, `worktree_trees`, + `external_taint`, `processed_events`, `attempts`, `mutation_events`); + `mbtAction` has no field anywhere in the wire types, so it is silently + dropped by serde's default unknown-field handling when the full + top-level state record deserializes — the mechanism that keeps it out of + the compared state. `driver.rs` defines `MutationCursorDriver { protocol: + ProtocolState, worktree_trees: BTreeMap }`, an + `init()` matching Quint's `init` exactly (both worktrees Tree0/rev0/ + healthy, all four scopes `NeverSeen` via `scopeActor`'s fixed partition, + all six attempts `Available`/`Flush(WT0)`/rev0/Tree0/Tree0), and + `Driver::step` dispatching via `switch!` on every `MbtAction` variant + (`Config { nondet: &["mbtAction"], state: &[] }`, confirmed correct + against `quint-connect`'s `extract_from_sum_type` path since `mbtAction` + is a plain top-level var, not Quint's builtin `mbt::actionTaken`). Every + arm unconditionally calls its `protocol::*` function with the + transported, converted arguments (`MbtMutate` touches only + `worktree_trees`; `MbtStutter` calls a dedicated no-op `mbt_stutter` + method rather than being inlined, so it isn't a bare `()` statement); + `boundary_worktree` (already `pub` in `types.rs`) resolves a + `prepare`/`recover` boundary's worktree from the driver's own `scopes` + map, which always agrees with Quint's static `scopeWorktree` partition + since both are seeded identically at `init` and a scope's `worktree_id` + never changes afterward. Added the one non-default-values smoke scenario + the task specifies as a new named `run` in `spec/mutation_cursor.qnt` + (`testMbtDriverTransportsNonDefaultArguments`, appended after the last + existing `run`) — required because `#[quint_test]` replays a + spec-defined `run` by name, and no existing named scenario used this + exact `mutate(WT1, Tree3)` → `prepare(Attempt5, Flush(WT1))` → + `commitAttempt(Attempt5)` chain; this one small, task-specified addition + was necessary to satisfy AC3/the task's own Done-when text, not a scope + expansion. `mbt/tests.rs` wires it via `#[quint_test(spec = + "../spec/mutation_cursor.qnt", test = + "testMbtDriverTransportsNonDefaultArguments")]` (relative to `cli/`, + `cargo test`'s working directory). Deviations from the gate's Approach: + none material — `mbt_commit`/`mbt_taint`/`mbt_database_failure`/ + `mbt_abandon`/`mbt_recover` take `&AttemptId`/`&WorktreeId`/`&ScopeId` + references rather than owned values (clippy `needless_pass_by_value`, + since they only borrow); `BTreeSet::new()` used in place of + `Default::default()` (clippy `default_trait_access`); both are + ordinary, reversible local implementation choices. + - Verify outcomes: `./scripts/run-cli-cargo.sh test --manifest-path + cli/Cargo.toml mutation_trace::mbt` (Nix `quint` 0.32.0 on `PATH`) — + passed: `mutation_cursor_transports_non_default_arguments` generated and + replayed 100 traces of the named scenario, `[OK]`, `1 passed; 0 failed`; + running the full `mutation_trace` suite together + (`./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml + mutation_trace`) shows `76 passed; 0 failed` — the pre-existing ~75 + handwritten tests plus this one new MBT test, confirming no regression. + `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml + --all-targets -- -D warnings` — passed after fixing doc-markdown, + default-trait-access, needless-pass-by-value, unused-self, and a + macro-generated `no_effect` lint (the original bare `MbtStutter => ()` + case expanded to a `();` statement inside `switch!`; replaced with an + explicit `mbt_stutter` method call). `cargo fmt --manifest-path + cli/Cargo.toml -- --check` — passed (ran `cargo fmt` once to fix import + ordering/line-wrap, then the check was clean). Additionally (not in this + task's own Verify list, but touched `spec/mutation_cursor.qnt`): `nix + run .#quint -- typecheck spec/mutation_cursor.qnt` passed; `nix run + .#quint -- test spec/mutation_cursor.qnt --match + '^testMbtDriverTransportsNonDefaultArguments$'` passed (`1 passing`); + `nix run .#quint -- test spec/mutation_cursor.qnt` (full suite, no + `--match`) exited 0 with no failure output. `grep -RnE + "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` + — no matches (AC9); `mod mbt;` confirmed behind `#[cfg(test)]` in + `mutation_trace/mod.rs`. + - Context impact: none. Only test-only files changed + (`cli/src/services/mutation_trace/mbt/*`, gated behind `#[cfg(test)]`) + plus one new named `run` scenario in `spec/mutation_cursor.qnt` (no + state/action/invariant change). No production dependency, public + interface, CLI surface, or architecture changed; `protocol.rs`/ + `types.rs` are unmodified and untouched by this task, so + `context/cli/mutation-trace-protocol.md` still accurately describes + them. The corrected-pipeline architecture write-up + (`context/cli/mutation-trace-quint-connect.md`) remains explicitly + deferred to T06 by this plan's own scope, as T02/T03 already noted. + - Context synchronization: synced + +- [x] T05: `Wire deterministic scenario replays, guarded-no-op regressions, and the generated Quint Connect simulation` (status:done) + - Task ID: T05 + - Scope: In — `mbt/tests.rs`: `#[quint_test]` functions for the remaining + named scenarios (`testCloseObservesBeforeDeactivation`, + `testContendedIntervalsRemainAiContended`, + `testNoChangeHookReplayCannotStealFutureChange`, + `testConcurrentObservationsHaveOneWinner`, + `testTaintInvalidatesPreparedObservation`, + `testRecoveryEstablishesBaseline`, `testClosedScopeCannotReactivate`), and + any other existing `run test...` declaration Quint Connect can wire + without duplicating scenario logic in Rust; two new deterministic + guarded-no-op regressions proving `MbtAction` transport survives a + guarded operation: (1) `init.then(prepare(Attempt0, + Start(...))).then(prepare(Attempt0, Advance(...)))`, where the second + `prepare` call guards because `Attempt0` is no longer `Available`, + asserting the driver still calls `protocol::prepare` a second time and + independently reaches the same no-op outcome; (2) one non-`prepare` + guarded case — `recover` on a worktree that does not need recovery — + asserting the driver still calls `protocol::recover` and independently + reaches the same no-op outcome; `mutation_cursor_generated_traces_refine_rust_protocol` + (`#[quint_run(max_samples = 500, max_steps = 30)]`) comparing `ModelState` + after every generated step, using the same `MbtAction` transport as the + deterministic runs; `QUINT_SEED` reproduction confirmed. Out — + driver/model changes (T04, already done); CI wiring and documentation + (T06). + - Dependencies: T04 + - Done when: all eight named scenarios (plus any further existing ones + wired) pass through Rust via `#[quint_test]`, each comparing the same + fields as T04's smoke replay; both guarded-no-op regressions pass, + proving the Rust driver called the corresponding `protocol::*` function + on the guarded step rather than skipping it; the generated simulation + passes at the configured sample/step budget; re-running it with an + explicit fixed `QUINT_SEED=` reproduces the same outcome twice. + - Verify: `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml + mutation_trace::mbt` with the Nix `quint` binary on `PATH`; the generated + simulation test re-run twice with the same explicit `QUINT_SEED=`, + comparing outcomes. + - Completed: 2026-08-27 + - Files changed: `spec/mutation_cursor.qnt`, + `cli/src/services/mutation_trace/mbt/tests.rs` + - Result: Added two new deterministic `run` scenarios to + `spec/mutation_cursor.qnt` proving guarded/no-op operations still invoke + the real Rust kernel function rather than being skipped: + `testMbtGuardedPrepareInvokesRealPrepare` (`init.then(prepare(Attempt0, + Start(...))).then(prepare(Attempt0, Advance(...)))`, where the second + `prepare` guards because `Attempt0` is no longer `Available`) and + `testMbtGuardedRecoverInvokesRealRecover` (`init.then(recover(WT0))`, + which guards immediately since `init`'s worktrees start untainted, + non-externally-tainted, and not needing rebaseline — the smallest + scenario that hits `recover`'s guarded branch). Both assert the + post-guard state is unchanged from what the guard implies (Attempt0 + stays `Prepared` with its original `Start` boundary; WT0 stays at + `Tree0`/revision `0`), plus `Safety`. Wired all seven remaining named + scenarios (`testStartObservesBeforeActivation`, + `testCloseObservesBeforeDeactivation`, + `testContendedIntervalsRemainAiContended`, + `testNoChangeHookReplayCannotStealFutureChange`, + `testConcurrentObservationsHaveOneWinner`, + `testTaintInvalidatesPreparedObservation`, + `testRecoveryEstablishesBaseline`, `testClosedScopeCannotReactivate`) plus + the two new regressions as `#[quint_test]` functions in `mbt/tests.rs`, + each following T04's established pattern + (`MutationCursorDriver::default()`, no per-scenario driver logic — the + same driver dispatches on `MbtAction` regardless of which named scenario + is replayed). Added + `mutation_cursor_generated_traces_refine_rust_protocol` as + `#[quint_run(spec = "../spec/mutation_cursor.qnt", max_samples = 500, + max_steps = 30)]`, comparing `ModelState` after every generated step + using the same `MbtAction` transport. No driver, model, or protocol code + changed (out of scope, already complete in T04); no new spec actions, + invariants, or state variables were added — only two new named `run` + scenarios exercising existing actions. + - Verify outcomes: `nix run .#quint -- typecheck spec/mutation_cursor.qnt` + — passed, no errors (the bare `nix run .#quint -- test + spec/mutation_cursor.qnt` invocation, without `--match`, prints only the + module header and no test results in this environment — confirmed by + `git stash`/re-run that this is a pre-existing tool quirk on the + unmodified baseline, not caused by this task; `--match '^test.*'` + reliably lists every named test, so it was used for verification + instead). `nix run .#quint -- test spec/mutation_cursor.qnt --match + '^test.*'` — "25 passing" (the pre-existing 23 named scenarios plus the + two new guarded-no-op regressions), including + `testMbtGuardedPrepareInvokesRealPrepare` and + `testMbtGuardedRecoverInvokesRealRecover`. `nix run .#quint -- run + spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore + SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20` — + "[ok] No violation found" (5000 traces, max/min/average trace length 21). + `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml + mutation_trace::mbt` (Nix `quint` 0.32.0 on `PATH`) — "12 passed; 0 + failed" (the T04 smoke test plus all ten scenarios/regressions added by + this task); the full `mutation_trace` suite together — "87 passed; 0 + failed" (the pre-existing ~75 handwritten tests plus all 12 MBT tests, no + regression). `./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` — one diff + (macro-attribute line-wrapping on the new `#[quint_run(...)]` + attribute), fixed by running `cargo fmt`; the check then passed clean. + `QUINT_SEED` reproduction: ran + `mutation_cursor_generated_traces_refine_rust_protocol` twice with + `QUINT_SEED=1337` — both runs generated 500 traces from that seed and + both reported `[OK]`, confirming reproducibility. + - Context impact: none. Only `spec/mutation_cursor.qnt` (two new named + `run` scenarios, no state/action/invariant change) and the test-only + `cli/src/services/mutation_trace/mbt/tests.rs` (gated behind + `#[cfg(test)]`) changed. No production dependency, public interface, CLI + surface, or architecture changed; `protocol.rs`/`types.rs` and the + `mbt/driver.rs`/`mbt/model.rs` T04 already built are untouched by this + task. The corrected-pipeline architecture write-up + (`context/cli/mutation-trace-quint-connect.md`) remains explicitly + deferred to T06 by this plan's own scope. + - Context synchronization: synced + +- [x] T06: `Add a Nix-pinned Rust+Quint CI check and document the architecture` (status:done) + - Task ID: T06 + - Scope: In — a dedicated Nix check (`mutation-trace-quint-connect`) + following the existing `cli-tests`/`cli-clippy`/`cli-fmt` `craneLib` + pattern in `flake.nix` — reusing the repository's pinned `rustToolchain`/ + `craneLib`/`cargoArtifacts` and adding the Nix `quint` package as a check + input — that runs `cargo test --manifest-path cli/Cargo.toml + mutation_trace::mbt` via `cargoTestExtraArgs`, reusing the existing CLI + generated-input mechanism (`scripts/produce-cli-generated-input.sh` / the + `cliGeneratedInput` Nix derivation) rather than bypassing it, and prints + `rustc --version` / `cargo --version` / `quint --version` at least while + stabilizing the check; adding the Nix `quint` package to the *existing* + `checks.cli-tests`' `nativeCheckInputs` too, since `mutation_trace::mbt` + is an ordinary `#[cfg(test)] mod mbt;` already reached by that check's + full `cargo test` run; adding the top-level `spec/` directory to + `workspaceSrc`'s Nix fileset (`craneLib.fileset.commonCargoSources` only + covers Cargo package sources, not files outside any crate, so the Quint + spec was never reaching either check's sandbox and every MBT test failed + there regardless of Quint's availability); `.github/workflows/quint.yml` + updated to invoke the dedicated check instead of stitching together the + Nix Quint binary with the runner's own Cargo, with its change-detector + regex extended to also match `cli/src/services/mutation_trace/mbt/**`, + `.../protocol.rs`, `.../types.rs`, `cli/Cargo.toml`, `cli/Cargo.lock` + (`flake.nix`/`flake.lock` are already watched, so no change needed + there), and its existing "Run Quint tests" step corrected to pass + `--match '^test.*'` (bare `quint test` silently selects zero tests on + this spec rather than erroring, so CI's test step was a silent no-op); + `context/cli/mutation-trace-quint-connect.md` documenting the corrected + architecture (semantic action → `mbtAction` transport → Quint Connect → + Rust driver), the compared/excluded fields (including why `mbtAction` is + excluded), the `randomPrepare` single-branch decision, the + operation-identity-vs-stutter distinction and why it matters (with the + guarded-no-op regressions as the proof), ID mapping, the `u64` revision + limitation, the generated-simulation configuration, deterministic runs + wired, seed reproduction, the Nix-pinned CI command, both Nix checks + needing Quint, and non-goals — see Assumptions for why this replaces the + request's literal `context/plans/...` target; a new entry in + `context/context-map.md`. Out — any change to the existing pure-Quint + typecheck/randomized-safety steps beyond the detector's watched-path + list and the `test` step's `--match` correction. + - Dependencies: T05 + - Done when: both `checks.cli-tests` and the new + `checks.mutation-trace-quint-connect` run the MBT suite under + repository-pinned Rust and Quint and pass; the dedicated check prints + Rust/Cargo/Quint versions at least while stabilizing; + `.github/workflows/quint.yml` invokes the dedicated check without + installing a separate Rust toolchain for this job, and its test step + actually exercises the named scenarios (not a silent zero-test pass); + the change-detector triggers on Rust-only `mutation_trace` changes as + well as spec changes; the context doc exists, covers the required + topics, and is linked from `context/context-map.md`. + - Verify: `nix build .#checks.x86_64-linux.cli-tests`; `nix build + .#checks.x86_64-linux.mutation-trace-quint-connect`; `nix flake check` + where practical; manual diff review of `.github/workflows/quint.yml` and + `flake.nix`; `cat context/cli/mutation-trace-quint-connect.md`; the + plan's full `Full validation` command list run end-to-end. + - Completed: 2026-08-27 + - Files changed: `flake.nix`, `.github/workflows/quint.yml`, + `context/cli/mutation-trace-quint-connect.md` (new), + `context/context-map.md`, `context/plans/mutation-cursor-quint-connect.md` + - Result: A post-implementation review of PR #239 found two defects beyond + the originally planned scope, both fixed here alongside the planned work: + + 1. **Generic `checks.cli-tests` was silently broken.** Since + `mutation_trace::mbt` is an ordinary `#[cfg(test)] mod mbt;`, the + pre-existing generic `checks.cli-tests` (the full `cargo test` every + `nix flake check` already runs) also reaches it — but that check's + `nativeCheckInputs` only listed `pkgs.git`, no Quint. Added + `pkgs.quint` to `checks.cli-tests`' `nativeCheckInputs` alongside the + new dedicated check's. + 2. **`workspaceSrc` never included `spec/`.** Even with Quint on PATH, + every MBT test still failed inside the Nix sandbox with an opaque + `"Quint returned non-zero code."` (`quint-connect`'s + `panic!("{}", err)` is `Display`-only, so the real Quint stderr never + surfaced). Root-caused via `nix build --keep-failed`: the copied + sandbox source tree contained only `cli/`, `config/`, and `.version` + — `craneLib.fileset.commonCargoSources` covers Cargo package sources + only, not the top-level `spec/` directory `quint run`/`quint test` + resolve `../spec/*.qnt` against. Added `(pkgs.lib.fileset.maybeMissing + ./spec)` to `workspaceSrc`'s fileset union. This was the true root + cause; adding Quint to `nativeCheckInputs` alone was necessary but not + sufficient. + + Implemented the originally planned work on top of those fixes: added + `checks.mutation-trace-quint-connect` in `flake.nix` — a + `craneLib.cargoTest` derivation following the `cli-tests`/`cli-clippy`/ + `cli-fmt` pattern exactly, reusing `rustToolchain`/`cargoArtifacts`, + scoped to `mutation_trace::mbt` via `cargoTestExtraArgs`, with + `nativeCheckInputs = [ pkgs.git pkgs.quint ]` and a `preCheck` printing + `rustc`/`cargo`/`quint --version`. Updated `.github/workflows/quint.yml`: + extended the change-detector regex to also match + `cli/src/services/mutation_trace/mbt/**`, `.../protocol.rs`, + `.../types.rs`, `cli/Cargo.toml`, `cli/Cargo.lock`; added a step invoking + `nix build .#checks.x86_64-linux.mutation-trace-quint-connect`; raised + the job's `timeout-minutes` from 15 to 30 (it now compiles the CLI + crate, not just Quint CLI invocations). Also discovered and fixed a + third, pre-existing (not introduced by this plan) latent defect while + validating the workflow: the existing "Run Quint tests" step ran bare + `nix run .#quint -- test spec/mutation_cursor.qnt` with no `--match`, + which — confirmed via `git stash` against the pre-T05 baseline — silently + selects zero tests on this spec (exit 0, no output) rather than running + the 25 named scenarios; that step now passes `--match '^test.*'`. Wrote + `context/cli/mutation-trace-quint-connect.md` (250 lines) documenting the + corrected pipeline, why `mbtAction` exists/is excluded, the + operation-identity-vs-`MbtStutter` distinction, record-payload encoding, + finite ID mapping, comparable-state fields, the `randomPrepare` + single-branch decision, driver/test coverage, the `u64` revision + boundary's relationship to this harness, both Nix checks' shared Quint + dependency and the `workspaceSrc` root cause, and non-goals — linked from + `context/context-map.md`. Cleaned this plan's own stale + pre-implementation Assumptions language (T01/T02/T03 "will be + resolved"/"is decided in T03" phrasing replaced with resolved facts; the + implementation-progress block updated to record T05 complete and T06 as + the (then-)remaining task) and replaced the stale "Open questions" + section with `None.` — both per this task's own additionally-assigned + scope, not a deviation from it. + - Verify outcomes: `nix run .#quint -- typecheck spec/mutation_cursor.qnt` + — passed. `nix run .#quint -- test spec/mutation_cursor.qnt --match + '^test.*'` — "25 passing". `nix run .#quint -- run + spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore + SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20` — + "[ok] No violation found" (5000 traces, up to 21 steps). + `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml + mutation_trace::mbt` — "12 passed; 0 failed". `./scripts/run-cli-cargo.sh + test --manifest-path cli/Cargo.toml mutation_trace` — "87 passed; 0 + failed". `./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. + `QUINT_SEED=1337` run twice against + `mutation_cursor_generated_traces_refine_rust_protocol` — both runs + generated 500 traces from seed `1337` and both reported `[OK]`. `nix + build .#checks.x86_64-linux.cli-tests` — passed, "692 passed; 0 failed" + (680 pre-existing plus the 12 MBT tests, confirming the generic check now + actually reaches and passes the MBT suite). `nix build + .#checks.x86_64-linux.mutation-trace-quint-connect` — passed, "12 + passed; 0 failed; ... 680 filtered out", with `rustc 1.95.0`/`cargo + 1.95.0`/quint `0.32.0` printed by `preCheck`. `nix build + .#checks.x86_64-linux.cli-clippy`, + `.#checks.x86_64-linux.cli-fmt`, `.#checks.x86_64-linux.workflow-actionlint` + — all passed (the last confirms the edited `quint.yml` is valid + Actions YAML). `nix flake check` (x86_64-linux) — "all checks passed!" + (all Nix checks green, including both `cli-tests` and + `mutation-trace-quint-connect`); aarch64-linux/x86_64-darwin/ + aarch64-darwin were evaluated (all four systems' `checks..*` + attribute sets, including `mutation-trace-quint-connect`, resolve without + error, and `pkgs.quint` already existed for all four systems before this + task) but not built, since this sandbox is x86_64-linux only — Darwin + build success is therefore not independently confirmed here. + - Context impact: root. `context/context-map.md` gained a new domain-file + entry for `context/cli/mutation-trace-quint-connect.md` (new), which + documents cross-cutting CI/build behavior (`flake.nix`'s `workspaceSrc` + fileset and both Nix checks) alongside the MBT harness architecture — + this is `root`-classified because the `workspaceSrc`/Quint-availability + fix affects the generic `checks.cli-tests` derivation everyone's `nix + flake check` already runs, not just this plan's own dedicated check. + `context/overview.md`/`context/architecture.md`/`context/glossary.md` + (already updated in T01 to record `quint-connect` as the CLI's first + dev-only dependency) remain accurate and needed no further edit — this + task didn't change the dependency baseline, only fixed the sandbox that + already-declared dependency runs in. + - Context synchronization: synced + +## Open questions + +None. + +## Validation Report + +**Status:** validated +**Date:** 2026-08-27 + +### Commands run + +- `./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace` -> exit 0 (87 passed; 0 failed — pre-existing ~75 handwritten tests plus all 12 MBT tests) +- `./scripts/run-cli-cargo.sh build --manifest-path cli/Cargo.toml` -> exit 0 (`Finished dev profile`) +- `./scripts/run-cli-cargo.sh clippy --manifest-path cli/Cargo.toml --all-targets -- -D warnings` -> exit 0 (no warnings) +- `cargo fmt --manifest-path cli/Cargo.toml -- --check` -> exit 0 (no diff) +- `nix run .#quint -- typecheck spec/mutation_cursor.qnt` -> exit 0 (no errors) +- `nix run .#quint -- test spec/mutation_cursor.qnt --match '^test.*'` -> exit 0 (25 passing) +- `nix run .#quint -- run spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20` -> exit 0 (`[ok] No violation found`, 5000 traces, max/min/avg length 21) +- `nix build .#checks.x86_64-linux.cli-tests` -> exit 0 (692 passed; 0 failed, per `nix log`) +- `nix build .#checks.x86_64-linux.mutation-trace-quint-connect` -> exit 0 (12 passed; 0 failed; 680 filtered out, per `nix log`; `preCheck` printed `rustc`/`cargo`/`quint --version`) +- `nix flake check` (x86_64-linux) -> exit 0 (`all checks passed!`; other systems omitted as incompatible with this sandbox, consistent with T06's prior evaluation-only confirmation) +- `nix run .#regenerate-cargo-sources` then `git diff --stat packaging/flatpak/cargo-sources.json` -> exit 0 (no diff — regeneration is a no-op against the already-committed file) +- `QUINT_SEED=1337 ./scripts/run-cli-cargo.sh test --manifest-path cli/Cargo.toml mutation_trace::mbt::tests::mutation_cursor_generated_traces_refine_rust_protocol` run twice -> exit 0 both times (`[OK]`, 500 traces from seed `1337`, same outcome both runs — AC4 reproduction) + +### Success-criteria verification + +- [x] AC1: `quint-connect` dev/test-only dependency -> `grep -A3 '^\[dev-dependencies\]' cli/Cargo.toml` shows only `quint-connect = "0.1.2"`; absent under `[dependencies]`; build passes. +- [x] AC2: every action reachable from `step` recorded via `MbtAction`, driver dispatches unconditionally -> inspection of `mbt/driver.rs`: every `switch!` arm calls exactly one `protocol::*` function (or mutates only `worktree_trees` for `MbtMutate`, or is a no-op for `MbtStutter`); no independent mutation logic. +- [x] AC3: concrete arguments transported unchanged for both generated and deterministic runs -> `testMbtDriverTransportsNonDefaultArguments` (`mbt/tests.rs`) passes, replaying `mutate(WT1, Tree3)` → `prepare(Attempt5, Flush(WT1))` → `commitAttempt(Attempt5)`. +- [x] AC4: generated trace refinement + seed reproduction -> `mutation_cursor_generated_traces_refine_rust_protocol` (`max_samples=500, max_steps=30`) passed under the Nix-pinned check; `QUINT_SEED=1337` run twice reproduced `[OK]` both times. +- [x] AC5: comparable state matches AC5's field list, excludes `mbtAction`/histories -> inspection of `mbt/model.rs`; `grep` for excluded-history identifiers returns matches only inside doc comments explaining the exclusion. +- [x] AC6: all eight named deterministic scenarios replay via `#[quint_test]` -> confirmed present and green in `mbt/tests.rs` and the 25-passing Quint test run / 12-passing Rust MBT run. +- [x] AC7: pure Quint semantics/`step` structure unchanged -> typecheck, `quint test`, and the 5000×20 `verifyStep` safety run all pass; `step`'s alternative list (`randomMutate, randomPrepare, randomCommit, randomTaint, randomRecover, randomDatabaseFailure, randomAbandon, stutter`) confirmed unchanged by direct inspection. +- [x] AC8: Nix-pinned CI wiring -> `flake.nix` shows `pkgs.quint` in both `cli-tests` and `mutation-trace-quint-connect` `nativeCheckInputs`, `workspaceSrc` fileset includes `./spec`, dedicated check prints tool versions; `.github/workflows/quint.yml` change-detector regex includes `mbt/**`/`protocol.rs`/`types.rs`/`Cargo.toml`/`Cargo.lock`, invokes the dedicated Nix check, and the test step uses `--match '^test.*'`; both `cli-tests` and `mutation-trace-quint-connect` Nix builds pass. +- [x] AC9: no production DB/Git/fs code; `mbt` gated by `#[cfg(test)]` -> `grep -RnE "std::(fs|process|env)|tokio|reqwest|turso" cli/src/services/mutation_trace` returns no matches; `mod mbt;` confirmed behind `#[cfg(test)]` in `mutation_trace/mod.rs`. +- [x] AC10: existing tests/clippy/fmt unmodified and green -> `mutation_trace` suite 87 passed/0 failed (includes the pre-existing ~75); clippy clean; `cargo fmt --check` clean. +- [x] AC11: every argument-carrying `MbtAction` variant is a record -> `spec/mutation_cursor.qnt`'s `MbtAction` definition inspected directly: every variant with fields uses `{ ... }` record syntax; only `MbtInit`/`MbtStutter` are bare. +- [x] AC12: guarded/no-op operations record their own variant, never `MbtStutter` -> `grep` for `mbtStutterAs`/`stutter` call sites shows `prepare`/`taint`/`databaseFailure`/`abandon`/`recover`'s guarded branches each call `mbtStutterAs(MbtOwnVariant(...))`; only the explicit top-level `stutter` action calls `mbtStutterAs(MbtStutter)`. +- [x] AC13: two guarded-no-op regressions prove the real kernel function still runs -> `mutation_cursor_guarded_prepare_invokes_real_prepare` and `mutation_cursor_guarded_recover_invokes_real_recover` (`mbt/tests.rs`) both pass. +- [x] AC14: guarded branches no longer share a single `stutter` call -> same `grep` evidence as AC12: `prepare`/`taint`/`databaseFailure`/`abandon`/`recover` each call `mbtStutterAs` with their own variant rather than the shared top-level `stutter` action; `commitAttempt`'s not-accepted path independently sets `mbtAction' = MbtCommit({attempt})`. + +### Failed checks and follow-ups + +None. + +### Residual risks + +- `nix flake check` in this sandbox evaluated but did not build for `aarch64-linux`/`x86_64-darwin`/`aarch64-darwin` (x86_64-linux-only sandbox); Darwin/other-arch build success remains unverified by this validation run, consistent with T06's own note. +- None otherwise identified. diff --git a/context/sce/flatpak-distribution-patterns.md b/context/sce/flatpak-distribution-patterns.md index 39c613fa..bdff4d2c 100644 --- a/context/sce/flatpak-distribution-patterns.md +++ b/context/sce/flatpak-distribution-patterns.md @@ -14,6 +14,7 @@ Implementation conventions for the source-built `dev.crocoder.sce` Flatpak chann - Generate the Flatpak manifest YAML from a Nix expression (`nix/flatpak/manifest.nix`) rendered via `pkgs.formats.yaml.generate`, exposing three flavors — release-pin, local-checkout override (`type: dir`), and commit-pinned-for-release-package. - The checked-in YAML is a generated artifact regenerated by `nix run .#regenerate-flatpak-manifest` and guarded by `flatpak-manifest-parity`. - Generate `packaging/flatpak/cargo-sources.json` from `cli/Cargo.lock` via a Nix derivation wrapping `flatpak-builder-tools`/`flatpak-cargo-generator.py`, guarded by `cargo-sources-parity`. +- That generator (`nix/flatpak/cargo-sources.nix`) is a fixed-output derivation with a hardcoded `outputHash`, required because `flatpak-cargo-generator.py` needs network access to fetch crate checksums inside the Nix sandbox. Its store path is keyed by `(name, outputHash)`, not by `cli/Cargo.lock`'s content: whenever `cli/Cargo.lock` changes, `nix run .#regenerate-cargo-sources` is a silent no-op against the old, already-realized store path until `outputHash` is bumped first. Update it by setting a dummy value, running the derivation (e.g. `nix build .#checks..cargo-sources-parity`) to read the real hash out of the resulting "hash mismatch" error, writing that in, then regenerating. - Keep Flatpak validation in dedicated Nix-built validator scripts under `nix/flatpak/`: static manifest validation, release-version parity, and local-manifest validation are Bash-owned. No `python3 - <<'PY'` heredoc in `sce-flatpak.sh`. - Keep checked-in Flatpak packaging under `packaging/flatpak/`: source-build manifest (generated), AppStream metadata, host-git wrapper source, Cargo source descriptor (generated), and a thin imperative `sce-flatpak.sh`. Generated assistant payloads are not checked in. diff --git a/flake.nix b/flake.nix index da4d86d7..206f5d85 100644 --- a/flake.nix +++ b/flake.nix @@ -192,6 +192,13 @@ (pkgs.lib.fileset.maybeMissing ./cli/migrations) cliBuildInputFileset (pkgs.lib.fileset.maybeMissing ./cli/assets/hooks) + # The `mutation_trace::mbt` Quint Connect tests shell out to + # `quint run`/`quint test` against `../spec/*.qnt` (relative to + # the `cli/` crate root). `commonCargoSources` only covers Cargo + # package sources, so the top-level `spec/` tree must be listed + # explicitly or it never reaches the sandbox and every MBT test + # fails with an opaque "Quint returned non-zero code." + (pkgs.lib.fileset.maybeMissing ./spec) ]; }; @@ -1541,13 +1548,18 @@ checks = { + # `mutation_trace::mbt` (the Quint Connect model-based-testing + # harness) is an ordinary `#[cfg(test)]` module reached by the + # full `cargo test` this check runs, so the pinned Quint binary + # must be on PATH here too, not only in the dedicated + # `mutation-trace-quint-connect` check below. cli-tests = craneLib.cargoTest ( commonCargoArgs // { pname = "sce-cli-tests"; inherit cargoArtifacts; doCheck = true; - nativeCheckInputs = [ pkgs.git ]; + nativeCheckInputs = [ pkgs.git pkgs.quint ]; } ); @@ -1567,6 +1579,27 @@ } ); + # Focused Quint Connect model-based-testing check: runs only + # `mutation_trace::mbt` under the repository's pinned Rust + # toolchain and pinned Quint binary, reusing the same + # `cargoArtifacts`/`commonCargoArgs` pipeline as `cli-tests` + # rather than a bespoke Rust+Quint environment. + mutation-trace-quint-connect = craneLib.cargoTest ( + commonCargoArgs + // { + pname = "sce-mutation-trace-quint-connect"; + inherit cargoArtifacts; + doCheck = true; + cargoTestExtraArgs = "mutation_trace::mbt"; + nativeCheckInputs = [ pkgs.git pkgs.quint ]; + preCheck = '' + rustc --version + cargo --version + quint --version + ''; + } + ); + cli-generated-input = cliGeneratedInputCheck; pkl-generated = pklGeneratedCheck; codex-hook-command = codexHookCommandCheck; diff --git a/nix/flatpak/cargo-sources.nix b/nix/flatpak/cargo-sources.nix index 60884987..e9879cff 100644 --- a/nix/flatpak/cargo-sources.nix +++ b/nix/flatpak/cargo-sources.nix @@ -33,7 +33,7 @@ let outputHashMode = "flat"; outputHashAlgo = "sha256"; - outputHash = "sha256-gFfKqW8lDLnJW8K7281zdOrCQztWy4YbzICQfxGWZ9w="; + outputHash = "sha256-p8fzi7KWNltCEopHvXFmswASt9ov7UWxh/XU8mGLgH0="; }; regenerateApp = pkgs.writeShellApplication { diff --git a/packaging/flatpak/cargo-sources.json b/packaging/flatpak/cargo-sources.json index fc4ea364..2d8e1844 100644 --- a/packaging/flatpak/cargo-sources.json +++ b/packaging/flatpak/cargo-sources.json @@ -519,6 +519,19 @@ "dest": "cargo/vendor/bit-vec-0.8.0", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/bitflags/bitflags-1.3.2.crate", + "sha256": "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a", + "dest": "cargo/vendor/bitflags-1.3.2" + }, + { + "type": "inline", + "contents": "{\"package\": \"bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a\", \"files\": {}}", + "dest": "cargo/vendor/bitflags-1.3.2", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -662,6 +675,19 @@ "dest": "cargo/vendor/branches-0.4.4", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/bs58/bs58-0.5.1.crate", + "sha256": "bf88ba1141d185c399bee5288d850d63b8369520c1eafc32a0430b5b6c287bf4", + "dest": "cargo/vendor/bs58-0.5.1" + }, + { + "type": "inline", + "contents": "{\"package\": \"bf88ba1141d185c399bee5288d850d63b8369520c1eafc32a0430b5b6c287bf4\", \"files\": {}}", + "dest": "cargo/vendor/bs58-0.5.1", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -974,6 +1000,19 @@ "dest": "cargo/vendor/colorchoice-1.0.5", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/colored/colored-3.1.1.crate", + "sha256": "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34", + "dest": "cargo/vendor/colored-3.1.1" + }, + { + "type": "inline", + "contents": "{\"package\": \"faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34\", \"files\": {}}", + "dest": "cargo/vendor/colored-3.1.1", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -1299,6 +1338,32 @@ "dest": "cargo/vendor/darling_macro-0.23.0", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/dashu-base/dashu-base-0.4.3.crate", + "sha256": "993b95dc1b248e3f5747dcb017a41d6e75853a2e5ee4504f7d537c5b8dffdae4", + "dest": "cargo/vendor/dashu-base-0.4.3" + }, + { + "type": "inline", + "contents": "{\"package\": \"993b95dc1b248e3f5747dcb017a41d6e75853a2e5ee4504f7d537c5b8dffdae4\", \"files\": {}}", + "dest": "cargo/vendor/dashu-base-0.4.3", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/dashu-int/dashu-int-0.4.3.crate", + "sha256": "49c05a0d5cb0b39fcc87c46432fdac24b90dce239857c7f6b798be4ffc3c42c6", + "dest": "cargo/vendor/dashu-int-0.4.3" + }, + { + "type": "inline", + "contents": "{\"package\": \"49c05a0d5cb0b39fcc87c46432fdac24b90dce239857c7f6b798be4ffc3c42c6\", \"files\": {}}", + "dest": "cargo/vendor/dashu-int-0.4.3", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -1325,6 +1390,45 @@ "dest": "cargo/vendor/datasketches-0.2.0", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/defmt/defmt-1.1.1.crate", + "sha256": "e2953bfe4f93bbd20cc71198842756f77d161884c99ebbabc41d80231ded88d1", + "dest": "cargo/vendor/defmt-1.1.1" + }, + { + "type": "inline", + "contents": "{\"package\": \"e2953bfe4f93bbd20cc71198842756f77d161884c99ebbabc41d80231ded88d1\", \"files\": {}}", + "dest": "cargo/vendor/defmt-1.1.1", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/defmt-macros/defmt-macros-1.1.1.crate", + "sha256": "bad9c72e7ca2137e0dc3813245a0d282fd6daad32fd800af018306a9169b5fe8", + "dest": "cargo/vendor/defmt-macros-1.1.1" + }, + { + "type": "inline", + "contents": "{\"package\": \"bad9c72e7ca2137e0dc3813245a0d282fd6daad32fd800af018306a9169b5fe8\", \"files\": {}}", + "dest": "cargo/vendor/defmt-macros-1.1.1", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/defmt-parser/defmt-parser-1.0.0.crate", + "sha256": "10d60334b3b2e7c9d91ef8150abfb6fa4c1c39ebbcf4a81c2e346aad939fee3e", + "dest": "cargo/vendor/defmt-parser-1.0.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"10d60334b3b2e7c9d91ef8150abfb6fa4c1c39ebbcf4a81c2e346aad939fee3e\", \"files\": {}}", + "dest": "cargo/vendor/defmt-parser-1.0.0", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -2079,6 +2183,19 @@ "dest": "cargo/vendor/h2-0.4.15", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/hashbrown/hashbrown-0.12.3.crate", + "sha256": "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888", + "dest": "cargo/vendor/hashbrown-0.12.3" + }, + { + "type": "inline", + "contents": "{\"package\": \"8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888\", \"files\": {}}", + "dest": "cargo/vendor/hashbrown-0.12.3", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -2521,6 +2638,19 @@ "dest": "cargo/vendor/idna_adapter-1.2.2", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/indexmap/indexmap-1.9.3.crate", + "sha256": "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99", + "dest": "cargo/vendor/indexmap-1.9.3" + }, + { + "type": "inline", + "contents": "{\"package\": \"bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99\", \"files\": {}}", + "dest": "cargo/vendor/indexmap-1.9.3", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -2690,6 +2820,19 @@ "dest": "cargo/vendor/itertools-0.14.0", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/itf/itf-0.4.0.crate", + "sha256": "5d620b7b3d17650581da9208d1240baaff4ee33decff1c7782bdb9b4cab71c20", + "dest": "cargo/vendor/itf-0.4.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"5d620b7b3d17650581da9208d1240baaff4ee33decff1c7782bdb9b4cab71c20\", \"files\": {}}", + "dest": "cargo/vendor/itf-0.4.0", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -2703,6 +2846,71 @@ "dest": "cargo/vendor/itoa-1.0.18", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/jiff/jiff-0.2.35.crate", + "sha256": "668b7183bd07af9a4885f5c35b0cc5c83c4607a913c16b7e17291832910d2dcc", + "dest": "cargo/vendor/jiff-0.2.35" + }, + { + "type": "inline", + "contents": "{\"package\": \"668b7183bd07af9a4885f5c35b0cc5c83c4607a913c16b7e17291832910d2dcc\", \"files\": {}}", + "dest": "cargo/vendor/jiff-0.2.35", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/jiff-core/jiff-core-0.1.0.crate", + "sha256": "7feca88439efe53da3754500c1851dedf3cb36c524dd5cf8225cc0794de95d09", + "dest": "cargo/vendor/jiff-core-0.1.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"7feca88439efe53da3754500c1851dedf3cb36c524dd5cf8225cc0794de95d09\", \"files\": {}}", + "dest": "cargo/vendor/jiff-core-0.1.0", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/jiff-static/jiff-static-0.2.35.crate", + "sha256": "3a69dcb3a21cfb32ce1cd056169337ca284af0766dd766e7878819b251a49204", + "dest": "cargo/vendor/jiff-static-0.2.35" + }, + { + "type": "inline", + "contents": "{\"package\": \"3a69dcb3a21cfb32ce1cd056169337ca284af0766dd766e7878819b251a49204\", \"files\": {}}", + "dest": "cargo/vendor/jiff-static-0.2.35", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/jiff-tzdb/jiff-tzdb-0.1.8.crate", + "sha256": "142bd39932ad231f10513df9ab62661fead8719872150b7ad02a2df79f4e141e", + "dest": "cargo/vendor/jiff-tzdb-0.1.8" + }, + { + "type": "inline", + "contents": "{\"package\": \"142bd39932ad231f10513df9ab62661fead8719872150b7ad02a2df79f4e141e\", \"files\": {}}", + "dest": "cargo/vendor/jiff-tzdb-0.1.8", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/jiff-tzdb-platform/jiff-tzdb-platform-0.1.3.crate", + "sha256": "875a5a69ac2bab1a891711cf5eccbec1ce0341ea805560dcd90b7a2e925132e8", + "dest": "cargo/vendor/jiff-tzdb-platform-0.1.3" + }, + { + "type": "inline", + "contents": "{\"package\": \"875a5a69ac2bab1a891711cf5eccbec1ce0341ea805560dcd90b7a2e925132e8\", \"files\": {}}", + "dest": "cargo/vendor/jiff-tzdb-platform-0.1.3", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -3366,6 +3574,32 @@ "dest": "cargo/vendor/num-iter-0.1.45", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/num-modular/num-modular-0.6.5.crate", + "sha256": "bd8e500409e6cd603b03e477c26a6caecdc27ac58979a53e881c75eafc079f44", + "dest": "cargo/vendor/num-modular-0.6.5" + }, + { + "type": "inline", + "contents": "{\"package\": \"bd8e500409e6cd603b03e477c26a6caecdc27ac58979a53e881c75eafc079f44\", \"files\": {}}", + "dest": "cargo/vendor/num-modular-0.6.5", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/num-order/num-order-1.2.0.crate", + "sha256": "537b596b97c40fcf8056d153049eb22f481c17ebce72a513ec9286e4986d1bb6", + "dest": "cargo/vendor/num-order-1.2.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"537b596b97c40fcf8056d153049eb22f481c17ebce72a513ec9286e4986d1bb6\", \"files\": {}}", + "dest": "cargo/vendor/num-order-1.2.0", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -3704,6 +3938,19 @@ "dest": "cargo/vendor/portable-atomic-1.15.0", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/portable-atomic-util/portable-atomic-util-0.2.7.crate", + "sha256": "c2a106d1259c23fac8e543272398ae0e3c0b8d33c88ed73d0cc71b0f1d902618", + "dest": "cargo/vendor/portable-atomic-util-0.2.7" + }, + { + "type": "inline", + "contents": "{\"package\": \"c2a106d1259c23fac8e543272398ae0e3c0b8d33c88ed73d0cc71b0f1d902618\", \"files\": {}}", + "dest": "cargo/vendor/portable-atomic-util-0.2.7", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -3847,6 +4094,32 @@ "dest": "cargo/vendor/quinn-udp-0.5.14", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/quint-connect/quint-connect-0.1.2.crate", + "sha256": "67a4e156a3d4580b73eff41805d3237c909f96388158b3eed12afaa4f619d61c", + "dest": "cargo/vendor/quint-connect-0.1.2" + }, + { + "type": "inline", + "contents": "{\"package\": \"67a4e156a3d4580b73eff41805d3237c909f96388158b3eed12afaa4f619d61c\", \"files\": {}}", + "dest": "cargo/vendor/quint-connect-0.1.2", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/quint-connect-macros/quint-connect-macros-0.1.2.crate", + "sha256": "814c6e076fa655b78d7127fda492f3fa980b8827fda16c33d891b57c8ccd735f", + "dest": "cargo/vendor/quint-connect-macros-0.1.2" + }, + { + "type": "inline", + "contents": "{\"package\": \"814c6e076fa655b78d7127fda492f3fa980b8827fda16c33d891b57c8ccd735f\", \"files\": {}}", + "dest": "cargo/vendor/quint-connect-macros-0.1.2", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -4393,6 +4666,32 @@ "dest": "cargo/vendor/schannel-0.1.29", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/schemars/schemars-0.9.0.crate", + "sha256": "4cd191f9397d57d581cddd31014772520aa448f65ef991055d7f61582c65165f", + "dest": "cargo/vendor/schemars-0.9.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"4cd191f9397d57d581cddd31014772520aa448f65ef991055d7f61582c65165f\", \"files\": {}}", + "dest": "cargo/vendor/schemars-0.9.0", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/schemars/schemars-1.2.2.crate", + "sha256": "687274d293b6cdc6e73e0fee520bf2049650090d7164f87672d212a3c530cf4a", + "dest": "cargo/vendor/schemars-1.2.2" + }, + { + "type": "inline", + "contents": "{\"package\": \"687274d293b6cdc6e73e0fee520bf2049650090d7164f87672d212a3c530cf4a\", \"files\": {}}", + "dest": "cargo/vendor/schemars-1.2.2", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -4562,6 +4861,32 @@ "dest": "cargo/vendor/serde_urlencoded-0.7.1", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/serde_with/serde_with-3.22.0.crate", + "sha256": "ee78f1fbe43ac4a0e47aadb3dbd357b69eb0d3793e948624cd03dd2750ab1c0a", + "dest": "cargo/vendor/serde_with-3.22.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"ee78f1fbe43ac4a0e47aadb3dbd357b69eb0d3793e948624cd03dd2750ab1c0a\", \"files\": {}}", + "dest": "cargo/vendor/serde_with-3.22.0", + "dest-filename": ".cargo-checksum.json" + }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/serde_with_macros/serde_with_macros-3.22.0.crate", + "sha256": "8705578779c2b6bd90d84d66eb2e206b708b1a4d7b9f17641b293545bf1c7e46", + "dest": "cargo/vendor/serde_with_macros-3.22.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"8705578779c2b6bd90d84d66eb2e206b708b1a4d7b9f17641b293545bf1c7e46\", \"files\": {}}", + "dest": "cargo/vendor/serde_with_macros-3.22.0", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -4718,6 +5043,19 @@ "dest": "cargo/vendor/simdutf8-0.1.5", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/similar/similar-2.7.0.crate", + "sha256": "bbbb5d9659141646ae647b42fe094daf6c6192d1620870b449d9557f748b2daa", + "dest": "cargo/vendor/similar-2.7.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"bbbb5d9659141646ae647b42fe094daf6c6192d1620870b449d9557f748b2daa\", \"files\": {}}", + "dest": "cargo/vendor/similar-2.7.0", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", @@ -4822,6 +5160,19 @@ "dest": "cargo/vendor/stable_deref_trait-1.2.1", "dest-filename": ".cargo-checksum.json" }, + { + "type": "archive", + "archive-type": "tar-gzip", + "url": "https://static.crates.io/crates/static_assertions/static_assertions-1.1.0.crate", + "sha256": "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f", + "dest": "cargo/vendor/static_assertions-1.1.0" + }, + { + "type": "inline", + "contents": "{\"package\": \"a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f\", \"files\": {}}", + "dest": "cargo/vendor/static_assertions-1.1.0", + "dest-filename": ".cargo-checksum.json" + }, { "type": "archive", "archive-type": "tar-gzip", diff --git a/spec/mutation_cursor.qnt b/spec/mutation_cursor.qnt index 05dd643f..1c4742fd 100644 --- a/spec/mutation_cursor.qnt +++ b/spec/mutation_cursor.qnt @@ -116,6 +116,23 @@ module mutation_cursor { mutationEvents: Set[MutationEvent], } + // Verification-only transport for Quint Connect: identifies the semantic + // operation and concrete arguments each step invoked, including on a + // guarded/no-op path, so the Rust driver can dispatch on it. Every + // argument-carrying variant is a record, even single-field ones, to match + // Quint Connect's unit-vs-record action decoder. Never read by any other + // action, value, or invariant. + type MbtAction = + | MbtInit + | MbtMutate({ worktree: WorktreeId, tree: TreeId }) + | MbtPrepare({ attempt: AttemptId, boundary: Boundary }) + | MbtCommit({ attempt: AttemptId }) + | MbtTaint({ worktree: WorktreeId }) + | MbtDatabaseFailure({ worktree: WorktreeId }) + | MbtAbandon({ scope: ScopeId }) + | MbtRecover({ worktree: WorktreeId }) + | MbtStutter + val WORKTREES: Set[WorktreeId] = Set(WT0, WT1) val SCOPES: Set[ScopeId] = Set(Scope0, Scope1, Scope2, Scope3) val TREES: Set[TreeId] = Set(Tree0, Tree1, Tree2, Tree3) @@ -261,6 +278,7 @@ module mutation_cursor { var taintHistory: Set[DurableProtocolCheckpoint] var evidenceAttempts: Set[AttemptId] var mutationEvents: Set[MutationEvent] + var mbtAction: MbtAction def liveScopesOn(worktree: WorktreeId): Set[ScopeId] = SCOPES.filter(scope => { @@ -372,9 +390,14 @@ module mutation_cursor { taintHistory' = Set(), evidenceAttempts' = Set(), mutationEvents' = Set(), + mbtAction' = MbtInit, } - action stutter: bool = all { + // Shared no-semantic-change transition, parameterized on the MbtAction to + // record. `stutter` itself is the only caller that passes MbtStutter; every + // guarded/no-op action passes its own operation-specific variant instead, + // so the invoked operation is never erased by falling through to `stutter`. + action mbtStutterAs(taken: MbtAction): bool = all { worktrees' = worktrees, scopes' = scopes, worktreeTrees' = worktreeTrees, @@ -392,8 +415,11 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = taken, } + action stutter: bool = mbtStutterAs(MbtStutter) + action mutate(worktree: WorktreeId, newTree: TreeId): bool = all { worktrees' = worktrees, scopes' = scopes, @@ -412,6 +438,7 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = MbtMutate({ worktree: worktree, tree: newTree }), } action prepareAvailable(attempt: AttemptId, boundary: Boundary): bool = { @@ -442,12 +469,13 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = MbtPrepare({ attempt: attempt, boundary: boundary }), } } action prepare(attempt: AttemptId, boundary: Boundary): bool = if (attempts.get(attempt).status != Available) { - stutter + mbtStutterAs(MbtPrepare({ attempt: attempt, boundary: boundary })) } else { prepareAvailable(attempt, boundary) } @@ -525,6 +553,7 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = MbtCommit({ attempt: attempt }), } } else { val nextScope = @@ -656,6 +685,7 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = nextEvidenceAttempts, mutationEvents' = mutationEvents.union(emitted), + mbtAction' = MbtCommit({ attempt: attempt }), } } } @@ -696,6 +726,7 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = MbtTaint({ worktree: worktree }), } } @@ -704,7 +735,7 @@ module mutation_cursor { worktrees.get(worktree).tainted or externalTaint.contains(worktree) ) { - stutter + mbtStutterAs(MbtTaint({ worktree: worktree })) } else { taintHealthy(worktree) } @@ -727,11 +758,12 @@ module mutation_cursor { taintHistory' = taintHistory.union(Set(durableProtocolStateFor(worktree))), evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = MbtDatabaseFailure({ worktree: worktree }), } action databaseFailure(worktree: WorktreeId): bool = if (externalTaint.contains(worktree)) { - stutter + mbtStutterAs(MbtDatabaseFailure({ worktree: worktree })) } else { recordDatabaseFailure(worktree) } @@ -788,6 +820,7 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = MbtAbandon({ scope: scope }), } } @@ -798,7 +831,7 @@ module mutation_cursor { not(isLive(oldScope.status)) or externalTaint.contains(oldScope.worktreeId) ) { - stutter + mbtStutterAs(MbtAbandon({ scope: scope })) } else { abandonLiveScope(scope) } @@ -868,6 +901,7 @@ module mutation_cursor { taintHistory' = taintHistory, evidenceAttempts' = evidenceAttempts, mutationEvents' = mutationEvents, + mbtAction' = MbtRecover({ worktree: worktree }), } } @@ -879,7 +913,7 @@ module mutation_cursor { not(externalTaint.contains(worktree)) and not(state.needsRebaseline) ) { - stutter + mbtStutterAs(MbtRecover({ worktree: worktree })) } else { recoverNeeded(worktree) } @@ -891,6 +925,11 @@ module mutation_cursor { mutate(worktree, tree) } + // Stays a single top-level `step` alternative. `prepare` already sets + // `mbtAction' = MbtPrepare({ attempt, boundary })` on every path, and + // `boundary` here is the exact concrete value passed to whichever inner + // `any` branch fires, so Quint Connect already exposes which boundary kind + // was selected without a dedicated `PrepareKind` choice. action randomPrepare: bool = { nondet attempt = ATTEMPTS.oneOf() nondet scope = SCOPES.oneOf() @@ -1734,4 +1773,51 @@ module mutation_cursor { .expect(worktrees.get(WT1).cursorTree == Tree2) .expect(scopes.get(Scope3).status == Abandoned) .expect(Safety) + + // Non-default-values smoke scenario for the Rust MBT driver (T04): proves + // that a worktree/tree/attempt/boundary combination other than the + // WT0/Tree0-Tree1/Attempt0/Flush(WT0) defaults used throughout the runs + // above is transported end to end. `#[quint_test]` replays this exact + // scenario through `protocol::prepare`/`protocol::commit` and compares the + // resulting Rust state against the state asserted below. + run testMbtDriverTransportsNonDefaultArguments = + init + .then(mutate(WT1, Tree3)) + .then(prepare(Attempt5, Flush(WT1))) + .then(commitAttempt(Attempt5)) + .expect(worktrees.get(WT1).cursorTree == Tree3) + .expect(worktrees.get(WT1).revision == 1) + .expect(attempts.get(Attempt5).status == Committed) + .expect(Safety) + + // Guarded-no-op regression: re-preparing Attempt0 after + // it is already Prepared hits `prepare`'s guarded branch + // (`attempts.get(attempt).status != Available`), which must still record + // `MbtPrepare({attempt: Attempt0, boundary: Advance(...)})` — the second + // call's own operation and arguments — rather than falling through to + // `MbtStutter`. `#[quint_test]` replays this through the real + // `protocol::prepare`, proving the Rust driver calls it a second time + // (never skipping the call because Quint's semantic state is unchanged) + // and independently reaches the same no-op outcome. + run testMbtGuardedPrepareInvokesRealPrepare = + init + .then(prepare(Attempt0, Start({ scope: Scope0, event: Event0 }))) + .then(prepare(Attempt0, Advance({ scope: Scope0, event: Event1 }))) + .expect(attempts.get(Attempt0).status == Prepared) + .expect(attempts.get(Attempt0).boundary == Start({ scope: Scope0, event: Event0 })) + .expect(Safety) + + // Guarded-no-op regression: `recover(WT0)` on a worktree + // that is neither tainted, externally tainted, nor needing rebaseline hits + // `recover`'s guarded branch, which must still record + // `MbtRecover({worktree: WT0})` rather than `MbtStutter`. `#[quint_test]` + // replays this through the real `protocol::recover`, proving the Rust + // driver calls it (never skipping the call) and independently reaches the + // same no-op outcome. + run testMbtGuardedRecoverInvokesRealRecover = + init + .then(recover(WT0)) + .expect(worktrees.get(WT0).cursorTree == Tree0) + .expect(worktrees.get(WT0).revision == 0) + .expect(Safety) }