diff --git a/research/native-shear-batch/CERTIFICATE.json b/research/native-shear-batch/CERTIFICATE.json new file mode 100644 index 0000000000..b774a521ff --- /dev/null +++ b/research/native-shear-batch/CERTIFICATE.json @@ -0,0 +1,66 @@ +{ + "matrix_rows": [5, 30, 11, 14], + "census": { + "sample_sets": 224, + "ordered_schedules": 5376, + "xor_histogram": {"30": 232, "32": 924, "34": 1820, "36": 1640, "38": 624, "40": 124, "42": 12}, + "best": { + "xor_scans": 30, + "source_states": [0, 5, 11, 27], + "target_reads": [5, 11, 12, 2], + "source_scans": 10, + "private_read_scans": 8, + "direct_scans": 12, + "queries": 8, + "affine_events": 48 + }, + "separate": { + "bases": 28, + "xor_scans": 36, + "basis": [5, 14, 16], + "target_reads": [5, 14, 2], + "queries": 12, + "affine_events": 72 + } + }, + "program": [ + ["query", 9, 1], + ["xor", 0, 9], + ["xor", 2, 9], + ["query", 9, -1], + ["xor", 9, 4], + ["xor", 9, 6], + ["query", 9, 1], + ["xor", 0, 9], + ["xor", 1, 9], + ["xor", 3, 9], + ["query", 9, -1], + ["xor", 9, 5], + ["xor", 9, 6], + ["xor", 9, 7], + ["query", 9, 1], + ["xor", 2, 9], + ["xor", 3, 9], + ["query", 9, -1], + ["xor", 9, 8], + ["query", 9, 1], + ["xor", 1, 9], + ["query", 9, -1], + ["xor", 9, 4], + ["xor", 9, 5], + ["xor", 9, 7], + ["xor", 9, 8], + ["xor", 0, 4], + ["xor", 0, 6], + ["xor", 1, 5], + ["xor", 1, 6], + ["xor", 1, 7], + ["xor", 1, 8], + ["xor", 2, 4], + ["xor", 2, 5], + ["xor", 2, 7], + ["xor", 3, 5], + ["xor", 3, 6], + ["xor", 3, 7] + ] +} diff --git a/research/native-shear-batch/CLAIM.md b/research/native-shear-batch/CLAIM.md new file mode 100644 index 0000000000..2aeb44872c --- /dev/null +++ b/research/native-shear-batch/CLAIM.md @@ -0,0 +1,21 @@ +# Sprint claim + +- Track: recursive interfaces, OS-random assignment seed 52, drawn with Python `secrets.randbelow(100)`. +- Exact base: `bbc600db2fc15007b7c914f4f2b2ed55fa909c87`. +- Started: 2026-10-13 15:38 UTC. Planned finish: 16:18 UTC. Verification and handoff reserved from 16:08 UTC. +- Object: PR #677's private-only restored DATA shear for PR #521's native BIT query. Batch a rank-three matrix of shears through one arbitrary-dirty private row. +- Hypothesis: share dirty-offset correction across four query excursions, reducing twelve rank-factored recursive queries to eight. Enumerate affine exposure bases and source transitions to price every XOR scan. +- Deliverable: exact schedule, written identity and complete local recurrence, source pins, reproducible checker, meaningful rejection controls, and an exhaustive finite schedule-cost certificate. No new kappa or supplier admission claim. +- Three candidates considered: batch PR #677's private-only DATA boundaries; extend PR #822's dirty connector reuse; extend PR #889's common-factor output batching. The latter two already have dedicated constructions and broader follow-ups. The selected task studies a fixed native ADDRESS query and explicitly prices its lowering and VALUE scans. +- Overlap checked: all 703 open PRs, followed by all-state metadata through #976; PRs #677, #822, #889, #938, #943, #951 and #974. PR #889 is credited for related common-factor dirty correction sharing. PR #974 studies optimistic selected-profile budgets, a different question. No pinned sprint coordination issue exists, so this local claim is used. +- Selected result at base: conditional kappa `1661960547713947/1000000000000000000`, PR #942 T37 with PR #589 on #555. The selected certificate was followed to `docs/research/community-batch952-review.md`, the source manifest and `research/complex-t37-owners/README.md`. + +Prepared for Sagar Thakrar / @thakrarsagar with substantial OpenAI Codex assistance. Apache-2.0. This claim does not reserve work against other contributors. + +## Completed result, 2026-10-13 16:05 UTC + +Submitted as [PR #990](https://github.com/CrocSwap/integer-mult-bounds/pull/990). The exact rank-three fixture uses eight complete native queries and 30 XOR scans, compared with twelve queries and 36 scans for the best separately completed rank-factor schedule. All 5,376 minimum-query excursion schedules were checked by two enumeration formulations; 232 attain the minimum. The complete paid recurrence and limited optimization class are in README.md. No new kappa is claimed. + +Normal, optimized and relocated verification passed, including 7,290 full-domain input columns and their inverse, eight built-in negative controls, a paid neutral pair and four actual-certificate corruptions. All nine source hashes, selected-record integrity and 17 selected-result tests passed. Existing files and upstream/ are unchanged. Full supplier replay, repository-wide make verify, hosted CI and Lean were not run. + +Construction finished before the final verification/packaging phase, which began by 15:57 UTC. The submission refresh covered all 694 then-open PRs through #984 and the latest metadata immediately before posting through #989. No pinned coordination issue existed. Related concurrent #982 is credited for its different output-borrowed contract. Main advanced to `55645f9d4d806d67875c1c8b9840b0b039ece22e`, retaining the same selected kappa and with no package-path overlap. The original investigation base remains the commit above. diff --git a/research/native-shear-batch/NOTICE.md b/research/native-shear-batch/NOTICE.md new file mode 100644 index 0000000000..8d954efe1d --- /dev/null +++ b/research/native-shear-batch/NOTICE.md @@ -0,0 +1,13 @@ +# Attribution and scope + +Contributed by Sagar Thakrar / @thakrarsagar with substantial OpenAI Codex assistance in task selection, mathematics, implementation, verification and writing. New code and prose are under the repository's Apache-2.0 license. No independent human review or official OpenAI endorsement is claimed. + +- Karl Appel / @applecrusher, PR #521 at `a190fdb39f31647fc6f651625353710624627348`, supplies the native unipotent ADDRESS map and seven-event lowering. The lowering in `verify.py` is an attributed transcription, checked against an independently written direct map. +- @commdata2338, PR #677 at `613c02b8b4411f991f108dcc1481b3f9100b996f`, supplies the completed DATA-shear contracts, single-shear private-only construction, query-model distinctions and typed cost accounting used here. Its notice discloses OpenAI Codex and Claude Code assistance. +- @CubeJerry, PR #889 at `e2021d1c9e06948528cbc0a8fd7079b671da981d`, supplies related common-factor multi-output dirty correction sharing. We claim no priority for that mechanism. Ross Richardson's PR #938 independently audits the corresponding star-word minima; our census concerns native-query excursions and their scalar scan costs, not that star language. +- PR #822 studies connector reuse in recursive product trees. PR #974 studies optimistic budgets for the selected T21/T37 interfaces. They are distinct concurrent work, credited and excluded from this packet's claims. +- Concurrent PR #982 at `5eca5b435d2ce172edf6ffb85694c7efa31bf114` borrows an output in place of a dedicated connector for common-factor batches. This packet keeps a dedicated private row and forbids DATA queries; no priority or dominance over that different contract is claimed. +- OpenAI #109 and the retained upstream stream/interchange sources supply the ordered-affine, complete-range, tape and restoration contracts. Those contracts remain premises. The original source and license notices in `upstream/` are unchanged. +- Jonathan Capalbo's selected PR942 T37 composition, its complex lineage and DreamingOfClouds' PR589 on eumemic's PR555 bit supplier retain their existing attribution and selected status. Their full proof and validation are not rerun or replaced here. + +The contribution is the explicit private-only batch boundary, paid recurrence and finite affine-state scheduling evidence. It does not claim a new kappa, an installed supplier, a general optimum, a practical multiplication speedup or a full formal multiplication theorem. diff --git a/research/native-shear-batch/README.md b/research/native-shear-batch/README.md new file mode 100644 index 0000000000..5b77631c5f --- /dev/null +++ b/research/native-shear-batch/README.md @@ -0,0 +1,133 @@ +# Batch restored native DATA shears through one dirty private row + +**Research construction with a scoped finite optimum. No new kappa.** + +This extends the private-only boundary of [PR #677](https://github.com/CrocSwap/integer-mult-bounds/pull/677), using Karl Appel's native ADDRESS query from [PR #521](https://github.com/CrocSwap/integer-mult-bounds/pull/521). Four DATA targets receive a rank-three combination of five immutable DATA sources. Sharing the correction for the arbitrary private input reduces twelve complete recursive queries to eight. The best schedule in the class below also reduces 36 aligned XOR scans to 30. + +The elementary sharing idea is related to @CubeJerry's [PR #889](https://github.com/CrocSwap/integer-mult-bounds/pull/889), which batches common-factor product shears. This contribution supplies a different, fully specified native-query boundary, its complete child/affine/scan bill, and an exhaustive affine-state schedule census. It does not claim priority for compute/uncompute or general dirty correction sharing. + +## Reproduce + +From the repository root, with Python 3.10 or later and no external packages: + +```sh +python3 -I -B research/native-shear-batch/verify.py +``` + +Expected: + +```text +PASS_NATIVE_SHEAR_BATCH schedules=5376 queries=12->8 xor_scans=36->30 columns=7290 negative_controls=8 no_new_kappa +``` + +`CERTIFICATE.json` contains the complete 38-event program. Rows 0 through 3 are targets, rows 4 through 8 are sources, and row 9 is the dirty private row. `query` acts only on row 9. Its last field is the signed direction of the native query. `xor` gives destination and source row numbers. The checker emits the schedule afresh and compares the entire certificate, then executes it symbolically and on the complete order-three ADDRESS domain. Optimized Python is supported; checks do not depend on `assert`. + +Exact base: `bbc600db2fc15007b7c914f4f2b2ed55fa909c87`. Source commits and SHA-256 values are in `SOURCES.json`. The selected result at that base is PR942's conditional `1661960547713947/1000000000000000000`. Neither it nor `upstream/` is modified. + +## Endpoint and schedule + +All VALUE arithmetic is XOR over F2. Every row has the same complete ADDRESS domain and volume U. Let h be PR521's invertible ADDRESS permutation acting linearly on VALUE arrays. The endpoint is + +```text +X' = X + (I+h) M Y, Y' = Y, q' = q. + +M = [1 0 1 0 0] + [0 1 1 1 1] + [1 1 0 1 0] + [0 1 1 1 0] +``` + +The private input q=d is arbitrary, including values unrelated to every DATA row. No row is copied, cleared or assumed zero. Source rows never change. Targets and private q are exclusively owned for the duration of the complete batch; intermediate states are not completed DATA interfaces. + +A source mask b represents the XOR of selected Y rows, with source zero in its low bit. The program visits the following four private states. Each visit applies h to q, adds that row to the indicated targets, then applies h inverse to q. Between visits it toggles the individual source rows needed to change b. Finally it restores b to zero and adds M Y directly to the targets. + +| b before query | Targets reading h q | Source scans from previous b | +|---:|---|---:| +| 0 | X0, X2 | 0 | +| 5 | X0, X1, X3 | 2 | +| 11 | X2, X3 | 3 | +| 27 | X1 | 1 | +| Return to 0 | None | 4 | + +There are ten source-to-q scans, eight q-to-target scans and twelve direct source-to-target scans. Four forward/inverse query pairs give eight recursive children and 48 affine events. + +For a general list of sample masks b_j and target-column masks a_j, the sampled target addition is + +```text +sum_j a_j h(d + b_j Y) + = (sum_j a_j) h(d) + h(sum_j a_j b_j Y). +``` + +Here the four target masks are `5, 11, 12, 2`. Their XOR is zero. Their outer products with the four source masks sum to M: the target rows are `5`, `5 XOR 27 = 30`, `0 XOR 11 = 11`, and `5 XOR 11 = 14`. Thus arbitrary dirt cancels, the sampled contribution is h M Y, and the direct scans finish the claimed endpoint. The final source toggles restore q=d. The inverse reverses every event and reverses each query direction. The endpoint itself is an involution. + +This is a written identity for arbitrary arrays and any invertible linear h. The finite tests below check its implementation, not the full multiplication theorem. + +## Exactly what was optimized + +An **excursion** in this note is one h query on q, any set of direct q-to-target reads, and one h-inverse query returning q to the unpermuted source chart. Source toggles happen only outside excursions. The allowed remaining operations are individual source-to-q and source-to-target XOR scans. Target-to-target and source-to-source mixing, extra private rows, negative-height excursions, adjacent queries without return, and alternative ADDRESS primitives are outside this optimization class. + +On arbitrary complete arrays, h and I are linearly independent over F2: PR521's h has a nontrivial odd-order ADDRESS orbit. With k sampled states, arbitrary-dirt restoration requires `sum a_j=0`, and matching the h coefficient requires `sum a_j b_j=M`. Consequently + +```text +M = sum_(j=1..k-1) a_j (b_j + b_0), +rank(M) <= k-1. +``` + +The fixture has rank three, so at least four excursions, hence eight queries, are necessary **in this class**. Four suffice. This does not generalize PR677's one-shear private-only lower bound to every multi-shear query word. + +At this minimum, the four b values must be affinely independent and their differences must span the three-dimensional row space +`{0,5,11,14,16,21,27,30}`. The checker considers all `choose(32,4)=35,960` four-element subsets of F2^5, retains exactly 224 valid sample sets, and evaluates all 24 orders of each. This includes offsets outside the row space. For each set, the even-parity coordinates of each M row uniquely determine all target reads. The minimum transitions between fixed source states cost their Hamming distance. Direct M Y costs twelve scans in this class. + +All 5,376 schedules were completed, with no timeout or early stopping. Their XOR cost histogram is in the certificate. A second enumeration starts with the 168 ordered bases of the target column space and solves source coordinates for each of 32 offsets; it produces the same full histogram. The minimum is 30, attained by 232 schedules. The certificate chooses the lexicographically first minimizing tuple of source states, then target masks. Longer source paths, repeated cancelling reads and extra direct scans cannot lower the count for any fixed schedule. + +The comparison is stronger than applying the four-query single-edge program twelve times. It considers all 28 unordered bases of the row space and uses the unique rank-three factorization `M=A B` for each. Each factor gets its own complete PR677 dirty restoration. Even allowing all final direct terms to cancel globally into M Y, this comparison needs twelve queries and at least + +```text +2 sum_j weight(B_j) + 2 sum_j weight(A_j) + weight(M) = 36 +``` + +XOR scans. The minimizing basis is `5,14,16`, with target masks `5,14,2`. This baseline optimum is also scoped to those separately completed rank factors. A DATA-query contract can instead use PR677's two-query shears; the present result is useful only when queries must stay private. + +Assignment seed 52 was drawn with operating-system randomness. The fixture uses `random.Random(52).getrandbits(5)` for four rows, rejecting zero rows, missing source columns and ranks other than three. The stopping rule is the first accepted matrix within 1,000 attempts. It is accepted at attempt six. Randomness selects the object; the subsequent schedule census is exhaustive. No closed global search or fixed-menu exponent barrier is reopened. + +## Complete local recurrence + +For odd prime ell and b at least one, retain PR521's six ordered ADDRESS fields `(H0,H1,H2,D0,D1,D2)`, each of width b. Its map is + +```text +h_address = I6 + s r^T / 4, +s = (1,0,1,-1,0,-1)^T, r = (1,0,-1,-1,0,1)^T. +``` + +Its seven chronological events are `a2-=a0`, `a3+=a0`, `a5=(a5+5a0-a2-a3)/4`, a complete recursive ordinary interchange of fields 0 and 5, `a2+=a0`, `a3-=a0`, and `a5=-4a5+3a0+a2+a3`. The reverse inverts every event. Every affine control precedes its target. Denominators and diagonal coefficients are units for every odd ell. Complete spectator ranges remain present in each child. + +Let C(U,b) bound a complete ordinary interchange child on the queried row, including its restored recursive workspace. Let A(U,b) bound one retained ordered-affine event, including coefficient preparation, source access, temporary streams, arithmetic and head returns. Let X(U) bound an aligned native XOR scan, including both source/target access and head returns. Let R(V,b) pay row routing, split/merge if needed, descriptors, parking/recovery and any fixed evaluator setup not already in C, A or X. These are the inherited streaming contracts, not unit-cost arithmetic assumptions. + +There are nine genuine DATA rows, so V=9U; the dirty private row adds U persistent storage. The paid local recurrence is + +```text +B_batch(V,3b) <= 8 C(V/9,b) + 48 A(V/9,b) + + 30 X(V/9) + R(V,b). +``` + +Every one of the eight children acts on the entire private row of actual volume V/9 and width b, including all spectators. The parent ADDRESS width is 3b in each H/D group. V/9 follows from this nine-row input contract; it is not borrowed from PR677's three-row V/3 normalization. For independent batches, sum this entire bill at every invocation. No child is omitted as a recovery step, and no cached h(d) row is retained between batches. + +For this fixed row count and fixed literal schedule, the non-child terms are O(V) under the inherited stream contracts. Therefore, if `C(U,b) <= U c(b)`, the conditional local normalization is `B_batch(V,3b)/V <= (8/9)c(b)+O(1)`. This is a typed reduction from B_batch to C, **not** a self-recursion for ordinary multiplication or a new exponent. The separately completed comparison has `12 C + 72 A + 36 X + R_sep`, with the same persistent rows. No measured runtime comparison is asserted, and the routing constants may differ. + +Persistent row storage is `10U = 10V/9`. A safe total peak bound is `10U + W_local(V,b) + W_C(U,b)`, where W_local includes affine evaluator, routing and parking scratch. Calls run sequentially and reuse restored child workspace. There are no new full helper rows, source copies, zeroing or erasure operations. Internal scratch, precision for address counters and tape work remain in A, C and W_local. VALUE arithmetic itself is exact XOR. + +## Verification and remaining obligations + +The checker compares the complete emitted word and both census formulations to the certificate. It checks the endpoint and literal inverse as Laurent polynomials over F2 with one arbitrary input symbol per row. Independently, a bitset matrix interpreter checks all 7,290 input columns over all 729 addresses in `(Z/3)^6`, including every private and source column, and then reverses the whole program. The direct ADDRESS map and chronological affine/child lowering agree on all six rational columns, every order-three address and every one of the 15,625 order-five addresses. The literal reversed affine/child lowering is also checked on every rational basis column. + +Eight negative controls reject omitted dirt compensation, omitted private restoration, an omitted direct term, a wrong query direction, a query on a DATA row, a wrong source, removal of the recursive child from its affine wrappers, and an underpriced certificate. A positive control adds two cancelling XORs and requires both to remain charged. + +Validation on 2026-10-13, macOS 26.5.2 arm64 with Python 3.14.8: normal and isolated optimized runs passed, including a two-file copy executed from outside the repository. Four additional actual-certificate mutations were rejected by the command-line verifier at their intended guards: query underpricing, a missing event, a histogram change preserving the schedule total, and a changed target matrix. All nine Git source hashes matched. `make selected-record-check` and all 17 `test_selected*.py` tests passed. No repository-wide `make verify`, cold supplier reconstruction, hosted CI or Lean build was run; this package changes no existing generator or selected supplier artifact. + +The rank argument is a written scoped proof. The 30-scan optimality is a complete finite census in its stated class, not a formal proof of an unrestricted circuit lower bound. The exact identities and finite replays do not instantiate a supplier or prove the complete multiplication theorem. + +Still required before any exponent claim: identify actual supplier calls with this common h and source/target incidence, authorize their private-only batch lifetime, admit their complete row stock and routes, compose the full bit and complex profiles, and check the assembly inequalities. All-size compilation, common-label realization, whole-call hosting and the inherited tape/analytic interfaces remain obligations. This packet does not change either supplier, so it makes no claim about which assembly constraint would bind after integration. It is not an inference from PR974's optimistic budget relaxations. + +The final overlap review also found [PR #982](https://github.com/CrocSwap/integer-mult-bounds/pull/982), which removes a dedicated connector by borrowing an output in a product-shear batch. That changes the scratch and permitted-query contract. This package retains one dedicated private row and never queries DATA; it does not compete with or supersede that result. + +Attribution, licensing and substantial AI assistance are disclosed in `NOTICE.md`. Session selection and overlap checks are recorded in `CLAIM.md`. diff --git a/research/native-shear-batch/SOURCES.json b/research/native-shear-batch/SOURCES.json new file mode 100644 index 0000000000..f423d9d93e --- /dev/null +++ b/research/native-shear-batch/SOURCES.json @@ -0,0 +1,58 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "base_commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "runtime_dependencies": "Python 3.10+ standard library only; no predecessor code imported at runtime", + "pins": [ + { + "commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "path": "upstream/build/sections/02-streams.tex", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + }, + { + "commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "path": "upstream/build/sections/04-swap.tex", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906" + }, + { + "commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "path": "certificates/selected-result.json", + "sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3" + }, + { + "commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "path": "docs/research/community-batch952-review.md", + "sha256": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b" + }, + { + "commit": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "path": "research/native-fusion-restored-shear/PROOF.md", + "sha256": "4f281eb48b9662c03269717b3919b45b27f7c2655abb185249a1eea2a03af186" + }, + { + "commit": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "path": "research/native-fusion-restored-shear/PROGRAM.json", + "sha256": "ee090fa1dde69d197ee147d7d92e0a43db30725a4984f9c464d97bd2c172f302" + }, + { + "commit": "613c02b8b4411f991f108dcc1481b3f9100b996f", + "path": "research/native-fusion-restored-shear/NOTICE.md", + "sha256": "d79071e9dda5edc60305f80910572c1a61daf0b4601f5673b5ff874a6d487742" + }, + { + "commit": "a190fdb39f31647fc6f651625353710624627348", + "path": "research/native-unipotent-fusion/PROOF.md", + "sha256": "320ce5529c1543f9e6fceb9e7f8b563ed332f13923229e38d4e7edac98f30283" + }, + { + "commit": "a190fdb39f31647fc6f651625353710624627348", + "path": "research/native-unipotent-fusion/check.py", + "sha256": "41f9b2bf8df9541f33903e8f7364efc4ed0da77aa43a8cad0368f95b9f68cf99" + } + ], + "related_work": [ + {"pr": 889, "commit": "e2021d1c9e06948528cbc0a8fd7079b671da981d", "relationship": "Common-factor multi-output shears and shared dirty correction; predecessor idea, not a priority claim here"}, + {"pr": 822, "commit": "8c5e1b557f59bca29139c4c2dcc65edfb808372b", "relationship": "Reuses dirty connectors across recursive products; different query contract"}, + {"pr": 974, "commit": "f40cd20a8c257bcfee17508c7de68fee24df0568", "relationship": "Selected-supplier optimistic interface budgets; no supplier budget improvement inferred here"}, + {"pr": 982, "commit": "5eca5b435d2ce172edf6ffb85694c7efa31bf114", "relationship": "Concurrent output-borrowed common-factor batching; different scratch and query contract"} + ] +} diff --git a/research/native-shear-batch/verify.py b/research/native-shear-batch/verify.py new file mode 100644 index 0000000000..32b5190b7a --- /dev/null +++ b/research/native-shear-batch/verify.py @@ -0,0 +1,310 @@ +#!/usr/bin/env python3 +"""Exact private-only native shear batching. Python 3.10+, standard library.""" + +import collections +from fractions import Fraction +import itertools +import json +from pathlib import Path +import random + + +ROOT = Path(__file__).resolve().parent +MATRIX = (5, 30, 11, 14) # Target rows, source zero in the low bit. +TARGETS, SOURCES, PRIVATE = 4, 5, 9 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def span(vectors): + values = {0} + for vector in vectors: + values |= {v ^ vector for v in tuple(values)} + return values + + +def combination(mask, vectors): + value = 0 + for j, vector in enumerate(vectors): + if mask >> j & 1: + value ^= vector + return value + + +def fixture(): + rng = random.Random(52) + for attempt in range(1, 1001): + rows = tuple(rng.getrandbits(5) for _ in range(4)) + if len(span(rows)) == 8 and all(rows) and rows[0] | rows[1] | rows[2] | rows[3] == 31: + return rows, attempt + raise ValueError("fixture stopping rule exhausted") + + +def census(): + space = span(MATRIX) + weight = sum(v.bit_count() for v in MATRIX) + best = None + histogram = collections.Counter() + sample_sets = 0 + for samples in itertools.combinations(range(1 << SOURCES), 4): + if span([b ^ samples[0] for b in samples[1:]]) != space: + continue + sample_sets += 1 + coefficients = {combination(c, samples): c for c in range(16) if c.bit_count() % 2 == 0} + require(len(coefficients) == 8, "nonunique affine coordinates") + reads = tuple(sum(((coefficients[row] >> j) & 1) << i for i, row in enumerate(MATRIX)) + for j in range(4)) + read_cost = sum(a.bit_count() for a in reads) + for order in itertools.permutations(range(4)): + states = tuple(samples[j] for j in order) + source_cost = sum((a ^ b).bit_count() for a, b in zip((0,) + states, states + (0,))) + total = source_cost + read_cost + weight + histogram[total] += 1 + candidate = (total, states, tuple(reads[j] for j in order), source_cost, read_cost) + if best is None or candidate < best: + best = candidate + separate = None + basis_count = 0 + for basis in itertools.combinations(sorted(space - {0}), 3): + if span(basis) != space: + continue + basis_count += 1 + coefficients = {combination(c, basis): c for c in range(8)} + reads = tuple(sum(((coefficients[row] >> j) & 1) << i for i, row in enumerate(MATRIX)) + for j in range(3)) + total = 2 * sum(b.bit_count() for b in basis) + 2 * sum(a.bit_count() for a in reads) + weight + candidate = (total, basis, reads) + if separate is None or candidate < separate: + separate = candidate + return { + "sample_sets": sample_sets, + "ordered_schedules": sum(histogram.values()), + "xor_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "best": {"xor_scans": best[0], "source_states": list(best[1]), "target_reads": list(best[2]), + "source_scans": best[3], "private_read_scans": best[4], "direct_scans": weight, + "queries": 8, "affine_events": 48}, + "separate": {"bases": basis_count, "xor_scans": separate[0], "basis": list(separate[1]), + "target_reads": list(separate[2]), "queries": 12, "affine_events": 72}, + } + + +def emit(states, reads): + program = [] + previous = 0 + for state, targets in zip(states, reads): + for j in range(SOURCES): + if (previous ^ state) >> j & 1: + program.append(["xor", PRIVATE, TARGETS + j]) + program.append(["query", PRIVATE, 1]) + for i in range(TARGETS): + if targets >> i & 1: + program.append(["xor", i, PRIVATE]) + program.append(["query", PRIVATE, -1]) + previous = state + for j in range(SOURCES): + if previous >> j & 1: + program.append(["xor", PRIVATE, TARGETS + j]) + for i, row in enumerate(MATRIX): + for j in range(SOURCES): + if row >> j & 1: + program.append(["xor", i, TARGETS + j]) + return program + + +def column_census(): + """Cross-check by enumerating target bases and solving source coordinates.""" + columns = tuple(sum(((row >> j) & 1) << i for i, row in enumerate(MATRIX)) + for j in range(SOURCES)) + space = span(columns) + histogram = collections.Counter() + for basis in itertools.permutations(sorted(space - {0}), 3): + coordinates = {combination(c, basis): c for c in range(8)} + if len(coordinates) != 8: + continue + differences = tuple(sum(((coordinates[col] >> i) & 1) << j for j, col in enumerate(columns)) + for i in range(3)) + reads = basis + (basis[0] ^ basis[1] ^ basis[2],) + for offset in range(1 << SOURCES): + states = tuple(offset ^ d for d in differences) + (offset,) + travel = sum((a ^ b).bit_count() for a, b in zip((0,) + states, states + (0,))) + cost = travel + sum(a.bit_count() for a in reads) + sum(row.bit_count() for row in MATRIX) + histogram[str(cost)] += 1 + return dict(histogram) + + +def inverse(program): + return [[op, dst, -src if op == "query" else src] for op, dst, src in reversed(program)] + + +def symbolic(program, initial=None): + rows = [{(i, 0)} for i in range(PRIVATE + 1)] if initial is None else [set(r) for r in initial] + for op, dst, src in program: + if op == "query": + require(dst == PRIVATE and src in (-1, 1), "query outside private row") + rows[dst] = {(i, degree + src) for i, degree in rows[dst]} + elif op == "xor": + require((dst == PRIVATE and TARGETS <= src < PRIVATE) or + (0 <= dst < TARGETS and TARGETS <= src <= PRIVATE), "illegal VALUE operation") + rows[dst] ^= rows[src] + else: + raise ValueError("unknown operation") + return rows + + +def expected_symbolic(): + rows = [{(i, 0)} for i in range(PRIVATE + 1)] + for i, mask in enumerate(MATRIX): + for j in range(SOURCES): + if mask >> j & 1: + rows[i] ^= {(TARGETS + j, 0), (TARGETS + j, 1)} + return rows + + +def lowered(address, missing_child=False): + # PR521's chronological ADDRESS lowering, also recorded by PR677. + a = list(address) + a[2] -= a[0] + a[3] += a[0] + a[5] = (a[5] + 5 * a[0] - a[2] - a[3]) / 4 + if not missing_child: + a[0], a[5] = a[5], a[0] + a[2] += a[0] + a[3] -= a[0] + a[5] = -4 * a[5] + 3 * a[0] + a[2] + a[3] + return tuple(a) + + +def lowered_inverse(address): + a = list(address) + a[5] = (-a[5] + 3 * a[0] + a[2] + a[3]) / 4 + a[3] += a[0] + a[2] -= a[0] + a[0], a[5] = a[5], a[0] + a[5] = 4 * a[5] - 5 * a[0] + a[2] + a[3] + a[3] -= a[0] + a[2] += a[0] + return tuple(a) + + +def direct_address(a, modulus): + delta = (a[0] - a[2] - a[3] + a[5]) * pow(4, -1, modulus) + return tuple((x + s * delta) % modulus for x, s in zip(a, (1, 0, 1, -1, 0, -1))) + + +def permutation(modulus): + addresses = list(itertools.product(range(modulus), repeat=6)) + indexes = {a: i for i, a in enumerate(addresses)} + push = [indexes[direct_address(a, modulus)] for a in addresses] + require(len(set(push)) == len(addresses), "ADDRESS map not bijective") + for a, index in zip(addresses, push): + value = lowered(tuple(map(Fraction, a))) + reduced = tuple(int(v.numerator * pow(v.denominator, -1, modulus)) % modulus for v in value) + require(reduced == addresses[index], "lowering differs from direct ADDRESS map") + return push + + +def full_columns(program, push): + volume = len(push) + original = [[1 << (row * volume + col) for col in range(volume)] for row in range(PRIVATE + 1)] + rows = [list(row) for row in original] + pull = [0] * volume + for src, dst in enumerate(push): + pull[dst] = src + + def run(word): + for op, dst, src in word: + if op == "query": + mapping = pull if src == 1 else push + rows[dst] = [rows[dst][i] for i in mapping] + else: + rows[dst] = [a ^ b for a, b in zip(rows[dst], rows[src])] + + run(program) + for i in range(PRIVATE + 1): + for col in range(volume): + expected = original[i][col] + if i < TARGETS: + for j in range(SOURCES): + if MATRIX[i] >> j & 1: + expected ^= original[TARGETS + j][col] ^ original[TARGETS + j][pull[col]] + require(rows[i][col] == expected, "full-domain endpoint mismatch") + run(inverse(program)) + require(rows == original, "full-domain inverse mismatch") + return (PRIVATE + 1) * volume + + +def rejected(call, message): + try: + call() + except ValueError: + return + raise ValueError("negative control accepted: " + message) + + +def controls(program, result): + mutations = {} + first_read = next(i for i, e in enumerate(program) if e[0] == "xor" and e[2] == PRIVATE) + mutations["omit dirty compensation"] = program[:first_read] + program[first_read + 1:] + last_restore = max(i for i, e in enumerate(program) if e[0] == "xor" and e[1] == PRIVATE) + mutations["omit private restoration"] = program[:last_restore] + program[last_restore + 1:] + mutations["omit direct source term"] = program[:-1] + changed = [e[:] for e in program] + changed[0][2] = -1 + mutations["reverse first query"] = changed + changed = [e[:] for e in program] + changed[0][1] = 0 + mutations["query DATA target"] = changed + changed = [e[:] for e in program] + changed[-1][2] = TARGETS + ((changed[-1][2] - TARGETS + 1) % SOURCES) + mutations["wrong source"] = changed + for name, word in mutations.items(): + rejected(lambda word=word: require(symbolic(word) == expected_symbolic(), name), name) + bad_basis = tuple(Fraction(i == 0) for i in range(6)) + rejected(lambda: require(lowered(bad_basis, True) == lowered(bad_basis), "missing recursive child"), "missing recursive child") + corrupted = json.loads(json.dumps(result)) + corrupted["best"]["queries"] -= 1 + rejected(lambda: require(corrupted == result, "underpriced certificate"), "underpriced certificate") + # A semantically neutral pair must still pay both scans. + padded = program + [["xor", 0, TARGETS], ["xor", 0, TARGETS]] + require(symbolic(padded) == expected_symbolic(), "neutral positive control failed") + require(sum(e[0] == "xor" for e in padded) == result["best"]["xor_scans"] + 2, + "neutral pair was not charged") + return len(mutations) + 2 + + +def main(): + require(fixture() == (MATRIX, 6), "seed fixture mismatch") + result = census() + require(column_census() == result["xor_histogram"], "row/column census disagreement") + certificate = json.loads((ROOT / "CERTIFICATE.json").read_text()) + require(certificate["matrix_rows"] == list(MATRIX), "certificate target mismatch") + require(certificate["census"] == result, "certificate census mismatch") + best = result["best"] + program = emit(best["source_states"], best["target_reads"]) + require(certificate["program"] == program, "certificate program mismatch") + require(sum(e[0] == "query" for e in program) == best["queries"], "wrong query invoice") + require(sum(e[0] == "xor" for e in program) == best["xor_scans"], "wrong XOR invoice") + require(symbolic(program) == expected_symbolic(), "Laurent endpoint mismatch") + require(symbolic(inverse(program), symbolic(program)) == [{(i, 0)} for i in range(PRIVATE + 1)], + "Laurent inverse mismatch") + # Rational columns prove this fixed linear lowering for arbitrary ADDRESS values. + for j in range(6): + unit = tuple(Fraction(i == j) for i in range(6)) + delta = (unit[0] - unit[2] - unit[3] + unit[5]) / 4 + expected = tuple(x + s * delta for x, s in zip(unit, (1, 0, 1, -1, 0, -1))) + require(lowered(unit) == expected, "rational lowering mismatch") + require(lowered_inverse(expected) == unit, "inverse lowering mismatch") + push = permutation(3) + columns = full_columns(program, push) + # An independent full order-five ADDRESS census checks modular specialization. + require(len(permutation(5)) == 15625, "order-five coverage mismatch") + negative = controls(program, result) + print("PASS_NATIVE_SHEAR_BATCH schedules=5376 queries=12->8 xor_scans=36->30 " + f"columns={columns} negative_controls={negative} no_new_kappa") + + +if __name__ == "__main__": + main()