diff --git a/research/dirty-echo-space-budget/CLAIM.json b/research/dirty-echo-space-budget/CLAIM.json new file mode 100644 index 0000000000..ca96772575 --- /dev/null +++ b/research/dirty-echo-space-budget/CLAIM.json @@ -0,0 +1,158 @@ +{ + "track": "recursive interfaces", + "assignment_seed": 50, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "started_at": "2026-10-13T00:53:05.729600-04:00", + "claimed_at": "2026-10-13T00:55:30.836858-04:00", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "object": "Ordered all-dirty product-shear trees formed from the PR673 multiway echo, under a caller-specified bound on simultaneously borrowed arrays.", + "method": "Exact dynamic programming over arbitrary positive contiguous child partitions and node fanouts, with the complete 2/4/2 child-call multiplicities and k-1 local arrays. Independent small-domain enumeration and symbolic noncommutative restoration checks.", + "seed_diversification": "The main generic instance has 50 ordered factors. The method changes the search class, rather than repeating balanced ternary placement.", + "domain": "Factor counts 1 through 64, scratch budgets 0 through 8; independent exhaustive tree enumeration in a smaller declared domain.", + "stopping_rule": "One deterministic optimum table for this grammar and budget domain, an executable schedule, complete cost recurrence, and negative controls; no search for a new kappa.", + "expected_deliverable": "Scoped interface construction and exact space/call tradeoff certificate; no multiplication bound claim.", + "expected_finish": "2026-10-13T01:53:05-04:00", + "time_allocation": "60-minute target; orientation at most 12 minutes, final 15 minutes reserved for verification and handoff.", + "coordination": { + "pinned_issues": [], + "open_issue_numbers": [ + 650 + ], + "claim_location": "local, because no pinned sprint coordination issue exists", + "open_prs_inspected": 544, + "checked_through_pr": 725 + }, + "candidate_tasks": [ + { + "task": "Optimal all-dirty echo trees under a fixed simultaneous scratch budget", + "decision": "selected; arbitrary partitions and mixed fanouts are outside the balanced family covered by PR689" + }, + { + "task": "Clean root checkpoint with dirty descendants", + "decision": "not selected; PR714 already supplies this construction and root optimum" + }, + { + "task": "Spectral split with a phase-restored dirty complement", + "decision": "not selected; PR665 already gives the complete unfavorable boundary bill" + } + ], + "overlap_heads": { + "628": "0768f97d06c623b8211e651543c66135796b62bf", + "673": "156f259b99723468cfdd2b5d47d0ba894f09bea7", + "689": "0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a", + "714": "efad8a40094ab453c0525efef0b0eff2a5d8b850" + }, + "predecessor_scope": { + "628": "binary dirty inverse and rounded leaf", + "673": "multiway echo identity, exact restoration and general error bound", + "689": "minimum among recursively balanced ternary splits, uniform leaf costs", + "714": "one clean root checkpoint with balanced binary dirty children" + }, + "status": "completed", + "completed_at": "2026-10-13T01:24:15.671435-04:00", + "final_overlap": { + "checked_at": "2026-10-13T01:22:02.586894-04:00", + "open_prs": 586, + "highest_pr": 767, + "related": [ + { + "number": 673, + "title": "Research: dirty echo, alias repair, and fully priced bit-sharing gates", + "headRefOid": "b3917936aafbd0d680a954a86e25c4ce7e28a9f9", + "updatedAt": "2026-10-13T05:17:11Z" + }, + { + "number": 758, + "title": "Research: higher-arity dirty echoes use 152 calls at five-array cap (no new kappa)", + "headRefOid": "a164f06263e438ead570b169e5b7103aa45bf228", + "updatedAt": "2026-10-13T05:10:54Z" + }, + { + "number": 744, + "title": "Independent verification: fixed-space ternary echo minima and rounded leaves", + "headRefOid": "302383e0c1ec71c50860362d3f394f85664c2445", + "updatedAt": "2026-10-13T05:10:23Z" + }, + { + "number": 730, + "title": "Research: optimize ordered dirty echoes at fixed scratch (no new kappa)", + "headRefOid": "d222e348179cc02a54d6d26dbd2838944f62c6e5", + "updatedAt": "2026-10-13T04:57:06Z" + }, + { + "number": 714, + "title": "Research: optimal clean root checkpoint saves 25\u201340% of binary product-shear calls", + "headRefOid": "efad8a40094ab453c0525efef0b0eff2a5d8b850", + "updatedAt": "2026-10-13T04:40:45Z" + }, + { + "number": 689, + "title": "Research: minimize balanced ternary dirty echo calls at fixed scratch", + "headRefOid": "0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a", + "updatedAt": "2026-10-13T04:14:38Z" + }, + { + "number": 525, + "title": "Kernel102 checkpoint: full cold reconstruction and exact fixed-word ceiling", + "headRefOid": "71acd0c35ee81de848316b3f2b4c3bd15b219c51", + "updatedAt": "2026-10-12T00:49:30Z" + }, + { + "number": 277, + "title": "Verified construction checkpoint: conditional \u03ba = 7.110455476244e-4", + "headRefOid": "c2f07d311bfdad0d89bf961e4da133ee97bb78de", + "updatedAt": "2026-10-10T04:22:16Z" + }, + { + "number": 135, + "title": "Paired physical scratch reuse: candidate conditional \u03ba = 3.62108222954e-4 (+4.02% vs #134)", + "headRefOid": "2bb675bba25771ae1cafd4ff7804b9bc094dd415", + "updatedAt": "2026-10-09T03:15:24Z" + }, + { + "number": 131, + "title": "Physical frames and scratch reuse on Cayley covers: conditional \u03ba = 3.32205398986e-4", + "headRefOid": "3acf2f944abd069301600ce468f16f1dd8f1f9e4", + "updatedAt": "2026-10-09T02:52:20Z" + }, + { + "number": 129, + "title": "Shared bit cores and gauged scratch reuse: conditional \u03ba = 1.29186205798e-4", + "headRefOid": "59fade1f7790db61a56b69e0d3974c0a97b41f4d", + "updatedAt": "2026-10-09T02:50:37Z" + }, + { + "number": 90, + "title": "Clarify current review checkpoint and published release", + "headRefOid": "8e0442641696b4c284bf7fbb4f2c97dccf24ea6c", + "updatedAt": "2026-10-08T21:24:49Z" + } + ], + "pinned_coordination_issues": [], + "main_head": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "pr673_consumed_files_unchanged_at_latest_head": "b3917936aafbd0d680a954a86e25c4ce7e28a9f9" + }, + "concurrent_contributions": { + "730": { + "head": "d222e348179cc02a54d6d26dbd2838944f62c6e5", + "credit": "unbalanced mixed binary/ternary weighted optimization" + }, + "744": { + "head": "302383e0c1ec71c50860362d3f394f85664c2445", + "credit": "independent strict-ternary census and rounded-leaf verification" + }, + "758": { + "head": "a164f06263e438ead570b169e5b7103aa45bf228", + "credit": "all-arity weighted optimization; actual planner and words independently compared at nine unit-price instances" + } + }, + "result": { + "status": "research note and independent verification; no new kappa", + "theorem": "Every ordered echo tree using at most s dirty arrays has N >= 2^(s+1)*n - 4^s; equality is attained for s>=2 and 3*2^(s-2)<=n<=2^s.", + "example": "F(50,6)=2304, versus 2752 in the pinned balanced binary schedule, with no additional array.", + "distinctness": "Concurrent PR758 already supplies all-arity optimization. The distinct result is the analytic scratch-dependent bound and explicit attaining family; optimizer minima are independent corroboration.", + "complete_search_domain": "All 576 cells n=1..64, s=0..8; 255 feasible witnesses; exact recurrence, no stochastic cutoff.", + "verification": "Python 3.11.15 and 3.14.7; all final certificate fields, relocation and seven artifact controls pass. make verify completed seven historical groups then stopped at inherited missing SymPy.", + "link": "https://github.com/AlexS-scale/integer-mult-bounds/tree/research/dirty-echo-space-budget-seed50/research/dirty-echo-space-budget" + } +} diff --git a/research/dirty-echo-space-budget/EXPECTED.json b/research/dirty-echo-space-budget/EXPECTED.json new file mode 100644 index 0000000000..6ff2ee4709 --- /dev/null +++ b/research/dirty-echo-space-budget/EXPECTED.json @@ -0,0 +1,1693 @@ +{ + "format": "ordered-dirty-echo-space-budget-v1", + "status": "passed", + "assignment_seed": 50, + "sources": { + "files": 13, + "manifest_sha256": "226e3ef62589608d22ed45f5c701b01db9fbd2cf2f52c79a4f7a926699459a60", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "heads": { + "628": "0768f97d06c623b8211e651543c66135796b62bf", + "673": "156f259b99723468cfdd2b5d47d0ba894f09bea7", + "689": "0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a", + "758": "a164f06263e438ead570b169e5b7103aa45bf228" + } + }, + "domain": { + "factors": [ + 1, + 64 + ], + "scratch_budget": [ + 0, + 8 + ], + "coverage": "all 576 cells; null denotes infeasibility", + "tree_encoding": "a leaf is '.', an internal node is its comma-separated children in parentheses", + "objective": "minimum uniform leaf calls in static ordered all-dirty echo trees" + }, + "costs_by_budget": [ + [ + 1, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 1, + 4, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 1, + 4, + 8, + 16, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 1, + 4, + 8, + 12, + 20, + 32, + 48, + 64, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 1, + 4, + 8, + 12, + 16, + 24, + 36, + 48, + 64, + 80, + 96, + 128, + 160, + 192, + 224, + 256, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 1, + 4, + 8, + 12, + 16, + 20, + 28, + 40, + 52, + 64, + 80, + 96, + 112, + 128, + 152, + 176, + 208, + 240, + 272, + 304, + 336, + 384, + 448, + 512, + 576, + 640, + 704, + 768, + 832, + 896, + 960, + 1024, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null, + null + ], + [ + 1, + 4, + 8, + 12, + 16, + 20, + 24, + 32, + 44, + 56, + 68, + 80, + 96, + 112, + 128, + 144, + 160, + 176, + 200, + 224, + 256, + 288, + 320, + 352, + 384, + 416, + 448, + 480, + 528, + 576, + 640, + 704, + 768, + 832, + 896, + 960, + 1024, + 1088, + 1152, + 1216, + 1280, + 1344, + 1408, + 1536, + 1664, + 1792, + 1920, + 2048, + 2176, + 2304, + 2432, + 2560, + 2688, + 2816, + 2944, + 3072, + 3200, + 3328, + 3456, + 3584, + 3712, + 3840, + 3968, + 4096 + ], + [ + 1, + 4, + 8, + 12, + 16, + 20, + 24, + 28, + 36, + 48, + 60, + 72, + 84, + 96, + 112, + 128, + 144, + 160, + 176, + 192, + 208, + 224, + 248, + 272, + 296, + 320, + 352, + 384, + 416, + 448, + 480, + 512, + 544, + 576, + 624, + 672, + 720, + 768, + 816, + 864, + 912, + 960, + 1024, + 1088, + 1152, + 1216, + 1280, + 1344, + 1408, + 1472, + 1536, + 1600, + 1664, + 1728, + 1792, + 1856, + 1952, + 2048, + 2144, + 2240, + 2368, + 2496, + 2624, + 2752 + ], + [ + 1, + 4, + 8, + 12, + 16, + 20, + 24, + 28, + 32, + 40, + 52, + 64, + 76, + 88, + 100, + 112, + 128, + 144, + 160, + 176, + 192, + 208, + 224, + 240, + 256, + 272, + 288, + 312, + 336, + 360, + 384, + 416, + 448, + 480, + 512, + 544, + 576, + 608, + 640, + 672, + 704, + 736, + 784, + 832, + 880, + 928, + 976, + 1024, + 1072, + 1120, + 1168, + 1216, + 1280, + 1344, + 1408, + 1472, + 1536, + 1600, + 1664, + 1728, + 1792, + 1856, + 1920, + 1984 + ] + ], + "main_witnesses": [ + { + "factors": 50, + "scratch_budget": 6, + "scratch_used": 6, + "baseline_source": "PR673", + "baseline_fanout": 2, + "baseline_scratch": 6, + "baseline_calls": 2752, + "minimum_calls": 2304, + "saved_calls": 448, + "root_partition": [ + 22, + 28 + ], + "tree": "(((((.,.),(.,.)),(.,.,.),((.,.),(.,.))),(((.,.),(.,.)),(.,.,.),((.,.),(.,.)))),((((.,.,.),(.,.,.)),((.,.,.),(.,.,.))),((((.,.),(.,.)),((.,.),(.,.))),(((.,.),(.,.)),((.,.),(.,.))))))", + "factor_multiplicities": [ + 32, + 32, + 32, + 32, + 32, + 64, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 64, + 32, + 32, + 32, + 32, + 32, + 32, + 64, + 32, + 32, + 64, + 32, + 32, + 64, + 32, + 32, + 64, + 32, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64, + 64 + ], + "all_feasible_pinned_baselines": [ + [ + 2752, + 6, + "PR673", + 2 + ] + ] + }, + { + "factors": 50, + "scratch_budget": 7, + "scratch_used": 7, + "baseline_source": "PR689", + "baseline_fanout": 3, + "baseline_scratch": 7, + "baseline_calls": 1568, + "minimum_calls": 1472, + "saved_calls": 96, + "root_partition": [ + 16, + 13, + 21 + ], + "tree": "((((.,.,.),(.,.,.)),(.,.,.,.),((.,.,.),(.,.,.))),((.,.,.,.),(.,.,.,.),((.,.),.,(.,.))),((((.,.),(.,.)),((.,.),(.,.))),((.,.),.,(.,.)),(((.,.),(.,.)),((.,.),(.,.)))))", + "factor_multiplicities": [ + 16, + 32, + 16, + 16, + 32, + 16, + 16, + 32, + 32, + 16, + 16, + 32, + 16, + 16, + 32, + 16, + 16, + 32, + 32, + 16, + 32, + 64, + 64, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32 + ], + "all_feasible_pinned_baselines": [ + [ + 1568, + 7, + "PR689", + 3 + ], + [ + 1904, + 7, + "PR673", + 3 + ], + [ + 2752, + 6, + "PR673", + 2 + ] + ] + }, + { + "factors": 50, + "scratch_budget": 8, + "scratch_used": 8, + "baseline_source": "PR689", + "baseline_fanout": 3, + "baseline_scratch": 7, + "baseline_calls": 1568, + "minimum_calls": 1120, + "saved_calls": 448, + "root_partition": [ + 18, + 12, + 20 + ], + "tree": "((((.,.),.,(.,.)),(.,.,.,.),(.,.,.,.),((.,.),.,(.,.))),((.,.,.,.,.,.),(.,.,.,.,.,.)),(((.,.,.),(.,.,.)),(.,.,.,.),(.,.,.,.),((.,.,.),(.,.,.))))", + "factor_multiplicities": [ + 16, + 16, + 16, + 16, + 16, + 16, + 32, + 32, + 16, + 16, + 32, + 32, + 16, + 16, + 16, + 16, + 16, + 16, + 16, + 32, + 32, + 32, + 32, + 16, + 16, + 32, + 32, + 32, + 32, + 16, + 16, + 32, + 16, + 16, + 32, + 16, + 16, + 32, + 32, + 16, + 16, + 32, + 32, + 16, + 16, + 32, + 16, + 16, + 32, + 16 + ], + "all_feasible_pinned_baselines": [ + [ + 1568, + 7, + "PR689", + 3 + ], + [ + 1904, + 7, + "PR673", + 3 + ], + [ + 2752, + 6, + "PR673", + 2 + ] + ] + } + ], + "concurrent_comparison": { + "source_pr": 758, + "source_commit": "a164f06263e438ead570b169e5b7103aa45bf228", + "cases": [ + { + "factors": 15, + "scratch_budget": 4, + "calls": 224, + "scratch_used": 4 + }, + { + "factors": 15, + "scratch_budget": 5, + "calls": 152, + "scratch_used": 5 + }, + { + "factors": 15, + "scratch_budget": 6, + "calls": 128, + "scratch_used": 6 + }, + { + "factors": 15, + "scratch_budget": 7, + "calls": 112, + "scratch_used": 7 + }, + { + "factors": 15, + "scratch_budget": 8, + "calls": 100, + "scratch_used": 8 + }, + { + "factors": 27, + "scratch_budget": 6, + "calls": 448, + "scratch_used": 6 + }, + { + "factors": 50, + "scratch_budget": 6, + "calls": 2304, + "scratch_used": 6 + }, + { + "factors": 50, + "scratch_budget": 7, + "calls": 1472, + "scratch_used": 7 + }, + { + "factors": 50, + "scratch_budget": 8, + "calls": 1120, + "scratch_used": 8 + } + ], + "scope": "Uniform-price agreement and exact symbolic forward/inverse words only; not review of the full PR or its weighted and numerical claims." + }, + "independent_checks": { + "exhaustive": { + "max_factors": 8, + "max_scratch": 8, + "trees_by_factors": [ + 1, + 1, + 3, + 11, + 45, + 197, + 903, + 4279 + ], + "trees": 5440, + "optimum_cells": 72, + "optimum_sha256": "c585da09d5edbd554aee7d0cf616ff7c9786f60be284aca3093428f8d8d7288b", + "symbolic_trees": 1161, + "symbolic_max_factors": 7 + }, + "table": { + "max_factors": 64, + "max_scratch": 8, + "feasible_plans": 255, + "costs_sha256": "c93a3d2f551849718f35aa521bcd4d1089c035c58298e16486347cb5c968d358", + "expanded_words_sha256": "de49fc27519b31138e758192a177981b6e96f5db499f37311b0f874912e3a1bc" + }, + "lower_bound": { + "formula": "2^(s+1)*n - 4^s", + "feasible_cells": 255, + "equality_family_scratch": [ + 2, + 6 + ], + "equality_family_plans": 36, + "equality_family_sha256": "253bee00df2b7d32d0cba06db2474cd64b8d20264dc4f14b2c0c3913f3de520e" + }, + "symbolic": { + "table_plans": 255, + "small_trees": 1161, + "equality_family_plans": 36, + "signed_identities": 2904, + "round_trips": 2904, + "coefficient_ring": "free noncommutative integer polynomials" + }, + "nonlinear": { + "map": "integer square and floor modulo 65521", + "width": 3, + "seeds": [ + 1, + 7, + 31 + ], + "round_trips": 1530, + "leaf_calls": 2182380, + "extra_unused_scratch_per_call": 1 + }, + "negative_controls": { + "deletions": 8, + "sign_flips": 8, + "live_scratch_reuse": 1, + "incorrect_inverse_order": 1, + "detected": 18, + "names_sha256": "d211dce376b687797ec072cb4949b59568a9b8aa8210a7f138dae8007d31bd20" + }, + "guards": { + "compose_rejections_without_mutation": 24, + "query_argument_rejections": 18, + "plan_rejections": 3, + "word_rejections": 7, + "infeasible_queries": 321, + "valid_optimal_plan_queries": 7 + }, + "main_factors": 50, + "main_calls_by_scratch_budget": { + "6": 2304, + "7": 1472, + "8": 1120 + } + }, + "rounded_execution": { + "status": "passed", + "cases": 186, + "cycle_lengths": [ + 1, + 3, + 5 + ], + "orientations": [ + -1, + 1 + ], + "initial_dirt": [ + -13, + 7 + ], + "beta": "1/2", + "multiplier_bound_r": "3", + "execution_error_formula": "N*a*(D+1)*2^-w*G^(N-1), a=13*(r+1)/beta^3, G=2+r/beta", + "plans": [ + { + "factors": 1, + "scratch_budget": 0, + "scratch_used": 0, + "leaf_calls": 1, + "factor_multiplicities": [ + 1 + ], + "working_bits": 131, + "phase_reads_by_cycle_length": { + "1": 4, + "3": 16, + "5": 28 + }, + "maximum_complete_error_bound": "611/680564733841876926926749214863536422912", + "maximum_observed_error_l1_le_2_pow": -129 + }, + { + "factors": 1, + "scratch_budget": 1, + "scratch_used": 0, + "leaf_calls": 1, + "factor_multiplicities": [ + 1 + ], + "working_bits": 131, + "phase_reads_by_cycle_length": { + "1": 4, + "3": 16, + "5": 28 + }, + "maximum_complete_error_bound": "611/680564733841876926926749214863536422912", + "maximum_observed_error_l1_le_2_pow": -129 + }, + { + "factors": 1, + "scratch_budget": 2, + "scratch_used": 0, + "leaf_calls": 1, + "factor_multiplicities": [ + 1 + ], + "working_bits": 131, + "phase_reads_by_cycle_length": { + "1": 4, + "3": 16, + "5": 28 + }, + "maximum_complete_error_bound": "611/680564733841876926926749214863536422912", + "maximum_observed_error_l1_le_2_pow": -129 + }, + { + "factors": 1, + "scratch_budget": 3, + "scratch_used": 0, + "leaf_calls": 1, + "factor_multiplicities": [ + 1 + ], + "working_bits": 131, + "phase_reads_by_cycle_length": { + "1": 4, + "3": 16, + "5": 28 + }, + "maximum_complete_error_bound": "611/680564733841876926926749214863536422912", + "maximum_observed_error_l1_le_2_pow": -129 + }, + { + "factors": 1, + "scratch_budget": 4, + "scratch_used": 0, + "leaf_calls": 1, + "factor_multiplicities": [ + 1 + ], + "working_bits": 131, + "phase_reads_by_cycle_length": { + "1": 4, + "3": 16, + "5": 28 + }, + "maximum_complete_error_bound": "611/680564733841876926926749214863536422912", + "maximum_observed_error_l1_le_2_pow": -129 + }, + { + "factors": 1, + "scratch_budget": 5, + "scratch_used": 0, + "leaf_calls": 1, + "factor_multiplicities": [ + 1 + ], + "working_bits": 131, + "phase_reads_by_cycle_length": { + "1": 4, + "3": 16, + "5": 28 + }, + "maximum_complete_error_bound": "611/680564733841876926926749214863536422912", + "maximum_observed_error_l1_le_2_pow": -129 + }, + { + "factors": 2, + "scratch_budget": 1, + "scratch_used": 1, + "leaf_calls": 4, + "factor_multiplicities": [ + 2, + 2 + ], + "working_bits": 140, + "phase_reads_by_cycle_length": { + "1": 14, + "3": 58, + "5": 102 + }, + "maximum_complete_error_bound": "611/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -139 + }, + { + "factors": 2, + "scratch_budget": 2, + "scratch_used": 1, + "leaf_calls": 4, + "factor_multiplicities": [ + 2, + 2 + ], + "working_bits": 140, + "phase_reads_by_cycle_length": { + "1": 14, + "3": 58, + "5": 102 + }, + "maximum_complete_error_bound": "611/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -139 + }, + { + "factors": 2, + "scratch_budget": 3, + "scratch_used": 1, + "leaf_calls": 4, + "factor_multiplicities": [ + 2, + 2 + ], + "working_bits": 140, + "phase_reads_by_cycle_length": { + "1": 14, + "3": 58, + "5": 102 + }, + "maximum_complete_error_bound": "611/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -139 + }, + { + "factors": 2, + "scratch_budget": 4, + "scratch_used": 1, + "leaf_calls": 4, + "factor_multiplicities": [ + 2, + 2 + ], + "working_bits": 140, + "phase_reads_by_cycle_length": { + "1": 14, + "3": 58, + "5": 102 + }, + "maximum_complete_error_bound": "611/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -139 + }, + { + "factors": 2, + "scratch_budget": 5, + "scratch_used": 1, + "leaf_calls": 4, + "factor_multiplicities": [ + 2, + 2 + ], + "working_bits": 140, + "phase_reads_by_cycle_length": { + "1": 14, + "3": 58, + "5": 102 + }, + "maximum_complete_error_bound": "611/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -139 + }, + { + "factors": 3, + "scratch_budget": 2, + "scratch_used": 2, + "leaf_calls": 8, + "factor_multiplicities": [ + 2, + 4, + 2 + ], + "working_bits": 152, + "phase_reads_by_cycle_length": { + "1": 28, + "3": 116, + "5": 204 + }, + "maximum_complete_error_bound": "611/85070591730234615865843651857942052864", + "maximum_observed_error_l1_le_2_pow": -150 + }, + { + "factors": 3, + "scratch_budget": 3, + "scratch_used": 2, + "leaf_calls": 8, + "factor_multiplicities": [ + 2, + 4, + 2 + ], + "working_bits": 152, + "phase_reads_by_cycle_length": { + "1": 28, + "3": 116, + "5": 204 + }, + "maximum_complete_error_bound": "611/85070591730234615865843651857942052864", + "maximum_observed_error_l1_le_2_pow": -150 + }, + { + "factors": 3, + "scratch_budget": 4, + "scratch_used": 2, + "leaf_calls": 8, + "factor_multiplicities": [ + 2, + 4, + 2 + ], + "working_bits": 152, + "phase_reads_by_cycle_length": { + "1": 28, + "3": 116, + "5": 204 + }, + "maximum_complete_error_bound": "611/85070591730234615865843651857942052864", + "maximum_observed_error_l1_le_2_pow": -150 + }, + { + "factors": 3, + "scratch_budget": 5, + "scratch_used": 2, + "leaf_calls": 8, + "factor_multiplicities": [ + 2, + 4, + 2 + ], + "working_bits": 152, + "phase_reads_by_cycle_length": { + "1": 28, + "3": 116, + "5": 204 + }, + "maximum_complete_error_bound": "611/85070591730234615865843651857942052864", + "maximum_observed_error_l1_le_2_pow": -150 + }, + { + "factors": 4, + "scratch_budget": 2, + "scratch_used": 2, + "leaf_calls": 16, + "factor_multiplicities": [ + 4, + 4, + 4, + 4 + ], + "working_bits": 176, + "phase_reads_by_cycle_length": { + "1": 56, + "3": 232, + "5": 408 + }, + "maximum_complete_error_bound": "611/42535295865117307932921825928971026432", + "maximum_observed_error_l1_le_2_pow": -175 + }, + { + "factors": 4, + "scratch_budget": 3, + "scratch_used": 3, + "leaf_calls": 12, + "factor_multiplicities": [ + 2, + 4, + 4, + 2 + ], + "working_bits": 164, + "phase_reads_by_cycle_length": { + "1": 42, + "3": 174, + "5": 306 + }, + "maximum_complete_error_bound": "1911/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -163 + }, + { + "factors": 4, + "scratch_budget": 4, + "scratch_used": 3, + "leaf_calls": 12, + "factor_multiplicities": [ + 2, + 4, + 4, + 2 + ], + "working_bits": 164, + "phase_reads_by_cycle_length": { + "1": 42, + "3": 174, + "5": 306 + }, + "maximum_complete_error_bound": "1911/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -163 + }, + { + "factors": 4, + "scratch_budget": 5, + "scratch_used": 3, + "leaf_calls": 12, + "factor_multiplicities": [ + 2, + 4, + 4, + 2 + ], + "working_bits": 164, + "phase_reads_by_cycle_length": { + "1": 42, + "3": 174, + "5": 306 + }, + "maximum_complete_error_bound": "1911/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -163 + }, + { + "factors": 5, + "scratch_budget": 3, + "scratch_used": 3, + "leaf_calls": 20, + "factor_multiplicities": [ + 4, + 4, + 4, + 4, + 4 + ], + "working_bits": 188, + "phase_reads_by_cycle_length": { + "1": 72, + "3": 296, + "5": 520 + }, + "maximum_complete_error_bound": "3185/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -186 + }, + { + "factors": 5, + "scratch_budget": 4, + "scratch_used": 4, + "leaf_calls": 16, + "factor_multiplicities": [ + 2, + 4, + 4, + 4, + 2 + ], + "working_bits": 176, + "phase_reads_by_cycle_length": { + "1": 56, + "3": 232, + "5": 408 + }, + "maximum_complete_error_bound": "169/10633823966279326983230456482242756608", + "maximum_observed_error_l1_le_2_pow": -174 + }, + { + "factors": 5, + "scratch_budget": 5, + "scratch_used": 4, + "leaf_calls": 16, + "factor_multiplicities": [ + 2, + 4, + 4, + 4, + 2 + ], + "working_bits": 176, + "phase_reads_by_cycle_length": { + "1": 56, + "3": 232, + "5": 408 + }, + "maximum_complete_error_bound": "169/10633823966279326983230456482242756608", + "maximum_observed_error_l1_le_2_pow": -174 + }, + { + "factors": 6, + "scratch_budget": 3, + "scratch_used": 3, + "leaf_calls": 32, + "factor_multiplicities": [ + 4, + 8, + 4, + 4, + 8, + 4 + ], + "working_bits": 224, + "phase_reads_by_cycle_length": { + "1": 112, + "3": 464, + "5": 816 + }, + "maximum_complete_error_bound": "637/21267647932558653966460912964485513216", + "maximum_observed_error_l1_le_2_pow": -223 + }, + { + "factors": 6, + "scratch_budget": 4, + "scratch_used": 4, + "leaf_calls": 24, + "factor_multiplicities": [ + 4, + 4, + 4, + 4, + 4, + 4 + ], + "working_bits": 200, + "phase_reads_by_cycle_length": { + "1": 84, + "3": 348, + "5": 612 + }, + "maximum_complete_error_bound": "507/21267647932558653966460912964485513216", + "maximum_observed_error_l1_le_2_pow": -199 + }, + { + "factors": 6, + "scratch_budget": 5, + "scratch_used": 5, + "leaf_calls": 20, + "factor_multiplicities": [ + 2, + 4, + 4, + 4, + 4, + 2 + ], + "working_bits": 188, + "phase_reads_by_cycle_length": { + "1": 70, + "3": 290, + "5": 510 + }, + "maximum_complete_error_bound": "3575/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -187 + }, + { + "factors": 7, + "scratch_budget": 3, + "scratch_used": 3, + "leaf_calls": 48, + "factor_multiplicities": [ + 4, + 8, + 4, + 8, + 8, + 8, + 8 + ], + "working_bits": 272, + "phase_reads_by_cycle_length": { + "1": 168, + "3": 696, + "5": 1224 + }, + "maximum_complete_error_bound": "1911/42535295865117307932921825928971026432", + "maximum_observed_error_l1_le_2_pow": -270 + }, + { + "factors": 7, + "scratch_budget": 4, + "scratch_used": 4, + "leaf_calls": 36, + "factor_multiplicities": [ + 4, + 8, + 4, + 4, + 4, + 8, + 4 + ], + "working_bits": 236, + "phase_reads_by_cycle_length": { + "1": 124, + "3": 516, + "5": 908 + }, + "maximum_complete_error_bound": "1521/42535295865117307932921825928971026432", + "maximum_observed_error_l1_le_2_pow": -234 + }, + { + "factors": 7, + "scratch_budget": 5, + "scratch_used": 5, + "leaf_calls": 28, + "factor_multiplicities": [ + 4, + 4, + 4, + 4, + 4, + 4, + 4 + ], + "working_bits": 212, + "phase_reads_by_cycle_length": { + "1": 100, + "3": 412, + "5": 724 + }, + "maximum_complete_error_bound": "5005/170141183460469231731687303715884105728", + "maximum_observed_error_l1_le_2_pow": -209 + }, + { + "factors": 8, + "scratch_budget": 3, + "scratch_used": 3, + "leaf_calls": 64, + "factor_multiplicities": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "working_bits": 320, + "phase_reads_by_cycle_length": { + "1": 224, + "3": 928, + "5": 1632 + }, + "maximum_complete_error_bound": "637/10633823966279326983230456482242756608", + "maximum_observed_error_l1_le_2_pow": -319 + }, + { + "factors": 8, + "scratch_budget": 4, + "scratch_used": 4, + "leaf_calls": 48, + "factor_multiplicities": [ + 4, + 8, + 8, + 4, + 4, + 8, + 8, + 4 + ], + "working_bits": 272, + "phase_reads_by_cycle_length": { + "1": 168, + "3": 696, + "5": 1224 + }, + "maximum_complete_error_bound": "507/10633823966279326983230456482242756608", + "maximum_observed_error_l1_le_2_pow": -271 + }, + { + "factors": 8, + "scratch_budget": 5, + "scratch_used": 5, + "leaf_calls": 40, + "factor_multiplicities": [ + 4, + 8, + 4, + 4, + 4, + 4, + 8, + 4 + ], + "working_bits": 248, + "phase_reads_by_cycle_length": { + "1": 140, + "3": 580, + "5": 1020 + }, + "maximum_complete_error_bound": "3575/85070591730234615865843651857942052864", + "maximum_observed_error_l1_le_2_pow": -247 + } + ], + "controls": [ + { + "name": "readonly_phase_alias_source", + "rejected": "read-only array aliases mutable data", + "leaf_calls": 0, + "arrays_unchanged": true + }, + { + "name": "readonly_phase_alias_target", + "rejected": "read-only array aliases mutable data", + "leaf_calls": 0, + "arrays_unchanged": true + }, + { + "name": "readonly_phase_alias_scratch", + "rejected": "read-only array aliases mutable data", + "leaf_calls": 0, + "arrays_unchanged": true + }, + { + "name": "underprecision", + "rejected": "closure precision" + }, + { + "name": "late_unstable_coefficient", + "rejected": "stable coefficients", + "prior_completed_leaf_calls": 1 + } + ], + "scope": "Finite generic stable factors, mixed inner/outer for n>=2; r bounds multipliers only. The complete rounded word is compared with PR628's independently assembled dense operator. Preparation, phase generation/storage, routing, and arithmetic workspace remain inherited costs; no kernel preparation or multiplication theorem is certified. Only outer alias rejection is checked before mutation; a later leaf failure has no rollback guarantee." + }, + "scope": "Exact grammar-specific cost certificate and finite implementation evidence. The all-size lower-bound and attainment statements use the written induction. No new kappa, common-label supplier, practical runtime or full multiplication proof." +} diff --git a/research/dirty-echo-space-budget/LICENSE b/research/dirty-echo-space-budget/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/dirty-echo-space-budget/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/dirty-echo-space-budget/NOTICE.md b/research/dirty-echo-space-budget/NOTICE.md new file mode 100644 index 0000000000..6cf2873a38 --- /dev/null +++ b/research/dirty-echo-space-budget/NOTICE.md @@ -0,0 +1,35 @@ +# Attribution and scope + +Prepared by Alexander Schwartzman (@AlexS-scale), with substantial OpenAI +Codex assistance in research, implementation, proof development and separate +verification. No independent human peer review is claimed. + +New files are licensed under Apache-2.0, as is this repository. The copied +license is in LICENSE. Vendored sources retain their original bytes and notices; +SOURCES.json identifies their exact commits and SHA-256 hashes. + +- Chafik Boukhalfa (@chafreaky), PR628: rounded stable cyclic-inverse leaves, + the binary dirty commutator, and the inherited restoration/error interface. + Its notice also credits Ali Romman's PR621 and its mathematical sources. +- @androolloyd, PR673: the multiway dirty echo, its nonlinear restoration + argument, fixed-fanout recurrence, error analysis and phase-alias guard. +- Dillon Amburgey (@dillona), PR689: the optimal balanced ternary placement + used as a stronger comparator. Its original notice preserves further + predecessor credit, including @0xkilgore's PR663 binary audit. +- Sagar Thakrar (@thakrarsagar), concurrent PR730: unbalanced ordered + binary/ternary optimization, including unequal prices. +- Ali Romman (@aliromman), concurrent PR744: independent strict-ternary + fixed-space census and rounded-leaf evidence. +- @Koroffstrogov, concurrent PR758: all-arity weighted optimization and a + phase-price application. Its exact planner is compared at uniform prices; + its notice is retained. No priority for shared optimization is claimed. +- Hao Yan (@FanPUYen), PR714: the concurrently reviewed clean-root checkpoint + scope, consulted to avoid duplicating a different storage contract. +- Douglas R. Colkitt (@Mister-Meeseeks), PR665: the separate spectral-split + boundary-cost investigation, consulted during task selection. + +The selected result's Kothe/Boukhalfa/eumemic supplier lineage is unchanged. +This contribution adds an analytic scratch-dependent lower bound with an +attaining family and scoped independent evidence for the ordered echo-tree +grammar. It claims neither the invention of dirty echoes nor priority over +the broader reversible-pebbling literature. diff --git a/research/dirty-echo-space-budget/PROOF.md b/research/dirty-echo-space-budget/PROOF.md new file mode 100644 index 0000000000..3a7c2f4c84 --- /dev/null +++ b/research/dirty-echo-space-budget/PROOF.md @@ -0,0 +1,227 @@ +# Ordered dirty-echo trees: cost, capacity and an exact minimum + +## 1. Model and retained local identity + +A leaf is a source-restoring additive shear. For arbitrary source `x`, target +`y` and fixed external data, it adds a deterministic function `f(x)` to `y`, +independently of `y`'s initial contents. Its negative call subtracts the same +value. The ideal factors are linear maps `A_0,...,A_(n-1)` on equal-length +arrays over an abelian group with linear structure; their required product is +`A_(n-1) ... A_0`. They need not commute. + +An internal node has `k >= 2` consecutive, nonempty factor blocks. It reserves +`k-1` distinct dirty arrays `z_1,...,z_(k-1)` throughout the node. A disjoint +deeper pool is reused sequentially by the children. Ancestor sources, targets +and reserved arrays cannot enter that pool. Each child uses one fixed tree +every time it is called, including when its exact inverse is requested. + +Let `C` be the ladder of the first `k-1` child shears, from source `x` through +the reserved arrays; let `D` omit the first link of `C`. PR673's word is + +```text +C; y += A_last(z_last); C^-1; +D; y -= A_last(z_last); D^-1. +``` + +Inverses reverse the complete instruction order and negate signs recursively. +The first and last child run twice; every interior child runs four times. +All reserved and deeper arrays are restored. For ideal linear children the +two target inputs differ by the product of the preceding child maps on `x`, +so the target increment is the required ordered product. + +The restoration argument also holds for nonlinear rounded leaves. Inverse +ladder calls see the same sources and restored deeper dirt as their forward +mates, and the intervening target update does not change any of those arrays. +Thus each node's net increment is a deterministic function of its source and +initial scratch, independent of its target. Induction preserves this interface. +Only the ideal linear increment is independent of all initial dirt. + +This identity and its nonlinear restoration argument are inherited from PR673. +Concurrent PR758 supplies the all-arity optimization principle, including +unequal prices. The distinct result here is the scratch-dependent bound and +attaining family in Section 3; an independent uniform-cost optimizer supplies +finite evidence for the same tree model. + +## 2. Exact optimality recurrence + +For a tree `T`, let `n(T)`, `N(T)` and `S(T)` count factors, completed leaf +calls and simultaneously borrowed arrays. A leaf has `(1,1,0)`. At an internal +node, with weights `w_1=w_k=2` and all interior `w_i=4`, + +```text +n(T) = sum_i n(T_i) +N(T) = sum_i w_i N(T_i) +S(T) = k-1 + max_i S(T_i). +``` + +Every restoration child is included. Storage takes a maximum because children +execute sequentially and return their deeper pool exactly; the `k-1` parent +arrays remain reserved during each call. + +Let `F(n,s)` minimize `N(T)` over this grammar with `n(T)=n` and `S(T)<=s`. +Write `infinity` when no such tree exists. Then + +```text +F(1,s) = 1 (s >= 0) +F(n,0) = infinity (n > 1) +F(n,s) = min over k=2,...,min(n,s+1) and n_1+...+n_k=n, n_i>=1: + 2 F(n_1,s-k+1) + 4 sum_(1 1) +``` + +Any allowed tree appears in this minimum at its root. Replacing each child +by an optimum for the same interval and remaining budget can only reduce +cost and cannot violate storage or factor order. Conversely, concatenating +any minimizing children in the echo realizes that candidate. Induction on +the budget proves equality, including infeasible states. + +`plan_table` evaluates this recurrence by min-plus convolution of child costs. +After each position it retains a minimum-cost prefix for each factor total. +All future costs depend only on that total and the common remaining budget, +so discarded prefixes cannot yield a cheaper completion. Ties retain the first +encountered plan; lower-budget plans are considered first. This deterministic +tie rule is not a uniqueness claim. + +This optimizes uniform leaf calls. For different per-factor costs the interval +itself, not only its length, would become part of the state. That weighted +optimization is outside this result. + +## 3. Capacity and a matching analytic lower bound + +**Capacity.** A tree fitting `s` arrays has at most `2^s` factors. At a `k`-ary +root its children have budget `r=s-k+1`, so induction gives at most +`k*2^r <= 2^s`, since `k <= 2^(k-1)`. Balanced binary trees attain every +positive factor count up to `2^s`. Hence feasibility is exactly `n <= 2^s`. + +**Lower bound.** Every tree fitting budget `s` satisfies + +```text +N(T) >= 2^(s+1) n(T) - 4^s. (1) +``` + +For a leaf the difference between the two sides is `(2^s-1)^2 >= 0`. +At a `k`-ary root put `r=s-k+1`, `p=2^r`, `t=2^(k-1)` and +`C=sum_i w_i=4k-4`. The child induction hypothesis gives + +```text +N(T) >= 2p sum_i w_i n_i - C p^2. +``` + +Subtract the desired right-hand side, `2pt sum_i n_i - t^2 p^2`. +Because `n_i<=p` by capacity and `t>=w_i`, the difference is at least + +```text +p^2 (t^2 - 2kt + C) + = p^2 (t-2)(t-2k+2) >= 0, +``` + +using `2^(k-1)>=2k-2` for `k>=2`. This proves (1) for every allowed tree, +independently of the finite dynamic-programming replay. The bound may be +negative and uninformative outside the regime below. + +**Attainment.** Let `s>=2` and `q=2^(s-2)`. For every integer +`3q <= n <= 4q`, put `b=n-3q`. Take a full binary top tree of depth `s-2` +whose `q` bottom blocks are `b` four-factor binary trees and `q-b` flat +three-factor echoes. These bottom blocks use two arrays each and cost 16 +or 8 calls. Each appears `q` times under the binary top tree. Thus + +```text +S = s, +N = q [16b + 8(q-b)] = 2^(s+1)n - 4^s. +``` + +Together with (1), this proves the exact formula throughout +`3*2^(s-2) <= n <= 2^s`. This sufficient equality interval is not claimed +maximal. For `n=50,s=6`, fourteen three-factor and two four-factor blocks +give `N=128*50-4096=2304`. The pinned balanced binary count is 2752; +the savings are achieved without an extra array or any clean data assumption. + +The other reported minima, `F(50,7)=1472` and `F(50,8)=1120`, come from the +exact recurrence and emitted witnesses. They are not instances of (1)'s +attainment formula. + +## 4. Complete local cost and approximation recurrence + +Let `m_j` be the number of executed occurrences of factor `j`. It is the +product of the endpoint/interior weights along that leaf's path, and +`sum_j m_j=N`. The verifier checks these counts against the emitted word. +For a completed leaf let `L_j` charge its arithmetic, source access, +coefficient/phase access, validation and all source restoration. Let `R_j` +charge any additional routing needed for that leaf. The total bill is + +```text +T_total = P_plan(n,s) + P_coefficients_and_phases(n,L,w) + Admission(L,s) + + sum_j m_j (L_j(L,w) + R_j(L,w)) + O((s+1)N). +``` + +The abstract recursive executor has node cost `sum_i w_i T_i + O(k)`. +The reference Python generator additionally forwards each yielded leaf through +up to `s` ancestor generator frames, so `O((s+1)N)` charges its dispatch, +including all inverse calls. +There are no implicit copies or clean length-`L` arrays. Live data consists +of source, target and `S(T)` dirty arrays. The reference retains the selected +tree, factor descriptors and `O(s)` active schedule records. Retaining the +tree and computing it are charged preprocessing, not free advice. + +The table performs `O(s^3 n^2)` min-plus comparisons, with at most `O(s)` +references copied at each successful update: `O(s^4 n^2)` elementary work +is a conservative bound for this implementation. Stored plan nodes use +`O(s^2 n)` references; integer sizes and arithmetic must also be paid in a +bit model. Precomputation may be shared only when the same schedule is reused. +Every tree has `S(T)<=n-1`, justifying the optimizer's cap on surplus budget. + +The pinned PR628 leaf makes three computational passes plus its stability +and grid-validation scans. Inner and outer factors can have different +phase-access costs, so a minimum of `N` need not minimize their weighted +sum. The rounded checks instrument actual phase reads and per-factor calls; +the certificate does not treat dispatch count as free volume-weighted work. +The radix normalization, when present, is paid in a leaf multiplier. +No frame conversion is performed at this array interface. Conversion to a +physical supplier, common-label/tape layout and arbitrary-stride routing are +additional obligations, not free consequences of a valid echo. + +For approximation, inherit PR628/PR673's completed-leaf hypotheses. Each ideal +factor has norm at most `K=r/beta`; the rounded leaf error on a source of norm +at most `B` is at most `a(B+1)u`, where + +```text +a = 13(r+1)/beta^3, u=2^-w, G=2+K, +a*u <= 1, u <= beta^2/2. +``` + +If `D` bounds all initial source, target and dirty-array norms, the actual +maximum array norm `M_j` after `j` completed leaves satisfies +`M_j+1 <= G^j(D+1)`. Let `E_j` be the maximum error against the ideal word +after the same `j` leaves. Comparing the full rounded word +with the full ideal word, including all restoration leaves, gives + +```text +E_(j+1) <= (1+K) E_j + a*u*G^j(D+1), +E_N <= N*a*(D+1)*u*G^(N-1). +``` + +Therefore execution error is at most `2^(-p-1)` when + +```text +w >= p+1+ceil(log2(N*a*(D+1))) + (N-1)*ceil(log2 G), +``` + +in addition to the two leaf precision conditions. Source and scratch +restoration remain exact. Initial dirt may affect the rounded target +increment within this bound. The same coefficient/phase preparation theorem +must separately supply at most `2^(-p-1)` operator error scaled for the +original source norm; it is not proved anew or removed here. + +Transient integer magnitudes also require bits. The completed-array bound +above contributes `ceil(log2(D+1))+N*ceil(log2 G)` bits; the inherited causal +and closure scalar estimates add `O(log(r/beta))`. With fractional precision +`w`, charge arithmetic at the resulting total width `W` and +`O(L(S(T)+2)W)` mutable data bits, in addition to the plan, descriptors and +the pinned leaf's `O(1)` clean scalar words and the chosen fast-arithmetic +implementation's workspace. No bit-reversible arithmetic compiler is supplied. + +This is a complete local array-level recurrence. It is not a complete +integer-multiplication recurrence. The fixed-budget optimization does not +alter the selected bit or complex supplier or any binding assembly constraint. +No improved multiplication exponent, globally optimal reversible program, +practical runtime speedup or fully formalized theorem follows from it. diff --git a/research/dirty-echo-space-budget/README.md b/research/dirty-echo-space-budget/README.md new file mode 100644 index 0000000000..647a027bf5 --- /dev/null +++ b/research/dirty-echo-space-budget/README.md @@ -0,0 +1,117 @@ +# A sharp scratch-dependent call bound for dirty echo trees + +**Recursive-interface theorem and independent verification; no new κ.** +For an ordered dirty-echo tree with `n` factors and at most `s` borrowed arrays, +the complete call count satisfies `N >= 2^(s+1)n - 4^s`. An explicit family +attains equality for every `s>=2` and `3*2^(s-2) <= n <= 2^s`. Thus 50 factors +and six arbitrary dirty arrays have exact minimum **2,304 calls**, compared +with 2,752 for the pinned balanced binary schedule. This is an analytic proof +of that minimum, independent of a finite optimizer's output. + +Every forward, inverse, source-restoration and dirty-restoration call is paid. +No clean array is required. The minimum concerns the stated static echo-tree +model, not arbitrary reversible programs. + +The trees use androolloyd's [PR673](https://github.com/CrocSwap/integer-mult-bounds/pull/673) +echo at each node, allowing all positive contiguous partitions and mixed +fanouts while preserving factor order. Concurrent +[PR758](https://github.com/CrocSwap/integer-mult-bounds/pull/758) independently +supplies an optimizer for the same class, including unequal prices. This +package credits that work and adds the general scratch-dependent bound, +attaining family, a complete uniform-cost table and independent exact evidence. +It claims no priority for all-arity or unbalanced tree optimization. + +| Factors | Dirty-array budget | PR673/PR689 reference | Independently checked minimum | +|---:|---:|---:|---:| +| 50 | 6 | 2,752, PR673 binary | 2,304 | +| 50 | 7 | 1,568, PR689 ternary | 1,472 | +| 50 | 8 | 1,568, PR689 ternary | 1,120 | + +The reference column takes the minimum over every feasible fixed fanout in +PR673 and PR689's refined ternary word. All three minima also match the actual +pinned PR758 optimizer; the larger-budget rows are finite recurrence results, +not instances of the displayed closed formula. These are complete operation counts, +not runtime benchmarks. The six-array improvement is 448 calls. The seed-selected +50-factor instance is a generic ordered product, not a prime-power kernel +certificate at radix 51. + +## Reproduce + +From the repository root, with Python 3.11+ and its standard library: + +```sh +python3 -I -O -B research/dirty-echo-space-budget/verify.py +``` + +Expected final line: `PASS_DIRTY_ECHO_SPACE_BUDGET: n=50, arrays=6, leaves=2752->2304`. +The verifier authenticates every vendored source, recomputes the complete +[EXPECTED.json](EXPECTED.json), and checks exact schedules, small exhaustive +tree enumeration, symbolic identities, rounded execution and negative controls. +All new checks remain active under `-O`. It needs neither Git nor network access. +`--write /absolute/new/result.json` writes the recomputed evidence to a new file. + +[PROOF.md](PROOF.md) states the grammar, optimality recurrence, general lower +bound, equality construction and complete execution bill. The finite search +domain is all `1 <= n <= 64`, `0 <= s <= 8`; infeasible cells are explicit. +The written induction proves the general statements, rather than extrapolating +from this finite domain. [CLAIM.json](CLAIM.json) records the OS-random seed 50, +three candidate tasks, overlap inspection and stopping rule. + +## Scope and source pins + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. + +| Source | Exact head | Role | +|---|---|---| +| PR628, Chafik Boukhalfa | `0768f97d06c623b8211e651543c66135796b62bf` | Restored-input rounded leaves and inherited error assumptions | +| PR673, androolloyd | `156f259b99723468cfdd2b5d47d0ba894f09bea7` | Multiway echo identity, dirty restoration and fixed-fanout baseline | +| PR689, Dillon Amburgey | `0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a` | Refined balanced ternary baseline | +| PR758, Koroffstrogov | `a164f06263e438ead570b169e5b7103aa45bf228` | Concurrent all-arity optimizer, independently compared at unit prices | + +The exact consumed files and SHA-256 digests are in [SOURCES.json](SOURCES.json). +Their original notices are retained under `vendor/`. No pending PR needs to +merge before this standalone package can run. + +At the base, the selected conditional result is +`51110230636731/31250000000000000 = 0.001635527380375392`, from #626/#543. +The selected certificate and maintainer review hashes are recorded in SOURCES.json. +This package supplies no replacement bit or complex supplier, owner allocation, +common-label realization, tape layout or complete multiplication recurrence. +The selected construction's uniform, hosting, normalized-residual, precision, +tape and analytic assumptions remain. No new κ or full formal proof is claimed. + +Optimality concerns **uniform leaf-call count in static ordered echo trees**. +It does not cover arbitrary reversible programs, interleaved scratch lifetimes, +factor reordering, clean checkpoints, unequal leaf costs, phase-read minima, +actual rounding error or execution time. Nonlinear rounded increments can +depend on the initial dirt even though restoration is exact. + +The generic callback interface requires fixed external inputs and ordinary, +distinct mutable lists. Declare read-only arrays through `readonly=` so direct +identity aliases are rejected before execution. Overlapping views, hidden +mutable callback state and transactional rollback after a malformed leaf are +outside this interface. The rounded adapter checks the pinned leaf's own +stability, grid and precision conditions. + +## Relationship to concurrent work + +PR689 already proves the minimum among recursively balanced ternary placements; +Sagar Thakrar's PR730 then admits unbalanced mixed binary/ternary trees and +unequal prices. Ali Romman's PR744 independently audits a strict ternary class +over a larger finite domain. Koroffstrogov's PR758 covers all arities and includes +weighted phase costs. These arrived during this run and are credited explicitly. +The distinct theorem here is the scratch-dependent bound and attaining family; +the optimizer is an independent implementation of the shared all-arity model. +PR714's clean root checkpoint changes the initial storage contract. PR665's +spectral encoder concerns a different boundary mechanism. + +The complete cost bill does not admit this array-level primitive into the +selected multiplication assembly. In particular, PR673's unfavorable bill for +its separate full-transform adapter is not invalidated by cheaper tree schedules. +The local result needs no claim that a stronger multiplication bound exists. + +Prepared by **Alexander Schwartzman (@AlexS-scale)** with substantial **OpenAI +Codex assistance**, including separate mathematical and implementation checks. +No independent human peer review is claimed. See [NOTICE.md](NOTICE.md) for +predecessor attribution and license scope, and [VALIDATION.md](VALIDATION.md) +for the executed checks and their limits. diff --git a/research/dirty-echo-space-budget/SOURCES.json b/research/dirty-echo-space-budget/SOURCES.json new file mode 100644 index 0000000000..c0e396727c --- /dev/null +++ b/research/dirty-echo-space-budget/SOURCES.json @@ -0,0 +1,106 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "files": [ + { + "local_path": "vendor/pr628/dirty.py", + "source_path": "research/prime-power-cyclic-scan/dirty.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "sha256": "09e7f41141594e6540828330d27be27c083ee6569660ae42c0cd519b09fc8d21" + }, + { + "local_path": "vendor/pr628/weighted.py", + "source_path": "research/prime-power-cyclic-scan/weighted.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "sha256": "8b0f93d131a30e64eb0ccd893779daffea79c0c00f1d2a30a91d23eb2bf0bff5" + }, + { + "local_path": "vendor/pr628/check.py", + "source_path": "research/prime-power-cyclic-scan/check.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "sha256": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d" + }, + { + "local_path": "vendor/pr628/scan.py", + "source_path": "research/prime-power-cyclic-scan/scan.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "sha256": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e" + }, + { + "local_path": "vendor/pr628/interval_kernel.py", + "source_path": "research/prime-power-cyclic-scan/interval_kernel.py", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe" + }, + { + "local_path": "vendor/pr628/DIRTY-PROOF.md", + "source_path": "research/prime-power-cyclic-scan/DIRTY-PROOF.md", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "sha256": "bb7c2fdc1c4673d56531fd56fb8790c81a16813ac152c10f1afabc9efdd70d61" + }, + { + "local_path": "vendor/pr628/NOTICE.md", + "source_path": "research/prime-power-cyclic-scan/NOTICE.md", + "source_pr": 628, + "source_commit": "0768f97d06c623b8211e651543c66135796b62bf", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68" + }, + { + "local_path": "vendor/pr673/echo.py", + "source_path": "research/cyclic-dirty-commutator-audit/echo.py", + "source_pr": 673, + "source_commit": "156f259b99723468cfdd2b5d47d0ba894f09bea7", + "sha256": "63d44c48801f51720a7cc994d6b5e2e857d1aa4fae4c6b83c0cca032b3d9e13b" + }, + { + "local_path": "vendor/pr673/ECHO-PROOF.md", + "source_path": "research/cyclic-dirty-commutator-audit/ECHO-PROOF.md", + "source_pr": 673, + "source_commit": "156f259b99723468cfdd2b5d47d0ba894f09bea7", + "sha256": "e98e459720d8013618853bb4836558cf8bb06a4a1be03fe0954a76f178ecf403" + }, + { + "local_path": "vendor/pr689/ternary.py", + "source_path": "research/ternary-dirty-composition/ternary.py", + "source_pr": 689, + "source_commit": "0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a", + "sha256": "aea6122da02900da3362f888f9237362a1ec6800345d5205d3ef79e6fa4a731c" + }, + { + "local_path": "vendor/pr689/NOTICE.md", + "source_path": "research/ternary-dirty-composition/NOTICE.md", + "source_pr": 689, + "source_commit": "0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a", + "sha256": "65f7f2fd6b5628820d81d9218655901fcc95a133c7267e3d8fe64c5a3147cff5" + }, + { + "local_path": "vendor/pr758/planner.py", + "source_path": "research/space-capped-dirty-echo/planner.py", + "source_pr": 758, + "source_commit": "a164f06263e438ead570b169e5b7103aa45bf228", + "sha256": "73ed7f7746cc37925db9add3b1a77fda736bd17e9fc191a283a5b40d4b781266" + }, + { + "local_path": "vendor/pr758/NOTICE.md", + "source_path": "research/space-capped-dirty-echo/NOTICE.md", + "source_pr": 758, + "source_commit": "a164f06263e438ead570b169e5b7103aa45bf228", + "sha256": "05eab27da2dc66bb0ab24df317ed45224edd6bff3b4100343e4cd8ccafa99ddd" + } + ], + "selected_context": { + "kappa": "51110230636731/31250000000000000", + "decimal": "0.001635527380375392", + "certificate": "research/community-k492-audit/pr626/replay/ASSEMBLY.json", + "certificate_sha256": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "review": "docs/research/community-k492-review.md", + "review_sha256": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47" + }, + "scope": "Vendored executable and proof inputs are byte-exact at their individual source commits. No pending PR must merge before replay." +} diff --git a/research/dirty-echo-space-budget/VALIDATION.md b/research/dirty-echo-space-budget/VALIDATION.md new file mode 100644 index 0000000000..506a8344cc --- /dev/null +++ b/research/dirty-echo-space-budget/VALIDATION.md @@ -0,0 +1,102 @@ +# Validation receipt + +Validated locally on macOS arm64 on 2026-10-13. Base: +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. + +## Completed checks + +| Check | Result | +|---|---| +| Complete certificate replay, Python 3.14.7, ordinary isolated mode | Passed | +| Complete certificate replay, Python 3.11.15, isolated optimized mode | Passed | +| Relocated package with spaces in its path, outside any Git checkout | Passed | +| Source bytes, missing inventory entry and wrong source commit controls | All rejected | +| Wrong optimum, boolean-for-integer and float-for-integer certificate controls | All rejected | +| Existing output overwrite control | Rejected; original bytes preserved | +| All 13 vendored files compared with their exact Git blobs | Passed | +| `make selected-record-check` | Passed | +| Python syntax, local document links and patch whitespace | Passed | +| Original `upstream/`, selected record, current status and review ledger | Unchanged | + +The reproducible core command is: + +```sh +python3 -I -O -B research/dirty-echo-space-budget/verify.py +``` + +Expected: +`PASS_DIRTY_ECHO_SPACE_BUDGET: n=50, arrays=6, leaves=2752->2304`. +The complete evidence is compared as canonical JSON, preserving the distinction +between integer, boolean and floating-point fields. + +The relocation and artifact controls are separately reproducible: + +```sh +python3 -I -O -B research/dirty-echo-space-budget/test_package.py +``` + +Expected: `PASS_DIRTY_ECHO_PACKAGE: relocated replay and 7 artifact rejection controls`. + +Every certificate field matches across the supported tested runtimes. +SHA-256 of EXPECTED.json: +`917e6eb0d2fc85efc06235ee36c033d41949c2b05378f1f55d525b4f72858e40`. + +## Mathematical and implementation coverage + +- All 576 `(n,s)` cells with `1<=n<=64`, `0<=s<=8`: 255 feasible plans and + 321 explicit infeasible cells. Every feasible plan is expanded and checked. +- Independent enumeration of all 5,440 ordered trees through eight leaves, + with 72 exact optimum comparisons. All 1,161 trees through seven leaves + additionally receive symbolic word checks. +- 2,904 signed free-noncommutative identities and inverse round trips, including + all feasible table plans and 36 explicit equality-family constructions. +- 1,530 nonlinear square/floor modular round trips, covering 2,182,380 executed + leaves, with arbitrary source/target/dirt and an unused spectator array. +- 18 mathematical instruction mutants; 24 public-interface rejections before + mutation, plus argument, malformed-plan and infeasibility controls. +- 186 complete rounded compositions and their inverses across 31 plan/budget + pairs, mixed inner/outer factors, cycle lengths 1/3/5 and both orientations. + Exact rational dense references, actual factor multiplicities and phase-read + counts agree; every complete error bound is at most `2^-96`. +- Five rounded-interface controls, including declared phase aliases, + insufficient precision and a later invalid coefficient. The latter does + not promise rollback after earlier completed leaves. +- Nine comparisons against PR758's actual pinned all-arity optimizer and + emitted words, including all three 50-factor results. This checks uniform + prices and symbolic endpoints, not the full PR or its weighted claims. + +These finite checks support the implementation. The general lower bound and +equality family use the written induction in PROOF.md. They are not a formal +verification of the full multiplication theorem. Generic rounded fixtures do +not supply prime-power coefficient preparation or a physical supplier. + +## Broader repository check and environment boundary + +One `make verify` run used an isolated checkout of the exact base with this +research directory added, avoiding regeneration in the contribution checkout. +It completed `verify-community`, `verify-producers`, `verify-partial-gauge`, +`verify-three-stage-cover`, `verify-paired-cube`, `verify-recycled-bit` and +`verify-entrance-banks`. After 560.319 seconds it stopped at `gen4-bank-verify`: + +```text +ModuleNotFoundError: No module named 'sympy' +``` + +The selected frontier cold replay and later full-suite groups were not reached. +No full repository suite or supplier cold-replay pass is claimed. The new +package uses only the standard library; SymPy is an inherited repository +environment dependency. The expensive global suite was not relaunched. + +A preliminary run on Apple's Python 3.9.6 exposed the pinned PR628 verifier's +`sys.set_int_max_str_digits` dependency. The documented minimum and early CLI +guard are therefore Python 3.11. Vendored source bytes were preserved. + +The GitHub push initially rejected an optional CI workflow because the OAuth +token lacks `workflow` scope. That unsubmitted file was removed before +publication; the research package and its executable checks are unchanged. +No remote CI, Linux, Lean or independent human-review pass is claimed here. + +Separate Codex workers checked the recurrence/proof, exhaustive and symbolic +evidence, rounded execution and the final implementation. Their review caught +the reference generator's `O((s+1)N)` dispatch charge, now explicit in PROOF.md. +This is substantial AI assistance, not independent human peer review. diff --git a/research/dirty-echo-space-budget/checks.py b/research/dirty-echo-space-budget/checks.py new file mode 100644 index 0000000000..e2c7dde7bf --- /dev/null +++ b/research/dirty-echo-space-budget/checks.py @@ -0,0 +1,359 @@ +"""Independent exhaustive, algebraic, and execution checks for schedule.py.""" + +from __future__ import annotations + +from collections import Counter +from functools import cache +from hashlib import sha256 +from itertools import combinations, product +import json + +from schedule import Plan, compose, optimal_plan, plan_table, word + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def digest(value): + return sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +@cache +def trees(leaves): + if leaves == 1: + return ((),) + result = [] + for cuts_count in range(1, leaves): + for cuts in combinations(range(1, leaves), cuts_count): + boundaries = (0, *cuts, leaves) + sizes = tuple(right - left for left, right in zip(boundaries, boundaries[1:])) + result.extend(product(*(trees(size) for size in sizes))) + return tuple(result) + + +@cache +def tree_statistics(tree): + if not tree: + return 1, 1, 0 + children = [tree_statistics(child) for child in tree] + calls = 2 * (children[0][1] + children[-1][1]) + calls += 4 * sum(child[1] for child in children[1:-1]) + return sum(child[0] for child in children), calls, len(tree) - 1 + max(child[2] for child in children) + + +@cache +def as_plan(tree): + return Plan(tuple(as_plan(child) for child in tree)) + + +def as_tree(plan): + return tuple(as_tree(child) for child in plan.children) + + +def expected_multiplicities(tree): + if not tree: + return [1] + counts = [] + for position, child in enumerate(tree): + weight = 2 if position == 0 or position == len(tree) - 1 else 4 + counts.extend(weight * value for value in expected_multiplicities(child)) + return counts + + +def inspect_word(plan): + leaves, calls, scratch = tree_statistics(as_tree(plan)) + require((plan.factors, plan.calls, plan.scratch) == (leaves, calls, scratch), "incorrect plan metadata") + forward = tuple(word(plan)) + backward = tuple(word(plan, -1)) + require(len(forward) == calls, "leaf-call count disagrees with the expanded word") + require(backward == tuple((factor, src, dst, -sign) for factor, src, dst, sign in reversed(forward)), + "inverse is not the reversed, sign-negated complete word") + for command in forward: + require(len(command) == 4 and all(type(value) is int for value in command), "malformed instruction") + factor, source, target, sign = command + require(0 <= factor < leaves, "factor index out of range") + require(0 <= source < scratch + 2 and 0 <= target < scratch + 2, "array index out of range") + require(source != target and target != 0, "illegal source or target alias") + require(sign in (-1, 1), "invalid instruction sign") + counts = Counter(command[0] for command in forward) + require([counts[index] for index in range(leaves)] == expected_multiplicities(as_tree(plan)), + "per-factor restoration multiplicities disagree") + require(max(max(command[1:3]) for command in forward) - 1 == scratch, "scratch peak disagrees") + return forward, backward + + +def polynomial_initial(scratch): + # Negative letters identify independent initial dirt; nonnegative letters are ordered factors. + return [{(-index - 1,): 1} for index in range(scratch + 2)] + + +def polynomial_execute(state, commands): + for factor, source, target, sign in commands: + for monomial, coefficient in tuple(state[source].items()): + term = (*monomial, factor) + value = state[target].get(term, 0) + sign * coefficient + if value: + state[target][term] = value + else: + state[target].pop(term, None) + + +def polynomial_expected(leaves, scratch, sign=1): + expected = polynomial_initial(scratch) + expected[1][(-1, *range(leaves))] = sign + return expected + + +def check_polynomials(plan, forward, backward): + initial = polynomial_initial(plan.scratch) + for sign, commands, inverse in ((1, forward, backward), (-1, backward, forward)): + state = polynomial_initial(plan.scratch) + polynomial_execute(state, commands) + require(state == polynomial_expected(plan.factors, plan.scratch, sign), + "noncommutative product or dirt restoration failed") + polynomial_execute(state, inverse) + require(state == initial, "symbolic complete inverse failed") + + +def check_exhaustive(table): + oracle = [[None] * 9 for _ in range(9)] + counts = [] + symbolic_count = 0 + for leaves in range(1, 9): + shapes = trees(leaves) + counts.append(len(shapes)) + for tree in shapes: + actual_leaves, calls, scratch = tree_statistics(tree) + require(actual_leaves == leaves, "exhaustive tree has the wrong leaf count") + for budget in range(scratch, 9): + previous = oracle[budget][leaves] + if previous is None or calls < previous: + oracle[budget][leaves] = calls + if leaves <= 7: + plan = as_plan(tree) + check_polynomials(plan, *inspect_word(plan)) + symbolic_count += 1 + for budget in range(9): + plan = table[budget][leaves] + observed = None if plan is None else plan.calls + require(observed == oracle[budget][leaves], f"exhaustive optimum mismatch at n={leaves}, s={budget}") + require(counts == [1, 1, 3, 11, 45, 197, 903, 4279], "ordered-tree enumeration is incomplete") + return { + "max_factors": 8, + "max_scratch": 8, + "trees_by_factors": counts, + "trees": sum(counts), + "optimum_cells": 72, + "optimum_sha256": digest(oracle), + "symbolic_trees": symbolic_count, + "symbolic_max_factors": 7, + } + + +def nonlinear_leaf(phase, call_count): + modulus = 65521 + + def leaf(source, target, factor, sign): + call_count[0] += 1 + for index in range(len(source)): + value = source[index] ** 2 + phase[factor] * source[(index + 1) % len(source)] + index + rounded = value // (2 + factor % 7) + target[index] = (target[index] + sign * rounded) % modulus + + return leaf + + +def check_nonlinear(plan): + calls = 0 + for seed in (1, 7, 31): + phase = [(factor + 3) * (seed + 11) for factor in range(plan.factors)] + for sign in (1, -1): + arrays = [[((index + 1) * 101 + component * 37 + seed * 13) % 65521 + for component in range(3)] for index in range(plan.scratch + 3)] + before = [array[:] for array in arrays] + phase_before = phase[:] + count = [0] + leaf = nonlinear_leaf(phase, count) + compose(plan, arrays[0], arrays[1], arrays[2:], leaf, sign=sign, readonly=(phase,)) + require(arrays[0] == before[0] and arrays[2:] == before[2:], + "nonlinear call failed to restore source, dirt, or unused extra scratch") + require(phase == phase_before, "nonlinear call changed a read-only input") + require(count[0] == plan.calls, "compose did not execute the full restoration bill") + compose(plan, arrays[0], arrays[1], arrays[2:], leaf, sign=-sign, readonly=(phase,)) + require(arrays == before and phase == phase_before, "nonlinear complete inverse failed") + require(count[0] == 2 * plan.calls, "inverse leaf-call count disagrees") + calls += count[0] + return calls + + +def check_mutations(): + plan = Plan((Plan(), Plan(), Plan())) + forward, _ = inspect_word(plan) + expected = polynomial_expected(plan.factors, plan.scratch) + mutants = [] + for index, command in enumerate(forward): + mutants.append((f"delete_{index}", forward[:index] + forward[index + 1:], expected)) + factor, source, target, sign = command + changed = (*forward[:index], (factor, source, target, -sign), *forward[index + 1:]) + mutants.append((f"flip_sign_{index}", changed, expected)) + reused = tuple((factor, 2 if source == 3 else source, 2 if target == 3 else target, sign) + for factor, source, target, sign in forward) + mutants.append(("reuse_live_scratch", reused, expected)) + binary_forward = tuple(word(Plan((Plan(), Plan())))) + wrong_inverse = tuple((factor, source, target, -sign) + for factor, source, target, sign in binary_forward) + mutants.append(("inverse_without_reversing", binary_forward + wrong_inverse, + polynomial_initial(plan.scratch))) + for name, commands, desired in mutants: + state = polynomial_initial(plan.scratch) + polynomial_execute(state, commands) + require(state != desired, f"negative control escaped detection: {name}") + return {"deletions": len(forward), "sign_flips": len(forward), "live_scratch_reuse": 1, + "incorrect_inverse_order": 1, "detected": len(mutants), + "names_sha256": digest([name for name, _, _ in mutants])} + + +def check_lower_bound(table): + checked = 0 + for budget, row in enumerate(table): + for factors, plan in enumerate(row[1:], 1): + if plan is not None: + require(plan.calls >= 2 ** (budget + 1) * factors - 4 ** budget, + "plan violates the universal call lower bound") + checked += 1 + equality_cases = [] + for budget in range(2, 7): + blocks = 2 ** (budget - 2) + for factors in range(3 * blocks, 4 * blocks + 1): + four_blocks = factors - 3 * blocks + forest = [(((), ()), ((), ()))] * four_blocks + forest.extend([((), (), ())] * (blocks - four_blocks)) + while len(forest) > 1: + forest = [(forest[index], forest[index + 1]) for index in range(0, len(forest), 2)] + tree = forest[0] + expected = 2 ** (budget + 1) * factors - 4 ** budget + require(tree_statistics(tree) == (factors, expected, budget), "equality-family construction failed") + plan = as_plan(tree) + check_polynomials(plan, *inspect_word(plan)) + require(table[budget][factors].calls == expected, "DP misses a proved sharp lower bound") + equality_cases.append([budget, factors, expected]) + return {"formula": "2^(s+1)*n - 4^s", "feasible_cells": checked, + "equality_family_scratch": [2, 6], "equality_family_plans": len(equality_cases), + "equality_family_sha256": digest(equality_cases)} + + +def must_reject(call, label): + try: + call() + except ValueError: + return + raise RuntimeError(f"invalid input was accepted: {label}") + + +def check_guards(table): + probe = Plan((Plan(), Plan(), Plan())) + patches = [ + ("source_target_alias", lambda args: args.update(target=args["source"])), + ("source_scratch_alias", lambda args: args["scratch"].__setitem__(0, args["source"])), + ("target_scratch_alias", lambda args: args["scratch"].__setitem__(0, args["target"])), + ("scratch_alias", lambda args: args["scratch"].__setitem__(1, args["scratch"][0])), + ("extra_scratch_alias", lambda args: args["scratch"].append(args["source"])), + ("readonly_source_alias", lambda args: args.update(readonly=(args["source"],))), + ("readonly_target_alias", lambda args: args.update(readonly=(args["target"],))), + ("readonly_scratch_alias", lambda args: args.update(readonly=(args["scratch"][0],))), + ("readonly_extra_alias", lambda args: args["scratch"].append(args["readonly"][0])), + ("insufficient_scratch", lambda args: args["scratch"].pop()), + ("tuple_source", lambda args: args.update(source=tuple(args["source"]))), + ("tuple_scratch", lambda args: args["scratch"].__setitem__(0, tuple(args["scratch"][0]))), + ("empty_source", lambda args: args["source"].clear()), + ("target_length", lambda args: args["target"].pop()), + ("scratch_length", lambda args: args["scratch"][0].pop()), + ("extra_scratch_length", lambda args: args["scratch"].append([1])), + ("invalid_plan", lambda args: args.update(plan=None)), + ("noncallable_leaf", lambda args: args.update(leaf=None)), + ] + patches.extend((f"sign_{repr(sign)}", lambda args, sign=sign: args.update(sign=sign)) + for sign in (0, 2, -2, True, 1.0, "1")) + for name, patch in patches: + count = [0] + phase = [41, 43, 47] + args = {"plan": probe, "source": [2, 3, 5], "target": [7, 11, 13], + "scratch": [[17, 19, 23], [29, 31, 37]], "leaf": nonlinear_leaf(phase, count), + "sign": 1, "readonly": (phase,)} + patch(args) + arrays = [args["source"], args["target"], *args["scratch"], *args["readonly"], phase] + snapshots = [(array, array[:]) for array in arrays if isinstance(array, list)] + must_reject(lambda: compose(**args), name) + require(count[0] == 0 and all(array == before for array, before in snapshots), + f"API rejection mutated caller data: {name}") + + invalid_queries = [(0, 0), (-1, 0), (True, 1), (1.0, 1), ("1", 1), + (1, -1), (1, True), (1, 1.0), (1, "1")] + for factors, budget in invalid_queries: + must_reject(lambda: optimal_plan(factors, budget), "optimal_plan argument") + must_reject(lambda: plan_table(factors, budget), "plan_table argument") + for children in ([], (Plan(),), (None, None)): + must_reject(lambda: Plan(children), "plan children") + for sign in (0, 2, -2, True, 1.0, "1"): + must_reject(lambda: tuple(word(probe, sign)), "word sign") + must_reject(lambda: tuple(word(None)), "word plan") + infeasible = 0 + for budget, row in enumerate(table): + for factors in range(1, len(row)): + if row[factors] is None: + must_reject(lambda: optimal_plan(factors, budget), "infeasible budget") + infeasible += 1 + for factors, budget in ((1, 0), (2, 1), (3, 2), (50, 6), (50, 7), (50, 8), (64, 6)): + plan = optimal_plan(factors, budget) + require(plan.calls == table[budget][factors].calls and plan.scratch <= budget, + "optimal_plan disagrees with the certificate table") + return {"compose_rejections_without_mutation": len(patches), "query_argument_rejections": 2 * len(invalid_queries), + "plan_rejections": 3, "word_rejections": 7, "infeasible_queries": infeasible, + "valid_optimal_plan_queries": 7} + + +def run_checks(): + table = plan_table(64, 8) + require(len(table) == 9 and all(len(row) == 65 for row in table), "incorrect table dimensions") + exhaustive = check_exhaustive(table) + words = sha256() + checked = 0 + nonlinear_calls = 0 + for budget, row in enumerate(table): + for factors in range(1, 65): + plan = row[factors] + require((plan is not None) == (factors <= 2 ** budget), "incorrect feasible domain") + if plan is None: + continue + require(plan.factors == factors and plan.scratch <= budget, "plan exceeds its requested budget") + forward, backward = inspect_word(plan) + check_polynomials(plan, forward, backward) + nonlinear_calls += check_nonlinear(plan) + words.update(json.dumps([budget, factors, forward], separators=(",", ":")).encode()) + checked += 1 + require(checked == 255, "incorrect feasible plan count") + lower_bound = check_lower_bound(table) + symbolic_plans = checked + exhaustive["symbolic_trees"] + lower_bound["equality_family_plans"] + costs = [[None if plan is None else plan.calls for plan in row[1:]] for row in table] + main_costs = {str(budget): table[budget][50].calls for budget in (6, 7, 8)} + require(main_costs == {"6": 2304, "7": 1472, "8": 1120}, "main instance disagrees with independent recurrence") + return { + "exhaustive": exhaustive, + "table": {"max_factors": 64, "max_scratch": 8, "feasible_plans": checked, + "costs_sha256": digest(costs), "expanded_words_sha256": words.hexdigest()}, + "lower_bound": lower_bound, + "symbolic": {"table_plans": checked, "small_trees": exhaustive["symbolic_trees"], + "equality_family_plans": lower_bound["equality_family_plans"], + "signed_identities": 2 * symbolic_plans, + "round_trips": 2 * symbolic_plans, + "coefficient_ring": "free noncommutative integer polynomials"}, + "nonlinear": {"map": "integer square and floor modulo 65521", "width": 3, + "seeds": [1, 7, 31], "round_trips": 6 * checked, "leaf_calls": nonlinear_calls, + "extra_unused_scratch_per_call": 1}, + "negative_controls": check_mutations(), + "guards": check_guards(table), + "main_factors": 50, + "main_calls_by_scratch_budget": main_costs, + } diff --git a/research/dirty-echo-space-budget/rounded_check.py b/research/dirty-echo-space-budget/rounded_check.py new file mode 100644 index 0000000000..3402dcb5a7 --- /dev/null +++ b/research/dirty-echo-space-budget/rounded_check.py @@ -0,0 +1,237 @@ +"""Finite rounded-leaf checks for the space-bounded echo scheduler. + +The leaf and independently assembled dense operator are pinned PR628 code. +These generic factors do not certify kernel preparation or a multiplication bound. +""" + +from fractions import Fraction as F +import importlib.util +import json +from pathlib import Path + +from schedule import compose, optimal_plan + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def inherited_leaf(): + path = Path(__file__).resolve().parent / "vendor" / "pr628" / "dirty.py" + spec = importlib.util.spec_from_file_location("space_budget_pr628_dirty", path) + need(spec is not None and spec.loader is not None, "missing pinned rounded leaf") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +class PhaseTable: + """Immutable phase entries with counted indexed reads.""" + + def __init__(self, values): + self.values = tuple(values) + self.reads = 0 + + def __len__(self): + return len(self.values) + + def __getitem__(self, index): + self.reads += 1 + return self.values[index] + + +def factor_multiplicities(plan, weight=1): + if not plan.children: + return [weight] + return [ + count + for i, child in enumerate(plan.children) + for count in factor_multiplicities( + child, weight * (2 if i in (0, len(plan.children) - 1) else 4) + ) + ] + + +def factors_for(count): + coefficients = ( + (F(1, 4), F(1, 8)), + (F(-1, 8), F(1, 4)), + (F(3, 16), F(-1, 16)), + (F(-1, 4), F(-1, 8)), + ) + return [ + (i % 2 == 0, coefficients[i % len(coefficients)], F(3 if i == 0 else 1)) + for i in range(count) + ] + + +def ceiling_log2(value): + if value == 0: + return None + need(value > 0, "positive error required") + exponent = value.numerator.bit_length() - value.denominator.bit_length() + power = F(2) ** exponent + return exponent + int(value > power) + + +def rejected(name, action): + try: + action() + except ValueError as error: + return {"name": name, "rejected": str(error)} + raise ValueError("negative control accepted: " + name) + + +def negative_controls(dirty): + c = dirty.c + controls = [] + plan = optimal_plan(3, 2) + for alias in ("source", "target", "scratch"): + source = [c.ONE, (F(1, 2), F(1, 4))] + target = [(F(7), F(1)), c.ONE] + scratch = [[(F(j + 2), F(i + 1)) for i in range(2)] for j in range(plan.scratch)] + arrays = [source, target, *scratch] + before = [array[:] for array in arrays] + phases = {"source": source, "target": target, "scratch": scratch[0]}[alias] + calls = [] + + def forbidden_leaf(src, dst, factor, sign): + calls.append(factor) + raise ValueError("leaf ran before alias rejection") + + control = rejected( + "readonly_phase_alias_" + alias, + lambda: compose(plan, source, target, scratch, forbidden_leaf, readonly=(phases,)), + ) + need(not calls and arrays == before, "phase alias was not rejected before mutation") + controls.append({**control, "leaf_calls": 0, "arrays_unchanged": True}) + + phases = PhaseTable((c.ONE, (F(3, 5), F(4, 5)))) + source = [c.ONE, (F(1, 2), F(1, 4))] + target = [(F(7), F(1)), c.ONE] + controls.append(rejected( + "underprecision", + lambda: dirty.leaf(source, target, factors_for(1)[0], phases, F(1, 2), 2, 1, 1, None), + )) + + factors = factors_for(3) + factors[1] = (False, c.ONE, F(1)) + scratch = [[(F(j + 2), F(i + 1)) for i in range(2)] for j in range(plan.scratch)] + stats = {"leaves": 0, "scalar_steps": 0} + + def late_invalid_leaf(src, dst, factor, sign): + dirty.leaf(src, dst, factors[factor], phases, F(1, 2), 128, 1, sign, stats) + + control = rejected( + "late_unstable_coefficient", + lambda: compose(plan, source, target, scratch, late_invalid_leaf, readonly=(phases,)), + ) + need(stats["leaves"] > 0, "late coefficient control did not reach a prior valid leaf") + controls.append({**control, "prior_completed_leaf_calls": stats["leaves"]}) + return controls + + +def run_rounded_checks(): + dirty = inherited_leaf() + c = dirty.c + units = (c.ONE, (F(0), F(1)), (F(3, 5), F(4, 5)), (F(-5, 13), F(12, 13))) + beta, r = F(1, 2), F(3) + a, growth = 13 * (r + 1) / beta**3, 2 + r / beta + records = [] + cases = 0 + for count in range(1, 9): + factors = factors_for(count) + need(all(c.norm2(b) <= (1 - beta)**2 and abs(scale) <= r + for _, b, scale in factors), "invalid stable factor fixture") + for budget in range((count - 1).bit_length(), 6): + plan = optimal_plan(count, budget) + multiplicities = factor_multiplicities(plan) + need(sum(multiplicities) == plan.calls, "plan call count disagrees with multiplicities") + bits = 128 + 3 * plan.calls + unit_roundoff = F(1, 1 << bits) + need(a * unit_roundoff <= 1 and unit_roundoff <= beta**2 / 2, "uniform precision") + maximum_bound = F(0) + maximum_error_l1 = F(0) + reads_by_length = {} + for length in (1, 3, 5): + phase_values = tuple(units[(i + count) % len(units)] for i in range(length)) + need(all(c.norm2(value) == 1 for value in phase_values), "nonunit fixture phase") + for direction in (-1, 1): + dirt = -13 if direction == -1 else 7 + source = [(F(2 * i - 3, 8), F(5 - i, 16)) for i in range(length)] + target = [(F(dirt + i, 4), F(dirt - i, 8)) for i in range(length)] + scratch = [ + [(F(dirt + 2 * i + j, 4), F(dirt - 3 * i - j, 8)) for i in range(length)] + for j in range(plan.scratch) + ] + source_before, target_before = source[:], target[:] + scratch_before = [array[:] for array in scratch] + initial_norm = max(abs(re) + abs(im) for array in [source, target, *scratch] + for re, im in array) + bound = plan.calls * a * (initial_norm + 1) * unit_roundoff * growth**(plan.calls - 1) + need(bound <= F(1, 1 << 96), "complete execution bound exceeds test tolerance") + maximum_bound = max(maximum_bound, bound) + phases = PhaseTable(phase_values) + stats = {"leaves": 0, "scalar_steps": 0} + observed = [0] * count + + def leaf(src, dst, factor, sign): + observed[factor] += 1 + dirty.leaf(src, dst, factors[factor], phases, beta, bits, direction, sign, stats) + + compose(plan, source, target, scratch, leaf, readonly=(phases,)) + need(source == source_before and scratch == scratch_before, "rounded dirty restoration") + need(phases.values == phase_values, "phase values changed") + need(stats["leaves"] == plan.calls and observed == multiplicities, "rounded leaf counts") + expected_reads = sum( + calls * ((6 if inside else 5) * length - 2) + for calls, (inside, _, _) in zip(multiplicities, factors) + ) + need(phases.reads == expected_reads, "rounded phase read count") + reads_by_length[str(length)] = expected_reads + expected = dirty.exact_operator(source_before, factors, phase_values, direction) + for actual, initial, exact in zip(target, target_before, expected): + error = c.sub(c.sub(actual, initial), exact) + need(c.norm2(error) <= bound**2, "complete rounded target differs from dense operator") + maximum_error_l1 = max(maximum_error_l1, abs(error[0]) + abs(error[1])) + compose(plan, source, target, scratch, leaf, sign=-1, readonly=(phases,)) + need(source == source_before and target == target_before and scratch == scratch_before, + "rounded complete word inverse") + need(phases.values == phase_values and phases.reads == 2 * expected_reads, "inverse phase reads") + need(stats["leaves"] == 2 * plan.calls and observed == [2 * n for n in multiplicities], + "inverse leaf counts") + need(stats["scalar_steps"] == 6 * length * plan.calls, "inherited three-pass counter") + cases += 1 + records.append({ + "factors": count, + "scratch_budget": budget, + "scratch_used": plan.scratch, + "leaf_calls": plan.calls, + "factor_multiplicities": multiplicities, + "working_bits": bits, + "phase_reads_by_cycle_length": reads_by_length, + "maximum_complete_error_bound": str(maximum_bound), + "maximum_observed_error_l1_le_2_pow": ceiling_log2(maximum_error_l1), + }) + return { + "status": "passed", + "cases": cases, + "cycle_lengths": [1, 3, 5], + "orientations": [-1, 1], + "initial_dirt": [-13, 7], + "beta": str(beta), + "multiplier_bound_r": str(r), + "execution_error_formula": "N*a*(D+1)*2^-w*G^(N-1), a=13*(r+1)/beta^3, G=2+r/beta", + "plans": records, + "controls": negative_controls(dirty), + "scope": "Finite generic stable factors, mixed inner/outer for n>=2; r bounds multipliers only. " + "The complete rounded word is compared with PR628's independently assembled dense operator. " + "Preparation, phase generation/storage, routing, and arithmetic workspace remain inherited costs; " + "no kernel preparation or multiplication theorem is certified. " + "Only outer alias rejection is checked before mutation; a later leaf failure has no rollback guarantee.", + } + + +if __name__ == "__main__": + print(json.dumps(run_rounded_checks(), indent=2)) diff --git a/research/dirty-echo-space-budget/schedule.py b/research/dirty-echo-space-budget/schedule.py new file mode 100644 index 0000000000..4d50996c5a --- /dev/null +++ b/research/dirty-echo-space-budget/schedule.py @@ -0,0 +1,150 @@ +"""Minimum uniform leaf-call counts in the ordered dirty-echo tree grammar.""" + +from __future__ import annotations + +from dataclasses import dataclass, field + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Plan: + children: tuple[Plan, ...] = () + factors: int = field(init=False) + calls: int = field(init=False) + scratch: int = field(init=False) + + def __post_init__(self): + need(isinstance(self.children, tuple), "children must be a tuple") + need(not self.children or len(self.children) >= 2, "internal nodes need two or more children") + need(all(isinstance(child, Plan) for child in self.children), "invalid child plan") + if self.children: + factors = sum(child.factors for child in self.children) + calls = sum( + (2 if i in (0, len(self.children) - 1) else 4) * child.calls + for i, child in enumerate(self.children) + ) + scratch = len(self.children) - 1 + max(child.scratch for child in self.children) + else: + factors, calls, scratch = 1, 1, 0 + object.__setattr__(self, "factors", factors) + object.__setattr__(self, "calls", calls) + object.__setattr__(self, "scratch", scratch) + + +def plan_table(max_factors, max_scratch): + """Return table[budget][factor_count]; None means no tree fits the budget. + + All positive contiguous partitions and all arities allowed by the budget + are considered. Min-plus convolution avoids enumerating their products. + """ + need(type(max_factors) is int and max_factors >= 1, "positive integer factor count required") + need(type(max_scratch) is int and max_scratch >= 0, "nonnegative integer scratch budget required") + table = [] + for budget in range(max_scratch + 1): + row = table[-1][:] if table else [None] * (max_factors + 1) + row[1] = Plan() + for arity in range(2, min(max_factors, budget + 1) + 1): + child_row = table[budget - arity + 1] + prefixes = [None] * (max_factors + 1) + prefixes[0] = (0, ()) + for position in range(arity): + weight = 2 if position in (0, arity - 1) else 4 + remaining = arity - position - 1 + extended = [None] * (max_factors + 1) + for used, prefix in enumerate(prefixes): + if prefix is None: + continue + for size in range(1, max_factors - remaining - used + 1): + child = child_row[size] + if child is None: + continue + cost = prefix[0] + weight * child.calls + total = used + size + if extended[total] is None or cost < extended[total][0]: + extended[total] = (cost, (*prefix[1], child)) + prefixes = extended + for count, candidate in enumerate(prefixes): + if candidate is not None and (row[count] is None or candidate[0] < row[count].calls): + row[count] = Plan(candidate[1]) + table.append(row) + return table + + +def optimal_plan(factors, scratch_budget): + """Minimize uniform leaf calls under the given simultaneous array budget.""" + need(type(factors) is int and factors >= 1, "positive integer factor count required") + need(type(scratch_budget) is int and scratch_budget >= 0, "nonnegative integer scratch budget required") + need((factors - 1).bit_length() <= scratch_budget, "no echo tree fits the scratch budget") + return plan_table(factors, min(scratch_budget, factors - 1))[-1][factors] + + +def word(plan, sign=1): + """Yield (factor, source, target, sign), with source 0 and target 1. + + Array indices 2 onward are arbitrary caller-supplied dirt. An inverse call + reverses the full word, including the instruction order within children. + """ + need(isinstance(plan, Plan), "invalid plan") + need(type(sign) is int and sign in (-1, 1), "sign must be +1 or -1") + + def inverse(commands): + return [(child, first, src, dst, -direction) for child, first, src, dst, direction in reversed(commands)] + + def emit(node, first, source, target, scratch_first, direction): + if not node.children: + yield first, source, target, direction + return + chain = [] + offset = first + for i, child in enumerate(node.children[:-1]): + src = source if i == 0 else scratch_first + i - 1 + chain.append((child, offset, src, scratch_first + i, 1)) + offset += child.factors + last = (node.children[-1], offset, scratch_first + len(chain) - 1, target, 1) + # Both dirty ladders and their inverses are required by PR673's echo. + commands = chain + [last] + inverse(chain) + chain[1:] + inverse([last]) + inverse(chain[1:]) + if direction == -1: + commands = inverse(commands) + for child, start, src, dst, child_sign in commands: + yield from emit(child, start, src, dst, scratch_first + len(chain), child_sign) + + yield from emit(plan, 0, 0, 1, 2, sign) + + +def compose(plan, source, target, scratch, leaf, sign=1, readonly=()): + """Execute a plan through leaf(source, target, factor_index, sign). + + Each leaf must restore its source, be independent of its target, and have + an exact subtracting inverse. Its external inputs must remain fixed. + Declared read-only arrays are checked for identity aliases before mutation. + """ + need(isinstance(plan, Plan), "invalid plan") + need(type(sign) is int and sign in (-1, 1), "sign must be +1 or -1") + need(callable(leaf), "leaf must be callable") + need(len(scratch) >= plan.scratch, "insufficient dirty arrays") + arrays = [source, target, *scratch] + need(all(isinstance(array, list) for array in arrays), "mutable arrays must be lists") + need(len({id(array) for array in arrays}) == len(arrays), "mutable arrays must be distinct") + need(not any(value is array for value in readonly for array in arrays), "read-only array aliases mutable data") + need(len(source) > 0 and all(len(array) == len(source) for array in arrays), "equal positive array lengths required") + for factor, src, dst, direction in word(plan, sign): + leaf(arrays[src], arrays[dst], factor, direction) + + +def multiplicities(plan): + """Return each factor's total calls, including restoration calls.""" + counts = [] + + def visit(node, weight): + if not node.children: + counts.append(weight) + else: + for i, child in enumerate(node.children): + visit(child, weight * (2 if i in (0, len(node.children) - 1) else 4)) + + visit(plan, 1) + return counts diff --git a/research/dirty-echo-space-budget/test_package.py b/research/dirty-echo-space-budget/test_package.py new file mode 100644 index 0000000000..4ace280e50 --- /dev/null +++ b/research/dirty-echo-space-budget/test_package.py @@ -0,0 +1,69 @@ +"""Check isolated relocation and fail-closed source/certificate handling.""" + +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def run(package, cwd, failure=None, arguments=()): + result = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(package / "verify.py"), *arguments], + cwd=cwd, capture_output=True, text=True, timeout=120, + ) + if failure is None: + if result.returncode != 0 or "PASS_DIRTY_ECHO_SPACE_BUDGET:" not in result.stdout: + raise RuntimeError("relocated replay failed: " + result.stderr) + elif result.returncode == 0 or failure not in result.stderr: + raise RuntimeError("expected rejection missing: " + str(failure) + "\n" + result.stderr) + + +def main(): + with tempfile.TemporaryDirectory(prefix="dirty-echo-space-budget-") as directory: + parent = Path(directory) + package = parent / "standalone package with spaces" + shutil.copytree(ROOT, package, ignore=shutil.ignore_patterns("__pycache__", "*.pyc")) + run(package, parent) + + source = package / "vendor" / "pr673" / "echo.py" + original_source = source.read_bytes() + source.write_bytes(original_source + b"\n") + run(package, parent, "source hash mismatch") + source.write_bytes(original_source) + + manifest = package / "SOURCES.json" + original_manifest = manifest.read_bytes() + changed = json.loads(original_manifest) + changed["files"].pop() + manifest.write_text(json.dumps(changed)) + run(package, parent, "source inventory is incomplete") + changed = json.loads(original_manifest) + changed["files"][0]["source_commit"] = "0" * 40 + manifest.write_text(json.dumps(changed)) + run(package, parent, "source provenance changed") + manifest.write_bytes(original_manifest) + + expected = package / "EXPECTED.json" + original_expected = expected.read_bytes() + changed = json.loads(original_expected) + changed["main_witnesses"][0]["minimum_calls"] -= 1 + expected.write_text(json.dumps(changed)) + run(package, parent, "recomputed certificate differs") + for invalid_count in (True, 1.0): + changed = json.loads(original_expected) + changed["costs_by_budget"][0][0] = invalid_count + expected.write_text(json.dumps(changed)) + run(package, parent, "recomputed certificate differs") + expected.write_bytes(original_expected) + run(package, parent, "FileExistsError", ("--write", str(expected))) + if expected.read_bytes() != original_expected: + raise RuntimeError("--write replaced an existing certificate") + print("PASS_DIRTY_ECHO_PACKAGE: relocated replay and 7 artifact rejection controls") + + +if __name__ == "__main__": + main() diff --git a/research/dirty-echo-space-budget/vendor/pr628/DIRTY-PROOF.md b/research/dirty-echo-space-budget/vendor/pr628/DIRTY-PROOF.md new file mode 100644 index 0000000000..caf4aafc78 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr628/DIRTY-PROOF.md @@ -0,0 +1,128 @@ +# Cyclic inverse shears with dirty array restoration + +This extends the classical rounded cyclic-inverse primitive of PR628. It removes +its need for a clean length-L intermediate array. It does not supply a common-label +Clifford realization, reversible bit arithmetic, transform layout, or the complete +integer-multiplication reduction. No new kappa follows from this lemma. + +## Contract + +Input x, target y and h borrowed arrays are complex dyadic grids of spacing u=2^-w. +Every array has length L>=1 and may initially contain arbitrary data. The arrays +are distinct. Their initial infinity norms are at most D. Read-only phases tau_i +have modulus one. Phase generation/storage and coefficient preparation are paid; +there is no free phase table. The primitive adds an approximation to Q(W)^-1 x +to y, restores x and every borrowed array exactly, and needs only a constant number +of clean scalar arithmetic registers besides loop counters and factor descriptors. +Here (Wx)_i=tau_i*x_(i-d), initially for d=+/-1 in a cyclic layout, and +Q(z)=r^-1 product_(j=1)^n(z-rho_j), n=r-1, with stable reciprocal/inner factors +of norm at most 1-beta. The final increment can depend on the initial dirt within +the stated approximation error. Exact independence of the increment from dirt is +not claimed for rounded arithmetic. + +## One factor + +First consider T x = y defined by y_i=x_i+b_i*y_(i-d), |b_i|<=1-beta. +Choose the cyclic order in direction d. Let z be the zero-boundary causal solution +and p_i the product of b from the first position through i. Let c be the complete +product. Then y_i=z_i+p_i*s, s=z_last/(1-c). The stable cyclic equation itself +implies ||y||<=B/beta when ||x||<=B, so |s|<=B/beta. + +On the dyadic grid, perform the causal pass directly in x, skipping the first +position: x_i += round(b_i*x_previous). These are integer lifts. Reversing their +order and subtracting the same rounded source products restores x exactly, +including arbitrary nonzero initial values. During the first pass also accumulate +the rounded scalar product c_hat. Compute s_hat=round(z_hat_last/(1-c_hat)). +In a second pass accumulate rounded prefix products p_hat_i and add +round(m_i*(z_hat_i+round(p_hat_i*s_hat))) to the appropriate target position. +Finally undo the causal lifts. Each target position is written exactly once; +its existing value never enters the computed increment. Scalar arithmetic and +coefficient scratch can be cleared classically; no reversible arithmetic gate +claim is made. Three passes suffice, excluding validation scans and paid +coefficient access. O(1) clean scalar words and O(log L) indexing bits suffice. + +Nearest complex rounding has norm error at most u. Assuming u<=beta^2/2, +|z_hat-z|<=u/beta, |p_hat-p|<=u/beta, |c_hat-c|<=u/beta, and +|1-c_hat|>=beta/2. Using s=z_last/(1-c), rather than separately bounding the +numerator and denominator, gives + + |s_hat-s| <= u + (2/beta)*(u/beta + (B/beta)*(u/beta)) + <= 5*(B+1)*u/beta^3. + +Also |p_hat|<=1+u/beta<=3/2. Hence the corrected output before m multiplication +has error at most 12*(B+1)*u/beta^3. If |m_i|<=r, the final rounded multiplication +has error at most a*(B+1)*u, a=13*(r+1)/beta^3. None of these constants depends +on L. + +For an outer root, b_i=rho^-1*tau_i, m_i=-rho^-1. For an inner root, scan in +direction -d with b_i=rho*conjugate(tau_(i+d)); the value at position i is +multiplied by conjugate(tau_i) and added at i-d. This is +(W-rho I)^-1=(I-rho W^-1)^-1 W^-1. The scalar r is included in one leaf's +multiplier. Each exact factor has operator norm at most K=r/beta. No permutation +of the mutable source array is required for the inner factor. + +## Product of factors + +For exact linear maps A,B and a dirty scratch array z, the sequence + + z += B*x; y += A*z; z -= B*x; y -= A*z + +adds AB*x to y and restores z. Split the factor list in halves recursively; +use one distinct borrowed array per recursion depth. A negative call executes +the exact inverse instruction word (reverse operation order and invert signs). +It is not obtained by negating signs in the original order. + +The rounded construction still restores every borrowed array and x exactly. +Inductively each call preserves its input and all deeper scratch, and its increment +is independent of its target. The paired calls computing B therefore see the same +input and deeper initial dirt. Never use an ancestor input or target as deeper +scratch: the ancestor target may have changed between the paired calls. This is +an explicit alias exclusion in the executable contract. + +There are h=ceil(log2 n) borrowed arrays and at most N=4*n^2 leaf calls. Pad to the +next power of two for this count if desired (identity leaves require no rounded +inverse). The implementation splits without padding and checks the actual count. + +For the ideal elementary shears, the joint max norm grows by at most C=1+K per +leaf. With a*u<=1 the computed trajectory satisfies + + M_j+1 <= G^j*(D+1), G=C+1. + +Comparing the complete rounded word with the ideal word on the same initial +arrays, and summing the propagated leaf errors, gives + + E_N <= N*a*(D+1)*u*G^(N-1). + +The ideal word cancels all borrowed initial data exactly. This proves the target +error bound for every length and every initial dirt bounded by D, while actual +restoration is exact without an error allowance. Choosing + + w >= p+1+ceil(log2(N*a*(D+1)))+(N-1)*ceil(log2 G) + +and enforcing a*u<=1 and u<=beta^2/2 gives execution error <=2^(-p-1). +PR628's coefficient/phase perturbation bound, budgeted to <=2^(-p-1) for the +original x, then gives total <=2^-p. That perturbation bound scales with ||x||; +for general input bound X use p+ceil(log2(max(1,X))) in its preparation budget. +The initial borrowed dirt does not enter the ideal operator perturbation bound. + +PR628 has log2(beta^-1)=O(r^3). Therefore these deliberately loose budgets need +w=O(p+log(D+1)+r^5) bits, and O(r^2) passes. Inside a leaf, the causal state and closure scalars add at most another +O(log(beta^-1)+log r) magnitude bits. Maximum transient magnitudes thus add +O(log(D+1)+r^5) integer bits, already covered by this word-size bound. Standard +fast fixed-precision arithmetic yields soft-O((L*r^2+r^3)*(p+log(D+1)+r^5)) +bit work plus charged phase-oracle and routing costs. Factor preparation and +coefficient enclosures are inherited from PR628. Borrowed storage is +O(L log r) words; clean arithmetic storage is O(w+log L) bits up to the chosen +multiplication implementation's workspace, plus O(r) read-only factor descriptors. +A machine with only a fixed number of dirty data arrays is not covered by this +contract. Arbitrary stride still incurs PR628's explicitly charged routing. + +## Executable evidence + +`dirty.py` uses exact rational arithmetic and explicit nearest dyadic rounding. +It checks generic variable-coefficient leaves, dense independently assembled +factor inverses, both orientations, nonzero targets, several initial dirty arrays, +exact source/scratch restoration, exact whole-word inversion, and the leaf count. +Finite checks support the implementation; the inequalities above are the all-L +argument. The exact-rational prototype does not itself implement the claimed +fast fixed-precision arithmetic cost. diff --git a/research/dirty-echo-space-budget/vendor/pr628/NOTICE.md b/research/dirty-echo-space-budget/vendor/pr628/NOTICE.md new file mode 100644 index 0000000000..22fbeb8ef0 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr628/NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and scope + +Ali Romman's PR621, exact head 520774462b19b29af41554b74def31f9d01e997e, +supplies the prime-power kernel circle bound. Its kernel attribution is +OpenAI's exact-DFT preprint at adc7f1241b42e322a6451854ab7e4b4c146bf78a +(`loc:newton`, `loc:fourier-factorization`) and classical q-Pochhammer/Newton +factorization, including Alexey Kuznetsov's cited q-calculus work. This +package does not claim to originate those constructions. + +Pan's approximate-factorization theorem is used in the form stated by +Mehlhorn, Sagraloff and Wang; Brent's work supplies fast elementary-function +evaluation. Causal/anticausal recursive filtering is standard, as illustrated +by the Briand-Davy source listed in SOURCE.json. Sources are cited for these +specific tools, not as proofs of this package's complete claim. + +The scan rounding analysis, explicit budget composition, interval and +factor certificates, routed reference execution, and packaging were +prepared with substantial OpenAI Codex assistance for chafreaky. The dense +matrix solver and algebraic coefficient crosschecks provide independent +computational paths, not human peer review or formal Lean verification. + +No new multiplication exponent, literature priority, maintainer acceptance, +physical tape execution, or production performance result is claimed. +The code and documents use the repository's Apache-2.0 license. diff --git a/research/dirty-echo-space-budget/vendor/pr628/check.py b/research/dirty-echo-space-budget/vendor/pr628/check.py new file mode 100644 index 0000000000..5ef6dd67b6 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr628/check.py @@ -0,0 +1,178 @@ +"""Rational proof of mixed inside/outside cyclic factor inversion.""" +from pathlib import Path +from fractions import Fraction as F +import argparse,importlib.util,json,math,sys +sys.set_int_max_str_digits(100000) +P=Path(__file__).resolve().parent +def module(name): + s=importlib.util.spec_from_file_location(name,P/(name+'.py'));m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m +c=module('scan');ik=module('interval_kernel') + +def prime_power(r): + if type(r)!=int or r<3:return False + p=next((d for d in range(2,math.isqrt(r)+1) if r%d==0),r) + while r%p==0:r//=p + return r==1 + +def certify(data): + r,k=data['radix'],data['embedding'] + c.need(prime_power(r) and type(k)==int and 00 and type(target)==int and target>0,'precision budget') + c.need(type(fb)==int and 0=F(1,2),'gauge chart') + parameters=[im/(1+re) for im in v[1] for re in v[0]] + mid=(min(parameters)+max(parameters))/2 + t=c.rounded((mid,F(0)),1024)[0] + sigma=c.mul(center,((1-t*t)/(1+t*t),2*t/(1+t*t))) + c.need(c.norm2(sigma)==1,'exact rational unit phase') + error=sum(max(abs(endpoint-coordinate) for endpoint in iv) for iv,coordinate in zip(box,sigma)) + c.need(error0) + for name in ('unit_root','missing_root','wrong_embedding','low_precision','bad_margin'): + row=json.loads(json.dumps(mixed)) + if name=='unit_root':row['roots'][0]=['1','0'] + if name=='missing_root':row['roots'].pop() + if name=='wrong_embedding':row['embedding']=row['radix'] + if name=='low_precision':row['working_bits']=8 + if name=='bad_margin':row['beta']='1' + try:certify(row) + except ValueError as error:controls.append(dict(name=name,rejected=str(error))) + else:raise ValueError('bad control accepted '+name) + state=certify(mixed);x=[c.ONE,c.ZERO,(F(1,2),F(1,4))] + bad=apply(x,state,1,omit_inner_shift=True) + try:residual_check(x,bad,state,1) + except ValueError as error:controls.append(dict(name='omitted_inner_shift',rejected=str(error))) + else:raise ValueError('inner-shift mutation accepted') + try:apply(x,state,1,(F(1),F(1))) + except ValueError as error:controls.append(dict(name='nonunit_gauge',rejected=str(error))) + else:raise ValueError('nonunit gauge accepted') + args.out.write_text(json.dumps(dict(status='passed',kernel_crosschecks=crosschecks,irrational_gauge=gauge_record,certificates=certificates,cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',certificates=len(certificates),cases=len(cases),dense_cases=sum(row['dense_comparison'] for row in cases),controls=len(controls)))) + +if __name__=='__main__':main() diff --git a/research/dirty-echo-space-budget/vendor/pr628/dirty.py b/research/dirty-echo-space-budget/vendor/pr628/dirty.py new file mode 100644 index 0000000000..2b94710837 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr628/dirty.py @@ -0,0 +1,133 @@ +"""Integer lifting for cyclic inverse shears using borrowed dirty arrays. +Exact rational prototype. Arithmetic workspace and phase access are charged in the proof; +this is not a common-label Clifford word or a bit-reversible arithmetic compiler. +""" +from pathlib import Path +from fractions import Fraction as F +import importlib.util,json,argparse,itertools +P=Path(__file__).resolve().parent +s=importlib.util.spec_from_file_location('weighted',P/'weighted.py');w=importlib.util.module_from_spec(s);s.loader.exec_module(w);c=w.c + +def scaled(z,q):return(z[0]*q,z[1]*q) +def conj(z):return(z[0],-z[1]) +def ordered(n,d):return range(n)if d==1 else range(n-1,-1,-1) + +def lift(x,y,coefficient,beta,bits,d,sign=1,destination=None,multiplier=None,stats=None): + """y += sign*F(x), restoring x exactly; no length-dependent clean data array.""" + n=len(x);c.need(x is not y and n==len(y)>0,'distinct equally sized arrays') + c.need(d in(-1,1)and sign in(-1,1),'orientation and sign') + c.need(0=(beta/2)**2,'closure denominator') + seed=c.rounded(c.div(x[previous],denominator),bits) + power=c.ONE + for i in ordered(n,d): + power=c.rounded(c.mul(coefficient(i),power),bits) + value=c.add(x[i],c.rounded(c.mul(power,seed),bits)) + value=c.rounded(c.mul(multiplier(i),value),bits) + j=destination(i);y[j]=c.add(y[j],scaled(value,sign)) + # The scalar seed and coefficient scratch may be cleared by ordinary classical + # arithmetic. The dirty data itself is restored by exact inverse integer lifts. + first=0 if d==1 else n-1 + for i in ordered(n,-d): + if i!=first:x[i]=c.sub(x[i],c.rounded(c.mul(coefficient(i),x[i-d]),bits)) + if stats is not None:stats['leaves']+=1;stats['scalar_steps']+=3*n + +def leaf(x,y,factor,phases,beta,bits,d,sign,stats): + inside,b,scale=factor;n=len(x) + if inside: + lift(x,y,lambda i:c.mul(b,conj(phases[(i+d)%n])),beta,bits,-d,sign, + lambda i:(i-d)%n,lambda i:scaled(conj(phases[i]),scale),stats) + else: + lift(x,y,lambda i:c.mul(b,phases[i]),beta,bits,d,sign, + multiplier=lambda i:scaled(c.neg(b),scale),stats=stats) + +def compose(x,y,factors,scratch,phases,beta,bits,d,sign=1,stats=None): + """Balanced commutator; negative call is the exact inverse instruction word.""" + c.need(sign in(-1,1)and d in(-1,1),'orientation and sign') + c.need(factors and len(scratch)>=(len(factors)-1).bit_length(),'dirty depth') + arrays=[x,y]+scratch;c.need(len({id(v)for v in arrays})==len(arrays),'all ancestor arrays distinct') + c.need(len(x)>0 and all(len(v)==len(x)for v in arrays)and len(phases)==len(x),'array lengths') + c.need(all(c.norm2(t)==1 for t in phases),'unit phases') + if len(factors)==1:return leaf(x,y,factors[0],phases,beta,bits,d,sign,stats) + mid=len(factors)//2;B,A=factors[:mid],factors[mid:];z=scratch[0];rest=scratch[1:] + operations=[(x,z,B,1),(z,y,A,1),(x,z,B,-1),(z,y,A,-1)] + if sign==-1:operations=[(src,dst,fs,-sgn)for src,dst,fs,sgn in reversed(operations)] + for src,dst,fs,sgn in operations:compose(src,dst,fs,rest,phases,beta,bits,d,sgn,stats) + +def exact_operator(x,factors,phases,d): + # Dense rational oracle constructed independently from the lifting recurrence. + n=len(x);out=x[:] + for inside,b,scale in factors: + a=[[c.ZERO for _ in range(n)]for _ in range(n)] + if inside: + for i in range(n):a[i][i]=c.neg(b);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + else: + rho=c.div(c.ONE,b) + for i in range(n):a[i][i]=c.neg(rho);a[i][(i-d)%n]=c.add(a[i][(i-d)%n],phases[i]) + out=[scaled(z,scale)for z in w.solve(a,out)] + return out + +def certificate(n,beta,r,D,bits): + N=4*n*n;a=13*(r+1)/beta**3;G=2+F(r)/beta;u=F(1,1<4:raise ValueError('angle bound') + itheta=(point(0),theta) + total=term=ONE + # Taylor remainder for complex exp: <=exp(4)*4^(N+1)/(N+1)! <128*... + n=0 + while True: + n+=1;term=cmul(term,itheta);term=(scale(term[0],F(1,n)),scale(term[1],F(1,n)));total=cadd(total,term) + remainder=F(128*4**(n+1),math.factorial(n+1)) + if remainder 0, 'empty cycle') + need(direction in (-1, 1), 'invalid direction') + need(0 < beta <= 1, 'invalid margin') + need(norm2(b) <= (1-beta)**2, 'uncertified stable factor') + u = F(1, 1 << bits) + need(u <= beta*beta/2, 'precision too low for closure') + order = list(range(len(x))) if direction == 1 else list(reversed(range(len(x)))) + z, power = ZERO, ONE + for i in order: + z = rounded(add(x[i], mul(b, z)), bits) + power = rounded(mul(b, power), bits) + den = sub(ONE, power) + need(norm2(den) >= (beta/2)**2, 'closure lower bound failed') + seed = rounded(div(z, den), bits) + y, previous = [ZERO]*len(x), seed + for i in order: + previous = rounded(add(x[i], mul(b, previous)), bits) + y[i] = previous + return y + +def dense_solve(x, b, direction): + """Independent exact Gaussian elimination on the cyclic matrix.""" + n = len(x) + a = [[ZERO for _ in range(n)] + [x[i]] for i in range(n)] + for i in range(n): + a[i][i] = add(a[i][i], ONE) + j = (i-direction) % n + a[i][j] = sub(a[i][j], b) + for k in range(n): + pivot = next(i for i in range(k, n) if a[i][k] != ZERO) + a[k], a[pivot] = a[pivot], a[k] + p = a[k][k] + a[k] = [div(v, p) for v in a[k]] + for i in range(n): + if i == k: continue + p = a[i][k] + a[i] = [sub(v, mul(p, w)) for v, w in zip(a[i], a[k])] + return [row[-1] for row in a] + +def residual_bound(x, y, b, beta, direction, bound): + # Neumann inverse norm <= 1/beta converts residual to forward error. + for i in range(len(x)): + residual = sub(sub(y[i], mul(b, y[(i-direction) % len(x)])), x[i]) + need(norm2(residual) <= (beta*bound)**2, 'residual error bound failed') + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + cases = [] + for beta in (F(1, 2), F(1, 16), F(1, 4096)): + for unit in (ONE, (F(-1), F(0)), (F(3, 5), F(4, 5))): + b = mul((1-beta, F(0)), unit) + for n in (1, 2, 3, 8, 17, 64): + x = [(F((i*7)%13-6, 8), F((i*11)%17-8, 16)) for i in range(n)] + B = max(abs(v[0])+abs(v[1]) for v in x) + for direction in (-1, 1): + bits = 64 + bound = 6*(B+1)*F(1, 1 << bits)/beta**3 + y = scan(x, b, beta, bits, direction) + residual_bound(x, y, b, beta, direction, bound) + if n <= 8: + exact = dense_solve(x, b, direction) + need(all(norm2(sub(v,w)) <= bound**2 for v,w in zip(y,exact)), 'dense comparison failed') + cases.append(dict(beta=str(beta), b=[str(v) for v in b], length=n, + direction=direction, bits=bits, forward_error_bound=str(bound), + dense_crosscheck=n<=8, residual_check=True)) + controls = [] + for name, x, b, beta, bits, direction in ( + ('unstable', [ONE], ONE, F(1,2), 64, 1), + ('underprecision', [ONE], (F(15,16),F(0)), F(1,16), 3, 1), + ('empty', [], ZERO, F(1,2), 64, 1), + ('bad_direction', [ONE], ZERO, F(1,2), 64, 0), + ): + try: scan(x,b,beta,bits,direction) + except ValueError as error: controls.append(dict(name=name,rejected=str(error))) + else: raise ValueError('negative control accepted: '+name) + x = [ONE, ZERO, ONE] + b, beta = (F(1,2),F(0)), F(1,2) + y = scan(x,b,beta,64,1) + y[0] = add(y[0],ONE) + try: residual_bound(x,y,b,beta,1,F(1,1<<40)) + except ValueError as error: controls.append(dict(name='corrupt_output',rejected=str(error))) + else: raise ValueError('corrupt output accepted') + args.out.write_text(json.dumps(dict(status='passed',cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',cases=len(cases),dense_cases=sum(c['dense_crosscheck'] for c in cases),controls=len(controls)))) + +if __name__ == '__main__': main() diff --git a/research/dirty-echo-space-budget/vendor/pr628/weighted.py b/research/dirty-echo-space-budget/vendor/pr628/weighted.py new file mode 100644 index 0000000000..da90ee6e83 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr628/weighted.py @@ -0,0 +1,118 @@ +"""Exact certificates for varying unit phases on a cyclic neighbor shift.""" +from pathlib import Path +from fractions import Fraction as F +import argparse, importlib.util, json +P=Path(__file__).resolve().parent +s=importlib.util.spec_from_file_location('kernel',P/'check.py');k=importlib.util.module_from_spec(s);s.loader.exec_module(k) +c=k.c + +def scan(x,bs,beta,bits,direction): + c.need(len(x)>0 and len(bs)==len(x),'coefficient length') + c.need(direction in (-1,1),'direction') + c.need(0=(beta/2)**2,'closure denominator') + previous=c.rounded(c.div(z,den),bits);y=[c.ZERO]*len(x) + for i in order: + previous=c.rounded(c.add(x[i],c.mul(bs[i],previous)),bits);y[i]=previous + return y + +def apply(x,state,phases,direction,wrong_phase=False): + n=len(x);c.need(n>0 and len(phases)==n,'phase length') + c.need(all(c.norm2(t)==1 for t in phases),'unit phases') + y=[(v[0]*state['radix'],v[1]*state['radix'])for v in x] + for inside,b in state['factors']: + if inside: + inv=[(phases[(i+direction)%n][0],-phases[(i+direction)%n][1])for i in range(n)] + if wrong_phase:inv=[(v[0],-v[1])for v in phases] + bs=[c.mul(b,t)for t in inv] + y=scan(y,bs,state['beta'],state['bits'],-direction) + y=[c.rounded(c.mul(inv[i],y[(i+direction)%n]),state['bits'])for i in range(n)] + else: + y=scan(y,[c.mul(b,t)for t in phases],state['beta'],state['bits'],direction) + y=[c.rounded(c.neg(c.mul(b,v)),state['bits'])for v in y] + return y + +def matrix(q,phases,direction): + # Independently expand W^j entry-by-entry, including wrap-around phases. + n=len(phases);a=[[c.ZERO for _ in range(n)]for _ in range(n)] + for i in range(n): + weight=c.ONE + for j,v in enumerate(q): + col=(i-direction*j)%n;a[i][col]=c.add(a[i][col],c.mul(v,weight)) + weight=c.mul(weight,phases[col]) + return a + +def residual(x,y,a,bound): + for i,row in enumerate(a): + v=c.ZERO + for z,t in zip(row,y):v=c.add(v,c.mul(z,t)) + c.need(c.norm2(c.sub(v,x[i]))<=bound**2,'expanded weighted residual') + +def solve(a,x): + a=[row[:]+[v]for row,v in zip(a,x)];n=len(a) + for j in range(n): + i=next(i for i in range(j,n)if a[i][j]!=c.ZERO);a[i],a[j]=a[j],a[i] + z=a[j][j];a[j]=[c.div(v,z)for v in a[j]] + for i in range(n): + if i!=j: + z=a[i][j];a[i]=[c.sub(v,c.mul(z,t))for v,t in zip(a[i],a[j])] + return [row[-1]for row in a] + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--out',type=Path,required=True);a=ap.parse_args() + units=[c.ONE,(F(0),F(1)),(F(3,5),F(4,5)),(F(-5,13),F(12,13))] + cases=[];certs=[];generic=[];controls=[] + for beta in (F(1,2),F(1,16),F(1,4096)): + for n in (1,2,3,8,17,64): + bs=[c.mul((1-beta,F(0)),units[(i*i+3*i+1)%4])for i in range(n)] + # Alternate magnitudes as well as phases. + bs=[(z[0]/(1+i%2),z[1]/(1+i%2))for i,z in enumerate(bs)] + x=[(F(i%5-2,4),F(i%7-3,8))for i in range(n)] + B=max(abs(z[0])+abs(z[1])for z in x);bound=6*(B+1)*F(1,1<<64)/beta**3 + for d in (-1,1): + y=scan(x,bs,beta,64,d) + m=[[c.ZERO for _ in range(n)]for _ in range(n)] + for i in range(n):m[i][i]=c.ONE;m[i][(i-d)%n]=c.sub(m[i][(i-d)%n],bs[i]) + residual(x,y,m,beta*bound) + if n<=8:c.need(all(c.norm2(c.sub(v,t))<=bound**2 for v,t in zip(y,solve(m,x))),'generic dense') + generic.append(dict(beta=str(beta),length=n,direction=d,dense=n<=8)) + sigma,nu,phase_cert=k.irrational_gauge() + for row in json.loads((P/'FACTORS.json').read_text()): + if row['radix'] not in (4,9,16):continue + st=k.certify(row);A=F(st['certificate']['inverse_norm_bound']) + eps=F(st['certificate']['coefficient_error_bound'])+sum(j*(abs(v[0])+abs(v[1]))for j,v in enumerate(st['q']))*nu + c.need(A*eps<1 and A*A*eps/(1-A*eps)+st['budgets'][-1]<=F(1,1<= 2 it uses O(n^alpha) factor calls, where +alpha = log_k(4k-4) < 2 for k > 2, with O(log n) borrowed length-L arrays. +It does not provide a common-label Clifford supplier, bit-reversible compiler, +transform layout, or new multiplication κ. The phase-alias repair is required +at this interface too and is included in `echo.py` before execution. + +## Exact algebra; no commutativity assumption + +Let A_1,...,A_k be arbitrary composable linear maps on equal-length arrays. +Source x, target y and dirty arrays z_1,...,z_(k-1) are all distinct. Define C +as the following ordered sequence of shears: + + z_1 += A_1 x + z_2 += A_2 z_1 + ... + z_(k-1) += A_(k-1) z_(k-2) + +Define D as C with its first shear omitted. Execute + + C; y += A_k z_(k-1); C^-1; + D; y -= A_k z_(k-1); D^-1. + +C^-1 and D^-1 reverse the operation order and negate every shear. They restore +all dirty arrays. The two target updates occur on dirty-chain states that differ +only by the propagated contribution of the first link. Inductively that +difference at z_i is A_i ... A_1 x. Consequently the net target increment is +A_k ... A_1 x. This proof holds for noncommuting maps and arbitrary initial dirt. +The source is never a target of an ideal shear. With k=2, D is empty and this +reduces to the original binary commutator. + +The complete count is + + (k-1) + 1 + (k-1) + (k-2) + 1 + (k-2) = 4k-4. + +It includes both ladders, both inverse ladders and both target updates. There +is no clean length-L work array or implicit copying. The two endpoint maps +are each called twice; each interior map is called four times. + +## Recursive schedule and storage + +Partition n factors into k' = min(k,n) consecutive groups, as evenly as +possible, preserving their order. Use k'-1 dirty arrays for this node. Recursively +implement each group map using a disjoint pool of deeper borrowed arrays, +which can be reused between calls because every call restores that pool. +Neither an ancestor source nor an ancestor target belongs to the deeper pool. +All mutable arrays, including surplus scratch, are checked distinct at entry. + +For group sizes n_i, the exact recurrences implemented by `resources` are + + S(1) = 0, N(1) = 1 + S(n) = k'-1 + max_i S(n_i) + N(n) = 2 N(n_1) + 2 N(n_k') + 4 sum_(10, a sufficiently large *fixed* k makes alpha<1+epsilon. +The flat choice k=n instead uses n-1 borrowed arrays and exactly 4n-4 calls. + +| Factors | Binary: arrays / calls | Fanout 8: arrays / calls | Flat: arrays / calls | +|---|---:|---:|---:| +| 8 | 3 / 64 | 7 / 28 | 7 / 28 | +| 16 | 4 / 256 | 8 / 112 | 15 / 60 | +| 64 | 6 / 4096 | 14 / 784 | 63 / 252 | +| 512 | 9 / 262144 | 21 / 21952 | 511 / 2044 | + +The generator streams instructions using O(k log_k n) active scheduling +records. It does not retain the expanded word. A positive or negative child +call takes the same resources. Negative calls reverse the full instruction +word, rather than negating signs in forward order. + +## Exact restoration despite rounded, nonlinear increments + +A valid PR628 leaf adds a deterministic function of its source to its target, +restores its source exactly, and does not read its target when computing the +increment. Its negative leaf subtracts exactly that same grid value. Fixed, +non-aliased phase and factor data are essential here. + +Inductively, a recursive call adds a deterministic function of its source and +initial deeper dirt, independently of its target, and restores the source and +all deeper dirt. Thus C's child calls can be undone in reverse order: each sees +the same source and deeper dirt as its forward mate. The intervening target +update changes only y, which is excluded from every ladder's scratch pool. +The same argument applies to D. This proves exact source and scratch restoration +at every level for valid finite-grid inputs. Reversing the complete word gives +an exact inverse. It does **not** prove that the rounded target increment is +independent of dirt; the error estimate below bounds that dependence. + +As with the pinned leaf, all input contracts must hold throughout execution. +This is not transactional rollback on arbitrary malformed coefficients or +stateful callbacks. The explicit alias checks reject ordinary list-identity +aliasing before any mutation; arbitrary overlapping views are outside the API. + +## Complete inherited error and cost budget + +Use PR628's leaf estimates with n=r-1, beta in (0,1], grid u=2^-w, and +multipliers bounded by r. The same hypotheses and preparation remain required. +Let D bound the initial joint max norm, K=r/beta, +a=13(r+1)/beta^3 and G=2+K. A rounded leaf on input norm at most B has error +at most a(B+1)u; an ideal shear has Lipschitz norm at most 1+K. Enforce +au<=1 and u<=beta^2/2. + +Writing M_j for the computed joint norm after j leaves gives +(M_j + 1) <= G^j(D+1). Comparing the complete rounded instruction word with the +complete ideal word gives, by propagation through each remaining ideal shear, + + E_N <= N a (D+1) u G^(N-1). + +This argument applies to the actual expanded word, including every restoration +operation. Substitute the new exact N; do not reuse the predecessor's 4n² +upper bound when measuring the improvement. The ideal identity proved above +cancels all initial borrowed dirt. Hence this E_N bounds target error while +actual source and scratch restoration are exact. + +For requested p bits choose + + w >= p+1+ceil(log2(N a (D+1)))+(N-1)ceil(log2 G), + +as well as the two leaf precision conditions. This budgets execution error +at most 2^(-p-1). The inherited coefficient/phase preparation error must still +be budgeted to 2^(-p-1), scaled for the original source norm as specified in +PR628. It does not receive a free exact phase table from this construction. + +Under PR628's log2(beta^-1)=O(r³), fixed fanout k gives + + N = O(r^alpha), + w = O(p + log(D+1) + r^(3+alpha)). + +Joint transient integer magnitudes add O(log(D+1)+N log G) bits; the leaf's +causal state and closure add O(log(beta^-1)+log r), all covered by that budget. +Borrowed data storage is O(L log r) words for fixed k. Clean arithmetic storage, +read-only factor descriptors, indexing and fast-arithmetic workspace retain +PR628's qualifications. Charging the same factor preparation and leaf arithmetic +as PR628 gives the conditional local work upper bound + + soft-O((L r^alpha + r³) (p + log(D+1) + r^(3+alpha))) + +plus charged phase-oracle and routing work. Every leaf still includes its +forward pass, output pass, undo pass and validation/access costs; none are +removed by a speedup claim. With k=8, alpha=log_8 28≈1.602452, replacing the +binary precision power 5 by about 4.602452. With flat k=n the corresponding +power is 4, but borrowed arrays become O(r), not O(log r). + +The Fraction prototype tests identities, rounding and restoration; its timings +are **not** evidence for a fast fixed-precision implementation. No complete +multiplication recurrence follows without integrating the required transform, +paid storage/layout, bit supplier and all conditional assembly assumptions. + +## Evidence and attribution + +`verify_echo.py` compares the streamed ideal word against direct composition of +arbitrary noncommuting 2x2 integer matrices. It separately compares rounded +execution with an integer-grid arithmetic interpreter (sharing only the tested +schedule), and with PR628's independently assembled dense cyclic inverse oracle. +The latter checks the complete error bound at a precision chosen by the formula +above, with positive, zero and negative initial dirt. These finite tests support +the implementation; they are not a formal proof of the general statement. +The algebraic and inductive arguments above state the general obligations. + +The schedule and analysis here were prepared for @androolloyd with substantial +OpenAI Codex assistance, under Apache-2.0. The rounded leaf and original binary +dirty inverse are Chafik Boukhalfa / chafreaky's PR628 work, with OpenAI Codex +assistance, built on Ali Romman's PR621 kernel and the sources retained in +SOURCE.json. This note claims an improvement relative to that pinned binary +schedule, not priority over all historical reversible-pebbling literature. diff --git a/research/dirty-echo-space-budget/vendor/pr673/echo.py b/research/dirty-echo-space-budget/vendor/pr673/echo.py new file mode 100644 index 0000000000..76a3117136 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr673/echo.py @@ -0,0 +1,75 @@ +"""Multiway dirty echo composition of PR628's restored-input leaf shears. + +Prepared for androolloyd with substantial OpenAI Codex assistance. Apache-2.0. +No new multiplication exponent is asserted. Read ECHO-PROOF.md for the storage +tradeoff and the complete inherited local error recurrence. +""" + + +def partition(count, fanout): + if count < 1 or fanout < 2: + raise ValueError('positive factor count and fanout >= 2 required') + k = min(count, fanout) + quotient, remainder = divmod(count, k) + return [quotient + (i < remainder) for i in range(k)] + + +def resources(count, fanout): + if count < 1 or fanout < 2: + raise ValueError('positive factor count and fanout >= 2 required') + if count == 1: + return 0, 1 + sizes = partition(count, fanout) + children = [resources(n, fanout) for n in sizes] + scratch = len(sizes)-1 + max(depth for depth, _ in children) + calls = sum((2 if i in (0, len(sizes)-1) else 4)*cost + for i, (_, cost) in enumerate(children)) + return scratch, calls + + +def instructions(first, count, src, dst, scratch_first, fanout, sign=1): + """Stream the exact instruction word or its reverse inverse.""" + if count == 1: + yield src, dst, first, sign + return + sizes = partition(count, fanout) + k = len(sizes) + offsets = [first] + for size in sizes[:-1]: + offsets.append(offsets[-1]+size) + # C: populate the whole dirty chain. D: the same chain without its first link. + chain = [(offsets[i], sizes[i], src if i == 0 else scratch_first+i-1, + scratch_first+i, 1) for i in range(k-1)] + last = (offsets[-1], sizes[-1], scratch_first+k-2, dst, 1) + invert = lambda commands: [(a,n,s,t,-q) for a,n,s,t,q in reversed(commands)] + commands = chain + [last] + invert(chain) + chain[1:] + invert([last]) + invert(chain[1:]) + if sign == -1: + commands = invert(commands) + for a,n,s,t,q in commands: + yield from instructions(a,n,s,t,scratch_first+k-1,fanout,q) + + +def compose(leaf_module, x, y, factors, scratch, phases, beta, bits, direction, + sign=1, fanout=8): + """Apply the dirty echo using a pinned PR628 leaf, restoring x and scratch.""" + if direction not in (-1,1) or sign not in (-1,1): + raise ValueError('orientation and sign') + depth, count = resources(len(factors), fanout) + arrays = [x,y]+scratch + if len(scratch) < depth: + raise ValueError('dirty depth') + if len({id(a) for a in arrays}) != len(arrays): + raise ValueError('all ancestor arrays distinct') + if any(phases is a for a in arrays): + raise ValueError('phase array aliases mutable data') + if not x or any(len(a) != len(x) for a in arrays) or len(phases) != len(x): + raise ValueError('array lengths') + if any(a*a+b*b != 1 for a,b in phases): + raise ValueError('unit phases') + stats = dict(leaves=0,scalar_steps=0) + for src,dst,index,q in instructions(0,len(factors),0,1,2,fanout,sign): + leaf_module.leaf(arrays[src],arrays[dst],factors[index],phases,beta,bits, + direction,q,stats) + if stats['leaves'] != count: + raise ValueError('leaf accounting') + return stats diff --git a/research/dirty-echo-space-budget/vendor/pr689/NOTICE.md b/research/dirty-echo-space-budget/vendor/pr689/NOTICE.md new file mode 100644 index 0000000000..cc0966a001 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr689/NOTICE.md @@ -0,0 +1,47 @@ +# Attribution and license + +New refinement, implementation, verification and documentation: Dillon +Amburgey, with substantial OpenAI Codex assistance. Apache-2.0, as in the +repository and the included LICENSE. No independent human review, formal +multiplication proof, practical speedup, or literature-priority claim is made. + +- androolloyd, [PR673](https://github.com/CrocSwap/integer-mult-bounds/pull/673) + at `0e35f56cab3cae1eb0a99447135569d687c5695a`: the general multiway dirty + echo, its nonlinear restoration proof, inherited precision accounting, and + `O(n^log_k(4k-4))` call bound. Its exact `echo.py` and `ECHO-PROOF.md` are + retained in `vendor/pr673`, including the source's OpenAI Codex disclosure. + This package refines balanced size placement at fanout three and supplies an + independent free-term/noncommutative audit of the actual pinned generator. + The echo identity and exponent are predecessor results. This package does + not review PR673's separate phase-alias repair or κ appendix. +- Chafik Boukhalfa / chafreaky, PR628 at + `0768f97d06c623b8211e651543c66135796b62bf`: cyclic inverse leaves, rounded + integer lifts, balanced binary dirty commutator, preparation/precision + arguments, dense reference solvers, kernel fixtures and executable sources. + The original notice is preserved at `vendor/pr628/NOTICE.md`; its credits to + Ali Romman / PR621, the exact-DFT preprint, Alexey Kuznetsov, Pan, Mehlhorn, + Sagraloff, Wang, Brent and Briand-Davy remain in force. This package does not + reprove their analytic or algorithmic results. +- 0xkilgore, PR663 at `e0e546fd01b396478c68b6b6c5a16d87515983ba`: + independent nonlinear restoration audit and the exact binary count + `3qn-2q²`. The count provides the fair baseline here; the original `4n²` + allowance is also retained in the precision comparisons. The symbolic + verifier in this package is separately implemented; PR663 supplies the + predecessor audit, not proof of the refined instruction schedule. +- Jeremy Kothe, Chafik Boukhalfa and eumemic, #622/#623/#626 and #543, and the + preceding lineage credited in the selected review: the base repository's + accepted conditional finite construction. Their multiplier bound is neither + changed nor newly verified by this package. +- Borrowed-workspace cancellation and ladder methods have substantial prior + literature. A related quantum setting is Khattar and Gidney, + [Rise of conditionally clean ancillae for efficient quantum circuit + constructions, §4](https://arxiv.org/html/2407.17966v2#S4), laddered toggle + detection. That paper is cited as related work, not as the correctness proof + or source of the exact eight-call array word retained from PR673. No quantum + implementation is asserted. + +Concurrent PR665 investigates spectral residual splitting and PR666/PR668 +verify cyclic certificates/resultants. Those are distinct scopes; none is an +executable dependency of this contribution. Existing scoped negative results +for fixed incidence graphs, grouped frames, and commuting duplicate scalar +gates do not test this change to the product-of-shears composition tree. diff --git a/research/dirty-echo-space-budget/vendor/pr689/ternary.py b/research/dirty-echo-space-budget/vendor/pr689/ternary.py new file mode 100644 index 0000000000..a8c2eb5775 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr689/ternary.py @@ -0,0 +1,101 @@ +"""A streaming three-block composition of source-restoring additive shears. + +The leaf callback must add a deterministic function of its source to its target, +restore its source, and implement its exact inverse when sign is -1. Its +increment must not depend on the target. Coefficients and read-only data must +stay fixed throughout a call. See README.md for the proof and charged scope. +""" + +from functools import lru_cache + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def split(n): + """Contiguous block sizes; extra factors go to the less-repeated ends.""" + need(type(n) is int and n >= 3, "ternary split requires at least three factors") + q, remainder = divmod(n, 3) + return q + (remainder > 0), q, q + (remainder > 1) + + +def resources(n): + """Return (executed leaf calls, simultaneously borrowed arrays).""" + need(type(n) is int and n >= 1, "positive integer factor count") + + @lru_cache(maxsize=None) + def count(size): + if size == 1: + return 1, 0 + if size == 2: + return 4, 1 + a, b, c = (count(k) for k in split(size)) + return 2 * a[0] + 4 * b[0] + 2 * c[0], 2 + max(a[1], b[1], c[1]) + + return count(n) + + +def word(n, sign=1): + """Yield (factor_index, source_array, target_array, sign) in execution order. + + Array 0 is the source, array 1 the target, and arrays 2 onward are borrowed. + Only O(log n) control frames are live; the expanded word is never stored. + Negative calls reverse the instruction order as well as the signs. + """ + need(type(n) is int and n >= 1, "positive integer factor count") + need(type(sign) is int and sign in (-1, 1), "sign must be +1 or -1") + + def emit(lo, hi, source, target, depth, direction): + size = hi - lo + if size == 1: + yield lo, source, target, direction + return + u = 2 + depth + if size == 2: + operations = [ + (lo, lo + 1, source, u, 1), + (lo + 1, hi, u, target, 1), + (lo, lo + 1, source, u, -1), + (lo + 1, hi, u, target, -1), + ] + child_depth = depth + 1 + else: + a, b, _ = split(size) + v = u + 1 + # PR673's echo at fanout 3, with longer blocks at the ends. + # Chronological order: A B C B^-1 A^-1 B C^-1 B^-1. + A = (lo, lo + a, source, u) + B = (lo + a, lo + a + b, u, v) + C = (lo + a + b, hi, v, target) + operations = [ + (*A, 1), (*B, 1), (*C, 1), (*B, -1), + (*A, -1), (*B, 1), (*C, -1), (*B, -1), + ] + child_depth = depth + 2 + if direction == -1: + operations = [(*op[:-1], -op[-1]) for op in reversed(operations)] + for left, right, src, dst, child_sign in operations: + yield from emit(left, right, src, dst, child_depth, child_sign) + + yield from emit(0, n, 0, 1, 0, sign) + + +def compose(source, target, factors, scratch, leaf, sign=1): + """Run the word using leaf(source, target, factor, sign). + + Scratch arrays are caller-supplied arbitrary data, not initialized copies. + Extra supplied arrays are admitted but untouched. Array aliasing is rejected + before the first leaf. Overlapping views and hidden mutable dependencies + are outside this contract; the reference uses ordinary lists of scalars. + """ + n = len(factors) + _, required = resources(n) + need(type(sign) is int and sign in (-1, 1), "sign must be +1 or -1") + need(len(scratch) >= required, "insufficient distinct dirty arrays") + arrays = [source, target, *scratch] + need(len({id(a) for a in arrays}) == len(arrays), "source, target and scratch must be distinct") + need(len(source) > 0 and all(len(a) == len(source) for a in arrays), "equal positive array lengths") + for factor, src, dst, direction in word(n, sign): + leaf(arrays[src], arrays[dst], factors[factor], direction) diff --git a/research/dirty-echo-space-budget/vendor/pr758/NOTICE.md b/research/dirty-echo-space-budget/vendor/pr758/NOTICE.md new file mode 100644 index 0000000000..3d19f09aaa --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr758/NOTICE.md @@ -0,0 +1,77 @@ +# Attribution and license + +New exact space-capped interval planner, literal plans, bounded experiments, +verification and written scope: **Koroffstrogov**, with substantial **OpenAI +Codex assistance**. New material is Apache-2.0, as in the included LICENSE. +No independent human peer review or priority over the general dynamic +programming/reversible-pebbling literature is claimed. + +- **androolloyd, PR673**, pinned at + `bfff94e78f0e75ebd2593e3cc7710ae5290e8be3`: the multiway echo identity, + arbitrary nonlinear source/scratch restoration, endpoint/interior execution + multiplicities, inherited error argument, generic fanout tradeoff, and later + all-role adapter cost obstruction. `vendor/pr673` retains exact source and + proof bytes with their original disclosure. This contribution optimizes + partitions/arity at a hard space cap; it does not originate the echo or its + subquadratic fixed-fanout bound and does not review the rest of that PR. +- **Dillon Amburgey / dillona, PR689**, pinned at + `0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a`: the improved balanced ternary + partition and 160-call/five-array comparison. Its `ternary.py`, README and + full NOTICE are retained byte-for-byte. Its explicit exclusion of unbalanced + partitions/other arities/unequal prices motivates the new class here. The + exact balanced predecessor word is recounted, not reconstructed from its PR + title. Our checkers and optimizer are new implementations; the earlier + symbolic-audit methodology is acknowledged. +- **Chafik Boukhalfa / chafreaky, PR628**, pinned at + `0768f97d06c623b8211e651543c66135796b62bf`: cyclic inverse leaves, exact + integer source lifts, finite root enclosures, coefficient preparation and + rounding bounds, dense rational reference routines and original binary + dispatcher. Its original notice is retained in `vendor/pr628/NOTICE.md`, + including Ali Romman / PR621, OpenAI's exact-DFT source, Kuznetsov, Pan, + Mehlhorn, Sagraloff, Wang, Brent and Briand-Davy. We use its unchanged leaf + and declared contracts; we do not reprove their analytic algorithms. Its + old public `compose` is not used, including its known phase-alias defect. +- **0xkilgore, PR663**, `e0e546fd01b396478c68b6b6c5a16d87515983ba`: + predecessor independent audit of nonlinear dirty restoration and the binary + call count. Credited context, not an executable dependency. +- **Jeremy Kothe, Chafik Boukhalfa, eumemic**, #622/#623/#626 and #543, and + their full cumulative lineage in the selected maintainer review: the base + repository's conditional accepted construction. It is unchanged and is not + newly cold-replayed here. + +Classical borrowed-workspace and cancellation methods have substantial prior +literature; PR673 and PR689 preserve their relevant Bennett/catalytic-space +and related ladder attributions. Their complete notices remain applicable. +This package makes a scoped minimum/count claim for an explicitly defined +tree family, not a new general reversible-computation theorem. + +Nearby pending #665 (spectral residual splitting), #677 (native DATA-shear +boundaries), and #679 (selector-volume batching) concern different interfaces. +None supplies executable code to this package. PR673's full-transform negative +result is explicitly retained rather than silently reopened by a lower local +leaf count. + +**FanPUYen, concurrent PR714**, inspected at +`efad8a40094ab453c0525efef0b0eff2a5d8b850`, improves the root split when one +array is genuinely clean, while retaining balanced binary dirty children. +Our entire pool is arbitrary dirty input; we change the whole tree's arities +and partitions without a clean-array premise. The interfaces and optimization +domains differ. No PR714 implementation or claimed optimum is consumed. + +**Sagar Thakrar / thakrarsagar, concurrent PR730**, at +`d222e348179cc02a54d6d26dbd2838944f62c6e5`, published an exact interval +optimizer for unbalanced contiguous binary/ternary echo trees and unequal +positive prices during this contribution's verification. It is prior published +work on that class; no priority for unbalanced/weighted optimization is claimed +here. Its byte-exact `optimize.py` and full NOTICE are retained in `vendor/pr730` +and pinned separately. The comparison runs that actual optimizer and its +literal words. The strict additional gain here comes from higher arities: +at 15 factors / five arrays, 160 becomes 152 through a four-child node. + +**Ali Romman, concurrent PR744**, at +`576c6b20065fff3402c1eed2ad74c5c7d03029e8`, independently audits the strict +ternary class with a larger finite state table, literal witnesses and rounded +leaf tests. Its code is not consumed. This package does not duplicate that +state-table claim; it supplies the higher-arity optimum and an actual pinned +radix-16 weighted fixture. Both concurrent submissions retain their independent +evidence and source credits. diff --git a/research/dirty-echo-space-budget/vendor/pr758/planner.py b/research/dirty-echo-space-budget/vendor/pr758/planner.py new file mode 100644 index 0000000000..fb315ad699 --- /dev/null +++ b/research/dirty-echo-space-budget/vendor/pr758/planner.py @@ -0,0 +1,146 @@ +"""Exact planning within sequential multiway dirty-echo trees. + +Koroffstrogov with substantial OpenAI Codex assistance. Apache-2.0. +The echo identity is PR673's; the balanced ternary comparator is PR689's. +This module optimizes contiguous partitions and arities at a fixed space cap. +It does not optimize arbitrary reversible programs. See PROOF.md. +""" + +from functools import lru_cache + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def invoice(tree, weights): + """Independently traverse a literal tree; return price, calls, peak, counts.""" + weights = tuple(weights) + need(weights and all(type(w) is int and w > 0 for w in weights), + "positive integer leaf weights") + + def walk(node): + if type(node) is int: + need(0 <= node < len(weights), "leaf index") + return [node], 0, {node: 1} + need(type(node) in (tuple, list) and len(node) >= 2, "tree arity") + leaves, peak, counts = [], 0, {} + for j, child in enumerate(node): + indices, space, occurrences = walk(child) + leaves.extend(indices) + peak = max(peak, space) + multiplier = 2 if j in (0, len(node)-1) else 4 + for i, count in occurrences.items(): + counts[i] = counts.get(i, 0) + multiplier * count + return leaves, len(node)-1+peak, counts + + leaves, space, counts = walk(tree) + need(leaves == list(range(len(weights))), "ordered complete factor list") + profile = [counts[i] for i in range(len(weights))] + return dict(price=sum(w*c for w, c in zip(weights, profile)), + calls=sum(profile), scratch=space, occurrences=profile) + + +def optimize(weights, budget): + """Return a minimum-price tree, then minimum calls among price ties. + + Leaves are ordered and cannot be deleted/reordered. Each k-child node + reserves k-1 arrays during every child call; the children share a deeper + pool sequentially. Infeasibility means only this explicit tree class. + """ + weights = tuple(weights) + need(weights and all(type(w) is int and w > 0 for w in weights), + "positive integer leaf weights") + need(type(budget) is int and budget >= 0, "nonnegative integer space cap") + budget = min(budget, len(weights)-1) + + @lru_cache(maxsize=None) + def best(lo, hi, space): + if hi-lo == 1: + return weights[lo], 1, lo + if space == 0 or hi-lo > 2**space: + return None + winner = None + for arity in range(2, min(space+1, hi-lo)+1): + remaining = space-arity+1 + # Partition DP: j complete consecutive children ending at a cut. + states = {lo: (0, 0, ())} + for j in range(arity): + next_states = {} + multiplier = 2 if j in (0, arity-1) else 4 + for cut, (cost, calls, children) in states.items(): + stop = min(hi-(arity-j-1), cut+2**remaining) + for end in range(cut+1, stop+1): + child = best(cut, end, remaining) + if child is None: + continue + candidate = (cost+multiplier*child[0], + calls+multiplier*child[1], children+(child[2],)) + old = next_states.get(end) + if old is None or candidate[:2] < old[:2]: + next_states[end] = candidate + states = next_states + candidate = states.get(hi) + if candidate is not None and (winner is None or candidate[:2] < winner[:2]): + winner = candidate + return winner + + answer = best(0, len(weights), budget) + need(answer is not None, "no tree fits space cap") + result = invoice(answer[2], weights) + need((result['price'], result['calls']) == answer[:2], "planner invoice") + need(result['scratch'] <= budget, "planner space") + return dict(tree=answer[2], **result) + + +def word(tree, sign=1): + """Stream (factor, source, target, sign), with source 0 and target 1.""" + need(type(sign) is int and sign in (-1, 1), "sign") + + def leaf_count(node): + if type(node) is int: + return 1 + need(type(node) in (tuple, list) and len(node) >= 2, "tree arity") + return sum(leaf_count(c) for c in node) + + invoice(tree, [1]*leaf_count(tree)) + + def emit(node, source, target, first_scratch, direction): + if type(node) is int: + yield node, source, target, direction + return + k = len(node) + chain = [(node[j], source if j == 0 else first_scratch+j-1, + first_scratch+j, 1) for j in range(k-1)] + last = (node[-1], first_scratch+k-2, target, 1) + + def inverse(commands): + return [(t, s, d, -q) for t, s, d, q in reversed(commands)] + + commands = chain+[last]+inverse(chain)+chain[1:]+inverse([last])+inverse(chain[1:]) + if direction == -1: + commands = inverse(commands) + for child, src, dst, child_sign in commands: + yield from emit(child, src, dst, first_scratch+k-1, child_sign) + + yield from emit(tree, 0, 1, 2, sign) + + +def compose(tree, source, target, factors, scratch, leaf, sign=1, read_only=()): + """Execute with a deterministic source-restoring additive leaf callback. + + leaf(source, target, factor, sign) must obey PROOF.md's contract. Ordinary + list identity aliases are checked before mutation, including declared + read-only arrays. Overlapping views/hidden callback state are not supported. + """ + bill = invoice(tree, [1]*len(factors)) + need(type(sign) is int and sign in (-1, 1), "sign") + need(len(scratch) >= bill['scratch'], "insufficient scratch") + arrays = [source, target, *scratch] + need(len({id(a) for a in arrays}) == len(arrays), "mutable arrays alias") + need(not any(ro is a for ro in read_only for a in arrays), "read-only alias") + need(len(source) > 0 and all(len(a) == len(source) for a in arrays), + "equal positive array lengths") + for factor, src, dst, direction in word(tree, sign): + leaf(arrays[src], arrays[dst], factors[factor], direction) diff --git a/research/dirty-echo-space-budget/verify.py b/research/dirty-echo-space-budget/verify.py new file mode 100644 index 0000000000..8b9c3288e7 --- /dev/null +++ b/research/dirty-echo-space-budget/verify.py @@ -0,0 +1,195 @@ +"""Replay the exact space/call certificate and its scoped negative controls.""" + +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) + +SOURCE_PINS = { + 628: ( + "0768f97d06c623b8211e651543c66135796b62bf", + "research/prime-power-cyclic-scan", + ("dirty.py", "weighted.py", "check.py", "scan.py", "interval_kernel.py", "DIRTY-PROOF.md", "NOTICE.md"), + ), + 673: ( + "156f259b99723468cfdd2b5d47d0ba894f09bea7", + "research/cyclic-dirty-commutator-audit", + ("echo.py", "ECHO-PROOF.md"), + ), + 689: ( + "0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a", + "research/ternary-dirty-composition", + ("ternary.py", "NOTICE.md"), + ), + 758: ( + "a164f06263e438ead570b169e5b7103aa45bf228", + "research/space-capped-dirty-echo", + ("planner.py", "NOTICE.md"), + ), +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate_sources(): + raw = (ROOT / "SOURCES.json").read_bytes() + manifest = json.loads(raw) + need(manifest["base_commit"] == "66849e1475c930fd7732b1a0067ffee7e1e95f60", "base commit changed") + expected = { + f"vendor/pr{pr}/{name}": (pr, commit, f"{directory}/{name}") + for pr, (commit, directory, names) in SOURCE_PINS.items() + for name in names + } + seen = set() + for record in manifest["files"]: + name = record["local_path"] + need(name in expected and name not in seen, "unexpected or repeated source path") + seen.add(name) + need((record["source_pr"], record["source_commit"], record["source_path"]) == expected[name], + "source provenance changed: " + name) + actual = hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + need(actual == record["sha256"], "source hash mismatch: " + name) + need(seen == set(expected), "source inventory is incomplete") + return {"files": len(seen), "manifest_sha256": hashlib.sha256(raw).hexdigest(), + "base_commit": manifest["base_commit"], + "heads": {str(pr): pin[0] for pr, pin in SOURCE_PINS.items()}} + + +def load_module(name, relative_path): + spec = importlib.util.spec_from_file_location(name, ROOT / relative_path) + need(spec is not None and spec.loader is not None, "cannot load " + relative_path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def tree_text(plan): + if not plan.children: + return "." + return "(" + ",".join(tree_text(child) for child in plan.children) + ")" + + +def compare_baselines(table): + from schedule import multiplicities, word + + original = load_module("space_budget_pr673", "vendor/pr673/echo.py") + ternary = load_module("space_budget_pr689", "vendor/pr689/ternary.py") + count = 50 + comparisons = [] + for budget in (6, 7, 8): + candidates = [] + for fanout in range(2, count + 1): + scratch, calls = original.resources(count, fanout) + if scratch <= budget: + candidates.append((calls, scratch, "PR673", fanout)) + calls, scratch = ternary.resources(count) + if scratch <= budget: + candidates.append((calls, scratch, "PR689", 3)) + calls, scratch, source, fanout = min(candidates) + if source == "PR673": + baseline_word = tuple(original.instructions(0, count, 0, 1, 2, fanout)) + baseline_peak = max(max(src, dst) for src, dst, _, _ in baseline_word) - 1 + else: + baseline_word = tuple(ternary.word(count)) + baseline_peak = max(max(src, dst) for _, src, dst, _ in baseline_word) - 1 + need(len(baseline_word) == calls and baseline_peak == scratch, "baseline word/resource mismatch") + plan = table[budget][count] + counts = multiplicities(plan) + expanded = tuple(word(plan)) + need(counts == [sum(command[0] == index for command in expanded) for index in range(count)], + "public multiplicities disagree with the actual word") + need(plan.calls <= calls and sum(counts) == plan.calls, "invalid cost comparison") + comparisons.append({ + "factors": count, "scratch_budget": budget, "scratch_used": plan.scratch, + "baseline_source": source, "baseline_fanout": fanout, + "baseline_scratch": scratch, "baseline_calls": calls, + "minimum_calls": plan.calls, "saved_calls": calls - plan.calls, + "root_partition": [child.factors for child in plan.children], + "tree": tree_text(plan), "factor_multiplicities": counts, + "all_feasible_pinned_baselines": [list(candidate) for candidate in sorted(candidates)], + }) + need([row["baseline_calls"] for row in comparisons] == [2752, 1568, 1568], "baseline changed") + return comparisons + + +def compare_concurrent(table): + from checks import polynomial_execute, polynomial_expected, polynomial_initial + + concurrent = load_module("space_budget_pr758", "vendor/pr758/planner.py") + domain = [(15, budget) for budget in range(4, 9)] + [(27, 6)] + domain += [(50, budget) for budget in (6, 7, 8)] + records = [] + for count, budget in domain: + result = concurrent.optimize([1] * count, budget) + plan = table[budget][count] + need(result["price"] == result["calls"] == plan.calls, "concurrent uniform optimum differs") + forward = tuple(concurrent.word(result["tree"])) + inverse = tuple(concurrent.word(result["tree"], -1)) + need(len(forward) == plan.calls, "concurrent word count differs") + need(result["scratch"] <= budget, "concurrent word exceeds scratch budget") + state = polynomial_initial(result["scratch"]) + polynomial_execute(state, forward) + need(state == polynomial_expected(count, result["scratch"]), "concurrent ordered product failed") + polynomial_execute(state, inverse) + need(state == polynomial_initial(result["scratch"]), "concurrent inverse failed") + records.append({"factors": count, "scratch_budget": budget, + "calls": result["calls"], "scratch_used": result["scratch"]}) + return {"source_pr": 758, "source_commit": SOURCE_PINS[758][0], "cases": records, + "scope": "Uniform-price agreement and exact symbolic forward/inverse words only; " + "not review of the full PR or its weighted and numerical claims."} + + +def certificate(): + sources = authenticate_sources() + from checks import run_checks + from rounded_check import run_rounded_checks + from schedule import plan_table + + table = plan_table(64, 8) + return { + "format": "ordered-dirty-echo-space-budget-v1", + "status": "passed", + "assignment_seed": 50, + "sources": sources, + "domain": {"factors": [1, 64], "scratch_budget": [0, 8], + "coverage": "all 576 cells; null denotes infeasibility", + "tree_encoding": "a leaf is '.', an internal node is its comma-separated children in parentheses", + "objective": "minimum uniform leaf calls in static ordered all-dirty echo trees"}, + "costs_by_budget": [[None if plan is None else plan.calls for plan in row[1:]] for row in table], + "main_witnesses": compare_baselines(table), + "concurrent_comparison": compare_concurrent(table), + "independent_checks": run_checks(), + "rounded_execution": run_rounded_checks(), + "scope": "Exact grammar-specific cost certificate and finite implementation evidence. " + "The all-size lower-bound and attainment statements use the written induction. " + "No new kappa, common-label supplier, practical runtime or full multiplication proof.", + } + + +def main(): + need(sys.version_info >= (3, 11), "Python 3.11 or newer is required by the pinned rounded-leaf verifier") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write recomputed evidence to a new file") + args = parser.parse_args() + result = certificate() + if args.write is not None: + with args.write.open("x") as output: + output.write(json.dumps(result, indent=2) + "\n") + else: + expected = json.loads((ROOT / "EXPECTED.json").read_text()) + actual_json = json.dumps(result, sort_keys=True, separators=(",", ":"), allow_nan=False) + expected_json = json.dumps(expected, sort_keys=True, separators=(",", ":"), allow_nan=False) + need(actual_json == expected_json, "recomputed certificate differs from EXPECTED.json") + print("PASS_DIRTY_ECHO_SPACE_BUDGET: n=50, arrays=6, leaves=2752->2304") + + +if __name__ == "__main__": + main()