buzz/docs/git-on-object-storage.md

# Git Refs over Object Storage: A Formal Specification

`draft`

## Abstract

This document specifies a protocol for hosting git repositories on an object
store (S3 and S3-compatible backends such as MinIO) with **no persistent
filesystem**, and gives a formal proof of its safety properties. Repository
content is stored as create-only, content-addressed pack objects (immutable by
protocol discipline — see A1, not by assuming an immutable store); the current
state of every ref is captured by a single mutable *manifest pointer* updated
by atomic compare-and-swap (CAS). We prove two safety theorems —
**durability-ordering** (a client never observes success for a ref change that
is not yet durable) and **manifest reconstruction** (hydrating a published
manifest reconstructs every object reachable from its refs; the named pack set is
a superset of that closure) — and one
**linearizability** theorem (concurrent ref-changing pushes never lose an
update). All three reduce to three explicitly stated object-store axioms.

The protocol is not novel as an *algorithm*: it is git's post-reftable ref
model — immutable content artifacts plus an atomic pointer swap — with the
atomic primitive substituted from POSIX `rename()` to an S3 conditional `PUT`.
The contribution of this document is the **formal characterization**: to our
knowledge, no prior formal treatment of git refs over conditional-write object
storage exists (see Prior Art). The proof is *parametric over the atomic
primitive*: it holds for any backend satisfying the three axioms, and a concrete
backend is *admitted for deployment* by a single conformance gate (a finite probe
cannot prove a universal axiom; it can only admit or reject a backend).

## Scope and Non-Goals

This specification proves **safety** ("nothing bad happens"). It deliberately
does **not** prove:

- **Liveness or performance.** That a hydrate completes within a latency budget
  is empirical, not formal; it is characterized by benchmark, not theorem.
- **Git's internal correctness.** `git index-pack`, `upload-pack`, and
  `receive-pack` are trusted upstream components. We prove only that our
  *composition* feeds them well-formed inputs and surfaces their outputs
  faithfully.
- **The object-store axioms themselves.** S3's durability, read-after-write
  consistency, and conditional-write linearizability are stated as axioms
  (§Axioms); each backend is *admitted* per-deployment by an empirical conformance
  gate (§Conformance), which rejects non-conforming backends — it does not prove
  the axiom universally.

Stating this boundary is part of the claim. "Provably sound" without naming the
trust boundary does not survive scrutiny; "safety is machine-checkable relative
to three stated axioms, each empirically gated per backend" does.

### v1 deployment architecture

The implementation has *no authoritative per-repo filesystem state*. Every
request hydrates an ephemeral working tree from the published manifest, runs
the appropriate git subprocess against it, and drops the tree on scope exit:
read paths (`info/refs`, `upload-pack`) via `hydrate_for_read`, the write path
(`receive-pack`) via `hydrate_for_write`, which also returns the `ParentState`
the CAS at §Push step 7 predicates on. The relay is multi-instance-ready by
construction: nothing on local disk needs to be coordinated between instances.
Each process may retain a byte-bounded, process-lifetime cache of immutable
pack/index pairs keyed by verified digest. Deployment mounts that cache on a
per-pod ephemeral volume, so accounting and single-flight coordination stay
local. Cache misses, restarts, and evictions only affect performance; object
storage remains the source of truth, and per-request refs/HEAD are still
materialized from the current manifest.

The accepted v1 tradeoff: under concurrent same-repo pushes, every contender
hydrates and runs receive-pack, and the CAS losers' subprocess work is
discarded. This is wasted CPU/IO under contention, not a correctness bug —
`Inv_NoFork` (Theorem 3) holds because the CAS is the only writer
serialization. Same-ref concurrent push is rare; the alternative (a
cross-instance lock service) is the kind of dependency this protocol exists
to avoid. If contention ever shows up in metrics the fix is a short
best-effort *local* lock as a latency optimization, never a correctness
dependency.

A bounded retry layer on classified-terminal-vs-transport errors is **parked,
not closed.** The checked-in regression fence is the 8-way live CAS race
(`e2e_git::git_concurrent_push_one_wins_and_repo_recovers`), which passes
against MinIO with no retry layer; we ship v1 without one. (A one-off 16-way
local run against MinIO also passed, as separate calibration evidence that
the property holds at greater width — the regression test stays at 8 because
each contender clones/commits/pushes through real `git` and the cost grows
with width.) The open question — "is the no-retry default safe past MinIO
and beyond the widths so far exercised?" — re-opens on a different backend
or a sustained-load regime the conformance probe (§Conformance) doesn't
already exercise. The non-negotiable rule: retry, if added, lives in the
store layer and retries *only* pre-classification network errors — never
`Ok(2xx)`, `LostRace(412)`, or `NotFound(404)`. Retrying a classified
outcome would change the TLA action and break the proof.

## System Model

A **repository** `R` has the following state in the object store:

- A set `P_R` of **pack objects**. Each is *content-addressed* (its key is a
  cryptographic digest of its bytes) and *treated as immutable by protocol*:
  written create-only, so the same key is never overwritten, and verified by
  digest on read (see A1 — this is protocol discipline, not an assumed store
  property). Writing the same content twice is idempotent.
- A single **manifest pointer** `M_R`: a mutable object holding the digest (and
  ETag) of the *current manifest*.

A **manifest** `m` is itself an immutable, content-addressed object containing:

- `m.packs` — the set of pack-object keys that constitute the repository.
- `m.refs` — a total map `refname ↦ object_id` (the published ref state).

We write `pointer(R) = (e, d)` for the current pointer state: `e` is the
object-store ETag of `M_R`, `d` is the manifest digest it holds. `manifest(d)`
denotes the (immutable) manifest object with digest `d`.

Two operations act on `R`:

- **Read(R)** — clone / fetch / ls-remote. Resolve `pointer(R) → d`, read
  `manifest(d)`, download `m.packs`, reconstruct the object graph, serve the
  requested refs.
- **Push(R, Δ)** — receive-pack. Δ is a set of requested ref updates
  `refname ↦ (old_id, new_id)`.

**The manifest pointer is the sole source of truth.** In Buzz, a successful
push may also publish a relay event (kind:30618) so subscribers learn refs moved.
That event is a *derived notification*, never the commit point: a push has
happened iff `M_R` was CAS-swapped (A3), regardless of whether — or when — any
event is published. Relay events can lag, duplicate, or replay; subscribers must
treat them only as a signal to re-read `pointer(R)`, never as ref state. The
dangerous inversion — "the push succeeded because the event published" — would
substitute relay ordering for manifest ordering and reintroduce the lost-update
hole A3 closes. (This is a real behavioral obligation, not a restatement: today
the commit point is the local filesystem — `receive-pack` updating the bare repo,
with the relay event published best-effort afterward — so making manifest-CAS the
commit, with the event derived from it, is the change, not just a storage swap.
See §Implementation Correspondence.)

### Default-branch management

`buzz repos default-branch get/set` reads or changes the published manifest's
symbolic `head`. It selects an **existing** `refs/heads/<branch>`; it never moves
branch tips, creates/deletes refs, or changes packs. A subsequent push preserves
that HEAD while the branch exists, and fresh clones check it out.

This is a narrow, intentional exception to the Nostr-first API preference:
`GET`/`POST /git/{owner}/{repo}/default-branch` completes against the host-local
Git pointer transaction. A kind:30617 metadata edit is not equivalent: normal
event ingest persists before side effects and duplicate acknowledgements do not
rerun them. A new signed command/result lifecycle could drive the same CAS, but
adds a second completion/retry protocol for this one Git-host operation. Repo
metadata and ACLs remain in Nostr; kind:30618 remains a derived notification,
never authoritative Git state. This exception is not a general repository-settings
HTTP API.

- Both methods require request-specific NIP-98 (exact host-derived URL/method,
  timestamp, signature, shared fail-closed replay check). POST also requires a
  payload hash. Reusable Smart HTTP credentials are insufficient.
- GET requires current membership of the channel bound by the current 30617
  announcement. POST additionally requires a non-archived channel and the repo
  author, a named maintainer, or the recorded human owner of an agent-authored
  repo. Push permission, channel admin status and project membership alone do
  not grant management. Relay admission and signer/attested-owner bans apply.
