From f212ee2c6ac44c3e99364a95c2d9883d687264cb Mon Sep 17 00:00:00 2001 From: James Sadler Date: Mon, 20 Jul 2026 23:16:45 +1000 Subject: [PATCH] docs: handoff for the EQL v3 type checker design Captures the EQL v3 domain model, three impact maps over eql-mapper (type system, SQL surface, declarations/macros), and the open design questions, so the design session starts fresh with full context. Records one corrected finding: literals are inference sinks (value.rs:19 unifies them with a fresh tvar, not Native), so a token type on EqlValue buys no literal checking. Two subagents disagreed on this; resolved by reading the code. --- .../2026-07-20-eql-v3-type-checker-handoff.md | 397 ++++++++++++++++++ 1 file changed, 397 insertions(+) create mode 100644 docs/plans/2026-07-20-eql-v3-type-checker-handoff.md diff --git a/docs/plans/2026-07-20-eql-v3-type-checker-handoff.md b/docs/plans/2026-07-20-eql-v3-type-checker-handoff.md new file mode 100644 index 000000000..310621375 --- /dev/null +++ b/docs/plans/2026-07-20-eql-v3-type-checker-handoff.md @@ -0,0 +1,397 @@ +# EQL v3 type checker — session handoff + +**Date:** 2026-07-20 +**Branch:** `chore/agent-skills-setup` (PR #415) +**Purpose:** carry context into a fresh session for `/grill-with-docs` on extending the +EQL Mapper type checker for EQL v3. + +This is a handoff, not a spec. It records what is already true, what was already decided, +and what is still open. The design itself has not started. + +--- + +## 1. How to use this + +Open a fresh session, reference this file, and run `/grill-with-docs`. The design questions +in §8 are the agenda. Everything above them is evidence gathered so the grill does not have +to re-derive it. + +Glossaries exist and should be updated as terms get resolved: +`CONTEXT-MAP.md`, `packages/eql-mapper/CONTEXT.md`, `packages/cipherstash-proxy/CONTEXT.md`. + +--- + +## 2. Where the branch is + +Five commits, unpushed beyond #415's first. In order: + +| Commit | What | +|---|---| +| `3d33c8ed` | Agent skills config (issue tracker, domain docs) | +| `74b63721` | Domain glossaries for Proxy and EQL Mapper | +| `64c658f2` | Deps: cipherstash-client `0.34.1-alpha.4` → `0.42.0`, EQL `2.3.0-pre.3` → `3.0.1` | +| `b3f293d7` | Encrypt path moved to `encrypt_eql_v3`; v2 retired | +| `a10b60cd` | v3 decrypt for scalar + SteVec | +| `387ca790` | Adopted the 0.42.0 representation; workspace compiles | + +**State:** the workspace compiles, `cargo fmt` and `cargo clippy --all-targets` are clean. +**Nothing has been run.** Compiling is not working — `eql-mapper` still emits `eql_v2_encrypted` +casts and `eql_v2.*` calls into every rewritten statement, so nothing works end to end. +229 `eql_v2` references remain repo-wide. + +The vendored `stack-auth` CIP-3159 patch was dropped (0.42.0 requires `stack-auth ^0.42.0`, +which carries the CancelGuard fix upstream). `vendor/stack-auth/` is still on disk, unreferenced. + +--- + +## 3. The EQL v3 model + +EQL 3.0 removes the `eql_v2` schema entirely. The single opaque `eql_v2_encrypted` +**composite** type is replaced by **53 typed domains over jsonb**, two-dimensional: + +**Token type** × **capability suffix** + +- Tokens: `integer`, `smallint`, `bigint`, `date`, `timestamp`, `numeric`, `text`, + `boolean`, `real`, `double`, `json` +- Suffixes: *(none)*, `_eq`, `_ord`, `_ord_ope`, `_ord_ore`, `_match`, `_search`, `_search_ore` + +Column domains live in `public` (`public.eql_v3_integer_ord`); query-operand twins live in +`eql_v3` (`eql_v3.query_integer_ord`). 39 query twins, enumerated separately. + +Capability is a property of the **type**, and the domain's CHECK enforces that the payload +actually carries the required terms — so a missing term fails on insert, not later at query time. + +### SEM terms (the storage beneath a capability) + +| Suffix | Operators | Term | +|---|---|---| +| *(none)* | — (storage only) | `c` | +| `_eq` | `=` `<>` | `hm` (HMAC-256) | +| `_ord` | `=` `<>` `<` `<=` `>` `>=`, MIN/MAX | `op` (CLLW-OPE) | +| `_ord_ope` | as `_ord` | `op` | +| `_ord_ore` | as `_ord` | `ob` (block-ORE) | +| `_match` | `@@` | `bf` (bloom filter) | +| `_search` | all | `hm` + `op` + `bf` | +| `_search_ore` | all | `hm` + `ob` + `bf` | + +Text is the exception: `text_ord*` carries `hm` **as well as** the ordering term, because +lexicographic ORE/OPE over text is not equality-lossless. + +> **Upstream doc bug.** `eql-bindings` `src/v3/mod.rs:26` claims "`ob` for `_ord`/`_ord_ore`, +> `op` for `_ord_ope`". The generated code disagrees — `IntegerOrd` requires `op`, +> `IntegerOrdOre` requires `ob`. Trust `term_json_keys_static()`, not that module doc. + +### Vocabulary + +`EqlTrait` is a **capability**; a **SEM term** (searchable encrypted metadata) is the storage +that satisfies it. Many-to-one. Neither is an "index" — that word is reserved for a PostgreSQL +index. The EQL config JSON and `cipherstash_client`'s `ColumnConfig` still spell SEM terms +`indexes`/`IndexType`; that is a shared wire format and not ours to rename. + +--- + +## 4. Upstream facts worth knowing + +**`eql-bindings` 3.0.1** (crates.io) is generated from `eql-domains::CATALOG` by `eql-codegen` — +the same catalog that generates the SQL. Light deps (serde, serde_json, schemars, ts-rs). + +The useful part for us: + +```rust +IntegerOrd::sql_domain_static() // "public.eql_v3_integer_ord" +IntegerOrd::term_json_keys_static() // Some(&["op"]) +``` + +`v3::all()` enumerates the 53 stored domains, `all_query()` the 39 query twins. Inverting +`all()` gives a **typname → (token type, required SEM terms)** map straight from the catalog, +which cannot drift from the SQL. `sql.rs` also embeds `INSTALL_SQL`/`UNINSTALL_SQL` as consts, +which could replace the `curl` in `mise.toml`'s `eql:download`. + +**Containment is gone.** `@>`/`<@` survive only as internal blockers that raise (CIP-3517). +Fuzzy match is `@@` via `eql_v3.matches`. + +**`boolean` is storage-only by design** — no `_eq`, no `_ord`, every operator blocked, because +a two-value column leaks its distribution under any index. + +### The 0.41.1 / 0.42.0 SteVec split — UNRESOLVED + +cipherstash-client changed the v3 SteVec wire format and nothing else followed: + +| | 0.41.1 (protect-ffi, eql-bindings 3.0.1) | 0.42.0 (what Proxy now pins) | +|---|---|---| +| Document | `{v,k,i,sv}` | `{v,k,i,**h**,sv}` | +| Entry `c` | self-describing mp_base85 record | raw base85 AEAD bytes | +| Key material | per entry | once, in `h` | +| Nonce / AAD | data key IV | `selector[..12]` / all 16 selector bytes | + +EQL 3.0.1's SQL CHECK accepts **both** (it never forbids extra keys), so the database will not +catch a mismatch. ProtectJS and Proxy writing encrypted jsonb to the same table would produce +mutually undecryptable documents. Either Proxy pins back to 0.41.1 or protect-ffi and +eql-bindings move forward. Not Proxy's call alone. **This is orthogonal to the type checker +work but blocks shipping.** + +### CLLW-ORE data is stranded + +`from_v2` returns `UnconvertibleOreTerm` for `oc` SteVec entries — re-encryption is the only +path. `cipherstash-config` now models this: `IndexType::SteVec { mode }` where +`SteVecMode::Compat` (CLLW-OPE, `op`) is the default and v3-compatible, and `SteVecMode::Standard` +(CLLW-ORE, `oc`) is documented upstream as "the legacy v2 protocol, still used by Proxy". +This is CIP-3233 made explicit in the config model. + +--- + +## 5. Impact map — the type system + +Three parallel agents surveyed `eql-mapper`. Findings, with the conflicts resolved. + +### Where encrypted types come from + +**Only two production sites** construct an `EqlValue` from schema data: + +- `inference/unifier/types.rs:508-517` — `Projection::new_from_schema_table` +- `inference/infer_type_impls/insert_statement.rs:40-49` — INSERT target columns + +Both produce `EqlTerm::Full`. Everything else clones. Upstream of both: +`packages/cipherstash-proxy/src/proxy/schema/manager.rs:142-148`, which matches the single +string `"eql_v2_encrypted"` and hardcodes `EqlTraits::all()`. **That one match arm is where the +53-domain mapping has to go.** + +### The shapes that must widen + +- `EqlValue(TableColumn, EqlTraits)` — `unifier/types.rs:274` +- `ColumnKind::{Native, Eql(EqlTraits)}` — `model/schema.rs:41-45` +- `Column::eql(name, features)` — `model/schema.rs:48` +- `SchemaTableColumn` — `model/schema.rs:63` + +There is **no field anywhere in eql-mapper holding a plaintext scalar type for an encrypted +column.** The `_ord` half of `eql_v3_integer_ord` is derivable from `EqlTraits`; the `integer` +half is derivable from nothing in the package. + +### Two authorities on the scalar type, no reconciliation + +The scalar type already exists in the system as `ColumnType`, sourced from the **encrypt config** +and consumed at `cipherstash-proxy/src/postgresql/data/from_sql.rs:123-292` and +`context/column.rs:68-86`. Under v3 the **Postgres type name** also encodes it. A config/schema +disagreement is currently undetectable. + +### Encrypted columns never unify with each other + +`unifier/types.rs:121` — *"An encrypted column never shares a type with another encrypted column."* +`unify_types.rs:84-121`: two EQL terms unify iff their `EqlValue`s are `==`, so `TableColumn` +identity dominates. `users.email = orders.email` is already a type error. + +**Therefore a token type is redundant for `Full`/`Full` unification.** Same column → same token +type, always. + +### Literals are inference sinks — CORRECTED FINDING + +Two agents disagreed here; resolved by reading the code. + +`infer_type_impls/value.rs:19` — a non-placeholder literal unifies with `self.fresh_tvar()`, +an **unbound variable**, not `Native`. And `(Eql, Native)` is a hard error +(`unify_types.rs:68-70`). + +So `WHERE encrypted_col = 'literal'` works because the literal has no type of its own and +**absorbs the column's**. Consequence: adding a token type to `EqlValue` buys **zero** literal +checking — there is nothing for `eql_v3_integer_ord = 'abc'` to contradict. Getting that check +would require literals to carry a syntactic type they deliberately do not have. + +This is not the same as "Native satisfies all bounds". That escape hatch +(`unifier/eql_traits.rs:279`) is about **bound satisfaction**, not cross-kind unification. + +### Bound checking is dead code today + +`Unifier::satisfy_bounds` (`unifier/mod.rs:235-248`) and `Type::must_implement` +(`unifier/types.rs:451-460`) can never fail in production, because: + +- every column gets `EqlTraits::all()` (`manager.rs:146`) +- `Native` ⇒ `ALL_TRAITS` (`eql_traits.rs:279`) +- `Type::Var` short-circuits to `Ok(())` (`mod.rs:236`) + +**Two latent bugs will become user-visible the moment these go live:** + +1. `EqlTraits::difference` (`eql_traits.rs:223-231`) is implemented as **XOR**, not set + difference. `UnsatisfiedBounds` will report the symmetric difference — listing traits the + type *has* but the bound never required. +2. `must_implement` (`types.rs:456`) passes its operands **reversed** relative to + `satisfy_bounds` (`mod.rs:245`). Harmless only because XOR is commutative. + +Fix both before making bounds reachable. + +### Associated types + +`AssociatedTypeSelector { eql_trait, type_name }` (`types.rs:236`) is keyed on +`(EqlTrait, &'static str)` only. Resolution (`eql_traits.rs:56-115`) maps +`Eq::Only`/`Ord::Only`/`Contain::Only` → `Partial`, `TokenMatch::Tokenized` → `Tokenized`, +`JsonLike::{Path,Accessor}` → `JsonPath`/`JsonAccessor`. + +**If the token type lives inside `EqlValue`, this machinery needs no change** — every arm does +`eql_col.clone()`, so it propagates free. Do **not** add a field to `AssociatedTypeSelector`: +it would break the `lhs.selector == rhs.selector` equality at `unify_types.rs:160` for a +dimension already determined by `impl_ty`. + +--- + +## 6. Impact map — the SQL surface + +### The entire v2 SQL surface is three call sites + +Six rules, composed at `type_checked_statement.rs:153-160`. Only three emit SQL. + +**`helpers.rs:6-27`** — `cast_as_encrypted`. The single source of every +`::JSONB::eql_v2_encrypted` cast. Takes **only** an `ast::Value` — no `EqlTerm`, no +`TableColumn`, no traits. The cast target is a hardcoded `Ident::new("eql_v2_encrypted")` +at line 17. **This is the one place the v3 domain name would be chosen.** + +**`cast_params_as_encrypted.rs:51`** — emits `$1::JSONB::eql_v2_encrypted`. Its gate at line 67 +matches `Some(Type::Value(Value::Eql(_)))` — **the `EqlTerm` is available and discarded by the +`_`, one line before use.** That is the hook for selecting a `query_` twin. + +**`cast_literals_as_encrypted.rs:33`** — emits `''::JSONB::eql_v2_encrypted`. Gated +on map membership, not type. Holds **no `node_types` field at all** (line 13), so it cannot see +type info even in principle. Needs plumbing, not just a pattern change. + +**`rewrite_standard_sql_fns_on_eql_types.rs:59-61`** — blindly prepends `eql_v2` to any +`pg_catalog.*` name. Emits `eql_v2.{count,min,max,jsonb_path_query,jsonb_path_query_first, +jsonb_path_exists,jsonb_array_length,jsonb_array_elements,jsonb_array_elements_text}`. +Note it emits `eql_v2.count`, which **is not in the declaration table** — a name the type +registry cannot round-trip. + +**`rewrite_containment_ops.rs:54-57,86-87`** — `@>` → `eql_v2.jsonb_contains`, +`<@` → `eql_v2.jsonb_contained_by`. Motivated by GIN index usage, not just type dispatch. + +`preserve_effective_aliases.rs` and `fail_on_placeholder_change.rs` emit nothing. + +### Rules that exist only because v2 had one opaque type + +`RewriteStandardSqlFnsOnEqlTypes` — PG cannot dispatch `min`/`max`/`jsonb_*` on one opaque +jsonb-backed type, so they are shadowed by hand-written `eql_v2.` overloads. Under v3, PG +resolves overloads by argument type natively — **but only if v3 ships operator/function +overloads bound to those domains.** Redundant *conditional on* that, and that is overload +resolution, not capability-in-the-type. Different mechanisms; verify before assuming. + +`RewriteContainmentOps` — same root cause: `@>` cannot be defined on a bare opaque type +without conflicting with jsonb's own operator. + +**Not in this category:** the two cast rules (still needed, only the target changes), +`PreserveEffectiveAliases` (projection naming, orthogonal), `FailOnPlaceholderChange` (assertion). + +### Discipline to preserve + +`rewrite_containment_ops.rs:92-99` uses `mem::replace` against a throwaway `Value::Null` rather +than cloning, specifically so operand `NodeKey` identity survives for the cast rules that run +after it. **Clone there and literal encryption inside containment expressions silently breaks.** + +--- + +## 7. Impact map — declarations and macros + +### Operator → EqlTrait, in full (`inference/sql_types/sql_decls.rs:16-31`) + +| Operator | Signature | Trait | +|---|---|---| +| `=` `<>` | `(T op T) -> Native` | `Eq` | +| `<` `<=` `>` `>=` | `(T op T) -> Native` | `Ord` | +| `->` `->>` | `(T op ::Accessor) -> T` | `JsonLike` | +| `@>` `<@` | `(T op T) -> Native` | `Contain` | +| `~~` `!~~` `~~*` `!~~*` | `(T op ::Tokenized) -> Native` | `TokenMatch` | + +No `@@` is declared. Anything unlisted falls to `Fallback`, which forces lhs, rhs and result +to `Type::native()` (`sql_binary_operator_types.rs:40-44`). + +Functions at `sql_decls.rs:58-79`: `min`/`max` require `Ord`; the `jsonb_*` family requires +`JsonLike`; `jsonb_array`/`jsonb_contains`/`jsonb_contained_by` require `Contain`; **`count` +has no bound at all** and accepts any `T` including EQL. + +### The macro grammar is capability-only by construction + +`eql-mapper-macros/src/parse_type_decl.rs:11-25` — the entire custom-keyword vocabulary is +`Accessor, Contain, EQL, Eq, Full, JsonLike, Native, Only, Ord, Partial, Path, SetOf, TokenMatch`. +Every one is a trait name, an associated-type name, or a type constructor. **Not one names a +data type.** + +`EQL(customer.age: Ord)` is expressible. "Encrypted integer with Ord" is not — not in the +keyword table, not in the grammar, not in the generated `EqlValue`. A v3 port needs a new +lexical class, new productions in `EqlTerm` (`:289-331`) and `VarDecl` (`:70-91`), and a +widened payload. Work is concentrated in that one file. + +`@@` will not parse today: `token::At` at `:480` unconditionally expects a following `Gt`. + +### Things that become ambiguous with a token type + +1. **`(T = T)` — the core ambiguity.** One tvar currently conflates *same column*, *same + token type*, and *any encrypted*. Indistinguishable today because encrypted identity **is** + the column. +2. **`EqlTerm::Partial`'s union-on-unify** (`unify_types.rs:91`) accumulates capabilities + monotonically. If capability is fixed by the domain, you cannot union your way into a + capability the column does not have. +3. **The payload-less variants** — `JsonAccessor`, `JsonPath`, `Tokenized` all return + `EqlTraits::none()` (`eql_traits.rs:320-322`). "A tokenized *what*" needs answering. +4. **`Native` ⇒ `ALL_TRAITS`** and **`Type::Var` ⇒ `Ok(())`** are two independent wildcards in + the bound checker. + +### Pre-existing gaps this work will expose + +- **`Expr::Like`/`ILike` bypass the trait system entirely.** `infer_type_impls/expr.rs:115-131` + only unifies the result with `Native` — never requires `TokenMatch`, never produces a + `Tokenized` term. The `~~` declarations fire only on the operator form. LIKE on an encrypted + column is currently unchecked. +- **`schema_delta.rs:447,479,529` uses `EqlTraits::default()`** (all false) while the loader uses + `all()` (all true). The two paths disagree. Invisible while bounds are dead. +- **Empty projections** return `EqlTraits::none()` (`eql_traits.rs:310`) while the + `satisfy_bounds` doc (`mod.rs:220`) says they satisfy all bounds. Doc and code disagree. +- `EqlTrait` parse error string (`parse_type_decl.rs:172`) is stale — omits `Contain`. + +### Removing `Contain` touches + +Keyword table (`parse_type_decl.rs:13`), enum (`eql_traits.rs:23`), assoc types (`:39`), +resolution (`:73`, `:101-105`), `ALL_TRAITS` (`:154`), struct field (`:145`), `add_mut` (`:200`), +`to_eql_trait_impls!` (`schema.rs:225-227`), two operators (`sql_decls.rs:25-26`), three +functions (`sql_decls.rs:76-78`). + +--- + +## 8. Open design questions — the grill agenda + +**The framing question.** The research says the token type's job is **naming a v3 domain at +cast time**, not type checking: it is redundant for unification (§5), and it buys no literal +checking (§5). So — does it belong in the type lattice at all, or should the transformation +rules look the domain up from the schema by `TableColumn` at emit time and leave the lattice +alone? The second is materially cheaper and nothing found so far rules it out. **Settle this +before anything else; most other answers follow from it.** + +Then: + +1. If it does go in the lattice: inside `EqlValue` (associated types come free, all six + unification arms come free) or on `EqlTerm` (six explicit merges)? +2. `_ord` vs `_ord_ope` vs `_ord_ore` — identical operators, different SEM terms. Does the type + checker distinguish them, or is that purely a cast-target concern? +3. `integer_eq` and `bigint_eq` are byte-identical on the wire but different domains. Type error + to compare? (Note: already a type error via `TableColumn` identity — is that enough?) +4. What replaces `Contain`? `@>`/`<@` are **directional**; `@@`/`eql_v3.matches` is **symmetric**. + `<@` has nowhere to go. Delete the trait, or repoint at `@@` and lose direction? +5. Do bounds go live? Real errors for `ORDER BY` on an `_eq` column — but the domain CHECK + catches it anyway, and `sql_decls.rs:49` states the existing philosophy is *"let the database + do its job."* Does v3 change that stance? +6. Params must cast to `eql_v3.query_` twins, not the stored domain. Does the mapper need + the query inventory too, or can the twin name be derived by prefixing? +7. Which authority owns an encrypted column's scalar type — `pg_type` or the encrypt config? + Should the other be cross-checked? +8. Does `eql-bindings` become a dependency of `eql-mapper` (inverting `all()` into a + typname → capability map), or does the mapper keep its own table? + +### Prerequisites, whatever the design + +- Fix `EqlTraits::difference` XOR bug and the reversed `must_implement` operands **before** + bounds become reachable. +- Reconcile `schema_delta.rs`'s `default()` with the loader's `all()`. +- Verify whether EQL 3 ships operator/function overloads bound to the domains — that alone + decides whether `RewriteStandardSqlFnsOnEqlTypes` retires. + +--- + +## 9. Related memory + +`~/.claude/projects/-Users-jamessadler-cipherstash-proxy/memory/`: +`eql-3-upgrade-in-flight.md`, `cip-3233-client-038-ore-cllw-break.md`, +`proxy-222-stackauth-15min-auth-bug.md`.