gkat-probe: a K3 guard reads a leaf plus validity, never a NULL's payload; D-GKAT-0 board closeout by AdaWorldAPI · Pull Request #1679 · AdaWorldAPI/lance-graph

AdaWorldAPI · 2026-10-21T20:23:43Z

Follow-up to #1676 (D-GKAT-0, PROBE). It also carries the board closeout.

K3 encoding

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, and what that means depends on the column type:
- for a BOOLEAN column, the stored bit itself (in Quack, a mask plane);
- for a numeric or text column, a comparison such as rev = 5. There, 0 and 1 in the lane are ordinary numbers.
Under valid = 0 PostgreSQL stores no value, and Quack keeps an arbitrary payload that "never takes part in the answer" (crates/lance-graph-quack/src/lib.rs, Filter::sql_where).
No constraint links the two tests, so all four pairs are atoms. NULL is the two with valid = 0.
The two guard reads match sql_where's T(φ) and ¬F(φ), and neither reads the leaf under a NULL:
- Where = valid ∧ leaf
- Check = ¬valid ∨ leaf

History.

gkat-probe: D-GKAT-0 PROBE, bounded GKAT checking of structured Rubicon flows #1676 used (is_t, is_u), an UNKNOWN bit the substrate does not have.
An intermediate commit of this PR used a value bit and forced it to 0 under NULL, then lowered Where as the bare value bit. That assumption is false, so the guard read the payload of a NULL wherever it failed.

Tests.

a_k3_guard_never_reads_the_payload_of_a_null failed before the fix. It checks that the atom set contains a NULL with either payload, and that flipping the leaf under valid = 0 changes neither guard.
The Rubicon flow now has 64 atoms. Every Rubicon and differential verdict is unchanged.

Disables, each red:

Where ungated. Only the payload test catches this one: the flow and the authorization share the lowering, so Rubicon safety stays green.
Check lowered as the leaf.
Where lowered as validity.
Check lowered as Where.

29 tests pass; clippy -D warnings and fmt are clean. The branch contains main.

Board closeout for #1676

STATUS_BOARD: the D-GKAT-0 row is now Shipped (6d7442c4).
PR_ARC_INVENTORY: a new entry for gkat-probe: D-GKAT-0 PROBE, bounded GKAT checking of structured Rubicon flows #1676. It records that the operator merged it before the Codex re-review of bccff823 and two workspace jobs had finished. The re-review came back clean, and no job failed on main.
The entry text is updated, and both indexes are regenerated.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

Quack carries NULL as a validity plane and a three-valued verdict as the masks T(φ) and F(φ) (Filter::sql_where); UNKNOWN is neither, so there is no separate UNKNOWN bit. The probe invented one (is_t, is_u). A K3 observable is now the pair (T, F) with T ∧ F excluded; WHERE = T and CHECK = ¬F. Same three atoms per observable, same verdicts on every flow. a_k3_observable_is_quacks_t_f_pair failed before this change. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

AdaWorldAPI · 2026-10-21T20:23:51Z

@codex review

Generated by Claude Code

coderabbitai · 2026-10-21T20:23:51Z

Important

🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

⚙️ Run configuration

Configuration used: Organization UI
Review profile: CHILL
Plan: Advanced
Run ID: f8fb83d9-d5de-4e50-8cd5-1b2d24aaf44d

Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Warning

Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption.

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

_{Comment @coderabbitai help to get the list of available commands.}

chatgpt-codex-connector · 2026-10-21T20:24:12Z

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-21T20:41:20.314277Z	`515a399`	Manual request

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

chatgpt-codex-connector · 2026-10-21T20:24:48Z

Codex Review: Didn't find any major issues. Keep it up!

Reviewed commit: 3d2e220e73

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

The previous commit encoded a K3 observable as a T/F verdict pair, which is not how the substrate stores it. Quack stores a nullable column as a value lane plus a validity bit; a cleared validity bit is NULL and its value is 0. A K3 observable is now exactly that: (value, valid) with value -> valid. WHERE = value, CHECK = value | !valid. a_k3_observable_is_a_value_bit_and_a_presence_bit failed before this. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

