mirror of
https://github.com/block/buzz.git
synced 2026-11-14 13:21:02 +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:
375 lines
18 KiB
Lean4
375 lines
18 KiB
Lean4
/-!
|
||
# Conditional pointer writes for Git on an object store
|
||
|
||
This file proves four safety properties of the storage protocol that
|
||
`../GitOnObjectStore.tla` checks with TLC for small finite instances. The
|
||
proofs here hold for any number of clients, refs, objects and packs. Only core
|
||
Lean is used.
|
||
|
||
## What is modeled
|
||
|
||
A repository is stored as immutable manifests and packs plus one mutable
|
||
pointer that names the current manifest. A writer reads the pointer (`begin`),
|
||
stages a successor manifest computed from the value it read, uploads that
|
||
manifest and its packs (`upload`), and then performs a conditional write of
|
||
the pointer (`cas`), which succeeds only if the ETag of the pointer equals the
|
||
ETag of the value the writer read. A writer may stop at any time (`abort`): a
|
||
lost race, a crash, or a timeout. Writers interleave arbitrarily.
|
||
|
||
`Model.Staged` is the set of manifests a writer may stage from a pointer value
|
||
`p`: the manifest records `p` as its parent, its ref state is a legal successor
|
||
of the ref state of `p`, and its pack list follows one of three rules (no new
|
||
pack, one delta pack added to the packs of `p`, or one pack that replaces them
|
||
all).
|
||
|
||
Two fields are ghost state, used only to state the results: `State.writes`
|
||
counts successful pointer writes, and `Writer.readAt` records the value of that
|
||
counter when the writer read the pointer.
|
||
|
||
## Assumptions
|
||
|
||
* `Model.etag_inj`: the ETag of a pointer body determines the body. This
|
||
stands for two facts about the implementation: the object store assigns
|
||
different ETags to different bodies, and SHA-256 has no collision among the
|
||
values that occur.
|
||
* A digest is modeled by the value it names. `Manifest.parent` therefore holds
|
||
the predecessor manifest itself, and the predecessor chain is finite because
|
||
`Manifest` is an inductive type.
|
||
* Nothing is removed from the manifest store or the pack store. Garbage
|
||
collection is outside this model.
|
||
* `Model.Legal`, `Model.reach` and `Model.objs` are arbitrary relations.
|
||
Nothing is assumed about which ref updates are legal or which objects a ref
|
||
state reaches.
|
||
|
||
## Results (for every reachable state)
|
||
|
||
* `fence`: the manifest the pointer names is stored, and so is every pack that
|
||
manifest lists.
|
||
* `closed`: the packs listed by the pointed-to manifest contain every object
|
||
reachable from its ref state. This is derived from the three pack rules.
|
||
* `pointer_step_legal`: a step either leaves the pointer unchanged or replaces
|
||
it by a manifest whose parent is the replaced value and whose ref state is a
|
||
legal successor of the replaced ref state. No update is lost.
|
||
* `cas_sees_no_intervening_write`: when a conditional write is enabled, no
|
||
pointer write has happened since the writer read the pointer, although the
|
||
ETag depends only on the body.
|
||
* `pointer_depth_eq_writes`: the length of the predecessor chain of the pointer
|
||
equals the number of pointer writes, so a published manifest is never
|
||
published again.
|
||
|
||
`write_is_possible` exhibits an instance in which a conditional write
|
||
succeeds, so the results are not vacuous.
|
||
|
||
## What is not covered
|
||
|
||
The proofs concern the pointer discipline only. The decision whether a push is
|
||
published, the reports sent to clients, the default-branch setter, readers and
|
||
garbage collection are covered by the TLA+ model for finite instances and are
|
||
not formalized here. `Model.Legal` stands for everything `git receive-pack` and
|
||
the push policy permit; this file does not say what that is.
|
||
-/
|
||
|
||
namespace GitPointer
|
||
|
||
/-- A manifest: a published ref state, the set of packs that hold its objects,
|
||
and the manifest it replaced (`none` for the first manifest of a repository). -/
|
||
structure Manifest (R Pk : Type) where
|
||
refs : R
|
||
packs : Pk → Prop
|
||
parent : Option (Manifest R Pk)
|
||
|
||
variable {R Obj Pk Client E : Type}
|
||
|
||
/-- The length of the predecessor chain of a manifest, counting the manifest. -/
|
||
def Manifest.depth : Manifest R Pk → Nat
|
||
| ⟨_, _, none⟩ => 1
|
||
| ⟨_, _, some p⟩ => p.depth + 1
|
||
|
||
/-- The depth of a pointer value; an absent pointer has depth 0. -/
|
||
def depthOpt : Option (Manifest R Pk) → Nat
|
||
| none => 0
|
||
| some m => m.depth
|
||
|
||
theorem Manifest.depth_eq (m : Manifest R Pk) : m.depth = depthOpt m.parent + 1 := by
|
||
cases m with
|
||
| mk r p par => cases par <;> simp [Manifest.depth, depthOpt]
|
||
|
||
/-- The parameters of the protocol. `objs pk o`: pack `pk` contains object `o`.
|
||
`reach r o`: object `o` is reachable from ref state `r`. `Legal b r`: ref state
|
||
`r` may follow base `b`, where `none` is a repository that does not exist.
|
||
`etag` is the ETag of a pointer body, assumed to determine the body. -/
|
||
structure Model (R Obj Pk E : Type) where
|
||
objs : Pk → Obj → Prop
|
||
reach : R → Obj → Prop
|
||
Legal : Option R → R → Prop
|
||
etag : Manifest R Pk → E
|
||
etag_inj : ∀ a b, etag a = etag b → a = b
|
||
|
||
/-- The local state of a writer: the pointer value it read, the manifest it
|
||
staged, whether it has uploaded that manifest, and (ghost) the write count at
|
||
the time of its read. -/
|
||
structure Writer (R Pk : Type) where
|
||
base : Option (Manifest R Pk)
|
||
staged : Manifest R Pk
|
||
uploaded : Bool
|
||
readAt : Nat
|
||
|
||
/-- The global state: the pointer, the manifest store, the pack store, the
|
||
writers in progress, and (ghost) the number of successful pointer writes. -/
|
||
structure State (R Pk Client : Type) where
|
||
pointer : Option (Manifest R Pk)
|
||
mstore : Manifest R Pk → Prop
|
||
pstore : Pk → Prop
|
||
writers : Client → Option (Writer R Pk)
|
||
writes : Nat
|
||
|
||
/-- The initial state: no pointer, empty stores, no writers. -/
|
||
def State.init : State R Pk Client :=
|
||
⟨none, fun _ => False, fun _ => False, fun _ => none, 0⟩
|
||
|
||
/-- `pk` is listed by the manifest `p` names. False when `p` is absent. -/
|
||
def basePacks (p : Option (Manifest R Pk)) (pk : Pk) : Prop :=
|
||
∃ b, p = some b ∧ b.packs pk
|
||
|
||
/-- `g` is `f` with the entry of client `c` replaced by `v`. Stated as a
|
||
relation so that equality of clients need not be decidable. -/
|
||
def Upd (f : Client → Option (Writer R Pk)) (c : Client) (v : Option (Writer R Pk))
|
||
(g : Client → Option (Writer R Pk)) : Prop :=
|
||
g c = v ∧ ∀ c', c' ≠ c → g c' = f c'
|
||
|
||
/-- A writer present after an update is the new entry or was present before. -/
|
||
theorem Upd.cases {f g : Client → Option (Writer R Pk)} {c : Client} {v : Option (Writer R Pk)}
|
||
(h : Upd f c v g) {c' : Client} {w : Writer R Pk} (hw : g c' = some w) :
|
||
v = some w ∨ f c' = some w := by
|
||
rcases Classical.em (c' = c) with rfl | hne
|
||
· exact Or.inl (h.1.symm.trans hw)
|
||
· exact Or.inr ((h.2 c' hne).symm.trans hw)
|
||
|
||
variable (M : Model R Obj Pk E)
|
||
|
||
/-- `o` is reachable from the ref state of the manifest `p` names. -/
|
||
def Model.baseReach (p : Option (Manifest R Pk)) (o : Obj) : Prop :=
|
||
∃ b, p = some b ∧ M.reach b.refs o
|
||
|
||
/-- The manifests a writer may stage after reading pointer value `p`. -/
|
||
def Model.Staged (p : Option (Manifest R Pk)) (m : Manifest R Pk) : Prop :=
|
||
m.parent = p ∧ M.Legal (p.map Manifest.refs) m.refs ∧
|
||
(-- no new pack
|
||
((∀ o, M.reach m.refs o → M.baseReach p o) ∧ ∀ pk, m.packs pk ↔ basePacks p pk) ∨
|
||
-- delta pack
|
||
(∃ d, (∀ o, M.reach m.refs o → M.baseReach p o ∨ M.objs d o) ∧
|
||
∀ pk, m.packs pk ↔ (basePacks p pk ∨ pk = d)) ∨
|
||
-- compaction
|
||
(∃ f, (∀ o, M.reach m.refs o → M.objs f o) ∧ ∀ pk, m.packs pk ↔ pk = f))
|
||
|
||
/-- The packs a manifest lists contain every object reachable from its refs. -/
|
||
def Model.Closed (m : Manifest R Pk) : Prop :=
|
||
∀ o, M.reach m.refs o → ∃ pk, m.packs pk ∧ M.objs pk o
|
||
|
||
/-- The steps of the protocol. Each constructor lists its enabling conditions;
|
||
the post-state is the pre-state with the named fields replaced. -/
|
||
inductive Model.Step : State R Pk Client → State R Pk Client → Prop
|
||
/-- Client `c` reads the pointer and stages a manifest `m`. -/
|
||
| begin (s : State R Pk Client) (c : Client) (m : Manifest R Pk) (ws) :
|
||
s.writers c = none → M.Staged s.pointer m →
|
||
Upd s.writers c (some ⟨s.pointer, m, false, s.writes⟩) ws →
|
||
Model.Step s { s with writers := ws }
|
||
/-- Client `c` stores its staged manifest and the packs it lists. -/
|
||
| upload (s : State R Pk Client) (c : Client) (w : Writer R Pk) (ws) :
|
||
s.writers c = some w →
|
||
Upd s.writers c (some { w with uploaded := true }) ws →
|
||
Model.Step s { s with
|
||
mstore := fun x => s.mstore x ∨ x = w.staged
|
||
pstore := fun pk => s.pstore pk ∨ w.staged.packs pk
|
||
writers := ws }
|
||
/-- The conditional write. The comparison is on `Option E`, so an absent
|
||
pointer matches only an absent base (`If-None-Match: *`). -/
|
||
| cas (s : State R Pk Client) (c : Client) (w : Writer R Pk) (ws) :
|
||
s.writers c = some w → w.uploaded = true →
|
||
s.pointer.map M.etag = w.base.map M.etag →
|
||
Upd s.writers c none ws →
|
||
Model.Step s { s with pointer := some w.staged, writes := s.writes + 1, writers := ws }
|
||
/-- Client `c` stops: a lost race, a crash, or a timeout. -/
|
||
| abort (s : State R Pk Client) (c : Client) (w : Writer R Pk) (ws) :
|
||
s.writers c = some w → Upd s.writers c none ws →
|
||
Model.Step s { s with writers := ws }
|
||
|
||
/-- The states reachable from the initial state by finitely many steps. -/
|
||
inductive Model.Reachable : State R Pk Client → Prop
|
||
| init : Model.Reachable State.init
|
||
| step {s s' : State R Pk Client} : Model.Reachable s → M.Step s s' → Model.Reachable s'
|
||
|
||
/-! ## Auxiliary lemmas and the inductive invariant -/
|
||
|
||
/-- A manifest staged from a closed base is closed. This is where the three
|
||
pack rules are used. -/
|
||
theorem Model.Staged.closed {p : Option (Manifest R Pk)} {m : Manifest R Pk}
|
||
(h : M.Staged p m) (hp : ∀ b, p = some b → M.Closed b) : M.Closed m := by
|
||
intro o ho
|
||
have base : M.baseReach p o → ∃ pk, basePacks p pk ∧ M.objs pk o := by
|
||
rintro ⟨b, rfl, hb⟩
|
||
obtain ⟨pk, hpk, hobj⟩ := hp b rfl o hb
|
||
exact ⟨pk, ⟨b, rfl, hpk⟩, hobj⟩
|
||
rcases h.2.2 with ⟨hr, hpk⟩ | ⟨d, hr, hpk⟩ | ⟨f, hr, hpk⟩
|
||
· obtain ⟨pk, h1, h2⟩ := base (hr o ho)
|
||
exact ⟨pk, (hpk pk).2 h1, h2⟩
|
||
· rcases hr o ho with hb | hd
|
||
· obtain ⟨pk, h1, h2⟩ := base hb
|
||
exact ⟨pk, (hpk pk).2 (Or.inl h1), h2⟩
|
||
· exact ⟨d, (hpk d).2 (Or.inr rfl), hd⟩
|
||
· exact ⟨f, (hpk f).2 rfl, hr o ho⟩
|
||
|
||
/-- Equal ETags (as `Option E`) imply equal pointer values, by `etag_inj`. -/
|
||
theorem Model.eq_of_etag_eq {p q : Option (Manifest R Pk)}
|
||
(h : p.map M.etag = q.map M.etag) : p = q := by
|
||
cases p <;> cases q <;> simp at h
|
||
· rfl
|
||
· exact congrArg some (M.etag_inj _ _ h)
|
||
|
||
/-- The invariant of one writer: its staged manifest was computed from its
|
||
base, its base is closed, the depth of its base is the write count it read,
|
||
and once it has uploaded, its staged manifest and packs are stored. -/
|
||
structure Model.WriterInv (s : State R Pk Client) (w : Writer R Pk) : Prop where
|
||
staged : M.Staged w.base w.staged
|
||
baseClosed : ∀ b, w.base = some b → M.Closed b
|
||
readAt : depthOpt w.base = w.readAt
|
||
stored : w.uploaded = true → s.mstore w.staged ∧ ∀ pk, w.staged.packs pk → s.pstore pk
|
||
|
||
/-- The inductive invariant of the protocol. -/
|
||
structure Model.Inv (s : State R Pk Client) : Prop where
|
||
fence : ∀ m, s.pointer = some m → s.mstore m ∧ ∀ pk, m.packs pk → s.pstore pk
|
||
closed : ∀ m, s.pointer = some m → M.Closed m
|
||
depth : depthOpt s.pointer = s.writes
|
||
writers : ∀ c w, s.writers c = some w → M.WriterInv s w
|
||
|
||
/-- The writer invariant survives any step that only adds to the stores. -/
|
||
theorem Model.WriterInv.mono {s s' : State R Pk Client} {w : Writer R Pk}
|
||
(h : M.WriterInv s w) (hm : ∀ x, s.mstore x → s'.mstore x)
|
||
(hp : ∀ pk, s.pstore pk → s'.pstore pk) : M.WriterInv s' w :=
|
||
⟨h.staged, h.baseClosed, h.readAt, fun hu =>
|
||
⟨hm _ (h.stored hu).1, fun pk hpk => hp pk ((h.stored hu).2 pk hpk)⟩⟩
|
||
|
||
theorem Model.Inv.init : M.Inv (State.init : State R Pk Client) :=
|
||
⟨fun _ h => (nomatch h), fun _ h => (nomatch h), rfl, fun _ _ h => (nomatch h)⟩
|
||
|
||
theorem Model.Inv.step {s s' : State R Pk Client} (inv : M.Inv s) (st : M.Step s s') :
|
||
M.Inv s' := by
|
||
cases st with
|
||
| begin c m ws hc hm hu =>
|
||
refine ⟨inv.fence, inv.closed, inv.depth, fun c' w' hw' => ?_⟩
|
||
rcases hu.cases hw' with hnew | hold
|
||
· cases hnew
|
||
exact ⟨hm, inv.closed, inv.depth, fun h => nomatch h⟩
|
||
· exact (inv.writers c' w' hold).mono M (fun _ h => h) (fun _ h => h)
|
||
| upload c w ws hc hu =>
|
||
refine ⟨fun m hm => ?_, inv.closed, inv.depth, fun c' w' hw' => ?_⟩
|
||
· exact ⟨Or.inl (inv.fence m hm).1, fun pk h => Or.inl ((inv.fence m hm).2 pk h)⟩
|
||
· rcases hu.cases hw' with hnew | hold
|
||
· cases hnew
|
||
have hw := inv.writers c w hc
|
||
exact ⟨hw.staged, hw.baseClosed, hw.readAt, fun _ => ⟨Or.inr rfl, fun _ h => Or.inr h⟩⟩
|
||
· exact (inv.writers c' w' hold).mono M (fun _ h => Or.inl h) (fun _ h => Or.inl h)
|
||
| cas c w ws hc hup he hu =>
|
||
have hw := inv.writers c w hc
|
||
have hbase : s.pointer = w.base := M.eq_of_etag_eq he
|
||
refine ⟨fun m hm => ?_, fun m hm => ?_, ?_, fun c' w' hw' => ?_⟩
|
||
· cases hm
|
||
exact hw.stored hup
|
||
· cases hm
|
||
exact hw.staged.closed M hw.baseClosed
|
||
· show w.staged.depth = s.writes + 1
|
||
rw [w.staged.depth_eq, hw.staged.1, ← hbase, inv.depth]
|
||
· rcases hu.cases hw' with hnew | hold
|
||
· cases hnew
|
||
· exact (inv.writers c' w' hold).mono M (fun _ h => h) (fun _ h => h)
|
||
| abort c w ws hc hu =>
|
||
refine ⟨inv.fence, inv.closed, inv.depth, fun c' w' hw' => ?_⟩
|
||
rcases hu.cases hw' with hnew | hold
|
||
· cases hnew
|
||
· exact (inv.writers c' w' hold).mono M (fun _ h => h) (fun _ h => h)
|
||
|
||
/-- Every reachable state satisfies the invariant. -/
|
||
theorem Model.Reachable.inv {s : State R Pk Client} (hs : M.Reachable s) : M.Inv s := by
|
||
induction hs with
|
||
| init => exact Model.Inv.init M
|
||
| step _ st ih => exact ih.step M st
|
||
|
||
/-! ## Main results -/
|
||
|
||
/-- The pointer names only what is stored: the manifest it names is in the
|
||
manifest store, and every pack that manifest lists is in the pack store. -/
|
||
theorem fence {s : State R Pk Client} (hs : M.Reachable s) {m : Manifest R Pk}
|
||
(hm : s.pointer = some m) : s.mstore m ∧ ∀ pk, m.packs pk → s.pstore pk :=
|
||
hs.inv.fence m hm
|
||
|
||
/-- The packs listed by the pointed-to manifest contain every object reachable
|
||
from its ref state. -/
|
||
theorem closed {s : State R Pk Client} (hs : M.Reachable s) {m : Manifest R Pk}
|
||
(hm : s.pointer = some m) : ∀ o, M.reach m.refs o → ∃ pk, m.packs pk ∧ M.objs pk o :=
|
||
hs.inv.closed m hm
|
||
|
||
/-- Every step from a reachable state leaves the pointer unchanged or replaces
|
||
it by a manifest whose parent is the replaced value and whose ref state is a
|
||
legal successor of the replaced ref state. Each change of the published ref
|
||
state is thus one step of an atomic ref database, computed against the state
|
||
it replaces. -/
|
||
theorem pointer_step_legal {s s' : State R Pk Client} (hs : M.Reachable s) (st : M.Step s s') :
|
||
s'.pointer = s.pointer ∨
|
||
∃ m, s'.pointer = some m ∧ m.parent = s.pointer ∧
|
||
M.Legal (s.pointer.map Manifest.refs) m.refs := by
|
||
cases st with
|
||
| begin => exact Or.inl rfl
|
||
| upload => exact Or.inl rfl
|
||
| abort => exact Or.inl rfl
|
||
| cas c w ws hc hup he hu =>
|
||
have hw := hs.inv.writers c w hc
|
||
have hbase : s.pointer = w.base := M.eq_of_etag_eq he
|
||
exact Or.inr ⟨w.staged, rfl, hbase ▸ hw.staged.1, hbase ▸ hw.staged.2.1⟩
|
||
|
||
/-- The length of the predecessor chain of the pointer equals the number of
|
||
pointer writes. Each write therefore publishes a manifest of a depth that no
|
||
earlier published manifest had. -/
|
||
theorem pointer_depth_eq_writes {s : State R Pk Client} (hs : M.Reachable s) :
|
||
depthOpt s.pointer = s.writes :=
|
||
hs.inv.depth
|
||
|
||
/-- If the conditional write of writer `w` is enabled in a reachable state (the
|
||
three hypotheses are the enabling conditions of `Model.Step.cas`), then no
|
||
pointer write has happened since `w` read the pointer. -/
|
||
theorem cas_sees_no_intervening_write {s : State R Pk Client} (hs : M.Reachable s)
|
||
{c : Client} {w : Writer R Pk} (hc : s.writers c = some w) (_hup : w.uploaded = true)
|
||
(he : s.pointer.map M.etag = w.base.map M.etag) : w.readAt = s.writes := by
|
||
have hw := hs.inv.writers c w hc
|
||
rw [← hw.readAt, ← M.eq_of_etag_eq he, hs.inv.depth]
|
||
|
||
/-! ## Non-vacuity -/
|
||
|
||
/-- The enabling conditions can be met: there is an instance of the model in
|
||
which a writer reads the absent pointer, uploads, and wins the conditional
|
||
write. The results above therefore do not hold merely because no pointer write
|
||
is ever possible. -/
|
||
theorem write_is_possible :
|
||
∃ (M : Model Unit Unit Unit (Manifest Unit Unit)) (s : State Unit Unit Unit),
|
||
M.Reachable s ∧ s.writes = 1 ∧ s.pointer ≠ none := by
|
||
let M : Model Unit Unit Unit (Manifest Unit Unit) :=
|
||
⟨fun _ _ => True, fun _ _ => True, fun _ _ => True, id, fun _ _ h => h⟩
|
||
let m : Manifest Unit Unit := ⟨(), fun _ => True, none⟩
|
||
have upd : ∀ (f : Unit → Option (Writer Unit Unit)) v, Upd f () v (fun _ => v) :=
|
||
fun _ _ => ⟨rfl, fun _ h => absurd rfl h⟩
|
||
have staged : M.Staged none m :=
|
||
⟨rfl, trivial, Or.inr (Or.inr ⟨(), fun _ _ => trivial, fun _ => ⟨fun _ => rfl, fun _ => trivial⟩⟩)⟩
|
||
have s1 := Model.Reachable.step Model.Reachable.init
|
||
(Model.Step.begin (M := M) State.init () m _ rfl staged (upd _ _))
|
||
have s2 := Model.Reachable.step s1 (Model.Step.upload _ () _ _ rfl (upd _ _))
|
||
have s3 := Model.Reachable.step s2 (Model.Step.cas _ () _ _ rfl rfl rfl (upd _ _))
|
||
exact ⟨M, _, s3, rfl, fun h => nomatch h⟩
|
||
|
||
end GitPointer
|
||
|
||
#print axioms GitPointer.fence
|
||
#print axioms GitPointer.closed
|
||
#print axioms GitPointer.pointer_step_legal
|
||
#print axioms GitPointer.cas_sees_no_intervening_write
|
||
#print axioms GitPointer.pointer_depth_eq_writes
|
||
#print axioms GitPointer.write_is_possible
|