Add a soundness fuzzer for satask handlers

README.md

@@ -83,6 +83,11 @@ pull request. Timing results and the validation progress comparison appear in
 the job summary; CI timings are illustrative and the validation comparison is
 informational.
 
+To audit definite `satask` answers for soundness, run
+`python tools/check_soundness.py`. It checks answers against concrete models
+and SymPy's `ask` and shrinks findings with Hypothesis; see
+`agent-reports/2026-09-22-soundness-fuzzer.md` for usage and results.
+
 The benchmark reports warm median conversion, discovery/encoding, query
 encoding, and solving times, plus clause and variable counts. Discovery and fact
 encoding are measured together because facts are encoded as they are produced.

agent-reports/2026-09-22-soundness-fuzzer.md

@@ -0,0 +1,129 @@
+# Agent report: a soundness fuzzer for satask handlers
+
+- **Date:** 2026-09-22
+- **Status:** tool implemented on branch `agent/handler-fuzzer` (based on `main`
+  `29cca2e`); no handler code touched
+- **Scope:** `tools/check_soundness.py`, `reasoning/tests/test_check_soundness.py`,
+  `pyproject.toml` (adds `hypothesis` to the dev extra), and the README
+  validation section
+- **Read this if:** you are adding or auditing handler facts and want to know
+  whether a definite `satask` answer is true, not just whether it matches a
+  validation expectation
+- **Stale after:** changes to `reasoning/satask.py`'s answer semantics, the
+  model value pools, or the curated regression list
+- **TL;DR:** the validation suites measure how many queries get answered; this
+  tool checks whether the answers are sound. It catches the T1 and T2
+  unsoundness on `cde5c70` and found a new one on `agent/tail-audits`:
+  `satask(Q.zero(x), ~Q.complex(1/x))` returns `False`, but `x = 0` satisfies
+  the assumption and makes the proposition true.
+
+## What it does
+
+`tools/check_soundness.py` generates queries (a curated regression list plus
+random queries) and checks each definite answer against two oracles:
+
+1. **Concrete models.** Each symbol is assigned a value, the assumptions are
+   evaluated with `sympy.ask` on the ground atoms, and only satisfying
+   assignments are kept. A definite answer contradicted by any model is
+   unsound.
+2. **`sympy.ask`.** When `ask` returns a definite answer for the same query and
+   `satask` returns the opposite, the result is reported.
+
+It also reports assumptions that raise `Inconsistent assumptions` even though a
+model exists, and propositions whose negation gets the same definite answer.
+Missing deductions (`None` where `ask` is definite) are expected while handlers
+are being added and are not findings.
+
+Some handlers deliberately mirror SymPy rules that a concrete model can
+contradict, such as the closed-group rule that a sum of imaginary arguments is
+imaginary even when the sum cancels. A model counterexample is therefore only
+reported when `sympy.ask` does not return the same definite answer; `--strict`
+reports those upstream-shared counterexamples as well.
+
+## Hypothesis engine
+
+Random queries come from Hypothesis by default. The `hypothesis_cases`
+strategy draws a model first and then builds assumptions that hold under it, so
+every generated query has a satisfying assignment and nothing is rejected.
+Findings are shrunk to a minimal example; the stub-driven smoke test shrinks an
+always-wrong solver down to `Q.zero(x)` under `Q.zero(x)` with `x = 0`.
+`--engine random` keeps the seedable stdlib generator, which reports every
+finding in one run instead of one minimized example per run.
+
+## Usage
+
+The script imports `reasoning` from the environment, so point `PYTHONPATH` at a
+checkout to audit its handlers:
+
+```console
+.venv/bin/python tools/check_soundness.py
+PYTHONPATH=/path/to/worktree .venv/bin/python tools/check_soundness.py \
+    --cases 200
+.venv/bin/python tools/check_soundness.py --engine random --seed 7
+```
+
+Exit status is 1 when a finding is reported. `--early-return` also audits
+`early_return=True` answers, `--no-oracle` drops the `ask` comparison,
+`--derandomize` fixes the Hypothesis seed, and `--no-matrices` / `--no-relations`
+narrow the generator.
+
+## Results
+
+| Checkout | Queries | Findings | Upstream-shared |
+|---|---|---|---|
+| `cde5c70` (pre T1/T2 fix), curated | 12 | 2 (T1, T2) | 1 |
+| `cde5c70`, 200 Hypothesis examples | 212 | 3 (T1, T2, Pow complex) | 1 |
+| `main` `29cca2e`, curated | 12 | 0 | 0 |
+| `agent/tail-audits` `67fb3ed`, curated | 12 | 1 (Pow complex) | 2 |
+| `agent/tail-audits`, seeds 2-5, 100 random each | 412 | 0 | 1 per run |
+| `agent/tail-audits`, seed 21 with matrices | 70 | 0 | 1 |
+
+The T1 and T2 findings on `cde5c70` are exactly the bugs fixed by
+`agent/tail-hermitian` and `agent/tail-positive`: `satask` returned `False` for
+`Q.hermitian(x + I)` under `Q.imaginary(x)` (witness `x = -I`) and for
+`Q.positive(x**I)` under `Q.positive(x)` (witness `x = exp(2*pi)`). T3
+(`algebraic(exp(x)) | algebraic(x)`) is not flagged because plain `satask`
+already returns `None`; the bug only appears under the validation harness's
+`_exp_is_pow(True)` mode, which the fuzzer does not set.
+
+## New finding: `~Q.complex(1/x)` implies `~Q.zero(x)`
+
+Reproduces on `agent/tail-audits` `67fb3ed` and, without the new Pow closure,
+not on `main`:
+
+```python
+satask(Q.complex(1/x), Q.complex(x))      # True, but x = 0 gives zoo
+satask(Q.zero(x), ~Q.complex(1/x))        # False, but x = 0 satisfies the assumption
+sympy.ask(Q.zero(x), ~Q.complex(1/x))     # None
+```
+
+Chain: the Pow closure `allargs complex -> complex(expr)` has no nonzero-base
+guard, so `complex(x) -> complex(1/x)`. Contraposition gives
+`~complex(1/x) -> ~complex(x)`, and `~complex(x) -> ~real(x) -> ~zero(x)`, so
+`Q.zero(x)` is answered `False`. `ask` also returns `True` for
+`Q.complex(1/x)` under `Q.complex(x)`, so that over-inference alone is
+upstream-shared and only shows under `--strict`; the `~zero(x)` consequence is
+not shared and is reported. Both curated cases are in the regression list.
+
+## Caveats
+
+- Model coverage is finite. The value pools include the witnesses for the known
+  bugs (`-I`, `exp(2*pi)`, `0`), but a new bug whose only witness is outside the
+  pool will be missed.
+- The Hypothesis engine reports one minimized example per run and stops there;
+  the random engine is available when all findings in a run are wanted.
+- Cases whose ground atoms are unknown to `ask` are skipped and counted in the
+  summary. The random engine skips roughly half of its queries at the default
+  `--model-tries 200`; the Hypothesis engine does not skip.
+- Relation assumptions are restricted to real operands, so complex comparisons
+  do not abort model search.
+
+## Next steps
+
+- Fix the Pow complex closure by guarding it with a nonzero base, then confirm
+  the curated case flips to passing.
+- Run the fuzzer against each tail/matrix worktree before merging handler
+  changes; `--strict` gives the upstream-shared list for review.
+- A fixed-seed Hypothesis run (`--cases 50 --derandomize`, about 10s) can gate
+  CI once the Pow finding is fixed; wiring it before then would turn `main` red
+  as soon as the tail-audit handlers merge.

