Define prepared-lower lease and reclaim invariants

docs/protocol/PreparedLower.cfg

@@ -0,0 +1,20 @@
+CONSTANTS
+    G1 = g1
+    G2 = g2
+    A1 = a1
+    NoArtifact = noArtifact
+    Generations <- GenerationsFixture
+    Artifact = a1
+
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    LeaseBindingConsistent
+    MountedGenerationLeased
+    LeasedArtifactPublished
+    GCExcludesLeases
+    ReplacementOnlyDuringGC
+    ForeignStagePreserved
+    OwnedStageRequiresIntent

docs/protocol/PreparedLower.tla

@@ -0,0 +1,221 @@
+------------------------- MODULE PreparedLower -------------------------
+EXTENDS FiniteSets, TLC
+
+(***************************************************************************
+Artifact-level refinement for prepared-lower publication, generation leases,
+State Anchor use, exact-owned abandoned preparation recovery, and reclaim.
+***************************************************************************)
+
+CONSTANTS
+    Generations,
+    Artifact,
+    NoArtifact,
+    G1,
+    G2,
+    A1
+
+ASSUME
+    /\ Generations = {G1, G2}
+    /\ G1 # G2
+    /\ Artifact = A1
+    /\ NoArtifact # Artifact
+
+ArtifactStates == {"Absent", "Published"}
+StageStates == {"Absent", "Owned", "Foreign"}
+GenerationsFixture == {G1, G2}
+
+VARIABLES
+    artifactState,
+    stageState,
+    prepareIntent,
+    leases,
+    mounts,
+    artifactBinding,
+    gcRequested,
+    replacementPresent,
+    foreignObserved
+
+vars == <<
+    artifactState,
+    stageState,
+    prepareIntent,
+    leases,
+    mounts,
+    artifactBinding,
+    gcRequested,
+    replacementPresent,
+    foreignObserved
+>>
+
+Init ==
+    /\ artifactState = "Absent"
+    /\ stageState = "Absent"
+    /\ prepareIntent = FALSE
+    /\ leases = {}
+    /\ mounts = {}
+    /\ artifactBinding = [g \in Generations |-> NoArtifact]
+    /\ gcRequested = FALSE
+    /\ replacementPresent = FALSE
+    /\ foreignObserved = FALSE
+
+BeginPrepare ==
+    /\ artifactState = "Absent"
+    /\ stageState = "Absent"
+    /\ ~prepareIntent
+    /\ prepareIntent' = TRUE
+    /\ UNCHANGED <<artifactState, stageState, leases, mounts,
+        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
+
+CreateOwnedStage ==
+    /\ artifactState = "Absent"
+    /\ stageState = "Absent"
+    /\ prepareIntent
+    /\ stageState' = "Owned"
+    /\ UNCHANGED <<artifactState, prepareIntent, leases, mounts,
+        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
+
+PublishArtifact ==
+    /\ artifactState = "Absent"
+    /\ stageState = "Owned"
+    /\ prepareIntent
+    /\ artifactState' = "Published"
+    /\ stageState' = "Absent"
+    /\ prepareIntent' = FALSE
+    /\ UNCHANGED <<leases, mounts, artifactBinding, gcRequested,
+        replacementPresent, foreignObserved>>
+
+RecoverOwnedStage ==
+    /\ artifactState = "Absent"
+    /\ stageState = "Owned"
+    /\ prepareIntent
+    /\ stageState' = "Absent"
+    /\ prepareIntent' = FALSE
+    /\ UNCHANGED <<artifactState, leases, mounts, artifactBinding,
+        gcRequested, replacementPresent, foreignObserved>>
+
+ObserveForeignStage ==
+    /\ artifactState = "Absent"
+    /\ stageState = "Absent"
+    /\ ~prepareIntent
+    /\ stageState' = "Foreign"
+    /\ foreignObserved' = TRUE
+    /\ UNCHANGED <<artifactState, prepareIntent, leases, mounts,
+        artifactBinding, gcRequested, replacementPresent>>
+
+RefuseForeignStage ==
+    /\ stageState = "Foreign"
+    /\ UNCHANGED vars
+
+AcquireLease(g) ==
+    /\ artifactState = "Published"
+    /\ ~gcRequested
+    /\ g \notin leases
+    /\ leases' = leases \cup {g}
+    /\ artifactBinding' = [artifactBinding EXCEPT ![g] = Artifact]
+    /\ UNCHANGED <<artifactState, stageState, prepareIntent, mounts,
+        gcRequested, replacementPresent, foreignObserved>>
+
+MountStateAnchor(g) ==
+    /\ g \in leases
+    /\ artifactBinding[g] = Artifact
+    /\ g \notin mounts
+    /\ mounts' = mounts \cup {g}
+    /\ UNCHANGED <<artifactState, stageState, prepareIntent, leases,
+        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
+
+UnmountStateAnchor(g) ==
+    /\ g \in mounts
+    /\ mounts' = mounts \ {g}
+    /\ UNCHANGED <<artifactState, stageState, prepareIntent, leases,
+        artifactBinding, gcRequested, replacementPresent, foreignObserved>>
+
+ReleaseLease(g) ==
+    /\ g \in leases
+    /\ g \notin mounts
+    /\ leases' = leases \ {g}
+    /\ artifactBinding' = [artifactBinding EXCEPT ![g] = NoArtifact]
+    /\ UNCHANGED <<artifactState, stageState, prepareIntent, mounts,
+        gcRequested, replacementPresent, foreignObserved>>
+
+RequestGC ==
+    /\ artifactState = "Published"
+    /\ leases = {}
+    /\ ~gcRequested
+    /\ gcRequested' = TRUE
+    /\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, mounts,
+        artifactBinding, replacementPresent, foreignObserved>>
+
+PublishReplacementDuringGC ==
+    /\ artifactState = "Published"
+    /\ gcRequested
+    /\ ~replacementPresent
+    /\ replacementPresent' = TRUE
+    /\ UNCHANGED <<artifactState, stageState, prepareIntent, leases, mounts,
+        artifactBinding, gcRequested, foreignObserved>>
+
+ReclaimArtifact ==
+    /\ artifactState = "Published"
+    /\ gcRequested
+    /\ leases = {}
+    /\ mounts = {}
+    /\ artifactState' = IF replacementPresent THEN "Published" ELSE "Absent"
+    /\ gcRequested' = FALSE
+    /\ replacementPresent' = FALSE
+    /\ UNCHANGED <<stageState, prepareIntent, leases, mounts,
+        artifactBinding, foreignObserved>>
+
+Next ==
+    \/ BeginPrepare
+    \/ CreateOwnedStage
+    \/ PublishArtifact
+    \/ RecoverOwnedStage
+    \/ ObserveForeignStage
+    \/ RefuseForeignStage
+    \/ (\E g \in Generations : AcquireLease(g))
+    \/ (\E g \in Generations : MountStateAnchor(g))
+    \/ (\E g \in Generations : UnmountStateAnchor(g))
+    \/ (\E g \in Generations : ReleaseLease(g))
+    \/ RequestGC
+    \/ PublishReplacementDuringGC
+    \/ ReclaimArtifact
+
+Spec == Init /\ [][Next]_vars
+
+TypeOK ==
+    /\ artifactState \in ArtifactStates
+    /\ stageState \in StageStates
+    /\ prepareIntent \in BOOLEAN
+    /\ leases \subseteq Generations
+    /\ mounts \subseteq Generations
+    /\ artifactBinding \in [Generations -> {NoArtifact, Artifact}]
+    /\ gcRequested \in BOOLEAN
+    /\ replacementPresent \in BOOLEAN
+    /\ foreignObserved \in BOOLEAN
+
+LeaseBindingConsistent ==
+    \A g \in Generations :
+        (g \in leases) <=> (artifactBinding[g] = Artifact)
+
+MountedGenerationLeased ==
+    /\ mounts \subseteq leases
+    /\ \A g \in mounts : artifactBinding[g] = Artifact
+
+LeasedArtifactPublished ==
+    leases # {} => artifactState = "Published"
+
+GCExcludesLeases ==
+    gcRequested =>
+        /\ artifactState = "Published"
+        /\ leases = {}
+        /\ mounts = {}
+
+ReplacementOnlyDuringGC ==
+    replacementPresent => gcRequested
+
+ForeignStagePreserved ==
+    foreignObserved => stageState = "Foreign"
+
+OwnedStageRequiresIntent ==
+    stageState = "Owned" => prepareIntent
+
+=============================================================================

