dongarandClaude Opus 5.5
266b5dbbd7
CI / checks (push) Skipped
test_loop_properties.py walks the new loop with a seeded mix of operator and Gitea actions (go-aheads, stale go-aheads, answers, comments, merges, the comment-then-merge race, closes, abandon, a crash and restart) and an adaptive scripted model, checking every loop.qnt property after every step. It found two bugs, both fixed with regression tests: abandoning an item left its open PR open (the model's fix 1, now in code), and after a review fix became a follow-up PR, the next fix went to the merged branch. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
78 lines
3.4 KiB
Markdown
78 lines
3.4 KiB
Markdown
# Formal models
|
|
|
|
[Quint](https://quint-lang.org) models of designs where interleavings matter
|
|
more than any single code path. A model is a hand-written reading of the code:
|
|
it finds flaws the design and the code share, not places where the code
|
|
strays from the design. So every counterexample is also reproduced as a failing
|
|
test against the real code before anything is changed.
|
|
|
|
## `orchestrator.qnt`: nisse-dev's control loop
|
|
|
|
Models `nisse-dev/src/nisse_dev/control.py`: the states, the gate, pending
|
|
questions, Gitea comment cursors, publish intents, and the worker queue.
|
|
Operator messages, Gitea comments, planner/executor/publisher outcomes
|
|
(exceptions included) and **a crash at any point** all interleave freely.
|
|
Each pure function is named after the method it mirrors.
|
|
|
|
The properties are at the end of the file (`all_properties` is their
|
|
conjunction). Counterexamples are written out as short traces in
|
|
`orchestrator_scenarios.qnt`, and replayed against the real code in
|
|
`nisse-dev/tests/test_quint_counterexamples.py`.
|
|
|
|
```sh
|
|
npm install -g @informalsystems/quint # 0.33 or later
|
|
|
|
# Random simulation, one property at a time:
|
|
quint run specs/orchestrator.qnt --invariant=no_stranding \
|
|
--max-steps=40 --max-samples=200000
|
|
|
|
# The counterexample traces (each expects its property to break):
|
|
quint test specs/orchestrator_scenarios.qnt
|
|
```
|
|
|
|
Exhaustive bounded checking (`quint verify`) uses Apalache and needs Java 17.
|
|
|
|
**Keeping it true.** When `control.py` changes how a state is entered or
|
|
left, change the matching function here in the same PR. When a
|
|
counterexample's fix lands, flip its scenario's `expect` to the property
|
|
holding, and drop the `xfail` from its Python reproduction.
|
|
|
|
## `loop.qnt`: the agent loop, as the architecture describes it
|
|
|
|
Models the design in `docs/Architecture.md` rather than code, since the new
|
|
loop doesn't exist yet:
|
|
- work items from assigned issues and conversations;
|
|
- restatements and revision-bound go-aheads;
|
|
- park-and-switch, with branches pushed on parking;
|
|
- blocked dependencies;
|
|
- harness-owned milestones and waiting for merges;
|
|
- review follow-ups;
|
|
- record issues;
|
|
- crashes and build VM wipes at any point.
|
|
|
|
A counterexample here is a gap in the architecture, so it is fixed there,
|
|
and the model carries the fix (marked `FIX n`). `loop_scenarios.qnt` keeps each
|
|
counterexample as a trace of the fixed behaviour. Each trace fails if its fix
|
|
is reverted, and each property that never failed was checked against a
|
|
deliberately broken model.
|
|
|
|
```sh
|
|
quint run specs/loop.qnt --invariant=all_properties --max-steps=80 --max-samples=200000
|
|
quint test specs/loop_scenarios.qnt
|
|
```
|
|
|
|
Traces need about 80 steps to reach second milestones. The `w_*` values at the
|
|
end are reachability witnesses: each should be *violated*, which shows the
|
|
state it names is reachable.
|
|
|
|
**Against the real code.** `nisse-dev/tests/test_loop_properties.py` checks
|
|
the same properties against the new loop itself: a seeded random walk over
|
|
what the operator and Gitea can do (go-aheads, answers, comments, merges,
|
|
closes, abandon, a crash and restart), checking every property after every
|
|
step. It found two bugs the design model couldn't, because they were in the
|
|
code: abandon left an open PR, and a review fix after a follow-up PR went to
|
|
the merged branch. Each also has its own regression test.
|
|
|
|
**Keeping it true.** When the architecture changes a rule this models, change
|
|
the model and the walk in the same PR.
|