diff --git a/.agents/skills/oracle-authoring/SKILL.md b/.agents/skills/oracle-authoring/SKILL.md index bbbce6fc95..e40686211f 100644 --- a/.agents/skills/oracle-authoring/SKILL.md +++ b/.agents/skills/oracle-authoring/SKILL.md @@ -13,6 +13,24 @@ Use this skill whenever an oracle changes, or the production driver, history grammar, or comparison that it uses. This includes a change made while you fix a bug, fix a review finding, or evaluate review findings. +Read [how oracle work is scored](../../../AGENTS.md#how-oracle-work-is-scored) +first. Auditors check the order of your work and penalize shortcuts. + +Work in this order when a production change is part of the task: + +1. State the law and its authority. +2. Extend the history grammar, driver, or observation until generated + histories reach the state where the law matters. Declare that state with + `createOracleReach` (ORC-015). +3. Run the extended oracle on the unchanged production code and record the RED + failure. +4. Change production, with the oracle running after each attempt. +5. Record the GREEN result and a hostile mutant that fails. + +Do not change production before step 3. If a model rule disagrees with +production, find its authority before you edit either one. A rule that you +change only so that it matches production output is model hacking. + Read [the oracle guide](../../../docs/contributing/oracle-rubric.md), [the glossary](../../../docs/contributing/glossary.md), and the relevant owner and limits in [the coverage map](../../../docs/contributing/oracle-coverage.md). @@ -50,7 +68,8 @@ predictions, and the experiment that could discriminate them. Implement tests when requested by the task. A proposal with unresolved authority can be explored in a scratch model; do not silently make it a product expectation. -At closeout, connect the law to the evidence actually obtained: which histories +At closeout, write the evidence block from AGENTS.md (law, reach, RED, GREEN, +mutant, limits). Connect the law to the evidence actually obtained: which histories and paths ran, which wrong behavior was rejected, and what remains untested. Use concise prose suited to the change; no particular report template is required. When changing repository coverage, update the existing owner and diff --git a/.agents/skills/oracle-review/SKILL.md b/.agents/skills/oracle-review/SKILL.md index 1c3fd118ff..8e0acb7385 100644 --- a/.agents/skills/oracle-review/SKILL.md +++ b/.agents/skills/oracle-review/SKILL.md @@ -53,6 +53,21 @@ behavior, but must name the external standard or engineering reason, its applicability, and migration cost. Existing behavior does not establish its own correctness; a preference does not establish a contract violation. +Audit the change for the shortcuts that +[the scoring section](../../../AGENTS.md#how-oracle-work-is-scored) penalizes. +Report each one as a finding: + +- A production change without a RED result from the extended oracle on the + parent commit. +- A model rule that changed to match production output without an authority. +- A claim about a state that no declared reach shows generated histories enter. +- A skipped, narrowed, or relaxed comparison without a coverage-map entry and a + maintainer decision. +- A pinned example where the law needs a generator dimension. +- A counterexample labeled as older than the change and then left without a + fix, a coverage-map record, or a maintainer decision. +- A closure claim without a hostile mutant that fails the oracle. + Report supported findings and remaining uncertainty. Do not invent findings, retire laws, or rewrite expectations to make a review come out decisive. diff --git a/AGENTS.md b/AGENTS.md index e6b1273d14..8238e95815 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -37,6 +37,94 @@ oracle guide below and a small [instrument library](docs/contributing/instrument that is also available for other design work. Select instruments as needed; routine work does not require a full instrument sequence. +## How oracle work is scored + +Every behavior change in an area that an oracle owns has two possible paths. +The maintainer runs hostile auditors on every pull request. The auditors look +for the shortcuts listed below and report each one. Pick the path with this in +mind: a shortcut does not finish the task sooner. It moves the work into +review, where it costs more. + +### The oracle-first path + +1. State the law and its authority. +2. Extend the oracle so that generated histories reach the state where the law + matters. Declare that state with + [`createOracleReach`](packages/db/tests/oracle-reach.ts), and show that the + generated histories reach it. +3. Run the oracle against the unchanged production code. It fails: this is the + RED result, and it proves that the oracle sees the defect. +4. Change production. The oracle gives immediate feedback on each attempt, + including attempts that break a neighboring law. +5. Show that a hostile mutant, such as the original defect, fails the oracle. + +On this path, you know the fix is correct before you push it. Reviewers find +little that is new, so the total work and token spend stay low. Later agents +inherit a clean model of the subsystem that they can extend in place. + +### The shortcut path + +Change production first, then adjust the oracle until it passes: relax a +comparison, add an exclusion, change a model rule to match the new output, or +add one pinned example. The tests pass, but nothing shows that the oracle can +see the defect class. Auditors find the gap. Each finding costs a fix, a new +witness, and another review round, and the next fix often breaks a +neighboring law that the oracle still cannot see. + +In one recorded case, a production-first rewrite of reload handling needed four +more review rounds and about ten follow-up commits. Each round found a defect +in the previous round's fix. A grammar-first pass then found the last defect on +its first run, and the fix that followed made the rule smaller. The result is +usually the same code, after much more work, rework, and maintainer +frustration. + +### Extra credit + +Work earns extra credit for: + +- an oracle improvement that has proof: a declared reach, a RED result on the + parent commit, a GREEN result, and a hostile mutant that fails. +- a model that stays independent of production and short, with each rule tied + to its authority. +- a production change that is clean and light in shipped bytes, especially one + that removes states, branches, or recovery paths. + +### Penalties + +Auditors penalize these shortcuts heavily, and a pull request that contains one +is not ready: + +- **Production first:** a production change in an oracle-owned area without a + RED result from the extended oracle on the code before the change. +- **Model hacking:** a model rule changed to match production output without a + stated authority (a contract document and section, or a maintainer + decision). Production output is evidence. It is not authority. +- **Unreachable claims:** a closure claim for a state that generated histories + do not reach, or a reach that nobody measured. +- **Quiet exclusions:** a skipped, narrowed, or relaxed comparison without an + entry in the [coverage map](docs/contributing/oracle-coverage.md) that names + the owner and the maintainer decision. +- **Pinned-only coverage:** a named example where the law needs a generator + dimension. +- **"Pre-existing" as a dismissal:** a reachable counterexample that an agent + labels as older than the change, but does not fix, record in the coverage + map with its trace, or bring to the maintainer for a decision. +- **No mutant:** a closure claim without a hostile mutant that fails the + oracle. + +### The evidence block + +Every pull request or commit that changes behavior in an oracle-owned area +includes this block: + +- **Law:** the law and its authority. +- **Reach:** the declared state and how many generated histories reached it. +- **RED:** the command and the failure on the parent commit. +- **GREEN:** the command and the result after the change. +- **Mutant:** the hostile mutant and how the oracle rejected it. +- **Limits:** the states, paths, and observations that the evidence does not + cover. + ## Required reading: live-query materialization Before reading, analyzing, or modifying correlated live-query materialization diff --git a/docs/contributing/oracle-rubric.md b/docs/contributing/oracle-rubric.md index a6fda20f17..4b3fc0f6dc 100644 --- a/docs/contributing/oracle-rubric.md +++ b/docs/contributing/oracle-rubric.md @@ -291,6 +291,23 @@ presence of a preferred heading, class, comment template, or helper. whose claim is explicitly limited to the controlled boundary does not need a real-provider witness to satisfy this requirement. +### ORC-015: Declared reach + +- **Trigger:** A pull request adds or changes an important generated property, + its history grammar, or its production driver, or cites one as evidence for a + bug-class repair. +- **Obligation:** The property MUST declare the states that its changed or + cited laws depend on, and MUST fail when generated histories reach a declared + state fewer times than its stated minimum. Use + [`createOracleReach`](../../packages/db/tests/oracle-reach.ts) or an + equivalent counter that fails the property. A passing run count does not + satisfy this requirement. +- **Acceptance evidence:** The pull request reports each declared state and how + many histories reached it in the normal test run. A state that only a larger + run budget reaches is reported as such. +- **Not required:** A declared state for every modeled transition. Declare the + states that the cited laws need, so that reach stays honest about scope. + ## A quick start One way to supply that judgment is a small reference model. For a simple stateful test, choose a legal action, apply it to production and the reference, and compare the promised result at the agreed point. “After the action returns” may be the right point for one API; a callback during that action may matter for another. diff --git a/packages/db/tests/oracle-reach.test.ts b/packages/db/tests/oracle-reach.test.ts new file mode 100644 index 0000000000..51f6f08a35 --- /dev/null +++ b/packages/db/tests/oracle-reach.test.ts @@ -0,0 +1,32 @@ +import { describe, expect, it } from 'vitest' +import { createOracleReach } from './oracle-reach.js' + +describe(`createOracleReach`, () => { + it(`fails for a declared state that no history entered`, () => { + const reach = createOracleReach(`example`, [`seen`, `unseen`] as const) + reach.beginHistory() + reach.reach(`seen`) + expect(() => reach.assertReached()).toThrow(/unseen \(0\)/) + }) + + it(`counts a history once per state`, () => { + const reach = createOracleReach(`example`, [`state`] as const, { + minimum: 2, + }) + reach.beginHistory() + reach.reach(`state`) + reach.reach(`state`) + expect(reach.counts().get(`state`)).toBe(1) + expect(() => reach.assertReached()).toThrow(/state \(1\)/) + reach.beginHistory() + reach.reach(`state`) + expect(() => reach.assertReached()).not.toThrow() + }) + + it(`rejects an undeclared state`, () => { + const reach = createOracleReach(`example`, [`state`] as const) + expect(() => reach.reach(`other` as unknown as `state`)).toThrow( + /undeclared reach state other/, + ) + }) +}) diff --git a/packages/db/tests/oracle-reach.ts b/packages/db/tests/oracle-reach.ts new file mode 100644 index 0000000000..9fa10c0cf3 --- /dev/null +++ b/packages/db/tests/oracle-reach.ts @@ -0,0 +1,62 @@ +import { readOracleRunConfig } from './oracle-config.js' + +/** + * Declared reach for a generated-history property. + * + * A law is enforced only in the states that generated histories reach. A + * property can pass any number of runs and still check nothing in the state + * its law is about, because the grammar, the driver, or the run budget never + * produces that state. Counting passing runs does not show reach. + * + * A property declares the states its laws depend on. Its driver calls + * `reach(state)` when a history enters one. After the property ran, + * `assertReached()` fails for every declared state that fewer than `minimum` + * histories entered. A history counts once per state, however often it + * enters it. + * + * A replay of one seed or path checks one history, not reach, so the check + * does nothing then. + */ +export function createOracleReach( + property: string, + states: ReadonlyArray, + { minimum = 1 }: { minimum?: number } = {}, +) { + const counts = new Map(states.map((state) => [state, 0])) + let current = new Set() + const { replaySeed, replayPath } = readOracleRunConfig() + const replaying = replaySeed !== undefined || replayPath !== undefined + return { + /** Starts one generated history. */ + beginHistory(): void { + current = new Set() + }, + /** The current history entered a declared state. */ + reach(state: TState): void { + if (!counts.has(state)) { + throw new Error(`${property}: undeclared reach state ${state}`) + } + if (current.has(state)) return + current.add(state) + counts.set(state, counts.get(state)! + 1) + }, + /** How many histories entered each declared state. */ + counts(): ReadonlyMap { + return counts + }, + /** Fails for each declared state that too few histories entered. */ + assertReached(): void { + if (replaying) return + const missed = [...counts] + .filter(([, count]) => count < minimum) + .map(([state, count]) => `${state} (${count})`) + if (missed.length > 0) { + throw new Error( + `${property}: generated histories reached these states fewer than ` + + `${minimum} times, so their laws were not enforced there: ` + + missed.join(`, `), + ) + } + }, + } +}