# 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 states what has been verified about it. 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).

The correctness statement is a refinement. Every behavior of the protocol is a
behavior of an *atomic ref database* (`docs/spec/GitRefDB.tla`), in which a push
takes effect in one step, is applied only if it is authorized and only against
the ref values it names, and is reported to the client truthfully. This covers
**linearizability** (concurrent pushes never lose an update) and the client-side
half of **durability-ordering** (a client is never told an update succeeded
unless it was published). Three further properties concern storage: the pointer
never names an object that is not stored, the packs a published manifest lists
contain every object reachable from its refs (**manifest reconstruction**), and
whatever a reader has resolved stays fetchable.

Three kinds of evidence support these statements, and §Mechanized Verification
says which claim rests on which. The refinement and the storage properties are
model-checked exhaustively for small instances. The pointer discipline is
proved in Lean for any number of clients, refs and objects. The correspondence
between the models and the Rust code rests on tests and review. All of it is
relative to three object-store axioms and to a stated contract for
`git receive-pack`. Two further behaviors of the implementation, the
serving-write lease and the order of the derived kind:30618 events, are checked
in a separate bounded model.

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 argument 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 concerns **safety** ("nothing bad happens"). It deliberately
does **not** establish:

- **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. The models represent
  `receive-pack` by a stated contract (assumption G1, §Mechanized Verification)
  and check that our *composition* publishes exactly what git did and reports
  git's 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 modeled action, and the checked results would no
longer apply to the code.

## 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. The model has a
reader process and checks the property as `ReaderComplete`; a seeded deletion of
an unlisted pack violates it (§Mechanized Verification).

### Push

```
1. (e, d_before) := pointer(R); m_before := manifest(d_before)
   hydrate an ephemeral workspace W from m_before      # one pointer observation
2. receive-pack on W with the pre-receive hook installed:
       the hook submits the whole command list Δ to the push policy;
           if the policy declines, git applies no command
       git applies a command only if its old_id is the ref's value in W
3. refs_after := refs(W)                              # what git actually did
       refs_after = m_before.refs -> relay git's output, STOP (nothing to publish)
       git exited abnormally      -> respond error, STOP (nothing is published)
4. O := a pack of the objects reachable from refs_after but not from
        m_before.refs (delta), or of all objects reachable from refs_after
        (compaction)
5. PUT pack-object(O)                                 # content-addressed, create-only (A1)
6. m_after := (refs_after, head, packs, parent = d_before)
        packs = m_before.packs ∪ keys(O), or keys(O) alone after compaction
   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 1)
       If-None-Match: *    if the repo has no pointer yet
       on 412 (lost race): respond conflict (HTTP 409), STOP
       on success: the ref change is PUBLISHED
8. relay git's output to the client   # ONLY after step 7 succeeds  -- the FENCE
```

**The fence (step 8 after step 7).** Git's status report for a push that
changed refs is not sent until the CAS in step 7 returns success. This is the
publish-ordering guarantee. It applies only when refs changed: a push that git
declined, or one that changed nothing, stops at step 3 and performs no write.

**Publication is decided from the workspace (step 3).** The relay does not infer
what git did from git's exit status or from the status report in its output.
Both are unreliable for this purpose. `git receive-pack` exits 0 when the
pre-receive hook declines a push and when a request carries no commands, it
reports a declined push only to a client that asked for a status report, and a
push with several commands can end with some applied and others refused. The
relay therefore compares the refs in the workspace after `receive-pack` with
the refs the workspace was hydrated from. If they are equal, nothing is
published and the client receives git's own answer. That answer contains `ok`
only for a command whose new value equals its old value: git accepts such a
command and changes nothing, and its report is true of the published state the
workspace was hydrated from. If they differ and git
exited normally, exactly the refs now in the workspace are published, so the
`ok` and `ng` lines git reported per ref are true of the published state. If
they differ and git exited abnormally, the request fails and nothing is
published. Under the contract G1 for `receive-pack` (§Mechanized Verification),
a changed workspace implies that the push policy accepted the command list, so
a publication always acts for an authorized push.

**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 states that this is
sufficient — the lock reftable uses is an optimization (it avoids wasted work
under contention), not a correctness requirement, *given A3*.

**No retry inside a request.** A push that loses the race at step 7 is answered
with a conflict. Its workspace was computed from a manifest that is no longer
current, so nothing derived from it may be published; the client pushes again,
which starts at step 1 against the new pointer. Whether and when a client
retries is a liveness matter and affects none of the safety properties. We
deliberately make no liveness claim here (§Scope).

