feat(kb): add a maintained consistency check, and fix what it found
kb_report/0 and kb_consistent/0 enumerate kb_error/1 solutions across four classes: domain integrity (layers, concerns and dependency edges name real crates), layering (no inverted crate dependency), rule soundness (rules must REJECT a sentinel drawn from no declared domain), and functional keys (a predicate declared functional/1 must not carry conflicting values for one key), plus cross-references between recorded work. Wired into CI as a third job, since kb.pl is executable knowledge and deserves checking like code. Proving the checker fires found two bugs in it. depends_transitively/2 was a naive transitive closure, so illegal_dependency/2 — whose entire purpose is detecting an inverted edge — looped forever on exactly that input; it now carries a visited set. And the :- discontiguous declarations added in the previous commit are a syntax error in trealla, which wants the parenthesized form; the MCP server had silently tolerated them, so validating kb.pl through the session alone had hidden it. Every check class is now verified by injecting the fault it targets and confirming it is reported, then reverting. A consistency check that has only ever said "consistent" has demonstrated nothing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01V69PGQfMJuGRmtSWpfVAqn
This commit is contained in:
Edward Langley
@@ -41,3 +41,17 @@ jobs:
|
||||
run: cargo check -p improvise-io --target wasm32-unknown-unknown
|
||||
- name: improvise-command
|
||||
run: cargo check -p improvise-command --target wasm32-unknown-unknown
|
||||
|
||||
kb:
|
||||
name: Knowledge base consistency
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- uses: actions/checkout@v4
|
||||
- uses: cachix/install-nix-action@v27
|
||||
# kb.pl is executable knowledge, so it gets checked like code: rules
|
||||
# must reject what they should, domains must close, and functional keys
|
||||
# must not carry conflicting values. See kb_report/0 in the file.
|
||||
- name: kb_consistent
|
||||
run: |
|
||||
nix shell nixpkgs#trealla --command tpl prolog-sessions/kb.pl \
|
||||
-g "(kb_consistent -> halt(0) ; (kb_report, halt(1)))"
|
||||
|
||||
+109
-11
@@ -3,15 +3,15 @@
|
||||
% Facts are appended chronologically as work happens, so most predicates are
|
||||
% spread through the file rather than grouped; these declarations keep that
|
||||
% shape without warnings on every consult.
|
||||
:- discontiguous crate/3.
|
||||
:- discontiguous layer/2.
|
||||
:- discontiguous location/3.
|
||||
:- discontiguous invariant/2.
|
||||
:- discontiguous doctrine/2.
|
||||
:- discontiguous work_done/3.
|
||||
:- discontiguous work_followup/3.
|
||||
:- discontiguous decision/3.
|
||||
:- discontiguous wire_carries/3.
|
||||
:- discontiguous(crate/3).
|
||||
:- discontiguous(layer/2).
|
||||
:- discontiguous(location/3).
|
||||
:- discontiguous(invariant/2).
|
||||
:- discontiguous(doctrine/2).
|
||||
:- discontiguous(work_done/3).
|
||||
:- discontiguous(work_followup/3).
|
||||
:- discontiguous(decision/3).
|
||||
:- discontiguous(wire_carries/3).
|
||||
|
||||
crate(improvise_core,'crates/improvise-core','Model, View, Workbook, formatting; no UI/IO').
|
||||
crate(improvise_formula,'crates/improvise-formula','formula parser, AST, parse_formula').
|
||||
@@ -113,8 +113,15 @@ crate_depends_on(improvise_main,improvise_formula).
|
||||
crate_depends_on(improvise_main,improvise_io).
|
||||
crate_depends_on(improvise_main,improvise_command).
|
||||
|
||||
depends_transitively(A,B) :- crate_depends_on(A,B).
|
||||
depends_transitively(A,B) :- crate_depends_on(A,X), depends_transitively(X,B).
|
||||
% Cycle-safe on purpose: illegal_dependency/2 exists to detect an inverted
|
||||
% edge, and an inverted edge IS a cycle -- a naive transitive closure loops
|
||||
% forever on exactly the input this is meant to catch (found 2026-08-30 by
|
||||
% injecting the fault the check is for).
|
||||
depends_transitively(A,B) :- depends_via(A,B,[A]).
|
||||
|
||||
depends_via(A,B,_) :- crate_depends_on(A,B).
|
||||
depends_via(A,B,Seen) :-
|
||||
crate_depends_on(A,X), \+ memberchk(X,Seen), depends_via(X,B,[X|Seen]).
|
||||
|
||||
% A dependency edge that would invert the layering.
|
||||
illegal_dependency(A,B) :-
|
||||
@@ -264,3 +271,94 @@ kb_issue_found(may_depend_on_type_confusion,'may_depend_on(A,B) :- crate(A,C,D),
|
||||
kb_issue_found(before_fixing_dead_guard,'before_fixing(A,B) :- A=C, doctrine(bug_first,B). A=C bound A to a fresh variable and constrained nothing, so the rule succeeded for any first argument. Now requires work_done(Bug,bug_fix,_).').
|
||||
kb_issue_found(discontiguous,'nine predicates are appended chronologically and so are scattered; added :- discontiguous declarations rather than reordering, because the chronological shape is the point.').
|
||||
doctrine(kb_is_code,'the knowledge base is executable, so audit it like code: check rules actually reject what they should, and check location/3 symbols still exist in the tree').
|
||||
|
||||
% ── Self-check ──────────────────────────────────────────────────────────────
|
||||
% Run `?- kb_report.` at the start of a session, or `?- kb_consistent.` for a
|
||||
% yes/no. Every violation is a kb_error/1 solution; kb_consistent succeeds
|
||||
% only when there are none.
|
||||
%
|
||||
% From a shell (this is what CI runs, see .github/workflows/ci.yml):
|
||||
%
|
||||
% nix shell nixpkgs#trealla --command tpl prolog-sessions/kb.pl \
|
||||
% -g "(kb_consistent -> halt(0) ; (kb_report, halt(1)))"
|
||||
%
|
||||
% Prefer the shell form when adding checks: the MCP server is more lenient
|
||||
% than trealla itself and silently accepted `:- discontiguous foo/1.`, which
|
||||
% trealla rejects (it wants the parenthesized form).
|
||||
%
|
||||
% What this CANNOT check, because Prolog cannot see the tree: whether
|
||||
% location/3 still names a symbol that exists. Do that from the shell —
|
||||
% see kb_external_check/1 for the command.
|
||||
|
||||
% Predicates whose first argument is a key that must map to ONE value.
|
||||
% Anything genuinely multi-valued (forbidden/2, record_column/4, decision/3,
|
||||
% which is keyed by issue AND topic) is deliberately absent.
|
||||
functional(invariant/2).
|
||||
functional(location/3).
|
||||
functional(doctrine/2).
|
||||
functional(groom_check/2).
|
||||
functional(kb_issue_found/2).
|
||||
functional(crate/3).
|
||||
functional(wasm_runtime_hazard/3).
|
||||
|
||||
% A sentinel that is deliberately not a member of any declared domain. A rule
|
||||
% that accepts it is under-constrained — this is how the two unsound rules of
|
||||
% 2026-08-30 would have been caught.
|
||||
kb_sentinel(zzz_not_a_real_term).
|
||||
|
||||
known_crate(C) :- crate(C,_,_).
|
||||
|
||||
% -- domain integrity ------------------------------------------------------
|
||||
kb_error(layer_names_unknown_crate(L,C)) :-
|
||||
layer(L,C), \+ known_crate(C).
|
||||
kb_error(forbidden_names_unknown_crate(C)) :-
|
||||
forbidden(C,_), \+ known_crate(C).
|
||||
kb_error(forbidden_names_unknown_concern(C,X)) :-
|
||||
forbidden(C,X), \+ concern(X).
|
||||
kb_error(depends_names_unknown_crate(A,B)) :-
|
||||
crate_depends_on(A,B), \+ ( known_crate(A), known_crate(B) ).
|
||||
kb_error(layering_inverted(A,B)) :-
|
||||
illegal_dependency(A,B).
|
||||
|
||||
% -- rule soundness: these must REJECT the sentinel ------------------------
|
||||
kb_error(rule_too_permissive(may_use/2)) :-
|
||||
kb_sentinel(S), may_use(_, S).
|
||||
kb_error(rule_too_permissive(before_fixing/2)) :-
|
||||
kb_sentinel(S), before_fixing(S, _).
|
||||
kb_error(rule_too_permissive(crate_depends_on/2)) :-
|
||||
kb_sentinel(S), crate_depends_on(S, _).
|
||||
|
||||
% -- functional keys must not carry conflicting values ---------------------
|
||||
kb_error(conflicting_values(P/2, Key)) :-
|
||||
functional(P/2), call(P, Key, _),
|
||||
findall(V, call(P, Key, V), Vs), sort(Vs, Sorted), Sorted = [_,_|_].
|
||||
kb_error(conflicting_values(P/3, Key)) :-
|
||||
functional(P/3), call(P, Key, _, _),
|
||||
findall(A-B, call(P, Key, A, B), Vs), sort(Vs, Sorted), Sorted = [_,_|_].
|
||||
|
||||
% -- cross-references between recorded work --------------------------------
|
||||
kb_error(followup_from_unrecorded_work(I)) :-
|
||||
work_followup(I,_,_), \+ work_done(I,_,_).
|
||||
kb_error(unblocked_by_unrecorded_work(I)) :-
|
||||
work_unblocked(I,_,_), \+ work_done(I,_,_).
|
||||
|
||||
kb_consistent :- \+ kb_error(_).
|
||||
|
||||
kb_report :-
|
||||
( setof(E, kb_error(E), Es)
|
||||
-> length(Es, N),
|
||||
format("kb: ~w problem(s)~n", [N]),
|
||||
forall(member(E, Es), format(" - ~w~n", [E]))
|
||||
; write('kb: consistent'), nl
|
||||
).
|
||||
|
||||
kb_external_check('grep -oE "^location\\([a-z_]+,''[^'']+'',''[^'']+''\\)" prolog-sessions/kb.pl # then confirm each file/symbol still exists').
|
||||
|
||||
|
||||
% Each check class is proven to FIRE, not merely to pass, by injecting the
|
||||
% fault it looks for; a checker that has only ever said "consistent" has
|
||||
% demonstrated nothing (see kb_issue_found(checker_never_failed, ...)).
|
||||
kb_issue_found(checker_never_failed,'a consistency check that has only ever reported success is untested. Inject one fault per kb_error class and confirm each is reported before trusting it.').
|
||||
kb_issue_found(cycle_unsafe_closure,'the first depends_transitively/2 was a naive transitive closure, so illegal_dependency/2 -- whose whole purpose is detecting an inverted edge -- looped forever on exactly that input. Found by fault injection; now carries a visited set.').
|
||||
kb_issue_found(mcp_lenience,'the prolog MCP server accepted `:- discontiguous foo/1.` which trealla rejects (needs parens). Validate kb.pl with trealla itself, not only through the MCP session.').
|
||||
doctrine(check_the_checker,'prove a consistency check fires by injecting the fault it targets, then revert; otherwise it is indistinguishable from a check that always succeeds').
|
||||
|
||||
Reference in New Issue
Block a user