pyproject.toml

@@ -14,7 +14,7 @@ sympy = [
     "sympy @ git+https://github.com/sympy/sympy.git@ddbb536d7e803e4c38d5d5808ad1217368b12655",
 ]
 
-dev = ["pytest", "mypy"]
+dev = ["hypothesis", "pytest", "mypy"]
 
 [tool.setuptools.package-data]
 reasoning = ["LICENSE.sympy"]

reasoning/tests/test_check_soundness.py

@@ -0,0 +1,143 @@
+"""Tests for the audit helpers in ``tools/check_soundness.py``."""
+from __future__ import annotations
+
+import importlib.util
+import random
+import sys
+from pathlib import Path
+from typing import Any
+
+from sympy import I, Q, S, symbols
+
+_TOOL = Path(__file__).resolve().parents[2] / "tools" / "check_soundness.py"
+_spec = importlib.util.spec_from_file_location("check_soundness", _TOOL)
+assert _spec is not None and _spec.loader is not None
+check_soundness: Any = importlib.util.module_from_spec(_spec)
+sys.modules["check_soundness"] = check_soundness
+_spec.loader.exec_module(check_soundness)
+
+x, y = symbols("x y")
+
+
+def _stub(result: Any, error: Exception | None = None) -> Any:
+    def satask_fn(proposition: Any, assumptions: Any = True,
+                  **kwargs: Any) -> Any:
+        if error is not None:
+            raise error
+        return result
+    return satask_fn
+
+
+def _audit(case: Any, satask_fn: Any, ask_fn: Any = None,
+           use_oracle: bool = False, strict: bool = False) -> Any:
+    rng = random.Random("audit")
+    return check_soundness.audit_case(
+        case, (x,), (), rng, satask_fn, ask_fn, use_oracle=use_oracle,
+        strict=strict)
+
+
+def test_ground_truth_evaluates_ground_atoms() -> None:
+    formula = Q.positive(x) & ~Q.zero(x)
+    assert check_soundness.ground_truth(formula, {x: S(2)}) is True
+    assert check_soundness.ground_truth(formula, {x: S.Zero}) is False
+    assert check_soundness.ground_truth(Q.prime(x) & ~Q.prime(x), {x: S(2)}) is False
+    assert check_soundness.ground_truth(True, {}) is True
+
+
+def test_ground_truth_returns_none_for_unknown_atoms() -> None:
+    assert check_soundness.ground_truth(Q.hermitian(x + y), {x: x, y: y}) is None
+
+
+def test_find_models_returns_satisfying_assignments() -> None:
+    case = check_soundness.Case(Q.hermitian(x + I), Q.imaginary(x), "t1")
+    models = check_soundness.find_models(
+        case, (x,), (), random.Random("models"), 12, 200)
+    assert models
+    for model in models:
+        assert check_soundness.ground_truth(Q.imaginary(x), model) is True
+
+
+def test_unsatisfiable_assumptions_are_skipped() -> None:
+    case = check_soundness.Case(Q.positive(x), Q.positive(x) & Q.negative(x),
+                                "unsat")
+    report = _audit(case, _stub(True))
+    assert report.findings == ()
+    assert not report.has_model
+
+
+def test_counterexample_is_reported() -> None:
+    case = check_soundness.Case(Q.hermitian(x + I), Q.imaginary(x), "t1")
+    report = _audit(case, _stub(False))
+    assert report.has_model
+    assert "counterexample" in [finding.kind for finding in report.findings]
+
+
+def test_upstream_shared_counterexample_is_suppressed() -> None:
+    case = check_soundness.Case(Q.positive(x), True, "positive")
+
+    def ask_fn(proposition: Any, assumptions: Any = True) -> Any:
+        return False
+
+    report = _audit(case, _stub(False), ask_fn, use_oracle=True)
+    assert report.suppressed == 1
+    assert "counterexample" not in [f.kind for f in report.findings]
+    strict_report = _audit(
+        case, _stub(False), ask_fn, use_oracle=True, strict=True)
+    assert "counterexample" in [f.kind for f in strict_report.findings]
+
+
+def test_spurious_inconsistency_is_reported() -> None:
+    case = check_soundness.Case(Q.positive(x), True, "positive")
+    report = _audit(
+        case, _stub(None, ValueError("Inconsistent assumptions")))
+    assert [finding.kind for finding in report.findings] == [
+        "spurious-inconsistency"]
+
+
+def test_both_polars_are_reported() -> None:
+    case = check_soundness.Case(Q.positive(x), True, "positive")
+    report = _audit(case, _stub(True))
+    assert "both-polars" in [finding.kind for finding in report.findings]
+
+
+def test_oracle_disagreement_is_reported() -> None:
+    case = check_soundness.Case(Q.positive(x), True, "positive")
+
+    def ask_fn(proposition: Any, assumptions: Any = True) -> Any:
+        return False
+
+    report = _audit(case, _stub(True), ask_fn, use_oracle=True)
+    assert "oracle-disagreement" in [finding.kind for finding in report.findings]
+
+
+def test_sound_stub_reports_nothing() -> None:
+    case = check_soundness.Case(Q.positive(x), True, "positive")
+    report = _audit(case, _stub(None))
+    assert report.findings == ()
+    assert report.has_model
+
+
+def test_hypothesis_cases_carry_satisfying_models() -> None:
+    from hypothesis import HealthCheck, given, settings
+
+    @settings(max_examples=15, deadline=None, database=None,
+              suppress_health_check=[HealthCheck.too_slow])
+    @given(check_soundness.hypothesis_cases(True))
+    def check(case: Any) -> None:
+        assert case.model is not None
+        assert check_soundness.ground_truth(case.premises, case.model) is True
+
+    check()
+
+
+def test_unsoundness_found_carries_findings() -> None:
+    case = check_soundness.Case(Q.positive(x), True, "positive")
+    finding = check_soundness.Finding("counterexample", case, "detail")
+    error = check_soundness.UnsoundnessFound([finding])
+    assert error.findings == (finding,)
+
+
+def test_hypothesis_runner_reports_nothing_for_sound_stub() -> None:
+    findings, _ = check_soundness.run_hypothesis(
+        _stub(None), None, matrices=False, max_examples=10, use_oracle=False)
+    assert findings == []