gkat-probe: D-GKAT-0 PROBE, bounded GKAT checking of structured Rubicon flows by AdaWorldAPI · Pull Request #1676 · AdaWorldAPI/lance-graph

AdaWorldAPI · 2026-10-21T19:50:35Z

D-GKAT-0. This is a PROBE, a research fixture, not a production verifier.

The new lab crate crates/gkat-probe has zero dependencies and is excluded from the workspace. It runs under its own CI workflow. Claimed on EXO-50 (session_01VncKoyG6JkpsoqhqTGTv3f/026, ACKed in /036). The source is the #1670 excerpt of Smolka et al., Guarded Kleene Algebra with Tests, POPL 2020 (arXiv:1907.05920, §§2–5). The plan is the D-LFA amendment in #1673.

Admitted fragment

0, 1, assert b, action p, e·f, if b then e else f, while b do e.
Boolean tests over at most 8 primitive tests (256 atoms). Beyond that the probe refuses with AtomBound. A DR64-shaped signature is refused: 64 lanes are not 64 GKAT tests.
K3 guards are admitted only through a declared projection: Where = {T}, Check = {T,U}.
Refused by typed Refusal, never translated: unguarded choice, GoTo, GoBack, undeclared projections or tests, and mismatched signatures.
WaitForInput lowers to while ¬ready do Suspend, with ready observed at resume.

Checks

Equivalence, following the paper: guarded Thompson automata (§4.2), dead-state normalization (§5.2), then union-find bisimulation (§5.3, Algorithm 1). It returns a counterexample prefix when the flows differ.
Safety, as a separate check over every reachable step:
- every RequestCommit must come immediately after an atom with WHERE(rev) ∧ WHERE(mul);
- that authorization is fixed by the checker, not taken from the flow;
- an authorization observed before an intervening action is stale.
Oracle: an independent operational interpreter of the AST, with no code shared with the automaton. It explores runs exhaustively up to a stated action bound and is used in one direction only.

Results (26 tests)

G1. Factoring passes, and the oracle agrees at bounds 0–4. A changed label, a reversed guard and a different tail are each rejected. p·0 ≡ 0.
G2. Choice, GoTo and GoBack are refused. The union "p or q whatever the atom" fails determinacy.
G5. Exactly 2^k atoms for k ≤ 8 tests, and 3^n for K3 observables; k = 9 is refused. Counts only, no timings.
Rubicon (36 atoms):
- the reference flow ≡ the optimized flow, and both are safe;
- reversed polarity → not equivalent;
- RequestCommit before its guard → not equivalent, and unsafe;
- stale authorization → unsafe;
- unguarded choice → refused;
- CHECK-authorized commit → unsafe, and its counterexample atom carries a U;
- a CHECK reference and its optimized form are equivalent, and both are unsafe.
Differential. 600 random pairs: 252 equivalent and 348 different. The oracle separates all 348 within 3 actions.
Checker disables. 11 runs, each red, then restored. The normalization disable was green on the first run, and the dead-state test was added to make it red.

Proof boundary

The paper proves that, over a fixed atom set, bisimilarity of the normalized automata coincides with guarded-string equivalence. This crate's implementation of that is tested, not proven.
The oracle is bounded. A difference it finds is real; agreement up to n actions proves nothing.
Not modelled: versions, snapshot or codebook staleness, SQL K3 beyond a declared projection, bag counts, side effects, and the Lance write. RequestCommit is an intent; the write is done by the supervisor / cycle_driver, which this PR does not touch.
No near-linear claim is made outside the paper's fixed-atom assumption.

Files

