Facet DoubleRange with an exclusive bound at an infinity is not empty: "value > +Infinity" matches the +Infinity documents

The facet range classes take explicit minInclusive / maxInclusive flags and store inclusive bounds: an exclusive min becomes Math.nextUp(min) and an exclusive max Math.nextAfter(max, -Inf) (range/DoubleRange.java:64-74 on main 645d4fe14a20). Math.nextUp(+Infinity) is +Infinity and Math.nextAfter(-Infinity, -Infinity) is -Infinity, so an exclusive bound that is the infinity on its own side silently becomes inclusive: "value > +Infinity", new DoubleRange(label, +Inf, false, +Inf, true), is stored as [+Inf, +Inf], and the only emptiness check, minIn > maxIn (:76-78), does not fire. The range then counts, and its drill-down query matches, every +Infinity document; the mirror [-Inf, -Inf) matches the -Infinity documents. Every other empty range in the class is rejected with "matches nothing", and LongRange rejects the same case for Long.MAX_VALUE since LUCENE-5371 (4.7.0). The same step is copied into rangeonrange.DoubleRange and DimRange.fromDoubles / fromFloats. Present since the API was added in 4.4.0; every executed release through 10.6.0 and main fails. A 2 x 3-line guard per constructor that rejects these inputs fixes it; the repro and the facet module's checks pass with it. Only this degenerate, always-empty shape is affected, so the priority is low.

1. The constructor (range/DoubleRange.java:61-78; the NaN checks are left out here):

   if (!minInclusive) {
     minIn = Math.nextUp(minIn);                                // :64-66
   }
   if (!maxInclusive) {
     // Why no Math.nextDown?
     maxIn = Math.nextAfter(maxIn, Double.NEGATIVE_INFINITY);   // :71-74
   }
   if (minIn > maxIn) {
     failNoMatch();                                             // :76-78
   }

Math.nextUp(+Inf) is +Inf and Math.nextAfter(-Inf, -Inf) is -Inf. For (+Inf, false, +Inf, true) both stored bounds are +Inf, so minIn > maxIn is false and the range is built.

1. Matching is inclusive on the stored bounds. accept(value) is value >= min && value <= max (:85-87). DoubleRangeFacetCounts.getLongRanges() counts with an inclusive LongRange over doubleToSortableLong(min/max) (DoubleRangeFacetCounts.java:255-270); the drill-down getQuery(...) (:335) matches values.advanceExact(approximation.docID()) && range.accept(values.doubleValue()) (:194-196); for a multi-valued source (:351) the query calls the same range.accept per value (:299).
2. Only the half-open shapes reach it. (+Inf, +Inf) is rejected, because the exclusive max steps down to Double.MAX_VALUE; [x, +Inf) excludes +Inf for the same reason. A Z3 model of the scalar range.DoubleRange constructor and accept proved that, for that class, the two cases (+Inf, +Inf] with x = +Inf and [-Inf, -Inf) with x = -Inf are the only mismatches between accept and the requested predicate, with no false negatives. The copies below are not in that model; they were tested separately.
3. Copies. rangeonrange.DoubleRange repeats the constructor's bound handling: the same NaN checks, nextUp / nextAfter steps, "Why no Math.nextDown?" comment and min > max check (rangeonrange/DoubleRange.java:43-60, written minInclusive == false instead of !minInclusive); a "> +Inf" query range then INTERSECTS every indexed range whose upper end is +Inf. DimRange.fromDoubles (facetset/DimRange.java:60-81) and fromFloats (:84-104) use Math.nextUp / Math.nextDown with the same min > max check.
4. The long siblings guard it. LongRange calls failNoMatch() for an exclusive Long.MAX_VALUE min or Long.MIN_VALUE max (range/LongRange.java:58-72), as do rangeonrange.LongRange and DimRange.fromLongs (DimRange.java:34-49, IllegalArgumentException("Invalid min input: ...")).

Five documents with a DoubleDocValuesField value of -Infinity, -2.5, 1.5, 7 and +Infinity:

An independent check reproduced the count and the drill-down hit with values {-Inf, -1.0, 0.5, 1.0, +Inf}.

• Who can hit it. Code that computes a bound and builds "value > threshold" as DoubleRange(label, threshold, false, +Inf, true), or the mirror "value < threshold", when the threshold is the infinity on that side. Natural sources: the minimum of no values is +Infinity (new DoubleSummaryStatistics().getMin()), and "value > min" then matched the +Infinity documents in an executed probe; a bucket list whose last boundary is +Infinity plus an overflow bucket "> last boundary" (an executed test with left-open buckets over {0, 10, +Inf} counted the +Infinity document in (10, +Inf] and again in the overflow bucket); for range-on-range, any indexed open-ended range [x, +Inf] is matched by a "> +Inf" query range.
• What it takes. The standard facet range API with its own inclusive flags; default codec, configuration and searcher; no opt-in setting; one +Infinity document suffices. The classes are marked @lucene.experimental.
• Effect. Silent wrong results: a range that should be empty counts, and drill-down matches, exactly the documents at that infinity. No exception, no hang, no false negatives. The extra matches are only documents whose value is exactly that infinity, still within the hits the application's query collects and the drill-down's other clauses.
• How likely. Rare: it needs an exclusive bound that is itself an infinity and documents at that infinity. The recorded searches found no public report since 4.4.0 (2013).

