Skip to content

docs: add invariants.md and engines.md - #975

Merged
aparajon merged 62 commits into
mainfrom
armand/invariants-doc
Sep 5, 2026
Merged

docs: add invariants.md and engines.md#975
aparajon merged 62 commits into
mainfrom
armand/invariants-doc

Conversation

@aparajon

@aparajon aparajon commented Aug 7, 2026

Copy link
Copy Markdown
Collaborator

Why this matters

SchemaBot's safety model is spread across check-runs.md, apply-lifecycle.md, code comments, and a long trail of merged PRs. An operator reasoning about a change during an incident, or a reviewer deciding whether a PR weakens a guarantee, has no single place that says what must never be false at runtime. Tier-0 services deserve that registry.

What it does

Adds docs/invariants.md: 71 runtime safety invariants in 9 families, covering availability and blast radius (AV), the merge gate (MG), the apply state machine (ST), ownership and leases (OW), control operations (CO), operator surfaces (UX), recovery (RC), review integrity and data safety (RV), and routing and authorization (AZ). Each states the rule, what breaks if it is violated, and where it is enforced. Every entry describes shipped behavior, not intent.

The doc opens by answering the two questions most readers have first: whether SchemaBot depends on GitHub (it does not, and a GitHub outage fails the merge gate closed rather than open), and what the control plane and data plane actually are, including that local mode collapses both into a single process.

Operator surfaces are part of the safety model

The UX family covers what an operator is shown while the system works, on the argument that a guarantee nobody can see is one nobody can act on, and that a surface reading plausibly while being wrong is worse than one that says nothing.

  • An operator's command shows its effect at the bottom of the PR. Rotation runs off a durable per-comment signal, so it survives a lease handover and fires at most once per phase, and it is gated on the command actually having been issued.
  • Acknowledgment means a deployment committed to acting, not that a packet arrived. An unacknowledged command is therefore a routing question rather than a lost one.
  • Progress is a projection. The lease-holding driver is the only engine poller; every other surface renders from stored rows and writes nothing, so a display problem stays a display problem and watching an apply never perturbs it.
  • A refusal says what to do next, bounded by the rule that guidance is written by SchemaBot rather than assembled out of an untrusted error string.
  • One severity vocabulary, one meaning per glyph, identical across surfaces, with lifecycle state kept as a separate vocabulary. A custom analyzer fails the build on a severity glyph written as a literal outside the package that owns it, which earns this entry a line in the structural-enforcement list.

AV-10 is the related new availability entry: every command a PR comment accepts has a CLI equivalent, because both surfaces converge on the same service methods and neither is privileged. It is what makes AV-1 worth having. A fallback path that covers most of the surface is not a fallback.

The README badges get a definition

MySQL: GA, Vitess: GA, and PostgreSQL: early alpha previously had no definition anywhere in the repo. They are claims about capability, so docs/engines.md is where they are defined: GA is an engine that can change a large table online and gives an operator a real lever over a change that is already in flight. Which verbs deliver that lever varies, so the bar is the ability rather than a fixed list.

They are deliberately not defined as "upholds every invariant in the registry". Most of the registry sits above the engine, and an engine cannot uphold or fail an entry it is not a participant in. invariants.md instead names the entries where the engine boundary actually lives, and keeps the part that does not move: an engine below GA is narrower, not looser. A change it cannot execute safely is blocked at plan time rather than routed to something less safe, and an operation it does not support is still recorded durably and still resolves to a typed terminal decline rather than a silent drop or a false success. That is the difference between an unfinished engine and an unsafe one.

Engine differences get their own doc

docs/engines.md is the capability matrix: how each engine executes a change, which control operations it supports, how it manages load, and how a dropped table is or is not recoverable, followed by why each difference follows from the execution model. Keeping it out of the registry is the point. The registry states what must never be false and is meant to be stable; what an engine can currently do moves as engines gain capabilities, so it lives in a document that is explicitly a description of the present rather than a contract.

What it does not promise

A guarantees-only safety document reads as marketing to a skeptic, so the doc states its own boundary: these invariants do not promise your schema change is correct, do not promise your database is unaffected while it runs, do not make changes reversible, and are not a security boundary against your own operators. Most importantly they do not promise liveness. Fail-closed spends workflow availability to buy correctness, which means SchemaBot will sometimes stop and wait for a human on purpose.

Using it

AGENTS.md gains a Runtime Invariants section so the registry is part of the workflow rather than a document: before changing safety-relevant code, find the entries that govern it, and cite them by ID in the PR summary and in review findings. "This preserves MG-5" is a reviewable claim; "this is safe" is not. A change then declares which of four is true: it upholds an invariant, extends its enforcement to a new engine or dialect, establishes a new one, or weakens one.

Weakening is allowed as a deliberate decision that gets stated. What the rule forbids is leaving an entry that describes behavior the code no longer has, because the registry is only worth consulting while it is true.

Corrections found while writing it

Auditing each entry against main turned up five that described behavior the code does not have. Worth reading as findings in their own right:

  • RV-5 claimed a dropped table is always held for a recovery window. The Spirit quarantine is opt-in and off by default, so on MySQL an unconfigured deployment executes the drop and the data is gone. The entry now separates the guarantee that always holds (a drop cannot run without explicit approval) from the recovery window, which is conditional.
  • OW-5 claimed one active apply per database, type, and environment. The unit of exclusion is the physical deployment, so two applies in the same environment with disjoint deployment sets may run concurrently.
  • ST-1 claimed start is the only way back into a stopped apply. A stopped apply is also claimable to deliver a pending cancel.
  • RC-5 claimed the terminal-summary claim can never be re-granted. It is re-armed when a summary is superseded, and a sentinel abandoned by a crashed publisher is recovered by its own stale-claim path.
  • AV-6 described a version-aware skip guard that does not exist. What makes version skew survivable is the additive-only gRPC and storage contracts; the HTTP API and config deliberately do the opposite and reject fields they do not recognize.

