5a79f7385b
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
748 lines
33 KiB
Bash
Executable File
748 lines
33 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# check_the_checker for scripts/kb: every refusal is proved by injecting the
|
|
# fault it names, and every refusal must leave the knowledge base UNCHANGED.
|
|
set -uo pipefail
|
|
|
|
here="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
|
repo="$(cd "$here/.." && pwd)"
|
|
work="$(mktemp -d)"
|
|
trap 'rm -rf "$work"' EXIT
|
|
# Fixtures are HEAD's kb.pl, never the working tree's: the tool now measures a
|
|
# write against HEAD, and the working tree is the thing that can be damaged.
|
|
KB="$work/head.pl"
|
|
if ! git -C "$repo" show HEAD:prolog-sessions/kb.pl > "$KB"; then
|
|
echo "kb-test: cannot read HEAD:prolog-sessions/kb.pl" >&2
|
|
exit 2
|
|
fi
|
|
|
|
pass=0
|
|
fail=0
|
|
ok() { printf ' ok %s\n' "$1"; pass=$((pass+1)); }
|
|
bad() { printf ' FAIL %s\n' "$1"; fail=$((fail+1)); }
|
|
|
|
# Each case runs against its own copy, so a bug cannot reach the real file.
|
|
# Also clears the ledger, the lock and any candidate a killed case left behind.
|
|
fresh() { rm -rf "$work"/kb.pl.*; cp "$KB" "$work/kb.pl"; }
|
|
kb() { KB_FILE="$work/kb.pl" "$here/kb" "$@"; }
|
|
unchanged() { diff -q "$KB" "$work/kb.pl" >/dev/null; }
|
|
# A refusal is only evidence when it is the refusal you NAMED: two of these
|
|
# cases passed against a tree with the fix reverted, because a DIFFERENT guard
|
|
# caught the same delta and the assertion was only "fails and kb unchanged"
|
|
# (review of PR #69). said() asserts which one fired.
|
|
said() { grep -qF "$2" "$1"; }
|
|
|
|
echo "kb-test: the refusals"
|
|
|
|
# 1. A duplicate key is refused, and nothing is written.
|
|
fresh
|
|
cat > "$work/dup.pl" <<'EOF'
|
|
doctrine(bug_first,'a second, contradicting text for a name that already exists').
|
|
EOF
|
|
if kb add "$work/dup.pl" >/dev/null 2>&1; then
|
|
bad "add accepted a duplicate key"
|
|
elif unchanged; then
|
|
ok "add refuses a duplicate key and leaves the kb unchanged"
|
|
else
|
|
bad "add refused a duplicate key but MODIFIED the kb"
|
|
fi
|
|
|
|
# 2. replace is the door that duplicate goes through, and it replaces rather
|
|
# than appending -- a count that grew would be two clauses for one name.
|
|
fresh
|
|
before="$(kb count | grep '^doctrine/2=')"
|
|
if kb replace "$work/dup.pl" >/dev/null 2>&1; then
|
|
after="$(kb count | grep '^doctrine/2=')"
|
|
if [ "$before" = "$after" ]; then
|
|
ok "replace overwrites in place ($after)"
|
|
else
|
|
bad "replace changed the clause count: $before -> $after"
|
|
fi
|
|
else
|
|
bad "replace refused a duplicate key"
|
|
fi
|
|
|
|
# 3. A delta that does not parse is refused.
|
|
fresh
|
|
printf 'doctrine(broken, unterminated\n' > "$work/bad.pl"
|
|
if kb add "$work/bad.pl" >/dev/null 2>&1; then
|
|
bad "add accepted an unparseable delta"
|
|
elif unchanged; then
|
|
ok "add refuses an unparseable delta and leaves the kb unchanged"
|
|
else
|
|
bad "add refused an unparseable delta but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4. A delta that parses but breaks kb_consistent is refused. This is the one
|
|
# that matters: the candidate is checked BEFORE it becomes the kb.
|
|
fresh
|
|
cat > "$work/illegal.pl" <<'EOF'
|
|
crate_depends_on(improvise_core,improvise_command).
|
|
EOF
|
|
if kb add "$work/illegal.pl" >/dev/null 2>&1; then
|
|
bad "add accepted a delta that breaks kb_consistent"
|
|
elif unchanged; then
|
|
ok "add refuses a kb_consistent violation and leaves the kb unchanged"
|
|
else
|
|
bad "add refused a violation but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4b. A delta trealla cannot even take apart must refuse, not crash into a
|
|
# success. `-g main,halt` exits 0 on a throw, so this is the guard for it.
|
|
fresh
|
|
printf '42.\n' > "$work/notaclause.pl"
|
|
if kb add "$work/notaclause.pl" >/dev/null 2>&1; then
|
|
bad "add accepted a term that is not a clause"
|
|
elif unchanged; then
|
|
ok "add refuses a non-clause term and leaves the kb unchanged"
|
|
else
|
|
bad "add refused a non-clause term but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4c. rm removes by key, and a key that is not there is REFUSED rather than
|
|
# silently doing nothing -- a typo would otherwise report success.
|
|
# The clause removed is one this case ADDS. It used to name bug_first, which
|
|
# the citation check (improvise-2f97) now refuses to retire -- correctly, since
|
|
# before_fixing/2 calls it and kb_issue_found names it in prose.
|
|
fresh
|
|
printf "doctrine(a_probe_doctrine_to_remove,'a clause nothing else names').\n" > "$work/probe.pl"
|
|
kb add "$work/probe.pl" >/dev/null 2>&1
|
|
printf "doctrine(a_probe_doctrine_to_remove,_).\n" > "$work/drop.pl"
|
|
before="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
|
if kb rm "$work/drop.pl" >/dev/null 2>&1; then
|
|
after="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
|
if [ "$((before - 1))" = "$after" ]; then
|
|
ok "rm removes exactly one clause ($before -> $after)"
|
|
else
|
|
bad "rm moved the count wrongly: $before -> $after"
|
|
fi
|
|
else
|
|
bad "rm refused a key that exists"
|
|
fi
|
|
|
|
fresh
|
|
printf "doctrine(a_key_that_does_not_exist_at_all,_).\n" > "$work/nokey.pl"
|
|
if kb rm "$work/nokey.pl" >/dev/null 2>&1; then
|
|
bad "rm accepted a key that is not present"
|
|
elif unchanged; then
|
|
ok "rm refuses an absent key and leaves the kb unchanged"
|
|
else
|
|
bad "rm refused an absent key but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4d. A DIRECTIVE is callable, so a callable test alone lets it through -- and
|
|
# the candidate is validated by CONSULTING it, so `:- halt(0).` exits the
|
|
# check with success before kb_consistent runs. The gate passes by never
|
|
# running. Found by review on PR #68; demonstrated before it was fixed.
|
|
fresh
|
|
printf ':- halt(0).\n' > "$work/directive.pl"
|
|
if kb add "$work/directive.pl" >/dev/null 2>&1; then
|
|
bad "add accepted a directive that disables its own gate"
|
|
elif unchanged; then
|
|
ok "add refuses a directive and leaves the kb unchanged"
|
|
else
|
|
bad "add refused a directive but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4e. Keys were checked only against the EXISTING file, so two clauses sharing a
|
|
# previously-unused key clashed with nothing and the merge dropped the first
|
|
# -- add discarding part of its own payload, visible only as a delta count
|
|
# that did not match the clauses added.
|
|
fresh
|
|
cat > "$work/selfdup.pl" <<'EOD'
|
|
doctrine(a_name_used_twice_in_one_delta,'first').
|
|
doctrine(a_name_used_twice_in_one_delta,'second').
|
|
EOD
|
|
if kb add "$work/selfdup.pl" >/dev/null 2>&1; then
|
|
bad "add accepted a delta naming one key twice"
|
|
elif unchanged; then
|
|
ok "add refuses a delta that names one key twice"
|
|
else
|
|
bad "add refused a self-duplicate but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4f. The gate can be REMOVED. kb_consistent then throws existence_error, and
|
|
# tpl exits 0 when a goal throws before reaching halt -- so the check passes
|
|
# by not existing and the unchecked candidate is committed.
|
|
fresh
|
|
printf 'kb_consistent.\n' > "$work/killgate.pl"
|
|
if kb rm "$work/killgate.pl" >/dev/null 2>&1; then
|
|
bad "rm removed the gate that validates the write"
|
|
elif unchanged; then
|
|
ok "rm refuses to remove the validating gate"
|
|
else
|
|
bad "rm refused to remove the gate but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4g. And REPLACED with something trivially true, which passes forever after.
|
|
fresh
|
|
if kb replace "$work/killgate.pl" >/dev/null 2>&1; then
|
|
bad "replace made the gate trivially true"
|
|
elif unchanged; then
|
|
ok "replace refuses to disarm the validating gate"
|
|
else
|
|
bad "replace refused to disarm the gate but MODIFIED the kb"
|
|
fi
|
|
|
|
# 4h. An intentional change to the gate is still possible, deliberately.
|
|
fresh
|
|
if KB_ALLOW_GATE=1 kb replace "$work/killgate.pl" >/dev/null 2>&1; then
|
|
ok "KB_ALLOW_GATE lets a deliberate gate change through"
|
|
else
|
|
bad "KB_ALLOW_GATE did not allow a gate change"
|
|
fi
|
|
|
|
# 4i. Two writers reading the same file would both validate, and the later mv
|
|
# would silently discard the earlier addition. The stamp makes the loser
|
|
# loud. KB_TEST_RACE simulates the other writer landing mid-flight.
|
|
fresh
|
|
cp "$work/kb.pl" "$work/other.pl"
|
|
printf "doctrine(written_by_the_other_writer,'x').\n" >> "$work/other.pl"
|
|
cat > "$work/mine.pl" <<'EOD'
|
|
doctrine(written_by_me,'y').
|
|
EOD
|
|
if KB_TEST_RACE="$work/other.pl" kb add "$work/mine.pl" >/dev/null 2>&1; then
|
|
bad "a concurrent write was silently discarded"
|
|
elif grep -q written_by_the_other_writer "$work/kb.pl" && ! grep -q written_by_me "$work/kb.pl"; then
|
|
ok "a concurrent write is refused, and the other writer's addition survives"
|
|
else
|
|
bad "the race was refused but the kb is not the other writer's file"
|
|
fi
|
|
|
|
# 4j. A multi-valued relation must accept several clauses. The key rule keyed
|
|
# on all-but-last, so a crate depending on two crates read as a duplicate
|
|
# key and was unaddable -- found by trying to model a design, not by a test.
|
|
fresh
|
|
cat > "$work/multi.pl" <<'EOD'
|
|
crate(improvise_probe,'crates/improvise-probe','a probe crate').
|
|
crate_depends_on(improvise_probe,improvise_core).
|
|
crate_depends_on(improvise_probe,improvise_protocol).
|
|
layer(probe,improvise_probe).
|
|
EOD
|
|
if kb add "$work/multi.pl" >/dev/null 2>&1; then
|
|
ok "a multi-valued relation accepts several clauses"
|
|
else
|
|
bad "add refused a legitimate multi-valued relation"
|
|
fi
|
|
|
|
# 4k. check --with asks whether a design the tree does not have is one the model
|
|
# accepts. It must be able to say BOTH, and must never write.
|
|
fresh
|
|
printf 'crate_depends_on(improvise_core,improvise_command).\n' > "$work/bad-design.pl"
|
|
if kb check --with "$work/bad-design.pl" >/dev/null 2>&1; then
|
|
bad "check --with accepted a design that inverts the layering"
|
|
elif unchanged; then
|
|
ok "check --with refuses an unsound design and writes nothing"
|
|
else
|
|
bad "check --with refused a design but MODIFIED the kb"
|
|
fi
|
|
|
|
if kb check --with "$work/multi.pl" >/dev/null 2>&1 && unchanged; then
|
|
ok "check --with accepts a sound design and writes nothing"
|
|
else
|
|
bad "check --with rejected a sound design, or wrote to the kb"
|
|
fi
|
|
|
|
echo "kb-test: the happy paths"
|
|
|
|
# 5. A genuinely new clause lands, and the count moves by exactly one.
|
|
fresh
|
|
cat > "$work/new.pl" <<'EOF'
|
|
doctrine(a_name_that_is_certainly_not_taken,'text for a brand new doctrine').
|
|
EOF
|
|
before="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
|
if kb add "$work/new.pl" >/dev/null 2>&1; then
|
|
after="$(kb count | grep '^doctrine/2=' | cut -d= -f2)"
|
|
if [ "$((before + 1))" = "$after" ]; then
|
|
ok "add lands one new clause ($before -> $after)"
|
|
else
|
|
bad "add moved the count wrongly: $before -> $after"
|
|
fi
|
|
else
|
|
bad "add refused a valid new clause"
|
|
fi
|
|
|
|
# 6. The new clause is readable back as itself -- a count can move without the
|
|
# content being what was asked for.
|
|
if KB_FILE="$work/kb.pl" "$here/kb" query \
|
|
"doctrine(a_name_that_is_certainly_not_taken,T), T == 'text for a brand new doctrine'" \
|
|
>/dev/null 2>&1; then
|
|
ok "the added clause reads back with the text it was given"
|
|
else
|
|
bad "the added clause is not readable back as itself"
|
|
fi
|
|
|
|
# 7. Canonical form is a fixed point: a second fmt changes nothing.
|
|
fresh
|
|
kb fmt >/dev/null 2>&1
|
|
cp "$work/kb.pl" "$work/once.pl"
|
|
kb fmt >/dev/null 2>&1
|
|
if diff -q "$work/once.pl" "$work/kb.pl" >/dev/null; then
|
|
ok "fmt is idempotent"
|
|
else
|
|
bad "fmt is not idempotent -- every add would churn the file"
|
|
fi
|
|
|
|
# 8. Canonicalizing loses no clause. A serializer that drops a predicate is the
|
|
# wipe-the-kb failure, so the count is checked across the reformat.
|
|
fresh
|
|
b="$(kb count)"
|
|
kb fmt >/dev/null 2>&1
|
|
a="$(kb count)"
|
|
if [ "$b" = "$a" ]; then
|
|
ok "fmt preserves every clause count"
|
|
else
|
|
bad "fmt changed the counts"
|
|
fi
|
|
|
|
# 9. A delta holding two clauses whose heads are VARIANTS -- same shape, fresh
|
|
# variables -- is two clauses. check_self_consistent compared keys with ==
|
|
# over findall results, which never holds for fresh variables, so the delta
|
|
# passed; the merge then matched by UNIFICATION and the second removed the
|
|
# first. Two in, one out, reported as a success (improvise-dj1l).
|
|
cat > "$work/rules.pl" <<'EOF'
|
|
probe_rule(X) :- doctrine(X,_).
|
|
probe_rule(Y) :- invariant(Y,_).
|
|
EOF
|
|
fresh
|
|
b="$(kb count | grep '^total=' | cut -d= -f2)"
|
|
if kb add "$work/rules.pl" >/dev/null 2>&1; then
|
|
a="$(kb count | grep '^total=' | cut -d= -f2)"
|
|
if [ "$((a - b))" -eq 2 ]; then
|
|
ok "two variant-headed rules in one delta both land ($b -> $a)"
|
|
else
|
|
bad "two clauses in the delta, $((a - b)) landed"
|
|
fi
|
|
else
|
|
bad "add refused two variant-headed rules"
|
|
fi
|
|
|
|
# 10. A non-ground key must not match a ground clause. `probe_fact(X) :- ...`
|
|
# unified with `probe_fact(a)`, which DELETED the fact and, worse, bound X
|
|
# to a, so the clause written was not the clause supplied. The round-trip
|
|
# check cannot see that: it compares the file against an intended list
|
|
# already corrupted by the same unification.
|
|
fresh
|
|
printf 'probe_fact(a).\nprobe_fact(b).\n' > "$work/facts.pl"
|
|
kb add "$work/facts.pl" >/dev/null 2>&1
|
|
printf 'probe_fact(X) :- doctrine(X,_).\n' > "$work/rule.pl"
|
|
# `add`, not `replace`: the rule is new, and a rule that is not already there
|
|
# is what case 15 makes replace refuse. This case is NOT where same_key is
|
|
# discriminated -- a rule keys on its whole clause, so the `:-` term cannot
|
|
# unify with probe_fact(a) and `conflicts` never fires here. Reverting same_key
|
|
# to unification leaves this case passing and fails the wildcard rm and case 17
|
|
# instead; the site is guarded, by those (improvise-9d5k).
|
|
if kb add "$work/rule.pl" >/dev/null 2>&1; then
|
|
kept=0
|
|
grep -q '^probe_fact(a)\.$' "$work/kb.pl" && grep -q '^probe_fact(b)\.$' "$work/kb.pl" && kept=1
|
|
if [ "$kept" = 1 ]; then
|
|
ok "a non-ground rule does not delete the ground clauses it would unify with"
|
|
else
|
|
bad "a non-ground rule deleted a ground clause"
|
|
fi
|
|
if grep -q '^probe_fact(a):-' "$work/kb.pl"; then
|
|
bad "the clause written is not the clause supplied: its variable was bound"
|
|
elif grep -qE '^probe_fact\([A-Z][A-Za-z0-9_]*\):-doctrine\(' "$work/kb.pl"; then
|
|
ok "the rule is written as supplied, with its variable still a variable"
|
|
else
|
|
bad "the rule was not written at all"
|
|
fi
|
|
else
|
|
bad "add refused a rule over a predicate holding facts: a variable key matched them"
|
|
fi
|
|
|
|
# 11. The duplicate gate must still fire once keys are compared as variants:
|
|
# two clauses that really are the same key are still two clauses for one key.
|
|
fresh
|
|
printf 'probe_rule(X) :- doctrine(X,_).\nprobe_rule(Z) :- doctrine(Z,_).\n' > "$work/same.pl"
|
|
if kb add "$work/same.pl" >"$work/out" 2>&1; then
|
|
bad "add accepted the same clause twice in one delta"
|
|
elif ! unchanged; then
|
|
bad "add refused a duplicate but MODIFIED the kb"
|
|
elif said "$work/out" "names one key twice"; then
|
|
ok "add still refuses one key named twice, compared as variants"
|
|
else
|
|
bad "the delta was refused, but not BY THE DUPLICATE GATE (canon_key is unreached)"
|
|
fi
|
|
|
|
# 12. The arithmetic check, proved by injecting the fault it exists for: a
|
|
# merge that silently drops the last clause of its delta. The count was
|
|
# PRINTED beside the delta size all along and nothing compared them, which
|
|
# is how the real loss reported itself as "2 in delta, 537 after". The
|
|
# injection is aimed at the fold rather than at the keys, because the check
|
|
# must catch a dropped clause whatever dropped it.
|
|
sed 's/^foldl_merge(_, \[\], _, Acc, Acc)\./foldl_merge(_, [_], _, Acc, Acc)./' \
|
|
"$here/kb-merge.pl" > "$work/merge-dropping.pl"
|
|
if ! grep -q '^foldl_merge(_, \[_\], _, Acc, Acc)\.$' "$work/merge-dropping.pl"; then
|
|
bad "the injection did not apply -- case 12 proves nothing"
|
|
else
|
|
fresh
|
|
if KB_MERGE="$work/merge-dropping.pl" kb add "$work/rules.pl" >/dev/null 2>&1; then
|
|
bad "a merge that dropped a clause was accepted: the total is unchecked"
|
|
elif unchanged; then
|
|
ok "a merge that drops a clause is refused by the total it already printed"
|
|
else
|
|
bad "the dropped clause was caught but the kb was MODIFIED"
|
|
fi
|
|
fi
|
|
|
|
# 13. Clauses cite each other by NAME inside their text, and nothing checked
|
|
# that the name resolved -- so retiring a clause silently dangled every
|
|
# clause referring to it, which is the fact-stated-twice hazard the KB's
|
|
# own doctrine warns about in prose (improvise-2f97). The token rule is
|
|
# deliberately narrow: only a name-shaped token inside doctrine(...),
|
|
# invariant(...) or decision(...) brackets, so ordinary prose cannot
|
|
# false-positive.
|
|
fresh
|
|
echo 'doctrine(an_advisory_gate_is_not_a_gate,_).' > "$work/cited.pl"
|
|
if kb rm "$work/cited.pl" >/dev/null 2>&1; then
|
|
bad "rm retired a clause that another clause cites by name"
|
|
elif unchanged; then
|
|
ok "retiring a cited clause is refused, and the kb is unchanged"
|
|
else
|
|
bad "the dangling citation was caught but the kb was MODIFIED"
|
|
fi
|
|
|
|
# The other direction: the arm must FIRE on a citation that resolves to
|
|
# nothing, and must not fire on one that resolves. A check that only ever
|
|
# reports success is untested (kb_issue_found(checker_never_failed)).
|
|
cat > "$work/dangling.pl" <<'EOF'
|
|
doctrine(a_probe_that_cites_nothing,'cites doctrine(a_name_that_was_retired), which does not exist').
|
|
EOF
|
|
cat > "$work/resolving.pl" <<'EOF'
|
|
doctrine(a_probe_that_cites_a_real_one,'cites doctrine(an_advisory_gate_is_not_a_gate), which exists').
|
|
EOF
|
|
fresh
|
|
if kb check --with "$work/dangling.pl" >/dev/null 2>&1; then
|
|
bad "the model accepted a design citing a clause that does not exist"
|
|
elif kb check --with "$work/resolving.pl" >/dev/null 2>&1; then
|
|
ok "a citation is checked, and one that resolves is still accepted"
|
|
else
|
|
bad "the citation check refuses a name that DOES resolve"
|
|
fi
|
|
|
|
# 14. The case only same_key/2 can catch. A rm key with a variable in a
|
|
# NON-final position -- work_done keys on two arguments -- matches nothing
|
|
# as a variant and everything by unification. Under unification it removed
|
|
# an arbitrary bug_fix entry and reported success; here it must be refused
|
|
# as ABSENT, by that message and no other.
|
|
fresh
|
|
printf 'work_done(_,bug_fix,_).\n' > "$work/wild.pl"
|
|
if kb rm "$work/wild.pl" >"$work/out" 2>&1; then
|
|
bad "rm removed clauses by unifying a variable key against them"
|
|
elif ! unchanged; then
|
|
bad "rm refused a wildcard key but MODIFIED the kb"
|
|
elif said "$work/out" "no such clause to remove"; then
|
|
ok "a key with a variable in it matches nothing, rather than everything"
|
|
else
|
|
bad "the wildcard rm was refused, but not as ABSENT (same_key is unreached)"
|
|
fi
|
|
|
|
# 15. A rule keys on its whole clause, so an EDITED rule matches nothing and
|
|
# replace would silently become add -- leaving the stale arm firing beside
|
|
# the new one, with correct arithmetic (found by review on PR #69).
|
|
fresh
|
|
printf 'probe_rule(X) :- doctrine(X,_).\n' > "$work/rule1.pl"
|
|
printf 'probe_rule(X) :- doctrine(X,_), X \\== b.\n' > "$work/rule2.pl"
|
|
kb add "$work/rule1.pl" >/dev/null 2>&1
|
|
before="$(kb count | grep '^total=' | cut -d= -f2)"
|
|
if kb replace "$work/rule2.pl" >"$work/out" 2>&1; then
|
|
after="$(kb count | grep '^total=' | cut -d= -f2)"
|
|
bad "replace ADDED an edited rule beside the old one ($before -> $after)"
|
|
elif said "$work/out" "kb rm the old one"; then
|
|
ok "replace refuses a rule it cannot find, and names the route"
|
|
else
|
|
bad "the edited rule was refused, but without naming rm/add"
|
|
fi
|
|
|
|
# The negative arm: replace of a rule that IS there must still work, or the
|
|
# refusal above would just be "replace never works on rules".
|
|
if kb replace "$work/rule1.pl" >/dev/null 2>&1; then
|
|
ok "replace of an unchanged rule is still accepted"
|
|
else
|
|
bad "replace refuses a rule that is present verbatim"
|
|
fi
|
|
|
|
# 16. All three citation markers must FIRE. doctrine( and invariant( take the
|
|
# name as the first field; decision( takes the SECOND, because the repo
|
|
# spells decision(<ticket>, <name>) and a ticket id is not name-shaped --
|
|
# so a single-field rule left that marker unreachable (review, PR #69).
|
|
cat > "$work/cite-d.pl" <<'EOF'
|
|
doctrine(a_probe_citing_a_doctrine,'cites doctrine(a_name_that_was_retired), which does not exist').
|
|
EOF
|
|
cat > "$work/cite-i.pl" <<'EOF'
|
|
doctrine(a_probe_citing_an_invariant,'cites invariant(a_rule_that_was_never_written), which does not exist').
|
|
EOF
|
|
cat > "$work/cite-x.pl" <<'EOF'
|
|
doctrine(a_probe_citing_a_decision,'cites decision(improvise-nope, a_name_that_was_never_decided), which does not exist').
|
|
EOF
|
|
fresh
|
|
markers=0
|
|
for m in d i x; do
|
|
kb check --with "$work/cite-$m.pl" >/dev/null 2>&1 || markers=$((markers+1))
|
|
done
|
|
if [ "$markers" -eq 3 ]; then
|
|
ok "all three citation markers are reachable, not just the first"
|
|
else
|
|
bad "only $markers of 3 citation markers fire"
|
|
fi
|
|
|
|
# 17. The case aimed at has_key/2 itself. A keyed FACT with a variable in a
|
|
# key position -- work_done keys on (id, kind) -- is a key no existing
|
|
# clause is a variant of, so the add must land and every sibling survive.
|
|
# Under unification the fold excludes the clauses the key happens to match
|
|
# and the add is refused instead (by the total, which is the backstop, not
|
|
# the fix). Asserted as the OUTCOME, because that is what a wrong has_key
|
|
# destroys.
|
|
fresh
|
|
before="$(kb count | grep '^work_done/3=' | cut -d= -f2)"
|
|
printf "work_done(_,maintenance,'a probe clause with a variable id').\n" > "$work/wildfact.pl"
|
|
if kb add "$work/wildfact.pl" >"$work/out" 2>&1; then
|
|
after="$(kb count | grep '^work_done/3=' | cut -d= -f2)"
|
|
if [ "$((before + 1))" = "$after" ]; then
|
|
ok "a fact whose key holds a variable adds without excluding its siblings"
|
|
else
|
|
bad "adding one clause moved work_done/3 from $before to $after"
|
|
fi
|
|
else
|
|
bad "add refused a key holding a variable: the fold matched by unification"
|
|
fi
|
|
|
|
echo "kb-test: completeness against HEAD (improvise-usus)"
|
|
|
|
# 18. The incident's shape: clauses gone from the working tree and the rest
|
|
# still CONSISTENT -- 276 of 801 were lost and kb_consistent passed, so the
|
|
# add landed. The fixture must keep kb_consistent green, or a different
|
|
# guard refuses it and the case proves nothing: dropping a whole predicate
|
|
# is an existence error, and dropping cited clauses fails the citation
|
|
# check. So it keeps one location/3 fact and drops the other 34. No
|
|
# KB_BASELINE: this case runs the real `git show HEAD` path, which is also
|
|
# what a guard counting the file against ITSELF would pass.
|
|
fresh
|
|
awk '/^location\(/ { if (seen++) next } { print }' "$KB" > "$work/kb.pl"
|
|
cp "$work/kb.pl" "$work/lost.pl"
|
|
if ! KB_FILE="$work/lost.pl" "$here/kb" check >/dev/null 2>&1; then
|
|
bad "the lossy fixture fails kb_consistent -- case 18 proves nothing"
|
|
else
|
|
kb add "$work/new.pl" >"$work/out" 2>&1; rc=$?
|
|
if [ "$rc" -eq 0 ]; then
|
|
bad "add wrote onto a kb missing 34 of HEAD's clauses"
|
|
elif ! cmp -s "$work/kb.pl" "$work/lost.pl"; then
|
|
bad "the loss was refused but the kb was MODIFIED"
|
|
elif [ "$rc" -ne 1 ]; then
|
|
bad "the loss was refused with exit $rc, not the verdict code 1"
|
|
elif said "$work/out" "34 of the baseline's are missing"; then
|
|
ok "add refuses a kb that lost clauses HEAD has, and names how many"
|
|
else
|
|
bad "the loss was refused, but not BY THE COMPLETENESS GUARD"
|
|
fi
|
|
fi
|
|
|
|
# 19. The ticket's own fixture: a copy truncated to half its clauses. This one
|
|
# ALSO breaks kb_consistent, so said() is what makes it evidence -- the
|
|
# completeness guard runs first and must be the one that answers.
|
|
fresh
|
|
head -n "$(( $(wc -l < "$KB") / 2 ))" "$KB" > "$work/kb.pl"
|
|
cp "$work/kb.pl" "$work/half.pl"
|
|
if kb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
bad "add wrote onto a kb truncated to half"
|
|
elif ! cmp -s "$work/kb.pl" "$work/half.pl"; then
|
|
bad "the truncation was refused but the kb was MODIFIED"
|
|
elif said "$work/out" "no kb rm recorded their removal"; then
|
|
ok "a kb truncated to half is refused by name, byte-identical"
|
|
else
|
|
bad "the truncation was refused, but not by the completeness guard"
|
|
fi
|
|
|
|
# 20. rm is how the count legitimately falls, and the ledger is how a LATER
|
|
# write knows it: rm a clause HEAD has, then add -- the add must land. A
|
|
# ledger that is never written, or is ignored, refuses here.
|
|
fresh
|
|
printf "location(cli_args,'src/main.rs',_).\n" > "$work/drop-head.pl"
|
|
if ! kb rm "$work/drop-head.pl" >"$work/out" 2>&1; then
|
|
bad "rm of a clause HEAD has was refused: $(tail -1 "$work/out")"
|
|
elif kb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
ok "an add after a recorded rm is accepted"
|
|
else
|
|
bad "an add after a legitimate rm was refused: the removal was not recorded"
|
|
fi
|
|
|
|
# 20b. ...and the record excuses exactly what it names. A second, unrecorded
|
|
# loss on top of a recorded rm must still refuse; a guard that stands down
|
|
# whenever a ledger exists passes 20 and fails here. The second loss is
|
|
# made by giving the BASELINE a clause, not by editing the kb: an edit
|
|
# voids the ledger (case 24), which would test that instead.
|
|
awk -v x="location(a_probe_only_head_has,'src/nowhere.rs',probe)." '
|
|
{ line[NR] = $0 } /^location\(/ { last = NR }
|
|
END { for (i = 1; i <= NR; i++) { print line[i]; if (i == last) print x } }
|
|
' "$KB" > "$work/head-plus.pl"
|
|
cp "$work/kb.pl" "$work/twice.pl"
|
|
printf "doctrine(another_probe_after_the_rm,'x').\n" > "$work/new2.pl"
|
|
if KB_BASELINE="$work/head-plus.pl" kb add "$work/new2.pl" >"$work/out" 2>&1; then
|
|
bad "a recorded rm excused an unrecorded loss beside it"
|
|
elif cmp -s "$work/kb.pl" "$work/twice.pl" && said "$work/out" "1 of the baseline's are missing" \
|
|
&& said "$work/out" "a_probe_only_head_has"; then
|
|
ok "a recorded rm excuses only the clause it removed"
|
|
else
|
|
bad "the unrecorded loss was refused, but not by name, or the kb changed"
|
|
fi
|
|
|
|
# 21. A usage error, an unreadable baseline and a verdict are three exit codes.
|
|
# Sharing one is improvise-b4ks: "could not check" reading as "refused".
|
|
fresh
|
|
KB_BASELINE="$work/no-such-file.pl" kb add "$work/new.pl" >/dev/null 2>&1; rc3=$?
|
|
kb add >/dev/null 2>&1; rc2=$?
|
|
if [ "$rc3" -eq 3 ] && [ "$rc2" -eq 2 ] && unchanged; then
|
|
ok "an unreadable baseline exits 3 and usage exits 2, neither a verdict"
|
|
else
|
|
bad "exit codes: unreadable baseline $rc3 (want 3), usage $rc2 (want 2)"
|
|
fi
|
|
|
|
# 22. A killed write leaves the old kb. The tool SIGKILLs itself once the
|
|
# candidate is complete and checked, just before publishing it. Two rivals
|
|
# this separates: writing into the kb in place (the kb changes), and
|
|
# building the candidate in $TMPDIR, where mv may cross a device and copy
|
|
# -- so the candidate must be a sibling of the kb, making mv a rename(2).
|
|
fresh
|
|
KB_TEST_KILL="$work/killed" kb add "$work/new.pl" >/dev/null 2>&1; rc=$?
|
|
cand="$(cat "$work/killed" 2>/dev/null)"
|
|
if [ "$rc" -ne 137 ] || [ -z "$cand" ]; then
|
|
bad "the kill seam did not fire (exit $rc) -- case 22 proves nothing"
|
|
elif ! unchanged; then
|
|
bad "a write killed before publishing MODIFIED the kb"
|
|
elif [ "$(dirname "$cand")" != "$work" ]; then
|
|
bad "the candidate was built in $(dirname "$cand"), not beside the kb: mv may copy"
|
|
elif ! grep -q '^doctrine(a_name_that_is_certainly_not_taken,' "$cand"; then
|
|
bad "the candidate was not complete when the write died"
|
|
else
|
|
ok "a write killed before its rename leaves the old kb byte-identical"
|
|
fi
|
|
|
|
echo "kb-test: what the ledger and the key comparison can be fooled by"
|
|
|
|
# 23. Keys compared as a SET cannot see one of two clauses sharing a key
|
|
# (improvise-ih3k). work_done/3 keys on (id, kind) and is not functional/1,
|
|
# so a git merge can commit two clauses under one key. Dropping one then
|
|
# leaves the key present and the loss unseen. The baseline carries the pair.
|
|
awk -v a="work_done('improvise-zzzz',bug_fix,'first fix, merged from branch A')." \
|
|
-v b="work_done('improvise-zzzz',bug_fix,'review fix, merged from branch B')." '
|
|
{ line[NR] = $0 } /^work_done\(/ { last = NR }
|
|
END { for (i = 1; i <= NR; i++) { print line[i]; if (i == last) { print a; print b } } }
|
|
' "$KB" > "$work/pair-base.pl"
|
|
grep -v "^work_done('improvise-zzzz',bug_fix,'review fix" "$work/pair-base.pl" > "$work/pair-lost.pl"
|
|
pkb() { KB_FILE="$work/kb.pl" KB_BASELINE="$work/pair-base.pl" "$here/kb" "$@"; }
|
|
fresh
|
|
if ! KB_FILE="$work/pair-base.pl" "$here/kb" check >/dev/null 2>&1; then
|
|
bad "the paired baseline fails kb_consistent -- case 23 proves nothing"
|
|
elif [ "$(grep -c "^work_done('improvise-zzzz'" "$work/pair-lost.pl")" -ne 1 ]; then
|
|
bad "the lossy fixture does not hold exactly one of the pair -- case 23 proves nothing"
|
|
else
|
|
cp "$work/pair-lost.pl" "$work/kb.pl"
|
|
if pkb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
bad "add wrote onto a kb that lost one of two clauses sharing a key"
|
|
elif ! cmp -s "$work/kb.pl" "$work/pair-lost.pl"; then
|
|
bad "the lost twin was refused but the kb was MODIFIED"
|
|
elif said "$work/out" "review fix, merged from branch B"; then
|
|
ok "losing one of two clauses under one key is refused, naming the one lost"
|
|
else
|
|
bad "the lost twin was refused, but the refusal does not name it"
|
|
fi
|
|
# The pair itself is not a loss: an add onto the intact pair must land, or
|
|
# the guard has turned "HEAD holds a duplicate" into "nothing may be written".
|
|
cp "$work/pair-base.pl" "$work/kb.pl"
|
|
if pkb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
ok "an add onto a kb that still holds both clauses of a pair is accepted"
|
|
else
|
|
bad "the intact pair was refused: $(tail -1 "$work/out")"
|
|
fi
|
|
# And the pair has a way out through the tool: rm the key (both go, recorded),
|
|
# add back the survivor, and a later write must still land.
|
|
printf "work_done('improvise-zzzz',bug_fix,_).\n" > "$work/pair-key.pl"
|
|
printf "work_done('improvise-zzzz',bug_fix,'the fix, both halves').\n" > "$work/pair-one.pl"
|
|
printf "doctrine(a_probe_after_the_pair_is_resolved,'x').\n" > "$work/after-pair.pl"
|
|
if ! pkb rm "$work/pair-key.pl" >"$work/out" 2>&1; then
|
|
bad "rm of a key HEAD holds twice was refused: $(tail -1 "$work/out")"
|
|
elif ! pkb add "$work/pair-one.pl" >"$work/out" 2>&1; then
|
|
bad "re-adding one clause for a removed pair was refused: $(tail -1 "$work/out")"
|
|
elif ! pkb add "$work/after-pair.pl" >"$work/out" 2>&1; then
|
|
bad "a write after resolving the pair was refused: $(tail -1 "$work/out")"
|
|
else
|
|
ok "a pair is resolved by rm then add, and later writes still land"
|
|
fi
|
|
fi
|
|
|
|
# 24. A ledger entry excuses only the kb it was recorded against
|
|
# (improvise-yea8). rm X, then restore kb.pl the way the refusal message
|
|
# recommends -- not a write, so nothing prunes -- then lose X some other
|
|
# way. The ledger entry from the abandoned rm must not excuse that loss.
|
|
fresh
|
|
printf "location(cli_args,'src/main.rs',_).\n" > "$work/drop-x.pl"
|
|
grep -v "^location(cli_args," "$KB" > "$work/lost-x.pl"
|
|
if ! kb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
|
bad "rm of a clause HEAD has was refused -- case 24 proves nothing"
|
|
elif [ ! -s "$work/kb.pl.removed" ]; then
|
|
bad "rm left no ledger -- case 24 proves nothing"
|
|
else
|
|
cp "$work/lost-x.pl" "$work/kb.pl"
|
|
if kb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
bad "a ledger entry from an abandoned rm excused a later loss of that clause"
|
|
elif ! cmp -s "$work/kb.pl" "$work/lost-x.pl"; then
|
|
bad "the stale excuse was refused but the kb was MODIFIED"
|
|
elif said "$work/out" "location(cli_args,'src/main.rs',clap)"; then
|
|
ok "a ledger entry does not outlive the kb its rm produced"
|
|
else
|
|
bad "the loss was refused, but not by naming the lost clause"
|
|
fi
|
|
fi
|
|
|
|
# 24b. ...and still excuses it across the tool's own writes: the stamp moves
|
|
# with each write, so rm then add then add must all land. A ledger stamped
|
|
# only by rm passes 24 and refuses the second add here.
|
|
fresh
|
|
printf "doctrine(a_second_probe_after_the_rm,'x').\n" > "$work/new3.pl"
|
|
if ! kb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
|
bad "rm refused -- case 24b proves nothing"
|
|
elif ! kb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
bad "the first add after an rm was refused: $(tail -1 "$work/out")"
|
|
elif ! kb add "$work/new3.pl" >"$work/out" 2>&1; then
|
|
bad "the second add after an rm was refused: the ledger did not follow the write"
|
|
else
|
|
ok "a recorded rm stays excused across the tool's later writes"
|
|
fi
|
|
|
|
# 25. The production paths, which every case above bypasses by setting KB_FILE:
|
|
# the baseline is `git show HEAD` and the ledger is `git rev-parse
|
|
# --git-path`. Run in a throwaway repo holding a copy of the tool.
|
|
r="$work/repo"
|
|
mkdir -p "$r/scripts" "$r/prolog-sessions"
|
|
cp "$here/kb" "$here/kb-merge.pl" "$r/scripts/"
|
|
cp "$KB" "$r/prolog-sessions/kb.pl"
|
|
g() { git -C "$r" -c user.name=kb-test -c user.email=kb-test@invalid "$@"; }
|
|
rkb() { (unset KB_FILE KB_BASELINE; "$r/scripts/kb" "$@"); }
|
|
if ! { g init -q && g add -A && g commit -qm base; } >/dev/null 2>&1; then
|
|
bad "could not build the throwaway repo -- case 25 proves nothing"
|
|
elif ! rkb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
|
bad "rm in a real repo was refused: $(tail -1 "$work/out")"
|
|
else
|
|
ledger="$(g rev-parse --path-format=absolute --git-path kb-removed.pl)"
|
|
if ! grep -q "^location(cli_args," "$ledger" 2>/dev/null; then
|
|
bad "rm in a real repo did not record its removal at the git-path ledger"
|
|
elif [ "$(g status --porcelain --untracked-files=all)" != " M prolog-sessions/kb.pl" ]; then
|
|
bad "the real-repo write left something git sees: $(g status --porcelain --untracked-files=all | tr '\n' ' ')"
|
|
elif ! rkb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
bad "the git-path ledger did not excuse its own rm: $(tail -1 "$work/out")"
|
|
else
|
|
g checkout -q -- prolog-sessions/kb.pl
|
|
cp "$work/lost-x.pl" "$r/prolog-sessions/kb.pl"
|
|
if rkb add "$work/new.pl" >"$work/out" 2>&1; then
|
|
bad "after git checkout restored the kb, the git-path ledger excused a new loss"
|
|
elif said "$work/out" "location(cli_args,'src/main.rs',clap)"; then
|
|
ok "the git-path ledger and HEAD baseline work, and a loss after a restore is refused"
|
|
else
|
|
bad "the real-repo loss was refused, but not by naming it"
|
|
fi
|
|
fi
|
|
fi
|
|
|
|
printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail"
|
|
[ "$fail" -eq 0 ]
|