## Safety Theorems

This section states the properties the protocol is required to have. The
statements are numbered as theorems because the implementation's comments cite
them by number. The paragraphs marked *Argument* explain why each property
holds; they are explanations and not the evidence. The evidence is in
§Mechanized Verification: each statement is checked exhaustively by TLC for
small instances, and the parts of Theorems 1–3 that concern the pointer are
proved in Lean without a bound on clients, refs or objects.

Two definitions are used throughout. A push is **published** when its
conditional write in step 7 succeeds. A client is **told `ok` for a ref** when
the response it receives contains git's status line `ok <ref>`.

### Theorem 1 (Durability-Ordering)

> (a) Whenever the pointer names a manifest, that manifest and every pack it
> lists are stored. (b) If a client is told `ok` for a command that changes a
> ref, the push was published before the response was sent, and the published
> manifest holds the value the client asked for.

**Argument.** For (a), a manifest becomes the pointer's value only in step 7,
and the same request stored that manifest in step 6 and its new packs in step
5. The packs it inherits were listed by `m_before`, which was the pointer's
value when read, so they were already stored; nothing is deleted (A1). For (b),
the response is built in step 8, which runs only after step 7 succeeded, and
`refs_after` in the published manifest is the workspace state from which git
produced its `ok` lines. A request that stops at step 3 relays git's output
without publishing. In that case every `ok` git reported belongs to a command
that asked for the value the ref already had, because a command that changes a
ref and is reported `ok` leaves the workspace different from `m_before`. Such a
report is true of the state the request read in step 1, and that read is where
the request takes effect.

*Model:* (a) is the invariant `Fence`; (b) is part of the refinement `Refines`
(the abstract specification allows a response to report only the outcome fixed
when the push took effect) and is also stated directly as `NoSilentDrop`.
The check `relayed-ok` confirms that the model reaches the case of an `ok`
that is relayed without a publication.

*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 been told `ok` unless step 7 completed; an incomplete push leaves
orphan packs and an unchanged pointer — wasted bytes, never a visible-but-lost
ref change. The converse does not hold and is not claimed: a push can be
published and the client can still receive an error, for example when the
response is lost. The client then learns the outcome by reading the refs.

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

**Argument.** By Theorem 1(a) every pack in `manifest(d).packs` is stored, and
by A2 a reader that resolves `d` can GET each of them. 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 sequence of publications: the empty repo's manifest names ∅ and
refs ∅ (covered vacuously). A normal step sets
`m_after.packs = m_before.packs ∪ keys(O)` where `O` holds every object
reachable from `refs_after` that is not reachable from `m_before.refs`, so an
object reachable from `refs_after` is either in `O` or covered by the induction
hypothesis. A compaction step instead feeds every `refs_after` 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. The induction applies to `m_before` because the conditional write
succeeds only if `m_before` is still the pointer's value (Theorem 3).

The step "`O` holds every object reachable from `refs_after` and not from
`m_before.refs`" requires those objects to be present in the workspace. That is
part of the contract G1: `receive-pack` refuses a ref update whose new value is
not fully connected.

*Model:* the invariant `PublishedClosed`, over an object graph in which one
object refers to another, so that a pack can lack an ancestor.

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

### Theorem 3 (Linearizable Refs / No Lost Update)

> Every behavior of the protocol is a behavior of the atomic ref database
> `GitRefDB` under the mapping that reads the database state from the manifest
> the pointer names. In particular: each change of the published refs applies
> commands of one push, each applied command names as its old value the value
> the ref held immediately before the change, and a push whose conditional
> write fails changes nothing.

**Argument.** A request observes the pointer once, in step 1, and every later
step works from that observation: git validates each command against the refs
hydrated from `m_before`, and the conditional write in step 7 is predicated on
the ETag `e` read in step 1. By A3 the write succeeds only if the pointer's
current ETag is `e`. Under the ETag assumption E1 (§Mechanized Verification)
that implies the pointer still holds `d_before`, so at the instant of the
write the published refs are exactly the refs git validated against. The whole
push therefore takes effect at that instant as one step of the atomic database:
the applied commands have the right old values, and the refs they did not touch
keep their published values. A request whose write fails publishes nothing and
is answered with a conflict. The default-branch setter (§Default-branch
management) follows the same discipline and is one further kind of atomic step.

The comparison in step 7 is on the ETag, which may be a function of the pointer
body alone. That is sufficient. If the pointer's body returns to an earlier
value, the manifest it names is the same manifest, with the same refs, HEAD and
packs, so a push computed from the earlier observation is also correct against
the current state. Because a manifest records its predecessor, a body in fact
never recurs (the Lean theorem `pointer_depth_eq_writes`), and a successful
write implies that no other write that changed the pointer happened since the
read (`cas_sees_no_intervening_write`; the Lean model omits the default-branch
setter, whose same-value write rewrites the same body and so preserves the
argument of the previous paragraph).

*Model:* the temporal property `Refines`. Removing the CAS guard, predicating
the write on a later observation than the one the workspace was built from, a
store whose ETag does not distinguish bodies, and sending the response before
the write each violate it.

### Theorem 4 (Authorized Publication)

> A request reaches step 4 only if the push policy accepted its command list
> and `receive-pack` changed at least one ref. A request that is answered from
> git's output without a publication reported `ok` only for commands that
> asked for no change.

**Argument.** Step 3 continues to step 4 only if the workspace refs differ from
`m_before.refs`. By G1 `receive-pack` changes a ref only after the pre-receive
hook accepted the command list, and the hook accepts only what the push policy
accepts. The second sentence restates the observation used for Theorem 1(b): a
command that changes a ref and is reported `ok` changes the workspace.

*Model:* the invariants `PublishIsAuthorizedChange` and `NoSilentDrop`. Both
fail for the rule this protocol used before (publish when git exits 0 and
reports no `ng`), which the model keeps as the seeded error
`Decision = "legacy"`.

## 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. A racer
   whose outcome is *unknown* (a socket or send failure, or a 5xx answer) is
   dropped from the
   round; every other answer is *classified*. **Pass** iff at least two racers
   classify, exactly one classified racer succeeds, every other classified racer
   is precondition-failed (any other answer, such as a 403, fails the probe),
   and a read right after the round returns the winner's body under the
   winner's ETag. That read is what keeps a dropped racer's write from passing:
   its outcome is unknown, so a backend that committed it and then answered 5xx
   must still leave the winner as the stored pointer. 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,
   with the same drop rule: at least two classified racers, exactly one create
   wins among them, the rest are precondition failures, and the final body is
   the racers' (identical, content-addressed) bytes.
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 nothing computed from it may be
  published (the seeded error `stale-base` is that mistake). The client
  re-pushes, which re-hydrates against the advanced state — that is the only
  safe retry, and `git` itself drives it.
- **Publication decided from observed refs.** `observe_push` takes the snapshot
  of the workspace after `receive-pack` (`snapshot_workspace`) and passes it,
  with the hydrated parent refs and git's exit status, to `push_disposition`,
  which returns `RelayOnly`, `Publish` or `Abort` exactly as §Push step 3
  prescribes. `finalize_push` calls `cas_publish` only for `Publish` and hands
  it the same snapshot, so the refs that are compared are the refs that are
  published. The snapshot parser fails closed: output it cannot read is an
  error, never an empty or partial ref set. The table-driven test
  `push_is_published_exactly_when_receive_pack_changed_refs` runs real `git`
  through the production `run_git_at` and `observe_push` for a request with no
  commands, a declined push with and without a status report, an accepted push,
  a command that asks for the value a ref already has, a push in which one ref
  is updated and another refused for its old value, and a push that creates
  two refs whose names conflict, of which git creates one and refuses the
  other. Which of the two git creates differs between git versions; the test
  accepts either and requires that each ref is in the snapshot exactly when
  git reported `ok` for it. The test is Unix-only because its hook fixture
  sets file modes. Two
  tests cover `finalize_push` itself and need Postgres and an object store:
  `finalize_push_publishes_nothing_when_receive_pack_changed_no_ref` checks
  that an unchanged workspace leaves the pointer unwritten and stores no
  kind:30618 event, and `e2e_git::git_partial_push_publishes_accepted_refs`
  drives a partially refused push through a live relay.
- **kind:30618 derived after CAS.** `cas_publish` is reached only for a push
  that changed refs, so every successful publication is followed by one
  kind:30618 event and a push that changed nothing emits none. The event is
  built by `manifest_event::build_ref_state_event` from `CasSuccess.manifest` —
  the values that were written by the CAS. 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.