- An agent may inherit management from a verified NIP-OA owner who is also a
  current channel member and manager. Kind-restricted credentials cannot grant
  this HTTP authority (there is no event kind); temporal restrictions still
  apply. Direct signer authority does not depend on an optional owner's channel
  membership. A stored agent-owner relationship is an ownership lookup, not a
  live delegation credential.
- Authorization is **admission-time**: later membership/maintainer removal,
  rebinding or archival does not cancel an already admitted write. This is
  narrower than the vision's instantaneous-revocation aspiration. The shared
  serving-write lease separately fences community deletion through the write.

GET returns `{branch, head, manifest}`. POST accepts only
`{branch, expected_manifest}` (maximum 4096 bytes) and returns the same snapshot
plus `changed`. The caller's digest must match the loaded pointer. A changed
manifest records the prior digest as its parent, then commits with that pointer's
observed ETag. Even a no-op checks the ETag. A concurrent push or default change
returns 409 instead of silently reloading and overwriting it.

The pointer CAS is the commit point. Notification failure after commit returns
an explicit error, not a rollback claim. The CLI sends POST once, with redirects
disabled. Ambiguous delivery (including server errors or a lost response) is
non-retryable `delivery_unknown` and retains the original expected digest. Read
current state before deciding on another write; blindly running `set` without
`--expected-manifest` would observe a fresh version and can override someone
else's later decision. A conflict is exit code 5.