docs/specification.md

@@ -282,15 +282,21 @@ Anchor lower. Archive export alone is not a complete preparation boundary;
 container tooling may participate only as transport into Lazaret-owned
 preparation. Ad hoc unsupported tar extractors are not a production preparer.
 
-Protocol prepared-lower lease, intent, and refuse-while-leased reclaim follow the
+Prepared-artifact identity is independent of its storage pathname. Before State
-protocol model. Product encoding binds a lease to prepared-artifact ID (and
+Anchor mount, Host Coordinator durable state binds the Domain generation to the
-generation identity) under Host Coordinator durable state—not an engine mount
+prepared-artifact ID with a prepared-lower lease. Distinct generations sharing
-refcount. Distinct Domain generations may share one prepared-artifact ID only
+an artifact hold separate leases; an engine mount refcount is not a lease.
-through separate protocol leases. Concurrent preparation of the same source may
+
-reuse a completed artifact or create a new prepared-artifact ID; an in-progress
+Concurrent preparation of the same source may reuse a completed artifact or
-prepare tree is not a State Anchor lower. After the last lease for an artifact
+publish a new prepared-artifact ID. An incomplete preparation is never a State
-drops, product GC may reclaim that tree; foreign trees under deterministic paths
+Anchor lower. Preparation, lease acquisition, and reclaim serialize so GC acts
-must not be deleted.
+only after the final lease is released. Recovery may reclaim an abandoned
+preparation only from matching exact-owned durable intent; foreign or mismatched
+trees remain untouched.
+
+The prepared rootfs preserves OCI modes and is exposed only as a read-only State
+Anchor lower. Lazaret enforces immutability through artifact ownership and
+lifecycle rather than by rewriting image permission bits.
 
 #### Durable generation document
 
