pass on quint-related skills#9
Open
angbrav wants to merge 6 commits into
Open
Conversation
beu5a
approved these changes
Jun 23, 2026
|
|
||
| - [1. No String Manipulation](#1-no-string-manipulation) | ||
| - [2. No Nested Pattern Matching](#2-no-nested-pattern-matching) | ||
| - [3. No Destructuring](#3-no-destructuring) |
Contributor
There was a problem hiding this comment.
In the latest versions of Quint we do support tuple destructuring: https://github.com/quint-co/quint/releases/tag/v0.30.0
New quint-modeling skill: generates a Quint spec from any of four starting
points, with a shared "modelling spine" (steps 1–7) all flows converge on and
a router that dispatches to the right intake guideline.
quint-modeling/SKILL.md — router + shared spine:
- separate concerns; system-model assumptions checklist
- state shaping: single grouped State var, extended to NodeId -> LocalState
for N actors; when-to-use-Choreo decision
- pure-functions-first, thin actions, witnesses-then-invariants, step + simulate
- handoff step (covers / does-not-cover / ground-truth)
- defers all syntax to the quint-lang reference
quint-modeling/guidelines/ — per-flow intake only, deferring the spine:
- from-nothing.md interactive interview (from spec-builder)
- from-requirements.md extract from a written doc
- from-code.md research + code intake + source->Quint mapping
- from-tlaplus.md fidelity, EXTENDS, CHOOSE, sentinels, Choreo, NameAnalysis
quint-lang reference corrections:
- constraints.md: destructuring is supported in val/let bindings (tuple and
record) and lambda params, not in def params or match arms — was wrongly
documented as "No Destructuring"
- SKILL.md: assume is not enforced by typecheck/run/verify; use a run test to
check a constant constraint
- patterns.md: add reserved-keyword-as-identifier/field-name rule; .with() is
valid-but-non-idiomatic, not an error
All Quint examples typechecked/run against the CLI (v0.32.0). Known bugs from the
source skills fixed on the way in: inline { tag: } sum-type variants -> named
constructors; no chooseSome (unsupported at runtime); .with() not treated as an
error; require kept as a basicSpells operator, not core Quint.
Reduce the suite from 6 skills to 3 (quint-modeling, quint-lang,
quint-execute-spec): fold spec review into quint-modeling as a guideline,
drop quint-verification-framing (language discipline now in simulations.md,
property-scoring in from-requirements) and quint-spec-explainer.
quint-modeling:
- Replace the {success,newState}+unchanged_all action pattern with guarded
actions (split can*/apply* pure defs; guard lifted into the action so it is
disabled when false); resolves the Step 4/Step 6 contradiction.
- Lead witnesses with `quint run --witnesses` (positive predicate, trace
count); demote not(target)-as-invariant to the trace-fetching fallback.
- Correct deadlock guidance: quint verify reports deadlocks, quint run does not.
- Add scope/granularity/abstraction decisions before modeling (from-code,
from-requirements); add boundedness note and Step 1 temporal layer.
- Soften NodeId->LocalState to a judgement call; self-review checklist; misc.
quint-lang:
- Fix Map[K,V] type syntax -> K -> V (QNT015).
- Align patterns.md to guarded actions; remove lastActionSuccess (not a
built-in; redundant under guarded actions).
- Rewrite quint test debugging: it shows no state on failure at any verbosity;
document REPL replay (--backend=typescript for piped stdin), .seed for
determinism, and --out-itf; document the test-name-ends-in-Test gotcha.
- Add --max-samples/--max-steps guidance: never below 10k to confirm a
property; size --max-steps by branching factor (actions x nondet fan-out).
- Narrow quint-lang to defer model-building/translation to quint-modeling.
Ignore _apalache-out/ (quint verify scratch output).
All Quint snippets and CLI claims verified against quint 0.32.0.
Collaborator
|
We can change the base of this to main and merge it directly to main. |
Add two verified .qnt reference examples to quint-modeling/examples/, each the canonical illustration of one way components coordinate: - ewd426.qnt: shared-memory coordination (grouped-map state, temporal liveness) - tendermint/: Choreo / real BFT consensus, split into spec + tendermintTest.qnt per the test-separation guideline, with a name-anchored "quick read" path to keep per-read token cost low Both verified clean on Quint 0.32.0; README.md documents the maintenance contract. Refine the modeling guidance: - Make Choreo the strong default for distributed message-passing protocols; verbosity on small specs is the one justified exception, gated through user sign-off. - Reframe actors and communication as the two early shaping questions that drive state shape, message medium, and the Choreo decision (Step 1 + Step 2 bridge). - Restrict quint verify to explicit user model-checking requests; the build, iterate, and review loops use quint run only. - Trim the Result-record note to an inline caveat in from-code; make scope confirmation conditional on ambiguity; drop the quint-specs/ prefix from the handoff example. Harvest reusable techniques into quint-lang guidelines: --mbt for trace analysis, conditional .expect() for nondet tests, and .expect() variable scoping.
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
3 participants
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.
Main skills:
Secondary, pre-existing ones:
Superseeded, ie, removed: