docs: formal spec + machine-checked proof for git refs over object storage#721
Merged
Conversation
…orage Adds a formal specification and TLA+ proof for hosting git repositories on conditional-write object storage (S3 / S3-compatible), under no-persistent-disk. - docs/git-on-object-storage.md: the spec + prose proof. Repository state is a set of create-only, content-addressed pack objects plus one mutable manifest pointer updated by atomic compare-and-swap. Proves three safety theorems (durability-ordering, manifest reconstruction, ref-update linearizability), each reduced to three explicitly stated, empirically-gated object-store axioms (durable write; strong read-after-write; linearizable conditional PUT). - docs/spec/GitOnObjectStore.tla (+ .cfg): TLA+ model, TLC-checked (435,745 distinct states, no violation) under a BoundedManifests constraint. Eight invariants, each proven non-vacuous by a mutation that trips it. - Scope is honest: safety is machine-checked relative to the axioms; liveness and performance are empirical (out of scope); a backend is admitted per deployment by a conformance probe, not proved universally. The algorithm is git's own (reftable: immutable artifacts + atomic pointer swap), with the atomic primitive substituted from POSIX rename() to an S3 conditional PUT; the contribution is the formal characterization. The publish-ordering fence is implemented in crates/sprout-relay/.../transport.rs (branch quinn/transport-fence-typesplit @ 17df788) via a PushContext -> finalize_push seam; S3 manifest-CAS and 412->409 are named future work. Authored by the Sprout agent team (Eva lead; Dawn, Max, Mari, Perci, Quinn review) under direction of tlongwell-block. Signed-off-by: tlongwell-block <109685178+tlongwell-block@users.noreply.github.com> Co-authored-by: Eva (sprout agent) <18234bd709ff00c47a3b66f001675bd14c07700d862ed61c21a4423dcc1d9687@sprout-oss.stage.blox.sqprod.co>
This was referenced May 28, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
A formal specification and machine-checked (TLA+) proof for hosting git repositories on conditional-write object storage (S3 / S3-compatible), with no persistent filesystem.
docs/git-on-object-storage.md— spec + prose proof. Repo state = create-only, content-addressed pack objects + one mutable manifest pointer updated by atomic compare-and-swap. Proves three safety theorems (durability-ordering, manifest reconstruction, ref-update linearizability), each reduced to three explicitly stated object-store axioms.docs/spec/GitOnObjectStore.tla(+.cfg) — TLA+ model, TLC-checked: 435,745 distinct states, no violation, under aBoundedManifestsconstraint. Eight invariants, each proven non-vacuous by a mutation that trips it.Why it's defensible
The algorithm isn't novel — it's git's own reftable model (immutable artifacts + atomic pointer swap), with the atomic primitive substituted from POSIX
rename()to an S3 conditionalPUT. The contribution is the formal characterization of git refs over conditional-write object storage, which prior-art search (incl. arXiv) found unaddressed.Honest scope boundary
Implementation status
The publish-ordering fence is real code in
crates/sprout-relay/.../transport.rs(branchquinn/transport-fence-typesplit@17df7884): aPushContext → finalize_pushseam where the compiler enforces "no push response without going through the fence," with six decision tests covering every arm including the both-snapshots-fail case. S3 manifest-CAS and the412→409mapping are named follow-up work.Provenance
Authored by the Sprout agent team — Eva (lead), with review from Dawn, Max, Mari, Perci, and Quinn — under direction of @tlongwell-block. Six review rounds; every pass caught what the last missed. Doc-only change (plus the referenced relay branch); no production code in this PR.