improvise/context/test-evidence/protocol.md

Test evidence — improvise-protocol

What each test's bug was, what fault it can see, and why it can fail. Keyed by exact test name (design-principles §7). A renamed test orphans its entry; python3 scripts/check-comment-runs.py --check-evidence catches that.

Tests whose name already states the whole property are not listed here. An entry earns its place by carrying something the assertion cannot: the bug, the injected fault, or the reason a negative arm exists.

---

src/render.rs — the fold

cell_updates_outside_the_cache_are_dropped

A projection naming a cell outside the current viewport must be dropped, not panic: frames and cell updates race on the wire, and a client that crashes on a stale index is a client that crashes. This is the totality half of the WidgetCache contract, stated as an example; the ordering half is a_cell_update_that_overtakes_its_labels_is_lost.

a_cell_update_that_overtakes_its_labels_is_lost

The fold is not commutative, and a client must not be written as though it were. The frames frame the cells, so a Cells update that overtakes the ColFrame/RowFrame naming its positions is dropped. Reordering the identical three updates gives a different cache, and the assert_ne! is the load-bearing line — without it, a fold where order did not matter would pass.

a_compacted_seed_folds_to_the_same_cache_as_the_whole_history

Bootstrap is not a second code path, but a server does not replay history to a late client either — it sends the state it holds now. So the property is compaction: folding the seed lands exactly where folding the whole history landed, including the history's relabels and overwrites.

The history is built to be worth compacting — overwritten, relabelled, populated and grown, with the extent moving twice so only the last survives — and seed.len() < history.len() is asserted, because a "seed" that is not smaller than the history is not a compaction and the equality would be vacuous.

Note the general rule this is an instance of: asserting fold(prefix) + fold(rest) == fold(whole) is vacuous, being the definition of a left fold (doctrine(fold_tests_must_test_order_not_the_axiom)).

a_snapshot_seeds_every_widget_from_its_compacted_state

The same property across the envelope, with two subscribers each folding only what is addressed to it — the dispatch a client does for real.

a_totals_update_that_overtakes_its_columns_is_cut_to_fit

The totals strip is framed by the columns on the same terms the cells are: a strip that overtakes the ColFrame naming its positions is cut down, because a renderer zips it with the columns and a length mismatch indexes off the end.

an_empty_totals_strip_is_not_padded_into_blanks

An empty strip says "this grid has no totals" — records mode, or an empty grid — and must not be padded into a row of blanks by the re-fit. Padding it would draw an empty total row under a records-mode grid that has none, which is the one thing the emptiness is for. This is the asymmetry that separates totals from cells and col_widths, which are always padded.

a_recategorized_axis_blanks_the_totals_too

The totals are contents, not frame: a reframing blanks them for the same reason it blanks the cells. A stale sum under fresh cells is the one number on the screen a user would take at face value. The length assertion is the other half — the frame survives, the numbers do not.

Renamed by improvise-n89z, which deleted GridUpdate::Invalidated. The test used to reach the blanking through that arm; it now reaches it through a cats change, which is the thing that really produces it. Proved discriminating by pinning recategorized to false.

a_relabelled_row_is_blanked_and_the_frame_survives

The other half of the same deletion. invalidation_blanks_contents_but_keeps_ the_frame asserted what the retired arm did; this asserts what invalidate_relabelled does, and it is strictly stronger, because the old arm blanked everything and so could not tell "blanks what it reframes" from "blanks the lot". Row 1's label does not change and row 1 keeps its value. Proved discriminating by weakening the stale filter from || to &&.

the_page_bar_outlives_a_reshape

page_coords is framed by nothing: it names categories, not positions. So it survives a reshape that drops every row and column. Without this, "re-fit everything on a frame update" would look correct.

the_first_rendered_entry_always_shows_its_level

Bug (improvise-jjx), moved here with the rule (improvise-anr9): header suppression compared against the entry at idx - 1 even when that entry was scrolled off-screen, so scrolling blanked the group label at the top of the viewport. The first rendered entry always shows its full tuple.

