#!/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

# 19b. ...and the refusal must not offer committing the loss as the way out:
#      a committed loss becomes the floor, and is never reported again
#      (improvise-za97).
if said "$work/out" "commit the removal"; then
  bad "the refusal still offers committing an unexplained loss"
elif said "$work/out" "do NOT commit"; then
  ok "the refusal warns against committing the loss"
else
  bad "the refusal says nothing about committing the short kb"
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 ]