Opened by Claude (Opus 5).

Copilot AI lite review requested due to automatic review settings August 7, 2026 21:20

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Adds a new documentation registry, docs/invariants.md, intended to centralize SchemaBot’s runtime safety invariants so operators and reviewers have a single reference for “must never be false at runtime” guarantees.

Changes:

  • Introduces a comprehensive invariants registry (56 invariants across 8 categories) with rationale and enforcement pointers.
  • Adds a “Structural enforcement” section describing CI-enforced meta-invariants (state completeness, route-table sweep, engine conformance, claim parity).
Suppressed comments (1)

docs/invariants.md:607

  • This enforcement reference has the same malformed inline code formatting: backticks only wrap pkg/webhook and the parenthetical never closes cleanly on the first line, which breaks Markdown rendering.
*Enforced:* the durable webhook inbox (`pkg/webhook` durable dispatch,
`webhook_events` storage).

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread docs/invariants.md Outdated
@aparajon
aparajon force-pushed the armand/invariants-doc branch from 47165df to 7cd0a00 Compare August 7, 2026 21:29
aparajon and others added 2 commits September 3, 2026 10:54
Distills the safety properties that make SchemaBot safe for tier-0
databases into a single registry: merge gate, apply state machine,
ownership and leases, control operations, recovery, review integrity,
routing and authorization, and availability. Each invariant states the
rule, what breaks if it is violated, and where it is enforced.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Bring docs/invariants.md current with the safety work that has landed since
it was drafted, and give AGENTS.md a rule for using it.

Corrections: the accepted control operations list (drop the retired one, add
release), CO-6's example, RV-6 now states that the parser is resolved from the
target's dialect rather than defaulted, MG-5 states that the ownership refusal
is decided in-transaction rather than inferred from a row count, and AV-5
covers gRPC handlers.

New entries: MG-11 (a terminal outcome lands on the commit the PR is gated
on), CO-10 (a retired operation settles rather than wedging), and AV-9 (the
storage bootstrap converges additively or not at all).

AGENTS.md gains a Runtime Invariants section: find the entries a change
touches, cite them by ID, and declare whether the change upholds, extends,
establishes, or weakens each one. Weakening an invariant is allowed and must
be stated; leaving an entry that describes behavior the code no longer has is
not.
@aparajon
aparajon force-pushed the armand/invariants-doc branch from 7cd0a00 to 9560f35 Compare September 3, 2026 15:05
@aparajon
aparajon marked this pull request as ready for review September 3, 2026 15:18
aparajon and others added 3 commits September 3, 2026 11:32
Five entries described behavior the code does not have. Each was checked
against main rather than reasoned about:

- RV-5 claimed a dropped table is always held for a recovery window. The
  Spirit quarantine is opt-in and off by default, so on MySQL an unconfigured
  deployment executes the drop. The entry now separates the guarantee that
  always holds (consent: a drop cannot run unapproved) from the recovery
  window, which is conditional.
- OW-5 claimed one active apply per (database, type, environment). The unit
  of exclusion is the physical deployment; disjoint deployment sets in the
  same environment may run concurrently.
- ST-1 claimed start is the only re-entry to a stopped apply. A stopped apply
  is also claimable to deliver a pending cancel.
- RC-5 claimed the terminal-summary claim can never be re-granted. It is
  re-armed when a summary is superseded, and abandoned sentinels are
  recovered by their own stale-claim path.
- AV-6 described a version-aware skip guard that does not exist. What makes
  skew survivable is the additive-only gRPC and storage contracts, and the
  HTTP API and config deliberately do the opposite and reject unknown fields.

Readability: the doc now opens by answering whether SchemaBot depends on
GitHub, since that is the first thing most readers want to know, and the
availability family leads. Adds a section defining control plane and data
plane, including that local mode collapses both into one process, because
"remote data plane" was used throughout without definition. Em dashes are
gone from the prose and entry titles use a colon separator.
The registry read as though every engine and dialect carried identical
guarantees. Several entries are engine-conditional by design, and PostgreSQL
target support is early alpha with a narrow supported set, which is a
different thing from PostgreSQL as a dialect of SchemaBot's own storage.
…imits

The README engine badges (MySQL GA, Vitess GA, PostgreSQL early alpha) had no
definition anywhere. Tie them to the registry: GA means the engine upholds every
invariant, early alpha means it does not yet and the gaps are named. PostgreSQL's
gaps are the control family beyond CO-1/CO-2 and RV-5's recovery window; a control
request there is still durable and still resolves to a typed terminal decline.

Add a section on what these invariants deliberately do not promise, including that
fail-closed spends workflow availability to buy correctness.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

@morgo morgo left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🤖 Approving on Morgan's behalf (automated review).

Docs-only — AGENTS.md, README.md, docs/invariants.md, no code — and it's the document I've most wanted while reviewing this repo. Approving, with one entry I think is wrong and would fix before merge.

I reviewed this against the bar the PR sets for itself, since AGENTS.md is the half that will outlive the initial read: "Every entry describes shipped behavior, not intent" and "Do not add aspirational entries. If the behavior is not enforced in shipped code, it belongs in a design doc or a TODO." That's the right rule, and it makes the registry falsifiable, so I spot-checked entries against main rather than reading for plausibility.

