Module subsume 

Query subsumption: does the result set of next provably fit inside the result set of prev? When it does (and the index generation is unchanged), the engine refines the cached prev ids instead of scanning — the incremental-typing fast path.

Every rule here must be sound (false positives lose results — the one unacceptable failure mode); being incomplete merely costs a cold scan. The oracle property test in exec.rs cross-checks refine == fresh search over random names and typing sequences.

Functions

bridge_needle 🔒

Needle-domain bridge: a byte needle proven about one pool implies one about the other only in the orig→folded direction. Valid-UTF-8 needles can only match at code-point boundaries and folding is length-preserving per code point, so a name matching n at offset i guarantees the lower pool holds fold(n) at i. The reverse (folded match → original bytes) does not hold.

implies 🔒

Does a positive match of n guarantee a positive match of p?

matcher_eq 🔒

Structural equality of two compiled matchers.

subsumes

True when every entry matching next (under next_opt) is guaranteed to be present in prev’s materialized ids, in the right order.