Add Quint Connect - #239
Open
davidabram wants to merge 9 commits into
Open
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
davidabram
force-pushed
the
quint-connect
branch
from
August 26, 2026 22:36
9aa80a7 to
ea23caf
Compare
davidabram
force-pushed
the
quint-connect
branch
from
August 26, 2026 22:46
ea23caf to
1961ab7
Compare
davidabram
force-pushed
the
quint-connect
branch
from
August 26, 2026 23:07
1c7dfdf to
09574f9
Compare
davidabram
force-pushed
the
quint-connect
branch
from
August 27, 2026 07:32
9c84263 to
8e89094
Compare
davidabram
force-pushed
the
quint-connect
branch
from
August 27, 2026 08:23
8915cb4 to
dabe94a
Compare
davidabram
force-pushed
the
quint-connect
branch
from
August 27, 2026 08:24
dabe94a to
5677884
Compare
davidabram
force-pushed
the
quint-connect
branch
from
August 27, 2026 08:31
5677884 to
2e612b8
Compare
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 <sce@crocoder.dev>
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 <sce@crocoder.dev>
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 <sce@crocoder.dev>
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 <sce@crocoder.dev>
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 <sce@crocoder.dev>
davidabram
force-pushed
the
quint-connect
branch
from
August 27, 2026 08:36
2e612b8 to
b390415
Compare
Exercise the remaining deterministic scenarios and guarded no-op regressions through the real Rust protocol, then compare generated Quint traces against the model across 500 samples. This expands MBT coverage without changing production protocol behavior. Plan: mutation-cursor-quint-connect, T05 Co-authored-by: SCE <sce@crocoder.dev>
davidabram
force-pushed
the
quint-connect
branch
from
August 27, 2026 08:46
b390415 to
7272d42
Compare
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 <sce@crocoder.dev>
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 <sce@crocoder.dev>
Keep the Quint test macro invocation in rustfmt's canonical single-line format.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.