Operations.isTotal can say "accepts everything" for a DFA that can reach a dead state, so an AutomatonQuery built from it matches every term

Operations.isTotal(a) is documented to return true only if the automaton accepts all strings. Since Lucene 10.0.0 it can return true for a deterministic automaton that rejects some strings: it checks only the live states, so a reachable non-accepting dead (sink) state is never looked at, while the transition into the sink still counts as covering the alphabet. The answer is wrong when every live state accepts and covers the alphabet, so that the only rejected strings are those that run into the sink; a reachable dead state alone is not enough. CompiledAutomaton turns the wrong true into AUTOMATON_TYPE.ALL, so an AutomatonQuery silently matches every term of the field (3 documents instead of 2 in the repro). Lucene 9.12.x answers correctly. The cause is #13707, which generalised isTotal from minimal to any deterministic automaton. A direct isTotal call with this automaton is inside its documented contract (determinism only); the AutomatonQuery path also crosses the CompiledAutomaton class javadoc, which says a deterministic automaton "must not have dead states", a rule that AutomatonQuery does not restate. Lucene's own query builders produced no dead state in sampled checks, so the trigger is an automaton that the application builds itself. Downstream code uses isTotal as a grant-all decision, but the bug is not security-sensitive: the trigger is an automaton the application builds, out of scope of Lucene's SECURITY.md (registry none since the strict re-evaluation of 2026-10-27). A one-line fix passes the repro and the whole core test suite.

• Deterministic automaton (DFA): from every state, each character leads to at most one next state. Lucene's Automaton numbers its states; state 0 is the start.
• Dead state (sink): a state from which no accepting state can be reached. A complete DFA, the textbook form, sends every character it rejects into one such sink, which loops on everything.
• Live state: a state reachable from the start that can still reach an accept state (getLiveStates, Operations.java:922-930).

  state 0 (accepting):     [U+0000 .. U+0060]  -> state 1   ('0', ' ', '`' ... go to the sink)
                           [U+0061 .. U+10FFFF] -> state 0   ('a' and above stay)
  state 1 (not accepting): [U+0000 .. U+10FFFF] -> state 1   (the sink)

It is deterministic, accepts b and zz, and rejects 0. Operations.removeDeadStates(a) gives the same language with only state 0.

1. isTotal(a) (844-846) calls isTotal(a, Character.MIN_CODE_POINT, Character.MAX_CODE_POINT) (856-879).
2. 857: BitSet states = getLiveStates(a); is {state 0}: the sink cannot reach an accept state, so it is not live.
3. 861-862, under the comment "all reachable states must be accept states": state 0 is accepting.
4. 863-871, the gap scan ("no gaps are allowed"): [0, 0x60] and [0x61, 0x10FFFF] leave no gap. The scan looks at label ranges only, not at where they go, so the range that leads into the sink counts as covered.
5. 878: return seenStates > 0; gives true. The sink, which is reachable and not accepting, was never checked.

• AutomatonQuery always builds new CompiledAutomaton(automaton, false, true, isBinary) (AutomatonQuery.java:99).
• CompiledAutomaton calls Operations.isTotal(automaton), or isTotal(automaton, 0, 0xff) for a binary automaton, and on true sets AUTOMATON_TYPE.ALL, "Automaton that accepts all possible strings" (CompiledAutomaton.java:55-56, 179-199).
• For ALL, getTermsEnum returns terms.iterator(): every term of the field (CompiledAutomaton.java:352-353). Terms.intersect on that compiled automaton throws IllegalArgumentException("please use CompiledAutomaton.getTermsEnum instead") instead (Terms.java:79-80, executed).

The 9.12 javadoc said "The automaton must be minimized", and the body recognised one shape only: state 0 accepting, with a single self-loop over the whole alphabet. Everything else got false. That could be a missed optimization, but never a wrong true. #13707 (10.0.0) replaced it with the live-state loop. The repro's automaton has a dead state, so it is not minimal: it was outside 9.12's documented domain, and 9.12's correct false shows the regression rather than a promise.

