0.8.0: native sort promotion + independent verification API#39
Merged
Conversation
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…verify API) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
…n, exit_code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Makes the public package produce the best rule sets from one command, and adds a public API to independently verify any rule set.
simplipy.promotion;find_rules(promote_sorts=True), CLI config key). After mining and pruning, every rule is re-certified at the stronger sorts and shipped at the strongest sound one —_(arbitrary subtree),!(certified-finite subtree), or?(variable-leaf fallback). Five stages (pointwise atom-lattice bar, const-bearing witness map, exact-arbiter overturn, subsumption/derivability refund,_→!→?ladder with spike refusal). Fail-safe: an uncertifiable rule stays?and loses only composite-subtree recall, never soundness. Recovers the simplification power conservative?-only rulesets leave unrealized (the limiter was sort generality, not rule count).simplipy.verify):verify_ruleset(8-bucket per-rule gate under an arbitrary-precision contract evaluator, 100% coverage),monitor_ruleset(deployed-engine corpus sweep with rule-level violation attribution under an independent high-precision evaluator),verify_rule. Deliberately independent of the compiled core — a second soundness authority that cross-checks the miner. Both carry poison self-tests.mpmath+scipyadded as offline-mining/verification dependencies.Test plan
cargo test,cargo fmt --check,cargo clippy; fullpytest tests(274 passed) on the built wheelfind_rules(promote_sorts=True)on 2-1/3-2/4-3 → gate-clean (0 KILL / 0 ENGINE-MISALIGN) and monitor 0 violations, via the public verify API🤖 Generated with Claude Code
https://claude.ai/code/session_01EhLKRZHNh5nNjLZhZqym9w