Finding: AV-8 does not meet that bar, and the new head makes it load-bearing. The entry says raw error strings "are never rendered into PR or check markdown," and that the raw error "goes to server logs with triage identifiers." Against main:

  • Triage identifiers do not exist. newErrorReference / error_ref have zero occurrences in pkg/webhook on main. That mechanism is #768, which is still open — and which I'm currently holding on CI. The entry describes it as shipped.
  • PR markdown does render raw errors. plan.go passes err.Error() straight to postCommandError at lines 41, 81 and 247, and sets data.ErrorDetail = err.Error() at 622, 631 and 639. These are PR-comment paths. Engine execution errors are exactly what carries hostnames, DSN fragments and quoted failing statements.
  • This is not fully closed by #768 either. userFacingError there still ends in return err.Error() for plan-execution errors, deliberately — the engine's text is the actionable part. Sanitizing that is #1246's job, at the source. So AV-8 as written is ahead of both open PRs, not just one.

What is shipped is the check surface and the size bound, and both are real: sanitizeCheckRunErrorSummary in check_publisher.go, clampDriftSummary in plan_drift.go, and http.MaxBytesReader(w, r.Body, maxWebhookBodyBytes) in handler.go:766. So the accurate version of AV-8 today is narrower: check markdown is sanitized, inbound payloads are size-bounded, and the PR-comment path is being closed by #768 and #1246. Splitting the enforced half from the in-flight half would make the entry true now and let the follow-ups tighten it.

The reason I'd fix this before merge rather than after is the README change in this head. "GA means the engine upholds every runtime safety invariant in docs/invariants.md" is a good definition — it converts a vibe into a checklist — but it means an overstated entry is no longer a doc nit. AV-8 sits in AV, which is webhook-layer and engine-independent, so it applies to the engines this head declares GA. The definition is only as strong as the weakest entry, and it's worth protecting precisely because it's a better standard than most projects hold themselves to.

By contrast, the new GA section's own claims check out exactly. I went at the most specific one — that a PostgreSQL control request gets "a typed unsupported-operation decline rather than a silent drop, a false success, or an unbounded retry." All six named controls (stop, cancel, start, cutover, revert, skip-revert) return engine.NewUnsupportedOperationError in postgres.go:459-492, the doc's list of six matches the code's list of six with nothing omitted, and TestLifecycleControlsDeclineAsUnsupported asserts engine.IsUnsupportedOperation(err) across all of them. The distinction the section draws — unfinished engine versus unsafe one — is backed by the code it points at.

MG-11 I'd already verified from the other direction. It says a terminal outcome lands on the gating commit, and that matches current behavior including the WithPRInfo single-read refinement from #1254. That's an entry written after the code, which is what the whole registry should read like.

The "what these invariants do not promise" section is the most valuable page here, and I'd resist any pressure to soften it. Three parts in particular: that fail-closed spends liveness on purpose and will stop and wait for a human; that this is not a security boundary against your own operators; and that absence of an entry means unpinned rather than known-unsafe. That last one preempts the exact misreading a registry invites.

Nit: the invariant families are referred to by ID throughout (RV-3, CO-3, AZ-*) with no ID→file index. AGENTS.md says a PR weakening an invariant must update this document, which means the first job of a reviewer holding a diff is mapping changed files back to IDs. A short table, or *Enforced:* lines carrying paths rather than package names, would make that lookup mechanical.

Scope: I verified AV-8, MG-11, and the new GA section against main. I did not check the other ~40 entries individually.

CI is 18 in flight with zero real failures at 761e7412; the three FAILURE-shaped entries earlier in this PR's history were aggregate gate jobs from cancelled runs, not real failures. Docs-only, so nothing here can turn red on its own merits.

Not blocking.

aparajon and others added 5 commits September 3, 2026 11:52
…term

Reading top to bottom, the opening sections used apply, engine, data plane, and
merge gate before defining any of them. Introduce each at its first use: apply as
the unit everything else is about, engine as the thing SchemaBot drives rather than
is, data plane where the GitHub-credential separation is first claimed, and the
merge gate as the check that gates a PR.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…swap

The absent control operations are a consequence, not a peer, of the real gap:
PostgreSQL executes only native in-place DDL, so a change needing a copy or a
rewrite is blocked at plan time and there is never anything long-running to pause.
Also name the non-atomic multi-statement plan.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…tart, and cutover

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…gnment

The engine envelopes move faster than this document should. Keep the definition of
GA and early alpha here, let the README badges carry which engine is where, and let
each engine's own doc be the authority on its current boundary. What this section
states instead is the part that does not move: an engine below GA is narrower, not
looser, and behaves the same way at the edge of its envelope.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The entry said operator surfaces show a fixed sanitized line. Shipped behavior is
redaction in place: control and bidi characters stripped, connection details
redacted, length clamped, markup escaped, with the fixed line only as the fallback
when sanitizing empties the message. Name the table-cell flattening too, and say
where the guarantee lives, since it holds because the renderers apply it rather
than because each caller remembers to.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@aparajon

aparajon commented Sep 3, 2026

Copy link
Copy Markdown
Collaborator Author

🤖 Thanks for reviewing this against the bar the PR sets for itself rather than reading for plausibility. That's the right way to hold it, and it caught a real defect. Splitting the response by finding, because they didn't all land the same way.

