Check loop.qnt's properties against the real loop (M2.1, PR D part 1)

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

nisse-dev/src/nisse_dev/loop/agent.py

@@ -561,8 +561,13 @@ class LoopAgent:
                     f"PR #{loop.pr}: {fixed.note}",
                 )
             elif fixed.kind == "new-pr" and fixed.pr is not None:
+                # Later fixes go to the new PR's branch, never the merged one.
                 loop = replace(
-                    loop, pr=fixed.pr.number, pr_url=fixed.pr.url, fixes=loop.fixes + 1
+                    loop,
+                    pr=fixed.pr.number,
+                    pr_url=fixed.pr.url,
+                    branch=fixed.branch,
+                    fixes=loop.fixes + 1,
                 )
                 self._wait(
                     item,
@@ -636,6 +641,15 @@ class LoopAgent:
 
     def _close(self, item: WorkItem, loop: Loop, outcome: str, note: str) -> None:
         self._fact(item, f"work item {outcome}: {note}")
+        if loop.pr and outcome == "abandoned":
+            # L2: abandoning closes the item's open PR with a note.
+            try:
+                self._gitea.post_comment(self._repo, loop.pr, f"abandoned: {note}")
+                self._gitea.close_pull_request(self._repo, loop.pr)
+            except GiteaError as exc:
+                self._transport.post(
+                    f"could not close PR #{loop.pr}: {exc}", thread=loop.thread
+                )
         save(self._store, item.id, CLOSED, loop, cause=outcome)
         self._store.close_work_item(item.id, outcome=outcome, cause=note)
         if loop.issue:

nisse-dev/src/nisse_dev/loop/milestones.py

@@ -32,6 +32,7 @@ class Fixed:
     kind: Literal["pushed", "nothing", "new-pr", "closed", "failed"]
     note: str
     pr: PullRequest | None = None
+    branch: str = ""  # a new PR's branch, which later fixes go to
 
 
 class Milestones:
@@ -177,7 +178,7 @@ class Milestones:
                     summary=f"PR #{pr} merged before this review fix landed.",
                     issue=0,
                 )
-                return Fixed("new-pr", new.note, new.pr)
+                return Fixed("new-pr", new.note, new.pr, follow)
             if state.state != "open":
                 return Fixed("closed", f"PR #{pr} was closed", state)
             return Fixed("pushed", f"pushed {sha[:8]}", state)

nisse-dev/tests/test_loop_milestones.py

@@ -96,6 +96,9 @@ class Forge:
     def close_issue(self, repo: str, index: int) -> None:
         self.closed_issues.append(index)
 
+    def close_pull_request(self, repo: str, index: int) -> None:
+        self.prs[index]["state"] = "closed"
+
     # what the operator does in Gitea
     def merge(self, n: int) -> None:
         head = self.prs[n]["head"]
@@ -429,3 +432,45 @@ def test_boot_asks_when_a_publish_never_reached_gitea(world: dict[str, Any]) ->
     assert store.pending_intents() == []
     assert loop_of(item(world)).wait == ANSWER
     assert "publishing was cut off by a restart" in transport.outbound[-1].text
+
+
+def test_a_fix_after_a_follow_up_pr_goes_to_the_follow_up(
+    world: dict[str, Any],
+) -> None:
+    # Found by the property walk (seed 7): after a fix became a follow-up PR,
+    # the next fix was pushed to the original, merged branch and lost.
+    forge: Forge = world["forge"]
+    model = ScriptedModel(
+        RESTATE,
+        WORK + FINISH,
+        [call("write_file", path="fix1.py", content="a = 1\n"), *FINISH],
+        [call("write_file", path="fix2.py", content="b = 2\n"), *FINISH],
+    )
+    agent, transport = loop_agent(world, model)
+    agent.intake()
+    say(transport, world, "go")
+    [first] = forge.prs
+    forge.comments[first] = [Comment(1, "don", "add fix1", "t")]
+    agent.watch()
+    forge.merge(first)  # merged before the fix lands: a follow-up PR
+    agent._schedule()
+    follow = loop_of(item(world)).pr
+    assert follow != first
+    forge.comments[follow] = [Comment(2, "don", "add fix2", "t")]
+    agent.watch()
+    agent._schedule()
+    assert len(forge.prs) == 2  # pushed to the follow-up, not a third PR
+    assert "fix2.py" in forge.files(follow)
+
+
+def test_abandoning_an_item_closes_its_open_pr(world: dict[str, Any]) -> None:
+    # Found by the property walk (seed 4); the model's fix 1 (L2).
+    forge: Forge = world["forge"]
+    agent, transport = loop_agent(world, ScriptedModel(RESTATE, WORK + FINISH))
+    agent.intake()
+    say(transport, world, "go")
+    [pr] = forge.prs
+    say(transport, world, "abandon")
+    assert item(world).outcome == "abandoned"
+    assert forge.prs[pr]["state"] == "closed"
+    assert (pr, "abandoned: abandoned by @don:test") in forge.posted

nisse-dev/tests/test_loop_properties.py