The test accepts either correct outcome: the constructor rejects the empty range (what the fix does, and what the class already does for (+Inf, +Inf)), or the range does not accept +Inf. accept() is the predicate the class documents as "True if this range accepts the provided value"; the facet count and the drill-down use the same stored bounds, so the end-to-end symptom follows from it. No index and no randomness; the seed only feeds the test runner.

Left out on purpose: the mirror case [-Inf, -Inf) and the two copies (rangeonrange.DoubleRange, DimRange.fromDoubles / fromFloats) are the same idiom at parallel fix sites; the fix covers all of them. The copy in src/ is the same test with the Apache license header and two lint fixes that ./gradlew check asks for (a comment line shortened to 100 columns, the unused catch parameter written as _). The unnamed _ needs Java 22 or later: fine on main (Java 25), but branch_10_6 has minJava = "21", and its ecj lint, like main's, rejects an unused named catch parameter, so a 10.x backport needs another form of the test (for example one that asserts the caught exception's message); none was written or built there.

cp $REPRO/TestDoubleRangeExclusiveInfinityBound.java $LUCENE/lucene/facet/src/test/org/apache/lucene/facet/range/
cd $LUCENE && ./gradlew :lucene:facet:test --tests TestDoubleRangeExclusiveInfinityBound -Ptests.seed=DEADBEEF -Ptests.asserts=true
# also with -Ptests.asserts=false

TestDoubleRangeExclusiveInfinityBound > testExclusiveMinAtPositiveInfinityMatchesNothing FAILED
    java.lang.AssertionError: (+Inf, +Inf] should match nothing, but accept(+Inf) returned true
        at __randomizedtesting.SeedInfo.seed([DEADBEEF:E81052A4E03D596]:0)
        ...
        at org.apache.lucene.facet.range.TestDoubleRangeExclusiveInfinityBound.testExclusiveMinAtPositiveInfinityMatchesNothing(TestDoubleRangeExclusiveInfinityBound.java:15)
:lucene:facet:test (FAILURE): 1 test, 1  failure

# the same with -Ptests.asserts=false; the same on the 10.6.0 release jars (assertions on and off)
# with the fix: :lucene:facet:test (SUCCESS): 1 test (assertions on and off)

• Contract. The constructors own the exclusive meaning: rangeonrange.DoubleRange documents "@param minInclusive if the minimum is inclusive" and "@param maxInclusive if the maximum is inclusive" (rangeonrange/DoubleRange.java:35, :37). An exclusive min of +Infinity means "value > +Infinity".
• Empty ranges are an error in this package. Range.failNoMatch() is "Invoke this for a useless range" (range/Range.java:37-40); testUselessRange asserts that new DoubleRange("useless", 7.0, true, 7.0, false) throws (TestRangeFacetCounts.java:288-295).
• The upstream oracle is strict. testRandomDoublesSingleValued expects values[i] > min for an exclusive min and values[i] < max for an exclusive max (TestRangeFacetCounts.java:1166-1174; multi-valued :1346, :1351). Its bounds are nextDouble() values in [0, 1) or earlier boundaries, never an infinity, which is why the tests miss it.
• History. LUCENE-4965 (3d60bd10d48d, 2013) also wrote LongRange with the integer form of the same saturation, if (!minInclusive && min != Long.MAX_VALUE) min++;. LUCENE-5371 (8e1879225a35; branch_4x merge 7477fde1cb06, first release 4.7.0) replaced it with failNoMatch() and, in the same commit, gave DoubleRange only the min > max check. Executed: LongRange (MAX, MAX] is accepted on 4.4.0-4.6.1 and rejected from 4.7.0; DoubleRange (+Inf, +Inf] is accepted on every release run. The recorded searches and our code reading found no javadoc, CHANGES entry, test, issue or PR that calls the double case intended.
• What this does not settle. The evidence shows the membership is wrong; it does not settle whether the constructor should throw. The scalar constructor's javadoc is only "Create a DoubleRange." (range/DoubleRange.java:51); only rangeonrange.DoubleRange documents the inclusive flags. Throwing follows the package's convention for empty ranges; matching nothing is a defensible alternative a maintainer may prefer (see the fixes).

The strongest case for "intended": Lucene's documented recipe for exclusive float/double bounds is to step to the next value and accept saturation. DoublePoint.newRangeQuery says "Ranges are inclusive. For exclusive ranges, pass nextUp(lowerValue)" (core document/DoublePoint.java:210), TestPointQueries pins DoublePoint.nextUp(+Inf) == +Inf (TestPointQueries.java:2401), and on LUCENE-7092 (#8148, 2016) Robert Muir wrote "The range facets in lucene are also inclusive too" and "If its float/double use Math.nextUp/nextDown". So the facet DoubleRange could be called "consistent with core".