On triage identifiers: you're right. newErrorReference and error_ref have zero occurrences on main. I checked before answering. The entry never named that mechanism, and the log line at plan.go:568 does carry repo, pr, environment, database, action, error next to the raw error, so the phrase was satisfied by shipped code as written. But it reads as a promise of correlation between a comment and a log line, and that promise is #768's. I've reworded so it claims only the identifiers that are actually on the log entry.

On PR markdown rendering raw errors: I don't think this one holds, and I'd rather say so than quietly narrow the entry. The call sites are as you describe, but they aren't the rendering boundary. Every one of them terminates in RenderGenericError, which does:

data.ErrorDetail = quoteBlockLines(html.EscapeString(sanitizeCommentError(data.ErrorDetail)))

sanitizeCommentError (templates/common.go:281) normalizes line endings, strips control and bidi-format characters, redacts connection details, trims, and clamps by rune count, with trimPartialRedactionMarker so truncation can't turn a redaction back into a partial leak. postCommandError reaches it via error_comment.go:34, and 622/631/639 each call RenderGenericError(data) on the next line.

The passthrough you'd be pointing at is userFacingErrorDetail, whose default arm is return errorDetail. That's real, but it runs before the renderer, so it isn't the last word on what reaches the comment.

Worth separating from #1246: sanitizing at the source is still worth doing, because redaction at the boundary is pattern-based and a source that never emits the endpoint is strictly better. But the PR-comment surface isn't currently unprotected, so I don't think AV-8 needs to wait on either PR.

There was a real defect in AV-8, and it's a different one. The entry said those surfaces "show a fixed sanitized line." They don't. They show the actual error, redacted in place; the fixed line is only the fallback when sanitizing empties the message. That was describing the AGENTS.md rule instead of the shipped behavior, which is exactly the failure the doc's contract is supposed to prevent. Fixed in 4f08c97, along with naming the table-cell flattening and stating that sanitizing is a property of the renderers rather than of each call site, since that's why it holds.

So AV-8 is narrower than it was, but on a different axis than you proposed. Narrowing it to the check surface alone would have understated what ships.

On the nit: agreed, and it's the most useful structural comment here. *Enforced:* lines carrying package names means mapping a diff back to invariant IDs is a manual step, which undercuts the AGENTS.md rule that depends on it. I'd rather do that as its own pass than inflate this one, since it touches every entry.

Two smaller notes: the GA section no longer pins which engine is at which level, so the six-control detail you verified has moved out of it and into docs/postgresql.md, which is the authority on a boundary that's moving quickly. And thanks for the note on the "do not promise" section; it was the last thing added and the part I was least sure would survive review.

Enforcement pointers named packages, so a reviewer holding a diff had to map
changed files back to invariant IDs by hand, which undercuts the AGENTS.md rule
that depends on that lookup. All 65 entries now name the files that enforce them.

Paths are verified against main and carry no line numbers, which would go stale
on the next edit. Package-level references remain only where enforcement really is
spread across a package rather than concentrated in a file.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@aparajon

aparajon commented Sep 3, 2026

Copy link
Copy Markdown
Collaborator Author

🤖 Follow-up on the nit: I said I'd do it as a separate pass, but it turned out small enough to land here. af6dc7f4 puts file paths on all 65 *Enforced:* lines, so mapping a diff back to invariant IDs is a grep rather than a reconstruction.

Two constraints worth naming, since they shaped the result:

  • No line numbers. They'd be stale on the next edit, and a pointer that's confidently wrong is worse than a vague one.
  • Package-level references survive where enforcement really is package-wide (pkg/engine, pkg/auth). Inventing a file to look precise would defeat the purpose.

The verification is the part I'd flag for anyone doing this kind of pass again. I checked all 69 referenced paths against main mechanically and got 0 missing, and two assertions were still wrong at that point:

  • RV-1 pointed at pkg/webhook/multi_apply.go for pre-apply change-set verification. That file has no change-set code. It's pkg/tern/change_set_compare.go, applied on the review-drift and rollup paths.
  • CO-10 pointed at sqlstore/applies.go for the retired-operation set. That grep hit was an unrelated comment about a retired DB session. It's RetiredControlOperations() in pkg/storage/types.go.

A path can exist and be the wrong file, so "does it exist" is not the check that matters; "does this file contain the mechanism the entry claims" is. Both were caught by content-grepping each file for its claimed mechanism and fixed before the commit. Which is the same failure mode as the AV-8 finding, one level down: the entry was plausible, verifiable, and wrong.

@morgo morgo left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🤖 Re-approving on Morgan's behalf after a head change (automated review).

First, a correction: my AV-8 finding on the previous head was wrong. I said the entry described unshipped behavior because plan.go passes err.Error() straight into postCommandError and sets data.ErrorDetail = err.Error(). I checked the call sites and stopped there. The sanitizing happens at the rendering boundary — errors.go:284 does quoteBlockLines(html.EscapeString(sanitizeCommentError(data.ErrorDetail))) — so those call sites are safe precisely because they don't have to be careful. That is the property the entry was claiming, and I tested it at the wrong layer.

The revised entry now says this explicitly ("Sanitizing is a property of the rendering boundary rather than of each call site, which is what makes it hold"), which is both the accurate statement and the one that would have stopped me making the mistake.

