From 264454acd8b94d926d42e94f3cb83ecd00a6daa9 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 14 Oct 2026 17:01:23 +0100 Subject: [PATCH] feat(research): certify swapped-chart source-code growth --- research/source-code-chart-order/ARCHIVE.json | 14 + research/source-code-chart-order/README.md | 230 ++++++++++++++ research/source-code-chart-order/RESULT.json | 68 ++++ research/source-code-chart-order/SOURCES.json | 30 ++ research/source-code-chart-order/TASK.json | 119 +++++++ research/source-code-chart-order/VERIFY.json | 21 ++ .../source-code-chart-order/test_verify.py | 114 +++++++ research/source-code-chart-order/verify.py | 297 ++++++++++++++++++ 8 files changed, 893 insertions(+) create mode 100644 research/source-code-chart-order/ARCHIVE.json create mode 100644 research/source-code-chart-order/README.md create mode 100644 research/source-code-chart-order/RESULT.json create mode 100644 research/source-code-chart-order/SOURCES.json create mode 100644 research/source-code-chart-order/TASK.json create mode 100644 research/source-code-chart-order/VERIFY.json create mode 100644 research/source-code-chart-order/test_verify.py create mode 100644 research/source-code-chart-order/verify.py diff --git a/research/source-code-chart-order/ARCHIVE.json b/research/source-code-chart-order/ARCHIVE.json new file mode 100644 index 0000000000..bddf364a2d --- /dev/null +++ b/research/source-code-chart-order/ARCHIVE.json @@ -0,0 +1,14 @@ +{ + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "members": { + "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz": { + "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c" + }, + "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz": { + "sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "payload_sha256": "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3" + } + } +} diff --git a/research/source-code-chart-order/README.md b/research/source-code-chart-order/README.md new file mode 100644 index 0000000000..2e7d12eab5 --- /dev/null +++ b/research/source-code-chart-order/README.md @@ -0,0 +1,230 @@ +# Swapping source-code charts destroys periodic restoration + +Scoped source-algebra obstruction. No new supplier or kappa is claimed. + +Ali Romman's [PR1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862) +constructs a valid order-six source code. It explicitly leaves changing-chart +restoration open. On the actual selected 112-port query matrix, alternating its +compensation and query port sets gives an **infinite-order** product. The product +has a real eigenvalue strictly between 170 and 171. Repeating this pair cannot +restore every source, even after arbitrarily many repetitions. + +This is a concrete, quantitative witness, not a correction to PR1862. David +Arias's [PR1973](https://github.com/CrocSwap/integer-mult-bounds/pull/1973) +uses these same two admissible charts to check a different statement, the +three-chart F-B-F exchange defect. Its all-length winding theorem concerns a +fixed code. This package instead derives the repeated source-only pair's +characteristic polynomial and growth. It imports neither predecessor's code. + +## Exact instance and result + +The selected source has an 8 by 112 query matrix R, with + +```text +K = R^T/4, RK = 14 I_8, +A = [0,7,20,27,36,46,57,111], +T = [21,37,47,76,81,87,92,110]. +``` + +Let P and S be K restricted to its A and T rows respectively. Let L_A and L_T +be R restricted to those columns. Both eight-port minors are orthogonal with +squared norm four. Thus + +```text +RP = RS = L_A P = L_T S = L_A K = L_T K = I_8, +L_A S = L_T P = 0. +``` + +PR1862's ordered code for a compensation section P and logger L is + +```text +Z = K - P(RK-I), Q = R-L, +G(P,L) = (I-PL)(I+ZQ) = I+ZQ-PR. +``` + +Set G_A = G(P,L_T), G_T = G(S,L_A), and C = G_T G_A. Products act on +column vectors, so G_A executes first. Both charts meet exactly the predecessor's +algebraic hypotheses RP=I, LK=I and LP=0. + +The checked full characteristic polynomial is + +```text +char_C(t) = (t-1)^88 (t^3-171t^2+27t-1)^8. +``` + +In particular, trace C is 1456. Each individual code has exact order six, +whereas C has infinite order over Q and Q(i). The same-chart pair G_A G_A has +order three and provides a positive restoration control. + +## Proof by three sections + +Put U = K-P-S. The three sections satisfy + +```text +L_A U = L_T U = 0, RU = 12 I_8. +``` + +The 112 by 24 matrix E = [P S U] therefore has the left inverse + +```text +D = stack(L_A, L_T, (R-L_A-L_T)/12), DE = I_24. +``` + +Every source splits uniquely into a vector in ker D and a vector E(u,v,z). +The complement has dimension 88. Both codes fix it pointwise because each of +R, L_A and L_T vanishes there. On the section coordinates, the two codes act +by the following matrices tensored with I_8: + +```text +H_A = [[-12, -1, -156], + [ 1, 1, 12], + [ 1, 0, 13]], + +H_T = [[ 1, 1, 12], + [ -1, -12, -156], + [ 0, 1, 13]]. +``` + +For example, G_A P = -12P+S+U, G_A S = -P+S, and +G_A U = -156P+12S+13U. These follow directly from the ordered code formula. +Swapping P and S gives H_T. Their product is + +```text +H_T H_A = [[ 1, 0, 12], + [-156, -11, -2016], + [ 14, 1, 181]]. +``` + +Its trace is 171, sum of principal two by two minors is 27, and determinant +is one. Its characteristic polynomial is p(t)=t^3-171t^2+27t-1. The direct-sum +decomposition proves the displayed full characteristic polynomial and +trace C = 88+8*171 = 1456. + +The integer signs p(170)=-24311 and p(171)=4616 put a real eigenvalue lambda +strictly between 170 and 171 by continuity. A finite-order matrix has only +roots of unity as eigenvalues, so C cannot have finite order. For any induced +real operator norm, ||C^k|| is at least lambda^k, hence greater than 170^k for +positive k. This describes worst-case growth in the source-only port algebra. +It is not a physical precision bill or a claim that every rational source +vector expands at this rate. + +There is also a short order obstruction independent of the cubic calculation. +For a finite-order 112-dimensional matrix in characteristic zero, each +eigenvalue has modulus one, so the absolute value of its trace is at most 112. +The measured exact trace 1456 already excludes finite order. + +## Reproduce and evidence + +From the repository root, Python 3.10 or later, standard library only: + +```sh +python3 -I -B research/source-code-chart-order/verify.py +python3 -I -O -B research/source-code-chart-order/verify.py +python3 -I -B research/source-code-chart-order/test_verify.py +python3 scripts/research_package.py --package research/source-code-chart-order --check-only +``` + +Expected verifier line: + +```text +PASS_SOURCE_CODE_CHART_ORDER orders=6,6,infinite trace=1456 eigenvalue=170..171 columns=336 controls=4 no_new_kappa +``` + +Standard and optimized registered replays pass, including the source pins, +336 column comparisons, four semantic controls and eight focused tests. +All 45 research-workflow tests pass with no skips; bytecode compilation with +`-Wall` also passes. Exact commands and unrun obligations are in TASK.json. + +The registered hook uses Python 3.12: + +```sh +python3.12 scripts/research_package.py --package research/source-code-chart-order +``` + +The verifier authenticates the selected PR1094 archive and two exact members +before parsing. It propagates all 112 source columns to the forward centre +cut. It does not replay helper or private-input columns. It independently +constructs the two 112 by 112 codes, proves DE=I, checks both section actions +and the fixed complement, and compares the matrix calculations with a +separate ordered-factor column interpreter in 336 cases. All checks remain +active under `-O`. + +Four semantic controls detect a broken minor, overlapping compensation/logger +supports, a changed section basis and a wrong active coefficient. The focused +tests also reject an archive mutation and a forged receipt, and exercise CLI +failure behavior. `RESULT.json` records the deterministic result. Default +replay is read-only; `--write` regenerates only this package's receipt. + +[SOURCES.json](SOURCES.json) records Git blobs and hashes at main +`d48fcf5eedae9d8e2296598a1868a0b1a37a83f1`. +[ARCHIVE.json](ARCHIVE.json) additionally pins raw members and decompressed +payloads. These payloads equal PR1862's historical PR1042 inputs. The query +matrix digest also equals PR1973's independently extracted digest. +The archive, selected record, frozen predecessors and `upstream/` are unchanged. + +## Scope and task selection + +Chooser seed `4a0e6caaf3f4e5d0026f7998e13a6835` proposed +`complex-new-helper-inventory` under priority revision 3. The scope changed +to a restoration audit of a proposed source-code interface. It does not meet +the original card's new-inventory construction gate. The binding complex +supplier motivates the question, but this is a scoped obstruction, not an +exponent improvement. + +The card's ceiling positive control and ideal levers were run. Centre-free +work has a favorable 2.80-times ceiling before the source coding, chart +routing, restoration and other costs of realizing it. This audit rejects only +periodic restoration by repetitions of the specific pair C. It supplies no +candidate invoice and credits no omitted work as a realized saving. + +[The coordination claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1976) +records the scope and overlap checks. A fully paginated refresh covered +404 open PRs and 625 Discussion records without warnings. Coverage timestamps +and pinned predecessor heads are in TASK.json. This is not a code-diff-wide +search or a global novelty certificate. + +No physical route between these charts is constructed. Abstract admissibility +does not establish legal native-frame reads or equivalence to a stage in the +nine-call controller. In particular, the result does not rule out coherent +conjugate transport, explicit inverse codes, different chart sequences, +port-dependent repairs, changed endpoints or PR1969's joint-query interface. +The inherited all-size, native/compiler, hosting, precision/tape and analytic +obligations remain open. No full `make frontier1094-verify`, native recipe +replay, controller admission or proof-assistant verification is claimed. + +## Open next questions + +Can an actual paid stage transport replace this raw swapped-chart product +with a restoring source transition? First derive one transport U from the +controller and check the full-source map G_T^-1 U G_A, not only its query +compression. Then price all reads, frame moves, inverse work and endpoint +restoration. The missing typed native transport and complete invoice block +any supplier conclusion. The structured question is in TASK.json. + +## Verification design and credit + +Power-of-ten inspection found no recursion in the new checker. Every algebra +loop is bounded by the pinned 112-port/8-query dimensions. The source loop is +capped at 30,000 events, files at 8 MiB, and archive member count at 2,000. +Functions are below 60 physical lines; failures propagate as exceptions with +no writes on ordinary replay. Python's rational/dictionary allocation and +unittest's bounded method dispatch are deviations from rules 3 and 9. Pinned +source and matrix sizes bound live state. Tests own and discard their temporary +directories, and subprocesses have 30-second timeouts. If these scripts become +runtime components, replace them with fixed-capacity storage and direct calls. +`-Wall`, bytecode compilation and standard/optimized replays check the +interpreted code; no static type analysis is claimed. + +Credit Ali Romman for PR1862's source-code construction and its explicit +changing-chart warning, inspected at +`bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f`. Credit David Arias for PR1973's +fixed-code winding and universal F-B-F obstruction, inspected at +`165f08a694b26b0f4c521ce5e1132ede0b7362a2`. Those are valid predecessor +results, not claims introduced here. + +The selected local source and assembly retain Jeremy Kothe's PR1042 and +mutable-leaver work, Rohan Arun's PR1094 and k8/slot work, Hao Yan's controller, +Chafik Boukhalfa's frame work, icekylinx and the earlier gauge44/split-centres +contributors. Original notices remain in the unchanged archive and source +packages. No predecessor executable or text is vendored. Nick Petalas. +New work is Apache-2.0 under the repository license. diff --git a/research/source-code-chart-order/RESULT.json b/research/source-code-chart-order/RESULT.json new file mode 100644 index 0000000000..48db49fcfc --- /dev/null +++ b/research/source-code-chart-order/RESULT.json @@ -0,0 +1,68 @@ +{ + "status": "PASS_SOURCE_CODE_CHART_ORDER", + "query_sha256": "70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213", + "ports": 112, + "query_rank": 8, + "A": [ + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "T": [ + 21, + 37, + 47, + 76, + 81, + 87, + 92, + 110 + ], + "individual_chart_order": 6, + "pair_fixed_dimension": 88, + "pair_active_dimension": 24, + "pair_action": [ + [ + "1", + "0", + "12" + ], + [ + "-156", + "-11", + "-2016" + ], + [ + "14", + "1", + "181" + ] + ], + "pair_characteristic_polynomial_low_to_high": [ + -1, + 27, + -171, + 1 + ], + "full_characteristic_polynomial": "(t-1)^88 * (t^3-171*t^2+27*t-1)^8", + "pair_trace": 1456, + "pair_order": "infinite over Q and Q(i)", + "real_eigenvalue_interval": [ + 170, + 171 + ], + "polynomial_at_endpoints": [ + -24311, + 4616 + ], + "column_oracle_cases": 336, + "semantic_failure_controls": 4, + "same_chart_pair_order": 3, + "scope": "Source-only port algebra, not native chart transport or a complete supplier.", + "selected_frontier_changed": false +} diff --git a/research/source-code-chart-order/SOURCES.json b/research/source-code-chart-order/SOURCES.json new file mode 100644 index 0000000000..85a830f9b7 --- /dev/null +++ b/research/source-code-chart-order/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "d48fcf5eedae9d8e2296598a1868a0b1a37a83f1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "provenance", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ] +} diff --git a/research/source-code-chart-order/TASK.json b/research/source-code-chart-order/TASK.json new file mode 100644 index 0000000000..fab6558f9f --- /dev/null +++ b/research/source-code-chart-order/TASK.json @@ -0,0 +1,119 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 3, + "base_commit": "d48fcf5eedae9d8e2296598a1868a0b1a37a83f1", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove and independently replay the source-only order and growth of two alternating admissible PR1862 charts with A and T swapped, on the selected 112-port query matrix.", + "scope_change_reason": "Nearby helper and decoder construction tasks already have substantial coverage. Source restoration remains a missing implication for the changed source-code interface. This is a scoped obstruction and does not meet the original card's new-inventory construction gate.", + "bottleneck_link": "The complex supplier binds. The centre-free lever has an ideal 2.80-times ceiling before realizing coding, routing and restoration. This result rejects periodic restoration of one specific swapped-chart pair, without claiming a realized gain.", + "budget_minutes": 60, + "stop_rule": "Stop after exact source extraction, a three-section proof and full source-column crosscheck of the two swapped charts. Do not extend to a controller search or native admission.", + "outcome": "negative-result", + "evidence": "README.md proof and RESULT.json; verify.py checks the selected source, section decomposition and 336 factor-oracle cases; test_verify.py supplies literal expectations and CLI mutation controls.", + "author": "Nick Petalas", + "ai_assistance": "Not recorded under account publication rules.", + "selection_seed": "4a0e6caaf3f4e5d0026f7998e13a6835", + "original_scope_key": "5868e5281a1e63d41a22", + "actual_scope_key": "selected-R112-swapped-A-T-source-code-product-order", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1976", + "predecessors": [ + { + "pr": 1862, + "author": "Ali Romman", + "head": "bb29ea73ad9be9a0c3d53cdcb1d22b2ee9ffe42f", + "retained_result": "Valid fixed-chart order-six source code and native identity transfers; changing-chart periodicity explicitly not claimed." + }, + { + "pr": 1973, + "author": "David Arias", + "head": "165f08a694b26b0f4c521ce5e1132ede0b7362a2", + "retained_result": "All-length fixed-code controller winding and universal three-chart F-B-F defect; same swapped charts used only as finite rank witnesses." + }, + { + "pr": 1969, + "author": "Ali Romman", + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "retained_result": "Joint-query local interface and selected-only recovery obstruction, outside this source-only product class." + } + ], + "entry_overlap": { + "live_open_prs": 542, + "discussion_snapshot_records": 605, + "discussion_snapshot_at": "2026-10-14T15:42:53.836381+00:00", + "complete_pagination": true, + "limitation": "Entry search covered paginated open PR titles, bodies and heads plus a Discussion snapshot. No code-diff-wide novelty claim." + }, + "submission_overlap": { + "checked_at": "2026-10-14T16:42:33.333804+00:00", + "live_open_prs": 404, + "open_pr_snapshot_at": "2026-10-14T16:41:22.219282+00:00", + "discussion_snapshot_records": 625, + "discussion_snapshot_at": "2026-10-14T16:42:33.263821+00:00", + "complete_pagination": true, + "warnings": [], + "result": "Exact scope terms matched only this package, its PR and its coordination claim. Broader task-card matches remain overlap leads, not evidence of novelty.", + "command": "python3.12 -B scripts/find_overlap.py --task complex-new-helper-inventory 'swapped chart' 'chart order' 'source-code-chart-order' --refresh --limit 200 --json", + "limits": "No all-diff search or global novelty certificate; closed work covered by local package notes and ledger." + }, + "registered_validation": { + "environment": "CPython 3.12.15; standard library only", + "commands": [ + "python3.12 -B scripts/research_package.py --package research/source-code-chart-order", + "python3.12 -I -O -B scripts/research_package.py --package research/source-code-chart-order", + "python3.12 -B -m unittest discover -s tests -p 'test_research_*.py'", + "python3.12 -Wall -m py_compile research/source-code-chart-order/verify.py research/source-code-chart-order/test_verify.py", + "python3.12 -B scripts/research_package.py --package research/source-code-chart-order --check-only", + "git diff --check" + ], + "results": "Standard and optimized registered replays pass, each including the 336 source-column comparisons, four semantic controls and eight focused tests. All 45 research-workflow tests pass with no skips; compilation and metadata/source pins pass. Replay does not modify package files.", + "unchanged": "Verifier, tests, VERIFY.json, archive/source pins, exact receipt and shared launcher version guard.", + "not_run": "Full selected cold replay, native routing, hosting/precision admission and proof-assistant verification not run." + }, + "open_questions": [ + { + "question": "Can an actual paid native stage transport replace the raw swapped-chart product with a restoring source transition?", + "why_it_matters": "Without full-source restoration the source-code approach cannot be adopted merely from fixed-chart periodicity or query transport.", + "first_step": "Derive one typed transport U and check the complete source map G_T^-1 U G_A, then charge reads, frame moves, inverses and endpoint restoration.", + "blocked_by": "No native transport or complete invoice is supplied for these two abstract port charts." + } + ] +} diff --git a/research/source-code-chart-order/VERIFY.json b/research/source-code-chart-order/VERIFY.json new file mode 100644 index 0000000000..4ed6f1d164 --- /dev/null +++ b/research/source-code-chart-order/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-O", "-B", "-Wall", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Pinned query extraction, both order-six codes, full section action, infinite-order product polynomial, all 336 ordered-factor column cases and four semantic controls." + }, + { + "argv": ["{python}", "-I", "-B", "-Wall", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Eight focused test groups with literal algebra results, standard/optimized real CLI, archive and receipt mutation rejection, cut/register boundaries, and unknown-option failure." + } + ] +} diff --git a/research/source-code-chart-order/test_verify.py b/research/source-code-chart-order/test_verify.py new file mode 100644 index 0000000000..5621bd6809 --- /dev/null +++ b/research/source-code-chart-order/test_verify.py @@ -0,0 +1,114 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Literal algebra expectations and real CLI failure controls.""" +from pathlib import Path +import json +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify + +ARCHIVE = verify.ROOT / "research/community-frontier1094-audit/selected-replay.tar.gz" + + +class ChartOrderTests(unittest.TestCase): + def command(self, package=HERE, archive=ARCHIVE, optimized=False, extra=()): + args = [sys.executable, "-I", "-B", "-Wall"] + if optimized: + args.append("-O") + args += [str(package / "verify.py"), "--archive", str(archive), *extra] + return subprocess.run(args, capture_output=True, text=True, timeout=30) + + def test_real_cli_standard_and_optimized(self): + expected = ("PASS_SOURCE_CODE_CHART_ORDER orders=6,6,infinite trace=1456 " + "eigenvalue=170..171 columns=336 controls=4 no_new_kappa\n") + before = (HERE / "RESULT.json").read_bytes() + for optimized in (False, True): + with self.subTest(optimized=optimized): + result = self.command(optimized=optimized) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(result.stdout, expected) + self.assertEqual(result.stderr, "") + self.assertEqual((HERE / "RESULT.json").read_bytes(), before) + + def test_literal_pair_and_cubic(self): + pair = verify.multiply(verify.small_action(True), verify.small_action()) + self.assertEqual(pair, [{0: 1, 2: 12}, {0: -156, 1: -11, 2: -2016}, + {0: 14, 1: 1, 2: 181}]) + self.assertEqual(verify.polynomial3(pair), [-1, 27, -171, 1]) + self.assertEqual(verify.evaluate([-1, 27, -171, 1], 170), -24311) + self.assertEqual(verify.evaluate([-1, 27, -171, 1], 171), 4616) + self.assertEqual(verify.determinant3(pair), 1) + + def test_individual_order_and_same_chart_return(self): + unit = [{0: 1}, {1: 1}, {2: 1}] + for swapped in (False, True): + action = verify.small_action(swapped) + power = unit + for exponent in range(1, 7): + power = verify.multiply(action, power) + self.assertEqual(power == unit, exponent == 6) + pair = verify.multiply(action, action) + self.assertEqual(verify.polynomial3(pair), [-1, 0, 0, 1]) + self.assertEqual(verify.multiply(verify.multiply(pair, pair), pair), unit) + + def test_query_source_and_section_dimensions(self): + result = verify.run(ARCHIVE) + self.assertEqual(result["query_sha256"], + "70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213") + self.assertEqual(result["pair_trace"], 1456) + self.assertEqual(result["pair_fixed_dimension"], 88) + self.assertEqual(result["pair_active_dimension"], 24) + self.assertEqual(result["semantic_failure_controls"], 4) + + def test_corrupt_archive_fails_before_parse(self): + with tempfile.TemporaryDirectory() as directory: + bad = Path(directory) / "bad.tar.gz" + raw = bytearray(ARCHIVE.read_bytes()) + raw[10] ^= 1 + bad.write_bytes(raw) + result = self.command(archive=bad, optimized=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn("archive pin mismatch", result.stderr) + self.assertEqual(result.stdout, "") + + def test_forged_receipt_is_rejected_without_rewrite(self): + with tempfile.TemporaryDirectory() as directory: + package = Path(directory) / "package" + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + path = package / "RESULT.json" + data = json.loads(path.read_text()) + data["pair_trace"] = 112 + path.write_text(json.dumps(data)) + forged = path.read_bytes() + result = self.command(package=package, optimized=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn("receipt mismatch", result.stderr) + self.assertEqual(path.read_bytes(), forged) + self.assertEqual(result.stdout, "") + + def test_ambiguous_cut_and_register_bounds(self): + word = {"v": 112, "R": 480, "h": 9, "centers": list(range(413, 421))} + for program in ([], [["phase", "centers"], ["phase", "centers"]]): + with self.assertRaisesRegex(ValueError, "ambiguous centre cut"): + verify.extract_query(word, program) + for port in (("L", 704), ("C", 8), ("L", -1), ("other", 0), ("L", True)): + with self.assertRaises(ValueError): + verify.register(port) + self.assertEqual(verify.register(("L", 703)), 703) + self.assertEqual(verify.register(("C", 7)), 711) + + def test_unknown_cli_option_is_rejected(self): + result = self.command(extra=("--unknown-option",)) + self.assertEqual(result.returncode, 2) + self.assertIn("unrecognized arguments", result.stderr) + self.assertEqual(result.stdout, "") + + +if __name__ == "__main__": + unittest.main() diff --git a/research/source-code-chart-order/verify.py b/research/source-code-chart-order/verify.py new file mode 100644 index 0000000000..e8c2b09d73 --- /dev/null +++ b/research/source-code-chart-order/verify.py @@ -0,0 +1,297 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact source-only audit of the two swapped PR1862 charts. + +No predecessor executable is imported. Native frames and routing are outside +this check. Default execution reads sources and compares the saved receipt. +""" +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import argparse +import gzip +import json +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +A = (0, 7, 20, 27, 36, 46, 57, 111) +T = (21, 37, 47, 76, 81, 87, 92, 110) +N, RANK = 112, 8 +MAX_BYTES = 8 * 1024 * 1024 + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def identity(n): + return [{i: Q(1)} for i in range(n)] + + +def add(a, b, scale=1): + require(len(a) == len(b), "matrix row mismatch") + result = [row.copy() for row in a] + for target, source in zip(result, b): + for j, value in source.items(): + updated = target.get(j, 0) + scale * value + if updated: + target[j] = updated + else: + target.pop(j, None) + return result + + +def multiply(a, b): + result = [] + for row in a: + target = {} + for k, value in row.items(): + for j, other in b[k].items(): + target[j] = target.get(j, 0) + value * other + result.append({j: x for j, x in target.items() if x}) + return result + + +def scaled(a, scale): + return [{j: scale * x for j, x in row.items() if scale * x} for row in a] + + +def transpose(a, columns): + return [{i: row[j] for i, row in enumerate(a) if j in row} + for j in range(columns)] + + +def selected(a, ports): + return [{j: x for j, x in row.items() if j in ports} for row in a] + + +def load_sources(archive_path): + pins = json.loads((HERE / "ARCHIVE.json").read_text(encoding="utf-8")) + require(archive_path.stat().st_size <= MAX_BYTES, "archive size limit") + require(sha256(archive_path.read_bytes()).hexdigest() == pins["sha256"], + "archive pin mismatch") + objects = {} + with tarfile.open(archive_path, "r:gz") as archive: + members = archive.getmembers() + require(len(members) <= 2000, "archive member limit") + for name, pin in pins["members"].items(): + matches = [m for m in members if m.name == name] + require(len(matches) == 1 and matches[0].isfile(), "member ambiguity") + member = matches[0] + require(member.size <= MAX_BYTES, "member size limit") + stream = archive.extractfile(member) + require(stream is not None, "missing member stream") + with stream: + raw = stream.read(MAX_BYTES + 1) + require(len(raw) == member.size, "partial member read") + require(sha256(raw).hexdigest() == pin["sha256"], "member pin mismatch") + payload = gzip.decompress(raw) + require(len(payload) <= MAX_BYTES, "payload size limit") + require(sha256(payload).hexdigest() == pin["payload_sha256"], + "payload pin mismatch") + objects[Path(name).name] = json.loads(payload) + return objects + + +def extract_query(word, program): + """Propagate only the 112 source columns to the unique centre cut.""" + require((word["v"], word["R"], word["h"]) == (112, 480, 9), "geometry") + require(len(program) <= 30000, "program event limit") + cut = ["phase", "centers"] + require(program.count(cut) == 1, "ambiguous centre cut") + require(len(word["centers"]) == 8 and len(set(word["centers"])) == 8, + "centre register count") + rows = identity(N) + [{} for _ in range(712 - N)] + for event in program[:program.index(cut)]: + if event[0] != "scalar": + continue + op = event[1] + target = register(op[1]) + if op[0] == "clear": + rows[target] = {} + elif op[0] == "copy": + rows[target] = rows[register(op[2])].copy() + elif op[0] == "scale": + rows[target] = scaled([rows[target]], Q(op[2], op[3]))[0] + else: + require(op[0] == "add", "unknown scalar operation") + rows[target] = add([rows[target]], [rows[register(op[2])]], + Q(op[3], op[4]))[0] + return [rows[c] for c in word["centers"]] + + +def register(port): + kind, index = port + require(type(index) is int, "register index type") + require((kind == "L" and 0 <= index < 704) or + (kind == "C" and 0 <= index < 8), "register bounds") + return index + (704 if kind == "C" else 0) + + +def chart(R, K, P, L): + unit = identity(RANK) + require(multiply(R, P) == unit, "RP != I") + require(multiply(L, K) == unit, "LK != I") + require(not any(multiply(L, P)), "LP != 0") + Z = add(K, multiply(P, add(multiply(R, K), unit, -1)), -1) + query = add(R, L, -1) + G = add(add(identity(N), multiply(Z, query)), multiply(P, R), -1) + require(not any(multiply(query, Z)), "QZ != 0") + return {"G": G, "P": P, "L": L, "Z": Z, "Q": query} + + +def apply_factors(code, vector): + """Separate column oracle: apply I+ZQ, then I-PL, in that order.""" + query = [sum(x * vector[j] for j, x in row.items()) for row in code["Q"]] + middle = [value + sum(x * query[j] for j, x in row.items()) + for value, row in zip(vector, code["Z"])] + logged = [sum(x * middle[j] for j, x in row.items()) for row in code["L"]] + return [value - sum(x * logged[j] for j, x in row.items()) + for value, row in zip(middle, code["P"])] + + +def small_action(swapped=False): + dense = [[-12, -1, -156], [1, 1, 12], [1, 0, 13]] + if swapped: + dense = [[1, 1, 12], [-1, -12, -156], [0, 1, 13]] + return [{j: Q(x) for j, x in enumerate(row) if x} for row in dense] + + +def lift(a): + """Three sections, each containing the same eight query coordinates.""" + return [{RANK * j + k: x for j, x in row.items()} + for row in a for k in range(RANK)] + + +def determinant3(a): + x = [[row.get(j, 0) for j in range(3)] for row in a] + return (x[0][0] * (x[1][1]*x[2][2] - x[1][2]*x[2][1]) + - x[0][1] * (x[1][0]*x[2][2] - x[1][2]*x[2][0]) + + x[0][2] * (x[1][0]*x[2][1] - x[1][1]*x[2][0])) + + +def polynomial3(a): + trace = sum(row.get(i, 0) for i, row in enumerate(a)) + square = multiply(a, a) + second = (trace**2 - sum(row.get(i, 0) for i, row in enumerate(square))) / 2 + return [-determinant3(a), second, -trace, Q(1)] + + +def evaluate(coefficients, x): + value = Q(0) + for coefficient in reversed(coefficients): + value = value * x + coefficient + return value + + +def verify_actions(codes, E, left): + require(multiply(left, E) == identity(24), "active sections dependent") + projection = multiply(E, left) + fixed = add(identity(N), projection, -1) + for code, action in zip(codes, (small_action(), small_action(True))): + require(multiply(code["G"], E) == multiply(E, lift(action)), "active action") + require(multiply(code["G"], fixed) == fixed, "fixed complement") + power = identity(3) + for exponent in range(1, 7): + power = multiply(action, power) + require((power == identity(3)) == (exponent == 6), "fixed-chart order") + product = multiply(codes[1]["G"], codes[0]["G"]) + for j in range(N): + vector = [Q(i == j) for i in range(N)] + first = apply_factors(codes[0], vector) + second = apply_factors(codes[1], vector) + require(first == [row.get(j, 0) for row in codes[0]["G"]], "first oracle") + require(second == [row.get(j, 0) for row in codes[1]["G"]], "second oracle") + both = apply_factors(codes[1], first) + require(both == [row.get(j, 0) for row in product], "product oracle") + require(sum(row.get(i, 0) for i, row in enumerate(product)) == 1456, + "full product trace") + + +def controls(R, K, codes, E, left): + bad = [row.copy() for row in codes[0]["P"]] + bad[A[0]] = {} + try: + chart(R, K, bad, codes[0]["L"]) + except ValueError as error: + require(str(error) == "RP != I", "wrong malformed-minor rejection") + else: + raise ValueError("malformed minor accepted") + try: + chart(R, K, codes[0]["P"], selected(R, A)) + except ValueError as error: + require(str(error) == "LP != 0", "wrong overlap rejection") + else: + raise ValueError("overlapping chart accepted") + broken = [row.copy() for row in E] + broken[A[0]].clear() + require(multiply(left, broken) != identity(24), "basis corruption undetected") + wrong = small_action(True) + wrong[0][2] = Q(11) + require(multiply(codes[1]["G"], E) != multiply(E, lift(wrong)), + "action corruption undetected") + same = multiply(small_action(), small_action()) + require(polynomial3(same) == [-1, 0, 0, 1], "same-chart positive control") + require(multiply(multiply(same, same), same) == identity(3), "same-chart return") + + +def run(archive_path): + data = load_sources(archive_path) + R = extract_query(data["CANONICAL-WORD.json.gz"], + data["LOCAL-PROGRAMS.json.gz"]["forward"]) + K = scaled(transpose(R, N), Q(1, 4)) + require(multiply(R, K) == scaled(identity(RANK), 14), "RK != 14I") + P = [row.copy() if i in A else {} for i, row in enumerate(K)] + S = [row.copy() if i in T else {} for i, row in enumerate(K)] + LA, LT = selected(R, A), selected(R, T) + codes = (chart(R, K, P, LT), chart(R, K, S, LA)) + U = add(add(K, P, -1), S, -1) + E = [{**p, **{8+j: x for j, x in s.items()}, **{16+j: x for j, x in u.items()}} + for p, s, u in zip(P, S, U)] + left = LA + LT + scaled(add(add(R, LA, -1), LT, -1), Q(1, 12)) + verify_actions(codes, E, left) + controls(R, K, codes, E, left) + pair = multiply(small_action(True), small_action()) + coefficients = polynomial3(pair) + require(coefficients == [-1, 27, -171, 1], "pair characteristic polynomial") + signs = [evaluate(coefficients, x) for x in (170, 171)] + require(signs == [-24311, 4616], "root bracket") + serial_R = [[str(row.get(j, 0)) for j in range(N)] for row in R] + return { + "status": "PASS_SOURCE_CODE_CHART_ORDER", + "query_sha256": sha256(json.dumps(serial_R, separators=(",", ":")).encode()).hexdigest(), + "ports": N, "query_rank": RANK, "A": list(A), "T": list(T), + "individual_chart_order": 6, "pair_fixed_dimension": 88, + "pair_active_dimension": 24, + "pair_action": [[str(row.get(j, 0)) for j in range(3)] for row in pair], + "pair_characteristic_polynomial_low_to_high": [int(x) for x in coefficients], + "full_characteristic_polynomial": "(t-1)^88 * (t^3-171*t^2+27*t-1)^8", + "pair_trace": 1456, "pair_order": "infinite over Q and Q(i)", + "real_eigenvalue_interval": [170, 171], "polynomial_at_endpoints": [int(x) for x in signs], + "column_oracle_cases": 336, "semantic_failure_controls": 4, + "same_chart_pair_order": 3, + "scope": "Source-only port algebra, not native chart transport or a complete supplier.", + "selected_frontier_changed": False, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--archive", type=Path, + default=ROOT / "research/community-frontier1094-audit/selected-replay.tar.gz") + parser.add_argument("--write", action="store_true", help="regenerate this package's receipt") + args = parser.parse_args() + result = run(args.archive) + receipt = HERE / "RESULT.json" + if args.write: + raw = json.dumps(result, indent=2) + "\n" + require(receipt.write_text(raw, encoding="utf-8") == len(raw), "partial receipt write") + else: + require(json.loads(receipt.read_text(encoding="utf-8")) == result, "receipt mismatch") + print("PASS_SOURCE_CODE_CHART_ORDER orders=6,6,infinite trace=1456 eigenvalue=170..171 columns=336 controls=4 no_new_kappa") + + +if __name__ == "__main__": + main()