AdaWorldAPI · 2026-10-21T20:32:57Z

@codex review

Head is now 4e062f2. A K3 guard is now a value bit plus a presence bit, replacing the earlier T/F pair, and main #1677 is merged in.

Generated by Claude Code

chatgpt-codex-connector · 2026-10-21T20:33:56Z

Codex Review: Didn't find any major issues. Breezy!

Reviewed commit: 4e062f2fc9

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

A K3 observable is now two tests, the leaf and validity, with no constraint between them. The leaf is the Boolean read off the stored value: the bit itself for a BOOLEAN column, a comparison for a numeric or text one. Under a cleared validity bit the payload is arbitrary (Quack Filter::sql_where; PostgreSQL stores no value), so all four pairs are atoms and NULL is the two with valid = 0. The previous encoding forced the payload to 0 under NULL and lowered Where as the bare leaf, so it read the payload wherever that assumption failed. Where is now valid AND leaf, Check is NOT valid OR leaf, matching sql_where's T and NOT F. New test a_k3_guard_never_reads_the_payload_of_a_null failed before the fix. Rubicon has 64 atoms; every equivalence and safety verdict is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

AdaWorldAPI · 2026-10-21T20:40:23Z

@codex review

Generated by Claude Code

chatgpt-codex-connector · 2026-10-21T20:41:19Z

Codex Review: Didn't find any major issues. Bravo.

Reviewed commit: 515a3997a4

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

claude added 2 commits October 21, 2026 20:21

board: D-GKAT-0 shipped (#1676); K3 encoding note

3d2e220

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

AdaWorldAPI marked this pull request as ready for review October 21, 2026 20:27

claude added 3 commits October 21, 2026 20:30

board: D-GKAT-0 K3 encoding is value + presence

894e88e

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

Merge remote-tracking branch 'origin/main' into ccr-d3ce1263-ied9yh

4e062f2

AdaWorldAPI changed the title ~~gkat-probe: encode K3 guards as Quack's T/F verdict pair; D-GKAT-0 board closeout~~ gkat-probe: a K3 guard is a value bit plus a presence bit; D-GKAT-0 board closeout Oct 21, 2026

claude added 2 commits October 21, 2026 20:38

board: D-GKAT-0 K3 leaf is payload-blind under NULL

515a399

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

AdaWorldAPI changed the title ~~gkat-probe: a K3 guard is a value bit plus a presence bit; D-GKAT-0 board closeout~~ gkat-probe: a K3 guard reads a leaf plus validity, never a NULL's payload; D-GKAT-0 board closeout Oct 21, 2026

AdaWorldAPI merged commit b8bb4eb into main Oct 21, 2026
13 checks passed

AdaWorldAPI mentioned this pull request Oct 21, 2026

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

Merged

Navigation Menu

Repository navigation

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

gkat-probe: a K3 guard reads a leaf plus validity, never a NULL's payload; D-GKAT-0 board closeout#1679
AdaWorldAPI merged 7 commits into
mainfrom
ccr-d3ce1263-ied9yh

AdaWorldAPI commented Oct 21, 2026 •

edited

Loading

Uh oh!

AdaWorldAPI commented Oct 21, 2026

Uh oh!

coderabbitai Bot commented Oct 21, 2026 •

edited

Loading

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026 •

edited

Loading

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

AdaWorldAPI commented Oct 21, 2026

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

AdaWorldAPI commented Oct 21, 2026

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

AdaWorldAPI commented Oct 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

K3 encoding

Board closeout for #1676

Uh oh!

AdaWorldAPI commented Oct 21, 2026

Uh oh!

coderabbitai Bot commented Oct 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codex Review Summary

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

AdaWorldAPI commented Oct 21, 2026

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

AdaWorldAPI commented Oct 21, 2026

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

AdaWorldAPI commented Oct 21, 2026 •

edited

Loading

coderabbitai Bot commented Oct 21, 2026 •

edited

Loading

chatgpt-codex-connector Bot commented Oct 21, 2026 •

edited

Loading