Over all 2,100,084 DFAs with 1 to 3 states over the labels a, b, c, compared with a brute-force oracle that does not use Lucene: 37,634 false positives (1.8%), all with dead states, and 0 false negatives (alphabet [a, c]). A reachable dead state alone is not enough: 574,233 of those automata have one, and isTotal is wrong on 37,634 of them and right on the rest. With the alphabet [b, c] (label a outside it) main gives 48,120 false positives, again all with dead states. A separate, older and conservative mode (a wrong false when a custom alphabet is narrower than the labels: 38,656 cases in the [b, c] scope, also in 9.12.0) is out of scope here; the recommended fix does not fix it and raises it to 43,466 (see the fix trade-offs).

• Trigger paths, all executed on main. A hand-built Automaton (the repro). An NFA built with Automaton.Builder and passed through Operations.determinize, which keeps its dead state (determinize returns its result without removeDeadStates, Operations.java:793-795): isTotal is true although 0 is rejected. A RegexpQuery with an AutomatonProvider that returns the repro's automaton for the named automaton <lower> (returned unchanged, RegExp.java:711-727): 3 hits instead of 2, compiled type ALL.
• Not hit, as far as checked: Lucene's own query builders. Sampling found no dead state in automata from RegExp (about 59,800 random regexps, the study), TermRangeQuery, PrefixQuery, WildcardQuery (20,000 each) and LevenshteinAutomata (120,000). Several Automata.make* builders assert there are none (Automata.java:564, 589, 609), and Operations' concatenate, union, intersection, complement, repeat and reverse call removeDeadStates on the automata they build. That is not a guarantee for every path: optional documents "This may create a dead state" (Operations.java:148), determinize returns its result without removeDeadStates (793-795), and optional, repeat, intersection and minus can return an input unchanged (155, 204, 209, 381, 393-400), so a dead state that an input already has can survive them.
• Default or opt-in. No setting is involved, but the trigger is opt-in: the application builds the automaton through the @lucene.experimental automaton API.
• Scale. None: two states, three documents.
• Silent and fail-open. No exception. This bug's wrong answer is always true ("accepts everything"): through CompiledAutomaton it becomes ALL and an AutomatonQuery over-matches, and a caller's match-all shortcut fires. Terms.intersect on that compiled automaton throws IllegalArgumentException instead (Terms.java:79-80, executed); SortedDocValues.intersect and SortedSetDocValues.intersect return every value for ALL (read).
• Downstream decisions (read in Elasticsearch main on 2026-10-26, not executed). Privilege.grantsAll is Operations.isTotal(automaton) (Privilege.java:49). FieldPermissions caches isTotal(permittedFieldsAutomaton) (FieldPermissions.java:110-112); when it is true, every field is granted (227), hasFieldLevelSecurity() is false (244-246) and filter() returns the reader unfiltered (249-253). The wildcard field mapper and the query languages' AbstractStringPattern use it as a match-all shortcut. The study found no Elasticsearch path that builds one of these automata with a dead state.
• How likely. Unknown. No prior report was found in about two years since 10.0.0, and no Lucene path that produces such an automaton is known; neither measures real-world frequency. A complete DFA with a sink is the textbook form, and Lucene's own package-private Operations.totalize builds exactly that shape ("added transitions to a dead state", Operations.java:1308-1345). It does not leak out: complement then flips every state's acceptance (351-354), so that sink becomes an accepting state of the complement, which the final removeDeadStates (356) keeps.

# Lucene main 645d4fe14a20, assertions on (-ea), seed DEADBEEF: 1 test(s) run, 1 failed
    => java.lang.AssertionError: isTotal of a DFA that rejects "0" expected:<false> but was:<true>
       org.junit.Assert.fail(Assert.java:89)
       org.junit.Assert.failNotEquals(Assert.java:835)
       org.junit.Assert.assertEquals(Assert.java:120)
       org.apache.lucene.util.automaton.TestIsTotalDeadState.testIsTotalWithReachableDeadState(TestIsTotalDeadState.java:33)

• The contract. Operations.java:838: "Returns true if the given automaton accepts all strings." 840: "The automaton must be deterministic, or this method may return false." 849-852 say the same for a min/max alphabet. The in-code comment at 861 states the rule: "all reachable states must be accept states".
• The consumers. AutomatonQuery "will match documents that contain terms accepted by a given finite-state machine" (AutomatonQuery.java:32) and "terms that are accepted are considered a match" (64, 75, 88). AUTOMATON_TYPE.ALL is the "Automaton that accepts all possible strings" (CompiledAutomaton.java:55-56).
• History. #13707 ("Relax Operations.isTotal() to work with a deterministic automaton", by rmuir, approved by dweiss and ChrisHegarty, merged 2024-09-05; CHANGES under 10.0.0: "Improve Operations.isTotal() to work with non-minimal automata") changed the javadoc from "must be minimized" to "must be deterministic". rmuir wrote that it "should work generally for any DFA, so IMO it is safe". getLiveStates(a) was already in rmuir's first coding of dweiss's idea in #13706, and the stated reason for it is that it "is easier to reason about"; the PR's randomized check later found "the situation where all states are dead states" for the draft's return a.getNumStates() > 0;, and the merged code returns seenStates > 0. In the motivating issue #13706 an earlier draft by rmuir documented "The automaton must be deterministic with no transitions to dead states" and returned false when hasDeadStatesFromInitial(a); dweiss described the rule as "a deterministic, total automaton must accept full language in each state reachable from root". The merged code dropped the guard; no comment discusses a reachable dead state next to live states. This is design context from before the bug shipped, not a report of it.
• Tests. TestOperations.testIsTotal (TestOperations.java:182-220, added by #13707) has minimal, non-minimal and "not total, but close" cases, and no automaton with a dead state.
• Dead states are legal. hasDeadStates, hasDeadStatesFromInitial and removeDeadStates are public (Operations.java:444-460, 1003-1007). Where a method cannot handle them it says so: getCommonPrefix documents and throws IllegalArgumentException "if the automaton has dead states reachable from the initial state" (1127-1134). isTotal documents nothing of the kind.
• Same language, two answers. a and removeDeadStates(a) accept the same strings, yet isTotal returns true and false. A predicate on the language cannot do that.

The strongest case for "intended" (the cross-model refute review rated it "moderate"): the CompiledAutomaton class javadoc says "For deterministic automaton, it must not have dead states but is not necessarily minimal" (CompiledAutomaton.java:36-41), AutomatonTermsEnum assumes "a DFA with no transitions to dead states" (AutomatonTermsEnum.java:297), CompiledAutomaton.java:181 says "NOTE: only approximate, because automaton may not be minimal", 9.12's isTotal documented "The automaton must be minimized", so the explicit-sink automaton was outside 9.12's domain too, the automaton API is @lucene.experimental, Lucene's own query builders produced no dead states in sampled checks, and SECURITY.md leaves untrusted input to the caller.

Why it fails: (1) the direct isTotal contract has no dead-state precondition and allows only a wrong false; (2) the "only approximate" comment predates #13707 (it is at CompiledAutomaton.java:176 in 9.12.0), when isTotal could only miss an optimization; (3) AutomatonQuery's javadoc does not repeat the CompiledAutomaton rule, and its constructor always simplifies; (4) the answer changes for the same language; (5) 9.12.x is right for the same input (an input outside 9.12's "must be minimized" precondition, so this shows the regression rather than a promise), and the rule as stated in #13706 (dweiss: "each state reachable from root") and in #13707's own code comment at Operations.java:861 ("all reachable states must be accept states") covers the sink; (6) the one-line fix keeps all 8,870 core tests passing (compatibility, not intent). Verdict: not intended, a defect in Operations.isTotal; the AutomatonQuery symptom follows from it. A maintainer may still call the AutomatonQuery input a violation of CompiledAutomaton's precondition; then AutomatonQuery's javadoc, which does not repeat the rule while its constructor always simplifies, is at least a documentation defect.

Option A was validated with gradle in a scratch worktree at ea57360912ed; option B was validated by the study on 7cecf79523; C and D were not run. Workaround today: call Operations.removeDeadStates(a) before isTotal, AutomatonQuery or CompiledAutomaton.

For a deterministic automaton whose labels lie in [min, max], the language is total exactly when every state reachable from state 0 is accepting and covers [min, max]: the rule the comment at Operations.java:861 states. The empty cases stay right: with 0 states the set is empty and seenStates > 0 is false; if no accept state is reachable, state 0 is in the set and is not accepting, so the loop returns false at once.

-    BitSet states = getLiveStates(a);
+    BitSet states = getLiveStatesFromInitial(a);

Trade-offs

• Removes every dead-state false positive: in the study's exhaustive scope, 0 false positives and 0 false negatives for labels inside the alphabet.
• Complete when every label lies inside [min, max]: always so for isTotal(a) on code-point labels and for CompiledAutomaton's isTotal(a, 0, 0xff) on a binary automaton. It does not fix the older conservative mode (narrow custom alphabets) and changes its count: in the study's [b, c] scope main gives 48,120 false positives and 38,656 false negatives, the fix 0 and 43,466. The 4,810 new answers are all a conservative false for a total language, from a dead state that can be reached only through a label outside [min, max]; no answer goes from false to true (executed). Only direct callers that pass a narrower alphabet see them; option B removes them.
• Does less work: it skips getLiveStatesToAccept, which builds a reversed copy of the automaton (Operations.java:959-1001); not benchmarked.
• An automaton with a reachable dead state now compiles to NORMAL instead of ALL: correct, and Lucene's own query builders were not seen to produce such automata.

What the checks validated

• Gradle, scratch worktree at ea57360912ed, JDK 25: 36 classes (automaton, regexp, wildcard, prefix, range, fuzzy and terms-enum tests and 5 related query classes) with the repro test: stock 406 tests, 4 failed (the 3 repro tests and the new TestOperations test); with the fix 406 tests, 0 failed (also seed 1234ABCD with assertions off).
• The whole :lucene:core:test: 8,870 tests in 748 classes, 0 failures, 322 skipped. queryparser, highlighter, monitor, queries, memory, suggest and analysis:common: 4,144 tests, all pass. checkGoogleJavaFormat passes on the diff.
• The plain program and the provider probe give the 9.12.3 answers with the fix; the cross-model reviewer's own test and 133 existing tests pass with it.

About 30 lines in isTotal: a breadth-first walk from state 0 that follows only labels inside [min, max], with each transition clipped to the alphabet before the gap check.

Trade-offs

Also fixes the conservative false negatives for narrow custom alphabets (0 oracle disagreements in both scopes): the full fix for direct callers that pass a custom alphabet. A larger change than A. The corrected specification it implements was proved sound and complete in Dafny by the study (not re-audited by the hunt).

What the checks validated

By the study on 7cecf79523 (classpath shadow, not gradle): 0 disagreements with the brute-force oracle in both scopes, and 297 tests from 24 Lucene test classes pass.

Call removeDeadStates, or skip the ALL shortcut when hasDeadStatesFromInitial(a), before isTotal.

Trade-offs

Fixes AutomatonQuery and the provider path, but not direct callers of isTotal, which is where the downstream authorization use is. Not run.

Keep the code and add the precondition.

Trade-offs

Keeps a fail-open answer in a public predicate that downstream code uses for grant-all decisions, and every 10.x release keeps it.

Method: bounded-exhaustive translation validation plus a deductive proof (the study's semi-formal tier, 2026-10-22, main 7cecf79523), in the experiment that verified org.apache.lucene.util.automaton.

• An AI tool wrote FvRef, an independent textbook semantics for automata that decides language equality, emptiness and totality exactly. It enumerated every automaton in small scopes, ran each Lucene operation on it, and compared. isTotal returned true on non-total DFAs, and every such case had a dead state (finding F2a). Dafny proved a corrected isTotal sound and complete and machine-checked counterexamples for main. The study's attribution table records it as found blind: the task did not point at this bug.
• A separate AI verifier re-derived it from scratch: a brute-force oracle over all 2,100,084 DFAs with 1 to 3 states over 3 labels (37,634 false positives, all with dead states), the end-to-end AutomatonQuery test, runs on 9.12.0, 10.0.0 and main, and two patches checked against 297 Lucene tests.
• On 2026-10-26 the hunt re-ran it on ea57360912ed, built the release matrix and the commit A/B, searched for prior reports, and had it reviewed by an independent reviewer from another model family (OpenAI GPT-5.6). For this page the fix was validated with gradle and two more trigger paths were run.