The fixture is two-level so the level-0 prefix of index 1 genuinely matches index 0's — a single-level frame could not express the case.

a_repeated_prefix_below_the_first_rendered_entry_is_suppressed

The negative arm of the above, and it has to stay: without it, "always show every level" would pass the_first_rendered_entry_always_shows_its_level and the multi-level header would repeat its outer label on every row.

a_data_index_skips_group_headers_and_still_names_its_group

Group headers do not consume a data index, and a data index resolves to the group whose header precedes it — which is what makes a column group span drawable by a client that holds no GridLayout. The collapse state travelling with the group is the third assertion, and it is why FrameGroup::collapsed is on the wire rather than re-derived.

shared_ancestry_widens_as_the_level_rises

The underline rule: at the leaf level only the selected column, at a higher level every column under the same ancestor. Both levels are checked because a version comparing whole tuples would pass the leaf arm and light only one column at the outer level, and a version comparing only the outermost label would pass the outer arm and light a sibling at the leaf.

body_from_starts_at_the_item_not_at_the_header_above_it

A window opening mid-group must be able to name its group without painting that group's header as a row inside the window. The second assertion — body_from(0) is everything, headers included — is what stops the fix being "drop all group headers".

header_widths_are_per_level_and_measured_in_display_cells

The one width rule (improvise-1125): per level, the widest label plus a gap, clamped. Measured in display cells, so 日本 counts four and not two — a chars().count() would make level 1 two cells wide, clamp it to MIN_ROW_HEADER_W, and draw the header short. Both clamps are exercised ("ab" is under the floor, "x" * 100 over the ceiling), because a rule whose clamps are never reached is a rule nobody has tested.

a_column_without_its_width_yet_is_measured_in_display_cells

Raised by Copilot on PR #23. The fallback width a column is drawn at between its ColFrame and its ColWidths must be in the same unit the authoritative widths are in. chars().count() would draw a wide label half as wide as it needs. The fixture is deliberately a two-scalar / four-cell string, which is the smallest input that separates the two counts.

an_axis_with_no_categories_still_has_one_level

An axis carrying no category still draws one header line, and its item tuples are empty — reading a level off one must answer "" rather than panic. This is the shape a view with nothing on Row produces, so it is a live layout and not a degenerate fixture.

a_relabelled_column_does_not_keep_the_old_columns_value

A column dropped from the middle used to slide the cells to its right one place left, because fit_to_labels truncates by position: [A,B,C] shrinking to [A,C] left the column now labelled C showing B's value. Nothing on the wire ever forced a producer to declare it first, so apply blanks what it reframes.

a_label_change_blanks_only_the_positions_it_reframes

The same rule on the row axis, and the case a bare label shrink gets right by accident: only the relabelled positions are blanked, so an unchanged row keeps what the server already sent for it.

renaming_a_row_category_invalidates_every_cell_under_it

Renaming the category re-identifies every cell on the axis, even where every label is byte-identical: a coordinate is cats zipped with the item tuple, so Region = [North] and Department = [North] are different cells wearing the same name.

Frame-only, and that word is the test. No Cells and no Totals follow the frame update, because the producer's follow-up is exactly what would hide the bug — apply has to be right with nothing behind it, the same shape as a_cell_update_that_overtakes_its_labels_is_lost.

The id assertion is the sharp half and is separate from the text on purpose. A stale CellId::Record under a re-identified coordinate is an editable cell whose write addresses the record the old coordinate named — silent, invisible in any rendering, and the same family of defect as gotcha 18's drill snapshot.

The precondition assertion (the items are identical) is load-bearing: without it the test is just the ordinary relabelling case, and cats proves nothing.

renaming_a_column_category_invalidates_every_cell_under_it

The column half of the same rule. Here the per-position arm already blanks each total as its column goes stale, so this pins the cells and the ids; the row arm above is the one that needed the totals handled separately.

an_unchanged_category_leaves_the_cells_that_still_fit