- **kind:30618 order follows the manifest chain.** kind:30618 events are
  stored side by side, and readers take the one with the greatest
  `created_at` (lowest id on a tie). Stamping each event with the emitting
  instance's clock let an older state win: two pushes in one second tie, and a
  later push on a slower clock sorts first. Each published manifest therefore
  carries `published_at`, strictly greater than its parent's (`now + 1` after
  an unstamped parent, such as the announce-time seed), and the derived event
  uses it as `created_at`. Since the manifests form a chain under CAS, the
  newest event is the newest manifest regardless of which instance emits it
  or when. The field is omitted when absent, so the shared empty seed and
  manifests written before the field existed keep their digests. The argument
  for a manifest whose parent carries no stamp rests on an assumption about
  clocks; see "Order of ref-state events" in §Mechanized Verification.
- **A landed CAS stands when the serving lease lapses after it.** The pointer
  CAS runs under the community serving-write lease, and the lease check after
  the operation can fail because the heartbeat missed a renewal, not only
  because deletion has fenced the community. The CAS cannot be undone at that
  point, so `finalize_push` (and the default-branch setter) keeps its outcome
  instead of answering 503, and lets the lease-guarded 30618 insert decide
  whether publication may continue. Lease loss *during* the operation still
  drops it and answers 503; whether the pointer PUT landed is then unknown.
- **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).

**Code correspondence.** The implementation is in
`crates/buzz-relay/src/api/git/`. The table names the symbol for each element
of the specification; symbols are given without line numbers because those
drift.

