# 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 per-repo persistent 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.

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 Sprout, 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.)

## 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). 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`. ∎

**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
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.

### 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 (sprout 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/sprout-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` |
| `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.

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 published manifest's pack set *covers* its published parent's |
| `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.
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
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` |
| `packs[m] = {m}` (manifest drops predecessor's packs) | `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 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); 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-
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) |