dongarandClaude Opus 5.5
97863c1939
Fixes counterexamples 1-4 from specs/orchestrator.qnt: a repeated 'approve', 'approve rev-1' meant for the architecture, approving on both channels, and 'approve' plus an afterthought all landed on the next plan, one the operator had not seen. - Revisions are numbered across the work item (A4 already required monotonic tags; the code numbered per gate), so rev-N names one plan. - Each reply is stamped on arrival with the revision that was up: in Matrix the one whose approval request had been sent (a plain value the transport thread reads, restored on boot), in Gitea the latest plan comment older than the reply (board.posts). - Gate.evaluate applies a reply that names no revision only if its stamp is the current revision. Otherwise an approval is not applied and feedback rejects nothing (it is still in the transcript), and the agent says which revision is up. 'approve rev-N' binds by its number. - Spec A4 states both rules. The model applies them; scenarios 1-4 now expect the properties to hold, and both held over 200,000 random traces and Apalache's exhaustive check to depth 8. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PPQ14L3LikyefCMFBqEbKE
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.
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.
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.