contract: normalize_kleene returns WhereSet (WHERE-terminal only); GKAT Where/Check negation duality pinned

.claude/board/entries/2026-10-21-d-rft-0-kleene-normalization.md

@@ -68,3 +68,12 @@ Without a server the example prints `SKIP` and exits 0.
   - empty / all-NULL `SUM` (the `SumFamily::Sym` path exists; no PostgreSQL differential yet);
   - `COUNT(expr)` vs `COUNT(*)`.
 - **Not done:** a PostgreSQL arm in CI. The example is a lab instrument only.
+
+## Correction: WHERE-terminal admission (post-merge review)
+
+Written by `session_013z2e1YXkm6o6HNrDn5BPWA` on the operator's instruction (EXO-50 `/038`), from `GPT:gpt-ada-01/20261021-pr1674-1682-consolidated-review-01` item 3.
+
+- `normalize_kleene` keeps the TRUE rows only; #1677 measured FALSE rows moving on 337/2000. It now returns `set_algebra::WhereSet` instead of a `SetExpr`. `where_true()` / `into_where_true()` name the WHERE-only restriction at every call site; `normalize_with` is private, so the Kleene result cannot leave the module as a plain `SetExpr`. `set_rules`' `SetNormalize` (a measure, terminal) and the two PostgreSQL examples take the set out explicitly. No new rule or framework; the existing `Semantics::truth` gate is unchanged.
+- Test `the_kleene_form_preserves_true_rows_but_not_false_rows`: `p ∧ ¬p` with `p` UNKNOWN keeps its (empty) TRUE rows, becomes `Empty`, and `NOT` over it is TRUE where `NOT (p ∧ ¬p)` is UNKNOWN.
+- GKAT (#1679): `Cond::Not` negates a projected guard. `tests/k3_negation_duality.rs` checks on all four atoms (TRUE, FALSE, NULL under both payloads) that `Where(NOT p) = NOT Check(p)`, `Check(NOT p) = NOT Where(p)`, that `NOT Where(p)` differs from SQL `WHERE NOT p` exactly on the two NULL atoms, and that no form reads a NULL payload. Two disables red (`Where` or `Check` without the validity test). The GKAT algorithm is unchanged; `flow.rs` docs name the boundary.
+- Unchanged after the change: contract 1626 tests pass; `k3_pg_parity` 2000/2000; `k3_where_pg_parity` TRUE/FALSE equal 2000/2000, FALSE moved on 337, two-valued wrong on 499.

crates/gkat-probe/src/flow.rs

@@ -43,6 +43,13 @@
 //!
 //! A Boolean observable is read with [`Cond::Is`]. Using a K3 projection on a
 //! Boolean observable, or `Is` on a K3 one, is refused.
+//!
+//! [`Cond::Not`] negates a guard AFTER projection; there is no SQL `NOT`
+//! before projection in this language. The two meet through
+//! `Where(NOT p) = NOT Check(p)` and `Check(NOT p) = NOT Where(p)`, so
+//! `Cond::Not(Where(p))` is SQL `CHECK(NOT p)`, not `WHERE NOT p`; a
+//! translator that lowers SQL `WHERE NOT p` must emit
+//! `Cond::Check(p).negated()` (`tests/k3_negation_duality.rs`).
 
 use crate::expr::{Action, Atoms, BExp, Exp, Refusal};
 

crates/gkat-probe/tests/k3_negation_duality.rs

@@ -0,0 +1,87 @@
+//! The SQL-negation / projection boundary of the K3 encoding (#1679).
+//!
+//! `Cond::Not` is Boolean negation of a guard that is already projected. SQL
+//! `NOT` acts on the K3 value before projection. With `Where(p) = valid ∧ leaf`
+//! and `Check(p) = ¬valid ∨ leaf` the two meet only through the duality
+//!
+//! * `Where(NOT p) = NOT Check(p)`
+//! * `Check(NOT p) = NOT Where(p)`
+//!
+//! so `Cond::Not(Where(p))` is SQL `CHECK(NOT p)`, never SQL `WHERE NOT p`;
+//! they differ exactly where `p` is UNKNOWN. Checked on all four atoms of one
+//! observable: TRUE `(1,1)`, FALSE `(0,1)`, and NULL under both payloads.
+
+use gkat_probe::Atom;
+use gkat_probe::flow::{Cond, Kind, Signature};
+
+const P: &str = "p";
+
+fn sig() -> Signature {
+    Signature {
+        observables: vec![(P, Kind::K3)],
+        actions: vec![],
+    }
+}
+
+/// (leaf, valid) bits: test 0 is the leaf, test 1 its validity.
+const T: Atom = Atom(0b11);
+const F: Atom = Atom(0b10);
+const NULL_0: Atom = Atom(0b00);
+const NULL_1: Atom = Atom(0b01);
+const ATOMS: [Atom; 4] = [T, F, NULL_0, NULL_1];
+
+/// SQL semantics of the K3 value of `p` on an atom: `None` is UNKNOWN.
+fn k3(a: Atom) -> Option<bool> {
+    a.holds(1).then(|| a.holds(0))
+}
+
+fn eval(c: Cond) -> [bool; 4] {
+    let g = sig().guard(&c).expect("guard");
+    ATOMS.map(|a| g.eval(a))
+}
+
+/// FAILS IF: the translator's negation is taken for SQL negation, or a
+/// projection reads a NULL payload. Each side is compared with the SQL
+/// meaning computed from `k3`, not with the other side.
+#[test]
+fn negating_a_projection_is_the_dual_projection_of_the_sql_negation() {
+    // SQL meanings, per atom.
+    let where_not_p = ATOMS.map(|a| k3(a).map(|b| !b) == Some(true));
+    let check_not_p = ATOMS.map(|a| k3(a).map(|b| !b) != Some(false));
+    assert_eq!(where_not_p, [false, true, false, false]);
+    assert_eq!(check_not_p, [false, true, true, true]);
+
+    // The only spellings of the SQL forms in the flow language.
+    assert_eq!(
+        eval(Cond::Check(P).negated()),
+        where_not_p,
+        "Where(NOT p) = NOT Check(p)"
+    );
+    assert_eq!(
+        eval(Cond::Where(P).negated()),
+        check_not_p,
+        "Check(NOT p) = NOT Where(p)"
+    );
+
+    // Boolean NOT of WHERE is not SQL WHERE NOT: they differ on both NULL atoms
+    // and nowhere else.
+    let not_where = eval(Cond::Where(P).negated());
+    let differs: Vec<Atom> = ATOMS
+        .iter()
+        .zip(not_where.iter().zip(where_not_p.iter()))
+        .filter(|(_, (a, b))| a != b)
+        .map(|(atom, _)| *atom)
+        .collect();
+    assert_eq!(differs, vec![NULL_0, NULL_1]);
+
+    // Payload blindness under NULL, for every form above.
+    for c in [
+        Cond::Where(P),
+        Cond::Check(P),
+        Cond::Where(P).negated(),
+        Cond::Check(P).negated(),
+    ] {
+        let v = eval(c.clone());
+        assert_eq!(v[2], v[3], "{c:?} reads the payload of a NULL");
+    }
+}

crates/lance-graph-contract/examples/k3_pg_parity.rs

@@ -203,7 +203,7 @@ fn main() {
             "SELECT count(*) FILTER (WHERE {}), count(*) FILTER (WHERE {}), \
              count(*) FILTER (WHERE {}) FROM t;\n",
             sql(e),
-            sql(&normalize_kleene(e)),
+            sql(normalize_kleene(e).where_true()),
             sql(&normalize(e))
         ));
     }
