From 5da3cd55b33fe6983bef42e982423a9c4cce092f Mon Sep 17 00:00:00 2001
From: Felipe705x <favendano.cse@gmail.com>
Date: Sun, 5 Jul 2026 23:47:46 -0400
Subject: [PATCH] test(3vl): add AND cod-override differentiator
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The cod override for the short-circuit connectives (checker.rs) special-
cases OR *and* AND, but the vacuity-soundness suite only had a witness for
OR (`x.status OR true`). Removing the `BinOp::And` arm from the override
therefore broke no test, even though the AND override is load-bearing.

Add the symmetric AND witness: `WHERE NOT (x.status AND false)`. `false` is
AND's absorbing element, so at runtime `NOT (null AND false) = NOT false =
true` keeps every row; under the strict (un-amended) cod, `x.status AND
false : ⊥` then `NOT ⊥ : ⊥`, so the pattern is pruned as guaranteed_empty —
the same static/dynamic unsoundness the OR override fixes. Verified as a real
differentiator: deleting the AND arm from the override flips this query's
guaranteed_empty to true and the test fails (the OR test is unaffected, so
the two are independent witnesses).

No semantics changed; test only.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 tests/three_valued_logic_test.rs | 49 ++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/tests/three_valued_logic_test.rs b/tests/three_valued_logic_test.rs
index 46d587d..46d77d3 100644
--- a/tests/three_valued_logic_test.rs
+++ b/tests/three_valued_logic_test.rs
@@ -483,3 +483,52 @@ fn test_cod_override_keeps_vacuity_sound_under_closed_schema() {
     };
     assert_eq!(rows, 3, "runtime keeps all rows: null OR true = true");
 }
+
+#[test]
+fn test_cod_override_keeps_vacuity_sound_for_and_under_closed_schema() {
+    use frogql::typing::descriptor_type::DescriptorType;
+    use frogql::typing::label_type::LabelType;
+    use frogql::typing::property_type::PropertyType;
+    use frogql::typing::simple_type::SimpleType;
+    use frogql::typing::variable_type::{Schema, VariableType};
+    use std::collections::BTreeMap;
+
+    // Same closed type N { n: Int } — `status` is unknown, so it types to bottom.
+    let mut props = BTreeMap::new();
+    props.insert("n".to_string(), SimpleType::Z);
+    let schema = Schema::from_parts(
+        vec![VariableType::Node(DescriptorType::new(
+            LabelType::Label("N".into()),
+            PropertyType::Closed(props),
+        ))],
+        vec![],
+    );
+
+    // AND's override is load-bearing too, and this is the witness that proves it.
+    // `false` is the absorbing element of AND, so `x.status AND false` is *defined*
+    // (= false) at runtime even though `x.status` reads as null. Wrapping it in a
+    // NOT surfaces that: `NOT (null AND false) = NOT false = true`, keeping every
+    // row. WITHOUT the AND cod override, `x.status AND false : ⊥` (strict cod), then
+    // `NOT ⊥ : ⊥` → the pattern is pruned as guaranteed_empty while the runtime
+    // returns all rows — unsound. The override types the AND as Bool, so `NOT Bool`
+    // stays Bool and the pattern is not pruned. (Delete the `BinOp::And` arm from the
+    // checker's cod override and this test fails: guaranteed_empty flips to true.)
+    let res = frogql::compile_query_with_diagnostics_with(
+        &schema,
+        "MATCH (x:N) WHERE NOT (x.status AND false) RETURN x.name",
+    )
+    .expect("compile");
+    assert!(
+        !res.guaranteed_empty,
+        "cod override must keep `NOT (bottom AND false)` non-empty to stay sound",
+    );
+    let g = active_graph();
+    let rows = match Runtime::new(&g).run_query(&res.query, 0) {
+        QueryResult::Projected(r) => r.len(),
+        _ => 0,
+    };
+    assert_eq!(
+        rows, 3,
+        "runtime keeps all rows: NOT (null AND false) = NOT false = true"
+    );
+}