docs(corpus): add the invariant template node - #1549
Conversation
Create launchpad/docs/corpus/templates/invariant.md so a future author has a schema-valid shape, evidence expectations and an adapted Design-by-Contract model to write a corpus node documenting one system invariant, distinct from the normative-language standard (#1320) and the not-yet-written policy template (#1344). Closes #1343 Signed-off-by: Serina Mcfall <serina.mcfall@gmail.com>
tucktuck101
left a comment
tucktuck101
left a comment
There was a problem hiding this comment.
Review — invariant template node
Strong template — the Design-by-Contract grounding (Meyer, Eiffel) checks out, the five
enforcement tiers are a genuinely useful frame, and letting an instance pick type by subject
matter rather than fixing one is the right call. But the flagship worked example inverts the
tier it exists to illustrate.
High — the thread.rs example files a transaction-enforced invariant under "convention only", and its cited functions are dead code
The FACT entry claims buzz-db's thread.rs "implements that gotcha as two functions,
increment_reply_count and decrement_reply_count ... nothing in the type system stops a
future call site ... from skipping these functions — the invariant holds only if every such
call site actually calls them", citing thread.rs:250-287 and :289-327.
Verified in launchpad:
thread.rs:250is#[allow(dead_code)], and its doc comment at:246-249reads: "NOTE:
The primary increment path is inlined inside [insert_thread_metadata]'s transaction. This
standalone version exists for future use cases..." — no insert path calls it.- The live path is
insert_thread_metadata, whose doc at:112-114reads: "The INSERT and all
counter UPDATEs are wrapped in a single transaction so a crash between them cannot leave
reply_count / descendant_count inconsistent with the actual number of reply rows (F9)." I
confirmedpool.begin()at:129andtx.commit()at:236, with both counter UPDATEs on
the same&mut *tx.
Two consequences. Required section 3 says "Naming the weakest true tier is the point of this
section" — yet the example files thread.rs under "nothing but the discipline of every caller
remembering to call the right function" when the live path is transactionally enforced and the
cited functions are unreachable. And the DbC illustration at :182-184 ("momentarily
inconsistent between the two UPDATE statements") holds only for the two dead-code functions,
which take &PgPool and issue independent execute(pool) calls; in the live path both UPDATEs
sit in one transaction precisely so that intermediate state is never observable.
This also trips the template's own rule at :337-343: an enforcement claim is a FACT "only if
the cited source actually enforces the invariant, not merely mentions it."
Re-cite thread.rs:112-114 and reclassify as transaction-enforced within one path plus
convention-and-review across future call sites, and re-ground the point-2 illustration.
Medium — the boundary against the test-contract template is unnamed
See my review on #1540 for the full analysis and the ownership ruling. Short form: your
flagship example ("kind 40002 replies must bump reply_count") is exactly the case
test-contract.md:132 also claims, and neither Boundary section mentions the other template.
One bullet each; both PRs are in this wave.
Low — an INFERENCE names the wrong file as its premise
The closing INFERENCE says "AGENTS.md's actual text states it as a property of which
CommunityId values can come to exist". Grepping the root AGENTS.md for
resolved from the connection host, never supplied, client-supplied community and
the fence returns nothing. The text described is crates/buzz-core/src/tenant.rs's module
doc — which is what the entry's own evidence array cites, and which the body attributes
correctly at :239-242. Reasoning, confidence and citation are all sound; only the prose names
the wrong file. It matters because this entry is the template's central
invariant-versus-policy discriminator.
Low — the skeleton omits frontmatter
:292-297 opens the fenced skeleton at # [Invariant name]: invariant with no --- block,
while both siblings in this wave ship a complete copyable one. That asymmetry bites hardest
here, because this is the one template that deliberately does not fix a single instance type
— so the author gets variable type guidance and no worked example of the field it applies to.
Not findings, ruled out on evidence
- The
launchpad/plans/file: 19 established siblings with the identical per-issue shape,
and the content matches this PR. Consistent with repo practice, not a roadmap-file violation. - Index registration: the corpus
AGENTS.mdforbids a hand-authored node index. - CI green at head (latest run per check); node validates clean.
Reviewed by tucktuck101's review lane. Every failing claim reported above was reproduced by me against this PR head before posting.
2 participants
Summary
Adds
launchpad/docs/corpus/templates/invariant.md, a corpus template node telling a future author how to document one Buzz system invariant: required sections, evidence expectations (FACT only when a source actually enforces the claim, not merely mentions it), and Design by Contract (Bertrand Meyer / Eiffel) as the industry model adapted rather than adopted wholesale. States an explicit boundary against#1320's normative-language standard (a rule about corpus prose wording, not system behavior) and the not-yet-written policy template#1344(what participants must do, vs. what always holds).Related issue
Closes #1343
Issue type
Task
Agent provenance
Objective
A single corpus node,
corpus-template-invariant, that governs the shape, evidence expectations and adapted industry model for any future corpus node documenting one Buzz system invariant.Impacted components
launchpad/docs/corpus/templates/invariant.md(new file)launchpad/plans/2026-08-27-issue-1343-corpus-template-invariant.md(new file, the plan this PR was built from)Approach and rejected alternatives
Adopted Bertrand Meyer's Design by Contract vocabulary (class invariant / precondition / postcondition) as the template's industry model, per the batch brief's own steer, but adapted rather than adopted it wholesale: Meyer's invariant is checked automatically by the Eiffel runtime on every routine boundary, and this repository has no such uniform mechanism. The six repo-native invariants surveyed while drafting (
crates/buzz-core/src/tenant.rs,crates/buzz-db/src/thread.rs,crates/buzz-audit/src/hash.rs,crates/buzz-relay/src/state.rs,crates/buzz-db/src/push.rs,crates/buzz-acp/src/pool.rs) are each held by a different mechanism (type system, structural code design, a unit test, a SQL predicate, an ordering convention, or nothing but caller discipline), so the template's "Enforcement today" required section asks an author to name the weakest true tier honestly, rather than implying Eiffel-style automatic checking that does not exist here.Considered citing Meyer's original 1992 IEEE Computer paper ("Applying Design by Contract") directly, since it is the usual primary reference the batch brief pointed at. Rejected as impossible in this environment: no
pdftotext/poppler-utils, no importablepypdf/PyPDF2, and automated web-fetch summarization of the PDF returned only a binary-content notice rather than extracted text (three separate attempts, two different PDF mirrors). Used Meyer's own ETH Zurich-hosted HTML page and Eiffel Software's own definitional page instead — both fetched and read directly, and both primary in the sense of being Meyer's/his company's own words — and recorded the paper-text gap explicitly in the node's "Expected but not verified" section rather than silently citing the PDF as read.Considered whether
referencesshould run from the invariant node toward an interface node it underpins. Drafted it that way first, then an independentreview-codepass (below) caught that this contradicted the template's own "Boundary" section, which frames an invariant as "the deeper claim an interface's contract can point at" — i.e. the interface should be thereferencessource, not the invariant. Fixed by reversing the Relationships section's guidance and the template skeleton to match, and re-validated.Verification
Command run:
Raw output:
Command run:
Raw output:
Not verified
pdftotext/poppler-utilsabsent,pypdf/PyPDF2not importable,pip3unavailable to install one), and automated web-fetch summarization of two different PDF mirrors returned only binary-content notices, not extracted text. The node cites Meyer's own ETH Zurich-hosted HTML page and Eiffel Software's own definitional page instead (both fetched and read directly this session) and records this gap explicitly in its own "Expected but not verified" section.validate.pyend to end.tenant.rs's fence, which affectsbuzz-db,buzz-auth,buzz-pubsub,buzz-search,buzz-auditandbuzz-media) should be one corpus node or split per-layer underAGENTS.md's "one node is one independently maintainable idea" rule is not settled by this template.implementsorreferencesis the corpus-wide convention for a node's optional self-link back to its own template remains unsettled, matching the same open question the sibling interface template (#1342, PR task: define the interface corpus template #1541) already noted for itself.Security implications
None. This is a new Markdown documentation file under
launchpad/docs/corpus/templates/; it adds no code path, no dependency, and no runtime behavior.Escalations
None. Two findings surfaced during review (see Approach section and pipeline note below) were both in-scope defects in this same artefact and were fixed directly, not deferred: (1)
review-codefound the Relationships section declaring the invariant→interfacereferencesedge in the opposite direction from the Boundary section's own stated reasoning — fixed by reversing the guidance and the skeleton to have the interface node declare the edge instead. (2) The same pass flagged the sole INFERENCE's confidence value (0.8) as better justified at 0.6 undercorpus-standard-confidence.md's own rubric, since one premise in the reasoning ("the ordinary meaning of 'policy'") is supplied by the author rather than cited — fixed. Both were re-validated after the fix (validate.pyexit 0, schema tests 27/27). Searched for duplicate escalation issues per the batch brief; none applied since nothing here needed escalating.Pipeline note. Followed plan-issue → review-plan → build-change → review-code → review-adjudicate → cross-model-substitute final pass, per the batch brief. Codex (the usual cross-model check) is down per issue #1467, so the final pass was a same-model adversarial self-review reading the finished node cold against parent PRD #605's acceptance sentence and against its own Boundary claims, in addition to the independent
review-codesubagent pass.review-testswas skipped as N/A: this issue adds no test code, only a documentation node validated by the existing schema tests.