perf(relay): compact Git packs before manifest limits (#2172)

crates/buzz-relay/src/api/git/manifest.rs

@@ -37,6 +37,12 @@ pub const MANIFEST_VERSION: u32 = 1;
 /// Hydration indexes packs one at a time, but an unbounded pack list still
 /// turns one request into unbounded object-store and git subprocess work.
 pub const MAX_MANIFEST_PACKS: usize = 128;
+/// Pack count that triggers proactive consolidation during the next accepted push.
+///
+/// Keeping one quarter of the manifest capacity in reserve prevents a hot
+/// repository from reaching the hard limit while a prior compaction attempt
+/// falls back to the normal delta-pack path.
+pub const PACK_COMPACTION_THRESHOLD: usize = MAX_MANIFEST_PACKS * 3 / 4;
 /// Maximum number of refs one manifest may advertise.
 pub const MAX_MANIFEST_REFS: usize = 10_000;
 

crates/buzz-relay/src/metrics.rs

@@ -97,6 +97,11 @@ pub fn install(port: u16, gauge_idle_timeout_secs: u64) {
             &GIT_DURATION_BUCKETS_S,
         )
         .expect("valid git cache population wait bucket boundaries")
+        .set_buckets_for_metric(
+            Matcher::Full("buzz_git_pack_compaction_seconds".to_owned()),
+            &GIT_DURATION_BUCKETS_S,
+        )
+        .expect("valid git compaction duration bucket boundaries")
         .set_buckets_for_metric(
             Matcher::Full("buzz_git_hydrate_bytes".to_owned()),
             &GIT_BYTES_BUCKETS,
@@ -107,11 +112,26 @@ pub fn install(port: u16, gauge_idle_timeout_secs: u64) {
             &GIT_BYTES_BUCKETS,
         )
         .expect("valid git stream byte bucket boundaries")
+        .set_buckets_for_metric(
+            Matcher::Full("buzz_git_pack_compaction_bytes".to_owned()),
+            &GIT_BYTES_BUCKETS,
+        )
+        .expect("valid git compaction byte bucket boundaries")
         .set_buckets_for_metric(
             Matcher::Full("buzz_git_hydrate_packs".to_owned()),
             &GIT_PACK_BUCKETS,
         )
         .expect("valid git pack-count bucket boundaries")
+        .set_buckets_for_metric(
+            Matcher::Full("buzz_git_pack_compaction_packs_before".to_owned()),
+            &GIT_PACK_BUCKETS,
+        )
+        .expect("valid git compaction input pack-count bucket boundaries")
+        .set_buckets_for_metric(
+            Matcher::Full("buzz_git_pack_compaction_packs_after".to_owned()),
+            &GIT_PACK_BUCKETS,
+        )
+        .expect("valid git compaction output pack-count bucket boundaries")
         .set_buckets_for_metric(Matcher::Suffix("_seconds".to_owned()), &DURATION_BUCKETS_S)
         .expect("valid seconds bucket boundaries")
         .set_buckets_for_metric(

docs/git-on-object-storage.md

@@ -285,24 +285,28 @@ against a pinned minimum `git` ≥ 2.31, the first release with `git index-pack
 --fsck-objects` defaults relied on here). It remains
 to show `manifest(d).packs` *covers* the reachable closure of `m.refs`. By
 induction on the push chain: the empty repo's manifest names ∅ and refs ∅
-(covered vacuously). Step 5 sets `m_after.packs = m_before.packs ∪ keys(O)` where
-`O` is every object this push introduced; and `m_after.refs` only points at
-objects in `m_before.refs`' closure (unchanged or deleted refs) or in `O` (new or
-force-moved refs). So every object reachable from `m_after.refs` is in
-`m_before.packs` (covered by IH) or in `keys(O)` — hence in `m_after.packs`. ∎
+(covered vacuously). A normal step sets
+`m_after.packs = m_before.packs ∪ keys(O)` where `O` is every object this push
+introduced; and `m_after.refs` only points at objects in `m_before.refs`'
+closure (unchanged or deleted refs) or in `O` (new or force-moved refs). A
+compaction step instead feeds every `m_after.refs` tip to `git pack-objects
+--revs` with no negative revisions, then names only the resulting bounded pack
+set. The normal case preserves coverage by induction; the compaction case
+re-establishes coverage directly from the complete post-push ref closure. ∎
 
 **Remark (force-push, delete, and GC).** Coverage is a *superset*, not equality,
 and that is the correct invariant. A delete-ref drops a key from `m.refs`; a
-force-push repoints a ref off its old history. Neither removes packs from
-`m.packs`, so objects reachable only from the old/deleted ref become unreachable
+force-push repoints a ref off its old history. Neither normal ref operation
+removes packs from `m.packs`, so objects reachable only from the old/deleted ref become unreachable
 but remain named. This is safe — reconstruction of the *current* refs is
-unaffected — but it means `m.packs` grows monotonically under the protocol as
-specified. Garbage collection (computing reachability from `m.refs` and
-publishing a manifest with a pruned pack set) is a separate, *also CAS-guarded*
-operation: it is just another `Push` whose `m_after` happens to name fewer packs,
-so Theorems 1 and 3 apply to it unchanged. GC correctness (that it never prunes a
-reachable pack) is an obligation on the GC's reachability computation, out of
-scope here and called out as future work.
+unaffected. Before the bounded manifest reaches its pack limit, an accepted push
+proactively captures the complete post-push reachable closure and CAS-publishes
+a replacement manifest that normally has fewer packs. At the hard cap, an
+equal-count replacement is also valid when it incorporates the newly reachable
+objects while remaining within the bound. The old immutable objects are not
+deleted, so readers holding an earlier manifest remain valid. Physical
+object-store deletion remains a separate retention concern outside this proof
+boundary.
 
 ### Theorem 3 (Linearizable Refs / No Lost Update)
 
@@ -482,6 +486,7 @@ symbol search, not line counts.)
 | `run_conformance_probe` (A1/A3 fail-closed startup gate) | `store.rs` + `main.rs` |
 | `hydrate_for_read` / `hydrate_for_write` | `hydrate.rs` |
 | Bounded digest-keyed pack/index cache and single-flight population | `pack_cache.rs` |
