Lock Counterexamples Before an Agent May Edit a Property Test

A green property after an agent rewrite is not a pass. Diff the saved counterexample journal against the parent commit. If examples disappeared, strategy bounds shrank, or max_examples dropped, treat the patch as a failed property check even when CI is green.

This article is a local method, not a production study. The scripts below are labeled proposals. Run them on your own repository before you trust the exit codes.

The failure the job color hides

Property tests fail on concrete values. Hypothesis and similar libraries then save those values so the next run can replay them. That journal is the evidence. The property source file is only the generator.

An agent patch can keep the test name and flip the outcome without fixing the code. It can narrow integers() to a tiny interval. It can cut max_examples. It can wrap the body in assume() until almost every draw is discarded. It can delete files under .hypothesis/examples. The job still prints passed.

A fixture hit count does not catch this. A tautology classifier does not catch a smaller domain. You need a journal diff.

What to lock besides the test file

Lock four artifacts from the parent tree. Store them next to the patch, not only in the agent's working copy.

1. The example database under .hypothesis/examples (or the equivalent replay store for your runner).
2. Declared strategy bounds and max_examples in the property modules.
3. assume() density and any deadline / timeout knobs.
4. The seed or derandomize setting used in CI.

If the patch changes the production code and those four stay equal, a newly passing property is stronger evidence. If any of the four move toward a smaller search, score the property as compromised.

Decision table

Use this table as the merge rule. Do not collapse it into one job color.

Parent journal	Patch journal	Generator / budget	Verdict
Saved example still present and still fails on parent code	Same example now passes on patch code	Bounds and max_examples unchanged	Accept as a candidate fix
Saved example missing from patch tree	n/a	Any	Reject: journal deletion
Example present	Example skipped by new assume()	Filter rate up	Reject: domain shrink
Example present	Property passes	integers(a, b) interval smaller, or max_examples lower	Reject: search shrink
No saved example	Property passes	Bounds unchanged, max_examples unchanged	Inconclusive: do not freeze; require a hit
Example present	Property fails	Unchanged	Real remaining bug; do not merge

Inconclusive is not green. It is a missing measurement.

Proposal: a journal and generator checker

The script below is a proposal you can run locally. It does not talk to a network. It compares two checkouts: parent/ and patch/.

#!/usr/bin/env python3
"""journal_diff.py — proposal, not a published benchmark."""
from __future__ import annotations

import ast
import json
import sys
from pathlib import Path
from typing import Any

PROPERTY_MARKERS = {"given", "hypothesis"}


def example_ids(root: Path) -> set[str]:
    base = root / ".hypothesis" / "examples"
    if not base.is_dir():
        return set()
    return {p.relative_to(base).as_posix() for p in base.rglob("*") if p.is_file()}


class PropVisitor(ast.NodeVisitor):
    def __init__(self) -> None:
        self.max_examples: list[int] = []
        self.assume_count = 0
        self.int_spans: list[tuple[int | None, int | None]] = []
        self.deadlines: list[int] = []

    def visit_Call(self, node: ast.Call) -> None:
        name = ast.unparse(node.func) if sys.version_info >= (3, 9) else ""
        if name.endswith("given") or name.endswith("settings"):
            for kw in node.keywords:
                if kw.arg == "max_examples" and isinstance(kw.value, ast.Constant):
                    if isinstance(kw.value.value, int):
                        self.max_examples.append(kw.value.value)
                if kw.arg == "deadline" and isinstance(kw.value, ast.Constant):
                    if isinstance(kw.value.value, int):
                        self.deadlines.append(kw.value.value)
        if name.endswith("assume"):
            self.assume_count += 1
        if name.endswith("integers"):
            lo = hi = None
            args = [a for a in node.args if isinstance(a, ast.Constant)]
            if len(args) >= 1 and isinstance(args[0].value, int):
                lo = args[0].value
            if len(args) >= 2 and isinstance(args[1].value, int):
                hi = args[1].value
            for kw in node.keywords:
                if kw.arg in {"min_value", "max_value"} and isinstance(kw.value, ast.Constant):
                    if kw.arg == "min_value" and isinstance(kw.value.value, int):
                        lo = kw.value.value
                    if kw.arg == "max_value" and isinstance(kw.value.value, int):
                        hi = kw.value.value
            self.int_spans.append((lo, hi))
        self.generic_visit(node)


def scan_props(root: Path) -> dict[str, Any]:
    visitor = PropVisitor()
    for path in root.rglob("test_*.py"):
        src = path.read_text(encoding="utf-8")
        if not any(m in src for m in PROPERTY_MARKERS):
            continue
        visitor.visit(ast.parse(src))
    return {
        "max_examples_sum": sum(visitor.max_examples),
        "max_examples_min": min(visitor.max_examples) if visitor.max_examples else None,
        "assume_count": visitor.assume_count,
        "int_spans": visitor.int_spans,
        "deadline_max": max(visitor.deadlines) if visitor.deadlines else None,
    }


def span_width(span: tuple[int | None, int | None]) -> float:
    lo, hi = span
    if lo is None or hi is None:
        return float("inf")
    return float(hi - lo)