Why it does not hold, in our reading: in core the caller does the stepping and the helper's return value is what is pinned; these constructors instead take an exclusive flag and promise the exclusive meaning themselves, reject every other empty range, and LUCENE-5371 removed the identical saturation for longs; the LUCENE-7092 remark was about the idiom in general, not an exclusive bound that is itself an infinity. As the cross-model intended-lens review put it, "the helper's saturation being intentional does not make the resulting membership semantics intentional." A sentinel reading (+Inf = "unbounded") does not apply either: the class excludes +Inf from [x, +Inf), and "> unbounded" has no meaning. The core convention is still real evidence for a maintainer who would rather document the degenerate input as unsupported; it does not justify silently including an excluded value. Verdict: not intended, a defect.

One option was built and run in a scratch worktree of 645d4fe14a20; the two alternatives are not recommended. The bug is the wrong membership; throwing is the recommended trade-off, not the only correct reaction, and a maintainer may prefer an empty range (option 2).

The finder's fix, two 3-line guards per constructor or factory. range.DoubleRange and rangeonrange.DoubleRange call failNoMatch(); DimRange.fromDoubles and fromFloats throw IllegalArgumentException("Invalid min input: " + min) / ("Invalid max input: " + max), the messages fromLongs uses. Shown for range.DoubleRange:

 if (!minInclusive) {
+  if (minIn == Double.POSITIVE_INFINITY) {
+    failNoMatch(); // nothing is > +Infinity (Math.nextUp(+Infinity) == +Infinity)
+  }
   minIn = Math.nextUp(minIn);
 }
 ...
 if (!maxInclusive) {
+  if (maxIn == Double.NEGATIVE_INFINITY) {
+    failNoMatch(); // nothing is < -Infinity
+  }
   // Why no Math.nextDown?
   maxIn = Math.nextAfter(maxIn, Double.NEGATIVE_INFINITY);

Trade-offs

• Matches LongRange, rangeonrange.LongRange, DimRange.fromLongs and the package's "a useless range throws" convention. No per-document matching or counting cost: the checks run once per range construction.
• Behaviour change: code that today builds (+Inf, +Inf] or [-Inf, -Inf) from computed bounds gets an IllegalArgumentException instead of a (wrong) count, so a CHANGES note is appropriate.
• The sandbox facet cutters of #13568 read DoubleRange's adjusted bounds, so they are covered too (by reading; not run).

What the checks validated

• Scratch worktree of 645d4fe14a20, gradle, JDK 25: stock + test fails with assertions on and off; + fix: the test passes with assertions on and off.
• + fix and the test: :lucene:facet:check BUILD SUCCESSFUL (all 40 facet test classes, 307 tests, 7 skipped, 0 failures; google-java-format, ecj lint, forbidden APIs, license checks); :lucene:facet:test with assertions off: 307 tests, 0 failures.
• Earlier, on main ea57360912ed with the fix shadowed in: the finder's, the independent reproduction's, the cross-model review's and the intended-behaviour check's tests all pass, and 56 of 56 upstream facet range, range-on-range and facet-set tests pass.
• Not run: the full Lucene test suite, nightly tests, and any build or test of the fix on branch_10_6 / 10.6.0 (same constructor lines; a 10.x backport needs a Java 21 form of the test, see the repro).

Represent the empty range explicitly (a flag, or bounds that accept() and the counters treat as empty). Not built.

Trade-offs

Avoids the behaviour change for callers that compute bounds from data, but contradicts the package convention that an empty range throws (testUselessRange), and DoubleRangeFacetCounts converts every range to an inclusive LongRange, which itself rejects min > max, so it touches more code.

A javadoc note that an exclusive bound at the infinity on its own side is not supported.

Trade-offs

Leaves the silent wrong result in place.

Method: SMT (Z3) floating-point model checking of the facet range classes, a hunt unit (facet taxonomy and ranges), over raw 64-bit patterns. Obligation O2a, "DoubleRange.accept equals the requested IEEE predicate whenever the constructor does not throw", was posed as an expected-UNSAT safety proof; the solver returned SAT with the counterexample [-Inf, -Inf), x = -Inf. Obligation O2a2 then proved (UNSAT) that the mismatch set is exactly (min = +Inf exclusive, x = +Inf) or (max = -Inf exclusive, x = -Inf). A bounded-exhaustive run over the public API (411,854 checks) found these two infinity classes as the only accept-versus-requested mismatches (its other classes belong to a separate signed-zero candidate). The finder then wrote a public-API JUnit on the stock main jars; the DimRange copy was pointed out by the cross-model refute review and the range-on-range copy came from code reading. This doc's test is a one-method form of it.