+| Proactive full-closure pack compaction before manifest capacity | `cas_publish.rs` |
 | `ParentState { if_match, parent_digest, parent }` + `from_loaded`/`fresh` | `cas_publish.rs:154` |
 | `cas_publish(.., &parent_state) -> Result<CasSuccess, CasError>` | `cas_publish.rs:410` |
 | `CasError::Conflict { winner_manifest, winner_manifest_key }` (typed 412) | `cas_publish.rs:92` |
@@ -519,7 +524,9 @@ snapshot reads succeed (`snapErr`); whether it *changes* refs is then **derived*
 (`DidChange == newVal ≠ value-in-the-manifest-it-read`), not a free boolean. The
 skip predicate is `MustPublish(p) == DidChange(p) \/ snapErr(p)` — "publish unless
 we *observed* no change," never "publish unless `b == a`" with failed reads
-compared equal.
+compared equal. A `compacted` marker distinguishes normal delta-pack stages
+from stages whose own pack is the trusted full closure produced from every
+post-push ref tip.
 
 Crucially the model carries the **real ref value** per manifest (`refs[m]` = the
 objectId `main` holds in manifest `m`) and explicit **history** (`parent[m]`).
@@ -531,7 +538,7 @@ TLC checks eight invariants (a finiteness constraint, `BoundedManifests`, caps p
 |---|---|---|
 | `Inv_Fence` | T1 | an obligated push's manifest is published before success is observed |
 | `Inv_ChangedPublished` | T1 | a ref-changing push is always published (fallible-snapshot bite) |
-| `Inv_Closed` | T2 | a published manifest's pack set *covers* its published parent's |
+| `Inv_Closed` | T2 | a normal manifest covers its parent's packs; a compacted manifest names its trusted full-closure pack |
 | `Inv_NoFork` | T3 | no two published manifests share a parent (a fork = a lost update) |
 | `Inv_RefEffectApplied` | T3 | an installed push's committed ref value equals the value it proposed |
 | `Inv_RefDerivedFromParent` | T3 | an install is derived from the pointer it read (no build on superseded state) |
@@ -541,7 +548,6 @@ TLC checks eight invariants (a finiteness constraint, `BoundedManifests`, caps p
 ```
 $ tlc GitOnObjectStore.tla -config GitOnObjectStore.cfg
 Model checking completed. No error has been found.
-1435102 states generated, 435745 distinct states found, 0 states left on queue.
 ```
 
 **Every invariant is proven non-vacuous** by a mutation that trips it (each
@@ -551,14 +557,16 @@ checked in isolation against each mutant). This is the discipline that catches
 | Mutation | Trips |
 |---|---|
 | skip predicate `DidChange /\ ~snapErr` (ref change + both snapshots fail → silently skipped) | `Inv_ChangedPublished` |
-| `packs[m] = {m}` (manifest drops predecessor's packs) | `Inv_Closed` |
+| a normal stage uses `packs[m] = {m}` without the full-closure marker | `Inv_Closed` |
 | drop CAS guard (two pushers install off one parent — a fork) | `Inv_NoFork` |
 | install records the *read* ref value, not the push's proposal (effect dropped) | `Inv_RefEffectApplied` |
 | record parent as root instead of the pointer actually read | `Inv_RefDerivedFromParent` (+ `Inv_NoFork`) |
 
-The `packs[m]={m}` and CAS-guard mutations are exactly the two vacuity tests an
-external reviewer ran against an earlier draft, where the then-invariants passed
-unchanged; the history + real-ref-value vocabulary is what makes them fail now.
+The unmarked `packs[m]={m}` and CAS-guard mutations are the two core closure and
+serialization vacuity tests. The full-closure marker is only assigned by the
+compaction branch; reusing it for a normal delta stage would make the closure
+claim vacuous, so the model explicitly clears stale markers when manifest ids
+are reused.
 The ref-value mutations (effect-dropped, wrong-parent) are what close the gap from
 "pointer CAS serializes" to "ref *updates* are linearizable" — the user-visible
 theorem the title promises. (A weaker mutation, `MustPublish == DidChange` alone,
@@ -574,9 +582,8 @@ The model is checked at `Pushers = {p1,p2,p3}`, `MaxManifests = 3`, under the
 the retry loop otherwise lets pushers churn fresh manifest ids and ref values
 without bound, so the model is *finite-state only with the bound*. Three
 concurrent pushers exercise every CAS race relevant to these invariants (a fourth
-adds no qualitatively new interleaving); the real-ref-value domain is what makes
-even three a ~436K-state check. This is a *bounded* model check, not an unbounded
-proof: it exhaustively verifies the invariants within the bound and is mutation-
+adds no qualitatively new interleaving). This is a *bounded* model check, not an
+unbounded proof: it exhaustively verifies the invariants within the bound and is mutation-
 shown non-vacuous, which is the standard claim for a TLC-checked safety spec.
 
 ## Summary

docs/spec/GitOnObjectStore.tla

@@ -9,7 +9,8 @@
 (* Pushers race to advance a single manifest pointer holding a ref value.   *)
 (* We assert (see SAFETY PROPERTIES for the full set and per-invariant docs):*)
 (*   T1  fence: observed success => the obligated push is durably published  *)
-(*   T2  closure: a published manifest's pack set covers its parent's        *)
+(*   T2  closure: a published manifest either covers its parent's packs or   *)
+(*       names a trusted full-closure compaction pack                         *)
 (*   T3  ref linearizability: installs form a fork-free chain, each commits  *)
 (*       exactly the value it proposed, derived from the pointer it read     *)
 (* Each invariant is mutation-tested non-vacuous; see docs/ Mechanized §.    *)
@@ -28,12 +29,13 @@ VARIABLES
     staged,     \* pusher id -> manifest id it intends to install
     parent,     \* manifest id -> the manifest id it was derived from (history)
     refs,       \* manifest id -> objectId that this manifest binds the ref "main" to
+    compacted,  \* manifests whose own pack is a full closure of their refs
     newVal,     \* pusher id -> objectId this push proposes for "main" (its effect)
     snapErr,    \* pusher id -> did either ref-snapshot read fail? (BOOLEAN)
     observed    \* set of pusher ids that have observed success (fence passed)
 
 vars == <<pointer, published, packs, pc, readEtag, staged,
-          parent, refs, newVal, snapErr, observed>>
+          parent, refs, compacted, newVal, snapErr, observed>>
 
 \* We model a single ref, "main", whose value is an objectId in ObjIds. This is
 \* enough to exhibit ref-update linearizability: a lost update is the published
@@ -57,6 +59,7 @@ TypeOK ==
     /\ staged \in [Pushers -> ManifestIds]
     /\ parent \in [ManifestIds -> ManifestIds]
     /\ refs \in [ManifestIds -> ObjIds]
+    /\ compacted \subseteq ManifestIds
     /\ newVal \in [Pushers -> ObjIds]
     /\ snapErr \in [Pushers -> BOOLEAN]
     /\ observed \subseteq Pushers
@@ -70,6 +73,7 @@ Init ==
     /\ staged = [p \in Pushers |-> 0]
     /\ parent = [m \in ManifestIds |-> 0]
     /\ refs = [m \in ManifestIds |-> 0]   \* "main" starts at objectId 0 (empty)
+    /\ compacted = {}
     /\ newVal = [p \in Pushers |-> 0]
     /\ snapErr = [p \in Pushers |-> FALSE]
     /\ observed = {}
@@ -99,15 +103,24 @@ Begin(p) ==
     \* fail (e). The staged manifest binds "main" to v and is derived from the
     \* manifest the push READ -- so a stale reader builds on stale ref state, and
     \* only the CAS guard stops it from clobbering a newer published value.
-    /\ \E v \in ObjIds, e \in BOOLEAN :
+    /\ \E v \in ObjIds, e \in BOOLEAN, compact \in BOOLEAN :
          /\ newVal'  = [newVal  EXCEPT ![p] = v]
          /\ snapErr' = [snapErr EXCEPT ![p] = e]
          /\ LET m == FreshId IN
               /\ readEtag' = [readEtag EXCEPT ![p] = pointer]
               /\ staged'   = [staged   EXCEPT ![p] = m]
               /\ parent'   = [parent   EXCEPT ![m] = pointer]
-              /\ packs'    = [packs    EXCEPT ![m] = packs[pointer] \union {m}]
+              \* A compact stage models `pack-objects` over every post-push
+              \* ref tip. Its own pack is therefore trusted to cover the full
+              \* reachable closure; a normal stage extends the parent pack set.
+              /\ packs'    = [packs EXCEPT
+                                  ![m] = IF compact
+                                        THEN {m}
+                                        ELSE packs[pointer] \union {m}]
               /\ refs'     = [refs     EXCEPT ![m] = v]
+              /\ compacted' = IF compact
+                              THEN compacted \union {m}
+                              ELSE compacted \ {m}
     /\ pc' = [pc EXCEPT ![p] = "staged"]
     /\ UNCHANGED <<pointer, published, observed>>
 
@@ -117,7 +130,7 @@ SkipPublish(p) ==
     /\ pc[p] = "staged"
     /\ ~MustPublish(p)
     /\ pc' = [pc EXCEPT ![p] = "done"]
-    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, newVal, snapErr, observed>>
+    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
 
 \* Step 7: CAS.  Succeeds iff pointer still equals the etag this pusher read (A3).
 CasSucceed(p) ==
@@ -127,27 +140,27 @@ CasSucceed(p) ==
     /\ pointer' = staged[p]
     /\ published' = published \union {staged[p]}
     /\ pc' = [pc EXCEPT ![p] = "done"]
-    /\ UNCHANGED <<packs, readEtag, staged, parent, refs, newVal, snapErr, observed>>
+    /\ UNCHANGED <<packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
 
 CasFail(p) ==
     /\ pc[p] = "staged"
     /\ MustPublish(p)
     /\ pointer # readEtag[p]
     /\ pc' = [pc EXCEPT ![p] = "lost"]   \* will retry from idle
-    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, newVal, snapErr, observed>>
+    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
 
 \* Step 8: the fence.  Observe success ONLY after the push reached "done"
 \* (either via successful CAS or a legitimate skip).
 Observe(p) ==
     /\ pc[p] = "done"
     /\ observed' = observed \union {p}
-    /\ UNCHANGED <<pointer, published, packs, pc, readEtag, staged, parent, refs, newVal, snapErr>>
+    /\ UNCHANGED <<pointer, published, packs, pc, readEtag, staged, parent, refs, compacted, newVal, snapErr>>
 
 \* A loser retries: back to idle, ready to re-read the advanced pointer.
 Retry(p) ==
     /\ pc[p] = "lost"
     /\ pc' = [pc EXCEPT ![p] = "idle"]
-    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, newVal, snapErr, observed>>
+    /\ UNCHANGED <<pointer, published, packs, readEtag, staged, parent, refs, compacted, newVal, snapErr, observed>>
 
 Next ==
     \E p \in Pushers :
@@ -209,14 +222,16 @@ Inv_RefDerivedFromParent ==
     \A p \in Pushers :
         Installed(p) => (parent[staged[p]] = readEtag[p] /\ readEtag[p] \in published)
 
-\* T2 (Reconstruction coverage -- non-vacuous): every published non-root manifest
-\* names a pack set that COVERS its published parent's pack set plus its own pack.
-\* Perci's mutation (packs[m] = {m} instead of packs[parent] U {m}) breaks this,
-\* because then packs[parent[m]] is not a subset of packs[m].
+\* T2 (Reconstruction coverage -- non-vacuous): every published non-root
+\* manifest either names its trusted full-closure compaction pack, or covers its
+\* published parent's pack set plus its own delta pack. The model abstracts
+\* Git's reachability walk as the `compacted` marker; production earns that
+\* marker only by feeding every post-push ref tip to `git pack-objects --revs`.
 Inv_Closed ==
     \A m \in published :
         (m # 0 /\ parent[m] \in published) =>
-            (packs[parent[m]] \subseteq packs[m] /\ m \in packs[m])
+            (m \in packs[m] /\
+                (m \in compacted \/ packs[parent[m]] \subseteq packs[m]))
 
 \* Parent integrity: every published non-root manifest's parent is also published
 \* (the install chain is grounded in durable history, never in vapor).