0.8.0: native sort promotion + independent verification API

.pre-commit-config.yaml

@@ -10,7 +10,7 @@ repos:
     hooks:
         - id: flake8
           additional_dependencies: [ Flake8-pyproject ]
-          exclude: ^(experimental/|benchmarks/)
+          exclude: ^(experimental/|benchmarks/|src/simplipy/verify/)
   - repo: https://github.com/pre-commit/mirrors-mypy
     rev: v1.16.0
     hooks:
@@ -20,4 +20,4 @@ repos:
             types-tqdm==4.67.0.20250516 ,
             types-toml==0.10.8.20240310,
             types-PyYAML==6.0.12.20250516]
-        exclude: ^(tests/|experimental/|benchmarks/)
+        exclude: ^(tests/|experimental/|benchmarks/|src/simplipy/promotion/|src/simplipy/verify/)

CHANGELOG.md

@@ -1,5 +1,37 @@
 # Changelog
 
+## 0.8.0 (unreleased)
+
+Makes the public package produce the BEST rule sets from one command: mining now natively
+promotes every rule to the strongest sound sort, and a public verification API can
+independently gate + monitor any rule set.
+
+### Added
+- **Native sort promotion** (`simplipy.promotion`; `find_rules(promote_sorts=True)`, CLI
+  config key `promote_sorts`). After mining and pruning, every rule (mined + proposed) is
+  re-certified at the stronger sorts and shipped at the strongest SOUND one: `_` (arbitrary
+  subtree), `!` (certified-finite subtree, enforced by a match-time defined-and-finite-a.e.
+  certificate), or `?` (variable-leaf, the fallback). Five stages: a pointwise exact bar on
+  an atom lattice, a const-bearing witness-map bar, an exact-arbiter overturn of finite-draw
+  demotions, a subsumption/derivability refund, and the `_`→`!`→`?` ladder with a
+  moving-spike structural refusal. Promotion is fail-safe: an uncertifiable rule stays `?`
+  and loses only composite-subtree recall, never soundness. This recovers the simplification
+  power that conservative `?`-only rulesets leave unrealized (a mined ruleset promoted this
+  way matches a far larger legacy engine's reduction at a fraction of the rules), because the
+  limiting factor was sort generality, not the number of rules.
+- **Independent verification API** (`simplipy.verify`): `verify_ruleset` gates a rule set by
+  judging every rule at its own symbolic trigger points under an arbitrary-precision contract
+  evaluator (eight-bucket classification, 100% coverage by construction); `monitor_ruleset`
+  runs the deployed engine over an adversarial+sampled corpus and attributes any
+  deployed-value violation to the responsible rule under an independent high-precision
+  evaluator; `verify_rule` gives a single-rule verdict. Deliberately implemented
+  independently of the compiled core so it cross-checks the miner rather than echoing it.
+  Both carry poison self-tests.
+
+### Changed
+- `mpmath` and `scipy` are now runtime dependencies (offline mining + verification only; the
+  inline simplify path remains the compiled core).
+
 ## 0.7.1 — 2026-07-21
 
 ### Fixed

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "simplipy-core"
-version = "0.7.1"              # kept in lockstep with the Python package version (pyproject.toml)
+version = "0.8.0"              # kept in lockstep with the Python package version (pyproject.toml)
 edition = "2021"
 rust-version = "1.83"          # MSRV floor of the resolved tree (pyo3 0.29 requires Rust >= 1.83)
 description = "Rust inline-phase backend for the SimpliPy prefix-expression simplifier (PyO3, the simplipy._core extension)"

pyproject.toml

@@ -6,7 +6,7 @@ authors = [
     ]
 readme = "README.md"
 requires-python = ">=3.11"
-version = "0.7.1"
+version = "0.8.0"
 license = "MIT"
 license-files = ["LICEN[CS]E*"]
 keywords = ["symbolic-regression", "simplification", "expression", "prefix", "rewriting", "rust"]
@@ -26,14 +26,17 @@ classifiers = [
     "Typing :: Typed",
 ]
 # The INLINE phase (simplify + conversions + validation) is the compiled Rust `simplipy._core`;
-# the OFFLINE phase (rule mining) stays pure Python. numpy is offline-only at
-# runtime, huggingface_hub powers asset resolution, platformdirs resolves the asset cache directory.
+# the OFFLINE phase (rule mining) stays pure Python. numpy/mpmath/scipy are offline-only at
+# runtime (mining + sort promotion), huggingface_hub powers asset resolution, platformdirs
+# resolves the asset cache directory.
 dependencies = [
     "filelock",
     "huggingface_hub",
+    "mpmath",
     "numpy",
     "platformdirs",
     "pyyaml",
+    "scipy",
     "tqdm",
 ]
 
@@ -94,17 +97,32 @@ exclude = [
 	"env",
 	".env",
 ]
-per-file-ignores = "__init__.py:F401"
+# The promotion subpackage is a faithful, logic-exact port of an external ratified
+# soundness certifier; its numeric style (short names, inline statements) is preserved
+# verbatim so the port cannot drift from the reference. Only style codes are relaxed.
+per-file-ignores = [
+    "__init__.py:F401",
+    "src/simplipy/promotion/*:E741,E702,E731,E126,E127,E128,E131,E122,F401,F841",
+]
 
 
 [tool.mypy]
 no_implicit_optional = false
 disallow_untyped_defs = true
 disallow_incomplete_defs = true
 explicit_package_bases = true
-exclude = "(.venv|tests/|dev/)"
+# The promotion subpackage is a verbatim port of external numeric code; annotating its
+# ~80 helper functions would edit ratified logic, so it is excluded from strict typing.
+exclude = "(.venv|tests/|dev/|src/simplipy/promotion/)"
 ignore_missing_imports = true
 
+# The promotion subpackage is a verbatim port of external numeric code; annotating its
+# ~80 helper functions would edit ratified logic, so its errors are ignored even when
+# reached via an import from the typed engine.
+[[tool.mypy.overrides]]
+module = "simplipy.promotion.*"
+ignore_errors = true
+
 
 [tool.pytest.ini_options]
 markers = [

src/simplipy/__main__.py

@@ -97,7 +97,8 @@ def main(argv: str = None) -> None:
                 'dummy_variables', 'extra_internal_terms', 'n_samples',
                 'constants_fit_challenges', 'constants_fit_retries', 'rtol', 'atol',
                 'min_informative', 'seed', 'confirm', 'source_sample_per_length',
-                'candidate_fold_filter', 'relaxed_kruskal', 'prune', 'proposals'}
+                'candidate_fold_filter', 'relaxed_kruskal', 'prune', 'proposals',
+                'promote_sorts'}
             unknown_keys = sorted(set(rule_finding_config) - known_keys)
             if unknown_keys:
                 print(f'Error: unknown key(s) in {args.config}: {", ".join(unknown_keys)}. '
@@ -123,6 +124,7 @@ def main(argv: str = None) -> None:
                 candidate_fold_filter=rule_finding_config.get('candidate_fold_filter', True),
                 relaxed_kruskal=rule_finding_config.get('relaxed_kruskal', True),
                 proposals=rule_finding_config.get('proposals', None),
+                promote_sorts=rule_finding_config.get('promote_sorts', False),
                 output_file=args.output_file,
                 save_every=args.save_every,
                 reset_rules=args.reset_rules,

src/simplipy/engine.py

@@ -837,7 +837,8 @@ def _find_rules_native(
             relaxed_kruskal: bool = True,
             provenance: dict | None = None,
             proposal_entries: list[tuple[tuple[str, ...], tuple[str, ...] | None]] | None = None,
-            leaf_nodes: list[str] | None = None) -> None:
+            leaf_nodes: list[str] | None = None,
+            promote_sorts: bool = False) -> None:
         """Phase 2 of :meth:`find_rules` on the compiled Rust core (``simplipy._core``).
 
         Mirrors the pure-Python worker pool, but correctly against the core: per source
@@ -937,6 +938,21 @@ def _find_rules_native(
             self.prune_covered_rules(verbose=verbose)
         elif prune:
             self.prune_redundant_rules(verbose=verbose)
+        # Sort promotion: re-certify every rule (mined + proposed) at the stronger `_`/`!`
+        # sorts and ship it at the strongest sound one (see `simplipy.promotion`). Runs AFTER
+        # the prune so promotion works on the already-reduced rule set (the promotion carries
+        # its own subsumption/derivability refund for the instances a promoted rule newly
+        # covers). Emits the deployment-strength ruleset directly.
+        if promote_sorts and not interrupted():
+            from .promotion import promote
+            kept, promotion_report = promote(self.simplification_rules, self)
+            self.simplification_rules = [(tuple(lhs), tuple(rhs)) for lhs, rhs in kept]
+            self.compile_rules()
+            self._core.set_rules([(list(lhs), list(rhs)) for lhs, rhs in self.simplification_rules])
+            if verbose:
+                print(f'Sort promotion: {promotion_report.get("stage_counts")}')
+            if provenance is not None:
+                provenance['sort_promotion'] = promotion_report.get('stage_counts')
         if output_file is not None:
             with open(output_file, 'w') as file:
                 json.dump(self.simplification_rules, file, indent=4)
@@ -1390,7 +1406,8 @@ def find_rules(
             source_sample_per_length: dict[int, int] | None = None,
             candidate_fold_filter: bool = True,
             relaxed_kruskal: bool = True,
-            proposals: str | list | dict | None = None) -> None:
+            proposals: str | list | dict | None = None,
+            promote_sorts: bool = False) -> None:
         """Systematically discovers new simplification rules.
 
         This powerful method automates the discovery of simplification rules.
