From dfba21817680dbbd1ca0455cae5e5e93c97710fb Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 13:32:49 +0000 Subject: [PATCH] feat(research): save eight Gaussian reader coefficient ADDs --- research/rational-reader-basis/PROOF.md | 91 ++++++++++++ research/rational-reader-basis/README.md | 103 ++++++++++++++ research/rational-reader-basis/SOURCES.json | 66 +++++++++ research/rational-reader-basis/TASK.json | 79 +++++++++++ research/rational-reader-basis/VERIFY.json | 37 +++++ research/rational-reader-basis/kernels.py | 120 ++++++++++++++++ research/rational-reader-basis/verify.py | 147 ++++++++++++++++++++ 7 files changed, 643 insertions(+) create mode 100644 research/rational-reader-basis/PROOF.md create mode 100644 research/rational-reader-basis/README.md create mode 100644 research/rational-reader-basis/SOURCES.json create mode 100644 research/rational-reader-basis/TASK.json create mode 100644 research/rational-reader-basis/VERIFY.json create mode 100644 research/rational-reader-basis/kernels.py create mode 100644 research/rational-reader-basis/verify.py diff --git a/research/rational-reader-basis/PROOF.md b/research/rational-reader-basis/PROOF.md new file mode 100644 index 0000000000..cccff692e2 --- /dev/null +++ b/research/rational-reader-basis/PROOF.md @@ -0,0 +1,91 @@ +# A rational shear removes eight coefficient instructions + +This scoped construction was produced by Nick Petalas. Apache-2.0. + +## Supplied boundary and changed hypothesis + +Ali Romman's PR #5646 supplies a 112-by-30 source kernel J and a +30-by-112 reader kernel D over Q[C2^9], after its ten published basis +operations. The source has 208 nonzero coefficients and the reader has +9,968. Its supplied boundary satisfies DJ=0. David Ganz's PR #5634 +supplies the four-shear borrowed-centre identity, and PR #5640 supplies +its grouped implementation and tariff. These are cited premises, not +results independently audited by this contribution. + +The alphabet here charges one coefficient ADD for each nonzero rational +translation coefficient. Its fixed rational coefficient and translation +are explicit. This is the same coefficient-support tariff as #5646; +this count does not price an arithmetic implementation, movement or tape. +The changed hypothesis is that the new basis shear may have denominator +five as well as a power of two. The published single-dyadic-ADD local +optimum does not exclude it. + +## Explicit change + +Number centre coordinates from zero. Set c=3/40 and + + E = I_30 + c e_5 e_4^T, + E^-1 = I_30 - c e_5 e_4^T, + D' = E D, J' = J E^-1. + +The off-diagonal matrix unit squares to zero, so the displayed inverse +is exact over Q and over Q[C2^9]. Only the following entries change: + + D'_5 = D_5 + (3/40) D_4, + J'_4 = J_4 - (3/40) J_5. + +Thus J'D'=JD and D'J'=E(DJ)E^-1=0. This holds as a formal kernel +identity, hence in the 512-address regular action and any representation +of these nine commuting involutions. Extra tensor axes, if present, +are spectators only. This does not assert an implementation at every +uniform algorithm size. + +For arbitrary data a and arbitrary dirty centre z, execute + + z += D' a + a += J' z + z -= D' a + a -= J' z. + +After the third step the centre is exactly its initial z because D'J'=0. +The last step therefore returns ((I+JD)a,z). No initial centre is zero, +discarded or granted independent productive-target credit. The old and +new words each have four rectangular shears and thirty borrowed fields. +The algebra proves the all-input statement; the literal payload replay +is a finite instruction-order control. + +## Strict coefficient bill + +The replay reconstructs the supplied factors from the exact pinned +response, inverse-character certificate, port directions and ten-step +basis. It then applies only the displayed new shear. It does not invoke +the predecessor verifier or repeat its rank/inverse/local-minimum audits. + +The changed source column still has twelve nonzero coefficients. +Reader row five loses four entries, changing from 892 to 888. All other +reader rows and source columns are unchanged. Consequently + + old: 2 (208 + 9968) = 20352 coefficient ADDs, + new: 2 (208 + 9964) = 20344 coefficient ADDs. + +The factor two counts a coefficient once in each sign of its shear. +The verifier executes and counts every one of these instructions in a +512-address payload, compares all output addresses and restores all +30 dirty fields. An exact comparison of every coefficient of the changed +two-term product proves the endpoint equality without sampling payloads. +Reversing the new basis recovers every supplied factor entry exactly. + +The common coefficient denominator changes from 960=2^6*3*5 to +1200=2^4*3*5^2. There is a larger power of five, although no new odd prime. +In both words, the largest absolute coefficient is one, the maximum +absolute row sum of J is 9/4, and that of D is 1036/15. These are endpoint +factor bounds, not a physical arithmetic-interior or error theorem. + +## Scope and stopping rule + +This is a finite explicit rational-kernel construction with an algebraic +change-of-basis proof. It improves the declared coefficient tariff by eight. +No global optimum is claimed, including among rational two-row changes. +The first strict improvement ends this investigation. No new kappa, +complete paid recursive invoice, selected-frontier update, arithmetic +precision/tape bound or complete multiplication theorem is supplied. diff --git a/research/rational-reader-basis/README.md b/research/rational-reader-basis/README.md new file mode 100644 index 0000000000..0a359f91db --- /dev/null +++ b/research/rational-reader-basis/README.md @@ -0,0 +1,103 @@ +# Eight fewer coefficient ADDs for the actual Gaussian reader + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: finite explicit rational-kernel construction with a scoped +algebraic proof. No new kappa. + +After Ali Romman's [PR #5646](https://github.com/CrocSwap/integer-mult-bounds/pull/5646) +basis, one further rational shear gives + + D5 += (3/40) D4, J4 -= (3/40) J5. + +It reduces the complete four-shear coefficient bill from 20,352 to 20,344. +There are 208 source coefficients and 9,964 reader coefficients, compared +with 208 and 9,968 before. The new word preserves every arbitrary dirty +centre and the supplied reader operator. It uses four shears and thirty +borrowed fields. [PROOF.md](PROOF.md) gives the all-input argument. + +This answers a small part of #5646's first Open next question. Its +single-dyadic-ADD local optimum permits this rational escape. The common +denominator changes from 960 to 1,200, introducing a second factor of five. +The largest coefficient remains one; the factor row-sum bounds remain +9/4 and 1036/15. A reduction in coefficient support does not establish a +reduction in bit operations, routing, precision, recursive cost or kappa. +The selected frontier and all five framework assumptions are unchanged. + +## Reproduction and evidence + +From the worktree root, with the Python 3.12 standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/rational-reader-basis/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/rational-reader-basis/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rational-reader-basis +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rational-reader-basis --check-source-history +``` + +Expected verifier status is `PASS_RATIONAL_READER_BASIS`. The JSON output +is generated from the replay and bound to package hashes; no stored receipt +is accepted as evidence. The source manifest binds the supplied factors, +port directions, inverse-character data and published basis. The replay +constructs these inputs to apply the new step; it does not run or audit +predecessor rank, inverse-certificate or local-optimum checks. + +The new checks compare every coefficient of the changed pair's kernel +product, the literal inverse basis and all untouched factor entries. A +literal 512-address payload executes and counts both complete words, +compares every data output and restores every dirty centre coordinate. +Five controls detect three losing coefficients, an omitted inverse source +update and a corrupted reader coefficient. The finite payload supports +instruction-order checking; the algebraic proof covers arbitrary inputs. + +## Open next questions + +1. Does the eight-instruction saving survive the extra factor of five in + one concrete rational-arithmetic caller? Start with a primitive that + implements these coefficients, including rounding, routing and storage. + Its complete physical price is missing. +2. Can one broader basis reduce coefficient support further without + increasing the complete physical bill? Start from the explicit changed + factors and a priced candidate. This package claims neither pairwise nor + global optimality and reserves no follow-up. + +The structured questions and changed card scope are in [TASK.json](TASK.json). + +## Credit and dependencies + +Ali Romman's #5646 supplies the actual factors, ten-operation basis and +broader-basis open question. David Ganz, @Dugongue, supplies +[PR #5634](https://github.com/CrocSwap/integer-mult-bounds/pull/5634), the +reader substitution and four-shear identity. Ali Romman's +[PR #5640](https://github.com/CrocSwap/integer-mult-bounds/pull/5640) +supplies the grouped tariff and dirty-bank boundary. +`kernels.py` reconstructs #5646's supplied factor formulas and basis with +that credit retained. Its original files and notices are unchanged. + +The underlying `centre-code-services` sources retain +`reciprocal-native-responses`, `native-centre-capture`, +`centre-metric-encoders`, PR #3133, #3148, #2588 and #2226 and their +individual contributor notices. This package cites their source identity +and boundary rather than asserting independent acceptance. The new result +is the explicit 3/40 shear and its eight-instruction saving. +Independent human and formal proof-kernel review are unclaimed. + +## Code bounds and verification limits + +The verifier is standard-library Python. There is no recursion, subprocess, +network operation, solver or mutable global research state. The fixed +matrix dimensions are 112 ports, 30 centre coordinates and 512 addresses; +each sparse kernel has at most 57,344 positions. There are exactly ten +supplied basis operations and one new operation. All input bytes are +SHA256 authenticated before decoding. Functions stay below sixty lines. +Runtime `require` checks remain enabled under optimization. + +Power-of-Ten rule 3 has a managed-runtime deviation. Python allocates +integers, fractions, dictionaries and lists while computing. The fixed +source dimensions and 16 MiB encoded/decoded source bounds constrain live +data, but no fixed allocation pool or byte-exact heap bound is claimed. +The literal replay uses a shared integer denominator at each of four +shears, avoiding per-address rational allocation. Interpreter/library +allocation remains outside direct inspection. Warning-strict normal and +optimized registered runs supply the available runtime diagnostics; +no unavailable static analyzer or formal kernel is claimed as run. diff --git a/research/rational-reader-basis/SOURCES.json b/research/rational-reader-basis/SOURCES.json new file mode 100644 index 0000000000..2d1bf68c54 --- /dev/null +++ b/research/rational-reader-basis/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/actual-gaussian-reader-tariff/BASIS.json", + "usage": "input", + "git_blob": "31923652cded9b0a131b84535536c43c83a01a66", + "sha256": "b21900ee6c5de7c7e5e77e99254f960c35a5f10a55972e27bad68ea9961278e5" + }, + { + "path": "research/actual-gaussian-reader-tariff/README.md", + "usage": "provenance", + "git_blob": "e5d49d12040e9f9079d73e6e5c93683e86f88db0", + "sha256": "32dc7b3e3262842eae8d18b800bf19d81890d163874e1db95de7f0375a238dd8" + }, + { + "path": "research/actual-gaussian-reader-tariff/verify.py", + "usage": "provenance", + "git_blob": "95faf1d5a5b5f59e061528307ff7b2e71cd2d4ae", + "sha256": "f11278e498805f94e24f7fdd25b0e84f8d8dbf768b438946574d2c414f669277" + }, + { + "path": "research/centre-code-services/frozen/lanes/new-core-transfer-20261017/low-displacement-20261020/run-normal/RESPONSE-PROGRAM.json", + "usage": "input", + "git_blob": "bcf3dd1d992257c2f933e6c1a0a3c3a27238f904", + "sha256": "5832788135e16c2427f8c746f251501621684a02ef88b0a14322056653dc2d7c" + }, + { + "path": "research/centre-code-services/frozen/lanes/history-encoding/independent-skeleton-20261018/fresh-three-child/FRESH-THREE-CHILD-PROGRAMS.json.gz", + "usage": "input", + "git_blob": "f552c66d6124c1fd84eacf4003638c82363bee81", + "sha256": "afc3aad86eb9b6da3027d3ac57eac1a2a766729dca0608e70e36d0554c8afc96" + }, + { + "path": "research/centre-code-services/frozen/root/RANK30-PHASE-SECTION-BLOCKS-20261020.json.gz", + "usage": "input", + "git_blob": "3695574aa24d06fd2d3b3a8ea923bfc3c3d0201a", + "sha256": "742c2a1907c61be01aa9a2f80df095ad21ad9608a43b38f7fb2ef7ee7ef6d994" + }, + { + "path": "research/actual-gaussian-reader-tariff/inputs/reader.md", + "usage": "provenance", + "git_blob": "3be2e5ecd836a3b9501be914d131f1ca580bd716", + "sha256": "028568bdcd33cf7daf7e9a754b5c686854d0825ca6a41d3c7362b13a9962b751" + }, + { + "path": "research/actual-gaussian-reader-tariff/inputs/tariff.md", + "usage": "provenance", + "git_blob": "df12205db8e6a49f0d7a7e08887a987391598e9e", + "sha256": "d84745ac51a83fbe56f3a3e88e63884cb2f97018f3ee374e7c520982789bd516" + } + ] +} diff --git a/research/rational-reader-basis/TASK.json b/research/rational-reader-basis/TASK.json new file mode 100644 index 0000000000..431edef111 --- /dev/null +++ b/research/rational-reader-basis/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "centre-path-sharing", + "question": "Can a specified persistent boundary eliminate a repeated centre operation in the current 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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Write a two-call input/output contract on the current source word, including arbitrary centre baselines and every later read. Price producer, retention, native alignment and restoration jointly. Historical 64-per-call and 1.90x figures are not current budgets. Stop if a missing consumer or restored-input obligation consumes the saving; reopen only with a changed legal boundary.", + "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": [ + "centre path", + "persistent boundary", + "dirty recoding" + ], + "existing_checks": [ + { + "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": "Explicit rational centre-basis shear reduces the actual Gaussian reader four-shear coefficient tariff by eight ADDs.", + "scope_change_reason": "PR5646 Open next question 1 asks for a broader basis. This scoped rational-kernel construction changes the dyadic single-ADD alphabet and does not claim a persistent-path or complete physical supplier improvement.", + "bottleneck_link": "Fewer actual reader coefficient instructions can help an ordinary caller, conditional on paying its rational arithmetic, routing, restoration and precision costs.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact strict coefficient-tariff improvement; do not extend the search or claim global optimality.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py: exact new shear, 20352 to 20344 coefficient ADDs, unchanged kernel product and dirty endpoints.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the coefficient-support improvement survive the extra factor of five in a physical caller?", + "why_it_matters": "Coefficient counts alone do not determine bit-operation or recursive cost.", + "first_step": "Price the explicit rational coefficients in one actual arithmetic primitive and caller.", + "blocked_by": "No complete rational arithmetic, routing, storage or precision implementation is supplied." + }, + { + "question": "Can a broader basis improve support and the complete physical bill further?", + "why_it_matters": "Only one explicit basis step is certified; no optimum is claimed.", + "first_step": "Start with these changed factors and one fully priced candidate.", + "blocked_by": "A complete physical objective is needed; no follow-up is reserved." + } + ] +} diff --git a/research/rational-reader-basis/VERIFY.json b/research/rational-reader-basis/VERIFY.json new file mode 100644 index 0000000000..4e672d9605 --- /dev/null +++ b/research/rational-reader-basis/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/actual-gaussian-reader-tariff/BASIS.json", + "research/centre-code-services/frozen/lanes/new-core-transfer-20261017/low-displacement-20261020/run-normal/RESPONSE-PROGRAM.json", + "research/centre-code-services/frozen/lanes/history-encoding/independent-skeleton-20261018/fresh-three-child/FRESH-THREE-CHILD-PROGRAMS.json.gz", + "research/centre-code-services/frozen/root/RANK30-PHASE-SECTION-BLOCKS-20261020.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact kernel-product invariance, literal inverse, full 512-address dirty word and five controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Same proof-relevant checks with optimization enabled." + } + ] +} diff --git a/research/rational-reader-basis/kernels.py b/research/rational-reader-basis/kernels.py new file mode 100644 index 0000000000..198963da53 --- /dev/null +++ b/research/rational-reader-basis/kernels.py @@ -0,0 +1,120 @@ +"""Reconstruct supplied reader factors, following Ali Romman PR5646. Apache-2.0. + +The factor formulas and published basis are predecessor inputs. This module +constructs their kernels for a new rational basis; it does not audit the source. +""" +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = 'research/centre-code-services/frozen/' +RESPONSE = SOURCE + ('lanes/new-core-transfer-20261017/low-displacement-20261020/' + 'run-normal/RESPONSE-PROGRAM.json') +DIRECTIONS = SOURCE + ('lanes/history-encoding/independent-skeleton-20261018/' + 'fresh-three-child/FRESH-THREE-CHILD-PROGRAMS.json.gz') +BLOCKS = SOURCE + 'root/RANK30-PHASE-SECTION-BLOCKS-20261020.json.gz' +BASIS = 'research/actual-gaussian-reader-tariff/BASIS.json' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def source_json(path): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + matches = [x for x in manifest['files'] if x['path'] == path] + require(len(matches) == 1, 'unique source pin') + raw = (ROOT / path).read_bytes() + require(len(raw) <= 16 * 1024 * 1024, 'source byte bound') + require(sha256(raw).hexdigest() == matches[0]['sha256'], 'source hash: ' + path) + if path.endswith('.gz'): + raw = gzip.decompress(raw) + require(len(raw) <= 16 * 1024 * 1024, 'decoded source byte bound') + return json.loads(raw) + + +def sparse_add(left, right, coefficient): + require(len(left) <= 57344 and len(right) <= 57344, 'kernel support bound') + result = {} + for key in left.keys() | right.keys(): + value = left.get(key, 0) + coefficient * right.get(key, 0) + if value: + result[key] = value + require(len(result) <= 57344, 'result support bound') + return result + + +def walsh(values): + require(len(values) == 512, 'nine-axis character table') + result = values[:] + for width in (1, 2, 4, 8, 16, 32, 64, 128, 256): + for first in range(0, 512, 2 * width): + for index in range(first, first + width): + left, right = result[index], result[index + width] + result[index], result[index + width] = left + right, left - right + return result + + +def inverse_times_reader(records, reader): + require(len(records) == 512 and len(reader) == 30, 'source matrix dimensions') + result = [] + for record in records: + inverse = [[Fraction(0)] * 30 for _ in range(30)] + for row in range(16): + for column in range(16): + inverse[row][column] = 60 * Fraction(record['large_inverse'][row][column]) + for row in range(16, 30): + inverse[row][row] = 60 / Fraction(record['small_diagonal'][row - 16]) + values = [[0] * 112 for _ in range(30)] + for row in range(30): + for column, coefficient in enumerate(inverse[row]): + if coefficient: + for port, value in reader[column].items(): + scaled = coefficient * value + require(scaled.denominator == 1, 'supplied inverse scale') + values[row][port] += int(scaled) + result.append(values) + return result + + +def supplied_factors(): + response = source_json(RESPONSE) + raw_u, raw_v = response['correction_U'], response['correction_V'] + require(len(raw_u) == 112 and len(raw_v) == 30, 'response dimensions') + source = [{int(k): Fraction(c) for k, c in row.items()} for row in raw_u] + reader = [{int(k): Fraction(c) for k, c in row.items()} for row in raw_v] + directions = [row['q'] for row in source_json(DIRECTIONS)['transfers']] + require(len(directions) == 112, 'port directions') + require(all(type(q) is int and 0 <= q < 512 for q in directions), 'direction range') + values = inverse_times_reader(source_json(BLOCKS)['characters'], reader) + kernels = [] + for row in range(30): + kernel = {} + for port in range(112): + spectrum = [values[0][row][port] * (1 - 2 * ((chi & directions[port]).bit_count() % 2)) + - values[chi][row][port] for chi in range(512)] + transformed = walsh(spectrum) + kernel.update({512 * port + shift: Fraction(c, 30720) + for shift, c in enumerate(transformed) if c}) + kernels.append(kernel) + columns = [{port: row[column] for port, row in enumerate(source) if column in row} + for column in range(30)] + operations = source_json(BASIS)['operations'] + require(len(operations) == 10, 'published basis length') + for left, right, coefficient in operations: + change_basis(columns, kernels, left, right, Fraction(coefficient)) + return columns, kernels, directions + + +def change_basis(source, reader, left, right, coefficient): + require(len(source) == len(reader) == 30, 'basis dimension') + require(type(left) is int and type(right) is int, 'basis index types') + require(0 <= left < 30 and 0 <= right < 30 and left != right, 'basis indices') + require(isinstance(coefficient, Fraction), 'exact basis coefficient') + reader[right] = sparse_add(reader[right], reader[left], coefficient) + source[left] = sparse_add(source[left], source[right], -coefficient) diff --git a/research/rational-reader-basis/verify.py b/research/rational-reader-basis/verify.py new file mode 100644 index 0000000000..5f9e4c5943 --- /dev/null +++ b/research/rational-reader-basis/verify.py @@ -0,0 +1,147 @@ +#!/usr/bin/env python3 +"""Verify a strict rational reader-basis improvement. Nick Petalas. Apache-2.0.""" +from fractions import Fraction +from hashlib import sha256 +import json +from math import lcm +from pathlib import Path +import sys + +from kernels import change_basis, require, supplied_factors + +HERE = Path(__file__).resolve().parent + + +def support_bill(source, reader): + return 2 * (sum(map(len, source)) + sum(map(len, reader))) + + +def metrics(source, reader): + denominator = lcm(*(c.denominator for row in source + reader for c in row.values())) + source_bound = max(sum(abs(row.get(port, 0)) for row in source) for port in range(112)) + reader_bound = max(sum(map(abs, row.values())) for row in reader) + return dict(source_coefficients=sum(map(len, source)), + reader_coefficients=sum(map(len, reader)), + four_shear_coefficient_adds=support_bill(source, reader), + common_denominator=denominator, + maximum_coefficient=str(max(abs(c) for row in source + reader for c in row.values())), + source_row_l1=str(source_bound), reader_row_l1=str(reader_bound)) + + +def pair_product(source, reader, directions): + result = {} + for column in (4, 5): + for output, coefficient in source[column].items(): + for packed, value in reader[column].items(): + port, shift = divmod(packed, 512) + key = (output, port, shift ^ directions[output]) + result[key] = result.get(key, 0) + coefficient * value + return {key: value for key, value in result.items() if value} + + +def apply_word(source, reader, directions, data, bank): + """Execute all coefficients with one exact integer scale per shear.""" + require(len(data) == 112 and len(bank) == 30, 'payload dimensions') + require(all(len(row) == 512 for row in data + bank), 'payload address width') + denominator = lcm(*(c.denominator for row in source + reader for c in row.values())) + centre, result = [row[:] for row in bank], [row[:] for row in data] + count, scale = 0, 1 + for sign in (1, -1): + gathered = [[denominator * value for value in row] for row in centre] + for row in range(30): + for packed, coefficient in reader[row].items(): + port, shift = divmod(packed, 512) + numerator = coefficient * denominator + require(numerator.denominator == 1, 'integer gather coefficient') + numerator = sign * int(numerator) + for address in range(512): + gathered[row][address] += numerator * result[port][address ^ shift] + count += 1 + centre = gathered + result = [[denominator * value for value in row] for row in result] + scale *= denominator + scattered = [[denominator * value for value in row] for row in result] + for row in range(30): + for port, coefficient in source[row].items(): + shift = directions[port] + numerator = coefficient * denominator + require(numerator.denominator == 1, 'integer scatter coefficient') + numerator = sign * int(numerator) + for address in range(512): + scattered[port][address] += numerator * centre[row][address ^ shift] + count += 1 + result = scattered + centre = [[denominator * value for value in row] for row in centre] + scale *= denominator + return result, centre, count, scale + + +def pair_controls(source, reader, directions, expected): + rejected = 0 + for coefficient in (Fraction(1, 40), Fraction(-3, 40), Fraction(3, 20)): + s, d = [row.copy() for row in source], [row.copy() for row in reader] + change_basis(s, d, 4, 5, coefficient) + require(support_bill(s, d) >= 20352, 'wrong coefficient must lose strict gain') + rejected += 1 + s, d = [row.copy() for row in source], [row.copy() for row in reader] + change_basis(s, d, 4, 5, Fraction(3, 40)) + s[4] = source[4].copy() + require(pair_product(s, d, directions) != expected, 'missing inverse source update') + rejected += 1 + d[5] = reader[5].copy() + s[4] = source[4].copy() + change_basis(s, d, 4, 5, Fraction(3, 40)) + key = min(d[5]) + d[5][key] += 1 + require(pair_product(s, d, directions) != expected, 'corrupted reader coefficient') + return rejected + 1 + + +def main(): + require(sys.version_info >= (3, 12), 'Python 3.12 or later') + source, reader, directions = supplied_factors() + before = metrics(source, reader) + expected = pair_product(source, reader, directions) + changed_s, changed_d = [row.copy() for row in source], [row.copy() for row in reader] + change_basis(changed_s, changed_d, 4, 5, Fraction(3, 40)) + after = metrics(changed_s, changed_d) + require(before['four_shear_coefficient_adds'] == 20352, 'supplied tariff') + require(after['four_shear_coefficient_adds'] == 20344, 'strict new tariff') + require((before['common_denominator'], after['common_denominator']) == (960, 1200), + 'changed common denominator') + require(all(m['maximum_coefficient'] == '1' and m['source_row_l1'] == '9/4' + and m['reader_row_l1'] == '1036/15' for m in (before, after)), + 'unchanged factor magnitude bounds') + require((len(reader[5]), len(changed_d[5])) == (892, 888), 'four cancellations') + require(pair_product(changed_s, changed_d, directions) == expected, 'all pair product coefficients') + require(all(changed_s[j] == source[j] for j in range(30) if j != 4), 'untouched source columns') + require(all(changed_d[j] == reader[j] for j in range(30) if j != 5), 'untouched reader rows') + change_basis(changed_s, changed_d, 4, 5, Fraction(-3, 40)) + require(changed_s == source and changed_d == reader, 'literal inverse basis') + controls = pair_controls(source, reader, directions, expected) + # One finite payload checks literal instruction order; the written conjugacy + # proof and coefficient identity cover arbitrary payloads and dirty banks. + data = [[((port + 7) * (address + 11)) % 17 - 8 + for address in range(512)] for port in range(112)] + bank = [[((row + 3) * (address + 5)) % 13 - 6 + for address in range(512)] for row in range(30)] + old_output, old_bank, old_count, old_scale = apply_word(source, reader, directions, data, bank) + change_basis(changed_s, changed_d, 4, 5, Fraction(3, 40)) + new_output, new_bank, new_count, new_scale = apply_word(changed_s, changed_d, directions, data, bank) + require(all(new_scale * old_output[p][x] == old_scale * new_output[p][x] + for p in range(112) for x in range(512)), 'literal data endpoints') + require(all(old_bank[j][x] == old_scale * bank[j][x] + and new_bank[j][x] == new_scale * bank[j][x] + for j in range(30) for x in range(512)), 'literal dirty restoration') + require((old_count, new_count) == (20352, 20344), 'executed instruction counts') + hashes = {name: sha256((HERE / name).read_bytes()).hexdigest() + for name in ('verify.py', 'kernels.py', 'SOURCES.json', 'TASK.json', 'VERIFY.json', 'README.md', 'PROOF.md')} + receipt = dict(status='PASS_RATIONAL_READER_BASIS', before=before, after=after, + operation=[4, 5, '3/40'], address_count=512, dirty_fields=30, + compared_pair_product_coefficients=len(expected), rejection_controls=controls, + literal_payloads=1, package_sha256=hashes) + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()