MaxScoreBulkScorer can skip a document whose score equals the minimum competitive score

For a top-k (TOP_SCORES) disjunction of 4 or more SHOULD clauses that runs on MaxScoreBulkScorer (a pure SHOULD disjunction with minShouldMatch <= 1, or SHOULD + FILTER with no MUST clause and minShouldMatch 1), the scorer may make the best non-essential clause required: if the essential clause plus every other non-essential clause cannot reach the minimum competitive score, documents that lack that clause are dropped. The test that decides this (MaxScoreBulkScorer.java:540) casts a double sum to float without MathUtil.sumUpperBound, and it adds the clause maxima in a different order from the document's own score. When clause scores span more than about 2^29 and the exact sum sits next to a float rounding midpoint, the bound rounds one float step below a document that lacks the clause, so that document is skipped although its score equals the minimum. Through IndexSearcher#search(q, n) the k-th hit becomes one float step worse than a skipped document, and with searchAfter paging the skipped document appears on no page. In this class and the other disjunction scorers, the floating-point bounds that add the maxima in a different order from the score use sumUpperBound; line 540 does not. Introduced by #12589 (9.9.0); every release from 9.9.0 to 10.5.2, 10.6.0 (by reading) and main is affected. No upstream report was found.

• Minimum competitive score: once a TopScoreDocCollector has counted more than totalHitsThreshold hits (1,000 for IndexSearcher#search(q, n)), it calls setMinCompetitiveScore(nextUp(k-th score)) (TopScoreDocCollector.java:154-164). The scorer "may safely ignore all documents whose score is less than" it (Scorable.java:45-47).
• Essential, non-essential and required clauses (MAXSCORE): the clauses whose summed maximum scores stay below the minimum are non-essential; a competitive document must match an essential one. With a single essential clause, #12589 added one more step: if the essential clause plus every non-essential clause but the best one cannot reach the minimum, the best one becomes required, and documents without it are dropped.
• MathUtil.sumUpperBound(sum, n): inflates a double sum of n values by a relative 2(n-1)·2^-52 so that it bounds the sum in any order: "The error of sums depends on the order in which values are summed up" (MathUtil.java:184-186).

1. A TOP_SCORES query with 2 or more SHOULD clauses, no MUST or FILTER clause and minShouldMatch <= 1 gets a MaxScoreBulkScorer (BooleanScorerSupplier.java:210, :308-328). So does SHOULD + FILTER with no MUST clause and minShouldMatch exactly 1 (:233-234, :340-364), for example after BooleanQuery.rewrite inlines a single MUST disjunction next to a FILTER (BooleanQuery.java:591-607); FILTER + SHOULD with the default minShouldMatch 0 does not. With sparse MUST_NOT clauses (cost at most 0.3% of maxDoc) the Scorer-based path runs instead (:203-207).
2. partitionScorers sorts the clauses by maxWindowScore / Math.max(1L, cost) and makes each clause non-essential whose max score keeps (float) MathUtil.sumUpperBound(runningSum, count) below minCompetitiveScore; the others become essential, so the non-essential set need not be a prefix of the sorted order (MaxScoreBulkScorer.java:486-511). The left fold of the non-essential maxima is stored in maxScoreSums (:505).
3. With a single essential clause (:524), the required-clause loop (:535-547) builds maxRequiredScore + maxScoreSums[firstRequiredScorer - 2] (:533, :536-539) and tests if ((float) maxPossibleScoreWithoutPreviousClause >= scorable.minCompetitiveScore) break; (:540), without sumUpperBound.
4. A document's score starts from the essential clause (:343-348) and adds clauses i = n-2 .. 0 one at a time (:452-466); required clauses go through ScorerUtil.applyRequiredClause, which drops every buffered document that does not match (ScorerUtil.java:173-190). Float cast at :469.
5. So the bound adds the tail of the maxima as one pre-summed group, the document adds it one term at a time. With 3 clauses the orders coincide; with 4 or more they can differ by one double rounding step, and on a float rounding midpoint the bound casts one float below the document.

Clauses sorted t, a, j (non-essential) and e (essential) at minimum nextUp(1f):

• 4 or more SHOULD clauses and a single essential clause in the window.
• Clause scores spanning more than about 2^29: if every term is at least about 2^-29 of the total, every double addition is exact and the bound is sound. Examples: a tiny tie-break boost beside normal scores, or a BM25 term present in almost every document of a very large index.
• An exact sum within a few double ulps of a float rounding midpoint. A model simulation with random scores and an adversarial minimum found 1 hit in 64M trials.
• The skipped document scores exactly the minimum (the study verifier's argument for realistic clause counts). In the executed path, a single TopScoreDocCollector, that is one float step above the k-th hit. In concurrent search, when the shared minimum comes from a later slice (TopScoreDocCollector.java:137-151), and with a TopFieldCollector whose first sort is relevance (TopFieldCollector.java:380-392), the minimum can be the k-th score itself, so a document that ties it and would win on doc ID could be lost (read in code, not executed).

• Who is exposed. The ordinary public TOP_SCORES path, no experimental or opt-in feature: IndexSearcher#search(q, n) or another TOP_SCORES collection of a query with 4 or more SHOULD clauses that runs on MaxScoreBulkScorer: a pure SHOULD disjunction with minShouldMatch <= 1, or SHOULD + FILTER with no MUST clause and minShouldMatch 1 (the FILTER case read in code, not executed). Codec-independent. The repro pins the default codec, one segment, NoMergePolicy and no query cache only to be deterministic; only the single-segment, no-executor path was executed.
• What they see. In the executed path, a document whose score is exactly one float step above the k-th returned hit is missing from the top k, and a hit one float step lower takes its place. With an executor or a relevance-first TopFieldCollector, a document that ties the k-th score exactly and would win on doc ID could be lost instead (read in code, not executed). The returned scores are correct, and nothing that does not match is added. No exception, with assertions on or off.
• Paging loses it for good. The skipped document ranks above the last hit of its page, so searchAfter never returns it: on the repro index, 111 pages of 10 hold 1,101 of the 1,102 hits and miss the best one. With the fix, page 1 starts with it.
• How likely. Contrived (registry likelihood "contrived"): the 2^29 spread plus a sum at a rounding midpoint; the study's model simulation saw 1 hit in 64M adversarial trials. For relevance alone a one-float-step swap is negligible; it matters where exact top-k is relied on, such as paging or comparing pruned and unpruned results.
• Scale. None: 2 documents for the contract test, 6,001 for the end-to-end test.
• Long-standing. Every release since 9.9.0 (released 2023-12-04). Severity low (registry priority low).

# Lucene main 645d4fe14a20, assertions on (-ea), seed DEADBEEF: 1 test(s) run, 1 failed
    => java.lang.AssertionError: doc 0 must be collected at minCompetitiveScore = its own score expected:<[4.0000005]> but was:<[]>
       org.junit.Assert.fail(Assert.java:89)
       org.junit.Assert.failNotEquals(Assert.java:835)
       org.junit.Assert.assertEquals(Assert.java:120)
       org.apache.lucene.search.TestMaxScoreRequiredClauseRounding.testDocScoringMinCompetitiveScoreIsCollected(TestMaxScoreRequiredClauseRounding.java:90)

The contract, in its own words (at ea57360912ed):

• Scorable#setMinCompetitiveScore: "Tell the scorer that its iterator may safely ignore all documents whose score is less than the given minScore" (Scorable.java:45-47).
• IndexSearcher#search(Query, int): "Finds the top n hits for query." (IndexSearcher.java:617-623). TopScoreDocCollectorManager: totalHitsThreshold is "the number of docs to count accurately" (:35-55).
• MathUtil.sumUpperBound: "The error of sums depends on the order in which values are summed up. In order to avoid this issue, we compute an upper bound of the value that the sum may take." (MathUtil.java:184-186).
• The comment above the loop presents the step as exact: "we know that hits must match both the essential clause and the best non-essential clause" (MaxScoreBulkScorer.java:525-531).
• Lucene's test oracle asserts that every document a pruned scorer skips scores strictly below minScore (CheckHits.java:744-749).

Cross-order bounds. Where a floating-point bound adds the maxima in a different order from the score, Lucene wraps it in sumUpperBound: the partition loop above line 540 (MaxScoreBulkScorer.java:500-502), ScorerUtil.minRequiredScore (ScorerUtil.java:131-142), WANDScorer.java:192 and :591, and DisjunctionSumScorer.java:68. The conjunction scorers cast a plain double sum (BlockMaxConjunctionBulkScorer.java:74-83, compared at :163; BlockMaxConjunctionScorer.java:225-231), which is sound because they add in the score's own order (MathUtil.java:188-191: for conjunctions "the order in which scores are summed up is predictable"). Line 540 adds in a different order and is not wrapped. #12589 wrapped its two new per-document comparisons but not the new required-clause test (diff lines 169, 187 and 284 of git show 611bbbd9512 -- lucene/core/src/java/org/apache/lucene/search/MaxScoreBulkScorer.java).

History. #12589 ("Sometimes intersect the essential clause and the best non-essential clause.", 2023-10-24): no discussion of rounding in the body or its 6 comments; the PR has no reviews. #13397 (2024-05-21) fixed a bound summed in float in BlockMaxConjunctionBulkScorer as a bug: "Otherwise, max scores may be returned that are less than actual scores." In the #14751 review a maintainer suggested (float) MathUtil.sumUpperBound(maxRemainingScore, numScorers) >= minCompetitiveScore, the shape of the fix here.

Why the tests miss it. TestMaxScoreBulkScorer.testPartition checks the required-clause partition with 3 clauses, where both orders coincide; its other tests use small integer scores with Math.nextUp thresholds, where every sum is exact.

Lucene accepts ulp-level score differences between execution strategies: BooleanWeight.explain pulls a scorer because "Replicating the same floating-point errors as the scorer does is quite complex" (BooleanWeight.java:121-125), and a 2021 maintainer comment on #10375 says top hits that differ "in the order of one ulp" can come from summation order. So a one-float-step swap at rank k could be called within tolerance. A read-only cross-model review recorded "not real, low confidence".

Why it fails:

1. That tolerance is about different strategies disagreeing in the last bit. Here one scorer, under one partition, skips a document it itself scores exactly at the minimum (explain agrees), and two TOP_SCORES runs on the same searcher that differ only in totalHitsThreshold return different top hits.
2. The class wraps its other cross-order bounds in sumUpperBound, the same commit did so for its other new comparisons, and #13397 treated the same kind of error as a bug.
3. The fix adds a few floating-point operations per iteration of the required-clause loop (at most n-1 per partition), never per document.
4. The read-only reviewer could not run code; it wrote that its verdict is "not a substantive refutation" and that static inspection "strongly supports a genuine, rare wrong-results defect". Its earlier, code-executing attempt wrote its own test, which fails on main and passes with the fix.

With other numbers the exhaustive BooleanScorer and explain() score the affected document one float lower, so an exact TOP_SCORES-vs-COMPLETE check can fail even after the fix: over the 24 clause orders of the end-to-end index, COMPLETE returns doc 5000 in only 12, before and after the fix, while the pruned search returns doc 0 in all 24 on stock and doc 5000 in all 24 with the fix.

One option was validated with gradle in a scratch worktree at ea57360912ed (removed after the runs); a second was validated with the repro runner only; the third was not run.

The same pattern as the partition loop above it (:500-502) and ScorerUtil.minRequiredScore.

// MaxScoreBulkScorer.partitionScorers, required-clause loop
// (was: if ((float) maxPossibleScoreWithoutPreviousClause >= scorable.minCompetitiveScore) {)
if ((float) MathUtil.sumUpperBound(maxPossibleScoreWithoutPreviousClause, allScorers.length)
    >= scorable.minCompetitiveScore) {
  break;
}

Trade-offs

• Sound for any summation order, now or after later refactorings: the study's Dafny model proves the fixed test sound on an abstract real-number rounding model with 5 axioms, for clause counts with n·2^-53 <= 1/16 (any realistic count); not a bit-level binary64 or bytecode proof. An independent replication fails the proof when the bug is re-introduced.
• The inflation is a relative 2(n-1)·2^-52 (about 1.3e-15 for 4 clauses), so it only changes the decision next to a rounding midpoint; the per-document filter already applies the same inflation.
• Cost: a few floating-point operations (Math.scalb, three multiplies, an add) per iteration of the required-clause loop, at most n-1 per partition; never per document; no benchmark run. allScorers.length is conservative; any count at least the number of summed terms is sound.

What the checks validated

• Gradle, stock: the repro fails 2 of 2 with assertions on and off.
• Gradle with the fix: the repro plus TestMaxScoreBulkScorer, TestBoolean2, TestBooleanQuery, TestBooleanMinShouldMatch, TestBooleanOr, TestBooleanScorer, TestBooleanScorerSupplier, TestWANDScorer, TestScorerUtil, TestTopDocsCollector and TestMathUtil: 157 tests, 0 failures (seed DEADBEEF, assertions on; seed CAFEBABE, assertions off).
• Gradle with the fix: all of org.apache.lucene.search.* in :lucene:core, 2,332 tests, 0 failures, 49 skipped.
• ./gradlew :lucene:core:tidy leaves the fix line unchanged.
• The repro runner: the three independent tests and the paging probe pass; 106 upstream tests pass stock and patched on seeds DEADBEEF and CAFEBABE, and 121 on seed 7E57AB1E.
• Not run: the rest of :lucene:core, other modules, a performance benchmark.

Replace + maxScoreSums[firstRequiredScorer - 2] by adding allScorers[i].maxWindowScore for i = firstRequiredScorer - 2 .. 0 one at a time onto maxRequiredScore, the order scoreNonEssentialClauses uses.

double maxPossibleScoreWithoutPreviousClause = maxRequiredScore;
for (int i = firstRequiredScorer - 2; i >= 0; --i) {
  maxPossibleScoreWithoutPreviousClause += allScorers[i].maxWindowScore;
}

Trade-offs

Exact rather than inflated, because rounded addition is monotone (an argument, not proved). But it ties correctness to the summation order in scoreNonEssentialClauses, which has been refactored before; a later change there would silently bring the bug back. O(n) per loop iteration instead of O(1).

What the checks validated

The repro passes 2 of 2 with -ea and -da, the 5-clause test 3 of 3, the reviewer's test 3 of 3, and 121 upstream tests pass (seed DEADBEEF). Not run with gradle.

Return to the 9.8.0 partition without required clauses.

Trade-offs

Loses the #12589 speedup for single-essential-clause windows. Not recommended.

Method: deductive proof (Dafny) plus IEEE-754 SMT (Z3), the study's formal tier, run 3, experiment "topk-pruning-proof" (2026-10-22, main 7cecf79523).

• An AI tool modelled Lucene's dynamic top-k pruning (the partition, the per-document filter and the required-clause test) and the document score fold, each mapped to Java lines. The obligation that the required-clause test as coded never drops a competitive document was not provable from the IEEE axioms (RequiredClauseUnsound.dfy); the same statement with sumUpperBound(., n) was proved.
• A Z3 model with exact binary32/binary64 round-to-nearest-even semantics then produced a witness for the scorer-level failure in 7.4 s and, adding cost-feasibility for the clause sort and the measured BooleanScorer order, an end-to-end witness in 6.0 s: the boosts of the end-to-end test. The 7.4 s witness has scores of about 1e-23; the contract test's round numbers (0.75, 0.25 + 2^-24, 2^-53 + 2^-76, 0.5) follow the same pattern, and the study's Dafny file lists them as an example, but no Z3 log records how they were chosen. A third query (every one of the 6 summation orders reaching the minimum) was UNSAT, so the bug needs an order-dependent score.
• The AI tool reported seeing no hint about this area. A separate AI verifier reproduced it with its own numbers and layout and found the COMPLETE/explain caveat; an independent Dafny replication fails when the bug is re-introduced into the fixed test.
• On 2026-10-26 the hunt re-ran it on ea57360912ed and the release jars, built the history, searched for prior reports, ran a cross-model review and a second adjudication with a third independent test, and for this page validated the fix with gradle and ran the paging probe.