chore(3vl): pushdown/3VL consistency test + doc follow-ups

docs/internals/iso-gql-gaps.md

@@ -140,6 +140,16 @@ Hoy `.save` es la única primitiva de "commit"; entre saves la sesión acumula R
 
 Cuando hay overlay no vacío, `lookup_node_eq` y `lookup_node_range` retornan `None` y el caller hace scan. Mantener hash y btree incrementales durante DML cuesta O(log N) por mutación; cabe en MVP-2.
 
+#### 3.4 Excepciones de datos ISO (hard-fail) vs modelo empty-output
+
+froGQL realiza un **error de tipo** como *salida vacía* (fila descartada en `WHERE`, celda null en `RETURN`) — el modelo FPPC "type errors yield empty outputs". ISO/IEC 39075 exige, en casos concretos, una **`data exception` que aborta el request** (ejecución "unsuccessful", sin efecto), no un vaciado silencioso. Es una divergencia pre-existente en todo el motor, no algo del trabajo de 3VL (que la *reduce*: al leer propiedades ausentes como null, menos cosas caen a la ruta de error). Un solo *workstream* futuro, en orden de leverage:
+
+1. **Error de tipo *esencial* → hard-abort (`22G12`)**. Hoy un mismatch de operador (`x.age + 'a'`, `false OR <string>`) es un *warning* del typechecker (no bloquea) y a runtime vacía. Escalar esos warnings a *errores* haría que la ruta con typecheck falle en compilación (conforme ISO), dejando `--no-typecheck` como escape. Entrada más barata; ojo con el override de `cod` de OR/AND que suprime el warning cuando un lado es Bool.
+2. **Tipos materiales (`NOT NULL`)**. Leer una propiedad declarada material cuyo valor es null → `22G12`; `null AS T NOT NULL` → `22G03`. Requiere trackear nulabilidad en el esquema; hoy todo es nullable-by-default (ver *Null semantics* en `CLAUDE.md`).
+3. **Validación de propiedad en grafo cerrado**. Un nombre de propiedad desconocido sobre un tipo cerrado (`x.eml`) debería ser error en *preparación* (ISO); hoy tipa lenientemente.
+
+Nota relacionada — **`IN` es una extensión de froGQL**: ISO GQL no tiene predicado de membresía `x IN [lista]` (usa `IN` solo para `FOR v IN …` / `LET … IN …`); FPPC omite listas por completo. La 3VL de `IN` en `eval_binop` es consistente con la expansión SQL `x=a OR x=b OR …` (`null IN […] → null`; encontrado → true; no-encontrado con null en la lista → null), pero es no-estándar, como `NODES`/`EDGES`.
+
 ## Cobertura LDBC Interactive Complex (IC)
 
 Estado de los 14 IC del benchmark cross-system (`bench/ldbc-queries/ic*.toml`). "Implementado" = el query corre por el motor y produce filas; la verificación de equivalencia de filas vive en `bench/cross-system/`.

src/runtime/engine.rs

@@ -4121,7 +4121,10 @@ impl<'g, G: GraphAccess + 'g> Runtime<'g, G> {
             BinOp::Eq => ExprResult::Success(Value::Bool(lv == rv)),
             BinOp::Ne => ExprResult::Success(Value::Bool(lv != rv)),
             // 3VL membership: `null IN xs` -> null; found -> true; not found but
