#!/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)"
KB="$repo/prolog-sessions/kb.pl"
work="$(mktemp -d)"
trap 'rm -rf "$work"' EXIT

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.
fresh() { 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 is also the discriminating door --
# under unification `conflicts` sees the non-ground key match both facts and
# refuses the add outright, so the reverted fix fails HERE.
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

printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail"
[ "$fail" -eq 0 ]