From 1fa7d4542b49382a1b369fe00803f96c4777da9c Mon Sep 17 00:00:00 2001 From: psaegert Date: Tue, 21 Jul 2026 16:21:35 +0200 Subject: [PATCH 1/4] feat(mining): native post-mine sort promotion (simplipy.promotion) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the sort-promotion pass that upgrades every mined/proposed rule from the conservative ? (variable-leaf) sort to the strongest SOUND sort — _ (arbitrary subtree) or ! (certified-finite subtree) — via a five-stage certifier: pointwise _-bar on an atom lattice, const-bearing witness-map bar, exact-arbiter overturn of finite-draw demotions, subsumption/derivability refund, and the _->!->? ladder with the moving-spike structural refusal. Promotion is fail-safe: an uncertifiable rule ships at ? and loses only composite-subtree recall, never soundness. find_rules gains an opt-in promote_sorts flag (default False; CLI config key). When set, the pass runs after the prune and emits deployment-strength sorts directly. Validated: on the (4,3) rule set the native pass output is gate-clean (0 KILL, 0 ENGINE-MISALIGN) and passes the independent deployed-realization monitor with 0 violations across all seeds. End-to-end find_rules(promote_sorts=True) on (2,1) produces 602 rules (486 promoted to _/!), gate-clean. The promotion modules are a faithful, logic-exact port of an external ratified certifier; lint/type checks are relaxed on them so the port cannot drift. Adds mpmath + scipy as offline-mining dependencies. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w --- .pre-commit-config.yaml | 2 +- pyproject.toml | 26 +- src/simplipy/__main__.py | 4 +- src/simplipy/engine.py | 22 +- src/simplipy/promotion/__init__.py | 87 +++ src/simplipy/promotion/_const_bearing.py | 212 +++++++ src/simplipy/promotion/_f64_eval.py | 216 +++++++ src/simplipy/promotion/_hp_equiv.py | 302 +++++++++ src/simplipy/promotion/_ladder.py | 739 +++++++++++++++++++++++ src/simplipy/promotion/_overturn.py | 77 +++ src/simplipy/promotion/_pointwise.py | 268 ++++++++ src/simplipy/promotion/_refund.py | 139 +++++ 12 files changed, 2086 insertions(+), 8 deletions(-) create mode 100644 src/simplipy/promotion/__init__.py create mode 100644 src/simplipy/promotion/_const_bearing.py create mode 100644 src/simplipy/promotion/_f64_eval.py create mode 100644 src/simplipy/promotion/_hp_equiv.py create mode 100644 src/simplipy/promotion/_ladder.py create mode 100644 src/simplipy/promotion/_overturn.py create mode 100644 src/simplipy/promotion/_pointwise.py create mode 100644 src/simplipy/promotion/_refund.py diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 3a9f0c0..288b023 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -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/) diff --git a/pyproject.toml b/pyproject.toml index 676344f..85b415d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -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,7 +97,13 @@ 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] @@ -102,9 +111,18 @@ 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 = [ diff --git a/src/simplipy/__main__.py b/src/simplipy/__main__.py index 9095ed6..f860544 100644 --- a/src/simplipy/__main__.py +++ b/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, diff --git a/src/simplipy/engine.py b/src/simplipy/engine.py index 2416cf7..dadd694 100644 --- a/src/simplipy/engine.py +++ b/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) diff --git a/src/simplipy/promotion/__init__.py b/src/simplipy/promotion/__init__.py new file mode 100644 index 0000000..d813d58 --- /dev/null +++ b/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 '' 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 diff --git a/src/simplipy/promotion/_const_bearing.py b/src/simplipy/promotion/_const_bearing.py new file mode 100644 index 0000000..c32cf07 --- /dev/null +++ b/src/simplipy/promotion/_const_bearing.py @@ -0,0 +1,212 @@ +# mypy: ignore-errors +"""Const-bearing witness-map certifier for wildcard rewrite rules. + +Certifies a rewrite ``S -> T`` whose subtrees carry ```` slots. The soundness +question, per rule, is:: + + for all c_s exists c_t for all v: S[v]_{c_s} = T[v]_{c_t} + +pointwise over R u {+-0, +-1, +-inf, nan} (nan = nan counts as equal). The target +constants c_t are fixed per application: c_t may depend on the source constants c_s but +never on the wildcard valuation v. + +MECHANISM: + 1. Draw c_s vectors adversarially: integer atoms first ({-2,-1,0,1,2,3}), because the + singular behaviour that breaks a candidate identity concentrates on the integers, + then half-integers and continuous draws. + 2. Find the existential witness c_t: a STRUCTURAL MENU (c1*c2, c1+c2, +-sqrt|c1|, 1/c1, + ...), exact for the constant-merge/absorb family that dominates recall, then a + bounded numeric least-squares fallback fitted on finite wildcard draws. + 3. Hold the INSTANTIATED pair (constants bound, wildcards free) to the SAME pointwise + atom bar as the const-free certifier (``_pointwise.judge``). + +VERDICTS: + PROMOTE -- every sampled c_s has a witness passing all valuations (sampling-based, + so acceptance is falsification-survival at these draws, with the + false-promote rate bounded by the sample count). + DEMOTE -- some c_s where a witness reproduces the finite behaviour but dies at an + atom, or every tried witness dies; recorded with the killing + (c_s, c_t, valuation). + NO-WITNESS -- no candidate even reproduces the finite behaviour (solver failure or a + dead source); fail-safe. + +DEMOTE and NO-WITNESS both cost only composite-binding recall (the rule ships in its +weaker sort, exactly what its certification established). PROMOTE is the only verdict +that changes deployment. +""" +import numpy as np + +from ._pointwise import judge, valuations_for, wildcards +from ._f64_eval import evaluate + +SEED = 20260717 +# The constant axis gets atom probes too -- appended at the END so the `[:5]` product +# slice below (used for the two-constant case) keeps its original coverage. Constants +# range over the reals, so the transcendental spike points (pi/2, pi, e) join as f64 +# renderings; numpy's saturation (sin(f64 pi/2) == 1.0) usefully mimics the real spike +# at the atom. +CS_ATOMS = [-2.0, -1.0, 0.0, 1.0, 2.0, 3.0, 0.5, -0.5, -3.0, 5.0, -5.0, + 1.5707963267948966, -1.5707963267948966, 3.141592653589793, 2.718281828459045] +N_CS_RAND = 4 +N_V_FIT = 48 # finite wildcard draws for witness fitting/screening +FIT_TOL = 1e-7 # a witness must reproduce finite behaviour to this rel tol +MAX_SOLVER_STARTS = 6 + + +def bind(tokens, consts): + out, k = [], 0 + for t in tokens: + if t == '': + v = consts[k]; k += 1 + out.append(repr(float(v)) if v >= 0 else f'({float(v)!r})') + else: + out.append(t) + return out + + +def n_consts(tokens): + return sum(1 for t in tokens if t == '') + + +def eval_on(tokens, ws, V): + """Evaluate tokens (constants already bound) on wildcard-value matrix V (n, len(ws)).""" + env = {w: V[:, i] for i, w in enumerate(ws)} if ws else {'__d__': np.zeros(len(V))} + with np.errstate(all='ignore'): + return np.broadcast_to(np.asarray(evaluate(list(tokens), env), np.float64), (len(V),)).copy() + + +def finite_match(y_src, y_tgt): + """Does the target reproduce the source's FINITE behaviour (and its nan pattern) on the fit + draws? Necessary screen before the atom bar; nan-pattern mismatch on finite draws is already + a pointwise kill.""" + sn, tn = np.isnan(y_src), np.isnan(y_tgt) + if (sn != tn).any(): + return False + both = ~sn + if not both.any(): + return True # nan-everywhere on finite draws: pattern agrees + a, b = y_src[both], y_tgt[both] + fin = np.isfinite(a) & np.isfinite(b) + if (np.isinf(a) != np.isinf(b)).any() or (np.isinf(a) & (a != b))[fin == False].any(): # noqa: E712 + return False + rel = np.abs(a[fin] - b[fin]) / np.maximum(1.0, np.maximum(np.abs(a[fin]), np.abs(b[fin]))) + return bool((rel <= FIT_TOL).all()) + + +def witness_menu(cs, nt): + """Structural candidates for c_t given c_s. Exact for the merge/absorb families.""" + cs = list(cs) + singles = set() + for c in cs: + singles.update([c, -c]) + if c != 0: + singles.update([1.0 / c]) + if c >= 0: + singles.add(float(np.sqrt(c))) + singles.update([float(np.sqrt(abs(c))), -float(np.sqrt(abs(c))), c * c]) + if len(cs) >= 2: + a, b = cs[0], cs[1] + singles.update([a * b, a + b, a - b, b - a]) + if b != 0: + singles.add(a / b) + if a != 0: + singles.add(b / a) + pool = sorted({float(v) for v in singles if np.isfinite(v)}) + if nt == 1: + return [[v] for v in pool] + if nt == 2: + base = [[a, b] for a in pool[:8] for b in pool[:8]] + return base[:64] + return [list(cs[:nt]) + [1.0] * max(0, nt - len(cs))] + + +def solve_witness(lhs_b, rhs, ws, nt, y_src, V, rng): + """Bounded least-squares fallback: fit c_t so T reproduces y_src on the finite draws.""" + try: + from scipy.optimize import least_squares + except ImportError: + return [] + defined = ~np.isnan(y_src) & np.isfinite(y_src) + if defined.sum() < max(4, nt + 2): + return [] + Vd, yd = V[defined], y_src[defined] + + def resid(theta): + y = eval_on(bind(rhs, theta), ws, Vd) + bad = ~np.isfinite(y) + y = np.where(bad, 1e12, y) + return (y - yd) / np.maximum(1.0, np.abs(yd)) + + out = [] + for _ in range(MAX_SOLVER_STARTS): + x0 = rng.normal(0, 2, nt) + try: + r = least_squares(resid, x0, method='lm', max_nfev=200) + except Exception: + continue + if r.success and np.max(np.abs(r.fun)) < FIT_TOL: + out.append([float(v) for v in r.x]) + return out + + +def certify_rule(lhs, rhs, rng, judge_fn=None, vals_override=None): + """The `forall c_s exists c_t` certifier. `judge_fn` and `vals_override` let a caller + hold the instantiated pairs to a different bar (e.g. an atom-only, extension-tolerant + valuation set) instead of the default `_pointwise.judge` bar -- the witness machinery + is identical.""" + if judge_fn is None: + judge_fn = judge + ws = wildcards(list(lhs) + list(rhs)) + ns, nt = n_consts(lhs), n_consts(rhs) + cs_draws = [[c] * ns if ns == 1 else None for c in CS_ATOMS] + cs_list = ([[c] for c in CS_ATOMS] if ns == 1 else + [[a, b] for a in CS_ATOMS[:5] for b in (-2.0, 1.0, 2.0)] if ns == 2 else + [list(rng.normal(0, 2, ns)) for _ in range(8)]) + cs_list = cs_list + [list(np.round(rng.normal(0, 3, ns), 4)) for _ in range(N_CS_RAND)] + V = np.column_stack([np.concatenate([rng.normal(0, 2, N_V_FIT // 2), + rng.uniform(-30, 30, N_V_FIT - N_V_FIT // 2)]) + for _ in ws]) if ws else np.zeros((N_V_FIT, 1)) + vals = vals_override if vals_override is not None else valuations_for(ws, rng) + n_no_witness = 0 + for cs in cs_list: + lhs_b = bind(lhs, cs) + try: + y_src = eval_on(lhs_b, ws, V) + except Exception as ex: + return 'EVAL-ERR', f'{type(ex).__name__}: {ex}' + found, atom_kill = None, None + cands = witness_menu(cs, nt) if nt else [[]] + seen_finite_match = False + for ct in cands: + try: + y_t = eval_on(bind(rhs, ct), ws, V) + except Exception: + continue + if not finite_match(y_src, y_t): + continue + seen_finite_match = True + v, info = judge_fn(bind(lhs, cs), bind(rhs, ct), vals) + if v in ('PROMOTE', 'PASS'): + found = ct + break + atom_kill = (cs, ct, info) + if found is None and not seen_finite_match and nt: + for ct in solve_witness(lhs_b, rhs, ws, nt, y_src, V, rng): + y_t = eval_on(bind(rhs, ct), ws, V) + if not finite_match(y_src, y_t): + continue + seen_finite_match = True + v, info = judge_fn(bind(lhs, cs), bind(rhs, ct), vals) + if v in ('PROMOTE', 'PASS'): + found = ct + break + atom_kill = (cs, ct, info) + if found is None: + if atom_kill is not None: + return 'DEMOTE', atom_kill + n_no_witness += 1 + if n_no_witness >= 2: # dead source / unfittable family: fail-safe, stays leaf-sort + return 'NO-WITNESS', cs + if n_no_witness: + return 'NO-WITNESS', None + return 'PROMOTE', None diff --git a/src/simplipy/promotion/_f64_eval.py b/src/simplipy/promotion/_f64_eval.py new file mode 100644 index 0000000..b3c9c7d --- /dev/null +++ b/src/simplipy/promotion/_f64_eval.py @@ -0,0 +1,216 @@ +# mypy: ignore-errors +"""Independent f64 oracle for domain-extension checks on rewrite rules. + +This module decides, for a candidate rule ``lhs -> rhs``, whether the rewrite +turns an UNDEFINED point into a DEFINED one (a "domain extension"). It does so +with an oracle that shares no code with the interval-arithmetic engine: the +deployed numpy realizations (``simplipy.operators.*``, resolved through the +engine's own ``realization`` fields), evaluated pointwise on sampled inputs. + +Why an independent oracle. Interval evaluation pushes ONE interval through the +whole tree, so every variable is bound to the SAME interval and only the +diagonal cube ``[lo, hi]^n`` is ever explored. A NaN region whose shape is +relational (e.g. ``x0 < x1``) is therefore invisible to it. Sampling each +variable INDEPENDENTLY has no such blind spot, so this oracle can detect +extensions the interval engine cannot. + +The verdict is asymmetric. Pointwise sampling is a LOWER bound on domain +extension: a narrow band (a constant inside a thin sliver, or a NaN region +thinner than the sample spacing) can be missed. So a detected extension is +real (up to the f64 saturation caveat below), but the absence of a detected +extension is only "no extension at this sampling density", never a proof of +soundness. + +Known blind spot of THIS oracle: f64 saturation. ``acosh(abs(tanh x))`` is NaN +in exact arithmetic (``tanh x < 1`` strictly) but reads ``0.0`` in f64 once +``tanh`` saturates to ``1.0``; numpy then calls the source defined and no +extension is reported. That family is out of scope here and needs an +extended-precision (mpmath) evaluator instead. It is documented, not silently +swallowed. +""" +import json +import math +import os +from typing import TYPE_CHECKING + +import numpy as np + +if TYPE_CHECKING: + from ..engine import SimpliPyEngine + +N_PTS = int(os.environ.get('N_PTS', 200_000)) +THRESH = float(os.environ.get('THRESH', 0.005)) # positive-measure floor +SEED = 20260716 + + +def build_oracle(engine: "SimpliPyEngine"): + """Resolve the engine's ``realization`` strings to the deployed numpy callables. + + Nothing here touches the Rust core: ``simplipy.operators`` is pure + Python/numpy, and it is what the engine names as each token's realization. + Infix realizations (``+ - * /``) map to the corresponding ``operator`` + builtins; ``simplipy.operators.`` realizations resolve by attribute + lookup. An unrecognised realization raises, so no token is silently dropped. + + Returns ``(arity, fns)``: the engine's operator-arity table and a mapping + from token to its numpy callable. + """ + import operator as _op + + from .. import operators as spo + + infix = {'+': _op.add, '-': _op.sub, '*': _op.mul, '/': _op.truediv} + fns = {} + for tok, real in engine.operator_realizations.items(): + if real in infix: + fns[tok] = infix[real] + elif real.startswith('simplipy.operators.'): + fns[tok] = getattr(spo, real.rsplit('.', 1)[1]) + else: + raise RuntimeError(f'unresolved realization for {tok!r}: {real!r}') + return engine.operator_arity, fns + + +# Populated by ``configure(engine)`` (or by assigning the result of +# ``build_oracle`` to these names) before any evaluation. Kept as module-level +# state so the pure evaluation helpers below stay free of oracle plumbing. +ARITY: dict = {} +FNS: dict = {} + + +def configure(engine: "SimpliPyEngine"): + """Install the oracle for ``engine`` into the module globals. + + Resolves ``engine`` through :func:`build_oracle` and binds ``ARITY`` and + ``FNS`` so that :func:`evaluate`, :func:`variables`, :func:`domain_extension` + and :func:`audit` operate against that engine's realizations. Must be called + before those functions are used. + """ + # Mutate the dicts IN PLACE rather than rebinding: sibling modules bind these + # objects at import time (``from ._f64_eval import ARITY``), so a rebind would + # leave them pointing at the empty originals. In-place update keeps every holder + # of the object in sync. + ar, fns = build_oracle(engine) + ARITY.clear(); ARITY.update(ar) + FNS.clear(); FNS.update(fns) + return ARITY, FNS + + +LITERALS = { + '0': 0.0, '1': 1.0, '(-1)': -1.0, 'np.e': math.e, 'np.pi': math.pi, + 'float("inf")': math.inf, 'float("-inf")': -math.inf, 'float("nan")': math.nan, +} + + +def _num(tok): + try: + return float(tok.strip('()')) + except ValueError: + return None + + +def evaluate(tokens, env): + """Evaluate a prefix expression on numpy arrays via the deployed realizations.""" + pos = 0 + + def walk(): + nonlocal pos + tok = tokens[pos] + pos += 1 + if tok in ARITY: + args = [walk() for _ in range(ARITY[tok])] + with np.errstate(all='ignore'): + return FNS[tok](*args) + if tok in env: + return env[tok] + if tok in LITERALS: + return np.full_like(next(iter(env.values())), LITERALS[tok]) + v = _num(tok) + if v is None: + raise KeyError(f'unknown leaf token: {tok!r}') + return np.full_like(next(iter(env.values())), v) + + out = walk() + if pos != len(tokens): + raise ValueError(f'trailing tokens in {tokens!r}') + return np.asarray(out, dtype=np.float64) + + +def variables(tokens): + """Every leaf that is not an operator, a literal, a number or ```` is a VARIABLE. + + Defined by EXCLUSION on purpose. Matching a name pattern instead (``x0``, + say) is unsafe: rules may use ``_0``/``_1`` style wildcard leaf names, so a + name-pattern match would classify them as variable-free and skip them + silently. An unknown leaf must become a loud ``KeyError`` in ``evaluate``, + never an empty set here. + """ + return sorted({t for t in tokens + if t not in ARITY and t not in LITERALS + and t != '' and _num(t) is None}) + + +def sample_env(varnames, rng): + """Broad INDEPENDENT draws per variable -- the axis on which the interval engine is blind. + + Independent (not diagonal) is the whole reason this oracle can see relational NaN regions like + `x0 < x1`. The mixture keeps mass near the +-1 branch points where inverse round-trips flip, + while the wide arm reaches the tails. + """ + env = {} + for v in varnames: + u = rng.random(N_PTS) + x = np.where(u < 0.5, rng.uniform(-2.0, 2.0, N_PTS), rng.uniform(-8.0, 8.0, N_PTS)) + env[v] = x + return env + + +def domain_extension(lhs, rhs): + """Fraction of rows where the SOURCE is undefined but the TARGET is defined. + + This is the asymmetric-accept principle's undefined side: filling a measure-ZERO hole is a + removable singularity and licit; filling a POSITIVE-measure region invents a function. + Returns None if the rule is out of this oracle's scope. + """ + varnames = variables(list(lhs) + list(rhs)) + if not varnames: + return None # variable-free: no x-measure to speak of + rng = np.random.default_rng(SEED) + env = sample_env(varnames, rng) + s = evaluate(list(lhs), env) + t = evaluate(list(rhs), env) + return float(np.mean(np.isnan(s) & ~np.isnan(t))) + + +def _pairs(d): + return list(d.items()) if isinstance(d, dict) else [(r[0], r[1]) for r in d] + + +def load(path): + out = {} + for k, v in _pairs(json.load(open(path))): + lhs = tuple(k.split()) if isinstance(k, str) else tuple(k) + rhs = tuple(v.split()) if isinstance(v, str) else tuple(v) + out[lhs] = rhs + return out + + +def audit(path, label): + rules = load(path) + scope = {k: v for k, v in rules.items() + if '' not in k and '' not in v} + hits, skipped = [], 0 + for lhs, rhs in scope.items(): + try: + f = domain_extension(lhs, rhs) + except Exception as e: # never silently: a skip is REPORTED + skipped += 1 + if skipped <= 3: + print(f' [skip] {" ".join(lhs)} -> {" ".join(rhs)}: {type(e).__name__}: {e}') + continue + if f is not None and f > THRESH: + hits.append((lhs, rhs, f)) + hits.sort(key=lambda r: -r[2]) + print(f'{label:18s} {len(rules):5,d} rules | {len(scope):5,d} const-free ' + f'| {len(hits):3d} EXTEND a domain | {skipped} un-evaluable') + return hits, len(scope), skipped diff --git a/src/simplipy/promotion/_hp_equiv.py b/src/simplipy/promotion/_hp_equiv.py new file mode 100644 index 0000000..9d59cd2 --- /dev/null +++ b/src/simplipy/promotion/_hp_equiv.py @@ -0,0 +1,302 @@ +# mypy: ignore-errors +"""INDEPENDENT high-precision equivalence checker (mpmath, default 200 dps) for auditing +candidate rules and engine simplifications. Deliberately a SEPARATE implementation from the +Rust core (f64 numeric.rs + astro-float hiprec.rs) so it can cross-verify soundness. + +Semantics match the deployment reference (numpy f64 + C99 libm), lifted to high precision: + * generic equivalence: a rule/pair holds iff on every row where the SOURCE (lhs) is + finite, the CANDIDATE (rhs) matches within (rtol, atol); source-nonfinite rows are + domain-extendable (x/x -> 1). Enough finite rows must bind (min_binding). + * const-free lhs & rhs -> direct check. + * const-bearing -> for several lhs-constant draws (challenges x sign combos), FIT the + rhs constants (numpy lstsq seed + scipy refine) and require the generic-equivalence + gate to hold at the fitted constants for EVERY draw. + +Public: equiv(lhs, rhs, dps=200, ...) -> dict(ok, worst_sep, n_binding, reason). +Wildcards `_k` are treated as variables x{k}. `` leaves bind to fitted params. +""" +import numpy as np +from mpmath import mp, mpf, isnan, isinf, nan, inf + + +def _num(x): + return mpf(str(x)) if not isinstance(x, mpf) else x + + +LEAF = { + 'np.e': lambda: mp.e, 'np.pi': lambda: mp.pi, '(-1)': lambda: mpf(-1), + 'float("inf")': lambda: mpf('inf'), 'float("-inf")': lambda: mpf('-inf'), + 'float("nan")': lambda: mpf('nan'), +} + + +def _odd_root(x, n): + if isnan(x): + return nan + return -((-x) ** (mpf(1) / n)) if x < 0 else x ** (mpf(1) / n) + + +def _even_root(x, n): + if isnan(x) or x < 0: + return nan + return x ** (mpf(1) / n) + + +def _pow(a, b): + # C99/numpy pow, high precision + if (not isnan(a)) and a == 1: + return mpf(1) + if (not isnan(b)) and b == 0: + return mpf(1) + if isnan(a) or isnan(b): + return nan + if a == 0: + return inf if b < 0 else mpf(0) + if isinf(a): + # |a| = inf > 1, so an infinite exponent depends only on sign(b) (parity is moot). + if isinf(b): + return inf if b > 0 else mpf(0) + if a > 0: + return inf if b > 0 else mpf(0) + # a == -inf, b finite: parity only matters for integer b + if b == int(b): + m = inf if b > 0 else mpf(0) + return -m if int(b) % 2 else m + # A NEGATIVE base (including -inf) with a non-integer exponent is UNDEFINED over + # the reals, so return nan. Using nan here (rather than the C99 pow branch that + # returns +inf for a negative base) keeps this atom consistent with the real + # even-root convention pow1_4(-inf) == nan, so equivalent forms such as + # `pow x div4 1` and `pow1_4 x` agree at the -inf atom instead of one of them + # reading as a domain shrink. + return nan + if isinf(b): + # numpy: infinite exponent depends only on |a| vs 1, sign of a ignored. + m = abs(a) + if m == 1: + return mpf(1) + return inf if ((m > 1) == (b > 0)) else mpf(0) + if a < 0: + if isinf(b) or b != int(b): + return nan + m = (-a) ** b + return -m if int(b) % 2 else m + try: + return a ** b + except (OverflowError, ValueError): + return inf + + +UN = { + 'neg': lambda x: -x, 'abs': lambda x: abs(x), + 'inv': lambda x: (inf if x >= 0 else -inf) if x == 0 else 1 / x, + 'mult2': lambda x: 2 * x, 'mult3': lambda x: 3 * x, 'mult4': lambda x: 4 * x, 'mult5': lambda x: 5 * x, + 'div2': lambda x: x / 2, 'div3': lambda x: x / 3, 'div4': lambda x: x / 4, 'div5': lambda x: x / 5, + 'pow2': lambda x: x ** 2, 'pow3': lambda x: x ** 3, 'pow4': lambda x: x ** 4, 'pow5': lambda x: x ** 5, + 'pow1_2': lambda x: _even_root(x, 2), 'pow1_4': lambda x: _even_root(x, 4), + 'pow1_3': lambda x: _odd_root(x, 3), 'pow1_5': lambda x: _odd_root(x, 5), + 'sin': mp.sin, 'cos': mp.cos, 'tan': mp.tan, + 'asin': lambda x: nan if abs(x) > 1 else mp.asin(x), + 'acos': lambda x: nan if abs(x) > 1 else mp.acos(x), + 'atan': mp.atan, 'sinh': mp.sinh, 'cosh': mp.cosh, 'tanh': mp.tanh, + 'asinh': mp.asinh, + 'acosh': lambda x: nan if x < 1 else mp.acosh(x), + 'atanh': lambda x: nan if abs(x) > 1 else ((inf if x > 0 else -inf) if abs(x) == 1 else mp.atanh(x)), + 'exp': mp.exp, 'log': lambda x: (-inf) if x == 0 else (nan if x < 0 else mp.log(x)), +} +BIN = { + '+': lambda a, b: a + b, '-': lambda a, b: a - b, '*': lambda a, b: a * b, + '/': lambda a, b: ((nan if a == 0 else (-inf if (a < 0) != (b < 0) else inf)) if b == 0 else a / b), + 'pow': _pow, +} + + +def _ev(tokens, i, env, consts, ci): + t = tokens[i] + i += 1 + if t in UN: + v, i, ci = _ev(tokens, i, env, consts, ci) + if isnan(v): + return nan, i, ci + try: + r = UN[t](v) + except (OverflowError, ValueError, ZeroDivisionError): + r = nan + return r, i, ci + if t in BIN: + a, i, ci = _ev(tokens, i, env, consts, ci) + b, i, ci = _ev(tokens, i, env, consts, ci) + if t == 'pow': + return _pow(a, b), i, ci + if isnan(a) or isnan(b): + return nan, i, ci + try: + r = BIN[t](a, b) + except (OverflowError, ValueError, ZeroDivisionError): + r = nan + return r, i, ci + if t == '': + v = consts[ci] + return _num(v), i, ci + 1 + if t in LEAF: + return LEAF[t](), i, ci + if t in env: + return env[t], i, ci + # numeric literal + return _num(float(t)), i, ci + + +def evaluate(tokens, env, consts): + v, j, _ = _ev(list(tokens), 0, dict(env), list(consts), 0) + return v + + +def _vars_in(tokens): + vs = set() + for t in tokens: + if t.startswith('x') and t[1:].isdigit(): + vs.add(t) + elif t.startswith('_') and t[1:].isdigit(): + vs.add(t) + return sorted(vs) + + +def _n_const(tokens): + return sum(1 for t in tokens if t == '') + + +def _wild_to_var(tokens): + return ['x' + t[1:] if (t.startswith('_') and t[1:].isdigit()) else t for t in tokens] + + +def equiv(lhs, rhs, dps=200, n_rows=48, challenges=6, seed=0, rtol=1e-12, atol=1e-15, + min_binding=6): + """Independent generic-equivalence verdict for lhs -> rhs. Returns a dict.""" + mp.dps = dps + lhs = _wild_to_var(list(lhs)) + rhs = _wild_to_var(list(rhs)) + allvars = sorted(set(_vars_in(lhs)) | set(_vars_in(rhs))) + rng = np.random.default_rng(seed) + nlc, nrc = _n_const(lhs), _n_const(rhs) + # var draws (shared across constant challenges) + Xrows = [{v: mpf(str(float(x))) for v, x in zip(allvars, rng.normal(0, 5, len(allvars)))} + for _ in range(n_rows)] or [{}] * n_rows + if not allvars: + Xrows = [{} for _ in range(n_rows)] + + worst = mpf(0) + total_binding = 0 + combos = [tuple()] if nlc == 0 else None + + def lhs_const_draws(): + if nlc == 0: + yield [] + return + for _ in range(challenges): + base = np.abs(rng.normal(0, 5, nlc)) + for signs in _sign_combos(nlc): + yield [mpf(str(float(b * s))) for b, s in zip(base, signs)] + + for lc in lhs_const_draws(): + yv = [] + rows_kept = [] + for row in Xrows: + a = evaluate(lhs, row, lc) + if isnan(a) or isinf(a): + continue + yv.append(a) + rows_kept.append(row) + if len(yv) < min_binding: + continue + total_binding += len(yv) + if nrc == 0: + for a, row in zip(yv, rows_kept): + b = evaluate(rhs, row, []) + if isnan(b) or isinf(b): + return _res(False, worst, total_binding, 'rhs nonfinite where lhs finite') + sep = abs(a - b) / max(abs(a), mpf(1)) + worst = max(worst, sep) + if worst > mpf(str(atol)) + mpf(str(rtol)): + return _res(False, worst, total_binding, 'const-free mismatch') + else: + ok, w = _fit_and_check(rhs, rows_kept, yv, nrc, rtol, atol, seed) + worst = max(worst, w) + if not ok: + return _res(False, worst, total_binding, 'no rhs constants fit this lhs draw') + if total_binding < min_binding: + return _res(None, worst, total_binding, 'insufficient finite evidence (vacuous)') + return _res(True, worst, total_binding, 'ok') + + +def _sign_combos(n): + # Measure-consistent sign grid {-1, +1}, NOT {-1, 0, +1}. C=0 is a measure-zero point + # that the constant sampler never draws; testing it would flag rules that hold for + # every random constant as false (`pow(cos(C), inf) -> 0` is 0 for all C except the + # measure-zero cos(C)=+-1 set). Magnitudes stay continuous, so any positive-measure + # falsity is still caught. Matches the reference sampler's default sign grid. + import itertools + return list(itertools.product((-1.0, 1.0), repeat=n)) + + +def _fit_and_check(rhs, rows, yv, nrc, rtol, atol, seed): + """Fit rhs constants to the lhs values yv over rows; accept if a fit reproduces yv. + Robust to power/exponential rhs (where naive least_squares stalls): a broad grid of + SIMPLE seeds (integers, simple fractions -- most true structural constants are simple) + plus random restarts, residual evaluated ONLY on rows where rhs is finite (no flat + penalty region), and a coverage requirement so a fit that matches on few rows fails.""" + from scipy.optimize import least_squares + y = np.array([float(a) for a in yv]) + n = len(y) + # FIT on moderate-magnitude rows only (a const-base pow C^x overflows float64 for the + # wide |x| the row draws span; drop the overflow-prone rows for the FIT and still + # VERIFY on ALL rows at high precision). + fit_idx = [i for i in range(n) if 1e-8 < abs(y[i]) < 1e8] + if len(fit_idx) < max(3, nrc + 1): + fit_idx = list(range(n)) + frows = [rows[i] for i in fit_idx] + fy = y[fit_idx] + + def resid(c): + out = [] + for row, ay in zip(frows, fy): + v = evaluate(rhs, row, [mpf(str(ci)) for ci in c]) + fv = float(v) if (not isnan(v) and not isinf(v)) else np.nan + out.append(0.0 if (np.isnan(fv) or abs(fv) > 1e12) else (fv - ay)) + return np.nan_to_num(np.array(out), nan=0.0, posinf=0.0, neginf=0.0) + + def finite_frac(c): + k = 0 + for row in frows: + v = evaluate(rhs, row, [mpf(str(ci)) for ci in c]) + if not (isnan(v) or isinf(v)): + k += 1 + return k / len(frows) + + SIMPLE = [0.0, 1.0, -1.0, 2.0, -2.0, 3.0, 0.5, -0.5, 1.0 / 3, 0.25, 4.0, 5.0, np.e, -np.e, + float(np.exp(-4)), float(np.exp(4)), float(np.exp(8))] + rng = np.random.default_rng(seed + 1) + seeds = [np.full(nrc, s) for s in SIMPLE] + seeds += [rng.normal(0, m, nrc) for m in (0.5, 1, 2, 4) for _ in range(4)] + best = None + for c0 in seeds: + try: + r = least_squares(resid, c0, max_nfev=300) + except Exception: + continue + # require the fit to keep rhs finite on (nearly) all binding rows + if finite_frac(r.x) < 0.9: + continue + if best is None or r.cost < best.cost: + best = r + if best is None: + return False, mpf(1) + worst = mpf(0) + for row, ay in zip(rows, yv): + v = evaluate(rhs, row, [mpf(str(ci)) for ci in best.x]) + if isnan(v) or isinf(v): + continue # rhs may extend the domain; judge only where it is finite + worst = max(worst, abs(ay - v) / max(abs(ay), mpf(1))) + return worst <= mpf('1e-7'), worst + + +def _res(ok, worst, nb, reason): + return {'ok': ok, 'worst_sep': float(worst), 'n_binding': int(nb), 'reason': reason} diff --git a/src/simplipy/promotion/_ladder.py b/src/simplipy/promotion/_ladder.py new file mode 100644 index 0000000..b2b8158 --- /dev/null +++ b/src/simplipy/promotion/_ladder.py @@ -0,0 +1,739 @@ +# mypy: ignore-errors +"""The subtree-sort promotion ladder driver: `_` -> `!` -> `?`. + +Certifies each mined rewrite rule against the strongest wildcard sort it can soundly +bind at, stepping DOWN a three-rung ladder of progressively weaker bindings when a +stronger rung's bar is not met. The atom lattice (see `._pointwise.ATOMS`: 0, +-1, +integers, half-integers, +-pi, +-e, +-inf, nan) is the finite set of exact probe points; +on it, exact value equality is required, tolerating ONLY undefined -> defined extensions +(e.g. `x/x -> 1` filling the hole at 0). A defined value may never change to a different +defined value, even on a null set. The continuum keeps measure tolerance (the sampled +jurisdiction of the miner, not this instrument). + +THREE TIERS over a rules artifact (each with its own bar, by the pushforward theorem): + + `_` (subtree sort, Dirac): the full exact-pointwise bar on the enriched atom lattice. + Failures are RESPELLED to `?` (they keep everything they were ever certified for) + and then face the `?` bar. + `?` (variable-leaf sort, identity pushforward): the atom bar -- full atom product, no + random draws (the continuum is the miner's sampled jurisdiction, not this + instrument's). Kill = defined->different-defined (value change) or defined->undefined + (domain shrink); undefined->defined is the tolerated extension. + ground (no wildcards; ``-bearing): SKELETON semantics, for-all c exists finite + c_t. Probed over the finite constant lattice (fitted constants are finite; no inf/nan + constants exist to bind): + - literal RHS: exact value equality at EVERY probed c (mpmath, high precision); + - bare `` RHS: the LHS value must be FINITE at every probed c (a finite + fitted constant must exist; nan/inf values are not constant-representable -- + e.g. `pow(c/5, nan) -> c` would invent a value for an undefined expression). + Any other RHS shape with `` is UNSUPPORTED -> conservative kill. + +Positive controls are checked first (raise on any miss). The public entry point is +`promote_rules(rules, engine)`; it returns the promoted rules plus a per-bucket report. +""" +import numpy as np + +from ._pointwise import (ATOMS, MAX_PRODUCT, judge, prefold, # noqa: E402 + substitute, eval_point, wildcards, valuations_for, + correlated_valuations) +from ._const_bearing import certify_rule # noqa: E402 +from ._hp_equiv import evaluate as hp_eval # noqa: E402 +from mpmath import mp, mpf, isnan, isinf # noqa: E402 + +SEED = 20260718 +GROUND_DRAWS = 16 # seeded finite draws on the constant axis, atop the finite atom lattice +DPS = 60 # ground expressions are special-value algebra; 60 digits is ample + +FINITE_ATOMS = [a for a in ATOMS if not a.startswith('float(')] + + +def atom_valuations(ws, rng): + """FULL atom product for the `?` bar (no random draws); sampled past MAX_PRODUCT (k>=4).""" + k = len(ws) + if k == 0: + return [{}] # ground expression: one empty valuation + na = len(ATOMS) ** k + if na <= MAX_PRODUCT: + idx = np.stack(np.meshgrid(*[np.arange(len(ATOMS))] * k, indexing='ij'), -1).reshape(-1, k) + else: + idx = rng.integers(0, len(ATOMS), size=(MAX_PRODUCT, k)) + return [{w: ATOMS[j] for w, j in zip(ws, row)} for row in idx] + + +def _symbolic_atom(t): + """The mp value a probe token denotes under real semantics: transcendental atoms bind + SYMBOLICALLY at working precision -- a variable or constant ranges over the REALS, so + pi/2 (where sin = 1 exactly) is a legitimate probe point even though no f64 equals it. + Everything else binds as its dyadic value. Build INSIDE the caller's workdps.""" + from mpmath import mp, mpf, inf as mp_inf, nan as mp_nan + special = {'float("inf")': lambda: mp_inf, 'float("-inf")': lambda: -mp_inf, + 'float("nan")': lambda: mp_nan, + '3.141592653589793': lambda: +mp.pi, '(-3.141592653589793)': lambda: -mp.pi, + '2.718281828459045': lambda: +mp.e, '(-2.718281828459045)': lambda: -mp.e, + '1.5707963267948966': lambda: mp.pi / 2, '(-1.5707963267948966)': lambda: -mp.pi / 2, + '6.283185307179586': lambda: 2 * mp.pi, '(-6.283185307179586)': lambda: -2 * mp.pi, + '0.7853981633974483': lambda: mp.pi / 4, '(-0.7853981633974483)': lambda: -mp.pi / 4} + return special[t]() if t in special else mpf(t.strip('()')) + + +def _env_mp(wmap): + """ATOM valuation -> mp env (symbolic transcendentals per `_symbolic_atom`).""" + return {w: _symbolic_atom(t) for w, t in wmap.items()} + + +def mp_value_at(tokens, wmap): + """Exact value classification of `tokens` at an atom valuation. + + f64 is unreliable at the atoms in two ways: zero coincidences (f64 sin(pi) = 1.2e-16, so + `sin(np.pi) * inf` reads inf where exact arithmetic gives 0 * inf = nan) and POLE + coincidences (`tan(atan(inf))`: atan(inf) is exactly pi/2 and tan(pi/2) is a pole, but + every finite precision renders a huge finite number). Both are classified by a + precision-stability gate: evaluate at dps 60, escalate suspicious values (|v| < 1e-40, + |v| > 1e40, or non-finite) to dps 120 -- + residue SHRINKS with precision -> exact zero; + magnitude GROWS with precision -> exact pole -> undefined (nan); + stable -> the value itself. + Returns an mp value (nan encodes undefined).""" + from mpmath import mp, mpf, isnan as mnan, isinf as minf, nan as mp_nan + with mp.workdps(60): + a = hp_eval(list(tokens), _env_mp(wmap), []) + suspicious = mnan(a) or minf(a) or (a != 0 and (abs(a) < mpf('1e-40') or abs(a) > mpf('1e40'))) + if not suspicious: + return a + with mp.workdps(120): + b = hp_eval(list(tokens), _env_mp(wmap), []) + if mnan(a) and mnan(b): + return mp_nan + if mnan(a) != mnan(b): + return mp_nan # nan-unstable: not a provable value + if minf(a) or minf(b): + return a if (minf(a) and minf(b) and (a > 0) == (b > 0)) else mp_nan + if (a == 0 and b == 0) or (abs(a) < mpf('1e-40') and abs(b) <= abs(a) * mpf('1e-20')): + return mpf(0) # residue shrinks: exact zero + if abs(a) > mpf('1e40') and abs(b) >= abs(a) * mpf('1e20'): + return mp_nan # magnitude grows with dps: exact pole + return b + + +def contract_value_at(tokens, wmap): + """The contract value of `tokens` at an atom valuation. + + Under the semantics this gate enforces (real-valued quantifiers, a single zero with + 1/0 = +inf, transcendental-literal denotation) the mp arm (`mp_value_at`: symbolic + transcendental atoms, two-rung zero/pole snaps, single-zero mpmath arithmetic, the + high-precision evaluation table) IS the value. f64 is NOT consulted for signed zeros: + a single zero has no sign to disagree on, and letting a -0-mediated infinity sign in + would wrongly convict sound rewrites (e.g. inv(0*x0) -> +inf). f64 remains only as an + evaluation FALLBACK when the mp arm cannot evaluate at all. Returns a float (nan encodes + undefined).""" + from mpmath import isnan as mnan, isinf as minf + try: + vm = mp_value_at(tokens, wmap) + except Exception: + try: + return eval_point(substitute(list(tokens), wmap)) # fallback: deployed f64 + except Exception: + return float('nan') + if mnan(vm): + return float('nan') + if minf(vm): + return float('inf') if vm > 0 else float('-inf') + return float(vm) + + +def judge_r2prime(lhs, rhs, valuations): + """The `?` atom bar: extension tolerated, value change / domain shrink killed. Judged on + `contract_value_at` (see its docstring). Prefolded first; rule-correlated atom valuations + appended.""" + lhs, rhs = prefold(lhs), prefold(rhs) + valuations = list(valuations) + correlated_valuations(lhs, rhs, wildcards(list(lhs) + list(rhs))) + for wmap in valuations: + try: + a = contract_value_at(lhs, wmap) + b = contract_value_at(rhs, wmap) + except Exception as ex: + return 'EVAL-ERR', f'{type(ex).__name__}: {ex}' + an, bn = np.isnan(a), np.isnan(b) + if an: + continue # undefined source: extension tolerated + if bn: + return 'KILL', (dict(wmap), a, b) # defined -> undefined: domain shrink + if np.isinf(a) or np.isinf(b): + if a == b: + continue + return 'KILL', (dict(wmap), a, b) # inf sign/finiteness change + # Single zero (1/0 = +inf): an f64 zero's sign is measurement rendering, never a value + # difference, so no signed-zero tie-break is applied here (float == treats -0 == +0). + if abs(a - b) <= 1e-9 * max(1.0, abs(a), abs(b)): + continue + return 'KILL', (dict(wmap), a, b) # defined-value change at an atom + return 'PASS', None + + +# --- the pow integer-preimage probe -------------------------------------------------------- +# A rule like `pow float("-inf") asinh _0 -> pow float("inf") _0` is violated exactly where +# the exponent chain crosses a small integer (asinh(x) = 1 at x = sinh(1) = 1.1752...) -- a +# point NO finite atom lattice contains. For single-wildcard rules whose pow has a literal +# +-inf / 0 / negative-numeric base, solve chain(x) = k for k in [-5, 5] by bisection and +# compare the two sides' EXACT pow classes at the root (integer-exponent algebra, so the +# transcendental root needs no precision at all on the solved side). + +def _pow_class(base, k): + """Exact value of pow(base, y) for INTEGER y = k, in the deployed algebra.""" + if np.isnan(base): + return float('nan') + if k == 0: + return 1.0 + if np.isinf(base): + if k > 0: + return base if k % 2 else abs(base) + return -0.0 if (base < 0 and k % 2) else 0.0 + if base == 0.0: + neg = np.signbit(base) + if k > 0: + return -0.0 if (neg and k % 2) else 0.0 + return float('-inf') if (neg and k % 2) else float('inf') + try: + return float(base) ** k + except OverflowError: + return float('inf') if (base > 0 or k % 2 == 0) else float('-inf') + + +def _subtree_end(tokens, i, arity): + j = i + 1 + for _ in range(arity.get(tokens[i], 0)): + j = _subtree_end(tokens, j, arity) + return j + + +def _val_token(v): + """Spell a float value as an expression token both evaluators parse.""" + if np.isnan(v): + return 'float("nan")' + if np.isinf(v): + return 'float("inf")' if v > 0 else 'float("-inf")' + return repr(float(v)) if v >= 0 else f'({float(v)!r})' + + +def pow_preimage_witness(lhs, rhs): + """Search for an integer-preimage witness killing the rule; None if none found. + + Scope: single-wildcard rules where some `pow` on either side has a LITERAL base + (+-inf, 0, or a negative numeric) and the wildcard inside its exponent subtree. + Mechanism: solve chain(x*) = k (k integer) by bisection; at x* the solved pow's value + is EXACT integer-exponent algebra (`_pow_class`) -- substitute that value back into the + expression as a token and evaluate the surroundings numerically. Any pow on either side + whose chain is TOKEN-IDENTICAL to the solved chain lands on exactly k too and gets the + same exact substitution, so identical-chain rules (`pow -inf f(_0) -> pow +inf f(_0)`) + are compared exactly on both sides. Comparison follows the atom bar (extension toward the + target tolerated; value change or shrink kills).""" + from ._f64_eval import ARITY, LITERALS as LITS, _num + toks_l, toks_r = list(lhs), list(rhs) + ws = wildcards(toks_l + toks_r) + if len(ws) != 1: + return None + w = ws[0] + + def pow_sites(tokens): + out = [] + for i, t in enumerate(tokens): + if t != 'pow': + continue + b0 = i + 1 + b1 = _subtree_end(tokens, b0, ARITY) + e1 = _subtree_end(tokens, b1, ARITY) + if b1 != b0 + 1: + continue # base must be a single literal token + bv = LITS.get(tokens[b0], _num(tokens[b0])) + if bv is None or not (np.isinf(bv) or bv <= 0.0): + continue + if w in tokens[b1:e1]: + out.append((i, e1, bv, tuple(tokens[b1:e1]))) + return out + + def f64_at(tokens, x): + try: + return eval_point(substitute(list(tokens), {w: _val_token(x)})) + except Exception: + return float('nan') + + def side_with_exact_pows(tokens, solved_chain, k, x): + """Evaluate a side at x, with every literal-base pow whose chain equals the solved + chain replaced by its exact integer-exponent class value.""" + toks = list(tokens) + for i, e1, bv, chain in sorted(pow_sites(toks), reverse=True): + if chain == solved_chain: + toks[i:e1] = [_val_token(_pow_class(bv, k))] + return f64_at(toks, x) + + all_sites = pow_sites(toks_l) + pow_sites(toks_r) + if not all_sites: + return None + grid = np.linspace(-40.0, 40.0, 4001) + seen_chains = set() + for _, _, _, chain in all_sites: + if chain in seen_chains: + continue + seen_chains.add(chain) + hv = np.array([f64_at(list(chain), x) for x in grid]) + for k in range(-5, 6): + d = hv - k + sgn = np.sign(d) + roots = [float(grid[i]) for i in np.where(d == 0.0)[0][:3]] # exact grid hits + hits = np.where((sgn[:-1] * sgn[1:] < 0) & np.isfinite(d[:-1]) & np.isfinite(d[1:]))[0] + for i in hits[:3]: + lo, hi = grid[i], grid[i + 1] + slo = np.sign(f64_at(list(chain), lo) - k) + for _ in range(80): + mid = 0.5 * (lo + hi) + if np.sign(f64_at(list(chain), mid) - k) == slo: + lo = mid + else: + hi = mid + roots.append(0.5 * (lo + hi)) + for x_star in roots: + a = side_with_exact_pows(toks_l, chain, k, x_star) + b = side_with_exact_pows(toks_r, chain, k, x_star) + an, bn = np.isnan(a), np.isnan(b) + if an: + continue # extension toward target: tolerated + kill = bn or ((np.isinf(a) or np.isinf(b)) and a != b) or \ + (np.isfinite(a) and np.isfinite(b) + and abs(a - b) > 1e-6 * max(1.0, abs(a), abs(b))) + if kill: + return {'x*': float(x_star), 'k': k, 'lhs_val': a, 'rhs_val': b} + return None + + +def mp_finite(v): + return not (isnan(v) or isinf(v)) + + +def mp_eq(a, b): + if isnan(a) and isnan(b): + return True + if isnan(a) != isnan(b): + return False + if isinf(a) or isinf(b): + return a == b + from mpmath import fabs + return fabs(a - b) <= mpf('1e-30') * max(1, fabs(a), fabs(b)) + + +def judge_ground(lhs, rhs, rng): + """SKELETON semantics for ``-bearing ground rules: for-all c exists finite c_t.""" + ns = lhs.count('') + if ns != 1: + return 'UNSUPPORTED', f'{ns} LHS slots (certifier handles exactly 1)' + bare_slot = list(rhs) == [''] + if '' in rhs and not bare_slot: + return 'UNSUPPORTED', 'structured RHS (needs a witness map)' + mp.dps = DPS + # Constants range over the REALS, so transcendental probe atoms bind SYMBOLICALLY here + # too. This keeps the ground tier consistent with the `?` bar: binding pi/2 as the f64 + # rational (sin < 1) would pass `pow sin inf -> 0` while the `?` bar binds it + # symbolically (sin = 1) and kills it -- a tier inconsistency that ships an unsound rule. + probes = ([_symbolic_atom(a) for a in FINITE_ATOMS] + + [mpf(repr(float(v))) for v in np.round(rng.normal(0, 5, GROUND_DRAWS), 6)]) + for c in probes: + try: + v = hp_eval(list(lhs), {}, [c]) + except Exception as ex: + return 'EVAL-ERR', f'{type(ex).__name__}: {ex}' + if bare_slot: + if not mp_finite(v): + return 'KILL', (float(c), str(v), '') + else: + try: + w = hp_eval(list(rhs), {}, []) + except Exception as ex: + return 'EVAL-ERR', f'{type(ex).__name__}: {ex}' + if not mp_eq(v, w): + return 'KILL', (float(c), str(v), str(w)) + # (No f64 zero-sign check here: a single zero makes `/ inf -> 0` sound.) + return 'PASS', None + + +def _pow_inf_sites(toks, ARITY): + """Base token-tuples of every pow(base, literal +-inf) subterm.""" + INF_T = ('float("inf")', 'float("-inf")') + out = [] + for i, t in enumerate(toks): + if t != 'pow': + continue + b0 = i + 1 + b1 = _subtree_end(toks, b0, ARITY) + e1 = _subtree_end(toks, b1, ARITY) + if e1 - b1 == 1 and toks[b1] in INF_T: + out.append(tuple(toks[b0:b1])) + return out + + +def _base_range_spiky(base, core): + """Does this base's interval range REACH +-1 non-degenerately (so pow(base,+-inf) has a + spike at a real point)? Wildcards/ become independent wide axes (they range over + the reals). Fail-closed: an unevaluable base counts as spiky. `core` is the compiled engine + core exposing the `interval_value_set_box` FFI query.""" + toks, m = [], {} + for t in base: + if t.startswith(('_', '?', '!')) or t == '': + m.setdefault(t, f'x{len(m)}') + toks.append(m[t]) + else: + toks.append(t) + n = max(len(m), 1) + try: + has_fin, pinf, ninf, nan, lo, hi = core.interval_value_set_box( + list(toks), [-1e6] * n, [1e6] * n) + except Exception: + return True + lo = float('-inf') if ninf else lo + hi = float('inf') if pinf else hi + return lo < hi and (lo <= 1.0 <= hi or lo <= -1.0 <= hi) + + +def spike_flattener_witness(lhs, rhs, core): + """Structural refusal of pow-inf SPIKE FLATTENERS (scope: flatteners only; wrappers pass). + + pow(t, +-inf) is a STEP in its base t: |t|<1 -> 0, |t|=1 -> 1, |t|>1 -> +inf. If the + base's real range reaches +-1 over a non-degenerate interval, the term SPIKES at a real + point (pow(sin(x),inf) = 1 exactly at x = pi/2). A rule whose RHS DROPS every such term + replaces the spike with the a.e. value -- unsound at a real point under real semantics -- + and no fixed atom lattice can chase the spike when it moves with a fitted constant + (pow(sin(c*x),inf) violates at x = pi/(2c), a point the fit chooses). Refusing the FORM + is invariant to that motion. Rules whose RHS keeps a spiky pow-inf term (wrappers like + abs(pow(_0,inf)) -> pow(_0,inf)) carry the spike honestly and are allowed through to the + normal bars. Conservative by construction (interval over-approximation can only + over-refuse); the lo==hi degenerate guard keeps exact ground facts like pow(-1,inf)->1. + + `core` is the compiled engine core supplying the interval query (see `_base_range_spiky`).""" + from ._f64_eval import ARITY + l_spiky = [b for b in _pow_inf_sites(list(lhs), ARITY) if _base_range_spiky(b, core)] + if not l_spiky: + return None + r_spiky = [b for b in _pow_inf_sites(list(rhs), ARITY) if _base_range_spiky(b, core)] + if r_spiky: + return None # spike carried over in kind: wrapper, honest + return {'spiky_base': ' '.join(l_spiky[0])} + + +NONFINITE_TOKENS = {'float("inf")', 'float("-inf")', 'float("nan")'} + + +def finite_only(valuations): + return [v for v in valuations if not any(t in NONFINITE_TOKENS for t in v.values())] + + +def judge_bang(lhs, rhs, rng): + """The `!`-sort promotion bar: exact pointwise over FINITE valuations only (atoms + draws + + correlated), plus the pow-preimage probe. A `!`-bound subtree is certified finite a.e., + so its pushforward puts NO mass on {nan, +-inf}: behaviour at nonfinite valuations is + a.e.-irrelevant and dropped from the bar. A constant subtree is a Dirac at a FINITE value, + which is why the finite bar must stay EXACT. + + An UNDECIDED near-band (f64 rounding is denied the authority to convict) escalates to the + exact arbiter (`._overturn.judge_exact`) on the same finite valuations -- this is what lets + saturating true identities (`atanh tanh ?0 -> ?0`) clear the bar and regain subtree + binding.""" + ws = wildcards(list(lhs) + list(rhs)) + vals = finite_only(valuations_for(ws, rng)) + v, info = judge(list(lhs), list(rhs), vals) + if v in ('UNDECIDED', 'DEMOTE'): + # DEMOTE escalates too: an f64 kill at a FINITE valuation can be pure saturation + # (tanh(37) == 1.0 exactly, so atanh(tanh(37)) reads inf), and f64 is denied the + # authority to convict; the exact arbiter confirms real kills and overturns + # saturation artifacts (real semantics governs). + from ._overturn import judge_exact + v2, _kill = judge_exact(list(lhs), list(rhs), vals) + if v2 == 'PROMOTE': + v, info = 'PROMOTE', 'exact-arbiter' + if v == 'PROMOTE' and pow_preimage_witness(lhs, rhs) is not None: + return 'DEMOTE', 'POW-PREIMAGE' + return v, info + + +def respell_bang(tokens): + return tuple('!' + t[1:] if t.startswith(('_', '?')) else t for t in tokens) + + +def tier_of(lhs, rhs): + """Five-way routing: {`_`, `?`} x {const-free, const-bearing}, plus ground. Const-bearing + wildcard rules go through the forall-exists witness machinery (`._const_bearing.certify_rule`); + routing them to the const-free judge would raise on the unbound `` slot.""" + toks = list(lhs) + list(rhs) + cb = '' in toks + if any(t.startswith('_') for t in toks): + return '_cb' if cb else '_cf' + if any(t.startswith('?') for t in toks): + return '?cb' if cb else '?cf' + return 'ground' + + +def respell(tokens): + return tuple('?' + t[1:] if t.startswith('_') else t for t in tokens) + + +def run_controls(rng, core): + """Positive-control self-test: run each labelled control through its judge and raise + RuntimeError on any verdict that does not match the expected outcome. This guards against + a miscalibrated judge silently mis-promoting rules.""" + ctrl = [ + # a null-set value change (4 vs 1 at x0 = +-1): killed on the ? bar + ('?', (['*', '4.0', 'pow', '?0', 'float("inf")'], ['pow', '?0', 'float("inf")']), 'KILL'), + # x/x -> 1: extension-only (nan at 0 and +-inf) -- must SURVIVE the ? bar + ('?', (['/', '?0', '?0'], ['1']), 'PASS'), + ('?', (['+', '?0', '0'], ['?0']), 'PASS'), + # domain shrink at an atom: log(?0) undefined at ?0 = -1 where the source is defined + ('?', (['+', '?0', '0'], ['log', '?0']), 'KILL'), + # transcendental zero + single zero: sin(pi) IS 0 (prefold), 0*t = 0 for finite t + # (zero-sign is measurement rendering, not a value), and 0*inf = nan -> 0 is a + # tolerated null-set extension at the atoms. PASS. + ('?', (['*', 'sin', 'np.pi', '?0'], ['0']), 'PASS'), + # pole coincidence: atan(inf) = pi/2 exactly, tan(pi/2) undefined -> extension + ('?', (['tan', 'atan', '?0'], ['?0']), 'PASS'), + # signed zero in the deployed algebra: pow1_3(-0.0) = +0.0 (the where-branch), so + # LHS(-inf) = inv(+0.0) = +inf vs RHS = -inf -- a genuine kill + ('?', (['inv', 'pow1_3', 'inv', '?0'], ['pow1_3', '?0']), 'KILL'), + # pow(0, exp(-inf)) = pow(0, 0) = 1 vs 0: a genuine value change at the atom + ('?', (['pow', '0', 'exp', '?0'], ['0']), 'KILL'), + # real semantics: sin attains 1 AT the real point pi/2, so pow(sin(?0),inf) -> 0 + # changes a defined value at a real point -- KILL. The symbolic pi/2 atom sees it. + ('?', (['pow', 'sin', '?0', 'float("inf")'], ['0']), 'KILL'), + # pow(c/5, nan) is nan for c != 5: cannot be simplified to a fitted + ('ground', (['pow', 'div5', '', 'float("nan")'], ['']), 'KILL'), + # the acos(pow(c, inf)) family: nan on ALL of c > 1 -- positive-measure, not just an atom + ('ground', (['acos', 'pow', '', 'float("inf")'], ['']), 'KILL'), + # sound ground rule: c + log(0) = -inf for every finite c + ('ground', (['+', '', 'log', '0'], ['float("-inf")']), 'PASS'), + # single zero: c/inf = 0 for every finite c -- sound + ('ground', (['/', '', 'float("inf")'], ['0']), 'PASS'), + # ground powsin: killed by the symbolic pi/2 probe on the CONSTANT axis + ('ground', (['pow', 'sin', '', 'float("inf")'], ['0']), 'KILL'), + # structural refusal (belt over the atoms' suspenders): flatteners refused, wrappers + # and degenerate ground facts allowed + ('spike', (['pow', 'sin', '?0', 'float("inf")'], ['0']), 'REFUSE'), + ('spike', (['pow', 'sin', '', 'float("inf")'], ['0']), 'REFUSE'), + ('spike', (['abs', 'pow', '_0', 'float("inf")'], ['pow', '_0', 'float("inf")']), 'ALLOW'), + ('spike', (['inv', 'pow', '_0', 'float("inf")'], ['pow', '_0', 'float("-inf")']), 'ALLOW'), + ('spike', (['pow', '(-1)', 'float("inf")'], ['1']), 'ALLOW'), + # a sign-clean survivor: c * inf = +inf is spelled inf, no zero involved + ('ground', (['+', '', 'atanh', '1'], ['float("inf")']), 'PASS'), + ] + for tier, (lhs, rhs), want in ctrl: + if tier == '?': + v, info = judge_r2prime(lhs, rhs, atom_valuations(wildcards(lhs + rhs), rng)) + elif tier == 'spike': + w = spike_flattener_witness(lhs, rhs, core) + v, info = ('REFUSE', w) if w is not None else ('ALLOW', None) + else: + v, info = judge_ground(lhs, rhs, rng) + if v != want: + raise RuntimeError( + f'positive control failed: [{tier}] {" ".join(lhs)} -> {" ".join(rhs)} ' + f'got {v} want {want} ({str(info)[:120]})') + + +def promote_rules(rules, engine, *, seed=SEED, run_positive_controls=True): + """Certify `rules` down the `_` -> `!` -> `?` ladder (plus the ground tier) and return the + promoted rules alongside a per-bucket report. + + Parameters + ---------- + rules : iterable of (lhs, rhs) + Each side is a sequence of prefix-expression tokens (wildcards `_i`/`?i`, literals, + ``), as produced by the miner. Matches the format the standalone pass loaded + from JSON. + engine : SimpliPyEngine + Supplies the compiled interval core via `engine._core`; its `interval_value_set_box` + FFI query drives the spike-flattener refusal. The interval query is over raw + expressions, so a rules-empty engine is sufficient (and matches the original setup). + seed : int + Seed for the single shared numpy RNG (all sampling flows from it); defaults to the + pass's fixed seed so behaviour is reproducible. + run_positive_controls : bool + Run the positive-control self-test first (raising on any miss) before promotion. + + Returns + ------- + (kept, report) : (list of (lhs, rhs), dict) + `kept` is the promoted rule set (with `_`/`!`/`?` sort respelling applied); `report` + buckets every routing decision (`promoted_bang`, `demoted_to_q`, `refused_spike`, + `killed_q`, `killed_ground`, `undecided`, `no_witness`, `eval_err`, `unsupported`). + """ + core = engine._core + rng = np.random.default_rng(seed) + if run_positive_controls: + run_controls(rng, core) + rules = list(rules) + tiers = {'_cf': [], '_cb': [], '?cf': [], '?cb': [], 'ground': []} + for lhs, rhs in rules: + tiers[tier_of(lhs, rhs)].append((lhs, rhs)) + + report = {'demoted_to_q': [], 'promoted_bang': [], 'refused_spike': [], + 'killed_q': [], 'killed_ground': [], + 'undecided': [], 'no_witness': [], 'eval_err': [], 'unsupported': []} + kept = [] + + # `_` tiers: exact-pointwise bar on the ENRICHED lattice; failures step DOWN THE SORT + # LADDER `_` -> `!` -> `?` (each strictly weaker binding, each with its own bar). + q_cf = list(tiers['?cf']) + q_cb = list(tiers['?cb']) + + def ladder_cf(lhs, rhs, verdict, info): + """A `_cf` failure tries `!` (finite-exact bar) before falling to `?`.""" + bv, _ = judge_bang(lhs, rhs, rng) + if bv == 'PROMOTE': + report['promoted_bang'].append((lhs, rhs, verdict, str(info)[:120])) + kept.append((respell_bang(lhs), respell_bang(rhs))) + else: + report['demoted_to_q'].append((lhs, rhs, verdict, str(info)[:120])) + q_cf.append((respell(lhs), respell(rhs))) + + for lhs, rhs in tiers['_cf']: + ws = wildcards(list(lhs) + list(rhs)) + v, info = judge(list(lhs), list(rhs), valuations_for(ws, rng)) + if v == 'PROMOTE': + pw = pow_preimage_witness(lhs, rhs) + if pw is not None: + ladder_cf(lhs, rhs, 'POW-PREIMAGE', pw) + continue + # Contract-atom check: the f64 `_` judge speaks deployed-numpy semantics at the + # atoms (signed zeros, numpy pow(-inf, non-int) = nan) while the enforced contract + # is single-zero real (the mp arm). A `_` promote must ALSO hold at the mp-contract + # atoms, else it takes the ladder -- otherwise `pow _0 div4 1 -> pow1_4 _0` would + # ship while the certifier kills its own ?-tier div2 twin on the identical witness. + av, ainfo = judge_r2prime(list(lhs), list(rhs), atom_valuations(ws, rng)) + if av != 'PASS': + ladder_cf(lhs, rhs, 'CONTRACT-ATOM', ainfo) + continue + kept.append((lhs, rhs)) + elif v in ('DEMOTE', 'UNDECIDED'): + # UNDECIDED at the `_` bar is fail-safe demotion (rounding may not convict, but + # it may not certify either); the ladder decides where it lands. + ladder_cf(lhs, rhs, v, info) + else: + report['eval_err'].append((lhs, rhs, v, str(info)[:120])) + + for lhs, rhs in tiers['_cb']: + v, info = certify_rule(lhs, rhs, rng) + if v == 'PROMOTE': + ws = wildcards(list(lhs) + list(rhs)) + av, ainfo = certify_rule(lhs, rhs, rng, judge_fn=judge_r2prime, + vals_override=atom_valuations(ws, rng)) + if av != 'PROMOTE': + bv, _ = certify_rule(lhs, rhs, rng, vals_override=finite_only( + valuations_for(ws, rng))) + if bv == 'PROMOTE' and pow_preimage_witness(lhs, rhs) is None: + report['promoted_bang'].append((lhs, rhs, 'CONTRACT-ATOM', str(ainfo)[:120])) + kept.append((respell_bang(lhs), respell_bang(rhs))) + else: + report['demoted_to_q'].append((lhs, rhs, 'CONTRACT-ATOM', str(ainfo)[:120])) + q_cb.append((respell(lhs), respell(rhs))) + continue + kept.append((lhs, rhs)) + elif v in ('DEMOTE', 'NO-WITNESS'): + bv, _ = certify_rule(lhs, rhs, rng, vals_override=finite_only( + valuations_for(wildcards(list(lhs) + list(rhs)), rng))) + if bv == 'PROMOTE' and pow_preimage_witness(lhs, rhs) is None: + report['promoted_bang'].append((lhs, rhs, v, str(info)[:120])) + kept.append((respell_bang(lhs), respell_bang(rhs))) + else: + report['demoted_to_q'].append((lhs, rhs, v, str(info)[:120])) + q_cb.append((respell(lhs), respell(rhs))) + else: + report['eval_err'].append((lhs, rhs, v, str(info)[:120])) + + # `?` const-free (incl. fresh demotions): the atom bar + seen = set() + for lhs, rhs in q_cf: + if (lhs, rhs) in seen: + continue + seen.add((lhs, rhs)) + v, info = judge_r2prime(list(lhs), list(rhs), atom_valuations(wildcards(list(lhs) + list(rhs)), rng)) + if v == 'PASS': + pw = pow_preimage_witness(lhs, rhs) + if pw is not None: + # a preimage witness is a REAL variable-leaf input (x = sinh(1) etc.), so at + # the ? sort this is a defined-value change on an actual point: killed. + report['killed_q'].append((lhs, rhs, 'POW-PREIMAGE ' + str(pw)[:140])) + continue + # UPGRADE attempt: `!` strictly generalizes `?` (a variable leaf is trivially + # finite a.e.), so a ? rule that also clears the finite-exact bar ships as `!` + # and gains certified-subtree recall for free. + bv, _ = judge_bang(lhs, rhs, rng) + if bv == 'PROMOTE': + report['promoted_bang'].append((lhs, rhs, '?-upgrade', '')) + kept.append((respell_bang(lhs), respell_bang(rhs))) + else: + kept.append((lhs, rhs)) + elif v == 'KILL': + report['killed_q'].append((lhs, rhs, str(info)[:160])) + elif v == 'UNDECIDED': + report['undecided'].append((lhs, rhs, str(info)[:120])) + else: + report['eval_err'].append((lhs, rhs, v, str(info)[:120])) + + # `?` const-bearing (incl. fresh demotions): the atom bar THROUGH the witness machinery + # (forall c_s exists c_t; instantiated pairs held to judge_r2prime on atom-only valuations). + # NO-WITNESS here is a solver limitation: held OUT of the artifact, conservative, reported + # in its own bucket. + for lhs, rhs in q_cb: + if (lhs, rhs) in seen: + continue + seen.add((lhs, rhs)) + ws = wildcards(list(lhs) + list(rhs)) + v, info = certify_rule(lhs, rhs, rng, judge_fn=judge_r2prime, + vals_override=atom_valuations(ws, rng)) + if v == 'PROMOTE': + bv, _ = certify_rule(lhs, rhs, rng, vals_override=finite_only( + valuations_for(ws, rng))) + if bv == 'PROMOTE' and pow_preimage_witness(lhs, rhs) is None: + report['promoted_bang'].append((lhs, rhs, '?-upgrade', '')) + kept.append((respell_bang(lhs), respell_bang(rhs))) + else: + kept.append((lhs, rhs)) + elif v == 'DEMOTE': + report['killed_q'].append((lhs, rhs, str(info)[:160])) + elif v == 'NO-WITNESS': + report['no_witness'].append((lhs, rhs, str(info)[:120])) + else: + report['eval_err'].append((lhs, rhs, v, str(info)[:120])) + + # Seeded canonical identities: the additive-cancel family cannot be MINED -- its sources + # (`- x0 x0`) are pre-canceled at enumeration, so no rule carrier ever exists. Seeds are + # certified through the SAME judge_bang bar as everything else, never trusted by fiat. + lhs_seen = {tuple(l) for l, _ in kept} + for lhs, rhs in [(('-', '!0', '!0'), ('0',)), + (('+', '!0', 'neg', '!0'), ('0',)), + (('+', 'neg', '!0', '!0'), ('0',))]: + if tuple(lhs) in lhs_seen: + continue + bv, _ = judge_bang(lhs, rhs, rng) + if bv == 'PROMOTE': + report['promoted_bang'].append((lhs, rhs, 'seed', '')) + kept.append((lhs, rhs)) + + # ground tier: skeleton semantics, mpmath + for lhs, rhs in tiers['ground']: + v, info = judge_ground(list(lhs), list(rhs), rng) + if v == 'PASS': + kept.append((lhs, rhs)) + elif v == 'KILL': + report['killed_ground'].append((lhs, rhs, str(info)[:160])) + elif v == 'UNSUPPORTED': + report['unsupported'].append((lhs, rhs, str(info)[:120])) + else: + report['eval_err'].append((lhs, rhs, v, str(info)[:120])) + + # STRUCTURAL spike-flattener refusal over EVERYTHING kept (all tiers): the powsin class + # dies here even when no atom happens to sit on its spike (moving-coincidence insurance). + still = [] + for lhs, rhs in kept: + w = spike_flattener_witness(lhs, rhs, core) + if w is None: + still.append((lhs, rhs)) + else: + report['refused_spike'].append((lhs, rhs, str(w)[:120])) + kept = still + + return kept, report diff --git a/src/simplipy/promotion/_overturn.py b/src/simplipy/promotion/_overturn.py new file mode 100644 index 0000000..1aea2e3 --- /dev/null +++ b/src/simplipy/promotion/_overturn.py @@ -0,0 +1,77 @@ +# mypy: ignore-errors +"""Exact re-arbitration of finite-draw demotions using arbitrary-precision arithmetic. + +A pointwise DEMOTE that was decided at a FINITE numeric draw is only float64 evidence, and +float64 saturation can spuriously kill an exact identity (for example ``atanh(tanh(x)) = x``, +whose float64 round-trip saturates at large-magnitude draws and reads as a mismatch). This +module re-judges exactly those finite-draw demotions in mpmath at adaptive precision: + + - each finite draw is evaluated at ADAPTIVE dps = 50 + int(max|v|) + 10, and again at twice + that precision. The ``+ int(max|v|)`` term adds one working decimal digit per unit of + |v|, which comfortably exceeds the ~0.87 digits per unit that the saturating round-trip's + conditioning actually loses; a draw counts as evidence only if BOTH precisions agree + (a precision-stability gate against precision-cliff artefacts); + - a draw whose required adaptive dps exceeds ``DPS_CAP`` is UNDECIDABLE, in which case the + demotion STANDS (fail-safe: never overturn on evidence that could not be computed). + +A rule is overturned (DEMOTE -> PROMOTE) only when every valuation agrees exactly under this +arbitration. Atom-only kills are not re-judged here: they are special-value algebra that is +already exact in float64, so a driver should exclude any demotion whose valuation is drawn +entirely from ``ATOMS`` before calling ``judge_exact``. +""" +import numpy as np + +from ._pointwise import ATOMS, wildcards, valuations_for +from ._hp_equiv import evaluate as hp_eval +from mpmath import mp, mpf, isnan, isinf, inf, nan, fabs + +SEED = 20260717 +DPS_CAP = 800 + +ATOM_VALS = {'0.0': mpf(0), '-0.0': mpf(0), '1.0': mpf(1), '(-1.0)': mpf(-1), + 'float("inf")': inf, 'float("-inf")': -inf, 'float("nan")': nan} + + +def tok_to_mp(t): + if t in ATOM_VALS: + return ATOM_VALS[t] + return mpf(t.strip('()')) + + +def eq(a, b): + if isnan(a) and isnan(b): + return True + if isnan(a) != isnan(b): + return False + if isinf(a) or isinf(b): + return a == b + return fabs(a - b) <= mpf('1e-30') * max(1, fabs(a), fabs(b)) + + +def judge_exact(lhs, rhs, valuations): + """Re-judge a rule over the supplied valuation set in mpmath. + + Returns ``('PROMOTE', None)`` when every valuation agrees exactly; ``('DEMOTE-EXACT', + wmap)`` when a valuation disagrees under the precision-stability gate; or + ``('UNDECIDABLE', wmap)`` when a valuation needs more precision than ``DPS_CAP`` allows + or evaluation raises. The paired ``wmap`` is the offending valuation. + """ + for wmap in valuations: + vals = {w: tok_to_mp(t) for w, t in wmap.items()} + finmax = max([abs(float(v)) for v in vals.values() if not (isnan(v) or isinf(v))] or [0.0]) + need = 50 + int(finmax) + 10 + if need > DPS_CAP: + return 'UNDECIDABLE', dict(wmap) + verdicts = [] + for dps in (need, 2 * need): + mp.dps = dps + env = {w: (v if (isnan(v) or isinf(v)) else mpf(repr(float(v)))) for w, v in vals.items()} + try: + a = hp_eval(list(lhs), env, []) + b = hp_eval(list(rhs), env, []) + except Exception: + return 'UNDECIDABLE', dict(wmap) + verdicts.append(eq(a, b)) + if not (verdicts[0] and verdicts[1]): + return 'DEMOTE-EXACT', dict(wmap) + return 'PROMOTE', None diff --git a/src/simplipy/promotion/_pointwise.py b/src/simplipy/promotion/_pointwise.py new file mode 100644 index 0000000..cb96e6b --- /dev/null +++ b/src/simplipy/promotion/_pointwise.py @@ -0,0 +1,268 @@ +# mypy: ignore-errors +"""Pointwise certifier for the `_`-sort (subtree-sort) promotion bar. + +Soundness bar: a rule whose slots are subtree-sort is sound iff S(v) = T(v) for +EVERY consistent valuation v of its wildcards over R u {+-0, +-inf, nan}, where +nan == nan counts as equal, in BOTH directions (a nan hole may not be filled; a +value may not be lost or changed). There is no measure tolerance in the subtree +sort: a constant subtree is a Dirac, so a single disagreeing valuation refutes. + +The atoms are TOTAL singular bindings (0, 1, -1, +-inf, nan, and finite draws): +they surface both directions of failure -- nan -> value (a filled hole) and +value -> wrong value. DISTINCT wildcards receive the full product of values; +repeated wildcard names share a value (consistent valuations: the diagonal). + +Verdicts (per rule): + PROMOTE -- all valuations agree; ships as `_`-sort (subtree sort). + DEMOTE -- a killing valuation exists (recorded); ships as `?`-sort + (variable-leaf sort), losing nothing it was ever certified for. + UNDECIDED -- only near-tolerance finite disagreements remain; f64 rounding may + not convict, so these are deferred to an exact arbiter. + +Scope: const-free wildcard rules. ``-bearing rules need a +forall-exists witness map and are handled by a separate promotion stage. +Acceptance is sampling-based: a PROMOTE is falsification-survival at these +valuations, with the false-promote rate bounded by the valuation count. +""" +import json + +import numpy as np + +from ._f64_eval import evaluate, ARITY, LITERALS, _num + +# THE ATOM LATTICE -- the shared list every certifier imports. Killing valuations +# for numeric rules cluster on the integers and on rule-correlated points, so the +# lattice must include them explicitly: +# * integers >= 2 and half-integers expose pow's odd/even-parity artifacts; +# * +-pi, +-e, +-pi/2, +-2pi, +-pi/4 (f64 renderings -- used only as refutation +# probes, so exact transcendence is not needed) expose trig/log coincidences. +# Capped at |10|: past ~20, tanh/exp towers saturate f64 EXACTLY (tanh(20) == 1.0) +# and a true identity would inf-mismatch at the atom -- a wrong kill this atom +# class is never re-judged for. +# +# Quantifiers range over the REALS, so transcendental probe points (x = pi/2 where +# sin = 1, x = pi/4 where tan = 1, ...) are LEGITIMATE: a rule wrong at x = pi/2 is +# wrong at a real point even though f64 never lands on it. The high-precision arm +# binds these tokens SYMBOLICALLY; the f64 arm binds their f64 renderings, whose +# saturation (sin(f64 pi/2) == 1.0) usefully MIMICS the real spike at the atom. +# Known incompleteness: coincidences that MOVE with a fitted constant +# (pow(sin(c*x), inf) at x = pi/(2c)) cannot be covered by any fixed lattice; a +# separate spike-flattening refusal covers that family structurally. +# +# '-0.0' is intentionally absent: it denotes the same real value as '0.0', so it +# probes nothing, and its f64 rendering carries non-normative sign effects. +ATOMS = ['0.0', '1.0', '(-1.0)', 'float("inf")', 'float("-inf")', 'float("nan")', + '2.0', '(-2.0)', '3.0', '(-3.0)', '5.0', '(-5.0)', '10.0', '(-10.0)', + '0.5', '(-0.5)', '1.5', '(-1.5)', '2.5', '(-2.5)', + '3.141592653589793', '(-3.141592653589793)', + '2.718281828459045', '(-2.718281828459045)', + '1.5707963267948966', '(-1.5707963267948966)', + '6.283185307179586', '(-6.283185307179586)', + '0.7853981633974483', '(-0.7853981633974483)'] +N_RAND = 24 # random finite draws appended per wildcard (mixture, seeded) +MAX_PRODUCT = 32768 # cap on the valuation product (30 atoms: full product through k=3) +SEED = 20260717 + + +def wildcards(tokens): + """DISTINCT slot names, all three sorts (`_` subtree, `!` certified subtree, `?` leaf).""" + seen = [] + for t in tokens: + if t.startswith(('_', '?', '!')) and t not in seen: + seen.append(t) + return seen + + +def is_const_free(tokens): + return '' not in tokens + + +def rand_pool(rng): + vals = list(np.round(rng.normal(0, 2, N_RAND // 2), 6)) + \ + list(np.round(rng.uniform(-40, 40, N_RAND - N_RAND // 2), 6)) + return [repr(float(v)) if v >= 0 else f'({float(v)!r})' for v in vals] + + +MAX_CORRELATED = 512 # cap on the per-rule correlated-atom product + +# OP-EMBEDDED constants: the op NAMES carry the numbers that make their fixed +# points special -- e.g. `pow float("-inf") div4 _0 -> pow float("inf") _0` is +# killed exactly at _0 = 4 (pow(-inf, 1) = -inf vs pow(inf, 4) = +inf), a value +# no literal in the rule spells -- so those embedded constants must be probed too. +OP_CONSTANTS = { + 'mult2': 2.0, 'mult3': 3.0, 'mult4': 4.0, 'mult5': 5.0, + 'div2': 2.0, 'div3': 3.0, 'div4': 4.0, 'div5': 5.0, + 'pow2': 2.0, 'pow3': 3.0, 'pow4': 4.0, 'pow5': 5.0, + 'pow1_2': 2.0, 'pow1_3': 3.0, 'pow1_4': 4.0, 'pow1_5': 5.0, +} + + +def correlated_valuations(lhs, rhs, ws): + """Rule-correlated atom valuations: killing points of a rule with numeric + literals are often IMAGES of its own constants. For each finite nonzero literal + c in the rule -- and each constant EMBEDDED in an op name (mult3 -> 3) -- probe + {c, -c, 1/c, -1/c}; full product over the slots, capped.""" + vals = set() + for t in list(lhs) + list(rhs): + v = LITERALS.get(t, _num(t)) + if v is None: + v = OP_CONSTANTS.get(t) + if v is not None and np.isfinite(v) and v != 0.0: + for u in (v, -v, 1.0 / v, -1.0 / v): + if np.isfinite(u) and abs(u) <= 1e6: + vals.add(round(float(u), 12)) + if not vals or not ws: + return [] + pool = [repr(v) if v >= 0 else f'({v!r})' for v in sorted(vals)] + k = len(ws) + if len(pool) ** k <= MAX_CORRELATED: + idx = np.stack(np.meshgrid(*[np.arange(len(pool))] * k, indexing='ij'), -1).reshape(-1, k) + else: + idx = np.random.default_rng(SEED).integers(0, len(pool), size=(MAX_CORRELATED, k)) + return [{w: pool[j] for w, j in zip(ws, row)} for row in idx] + + +def substitute(tokens, wmap): + return [wmap.get(t, t) for t in tokens] + + +def _literal_spans(tokens): + """(start, end) spans of MAXIMAL subtrees containing only operators/literals/numerics + (no wildcards, no variables, no ``).""" + n = len(tokens) + end = [0] * n + + def walk(i): + t = tokens[i] + j = i + 1 + for _ in range(ARITY.get(t, 0)): + j = walk(j) + end[i] = j + return j + walk(0) + + def is_lit(i): + return all(tokens[k] in ARITY or tokens[k] in LITERALS or _num(tokens[k]) is not None + for k in range(i, end[i])) + spans, i = [], 0 + while i < n: + if is_lit(i): + spans.append((i, end[i])) + i = end[i] + else: + i += 1 + return spans + + +_PREFOLD_CACHE = {} + + +def prefold(tokens): + """ZERO-SNAP: replace literal-only subtrees that denote EXACT zero by '0'. + + Transcendental literals denote their real value: `sin(np.pi)` IS zero, but f64 + renders it as 1.2e-16 -- harmless in the finite rel-band, but WRONG at the inf + atoms (1.2e-16 * inf = inf where 0 * inf must be nan, a spurious extension). The + sound `* sin np.pi ?0 -> 0` family would be killed at the inf atom without this + snap. + + The snap criterion is a precision-stability gate, not a bare threshold: evaluate + the subtree at dps 60 AND 120. An exact zero's rounding residue SHRINKS with + precision (~10^-dps), while a legitimately tiny value (exp(-exp(pow(e, e))) ~ + 10^-1.6M) is precision-STABLE and must NOT be snapped. Zeros are the only snapped + class: finite nonzero coincidences are already protected by the rel-band, and + only zero flips an algebraic class (0*inf, 0/0).""" + key = tuple(tokens) + if key in _PREFOLD_CACHE: + return _PREFOLD_CACHE[key] + out = list(tokens) + spans = [s for s in _literal_spans(out) if s[1] - s[0] > 1] + if spans: + from mpmath import mp, mpf, isnan as mp_isnan, isinf as mp_isinf + from ._hp_equiv import evaluate as hp_eval + for s, e in reversed(spans): + sub = out[s:e] + try: + with mp.workdps(60): + a = hp_eval(list(sub), {}, []) + with mp.workdps(120): + b = hp_eval(list(sub), {}, []) + except Exception: + continue + if mp_isnan(a) or mp_isnan(b) or mp_isinf(a) or mp_isinf(b): + continue + exact_zero = (a == 0 and b == 0) or \ + (abs(a) < mpf('1e-40') and abs(b) <= abs(a) * mpf('1e-20')) + if exact_zero: + out[s:e] = ['0'] + _PREFOLD_CACHE[key] = out + return out + + +def eval_point(tokens): + """Evaluate a GROUND prefix expression (no variables) to one f64.""" + env = {'__dummy__': np.zeros(1)} + return float(np.asarray(evaluate(list(tokens), env)).reshape(-1)[0]) + + +def judge(lhs, rhs, valuations): + """PROMOTE / DEMOTE(+witness) / UNDECIDED / EVAL-ERR over the given valuations. + Rules are zero-snap prefolded first (exact-zero literal subtrees -> '0'), so the + f64 evaluation below judges the intended denotation, not f64's rendering of it. + Rule-correlated atom valuations are appended to whatever grid the caller + supplies.""" + lhs, rhs = prefold(lhs), prefold(rhs) + valuations = list(valuations) + correlated_valuations(lhs, rhs, wildcards(list(lhs) + list(rhs))) + near = 0 + for wmap in valuations: + try: + a = eval_point(substitute(lhs, wmap)) + b = eval_point(substitute(rhs, wmap)) + except Exception as ex: + return 'EVAL-ERR', f'{type(ex).__name__}: {ex}' + an, bn = np.isnan(a), np.isnan(b) + if an and bn: + continue + if an != bn: + return 'DEMOTE', (dict(wmap), a, b) # hole filled or value lost: exact kill + if np.isinf(a) or np.isinf(b): + if a == b: + continue + return 'DEMOTE', (dict(wmap), a, b) # inf sign/finiteness mismatch: exact kill + # ONE ZERO: there is a single zero and 1/0 = +inf; the sign of an f64 zero + # is measurement rendering, never a value difference. No sign tie-break is + # applied to a `-> 0` collapse -- float == already treats -0.0 == +0.0. + rel = abs(a - b) / max(1.0, abs(a), abs(b)) + if rel <= 1e-9: + continue + if rel > 1e-6: + return 'DEMOTE', (dict(wmap), a, b) # gross finite disagreement + near += 1 # rounding band: not convicting evidence (f64 lacks authority here) + return ('UNDECIDED', near) if near else ('PROMOTE', None) + + +def valuations_for(ws, rng): + pool = ATOMS + rand_pool(rng) + k = len(ws) + total = len(pool) ** k + if total <= MAX_PRODUCT: + idx = np.stack(np.meshgrid(*[np.arange(len(pool))] * k, indexing='ij'), -1).reshape(-1, k) + else: + na = len(ATOMS) ** k + if na <= MAX_PRODUCT: + # full ATOM product (the exact kills live there) + random completions + ai = np.stack(np.meshgrid(*[np.arange(len(ATOMS))] * k, indexing='ij'), -1).reshape(-1, k) + ri = rng.integers(0, len(pool), size=(MAX_PRODUCT - na, k)) + idx = np.vstack([ai, ri]) + else: + # k >= 4: even the full ATOM product overflows MAX_PRODUCT -- SAMPLED + # atom coverage (seeded), a stated bound, not a silent truncation. + idx = rng.integers(0, len(ATOMS), size=(MAX_PRODUCT, k)) + return [{w: pool[j] for w, j in zip(ws, row)} for row in idx] + + +def load_rules(path): + raw = json.load(open(path)) + pairs = raw.items() if isinstance(raw, dict) else ((r[0], r[1]) for r in raw) + return [(tuple(k.split()) if isinstance(k, str) else tuple(k), + tuple(v.split()) if isinstance(v, str) else tuple(v)) for k, v in pairs] diff --git a/src/simplipy/promotion/_refund.py b/src/simplipy/promotion/_refund.py new file mode 100644 index 0000000..b156c02 --- /dev/null +++ b/src/simplipy/promotion/_refund.py @@ -0,0 +1,139 @@ +# mypy: ignore-errors +"""Redundancy refund: apply the ?->_ promotion, then prune rules the promoted set derives. + +Mining at the ? (variable-leaf) quantifier makes the miner spell out composite-headed +instances that broader subtree rules would otherwise (unsoundly) subsume: `* (-1) abs ?0 -> +neg abs ?0` sits alongside the base rule `* (-1) ?0 -> neg ?0`. Once the base rule passes the +pointwise bar and is promoted to the `_` (arbitrary subtree) sort, every such instance is +derivable at deploy time and can be pruned. + +Two prunes, both conservative (any mismatch keeps the rule): + 1. SYNTACTIC SUBSUMPTION (exact, sort-aware): rule B is redundant iff B = sigma(A) for + another kept rule A, where sigma maps A's `_i` to any subpattern of B and A's `?i` only + to B's `?j` leaf slots (a leaf slot may not receive a composite). + 2. SEQUENTIAL derivability probe (?-rules only): bind each `?i` to a fresh variable leaf, + simplify the lhs under the engine WITHOUT this rule; redundant iff the result equals the + rhs. Sequential so mutually-derivable siblings cannot both vanish. +""" +import re + +from ..engine import SimpliPyEngine + +Q = re.compile(r'^\?(\d+)$') + + +def refund(rules, operators, promote_set): + """Apply ?->_ for rules in ``promote_set``, then prune the derivable instances. + + ``rules``: iterable of (lhs, rhs) token sequences (all ?-sorted from the mine). + ``operators``: the engine operator config dict (``{name: {arity, realization, ...}}``), + supplying operator arities for tree parsing and the rule-free probe engine. + ``promote_set``: set of (lhs, rhs) tuples (the pointwise + const-bearing PROMOTE verdicts) + to upgrade to the `_` subtree sort. Returns the kept, sorted-and-pruned rules. + """ + OPS = operators + rules = [(tuple(l), tuple(r)) for l, r in rules] + up = lambda ts: tuple('_' + Q.match(t).group(1) if Q.match(t) else t for t in ts) + sorted_rules = [] + for lhs, rhs in rules: + if (lhs, rhs) in promote_set: + sorted_rules.append((up(lhs), up(rhs))) + else: + sorted_rules.append((lhs, rhs)) + + # PRUNE 1 -- SYNTACTIC SUBSUMPTION (exact, order-safe, sort-aware): rule B is redundant iff + # B = sigma(A) for another kept rule A, where sigma maps A's `_i` to any subpattern of B and + # A's `?i` only to B's `?j` slots (a leaf slot may not receive a composite). This refunds the + # composite-headed instances the ?-native mine spells out once their base rule is promoted + # (`* (-1) abs _0` = sigma(`* (-1) _0`), sigma: _0 -> abs _0). + def parse(ts, ops_ar): + def sub(i): + t = ts[i] + ar = ops_ar(t) + if ar is None: + return (t, ()), i + 1 + kids, j = [], i + 1 + for _ in range(ar): + k, j = sub(j) + kids.append(k) + return (t, tuple(kids)), j + tree, j = sub(0) + assert j == len(ts) + return tree + ar_map = {} + for name, props in OPS.items(): + ar_map[name] = 2 if props.get('arity', 1) == 2 else 1 + + def ops_ar(t): + a = ar_map.get(t) + return a + + def subsumes(a, b, sig): + ta, kids_a = a + if ta.startswith('_') and ta[1:].isdigit(): + if ta in sig: + return sig[ta] == b + sig[ta] = b + return True + if ta.startswith('?') and ta[1:].isdigit(): + tb, kids_b = b + if not (tb.startswith('?') and tb[1:].isdigit() and not kids_b): + return False # a leaf slot may not receive a composite or a subtree slot + if ta in sig: + return sig[ta] == b + sig[ta] = b + return True + tb, kids_b = b + if ta != tb or len(kids_a) != len(kids_b): + return False + return all(subsumes(x, y, sig) for x, y in zip(kids_a, kids_b)) + + def sub_apply(a, sig): + t, kids = a + if (t.startswith('_') or t.startswith('?')) and t[1:].isdigit(): + return sig[t] + return (t, tuple(sub_apply(k, sig) for k in kids)) + trees = [(parse(list(l), ops_ar), parse(list(r), ops_ar)) for l, r in sorted_rules] + wc_rules = [i for i, (l, r) in enumerate(sorted_rules) + if any((t.startswith('_') or t.startswith('?')) and t[1:].isdigit() for t in l)] + by_root = {} + for i in wc_rules: + by_root.setdefault(trees[i][0][0], []).append(i) + subsumed = set() + for j in wc_rules: # is rule j an instance of some other rule i? + lj, rj = trees[j] + for i in by_root.get(lj[0], []): + if i == j or i in subsumed: + continue + li, ri = trees[i] + if len(sorted_rules[i][0]) > len(sorted_rules[j][0]): + continue + sig = {} + if subsumes(li, lj, sig) and sub_apply(ri, sig) == rj: + subsumed.add(j) + break + remaining = [rl for i, rl in enumerate(sorted_rules) if i not in subsumed] + + # PRUNE 2 -- SEQUENTIAL derivability probe, ?-rules only (a ?-rule claims ONLY variable + # bindings, so a variable probe covers its whole claim; sequential so mutually-derivable + # siblings cannot both vanish). + keep, pruned = [], [] + current = list(remaining) + fresh = lambda ts: [f'x{t[1:]}' if Q.match(t) else t for t in ts] + for i in range(len(current)): + lhs, rhs = current[i] + if not any(Q.match(t) for t in lhs): + keep.append((lhs, rhs)) + continue + rest = [[list(l), list(r)] for j, (l, r) in enumerate(current) if j != i and (l, r) not in pruned] + e2 = SimpliPyEngine(operators=OPS, rules=rest) + try: + got = e2.simplify(fresh(lhs), max_pattern_length=None, mask_elementary_literals=False) + except Exception: + keep.append((lhs, rhs)) + continue + if list(got) == list(fresh(rhs)): + pruned.append((lhs, rhs)) + else: + keep.append((lhs, rhs)) + return keep From bba35139ddc0d2095bc7f9786e192a432e2aead5 Mon Sep 17 00:00:00 2001 From: psaegert Date: Wed, 22 Jul 2026 01:05:41 +0200 Subject: [PATCH 2/4] feat(verify): independent soundness-verification API (simplipy.verify) Adds a second, independent soundness authority alongside the miner's own certification: a public gate + monitor that re-judge a finished rule set. - verify_ruleset / _gate + _contract: the GATE judges every rule at its own symbolic trigger points under an arbitrary-precision contract evaluator, classifying into eight buckets. 100% coverage by construction. - monitor_ruleset / _monitor: the MONITOR runs the deployed engine over an adversarial+sampled corpus and re-judges every rewrite under its own independent high-precision evaluator, attributing violations to rules. - verify_rule: single-rule verdict. Deliberately independent of the compiled core (its own evaluator) so it cross-checks the miner rather than echoing it. Validated: the ported gate reproduces the reference gate bucket-for-bucket on the promoted (4,3) set (2897/593/0/0/2, same indices), and the monitor reproduces it violation-for-violation (poison self-test green; 0 artifact-attributed violations across seeds). Faithful, logic-exact port; lint/type checks relaxed on the vendored modules. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w --- .pre-commit-config.yaml | 4 +- src/simplipy/verify/__init__.py | 81 +++ src/simplipy/verify/_contract.py | 908 +++++++++++++++++++++++++++ src/simplipy/verify/_gate.py | 105 ++++ src/simplipy/verify/_monitor.py | 1010 ++++++++++++++++++++++++++++++ 5 files changed, 2106 insertions(+), 2 deletions(-) create mode 100644 src/simplipy/verify/__init__.py create mode 100644 src/simplipy/verify/_contract.py create mode 100644 src/simplipy/verify/_gate.py create mode 100644 src/simplipy/verify/_monitor.py diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 288b023..8c75189 100644 --- a/.pre-commit-config.yaml +++ b/.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/|src/simplipy/promotion/) + exclude: ^(tests/|experimental/|benchmarks/|src/simplipy/promotion/|src/simplipy/verify/) diff --git a/src/simplipy/verify/__init__.py b/src/simplipy/verify/__init__.py new file mode 100644 index 0000000..3bb6d88 --- /dev/null +++ b/src/simplipy/verify/__init__.py @@ -0,0 +1,81 @@ +"""Independent soundness verification for rule sets. + +This subpackage is a SECOND, independent soundness authority alongside the miner's own +certification. Where the miner certifies each rule as it is discovered (via the compiled +core), this package re-judges a *finished* rule set two ways: + +- :func:`verify_ruleset` (the GATE) judges every rule at its own symbolic trigger points + under an arbitrary-precision contract evaluator, classifying each into eight buckets + (CERTIFIED / TOLERATED / KILL / ENGINE-MISALIGN / NO-WITNESS / UNRESOLVED-COVERAGE / + UNSUPPORTED-SHAPE / JUDGE-TIMEOUT). Coverage is 100% of the rule set by construction. + +- :func:`monitor_ruleset` (the MONITOR) runs the *deployed* engine over an + adversarial-plus-sampled corpus and re-judges every input->output rewrite under an + independent high-precision evaluator, attributing any deployed-value violation to the + responsible rule. It complements the gate: a corpus sweep rather than a per-rule scan. + +Both carry poison self-tests that must pass before they are trusted. Both are deliberately +implemented independently of the compiled core so they cross-check it rather than echo it. +""" +import json + +from . import _contract, _gate, _monitor + + +def _load(rules): + """Accept a rule list ([lhs, rhs] pairs) or a path to a JSON rule file.""" + if isinstance(rules, str): + rules = json.load(open(rules)) + return rules + + +def verify_rule(lhs, rhs, deployed_check=True): + """Judge a single ``lhs -> rhs`` rule at its symbolic trigger points. + + Returns a dict with ``verdict`` (CERTIFIED / TOLERATED / KILL / ENGINE-MISALIGN / + NO-WITNESS / UNSUPPORTED-SHAPE) and the supporting witness points / measure. + """ + return _contract.judge_rule(list(lhs), list(rhs), deployed_check=deployed_check) + + +def verify_ruleset(rules, *, report_path=None, build_path=None, judge_timeout_s=30): + """Gate a whole rule set: judge every rule at its own trigger points. + + ``rules``: a list of ``[lhs, rhs]`` token-list pairs, or a path to such a JSON file. + ``report_path``: optional path to dump the full per-rule report. + ``build_path``: optional path to write the kept set (CERTIFIED + TOLERATED). + ``judge_timeout_s``: per-rule wall-clock cap (a rule that exceeds it is bucketed + JUDGE-TIMEOUT rather than blocking the sweep). + + Returns the report dict; ``report['buckets']`` maps each bucket name to the list of + rule indices in it. A rule set is clean iff only CERTIFIED / TOLERATED are non-empty. + """ + return _gate.sweep(_load(rules), report_path=report_path, build_path=build_path, + judge_timeout_s=judge_timeout_s) + + +def monitor_ruleset(rules, engine_config, *, corpus_n=6000, seed=20260718, + run_selftest=False, judge_timeout_s=10, label=''): + """Sweep the deployed engine over a corpus and attribute any violation to a rule. + + ``rules``: a list of ``[lhs, rhs]`` pairs or a path to a JSON rule file. + ``engine_config``: path to the engine config whose operator realizations define the + deployed semantics the monitor judges against. + ``run_selftest``: run the poison self-test first (raises if a known-unsound rule is + not caught and attributed). + + Returns a dict with ``violations`` (artifact-attributed), ``native`` (pre-existing + engine behavior, present even with an empty rule set), ``tolerated`` (null-event + classes), ``changed`` and ``corpus`` counts. + """ + return _monitor.monitor(_load(rules), engine_config, corpus_n=corpus_n, seed=seed, + run_selftest=run_selftest, judge_timeout_s=judge_timeout_s, + label=label) + + +def selftest(): + """Run the gate + contract judge poison self-tests. Returns True iff both pass.""" + return _gate.selftest() and _contract.selftest(verbose=False) + + +__all__ = ['verify_rule', 'verify_ruleset', 'monitor_ruleset', 'selftest'] diff --git a/src/simplipy/verify/_contract.py b/src/simplipy/verify/_contract.py new file mode 100644 index 0000000..f2ed248 --- /dev/null +++ b/src/simplipy/verify/_contract.py @@ -0,0 +1,908 @@ +# mypy: ignore-errors +#!/usr/bin/env python +"""Canonical mpmath judge for the simplification-soundness contract. + +A single implementation of the contract semantics: every soundness instrument +(the rule-completeness gate, a deployed-realization sweep, a manual review gate) +derives from this module. The judge evaluates both sides of a candidate rule +under an arbitrary-precision contract algebra and compares the results across a +battery of symbolic points and a generic grid. + +Semantics implemented here: + - One zero: neg(0) = 0, 1/0 = +inf (c/0 = sign(c)*inf, derived from c*(1/0)), + 0/0 undefined. + - Limit-completion: tanh(+-inf) = +-1, exp(-inf) = 0, log(0) = -inf, + atanh(+-1) = +-inf, 1/+-inf = 0; tan poles are UNDEFINED (two-sided); + pow(negative including -inf, non-integer) is UNDEFINED. + - The kill bar: + (a) both-sides-REAL disagreement -> KILL at any measure; + (b)/(c) disagreements involving nan/+-inf -> judged by MEASURE over data + (positive measure kills; null / Dirac-degenerate events are tolerated + and classified). + +Precision honesty: + - Battery points are SYMBOLIC (mp.pi/2 etc.), rebuilt per dps rung; f64 + renderings of transcendentals are NOT the contract's points. + - Trig outputs with |v| < 10^(-dps+10) snap to exact 0 (symbolic-cancellation + floor; battery/grid inputs are >= 1e-3 in magnitude so genuine tiny trig + values cannot occur); |v| > 10^(dps-10) is a pole -> undefined. + - Every non-eq point verdict is CONFIRMED at a second rung (dps 120); rung + disagreement -> Unresolved (the point is skipped, never convicted). + - mpmath wedge caps: |exponent| > 1e6 in pow, |arg| > 1e12 in trig -> + Unresolved. +""" +import math +import re +import numpy as np +from mpmath import mp, mpf, isnan as misnan, isinf as misinf + +np.seterr(all='ignore') +F = np.float64 + +ARITY = {'+': 2, '-': 2, '*': 2, '/': 2, 'pow': 2, + 'neg': 1, 'inv': 1, 'abs': 1, 'exp': 1, 'log': 1, + 'sin': 1, 'cos': 1, 'tan': 1, 'asin': 1, 'acos': 1, 'atan': 1, + 'sinh': 1, 'cosh': 1, 'tanh': 1, 'asinh': 1, 'acosh': 1, 'atanh': 1, + 'pow2': 1, 'pow3': 1, 'pow4': 1, 'pow5': 1, + 'pow1_2': 1, 'pow1_3': 1, 'pow1_4': 1, 'pow1_5': 1, + 'div2': 1, 'div3': 1, 'div4': 1, 'div5': 1, + 'mult2': 1, 'mult3': 1, 'mult4': 1, 'mult5': 1} +SLOT_RE = re.compile(r'^([?!_])(\d+)$') + + +class Unresolved(Exception): + """the point cannot be judged honestly at working precision -- skip, never convict""" + + +SNAP_EVENTS = [0] # incremented when a symbolic-cancellation snap / pole-guard fires; + # at such points the f64 deployed algebra evaluates a DIFFERENT point + # (a measurement artifact), so the deployed check is skipped + + +# ---------------------------------------------------------------- parse +def parse(tokens, cname=''): + toks = [cname if t == '' else t for t in tokens] + pos = 0 + + def rec(): + nonlocal pos + t = toks[pos]; pos += 1 + if t in ARITY: + return (t,) + tuple(rec() for _ in range(ARITY[t])) + if SLOT_RE.match(t) or t.startswith('': + out[cname] = 'c' + return out + + +# ---------------------------------------------------------------- contract evaluator +NAN, PINF, NINF = mpf('nan'), mpf('inf'), mpf('-inf') + + +def _z(v): + """one zero -- every zero result is THE zero (sign erased)""" + return mpf(0) if v == 0 else v + + +def _snap(v): + """symbolic-cancellation floor: trig output below the dps noise floor is exact 0; + above the pole floor it is a pole (undefined); the band between is ambiguous.""" + if misnan(v) or misinf(v): + return v + floor = mpf(10) ** (-mp.dps + 10) + ceil = mpf(10) ** (mp.dps - 10) + a = abs(v) + if a == 0: + return mpf(0) + if a < floor: + SNAP_EVENTS[0] += 1 + return mpf(0) + if a > ceil: + SNAP_EVENTS[0] += 1 + return NAN + return v + + +def _int_or_none(b): + if misnan(b) or misinf(b) or abs(b) > mpf('1e15'): + return None + ib = mp.floor(b) + return int(ib) if b == ib else None + + +def c_div(a, b): + if misnan(a) or misnan(b): + return NAN + if b == 0: + return NAN if a == 0 else (PINF if a > 0 else NINF) # c/0 = c*(1/0), 0/0 undef + if misinf(a) and misinf(b): + return NAN + if misinf(b): + return mpf(0) # one zero + return _z(a / b) + + +def c_pow(a, b): + if not misnan(a) and a == 1: + return mpf(1) + if b == 0: + return mpf(1) # x^0 = 1 incl nan^0 + if misnan(a) or misnan(b): + return NAN + if a == 0: + return mpf(0) if b > 0 else PINF # 0^neg = 1/0^pos = +inf + if not misinf(a) and abs(a) == 1 and misinf(b): + return mpf(1) # pow(+-1, +-inf) = 1 + if misinf(b): + # pow(t, +-inf) uses the spike-step semantics (|t|<1 -> 0, |t|=1 -> 1, + # |t|>1 -> +inf), magnitude-based INCLUDING negative bases -- an explicit + # exception to naive limit-completion (the sign oscillates along the integer + # lattice; the step takes the magnitude limit, deployed-consistent) + aa = abs(a) + if aa < 1: + return mpf(0) if b > 0 else PINF + return PINF if b > 0 else mpf(0) + if misinf(a): + if a > 0: + return PINF if b > 0 else mpf(0) + ib = _int_or_none(b) + if ib is None: + return NAN # pow(-inf, non-integer) undefined + if b > 0: + return NINF if ib % 2 else PINF + return mpf(0) # one zero + if a < 0: + if abs(b) > mpf('1e15'): + raise Unresolved() # integrality/parity unknowable beyond the cap: an exact + # even integer 1e16 exists and is DEFINED, so returning + # nan there would be a wrong definite value + ib = _int_or_none(b) + if ib is None: + return NAN # non-integer exponent on a negative base: undefined + v = mp.power(abs(a), b) + return _z(-v if ib % 2 else v) + if abs(b) > mpf('1e6'): + raise Unresolved() + return _z(mp.power(a, b)) + + +def _dom(fn, lo=None, hi=None, lo_open=False, hi_open=False): + def g(a): + if misnan(a): + return NAN + if lo is not None and (a < lo or (lo_open and a == lo)): + return NAN + if hi is not None and (a > hi or (hi_open and a == hi)): + return NAN + v = fn(a) + if isinstance(v, mp.mpc): + return NAN + return _z(v) + return g + + +def _trig(fn): + def g(a): + if misnan(a) or misinf(a): + return NAN + if abs(a) > mpf('1e12'): + raise Unresolved() + if fn is mp.tan: + # pole PROXIMITY, not output magnitude: tan(atan(1e43)) = 1e43 is a genuine + # huge value, not a pole -- an output-magnitude ceiling would snap it to nan + # and manufacture spurious nonzero-measure disagreements. A pole is where + # cos vanishes at working precision. + c = mp.cos(a) + if abs(c) < mpf(10) ** (-mp.dps + 10): + SNAP_EVENTS[0] += 1 # a pole at working precision is a symbolic event: + # f64 evaluates a DIFFERENT point (tan(f64-pi/2) = + # 1.6e16), so the deployed check must be skipped -- + # omitting this flag manufactures false + # ENGINE-MISALIGNs + return NAN + return _snap(mp.sin(a) / c) + return _snap(fn(a)) + return g + + +def _oddroot(k): + # the exponent 1/k MUST be built at CALL time: a module-level mpf(1)/3 freezes a + # dps-15 (import-time) approximation of 1/3 into every evaluation, producing false + # clause-(a) kills of exact odd-root identities (the dyadic roots 1/2, 1/4 are exact + # and unaffected). + def g(a): + if misnan(a): + return NAN + if misinf(a): + return a + return _z(mp.sign(a) * mp.power(abs(a), mpf(1) / k)) + return g + + +OPS = { + '+': lambda a, b: NAN if (misnan(a) or misnan(b)) else + (NAN if (misinf(a) and misinf(b) and mp.sign(a) != mp.sign(b)) else _z(a + b)), + '-': lambda a, b: NAN if (misnan(a) or misnan(b)) else + (NAN if (misinf(a) and misinf(b) and mp.sign(a) == mp.sign(b)) else _z(a - b)), + '*': lambda a, b: NAN if (misnan(a) or misnan(b)) else + (NAN if ((a == 0 and misinf(b)) or (b == 0 and misinf(a))) else _z(a * b)), + '/': c_div, 'inv': lambda a: c_div(mpf(1), a), 'pow': c_pow, + 'neg': lambda a: NAN if misnan(a) else _z(-a), + 'abs': lambda a: NAN if misnan(a) else _z(abs(a)), + 'exp': lambda a: NAN if misnan(a) else + (mpf(0) if a == NINF else (PINF if a == PINF else + (_z(mp.exp(a)) if abs(a) < mpf('1e5') else (_ for _ in ()).throw(Unresolved())))), + 'log': lambda a: NAN if misnan(a) else + (NINF if a == 0 else (NAN if a < 0 else (PINF if a == PINF else _z(mp.log(a))))), + 'sin': _trig(mp.sin), 'cos': _trig(mp.cos), 'tan': _trig(mp.tan), + 'asin': lambda a: NAN if misnan(a) else + ((_ for _ in ()).throw(Unresolved()) + if (not misinf(a) and abs(a) > 1 and abs(abs(a) - 1) < mpf(10) ** (-mp.dps + 10)) + else (NAN if abs(a) > 1 else _z(mp.asin(a)))), + 'acos': lambda a: NAN if misnan(a) else + ((_ for _ in ()).throw(Unresolved()) + if (not misinf(a) and abs(a) > 1 and abs(abs(a) - 1) < mpf(10) ** (-mp.dps + 10)) + else (NAN if abs(a) > 1 else _z(mp.acos(a)))), + 'atan': lambda a: NAN if misnan(a) else + (_z(mp.sign(a) * mp.pi / 2) if misinf(a) else _z(mp.atan(a))), + 'sinh': lambda a: NAN if misnan(a) else + (a if misinf(a) else (_z(mp.sinh(a)) if abs(a) < mpf('1e5') + else (_ for _ in ()).throw(Unresolved()))), + 'cosh': lambda a: NAN if misnan(a) else + (PINF if misinf(a) else (_z(mp.cosh(a)) if abs(a) < mpf('1e5') + else (_ for _ in ()).throw(Unresolved()))), + 'tanh': lambda a: NAN if misnan(a) else (_z(mp.sign(a)) if misinf(a) else _z(mp.tanh(a))), + 'asinh': lambda a: NAN if misnan(a) else (a if misinf(a) else _z(mp.asinh(a))), + 'acosh': lambda a: NAN if misnan(a) else + ((_ for _ in ()).throw(Unresolved()) + if (not misinf(a) and abs(a - 1) < mpf(10) ** (-mp.dps + 10)) else + (NAN if a < 1 else (PINF if a == PINF else _z(mp.acosh(a))))), + # BOUNDARY HONESTY: an argument within the working-precision band of a closed + # boundary is indistinguishable from the boundary -- dps-50 rounds tanh(100) to + # EXACTLY 1, and limit-completing that would fabricate atanh(tanh(x)) = +inf vs x, + # false-killing an exact identity on the magnitude tail. Within the band: + # Unresolved, never a verdict. + 'atanh': lambda a: NAN if misnan(a) else + ((_ for _ in ()).throw(Unresolved()) + if (not misinf(a) and abs(abs(a) - 1) < mpf(10) ** (-mp.dps + 10)) else + (NAN if abs(a) > 1 else _z(mp.atanh(a)))), + 'pow2': lambda a: c_pow(a, mpf(2)), 'pow3': lambda a: c_pow(a, mpf(3)), + 'pow4': lambda a: c_pow(a, mpf(4)), 'pow5': lambda a: c_pow(a, mpf(5)), + 'pow1_2': lambda a: c_pow(a, mpf(1) / 2), 'pow1_4': lambda a: c_pow(a, mpf(1) / 4), + 'pow1_3': _oddroot(3), 'pow1_5': _oddroot(5), + 'div2': lambda a: c_div(a, mpf(2)), 'div3': lambda a: c_div(a, mpf(3)), + 'div4': lambda a: c_div(a, mpf(4)), 'div5': lambda a: c_div(a, mpf(5)), + 'mult2': lambda a: OPS['*'](a, mpf(2)), 'mult3': lambda a: OPS['*'](a, mpf(3)), + 'mult4': lambda a: OPS['*'](a, mpf(4)), 'mult5': lambda a: OPS['*'](a, mpf(5)), +} + + +def c_eval(tree, env): + """evaluate under the contract semantics (env values: mpf/mp expressions)""" + op = tree[0] + if op == 'slot': + return env[tree[1]] + if op == 'lit': + v = tree[1] + if v == math.pi: + return mp.pi + if v == math.e: + return mp.e + return mpf(v) + # LITERAL PROVENANCE: a boundary literal WRITTEN in the rule is the exact boundary + # point. The honesty band exists for COMPUTED values that merely round into the + # precision band of the boundary; it cannot apply to a token the rule itself spells. + # atanh at a written +-1 limit-completes to +-inf; acosh at a written 1 is 0. + if op in ('atanh', 'acosh') and len(tree) == 2 and tree[1][0] == 'lit': + lv = tree[1][1] + if op == 'atanh' and lv == 1.0: + return PINF + if op == 'atanh' and lv == -1.0: + return NINF + if op == 'acosh' and lv == 1.0: + return mpf(0) + args = [c_eval(c, env) for c in tree[1:]] + return OPS[op](*args) + + +# ---------------------------------------------------------------- deployed evaluator +import simplipy.operators as _spo + + +def _wrap_arr(f): + # the numpy ARRAY path is the deployed consumer path (the 0-d scalar path + # diverges at e.g. pow(-inf, 0.5): nan vs inf) + def g(*a): + r = f(*[np.array([x], dtype=F) for x in a]) + return F(np.asarray(r).ravel()[0]) + return g + + +DEP_OPS = { + '+': lambda a, b: a + b, '-': lambda a, b: a - b, '*': lambda a, b: a * b, + '/': lambda a, b: F(np.divide(F(a), F(b))), + 'inv': lambda a: F(np.divide(F(1.0), F(a))), + 'neg': lambda a: -a, 'abs': np.abs, + 'div2': lambda a: a / F(2), 'div3': lambda a: a / F(3), + 'div4': lambda a: a / F(4), 'div5': lambda a: a / F(5), + 'mult2': lambda a: a * F(2), 'mult3': lambda a: a * F(3), + 'mult4': lambda a: a * F(4), 'mult5': lambda a: a * F(5), +} +for _n in ARITY: + _fn = getattr(_spo, _n, None) + if callable(_fn): + DEP_OPS[_n] = _wrap_arr(_fn) + + +def d_eval(tree, env): + """evaluate under the deployed engine's operator algebra (numpy array path)""" + op = tree[0] + if op == 'slot': + return env[tree[1]] + if op == 'lit': + return F(tree[1]) + args = [d_eval(c, env) for c in tree[1:]] + return F(DEP_OPS[op](*args)) + + +# ---------------------------------------------------------------- comparison +def cls_mp(v): + if misnan(v): + return ('nan',) + if misinf(v): + return ('inf', 1 if v > 0 else -1) + return ('fin', v) + + +def cls_np(v): + v = F(v) + if np.isnan(v): + return ('nan',) + if np.isinf(v): + return ('inf', 1 if v > 0 else -1) + return ('fin', float(v)) # quotient zeros: -0 == 0 + + +def compare(cl, cr, rel=mpf('1e-25')): + """-> 'eq' | 'REAL-CHANGE' (both fin, differ: clause a) | + 'EXT' | 'SHRINK' (nan vs defined: clause b) | + 'INF-CHANGE' (an infinity involved: clause c)""" + if cl[0] == 'nan' and cr[0] == 'nan': + return 'eq' + if cl[0] == 'nan': + return 'EXT' + if cr[0] == 'nan': + return 'SHRINK' + if cl[0] == 'inf' or cr[0] == 'inf': + return 'eq' if cl == cr else 'INF-CHANGE' + a, b = cl[1], cr[1] + if a == b: + return 'eq' + tol = rel * max(mpf(1), abs(mpf(a)), abs(mpf(b))) if not isinstance(a, float) \ + else 1e-9 * max(1.0, abs(a), abs(b)) + return 'eq' if abs(a - b) <= tol else 'REAL-CHANGE' + + +# ---------------------------------------------------------------- batteries +def battery_reals(): + """symbolic contract points, rebuilt at the CURRENT dps (per-rung builders)""" + return [mpf(0), mpf(1) / 2, -mpf(1) / 2, mpf(1), mpf(-1), mpf(2), mpf(-2), + mpf(3), mpf(-3), mpf(1) / 4, -mpf(1) / 4, mpf(3) / 2, -mpf(3) / 2, + mp.pi / 2, -mp.pi / 2, mp.pi, mp.pi / 4, mp.pi / 3, mp.pi / 6, + mp.e, mpf('-1.7')] + + +def battery_for(sort): + """-> list of (builder() -> mp value, tag); tags: real | dirac-inf | nullx""" + reals = [((lambda v=i: battery_reals()[v]), 'real') for i in range(len(battery_reals()))] + if sort == '?': + return reals # data is real; +-inf is outside the quantifier + if sort == '_': + return reals + [((lambda: PINF), 'dirac-inf'), ((lambda: NINF), 'dirac-inf')] + if sort == '!': + return reals + [((lambda: PINF), 'nullx'), ((lambda: NINF), 'nullx')] + raise ValueError(sort) + + +CONSTS = [2.5, -1.5, 3.0, 0.5, -0.7] # witness-fitting battery (generic values) + + +def judge_cl_battery(): + """judging battery for a SOURCE-side constant (forall c_s over R). Includes the + special rationals (pow(1,nan)=1 class) AND the SYMBOLIC transcendental atoms, + built at the CURRENT dps: a fitted constant reaches pi/2, and pow(sin(c),inf) + at c = pi/2 is the powsin class in constant space -- an f64 pi/2 misses the + coincidence by 5e-33 (a false rescue can otherwise slip through; the symbolic + constant atoms kill it correctly). A cl whose witness is unfittable (degenerate + LHS there) is skipped with a tally; only core-CONSTS failures mean NO-WITNESS.""" + return ([(lambda c=c: mpf(c)) for c in CONSTS] + + [(lambda: mpf(1)), (lambda: mpf(-1)), (lambda: mpf(0)), + (lambda: mpf(2)), (lambda: mpf(-2)), (lambda: mpf(4)), + (lambda: mpf(-4)), (lambda: mpf(5)), (lambda: mpf(-5)), + (lambda: mp.pi / 2), (lambda: -mp.pi / 2), (lambda: mp.pi), + (lambda: mp.e)]) +GRID = np.concatenate([np.linspace(-3, 3, 121), np.linspace(-20, 20, 41), + np.array([-1e4, -1e3, -300., -100., -50., -30., + 30., 50., 100., 300., 1e3, 1e4])]) + 0.0137421 +# dense center (0.05 spacing: sub-unit undefined intervals like (0.2, 0.8) are visible), +# unit-spaced mid-range, and a magnitude tail (half-line violations opening at |x|>20, +# e.g. exp-shift constructions) +MEASURE_KILL = 0.05 # fraction of the generic grid; a genuine positive-measure set + # shows as many points; single-point flukes never reach this + + +# ---------------------------------------------------------------- witness fitting +GEN = [1.7, -1.3, 0.6, 2.3, -0.8] + + +def _gen_env(names, k): + return {n: F(GEN[(k + i) % len(GEN)]) for i, n in enumerate(sorted(names))} + + +_XS = np.concatenate([-np.logspace(12, -3, 120), np.linspace(-3, 3, 81), + np.logspace(-3, 12, 120)]) + + +def fit_witness(tl, tr, shared, cl_val=None): + """fit the exists-witness for a RHS on generic reals (deployed algebra); + validated on two further generic envs; None if no witness exists/found""" + def lhs_at(env): + e = dict(env) + if cl_val is not None: + e[''] = F(cl_val) + return d_eval(tl, e) + + def rhs_at(env, c): + e = dict(env) + e[''] = F(c) + if cl_val is not None: + e[''] = F(cl_val) + return d_eval(tr, e) + + env0, L0 = None, None + for k in (0, 1, 4): + try: + e0 = _gen_env(shared, k) + v = lhs_at(e0) + if np.isfinite(v): + env0, L0 = e0, v + break + except Exception: + pass + if env0 is None: + return None + + def g(c): + try: + v = rhs_at(env0, c) + return v - L0 if np.isfinite(v) else np.nan + except Exception: + return np.nan + + vals = np.array([g(x) for x in _XS]) + ok = np.isfinite(vals) + best = None + for i in range(len(_XS) - 1): + if ok[i] and vals[i] == 0: + best = _XS[i] + break + if ok[i] and ok[i + 1] and np.sign(vals[i]) != np.sign(vals[i + 1]): + lo, hi, vlo = _XS[i], _XS[i + 1], vals[i] + for _ in range(300): + mid = 0.5 * (lo + hi) + vm = g(mid) + if not np.isfinite(vm): + break + if np.sign(vm) == np.sign(vlo): + lo, vlo = mid, vm + else: + hi = mid + best = 0.5 * (lo + hi) + break + if best is None: + for c in [1., -1., 2., -2., 0.5, -0.5, math.e, -math.e, math.pi, -math.pi]: + v = g(c) + if np.isfinite(v) and abs(v) <= 1e-9 * max(1.0, abs(L0)): + best = c + break + if best is None: + return None + for c in [1., -1., 2., -2., 3., -3., 0.5, -0.5, math.e, -math.e, math.pi, -math.pi, + round(best), round(best * 2) / 2]: + if abs(c - best) < max(1e-6, 1e-9 * abs(best)): + best = float(c) + break + for k in (2, 3): + env = _gen_env(shared, k) + try: + Lv, Rv = lhs_at(env), rhs_at(env, best) + except Exception: + return None + if np.isfinite(Lv) != np.isfinite(Rv): + return None + if np.isfinite(Lv) and abs(Lv - Rv) > 1e-4 * max(1.0, abs(Lv)): + return None + return float(best) + + +def mp_polish(tl, tr, nvars, clb, c0): + """Refine an f64-fitted exists-witness to mp precision against the CONTRACT + evaluator (the quantifier ranges over R; the f64 fit is only a starting point -- + left at f64 it manufactures 1e-17 'real changes' against exact transcendental + literals like np.e, producing false clause-(a) kills). mp secant at a generic + point; falls back to the f64 value if the landscape defeats it (any residual kill + then surfaces in the sweep for investigation, never silently).""" + old = mp.dps + try: + mp.dps = 60 + env = {} + for i, n in enumerate(sorted(nvars)): + env[n] = mpf(GEN[i % len(GEN)]) + if clb is not None: + # the EXACT battery value (symbolic builder), NOT its f64 rendering: a + # witness polished against f64-pi differs from the judge's exact mp.pi by + # ~4e-17, producing false clause-(a) kills of the witness family + env[''] = clb() + try: + target = c_eval(tl, env) + except Unresolved: + return mpf(c0) + if misnan(target) or misinf(target): + return mpf(c0) + + def h(c): + e = dict(env) + e[''] = c + v = c_eval(tr, e) + if misnan(v) or misinf(v): + raise Unresolved() + return v - target + + if c0 == 0: + return mpf(0) # an exact-zero witness stays exact: the secant otherwise + # drifts to ~1e-62 and crosses pow's discontinuity at (0,0), + # fabricating phantom events on identities + try: + a, b = mpf(c0) * (1 - mpf('1e-8')) - mpf('1e-12'), mpf(c0) * (1 + mpf('1e-8')) + mpf('1e-12') + fa, fb = h(a), h(b) + for _ in range(120): + if fb == fa: + break + c = b - fb * (b - a) / (fb - fa) + fc = h(c) + a, fa, b, fb = b, fb, c, fc + if abs(fc) <= mpf('1e-45') * max(1, abs(target)): + if abs(c) < mpf('1e-50'): + try: + if abs(h(mpf(0))) <= mpf('1e-45') * max(1, abs(target)): + return mpf(0) # snap near-zero polish results to exact 0 + except Unresolved: + pass + return c + except (Unresolved, ZeroDivisionError): + pass + return mpf(c0) + finally: + mp.dps = old + + +# ---------------------------------------------------------------- the judge +def _point_verdict(tl, tr, env_mp): + """two-rung confirmed contract verdict at one point -> (verdict|None, snapped)""" + def once(): + try: + return compare(cls_mp(c_eval(tl, env_mp())), cls_mp(c_eval(tr, env_mp()))) + except Unresolved: + return None + old = mp.dps + snap0 = SNAP_EVENTS[0] + try: + mp.dps = 50 + v1 = once() + snapped1 = SNAP_EVENTS[0] > snap0 + if v1 is None: + return None, snapped1 + if v1 == 'eq' and not snapped1: + return 'eq', False + # non-eq, OR an 'eq' that involved a snap (the snap can FABRICATE equality: + # sin(exp(-100)) = 3.7e-44 snaps to 0 at dps 50): confirm at rung 2; a + # snapped-eq that changes class at dps 120 takes rung 3. + mp.dps = 120 + v2 = once() + if v1 == v2: + return v1, snapped1 + if v1 == 'eq': + mp.dps = 250 + v3 = once() + return (v2 if v2 == v3 else None), snapped1 + return None, snapped1 + finally: + mp.dps = old + + +def judge_rule(lhs, rhs, deployed_check=True): + """-> dict: verdict CERTIFIED | TOLERATED | KILL | ENGINE-MISALIGN | NO-WITNESS, + with clause/class, points, measures. Implements the kill bar: + KILL iff a REAL-CHANGE exists at any resolved point (clause a) + or the generic-grid disagreement measure exceeds MEASURE_KILL (b/c); + ENGINE-MISALIGN iff the contract certifies but the deployed algebra + structurally diverges at a non-gap battery point / on the grid; + TOLERATED else-if any null-event disagreement exists (documented class); + CERTIFIED otherwise.""" + tl = parse(lhs, '') + tr = parse(rhs, '') + sl = slots_of(lhs, '') + sr = slots_of(rhs, '') + slots = dict(sl) + slots.update({k: v for k, v in sr.items() if k not in slots}) + nvars = {n: s for n, s in slots.items() if not n.startswith('' in slots + if lhs.count('') > 1: + # the deployed matcher binds multiple leaves INDEPENDENTLY; this + # judge models one shared symbol (diagonal only) -- rather than silently + # under-judging the off-diagonal, the shape is refused fail-closed + return {'verdict': 'UNSUPPORTED-SHAPE', 'detail': 'multiple LHS '} + + # cl battery entries: (builder, f64key). builder() gives the EXACT value at the + # current dps (symbolic atoms rebuild per rung); f64key indexes the witness map + # and feeds the f64 fitter / deployed check. + witness = {} + if has_cl: + cl_battery = [(b, float(b())) for b in judge_cl_battery()] + else: + cl_battery = [(None, None)] + core = {float(c) for c in CONSTS} + skipped_cl = [] + if has_cr: + kept_cl = [] + any_fit = False + for b, key in cl_battery: + w = fit_witness(tl, tr, set(nvars), key) + if w is None: + # distinguish: LHS UNDEFINED at this cl for the generic envs -> the rows + # are tolerated degenerate extensions (the acos(pow(c,-inf)) class), + # skip WITH tally; LHS defined but unfittable -> a genuine exists-failure + lhs_defined = False + for k in (0, 1, 4): + try: + v = d_eval(tl, dict(_gen_env(set(nvars), k), + **({'': F(key)} if key is not None else {}))) + if np.isfinite(v): + lhs_defined = True + break + except Exception: + pass + if lhs_defined and (key is None or key in core): + return {'verdict': 'NO-WITNESS', 'detail': f'cl={key} (LHS defined)'} + skipped_cl.append(key) + continue + any_fit = True + witness[key] = mp_polish(tl, tr, nvars, b, w) + kept_cl.append((b, key)) + if has_cr and not any_fit: + return {'verdict': 'NO-WITNESS', 'detail': 'no cl with a finite LHS/witness'} + cl_battery = kept_cl if has_cl else [(None, None)] + + a_kills, tolerated, dep_div = [], [], [] + resolved_pts = 0 + attempted_pts = 0 + # battery sweep (cap the slot-product deterministically) + names = sorted(nvars) + combos = [{}] + for n in names: + nxt = [] + for c in combos: + for builder, tag in battery_for(nvars[n]): + e = dict(c) + e[n] = (builder, tag) + nxt.append(e) + combos = nxt + if len(combos) > 500: + # 500 covers every <=2-slot rule exhaustively (23^2 = 529 ~ capped edge); + # sampling below that drops single-point clause-(a) violations of 2-var + # rules; >=3-slot rules keep the seeded sample + rng = np.random.default_rng(11) + combos = [combos[i] for i in rng.choice(len(combos), 500, replace=False)] + for clb, clkey in cl_battery: + cr = witness.get(clkey) if has_cr else None + for combo in combos: + tags = {n: t for n, (b, t) in combo.items()} + + def env_mp(): + e = {n: b() for n, (b, t) in combo.items()} + if clb is not None: + e[''] = clb() # exact symbolic constant at the CURRENT dps + if cr is not None: + e[''] = +cr # mpf witness, re-rounded to the current dps + return e + + v, snapped = _point_verdict(tl, tr, env_mp) + attempted_pts += 1 + if v is not None: + resolved_pts += 1 + point = {n: float(b()) for n, (b, t) in combo.items()} + if clkey is not None: + point[''] = clkey + if cr is not None: + point[''] = float(cr) + if v == 'REAL-CHANGE': + if all(t == 'real' for t in tags.values()): + a_kills.append(point) + else: + # a real-VALUED disagreement at an extension-INPUT point (+-inf + # binding) is convention-mediated (it arose through extended ops: + # e.g. one-zero's inv(-inf)=0 vs the composition limit) -- clause (c) + # territory, not clause (a): clause (a)'s authority is REAL points, + # where mathematics answers. + tolerated.append(('REAL-CHANGE@ext', point, tags)) + elif v in ('EXT', 'SHRINK', 'INF-CHANGE'): + tolerated.append((v, point, tags)) + all_real = all(t == 'real' for t in tags.values()) + if deployed_check and v in (None, 'eq') and not snapped and all_real: + try: + ed = {n: F(float(b())) for n, (b, t) in combo.items()} + if clkey is not None: + ed[''] = F(clkey) + if cr is not None: + ed[''] = F(float(cr)) + dv = compare(cls_np(d_eval(tl, ed)), cls_np(d_eval(tr, ed))) + if dv != 'eq': + dep_div.append((dv, point)) + except Exception: + pass + + # measure scan: generic grid per slot, identity binding, contract semantics + meas = 0.0 + old = mp.dps + mp.dps = 50 + try: + for cfg in (1.7, -1.3): + for n in names: + res = [] + for g in GRID: + e = {m: mpf(cfg) for m in names} + e[n] = mpf(float(g)) + if has_cl: + e[''] = mpf(CONSTS[0]) # measure scan: generic cl suffices + if has_cr: + wv = witness.get(float(CONSTS[0]) if has_cl else None) + if wv is None: + continue + e[''] = +wv + try: + res.append(compare(cls_mp(c_eval(tl, e)), cls_mp(c_eval(tr, e)))) + except Unresolved: + pass + if res: + bad = sum(1 for c in res if c != 'eq') / len(res) + meas = max(meas, bad) + finally: + mp.dps = old + + if a_kills: + return {'verdict': 'KILL', 'clause': 'a-real-change', 'points': a_kills[:3], + 'measure': meas, 'skipped_cl': skipped_cl} + if meas > MEASURE_KILL: + return {'verdict': 'KILL', 'clause': 'bc-positive-measure', 'measure': meas, + 'tolerated_events': len(tolerated), 'skipped_cl': skipped_cl} + if resolved_pts == 0 or resolved_pts / max(1, attempted_pts) < 0.25: + # "skip, never convict" must not become "skip everything, acquit": a rule whose + # battery is almost entirely Unresolved has no evidence either way (e.g. a + # 1e15-argument trig rule certifying from one resolved point). The bar is a + # FRACTION of attempted points: a ground rule with its single point resolved has + # full coverage. + return {'verdict': 'UNRESOLVED-COVERAGE', 'resolved_points': resolved_pts, + 'attempted_points': attempted_pts, 'skipped_cl': skipped_cl} + for r in ({},): + pass + if dep_div: + # contract certifies; deployed diverges. Gap class (literal-zero division / + # zero-sign) never reaches here because cls_np uses quotient zeros; what + # remains is a genuine realization split. + return {'verdict': 'ENGINE-MISALIGN', 'points': [p for _, p in dep_div[:3]], + 'kinds': sorted({k for k, _ in dep_div}), 'measure': meas} + if tolerated: + kinds = sorted({v for v, _, _ in tolerated}) + return {'verdict': 'TOLERATED', 'classes': kinds, + 'events': [(v, p) for v, p, _ in tolerated[:3]], 'measure': meas, + 'skipped_cl': skipped_cl, 'resolved_points': resolved_pts} + return {'verdict': 'CERTIFIED', 'measure': meas, 'skipped_cl': skipped_cl, + 'resolved_points': resolved_pts} + + +# ---------------------------------------------------------------- self-test +TOUCHSTONES = [ + # (lhs, rhs, expected verdict, why -- the mathematical reason) + ('+ ?0 pow sin ?0 float("inf")', '?0', 'KILL', + 'powsin: real value x+1 changed at exact pi/2 (clause a, null measure irrelevant)'), + ('pow1_2 pow2 ?0', '?0', 'KILL', + 'sqrt(x^2)->x: real values differ on x<0 (clause a + measure)'), + ('atan tan asin _0', 'asin _0', 'TOLERATED', + 'nan-caused zero-measure extension at +-1 is NOT the powsin class'), + ('/ ?0 ?0', '1', 'TOLERATED', + 'x/x->1: undefined->defined at 0 only (clause b, null set)'), + ('neg inv neg !0', 'inv !0', 'TOLERATED', + 'sign-flip family: inf-artifact at 0-events only (clause c, finite-null class)'), + ('* 0 !0', '0', 'TOLERATED', + 'absorption: exact everywhere on reals; 0*inf indeterminate at nullx events only'), + ('inv sin np.pi', 'float("inf")', 'CERTIFIED', + 'sin(pi) is exactly 0 (symbolic point + snap), 1/0 = +inf'), + ('pow4 inv pow1_4 ?0', 'pow ?0 ', 'KILL', + 'even-root extension on the negative half-line (clause b, positive measure)'), + ('pow1_2 pow float("-inf") ?0', 'pow float("inf") ?0', 'KILL', + 'pow(-inf, data): undefined a.e. (clause b, positive measure)'), + ('pow1_2 pow1_2 atanh !0', 'pow1_4 atanh !0', 'CERTIFIED', + 'pow1_4(-inf) = nan = sqrt(sqrt(-inf)): both spellings agree with the contract'), + ('/ 0 mult2 ?0', '0', 'TOLERATED', + '0/0 at x=0 is an undefined->defined null-set extension (the x/x->1 class); the ' + 'deployed zero-sign residue is a documented gap by design'), + ('neg + (-1) _0', '- 1 _0', 'CERTIFIED', + 'algebraic identity, exact everywhere incl the cancellation point (one zero)'), + ('pow sin float("inf")', '0', 'KILL', + 'powsin in CONSTANT space: at c = pi/2 (symbolic atom) the value is 1, not 0 -- ' + 'clause (a); fitted constants reach pi/2'), + ('pow1_3 pow3 _0', '_0', 'CERTIFIED', + 'cbrt(t^3) = t exactly on all of R incl negatives and +-inf (odd-root exactness)'), + ('mult3 log pow1_3 _0', 'log _0', 'CERTIFIED', + '3*log(cbrt t) = log t for t>0; both undefined for t<0; -inf vs -inf equal at 0; ' + '3*inf = inf at +inf: no disagreement event anywhere -- exactly certified'), + ('atanh tanh !0', '!0', 'CERTIFIED', + 'exactly true on ALL of R; dps-50 rounding of tanh(100) to 1 must go Unresolved at ' + 'the boundary, never fabricate +inf (boundary-honesty band)'), + # -- regression guards -- + ('+ ?0 sin exp -100', '?0', 'CERTIFIED', + 'sin(e^-100) = 3.7e-44 differs from 0 BELOW the judge resolution floor (rel 1e-25):' + ' any snap-absorbable value (<1e-40) is also below the floor, so the snap cannot' + ' fabricate an equality the tolerance would not grant; f64-mined rules cannot' + ' express sub-1e-16 discrepancies (rung-2 confirmation kept as belt-and-braces)'), + ('pow1_2 * - ?0 0.2 - ?0 0.8', 'pow1_2 abs * - ?0 0.2 - ?0 0.8', 'KILL', + 'undefined on (0.2, 0.8), measure 0.6: invisible to a coarse unit-spaced grid'), + ('+ ?0 * pow exp neg pow2 - 2 float("inf") ?0', '?0', 'KILL', + 'violates exactly at c = 2: requires the constant battery to include even integers ' + '(powsin-in-constant-space at an ordinary value)'), + ('pow abs ?0 ', 'pow abs ?0 ', 'CERTIFIED', + 'identity: the polisher must not de-snap the exact-zero witness into 1e-62 and ' + 'fabricate a pow(0,0)-crossing phantom'), + ('sin * ?0 * 1e15 + 1 1e-20', 'sin * ?0 1e15', 'UNRESOLVED-COVERAGE', + 'nearly every probe is beyond the trig wedge: no evidence either way must not ' + 'certify'), + ('- ', '0', 'UNSUPPORTED-SHAPE', + 'two LHS constants bind independently in the deployed matcher; the one-symbol ' + 'diagonal model must refuse, fail-closed'), +] + + +def selftest(verbose=True): + ok = True + for lhs, rhs, want, why in TOUCHSTONES: + r = judge_rule(lhs.split(), rhs.split()) + got = r['verdict'] + mark = 'ok ' if got == want else 'FAIL' + if got != want: + ok = False + if verbose: + print(f' [{mark}] {lhs} -> {rhs}: {got} (want {want})') + if got != want: + print(f' {r}') + print(f' reason: {why}') + return ok diff --git a/src/simplipy/verify/_gate.py b/src/simplipy/verify/_gate.py new file mode 100644 index 0000000..c62dba0 --- /dev/null +++ b/src/simplipy/verify/_gate.py @@ -0,0 +1,105 @@ +# mypy: ignore-errors +"""Rule-completeness gate: judge every shipped rule at ITS OWN trigger points. + +Coverage is 100% of the rule set by construction (unlike a corpus sweep, no rule can +escape by never firing). Judgment = ``judge_rule`` (the canonical per-rule judge): +per-sort symbolic batteries, witness-fitted constants, generic-offset measure grids, +two-rung precision confirmation, deployed-consistency check. + +Poison self-test (``selftest``): the gate must CATCH a planted clause-(a) poison, a +planted clause-(b) positive-measure poison, and a planted infinity poison, and must +NOT kill the planted phantom (the tolerated sign-flip rule). A gate that cannot catch +a poisoned rule set, or that convicts the sound, refuses to bless. +""" +import json +import signal + +from ._contract import judge_rule + + +class _JudgeTimeout(Exception): + pass + + +def _alarm(_s, _f): + raise _JudgeTimeout() + + +JUDGE_TIMEOUT_S = 30 # per-rule budget. A gate that can HANG is not a gate: mpmath has + # uninterruptible code paths that can wedge; the judge caps the + # KNOWN wedge classes and this alarm covers the unknown ones. + # Timeout -> JUDGE-TIMEOUT bucket, held out fail-closed, never + # silently skipped. + +POISONS = [ + ('pow1_2 pow2 ?0'.split(), '?0'.split(), 'KILL', + 'clause (a): sqrt(x^2)->x changes real values on x<0'), + ('pow4 pow5 pow1_2 !0'.split(), 'pow !0 '.split(), 'KILL', + 'clause (b): even-root half-line domain extension'), + ('pow1_2 pow float("-inf") ?0'.split(), 'pow float("inf") ?0'.split(), 'KILL', + 'clause (b): pow(-inf, data) undefined a.e.'), +] +PHANTOM = ('neg inv neg !0'.split(), 'inv !0'.split(), 'TOLERATED', + 'clause (c): must NOT be killed') + + +def selftest(): + print('=== rule-complete gate poison self-test ===') + ok = True + for lhs, rhs, want, why in POISONS + [PHANTOM]: + r = judge_rule(lhs, rhs) + got = r['verdict'] + good = (got == want) + ok &= good + print(f" [{'ok ' if good else 'FAIL'}] {' '.join(lhs)} -> {' '.join(rhs)}: " + f"{got} (want {want}) -- {why}") + if not good: + print(f' {r}') + print('GATE SELF-TEST', 'PASSED' if ok else 'FAILED') + return ok + + +def sweep(rules, report_path=None, build_path=None, judge_timeout_s=JUDGE_TIMEOUT_S): + signal.signal(signal.SIGALRM, _alarm) + buckets = {'CERTIFIED': [], 'TOLERATED': [], 'KILL': [], + 'ENGINE-MISALIGN': [], 'NO-WITNESS': [], + 'UNRESOLVED-COVERAGE': [], 'UNSUPPORTED-SHAPE': [], 'JUDGE-TIMEOUT': []} + detail = [] + for idx, (lhs, rhs) in enumerate(rules): + signal.alarm(judge_timeout_s) + try: + r = judge_rule(list(lhs), list(rhs)) + except _JudgeTimeout: + r = {'verdict': 'JUDGE-TIMEOUT', 'detail': f'> {judge_timeout_s}s'} + except Exception as ex: + r = {'verdict': 'NO-WITNESS', 'detail': f'judge error {type(ex).__name__}: {ex}'} + finally: + signal.alarm(0) + r['idx'] = idx + r['lhs'] = ' '.join(lhs) + r['rhs'] = ' '.join(rhs) + buckets[r['verdict']].append(idx) + detail.append(r) + if idx % 200 == 0: + print(f"[{idx}/{len(rules)}] " + + ' '.join(f'{k}={len(v)}' for k, v in buckets.items()), flush=True) + print('\n================ GATE RESULT ================') + for k, v in buckets.items(): + print(f' {k:16s} {len(v)}') + for k in ('KILL', 'ENGINE-MISALIGN', 'NO-WITNESS', 'UNRESOLVED-COVERAGE', + 'UNSUPPORTED-SHAPE', 'JUDGE-TIMEOUT'): + for i in buckets[k]: + d = detail[i] + why = d.get('clause') or ','.join(d.get('kinds', [])) or d.get('detail', '') + print(f" {k} idx {i}: {d['lhs']} -> {d['rhs']} [{why}]") + if report_path: + json.dump({'buckets': buckets, 'detail': detail}, open(report_path, 'w'), + default=str) + print(f'report -> {report_path}') + if build_path: + keep = [rules[i] for i in sorted(buckets['CERTIFIED'] + buckets['TOLERATED'])] + json.dump(keep, open(build_path, 'w')) + print(f'built {len(keep)} kept rules -> {build_path}') + return 0 if not (buckets['KILL'] or buckets['ENGINE-MISALIGN'] + or buckets['NO-WITNESS'] or buckets['UNRESOLVED-COVERAGE'] + or buckets['UNSUPPORTED-SHAPE'] or buckets['JUDGE-TIMEOUT']) else 1 diff --git a/src/simplipy/verify/_monitor.py b/src/simplipy/verify/_monitor.py new file mode 100644 index 0000000..b2a78c6 --- /dev/null +++ b/src/simplipy/verify/_monitor.py @@ -0,0 +1,1010 @@ +# mypy: ignore-errors +"""Independent deployed-realization monitor: an end-to-end soundness gate. + +This monitor is deliberately independent of the certifier's own judges. Its evaluator, +operator semantics, probe machinery, and corpus are written from the simplification +contract alone, so it can catch violations that a checker sharing the certifier's own +machinery would structurally miss. It exercises the DEPLOYED engine end-to-end +(``simplify`` on real expression shapes, with default constant masking) and judges every +rewrite under REAL (exact) semantics: + + Values are compared in mpmath (no float64 saturation/overflow); a single unsigned zero; + 1/0 = +inf; IEEE pow specials (pow(+-1, +-inf) = 1, pow(0, 0) = 1); literal folding + (np.pi -> pi). A DEFINED value may never change (checked pointwise; symbolic points such + as pi/2 are probe points). Extending an undefined point to a defined one is tolerated on + NULL sets only: extension at isolated atoms is tolerated, while extension on a large + fraction of continuum draws is a positive-measure violation. + +Verdict classes per rewrite: OK | VIOLATION (value change / shrink / positive-measure +extension) | UNSCORED (multi-slot outputs). A violation that is ALSO present under the +rules-empty engine is bucketed NATIVE-LINE (pre-existing engine behavior, not attributable +to the ruleset under test). + +Self-test: :func:`selftest` poisons a copy of the ruleset with known-unsound rules and +reports failure loudly unless the monitor flags all of them. + +Importable API: + * :func:`judge_pair` -- judge a single ``inp -> out`` rewrite. + * :func:`sweep` -- run the engine over a corpus and collect violations. + * :func:`build_engine`, :func:`make_corpus` -- engine/corpus construction. + * :func:`selftest` -- poison self-test (returns True iff every poison is caught). + * :func:`monitor` -- top-level driver (optional self-test, then the main sweep). +""" +import json +import os +import tempfile + +import numpy as np +import yaml +from mpmath import mp, mpf, isnan, isinf + +from ..engine import SimpliPyEngine +from ..utils import count_expressions, sample_expression + +DPS = 50 +REL_TOL = mpf('1e-30') +SLOT_TOL = mpf('1e-12') # slot-bound comparisons check WITNESS EXISTENCE, and the witness + # is bound as a 40-digit token (~1e-40 relative error). Phase- + # sensitive compositions amplify token error: observed at 1e-21 + # (cos of a pow tower, amplification ~1e19) -- stable across dps + # rungs, so the stability gate cannot clear it. 1e-12 sits 9 orders + # above the worst amplification observed while leaving genuine value + # changes at any consumer-relevant scale (>= 1e-9) caught. NB this + # does NOT mean sub-1e-12 changes are invisible to f64 consumers + # (f64 resolves ~1e-16); it means a 40-digit-token instrument cannot + # honestly distinguish them from its own binding noise. Exact-real + # strictness (mp-polished witnesses) is the rule-complete gate's job. + # Slot-bearing pairs: the fitted c carries secant precision ~1e-30, + # which HOVERS at REL_TOL on other probes (observed as same-displayed + # 'value changes'); slot comparisons use this looser, stated bound. +MEASURE_FRACTION = 0.15 # extension-layer disagreements (nan<->defined and infinity-involved + # changes) are judged by MEASURE over the data. ~40 continuum + # draws/pair: 0.15 = 6 draws -- far above single-draw noise, far + # below any genuine positive-measure set (half-lines show ~0.5). This + # end-to-end sweep is the realization check; the rule-complete gate is + # the primary measure instrument. Null events (atom probes incl + # +-inf) are tolerated and tallied (TOL_COUNTS) per the null-event + # doctrine. + +TOL_COUNTS = {'shrink-null': 0, 'inf-null': 0, 'ext-null': 0} +N_DRAWS = 40 # continuum draws per variable set +mp.dps = DPS + + +# --------------------------------------------------------------------------------------- +# The contract evaluator: mpmath, written from the contract semantics alone. +# --------------------------------------------------------------------------------------- + +def _nan(): + return mpf('nan') + + +class Unresolved(Exception): + """A probe whose value is UNKNOWABLE at working precision (atanh at a possibly-rounded + +-1). Distinct from nan (= genuinely undefined): an Unresolved probe is SKIPPED entirely + -- it must count neither as agreement, nor violation, nor extension measure. (Counting it + as nan fabricated 'positive-measure extension' verdicts on sound atanh(tanh(t)) chains.)""" + + +def _pole_guard(denom): + """A denominator indistinguishable from an exact pole at working precision is a pole.""" + return abs(denom) < mpf(10) ** (-(DPS - 10)) + + +def c_div(a, b): + if isnan(a) or isnan(b): + return _nan() + if isinf(a) and isinf(b): + return _nan() + if b == 0: # ONE zero; c/0 = sign(c)*inf, 0/0 = nan + if a == 0: + return _nan() + if isinf(a) or a > 0: + return mpf('inf') if (not isinf(a) or a > 0) else mpf('-inf') + return mpf('-inf') + if isinf(b): + return mpf(0) if not isinf(a) else _nan() + return a / b + + +PARITY_CAP = mpf('1e15') # beyond this an exponent's integrality/parity is unresolvable at any + # reasonable precision -- and int(mpf) on an exponent like exp(exp(700)) + # (a 10^304-bit integer) is a bignum operation that can hang the + # process. Precision-honest verdict for parity-dependent branches: + # nan (symmetric). + + +def _int_or_none(b): + """b as an exact int, None if non-integer, nan-sentinel if parity is unresolvable.""" + if abs(b) > PARITY_CAP: + return 'unresolvable' + ib = int(b) + return ib if b == ib else None + + +def c_pow(a, b): + if not isnan(a) and a == 1: + return mpf(1) # IEEE: pow(1, y) = 1 for EVERY y, including nan + if isnan(a) or isnan(b): + return mpf(1) if (not isnan(b) and b == 0) else _nan() # contract: pow(nan,0)=1 + if b == 0: + return mpf(1) # pow(0,0)=1, pow(inf,0)=1 + if a == 0: + if isinf(b): + return mpf(0) if b > 0 else mpf('inf') + return mpf(0) if b > 0 else mpf('inf') + if isinf(b): + aa = abs(a) + if aa == 1: + return mpf(1) # pow(+-1, +-inf) = 1 + if b > 0: + return mpf('inf') if aa > 1 else mpf(0) + return mpf(0) if aa > 1 else mpf('inf') + if isinf(a): + if a > 0: + return mpf('inf') if b > 0 else mpf(0) + ib = _int_or_none(b) + if ib == 'unresolvable': + return _nan() + if ib is None: + return _nan() # REAL semantics: (-inf)^non-integer is undefined + if b > 0: + return mpf('-inf') if ib % 2 else mpf('inf') + return mpf(0) # one zero: no -0 + if a < 0: + ib = _int_or_none(b) + if ib == 'unresolvable': + return _nan() + if ib is None: + return _nan() # negative base, non-integer exponent + r = _pow_mag_capped(-a, b) + return -r if ib % 2 else r + try: + return _pow_mag_capped(a, b) + except Exception: + return _nan() + + +PHASE_CAP = mpf('1e25') # a trig argument's phase mod 2pi is only knowable to the precision + # of the WEAKEST value feeding it: fitted slots are bound as 40-digit + # tokens, so phase is garbage beyond ~1e3x -- observed (cos at ~9e48 + # under an older 1e50 cap flipped sign purely from slot rounding: a + # false violation). 1e25 leaves >= 1e14 phase margin for 40-digit + # tokens. Beyond the cap: unresolved -> nan, SYMMETRICALLY on both + # sides. (Also guards mpmath's quasi-unbounded argument reduction, one + # of its uninterruptible paths.) Cost: huge-argument trig pairs go + # unjudged (coverage loss, never a wrong verdict). + + +def _trig_inf(f): + def g(x): + if isnan(x) or isinf(x) or abs(x) > PHASE_CAP: + return _nan() + return f(x) + return g + + +def c_tan(x): + if isnan(x) or isinf(x) or abs(x) > PHASE_CAP: + return _nan() + c = mp.cos(x) + if _pole_guard(c): + return _nan() # exact pole at working precision + return mp.sin(x) / c + + +def c_inv(x): + return c_div(mpf(1), x) + + +MAG_CAP = mpf('1e50') # exponent-magnitude cap: a result beyond 10^(1e50) forces mpmath's + # exponent INT to ~1e50 digits -- a single uninterruptible CPython + # bignum op (an alarm cannot fire mid-op; observed via exp/pow + # towers). Values beyond it are PRACTICALLY INFINITE for any + # consumer; returned as +-inf/0 SYMMETRICALLY on both sides, so + # comparisons at such magnitudes stay fair. + + +def c_exp(x): + if isnan(x): + return _nan() + if isinf(x): + return mpf('inf') if x > 0 else mpf(0) # exact limit values + if abs(x) > MAG_CAP: + # a FINITE huge argument: capping to +-inf/0 is NOT symmetric across + # algebraically-equal spellings (observed: 9*log((e^(cosh/4))^5) = 11.25*cosh -- + # the exp side capped to inf, the cosh side arrived finite -> false INF-CHANGE). + # The only honest verdict at such probes is unresolved. + raise Unresolved() + return mp.exp(x) + + +def _hyp(f): + def g(x): + if isnan(x): + return _nan() + if isinf(x): + if f is mp.cosh: + return mpf('inf') + return (mpf('inf') if x > 0 else mpf('-inf')) if f is mp.sinh else (mpf(1) if x > 0 else mpf(-1)) + if abs(x) > MAG_CAP: + if f is mp.tanh: + return mpf(1) if x > 0 else mpf(-1) # saturation exact to any precision + raise Unresolved() # sinh/cosh: see c_exp rationale + return f(x) + return g + + +def _pow_mag_capped(a, b): + """mp.power for finite a>0, finite b, with the exponent-magnitude guard.""" + if a == 1: + return mpf(1) + try: + mag = b * mp.log10(a) + except Exception: + return _nan() + if abs(mag) > MAG_CAP: + raise Unresolved() # see c_exp rationale + return mp.power(a, b) + + +def _odd_root(k): + def g(x): + if isnan(x): + return _nan() + if isinf(x): + return x + r = mp.power(abs(x), mpf(1) / k) + return -r if x < 0 else r + return g + + +def _even_root(k): + def g(x): + if isnan(x) or x < 0: # sign check FIRST: even root of -inf is nan + return _nan() # (isinf-first returned +inf for -inf: a live bug) + if isinf(x): + return mpf('inf') + return mp.power(x, mpf(1) / k) + return g + + +def _tot(f, dom=None, lo=None, hi=None): + def g(x): + if isnan(x): + return _nan() + if isinf(x): + return dom(x) if dom else _nan() + if lo is not None and (x < lo or x > hi): + # BOUNDARY HONESTY: an argument outside the domain by less than the working- + # precision noise floor is indistinguishable from the boundary itself (observed: + # acosh(atanh(tanh(1))) -- the roundtrip lands at 1 - 1e-50, truth is + # exactly 1). Unresolved, never a fabricated domain verdict. + band = mpf(10) ** (-mp.dps + 10) + if min(abs(x - lo), abs(x - hi)) < band: + raise Unresolved() + return _nan() + try: + return f(x) + except Exception: + return _nan() + return g + + +OPS = { + '+': (2, lambda a, b: _nan() if (isnan(a) or isnan(b)) else (_nan() if (isinf(a) and isinf(b) and (a > 0) != (b > 0)) else a + b)), + '-': (2, lambda a, b: _nan() if (isnan(a) or isnan(b)) else (_nan() if (isinf(a) and isinf(b) and (a > 0) == (b > 0)) else a - b)), + '*': (2, lambda a, b: _nan() if (isnan(a) or isnan(b)) else (_nan() if ((a == 0 and isinf(b)) or (b == 0 and isinf(a))) else a * b)), + '/': (2, c_div), + 'pow': (2, c_pow), + 'neg': (1, lambda x: _nan() if isnan(x) else -x), + 'abs': (1, lambda x: _nan() if isnan(x) else abs(x)), + 'inv': (1, c_inv), + 'exp': (1, c_exp), + 'log': (1, lambda x: _nan() if (isnan(x) or x < 0) + else (mpf('-inf') if x == 0 + else (_raise_unresolved() if x < mpf(10) ** (-mp.dps + 10) + else (mpf('inf') if isinf(x) else mp.log(x))))), + 'sin': (1, _trig_inf(mp.sin)), 'cos': (1, _trig_inf(mp.cos)), 'tan': (1, c_tan), + 'asin': (1, _tot(mp.asin, lo=-1, hi=1)), 'acos': (1, _tot(mp.acos, lo=-1, hi=1)), + 'atan': (1, _tot(mp.atan, dom=lambda x: mp.pi / 2 if x > 0 else -mp.pi / 2)), + 'sinh': (1, _hyp(mp.sinh)), + 'cosh': (1, _hyp(mp.cosh)), + 'tanh': (1, _hyp(mp.tanh)), + 'asinh': (1, _tot(mp.asinh, dom=lambda x: x)), + 'acosh': (1, lambda x: _nan() if isnan(x) + else (_raise_unresolved() if (x < 1 and 1 - x < mpf(10) ** (-mp.dps + 10)) + else (_nan() if x < 1 else (mpf('inf') if isinf(x) else mp.acosh(x))))), + # atanh at EXACTLY +-1: in composition, an argument that reads +-1 at working precision is + # indistinguishable from a saturated 1-eps (mp.tanh(11013) ROUNDS to 1 at dps 50 -- observed + # as a false +inf). Precision-honest: unresolvable -> nan. (Cost: rules that hinge on + # a literal atanh(1)=inf go unresolved here, never wrongly judged.) + # atanh at EXACTLY +-1: indistinguishable from a saturated 1-eps at working precision + # (mp.tanh(11013) rounds to 1 at dps 50) -> Unresolved, probe skipped. + 'atanh': (1, lambda x: _nan() if isnan(x) + else (_raise_unresolved() if abs(abs(x) - 1) < mpf(10) ** (-mp.dps + 10) + else (_nan() if abs(x) > 1 else mp.atanh(x)))), + 'pow2': (1, lambda x: c_pow(x, mpf(2))), 'pow3': (1, lambda x: c_pow(x, mpf(3))), + 'pow4': (1, lambda x: c_pow(x, mpf(4))), 'pow5': (1, lambda x: c_pow(x, mpf(5))), + 'pow1_2': (1, _even_root(2)), 'pow1_3': (1, _odd_root(3)), + 'pow1_4': (1, _even_root(4)), 'pow1_5': (1, _odd_root(5)), + 'mult2': (1, lambda x: _nan() if isnan(x) else 2 * x), 'mult3': (1, lambda x: _nan() if isnan(x) else 3 * x), + 'mult4': (1, lambda x: _nan() if isnan(x) else 4 * x), 'mult5': (1, lambda x: _nan() if isnan(x) else 5 * x), + 'div2': (1, lambda x: _nan() if isnan(x) else x / 2), 'div3': (1, lambda x: _nan() if isnan(x) else x / 3), + 'div4': (1, lambda x: _nan() if isnan(x) else x / 4), 'div5': (1, lambda x: _nan() if isnan(x) else x / 5), +} + +LITS = {'0': lambda: mpf(0), '1': lambda: mpf(1), '(-1)': lambda: mpf(-1), + 'np.pi': lambda: +mp.pi, 'np.e': lambda: +mp.e, + 'float("inf")': lambda: mpf('inf'), 'float("-inf")': lambda: mpf('-inf'), + 'float("nan")': _nan} + + +def _raise_unresolved(): + raise Unresolved() + + +def _slot_token(v): + """Bind a fitted slot at FULL working precision. Binding via '%r' % float(v) rounded the + constant to f64 (1e-17 error) -- which the two-rung stability gate then CORRECTLY reported + as a stable value change on perfectly sound rewrites (observed, both in flagged rules and + as ~700 spurious native-line entries).""" + s = mp.nstr(abs(v), 40) + return s if v >= 0 else f'(-{s})' + + +def evaluate(tokens, env): + """Contract-semantics value of a prefix expression at env (variable name -> mp value).""" + pos = 0 + + def walk(): + nonlocal pos + t = tokens[pos] + pos += 1 + if t in OPS: + ar, f = OPS[t] + args = [walk() for _ in range(ar)] + return f(*args) + if t in env: + return env[t] + if t in LITS: + return LITS[t]() + return mpf(t.strip('()')) + v = walk() + if pos != len(tokens): + raise ValueError(f'trailing tokens: {tokens}') + return v + + +# --------------------------------------------------------------------------------------- +# Probes and judgment +# --------------------------------------------------------------------------------------- + +def probe_points(rng): + # SYMBOLIC probes are BUILDERS, materialized inside the caller's workdps: a frozen dps-50 + # mp.pi/2 drifts off the spike at rung 2 (pi/2 +- 1e-51, where sin < 1 strictly), which + # let the pow-sin poison evaporate under the two-rung stability gate (observed, caught by + # the self-test). Rational draws are exact at every dps and stay frozen. + sym = [lambda: mpf(0), lambda: mpf(1), lambda: mpf(-1), lambda: mpf(2), lambda: mpf(-2), + lambda: mpf(3), lambda: mpf('0.5'), lambda: mpf('-0.5'), + lambda: +mp.pi, lambda: -mp.pi, lambda: mp.pi / 2, lambda: -mp.pi / 2, + lambda: mp.pi / 4, lambda: +mp.e, lambda: -mp.e, lambda: mpf(10), + lambda: mpf('inf'), lambda: mpf('-inf'), _nan] + draws = [mpf(repr(float(v))) for v in + np.concatenate([rng.normal(0, 3, N_DRAWS // 2), rng.uniform(-30, 30, N_DRAWS // 2)])] + return sym, draws + + +def variables(tokens): + return sorted({t for t in tokens if t not in OPS and t not in LITS + and t != '' and not _is_num(t)}) + + +def _is_num(t): + try: + float(t.strip('()')) + return True + except ValueError: + return False + + +def _snap_literal_zeros(tokens): + """Literal zero-snap, independently implemented: a maximal VARIABLE-FREE subtree that + denotes exact zero (sin(np.pi)) evaluates to a precision residue (1e-51 at dps 50), which + turns 0*inf = nan into +-inf and fabricates violations (observed). Two-rung test: residue + that SHRINKS quadratically with dps is an exact zero; a stable tiny value is left alone.""" + n = len(tokens) + ends = [0] * n + + def walk(i): + j = i + 1 + for _ in range(OPS.get(tokens[i], (0,))[0]): + j = walk(j) + ends[i] = j + return j + walk(0) + + def var_free(i): + return all(tokens[k] in OPS or tokens[k] in LITS or _is_num(tokens[k]) + for k in range(i, ends[i])) + out, i = list(tokens), 0 + spans = [] + while i < n: + if var_free(i) and ends[i] - i > 1: + spans.append((i, ends[i])) + i = ends[i] + else: + i += 1 + for s, e in reversed(spans): + try: + with mp.workdps(50): + a = evaluate(out[s:e], {}) + with mp.workdps(110): + b = evaluate(out[s:e], {}) + except Exception: + continue + if isnan(a) or isnan(b) or isinf(a) or isinf(b): + continue + if (a == 0 and b == 0) or (abs(a) < mpf('1e-40') and abs(b) <= abs(a) * mpf('1e-20')): + out[s:e] = ['0'] + return out + + +def judge_pair(inp, out, rng, _refit_left=1, _slot_bound=False): + """Judge one rewrite inp -> out under the contract. Returns (verdict, detail). + + `_refit_left`: on a violation while a fittable slot is bound, the bound c may be the + artifact of a DEGENERATE first fit (pow(c, x) at x = 0 fits every c). One refit at the + violating probe is allowed, re-judging from scratch with that c substituted; a second + disagreement means no single constant exists -- a genuine violation.""" + inp, out = _snap_literal_zeros(list(inp)), _snap_literal_zeros(list(out)) + if '' in inp: + # PRE-MASKED input (deployed traffic arrives masked): an input-side + # is unevaluable, so every probe threw and the pair silently judged OK -- the + # masked-scale poison was invisible on rulesets too small to fold-create + # triggers (observed in practice). Bind input-side constants to a fixed + # probe value on BOTH sides (the engine passes placeholders through verbatim, + # so the shared spelling is the shared value pre-refit). + inp = ['2.5' if t == '' else t for t in inp] + out = ['2.5' if t == '' else t for t in out] + vs = sorted(set(variables(inp)) | set(variables(out))) + n_slots = out.count('') + if n_slots > 1: + return 'UNSCORED', 'multi-slot output' + sym, draws = probe_points(rng) + + def _viol(env, msg): + """A violation -- unless a slot refit at THIS probe is available and unspent.""" + if n_slots == 1 and _refit_left > 0: + try: + a_here = evaluate(list(inp), env) + if not isnan(a_here) and not isinf(a_here): + c2 = a_here if list(out) == [''] else _fit_slot(list(out), env, a_here) + if c2 is not None: + bound = [_slot_token(c2) if t == '' else t for t in out] + return judge_pair(inp, bound, rng, _refit_left=0, _slot_bound=True) + except Exception: + pass + cinfo = f' [bound c={_fmt(slot_val)}]' if slot_val is not None else '' + return 'VIOLATION', msg + cinfo + + def envs(): + for b in sym: + yield ({v: b for v in vs} if len(vs) <= 1 else None), b, True + # independent + correlated draw grids (frozen rationals wrapped as builders) + for i, p in enumerate(draws): + if len(vs) <= 1: + yield {v: (lambda q=p: q) for v in vs}, (lambda q=p: q), False + else: + e = {v: (lambda q=draws[(i + j * 7) % len(draws)]: q) for j, v in enumerate(vs)} + yield e, (lambda q=p: q), False + if i % 4 == 0: + yield {v: (lambda q=p: q) for v in vs}, (lambda q=p: q), False + if len(vs) > 1: + for b in sym: + yield {v: b for v in vs}, b, True # correlated atoms + + slot_val = None + ext_draws = 0 + shrink_draws = 0 + inf_draws = 0 + tot_draws = 0 + for envb, pb, is_atom in envs(): + if envb is None: + continue + env = {k: f() for k, f in envb.items()} + p = pb() + try: + a = evaluate(list(inp), env) + except Exception: + continue + try: + b_tokens = list(out) + if n_slots == 1: + # bind the slot: a candidate c must fit CONSISTENTLY -- fitting at a single + # probe is unsound when that probe is DEGENERATE (out = pow(c, x) at x = 0 + # fits EVERY c; observed as a fabricated mismatch). Collect the fit here but + # VALIDATE it at later probes: an inconsistent c is re-fitted once at the + # disagreeing probe; if the refit disagrees at yet another probe, no single + # constant exists (genuine violation via the normal comparison below). + if slot_val is None and not isnan(a) and not isinf(a): + if b_tokens == ['']: + slot_val = a + elif not _informative(inp, env, a): + pass # plateau probe: wait for a responsive one + else: + # MULTI-ROOT landscapes (sin/cos compositions admit many c at one + # probe) defeat a single-start secant: collect this probe's candidate + # but VALIDATE it at a second, independent point before adopting -- + # a wrong root fits here and nowhere else (observed twice). + cand = _fit_slot(b_tokens, env, a) + if cand is not None: + ok2 = True + n_checked = 0 + # validate at THIS pair's finite-domain points: the fixed + # magic points (0.7891/-1.2345) fall outside narrow domains + # (asin-compositions) and validation silently passed on nan, + # adopting a wrong periodic root (observed on alt seeds) + for w in [mpf('0.7891'), mpf('-1.2345'), mpf('0.31'), + mpf('-0.13'), mpf('0.052'), mpf('1.9')]: + if n_checked >= 2: + break + env_v = {k: w for k in env} + try: + av = evaluate(list(inp), env_v) + if isnan(av) or isinf(av): + continue + bt = [_slot_token(cand) if t == '' else t + for t in b_tokens] + bv = evaluate(bt, env_v) + if isnan(bv) or isinf(bv): + continue + if not _informative(inp, env_v, av): + continue # saturated point: vacuous agreement + n_checked += 1 + if abs(av - bv) > SLOT_TOL * max(1, abs(av), abs(bv)): + ok2 = False + break + except Unresolved: + continue + except Exception: + continue + if ok2 and n_checked == 0: + ok2 = False # nothing validated: do not adopt blindly + try: + env_v = {k: mpf('0.31') for k in env} + av = evaluate(list(inp), env_v) + if not isnan(av) and not isinf(av): + c2 = _fit_slot(b_tokens, env_v, av) + if c2 is not None: + slot_val = c2 + except Exception: + pass + if ok2: + slot_val = cand + else: + # wrong root: re-fit at the validation point instead + try: + env_v = {k: mpf('0.7891') for k in env} + av = evaluate(list(inp), env_v) + if not isnan(av) and not isinf(av): + slot_val = _fit_slot(b_tokens, env_v, av) + except Exception: + pass + if slot_val is None: + continue + b_tokens = [_slot_token(slot_val) if t == '' else t + for t in b_tokens] + b = evaluate(b_tokens, env) + except Exception: + continue + an, bn = isnan(a), isnan(b) + if not is_atom: + tot_draws += 1 + if an and bn: + continue + if an and not bn: + if not is_atom: + ext_draws += 1 # extension on the continuum: count the measure + else: + TOL_COUNTS['ext-null'] += 1 # extension at an atom: tolerated (null set) + continue + if bn: + # defined->undefined is judged by MEASURE over data. A null event (atom probe, + # incl +-inf) is tolerated + tallied; continuum draws count. + # (NB the slot-refit escape does not apply on the measure path -- the two-point + # fit validation above already rejects degenerate constants.) + if is_atom: + TOL_COUNTS['shrink-null'] += 1 + continue + shrink_draws += 1 + continue + if isinf(a) or isinf(b): + if (isinf(a) and isinf(b) and (a > 0) == (b > 0)): + continue + # an infinity-involved disagreement is an extension-layer artifact, judged by + # MEASURE; null events tolerated (null-event doctrine). Both-sides-REAL + # disagreements (the strict value-change clause) never reach here and stay strict. + if is_atom: + TOL_COUNTS['inf-null'] += 1 + continue + inf_draws += 1 + continue + tol = SLOT_TOL if (n_slots == 1 or _slot_bound) else REL_TOL + if (n_slots == 1 or _slot_bound) and max(abs(a), abs(b)) > mpf('1e1000000'): + # exponent-amplified token noise: pow(c_token, E) vs pow(c_exact, E) differ + # by E*1e-40 relative -- at magnitudes 10^(1e28) that exceeds any fixed + # tolerance while both printed values agree to 8 digits (observed). A + # 40-digit token cannot resolve such comparisons: unresolved, tallied. + TOL_COUNTS['slot-magnitude-unres'] = TOL_COUNTS.get('slot-magnitude-unres', 0) + 1 + continue + if abs(a - b) > tol * max(1, abs(a), abs(b)) and any(isinf(v) for v in env.values()): + # a real-valued disagreement at an +-inf INPUT probe is convention-mediated + # (one-zero composition vs the limit: inv(-inf)=0 -> pi/0=+inf flips a tanh + # sign -- observed on the alt-seed sweep; the rewrite was limit-correct). + # The strict value-change clause has authority at REAL points only; +-inf-input + # events are extension-layer -> tolerated + tallied (null-in-data / degenerate). + TOL_COUNTS['inf-input-null'] = TOL_COUNTS.get('inf-input-null', 0) + 1 + continue + if abs(a - b) > tol * max(1, abs(a), abs(b)): + # PRECISION-STABILITY gate: a finite mismatch may be dps-50 rounding amplified by + # a singularity (acos near 1 turns a 1e-50 roundtrip residue into 1e-25 -- + # observed). Re-evaluate BOTH sides at the SAME point at dps 120: a true identity + # agrees at any fixed point, so a shrinking difference is rounding; a stable + # difference is a real violation. + try: + with mp.workdps(120): + env2 = {k: f() for k, f in envb.items()} + a2 = evaluate(list(inp), env2) + b2 = evaluate(b_tokens, env2) + if isnan(a2) or isnan(b2) or isinf(a2) or isinf(b2): + raise ValueError + if abs(a2 - b2) <= tol * max(1, abs(a2), abs(b2)): + continue # rounding artifact: cleared + except Exception: + pass + return _viol(env, f'value change at {_fmt(p)}: {_fmt(a)} -> {_fmt(b)}') + if tot_draws: + for cnt, label in ((ext_draws, 'EXTENSION: undefined->defined'), + (shrink_draws, 'SHRINK: defined->undefined'), + (inf_draws, 'INF-CHANGE: extension values')): + if cnt / tot_draws > MEASURE_FRACTION: + return 'VIOLATION', (f'positive-measure {label} on {cnt}/{tot_draws} ' + f'continuum draws (measure clause)') + return 'OK', None + + +CANDIDATE_CS = sorted({float(s * a * b * c / d) + for a in (1, 2, 3, 4, 5) for b in (1, 2, 3, 4, 5) + for c in (1, 2, 3, 4, 5) for d in (1, 2, 3, 4, 5, 6, 8, 9, + 10, 12, 15, 16, 20, 25, + 27, 36, 48, 64, 75, 100, + 125) + for s in (1, -1)}) + + +def _informative(inp_tokens, env, target): + """A fit/validation probe is INFORMATIVE only if the target RESPONDS to the input: + at a saturation plateau (tanh beyond ~60 is exactly 1.0 at dps 50) EVERY large + candidate matches the target, so fitting or validating there is vacuous -- observed: + a wrong constant validated on two saturated probes, then violated at the first + responsive one.""" + if not env: + return True + try: + env2 = {k: (v * (1 + mpf('1e-9')) if v != 0 else mpf('1e-12')) + for k, v in env.items()} + t2 = evaluate(list(inp_tokens), env2) + except Exception: + return False + if isnan(t2) or isinf(t2): + return False + return abs(t2 - target) > mpf('1e-35') * max(1, abs(target)) + + +def _fit_slot(out_tokens, env, target): + """Solve the single slot so out(env) == target. The masked constants in + mined rules are overwhelmingly PRODUCTS OF THE SMALL FACTORS the unary ops carry + (div2..div5, mult2..mult5), so exact candidates are tried FIRST -- a secant root in + a periodic landscape (sin/tan-wrapped outputs) can satisfy one probe and be wrong + everywhere else (observed twice on alt seeds). Secant remains the fallback.""" + for cand in CANDIDATE_CS: + toks = [_slot_token(mpf(cand)) if t == '' else t for t in out_tokens] + try: + v = evaluate(toks, env) + except Unresolved: + break + except Exception: + continue + if not isnan(v) and not isinf(v) and abs(v - target) <= mpf('1e-30') * max(1, abs(v), abs(target)): + return mpf(cand) + def f(c): + toks = [_slot_token(mpf(c)) if t == '' else t for t in out_tokens] + try: + return evaluate(toks, env) - target + except Exception: + return _nan() + def _snap(c): + # INTEGRALITY restoration: a fitted exponent c = 3 +- 1e-30 breaks pow's parity + # branch (pow(-1, 3.000..1) -> nan, a fabricated SHRINK -- observed). A fit this + # close to an integer IS that integer at fit precision. + r = mp.nint(c) + if abs(c - r) <= mpf('1e-24') * max(1, abs(c)): + return r + return c + # FULL-mp secant, no float casts: an f64-rounded slot is ~1e-17 accurate, which can + # never meet SLOT_TOL at symbolic probes (observed at pi/4: a perfectly-fitted c flagged + # as a stable same-displayed mismatch). The contract's slot semantics is exists-c-REAL. + x0, x1 = mpf(1), mpf(2) + f0, f1 = f(x0), f(x1) + for _ in range(80): + if isnan(f1) or f0 == f1: + return None + x2 = x1 - f1 * (x1 - x0) / (f1 - f0) + if isnan(x2) or isinf(x2): + return None + if abs(f(x2)) <= mpf('1e-40') * max(1, abs(target)): + return _snap(x2) + x0, f0, x1, f1 = x1, f1, x2, f(x2) + return None + + +def _fmt(v): + if isnan(v): + return 'nan' + if isinf(v): + return '+inf' if v > 0 else '-inf' + return mp.nstr(v, 8) + + +# --------------------------------------------------------------------------------------- +# Corpus, engines, the sweep +# --------------------------------------------------------------------------------------- + +ADVERSARIAL = [ + ['+', 'x0', 'pow', 'sin', 'x0', 'float("inf")'], + ['pow', 'sin', 'x0', 'float("inf")'], + ['mult4', 'pow', 'x0', 'float("inf")'], + ['-', 'exp', 'x0', 'exp', 'x0'], + ['-', 'log', 'x0', 'log', 'x0'], + ['inv', '*', '0', 'x0'], + ['/', 'log', 'x0', 'log', 'x0'], + ['atanh', 'tanh', 'sinh', 'x0'], + ['*', 'x0', 'pow', 'cos', 'x1', 'float("inf")'], + ['+', 'pow', 'tanh', 'x0', 'float("inf")', 'x1'], + ['pow', 'div5', '7.0', 'float("nan")'], + ['*', 'sin', 'np.pi', 'x0'], + ['abs', 'pow', 'x0', 'mult3', '1'], + ['tan', '+', 'x0', 'np.pi'], + ['inv', '+', '0', 'neg', 'pow2', 'pow2', 'x0'], + ['pow', 'float("-inf")', 'pow1_3', '3.0'], + # triggers for the measure-clause poison (even-root half-line extension) + ['pow4', 'pow5', 'pow1_2', 'x0'], + ['mult2', 'pow4', 'pow5', 'pow1_2', 'x1'], + # PRE-MASKED shapes (realization fidelity: deployed traffic arrives with literals + # already masked to ; also guarantees the masked-scale poison a trigger on + # ANY ruleset -- on a small ruleset the poison had no fold-created triggers and the + # self-test failed closed, observed in practice) + ['*', '', 'x0'], + ['+', '*', '', 'x1', 'x0'], + ['sin', '*', '', 'x0'], +] + +# Default leaf vocabulary used to sample the random half of the corpus. +DEFAULT_LEAVES = ['x0', 'x1', '0', '1', 'np.pi', '2.0', '(-0.5)', '3.0'] + +# Known-unsound rules for the poison self-test. Each must be a DEPLOYABLE spelling: the +# engine masks numeric literals to before matching, so a rule keyed on a bare +# literal can never fire on real traffic. Catch requires ATTRIBUTION: a flagged input whose +# output CHANGED versus the unpoisoned engine. +POISON = [((u'pow', u'sin', u'?0', u'float("inf")'), (u'0',)), + ((u'*', u'', u'?0'), (u'?0',)), + ((u'mult4', u'pow', u'?0', u'float("inf")'), (u'pow', u'?0', u'float("inf")')), + # measure-clause poison: even-root half-line extension -- must be caught via + # the positive-measure counters + ((u'pow4', u'pow5', u'pow1_2', u'?0'), (u'pow', u'?0', u''))] + + +def build_engine(rules, config_path): + """Build a deployed engine from `config_path`, overriding its ruleset with `rules`. + + `config_path` is the deployed engine config the monitor realizes against; the driver + passes the path in. `rules` is a list of (lhs, rhs) token-sequence pairs (empty for the + rules-empty baseline engine).""" + base = yaml.safe_load(open(config_path)) + d = tempfile.mkdtemp(prefix='monitor_') + with open(os.path.join(d, 'rules.json'), 'w') as fh: + json.dump([[list(l), list(r)] for l, r in rules], fh) + base['rules'] = 'rules.json' + with open(os.path.join(d, 'config.yaml'), 'w') as fh: + yaml.safe_dump(base, fh) + return SimpliPyEngine.from_config(os.path.join(d, 'config.yaml')) + + +def make_corpus(eng, n, rng, adversarial=None, leaves=None): + if adversarial is None: + adversarial = ADVERSARIAL + if leaves is None: + leaves = DEFAULT_LEAVES + non_leaf = dict(sorted(eng.operator_arity.items(), key=lambda x: x[1])) + counts = count_expressions(len(leaves), non_leaf, 10) + corpus = [list(e) for e in adversarial] + for _ in range(n): + L = int(rng.integers(3, 10)) + corpus.append(list(sample_expression(L, leaves, non_leaf, counts, rng))) + return corpus + + +class _JudgeTimeout(Exception): + pass + + +def _alarm(_sig, _frm): + raise _JudgeTimeout() + + +JUDGE_TIMEOUT_S = 10 # a single expression may not eat the sweep. mpmath has quasi-unbounded + # paths (trig argument reduction, bignum parity, and at least one more + # observed live); a gate that can HANG is not a gate. Timeouts are + # recorded as unresolved (with the offending expression printed) and + # skipped. + + +def sweep(rules, corpus, rng, baseline_engine, config_path, tag='', + judge_timeout_s=JUDGE_TIMEOUT_S): + import signal + signal.signal(signal.SIGALRM, _alarm) + eng = build_engine(rules, config_path) + viol, native, unscored, changed, timeouts = [], [], 0, 0, 0 + for i, expr in enumerate(corpus): + if tag and (i + 1) % 500 == 0: + print(f' [{tag} {i+1}/{len(corpus)}] changed={changed} viol={len(viol)} ' + f'timeouts={timeouts}', flush=True) + try: + out = list(eng.simplify(list(expr))) + except Exception as ex: + viol.append((expr, [''], f'simplify raised {type(ex).__name__}')) + continue + if out == list(expr): + continue + changed += 1 + signal.alarm(judge_timeout_s) + try: + v, detail = judge_pair(list(expr), out, rng) + except _JudgeTimeout: + timeouts += 1 + print(f' [{tag}] TIMEOUT-unresolved: {" ".join(expr)} -> {" ".join(out)}', flush=True) + continue + finally: + signal.alarm(0) + if v == 'UNSCORED': + unscored += 1 + elif v == 'VIOLATION': + try: + base_out = list(baseline_engine.simplify(list(expr))) + except Exception: + base_out = None + if base_out == out: + native.append((expr, out, detail)) + elif base_out is not None and base_out != list(expr): + # CAUSE attribution: if the rules-empty engine's own rewrite of this + # expression ALREADY violates, the violation is native (an f64-saturation + # constant fold etc.) and the ruleset merely rewrote further on top -- + # observed: a native sinh-overflow fold to inf extended the negative-base + # domain, and a SOUND rule (|x^inf|^(1/4) -> x^inf) inherited the blame + # under exact-output matching. + signal.alarm(judge_timeout_s) + try: + vb, _ = judge_pair(list(expr), base_out, rng) + except _JudgeTimeout: + vb = None + finally: + signal.alarm(0) + if vb == 'VIOLATION': + native.append((expr, out, detail)) + else: + viol.append((expr, out, detail)) + else: + viol.append((expr, out, detail)) + return viol, native, unscored, changed + + +def selftest(rules, config_path, corpus, baseline, seed, poison=None, + judge_timeout_s=JUDGE_TIMEOUT_S): + """Poison a copy of the ruleset with known-unsound rules; return True iff EVERY poison is + caught. A catch requires ATTRIBUTION: a flagged input whose output differs from the + unpoisoned (clean) engine's output. Prints a per-poison CAUGHT / *** MISSED *** line.""" + if poison is None: + poison = POISON + clean_eng = build_engine(rules, config_path) + caught = 0 + for p in poison: + v, _, _, _ = sweep(rules + [p], corpus[:600], np.random.default_rng(seed), + baseline, config_path, tag="poison", judge_timeout_s=judge_timeout_s) + attributed = [] + for expr, out, detail in v: + try: + if list(clean_eng.simplify(list(expr))) != list(out): + attributed.append((expr, out, detail)) + except Exception: + attributed.append((expr, out, detail)) + hit = len(attributed) > 0 + caught += hit + print(f' poison {" ".join(p[0])} -> {" ".join(p[1])}: ' + f'{"CAUGHT" if hit else "*** MISSED ***"} ' + f'({len(attributed)} attributed / {len(v)} flagged)') + return caught == len(poison) + + +class MonitorSelfTestError(RuntimeError): + """Raised by :func:`monitor` when the poison self-test fails to flag a known-unsound rule. + + A self-test failure means the monitor cannot be trusted to catch an unsound ruleset, so + the main sweep is not run: the gate has lost its own guarantee.""" + + +def monitor(rules, config_path, corpus_n=6000, seed=20260718, run_selftest=False, + adversarial=None, leaves=None, poison=None, judge_timeout_s=JUDGE_TIMEOUT_S, + label=''): + """Run the independent monitor against a deployed engine built from `config_path`. + + `rules` is either a list of (lhs, rhs) token-sequence pairs or a path to a JSON file of + ``[[lhs, rhs], ...]`` (loaded as tuples). When `run_selftest` is True the poison self-test + runs first and a failure raises :class:`MonitorSelfTestError` before the main sweep. + + Returns a dict with keys: rules, corpus, changed, violations, native, unscored, + tolerated, selftest_passed.""" + if adversarial is None: + adversarial = ADVERSARIAL + if leaves is None: + leaves = DEFAULT_LEAVES + if poison is None: + poison = POISON + rules = _load_rules(rules) + rng = np.random.default_rng(seed) + baseline = build_engine([], config_path) + corpus = make_corpus(baseline, corpus_n, rng, adversarial=adversarial, leaves=leaves) + print(f'monitor: {len(rules):,} rules | corpus {len(corpus):,} ' + f'({len(adversarial)} adversarial + {corpus_n:,} sampled)', flush=True) + + selftest_passed = None + if run_selftest: + selftest_passed = selftest(rules, config_path, corpus, baseline, seed, + poison=poison, judge_timeout_s=judge_timeout_s) + if not selftest_passed: + print('SELF-TEST FAILED: the monitor cannot catch a poisoned artifact') + raise MonitorSelfTestError( + 'poison self-test failed: a known-unsound rule was not flagged') + print('SELF-TEST PASSED (all poisons caught, attribution-verified)\n', flush=True) + + viol, native, unscored, changed = sweep(rules, corpus, rng, baseline, config_path, + tag="main", judge_timeout_s=judge_timeout_s) + print(f'\n=== INDEPENDENT MONITOR {label} ===') + print(f' rewritten {changed:7,} / {len(corpus):,}') + print(f' VIOLATIONS {len(viol):7,} (artifact-attributed)') + print(f' native-line {len(native):7,} (present with rules=[]; pre-existing engine behavior)') + print(f' unscored {unscored:7,} (multi-slot outputs)') + print(f' tolerated {dict(TOL_COUNTS)} (null-event doctrine)') + for expr, out, detail in viol[:15]: + print(f' VIOL {" ".join(expr)} -> {" ".join(out)} [{detail}]') + for expr, out, detail in native[:5]: + print(f' (native) {" ".join(expr)} -> {" ".join(out)} [{detail}]') + return { + 'rules': len(rules), + 'corpus': len(corpus), + 'changed': changed, + 'violations': viol, + 'native': native, + 'unscored': unscored, + 'tolerated': dict(TOL_COUNTS), + 'selftest_passed': selftest_passed, + } + + +def _load_rules(rules): + """Load rules from a JSON path (list of [lhs, rhs]) into (tuple, tuple) pairs, or pass a + pre-loaded rule list through unchanged.""" + if isinstance(rules, (str, os.PathLike)): + with open(rules) as fh: + return [(tuple(l), tuple(r)) for l, r in json.load(fh)] + return rules From 79484715b6334ee140c57de896b3fb68ca895688 Mon Sep 17 00:00:00 2001 From: psaegert Date: Wed, 22 Jul 2026 01:09:03 +0200 Subject: [PATCH 3/4] 0.8.0: version bump + changelog (native sort promotion + independent verify API) Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w --- CHANGELOG.md | 32 ++++++++++++++++++++++++++++++++ Cargo.toml | 2 +- pyproject.toml | 2 +- 3 files changed, 34 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fbb70c3..4a8ee98 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/Cargo.toml b/Cargo.toml index fcb0219..7c1a5b1 100644 --- a/Cargo.toml +++ b/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)" diff --git a/pyproject.toml b/pyproject.toml index 85b415d..8e7647d 100644 --- a/pyproject.toml +++ b/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"] From 437b913b1e9a6528882d53513a193cdf45c00cfc Mon Sep 17 00:00:00 2001 From: psaegert Date: Wed, 22 Jul 2026 01:38:10 +0200 Subject: [PATCH 4/4] fix(verify): verify_ruleset returns the report dict (buckets, is_clean, exit_code) Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w --- Cargo.lock | 2 +- src/simplipy/verify/__init__.py | 17 ++++++++++++++--- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e281ab4..ae4d08f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -361,7 +361,7 @@ dependencies = [ [[package]] name = "simplipy-core" -version = "0.7.1" +version = "0.8.0" dependencies = [ "astro-float", "pyo3", diff --git a/src/simplipy/verify/__init__.py b/src/simplipy/verify/__init__.py index 3bb6d88..2038f31 100644 --- a/src/simplipy/verify/__init__.py +++ b/src/simplipy/verify/__init__.py @@ -47,11 +47,22 @@ def verify_ruleset(rules, *, report_path=None, build_path=None, judge_timeout_s= ``judge_timeout_s``: per-rule wall-clock cap (a rule that exceeds it is bucketed JUDGE-TIMEOUT rather than blocking the sweep). - Returns the report dict; ``report['buckets']`` maps each bucket name to the list of - rule indices in it. A rule set is clean iff only CERTIFIED / TOLERATED are non-empty. + Returns the report dict: ``report['buckets']`` maps each bucket name to the list of + rule indices in it, ``report['is_clean']`` is True iff only CERTIFIED / TOLERATED are + non-empty, and ``report['exit_code']`` is 0 iff clean. """ - return _gate.sweep(_load(rules), report_path=report_path, build_path=build_path, + import tempfile + import os + tmp = report_path or os.path.join(tempfile.mkdtemp(), 'gate_report.json') + code = _gate.sweep(_load(rules), report_path=tmp, build_path=build_path, judge_timeout_s=judge_timeout_s) + report = json.load(open(tmp)) + dirty = any(report['buckets'].get(k) for k in + ('KILL', 'ENGINE-MISALIGN', 'NO-WITNESS', 'UNRESOLVED-COVERAGE', + 'UNSUPPORTED-SHAPE', 'JUDGE-TIMEOUT')) + report['is_clean'] = not dirty + report['exit_code'] = code + return report def monitor_ruleset(rules, engine_config, *, corpus_n=6000, seed=20260718,