M4.4: an unreachable build VM blocks its projects until it's back (#137)

M4.3's block, with new triggers and a way out. A VM out of reach at the
check before a run, in a run (which ends there: the driver, a toolchain
step and a requested step), or while preparing the workspace blocks every
project on it; the item stays ready, waiting on no one. On the intake round
it is tried again every tuning.build_vm.retry_s (300), and once it answers
it must still answer settle_s (180) later; then the work a lost run left
there is parked (pushed), the VM unblocked, and that said once.

A changed host key, at the check or on a retry, blocks the VM too, until
the operator's `vm ready`, which trusts the new key: `trust new host key`
is retired, and the message says it's a key problem that may be an
impersonation. Questions are answered while a VM is blocked, without it.
Starting the agent with a VM down no longer fails.

The walk breaks the VM's SSH, now or partway through a run, and checks that
no model works on a VM that is down; loop.qnt models the VM going and
coming back (unblocked_only_when_up). Together they found: a lost run's
work set aside by the next item there; a question left behind a block; a
lost VM swallowed while the toolchain step checked or recorded it; and a
remark waiting to be answered that outlived its PR's merge. All fixed.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J5Utyfzw7gF7UhjRDEtjTk

specs/loop.qnt

@@ -63,6 +63,9 @@ module loop {
     inbox: List[Msg],
     // -- durable: the state store's VM blocks (D3) --
     vmBlocked: Set[str],      // projects whose build VM waits for recovery
+    vmUnreachable: Set[str],  // ...because it was out of reach: probes may clear it (#137)
+    // -- the world: build VMs out of reach --
+    vmDown: Set[str],
     // -- volatile --
     work: str,                // none / publish
     pubStage: int,
@@ -73,6 +76,7 @@ module loop {
     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
+    badUnblock: bool,         // a probe unblocked a VM that was still down
   }
 
   var s: Sys
@@ -102,9 +106,10 @@ module loop {
     issues: ISSUES.mapBy(_ => { open: false, assigned: false, linked: 0 }),
     depOpen: DEP_ISSUES.mapBy(_ => true),
     prs: Map(), opened: Map(), inbox: List(), vmBlocked: Set(),
+    vmUnreachable: Set(), vmDown: Set(),
     work: "none", pubStage: 0, pending: 0,
     badGo: false, earlyMs: false, lostFix: false, lostWork: false,
-    ranBlocked: false,
+    ranBlocked: false, badUnblock: false,
   }
 
   // ---- the operator ----------------------------------------------------------
@@ -237,15 +242,21 @@ module loop {
   }
 
   // Taking up a ready item: a fresh workspace on its project's build VM (D3)
-  // sets aside whatever is left there.
+  // sets aside whatever is left there. The check before it finds a VM out
+  // of reach, and blocks it instead (#137).
   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
+      val p = itm(s, i).project
+      val leftovers = s.items.keys().exists(j => j != i and itm(s, j).project == p
                                                   and itm(s, j).unpushed)
-      { ...s, active: i, lostWork: s.lostWork or leftovers,
-        ranBlocked: s.ranBlocked or s.vmBlocked.contains(itm(s, i).project) }
+      if (s.vmDown.contains(p))
+        { ...s, vmBlocked: s.vmBlocked.union(Set(p)),
+          vmUnreachable: s.vmUnreachable.union(Set(p)) }
+      else
+        { ...s, active: i, lostWork: s.lostWork or leftovers,
+          ranBlocked: s.ranBlocked or s.vmBlocked.contains(p) }
     },
   }
 
@@ -389,13 +400,15 @@ module loop {
   }
 
   // The build VM is wiped (D3): unpushed work on it is lost, accepted for
-  // the active item, never for a parked one.
+  // the active item, never for a parked one. Nor for an item cut off by its
+  // VM going out of reach (#137): that work couldn't be pushed, and the
+  // operator was told a reimage loses it.
   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) },
+      lostWork: s.lostWork or (not(s.vmUnreachable.contains(p)) and s.items.keys().exists(j =>
+        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
@@ -411,15 +424,47 @@ module loop {
     }
   }
 
-  // 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 {
+  // The build VM goes out of reach, or comes back (the world, #137).
+  action goDown(p: str): bool = s' = { ...s, vmDown: s.vmDown.union(Set(p)) }
+  action comeBack(p: str): bool = s' = { ...s, vmDown: s.vmDown.exclude(Set(p)) }
+
+  // A run finds its VM gone: it ends there, the item stays ready, and the
+  // VM is blocked. Its work stays on the VM, which isn't wiped.
+  action lostMidRun: bool = {
+    val it = itm(s, s.active)
+    all {
+      s.active != 0, s.work == "none", s.intents.size() == 0, it.status == "ready",
+      s.vmDown.contains(it.project),
+      s' = { ...s, active: 0,
+             vmBlocked: s.vmBlocked.union(Set(it.project)),
+             vmUnreachable: s.vmUnreachable.union(Set(it.project)) },
+    }
+  }
+
+  // A background probe (#137): a VM blocked for being out of reach is
+  // unblocked once it answers (and has settled, which the model leaves out).
+  // First the work a lost run left on it is parked (pushed).
+  action probe(p: str): bool = all {
+    s.vmUnreachable.contains(p),
+    not(s.vmDown.contains(p)),  // it answered
+    s' = { ...s,
+           items: s.items.keys().mapBy(j =>
+             if (itm(s, j).project == p) { ...itm(s, j), unpushed: false } else itm(s, j)),
+           vmBlocked: s.vmBlocked.exclude(Set(p)),
+           vmUnreachable: s.vmUnreachable.exclude(Set(p)),
+           badUnblock: s.badUnblock or s.vmDown.contains(p) },
+  }
+
+  // The operator's `vm ready`: the block lifts, after parking what a lost
+  // run left there. A reimage loses what wasn't pushed on the VM; the
+  // operator was told so, and agreed by doing it.
+  action vmReady(p: str): 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 },
+      vmUnreachable: s.vmUnreachable.exclude(Set(p)),
+      items: s.items.keys().mapBy(j =>
+               if (itm(s, j).project == p) { ...itm(s, j), unpushed: false } else itm(s, j)) },
   }
 
   // ---- crash and boot (L8) --------------------------------------------------
@@ -457,7 +502,8 @@ 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, requestReimage, vmReady(p, b),
+      finish, wipe(p), crash, requestReimage, vmReady(p),
+      goDown(p), comeBack(p), lostMidRun, probe(p),
     }
   }
 
@@ -506,10 +552,13 @@ module loop {
   // Nothing is taken up on a build VM that is blocked (D3).
   val blocked_vm_runs_nothing = not(s.ranBlocked)
 
+  // A VM blocked for being out of reach is unblocked only once it answers.
+  val unblocked_only_when_up = not(s.badUnblock)
+
   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,
+    blocked_vm_runs_nothing, unblocked_only_when_up,
   }
 
   // ---- reachability witnesses (each should be violated) --------------------------
@@ -520,5 +569,6 @@ module loop {
   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_vm_unreachable = s.vmUnreachable.size() == 0
   val w_finished = not(s.items.keys().exists(i => itm(s, i).status == "closed" and itm(s, i).ms > 0))
 }