Deploy relay support **before** using an updated CLI against that relay. This
requires no schema migration and changes no live repository merely by deploying.
See the [CLI examples](../crates/buzz-cli/README.md#default-branch).

## Axioms

The protocol's safety is proved *relative to* the following properties of the
object store. Each is a documented property of AWS S3 (2024+) and a testable
assumption for any S3-compatible backend.

- **(A1) Durable write.** A `PUT` that returns success is durable. S3 does *not*
  by itself make an object immutable — that is enforced by **protocol rule**, not
  assumed of the store: pack and manifest objects use content-addressed keys and
  are written create-only (`If-None-Match: *`), so a key is never overwritten,
  and readers verify the object's bytes against its key digest. Any deviation is
  therefore *detectable* (digest mismatch), not silent. (We do not rely on S3
  Object Lock or bucket immutability policy; the create-only + content-address
  discipline is sufficient and backend-portable.) **No deletion under the
  protocol.** Pack and manifest objects are never deleted by the protocol. This
  is what makes Read a consistent snapshot in the presence of concurrent writers:
  a reader holding an old manifest digest can always GET every pack it names,
  because no writer removes packs. Physical pruning of unreachable packs is a
  *backend retention concern* outside this proof boundary; any such sweep must
  honor in-flight readers (e.g. a retention window longer than the max hydrate
  time), and proving that bound is future GC work, not part of the safety
  argument here. (Without this rule, a GC that prunes packs a winning push
  orphaned could 404 a concurrent reader mid-hydrate — see Theorem 2's reliance
  on every named pack being GETtable.)

- **(A2) Strong read-after-write.** A read issued after a successful `PUT`
  observes that write. (AWS S3 provides this for all regions and all
  PUT/DELETE.)

- **(A3) Linearizable conditional write (CAS).** `PUT M_R If-Match: e` succeeds
  iff the current ETag of `M_R` equals `e`; otherwise it fails with a
  precondition error and does not modify `M_R`. Among any set of conditional
  PUTs predicated on the same `e`, **at most one succeeds**, and all PUTs are
  linearizable (there is a single total order consistent with observed
  successes/failures). "Linearizable conditional write" is *our* formal term for
  the axiom. The supporting AWS evidence: S3 documents `If-Match` as comparing the
  supplied ETag against the current object ETag (match → `200`, mismatch → `412`)
  and strong read-after-write consistency in all regions; the Nov 2024
  conditional-update announcement states this offloads compare-and-swap to S3.
  (`If-None-Match: *` for create-only PUT shipped Aug 2024.) AWS does not use the
  word "linearizable" in the user guide — we treat the documented CAS + strong
  consistency as evidence *for* the axiom, not as AWS asserting our term.

A3 is the single load-bearing backend assumption. It replaces the POSIX
`rename()` atomicity that reftable relies on. See §Conformance for how a backend
is *admitted* against it.

## Protocol

### Read

1. Resolve `pointer(R) = (e, d)`.
2. Fetch `manifest(d)`; let `m = manifest(d)`.
3. For each key in `m.packs`, GET the pack object (A2 guarantees visibility;
   content-addressing lets the reader verify each, given A1).
4. Hydrate a bare repository from the packs; serve refs from `m.refs`.

Read takes no locks and never writes. It observes a single committed manifest
`d` and is therefore a consistent snapshot by construction, even under concurrent
writers, because: (i) `manifest(d)` and the packs it names are immutable
[A1 + content-addressing], so a writer that advances the pointer past `d` cannot
alter what `d` resolves to; and (ii) **no pack `d` names is ever deleted**
[A1, no-deletion rule] and every named pack was durably written before `d` was
published [A1 + A2, §Push step order], so a reader holding an older `d` can always
GET every pack — a concurrent GC that prunes packs unreachable from the *new*
pointer never 404s this reader. This read-consistency-during-writer property is the
reason the no-deletion rule is load-bearing, not cosmetic; it is asserted in the
prose here because the mechanized model has no Read action (it checks the writer
side; this is the reader-side complement).

### Push

```
1. receive-pack: accept the pack, index it, derive new object set O.
2. for each o in O: PUT pack-object(o)            # content-addressed, idempotent (A1)
3. (e, d_before) := pointer(R); m_before := manifest(d_before)
4. validate Δ against m_before.refs               # fast-forward / push rules
       on rejection -> respond non-ff, STOP (no write, no fence cost)
5. m_after := m_before with refs updated per Δ; packs := m_before.packs ∪ keys(O)
6. d_after := PUT manifest-object(m_after)         # content-addressed (A1)
7. result := PUT M_R (value = d_after)          # CAS (A3)
       If-Match: e         if a pointer already exists (e from step 3)
       If-None-Match: *    if the repo has no pointer yet (first push / repo init)
       on 412 (lost race): re-read pointer, GOTO 3 (retry) or respond non-ff
       on success: the ref change is PUBLISHED
8. construct success response   # ONLY after step 7 succeeds  -- the FENCE
```

**The fence (step 8 after step 7).** The success response is not constructed
until the CAS in step 7 returns success. This is the publish-ordering
guarantee. It is *conditional on refs changing*: a no-op or rejected push
(step 4) never reaches step 7 and pays zero CAS/fence latency.

**No advisory lock.** Reftable serializes writers with `tables.list.lock` *and*
the rename. This protocol has **no advisory lock in v1**: writer serialization
is provided entirely by the CAS in step 7. §Theorem 3 proves this is
sufficient — the lock reftable uses is an optimization (it avoids wasted work
under contention), not a correctness requirement, *given A3*.

**Retry is policy, not safety.** The "GOTO 3" loop on a 412 is a *liveness/policy*
choice — retry count, backoff, or immediate non-ff rejection are all sound. Safety
(Theorems 1–3) holds for any of them, because a losing push that retries simply
re-runs steps 3–7 against the advanced pointer; it never writes `M_R` while
predicated on a stale ETag. We deliberately make no liveness claim here (§Scope).

## Safety Theorems

Let a push `p` be **ref-changing** if it reaches step 7. Let `observe(p) =
success` mean a client received `p`'s success response (step 8 executed).

### Theorem 1 (Durability-Ordering)

> If `observe(p) = success` for a ref-changing push `p`, then at the moment of
> observation, `pointer(R)` has held a value `d_after` whose manifest reflects
> `p`'s ref updates, and that manifest and all packs it names are durable.

**Proof.** Step 8 executes only after step 7 returns success (program order;
enforced by type in the implementation — see §Implementation Correspondence).
By A3, step 7's success means `M_R` was atomically set to `d_after`. By A1,
`manifest(d_after)` (written step 6) and every pack in `O` (written step 2,
before step 6) are durable. The fence orders the client-visible success strictly
after the durable pointer swap. Therefore observation implies durability. ∎

*Pointer integrity:* the pointer object holds a manifest *digest*, not inline
state. A1+A2 mean a successful pointer write is durable and read-after-write
consistent; a bit-flip in the stored digest yields a value that resolves to no
manifest (or a digest-mismatched one), so Read fails *closed* (error, not a
wrong-but-plausible history). The protocol never trusts an unresolvable or
mismatched pointer.

Corollary (crash safety): if the process crashes between any two steps, no
client has observed success unless step 7 completed; an incomplete push leaves
orphan packs and an unchanged pointer — wasted bytes, never a visible-but-lost
ref change.

### Theorem 2 (Manifest Reconstruction)

> Read(R) resolving to manifest digest `d` can reconstruct, in full, the object
> graph reachable from every ref in `manifest(d).refs` — no reachable object is
> missing. (The named pack set is a *superset* of that reachable closure; see
> the remark on force-push/delete below.)

**Proof.** By the push order, `d` is published (step 7) only after all packs in
`manifest(d).packs` are durably written (step 2, before step 6). By A2 a reader
that resolves `d` (step 1) can GET every pack in `manifest(d).packs` (step 3).
By A1 + content-addressing, each pack's bytes are exactly those written, and any
deviation is detected by digest. Git's `index-pack` over a complete, verified
pack set reconstructs the object graph (trusted upstream, §Non-Goals; reproducible
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). 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 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. 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)