I verified the rewritten AV-8 clause by clause against main, and it holds:

  • control and bidi-format characters stripped — stripControlText drops unicode.IsControl and unicode.Is(unicode.Cf, ...) after removing ANSI escapes, keeping only \n and \t;
  • connection details redacted — redactConnectionDetails runs thirteen passes covering DSN fragments, URL userinfo, libpq password/parameters, MySQL and Postgres identity lines, host:port, and bare IPs;
  • length clamped by rune count, with maxCellErrorLen tighter than the comment-wide clamp;
  • escaped so it cannot inject markup — html.EscapeString plus quoteBlockLines keeping multi-line errors inside the blockquote;
  • table-cell text flattened to one line with | neutralized to /sanitizeCellError;
  • sanitizes-to-nothing handled — writeErrorBlock and writeTableErrorLine bail on empty, and multi_apply.go:166 emits the deployment name alone.

The dropped "triage identifiers" phrasing was the right cut. That mechanism is #768's newErrorReference, which has zero occurrences on main and is still open. The entry now says the unredacted error goes to the log "next to the repo, PR, environment, database, and command," which is what actually ships.

trimPartialRedactionMarker deserves a mention since it's the kind of detail that only exists if someone thought about the failure: clamping a message could otherwise cut [endpoint redacted] down to [endp, turning a successful redaction into something that reads like a partially leaked value. Worth having an entry that implies it.

All 65 file paths the document now cites exist on main — I checked every one, zero missing. That closes the lookup nit I raised last head, and it closes it in the form that's actually verifiable: a wrong path would be worse than no path, and a path list is something CI could eventually assert.

The maturity section is structurally better than what I approved. Enumerating PostgreSQL's missing controls inline was a list guaranteed to drift, inside the document that defines GA. Deferring to postgresql.md as the authority on a moving envelope — and separating the definition of the badges (here, stable) from the assignment (README, moves) — removes the drift risk rather than restating it more carefully. "Narrower, not looser" is the right frame, and the CO-1/CO-2 point behind it still checks out: all six PostgreSQL lifecycle controls return engine.NewUnsupportedOperationError, with TestLifecycleControlsDeclineAsUnsupported asserting it.

Nit: AV-8 says a message that sanitizes to nothing "falls back to a fixed line rather than publishing an empty summary." Two of the three helpers write nothing rather than a fixed line; only the multi-apply path emits a line. Both are the safe behavior and neither publishes an empty summary, so this is wording, not substance.

CI is now fully green at af6dc7f4 — zero failures, nothing in flight, mergeStateStatus: CLEAN.

Not blocking.

A Check Run summary falls back to a fixed line because the Check Run has to carry
one; a comment omits the error block instead. Neither publishes an empty summary,
which is the invariant, but they are two behaviors and the entry claimed one.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@aparajon

aparajon commented Sep 3, 2026

Copy link
Copy Markdown
Collaborator Author

🤖 Appreciate the correction, and more so the fact that you named the layer you tested at. That's the part that makes it reusable: the entry was claiming a property of the rendering boundary, and checking the call sites is exactly the test that would pass or fail for the wrong reason. It's the same shape as the two bad paths I hit on the *Enforced:* pass — plausible, verifiable, and wrong, because the check was one level away from the claim.

The nit is right, and it was one behavior described where there are two. sanitizeCheckRunErrorSummary falls back to planFailedCheckText; writeErrorBlock and writeTableErrorLine both return on empty and write nothing. Fixed in 6239688f, which now names both and the reason they differ: a Check Run has to carry some summary, so it needs a fallback, while a comment can just omit the block rather than render an empty quote.

Agreed on trimPartialRedactionMarker. I left it out to keep the entry from turning into a catalogue, but you're right that it's load-bearing in a way the others aren't: every other pass fails safe if it does nothing, whereas clamping without it actively converts a successful redaction into something that reads like a leak. The entry implies it now; if it earns explicit mention later it'd be as its own line about redaction surviving truncation, not as another item in the list.

On CI asserting the path list: worth doing, and it's the natural next step now that every entry carries one. A test that parses the backticked paths out of invariants.md and fails when one doesn't exist would have caught nothing I shipped, though. Both of my wrong paths pointed at files that exist. The check that would have caught them is harder to automate, and I don't have a good mechanical form for it yet.

@aparajon aparajon changed the title docs: add invariants.md, the runtime safety invariant registry docs: add invariants.md and engines.md Sep 4, 2026
@Kiran01bm

Copy link
Copy Markdown
Collaborator

🤖 Review findings - created by Kiran's code review agent - for schemabot/pull/975, 1a10a99.

Verdict: 8 findings — 3 blocking (one claim not enforced in CI, two stated absolutes the code contradicts), 4 non-blocking, 1 suggestion. The registry is a genuinely good artifact; every finding below is drift, not disagreement with the idea.

