gkat-probe: a K3 guard reads a leaf plus validity, never a NULL's payload; D-GKAT-0 board closeout

.claude/board/PR_ARC_INVENTORY.md

@@ -1,3 +1,10 @@
+## 2026-10-21 — lance-graph PR #1676 (merged `6d7442c4`, branch `ccr-d3ce1263-ied9yh`, head `bccff823`) — D-GKAT-0: PROBE, bounded GKAT checking of structured Rubicon flows
+
+- **Added:** lab crate `crates/gkat-probe` (zero deps, own workspace, excluded): `expr::{Action, Atom, Atoms, BExp, Exp, Refusal, MAX_TESTS}`, `automaton::{thompson, equivalent, commit_safe, Equivalence, Safety, Out}`, `oracle::{explore, same_up_to, unsafe_within, deterministic}`, `flow::{Kind, Cond, Step, Signature, Flow, flows_equivalent}`, `rubicon` fixtures; `.github/workflows/gkat-probe.yml`; entry `2026-10-21-d-gkat-0-probe.md`.
+- **Locked:** the admitted fragment (skip, fail, assert, action, sequence, `if`, `while`) over at most 8 primitive tests; unguarded choice, `GoTo`/`GoBack`, undeclared tests, actions or projections and mismatched signatures are refused, never translated. Equivalence (Thompson + normalization + union-find bisimulation) and commit safety (WHERE(rev) ∧ WHERE(mul) immediately before every `RequestCommit`, fixed by the checker) are separate checks.
+- **Deferred / open:** D-LFA-1 runtime (unclaimed; handoff in EXO-50 `/028`); symbolic guards past 8 tests; G3/G4/G6/G7. Merged by the operator before the Codex re-review of `bccff823` and two workspace jobs finished; the re-review came back clean and no main job failed.
+- **Confidence:** TEST-PINNED, not proven. 28 tests; 11 checker disables red; 2 Codex P2s (fixed-budget divergence, determinacy without acceptance) fixed failing-first; CI green on `55c64a44`.
+
 ## 2026-10-21 — lance-graph PR #1674 (merged `414377f3`, branch `ccr-f5674497-orfkox`, head `ed54930e`) — D-TGB-4: thought-git receipt and deterministic replay
 
 - **Added:** `thought_git_probe::receipt::{BaseRef, VersionStore, ProgramId, DERIVE, ProgramInputs, ExecConfig, EXEC_DEFAULT, Fold, Receipt, ReceiptIdentity, Refusal, Plan, capture, Replayed, replay, replay_live, MetaKey, MetaRow, MetadataTable}`; `tests/receipt.rs` (10 falsifiers); `.github/workflows/thought-git-probe.yml` (first CI line for the crate); entry `2026-10-21-d-tgb-4-receipt-replay.md`.

.claude/board/STATUS_BOARD.md