> If two ref-changing pushes `p₁`, `p₂` execute concurrently, the published
> history of `M_R` contains both effects in some serial order, or rejects one;
> neither silently overwrites the other.

**Proof.** Both read the pointer (step 3) and CAS predicated on the ETag they
read (step 7). Suppose both read ETag `e`. By A3 at most one CAS predicated on
`e` succeeds; WLOG `p₁` succeeds, `M_R` advances to `e′`. `p₂`'s CAS predicated
on `e` then fails (412): `p₂` re-reads (now `e′`, `d_after(p₁)`), re-validates Δ
against `p₁`'s published refs (step 4), and either composes onto `p₁`'s state or
is rejected non-ff. `p₂` never writes `M_R` while predicated on the stale `e`.
By A3's linearizability, the successful CAS sequence is a single total order;
each push's `m_after` is computed from its immediate predecessor's published
state. Hence no update is lost and the published ref history is serial. The
absence of an advisory lock changes only *efficiency under contention* (a loser
may do wasted indexing before its 412), not correctness. ∎

The mechanized model makes "no update is lost" concrete in checked forms over
**real ref values**: the published manifests form a chain with no two sharing a
parent (`Inv_NoFork` — a shared parent *is* a lost update); an installed push's
committed ref value equals the value it proposed (`Inv_RefEffectApplied` — your
write is what lands); each install is derived from the pointer it actually read
(`Inv_RefDerivedFromParent` — never built on superseded state). Removing the CAS
guard makes the model fork; that is the precise sense in which A3 is load-bearing.

## Conformance (Admitting a Backend for A3)

A3 is the only axiom not guaranteed by the protocol itself; for AWS S3 it is
documented, for any other backend (MinIO, Ceph RGW, ...) it is an empirical
claim. A backend is **admitted** against it by a **conformance probe** run at
startup against the target backend. The probe is a **deployment admission gate**: a backend is
trusted only if it passes. Passing does *not* prove the universal axiom — a
finite probe yields operational confidence for *this backend, build, and
config*; failure invalidates the design against that backend, exactly as
non-atomic `rename()` would invalidate reftable.

The probe has both a sequential half (semantic correctness) and a concurrent
half (linearizability under contention). The concurrent half is the load-bearing
part — A3 is a claim about *races*, so a probe that only checks sequential
conditional writes cannot admit a backend against it.

1. **Sequential semantics.** create-if-absent succeeds; duplicate
   `If-None-Match: *` fails; `If-Match: E` with current ETag succeeds; stale
   `If-Match` fails; `If-Match` on a missing key does not create; read-after-write
   returns the written value.
