dongarandClaude Opus 5.5
6ae2375194
nisse-dev now runs only the conversational loop. The gated state machine it was built alongside is gone: - Removed control.py, planner.py, executor.py, approvals.py, gates.py (command_form moves to loop/reader.py), publish.py and poller.py, the old assembly in agent.py (its shared helpers move to loop/build.py), the store's state-machine view (get_state, transition), their tests, the old end-to-end and live planning/milestone/gate tests, and specs/orchestrator.qnt with its scenarios. - Roles are driver, helper, expert and classifier; driver is required. loop:, roles.planner, roles.executor and tuning.executor are refused with what to use instead; tuning.driver takes the turn cap and failure limit. - The benchmark and the capability matrix measure the driver: the loop's own system prompt and tools, the task's plan as the agreed restatement. Task plans end with finish_milestone, so earlier runs show as (old); stored runs' executor tuning reads as the driver's. - A delegation on the loop records what its helper's alias resolved to (L9), as the old path's did. - The dump shows a work item's revision and what it waits for. - Behaviour the old tests covered and the loop shares stays covered: driver runs that fail on a model call, stop mid-turn, reset the failure count; go-aheads ignoring case and punctuation; a request too big to fit is never sent; the assembly tests, now on build_loop_agent. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
56 lines
2.4 KiB
Markdown
56 lines
2.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.
|
|
|
|
```sh
|
|
npm install -g @informalsystems/quint # 0.33 or later
|
|
```
|
|
|
|
Exhaustive bounded checking (`quint verify`) uses Apalache and needs Java 17.
|
|
|
|
The gated state machine the agent ran before the switch-over (M2.8) had its
|
|
own model, `orchestrator.qnt`; it went with that code, and is in the history.
|
|
|
|
## `loop.qnt`: the agent loop, as the architecture describes it
|
|
|
|
Models the design in `docs/Architecture.md` rather than the code (it was
|
|
written before the loop was):
|
|
- 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 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.
|