fix(kb): keys are compared as variants, and a cited clause cannot be silently retired (improvise-dj1l, improvise-2f97)

dj1l (P1, found by review of PR #68 after it merged). kb-merge.pl matched
clause keys by UNIFICATION, which both lost and corrupted clauses.
check_self_consistent compared keys with ==, but findall hands back fresh
variables, so two clauses with variant heads were never == and passed the
duplicate gate; foldl_merge then matched by unification and the second removed
the first. Reproduced: 536 before, 2 in delta, 537 after. Worse, adding
`probe_fact(X) :- doctrine(X,_).` over a kb holding probe_fact(a) and
probe_fact(b) deleted probe_fact(a) AND wrote `probe_fact(a):-doctrine(a,A)` --
the match bound X, so the clause written was not the clause supplied. The
round-trip verify cannot see that: it compares the file against an intended
list already corrupted by the same unification.

same_key/2 (copy_term + numbervars) in has_key, conflicts and absent;
canonicalize before duplicate detection; a RULE keys on the whole clause, since
one head shape with different bodies is ordinary Prolog; and check_total/2
asserts the arithmetic the tool already PRINTED beside the delta size -- "2 in
delta, 537 after" was visible in its own output twice and nothing compared them.

2f97. kb_error(dangling_citation/3): a name cited inside another clause's text
must resolve as a doctrine/2, invariant/2 or decision/3, so retiring a clause
can no longer dangle every clause naming it. The token rule is narrow on
purpose -- a name-shaped token directly inside doctrine(, invariant( or
decision( -- so prose cannot false-positive. kb_error/1 is a gate predicate,
so this was written with KB_ALLOW_GATE=1 deliberately: the refusal exists so a
write cannot disarm its own gate, and an intentional change to the gate is
supposed to be a greppable act rather than an impossible one.

Seven cases added to kb-test.sh, each proved by injection: two variant-headed
rules both land; a non-ground rule deletes nothing and is written as supplied;
a duplicate key is still refused; an injected dropping fold is caught by the
total; a cited clause cannot be retired; and the citation arm fires on a name
that resolves to nothing without firing on one that resolves. scripts/kb gains
a KB_MERGE seam so a broken merge can be injected. One pre-existing case moved
off doctrine(bug_first), which the new arm correctly refuses to retire.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FC2jVn8Au7E9JPkw6bwXXH
This commit is contained in:
Edward Langley
2026-09-20 16:31:02 -07:00
parent 3bb484b1f3
commit 50de0a8fd2
4 changed files with 205 additions and 7 deletions
+3 -1
View File
@@ -6,7 +6,9 @@ set -euo pipefail
here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
repo="$(cd "$here/.." && pwd)"
KB="${KB_FILE:-$repo/prolog-sessions/kb.pl}"
MERGE="$here/kb-merge.pl"
# Test seam: kb-test.sh injects a pre-fix kb-merge.pl to prove the arithmetic
# check catches a merge that drops a clause.
MERGE="${KB_MERGE:-$here/kb-merge.pl}"
# trealla comes from the dev shell, which direnv puts on PATH. Reaching it
# through `nix shell` per invocation cost more than the work it did: this