`feat` PRD: Existence tests — `.exists()` on reverse and M2M relations, rendered as correlated EXISTS

[0x054]

Origin: design session for #307/#308 (2026-07-18), owner-approved — the SQL shapes in those external PRDs are requirements; the Python spelling was redesigned. Decision records: ADR-0007 (reverse relations are tested, not traversed), ADR-0006 (traversal join semantics, unchanged inside subqueries). Glossary: Existence test (CONTEXT.md). Depends on the uniform-negation PRD #310: NOT EXISTS is spelled ~t.rel.exists(). Deferred follow-up: #309 (cross-scope correlation). Closes #307 and #308 when shipped.

Problem Statement

As a ferro user I cannot filter a root query on membership in a reverse (BackRef) or many-to-many relation. Forward FK traversal works (t.account.ledger_id == lid), but the reverse direction — "transactions that appear in any transfer" (#307), "transactions whose split lines match a category" (#308) — is unspellable: reverse edges are invisible to predicates, left_join(), and in_(). The blocked Pinch M6/M8 workloads need these filters composed with every other root predicate and keyset pagination, with root-set semantics: no duplicated roots when the relation is to-many, no dropped roots on the other branch of an OR.

Solution

A reverse or M2M relation in a predicate supports exactly one verb — the existence test:

# 307: is_transfer true / false
Txn.where(lambda t: t.transfer_out.exists() | t.transfer_in.exists())
Txn.where(lambda t: ~t.transfer_out.exists() & ~t.transfer_in.exists())

# 308: line-aware category filter; child-less roots survive via the OR
Txn.where(lambda t: t.category_id.in_(ids)
                  | t.lines.exists(lambda l: l.category_id.in_(ids)))

.exists() renders as a correlated EXISTS at every cardinality and for both relation kinds. The result stays root-shaped, so it composes with any predicate, ordering, and paging. The optional inner lambda is a full ferro predicate over the related model. Reverse relations are tested, never traversed — the explicit lambda scope is what makes multi-condition grouping unambiguous, the Django-style implicit-traversal trap ADR-0007 rejects.

User Stories

1. As a Pinch backend developer, I want an is_transfer filter on the transaction list, so that spending exclusion derives from transfer membership (one EXISTS) instead of a flag that can drift.
2. As a Pinch backend developer, I want the negated form of that filter, so that is_transfer=false renders NOT EXISTS and both branches of the list filter work.
3. As a Pinch backend developer, I want a line-aware category_id filter, so that splitting a transaction never makes it less findable.
4. As a Pinch backend developer, I want existence tests to compose with keyset ordering and limit, so that the paginated list query works unchanged.
5. As an application developer, I want a to-many existence test to return each matching root exactly once, so that a transaction with three matching lines is one result row with no DISTINCT bookkeeping on my side.
6. As an application developer, I want roots without child rows to survive the other branch of an OR, so that plain transactions still match a category filter alongside split ones.
7. As an application developer, I want one verb (.exists()) at every cardinality and relation kind, so that a one-to-one BackRef, a to-many BackRef, and an M2M edge all spell the same and a schema cardinality change never breaks call-site spelling.
8. As an application developer, I want the inner lambda to be a full ferro predicate, so that I can use any operator, forward traversal, and &/|/~ inside the test without learning a sub-language.
9. As an application developer, I want forward traversal inside the subquery to keep ADR-0006 semantics, so that there is exactly one set of join rules to know.
10. As an application developer, I want nested existence tests, so that "categories with a transaction that has a negative line" is spellable to arbitrary depth.
11. As an application developer, I want an explicit grouping choice between "one child row matches all conditions" and "some child row matches each", so that multi-condition filters on the same relation are never ambiguous.
12. As an application developer migrating from the feat Reverse-relation membership predicates: EXISTS from the root query (PRD from Pinch) #307 repro, I want t.transfer_out != None to fail at build time with the supported spelling in the message, so that my first wrong guess teaches me the right one.
13. As an application developer, I want reverse-proxy column access, left_join() on a reverse edge, and in_(query) to each fail with an error naming .exists(), so that every dead end points at the exit.
14. As an application developer, I want a cross-scope reference in the inner lambda to fail loudly rather than misrender, so that the deferred capability (feat Cross-scope correlation in existence tests (deferred from ADR-0007) #309) can't silently corrupt a query.
15. As a maintainer, I want the existence-test node pinned by golden vectors, so that the Python emitter and Rust decoder cannot drift on the new wire shape.
16. As a maintainer, I want M2M carried by the same node and render loop as reverse FK, so that M2M support is test surface rather than a second mechanism.
17. As a docs reader, I want a guide section with both field-declaration styles and lambda-style examples plus rendered SQL, so that the feature is learnable from the docs alone.

Implementation Decisions

• Spelling: .exists(inner_lambda=None) is the only verb on a reverse or M2M relation in a predicate. No implicit path traversal, no .any()/.has() split, no != None/== None sugar, no in_(subquery) — all recorded with rationale in ADR-0007.
• Rendering: always a correlated EXISTS, at every cardinality (no LEFT JOIN + IS NOT NULL specialization for unique BackRefs). Root-set semantics guaranteed: the pinned "a join never multiplies root rows" property is preserved by construction.
• Reverse specs: a reverse-spec map is derived once at the existing compile choke point (beside the forward relation specs), from facts relationship resolution already computes — related model, child FK column for reverse FK, join-table triple for M2M, one-to-one flag. The predicate proxy consults it ahead of the column fallback and returns a reverse-relation proxy exposing .exists() only.
• Inner predicate: resolved through the existing predicate resolver against the related model — same operators, forward traversal (joins rendered inside the subquery under unchanged ADR-0006 semantics), nested existence tests to arbitrary depth. Cross-scope references (any proxy other than the inner lambda's parameter, or a field proxy as comparison RHS) are a build-time error pointing at feat Cross-scope correlation in existence tests (deferred from ADR-0007) #309.
• Wire: one new recursive node kind (exists {hops, where}) beside leaf/compound/not. hops reuses the existing join-hop vocabulary: one hop for reverse FK, two for M2M (join table, then target). where is an ordinary nested condition tree. QueryIR version bumps; hand-authored golden vectors pin the shapes.
• Rust render: one loop — first hop's table is the subquery FROM, correlated to the enclosing scope's alias; remaining hops render as inner joins inside the subquery; the inner tree builds through the existing condition builder recursively. Negation arrives via the NOT node from the sibling PRD; the exists node carries no negation flag.
• Error surfaces: reverse edges become recognized everywhere and accepted nowhere except .exists() — reverse-proxy column access/comparison, left_join() on a reverse edge, and in_() with a query RHS each raise naming .exists(). The include() rejection is unchanged (population stays a separate future mechanism, per the Include glossary term).

Testing Decisions

• Tests assert external behavior only: result sets at the end-to-end query seam, payload shape at the golden-vector wire seam, and error messages. No assertions on proxy or spec internals.
• End-to-end, on both database backends via the existing backend matrix, in the style of the existing per-feature query test files: both feat Reverse-relation membership predicates: EXISTS from the root query (PRD from Pinch) #307 branches (membership via either FK column, found exactly once), the feat OR-composition across a left-joined reverse child table (PRD from Pinch) #308 shape (multi-line split → one root row; child-less root survives the OR; keyset order_by + limit compose), bare vs scoped tests, one-to-one BackRef, M2M bare + scoped, forward traversal inside the subquery, depth-2 nesting, ~ over existence tests.
• Golden vectors: exists 1-hop, exists 2-hop (M2M), nested exists-in-exists, not-of-exists — asserted from both the Python emitter and the Rust decoder.
• Negative paths: every error surface above, including the cross-scope rejection and the != None bounce, pinning that each message names the supported spelling.
• Docs examples follow the repo conventions: both field-declaration styles shown, lambda predicates throughout, rendered SQL alongside.

Out of Scope

• Cross-scope correlation / column-to-column comparison — deferred to feat Cross-scope correlation in existence tests (deferred from ADR-0007) #309.
• BackRef/M2M population (include() on reverse edges) — a separate future mechanism (batched second query), unchanged by this work.
• in_(single-column ProjectedQuery) — declined, not deferred (ADR-0007).
• Aggregates over related rows ("transactions with ≥2 lines") — not requested; the existence test answers membership only.
• Planner-side optimizations (e.g. semi-join specialization for unique BackRefs).

Further Notes

Builds on the uniform-negation PRD's NOT node; land that first. When this PRD ships, #307 and #308 close (maintainer comments there record the accepted-workload/respelled-API decision). M2M was pulled into v1 scope deliberately: with the hop-path wire shape, its marginal cost is test coverage, and users will expect t.tags.exists(...) to work wherever t.lines.exists(...) does.