diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 529790ce..ed1272e7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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)))" diff --git a/prolog-sessions/kb.pl b/prolog-sessions/kb.pl index 33ea03a1..e48afefd 100644 --- a/prolog-sessions/kb.pl +++ b/prolog-sessions/kb.pl @@ -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').