astrta medium: Separate validation progress from solver performance benchmarks

.github/workflows/ci.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Install the package with pinned SymPy and dev tools
         run: python -m pip install -e '.[sympy,dev]'
       - name: Run unit tests
-        run: python -m pytest reasoning/tests -q
+        run: python -m pytest reasoning/tests tests -q
       - name: Type check
         run: python -m mypy
       - name: Check the vendored known facts are up to date
@@ -75,7 +75,7 @@ jobs:
         continue-on-error: true
         run: |
           set -o pipefail
-          python validation/compare_backends.py --timings 0 | tee validation.txt
+          python validation/compare_backends.py --timings 0 --output validation.json | tee validation.txt
       - name: Add the validation progress to the job summary
         if: always() && hashFiles('validation.txt') != ''
         run: |
@@ -98,4 +98,5 @@ jobs:
           path: |
             benchmark.json
             validation.txt
+            validation.json
           if-no-files-found: ignore

.gitignore

@@ -8,3 +8,6 @@ __pycache__/
 env/
 results/
 html/
+
+# Container benchmark artifacts
+bench-results/

README.md

@@ -70,9 +70,13 @@ lightweight formulas. Legacy substitution helpers remain available for callers.
 
 ## Validation and performance
 
-Run `python -m pytest reasoning/tests` and
+Run `python -m pytest reasoning/tests tests` and
 `python -m benchmarks.satask --repeat 25`.
 
+For fixed-workload ASV timings with answer checks, phase measurements, and
+scaling cases, see [benchmarks/README.md](benchmarks/README.md). Upstream validation
+tracks correctness separately; its wall time measures test execution cost.
+
 To compare answers against the pinned SymPy `satask`, run
 `python -m benchmarks.compare_satask --include-early-return`. Saved original
 modules remain supported with `--baseline-satask` and `--baseline-handlers`.

asv.conf.json

@@ -2,10 +2,23 @@
     "version": 1,
     "project": "reasoning",
     "repo": ".",
-    "branches": ["HEAD"],
+    "branches": [
+        "HEAD"
+    ],
     "environment_type": "virtualenv",
-    "pythons": ["3.14"],
+    "pythons": [
+        "3.14"
+    ],
     "benchmark_dir": "asvbench",
     "install_command": "python -m pip install '{wheel_file}[sympy,dev]'",
-    "plugins": [".asvbench.loadcheck"]
+    "plugins": [
+        ".asvbench.loadcheck"
+    ],
+    "matrix": {
+        "env_nobuild": {
+            "PYTHONHASHSEED": [
+                "0"
+            ]
+        }
+    }
 }

asvbench/_workloads.py

@@ -0,0 +1,62 @@
+"""Fixed workloads and answer contracts; independent of validation test flow."""
+from collections.abc import Callable
+from dataclasses import dataclass
+
+from sympy import MatrixSymbol, Q, symbols
+
+# Bump when inputs, expected answers, or cache policy change. This also versions
+# timings whose function source does not include the workload definitions.
+VERSION = "1"
+NAMES = ("simple", "nested", "sum10", "matrix", "contradiction",
+         "upstream_integer", "upstream_zero", "upstream_unknown")
+CONSISTENT_NAMES = tuple(name for name in NAMES if name != "contradiction")
+
+
+@dataclass(frozen=True)
+class Case:
+    proposition: object
+    assumptions: object
+    expected: bool | str | None
+
+
+def sum_case(arity: int) -> Case:
+    xs = symbols(f"x:{arity}")
+    return Case(Q.integer(sum(xs)), Q.integer(xs[0]), None)
+
+
+def case(name: str) -> Case:
+    x, y = symbols("x y")
+    matrix = MatrixSymbol("A", 2, 2)
+    # First five inputs match benchmarks.satask.cases(). The remaining cases
+    # are individual assertions from pinned SymPy test_query.py's test_integer
+    # and test_zero. Extracting assertions fixes the workload even when an
+    # earlier assertion in the upstream test starts passing or failing.
+    return {
+        "simple": Case(Q.real(x), Q.positive(x), True),
+        "nested": Case(Q.zero(x*(x+y)), Q.positive(x) & Q.positive(y), False),
+        "sum10": sum_case(10),
+        "matrix": Case(Q.invertible(matrix), Q.fullrank(matrix) & Q.square(matrix), True),
+        "contradiction": Case(Q.real(x), Q.real(x) & ~Q.real(x), "inconsistent"),
+        "upstream_integer": Case(Q.integer(x), Q.even(x) | Q.odd(x), True),
+        "upstream_zero": Case(Q.zero(x), Q.negative(x) | Q.positive(x), False),
+        "upstream_unknown": Case(Q.integer(x), ~Q.positive(x), None),
+    }[name]
+
+
+def answer(call: Callable[[], bool | None]) -> bool | str | None:
+    try:
+        return call()
+    except ValueError as error:
+        if str(error) != "Inconsistent assumptions":
+            raise
+        return "inconsistent"
+
+
+def check(actual: bool | str | None, expected: bool | str | None) -> None:
+    if type(actual) is not type(expected) or actual != expected:
+        raise AssertionError(f"answer changed: expected {expected!r}, got {actual!r}")
+
+
+def answer_code(value: bool | str | None) -> int:
+    """-1 unknown, 0 false, 1 true, 2 inconsistent; never a speed score."""
+    return {None: -1, False: 0, True: 1, "inconsistent": 2}[value]

