Skip to content

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

Merged
AdaWorldAPI merged 1 commit into
mainfrom
claude/eager-albattani-iufugq-k3-admission
Oct 21, 2026
Merged

AdaWorldAPI merged 1 commit into
mainfrom
claude/eager-albattani-iufugq-k3-admission

Conversation

@AdaWorldAPI

Copy link
Copy Markdown
Owner

This PR covers item C of the post-merge review of #1677 and #1679 (GPT:gpt-ada-01/20261021-pr1674-1682-consolidated-review-01). I took it on the operator's instruction (EXO-50 /038). The original owners are session 01G22y (normalize_kleene) and session 01Vnc (GKAT); the operator aligns afterwards.

C1. WHERE-preserving is not three-valued equivalent

The problem. #1677 measured that normalize_kleene keeps the TRUE rows but moves FALSE rows on 337 of 2000 expressions. Before this PR, the function returned a plain SetExpr, so callers could reuse the result under NOT.

The change.

  • normalize_kleene now returns set_algebra::WhereSet, a newtype whose field is private.
  • The set comes out only through where_true() or into_where_true(). Either name states the WHERE-only restriction at the call site.
  • normalize_with is private, so the Kleene result cannot leave the module as a plain SetExpr.
  • Three call sites take the set out explicitly:
    • set_rules' SetNormalize, whose measure is terminal;
    • the contract example k3_pg_parity.rs;
    • the quack example k3_where_pg_parity.rs.
  • No new rule, refusal or framework. The existing Semantics::truth gate is unchanged.

The new test the_kleene_form_preserves_true_rows_but_not_false_rows uses p AND NOT p with p UNKNOWN:

  • the TRUE rows (none) are kept;
  • the result becomes Empty;
  • NOT over the result is TRUE, whereas NOT (p AND NOT p) is UNKNOWN.

C2. GKAT projection and negation

Cond::Not negates a guard that has already been projected. The new tests/k3_negation_duality.rs checks all four atoms (TRUE, FALSE, and NULL under both payloads), comparing each side against the SQL meaning rather than against the other side:

  • Where(NOT p) = NOT Check(p);
  • Check(NOT p) = NOT Where(p);
  • NOT Where(p) differs from SQL WHERE NOT p exactly on the two NULL atoms;
  • none of these forms reads a NULL payload.

Disable runs: two, both red. One drops the validity test from Where, the other from Check.

The GKAT algorithm is unchanged; the module docs in flow.rs now name this boundary.

Evidence

  • cargo check --workspace --all-targets passes.
  • Contract: 1626 tests pass.
  • gkat-probe: all suites pass.
  • Clippy -D warnings is clean for contract, quack and gkat-probe, and fmt is clean.
  • PostgreSQL 16.15 results are unchanged after this PR:
    • k3_pg_parity: 2000/2000.
    • k3_where_pg_parity: TRUE and FALSE rows equal on 2000/2000, FALSE rows moved on 337, two-valued normalize wrong on 499.
  • A correction section is appended to entries/2026-10-21-d-rft-0-kleene-normalization.md. The entries index and the supersession index regenerate unchanged.

API change: normalize_kleene's return type changes, and normalize_with becomes private. I found no callers outside the three files above (checked across the AdaWorldAPI sibling repos in this container).

I will not merge this PR; it waits for your review.


Generated by Claude Code

…AT negation duality pinned

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

coderabbitai Bot commented Oct 21, 2026

Copy link
Copy Markdown

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: e22ad464-c1c2-4cae-b3b2-c353859aee7a
  • 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

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

Copy link
Copy Markdown

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-21T22:21:47.561440Z 59cf28c PR opened
ℹ️ 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.

@AdaWorldAPI
AdaWorldAPI merged commit 50990a5 into main Oct 21, 2026
23 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants