diff --git a/context/code/kb-tool.md b/context/code/kb-tool.md index ae881c5d..92ddafe6 100644 --- a/context/code/kb-tool.md +++ b/context/code/kb-tool.md @@ -83,8 +83,67 @@ argument but the last, so `doctrine(Name,_)` keys on the name and through, and it overwrites in place — a count that grew would be two clauses under one name. +**A write may not end up short of HEAD** (improvise-usus). `kb add` wrote four +facts onto a working-tree `kb.pl` that had already lost 276 of its 801, and +reported success: `kb_consistent` asks whether the facts are *consistent*, never +whether they are all *there*, and a knowledge base missing a prefix of a +predicate is perfectly consistent. `kb-merge` printed `529 before` beside a last +known 805 and nothing compared them. The cause was never settled between a +`kb replace` killed mid-write and git being moved under the session, so the +guard had to catch both, and only a comparison against something *outside* the +working tree can: a guard that compares the file against its own pre-write +count passes a file that was truncated before the write began, which is exactly +what happened. So every write runs `kb-merge.pl complete` on the candidate, +before `kb_consistent`, against `git show HEAD:prolog-sessions/kb.pl`, and +refuses unless every clause HEAD has is still present **by key**. It runs first +so that the refusal names the loss rather than whatever consistency error the +loss happens to cause. + +It compares keys rather than counts, although the ticket asked for a count, +because a count can be masked: uncommitted adds in one predicate offset a +truncation in another, and the count comes out even. Keys cost the same (0.26s +for a write, most of it trealla start-up) and the message still names both +totals and the number missing. + +**How the count legitimately falls.** `add` never lowers it and `replace` +overwrites in place, so neither can trip the guard. `kb rm` is the only +intended removal, and it records the keys it removed in a **ledger** that later +writes read: a clause missing from the working tree is excused only if its key +is in the ledger. The ledger lives in the git dir (`git rev-parse --git-path +kb-removed.pl`), so it is per-worktree and can never be committed; with +`KB_FILE` set it sits beside that file. It prunes itself on every write, keeping +only keys HEAD still has and the candidate does not, so an entry drops once the +removal is committed, and once the key is re-added. That second case matters: +without it, a re-added clause that was lost again would still be excused. There +is deliberately no override flag. The way out of a refusal is to restore +`kb.pl` from HEAD and re-apply, or to commit the removal so HEAD moves. + +**The write is a rename.** The candidate used to come from `mktemp` in +`$TMPDIR`, and `mv` from there onto the repository crosses a device wherever +`/tmp` is its own filesystem. That makes `mv` a copy and an unlink, so a kill +partway through leaves a truncated `kb.pl`. The candidate is now a sibling of +`kb.pl` (`kb.pl.cand.XXXXXX`), so publishing it is `rename(2)`. The ledger is +renamed first. A kill between the two renames then leaves a ledger naming keys +the kb still has, and the next write prunes those entries. Until it does, they +would excuse the loss of exactly those clauses, which is a narrower hole than a +kb.pl that is already short. + +**Exit codes.** 0 done, 1 refused, 2 usage, 3 HEAD's `kb.pl` could not be read, +127 no `tpl`. Only 1 is a verdict. 3 is separate because "could not compare" +is not "compared and refused" (improvise-b4ks). A pre-existing wart survives: +failing to acquire the lock exits 1 too. + ## What no test here reaches +The completeness guard trusts HEAD. A loss that has been **committed** is +invisible to it by construction. That was the right trade for this incident, +where HEAD held all 801, but a bad commit of `kb.pl` becomes the new floor. + +A `SIGKILL` leaves its `kb.pl.cand.*` and `kb.pl.lock` behind, because no trap +runs. The lock already had that property. The stray candidate is new: it is +never read, but it shows as untracked in `prolog-sessions/`, where a `git add +-A` would pick it up. + The key rule is looser than `functional/1` for `crate/3`, which keys on the first argument alone; `kb_consistent` is the backstop for that case rather than the merge. diff --git a/context/test-evidence/tooling.md b/context/test-evidence/tooling.md index 5d2b0a1e..38c28214 100644 --- a/context/test-evidence/tooling.md +++ b/context/test-evidence/tooling.md @@ -438,3 +438,51 @@ same way: the suite passed *under a rival*. The generalisable rule is that a stub must fail in the **shape** of the real fault, not merely fail — a stub that breaks more than the real thing breaks satisfies the test through the wrong arm, and reads exactly like coverage. + +### The kb tool's completeness guard and atomic write — `scripts/kb-test.sh` cases 18–22 + +improvise-usus: `scripts/kb add` wrote onto a working-tree `kb.pl` that had lost +276 of its 801 clauses, and `kb_consistent` passed. The argument for the fix +(compare with HEAD by key, record `kb rm` removals in a ledger, publish by +rename) is in `context/code/kb-tool.md`. This entry covers what each case was +watched to catch. + +**Reproduced at `40b8913` before any fix.** A copy of HEAD's `kb.pl` with 34 of +its 35 `location/3` facts removed still passes `kb_consistent`, and +`kb add` onto it printed `775 before, 1 in delta, 776 after` and exited 0. +Against the unfixed tool, the new cases gave 33 passed, 5 failed: 18, 19, 20b, +21 and 22 failed. Case 20 passed there because an rm followed by an add has no +guard to trip. + +**The fixture has to fail in the incident's shape.** The ticket's "truncate to +half" fixture also breaks `kb_consistent`, because the rules live in the second +half. So the unfixed tool refused it too, by the wrong guard. Removing a whole +predicate is an existence error, and removing cited clauses fails the citation +check. Case 18 keeps one `location/3` fact and asserts that the fixture passes +`kb_consistent` before using it. Case 19 keeps the ticket's half-truncation, and +`said()` is what makes it evidence: the completeness guard runs first and must +be the one that answers. + +**Rivals injected into `scripts/kb`, one at a time. Each failed only its own +case:** + +- baseline taken from the file's own pre-write state rather than HEAD: 18, 19 + and 20b failed (35/38 passed). This is the guard that would have passed the + real incident. +- ledger never consulted: 20 and 20b failed. A legitimate rm then blocks every + later write. +- guard stands down whenever the ledger is non-empty: 20b failed. +- candidate built by plain `mktemp` in `$TMPDIR`: 22 failed on the directory + check. +- candidate copied over `kb.pl` before the publish point: 22 failed as + modified. +- unreadable baseline exiting 1 rather than 3: 21 failed. + +**A rival can fail wider than its fault.** The first form of the "stands down" +rival skipped `merge complete` altogether. That also skipped writing +`$cand.ledger`, so the later `mv` crashed under `set -e` and five unrelated +cases failed. It proved nothing until it was rewritten to carry the ledger +forward. + +**Checked by hand, not in the suite:** the ledger prunes an entry once the key +is re-added and once HEAD stops having it (a committed removal). diff --git a/scripts/kb b/scripts/kb index 68998f01..bd029e86 100755 --- a/scripts/kb +++ b/scripts/kb @@ -9,6 +9,8 @@ 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}" +# Exit codes: 0 done, 1 REFUSED (a verdict on the write), 2 usage, 3 the +# completeness baseline could not be read, 127 no tpl. Only 1 is a verdict. # 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 @@ -62,7 +64,39 @@ acquire_lock() { fi sleep 0.1 done - trap 'rmdir "$KB.lock" 2>/dev/null || true' EXIT + trap 'rm -f "${scratch[@]}"; rmdir "$KB.lock" 2>/dev/null || true' EXIT +} + +# Every temporary a writing command makes. The candidate lives BESIDE the kb, so +# publishing it is a rename(2): a mv from $TMPDIR may cross a device and copy. +scratch=() +new_cand() { + cand="$(mktemp "$KB.cand.XXXXXX")" + scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base") +} + +# What `kb rm` removed that HEAD still has: the record that tells an intended +# removal from a lost clause. A fixture's sits beside it; the real one in .git. +ledger_path() { + if [ -n "${KB_FILE:-}" ]; then echo "$KB.removed" + else git -C "$repo" rev-parse --path-format=absolute --git-path kb-removed.pl + fi +} + +# The committed knowledge base, which no write may end up short of. +# KB_BASELINE is the test seam, naming a file. +baseline_to() { + if [ -n "${KB_BASELINE:-}" ]; then cp -f "$KB_BASELINE" "$1" + else git -C "$repo" show HEAD:prolog-sessions/kb.pl > "$1" 2>/dev/null + fi +} + +# Test seam: SIGKILL once the candidate is complete and checked, before it is +# published -- where a killed write dies. Records the candidate's path first. +kill_hook() { + [ -n "${KB_TEST_KILL:-}" ] || return 0 + echo "$1" > "$KB_TEST_KILL" + kill -9 $$ } # Test seam: simulate another writer landing between the read and the commit. @@ -83,14 +117,17 @@ usage: kb replace add clauses, overwriting existing keys rm 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. +Every writing command verifies the result reads back as the clauses intended, +still holds every clause HEAD has that no `kb rm` removed, and passes +kb_consistent before it replaces the knowledge base. + +Exit: 0 done, 1 refused, 2 usage, 3 HEAD's kb.pl unreadable, 127 no tpl. EOF exit 2 } -commit() { # $1 = candidate file, $2 = stamp of the kb before it was read - local cand="$1" was="${2:-}" +commit() { # $1 = candidate, $2 = stamp of the kb as read, $3 = keys a rm removes + local cand="$1" was="${2:-}" removing="${3:-}" ledger race_hook if [ -n "$was" ] && [ "$(stamp_of "$KB")" != "$was" ]; then rm -f "$cand" @@ -98,11 +135,24 @@ commit() { # $1 = candidate file, $2 = stamp of the kb before it was read echo "kb: another writer won; re-run and your delta applies on top." >&2 exit 1 fi + ledger="$(ledger_path)" + if ! baseline_to "$cand.base"; then + echo "kb: cannot read the committed kb.pl to compare against; $KB is unchanged" >&2 + exit 3 + fi + { if [ -f "$ledger" ]; then cat "$ledger"; fi + if [ -n "$removing" ]; then cat "$removing"; fi; } > "$cand.removed" + if ! merge complete "$cand.base" "$cand" "$cand.removed" "$cand.ledger"; then + echo "kb: REFUSED -- clauses HEAD has are gone, with no kb rm recorded; $KB is unchanged." >&2 + echo "kb: restore it from HEAD and re-apply your deltas, or commit the removal." >&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 + kill_hook "$cand" + mv -f "$cand.ledger" "$ledger" mv -f "$cand" "$KB" } @@ -138,7 +188,7 @@ case "$cmd" in fmt) acquire_lock was="$(stamp_of "$KB")" - cand="$(mktemp)" + new_cand : > "${cand}.delta" if ! merge add "$KB" "${cand}.delta" "$cand" >/dev/null 2>&1; then rm -f "$cand" "${cand}.delta" @@ -153,20 +203,20 @@ case "$cmd" in [ $# -eq 1 ] || usage acquire_lock was="$(stamp_of "$KB")" - cand="$(mktemp)" + new_cand if ! merge remove "$KB" "$1" "$cand"; then rm -f "$cand" echo "kb: REFUSED -- $KB is unchanged" >&2 exit 1 fi - commit "$cand" "$was" + commit "$cand" "$was" "$1" echo "kb: $KB updated" ;; add|replace) [ $# -eq 1 ] || usage acquire_lock was="$(stamp_of "$KB")" - cand="$(mktemp)" + new_cand if ! merge "$cmd" "$KB" "$1" "$cand"; then rm -f "$cand" echo "kb: REFUSED -- $KB is unchanged" >&2 diff --git a/scripts/kb-merge.pl b/scripts/kb-merge.pl index 580b2d08..2985f912 100644 --- a/scripts/kb-merge.pl +++ b/scripts/kb-merge.pl @@ -10,7 +10,9 @@ main :- -> run(Mode, KbFile, DeltaFile, OutFile) ; Argv = [CountStr, KbFile], CountStr == "count" -> count_only(KbFile) - ; die('usage: kb-merge.pl | count ') + ; Argv = [CS, BaseFile, CandFile, ExcFile, LedgerOut], CS == "complete" + -> complete(BaseFile, CandFile, ExcFile, LedgerOut) + ; die('usage: kb-merge.pl | count | complete ') ). % argv arrives as strings; every later comparison is on an atom. @@ -321,5 +323,38 @@ count_only(KbFile) :- length(Terms, Total), format("total=~w~n", [Total]). +% Consistency is not completeness: a kb that lost 276 clauses still passed +% kb_consistent. Why by key and against HEAD: context/code/kb-tool.md. +complete(BaseFile, CandFile, ExcFile, LedgerOut) :- + terms_of(BaseFile, Base), + terms_of(CandFile, Cand), + terms_of(ExcFile, Exc), + ground_keys(Cand, CandKeys), + ground_keys(Exc, ExcKeys), + findall(T, ( member(T, Base), ground_key(T, K), + \+ memberchk(K, CandKeys), \+ memberchk(K, ExcKeys) ), Missing), + length(Base, NB), length(Cand, NC), + ( Missing == [] + -> ground_keys(Base, BaseKeys), + findall(E, ( member(E, Exc), ground_key(E, K), + memberchk(K, BaseKeys), \+ memberchk(K, CandKeys) ), Kept), + write_terms(LedgerOut, Kept), + length(Kept, NK), + format("kb-merge: complete -- baseline ~w, result ~w, ~w removal(s) recorded~n", + [NB, NC, NK]) + ; length(Missing, NM), + format("kb-merge: REFUSED -- the baseline has ~w clauses and the result ~w; ~w of the baseline's are missing and no kb rm recorded their removal:~n", + [NB, NC, NM]), + forall(( nth1(I, Missing, T), I =< 10 ), format(" ~q~n", [T])), + ( NM > 10 -> Rest is NM - 10, format(" ... and ~w more~n", [Rest]) ; true ), + halt(2) + ). + +ground_key(T, C) :- clause_key([], T, K), canon_key(K, C). + +ground_keys(Terms, Sorted) :- + findall(C, ( member(T, Terms), ground_key(T, C) ), Cs), + sort(Cs, Sorted). + die(Msg) :- format("kb-merge: ~w~n", [Msg]), halt(2). die_file(F) :- format("kb-merge: cannot read ~w~n", [F]), halt(2). diff --git a/scripts/kb-test.sh b/scripts/kb-test.sh index 69e8eed0..52797816 100755 --- a/scripts/kb-test.sh +++ b/scripts/kb-test.sh @@ -5,9 +5,15 @@ 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 +# 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 @@ -15,7 +21,8 @@ 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"; } +# 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 @@ -500,5 +507,109 @@ 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. +sed -i.bak '/^location(add_command,/d' "$work/kb.pl"; rm -f "$work/kb.pl.bak" +cp "$work/kb.pl" "$work/twice.pl" +printf "doctrine(another_probe_after_the_rm,'x').\n" > "$work/new2.pl" +if 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"; 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 + printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail" [ "$fail" -eq 0 ]