@@ -8,7 +8,7 @@ Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quac
 | **D-QSP-0 remainder, slice 1** | scalar aggregates under SQL NULL: empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG | In PR (EXO-50 claim `session_013z2e1YXkm6o6HNrDn5BPWA/026`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`): Quack `lower_sum` + `sum_finish` over existing terminals. MEASURED: PostgreSQL 16.15 = Quack = Kleene oracle on 3600/3600 queries | `tests/sql_aggregate_null.rs` (4 disables red); `examples/qsp_agg_pg_parity.rs` (SKIP without a server) |
 | **D-RFT-1..5, D-LFA-0** | composition, substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed |
 | **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed |
-| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | In PR, PROBE (EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused | 3 flow disables + 11 checker disables red; independent bounded oracle; not a production verifier |
+| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | Shipped, PROBE (#1676, merged `6d7442c4`; EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`, RESULT `/028`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused. K3 guards are a leaf plus a validity bit and never read the payload of a NULL, as Quack's `sql_where` (#1679) | 3 flow disables + 15 checker disables red; independent bounded oracle; not a production verifier |
 
 ## D-RU — D-RELALG-UNIFIED: JC/R statistics and Datalog sharing work through the contract set IR (2026-10-20)
 

.claude/board/entries/2026-10-21-d-gkat-0-probe.md

@@ -26,10 +26,13 @@
 | choice without a condition | `Refusal::UnguardedChoice` |
 
 **K3 guards.**
-- A K3 observable occupies two primitive tests, `is_t` and `is_u`. The atom set excludes `is_t ∧ is_u`, which leaves exactly three values.
+- A K3 observable is a leaf over a nullable column, and it occupies two tests: `leaf` and `valid`.
+  - The leaf is the Boolean read off the stored value: the bit itself for a `BOOLEAN` column, a comparison such as `rev = 5` for a numeric one.
+  - Under `valid = 0` the payload is arbitrary (Quack `Filter::sql_where`; PostgreSQL stores none). There is no constraint between the two tests, so NULL is two atoms.
+  - History: #1676 used `is_t`/`is_u`, an UNKNOWN bit Quack does not have. #1679 first replaced it with a value bit forced to 0 under NULL; that assumption is also false, and it was dropped.
 - A K3 guard reaches a Boolean test only through a declared projection:
-  - `Where` = `{T}`
-  - `Check` = `{T,U}`
+  - `Where` = `{T}` = `valid ∧ leaf`
+  - `Check` = `{T,U}` = `¬valid ∨ leaf`; neither reads the leaf under a NULL
   - `Is` applies to Boolean observables only.
 - Any other pairing of projection and observable is refused.
 
@@ -47,7 +50,7 @@
 - **Oracle** (`oracle.rs`): an independent operational interpreter of the expression AST that shares no code with the automaton. It explores every run exhaustively up to a stated action bound.
   Divergence is detected exactly, by a repeated continuation stack at a loop head, not by a step budget. The first version used a fixed budget, which Codex showed misclassifies a terminating run of 2^14 silent steps.
 
-## Measured (`cargo test`, 28 tests)
+## Measured (`cargo test`, 29 tests)
 
 - **G1.** `if b then {p;q} else {q}` ≡ `(if b then {p} else {skip}); q`. The oracle agrees at bounds 0–4. A changed action label is rejected, a reversed guard is rejected, and a different tail is rejected. `p·0 ≡ 0` (normalization).
 - **G2.** Rejections:
@@ -57,11 +60,11 @@
 
   So does the union of `skip` and `p`: on one atom it may either accept or act. The admitted Rubicon flows are deterministic.
 - **G5.**
-  - For `k ≤ 8` tests: `2^k` atoms exactly. For `n ≤ 4` K3 observables: `3^n` atoms exactly.
+  - For `k ≤ 8` tests: `2^k` atoms exactly. For `n ≤ 4` K3 observables: `4^n` atoms exactly (three values each).
   - `k = 9` is refused (`AtomBound`). A DR64-shaped signature (64 Boolean lanes) is refused, as is one with 5 K3 observables (10 tests).
   - On a chain of `k` guards, the automaton has `2k` states while the atom count is `2^k`. Measured (k, atoms, states, merged pairs): (1,2,2,3) … (8,256,16,17).
   - Counts only, no timings (the workspace's no-ms rule).
-- **Rubicon** (11 tests, 36 atoms).
+- **Rubicon** (12 tests, 64 atoms).
   - The reference flow has the decision tail written out twice; the optimized flow factors it out (G1) and reorders the decision. The two are **equivalent**, and both are **safe**.
   - Disable runs on the flows:
     - reversed authorization polarity → equivalence fails;
@@ -85,7 +88,8 @@
   - atom bound raised to 64;
   - uniform sequence continuation not patched;
   - signature mismatch not refused;
-  - K3 exclusion dropped.
+  - K3 `Where` ungated (only the payload test catches it: flow and authorization share the lowering);
+  - K3 `Check` lowered as the leaf, `Where` as validity, `Check` as `Where`.
 
   The first normalization disable stayed green because no test compared a step into a dead state with a rejection. `a_step_into_a_dead_state_is_a_rejection` was added to close that gap.
 

crates/gkat-probe/src/flow.rs

@@ -24,13 +24,22 @@
 //! ## Guards and projections
 //!
 //! An observable is declared as Boolean or as three-valued (K3: T, F, U). A
-//! K3 observable occupies two primitive tests, `is_t` and `is_u`, and the
-//! atom set excludes the assignment where both hold, so it has exactly three
-//! values. A K3 observable reaches a Boolean guard only through a declared
-//! projection:
+//! K3 observable is a leaf over a nullable column (`crates/lance-graph-quack`,
+//! `Filter::sql_where`): the column's stored value plus its validity plane.
+//! The leaf is the Boolean read off the stored value, and what that means
+//! depends on the column's type. For a `BOOLEAN` column the leaf is the stored
+//! bit itself (in Quack, a mask plane). For a numeric or text column it is a
+//! comparison such as `rev = 5`, and 0 and 1 in the lane are ordinary
+//! numbers. Either way the observable occupies two tests: `leaf` and `valid`.
+//! Under `valid = 0` no value is stored (PostgreSQL) or the payload is
+//! arbitrary (Quack), so the leaf there reads nothing meaningful. There is no
+//! constraint between the two tests: all four pairs are atoms, and NULL is the
+//! two with `valid = 0`. A K3 observable reaches a Boolean guard only through
+//! a declared projection, and neither projection reads the leaf under a NULL:
 //!
-//! * [`Cond::Where`]: designated `{T}`, i.e. `is_t`;
-//! * [`Cond::Check`]: designated `{T, U}`, i.e. `is_t ∨ is_u`.
+//! * [`Cond::Where`]: designated `{T}`, i.e. `T(φ) = valid ∧ leaf`, what
+//!   Quack's `WHERE` keeps;
+//! * [`Cond::Check`]: designated `{T, U}`, i.e. `¬F(φ) = ¬valid ∨ leaf`.
 //!
 //! A Boolean observable is read with [`Cond::Is`]. Using a K3 projection on a
 //! Boolean observable, or `Is` on a K3 one, is refused.
@@ -114,8 +123,8 @@ pub struct Signature {
 }
 
 impl Signature {
-    /// The primitive test of an observable: `is_t` for K3 (and the only test
-    /// of a Boolean), plus `is_u` for K3.
+    /// The first primitive test of an observable: the leaf for K3
+    /// (followed by its validity bit), or the only test of a Boolean.
     fn tests_of(&self, name: &'static str) -> Result<(Kind, u8), Refusal> {
         let mut next = 0u8;
         for (n, k) in &self.observables {
@@ -151,20 +160,9 @@ impl Signature {
                 max: crate::expr::MAX_TESTS,
             });
         }
-        // Each K3 observable excludes the assignment is_t ∧ is_u.
-        let mut constraint = BExp::True;
-        let mut next = 0u8;
-        for (_, k) in &self.observables {
-            match k {
-                Kind::Bool => next += 1,
-                Kind::K3 => {
-                    constraint =
-                        constraint.and(BExp::Test(next).and(BExp::Test(next + 1)).negated());
-                    next += 2;
-                }
-            }
-        }
-        Atoms::new(tests, &constraint)
+        // No constraint: under a NULL the stored payload, and so the leaf, is
+        // arbitrary. The guards, not the atom set, make NULL one value.
+        Atoms::new(tests, &BExp::True)
     }
 
     /// Lowers a condition to a Boolean test.
@@ -180,7 +178,7 @@ impl Signature {
                 }
             },
             Cond::Where(n) => match self.tests_of(n)? {
-                (Kind::K3, t) => BExp::Test(t),
+                (Kind::K3, t) => BExp::Test(t + 1).and(BExp::Test(t)),
                 (Kind::Bool, _) => {
                     return Err(Refusal::UndeclaredProjection {
                         observable: n,
@@ -189,7 +187,7 @@ impl Signature {
                 }
             },
             Cond::Check(n) => match self.tests_of(n)? {
-                (Kind::K3, t) => BExp::Test(t).or(BExp::Test(t + 1)),
+                (Kind::K3, t) => BExp::Test(t + 1).negated().or(BExp::Test(t)),
                 (Kind::Bool, _) => {
                     return Err(Refusal::UndeclaredProjection {
                         observable: n,

crates/gkat-probe/src/rubicon.rs

@@ -39,7 +39,7 @@ pub const DELIBERATE_NEEDED: &str = "deliberate";
 /// Whether external input is ready at resume.
 pub const INPUT_READY: &str = "input";
 
-/// 6 primitive tests: rev (2), mul (2), deliberate (1), input (1); 36 atoms.
+/// 6 primitive tests: rev (2), mul (2), deliberate (1), input (1); 64 atoms.
 pub fn signature() -> Signature {
     Signature {
         observables: vec![

crates/gkat-probe/tests/g5_atoms.rs

@@ -9,13 +9,14 @@ fn atom_counts_are_exact() {
     for k in 0..=MAX_TESTS as usize {
         assert_eq!(Atoms::new(k, &BExp::True).unwrap().len(), 1 << k);
     }
-    // A K3 observable occupies two tests and has three values.
+    // A K3 observable occupies two tests (leaf, valid) with no constraint:
+    // four atoms, of which the two with valid = 0 are one value, NULL.
     let sig = |n: usize| Signature {
         observables: (0..n).map(|_| ("x", Kind::K3)).collect(),
         actions: vec![],
     };
     for n in 0..=4 {
-        assert_eq!(sig(n).atoms().unwrap().len(), 3usize.pow(n as u32));
+        assert_eq!(sig(n).atoms().unwrap().len(), 4usize.pow(n as u32));
     }
 }
 

crates/gkat-probe/tests/rubicon.rs

@@ -7,7 +7,7 @@ use gkat_probe::rubicon::{self, REQUEST_COMMIT};
 use gkat_probe::{Refusal, commit_safe};
 
 /// Oracle bound: two actions covers Deliberate or one Suspend, followed by
-/// the decision. With 36 atoms that is 36^3 runs per flow.
+/// the decision. With 64 atoms that is 64^3 runs per flow.
 const BOUND: usize = 2;
 
 fn safe(flow: &gkat_probe::flow::Flow) -> bool {
@@ -42,8 +42,9 @@ fn equivalent(a: &gkat_probe::flow::Flow, b: &gkat_probe::flow::Flow) -> bool {
 }
 
 #[test]
-fn the_signature_declares_36_atoms() {
-    assert_eq!(rubicon::signature().atoms().unwrap().len(), 36);
+fn the_signature_declares_64_atoms() {
+    // Two K3 observables (4 atoms each) and two Booleans.
+    assert_eq!(rubicon::signature().atoms().unwrap().len(), 64);
 }
 
 #[test]
@@ -107,8 +108,10 @@ fn the_check_counterexample_has_an_unknown() {
     let auth = rubicon::authorized().unwrap();
     match commit_safe(&e, &atoms, REQUEST_COMMIT, &auth).unwrap() {
         gkat_probe::Safety::Unsafe { atom, .. } => {
-            // rev is tests 0 (is_t) and 1 (is_u); mul is tests 2 and 3.
-            assert!(atom.holds(1) || atom.holds(3), "{atom:?}");
+            // rev is tests 0 (leaf) and 1 (valid); mul is tests 2 and 3.
+            // UNKNOWN is a cleared validity bit.
+            let unknown = |t: u8| !atom.holds(t + 1);
+            assert!(unknown(0) || unknown(2), "{atom:?}");
         }
         gkat_probe::Safety::Safe => panic!("expected unsafe"),
     }
@@ -147,3 +150,40 @@ fn undeclared_projections_are_refused() {
         Err(Refusal::UnknownObservable("nope"))
     ));
 }
+
+/// A K3 observable is a leaf over a nullable column: the Boolean read off the
+/// stored value (the bit itself for a `BOOLEAN` column, a comparison for a
+/// numeric one) and the validity bit. Under `valid = 0` the payload is
+/// arbitrary (Quack, `Filter::sql_where`), so the leaf there reads nothing.
+/// All four `(leaf, valid)` pairs are atoms, NULL is the two with `valid = 0`,
+/// and no guard may tell those two apart.
+#[test]
+fn a_k3_guard_never_reads_the_payload_of_a_null() {
+    use gkat_probe::Atom;
+    use gkat_probe::flow::Cond;
+    let sig = rubicon::signature();
+    let atoms = sig.atoms().unwrap();
+    // rev occupies tests 0 (leaf) and 1 (valid). A NULL with either payload
+    // is an atom: nothing forces the lane to 0.
+    assert!(atoms.iter().any(|a| a.holds(0) && !a.holds(1)));
+    assert!(atoms.iter().any(|a| !a.holds(0) && !a.holds(1)));
+    for g in [Cond::Where(rubicon::REV), Cond::Check(rubicon::REV)] {
+        let b = sig.guard(&g).unwrap();
+        for a in atoms.iter().filter(|a| !a.holds(1)) {
+            let flipped = Atom(a.0 ^ 1);
+            assert_eq!(b.eval(a), b.eval(flipped), "{g:?} reads a NULL payload");
+        }
+    }
+    let r#where = sig.guard(&Cond::Where(rubicon::REV)).unwrap();
+    let check = sig.guard(&Cond::Check(rubicon::REV)).unwrap();
+    // (leaf, valid): TRUE = (1,1), FALSE = (0,1), NULL = (_,0).
+    let (t, f, null0, null1) = (Atom(0b11), Atom(0b10), Atom(0b00), Atom(0b01));
+    assert_eq!(
+        [t, f, null0, null1].map(|a| r#where.eval(a)),
+        [true, false, false, false]
+    );
+    assert_eq!(
+        [t, f, null0, null1].map(|a| check.eval(a)),
+        [true, false, true, true]
+    );
+}