Check host coordinator domain ownership

Add a TLC-checked invariant requiring any Host Coordinator process record to belong to a non-absent, lock-held Domain. Include the invariant in the aggregate safety operator and remove journal-only markers from protocol model comments so the model remains grounded in product vocabulary.

docs/protocol/Lazaret.cfg

@@ -66,6 +66,7 @@ INVARIANTS
     SupervisorLeaseConsistency
     RuntimeResourceOwnership
     CoordinatorPhysicalConsistency
+    HostCoordinatorRequiresDomainOwnership
     NoVanishPresentRuntime
     OrderedLeaseTeardown
     DomainGenerationBounds

docs/protocol/Lazaret.tla

@@ -10,10 +10,10 @@ resource preparation owned by the supervisor; Host Coordinator lifetime lease;
 role-separated runtime identity tuples; sandbox launch isolation; Client Session
 registration; host escalation; correlated result delivery; terminal ownership;
 failure; lease-driven teardown; recovery; and abstract durable generation-document
-intent with mismatch refuse (DR-M3 vocabulary).
+intent with mismatch refuse.
 
 Product names SessionCoordinatorPresent and Session Coordinator ID alias the
-existing multi-process predicates and DomainCoordinatorIdentity fixture (SC1–SC3).
+multi-process predicates and DomainCoordinatorIdentity fixture.
 Cryptographic algorithms, serialization, container commands, filesystems, typed
 redb tables, and network packet handling are refinement boundaries.
 ***************************************************************************)
@@ -119,7 +119,6 @@ PhysicalProcessStates == {"Absent", "Alive", "Stopped", "Dead"}
 RuntimeCausalEdgeStates == {"Unarmed", "Armed"}
 SupervisorLeaseStates == {"Unarmed", "Held", "Lost"}
 MaxDomainGeneration == 4
-\* DR-M3 generation-document decision lifecycle (abstract; not typed redb tables).
 DurableDecisions == {"None", "Preparing", "Published", "Clean"}
 SessionPhases == {
     "New", "Waiting", "Registering", "Attached", "Prompting",
@@ -308,7 +307,6 @@ RuntimeLogicalAuthorityPresent(d) ==
     \/ ProcessPresent(runtimeSupervisorProc[d])
     \/ ProcessPresent(attachedRunscProc[d])
 
-\* Multi-process Session Coordinator product vocabulary (saga 18 SC1–SC3).
 \* Constitutive processes: Host Coordinator (protocol face), Runtime Supervisor,
 \* attached runsc. Present = Alive or Stopped; Dead/Absent do not count.
 SessionCoordinatorPresent(d) == RuntimeLogicalAuthorityPresent(d)
@@ -316,7 +314,7 @@ SessionCoordinatorAbsent(d) == ~SessionCoordinatorPresent(d)
 \* SandboxRunning(d) ≜ sandboxState[d] = "Ready"
 \* Coupling: SandboxRunning(d) ⇒ SessionCoordinatorPresent(d)
 
-\* SC3: one logical SC ID per instance; fixture DomainCoordinatorIdentity is not
+\* One logical Session Coordinator ID per instance; fixture DomainCoordinatorIdentity is not
 \* reminted on domainGeneration. HC alone serves session-control Protocol Identity.
 SessionCoordinatorIdentity(d) == DomainCoordinatorIdentity[d]
 SessionCoordinatorProtocolFaceAlive(d) == HostCoordinatorAlive(d)
@@ -640,8 +638,8 @@ StartSandbox(d) ==
     /\ SandboxCertificateValid[d]
     /\ ~durableSandboxIntent[d]
     /\ ~pathMismatch[d]
-    \* Durable sandbox Intent is recorded with the generation document before the
+    \* Intent and external creation are one abstract step here; implementations
-    \* external sandbox create completes (DR-M3 intent-before-create).
+    \* must persist Intent before the resource can outlive the caller.
     /\ durableSandboxIntent' = [durableSandboxIntent EXCEPT ![d] = TRUE]
     /\ durableDecision' = [durableDecision EXCEPT ![d] = "Preparing"]
     /\ sandboxState' = [sandboxState EXCEPT ![d] = "Ready"]
@@ -1557,7 +1555,7 @@ RecoverSandbox(d) ==
     /\ ~pathMismatch[d]
     /\ \/ sandboxState[d] # "Stopped"
        \/ attachedRunscProc[d] = "Dead"
-    \* Exact-owned Ready sandbox cleanup requires durable intent (DR-M3).
+    \* Exact-owned Ready sandbox cleanup requires durable intent.
     /\ (sandboxState[d] # "Stopped" => durableSandboxIntent[d])
     /\ sandboxState' = [sandboxState EXCEPT ![d] = "Stopped"]
     /\ attachedRunscProc' = [attachedRunscProc EXCEPT ![d] = "Absent"]
@@ -1637,7 +1635,7 @@ FinishRecovery(d) ==
     /\ durableDecision' = [durableDecision EXCEPT ![d] = "Clean"]
     /\ durableSandboxIntent' = [durableSandboxIntent EXCEPT ![d] = FALSE]
     \* Drop generation-document observation of path leftovers; physical foreign
-    \* leftovers remain outside the model (SC6 unpublished leftovers).
+    \* leftovers remain outside the model.
     /\ pathMismatch' = [pathMismatch EXCEPT ![d] = FALSE]
     /\ UNCHANGED <<
         stateAnchorState, sidecarState, sandboxState, published,
@@ -1649,7 +1647,7 @@ FinishRecovery(d) ==
 
 
 (***************************************************************************
-Durable generation document / mismatch refuse (DR-M3 / FM4 abstract)
+Durable generation document and mismatch refuse
 
 pathMismatch abstracts wrong-owner or missing-intent observation at the
 deterministic sandbox path. Refuse leaves the claim in place; recovery never
@@ -1878,6 +1876,12 @@ CoordinatorPhysicalConsistency ==
         /\ (domainPhase[d] = "Recovering" => HostCoordinatorAlive(d))
         /\ (hostCoordinatorProc[d] = "Dead" => domainPhase[d] = "Failed")
 
+HostCoordinatorRequiresDomainOwnership ==
+    \A d \in Domains :
+        hostCoordinatorProc[d] # "Absent" =>
+            /\ domainPhase[d] # "Absent"
+            /\ domainLockHeld[d]
+
 ExclusiveBootstrapOwnership ==
     \A d \in Domains : lockOwner[d] # NoSession =>
         /\ domainPhase[d] = "Starting"
@@ -2013,7 +2017,6 @@ DomainGenerationBounds ==
         /\ domainGeneration[d] \in 0..MaxDomainGeneration
         /\ (domainPhase[d] # "Absent" => domainGeneration[d] > 0)
 
-\* DR-M3 / FM4: Ready sandbox implies durable sandbox Intent was recorded.
 DurableIntentBeforeSandboxReady ==
     \A d \in Domains :
         sandboxState[d] = "Ready" => durableSandboxIntent[d]
@@ -2055,6 +2058,7 @@ Safety ==
     /\ SupervisorLeaseConsistency
     /\ RuntimeResourceOwnership
     /\ CoordinatorPhysicalConsistency
+    /\ HostCoordinatorRequiresDomainOwnership
     /\ NoVanishPresentRuntime
     /\ OrderedLeaseTeardown
     /\ DomainGenerationBounds