Formal models and scripts: indexingchain-schema

Tools: Alloy, 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

• The frozen-FieldType validation cache (#15886) keys a field on its first value's type, so for a field built from several field types a later document skips the per-field schema check (or is checked against stale state after a rejected addBatch), depending on value order, flushes and earlier operations (finding LFV-118; repro · finding page)
• A rejected document leaves its doc-values skip index type in the field's per-document schema state, so later valid documents with that field are rejected until the in-memory segment is flushed (finding LFV-116; repro · finding page)
• IndexWriter#addBatch marks the frozen FieldType of an earlier rejected document as validated, so later documents with that type skip the per-field schema check (a wrong-dimension vector is stored truncated) (finding LFV-127; repro · finding page)
• A failed addIndexes(Directory...) leaves the incoming fields registered in the writer's field schema, so getFieldNames() lists them and later valid documents that use those names differently are rejected until the writer is reopened (finding LFV-124; repro · finding page)

Files

• addindexes-directory-registers-schema-before-failing/model/FieldNumbersTxn.als (used for LFV-124)
• fieldschema-reset-keeps-skip-index/model/FieldSchemaCache.als (used for LFV-116)
• fieldschema-reset-keeps-skip-index/model/FieldSchemaCacheSmall.als (used for LFV-116)
• fieldschema-reset-keeps-skip-index/model/decode_m1.py (used for LFV-116)
• frozen-type-cache-promotes-rejected-type-via-addbatch/model/FieldSchemaCache.als (used for LFV-127)
• frozen-type-cache-promotes-rejected-type-via-addbatch/model/FieldSchemaCacheSmall.als (used for LFV-127)
• frozen-type-cache-promotes-rejected-type-via-addbatch/model/decode_m1.py (used for LFV-127)
• frozen-type-cache-skips-check-for-multi-type-fields/model/FieldSchemaCache.als (used for LFV-118)
• frozen-type-cache-skips-check-for-multi-type-fields/model/FieldSchemaCacheSmall.als (used for LFV-118)
• frozen-type-cache-skips-check-for-multi-type-fields/model/decode_m1.py (used for LFV-118)

How to run

• Alloy 6: open the .als file and run its commands (a counterexample found for one of its assertions is the finding).
• Python: python3 <file>.py; scripts that import z3 need the z3-solver package.

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