From 57d092c10255837543bc712e84c02936e63b3c94 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 09:10:05 +0200
Subject: [PATCH 01/15] doc: design doc for compute protocol Lean 4 semantics,
 Phase 1

Phase 1 of a layered plan to mechanize the compute protocol's control-plane
contract in Lean 4, following the #36614 error-semantics precedent. Covers
staging/handshake ordering and command/response legality only; read-hold
lifecycle and multi-replica fan-out are later phases.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
---
 .../20260724_compute_protocol_semantics.md    | 218 ++++++++++++++++++
 1 file changed, 218 insertions(+)
 create mode 100644 doc/developer/design/20260724_compute_protocol_semantics.md

diff --git a/doc/developer/design/20260724_compute_protocol_semantics.md b/doc/developer/design/20260724_compute_protocol_semantics.md
new file mode 100644
index 0000000000000..2730e10307ff0
--- /dev/null
+++ b/doc/developer/design/20260724_compute_protocol_semantics.md
@@ -0,0 +1,218 @@
+# Compute protocol semantics (Lean 4 model), Phase 1: staging and command/response legality
+
+- Associated: MaterializeInc/materialize#36614 (Lean 4 mechanization precedent, error-handling semantics)
+
+## The problem
+
+The compute protocol (`src/compute-client/src/protocol/{command,response,history}.rs`)
+encodes several non-obvious invariants only in prose: a three-stage handshake,
+per-command legality preconditions tied to `GlobalId`s, frontier monotonicity
+and terminality for responses, and a 1:1 contract between `Peek` and
+`PeekResponse`. These invariants are load-bearing (violating them causes
+replica undefined behavior per the doc comments) but are currently checked
+only by code review and by whatever the implementation happens to enforce.
+There is no artifact that states the invariants independently of the
+implementation, so it is hard to know whether the invariants are mutually
+consistent, whether a proposed protocol change preserves them, or whether the
+prose is complete.
+
+There is no open GitHub issue tracking this work. It originated from a
+conversation about whether the protocol's invariants could be captured in a
+semantic model and checked with a proof assistant, following the precedent
+set by #36614's Lean 4 mechanization of the error-handling design.
+
+This doc proposes a Lean 4 model of the protocol's control-plane contract: a
+state machine plus a small set of safety theorems that codifies the doc
+comments as checked mathematics. The goal is to verify the model's internal
+consistency (the invariants do not contradict each other, a well-formed
+execution cannot get stuck), not to verify the Rust implementation against
+the model.
+
+This is Phase 1 of a three-phase layered plan. Phase 2 (read-hold lifecycle
+against `AllowCompaction`) and Phase 3 (command sharing and response
+reconciliation across replicas and workers) extend Phase 1's state machine
+rather than starting fresh; they are not covered by this doc.
+
+## Success criteria
+
+- A Lean 4 project (a new `lean_lib` in the existing `doc/developer/semantics/`
+  package) defines `ProtocolState`, `Event` (mirroring `ComputeCommand` /
+  `ComputeResponse`), and a `step : ProtocolState → Event → Option
+  ProtocolState` relation whose preconditions match the "invalid to" / "must"
+  statements in `command.rs`, `response.rs`, and `protocol.rs`.
+- At least the five theorems listed under Solution Proposal are stated and
+  proved with no `sorry`, each traceable to an explicit doc-comment contract.
+- The model builds in CI via the existing `ci/test/lean-semantics.sh` harness.
+- A reader can go from a doc-comment sentence in `command.rs` / `response.rs`
+  to the Lean lemma that encodes it, and back.
+
+## Out of scope
+
+- Payload semantics: the contents of `Row`, `DataflowDescription`,
+  `RelationDesc`, and similar types are opaque and uninterpreted in the
+  model. Phase 1 is about control flow and identifiers, not data.
+- Read-hold / `since` correctness against `AllowCompaction`. That is a
+  controller-side accounting property (Phase 2), not a protocol-legality
+  property. Phase 1 only models what the wire contract says about
+  `AllowCompaction`, which is silent on monotonicity of the frontier the
+  controller chooses to send.
+- Multi-replica and multi-worker command sharing and response demuxing
+  (Phase 3).
+- Liveness ("must eventually respond", "must eventually report empty
+  frontiers"). Phase 1 proves safety only: what must hold if an event
+  occurs, not that a required event eventually occurs.
+- Wire transport (bincode / CTP encoding, delivery scheduling). In-order,
+  reliable delivery is a hypothesis of the model, not something proved.
+- Verifying the Rust implementation against the model. Out of scope for the
+  whole layered project, not only Phase 1.
+
+## Solution proposal
+
+Model the protocol as a single event stream folded through one
+state-transition relation, with safety properties stated as invariants
+preserved by that fold. This is the same technique #36614 uses for
+`Collection.refines` / `NoRowErr`: define state and step, prove step
+preserves the invariant, induct over the execution.
+
+### State and events
+
+`ProtocolState` tracks exactly what the doc comments make legality depend
+on:
+
+- `created : Set GlobalId`, ids exported by a `CreateDataflow` seen so far.
+- `scheduled`, `allowedWrites : Set GlobalId`.
+- `since : GlobalId → Option (Antichain Timestamp)`, most recent
+  `AllowCompaction` frontier per id.
+- `reportedFrontiers : GlobalId → FrontierKind → Option (Antichain
+  Timestamp)`, last `Frontiers` response per id per kind (write / input /
+  output), used to check monotonicity and terminality of future responses.
+- `peeks : Uuid → PeekState` where `PeekState := Pending | Answered`.
+- `stage : Stage` where `Stage := Creation | Initialization | Computation`,
+  plus `helloSeen` / `createInstanceSeen` flags to pin the first two events.
+
+`Event := Cmd ComputeCommand | Resp ComputeResponse`, an inductive mirror of
+the two real Rust enums. Fields with no bearing on protocol-level legality
+(`RelationDesc`, `Row`, `DataflowDescription`'s internals, `RowSetFinishing`,
+and similar) are represented by an opaque placeholder type rather than
+reconstructed field for field. Fields legality does depend on (`GlobalId`,
+`Uuid`, `Antichain Timestamp`, the `PeekTarget`'s id) are kept concrete.
+
+### Step relation
+
+`step : ProtocolState → Event → Option ProtocolState`. Each command or
+response variant gets one equation. Example shapes, illustrative rather than
+final Lean syntax:
+
+- `step s (Cmd (Schedule id)) = if id ∈ s.created then some {s with scheduled := s.scheduled.insert id} else none`
+- `step s (Resp (Frontiers id fr)) = if id ∈ s.created ∧ frontierAdvances s id fr then some (s.withReportedFrontiers id fr) else none`
+- `step s (Cmd (Peek p)) = if p.uuid ∉ s.peeks.keys then some {s with peeks := s.peeks.insert p.uuid Pending} else none`
+- `step s (Resp (PeekResponse uuid _ _)) = if s.peeks.find? uuid = some Pending then some {s with peeks := s.peeks.insert uuid Answered} else none`
+
+A `none` result models the "may cause undefined behavior" clause: the model
+has nothing further to say about what happens next, matching the doc's
+contract rather than inventing recovery behavior the real protocol does not
+specify.
+
+An execution is `List Event`, well-formed iff folding `step` from an initial
+empty state never produces `none`.
+
+### Target theorems
+
+1. `hello_create_instance_first`: in any well-formed execution, the first
+   event is `Cmd (Hello _)` and the second is `Cmd (CreateInstance _)`.
+2. `create_before_reference`: any event that names `id` other than the
+   `CreateDataflow` that creates it (Schedule, AllowWrites, AllowCompaction,
+   Peek on an index target, Frontiers, SubscribeResponse, CopyToResponse,
+   Status) occurs strictly after `id`'s `CreateDataflow` in the execution.
+3. `frontiers_monotone_and_terminal`: for each id and frontier kind, the
+   sequence of reported frontiers in a well-formed execution is
+   non-decreasing, and once a kind reports the empty frontier for an id, no
+   later event reports a non-empty value for that (id, kind).
+4. `peek_response_unique`: for each `Uuid`, a well-formed execution contains
+   at most one `PeekResponse` for it, and if present, it is preceded by
+   exactly one `Peek` command with the same uuid.
+5. `cancel_requires_peek`: `CancelPeek uuid` is only legal after a `Peek`
+   with matching uuid.
+
+Each theorem's statement should be traceable to the specific doc-comment
+sentence it encodes, linked from the Lean docstring rather than narrated in
+the proof.
+
+### Project structure
+
+Add a `MzCompute` `lean_lib` target to the existing
+`doc/developer/semantics/lakefile.toml`, alongside the current `Mz` target.
+This reuses the Docker image, pinned Mathlib version, and
+`ci/test/lean-semantics.sh` harness, which are expensive to duplicate, and
+later phases may want `Finset` / `BTreeMap`-style reasoning for the
+multi-replica layer. It is kept as a separate library and namespace rather
+than folded into `Mz`, since `Mz`'s existing docstring scopes it to scalar
+evaluation and collection semantics, a different subsystem (data plane, not
+control plane). New `MzCompute/` module directory, own root import file, own
+`compute-protocol.md` reading-order doc parallel to the existing `model.md`
+and `transforms.md`, with `README.md` updated to list both subsystems and
+their relationship.
+
+## Minimal viable prototype
+
+A single Lean module defining `ProtocolState` / `Event` / `step` and proving
+`hello_create_instance_first` and `create_before_reference`, the two
+simplest and most structural theorems, is the MVP. It validates the
+state/step shape before investing in the frontier-monotonicity and
+peek-uniqueness proofs, which touch more of the state and are more likely to
+reveal that the chosen state shape is wrong.
+
+## Alternatives
+
+**Fully integrated single model (stages, read holds, and replica fan-out
+together).** Considered and rejected for Phase 1: it would catch
+cross-cutting invariants at subsystem boundaries, but the combined state
+space is large before anything is proved, and it front-loads the exact
+complexity a layered approach exists to avoid. Worth revisiting once Phases
+1 through 3 exist independently, as a possible Phase 4 "boundary" pass.
+
+**Fully separate models per phase, no shared kernel.** Rejected: each phase
+would carry its own simplified assumptions about the other phases, and the
+subtle bugs this protocol actually has tend to live at exactly those
+boundaries (for example, a race between `AllowCompaction` and an in-flight
+`Peek`). The layered approach instead has Phase 2 and Phase 3 extend Phase
+1's `ProtocolState` / `Event` / `step`, so cross-phase reasoning stays
+possible without Phase 1 paying Phase 3's cost.
+
+**Trace well-formedness predicate instead of a state machine.** An
+alternative shape defines well-formedness directly as a predicate over
+`List Event` (for example, "id's `CreateDataflow` appears before any other
+event naming id") rather than through a `step` relation. Rejected because it
+does not compose across phases the same way: Phase 2's read-hold invariants
+need a running `since` per id to state "since never exceeds a live hold's
+frontier", which needs state that accumulates across the fold, not a
+predicate over the whole list. The `step`-relation shape generalizes to that
+need; the trace-predicate shape would need to be rebuilt for Phase 2 anyway.
+
+**New standalone Lean project instead of a second `lean_lib` in the existing
+package.** Rejected for now: it duplicates the Docker image, Mathlib pin,
+and CI harness for no isolation benefit `MzCompute` does not already get
+from being a separate library target. Worth reconsidering if the two
+subsystems' dependency needs diverge enough to matter, for instance if
+`MzCompute` never needs Mathlib and its presence meaningfully slows
+iteration.
+
+## Open questions
+
+- Does "protocol iteration" in the doc comments (peek uuid uniqueness,
+  `Hello` nonce uniqueness) mean one CTP connection's lifetime, or does the
+  model need to handle reconnection (a second `Hello` after a connection
+  drop) within Phase 1? The current proposal assumes a single connection per
+  execution and defers reconnection modeling to a later phase; confirm this
+  does not undercut the Phase 1 theorems' relevance to the real,
+  reconnecting system.
+- `UpdateConfiguration` and `Hello` are broadcast to all workers rather than
+  routed through the first worker only. Phase 1 treats the protocol as a
+  single logical stream (one controller, one logical receiver) and defers
+  the worker-fan-out distinction entirely to Phase 3. Confirm the Phase 1
+  theorems remain meaningful stated over the logical single-stream view.
+- Should `frontiers_monotone_and_terminal` also state the doc's stronger
+  requirement that the first reported frontier of any kind is not less than
+  the dataflow's initial `as_of`? That requires `CreateDataflow`'s `as_of`
+  to be tracked in state, currently left opaque. Left for the Phase 1
+  implementation to decide once the state shape is in hand.

From 8667810913f1bd7bdf3b84858f3f6022bd9c0726 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 09:47:30 +0200
Subject: [PATCH 02/15] doc: address adversarial review findings on compute
 protocol design

Fix three real gaps found by review: missing drop-after-compaction
precondition on Schedule/AllowWrites, an unstatable Status theorem clause
(no GlobalId on that response variant), and missing CreateDataflow
export-id-uniqueness theorem. Also tighten the trace-predicate rejection
in Alternatives, note the opaque-type erasure caveat explicitly, and
resolve the infra dependency by bootstrapping doc/developer/semantics/
ourselves instead of depending on unmerged #36614.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
---
 .../20260724_compute_protocol_semantics.md    | 109 ++++++++++++------
 1 file changed, 75 insertions(+), 34 deletions(-)

diff --git a/doc/developer/design/20260724_compute_protocol_semantics.md b/doc/developer/design/20260724_compute_protocol_semantics.md
index 2730e10307ff0..32696d77b30f5 100644
--- a/doc/developer/design/20260724_compute_protocol_semantics.md
+++ b/doc/developer/design/20260724_compute_protocol_semantics.md
@@ -1,6 +1,6 @@
 # Compute protocol semantics (Lean 4 model), Phase 1: staging and command/response legality
 
-- Associated: MaterializeInc/materialize#36614 (Lean 4 mechanization precedent, error-handling semantics)
+- Associated: MaterializeInc/materialize#36614 (Lean 4 mechanization precedent, error-handling semantics. Unmerged, referenced as prior art only, not a dependency)
 
 ## The problem
 
@@ -31,18 +31,20 @@ the model.
 This is Phase 1 of a three-phase layered plan. Phase 2 (read-hold lifecycle
 against `AllowCompaction`) and Phase 3 (command sharing and response
 reconciliation across replicas and workers) extend Phase 1's state machine
-rather than starting fresh; they are not covered by this doc.
+rather than starting fresh. They are not covered by this doc.
 
 ## Success criteria
 
-- A Lean 4 project (a new `lean_lib` in the existing `doc/developer/semantics/`
-  package) defines `ProtocolState`, `Event` (mirroring `ComputeCommand` /
-  `ComputeResponse`), and a `step : ProtocolState → Event → Option
-  ProtocolState` relation whose preconditions match the "invalid to" / "must"
-  statements in `command.rs`, `response.rs`, and `protocol.rs`.
-- At least the five theorems listed under Solution Proposal are stated and
+- A Lean 4 project (a new `lean_lib` in a `doc/developer/semantics/` package,
+  see Project Structure) defines `ProtocolState`, `Event` (mirroring
+  `ComputeCommand` / `ComputeResponse`), and a `step : ProtocolState → Event →
+  Option ProtocolState` relation whose preconditions match the "invalid to" /
+  "must" statements in `command.rs`, `response.rs`, and `protocol.rs`.
+- At least the seven theorems listed under Solution Proposal are stated and
   proved with no `sorry`, each traceable to an explicit doc-comment contract.
-- The model builds in CI via the existing `ci/test/lean-semantics.sh` harness.
+- The model builds in CI via a `ci/test/lean-semantics.sh` harness, bootstrapped
+  as part of this phase (see Project Structure). This does not depend on
+  #36614 landing first.
 - A reader can go from a doc-comment sentence in `command.rs` / `response.rs`
   to the Lean lemma that encodes it, and back.
 
@@ -80,6 +82,10 @@ preserves the invariant, induct over the execution.
 on:
 
 - `created : Set GlobalId`, ids exported by a `CreateDataflow` seen so far.
+  `CreateDataflow`'s command payload keeps its export id set (`Finset
+  GlobalId`) concrete even though the rest of `DataflowDescription` is
+  opaque, since export-id freshness is itself a Phase 1 legality theorem
+  (see Target theorems).
 - `scheduled`, `allowedWrites : Set GlobalId`.
 - `since : GlobalId → Option (Antichain Timestamp)`, most recent
   `AllowCompaction` frontier per id.
@@ -97,17 +103,33 @@ and similar) are represented by an opaque placeholder type rather than
 reconstructed field for field. Fields legality does depend on (`GlobalId`,
 `Uuid`, `Antichain Timestamp`, the `PeekTarget`'s id) are kept concrete.
 
+Opaquing a field erases whatever structural facts it carries, not only its
+data content. For example `Peek::literal_constraints`'s documented "the
+vector is never empty" becomes unstatable once that field is opaque. This is
+an accepted Phase 1 cut, not an oversight: only the seven theorems below are
+committed deliverables, and structural payload facts unrelated to them are
+left for a later phase to pick up if they turn out to matter.
+
 ### Step relation
 
 `step : ProtocolState → Event → Option ProtocolState`. Each command or
 response variant gets one equation. Example shapes, illustrative rather than
 final Lean syntax:
 
-- `step s (Cmd (Schedule id)) = if id ∈ s.created then some {s with scheduled := s.scheduled.insert id} else none`
+- `step s (Cmd (CreateDataflow exports _)) = if exports ∩ s.created = ∅ ∧ exports.Nodup then some {s with created := s.created ∪ exports} else none`
+- `step s (Cmd (Schedule id)) = if id ∈ s.created ∧ s.since id ≠ some ∅ then some {s with scheduled := s.scheduled.insert id} else none`
+- `step s (Cmd (AllowWrites id)) = if id ∈ s.created ∧ s.since id ≠ some ∅ then some {s with allowedWrites := s.allowedWrites.insert id} else none`
 - `step s (Resp (Frontiers id fr)) = if id ∈ s.created ∧ frontierAdvances s id fr then some (s.withReportedFrontiers id fr) else none`
 - `step s (Cmd (Peek p)) = if p.uuid ∉ s.peeks.keys then some {s with peeks := s.peeks.insert p.uuid Pending} else none`
 - `step s (Resp (PeekResponse uuid _ _)) = if s.peeks.find? uuid = some Pending then some {s with peeks := s.peeks.insert uuid Answered} else none`
 
+`Schedule` and `AllowWrites` both check `s.since id ≠ some ∅`: `command.rs`
+states it is invalid to send either once the collection has been allowed to
+compact to the empty frontier (the canonical drop). `CreateDataflow` checks
+its export ids are pairwise distinct (`exports.Nodup`) and disjoint from
+everything already created, mirroring `command.rs`'s "dataflow exports have
+unique IDs... do not repeat (within a single protocol iteration)".
+
 A `none` result models the "may cause undefined behavior" clause: the model
 has nothing further to say about what happens next, matching the doc's
 contract rather than inventing recovery behavior the real protocol does not
@@ -122,16 +144,27 @@ empty state never produces `none`.
    event is `Cmd (Hello _)` and the second is `Cmd (CreateInstance _)`.
 2. `create_before_reference`: any event that names `id` other than the
    `CreateDataflow` that creates it (Schedule, AllowWrites, AllowCompaction,
-   Peek on an index target, Frontiers, SubscribeResponse, CopyToResponse,
-   Status) occurs strictly after `id`'s `CreateDataflow` in the execution.
-3. `frontiers_monotone_and_terminal`: for each id and frontier kind, the
+   Peek on an index target, Frontiers, SubscribeResponse, CopyToResponse)
+   occurs strictly after `id`'s `CreateDataflow` in the execution. `Status`
+   is excluded: `ComputeResponse::Status` carries no `GlobalId` in the
+   current protocol (`StatusResponse` is an unimplemented placeholder), so
+   the doc's per-collection `Status` obligation isn't statable against the
+   real enum yet. Revisit if `Status` grows collection-scoped variants.
+3. `no_reference_after_drop`: `Schedule`, `AllowWrites`, and `Peek` (index
+   target) on `id` are only legal while `since id` has not yet reached the
+   empty frontier. Once an `AllowCompaction` with the empty frontier for
+   `id` has taken effect, no later event may `Schedule`, `AllowWrites`, or
+   `Peek` against it.
+4. `create_dataflow_ids_fresh`: a `CreateDataflow`'s export ids are pairwise
+   distinct and disjoint from every id created earlier in the execution.
+5. `frontiers_monotone_and_terminal`: for each id and frontier kind, the
    sequence of reported frontiers in a well-formed execution is
    non-decreasing, and once a kind reports the empty frontier for an id, no
    later event reports a non-empty value for that (id, kind).
-4. `peek_response_unique`: for each `Uuid`, a well-formed execution contains
+6. `peek_response_unique`: for each `Uuid`, a well-formed execution contains
    at most one `PeekResponse` for it, and if present, it is preceded by
    exactly one `Peek` command with the same uuid.
-5. `cancel_requires_peek`: `CancelPeek uuid` is only legal after a `Peek`
+7. `cancel_requires_peek`: `CancelPeek uuid` is only legal after a `Peek`
    with matching uuid.
 
 Each theorem's statement should be traceable to the specific doc-comment
@@ -140,18 +173,23 @@ the proof.
 
 ### Project structure
 
-Add a `MzCompute` `lean_lib` target to the existing
-`doc/developer/semantics/lakefile.toml`, alongside the current `Mz` target.
-This reuses the Docker image, pinned Mathlib version, and
-`ci/test/lean-semantics.sh` harness, which are expensive to duplicate, and
-later phases may want `Finset` / `BTreeMap`-style reasoning for the
-multi-replica layer. It is kept as a separate library and namespace rather
-than folded into `Mz`, since `Mz`'s existing docstring scopes it to scalar
-evaluation and collection semantics, a different subsystem (data plane, not
-control plane). New `MzCompute/` module directory, own root import file, own
-`compute-protocol.md` reading-order doc parallel to the existing `model.md`
-and `transforms.md`, with `README.md` updated to list both subsystems and
-their relationship.
+`doc/developer/semantics/` (Docker image, pinned Mathlib version,
+`lakefile.toml`, `ci/test/lean-semantics.sh` harness) does not exist on this
+branch: it was built on #36614's still-unmerged fork branch. Phase 1
+bootstraps this scaffolding itself, following #36614's shape as prior art
+(same Lean/Mathlib pin approach, same Docker-image-plus-CI-script structure)
+without depending on that PR landing. Concretely: a `doc/developer/semantics/`
+package with a `lakefile.toml` declaring an `MzCompute` `lean_lib` target, a
+`Dockerfile` and `ci/test/lean-semantics.sh` harness for CI, and a
+`MzCompute/` module directory with its own root import file. If #36614 lands
+first, the two efforts reconcile by merging into a single `lakefile.toml`
+with two `lean_lib` targets (`Mz` and `MzCompute`) sharing one Docker image.
+Until then `MzCompute` stands alone. It is designed as a separate library and
+namespace from the start rather than planned as a merge into `Mz`, since
+`Mz`'s docstring (on the #36614 branch) scopes it to scalar evaluation and
+collection semantics, a different subsystem (data plane, not control plane).
+Own `compute-protocol.md` reading-order doc, matching the naming #36614 uses
+for `model.md` / `transforms.md`, to keep the two efforts easy to merge later.
 
 ## Minimal viable prototype
 
@@ -182,12 +220,15 @@ possible without Phase 1 paying Phase 3's cost.
 **Trace well-formedness predicate instead of a state machine.** An
 alternative shape defines well-formedness directly as a predicate over
 `List Event` (for example, "id's `CreateDataflow` appears before any other
-event naming id") rather than through a `step` relation. Rejected because it
-does not compose across phases the same way: Phase 2's read-hold invariants
-need a running `since` per id to state "since never exceeds a live hold's
-frontier", which needs state that accumulates across the fold, not a
-predicate over the whole list. The `step`-relation shape generalizes to that
-need; the trace-predicate shape would need to be rebuilt for Phase 2 anyway.
+event naming id") rather than through a `step` relation. The two shapes are
+formally interchangeable: any such predicate can be written as a fold that
+threads state through the list, which is exactly what `step` does under a
+different name. The reason to prefer `step` isn't expressiveness, it's
+reuse: `step` names and exposes the intermediate state (`ProtocolState`) as
+a first-class definition that Phase 2 can literally extend with a few more
+fields and Phase 3 can literally lift to a product over replicas, whereas a
+predicate's internal fold state is private to its own proof and would need
+to be re-extracted and renamed for each later phase to build on.
 
 **New standalone Lean project instead of a second `lean_lib` in the existing
 package.** Rejected for now: it duplicates the Docker image, Mathlib pin,
@@ -203,7 +244,7 @@ iteration.
   `Hello` nonce uniqueness) mean one CTP connection's lifetime, or does the
   model need to handle reconnection (a second `Hello` after a connection
   drop) within Phase 1? The current proposal assumes a single connection per
-  execution and defers reconnection modeling to a later phase; confirm this
+  execution and defers reconnection modeling to a later phase. Confirm this
   does not undercut the Phase 1 theorems' relevance to the real,
   reconnecting system.
 - `UpdateConfiguration` and `Hello` are broadcast to all workers rather than

From 2025744ba8ee2452046e4e9ff2c6aaaa56fa6515 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 10:14:54 +0200
Subject: [PATCH 03/15] lean: bootstrap MzCompute Lean 4 project and CI harness

Docker image, lakefile, and CI script for the compute protocol
semantics model (Phase 1 of doc/developer/design/20260724_compute_
protocol_semantics.md). No Mathlib dependency: the protocol model is
finite-state and needs only core Lean.
---
 ci/test/lean-semantics.sh              | 43 ++++++++++++++++++
 ci/test/pipeline.template.yml          | 13 ++++++
 doc/developer/semantics/.dockerignore  |  1 +
 doc/developer/semantics/.gitignore     |  2 +
 doc/developer/semantics/Dockerfile     | 60 ++++++++++++++++++++++++++
 doc/developer/semantics/MzCompute.lean | 11 +++++
 doc/developer/semantics/bin/in-image   | 40 +++++++++++++++++
 doc/developer/semantics/lakefile.toml  |  5 +++
 doc/developer/semantics/lean-toolchain |  1 +
 9 files changed, 176 insertions(+)
 create mode 100755 ci/test/lean-semantics.sh
 create mode 100644 doc/developer/semantics/.dockerignore
 create mode 100644 doc/developer/semantics/.gitignore
 create mode 100644 doc/developer/semantics/Dockerfile
 create mode 100644 doc/developer/semantics/MzCompute.lean
 create mode 100755 doc/developer/semantics/bin/in-image
 create mode 100644 doc/developer/semantics/lakefile.toml
 create mode 100644 doc/developer/semantics/lean-toolchain

diff --git a/ci/test/lean-semantics.sh b/ci/test/lean-semantics.sh
new file mode 100755
index 0000000000000..5f1243709b86d
--- /dev/null
+++ b/ci/test/lean-semantics.sh
@@ -0,0 +1,43 @@
+#!/usr/bin/env bash
+
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# lean-semantics.sh: build the Lean 4 compute protocol semantics
+# model in `doc/developer/semantics`. The Lean toolchain version is
+# read from `lean-toolchain` and forwarded to the Dockerfile in the
+# same directory, so the elan toolchain pin used by local developers
+# and the CI image stay in lockstep.
+#
+# The Docker image is built locally on the agent and reused across CI
+# runs by Docker's layer cache. There is no registry push. The image
+# is cheap to rebuild from cold (no Mathlib dependency, see the
+# Dockerfile's comment).
+
+set -euo pipefail
+
+cd "$(dirname "$0")/../.."
+
+semantics_dir="doc/developer/semantics"
+lean_toolchain="$(tr -d '[:space:]' < "$semantics_dir/lean-toolchain")"
+image_tag="mz-lean-semantics:latest"
+
+docker build \
+    --build-arg "LEAN_TOOLCHAIN=$lean_toolchain" \
+    --tag "$image_tag" \
+    -f "$semantics_dir/Dockerfile" \
+    "$semantics_dir"
+
+docker run --rm \
+    --user "$(id -u):$(id -g)" \
+    -v "$PWD/$semantics_dir/MzCompute:/workspace/MzCompute" \
+    -v "$PWD/$semantics_dir/MzCompute.lean:/workspace/MzCompute.lean" \
+    -w /workspace \
+    "$image_tag" \
+    lake build
diff --git a/ci/test/pipeline.template.yml b/ci/test/pipeline.template.yml
index 9a013e7a8982d..877f936a891b9 100644
--- a/ci/test/pipeline.template.yml
+++ b/ci/test/pipeline.template.yml
@@ -201,6 +201,19 @@ steps:
         coverage: skip
         sanitizer: skip
 
+      - id: lean-semantics
+        label: ":lean: Lean semantics"
+        command: ci/test/lean-semantics.sh
+        inputs:
+          - doc/developer/semantics
+          - ci/test/lean-semantics.sh
+        depends_on: []
+        timeout_in_minutes: 15
+        agents:
+          queue: hetzner-x86-64-4cpu-8gb
+        coverage: skip
+        sanitizer: skip
+
       - id: lint-macos
         label: ":rust: macOS Clippy"
         # Running on a manually installed macOS agent, so make sure we don't go out of disk
diff --git a/doc/developer/semantics/.dockerignore b/doc/developer/semantics/.dockerignore
new file mode 100644
index 0000000000000..01f8cdb637da2
--- /dev/null
+++ b/doc/developer/semantics/.dockerignore
@@ -0,0 +1 @@
+.lake/
diff --git a/doc/developer/semantics/.gitignore b/doc/developer/semantics/.gitignore
new file mode 100644
index 0000000000000..b914de79dca12
--- /dev/null
+++ b/doc/developer/semantics/.gitignore
@@ -0,0 +1,2 @@
+# Lake build cache.
+.lake/
diff --git a/doc/developer/semantics/Dockerfile b/doc/developer/semantics/Dockerfile
new file mode 100644
index 0000000000000..12d169f9f3a34
--- /dev/null
+++ b/doc/developer/semantics/Dockerfile
@@ -0,0 +1,60 @@
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# Lean 4 toolchain image for building the compute protocol semantics
+# model in this directory. The Lean version is supplied via build
+# arg, which `ci/test/lean-semantics.sh` reads from `lean-toolchain`,
+# so the elan toolchain pin used by local developers and the CI image
+# stay in lockstep.
+#
+# Unlike a Mathlib-backed Lean project, this one has no `[[require]]`
+# in `lakefile.toml`: the compute protocol model is finite-state and
+# needs nothing beyond core Lean (structural recursion, `List`,
+# `Option`, `Bool`). This keeps the image small and the build fast.
+# If a later phase needs Mathlib, add a `[[require]]` entry and a
+# `lake exe cache get` step here, following the pattern in the (at
+# time of writing, unmerged) MaterializeInc/materialize#36614.
+#
+# Runtime contract: the source under `MzCompute/` and `MzCompute.lean`
+# is bind-mounted over the image's empty placeholders. Lake writes
+# build artifacts to the image's overlay filesystem. They are
+# ephemeral and discarded when the container exits.
+
+FROM ubuntu:26.04
+
+ARG LEAN_TOOLCHAIN
+
+ENV ELAN_HOME=/opt/elan
+ENV PATH=$ELAN_HOME/bin:$PATH
+ENV HOME=/tmp
+
+RUN apt-get update \
+    && DEBIAN_FRONTEND=noninteractive apt-get install -y --no-install-recommends \
+        ca-certificates \
+        curl \
+        git \
+    && rm -rf /var/lib/apt/lists/*
+
+RUN curl --proto '=https' --tlsv1.2 -sSf \
+        https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+        | sh -s -- --default-toolchain "$LEAN_TOOLCHAIN" -y --no-modify-path \
+    && chmod -R a+rX "$ELAN_HOME" \
+    && lean --version
+
+RUN git config --system --add safe.directory '*'
+
+WORKDIR /workspace
+
+COPY lakefile.toml lean-toolchain ./
+
+RUN mkdir -p MzCompute \
+    && touch MzCompute.lean \
+    && lake update \
+    && lake build \
+    && chmod -R a+rwX /workspace
diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
new file mode 100644
index 0000000000000..1d3a555e10ca5
--- /dev/null
+++ b/doc/developer/semantics/MzCompute.lean
@@ -0,0 +1,11 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Root import file for the `MzCompute` library. Each module below is
+-- added by the plan task that introduces it.
diff --git a/doc/developer/semantics/bin/in-image b/doc/developer/semantics/bin/in-image
new file mode 100755
index 0000000000000..6781af7e64d78
--- /dev/null
+++ b/doc/developer/semantics/bin/in-image
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+
+# Copyright Materialize, Inc. and contributors. All rights reserved.
+#
+# Use of this software is governed by the Business Source License
+# included in the LICENSE file at the root of this repository.
+#
+# As of the Change Date specified in that file, in accordance with
+# the Business Source License, use of this software will be governed
+# by the Apache License, Version 2.0.
+#
+# in-image: run a command inside the `mz-lean-semantics` Docker
+# image with the project's `MzCompute/` and `MzCompute.lean`
+# bind-mounted.
+#
+# Examples:
+#   bin/in-image lake build
+#   bin/in-image lake env lean MzCompute/State.lean
+#
+# The script assumes the image is already built. Run
+# `ci/test/lean-semantics.sh` once to build it.
+
+set -euo pipefail
+
+script_dir="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+semantics_dir="$(cd "$script_dir/.." && pwd)"
+image_tag="mz-lean-semantics:latest"
+
+if ! docker image inspect "$image_tag" >/dev/null 2>&1; then
+    echo "error: image $image_tag not found. Run ci/test/lean-semantics.sh first." >&2
+    exit 1
+fi
+
+exec docker run --rm -i \
+    --user "$(id -u):$(id -g)" \
+    -v "$semantics_dir/MzCompute:/workspace/MzCompute" \
+    -v "$semantics_dir/MzCompute.lean:/workspace/MzCompute.lean" \
+    -w /workspace \
+    "$image_tag" \
+    "$@"
diff --git a/doc/developer/semantics/lakefile.toml b/doc/developer/semantics/lakefile.toml
new file mode 100644
index 0000000000000..18b29be5dfe8f
--- /dev/null
+++ b/doc/developer/semantics/lakefile.toml
@@ -0,0 +1,5 @@
+name = "mz-semantics"
+defaultTargets = ["MzCompute"]
+
+[[lean_lib]]
+name = "MzCompute"
diff --git a/doc/developer/semantics/lean-toolchain b/doc/developer/semantics/lean-toolchain
new file mode 100644
index 0000000000000..33e0c088939ad
--- /dev/null
+++ b/doc/developer/semantics/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.1

From 060d1ac95d440b8a89b7d5e9aed9628997e97363 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 10:21:42 +0200
Subject: [PATCH 04/15] lean: add core types (GlobalId, Uuid, Frontier, Stage,
 PeekState)

---
 doc/developer/semantics/MzCompute.lean       |   2 +
 doc/developer/semantics/MzCompute/Basic.lean | 119 +++++++++++++++++++
 2 files changed, 121 insertions(+)
 create mode 100644 doc/developer/semantics/MzCompute/Basic.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index 1d3a555e10ca5..e50c2e7bb1883 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -9,3 +9,5 @@
 --
 -- Root import file for the `MzCompute` library. Each module below is
 -- added by the plan task that introduces it.
+
+import MzCompute.Basic
diff --git a/doc/developer/semantics/MzCompute/Basic.lean b/doc/developer/semantics/MzCompute/Basic.lean
new file mode 100644
index 0000000000000..d2add4ae3ff11
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Basic.lean
@@ -0,0 +1,119 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Core types shared by the compute protocol model: identifiers,
+-- frontiers, and the small enums `step` (see `State.lean`) dispatches
+-- on.
+
+namespace MzCompute
+
+/-- Compute-collection identifier. Only equality matters for
+protocol-level legality, so a bare `Nat` stands in for the real
+`mz_repr::GlobalId`. -/
+abbrev GlobalId := Nat
+
+/-- Peek request identifier, standing in for `uuid::Uuid`. Also reused
+for `Hello`'s nonce, which the model does not otherwise constrain
+(see the design doc's open question on reconnection). -/
+abbrev Uuid := Nat
+
+/-- A single-dimensional frontier over `mz_repr::Timestamp`. Because
+`Timestamp` is totally ordered, an antichain over it has at most one
+element: `.empty` models the empty antichain (the terminal frontier,
+nothing more will ever be written), `.at t` models the singleton
+antichain `{t}`. -/
+inductive Frontier where
+  | at (t : Nat)
+  | empty
+  deriving Repr
+
+/-- `Frontier.advances new old` holds (as `true`) exactly when `new`
+is at least as advanced as `old` (`new ⊒ old` in `response.rs`'s
+terms). `.empty` is the top element: nothing exceeds it, and only
+`.empty` can follow it. `.at 0` doubles as the "nothing reported yet"
+sentinel (see `State.lean`), which is sound because `Nat`'s minimum
+value is `0`: any real first report `.at t` satisfies `t ≥ 0`. -/
+def Frontier.advances (new old : Frontier) : Bool :=
+  match old, new with
+  | .empty, .empty => true
+  | .empty, .at _ => false
+  | .at _, .empty => true
+  | .at o, .at n => Nat.ble o n
+
+/-- The three frontier kinds a `Frontiers` response can report, per
+`response.rs`'s `FrontiersResponse`. -/
+inductive FrontierKind where
+  | write | input | output
+  deriving Repr
+
+/-- The three protocol stages from `protocol.rs`'s module doc. -/
+inductive Stage where
+  | creation | initialization | computation
+  deriving Repr
+
+def Stage.isCreation : Stage → Bool
+  | .creation => true
+  | _ => false
+
+/-- Lifecycle of a single `Peek` (identified by its `uuid`), per the
+1:1 `Peek`/`PeekResponse` contract in `command.rs`/`response.rs`. -/
+inductive PeekState where
+  | notSeen | pending | answered
+  deriving Repr
+
+def PeekState.isNotSeen : PeekState → Bool
+  | .notSeen => true
+  | _ => false
+
+def PeekState.isPending : PeekState → Bool
+  | .pending => true
+  | _ => false
+
+def PeekState.isAnswered : PeekState → Bool
+  | .answered => true
+  | _ => false
+
+/-- A `step` arm's precondition check: `some s` if `cond` holds, else
+`none`. A `none` result models the doc comments' "undefined behavior"
+clause: the model has nothing further to say, rather than inventing
+recovery behavior the protocol does not specify. -/
+def guard (cond : Bool) (s : α) : Option α :=
+  if cond then some s else none
+
+/-- Whether an optional new frontier report (`none` = this kind was
+not reported this time) is compatible with the previously reported
+value. `none` is always compatible: an absent field means "unchanged",
+per `FrontiersResponse`'s doc comment. -/
+def checkAdvance (new? : Option Frontier) (old : Frontier) : Bool :=
+  match new? with
+  | none => true
+  | some new => Frontier.advances new old
+
+/-- Applies an optional new frontier report, keeping the old value
+when the report is absent. -/
+def applyAdvance (new? : Option Frontier) (old : Frontier) : Frontier :=
+  match new? with
+  | none => old
+  | some new => new
+
+end MzCompute
+
+namespace MzCompute
+
+example : Frontier.advances (.at 5) (.at 3) = true := by rfl
+example : Frontier.advances (.at 2) (.at 3) = false := by rfl
+example : Frontier.advances .empty (.at 3) = true := by rfl
+example : Frontier.advances (.at 3) .empty = false := by rfl
+example : Frontier.advances .empty .empty = true := by rfl
+example : checkAdvance none (.at 3) = true := by rfl
+example : checkAdvance (some (.at 2)) (.at 3) = false := by rfl
+example : applyAdvance none (.at 3) = .at 3 := by rfl
+example : applyAdvance (some (.at 5)) (.at 3) = .at 5 := by rfl
+
+end MzCompute

From 74d51ad81ccee3b67c83a1e0ced67d36ec521a25 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 10:26:04 +0200
Subject: [PATCH 05/15] lean: add ComputeCommand/ComputeResponse/Event mirror
 types

---
 doc/developer/semantics/MzCompute.lean       |   1 +
 doc/developer/semantics/MzCompute/Event.lean | 103 +++++++++++++++++++
 2 files changed, 104 insertions(+)
 create mode 100644 doc/developer/semantics/MzCompute/Event.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index e50c2e7bb1883..9d12b7a6aa38f 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -11,3 +11,4 @@
 -- added by the plan task that introduces it.
 
 import MzCompute.Basic
+import MzCompute.Event
diff --git a/doc/developer/semantics/MzCompute/Event.lean b/doc/developer/semantics/MzCompute/Event.lean
new file mode 100644
index 0000000000000..43859743d85cf
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Event.lean
@@ -0,0 +1,103 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Inductive mirror of `ComputeCommand` (command.rs) and
+-- `ComputeResponse` (response.rs). Payload fields with no bearing on
+-- protocol-level legality (`RelationDesc`, `Row`, `DataflowDescription`'s
+-- internals, `RowSetFinishing`, and similar) are left out entirely
+-- rather than modeled as an opaque placeholder: nothing in this
+-- model's theorems needs them, so there is nothing to erase. See
+-- doc/developer/design/20260724_compute_protocol_semantics.md's
+-- "State and events" section for the opaque/concrete boundary this
+-- follows.
+
+import MzCompute.Basic
+
+namespace MzCompute
+
+/-- `Peek`'s target, per `command.rs`'s `PeekTarget`. Only `.index`
+peeks are required to reference a previously created collection (see
+theorem 2 in `Staging.lean`). `.persist` peeks target a storage
+collection this model does not track. -/
+inductive PeekTarget where
+  | index (id : GlobalId)
+  | persist (id : GlobalId)
+  deriving Repr
+
+/-- Mirrors `command.rs`'s `ComputeCommand`. -/
+inductive ComputeCommand where
+  | hello (nonce : Uuid)
+  | createInstance
+  | initializationComplete
+  | updateConfiguration
+  | createDataflow (exports : List GlobalId)
+  | schedule (id : GlobalId)
+  | allowWrites (id : GlobalId)
+  | allowCompaction (id : GlobalId) (frontier : Frontier)
+  | peek (uuid : Uuid) (target : PeekTarget)
+  | cancelPeek (uuid : Uuid)
+  deriving Repr
+
+/-- Mirrors `response.rs`'s `ComputeResponse`. `frontiers` carries the
+three optional per-kind reports from `FrontiersResponse` directly
+(write, input, output), rather than one event per kind, matching the
+real wire response. -/
+inductive ComputeResponse where
+  | frontiers (id : GlobalId) (write input output : Option Frontier)
+  | peekResponse (uuid : Uuid)
+  | subscribeResponse (id : GlobalId)
+  | copyToResponse (id : GlobalId)
+  | status
+  deriving Repr
+
+inductive Event where
+  | cmd (c : ComputeCommand)
+  | resp (r : ComputeResponse)
+  deriving Repr
+
+def Event.isHello : Event → Bool
+  | .cmd (.hello _) => true
+  | _ => false
+
+def Event.isCreateInstance : Event → Bool
+  | .cmd .createInstance => true
+  | _ => false
+
+/-- Whether `e` is one of the event kinds `command.rs`/`response.rs`
+require a prior `CreateDataflow` for `id`: `Schedule`, `AllowWrites`,
+`AllowCompaction`, `Peek` on an index target, `Frontiers`,
+`SubscribeResponse`, `CopyToResponse`. `Status` is excluded: it
+carries no `GlobalId` in the current protocol (see theorem 2's doc
+comment in `Staging.lean`). `CreateDataflow` itself is excluded: it is
+the event that satisfies the requirement, not one that needs it. -/
+def Event.references : Event → GlobalId → Bool
+  | .cmd (.schedule id'), id => id' == id
+  | .cmd (.allowWrites id'), id => id' == id
+  | .cmd (.allowCompaction id' _), id => id' == id
+  | .cmd (.peek _ (.index id')), id => id' == id
+  | .resp (.frontiers id' _ _ _), id => id' == id
+  | .resp (.subscribeResponse id'), id => id' == id
+  | .resp (.copyToResponse id'), id => id' == id
+  | _, _ => false
+
+end MzCompute
+
+namespace MzCompute
+
+example : Event.isHello (.cmd (.hello 0)) = true := by rfl
+example : Event.isHello (.cmd .createInstance) = false := by rfl
+example : Event.isCreateInstance (.cmd .createInstance) = true := by rfl
+example : Event.references (.cmd (.schedule 7)) 7 = true := by rfl
+example : Event.references (.cmd (.schedule 7)) 8 = false := by rfl
+example : Event.references (.resp .status) 7 = false := by rfl
+example : Event.references (.cmd (.createDataflow [7])) 7 = false := by rfl
+example : Event.references (.cmd (.peek 0 (.persist 7))) 7 = false := by rfl
+example : Event.references (.cmd (.peek 0 (.index 7))) 7 = true := by rfl
+
+end MzCompute

From 9258ba44cd44b8bb6dfba5eb0f9128227a7fd4e4 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 10:33:15 +0200
Subject: [PATCH 06/15] doc: fix design doc to match the plan's
 leave-out-entirely decision

Task 3's review caught that the design doc still described unused
payload fields as an opaque placeholder type, but the implementation
plan (and Event.lean) leave them out of the mirror types entirely.
Update the design doc's "State and events" section to match.
---
 .../design/20260724_compute_protocol_semantics.md  | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/doc/developer/design/20260724_compute_protocol_semantics.md b/doc/developer/design/20260724_compute_protocol_semantics.md
index 32696d77b30f5..cd760c5b1b1be 100644
--- a/doc/developer/design/20260724_compute_protocol_semantics.md
+++ b/doc/developer/design/20260724_compute_protocol_semantics.md
@@ -99,14 +99,16 @@ on:
 `Event := Cmd ComputeCommand | Resp ComputeResponse`, an inductive mirror of
 the two real Rust enums. Fields with no bearing on protocol-level legality
 (`RelationDesc`, `Row`, `DataflowDescription`'s internals, `RowSetFinishing`,
-and similar) are represented by an opaque placeholder type rather than
-reconstructed field for field. Fields legality does depend on (`GlobalId`,
-`Uuid`, `Antichain Timestamp`, the `PeekTarget`'s id) are kept concrete.
+and similar) are left out of the mirror types entirely rather than
+reconstructed field for field or carried as an opaque placeholder: nothing in
+this phase's theorems needs them, so there is nothing to represent. Fields
+legality does depend on (`GlobalId`, `Uuid`, `Antichain Timestamp`, the
+`PeekTarget`'s id) are kept concrete.
 
-Opaquing a field erases whatever structural facts it carries, not only its
+Leaving a field out erases whatever structural facts it carried, not only its
 data content. For example `Peek::literal_constraints`'s documented "the
-vector is never empty" becomes unstatable once that field is opaque. This is
-an accepted Phase 1 cut, not an oversight: only the seven theorems below are
+vector is never empty" becomes unstatable once that field is gone. This is an
+accepted Phase 1 cut, not an oversight: only the seven theorems below are
 committed deliverables, and structural payload facts unrelated to them are
 left for a later phase to pick up if they turn out to matter.
 

From 5675efa18e9cf4393ae5142d8e365bff5bbe90ef Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 10:39:52 +0200
Subject: [PATCH 07/15] lean: add ProtocolState and the step relation

---
 doc/developer/semantics/MzCompute.lean       |   1 +
 doc/developer/semantics/MzCompute/State.lean | 161 +++++++++++++++++++
 2 files changed, 162 insertions(+)
 create mode 100644 doc/developer/semantics/MzCompute/State.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index 9d12b7a6aa38f..1db28f7609392 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -12,3 +12,4 @@
 
 import MzCompute.Basic
 import MzCompute.Event
+import MzCompute.State
diff --git a/doc/developer/semantics/MzCompute/State.lean b/doc/developer/semantics/MzCompute/State.lean
new file mode 100644
index 0000000000000..2f59ab7c09502
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/State.lean
@@ -0,0 +1,161 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- The protocol state machine: `ProtocolState` plus the `step`
+-- relation whose guards encode `command.rs`/`response.rs`'s "invalid
+-- to" / "must" contracts. A `none` result means the doc comments call
+-- the transition undefined behavior. The model stops there rather
+-- than inventing recovery semantics the protocol does not specify.
+
+import MzCompute.Basic
+import MzCompute.Event
+
+namespace MzCompute
+
+/-- Everything `step`'s guards depend on. `created`/`scheduled`/
+`allowedWrites`/`dropped` are total functions `GlobalId → Bool`
+rather than a set or map type, so the model needs no map/set library
+(see Global Constraints in the implementation plan: no Mathlib). -/
+structure ProtocolState where
+  stage : Stage := .creation
+  helloSeen : Bool := false
+  createInstanceSeen : Bool := false
+  /-- Ids exported by a `CreateDataflow` seen so far. -/
+  created : GlobalId → Bool := fun _ => false
+  scheduled : GlobalId → Bool := fun _ => false
+  allowedWrites : GlobalId → Bool := fun _ => false
+  /-- Whether `id` has been allowed to compact to the empty frontier,
+  the canonical "drop" per `command.rs`'s `AllowCompaction` doc. -/
+  dropped : GlobalId → Bool := fun _ => false
+  /-- Last reported value per id and frontier kind. `.at 0` is both
+  the real value `0` and the "nothing reported yet" sentinel. See
+  `Frontier.advances`'s doc comment for why that is sound. -/
+  reportedFrontiers : GlobalId → FrontierKind → Frontier := fun _ _ => .at 0
+  peeks : Uuid → PeekState := fun _ => .notSeen
+
+/-- `true` iff every id in `exports` is currently un-created and the
+list has no internal duplicates, matching `command.rs`'s "dataflow
+exports have unique IDs... do not repeat". Written by hand recursion
+rather than `List.Nodup`/`List.Pairwise` (Mathlib-only in the relevant
+form. See Global Constraints). -/
+def freshExports (created : GlobalId → Bool) : List GlobalId → Bool
+  | [] => true
+  | id :: rest => !created id && !rest.elem id && freshExports created rest
+
+/-- The protocol step relation. Each `ComputeCommand`/`ComputeResponse`
+variant gets one equation. The comment above each cites the
+`command.rs`/`response.rs` sentence its guard encodes. -/
+def step (s : ProtocolState) : Event → Option ProtocolState
+  -- protocol.rs: Hello is the first command of the Creation stage.
+  | .cmd (.hello _) =>
+      guard (s.stage.isCreation && !s.helloSeen)
+        { s with helloSeen := true }
+  -- protocol.rs: CreateInstance completes the Creation stage and
+  -- begins Initialization.
+  | .cmd .createInstance =>
+      guard (s.stage.isCreation && s.helloSeen && !s.createInstanceSeen)
+        { s with createInstanceSeen := true, stage := .initialization }
+  -- protocol.rs: InitializationComplete marks the end of the
+  -- Initialization stage.
+  | .cmd .initializationComplete =>
+      guard (match s.stage with | .initialization => true | _ => false)
+        { s with stage := .computation }
+  -- protocol.rs: UpdateConfiguration is a computation-stage command.
+  | .cmd .updateConfiguration =>
+      guard (!s.stage.isCreation) s
+  -- command.rs:107-108: dataflow exports have unique IDs and do not
+  -- repeat.
+  | .cmd (.createDataflow exports) =>
+      guard (!s.stage.isCreation && freshExports s.created exports)
+        { s with created := fun id => s.created id || exports.elem id }
+  -- command.rs:148-153: Schedule requires a prior CreateDataflow and
+  -- is invalid once the collection has been allowed to compact to
+  -- the empty frontier.
+  | .cmd (.schedule id) =>
+      guard (!s.stage.isCreation && s.created id && !s.dropped id)
+        { s with scheduled := fun id' => id' == id || s.scheduled id' }
+  -- command.rs:158-163: AllowWrites requires a prior CreateDataflow
+  -- and is invalid once the collection has been dropped.
+  | .cmd (.allowWrites id) =>
+      guard (!s.stage.isCreation && s.created id && !s.dropped id)
+        { s with allowedWrites := fun id' => id' == id || s.allowedWrites id' }
+  -- command.rs:185-187, :200-201: AllowCompaction requires a prior
+  -- CreateDataflow. An empty frontier is the canonical way to drop a
+  -- collection.
+  | .cmd (.allowCompaction id frontier) =>
+      let isEmpty := match frontier with | .empty => true | .at _ => false
+      guard (!s.stage.isCreation && s.created id)
+        { s with dropped := fun id' => s.dropped id' || (id' == id && isEmpty) }
+  -- command.rs:219-224: an index-target Peek requires a prior
+  -- CreateDataflow for the target. Persist-target peeks do not.
+  -- command.rs:223-224: the peek's uuid must be unique.
+  | .cmd (.peek uuid target) =>
+      guard (!s.stage.isCreation && (s.peeks uuid).isNotSeen
+             && (match target with | .index id => s.created id | .persist _ => true))
+        { s with peeks := fun u => if u == uuid then .pending else s.peeks u }
+  -- command.rs:248-250: CancelPeek requires a prior matching Peek.
+  | .cmd (.cancelPeek uuid) =>
+      guard (!s.stage.isCreation && !(s.peeks uuid).isNotSeen) s
+  -- response.rs:37-52: Frontiers reports must never regress, and
+  -- response.rs:52-54 requires a prior CreateDataflow.
+  | .resp (.frontiers id write? input? output?) =>
+      guard (!s.stage.isCreation && s.created id
+             && checkAdvance write? (s.reportedFrontiers id .write)
+             && checkAdvance input? (s.reportedFrontiers id .input)
+             && checkAdvance output? (s.reportedFrontiers id .output))
+        { s with reportedFrontiers := fun id' k =>
+            if id' == id then
+              match k with
+              | .write => applyAdvance write? (s.reportedFrontiers id .write)
+              | .input => applyAdvance input? (s.reportedFrontiers id .input)
+              | .output => applyAdvance output? (s.reportedFrontiers id .output)
+            else s.reportedFrontiers id' k }
+  -- response.rs:66: exactly one PeekResponse per Peek, so this
+  -- requires the peek to currently be pending.
+  | .resp (.peekResponse uuid) =>
+      guard (!s.stage.isCreation && (s.peeks uuid).isPending)
+        { s with peeks := fun u => if u == uuid then .answered else s.peeks u }
+  -- response.rs:106-107: SubscribeResponse requires a prior
+  -- CreateDataflow.
+  | .resp (.subscribeResponse id) =>
+      guard (!s.stage.isCreation && s.created id) s
+  -- response.rs:120-121: CopyToResponse requires a prior
+  -- CreateDataflow.
+  | .resp (.copyToResponse id) =>
+      guard (!s.stage.isCreation && s.created id) s
+  -- response.rs:130-131: Status has no effect on collection
+  -- lifecycles and carries no GlobalId in the current protocol.
+  | .resp .status =>
+      some s
+
+end MzCompute
+
+namespace MzCompute
+
+-- Hello is legal from the initial state.
+example : (step {} (.cmd (.hello 0))).isSome = true := by decide
+-- CreateInstance is illegal before Hello.
+example : step {} (.cmd .createInstance) = none := by decide
+-- Schedule is illegal before any CreateDataflow.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true }
+    (.cmd (.schedule 7)) = none := by decide
+-- Schedule is legal once id 7 has been created.
+example : (step { stage := .computation, createInstanceSeen := true, helloSeen := true, created := fun id => id == 7 }
+    (.cmd (.schedule 7))).isSome = true := by decide
+-- Schedule is illegal once id 7 has been dropped.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true, created := fun id => id == 7, dropped := fun id => id == 7 }
+    (.cmd (.schedule 7)) = none := by decide
+-- CreateDataflow rejects a duplicate id within the same export list.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true }
+    (.cmd (.createDataflow [7, 7])) = none := by decide
+-- A second PeekResponse for an already-answered uuid is illegal.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true, peeks := fun u => if u == 0 then .answered else .notSeen }
+    (.resp (.peekResponse 0)) = none := by decide
+
+end MzCompute

From 08260cb563717c63224629264ee22dcbcbcb71ec Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 10:46:38 +0200
Subject: [PATCH 08/15] lean: gate index-target Peek on dropped collections

Task 4's step relation was missing the !dropped check on index-target
Peek that Schedule/AllowWrites already had, inconsistent with the
no_reference_after_drop theorem's stated intent for peekIndex_fails_when_dropped.
Found by task review.
---
 doc/developer/semantics/MzCompute/State.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/doc/developer/semantics/MzCompute/State.lean b/doc/developer/semantics/MzCompute/State.lean
index 2f59ab7c09502..89e52bdffcd07 100644
--- a/doc/developer/semantics/MzCompute/State.lean
+++ b/doc/developer/semantics/MzCompute/State.lean
@@ -93,11 +93,13 @@ def step (s : ProtocolState) : Event → Option ProtocolState
       guard (!s.stage.isCreation && s.created id)
         { s with dropped := fun id' => s.dropped id' || (id' == id && isEmpty) }
   -- command.rs:219-224: an index-target Peek requires a prior
-  -- CreateDataflow for the target. Persist-target peeks do not.
+  -- CreateDataflow for the target and is treated as illegal once the
+  -- target has been dropped, matching Schedule/AllowWrites. Persist-target
+  -- peeks require neither.
   -- command.rs:223-224: the peek's uuid must be unique.
   | .cmd (.peek uuid target) =>
       guard (!s.stage.isCreation && (s.peeks uuid).isNotSeen
-             && (match target with | .index id => s.created id | .persist _ => true))
+             && (match target with | .index id => s.created id && !s.dropped id | .persist _ => true))
         { s with peeks := fun u => if u == uuid then .pending else s.peeks u }
   -- command.rs:248-250: CancelPeek requires a prior matching Peek.
   | .cmd (.cancelPeek uuid) =>
@@ -154,6 +156,9 @@ example : step { stage := .computation, createInstanceSeen := true, helloSeen :=
 -- CreateDataflow rejects a duplicate id within the same export list.
 example : step { stage := .computation, createInstanceSeen := true, helloSeen := true }
     (.cmd (.createDataflow [7, 7])) = none := by decide
+-- An index-target Peek is illegal once its target id has been dropped.
+example : step { stage := .computation, createInstanceSeen := true, helloSeen := true, created := fun id => id == 7, dropped := fun id => id == 7 }
+    (.cmd (.peek 0 (.index 7))) = none := by decide
 -- A second PeekResponse for an already-answered uuid is illegal.
 example : step { stage := .computation, createInstanceSeen := true, helloSeen := true, peeks := fun u => if u == 0 then .answered else .notSeen }
     (.resp (.peekResponse 0)) = none := by decide

From 6556c03e19d0aa15880e7f24a3f44a3e118e2f4d Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 10:52:45 +0200
Subject: [PATCH 09/15] lean: add run/WellFormed and sanity example traces

---
 doc/developer/semantics/MzCompute.lean     |  1 +
 doc/developer/semantics/MzCompute/Run.lean | 71 ++++++++++++++++++++++
 2 files changed, 72 insertions(+)
 create mode 100644 doc/developer/semantics/MzCompute/Run.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index 1db28f7609392..ae412b80323ec 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -13,3 +13,4 @@
 import MzCompute.Basic
 import MzCompute.Event
 import MzCompute.State
+import MzCompute.Run
diff --git a/doc/developer/semantics/MzCompute/Run.lean b/doc/developer/semantics/MzCompute/Run.lean
new file mode 100644
index 0000000000000..e80c4b613bfdd
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Run.lean
@@ -0,0 +1,71 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Folding `step` over a list of events into an execution, and the
+-- well-formedness predicate the plan's theorems are stated over.
+
+import MzCompute.State
+
+namespace MzCompute
+
+def initState : ProtocolState := {}
+
+/-- Folds `step` over `es` starting from `s`, short-circuiting to
+`none` at the first illegal event. -/
+def run (s : ProtocolState) : List Event → Option ProtocolState
+  | [] => some s
+  | e :: rest =>
+      match step s e with
+      | none => none
+      | some s' => run s' rest
+
+/-- An execution is well-formed iff folding `step` from `initState`
+never hits an illegal event. -/
+def WellFormed (es : List Event) : Prop := ∃ s, run initState es = some s
+
+end MzCompute
+
+namespace MzCompute
+
+/-- A minimal legal trace: handshake, create a dataflow exporting id
+`1`, schedule it, report its write frontier advancing to `5`, peek it,
+answer the peek, then drop it. -/
+def legalTrace : List Event :=
+  [ .cmd (.hello 0)
+  , .cmd .createInstance
+  , .cmd .initializationComplete
+  , .cmd (.createDataflow [1])
+  , .cmd (.schedule 1)
+  , .resp (.frontiers 1 (some (.at 5)) none none)
+  , .cmd (.peek 10 (.index 1))
+  , .resp (.peekResponse 10)
+  , .cmd (.allowCompaction 1 .empty)
+  ]
+
+example : WellFormed legalTrace := by
+  refine ⟨?_, ?_⟩
+  · exact (run initState legalTrace).get (by decide)
+  · rfl
+
+/-- Same trace, but with the `Schedule` moved before `CreateDataflow`:
+illegal per command.rs:148-150. -/
+def illegalTrace : List Event :=
+  [ .cmd (.hello 0)
+  , .cmd .createInstance
+  , .cmd .initializationComplete
+  , .cmd (.schedule 1)
+  , .cmd (.createDataflow [1])
+  ]
+
+example : ¬ WellFormed illegalTrace := by
+  rintro ⟨s, hs⟩
+  rw [show run initState illegalTrace = none from rfl] at hs
+  cases hs
+
+end MzCompute

From 39b4b49f6be55d5dade118f222ac2b111740706b Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 11:13:35 +0200
Subject: [PATCH 10/15] lean: prove staging theorems (hello/create-instance
 order, create-before-reference)

Proves the plan's first two target theorems in `Staging.lean`:
`hello_first`, `create_instance_second`, and the `created` invariant
chain (`created_of_step`, `created_of_run_from`, `created_of_run`)
culminating in `create_before_reference`.

Fixes a soundness gap this MVP surfaced in `step`: the `Status`
response arm returned `some s` unconditionally, so a `Status` before
`Hello` (or as the second event) was legal. That made `hello_first`
and `create_instance_second` false as stated. Every other response
already requires `!s.stage.isCreation`; the fix gives `Status` the
same guard, matching the protocol's "nothing on the wire before the
connection is established" intent.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
---
 doc/developer/semantics/MzCompute.lean        |   1 +
 .../semantics/MzCompute/Staging.lean          | 202 ++++++++++++++++++
 doc/developer/semantics/MzCompute/State.lean  |   7 +-
 3 files changed, 208 insertions(+), 2 deletions(-)
 create mode 100644 doc/developer/semantics/MzCompute/Staging.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index ae412b80323ec..275cfb509e096 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -14,3 +14,4 @@ import MzCompute.Basic
 import MzCompute.Event
 import MzCompute.State
 import MzCompute.Run
+import MzCompute.Staging
diff --git a/doc/developer/semantics/MzCompute/Staging.lean b/doc/developer/semantics/MzCompute/Staging.lean
new file mode 100644
index 0000000000000..ef25111020e6c
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Staging.lean
@@ -0,0 +1,202 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Staging-order theorems: the first two commands of any legal
+-- execution are `Hello` then `CreateInstance`, and any event naming a
+-- collection `id` requires a prior `CreateDataflow` exporting `id`.
+-- These are the plan's Minimal Viable Prototype, validating the
+-- state/step/run shape before the drop, frontier, and peek theorems.
+
+import MzCompute.Run
+
+namespace MzCompute
+
+/-- Theorem 1. Encodes protocol.rs:52-58: Hello is the first command
+of the Creation stage. -/
+theorem hello_first (e : Event) (rest : List Event) (s : ProtocolState)
+    (h : run initState (e :: rest) = some s) : e.isHello = true := by
+  unfold run at h
+  cases e with
+  | cmd c =>
+      cases c with
+      | hello _ => rfl
+      | _ => simp [step, guard, initState, Stage.isCreation] at h
+  | resp r =>
+      cases r <;> simp [step, guard, initState, Stage.isCreation] at h
+
+/-- Theorem 1, continued. Encodes protocol.rs:52-58: CreateInstance is
+the second command, completing the Creation stage. -/
+theorem create_instance_second (e1 e2 : Event) (rest : List Event) (s : ProtocolState)
+    (h : run initState (e1 :: e2 :: rest) = some s) : e2.isCreateInstance = true := by
+  have he1 : e1.isHello = true := hello_first e1 (e2 :: rest) s h
+  unfold run at h
+  cases e1 with
+  | cmd c =>
+      cases c with
+      | hello n =>
+          cases e2 with
+          | cmd c2 =>
+              cases c2 with
+              | createInstance => rfl
+              | _ => simp [run, step, guard, initState, Stage.isCreation] at h
+          | resp r2 => cases r2 <;> simp [run, step, guard, initState, Stage.isCreation] at h
+      | _ => simp [Event.isHello] at he1
+  | resp _ => simp [Event.isHello] at he1
+
+/-- A successful `guard` returns its payload unchanged. -/
+private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : x = y := by
+  unfold guard at h
+  cases cond with
+  | true => simpa using h
+  | false => simp at h
+
+/-- A successful `guard` witnesses its condition held. -/
+private theorem guard_cond {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : cond = true := by
+  unfold guard at h
+  cases cond with
+  | true => rfl
+  | false => simp at h
+
+/-- A single step either preserves `created` or, for a `CreateDataflow`
+event, adds exactly its export list. -/
+theorem created_of_step (s s' : ProtocolState) (e : Event) (h : step s e = some s') (id : GlobalId) :
+    s'.created id = true →
+      s.created id = true ∨ ∃ exports, e = .cmd (.createDataflow exports) ∧ exports.elem id = true := by
+  intro hc
+  cases e with
+  | cmd c =>
+      cases c with
+      | createDataflow exports =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          simp only [Bool.or_eq_true] at hc
+          rcases hc with h1 | h2
+          · exact Or.inl h1
+          · exact Or.inr ⟨exports, rfl, h2⟩
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact Or.inl hc
+  | resp r =>
+      cases r <;>
+        (simp only [step] at h
+         have hs := guard_eq_some h
+         subst hs
+         exact Or.inl hc)
+
+/-- Generalization of `created_of_run` over the starting state, the
+form the induction needs. -/
+theorem created_of_run_from (es : List Event) (s0 s : ProtocolState) (h : run s0 es = some s)
+    (id : GlobalId) (hc : s.created id = true) :
+    s0.created id = true ∨
+      ∃ (pre : List Event) (exports : List GlobalId) (suf : List Event),
+        es = pre ++ [.cmd (.createDataflow exports)] ++ suf ∧ exports.elem id = true := by
+  induction es generalizing s0 with
+  | nil => simp [run] at h; subst h; exact Or.inl hc
+  | cons e rest ih =>
+      unfold run at h
+      cases hstep : step s0 e with
+      | none => simp [hstep] at h
+      | some s1 =>
+          simp only [hstep] at h
+          rcases ih s1 h with h1 | ⟨pre, exports, suf, heq, hel⟩
+          · rcases created_of_step s0 s1 e hstep id h1 with h0 | ⟨exports, heq, hel⟩
+            · exact Or.inl h0
+            · exact Or.inr ⟨[], exports, rest, by simp [heq], hel⟩
+          · exact Or.inr ⟨e :: pre, exports, suf, by simp [heq], hel⟩
+
+/-- Lifting `created_of_step` across a whole execution: if `id` is
+created at the end, some `CreateDataflow` event in the execution
+exported it. -/
+theorem created_of_run (es : List Event) (s : ProtocolState) (h : run initState es = some s)
+    (id : GlobalId) (hc : s.created id = true) :
+    ∃ (pre : List Event) (exports : List GlobalId) (suf : List Event),
+      es = pre ++ [.cmd (.createDataflow exports)] ++ suf ∧ exports.elem id = true := by
+  rcases created_of_run_from es initState s h id hc with h0 | hex
+  · simp [initState] at h0
+  · exact hex
+
+/-- Theorem 2. Encodes command.rs:148-153, :158-163, :185-187,
+:219-224 and response.rs:52-54, :106-107, :120-121: any event naming
+`id` (other than the `CreateDataflow` that creates it) requires a
+prior `CreateDataflow` exporting `id`. -/
+theorem create_before_reference (pre : List Event) (mid : Event) (id : GlobalId)
+    (s s' : ProtocolState)
+    (hpre : run initState pre = some s)
+    (hstep : step s mid = some s')
+    (href : mid.references id = true) :
+    ∃ (pre' : List Event) (exports : List GlobalId) (suf : List Event),
+      pre = pre' ++ [.cmd (.createDataflow exports)] ++ suf ∧ exports.elem id = true := by
+  have hc : s.created id = true := by
+    cases mid with
+    | cmd c =>
+        cases c with
+        | schedule id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | allowWrites id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | allowCompaction id' _ =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | peek _ target =>
+            cases target with
+            | index id' =>
+                simp only [Event.references, beq_iff_eq] at href
+                subst href
+                simp only [step] at hstep
+                have hcond := guard_cond hstep
+                simp only [Bool.and_eq_true] at hcond
+                simp_all
+            | persist _ => simp [Event.references] at href
+        | _ => simp [Event.references] at href
+    | resp r =>
+        cases r with
+        | frontiers id' _ _ _ =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | subscribeResponse id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | copyToResponse id' =>
+            simp only [Event.references, beq_iff_eq] at href
+            subst href
+            simp only [step] at hstep
+            have hcond := guard_cond hstep
+            simp only [Bool.and_eq_true] at hcond
+            simp_all
+        | _ => simp [Event.references] at href
+  exact created_of_run pre s hpre id hc
+
+end MzCompute
diff --git a/doc/developer/semantics/MzCompute/State.lean b/doc/developer/semantics/MzCompute/State.lean
index 89e52bdffcd07..e5b48b033b4ca 100644
--- a/doc/developer/semantics/MzCompute/State.lean
+++ b/doc/developer/semantics/MzCompute/State.lean
@@ -132,9 +132,12 @@ def step (s : ProtocolState) : Event → Option ProtocolState
   | .resp (.copyToResponse id) =>
       guard (!s.stage.isCreation && s.created id) s
   -- response.rs:130-131: Status has no effect on collection
-  -- lifecycles and carries no GlobalId in the current protocol.
+  -- lifecycles and carries no GlobalId in the current protocol. Like
+  -- every other response, it is only legal once the connection is
+  -- established, i.e. past the Creation stage. A response arriving
+  -- before Hello/CreateInstance is undefined behavior.
   | .resp .status =>
-      some s
+      guard (!s.stage.isCreation) s
 
 end MzCompute
 

From e6613e4e9896fdcd633804d8335861fe9555e272 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 11:23:39 +0200
Subject: [PATCH 11/15] lean: prove legality theorems (no-reference-after-drop,
 create-dataflow-ids-fresh)

---
 doc/developer/semantics/MzCompute.lean        |   1 +
 .../semantics/MzCompute/Legality.lean         | 130 ++++++++++++++++++
 2 files changed, 131 insertions(+)
 create mode 100644 doc/developer/semantics/MzCompute/Legality.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index 275cfb509e096..814b548163306 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -15,3 +15,4 @@ import MzCompute.Event
 import MzCompute.State
 import MzCompute.Run
 import MzCompute.Staging
+import MzCompute.Legality
diff --git a/doc/developer/semantics/MzCompute/Legality.lean b/doc/developer/semantics/MzCompute/Legality.lean
new file mode 100644
index 0000000000000..61855b059f203
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Legality.lean
@@ -0,0 +1,130 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Theorems 3-4: a dropped collection can't be referenced again, and
+-- CreateDataflow's export ids are fresh.
+
+import MzCompute.State
+import MzCompute.Run
+
+namespace MzCompute
+
+/-- A successful `guard` returns its payload unchanged. -/
+private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : x = y := by
+  unfold guard at h
+  cases cond with
+  | true => simpa using h
+  | false => simp at h
+
+/-- Theorem 3, part 1. Encodes command.rs:152-153. -/
+theorem schedule_fails_when_dropped (s : ProtocolState) (id : GlobalId) (h : s.dropped id = true) :
+    step s (.cmd (.schedule id)) = none := by
+  simp [step, guard, h]
+
+/-- Theorem 3, part 2. Encodes command.rs:162-163. -/
+theorem allowWrites_fails_when_dropped (s : ProtocolState) (id : GlobalId) (h : s.dropped id = true) :
+    step s (.cmd (.allowWrites id)) = none := by
+  simp [step, guard, h]
+
+/-- Theorem 3, part 3. `command.rs` does not give index-peek-after-drop
+the same explicit "invalid to" wording as Schedule/AllowWrites, but a
+dropped collection's arrangement is gone, so this model treats it the
+same way (see the design doc's Solution Proposal). -/
+theorem peekIndex_fails_when_dropped (s : ProtocolState) (id uuid : Uuid) (h : s.dropped id = true) :
+    step s (.cmd (.peek uuid (.index id))) = none := by
+  simp [step, guard, h]
+
+/-- `dropped` only ever grows: no step un-drops a collection. -/
+theorem dropped_monotone (s s' : ProtocolState) (e : Event) (h : step s e = some s') (id : GlobalId) :
+    s.dropped id = true → s'.dropped id = true := by
+  intro hd
+  cases e with
+  | cmd c =>
+      cases c with
+      | allowCompaction id' frontier =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          simp [hd]
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact hd
+  | resp r =>
+      cases r <;>
+        (simp only [step] at h
+         have hs := guard_eq_some h
+         subst hs
+         exact hd)
+
+/-- Theorem 3, lifted across a whole execution. Once `id` is dropped,
+no later `Schedule`, `AllowWrites`, or index-target `Peek` for `id`
+can succeed. -/
+theorem no_reference_after_drop (pre mid : List Event) (e : Event) (id uuid : Uuid)
+    (s s' s'' : ProtocolState)
+    (hpre : run initState pre = some s)
+    (hdrop : s.dropped id = true)
+    (hmid : run s mid = some s')
+    (he : e = .cmd (.schedule id) ∨ e = .cmd (.allowWrites id) ∨ e = .cmd (.peek uuid (.index id)))
+    (hstep : step s' e = some s'') : False := by
+  have hdrop' : s'.dropped id = true := by
+    clear hpre he hstep
+    induction mid generalizing s with
+    | nil => simp [run] at hmid; subst hmid; exact hdrop
+    | cons e0 rest ih =>
+        unfold run at hmid
+        cases hstep0 : step s e0 with
+        | none => simp [hstep0] at hmid
+        | some s1 =>
+            simp only [hstep0] at hmid
+            exact ih s1 (dropped_monotone s s1 e0 hstep0 id hdrop) hmid
+  rcases he with he | he | he
+  · rw [he, schedule_fails_when_dropped s' id hdrop'] at hstep; simp at hstep
+  · rw [he, allowWrites_fails_when_dropped s' id hdrop'] at hstep; simp at hstep
+  · rw [he, peekIndex_fails_when_dropped s' id uuid hdrop'] at hstep; simp at hstep
+
+/-- Decodes `freshExports`'s `Bool` into the two `Prop`s `command.rs`
+states in English: no id in `exports` is already created, and
+`exports` has no internal duplicate. -/
+theorem freshExports_sound (created : GlobalId → Bool) (exports : List GlobalId)
+    (h : freshExports created exports = true) :
+    (∀ id ∈ exports, created id = false) ∧ exports.Nodup := by
+  induction exports with
+  | nil => exact ⟨by simp, List.nodup_nil⟩
+  | cons id rest ih =>
+      simp only [freshExports, Bool.and_eq_true] at h
+      obtain ⟨⟨hnc, hne⟩, hrest⟩ := h
+      obtain ⟨ihc, ihn⟩ := ih hrest
+      refine ⟨?_, ?_⟩
+      · intro id' hmem
+        simp only [List.mem_cons] at hmem
+        rcases hmem with rfl | hmem
+        · simpa using hnc
+        · exact ihc id' hmem
+      · rw [List.nodup_cons]
+        refine ⟨?_, ihn⟩
+        intro hmem
+        exact absurd (List.elem_eq_true_of_mem hmem) (by simpa using hne)
+
+/-- Theorem 4. Encodes command.rs:107-108: a CreateDataflow's export
+ids are pairwise distinct and disjoint from every id created earlier
+in the execution. -/
+theorem create_dataflow_ids_fresh (s s' : ProtocolState) (exports : List GlobalId)
+    (h : step s (.cmd (.createDataflow exports)) = some s') :
+    (∀ id ∈ exports, s.created id = false) ∧ exports.Nodup := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    rw [Bool.and_eq_true] at hcond
+    exact freshExports_sound s.created exports hcond.2
+  · contradiction
+
+end MzCompute

From cb38e5b2562a2ba9df89b0b1a550ba18d4c86765 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 11:36:03 +0200
Subject: [PATCH 12/15] lean: prove frontier monotonicity and terminality
 theorem

---
 doc/developer/semantics/MzCompute.lean        |   1 +
 .../semantics/MzCompute/Frontiers.lean        | 159 ++++++++++++++++++
 2 files changed, 160 insertions(+)
 create mode 100644 doc/developer/semantics/MzCompute/Frontiers.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index 814b548163306..9256bb8de0e3d 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -16,3 +16,4 @@ import MzCompute.State
 import MzCompute.Run
 import MzCompute.Staging
 import MzCompute.Legality
+import MzCompute.Frontiers
diff --git a/doc/developer/semantics/MzCompute/Frontiers.lean b/doc/developer/semantics/MzCompute/Frontiers.lean
new file mode 100644
index 0000000000000..2998e02bde2ca
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Frontiers.lean
@@ -0,0 +1,159 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Theorem 5: reported frontiers never regress, and once a kind
+-- reports the empty frontier for an id, it stays empty.
+
+import MzCompute.State
+import MzCompute.Run
+
+namespace MzCompute
+
+theorem Frontier.advances_refl (f : Frontier) : Frontier.advances f f = true := by
+  cases f with
+  | «at» t => simp [Frontier.advances, Nat.ble_eq]
+  | empty => rfl
+
+theorem Frontier.advances_trans {a b c : Frontier}
+    (hab : Frontier.advances b a = true) (hbc : Frontier.advances c b = true) :
+    Frontier.advances c a = true := by
+  cases a with
+  | empty => cases b with
+      | empty => cases c with
+          | empty => rfl
+          | «at» _ => simp [Frontier.advances] at hbc
+      | «at» _ => simp [Frontier.advances] at hab
+  | «at» o =>
+      cases b with
+      | empty => cases c with
+          | empty => rfl
+          | «at» _ => simp [Frontier.advances] at hbc
+      | «at» m =>
+          cases c with
+          | empty => rfl
+          | «at» n =>
+              simp only [Frontier.advances] at hab hbc ⊢
+              exact Nat.ble_eq_true_of_le
+                (Nat.le_trans (Nat.le_of_ble_eq_true hab) (Nat.le_of_ble_eq_true hbc))
+
+/-- Only `.empty` can advance past `.empty`. -/
+theorem Frontier.advances_empty_inv (new : Frontier) (h : Frontier.advances new .empty = true) :
+    new = .empty := by
+  cases new with
+  | empty => rfl
+  | «at» _ => simp [Frontier.advances] at h
+
+/-- A passing `checkAdvance` guarantees the applied result advances the
+old value: when the report is absent the value is unchanged (reflexive),
+and when present the guard is exactly `Frontier.advances`. -/
+theorem checkAdvance_advances (new? : Option Frontier) (old : Frontier)
+    (h : checkAdvance new? old = true) : Frontier.advances (applyAdvance new? old) old = true := by
+  cases new? with
+  | none => exact Frontier.advances_refl old
+  | some new => simpa [checkAdvance, applyAdvance] using h
+
+/-- Theorem 5, single-step form. Encodes response.rs:37-42
+(monotonicity) and :44-51 (terminality, which is the same fact
+specialized to `old = .empty` via `advances_empty_inv`). -/
+theorem frontiers_advance (s s' : ProtocolState) (id : GlobalId) (w i o : Option Frontier)
+    (h : step s (.resp (.frontiers id w i o)) = some s') (k : FrontierKind) :
+    Frontier.advances (s'.reportedFrontiers id k) (s.reportedFrontiers id k) = true := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    injection h with h
+    subst h
+    simp only [Bool.and_eq_true] at hcond
+    obtain ⟨⟨⟨⟨-, -⟩, hw⟩, hi⟩, ho⟩ := hcond
+    cases k with
+    | write => simpa using (checkAdvance_advances w (s.reportedFrontiers id .write) hw)
+    | input => simpa using (checkAdvance_advances i (s.reportedFrontiers id .input) hi)
+    | output => simpa using (checkAdvance_advances o (s.reportedFrontiers id .output) ho)
+  · contradiction
+
+/-- A successful `guard` returns its payload unchanged. Local copy of
+the helper `Legality.lean` uses. -/
+private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : x = y := by
+  unfold guard at h
+  cases cond with
+  | true => simpa using h
+  | false => simp at h
+
+/-- Theorem 5, lifted across a whole execution. -/
+theorem reportedFrontiers_monotone (s0 s : ProtocolState) (es : List Event)
+    (h : run s0 es = some s) (id : GlobalId) (k : FrontierKind) :
+    Frontier.advances (s.reportedFrontiers id k) (s0.reportedFrontiers id k) = true := by
+  induction es generalizing s0 with
+  | nil => simp [run] at h; subst h; exact Frontier.advances_refl _
+  | cons e rest ih =>
+      unfold run at h
+      cases hstep : step s0 e with
+      | none => simp [hstep] at h
+      | some s1 =>
+          simp [hstep] at h
+          have h1 : Frontier.advances (s1.reportedFrontiers id k) (s0.reportedFrontiers id k) = true := by
+            cases e with
+            | resp r =>
+                cases r with
+                | frontiers id' w i o =>
+                    by_cases hid : id' = id
+                    · subst id'; exact frontiers_advance s0 s1 id w i o hstep k
+                    · -- A Frontiers response for a different id leaves
+                      -- `reportedFrontiers id k` untouched.
+                      simp only [step] at hstep
+                      have hs := guard_eq_some hstep
+                      subst hs
+                      have hne : (id == id') = false := by
+                        simp only [beq_eq_false_iff_ne, ne_eq]
+                        exact fun heq => hid heq.symm
+                      simp only [hne, if_false, Bool.false_eq_true]
+                      exact Frontier.advances_refl _
+                | peekResponse _ =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+                | subscribeResponse _ =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+                | copyToResponse _ =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+                | status =>
+                    simp only [step] at hstep
+                    have hs := guard_eq_some hstep; subst hs
+                    exact Frontier.advances_refl _
+            | cmd c =>
+                cases c <;>
+                  (simp only [step] at hstep
+                   have hs := guard_eq_some hstep
+                   subst hs
+                   exact Frontier.advances_refl _)
+          exact Frontier.advances_trans h1 (ih s1 h)
+
+/-- Theorem 5, terminality corollary: once a kind reports empty, it
+stays empty for the rest of the execution. -/
+theorem reportedFrontiers_terminal (s0 s : ProtocolState) (es : List Event)
+    (h : run s0 es = some s) (id : GlobalId) (k : FrontierKind)
+    (hempty : s0.reportedFrontiers id k = .empty) :
+    s.reportedFrontiers id k = .empty :=
+  Frontier.advances_empty_inv _ (hempty ▸ reportedFrontiers_monotone s0 s es h id k)
+
+/-- Theorem 5, combined statement: monotonicity plus terminality, over
+an execution rooted at `initState`. -/
+theorem frontiers_monotone_and_terminal (es : List Event) (s : ProtocolState)
+    (h : run initState es = some s) (id : GlobalId) (k : FrontierKind) :
+    Frontier.advances (s.reportedFrontiers id k) (initState.reportedFrontiers id k) = true ∧
+      (initState.reportedFrontiers id k = .empty → s.reportedFrontiers id k = .empty) :=
+  ⟨reportedFrontiers_monotone initState s es h id k,
+   fun hempty => reportedFrontiers_terminal initState s es h id k hempty⟩
+
+end MzCompute

From add4bf2d3cf9e61c17a169bfe7479d0abb9f2aae Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 11:50:55 +0200
Subject: [PATCH 13/15] lean: prove peek theorems (peek-response-unique,
 cancel-requires-peek)

---
 doc/developer/semantics/MzCompute.lean       |   1 +
 doc/developer/semantics/MzCompute/Peeks.lean | 232 +++++++++++++++++++
 2 files changed, 233 insertions(+)
 create mode 100644 doc/developer/semantics/MzCompute/Peeks.lean

diff --git a/doc/developer/semantics/MzCompute.lean b/doc/developer/semantics/MzCompute.lean
index 9256bb8de0e3d..9abf012bf4037 100644
--- a/doc/developer/semantics/MzCompute.lean
+++ b/doc/developer/semantics/MzCompute.lean
@@ -17,3 +17,4 @@ import MzCompute.Run
 import MzCompute.Staging
 import MzCompute.Legality
 import MzCompute.Frontiers
+import MzCompute.Peeks
diff --git a/doc/developer/semantics/MzCompute/Peeks.lean b/doc/developer/semantics/MzCompute/Peeks.lean
new file mode 100644
index 0000000000000..4e3f8baf17dc1
--- /dev/null
+++ b/doc/developer/semantics/MzCompute/Peeks.lean
@@ -0,0 +1,232 @@
+-- Copyright Materialize, Inc. and contributors. All rights reserved.
+--
+-- Use of this software is governed by the Business Source License
+-- included in the LICENSE file at the root of this repository.
+--
+-- As of the Change Date specified in that file, in accordance with
+-- the Business Source License, use of this software will be governed
+-- by the Apache License, Version 2.0.
+--
+-- Theorems 6-7: at most one PeekResponse per Peek, and CancelPeek
+-- requires a prior Peek.
+
+import MzCompute.State
+import MzCompute.Run
+
+namespace MzCompute
+
+/-- A successful `guard` returns its payload unchanged. Local copy of
+the helper `Staging.lean`/`Frontiers.lean` use. -/
+private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : x = y := by
+  unfold guard at h
+  cases cond with
+  | true => simpa using h
+  | false => simp at h
+
+/-- A successful `guard` witnesses its condition held. -/
+private theorem guard_cond {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : cond = true := by
+  unfold guard at h
+  cases cond with
+  | true => rfl
+  | false => simp at h
+
+theorem peekResponse_requires_pending (s s' : ProtocolState) (uuid : Uuid)
+    (h : step s (.resp (.peekResponse uuid)) = some s') :
+    s.peeks uuid = .pending ∧ s'.peeks uuid = .answered := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    injection h with h
+    subst h
+    refine ⟨?_, by simp⟩
+    cases hp : s.peeks uuid with
+    | pending => rfl
+    | notSeen => simp [hp, PeekState.isPending] at hcond
+    | answered => simp [hp, PeekState.isPending] at hcond
+  · contradiction
+
+theorem peek_requires_notSeen (s s' : ProtocolState) (uuid : Uuid) (target : PeekTarget)
+    (h : step s (.cmd (.peek uuid target)) = some s') :
+    s.peeks uuid = .notSeen ∧ s'.peeks uuid = .pending := by
+  simp only [step] at h
+  have hcond := guard_cond h
+  have hs := guard_eq_some h
+  subst hs
+  refine ⟨?_, by simp⟩
+  cases hp : s.peeks uuid with
+  | notSeen => rfl
+  | pending => simp [hp, PeekState.isNotSeen] at hcond
+  | answered => simp [hp, PeekState.isNotSeen] at hcond
+
+/-- Once `.answered`, a peek's state stays `.answered`: no `step` arm
+moves a peek out of `.answered`. -/
+theorem peeks_answered_monotone (s s' : ProtocolState) (e : Event) (h : step s e = some s')
+    (uuid : Uuid) : s.peeks uuid = .answered → s'.peeks uuid = .answered := by
+  intro ha
+  cases e with
+  | cmd c =>
+      cases c with
+      | peek uuid' _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          have hcond := guard_cond h
+          subst hs
+          simp only []
+          split
+          · rename_i heq
+            have huuid : uuid = uuid' := eq_of_beq heq
+            subst huuid
+            simp only [Bool.and_eq_true] at hcond
+            obtain ⟨⟨_, hnot⟩, _⟩ := hcond
+            rw [ha] at hnot
+            simp [PeekState.isNotSeen] at hnot
+          · exact ha
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact ha
+  | resp r =>
+      cases r with
+      | peekResponse uuid' =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          simp only []
+          split
+          · rfl
+          · exact ha
+      | _ =>
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact ha
+
+/-- Theorem 7. Encodes command.rs:248-250. -/
+theorem cancel_requires_peek (s s' : ProtocolState) (uuid : Uuid) (h : step s (.cmd (.cancelPeek uuid)) = some s') :
+    s.peeks uuid ≠ .notSeen := by
+  simp only [step, guard] at h
+  split at h
+  · rename_i hcond
+    intro hcontra
+    simp [hcontra, PeekState.isNotSeen] at hcond
+  · contradiction
+
+/-- A single step either leaves a peek's `notSeen`-ness reflected in the
+prior state, or is exactly the `Peek` that first touched this uuid. Only
+a `Peek uuid _` moves `peeks uuid` out of `notSeen`. A `PeekResponse
+uuid` also writes `peeks uuid`, but its guard already required the peek
+to be `pending`, so the prior state was not `notSeen` either. -/
+theorem peeks_notSeen_of_step (s s' : ProtocolState) (e : Event) (uuid : Uuid)
+    (h : step s e = some s') (hns : s'.peeks uuid ≠ .notSeen) :
+    s.peeks uuid ≠ .notSeen ∨ ∃ target, e = .cmd (.peek uuid target) := by
+  cases e with
+  | cmd c =>
+      cases c with
+      | peek uuid' target =>
+          by_cases huuid : uuid' = uuid
+          · exact Or.inr ⟨target, by rw [huuid]⟩
+          · left
+            simp only [step] at h
+            have hs := guard_eq_some h
+            subst hs
+            simp only [] at hns
+            have hne : (uuid == uuid') = false := by
+              simp only [beq_eq_false_iff_ne, ne_eq]
+              exact fun heq => huuid heq.symm
+            simpa only [hne, if_false, Bool.false_eq_true] using hns
+      | _ =>
+          left
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact hns
+  | resp r =>
+      cases r with
+      | peekResponse uuid' =>
+          left
+          simp only [step] at h
+          have hs := guard_eq_some h
+          have hcond := guard_cond h
+          subst hs
+          by_cases huuid : uuid' = uuid
+          · subst huuid
+            simp only [Bool.and_eq_true] at hcond
+            obtain ⟨_, hpend⟩ := hcond
+            cases hp : s.peeks uuid' with
+            | pending => simp
+            | notSeen => rw [hp] at hpend; simp [PeekState.isPending] at hpend
+            | answered => simp
+          · simp only [] at hns
+            have hne : (uuid == uuid') = false := by
+              simp only [beq_eq_false_iff_ne, ne_eq]
+              exact fun heq => huuid heq.symm
+            simpa only [hne, if_false, Bool.false_eq_true] using hns
+      | _ =>
+          left
+          simp only [step] at h
+          have hs := guard_eq_some h
+          subst hs
+          exact hns
+
+theorem peeks_notSeen_of_run_from (es : List Event) (s0 s : ProtocolState) (h : run s0 es = some s)
+    (uuid : Uuid) (hns : s.peeks uuid ≠ .notSeen) :
+    s0.peeks uuid ≠ .notSeen ∨ ∃ target, .cmd (.peek uuid target) ∈ es := by
+  induction es generalizing s0 with
+  | nil => simp [run] at h; subst h; exact Or.inl hns
+  | cons e rest ih =>
+      unfold run at h
+      cases hstep : step s0 e with
+      | none => simp [hstep] at h
+      | some s1 =>
+          simp only [hstep] at h
+          rcases ih s1 h with h1 | ⟨target, hmem⟩
+          · rcases peeks_notSeen_of_step s0 s1 e uuid hstep h1 with h0 | ⟨target, heq⟩
+            · exact Or.inl h0
+            · exact Or.inr ⟨target, by rw [heq]; exact List.mem_cons_self⟩
+          · exact Or.inr ⟨target, List.mem_cons_of_mem e hmem⟩
+
+/-- Lifting `peeks_answered_monotone` across a whole execution. -/
+theorem peeks_answered_run (es : List Event) (s s' : ProtocolState) (uuid : Uuid)
+    (h : run s es = some s') : s.peeks uuid = .answered → s'.peeks uuid = .answered := by
+  induction es generalizing s with
+  | nil => intro ha; simp [run] at h; subst h; exact ha
+  | cons e rest ih =>
+      intro ha
+      unfold run at h
+      cases hstep0 : step s e with
+      | none => simp [hstep0] at h
+      | some sm =>
+          simp only [hstep0] at h
+          exact ih sm h (peeks_answered_monotone s sm e hstep0 uuid ha)
+
+/-- Theorem 6. Encodes response.rs:66-69: exactly one PeekResponse per
+Peek. Phrased as "a second PeekResponse for the same uuid, anywhere
+later in a well-formed execution, is impossible". See the design
+doc's "Target theorems" section for why this form captures
+uniqueness. -/
+theorem peek_response_unique (pre mid : List Event) (uuid : Uuid) (s1 s2 s3 s4 : ProtocolState)
+    (hpre : run initState pre = some s1)
+    (hstep1 : step s1 (.resp (.peekResponse uuid)) = some s2)
+    (hmid : run s2 mid = some s3)
+    (hstep2 : step s3 (.resp (.peekResponse uuid)) = some s4) : False := by
+  have h2 : s2.peeks uuid = .answered := (peekResponse_requires_pending s1 s2 uuid hstep1).2
+  have h3 : s3.peeks uuid = .answered := peeks_answered_run mid s2 s3 uuid hmid h2
+  have h4 : s3.peeks uuid = .pending := (peekResponse_requires_pending s3 s4 uuid hstep2).1
+  rw [h3] at h4
+  exact absurd h4 (by simp)
+
+/-- Theorem 6, provenance half: a `PeekResponse` is always preceded by
+a matching `Peek`. -/
+theorem peek_response_preceded_by_peek (pre : List Event) (uuid : Uuid) (s s' : ProtocolState)
+    (hpre : run initState pre = some s)
+    (hstep : step s (.resp (.peekResponse uuid)) = some s') :
+    ∃ target, .cmd (.peek uuid target) ∈ pre := by
+  have hp : s.peeks uuid = .pending := (peekResponse_requires_pending s s' uuid hstep).1
+  rcases peeks_notSeen_of_run_from pre initState s hpre uuid (by simp [hp]) with h0 | hex
+  · simp [initState] at h0
+  · exact hex
+
+end MzCompute

From d317a0b2efd4e86bfa5bf5aa3fd3405f8dac657e Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 11:55:39 +0200
Subject: [PATCH 14/15] lean: add reading-order doc and README for MzCompute

---
 doc/developer/semantics/README.md           | 36 +++++++++++++++++++
 doc/developer/semantics/compute-protocol.md | 38 +++++++++++++++++++++
 2 files changed, 74 insertions(+)
 create mode 100644 doc/developer/semantics/README.md
 create mode 100644 doc/developer/semantics/compute-protocol.md

diff --git a/doc/developer/semantics/README.md b/doc/developer/semantics/README.md
new file mode 100644
index 0000000000000..d136e618bc28b
--- /dev/null
+++ b/doc/developer/semantics/README.md
@@ -0,0 +1,36 @@
+# Lean 4 compute protocol semantics
+
+A mechanized model of Materialize's compute protocol control-plane
+contract: the staging handshake and per-command/per-response legality
+rules documented in `src/compute-client/src/protocol/{command,
+response}.rs`.
+
+Read `compute-protocol.md` first for the reading order and a
+cross-reference from doc-comment sentence to Lean theorem.
+
+This is Phase 1 of a three-phase plan (see
+`doc/developer/design/20260724_compute_protocol_semantics.md`): only
+staging and command/response legality are modeled here. Read-hold
+lifecycle against `AllowCompaction` and multi-replica/worker command
+sharing are later phases, not yet started.
+
+## Relationship to MaterializeInc/materialize#36614
+
+That (at time of writing, unmerged) PR builds a different Lean 4
+model in this same directory: `Mz`, covering scalar evaluation and
+collection semantics (the data plane), under Lean namespace `Mz`.
+This directory's `MzCompute` library covers the compute protocol (the
+control plane) instead, under its own namespace, and was bootstrapped
+independently (its own `Dockerfile`/`lakefile.toml`/CI script) because
+`doc/developer/semantics/` did not yet exist on this codebase's
+history when this work started. If #36614 lands, the two efforts
+reconcile into one `lakefile.toml` with two `lean_lib` targets sharing
+one Docker image. See that PR's design doc and this directory's for
+each library's own scope.
+
+## Build
+
+`ci/test/lean-semantics.sh` builds the `mz-lean-semantics` Docker
+image and runs `lake build` inside it. For one-shot probes (`lake env
+lean`, inspecting a `sorry`'s goal state, and similar), use
+`bin/in-image` once the image exists.
diff --git a/doc/developer/semantics/compute-protocol.md b/doc/developer/semantics/compute-protocol.md
new file mode 100644
index 0000000000000..4e22401360291
--- /dev/null
+++ b/doc/developer/semantics/compute-protocol.md
@@ -0,0 +1,38 @@
+# Compute protocol semantics: reading order and theorem cross-reference
+
+Phase 1 of `doc/developer/design/20260724_compute_protocol_semantics.md`:
+a Lean 4 model of the compute protocol's staging and command/response
+legality contract.
+
+## Reading order
+
+1. `MzCompute/Basic.lean`: identifiers, `Frontier`, and the small
+   enums (`Stage`, `PeekState`, `FrontierKind`) the model dispatches
+   on.
+2. `MzCompute/Event.lean`: the `ComputeCommand`/`ComputeResponse`/
+   `Event` mirror types.
+3. `MzCompute/State.lean`: `ProtocolState` and the `step` relation.
+   Start here to see how a `command.rs`/`response.rs` doc-comment
+   contract becomes a guard.
+4. `MzCompute/Run.lean`: folding `step` into an execution,
+   `WellFormed`, and two worked example traces (one legal, one not).
+5. `MzCompute/Staging.lean`, `Legality.lean`, `Frontiers.lean`,
+   `Peeks.lean`: the seven theorems, grouped by which part of the
+   protocol they cover.
+
+## Theorem cross-reference
+
+| Theorem | Module | Encodes |
+| --- | --- | --- |
+| `hello_first` / `create_instance_second` | `Staging.lean` | `protocol.rs:52-58` |
+| `create_before_reference` | `Staging.lean` | `command.rs:148-153,158-163,185-187,219-224`, `response.rs:52-54,106-107,120-121` |
+| `no_reference_after_drop` | `Legality.lean` | `command.rs:152-153,162-163` |
+| `create_dataflow_ids_fresh` | `Legality.lean` | `command.rs:107-108` |
+| `frontiers_monotone_and_terminal` | `Frontiers.lean` | `response.rs:37-51` |
+| `peek_response_unique` | `Peeks.lean` | `response.rs:66-69` |
+| `cancel_requires_peek` | `Peeks.lean` | `command.rs:248-250` |
+
+This table is the concrete form of the design doc's Success Criteria
+("a reader can go from a doc-comment sentence... to the Lean lemma
+that encodes it, and back"). Keep it in sync if a later phase adds or
+renames a theorem.

From fa8611d5308f2c9d439af37f385597a67f4a4447 Mon Sep 17 00:00:00 2001
From: Moritz Hoffmann <antiguru@gmail.com>
Date: Fri, 24 Jul 2026 12:07:43 +0200
Subject: [PATCH 15/15] lean: dedupe guard helpers into Basic.lean, silence
 unused-hpre warnings

guard_eq_some/guard_cond were private-and-duplicated across four/two
theorem modules; hoisted one shared copy into Basic.lean next to guard's
definition. Renamed two intentionally-unused hpre binders to _hpre.
Found by the final whole-branch review.
---
 doc/developer/semantics/MzCompute/Basic.lean  | 16 ++++++++++++++++
 .../semantics/MzCompute/Frontiers.lean        |  9 ---------
 .../semantics/MzCompute/Legality.lean         | 12 ++----------
 doc/developer/semantics/MzCompute/Peeks.lean  | 19 +------------------
 .../semantics/MzCompute/Staging.lean          | 16 ----------------
 5 files changed, 19 insertions(+), 53 deletions(-)

diff --git a/doc/developer/semantics/MzCompute/Basic.lean b/doc/developer/semantics/MzCompute/Basic.lean
index d2add4ae3ff11..6374c3cbd3fa5 100644
--- a/doc/developer/semantics/MzCompute/Basic.lean
+++ b/doc/developer/semantics/MzCompute/Basic.lean
@@ -86,6 +86,22 @@ recovery behavior the protocol does not specify. -/
 def guard (cond : Bool) (s : α) : Option α :=
   if cond then some s else none
 
+/-- A successful `guard` returns its payload unchanged. -/
+theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : x = y := by
+  unfold guard at h
+  cases cond with
+  | true => simpa using h
+  | false => simp at h
+
+/-- A successful `guard` witnesses its condition held. -/
+theorem guard_cond {α : Type _} {cond : Bool} {x y : α}
+    (h : guard cond x = some y) : cond = true := by
+  unfold guard at h
+  cases cond with
+  | true => rfl
+  | false => simp at h
+
 /-- Whether an optional new frontier report (`none` = this kind was
 not reported this time) is compatible with the previously reported
 value. `none` is always compatible: an absent field means "unchanged",
diff --git a/doc/developer/semantics/MzCompute/Frontiers.lean b/doc/developer/semantics/MzCompute/Frontiers.lean
index 2998e02bde2ca..baa7313493ba7 100644
--- a/doc/developer/semantics/MzCompute/Frontiers.lean
+++ b/doc/developer/semantics/MzCompute/Frontiers.lean
@@ -77,15 +77,6 @@ theorem frontiers_advance (s s' : ProtocolState) (id : GlobalId) (w i o : Option
     | output => simpa using (checkAdvance_advances o (s.reportedFrontiers id .output) ho)
   · contradiction
 
-/-- A successful `guard` returns its payload unchanged. Local copy of
-the helper `Legality.lean` uses. -/
-private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
-    (h : guard cond x = some y) : x = y := by
-  unfold guard at h
-  cases cond with
-  | true => simpa using h
-  | false => simp at h
-
 /-- Theorem 5, lifted across a whole execution. -/
 theorem reportedFrontiers_monotone (s0 s : ProtocolState) (es : List Event)
     (h : run s0 es = some s) (id : GlobalId) (k : FrontierKind) :
diff --git a/doc/developer/semantics/MzCompute/Legality.lean b/doc/developer/semantics/MzCompute/Legality.lean
index 61855b059f203..730de42d8a574 100644
--- a/doc/developer/semantics/MzCompute/Legality.lean
+++ b/doc/developer/semantics/MzCompute/Legality.lean
@@ -15,14 +15,6 @@ import MzCompute.Run
 
 namespace MzCompute
 
-/-- A successful `guard` returns its payload unchanged. -/
-private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
-    (h : guard cond x = some y) : x = y := by
-  unfold guard at h
-  cases cond with
-  | true => simpa using h
-  | false => simp at h
-
 /-- Theorem 3, part 1. Encodes command.rs:152-153. -/
 theorem schedule_fails_when_dropped (s : ProtocolState) (id : GlobalId) (h : s.dropped id = true) :
     step s (.cmd (.schedule id)) = none := by
@@ -70,13 +62,13 @@ no later `Schedule`, `AllowWrites`, or index-target `Peek` for `id`
 can succeed. -/
 theorem no_reference_after_drop (pre mid : List Event) (e : Event) (id uuid : Uuid)
     (s s' s'' : ProtocolState)
-    (hpre : run initState pre = some s)
+    (_hpre : run initState pre = some s)
     (hdrop : s.dropped id = true)
     (hmid : run s mid = some s')
     (he : e = .cmd (.schedule id) ∨ e = .cmd (.allowWrites id) ∨ e = .cmd (.peek uuid (.index id)))
     (hstep : step s' e = some s'') : False := by
   have hdrop' : s'.dropped id = true := by
-    clear hpre he hstep
+    clear _hpre he hstep
     induction mid generalizing s with
     | nil => simp [run] at hmid; subst hmid; exact hdrop
     | cons e0 rest ih =>
diff --git a/doc/developer/semantics/MzCompute/Peeks.lean b/doc/developer/semantics/MzCompute/Peeks.lean
index 4e3f8baf17dc1..fcd589032d5ef 100644
--- a/doc/developer/semantics/MzCompute/Peeks.lean
+++ b/doc/developer/semantics/MzCompute/Peeks.lean
@@ -15,23 +15,6 @@ import MzCompute.Run
 
 namespace MzCompute
 
-/-- A successful `guard` returns its payload unchanged. Local copy of
-the helper `Staging.lean`/`Frontiers.lean` use. -/
-private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
-    (h : guard cond x = some y) : x = y := by
-  unfold guard at h
-  cases cond with
-  | true => simpa using h
-  | false => simp at h
-
-/-- A successful `guard` witnesses its condition held. -/
-private theorem guard_cond {α : Type _} {cond : Bool} {x y : α}
-    (h : guard cond x = some y) : cond = true := by
-  unfold guard at h
-  cases cond with
-  | true => rfl
-  | false => simp at h
-
 theorem peekResponse_requires_pending (s s' : ProtocolState) (uuid : Uuid)
     (h : step s (.resp (.peekResponse uuid)) = some s') :
     s.peeks uuid = .pending ∧ s'.peeks uuid = .answered := by
@@ -208,7 +191,7 @@ later in a well-formed execution, is impossible". See the design
 doc's "Target theorems" section for why this form captures
 uniqueness. -/
 theorem peek_response_unique (pre mid : List Event) (uuid : Uuid) (s1 s2 s3 s4 : ProtocolState)
-    (hpre : run initState pre = some s1)
+    (_hpre : run initState pre = some s1)
     (hstep1 : step s1 (.resp (.peekResponse uuid)) = some s2)
     (hmid : run s2 mid = some s3)
     (hstep2 : step s3 (.resp (.peekResponse uuid)) = some s4) : False := by
diff --git a/doc/developer/semantics/MzCompute/Staging.lean b/doc/developer/semantics/MzCompute/Staging.lean
index ef25111020e6c..5261ba361dd1e 100644
--- a/doc/developer/semantics/MzCompute/Staging.lean
+++ b/doc/developer/semantics/MzCompute/Staging.lean
@@ -49,22 +49,6 @@ theorem create_instance_second (e1 e2 : Event) (rest : List Event) (s : Protocol
       | _ => simp [Event.isHello] at he1
   | resp _ => simp [Event.isHello] at he1
 
-/-- A successful `guard` returns its payload unchanged. -/
-private theorem guard_eq_some {α : Type _} {cond : Bool} {x y : α}
-    (h : guard cond x = some y) : x = y := by
-  unfold guard at h
-  cases cond with
-  | true => simpa using h
-  | false => simp at h
-
-/-- A successful `guard` witnesses its condition held. -/
-private theorem guard_cond {α : Type _} {cond : Bool} {x y : α}
-    (h : guard cond x = some y) : cond = true := by
-  unfold guard at h
-  cases cond with
-  | true => rfl
-  | false => simp at h
-
 /-- A single step either preserves `created` or, for a `CreateDataflow`
 event, adds exactly its export list. -/
 theorem created_of_step (s s' : ProtocolState) (e : Event) (h : step s e = some s') (id : GlobalId) :