diff --git a/research/ck-grid-synthesis-seed24/CENSUS.json.gz b/research/ck-grid-synthesis-seed24/CENSUS.json.gz new file mode 100644 index 0000000000..b293518489 Binary files /dev/null and b/research/ck-grid-synthesis-seed24/CENSUS.json.gz differ diff --git a/research/ck-grid-synthesis-seed24/CLAIM.json b/research/ck-grid-synthesis-seed24/CLAIM.json new file mode 100644 index 0000000000..70f4829a8e --- /dev/null +++ b/research/ck-grid-synthesis-seed24/CLAIM.json @@ -0,0 +1,21 @@ +{ + "track": "complex supplier", + "assignment_seed": 24, + "random_source": "Python secrets.randbelow(100), operating-system randomness", + "seed_generated_utc": "2026-10-13T18:06:08.791009+00:00", + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "claimed_utc": "2026-10-13T18:17:00Z", + "coordination": "No pinned sprint issue found; local claim and live PR overlap checks.", + "object": "All 103 absolute coefficient magnitudes in frozen PR626 CK forward/backward scalar streams; shortest single-scratch preparation with the original numerator magnitude and dyadic grid retained.", + "method": "Complete finite integer-state shortest paths, separate Bellman certificate check, exact macro and full scalar replay. Every COPY, source ADD/SUB, DOUBLE, HALF, accumulation and final dirty-work clear paid.", + "deliverable": "Scoped CK circuit construction or certified negative result, complete coefficient census and source-bound receipt; no new kappa.", + "expected_finish_utc": "2026-10-13T18:36:08Z", + "candidates": [ + "Canonical signed-digit fixed-macro lowering: rejected for overlap with PR723/734/787.", + "Same-source adjacent coefficient reuse: rejected for overlap with PR722/739/769/811.", + "CK grid-preserving single-scratch minima: selected; PR882 covers JP8, PR1036 covers source/target mutation." + ], + "stopping_rule": "Enumerate every vertex/edge for all 103 CK magnitudes once; finish one receipt and focused verification. Do not reopen the JP8 search or claim unrestricted circuit optimality.", + "time_note": "Fresh clone required because the old clone reported a truncated pack; orientation exceeded the intended first 20 percent. Remaining implementation is bounded and final 25 percent reserved for verification/handoff.", + "contributor": "Eva Ayala / ToikY, with substantial OpenAI Codex assistance" +} diff --git a/research/ck-grid-synthesis-seed24/EXPECTED.json b/research/ck-grid-synthesis-seed24/EXPECTED.json new file mode 100644 index 0000000000..e29417ff75 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/EXPECTED.json @@ -0,0 +1,833 @@ +{ + "comparisons": { + "1": { + "best_four_horner": 2, + "bounded_class_cost": 3, + "copy_binary": 2, + "installed": 2 + }, + "1/16": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "1/2": { + "best_four_horner": 4, + "bounded_class_cost": 4, + "copy_binary": 4, + "installed": 4 + }, + "1/4": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 5, + "installed": 5 + }, + "1/64": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "1/8": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "10": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "11": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "11/4": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 10, + "installed": 8 + }, + "12": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "125": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 14, + "installed": 12 + }, + "126": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 14, + "installed": 11 + }, + "128": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "13": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "13/2": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "13/4": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 10, + "installed": 8 + }, + "130": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "134": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "14": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "15": { + "best_four_horner": 8, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "15/2": { + "best_four_horner": 9, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "15/4": { + "best_four_horner": 10, + "bounded_class_cost": 9, + "copy_binary": 11, + "installed": 9 + }, + "15/8": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 12, + "installed": 8 + }, + "16": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "17": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "17/2": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "17/4": { + "best_four_horner": 10, + "bounded_class_cost": 9, + "copy_binary": 10, + "installed": 9 + }, + "17/8": { + "best_four_horner": 9, + "bounded_class_cost": 8, + "copy_binary": 11, + "installed": 8 + }, + "18": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "19": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "19/2": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "19/4": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "2": { + "best_four_horner": 4, + "bounded_class_cost": 4, + "copy_binary": 4, + "installed": 4 + }, + "20": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "21": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "21/4": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "22": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "23/2": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "23/8": { + "best_four_horner": 11, + "bounded_class_cost": 9, + "copy_binary": 13, + "installed": 9 + }, + "24": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "247/2": { + "best_four_horner": 14, + "bounded_class_cost": 15, + "copy_binary": 17, + "installed": 15 + }, + "249": { + "best_four_horner": 13, + "bounded_class_cost": 13, + "copy_binary": 15, + "installed": 13 + }, + "252": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 15, + "installed": 12 + }, + "255": { + "best_four_horner": 12, + "bounded_class_cost": 13, + "copy_binary": 17, + "installed": 13 + }, + "256": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "257/2": { + "best_four_horner": 13, + "bounded_class_cost": 13, + "copy_binary": 13, + "installed": 13 + }, + "26": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "260": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "27": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "27/2": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "28": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "29": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "29/2": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "29/8": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 13, + "installed": 10 + }, + "3": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 5, + "installed": 5 + }, + "3/2": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 6, + "installed": 5 + }, + "3/4": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 7, + "installed": 6 + }, + "3/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 8, + "installed": 7 + }, + "30": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 10, + "installed": 9 + }, + "31": { + "best_four_horner": 9, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "31/2": { + "best_four_horner": 10, + "bounded_class_cost": 11, + "copy_binary": 12, + "installed": 11 + }, + "31/4": { + "best_four_horner": 11, + "bounded_class_cost": 12, + "copy_binary": 13, + "installed": 12 + }, + "31/8": { + "best_four_horner": 11, + "bounded_class_cost": 10, + "copy_binary": 14, + "installed": 10 + }, + "32": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "33/2": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "34": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "35/8": { + "best_four_horner": 12, + "bounded_class_cost": 11, + "copy_binary": 13, + "installed": 11 + }, + "36": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "38": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "39/2": { + "best_four_horner": 11, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "39/8": { + "best_four_horner": 12, + "bounded_class_cost": 11, + "copy_binary": 14, + "installed": 11 + }, + "4": { + "best_four_horner": 5, + "bounded_class_cost": 5, + "copy_binary": 5, + "installed": 5 + }, + "40": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "48": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "5": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "5/2": { + "best_four_horner": 7, + "bounded_class_cost": 6, + "copy_binary": 7, + "installed": 6 + }, + "5/4": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 8, + "installed": 6 + }, + "5/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 9, + "installed": 7 + }, + "512": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "52": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "54": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "58": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "6": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "60": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 11, + "installed": 10 + }, + "62": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 12, + "installed": 10 + }, + "63": { + "best_four_horner": 10, + "bounded_class_cost": 11, + "copy_binary": 13, + "installed": 11 + }, + "63/2": { + "best_four_horner": 11, + "bounded_class_cost": 12, + "copy_binary": 14, + "installed": 12 + }, + "64": { + "best_four_horner": 9, + "bounded_class_cost": 9, + "copy_binary": 9, + "installed": 9 + }, + "65": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "67": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "67/2": { + "best_four_horner": 12, + "bounded_class_cost": 12, + "copy_binary": 12, + "installed": 12 + }, + "68": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "7": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "7/2": { + "best_four_horner": 8, + "bounded_class_cost": 7, + "copy_binary": 8, + "installed": 7 + }, + "7/4": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 9, + "installed": 7 + }, + "7/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 10, + "installed": 7 + }, + "72": { + "best_four_horner": 10, + "bounded_class_cost": 10, + "copy_binary": 10, + "installed": 10 + }, + "76": { + "best_four_horner": 11, + "bounded_class_cost": 11, + "copy_binary": 11, + "installed": 11 + }, + "8": { + "best_four_horner": 6, + "bounded_class_cost": 6, + "copy_binary": 6, + "installed": 6 + }, + "9": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 7, + "installed": 7 + }, + "9/2": { + "best_four_horner": 8, + "bounded_class_cost": 8, + "copy_binary": 8, + "installed": 8 + }, + "9/4": { + "best_four_horner": 8, + "bounded_class_cost": 7, + "copy_binary": 9, + "installed": 7 + }, + "9/8": { + "best_four_horner": 7, + "bounded_class_cost": 7, + "copy_binary": 10, + "installed": 7 + } + }, + "controls": { + "endpoint_neutral_finer_grid": "fractional grid", + "endpoint_neutral_growth": "magnitude envelope", + "missing_clear": "macro endpoint", + "missing_copy": "dirty work initialization", + "uncharged_redundant_ops": "macro cost", + "wrong_accumulation": "macro endpoint" + }, + "graphs": { + "census_sha256": "8c94db25fd01b1220253d1f330665d4f6e5ff982e3af0f09854ba870d7e83826", + "coefficients": 103, + "labelled_edges": 96929, + "negative_controls": [ + "wrong_bound", + "missing_vertex", + "duplicate_vertex", + "wrong_distance", + "boolean_distance", + "wrong_word", + "unknown_primitive", + "wrong_cost", + "wrong_terminal_sign" + ], + "preparation_operations": 617, + "relaxation_rounds": 1609, + "signed_dirty_macro_columns": 618, + "source_payload_sha256": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "vertices": 16251 + }, + "magnitudes": 103, + "programs": { + "backward": { + "baseline_real_primitives": 169634, + "best_four_horner_complete_real_primitives": 168504, + "changed_coefficients": { + "11/4": 1, + "125": 1, + "126": 4, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "247/2": 1, + "249": 1, + "252": 2, + "255": 1, + "29/8": 1, + "3/2": 89, + "3/4": 259, + "3/8": 9, + "30": 5, + "31": 1, + "31/2": 2, + "31/4": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "5/4": 18, + "5/8": 5, + "60": 4, + "62": 2, + "63": 5, + "63/2": 1, + "7/2": 26, + "7/4": 6, + "7/8": 2, + "9/4": 5, + "9/8": 3 + }, + "charged_payload_bits": 192, + "columns": 725, + "dirty_helpers": 492, + "net_saving_vs_complete_four_horner": 180, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_sha256": "247423364c6cf48ffe178c5a4ceed808df465d5762e84455581bf29b1a20fbad", + "primitive_tags": { + "add": 24194, + "clear": 42934, + "copy": 30452, + "double": 9740, + "halve": 38998, + "negate": 696, + "subtract": 21310 + }, + "replacement_real_primitives": 168324, + "retained_original_envelope": "146068000389976309073/32", + "saving": 1310, + "selected_occurrence_saving_vs_four_horner": 234, + "strictly_beyond_four_horner": { + "11/4": 1, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "29/8": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "7/2": 26, + "9/4": 5 + } + }, + "forward": { + "baseline_real_primitives": 169618, + "best_four_horner_complete_real_primitives": 168488, + "changed_coefficients": { + "11/4": 1, + "125": 1, + "126": 4, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "247/2": 1, + "249": 1, + "252": 2, + "255": 1, + "29/8": 1, + "3/2": 89, + "3/4": 259, + "3/8": 9, + "30": 5, + "31": 1, + "31/2": 2, + "31/4": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "5/4": 18, + "5/8": 5, + "60": 4, + "62": 2, + "63": 5, + "63/2": 1, + "7/2": 26, + "7/4": 6, + "7/8": 2, + "9/4": 5, + "9/8": 3 + }, + "charged_payload_bits": 192, + "columns": 725, + "dirty_helpers": 492, + "net_saving_vs_complete_four_horner": 180, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "primitive_sha256": "a189dfbdb7f3b8d61bfdff1c264cfd905a54350b17c87e8cd8cc2ca3958d25ed", + "primitive_tags": { + "add": 23796, + "clear": 42918, + "copy": 30468, + "double": 9740, + "halve": 38998, + "negate": 696, + "subtract": 21692 + }, + "replacement_real_primitives": 168308, + "retained_original_envelope": "920709848294", + "saving": 1310, + "selected_occurrence_saving_vs_four_horner": 234, + "strictly_beyond_four_horner": { + "11/4": 1, + "13/4": 1, + "15/4": 4, + "15/8": 3, + "17/4": 3, + "17/8": 1, + "19/4": 4, + "21/4": 2, + "23/8": 5, + "29/8": 1, + "31/8": 4, + "35/8": 1, + "39/8": 2, + "5/2": 49, + "7/2": 26, + "9/4": 5 + } + } + }, + "status": "PASS_CK_GRID_SYNTHESIS" +} diff --git a/research/ck-grid-synthesis-seed24/OVERLAP.json b/research/ck-grid-synthesis-seed24/OVERLAP.json new file mode 100644 index 0000000000..29cd0aa5bb --- /dev/null +++ b/research/ck-grid-synthesis-seed24/OVERLAP.json @@ -0,0 +1,133 @@ +{ + "checked_utc": "2026-10-13T18:28:00Z", + "open_issues": [ + { + "number": 913, + "title": "All size/compiler is retained" + }, + { + "number": 650, + "title": "Can we turn on Discussions?" + } + ], + "latest_open_prs": [ + { + "number": 1113, + "title": "Research: exclude a finite precision neighborhood of R439 matching optima" + }, + { + "number": 1112, + "title": "Independent verification: selected PR1042 finite invoice, 9 guards, 14 bootstrap steps and 94 outer slacks (seed 81, no new kappa)" + }, + { + "number": 1111, + "title": "Conditional κ = 0.001672780159952542: reverse one entrance promotion to fill T16 gaps" + }, + { + "number": 1110, + "title": "Research consolidation: reconcile PR225 five-stage pricing with exact intervals (no new kappa)" + }, + { + "number": 1108, + "title": "Research: exact compact-control boundary cancellation obstruction (no new kappa)" + }, + { + "number": 1107, + "title": "Conditional κ = 0.001672765980186726: rank-seven helper ends and T16 owner packing on the seven-slot k8 word" + }, + { + "number": 1106, + "title": "Mathematical audit: PR1064 nine-shift factory gauge is unique" + }, + { + "number": 1105, + "title": "Mathematical audit: raw endpoint independence does not justify target-feedback cleanup" + }, + { + "number": 1104, + "title": "Conditional κ = 0.001672691689152441: rank-seven helper ends and T16 owner packing on the seven-slot k8 word" + }, + { + "number": 1103, + "title": "Research: rectangular output borrowing and complete minimum-word census (no new kappa)" + }, + { + "number": 1102, + "title": "Audit: two inputs optimally detect all PR967 single-ADD omissions" + }, + { + "number": 1101, + "title": "Tooling: overlap bit589 and complex741 in the #741 ancestry replay, 17% (50% with --complex-jobs 3) less wall time (no new kappa)" + }, + { + "number": 1100, + "title": "Research: give short donor certificates for R439 class exclusions" + }, + { + "number": 1099, + "title": "Tooling: accelerate exact frame-pair enumeration with unchanged D/E/H checks" + }, + { + "number": 1098, + "title": "Independent verification: label-free P112 Gram support spectra (no new kappa)" + }, + { + "number": 1097, + "title": "Research consolidation: checked P111 minrank and fitting-matrix uniqueness proofs" + }, + { + "number": 1096, + "title": "Finite precision audit: PR589 bank envelope uses 132 bits versus a 177-bit bound" + }, + { + "number": 1095, + "title": "Certify exact prefix-monomial costs for 168 historical complex boundaries" + }, + { + "number": 1094, + "title": "Conditional kappa 0.001672660197076918: rare-pattern T16 exchanges" + }, + { + "number": 1093, + "title": "Research: tighten fixed precision for a complete signed inverse word" + }, + { + "number": 1092, + "title": "Tooling: exact Clifford state reuse with independent controls (no new kappa)" + }, + { + "number": 1091, + "title": "Research audit: independent owner-map check of all 15 open T16 claims on the seven-slot k8 word (no new kappa)" + }, + { + "number": 1090, + "title": "Conditional κ = 0.001672404744903063: rank-seven helper ends on the k8 word" + }, + { + "number": 1089, + "title": "Finite bit construction: R480 Q-node5 saves 20 ADDs (no new kappa)" + }, + { + "number": 1088, + "title": "Research: exact weighted optimum for signed 3x3 connector repairs (no new kappa)" + } + ], + "refreshed_heads": [ + { + "pr": 882, + "head": "e698981e0ffa680b6c5896dace1609025b97ad70", + "state": "closed" + }, + { + "pr": 1036, + "head": "c4ad801099d0813ffac56f0b517a908cd8ae0c6a", + "state": "open" + }, + { + "pr": 999, + "head": "fd38a824adb3a5c60c101a86c950a6d590454adf", + "state": "open" + } + ], + "distinction": "CK complete grid-bounded single-scratch graphs, not PR882 JP8, PR1036 source/target mutation, PR999 multiple target updates or already-covered signed-Horner/work-sharing. No pending implementation consumed." +} diff --git a/research/ck-grid-synthesis-seed24/PROOF.md b/research/ck-grid-synthesis-seed24/PROOF.md new file mode 100644 index 0000000000..30803c1793 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/PROOF.md @@ -0,0 +1,69 @@ +# Finite class, complete cost and inherited prefix bounds + +The source and target are distinct and never written during preparation. +Private work may be arbitrarily dirty. For reduced `|q|=a/D`, where `D` is a +power of two, the searched word has one initial COPY, an arbitrary finite +preparation, one target ADD/SUB, and one final CLEAR. Preparation may use +unit source ADD/SUB, DOUBLE, HALF, NEGATE, COPY and CLEAR on work only, while +its coefficient remains in `D^-1 Z` and has absolute value at most `a`. +The unit macro's cheaper direct two-instruction lowering is outside this +mandatory-copy form and is retained. + +Write `W=(x/D)S`. Every admissible preparation is exactly a walk on the full +integer vertex set `[-aD,aD]`, starting at `D` and ending at either `a` or `-a`. +The unit-cost transitions are `x+D`, `x-D`, `2x`, `-x`, `0`, `D`, and `x/2` +when `x` is even; only destinations in the vertex set are admitted. This +describes all words of arbitrary length in this class. Any repeated-state +cycle can be removed without increasing cost. The three instructions outside +the walk are all paid, giving complete cost `3+min(d(a),d(-a))`. + +The construction uses breadth-first search from `D`. A separately implemented +synchronous Bellman recurrence rebuilds every label. Every edge `x -> y` +satisfies `d(y)<=d(x)+1`; telescoping from `d(D)=0` lower-bounds every path's +length by its endpoint label. Every noninitial vertex has an attaining +predecessor, and the submitted witness explicitly attains the lesser goal +label. These exact obligations prove optimality in the declared finite graph. +They do not prove optimality with extra registers, changed source/target, +multiple target updates, different initialization, a finer grid, a larger +envelope, macro reuse or physical tape instructions. The frozen inventory +from both CK programs is compared to all 103 certificate records. + +After COPY, induction gives `W=(x/D)S` for arbitrary inputs. Adjusting the +target accumulation sign for the witness's terminal sign produces exactly +`T+qS`, with unchanged `S`; CLEAR leaves zero work. Testing all three formal +columns establishes the entire linear map, including dirty work and +correlated inputs. Applying the real-coefficient identity to each complex +component proves the same complex boundary map. Substitution at every +original macro boundary preserves subsequent states by induction. Paid +events, frames and recursive children are retained, rather than commuted or +omitted. The scalar projection does not execute physical frame operators. + +The original binary preparation reaches `aS` before terminal halvings. Every +candidate prefix has `|W|<=a|S|`, so its work magnitude and row-L1 norm are +bounded by that original attained state. Source and target values before +and after the single update, initial private dirt and final zero also match +the original boundary values. This proves maximum-row/prefix domination; +it does not claim literal prefix containment or entrywise domination of +simultaneous transfer matrices. The verifier separately reconstructs the +original nonnegative Horner envelope from every event and matches the pinned +independent receipt: `920709848294` forward and +`146068000389976309073/32` backward, within the retained 192-bit allowance. +Candidate macro checks certify the local bound used in this substitution +argument, and complete sparse primitive replay certifies both endpoints. + +For fractional depth, a prefix work coefficient is `x*s_j/D` for each source +row coefficient `s_j`. If `D>1`, reduced `a` is odd, so its denominator depth +is no larger than that of the original attained terminal coefficient +`a*s_j/D`. For `D=1` the multiplier is integral, so the original leading +source state already bounds its denominator depth. All other register states +are unchanged at boundaries. Thus these substitutions need no finer scalar +prefix grid than original/copy binary Horner. This is not a full physical +rounding, overflow, tape or compiler precision certificate. + +The net saving against PR837 is a complete instruction recount, including +cost increases at some coefficients. It is not obtained by summing only +strict improvements. More source additions can replace shifts, and each is +charged; no physical memory-traffic or runtime inference follows. Paid ranks +and assembly choices stay fixed, so these finite circuits give no new kappa. +Inherited all-size and physical interfaces remain assumptions, and finite +graph/column verification is not a formal multiplication theorem proof. diff --git a/research/ck-grid-synthesis-seed24/README.md b/research/ck-grid-synthesis-seed24/README.md new file mode 100644 index 0000000000..93a85eece4 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/README.md @@ -0,0 +1,103 @@ +# CK grid-preserving single-scratch coefficient circuits + +Finite complex-supplier construction and scoped optimality certificate; **no +new kappa**. This supplies a CK companion to Philipp / @mightyOil's JP8 search +in [PR882](https://github.com/CrocSwap/integer-mult-bounds/pull/882). It covers +all 103 magnitudes in the historical PR626 CK streams, including numerators +through 512 and denominators through 64, rather than reopening the JP8 domain. + +| Complete CK scalar projection | PR696 copy/unit | Best four PR837 Horner choices | This construction | +| --- | ---: | ---: | ---: | +| Forward | 169,618 | 168,488 | 168,308 | +| Backward / inverse-transpose | 169,634 | 168,504 | 168,324 | + +The saving is **1,310 real-component primitives per orientation against +PR696**, or **180 net against the complete four-Horner comparator**. At the +individual occurrences that strictly beat every Horner choice the saving is +234; other occurrences cost 54 more than that comparator, giving the stated +net 180. All original magnitude envelopes and coefficient grids are retained. +These are finite instruction counts, not measured runtime improvements. + +Run offline with standard-library Python 3.11+: + +```sh +python3 -B -I research/ck-grid-synthesis-seed24/verify.py +python3 -B -I research/ck-grid-synthesis-seed24/independent.py +python3 -B -I research/ck-grid-synthesis-seed24/test_package.py +``` + +Main expected marker: + +```text +PASS_CK_GRID_SYNTHESIS magnitudes=103 programs=2 columns=725 savings=1310,1310 no_new_kappa +``` + +The default verifier writes nothing and compares its complete deterministic +receipt to [EXPECTED.json](EXPECTED.json). `--write-certificate` explicitly +regenerates that receipt after all checks. [CENSUS.json.gz](CENSUS.json.gz) +contains every graph distance and chosen preparation witness; equality is on +decoded JSON, not gzip packaging. [SOURCES.json](SOURCES.json) binds the seven +consumed inputs by payload SHA256 and records their immutable Git blobs. + +For `q = +/-a/D`, preparation starts with one paid `COPY W <- S`, stays on +the grid `D^-1 Z` with `|W/S| <= a`, and ends at either signed coefficient +`+/-a/D`. Every source ADD/SUB, DOUBLE, HALF, NEGATE, COPY or CLEAR costs one. +One signed target accumulation and one final CLEAR complete the map +`(T,S,W) -> (T+qS,S,0)`, including arbitrary initial work. The accepted unit +macro costs two and is kept separately. Every primitive uses the original +macro frame; source, helper count, paid children and event boundaries stay +fixed. No additional source access, frame change, copy, restoration or child +is hidden in these counts. Only a strictly shorter complete word replaces +the PR696 word. + +The complete finite search comprises 16,251 vertices and 96,929 labelled +edges, with no depth cap, sampled coefficients or unresolved search nodes. +A separately written synchronous Bellman implementation checks every label, +edge inequality and shortest witness. This is independent AI implementation, +not independent human review. The primitive replay checks all 725 formal +input columns in both complete scalar programs: 224 data, 492 arbitrary dirty +helpers, eight dirty private centers and dirty coefficient work. Helpers are +restored and private cells erased. Nine graph controls, six macro controls +and focused whole-word/source/certificate tests check meaningful failures. +The [proof](PROOF.md) states exactly which minimum and prefix claims follow. + +Exact base: `ba82555c64e1879e4b7decce28186f208fcb8262`. OS assignment seed +**24**, complex-supplier track. The local [claim](CLAIM.json) records candidate +selection, stopping rule and timing. The old clone reported a truncated pack, +so this sprint used a fresh shallow clone and isolated `codex/complex-seed24` +branch. Orientation exceeded the intended first 20 percent; implementation +then stayed bounded and the final quarter was reserved for verification and +handoff. + +At this base the actual selected result is **PR1042**, conditional kappa +`1672188119205421/10^18 = 0.001672188119205421`, with reviewed source head +`7e8ef087c02a77038a28a337a7ee3a77039cac0d`. The selected record, manifest, +assembly, batch1047 review, mutable-leaver/slot construction and T16 owner +package were read. This contribution deliberately concerns historical CK, +not transport to that newly selected word. The paid profile is unchanged, +so no exponent improvement follows. + +PR723/734/787 already cover forward signed-digit recoding; PR837 supplies the +four-Horner comparator and PR866 explains the fractional-grid obligation. +PR722/739/769/811 reuse work across macros and are not composed here. +[PR1036](https://github.com/CrocSwap/integer-mult-bounds/pull/1036), by Hanson +Sun / @bbMisk, obtains larger CK savings in a distinct source/target mutation +class. Its two-register exclusion does not settle this single-scratch class; +we claim no stronger unrestricted circuit result. PR999 permits multiple +target accumulations and is also distinct. No pending implementation is a +code dependency, and no savings from these packages are added together. + +Credit Sagar Thakrar / @thakrarsagar's PR696 copy/unit lowering (also used in +the verifier adaptation), Gareth Davidson / @bitplane's PR837 comparator, +Philipp / @mightyOil's PR882 graph method and grid proof, Chris Pagolu's PR734, +Hanson Sun's PR1036, and the retained icekylinx / Jeremy Kothe / Chafik +Boukhalfa / DreamingOfClouds / Rohan Arun / eumemic construction lineage. +Prepared for **Eva Ayala / @ToikY with substantial OpenAI Codex assistance** +in selection, implementation, proof, verification and separate AI review. +Apache-2.0; no elementary shift/add synthesis priority is claimed. + +Production/native phase admission, complete global invoice and owner replay, +transport to PR1042 and all-size compiler/realization/hosting/precision/tape/ +analytic obligations remain separate. Full repository, supplier cold replay, +Lean and hosted CI passes are not claimed. `upstream/`, the production emitter +and selected frontier are unchanged. diff --git a/research/ck-grid-synthesis-seed24/SOURCES.json b/research/ck-grid-synthesis-seed24/SOURCES.json new file mode 100644 index 0000000000..212cd08978 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/SOURCES.json @@ -0,0 +1,28 @@ +{ + "base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262", + "git_blobs": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/INDEPENDENT-LOCAL-REPLAY.json": "ec8d742c3d932160fac10d0d9befdd2056cb240e", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json": "d2b8854114b19b88e14d2af0dd84ad79e9eedbaa", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": "61ef73c1f958e0d26f3e7a3a82bc3826b7098c93", + "research/complex-dyadic-lowering/EXPECTED.json": "6cdc73b8867b8e06f24a1c84d23baabfc7671cbf", + "research/complex-dyadic-lowering/lower.py": "a2c2889e5be41a0fc30d4dfa5dfcebb03d6d47f8", + "research/dyadic-horner-direction/lower.py": "a7855d2a87b77913bac097e1ece8ee35119bae28", + "research/dyadic-horner-direction/vendor/pr696_lower.py": "a2c2889e5be41a0fc30d4dfa5dfcebb03d6d47f8" + }, + "historical_pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "payload_sha256": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/INDEPENDENT-LOCAL-REPLAY.json": "ecefb9e661301d8081522be68bbe6640e175c011eb1177f643383d193c6fb2f0", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json": "059c4e59142bdf5c19dc7c0afebcddfec28e6e60cbc7299b8bdcc624afbc0cbe", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "research/complex-dyadic-lowering/EXPECTED.json": "81ec6ec0cbeeae16ee72fcfa956b42ff761eadd5985cf495714f323081440782", + "research/complex-dyadic-lowering/lower.py": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753", + "research/dyadic-horner-direction/lower.py": "6a7ae3f2aff61077ce4b3f179f7ccc2024f5176b5894547250eb14105b14f5e2", + "research/dyadic-horner-direction/vendor/pr696_lower.py": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + }, + "pr1036_head": "c4ad801099d0813ffac56f0b517a908cd8ae0c6a", + "pr622_head": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "pr696_head": "5a3f983715027c4fd83f50bc9001d4b18463bed1", + "pr837_head": "0a2977195efc8fb2a918fbfb694ec8d294387f08", + "pr882_head": "e698981e0ffa680b6c5896dace1609025b97ad70", + "pr883_head": "b31a870a3842b37f6ab97767c506ce91783632a2" +} diff --git a/research/ck-grid-synthesis-seed24/VALIDATION.md b/research/ck-grid-synthesis-seed24/VALIDATION.md new file mode 100644 index 0000000000..ca2e7e5101 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/VALIDATION.md @@ -0,0 +1,37 @@ +# Validation and handoff + +2026-10-13, macOS, bundled CPython 3.12.14, standard library only. +Base `ba82555c64e1879e4b7decce28186f208fcb8262`. + +Passed: + +```sh +python3 -B -I research/ck-grid-synthesis-seed24/verify.py --write-certificate +python3 -B -I -O research/ck-grid-synthesis-seed24/verify.py +python3 -B -I research/ck-grid-synthesis-seed24/independent.py +python3 -B -I -O research/ck-grid-synthesis-seed24/test_package.py +``` + +- Both complete literal primitive streams, all 725 formal columns, exact + endpoints, 492 restored helpers, private cleanup and unchanged paid profiles. +- All 103 magnitudes, 16,251 graph vertices and 96,929 labelled edges; separate + BFS and synchronous Bellman engines agree on every distance and signed witness. +- Nine graph and six macro controls; two complete-word controls reject a wrong + target sign and omitted work clear; two admission controls reject altered + source semantics and an understated certificate cost. Gzip repackaging passes. +- Isolated optimized replay from a minimal offline relocated checkout whose + path contains spaces, invoked from a different working directory, passes. +- Current selected certificate SHA256 and exact kappa agree with the record. + This small check is explicitly **not** the complete selected-record source + inventory check; the sparse research checkout omits unrelated packages. +- Staged whitespace and one-package scope checked before commit. + +No new dependency, native supplier regeneration, complete selected cold replay, +full repository suite, hosted CI, Lean or physical runtime benchmark was run. +Those passes are not claimed. The prefix/grid claim combines exact local macro +checks with the written substitution argument and reconstructed pinned original +envelopes; it is not an independent full physical precision certificate. + +The immediate overlap refresh through PR1113 is recorded in OVERLAP.json. +The closest input/comparison heads remained unchanged. No pinned coordination +issue existed. A local claim result will record the single published PR link. diff --git a/research/ck-grid-synthesis-seed24/independent.py b/research/ck-grid-synthesis-seed24/independent.py new file mode 100644 index 0000000000..5b5b0278db --- /dev/null +++ b/research/ck-grid-synthesis-seed24/independent.py @@ -0,0 +1,188 @@ +"""Independent integer-grid distance and dirty-macro checks for frozen CK words. + +Eva Ayala / ToikY, with substantial OpenAI Codex assistance; Apache-2.0. +No constructor imports. Distances use synchronous Bellman relaxation rather +than the construction's breadth-first queue. Optimality is only in the stated +bounded, single-work-register graph with paid COPY before preparation. +""" +import argparse +import copy +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def inventory(): + payload = gzip.decompress(SOURCE.read_bytes()) + programs = json.loads(payload) + require(set(programs) == {'forward', 'backward'}, 'source orientations') + values = set() + for events in programs.values(): + for event in events: + if event[0] == 'scalar' and event[1][0] == 'add': + q = abs(Fraction(event[1][3], event[1][4])) + require(q > 0, 'source coefficient zero') + values.add(q) + require(len(values) == 103, 'frozen CK coefficient inventory') + return values, hashlib.sha256(payload).hexdigest() + + +def transitions(x, denominator, bound): + """Enumerate every labelled graph edge; duplicate endpoints stay distinct.""" + destinations = { + 'add': x + denominator, 'subtract': x - denominator, + 'double': x * 2, 'negate': -x, 'clear': 0, 'copy': denominator, + } + if x % 2 == 0: + destinations['halve'] = x // 2 + return {tag: y for tag, y in destinations.items() if -bound <= y <= bound} + + +def dirty_macro(word, a, denominator, sign, terminal_sign): + """All three arbitrary input columns, represented in integer units 1/D.""" + source = [0, denominator, 0] + target = [denominator, 0, 0] + work = source.copy() # Paid COPY overwrites the arbitrary dirty work column. + for tag in word: + if tag == 'clear': + work = [0, 0, 0] + elif tag == 'copy': + work = source.copy() + elif tag == 'halve': + require(all(v % 2 == 0 for v in work), 'macro leaves the grid') + work = [v // 2 for v in work] + elif tag == 'double': + work = [2 * v for v in work] + elif tag == 'negate': + work = [-v for v in work] + elif tag in ('add', 'subtract'): + multiplier = 1 if tag == 'add' else -1 + work = [v + multiplier * s for v, s in zip(work, source)] + else: + raise ValueError('unknown preparation primitive') + target = [t + sign * terminal_sign * w for t, w in zip(target, work)] + work = [0, 0, 0] # Paid final CLEAR. + require(target == [denominator, sign * a, 0], 'dirty target map') + require(source == [0, denominator, 0] and work == [0, 0, 0], 'dirty restoration') + + +def check_record(q, record): + require(type(record) is dict and set(record) == {'a', 'D', 'bound', 'states', 'word', 'cost', 'terminal_sign'}, 'record schema') + a, denominator = q.numerator, q.denominator + for key, value in (('a', a), ('D', denominator), ('bound', a * denominator)): + require(type(record[key]) is int and record[key] == value, 'parameter ' + key) + bound = record['bound'] + vertices = list(range(-bound, bound + 1)) + require(type(record['states']) is list, 'state list') + labels = {} + for state in record['states']: + require(type(state) is dict and set(state) == {'x', 'distance'}, 'state schema') + x, distance = state['x'], state['distance'] + require(type(x) is int and type(distance) is int and distance >= 0, 'state integer labels') + require(x not in labels, 'duplicate state') + labels[x] = distance + require(set(labels) == set(vertices), 'complete vertex inventory') + edges = [(x, tag, y) for x in vertices for tag, y in transitions(x, denominator, bound).items()] + + # Complete synchronous shortest-distance recurrence. Each iteration admits + # one further edge, so convergence requires at most |V| iterations. + infinity = len(vertices) + 1 + distances = {x: infinity for x in vertices} + distances[denominator] = 0 + for rounds in range(1, len(vertices) + 1): + following = distances.copy() + for x, _tag, y in edges: + following[y] = min(following[y], distances[x] + 1) + if following == distances: + break + distances = following + else: + raise ValueError('Bellman relaxation did not converge') + require(all(d < infinity for d in distances.values()), 'unreachable graph vertex') + require(labels == distances, 'independent distance labels') + + # Explicit certificate obligations: edge lower bounds and attainment. + require(labels[denominator] == 0, 'start distance') + attained = {denominator} + for x, _tag, y in edges: + require(labels[y] <= labels[x] + 1, 'Bellman edge inequality') + if labels[y] == labels[x] + 1: + attained.add(y) + require(attained == set(vertices), 'shortest predecessor attainment') + require(type(record['word']) is list, 'word list') + x = denominator + for tag in record['word']: + require(type(tag) is str and tag in transitions(x, denominator, bound), 'witness edge') + x = transitions(x, denominator, bound)[tag] + terminal_sign = record['terminal_sign'] + require(type(terminal_sign) is int and terminal_sign in (-1, 1), 'terminal sign') + require(x == terminal_sign * a, 'witness endpoint') + shortest = min(labels[a], labels[-a]) + require(len(record['word']) == shortest, 'witness minimum length') + require(type(record['cost']) is int and record['cost'] == shortest + 3, 'paid copy/add/clear cost') + for sign in (1, -1): + dirty_macro(record['word'], a, denominator, sign, terminal_sign) + return len(vertices), len(edges), rounds, len(record['word']) + + +def negative_controls(census): + q = Fraction(1, 64) + original = census[str(q)] + mutations = {} + for name in ('wrong_bound', 'missing_vertex', 'duplicate_vertex', 'wrong_distance', 'boolean_distance', 'wrong_word', 'unknown_primitive', 'wrong_cost', 'wrong_terminal_sign'): + mutations[name] = copy.deepcopy(original) + mutations['wrong_bound']['bound'] += 1 + mutations['missing_vertex']['states'].pop() + mutations['duplicate_vertex']['states'].append(mutations['duplicate_vertex']['states'][0].copy()) + mutations['wrong_distance']['states'][0]['distance'] += 1 + mutations['boolean_distance']['states'][0]['distance'] = True + mutations['wrong_word']['word'].pop() + mutations['unknown_primitive']['word'].append('unpaid_halve') + mutations['wrong_cost']['cost'] -= 1 + mutations['wrong_terminal_sign']['terminal_sign'] *= -1 + rejected = [] + for name, mutation in mutations.items(): + try: + check_record(q, mutation) + except ValueError: + rejected.append(name) + else: + raise ValueError('accepted negative control: ' + name) + return rejected + + +def check(census): + values, source_hash = inventory() + require(type(census) is dict and set(census) == {str(q) for q in values}, 'complete coefficient census') + totals = [0, 0, 0, 0] + for q in sorted(values): + result = check_record(q, census[str(q)]) + totals = [x + y for x, y in zip(totals, result)] + return {'coefficients': len(values), 'vertices': totals[0], 'labelled_edges': totals[1], + 'relaxation_rounds': totals[2], 'preparation_operations': totals[3], + 'signed_dirty_macro_columns': 6 * len(values), 'source_payload_sha256': source_hash, + 'census_sha256': hashlib.sha256(json.dumps(census, sort_keys=True, separators=(',', ':')).encode()).hexdigest(), + 'negative_controls': negative_controls(census)} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('certificate', nargs='?', type=Path, default=HERE / 'CENSUS.json.gz') + args = parser.parse_args() + raw = args.certificate.read_bytes() + if args.certificate.suffix == '.gz': + raw = gzip.decompress(raw) + result = check(json.loads(raw)) + print(json.dumps(result, sort_keys=True)) + print('PASS_INDEPENDENT_CK_GRID coefficients=103 vertices=' + str(result['vertices'])) diff --git a/research/ck-grid-synthesis-seed24/synth.py b/research/ck-grid-synthesis-seed24/synth.py new file mode 100644 index 0000000000..c63fd34e25 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/synth.py @@ -0,0 +1,37 @@ +"""Finite CK single-scratch grid synthesis. Eva Ayala / ToikY + Codex; Apache-2.0.""" +from collections import deque + + +def edges(x, denominator, bound): + options = [('add', x + denominator), ('subtract', x - denominator), + ('double', 2 * x), ('negate', -x), ('clear', 0), + ('copy', denominator)] + if x % 2 == 0: + options.append(('halve', x // 2)) + return [(tag, y) for tag, y in options if abs(y) <= bound] + + +def solve(a, denominator): + if type(a) is not int or type(denominator) is not int or a <= 0 or denominator <= 0: + raise ValueError('positive integer parameters required') + if denominator & (denominator - 1): + raise ValueError('dyadic denominator required') + bound = a * denominator + distance, parent = {denominator: 0}, {} + pending = deque([denominator]) + while pending: + x = pending.popleft() + for tag, y in edges(x, denominator, bound): + if y not in distance: + distance[y] = distance[x] + 1 + parent[y] = (x, tag) + pending.append(y) + goal = min((a, -a), key=lambda x: distance[x]) + word, x = [], goal + while x != denominator: + x, tag = parent[x] + word.append(tag) + return {'a': a, 'D': denominator, 'bound': bound, + 'states': [{'x': x, 'distance': distance[x]} for x in sorted(distance)], + 'word': word[::-1], 'terminal_sign': 1 if goal > 0 else -1, + 'cost': distance[goal] + 3} diff --git a/research/ck-grid-synthesis-seed24/test_package.py b/research/ck-grid-synthesis-seed24/test_package.py new file mode 100644 index 0000000000..bb5d2fdc95 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/test_package.py @@ -0,0 +1,98 @@ +"""Focused admission and complete-word failure controls; Apache-2.0. + +Eva Ayala / ToikY, with substantial OpenAI Codex assistance. +Run from any directory with Python 3.10+ and its standard library. +""" +import copy +import gzip +import importlib.util +import json +from pathlib import Path +import tempfile +from unittest import mock + +spec = importlib.util.spec_from_file_location('ck_grid_audit', Path(__file__).resolve().parent/'verify.py') +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) + + +def rejects(action, expected): + try: + action() + except ValueError as error: + if expected not in str(error): + raise ValueError('unexpected rejection: ' + str(error)) from error + else: + raise ValueError('accepted failure control: ' + expected) + + +def run(): + census = audit.read(audit.HERE / 'CENSUS.json.gz') + reference = audit.load(audit.ROOT / 'research/complex-dyadic-lowering/lower.py', 'control_reference') + programs = audit.read(audit.DATA / 'LOCAL-PROGRAMS.json.gz') + checks = audit.read(audit.DATA / 'LOCAL-CHECKS.json')['forward'] + inherited = audit.read(audit.DATA / 'INDEPENDENT-LOCAL-REPLAY.json')['local']['forward'] + + # Alter the final target-writing addition rather than a preparation that + # could be cancelled by a later inverse. The complete map must reject it. + altered = copy.deepcopy(programs['forward']) + indices = [i for i, event in enumerate(altered) + if event[0] == 'scalar' and event[1][0] == 'add' + and event[1][1][0] == 'L' and 112 <= event[1][1][1] < 224] + if not indices: + raise ValueError('no forward target addition') + altered[indices[-1]][1][3] *= -1 + rejects(lambda: audit.replay('forward', altered, census, reference, checks, inherited), + 'full scalar endpoint') + + original_emit = audit.emit + + def omit_clear(op, *args): + word = original_emit(op, *args) + return word[:-1] if op[0] == 'add' else word + + with mock.patch.object(audit, 'emit', omit_clear): + rejects(lambda: audit.replay('forward', programs['forward'], census, reference, checks, inherited), + 'work survived macro') + + # Pin admission happens before mathematical replay. A semantic source edit + # must reject; a gzip-container change with the same payload remains valid. + source_names = audit.read(audit.HERE / 'SOURCES.json')['payload_sha256'] + with tempfile.TemporaryDirectory(prefix='ck-grid-source-control-') as temporary: + root = Path(temporary) + changed_name = 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz' + for name in source_names: + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + if name == changed_name: + changed_programs = copy.deepcopy(programs) + changed_programs['forward'][indices[-1]][1][3] *= -1 + path.write_bytes(gzip.compress(audit.canonical(changed_programs), mtime=7)) + else: + path.symlink_to(audit.ROOT / name) + with mock.patch.object(audit, 'ROOT', root): + rejects(audit.verify, 'source pin ' + changed_name) + + with tempfile.TemporaryDirectory(prefix='ck-grid-census-control-') as temporary: + here = Path(temporary) + (here / 'SOURCES.json').symlink_to(audit.HERE / 'SOURCES.json') + (here / 'synth.py').symlink_to(audit.HERE / 'synth.py') + changed = copy.deepcopy(census) + changed['1/64']['cost'] -= 1 + (here / 'CENSUS.json.gz').write_bytes(gzip.compress(audit.canonical(changed), mtime=0)) + with mock.patch.object(audit, 'HERE', here): + rejects(audit.verify, 'census mismatch') + + # Same semantic census under a different gzip timestamp is accepted by + # the payload reader and the independent checker. + (here / 'CENSUS.json.gz').write_bytes(gzip.compress(audit.canonical(census), mtime=123)) + recompressed = audit.read(here / 'CENSUS.json.gz') + if recompressed != census: + raise ValueError('gzip recompression changed semantic census') + independent = audit.load(audit.HERE / 'independent.py', 'recompression_independent') + independent.check(recompressed) + print('PASS_CK_GRID_PACKAGE full_word_rejections=2 admission_rejections=2 recompression=1') + + +if __name__ == '__main__': + run() diff --git a/research/ck-grid-synthesis-seed24/verify.py b/research/ck-grid-synthesis-seed24/verify.py new file mode 100644 index 0000000000..97d9561875 --- /dev/null +++ b/research/ck-grid-synthesis-seed24/verify.py @@ -0,0 +1,257 @@ +"""CK grid-preserving finite scalar construction; ToikY + substantial Codex assistance. + +Sparse primitive interpreter adapted from Sagar Thakrar's PR696 verify.py. +Apache-2.0. Independent graph certificate checker is in independent.py. +""" +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 + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +DATA = ROOT / 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck' +WORK = ('W', 0) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def step(rows, op): + tag, target = op[:2] + if tag == 'clear': + rows[target] = {} + elif tag == 'copy': + rows[target] = rows[op[2]].copy() + elif tag in ('double', 'halve', 'negate'): + factor = {'double': Q(2), 'halve': Q(1, 2), 'negate': Q(-1)}[tag] + rows[target] = {j: factor*x for j, x in rows[target].items()} + elif tag in ('add', 'subtract'): + row = rows[target] + for j, x in rows[op[2]].items(): + value = row.get(j, Q(0)) + (x if tag == 'add' else -x) + if value: + row[j] = value + else: + row.pop(j, None) + else: + raise ValueError('unknown primitive') + + +def emit(op, census, reference): + baseline = reference.lower(op) # Retains all domain and alias checks. + if op[0] != 'add' or abs(Q(op[3], op[4])) == 1: + return baseline + q = Q(op[3], op[4]) + entry = census[str(abs(q))] + if entry['cost'] >= len(baseline): + return baseline + source, target = tuple(op[2]), tuple(op[1]) + word = [('copy', WORK, source)] + for tag in entry['word']: + word.append((tag, WORK, source) if tag in ('add', 'subtract', 'copy') else (tag, WORK)) + word.extend([('add' if q*entry['terminal_sign'] > 0 else 'subtract', target, WORK), ('clear', WORK)]) + return word + + +def macro_check(q, word, expected_cost=None): + t, s = ('T', 0), ('S', 0) + rows = {t: {0: Q(1)}, s: {1: Q(1)}, WORK: {2: Q(1)}} + a, denominator = abs(q.numerator), q.denominator + for index, op in enumerate(word): + step(rows, op) + require(rows[s] == {1: Q(1)}, 'source restoration') + if index < len(word)-2: + require(rows[t] == {0: Q(1)}, 'early target update') + coefficient = rows[WORK].get(1, Q(0)) + require(set(rows[WORK]) <= {1}, 'dirty work initialization') + require(abs(coefficient) <= a, 'magnitude envelope') + require((coefficient*denominator).denominator == 1, 'fractional grid') + require(rows == {t: {0: Q(1), 1: q}, s: {1: Q(1)}, WORK: {}}, 'macro endpoint') + if expected_cost is not None: + require(len(word) == expected_cost, 'macro cost') + + +def replay(orientation, events, census, reference, checks, inherited): + n = 716 + rows = {('L', r): {r: Q(1)} for r in range(n)} + rows.update({('C', r): {n+r: Q(1)} for r in range(8)}) + rows[WORK] = {724: Q(1)} + env = {register: Q(1) for register in rows} + peak = Q(1) + paid, tags, changed = Counter(), Counter(), Counter() + old = macros = new = 0 + word_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': + require(event[0] in ('phase', 'adapter', 'residual_adapter'), 'unknown event') + else: + op, frame = event[1:] + target = tuple(op[1]) + baseline, word = reference.lower(op), emit(op, census, reference) + old += 2*len(baseline) + new += 2*len(word) + macros += 1 + if len(word) < len(baseline): + changed[str(abs(Q(op[3], op[4])))] += 1 + if op[0] == 'add': + source, q = tuple(op[2]), Q(op[3], op[4]) + peak = max(peak, abs(q.numerator)*env[source]) + env[target] = env[target] + abs(q)*env[source] + elif op[0] == 'scale': + env[target] *= abs(Q(op[2], op[3])) + elif op[0] == 'clear': + env[target] = Q(0) + elif op[0] == 'copy': + env[target] = env[tuple(op[2])] + peak = max(peak, env[target]) + for primitive in word: + step(rows, primitive) + tags[primitive[0]] += 2 + word_hash.update(canonical([frame, primitive])+b'\n') + if op[0] == 'add': + require(not rows[WORK], 'work survived macro') + for r in range(n): + wanted = {r: Q(1)} + if orientation == 'forward' and 112 <= r < 224: + wanted[r-112] = Q(1) + if orientation == 'backward' and r < 112: + wanted[r+112] = Q(-1) + require(rows[('L', r)] == wanted, 'full scalar endpoint') + require(all(not row for register, row in rows.items() if register[0] != 'L'), 'private cleanup') + require(dict(paid) == {int(k): v for k, v in checks['paid_profile'].items()}, 'paid profile') + require(macros == checks['scalar_macros'], 'macro inventory') + require(peak == Q(inherited['prefix_l1_upper']), 'original envelope') + require(peak < 2**inherited['charged_payload_bits'], 'charged magnitude budget') + return {'columns': 725, 'dirty_helpers': 492, 'baseline_real_primitives': old, + 'replacement_real_primitives': new, 'saving': old-new, + 'changed_coefficients': dict(sorted(changed.items())), + 'primitive_tags': dict(sorted(tags.items())), 'primitive_sha256': word_hash.hexdigest(), + 'paid_profile': dict(sorted(checks['paid_profile'].items())), + 'retained_original_envelope': str(peak), + 'charged_payload_bits': inherited['charged_payload_bits']} + + +def controls(census, reference): + q = Q(5, 2) + op = ['add', ['T', 0], ['S', 0], 5, 2] + word = emit(op, census, reference) + bad = { + 'missing_copy': word[1:], 'missing_clear': word[:-1], + 'wrong_accumulation': word[:-2]+[('subtract', ('T', 0), WORK)]+word[-1:], + 'endpoint_neutral_growth': word[:1]+[('double', WORK)]*5+[('halve', WORK)]*5+word[1:], + 'endpoint_neutral_finer_grid': word[:1]+[('halve', WORK)]*2+[('double', WORK)]*2+word[1:], + 'uncharged_redundant_ops': word[:1]+[('negate', WORK)]*2+word[1:], + } + rejected = {} + for name, candidate in bad.items(): + try: + macro_check(q, candidate, len(word)) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError('accepted control '+name) + require(rejected['endpoint_neutral_growth'] == 'magnitude envelope', 'growth reason') + require(rejected['endpoint_neutral_finer_grid'] == 'fractional grid', 'grid reason') + require(rejected['uncharged_redundant_ops'] == 'macro cost', 'cost reason') + return rejected + + +def verify(): + for name, sha in read(HERE/'SOURCES.json')['payload_sha256'].items(): + path = ROOT/name + raw = path.read_bytes() + if path.suffix == '.gz': + raw = gzip.decompress(raw) + require(hashlib.sha256(raw).hexdigest() == sha, 'source pin '+name) + reference = load(ROOT/'research/complex-dyadic-lowering/lower.py', 'pr696') + horner = load(ROOT/'research/dyadic-horner-direction/lower.py', 'pr837') + programs = read(DATA/'LOCAL-PROGRAMS.json.gz') + qs = sorted({abs(Q(e[1][3], e[1][4])) for es in programs.values() + for e in es if e[0] == 'scalar' and e[1][0] == 'add'}) + solve = load(HERE/'synth.py', 'synth_ck').solve + census = {str(q): solve(q.numerator, q.denominator) for q in qs} + require(canonical(census) == canonical(read(HERE/'CENSUS.json.gz')), 'census mismatch') + independent = load(HERE/'independent.py', 'independent_ck') + graph = independent.check(census) + comparisons = {} + for q in qs: + op = ['add', ['T', 0], ['S', 0], q.numerator, q.denominator] + word = emit(op, census, reference) + macro_check(q, word) + negative = ['add', ['T', 0], ['S', 0], -q.numerator, q.denominator] + macro_check(-q, emit(negative, census, reference)) + four = horner.candidates(op) + comparisons[str(q)] = {'copy_binary': len(reference.lower(op)), + 'best_four_horner': min(map(len, four.values())), + 'installed': len(word), 'bounded_class_cost': census[str(q)]['cost']} + checks = read(DATA/'LOCAL-CHECKS.json') + inherited = read(DATA/'INDEPENDENT-LOCAL-REPLAY.json')['local'] + result = {orientation: replay(orientation, programs[orientation], census, reference, + checks[orientation], inherited[orientation]) + for orientation in ('forward', 'backward')} + baseline_receipt = read(ROOT/'research/complex-dyadic-lowering/EXPECTED.json') + for orientation, events in programs.items(): + require(hashlib.sha256(canonical(events)).hexdigest() == checks[orientation]['sha256'], + 'program semantic hash') + require(result[orientation]['baseline_real_primitives'] == + baseline_receipt['programs']['ck/'+orientation]['new_real_primitives'], + 'copy binary complete baseline') + for orientation, events in programs.items(): + saving = 0 + four_total = 0 + cases = Counter() + for event in events: + if event[0] == 'scalar': + four_total += 2*min(map(len, horner.candidates(event[1]).values())) + if event[0] == 'scalar' and event[1][0] == 'add': + q = str(abs(Q(event[1][3], event[1][4]))) + c = comparisons[q] + if c['installed'] < c['best_four_horner']: + saving += 2*(c['best_four_horner']-c['installed']) + cases[q] += 1 + result[orientation]['selected_occurrence_saving_vs_four_horner'] = saving + result[orientation]['strictly_beyond_four_horner'] = dict(sorted(cases.items())) + result[orientation]['best_four_horner_complete_real_primitives'] = four_total + result[orientation]['net_saving_vs_complete_four_horner'] = four_total-result[orientation]['replacement_real_primitives'] + return {'status': 'PASS_CK_GRID_SYNTHESIS', 'magnitudes': len(qs), 'graphs': graph, + 'programs': result, 'comparisons': comparisons, 'controls': controls(census, reference)} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', action='store_true') + args = parser.parse_args() + result = verify() + if args.write_certificate: + (HERE/'EXPECTED.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + require(canonical(result) == canonical(read(HERE/'EXPECTED.json')), 'receipt mismatch') + print('PASS_CK_GRID_SYNTHESIS magnitudes=103 programs=2 columns=725 savings='+ + ','.join(str(p['saving']) for p in result['programs'].values())+' no_new_kappa')