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

.claude/board/INTEGRATION_PLANS.md

@@ -2,6 +2,10 @@
 
 **Status:** PROPOSED, docs only. **Board:** [entry](entries/2026-10-30-d-xlog-native-crosswalk.md), [STATUS_BOARD](STATUS_BOARD.md) D-XLOG-NATIVE. Crosswalk of XLOG's compiled-plan nodes onto the `ndarray::simd` polyfill that `lance-graph-onnx` aliases, in the D-ONNX-NATIVE categories (ALIAS / INLINE / NATIVE / REFUSE), name-checked, not tested; shared operations are the same native symbols as ONNX's. Decides that a `lance-graph-xlog` crate (ndarray only, like `lance-graph-onnx`; no `xlog-*` dependency, no plan type) waits until selection rows are tested and the many-to-many join has a native home.
 **Confidence:** name-checked crosswalk; no code.
+## 2026-10-30 — D-MIST-NATIVE: Mistaber's Kripke holdings as a vocabulary over existing algebra → `.claude/plans/d-mistaber-native-v1.md`
+
+**Status:** D-MIST-NATIVE-0 LAB PROBE (`crates/mistaber-kripke-probe`, own workspace); D-MIST-NATIVE-1..4 PROPOSED. **Board:** [entry](entries/2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md), [STATUS_BOARD](STATUS_BOARD.md) D-MIST-NATIVE. `holds` is a stratified least fixpoint over the existing DR64 `relcomp::compose`; holdings are one lens read by `WideFieldMask` selections, `holds/2` a Set projection. Endgame: an onnx-shaped `lance-graph-mistaber` facade, blocked on a production home for `compose`.
+**Confidence:** 11/11 Clingo goldens exact, 6 disable runs fail as expected; lab only, no timing.
 
 ## 2026-10-30 — D-LITHO: the photolithography contract → `.claude/plans/d-litho-photolithography-contract-v1.md`
 

.claude/board/STATUS_BOARD.md

@@ -1,3 +1,15 @@
+## D-MIST-NATIVE — Mistaber's Kripke holdings over the DR64 relation register (2026-10-30)
+
+**Status:** LAB PROBE; test-only, standalone crate, no production API. [Plan](../plans/d-mistaber-native-v1.md); [board entry](entries/2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md).
+
+| D-id | Deliverable | Status | Gate |
+|---|---|---|---|
+| D-MIST-NATIVE-0 | Kripke `holds` + rule/origin lineage as a least fixpoint over `relcomp::compose`; 11 Clingo goldens exact; holdings lens with Set/Bag projection; 6 disable runs | In PR | lab only |
+| D-MIST-NATIVE-1 | `lance-graph-mistaber`: onnx-shaped ALIAS/INLINE/REFUSE facade (plan §3) | Queued | production home for `compose` (plan Q1) |
+| D-MIST-NATIVE-2 | lineage origins into `SupportLedger` (`EvidenceSourceId`, `TextAttested`) | Queued | after D-MIST-NATIVE-1 |
+| D-MIST-NATIVE-3 | axes past 64 (worlds, propositions, rules) | Queued | refused today |
+| D-MIST-NATIVE-4 | intake from compiled HLL | Queued | upstream provenance defects (`mistaber-rs#3`, `#4`) |
+
 ## D-XLOG-NATIVE — XLOG plan vocabulary over the ndarray::simd polyfill, the algebra under lance-graph-onnx (2026-10-30)
 
 **Status:** PROPOSED / DOCS ONLY. [Plan](../plans/d-xlog-native-v1.md); [board entry](entries/2026-10-30-d-xlog-native-crosswalk.md). No crate yet.

.claude/board/entries/2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md

