From a2e2d4da922b64c6b137fe74e9b0fe845c60dc24 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 16:36:29 +0000 Subject: [PATCH] feat(research): minimize aligned spectator gather support --- research/optimal-spectator-gather/PROOF.md | 152 +++++++++ research/optimal-spectator-gather/README.md | 111 ++++++ .../optimal-spectator-gather/SOURCES.json | 42 +++ research/optimal-spectator-gather/TASK.json | 108 ++++++ .../optimal-spectator-gather/VALIDATION.md | 73 ++++ research/optimal-spectator-gather/VERIFY.json | 34 ++ research/optimal-spectator-gather/gather.py | 84 +++++ research/optimal-spectator-gather/verify.py | 323 ++++++++++++++++++ 8 files changed, 927 insertions(+) create mode 100644 research/optimal-spectator-gather/PROOF.md create mode 100644 research/optimal-spectator-gather/README.md create mode 100644 research/optimal-spectator-gather/SOURCES.json create mode 100644 research/optimal-spectator-gather/TASK.json create mode 100644 research/optimal-spectator-gather/VALIDATION.md create mode 100644 research/optimal-spectator-gather/VERIFY.json create mode 100644 research/optimal-spectator-gather/gather.py create mode 100644 research/optimal-spectator-gather/verify.py diff --git a/research/optimal-spectator-gather/PROOF.md b/research/optimal-spectator-gather/PROOF.md new file mode 100644 index 0000000000..9c06abe727 --- /dev/null +++ b/research/optimal-spectator-gather/PROOF.md @@ -0,0 +1,152 @@ +# Optimal overlap-aware spectator gathers + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and result + +Partition a finite binary address into N neighborhoods of K coordinates each. +All neighborhoods use the same offset convention. Let A and B be sets of h +neighborhoods, with c=|A intersection B|. Write S and T for their full sets of +hK binary coordinates. The input is the complete binary rectangle, with arbitrary +payloads, preceding fibers and arbitrary correlations between all coordinates. + +The completed operator on each active neighborhood is the same operator U. +The assignment of source neighborhoods to target neighborhoods is free, while +all K offsets within each neighborhood must be preserved. This is appropriate +for the common completed kernels in zxv's PR6070 global-H interface. It is a +changed assignment policy, not a new proof of its router or callee. + +**Theorem.** There is a gather P sending S to T that moves exactly + + 2K(h-c) binary coordinate positions + +and is a product of exactly + + h-c whole-neighborhood swaps = K(h-c) binary-coordinate swaps. + +Both counts are minimum, simultaneously. The binary-coordinate lower bounds +hold even if a competing coordinate permutation is allowed to split or reorder +neighborhoods, provided it still sends the complete set S onto T. + +The theorem is an exact optimum in a coordinate-permutation model. A +coordinate swap is one transposition of two binary address positions. It is +not a claim about a minimum CNOT count, adjacent tape movements, arbitrary +linear charts, native recursive children or a complete physical invoice. + +## Construction and lower bound + +Put L=A minus B and E=B minus A. They have the same cardinality m=h-c. +Choose any bijection f:L to E. Exchange neighborhood a with neighborhood f(a), +offset by offset, for each a in L. Fix every other coordinate. + +These exchanges have disjoint endpoints. They map A onto B, fix A intersection B +pointwise, fix every coordinate outside their symmetric difference and form an +involution. They move 2Km positions and use Km disjoint coordinate transpositions. +The deterministic implementation pairs the two sorted difference lists. + +Let sigma be any coordinate permutation with sigma(S)=T. Every coordinate of +S minus T must move: fixing one would leave a coordinate outside T in sigma(S). +Every coordinate of T minus S must also move: if fixed, its unique preimage +would lie outside S. Thus at least |S symmetric-difference T|=2Km positions move. + +The support of a word of l coordinate transpositions is contained in their +2l endpoints. Consequently l>=Km. The construction attains both lower bounds. +The same endpoint argument on neighborhood indices proves the m-swap lower +bound when each instruction exchanges two complete neighborhoods. This proof +works for every finite N,K,h and every overlap, including A=B, when no routing +is needed. The executable API requires h>=1; the empty case is trivial. + +The use of disjoint transpositions and elementary support counting is standard. +The new contribution is the optimal assignment at this spectator gather +boundary, its executable constructor and its exact before/after application. +The original sparse-extension theorem already allows arbitrary bijections. +Its general extension and support-routing cost are not claimed again here. + +## Arbitrary-input operator boundary + +For any common linear operator U on one K-bit neighborhood, let U_A be the +product of its copies on A. Disjoint copies commute. Because P preserves every +neighborhood's offsets and sends A bijectively onto B, + + P inverse * U_B * P = U_A. + +One can check this on basis tensors and extend linearly. It holds on all +payloads, including correlated dirty spectator data. No separability of the +actual input or zero workspace is assumed. P inverse=P, so the exact same +finite swap word restores the layout. + +The hypothesis that the kernels are identical matters. Distinguishable jobs +must follow their own assignment constraints; a shared neighborhood may then +have to move. Offsets matter too: the implementation preserves them even for +an operator that treats different offsets differently. The finite checks use +both exact phase-sensitive Gaussian columns and a nonsymmetric, nonseparable +four-entry neighborhood operator. + +## The spectator-row wrapper + +Retain PR6070's row, front, active and back field capacities and its complete +nested stock Q. Suppose the source neighborhoods are aligned to the same K-bit +grid as the target active slots. Replace only its ordered exposure permutation +by P above. The active target slots and every field capacity are unchanged. + +Every source coordinate maps into T. Therefore every preimage of a physical +position outside T is a genuine source spectator. This includes the complete +row prefix and compact controls, even if they originally intersect S. The +original wrapper's one whole-row padding and its row-independent completed +callee can consequently be used with the same declared contracts. + +On a completed exact return, restrict to the original rows, then apply P again. +The result is U_A. For surrounding coarse-dependent diagonals D1,D2, the result +is exactly D2 U_A D1. The second diagonal must still wait for padding removal +and inverse exposure. This proof does not assume that a diagonal commutes with +exposure or with internal row mixing. + +This is a local replacement implication under PR6070's stated completed-callee, +paid-router, ownership, precision, padding-disposal and tape hypotheses. It +does not discharge those hypotheses or any selected framework assumption. +No predecessor scientific replay is needed or claimed for this implication. + +Under the retained support-router theorem, substitute k=2K(h-c) in its cost + + O(V (k+1)^(1-a_BIT) polylog(p) + poly(p)). + +When c=0 this equals the previous 2Kh upper bound. When overlap is present it +can be smaller. The ordered construction can also already be optimal on some +inputs; no strict gain is claimed for every gather. When c=h the exposure is +identity and its routing can be omitted. No asymptotic exponent improvement +or fully priced supplier gain follows from these local counts alone. + +## A strict before/after example + +In the PR6070 layout take h=3, Q=3, G>=1 and K=128G. The row, front and back +widths are all K. The target block indices are B={2,3,4}; choose A={0,2,3}. +Enough trailing spectator capacity is retained. + +The ordered gather maps 0 to 2, 2 to 3, 3 to 4 and closes with 4 to 0. At each +of the K offsets it is a four-cycle. Hence it moves 4K coordinates and its +shortest coordinate-transposition word has length 3K. The usual cycle-count +lower bound follows because a transposition changes the number of cycles by +at most one; each four-cycle can be built with three transpositions. + +The new gather simply exchanges blocks 0 and 4. It moves 2K coordinates and +uses K coordinate transpositions, both optimal by the theorem. Blocks 2 and 3 +stay fixed. The original row block 0 receives the old block 4, which is a +source spectator. All three original kernel jobs are still delivered. + +The verifier constructs and enumerates both actual sparse permutations. +An encoded fixture has log2(p)=32, G=134, K=17152 and enough ambient reservoir +and suffix capacity. Its counts are 68608 to 34304 moved coordinates and +51456 to 17152 coordinate swaps. It is an encoded geometry, not an exported +production caller or execution of its enormous tensor. Small exact complete +row fixtures separately execute padding, dirty internal row cycling, return, +inverse exposure and both surrounding diagonals. + +## Verification boundaries + +The all-parameter theorem is the written proof above. Exhaustive enumeration +through seven neighborhood positions independently minimizes over every +permutation, including permutations moving unrelated spectators. The exact +operator checks corroborate the new implementation and boundary. They do not +formally prove the universal result or accept the inherited multiplication +framework. Unaligned source neighborhoods, different active operators, physical +router lowering and actual production-call installation remain open. diff --git a/research/optimal-spectator-gather/README.md b/research/optimal-spectator-gather/README.md new file mode 100644 index 0000000000..b33388cfc3 --- /dev/null +++ b/research/optimal-spectator-gather/README.md @@ -0,0 +1,111 @@ +# Optimal overlap-aware spectator gathers + +A freely assigned gather for identical, aligned K-bit kernels needs exactly +`2K(h-c)` moved coordinates and `K(h-c)` binary-coordinate swaps, where h +neighborhoods are active and c source neighborhoods already coincide with target +neighborhoods. The constructor fixes the overlap and exchanges the two difference +sets. Both counts are proved optimal, even against arbitrary coordinate +permutations sending the full source set onto the target set. + +This contribution was produced by Nick Petalas. Claim type: scoped proof with +finite exact corroboration. No new kappa or completed supplier is claimed. + +The new assignment improves one routing step of zxv's +[PR6070 spectator-row wrapper](https://github.com/CrocSwap/integer-mult-bounds/pull/6070). +Its ordered assignment can move shared neighborhoods unnecessarily. In the +explicit h=3, Q=3, K=128G layout, moved support falls from 4K to 2K and the +shortest coordinate-swap word from 3K to K. The same complete active slots, +stock, dirty-input operator and inverse-restoration boundary are retained. +[PROOF.md](PROOF.md) states the exact changed contract and optimality argument. + +`gather.py` constructs the new involution. `verify.py` enumerates a separate +permutation oracle and interprets complete exact operators. It imports no +predecessor verifier and does not rerun or audit the source theorem. + +## Evidence + +The normal local checker passes: + +- 5,913 permutations and 695,482 subset images, covering all 4,706 equal-size + source/target-set pairs through seven neighborhood positions; +- 3,878 complete exact Gaussian basis columns, including both offsets of + two-bit neighborhoods, and 93 nonsymmetric whole-neighborhood fixtures; +- three complete spectator-row fixtures with arbitrary dirty payloads, + whole-row padding, internal row cycling, inverse exposure and surrounding + coarse-dependent diagonals; +- one encoded layout with K=17152, reducing moved support 68608 to 34304 and + shortest coordinate swaps 51456 to 17152; +- 13 malformed-input/capacity rejections and two semantic scope controls. + +Every reported count is generated by the checker. Its JSON output also binds +all package files by SHA256. There is no hand-authored mathematical receipt. +[VALIDATION.md](VALIDATION.md) records verification and implementation limits. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/optimal-spectator-gather/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/optimal-spectator-gather/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/optimal-spectator-gather +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/optimal-spectator-gather --check-source-history --check-modes +``` + +Any CPython 3.12 path can replace the local path. Expected scientific status: +`PASS_OPTIMAL_SPECTATOR_GATHER`. The registered runner and publication preflight +have their own separate PASS markers. + +## Scope and limitations + +This is a local routing construction and exact optimum. It permits a changed +assignment among identical completed kernels. A fixed ordered assignment, +unaligned neighborhoods, distinguishable operators, CNOT counts, adjacent tape +movements and arbitrary linear encoders are different optimization problems. +The executable planner has explicit finite resource caps; the proof has no +size cap. Literal vector execution is limited to 16 address bits. + +The source's paid support-router theorem can use the smaller moved support. +A complete physical invoice, actual global-H production event, supplier, +rounded-callee/padding-disposal proof, native/compiler closure and outer +multiplication theorem remain unimplemented. All five selected assumptions +remain. The selected conditional kappa stays .003125804. No full selected cold +replay, Lean, Docker, independent human or formal proof-kernel review is claimed. + +## Open next questions + +1. Export one literal global-H call whose source and target neighborhoods share + a K-grid. Count their overlap and lower this exact gather through the paid + support router. Actual physical layout, complete stock and callee return + evidence are prerequisites; these fixtures are not that installation. +2. For unaligned complete neighborhoods, determine an exact offset-preserving + assignment and completion objective. Start with two overlapping grids and + state which chunk boundaries the physical callee requires. The present + aligned proof must not be transferred without that contract. + +## Related open work + +No open PR specifically optimizing the moved-coordinate support of this +aligned spectator gather was identified in the live open-title/body and +main/merged searches. PR6070 is a merged cited predecessor. Search caps, +sparse local notes and unpublished work limit that coverage. No additional +computation was run to check another contributor's mathematical result. + +## Credit and provenance + +Credit zxv's PR6070 for the spectator placement, row-independent completed-call +contract and installation question. The arbitrary S-union-T extension and paid +support-router theorem are retained predecessor work, including Vlado +Vojdanovski's PR1673, Jeremy Kothe's PR1758, Chafik Boukhalfa's PR1786 and their +compact-layout/support-audit lineage. Retain PR4359's stock and precision +framework and the selected P104/helper/native/compiler contributors. Elementary +permutation support and cycle facts are standard background. This package +claims the optimal assignment at this boundary and its constructor/application, +not a new general theory of permutations or a predecessor supplier result. + +Canonical base is a5bff3bf133e482541c09eba4e773884bdb2b1b7, priority revision 8. +SOURCES.json pins the retained source bytes as provenance. They are not imported +by the new verifier. The card is explicitly changed to this local constructive +step; it does not discharge an inherited assumption at a production caller. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272318) +sets this same scope. Apache-2.0. diff --git a/research/optimal-spectator-gather/SOURCES.json b/research/optimal-spectator-gather/SOURCES.json new file mode 100644 index 0000000000..646da0e65d --- /dev/null +++ b/research/optimal-spectator-gather/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/spectator-row-reservoir/README.md", + "usage": "provenance", + "git_blob": "5af75bdb7fd55ba8a810ff9e035d50dcdbcd06a1", + "sha256": "408e3ef76487a7dc43832d73bfb5b9fcc33c8cafd4e9078f40dc3f0887090a59" + }, + { + "path": "research/spectator-row-reservoir/PROOF.md", + "usage": "provenance", + "git_blob": "000c4e5ddf1446b11ee15679bf4238bec77760c8", + "sha256": "a895844a13bd747dccd64eb260dc30a0e7bb77cb66269f82ef5f5aeda2d9c782" + }, + { + "path": "research/spectator-row-reservoir/verify.py", + "usage": "provenance", + "git_blob": "a5e05c3856779c8469d178b1210090553243b9cd", + "sha256": "0e15cea067c77b1653822359cb06680581ac1ba3d9f87474bc8da11f5f71f7e9" + }, + { + "path": "research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPORT-ROUTER.md", + "usage": "provenance", + "git_blob": "4f39fa9eaf553d1df5111de8c19bcf5bf9829c2b", + "sha256": "6ddb322e11883c1177ba6cd1a77d23a1dac827d7290b32eaf642457b1d762a54" + } + ] +} diff --git a/research/optimal-spectator-gather/TASK.json b/research/optimal-spectator-gather/TASK.json new file mode 100644 index 0000000000..5bb2f6a530 --- /dev/null +++ b/research/optimal-spectator-gather/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct and prove a minimum-support, minimum-transposition gather for identical K-aligned kernels at the PR6070 spectator-row boundary.", + "scope_change_reason": "The source installation question is narrowed to one constructive routing step. The source-to-target assignment is free among identical kernels. This is not an audit or discharge of a selected assumption at a production caller.", + "bottleneck_link": "Local reduction in the moved support passed to the paid support router at a candidate global-H boundary. No completed signed moment or kappa improvement is asserted.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact local routing improvement; do not extend to unaligned neighborhoods or a production caller in this contribution.", + "outcome": "completed", + "evidence": "PROOF.md; independent finite permutation oracle, exact Gaussian columns, general block operators, dirty whole-row fixtures and generated source-hash receipt from verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Install the gather at one literal aligned global-H call.", + "why_it_matters": "Only an actual paid routing and callee boundary can turn smaller support into a completed physical benefit.", + "first_step": "Export the actual source/target neighborhoods, complete stock, protected suffix and returned endpoint; compute c and lower the new involution.", + "blocked_by": "A physical call descriptor and retained routing/callee admission are not supplied." + }, + { + "question": "Determine the corresponding optimum for unaligned complete neighborhoods.", + "why_it_matters": "A common K-grid is an explicit hypothesis of the present construction.", + "first_step": "Specify two offset grids and the callee chunk-preservation rules before optimizing a two-neighborhood example.", + "blocked_by": "An offset-preserving physical boundary for unaligned chunks is not declared." + } + ], + "source": { + "pr": 6070, + "author": "zxv", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6070" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272318", + "overlap": { + "coverage": "Live open PR titles/bodies, latest handoffs, all 807 account PR records through October 14, main README formula/object searches, targeted merged PR searches and local reservations.", + "limitations": "Some merged searches reached their 50-result cap; sparse local notes, arbitrary diffs and unpublished work are not covered.", + "main_checked": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "priority_revision": 8 + }, + "claim_type": "scoped proof with finite exact corroboration", + "environment": { + "implementation": "CPython", + "version": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + } +} diff --git a/research/optimal-spectator-gather/VALIDATION.md b/research/optimal-spectator-gather/VALIDATION.md new file mode 100644 index 0000000000..7a5fc589b6 --- /dev/null +++ b/research/optimal-spectator-gather/VALIDATION.md @@ -0,0 +1,73 @@ +# Validation and implementation limits + +Produced by Nick Petalas. Apache-2.0. + +The scientific checker uses a written all-parameter optimality proof, an +independent finite permutation minimization and literal exact operator checks. +It does not import or re-verify the predecessor construction. JSON receipts are +generated on stdout and bind the current package files. No stored expected +receipt or equality to a hand-written answer substitutes for these checks. + +The permutation oracle visits all permutations at sizes one through seven and +all source subsets, derives each target image, and records the two actual +minima. The constructor is compared with every nonempty equal-size pair. +The operator oracle compares each literal conjugated Gaussian basis column +with an independently assembled matrix-entry formula, including absolute phase. +A nonsymmetric four-entry block operator checks that whole neighborhoods and +all offsets are preserved. The full-row fixtures include correlated dirty data +and noncommuting surrounding diagonals. Capacity and semantic controls remain +active under optimized Python. + +The encoded large fixture checks integer geometry, sparse maps and the retained +finite K and reservoir/suffix inequalities. It does not materialize the tensor, +export actual long-axis neighborhoods or prove a physical call. An initial +log2(p)=30 development fixture lacked the requested reservoir capacity and was +rejected. The final log2(p)=32 fixture satisfies the unchanged inequality; the +all-size optimization claim and small semantic domain were not narrowed. + +## Local verification + +Warning-strict normal and optimized direct replays pass in 1.550 and 1.558 +seconds on macOS arm64, CPython 3.12.15. These establish the replay budget, +not a speed claim. Both emit the same mathematical counts and hash-bound +receipt. AST/syntax and JSON parsing pass; maximum function length is 33 +lines. Ruff, mypy and pyright are unavailable in this environment. No shared +diagnostic configuration is changed. Registered and committed-byte/source- +history checks are separate publication gates. + +## Power of Ten inspection + +There is no recursion, dynamic code generation, network access, subprocess, +mutable cache or concurrent state in the new code. Every loop is bounded by +an explicit input cap or a fixed finite verifier domain. Constructor validation +rejects booleans, duplicate/out-of-range blocks, unequal counts and oversized +input. Gather values are immutable and treated as trusted constructor outputs. +The literal execution path separately checks its address/vector capacities. +No assertions carry externally visible rejection or scientific acceptance. + +Functions remain below 60 physical lines. The oracle's largest subset table +has 128 entries and its largest pair-minimum table has 3432 entries. The planner +accepts at most 256 neighborhoods and 65536 selected bits, hence at most 131072 +mapped positions. The finite vector interpreter accepts at most 16 address +bits; the largest committed dirty fixture uses 14. Normal and optimized +warning-strict execution and AST/syntax inspection are the applicable Python +checks. Registered CI runs both warning-strict modes. + +Rule: 3, fix memory capacity before steady operation. +Location: gather.py and verify.py. +Reason: Python integers, Fraction values, tuples and dictionaries allocate at +runtime; this standard-library exact research checker is not a fixed-memory +physical machine. +Scope: the explicitly capped constructor, literal interpreter and fixed +permutation/operator verification domains. +Compensating control: finite caps above, no persistent caches, no retained child +processes and scoped temporary bytecode namespace cleanup. The receipt hashes +only the finite package inventory. +Verification: direct and registered normal/optimized replay, capacity exhaustion +controls and successful return from the literal semantic fixtures. +Follow-up: redesign the storage representation before increasing these caps or +using this reference as an implementation of a fixed-tape algorithm. + +No shared repository code, selected record, frozen predecessor or pinned source +is edited. Full physical routing, rounded padding disposal, supplier/compiler, +stock generation, outer recovery and proof-kernel obligations remain unrun. diff --git a/research/optimal-spectator-gather/VERIFY.json b/research/optimal-spectator-gather/VERIFY.json new file mode 100644 index 0000000000..0ee2b60b27 --- /dev/null +++ b/research/optimal-spectator-gather/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All finite permutation minima, complete exact Gaussian columns, nonsymmetric block kernels, dirty padded rows and boundary/capacity controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The identical scientific and rejection checks with Python assertions disabled." + } + ] +} diff --git a/research/optimal-spectator-gather/gather.py b/research/optimal-spectator-gather/gather.py new file mode 100644 index 0000000000..32fc38d0aa --- /dev/null +++ b/research/optimal-spectator-gather/gather.py @@ -0,0 +1,84 @@ +"""Minimum-support gathers for indistinguishable aligned neighborhoods. + +Produced by Nick Petalas. Apache-2.0. +The spectator wrapper and support-router contracts retain their source credit. +""" +from dataclasses import dataclass +from typing import Sequence + +MAX_BLOCKS = (1 << 31) - 1 +MAX_SELECTED = 256 +MAX_SELECTED_BITS = 65536 +MAX_EXECUTED_BITS = 16 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def integer(value: int, lower: int, upper: int, name: str) -> None: + require(type(value) is int and lower <= value <= upper, name) + + +@dataclass(frozen=True) +class Gather: + blocks: int + width: int + sources: tuple[int, ...] + targets: tuple[int, ...] + exchanges: tuple[tuple[int, int], ...] + + def bit_swaps(self) -> tuple[tuple[int, int], ...]: + return tuple((a*self.width+j, b*self.width+j) + for a, b in self.exchanges for j in range(self.width)) + + def mapping(self) -> dict[int, int]: + swaps = self.bit_swaps() + return dict(tuple(swaps) + tuple((b, a) for a, b in swaps)) + + +def compile_gather(blocks: int, width: int, sources: Sequence[int], + targets: Sequence[int]) -> Gather: + """Offsets are preserved; the assignment of identical kernels is free.""" + integer(blocks, 1, MAX_BLOCKS, 'Invalid block count') + integer(width, 1, MAX_SELECTED_BITS, 'Invalid neighborhood width') + require(type(sources) in (tuple, list) and type(targets) in (tuple, list), + 'Neighborhoods must be finite lists or tuples') + require(1 <= len(sources) == len(targets) <= MAX_SELECTED, + 'Equal nonempty bounded neighborhood counts required') + require(len(sources)*width <= MAX_SELECTED_BITS, 'Selected-bit capacity') + for block in tuple(sources) + tuple(targets): + integer(block, 0, blocks-1, 'Invalid neighborhood index') + source, target = frozenset(sources), frozenset(targets) + require(len(source) == len(sources) and len(target) == len(targets), + 'Repeated neighborhoods') + leaving, entering = sorted(source-target), sorted(target-source) + require(len(leaving) == len(entering), 'Unbalanced symmetric difference') + exchanges = tuple(zip(leaving, entering)) + return Gather(blocks, width, tuple(sorted(source)), tuple(sorted(target)), + exchanges) + + +def address(value: int, plan: Gather) -> int: + """Literal address oracle; symbolic plans can be much larger.""" + bits = plan.blocks*plan.width + integer(bits, 1, MAX_EXECUTED_BITS, 'Literal-address capacity') + integer(value, 0, (1 << bits)-1, 'Invalid address') + result = value + for a, b in plan.bit_swaps(): + i, j = bits-1-a, bits-1-b + different = ((result >> i) ^ (result >> j)) & 1 + result ^= different*((1 << i) | (1 << j)) + return result + + +def permute(values: list, plan: Gather) -> list: + bits = plan.blocks*plan.width + integer(bits, 1, MAX_EXECUTED_BITS, 'Literal-vector capacity') + require(type(values) is list and len(values) == 1 << bits, + 'Complete binary rectangle required') + out = [None]*len(values) + for index, value in enumerate(values): + out[address(index, plan)] = value + return out diff --git a/research/optimal-spectator-gather/verify.py b/research/optimal-spectator-gather/verify.py new file mode 100644 index 0000000000..b34823f575 --- /dev/null +++ b/research/optimal-spectator-gather/verify.py @@ -0,0 +1,323 @@ +#!/usr/bin/env python3 +"""Exact optimization and operator certificates for the new gather. + +Produced by Nick Petalas. Apache-2.0. No predecessor verifier is imported. +""" +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations, permutations +from pathlib import Path +import json +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def cycle_cost(permutation): + seen = set() + cycles = 0 + for start in range(len(permutation)): + if start in seen: + continue + cycles += 1 + current = start + for _ in range(len(permutation)): + if current in seen: + break + seen.add(current) + current = permutation[current] + need(current == start, 'Cycle decomposition did not close') + return len(permutation)-cycles + + +def permutation_oracle(api): + pair_count = permutation_count = image_count = 0 + for size in range(1, 8): + minima = {} + for permutation in permutations(range(size)): + permutation_count += 1 + moved = sum(i != j for i, j in enumerate(permutation)) + swaps = cycle_cost(permutation) + images = [0]*(1 << size) + for mask in range(1 << size): + if mask: + low = mask & -mask + images[mask] = images[mask ^ low] | (1 << permutation[low.bit_length()-1]) + key = (mask, images[mask]) + old = minima.get(key, (size+1, size+1)) + minima[key] = (min(old[0], moved), min(old[1], swaps)) + image_count += 1 + for (source, target), best in minima.items(): + missing = (source & ~target).bit_count() + need(best == (2*missing, missing), 'Independent permutation optimum') + if source: + sources = tuple(i for i in range(size) if source >> i & 1) + targets = tuple(i for i in range(size) if target >> i & 1) + plan = api.compile_gather(size, 1, sources, targets) + mapping = plan.mapping() + need(len(mapping) == best[0], 'Constructed support attains minimum') + need(len(plan.bit_swaps()) == best[1], 'Constructed word attains minimum') + need({mapping.get(i, i) for i in sources} == set(targets), 'Exact gather image') + need(all(mapping.get(mapping.get(i, i), i) == i for i in range(size)), + 'Involution restores every coordinate') + pair_count += 1 + return dict(permutations=permutation_count, subset_images=image_count, + equal_cardinality_pairs=pair_count, maximum_blocks=7) + + +def ordered_counts(plan): + """Count the ordered S-to-T completion used for the before fixture.""" + sources = tuple(block*plan.width+j for block in plan.sources + for j in range(plan.width)) + targets = tuple(block*plan.width+j for block in plan.targets + for j in range(plan.width)) + mapping = dict(zip(sources, targets)) + for a, b in zip(sorted(set(targets)-set(sources)), + sorted(set(sources)-set(targets))): + mapping[a] = b + support = tuple(sorted(mapping)) + indices = {value: i for i, value in enumerate(support)} + permutation = tuple(indices[mapping[value]] for value in support) + moved = sum(a != b for a, b in mapping.items()) + return moved, cycle_cost(permutation) + + +def multiply(a, b): + return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0] + + +def gaussian(values, positions, bits): + out = list(values) + for position in positions: + mask = 1 << (bits-1-position) + for x in range(len(out)): + if x & mask: + continue + ar, ai = out[x] + br, bi = out[x | mask] + out[x] = ((ar-ai+br+bi)/2, (ar+ai-br+bi)/2) + out[x | mask] = ((ar+ai+br-bi)/2, (-ar+ai+br+bi)/2) + return out + + +def gaussian_column(column, positions, bits): + """Independent matrix-entry formula, with no butterfly evaluation.""" + out = [ZERO]*(1 << bits) + for flips in range(1 << len(positions)): + row, coefficient = column, ONE + for j, position in enumerate(positions): + flip = (flips >> j) & 1 + row ^= flip << (bits-1-position) + coefficient = multiply(coefficient, (F(1, 2), F(-1 if flip else 1, 2))) + out[row] = coefficient + return out + + +def complete_columns(api): + columns = 0 + for width, sizes in ((1, range(1, 5)), (2, range(1, 4))): + for size in sizes: + bits = width*size + for count in range(1, size+1): + choices = tuple(combinations(range(size), count)) + for sources in choices: + for targets in choices: + plan = api.compile_gather(size, width, sources, targets) + for offset in range(width): + selected = tuple(i*width+offset for i in sources) + placed = tuple(i*width+offset for i in targets) + for column in range(1 << bits): + values = [ZERO]*(1 << bits) + values[column] = ONE + actual = api.permute(gaussian(api.permute(values, plan), placed, bits), plan) + need(actual == gaussian_column(column, selected, bits), + 'Complete exact Gaussian operator column') + columns += 1 + return columns + + +def nonsymmetric_block(values, blocks, width): + """A nonseparable integer block operator distinguishes every offset.""" + bits = (len(values)-1).bit_length() + out = list(values) + for block in blocks: + shift = bits-(block+1)*width + mask = ((1 << width)-1) << shift + for index in range(len(out)): + if index & mask: + continue + indices = tuple(index | (j << shift) for j in range(1 << width)) + incoming = tuple(out[j] for j in indices) + for row, target in enumerate(indices): + out[target] = incoming[row] + (row+2)*incoming[(row+1) % len(indices)] + return out + + +def general_block_controls(api): + cases = 0 + for size in range(2, 5): + for count in range(1, size+1): + for sources in combinations(range(size), count): + for targets in combinations(range(size), count): + plan = api.compile_gather(size, 2, sources, targets) + values = [i*i-3*i+1 for i in range(1 << (2*size))] + actual = api.permute(nonsymmetric_block(api.permute(values, plan), targets, 2), plan) + need(actual == nonsymmetric_block(values, sources, 2), + 'Identical general block operator, offsets preserved') + cases += 1 + plan = api.compile_gather(3, 1, (0, 1), (1, 2)) + # A distinguished source-to-target assignment cannot be dropped. + values = list(range(8)) + expected = nonsymmetric_block(nonsymmetric_block(values, (0,), 1), (1,), 1) + actual = api.permute(nonsymmetric_block(nonsymmetric_block(api.permute(values, plan), (1,), 1), (2,), 1), plan) + # Equal operators are the positive control; unequal scalar-weighted jobs fail below. + need(actual == expected, 'Equal-job control') + unequal = [v*(1+((x >> 2) & 1)) for x, v in enumerate(values)] + wrong = api.permute([v*(1+((x >> 1) & 1)) + for x, v in enumerate(api.permute(values, plan))], plan) + need(wrong != unequal, 'Distinguishable-job mutation must fail') + return cases + + +def diagonal(values, bits, salt): + phases = (ONE, (F(0), F(1)), (F(-1), F(0)), (F(0), F(-1))) + return [multiply(value, phases[((x*salt) ^ (x >> 1)).bit_count() % 4]) + for x, value in enumerate(values)] + + +def wrapped(values, api, plan, row_bits, stock, early_diagonal=False): + bits = plan.blocks*plan.width + data = api.permute(values, plan) + rows = 1 << row_bits + padded = stock*((rows+stock-1)//stock) + stride = 1 << (bits-row_bits) + need(rows >= stock and rows <= padded < 2*rows, 'Single bounded whole-row padding') + records = [data[j*stride:(j+1)*stride] for j in range(rows)] + records += [[ZERO]*stride for _ in range(padded-rows)] + records = records[1:] + records[:1] + targets = tuple(block*plan.width-row_bits for block in plan.targets) + records = [gaussian(row, targets, bits-row_bits) for row in records] + records = records[-1:] + records[:-1] + need(all(v == ZERO for row in records[rows:] for v in row), 'Padded zero return') + data = [v for row in records[:rows] for v in row] + if early_diagonal: + data = diagonal(data, bits, 7) + return api.permute(data, plan) + + +def wrapper_fixtures(api): + # This is PR6070's geometry formula, not a replay of its scientific suite. + width = guard = 1 + stock = 3 + cases = [] + for count in (1, 2, 3): + row_bits = width*((stock-1).bit_length()+width-1)//width + front = width*((2*count*guard+width-1)//width) + back = width*((count*guard+width-1)//width) + start = row_bits+front + targets = tuple(range(start, start+count)) + sources = (0,)+targets[:-1] + bits = start+count+back + plan = api.compile_gather(bits, width, sources, targets) + values = [(F(x % 7-3), F(x % 5-2)) for x in range(1 << bits)] + inputs = diagonal(values, bits, 3) + expected = diagonal(gaussian(inputs, sources, bits), bits, 7) + actual = diagonal(wrapped(inputs, api, plan, row_bits, stock), bits, 7) + need(actual == expected, 'Dirty complete rows and surrounding coarse diagonals') + if count == 3: + need(wrapped(inputs, api, plan, row_bits, stock, True) != expected, + 'Early coarse diagonal must fail') + mapping = plan.mapping() + need(all(mapping.get(i, i) not in sources for i in range(row_bits)), + 'Exposed rows are genuine spectators') + old_moved, old_swaps = ordered_counts(plan) + need((old_moved, old_swaps) == (count+1, count), 'Ordered fixture cycle') + cases.append(dict(h=count, K=width, n=bits, Q=stock, + old_moved=old_moved, new_moved=len(mapping), + old_minimum_swaps=old_swaps, new_swaps=len(plan.bit_swaps()))) + return cases + + +def rejection_controls(api): + bad = [(0, 1, (0,), (0,)), (2, 0, (0,), (1,)), + (2, 1, (), ()), (2, 1, (0,), (0, 1)), + (2, 1, (0, 0), (0, 1)), (2, 1, (0,), (2,)), + (2, 1, (True,), (0,)), (2, 1, {0}, (1,)), + (257, 1, tuple(range(257)), tuple(range(257))), + (2, 65536, (0, 1), (0, 1))] + rejected = 0 + for args in bad: + try: + api.compile_gather(*args) + except ValueError: + rejected += 1 + else: + raise ValueError('Malformed or over-capacity gather accepted') + huge = api.compile_gather(1000000, 1, (0,), (999999,)) + for call in (lambda: api.address(0, huge), + lambda: api.address(4, api.compile_gather(2, 1, (0,), (1,))), + lambda: api.permute([1], api.compile_gather(2, 1, (0,), (1,)))): + try: + call() + except ValueError: + rejected += 1 + else: + raise ValueError('Literal execution boundary accepted') + return rejected + + +def encoded_geometry(api): + logp = 32 + guard = 4*logp+6 + width = 128*guard + # Q=3 gives R=K; h=3 gives front=back=K in the retained layout. + blocks = (1 << logp)//(16*width) + plan = api.compile_gather(blocks, width, (0, 2, 3), (2, 3, 4)) + need(width >= guard+4*logp+10, 'Retained finite K guard') + need(plan.blocks*width > 9*(2*width)*guard+2*(2*width+1)*logp**2+6*width, + 'Encoded reservoir and suffix capacity') + need(len(plan.mapping()) == 2*width and len(plan.bit_swaps()) == width, + 'Encoded optimal gather') + old_moved, old_swaps = ordered_counts(plan) + need((old_moved, old_swaps) == (4*width, 3*width), 'Encoded ordered cycles') + return dict(log2p=logp, K=width, G=guard, Q=3, h=3, + old_moved=old_moved, new_moved=len(plan.mapping()), + old_minimum_swaps=old_swaps, new_swaps=len(plan.bit_swaps()), + scope='Encoded aligned layout only; no production call or tensor execution') + + +def verify(api): + return dict(status='PASS_OPTIMAL_SPECTATOR_GATHER', + claim_type='scoped proof with finite exact corroboration', + optimum='moved=2*K*(h-c); coordinate_swaps=K*(h-c)', + oracle=permutation_oracle(api), gaussian_basis_columns=complete_columns(api), + general_block_fixtures=general_block_controls(api), + spectator_row_fixtures=wrapper_fixtures(api), + encoded_geometry=encoded_geometry(api), + malformed_or_capacity_rejections=rejection_controls(api), + semantic_rejections=['distinguishable kernels', 'early coarse diagonal'], + new_kappa=False) + + +def main(): + # A fresh read namespace prevents preexisting bytecode from replacing source. + with tempfile.TemporaryDirectory(prefix='optimal-gather-bytecode-') as cache: + sys.pycache_prefix = cache + sys.path.insert(0, str(HERE)) + import gather + result = verify(gather) + result['package_sha256'] = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()