From d384ddcae01e881e658ffb3f162f5eac2ff852d1 Mon Sep 17 00:00:00 2001 From: choiyounggi <74581798+choiyounggi@users.noreply.github.com> Date: Sun, 9 Aug 2026 16:01:15 +0900 Subject: [PATCH] knowledge: ingest 2 verified insight(s) --- .dev-loop/INGEST_REPORT.md | 213 ++++++++++++++---- log.md | 1 + .../common/api-design/error-responses.md | 2 +- .../api-design/unenforced-declarations.md | 2 +- .../change-impact/call-site-enumeration.md | 2 +- .../diagnostics-from-a-shared-code-path.md | 86 +++++++ wiki/backend/index.md | 1 + .../methodology/hypothesis-testing.md | 2 +- .../signals/reading-error-messages.md | 2 +- .../exclusivity-and-absence-claims.md | 86 +++++++ ...nerated-artifacts-as-deliverable-source.md | 2 +- .../spec-document-gates.md | 1 + wiki/qa/index.md | 1 + 13 files changed, 352 insertions(+), 49 deletions(-) create mode 100644 wiki/backend/common/errors/diagnostics-from-a-shared-code-path.md create mode 100644 wiki/qa/deliverables/exclusivity-and-absence-claims.md diff --git a/.dev-loop/INGEST_REPORT.md b/.dev-loop/INGEST_REPORT.md index 55ccfd1..95203db 100644 --- a/.dev-loop/INGEST_REPORT.md +++ b/.dev-loop/INGEST_REPORT.md @@ -1,53 +1,180 @@ -# Knowledge consolidation — 15 open PRs (#17–#40) → one reconciled state +# Knowledge flush — 5 insight(s): 2 ingested, 3 dropped as in-flight duplicates -The 15 open `knowledge/*` PRs (created 2026-08-04 → 2026-08-05, before the -harvest processed-store dedupe fix in #41) contained 123 file-versions of ~75 -unique pages, with the same insight landing at up to 3 different paths across -up to 8 PRs. Per-PR review would re-import those duplicates, so — as with the -#6–#13 consolidation — this branch carries the reconciled end-state and the 15 -PRs are closed in its favor. +Queue drained: `~/.dev-loop/queue/` — 5 pending rows across 2 sessions. ## Verified best-practice -Every adopted page's sources were carried from its originating PR's flush, where -they were live-verified at flush time; no new URLs were introduced during -consolidation (checked mechanically: every `http(s)` URL in every merged page -appears in a source PR's diff; every added body line in amended pages traces to -a source PR hunk — orphan-line verification). Confidence fields were kept as the -originating flushes set them, except client-side-rate-limiting where the union -of provider-doc citations (Okta, Auth0, GitHub, OpenAI, RFC 6585) supports -`verified` for the load-bearing claims. One subagent's fabricated content (12 -files matching neither main nor any PR, with invented source URLs) was detected -by the same verification and replaced with true PR content. +### 1. A rejection message emitted from a code path two constructs share → `verified` + +**Claim.** When one function is reached by more than one caller and its message +names a construct in literal text, the subject belongs in a caller-supplied +parameter — and the *repair* the message offers ("use `X` instead") must be +executed from each emitting path, because a wrong subject is caught by reading +while an illegal repair reads as a fix and sends the author into a second, +unrelated rejection. + +**Sources checked (all fetched this session):** + +- — confirms the + confidence-rating half directly: suggestions carry an applicability level and + "Be conservative when choosing the level"; `MachineApplicable` = "Can be + applied mechanically", `MaybeIncorrect` = "Cannot be applied mechanically + because the suggestion may or may not be a good one", `Unspecified` = "we don't + know which of the above cases it falls into". +- + — the enum tools read to decide whether a suggestion is auto-applied or shown + for review. A production compiler encoding "this suggestion may not be valid" + as a required field is the strongest available corroboration that repair + validity is a separate property from message correctness. +- — an error message + must offer constructive advice describing a solution *sufficient for the user + to fix the problem*. Advice that is illegal on the reader's path fails that bar. + +**How verified.** Both Rust pages were fetched and quoted verbatim (not +paraphrased from memory); the NN/g guideline was retrieved via search and its +"constructive advice / solution sufficient to fix the problem" wording confirmed. +The field incident behind the candidate is reproducible in `linkly` +(`impl/lnpl/lower.py`: `_Scope.check_reference` hardcoded "guard condition" while +serving both the guard and assignment paths; its `set`-target advice recommended +`input.`, which `_derive_assignment` rejects for `set` targets by a +separate rule — suite 1864 → 1872 after parameterizing subject/target, the 8 new +per-path assertions and no other delta). + +**Confidence: `verified`** — the general directive is doc-backed, the incident is +the reproduction. + +### 2. An exclusivity or absence claim in a document → `verified` + +**Claim.** "The only way is Y" / "this cannot be expressed" / "exactly N forms" +must be *falsified* before publication, not confirmed — and the document should +carry the rule that generates the forms rather than an enumeration of them. + +**Sources checked (all fetched this session):** + +- — Dijkstra, + EWD303, fetched and quoted: "program testing can be used very effectively to + show the presence of bugs but never to show their absence", and on sampling: + "hopelessly inadequate to convince ourselves of the correctness … whole classes + of in some sense critical cases can and will be missed". This is exactly the + asymmetry an absence claim runs into. +- — fetched and quoted: "It is + logically impossible to verify a universal proposition by reference to + experience …, but a single genuine counter-instance falsifies the corresponding + universal law"; "an exception, far from 'proving' a rule, conclusively refutes + it". Supplies the logic for "supported by a failed refutation, never by + confirmations". +- — dead docs + misinform; documentation changes in the same change as the code it describes. + Supports the re-check directive (an exclusivity claim is invalidated by + additions elsewhere). + +**How verified.** EWD303 and the SEP entry were both fetched and the sentences +quoted verbatim from the retrieved text. The Google docguide URL is the same one +already cited by the merged wiki, so it resolves in this repo's existing +citation set. The field incident is a recorded run: `lnpl spec --run` on +`find order` + `create order` returned `failed` with +`failure_reason='repository create conflicts: entity.order already exists'`, +falsifying the published "only two `create`s conflict" sentence. + +**Confidence: `verified`.** + +### 3–5. The three dev-loop orchestration candidates → not re-verified (dropped) + +Guardrail read-only worktree escalation; Orca terminal/dispatch binding taxonomy; +tmux in-band question menu. These were not researched further because the +open-PR check (below) found each already ingested in an open PR in equal or +better form. Nothing was upgraded to `verified` on the strength of this session. ## Existing-layer check -- Merged-main near-dup scan before consolidation: pairwise Jaccard over - title + "When this applies" across all 141 merged pages → **0 flagged pairs**; - previously merged content carries no duplication. -- Cross-PR dedup during consolidation: 10 duplicate clusters collapsed to one - canonical page each (rate limiting 8→1, call-site enumeration 7→folded into - the canonical merged in #20, stderr/exit-0 diagnostics 4→1, sysroot 2→1, - env-off-switch 2→1, completion predicates 2→1, robots.txt 2→1, - harness-mediated results 2→1, leaked artifacts 2→1, orchestration category - naming unified). Three near-pairs kept distinct after trigger comparison, - with mutual `related:` links (differential setup vs interpretation; expansion - semantics vs off-switch design; import-time tactics vs level choice). -- 24 existing pages received union-merged amendments; additions already present - in main (from #16/#20) were skipped, and all non-canonical `related:` ids - were remapped to canonical page ids (post-merge broken-link scan: 0). +Routed via `INDEX.md` → `backend` (server-side application code, `common/errors` +owns error structure) and `qa` (release-quality process, `deliverables` owns +claims in a published document). + +Pages read: backend-common-api-design-error-responses, backend-common-api-design-unenforced-declarations, backend-common-change-impact-call-site-enumeration, backend-common-errors-exception-handling, backend-common-errors-async-failure-handling, debugging-signals-reading-error-messages, debugging-methodology-hypothesis-testing, qa-deliverables-generated-artifacts-as-deliverable-source, qa-document-verification-spec-document-gates, qa-document-verification-editing-a-gated-document, qa-process-scope-purity-checks, qa-exploratory-lowered-declaration-survival, infrastructure-agent-orchestration-worktree-isolated-workers, infrastructure-agent-orchestration-pane-delivery-confirmation + +Plus a `grep -ril 'diagnostic' wiki/` and `grep -ril 'error message' wiki/` sweep +over the whole wiki, to make sure no page under another domain already owned the +producer side of diagnostics. + +**Overlaps found, and why each is adjacent rather than duplicate:** + +| Existing page | Relation to insight 1 | +|---|---| +| `backend-common-api-design-error-responses` | Owns the *transport* contract — HTTP status codes and the problem+json body. Says nothing about a message's subject or its repair advice. Adjacent, now cross-linked. | +| `debugging-signals-reading-error-messages` | The **consumer** side — how to read a message you were given, including "compilers often print the fix". The new page is the **producer** side: making that printed fix true on the path it was printed from. Complementary; cross-linked both ways. | +| `backend-common-api-design-unenforced-declarations` | Owns *which* diagnostic to emit for unrecognized vs recognized-but-unenforced input; the new page owns how a shared emitter words one. Cross-linked. | +| `backend-common-change-impact-call-site-enumeration` | Supplies the mechanism for "enumerate the emitting paths"; the new page cites it inline. Cross-linked. | + +| Existing page | Relation to insight 2 | +|---|---| +| `qa-deliverables-quantitative-claims-in-a-published-document` (**not merged — open in #51**) | Nearest sibling: *numeric* claims in a published document, recomputed by command. The new page covers *exclusivity/absence* claims, which have the opposite logic (a count is verified by recomputation; a universal claim can only survive a failed refutation). Deliberately **not** related-linked, because the id does not exist on `main` and a link to it would dangle until #51 merges. Flagged here so the owner can add the reciprocal link when #51 lands. | +| `qa-deliverables-generated-artifacts-as-deliverable-source` | Owns "regenerate rather than hand-write"; orthogonal, cross-linked. | +| `qa-document-verification-spec-document-gates` | Owns turning a document requirement into an automated check — the new page's step 6 routes there for making the re-check a gate. Cross-linked. | +| `debugging-methodology-hypothesis-testing` | Owns the structure of the refutation attempt itself; cited inline and cross-linked. | + +**Conflicts flagged:** none. No existing page states a conflicting directive on +either trigger. + +**Merged vs created:** both created new — neither trigger existed anywhere in the +wiki (merge-before-create was checked against every "load when" line in the two +target categories plus the two grep sweeps above). + +**Reciprocal `related:` links added to 6 existing pages:** +`error-responses`, `unenforced-declarations`, `call-site-enumeration`, +`reading-error-messages` (→ insight 1); `generated-artifacts-as-deliverable-source`, +`spec-document-gates`, `hypothesis-testing` (→ insight 2). `last_verified` was +**not** bumped on those pages — only a link was added, no claim was re-verified. + +## Open-PR check + +13 open `knowledge/*` heads listed and each fetched; `git diff origin/main +origin/ -- wiki/` inspected for every one: + +`#66 choiyounggi-20260808-013406`, `#64 choiyounggi-20260808-004155`, +`#62 choiyounggi-20260807-225916`, `#61 choiyounggi-20260807-213244`, +`#58 choiyounggi-20260807-191239`, `#57 choiyounggi-20260807-163902`, +`#56 choiyounggi-20260807-153857`, `#55 choiyounggi-20260807-144058`, +`#52 dch0202-rsquare-20260807-100149`, `#51 dch0202-20260806-183029`, +`#50 dch0202-20260806-172420`, `#49 dch0202-rsquare-20260806-142309`, +`#47 dch0202-20260806-130040`. + +| Candidate | Overlapping head(s) | Verdict | +|-----------|--------------------|---------| +| Shared-code-path rejection message (subject + repair) | none — `#58` touches `backend/common/change-impact/` (corpus sweep before a rejection rule: how to *bound* a new rejection, not how to *word* one from a shared emitter); `#56` touches `unenforced-declarations` frontmatter only | **new** | +| Exclusivity/absence claims in a document | `#51` adds `qa/deliverables/quantitative-claims-in-a-published-document` (numeric claims), `#66` extends `qa/document-verification/spec-document-gates` (gate design) — neither carries the falsification directive or the enumeration-vs-generating-rule rule | **new** | +| Guardrail `worktree_escape` fires on read-only cross-worktree access | `#51` and `#47`, both on `infrastructure/agent-orchestration/worktree-isolated-workers` | **drop** — `#47` carries the identical directive including the escalation round trip and the "reads pre-approved, writes and system-temp still refused" briefing line; `#51` additionally reproduces the rule's mechanism (main-root mention surviving the strip **and** an independent write-verb/absolute-redirect match). Strictly better than the candidate. | +| Orca terminal binding: check idle prompt, branch on `runtime_unavailable` vs `agent_unconfigured`, pass `--worktree` | `#51`, on `infrastructure/agent-orchestration/pane-delivery-confirmation` | **drop** — carries all four rows (bind-after-"done" is a report not a turn end, occupied runtime → wait and rebind, dead agent → replace, pane/worktree mismatch → pass the worktree) plus an `Instead of` row and the three field observations. | +| tmux worker wedged on a numbered in-band question menu | `#64`, new page `infrastructure/agent-orchestration/unattended-worker-questions` | **drop** — supersedes the candidate: it adds the out-of-band question channel, the stall-classification table, the allowlisted key sequence with the selection-then-confirmation step, and the re-send of the interrupted prompt. | + +Three drops, no folds — nothing unique in the dropped candidates was missing from +the open heads, so there was nothing to push to those branches. This is the +recurring trio flagged in `#39`; it re-enters the queue on every flush until +`#47`/`#51`/`#64` merge. ## Routing decision -- New categories: `infrastructure/agent-orchestration` (5 pages; unified the - competing `orchestration`/`agent-orchestration` names), `databases/data-survey` - (1), `qa/deliverables` (1). All other pages route into existing categories. -- Canonical-path decisions: rate limiting → `backend/common/reliability/` - (sits beside timeouts-and-retries; 6 of 8 variants chose it); stderr - diagnostics → `platforms/processes/` (concern spans beyond shells); leaked - artifacts → `testing/data/artifact-leakage-from-a-suite`; call-site - enumeration → the existing `backend/common/change-impact/` page. -- All 38 new pages listed in their domain indexes (nearest-index rule; backend - routes via its python sub-index for bytecode-cache-staleness); INDEX.md domain - summaries updated for infrastructure/qa/databases. Full-wiki lint: frontmatter, - ids, related-links, index coverage, size, qualifiers, staleness → 0 findings. +| Insight | Domain | Category | Page | New category? | +|---------|--------|----------|------|---------------| +| Shared-code-path rejection message | `backend` | `common/errors` (existing — owns error structure and where errors are translated) | `wiki/backend/common/errors/diagnostics-from-a-shared-code-path.md` (new) | No | +| Exclusivity/absence claims | `qa` | `deliverables` (existing — owns claims in a document about to be handed out) | `wiki/qa/deliverables/exclusivity-and-absence-claims.md` (new) | No | + +No new categories were added. Both candidates were considered against the +alternatives before landing: + +- Insight 1 was weighed against `backend/common/api-design/` (where + `unenforced-declarations` lives) and against `debugging/signals/`. It went to + `errors` because the artifact being changed is the emitted error, not the API + contract shape and not the reader's diagnosis workflow. +- Insight 2 was weighed against `qa/document-verification/` (automated gates on a + document). It went to `deliverables` because the directive governs what an + author writes, and only routes onward to `document-verification` for turning + the re-check into a gate. + +Plumbing updated: `wiki/backend/index.md` and `wiki/qa/index.md` each gained a +"load when" row; `log.md` gained the dated ingest entry naming both new pages, +the sources verified, and the three drops with their PR numbers. + +Mechanical check before commit: both pages are 72 body lines (limit 120), every +`related:` id and inline `[page-id]` reference resolves against `wiki/`, and +neither body contains a banned vague qualifier. diff --git a/log.md b/log.md index c930fc2..6aee615 100644 --- a/log.md +++ b/log.md @@ -43,3 +43,4 @@ Append-only. Format: `## [YYYY-MM-DD] ` instead") | Executing the repair as written from each call path and requiring the result to be accepted | +| A pointer to another rule or section | Confirming that rule admits this caller's construct at all | + +3. **Treat the repair as the part most likely to be wrong, and check it per + path.** A repair is advice the author will follow literally; when it is + illegal on one of the emitting paths, following it lands the author in a + second, unrelated rejection. NN/g's rule is that the message must describe a + solution sufficient to fix the problem — on the path the reader is on. +4. **Rate the repair by whether it holds on every path that can emit it.** + Present it as *the* fix (and allow any auto-apply tooling to use it) only when + it is valid on all of them; otherwise branch it. `rustc` encodes the same + distinction as `Applicability` — `MachineApplicable` for a suggestion that can + be applied mechanically, `MaybeIncorrect` for one that "may or may not be a + good one" — and instructs authors to "be conservative when choosing the level". +5. **Assert the message once per emitting path, not once per message.** A single + test on one caller leaves the other caller's subject and repair unasserted, so + parameterizing the subject and breaking the other path's advice both stay + green ([backend-common-change-impact-call-site-enumeration] enumerates the + paths). +6. **When the repair differs by path, branch on the parameter that already + distinguishes them** — pass the repair alongside the subject, so each caller + states the fix that is legal for it. + +## Edge cases + +| Case | Then | +|------|------| +| The two callers reject for the same reason but repair differently | Pass the repair text as a second caller-supplied parameter; keep one rejection rule and two suggestions | +| The suggested form is legal at parse time but rejected by a later rule on this path | The advice is still wrong — run it end to end on that path, not just past the check that emitted it | +| Only one caller exists today | Parameterize the subject anyway when the function is named for the *check* rather than the construct; the second caller is what makes the literal wrong, and it arrives without touching this file | +| The message is localized or templated | Pass the subject as a named placeholder argument rather than concatenating it, so translators receive a slot instead of a sentence fragment | +| The shared function genuinely cannot know the subject | Have callers pass a context value carrying subject and repair together, so a new caller cannot compile without supplying both | +| A repair is valid everywhere except one rarely reached path | Branch it — a suggestion that is wrong on one path is `MaybeIncorrect` for all of them, and rating it that way costs the reader on every path | + +## Instead of + +| If you are about to | Do this instead | Why | +|---------------------|-----------------|-----| +| Write the construct's name into the shared function's message text | Take the subject as a parameter each call site fills | The literal is right for the caller you had in mind and misnames every other one | +| Fix the misnamed subject and ship | Also execute the repair from each emitting path and require acceptance | The subject is checked by reading; the repair is only checked by running, so it is the part that stays wrong | +| Soften the repair into something true on every path ("check the syntax") | Branch the repair on the parameter that distinguishes the callers | A repair that carries no action returns the reader to guessing, which is what the message existed to prevent | +| Assert the message text in one test and call the wording covered | Assert subject and repair once per emitting path | One assertion cannot distinguish "both paths right" from "one path never exercised" | + +## Sources + +- https://rustc-dev-guide.rust-lang.org/diagnostics.html — suggestions carry a confidence level and "Be conservative when choosing the level"; `MachineApplicable` = "Can be applied mechanically", `MaybeIncorrect` = "Cannot be applied mechanically because the suggestion may or may not be a good one", `Unspecified` = "we don't know which of the above cases it falls into" +- https://doc.rust-lang.org/stable/nightly-rustc/rustc_errors/enum.Applicability.html — the enum tools read to decide whether a suggestion is auto-applied or shown for review +- https://www.nngroup.com/articles/error-message-guidelines/ — an error message offers constructive advice: the described solution must be sufficient for the user to fix the problem +- Field incident 2026-08-09 (`linkly`, `impl/lnpl/lower.py`): `_Scope.check_reference` is called from both the guard path and the assignment path and hardcoded "guard condition" into three messages. The `set`-target rejection additionally advised writing `input.`, which `_derive_assignment` rejects for `set` targets by a separate rule — an author following the advice hit a second, unrelated rejection. After threading subject/target through as parameters the suite went 1864 → 1872 (the 8 new per-path assertions, no other change), and an independent audit exercised each branch as its own mutation diff --git a/wiki/backend/index.md b/wiki/backend/index.md index cee0276..691bd26 100644 --- a/wiki/backend/index.md +++ b/wiki/backend/index.md @@ -58,6 +58,7 @@ Match your situation to a "load when" line; load only matching pages. | Page | Load when | |------|-----------| | [exception-handling](common/errors/exception-handling.md) | Writing a catch block or deciding where errors are handled/logged/translated in a service — catch placement, log-once, wrapping with cause preserved, typed results for expected outcomes; one fault producing duplicate alerts | +| [diagnostics-from-a-shared-code-path](common/errors/diagnostics-from-a-shared-code-path.md) | Writing or reviewing a rejection/validation message emitted by one function several callers reach (a check shared by two syntaxes, request and response, two config blocks) — especially when the message names a construct in literal text or tells the author what to write instead; a user reports a rejection naming a construct they did not write | | [async-failure-handling](common/errors/async-failure-handling.md) | Handing work to in-process async (@Async, unawaited futures/promises) — deciding fire-and-forget vs consumed future vs durable job; side effects silently never happening with no error logs; unobserved futures; async work enqueued inside a transaction | ### auth diff --git a/wiki/debugging/methodology/hypothesis-testing.md b/wiki/debugging/methodology/hypothesis-testing.md index 282859c..191a11f 100644 --- a/wiki/debugging/methodology/hypothesis-testing.md +++ b/wiki/debugging/methodology/hypothesis-testing.md @@ -8,7 +8,7 @@ sources: - https://www.debuggingbook.org/html/Intro_Debugging.html - https://sre.google/sre-book/effective-troubleshooting/ last_verified: 2026-07-10 -related: [debugging-methodology-reproduce-first, debugging-methodology-isolate-by-bisection] +related: [debugging-methodology-reproduce-first, debugging-methodology-isolate-by-bisection, qa-deliverables-exclusivity-and-absence-claims] --- # Testing a Suspected Cause Before Changing Code diff --git a/wiki/debugging/signals/reading-error-messages.md b/wiki/debugging/signals/reading-error-messages.md index 6dd651e..ac49f59 100644 --- a/wiki/debugging/signals/reading-error-messages.md +++ b/wiki/debugging/signals/reading-error-messages.md @@ -8,7 +8,7 @@ sources: - https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Errors - https://gcc.gnu.org/onlinedocs/gcc/Warning-Options.html last_verified: 2026-07-10 -related: [debugging-signals-stack-traces, debugging-methodology-hypothesis-testing] +related: [debugging-signals-stack-traces, debugging-methodology-hypothesis-testing, backend-common-errors-diagnostics-from-a-shared-code-path] --- # Reading an Error Message Before Acting on It diff --git a/wiki/qa/deliverables/exclusivity-and-absence-claims.md b/wiki/qa/deliverables/exclusivity-and-absence-claims.md new file mode 100644 index 0000000..c0a73e0 --- /dev/null +++ b/wiki/qa/deliverables/exclusivity-and-absence-claims.md @@ -0,0 +1,86 @@ +--- +id: qa-deliverables-exclusivity-and-absence-claims +domain: qa +category: deliverables +applies_to: [general] +confidence: verified +sources: + - https://www.cs.utexas.edu/~EWD/transcriptions/EWD03xx/EWD303.html + - https://plato.stanford.edu/entries/popper/ + - https://google.github.io/styleguide/docguide/best_practices.html +last_verified: 2026-08-09 +related: [qa-deliverables-generated-artifacts-as-deliverable-source, qa-document-verification-spec-document-gates, debugging-methodology-hypothesis-testing] +--- + +# An Exclusivity or Absence Claim in a Document + +## When this applies + +You are about to write a sentence in a spec, RFC, README, or reference doc that +claims exclusivity or absence: "the only way to X is Y", "there are exactly two +ways this conflicts", "this cannot be expressed", "no path produces Z". Also +when reviewing such a sentence someone else wrote, or when a reader reports a +case the document says is impossible. + +## Do this + +1. **Try to falsify the claim before writing it, and write it only after the + attempt fails.** Construct inputs designed to break it and run them. A + positive claim is established by one supporting example; an exclusivity or + absence claim is destroyed by one counterexample and supported by none, so the + evidence that makes it publishable is a failed refutation, not a confirmation + ([debugging-methodology-hypothesis-testing] owns the attempt's structure). +2. **Choose the claim's form by what you can defend:** + +| You want to write | Defend it with | If you cannot | +|-------------------|----------------|---------------| +| "The only way is Y" | An enumeration of producing paths derived from the code that produces them, plus a failed attempt at a path outside it | Write the existential claim ("Y produces it"), which one example supports | +| "There are exactly N forms" | The rule that generates the forms, plus N as a consequence of that rule | State the rule and drop the count | +| "This cannot be expressed" | A run of the closest expressible input showing the rejection, naming the rule that rejects it | Write "the vocabulary has no verb for it as of ``" | +| "No path produces Z" | A sweep of every module that can write Z, listed by name in the document | Write which paths you swept and that others were not checked | + +3. **Write the rule that generates the cases instead of the list of cases.** "A + create conflicts when the row already exists, and rows appear from the seed + and from an earlier create" stays true when a third row-creating path is + added; "there are two conflicting shapes" quietly becomes false. An + enumeration records what the author knew; a generating rule records what the + system does. +4. **Derive the enumeration by a sweep of the producing code, not from memory.** + Name the modules swept in the document or its review notes, so the next + author can re-run the same sweep instead of re-deriving the boundary. +5. **Record the falsification attempt next to the claim** — the command run, the + input, and the observed result — so a reader can re-run it. Google's docs + guidance is to keep documentation changing with the code it describes; a + recorded attempt is what lets the next change re-check the claim instead of + inheriting it. +6. **Re-run the attempt when the producing paths change.** An exclusivity claim + is invalidated by additions elsewhere, so it belongs in the re-check list of + any change that adds a producer ([qa-document-verification-spec-document-gates] + for turning that re-check into a gate). + +## Edge cases + +| Case | Then | +|------|------| +| The claim is about your own closed vocabulary (a DSL's verb set, an enum) | Derive it from the table the implementation reads, and cite that table's path; a vocabulary listed in prose drifts from the one that is enforced | +| The falsifying input is expressible but has never been run | Run it — a documented impossibility that no test exercises is the shape most likely to be false | +| The counterexample appears only through a second feature's side effect (a seed, a fixture, an import) | It still falsifies the claim; the claim was about the system, not about one entry point | +| An audit confirms the enumeration is complete | Publish the enumeration with the sweep's scope named, so completeness is re-checkable rather than asserted | +| The claim is about an external system you do not control | State the version you checked and the check you ran; without both it is an absence claim about a moving target | +| The document already carries an unverified exclusivity claim | Attempt the refutation before editing the sentence; a reworded unfalsified claim is the same claim | + +## Instead of + +| If you are about to | Do this instead | Why | +|---------------------|-----------------|-----| +| Confirm the claim by running the cases you already believe in | Run the cases designed to break it | Confirmations accumulate without ever ruling out the counterexample; a single counter-instance settles it | +| Enumerate the forms you can think of | Write the rule that generates the forms, and derive any count from it | The enumeration is bounded by the author's knowledge and goes stale the next time a producer is added | +| Write "the only way" because no other way came to mind | Write the existential claim you can support | An unfalsified universal claim reads with the same authority as a checked one and is the one readers act on | +| Take the enumeration from an earlier document or session summary | Re-derive it by sweeping the producing code now | The earlier document has the same drift mechanism and no check, so agreement between two documents is not corroboration | + +## Sources + +- https://www.cs.utexas.edu/~EWD/transcriptions/EWD03xx/EWD303.html — Dijkstra, EWD303: "program testing can be used very effectively to show the presence of bugs but never to show their absence"; sampling "is hopelessly inadequate to convince ourselves of the correctness … whole classes of in some sense critical cases can and will be missed" +- https://plato.stanford.edu/entries/popper/ — "It is logically impossible to verify a universal proposition by reference to experience …, but a single genuine counter-instance falsifies the corresponding universal law"; "an exception, far from 'proving' a rule, conclusively refutes it" +- https://google.github.io/styleguide/docguide/best_practices.html — dead docs misinform; change documentation in the same change as the code it describes +- Field incident 2026-08-09 (`linkly`, spec documentation): the sentence "the only conflicting shape is two `create`s" was falsified by `find order` followed by `create order` against a seeded row — `lnpl spec --run` returned `failed` with `failure_reason='repository create conflicts: entity.order already exists'`. The replacement sentence states the generating rule (a create conflicts when the row exists; rows arise from the seed and from an earlier create) and was published only after an independent sweep of the repo-policy, interpreter, backend, CLI, and spec paths found no third row-creating path diff --git a/wiki/qa/deliverables/generated-artifacts-as-deliverable-source.md b/wiki/qa/deliverables/generated-artifacts-as-deliverable-source.md index 96aa588..f6d4c41 100644 --- a/wiki/qa/deliverables/generated-artifacts-as-deliverable-source.md +++ b/wiki/qa/deliverables/generated-artifacts-as-deliverable-source.md @@ -10,7 +10,7 @@ sources: - https://google.github.io/styleguide/docguide/best_practices.html — keep documentation sources close to the code they describe so they change together last_verified: 2026-08-04 related: - [frontend-state-derived-state, qa-document-verification-spec-document-gates] + [frontend-state-derived-state, qa-document-verification-spec-document-gates, qa-deliverables-exclusivity-and-absence-claims] --- # A Requested Deliverable Duplicating an Artifact the Repo Already Generates diff --git a/wiki/qa/document-verification/spec-document-gates.md b/wiki/qa/document-verification/spec-document-gates.md index 9c2fea6..0a255d7 100644 --- a/wiki/qa/document-verification/spec-document-gates.md +++ b/wiki/qa/document-verification/spec-document-gates.md @@ -20,6 +20,7 @@ related: testing-quality-tests-that-cannot-fail, platforms-environment-unicode-text-matching, qa-deliverables-generated-artifacts-as-deliverable-source, + qa-deliverables-exclusivity-and-absence-claims, ] --- diff --git a/wiki/qa/index.md b/wiki/qa/index.md index 2278dfd..84d5b07 100644 --- a/wiki/qa/index.md +++ b/wiki/qa/index.md @@ -24,6 +24,7 @@ Match your situation to a "load when" line; load only matching pages. | Page | Load when | |------|-----------| | [generated-artifacts-as-deliverable-source](deliverables/generated-artifacts-as-deliverable-source.md) | Asked to produce a document (ERD, schema reference, API surface list, dependency inventory) for a hand-off, review, or external partner when the repo already generates that content from code; deciding whether to re-run a stale generator or hand-write the deliverable; a hand-written reference document disagrees with the live system (checks that gate a document → document-verification) | +| [exclusivity-and-absence-claims](deliverables/exclusivity-and-absence-claims.md) | About to write or review a sentence claiming exclusivity or absence in a spec/RFC/README ("the only way is Y", "exactly two forms", "this cannot be expressed", "no path produces Z"); a reader reports a case the document calls impossible; deciding whether to enumerate forms or state the rule that generates them | ## document-verification