mirror of
https://github.com/block/buzz.git
synced 2026-11-13 21:01:53 +00:00
1fb33e4545
## Summary This PR is stacked on #9064. It does two things to the Git-on-object-storage code in `buzz-relay`. It replaces the TLA+ model of the push protocol with one that states what the protocol is supposed to implement and checks that it does. It also changes the rule by which the relay decides whether to publish a push, because the new model shows that the rule #9064 introduces still publishes requests in which git accepted nothing. ### Relationship to #9064 The branch is `main`, then the two commits of #9064, then four commits of this PR: the specification work, the publish-rule change, a review fix merged from #9429, and a fix to `check.sh`. A merge of `main` follows them; it was needed because `main` changed `Justfile`, which #9429 also edits, after the branch point. The first two commits are #9064's, replayed onto current `main` without conflicts and otherwise unchanged. The base of this PR stays `main` because #9064's branch is about 200 commits behind it. Once #9064 merges, this branch can be rebased and the diff shrinks to the last four commits. Until then, review the commits after the first two. This PR keeps two of #9064's three changes as they are: the `published_at` stamp that orders kind:30618 events by the manifest chain, and `protect_landed`, which lets a landed conditional write stand when the serving lease lapses after it. It replaces the third, the publish rule. ### The publish rule #9064 publishes when git exits 0 and the status report has an `ok` line or no `ng` line. That handles a push in which one ref is updated and another refused. The report, however, is not evidence of what git did. - git exits 0 for a request that carries no commands, and for a push the pre-receive hook declined. A decline is reported only to a client that negotiated `report-status`. For a request with no commands, and for a decline when the client did not negotiate a report, there is no `ng` line. The relay then writes the pointer and emits a relay-signed kind:30618 event that names the caller as pusher, although the push policy approved nothing. - The report is read from a stream whose framing the client's capabilities determine, so the decision depends on parsing a client-shaped stream. The decision is now taken from the workspace. `push_disposition` compares the refs after receive-pack with the refs the workspace was hydrated from. Unchanged refs are answered with git's own output and nothing is published. Changed refs are published if git exited normally. Changed refs after an abnormal exit fail the request. The snapshot that is compared is the one `cas_publish` publishes, so git's per-ref report is true of the published state. The status-report scanner and its tests are removed, and the ref-name conflict case they covered moves into the table-driven test described below. Three smaller changes follow. The ref-snapshot parser now fails closed: output that was not UTF-8 used to read as an empty ref set and a malformed line was skipped, and either would publish a manifest that lacks refs. `manifest_changed` in `finalize_push` could not be false and is removed. Taking the snapshot before the publish decision moved its resource-limit error (snapshot larger than 4 MiB, or more refs than a manifest may hold) onto a path that answered 500; #9429 restores the 413 the publish path gave before and adds `snapshot_resource_limit_answers_413`. ### What the specification work adds - `docs/spec/GitRefDB.tla` is the specification: a ref database in which a push takes effect in one step, is applied only if authorized and only against the old values it names, and is reported truthfully. - `docs/spec/GitOnObjectStore.tla` is the protocol: several refs, an object graph with reachability, packs, compaction, the pre-receive hook, the publish decision, the default-branch setter, repository creation, and a reader. `git receive-pack` is represented by a stated contract rather than modeled internally. - The correctness statement is `Refines`: every behavior of the protocol is a behavior of the specification. TLC checks it together with the store invariants (fence, reader completeness, closure of published manifests). - `docs/spec/check.sh` pins TLC 1.7.4 by SHA-256 and runs 28 checks. Eight instances must pass. Nineteen seeded design errors must each be detected with the violation named for them. One coverage check confirms that a behavior the properties depend on (git reporting `ok` for a command that changes nothing) is reachable. A name passed to `check.sh` that is not a check is an error, so a misspelled selection cannot report success. - Both earlier publish rules are among the seeded errors: the original rule (exit 0 and no `ng`) and #9064's status-report rule. For each, TLC reports a publication the policy did not approve (`PublishIsAuthorizedChange`) and a violation of `Refines`. - `docs/spec/GitPushPath.qnt`, the Quint model from #9064 that covers the serving lease and the event timestamps, is extended. The publish rule becomes a parameter with three values, a request may carry no commands or come from a client without a status report, and a new invariant, `publicationChangesRefs`, states that a published manifest differs in its refs from the one it replaces. The implemented rule satisfies all four invariants; the status-report rule violates the new one with a zero-command request. - `docs/spec/lean/GitPointer.lean` is a Lean 4 proof, with no dependencies, of the pointer discipline for any number of clients, refs and objects: the fence, closure, that every pointer change is a legal step from the value it replaces, that the length of the pointer's predecessor chain equals the number of pointer writes, and that a successful conditional write implies no intervening write. - `.github/workflows/spec.yml` runs TLC and Lean when a file under `docs/spec/` changes. On this PR's first run the TLC job took 10 minutes 19 seconds and the Lean job 22 seconds. Quint is not run in CI. - `docs/git-on-object-storage.md` is revised to match. The push listing follows the implemented order. The verification section separates definitions, assumptions, results checked by TLC, results proved in Lean, results checked with Quint, evidence about the implementation, and limitations. The invariant names cited by code comments and by migration 0002 are kept as aliases in the TLA+ module. ### Assumptions and limitations The TLC results hold for the bounded instances in `check.sh`, not for arbitrary sizes. The Lean proof is unbounded but covers the pointer discipline only, not the refinement. The Quint results are from random simulation (2,000,000 runs of at most 14 steps) and a bounded symbolic check (8 steps, Apalache); neither is a proof for unbounded runs. All of them rest on the assumptions named in the document: the object store's conditional-write semantics, ETag equality implying body equality, no SHA-256 collision among the values that occur, the stated contract for `git receive-pack`, and the policy endpoint deciding authorization. The correspondence between the models and the Rust code is established by reading the code and by the tests below; it is not mechanized. The document states one assumption that #9064's ordering fix depends on and that no model covers (Assumption C1). A manifest whose parent carries no `published_at` (the empty manifest written when a repository is announced, or a manifest written before the field existed) is stamped with the writing instance's current time plus one second. Its event is selected over the parent's only if that value exceeds the parent event's `created_at`, which was taken from the clock of the instance that emitted it. 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 elapsed between the two events. The assumption concerns one write per repository. The document lists its removal as a proposed extension, for example by having the first push after an unstamped manifest read the stored event's `created_at` and exceed it. ### Related issue Related to #2621 (CI for the formal models). This adds the TLC job for the git model and a Lean job; it does not cover the Tamarin models or the NIP-PL scripts, so it should not close that issue. ### Testing Run locally on the restacked branch: - `docs/spec/check.sh`: 28 checks, each with the expected result (8 pass, 19 seeded errors violate the named property, 1 coverage witness reached). About three minutes on 16 cores; the largest instance has 6,773,286 distinct states. - `lake build` in `docs/spec/lean` (Lean 4.33.1): succeeds. The safety theorems depend only on `propext`, `Classical.choice` and `Quot.sound`. - Quint 0.33.0, `GitPushPath.qnt`: `quint run --main fixed --invariant safety --max-steps 14 --max-samples 2000000 --seed 0x1` reports no violation; `quint verify --main fixed --invariant safety --max-steps 8` (Apalache 0.62.1) reports no violation; each single-defect module produces the counterexample the document lists. - `cargo fmt --all -- --check` and `cargo clippy -p buzz-relay --all-targets -- -D warnings`: clean. - `cargo nextest run -p buzz-relay --lib -E 'test(/^api::/) + test(/side_effects/)'`: 158 passed. - The storage-backed `finalize_push` tests (`api: