kb: a write cannot disarm its own gate, and cannot silently lose another's
Second review pass on PR #68. All three findings real; the first two reproduced by injection before fixing. The candidate is validated by CONSULTING it, so the thing being checked got to influence the check. Three ways through, all demonstrated: - `:- halt(0).` as a delta -- fixed last round by refusing directives - REMOVING kb_consistent: it then throws existence_error, and tpl exits 0 when a goal throws before reaching halt, so the gate passed by not existing. The error was printed and the tool still reported success. - REPLACING it with the fact `kb_consistent.`, which passes forever after. CHECK_GOAL now catches, so a throw exits non-zero, and writes touching the gate predicates are refused unless KB_ALLOW_GATE makes it deliberate. That list is hand-maintained and a new gate predicate is unprotected until named -- stated rather than hidden. Writes were read/validate/mv with nothing in between, so two agents -- ordinary here, waves run in parallel -- would both read the same file, both validate, and the later mv would discard the earlier addition. The lost-update class this tool exists to remove, reintroduced in the tool. Closed by stamping content at read time and refusing to commit if it moved, plus an mkdir lock. The stamp is the part that matters; the lock only makes the collision rare. AGENTS.md's top-level instruction still said to save facts through the MCP. The wave section had been fixed; the authoritative line had not. kb-test.sh is 17 cases. The race is deterministic via KB_TEST_RACE. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FC2jVn8Au7E9JPkw6bwXXH
This commit is contained in:
Edward Langley
+55
-6
@@ -29,8 +29,44 @@ merge() { tpl -q "$MERGE" -g "$MERGE_GOAL" -- "$@"; }
|
||||
|
||||
# kb_consistent is the gate CI runs. Anything that writes runs it on the
|
||||
# CANDIDATE, before the candidate becomes the knowledge base.
|
||||
# The goal reaches a halt on EVERY path, for the same reason MERGE_GOAL does: a
|
||||
# goal that throws never reaches the halt beside it and tpl exits 0. Without the
|
||||
# catch, a write that REMOVED kb_consistent made the gate pass by not existing.
|
||||
CHECK_GOAL="(catch(kb_consistent,E,(write(user_error,E),nl(user_error),halt(2))) -> halt(0) ; (kb_report, halt(1)))"
|
||||
check_file() {
|
||||
tpl "$1" -g "(kb_consistent -> halt(0) ; (kb_report, halt(1)))" 2>/dev/null
|
||||
tpl "$1" -g "$CHECK_GOAL" 2>/dev/null
|
||||
}
|
||||
|
||||
# A content stamp of the knowledge base as it was READ. Two agents running this
|
||||
# concurrently would otherwise both read the same file, both validate, and the
|
||||
# later mv would discard the earlier addition -- the lost-update class this tool
|
||||
# exists to avoid, and waves here run agents in parallel.
|
||||
stamp_of() {
|
||||
if command -v sha256sum >/dev/null 2>&1; then sha256sum "$1" | cut -d' ' -f1
|
||||
elif command -v shasum >/dev/null 2>&1; then shasum -a 256 "$1" | cut -d' ' -f1
|
||||
else cksum "$1" | tr -d ' '
|
||||
fi
|
||||
}
|
||||
|
||||
# mkdir is atomic everywhere; flock is absent on macOS. The lock makes a
|
||||
# collision rare, the stamp makes one that happens anyway LOUD rather than silent.
|
||||
acquire_lock() {
|
||||
local tries=0
|
||||
until mkdir "$KB.lock" 2>/dev/null; do
|
||||
tries=$((tries + 1))
|
||||
if [ "$tries" -ge 300 ]; then
|
||||
echo "kb: could not acquire $KB.lock after 30s; remove it if stale" >&2
|
||||
exit 1
|
||||
fi
|
||||
sleep 0.1
|
||||
done
|
||||
trap 'rmdir "$KB.lock" 2>/dev/null || true' EXIT
|
||||
}
|
||||
|
||||
# Test seam: simulate another writer landing between the read and the commit.
|
||||
race_hook() {
|
||||
[ -n "${KB_TEST_RACE:-}" ] || return 0
|
||||
cp -f "$KB_TEST_RACE" "$KB"
|
||||
}
|
||||
|
||||
usage() {
|
||||
@@ -51,8 +87,15 @@ EOF
|
||||
exit 2
|
||||
}
|
||||
|
||||
commit() { # $1 = candidate file
|
||||
local cand="$1"
|
||||
commit() { # $1 = candidate file, $2 = stamp of the kb before it was read
|
||||
local cand="$1" was="${2:-}"
|
||||
race_hook
|
||||
if [ -n "$was" ] && [ "$(stamp_of "$KB")" != "$was" ]; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB changed while this write was being prepared." >&2
|
||||
echo "kb: another writer won; re-run and your delta applies on top." >&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
|
||||
@@ -76,6 +119,8 @@ case "$cmd" in
|
||||
tpl "$KB" -g "($1 -> halt(0) ; (write('false'), nl, halt(1)))" 2>/dev/null
|
||||
;;
|
||||
fmt)
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
: > "${cand}.delta"
|
||||
if ! merge add "$KB" "${cand}.delta" "$cand" >/dev/null 2>&1; then
|
||||
@@ -84,29 +129,33 @@ case "$cmd" in
|
||||
exit 1
|
||||
fi
|
||||
rm -f "${cand}.delta"
|
||||
commit "$cand"
|
||||
commit "$cand" "$was"
|
||||
echo "kb: canonicalized"
|
||||
;;
|
||||
rm)
|
||||
[ $# -eq 1 ] || usage
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
if ! merge remove "$KB" "$1" "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
commit "$cand"
|
||||
commit "$cand" "$was"
|
||||
echo "kb: $KB updated"
|
||||
;;
|
||||
add|replace)
|
||||
[ $# -eq 1 ] || usage
|
||||
acquire_lock
|
||||
was="$(stamp_of "$KB")"
|
||||
cand="$(mktemp)"
|
||||
if ! merge "$cmd" "$KB" "$1" "$cand"; then
|
||||
rm -f "$cand"
|
||||
echo "kb: REFUSED -- $KB is unchanged" >&2
|
||||
exit 1
|
||||
fi
|
||||
commit "$cand"
|
||||
commit "$cand" "$was"
|
||||
echo "kb: $KB updated"
|
||||
;;
|
||||
*) usage ;;
|
||||
|
||||
@@ -70,6 +70,29 @@ bad_shape(T, 'a query') :-
|
||||
nonvar(T), T = (?- _), !.
|
||||
bad_shape(T, 'not a clause') :-
|
||||
clause_head(T, H), \+ callable(H).
|
||||
bad_shape(T, 'part of the gate that validates this write') :-
|
||||
\+ gate_writes_allowed,
|
||||
clause_pred(T, P),
|
||||
gate_predicate(P).
|
||||
|
||||
% Removing kb_consistent made the check pass by not existing; REPLACING it with
|
||||
% a fact that is trivially true passes forever after. A write that can disarm
|
||||
% its own validation is refused unless KB_ALLOW_GATE says otherwise, which makes
|
||||
% an intentional change to the checker a deliberate, greppable act.
|
||||
% Hand-maintained, and that is its weakness: a new gate predicate is unprotected
|
||||
% until it is named here.
|
||||
gate_predicate(kb_consistent/0).
|
||||
gate_predicate(kb_report/0).
|
||||
gate_predicate(kb_error/1).
|
||||
gate_predicate(functional/1).
|
||||
gate_predicate(kb_sentinel/1).
|
||||
gate_predicate(known_crate/1).
|
||||
gate_predicate(kb_external_check/1).
|
||||
|
||||
gate_writes_allowed :-
|
||||
catch(getenv('KB_ALLOW_GATE', V), _, fail),
|
||||
V \== '',
|
||||
V \== '0'.
|
||||
|
||||
clause_head((H :- _), H) :- !.
|
||||
clause_head(H, H).
|
||||
|
||||
@@ -143,6 +143,54 @@ else
|
||||
bad "add refused a self-duplicate but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4f. The gate can be REMOVED. kb_consistent then throws existence_error, and
|
||||
# tpl exits 0 when a goal throws before reaching halt -- so the check passes
|
||||
# by not existing and the unchecked candidate is committed.
|
||||
fresh
|
||||
printf 'kb_consistent.\n' > "$work/killgate.pl"
|
||||
if kb rm "$work/killgate.pl" >/dev/null 2>&1; then
|
||||
bad "rm removed the gate that validates the write"
|
||||
elif unchanged; then
|
||||
ok "rm refuses to remove the validating gate"
|
||||
else
|
||||
bad "rm refused to remove the gate but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4g. And REPLACED with something trivially true, which passes forever after.
|
||||
fresh
|
||||
if kb replace "$work/killgate.pl" >/dev/null 2>&1; then
|
||||
bad "replace made the gate trivially true"
|
||||
elif unchanged; then
|
||||
ok "replace refuses to disarm the validating gate"
|
||||
else
|
||||
bad "replace refused to disarm the gate but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
# 4h. An intentional change to the gate is still possible, deliberately.
|
||||
fresh
|
||||
if KB_ALLOW_GATE=1 kb replace "$work/killgate.pl" >/dev/null 2>&1; then
|
||||
ok "KB_ALLOW_GATE lets a deliberate gate change through"
|
||||
else
|
||||
bad "KB_ALLOW_GATE did not allow a gate change"
|
||||
fi
|
||||
|
||||
# 4i. Two writers reading the same file would both validate, and the later mv
|
||||
# would silently discard the earlier addition. The stamp makes the loser
|
||||
# loud. KB_TEST_RACE simulates the other writer landing mid-flight.
|
||||
fresh
|
||||
cp "$work/kb.pl" "$work/other.pl"
|
||||
printf "doctrine(written_by_the_other_writer,'x').\n" >> "$work/other.pl"
|
||||
cat > "$work/mine.pl" <<'EOD'
|
||||
doctrine(written_by_me,'y').
|
||||
EOD
|
||||
if KB_TEST_RACE="$work/other.pl" kb add "$work/mine.pl" >/dev/null 2>&1; then
|
||||
bad "a concurrent write was silently discarded"
|
||||
elif grep -q written_by_the_other_writer "$work/kb.pl" && ! grep -q written_by_me "$work/kb.pl"; then
|
||||
ok "a concurrent write is refused, and the other writer's addition survives"
|
||||
else
|
||||
bad "the race was refused but the kb is not the other writer's file"
|
||||
fi
|
||||
|
||||
echo "kb-test: the happy paths"
|
||||
|
||||
# 5. A genuinely new clause lands, and the count moves by exactly one.
|
||||
|
||||
Reference in New Issue
Block a user