@@ -257,7 +257,7 @@ fn main() {
         assert_eq!(n[1], n[0], "normalize_kleene changed the count: {e:?}");
         kleene_ok += 1;
         two_valued_wrong += usize::from(n[2] != n[0]);
-        rewritten += usize::from(normalize_kleene(e) != *e);
+        rewritten += usize::from(normalize_kleene(e).where_true() != e);
     }
     println!(
         "PostgreSQL {}: {EXPRS} expressions over {ROWS} rows; as written = Kleene oracle = \

crates/lance-graph-contract/src/set_algebra.rs

@@ -70,6 +70,16 @@
 //! TRUE). A [`SetExpr::Sym`] is two-valued by definition, so its complement
 //! rule stays.
 //!
+//! **WHERE-terminal only.** The Kleene form keeps the TRUE rows and nothing
+//! else: it may move a row between FALSE and UNKNOWN. `p ∧ ¬p` becomes
+//! `Empty`, which is FALSE on a row where `p` is UNKNOWN, so `NOT` over the
+//! result selects that row while `NOT (p ∧ ¬p)` does not (PostgreSQL agrees;
+//! `examples/k3_where_pg_parity.rs` measures it). The result is therefore a
+//! [`WhereSet`], not a [`SetExpr`]: a consumer that negates or embeds it must
+//! take the set out explicitly with [`WhereSet::into_where_true`], which names
+//! the restriction at the call site. A measure (`Count`, `Sum`) and a SQL
+//! `WHERE` are terminal and may.
+//!
 //! An interval is always emitted as `<` / `>` bounds or one `==`.
 //!
 //! Zero dependencies.
@@ -197,13 +207,37 @@ pub fn normalize(e: &SetExpr) -> SetExpr {
 }
 
 /// [`normalize`] for lanes that may hold NULL: the result is TRUE on exactly
-/// the rows where `e` is TRUE under Kleene logic (module docs).
-pub fn normalize_kleene(e: &SetExpr) -> SetExpr {
-    normalize_with(e, Logic::Kleene)
+/// the rows where `e` is TRUE under Kleene logic (module docs). Its FALSE and
+/// UNKNOWN rows are not those of `e`, so it is returned as a [`WhereSet`].
+pub fn normalize_kleene(e: &SetExpr) -> WhereSet {
+    WhereSet(normalize_with(e, Logic::Kleene))
+}
+
+/// The result of [`normalize_kleene`]: a set whose TRUE rows are the original
+/// expression's TRUE rows under Kleene logic. Its FALSE / UNKNOWN split is
+/// not the original's, so it is valid only where a terminal reads TRUE rows
+/// (a measure, a SQL `WHERE`), never under `NOT`, inside a `CHECK`, or as an
+/// operand of a larger three-valued expression (module docs).
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[must_use]
+pub struct WhereSet(SetExpr);
+
+impl WhereSet {
+    /// The set, to be read only as "the rows where it is TRUE".
+    pub fn where_true(&self) -> &SetExpr {
+        &self.0
+    }
+
+    /// Take the set out for a terminal that reads TRUE rows. The caller
+    /// asserts that nothing negates or embeds it in a three-valued context.
+    pub fn into_where_true(self) -> SetExpr {
+        self.0
+    }
 }
 
-/// [`normalize`] under `logic`.
-pub fn normalize_with(e: &SetExpr, logic: Logic) -> SetExpr {
+/// [`normalize`] under `logic`. Private: the Kleene result must leave this
+/// module as a [`WhereSet`].
+fn normalize_with(e: &SetExpr, logic: Logic) -> SetExpr {
     let mut cur = nnf(e, false);
     for _ in 0..64 {
         let next = simplify(&cur, logic);
@@ -911,9 +945,13 @@ mod tests {
             let null = nulls(1 + k % 5);
             let e = g.expr(5);
             let want = true_rows(&w, &null, &e);
-            let n = normalize_kleene(&e);
+            let n = normalize_kleene(&e).into_where_true();
             assert_eq!(true_rows(&w, &null, &n), want, "{e:?}\n => {n:?}");
-            assert_eq!(normalize_kleene(&n), n, "not idempotent: {e:?}");
+            assert_eq!(
+                normalize_kleene(&n).into_where_true(),
+                n,
+                "not idempotent: {e:?}"
+            );
             changed += usize::from(n != e);
             two_valued_wrong += usize::from(true_rows(&w, &null, &normalize(&e)) != want);
         }
@@ -972,7 +1010,11 @@ mod tests {
         for e in &covers {
             let want = true_rows(&w, &null, e);
             assert_eq!(want.iter().filter(|&&b| b).count(), N.div_ceil(2), "{e:?}");
-            assert_eq!(true_rows(&w, &null, &normalize_kleene(e)), want, "{e:?}");
+            assert_eq!(
+                true_rows(&w, &null, normalize_kleene(e).where_true()),
+                want,
+                "{e:?}"
+            );
             assert_ne!(true_rows(&w, &null, &normalize(e)), want, "{e:?}");
         }
     }
@@ -1016,11 +1058,14 @@ mod tests {
         let mut g = Gen(0xB0B);
         for _ in 0..3000 {
             let e = g.expr(5);
-            assert!(normalize_kleene(&e).leaves() <= e.leaves(), "{e:?}");
+            assert!(
+                normalize_kleene(&e).into_where_true().leaves() <= e.leaves(),
+                "{e:?}"
+            );
         }
         // The `!=` case on its own: `x != 1` stays one atom.
         let ne = SetExpr::i32(0, Cmp::Ne, 1);
-        assert_eq!(normalize_kleene(&ne), ne);
+        assert_eq!(normalize_kleene(&ne).into_where_true(), ne);
     }
 
     fn x() -> SetExpr {
@@ -1201,3 +1246,81 @@ mod tests {
         assert_eq!(Runs::empty().complement(5).unwrap(), Runs::full(5));
     }
 }
+
+#[cfg(test)]
+mod where_terminal {
+    use super::*;
+
+    /// Kleene evaluation of the one-lane fixture: `x` is `[3, NULL]`.
+    fn k(e: &SetExpr, null: bool) -> Option<bool> {
+        match e {
+            SetExpr::All => Some(true),
+            SetExpr::Empty => Some(false),
+            SetExpr::Res(Res::I32 { op, t, .. }) => {
+                if null {
+                    None
+                } else {
+                    let x = 3;
+                    Some(match op {
+                        Cmp::Lt => x < *t,
+                        Cmp::Le => x <= *t,
+                        Cmp::Gt => x > *t,
+                        Cmp::Ge => x >= *t,
+                        Cmp::Eq => x == *t,
+                        Cmp::Ne => x != *t,
+                    })
+                }
+            }
+            SetExpr::Not(c) => k(c, null).map(|b| !b),
+            SetExpr::And(cs) => {
+                let vs: Vec<Option<bool>> = cs.iter().map(|c| k(c, null)).collect();
+                if vs.contains(&Some(false)) {
+                    Some(false)
+                } else if vs.contains(&None) {
+                    None
+                } else {
+                    Some(true)
+                }
+            }
+            SetExpr::Or(cs) => k(
+                &SetExpr::negated(SetExpr::And(
+                    cs.iter().cloned().map(SetExpr::negated).collect(),
+                )),
+                null,
+            ),
+            _ => unreachable!("fixture uses I32 residuals only"),
+        }
+    }
+
+    /// FAILS IF: the Kleene form is claimed to be fully three-valued
+    /// equivalent. `p ∧ ¬p` keeps its TRUE rows (none) but becomes `Empty`,
+    /// which is FALSE where `p` is UNKNOWN; so `NOT` over the normalized set
+    /// selects the NULL row and `NOT` over the original does not. This pins
+    /// why [`normalize_kleene`] returns a [`WhereSet`].
+    #[test]
+    fn the_kleene_form_preserves_true_rows_but_not_false_rows() {
+        let p = SetExpr::i32(0, Cmp::Lt, 5);
+        let e = SetExpr::And(vec![p.clone(), SetExpr::negated(p)]);
+        let n = normalize_kleene(&e);
+        assert_eq!(n.where_true(), &SetExpr::Empty);
+        for null in [false, true] {
+            assert_eq!(
+                k(&e, null) == Some(true),
+                k(n.where_true(), null) == Some(true),
+                "TRUE rows must agree (null = {null})"
+            );
+        }
+        // Present row: both FALSE. NULL row: original UNKNOWN, normalized FALSE.
+        assert_eq!(k(&e, false), Some(false));
+        assert_eq!(k(&e, true), None);
+        assert_eq!(k(n.where_true(), true), Some(false));
+        let not_orig = SetExpr::negated(e);
+        let not_norm = SetExpr::negated(n.into_where_true());
+        assert_eq!(k(&not_orig, true), None, "NOT (p AND NOT p) is UNKNOWN");
+        assert_eq!(
+            k(&not_norm, true),
+            Some(true),
+            "NOT over the WHERE form is TRUE"
+        );
+    }
+}

crates/lance-graph-contract/src/set_rules.rs

@@ -443,7 +443,8 @@ fn apply(rule: Rule, m: &Measure, sem: &Semantics) -> Option<Result<Measure, Ref
             // form keeps exactly those (`set_algebra` module docs).
             let n = match sem.truth {
                 Truth::TwoValued => normalize(set),
-                Truth::ThreeValued => normalize_kleene(set),
+                // Terminal: a measure reads only the TRUE rows.
+                Truth::ThreeValued => normalize_kleene(set).into_where_true(),
             };
             if n == *set {
                 return None;

crates/lance-graph-quack/examples/k3_where_pg_parity.rs

@@ -382,7 +382,7 @@ fn main() {
         let (tbits, fbits) = line.split_once(',').expect("two columns");
         let (pg_t, pg_f) = (plane(tbits), plane(fbits));
         unknown_rows += ROWS - tbits.matches('1').count() - fbits.matches('1').count();
-        let (f, nk) = (filter(e), filter(&normalize_kleene(e)));
+        let (f, nk) = (filter(e), filter(normalize_kleene(e).where_true()));
         for mode in [Mode::InPlace, Mode::Fused] {
             let neg = Filter::Not(Box::new(f.clone()));
             assert!(
@@ -404,7 +404,7 @@ fn main() {
             &keep(&t, &Filter::Not(Box::new(nk.clone())), Mode::InPlace),
             &pg_f,
         ));
-        rewritten += usize::from(normalize_kleene(e) != *e);
+        rewritten += usize::from(normalize_kleene(e).where_true() != e);
         two_valued_wrong += usize::from(differ(
             &keep(&t, &filter(&normalize(e)), Mode::InPlace),
             &pg_t,