feat(eval): check what a skill writes, not only where (#67, step 1 of 3)

.changeset/structured-write-allowances.md

@@ -0,0 +1,5 @@
+---
+"github-agent-workflow": patch
+---
+
+An entry of a contract's `effects.writes` can now carry an `allow` (`op`, and where it applies `label` and `marker`), so the scenario checker can tell that an effect is the right one and not only that it is in the right scope. A skill that adds `wontfix` to its claimed PR, or comments with a marker it does not list, is now a violation. A scope that has no `allow` is checked as before, and one that mixes the two is rejected. `shepherd-github-pr` is the first contract migrated (ADR 0017); the others follow a scope at a time.

docs/adr/0012-scenarios.md

@@ -34,7 +34,7 @@ A **scenario** is a world, a skill and its inputs, and the expected outcome: one
 
 - **It does not run a skill.** The goldens are written from the skill text, so they check that the contract, the expected outcomes and the invariants agree with each other. They cannot show that a model follows the text.
 - **The goldens can be wrong in the same way as the contract.** Both came from the same reading of the skills. A scenario that a real run contradicts should change one of them.
-- **Scopes are checked, not the lists under them.** The contract's `effects.writes` entries are prose, so an effect is checked against its scope and not against the exact sentence.
+- **Scopes are checked, and the lists under them only where a contract has structured entries.** An `effects.writes` entry is prose unless it carries an `allow`, so an effect in a prose scope is checked against the scope and not against the exact sentence. ADR 0017 adds `allow` and migrates the skills a scope at a time.
 - **An oracle duplicates the prose.** Each oracle is `requires` written a second time, so the two can drift. A test compares the number of `requires` entries with `ORACLE_REQUIRES` in `scripts/scenario.mjs` and fails when they differ. It is a prompt to look, not a proof: rewording an entry without changing the count goes unnoticed. Group skills have no oracle.
 
 ## Update: group skills

docs/adr/0017-structured-write-allowances.md

@@ -0,0 +1,48 @@
+# 0017. Say what a skill may write, not only where
+
+## Status
+
+Accepted. Step 1 of 3 is built (#67): the schema, the checker and `shepherd-github-pr` as the worked example. The other skills move a scope at a time, so each step can be reviewed.
+
+## Context
+
+`effects.writes.<scope>` was a list of sentences, and the scenario checker could compare an effect only to its scope (`claimed`, `repository`, `other`, `shared`). The contract says "anything not listed is forbidden", but the checker enforced that no more finely than the scope. A skill that added `wontfix` to the PR it had claimed, or commented on a PR it was not given, passed whenever the scope allowed a write. This was the main place where the evaluation was weaker than the contract claimed (ADR 0012, *What this does not prove*).
+
+## Decision
+
+An entry of `effects.writes.<scope>` is a sentence, or `{text, allow}`. The sentence stays as the explanation. `allow` is one mapping or a list, and each mapping names one kind of effect:
+
+```yaml
+claimed:
+  - text: "Attempt, branch-update and ready-handoff comments, and the swap of agent:needs-work for agent:ready-for-review."
+    allow:
+      - { op: comment, marker: agent:attempt }
+      - { op: label_remove, label: agent:needs-work }
+      - { op: label_add, label: agent:ready-for-review }
+```
+
+- `op` is required and is one of the effect ops the checker models, except `unmodelled`.
+- `label` is required for `label_add` and `label_remove`, and is a name or a glob. `*` is the only wildcard. Use `*` alone to allow any label, which is then a visible choice and not a gap.
+- `marker` is required for `comment` and `comment_edit`: a name, a glob, or `null` for a comment with no marker (a run-log entry, a one-line comment on a linked issue). A `comment_edit` carries only an index, so its marker is the marker of the comment it edits in the world the run started from. A comment that cannot be found matches nothing.
+
+`scripts/scenario.mjs` first places an effect in its scope (`scopeOf`, unchanged) and then, if that scope has `allow` entries, asks `allowedBy` whether one matches. All three places that checked a scope now go through one function, `forbiddenWrite`: a pure skill's effects, an item skill's effects, and the effects of a rerun. A real run is judged the same way, because `eval` reads its effects from `diffWorlds` and hands them to `checkScenario`.
+
+**A scope is all sentences or all `allow`.** An effect in a scope with no `allow` is checked by the scope alone, as before, so no contract changes until it is migrated. Once one entry has an `allow`, only what some `allow` lists is permitted, so a sentence without one beside it would look like permission it does not give. The validator rejects the mix, and also an `allow` for an op that can never land in its scope (a `push` under `claimed`), which would allow nothing and look as if it did.
+
+## Why not
+
+- **Parse the sentences.** They are written for a model to follow. Parsing them would tie the wording of every skill to the checker.
+- **Only check the label set.** Comments and markers are where a skill most easily writes something it should not, and the lease and handoff protocols are built on markers.
+- **Require `allow` everywhere at once.** It is a large change across eleven contracts, and the scenarios would all have to be right at once. A prose scope keeps its old behaviour until it is migrated.
+
+## What it does not do
+
+- **`create_pr`, `create_issue`, `close` and `review_request` are matched by op alone.** What a new item is labelled with, or what a PR is closed for, is not constrained yet. The schema rejects `label` and `marker` on them, so they cannot be mistaken for checked.
+- **The golden scenarios still come from the same reading of the skill.** An `allow` made from the prose and a scenario made from the prose can share a mistake. Running a model (ADR 0016) is what tests that.
+- **It checks effects, not their order or count.** One extra comment with an allowed marker passes.
+
+## Migration
+
+1. The schema, the checker and `shepherd-github-pr` (this step).
+2. The item skills: `triage-github-issue`, `implement-github-issue`, `review-github-pr`.
+3. The group, sweep and file skills: the `-issues` and `-prs` groups, `reconcile-github-issues`, `file-github-issues` and `explore-github-repo`.

scripts/contracts.mjs

@@ -14,6 +14,55 @@ export const PIPELINE_KINDS = ["item", "group", "sweep"];
 export const KINDS = [...PIPELINE_KINDS, "utility", "reference"];
 export const WRITE_SCOPES = ["claimed", "repository", "other", "shared", "unmodelled"];
 
+// What an effect can be, as the scenario checker models it (scripts/scenario.mjs). `unmodelled` is not something a skill
+// does, so a contract cannot allow it. An effect in REPOSITORY_OPS is a `repository` write, whatever it targets.
+export const REPOSITORY_OPS = ["push", "merge", "delete_branch", "create_pr", "label_create", "label_update", "write_file"];
+const ITEM_OPS = ["label_add", "label_remove", "comment", "comment_edit", "close", "review_request"];
+export const ALLOW_OPS = [...ITEM_OPS, "create_issue", ...REPOSITORY_OPS];
+const LABEL_OPS = ["label_add", "label_remove"];
+const MARKER_OPS = ["comment", "comment_edit"];
+// The ops that can land in each scope: scopeOf puts REPOSITORY_OPS in `repository`, a comment on the run log in `shared`,
+// and a `create_issue` always in `other`.
+export const SCOPE_OPS = {
+  claimed: ITEM_OPS,
+  repository: REPOSITORY_OPS,
+  other: [...ITEM_OPS, "create_issue"],
+  shared: MARKER_OPS,
+};
+
+/**
+ * The parts of one `effects.writes.<scope>` entry. An entry is a sentence, or `{text, allow}`: the sentence stays as the
+ * explanation, and `allow` is one mapping or a list of them, each saying which effect the sentence permits.
+ * @returns {{text: string|undefined, allow: object[]|undefined}} `allow` is undefined for a prose-only entry
+ */
+export function entryParts(entry) {
+  if (typeof entry === "string") return { text: entry, allow: undefined };
+  if (!entry || typeof entry !== "object" || Array.isArray(entry)) return { text: undefined, allow: undefined };
+  const a = entry.allow;
+  return { text: entry.text, allow: a === undefined ? undefined : Array.isArray(a) ? a : [a] };
+}
+
+/** Every structured `allow` mapping in a scope's entries, flattened. Empty when the scope is still prose. */
+export function allowsOf(list) {
+  return (Array.isArray(list) ? list : []).flatMap((e) => entryParts(e).allow ?? []);
+}
+
+/** Problems with one `allow` mapping, as short messages. */
+function checkAllow(a, scope) {
+  if (!a || typeof a !== "object" || Array.isArray(a)) return ["an `allow` must be a mapping with an `op`"];
+  const out = [];
+  for (const k of Object.keys(a)) if (!["op", "label", "marker"].includes(k)) out.push(`\`allow\` has unknown key \`${k}\``);
+  if (!ALLOW_OPS.includes(a.op)) return [...out, `\`allow.op\` must be one of ${ALLOW_OPS.join(", ")}`];
+  if (SCOPE_OPS[scope] && !SCOPE_OPS[scope].includes(a.op)) out.push(`\`${a.op}\` can never land in \`${scope}\`, so this entry would allow nothing`);
+  if (LABEL_OPS.includes(a.op)) {
+    if (!isText(a.label)) out.push(`\`${a.op}\` needs a \`label\`: a name, or a glob such as \`agent:*\`. Use \`*\` to allow any`);
+  } else if (a.label !== undefined) out.push(`\`label\` applies only to ${LABEL_OPS.join(" and ")}, not \`${a.op}\``);
+  if (MARKER_OPS.includes(a.op)) {
+    if (!("marker" in a) || (a.marker !== null && !isText(a.marker))) out.push(`\`${a.op}\` needs a \`marker\`: a name, a glob such as \`agent:*\`, or \`null\` for a comment with no marker`);
+  } else if ("marker" in a) out.push(`\`marker\` applies only to ${MARKER_OPS.join(" and ")}, not \`${a.op}\``);
+  return out;
+}
+
 const COMMON = ["kind", "step", "params", "requires", "returns", "ensures", "effects", "never", "calls", "idempotent", "terminates"];
 // A utility skill is called from other skills and has no step of its own, but says who calls it.
 const UTILITY = COMMON.filter((k) => k !== "step").concat("used_by");
@@ -154,8 +203,21 @@ export function checkContracts(skills, byName, external = new Set(), { pending =
         if (!e.writes || typeof e.writes !== "object" || Array.isArray(e.writes)) err("`effects.writes` must be a mapping (it may be empty)");
         else {
           for (const [scope, list] of Object.entries(e.writes)) {
-            if (!WRITE_SCOPES.includes(scope)) err(`effects.writes scope \`${scope}\` is not one of ${WRITE_SCOPES.join(", ")}`);
-            else if (!isStrings(list)) err(`effects.writes.${scope} must be a non-empty list of strings`);
+            if (!WRITE_SCOPES.includes(scope)) { err(`effects.writes scope \`${scope}\` is not one of ${WRITE_SCOPES.join(", ")}`); continue; }
+            if (!Array.isArray(list) || list.length === 0) { err(`effects.writes.${scope} must be a non-empty list of entries`); continue; }
+            const parts = list.map(entryParts);
+            list.forEach((x, i) => {
+              if (typeof x === "string" ? !isText(x) : !isText(parts[i].text)) err(`effects.writes.${scope}[${i}] must be a sentence, or a mapping with a \`text\` sentence and an \`allow\``);
+              if (typeof x === "object" && x !== null && !Array.isArray(x)) {
+                for (const k of Object.keys(x)) if (k !== "text" && k !== "allow") err(`effects.writes.${scope}[${i}] has unknown key \`${k}\``);
+                if (x.allow !== undefined && parts[i].allow.length === 0) err(`effects.writes.${scope}[${i}].allow must not be empty`);
+              }
+              for (const a of parts[i].allow ?? []) for (const m of checkAllow(a, scope)) err(`effects.writes.${scope}[${i}]: ${m}`);
+            });
+            // A scope is prose or it is structured. Once one entry has an \`allow\`, anything no \`allow\` matches is forbidden, so a
+            // prose-only entry beside it would read as permission it does not give.
+            const structured = parts.filter((x) => x.allow).length;
+            if (structured && structured !== parts.length) err(`effects.writes.${scope} mixes entries with and without \`allow\`. Once one has it, every entry must, because only what an \`allow\` lists is permitted`);
           }
           if (c.kind !== "item" && e.writes.claimed) err("only an item skill claims, so a group or sweep skill has no `effects.writes.claimed`");
           if (c.kind === "item" && argTarget && !e.writes.claimed) err("an item skill that is given an issue or PR claims it, so it needs `effects.writes.claimed`");

scripts/scenario.mjs

@@ -14,14 +14,14 @@
 import { isDeepStrictEqual } from "node:util";
 import { readFileSync } from "node:fs";
 import { contractOf } from "./skill-contracts.mjs";
+import { ALLOW_OPS, REPOSITORY_OPS, allowsOf } from "./contracts.mjs";
 import { canSplit, depthOf } from "../skills/meta/agent-workflow-protocol/scripts/helpers.mjs";
 
 export const MUTEX_ISSUE = ["needs-info", "ready-for-agent", "ready-for-human", "agent:pr-open"];
 export const MUTEX_PR = ["agent:needs-work", "agent:ready-for-review", "agent:human-merge"];
 export const LEASE_LABELS = ["agent:triage", "agent:in-progress"];
-const REPOSITORY_OPS = ["push", "merge", "delete_branch", "create_pr", "label_create", "label_update", "write_file"];
 // `unmodelled` is not something a skill does: diffWorlds reports a change it cannot express with it.
-const OPS = ["label_add", "label_remove", "comment", "comment_edit", "close", "push", "merge", "delete_branch", "create_pr", "create_issue", "review_request", "label_create", "label_update", "write_file", "unmodelled"];
+const OPS = [...ALLOW_OPS, "unmodelled"];
 
 // ---- repository state: the label set and the agent instructions file ------------------------------
 // A world may hold `labels: [{name, description}]` (the repository's label set) and `files: {path: text}`.
@@ -210,6 +210,54 @@ export function scopeOf(effect, ctx) {
   return "other";
 }
 
+/** `*` matches any run of characters, and nothing else is special: labels and markers are plain names. */
+export function globMatches(glob, s) {
+  const re = glob.split("*").map((p) => p.replace(/[.+?^${}()|[\]\\]/g, "\\$&")).join(".*");
+  return new RegExp(`^${re}$`).test(s);
+}
+
+/**
+ * The marker of the comment an effect writes. A `comment` names its own. A `comment_edit` names only the index, so the
+ * marker is the one on that comment in the world the run started from. `null`: the comment has no marker.
+ * `undefined`: it cannot be found, which no `allow` matches.
+ */
+export function markerOf(effect, ctx) {
+  if (effect.op === "comment") return effect.marker ?? null;
+  const c = item(ctx.world, effect.target)?.comments?.[effect.index];
+  return c ? (c.marker ?? null) : undefined;
+}
+
+/** The first of the structured `allow` mappings that permits the effect, or null. `op` must match, and so must `label` and `marker` where the mapping has them. */
+export function allowedBy(effect, allows, ctx) {
+  for (const a of allows) {
+    if (a.op !== effect.op) continue;
+    if (a.label !== undefined && !(typeof effect.label === "string" && globMatches(a.label, effect.label))) continue;
+    if ("marker" in a) {
+      const m = markerOf(effect, ctx);
+      if (a.marker === null ? m !== null : !(typeof m === "string" && globMatches(a.marker, m))) continue;
+    }
+    return a;
+  }
+  return null;
+}
+
+const describe = (x) => [x.op, x.label !== undefined && `\`${x.label}\``, "marker" in x && (x.marker === null ? "(no marker)" : `\`${x.marker}\``)].filter(Boolean).join(" ");
+
+/**
+ * Why the contract does not allow an effect, or null when it does. First the scope must be one `effects.writes` lists.
+ * Then, if that scope has structured entries (`allow`), one of them must match: the scope alone is not enough, because
+ * a skill that may add its own labels could otherwise add any label. `why` ends the sentence that the caller starts.
+ * Throws when the effect cannot be placed (it names an item that is not in the world).
+ */
+export function forbiddenWrite(contract, effect, ctx) {
+  const scope = scopeOf(effect, ctx);
+  const writes = contract.effects?.writes ?? {};
+  if (!Object.hasOwn(writes, scope)) return { scope, why: `is a \`${scope}\` write, which the contract does not allow` };
+  const allows = allowsOf(writes[scope]);
+  if (allows.length === 0 || allowedBy(effect, allows, ctx)) return null;
+  return { scope, why: `is a \`${scope}\` write, but it is not one the contract's \`allow\` entries permit (${describe({ ...effect, ...(effect.op === "comment_edit" ? { marker: markerOf(effect, ctx) } : {}) })}). It allows: ${allows.map(describe).join("; ")}` };
+}
+
 /** The item that a `create_pr` or `create_issue` effect adds to the world `w`. */
 export function createdItem(w, e) {
   if (e.op === "create_pr") return { ...e.data, number: e.number, state: "open", labels: e.labels ?? [], draft: false, head: e.sha ?? "new", base: e.base ?? w.default_branch ?? "main", checks: [], openFindings: 0, closes: e.closes ?? [], comments: [] };
@@ -589,8 +637,8 @@ export function checkPureScenario(contract, sc) {
   if (allowed.length === 0 && work.length) bad("a pure skill must leave no effects");
   for (const e of work.length && allowed.length ? work : []) {
     try {
-      const scope = scopeOf(e, { world: sc.world ?? { issues: [], prs: [] }, claimed: new Set() });
-      if (!allowed.includes(scope)) bad(`${e.op} on ${e.target ?? `#${e.number}`} is a \`${scope}\` write, which the contract does not allow`);
+      const f = forbiddenWrite(contract, e, { world: sc.world ?? { issues: [], prs: [] }, claimed: new Set() });
+      if (f) bad(`${e.op} on ${e.target ?? `#${e.number}`} ${f.why}`);
     } catch (err) { bad(err.message); }
   }
   if (work.length) { try { applyEffects(sc.world ?? { issues: [], prs: [] }, work); } catch (err) { bad(err.message); } }
@@ -800,13 +848,12 @@ export function checkScenario(contract, sc) {
   const ctx = { world, claimed };
 
   // 2. scopes
-  const allowed = Object.keys(contract.effects?.writes ?? {});
   for (const e of work) {
-    let scope;
-    try { scope = scopeOf(e, ctx); } catch (err) { bad(err.message); continue; }
-    if (allowed.includes(scope)) continue;
+    let f;
+    try { f = forbiddenWrite(contract, e, ctx); } catch (err) { bad(err.message); continue; }
+    if (!f) continue;
     if (e.op === "unmodelled") bad(`the run changed \`${e.field}\` of ${e.target}, which the checker cannot model, and the contract lists no \`unmodelled\` write`);
-    else bad(`${e.op} on ${e.target ?? `#${e.number}`} is a \`${scope}\` write, which the contract does not allow`);
+    else bad(`${e.op} on ${e.target ?? `#${e.number}`} ${f.why}`);
   }
   if (outcome === "skipped" && work.length) bad("skipped must leave no effects");
   if (outcome === "noop" && work.length) bad("noop may leave only the lease comment");
@@ -985,8 +1032,8 @@ export function checkScenario(contract, sc) {
     for (const e of again) {
       if (e.marker !== "agent:lease" && made.has(key(e))) bad(`the rerun repeats ${e.op} on ${e.target}, which the interrupted run already did`);
       try {
-        const scope = scopeOf(e, { world: after, claimed });
-        if (!allowed.includes(scope)) bad(`the rerun's ${e.op} on ${e.target} is a \`${scope}\` write, which the contract does not allow`);
+        const f = forbiddenWrite(contract, e, { world: after, claimed });
+        if (f) bad(`the rerun's ${e.op} on ${e.target} ${f.why}`);
       } catch (err) { bad(err.message); }
     }
     try { applyEffects(after, again); } catch (err) { bad(`the rerun's effects do not apply: ${err.message}`); }