@@ -0,0 +1,11 @@
+# D-MIST-NATIVE-0 — Mistaber's Kripke holdings as a least fixpoint over DR64 compose
+
+**Date 2026-10-30 · Status LAB PROBE · Crate `crates/mistaber-kripke-probe` (standalone, not a member) · Goldens `AdaWorldAPI/mistaber-rs@f163fa7` (Clingo over `BrainyBlaze/mistaber@b50bf33`) · Plan `.claude/plans/d-mistaber-native-v1.md`**
+
+Upstream `kripke_rules.lp` is stratified: `holds` is recursive through `holds_via(inherited(Parent), …)`, and every negation (`overridden`, `asserts`, `endorses` at the child) is over inputs. So `holds` is the least fixpoint `H = H₀ ∪ ((H ∘ children) ∧ ¬Block)`, one existing `relcomp::compose` plus an AND-NOT per step. Rule and origin lineage are the same fixpoint gated by `H`. No new algebra; relalg (single-table selection, no `μ`) was the wrong host.
+
+All 11 goldens reproduce exactly: F1-modes, F1-reversed, F2-cycle, F5-gates, F6-undeclared-child, C-mammal-C2/C4/C6/C6i and E-xlog-plain/override. F3-naf (even negative cycle over `asserts/2`) is refused at export and stays with Clingo. 6 disable runs fail as expected. One guard, the `holds` gate on lineage, is also enforced at render time, so no golden can catch its removal; it has its own unit test. F5-gates was added because no earlier fixture exercised the world masks or that gate.
+
+Holdings are one lens (`proposition, world, mode, immediate_rule, source_rule`), and each predicate is a `WideFieldMask` selection over it. `holds/2` needs a **Set** projection: on the F1 diamond the lens has two rows for `holds(p,d)` and the bag reading fails the golden. The bag/set split was sent to XLOG for the #1866 crosswalk (EXO-50).
+
+**OPEN:** a production home for `compose` (blocks the `lance-graph-mistaber` facade); axes past 64; lineage into `SupportLedger` as `EvidenceSourceId`/`TextAttested`; intake from compiled HLL (expected refusals, `mistaber-rs#3`/`#4`); no timing taken.

.claude/board/entries/README.md

@@ -25,14 +25,15 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately
 opposite directions; the stranding this convention prevents shows up in
 exactly one of them, never both.
 
-510 entries, 2026-08-06 .. 2026-10-30.
+511 entries, 2026-08-06 .. 2026-10-30.
 
 | date | entry id | finding | file |
 |---|---|---|---|
 | 2026-10-30 | `D-XLOG-NATIVE-0` |  | [2026-10-30-d-xlog-native-crosswalk.md](2026-10-30-d-xlog-native-crosswalk.md) |
 | 2026-10-30 | `D-XLOG-DR64-0` | XLOG's CPU frontend lowers onto DR64 relcomp (answer {2}, 2 oracles); its optimizer emits ChainJoin and swapped orders; arrow 60 vs 58 blocks in-tree use; masks lose to scalar on selective data | [2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md](2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md) |
 | 2026-10-30 | `D-TRACT-SHAPE-1` |  | [2026-10-30-d-tract-shape-1-cold-shape-folding.md](2026-10-30-d-tract-shape-1-cold-shape-folding.md) |
 | 2026-10-30 | `D-TRACT-HARVEST-0` |  | [2026-10-30-d-tract-harvest-0-native-algebra-bridge.md](2026-10-30-d-tract-harvest-0-native-algebra-bridge.md) |
+| 2026-10-30 | `D-MIST-NATIVE-0` |  | [2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md](2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md) |
 | 2026-10-30 | `D-LITHO` |  | [2026-10-30-d-litho-photolithography-contract.md](2026-10-30-d-litho-photolithography-contract.md) |
 | 2026-10-30 | `D-LITHO-1` |  | [2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md](2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md) |
 | 2026-10-30 | `D-DT64-6-BS` |  | [2026-10-30-d-dt64-6-bs-bind-store-crate.md](2026-10-30-d-dt64-6-bs-bind-store-crate.md) |

.claude/plans/d-mistaber-native-v1.md

