docs(protocol): land the crate's reasoning as context/ prose
The arguments in improvise-protocol's comments, relocated before the comments are capped: the fold rules, the basis tiers, the one-envelope-pair derivation, the TextEntry spine, and the four accessors that must not enter a draw loop. Test narratives go to context/test-evidence/protocol.md, keyed by test name per design-principles §7. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
Edward Langley
@@ -0,0 +1,388 @@
|
||||
# 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.
|
||||
|
||||
### invalidation_blanks_the_totals_too
|
||||
|
||||
The totals are **contents, not frame**: `Invalidated` 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.
|
||||
|
||||
### 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 forced a producer to send an `Invalidated` 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.
|
||||
|
||||
`GridUpdate::Invalidated` is payload-free and so proves least about the
|
||||
envelope; it is present but does not stand in for the rest.
|
||||
|
||||
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_wrap_in_both_directions_and_set_clamps
|
||||
|
||||
Both wrap directions and the clamp, because the backwards wrap 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.
|
||||
|
||||
---
|
||||
|
||||
## `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.
|
||||
Reference in New Issue
Block a user