Repository navigation
fix(provenance): stop .why_not refusing derived rows and report the actual blocker - #353
Merged
Merged
Conversation
…rue blocker (#291) .why_not read only the base facts, so a body atom over a derived view (such as candidate(S, "issue_refund") <- ...) found no tuples and a derived row was reported as NOT derived. It also took the first match of each body atom without backtracking, so a dead-end first match refused a derivable row, and it reported every head mismatch, including a differing constant, as "Target arity 2 does not match head arity 2". .why_not now evaluates the target relation (uncapped) and answers from its derived relations. A row the base facts or the evaluation hold is reported as derived, with its proof, as .why gives it; a refusal comes only when ?relation(values) has no row. For each clause, a backtracking search over base facts and derived relations finds the attempt that gets furthest and reports the premise it failed on, so every premise shown as holding holds. Head mismatches name their cause: the value count, the column whose constant differs, or the computed column (N+1, count<X>) that evaluates to another value. A premise the explainer cannot evaluate (a function call, a nearest-neighbour search) or a search past its limit yields a new not_explained blocker instead of a made-up failure. Body predicates are evaluated in one order for .why and .why_not: each as soon as it can be, so comparisons wait for the atoms that bind them, equalities assign variables (D = N * 2), and negations wait for every predicate that can bind their variables. Negated atoms read the derived relations too, so .why no longer proves a row through !blocked(...) when blocked is derived and holds. .why also proves rows of rules with computed head columns. Regression tests cover the issue's reproduction, constant and mixed heads, dead-end matches, recursion, negation over derived relations, computed and aggregate heads, and a property test: for random small programs, .why_not x refuses exactly when ?x has no row, and every premise it shows holds.
…head # Conflicts: # gui/lib/docs-bundle.ts # src/protocol/handler.rs
This was referenced Oct 5, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Intent
I want you to really hyper focus on making the symbolic engine, you know, crisp and really truly production ready. (Context: issue #291: .why_not mis-evaluates body atoms over a view whose rules have constants in the head, reporting a derived row as NOT derived, and .why_not on such a view fails with 'Head unification failed: Target arity 2 does not match head arity 2'. Proof and refusal explanations are the core of 'Decisions your agents can prove'.)
What Changed
.why_notnow evaluates the target relation in full, with no result cap, and reads the derived relations as well as base facts. A row that is actually derived is reported as derived, with the same proof.whygives. A row is reported as NOT derived only when?relation(values)returns nothing. This fixes body atoms over views whose rule heads contain constants (.why_not mis-evaluates views whose rules have constants in the head, reporting derived rows as not derived #291).N+1,count<X>) that evaluates to a different value. Previously all of these produced the misleading "Target arity 2 does not match head arity 2". There is also a newnot_explainedblocker for function calls, nearest-neighbour searches and searches that hit their limit, so these no longer produce an invented failure..whyand.why_notnow evaluate body predicates in the same order. Comparisons wait until their variables are bound, equalities assign variables, and negations wait for every predicate that can bind their variables. Negated atoms read derived relations, and.whycan prove rules that have computed head columns. The explainability and commands docs (and the GUI docs bundle) are updated, and regression and property tests are added insrc/protocol/handler/why_not_tests.rs.Risk Assessment
.why_notexplainer and changes the shared prove_body evaluation order that.whyalso uses. I traced the main paths (constant and computed heads, negation over derived relations, assignments, aggregates) and found them correct; the only notes are informational: a cut-short search isn't disclosed, and each.why_notnow runs a full uncapped evaluation.Testing
I built the fixed commit and the base commit and ran both as live servers, each with its own throwaway data directory. I drove them with the real client and with a small WebSocket driver that captures the full explanation text. On the fixed build, every scenario passes: - Issue repro: both derived rows are reported as derived, with proofs. - True blocker: the blocked row names its real cause, the negatedblockedfact. - Arity message: the "Target arity 2 does not match head arity 2" message is gone. It is replaced by the specific mismatch, either the differing constant or the wrong value count. - Other head shapes: mixed constant/variable heads, computed heads and recursive views all give correct results. - Sweep: across 24 tuples,.why_notagrees with the query every time. The base commit reproduces the bug (16 of 24 tuples disagree, plus the arity message). The targetedwhy_notunit tests also pass. There is no UI surface, so the evidence is CLI and WebSocket transcripts. Servers, temp directories and build outputs were removed afterwards.Evidence: Issue #291 script on the fixed server (full explanation text)
Evidence: Same script on the base server (reproduces the bug)
Evidence: Issue #291 script via inputlayer-client (REPL rendering, fixed build)
Evidence: Adversarial cases on the fixed server (mixed/computed heads, recursion, negation, arity)
Evidence: Query vs .why_not sweep, fixed build (24/24 agree)
Evidence: Query vs .why_not sweep, base build (8 agree, 16 disagree)
Evidence: .why proof tree JSON through the constant-head view
Evidence: Before/after excerpt
Pipeline
Updates from git push no-mistakes
✅ **intent** - passed
✅ No issues found.
✅ **Rebase** - passed
✅ No issues found.
src/provenance/why_not.rs:572- When ClauseSearch stops at MAX_SEARCH_STEPS but has already recorded a failure, explain_clause shows that failure as the clause's blocker and gives no sign that the search was cut short. The reported premise does fail for the bindings shown, so nothing false is claimed. But the docs promise 'the attempt that got furthest', and after a truncated search a later branch could have got further. One way to make the explanation honest about this is to add a note (for example, appending 'search stopped after N body matches' to the clause text or bindings) whensearch.exhausted && search.furthest.is_some().src/protocol/handler.rs:907-.why_notnow evaluates the whole target relation with the result cap turned off (handler.rs:907) on every call, where it used to read only the base facts. This is needed for a correct derived / NOT-derived verdict and matches other uncapped evaluations in this file. The trade-off: one.why_noton a very large view now costs as much as a full uncapped?view(...)query.✅ **Test** - passed
✅ No issues found.
cargo build --release --bin inputlayer-server --bin inputlayer-clientat target ae341701; launched the server on 127.0.0.1:18291 with a throwaway data dir, credentials file and configBuilt base 6ac53223 (from git archive into a temp dir) and launched it on 127.0.0.1:18292 with its own throwaway data dir for before/after comparisoninputlayer-client --script issue291.iql(the issue #291 support demo) against the live fixed serverNode WebSocket driverdrive.mjs(authenticate + execute frames) to capture the full explanation text for issue291.iql and adversarial.iql on both serversSweep over 24 tuples (candidate/allowed × 3 sessions × 4 actions) comparing?rel(...)row presence to the.why_not rel(...)verdict on both servers.why ?allowed("s-43", "open_ticket")proof_trees JSON captured from the live fixed servercargo test --release --lib why_not(26 targeted tests, including the new why_not_tests proptest; all pass)✅ **Document** - passed
✅ No issues found.
✅ **Lint** - passed
✅ No issues found.
✅ **Push** - passed
✅ No issues found.