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.