dongarandClaude Opus 5.5
c794a1e52b
The driver can request_reimage(reason) when its build VM is broken past the usual fixes (before the go-ahead too: it asks, it doesn't act). The harness parks the work in progress (pushed to Gitea), then blocks the VM in the state store (schema 5, vm_blocks): no item on any project on it is taken up, across restarts. The operator hears once at top level, with the command to clear it, and each blocked item's thread gets a line. `vm ready <project>` lifts the block and trusts the VM's new host key; a reimaged VM is set up again by the toolchain step, and the item that found it goes first. loop.qnt gains the block (blocked_vm_runs_nothing) and a scenario; it found that a reimage lost work in progress, hence parking first. The walk requests reimages and recovers them, reimaged or not. The unreachable case reuses the block in #137. Architecture P5 is softer, and D3 describes the block. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J5Utyfzw7gF7UhjRDEtjTk
Formal models
Quint 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.
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.
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.