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 2d350c15..341a0a32 100644 --- a/context/test-evidence/tooling.md +++ b/context/test-evidence/tooling.md @@ -551,3 +551,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(,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 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-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..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. @@ -568,13 +579,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" @@ -611,5 +628,131 @@ 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 ]