simplipy 0.6.0: sorted rule placeholders, certificate-gated matching, ~59x faster simplify, covered-rule pruning

[psaegert]

Summary

0.6.0 is a major release in three movements: a richer rule language (placeholder sorts with match-time certificates), a performance overhaul of the simplify hot path at byte-identical outputs, and new ruleset tooling (deterministic covered-rule pruning, hot-path observability), together with a documentation refresh including a formally typeset specification of the mining algorithm.

Rule language: placeholder sorts

Every placeholder in a rule now carries a sort — the binding claim its sigil encodes, enforced by the matcher at apply time:

• _i binds any subtree;
• ?i binds only a bare variable leaf;
• !i binds a variable leaf freely, but a composite subtree only when a match-time certificate proves it defined and finite almost everywhere (an adaptive interval analysis over the reals; fail-closed — what cannot be certified is not bound).

Sorts let a rule that is value-sound only for certified operands make the wider claim without giving up soundness. Newly mined rulesets emit sorted patterns; existing assets behave exactly as before, and the shipped dev_7-3 asset is unchanged.

Performance (byte-identical outputs)

• Certificate economics: certificates are evaluated once per completed syntactic match (not per candidate attempt) and memoized per call plus in a generational per-engine cache that never stops memoizing — replacing a hard-capped cache that silently degraded at scale.
• Fixpoint memoization: whole cancel/rules passes and rule-normal subtrees are memoized per call, so the convergence-confirming iteration and unchanged subexpressions cost hash lookups instead of re-scans.
• Interned tokens: the kernel runs on interned token ids with a per-engine property table (~20× fewer allocations per call).

Net effect on a 65,536-expression training-prior benchmark: large certificate-bearing rulesets simplify ~59× faster than 0.5.0; certificate-free rulesets gain ~2.3×. Verified byte-identical on ~1M expressions across four rulesets and three corpora.

Tooling

• SimpliPyEngine.prune_covered_rules() / find_rules(prune='covered') / CLI prune-covered-rules: deterministic batch remove-and-repair pruning of compositionally covered rules (strict instantiation criterion incl. composite probes for wide slots; greedy — valid, not necessarily minimal).
• simplify_counters() / reset_simplify_counters(): hot-path counters and per-stage timing for profiling batches.
• Mining: high-precision (1024-bit) rescue for const-free equivalence, provenance sidecars, per-run sampler validation, relaxed Kruskal search as the production default.

Fixes

• Term cancellation now respects non-finite algebra (0/0, inf - inf etc. no longer cancel to wrong finite values with rule application disabled).
• NaN literals propagate through constant folding; inf/nan are never absorbed into a fittable <constant>.
• One leaf-value table everywhere; affine-fit conditioning and equivalence-vacuity fixes in the miner.

Removed

• The scipy runtime dependency (dead since the 0.5.0 native constant-fit cutover) and the unused criterion dev-dependency.
• 14 dead SimpliPyEngine attributes left over from the removed pure-Python engine, utils.leaf_value, and two undocumented dev-only core methods. See CHANGELOG for the full list.

Documentation

• New: a formally typeset mining-algorithm specification (docs/algorithm.md, with PDF/LaTeX downloads and a line-to-configuration reading guide).
• Corrected: the simplify pipeline description (mask-then-sort after the fixpoint loop, longer-result guard), rule-sort semantics, a pruning guide covering both prunes, and the README installation behavior (the compiled extension is required; there is no pure-Python fallback).

Validation

• 61 Rust tests + 263 Python tests, all green; cargo check --all-targets warning-free.
• Token-exact output parity against the 0.5.0 engine on 65,536 benchmark expressions × 4 rulesets, plus two additional corpora (512k prior samples, 488k model-decoded candidates) — byte-identical throughout.
• mkdocs build --strict clean.

🤖 Generated with Claude Code

https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w