@@ -456,7 +462,7 @@ follow a symlink outside the Domain Root.
 | **FR-19** | The Host Coordinator shall derive generation-bound network policy from trusted host configuration; the Runtime Supervisor shall install only that derived policy and attest readiness by observed namespace state. Durable network participant state shall record the network readiness fingerprint. |
 | **FR-20** | Before publication, Lazaret shall verify from the Agent Sandbox network view, or an equivalent generation-bound probe using the same enforcement namespace, that default-denied private destinations are unreachable and that required permitted reachability including selected DNS resolvers works. |
 | **FR-21** | The durable generation document encoding shall include schema/db version, generation identity, minted runtime component IDs, model-governed durable decision and participant intent, and ownership material for product recovery. Unknown newer schema versions shall fail closed until an explicit Host Coordinator migration runs. |
-| **FR-22** | Preparation shall use a supported OCI-aware preparer that materialises a Lazaret-owned immutable rootfs with source identity and prepared-artifact ID. Protocol prepared-lower lease rules apply before State Anchor mount. |
+| **FR-22** | Preparation shall use a supported OCI-aware preparer that materialises a Lazaret-owned immutable rootfs with source identity and prepared-artifact ID. A durable generation-bound prepared-lower lease shall exist before State Anchor mount. |
 
 ### 4.3 Developer-Experience Requirements
 
@@ -479,4 +485,4 @@ follow a symlink outside the Domain Root.
 | **OR-4** | Security-sensitive behavior shall be covered by integration tests on supported runsc, filesystem, and network configurations. Test evidence belongs in the journal. |
 | **OR-5** | An interrupted State Anchor reset shall recover to either the prior generation or a new empty generation; it shall not leave a partially reset active upper layer. |
 | **OR-6** | Lazaret shall not require a persistent global daemon or multi-Domain resident process that holds mutable runtime authority across Domains. Per-Domain authority shall be scoped by Domain ID, generation, configuration fingerprint, role identity, and exact physical ownership. |
-| **OR-7** | After protocol leases for a prepared-artifact ID are released, product GC may reclaim that tree. Shared-artifact reclaim must wait until no lease remains for that artifact. In-progress prepare trees and foreign trees must not be deleted except through fail-closed recovery of exact-owned prepare intent. |
+| **OR-7** | Product GC shall provide policy-controlled reclamation for prepared artifacts after all protocol leases for the prepared-artifact ID are released. Shared-artifact reclaim shall wait until no lease remains for that artifact. In-progress prepare trees and foreign trees shall not be deleted; exact-owned abandoned prepare trees may be reclaimed only through fail-closed recovery backed by durable prepare intent. |