From 3089af714a529b598b70beee9ac05b2915faf40d Mon Sep 17 00:00:00 2001 From: tilorc-bot <309221022+tilorc-bot@users.noreply.github.com> Date: Tue, 22 Sep 2026 17:05:58 +0000 Subject: [PATCH] Expand the soundness fuzzer's model pools and grammar Cover the blind spots the adversarial audit named: declared symbols (n, ni, xi) with declaration-respecting pools, infinities and undefined values, evaluate=False powers, acos/factorial, extended-real predicates, and matrix expressions with element-predicate expansion. On the sathandlers tip this found a regression: _pow_real_facts compares a Number exponent against zero, so a nan exponent raises TypeError (Invalid NaN comparison). main returns None and sympy.ask answers None. The curated list pins the reduced query. --- agent-reports/2026-09-22-fuzzer-coverage.md | 83 ++++++++++ reasoning/tests/test_check_soundness.py | 37 ++++- tools/check_soundness.py | 167 ++++++++++++++++++-- 3 files changed, 269 insertions(+), 18 deletions(-) create mode 100644 agent-reports/2026-09-22-fuzzer-coverage.md diff --git a/agent-reports/2026-09-22-fuzzer-coverage.md b/agent-reports/2026-09-22-fuzzer-coverage.md new file mode 100644 index 0000000..84b8aa8 --- /dev/null +++ b/agent-reports/2026-09-22-fuzzer-coverage.md @@ -0,0 +1,83 @@ +# Agent report: closing the soundness fuzzer's blind spots + +- **Date:** 2026-09-22 +- **Status:** branch `agent/fuzz-coverage` on top of `main` `b07b332` (the + merged fuzzer from #8); tool-only, no handler code touched +- **Scope:** `tools/check_soundness.py` and + `reasoning/tests/test_check_soundness.py` +- **Read this if:** you are fixing the remaining adversarial regressions, or + you want the fuzzer to explore a query class it previously missed +- **Stale after:** changes to the model pools, the handler grammar, or PR #9's + adversarial suite +- **TL;DR:** the fuzzer now generates declared symbols, infinities/undefined + values, `evaluate=False` powers, extended-real predicates, `acos`, + `factorial`, and matrix expressions, and expands matrix element predicates + itself. On PR #9's tip it found a new crash: `satask` raises + `TypeError: Invalid NaN comparison` for any unevaluated power with a `nan` + exponent. The matrix fix branch (`cd0a061`) verifies clean. + +## What changed + +The adversarial report from PR #9 listed the fuzzer's blind spots; each is now +covered: + +| Blind spot | Coverage | +|---|---| +| No `oo`/`zoo`/`nan` in `SCALAR_VALUES` | Added, plus `oo`/`-oo`/`zoo` to `CONSTANTS` and the extended-real predicates | +| No declared symbols | Added `n` (integer), `ni` (integer negative), `xi` (infinite); models are drawn from per-symbol pools filtered by the declared assumptions | +| Only plain `MatrixSymbol` subjects | Added `MatMul`, `MatPow`, `HadamardProduct`, `Transpose`, `MatrixSlice` and `ZeroMatrix`, plus the element predicates | +| `ask` cannot decide element predicates | `atom_truth` expands concrete matrices with `as_explicit` and asks about each element; only then falls back to `ask` | +| No `acos`/`factorial`/`evaluate=False` | Added to both the stdlib and Hypothesis grammars | + +Assumptions are still satisfied by construction: the model is drawn first and +each generated literal is emitted with the polarity that makes it true. + +## New finding: `nan` exponent crashes `_pow_real_facts` + +Found by the random engine on PR #9's tip (`924c4a9`, `--engine random +--seed 1 --cases 500`), reduced to: + +```python +satask(Q.algebraic(Pow(2, nan, evaluate=False))) # TypeError, was None on main +satask(Q.real(Pow(x, nan, evaluate=False))) # TypeError, was None on main +sympy.ask(Q.algebraic(Pow(2, nan, evaluate=False))) # None +``` + +Root cause is `reasoning/sathandlers.py:468`: + +```python +if (isinstance(exp, Number) and exp < 0 +``` + +`S.NaN` is a `Number`, and `nan < 0` raises `TypeError: Invalid NaN +comparison`. The comparison needs a realness guard (or a `nan` short-circuit). +`main` returns `None` for these queries, so this is a regression from the new +Pow facts, and `sympy.ask` answers `None` rather than raising. The curated list +now includes `algebraic(Pow(2, nan, evaluate=False))`; it passes on `main` and +reports the crash on `924c4a9` and `cd0a061`. + +## Verification runs + +| Checkout | Run | Result | +|---|---|---| +| `main` `b07b332` | curated | 0 findings | +| PR #9 tip `924c4a9` | curated | 1 finding (the `nan` crash) | +| PR #9 tip | 150 Hypothesis examples | 0 findings | +| PR #9 tip | 500 random cases, seed 1 | 1 finding (the `nan` crash) | +| `fix/sathandlers-matrixfacts` `cd0a061` | adversarial + matrixfacts suites | 21 passed, 9 xfailed (scalar) | +| `fix/sathandlers-matrixfacts` | curated + 200 Hypothesis examples | only the `nan` crash; no matrix findings | + +The 500-case random run takes about 11 minutes with the expanded grammar (the +infinities and undefined values make some `ask` calls slower); the Hypothesis +engine is much faster and is the better fit for quick checks. + +## Notes + +- The advisory old-assumptions scan gains four `keyword` findings from the + declared symbols in the tool, matching the five PR #9 adds in its adversarial + test file; the scan remains advisory and exits 0. +- `fix/sathandlers-scalar` owns the file with the `nan` crash. Once it lands, + rerun `tools/check_soundness.py` against it and remove the curated case's + finding from the remaining list. +- The curated list still tracks the Pow `~complex(1/x)` case, which is fixed on + PR #9 and passes there. diff --git a/reasoning/tests/test_check_soundness.py b/reasoning/tests/test_check_soundness.py index 813277c..e9074df 100644 --- a/reasoning/tests/test_check_soundness.py +++ b/reasoning/tests/test_check_soundness.py @@ -7,7 +7,9 @@ from pathlib import Path from typing import Any -from sympy import I, Q, S, symbols +from sympy import I, Q, S, ask, symbols +from sympy.matrices.expressions import MatPow, MatrixSlice +from sympy.matrices.immutable import ImmutableMatrix _TOOL = Path(__file__).resolve().parents[2] / "tools" / "check_soundness.py" _spec = importlib.util.spec_from_file_location("check_soundness", _TOOL) @@ -141,3 +143,36 @@ 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 == [] + + +def test_declared_pools_respect_declared_assumptions() -> None: + integer_pool = check_soundness.declared_pool(check_soundness.n) + assert integer_pool + for value in integer_pool: + assert ask(Q.integer(value)) is True + infinite_pool = check_soundness.declared_pool(check_soundness.xi) + assert infinite_pool + for value in infinite_pool: + assert ask(Q.infinite(value)) is True + negative_pool = check_soundness.declared_pool(check_soundness.ni) + assert negative_pool + for value in negative_pool: + assert ask(Q.integer(value)) is True + assert ask(Q.negative(value)) is True + + +def test_matrix_element_predicates_are_expanded() -> None: + integer_matrix = ImmutableMatrix([[2, 0], [0, 1]]) + fractional_matrix = ImmutableMatrix([[S.Half, 0], [0, 1]]) + A = check_soundness.A + values = {A: integer_matrix, check_soundness.B: integer_matrix} + assert check_soundness.ground_truth( + Q.integer_elements(A), values) is True + assert check_soundness.ground_truth( + Q.integer_elements(A), {A: fractional_matrix, + check_soundness.B: integer_matrix}) is False + assert check_soundness.ground_truth( + Q.integer_elements(MatPow(A, -2)), values) is False + assert check_soundness.ground_truth( + Q.integer_elements(MatrixSlice(A, slice(0, 1), slice(0, 1))), + values) is True diff --git a/tools/check_soundness.py b/tools/check_soundness.py index 2ae1011..35d2c03 100644 --- a/tools/check_soundness.py +++ b/tools/check_soundness.py @@ -29,6 +29,13 @@ selects the seedable stdlib generator instead, which reports every finding it encounters rather than one minimized example per run. +The model pools and grammar cover declared symbols (``n``, ``ni`` and ``xi``), +infinities and undefined values, ``evaluate=False`` powers, and matrix +expressions (products, powers, slices and zero matrices). Matrix element +predicates are evaluated by expanding the substituted expression and asking +about each element, because ``ask`` does not decide them for explicit +matrices. + The audit imports ``reasoning`` from the environment; point ``PYTHONPATH`` at another checkout to audit its handlers:: @@ -52,14 +59,17 @@ from hypothesis import strategies as st from hypothesis.strategies import DrawFn from sympy import ( - Abs, E, I, Q, Rational, S, ask, cos, exp, im, log, pi, re, sin, sqrt, - symbols, + Abs, E, I, Pow, Q, Rational, S, Symbol, acos, ask, cos, exp, factorial, + im, log, nan, oo, pi, re, sin, sqrt, symbols, zoo, ) from sympy.assumptions.assume import AppliedPredicate from sympy.logic.boolalg import ( And, Equivalent, Implies, Not, Or, Xor, simplify_logic, ) -from sympy.matrices.expressions import MatrixSymbol +from sympy.matrices.expressions import ( + HadamardProduct, MatMul, MatPow, MatrixSlice, MatrixSymbol, Transpose, +) +from sympy.matrices.expressions.special import ZeroMatrix from sympy.matrices.immutable import ImmutableMatrix from reasoning.satask import satask @@ -71,7 +81,7 @@ SCALAR_VALUES: tuple[Any, ...] = ( S.Zero, S.One, S.NegativeOne, S(2), S(-2), S.Half, Rational(2, 3), Rational(-3, 2), I, -I, 2*I, 1 + I, 1 - I, sqrt(2), -sqrt(2), pi, E, - exp(2*pi), exp(pi), log(2), 3 + 4*I, + exp(2*pi), exp(pi), log(2), 3 + 4*I, oo, -oo, zoo, nan, ) MATRIX_VALUES: tuple[Any, ...] = ( @@ -85,34 +95,64 @@ ImmutableMatrix([[I, 0], [0, I]]), ImmutableMatrix([[1, 2], [3, 4]]), ImmutableMatrix([[1, 0], [0, 0]]), + ImmutableMatrix([[0, 0], [0, 0]]), + ImmutableMatrix([[0, 1], [0, 0]]), ) CONSTANTS: tuple[Any, ...] = ( - S.Zero, S.One, S.NegativeOne, S(2), I, pi, Rational(1, 2), E, + S.Zero, S.One, S.NegativeOne, S(2), I, pi, Rational(1, 2), E, oo, -oo, + zoo, ) SCALAR_PREDICATES: tuple[Any, ...] = ( Q.zero, Q.nonzero, Q.positive, Q.negative, Q.nonnegative, Q.nonpositive, - Q.real, Q.extended_real, Q.imaginary, Q.complex, Q.integer, Q.rational, - Q.irrational, Q.algebraic, Q.transcendental, Q.even, Q.odd, Q.prime, - Q.composite, Q.finite, Q.infinite, Q.hermitian, Q.antihermitian, - Q.commutative, + Q.real, Q.extended_real, Q.extended_positive, Q.extended_negative, + Q.extended_nonnegative, Q.extended_nonpositive, Q.imaginary, Q.complex, + Q.integer, Q.rational, Q.irrational, Q.algebraic, Q.transcendental, + Q.even, Q.odd, Q.prime, Q.composite, Q.finite, Q.infinite, Q.hermitian, + Q.antihermitian, Q.commutative, ) MATRIX_PREDICATES: tuple[Any, ...] = ( Q.square, Q.invertible, Q.fullrank, Q.symmetric, Q.diagonal, Q.lower_triangular, Q.upper_triangular, Q.orthogonal, Q.unitary, - Q.positive_definite, Q.singular, Q.hermitian, + Q.positive_definite, Q.singular, Q.hermitian, Q.integer_elements, + Q.real_elements, Q.complex_elements, ) RELATION_PREDICATES: tuple[Any, ...] = (Q.eq, Q.ne, Q.gt, Q.ge, Q.lt, Q.le) x, y, z = symbols("x y z") +n = Symbol("n", integer=True) +ni = Symbol("ni", integer=True, negative=True) +xi = Symbol("xi", infinite=True) A, B = MatrixSymbol("A", 2, 2), MatrixSymbol("B", 2, 2) -SCALAR_SYMBOLS: tuple[Any, ...] = (x, y, z) +SCALAR_SYMBOLS: tuple[Any, ...] = (x, y, z, n, ni, xi) MATRIX_SYMBOLS: tuple[Any, ...] = (A, B) +DECLARED_PREDICATES: dict[Any, tuple[Any, ...]] = { + n: (Q.integer, Q.commutative), + ni: (Q.integer, Q.negative, Q.commutative), + xi: (Q.infinite, Q.commutative), +} + +_DECLARED_POOLS: dict[Any, tuple[Any, ...]] = {} + + +def declared_pool(symbol: Any) -> tuple[Any, ...]: + """Values a symbol can take while respecting its declared assumptions.""" + if symbol not in _DECLARED_POOLS: + predicates = DECLARED_PREDICATES.get(symbol) + if predicates is None: + _DECLARED_POOLS[symbol] = SCALAR_VALUES + else: + _DECLARED_POOLS[symbol] = tuple( + value for value in SCALAR_VALUES + if all(ask(predicate(value)) is True + for predicate in predicates)) + return _DECLARED_POOLS[symbol] + CURATED_MODEL_COUNT = 32 CURATED_MODEL_TRIES = 400 @@ -127,6 +167,8 @@ "negative(-I + I*(cos(2)**2 + sin(2)**2))"), (Q.complex(1/x), Q.complex(x), "complex(1/x) | complex(x)"), (Q.zero(x), ~Q.complex(1/x), "zero(x) | ~complex(1/x)"), + (Q.algebraic(Pow(S(2), nan, evaluate=False)), True, + "algebraic(Pow(2, nan, evaluate=False))"), (Q.integer(sqrt(2)*x), Q.integer(x), "integer(sqrt(2)*x) | integer(x)"), (Q.real(x*y), Q.real(x) & Q.real(y), "real(x*y) | real(x) & real(y)"), (Q.zero(x*y), Q.zero(x), "zero(x*y) | zero(x)"), @@ -165,6 +207,55 @@ class CaseReport: suppressed: int = 0 +ELEMENT_PREDICATES: dict[Any, Any] = { + Q.integer_elements: Q.integer, + Q.real_elements: Q.real, + Q.complex_elements: Q.complex, +} + + +def _is_matrix(value: Any) -> bool: + return bool(getattr(value, "is_Matrix", False) + or getattr(value, "is_MatrixExpr", False)) + + +def _explicit_matrix(value: Any) -> Any: + if isinstance(value, ImmutableMatrix): + return value + if not _is_matrix(value): + return None + try: + explicit = value.as_explicit() + except Exception: + return None + return explicit if isinstance(explicit, ImmutableMatrix) else None + + +def _ask_bool(proposition: Any) -> bool | None: + truth = ask(proposition) + if truth is True: + return True + if truth is False: + return False + return None + + +def atom_truth(atom: Any) -> bool | None: + """Evaluate one ground atom, expanding matrix element predicates.""" + arguments = getattr(atom, "arguments", ()) + if arguments and _is_matrix(arguments[0]): + matrix = _explicit_matrix(arguments[0]) + if matrix is not None: + scalar = ELEMENT_PREDICATES.get(atom.function) + if scalar is not None: + element_truths = [_ask_bool(scalar(element)) for element in matrix] + if any(truth is None for truth in element_truths): + return None + return all(truth is True for truth in element_truths) + return _ask_bool(atom.function(matrix)) + return _ask_bool(atom) + + def ground_truth(formula: Any, values: dict[Any, Any]) -> bool | None: """Evaluate a ground formula with ``ask``, or None if an atom is unknown.""" if formula is True: @@ -175,7 +266,7 @@ def ground_truth(formula: Any, values: dict[Any, Any]) -> bool | None: substituted = formula.subs(values) replacements: dict[Any, Any] = {} for atom in substituted.atoms(AppliedPredicate): - truth = ask(atom) + truth = atom_truth(atom) if truth is None: return None replacements[atom] = S.true if truth is True else S.false @@ -204,7 +295,8 @@ def find_models(case: Case, scalar_symbols: Sequence[Any], if len(models) >= count: break values: dict[Any, Any] = { - symbol: rng.choice(SCALAR_VALUES) for symbol in scalar_symbols} + symbol: rng.choice(declared_pool(symbol)) + for symbol in scalar_symbols} values.update( {symbol: rng.choice(MATRIX_VALUES) for symbol in matrix_symbols}) if ground_truth(case.premises, values) is not True: @@ -318,7 +410,7 @@ def random_scalar(rng: random.Random, scalar_symbols: Sequence[Any], return rng.choice((*scalar_symbols, *CONSTANTS)) left = random_scalar(rng, scalar_symbols, depth - 1) right = random_scalar(rng, scalar_symbols, depth - 1) - operation = rng.randrange(11) + operation = rng.randrange(14) if operation == 0: return left + right if operation == 1: @@ -339,7 +431,13 @@ def random_scalar(rng: random.Random, scalar_symbols: Sequence[Any], return log(left) if operation == 9: return re(left) - return im(left) + if operation == 10: + return im(left) + if operation == 11: + return acos(left) + if operation == 12: + return factorial(left) + return Pow(left, right, evaluate=False) def random_atom(rng: random.Random, scalar_symbols: Sequence[Any], @@ -411,11 +509,46 @@ def scalar_strategy() -> Any: st.builds(log, children), st.builds(re, children), st.builds(im, children), + st.builds(acos, children), + st.builds(factorial, children), + st.builds( + lambda base, exp: Pow(base, exp, evaluate=False), + children, children), ), max_leaves=6, ) +def _matrix_slice(parent: Any, rows: tuple[int, int], + cols: tuple[int, int]) -> Any: + return MatrixSlice(parent, slice(*rows), slice(*cols)) + + +MATRIX_INDEX_RANGES: tuple[tuple[int, int], ...] = ( + (0, 1), (0, 2), (1, 2), +) + + +def matrix_strategy() -> Any: + square = st.recursive( + st.sampled_from(MATRIX_SYMBOLS), + lambda children: st.one_of( + st.builds(MatMul, children, children), + st.builds(HadamardProduct, children, children), + st.builds(MatPow, children, st.sampled_from((2, 3, 0, -1, -2))), + st.builds(Transpose, children), + ), + max_leaves=4, + ) + slices = st.builds( + _matrix_slice, st.sampled_from(MATRIX_SYMBOLS), + st.sampled_from(MATRIX_INDEX_RANGES), + st.sampled_from(MATRIX_INDEX_RANGES)) + zeros = st.builds( + ZeroMatrix, st.sampled_from((2, 3)), st.sampled_from((2, 3))) + return st.one_of(square, slices, zeros) + + def atom_strategy(matrices: bool) -> Any: scalar = st.builds( lambda predicate, subject: predicate(subject), @@ -424,7 +557,7 @@ def atom_strategy(matrices: bool) -> Any: return scalar matrix = st.builds( lambda predicate, subject: predicate(subject), - st.sampled_from(MATRIX_PREDICATES), st.sampled_from(MATRIX_SYMBOLS)) + st.sampled_from(MATRIX_PREDICATES), matrix_strategy()) return st.one_of(scalar, matrix) @@ -448,7 +581,7 @@ def formula_strategy(matrices: bool) -> Any: def hypothesis_cases(draw: DrawFn, matrices: bool = True) -> Case: """Generate a query together with a model satisfying its assumptions.""" values: dict[Any, Any] = { - symbol: draw(st.sampled_from(SCALAR_VALUES)) + symbol: draw(st.sampled_from(declared_pool(symbol))) for symbol in SCALAR_SYMBOLS} if matrices: values.update({