M4.3: a broken build VM blocks its projects until it's ready

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

specs/loop.qnt

@@ -61,6 +61,8 @@ module loop {
     opened: int -> int,       // PR key -> PRs ever opened for it
     // -- durable: Matrix holds messages until the agent handles them --
     inbox: List[Msg],
+    // -- durable: the state store's VM blocks (D3) --
+    vmBlocked: Set[str],      // projects whose build VM waits for recovery
     // -- volatile --
     work: str,                // none / publish
     pubStage: int,
@@ -70,6 +72,7 @@ module loop {
     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
+    ranBlocked: bool,         // an item was taken up on a blocked build VM
   }
 
   var s: Sys
@@ -98,9 +101,10 @@ module loop {
     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(),
+    prs: Map(), opened: Map(), inbox: List(), vmBlocked: Set(),
     work: "none", pubStage: 0, pending: 0,
     badGo: false, earlyMs: false, lostFix: false, lostWork: false,
+    ranBlocked: false,
   }
 
   // ---- the operator ----------------------------------------------------------
@@ -236,10 +240,12 @@ module loop {
   // 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",
+    not(s.vmBlocked.contains(itm(s, i).project)),  // D3: nothing runs on a blocked VM
     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 }
+      { ...s, active: i, lostWork: s.lostWork or leftovers,
+        ranBlocked: s.ranBlocked or s.vmBlocked.contains(itm(s, i).project) }
     },
   }
 
@@ -392,6 +398,30 @@ module loop {
         j != s.active and itm(s, j).project == p and itm(s, j).unpushed) },
   }
 
+  // The driver finds its build VM broken (request_reimage, D3): its work is
+  // parked (pushed), the VM blocked and the run ends; the item stays ready,
+  // to go on once it's fixed. (A VM too broken to push loses the work; the
+  // operator is told before reimaging it, accepted as for any wipe.)
+  action requestReimage: bool = {
+    val it = itm(s, s.active)
+    all {
+      s.active != 0, s.work == "none", s.intents.size() == 0, it.status == "ready",
+      s' = { ...upd(s, s.active, { ...it, unpushed: false }),
+             vmBlocked: s.vmBlocked.union(Set(it.project)), active: 0 },
+    }
+  }
+
+  // The operator's `vm ready`: the block lifts. A reimage loses what wasn't
+  // pushed on the VM; the operator was told so, and agreed by doing it.
+  action vmReady(p: str, reimaged: bool): bool = all {
+    s.vmBlocked.contains(p),
+    s' = { ...s,
+      vmBlocked: s.vmBlocked.exclude(Set(p)),
+      items: if (reimaged) s.items.keys().mapBy(j =>
+               if (itm(s, j).project == p) { ...itm(s, j), unpushed: false } else itm(s, j))
+             else s.items },
+  }
+
   // ---- crash and boot (L8) --------------------------------------------------
 
   // Volatile state is lost; boot reconciles each pending intent against
@@ -427,7 +457,7 @@ module loop {
       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,
+      finish, wipe(p), crash, requestReimage, vmReady(p, b),
     }
   }
 
@@ -473,9 +503,13 @@ module loop {
       s.intents.forall(k => k / 100 != i),
     })
 
+  // Nothing is taken up on a build VM that is blocked (D3).
+  val blocked_vm_runs_nothing = not(s.ranBlocked)
+
   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,
+    blocked_vm_runs_nothing,
   }
 
   // ---- reachability witnesses (each should be violated) --------------------------
@@ -485,5 +519,6 @@ module loop {
   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_vm_blocked = s.vmBlocked.size() == 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

@@ -74,4 +74,15 @@ module loop_scenarios {
       .expect(s.issues.get(99).linked == 1)
       .then(linkRecord)
       .expect(one_item_per_issue and itm(s, 1).issue == 99)
+
+  // M4.3: a build VM the driver finds broken blocks its project; nothing is
+  // taken up on it until the operator says `vm ready`, then work goes on.
+  run aBrokenVmBlocksUntilReadyTest =
+    init
+      .then(assignIssue(1)).then(intake(1, "A", false))
+      .then(activate(1)).then(requestReimage)
+      .expect(s.vmBlocked.contains("A") and s.active == 0)
+      .then(vmReady("A", true))
+      .then(activate(1))
+      .expect(blocked_vm_runs_nothing and s.active == 1)
 }