fix(relay): Git pushes report and publish what actually landed - #9064

…ocol by refinement (#9425)

## 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::git::/) +
test(/side_effects/)'`: 158 passed.
- The storage-backed `finalize_push` tests
(`api::git::transport::track_c_tests::external_infra_minio_tests`, with
`--run-ignored ignored-only`) against local Postgres and MinIO: 5
passed.
- `e2e_git` against a local relay built from this branch, with Postgres,
Redis and MinIO: 3 passed (clone/push/fetch/force-push round trip,
concurrent push, partially refused push). The storage probe in that test
needs `BUZZ_E2E_GIT_COMMUNITY_ID` set to the local community's id.
- `just file-size-check` and `just security-review-check`: pass.

Two regression tests bind the changed decision to production code, and
both were confirmed to fail when the decision is forced back to the exit
status:

- `push_is_published_exactly_when_receive_pack_changed_refs` runs real
git through the production `run_git_at` and `observe_push` for seven
ways a push can end: a request with no commands, a push the hook
declines with and without a status report, an accepted push, an accepted
command that asks for the value the 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. It needs no services. Which of the two conflicting
refs git creates depends on the git version (2.50 creates the first
command's ref, 2.56 on the flake-check runner creates the other), so the
test accepts either outcome and requires that each ref is in the
published snapshot exactly when git reported `ok` for it. The first
version of this case assumed one outcome and failed the Rust flake check
for that reason. Before #9429, `just test-unit` selected neither
`api::git::cas_publish::tests` nor `api::git::transport::track_c_tests`,
so this test ran only in the flake check; both modules are now in the
unit-test lane (45 tests, none needing services). It is Unix-only
because its hook fixture sets file modes; the first push of this PR
failed Windows clippy for that reason, and the test and its fixture are
now gated with `#[cfg(unix)]`. That gating has not been compiled for
Windows locally, so the Windows CI job is the check.
- `finalize_push_publishes_nothing_when_receive_pack_changed_no_ref`
calls `finalize_push` with an unchanged workspace and checks that the
pointer is not written and no kind:30618 event is stored. It needs
Postgres and an object store.

Not done, or not covered:

- No CI job selects the storage-backed `finalize_push` tests or
`e2e_git`, so the second regression test and the end-to-end tests are
evidence only when someone runs them. Adding them to CI needs a change
to the test fixture, which applies migrations itself, and is left as a
follow-up.
- `just ci` was not run in full.
- No human has tested the change. The human-testing step of the
readiness checklist in `AGENTS.md` is not met, and
`buzz-review-completed` is not claimed.

The local secret-scanning hook (`sadscan`) was skipped for the commits
and pushes that touch `crates/buzz-relay/src/api/git/settings_tests.rs`.
It scans whole files and flags the P-256 test key fixtures that file
already contains on `main`; this branch adds no key material.

---------

Signed-off-by: Jordan Mecom <[email protected]>
Signed-off-by: Tom Brow <[email protected]>
Co-authored-by: Tom Brow <[email protected]>
Co-authored-by: studio <dc2fc481343672df31a689840c09299972e704dac592e0da6f18486646a7ee3e@localhost>