From 45a5c8b9e5345c3889096227ebc9a185ee930bed Mon Sep 17 00:00:00 2001 From: Edgar Arakelyan Date: Wed, 21 Oct 2026 12:41:29 -0700 Subject: [PATCH] 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 --- .../agent-environments/state-writes/spec.md | 8 +- .../state-writes/verification.md | 7 + .../EnvironmentStateWriteSimulation.test.ts | 175 ++++++++++++------ .../EnvironmentStateWriteSimulation.ts | 35 ++-- 4 files changed, 146 insertions(+), 79 deletions(-) diff --git a/docs/specs/agent-environments/state-writes/spec.md b/docs/specs/agent-environments/state-writes/spec.md index a72298e4ca..83046f89f0 100644 --- a/docs/specs/agent-environments/state-writes/spec.md +++ b/docs/specs/agent-environments/state-writes/spec.md @@ -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. diff --git a/docs/specs/agent-environments/state-writes/verification.md b/docs/specs/agent-environments/state-writes/verification.md index ffe4761abb..ecf8f3bd8f 100644 --- a/docs/specs/agent-environments/state-writes/verification.md +++ b/docs/specs/agent-environments/state-writes/verification.md @@ -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. diff --git a/src/domain/analysisView/EnvironmentStateWriteSimulation.test.ts b/src/domain/analysisView/EnvironmentStateWriteSimulation.test.ts index 8bd05a7dad..e7f9f44570 100644 --- a/src/domain/analysisView/EnvironmentStateWriteSimulation.test.ts +++ b/src/domain/analysisView/EnvironmentStateWriteSimulation.test.ts @@ -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, 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 }); diff --git a/src/domain/analysisView/EnvironmentStateWriteSimulation.ts b/src/domain/analysisView/EnvironmentStateWriteSimulation.ts index 4d247ddcc6..dd40f859ce 100644 --- a/src/domain/analysisView/EnvironmentStateWriteSimulation.ts +++ b/src/domain/analysisView/EnvironmentStateWriteSimulation.ts @@ -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, record: StateRecordFacts, + only: ReadonlySet, ): 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. */