mistaber-kripke-probe: Kripke holdings as a least fixpoint over DR64 compose by AdaWorldAPI · Pull Request #1873 · AdaWorldAPI/lance-graph

AdaWorldAPI · 2026-10-30T16:19:18Z

Adds a standalone probe that computes Mistaber's Kripke holdings natively and checks them against Clingo goldens. Plan: .claude/plans/d-mistaber-native-v1.md.

Approach

Mistaber's kripke_rules.lp is stratified: holds recurses through inheritance, and every negation is over input relations. The holdings are therefore one least fixpoint:

H₀   = (asserts ∪ endorses) ∧ world
Hₖ₊₁ = H₀ ∪ ((Hₖ ∘ children) ∧ ¬Block)      Block = asserts ∪ endorses ∪ overridden

Each step is one dr-math-binding-probe::relcomp::compose plus an AND-NOT; no new algebra is introduced. Rule and origin lineage use the same fixpoint, gated by H.

Holdings are exposed as one lens (proposition, world, mode, immediate_rule, source_rule); each predicate is a WideFieldMask selection over it. holds/2 is the set projection of that lens.

Changes

crates/mistaber-kripke-probe: standalone workspace, depending only on dr-math-binding-probe and lance-graph-contract.
.github/workflows/mistaber-kripke-probe.yml: fmt, clippy and test for the crate.
crates/lance-graph-contract/src/morton8x8.rs: rustfmt only, matching main.
Plan and status rows for the probe.

Tests

11 tests; all 11 Clingo goldens (exported by AdaWorldAPI/mistaber-rs@62e2382) match exactly, compared as sorted lists.
The even negative cycle (F3-naf) is out of scope and stays with Clingo.
Removing ¬Block, either world mask, the direct-only moderate rule, per-rule bag counting or the lineage gate each turns tests red.
Malformed input is refused: unknown fact kinds, wrong arity, a 65th value on an axis, a non-predicate field selection.
No timings were taken.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

…DR64 compose D-MIST-NATIVE-0. Mistaber's kripke_rules.lp is stratified (every negation is over input relations), so holds is the least fixpoint H = H0 | ((H o children) & !Block), one dr-math-binding-probe::relcomp::compose plus an AND-NOT per step. Rule and origin lineage are the same fixpoint gated by H. Holdings are read as WideFieldMask selections over one lens; holds/2 is a Set projection (a Bag projection double-counts the diamond). Reproduces all 10 Clingo goldens exported by AdaWorldAPI/mistaber-rs exactly. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

Rendering already re-checks holds at the parent, so the gate inside the lineage fixpoint could not fail any golden comparison. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

…robe Plan d-mistaber-native-v1.md: the crosswalk the lance-graph-mistaber facade would export (ALIAS/INLINE/REFUSE), the holdings lens with its Set/Bag split, the probe's evidence and the open questions (production home for compose, lens classid, upstream licence). Own CI workflow for the standalone crate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

coderabbitai · 2026-10-30T16:19:27Z

Important

🔍 Trigger review

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

Run configuration

Source mode: Auto
Repository: Unavailable
Branch: Unavailable
File: No configuration file from this repository applied
Commit: Unavailable
Layers: Organization UI
Review profile: CHILL
Plan: Advanced
Run ID: eaabe3eb-e3bb-404c-8626-41f4ad18df87

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

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

rustfmt output only; one assert_eq! wrapped. Not this PR's change; ported so the style.yml format job passes here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

AdaWorldAPI · 2026-10-30T16:29:57Z

The format check (style.yml) failed on this PR, but the failure isn't caused by this PR's changes. It is in crates/lance-graph-contract/src/morton8x8.rs:295, which c04ffe9 (D-LITHO G3) added to main without rustfmt. This PR does not touch lance-graph-contract.

I've pushed the fix here as dbfb187. It is plain rustfmt output: one assert_eq! wrapped across lines, with no logic change. After it, cargo fmt --manifest-path crates/lance-graph-contract/Cargo.toml -- --check passes locally. The same one-line fix is needed on main for any other PR that isn't based on this branch.

Generated by Claude Code

chatgpt-codex-connector · 2026-10-30T20:37:08Z

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-30T20:39:09.232757Z	`dbfb187`	Draft marked ready

ℹ️ 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: dbfb187f7b

ℹ️ 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 lens row is one (mode, source rule), or one (mode) with empty rule fields when the holding has no rule. Bag projection counted modes, so p,e (one mode, inherited(d), two source rules) gave one row instead of two, and the three-field selection ignored Bag entirely. Each mode now carries a per-rule cell mask; bag_counts_lens_rows_not_modes pins both selections. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

…nic message F6 (from mistaber-rs@62e2382) pins that upstream's inherited rule has no world(W_child) condition: a holding reaches an undeclared child world, and the probe matches it with no world mask on inheritance. F5 only covered an undeclared parent. The lfp unreachable! named a 4096-step bound; the loop runs at most 65 steps (63 hops between 64 worlds, plus one step confirming no change). Board text counts updated; the licensing open question is removed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

…1873); plan §9 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

…; D-MIST-NATIVE-1a shipped Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ

…t-9gtxd4 board: PR_ARC + LATEST_STATE after #1873, #1874, #1875; D-MIST-NATIVE-1a shipped

claude added 3 commits October 30, 2026 16:17

AdaWorldAPI marked this pull request as ready for review October 30, 2026 20:36

chatgpt-codex-connector Bot reviewed Oct 30, 2026

View reviewed changes

Comment thread crates/mistaber-kripke-probe/src/lib.rs Resolved

claude added 2 commits October 30, 2026 20:41

AdaWorldAPI merged commit a6be979 into main Oct 30, 2026
26 checks passed

AdaWorldAPI mentioned this pull request Oct 30, 2026

mistaber-kripke-probe: HHTL16 Register128 rows replace the name interner #1875

Merged

AdaWorldAPI mentioned this pull request Oct 31, 2026

board: record #1873, #1874, #1875 #1877

Merged

AdaWorldAPI added a commit that referenced this pull request Oct 31, 2026

Merge pull request #1877 from AdaWorldAPI/claude/mistaber-ruff-harves…

ebde7df

…t-9gtxd4 board: PR_ARC + LATEST_STATE after #1873, #1874, #1875; D-MIST-NATIVE-1a shipped

AdaWorldAPI changed the title ~~D-MIST-NATIVE-0: Mistaber's Kripke holdings as a least fixpoint over DR64 compose (lab probe)~~ mistaber-kripke-probe: Kripke holdings as a least fixpoint over DR64 compose Oct 31, 2026

Navigation Menu

Repository navigation

mistaber-kripke-probe: Kripke holdings as a least fixpoint over DR64 compose - #1873

mistaber-kripke-probe: Kripke holdings as a least fixpoint over DR64 compose#1873
AdaWorldAPI merged 6 commits into
mainfrom
claude/mistaber-ruff-harvest-9gtxd4

AdaWorldAPI commented Oct 30, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Oct 30, 2026 •

edited

Loading

Uh oh!

AdaWorldAPI commented Oct 30, 2026

Uh oh!

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

edited

Loading

Uh oh!

chatgpt-codex-connector Bot left a comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

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

Uh oh!

Approach

Changes

Tests

Uh oh!

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

Uh oh!

Uh oh!

AdaWorldAPI commented Oct 30, 2026

Uh oh!

chatgpt-codex-connector Bot commented Oct 30, 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!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

AdaWorldAPI commented Oct 30, 2026 •

edited

Loading

coderabbitai Bot commented Oct 30, 2026 •

edited

Loading

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

edited

Loading