diff --git a/research/complex-restored-source29/CLAIM.json b/research/complex-restored-source29/CLAIM.json new file mode 100644 index 0000000000..908b37e219 --- /dev/null +++ b/research/complex-restored-source29/CLAIM.json @@ -0,0 +1,69 @@ +{ + "track": "complex supplier", + "assignment_seed": 29, + "random_source": "Python secrets.randbelow(100), operating-system randomness; drawn once", + "started_utc": "2026-10-13T16:31:24Z", + "claimed_utc": "2026-10-13T16:40:34Z", + "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "selected_at_base": { + "source_pr": 942, + "kappa": "1661960547713947/1000000000000000000", + "review": "docs/research/community-batch952-review.md", + "construction": "research/complex-t37-owners/PROOF.md" + }, + "candidate_tasks": [ + { + "task": "Relocate dyadic scales in the historical contracted coordinate-total factory", + "decision": "Excluded: complex-factory-scale-frontier27 already closes the fixed ADD-order scale class." + }, + { + "task": "Share coefficient preparation across consecutive X4 reads", + "decision": "Excluded: PR945/975 and PR999 already cover nearby pair/four-source and bounded target-accumulation mechanisms." + }, + { + "task": "Synthesize restored two-register CK scalar shears without using coefficient scratch", + "decision": "Chosen: extends PR883's two-register alphabet from one precondition block to CK's complete coefficient inventory; allows temporary source/target mutation and proves bounded word-metric minima without magnitude pruning." + } + ], + "scope": { + "provider": "Historical PR626 CK; seed odd selects CK rather than JP8", + "coefficients": "All 103 distinct positive absolute coefficients occurring in the two pinned CK programs; signs covered by conjugation and literal replay", + "alphabet": "Signed unit additions in both directions; negate, double, halve on either of T,S; no scratch, free swap, copy, or nonunit primitive", + "endpoint": "(T,S,W) -> (T+q*S,S,0); one private W clear is charged in addition to the two-register word", + "method": "Exact meet-in-the-middle search from the complete radius-six group ball, covering every word through length twelve; separate Fraction-matrix check", + "seed_use": "CK provider, cyclic gate traversal order, and selected diagnostic coefficient", + "stopping_rule": "Complete the fixed radius-six census and all source coefficients; no timeout-based claim or larger search restart", + "preflight": "A radius-four probe on the 37 coefficients with PR999 cost <=8 found candidate savings and established that exact enumeration is inexpensive; no optimality claim made from that probe.", + "diagnostic_coefficient": "29/8, from seed numerator 29; present in both CK orientations" + }, + "comparators": [ + 696, + 734, + 837, + 866, + 882, + 883, + 999 + ], + "coordination": "No pinned issue found via GitHub GraphQL; two open issues were unrelated. Local claim, no reservation issue opened. Open PR snapshot and targeted all-state searches inspected through PR1012.", + "expected_deliverable": "One exact finite circuit/negative-result package with source pins, shortest-word evidence, literal dirty-input replay, paid costs, precision scope, meaningful mutations, and one focused PR if useful.", + "expected_finish_utc": "2026-10-13T17:31:24Z", + "verification_reserve": "Final 15 minutes of the one-hour budget", + "attribution": "Hanson Sun (@bbMisk), substantial OpenAI Codex assistance; predecessor attribution retained", + "status": "completed", + "result": { + "coefficient_magnitudes": 103, + "ball_states": 30576, + "exact_minima": 77, + "unreached_through_length_12": 26, + "strict_improvement_magnitudes": [ + 2, + 3 + ], + "source_mutation_required_for_improvements": false, + "saved_real_primitives_per_ck_orientation": 3124, + "selected_frontier_changed": false, + "link": "https://github.com/bbMisk/integer-mult-bounds/tree/research/complex-restored-source-seed29", + "overlap_refresh_through_pr": 1026 + } +} diff --git a/research/complex-restored-source29/EXPECTED.json b/research/complex-restored-source29/EXPECTED.json new file mode 100644 index 0000000000..68a329a6f3 --- /dev/null +++ b/research/complex-restored-source29/EXPECTED.json @@ -0,0 +1,3277 @@ +{ + "schema": "restored-two-register-ck/1", + "seed": 29, + "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "provider": "historical PR626 CK", + "radius": 6, + "covered_word_length": 12, + "alphabet": [ + "t+s", + "t-s", + "s+t", + "s-t", + "2t", + "t/2", + "2s", + "s/2", + "-t", + "-s" + ], + "layer_sizes": [ + 1, + 10, + 69, + 370, + 1646, + 6312, + 22168 + ], + "ball_states": 30576, + "distance_sha256": "f5c77025594055b6e8736ed8df2b9a991e936680137004bfc187d787793c73a1", + "coefficient_count": 103, + "exact_minima": 77, + "strict_improvement_coefficients": [ + "2", + "3" + ], + "coefficients": [ + { + "coefficient": "1/64", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "1/16", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "2t", + "2t", + "2t", + "2t", + "t+s", + "t/2", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "1/8", + "two_register_minimum": 7, + "two_register_lower_bound": 7, + "word": [ + "2t", + "2t", + "2t", + "t+s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 18, + "backward": 18 + }, + "comparator_costs": { + "pr696": 6, + "pr837_binary-forward": 6, + "pr837_naf-forward": 6, + "pr837_binary-reverse": 6, + "pr837_naf-reverse": 6, + "pr882_method_on_ck": 6, + "pr999": 6 + }, + "best_comparator_cost": 6, + "minimum_complete_cost": 8, + "complete_cost_lower_bound": 8, + "strict_improvement": false + }, + { + "coefficient": "1/4", + "two_register_minimum": 5, + "two_register_lower_bound": 5, + "word": [ + "2t", + "2t", + "t+s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 6249, + "backward": 6249 + }, + "comparator_costs": { + "pr696": 5, + "pr837_binary-forward": 5, + "pr837_naf-forward": 5, + "pr837_binary-reverse": 5, + "pr837_naf-reverse": 5, + "pr882_method_on_ck": 5, + "pr999": 5 + }, + "best_comparator_cost": 5, + "minimum_complete_cost": 6, + "complete_cost_lower_bound": 6, + "strict_improvement": false + }, + { + "coefficient": "3/8", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "2t", + "t+s", + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 9, + "backward": 9 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "1/2", + "two_register_minimum": 3, + "two_register_lower_bound": 3, + "word": [ + "2t", + "t+s", + "t/2" + ], + "occurrences": { + "forward": 5834, + "backward": 5834 + }, + "comparator_costs": { + "pr696": 4, + "pr837_binary-forward": 4, + "pr837_naf-forward": 4, + "pr837_binary-reverse": 4, + "pr837_naf-reverse": 4, + "pr882_method_on_ck": 4, + "pr999": 4 + }, + "best_comparator_cost": 4, + "minimum_complete_cost": 4, + "complete_cost_lower_bound": 4, + "strict_improvement": false + }, + { + "coefficient": "5/8", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "2t", + "t+s", + "2t", + "2t", + "t+s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 5, + "backward": 5 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "3/4", + "two_register_minimum": 6, + "two_register_lower_bound": 6, + "word": [ + "t+s", + "2t", + "2t", + "t-s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 259, + "backward": 259 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 6, + "pr837_naf-reverse": 6, + "pr882_method_on_ck": 6, + "pr999": 6 + }, + "best_comparator_cost": 6, + "minimum_complete_cost": 7, + "complete_cost_lower_bound": 7, + "strict_improvement": false + }, + { + "coefficient": "7/8", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t+s", + "2t", + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 8, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 7, + "pr999": 8 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "1", + "two_register_minimum": 1, + "two_register_lower_bound": 1, + "word": [ + "t+s" + ], + "occurrences": { + "forward": 6217, + "backward": 6225 + }, + "comparator_costs": { + "pr696": 2, + "pr837_binary-forward": 2, + "pr999": 2 + }, + "best_comparator_cost": 2, + "minimum_complete_cost": 2, + "complete_cost_lower_bound": 2, + "strict_improvement": false + }, + { + "coefficient": "9/8", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t+s", + "2t", + "2t", + "2t", + "t+s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "5/4", + "two_register_minimum": 6, + "two_register_lower_bound": 6, + "word": [ + "t+s", + "2t", + "2t", + "t+s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 18, + "backward": 18 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 6, + "pr837_naf-reverse": 6, + "pr882_method_on_ck": 6, + "pr999": 6 + }, + "best_comparator_cost": 6, + "minimum_complete_cost": 7, + "complete_cost_lower_bound": 7, + "strict_improvement": false + }, + { + "coefficient": "3/2", + "two_register_minimum": 4, + "two_register_lower_bound": 4, + "word": [ + "t+s", + "2t", + "t+s", + "t/2" + ], + "occurrences": { + "forward": 89, + "backward": 89 + }, + "comparator_costs": { + "pr696": 6, + "pr837_binary-forward": 6, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 5, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 5, + "pr999": 5 + }, + "best_comparator_cost": 5, + "minimum_complete_cost": 5, + "complete_cost_lower_bound": 5, + "strict_improvement": false + }, + { + "coefficient": "7/4", + "two_register_minimum": 7, + "two_register_lower_bound": 7, + "word": [ + "t+s", + "t+s", + "2t", + "2t", + "t-s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 6, + "backward": 6 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 8, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 8, + "complete_cost_lower_bound": 8, + "strict_improvement": false + }, + { + "coefficient": "15/8", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t+s", + "t+s", + "2t", + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 9, + "pr882_method_on_ck": 8, + "pr999": 9 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "2", + "two_register_minimum": 2, + "two_register_lower_bound": 2, + "word": [ + "t+s", + "t+s" + ], + "occurrences": { + "forward": 1447, + "backward": 1447 + }, + "comparator_costs": { + "pr696": 4, + "pr837_binary-forward": 4, + "pr837_naf-forward": 4, + "pr837_binary-reverse": 4, + "pr837_naf-reverse": 4, + "pr882_method_on_ck": 4, + "pr999": 4 + }, + "best_comparator_cost": 4, + "minimum_complete_cost": 3, + "complete_cost_lower_bound": 3, + "strict_improvement": true + }, + { + "coefficient": "17/8", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t+s", + "t+s", + "2t", + "2t", + "2t", + "t+s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 9, + "pr882_method_on_ck": 8, + "pr999": 9 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "9/4", + "two_register_minimum": 7, + "two_register_lower_bound": 7, + "word": [ + "t+s", + "t+s", + "2t", + "2t", + "t+s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 5, + "backward": 5 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 8, + "pr837_naf-reverse": 8, + "pr882_method_on_ck": 7, + "pr999": 8 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 8, + "complete_cost_lower_bound": 8, + "strict_improvement": false + }, + { + "coefficient": "5/2", + "two_register_minimum": 5, + "two_register_lower_bound": 5, + "word": [ + "t+s", + "t+s", + "2t", + "t+s", + "t/2" + ], + "occurrences": { + "forward": 49, + "backward": 49 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 6, + "pr999": 7 + }, + "best_comparator_cost": 6, + "minimum_complete_cost": 6, + "complete_cost_lower_bound": 6, + "strict_improvement": false + }, + { + "coefficient": "11/4", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "t-s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 8, + "pr999": 9 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "23/8", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 5, + "backward": 5 + }, + "comparator_costs": { + "pr696": 13, + "pr837_binary-forward": 13, + "pr837_naf-forward": 13, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 9, + "pr999": 11 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "3", + "two_register_minimum": 3, + "two_register_lower_bound": 3, + "word": [ + "t+s", + "t+s", + "t+s" + ], + "occurrences": { + "forward": 115, + "backward": 115 + }, + "comparator_costs": { + "pr696": 5, + "pr837_binary-forward": 5, + "pr837_naf-forward": 6, + "pr837_binary-reverse": 6, + "pr837_naf-reverse": 8, + "pr882_method_on_ck": 5, + "pr999": 5 + }, + "best_comparator_cost": 5, + "minimum_complete_cost": 4, + "complete_cost_lower_bound": 4, + "strict_improvement": true + }, + { + "coefficient": "13/4", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "t+s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 8, + "pr999": 9 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "7/2", + "two_register_minimum": 6, + "two_register_lower_bound": 6, + "word": [ + "t+s", + "t+s", + "t+s", + "2t", + "t+s", + "t/2" + ], + "occurrences": { + "forward": 26, + "backward": 26 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 8, + "pr837_naf-reverse": 9, + "pr882_method_on_ck": 7, + "pr999": 8 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 7, + "complete_cost_lower_bound": 7, + "strict_improvement": false + }, + { + "coefficient": "29/8", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t+s", + "t+s", + "t+s", + "2t", + "t+s", + "2t", + "2t", + "t+s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 13, + "pr837_binary-forward": 13, + "pr837_naf-forward": 13, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 10, + "pr999": 11 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "15/4", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "t-s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 10, + "pr882_method_on_ck": 9, + "pr999": 10 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "31/8", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 14, + "pr837_binary-forward": 14, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 10, + "pr999": 12 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "4", + "two_register_minimum": 4, + "two_register_lower_bound": 4, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s" + ], + "occurrences": { + "forward": 403, + "backward": 403 + }, + "comparator_costs": { + "pr696": 5, + "pr837_binary-forward": 5, + "pr837_naf-forward": 5, + "pr837_binary-reverse": 5, + "pr837_naf-reverse": 5, + "pr882_method_on_ck": 5, + "pr999": 5 + }, + "best_comparator_cost": 5, + "minimum_complete_cost": 5, + "complete_cost_lower_bound": 5, + "strict_improvement": false + }, + { + "coefficient": "17/4", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "t+s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 10, + "pr882_method_on_ck": 9, + "pr999": 10 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "35/8", + "two_register_minimum": 12, + "two_register_lower_bound": 12, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "t+s", + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 13, + "pr837_binary-forward": 13, + "pr837_naf-forward": 13, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 11, + "pr999": 12 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": 13, + "complete_cost_lower_bound": 13, + "strict_improvement": false + }, + { + "coefficient": "9/2", + "two_register_minimum": 7, + "two_register_lower_bound": 7, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "t+s", + "t/2" + ], + "occurrences": { + "forward": 24, + "backward": 24 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 9, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 8, + "complete_cost_lower_bound": 8, + "strict_improvement": false + }, + { + "coefficient": "19/4", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "t-s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 10, + "pr999": 11 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "39/8", + "two_register_minimum": 12, + "two_register_lower_bound": 12, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 14, + "pr837_binary-forward": 14, + "pr837_naf-forward": 13, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 11, + "pr999": 13 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": 13, + "complete_cost_lower_bound": 13, + "strict_improvement": false + }, + { + "coefficient": "5", + "two_register_minimum": 5, + "two_register_lower_bound": 5, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "t+s" + ], + "occurrences": { + "forward": 37, + "backward": 37 + }, + "comparator_costs": { + "pr696": 6, + "pr837_binary-forward": 6, + "pr837_naf-forward": 6, + "pr837_binary-reverse": 8, + "pr837_naf-reverse": 8, + "pr882_method_on_ck": 6, + "pr999": 6 + }, + "best_comparator_cost": 6, + "minimum_complete_cost": 6, + "complete_cost_lower_bound": 6, + "strict_improvement": false + }, + { + "coefficient": "21/4", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "t+s", + "t/2", + "t/2" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 10, + "pr999": 11 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "6", + "two_register_minimum": 5, + "two_register_lower_bound": 5, + "word": [ + "t/2", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 44, + "backward": 44 + }, + "comparator_costs": { + "pr696": 6, + "pr837_binary-forward": 6, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 9, + "pr882_method_on_ck": 6, + "pr999": 6 + }, + "best_comparator_cost": 6, + "minimum_complete_cost": 6, + "complete_cost_lower_bound": 6, + "strict_improvement": false + }, + { + "coefficient": "13/2", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "2t", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "7", + "two_register_minimum": 6, + "two_register_lower_bound": 6, + "word": [ + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 24, + "backward": 24 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 10, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 7, + "complete_cost_lower_bound": 7, + "strict_improvement": false + }, + { + "coefficient": "15/2", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t+s", + "2t", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 10, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "31/4", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "2t", + "2t", + "t-s", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 13, + "pr837_binary-forward": 13, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 12, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "8", + "two_register_minimum": 6, + "two_register_lower_bound": 6, + "word": [ + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 176, + "backward": 176 + }, + "comparator_costs": { + "pr696": 6, + "pr837_binary-forward": 6, + "pr837_naf-forward": 6, + "pr837_binary-reverse": 6, + "pr837_naf-reverse": 6, + "pr882_method_on_ck": 6, + "pr999": 6 + }, + "best_comparator_cost": 6, + "minimum_complete_cost": 7, + "complete_cost_lower_bound": 7, + "strict_improvement": false + }, + { + "coefficient": "17/2", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "2t", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 5, + "backward": 5 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "9", + "two_register_minimum": 7, + "two_register_lower_bound": 7, + "word": [ + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 19, + "backward": 19 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 10, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 8, + "complete_cost_lower_bound": 8, + "strict_improvement": false + }, + { + "coefficient": "19/2", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t+s", + "2t", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "10", + "two_register_minimum": 7, + "two_register_lower_bound": 7, + "word": [ + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 15, + "backward": 15 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 9, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 8, + "complete_cost_lower_bound": 8, + "strict_improvement": false + }, + { + "coefficient": "11", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "23/2", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "2t", + "t-s", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "12", + "two_register_minimum": 7, + "two_register_lower_bound": 7, + "word": [ + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 17, + "backward": 17 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 8, + "pr837_naf-reverse": 10, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 8, + "complete_cost_lower_bound": 8, + "strict_improvement": false + }, + { + "coefficient": "13", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "27/2", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t+s", + "2t", + "t+s", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "14", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 10, + "backward": 10 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "29/2", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "2t", + "t+s", + "t/2", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "15", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t+s", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 11, + "backward": 11 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 9, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "31/2", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "2t", + "t-s", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 14, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 11, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "16", + "two_register_minimum": 8, + "two_register_lower_bound": 8, + "word": [ + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 75, + "backward": 75 + }, + "comparator_costs": { + "pr696": 7, + "pr837_binary-forward": 7, + "pr837_naf-forward": 7, + "pr837_binary-reverse": 7, + "pr837_naf-reverse": 7, + "pr882_method_on_ck": 7, + "pr999": 7 + }, + "best_comparator_cost": 7, + "minimum_complete_cost": 9, + "complete_cost_lower_bound": 9, + "strict_improvement": false + }, + { + "coefficient": "33/2", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "2t", + "t+s", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "17", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 11, + "backward": 11 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "18", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 16, + "backward": 16 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "19", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t+s", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "39/2", + "two_register_minimum": 12, + "two_register_lower_bound": 12, + "word": [ + "2t", + "t-s", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 15, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 12, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": 13, + "complete_cost_lower_bound": 13, + "strict_improvement": false + }, + { + "coefficient": "20", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 10, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "21", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "22", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "24", + "two_register_minimum": 9, + "two_register_lower_bound": 9, + "word": [ + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 10, + "complete_cost_lower_bound": 10, + "strict_improvement": false + }, + { + "coefficient": "26", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t/2", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 3, + "backward": 3 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "27", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t+s", + "t/2", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 14, + "pr837_naf-reverse": 15, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "28", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t/2", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "29", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t+s", + "t/2", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 14, + "pr837_naf-reverse": 15, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "30", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t/2", + "t+s", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 5, + "backward": 5 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "31", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t-s", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 15, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 10, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "63/2", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 14, + "pr837_binary-forward": 14, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 17, + "pr837_naf-reverse": 15, + "pr882_method_on_ck": 12, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "32", + "two_register_minimum": 10, + "two_register_lower_bound": 10, + "word": [ + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 46, + "backward": 46 + }, + "comparator_costs": { + "pr696": 8, + "pr837_binary-forward": 8, + "pr837_naf-forward": 8, + "pr837_binary-reverse": 8, + "pr837_naf-reverse": 8, + "pr882_method_on_ck": 8, + "pr999": 8 + }, + "best_comparator_cost": 8, + "minimum_complete_cost": 11, + "complete_cost_lower_bound": 11, + "strict_improvement": false + }, + { + "coefficient": "67/2", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 16, + "pr837_naf-reverse": 16, + "pr882_method_on_ck": 12, + "pr999": 12 + }, + "best_comparator_cost": 12, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "34", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t/2", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 6, + "backward": 6 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "36", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t/2", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "38", + "two_register_minimum": 12, + "two_register_lower_bound": 12, + "word": [ + "t/2", + "t+s", + "t/2", + "t+s", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 14, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 13, + "complete_cost_lower_bound": 13, + "strict_improvement": false + }, + { + "coefficient": "40", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 11, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "48", + "two_register_minimum": 11, + "two_register_lower_bound": 11, + "word": [ + "t/2", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 12, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 12, + "complete_cost_lower_bound": 12, + "strict_improvement": false + }, + { + "coefficient": "52", + "two_register_minimum": 12, + "two_register_lower_bound": 12, + "word": [ + "t/2", + "t/2", + "t+s", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 15, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": 13, + "complete_cost_lower_bound": 13, + "strict_improvement": false + }, + { + "coefficient": "54", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 15, + "pr837_naf-reverse": 16, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "58", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 15, + "pr837_naf-reverse": 16, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "60", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 14, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "62", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 16, + "pr837_naf-reverse": 15, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "63", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 5, + "backward": 5 + }, + "comparator_costs": { + "pr696": 13, + "pr837_binary-forward": 13, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 18, + "pr837_naf-reverse": 16, + "pr882_method_on_ck": 11, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "64", + "two_register_minimum": 12, + "two_register_lower_bound": 12, + "word": [ + "t/2", + "t/2", + "t/2", + "t/2", + "t+s", + "t+s", + "t+s", + "t+s", + "2t", + "2t", + "2t", + "2t" + ], + "occurrences": { + "forward": 19, + "backward": 19 + }, + "comparator_costs": { + "pr696": 9, + "pr837_binary-forward": 9, + "pr837_naf-forward": 9, + "pr837_binary-reverse": 9, + "pr837_naf-reverse": 9, + "pr882_method_on_ck": 9, + "pr999": 9 + }, + "best_comparator_cost": 9, + "minimum_complete_cost": 13, + "complete_cost_lower_bound": 13, + "strict_improvement": false + }, + { + "coefficient": "65", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 16, + "pr837_naf-reverse": 16, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "67", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 17, + "pr837_naf-reverse": 17, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "68", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 14, + "pr837_naf-reverse": 14, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "72", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 13, + "pr837_naf-reverse": 13, + "pr882_method_on_ck": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "76", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 15, + "pr837_naf-reverse": 15, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "247/2", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 17, + "pr837_binary-forward": 17, + "pr837_naf-forward": 14, + "pr837_binary-reverse": 22, + "pr837_naf-reverse": 20, + "pr999": 14 + }, + "best_comparator_cost": 14, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "125", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 14, + "pr837_binary-forward": 14, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 20, + "pr837_naf-reverse": 19, + "pr882_method_on_ck": 12, + "pr999": 12 + }, + "best_comparator_cost": 12, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "126", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 4, + "backward": 4 + }, + "comparator_costs": { + "pr696": 14, + "pr837_binary-forward": 14, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 19, + "pr837_naf-reverse": 17, + "pr882_method_on_ck": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "128", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 5, + "backward": 5 + }, + "comparator_costs": { + "pr696": 10, + "pr837_binary-forward": 10, + "pr837_naf-forward": 10, + "pr837_binary-reverse": 10, + "pr837_naf-reverse": 10, + "pr999": 10 + }, + "best_comparator_cost": 10, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "257/2", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 13, + "pr837_binary-forward": 13, + "pr837_naf-forward": 13, + "pr837_binary-reverse": 19, + "pr837_naf-reverse": 19, + "pr999": 13 + }, + "best_comparator_cost": 13, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "130", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 17, + "pr837_naf-reverse": 17, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "134", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 18, + "pr837_naf-reverse": 18, + "pr999": 12 + }, + "best_comparator_cost": 12, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "249", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 15, + "pr837_binary-forward": 15, + "pr837_naf-forward": 13, + "pr837_binary-reverse": 22, + "pr837_naf-reverse": 21, + "pr999": 13 + }, + "best_comparator_cost": 13, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "252", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 15, + "pr837_binary-forward": 15, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 20, + "pr837_naf-reverse": 18, + "pr999": 12 + }, + "best_comparator_cost": 12, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "255", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 17, + "pr837_binary-forward": 17, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 24, + "pr837_naf-reverse": 20, + "pr999": 12 + }, + "best_comparator_cost": 12, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "256", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 2, + "backward": 2 + }, + "comparator_costs": { + "pr696": 11, + "pr837_binary-forward": 11, + "pr837_naf-forward": 11, + "pr837_binary-reverse": 11, + "pr837_naf-reverse": 11, + "pr999": 11 + }, + "best_comparator_cost": 11, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "260", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 18, + "pr837_naf-reverse": 18, + "pr999": 12 + }, + "best_comparator_cost": 12, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + }, + { + "coefficient": "512", + "two_register_minimum": null, + "two_register_lower_bound": 13, + "word": null, + "occurrences": { + "forward": 1, + "backward": 1 + }, + "comparator_costs": { + "pr696": 12, + "pr837_binary-forward": 12, + "pr837_naf-forward": 12, + "pr837_binary-reverse": 12, + "pr837_naf-reverse": 12, + "pr999": 12 + }, + "best_comparator_cost": 12, + "minimum_complete_cost": null, + "complete_cost_lower_bound": 14, + "strict_improvement": false + } + ], + "scalar_replays": { + "forward": { + "pr696": { + "input_columns": 725, + "native_columns": 716, + "scalar_macros": 21936, + "replaced_macros": 0, + "real_component_primitives": 169618, + "one_component_operations": { + "add": 11919, + "clear": 21459, + "copy": 15234, + "double": 5585, + "halve": 19499, + "negate": 348, + "subtract": 10765 + }, + "exact_row_l1_peak": "5120", + "exact_denominator_bits": 3, + "cancellation_free_peak": "920709848294", + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_stream_sha256": "f5a5a1f90a41884da913642f43381b5f5d64a5afba956c1ae0a8222542c0186f", + "endpoint_sha256": "f1533caad12b1987e776bb5b69891614747a28260257366f50ea517493ee99f6", + "endpoint_private_cells_cleared": true, + "endpoint_native_helpers_restored": true + }, + "direct_shortcuts": { + "input_columns": 725, + "native_columns": 716, + "scalar_macros": 21936, + "replaced_macros": 1562, + "real_component_primitives": 166494, + "one_component_operations": { + "add": 12526, + "clear": 21459, + "copy": 13672, + "double": 4023, + "halve": 19499, + "negate": 348, + "subtract": 11720 + }, + "exact_row_l1_peak": "5120", + "exact_denominator_bits": 3, + "cancellation_free_peak": "920709848294", + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_stream_sha256": "67d40d27b2a7b131d8ebced584cdff0dd270d6b98e11206f60f3fb7a64009862", + "endpoint_sha256": "f1533caad12b1987e776bb5b69891614747a28260257366f50ea517493ee99f6", + "endpoint_private_cells_cleared": true, + "endpoint_native_helpers_restored": true + }, + "saved_real_primitives": 3124 + }, + "backward": { + "pr696": { + "input_columns": 725, + "native_columns": 716, + "scalar_macros": 21936, + "replaced_macros": 0, + "real_component_primitives": 169634, + "one_component_operations": { + "add": 12118, + "clear": 21467, + "copy": 15226, + "double": 5585, + "halve": 19499, + "negate": 348, + "subtract": 10574 + }, + "exact_row_l1_peak": "4847", + "exact_denominator_bits": 8, + "cancellation_free_peak": "146068000389976309073/32", + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_stream_sha256": "f94c6e048fd9de54ac92f781d5e3b55ac56ae5eb27d93270d702510fda55511a", + "endpoint_sha256": "84875871c81c205719ceb6d629a05fb0ed0894a3f2bc3d44be13e0ee6d5064b2", + "endpoint_private_cells_cleared": true, + "endpoint_native_helpers_restored": true + }, + "direct_shortcuts": { + "input_columns": 725, + "native_columns": 716, + "scalar_macros": 21936, + "replaced_macros": 1562, + "real_component_primitives": 166510, + "one_component_operations": { + "add": 12958, + "clear": 21467, + "copy": 13664, + "double": 4023, + "halve": 19499, + "negate": 348, + "subtract": 11296 + }, + "exact_row_l1_peak": "4847", + "exact_denominator_bits": 8, + "cancellation_free_peak": "146068000389976309073/32", + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_stream_sha256": "9bc505f8d887526fef1ae509949772526627822a97144cdef4da9bb89c00e0c0", + "endpoint_sha256": "84875871c81c205719ceb6d629a05fb0ed0894a3f2bc3d44be13e0ee6d5064b2", + "endpoint_private_cells_cleared": true, + "endpoint_native_helpers_restored": true + }, + "saved_real_primitives": 3124 + } + }, + "negative_controls": [ + "missing_source_read", + "wrong_sign", + "dirty_work_not_cleared", + "source_not_restored", + "target_dirt_lost", + "work_dirt_used_as_source", + "source_target_alias", + "source_work_alias", + "nondyadic", + "missing_gate_from_alphabet" + ], + "kappa_claim": "none; selected frontier unchanged" +} diff --git a/research/complex-restored-source29/OVERLAP.json b/research/complex-restored-source29/OVERLAP.json new file mode 100644 index 0000000000..32eba40a78 --- /dev/null +++ b/research/complex-restored-source29/OVERLAP.json @@ -0,0 +1,154 @@ +{ + "initial_open_prs": 707, + "refresh_open_prs": 721, + "reviewed_through": 1026, + "pinned_coordination_issues": [], + "comparison_heads": [ + { + "number": 975, + "head": "4b40489c3e0f5819d00251de179a9ea7b1acfba8" + }, + { + "number": 981, + "head": "6c9dc6d180ac0fde42c1c2b0fe549d5a13851cf9" + }, + { + "number": 984, + "head": "51b8bce91ab21e1fffa42a907c5de3439551decb" + }, + { + "number": 999, + "head": "fd38a824adb3a5c60c101a86c950a6d590454adf" + }, + { + "number": 1011, + "head": "e978aa0ca28612afe47f487be7c7f102cfabe9b9" + }, + { + "number": 882, + "head": "e698981e0ffa680b6c5896dace1609025b97ad70" + }, + { + "number": 883, + "head": "b31a870a3842b37f6ab97767c506ce91783632a2" + }, + { + "number": 734, + "head": "ba76ba3321d000c8996b0b254bcf0d7260e1bbb6" + }, + { + "number": 755, + "head": "a1dd9f819102c40e0b5e4a75215cf69ee864f480" + }, + { + "number": 811, + "head": "b5c244c916dd0b30957332edad7ae7ae22b0eb9d" + } + ], + "new_arrivals": [ + { + "number": 1026, + "title": "[Lean] Prove all-length cyclic Schur elimination and indexed passes (no new kappa)", + "head": "c4be063c0afb634db7aa02bc1876ff29640bec65" + }, + { + "number": 1025, + "title": "Research: averaged cyclotomic heights give O(r\u00b2 log\u00b2 r) precision (no new kappa)", + "head": "6ef2168ac90d42926bceb7ac9b2e029463800c76" + }, + { + "number": 1024, + "title": "Research consolidation: reconcile archived R714 local replay (no new kappa)", + "head": "86a21357eb64d154f1b641c720c73627df68d71b" + }, + { + "number": 1023, + "title": "Research note: PR589 bit hosting is width-8 optimal; width-7 residuals worth up to +17-23% bit headroom (no new kappa)", + "head": "babca68167d8db321d194b7dc54230d88a8ad5f0" + }, + { + "number": 1022, + "title": "Conditional \u03ba = 0.001672081255752945: sixteen-replica owner controller on the seven-slot k8 word", + "head": "58618bcbfe88a252467755fc283c04c3db5ca4fd" + }, + { + "number": 1021, + "title": "Research: heterogeneous stage-rank rigidity for exact two-bank exchange", + "head": "2f88079208acdc4ae644934668ffee7673de7b01" + }, + { + "number": 1020, + "title": "Research: certify the first cost-six root-pair threshold at 26 punctures", + "head": "bf4ee95df4ee6e3101a88f5d015c8aa85b688b6d" + }, + { + "number": 1019, + "title": "Conditional \u03ba = 0.001661960547713947858091 by exact T37 grid refinement", + "head": "eff657644137971f6e31ac3c825950c770471349" + }, + { + "number": 1018, + "title": "Conditional \u03ba = 0.00167166528321877: seven triangle-hybrid slots (PR987 search) on the k8 leaver word", + "head": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef" + }, + { + "number": 1017, + "title": "Independent verification: complete R439 single-ADD omission atlas", + "head": "b66839f4707e4580524b0f4031d4edc1be939e27" + }, + { + "number": 1016, + "title": "Negative result: PR952 frame assignments cannot improve its bit moment", + "head": "83e8e4ce9a556eb890c02af79b43b1505fd9cead" + }, + { + "number": 1015, + "title": "Finite bit construction: multi-write shear programs for all ten R439 phase-B blocks (24,305 -> 24,053 ADDs, no new kappa)", + "head": "7588c797f4a4e9f2b9fc663cfa6e35afcac05e06" + }, + { + "number": 1014, + "title": "Research note: 30 all-dimension parity edge obstructions beyond local frames", + "head": "830842d08c48d7b7f6847882d065157b3e978b3c" + }, + { + "number": 1013, + "title": "Research consolidation: bind and independently replay the historical prime-subset ceiling (no new kappa)", + "head": "aaa05c733451ae2ce986b448c43b5d0926655159" + } + ], + "distinction": "PR883 treats one X4 precondition block. PR882 treats bounded single-scratch JP8 circuits. PR999 uses read-only sources and target accumulation. This package proves the complete two-register CK improvement exclusion and replays only the direct 2/3 exceptions; no savings with pending complete programs are added.", + "final_refresh_through_pr": 1034, + "final_nearby": [ + { + "number": 1032, + "head": "d12585673cb30deabad6df7f5da78f86c7ca3121", + "paths": [ + "research/factory-persistent-work-seed23/CERTIFICATE.json", + "research/factory-persistent-work-seed23/CLAIM.md", + "research/factory-persistent-work-seed23/LICENSE", + "research/factory-persistent-work-seed23/NOTICE.md", + "research/factory-persistent-work-seed23/PR_BODY.md", + "research/factory-persistent-work-seed23/README.md", + "research/factory-persistent-work-seed23/SOURCES.json", + "research/factory-persistent-work-seed23/VALIDATION.json", + "research/factory-persistent-work-seed23/independent.py", + "research/factory-persistent-work-seed23/search.py" + ] + }, + { + "number": 1033, + "head": "20b584994d99da1acd866b12eebc59e561ea3e15", + "paths": [ + "research/factory-window-synthesis-seed23/CLAIM.json", + "research/factory-window-synthesis-seed23/EXPECTED.json", + "research/factory-window-synthesis-seed23/README.md", + "research/factory-window-synthesis-seed23/SOURCES.json", + "research/factory-window-synthesis-seed23/independent.py", + "research/factory-window-synthesis-seed23/test_package.py", + "research/factory-window-synthesis-seed23/verify.py" + ] + } + ], + "final_distinction": "PR1032 studies persistent coefficient work across the contracted factory; PR1033 studies short factory windows with changed topology. This package studies the single-macro CK coefficient inventory under two-register restoration and a cleared-work boundary." +} diff --git a/research/complex-restored-source29/README.md b/research/complex-restored-source29/README.md new file mode 100644 index 0000000000..6a874ee212 --- /dev/null +++ b/research/complex-restored-source29/README.md @@ -0,0 +1,151 @@ +# Exact two-register frontier for the historical CK coefficients + +**Scoped negative result and finite scalar construction; no new kappa.** +For all 103 coefficient magnitudes in the pinned [PR626](https://github.com/CrocSwap/integer-mult-bounds/pull/626) CK programs, allowing +temporary source and target mutation with exact restoration cannot beat the +stated scratch-circuit comparators, except at magnitudes 2 and 3. Those two +exceptions are attained by ordinary repeated unit additions; they do not +require source mutation. No novelty is claimed for those elementary identities. +The contribution is the complete source-bound exclusion and its checked finite +application. + +This package adds only `research/complex-restored-source29/`. The selected +T37 result remains conditional kappa 0.001661960547713947. The historical CK +supplier, selected frontier, and `upstream/` are unchanged. + +## Reproduce + +Use Python 3.11+ and the standard library, offline, from the repository root: + +```sh +python3 -I -B research/complex-restored-source29/verify.py +python3 -I -B research/complex-restored-source29/independent.py +python3 -I -B research/complex-restored-source29/test_package.py +``` + +The first command ends with: + +```text +PASS_RESTORED_SOURCE_CK coefficients=103 exact_minima=77 improvements=2,3 saved_real=3124,3124 no_new_kappa +``` + +The second reports `PASS_RESTORED_SOURCE_INDEPENDENT`. Normal verification +compares the complete deterministic receipt with `EXPECTED.json` and writes +nothing. `--write NEW_PATH` explicitly produces a fresh receipt and refuses +overwrite. `SOURCES.json` pins exact input bytes and decompressed gzip payloads. + +## Cost model and exhaustive scope + +The task is to produce the scalar boundary `(T,S,W) -> (T+q*S,S,0)` for arbitrary inputs. +The two-register word may change both T and S, but must restore S exactly. +It may use `T += S`, `T -= S`, `S += T`, `S -= T`, and NEGATE, DOUBLE or HALF +on either register. Each instruction costs one primitive per real component. +No coefficient scratch, extra register, free swap or nonunit addition is +available. The incoming private W is arbitrary: its final clear costs one +additional primitive, even when the word never uses it. + +No restrictions are put on intermediate magnitudes or denominator depths. Copying +or clearing T or S cannot help within this class: either makes their map +singular, and subsequent two-register linear operations cannot recover rank. +Adding reads, frame work or physical restrictions would only make the +optimistic exclusion stronger. Three-register circuits and cross-macro +sharing remain outside the claim. + +Comparators include Sagar Thakrar's [PR696](https://github.com/CrocSwap/integer-mult-bounds/pull/696) copy/unit lowering, Gareth Davidson's +four [PR837](https://github.com/CrocSwap/integer-mult-bounds/pull/837) Horner variants, Philipp/mightyOil's [PR882](https://github.com/CrocSwap/integer-mult-bounds/pull/882) bounded scratch graph +method transferred explicitly to eligible CK coefficients, and Seb/ZK-Snarky's +[PR999](https://github.com/CrocSwap/integer-mult-bounds/pull/999) target-accumulation circuits. The [PR882](https://github.com/CrocSwap/integer-mult-bounds/pull/882) transfer is recomputed for CK; +its original 49-coefficient JP8 certificate is not treated as CK evidence. +Every comparator word receives a separate exact three-register endpoint check. +Comparison uses exact scalar costs, without asserting that all comparator +precision or production interfaces are jointly admitted. + +The complete radius-six group ball has layer sizes +`1, 10, 69, 370, 1646, 6312, 22168`: 30,576 distinct matrices. Its digest +includes every exact matrix and shortest distance. Searching two halves covers +every word through length twelve, with no coefficient pruning. The calculation +finds exact minima for 77 magnitudes; for the other 26, the two-register cost +is at least 13, or at least 14 after the private clear. + +This suffices to exclude *every strict cost improvement* in the stated class, +not merely the twelve-operation trials. Every coefficient has a checked +comparator costing at most 14. A strictly cheaper implementation must cost +at most 13, including its mandatory clear, hence contain at most twelve +two-register instructions. That entire domain was checked. Negative +coefficients have the same distances: conjugation by `diag(1,-1)` relabels +the addition signs without adding instructions. Both signs of every attained +witness are also replayed literally. + +Any word of length at most twelve can be split chronologically into two words +of length at most six. Their matrices A and B +belong to the enumerated ball, and the endpoint is `B*A`. The main checker +looks up `B = G(q)*inverse(A)`. Breadth-first deduplication loses no continuation +because the current exact matrix determines every subsequent state. This is +an elementary finite certificate argument, not a Lean proof of multiplication. + +## The two elementary exceptions + +For the small positive integers q = 2 and 3, perform q unit additions into T +and clear W. Negative +q uses subtractions. Complete costs are 3 and 4, compared with the best stated +comparator costs 4 and 5. Exact shortest distances are respectively 2 and 3 +before the clear. The original target, source and frame remain the boundary; +every additional source read is charged. Source and work magnitudes do not +grow, and target partial sums lie between its initial and final source +coefficients. Thus the shortcut preserves the original per-register envelope +and cannot introduce fractional precision requirements. + +Applying only these two substitutions to the [PR696](https://github.com/CrocSwap/integer-mult-bounds/pull/696) CK programs gives: + +| Complete scalar projection | [PR696](https://github.com/CrocSwap/integer-mult-bounds/pull/696) | Replacement | Saved real primitives | +|---|---:|---:|---:| +| Forward | 169,618 | 166,494 | 3,124 | +| Inverse transpose | 169,634 | 166,510 | 3,124 | + +Each orientation replaces 1,562 macros. Literal replay covers all 725 input +columns: 716 native, eight private centers, and arbitrary coefficient-work +dirt. It checks the expected CK shear, all 492 helper restorations, private +clearing and the unchanged paid profile. Exact prefix row-L1 maxima remain +5,120 forward and 4,847 backward; denominator depths remain 3 and 8. The +cancellation-free envelope is also unchanged. These are scalar counts and +prefix calculations, not measured runtime or a new recursive saving. + +A separate checker imports no code from the project. It reconstructs the group ball +with Fraction matrices and column operations, then uses the different quotient +`A = inverse(B)*G(q)` to check all 103 distances. It agrees on every matrix +distance, all 77 minima and both signs of each witness. Both implementations +are AI-written; this is algorithmic crosschecking, not independent human review. +Adverse controls cover lost source restoration, dirty work, target dirt, wrong +signs, missing reads, false distances, unpaid clearing and incomplete coverage. +Package tests cover isolated optimized relocation, equivalent recompression, +source and receipt corruption, and output preservation. + +## Provenance and limits + +Exact base: `2921874911956718fcaaaf9396fe8267b3cfa9f0`. OS assignment seed 29 +selects the complex track, CK provider and gate tie order. `CLAIM.json` records +the rejected alternatives, fixed stopping rule and local coordination fallback; +no pinned sprint issue existed. The complete fixed domain was finished without +a timeout or larger search restart. + +Credit Philipp/mightyOil's [PR883](https://github.com/CrocSwap/integer-mult-bounds/pull/883) for the two-register alphabet and precondition +minimum precedent; [PR882](https://github.com/CrocSwap/integer-mult-bounds/pull/882) for bounded scratch synthesis; Sagar Thakrar's [PR696](https://github.com/CrocSwap/integer-mult-bounds/pull/696) +and [PR723](https://github.com/CrocSwap/integer-mult-bounds/pull/723), Chris Pagolu's [PR734](https://github.com/CrocSwap/integer-mult-bounds/pull/734), Gareth Davidson's [PR837](https://github.com/CrocSwap/integer-mult-bounds/pull/837)/866, and Seb's [PR999](https://github.com/CrocSwap/integer-mult-bounds/pull/999) +for the coefficient comparison lineage. The verbatim [PR999](https://github.com/CrocSwap/integer-mult-bounds/pull/999) module retains its +author notice and is pinned to `fd38a824adb3a5c60c101a86c950a6d590454adf`. +The CK source is Chafik Boukhalfa's [PR626](https://github.com/CrocSwap/integer-mult-bounds/pull/626) at +`660de893d27bb7abd1d5b01b1640207528a5c851`, on Jeremy Kothe's [PR622](https://github.com/CrocSwap/integer-mult-bounds/pull/622) at +`f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`, with icekylinx's primitive/emitter +lineage and the retained predecessor notices. No priority is claimed for the +alphabet, meet-in-the-middle search, or repeated unit additions. + +Full native phase/frame execution, cold provider rebuilding, global invoice +admission, selected T37 transport, Linux CI and Lean are not supplied. The +unaltered event inventory and recursive profile are counted, not physically +executed by these scalar projections. All-size/compiler, mutable-source +realization, whole-call hosting, precision/tape and analytic assumptions remain +inherited. Other registers, alphabets, coefficient inventories and shared +clearing boundaries are outside the exclusion. + +Prepared for Hanson Sun (@bbMisk) with substantial OpenAI Codex assistance in +research, implementation, verification and writing. Apache-2.0. diff --git a/research/complex-restored-source29/SOURCES.json b/research/complex-restored-source29/SOURCES.json new file mode 100644 index 0000000000..0ba09fd3e2 --- /dev/null +++ b/research/complex-restored-source29/SOURCES.json @@ -0,0 +1,73 @@ +{ + "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "source_heads": { + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "696": "5a3f983715027c4fd83f50bc9001d4b18463bed1", + "837": "0a2977195efc8fb2a918fbfb694ec8d294387f08", + "882": "e698981e0ffa680b6c5896dace1609025b97ad70", + "883": "b31a870a3842b37f6ab97767c506ce91783632a2", + "999": "fd38a824adb3a5c60c101a86c950a6d590454adf" + }, + "vendored_pr999": { + "upstream_path": "research/complex-coefficient-accumulation/lower.py", + "local_path": "research/complex-restored-source29/vendor/pr999_lower.py", + "representation": "verbatim at source head", + "contributor": "Seb (@ZK-Snarky), substantial OpenAI Codex assistance", + "license": "Apache-2.0" + }, + "files": { + "research/complex-dyadic-lowering/lower.py": { + "representation": "exact-bytes", + "sha256": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + }, + "research/dyadic-horner-direction/lower.py": { + "representation": "exact-bytes", + "sha256": "6a7ae3f2aff61077ce4b3f179f7ccc2024f5176b5894547250eb14105b14f5e2" + }, + "research/dyadic-horner-direction/vendor/pr696_lower.py": { + "representation": "exact-bytes", + "sha256": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + }, + "research/jp8-grid-bounded-synthesis/synth.py": { + "representation": "exact-bytes", + "sha256": "5f28a055b002c6d3ec42e73321efe5a6c3f4574cbf356debf8cee779702e2f95" + }, + "research/jp8-grid-bounded-synthesis/vendor/pr837/lower.py": { + "representation": "exact-bytes", + "sha256": "6a7ae3f2aff61077ce4b3f179f7ccc2024f5176b5894547250eb14105b14f5e2" + }, + "research/jp8-grid-bounded-synthesis/vendor/pr837/vendor/pr696_lower.py": { + "representation": "exact-bytes", + "sha256": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + }, + "research/complex-restored-source29/vendor/pr999_lower.py": { + "representation": "exact-bytes", + "sha256": "bc7a235ea303efe2ffc69634d2bb86bfd3d1a017527e7cf66d8a72965a8317fc" + }, + "research/complex-k492-owner-repair/data/SPEC.json": { + "representation": "exact-bytes", + "sha256": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323" + }, + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": { + "representation": "gzip-payload", + "sha256": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900" + }, + "certificates/checkpoints/k492626.json": { + "representation": "exact-bytes", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "research/x4-precondition-seed22/PAIR-PROOF.md": { + "representation": "exact-bytes", + "sha256": "0a60e63ce7100f80b110f248686b50b6e1864e21882d6a55aa3ef47e18d3ad71" + }, + "research/complex-k492-owner-repair/code/hpe_emit_local.py": { + "representation": "exact-bytes", + "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805" + }, + "research/complex-k492-owner-repair/code/invoice_allcold.py": { + "representation": "exact-bytes", + "sha256": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec" + } + } +} diff --git a/research/complex-restored-source29/VALIDATION.json b/research/complex-restored-source29/VALIDATION.json new file mode 100644 index 0000000000..47099cb1e3 --- /dev/null +++ b/research/complex-restored-source29/VALIDATION.json @@ -0,0 +1,85 @@ +{ + "status": "local scoped verification complete", + "environment": { + "python": "3.14.6", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "machine": "arm64" + }, + "commands": [ + { + "command": "python3 -I -B research/complex-restored-source29/verify.py", + "result": "PASS_RESTORED_SOURCE_CK coefficients=103 exact_minima=77 improvements=2,3 saved_real=3124,3124 no_new_kappa" + }, + { + "command": "python3 -I -B research/complex-restored-source29/independent.py", + "result": { + "coefficients": 103, + "controls": [ + "optimistic_distance", + "boolean_distance", + "unpaid_clear", + "unproved_long_target", + "false_improvement", + "wrong_witness_sign", + "missing_depth_six_frontier" + ], + "distance_sha256": "f5c77025594055b6e8736ed8df2b9a991e936680137004bfc187d787793c73a1", + "exact_minima": 77, + "states": 30576, + "status": "PASS_RESTORED_SOURCE_INDEPENDENT" + } + }, + { + "command": "python3 -I -B research/complex-restored-source29/test_package.py", + "result": "5 tests passed; includes isolated optimized minimal relocation, equivalent recompression, source/receipt corruption and output preservation" + }, + { + "command": "make selected-record-check", + "result": "PASS 1661960547713947/1000000000000000000" + }, + { + "command": "python3 -m unittest discover -s tests -p '*selected*'", + "result": "25 tests passed" + }, + { + "command": "python3 -I -O -B research/complex-restored-source29/independent.py", + "result": { + "coefficients": 103, + "controls": [ + "optimistic_distance", + "boolean_distance", + "unpaid_clear", + "unproved_long_target", + "false_improvement", + "wrong_witness_sign", + "missing_depth_six_frontier" + ], + "distance_sha256": "f5c77025594055b6e8736ed8df2b9a991e936680137004bfc187d787793c73a1", + "exact_minima": 77, + "states": 30576, + "status": "PASS_RESTORED_SOURCE_INDEPENDENT" + } + } + ], + "source_recheck": { + "base": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "origin_main": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "base_git_blobs_and_upstream_and_worktree_identical": 12 + }, + "excluded": [ + "full make verify", + "cold provider regeneration", + "native phase/frame execution", + "global owner/invoice admission", + "selected T37 transport", + "hosted CI", + "Lean" + ], + "review_scope": "Two AI-written algorithms; no independent human review. Exact finite scalar and group-word checks only.", + "staged_scope": { + "files": 11, + "paths": "research/complex-restored-source29/ only", + "reviewed_worktree_equals_staged_content": true, + "whitespace_check": "pass" + } +} diff --git a/research/complex-restored-source29/independent.py b/research/complex-restored-source29/independent.py new file mode 100644 index 0000000000..46e0ea861f --- /dev/null +++ b/research/complex-restored-source29/independent.py @@ -0,0 +1,198 @@ +"""Independent Fraction/column-action distance checker; no project imports. + +Hanson Sun (@bbMisk), substantial OpenAI Codex assistance. Apache-2.0. +Checks the exact two-register census, not physical/native supplier admission. +""" + +import argparse +from collections import Counter +from fractions import Fraction as F +import gzip +from hashlib import sha256 +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +I = (F(1), F(0), F(0), F(1)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def right_action(matrix, instruction): + """Multiply on the RIGHT, by elementary column operations.""" + kind, column, value = instruction + out = list(matrix) + if kind == "mix": + for row in (0, 1): + out[2 * row + column] += value * matrix[2 * row + 1 - column] + else: + for row in (0, 1): + out[2 * row + column] *= value + return tuple(out) + + +ALPHABET = tuple( + [("mix", c, F(sign)) for c in (0, 1) for sign in (-1, 1)] + + [("scale", c, factor) for c in (0, 1) for factor in (F(-1), F(1, 2), F(2))] +) + + +def rational_ball(radius=6): + distances = {I: 0} + frontier = [I] + layers = [1] + for depth in range(radius): + next_layer = [] + for matrix in frontier: + for gate in ALPHABET: + other = right_action(matrix, gate) + if other not in distances: + distances[other] = depth + 1 + next_layer.append(other) + frontier = next_layer + layers.append(len(frontier)) + return distances, layers + + +def normalized_row(matrix, distance): + denominator = max(value.denominator for value in matrix) + require(denominator & (denominator - 1) == 0, "non-dyadic matrix") + coefficients = [value.numerator * (denominator // value.denominator) for value in matrix] + return (*coefficients, denominator.bit_length() - 1, distance) + + +def inverse(matrix): + a, b, c, d = matrix + determinant = a * d - b * c + require(determinant != 0, "singular matrix") + return d / determinant, -b / determinant, -c / determinant, a / determinant + + +def shortest(q, distances, inverses): + best = None + for (a, b, c, d), suffix_distance in inverses: + # A = B^(-1) G(q), whereas the constructor solves B = G(q) A^(-1). + prefix = (a, a * q + b, c, c * q + d) + first = distances.get(prefix) + if first is not None and (best is None or first + suffix_distance < best): + best = first + suffix_distance + return best + + +def word_matrix(names, sign=1): + rows = [[F(1), F(0)], [F(0), F(1)]] + for name in names: + if name in ("t+s", "t-s", "s+t", "s-t"): + dest = 0 if name[0] == "t" else 1 + value = sign * (1 if name[1] == "+" else -1) + rows[dest] = [rows[dest][i] + value * rows[1 - dest][i] for i in (0, 1)] + else: + dest = 0 if "t" in name else 1 + factor = F(2) if name.startswith("2") else F(-1) if name.startswith("-") else F(1, 2) + require(name in ("2t", "t/2", "2s", "s/2", "-t", "-s"), "unknown witness gate") + rows[dest] = [factor * x for x in rows[dest]] + return tuple(rows[0] + rows[1]) + + +def validate_entry(entry, minimum): + require(type(entry["best_comparator_cost"]) is int, "noninteger comparator cost") + require(entry["two_register_minimum"] is None or type(entry["two_register_minimum"]) is int, + "noninteger minimum") + require(entry["two_register_minimum"] == minimum, "wrong shortest distance") + lower = 13 if minimum is None else minimum + require(type(entry["two_register_lower_bound"]) is int and entry["two_register_lower_bound"] == lower, + "wrong lower bound") + require(entry["complete_cost_lower_bound"] == lower + 1, "unpaid private clear") + require(entry["best_comparator_cost"] <= 14, "cutoff does not exclude all improvements") + improvement = minimum is not None and minimum + 1 < entry["best_comparator_cost"] + require(type(entry["strict_improvement"]) is bool and entry["strict_improvement"] == improvement, + "incorrect strict comparison") + if minimum is not None: + q = F(entry["coefficient"]) + require(len(entry["word"]) == minimum, "witness cost mismatch") + require(word_matrix(entry["word"]) == (1, q, 0, 1), "positive witness endpoint") + require(word_matrix(entry["word"], -1) == (1, -q, 0, 1), "negative witness endpoint") + else: + require(entry["word"] is None, "unreached target has a witness") + + +def independent_controls(entries, minima, distances): + import copy + examples = {entry["coefficient"]: entry for entry in entries} + mutants = [] + for label, q, field, value in ( + ("optimistic_distance", "3", "two_register_minimum", 2), + ("boolean_distance", "1", "two_register_minimum", True), + ("unpaid_clear", "3", "complete_cost_lower_bound", 3), + ("unproved_long_target", "1/64", "two_register_lower_bound", 14), + ("false_improvement", "5/2", "strict_improvement", True), + ): + mutant = copy.deepcopy(examples[q]) + mutant[field] = value + mutants.append((label, q, mutant)) + mutant = copy.deepcopy(examples["3"]) + mutant["word"][0] = "t-s" + mutants.append(("wrong_witness_sign", "3", mutant)) + rejected = [] + for label, q, mutant in mutants: + try: + validate_entry(mutant, minima[q]) + except ValueError: + rejected.append(label) + else: + raise ValueError("accepted mutant: " + label) + # A reduced ball actually loses a reachable frontier state. + radius_five = {m: d for m, d in distances.items() if d <= 5} + require(len(radius_five) == 8408 and len(radius_five) != len(distances), "radius deletion undetected") + rejected.append("missing_depth_six_frontier") + return rejected + + +def run(certificate): + receipt = json.loads(certificate.read_text(encoding="utf-8")) + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + path = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz" + raw = gzip.decompress((ROOT / path).read_bytes()) + require(sha256(raw).hexdigest() == pins["files"][path]["sha256"], "CK source pin") + programs = json.loads(raw) + domains = {} + for orientation in ("forward", "backward"): + domains[orientation] = Counter(abs(F(e[1][3], e[1][4])) for e in programs[orientation] + if e[0] == "scalar" and e[1][0] == "add") + entries = receipt["coefficients"] + require([F(e["coefficient"]) for e in entries] == sorted(domains["forward"]), "incomplete coefficient domain") + require(set(domains["forward"]) == set(domains["backward"]), "orientation domain differs") + distances, layers = rational_ball() + require(layers == receipt["layer_sizes"] == [1, 10, 69, 370, 1646, 6312, 22168], "BFS layer census") + rows = sorted(normalized_row(m, d) for m, d in distances.items()) + digest = sha256() + for row in rows: + digest.update((",".join(map(str, row)) + "\n").encode("ascii")) + require(digest.hexdigest() == receipt["distance_sha256"], "full group-ball distance digest") + require(len(distances) == receipt["ball_states"] == 30576, "group-ball coverage") + inverses = [(inverse(m), d) for m, d in distances.items()] + minima = {} + for entry in entries: + q = F(entry["coefficient"]) + for orientation, domain in domains.items(): + require(entry["occurrences"][orientation] == domain[q], "occurrence count") + minimum = shortest(q, distances, inverses) + validate_entry(entry, minimum) + minima[str(q)] = minimum + require(sum(d is not None for d in minima.values()) == 77, "minimum census") + require([e["coefficient"] for e in entries if e["strict_improvement"]] == ["2", "3"], "improvement census") + controls = independent_controls(entries, minima, distances) + return {"status": "PASS_RESTORED_SOURCE_INDEPENDENT", "states": len(distances), + "coefficients": len(entries), "exact_minima": 77, + "distance_sha256": digest.hexdigest(), "controls": controls} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser() + parser.add_argument("--certificate", type=Path, default=HERE / "EXPECTED.json") + args = parser.parse_args() + print(json.dumps(run(args.certificate), sort_keys=True)) diff --git a/research/complex-restored-source29/search.py b/research/complex-restored-source29/search.py new file mode 100644 index 0000000000..7f6d02b330 --- /dev/null +++ b/research/complex-restored-source29/search.py @@ -0,0 +1,142 @@ +"""Exact two-register word metric; Hanson Sun, with OpenAI Codex assistance. + +Apache-2.0. The ten-operation alphabet follows Philipp/mightyOil's PR883. +This implementation uses normalized integer matrices, with no magnitude cap. +""" + +from fractions import Fraction +import hashlib + + +SEED = 29 +RADIUS = 6 +IDENTITY = (1, 0, 0, 1, 0) +GATES = ("t+s", "t-s", "s+t", "s-t", "2t", "t/2", "2s", "s/2", "-t", "-s") +INVERSE = (1, 0, 3, 2, 5, 4, 7, 6, 8, 9) +ORDER = tuple((i + SEED) % len(GATES) for i in range(len(GATES))) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def normalize(a, b, c, d, exponent): + """Represent [[a,b],[c,d]] / 2**exponent uniquely.""" + need(type(exponent) is int and exponent >= 0, "invalid denominator exponent") + while exponent and not ((a | b | c | d) & 1): + a, b, c, d, exponent = a // 2, b // 2, c // 2, d // 2, exponent - 1 + return a, b, c, d, exponent + + +def step(matrix, gate): + a, b, c, d, k = matrix + if gate == 0: + a, b = a + c, b + d + elif gate == 1: + a, b = a - c, b - d + elif gate == 2: + c, d = c + a, d + b + elif gate == 3: + c, d = c - a, d - b + elif gate == 4: + a, b = 2 * a, 2 * b + elif gate == 5: + c, d, k = 2 * c, 2 * d, k + 1 + elif gate == 6: + c, d = 2 * c, 2 * d + elif gate == 7: + a, b, k = 2 * a, 2 * b, k + 1 + elif gate == 8: + a, b = -a, -b + elif gate == 9: + c, d = -c, -d + else: + raise ValueError("unknown gate") + return normalize(a, b, c, d, k) + + +def multiply(x, y): + a, b, c, d, k = x + e, f, g, h, ell = y + return normalize(a * e + b * g, a * f + b * h, + c * e + d * g, c * f + d * h, k + ell) + + +def inverse(matrix): + a, b, c, d, k = matrix + determinant = a * d - b * c + magnitude = abs(determinant) + need(magnitude > 0 and magnitude & (magnitude - 1) == 0, + "determinant is not a signed power of two") + sign = 1 if determinant > 0 else -1 + exponent = magnitude.bit_length() - 1 - k + values = [sign * d, -sign * b, -sign * c, sign * a] + if exponent < 0: + values = [v * 2 ** (-exponent) for v in values] + exponent = 0 + return normalize(*values, exponent) + + +def ball(radius=RADIUS, order=ORDER): + """Complete BFS ball: deduplication is exact matrix equality only.""" + need(type(radius) is int and 0 <= radius <= RADIUS, "radius outside fixed experiment") + need(sorted(order) == list(range(10)), "incomplete gate alphabet") + words = {IDENTITY: ()} + frontier = [IDENTITY] + layers = [1] + for _ in range(radius): + following = [] + for matrix in frontier: + for gate in order: + nxt = step(matrix, gate) + if nxt not in words: + words[nxt] = words[matrix] + (gate,) + following.append(nxt) + frontier = following + layers.append(len(frontier)) + return words, layers + + +def distance_digest(words): + digest = hashlib.sha256() + for matrix in sorted(words): + row = (*matrix, len(words[matrix])) + digest.update((",".join(map(str, row)) + "\n").encode("ascii")) + return digest.hexdigest() + + +def shear(q): + q = Fraction(q) + denominator = q.denominator + need(denominator & (denominator - 1) == 0, "nondyadic shear") + return normalize(denominator, q.numerator, 0, denominator, + denominator.bit_length() - 1) + + +def execute(word): + result = IDENTITY + for gate in word: + result = step(result, gate) + return result + + +def metric(coefficients, words): + inverses = [(inverse(matrix), word) for matrix, word in words.items()] + result = [] + for q in coefficients: + goal = shear(q) + best = None + for left_inverse, prefix in inverses: + suffix = words.get(multiply(goal, left_inverse)) + if suffix is not None and (best is None or len(prefix) + len(suffix) < len(best)): + best = prefix + suffix + if best is not None: + need(execute(best) == goal, "constructed word misses the complete shear") + result.append({ + "coefficient": str(q), + "two_register_minimum": len(best) if best is not None else None, + "two_register_lower_bound": len(best) if best is not None else 2 * RADIUS + 1, + "word": [GATES[g] for g in best] if best is not None else None, + }) + return result diff --git a/research/complex-restored-source29/test_package.py b/research/complex-restored-source29/test_package.py new file mode 100644 index 0000000000..9cd0333e61 --- /dev/null +++ b/research/complex-restored-source29/test_package.py @@ -0,0 +1,116 @@ +"""Mathematical boundary and source/receipt failure controls. Apache-2.0.""" + +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import search +import verify +import independent + + +class MathematicalControls(unittest.TestCase): + def test_full_ball_inverse_and_no_depth_loss(self): + words, layers = search.ball() + self.assertEqual(layers, [1, 10, 69, 370, 1646, 6312, 22168]) + for matrix, word in words.items(): + with self.subTest(matrix=matrix): + self.assertEqual(search.execute(word), matrix) + self.assertEqual(search.multiply(matrix, search.inverse(matrix)), search.IDENTITY) + self.assertEqual(independent.rational_ball(3)[1], layers[:4]) + + def test_shortcut_arbitrary_dirt_and_prefix_contract(self): + _, reference, _, _, _, _, _ = verify.sources() + t, s, w = ("T", 0), ("S", 0), verify.WORK + for q in map(Q, (-3, -2, 2, 3)): + word = verify.shortcut(["add", list(t), list(s), q.numerator, 1], reference) + verify.local_check(q, word) + rows = {t: {0: Q(1)}, s: {1: Q(1)}, w: {2: Q(1)}} + for primitive in word: + verify.step(rows, primitive) + self.assertEqual(rows[s], {1: 1}) + self.assertEqual(rows[t][0], 1) + self.assertLessEqual(abs(rows[t].get(1, 0)), abs(q)) + self.assertIn(rows[w], ({2: 1}, {})) + self.assertTrue(all(v.denominator == 1 for row in rows.values() for v in row.values())) + + def test_declared_adverse_cases(self): + _, reference, _, _, _, _, _ = verify.sources() + self.assertEqual(len(verify.controls(reference)), 10) + entries = verify.read(HERE / "EXPECTED.json")["coefficients"] + minima = {e["coefficient"]: e["two_register_minimum"] for e in entries} + distances = {m: len(w) for m, w in search.ball()[0].items()} + self.assertEqual(len(independent.independent_controls(entries, minima, distances)), 7) + + def test_negative_sign_is_gate_relabeling(self): + for q in (Q(1, 2), Q(3, 4), Q(5, 2), Q(29, 8), Q(17)): + row = search.metric([q], search.ball()[0])[0] + self.assertIsNotNone(row["word"]) + verify.local_check(-q, verify.two_register_word(row["word"], negative=True)) + + +class PackageControls(unittest.TestCase): + def test_offline_relocation_recompression_corruption_and_preservation(self): + pins = verify.read(HERE / "SOURCES.json") + with tempfile.TemporaryDirectory(prefix="restored source 29 ") as temporary: + root = Path(temporary) / "minimal checkout with spaces" + package = root / "research/complex-restored-source29" + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__", "*.pyc")) + for name in pins["files"]: + destination = root / name + if not destination.exists(): + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / name, destination) + source = root / verify.PROVIDER / "LOCAL-PROGRAMS.json.gz" + source.write_bytes(gzip.compress(gzip.decompress(source.read_bytes()), compresslevel=1, mtime=123)) + command = [sys.executable, "-I", "-O", "-B", str(package / "verify.py")] + + def run(*extra): + return subprocess.run(command + list(extra), cwd=temporary, text=True, capture_output=True, timeout=90) + + def snapshot(): + return {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") if p.is_file()} + + before = snapshot() + completed = run() + self.assertEqual(completed.returncode, 0, completed.stdout + completed.stderr) + self.assertIn("PASS_RESTORED_SOURCE_CK", completed.stdout) + self.assertEqual(before, snapshot(), "default replay wrote into the source tree") + + # Default and --write must both preserve an existing certificate. + certificate = package / "EXPECTED.json" + original_certificate = certificate.read_bytes() + preserved = run("--write", str(certificate)) + self.assertNotEqual(preserved.returncode, 0) + self.assertIn("refusing to overwrite", preserved.stderr) + self.assertEqual(certificate.read_bytes(), original_certificate) + + # Float/int equality cannot conceal a changed deterministic receipt. + receipt = json.loads(original_certificate) + receipt["coefficient_count"] = 103.0 + certificate.write_text(json.dumps(receipt), encoding="utf-8") + altered = run() + self.assertNotEqual(altered.returncode, 0) + self.assertIn("complete certificate mismatch", altered.stderr) + self.assertEqual(json.loads(certificate.read_text())["coefficient_count"], 103.0) + certificate.write_bytes(original_certificate) + + # Corrupt decompressed input, not a gzip header. + source.write_bytes(gzip.compress(gzip.decompress(source.read_bytes()) + b" ")) + corrupted = run() + self.assertNotEqual(corrupted.returncode, 0) + self.assertIn("source pin:", corrupted.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/complex-restored-source29/vendor/pr999_lower.py b/research/complex-restored-source29/vendor/pr999_lower.py new file mode 100644 index 0000000000..e3cbf7be8f --- /dev/null +++ b/research/complex-restored-source29/vendor/pr999_lower.py @@ -0,0 +1,309 @@ +"""Exact bounded-accumulator lowering of the selected complex scalar words. + +Prepared for Seb (@ZK-Snarky) with substantial OpenAI Codex assistance. +Apache-2.0. The primitive vocabulary is from icekylinx's PR425/433/531 +lineage. Copy-Horner/unit lowering and the sparse replay structure follow +Sagar Thakrar's PR696 (5a3f983715027c4fd83f50bc9001d4b18463bed1). +The two target-accumulation circuits and their prefix check are new here. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROVIDERS = ROOT / "research/community-k492-audit/pr626/replay/mixed-global/base/providers" +WORK = ("W", 0) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def power_two(n): + return n > 0 and n & (n - 1) == 0 + + +def shifts(register, exponent): + return [("double" if exponent > 0 else "halve", register)] * abs(exponent) + + +@lru_cache(maxsize=None) +def addition(q): + """Choose the shortest of three explicit circuits, keeping Horner on ties. + + Abstract registers T/S/W are target/source/private coefficient work. + Every candidate has exact endpoint T += q*S, S unchanged, W = 0. + """ + a, b = abs(q.numerator), q.denominator + require(a and power_two(b), "addition requires a nonzero dyadic") + accumulate = "add" if q > 0 else "subtract" + if a == b: + return "unit", ((accumulate, "T", "S"), ("clear", "W")) + k, d = a.bit_length() - 1, b.bit_length() - 1 + horner = [("copy", "W", "S")] + for bit in bin(a)[3:]: + horner.append(("double", "W")) + if bit == "1": + horner.append(("add", "W", "S")) + horner += shifts("W", -d) + [(accumulate, "T", "W"), ("clear", "W")] + + # Descending positive binary summands: every target prefix lies in [0,q] + # (or [q,0]) and the work never exceeds the leading power of two. + binary = [("copy", "W", "S")] + shifts("W", k - d) + for i in range(k, -1, -1): + if a >> i & 1: + binary.append((accumulate, "T", "W")) + if i: + binary.append(("halve", "W")) + binary.append(("clear", "W")) + + # Non-adjacent signed digits. Split a too-large leading work value into + # two visits to its half; this matters for integral coefficients only. + digits, n = [], a + while n: + digit = 2 - n % 4 if n & 1 else 0 + digits.append(digit) + n = (n - digit) // 2 + if 1 << (len(digits) - 1) > a * b: + top = digits.pop() + digits[-1] += 2 * top + signed = [("copy", "W", "S")] + shifts("W", -d) + for i, digit in enumerate(digits): + operation = "add" if (digit > 0) == (q > 0) else "subtract" + signed += [(operation, "T", "W")] * abs(digit) + if i + 1 < len(digits): + signed.append(("double", "W")) + signed.append(("clear", "W")) + candidates = (("horner", horner), ("binary_descending", binary), + ("signed_ascending", signed)) + method, word = min(candidates, key=lambda item: len(item[1])) + return method, tuple(word) + + +def lower(op, work=WORK): + """Lower one scalar macro; caller executes all primitives at its frame.""" + tag, target = op[0], tuple(op[1]) + require(target != work, "work aliases target") + if tag == "clear": + return "clear", [("clear", target)] + if tag == "scale": + q = Q(op[2], op[3]) + require(power_two(abs(q.numerator)) and power_two(q.denominator), + "scale requires a signed power of two") + word = shifts(target, abs(q.numerator).bit_length() - q.denominator.bit_length()) + return "scale", word + ([("negate", target)] if q < 0 else []) + require(tag in ("add", "copy"), "unknown macro") + source = tuple(op[2]) + require(source not in (target, work), "source aliases target or work") + if tag == "copy": + return "copy", [("copy", target, source)] + method, word = addition(Q(op[3], op[4])) + registers = {"T": target, "S": source, "W": work} + return method, [(p[0], *(registers[r] for r in p[1:])) for p in word] + + +def step(rows, op): + """Exact sparse row interpreter; executes primitives, not scalar macros.""" + tag, target = op[:2] + if tag == "clear": + rows[target] = {} + elif tag == "copy": + rows[target] = rows[op[2]].copy() + elif tag in ("double", "halve", "negate"): + q = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[target] = {j: q * x for j, x in rows[target].items()} + elif tag in ("add", "subtract"): + for j, x in list(rows[op[2]].items()): + value = rows[target].get(j, Q(0)) + (x if tag == "add" else -x) + if value: + rows[target][j] = value + else: + rows[target].pop(j, None) + else: + raise ValueError("unknown primitive") + + +def check_addition(q, word): + """Independently check arbitrary T,S,W and the reference prefix envelope.""" + rows = {r: {r: Q(1)} for r in ("T", "S", "W")} + for primitive in word: + step(rows, primitive) + require(rows["S"] == {"S": Q(1)}, "source changed") + t, w = rows["T"], rows["W"] + require(t.get("T") == 1 and set(t) <= {"T", "S"} + and abs(t.get("S", 0)) <= abs(q), "target prefix envelope") + require(w == {"W": Q(1)} or + (set(w) <= {"S"} and abs(w.get("S", 0)) <= abs(q.numerator)), + "work prefix envelope") + require(rows == {"T": {"T": Q(1), "S": q}, "S": {"S": Q(1)}, "W": {}}, + "endpoint or dirty-work cleanup") + + +def baseline_count(op): + if op[0] in ("clear", "copy"): + return 1 + q = Q(op[3], op[4]) if op[0] == "add" else Q(op[2], op[3]) + a, b = abs(q.numerator), q.denominator + if op[0] == "scale": + return abs(a.bit_length() - b.bit_length()) + int(q < 0) + return 3 + a.bit_length() - 1 + a.bit_count() + b.bit_length() - 1 + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == ".gz" else raw) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def controls(): + q = Q(63, 8) + _, word = addition(q) + word = list(word) + mutations = { + "missing_cleanup": word[:-1], + "dirty_source_copy_omitted": word[1:], + "wrong_accumulation_sign": [ + ("add", *p[1:]) if p[0] == "subtract" else p for p in word], + "endpoint_neutral_source_growth": [("double", "S"), ("halve", "S")] + word, + "endpoint_neutral_target_growth": [("add", "T", "S")] * 8 + + [("subtract", "T", "S")] * 8 + word, + "endpoint_neutral_work_growth": [("copy", "W", "S")] + + [("double", "W")] * 6 + [("halve", "W")] * 6 + word, + } + rejected = [] + for name, mutant in mutations.items(): + try: + check_addition(q, mutant) + except ValueError: + rejected.append(name) + else: + raise ValueError("accepted mutation: " + name) + for name, op in { + "nondyadic": ["add", ["T", 0], ["S", 0], 1, 3], + "zero_coefficient": ["add", ["T", 0], ["S", 0], 0, 1], + "source_alias": ["add", ["T", 0], ["T", 0], 1, 1], + "work_alias": ["add", ["T", 0], list(WORK), 1, 1], + }.items(): + try: + lower(op) + except ValueError: + rejected.append(name) + else: + raise ValueError("accepted invalid macro: " + name) + return rejected + + +def replay(events, checks, inherited, orientation): + n, v = 716, 112 + rows = {("L", r): {r: Q(1)} for r in range(n)} + rows[WORK] = {n: Q(1)} + paid, methods, primitives, coefficients = Counter(), Counter(), Counter(), set() + original = predecessor = macro_count = 0 + circuit_hash = hashlib.sha256() + for event in events: + if event[0] == "climb": + paid[event[5]] += 1 + elif event[0] == "center": + paid[event[4]] += 1 + elif event[0] == "scalar": + op, frame = event[1:] + method, word = lower(op) + methods[method] += 1 + macro_count += 1 + old = baseline_count(op) + original += 2 * old + predecessor += 2 * old + if op[0] == "add": + q = Q(op[3], op[4]) + coefficients.add(q) + predecessor -= 2 * (1 + (abs(q) == 1)) + rows.setdefault(tuple(op[1]), {}) + for primitive in word: + step(rows, primitive) + primitives[primitive[0]] += 2 + circuit_hash.update(json.dumps([frame, primitive], separators=(",", ":")).encode() + b"\n") + if op[0] == "add": + require(not rows[WORK], "private coefficient work survived") + else: + require(event[0] in ("phase", "adapter", "residual_adapter"), "unknown event") + for r in range(n): + expected = {r: Q(1)} + if orientation == "forward" and v <= r < 2 * v: + expected[r - v] = Q(1) + if orientation == "backward" and r < v: + expected[r + v] = Q(-1) + require(rows[("L", r)] == expected, "full arbitrary-input endpoint at " + str(r)) + require(all(not row for r, row in rows.items() if r[0] != "L"), "private work not zero") + require(original == checks["real_component_primitive_bound"], "original primitive count") + require(macro_count == checks["scalar_macros"], "scalar count") + require(dict(paid) == {int(k): v for k, v in checks["paid_profile"].items()}, "paid profile") + total = sum(primitives.values()) + return { + "original_real_primitives": original, + "pr696_real_primitives": predecessor, + "new_real_primitives": total, + "saved_vs_pr696": predecessor - total, + "saved_vs_original": original - total, + "all_input_columns": n, + "extra_dirty_work_column": 1, + "scalar_macros": macro_count, + "methods": dict(sorted(methods.items())), + "primitives": dict(sorted(primitives.items())), + "primitive_word_sha256": circuit_hash.hexdigest(), + "paid_profile": {str(k): v for k, v in sorted(paid.items())}, + "inherited_prefix_l1_upper": inherited["prefix_l1_upper"], + "charged_payload_bits": inherited["charged_payload_bits"], + }, coefficients + + +def certificate(): + pins = read(HERE / "SOURCES.json") + for name, expected in pins["files"].items(): + path = ROOT / name + data = path.read_bytes() + if path.suffix == ".gz": + data = gzip.decompress(data) + require(digest(data) == expected, "source pin: " + name) + results, coefficients = {}, set() + for provider in ("ck", "jp8"): + directory = PROVIDERS / provider + programs = read(directory / "LOCAL-PROGRAMS.json.gz") + checks = read(directory / "LOCAL-CHECKS.json") + inherited = read(directory / "INDEPENDENT-LOCAL-REPLAY.json") + for orientation in ("forward", "backward"): + events = programs[orientation] + require(digest(json.dumps(events, sort_keys=True, separators=(",", ":")).encode()) + == checks[orientation]["sha256"], "program semantic hash") + key = provider + "/" + orientation + results[key], used = replay(events, checks[orientation], + inherited["local"][orientation], orientation) + coefficients.update(used) + for q in sorted(coefficients): + _, word = addition(q) + check_addition(q, word) + return {"status": "PASS_COMPLEX_COEFFICIENT_ACCUMULATION", "programs": results, + "distinct_coefficients": len(coefficients), "controls": controls()} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-certificate", type=Path, help="write to a NEW file instead of checking EXPECTED.json") + args = parser.parse_args() + result = certificate() + if args.write_certificate: + with args.write_certificate.open("x") as out: + out.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(result == read(HERE / "EXPECTED.json"), "expected certificate differs") + savings = ",".join(str(p["saved_vs_pr696"]) for p in result["programs"].values()) + print(f"PASS_COMPLEX_COEFFICIENT_ACCUMULATION programs=4 columns=716 extra_savings={savings} controls={len(result['controls'])}") diff --git a/research/complex-restored-source29/verify.py b/research/complex-restored-source29/verify.py new file mode 100644 index 0000000000..311ff87844 --- /dev/null +++ b/research/complex-restored-source29/verify.py @@ -0,0 +1,360 @@ +"""Source-bound CK coefficient census and complete scalar-projection replay. + +Hanson Sun (@bbMisk), substantial OpenAI Codex assistance. Apache-2.0. +Predecessor algorithms are imported only after checking exact source pins. +""" + +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import search + +PROVIDER = "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck" +WORK = ("W", 0) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), ensure_ascii=True) + + +def payload(path): + data = path.read_bytes() + return gzip.decompress(data) if path.suffix == ".gz" else data + + +def read(path): + return json.loads(payload(path)) + + +def pin_check(): + pins = read(HERE / "SOURCES.json") + for name, entry in pins["files"].items(): + path = ROOT / name + need(entry["representation"] == ("gzip-payload" if path.suffix == ".gz" else "exact-bytes"), + "incorrect hash representation") + need(hashlib.sha256(payload(path)).hexdigest() == entry["sha256"], "source pin: " + name) + return pins + + +def module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + result = importlib.util.module_from_spec(spec) + spec.loader.exec_module(result) + return result + + +def sources(): + pins = pin_check() + reference = module("source29_reference", ROOT / "research/complex-dyadic-lowering/lower.py") + horner = module("source29_horner", ROOT / "research/dyadic-horner-direction/lower.py") + grid = module("source29_grid", ROOT / "research/jp8-grid-bounded-synthesis/synth.py") + accumulation = module("source29_accumulation", HERE / "vendor/pr999_lower.py") + programs = read(ROOT / PROVIDER / "LOCAL-PROGRAMS.json.gz") + spec = read(ROOT / "research/complex-k492-owner-repair/data/SPEC.json") + need(hashlib.sha256(payload(ROOT / PROVIDER / "LOCAL-PROGRAMS.json.gz")).hexdigest() == + spec["providers"]["ck"]["artifact_semantic_sha256"]["LOCAL-PROGRAMS.json.gz"], + "program does not match the historical provider SPEC") + return pins, reference, horner, grid, accumulation, programs, spec + + +def coefficient_inventory(programs): + inventories = {} + for orientation in ("forward", "backward"): + counts = Counter() + for event in programs[orientation]: + if event[0] == "scalar" and event[1][0] == "add": + counts[abs(Q(event[1][3], event[1][4]))] += 1 + inventories[orientation] = counts + need(set(inventories["forward"]) == set(inventories["backward"]), "coefficient domains differ") + return inventories + + +def comparator_words(q, reference, horner, grid, accumulation): + op = ["add", ["T", 0], ["S", 0], q.numerator, q.denominator] + choices = {"pr696": reference.lower(op)} + choices.update({"pr837_" + name: word for name, word in horner.candidates(op).items()}) + # Reuse the published PR882 graph method on eligible CK coefficients. + # This is an explicit transfer of its local algebraic method, not a claim + # that PR882's original 49-coefficient JP8 certificate covers CK. + if q != 1 and q.numerator <= 127 and q.denominator <= 16: + entry = grid.solve(q.numerator, q.denominator) + w = [("copy", WORK, ("S", 0))] + for tag in entry["operations"]: + w.append((tag, WORK, ("S", 0)) if tag in ("add", "subtract") else (tag, WORK)) + w += [("add" if entry["end_sign"] > 0 else "subtract", ("T", 0), WORK), ("clear", WORK)] + choices["pr882_method_on_ck"] = w + _, abstract = accumulation.addition(q) + names = {"T": ("T", 0), "S": ("S", 0), "W": WORK} + choices["pr999"] = [(p[0], *(names[r] for r in p[1:])) for p in abstract] + return choices + + +def step(rows, instruction): + """Sparse Fraction interpreter, including every arbitrary input column.""" + tag, target = instruction[:2] + if tag == "clear": + rows[target] = {} + elif tag == "copy": + rows[target] = dict(rows[instruction[2]]) + elif tag in ("double", "halve", "negate"): + factor = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[target] = {column: factor * value for column, value in rows[target].items()} + elif tag in ("add", "subtract"): + for column, value in list(rows[instruction[2]].items()): + value = rows[target].get(column, 0) + (value if tag == "add" else -value) + if value: + rows[target][column] = value + else: + rows[target].pop(column, None) + else: + raise ValueError("unknown primitive") + + +def local_check(q, word): + t, s = ("T", 0), ("S", 0) + rows = {t: {0: Q(1)}, s: {1: Q(1)}, WORK: {2: Q(1)}} + for primitive in word: + step(rows, primitive) + need(rows == {t: {0: Q(1), 1: q}, s: {1: Q(1)}, WORK: {}}, + "local shear or source restoration or private clearing") + + +def two_register_word(gates, negative=False): + out = [] + for name in gates: + index = search.GATES.index(name) + # Conjugation by diag(1,-1) relabels addition signs without gates. + if negative and index < 4: + index ^= 1 + if index < 4: + target, source = (("T", 0), ("S", 0)) if index < 2 else (("S", 0), ("T", 0)) + out.append(("add" if index % 2 == 0 else "subtract", target, source)) + else: + tag, target = (("double", "T"), ("halve", "T"), ("double", "S"), + ("halve", "S"), ("negate", "T"), ("negate", "S"))[index - 4] + out.append((tag, (target, 0))) + return out + [("clear", WORK)] + + +def shortcut(op, reference): + if op[0] == "add": + q = Q(op[3], op[4]) + if abs(q) in (2, 3): + # Validate all inherited alias/coefficient restrictions as well. + reference.lower(op) + return [("add" if q > 0 else "subtract", tuple(op[1]), tuple(op[2]))] * abs(q.numerator) + [("clear", WORK)] + return reference.lower(op) + + +def scalar_replay(events, reference, use_shortcut, orientation): + registers = set() + paid = Counter() + for event in events: + if event[0] == "scalar": + op = event[1] + registers.add(tuple(op[1])) + if op[0] in ("copy", "add"): + registers.add(tuple(op[2])) + elif event[0] == "climb": + paid[event[5]] += 1 + elif event[0] == "center": + paid[event[4]] += 1 + else: + need(event[0] in ("phase", "adapter", "residual_adapter"), "unknown non-scalar event") + registers.add(WORK) + for i in range(716): + registers.add(("L", i)) + rows = {r: {r: Q(1)} for r in registers} + magnitude = {r: Q(1) for r in registers} + peak = Q(1) + positive_peak = Q(1) + denominator_bits = 0 + word_hash = hashlib.sha256() + operations = Counter() + macros = changed = 0 + for event in events: + if event[0] != "scalar": + continue + op, frame = event[1:] + macros += 1 + old = reference.lower(op) + word = shortcut(op, reference) if use_shortcut else old + changed += word != old + for instruction in word: + operations[instruction[0]] += 1 + word_hash.update((canonical([instruction, frame]) + "\n").encode()) + step(rows, instruction) + target = instruction[1] + tag = instruction[0] + if tag == "clear": + magnitude[target] = Q(0) + elif tag == "copy": + magnitude[target] = magnitude[instruction[2]] + elif tag in ("double", "halve"): + magnitude[target] *= Q(2) if tag == "double" else Q(1, 2) + elif tag in ("add", "subtract"): + magnitude[target] += magnitude[instruction[2]] + positive_peak = max(positive_peak, magnitude[target]) + row = rows[target] + peak = max(peak, sum(map(abs, row.values()), Q(0))) + denominator_bits = max(denominator_bits, max((x.denominator.bit_length() - 1 for x in row.values()), default=0)) + if op[0] == "add": + need(not rows[WORK], "dirty coefficient work escaped a macro") + for i in range(716): + expected = {("L", i): Q(1)} + if orientation == "forward" and 112 <= i < 224: + expected[("L", i - 112)] = Q(1) + elif orientation == "backward" and i < 112: + expected[("L", i + 112)] = Q(-1) + need(rows[("L", i)] == expected, "full CK endpoint at native row " + str(i)) + row_data = [[list(r), [[list(c), str(v)] for c, v in sorted(rows[r].items())]] for r in sorted(rows)] + return { + "input_columns": len(registers), "native_columns": 716, + "scalar_macros": macros, "replaced_macros": changed, + "real_component_primitives": 2 * sum(operations.values()), + "one_component_operations": dict(sorted(operations.items())), + "exact_row_l1_peak": str(peak), "exact_denominator_bits": denominator_bits, + "cancellation_free_peak": str(positive_peak), + "paid_profile": {str(k): v for k, v in sorted(paid.items())}, + "primitive_stream_sha256": word_hash.hexdigest(), + "endpoint_sha256": hashlib.sha256(canonical(row_data).encode()).hexdigest(), + "endpoint_private_cells_cleared": all(not row for reg, row in rows.items() if reg[0] != "L"), + "endpoint_native_helpers_restored": all(rows[("L", i)] == {("L", i): Q(1)} for i in range(224, 716)), + } + + +def controls(reference): + t, s = ("T", 0), ("S", 0) + valid = [("add", t, s)] * 3 + [("clear", WORK)] + cases = { + "missing_source_read": valid[1:], + "wrong_sign": [("subtract", t, s)] + valid[1:], + "dirty_work_not_cleared": valid[:-1], + "source_not_restored": [("double", s)] + valid, + "target_dirt_lost": [("clear", t)] + valid, + "work_dirt_used_as_source": [("add", t, WORK)] + valid, + } + rejected = [] + for name, word in cases.items(): + try: + local_check(Q(3), word) + except ValueError: + rejected.append(name) + else: + raise ValueError("accepted control: " + name) + for label, op in { + "source_target_alias": ["add", list(t), list(t), 2, 1], + "source_work_alias": ["add", list(t), list(WORK), 3, 1], + "nondyadic": ["add", list(t), list(s), 1, 3], + }.items(): + try: + shortcut(op, reference) + except ValueError: + rejected.append(label) + else: + raise ValueError("accepted invalid macro: " + label) + # Neither a restricted alphabet nor a smaller ball is accepted as coverage. + try: + search.ball(order=search.ORDER[:-1]) + except ValueError: + rejected.append("missing_gate_from_alphabet") + else: + raise ValueError("accepted incomplete alphabet") + return rejected + + +def build(): + pins, reference, horner, grid, accumulation, programs, spec = sources() + inventory = coefficient_inventory(programs) + coefficients = sorted(inventory["forward"]) + need(len(coefficients) == 103, "CK coefficient inventory drift") + words, layers = search.ball() + result = search.metric(coefficients, words) + strict = [] + for entry, q in zip(result, coefficients): + choices = comparator_words(q, reference, horner, grid, accumulation) + for word in choices.values(): + local_check(q, word) + prices = {name: len(word) for name, word in choices.items()} + best = min(prices.values()) + # Any strict improvement pays a clear, so at most best-2 group gates. + need(best - 2 <= 2 * search.RADIUS, "search cutoff cannot decide improvement") + minimum = entry["two_register_minimum"] + improved = minimum is not None and minimum + 1 < best + if minimum is not None: + local_check(q, two_register_word(entry["word"])) + local_check(-q, two_register_word(entry["word"], negative=True)) + if improved: + strict.append(str(q)) + entry.update({ + "occurrences": {orientation: inventory[orientation][q] for orientation in inventory}, + "comparator_costs": prices, "best_comparator_cost": best, + "minimum_complete_cost": minimum + 1 if minimum is not None else None, + "complete_cost_lower_bound": entry["two_register_lower_bound"] + 1, + "strict_improvement": improved, + }) + need(strict == ["2", "3"], "unexpected improvement set; inspect mathematical result") + replays = {} + for orientation in ("forward", "backward"): + old = scalar_replay(programs[orientation], reference, False, orientation) + new = scalar_replay(programs[orientation], reference, True, orientation) + need(old["endpoint_sha256"] == new["endpoint_sha256"], "full arbitrary-input endpoint changed") + need(old["paid_profile"] == new["paid_profile"] == + {str(k): v for k, v in spec["providers"]["ck"]["expected_profile"].items()}, "paid profile changed") + need(old["exact_denominator_bits"] == new["exact_denominator_bits"], "fractional grid changed") + need(Q(new["exact_row_l1_peak"]) <= Q(old["exact_row_l1_peak"]), "prefix grew") + need(Q(new["cancellation_free_peak"]) <= Q(old["cancellation_free_peak"]), "positive envelope grew") + need(new["endpoint_private_cells_cleared"] and new["endpoint_native_helpers_restored"], "endpoint lifecycle failure") + replays[orientation] = {"pr696": old, "direct_shortcuts": new, + "saved_real_primitives": old["real_component_primitives"] - new["real_component_primitives"]} + return { + "schema": "restored-two-register-ck/1", "seed": search.SEED, + "base_commit": pins["base_commit"], "provider": "historical PR626 CK", + "radius": search.RADIUS, "covered_word_length": 2 * search.RADIUS, + "alphabet": list(search.GATES), "layer_sizes": layers, + "ball_states": len(words), "distance_sha256": search.distance_digest(words), + "coefficient_count": len(coefficients), + "exact_minima": sum(row["two_register_minimum"] is not None for row in result), + "strict_improvement_coefficients": strict, + "coefficients": result, "scalar_replays": replays, + "negative_controls": controls(reference), + "kappa_claim": "none; selected frontier unchanged", + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", type=Path, help="write a fresh certificate; refuse overwrite") + parser.add_argument("--json", action="store_true") + args = parser.parse_args() + if args.write: + need(not args.write.exists(), "refusing to overwrite an existing certificate") + receipt = build() + if args.write: + with args.write.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(receipt, indent=2) + "\n") + else: + need(canonical(receipt) == canonical(read(HERE / "EXPECTED.json")), "complete certificate mismatch") + if args.json: + print(json.dumps(receipt, indent=2)) + print("PASS_RESTORED_SOURCE_CK coefficients=103 exact_minima=77 improvements=2,3 " + "saved_real=3124,3124 no_new_kappa") + + +if __name__ == "__main__": + main()