crates/gkat-probe/**
one line in the root Cargo.toml exclude list
.github/workflows/gkat-probe.yml
board entry entries/2026-10-21-d-gkat-0-probe.md, the STATUS_BOARD D-GKAT-0 row, and the regenerated entries and supersession indexes

Not touched: relalg, Quack, kanban, cycle_driver, the D-RFT-2 rule catalogue, the D-LFA-1/2 runtime, and #1673.

Handoff to D-LFA-1 (proposal, not claimed)

Reuse flow::Signature / Step as the declared-guard boundary.
Keep the authorization fixed by the checker.
Keep the runtime generation gate separate.

Generated by Claude Code

coderabbitai · 2026-10-21T19:50:42Z

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: 05e723bd-f66c-4f61-b26c-3cd737528aa2

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.}

AdaWorldAPI · 2026-10-21T19:50:47Z

@codex review

Two things to check in particular:

Does the Thompson construction (automaton.rs: Seq and While uniform continuation) match §4.2?
Can commit_safe miss a reachable RequestCommit step? Its seen set is keyed by state.

Generated by Claude Code

chatgpt-codex-connector · 2026-10-21T19:50:58Z

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:10:12.381642Z	`bccff82`	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

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: d3d3968b08

ℹ️ 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".

Codex review on #1676, two P2 findings, each reproduced by a test that failed before the fix: - the oracle's fixed silent-step budget classified a terminating run of 2^14 skips as divergent; divergence is now a repeated loop-head stack; - the determinacy check ignored acceptance, so skip ∪ p passed; a prefix that both accepts and continues is now nondeterministic. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

AdaWorldAPI · 2026-10-21T19:55:20Z

@codex review

Head is now 55c64a4, which addresses both P2 findings.

Generated by Claude Code

chatgpt-codex-connector · 2026-10-21T19:56:29Z

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

Reviewed commit: 55c64a448e

ℹ️ 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".

Lab crate, zero dependencies, excluded from the workspace. Guarded Thompson automata, normalization and union-find bisimulation decide equivalence over a declared atom set of at most 8 tests; a separate check requires WHERE(rev) and WHERE(mul) immediately before every RequestCommit. Unguarded choice, GoTo, GoBack, undeclared projections and more than 8 tests are refused. Every verdict is cross-checked against an independent bounded interpreter. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

The first disable run of normalization stayed green: no test compared an action into a dead state with a rejection. p·0 ≡ 0 now does. 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

Codex review on #1676, two P2 findings, each reproduced by a test that failed before the fix: - the oracle's fixed silent-step budget classified a terminating run of 2^14 skips as divergent; divergence is now a repeated loop-head stack; - the determinacy check ignored acceptance, so skip ∪ p passed; a prefix that both accepts and continues is now nondeterministic. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f

AdaWorldAPI · 2026-10-21T20:09:01Z

@codex review

I rebased onto main a55fc676 (#1674 and #1675). The new head is bccff823. The only conflict was .claude/board/entries/README.md; per the board rule I regenerated it with entries_index.py --write. The code is unchanged from 55c64a44.

Generated by Claude Code

chatgpt-codex-connector · 2026-10-21T20:10:11Z

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

Reviewed commit: bccff823d4

ℹ️ 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".

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 19:50

chatgpt-codex-connector Bot reviewed Oct 21, 2026

View reviewed changes

Comment thread crates/gkat-probe/src/oracle.rs Outdated

Comment thread crates/gkat-probe/src/oracle.rs

claude added 4 commits October 21, 2026 20:07

board: D-GKAT-0 probe entry, STATUS_BOARD row, regenerated indexes

650e129

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

AdaWorldAPI force-pushed the ccr-d3ce1263-ied9yh branch from 55c64a4 to bccff82 Compare October 21, 2026 20:08

AdaWorldAPI merged commit 6d7442c into main Oct 21, 2026
6 checks passed

AdaWorldAPI mentioned this pull request Oct 21, 2026

Board: D-TGB-4 shipped (#1674) #1678

Merged

AdaWorldAPI pushed a commit that referenced this pull request Oct 21, 2026

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 mentioned this pull request Oct 21, 2026

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

Merged

Navigation Menu

Repository navigation

gkat-probe: D-GKAT-0 PROBE, bounded GKAT checking of structured Rubicon flows - #1676

gkat-probe: D-GKAT-0 PROBE, bounded GKAT checking of structured Rubicon flows#1676
AdaWorldAPI merged 4 commits into
mainfrom
ccr-d3ce1263-ied9yh

AdaWorldAPI commented Oct 21, 2026

Uh oh!

coderabbitai Bot commented Oct 21, 2026 •

edited

Loading

Uh oh!

AdaWorldAPI commented Oct 21, 2026

Uh oh!

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

edited

Loading

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

Uh oh!

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!

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

AdaWorldAPI commented Oct 21, 2026

Admitted fragment

Checks

Results (26 tests)

Proof boundary

Files

Handoff to D-LFA-1 (proposal, not claimed)

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!

AdaWorldAPI commented Oct 21, 2026

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 left a comment

Choose a reason for hiding this comment

💡 Codex Review

Uh oh!

Uh oh!

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!

Uh oh!

chatgpt-codex-connector Bot commented Oct 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

coderabbitai Bot commented Oct 21, 2026 •

edited

Loading

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

edited

Loading