@@ -0,0 +1,103 @@
+# D-MIST-NATIVE — Mistaber's Kripke holdings as a vocabulary over existing algebra
+
+**Status:** D-MIST-NATIVE-0 LAB PROBE (this PR); D-MIST-NATIVE-1..4 PROPOSED.
+**Date:** 2026-10-30.
+**Upstream evidence:** `AdaWorldAPI/mistaber-rs` (`docs/D-MIST-RUFF-XLOG-0.md`, decision table §7; Clingo oracle; `goldens/`).
+**Claim:** EXO-50 `MIST-PROJECT-BAG-SET-20261030-02`.
+
+## 1. Overview
+
+The endgame is a `lance-graph-mistaber` crate wired like `lance-graph-onnx`. The crate holds no interpreter, graph or runtime. Each Mistaber operation is either an alias of an existing operation, a small adapter in front of one, or a typed refusal.
+
+The `mistaber-rs` harvest found that every operation it could carry natively is classes A or B in its decision table: relational selection, plus stratified negation over input relations. The stable-model features stay with Clingo. This plan does not port a solver or the HLL compiler.
+
+D-MIST-NATIVE-0 is the probe that tests this claim. Its findings:
+
+- **The recursion is `holds`, not `accessible_transitive`.** Upstream's `holds_via(inherited(Parent), P, Child)` reads `holds` at the parent. The only negations are `not overridden`, `not asserts` and `not endorses`, all at the child and all over inputs. The answer is therefore the least fixpoint
+
+  ```text
+  H₀   = (asserts ∪ endorses) ∧ world
+  Hₖ₊₁ = H₀ ∪ ((Hₖ ∘ children) ∧ ¬Block)      Block = asserts ∪ endorses ∪ overridden
+  ```
+
+  Each step is one `dr-math-binding-probe::relcomp::compose` and one AND-NOT. `accessible_transitive/2` is derived upstream, but no rule reads it and the goldens do not include it.
+- **The two lineages use the same fixpoint.** `holds_via_rule`'s source rule and `inheritance_source`'s origin are each that fixpoint, gated by the final `H`: one register per rule, one per origin world.
+- **relalg is the wrong host for the recursion.** It describes selections over one table; its docs say recursion (`μ`) and the hop are not built. The relation register and `compose` already exist in `dr-math-binding-probe`, which is what `xlog-relcomp-probe` uses as well.
+
+## 2. Checklist
+
+- [x] D-MIST-NATIVE-0: probe `crates/mistaber-kripke-probe` (own workspace root, CI workflow).
+  - Reproduces all 11 Clingo goldens exactly.
+  - 6 disable runs fail as expected.
+  - Bag/set falsifier on the diamond.
+  - Refusals: unknown fact, arity, 65th value on an axis, a selection that is no predicate.
+- [x] Goldens exported by `mistaber-rs` (`oracle/export_goldens.py`, `test_goldens.py`, F5-gates and F6-undeclared-child fixtures); F3-naf refused at export.
+- [ ] D-MIST-NATIVE-1: `lance-graph-mistaber`, an onnx-shaped facade (crosswalk §3). Blocked on a production home for `compose` (§6, Q1).
+- [ ] D-MIST-NATIVE-2: lineage origins into `SupportLedger` as `EvidenceSourceId` with `SupportBasis::TextAttested`. This is the only lawful route to Epi5 (#1863/#1868 closed the topology route for non-causal steps).
+- [ ] D-MIST-NATIVE-3: axes past 64 (worlds, propositions, rules). Refused today; tiling or a wider register is open.
+- [ ] D-MIST-NATIVE-4: intake from compiled HLL. Real-corpus holdings hit the upstream provenance defects (`mistaber-rs#3`, `#4`), so the expected outcome there is refusals, not values.
+
+## 3. Crosswalk (the facade D-MIST-NATIVE-1 would export)
+
+| Mistaber (`kripke_rules.lp`) | Class | Native |
+|---|---|---|
+| `holds_via(asserted/endorsed, P, W)` | ALIAS | the input relation ∧ world mask |
+| `holds_via(inherited(Wp), P, W)` | INLINE | `H[P]` has `Wp` → `children[Wp] ∧ ¬Block[P]` |
+| `holds(P, W)` | INLINE | the least fixpoint above (compose + AND-NOT) |
+| `holds/2`, `holds_via/3`, `holds_via_rule/5` as views | ALIAS | `WideFieldMask` selection over the holdings lens (§4), **Set** projection |
+| `holding_strength(strong/moderate/weak)` | INLINE | masks over direct and inherited-from-direct; a label, never an Epi5 code |
+| `inheritance_source`, `holds_via_rule` source | INLINE | the same fixpoint per origin or rule, gated by `H` |
+| `overridden(P, W)` | ALIAS | the input relation |
+| `accessible_transitive` | not exported | derived upstream, read by no rule |
+| negative cycles over inputs, choice, optimisation (F3-naf) | REFUSE | stays with Clingo |
+| taxonomy → worlds, strength → Epi5, `is_a` → Pearl3 | REFUSE | category errors (`mistaber-rs` `qualify.py`) |
+| a holding with no `holds_via_rule` (`mistaber-rs#3`) | REFUSE | `MissingProvenance` |
+
+## 4. The holdings lens and the bag/set split
+
+Following the field-view ruling (`ogar-consumer-preflight.md:277`, "Classview can be used for any compute masking"), holdings are one relation lens with fields `proposition, world, mode, immediate_rule, source_rule`. Each predicate is a `WideFieldMask` selection over it:
+
+- `holds/2` = {proposition, world};
+- `holds_via/3` adds mode;
+- `holds_via_rule/5` adds both rules.
+
+Provenance is therefore part of the same relation, not a side table. Worlds are values in the `world` field; they never take a classid. The lens id comes from the OGAR codebook through hotplug, as in `dto_binding.rs`. The probe uses no classid.
+
+A narrower selection can make two lens rows equal. In the diamond (F1), `p` holds in `d` by `inherited(a)` and by `inherited(b)`, so the lens has two rows but `holds(p,d)` is one fact. Mistaber's semantics are Datalog (set):
+
+| Projection | Maps to |
+|---|---|
+| bag (column subset, multiplicity kept) | ALIAS to the selection |
+| set (Datalog head) | the selection **followed by** a distinct/existence fold |
+
+A lens row is one (mode, source rule), or one (mode) with empty rule fields when the holding has no rule. Two rows can also share a mode: `p` holds in `e` only by `inherited(d)` but traces to two source rules, so a bag projection gives two `holds_via(inherited(d),p,e)` and two `holds(p,e)` (`bag_counts_lens_rows_not_modes`; caught in review on #1873, where Bag first counted modes). `set_projection_is_required_on_the_diamond` pins both: bag multiplicity 2, set count 1, and the bag reading does not reproduce the golden. `bag_and_set_agree_where_no_holding_has_two_modes` is the silence twin. The same split was sent to the XLOG session for the #1866 crosswalk (EXO-50).
+
+## 5. Evidence (D-MIST-NATIVE-0)
+
+`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 11 tests.
+
+Goldens: F1-modes, F1-reversed, F2-cycle, F5-gates, F6-undeclared-child, C-mammal-C2/C4/C6/C6i, E-xlog-plain/override. All are exact, compared as sorted lists, so a duplicate atom would also fail.
+
+Disable runs (each made after committing, red, then restored):
+
+| Disable | Fails |
+|---|---|
+| drop `¬Block` in the fixpoint | `every_golden_is_reproduced_exactly` |
+| count one bag row per mode instead of per (mode, source rule) | `bag_counts_lens_rows_not_modes` (`left: 1, right: 2`) |
+| drop the `holds` gate on lineage | `lineage_never_leaves_the_held_cells` (`left: 3, right: 1`) |
+| drop the world mask on direct holdings | `every_golden_…` (F5 ghost world) |
+| drop the world mask on rule atoms | `every_golden_…` (F5) |
+| moderate from any holding instead of direct | `every_golden_…` |
+
+The lineage gate is also enforced at render time (`inherited_from` checks `holds` at the parent). This is why the golden comparison could not catch its removal, and why it has its own unit test. F5-gates was added to `mistaber-rs` because no earlier fixture exercised the world mask or that gate. F6-undeclared-child pins the opposite case: upstream's inherited rule has no `world(W_child)` condition, so a holding reaches an undeclared child world, and the probe deliberately applies no world mask on inheritance (found in review on #1873).
+
+No timing was taken, and none is claimed. `mistaber-rs` §7 defers mask folds (class E) until a repeated workload exists.
+
+## 6. Open questions
+
+- **Q1 (blocks D-MIST-NATIVE-1):** `compose` lives in `dr-math-binding-probe`, a lab crate. A production `lance-graph-mistaber` cannot depend on it. Where should the Boolean relation register and `compose` live in production: ndarray's SIMD facade, the contract, or a native relation crate? `xlog-relcomp-probe` faces the same question; D-XLOG-NATIVE-3 asks the ndarray and mask-risc owners for a native home for its many-to-many join. Both should get one answer.
+- **Q2:** the lens classid comes from the OGAR codebook via hotplug, and none is minted. Does it need a concept, or a lab stand-in as in `dto_binding.rs`?
+
+## 7. Not in scope
+
+A port of the HLL compiler or Clingo. Stable-model semantics. Any CE64 bit, any Epi5 code. Writes to `BrainyBlaze/mistaber`.

.github/workflows/mistaber-kripke-probe.yml

@@ -0,0 +1,70 @@
+name: Mistaber Kripke Probe
+# Own [workspace] excluded from root tests; a lab gate, not production
+# admission. Mirrors egglog-r2il-probe.yml's toolchain setup: the pinned
+# toolchain from rust-toolchain.toml, never `stable`.
+on:
+  pull_request:
+    paths:
+      - "crates/mistaber-kripke-probe/**"
+      - "crates/dr-math-binding-probe/**"
+      - "crates/lance-graph-contract/**"
+      - "crates/lance-graph-act-r/**"
+      - "crates/lance-graph-quack/**"
+      - "crates/lance-graph-mask-risc/**"
+      - ".github/workflows/mistaber-kripke-probe.yml"
+      - "rust-toolchain.toml"
+  push:
+    branches: [main]
+    paths:
+      - "crates/mistaber-kripke-probe/**"
+      - "crates/dr-math-binding-probe/**"
+      - "crates/lance-graph-contract/**"
+      - "crates/lance-graph-act-r/**"
+      - "crates/lance-graph-quack/**"
+      - "crates/lance-graph-mask-risc/**"
+      - ".github/workflows/mistaber-kripke-probe.yml"
+      - "rust-toolchain.toml"
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+env:
+  CARGO_TERM_COLOR: always
+  CARGO_INCREMENTAL: "0"
+  CARGO_PROFILE_DEV_DEBUG: "0"
+  CARGO_PROFILE_TEST_DEBUG: "0"
+  RUST_BACKTRACE: "1"
+jobs:
+  isolated-probe:
+    name: excluded-crate fmt, clippy and tests
+    runs-on: ubuntu-24.04
+    timeout-minutes: 60
+    defaults:
+      run:
+        working-directory: lance-graph
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          path: lance-graph
+          persist-credentials: false
+      - name: Rust toolchain
+        run: rustup show
+      - name: Resolve target-cpu=native for this runner
+        id: cpu
+        run: |
+          flags=$(.github/scripts/resolve-native-rustflags.sh)
+          echo "RUSTFLAGS=$flags" >> "$GITHUB_ENV"
+          hash=$(printf %s "$flags" | sha256sum | cut -c1-16)
+          echo "flags=$hash" >> "$GITHUB_OUTPUT"
+      - uses: Swatinem/rust-cache@v2
+        with:
+          key: cpu-${{ steps.cpu.outputs.flags }}
+          workspaces: lance-graph/crates/mistaber-kripke-probe
+      - name: fmt
+        run: cargo fmt --manifest-path crates/mistaber-kripke-probe/Cargo.toml --check
+      - name: clippy
+        run: cargo clippy --manifest-path crates/mistaber-kripke-probe/Cargo.toml --all-targets -- -D warnings
+      - name: tests
+        run: cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml

crates/lance-graph-contract/src/morton8x8.rs

@@ -295,7 +295,11 @@ mod tests {
             for start in (0..=u16::MAX as u32).step_by(run as usize) {
                 let first = Morton8x8::from_code(start as u16);
                 let (x0, y0) = (u32::from(first.x()), u32::from(first.y()));
-                assert_eq!((x0 % side, y0 % side), (0, 0), "j={j} run {start}: corner not aligned");
+                assert_eq!(
+                    (x0 % side, y0 % side),
+                    (0, 0),
+                    "j={j} run {start}: corner not aligned"
+                );
                 let mut seen = vec![false; run as usize];
                 for c in start..start + run {
                     let m = Morton8x8::from_code(c as u16);

crates/mistaber-kripke-probe/Cargo.toml

@@ -0,0 +1,23 @@
+# D-MIST-NATIVE-0: isolated, test-only probe. NOT a workspace member, NOT a
+# runtime. Verify with
+#   cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml
+[package]
+name = "mistaber-kripke-probe"
+version = "0.0.0"
+edition = "2024"
+publish = false
+license = "MIT OR Apache-2.0"
+description = "Mistaber's Kripke holding rules as a least fixpoint over the existing DR64 Boolean relation register (dr-math-binding-probe::relcomp::compose), checked against Clingo golden files exported by AdaWorldAPI/mistaber-rs."
+
+# Own workspace root, like xlog-relcomp-probe: dr-math-binding-probe pulls
+# egglog by git, which must not enter the lance-graph graph.
+[workspace]
+
+[dependencies]
+# The relation register and its compose kernel. Public API only.
+dr-math-binding-probe = { path = "../dr-math-binding-probe" }
+# The holdings lens's field selection (ClassView x WideFieldMask).
+lance-graph-contract = { path = "../lance-graph-contract" }
+
+[patch."https://github.com/AdaWorldAPI/lance-graph"]
+lance-graph-contract = { path = "../lance-graph-contract" }

crates/mistaber-kripke-probe/goldens/C-mammal-C2.tsv

@@ -0,0 +1,11 @@
+# fixture	C-mammal-C2
+# upstream_commit	b50bf3323056793830c35795eace57e43caa23b5
+# kripke_lp_sha256	6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9
+# fixture_sha256	880c932d5efb0c5b45ecb11af429859e4fdda4437c600a663963bde10b196338
+fact	world	obs1
+fact	world	obs2
+fact	world	obs3
+fact	world	reader
+fact	accessible	obs2	obs1
+fact	accessible	reader	obs2
+fact	accessible	reader	obs3