kb: design against the model before implementing, and fix the key rule it exposed
AGENTS.md has always said Prolog is a design tool for reasoning about tickets; it was the least-used line in the file, because kb.pl was only ever written retrospectively. `kb check --with <design.pl>` merges proposed facts into a throwaway candidate and runs kb_consistent over the union, so a design can be refused before any code exists. Nothing is written either way. The model already derives rather than records -- illegal_dependency, may_use, depends_transitively, portable, snapshot_safe, view_state_admits, record_obligation, and eleven kb_error classes. Three proposals exercised it in one sitting: one added dependency edge produced SIX layering violations through the transitive closure; a proposal to declare decision/3 functional was refused, correctly, because improvise-907 carries two decisions; and a mis-ordered layer/2 argument was named rather than accepted. Trying to model a design found a real defect in the tool. Keys were the functor plus all arguments but the last, which is right for doctrine(Name,Text) and wrong for any RELATION: crate_depends_on(A,B) keyed on A, so a crate depending on two crates read as one key twice and was unaddable. It cannot be read off the KB's functional/1 -- that keys an arity-3 predicate on its first argument, right for crate/3 and wrong for decision/3 -- so key_arity/2 is a table, and anything unlisted keys on the whole head, which is the safe direction. kb-test.sh is 20 cases. 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
@@ -10,6 +10,7 @@ the only thing that writes it.** `tpl` is assumed on `PATH` from the dev shell.
|
||||
|
||||
```
|
||||
scripts/kb check # kb_consistent, exactly what CI runs
|
||||
scripts/kb check --with <d.pl># does the model accept a design you have not built?
|
||||
scripts/kb count # clauses per keyed predicate
|
||||
scripts/kb query '<goal>' # run a goal; exit 1 if it fails
|
||||
scripts/kb add <delta.pl> # add clauses; refuses if a key already exists
|
||||
@@ -25,6 +26,32 @@ with the last argument left as `_`:
|
||||
doctrine(a_name_that_went_false,_).
|
||||
```
|
||||
|
||||
## Designing against the model
|
||||
|
||||
Before implementing a ticket, state the design as facts and ask whether the
|
||||
model accepts it:
|
||||
|
||||
```prolog
|
||||
crate(improvise_report,'crates/improvise-report','render a View as a report').
|
||||
crate_depends_on(improvise_report,improvise_core).
|
||||
layer(report,improvise_report).
|
||||
```
|
||||
|
||||
`scripts/kb check --with design.pl` merges those into a throwaway candidate and
|
||||
runs `kb_consistent` over the union. Nothing is written either way.
|
||||
|
||||
It derives consequences you would not enumerate: one wrong dependency edge
|
||||
returns six `layering_inverted` violations through the transitive closure. It
|
||||
also catches schema mistakes — `layer/2` is `(layer, crate)`, and the wrong
|
||||
order comes back as `layer_names_unknown_crate` rather than being accepted.
|
||||
|
||||
What the model can refuse today: layering and dependency direction
|
||||
(`illegal_dependency`, `layering_inverted`, `may_use`), `ViewState` membership
|
||||
(`portable`, `snapshot_safe`, `view_state_admits`, `field_misplaced_in_view_state`),
|
||||
record obligations, and functional-key conflicts. A design touching those areas
|
||||
is worth stating; one that touches none of them will be accepted vacuously, so
|
||||
extend the model rather than trusting the green.
|
||||
|
||||
## Rules
|
||||
|
||||
**Write a fact when you learn it.** There is no reason to batch.
|
||||
|
||||
@@ -216,6 +216,8 @@ doctrine(documentation_is_operational_and_history_lives_in_the_kb,'User ruling 2
|
||||
doctrine(an_agent_posting_to_github_says_so,'User instruction 2026-09-20: anything an agent posts to GitHub goes out under the repository owner account, so every PR comment, review and issue body opens with a line naming the model and that it is an agent posting in his session. A PR body 🤖 Generated with Claude Code footer already does this; comments carry nothing unless it is added, and an unattributed comment reads as the owner own words to every reader -- including reviewers deciding how much weight to give it. The same applies to anything else published outward under his identity.').
|
||||
doctrine(a_write_must_not_be_able_to_disarm_its_own_gate,'scripts/kb validates a candidate by CONSULTING it and running kb_consistent, so the thing being checked gets to influence the check. Three ways that was exploitable, each demonstrated on PR #68 before it was closed: a delta of \`:- halt(0).\` -- a directive is callable, so a callable test lets it through -- exited the check with success before kb_consistent ran; REMOVING kb_consistent made it throw existence_error, and tpl exits 0 when a goal throws before reaching halt, so the gate passed by not existing; and REPLACING it with the fact kb_consistent. passes forever after. Fixes: refuse directives and queries by shape, catch in the validation goal so a throw exits non-zero, and refuse writes touching the gate predicates unless KB_ALLOW_GATE makes it deliberate. The general form: when a checker consults its own input, ask what the input can do to the checker, not only what the checker says about the input. The gate predicate list is hand-maintained, which is its residual weakness -- a new one is unprotected until named.').
|
||||
doctrine(a_read_validate_write_sequence_is_a_lost_update,'scripts/kb read the knowledge base, merged, validated and moved the result into place, with nothing between the read and the move. Two agents doing that concurrently -- which is ordinary here, waves run agents in parallel -- both read the same file, both validate, and the later move silently discards the earlier addition. Exactly the class this tool was built to remove, reintroduced one level up in the tool itself. Closed by stamping the file content at read time and refusing to commit if it changed, plus an mkdir lock (flock is absent on macOS) so the collision is rare rather than merely loud. The stamp is the part that matters: a lock prevents the common case, a compare-and-swap is what makes an uncommon one impossible to lose silently.').
|
||||
doctrine(design_against_the_model_before_implementing,'AGENTS.md has always said Prolog is a design tool for reasoning about tickets, and it was the least-used line in the file: kb.pl was written retrospectively. \`scripts/kb check --with <design.pl>\` closes that -- proposed facts are merged into a throwaway candidate and kb_consistent runs over the union, so a design can be refused before code exists. The model already DERIVES rather than merely records: illegal_dependency, may_use, depends_transitively, portable, snapshot_safe, view_state_admits, record_obligation, needs_runtime_check, and eleven kb_error classes including layering_inverted and field_misplaced_in_view_state. Demonstrated on three proposals in one sitting: one added edge (improvise_core depending on improvise_command) produced SIX derived layering violations through the transitive closure, which no author would have enumerated; a proposal to declare decision/3 functional was refused with conflicting_values naming improvise-907, correctly, because one ticket carries several decisions; and a mis-ordered layer/2 argument was named as layer_names_unknown_crate rather than silently accepted. What makes this worth doing rather than decorative is the same rule as everywhere else -- the model must be able to REFUSE, and you must watch it refuse. A design language nothing can reject is documentation with parentheses.').
|
||||
doctrine(a_key_rule_must_ask_whether_the_relation_is_multi_valued,'scripts/kb keyed every clause on the functor plus all arguments but the last, which is right for doctrine(Name,Text) and wrong for any RELATION: crate_depends_on(A,B) then keyed on A, so a crate depending on two crates read as one key twice and was unaddable. Found by trying to model a proposed crate, not by any test -- the tool had only ever been pointed at single-valued facts. The fix cannot read the KB own functional/1, because that check keys an arity-3 predicate on its FIRST argument, which is right for crate/3 and wrong for decision/3 where one ticket holds several decisions under different names. So key_arity/2 is a hand-maintained table and anything unlisted keys on the WHOLE head, which is the safe direction: an unlisted relation accepts many clauses and only an exact repeat is a duplicate.').
|
||||
work_done('improvise-8tk',bug_fix,'ZZ/:wq quit even when the save failed, silently discarding the model. Save now aborts the effect batch on failure; save_to_current_path/1 returns Result<String,String>; three tests in ui/effect.rs.').
|
||||
work_done('improvise-907',bug_fix,'Import wizard step machine redesign: validation_error() gate at ReviewProposals (no-category and over-limit), history-stack previous() bound to Left on every step, and Done made a real confirmation step holding the built workbook. Superseded improvise-gfq, improvise-o1c, improvise-c6j.').
|
||||
work_done('improvise-6sq',wont_do,'Merging EditOrDrill and EnterEditAtCursorCmd into one EnterEdit{mode} is not safe: they differ in WHEN the cell value is read, not in a mode parameter. Added ui/app.rs::tests::i_and_o_diverge_on_an_empty_records_grid as executable evidence.').
|
||||
|
||||
+17
-2
@@ -73,7 +73,7 @@ usage() {
|
||||
cat >&2 <<'EOF'
|
||||
usage: kb <command>
|
||||
|
||||
check run kb_consistent (what CI runs)
|
||||
check [--with <d.pl>] run kb_consistent, optionally over a proposed design
|
||||
count clauses per keyed predicate
|
||||
query '<goal>' run a goal against the knowledge base
|
||||
fmt rewrite in canonical form (idempotent)
|
||||
@@ -109,7 +109,22 @@ cmd="$1"; shift
|
||||
|
||||
case "$cmd" in
|
||||
check)
|
||||
if check_file "$KB"; then echo "kb_consistent: TRUE"; else exit 1; fi
|
||||
# `check --with <design.pl>` asks whether a design the tree does not yet
|
||||
# have is one the model accepts: the facts are merged into a throwaway
|
||||
# candidate -- which keeps each predicate contiguous -- and kb_consistent
|
||||
# runs over the union. Nothing is ever committed.
|
||||
if [ "${1:-}" = "--with" ]; then
|
||||
[ $# -eq 2 ] || usage
|
||||
cand="$(mktemp)"
|
||||
if ! merge replace "$KB" "$2" "$cand" >/dev/null; then
|
||||
rm -f "$cand"; echo "kb: the proposal is not well-formed" >&2; exit 1
|
||||
fi
|
||||
if check_file "$cand"; then
|
||||
rm -f "$cand"; echo "kb_consistent with $2: TRUE"
|
||||
else
|
||||
rm -f "$cand"; echo "kb: the model REFUSES this design (above)" >&2; exit 1
|
||||
fi
|
||||
elif check_file "$KB"; then echo "kb_consistent: TRUE"; else exit 1; fi
|
||||
;;
|
||||
count)
|
||||
merge count "$KB" 2>/dev/null
|
||||
|
||||
+53
-34
@@ -23,15 +23,16 @@ run(remove, KbFile, DeltaFile, OutFile) :-
|
||||
terms_of(KbFile, Old),
|
||||
terms_of(DeltaFile, Doomed),
|
||||
check_callable(Doomed),
|
||||
check_self_consistent(Doomed),
|
||||
absent(Old, Doomed, Missing),
|
||||
functional_preds(Old, Funcs),
|
||||
check_self_consistent(Funcs, Doomed),
|
||||
absent(Funcs, Old, Doomed, Missing),
|
||||
( Missing == []
|
||||
-> true
|
||||
; format("kb-merge: REFUSED -- no such clause to remove:~n", []),
|
||||
forall(member(K, Missing), format(" ~q~n", [K])),
|
||||
halt(2)
|
||||
),
|
||||
foldl_remove(Doomed, Old, Kept),
|
||||
foldl_remove(Funcs, Doomed, Old, Kept),
|
||||
write_terms(OutFile, Kept),
|
||||
verify(OutFile, Kept),
|
||||
length(Old, NO), length(Kept, NK),
|
||||
@@ -41,10 +42,11 @@ run(Mode, KbFile, DeltaFile, OutFile) :-
|
||||
terms_of(KbFile, Old),
|
||||
terms_of(DeltaFile, New),
|
||||
check_callable(New),
|
||||
check_self_consistent(New),
|
||||
conflicts(Old, New, Clashes),
|
||||
functional_preds(Old, Funcs),
|
||||
check_self_consistent(Funcs, New),
|
||||
conflicts(Funcs, Old, New, Clashes),
|
||||
gate(Mode, Clashes),
|
||||
foldl_merge(New, Mode, Old, Merged),
|
||||
foldl_merge(Funcs, New, Mode, Old, Merged),
|
||||
write_terms(OutFile, Merged),
|
||||
verify(OutFile, Merged),
|
||||
length(Old, NO), length(New, NN), length(Merged, NM),
|
||||
@@ -97,19 +99,36 @@ gate_writes_allowed :-
|
||||
clause_head((H :- _), H) :- !.
|
||||
clause_head(H, H).
|
||||
|
||||
% A clause key is the functor plus every argument but the last, so
|
||||
% doctrine(Name,_) keys on Name and decision(Id,Key,_) on the pair. Looser than
|
||||
% functional/1 for crate/3; kb_consistent is the backstop for that.
|
||||
clause_key((H :- _), K) :- !, head_key(H, K).
|
||||
clause_key(H, K) :- head_key(H, K).
|
||||
% Which leading arguments identify a clause. Anything not listed keys on the
|
||||
% WHOLE head, so a multi-valued relation -- a crate depends on several crates --
|
||||
% can hold many clauses and only an exact repeat is a duplicate.
|
||||
% This cannot be read off the KB's own functional/1: that check keys an arity-3
|
||||
% predicate on its FIRST argument, which is right for crate/3 and wrong for
|
||||
% decision/3, where one ticket carries several decisions under different names.
|
||||
% Hand-maintained, like gate_predicate/1, but the default is the safe direction.
|
||||
clause_key(Funcs, (H :- _), K) :- !, head_key(Funcs, H, K).
|
||||
clause_key(Funcs, H, K) :- head_key(Funcs, H, K).
|
||||
|
||||
head_key(H, K) :-
|
||||
H =.. [F|Args],
|
||||
( append(Front, [_], Args)
|
||||
key_arity(doctrine/2, 1).
|
||||
key_arity(invariant/2, 1).
|
||||
key_arity(decision/3, 2).
|
||||
key_arity(work_done/3, 2).
|
||||
key_arity(work_followup/3, 2).
|
||||
key_arity(crate/3, 1).
|
||||
key_arity(location/3, 2).
|
||||
key_arity(groom_check/2, 1).
|
||||
key_arity(kb_issue_found/2, 1).
|
||||
key_arity(wasm_runtime_hazard/3, 2).
|
||||
|
||||
head_key(_, H, K) :-
|
||||
functor(H, F, A),
|
||||
( key_arity(F/A, N), H =.. [F|Args], length(Front, N), append(Front, _, Args)
|
||||
-> K =.. [F|Front]
|
||||
; K = F
|
||||
; K = H
|
||||
).
|
||||
|
||||
functional_preds(_, []).
|
||||
|
||||
clause_pred((H :- _), F/A) :- !, functor(H, F, A).
|
||||
clause_pred(H, F/A) :- functor(H, F, A).
|
||||
|
||||
@@ -117,8 +136,8 @@ clause_pred(H, F/A) :- functor(H, F, A).
|
||||
% previously-unused key clashed with nothing and the merge silently dropped the
|
||||
% first -- add discarding part of its own payload, visible only as a delta count
|
||||
% that did not match the clauses added.
|
||||
check_self_consistent(New) :-
|
||||
findall(K, ( member(T, New), clause_key(T, K) ), Ks),
|
||||
check_self_consistent(Funcs, New) :-
|
||||
findall(K, ( member(T, New), clause_key(Funcs, T, K) ), Ks),
|
||||
msort(Ks, Sorted),
|
||||
adjacent_dups(Sorted, Dups0),
|
||||
sort(Dups0, Dups),
|
||||
@@ -138,10 +157,10 @@ adjacent_dups([A, B|T], Out) :-
|
||||
),
|
||||
adjacent_dups([B|T], Rest).
|
||||
|
||||
conflicts(Old, New, Clashes) :-
|
||||
conflicts(Funcs, Old, New, Clashes) :-
|
||||
findall(K,
|
||||
( member(T, New), clause_key(T, K),
|
||||
member(O, Old), clause_key(O, K) ),
|
||||
( member(T, New), clause_key(Funcs, T, K),
|
||||
member(O, Old), clause_key(Funcs, O, K) ),
|
||||
Clashes).
|
||||
|
||||
gate(add, []) :- !.
|
||||
@@ -153,29 +172,29 @@ gate(add, Clashes) :-
|
||||
gate(replace, _).
|
||||
gate(M, _) :- die(M).
|
||||
|
||||
foldl_merge([], _, Acc, Acc).
|
||||
foldl_merge([T|Ts], Mode, Acc0, Acc) :-
|
||||
clause_key(T, K),
|
||||
exclude(has_key(K), Acc0, Acc1),
|
||||
foldl_merge(_, [], _, Acc, Acc).
|
||||
foldl_merge(Funcs, [T|Ts], Mode, Acc0, Acc) :-
|
||||
clause_key(Funcs, T, K),
|
||||
exclude(has_key(Funcs, K), Acc0, Acc1),
|
||||
clause_pred(T, P),
|
||||
insert_after_last(Acc1, P, T, Acc2),
|
||||
foldl_merge(Ts, Mode, Acc2, Acc).
|
||||
foldl_merge(Funcs, Ts, Mode, Acc2, Acc).
|
||||
|
||||
has_key(K, T) :- clause_key(T, K).
|
||||
has_key(Funcs, K, T) :- clause_key(Funcs, T, K).
|
||||
|
||||
% A remove that matches nothing is refused rather than silently doing nothing:
|
||||
% a typo'd key would otherwise report success and leave the clause in place.
|
||||
absent(Old, Doomed, Missing) :-
|
||||
absent(Funcs, Old, Doomed, Missing) :-
|
||||
findall(K,
|
||||
( member(T, Doomed), clause_key(T, K),
|
||||
\+ ( member(O, Old), clause_key(O, K) ) ),
|
||||
( member(T, Doomed), clause_key(Funcs, T, K),
|
||||
\+ ( member(O, Old), clause_key(Funcs, O, K) ) ),
|
||||
Missing).
|
||||
|
||||
foldl_remove([], Acc, Acc).
|
||||
foldl_remove([T|Ts], Acc0, Acc) :-
|
||||
clause_key(T, K),
|
||||
exclude(has_key(K), Acc0, Acc1),
|
||||
foldl_remove(Ts, Acc1, Acc).
|
||||
foldl_remove(_, [], Acc, Acc).
|
||||
foldl_remove(Funcs, [T|Ts], Acc0, Acc) :-
|
||||
clause_key(Funcs, T, K),
|
||||
exclude(has_key(Funcs, K), Acc0, Acc1),
|
||||
foldl_remove(Funcs, Ts, Acc1, Acc).
|
||||
|
||||
% Keeps each predicate a contiguous block: a new clause lands after the last
|
||||
% one of its own predicate, or at the end when the predicate is new.
|
||||
|
||||
@@ -191,6 +191,40 @@ else
|
||||
bad "the race was refused but the kb is not the other writer's file"
|
||||
fi
|
||||
|
||||
# 4j. A multi-valued relation must accept several clauses. The key rule keyed
|
||||
# on all-but-last, so a crate depending on two crates read as a duplicate
|
||||
# key and was unaddable -- found by trying to model a design, not by a test.
|
||||
fresh
|
||||
cat > "$work/multi.pl" <<'EOD'
|
||||
crate(improvise_probe,'crates/improvise-probe','a probe crate').
|
||||
crate_depends_on(improvise_probe,improvise_core).
|
||||
crate_depends_on(improvise_probe,improvise_protocol).
|
||||
layer(probe,improvise_probe).
|
||||
EOD
|
||||
if kb add "$work/multi.pl" >/dev/null 2>&1; then
|
||||
ok "a multi-valued relation accepts several clauses"
|
||||
else
|
||||
bad "add refused a legitimate multi-valued relation"
|
||||
fi
|
||||
|
||||
# 4k. check --with asks whether a design the tree does not have is one the model
|
||||
# accepts. It must be able to say BOTH, and must never write.
|
||||
fresh
|
||||
printf 'crate_depends_on(improvise_core,improvise_command).\n' > "$work/bad-design.pl"
|
||||
if kb check --with "$work/bad-design.pl" >/dev/null 2>&1; then
|
||||
bad "check --with accepted a design that inverts the layering"
|
||||
elif unchanged; then
|
||||
ok "check --with refuses an unsound design and writes nothing"
|
||||
else
|
||||
bad "check --with refused a design but MODIFIED the kb"
|
||||
fi
|
||||
|
||||
if kb check --with "$work/multi.pl" >/dev/null 2>&1 && unchanged; then
|
||||
ok "check --with accepts a sound design and writes nothing"
|
||||
else
|
||||
bad "check --with rejected a sound design, or wrote to the kb"
|
||||
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