From 5ea15dbe66b7e041e0aa03b9079b820fbe05f574 Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 00:23:12 +0200 Subject: [PATCH 1/9] mutation-trace: Add Quint Connect refinement plan Define the staged implementation for continuously checking the pure Rust mutation-trace protocol against the Quint model. The plan covers the dev-only dependency, named randomized prepare actions, model-based driver and state projection, deterministic scenario replays, generated traces with seed reproduction, CI wiring, and architecture documentation. Plan: mutation-cursor-quint-connect (T01-T06) Co-authored-by: SCE --- .../plans/mutation-cursor-quint-connect.md | 583 ++++++++++++++++++ 1 file changed, 583 insertions(+) create mode 100644 context/plans/mutation-cursor-quint-connect.md diff --git a/context/plans/mutation-cursor-quint-connect.md b/context/plans/mutation-cursor-quint-connect.md new file mode 100644 index 00000000..fe145077 --- /dev/null +++ b/context/plans/mutation-cursor-quint-connect.md @@ -0,0 +1,583 @@ +# 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, latest reviewed head +`ea23caf5`, plan-only, confirmed current via `git fetch`), 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 currently fall 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 + +- [ ] 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. +- [ ] 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. +- [ ] 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. +- [ ] 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. +- [ ] 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. +- [ ] 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. +- [ ] 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. +- [ ] 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. + - Validate: inspection of the new Nix check definition (`craneLib`-based, + reusing the repository `rustToolchain`, with the Nix `quint` package + available to the test run) and `.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 unchanged in behavior. +- [ ] 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)]`. +- [ ] 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`. +- [ ] 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. +- [ ] 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. +- [ ] 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. +- [ ] 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` +- `nix run .#quint -- run spec/mutation_cursor.qnt --step=verifyStep --invariants SafetyCore SafetyAttribution SafetyHistory --max-samples=5000 --max-steps=20` +- `nix build .#checks..mutation-trace-quint-connect` (exact attribute name confirmed in T06) — the Nix-pinned Rust+Quint Quint Connect suite +- `nix flake check` if the new check is wired into normal flake checks +- `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. +- The exact `quint-connect` crate/package name, current compatible version, + and its custom action/nondet `Config` API for driver dispatch are resolved + in T01 against the upstream `quint-co/quint-connect` repository (README and + `connect/examples/two_phase_commit/mbt.rs`, plus any example closer to a + Choreo-style action-plus-arguments sum type) at implementation time, per + the request's own instruction not to assume `0.1.2` or the illustrative + `Driver`/`State`/`#[quint_run]`/`#[quint_test]`/`switch!`/`Config` + sketches are still current. This same research step confirms exactly how + Quint Connect's custom decoder distinguishes a unit variant from a record + variant, which is the mechanism AC11's record-payload rule depends on. +- Whether `randomPrepare`'s selected boundary needs a dedicated + `PrepareKind`-style nondet choice, or is already fully observable from the + `MbtPrepare { attempt, boundary }` variant `mbtAction` records regardless of + which `any { ... }` branch fired, is decided in T03 by testing the smallest + option first, per the request's own "prefer the smallest correct solution" + instruction. +- As of this revision, `prepare` (spec line 448-453), `taint` (~702-711), + `databaseFailure` (~732-737), `abandon` (~794-805), and `recover` + (~874-886) each guard their real transition and fall through to the shared + top-level `stutter` action on the guarded path; `commitAttempt` + (line 455+) computes its own `fresh`/`accepted`/`changed` logic rather than + delegating to `stutter`. T02 audits all six (not just the five that + currently call `stutter`) for a guarded/no-op path and applies the same + operation-identity-preserving fix wherever one exists; exact line numbers + are re-checked at implementation time since T02/T03 edit this same file + before T02's own guard refactor lands. +- PR #238 (branch `mutation-cursor`) is confirmed open, not merged, based on + `main`. PR #239 (branch `quint-connect`, latest reviewed head `ea23caf5`, + confirmed current via `git fetch`) stacks on PR #238's head (`2a097408`) + and at the time of this revision contains only this plan file — no + implementation has started, so this revision changes the plan only, per + the request's own "plan correction only" instruction. + +## Task stack + +- [ ] T01: `Pin quint-connect as a CLI dev-dependency` (status:todo) + - 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. + - Context synchronization: pending + +- [ ] T02: `Add operation-preserving MBT action-transport instrumentation to the spec` (status:todo) + - 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. + - Context synchronization: pending + +- [ ] T03: `Keep randomPrepare a single step alternative while making it Connect-observable` (status:todo) + - 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). + - Context synchronization: pending + +- [ ] T04: `Build the MBT driver, ID mapping, and comparable model state` (status:todo) + - 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`. + - Context synchronization: pending + +- [ ] T05: `Wire deterministic scenario replays, guarded-no-op regressions, and the generated Quint Connect simulation` (status:todo) + - 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. + - Context synchronization: pending + +- [ ] T06: `Add a Nix-pinned Rust+Quint CI check and document the architecture` (status:todo) + - Task ID: T06 + - Scope: In — a dedicated Nix check (e.g. `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`, 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; `.github/workflows/quint.yml` updated to invoke that 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); + `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, 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/test/ + randomized-safety steps beyond the detector's watched-path list. + - Dependencies: T05 + - Done when: the new Nix check runs the MBT suite under repository-pinned + Rust and Quint, printing their versions at least while stabilizing; + `.github/workflows/quint.yml` invokes it without installing a separate + Rust toolchain for this job; 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..mutation-trace-quint-connect` (or + `nix flake check` if wired into normal checks) run locally; manual diff + review of `.github/workflows/quint.yml`; `cat + context/cli/mutation-trace-quint-connect.md`; the plan's full `Full + validation` command list run end-to-end. + - Context synchronization: pending + +## Open questions + +None. The genuine ambiguities found while planning — the requested +architecture-doc path colliding with this plan's own file, the exact +`quint-connect` version/custom-action API, and whether `commitAttempt` has a +guarded no-op path analogous to the other five actions — resolve cleanly by +repository convention and by deferring live verification to T01/T02, both +recorded under Assumptions rather than blocking authoring, since none of them +changes scope or acceptance criteria. Whether `randomPrepare`'s boundary +needs a dedicated `PrepareKind` beyond `mbtAction` is an implementation-time +decision scoped explicitly into T03's Done-when criteria, not a +planning-time unknown. From d5f10a35ceddc415b4656739445a86dd7f43bde7 Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 01:03:12 +0200 Subject: [PATCH 2/9] cli: Add quint-connect for model-based testing Enable the planned mutation-cursor Quint Connect harness without adding a runtime dependency by declaring quint-connect as a CLI dev-dependency and refreshing the Cargo lockfile and Flatpak cargo source descriptors. Document the dependency baseline and complete the dependency-pinning task for the model-based-testing plan. Plan: mutation-cursor-quint-connect, T01 Co-authored-by: SCE --- cli/Cargo.lock | 312 +++++++++++++++- cli/Cargo.toml | 3 + context/architecture.md | 2 +- context/glossary.md | 2 +- context/overview.md | 2 +- .../plans/mutation-cursor-quint-connect.md | 67 +++- context/sce/flatpak-distribution-patterns.md | 1 + nix/flatpak/cargo-sources.nix | 2 +- packaging/flatpak/cargo-sources.json | 351 ++++++++++++++++++ 9 files changed, 722 insertions(+), 20 deletions(-) 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/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/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 index fe145077..9cca574d 100644 --- a/context/plans/mutation-cursor-quint-connect.md +++ b/context/plans/mutation-cursor-quint-connect.md @@ -346,7 +346,7 @@ Persist this field in every plan; this is durable plan state, not chat state: ## Task stack -- [ ] T01: `Pin quint-connect as a CLI dev-dependency` (status:todo) +- [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 @@ -365,7 +365,70 @@ Persist this field in every plan; this is durable plan state, not chat state: - 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. - - Context synchronization: pending + - 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 - [ ] T02: `Add operation-preserving MBT action-transport instrumentation to the spec` (status:todo) - Task ID: T02 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/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", From ba9a2aa04129f0c1396f926972fa091b8fe44aee Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 01:15:26 +0200 Subject: [PATCH 3/9] spec: Add operation-specific MBT action instrumentation Record the semantic operation and concrete arguments in a verification-only MbtAction state variable, including guarded no-op paths, so Quint Connect can dispatch on the invoked operation without stutter erasing its attribution. Update the mutation cursor actions while preserving their semantic state transitions and verify the spec's existing scenarios and safety invariants. Plan: mutation-cursor-quint-connect T02 Co-authored-by: SCE --- .../plans/mutation-cursor-quint-connect.md | 65 ++++++++++++++++++- spec/mutation_cursor.qnt | 46 +++++++++++-- 2 files changed, 103 insertions(+), 8 deletions(-) diff --git a/context/plans/mutation-cursor-quint-connect.md b/context/plans/mutation-cursor-quint-connect.md index 9cca574d..08d5e8a6 100644 --- a/context/plans/mutation-cursor-quint-connect.md +++ b/context/plans/mutation-cursor-quint-connect.md @@ -430,7 +430,7 @@ Persist this field in every plan; this is durable plan state, not chat state: introduce no new runtime architecture or production interface. - Context synchronization: synced -- [ ] T02: `Add operation-preserving MBT action-transport instrumentation to the spec` (status:todo) +- [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 @@ -476,7 +476,68 @@ Persist this field in every plan; this is durable plan state, not chat state: inspection of one guarded `prepare` call and one guarded `recover` (or `abandon`) call, confirming their operation-specific `MbtAction` — not `MbtStutter` — is recorded. - - Context synchronization: pending + - 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 - [ ] T03: `Keep randomPrepare a single step alternative while making it Connect-observable` (status:todo) - Task ID: T03 diff --git a/spec/mutation_cursor.qnt b/spec/mutation_cursor.qnt index 05dd643f..5606804b 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) } From b69e4ed2d5a772c9db997ea6f035b7f3499732e0 Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 01:21:32 +0200 Subject: [PATCH 4/9] spec: Document Connect-visible prepare boundary selection Record why `randomPrepare` remains a single `step` alternative: `prepare` already carries the concrete boundary through `MbtPrepare`, so no redundant `PrepareKind` choice is needed. Mark the completed task and verification evidence in the associated plan without changing model behavior. Plan: mutation-cursor-quint-connect.md (T03) Co-authored-by: SCE --- .../plans/mutation-cursor-quint-connect.md | 45 ++++++++++++++++++- spec/mutation_cursor.qnt | 5 +++ 2 files changed, 48 insertions(+), 2 deletions(-) diff --git a/context/plans/mutation-cursor-quint-connect.md b/context/plans/mutation-cursor-quint-connect.md index 08d5e8a6..7bccc8af 100644 --- a/context/plans/mutation-cursor-quint-connect.md +++ b/context/plans/mutation-cursor-quint-connect.md @@ -539,7 +539,7 @@ Persist this field in every plan; this is durable plan state, not chat state: this plan's own scope, not skipped here. - Context synchronization: synced -- [ ] T03: `Keep randomPrepare a single step alternative while making it Connect-observable` (status:todo) +- [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); @@ -564,7 +564,48 @@ Persist this field in every plan; this is durable plan state, not chat state: 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). - - Context synchronization: pending + - 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 - [ ] T04: `Build the MBT driver, ID mapping, and comparable model state` (status:todo) - Task ID: T04 diff --git a/spec/mutation_cursor.qnt b/spec/mutation_cursor.qnt index 5606804b..0eb898a3 100644 --- a/spec/mutation_cursor.qnt +++ b/spec/mutation_cursor.qnt @@ -925,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() From 535a22c7ee3f77683a16c24b6895b78d64c35ebf Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 09:15:51 +0200 Subject: [PATCH 5/9] mutation-trace: Add Quint Connect model-based test driver Connect the mutation cursor Quint model to the pure Rust protocol so non-default trace arguments and resulting comparable state are exercised end to end. Add ITF wire mappings, a test-only driver, and a non-default-value replay scenario without changing production behavior. Plan: mutation-cursor-quint-connect T04 Co-authored-by: SCE --- cli/src/services/mutation_trace/mbt/driver.rs | 230 +++++++++ cli/src/services/mutation_trace/mbt/mod.rs | 13 + cli/src/services/mutation_trace/mbt/model.rs | 467 ++++++++++++++++++ cli/src/services/mutation_trace/mbt/tests.rs | 22 + cli/src/services/mutation_trace/mod.rs | 3 + .../plans/mutation-cursor-quint-connect.md | 131 ++++- spec/mutation_cursor.qnt | 16 + 7 files changed, 871 insertions(+), 11 deletions(-) create mode 100644 cli/src/services/mutation_trace/mbt/driver.rs create mode 100644 cli/src/services/mutation_trace/mbt/mod.rs create mode 100644 cli/src/services/mutation_trace/mbt/model.rs create mode 100644 cli/src/services/mutation_trace/mbt/tests.rs 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..4d9db919 --- /dev/null +++ b/cli/src/services/mutation_trace/mbt/model.rs @@ -0,0 +1,467 @@ +//! 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. `spec/ +//! mutation_cursor.qnt`'s verification-only `mbtAction` variable is never +//! given a field here, so it is silently ignored by `serde`'s default +//! unknown-field handling when the whole top-level state record is +//! deserialized — that omission is what keeps `mbtAction` out of the +//! compared state. + +use std::collections::{BTreeMap, BTreeSet}; + +use serde::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)] +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")] +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")] +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")] +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")] +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")] +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. `mbtAction` has no field here +/// and is dropped by `serde`'s default unknown-field handling when +/// [`WireModelState`] deserializes the full top-level state record. +#[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, +} + +#[derive(Deserialize)] +#[serde(rename_all = "camelCase")] +struct WireModelState { + worktrees: BTreeMap, + scopes: BTreeMap, + worktree_trees: BTreeMap, + external_taint: BTreeSet, + processed_events: BTreeSet, + attempts: BTreeMap, + mutation_events: BTreeSet, +} + +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..363c736f --- /dev/null +++ b/cli/src/services/mutation_trace/mbt/tests.rs @@ -0,0 +1,22 @@ +//! Deterministic Quint Connect replays through the real `protocol.rs`. + +use quint_connect::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" +)] +fn mutation_cursor_transports_non_default_arguments() -> 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/plans/mutation-cursor-quint-connect.md b/context/plans/mutation-cursor-quint-connect.md index 7bccc8af..d77ccb32 100644 --- a/context/plans/mutation-cursor-quint-connect.md +++ b/context/plans/mutation-cursor-quint-connect.md @@ -12,9 +12,8 @@ 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, latest reviewed head -`ea23caf5`, plan-only, confirmed current via `git fetch`), correcting one -remaining MBT-transport issue found in review, on top of two earlier rounds of +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 @@ -337,12 +336,26 @@ Persist this field in every plan; this is durable plan state, not chat state: operation-identity-preserving fix wherever one exists; exact line numbers are re-checked at implementation time since T02/T03 edit this same file before T02's own guard refactor lands. -- PR #238 (branch `mutation-cursor`) is confirmed open, not merged, based on - `main`. PR #239 (branch `quint-connect`, latest reviewed head `ea23caf5`, - confirmed current via `git fetch`) stacks on PR #238's head (`2a097408`) - and at the time of this revision contains only this plan file — no - implementation has started, so this revision changes the plan only, per - the request's own "plan correction only" instruction. +- PR #238 (`mutation-cursor`) remains the semantic base for this stacked PR. + +- PR #239 (`quint-connect`) is now in active implementation. The durable task + state in this plan is the source of truth for implementation progress: + + - T01 complete: `quint-connect` dev-dependency and packaging synchronization. + - T02 complete: operation-preserving `MbtAction` instrumentation in Quint. + - T03 complete: `randomPrepare` remains a single top-level `step` branch; + no additional `PrepareKind` instrumentation was required. + - T04 complete: Quint Connect Rust driver, comparable model-state projection, + finite ID mapping, and the non-default + `WT1` / `Tree3` / `Attempt5` / `Flush(WT1)` transport smoke replay. + - T05 is the next pending task. + + 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 @@ -607,7 +620,7 @@ Persist this field in every plan; this is durable plan state, not chat state: resynchronize. - Context synchronization: synced -- [ ] T04: `Build the MBT driver, ID mapping, and comparable model state` (status:todo) +- [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}`; @@ -650,7 +663,103 @@ Persist this field in every plan; this is durable plan state, not chat state: 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`. - - Context synchronization: pending + - 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 - [ ] T05: `Wire deterministic scenario replays, guarded-no-op regressions, and the generated Quint Connect simulation` (status:todo) - Task ID: T05 diff --git a/spec/mutation_cursor.qnt b/spec/mutation_cursor.qnt index 0eb898a3..6bd36094 100644 --- a/spec/mutation_cursor.qnt +++ b/spec/mutation_cursor.qnt @@ -1773,4 +1773,20 @@ 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) } From 7272d421cb67da27b16dd8def80aedbf64b3f976 Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 09:46:41 +0200 Subject: [PATCH 6/9] tests: Add mutation cursor Quint Connect replays Exercise the remaining deterministic scenarios and guarded no-op regressions through the real Rust protocol, then compare generated Quint traces against the model across 500 samples. This expands MBT coverage without changing production protocol behavior. Plan: mutation-cursor-quint-connect, T05 Co-authored-by: SCE --- .github/workflows/quint.yml | 19 +- cli/src/services/mutation_trace/mbt/tests.rs | 118 ++++- context/cli/mutation-trace-quint-connect.md | 250 ++++++++++ context/context-map.md | 1 + .../plans/mutation-cursor-quint-connect.md | 458 ++++++++++++++---- flake.nix | 35 +- spec/mutation_cursor.qnt | 31 ++ 7 files changed, 806 insertions(+), 106 deletions(-) create mode 100644 context/cli/mutation-trace-quint-connect.md diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index d9639cb0..a0dc5a64 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/mbt/|^cli/src/services/mutation_trace/protocol\.rs$|^cli/src/services/mutation_trace/types\.rs$|^cli/Cargo\.toml$|^cli/Cargo\.lock$|^\.github/workflows/quint\.yml$|^\.github/workflows/quint-deep-verify\.yml$|^flake\.nix$|^flake\.lock$)'; then echo "quint=true" >> "$GITHUB_OUTPUT" else echo "quint=false" >> "$GITHUB_OUTPUT" @@ -55,7 +55,9 @@ jobs: needs: detect if: needs.detect.outputs.quint == 'true' runs-on: ubuntu-latest - timeout-minutes: 15 + # The Quint Connect Nix check compiles the CLI crate, so this needs more + # headroom than the pure-Quint steps alone required. + timeout-minutes: 30 steps: - name: Harden the runner (Audit all outbound calls) uses: step-security/harden-runner@05e31511f85b41b11d1cf0ef85d0992719546e2c # v2.21.0 @@ -78,7 +80,11 @@ jobs: run: nix run .#quint -- typecheck spec/mutation_cursor.qnt - name: Run Quint tests - run: nix run .#quint -- test spec/mutation_cursor.qnt + # `quint test` without `--match` silently selects zero tests (exit 0, + # no output) on this spec instead of running every named `run` + # scenario — matching every top-level `test...`-named `run` is the + # explicit selection that actually exercises them. + run: nix run .#quint -- test spec/mutation_cursor.qnt --match '^test.*' - name: Randomized Quint safety check run: > @@ -89,6 +95,13 @@ jobs: --max-samples=5000 --max-steps=20 + - name: Quint Connect model-based tests (Nix-pinned Rust + Quint) + # The entire MBT invocation goes through this Nix check rather than + # `cargo test` on the runner's own Cargo, so both the Rust toolchain + # and the Quint binary come from the repository's pinned flake + # inputs, never a second, unpinned Rust installation. + run: nix build .#checks.x86_64-linux.mutation-trace-quint-connect --print-build-logs + gate: name: Quint gate if: always() diff --git a/cli/src/services/mutation_trace/mbt/tests.rs b/cli/src/services/mutation_trace/mbt/tests.rs index 363c736f..8166df3f 100644 --- a/cli/src/services/mutation_trace/mbt/tests.rs +++ b/cli/src/services/mutation_trace/mbt/tests.rs @@ -1,6 +1,6 @@ //! Deterministic Quint Connect replays through the real `protocol.rs`. -use quint_connect::quint_test; +use quint_connect::{quint_run, quint_test}; use super::driver::MutationCursorDriver; @@ -20,3 +20,119 @@ use super::driver::MutationCursorDriver; fn mutation_cursor_transports_non_default_arguments() -> impl Driver { MutationCursorDriver::default() } + +/// Replays `testStartObservesBeforeActivation`: the freshness-boundary +/// semantics for a `Start` observation. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testStartObservesBeforeActivation" +)] +fn mutation_cursor_start_observes_before_activation() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testCloseObservesBeforeDeactivation`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testCloseObservesBeforeDeactivation" +)] +fn mutation_cursor_close_observes_before_deactivation() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testContendedIntervalsRemainAiContended`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testContendedIntervalsRemainAiContended" +)] +fn mutation_cursor_contended_intervals_remain_ai_contended() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testNoChangeHookReplayCannotStealFutureChange`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testNoChangeHookReplayCannotStealFutureChange" +)] +fn mutation_cursor_no_change_hook_replay_cannot_steal_future_change() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testConcurrentObservationsHaveOneWinner`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testConcurrentObservationsHaveOneWinner" +)] +fn mutation_cursor_concurrent_observations_have_one_winner() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testTaintInvalidatesPreparedObservation`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testTaintInvalidatesPreparedObservation" +)] +fn mutation_cursor_taint_invalidates_prepared_observation() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testRecoveryEstablishesBaseline`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testRecoveryEstablishesBaseline" +)] +fn mutation_cursor_recovery_establishes_baseline() -> impl Driver { + MutationCursorDriver::default() +} + +/// Replays `testClosedScopeCannotReactivate`. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testClosedScopeCannotReactivate" +)] +fn mutation_cursor_closed_scope_cannot_reactivate() -> impl Driver { + MutationCursorDriver::default() +} + +/// Guarded-no-op regression: replays +/// `testMbtGuardedPrepareInvokesRealPrepare` +/// (`init.then(prepare(Attempt0, Start(...))).then(prepare(Attempt0, +/// Advance(...)))`), where the second `prepare` guards because `Attempt0` is +/// no longer `Available`. A passing replay proves the driver still calls +/// `protocol::prepare` on the guarded step — dispatch is on the `MbtAction` +/// variant Quint recorded, never skipped because Quint's own state happened +/// not to change — and independently reaches the same no-op outcome. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testMbtGuardedPrepareInvokesRealPrepare" +)] +fn mutation_cursor_guarded_prepare_invokes_real_prepare() -> impl Driver { + MutationCursorDriver::default() +} + +/// Guarded-no-op regression: replays +/// `testMbtGuardedRecoverInvokesRealRecover` (`init.then(recover(WT0))`), +/// where `recover` guards because `WT0` is neither tainted, externally +/// tainted, nor needing rebaseline. A passing replay proves the driver still +/// calls `protocol::recover` on the guarded step and independently reaches +/// the same no-op outcome. +#[quint_test( + spec = "../spec/mutation_cursor.qnt", + test = "testMbtGuardedRecoverInvokesRealRecover" +)] +fn mutation_cursor_guarded_recover_invokes_real_recover() -> impl Driver { + MutationCursorDriver::default() +} + +/// Generated-trace refinement: replays Quint-generated randomized +/// traces through the real `protocol.rs`, comparing `ModelState` against +/// Quint's semantic state after every step. Reproducible with a fixed +/// `QUINT_SEED`. +#[quint_run( + spec = "../spec/mutation_cursor.qnt", + max_samples = 500, + max_steps = 30 +)] +fn mutation_cursor_generated_traces_refine_rust_protocol() -> impl Driver { + MutationCursorDriver::default() +} 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/plans/mutation-cursor-quint-connect.md b/context/plans/mutation-cursor-quint-connect.md index d77ccb32..7a4ec8ad 100644 --- a/context/plans/mutation-cursor-quint-connect.md +++ b/context/plans/mutation-cursor-quint-connect.md @@ -29,7 +29,7 @@ correction: 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 currently fall through to the shared `stutter` + 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 @@ -67,12 +67,12 @@ architecture-doc output, but that path is this plan's own file — see ## Acceptance criteria -- [ ] AC1: `quint-connect` is a dev/test-only dependency of the CLI crate; no +- [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. -- [ ] AC2: every action reachable from Quint's randomized `step` (`init`, +- [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 @@ -89,7 +89,7 @@ architecture-doc output, but that path is this plan's own file — see 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. -- [ ] AC3: both the generated `#[quint_run]` trace and the deterministic +- [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. @@ -98,7 +98,7 @@ architecture-doc output, but that path is this plan's own file — see 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. -- [ ] AC4: a Quint-generated random trace, replayed through the real +- [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`. @@ -106,7 +106,7 @@ architecture-doc output, but that path is this plan's own file — see (`#[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. -- [ ] AC5: the comparable state includes every Quint variable named in the +- [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 @@ -117,7 +117,7 @@ architecture-doc output, but that path is this plan's own file — see "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. -- [ ] AC6: at least the eight named deterministic Quint `run` scenarios +- [x] AC6: at least the eight named deterministic Quint `run` scenarios (`testStartObservesBeforeActivation`, `testCloseObservesBeforeDeactivation`, `testContendedIntervalsRemainAiContended`, `testNoChangeHookReplayCannotStealFutureChange`, @@ -128,7 +128,7 @@ architecture-doc output, but that path is this plan's own file — see 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. -- [ ] AC7: the `MbtAction` instrumentation and the `randomPrepare` +- [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 @@ -143,40 +143,58 @@ architecture-doc output, but that path is this plan's own file — see 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. -- [ ] AC8: CI runs the Quint Connect suite inside a Nix check that pins both +- [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. - - Validate: inspection of the new Nix check definition (`craneLib`-based, - reusing the repository `rustToolchain`, with the Nix `quint` package - available to the test run) and `.github/workflows/quint.yml` — the - change-detector regex additionally matches - `cli/src/services/mutation_trace/mbt/**`, `.../protocol.rs`, + 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 unchanged in behavior. -- [ ] AC9: no production DB/Git/filesystem/coordinator/hook code is + 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)]`. -- [ ] AC10: the existing ~75 handwritten `mutation_trace` protocol tests, +- [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`. -- [ ] AC11: every argument-carrying `MbtAction` variant uses a record payload +- [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. -- [ ] AC12: `MbtAction` identifies the invoked semantic operation and its +- [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 @@ -186,7 +204,7 @@ architecture-doc output, but that path is this plan's own file — see - 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. -- [ ] AC13: at least two deterministic MBT regressions prove that a guarded +- [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 @@ -195,7 +213,7 @@ architecture-doc output, but that path is this plan's own file — see 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. -- [ ] AC14: the `stutter` action itself, and every guarded action that used +- [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`" @@ -216,10 +234,14 @@ architecture-doc output, but that path is this plan's own file — see - `./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` +- `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..mutation-trace-quint-connect` (exact attribute name confirmed in T06) — the Nix-pinned Rust+Quint Quint Connect suite -- `nix flake check` if the new check is wired into normal flake checks +- `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 @@ -310,45 +332,50 @@ Persist this field in every plan; this is durable plan state, not chat state: `mutation_trace::mbt` with the Nix `quint` package added to its check inputs — rather than assembling a bespoke Rust+Quint environment from scratch. -- The exact `quint-connect` crate/package name, current compatible version, - and its custom action/nondet `Config` API for driver dispatch are resolved - in T01 against the upstream `quint-co/quint-connect` repository (README and - `connect/examples/two_phase_commit/mbt.rs`, plus any example closer to a - Choreo-style action-plus-arguments sum type) at implementation time, per - the request's own instruction not to assume `0.1.2` or the illustrative - `Driver`/`State`/`#[quint_run]`/`#[quint_test]`/`switch!`/`Config` - sketches are still current. This same research step confirms exactly how - Quint Connect's custom decoder distinguishes a unit variant from a record - variant, which is the mechanism AC11's record-payload rule depends on. -- Whether `randomPrepare`'s selected boundary needs a dedicated - `PrepareKind`-style nondet choice, or is already fully observable from the - `MbtPrepare { attempt, boundary }` variant `mbtAction` records regardless of - which `any { ... }` branch fired, is decided in T03 by testing the smallest - option first, per the request's own "prefer the smallest correct solution" - instruction. -- As of this revision, `prepare` (spec line 448-453), `taint` (~702-711), - `databaseFailure` (~732-737), `abandon` (~794-805), and `recover` - (~874-886) each guard their real transition and fall through to the shared - top-level `stutter` action on the guarded path; `commitAttempt` - (line 455+) computes its own `fresh`/`accepted`/`changed` logic rather than - delegating to `stutter`. T02 audits all six (not just the five that - currently call `stutter`) for a guarded/no-op path and applies the same - operation-identity-preserving fix wherever one exists; exact line numbers - are re-checked at implementation time since T02/T03 edit this same file - before T02's own guard refactor lands. +- 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`) is now in active implementation. The durable task +- 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` dev-dependency and packaging synchronization. - - T02 complete: operation-preserving `MbtAction` instrumentation in Quint. - - T03 complete: `randomPrepare` remains a single top-level `step` branch; - no additional `PrepareKind` instrumentation was required. - - T04 complete: Quint Connect Rust driver, comparable model-state projection, - finite ID mapping, and the non-default - `WT1` / `Tree3` / `Attempt5` / `Flush(WT1)` transport smoke replay. - - T05 is the next pending task. + - 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 @@ -761,7 +788,7 @@ Persist this field in every plan; this is durable plan state, not chat state: deferred to T06 by this plan's own scope, as T02/T03 already noted. - Context synchronization: synced -- [ ] T05: `Wire deterministic scenario replays, guarded-no-op regressions, and the generated Quint Connect simulation` (status:todo) +- [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`, @@ -798,25 +825,108 @@ Persist this field in every plan; this is durable plan state, not chat state: 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. - - Context synchronization: pending + - 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 -- [ ] T06: `Add a Nix-pinned Rust+Quint CI check and document the architecture` (status:todo) +- [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 (e.g. `mutation-trace-quint-connect`) + - 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`, 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; `.github/workflows/quint.yml` updated to invoke that 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); + 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 @@ -824,34 +934,180 @@ Persist this field in every plan; this is durable plan state, not chat state: 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, 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/test/ - randomized-safety steps beyond the detector's watched-path list. + 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: the new Nix check runs the MBT suite under repository-pinned - Rust and Quint, printing their versions at least while stabilizing; - `.github/workflows/quint.yml` invokes it without installing a separate - Rust toolchain for this job; 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..mutation-trace-quint-connect` (or - `nix flake check` if wired into normal checks) run locally; manual diff - review of `.github/workflows/quint.yml`; `cat - context/cli/mutation-trace-quint-connect.md`; the plan's full `Full - validation` command list run end-to-end. - - Context synchronization: pending + - 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. The genuine ambiguities found while planning — the requested -architecture-doc path colliding with this plan's own file, the exact -`quint-connect` version/custom-action API, and whether `commitAttempt` has a -guarded no-op path analogous to the other five actions — resolve cleanly by -repository convention and by deferring live verification to T01/T02, both -recorded under Assumptions rather than blocking authoring, since none of them -changes scope or acceptance criteria. Whether `randomPrepare`'s boundary -needs a dedicated `PrepareKind` beyond `mbtAction` is an implementation-time -decision scoped explicitly into T03's Done-when criteria, not a -planning-time unknown. +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/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/spec/mutation_cursor.qnt b/spec/mutation_cursor.qnt index 6bd36094..1c4742fd 100644 --- a/spec/mutation_cursor.qnt +++ b/spec/mutation_cursor.qnt @@ -1789,4 +1789,35 @@ module mutation_cursor { .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) } From de37f57189fce99d607633c147c3480c399ce2d5 Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 11:08:30 +0200 Subject: [PATCH 7/9] mutation-trace+CI: Harden Quint MBT coverage and state decoding Ensure Rust refinement tests replay every named Quint scenario while limiting deterministic samples to one, and make wire-state deserialization reject unclassified Quint fields. Update the workflow path filter so all mutation-trace changes trigger Quint checks. This prevents verification-only state from being silently ignored and keeps new mutation-trace changes covered by CI. Co-authored-by: SCE --- .github/workflows/quint.yml | 2 +- cli/src/services/mutation_trace/mbt/model.rs | 60 ++++++++++++++------ cli/src/services/mutation_trace/mbt/tests.rs | 51 +++++++++++++---- 3 files changed, 85 insertions(+), 28 deletions(-) diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index a0dc5a64..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$|^cli/src/services/mutation_trace/mbt/|^cli/src/services/mutation_trace/protocol\.rs$|^cli/src/services/mutation_trace/types\.rs$|^cli/Cargo\.toml$|^cli/Cargo\.lock$|^\.github/workflows/quint\.yml$|^\.github/workflows/quint-deep-verify\.yml$|^flake\.nix$|^flake\.lock$)'; then + 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" diff --git a/cli/src/services/mutation_trace/mbt/model.rs b/cli/src/services/mutation_trace/mbt/model.rs index 4d9db919..1d145e75 100644 --- a/cli/src/services/mutation_trace/mbt/model.rs +++ b/cli/src/services/mutation_trace/mbt/model.rs @@ -7,16 +7,21 @@ //! 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. `spec/ -//! mutation_cursor.qnt`'s verification-only `mbtAction` variable is never -//! given a field here, so it is silently ignored by `serde`'s default -//! unknown-field handling when the whole top-level state record is -//! deserialized — that omission is what keeps `mbtAction` out of the -//! compared state. +//! 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::Deserialize; +use serde::{de::IgnoredAny, Deserialize}; use super::super::types::{ ActorKind, AttemptId, AttemptState, AttemptStatus, Attribution, Boundary, EventId, EventKey, @@ -240,6 +245,7 @@ impl From for AttemptStatus { // --------------------------------------------------------------------- #[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] +#[serde(deny_unknown_fields)] pub(super) struct WireScopeEvent { pub scope: WireScopeId, pub event: WireEventId, @@ -295,7 +301,7 @@ impl From for Attribution { } #[derive(Clone, Debug, Eq, PartialEq, Deserialize)] -#[serde(rename_all = "camelCase")] +#[serde(rename_all = "camelCase", deny_unknown_fields)] pub(super) struct WireWorktreeState { pub cursor_tree: WireTreeId, pub revision: u64, @@ -317,7 +323,7 @@ impl From for WorktreeState { } #[derive(Clone, Debug, Eq, PartialEq, Deserialize)] -#[serde(rename_all = "camelCase")] +#[serde(rename_all = "camelCase", deny_unknown_fields)] pub(super) struct WireScopeState { pub status: WireScopeStatus, pub actor_kind: WireActorKind, @@ -335,7 +341,7 @@ impl From for ScopeState { } #[derive(Clone, Debug, Eq, PartialEq, Deserialize)] -#[serde(rename_all = "camelCase")] +#[serde(rename_all = "camelCase", deny_unknown_fields)] pub(super) struct WireAttemptState { pub status: WireAttemptStatus, pub boundary: WireBoundary, @@ -357,7 +363,7 @@ impl From for AttemptState { } #[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] -#[serde(rename_all = "camelCase")] +#[serde(rename_all = "camelCase", deny_unknown_fields)] pub(super) struct WireEventKey { pub scope_id: WireScopeId, pub event_id: WireEventId, @@ -373,7 +379,7 @@ impl From for EventKey { } #[derive(Clone, Debug, Eq, Ord, PartialEq, PartialOrd, Deserialize)] -#[serde(rename_all = "camelCase")] +#[serde(rename_all = "camelCase", deny_unknown_fields)] pub(super) struct WireMutationEvent { pub worktree_id: WireWorktreeId, pub revision: u64, @@ -409,9 +415,10 @@ impl From for MutationEvent { /// 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. `mbtAction` has no field here -/// and is dropped by `serde`'s default unknown-field handling when -/// [`WireModelState`] deserializes the full top-level state record. +/// 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 { @@ -424,9 +431,16 @@ pub struct ModelState { 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")] +#[serde(rename_all = "camelCase", deny_unknown_fields)] struct WireModelState { + // Semantic state: compared against Rust via `ModelState`. worktrees: BTreeMap, scopes: BTreeMap, worktree_trees: BTreeMap, @@ -434,6 +448,20 @@ struct WireModelState { 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 { diff --git a/cli/src/services/mutation_trace/mbt/tests.rs b/cli/src/services/mutation_trace/mbt/tests.rs index 8166df3f..0543231a 100644 --- a/cli/src/services/mutation_trace/mbt/tests.rs +++ b/cli/src/services/mutation_trace/mbt/tests.rs @@ -15,7 +15,8 @@ use super::driver::MutationCursorDriver; /// them. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testMbtDriverTransportsNonDefaultArguments" + test = "testMbtDriverTransportsNonDefaultArguments", + max_samples = 1 )] fn mutation_cursor_transports_non_default_arguments() -> impl Driver { MutationCursorDriver::default() @@ -25,7 +26,8 @@ fn mutation_cursor_transports_non_default_arguments() -> impl Driver { /// semantics for a `Start` observation. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testStartObservesBeforeActivation" + test = "testStartObservesBeforeActivation", + max_samples = 1 )] fn mutation_cursor_start_observes_before_activation() -> impl Driver { MutationCursorDriver::default() @@ -34,7 +36,8 @@ fn mutation_cursor_start_observes_before_activation() -> impl Driver { /// Replays `testCloseObservesBeforeDeactivation`. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testCloseObservesBeforeDeactivation" + test = "testCloseObservesBeforeDeactivation", + max_samples = 1 )] fn mutation_cursor_close_observes_before_deactivation() -> impl Driver { MutationCursorDriver::default() @@ -43,7 +46,8 @@ fn mutation_cursor_close_observes_before_deactivation() -> impl Driver { /// Replays `testContendedIntervalsRemainAiContended`. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testContendedIntervalsRemainAiContended" + test = "testContendedIntervalsRemainAiContended", + max_samples = 1 )] fn mutation_cursor_contended_intervals_remain_ai_contended() -> impl Driver { MutationCursorDriver::default() @@ -52,7 +56,8 @@ fn mutation_cursor_contended_intervals_remain_ai_contended() -> impl Driver { /// Replays `testNoChangeHookReplayCannotStealFutureChange`. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testNoChangeHookReplayCannotStealFutureChange" + test = "testNoChangeHookReplayCannotStealFutureChange", + max_samples = 1 )] fn mutation_cursor_no_change_hook_replay_cannot_steal_future_change() -> impl Driver { MutationCursorDriver::default() @@ -61,7 +66,8 @@ fn mutation_cursor_no_change_hook_replay_cannot_steal_future_change() -> impl Dr /// Replays `testConcurrentObservationsHaveOneWinner`. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testConcurrentObservationsHaveOneWinner" + test = "testConcurrentObservationsHaveOneWinner", + max_samples = 1 )] fn mutation_cursor_concurrent_observations_have_one_winner() -> impl Driver { MutationCursorDriver::default() @@ -70,7 +76,8 @@ fn mutation_cursor_concurrent_observations_have_one_winner() -> impl Driver { /// Replays `testTaintInvalidatesPreparedObservation`. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testTaintInvalidatesPreparedObservation" + test = "testTaintInvalidatesPreparedObservation", + max_samples = 1 )] fn mutation_cursor_taint_invalidates_prepared_observation() -> impl Driver { MutationCursorDriver::default() @@ -79,7 +86,8 @@ fn mutation_cursor_taint_invalidates_prepared_observation() -> impl Driver { /// Replays `testRecoveryEstablishesBaseline`. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testRecoveryEstablishesBaseline" + test = "testRecoveryEstablishesBaseline", + max_samples = 1 )] fn mutation_cursor_recovery_establishes_baseline() -> impl Driver { MutationCursorDriver::default() @@ -88,7 +96,8 @@ fn mutation_cursor_recovery_establishes_baseline() -> impl Driver { /// Replays `testClosedScopeCannotReactivate`. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testClosedScopeCannotReactivate" + test = "testClosedScopeCannotReactivate", + max_samples = 1 )] fn mutation_cursor_closed_scope_cannot_reactivate() -> impl Driver { MutationCursorDriver::default() @@ -104,7 +113,8 @@ fn mutation_cursor_closed_scope_cannot_reactivate() -> impl Driver { /// not to change — and independently reaches the same no-op outcome. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testMbtGuardedPrepareInvokesRealPrepare" + test = "testMbtGuardedPrepareInvokesRealPrepare", + max_samples = 1 )] fn mutation_cursor_guarded_prepare_invokes_real_prepare() -> impl Driver { MutationCursorDriver::default() @@ -118,7 +128,8 @@ fn mutation_cursor_guarded_prepare_invokes_real_prepare() -> impl Driver { /// the same no-op outcome. #[quint_test( spec = "../spec/mutation_cursor.qnt", - test = "testMbtGuardedRecoverInvokesRealRecover" + test = "testMbtGuardedRecoverInvokesRealRecover", + max_samples = 1 )] fn mutation_cursor_guarded_recover_invokes_real_recover() -> impl Driver { MutationCursorDriver::default() @@ -136,3 +147,21 @@ fn mutation_cursor_guarded_recover_invokes_real_recover() -> impl Driver { 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() +} From 33368af2d5812a0171b8467090f256c707be07e6 Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 11:55:18 +0200 Subject: [PATCH 8/9] CI: Allow Nix builds to fall back to alternate stores Keep pull-request checks working when the preferred binary cache is unavailable. Pass Nix's fallback option to flake checks and package builds so CI can build dependencies locally instead of failing on cache access. Co-authored-by: SCE --- .github/workflows/pr-ci.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 From 66e519952169cab00cbb4708e1886f140a067c07 Mon Sep 17 00:00:00 2001 From: David Abram Date: Thu, 27 Aug 2026 12:17:42 +0200 Subject: [PATCH 9/9] tests: Reformat mutation trace test attribute Keep the Quint test macro invocation in rustfmt's canonical single-line format. --- cli/src/services/mutation_trace/mbt/tests.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/cli/src/services/mutation_trace/mbt/tests.rs b/cli/src/services/mutation_trace/mbt/tests.rs index 0543231a..a5b52106 100644 --- a/cli/src/services/mutation_trace/mbt/tests.rs +++ b/cli/src/services/mutation_trace/mbt/tests.rs @@ -157,11 +157,7 @@ fn mutation_cursor_generated_traces_refine_rust_protocol() -> impl Driver { /// 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 -)] +#[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() }