2. **N-way `If-Match` race (required).** Write key with body `base`; read its
   ETag `E` via the *same code path production uses for the pointer*. Spawn N
   (e.g. 32–64) concurrent `PUT key If-Match: E` with unique bodies. **Pass** iff
   exactly one succeeds, the other N−1 classify as precondition-failed, a
   subsequent read returns the winner's body and a new ETag, and the final body is
   never one of the *failed* payloads. Repeat for R rounds (configurable; default
   trades boot time against confidence).
3. **N-way `If-None-Match: *` race (required).** Same shape on a missing key:
   exactly one create wins, N−1 precondition failures, final body is the winner.
4. **ETag-token consistency.** Verify HEAD-path and GET-path ETag extraction
   agree byte-for-byte (quoting included). `If-Match` compares tokens literally;
   a quote mismatch between the read path and the write path silently tests the
   wrong thing. The probe must use the exact token format the pointer write uses.

**Proof surface (explicit non-goals of the probe and the design).** The protocol
depends only on conditional writes of *small single objects* (the manifest
pointer). It does **not** depend on, and the probe does **not** test:
conditional *multipart* uploads (packs are content-addressed plain PUTs, staged
without conditionals) or conditional *delete* (GC uses retention/sweep over a
republished manifest, not `If-Match` delete). Keeping the proof surface to
single-object conditional PUT is what makes A3 both sufficient and cheaply
checkable.

If the probe passes, A3 is admitted for that backend and Theorems 1–3 transfer
unchanged.

## Prior Art

The *algorithm* is established; the *formal characterization* is, to our
knowledge, new.

- **JGit `DfsRefDatabase`** reduces backend ref consistency to two **per-ref**
  CAS hooks, `compareAndPut(oldRef, newRef)` and `compareAndRemove(oldRef)`
  (`org.eclipse.jgit/.../dfs/DfsRefDatabase.java`). This *is* the model "git
  refs = CAS over ref state," spelled in Java — at per-ref granularity.
- **JGit/Google `reftable`** (`Documentation/technical/reftable.md`): immutable
  reftable files plus a single mutable `tables.list` pointer swapped atomically
  via `tables.list.lock` + POSIX `rename()`. Note this is *pointer*-granularity,
  not the per-ref CAS of `DfsRefDatabase` — reftable CASes one stack pointer.
  This protocol is the same shape: it substitutes an S3 conditional `PUT` for
  reftable's `rename()` and (v1) omits the advisory lock. Our granularity is one
  **repo manifest pointer** — the same single-pointer granularity as reftable,
  not the per-ref granularity of `DfsRefDatabase`.
- **`awslabs/git-remote-s3`** uses per-ref lock objects via S3 conditional
  writes (advisory lock substitute). **`mattn/git-remote-s3`** uses a
  `latest.json` pointer with `If-Match`/`If-None-Match` optimistic locking —
  closest to this design; advertises MinIO compatibility.
- **`johnny0917/jgit-aws`** stores packs in S3 but refs in DynamoDB
  (`compareAndPut` → Dynamo conditional update), the canonical pre-2024 *punt*:
  before S3 had conditional writes, the CAS-needing state went elsewhere. This
  protocol is what becomes possible once S3 itself offers CAS.
- **Gitaly (GitLab)** supports only local Git storage for refs; it punts ref
  consistency to the local filesystem and does not attempt object-store CAS.
- **arXiv:** no formal treatment of git refs over object storage found.
  `arXiv:1904.06584` ("GoT: Git, but for Objects") is a git-*inspired*
  replicated-object model, not a formalization of this problem.

## Implementation Correspondence

The fence (Theorem 1) maps to a single structural obligation on the
implementation, stated here as a requirement the code must meet for the proof to
transfer:

- **Unique constructor seam.** There must be exactly one path that builds a
  *push* `Response`, and it is `finalize_push(PushContext) -> Response`. The
  discriminator is the `PushContext`: only `finalize_push` consumes one, and a
  push subprocess's output reaches a response only by being wrapped in a
  `PushContext`. (The lower-level `build_git_response` helper that does the literal
  `Body::from(stdout)` conversion is *shared* with the read paths — info_refs,
  upload_pack — so it has two call sites; but those carry no `PushContext` and no
  fence obligation, so push-side uniqueness is structural, not a property of the
  body conversion itself. A reader auditing the code will see `build_git_response`
  reached twice and should check the discriminator is `PushContext`, not the
  conversion.) If any other path could build a push response without going through
  `finalize_push`, the fence would be convention, not structure, and Theorem 1
  would not hold. This is a checkable code property, verified by reviewers against
  the actual seam (`finalize_push`).
- **Parent observed once.** `hydrate_for_write` reads the pointer, fetches and
  verifies the parent manifest, materializes the workspace from it, and returns
  a `(HydratedRepo, ParentState)` pair where `ParentState` carries the exact
  `(ETag, digest, Manifest)` triple the workspace was hydrated against. That
  same `ParentState` rides on the `PushContext` through receive-pack, and
  `cas_publish` predicates the CAS on `parent_state.if_match` — it never re-reads
  the pointer. The "build on `d_old`, publish against `d_new`" hazard is closed
  at the type system: a concurrent writer that advances the pointer between
  hydrate and CAS surfaces as `CasError::Conflict`/HTTP 409, not as a manifest
  whose `parent` disagrees with the refs the workspace produced. This is the
  Rust analogue of `Inv_RefDerivedFromParent`.
- **412 → 409, terminal.** The CAS lost-race outcome maps to a typed
  `CasError::Conflict { winner_manifest, winner_manifest_key }`. The variant is
  distinct from `Backend(StoreError)` so `?`-bubbling cannot turn 412 into 500.
  There is no in-handler retry: the loser's receive-pack output was derived
  against a now-superseded parent, so reusing it would change the TLA action
  and break `Inv_RefDerivedFromParent`. The client re-pushes, which re-hydrates
  against the advanced state — that is the only safe retry, and `git` itself
  drives it.
- **kind:30618 derived after CAS.** Emission is conditional on
  `manifest_changed = (parent_digest != committed_digest)` — `Manifest::
  canonical_bytes` is deterministic, so equal published state ⇒ equal digest by
  construction (no-op pushes pay no 30618 cost). The event is built by
  `manifest_event::build_ref_state_event` from `CasSuccess.manifest` — the
  values that *physically landed* via CAS, by `Inv_RefEffectApplied`. The event
  is relay-signed (the relay is authoritative for ref state of repos it hosts);
  the pusher's pubkey rides in a `p` tag (buzz extension; NIP-34 does not
  define one). 30618 emission happens after `cas_publish` returns `Ok` and
  before the success `Response` is constructed — so 30618 is a strict
  consequence of a committed CAS, never the commit itself. A failed 30618
  insert is non-fatal: the push remains durable in the object store, and the
  next read/push surfaces the committed state from the manifest.
- **No advisory lock.** Writer serialization is the CAS. The per-repo mutex the
  legacy persistent-disk path used would only have spanned a single process and
  is incompatible with the multi-instance v1 architecture (§Scope). Dropping it
  was strictly more correct, not a risk — same-repo concurrent pushes each
  hydrate + run receive-pack, and the CAS losers' work is discarded (an
  accepted v1 tradeoff named in §Scope).

**Current code status (verified provenance).** The full S3-CAS implementation
exists in code at PR #726's tip (`crates/buzz-relay/src/api/git/`), with the
relay lib green, clippy `--tests -D warnings` clean, fmt clean, and the live
MinIO e2e — clone/push/fetch/force-push roundtrip + N-way concurrent-push
no-fork — green on the assembled tip. (Line numbers below are pinned at
landing time; reviewers checking after subsequent refactors should consult
symbol search, not line counts.)

