Files
improvise/scripts/kb
T
Edward Langley 50de0a8fd2 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
2026-09-20 16:31:02 -07:00

180 lines
6.2 KiB
Bash
Executable File

#!/usr/bin/env bash
# The knowledge base's one maintenance tool. Replaces the Prolog MCP cycle:
# adding a clause costs the clause, not the whole predicate.
set -euo pipefail
here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
repo="$(cd "$here/.." && pwd)"
KB="${KB_FILE:-$repo/prolog-sessions/kb.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
# tool's first real use timed out past two minutes on a half-second write.
if ! command -v tpl >/dev/null 2>&1; then
echo "kb: tpl is not on PATH -- run inside the dev shell (direnv allow, or nix develop)" >&2
exit 127
fi
# stdin is closed on every call: an uncaught Prolog error falls back to the
# REPL, which hangs on a terminal and exits 0 without one -- a refusal that
# reads as acceptance. kb-merge.pl catches parse errors; this is the backstop.
tpl() { command tpl "$@" </dev/null; }
# The goal that runs kb-merge.pl. `-g main,halt` is NOT enough: measured on
# trealla 3.10.3 it exits 0 on a throw and on a failure alike, so a crash reads
# as success to `if ! tpl ...`. This propagates both.
MERGE_GOAL="(catch(main,E,(write(user_error,E),nl(user_error),halt(2))) -> halt(0) ; halt(1))"
merge() { tpl -q "$MERGE" -g "$MERGE_GOAL" -- "$@"; }
# kb_consistent is the gate CI runs. Anything that writes runs it on the
# CANDIDATE, before the candidate becomes the knowledge base.
# The goal reaches a halt on EVERY path, for the same reason MERGE_GOAL does: a
# goal that throws never reaches the halt beside it and tpl exits 0. Without the
# catch, a write that REMOVED kb_consistent made the gate pass by not existing.
CHECK_GOAL="(catch(kb_consistent,E,(write(user_error,E),nl(user_error),halt(2))) -> halt(0) ; (kb_report, halt(1)))"
check_file() {
tpl "$1" -g "$CHECK_GOAL" 2>/dev/null
}
# A content stamp of the knowledge base as it was READ. Two agents running this
# concurrently would otherwise both read the same file, both validate, and the
# later mv would discard the earlier addition -- the lost-update class this tool
# exists to avoid, and waves here run agents in parallel.
stamp_of() {
if command -v sha256sum >/dev/null 2>&1; then sha256sum "$1" | cut -d' ' -f1
elif command -v shasum >/dev/null 2>&1; then shasum -a 256 "$1" | cut -d' ' -f1
else cksum "$1" | tr -d ' '
fi
}
# mkdir is atomic everywhere; flock is absent on macOS. The lock makes a
# collision rare, the stamp makes one that happens anyway LOUD rather than silent.
acquire_lock() {
local tries=0
until mkdir "$KB.lock" 2>/dev/null; do
tries=$((tries + 1))
if [ "$tries" -ge 300 ]; then
echo "kb: could not acquire $KB.lock after 30s; remove it if stale" >&2
exit 1
fi
sleep 0.1
done
trap 'rmdir "$KB.lock" 2>/dev/null || true' EXIT
}
# Test seam: simulate another writer landing between the read and the commit.
race_hook() {
[ -n "${KB_TEST_RACE:-}" ] || return 0
cp -f "$KB_TEST_RACE" "$KB"
}
usage() {
cat >&2 <<'EOF'
usage: kb <command>
check [--with <d.pl>] run kb_consistent, optionally over a proposed design
count clauses per keyed predicate
query '<goal>' run a goal against the knowledge base
fmt rewrite in canonical form (idempotent)
add <delta.pl> add clauses; refuses if any key already exists
replace <delta.pl> add clauses, overwriting existing keys
rm <keys.pl> remove clauses by key; refuses if any key is absent
Every writing command verifies the result reads back as the clauses intended
and passes kb_consistent before it replaces the knowledge base.
EOF
exit 2
}
commit() { # $1 = candidate file, $2 = stamp of the kb before it was read
local cand="$1" was="${2:-}"
race_hook
if [ -n "$was" ] && [ "$(stamp_of "$KB")" != "$was" ]; then
rm -f "$cand"
echo "kb: REFUSED -- $KB changed while this write was being prepared." >&2
echo "kb: another writer won; re-run and your delta applies on top." >&2
exit 1
fi
if ! check_file "$cand"; then
rm -f "$cand"
echo "kb: REFUSED -- kb_consistent fails on the result; $KB is unchanged" >&2
exit 1
fi
mv -f "$cand" "$KB"
}
[ $# -ge 1 ] || usage
cmd="$1"; shift
case "$cmd" in
check)
# `check --with <design.pl>` asks whether a design the tree does not yet
# have is one the model accepts: the facts are merged into a throwaway
# candidate -- which keeps each predicate contiguous -- and kb_consistent
# runs over the union. Nothing is ever committed.
if [ "${1:-}" = "--with" ]; then
[ $# -eq 2 ] || usage
cand="$(mktemp)"
if ! merge replace "$KB" "$2" "$cand" >/dev/null; then
rm -f "$cand"; echo "kb: the proposal is not well-formed" >&2; exit 1
fi
if check_file "$cand"; then
rm -f "$cand"; echo "kb_consistent with $2: TRUE"
else
rm -f "$cand"; echo "kb: the model REFUSES this design (above)" >&2; exit 1
fi
elif check_file "$KB"; then echo "kb_consistent: TRUE"; else exit 1; fi
;;
count)
merge count "$KB" 2>/dev/null
;;
query)
[ $# -eq 1 ] || usage
tpl "$KB" -g "($1 -> halt(0) ; (write('false'), nl, halt(1)))" 2>/dev/null
;;
fmt)
acquire_lock
was="$(stamp_of "$KB")"
cand="$(mktemp)"
: > "${cand}.delta"
if ! merge add "$KB" "${cand}.delta" "$cand" >/dev/null 2>&1; then
rm -f "$cand" "${cand}.delta"
echo "kb: REFUSED -- $KB is unchanged" >&2
exit 1
fi
rm -f "${cand}.delta"
commit "$cand" "$was"
echo "kb: canonicalized"
;;
rm)
[ $# -eq 1 ] || usage
acquire_lock
was="$(stamp_of "$KB")"
cand="$(mktemp)"
if ! merge remove "$KB" "$1" "$cand"; then
rm -f "$cand"
echo "kb: REFUSED -- $KB is unchanged" >&2
exit 1
fi
commit "$cand" "$was"
echo "kb: $KB updated"
;;
add|replace)
[ $# -eq 1 ] || usage
acquire_lock
was="$(stamp_of "$KB")"
cand="$(mktemp)"
if ! merge "$cmd" "$KB" "$1" "$cand"; then
rm -f "$cand"
echo "kb: REFUSED -- $KB is unchanged" >&2
exit 1
fi
commit "$cand" "$was"
echo "kb: $KB updated"
;;
*) usage ;;
esac