Correct the determinism law's width-guard and analyzer claims (improvise-b9f2)
This commit is contained in:
+15
-6
@@ -3276,9 +3276,12 @@ yank, panels and cursor.
|
||||
against one `CmdContext`. Every `HashMap` it reached was the same instance with
|
||||
the same `RandomState`, so it iterated the same way both times: `f(x) == f(x)`,
|
||||
which nothing can fail. Separately built `App`s give every map its own seed. So a
|
||||
command whose effects follow hash iteration order disagrees with itself. That is
|
||||
the one kind of nondeterminism this repo has actually shipped (gotcha 18: the
|
||||
drill snapshot in hash order, the analyzer's `HashSet`). The companion test
|
||||
command whose effects follow hash iteration order disagrees with itself. Hash
|
||||
order is the one kind of nondeterminism this repo has actually shipped (gotcha
|
||||
18). This law can see it where a command's `execute` builds it, as the drill
|
||||
snapshot's record order was. It cannot see the other shipped instance, the
|
||||
analyzer's `HashSet`: `analyze_records` is reached only from inside
|
||||
`Effect::apply`, which is outside this law (see below). The companion test
|
||||
`only_distinct_instances_can_see_a_command_that_follows_hash_order` keeps that
|
||||
property checked: a test-only command that emits `ctx.buffers` in iteration
|
||||
order must agree with itself on one context and disagree across two.
|
||||
@@ -3304,9 +3307,15 @@ the whole slice of records under that item, not one record picked by name. In
|
||||
the demo that is four records and eight cells for each of the eight drills. The
|
||||
test
|
||||
also asserts that the widest candidate it actually passes matches at least four
|
||||
records. That guard reads the argument list the law uses, not a copy of it, so
|
||||
dropping the derived drills fails it, and so does a demo with too little data.
|
||||
With the store's sort removed, the law now fails 400 of 400 runs.
|
||||
records. That guard catches a demo with too little data, and it catches the
|
||||
derived drills being dropped from the argument list. It does **not** catch the
|
||||
comparison losing its wide drills some other way, because it measures what the
|
||||
argument lists match, not what the built commands ordered (improvise-b9f2). The
|
||||
review showed this with a rival: a `drill-into-cell` parser that refuses fewer
|
||||
than two arguments sends every one-coordinate drill to the one-record cursor
|
||||
fallback. The guard still reports four records, and with the store's sort
|
||||
removed the law passed 38 of 300 runs. With the store's sort removed and the
|
||||
parser intact, the law fails 400 of 400 runs.
|
||||
|
||||
**What it cannot see.** Only commands and arguments the fixture reaches. A
|
||||
command whose nondeterminism needs some other state, such as records mode, a
|
||||
|
||||
@@ -5375,9 +5375,14 @@ rivals it catches:
|
||||
still pin the store directly.
|
||||
- **The derived drills dropped from the argument list** (the
|
||||
`all.extend(one_coordinate_drills(model))` line commented out): the test
|
||||
fails before comparing anything, with "the widest drill orders 1 records". The
|
||||
width guard reads the same argument list the comparison uses, so it cannot
|
||||
pass while the comparison has lost its wide drills.
|
||||
fails before comparing anything, with "the widest drill orders 1 records".
|
||||
That is the only way of losing the wide drills the guard can see. It measures
|
||||
what the argument lists match, not what the built commands ordered, so it can
|
||||
pass while the comparison has lost its wide drills (improvise-b9f2). Review
|
||||
rival: `drill-into-cell`'s parser changed to refuse fewer than two arguments,
|
||||
which sends every one-coordinate drill to the one-record cursor fallback. The
|
||||
guard stays silent and, with gotcha 18 re-injected, the law passed 38 of 300
|
||||
runs.
|
||||
- **A stale exemption**: `("quit", "stale")` listed in `OUTSIDE_THE_CONTEXT`.
|
||||
It fails as "listed … but did not".
|
||||
|
||||
|
||||
Reference in New Issue
Block a user