Blocking

  1. UX-5 and the structural-enforcement list both claim the severity-glyph analyzer runs in CI. It does not. invariants.md:1213 and :1004 say a custom analyzer "runs in CI and in the pre-commit hook". severityglyphs appears zero times in .github/, the Makefile, and .golangci.yaml; Makefile:139 is lint: check-closeandlog check-webhookheaders with no check-severityglyphs target, and its only invocation is scripts/lint-fix.sh:237 via the opt-in pre-commit hook. A --no-verify commit, or a contributor who never ran make setup, lands a literal glyph on a green build — and "anywhere outside its home package" is also overstated, since the hook checks staged packages only and skips test files. Either wire it into lint.yaml or say "pre-commit hook".

  2. One code path falsifies three absolutes: UX-3, OW-2, and ST-4. progress_handlers.go:1244s.storage.Tasks().Update(ctx, task) — runs inside syncTasksFromTern, reached from the genuinely-GET route at service.go:812. That single write contradicts UX-3's "nothing that reads progress writes", OW-2's "apply and task updates … all carry the lease token" (an API request context never gets one, so the storage lease predicate is empty), and ST-4's "a stale engine poll can never rewind stored task state" (it assigns task.State raw, skipping taskStateWithNoBackwardProgress, and stopped/failed_retryable are not in IsTerminalTaskState). Correctly scoped it is gRPC-data-plane only, and apply headline state still comes from storage — so no safety hole, but three entries state absolutes this path breaks.

  3. MG-5's "never" is contradicted by the code's own interface doc. invariants.md:475 says a plan result never overwrites an in_progress row carrying an apply_id, but storage.go:162 enumerates three release paths including "the explicit same-head no-op recovery path (RecoverApplyOwnedCheckWithNoOpPlan)", which sets apply_id = NULL on exactly those rows. Nothing in docs/ mentions the exception. Two sub-claims are also wrong: the recovery path uses the "row count" shape MG-5 says is never used (return rows > 0, no transaction, no FOR UPDATE), and MarkActionRequiredForApply explicitly does not require ownership (AND (apply_id IS NULL OR apply_id <= ?)).

Non-blocking

  1. Eleven *Enforced:* pointers resolve cleanly to the wrong file. ST-4 names pkg/tern/observer.go, which is 147 lines of interface declaration (the logic is taskStateWithNoBackwardProgress, local_client.go:3330); ST-9 names sqlstore/retry.go, which is DB lock-conflict backoff, not the apply retry budget; RV-1 names the review-time comparison instead of pkg/tern/local_plan_drift.go; RV-2 names plan_freshness.go instead of schema_freshness.go; likewise MG-3, MG-7, MG-8, ST-1, OW-6, RC-2, RC-5. This is the most consequential systemic issue here: two of my own finder agents concluded RV-1 and RV-2 were false invariants purely because the pointer sent them to the wrong mechanism. A registry whose value is "cite it by ID" needs pointers that survive a reader following them.

  2. engines.md states two engine capabilities the code contradicts. engines.md:269 says CREATE INDEX CONCURRENTLY and NOT VALID + validate "run whatever the table size", but blockOversizedTable (postgres.go:298, called unconditionally) blocks every executable step on a *SizeError, and apply.go:402 runs preflight.CheckTable before the concurrent-index branch at :420. engines.md:367 says SchemaBot "reads the resulting throttle state and reports it" for Vitess, but TableProgress.Throttled is set in exactly one place repo-wide — spirit.go:992 — and vitessMigrationRow has no throttle fields at all. The second arrived in this PR's final commit.

  3. RC-2 contradicts RC-1 six lines earlier. RC-2 says "no claim, reaper, or recovery path touches an apply whose verdict is recorded"; RC-1 approvingly describes a reaper that marks stranded operation rows "only once the parent is settled". The code agrees with RC-1 — strandedParentGate (apply_operations.go:1850) gates on a.state IN (settled) as an inclusion, then writes. Startup summary reconciliation (handler.go:693) likewise writes new apply_comments rows for terminal applies.

  4. RC-5's "exactly once" is at-least-once with a bounded duplicate, and the code says so. comment_observer.go:1643 — "reconciliation will reclaim it and may post one duplicate — the bounded-duplicate contract for a lost tracking write" — and handler.go:721 repeats it. If CreateIssueComment succeeds but the follow-up Upsert fails, the sentinel goes stale and the reconciler posts a second summary. The corrected entry addresses re-arm and stale-claim but never states the actual contract.

  5. Three entries overstate a rule that holds in narrower form. OW-6's "exactly one claim query" is false at the operation level — FindNextApplyOperation and FindNextApplyOperationCutover are two queries with different eligibility gates, and apply_operations.go:1468 says "Both claim queries draw from the same driver pool"; the entry even illustrates itself with waiting_for_cutover → cutting_over, owned solely by the query it says doesn't exist. ST-1's "Storage refuses any write that would move a terminal apply back to an active state" names a guard that isn't there (applies.go:1073 is WHERE id = ? plus an optional lease predicate) — the invariant holds via the claim query's state arms and the API layer instead. ST-3's "never written directly by a drive" is true only for an operation-lease-only context, per its own code comment.

General suggestions

  1. AGENTS.md's new family list enumerates eight families and omits UX — the one a PR-comment or rendering change is most likely to touch, and the family owning the analyzer in finding 1. It also mandates a *Breaks if violated:* format that 8 of ~71 entries actually use. Minor: make docs-toc isn't enforced anywhere, so both new TOCs can drift silently; and spirit_progress.md:309 omits SkippingRevert from the yellow-bar states (the renderer emits five, the doc lists four).

The one thing that could have broken, verified

Whether the two most safety-critical entries — RV-1 (apply-time re-derivation of a plan reviewed elsewhere) and RV-2 (plan freshness) — describe mechanisms that exist. I nearly reported both as false: CompareChangeSets really does have one production caller and it really is review-time, and plan_freshness.go really does fail open in three places. Both survived. RV-1 is enforced by verifyMaterializedPlanMatchesLiveSchema (local_plan_drift.go:51), reached from materializeApplyRequestPlan on the Apply path, fail-closed on unparseable DDL. RV-2 is enforced by assertBaseSchemaStillCurrent (schema_freshness.go:78), which compares Git tree OIDs, stops on GitHub read uncertainty, takes no allowUnsafe, and is wired to both apply entry points (apply_handlers.go:255 and :733). The rules hold; only their pointers are wrong.

