docs(kb): what adversarial review found, and four vacuity shapes

From PRs #143/#146/#147/#150/#152/#156/#157 and the adversarial review of the
first five.

The finding worth the review's cost: `Repr::Nonfinite(&'a str)` could only be
produced by a deserializer that borrows from its input, so the new wire
spelling round-tripped through `from_str` and `from_slice` and nothing else —
the same JSON document escaped as `inf` was refused, and `to_value` did
not round-trip its own output. Both of the PR's tests used `from_str`, which
is precisely the one path that borrows.

Four vacuity shapes, each confirmed by injection rather than argued:

- A disjunctive assertion can accept the bug it guards — one branch here was
  exactly the error message the defect produces.
- A law asserted over an immutable `CmdContext` is a tautology: a `Cmd` is
  pure over its context by construction, so `execute` twice without applying
  effects asserts `f(x) == f(x)` and no rival can fail it. Applying the
  effects REFUTED this one rather than rescuing it.
- A rival must fail the property, not the setup — `AddFormula` and
  `RemoveItem` are both `CellData`, so the obvious test proved the neighbour.
- Every agent appends to the same evidence file at EOF: four conflicts in ten
  PRs. Loud, but the resolution is the hazard, since `--check-evidence` cannot
  see a dropped entry.

kb_consistent: TRUE, 803 facts.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FC2jVn8Au7E9JPkw6bwXXH

prolog-sessions/kb.pl

@@ -375,6 +375,10 @@ doctrine(a_type_name_is_not_a_field,'An assertion naming a field-carrying effect
 doctrine(a_clean_text_merge_can_delete_an_evidence_entry_that_no_gate_checks,'Two agents appending disjoint sections to context/test-evidence/*.md at the same point conflict, and the resolution LOOKS right whichever side is dropped. --check-evidence CANNOT CATCH IT: it asserts every heading names a running test and that no test is named twice, never that every entry SURVIVED. So a resolution must be verified line-by-line against BOTH parents -- every non-marker line of :2 and :3 present in the result -- and not eyeballed. Same family as a-clean-merge-can-delete-your-tests, one level up: there the loss was a test, here it is the recorded reason the test exists, and a lost reason is invisible forever because nothing regenerates it.').
 doctrine(an_additive_gate_read_through_tail_is_not_a_gate,'scripts/check-comment-runs.py --check-evidence is ADDITIVE since improvise-ijql -- every invocation that can exit 0 also answers the comment cap -- and it prints TWO lines, the cap FIRST and the evidence summary second. So reading it through tail -1 keeps the half you added the flag for and silently drops the half that was always there. Measured: an agent ran it that way, its local run HAD already found a three-line comment, and CI caught it instead. The general shape is worse than this one instance: a gate that grows a second responsibility keeps the same command line, so every pipeline written against the old single-line output degrades SILENTLY into checking less. Never pipe a gate through head or tail, and when adding an output line to a checker, consider that callers may be filtering.').
 doctrine(a_compound_command_refused_by_the_shell_guard_runs_none_of_its_parts,'In a worktree-isolated agent the shell guard refuses a whole compound command, so \"cp -f <restore> && cat >> <evidence>\" ran NEITHER part -- leaving an injected rival in the working tree, which was then carried through a git merge autostash into a branch. The full suite caught it at 1713 passed / 1 failed. Two things follow. A refusal is not a partial execution and must not be read as one, so re-check the state a refused command was meant to produce rather than assuming the first half landed. And this is the concrete argument for running EVERY gate after EVERY change rather than once after the last one: the window between injecting a rival and reverting it is exactly where a refused restore hides.').
+doctrine(a_disjunctive_assertion_can_accept_the_bug_it_guards,'a_string_that_is_not_one_of_the_three_tokens_is_refused asserted contains(\"Infinity\") || contains(\"data did not match\") -- and the SECOND DISJUNCT IS EXACTLY THE MESSAGE THE BUG PRODUCES, so the test passed both in the world where the refusal names what it saw and in the world where untagged silently swallowed it. An || in an assertion is a place to look: each branch must be a form of SUCCESS, never a form of the failure being guarded against. Writing one because you are unsure which message appears is the tell -- run it and find out, then assert that one.').
+doctrine(a_law_asserted_over_an_immutable_context_is_a_tautology,'law_toggle_group_involution called execute twice against the SAME immutable CmdContext, so it asserted f(x)==f(x) and NO RIVAL OF ANY KIND could fail it -- not merely the one the ticket named. Vacuous twice over, since the fixture had no groups and both sides were the empty string. A Cmd is pure over its context BY CONSTRUCTION (design-principles section 1), so any property stated by calling one twice without applying the effects between is restating that purity. Worse, applying the effects here REFUTED the law rather than rescuing it: collapsing removes the group data rows, so the cursor then names the NEIGHBOUR. Applying the effects is the minimum for such a test to say anything, and it may reveal the law is false.').
+doctrine(a_rival_must_fail_the_property_not_the_setup,'When a test setup shares a classification with the thing under test, a rival takes down the SETUP and the red proves the neighbouring question. improvise-en4s: AddFormula and RemoveItem are BOTH EffectKind::Model(CellData), so tightening the CellData arm meant the formula never reached the client and the test failed at \"the client must be holding the formula before it can lose it\" rather than at the deletion property. Fix: move the setup off the shared path -- seed the formula BEFORE Sessions::connect, so it arrives in the bootstrap seed, which no Dirty gates. Check WHERE a rival makes a test fail, not merely THAT it does.').
+doctrine(every_agent_appends_to_the_same_evidence_file_at_eof,'Four evidence-file conflicts in one batch of ten PRs -- command.md twice, gp.md, core.md -- because context/test-evidence/<area>.md is append-at-EOF and every agent touching an area lands there. They are LOUD conflicts and get noticed; the hazard is the RESOLUTION, since --check-evidence cannot see a dropped entry (it checks that every heading names a running test, and that a test CITING the file has an entry -- a test that cites nothing loses its entry silently). So resolve by keeping both sides and VERIFY LINE-BY-LINE against :2 and :3 rather than reading the merged text. Expect this conflict rather than treating each instance as bad luck; it is structural.').
 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.').
@@ -529,6 +533,7 @@ decision('improvise-gd28',browser_drill_blocked_by_surrogate_scope_not_layer_2,'
 decision('improvise-rr8n',keep_the_table_derived_from_what_it_describes,'The ticket asked to rewrite the tile-bar hint literal and SUPPRESS the derived status line in TileSelect. The implementing agent did the opposite and the orchestrator ACCEPTED it: the derived status line is a STRICT SUPERSET of the literal (Space, h/l, Tab appear only there) and cannot go stale, so suppressing it would delete information and keep the table that had just rotted. Verified before accepting -- the literal read \"Ctrl+arrows to move tiles\" while those keys are bound to enter-tile-select, so it was already false. Both tile-bar literals deleted; Normal derived line already says T:tiles. The import wizard keeps the ticket ORIGINAL answer, and the asymmetry is the point: ITS status line is derived from the MODE keymap while the real keys are per-step inside HandleWizardKey, so there the derived table is the one that lies. RULE: keep whichever table is derived from the thing it describes. COROLLARY: every_hint_key_resolves_in_its_mode CANNOT SEE A STRING LITERAL IN A WIDGET, the same blind spot improvise-wk18 names for help.rs, so a hand-written key literal is invisible to every hint guard in the repo.').
 decision('improvise-t14d',an_affordance_outranks_a_decoration,'draw.rs::fill_line takes a Keeps parameter rather than a global rule, because the three rows sharing a composed line genuinely disagree about which side yields. The title bar keeps the RIGHT -- the ?:help/:q escape hatch outranks an unbounded document name -- while minibuffer_line and draw_status keep the LEFT, which is what they already did, since right-priority there would let a long status message eat the text the user is editing. So the ticket \"give the right segment priority\" was correct ONLY for the title bar. Second fault, and the ticket framed it wrongly: padding by str::len mis-padded EVERY document including pure-ASCII ones, because the separator dot is in draw_title own format string at two bytes and one cell -- not a non-ASCII-NAME problem as filed. Widths now go through ui::text::truncate.').
 decision('improvise-6uva',a_registry_with_two_arms_demotes_the_weaker_caller,'CmdRegistry has three registration arms and NOTHING TYPE-CHECKS WHICH ARM A CALLER DESERVES. Three instances surfaced in one fix, and they do not point the same way, which is the part to carry. (1) The pure arm demoted every Move: parse built CursorState::default() so a script cursor reset instead of moving. (2) register_pure two arms DISAGREED WITH EACH OTHER -- interactive refused empty args, pure accepted them -- so \"w\" parsed one way and refused the other. (3) Found by ChatGPT Codex: the interactive arms of clear-cell/yank/paste/drill-into-cell took |_args, ctx| and DISCARDED EXPLICIT COORDINATES, so after the fix \"clear-cell Region/East\" cleared the origin. HERE THE WEAKER ARM WAS THE ONE THAT HAD THE CONTEXT, which is why \"always prefer the interactive arm\" is not the lesson. Make the arms agree, or make the difference the point; resolved for the cell-key commands by key_from_args_or_cursor -- explicit coordinates win, cursor is the fallback.').
+decision('improvise-55v2',a_borrowed_str_in_a_wire_adaptor_narrows_the_format,'Repr::Nonfinite(&\'a str) in an untagged serde adaptor can only be produced by a deserializer that BORROWS FROM ITS INPUT, so the spelling round-tripped through from_str and from_slice and through nothing else. Measured before fixing: {\"Number\":\"inf\"} parsed while {\"Number\":\"in\\u0066\"} -- THE SAME JSON DOCUMENT, since escaping is not a distinction JSON makes -- was refused, and to_value/from_value did not round-trip the adaptor own output. So the wire accepted a SUBSET of the encodings of the spelling it claimed to share with the .improv file. Cow<\'a, str> fixes all four paths and leaves the serialized form unchanged. THE TESTS COULD NOT SEE IT because both used from_str exclusively, which is precisely the one path that borrows -- a check adjacent to the question it names, arriving inside the change that DEFINES the question. Found by adversarial review, confirmed by injection.').
 wire_carries(command,both_directions,'user intent up, projection commands down').
 wire_carries(snapshot,on_connect_only,'improvise-q08: full ViewState + render cache filled from current viewport').
 wire_carries(command,both_directions,'user intent client->server, projections server->client').