def classify(parent: Path, patch: Path) -> dict[str, Any]:
    p_ex, n_ex = example_ids(parent), example_ids(patch)
    dropped = sorted(p_ex - n_ex)
    p_meta, n_meta = scan_props(parent), scan_props(patch)
    p_width = min((span_width(s) for s in p_meta["int_spans"]), default=float("inf"))
    n_width = min((span_width(s) for s in n_meta["int_spans"]), default=float("inf"))
    reasons: list[str] = []
    if dropped:
        reasons.append("journal_deletion")
    if n_meta["assume_count"] > p_meta["assume_count"]:
        reasons.append("assume_increase")
    if (
        n_meta["max_examples_min"] is not None
        and p_meta["max_examples_min"] is not None
        and n_meta["max_examples_min"] < p_meta["max_examples_min"]
    ):
        reasons.append("max_examples_drop")
    if n_width < p_width:
        reasons.append("integer_domain_shrink")
    if (
        n_meta["deadline_max"] is not None
        and p_meta["deadline_max"] is not None
        and n_meta["deadline_max"] > p_meta["deadline_max"]
    ):
        reasons.append("deadline_relaxed")
    verdict = "reject" if reasons else "candidate"
    return {
        "verdict": verdict,
        "reasons": reasons,
        "dropped_examples": dropped,
        "parent": p_meta,
        "patch": n_meta,
    }


def main() -> int:
    if len(sys.argv) != 3:
        print("usage: journal_diff.py PARENT_DIR PATCH_DIR", file=sys.stderr)
        return 2
    report = classify(Path(sys.argv[1]), Path(sys.argv[2]))
    print(json.dumps(report, indent=2, default=str))
    return 1 if report["verdict"] == "reject" else 0


if __name__ == "__main__":
    raise SystemExit(main())

Exit code 1 means the property lane is compromised. Exit code 0 means the journal and generator budget did not shrink. It does not mean the production bug is gone.

Numbered workflow

Run the parent and the patch as two trees. Do not let the agent overwrite the parent journal in place.

1. Check out the merge base into parent/. Keep .hypothesis/examples from CI, not a fresh empty directory.
2. Check out the agent patch into patch/. Copy the parent example database into the patch tree before the first patch run so replay is possible.
3. Run the same property selection on both trees with the same seed. Example:

export HYPOTHESIS_PROFILE=ci
pytest parent/tests/test_invariants.py -q --hypothesis-seed=20260921
cp -a parent/.hypothesis/examples patch/.hypothesis/examples
pytest patch/tests/test_invariants.py -q --hypothesis-seed=20260921
python journal_diff.py parent patch

1. If journal_diff.py exits 1, stop. Restore any deleted example as a committed regression file under tests/counterexamples/ so a later patch cannot drop it by ignoring the Hypothesis cache.
2. If the verdict is candidate, replay each saved example as a plain unit test. A property that only passes because the generator no longer draws the old value is not a candidate.
3. Only after the journal is stable should you look at flake retries. A flake freeze is unrelated to a missing counterexample. Do not use a freeze to hide a dropped example.

Promote surviving examples out of the cache. A cache is not a merge artifact. A committed file is.

# tests/counterexamples/test_replay_order_id.py
# proposal: human-owned replay, not agent-owned generator
from myapp.orders import apply_discount

def test_replay_zero_qty_does_not_go_negative():
    # value originally saved by Hypothesis on the parent tree
    assert apply_discount(qty=0, rate=0.3) == 0

The agent may add new properties. It may not edit this replay file in the same patch that claims to fix it.

Candidate properties from a free server

Generating extra properties is useful. Scoring the patch with those generated properties is not, until a human has locked at least one replay value.

Disclosure: This article was prepared as part of MonkeyCode's product outreach.

A free model endpoint and a free server are enough for the cheap half of this workflow: draft candidate @given tests in an isolated checkout, run them until they hit or time out, and write surviving values into tests/counterexamples/. Keep that queue off the merge gate. The gate reads only the committed journal and the generator-budget diff. If you already use MonkeyCode for that isolated checkout, keep the disclosure in the PR template so reviewers know which files were model-drafted.

Do not send the parent example database to a public model if it contains production payloads. Redact or synthesize values first.

What this does not measure

The checker uses AST text, not a full Hypothesis internal format. Unusual helper wrappers will evade it. That is a limitation, not a known exploit yield.

Integer span is a proxy. text(), lists(), and custom strategies need their own width functions. Add them per repository. A false reject is possible when a human tightens a bound because the spec changed. Record the spec change in the same PR and skip that rule explicitly. Silent skips are not allowed.

A missing .hypothesis/examples directory on parent is inconclusive. It is not a pass. Teams that never persist the database cannot use this method until they start persisting it.

This method does not replace contract tests, typed boundaries, or review of behavior the properties never mentioned.

Who should not use this

Skip this workflow if you have no property tests. A journal diff on an empty store is theater.

Skip it if the agent is also the only author of the replay files. Human ownership of tests/counterexamples/ is the point.

Skip it for one-off scripts with no merge gate. The cost of two checkouts is wasted if nothing blocks the merge.

Skip it when examples contain secrets. Persist redacted shapes, not live tokens.

Close

Keep the generator editable. Keep the saved values frozen. If you already persist a Hypothesis database, run journal_diff.py on the next agent patch before you trust a green property job.