Repository navigation
Measure chance reach misses in oracle properties #2289
Description
Problem
A generated property declares the states its laws depend on, and createOracleReach fails a run in which too few histories entered one (ORC-015). When only random histories enter a declared state, the check can fail by chance at the normal run budget. No law fails, but CI goes red. #2287 was one case: in about 0.3% of 60-run campaigns, source-health.history never chose the one reach prefix that enters two of its states.
The fix for #2287 adds a shared seam for this:
oraclePropertyOptions(…, { examples })runs fixed examples first in every run, on top of the base budget.createOracleReach(…, { fixedHistories })fails for each declared state that those examples did not enter.
The three source-health properties use the seam, so their reach does not depend on the seed. packages/db/tests/declared-reach-oracle.property.test.ts (oracle.declared-reach) owns these rules.
About 40 other files use createOracleReach or runOracleCampaign. Their chance of a reach miss at the normal budget has not been measured.
Work
- For each property with declared reach, list the declared states that no fixed example enters.
- Measure how often a normal-budget run misses each of those states. For example, count the misses across many seeds, or sample the generator.
- For each state that can miss, add a fixed example through the seam, or record the state as probabilistic in
docs/contributing/oracle-coverage.mdwith a maintainer decision. Raise a run budget only with a maintainer decision, because it adds CI time. - Consider a lint rule that reports a property that chooses a reach prefix by chance (
fc.option(fc.constantFrom(...prefixes))) without fixed examples.
The coverage map's "Oracle tooling" section links to this issue as the destination for the gap.
This issue was written by Isaac.
Activity
KyleAMathews commentedon Oct 29, 2026
PR #2290 moves two parts of this work here, by agreement with the maintainer.
examplesinside their base runs, so the examples displace random histories. Examples includeSortedMap-oracle.test.ts,cleanup-queue-oracle.property.test.ts,notification-laws-oracle.test.ts, the three Svelte SSR oracles, and the db-ivm top-k oracles.oraclePropertyOptions(base, property, { examples })now runs examples on top of the base runs. Moving a property to it raises its total runs by its number of examples, so each move belongs with that property's reach measurement.runOracleCampaigngives each campaign a reach without fixed histories. Thus a campaign cannot make a declared state's reach independent of the seed, asfixedHistorieswithbeginHistory({ fixed: true })now does for a property. The 22 campaign users need that option, or a measurement that shows they do not miss by chance.The needed witness stays the same: per property, the declared states that no fixed example enters, and how often a normal-budget run misses each one.
This comment was written by Isaac.
fix(persistence): recover Electric rows after interleaved source comm…