asvbench/pipeline.py

@@ -0,0 +1,128 @@
+"""Warm-cache timings with fixed queries and explicit answer contracts.
+
+Inputs are built and answers checked outside timing. Mutable databases/engines
+are recreated for each call; Solve additionally disables timeit's inner loop
+and warmup so its engine has not already answered the query. See benchmarks/README.md.
+"""
+from typing import ClassVar
+
+from reasoning.clauses import assert_formula, compile_formula
+from reasoning.engine import ReasoningEngine
+from reasoning.satask import get_all_relevant_facts, satask
+from reasoning.sympy_adapter import normalize
+
+from ._workloads import (
+    CONSISTENT_NAMES,
+    NAMES,
+    VERSION,
+    answer,
+    answer_code,
+    case,
+    check,
+    sum_case,
+)
+
+
+def _database(workload):
+    prop, assumptions = normalize(workload.proposition), normalize(workload.assumptions)
+    db = get_all_relevant_facts(prop, assumptions)
+    assert_formula(assumptions, db)
+    return db, compile_formula(prop, db)
+
+
+class Pipeline:
+    params = NAMES
+    param_names: ClassVar[list[str]] = ["case"]
+    version = VERSION
+
+    def setup(self, name):
+        self.workload = case(name)
+        check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)),
+              self.workload.expected)
+
+    def time_satask(self, name):
+        # Keep the result check in the timed path too: a behavior change on a
+        # repeated call must not produce a misleading successful measurement.
+        check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)),
+              self.workload.expected)
+
+
+class Phases:
+    params = CONSISTENT_NAMES
+    param_names: ClassVar[list[str]] = ["case"]
+    version = VERSION
+
+    def setup(self, name):
+        self.workload = case(name)
+        self.prop = normalize(self.workload.proposition)
+        self.assumptions = normalize(self.workload.assumptions)
+        self.db, self.query = _database(self.workload)
+        check(ReasoningEngine(self.db).ask(self.query), self.workload.expected)
+
+    def time_discovery_encoding(self, name):
+        db = get_all_relevant_facts(self.prop, self.assumptions)
+        assert_formula(self.assumptions, db)
+        compile_formula(self.prop, db)
+
+    def time_engine_ctor(self, name):
+        ReasoningEngine(self.db)
+
+    def track_clauses(self, name):
+        return len(self.db.data)
+
+    def track_variables(self, name):
+        return len(self.db.variables)
+
+
+class Solve:
+    params = CONSISTENT_NAMES
+    param_names: ClassVar[list[str]] = ["case"]
+    version = VERSION
+    number = 1
+    warmup_time = 0
+    repeat = 10
+
+    def setup(self, name):
+        self.workload = case(name)
+        db, self.query = _database(self.workload)
+        check(ReasoningEngine(db).ask(self.query), self.workload.expected)
+        self.engine = ReasoningEngine(db)
+
+    def time_solve(self, name):
+        check(self.engine.ask(self.query), self.workload.expected)
+
+
+class Outcomes:
+    """Record actual behavior even when a timing's answer contract fails."""
+    params = NAMES
+    param_names: ClassVar[list[str]] = ["case"]
+    version = VERSION
+
+    def setup(self, name):
+        self.workload = case(name)
+
+    def track_answer(self, name):
+        return answer_code(answer(lambda: satask(self.workload.proposition,
+                                                self.workload.assumptions)))
+
+
+class SumScaling:
+    params: ClassVar[list[int]] = [10, 20, 40, 80]
+    param_names: ClassVar[list[str]] = ["arity"]
+    version = VERSION
+
+    def setup(self, arity):
+        self.workload = sum_case(arity)
+        check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)),
+              self.workload.expected)
+        self.db, _ = _database(self.workload)
+
+    def time_satask(self, arity):
+        check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)),
+              self.workload.expected)
+
+    def track_clauses(self, arity):
+        return len(self.db.data)
+
+    def track_variables(self, arity):
+        return len(self.db.variables)

