Merge remote-tracking branch 'gh/main' into docs/wave-agent-rules

AGENTS.md

@@ -134,9 +134,16 @@ does not go into the next brief.
    reports spurious failures. And **never pipe a gate**: `$?` must be the gate's
    own, and `check-comment-runs.py --check-evidence` prints two lines with the
    comment cap **first**, so `| tail -1` silently drops half of it.
-4. **Do not push, do not merge to `main`.** The orchestrator merges.
-5. The commit-message trailers, spelled out.
-6. **What to report**: branch and commits, what changed per ticket, *what could
+4. **Commit frequently, so the work is safe in git.** A WIP commit after the
+   first green test, and again after every meaningful step. A worktree is not
+   durable storage: an agent finished a whole ticket with every gate green and
+   lost all of it, uncommitted, when its worktree was deleted during a disk
+   cleanup. Tidying the history before the PR is fine; losing it is not.
+5. **Do not merge to `main`.** The orchestrator merges. Pushing the agent's own
+   branch (`git push gh HEAD:refs/heads/<branch>`) is encouraged once it is
+   worth keeping.
+6. The commit-message trailers, spelled out.
+7. **What to report**: branch and commits, what changed per ticket, *what could
    not be verified and why*, and proposed repo-map/`kb.pl` text. Ask explicitly
    for the thing the agent learned that the ticket did not predict — that is
    consistently the most valuable part of a hand-back, and agents omit it unless

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.

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).

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 <command>
   replace <delta.pl>    add clauses, overwriting existing keys
   rm <keys.pl>          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

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 <add|replace> <kb> <delta> <out>  |  count <kb>')
+    ;  Argv = [CS, BaseFile, CandFile, ExcFile, LedgerOut], CS == "complete"
+    -> complete(BaseFile, CandFile, ExcFile, LedgerOut)
+    ;  die('usage: kb-merge.pl <add|replace|remove> <kb> <delta> <out>  |  count <kb>  |  complete <baseline> <candidate> <removed> <ledger-out>')
     ).
 
 % 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).

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 ]