The negative arm, and it is load-bearing: without it, "blank everything on every frame update" would pass both renaming tests above, and the fold would resend the whole grid after a group collapse.

a_relabelled_column_drops_its_total

improvise-hkt6. invalidate_relabelled blanked the cells under a renamed column and left its total standing, so a client that heard ColFrame without a Totals behind it drew the old column's sum under the new column's blanks.

Unreachable from grid_updates, which always sends the changed totals in the same batch — which is the point: the rule is that apply does not trust a producer to remember, and the only way to test it is to send the update the producer never sends alone.

Three columns and a rename in the middle, so "blanked the right one" is separable from "blanked all of them".

a_relabelled_row_leaves_the_totals_alone

The row half is the negative arm and has to stay: a total spans every row, so no single row frames it. Without this, "blank the totals on any relabel" would pass a_relabelled_column_drops_its_total.

col_widths_always_span_the_column_labels

col_widths is framed by the columns: a renderer zips the two, so a cache where they disagree in length is one that indexes off the end. ColWidths is its own update and may be a frame behind the frames.

a_col_widths_update_is_fitted_to_the_labels_it_is_framed_by

The same invariant seen from the other arm. ColWidths used to be assigned verbatim, so a widths update that disagreed with the frame put the cache straight back into the state col_widths_always_span_the_column_labels exists to forbid — the frame arm was fitted and the widths arm was not.

A short update is the ordinary case: the server resized a column the client has not been told about yet. A long one means the widths overtook the ColFrame that frames them, and the fold drops what overtakes its frame — the same rule Cells is already held to. Both directions are asserted, because fitting only one of them is exactly the bug.

item_updates_touch_only_the_named_category

Plus the dropped-update arm at the end: an Items update for a category the cache has never heard of is dropped, not inserted — the totality rule again, on a different widget.

an_axes_update_moves_several_categories_at_once

A transpose moves two axes at once, which is why Axes takes a list rather than a single pair. The third assertion — membership is undisturbed — is what stops the fix being "resend the whole category list".

every_projection_round_trips_through_json

One populated value per CellDisplay shape: numeric decides the alignment and error the styling, so a round trip that only ever carries them at their default proves nothing about either (doctrine(populate_before_roundtrip)).

a_populated_snapshot_round_trips_through_json

The Snapshot is the only thing on the wire that is not an event, and the only point at which ViewState is serialized (improvise-q08) — so it is the one message whose round trip nothing else covers. Populated on both halves: a default ViewState beside an empty seed would round-trip through almost no code.

---

src/basis.rs

a_client_that_has_folded_nothing_cannot_claim_a_basis

The floor. A client that has been told nothing cannot compose a basis, so it cannot compose a write. Basis has no Default and no public constructor, so BasisCache::claim is the only door — which is what this asserts is shut before the server has published anything.

an_unknown_record_is_omitted_rather_than_guessed

A record the client has never been told about is left out, not invented. Defaulting it to zero would be a claim the client cannot support, and the server would read it as "untouched" — the exact forged-basis case Rejection::RecordUnstated exists to catch.

a_claim_carries_the_counter_for_each_record_it_names

The second assertion is the one that earns its place: a claim naming one record must not carry another's counter. A claim that returned the whole cache would pass the first assertion and fail this.

the_published_record_list_is_stable_under_traversal_order

The published list is deduplicated and ordered, so a client is not sent a fresh basis every time a row moves on screen. Two maps built in opposite insertion order must compare equal — which is the property the BTreeMap parameter buys and a Vec would not.

---

src/frame.rs

the_retired_spellings_do_not_parse

The names the deleted envelopes used, which must not resurrect as serde aliases: an envelope accepting two spellings of one variant is two homes again, wearing one type.