asvbench/validation_progress.py

@@ -13,14 +13,14 @@
   backend.  Control series: it measures the pinned SymPy suite against
   itself, so it should stay near-flat at a high count; movement there
   reflects a changed environment or pin, not progress in this project.
-- ``track_suite_wall_time``: whole-suite wall-clock seconds per backend.
-
-A full run costs ~50 s per backend, so the work happens once per commit in
-``setup_cache``; asv pickles its return value and passes it as the first
-argument to every benchmark function.  Counts and wall times are reported
-as ``track_*`` benchmarks (single recorded values) rather than ``time_*``
-ones, which auto-repeat and keep the minimum -- minutes of wasted
-subprocess runs for a ~50 s suite.
+- ``track_validation_wall_time``: whole-suite wall-clock seconds per backend.
+
+The expensive upstream generated-facts control is excluded. Counts therefore
+start a new series with one fewer test per backend than the original 104-test
+collection. Per-test outcomes can be saved with the harness's ``--output`` flag.
+Whole-suite time measures validation execution cost, not engine performance:
+fixing an early assertion makes the same test perform more work. Use pipeline.py
+for fixed-workload performance measurements.
 """
 from __future__ import annotations
 
@@ -42,14 +42,14 @@ def setup_cache() -> Runs:
     """Run both backends once per commit; cache outcomes and wall time."""
     runs = {}
     for backend in BACKENDS:
-        outcomes, _, _, wall = run_backend(backend, list(DEFAULT_SUITES), [])
+        outcomes, _, _, wall = run_backend(backend, list(DEFAULT_SUITES), [],
+                                            include_controls=False)
         runs[backend] = (outcomes, wall)
     return runs
 
 
-# Two ~50 s pytest subprocesses per commit; asv kills setup_cache after the
-# 60 s default benchmark timeout otherwise.
-setup_cache.timeout = 900.0
+# Allow for slow hosts without retaining the old full-control timeout.
+setup_cache.timeout = 120.0
 
 
 def _count_passed(runs: Runs, backend: str,
@@ -75,7 +75,7 @@ def track_passed_sympy(runs: Runs, suite_file: str) -> int:
     return _count_passed(runs, "sympy", suite_file)
 
 
-def track_suite_wall_time(runs: Runs, backend: str) -> float:
+def track_validation_wall_time(runs: Runs, backend: str) -> float:
     """Wall-clock seconds for one full pytest run of both suites."""
     return runs[backend][1]
 
@@ -86,5 +86,10 @@ def track_suite_wall_time(runs: Runs, backend: str) -> float:
 track_passed_sympy.params = [SUITE_NAMES]
 track_passed_sympy.unit = "tests"
 
-track_suite_wall_time.params = [list(BACKENDS)]
-track_suite_wall_time.unit = "s"
+track_validation_wall_time.params = [list(BACKENDS)]
+track_validation_wall_time.unit = "s"
+
+# The control exclusion changes the population, not solver correctness.
+track_passed.version = "2-exclude-generated-facts-control"
+track_passed_total.version = "2-exclude-generated-facts-control"
+track_passed_sympy.version = "2-exclude-generated-facts-control"

benchmarks/Dockerfile

@@ -0,0 +1,10 @@
+FROM python:3.14-slim
+RUN apt-get update && apt-get install -y --no-install-recommends git g++ \
+    && rm -rf /var/lib/apt/lists/*
+COPY pyproject.toml /tmp/project/pyproject.toml
+# Install dependencies, not a source snapshot: bench-container mounts the
+# checkout under test at /work. Preserve SymPy's VCS metadata for the pin check.
+RUN python -c 'import tomllib, subprocess; p = tomllib.load(open("/tmp/project/pyproject.toml", "rb")); subprocess.check_call(["python", "-m", "pip", "install", "asv==0.6.6", *p["project"]["optional-dependencies"]["sympy"], *p["project"]["optional-dependencies"]["dev"]])'
+RUN python -m pip install "setuptools>=68"
+# ASV hardcodes ~/.asv-machine.json; redirect just that file to writable tmpfs.
+RUN ln -s /tmp/asv-machine.json /root/.asv-machine.json