nisse/specs/README.md

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.

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.

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.