Verified correct

  • AV-1: deploy/local/config/grpc-tern.yaml carries no GitHub credentials; the gate publishes nothing on an unverifiable head rather than passing.
  • AV-10: all 15 comment commands enumerated against pkg/cmd/main.go — every one has a CLI counterpart.
  • ST-7 was investigated and refuted as a finding: a Vitess stop is refused at local_control.go:474, ~70 lines before the cancelled branch, and CO-8 already documents the legacy-row settlement case.
  • CO-8 was likewise investigated and dropped: the PostgreSQL gap is real but the safety property is intact (resolveFailedEngineStop terminalizes without touching the change) and nothing is made permanent.
  • Structural enforcement, 5 of 6 bullets: state-completeness, route-authorization sweep, engine conformance, claim parity, and cross-dialect parity tests all exist and do what the doc says.
  • Capability matrix spot-checked cell by cell: pg-sprite's six control ops all return typed NewUnsupportedOperationError; only PlanetScale implements ProgressIsExternallyAuthoritative; direct execution is MySQL-only by construction.
  • OW-3's two deadlines really are one constant (ApplyLeaseStaleAfter); OW-4 stops only on a proven ErrApplyLeaseLost.
  • All 100 internal anchors and cross-file links in both new docs resolve, and every backticked repo path exists.

This review was generated by Claude Code (claude-opus-5).

The exemption written into UX-3, OW-2 and ST-4 claimed the reconciliation
runs only against a settled apply. It does not: the storage-served read
path also admits resuming, which a driver writes as it claims the row, so
the write can land without a lease token and without the forward-only
guard while a driver is live. State the gap instead of the justification.

Also name what MG-5's recovery path does not check.

@morgo morgo left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🤖 Re-approving on Morgan's behalf after a head change (automated review).

42 commits since 75ec71e4+582/-133 in invariants.md, +364/-69 in engines.md. CI is clean at 661e39f0 (zero failures, nothing in flight, mergeStateStatus: CLEAN) and all 67 code paths cited across the two files still resolve.

Several commits explicitly retract earlier claims, including 86a40ee2 docs: correct entries the review found describing behavior the code does not have. Corrections are where a doc is most likely to overshoot in the other direction, so I spent this pass on the row that changed rather than re-reading the parts I'd already checked.

The corrected PlanetScale stop row holds, and it holds at a layer that grepping the engine would get wrong. The matrix now says stop is not available on PlanetScale and the prose claims the stop is refused — that SchemaBot "will not quietly carry out the stop as a cancel." Read the engine and that looks flatly contradicted:

// Stop preserves the legacy deploy-request cancel behavior until callers move
// to Cancel.
func (e *Engine) Stop(...) { return e.cancelDeployRequest(ctx, engine.ControlStop, req) }

The method does exactly the thing the doc says doesn't happen. But the refusal is upstream of it: executeStopForApply rejects storage.EnginePlanetScale with a 400 before queueStopForApplyOwner, so no durable intent is recorded and the engine method is never reached from an operator stop. The message is "stop is not supported for this schema change; use cancel to permanently cancel it" — it names cancel and says permanent, which is the claim the prose makes, and the operation is metered as rejected. handlers_test.go pins it as "rejects planetscale stop before queuing durable intent." The doc is right and the engine method is a leftover behind a closed door.

The two-shapes paragraph is the strongest thing added here and it survives the same check. "Refused on the spot and nothing durable is recorded" is the API gate above; "the engine is the one that declines, the request was already recorded durably" is the typed NewUnsupportedOperationError path, which PostgreSQL uses for all six controls and which local_control.go resolves terminally via IsUnsupportedOperation at :1499 and :1551. Two genuinely different mechanisms, described in the order an operator meets them, without pretending they're one.

My earlier nit is addressed — the legend now defines plain no ("does not do this today") alongside planned, so the cells are no longer read-by-inference.

Finding: the stop / start cell is correct for stop and wrong for start. Combining both operations into one row and marking it no says, per the legend just below it, that PlanetScale does not do start today. It does. The page's own prose says so two paragraphs later — "on the PlanetScale engine it exists only to launch a deploy request that was created and deliberately left undeployed" — and the code agrees:

  • executeStartForApply has no PlanetScale gate, unlike the stop path at control_handlers.go:734.
  • validateStartRequestState carries a dedicated GetOptions().DeferDeploy branch requiring WaitingForDeploy, which only exists because starting a deferred deploy is a real path.
  • It reaches startDeferredDeploy in local_control_resume.go from the control-request path, and the engine's Start returns Accepted: true whenever meta.DeferredDeploy is set.

So a reader who trusts the matrix concludes they cannot start a deferred PlanetScale deploy, when start is precisely how one begins. Splitting the row, or writing the cell as "stop: no / start: deferred deploys only," would match what the prose already says correctly. This is the one place where the matrix and the surrounding text disagree, and the matrix is the part people will read.

Unchanged from my last pass and still out of scope for a docs PR: Spirit's Revert / SkipRevert return a bare fmt.Errorf rather than engine.NewUnsupportedOperationError, so IsTerminalControlError classifies a permanently unsupported operation as retryable. The matrix's "no" for that row is accurate about the capability; the code's classification of the refusal is the part worth an issue.

Docs-only, CI clean, citations verified. Not blocking.

… upholds it

The read-path task reconciliation the registry carried an exemption for is
gone: progress reads report task rows as stored and write nothing. Remove the
exemption from UX-3, OW-2 and ST-4, which described a write that no longer
exists.

Add OW-8 for the rule that replaces it, and state why it is worth an entry: a
writer outside the lease system does not weaken "stored state is what the
lease-holder wrote" so much as make it uncheckable.

