Repository navigation
Add a soundness fuzzer for satask handlers - #8
Merged
Merged
Conversation
tools/check_soundness.py generates queries and checks definite satask answers against concrete models and sympy.ask. Model counterexamples are suppressed when ask shares the answer, because some handlers mirror upstream rules that ground models can contradict; --strict reports them. The curated regression list catches the T1/T2 unsoundness on cde5c70, and the audit is clean on agent/tail-audits across 470 random queries. No handler code is touched.
The hypothesis engine draws a model first and builds assumptions that hold under it, so no query is rejected for lack of a model, and findings shrink to a minimal example. The stdlib generator remains available with --engine random. The fuzzer found a new unsoundness on agent/tail-audits: the Pow complex closure lacks a nonzero-base guard, so complex(x) gives complex(1/x) and ~complex(1/x) gives ~zero(x). Both queries are curated regressions now.
Case.assumptions shadowed the SymPy attribute name the advisory old-assumptions scan looks for, so the scan reported seven false positives. Renaming the field keeps the scan at its two pre-existing findings. The README now points at the audit, and the report notes that CI wiring waits for the Pow complex fix.
Generating an example calls ask on ground atoms, which can exceed Hypothesis's slow-generation threshold on CI runners.
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Why
The validation suites measure how many queries get answered; they do not check
whether a definite answer is true. The
--oraclecomparison in #7 catchesdefinite contradictions with
ask, but a definite answer whereaskis unsureis accepted there and can still be unsound.
What
tools/check_soundness.py, which checks definitesataskanswersagainst concrete models and
ask. Hypothesis shrinks findings to minimalexamples, and generated assumptions are satisfied by a model drawn first, so
no query is rejected for lack of a model.
cde5c70) plus an--engine randommode for runs that report every finding.askalso gives, since some handlersintentionally mirror upstream rules that ground models can contradict;
--strictreports them.hypothesisto the dev extra, cover the helpers and strategy with unittests, and document the command in the README. No handler code is touched.
Findings
cde5c70.agent/tail-audits(not onmain): the Pow complexclosure has no nonzero-base guard, so
complex(x)givescomplex(1/x)and~complex(1/x)gives~zero(x). Reported separately; both queries arecurated regressions.
maingoesred when the tail-audit handlers merge.
Verification
pytest reasoning/tests: 154 passed, 1 xfailed.mypystrict clean;tools/regen_known_facts.py --checkup to date;old-assumptions scan at its 2 pre-existing findings.
This description was written by an AI agent (opencode, deepseek-v4.1-flash) on
behalf of TiloRC.