| Spec element | Code |
|---|---|
| `Manifest { version, head, refs, packs, parent }` + `canonical_bytes` | `manifest.rs` |
| `Manifest::validate()` (pre-CAS rejection: refs/HEAD/OIDs/parent-shape) | `manifest.rs` |
| `GitStore::{put_pack, put_manifest, put_pointer}` (create-only + CAS) | `store.rs` |
| `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` |
| `build_ref_state_event(&RefStateInputs, &Keys)` (NIP-34 kind:30618) | `manifest_event.rs` |
| `PushContext { pack, parent_state, repo_handle, … }` | `transport.rs:643` |
| `finalize_push(state, ctx) -> Response` — **the seam** | `transport.rs:674` |
| `build_git_response` (sole `Body::from(stdout)` site) | `transport.rs:627` |

The push path reaches `build_git_response` *only* through `finalize_push`,
which consumes a `PushContext`; the compiler enforces "no `PushContext` ⇒ no
push `Response`." Read paths reach `build_git_response` independently after
hydrating the published state via `hydrate_for_read` — pointer-absent → 404,
any below-pointer failure → 5xx, never a synthesized empty repo (A1
detectability holds in the read direction too). The 404 invariant is
unambiguous because kind:30617 announce seeds an empty-manifest pointer
*before* the announcement event is published: an announced repo is always
cloneable (empty refs, but a valid pointer), and pointer-absence means "never
announced."

One named follow-up: a behavioral integration test for runtime ordering
(publish-before-response) — currently enforced by `finalize_push` being a
single sequential async fn (no detached `tokio::spawn`) — is the
belt-and-suspenders item to add once a mockable-CAS seam exists. The
mechanical no-fork claim is empirically gated by the live N-way
concurrent-push e2e (`e2e_git::git_concurrent_push_one_wins_and_repo_recovers`).

## Mechanized Verification

The safety theorems are model-checked, not only argued in prose. The companion
TLA+ module `docs/spec/GitOnObjectStore.tla` models concurrent pushers racing to
advance the manifest pointer, with the CAS action (`If-Match`) as the sole
pointer writer — directly encoding axiom A3. Each push models a proposed ref
value (`newVal`, the objectId it wants `main` to hold) and whether its ref
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. 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]`).
This is what lets the invariants prove ref-*update* linearizability — that *your*
ref write is what gets committed and survives — not merely pointer-id bookkeeping.
TLC checks eight invariants (a finiteness constraint, `BoundedManifests`, caps published manifests at `MaxManifests` so the retry loop terminates):

| Invariant | Theorem | Statement |
|---|---|---|
| `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 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) |
| `Inv_ParentPublished` | T2/T3 | every published manifest's parent is published (grounded history) |
| `Inv_PointerPublished` | T1 | the pointer always names a published manifest |

```
$ tlc GitOnObjectStore.tla -config GitOnObjectStore.cfg
Model checking completed. No error has been found.
```

**Every invariant is proven non-vacuous** by a mutation that trips it (each
checked in isolation against each mutant). This is the discipline that catches
"green but vacuous" specs:

| Mutation | Trips |
|---|---|
| skip predicate `DidChange /\ ~snapErr` (ref change + both snapshots fail → silently skipped) | `Inv_ChangedPublished` |
| 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 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,
does *not* break safety — it over-publishes, safe-but-wasteful; noted so the
mutation set is honest about which mutations are true safety regressions.
`Inv_ChangedPublished` and `Inv_Fence` look redundant but are not: see the .tla
comment — mutating the `MustPublish` operator weakens `Inv_Fence`'s own predicate,
so the `DidChange`-predicated `Inv_ChangedPublished` is the one that stays
load-bearing under exactly that mutation.)

The model is checked at `Pushers = {p1,p2,p3}`, `MaxManifests = 3`, under the
`BoundedManifests` constraint (`|published| ≤ MaxManifests`) — required because
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). 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

| Property | Status | Discharged by |
|---|---|---|
| Durability-ordering (T1) | Proved | Fence + A1, A2 |
| Manifest reconstruction (T2) | Proved | Content-addressing + A1, A2; git upstream |
| No lost update (T3) | Proved | A3 (no advisory lock needed) |
| A1/A2/A3 hold on backend | Empirical | Conformance probe (gate) |
| Liveness / latency | Empirical | Benchmark (out of scope) |