Correct RC-2's account of why the reaper waits. A settled parent is not on its
own a promise that its children stopped, because a rollout can settle on one
deployment's failure while a sibling drives under an apply row it may not bump.
The window that matters is over the row a live drive writes, and it is sized to
the operator's whole recovery budget.
@aparajon

aparajon commented Sep 5, 2026

Copy link
Copy Markdown
Collaborator Author

🤖 Addressing @Kiran01bm's 8-finding review. All nine items are resolved except one, called out below. Re-verified against current main, not against the tree you reviewed: 17 commits landed since 1a10a998, including the one that changes finding 2 from a doc problem into a code fix.

# Finding Status
1 severityglyphs claimed to run in CI Fixed in 86a40ee2 — both sites now say "a custom analyzer run by the pre-commit hook", and the "anywhere outside its home package" overstatement is gone with it
2 One code path falsifies UX-3, OW-2, ST-4 Fixed in the code, not the doc. See below
3 MG-5's "never" Fixed in 86a40ee2 — the entry now names the same-head no-op recovery path, and both sub-claims are corrected
4 Eleven *Enforced:* pointers resolve to the wrong file Fixed in 86a40ee2
5 engines.md states two capabilities the code contradicts Fixed in 86a40ee2
6 RC-2 contradicts RC-1 Fixed in 86a40ee2 — RC-2 now reads "No claim or recovery path reopens…" and describes the reaper as a precondition rather than a counterexample
7 RC-5's "exactly once" Fixed in 86a40ee2 — now "The contract is at-least-once with a bounded duplicate"
8 OW-6, ST-1, ST-3 overstate Fixed in 86a40ee2 — each now carries its narrower form
9 AGENTS.md omits UX; format mandate; docs-toc; spirit_progress Three of four fixed. docs-toc enforcement is still open

Finding 2 was the one worth having. You scoped it correctly: gRPC-data-plane only, headline state still from storage, no safety hole. But the entries were not the thing that was wrong. The write was. #1283 removed it (merged as 8520115b), and the read path now reports stored task state verbatim.

Two things fell out of fixing it that are worth recording, because both contradict what I would have written if I had only repaired the prose:

  • The obvious repair was to clamp the display so a settled apply never renders a task as active. That is unsafe. A settled parent is not a promise its children stopped: under a fan-out rollout one failed deployment settles the apply while its siblings keep copying, so the clamp would have hidden live work. Stored state is reported as stored.
  • Repairing the genuinely stranded rows is a write, so it belongs to a writer that can hold a lease. That is now the reaper, and the rule you exposed is written down as OW-8: only drivers and elected reapers write apply and task rows (01ad99ad), with UX-3, OW-2, and ST-4 rewritten to derive from it rather than each carrying an exception.

On finding 4, which I agree was the most consequential. Two of your finder agents concluding RV-1 and RV-2 were false invariants purely because the pointer misdirected them is exactly the failure mode that makes a registry worth less than nothing. Beyond the eleven, I now validate the pointers mechanically: all 70 file paths cited across the two files resolve, checked again after the 17-commit sweep. That catches the dangling kind. The resolves-cleanly-to-the-wrong-file kind still needs a reader, which is why AGENTS.md now spells out that a pointer can be wrong in two ways and only one is obvious.

What is still open: make docs-toc is not enforced anywhere, so both TOCs can still drift silently. You are right, and I am deliberately not fixing it here. It needs a check-docs-toc target and a CI step, which makes a docs-only PR touch the build right before merge. Better as its own change.

Two smaller notes on finding 9: the UX family is in the AGENTS.md list now, and spirit_progress.md:309 lists all five yellow-bar states including skipping revert. On the format mandate, you were right that it described something 8 of 72 entries do. Rather than retrofit 64 entries, 1af25f30 changes the mandate to match the practice: rule and Enforced: always, Breaks if violated: where the consequence is not obvious.

@aparajon

aparajon commented Sep 5, 2026

Copy link
Copy Markdown
Collaborator Author

🤖 Addressing @morgo's review.

The stop / start finding is correct and is fixed in a7b0dff8. I verified all three of your code claims before changing anything:

  • executeStartForApply has no PlanetScale gate, unlike the stop path at control_handlers.go:734.
  • validateStartRequestState carries the GetOptions().DeferDeploy branch requiring WaitingForDeploy.
  • TestStart_AcceptsDeferredDeploy pins the engine returning Accepted: true for a deferred deploy.

So the matrix said a reader cannot do the one thing that is precisely how a deferred PlanetScale deploy begins, while the prose fourteen lines later said the opposite. I split the row rather than qualifying the combined cell, since one capability per row is what the rest of the matrix does:

Spirit (MySQL) PlanetScale (Vitess) pg-sprite (PostgreSQL)
stop yes no planned
start yes deferred deploys only planned

Your point about which half people read is the reason this was worth catching rather than leaving to the prose: a combined row forces the stricter answer onto both operations, and the matrix is the part that gets skimmed.

On Spirit's Revert / SkipRevert returning a bare fmt.Errorf so IsTerminalControlError classifies a permanently unsupported operation as retryable: agreed it is real and agreed it stays out of a docs PR. The matrix cell is accurate about the capability, which is all this page claims. Flagging it to Armand rather than filing anything myself.

@aparajon
aparajon merged commit 92ed18e into main Sep 5, 2026
38 checks passed
@aparajon
aparajon deleted the armand/invariants-doc branch September 5, 2026 02:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants