specs/README.md

@@ -36,3 +36,35 @@ Exhaustive bounded checking (`quint verify`) uses Apalache and needs Java 17.
 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.
+
+```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.
+
+**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),
+each property gets a test against the real code, as `orchestrator.qnt`'s did.

specs/loop.qnt

@@ -0,0 +1,489 @@
+// A model of the agent loop as docs/Architecture.md describes it (PR #90):
+// work items from assigned issues and conversations, restatements and
+// go-aheads, park-and-switch, blocked dependencies, harness-owned milestones,
+// waiting for merges, review follow-ups, and crashes at any point.
+//
+// Unlike orchestrator.qnt, this models a design, not code: the new loop
+// doesn't exist yet, so a counterexample here is a gap in the architecture.
+//
+// Everything lives in one record, `s`. Durable state (the state store,
+// Gitea, the build VM's disk) survives a crash; volatile state (work in
+// flight) does not. Ghost fields record what the properties need to know
+// and the agent never reads.
+//
+// Run:  quint run specs/loop.qnt --invariant=all_properties
+module loop {
+
+  // ---- bounds --------------------------------------------------------------
+
+  pure val MAX_ITEMS = 3     // work items per run
+  pure val MAX_REV = 3       // restatement revisions per item
+  pure val MAX_MS = 2        // milestones per item
+  pure val MAX_INBOX = 3     // operator messages not yet handled
+  pure val PROJECTS = Set("A", "B")
+  pure val ISSUES = Set(1, 2)          // issues the operator can file and assign
+  pure val DEP_ISSUES = Set(101, 102)  // other issues an item can be blocked by
+
+  // ---- state ---------------------------------------------------------------
+
+  type Item = {
+    status: str,       // ready / waiting / blocked / closed (active is s.active)
+    src: str,          // issue / conv
+    issue: int,        // its record issue, 0 if none yet
+    project: str,
+    bug: bool,
+    waitFor: str,      // goahead / grace / answer / agree / merge, when waiting
+    question: bool,    // a question to the operator is pending (L2)
+    rev: int,          // latest restatement put up (L3)
+    needRestate: bool, // an answer changed the understanding: restate again
+    started: bool,     // scope agreed: a go-ahead, or a bug's grace period over (D1)
+    ms: int,           // current milestone, 0 before the first
+    attempt: int,      // a redo of a milestone whose PR was closed gets a new branch
+    stage: str,        // none / working / pr
+    review: bool,      // a review comment is waiting to be answered (D5)
+    unpushed: bool,    // work on the build VM not yet pushed
+    deps: Set[int],    // recorded dependencies (L1)
+  }
+
+  type Issue = { open: bool, assigned: bool, linked: int }
+  type Msg = { item: int, kind: str, saw: int }
+
+  type Sys = {
+    // -- durable: the state store --
+    items: int -> Item,
+    nextItem: int,
+    active: int,              // 0: none (L1)
+    intents: Set[int],        // pending publish intents, by PR key (L8)
+    // -- durable: Gitea --
+    issues: int -> Issue,
+    depOpen: int -> bool,
+    prs: int -> str,          // PR key -> open / merged / closed
+    opened: int -> int,       // PR key -> PRs ever opened for it
+    // -- durable: Matrix holds messages until the agent handles them --
+    inbox: List[Msg],
+    // -- volatile --
+    work: str,                // none / publish
+    pubStage: int,
+    pending: int,             // a record issue created but not yet linked
+    // -- ghosts --
+    badGo: bool,              // work started on a revision the operator never saw
+    earlyMs: bool,            // a milestone started before the previous merged
+    lostFix: bool,            // a review fix pushed to a PR no longer open
+    lostWork: bool,           // a parked item's unpushed work was set aside or wiped
+  }
+
+  var s: Sys
+
+  pure def prKey(i: int, ms: int, a: int): int = i * 100 + ms * 10 + a
+  pure def keyOf(t: Sys, i: int): int = prKey(i, t.items.get(i).ms, t.items.get(i).attempt)
+  pure def prOf(t: Sys, i: int): str = {
+    val k = keyOf(t, i)
+    if (t.prs.keys().contains(k)) t.prs.get(k) else ""
+  }
+  pure def upd(t: Sys, i: int, it: Item): Sys = { ...t, items: t.items.set(i, it) }
+  pure def itm(t: Sys, i: int): Item = t.items.get(i)
+  pure def live(t: Sys): Set[int] = t.items.keys().filter(i => t.items.get(i).status != "closed")
+
+  pure def newItem(src: str, issue: int, project: str, bug: bool): Item = {
+    status: "ready", src: src, issue: issue, project: project, bug: bug,
+    waitFor: "", question: false, rev: 0, needRestate: false, started: false,
+    ms: 0, attempt: 0, stage: "none", review: false, unpushed: false, deps: Set(),
+  }
+
+  pure def wait(it: Item, why: str, q: bool): Item =
+    { ...it, status: "waiting", waitFor: why, question: q }
+  pure def ready(it: Item): Item = { ...it, status: "ready", waitFor: "", question: false }
+
+  action init = s' = {
+    items: Map(), nextItem: 1, active: 0, intents: Set(),
+    issues: ISSUES.mapBy(_ => { open: false, assigned: false, linked: 0 }),
+    depOpen: DEP_ISSUES.mapBy(_ => true),
+    prs: Map(), opened: Map(), inbox: List(),
+    work: "none", pubStage: 0, pending: 0,
+    badGo: false, earlyMs: false, lostFix: false, lostWork: false,
+  }
+
+  // ---- the operator ----------------------------------------------------------
+
+  // Files an issue and assigns it to the agent (D1).
+  // (Its project and `bug` label are chosen at intake.)
+  action assignIssue(n: int): bool = all {
+    not(s.issues.get(n).open), s.issues.get(n).linked == 0,
+    s' = { ...s, issues: s.issues.set(n, { open: true, assigned: true, linked: 0 }) },
+  }
+
+  // Starts a conversation: a work item from its first message (L5).
+  action converse(p: str): bool = all {
+    s.nextItem <= MAX_ITEMS,
+    s' = { ...s, items: s.items.put(s.nextItem, newItem("conv", 0, p, false)),
+           nextItem: s.nextItem + 1 },
+  }
+
+  // Replies in an item's thread. `saw` is the revision on screen when sent.
+  action say(i: int, kind: str): bool = all {
+    live(s).contains(i), s.inbox.length() < MAX_INBOX,
+    s' = { ...s, inbox: s.inbox.append({ item: i, kind: kind, saw: itm(s, i).rev }) },
+  }
+
+  // Merges, closes or comments on an item's open PR (D4, D5).
+  action prAct(i: int, what: str): bool = {
+    val k = keyOf(s, i)
+    all {
+      s.items.keys().contains(i), prOf(s, i) == "open",
+      s' = if (what == "comment") upd(s, i, { ...itm(s, i), review: true })
+           else { ...s, prs: s.prs.set(k, what) },
+    }
+  }
+
+  // Closes an issue another item depends on.
+  action closeDep(d: int): bool = all {
+    s.depOpen.get(d), s' = { ...s, depOpen: s.depOpen.set(d, false) },
+  }
+
+  // ---- intake and the duty ---------------------------------------------------
+
+  // The duty picks up an assigned, open issue that no item is linked to (D1).
+  action intake(n: int, p: str, bug: bool): bool = {
+    val known = s.issues.keys().contains(n)
+    val is = s.issues.get(n)
+    all {
+      known, is.open, is.assigned, is.linked == 0, s.nextItem <= MAX_ITEMS,
+      s' = { ...s, items: s.items.put(s.nextItem, newItem("issue", n, p, bug)),
+             issues: s.issues.set(n, { ...is, linked: s.nextItem }),
+             nextItem: s.nextItem + 1 },
+    }
+  }
+
+  // The duty notices external truth: a merged or closed PR, a dependency
+  // closed. (L1 blocked, D4 wait for the merge.)
+  action observe(i: int): bool = {
+    val it = itm(s, i)
+    all {
+      live(s).contains(i),
+      any {
+        all { it.status == "blocked", it.deps.forall(d => not(s.depOpen.get(d))),
+              s' = upd(s, i, ready({ ...it, deps: Set() })) },
+        all { it.stage == "pr", prOf(s, i) == "merged", not(it.review),
+              s' = upd(s, i, ready({ ...it, stage: "none" })) },
+        // D4: ready with that fact; the agent asks what next.
+        // FIX 4 (D4): a redo is the same milestone on a new branch and PR.
+        all { it.stage == "pr", prOf(s, i) == "closed",
+              s' = upd(s, i, wait({ ...it, stage: "none", ms: it.ms - 1,
+                                         attempt: it.attempt + 1 }, "answer", true)) },
+        all { it.stage == "pr", it.review, it.status == "waiting",
+              s' = upd(s, i, ready(it)) },
+      },
+    }
+  }
+
+  // ---- handling messages (conversation is not work, L1) ----------------------
+
+  pure def handle(t: Sys, m: Msg): Sys = {
+    val it = itm(t, m.item)
+    if (it.status == "closed") t
+    else if (m.kind == "go")
+      // L3: bound to the revision up when the reply arrived.
+      if (it.status == "waiting" and it.waitFor == "goahead" and m.saw == it.rev)
+        { ...upd(t, m.item, ready({ ...it, started: true })), badGo: t.badGo or m.saw != it.rev }
+      else t
+    else if (m.kind == "answer")
+      if (it.question and (it.waitFor == "answer"))
+        upd(t, m.item, ready({ ...it, needRestate: not(it.started) }))
+      else t
+    else if (m.kind == "agree")
+      // D1/L1: the operator agrees a blocker should be recorded.
+      if (it.waitFor == "agree") upd(t, m.item, { ...it, status: "blocked", waitFor: "",
+                                                  question: false, deps: Set(101) })
+      else t
+    else if (m.kind == "decline")
+      if (it.waitFor == "agree") upd(t, m.item, ready(it)) else t
+    else if (m.kind == "abandon")
+      // L2: from any waiting point; closes the record, aborts its intents.
+      if (t.active == m.item and t.work != "none") t
+      else {
+        val closed = upd(t, m.item, { ...it, status: "closed", question: false })
+        val withIssue = if (it.issue != 0)
+            { ...closed, issues: closed.issues.set(it.issue,
+                { ...closed.issues.get(it.issue), open: false }) }
+          else closed
+        val noIntents = { ...withIssue, intents: withIssue.intents.filter(k => k / 100 != m.item) }
+        // FIX 1 (L2): abandoning closes the item's open PR with a note.
+        { ...noIntents, prs: noIntents.prs.keys().mapBy(k =>
+            if (k / 100 == m.item and noIntents.prs.get(k) == "open") "closed"
+            else noIntents.prs.get(k)) }
+      }
+    else t
+  }
+
+  action handleMsg: bool = all {
+    s.inbox.length() > 0, s.work == "none",
+    s' = { ...handle(s, s.inbox.head()), inbox: s.inbox.tail() },
+  }
+
+  // ---- the agent ---------------------------------------------------------------
+
+  // Switching: the active item is at a safe point; parking pushes its branch (D4).
+  action park: bool = {
+    val it = itm(s, s.active)
+    all {
+      s.active != 0, s.work == "none", s.intents.size() == 0,
+      Set("waiting", "blocked", "closed").contains(it.status),
+      s' = { ...upd(s, s.active, { ...it, unpushed: false }), active: 0 },
+    }
+  }
+
+  // Taking up a ready item: a fresh workspace on its project's build VM (D3)
+  // sets aside whatever is left there.
+  action activate(i: int): bool = all {
+    s.active == 0, s.work == "none", live(s).contains(i), itm(s, i).status == "ready",
+    s' = {
+      val leftovers = s.items.keys().exists(j => j != i and itm(s, j).project == itm(s, i).project
+                                                  and itm(s, j).unpushed)
+      { ...s, active: i, lostWork: s.lostWork or leftovers }
+    },
+  }
+
+  // Restating (D1): bug → grace period; otherwise wait for a go-ahead; or ask.
+  action restate(ask: bool): bool = {
+    val i = s.active
+    val it = itm(s, i)
+    all {
+      i != 0, s.work == "none", it.status == "ready", not(it.started),
+      it.rev < MAX_REV,
+      s' = upd(s, i,
+        if (ask) wait({ ...it, rev: it.rev + 1, needRestate: false }, "answer", true)
+        else if (it.bug) wait({ ...it, rev: it.rev + 1, needRestate: false }, "grace", false)
+        else wait({ ...it, rev: it.rev + 1, needRestate: false }, "goahead", false)),
+    }
+  }
+
+  // A bug's grace period runs out: the item is ready to work (D1).
+  action graceOver(i: int): bool = all {
+    live(s).contains(i), itm(s, i).waitFor == "grace",
+    s' = upd(s, i, ready({ ...itm(s, i), started: true })),
+  }
+
+  // Work on a repository needs a record issue (D1). Opening one is an
+  // external effect, then the link is written: two steps.
+  action createRecord: bool = {
+    val it = itm(s, s.active)
+    val n = 100 - s.active   // the record's issue number
+    all {
+      s.active != 0, s.work == "none", it.status == "ready", it.started, it.issue == 0,
+      s.pending == 0,
+      // FIX 5 (D1): the issue carries its work item's ID from creation, so
+      // intake never takes it for new work, even before the link is stored.
+      s' = { ...s, pending: s.active,
+             issues: s.issues.put(n, { open: true, assigned: true, linked: s.active }) },
+    }
+  }
+
+  action linkRecord: bool = {
+    val n = 100 - s.pending
+    all {
+      s.pending != 0,
+      s' = { ...upd(s, s.pending, { ...itm(s, s.pending), issue: n }),
+             issues: s.issues.set(n, { ...s.issues.get(n), linked: s.pending }),
+             pending: 0 },
+    }
+  }
+
+  // start_milestone (D4): only after the previous milestone's PR merged.
+  action startMilestone: bool = {
+    val i = s.active
+    val it = itm(s, i)
+    all {
+      i != 0, s.work == "none", it.status == "ready", it.started, it.issue != 0,
+      it.stage == "none", it.ms < MAX_MS,
+      s' = {
+        val early = it.ms > 0 and prOf(s, i) != "merged"
+        { ...upd(s, i, { ...it, ms: it.ms + 1, stage: "working", unpushed: true }),
+          earlyMs: s.earlyMs or early }
+      },
+    }
+  }
+
+  // A turn of work: progress, a blocker to propose, or a question.
+  action turn(outcome: str): bool = {
+    val i = s.active
+    val it = itm(s, i)
+    all {
+      i != 0, s.work == "none", it.status == "ready", it.stage == "working",
+      s' = upd(s, i,
+        if (outcome == "progress") { ...it, unpushed: true }
+        else if (outcome == "blocker") wait(it, "agree", true)
+        else wait(it, "answer", true)),
+    }
+  }
+
+  // finish_milestone (D4): commit, push, open the PR, under an intent (L8).
+  action finishMilestone: bool = {
+    val it = itm(s, s.active)
+    all {
+      s.active != 0, s.work == "none", it.status == "ready", it.stage == "working",
+      s' = { ...s, work: "publish", pubStage: 0 },
+    }
+  }
+
+  action publishStep(lost: bool): bool = {
+    val i = s.active
+    val it = itm(s, i)
+    val k = keyOf(s, i)
+    all {
+      s.work == "publish",
+      s' =
+        if (s.pubStage == 0) { ...s, intents: s.intents.union(Set(k)), pubStage: 1 }
+        else if (s.pubStage == 1) {
+          val pushed = upd(s, i, { ...it, unpushed: false })
+          if (s.prs.keys().contains(k) and s.prs.get(k) == "open") { ...pushed, pubStage: 2 }
+          // FIX 2 (D4, L8): the branch's PR was closed: report it, never open another.
+          else if (s.prs.keys().contains(k) and s.prs.get(k) != "open")
+            { ...upd(pushed, i, wait({ ...itm(pushed, i), stage: "pr" }, "answer", true)),
+              intents: pushed.intents.exclude(Set(k)), work: "none", pubStage: 0 }
+          else {
+            val n = if (s.opened.keys().contains(k)) s.opened.get(k) else 0
+            val withPr = { ...pushed, prs: pushed.prs.put(k, "open"),
+                           opened: pushed.opened.put(k, n + 1) }
+            // A lost response: Gitea opened it, the agent never heard.
+            if (lost) { ...withPr, work: "none", pubStage: 0 } else { ...withPr, pubStage: 2 }
+          }
+        }
+        else { ...upd(s, i, wait({ ...it, stage: "pr", unpushed: false }, "merge", false)),
+               intents: s.intents.exclude(Set(k)), work: "none", pubStage: 0 },
+    }
+  }
+
+  // Answering a review comment: commits pushed to the PR's branch (D5).
+  action answerReview: bool = {
+    val i = s.active
+    val it = itm(s, i)
+    all {
+      i != 0, s.work == "none", it.status == "ready", it.stage == "pr", it.review,
+      s' =
+        if (prOf(s, i) == "open")
+          upd(s, i, wait({ ...it, review: false, unpushed: false }, "merge", false))
+        // FIX 3 (D5): the PR merged first: the fix goes out as a new PR.
+        else if (prOf(s, i) == "merged")
+          upd(s, i, { ...it, review: false, stage: "working", attempt: it.attempt + 1,
+                      unpushed: true })
+        // ...or it was closed: say so and ask.
+        else upd(s, i, wait({ ...it, review: false, stage: "none" }, "answer", true)),
+    }
+  }
+
+  // Finishing: the last PR merged, the agent closes the item (D1).
+  action finish: bool = {
+    val i = s.active
+    val it = itm(s, i)
+    all {
+      i != 0, s.work == "none", it.status == "ready", it.ms > 0, it.stage == "none",
+      prOf(s, i) == "merged",
+      s' = upd(s, i, { ...it, status: "closed" }),
+    }
+  }
+
+  // The build VM is wiped (D3): unpushed work on it is lost, accepted for
+  // the active item, never for a parked one.
+  action wipe(p: str): bool = all {
+    s' = { ...s,
+      items: s.items.keys().mapBy(j =>
+        if (itm(s, j).project == p) { ...itm(s, j), unpushed: false } else itm(s, j)),
+      lostWork: s.lostWork or s.items.keys().exists(j =>
+        j != s.active and itm(s, j).project == p and itm(s, j).unpushed) },
+  }
+
+  // ---- crash and boot (L8) --------------------------------------------------
+
+  // Volatile state is lost; boot reconciles each pending intent against
+  // Gitea: an open PR is adopted, otherwise the intent is aborted and the
+  // operator is told (L8 step 5).
+  pure def reconcile(t: Sys, k: int): Sys = {
+    val i = k / 100
+    val it = itm(t, i)
+    val t2 = { ...t, intents: t.intents.exclude(Set(k)) }
+    if (t.prs.keys().contains(k) and t.prs.get(k) == "open")
+      upd(t2, i, wait({ ...it, stage: "pr", unpushed: false }, "merge", false))
+    else upd(t2, i, wait(it, "answer", true))
+  }
+
+  action crash: bool =
+    s' = s.intents.fold({ ...s, work: "none", pubStage: 0, pending: 0 },
+                        (t, k) => reconcile(t, k))
+
+  // ---- step ---------------------------------------------------------------------
+
+  action step = {
+    nondet n = ISSUES.oneOf()
+    nondet anyIssue = s.issues.keys().oneOf()
+    nondet i = 1.to(MAX_ITEMS).oneOf()
+    nondet p = PROJECTS.oneOf()
+    nondet b = Set(true, false).oneOf()
+    nondet kind = Set("go", "answer", "agree", "decline", "abandon").oneOf()
+    nondet what = Set("merged", "closed", "comment").oneOf()
+    nondet outcome = Set("progress", "blocker", "question").oneOf()
+    nondet d = DEP_ISSUES.oneOf()
+    any {
+      assignIssue(n), converse(p), say(i, kind), prAct(i, what), closeDep(d),
+      intake(anyIssue, p, b), observe(i), handleMsg,
+      park, activate(i), restate(b), graceOver(i), createRecord, linkRecord,
+      startMilestone, turn(outcome), finishMilestone, publishStep(b), answerReview,
+      finish, wipe(p), crash,
+    }
+  }
+
+  // ---- properties ---------------------------------------------------------------
+
+  // An issue is the record of at most one work item (D1 intake).
+  val one_item_per_issue = s.items.keys().forall(a => s.items.keys().forall(b =>
+    (a != b and itm(s, a).issue != 0) implies itm(s, a).issue != itm(s, b).issue))
+
+  // Every wait is for something the operator can see or a dependency (L2).
+  val waits_are_explainable = live(s).forall(i => {
+    val it = itm(s, i)
+    and {
+      it.status == "waiting" implies or {
+        it.waitFor == "goahead" and it.rev > 0,
+        it.waitFor == "grace",
+        Set("answer", "agree").contains(it.waitFor) and it.question,
+        it.waitFor == "merge" and prOf(s, i) != "",
+      },
+      it.status == "blocked" implies it.deps.size() > 0,
+    }
+  })
+
+  // Work starts only on a go-ahead for the revision the operator saw (L3).
+  val go_binds = not(s.badGo)
+
+  // The next milestone starts only after the previous PR merged (D4).
+  val milestone_after_merge = not(s.earlyMs)
+
+  // A parked item's work is never set aside or wiped (D4 parking).
+  val parked_work_safe = not(s.lostWork)
+
+  // Never more than one PR opened for a milestone (L8).
+  val one_pr_per_milestone = s.opened.keys().forall(k => s.opened.get(k) <= 1)
+
+  // A review fix always lands on an open PR (D5).
+  val review_fixes_land = not(s.lostFix)
+
+  // A closed item leaves no open PR and no pending intent behind (L2).
+  val closed_items_leave_nothing = s.items.keys().forall(i =>
+    itm(s, i).status == "closed" implies and {
+      s.prs.keys().forall(k => k / 100 == i implies s.prs.get(k) != "open"),
+      s.intents.forall(k => k / 100 != i),
+    })
+
+  val all_properties = and {
+    one_item_per_issue, waits_are_explainable, go_binds, milestone_after_merge,
+    parked_work_safe, one_pr_per_milestone, review_fixes_land, closed_items_leave_nothing,
+  }
+
+  // ---- reachability witnesses (each should be violated) --------------------------
+  val w_pr_opened = s.opened.keys().size() == 0
+  val w_merged = not(s.prs.keys().exists(k => s.prs.get(k) == "merged"))
+  val w_second_ms = not(s.items.keys().exists(i => itm(s, i).ms == 2))
+  val w_blocked = not(s.items.keys().exists(i => itm(s, i).status == "blocked"))
+  val w_review = not(s.items.keys().exists(i => itm(s, i).review))
+  val w_record = not(s.items.keys().exists(i => itm(s, i).src == "conv" and itm(s, i).issue != 0))
+  val w_finished = not(s.items.keys().exists(i => itm(s, i).status == "closed" and itm(s, i).ms > 0))
+}

specs/loop_scenarios.qnt

@@ -0,0 +1,77 @@
+// Counterexamples found in loop.qnt, written out as short traces. Each was a
+// gap in docs/Architecture.md; the model now has the proposed fix (marked
+// FIX n in loop.qnt), and each trace checks the fixed behaviour.
+//
+// Run:  quint test specs/loop_scenarios.qnt   (runs every *Test)
+module loop_scenarios {
+  import loop.* from "./loop"
+
+  // An assigned issue, restated, a go-ahead, milestone 1 under way.
+  action toWorking = init
+    .then(assignIssue(1)).then(intake(1, "A", false))
+    .then(activate(1)).then(restate(false))
+    .then(say(1, "go")).then(handleMsg)
+    .then(startMilestone)
+
+  // ...and published: its PR is open and the item waits for the merge.
+  action toPrOpen = toWorking
+    .then(finishMilestone)
+    .then(publishStep(false)).then(publishStep(false)).then(publishStep(false))
+
+  // 1. Abandoning an item left its open PR open: L2 closed the record and
+  //    aborted intents, but said nothing about PRs. Fixed: abandon closes
+  //    the item's open PRs with a note.
+  run abandonClosesTheOpenPrTest =
+    toPrOpen
+      .then(park)
+      .then(say(1, "abandon")).then(handleMsg)
+      .expect(closed_items_leave_nothing and s.prs.get(prKey(1, 1, 0)) == "closed")
+
+  // 2. Gitea opened the PR but the response was lost, so the agent never
+  //    knew. The operator closed that PR; the agent's retry only adopted
+  //    *open* PRs, so it opened a second one over the operator's close.
+  //    Fixed: a closed PR on the branch is an answer: report it and ask.
+  run retryNeverReopensAClosedPrTest =
+    toWorking
+      .then(finishMilestone)
+      .then(publishStep(false))
+      .then(publishStep(true))          // opened, response lost
+      .then(prAct(1, "closed"))         // the operator closes it
+      .then(finishMilestone)            // the agent retries
+      .then(publishStep(false)).then(publishStep(false))
+      .expect(one_pr_per_milestone and itm(s, 1).waitFor == "answer")
+
+  // 3. A review comment made the item ready; the operator merged the PR
+  //    before the fix was pushed, so the fix went to a merged branch and
+  //    never reached main. Fixed: a fix for a PR that merged meanwhile goes
+  //    out as a new PR (and one for a closed PR is reported).
+  run reviewFixAfterMergeGetsANewPrTest =
+    toPrOpen
+      .then(prAct(1, "comment")).then(observe(1))
+      .then(prAct(1, "merged"))
+      .then(answerReview)
+      .expect(review_fixes_land and itm(s, 1).stage == "working" and itm(s, 1).attempt == 1)
+
+  // 4. After a PR closed unmerged and the operator answered, the next
+  //    milestone could start with the closed one never merged. Fixed: a
+  //    redo is the same milestone on a new branch and PR.
+  run closedPrRedoesTheSameMilestoneTest =
+    toPrOpen
+      .then(prAct(1, "closed")).then(observe(1))
+      .then(say(1, "answer")).then(handleMsg)
+      .then(startMilestone)
+      .expect(milestone_after_merge and itm(s, 1).ms == 1 and itm(s, 1).attempt == 1)
+
+  // 5. Work begun in conversation gets a record issue, assigned to the
+  //    agent. Opening it and storing the link were two steps, and intake
+  //    could take the assigned, unlinked issue for new work in between.
+  //    Fixed: the issue carries its work item's ID from creation.
+  run recordIssueIsNeverTakenForNewWorkTest =
+    init
+      .then(converse("A")).then(activate(1)).then(restate(false))
+      .then(say(1, "go")).then(handleMsg)
+      .then(createRecord)
+      .expect(s.issues.get(99).linked == 1)
+      .then(linkRecord)
+      .expect(one_item_per_issue and itm(s, 1).issue == 99)
+}