schema = 1

[[model]]
name = "Lazaret"
module = "docs/protocol/Lazaret.tla"
config = "docs/protocol/Lazaret.cfg"
action_aggregates = ["Next", "DomainServiceProgress", "RuntimePhysicalInterleaving", "RequestProgress"]

[[model]]
name = "PreparedLower"
module = "docs/protocol/PreparedLower.tla"
config = "docs/protocol/PreparedLower.cfg"
action_aggregates = ["Next"]

[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["StartNewDomain", "StartReadySession", "WaitForDomain", "RestartWaitingDomain", "AdvanceWaitingSession", "RejectConfigurationMismatch", "RegisterSession", "DisconnectSession"]
owners = ["IP-30", "IP-31"]
levels = ["V1", "V3"]
verifier = "Deterministic lifecycle adapters and the IP-40 cold-start slice"

[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["CreateTrustAnchor"]
owners = ["IP-23", "IP-30"]
levels = ["V2", "V3"]
verifier = "Credential/control physical tests and generation publication"

[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["StartRuntimeSupervisor", "LeasePreparedLower", "MountStateAnchor", "StartSidecar", "StartConnectivityHelper", "MarkNetworkReady", "ArmRuntimeCausalEdge", "StartSandbox", "PublishDomain"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-14", "IP-15", "IP-16", "IP-21", "IP-22", "IP-23", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Component tests, the IP-21 composition harness, and IP-40"

[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["BeginTeardown", "StopSandbox", "StopSidecar", "UnmountStateAnchor", "ReleasePreparedLowerLease", "GracefulSupervisorExit", "FinishTeardown"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Lifecycle adapters and IP-40 normal teardown"

[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["FailDomain", "HostCoordinatorTerminateUnresponsiveRuntime", "LeaseTeardownStopSandbox", "LeaseTeardownStopSidecar", "LeaseTeardownUnmountStateAnchor", "LeaseTeardownSupervisorExit", "ExternalReapStoppedSupervisorAfterHcLoss", "BootstrapRecoveryCoordinator", "BeginRecovery", "RecoverSandbox", "RecoverSidecar", "RecoverStateAnchor", "RecoverPreparedLowerLease", "FinishRecovery"]
owners = ["IP-21", "IP-22", "IP-32"]
levels = ["V2", "V4"]
verifier = "Causal-loss tests and the recovery failpoint matrix"

[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["HardLoseHostCoordinator", "HardLoseRuntimeSupervisor", "HardLoseAttachedRunsc", "HardLoseConnectivityHelper", "StopHostCoordinatorProcess", "ResumeHostCoordinatorProcess", "StopRuntimeSupervisorProcess", "ResumeRuntimeSupervisorProcess", "StopAttachedRunscProcess", "ResumeAttachedRunscProcess", "ObservePathMismatch", "RefusePathMismatchCleanup", "RefusePreparedLowerReclaim"]
owners = ["IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-32"]
levels = ["V2", "V4"]
verifier = "Physical mismatch, stop, loss, and hostile-failure cases"

[[coverage]]
model = "Lazaret"
kind = "action"
symbols = ["ReceiveEscalation", "AutoApprove", "QueuePrompt", "BeginPrompt", "DeveloperApprove", "DeveloperDeny", "StartHostExecution", "CompleteHostExecution", "TimeoutRequest", "CancelRequest", "FailHostExecution", "DeliverResult"]
owners = ["IP-15", "IP-24", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Protocol tests, the IP-43 slice, and hostile-loss cases"

[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["TypeOK", "DomainGenerationBounds", "RuntimeRoleIdentitySeparation", "GenerationScopedIdentitiesDistinct"]
owners = ["IP-01", "IP-10", "IP-14", "IP-15", "IP-30"]
levels = ["V1"]
verifier = "IP-01 strict schema-codec, malformed-version, record-invariant, and nominal identity tests plus later lifecycle state assertions"

[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["ConfigurationConfinement", "SandboxNamespaceIsolation", "OrderedNetworkStartup", "NetworkReadyBeforePublish"]
owners = ["IP-02", "IP-14", "IP-16", "IP-20", "IP-21", "IP-22", "IP-30"]
levels = ["V1", "V2", "V3"]
verifier = "Builders/codecs, physical isolation, and IP-40/IP-41"

[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["PublishedDomainsReady", "DomainLockLifetime", "RuntimeCausalEdgeArmedBeforeSandbox", "RuntimeCausalEdgeOwnerPresent", "SandboxRunningImpliesCoordinatorPresent", "PublishedRuntimeAuthorityPresent", "SupervisorLeaseConsistency", "RuntimeResourceOwnership", "CoordinatorPhysicalConsistency", "HostCoordinatorRequiresDomainOwnership", "NoVanishPresentRuntime", "StateAnchorOwnership", "HelperUnderSupervisor"]
owners = ["IP-10", "IP-13", "IP-21", "IP-22", "IP-30", "IP-32"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Lifecycle adapters, causal harnesses, and IP-44"

[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["ExclusiveBootstrapOwnership", "TeardownNotJoinable", "RegisteredSessionsConnected", "AttachedSessionsValid", "TerminalIsolation"]
owners = ["IP-23", "IP-30", "IP-31", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3"]
verifier = "Control/session tests and IP-40/IP-42"

[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["AuthenticatedRequestsOnly", "RegisteredSessionIdentityUniqueness", "LiveRequestIdentityAuthorized", "DeveloperApprovalAuthenticated", "HostExecutionAuthorized", "AutoApprovalNoShell", "NoOrphanHostProcess", "ResultDeliveryStateConsistent"]
owners = ["IP-15", "IP-23", "IP-24", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Protocol tests, IP-43, and hostile-loss cases"

[[coverage]]
model = "Lazaret"
kind = "invariant"
symbols = ["OrderedLeaseTeardown", "DurableIntentBeforeSandboxReady", "DurableDecisionPublicationConsistent", "PathMismatchNotAdopted", "FailedDomainIsolation", "OrderedFailureRecovery", "MultiRoleDurableIntent", "PreparedLowerLeaseBeforeMount"]
owners = ["IP-10", "IP-11", "IP-12", "IP-13", "IP-21", "IP-22", "IP-30", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Transactional and failpoint tests plus IP-44"

[[coverage]]
model = "Lazaret"
kind = "property"
symbols = ["SessionEventuallyResolves", "RequestEventuallyResolves", "PromptEventuallyRestoresTerminal", "EmptyDomainEventuallyStops", "FailedDomainEventuallyRecovers"]
owners = ["IP-24", "IP-30", "IP-31", "IP-32", "IP-33", "IP-34"]
levels = ["V1", "V2", "V3", "V4"]
verifier = "Bounded progress tests, integrated slices, and TLC"

[[coverage]]
model = "Lazaret"
kind = "property"
symbols = ["LeaseLossUnmountRetainsPreparedLowerLease"]
owners = ["IP-10", "IP-11", "IP-13", "IP-21", "IP-30", "IP-32"]
levels = ["V2", "V4"]
verifier = "Lease-loss failpoints and TLC"

[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["BeginPrepare", "CreateOwnedStage", "PublishArtifact", "RecoverOwnedStage", "ObserveForeignStage", "RefuseForeignStage"]
owners = ["IP-12", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Preparer publication, ownership, and recovery tests"

[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["AcquireLease", "MountStateAnchor", "UnmountStateAnchor", "ReleaseLease"]
owners = ["IP-11", "IP-13", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Catalog and State Anchor lease lifecycle tests"

[[coverage]]
model = "PreparedLower"
kind = "action"
symbols = ["RequestGC", "PublishReplacementDuringGC", "ReclaimArtifact"]
owners = ["IP-11", "IP-12", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Concurrent publication and exact-owned reclamation tests"

[[coverage]]
model = "PreparedLower"
kind = "invariant"
symbols = ["TypeOK", "LeaseBindingConsistent", "MountedGenerationLeased", "LeasedArtifactPublished", "GCExcludesLeases", "ReplacementOnlyDuringGC", "ForeignStagePreserved", "OwnedStageRequiresIntent"]
owners = ["IP-11", "IP-12", "IP-13", "IP-32"]
levels = ["V1", "V2", "V4"]
verifier = "Catalog/preparer concurrency and recovery tests plus TLC"