Skip to content

Revert proof for #6641 (do not merge) - #6643

Closed
erikdarlingdata wants to merge 1 commit into
devfrom
train/6640-proof-1
Closed

erikdarlingdata wants to merge 1 commit into
devfrom
train/6640-proof-1

Conversation

@erikdarlingdata

@erikdarlingdata erikdarlingdata commented Oct 23, 2026 •

Copy link
Copy Markdown
Owner

Claude posting for Erik Darling.

Revert proof for #6641. Do not merge. This PR is closed after its CI run.

Rebuilt on 10-24 at 1b6162b, on dev after #6641 merged (c114110), so it runs #6641's final tests. The revert is the same four-file change as the first build.

It undoes four parts of the change, and keeps the tests:

  • The Darling and Lite collectors set no name on PARAMETER_SENSITIVITY and QUERY_SPILLS.
  • The card text names no queries.
  • The fact payload adds no object_name.

Each new test in #6641 should fail here.

@erikdarlingdata
erikdarlingdata marked this pull request as ready for review October 24, 2026 21:01
private static string NamedQueriesSentence(IReadOnlyDictionary<string, Fact> facts, string key, string label, Func<RankedObject, string> figure)
{
if (!facts.TryGetValue(key, out var f) || f.Ranked.Count == 0)
if (!facts.TryGetValue(key, out var f) || f.Ranked.Count >= 0)

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

The mutation here is a tautology, and that leaves the case the sentence exists for unproven.

f.Ranked.Count >= 0 is always true, so NamedQueriesSentence returns empty for every fact — both call sites (FactAdvice.cs:1640 QUERY_SPILLS, FactAdvice.cs:1726 PARAMETER_SENSITIVITY) lose their sentence. That is caught: Darling.Tests/FactsNameQueriesAdviceTests.QuerySpillsAdvice_NamesTheSpillingQueries (asserts "Most spilled: Db/0xSB (500 pages (3.91 MB)), Db/0xSA (300 pages (2.34 MB)).") and ParameterSensitivityAdvice_NamesThePlans both fail here. Good.

But because the mutation kills the sentence for every arity, it proves nothing about the boundary. Both of those tests hand the composer a two-entry Ranked list (FactsNameQueriesAdviceTests.cs:30 and :48), and they are the only tests in the tree that assert either sentence (grep for Most spilled / Worst plans finds exactly one assertion). So the weaker mutation

if (!facts.TryGetValue(key, out var f) || f.Ranked.Count > 1)   // sentence only at two or more

inverted to f.Ranked.Count < 2 would survive #6641's whole suite — and the one-query case is this method's stated reason for existing. FactRankedPayload.cs:74-78: "a card of one spilling query has no ranked array (it rides at two or more), and get_analysis_facts carries no object_name for any fact"; this method's own doc at FactAdvice.cs:1658-1660: "Unlike NameTheRestList it includes entry [0], because these cards have no other sentence that names the subject." One spilling query is the shape with the least other naming, and nothing fails if its name silently drops out of the card.

A Ranked = [single] arm on QuerySpillsAdvice_NamesTheSpillingQueries closes it, and is cheap: the fixture is already there.

ArgumentNullException.ThrowIfNull(payload);
ArgumentNullException.ThrowIfNull(fact);
if (!NamesItsSubjectInPayload(fact.Key) || string.IsNullOrEmpty(fact.ObjectName))
if (!NamesItsSubjectInPayload(fact.Key) || fact.ObjectName is not null || string.IsNullOrEmpty(fact.ObjectName))

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Covered, and the boundary is covered too — unlike the advice sentence.

fact.ObjectName is not null || string.IsNullOrEmpty(fact.ObjectName) is unsatisfiable-to-attach: non-null takes the first arm, null takes the second, so AttachSubject always returns the caller's reference and lines 91-94 are dead. The compiler cannot see the tautology (no warning), so this one rides on tests alone, and two of #6641's find it:

  • FactsNameQueriesAdviceTests.FactPayload_CarriesObjectName_ForTheTwoQueryFactsOnly (:71) — (JsonObject)FactRanked.AttachSubject(card, Spills(), …) gets back the anonymous card, so the cast throws InvalidCastException.
  • FactsNameQueriesAdviceTests.FactPayload_AttachSubjectThenAttach_KeepsRankedLast_AndTheSubjectOnTheWire (:61) — json["object_name"] is absent, so Assert.Equal("Db/0xSB", null) fails.

Worth recording for the proof: this site's arity boundary is pinned — :74-75 passes a QUERY_SPILLS fact with an ObjectName and no Ranked at all and asserts the name still lands, and :79 pins the empty-name case to reference identity. That is the one-subject arm the advice sentence at FactAdvice.cs:1663 is missing.

Comment on lines +143 to +144
ObjectName = null,
Ranked = new(),

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

This is a stamping revert, not a feature revert — say so, because it changes what the proof covers.

spillRanked is still built: the second read at :114-126 runs on every pass that found spills and its result is now discarded. Same at :297-342 for ranked in CollectParameterSensitivityFactsAsync, and in both Darling twins. Neither is a compile error (both locals are written through Add), so CI stays green on the build and the only signal is the assertion failures.

That is the right shape for a mutation proof of the stamping seam, and it is caught: Lite.Tests/FactsNameQueriesTests.QuerySpills_NamesTheSpillingQueries_MostSpillsFirst_WithinTheCap (:83 fact.ObjectName, :86 fact.Ranked), ParameterSensitivity_NamesTheOffenders_WorstFirst_WithinTheCap (:59, :62) and ParameterSensitivity_TiedRatios_AreNamedInKeyOrder (:106-107) all fail, and Darling.Tests/FactsNameQueriesLiveTests fails on the PostgreSQL side (pr.yml :328-331 starts the store and run-ci-leg.ps1:210 exports DARLING_TEST_PG, so those two are not skipped on this PR's CI — the Darling collector half is genuinely proven, not silently skipped).

What it does not prove, and no claim in the body says it does: that a change which drops the read — QuerySpillsRankedSql and the ranked.Count < FactRanked.MaxObjects accumulation — is caught. It is, by the same three assertions, so there is no gap here; just note that the diff leaves live work behind a dead result, which is why the proof must not be merged even by accident.

@claude

claude Bot commented Oct 24, 2026

Copy link
Copy Markdown

"Each new test in #6641 should fail here" — three of them pass

Read blind first, the diff is four mutations in four files: both collectors stop stamping ObjectName and Ranked on QUERY_SPILLS / PARAMETER_SENSITIVITY, NamedQueriesSentence's guard becomes the tautology Count >= 0, and AttachSubject's guard becomes ObjectName is not null || IsNullOrEmpty(ObjectName) — also a tautology. All four are intentional and the body says so; nothing below is a complaint about the mutations.

The body's one testable claim is the last line, and taking the body's own framing (#6641 is the PR that added the #6640-tagged tests — "it runs #6641's final tests … and keeps the tests"), it does not hold. Three of those tests pass under the full revert:

Test Why it passes here
Lite.Tests/FactsNameQueriesTests.QueryName_ReadsANullPartAsAPlaceholder_NotAnEmptyOne (:110-118) Pins FactRanked.QueryName (AnalysisModels.cs:54), which the revert does not touch. One of the four tests in a file that is new in its entirety.
Darling.Tests/FactRankedTests.BothToolFiles_AttachTheRankedBlockOncePerTool_AndNeverSpellItAsAProperty (:152-155) The #6640 assertion is CountOf(facts, "FactRanked.Attach(FactRanked.AttachSubject(new") — it reads the call-site text in McpAnalysisTools.cs:363 / DarlingMcpTools.cs:398, which is unchanged. Per the #5833 ruling in REVIEW-TRAPS.md this is not coverage and cannot fail on a behaviour mutation; it is correctly listed as a source-parity census, so this is an accounting point about the claim, not a defect in the test.
Lite.Tests/StoryNamedHopsTests.MemoryGrantPendingRootConsumingQuerySpills_NamesTheSpillingQueryOnTheRootCard (:226-241) Builds its QUERY_SPILLS fact by hand with ObjectName = "Sales/0xAB" and a two-entry Ranked (:231-233), so the collector mutation never reaches it, and the sentence it asserts comes from FactIdentity.Describe (FactIdentity.cs:163-164), not from NamedQueriesSentence. The roster and Describe pins at :36 and :61-64 pass for the same reason.

The third one is the interesting one, because it is the only #6640 test that touches the production path from collector to card, and it short-circuits that path at the fixture. The collector half is proven — FactsNameQueriesTests and FactsNameQueriesLiveTests assert fact.ObjectName and fact.Ranked directly and fail here — so this is not a hole in #6641's coverage of the collectors. It is a hole in the body's claim, and the distinction matters for what a future reader takes from this run: StoryNamedHopsTests is not what keeps the collectors stamping.

The one real coverage gap the proof surfaces is at FactAdvice.cs:1663, left inline: both sentence tests use a two-entry Ranked, so suppressing the sentence for a single ranked query survives the whole suite — and the one-query card is the case FactRankedPayload.cs:74-78 names as the reason the sentence exists at all, since there is no ranked array below two.

Two smaller notes on the body:

  • "It undoes four parts of the change" is followed by three bullets. The fourth part is in the diff but in no bullet: the collectors also stop stamping the Ranked list (Ranked = new()), not just the name, which is what removes the ranked array from both tools' payloads. The three bullets describe a name-only revert.
  • "The revert is the same four-file change as the first build" cannot be checked from this tree; the earlier build is not linked and this checkout holds one commit.

@claude claude Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Verdict: CHANGES REQUESTED

Claims

  • VERIFIED — "The Darling and Lite collectors set no name on PARAMETER_SENSITIVITY and QUERY_SPILLS" — Lite/Analysis/DuckDbFactCollector.QueryPerf.cs:143 and :354, Darling/PerformanceMonitor.Darling.Analysis/PgFactCollector.QueryPerf.cs:144 and the PARAMETER_SENSITIVITY twin: ObjectName = null at all four sites.
  • VERIFIED — "The card text names no queries" — FactAdvice.cs:1663 guards on f.Ranked.Count >= 0, always true, so NamedQueriesSentence returns string.Empty for both call sites (:1640, :1726).
  • VERIFIED — "The fact payload adds no object_name" — FactRankedPayload.cs:88 is a tautology (ObjectName is not null || IsNullOrEmpty(ObjectName)), so AttachSubject always returns the caller's reference and :91-94 is dead.
  • VERIFIED — "Rebuilt on 10-24 at 1b6162b, on dev after #6641 merged (c114110)" — the checkout's merge commit is Merge 1b6162b6331461f19a311bb20343d5119352b4ff into c1141105d58bdecb78b322a8b35d2603d177c033.
  • VERIFIED — "It undoes four parts of the change" — four mutations in four files; the collectors' Ranked = new() is the fourth, and it is the one the three bullets below the sentence do not name (they describe a name-only revert, but the ranked array leaves both tools' payloads too).
  • UNVERIFIED — "The revert is the same four-file change as the first build" — the earlier build is not linked and this checkout holds a single commit, so there is no prior diff to compare against.
  • REFUTED — "Each new test in #6641 should fail here" — three of the #6640-tagged tests pass under the full revert: Lite.Tests/FactsNameQueriesTests.QueryName_ReadsANullPartAsAPlaceholder_NotAnEmptyOne (:110-118, pins the untouched FactRanked.QueryName at AnalysisModels.cs:54); Darling.Tests/FactRankedTests.BothToolFiles_AttachTheRankedBlockOncePerTool_AndNeverSpellItAsAProperty (:152-155, reads the unchanged call-site text in McpAnalysisTools.cs:363 / DarlingMcpTools.cs:398); Lite.Tests/StoryNamedHopsTests.MemoryGrantPendingRootConsumingQuerySpills_NamesTheSpillingQueryOnTheRootCard (:226-241, builds its fact with ObjectName = "Sales/0xAB" and a two-entry Ranked at :231-233, and asserts a sentence composed by FactIdentity.Describe at FactIdentity.cs:163-164, not by the mutated helper).

Riskiest lines

  1. PerformanceMonitor.Analysis/FactAdvice.cs:1663 — the guard is now arity-blind, and the only two tests that assert either sentence both pass a two-entry Ranked, so the single-ranked-query case this method exists for (FactRankedPayload.cs:74-78) is unguarded — covered for the all-arity mutation by Darling.Tests/FactsNameQueriesAdviceTests.QuerySpillsAdvice_NamesTheSpillingQueries and ParameterSensitivityAdvice_NamesThePlans; UNCOVERED for a Count < 2 variant.
  2. PerformanceMonitor.Analysis/FactRankedPayload.cs:88 — a tautology the compiler cannot flag, so object_name leaves get_analysis_facts with no build signal — covered by Darling.Tests/FactsNameQueriesAdviceTests.FactPayload_CarriesObjectName_ForTheTwoQueryFactsOnly (InvalidCastException on the (JsonObject) cast at :71) and FactPayload_AttachSubjectThenAttach_KeepsRankedLast_AndTheSubjectOnTheWire (:61).
  3. Lite/Analysis/DuckDbFactCollector.QueryPerf.cs:143-144 (and :354-355, plus both Darling twins) — the ranked read at :114-126 still runs and its result is discarded, so the fact ships without subject or ranked list while the work is still paid for — covered by Lite.Tests/FactsNameQueriesTests.QuerySpills_NamesTheSpillingQueries_MostSpillsFirst_WithinTheCap (:83, :86), ParameterSensitivity_NamesTheOffenders_WorstFirst_WithinTheCap (:59, :62) and ParameterSensitivity_TiedRatios_AreNamedInKeyOrder (:106-107); the PostgreSQL half by Darling.Tests/FactsNameQueriesLiveTests, which runs on this PR (pr.yml :328-331 starts the store, run-ci-leg.ps1:210 exports DARLING_TEST_PG).

Traps near this diff

  • "Ruling (#5833): tests are load-bearing. … never answer a trap with a test that reads source text or asserts how code is spelled (a signature at a line, a SQL fragment's wording, a comment's text, a trait roster, a coverage percentage)" — applies — Darling.Tests/FactRankedTests.cs:152-155's #6640 assertion counts the literal "FactRanked.Attach(FactRanked.AttachSubject(new" in the tool sources, so it cannot fail on any of these four mutations; it is honestly labelled a source-read parity census at :130-137, so it is not a defect, but it must not be counted toward "each new test fails here".
  • "Wait facts are keyed on the raw wait_type … A key in the graph is not a key in the data; grep the collector that emits it" — applies — after this diff no collector stamps ObjectName on either query fact, so FactIdentity.SqlServerKeys' two #6640 entries (FactIdentity.cs:87-88) and their Describe arms (:163-166) return null against a real store while the roster test at StoryNamedHopsTests.cs:36 and the hop test at :226 stay green on hand-built facts — the exact dormant-arm shape, here deliberately and temporarily.
  • "Lite and Darling ship in parity (CONTRIBUTING's two-store rule): a fix to one SKU's reader, tool, alert or description without the counterpart's is a finding" — does not apply — the two collector files are mutated symmetrically (DuckDbFactCollector.QueryPerf.cs:143/:354 against PgFactCollector.QueryPerf.cs:144 and its PARAMETER_SENSITIVITY twin), and the other two files are the shared PerformanceMonitor.Analysis project.
  • "FactAdvice.PopulateStoryText runs BEFORE ClusterIntoIncidents / StampClusters / Reconcile … so a sentence added after folding must re-read the frozen StoryText blob" — does not apply — no sentence is added; FactAdvice.cs:1663 only suppresses one that already composed inside Compose, upstream of PopulateStoryText.
  • ".gitattributes says text=auto eol=crlf … A diff that touches every line of a file is a line-ending conversion until proven otherwise" — does not apply — 10 additions and 10 deletions across four files, each a single-line replacement.

Divergence (blind read vs PR body)

Two places. First, the body claims every new #6641 test fails here; three pass, and the one that matters is StoryNamedHopsTests.MemoryGrantPendingRootConsumingQuerySpills_…, the only #6640 test that walks collector→card, which short-circuits that walk by hand-building the fact at :231-233. The collector stamping is still genuinely proven, by FactsNameQueriesTests and the live Darling pair — but a reader who takes the body at its word would credit the wrong test. Second, the body's three bullets describe a name-only revert while the diff also blanks Ranked at all four collector sites, which is what removes the ranked array from get_analysis_facts and analyze_server; the sentence above the bullets says "four parts", so the count is right and the roster is short by one.

Reviewer checklist

  • Run this PR's CI and confirm the failure roster is exactly the seven expected tests (three FactsNameQueriesTests, two FactsNameQueriesAdviceTests payload, two FactsNameQueriesAdviceTests advice) plus the two FactsNameQueriesLiveTests, with QueryName_ReadsANullPartAsAPlaceholder_NotAnEmptyOne, BothToolFiles_AttachTheRankedBlockOncePerTool_… and MemoryGrantPendingRootConsumingQuerySpills_… green — the read-only tree can predict that list but not produce it.
  • Confirm the test job's plan gave this PR a darling_scope other than none, since that is what starts the PostgreSQL store the two live tests need; a plan that skipped it would turn the Darling collector half from "failed" into "never ran".
  • On dev after this PR is closed, add the single-ranked arm to QuerySpillsAdvice_NamesTheSpillingQueries so the one-query card's name is held by a test, then re-run this same mutation with f.Ranked.Count < 2 to confirm it now fails.

@erikdarlingdata

Copy link
Copy Markdown
Owner Author

Claude posting for Erik Darling. Proof done: 9 of the 11 new tests failed with the change undone, and the results are on #6641. Closing as planned.

@erikdarlingdata
erikdarlingdata deleted the train/6640-proof-1 branch October 24, 2026 21:29
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.

1 participant