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
This commit is contained in:
Edward Langley
+40
-10
@@ -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).
|
||||
|
||||
@@ -611,5 +611,97 @@ else
|
||||
ok "a write killed before its rename leaves the old kb byte-identical"
|
||||
fi
|
||||
|
||||
echo "kb-test: what the ledger and the key comparison can be fooled by"
|
||||
|
||||
# 23. Keys compared as a SET cannot see one of two clauses sharing a key
|
||||
# (improvise-ih3k). work_done/3 keys on (id, kind) and is not functional/1,
|
||||
# so a git merge can commit two clauses under one key. Dropping one then
|
||||
# leaves the key present and the loss unseen. The baseline carries the pair.
|
||||
awk -v a="work_done('improvise-zzzz',bug_fix,'first fix, merged from branch A')." \
|
||||
-v b="work_done('improvise-zzzz',bug_fix,'review fix, merged from branch B')." '
|
||||
{ line[NR] = $0 } /^work_done\(/ { last = NR }
|
||||
END { for (i = 1; i <= NR; i++) { print line[i]; if (i == last) { print a; print b } } }
|
||||
' "$KB" > "$work/pair-base.pl"
|
||||
grep -v "^work_done('improvise-zzzz',bug_fix,'review fix" "$work/pair-base.pl" > "$work/pair-lost.pl"
|
||||
pkb() { KB_FILE="$work/kb.pl" KB_BASELINE="$work/pair-base.pl" "$here/kb" "$@"; }
|
||||
fresh
|
||||
if ! KB_FILE="$work/pair-base.pl" "$here/kb" check >/dev/null 2>&1; then
|
||||
bad "the paired baseline fails kb_consistent -- case 23 proves nothing"
|
||||
elif [ "$(grep -c "^work_done('improvise-zzzz'" "$work/pair-lost.pl")" -ne 1 ]; then
|
||||
bad "the lossy fixture does not hold exactly one of the pair -- case 23 proves nothing"
|
||||
else
|
||||
cp "$work/pair-lost.pl" "$work/kb.pl"
|
||||
if pkb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "add wrote onto a kb that lost one of two clauses sharing a key"
|
||||
elif ! cmp -s "$work/kb.pl" "$work/pair-lost.pl"; then
|
||||
bad "the lost twin was refused but the kb was MODIFIED"
|
||||
elif said "$work/out" "review fix, merged from branch B"; then
|
||||
ok "losing one of two clauses under one key is refused, naming the one lost"
|
||||
else
|
||||
bad "the lost twin was refused, but the refusal does not name it"
|
||||
fi
|
||||
# The pair itself is not a loss: an add onto the intact pair must land, or
|
||||
# the guard has turned "HEAD holds a duplicate" into "nothing may be written".
|
||||
cp "$work/pair-base.pl" "$work/kb.pl"
|
||||
if pkb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
ok "an add onto a kb that still holds both clauses of a pair is accepted"
|
||||
else
|
||||
bad "the intact pair was refused: $(tail -1 "$work/out")"
|
||||
fi
|
||||
# And the pair has a way out through the tool: rm the key (both go, recorded),
|
||||
# add back the survivor, and a later write must still land.
|
||||
printf "work_done('improvise-zzzz',bug_fix,_).\n" > "$work/pair-key.pl"
|
||||
printf "work_done('improvise-zzzz',bug_fix,'the fix, both halves').\n" > "$work/pair-one.pl"
|
||||
printf "doctrine(a_probe_after_the_pair_is_resolved,'x').\n" > "$work/after-pair.pl"
|
||||
if ! pkb rm "$work/pair-key.pl" >"$work/out" 2>&1; then
|
||||
bad "rm of a key HEAD holds twice was refused: $(tail -1 "$work/out")"
|
||||
elif ! pkb add "$work/pair-one.pl" >"$work/out" 2>&1; then
|
||||
bad "re-adding one clause for a removed pair was refused: $(tail -1 "$work/out")"
|
||||
elif ! pkb add "$work/after-pair.pl" >"$work/out" 2>&1; then
|
||||
bad "a write after resolving the pair was refused: $(tail -1 "$work/out")"
|
||||
else
|
||||
ok "a pair is resolved by rm then add, and later writes still land"
|
||||
fi
|
||||
fi
|
||||
|
||||
# 24. A ledger entry excuses only the kb it was recorded against
|
||||
# (improvise-yea8). rm X, then restore kb.pl the way the refusal message
|
||||
# recommends -- not a write, so nothing prunes -- then lose X some other
|
||||
# way. The ledger entry from the abandoned rm must not excuse that loss.
|
||||
fresh
|
||||
printf "location(cli_args,'src/main.rs',_).\n" > "$work/drop-x.pl"
|
||||
grep -v "^location(cli_args," "$KB" > "$work/lost-x.pl"
|
||||
if ! kb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
||||
bad "rm of a clause HEAD has was refused -- case 24 proves nothing"
|
||||
elif [ ! -s "$work/kb.pl.removed" ]; then
|
||||
bad "rm left no ledger -- case 24 proves nothing"
|
||||
else
|
||||
cp "$work/lost-x.pl" "$work/kb.pl"
|
||||
if kb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "a ledger entry from an abandoned rm excused a later loss of that clause"
|
||||
elif ! cmp -s "$work/kb.pl" "$work/lost-x.pl"; then
|
||||
bad "the stale excuse was refused but the kb was MODIFIED"
|
||||
elif said "$work/out" "location(cli_args,'src/main.rs',clap)"; then
|
||||
ok "a ledger entry does not outlive the kb its rm produced"
|
||||
else
|
||||
bad "the loss was refused, but not by naming the lost clause"
|
||||
fi
|
||||
fi
|
||||
|
||||
# 24b. ...and still excuses it across the tool's own writes: the stamp moves
|
||||
# with each write, so rm then add then add must all land. A ledger stamped
|
||||
# only by rm passes 24 and refuses the second add here.
|
||||
fresh
|
||||
printf "doctrine(a_second_probe_after_the_rm,'x').\n" > "$work/new3.pl"
|
||||
if ! kb rm "$work/drop-x.pl" >"$work/out" 2>&1; then
|
||||
bad "rm refused -- case 24b proves nothing"
|
||||
elif ! kb add "$work/new.pl" >"$work/out" 2>&1; then
|
||||
bad "the first add after an rm was refused: $(tail -1 "$work/out")"
|
||||
elif ! kb add "$work/new3.pl" >"$work/out" 2>&1; then
|
||||
bad "the second add after an rm was refused: the ledger did not follow the write"
|
||||
else
|
||||
ok "a recorded rm stays excused across the tool's later writes"
|
||||
fi
|
||||
|
||||
printf '\nkb-test: %d passed, %d failed\n' "$pass" "$fail"
|
||||
[ "$fail" -eq 0 ]
|
||||
|
||||
Reference in New Issue
Block a user