Repository navigation
docs(oracles): score oracle-first work and add declared reach #2233
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
4 commits
Select commit
Hold shift + click to select a range
91ee6db
docs(oracles): score oracle-first work and add declared reach
098a06a
docs(oracles): plan the oracle lint rules, CI checks, and agent feedb…
f41f4c9
docs(oracles): split long plan sentences
be0631a
docs(oracles): move the enforcement plan to issue #2234
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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/, | ||
| ) | ||
| }) | ||
| }) | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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<TState extends string>( | ||
| property: string, | ||
| states: ReadonlyArray<TState>, | ||
| { minimum = 1 }: { minimum?: number } = {}, | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win Reject a minimum that disables the reach check. If a caller sets 🤖 Prompt for AI Agents
|
||
| ) { | ||
| const counts = new Map<TState, number>(states.map((state) => [state, 0])) | ||
| let current = new Set<TState>() | ||
| 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<TState, number> { | ||
| 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(`, `), | ||
| ) | ||
| } | ||
| }, | ||
| } | ||
| } | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
Make the reach assertions independent of replay environment variables.
If
TANSTACK_DB_ORACLE_SEEDis set,createOracleReachskipsassertReached(). This test and the minimum-count test then fail because both expect an exception. Run these tests with an explicit non-replay configuration, or isolate the replay environment before constructing the helper.🤖 Prompt for AI Agents