-            // the list carries a null -> null (unknown); else false.
+            // the list carries a null -> null (unknown); else false. NB: `IN` as
+            // a membership predicate is a froGQL extension — neither ISO GQL nor
+            // FPPC has it; this matches the SQL `x=a OR x=b OR …` expansion. See
+            // docs/internals/iso-gql-gaps.md §3.4.
             BinOp::In => match rv {
                 Value::List(items) => {
                     if lv.is_null() {

src/runtime/mod.rs

@@ -16,6 +16,20 @@ use crate::syntax::expr::BinOp;
 /// `Eq`/`Ne` only — ordering on composite values is not defined here and
 /// returns false. Shared between the LTJ filter loop and the standard
 /// node/edge scan.
+///
+/// This returns a bare keep/drop `bool`, NOT the 3VL value the interpreter's
+/// `eval_binop` returns (`Null` for a null operand). That is sound because the
+/// value-predicate pushdown only lifts top-level positive `attr op literal`
+/// AND-conjuncts, where a null operand means "drop" under both (`false` here;
+/// `Null` → `get_bool` false there) — so they never disagree on which rows
+/// survive. Pushing a conjunct out of an `OR` / under a `NOT` is already
+/// forbidden (wrong for non-null rows too), and those keep-despite-null shapes
+/// stay on the residual 3VL path. Pinned by `tests/pushdown_null_test.rs`.
+///
+/// UNIFY TRIGGER: if a pushed comparison's *value* is ever consumed as
+/// something other than keep/drop (e.g. a future computed-column pushdown that
+/// feeds a projection / `CASE`), replace this with a shared 3VL core —
+/// `cmp_3vl(..) -> Value` — and make this a `matches!(.., Bool(true))` wrapper.
 pub fn cmp_values(lhs: &Value, op: BinOp, rhs: &Value) -> bool {
     use std::cmp::Ordering;
     if lhs.is_null() || rhs.is_null() {

tests/pushdown_null_test.rs

@@ -0,0 +1,140 @@
+//! Pushdown / 3VL consistency.
+//!
+//! The interpreter (`eval_binop`) yields `Value::Null` for a null-operand
+//! comparison; the pushdown path (`cmp_values`, used by the LTJ `NodeAttrCmp`
+//! filter and the standard scan) yields `false`. These *look* divergent but
+//! must produce identical rows, because the value-predicate pushdown only lifts
+//! top-level positive `attr op literal` AND-conjuncts — where a null/missing
+//! operand means "drop the row" under both (`false`→drop; `Null`→get_bool
+//! false→drop). The keep-despite-null cases (`… OR true`, `NOT (…)`) are never
+//! pushed and stay on the 3VL interpreter.
+//!
+//! This suite pins that invariant. It fails if the optimizer ever pushes a
+//! non-conjunct (out of an OR / under a NOT — a bug for non-null rows too), or
+//! if `cmp_values` and `eval_binop` drift apart on the keep/drop decision.
+
+use frogql::compile_query;
+use frogql::model::graph::MemoryGraphStore;
+use frogql::model::value::Value;
+use frogql::runtime::engine::Runtime;
+use frogql::runtime::result::QueryResult;
+
+/// Three N-nodes: a=5, a=6, and one with `a` absent (reads as null).
+fn nodes() -> MemoryGraphStore {
+    MemoryGraphStore::from_json_str(
+        r#"{"nodes":[
+            {"id":"p5","labels":["N"],"props":{"name":"p5","a":5}},
+            {"id":"p6","labels":["N"],"props":{"name":"p6","a":6}},
+            {"id":"pN","labels":["N"],"props":{"name":"pN"}}
+        ],"edges":[]}"#,
+    )
+    .unwrap()
+}
+
+/// Same three nodes, each with one outgoing edge to a shared sink — so a pushed
+/// `x.a <op> literal` filter runs inside the LTJ `NodeAttrCmp` path, not the
+/// plain node scan.
+fn nodes_with_edges() -> MemoryGraphStore {
+    MemoryGraphStore::from_json_str(
+        r#"{"nodes":[
+            {"id":"p5","labels":["N"],"props":{"name":"p5","a":5}},
+            {"id":"p6","labels":["N"],"props":{"name":"p6","a":6}},
+            {"id":"pN","labels":["N"],"props":{"name":"pN"}},
+            {"id":"s","labels":["S"],"props":{"name":"s"}}
+        ],"edges":[
+            {"id":"e5","labels":["E"],"props":{},"endpoints":["p5","s"],"directionality":"->"},
+            {"id":"e6","labels":["E"],"props":{},"endpoints":["p6","s"],"directionality":"->"},
+            {"id":"eN","labels":["E"],"props":{},"endpoints":["pN","s"],"directionality":"->"}
+        ]}"#,
+    )
+    .unwrap()
+}
+
+fn names(g: &MemoryGraphStore, q: &str) -> Vec<String> {
+    let query = compile_query(q).expect("compile");
+    let mut ns: Vec<String> = match Runtime::new(g).run_query(&query, 0) {
+        QueryResult::Projected(rs) => rs
+            .into_iter()
+            .map(|r| match &r[0] {
+                Value::Str(s) => s.clone(),
+                other => panic!("expected Str, got {other:?}"),
+            })
+            .collect(),
+        other => panic!("expected projected rows, got {other:?}"),
+    };
+    ns.sort();
+    ns
+}
+
+fn v(xs: &[&str]) -> Vec<String> {
+    xs.iter().map(|s| s.to_string()).collect()
+}
+
+#[test]
+fn test_pushed_scan_filters_are_3vl_consistent() {
+    let g = nodes();
+    // pushed vs reversed (same logical comparison, possibly different path)
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE x.a = 5 RETURN x.name"),
+        v(&["p5"])
+    );
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE 5 = x.a RETURN x.name"),
+        v(&["p5"])
+    );
+    // <> drops the missing-property row (null <> 5 = unknown -> drop)
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE x.a <> 5 RETURN x.name"),
+        v(&["p6"])
+    );
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE 5 <> x.a RETURN x.name"),
+        v(&["p6"])
+    );
+    // ordering + range-fold (btree) path — nulls not indexable -> excluded
+    assert!(names(&g, "MATCH (x:N) WHERE x.a > 100 RETURN x.name").is_empty());
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE x.a >= 5 RETURN x.name"),
+        v(&["p5", "p6"])
+    );
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE x.a IS NULL RETURN x.name"),
+        v(&["pN"])
+    );
+}
+
+#[test]
+fn test_keep_despite_null_stays_residual_not_pushed() {
+    let g = nodes();
+    // `= 999` must NOT be lifted out of the OR: `_ OR true` keeps every row.
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE x.a = 999 OR true RETURN x.name"),
+        v(&["p5", "p6", "pN"]),
+    );
+    // NOT over a comparison stays residual: missing -> NOT(null=5)=null -> drop.
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE NOT (x.a = 5) RETURN x.name"),
+        v(&["p6"])
+    );
+    // OR of two pushable conjuncts is still a residual OR, not two pushed filters.
+    assert_eq!(
+        names(&g, "MATCH (x:N) WHERE x.a = 5 OR x.a = 6 RETURN x.name"),
+        v(&["p5", "p6"]),
+    );
+}
+
+#[test]
+fn test_pushed_ltj_filters_are_3vl_consistent() {
+    // Same predicates, but with an edge so the filter runs in the LTJ
+    // `NodeAttrCmp` path (which calls the same `cmp_values`).
+    let g = nodes_with_edges();
+    assert_eq!(
+        names(&g, "MATCH (x:N)-[:E]->(s) WHERE x.a = 5 RETURN x.name"),
+        v(&["p5"]),
+    );
+    assert_eq!(
+        names(&g, "MATCH (x:N)-[:E]->(s) WHERE x.a <> 5 RETURN x.name"),
+        v(&["p6"]), // missing-a row dropped, exactly as the scan path
+    );
+    assert!(names(&g, "MATCH (x:N)-[:E]->(s) WHERE x.a > 100 RETURN x.name").is_empty(),);
+}