7 Commits

Author SHA1 Message Date
Ed Langley ae96b8ccaa Merge pull request #179 from fiddlerwoaroof/fix/kb-guard-followups
CI / Build all bundles (push) Has been cancelled
CI / Test and lint (host) (push) Has been cancelled
CI / wasm32 check (browser bundle crates) (push) Has been cancelled
CI / Browser JS unit tests (node --test) (push) Has been cancelled
CI / Knowledge base consistency (push) Has been cancelled
CI / Lint the harness crate (push) Has been cancelled
CI / Browser harness (OPFS contract + shell) (push) Has been cancelled
CI / Deploy to GitHub Pages (push) Has been cancelled
kb: count keys, tie the rm ledger to the file it describes, fix the guard's docs (ih3k, yea8, za97)
2026-09-22 21:29:29 -07:00
Edward Langley 947298952d Merge remote-tracking branch 'gh/main' into fix/kb-guard-followups 2026-09-22 21:19:47 -07:00
Edward Langley f2a6b9e4cb test-evidence: do not spell an ID-shaped fixture name where the audit scans
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
2026-09-22 21:19:42 -07:00
Edward Langley 4ca3a47b41 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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
2026-09-22 21:17:17 -07:00
Edward Langley 5a79f7385b kb-test: exercise the git-path ledger and HEAD baseline in a throwaway repo
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
2026-09-22 21:10:13 -07:00
Edward Langley d90c45c14e kb: a ledger excuses only the kb file its write published (improvise-yea8)
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
2026-09-22 21:09:17 -07:00
Edward Langley b3a41bca57 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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
2026-09-22 21:06:34 -07:00
7 changed files with 424 additions and 41 deletions
+35 -3
View File
@@ -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.
+35 -3
View File
@@ -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.
+93 -17
View File
@@ -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
+59
View File
@@ -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(<fixture id>,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/*`).
+15 -4
View File
@@ -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"
}
+40 -10
View File
@@ -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).
+147 -4
View File
@@ -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 ]