Not a hypothetical rename — Bootstrap and Command are exactly what the worker pair (improvise-wasm-client::wire) spelled these two payloads before improvise-xks6. ClientFrame::Command joined the list with improvise-bpq2, and it is the sharper of the two: the singleton spelling was this crate's own until that commit, so an alias would be a revival rather than a resurrection, and the payload shapes differ only by a pair of brackets — {"Command":{...}} against {"Commands":[{...}]} — which is exactly the difference a permissive alias would paper over.

The injected-fault discipline is the part to keep (doctrine(check_the_checker)): the mutated input is asserted well-formed JSON first, and the failure is asserted to be about the name — serde's unknown variant — not merely that an error occurred. A rewrite that also breaks the JSON makes this pass against an enum that really does have the variant.

---

src/reduce.rs

a_model_command_leaves_the_view_slice_untouched

A model command is the document's business, not this client's. Folding one into the view slice would be a client writing state it does not own — the document's answer comes back as projections. The cursor is set to a non-default value first, so "the whole state is still default" cannot stand in for "the state did not move".

folding_the_same_stream_twice_gives_the_same_state

Both ends fold the same commands, so the same stream must produce the same state — otherwise the server's mirror drifts from the client it is mirroring (improvise-m91). A Projection is included in the stream, to pin that it passes through reduce_view untouched rather than being a case it handles.

every_command_round_trips_through_json

One populated value per payload family (doctrine(populate_before_roundtrip)), not per variant: the exhaustive walk over the 26 ModelCommand variants is every_model_command in improvise-command, where the effect each one names can also be checked.

The modelled() helper composes its basis through a seeded BasisCache rather than building a Basis literal — not because this test is about the basis, but because that is the only constructor there is, and a test that needed a second one would be evidence the door had been left open.

cursor_commands_land_in_the_active_views_entry

The second assertion is the point: the view we switched away from never gained an entry. An implementation writing a single cursor and copying it per view would pass the first assertion.

switching_views_restores_each_cursor

The point of keying the cursor map: switching back restores where you were, and the client can do that without a Workbook.

help_pages_stop_at_both_ends_and_set_clamps

Both bounds and the clamp, because going back from page 0 is the one that underflows if written as help_page - 1, and Set out of range is the one that panics if written as an index.

It used to be named ..._wrap_in_both_directions_... and asserted wrapping, which was a second derivation of the effects it came from and disagreed with them: effect::HelpPageNext clamps at the last page and HelpPagePrev saturates at zero, while this arm wrapped modulo HELP_PAGE_COUNT. Nothing compared the two, because no client had ever sent Command::HelpPage — the help overlay's h/l were still upstream keys. improvise-e24v made them a client's, and walking_off_the_end_of_the_help_pages_agrees_with_the_host failed on the first press past the end (client 0, host 4). The wire was changed to match the effect rather than the other way round: the effect is what ships in the TUI, and changing that is a product decision nobody asked for. Whether wrapping is wanted on both ends is filed separately.

---

src/lib.rs

the_wire_types_need_nothing_but_core_and_serde

improvise-cqi AC 2: this crate crosses a process boundary, so it must not drag a terminal backend with it. A cargo tree check would be external; this is the part the compiler can hold — the types here resolve with only improvise-core and serde in scope, and adding a ratatui or crossterm dependency would have to be written into Cargo.toml deliberately rather than arriving through a use. The CI wasm job is the other half: a crate pulling in crossterm would stop building for wasm32.

---

src/viewmodel.rs

expanding_an_absent_category_is_harmless

An expanded name the cache does not carry must not shift the flattening: expanded_cats is per-client and survives a document swap, so it routinely names categories that are gone. A flattening that indexed by expanded-name would go off the end here.

only_quit_advertises_nothing

improvise-2hi, carried over from only_quit_has_no_hint when the hints moved out of AppMode (improvise-k099). The old hint_text had a _ => "" arm, so the modes without hints were invisible; ExportPrompt was blank too (improvise-1c9), and the status bar went empty at the one moment the user has to be told what to type. Only Quit may say nothing — it is never rendered.

What it asserts now is one step stronger, because hint_line is derived: a mode goes quiet not by someone forgetting a string but by every command it advertises becoming unbound, which every_advertised_hint_names_a_binding_that_exists catches first.

every_advertised_hint_names_a_binding_that_exists

The replacement for every_hint_key_resolves_in_its_mode (improvise-2hi), which is deleted, and the deletion is the point (doctrine(a_consolidation_that_keeps_its_compatibility_test_is_unfinished)).

That test existed because AppMode::hint_text was a hand-written string promising what the keys do, with nothing tying it to the keymaps. It walked every Key:verb token in every hint through a 60-line tokenizer that had to know the hint dialect — named keys, Ctrl-<c>, F/C/V alternatives, runs like hjkl, the em-dash prose tail, CommandMode's ex-commands — and panicked on a token it could not classify, because a token it skipped was exactly the one that would go unchecked.

None of that is needed now. A hint names a command, and its keys are looked up in Keymaps::default_keymaps(), so "the hint names a key that resolves" is true by construction and cannot be otherwise. What remains checkable, and is what this test checks, is the other direction: a mode advertising a command that nothing binds. That was never checkable before.

Note what neither version reaches, and gotcha 14 stated for the old one: that the caption is accurate. i:edit where i enters records mode still passes. The caption is English beside a command name, and only a reader can judge it.

the_retired_invalidated_spelling_does_not_parse

improvise-n89z deleted GridUpdate::Invalidated, and the one way it can come back without anyone noticing is as a serde alias — a wire spelling that parses and that nothing produces, which is the state the deletion was for.

It keeps the discipline the_retired_spellings_do_not_parse earned in frame.rs: assert the mutated input is still well-formed first (a ColWidths projection of the same shape parses), and assert the error kind — serde's unknown variant — rather than merely that an error occurred, because a rewrite that also broke the JSON would make the check pass against an enum that really did have the variant.

Proved discriminating by re-adding the variant with an empty apply arm: the retired spelling parses again and the test fails on expect_err.

a_chord_is_recognised_by_its_modifiers_and_not_by_its_label

help::compact dropped a chorded key from a status-bar hint by testing whether the formatted label started with "Ctrl-" or "Alt-" — parsing a string it had just formatted. Finding 3 of the adversarial review of PR #50, filed as improvise-thpe and deliberately not fixed there: the reviewer enumerated every format_key_label output and none begins with either, so there was no false positive. The defect was the shape.

The regression guard is the signature, as it is for Checked (gotcha 43): compact now takes &[(KeyCode, KeyModifiers)], so the string it used to parse is not in scope to parse. keys_for returns the pairs and Hint::keys carries them; help.rs formats last, through Hint::labels and the one spelling in keymap::key_label. Keymap::labels_for — the "throw the modifiers away into a string" step the ticket names — has no caller left and is deleted, because a consolidation that keeps its old path keeps the defect available (doctrine(a_consolidation_that_keeps_its_compatibility_test_is_unfinished)).

The rule also got wider, and that is the part a test can state: a chord is any modifier beyond shift, which is total over the bitset, where the string test enumerated two prefixes. Shift alone is not a chord — it is how a key is named rather than how it is held, which S-Tab is the case for.

Injected fault, run rather than argued. A KeyModifiers::SUPER bit and a key_label arm spelling it Super-x were added temporarily. The old filter keeps it — ["T", "Super-x"], two survivors where one is wanted — while compact returns "T". That is the ticket's own reproduction, executed, and it is the only way to see the difference: with KeyModifiers as shipped, every chord's label does begin with Ctrl- or Alt-, so no permanent test can separate the two rules. Both the bit and the probe were removed afterwards.

One behaviour that had to be preserved deliberately: keys_for used to dedup labels, and deduping the pairs instead would let two patterns that spell the same key both reach the status bar. It now dedups by label explicitly.

The binding dump is byte-identical across this change (4406 lines, diff clean), which is what doctrine(binding_dump_diff) asks of anything touching the keymap: the dump's prefix rows go through Hint, so they had to be checked rather than assumed.