Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Invariant Safety

Abstract

An inductive invariant makes every finitely reachable state safe.

Theorem 1.1 (Inductive invariants certify finite executions).

Proof. Machine-checked in Lean as D5/S0/Rewriting/Safety/InvariantSafety.invariant_safety (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let R be a transition relation, I0 the initial set, J an invariant, and S the safe set. The hypotheses expose all three invariant conditions: I0 is contained in J, J is contained in S, and every R-successor of a state in J remains in J.

A reflexive-transitive R path represents an arbitrary finite execution. Direct induction with Relation.ReflTransGen.head_induction_on propagates membership in J from the actual initial state to the endpoint, where containment in S gives safety.

The relation need not be deterministic, terminating or confluent. The conclusion concerns each finite path; it asserts no fairness or eventual completion.

A stronger conditional material-preservation model

Material-preserving operations illustrate how to obtain the one-step premise from effects rather than assuming safety of each successor. The following seven-effect model requires exhaustive preservation, absence of active users at a discarded location and continuous exclusion. These are stronger conditional premises, not eligibility requirements for worktree cleanup. Branch-backed deletion need not be a transition of this stronger relation, which requires remote support for every discarded pair. Let M, P and J be arbitrary types of immutable material versions, recovery locations and actual jobs. A state has required material R, confirmed remote material D, local support L in M times P, active use U in J times P, and qualified exclusion holders H in J times P. These are mathematical observations of one realization, not an additional stored record. An item is recoverable when it is in D or has some support in L. Safety requires this for every item of R.

A location p is held when some pair (j,p) belongs to H. Qualification at p means that every material item supported there is in D and no job has active use there. This checks all discarded support, including support for items outside R. The stronger invariant combines safety with qualification of every held location. Locations may denote a directory, a branch/object store or another affected resource; they are not necessarily whole trees. The material relation represents protected obligations and recovery effects; it does not make every intermediate keystroke a permanently required historical version. Mapping an actual edit requires identifying the still-required items and their genuine reconstruction supports.

The elementary relation has seven effects. Entry adds (j,p) to U only when p is not held. Production at an active, unheld location adds a new required version m together with support (m,p). Confirmation adds m to D. Acquisition adds (j,p) to H at an unheld, qualified location. Inheritance adds (k,p) to H from an existing holder (j,p). Exit removes only pairs labelled by the exiting job from U and H. A destructive effect at a held p removes the pairs (m,p) for m in an arbitrary selected cut, without changing R or D. No effect takes safety or the stronger invariant as its enabling condition. Acquisition denotes the final qualification boundary of an operation already protected by real exclusion, rather than a lock-system call. Preliminary lock acquisition or failed inspection authorizes no destructive effect and must leave material intact; it contributes no qualified holder to H.

Each effect preserves the stronger invariant by set membership laws. Production supplies the new item’s local witness. Confirmation only enlarges remote retention. Entry and production cannot affect a held location. Acquisition supplies qualification at its new location; inheritance obtains it from the parent holder. Exit removes activity and holders while retaining all material. Destruction leaves an old support witness unless it cuts that pair; in that case qualification supplies remote retention of the item. It also only shrinks the support set, so every surviving held location stays qualified. Applying invariant_safety to this relation, with the stronger invariant as both J and S, proves preservation through every finite interleaving of these seven effects, including a prefix interrupted between destructive effects.

Exclusion is continuous in this stronger argument. While any holder at p survives, new entry and new material production at p are disabled, and confirmed retention is unchanged or enlarged. After the last holder exits, further destruction requires a fresh acquisition and qualification. Partial destruction therefore needs no rollback assumption. A one-time sample without exclusion has a countermodel: start with an empty qualified location, admit a writer, produce one unconfirmed item there, then delete its sole support using the obsolete sample. The final state loses a required item.

The allowed relation also has nonempty successful cases. A location supporting a remotely retained item can be qualified and removed while a different location has an active writer and an unconfirmed item. A child inheriting the first location’s exclusion can survive the parent’s exit and perform the destructive effect. Its later exit releases the last holder. Thus preservation permits concurrent work, recovery and actual disposal; it does not require permanent refusal.

Ordinary snapshots and branch-backed recovery

An ordinary Git checkpoint stages the current working snapshot with git add -A and commits it on the current branch. Tracked files and ordinary untracked files follow native Git ignore rules. Pre-existing staged versions are replaced by current working values; ignored files and intermediate staged versions are not preservation obligations. Unmerged entries and unfinished operations are refused before staging. A clean snapshot needs no empty commit. Native hooks, index locks and ref updates retain their normal failure semantics.

For removal, the required material is the successful commit’s tracked snapshot and reachable history. Its local support is the surviving branch reference together with the common repository’s reachable Git objects, outside the removed checkout. Removing only the checkout does not remove that support. This is the surviving-witness case of the inductive-invariant argument: each permitted deletion retains a support witness for every required item. Automatic cleanup retains task and recovery branches without a branch sweep. Native git worktree add on the retained branch reconstructs its tracked snapshot, subject to intact objects and normal checkout semantics. Neither a remote nor publication confirmation is needed for this local route. Detached HEAD acquires a new local branch at the checkpoint commit before deletion. A failed checkpoint or branch creation retains the tree. Later deletion of the branch or object store is outside this guarantee.

Cooperative workers may edit one checkout concurrently. Snapshot claims require coordination while Git consumes the working files, index and current branch; operation scopes end with OS descriptor lifetime. They impose no session-long writer lease. Changes made after staging belong to a later snapshot. Disjoint writes alone do not imply semantic independence: D5/S3/ConceptDynamics/Governance/TwoStateLocalityIncrementalPreservation.two_state_locality_yields_incremental_preservation applies only when the target and both actual read sets remain equal. D5/S0/Rewriting/HindleyRosen.reflTransGen_commute_of_strong_commute concerns finite blocks with commuting squares, not a merge procedure for overlapping edits. Native fixtures establish the Git correspondence; the abstract invariant theorem does not verify Git or OS behavior.

Exit, durability and the realization boundary

In the conditional model, for distinct jobs j and k, exit of j leaves every active-use and holder pair labelled k unchanged. An inherited descriptor is represented by a holder pair for the child, rather than by the parent’s continued existence. Exit also leaves R, D and L unchanged. Even an exit leaving no activity and no exclusion holder can leave a required item only locally supported. Automatic release establishes no publication.

For finite material sets, D5/S3/ConceptDynamics/OperationalTuition/ArtifactSufficiencyAndKillLoss.artifact_sufficient_iff_every_kill_zero_byte_loss gives the separate complete-local-loss boundary: with artifact set D and session set equal to all local material, zero required loss after erasing the latter is equivalent to R being contained in D. Its insufficiency direction exhibits nonempty loss. In this application local Git commits belong to local support until confirmation, even though they are persistent on local disk. A single participant’s exit does not perform this erasure. For the actual recovery guarantee, R can be the authorized commit units whose remote retention has been confirmed. Then R is contained in D, so loss of all local support leaves those units recoverable. If R also includes local-only items, the complete-local-loss conclusion need not hold. Removing a checkout while retaining its branch and objects is not complete local loss.

Remote support means a genuine reconstruction route, including required metadata and object dependencies. Publication resolves the named remote’s push destination; push and fresh confirmation refer to the same endpoint. Multiple push destinations are refused before writing. Confirmation observes a remote branch tip and establishes that the required exact commit is that tip or an ancestor of it. A successful process exit, push invocation or stale tracking ref is insufficient. Retention must remain valid through each recovery relying on it. Rebuilding additionally depends on the complete reconstruction relation and the required toolchain; confirmation alone promises neither future remote availability nor reconstruction progress.

Cooperative editing protects overlapping writes and actual semantic reads; compound Git operations coordinate their affected index and ref scopes. Disjoint editing remains concurrent. OS descriptor lifetime releases operation exclusion without an LLM unlock; children that continue a protected operation must retain its descriptors or enter the protocol themselves. Normal finalization follows host joining of this task’s writers, checkpoints the ordinary working snapshot and confirms publication. Other participants can continue. Abnormal exit and lock release establish no publication fact. These scoped coordination premises do not create a session-long writer lease or a deletion-exclusion requirement.

Actual worktree disposal uses user-directed selection and the Git lock/time rule: a selected unlocked tree may be removed; a locked tree requires the existing 24-hour lock duration. Automatic selection has its own Git-update age and behind-count conditions, which named removal bypasses. Target identity, main-tree protection, nested registration checks and accurate partial-failure reporting remain. Active programs, cwd, open resources, protocol participation, cache use and remote confirmation do not qualify or veto deletion. Eligible registered trees first commit outstanding ordinary changes, then retain the current branch or create a recovery branch for detached HEAD; deletion requires this support. The recovery branch survives the entire invocation. Ordinary non-worktree artifacts retain their independent policy. The stronger seven-effect argument does not certify this eligibility rule; local branch recovery and remote-confirmed durability have distinct premises. No mathematical statement here verifies the Git/OS realization, eventual publication or fairness.

References