| Spec element | Code |
|---|---|
| `Manifest { version, head, refs, packs, parent, published_at }` + `canonical_bytes` | `manifest.rs` |
| `next_published_at` (stamp strictly after the parent's) | `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` |
| §Push step 1: `hydrate_for_write` → `(HydratedRepo, ParentState)` | `hydrate.rs` |
| §Read: `hydrate_for_read` | `hydrate.rs` |
| Bounded digest-keyed pack/index cache and single-flight population | `pack_cache.rs` |
| §Push step 2: `receive_pack`, `install_hook`, the policy callback | `transport.rs`, `hook.rs`, `policy.rs` |
| §Push step 3: `snapshot_workspace`, `push_disposition`, `observe_push` | `cas_publish.rs`, `transport.rs` |
| §Push steps 4–7: `cas_publish(.., &parent_state, &workspace, ..)` | `cas_publish.rs` |
| Proactive full-closure pack compaction before manifest capacity | `cas_publish.rs` |
| `ParentState { if_match, parent_digest, parent }` + `from_loaded`/`fresh` | `cas_publish.rs` |
| `CasError::Conflict { winner_manifest, winner_manifest_key }` (typed 412) | `cas_publish.rs` |
| `build_ref_state_event(&RefStateInputs, &Keys)` (NIP-34 kind:30618) | `manifest_event.rs` |
| `PushContext { pack, parent_state, repo_handle, … }` | `transport.rs` |
| §Push step 8: `finalize_push(state, ctx) -> Response` — **the seam** | `transport.rs` |
| `build_git_response` (sole `Body::from(stdout)` site) | `transport.rs` |
| Default-branch setter: `DefaultBranchSnapshot::set` | `settings.rs` |
| `protect_landed`: a landed conditional write stands when the lease lapses after it | `buzz-deletion`; called from `transport.rs`, `settings.rs` |

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 item to add
once a mockable-CAS seam exists. The no-lost-update claim is exercised
end-to-end by the live N-way concurrent-push test
(`e2e_git::git_concurrent_push_one_wins_and_repo_recovers`), which needs
Postgres and an object store.

## Mechanized Verification

This section separates what is defined, what is assumed, what has been checked
by a tool, what is supported by tests of the implementation, and what is only
proposed. The TLC and Lean results can be reproduced with two commands:
`docs/spec/check.sh` (TLC, pinned to version 1.7.4 by SHA-256; needs Java) and
`lake build` in `docs/spec/lean` (Lean 4.33.1, no dependencies). Both run in CI
when a file under `docs/spec/` changes. The Quint results are reproduced with
the commands given in "Results checked with Quint"; they are not run in CI.

### Definitions

Two TLA+ modules define the claim.

`GitRefDB.tla` is the specification. It describes a database of refs and a HEAD
with no object store and no concurrency control. A push is an invocation (the
client submits commands, and it is recorded whether the push policy authorizes
them), one atomic step in which a subset of the commands is applied, and a
response. A command may be applied only if the push is authorized and only if
its old value is the ref's current value. A command whose new value equals its
old value can be applied; it confirms the value of the ref and changes nothing. A
response may report the true per-ref outcome, report nothing, or be an error;
it may not report an outcome that did not occur. The module also records which
actor the published state is attributed to, which stands for the pusher named
in the kind:30618 event.

`GitOnObjectStore.tla` is the protocol of §Push together with a default-branch
setter, a reader, and repository creation. Its state is the pointer, the
manifest store, the pack store, and the local state of each request. A manifest
is a record of refs, HEAD, packs and (optionally) predecessor. A pack is a set
of objects, and objects refer to other objects, so reachability and closure are
computed, not asserted. `receive-pack` is one step that chooses which commands
to apply, subject to G1 below, and may exit abnormally after applying some.

The correctness statement `Refines` says that every behavior of
`GitOnObjectStore` is a behavior of `GitRefDB`, where the abstract database is
read from the manifest the pointer names. The abstract outcome of a push is
fixed at its conditional write, or, for a request that publishes nothing, at
its read of the pointer. TLC checks this as a temporal property: every
step of the protocol must be a step of the specification or leave the abstract
state unchanged.

### Assumptions

The checked results hold under the following assumptions. None is verified
here.

- **A1–A3** (§Axioms): durable create-only writes, read-after-write, and a
  linearizable conditional write on the pointer.
- **E1 (ETag).** If the pointer's ETag equals the ETag a request read, the
  pointer's body equals the body that request read. A store whose ETag changes
  on every write satisfies E1. So does a store whose ETag is a digest of the
  body, provided that digest does not collide on two pointer bodies that occur.
  On S3 the ETag of such an object is an MD5 digest, and the body is the
  hexadecimal SHA-256 digest of a manifest; E1 then asks that no two manifest
  digests published for one repository have the same MD5.
- **H1 (digests).** SHA-256 does not collide on the manifests and packs that
  occur. The models identify a digest with the value it names.
- **G1 (`git receive-pack`).** `receive-pack` changes a ref only by applying a
  command the client submitted; only after the pre-receive hook accepted the
  whole command list; only if the command's old value is the ref's current
  value in the workspace; and only if every object reachable from the new value
  is present. It may refuse any command and may exit abnormally after applying
  some. The hook accepts exactly what the push policy accepts. This is git's
  documented behavior, and the test named in §Implementation Correspondence
  exercises the cases that matter here against the installed git, but git
  itself is not verified.
- **Policy.** Whether the push policy's decision is the right one is outside
  these models. They record its answer as a boolean per push.

### Results checked by TLC

TLC explores every reachable state of a finite instance. The base instance has
two concurrent pushing clients, two refs, the default-branch setter, repository
creation, and compaction when a manifest lists two packs. The ETag is a
function of the body and manifests do not record a predecessor. This is the
weakest comparison a conforming store can provide (the write succeeds in the
most situations), and it makes the state space finite without any bound on the
number of pushes, so the base check covers behaviors of unbounded length. The
other instances vary one dimension each.

| Check | Instance | Distinct states | Result |
|---|---|---|---|
| `refdb` | the specification alone, one client; its stated consequences | 11,262 | pass |
| `push` | base instance | 2,349,839 | pass |
| `objects` | one client, two objects (one refers to the other), reader | 531,099 | pass |
| `three-clients` | three clients, one ref | 91,039 | pass |
| `stale-commands` | a client may name an old value other than the hydrated one | 43,314 | pass |
| `parent-links` | manifests record their predecessor; at most 3 pointer writes | 1,329,939 | pass |
| `version-etag` | ETag changes on every write; at most 3 pointer writes | 505,468 | pass |
| `no-view` | base instance without the setter and without state identification | 6,773,286 | pass |

Each passing check establishes, for its instance, `Refines` and the invariants
`Fence`, `ReaderComplete`, `PublishedClosed`, `HeadPublished`, `NoSilentDrop`
and `PublishIsAuthorizedChange`, and the action property `ParentIsPredecessor`
(a pointer write that changes the manifest names the manifest it replaced,
where predecessors are recorded). `ReaderComplete` constrains only `objects`,
the instance with a reader. The whole suite takes about three minutes on a
16-core machine and about ten minutes on a GitHub-hosted runner.

The instances identify states that differ only in stored objects that nothing
reads (a TLC `VIEW`), and treat clients as interchangeable (`SYMMETRY`). The
argument that the first loses nothing is given in `MCGitOnObjectStore.tla`, and
`no-view` repeats the check without it.

### Seeded design errors

A property that cannot fail constrains nothing. Each row below changes the
design in one way, and `check.sh` requires TLC to report a violation of the
named property; the suite fails if a seeded error goes undetected. The view is
not used for these runs.

| Seeded error | Violates |
|---|---|
| publish when git exits 0 and reports no `ng` (the original rule): a declined or empty push is published | `PublishIsAuthorizedChange` |
| the original rule, mixed outcome: the client is told `ok` for a ref that is not published | `NoSilentDrop` |
| the original rule, git exits abnormally after applying a command | `NoSilentDrop` |
| the original rule, as a whole | `Refines` |
| publish when git exits 0 and reports an `ok` or no `ng` (the status-report rule): a declined or empty push is published | `PublishIsAuthorizedChange` |
| the status-report rule, git exits abnormally after applying a command | `NoSilentDrop` |
| the status-report rule, as a whole | `Refines` |
| no pre-receive hook | `PublishIsAuthorizedChange` |
| pointer write without the condition | `Refines` |
| condition taken from a later pointer read than the one the workspace was built from | `Refines`, `ParentIsPredecessor` |
| ETag that does not distinguish bodies (against a push; against the setter) | `Refines` |
| response sent before the pointer write | `Refines` |
| pointer write before the uploads | `Fence` |
| deletion of a pack that the current manifest does not list | `Fence`, `ReaderComplete` |
| a delta push that drops the packs it inherits | `PublishedClosed` |
| `receive-pack` without the connectivity check | `PublishedClosed` |

The first seven rows concern the two rules the relay used before the present
one. Both decided from git's exit status and the lines of its status report.
The original rule treated any `ng` line as "nothing happened". The status-report
rule repaired the mixed outcome by publishing whenever an `ok` line is present.
Neither sees a status report from a client that did not negotiate one, and
neither sees any line for a request without commands, so both publish in those
cases. The model was written against what git can do and not against the status
report, and for either rule it produces a counterexample of four states: the
repository is created, a request arrives, `receive-pack` declines it, and the
request is on the publish path, where the published state would be attributed
to the caller.

One further check, `relayed-ok`, asserts something that is not required (that a
request answered without a publication never carries an `ok`) and must be
violated by the protocol as specified. It shows that the model reaches the case
of a command that asks for no change, which Theorem 1(b) and Theorem 4 make an
exception for.

### Results proved in Lean

`docs/spec/lean/GitPointer.lean` proves the pointer discipline for arbitrary
types of clients, refs, objects and packs, with no finiteness assumption. The
model there has four steps (read the pointer and stage a successor, upload,
conditional write, abort) and arbitrary relations for which ref states may
follow which, which objects a ref state reaches, and which objects a pack
holds. Its one hypothesis about the store is E1. For every reachable state it
proves:

- `fence`: the manifest the pointer names and the packs it lists are stored
  (Theorem 1a).
- `closed`: those packs contain every object reachable from the manifest's
  refs, derived from the three rules for composing a pack list (Theorem 2).
- `pointer_step_legal`: every step leaves the pointer unchanged or replaces it
  with a manifest computed as a legal successor of the value it replaces
  (the pointer part of Theorem 3).
- `pointer_depth_eq_writes` and `cas_sees_no_intervening_write`: a pointer body
  never recurs, and a successful conditional write implies that no other write
  that changed the pointer happened since the read (the Lean model omits the
  default-branch setter, whose same-value write rewrites the same body and so
  preserves the argument of the previous paragraph).

`write_is_possible` shows that a successful write is reachable, so the results
do not hold vacuously. The proofs use no axioms beyond Lean's standard three
(`propext`, `Classical.choice`, `Quot.sound`).

The Lean model is narrower than the TLA+ model. It does not contain the publish
decision, the responses to clients, the default-branch setter, the reader, or
`receive-pack`; "legal successor" is a parameter. The two models are related by
reading, not by a mechanical link.

### Results checked with Quint

The TLA+ and Lean models contain neither the serving-write lease nor the
kind:30618 events. `docs/spec/GitPushPath.qnt` is a Quint model of the push
path that contains both. Two pushers each fetch the ref advertisement and then
send a receive-pack request, which hydrates from whatever pointer is current
when it runs. A request names at most two of three refs (which include the
directory/file pair `feature` and `feature/x`), may name none, and may come
from a client that did not negotiate a status report. The publish decision,
the lease and the event timestamps follow `finalize_push`. Each relay instance
reads a clock that may run one second ahead. The invariants are stated over
what clients observe:

| Invariant | Statement |
|---|---|
| `noFalseSuccess` | a ref the client printed as `ok` reached the published pointer |
| `noFalseFailure` | a ref the client was told failed did not reach the pointer |
| `refStateMatchesPointer` | once pushes settle, the kind:30618 event that readers select matches the pointer |
| `publicationChangesRefs` | every published manifest differs in its refs from the one it replaced |

The module `fixed` is the implementation: the publish decision of §Push step
3, a landed conditional write kept when the lease lapses after it, and events
stamped with the manifest's `published_at`. The other modules each restore one
earlier behavior, so that a counterexample is attributed to one defect.

| Module | Restores | Result |
|---|---|---|
| `fixed` | nothing | all four invariants hold |
| `partialBugOnly` | the original publish rule | violates `noFalseSuccess` and `publicationChangesRefs` |
| `reportRuleOnly` | the status-report publish rule | violates `publicationChangesRefs`; `noFalseSuccess` and `noFalseFailure` hold |
| `leaseBugOnly` | a landed write reported as a failure when the lease lapses | violates `noFalseFailure` |
| `timestampBugOnly` | events stamped with the emitting instance's clock | violates `refStateMatchesPointer` |
| `current` | all three original behaviors | violates `safety` |

The results were obtained with Quint 0.33.0 in two ways. Random simulation
explores runs of at most 14 steps:

```
quint run docs/spec/GitPushPath.qnt --main fixed --invariant safety \
  --max-steps 14 --max-samples 2000000 --seed 0x1
```

For `fixed` it reports no violation of `safety` (the conjunction of the four
invariants) in 2,000,000 runs. For `reportRuleOnly`, the same command with one
invariant at a time reports no violation of `noFalseSuccess`, `noFalseFailure`
or `refStateMatchesPointer` in 2,000,000 runs each, and a counterexample for
`publicationChangesRefs`. Each of the other modules produces a counterexample
for the invariant named in the table. Simulation samples runs; the absence of a
violation is evidence, not a proof.

The second way is a bounded symbolic check, which considers every run up to
the bound:

```
quint verify docs/spec/GitPushPath.qnt --main fixed --invariant safety \
  --max-steps 8
```

With Apalache 0.62.1 this reports no violation for `fixed` (81 seconds), and
the same command for `reportRuleOnly` with `publicationChangesRefs` returns a
counterexample. A push that publishes takes four steps (advertisement,
receive-pack, conditional write, event), so the bound of eight covers every
interleaving of the two pushes in which the clock does not advance. Runs in
which it advances between steps of both pushes are longer, and are covered by
simulation only.

A `reportRuleOnly` counterexample is a request that changes no ref and whose
visible report has no `ng` line: a request with no commands, or a declined push
from a client that did not negotiate a status report. The status-report rule
publishes it. In the Quint model the published refs equal
their predecessor's, so the client-facing invariants still hold; what the
publication adds is a pointer write and a kind:30618 event that names the
caller as the pusher. The TLA+ model, which has the push policy, reports the
same behavior as a violation of `PublishIsAuthorizedChange` (the seeded error
`report-unauthorized`).

### Evidence about the implementation

The models are about the design. Three things connect them to the code. The
publish decision is a pure function, `push_disposition`, whose three outcomes
are the three branches of the model's `Disposition`, and a unit test covers its
cases. The test `push_is_published_exactly_when_receive_pack_changed_refs` runs
the production subprocess path against real git for seven ways a push can
end, and fails if the decision is changed to depend on the exit status alone.
The test `finalize_push_publishes_nothing_when_receive_pack_changed_no_ref`
calls `finalize_push` with an unchanged workspace against Postgres and an
object store, and fails in the same way under that change. The remaining
correspondence (one pointer observation per request, uploads before the
conditional write, the response built only in `finalize_push`) is by the
structure described in §Implementation Correspondence and by the other
storage-backed tests.

The storage-backed tests of `finalize_push` and `e2e_git` are marked ignored
and are not selected by any CI job at the time of writing, so they are evidence
only when someone runs them. The seven-case test needs no services and runs in
the Unix unit-test jobs.

### Assumptions and limitations

- The TLC results are exhaustive for the instances listed and say nothing
  directly about larger ones. Two clients with two objects and two refs is
  beyond what the suite can check in reasonable time. The Lean results remove
  the bound for the pointer discipline only.
- Hydration is one atomic step in the push model. The reader process covers
  reads that are interleaved with writes.
- Only safety is covered. Nothing here shows that a push eventually succeeds.
- Deletion of stored objects is modeled only as a seeded error. A garbage
  collector would need its own model, with the reader and the upload-then-write
  window as the cases it must respect.
- The TLA+ and Lean models do not include the relay's database, the
  serving-write lease, request authentication, or the kind:30618 event stream.
  The Quint model includes the lease and the events, with the bounds stated in
  its section, and is not connected to the other two by any mechanical link.

### Order of ref-state events

Two pushes can win their conditional writes in the order A, B and then store
their kind:30618 events in the order B, A, because event storage happens after
the write and nothing orders the two requests. When each event carried the
time at which its relay instance built it, a consumer that reads ref state from
the newest event could then see A's refs although the pointer holds B's. Two
pushes within one second, or a later push handled by an instance with a slower
clock, had the same effect.

The implementation removes the dependence on storage order and on the emitting
clock. Every manifest written by a push or by the default-branch setter carries
`published_at`, computed by `next_published_at` as the later of the current
time and one second after the parent's stamp, and the derived event uses that
value as its `created_at`. Stamps therefore increase strictly along the chain
of manifests, and the chain is totally ordered by the conditional write
(Theorem 3), so the event with the greatest `created_at` is the event of the
manifest the pointer names. `refStateMatchesPointer` in the Quint model checks
this for stamped manifests, and `timestampBugOnly` shows the earlier behavior
violating it.

**Assumption C1 (clocks, unstamped parent).** Two manifests carry no stamp: the
empty manifest written when a repository is announced, whose bytes are shared
by all repositories, and any manifest written before the field existed. The
event of such a manifest was stamped with the clock of the instance that
emitted it. Its successor takes the current time plus one second on the
instance that writes it. The successor's event is selected over the
parent's only if that value exceeds the parent event's `created_at`. This
holds when one instance handles both, and otherwise when the writing
instance's clock is not behind the other's by more than the time that passed
between the two events. C1 states that it holds. It concerns one write per
repository (the first after creation, or the first after the field was
introduced); every later manifest has a stamped parent. C1 is established by
reading the code. It is not modeled: the Quint model starts from a stamped
manifest. If C1 fails, readers of the newest event see the parent's refs until
the next push, and the pointer is unaffected.

### Proposed extensions

- Bind publication to the policy decision itself: have the policy endpoint
  record, per request, the command list it approved, and have step 3 require
  that the observed ref changes are a subset of an approved list. This would
  replace assumption G1's clause about the hook with a check in the relay.
- Remove assumption C1, for example by having the first push after an
  unstamped manifest read the `created_at` of the stored event and exceed it,
  and model the unstamped case in Quint.
- Run the Quint checks in CI with a pinned Quint and Apalache.
- Run the storage-backed `finalize_push` tests in CI. Their fixture applies the
  migrations itself, which the CI database (built from the desired-state
  schema) does not expect, so the fixture needs the schema-mode switch the
  other storage-backed suites use.
- A mechanical link between the Lean model and the TLA+ model, or a proof of
  the full refinement for unbounded parameters.

### Names used by earlier revisions

Code comments and a database migration cite invariant names from an earlier
model. They are kept as aliases in `GitOnObjectStore.tla`: `Inv_NoFork` and
`Inv_RefEffectApplied` stand for `Refines`, `Inv_RefDerivedFromParent` for
`ParentIsPredecessor`, and `Inv_Closed` for `PublishedClosed`.

## Summary

| Property | Evidence | Relative to |
|---|---|---|
| Durability-ordering (T1) | TLC, finite instances; Lean (`fence`), unbounded | A1, A2 |
| Manifest reconstruction (T2) | TLC, finite instances; Lean (`closed`), unbounded | A1, A2, G1; git upstream |
| Linearizable refs (T3) | TLC refinement, finite instances; Lean (`pointer_step_legal`), unbounded, pointer discipline only | A3, E1, H1, G1 |
| Authorized publication (T4) | TLC, finite instances | G1; policy correctness not covered |
| Landed write reported as landed; ref-state events ordered as the manifests | Quint, bounded | C1 |
| Model matches the code | Tests and review | — |
| A1/A2/A3 hold on backend | Empirical | Conformance probe (gate) |
| Liveness / latency | Empirical | Benchmark (out of scope) |