diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index bcd25e4d7..185dfb18d 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.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` diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index ebf5636f0..f2e4371c9 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.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. diff --git a/.claude/board/entries/2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md b/.claude/board/entries/2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md new file mode 100644 index 000000000..46a4dbcd8 --- /dev/null +++ b/.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. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 8750a21ef..23dde95af 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ 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 | |---|---|---|---| @@ -33,6 +33,7 @@ exactly one of them, never both. | 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) | diff --git a/.claude/plans/d-mistaber-native-v1.md b/.claude/plans/d-mistaber-native-v1.md new file mode 100644 index 000000000..bd144e92c --- /dev/null +++ b/.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`. diff --git a/.github/workflows/mistaber-kripke-probe.yml b/.github/workflows/mistaber-kripke-probe.yml new file mode 100644 index 000000000..7103d5454 --- /dev/null +++ b/.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 diff --git a/crates/lance-graph-contract/src/morton8x8.rs b/crates/lance-graph-contract/src/morton8x8.rs index 7f63c8c20..cd21f1bf6 100644 --- a/crates/lance-graph-contract/src/morton8x8.rs +++ b/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); diff --git a/crates/mistaber-kripke-probe/Cargo.toml b/crates/mistaber-kripke-probe/Cargo.toml new file mode 100644 index 000000000..ea3c9f174 --- /dev/null +++ b/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" } diff --git a/crates/mistaber-kripke-probe/goldens/C-mammal-C2.tsv b/crates/mistaber-kripke-probe/goldens/C-mammal-C2.tsv new file mode 100644 index 000000000..7a8625d5a --- /dev/null +++ b/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 diff --git a/crates/mistaber-kripke-probe/goldens/C-mammal-C4.tsv b/crates/mistaber-kripke-probe/goldens/C-mammal-C4.tsv new file mode 100644 index 000000000..5276095b6 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/C-mammal-C4.tsv @@ -0,0 +1,28 @@ +# fixture C-mammal-C4 +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 50f8379ad953f8d86b01d545184ae6cd64ab45181c28c92659a434ed8659ea02 +fact world obs1 +fact world obs2 +fact world obs3 +fact world reader +fact accessible obs2 obs1 +fact accessible reader obs2 +fact accessible reader obs3 +fact asserts obs1 lays_eggs(platypus) +fact asserts_rule obs1 lays_eggs(platypus) r_obs1 +atom holding_strength(moderate,lays_eggs(platypus),obs2) +atom holding_strength(strong,lays_eggs(platypus),obs1) +atom holding_strength(weak,lays_eggs(platypus),reader) +atom holds(lays_eggs(platypus),obs1) +atom holds(lays_eggs(platypus),obs2) +atom holds(lays_eggs(platypus),reader) +atom holds_via(asserted,lays_eggs(platypus),obs1) +atom holds_via(inherited(obs1),lays_eggs(platypus),obs2) +atom holds_via(inherited(obs2),lays_eggs(platypus),reader) +atom holds_via_rule(asserted,lays_eggs(platypus),obs1,r_obs1,r_obs1) +atom holds_via_rule(inherited(obs1),lays_eggs(platypus),obs2,r_kripke_inherit,r_obs1) +atom holds_via_rule(inherited(obs2),lays_eggs(platypus),reader,r_kripke_inherit,r_obs1) +atom inheritance_source(lays_eggs(platypus),obs1,obs1) +atom inheritance_source(lays_eggs(platypus),obs2,obs1) +atom inheritance_source(lays_eggs(platypus),reader,obs1) diff --git a/crates/mistaber-kripke-probe/goldens/C-mammal-C6.tsv b/crates/mistaber-kripke-probe/goldens/C-mammal-C6.tsv new file mode 100644 index 000000000..65ccb65a6 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/C-mammal-C6.tsv @@ -0,0 +1,30 @@ +# fixture C-mammal-C6 +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 134b3908182ec5aacc1c137fc6ae0dfab5090a583a5a1d0115dc4f17594826dc +fact world obs1 +fact world obs2 +fact world obs3 +fact world reader +fact accessible obs2 obs1 +fact accessible reader obs2 +fact accessible reader obs3 +fact asserts obs1 lays_eggs(platypus) +fact asserts_rule obs1 lays_eggs(platypus) r_obs1 +fact endorses obs2 lays_eggs(platypus) +fact endorses_rule obs2 lays_eggs(platypus) r_obs2_endorse +atom holding_strength(moderate,lays_eggs(platypus),reader) +atom holding_strength(strong,lays_eggs(platypus),obs1) +atom holding_strength(strong,lays_eggs(platypus),obs2) +atom holds(lays_eggs(platypus),obs1) +atom holds(lays_eggs(platypus),obs2) +atom holds(lays_eggs(platypus),reader) +atom holds_via(asserted,lays_eggs(platypus),obs1) +atom holds_via(endorsed,lays_eggs(platypus),obs2) +atom holds_via(inherited(obs2),lays_eggs(platypus),reader) +atom holds_via_rule(asserted,lays_eggs(platypus),obs1,r_obs1,r_obs1) +atom holds_via_rule(endorsed,lays_eggs(platypus),obs2,r_obs2_endorse,r_obs2_endorse) +atom holds_via_rule(inherited(obs2),lays_eggs(platypus),reader,r_kripke_inherit,r_obs2_endorse) +atom inheritance_source(lays_eggs(platypus),obs1,obs1) +atom inheritance_source(lays_eggs(platypus),obs2,obs2) +atom inheritance_source(lays_eggs(platypus),reader,obs2) diff --git a/crates/mistaber-kripke-probe/goldens/C-mammal-C6i.tsv b/crates/mistaber-kripke-probe/goldens/C-mammal-C6i.tsv new file mode 100644 index 000000000..37f3a92c2 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/C-mammal-C6i.tsv @@ -0,0 +1,40 @@ +# fixture C-mammal-C6i +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 b046d3524ba3fb1b494bffc1b672c83a13990229040660c0bd873ee07670f6a1 +fact world obs1 +fact world obs2 +fact world obs3 +fact world reader +fact accessible obs2 obs1 +fact accessible reader obs2 +fact accessible reader obs3 +fact asserts obs1 lays_eggs(platypus) +fact asserts_rule obs1 lays_eggs(platypus) r_obs1 +fact endorses obs2 lays_eggs(platypus) +fact endorses_rule obs2 lays_eggs(platypus) r_obs2_endorse +fact asserts obs3 lays_eggs(platypus) +fact asserts_rule obs3 lays_eggs(platypus) r_obs3 +atom holding_strength(moderate,lays_eggs(platypus),reader) +atom holding_strength(strong,lays_eggs(platypus),obs1) +atom holding_strength(strong,lays_eggs(platypus),obs2) +atom holding_strength(strong,lays_eggs(platypus),obs3) +atom holds(lays_eggs(platypus),obs1) +atom holds(lays_eggs(platypus),obs2) +atom holds(lays_eggs(platypus),obs3) +atom holds(lays_eggs(platypus),reader) +atom holds_via(asserted,lays_eggs(platypus),obs1) +atom holds_via(asserted,lays_eggs(platypus),obs3) +atom holds_via(endorsed,lays_eggs(platypus),obs2) +atom holds_via(inherited(obs2),lays_eggs(platypus),reader) +atom holds_via(inherited(obs3),lays_eggs(platypus),reader) +atom holds_via_rule(asserted,lays_eggs(platypus),obs1,r_obs1,r_obs1) +atom holds_via_rule(asserted,lays_eggs(platypus),obs3,r_obs3,r_obs3) +atom holds_via_rule(endorsed,lays_eggs(platypus),obs2,r_obs2_endorse,r_obs2_endorse) +atom holds_via_rule(inherited(obs2),lays_eggs(platypus),reader,r_kripke_inherit,r_obs2_endorse) +atom holds_via_rule(inherited(obs3),lays_eggs(platypus),reader,r_kripke_inherit,r_obs3) +atom inheritance_source(lays_eggs(platypus),obs1,obs1) +atom inheritance_source(lays_eggs(platypus),obs2,obs2) +atom inheritance_source(lays_eggs(platypus),obs3,obs3) +atom inheritance_source(lays_eggs(platypus),reader,obs2) +atom inheritance_source(lays_eggs(platypus),reader,obs3) diff --git a/crates/mistaber-kripke-probe/goldens/E-xlog-override.tsv b/crates/mistaber-kripke-probe/goldens/E-xlog-override.tsv new file mode 100644 index 000000000..72c007a27 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/E-xlog-override.tsv @@ -0,0 +1,76 @@ +# fixture E-xlog-override +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 52c34f88425da820335a7e07d131883b21814ba03b98ea7ca039a3faaefd7d91 +fact world src +fact world curated +fact accessible curated src +fact asserts src r(1,2) +fact asserts_rule src r(1,2) r_R_0 +fact asserts src r(1,3) +fact asserts_rule src r(1,3) r_R_1 +fact asserts src r(9,7) +fact asserts_rule src r(9,7) r_R_2 +fact asserts src s(2,4) +fact asserts_rule src s(2,4) r_S_0 +fact asserts src s(3,5) +fact asserts_rule src s(3,5) r_S_1 +fact asserts src s(7,4) +fact asserts_rule src s(7,4) r_S_2 +fact override curated r(1,2) retracted +atom holding_strength(moderate,r(1,3),curated) +atom holding_strength(moderate,r(9,7),curated) +atom holding_strength(moderate,s(2,4),curated) +atom holding_strength(moderate,s(3,5),curated) +atom holding_strength(moderate,s(7,4),curated) +atom holding_strength(strong,r(1,2),src) +atom holding_strength(strong,r(1,3),src) +atom holding_strength(strong,r(9,7),src) +atom holding_strength(strong,s(2,4),src) +atom holding_strength(strong,s(3,5),src) +atom holding_strength(strong,s(7,4),src) +atom holds(r(1,2),src) +atom holds(r(1,3),curated) +atom holds(r(1,3),src) +atom holds(r(9,7),curated) +atom holds(r(9,7),src) +atom holds(s(2,4),curated) +atom holds(s(2,4),src) +atom holds(s(3,5),curated) +atom holds(s(3,5),src) +atom holds(s(7,4),curated) +atom holds(s(7,4),src) +atom holds_via(asserted,r(1,2),src) +atom holds_via(asserted,r(1,3),src) +atom holds_via(asserted,r(9,7),src) +atom holds_via(asserted,s(2,4),src) +atom holds_via(asserted,s(3,5),src) +atom holds_via(asserted,s(7,4),src) +atom holds_via(inherited(src),r(1,3),curated) +atom holds_via(inherited(src),r(9,7),curated) +atom holds_via(inherited(src),s(2,4),curated) +atom holds_via(inherited(src),s(3,5),curated) +atom holds_via(inherited(src),s(7,4),curated) +atom holds_via_rule(asserted,r(1,2),src,r_R_0,r_R_0) +atom holds_via_rule(asserted,r(1,3),src,r_R_1,r_R_1) +atom holds_via_rule(asserted,r(9,7),src,r_R_2,r_R_2) +atom holds_via_rule(asserted,s(2,4),src,r_S_0,r_S_0) +atom holds_via_rule(asserted,s(3,5),src,r_S_1,r_S_1) +atom holds_via_rule(asserted,s(7,4),src,r_S_2,r_S_2) +atom holds_via_rule(inherited(src),r(1,3),curated,r_kripke_inherit,r_R_1) +atom holds_via_rule(inherited(src),r(9,7),curated,r_kripke_inherit,r_R_2) +atom holds_via_rule(inherited(src),s(2,4),curated,r_kripke_inherit,r_S_0) +atom holds_via_rule(inherited(src),s(3,5),curated,r_kripke_inherit,r_S_1) +atom holds_via_rule(inherited(src),s(7,4),curated,r_kripke_inherit,r_S_2) +atom inheritance_source(r(1,2),src,src) +atom inheritance_source(r(1,3),curated,src) +atom inheritance_source(r(1,3),src,src) +atom inheritance_source(r(9,7),curated,src) +atom inheritance_source(r(9,7),src,src) +atom inheritance_source(s(2,4),curated,src) +atom inheritance_source(s(2,4),src,src) +atom inheritance_source(s(3,5),curated,src) +atom inheritance_source(s(3,5),src,src) +atom inheritance_source(s(7,4),curated,src) +atom inheritance_source(s(7,4),src,src) +atom overridden(r(1,2),curated) diff --git a/crates/mistaber-kripke-probe/goldens/E-xlog-plain.tsv b/crates/mistaber-kripke-probe/goldens/E-xlog-plain.tsv new file mode 100644 index 000000000..f1a5f150b --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/E-xlog-plain.tsv @@ -0,0 +1,79 @@ +# fixture E-xlog-plain +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 cf2c41848cfc5072cfea504293bc1e9a3851bc9fcd1408719f41c799dadcf8ac +fact world src +fact world curated +fact accessible curated src +fact asserts src r(1,2) +fact asserts_rule src r(1,2) r_R_0 +fact asserts src r(1,3) +fact asserts_rule src r(1,3) r_R_1 +fact asserts src r(9,7) +fact asserts_rule src r(9,7) r_R_2 +fact asserts src s(2,4) +fact asserts_rule src s(2,4) r_S_0 +fact asserts src s(3,5) +fact asserts_rule src s(3,5) r_S_1 +fact asserts src s(7,4) +fact asserts_rule src s(7,4) r_S_2 +atom holding_strength(moderate,r(1,2),curated) +atom holding_strength(moderate,r(1,3),curated) +atom holding_strength(moderate,r(9,7),curated) +atom holding_strength(moderate,s(2,4),curated) +atom holding_strength(moderate,s(3,5),curated) +atom holding_strength(moderate,s(7,4),curated) +atom holding_strength(strong,r(1,2),src) +atom holding_strength(strong,r(1,3),src) +atom holding_strength(strong,r(9,7),src) +atom holding_strength(strong,s(2,4),src) +atom holding_strength(strong,s(3,5),src) +atom holding_strength(strong,s(7,4),src) +atom holds(r(1,2),curated) +atom holds(r(1,2),src) +atom holds(r(1,3),curated) +atom holds(r(1,3),src) +atom holds(r(9,7),curated) +atom holds(r(9,7),src) +atom holds(s(2,4),curated) +atom holds(s(2,4),src) +atom holds(s(3,5),curated) +atom holds(s(3,5),src) +atom holds(s(7,4),curated) +atom holds(s(7,4),src) +atom holds_via(asserted,r(1,2),src) +atom holds_via(asserted,r(1,3),src) +atom holds_via(asserted,r(9,7),src) +atom holds_via(asserted,s(2,4),src) +atom holds_via(asserted,s(3,5),src) +atom holds_via(asserted,s(7,4),src) +atom holds_via(inherited(src),r(1,2),curated) +atom holds_via(inherited(src),r(1,3),curated) +atom holds_via(inherited(src),r(9,7),curated) +atom holds_via(inherited(src),s(2,4),curated) +atom holds_via(inherited(src),s(3,5),curated) +atom holds_via(inherited(src),s(7,4),curated) +atom holds_via_rule(asserted,r(1,2),src,r_R_0,r_R_0) +atom holds_via_rule(asserted,r(1,3),src,r_R_1,r_R_1) +atom holds_via_rule(asserted,r(9,7),src,r_R_2,r_R_2) +atom holds_via_rule(asserted,s(2,4),src,r_S_0,r_S_0) +atom holds_via_rule(asserted,s(3,5),src,r_S_1,r_S_1) +atom holds_via_rule(asserted,s(7,4),src,r_S_2,r_S_2) +atom holds_via_rule(inherited(src),r(1,2),curated,r_kripke_inherit,r_R_0) +atom holds_via_rule(inherited(src),r(1,3),curated,r_kripke_inherit,r_R_1) +atom holds_via_rule(inherited(src),r(9,7),curated,r_kripke_inherit,r_R_2) +atom holds_via_rule(inherited(src),s(2,4),curated,r_kripke_inherit,r_S_0) +atom holds_via_rule(inherited(src),s(3,5),curated,r_kripke_inherit,r_S_1) +atom holds_via_rule(inherited(src),s(7,4),curated,r_kripke_inherit,r_S_2) +atom inheritance_source(r(1,2),curated,src) +atom inheritance_source(r(1,2),src,src) +atom inheritance_source(r(1,3),curated,src) +atom inheritance_source(r(1,3),src,src) +atom inheritance_source(r(9,7),curated,src) +atom inheritance_source(r(9,7),src,src) +atom inheritance_source(s(2,4),curated,src) +atom inheritance_source(s(2,4),src,src) +atom inheritance_source(s(3,5),curated,src) +atom inheritance_source(s(3,5),src,src) +atom inheritance_source(s(7,4),curated,src) +atom inheritance_source(s(7,4),src,src) diff --git a/crates/mistaber-kripke-probe/goldens/F1-modes.tsv b/crates/mistaber-kripke-probe/goldens/F1-modes.tsv new file mode 100644 index 000000000..a8bd0fcd5 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/F1-modes.tsv @@ -0,0 +1,78 @@ +# fixture F1-modes +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 c8758fa9edd41cd5e475734cd8406144ae046ec95c24cd57eb04c45655888588 +fact world base +fact world a +fact world b +fact world c +fact world d +fact world e +fact asserts base p +fact asserts_rule base p r_base_p +fact accessible a base +fact accessible b base +fact endorses b p +fact endorses_rule b p r_b_endorse +fact accessible c base +fact override c p q +fact accessible d a +fact accessible d b +fact accessible e d +fact asserts base g +atom holding_strength(moderate,g,a) +atom holding_strength(moderate,g,b) +atom holding_strength(moderate,g,c) +atom holding_strength(moderate,p,a) +atom holding_strength(moderate,p,d) +atom holding_strength(strong,g,base) +atom holding_strength(strong,p,b) +atom holding_strength(strong,p,base) +atom holding_strength(weak,g,d) +atom holding_strength(weak,g,e) +atom holding_strength(weak,p,e) +atom holds(g,a) +atom holds(g,b) +atom holds(g,base) +atom holds(g,c) +atom holds(g,d) +atom holds(g,e) +atom holds(p,a) +atom holds(p,b) +atom holds(p,base) +atom holds(p,d) +atom holds(p,e) +atom holds_via(asserted,g,base) +atom holds_via(asserted,p,base) +atom holds_via(endorsed,p,b) +atom holds_via(inherited(a),g,d) +atom holds_via(inherited(a),p,d) +atom holds_via(inherited(b),g,d) +atom holds_via(inherited(b),p,d) +atom holds_via(inherited(base),g,a) +atom holds_via(inherited(base),g,b) +atom holds_via(inherited(base),g,c) +atom holds_via(inherited(base),p,a) +atom holds_via(inherited(d),g,e) +atom holds_via(inherited(d),p,e) +atom holds_via_rule(asserted,p,base,r_base_p,r_base_p) +atom holds_via_rule(endorsed,p,b,r_b_endorse,r_b_endorse) +atom holds_via_rule(inherited(a),p,d,r_kripke_inherit,r_base_p) +atom holds_via_rule(inherited(b),p,d,r_kripke_inherit,r_b_endorse) +atom holds_via_rule(inherited(base),p,a,r_kripke_inherit,r_base_p) +atom holds_via_rule(inherited(d),p,e,r_kripke_inherit,r_b_endorse) +atom holds_via_rule(inherited(d),p,e,r_kripke_inherit,r_base_p) +atom inheritance_source(g,a,base) +atom inheritance_source(g,b,base) +atom inheritance_source(g,base,base) +atom inheritance_source(g,c,base) +atom inheritance_source(g,d,base) +atom inheritance_source(g,e,base) +atom inheritance_source(p,a,base) +atom inheritance_source(p,b,b) +atom inheritance_source(p,base,base) +atom inheritance_source(p,d,b) +atom inheritance_source(p,d,base) +atom inheritance_source(p,e,b) +atom inheritance_source(p,e,base) +atom overridden(p,c) diff --git a/crates/mistaber-kripke-probe/goldens/F1-reversed.tsv b/crates/mistaber-kripke-probe/goldens/F1-reversed.tsv new file mode 100644 index 000000000..eea1b14bd --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/F1-reversed.tsv @@ -0,0 +1,63 @@ +# fixture F1-reversed +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 174928c11850e5d35d4b4ecf692fc951bfbf59cbdf0f949cd2a851059af864f6 +fact world base +fact world a +fact world b +fact world c +fact world d +fact world e +fact asserts base p +fact asserts_rule base p r_base_p +fact accessible base a +fact accessible b base +fact endorses b p +fact endorses_rule b p r_b_endorse +fact accessible c base +fact override c p q +fact accessible d a +fact accessible d b +fact accessible e d +fact asserts base g +atom holding_strength(moderate,g,b) +atom holding_strength(moderate,g,c) +atom holding_strength(moderate,p,d) +atom holding_strength(strong,g,base) +atom holding_strength(strong,p,b) +atom holding_strength(strong,p,base) +atom holding_strength(weak,g,d) +atom holding_strength(weak,g,e) +atom holding_strength(weak,p,e) +atom holds(g,b) +atom holds(g,base) +atom holds(g,c) +atom holds(g,d) +atom holds(g,e) +atom holds(p,b) +atom holds(p,base) +atom holds(p,d) +atom holds(p,e) +atom holds_via(asserted,g,base) +atom holds_via(asserted,p,base) +atom holds_via(endorsed,p,b) +atom holds_via(inherited(b),g,d) +atom holds_via(inherited(b),p,d) +atom holds_via(inherited(base),g,b) +atom holds_via(inherited(base),g,c) +atom holds_via(inherited(d),g,e) +atom holds_via(inherited(d),p,e) +atom holds_via_rule(asserted,p,base,r_base_p,r_base_p) +atom holds_via_rule(endorsed,p,b,r_b_endorse,r_b_endorse) +atom holds_via_rule(inherited(b),p,d,r_kripke_inherit,r_b_endorse) +atom holds_via_rule(inherited(d),p,e,r_kripke_inherit,r_b_endorse) +atom inheritance_source(g,b,base) +atom inheritance_source(g,base,base) +atom inheritance_source(g,c,base) +atom inheritance_source(g,d,base) +atom inheritance_source(g,e,base) +atom inheritance_source(p,b,b) +atom inheritance_source(p,base,base) +atom inheritance_source(p,d,b) +atom inheritance_source(p,e,b) +atom overridden(p,c) diff --git a/crates/mistaber-kripke-probe/goldens/F2-cycle.tsv b/crates/mistaber-kripke-probe/goldens/F2-cycle.tsv new file mode 100644 index 000000000..b45c9a857 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/F2-cycle.tsv @@ -0,0 +1,17 @@ +# fixture F2-cycle +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 3148c09d8414db582b9e69343d3bfc142a755c17f369b6d05588deeb630756d5 +fact world x +fact world y +fact world z +fact accessible x y +fact accessible y x +fact accessible z x +fact asserts z t +fact asserts_rule z t r_z_t +atom holding_strength(strong,t,z) +atom holds(t,z) +atom holds_via(asserted,t,z) +atom holds_via_rule(asserted,t,z,r_z_t,r_z_t) +atom inheritance_source(t,z,z) diff --git a/crates/mistaber-kripke-probe/goldens/F5-gates.tsv b/crates/mistaber-kripke-probe/goldens/F5-gates.tsv new file mode 100644 index 000000000..c27d2bc92 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/F5-gates.tsv @@ -0,0 +1,12 @@ +# fixture F5-gates +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 2cabddeb6c458e43d9563e71f361488458c64c6567bf6dc85c1f980f9e124a47 +fact world base +fact world a +fact accessible a base +fact asserts_rule base p r_orphan +fact accessible a ghost +fact asserts ghost h +fact asserts_rule ghost h r_ghost +atom holds_via_rule(asserted,p,base,r_orphan,r_orphan) diff --git a/crates/mistaber-kripke-probe/goldens/F6-undeclared-child.tsv b/crates/mistaber-kripke-probe/goldens/F6-undeclared-child.tsv new file mode 100644 index 000000000..c9c8dbb8d --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/F6-undeclared-child.tsv @@ -0,0 +1,18 @@ +# fixture F6-undeclared-child +# upstream_commit b50bf3323056793830c35795eace57e43caa23b5 +# kripke_lp_sha256 6c55720475add0f81915c46a84da8146235cee38dffa0db73e72a7bf0e58a9e9 +# fixture_sha256 403d77f552a6a3bf76f9329f303c9e393138c1dc103ea22aa835ec0829f50f9a +fact world base +fact asserts base p +fact asserts_rule base p r_base_p +fact accessible x base +atom holding_strength(moderate,p,x) +atom holding_strength(strong,p,base) +atom holds(p,base) +atom holds(p,x) +atom holds_via(asserted,p,base) +atom holds_via(inherited(base),p,x) +atom holds_via_rule(asserted,p,base,r_base_p,r_base_p) +atom holds_via_rule(inherited(base),p,x,r_kripke_inherit,r_base_p) +atom inheritance_source(p,base,base) +atom inheritance_source(p,x,base) diff --git a/crates/mistaber-kripke-probe/goldens/SOURCE b/crates/mistaber-kripke-probe/goldens/SOURCE new file mode 100644 index 000000000..48d6f9c20 --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/SOURCE @@ -0,0 +1,4 @@ +Copied verbatim from AdaWorldAPI/mistaber-rs@62e2382 goldens/ +(oracle/export_goldens.py: Clingo over BrainyBlaze/mistaber@b50bf33 +mistaber/ontology/worlds/kripke_rules.lp, sha256 in each file's header). +Regenerate there, then copy; never edit here. diff --git a/crates/mistaber-kripke-probe/src/lib.rs b/crates/mistaber-kripke-probe/src/lib.rs new file mode 100644 index 000000000..551d37755 --- /dev/null +++ b/crates/mistaber-kripke-probe/src/lib.rs @@ -0,0 +1,588 @@ +//! D-MIST-NATIVE-0: Mistaber's Kripke holding rules as a least fixpoint over +//! the existing DR64 Boolean relation register. +//! +//! Plan: `.claude/plans/d-mistaber-native-v1.md`. Reference answers: Clingo +//! golden files exported by `AdaWorldAPI/mistaber-rs` (`goldens/SOURCE`). +//! +//! # The fixpoint +//! +//! Upstream `kripke_rules.lp` makes `holds` recursive through +//! `holds_via(inherited(Parent), P, Child)`, and every negation in that rule +//! is over INPUT relations (`override`, `asserts`, `endorses` at the child). +//! The program is therefore stratified and its answer is the least fixpoint +//! +//! ```text +//! H₀ = (asserts ∪ endorses) ∧ world +//! Hₖ₊₁ = H₀ ∪ ((Hₖ ∘ children) ∧ ¬Block) Block = asserts ∪ endorses ∪ overridden +//! ``` +//! +//! with `H` a proposition × world relation and `children` the world × world +//! relation `parent → child`. Each step is one +//! [`compose`](dr_math_binding_probe::relcomp::compose) plus an AND-NOT: no new +//! algebra. The two lineages (`holds_via_rule`'s source rule and +//! `inheritance_source`'s origin) are the same fixpoint gated by the final +//! `H`, one per rule or origin. +//! +//! # The holdings lens +//! +//! Holdings are read through one lens whose fields are [`HOLDINGS_FIELDS`]. +//! A predicate is a [`WideFieldMask`] selection over it: `holds/2` selects +//! proposition and world, `holds_via/3` adds the mode, `holds_via_rule/5` +//! adds both rules. Selecting fewer fields can make two lens rows equal, so +//! the projection is [`Projection::Set`] (Datalog: one fact) or +//! [`Projection::Bag`] (one row per lens row). Only `Set` is Mistaber's +//! semantics; `Bag` exists to show where an alias-only reading goes wrong. +//! +//! # Not covered, refused +//! +//! Anything that is not one fixpoint of facts: a fact kind outside the Kripke +//! inputs, more than 64 worlds, propositions or rules (one register), and a +//! selection that is not one of the three predicates. +#![forbid(unsafe_code)] + +use dr_math_binding_probe::relcomp::{Rows, Work, compose}; +use lance_graph_contract::class_view::WideFieldMask; + +/// The slot count of one register axis. +pub const SLOTS: usize = 64; + +/// The holdings lens's fields, by position. +pub const HOLDINGS_FIELDS: [&str; 5] = [ + "proposition", + "world", + "mode", + "immediate_rule", + "source_rule", +]; +const F_PROP: u8 = 0; +const F_WORLD: u8 = 1; +const F_MODE: u8 = 2; +const F_IMMEDIATE: u8 = 3; +const F_SOURCE: u8 = 4; + +/// The immediate rule upstream attributes every inherited holding to. +const INHERIT_RULE: &str = "r_kripke_inherit"; + +/// Why an input or a selection is refused. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Refusal { + /// A fact kind the Kripke rules do not read. + UnknownFact(String), + /// A known fact kind with the wrong number of arguments. + Arity(String), + /// More than [`SLOTS`] distinct values on one axis. + TooMany(&'static str), + /// A golden line that is neither header, fact nor atom. + Format(String), + /// A field selection that is not `holds/2`, `holds_via/3` or + /// `holds_via_rule/5`. + Selection, +} + +/// How a narrower selection treats rows that become equal. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Projection { + /// One row per distinct value of the selected fields (Datalog). + Set, + /// One row per lens row. + Bag, +} + +#[derive(Default)] +struct Interner(Vec); + +impl Interner { + fn id(&mut self, name: &str, axis: &'static str) -> Result { + if let Some(i) = self.0.iter().position(|n| n == name) { + return Ok(i); + } + if self.0.len() == SLOTS { + return Err(Refusal::TooMany(axis)); + } + self.0.push(name.to_owned()); + Ok(self.0.len() - 1) + } +} + +/// A golden file: its fixture id, input facts and expected atoms. +pub struct Golden { + pub fixture_id: String, + pub facts: Vec>, + pub atoms: Vec, +} + +/// Parse one golden TSV. +pub fn parse_golden(text: &str) -> Result { + let mut g = Golden { + fixture_id: String::new(), + facts: Vec::new(), + atoms: Vec::new(), + }; + for line in text.lines() { + let mut cols = line.split('\t'); + match cols.next() { + Some("# fixture") => g.fixture_id = cols.next().unwrap_or_default().to_owned(), + Some(h) if h.starts_with('#') => {} + Some("fact") => g.facts.push(cols.map(str::to_owned).collect()), + Some("atom") => g.atoms.push(cols.collect::>().join("\t")), + _ => return Err(Refusal::Format(line.to_owned())), + } + } + Ok(g) +} + +fn or(a: &Rows, b: &Rows) -> Rows { + std::array::from_fn(|i| a[i] | b[i]) +} + +fn and(a: &Rows, b: &Rows) -> Rows { + std::array::from_fn(|i| a[i] & b[i]) +} + +fn and_not(a: &Rows, b: &Rows) -> Rows { + std::array::from_fn(|i| a[i] & !b[i]) +} + +fn and_row(a: &Rows, m: u64) -> Rows { + std::array::from_fn(|i| a[i] & m) +} + +fn bits(mut x: u64) -> impl Iterator { + std::iter::from_fn(move || { + (x != 0).then(|| { + let b = x.trailing_zeros() as usize; + x &= x - 1; + b + }) + }) +} + +/// The Kripke inputs, one register per relation. +pub struct Kb { + worlds: Interner, + props: Interner, + rules: Interner, + world_set: u64, + asserts: Rows, + endorses: Rows, + overridden: Rows, + /// Row `parent`, bit `child`: `accessible(child, parent)`. + children: Rows, + asserts_rule: Vec, + endorses_rule: Vec, +} + +impl Kb { + /// Load fact tuples (`kind, args…`). Refuses any fact kind the Kripke + /// rules do not read. + pub fn load(facts: &[Vec]) -> Result { + let mut kb = Kb { + worlds: Interner::default(), + props: Interner::default(), + rules: Interner::default(), + world_set: 0, + asserts: [0; SLOTS], + endorses: [0; SLOTS], + overridden: [0; SLOTS], + children: [0; SLOTS], + asserts_rule: Vec::new(), + endorses_rule: Vec::new(), + }; + for f in facts { + let (kind, args) = f.split_first().ok_or(Refusal::Format(String::new()))?; + let want = match kind.as_str() { + "world" => 1, + "asserts" | "endorses" | "accessible" => 2, + "override" | "asserts_rule" | "endorses_rule" => 3, + _ => return Err(Refusal::UnknownFact(kind.clone())), + }; + if args.len() != want { + return Err(Refusal::Arity(kind.clone())); + } + match kind.as_str() { + "world" => kb.world_set |= 1 << kb.worlds.id(&args[0], "world")?, + "accessible" => { + let child = kb.worlds.id(&args[0], "world")?; + let parent = kb.worlds.id(&args[1], "world")?; + kb.children[parent] |= 1 << child; + } + _ => { + let w = kb.worlds.id(&args[0], "world")?; + let p = kb.props.id(&args[1], "proposition")?; + match kind.as_str() { + "asserts" => kb.asserts[p] |= 1 << w, + "endorses" => kb.endorses[p] |= 1 << w, + "override" => kb.overridden[p] |= 1 << w, + _ => { + let r = kb.rules.id(&args[2], "rule")?; + for v in [&mut kb.asserts_rule, &mut kb.endorses_rule] { + v.resize(kb.rules.0.len(), [0; SLOTS]); + } + let table = if kind == "asserts_rule" { + &mut kb.asserts_rule + } else { + &mut kb.endorses_rule + }; + table[r][p] |= 1 << w; + } + } + } + } + } + Ok(kb) + } + + /// Solve: the holds fixpoint, then both lineages. + pub fn solve(&self) -> Holdings<'_> { + let mut work = Work::default(); + let block = or(&or(&self.asserts, &self.endorses), &self.overridden); + let direct = and_row(&or(&self.asserts, &self.endorses), self.world_set); + let (holds, steps) = lfp(&direct, None, &self.children, &block, &mut work); + let lineage = + |base: &Rows, work: &mut Work| lfp(base, Some(&holds), &self.children, &block, work).0; + let sources = (0..self.rules.0.len()) + .map(|r| { + let base = and_row( + &or(&self.asserts_rule[r], &self.endorses_rule[r]), + self.world_set, + ); + lineage(&base, &mut work) + }) + .collect(); + let origins = (0..self.worlds.0.len()) + .map(|o| lineage(&and_row(&direct, 1 << o), &mut work)) + .collect(); + Holdings { + kb: self, + block, + direct, + holds, + sources, + origins, + steps, + work, + } + } +} + +/// `X = base ∪ ((gate(X) ∘ children) ∧ ¬block)` to its least fixpoint. +/// `gate = None` gates by `X` itself; `Some(h)` gates by `X ∧ h`. +fn lfp( + base: &Rows, + gate: Option<&Rows>, + children: &Rows, + block: &Rows, + work: &mut Work, +) -> (Rows, usize) { + let mut cur = *base; + for step in 1..=SLOTS + 1 { + let from = gate.map_or(cur, |h| and(&cur, h)); + let next = or(base, &and_not(&compose(&from, children, work), block)); + if next == cur { + return (cur, step); + } + cur = next; + } + unreachable!( + "each step extends every proposition by one hop; 64 worlds have no path longer than 63 hops" + ) +} + +/// One holding mode: its cells, and per rule the cells that rule supports. +struct Mode { + label: String, + cells: Rows, + rules: Vec, +} + +impl Mode { + /// Lens rows at `(p, w)`: one per supporting rule, one if the holding has + /// none, zero if the mode does not hold there. + fn rows(&self, p: usize, w: usize) -> usize { + if self.cells[p] >> w & 1 == 0 { + return 0; + } + self.rules + .iter() + .filter(|r| r[p] >> w & 1 == 1) + .count() + .max(1) + } +} + +/// The solved holdings lens. +pub struct Holdings<'a> { + kb: &'a Kb, + block: Rows, + direct: Rows, + holds: Rows, + /// Per rule: the (proposition, world) cells whose holding traces to it. + sources: Vec, + /// Per origin world: the cells whose holding traces to it. + origins: Vec, + /// Fixpoint steps of `holds`, the last one confirming no change. + pub steps: usize, + /// Row ORs the compose kernel performed. + pub work: Work, +} + +impl Holdings<'_> { + fn w(&self, i: usize) -> &str { + &self.kb.worlds.0[i] + } + + fn p(&self, i: usize) -> &str { + &self.kb.props.0[i] + } + + /// `holds_via(inherited(parent), p, ·)` as a world mask. + fn inherited_from(&self, parent: usize, p: usize) -> u64 { + if self.holds[p] >> parent & 1 == 0 { + return 0; + } + self.kb.children[parent] & !self.block[p] + } + + /// Every mode with its cells and, per rule, the cells that rule supports + /// under that mode. + fn modes(&self) -> Vec { + let kb = self.kb; + let n = kb.props.0.len(); + let direct = |table: &Rows, rules: &[Rows]| Mode { + cells: and_row(table, kb.world_set), + rules: rules + .iter() + .map(|r| and(r, &and_row(table, kb.world_set))) + .collect(), + label: String::new(), + }; + let mut out = vec![ + Mode { + label: "asserted".to_owned(), + ..direct(&kb.asserts, &kb.asserts_rule) + }, + Mode { + label: "endorsed".to_owned(), + ..direct(&kb.endorses, &kb.endorses_rule) + }, + ]; + for par in 0..kb.worlds.0.len() { + let cells: Rows = std::array::from_fn(|p| { + if p < n { + self.inherited_from(par, p) + } else { + 0 + } + }); + let rules = self + .sources + .iter() + .map(|src| { + std::array::from_fn(|p| if src[p] >> par & 1 == 1 { cells[p] } else { 0 }) + }) + .collect(); + out.push(Mode { + label: format!("inherited({})", self.w(par)), + cells, + rules, + }); + } + out + } + + /// How many lens rows hold `p` in `w`: the multiplicity a bag projection + /// to `holds/2` reports. A lens row is one (mode, source rule); a holding + /// with no rule is one row with empty rule fields. + pub fn bag_multiplicity(&self, prop: &str, world: &str) -> usize { + let (Some(p), Some(w)) = ( + self.kb.props.0.iter().position(|n| n == prop), + self.kb.worlds.0.iter().position(|n| n == world), + ) else { + return 0; + }; + self.modes().iter().map(|m| m.rows(p, w)).sum() + } + + /// Materialize one predicate as atoms: a [`WideFieldMask`] selection over + /// [`HOLDINGS_FIELDS`]. For the test oracle only. + pub fn materialize_selection( + &self, + sel: &WideFieldMask, + proj: Projection, + ) -> Result, Refusal> { + let has = |f| sel.has(f); + let base = has(F_PROP) && has(F_WORLD); + let mut out = Vec::new(); + match ( + base, + has(F_MODE), + has(F_IMMEDIATE), + has(F_SOURCE), + sel.count(), + ) { + (true, false, false, false, 2) => match proj { + Projection::Set => { + for p in 0..self.kb.props.0.len() { + for w in bits(self.holds[p]) { + out.push(format!("holds({},{})", self.p(p), self.w(w))); + } + } + } + Projection::Bag => { + for m in self.modes() { + for (p, &row) in m.cells.iter().enumerate().take(self.kb.props.0.len()) { + for w in bits(row) { + for _ in 0..m.rows(p, w) { + out.push(format!("holds({},{})", self.p(p), self.w(w))); + } + } + } + } + } + }, + (true, true, false, false, 3) => { + for m in self.modes() { + for (p, &row) in m.cells.iter().enumerate().take(self.kb.props.0.len()) { + for w in bits(row) { + let copies = match proj { + Projection::Set => 1, + Projection::Bag => m.rows(p, w), + }; + for _ in 0..copies { + out.push(format!( + "holds_via({},{},{})", + m.label, + self.p(p), + self.w(w) + )); + } + } + } + } + } + (true, true, true, true, 5) => self.rule_atoms(&mut out), + _ => return Err(Refusal::Selection), + } + Ok(out) + } + + fn rule_atoms(&self, out: &mut Vec) { + let kb = self.kb; + for (r, rule) in kb.rules.0.iter().enumerate() { + for (mode, table) in [ + ("asserted", &kb.asserts_rule[r]), + ("endorsed", &kb.endorses_rule[r]), + ] { + for (p, &row) in table.iter().enumerate().take(kb.props.0.len()) { + for w in bits(row & kb.world_set) { + out.push(format!( + "holds_via_rule({mode},{},{},{rule},{rule})", + self.p(p), + self.w(w) + )); + } + } + } + for par in 0..kb.worlds.0.len() { + for p in 0..kb.props.0.len() { + if self.sources[r][p] >> par & 1 == 1 { + for w in bits(self.inherited_from(par, p)) { + out.push(format!( + "holds_via_rule(inherited({}),{},{},{INHERIT_RULE},{rule})", + self.w(par), + self.p(p), + self.w(w) + )); + } + } + } + } + } + } + + /// Every Kripke atom the golden files carry, sorted. `proj` applies to + /// `holds/2`, the only selection where rows can coincide. + pub fn materialize_atoms(&self, proj: Projection) -> Vec { + let sel = |f: &[u8]| WideFieldMask::from_positions(f); + let mut out = Vec::new(); + for (s, pr) in [ + (sel(&[F_PROP, F_WORLD]), proj), + (sel(&[F_PROP, F_WORLD, F_MODE]), Projection::Set), + ( + sel(&[F_PROP, F_WORLD, F_MODE, F_IMMEDIATE, F_SOURCE]), + Projection::Set, + ), + ] { + out.extend( + self.materialize_selection(&s, pr) + .expect("a supported selection"), + ); + } + let kb = self.kb; + for p in 0..kb.props.0.len() { + let inherited: u64 = (0..kb.worlds.0.len()) + .map(|par| self.inherited_from(par, p)) + .fold(0, |a, b| a | b); + let moderate: u64 = bits(self.direct[p]) + .map(|par| self.inherited_from(par, p)) + .fold(0, |a, b| a | b); + let strong = self.direct[p]; + for (level, m) in [ + ("strong", strong), + ("moderate", moderate), + ("weak", inherited & !strong & !moderate), + ] { + for w in bits(m) { + out.push(format!( + "holding_strength({level},{},{})", + self.p(p), + self.w(w) + )); + } + } + for (o, cells) in self.origins.iter().enumerate() { + for w in bits(cells[p]) { + out.push(format!( + "inheritance_source({},{},{})", + self.p(p), + self.w(w), + self.w(o) + )); + } + } + for w in bits(kb.overridden[p]) { + out.push(format!("overridden({},{})", self.p(p), self.w(w))); + } + } + out.sort(); + out + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn lineage_never_leaves_the_held_cells() { + // F5: r_orphan has a rule companion but no assertion, so p holds + // nowhere. Its lineage must stay at its own cell, not flow to a. + let g = parse_golden(include_str!("../goldens/F5-gates.tsv")).unwrap(); + let kb = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + let r = kb.rules.0.iter().position(|n| n == "r_orphan").unwrap(); + let p = kb.props.0.iter().position(|n| n == "p").unwrap(); + let base = kb.worlds.0.iter().position(|n| n == "base").unwrap(); + assert_eq!(h.holds[p], 0); + assert_eq!(h.sources[r][p], 1 << base); + // Every lineage cell outside the base lies inside holds. + for s in h.sources.iter().chain(&h.origins) { + for (i, row) in s.iter().enumerate() { + let base_row = (0..kb.rules.0.len()) + .map(|r| (kb.asserts_rule[r][i] | kb.endorses_rule[r][i]) & kb.world_set) + .fold(h.direct[i], |a, b| a | b); + assert_eq!(row & !base_row & !h.holds[i], 0); + } + } + } +} diff --git a/crates/mistaber-kripke-probe/tests/goldens.rs b/crates/mistaber-kripke-probe/tests/goldens.rs new file mode 100644 index 000000000..1ff5cdbec --- /dev/null +++ b/crates/mistaber-kripke-probe/tests/goldens.rs @@ -0,0 +1,189 @@ +//! The native fixpoint against the Clingo goldens, and the falsifiers. + +use std::fs; +use std::path::PathBuf; + +use lance_graph_contract::class_view::WideFieldMask; +use mistaber_kripke_probe::{Golden, Kb, Projection, Refusal, parse_golden}; + +fn goldens() -> Vec { + let dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("goldens"); + let mut out: Vec = fs::read_dir(&dir) + .expect("goldens/") + .map(|e| e.expect("entry").path()) + .filter(|p| p.extension().is_some_and(|x| x == "tsv")) + .map(|p| parse_golden(&fs::read_to_string(p).expect("read")).expect("parse")) + .collect(); + out.sort_by(|a, b| a.fixture_id.cmp(&b.fixture_id)); + out +} + +fn golden(id: &str) -> Golden { + goldens() + .into_iter() + .find(|g| g.fixture_id == id) + .expect(id) +} + +fn sorted(mut v: Vec) -> Vec { + v.sort(); + v +} + +#[test] +fn every_golden_is_reproduced_exactly() { + let all = goldens(); + // Anti-vacuity: the eleven exported fixtures, not an empty directory. + assert_eq!(all.len(), 11); + for g in &all { + let kb = Kb::load(&g.facts).expect(&g.fixture_id); + let got = kb.solve().materialize_atoms(Projection::Set); + assert_eq!(got, sorted(g.atoms.clone()), "{}", g.fixture_id); + } +} + +#[test] +fn the_goldens_are_not_trivial() { + // Every derived predicate appears somewhere, and inheritance happens. + let atoms: Vec = goldens().into_iter().flat_map(|g| g.atoms).collect(); + for pred in [ + "holds(", + "holds_via(inherited(", + "holds_via_rule(inherited(", + "holding_strength(weak", + "inheritance_source(", + "overridden(", + ] { + assert!(atoms.iter().any(|a| a.starts_with(pred)), "{pred}"); + } +} + +#[test] +fn orientation_is_load_bearing() { + let a = golden("F1-modes"); + let b = golden("F1-reversed"); + let (ka, kb) = (Kb::load(&a.facts).unwrap(), Kb::load(&b.facts).unwrap()); + let sa = ka.solve().materialize_atoms(Projection::Set); + let sb = kb.solve().materialize_atoms(Projection::Set); + assert!(sa.contains(&"holds(p,a)".to_owned())); + assert!(!sb.contains(&"holds(p,a)".to_owned())); +} + +#[test] +fn a_cycle_supports_nothing_and_terminates() { + let g = golden("F2-cycle"); + let kb = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + let got = h.materialize_atoms(Projection::Set); + let held: Vec<_> = got.iter().filter(|a| a.starts_with("holds(")).collect(); + assert_eq!(held, ["holds(t,z)"]); + assert!(h.steps <= 4, "{} steps", h.steps); +} + +#[test] +fn set_projection_is_required_on_the_diamond() { + // p holds in d by inherited(a) and inherited(b): two lens rows, one fact. + let g = golden("F1-modes"); + let kb = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + assert_eq!(h.bag_multiplicity("p", "d"), 2); + assert_eq!(h.bag_multiplicity("p", "a"), 1); + let sel = WideFieldMask::from_positions(&[0, 1]); + let set = h.materialize_selection(&sel, Projection::Set).unwrap(); + let bag = h.materialize_selection(&sel, Projection::Bag).unwrap(); + let count = |v: &[String]| v.iter().filter(|a| *a == "holds(p,d)").count(); + assert_eq!(count(&set), 1); + assert_eq!(count(&bag), 2); + // The bag reading does not reproduce the golden. + assert_ne!(h.materialize_atoms(Projection::Bag), sorted(g.atoms)); +} + +#[test] +fn bag_and_set_agree_where_every_holding_has_one_lens_row() { + // Silence twin: one mode and one source rule per holding, so the two + // projections coincide. + let g = golden("C-mammal-C4"); + let kb = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + assert_eq!( + h.materialize_atoms(Projection::Bag), + h.materialize_atoms(Projection::Set) + ); +} + +#[test] +fn a_fact_outside_the_kripke_inputs_is_refused() { + let facts = vec![vec![ + "is_a".to_owned(), + "monotreme".to_owned(), + "mammal".to_owned(), + ]]; + assert!(matches!(Kb::load(&facts), Err(Refusal::UnknownFact(k)) if k == "is_a")); + let facts = vec![vec!["asserts".to_owned(), "w".to_owned()]]; + assert!(matches!(Kb::load(&facts), Err(Refusal::Arity(_)))); +} + +#[test] +fn a_65th_world_is_refused_not_wrapped() { + let facts: Vec> = (0..65) + .map(|i| vec!["world".to_owned(), format!("w{i}")]) + .collect(); + assert_eq!(Kb::load(&facts[..64]).err(), None); + assert!(matches!(Kb::load(&facts), Err(Refusal::TooMany("world")))); +} + +#[test] +fn a_selection_that_is_no_predicate_is_refused() { + let g = golden("F1-modes"); + let kb = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + for f in [&[0u8][..], &[0, 2], &[0, 1, 3], &[0, 1, 2, 4]] { + let sel = WideFieldMask::from_positions(f); + assert_eq!( + h.materialize_selection(&sel, Projection::Set), + Err(Refusal::Selection), + "{f:?}" + ); + } +} + +#[test] +fn bag_counts_lens_rows_not_modes() { + // p holds in e by ONE mode, inherited(d), traced to TWO source rules + // (r_base_p, r_b_endorse): two lens rows, one holds_via fact, one holds + // fact. g holds in a with no rule at all: one lens row, empty rule fields. + let g = golden("F1-modes"); + let kb = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + assert_eq!(h.bag_multiplicity("p", "e"), 2); + assert_eq!(h.bag_multiplicity("g", "a"), 1); + let count = |sel: &[u8], proj, atom: &str| { + h.materialize_selection(&WideFieldMask::from_positions(sel), proj) + .unwrap() + .iter() + .filter(|a| *a == atom) + .count() + }; + let via = "holds_via(inherited(d),p,e)"; + assert_eq!(count(&[0, 1, 2], Projection::Set, via), 1); + assert_eq!(count(&[0, 1, 2], Projection::Bag, via), 2); + assert_eq!(count(&[0, 1], Projection::Set, "holds(p,e)"), 1); + assert_eq!(count(&[0, 1], Projection::Bag, "holds(p,e)"), 2); + // The five-field selection is the lens itself: Set and Bag agree. + assert_eq!( + sorted( + h.materialize_selection( + &WideFieldMask::from_positions(&[0, 1, 2, 3, 4]), + Projection::Set + ) + .unwrap() + ), + sorted( + h.materialize_selection( + &WideFieldMask::from_positions(&[0, 1, 2, 3, 4]), + Projection::Bag + ) + .unwrap() + ), + ); +}