G21 — `docs/13` §4 grants `notIn:` an index rewrite that §10.2's scoping and §7.10's table never granted

Labels: §10.2 · §7.10 · §7.5 · docs/13 §4 · docs/12 §3.3 · spec-gap Blocks: No stored byte, no derived value, no vector in any family. Prisma adapter L2: notIn: is on the §4 table as rewritable, and the adapter shipped the opposite behaviour pending this issue. Found: 2026-08-27, writing the Prisma adapter’s throw list (WS-F PR1) against docs/13 §4.

Status: CLOSED 2026-08-31 — tracker #87. Closed as filed, all four proposed steps taken: spec §7.10 gains a negated-membership/negated-equality row with the honest fallback; §10.2’s in: permission is explicitly scoped and a new All ORMs negation bullet carries the adapter obligation; docs/13 §4’s combined row splits and §2.2’s note stops citing this issue as open; docs/12’s exclude() row now points at the spec rather than reading as Django’s own rule.

No code changed in either adapter, and that is the finding worth keeping. Both already shipped the refusal — Django with the exact asymmetry argument in the message (query.py:276) and test_exclude_refuses; Prisma with does NOT lift \notIn` or `not`andexplains notIn as an exclusion asymmetry…`. The implementations were right and the specification was wrong, which is the reverse of the usual direction and the reason the conservative reading was worth shipping while the issue sat open.

Gap

docs/13 §4’s throw table lists, as one row:

| in: / notIn: with no declared index | Not rewritable — throw. With a declared index this upgrades to a rewrite (below) |

and the note beneath it describes the rewrite as emailBidx: { in: [bidx(v1), bidx(v2), …] }, citing G13’s scoping of §10.2 as the authority.

G13 scoped in: only. §10.2’s Prisma bullet, as amended:

An adapter MUST reject in: over an encrypted field unless it rewrites the predicate to the field’s declared blind index as §7.10 membership (the N index values, OR’d or as a single IN), subject to §7.5 re-verification of the candidates.

notIn appears nowhere in that clause. And §7.10’s table has no row for negated membership — it has Membership (IN) | **Yes** — N indexes OR'd, and nothing else. So docs/13 extends a permission to a shape the specification has never addressed, on the strength of a citation that does not cover it.

Why the extension is not merely unstated but wrong

The asymmetry is the one docs/12:107 already states for Django’s exclude(), and it transfers verbatim:

A filter’s false positives are recoverable; an exclusion’s false negatives are not.

Concretely. §7.4 mandates collisions: the band 2 ≤ P × 2^(−b) < √P guarantees that an index value corresponds to at least two distinct plaintexts. A positive in: therefore returns a superset of the answer, and §7.5’s re-verification pass removes the extras — the mechanism works because the surplus rows are present and can be inspected.

A negated notIn: inverts that. WHERE emailBidx NOT IN (bidx(v1), …) excludes every row in those buckets, including rows whose plaintext is not any of v1…vN and which belong in the result. Those rows are excluded by the database and never reach the adapter, so §7.5 has nothing to put back. The query silently drops correct rows, in proportion to the collision rate the spec deliberately requires.

The same argument covers Prisma’s scalar .not and any NOT-wrapped equality over an encrypted column. docs/13 §2.1 currently lists .not (scalar form) among the where-shapes the visitor rewrites, which has the same defect.

Proposed direction (starting point, not a decision)

1. §7.10 gains a row: negated membership and negated equality over a blind index — No, with the honest fallback (fetch the matches by index with in:/equality, re-verify, and exclude their primary keys in application code, or over-fetch and filter after decryption).
2. §10.2’s Prisma bullet stays scoped to in: and gains a sentence stating that the permission does not extend to notIn:, so the next adapter does not read the silence the way docs/13 did.
3. docs/13 §4’s row splits: in: rewritable with a declared index; notIn: an unconditional rejection. §2.1’s .not entry moves from the rewrite list to the rejection list.
4. Consider whether docs/12 should say the same thing explicitly rather than only in Django’s exclude() message, since the rule is not Django’s.

Justification

Spec §7.4 (truncation band, collisions mandated) and §7.5 (the index is a filter, never an answer; candidates MUST be decrypted and re-verified) together make the positive case sound and the negated case unsound, without any new citation. The Naveed–Kamara–Wright and AWS material §7.6 already cites is not needed here: this is an internal-consistency defect, not a leakage question.

What it breaks

Nothing stored, nothing derived. It removes a capability docs/13 promised and no adapter has shipped — the Prisma adapter refuses it today, and the Django adapter already refuses the analogue. If any implementation has built the rewrite, its results were wrong in proportion to P × 2^(−b).

Vector obligations

None. The rule is an adapter obligation over already-decrypted plaintext and query shapes, downstream of every cryptographic operation — the same shape as G19’s comparison rule, which docs/07 §7 records as held by per-adapter tests rather than by the suite. Per-adapter refusal tests are the executable form.

Review flag

No cryptographic review. No construction, no derivation, no stored byte, no error code. It resolves an internal contradiction between docs/13 §4 and §10.2/§7.10, and no Gate 0b question depends on it.

View source: docs/issues/G21-negated-membership-over-a-blind-index.md