From 26d94d2297f4454b87778df6aa09f77e450343dc Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 30 Oct 2026 16:14:42 +0000 Subject: [PATCH 1/6] mistaber-kripke-probe: Kripke holding rules as a least fixpoint over 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 Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ --- crates/mistaber-kripke-probe/Cargo.toml | 23 + .../goldens/C-mammal-C2.tsv | 11 + .../goldens/C-mammal-C4.tsv | 28 + .../goldens/C-mammal-C6.tsv | 30 ++ .../goldens/C-mammal-C6i.tsv | 40 ++ .../goldens/E-xlog-override.tsv | 76 +++ .../goldens/E-xlog-plain.tsv | 79 +++ .../goldens/F1-modes.tsv | 78 +++ .../goldens/F1-reversed.tsv | 63 +++ .../goldens/F2-cycle.tsv | 17 + .../goldens/F5-gates.tsv | 12 + crates/mistaber-kripke-probe/goldens/SOURCE | 4 + crates/mistaber-kripke-probe/src/lib.rs | 503 ++++++++++++++++++ crates/mistaber-kripke-probe/tests/goldens.rs | 147 +++++ 14 files changed, 1111 insertions(+) create mode 100644 crates/mistaber-kripke-probe/Cargo.toml create mode 100644 crates/mistaber-kripke-probe/goldens/C-mammal-C2.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/C-mammal-C4.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/C-mammal-C6.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/C-mammal-C6i.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/E-xlog-override.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/E-xlog-plain.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/F1-modes.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/F1-reversed.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/F2-cycle.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/F5-gates.tsv create mode 100644 crates/mistaber-kripke-probe/goldens/SOURCE create mode 100644 crates/mistaber-kripke-probe/src/lib.rs create mode 100644 crates/mistaber-kripke-probe/tests/goldens.rs 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/SOURCE b/crates/mistaber-kripke-probe/goldens/SOURCE new file mode 100644 index 000000000..b8902156f --- /dev/null +++ b/crates/mistaber-kripke-probe/goldens/SOURCE @@ -0,0 +1,4 @@ +Copied verbatim from AdaWorldAPI/mistaber-rs@f163fa7 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..d7c37da4e --- /dev/null +++ b/crates/mistaber-kripke-probe/src/lib.rs @@ -0,0 +1,503 @@ +//! 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!("a monotone fixpoint over 64 x 64 bits converges within 4096 steps") +} + +/// 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 as `(label, proposition × world mask)`. + fn modes(&self) -> Vec<(String, Rows)> { + let mut out = vec![ + ( + "asserted".to_owned(), + and_row(&self.kb.asserts, self.kb.world_set), + ), + ( + "endorsed".to_owned(), + and_row(&self.kb.endorses, self.kb.world_set), + ), + ]; + for par in 0..self.kb.worlds.0.len() { + let m: Rows = std::array::from_fn(|p| { + if p < self.kb.props.0.len() { + self.inherited_from(par, p) + } else { + 0 + } + }); + out.push((format!("inherited({})", self.w(par)), m)); + } + out + } + + /// How many lens rows (modes) hold `p` in `w`: the multiplicity a bag + /// projection to `holds/2` would report. + 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() + .filter(|(_, m)| m[p] >> w & 1 == 1) + .count() + } + + /// 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.iter().enumerate().take(self.kb.props.0.len()) { + for w in bits(row) { + out.push(format!("holds({},{})", self.p(p), self.w(w))); + } + } + } + } + }, + (true, true, false, false, 3) => { + for (mode, m) in self.modes() { + for (p, &row) in m.iter().enumerate().take(self.kb.props.0.len()) { + for w in bits(row) { + out.push(format!("holds_via({mode},{},{})", 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 + } +} diff --git a/crates/mistaber-kripke-probe/tests/goldens.rs b/crates/mistaber-kripke-probe/tests/goldens.rs new file mode 100644 index 000000000..41c6b2ae5 --- /dev/null +++ b/crates/mistaber-kripke-probe/tests/goldens.rs @@ -0,0 +1,147 @@ +//! 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 ten exported fixtures, not an empty directory. + assert_eq!(all.len(), 10); + 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_no_holding_has_two_modes() { + // Silence twin: on a chain without a diamond 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:?}" + ); + } +} From 5a5751abeae3de425eef181cc411ef69d3464d51 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 30 Oct 2026 16:15:12 +0000 Subject: [PATCH 2/6] mistaber-kripke-probe: test the holds gate on lineage directly 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 Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ --- crates/mistaber-kripke-probe/src/lib.rs | 28 +++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/crates/mistaber-kripke-probe/src/lib.rs b/crates/mistaber-kripke-probe/src/lib.rs index d7c37da4e..2501c64cf 100644 --- a/crates/mistaber-kripke-probe/src/lib.rs +++ b/crates/mistaber-kripke-probe/src/lib.rs @@ -501,3 +501,31 @@ impl Holdings<'_> { 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); + } + } + } +} From dde980bb525777e3533257541147abbd4a0b06f9 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 30 Oct 2026 16:17:46 +0000 Subject: [PATCH 3/6] D-MIST-NATIVE: plan, board rows and CI line for the Mistaber Kripke probe 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 Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ --- .claude/board/INTEGRATION_PLANS.md | 4 + .claude/board/STATUS_BOARD.md | 12 ++ ...mist-native-0-kripke-fixpoint-over-dr64.md | 11 ++ .claude/board/entries/README.md | 3 +- .claude/plans/d-mistaber-native-v1.md | 103 ++++++++++++++++++ .github/workflows/mistaber-kripke-probe.yml | 70 ++++++++++++ 6 files changed, 202 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md create mode 100644 .claude/plans/d-mistaber-native-v1.md create mode 100644 .github/workflows/mistaber-kripke-probe.yml diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index bcd25e4d7..4c3aedfca 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:** 10/10 Clingo goldens exact, 5 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..3db02f6b5 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`; 10 Clingo goldens exact; holdings lens with Set/Bag projection; 5 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..c5731018a --- /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 10 goldens reproduce exactly: F1-modes, F1-reversed, F2-cycle, F5-gates, 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. 5 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`); the upstream licence before fixture text enters a production crate. 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..67ba43578 --- /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 10 Clingo goldens exactly. + - 5 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 fixture); 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 | + +`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`: 10 tests. + +Goldens: F1-modes, F1-reversed, F2-cycle, F5-gates, 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` | +| 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. + +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`? +- **Q3:** licence. `BrainyBlaze/mistaber`'s licence must be checked before Mistaber fixture text enters a production crate. The probe copies only domain-neutral fixtures authored in `mistaber-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 From dbfb187f7b911f31140aa6ef5a0085e3e02e8950 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 30 Oct 2026 16:29:48 +0000 Subject: [PATCH 4/6] contract: rustfmt morton8x8.rs (format check red on main since c04ffe9) 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 Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ --- crates/lance-graph-contract/src/morton8x8.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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); From 5ca38fb7ee2cd740e534c4ce1f561f77a9e198ff Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 30 Oct 2026 20:41:58 +0000 Subject: [PATCH 5/6] mistaber-kripke-probe: Bag projection counts lens rows, not modes 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 Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ --- .claude/plans/d-mistaber-native-v1.md | 2 +- crates/mistaber-kripke-probe/src/lib.rs | 107 +++++++++++++----- crates/mistaber-kripke-probe/tests/goldens.rs | 46 +++++++- 3 files changed, 126 insertions(+), 29 deletions(-) diff --git a/.claude/plans/d-mistaber-native-v1.md b/.claude/plans/d-mistaber-native-v1.md index 67ba43578..59ef6b20b 100644 --- a/.claude/plans/d-mistaber-native-v1.md +++ b/.claude/plans/d-mistaber-native-v1.md @@ -70,7 +70,7 @@ A narrower selection can make two lens rows equal. In the diamond (F1), `p` hold | bag (column subset, multiplicity kept) | ALIAS to the selection | | set (Datalog head) | the selection **followed by** a distinct/existence fold | -`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). +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) diff --git a/crates/mistaber-kripke-probe/src/lib.rs b/crates/mistaber-kripke-probe/src/lib.rs index 2501c64cf..469848ee3 100644 --- a/crates/mistaber-kripke-probe/src/lib.rs +++ b/crates/mistaber-kripke-probe/src/lib.rs @@ -286,6 +286,28 @@ fn lfp( unreachable!("a monotone fixpoint over 64 x 64 bits converges within 4096 steps") } +/// 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, @@ -319,33 +341,56 @@ impl Holdings<'_> { self.kb.children[parent] & !self.block[p] } - /// Every mode as `(label, proposition × world mask)`. - fn modes(&self) -> Vec<(String, Rows)> { + /// 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![ - ( - "asserted".to_owned(), - and_row(&self.kb.asserts, self.kb.world_set), - ), - ( - "endorsed".to_owned(), - and_row(&self.kb.endorses, self.kb.world_set), - ), + 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..self.kb.worlds.0.len() { - let m: Rows = std::array::from_fn(|p| { - if p < self.kb.props.0.len() { + 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 } }); - out.push((format!("inherited({})", self.w(par)), m)); + 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 (modes) hold `p` in `w`: the multiplicity a bag - /// projection to `holds/2` would report. + /// 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), @@ -353,10 +398,7 @@ impl Holdings<'_> { ) else { return 0; }; - self.modes() - .iter() - .filter(|(_, m)| m[p] >> w & 1 == 1) - .count() + self.modes().iter().map(|m| m.rows(p, w)).sum() } /// Materialize one predicate as atoms: a [`WideFieldMask`] selection over @@ -385,20 +427,33 @@ impl Holdings<'_> { } } Projection::Bag => { - for (_, m) in self.modes() { - for (p, &row) in m.iter().enumerate().take(self.kb.props.0.len()) { + for m in self.modes() { + for (p, &row) in m.cells.iter().enumerate().take(self.kb.props.0.len()) { for w in bits(row) { - out.push(format!("holds({},{})", self.p(p), self.w(w))); + for _ in 0..m.rows(p, w) { + out.push(format!("holds({},{})", self.p(p), self.w(w))); + } } } } } }, (true, true, false, false, 3) => { - for (mode, m) in self.modes() { - for (p, &row) in m.iter().enumerate().take(self.kb.props.0.len()) { + for m in self.modes() { + for (p, &row) in m.cells.iter().enumerate().take(self.kb.props.0.len()) { for w in bits(row) { - out.push(format!("holds_via({mode},{},{})", self.p(p), self.w(w))); + 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) + )); + } } } } diff --git a/crates/mistaber-kripke-probe/tests/goldens.rs b/crates/mistaber-kripke-probe/tests/goldens.rs index 41c6b2ae5..c0774041d 100644 --- a/crates/mistaber-kripke-probe/tests/goldens.rs +++ b/crates/mistaber-kripke-probe/tests/goldens.rs @@ -99,8 +99,9 @@ fn set_projection_is_required_on_the_diamond() { } #[test] -fn bag_and_set_agree_where_no_holding_has_two_modes() { - // Silence twin: on a chain without a diamond the two projections coincide. +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(); @@ -145,3 +146,44 @@ fn a_selection_that_is_no_predicate_is_refused() { ); } } + +#[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() + ), + ); +} From 7f60c75c17034b331704a8fea9026b6a7b5f637d Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 30 Oct 2026 20:50:39 +0000 Subject: [PATCH 6/6] mistaber-kripke-probe: F6-undeclared-child golden; correct the lfp panic 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 Claude-Session: https://claude.ai/code/session_01XAqKMMCqUkM2QW7zqLC2NJ --- .claude/board/INTEGRATION_PLANS.md | 2 +- .claude/board/STATUS_BOARD.md | 2 +- ...-mist-native-0-kripke-fixpoint-over-dr64.md | 4 ++-- .claude/plans/d-mistaber-native-v1.md | 14 +++++++------- .../goldens/F6-undeclared-child.tsv | 18 ++++++++++++++++++ crates/mistaber-kripke-probe/goldens/SOURCE | 2 +- crates/mistaber-kripke-probe/src/lib.rs | 4 +++- crates/mistaber-kripke-probe/tests/goldens.rs | 4 ++-- 8 files changed, 35 insertions(+), 15 deletions(-) create mode 100644 crates/mistaber-kripke-probe/goldens/F6-undeclared-child.tsv diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 4c3aedfca..185dfb18d 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -5,7 +5,7 @@ ## 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:** 10/10 Clingo goldens exact, 5 disable runs fail as expected; lab only, no timing. +**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 3db02f6b5..f2e4371c9 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -4,7 +4,7 @@ | D-id | Deliverable | Status | Gate | |---|---|---|---| -| D-MIST-NATIVE-0 | Kripke `holds` + rule/origin lineage as a least fixpoint over `relcomp::compose`; 10 Clingo goldens exact; holdings lens with Set/Bag projection; 5 disable runs | In PR | lab only | +| 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 | 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 index c5731018a..46a4dbcd8 100644 --- 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 @@ -4,8 +4,8 @@ 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 10 goldens reproduce exactly: F1-modes, F1-reversed, F2-cycle, F5-gates, 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. 5 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. +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`); the upstream licence before fixture text enters a production crate. No timing taken. +**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/plans/d-mistaber-native-v1.md b/.claude/plans/d-mistaber-native-v1.md index 59ef6b20b..bd144e92c 100644 --- a/.claude/plans/d-mistaber-native-v1.md +++ b/.claude/plans/d-mistaber-native-v1.md @@ -27,11 +27,11 @@ D-MIST-NATIVE-0 is the probe that tests this claim. Its findings: ## 2. Checklist - [x] D-MIST-NATIVE-0: probe `crates/mistaber-kripke-probe` (own workspace root, CI workflow). - - Reproduces all 10 Clingo goldens exactly. - - 5 disable runs fail as expected. + - 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 fixture); F3-naf refused at export. +- [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. @@ -74,21 +74,22 @@ A lens row is one (mode, source rule), or one (mode) with empty rule fields when ## 5. Evidence (D-MIST-NATIVE-0) -`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 10 tests. +`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 11 tests. -Goldens: F1-modes, F1-reversed, F2-cycle, F5-gates, C-mammal-C2/C4/C6/C6i, E-xlog-plain/override. All are exact, compared as sorted lists, so a duplicate atom would also fail. +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. +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. @@ -96,7 +97,6 @@ No timing was taken, and none is claimed. `mistaber-rs` §7 defers mask folds (c - **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`? -- **Q3:** licence. `BrainyBlaze/mistaber`'s licence must be checked before Mistaber fixture text enters a production crate. The probe copies only domain-neutral fixtures authored in `mistaber-rs`. ## 7. Not in scope 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 index b8902156f..48d6f9c20 100644 --- a/crates/mistaber-kripke-probe/goldens/SOURCE +++ b/crates/mistaber-kripke-probe/goldens/SOURCE @@ -1,4 +1,4 @@ -Copied verbatim from AdaWorldAPI/mistaber-rs@f163fa7 goldens/ +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 index 469848ee3..551d37755 100644 --- a/crates/mistaber-kripke-probe/src/lib.rs +++ b/crates/mistaber-kripke-probe/src/lib.rs @@ -283,7 +283,9 @@ fn lfp( } cur = next; } - unreachable!("a monotone fixpoint over 64 x 64 bits converges within 4096 steps") + 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. diff --git a/crates/mistaber-kripke-probe/tests/goldens.rs b/crates/mistaber-kripke-probe/tests/goldens.rs index c0774041d..1ff5cdbec 100644 --- a/crates/mistaber-kripke-probe/tests/goldens.rs +++ b/crates/mistaber-kripke-probe/tests/goldens.rs @@ -33,8 +33,8 @@ fn sorted(mut v: Vec) -> Vec { #[test] fn every_golden_is_reproduced_exactly() { let all = goldens(); - // Anti-vacuity: the ten exported fixtures, not an empty directory. - assert_eq!(all.len(), 10); + // 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);