Formal models and scripts: bitsets-livedocs-acceptdocs

Tools: Python

These are the working models and scripts this part of the hunt used. Some encode the code as it is (a counterexample is the expected result), others a fixed or correct variant; read the header comment of each file. Paths inside them were replaced by placeholders such as $LUCENE (a Lucene checkout) and $WORK.

Findings

• ReqExclBulkScorer.WindowBits.applyMask adds offset + bitSet.length() in int, so FILTER/MUST + MUST_NOT queries silently drop every match in a 4096-doc window based at doc 2^31-4096 or above (up to the last 3,967 doc IDs of a segment near IndexWriter.MAX_DOCS) (finding LFV-139; repro · finding page)
• Lucene90LiveDocsFormat.writeLiveDocs and CheckIndex.bitsCardinality step an int offset by 1024 that wraps to Integer.MIN_VALUE for segments of more than 2,147,482,624 documents, so a deletion in such a segment can never be committed (10.4.0+) and CheckIndex at level 2 or higher reports its valid live docs as an error (10.3.0+) (finding LFV-147; repro · finding page)
• FixedBitSet.ensureCapacity computes the grown length as int arr.length << 6, which wraps negative once the requested bit reaches about 1.91 billion, so DocsWithFieldSet iterates no documents and a flushed segment silently drops every value of its sparse doc-values and norms fields (finding LFV-137; repro · finding page)
• (Latent) FixedBitSet.approximateCardinality returns a negative value for bit sets of 2^31-63 bits or more, because its scale factor 64 * numWords overflows int (finding LFV-133; repro · finding page)

Files

• fixedbitset-approximatecardinality-overflow/model/overflow_findings.py (used for LFV-133)
• fixedbitset-ensurecapacity-numbits-overflow/model/overflow_findings.py (used for LFV-137)
• livedocs-batch-offset-overflow/model/overflow_findings.py (used for LFV-147)
• reqexcl-windowbits-applymask-offset-overflow/model/overflow_findings.py (used for LFV-139)

How to run

• Python: python3 <file>.py; scripts that import z3 need the z3-solver package.

Snapshot of 2026-11-03. AI-assisted; not yet triaged by a human Lucene committer. Feedback: open an issue in lucene-ai-bug-hunt.