From b3a41bca57e0f12c411dc324f8b5a03d7a34d17c Mon Sep 17 00:00:00 2001 From: Edward Langley Date: Tue, 22 Sep 2026 21:06:34 -0700 Subject: [PATCH 1/5] kb: count keys, so one of a pair sharing a key cannot vanish (improvise-ih3k) WIP: cases 23-24 added; 24 (improvise-yea8) still fails. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- scripts/kb-merge.pl | 50 +++++++++++++++++++----- scripts/kb-test.sh | 92 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 132 insertions(+), 10 deletions(-) diff --git a/scripts/kb-merge.pl b/scripts/kb-merge.pl index 2985f912..38ac2461 100644 --- a/scripts/kb-merge.pl +++ b/scripts/kb-merge.pl @@ -35,8 +35,11 @@ run(remove, KbFile, DeltaFile, OutFile) :- halt(2) ), foldl_remove(Funcs, Doomed, Old, Kept), - length(Old, NOld), length(Doomed, NDoomed), - ExpectK is NOld - NDoomed, + length(Old, NOld), + findall(x, ( member(O, Old), clause_key(Funcs, O, KO), + member(T, Doomed), clause_key(Funcs, T, KT), same_key(KO, KT) ), Hits), + length(Hits, NHits), + ExpectK is NOld - NHits, check_total(Kept, ExpectK), write_terms(OutFile, Kept), verify(OutFile, Kept), @@ -325,24 +328,27 @@ count_only(KbFile) :- % 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. +% Keys are counted, not collected: a merge can commit two clauses under one +% key, and a set of keys cannot see one of them go (improvise-ih3k). complete(BaseFile, CandFile, ExcFile, LedgerOut) :- terms_of(BaseFile, Base), terms_of(CandFile, Cand), terms_of(ExcFile, Exc), - ground_keys(Cand, CandKeys), + key_counts(Base, BaseCounts), + key_counts(Cand, CandCounts), ground_keys(Exc, ExcKeys), - findall(T, ( member(T, Base), ground_key(T, K), - \+ memberchk(K, CandKeys), \+ memberchk(K, ExcKeys) ), Missing), + findall(K-D, ( member(K-NBK, BaseCounts), count_of(K, CandCounts, NCK), + D is NBK - NCK, D > 0 ), Short), + findall(K-D, ( member(K-D, Short), \+ memberchk(K, ExcKeys) ), Unexcused), + findall(T, ( member(K-_, Unexcused), lost_under(K, Base, Cand, T) ), 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), + ( Unexcused == [] + -> findall(E, ( member(E, Exc), ground_key(E, K), memberchk(K-_, Short) ), 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), + ; foldl(add_deficit, Unexcused, 0, 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])), @@ -356,5 +362,29 @@ ground_keys(Terms, Sorted) :- findall(C, ( member(T, Terms), ground_key(T, C) ), Cs), sort(Cs, Sorted). +key_counts(Terms, Counts) :- + findall(C, ( member(T, Terms), ground_key(T, C) ), Cs), + msort(Cs, Sorted), + run_lengths(Sorted, Counts). + +run_lengths([], []). +run_lengths([K|T], [K-N|Rest]) :- + same_run(K, T, 1, N, After), + run_lengths(After, Rest). + +same_run(K, [X|T], N0, N, After) :- X == K, !, N1 is N0 + 1, same_run(K, T, N1, N, After). +same_run(_, After, N, N, After). + +count_of(K, Counts, N) :- ( memberchk(K-N0, Counts) -> N = N0 ; N = 0 ). + +add_deficit(_-D, N0, N) :- N is N0 + D. + +% What to name for a short key: the baseline's clauses under it that the +% result holds no variant of, or the first one when every text survives. +lost_under(K, Base, Cand, T) :- + findall(B, ( member(B, Base), ground_key(B, KB), KB == K ), Under), + findall(B, ( member(B, Under), \+ ( member(C, Cand), same_key(B, C) ) ), Gone), + ( Gone == [] -> Under = [T|_] ; member(T, Gone) ). + 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 52797816..3dce2b47 100755 --- a/scripts/kb-test.sh +++ b/scripts/kb-test.sh @@ -611,5 +611,97 @@ 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 + printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail" [ "$fail" -eq 0 ] From d90c45c14e4bde11fe4852a188c9fed1979b94b3 Mon Sep 17 00:00:00 2001 From: Edward Langley Date: Tue, 22 Sep 2026 21:09:17 -0700 Subject: [PATCH 2/5] kb: a ledger excuses only the kb file its write published (improvise-yea8) Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- scripts/kb | 19 +++++++++++++++---- scripts/kb-test.sh | 14 ++++++++++---- 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/scripts/kb b/scripts/kb index bd029e86..f4465e6f 100755 --- a/scripts/kb +++ b/scripts/kb @@ -72,7 +72,7 @@ acquire_lock() { scratch=() new_cand() { cand="$(mktemp "$KB.cand.XXXXXX")" - scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base") + scratch+=("$cand" "$cand.delta" "$cand.removed" "$cand.ledger" "$cand.base" "$cand.stamped") } # What `kb rm` removed that HEAD still has: the record that tells an intended @@ -83,6 +83,14 @@ ledger_path() { fi } +# A ledger speaks only for the kb FILE this tool last published, named on its +# first line; bytes alone are not enough, since a restore can reproduce them. +file_stamp() { + printf '%s %s' "$(stamp_of "$1")" \ + "$(stat -c '%i %.9Y' "$1" 2>/dev/null || stat -f '%i %Fm' "$1")" +} +ledger_holds() { [ -f "$1" ] && [ "$(head -n 1 "$1")" = "% kb-stamp $(file_stamp "$2")" ]; } + # The committed knowledge base, which no write may end up short of. # KB_BASELINE is the test seam, naming a file. baseline_to() { @@ -140,19 +148,22 @@ commit() { # $1 = candidate, $2 = stamp of the kb as read, $3 = keys a rm remove 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 ledger_holds "$ledger" "$KB"; 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 + echo "kb: restore it from HEAD (git show HEAD:prolog-sessions/kb.pl) and re-apply your deltas." >&2 + echo "kb: do NOT commit this kb.pl: a committed loss becomes the floor this check compares against." >&2 + echo "kb: to drop a clause on purpose, restore first and then kb rm it." >&2 exit 1 fi if ! check_file "$cand"; then echo "kb: REFUSED -- kb_consistent fails on the result; $KB is unchanged" >&2 exit 1 fi + { printf '%% kb-stamp %s\n' "$(file_stamp "$cand")"; cat "$cand.ledger"; } > "$cand.stamped" kill_hook "$cand" - mv -f "$cand.ledger" "$ledger" + mv -f "$cand.stamped" "$ledger" mv -f "$cand" "$KB" } diff --git a/scripts/kb-test.sh b/scripts/kb-test.sh index 3dce2b47..fd54fae9 100755 --- a/scripts/kb-test.sh +++ b/scripts/kb-test.sh @@ -568,13 +568,19 @@ 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" +# 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 add "$work/new2.pl" >"$work/out" 2>&1; then +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"; then +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" From 5a79f7385be991233f66ef01c9300a1b394d81dc Mon Sep 17 00:00:00 2001 From: Edward Langley Date: Tue, 22 Sep 2026 21:10:13 -0700 Subject: [PATCH 3/5] kb-test: exercise the git-path ledger and HEAD baseline in a throwaway repo Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- scripts/kb-test.sh | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/scripts/kb-test.sh b/scripts/kb-test.sh index fd54fae9..4960d0a4 100755 --- a/scripts/kb-test.sh +++ b/scripts/kb-test.sh @@ -709,5 +709,39 @@ 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 ] From 4ca3a47b417231470ad4e0955087c975c45a29df Mon Sep 17 00:00:00 2001 From: Edward Langley Date: Tue, 22 Sep 2026 21:17:17 -0700 Subject: [PATCH 4/5] kb: refusal no longer offers committing the loss; skill and kb-tool.md describe the guard (improvise-za97) The kb skill (both copies) now describes the HEAD comparison, the ledger, exit code 3 and the recovery. kb-tool.md records the ih3k/yea8 arguments and corrects the residue paragraph: .gitignore hides the leftovers, and there are six, not one. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- .agents/skills/kb/SKILL.md | 38 ++++++++++- .claude/skills/kb/SKILL.md | 38 ++++++++++- context/code/kb-tool.md | 110 ++++++++++++++++++++++++++----- context/test-evidence/tooling.md | 59 +++++++++++++++++ scripts/kb-test.sh | 11 ++++ 5 files changed, 233 insertions(+), 23 deletions(-) diff --git a/.agents/skills/kb/SKILL.md b/.agents/skills/kb/SKILL.md index 85c0ffc7..ea57a3f6 100644 --- a/.agents/skills/kb/SKILL.md +++ b/.agents/skills/kb/SKILL.md @@ -78,9 +78,41 @@ examples and history belong; prose docs should stay operational. - **Reading through the MCP is fine.** `loadSession` at session start is still how a session gets the model in hand; only writing moved. -Every write verifies the result reads back as intended and runs `kb_consistent` -on the candidate, so a bad delta leaves the file untouched. `count` before and -after is still the cheapest evidence a write did what you meant. +Every write checks three things before it replaces the file: the result reads +back as intended, it still holds every clause **HEAD** has, and `kb_consistent` +passes. So a bad delta leaves the file untouched. `count` before and after is +still the cheapest evidence a write did what you meant. + +## When a write is refused + +Exit codes: `0` done, `1` refused, `2` usage, `3` HEAD's `kb.pl` could not be +read, so nothing was compared, `127` no `tpl`. Only `1` is a verdict. + +**"clauses HEAD has are gone, with no kb rm recorded"** means the working-tree +`kb.pl` is short of the committed one. Your delta did not cause it. The file +was already damaged, by a killed write, a bad merge resolution or an edit. The +refusal lists the clauses that are missing. The check counts clauses **per +key**, so losing one of two clauses that share a key is caught too. + +- **Recover:** `git show HEAD:prolog-sessions/kb.pl > prolog-sessions/kb.pl`, + then re-run your `add`/`replace`/`rm` deltas. +- **Do not commit the short file to get past the refusal.** HEAD is what the + check compares against, so a committed loss becomes the new floor and is + never reported again. +- **To remove a clause on purpose, use `kb rm`.** It records the removal in a + per-worktree ledger (`git rev-parse --git-path kb-removed.pl`, never + committed), and that record is what lets later writes accept the missing + clause. A hand deletion has no record, so it is refused. + +The ledger vouches only for the exact `kb.pl` file the tool last wrote. Any +rewrite outside the tool voids it, including a restore, `git checkout`, `cp` +or an editor. After an `rm`, a restore therefore also undoes the `rm`, and you +must redo it. That is deliberate. Otherwise the abandoned `rm` would go on +excusing a later, accidental loss of the same clause. + +A killed write can leave `kb.pl.cand.*` files and a `kb.pl.lock` directory in +`prolog-sessions/`. Git ignores them. The lock makes the next write wait 30 +seconds and then fail, so delete it if nothing else is writing. `context/code/kb-tool.md` has the argument. `scripts/kb-test.sh` proves each refusal by injecting the fault it names. diff --git a/.claude/skills/kb/SKILL.md b/.claude/skills/kb/SKILL.md index 85c0ffc7..ea57a3f6 100644 --- a/.claude/skills/kb/SKILL.md +++ b/.claude/skills/kb/SKILL.md @@ -78,9 +78,41 @@ examples and history belong; prose docs should stay operational. - **Reading through the MCP is fine.** `loadSession` at session start is still how a session gets the model in hand; only writing moved. -Every write verifies the result reads back as intended and runs `kb_consistent` -on the candidate, so a bad delta leaves the file untouched. `count` before and -after is still the cheapest evidence a write did what you meant. +Every write checks three things before it replaces the file: the result reads +back as intended, it still holds every clause **HEAD** has, and `kb_consistent` +passes. So a bad delta leaves the file untouched. `count` before and after is +still the cheapest evidence a write did what you meant. + +## When a write is refused + +Exit codes: `0` done, `1` refused, `2` usage, `3` HEAD's `kb.pl` could not be +read, so nothing was compared, `127` no `tpl`. Only `1` is a verdict. + +**"clauses HEAD has are gone, with no kb rm recorded"** means the working-tree +`kb.pl` is short of the committed one. Your delta did not cause it. The file +was already damaged, by a killed write, a bad merge resolution or an edit. The +refusal lists the clauses that are missing. The check counts clauses **per +key**, so losing one of two clauses that share a key is caught too. + +- **Recover:** `git show HEAD:prolog-sessions/kb.pl > prolog-sessions/kb.pl`, + then re-run your `add`/`replace`/`rm` deltas. +- **Do not commit the short file to get past the refusal.** HEAD is what the + check compares against, so a committed loss becomes the new floor and is + never reported again. +- **To remove a clause on purpose, use `kb rm`.** It records the removal in a + per-worktree ledger (`git rev-parse --git-path kb-removed.pl`, never + committed), and that record is what lets later writes accept the missing + clause. A hand deletion has no record, so it is refused. + +The ledger vouches only for the exact `kb.pl` file the tool last wrote. Any +rewrite outside the tool voids it, including a restore, `git checkout`, `cp` +or an editor. After an `rm`, a restore therefore also undoes the `rm`, and you +must redo it. That is deliberate. Otherwise the abandoned `rm` would go on +excusing a later, accidental loss of the same clause. + +A killed write can leave `kb.pl.cand.*` files and a `kb.pl.lock` directory in +`prolog-sessions/`. Git ignores them. The lock makes the next write wait 30 +seconds and then fail, so delete it if nothing else is writing. `context/code/kb-tool.md` has the argument. `scripts/kb-test.sh` proves each refusal by injecting the fault it names. diff --git a/context/code/kb-tool.md b/context/code/kb-tool.md index 92ddafe6..bce04912 100644 --- a/context/code/kb-tool.md +++ b/context/code/kb-tool.md @@ -99,34 +99,98 @@ 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 +It compares keys rather than totals, although the ticket asked for a count, +because a total 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. +**Keys are counted, not collected** (improvise-ih3k). The guard first compared +the *set* of keys, and a set cannot see one of two clauses sharing a key. +`work_done/3`, `decision/3` and `work_followup/3` key on two arguments and are +not `functional/1`, so `kb_consistent` accepts two clauses under one key. `kb +add` refuses to *write* such a pair, but a git merge is not a `kb add`: two +branches that each record `work_done(T, bug_fix, …)` conflict at the end of the +block, and keep-both is the natural resolution. Once HEAD holds a pair, losing +either clause left the key present and the write was accepted, with both totals +printed equal. So the guard counts clauses per key, and a key is short when the +result holds fewer than HEAD does. The refusal names the HEAD clauses the result +holds no copy of, which is the one that went. + +Two alternatives were rejected. Comparing whole clauses would refuse every +`replace`, whose purpose is to change the text under a key. Making the three +predicates functional would refuse the pair itself at `kb_consistent`. That +would force a merge to resolve it, and may be worth doing, but it is a change to +the gate in `kb.pl`, not to this tool. `functional/1` also keys an arity-3 +predicate on its first argument, which is wrong for `decision/3`, so it would +need a new two-argument form. And the tool must not lose a clause whatever the +gate allows, so counting is needed either way. + +A pair also had no way out through the tool. `rm` checked its result against +`before - clauses in the delta`, which assumes one clause per key, so removing a +paired key was refused as "a clause was dropped". The expected total is now +`before - clauses the delta's keys match`, which is still counted separately +from the fold that removes them. `replace` of a paired key is still refused by +its total. That is the right answer, because it would silently collapse two +clauses into one. The route for a pair is `kb rm` the key, then `kb add` the one +clause to keep. + **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 +writes read: a key the result is short of is excused only if the ledger names +it. 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: +`KB_FILE` set it sits beside that file. Every write rewrites it, keeping only +the keys the result is still short of, so an entry drops once the removal is +committed and once the key is back to HEAD's count. 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. +is deliberately no override flag. + +The way out of a refusal is to restore `kb.pl` from HEAD and re-apply your +deltas. Do **not** commit the short `kb.pl` to get past it. The refusal +message used to offer that, and taken on a loss nobody intended it makes the +loss permanent: the committed file becomes the floor this guard compares +against, and nothing ever reports it again. A removal you intend goes through +`kb rm`, onto a restored file. + +**A ledger speaks only for the file its write published** (improvise-yea8). +Pruning happens only when the tool writes. A commit, a `git checkout -- +prolog-sessions/kb.pl`, a `cp`, and a branch switch are not writes. So an +entry from an `rm` that was later abandoned would excuse a later loss of that +same clause by any path. That is easy to reach, because the recommended +recovery is exactly a restore. Pruning against the kb read at the next write +cannot close it, because that kb has already lost the clause. So the ledger's +first line is a `% kb-stamp` comment naming the kb file the write published, +and a later write reads the entries only if the kb it finds is still that file. + +The stamp is the content hash **and** the file's inode and nanosecond mtime. +Content alone is not enough, and the test that showed it was the ticket's own +reproduction. `kb.pl` is kept in canonical form, so `grep -v` of one clause +from HEAD produces output **byte-identical** to what `kb rm` of that clause +writes. After `rm X`, a restore, and then the same loss by hand, a content-only +stamp still matched. `rename(2)` carries the candidate's inode and mtime onto +`kb.pl`. Anything else that rewrites the file, whether a `cp` onto it, a git +checkout or an editor, gives a new mtime and usually a new inode. `stat -c` is +tried before `stat -f` because GNU `stat -f` means *filesystem* status and +would silently stamp the wrong thing. It is not keyed by HEAD commit, because a +commit that does not touch `kb.pl` does not make the ledger wrong. And an +uncommitted `rm` carried across a branch switch, with `kb.pl` untouched, is +still exactly the kb it describes. + +The cost is a false refusal after an intended `rm` followed by anything that +rewrites the file without the tool. That refusal is loud, and the recovery is +the usual one: restore and redo the `rm`. **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. +renamed first. A kill between the two renames leaves a ledger stamped for a +candidate that was never published. It therefore matches nothing, and the next +write ignores it. That can refuse a write an earlier `rm` should have excused. +It cannot excuse a loss, which was the hole before the stamp. **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" @@ -139,10 +203,22 @@ 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. +A `SIGKILL` leaves six files behind, because no trap runs: the candidate +`kb.pl.cand.XXXXXX`, its `.base`, `.ledger`, `.removed` and `.stamped` +siblings, and the `kb.pl.lock` directory. None of them is ever read again, +and **git does not see them**. `.gitignore` ignores `prolog-sessions/*`, so +neither `git status --untracked-files=all` nor `git add -A` lists them. That +was measured, and an earlier version of this paragraph warned about `git add +-A` staging them, which does not happen. The one that matters is the lock: the +next write waits 30 seconds for it and then exits 1 with "remove it if stale". +Delete it and the candidates by hand. + +The ledger's stamp names a file by inode and nanosecond mtime. A rewrite that +preserves both, such as a `touch -r`, a filesystem with coarse timestamps +rewriting within one tick, or an inode reused at the same mtime, with the bytes +also identical to what the tool published, is indistinguishable from the file +the tool wrote. That takes deliberate effort or a filesystem this repository +does not run on. 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 diff --git a/context/test-evidence/tooling.md b/context/test-evidence/tooling.md index 38c28214..e3a93412 100644 --- a/context/test-evidence/tooling.md +++ b/context/test-evidence/tooling.md @@ -486,3 +486,62 @@ 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). + +### The kb completeness guard's follow-ups — `scripts/kb-test.sh` cases 19b, 20b, 23–25 + +improvise-ih3k, improvise-yea8 and improvise-za97, filed by the review of PR +#166. The argument is in `context/code/kb-tool.md`. This entry covers what each +case was watched to catch. + +**Reproduced at `f909cad` before any fix.** The new cases 23, 23c and 24 gave +40 passed, 3 failed. 23 failed because an add onto a kb that had lost one of +two `work_done('improvise-zzzz',bug_fix,…)` clauses exited 0. 23c failed +because `rm` of that paired key was refused as "a clause was dropped": its +expected total assumed one clause per key. The tickets did not predict that +one, and it meant a pair could not be resolved through the tool at all. 24 +failed because the stale ledger entry excused the loss. + +**The ticket's own reproduction defeats a content stamp.** The first fix +stamped the ledger with the kb's sha256, and case 24 still failed. `kb.pl` is +canonical, so `grep -v` of one clause from HEAD is byte-identical to what `kb +rm` of that clause writes. The stamp therefore also carries the inode and the +nanosecond mtime. + +**Case 20b had to change, and why that is not a weakening.** It made its +second loss with `sed -i` on the kb. Under the fix, any edit outside the tool +voids the ledger, so 20b then refused two clauses instead of one and failed on +its "1 of" assertion. It was testing the new voiding rather than what its +comment names. The second loss now comes from giving the *baseline* an extra +clause (`KB_BASELINE`). The kb file stays exactly as the tool wrote it, the +ledger stays valid, and the case again isolates "excuses only what it names". +It also now asserts the unexcused clause is named. + +**Rivals injected, one at a time. Each failed only the cases listed:** + +- keys compared as a set (`min(1, N)` per key) in `complete`: 23 only. +- `rm`'s expected total back to `before - |delta|`: 23c's rm step only. +- ledger pruned by key presence rather than count: 23c's final write only. +- ledger honoured whenever it exists: 24 and 25. +- ledger stamped by content alone: 24 only. 25 cannot see it, because its + intervening `add` makes the restored-then-lost file differ in content + anyway. 24 is the case that carries identity. +- ledger re-stamped only by `rm`, keeping the old stamp on other writes: 24b + (as named), 20b and 23c. All three write again after an add. +- ledger stamped with the kb as read rather than the candidate: 20, 20b, 23c, + 24b and 25. That is wider than any one case, as expected, since no later + write can ever match. +- the `gh/main` `scripts/kb` (old refusal text, no stamp): 19b, 24 and 25. + +**Case 25 is the first to run the production paths.** Every other case sets +`KB_FILE`, so `ledger_path`'s `git rev-parse --git-path` branch and +`baseline_to`'s `git show HEAD` were unexercised. It copies the tool into a +throwaway `git init` repo and checks four things. `rm` records to the git-path +ledger. `git status` shows only `kb.pl` modified, so the ledger is invisible +to git. A later `add` is excused. After `git checkout --` and a hand loss, the +`add` is refused. + +**Checked by hand, not in the suite:** a `SIGKILL` at the publish point (the +`KB_TEST_KILL` seam) on a copy inside `prolog-sessions/` leaves the candidate, +its `.base`, `.ledger`, `.removed` and `.stamped` siblings and `.lock`. `git +status --untracked-files=all` and `git add -A --dry-run` both show none of +them, and `git check-ignore -v` names `.gitignore:40` (`prolog-sessions/*`). diff --git a/scripts/kb-test.sh b/scripts/kb-test.sh index 4960d0a4..eda7bd5d 100755 --- a/scripts/kb-test.sh +++ b/scripts/kb-test.sh @@ -553,6 +553,17 @@ 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. From f2a6b9e4cb2d79a5e2f9a35806deb6b6dc7f2e22 Mon Sep 17 00:00:00 2001 From: Edward Langley Date: Tue, 22 Sep 2026 21:19:42 -0700 Subject: [PATCH 5/5] test-evidence: do not spell an ID-shaped fixture name where the audit scans Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/test-evidence/tooling.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/context/test-evidence/tooling.md b/context/test-evidence/tooling.md index e3a93412..c43342ae 100644 --- a/context/test-evidence/tooling.md +++ b/context/test-evidence/tooling.md @@ -495,7 +495,7 @@ case was watched to catch. **Reproduced at `f909cad` before any fix.** The new cases 23, 23c and 24 gave 40 passed, 3 failed. 23 failed because an add onto a kb that had lost one of -two `work_done('improvise-zzzz',bug_fix,…)` clauses exited 0. 23c failed +two `work_done(,bug_fix,…)` clauses exited 0. 23c failed because `rm` of that paired key was refused as "a clause was dropped": its expected total assumed one clause per key. The tickets did not predict that one, and it meant a pair could not be resolved through the tool at all. 24