fix(environment): count interference on any target a read covers, and contradict a failed item read's other writes

Greptile raised these on the list-queries branch against this branch's interference rule.
- An unmodelled write counts against a tool when it followed the tool's call on any entity or collection the read covers, so a later call on another entity no longer hides it.
- A failed item read contradicts the writes no unmodelled write followed, and checks only the others on the members they sent, so an envelope it cannot reproduce no longer confirms a rename.

The verdicts over the 50 captures are unchanged plan by plan, and the smoke applies all 31 served write tools.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
Edgar ArakelyanandClaude Opus 5.5 committed 2026-10-21 12:41:29 -07:00
1 parent 7cef2fb2b6
commit 45a5c8b9e5
4 files changed
+146 -79

No files matched your search

@@ -241,10 +241,10 @@ refuses to answer with.
an update's changes confirms nothing of it, and leaves it for a later check
of that entity or collection.
- A mismatch contradicts each exercised write that no unmodelled write came
after its latest call on the read's entity or collection, whatever earlier
write is still pending. When an unmodelled write
followed some of them, an item read checks those only on the members they
sent and a list is not checked again: such a write may explain the rest.
after its latest call on any of the read's entities or collections, whatever
earlier write is still pending. An item read checks the writes an unmodelled
write did follow only on the members they sent, and a list with such a write
is not checked again: the unmodelled write may explain the rest.
- A mismatch on an entity or collection that no write changed contradicts,
as `side-effect`, the modelled writes since that previous check whose paths
are segment-prefix related to the read's path.
@@ -350,3 +350,10 @@ list-lines and list-queries branches:
Each new test fails on the previous head. The verdicts over the 50 captures are unchanged plan by plan, the smoke
applies all 31 served write tools, and the gates passed again.
A seventeenth round settled two more findings Greptile raised on the list-queries branch against this branch's
interference rule: an unmodelled write counts against a tool when it followed the tool's call on any target the read
covers, so a later call on another entity does not hide it; and a failed item read contradicts the writes no
unmodelled write followed, checking only the others on their members. Both tests fail on the previous head. The
verdicts over the 50 captures are unchanged plan by plan, the smoke applies all 31 served write tools, and the gates
passed again.
@@ -1012,63 +1012,6 @@ describe("what a write's effect keeps", () => {
});
});
it("weighs an unmodelled write against a tool's call on the entity a read checks, not its latest call elsewhere", () => {
const tagged = (id: number, name: string, tag: string) => ({
id,
name,
tag,
});
const rows: TimedCaptureRow[] = [
["GET", "/api/books", [tagged(1, "A", "x"), tagged(2, "B", "x")]],
["GET", "/api/books/1", tagged(1, "A", "x")],
["GET", "/api/books/2", tagged(2, "B", "x")],
["PATCH", "/api/books/1", tagged(1, "A2", "x"), 200, { name: "A2" }],
["POST", "/api/exports", { queued: true }, 202, { format: "csv" }],
["PATCH", "/api/books/2", tagged(2, "B2", "x"), 200, { name: "B2" }],
// The export came after book 1's rename, so it may explain the changed tag; the rename itself shows.
["GET", "/api/books/1", tagged(1, "A2", "y")],
];
expect(gated(rows, "patch_books_by_id")).toMatchObject({
served: true,
contradicted_by: null,
checked_record_ordinals: [6],
});
});
it("contradicts a write made after an unmodelled one, though an earlier pending write came before it", () => {
const summary = (name: string) => [
{ id: 1, name },
{ id: 2, name: "B" },
];
const full = (name: string, description: string) => ({
id: 1,
name,
description,
});
const rows: TimedCaptureRow[] = [
["GET", "/api/books", summary("A")],
["GET", "/api/books/1", full("A", "x")],
["GET", "/api/books/2", { id: 2, name: "B", description: "y" }],
["PATCH", "/api/books/1", full("A", "new"), 200, { description: "new" }],
["GET", "/api/books", summary("A")],
["POST", "/api/exports", { queued: true }, 202, { format: "csv" }],
[
"PUT",
"/api/books/1",
full("Z", "new"),
200,
{ name: "Z", description: "new" },
],
["GET", "/api/books/1", full("Z", "new")],
// The export came before the rename, so it cannot explain the list showing the old name.
["GET", "/api/books", summary("A")],
];
expect(gated(rows, "put_books_by_id")).toMatchObject({
served: false,
contradicted_by: 8,
});
});
const subtitled = (id: number, name: string, subtitle?: string) =>
subtitle === undefined ? { id, name } : { id, name, subtitle };
const summaries = (first: string): TimedCaptureRow => [
@@ -1107,6 +1050,124 @@ describe("what a write's effect keeps", () => {
});
});
describe("what an unmodelled write explains", () => {
it("weighs an unmodelled write against a tool's call on the entity a read checks, not its latest call elsewhere", () => {
const tagged = (id: number, name: string, tag: string) => ({
id,
name,
tag,
});
const rows: TimedCaptureRow[] = [
["GET", "/api/books", [tagged(1, "A", "x"), tagged(2, "B", "x")]],
["GET", "/api/books/1", tagged(1, "A", "x")],
["GET", "/api/books/2", tagged(2, "B", "x")],
["PATCH", "/api/books/1", tagged(1, "A2", "x"), 200, { name: "A2" }],
["POST", "/api/exports", { queued: true }, 202, { format: "csv" }],
["PATCH", "/api/books/2", tagged(2, "B2", "x"), 200, { name: "B2" }],
// The export came after book 1's rename, so it may explain the changed tag; the rename itself shows.
["GET", "/api/books/1", tagged(1, "A2", "y")],
];
expect(gated(rows, "patch_books_by_id")).toMatchObject({
served: true,
contradicted_by: null,
checked_record_ordinals: [6],
});
});
it("lets an unmodelled write explain a list's change to an entity a tool made before it, whatever the tool did after", () => {
const fourth = book(4, "Fourth Book", bookClock(5));
const rows: TimedCaptureRow[] = [
["GET", "/api/books", [FIRST_BOOK, SECOND_BOOK]],
["GET", "/api/books/1", FIRST_BOOK],
["GET", "/api/books/2", SECOND_BOOK],
["POST", "/api/books", THIRD_BOOK, 201, { name: "Third Book" }],
["POST", "/api/exports", { queued: true }, 202, { format: "csv" }],
["POST", "/api/books", fourth, 201, { name: "Fourth Book" }],
["GET", "/api/books/4", fourth],
// The export came after the third book was made, so it may explain the third book's other name.
[
"GET",
"/api/books",
[FIRST_BOOK, SECOND_BOOK, { ...THIRD_BOOK, name: "Retitled" }, fourth],
],
];
expect(gated(rows, "post_books")).toMatchObject({
served: true,
contradicted_by: null,
});
});
it("contradicts by a failed item read the writes no unmodelled write came after, checking only the others' members", () => {
const enveloped = (data: Record<string, JsonValue>, revision: string) => ({
data,
revision,
});
const full = (name: string, description: string) => ({
id: 1,
name,
description,
});
const summary = [
{ id: 1, name: "A" },
{ id: 2, name: "B" },
];
const rows: TimedCaptureRow[] = [
["GET", "/api/books", summary],
["GET", "/api/books/1", enveloped(full("A", "x"), "r1")],
[
"GET",
"/api/books/2",
enveloped({ id: 2, name: "B", description: "y" }, "r1"),
],
["PATCH", "/api/books/1", full("A", "new"), 200, { description: "new" }],
["GET", "/api/books", summary],
["POST", "/api/exports", { queued: true }, 202, { format: "csv" }],
// The rename sends the name alone, so the earlier description patch stays pending.
["PUT", "/api/books/1", full("Z", "new"), 200, { name: "Z" }],
// The rename shows, but the envelope serving would answer with does not.
["GET", "/api/books/1", enveloped(full("Z", "new"), "r2")],
];
expect(gated(rows, "put_books_by_id")).toMatchObject({
served: false,
contradicted_by: 7,
});
});
it("contradicts a write made after an unmodelled one, though an earlier pending write came before it", () => {
const summary = (name: string) => [
{ id: 1, name },
{ id: 2, name: "B" },
];
const full = (name: string, description: string) => ({
id: 1,
name,
description,
});
const rows: TimedCaptureRow[] = [
["GET", "/api/books", summary("A")],
["GET", "/api/books/1", full("A", "x")],
["GET", "/api/books/2", { id: 2, name: "B", description: "y" }],
["PATCH", "/api/books/1", full("A", "new"), 200, { description: "new" }],
["GET", "/api/books", summary("A")],
["POST", "/api/exports", { queued: true }, 202, { format: "csv" }],
[
"PUT",
"/api/books/1",
full("Z", "new"),
200,
{ name: "Z", description: "new" },
],
["GET", "/api/books/1", full("Z", "new")],
// The export came before the rename, so it cannot explain the list showing the old name.
["GET", "/api/books", summary("A")],
];
expect(gated(rows, "put_books_by_id")).toMatchObject({
served: false,
contradicted_by: 8,
});
});
});
describe("what later calls must keep consistent", () => {
it("refuses an update one call sends an ignored id with and another the path's id", () => {
const renamed = (at: Book, name: string) => ({ ...at, name });
@@ -168,12 +168,8 @@ export class EnvironmentStateWriteSimulation {
io: this.#input.io,
records: this.#input.records,
timed: this.#input.timed,
viewOf: (ordinal) => {
const tool = this.#toolOf.get(ordinal);
return tool === undefined
? undefined
: this.#input.views.get(tool.name);
},
viewOf: (ordinal) =>
this.#input.views.get(this.#toolOf.get(ordinal)?.name ?? ""),
idField: (type) => this.#types.get(type)!.id_field,
observed: (ordinal) =>
this.#observations.set(
@@ -368,16 +364,16 @@ export class EnvironmentStateWriteSimulation {
? this.#confirm(view, record, keys, exercised)
: undefined;
if (!pass) {
const interfered = [...exercised].filter((name) =>
this.#interferedWith(name, keys),
const interfered = new Set(
[...exercised].filter((name) => this.#interferedWith(name, keys)),
);
if (interfered.length === 0)
if (interfered.size === 0)
this.#mismatch({ record, index, keys, exercised, view });
// An unmodelled write after some of these writes may explain the difference: those are checked on their own members only.
else if (view.shape === "item") this.#checkMembers(view, record);
else {
// An unmodelled write after some of these writes may explain the difference: those are checked on their own members only.
this.#contradictOthers(keys, exercised, record);
for (const key of keys) this.#taint.fail(key);
if (view.shape === "item") this.#checkMembers(view, record, interfered);
else for (const key of keys) this.#taint.fail(key);
}
if (view.shape === "item") this.#adopt(view, record);
}
@@ -427,24 +423,27 @@ export class EnvironmentStateWriteSimulation {
this.#unmodelledAt.push(index);
}
/** Whether a write the gate does not model came after a tool's latest modelled call on these targets, so it may explain what a read shows of it. */
/** Whether a write the gate does not model came after a tool's latest call on one of these targets, so it may explain what a read shows there. */
#interferedWith(tool: string, keys: readonly string[]): boolean {
const last = Math.max(
...keys.map((key) => this.#touchedSince.get(key)?.at.get(tool) ?? -1),
);
return this.#unmodelledAt.some((index) => index > last);
return keys.some((key) => {
const at = this.#touchedSince.get(key)?.at.get(tool);
return at !== undefined && this.#unmodelledAt.some((index) => index > at);
});
}
/** Check the writes to an item read's entity on the members they sent, as a resynchronising read does. */
#checkMembers(
view: Extract<StateView, { shape: "item" }>,
record: StateRecordFacts,
only: ReadonlySet<string>,
): void {
const { collection, id } = itemTarget(this.#state, view.type, record);
const entity = this.#state.entity(view.type, collection, id);
if (entity === undefined) return;
const target = entityTarget(entity.type, entity.collection, entity.id);
this.#checkFields(view, record, entity, this.#touched.get(target));
const writes = [...(this.#touched.get(target) ?? [])];
const checked = new Map(writes.filter(([name]) => only.has(name)));
this.#checkFields(view, record, entity, checked);
}
/** Check the writes to an entity on the fields each wrote against an item read; the read's object, when it shows one. */