@@ -1647,6 +1664,7 @@ def _default_dummy_variables() -> list[str]:
                 provenance=provenance,
                 proposal_entries=proposal_entries,
                 leaf_nodes=leaf_nodes,
+                promote_sorts=promote_sorts,
             )
         finally:
             signal.signal(signal.SIGINT, old_handler)

src/simplipy/promotion/__init__.py

@@ -0,0 +1,87 @@
+# mypy: ignore-errors
+"""Post-mine sort promotion.
+
+The miner emits every rule at the conservative ``?`` (variable-leaf) sort. This pass
+re-certifies each rule at the stronger sorts and ships it at the strongest SOUND one:
+
+  ``_``  arbitrary-subtree (pointwise Dirac bar over the atom lattice, both directions),
+  ``!``  certified-finite subtree (the finite-only bar, enforced by a match-time
+         defined-and-finite-a.e. certificate),
+  ``?``  variable-leaf (the fallback: what the mine already certified).
+
+Five stages, matching the reference pipeline exactly:
+  1. pointwise ``_``-bar on const-free wildcard rules,
+  2. const-bearing witness-map ``_``-bar,
+  3. exact-arbiter overturn of finite-draw demotions (f64 saturation is not authoritative),
+  4. apply ``?``->``_`` for the promoted set and refund the now-derivable instances,
+  5. the ``_``->``!``->``?`` ladder on the enriched atom lattice, with the moving-spike
+     structural refusal.
+
+Promotion is fail-safe: a rule that cannot be certified at a stronger sort ships at ``?`` and
+loses only composite-subtree recall, never soundness.
+"""
+import numpy as np
+
+from . import _f64_eval, _pointwise, _const_bearing, _overturn, _refund, _ladder
+
+
+def promote(rules, engine, *, run_positive_controls=True):
+    """Assign each ``?``-sorted mined rule its strongest sound sort; prune derivable rules.
+
+    ``rules``: iterable of (lhs, rhs) prefix-token sequences, all ``?``-sorted.
+    ``engine``: the ``SimpliPyEngine`` whose operator realizations define the semantics.
+    Returns ``(kept_rules, report)`` where ``kept_rules`` is a list of ``[lhs, rhs]`` lists.
+    """
+    _f64_eval.configure(engine)
+    rules = [(tuple(l), tuple(r)) for l, r in rules]
+
+    # STAGE 1 -- pointwise `_`-bar on const-free wildcard rules.
+    rng1 = np.random.default_rng(_pointwise.SEED)
+    scoped_cf = [(l, r) for l, r in rules
+                 if _pointwise.wildcards(l) and _pointwise.is_const_free(list(l) + list(r))]
+    pw = {'PROMOTE': [], 'DEMOTE': [], 'UNDECIDED': [], 'EVAL-ERR': []}
+    for lhs, rhs in scoped_cf:
+        ws = _pointwise.wildcards(list(lhs) + list(rhs))
+        v, info = _pointwise.judge(list(lhs), list(rhs), _pointwise.valuations_for(ws, rng1))
+        pw[v].append((lhs, rhs, info))
+
+    # STAGE 2 -- const-bearing witness-map bar.
+    rng2 = np.random.default_rng(_const_bearing.SEED)
+    scoped_cb = [(l, r) for l, r in rules
+                 if _pointwise.wildcards(list(l)) and '<constant>' in (list(l) + list(r))]
+    cb = {'PROMOTE': [], 'DEMOTE': [], 'NO-WITNESS': [], 'EVAL-ERR': []}
+    for lhs, rhs in scoped_cb:
+        v, info = _const_bearing.certify_rule(lhs, rhs, rng2)
+        cb[v].append((lhs, rhs, info))
+
+    # STAGE 3 -- exact-arbiter overturn of finite-draw demotions. A kill at an ATOM valuation
+    # is exact special-value algebra; a kill at a FINITE draw is f64 evidence that may be pure
+    # saturation (atanh(tanh(37)) since tanh(37) == 1.0), so it is re-judged at high precision.
+    rng3 = np.random.default_rng(_overturn.SEED)
+    finite_kills = [(l, r, info) for l, r, info in pw['DEMOTE']
+                    if not all(v in _pointwise.ATOMS for v in info[0].values())]
+    overturned = []
+    for lhs, rhs, info in finite_kills:
+        ws = _pointwise.wildcards(list(lhs) + list(rhs))
+        v, _kill = _overturn.judge_exact(list(lhs), list(rhs), _pointwise.valuations_for(ws, rng3))
+        if v == 'PROMOTE':
+            overturned.append((lhs, rhs, info))
+    ot_keys = {(tuple(l), tuple(r)) for l, r, _ in overturned}
+    pw['DEMOTE'] = [x for x in pw['DEMOTE'] if (tuple(x[0]), tuple(x[1])) not in ot_keys]
+    pw['PROMOTE'] = pw['PROMOTE'] + [(l, r, 'overturned-by-exact-arbiter') for l, r, _ in overturned]
+
+    # STAGE 4 -- apply ?->_ for the promoted set, then refund the derivable instances.
+    promote_set = {(tuple(l), tuple(r)) for l, r, *_ in pw['PROMOTE']} \
+        | {(tuple(l), tuple(r)) for l, r, *_ in cb['PROMOTE']}
+    sorted_rules = _refund.refund(rules, engine._operators_config, promote_set)
+
+    # STAGE 5 -- the _->!->? ladder on the enriched lattice + moving-spike refusal.
+    kept, report = _ladder.promote_rules(sorted_rules, engine,
+                                         run_positive_controls=run_positive_controls)
+    report = dict(report)
+    report['stage_counts'] = {
+        'pointwise_promote': len(pw['PROMOTE']), 'pointwise_demote': len(pw['DEMOTE']),
+        'cb_promote': len(cb['PROMOTE']), 'overturned': len(overturned),
+        'after_refund': len(sorted_rules), 'final': len(kept),
+    }
+    return kept, report