@@ -0,0 +1,247 @@
+"""specs/loop.qnt's properties, checked against the real loop (M2.1, PR D).
+
+The Quint model checks the design; this checks the code. A seeded random
+walk interleaves what the operator and Gitea can do (go-aheads, answers,
+comments, merges, closes, abandon, a crash and restart) with an adaptive
+scripted model, and checks every property after every step. A failure prints
+the seed and the steps, so it replays exactly.
+"""
+
+import random
+import subprocess
+from pathlib import Path
+from typing import Any
+
+import pytest
+from test_loop_milestones import DON, Forge, call
+from test_loop_milestones import world as world  # noqa: PLC0414 -- the fixture
+
+from nisse_dev.cancel import Cancel
+from nisse_dev.canonical import Fact, ToolCall
+from nisse_dev.gitea import Comment
+from nisse_dev.loop.agent import LoopAgent
+from nisse_dev.loop.driver import Driver
+from nisse_dev.loop.items import ANSWER, GO_AHEAD, MERGE, WAITING, loop_of
+from nisse_dev.oplog import OpLog
+from nisse_dev.tools import Workspace
+from nisse_dev.transport import InboundMessage, InMemoryTransport
+from nisse_dev.worker import InlineWorker
+
+SEEDS = range(32)
+STEPS = 20
+
+
+class PolicyModel:
+    """Plays a plausible driver: restate first, then a milestone, fixes
+    after comments, close after a merge; sometimes asks a question or
+    replies in prose. Seeded, so a walk replays exactly."""
+
+    def __init__(self, rng: random.Random) -> None:
+        self.rng = rng
+        self.n = 0
+
+    def complete(self, events, tools, model, system=None) -> list[Any]:
+        self.n += 1
+        offered = {t["function"]["name"] for t in tools}
+        facts = [getattr(e.event, "text", "") for e in events]
+        roll = self.rng.random()
+        if roll < 0.08:
+            return [call("ask_human", question=f"question {self.n}?")]
+        if roll < 0.12:
+            return [ToolCall(call_id=f"p{self.n}", tool="nonsense", arguments={})]
+        if "finish_milestone" not in offered:
+            return [call("restate", text=f"restatement {self.n}")]
+        merged = any("merged" in t for t in facts[-6:])
+        if merged and self.rng.random() < 0.8:
+            return [call("close_item", summary=f"done {self.n}")]
+        return [
+            call("start_milestone", name=f"m{self.n}"),
+            call("write_file", path=f"f{self.n}.py", content=f"x = {self.n}\n"),
+            call("finish_milestone", summary=f"work {self.n}"),
+        ]
+
+
+class Walk:
+    def __init__(self, world: dict[str, Any], seed: int) -> None:
+        self.world = world
+        self.rng = random.Random(seed)
+        self.seed = seed
+        self.steps: list[str] = []
+        self.shown_at_go: list[int] = []  # the revision on screen at each go
+        self.agent, self.transport = self._agent()
+
+    def _agent(self) -> tuple[LoopAgent, InMemoryTransport]:
+        transport = InMemoryTransport()
+        cancel = Cancel()
+        w = self.world
+        agent = LoopAgent(
+            w["store"],
+            transport,
+            w["forge"],
+            repo="don/sandbox",
+            project="sandbox",
+            account="nisse-dev",
+            operators={DON},
+            gitea_operators={"don"},
+            driver=Driver(PolicyModel(self.rng), "m", cancel=cancel),  # type: ignore[arg-type]
+            workspace=Workspace(w["host"], w["repo"].root, timeout_s=30),
+            worker=InlineWorker(),
+            cancel=cancel,
+            oplog=OpLog("nisse-dev", _Null()),
+            milestones=w["milestones"],
+        )
+        transport.on_message(agent.on_message)
+        return agent, transport
+
+    def items(self) -> list[Any]:
+        return self.world["store"].work_items()
+
+    def step(self) -> None:
+        forge: Forge = self.world["forge"]
+        open_items = [i for i in self.items() if i.status == "open"]
+        # Weighted towards what an item can actually do, so review paths
+        # are walked often, not drowned out by intake and crashes.
+        weights = {"intake": 2 if not open_items else 1, "crash": 1}
+        for item in open_items:
+            loop = loop_of(item)
+            weights.update({"go": 3, "answer": 2, "abandon": 1, "go-stale": 1})
+            if loop.pr:
+                weights.update(
+                    {"comment": 4, "merge": 2, "close-pr": 1, "comment-merge": 2}
+                )
+        action = self.rng.choices(list(weights), list(weights.values()))[0]
+        self.steps.append(action)
+        item = open_items[0] if open_items else None
+        loop = loop_of(item) if item else None
+        if action == "intake":
+            self.agent.intake()
+        elif action == "crash":
+            # Volatile state is lost: a new agent over the same store.
+            self.agent, self.transport = self._agent()
+            self.agent.boot()
+            self.agent._schedule()
+        elif action in ("go", "answer", "abandon") and loop:
+            text = {"go": "go", "answer": "an answer", "abandon": "abandon"}[action]
+            if action == "go" and item.position == WAITING and loop.wait == GO_AHEAD:
+                self.shown_at_go.append(loop.rev)
+            self.transport.receive(DON, text, thread=loop.thread)
+        elif action == "go-stale" and loop and loop.rev > 1:
+            # A go sent while an older revision was on screen.
+            self.agent.handle(
+                InboundMessage(DON, "go", thread=loop.thread), about=loop.rev - 1
+            )
+        elif action == "comment" and loop:
+            forge.comments.setdefault(loop.pr, []).append(
+                Comment(len(self.steps) * 10, "don", f"comment {len(self.steps)}", "t")
+            )
+            self.agent.watch()
+            self.agent._schedule()
+        elif (
+            action == "comment-merge" and loop and forge.prs[loop.pr]["state"] == "open"
+        ):
+            # The race: a comment is seen, then the PR merges before the
+            # driver's fix lands.
+            forge.comments.setdefault(loop.pr, []).append(
+                Comment(len(self.steps) * 10, "don", f"comment {len(self.steps)}", "t")
+            )
+            self.agent.watch()
+            forge.merge(loop.pr)
+            self.agent._schedule()
+        elif action == "merge" and loop and forge.prs[loop.pr]["state"] == "open":
+            forge.merge(loop.pr)
+            self.agent.watch()
+            self.agent._schedule()
+        elif action == "close-pr" and loop and forge.prs[loop.pr]["state"] == "open":
+            forge.prs[loop.pr]["state"] = "closed"
+            self.agent.watch()
+            self.agent._schedule()
+
+    # -- the properties (specs/loop.qnt) -------------------------------------
+
+    def check(self) -> None:
+        where = f"seed {self.seed}, steps {self.steps}"
+        store, forge = self.world["store"], self.world["forge"]
+        items = self.items()
+        issues = [loop_of(i).issue for i in items if loop_of(i).issue]
+        assert len(issues) == len(set(issues)), f"one_item_per_issue: {where}"
+        for item in items:
+            loop = loop_of(item)
+            if item.status == "open" and item.position == WAITING:
+                explained = (
+                    (loop.wait == GO_AHEAD and loop.rev > 0)
+                    or (loop.wait == ANSWER and bool(loop.note))
+                    or (loop.wait == MERGE and loop.pr > 0)
+                )
+                assert explained, (
+                    f"waits_are_explainable: {item.position} {loop}: {where}"
+                )
+            gos = [
+                int(f.event.text.split("rev-")[1].split()[0])
+                for f in store.transcript(item.id, "orchestrator").read()
+                if isinstance(f.event, Fact)
+                and f.event.text.startswith("go-ahead on rev-")
+            ]
+            assert all(rev in self.shown_at_go for rev in gos), (
+                f"go_binds: {gos}: {where}"
+            )
+            mine = [p for p in forge.prs.values() if p["head"].startswith(item.id)]
+            assert sum(p["state"] == "open" for p in mine) <= 1, (
+                f"milestone_after_merge: {where}"
+            )
+            if item.status == "closed":
+                assert not any(p["state"] == "open" for p in mine), (
+                    f"closed_items_leave_nothing (PR): {where}"
+                )
+                assert not [
+                    i for i in store.pending_intents() if i.work_item == item.id
+                ], f"closed_items_leave_nothing (intent): {where}"
+        heads = [p["head"] for p in forge.prs.values()]
+        assert len(heads) == len(set(heads)), f"one_pr_per_milestone: {where}"
+        bare = self.world["bare"]
+        for n, pr in forge.prs.items():
+            if not pr["merged"]:
+                continue
+            head = _rev(bare, f"refs/heads/{pr['head']}")
+            # A fix pushed after the merge must reach the operator as a PR
+            # (loop.qnt's lostFix): in main, or in a later PR, whatever they
+            # then decide about it.
+            landed = _is_ancestor(bare, head, "refs/heads/main") or any(
+                _is_ancestor(bare, head, f"refs/heads/{other['head']}")
+                for m, other in forge.prs.items()
+                if m > n
+            )
+            assert landed, f"review_fixes_land (PR {n}): {where}"
+
+
+class _Null:
+    def write(self, _: str) -> None: ...
+
+    def flush(self) -> None: ...
+
+
+def _rev(bare: Path, ref: str) -> str:
+    return subprocess.run(
+        ["git", "--git-dir", str(bare), "rev-parse", ref],
+        capture_output=True,
+        text=True,
+        check=True,
+    ).stdout.strip()
+
+
+def _is_ancestor(bare: Path, commit: str, ref: str) -> bool:
+    return (
+        subprocess.run(
+            ["git", "--git-dir", str(bare), "merge-base", "--is-ancestor", commit, ref],
+            capture_output=True,
+            check=False,
+        ).returncode
+        == 0
+    )
+
+
+@pytest.mark.parametrize("seed", SEEDS)
+def test_the_loop_keeps_its_properties(world: dict[str, Any], seed: int) -> None:
+    walk = Walk(world, seed)
+    for _ in range(STEPS):
+        walk.step()
+        walk.check()

specs/README.md

@@ -65,6 +65,13 @@ 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 in the same PR. When the new loop is built (Development Plan Phase 2),
+the model and the walk in the same PR.
-each property gets a test against the real code, as `orchestrator.qnt`'s did.