From 11fedb46fa199283f78282187c10aea432d8b0bb Mon Sep 17 00:00:00 2001 From: zxv Date: Sat, 24 Oct 2026 10:35:42 -0400 Subject: [PATCH] Certify finite-memory physical endpoints and bound routing dimension --- research/finite-memory-lifting/MUTATIONS.json | 45 ++ research/finite-memory-lifting/OVERLAP.json | 461 ++++++++++++++++++ research/finite-memory-lifting/PROOF.md | 153 ++++++ research/finite-memory-lifting/README.md | 94 ++++ research/finite-memory-lifting/RESULT.json | 157 ++++++ .../finite-memory-lifting/SOURCE-FIXTURE.json | 165 +++++++ research/finite-memory-lifting/SOURCES.json | 65 +++ .../finite-memory-lifting/VALIDATION.json | 57 +++ .../finite-memory-lifting/audit_mutations.py | 90 ++++ research/finite-memory-lifting/certify.py | 100 ++++ .../check_certificate.py | 76 +++ research/finite-memory-lifting/exact.py | 139 ++++++ .../hadamard-wrong-scale.certificate.json | 12 + .../examples/hadamard-wrong-scale.json | 62 +++ .../mixed-column-error.certificate.json | 12 + .../examples/mixed-column-error.json | 60 +++ .../examples/prefix-inverse.certificate.json | 91 ++++ .../examples/prefix-inverse.json | 182 +++++++ research/finite-memory-lifting/models.py | 201 ++++++++ research/finite-memory-lifting/verify.py | 412 ++++++++++++++++ 20 files changed, 2634 insertions(+) create mode 100644 research/finite-memory-lifting/MUTATIONS.json create mode 100644 research/finite-memory-lifting/OVERLAP.json create mode 100644 research/finite-memory-lifting/PROOF.md create mode 100644 research/finite-memory-lifting/README.md create mode 100644 research/finite-memory-lifting/RESULT.json create mode 100644 research/finite-memory-lifting/SOURCE-FIXTURE.json create mode 100644 research/finite-memory-lifting/SOURCES.json create mode 100644 research/finite-memory-lifting/VALIDATION.json create mode 100644 research/finite-memory-lifting/audit_mutations.py create mode 100644 research/finite-memory-lifting/certify.py create mode 100644 research/finite-memory-lifting/check_certificate.py create mode 100644 research/finite-memory-lifting/exact.py create mode 100644 research/finite-memory-lifting/examples/hadamard-wrong-scale.certificate.json create mode 100644 research/finite-memory-lifting/examples/hadamard-wrong-scale.json create mode 100644 research/finite-memory-lifting/examples/mixed-column-error.certificate.json create mode 100644 research/finite-memory-lifting/examples/mixed-column-error.json create mode 100644 research/finite-memory-lifting/examples/prefix-inverse.certificate.json create mode 100644 research/finite-memory-lifting/examples/prefix-inverse.json create mode 100644 research/finite-memory-lifting/models.py create mode 100644 research/finite-memory-lifting/verify.py diff --git a/research/finite-memory-lifting/MUTATIONS.json b/research/finite-memory-lifting/MUTATIONS.json new file mode 100644 index 0000000000..ea9e5ebbf3 --- /dev/null +++ b/research/finite-memory-lifting/MUTATIONS.json @@ -0,0 +1,45 @@ +{ + "checks": [ + { + "diagnostic": "ValueError: noncommuting composition order", + "mutation": "reverse-composition", + "optimized": false + }, + { + "diagnostic": "ValueError: noncommuting composition order", + "mutation": "reverse-composition", + "optimized": true + }, + { + "diagnostic": "ValueError: closure not reached", + "mutation": "erase-positive-seed", + "optimized": false + }, + { + "diagnostic": "ValueError: closure not reached", + "mutation": "erase-positive-seed", + "optimized": true + }, + { + "diagnostic": "ValueError: mutant changed source endpoint phase", + "mutation": "erase-source-absolute-phase", + "optimized": false + }, + { + "diagnostic": "ValueError: mutant changed source endpoint phase", + "mutation": "erase-source-absolute-phase", + "optimized": true + }, + { + "diagnostic": "ValueError: mutant accepted false dirty return", + "mutation": "drop-dirty-return-check", + "optimized": false + }, + { + "diagnostic": "ValueError: mutant accepted false dirty return", + "mutation": "drop-dirty-return-check", + "optimized": true + } + ], + "status": "PASS_FINITE_MEMORY_SEMANTIC_MUTATIONS" +} diff --git a/research/finite-memory-lifting/OVERLAP.json b/research/finite-memory-lifting/OVERLAP.json new file mode 100644 index 0000000000..e35ef015b1 --- /dev/null +++ b/research/finite-memory-lifting/OVERLAP.json @@ -0,0 +1,461 @@ +{ + "status": "BOUNDED_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "upstream_refresh": { + "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "checked_at": "2026-10-24T14:14:01.574214+00:00", + "priority_revision": 7, + "guidance_and_selected_unchanged": true, + "decision": "Continue the explicit finite-memory physical-endpoint assignment; preserve source pins and scope. No frontier or priority change." + }, + "searches": [ + { + "searched_at": "2026-10-24T13:31:45.444055+00:00", + "terms": [ + "weighted automata", + "finite memory", + "finite-state", + "Hankel", + "observability", + "quotient module" + ], + "coverage": { + "local": { + "head": "a8e0467c60fc851f7a94b1ad5524fd562f5922bd", + "records": 7377, + "head_records": 7377, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-24T13:27:35.471342+00:00", + "complete_pagination": true, + "records": 309 + }, + "discussions": { + "fetched_at": "2026-10-24T13:28:38.545107+00:00", + "complete_pagination": true, + "records": 4711 + } + }, + "matches_total": 73, + "displayed_matches": [ + { + "kind": "local-readme", + "title": "research/cross-endframe-observability/README.md", + "path": "research/cross-endframe-observability/README.md", + "matched_terms": [ + "observability" + ] + }, + { + "kind": "local-readme", + "title": "research/selected-k8-omission-observability/README.md", + "path": "research/selected-k8-omission-observability/README.md", + "matched_terms": [ + "observability" + ] + }, + { + "kind": "local-task", + "title": "research/cross-endframe-observability/TASK.json", + "path": "research/cross-endframe-observability/TASK.json", + "matched_terms": [ + "observability" + ] + }, + { + "kind": "local-task", + "title": "research/selected-k8-omission-observability/TASK.json", + "path": "research/selected-k8-omission-observability/TASK.json", + "matched_terms": [ + "observability" + ] + }, + { + "kind": "discussion", + "number": 5142, + "title": "DONE: exact degree 881 for the one-slot doubled centre Gram (#5168)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5142", + "matched_terms": [ + "hankel" + ] + }, + { + "kind": "discussion", + "number": 4577, + "title": "DONE: independent all-length receiver-window cost certificate (#4581)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4577", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion", + "number": 4573, + "title": "DONE: independent receiver-window floor and pinned peer-certificate comparison (#4587)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4573", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion", + "number": 4574, + "title": "DONE: static contact proof for all 128 PR4470 receiver windows (#4585)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4574", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion", + "number": 1884, + "title": "Ten-instance independent research session: interface and verifier audits", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1884", + "matched_terms": [ + "observability" + ] + }, + { + "kind": "discussion-comment", + "number": 1587, + "title": "CLAIM: where does the one unpaid coordinate per live family come from, and is it forced? (ctoth, expires 07:30Z)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1587#discussioncomment-19003763", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion-comment", + "number": 1587, + "title": "CLAIM: where does the one unpaid coordinate per live family come from, and is it forced? (ctoth, expires 07:30Z)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1587#discussioncomment-19003766", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion-comment", + "number": 4709, + "title": "DONE: current-state CRT repair queries and safe fixed-inverse caching", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19141162", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion-comment", + "number": 4709, + "title": "DONE: current-state CRT repair queries and safe fixed-inverse caching", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19144264", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion-comment", + "number": 2750, + "title": "DONE: exact internal precision for the first physical P104 collector", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2750#discussioncomment-19010968", + "matched_terms": [ + "observability" + ] + }, + { + "kind": "discussion-comment", + "number": 4572, + "title": "DONE: independently certified all-length receiver-window floor (#4582)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4572#discussioncomment-19118089", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion-comment", + "number": 5236, + "title": "DONE: reusable universal certificates for dirty linear circuits", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19147346", + "matched_terms": [ + "weighted automata" + ] + }, + { + "kind": "discussion-comment", + "number": 4574, + "title": "DONE: static contact proof for all 128 PR4470 receiver windows (#4585)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4574#discussioncomment-19118098", + "matched_terms": [ + "finite-state" + ] + }, + { + "kind": "discussion-comment", + "number": 1166, + "title": "Handoffs and requests for independent checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19003933", + "matched_terms": [ + "finite-state" + ] + } + ], + "warnings": [ + "open_prs: offline; cached data may miss current changes", + "discussions: offline; cached data may miss current changes" + ] + }, + { + "searched_at": "2026-10-24T14:07:02.911011+00:00", + "terms": [ + "matrix product", + "matrix-product", + "transfer dimension", + "column-mixing", + "finite-memory" + ], + "coverage": { + "local": { + "head": "a8e0467c60fc851f7a94b1ad5524fd562f5922bd", + "records": 7377, + "head_records": 7377, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-24T14:05:56.655979+00:00", + "complete_pagination": true, + "records": 311 + }, + "discussions": { + "fetched_at": "2026-10-24T14:07:02.504197+00:00", + "complete_pagination": true, + "records": 4711 + } + }, + "matches_total": 82, + "displayed_matches": [ + { + "kind": "local-readme", + "title": "research/matrix-product-common-three-factor/README.md", + "path": "research/matrix-product-common-three-factor/README.md", + "matched_terms": [ + "matrix-product" + ] + }, + { + "kind": "local-task", + "title": "research/matrix-product-common-three-factor/TASK.json", + "path": "research/matrix-product-common-three-factor/TASK.json", + "matched_terms": [ + "matrix-product" + ] + }, + { + "kind": "discussion-comment", + "number": 1167, + "title": "Larger κ: proposals that change the current cost structure", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18924220", + "matched_terms": [ + "matrix product", + "matrix-product" + ] + }, + { + "kind": "local-readme", + "title": "research/orthogonal-witness-precision/README.md", + "path": "research/orthogonal-witness-precision/README.md", + "matched_terms": [ + "matrix product", + "matrix-product" + ] + }, + { + "kind": "local-readme", + "title": "research/p104-endpoint-rank-lean/README.md", + "path": "research/p104-endpoint-rank-lean/README.md", + "matched_terms": [ + "matrix product", + "matrix-product" + ] + }, + { + "kind": "local-readme", + "title": "research/scalar-block-schur-dimension/README.md", + "path": "research/scalar-block-schur-dimension/README.md", + "matched_terms": [ + "matrix product", + "matrix-product" + ] + }, + { + "kind": "local-readme", + "title": "research/scalar-pivot-schur-dimension/README.md", + "path": "research/scalar-pivot-schur-dimension/README.md", + "matched_terms": [ + "matrix product", + "matrix-product" + ] + }, + { + "kind": "local-task", + "title": "research/scalar-block-schur-dimension/TASK.json", + "path": "research/scalar-block-schur-dimension/TASK.json", + "matched_terms": [ + "matrix product", + "matrix-product" + ] + }, + { + "kind": "discussion", + "number": 4182, + "title": "Rounded block solves at the fine-prime Gaussian boundary", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4182", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "discussion-comment", + "number": 1798, + "title": "CLAIM: three-dimensional coordinate-CNOT two-role sharing (seed 1385e243)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1798#discussioncomment-18921618", + "matched_terms": [ + "matrix-product" + ] + }, + { + "kind": "discussion-comment", + "number": 4611, + "title": "DONE: formal controllers without idles and priced recovery failures (#4623)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4611#discussioncomment-19151553", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "discussion-comment", + "number": 1166, + "title": "Handoffs and requests for independent checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19026147", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "discussion-comment", + "number": 1166, + "title": "Handoffs and requests for independent checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19085389", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "discussion-comment", + "number": 1166, + "title": "Handoffs and requests for independent checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131555", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "discussion-comment", + "number": 1166, + "title": "Handoffs and requests for independent checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144340", + "matched_terms": [ + "matrix-product" + ] + }, + { + "kind": "discussion-comment", + "number": 1166, + "title": "Handoffs and requests for independent checks", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146370", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "discussion-comment", + "number": 1167, + "title": "Larger κ: proposals that change the current cost structure", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18936773", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "discussion-comment", + "number": 1596, + "title": "Selected complex rank-one block delivery: sharp integer budget and overhead tax", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1596#discussioncomment-18922195", + "matched_terms": [ + "matrix-product" + ] + }, + { + "kind": "local-readme", + "title": "research/binary-schur-minimal-dimension/README.md", + "path": "research/binary-schur-minimal-dimension/README.md", + "matched_terms": [ + "matrix product" + ] + }, + { + "kind": "local-readme", + "title": "research/bit-dyadic-ternary-catalyst/README.md", + "path": "research/bit-dyadic-ternary-catalyst/README.md", + "matched_terms": [ + "matrix product" + ] + } + ], + "warnings": [] + } + ], + "direct_pr_bodies_read": [ + 5235, + 5262, + 5352, + 5369, + 5419, + 5427, + 5425, + 5436 + ], + "additional_live_checks": { + "latest_open_pr_titles_through": 5439, + "github_queries": [ + "repo:CrocSwap/integer-mult-bounds is:pr \"automata\"", + "repo:CrocSwap/integer-mult-bounds is:pr \"finite-memory\"", + "repo:CrocSwap/integer-mult-bounds is:pr \"matrix-product\"" + ], + "matrix_product_search_results": 77, + "matrix_product_search_results_displayed": 15 + }, + "novelty_boundary": "Weighted automata, matrix-product representations, Hankel/cut rank and projection error bounds are classical. The proposed contribution is the concrete physical-column finite-memory contract, complete-return/source adapter, and explicit native research boundaries. No global priority claim.", + "limits": "The local corpus is the recorded 7,377-note checkout, not all notes at refreshed main. Remote snapshots search open PR bodies and discussion records, not all historical code diffs, closed PR bodies, or unpublished work. Only the displayed matches and directly named predecessor sources were inspected.", + "submission_refresh": { + "checked_at": "2026-10-24T14:35:42.283535+00:00", + "canonical_main": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "source_files_unchanged": 7, + "live_query": { + "items": [ + { + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/236", + "number": 236, + "title": "[Lean] Verification of paired-cube finite identities and arithmetic — κ = 0.0004609169" + }, + { + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1790", + "number": 1790, + "title": "Selected PR1094: complete two-role whole-helper swap census (no improving swap)" + } + ], + "total": 2 + }, + "decision": "Proceed with the reviewed scoped theorem; retain source pins and independent-review limitations." + } +} diff --git a/research/finite-memory-lifting/PROOF.md b/research/finite-memory-lifting/PROOF.md new file mode 100644 index 0000000000..36152f9e31 --- /dev/null +++ b/research/finite-memory-lifting/PROOF.md @@ -0,0 +1,153 @@ +# Finite-memory lifting and the limits of column routing + +**Status:** local written proof with exact finite calibration, awaiting independent mathematical review. The weighted-automata and matrix-product foundations are classical. The contribution is their concrete physical-column contract for native protocols, its positive-width and complete-return treatment, an explicit source adapter, and the routing/approximation boundaries below. No new κ, physical supplier, general automata algorithm or global literature priority is claimed. + +## 1. A concrete family, rather than independent operator letters + +Fix a field K, a local column dimension d, a transfer dimension D, p output roles and q independent input roles. Supply fixed matrices + +`F ∈ K^(p×D), B ∈ K^(D×q), T_(y,x) ∈ K^(D×D)`, + +for every pair `0<=y,x=r for any representation of that endpoint. This is the classical matrix-product cut-rank obstruction, here applied to the complete physical endpoint. It also applies to position-dependent tables at a fixed width, although those do not inherit Theorem A's all-width cutoff. + +**Half-swap.** Let f=2k, local dimension d, and let S swap the two k-column halves. Put `N=d^(2k)`, the physical Hilbert-space dimension. At the middle cut its unfolding is the N-by-N permutation matrix + +`H_(yL,xL ; yR,xR) = [yL=xR][yR=xL]`. + +Therefore exact representation requires `D>=d^(2k)`. Over C, every approximant A with cut rank at most D satisfies + +`||A-S||_op² >= max(0, 1-D/d^(2k))`. + +**Proof of the robust bound.** Let Q project onto the column space of H(A), of rank r<=D. Since H(S) is unitary, + +`||H(A)-H(S)||_F² >= ||(I-Q)H(S)||_F² = N-r >= N-D`. + +Unfolding preserves the Frobenius norm. For an N-dimensional physical operator, `||E||_F²<=N||E||_op²`. Divide by N. ∎ + +**Nonlocal quadratic phase.** Over C, on two k-bit halves let + +`V|a,b> = (-1)^(a dot b)|a,b>`. + +The nonzero part of its middle unfolding is the `2^k`-dimensional Walsh matrix W, with `WW*=2^k I`. Consequently + +`D>=2^k` exactly, and `||A-V||_op²>=max(0,1-D/2^k)` for any cut-rank-D approximant. + +For the robust statement, with M=2^k the discarded squared Frobenius energy is at least `M(M-D)` and the physical Hilbert-space dimension is M². The same projection argument gives the bound. Thus even this phase-only Clifford family cannot have a uniformly bounded transfer dimension in the fixed column order. + +The bits label the address basis; the coefficients here are complex. In characteristic two the signs coincide and this phase obstruction disappears. It is not an F2/BIT lower bound. + +For a product of scalar-block layers with dimensions b_1,…,b_h, composition gives `D<=Π b_j`. The half-swap therefore requires `Π b_j >= (1-ε²)d^(2k)` to reach operator error ε<1; the paired phase requires `Π b_j >= (1-ε²)2^k`. Owner sums, physical memory conversions and routing direction must be accounted for separately. These are representation bounds, not native paid-call or tape-time lower bounds. Changing the column order changes the cut and can remove the obstruction. + +## 6. Essential limits of finite testing + +**Bounded bond at individual widths is insufficient.** A one-state family with width-dependent left boundary equal to zero through any chosen M and one afterwards passes those M tests but fails later. Arbitrary unrepresented position dependence gives the same problem. A fixed transfer table, or an explicit finite controller included in D, is essential. + +**Tolerance is not equality.** Even a fixed one-state unitary per instance can have small early errors and large late errors. Let `α_N=(N+i)/(N-i)` and compare `α_N^f I` with I. For f<=M, + +`|α_N^f-1| <= f|α_N-1| <= 2M/N`. + +Write `θ=2 arctan(1/N)>0`. At an integer f nearest π/θ, the phase is within θ/2 of π, so `|α_N^f-1|>=2 cos(θ/4)>=sqrt(2)` for N>=1. Hence no D-only finite-width **tolerance** test certifies a uniform small error, even for a two-state comparison of fixed unitary families. The exact algorithm sees a nonzero discrepancy immediately; numerical resolution and a recovery-safe error budget are separate obligations. + +The theorem decides equality after a valid fixed finite representation has been supplied. Extracting that representation from an actual program, pricing it, and proving its precision/tape/recursive admissibility remain independent research tasks. + +## Open next questions + +1. Extract the smallest useful physical transfer tables for one currently investigated provider/consumer, preserving all source versions and dirty returns. Table/bond growth, not a missing equivalence algorithm, is the first obstacle. +2. Build a real cross-column native adapter for the prefix construction and price its complete inverse, storage and movement. The virtual two-state description is not that implementation. +3. Derive source-specific cut minors for an actual observation or routing obligation; account for legal column reorderings before calling it a barrier. +4. Extend exact certificates to a uniform approximation criterion with proven contraction/conditioning assumptions. Small early-width errors alone are insufficient. +5. Use the bit-bound methods of [#5352](https://github.com/CrocSwap/integer-mult-bounds/pull/5352) to optimize this concrete table format and quantify practical extraction limits; symbolic succinctness and explicit-table bit complexity are different questions. diff --git a/research/finite-memory-lifting/README.md b/research/finite-memory-lifting/README.md new file mode 100644 index 0000000000..5ce4fa86af --- /dev/null +++ b/research/finite-memory-lifting/README.md @@ -0,0 +1,94 @@ +# Beyond columnwise controls: finite certificates and routing bounds + +Columnwise tensor tests leave genuine cross-column programs outside their hypotheses. A **fixed finite transfer table** supplies another usable contract: complete endpoint equality at every positive width has a finite exact certificate, or a literal discrepancy at a width bounded by the transfer dimension. This includes dense/non-Clifford local operators, finite-memory column mixing and explicitly represented recurrent width coefficients. + +The same representation gives exact and robust obstructions. Swapping two k-column halves requires transfer dimension at least d^(2k); pairing their binary quadratic phases requires at least 2^k. At operator error ε<1 these become `(1−ε²)d^(2k)` and `(1−ε²)2^k`. These are bounds on representation at a specified column cut, not paid-query or tape-time bounds. + +The [complete proof](PROOF.md) credits classical weighted automata and matrix-product methods. The new repository contribution is the concrete physical-column contract, complete-return/source adapter and the explicit enabling/exclusion boundaries. This is local written mathematics and author-checked code, awaiting independent review. No global literature priority, new κ or admitted supplier is claimed. + +## The usable theorem + +Let F,B be fixed role boundaries and T_(y,x) fixed D-by-D transitions for each physical output/input column pair. The width-f endpoint entry is + +`[F T_(y1,x1) … T_(yf,xf) B]_(output_role,input_role)`. + +**Every positive width agrees with the reference iff the residual vanishes at all widths 1,…,D.** This means every physical entry and every original/returned role at those widths. A few sampled columns are insufficient. The implementation avoids constructing those large matrices: it builds a reachable-row certificate R satisfying + +`F T_s = E_s R`, `R T_s = C_s R`, `R B = 0` for every local symbol s. + +These equations suffice for an independently checkable all-width conclusion. On failure the producer returns one physical input column, output column, input/output role pair and exact nonzero discrepancy. Its width is at most D. If the positive seed span has rank r1>0, the proof improves this to D−r1+1. A D-cycle has its first positive discrepancy exactly at width D, so the general D bound is sharp. + +All coefficients are interpreted as concrete physical entries. Local inverse/phase relations are therefore already present. The statement does not require independent formal native letters, monomiality, a finite Clifford group, bounded expanded term support or column permutation symmetry. + +## Contract and composition + +| Feature | Construction and cost in transfer dimension | +|---|---| +| Sum or reference subtraction | Direct sum; dimensions add. Exterior scalars multiply one boundary. | +| Physical composition | Contract the intermediate column index and tensor virtual spaces; dimensions multiply. Global owner sums are performed separately. | +| Supplied inverse | Check both complete compositions. An arbitrary MPO inverse is not assumed to have finite transfer dimension. | +| Recurrent coefficient `a G^f b` | Tensor the k-state coefficient recurrence into the transitions; dimension multiplies by k. Polynomial, exponential and periodic coefficients fit. | +| Regular restrictions | Include the finite recognizer in the state bound. A restricted width subsequence is not all positive widths. | +| Dirty or rectangular role endpoints | Keep every required independent input/output role in F,B and the reference. Returning zero does not restore arbitrary dirt. | + +Tables must remain fixed across widths, including any schedule/controller state. Bounded bond dimension separately at each width does not suffice. Explicit tables can grow exponentially during extraction from a succinct circuit. The classical polynomial equivalence algorithm is polynomial in the **extracted table**, not necessarily in the original program. The checker currently implements exact Q(i), shared arithmetic/parsing and separately transcribed closure checks; it imports no producer or elimination code. Its default state budget is 256; exceeding it is no decision. + +## Examples that enable or stop research + +**Genuine column mixing.** Prefix XOR maps `y_j=x_1 xor … xor x_j` using two transfer states and has an exactly certified inverse. It does not commute with swapping columns and therefore cannot be represented as a scalar sum of identical one-column tensor powers. A two-by-two cut minor proves that two states are necessary. This goes beyond the interface in [#5436](https://github.com/CrocSwap/integer-mult-bounds/pull/5436), while giving no free physical realization. + +**Pinned native source.** The byte-exact [nine-axis, two-role source word](SOURCE-FIXTURE.json) comes from [#5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369)'s [source-conjugation example](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/native-tensor-cutoff/examples/source-conjugation.json). Its eight instructions implement and cancel the actual `G Z G^-1=R` query, with both dirty roles restored. The new frontend checks all four owner/input blocks, independently checks all 512 local addresses, and certifies the prefix-encoded source shear with eight virtual states and a two-row invariant. Removing R's absolute phase fails at width one. This is a concrete algebraic adapter, not a replay of the selected provider or caller. + +**Routing that cannot stay bounded.** At the middle cut, a half-swap unfolds to a full permutation matrix; a phase `(-1)^(a dot b)` unfolds to a Walsh matrix. Exact rank and discarded Frobenius energy give the bounds above, including operator-norm approximation. Fixed transfer dimension fails for both families as width grows, in this column order. Changing column order, growing state or a different representation may evade them. + +The signed phase and norm statements use complex coefficients. They are not F2/BIT bounds: in characteristic two those signs coincide. The prototype checker implements Q(i). + +**Two misleading probes.** A three-state example vanishes on every constant repeated column yet fails on a mixed word of length two. A fixed unitary `α_N=(N+i)/(N-i)` has error at most 2M/N through width M, but some later width has error at least sqrt(2). Exact closure certificates work; short-width tolerance tests need a separate conditioning/contractivity theorem. + +## Run and inspect + +Python 3.10+ and its standard library are sufficient. From the repository root: + +```sh +python3 -B research/finite-memory-lifting/certify.py \ + research/finite-memory-lifting/examples/prefix-inverse.json > /tmp/prefix-certificate.json +python3 -B research/finite-memory-lifting/check_certificate.py \ + research/finite-memory-lifting/examples/prefix-inverse.json /tmp/prefix-certificate.json +python3 -B research/finite-memory-lifting/verify.py +python3 -O -B research/finite-memory-lifting/verify.py +python3 -B research/finite-memory-lifting/audit_mutations.py +# Optional byte authentication against the pinned canonical checkout: +python3 -B research/finite-memory-lifting/verify.py --source-root . +``` + +The standalone checker can be distributed with `exact.py`, the problem and certificate; it does not need `certify.py`, `models.py`, Git or repository sources. Python isolated mode omits the script's sibling-module directory, so these commands use `-B`; the portable audit additionally supplies a fresh bytecode-cache prefix in a private directory. Arbitrary preexisting Python import environments are not authenticated by these direct commands. + +The problem format declares `local_dimension`, `states`, `outputs`, `inputs`, `left`, `right` and a `transitions` object indexed by canonical `"output,input"` pairs. Every absent pair is the zero transition. Matrices use explicit integers/fraction strings or `[real,imaginary]` pairs. Floats, exponent notation, duplicate JSON keys and malformed dimensions reject. Supply the **residual** operator, including every required return. A counterexample names a physical entry; it is not a profitable program or a priced native witness. + +## Evidence and attribution + +[RESULT.json](RESULT.json) records exact finite calibration; [VALIDATION.json](VALIDATION.json) records the executed environment, output hash, portable and optimized checks; [MUTATIONS.json](MUTATIONS.json) records private semantic mutations. Tests cover literal path sums, sharp delayed counterexamples, full prefix matrices, exact source phases/returns, rank/Gram routing controls and forged-certificate rejection. Finite checks corroborate the written proof; they are not its universal justification. + +Canonical base: [`32890bc5de034ab8fc93ac88ead7279a6a416d04`](https://github.com/CrocSwap/integer-mult-bounds/commit/32890bc5de034ab8fc93ac88ead7279a6a416d04), priority revision 7, selected conditional κ=.003027288235. [SOURCES.json](SOURCES.json) binds seven canonical provenance files and the classical literature. [OVERLAP.json](OVERLAP.json) records bounded coverage and the scope distinction. Closed historical bodies, arbitrary code diffs and unpublished work are not exhaustively searched. + +The closest work is [#5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235)'s independent-operator register certificates by [zxv](https://github.com/zxv), [#5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262)'s true-inverse extension by [Krzysztof Wójt](https://github.com/krzysztofwojt), [#5352](https://github.com/CrocSwap/integer-mult-bounds/pull/5352)'s bit bounds by [Ali Romman](https://github.com/aliromman), and [#5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369)'s specialized physical native criterion. The new physical-pair alphabet resolves operator relations directly and permits finite-memory column coupling. It does not replace the predecessor frontends or their substantially more compact certificates in their own domains. + +Retain [the recipe/source attribution](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/native-tensor-cutoff/README.md#sources-and-credit), including [Jose Manuel](https://github.com/jmbarrancoml)'s [#2250](https://github.com/CrocSwap/integer-mult-bounds/pull/2250) implementation and its native, phase, compiler and verification lineage. The [weighted-automata theorem](https://people.mpi-sws.org/~joel/publications/Q_weighted_automata13.pdf) and [matrix-product correspondence](https://arxiv.org/abs/0708.1221) are classical, as are cut-rank and projection-error arguments. New prose/code are Apache-2.0 with substantial OpenAI Codex assistance. No independent human or formal-kernel acceptance is claimed. + +No full 112-owner/17-axis provider, selected cold replay, physical cross-column implementation, paid/tape/precision bill, generic replay registration, Lean or Docker run is included. + +## Significance for researchers + +The result makes a named class of cross-column proposals testable without forcing it into a columnwise or free-word model. A successful table yields complete all-width semantics with inspectable certificates; a failed table yields a concrete input/output discrepancy. Cut-rank certificates can reject bounded-state routing proposals before expensive synthesis, including some approximate proposals. The first work for an active caller is now explicit: extract its true physical transfer tables, retain source versions and returns, and measure dimension/column order before pricing a construction. + +## Open next questions + +| Direction | Useful first result | Risk or blocker | +|---|---|---| +| **One actual provider/consumer** | Extract a complete endpoint from [#5419](https://github.com/CrocSwap/integer-mult-bounds/pull/5419)'s changed-interface program or another source-bound caller. | State/table expansion may make the representation unusable; missing observations remain missing. | +| **Physical observation audit** | Bind one candidate relation from [#5427](https://github.com/CrocSwap/integer-mult-bounds/pull/5427) to actual local entries and phases. | Its formal-word nonmembership is not automatically physical nonmembership; this package has not decided that source question. | +| **A legal cross-column adapter** | Implement prefix encoding and return in a permitted native/tape contract. | Virtual dimension two does not price memory, access, copying or inversion. | +| **Source-specific cut certificates** | Exhibit one exact coefficient minor for an actual routing or observation demand. | Legal column reorderings and preexisting side information can change the cut. | +| **Compact table extraction** | Reuse [#5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), [#5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262) and [#5352](https://github.com/CrocSwap/integer-mult-bounds/pull/5352) to avoid explicit word expansion in one physical frontend. | Concrete relations and succinct extraction can be harder than equivalence of the final table. | +| **Uniform approximate certification** | Add a proved contraction/conditioning hypothesis and an actual recovery error budget. | Finite-width tolerance tests fail even for fixed unitary families. | +| **Complete cost transfer** | Turn a semantically accepted table into a priced supplier or a justified scoped rejection. | The representation theorem alone settles none of the selected compiler, tape, storage, precision or analytic assumptions. | diff --git a/research/finite-memory-lifting/RESULT.json b/research/finite-memory-lifting/RESULT.json new file mode 100644 index 0000000000..e31cf2b8fb --- /dev/null +++ b/research/finite-memory-lifting/RESULT.json @@ -0,0 +1,157 @@ +{ + "approximate_cutoff_controls": [ + { + "early_widths": 8, + "late_error_squared_exceeds": 2, + "late_width": 24, + "parameter": 16 + }, + { + "early_widths": 8, + "late_error_squared_exceeds": 2, + "late_width": 96, + "parameter": 64 + }, + { + "early_widths": 8, + "late_error_squared_exceeds": 2, + "late_width": 192, + "parameter": 128 + } + ], + "columns": { + "complete_prefix_entries": 340, + "exact_minimum_prefix_bond": 2, + "invariant_rows": 2, + "inverse_certificate_states": 5, + "literal_prefix_columns": 126 + }, + "core": { + "mixed_word_width": 2, + "path_sum_comparisons": 138, + "phase_filter_period": 4, + "random_transducers": 24, + "rectangular_role_controls": 2, + "recurrence_widths": 9, + "sharp_first_failure_widths": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12 + ], + "wrong_Hadamard_scale_failure_width": 2 + }, + "native": { + "absolute_phase_mutation_width": 1, + "all_owner_blocks": [ + { + "input": 0, + "invariant_rows": 1, + "output": 0, + "states": 2 + }, + { + "input": 1, + "invariant_rows": 0, + "output": 0, + "states": 1 + }, + { + "input": 0, + "invariant_rows": 1, + "output": 1, + "states": 2 + }, + { + "input": 1, + "invariant_rows": 1, + "output": 1, + "states": 2 + } + ], + "encoded_source_invariant_rows": 2, + "encoded_source_local_entries": 1024, + "encoded_source_shear_states": 8, + "independent_source_addresses": 512, + "source_axes": 9, + "source_instruction_count": 8 + }, + "rejections": [ + "width-bound", + "missing-seed-symbol", + "missing-closure-symbol", + "wrong-closure", + "changed-dirty-return-binding", + "changed-dirty-return-semantic", + "float-coefficient", + "noncanonical-alphabet-entry", + "zero-counterexample", + "wrong-counterexample-width" + ], + "routing": { + "half_swaps": [ + { + "entry_checks": 16, + "unfolding_rank": 4, + "width": 2 + }, + { + "entry_checks": 256, + "unfolding_rank": 16, + "width": 4 + }, + { + "entry_checks": 4096, + "unfolding_rank": 64, + "width": 6 + }, + { + "entry_checks": 65536, + "unfolding_rank": 256, + "width": 8 + } + ], + "paired_quadratic_phases": [ + { + "cut_rank": 2, + "squared_singular_value": 2, + "width": 2 + }, + { + "cut_rank": 4, + "squared_singular_value": 4, + "width": 4 + }, + { + "cut_rank": 8, + "squared_singular_value": 8, + "width": 6 + }, + { + "cut_rank": 16, + "squared_singular_value": 16, + "width": 8 + }, + { + "cut_rank": 32, + "squared_singular_value": 32, + "width": 10 + }, + { + "cut_rank": 64, + "squared_singular_value": 64, + "width": 12 + } + ] + }, + "standalone": "producer_absent_readonly_empty_PATH_normal_and_optimized", + "status": "PASS_FINITE_MEMORY_LIFTING_CALIBRATION" +} diff --git a/research/finite-memory-lifting/SOURCE-FIXTURE.json b/research/finite-memory-lifting/SOURCE-FIXTURE.json new file mode 100644 index 0000000000..760f54ac2d --- /dev/null +++ b/research/finite-memory-lifting/SOURCE-FIXTURE.json @@ -0,0 +1,165 @@ +{ + "axes": 9, + "roles": 2, + "generators": { + "G": { + "matrix_rows": [ + 6, + 64, + 384, + 5, + 34, + 32, + 8, + 48, + 256 + ], + "offset": 426, + "quadratic_rows": [ + 4, + 38, + 39, + 0, + 0, + 6, + 256, + 256, + 448 + ], + "linear_Z4": [ + 2, + 1, + 3, + 0, + 0, + 2, + 0, + 0, + 1 + ], + "phase": 1 + }, + "Z": { + "matrix_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "linear_Z4": [ + 0, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "R": { + "matrix_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 2, + "linear_Z4": [ + 0, + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0 + ], + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + }, + "program": [ + { + "op": "apply", + "dst": 0, + "generator": "G", + "inverse": true + }, + { + "op": "apply", + "dst": 0, + "generator": "Z" + }, + { + "op": "apply", + "dst": 0, + "generator": "G" + }, + { + "op": "add", + "src": 0, + "dst": 1 + }, + { + "op": "apply", + "dst": 0, + "generator": "G", + "inverse": true + }, + { + "op": "apply", + "dst": 0, + "generator": "Z", + "inverse": true + }, + { + "op": "apply", + "dst": 0, + "generator": "G" + }, + { + "op": "query", + "src": 0, + "dst": 1, + "generator": "R", + "coefficient": -1 + } + ], + "reference": [] +} diff --git a/research/finite-memory-lifting/SOURCES.json b/research/finite-memory-lifting/SOURCES.json new file mode 100644 index 0000000000..90d8675e33 --- /dev/null +++ b/research/finite-memory-lifting/SOURCES.json @@ -0,0 +1,65 @@ +{ + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "research/native-tensor-cutoff/examples/source-conjugation.json", + "usage": "provenance", + "git_blob": "760f54ac2dc7b3204fdfbd60a8496d785c421f3c", + "sha256": "895c6991b272335fd9c92330933addf2ec52956454c37f0be3939d2f4afb3eff" + }, + { + "path": "research/native-tensor-cutoff/PROOF.md", + "usage": "provenance", + "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0", + "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041" + }, + { + "path": "research/native-tensor-cutoff/README.md", + "usage": "provenance", + "git_blob": "91ae9eadd8a8679de7cf488fc2e3f350214feeff", + "sha256": "98a3166b7d0db513e8918f17f73359bebde1f802af251f6c55305fb99b869f87" + }, + { + "path": "research/universal-dirty-certificates/PROOF.md", + "usage": "provenance", + "git_blob": "3a405e327a7fd5d59a570d7f9920f1ce7f229a76", + "sha256": "ef4cfcfd65b1dde1f11eedace0ed90a1b47a2cc100daaf778fbecbff3ec685a7" + }, + { + "path": "research/inverse-dirty-certificates/PROOF.md", + "usage": "provenance", + "git_blob": "d2433c24ca46a1cf4af481f6ae9b281991cdafac", + "sha256": "de0820379f76fb4ab680c6401c852cc9ea127e447de11ca93a1453471d858f11" + }, + { + "path": "research/inverse-certificate-bit-bounds/PROOF.md", + "usage": "provenance", + "git_blob": "553005f2257a2cfdf5e00d6c8b4c207de86cfc1b", + "sha256": "6aa449921fec182b9c8a56bfe96570140c821e72ff8f8157a15da5690ac276ad" + } + ], + "literature": [ + { + "title": "On the Complexity of Equivalence and Minimisation for Q-Weighted Automata", + "url": "https://people.mpi-sws.org/~joel/publications/Q_weighted_automata13.pdf", + "used": "Proposition 3.1 and classical reachable-space equivalence; credited input, not a new general automata theorem." + }, + { + "title": "Finite automata for caching in matrix product algorithms", + "url": "https://arxiv.org/abs/0708.1221", + "used": "Classical weighted-automata/matrix-product correspondence; not claimed new." + }, + { + "title": "A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata", + "url": "https://doi.org/10.1137/0221017", + "used": "Classical algorithmic predecessor." + } + ], + "scope": "Local theorem and standalone checker; source recipe retained with attribution. No complete native caller, free cross-column operation, new kappa or independent review." +} diff --git a/research/finite-memory-lifting/VALIDATION.json b/research/finite-memory-lifting/VALIDATION.json new file mode 100644 index 0000000000..db12c28202 --- /dev/null +++ b/research/finite-memory-lifting/VALIDATION.json @@ -0,0 +1,57 @@ +{ + "status": "PASS_LOCAL_FINITE_MEMORY_LIFTING", + "checked_at": "2026-10-24T14:14:12.588123+00:00", + "python": "3.14.5 (main, May 10 2026, 10:21:34) [Clang 21.0.0 (clang-2100.0.123.102)]", + "platform": "macOS-26.5.1-arm64-arm-64bit-Mach-O", + "result_sha256": "4e542c1cbd569d50d6ee3ded30bcfdbe808befd8500d36609fbf70bcaa773ec7", + "checks": [ + { + "check": "source_bound_normal", + "seconds": 2.888243 + }, + { + "check": "source_bound_optimized", + "seconds": 2.918726 + }, + { + "check": "four_semantic_mutations_normal_and_optimized", + "seconds": 2.24907 + }, + { + "check": "portable_readonly_optimized_empty_PATH", + "seconds": 2.953047, + "unchanged_files": 8, + "files": [ + "exact.py", + "certify.py", + "check_certificate.py", + "models.py", + "verify.py", + "audit_mutations.py", + "SOURCE-FIXTURE.json", + "SOURCES.json" + ] + } + ], + "proof_and_source_sha256": { + "exact.py": "dba9d6aa1ecd15c52c752faf595b588edebc9d100cc48666633c6c3981f0751d", + "certify.py": "479b5b3fe360fe69024dbc6104e57c6b7bf141848f47a0491ee3148fda71105a", + "check_certificate.py": "043bd7951098c8af83c6bc190b898da7b7e7c454049e4fc572a47002983b8b94", + "models.py": "211c91077eae89a3a6aac1bb32950abd4aa08afa130dbaa03b80aee6c6d1e01b", + "verify.py": "35ebc57b63da4e4067943c741a8647e7418af898a0dcfb5615e2733e9bc662c9", + "audit_mutations.py": "192f7de5b79528783d851f285c4a3ad5c7365a2e15e3eee1818177d6e6c33a3b", + "SOURCE-FIXTURE.json": "895c6991b272335fd9c92330933addf2ec52956454c37f0be3939d2f4afb3eff", + "SOURCES.json": "7dd2dd5b663f503209178096861d17c0d02a3cae81780fb3b51ff4cc8e2288dc", + "PROOF.md": "de4a6b79d480d7718b3d157d2be73b4f45723ccac6719160dd815f8cef40356b" + }, + "scope": "Exact finite calibration, source-byte binding and certificate checks. Hashes identify the written proof; they do not validate it. No independent mathematical review, full provider/caller, physical cost, selected replay or formal-kernel acceptance.", + "additional_checks": { + "cli_examples": { + "prefix-inverse": "PASS_ALL_POSITIVE_WIDTHS", + "mixed-column-error": "PASS_PHYSICAL_COUNTEREXAMPLE", + "hadamard-wrong-scale": "PASS_PHYSICAL_COUNTEREXAMPLE" + }, + "documentation": "All relative document targets exist; pinned canonical GitHub file targets resolve; every PR reference in PR-DRAFT.md, README.md and PROOF.md is linked; JSON and whitespace checks pass.", + "publication": "Validation covers local source and certificate checks; publication and hosted execution are separate." + } +} diff --git a/research/finite-memory-lifting/audit_mutations.py b/research/finite-memory-lifting/audit_mutations.py new file mode 100644 index 0000000000..d747fd74a8 --- /dev/null +++ b/research/finite-memory-lifting/audit_mutations.py @@ -0,0 +1,90 @@ +"""Private semantic mutations; never edit the source package in place. + +Apache-2.0; substantial OpenAI Codex assistance. +""" +from copy import deepcopy +from pathlib import Path +import json +import subprocess +import sys +import tempfile +from exact import G, fingerprint, need, scalar +from certify import certify +from check_certificate import check +from models import compose, difference, prefix_xor, transpose, unit + +ROOT = Path(__file__).resolve().parent + + +def main(): + p = prefix_xor() + data = difference(compose(transpose(p), p), unit(2)).problem() + claim = certify(data) + column = next(j for j in range(data['states']) if any(scalar(r[j]) for r in claim['basis'])) + changed = deepcopy(data) + changed['right'] = [[int(i == column)] for i in range(data['states'])] + bad = deepcopy(claim) + bad['problem_sha256'] = fingerprint(changed) + try: + check(changed, bad) + except ValueError: + pass + else: + raise ValueError('baseline accepted bad dirty return') + cases = [ + ('reverse-composition', 'models.py', + " need(a.d == b.d, 'composition local dimension')", + " need(a.d == b.d, 'composition local dimension')\n a, b = b, a", + ['verify.py', '--suite', 'core']), + ('erase-positive-seed', 'certify.py', + " visit(rowmul(left[i], transitions[symbol]), i, [symbol])", + " visit([G() for _ in range(n)], i, [symbol])", + ['verify.py', '--suite', 'core']), + ('erase-source-absolute-phase', 'models.py', + " exponent = recipe['phase']", + " exponent = 0", + ['source_control.py']), + ('drop-dirty-return-check', 'check_certificate.py', + " need(not sum((rows[i][k]*right[k][j] for k in range(n)), G()), 'all returned channels')", + " need(True, 'all returned channels')", + ['return_control.py'])] + results = [] + for name, filename, old, new, args in cases: + for optimized in (False, True): + with tempfile.TemporaryDirectory(prefix='finite-memory-mutant-') as folder: + out = Path(folder) + for f in ('exact.py', 'certify.py', 'check_certificate.py', 'models.py', 'verify.py', + 'SOURCE-FIXTURE.json'): + (out/f).write_bytes((ROOT/f).read_bytes()) + target = out/filename + text = target.read_text() + need(text.count(old) == 1, 'unique mutation site: '+name) + target.write_text(text.replace(old, new, 1)) + (out/'bad-problem.json').write_text(json.dumps(changed)) + (out/'bad-certificate.json').write_text(json.dumps(bad)) + (out/'return_control.py').write_text( + "from exact import load\nfrom check_certificate import check\n" + "try:\n check(load('bad-problem.json'),load('bad-certificate.json'))\n" + "except ValueError:\n pass\n" + "else:\n raise ValueError('mutant accepted false dirty return')\n") + (out/'source_control.py').write_text( + "from exact import load,need\nfrom certify import certify\n" + "from models import native_frontend\n" + "for row in native_frontend(load('SOURCE-FIXTURE.json')):\n" + " for block in row:\n" + " need(certify(block.problem())['kind']=='all_positive_widths'," + " 'mutant changed source endpoint phase')\n") + command = [sys.executable, '-B', '-X', 'pycache_prefix='+str(out/'no-cache')] + if optimized: + command.append('-O') + run = subprocess.run(command+args, cwd=out, capture_output=True, text=True, timeout=30, + env={'PATH': ''}) + need(run.returncode != 0 and 'ValueError' in run.stderr, 'semantic mutation survived: '+name) + results.append({'mutation': name, 'optimized': optimized, + 'diagnostic': run.stderr.strip().splitlines()[-1]}) + print(json.dumps({'status': 'PASS_FINITE_MEMORY_SEMANTIC_MUTATIONS', 'checks': results}, + sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/finite-memory-lifting/certify.py b/research/finite-memory-lifting/certify.py new file mode 100644 index 0000000000..8fc690872d --- /dev/null +++ b/research/finite-memory-lifting/certify.py @@ -0,0 +1,100 @@ +"""Reachable-row certificate producer for positive tensor widths. + +The algorithm is classical weighted-automata equivalence, used here on +concrete physical column entries. Apache-2.0; OpenAI Codex assistance. +""" +import argparse +import json +from exact import G, encode, fingerprint, load, need, parse, rowmul + + +class Basis: + def __init__(self, width): + self.width = width + self.rows, self.echelon, self.pivots, self.transforms = [], [], [], [] + + def reduce(self, v): + w = list(v) + coordinates = [G() for _ in self.rows] + for e, pivot, transform in zip(self.echelon, self.pivots, self.transforms): + gain = w[pivot] + if gain: + w = [x-gain*y for x, y in zip(w, e)] + coordinates = [x+gain*y for x, y in zip(coordinates, transform)] + return w, coordinates + + def add(self, v): + w, coordinates = self.reduce(v) + pivot = next((i for i, x in enumerate(w) if x), None) + if pivot is None: + return False + gain = w[pivot] + for transform in self.transforms: + transform.append(G()) + self.rows.append(list(v)) + self.echelon.append([x/gain for x in w]) + self.pivots.append(pivot) + self.transforms.append([-x/gain for x in coordinates] + [G(1)/gain]) + return True + + def coordinates(self, v): + remainder, coordinates = self.reduce(v) + need(not any(remainder), 'closure not reached') + return coordinates + + +def certify(data, max_states=256): + _, n, p, q, left, right, transitions = parse(data, max_states) + symbols = sorted(transitions, key=lambda t: tuple(map(int, t.split(',')))) + basis = Basis(n) + labels = [] + first_bad = None + + def visit(v, output, word): + nonlocal first_bad + values = rowmul(v, right) + for j, z in enumerate(values): + if z and first_bad is None: + first_bad = {'kind': 'counterexample', 'problem_sha256': fingerprint(data), + 'word': word, 'output': output, 'input': j, + 'value': z.json(), 'width_bound': n} + if basis.add(v): + labels.append((output, word)) + + for symbol in symbols: + for i in range(p): + visit(rowmul(left[i], transitions[symbol]), i, [symbol]) + seed_rank = len(basis.rows) + if first_bad: + return first_bad + cursor = 0 + while cursor < len(basis.rows): + v = basis.rows[cursor] + output, word = labels[cursor] + for symbol in symbols: + visit(rowmul(v, transitions[symbol]), output, word + [symbol]) + if first_bad: + need(len(first_bad['word']) <= n-seed_rank+1, 'short-witness bound') + return first_bad + cursor += 1 + r = len(basis.rows) + return {'kind': 'all_positive_widths', 'problem_sha256': fingerprint(data), + 'rank': r, 'positive_seed_rank': seed_rank, + 'basis': encode(basis.rows), + 'seeds': {s: encode([basis.coordinates(rowmul(v, transitions[s])) for v in left]) + for s in symbols}, + 'closure': {s: encode([basis.coordinates(rowmul(v, transitions[s])) + for v in basis.rows]) for s in symbols}, + 'width_bound': n} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('problem') + parser.add_argument('--max-states', type=int, default=256) + args = parser.parse_args() + print(json.dumps(certify(load(args.problem), args.max_states), indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/finite-memory-lifting/check_certificate.py b/research/finite-memory-lifting/check_certificate.py new file mode 100644 index 0000000000..99d3289765 --- /dev/null +++ b/research/finite-memory-lifting/check_certificate.py @@ -0,0 +1,76 @@ +"""Check finite-memory equality or one literal physical entry discrepancy. + +No producer import, basis search or elimination. Arithmetic/parser are shared +with the producer. Apache-2.0; substantial OpenAI Codex assistance. +""" +import argparse +from exact import G, fingerprint, load, matrix, need, parse + + +def check(data, certificate, max_states=256): + d, n, p, q, left, right, transitions = parse(data, max_states) + c = certificate + need(isinstance(c, dict) and c.get('problem_sha256') == fingerprint(data), 'problem binding') + need(type(c.get('width_bound')) is int and c['width_bound'] == n, 'width bound') + if c.get('kind') == 'counterexample': + need(set(c) == {'kind', 'problem_sha256', 'word', 'output', 'input', + 'value', 'width_bound'}, 'counterexample fields') + word, i, j = c['word'], c['output'], c['input'] + need(isinstance(word, list) and 1 <= len(word) <= n, 'positive witness width') + need(type(i) is int and type(j) is int and 0 <= i < p and 0 <= j < q, 'endpoint channel') + v = list(left[i]) + for symbol in word: + need(symbol in transitions, 'unknown witness symbol') + a = transitions[symbol] + v = [sum((v[k]*a[k][h] for k in range(n)), G()) for h in range(n)] + value = sum((v[k]*right[k][j] for k in range(n)), G()) + from exact import scalar + need(value and value == scalar(c['value']), 'literal nonzero discrepancy') + return {'status': 'PASS_PHYSICAL_COUNTEREXAMPLE', 'width': len(word), + 'output_column': [int(s.split(',')[0]) for s in word], + 'input_column': [int(s.split(',')[1]) for s in word], + 'output_role': i, 'input_role': j, 'value': value.json()} + need(c.get('kind') == 'all_positive_widths', 'certificate kind') + need(set(c) == {'kind', 'problem_sha256', 'rank', 'positive_seed_rank', 'basis', + 'seeds', 'closure', 'width_bound'}, 'equality fields') + r = c['rank'] + need(type(r) is int and 0 <= r <= n, 'certificate rank') + seed_rank = c['positive_seed_rank'] + need(type(seed_rank) is int and 0 <= seed_rank <= r, 'seed rank range') + # Independence and the advertised seed rank are producer diagnostics. The + # checker needs only a spanning invariant set, not an optimal basis. + rows = matrix(c['basis'], r, n) + need(isinstance(c['seeds'], dict) and set(c['seeds']) == set(transitions), 'all seed symbols') + need(isinstance(c['closure'], dict) and set(c['closure']) == set(transitions), 'all closure symbols') + for s, t in transitions.items(): + seeds = matrix(c['seeds'][s], p, r) + closure = matrix(c['closure'][s], r, r) + for i in range(p): + for j in range(n): + actual = sum((left[i][k]*t[k][j] for k in range(n)), G()) + claimed = sum((seeds[i][k]*rows[k][j] for k in range(r)), G()) + need(actual == claimed, 'positive seed containment') + for i in range(r): + for j in range(n): + actual = sum((rows[i][k]*t[k][j] for k in range(n)), G()) + claimed = sum((closure[i][k]*rows[k][j] for k in range(r)), G()) + need(actual == claimed, 'transition closure') + for i in range(r): + for j in range(q): + need(not sum((rows[i][k]*right[k][j] for k in range(n)), G()), 'all returned channels') + return {'status': 'PASS_ALL_POSITIVE_WIDTHS', 'invariant_rows': r, + 'states': n, 'local_dimension': d, 'outputs': p, 'inputs': q} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('problem') + parser.add_argument('certificate') + parser.add_argument('--max-states', type=int, default=256) + args = parser.parse_args() + import json + print(json.dumps(check(load(args.problem), load(args.certificate), args.max_states), indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/finite-memory-lifting/exact.py b/research/finite-memory-lifting/exact.py new file mode 100644 index 0000000000..634f1f1313 --- /dev/null +++ b/research/finite-memory-lifting/exact.py @@ -0,0 +1,139 @@ +"""Small exact Q(i) arithmetic and strict transfer-table parsing. + +Apache-2.0; substantial OpenAI Codex assistance. +""" +from fractions import Fraction +import hashlib +import json +import re + + +def need(value, message): + if not value: + raise ValueError(message) + + +class G: + __slots__ = ('a', 'b') + + def __init__(self, a=0, b=0): + if isinstance(a, G): + self.a, self.b = a.a, a.b + else: + self.a, self.b = Fraction(a), Fraction(b) + + def __add__(self, other): + z = G(other) + return G(self.a + z.a, self.b + z.b) + + __radd__ = __add__ + + def __neg__(self): + return G(-self.a, -self.b) + + def __sub__(self, other): + return self + -G(other) + + def __mul__(self, other): + z = G(other) + return G(self.a*z.a - self.b*z.b, self.a*z.b + self.b*z.a) + + __rmul__ = __mul__ + + def __truediv__(self, other): + z = G(other) + den = z.a*z.a + z.b*z.b + need(bool(den), 'zero divisor in coefficient field') + return G((self.a*z.a + self.b*z.b)/den, + (self.b*z.a - self.a*z.b)/den) + + def __bool__(self): + return bool(self.a or self.b) + + def __eq__(self, other): + if not isinstance(other, (G, int, Fraction)): + return False + z = G(other) + return self.a == z.a and self.b == z.b + + def json(self): + return str(self.a) if not self.b else [str(self.a), str(self.b)] + + +def scalar(x): + def part(t): + need(type(t) is int or (isinstance(t, str) and + re.fullmatch(r'[+-]?\d+(?:/[+-]?\d+)?', t, flags=re.ASCII)), + 'explicit integer/fraction coefficient required') + return Fraction(t) + if isinstance(x, list): + need(len(x) == 2, 'Gaussian pair required') + return G(part(x[0]), part(x[1])) + return G(part(x)) + + +def zeros(rows, cols): + return [[G() for _ in range(cols)] for _ in range(rows)] + + +def mm(a, b): + need(bool(a) and bool(b) and len(a[0]) == len(b), 'matrix product shape') + c = zeros(len(a), len(b[0])) + for i, row in enumerate(a): + for k, x in enumerate(row): + if x: + for j, y in enumerate(b[k]): + if y: + c[i][j] = c[i][j] + x*y + return c + + +def rowmul(v, a): + return mm([v], a)[0] + + +def encode(a): + return [[G(x).json() for x in row] for row in a] + + +def matrix(a, rows, cols): + need(isinstance(a, list) and len(a) == rows, 'matrix row count') + need(all(isinstance(row, list) and len(row) == cols for row in a), 'matrix column count') + return [[scalar(x) for x in row] for row in a] + + +def fingerprint(data): + return hashlib.sha256(json.dumps(data, sort_keys=True, separators=(',', ':'), + ensure_ascii=True).encode()).hexdigest() + + +def parse(data, max_states=256): + need(isinstance(data, dict), 'problem object required') + need(set(data) == {'local_dimension', 'states', 'outputs', 'inputs', + 'left', 'right', 'transitions'}, 'exact problem fields required') + d, n, p, q = (data[k] for k in ('local_dimension', 'states', 'outputs', 'inputs')) + need(all(type(x) is int and x > 0 for x in (d, n, p, q)), 'positive dimensions required') + need(n <= max_states, 'state budget exceeded: no decision') + left, right = matrix(data['left'], p, n), matrix(data['right'], n, q) + need(isinstance(data['transitions'], dict), 'transition object required') + trans = {} + for symbol, a in data['transitions'].items(): + need(isinstance(symbol, str) and re.fullmatch(r'\d+,\d+', symbol, flags=re.ASCII), + 'symbol must be output,input indices') + y, x = map(int, symbol.split(',')) + need(0 <= y < d and 0 <= x < d and symbol == f'{y},{x}', 'noncanonical symbol') + trans[symbol] = matrix(a, n, n) + # Every omitted local matrix entry has the zero transition. This is an + # explicit sparse-table contract, not a promise about unexamined entries. + return d, n, p, q, left, right, trans + + +def load(path): + def unique(pairs): + result = {} + for k, v in pairs: + need(k not in result, 'duplicate JSON key') + result[k] = v + return result + with open(path, encoding='utf-8') as f: + return json.load(f, object_pairs_hook=unique) diff --git a/research/finite-memory-lifting/examples/hadamard-wrong-scale.certificate.json b/research/finite-memory-lifting/examples/hadamard-wrong-scale.certificate.json new file mode 100644 index 0000000000..5e20900be4 --- /dev/null +++ b/research/finite-memory-lifting/examples/hadamard-wrong-scale.certificate.json @@ -0,0 +1,12 @@ +{ + "kind": "counterexample", + "problem_sha256": "6d2cadb642e9c3e3395ab59260b1cfc05a0121788141d0f1c6c8cc69569a078e", + "word": [ + "0,0", + "0,0" + ], + "output": 0, + "input": 0, + "value": "2", + "width_bound": 2 +} diff --git a/research/finite-memory-lifting/examples/hadamard-wrong-scale.json b/research/finite-memory-lifting/examples/hadamard-wrong-scale.json new file mode 100644 index 0000000000..187fd1b573 --- /dev/null +++ b/research/finite-memory-lifting/examples/hadamard-wrong-scale.json @@ -0,0 +1,62 @@ +{ + "local_dimension": 2, + "states": 2, + "outputs": 1, + "inputs": 1, + "left": [ + [ + "1", + "-2" + ] + ], + "right": [ + [ + "1" + ], + [ + "1" + ] + ], + "transitions": { + "0,0": [ + [ + "2", + "0" + ], + [ + "0", + "1" + ] + ], + "0,1": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "1,0": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "1,1": [ + [ + "2", + "0" + ], + [ + "0", + "1" + ] + ] + } +} diff --git a/research/finite-memory-lifting/examples/mixed-column-error.certificate.json b/research/finite-memory-lifting/examples/mixed-column-error.certificate.json new file mode 100644 index 0000000000..16cd20e0d0 --- /dev/null +++ b/research/finite-memory-lifting/examples/mixed-column-error.certificate.json @@ -0,0 +1,12 @@ +{ + "kind": "counterexample", + "problem_sha256": "6da62ac760c410d19b4bb3e61471ee345b563dac41051787356e906ded3cc255", + "word": [ + "0,0", + "1,1" + ], + "output": 0, + "input": 0, + "value": "1", + "width_bound": 3 +} diff --git a/research/finite-memory-lifting/examples/mixed-column-error.json b/research/finite-memory-lifting/examples/mixed-column-error.json new file mode 100644 index 0000000000..4ea66ea982 --- /dev/null +++ b/research/finite-memory-lifting/examples/mixed-column-error.json @@ -0,0 +1,60 @@ +{ + "local_dimension": 2, + "states": 3, + "outputs": 1, + "inputs": 1, + "left": [ + [ + "1", + "0", + "0" + ] + ], + "right": [ + [ + "0" + ], + [ + "0" + ], + [ + "1" + ] + ], + "transitions": { + "0,0": [ + [ + "0", + "1", + "0" + ], + [ + "0", + "0", + "0" + ], + [ + "0", + "0", + "0" + ] + ], + "1,1": [ + [ + "0", + "0", + "0" + ], + [ + "0", + "0", + "1" + ], + [ + "0", + "0", + "0" + ] + ] + } +} diff --git a/research/finite-memory-lifting/examples/prefix-inverse.certificate.json b/research/finite-memory-lifting/examples/prefix-inverse.certificate.json new file mode 100644 index 0000000000..66a01d17e8 --- /dev/null +++ b/research/finite-memory-lifting/examples/prefix-inverse.certificate.json @@ -0,0 +1,91 @@ +{ + "kind": "all_positive_widths", + "problem_sha256": "76d488572cf2db9e01627ff386faa234a94d5ff835ea0e286e80bfa6c7ff3931", + "rank": 2, + "positive_seed_rank": 2, + "basis": [ + [ + "1", + "0", + "0", + "0", + "-1" + ], + [ + "0", + "0", + "0", + "1", + "-1" + ] + ], + "seeds": { + "0,0": [ + [ + "1", + "0" + ] + ], + "0,1": [ + [ + "0", + "0" + ] + ], + "1,0": [ + [ + "0", + "0" + ] + ], + "1,1": [ + [ + "0", + "1" + ] + ] + }, + "closure": { + "0,0": [ + [ + "1", + "0" + ], + [ + "0", + "1" + ] + ], + "0,1": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "1,0": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "1,1": [ + [ + "0", + "1" + ], + [ + "1", + "0" + ] + ] + }, + "width_bound": 5 +} diff --git a/research/finite-memory-lifting/examples/prefix-inverse.json b/research/finite-memory-lifting/examples/prefix-inverse.json new file mode 100644 index 0000000000..5617e15879 --- /dev/null +++ b/research/finite-memory-lifting/examples/prefix-inverse.json @@ -0,0 +1,182 @@ +{ + "local_dimension": 2, + "states": 5, + "outputs": 1, + "inputs": 1, + "left": [ + [ + "1", + "0", + "0", + "0", + "-1" + ] + ], + "right": [ + [ + "1" + ], + [ + "1" + ], + [ + "1" + ], + [ + "1" + ], + [ + "1" + ] + ], + "transitions": { + "0,0": [ + [ + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1" + ] + ], + "0,1": [ + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ] + ], + "1,0": [ + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "1", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ] + ], + "1,1": [ + [ + "0", + "0", + "0", + "1", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "1" + ] + ] + } +} diff --git a/research/finite-memory-lifting/models.py b/research/finite-memory-lifting/models.py new file mode 100644 index 0000000000..a1381d66c2 --- /dev/null +++ b/research/finite-memory-lifting/models.py @@ -0,0 +1,201 @@ +"""Explicit matrix-product operator constructors, not a physical-cost compiler. + +Apache-2.0; substantial OpenAI Codex assistance. +""" +from dataclasses import dataclass +from exact import G, encode, need, scalar, zeros + + +def identity(n): + return [[G(i == j) for j in range(n)] for i in range(n)] + + +def kron_vector(a, b): + return [x*y for x in a for y in b] + + +def kron(a, b): + n, m = len(a), len(b) + c = zeros(n*m, n*m) + for i in range(n): + for j in range(n): + if a[i][j]: + for k in range(m): + for h in range(m): + if b[k][h]: + c[i*m+k][j*m+h] = a[i][j]*b[k][h] + return c + + +@dataclass +class MPO: + d: int + left: list + right: list + transitions: dict + + @property + def n(self): + return len(self.left) + + def problem(self): + return {'local_dimension': self.d, 'states': self.n, 'outputs': 1, 'inputs': 1, + 'left': encode([self.left]), 'right': encode([[x] for x in self.right]), + 'transitions': {f'{y},{x}': encode(a) + for (y, x), a in sorted(self.transitions.items())}} + + +def local(d, entries): + return MPO(d, [G(1)], [G(1)], + {key: [[G(value)]] for key, value in entries.items() if value}) + + +def unit(d): + return local(d, {(i, i): G(1) for i in range(d)}) + + +def zero(d): + return MPO(d, [G()], [G(1)], {}) + + +def scale(a, c): + if not c: + return zero(a.d) + return MPO(a.d, [c*x for x in a.left], a.right, a.transitions) + + +def add(a, b): + need(a.d == b.d, 'sum local dimension') + if not any(a.left) or not a.transitions: + return b + if not any(b.left) or not b.transitions: + return a + n, m = a.n, b.n + trans = {} + for key in set(a.transitions) | set(b.transitions): + c = zeros(n+m, n+m) + for offset, size, t in ((0, n, a.transitions.get(key)), (n, m, b.transitions.get(key))): + if t is not None: + for i in range(size): + for j in range(size): + c[offset+i][offset+j] = t[i][j] + trans[key] = c + return MPO(a.d, a.left+b.left, a.right+b.right, trans) + + +def difference(a, b): + return add(a, scale(b, G(-1))) + + +def compose(a, b): + """a after b; contract the same intermediate physical column entry.""" + need(a.d == b.d, 'composition local dimension') + if not any(a.left) or not any(b.left) or not a.transitions or not b.transitions: + return zero(a.d) + by_input, by_output = {}, {} + for (y, z), t in a.transitions.items(): + by_input.setdefault(z, []).append((y, t)) + for (z, x), t in b.transitions.items(): + by_output.setdefault(z, []).append((x, t)) + trans = {} + size = a.n*b.n + for z in by_input.keys() & by_output.keys(): + for y, at in by_input[z]: + for x, bt in by_output[z]: + term = kron(at, bt) + if (y, x) not in trans: + trans[y, x] = term + else: + old = trans[y, x] + trans[y, x] = [[u+v for u, v in zip(row, addrow)] + for row, addrow in zip(old, term)] + return MPO(a.d, kron_vector(a.left, b.left), kron_vector(a.right, b.right), trans) + + +def transpose(a): + return MPO(a.d, a.left, a.right, {(x, y): t for (y, x), t in a.transitions.items()}) + + +def recurrence(a, transition, left, right): + """Multiply the width-f operator by left * transition^f * right.""" + return MPO(a.d, kron_vector(a.left, left), kron_vector(a.right, right), + {s: kron(t, transition) for s, t in a.transitions.items()}) + + +def prefix_xor(d=2, bit=0): + need(d > 1 and d & (d-1) == 0 and 0 <= bit < d.bit_length()-1, 'binary column space') + trans = {} + for x in range(d): + for previous in range(2): + y = x ^ (previous << bit) + t = zeros(2, 2) + t[previous][(y >> bit) & 1] = G(1) + trans[y, x] = t + return MPO(d, [G(1), G()], [G(1), G(1)], trans) + + +def cyclic_delay(n, d=1): + t = zeros(n, n) + for i in range(n): + t[i][(i+1) % n] = G(1) + return MPO(d, [G(i == 0) for i in range(n)], [G(i == 0) for i in range(n)], + {(i, i): t for i in range(d)}) + + +def native_entries(recipe, n): + """Literal source convention: upper quadratic entries, phase at input.""" + entries = {} + phases = (G(1), G(0, 1), G(-1), G(0, -1)) + for x in range(1 << n): + y = recipe['offset'] + for j, row in enumerate(recipe['matrix_rows']): + y ^= ((row & x).bit_count() & 1) << j + exponent = recipe['phase'] + for i in range(n): + if x >> i & 1: + exponent += recipe['linear_Z4'][i] + exponent += 2*sum(1 for j in range(i+1, n) + if x >> j & 1 and recipe['quadratic_rows'][i] >> j & 1) + entries[y, x] = phases[exponent % 4] + need(len({y for y, _ in entries}) == 1 << n, 'source permutation must be invertible') + return entries + + +def native_frontend(data): + """Compile every owner/input block of the supplied finite literal word. + + Local products are composed before tensor lifting only when both operands + have one virtual state; exterior register coefficients stay in boundaries. + """ + n, roles = data['axes'], data['roles'] + d = 1 << n + operators = {} + for name, recipe in data['generators'].items(): + entries = native_entries(recipe, n) + operators[name, False] = local(d, entries) + operators[name, True] = local(d, {(x, y): G(1)/v for (y, x), v in entries.items()}) + + def compile_word(word): + state = [[unit(d) if i == j else zero(d) for j in range(roles)] for i in range(roles)] + for op in word: + kind, dst = op['op'], op['dst'] + need(kind in ('apply', 'add', 'query', 'scale', 'swap'), 'unsupported source instruction') + if kind == 'apply': + a = operators[op['generator'], op.get('inverse', False)] + state[dst] = [compose(a, v) for v in state[dst]] + elif kind == 'scale': + c = scalar(op['coefficient']) + state[dst] = [scale(v, c) for v in state[dst]] + elif kind == 'swap': + src = op['src'] + state[dst], state[src] = state[src], state[dst] + else: + src = op['src'] + before_src, before_dst = list(state[src]), list(state[dst]) + c = scalar(op.get('coefficient', 1)) + a = operators[op['generator'], op.get('inverse', False)] if kind == 'query' else None + state[dst] = [add(v, scale(compose(a, u) if a else u, c)) + for v, u in zip(before_dst, before_src)] + return state + actual, expected = compile_word(data['program']), compile_word(data['reference']) + return [[difference(actual[i][j], expected[i][j]) for j in range(roles)] for i in range(roles)] diff --git a/research/finite-memory-lifting/verify.py b/research/finite-memory-lifting/verify.py new file mode 100644 index 0000000000..13efb9d12f --- /dev/null +++ b/research/finite-memory-lifting/verify.py @@ -0,0 +1,412 @@ +#!/usr/bin/env python3 +"""Bounded exact calibration; universal claims are proved in PROOF.md. + +Apache-2.0; substantial OpenAI Codex assistance. +""" +from copy import deepcopy +from fractions import Fraction +from itertools import product +from pathlib import Path +import argparse +import hashlib +import json +import random +import subprocess +import sys +import tempfile + +from exact import G, fingerprint, load, need, parse, rowmul, zeros +from certify import certify +from check_certificate import check +from models import (MPO, add, compose, cyclic_delay, difference, identity, + local, native_frontend, prefix_xor, recurrence, scale, + transpose, unit) + +ROOT = Path(__file__).resolve().parent + + +def literal_entry(data, word, output=0, source=0): + """Separate path-sum oracle; it does not use the producer's row updates.""" + _, n, _, _, left, right, trans = parse(data) + total = G() + for path in product(range(n), repeat=len(word)+1): + value = left[output][path[0]]*right[path[-1]][source] + if not value: + continue + for j, symbol in enumerate(word): + value = value*trans[symbol][path[j]][path[j+1]] + if not value: + break + total = total+value + return total + + +def entry(a, outputs, inputs): + v = list(a.left) + for y, x in zip(outputs, inputs): + t = a.transitions.get((y, x)) + if t is None: + return G() + v = rowmul(v, t) + return sum((x*y for x, y in zip(v, a.right)), G()) + + +def verified(a, expected): + data = a.problem() if isinstance(a, MPO) else a + certificate = certify(data) + need(certificate['kind'] == expected, 'unexpected decision') + result = check(data, certificate) + return data, certificate, result + + +def core_suite(): + rng = random.Random(20261024) + differential = 0 + for n in range(1, 4): + for _ in range(8): + a = MPO(2, [G(rng.randrange(-1, 2)) for _ in range(n)], + [G(rng.randrange(-1, 2)) for _ in range(n)], + {(y, x): [[G(rng.randrange(-1, 2)) for _ in range(n)] for _ in range(n)] + for y in range(2) for x in range(2)}) + data = a.problem() + certificate = certify(data) + check(data, certificate) + if certificate['kind'] == 'counterexample': + value = literal_entry(data, certificate['word']) + from exact import scalar + need(value == scalar(certificate['value']) and value, 'path-sum discrepancy') + differential += 1 + else: + for width in range(1, n+1): + for word in product(sorted(data['transitions']), repeat=width): + need(not literal_entry(data, word), 'path-sum equality') + differential += 1 + # A correct positive-width identity can fail at the empty word. + empty_only = MPO(1, [G(1)], [G(1)], {(0, 0): [[G()]]}) + verified(empty_only, 'all_positive_widths') + need(sum((x*y for x, y in zip(empty_only.left, empty_only.right)), G()) == 1, + 'empty-width discriminator') + # Uniform repeated columns miss a mixed-column defect. + a, b = zeros(3, 3), zeros(3, 3) + a[0][1], b[1][2] = G(1), G(1) + mixed = MPO(2, [G(1), G(), G()], [G(), G(), G(1)], {(0, 0): a, (1, 1): b}) + _, mixed_certificate, _ = verified(mixed, 'counterexample') + need(len(mixed_certificate['word']) == 2, 'mixed-word witness') + for width in range(1, 9): + for bit in range(2): + need(not entry(mixed, [bit]*width, [bit]*width), 'uniform-column false positive') + sharp = [] + for n in range(1, 13): + a = cyclic_delay(n) + _, c, _ = verified(a, 'counterexample') + need(len(c['word']) == n, 'positive-width cutoff is sharp') + for width in range(1, n): + need(not entry(a, [0]*width, [0]*width), 'delayed first discrepancy') + sharp.append(n) + x = local(2, {(0, 1): 1, (1, 0): 1}) + z = local(2, {(0, 0): 1, (1, 1): -1}) + xz = compose(x, z) + for i in range(2): + for j in range(2): + wanted = (-1 if j else 1) if i == 1-j else 0 + need(entry(xz, [i], [j]) == wanted, 'noncommuting composition order') + verified(difference(compose(x, z), compose(z, x)), 'counterexample') + w = local(2, {(0, 0): 1, (0, 1): 1, (1, 0): 1, (1, 1): -1}) + wrong = difference(compose(w, w), scale(unit(2), G(2))) + _, c, _ = verified(wrong, 'counterexample') + need(len(c['word']) == 2, 'exterior scalar must not be tensor-powered') + right = recurrence(unit(2), [[G(2)]], [G(1)], [G(1)]) + verified(difference(compose(w, w), right), 'all_positive_widths') + jordan = [[G(1), G(1)], [G(), G(1)]] + linear_width = recurrence(unit(2), jordan, [G(1), G()], [G(), G(1)]) + for width in range(1, 10): + need(entry(linear_width, [0]*width, [0]*width) == width, 'recurrent width coefficient') + phase = local(2, {(0, 0): G(0, 1), (1, 1): G(0, 1)}) + phase_error = difference(phase, unit(2)) + verified(phase_error, 'counterexample') + cycle4 = cyclic_delay(4) + filtered = recurrence(phase_error, cycle4.transitions[0, 0], cycle4.left, cycle4.right) + verified(filtered, 'all_positive_widths') + # Infinite-order Q(i) unitary and a nonlinear local permutation. + alpha = G(Fraction(3, 5), Fraction(4, 5)) + t = local(2, {(0, 0): 1, (1, 1): alpha}) + tinv = local(2, {(0, 0): 1, (1, 1): G(1)/alpha}) + verified(difference(compose(tinv, t), unit(2)), 'all_positive_widths') + tof = local(8, {(x ^ (4 if x & 3 == 3 else 0), x): 1 for x in range(8)}) + verified(difference(compose(tof, tof), unit(8)), 'all_positive_widths') + # A defect exclusively on a later borrowed/rectangular channel must be + # reported; checking only the first demanded block would miss it. + roles = {'local_dimension': 1, 'states': 1, 'outputs': 2, 'inputs': 3, + 'left': [[0], [1]], 'right': [[0, 0, 1]], 'transitions': {'0,0': [[1]]}} + _, c, witness = verified(roles, 'counterexample') + need((c['output'], c['input']) == (1, 2), 'all independent rectangular role channels') + complete_zero = {'local_dimension': 1, 'states': 2, 'outputs': 2, 'inputs': 3, + 'left': [[1, 0], [2, 0]], 'right': [[0, 0, 0], [1, 2, 3]], + 'transitions': {'0,0': [[1, 0], [0, 0]]}} + verified(complete_zero, 'all_positive_widths') + return {'path_sum_comparisons': differential, 'random_transducers': 24, + 'sharp_first_failure_widths': sharp, 'mixed_word_width': 2, + 'wrong_Hadamard_scale_failure_width': 2, + 'recurrence_widths': 9, 'phase_filter_period': 4, + 'rectangular_role_controls': 2} + + +def column_suite(): + p = prefix_xor() + pinv = transpose(p) + positive = difference(compose(pinv, p), unit(2)) + data, cert, _ = verified(positive, 'all_positive_widths') + columns = 0 + for width in range(1, 7): + for bits in product(range(2), repeat=width): + total = 0 + out = [] + for x in bits: + total ^= x + out.append(total) + need(entry(p, out, bits) == 1, 'literal prefix action') + need(entry(pinv, bits, out) == 1, 'literal inverse action') + columns += 1 + # Every output entry through width four, not just its deterministic image. + all_entries = 0 + for width in range(1, 5): + for x in product(range(2), repeat=width): + y_expected = tuple(sum(x[:j+1]) % 2 for j in range(width)) + for y in product(range(2), repeat=width): + need(entry(p, y, x) == int(y == y_expected), 'complete prefix matrix') + all_entries += 1 + # Witness that this is outside sums of identical one-column tensor powers. + # Swapping two columns and taking prefix XOR do not commute. + need(entry(p, [1, 1], [1, 0]) == 1 and entry(p, [1, 1], [0, 1]) == 0, + 'column-permutation noncommutation') + u = ((0, 0), (1, 1)) + v = ((0, 0), (1, 0)) + hankel = [[entry(p, [a[0], b[0]], [a[1], b[1]]) for b in v] for a in u] + need(hankel == identity(2), 'prefix Hankel minor') + return {'literal_prefix_columns': columns, 'complete_prefix_entries': all_entries, + 'inverse_certificate_states': data['states'], 'invariant_rows': cert['rank'], + 'exact_minimum_prefix_bond': 2}, data, cert + + +def routing_suite(): + counts = [] + for k in range(1, 5): + half = 1 << k + size = half*half + # Flatten the half-swap coefficient tensor at the middle cut. + # Row=(y_left,x_left), column=(y_right,x_right). + rows, cols = [], [] + for yl in range(half): + supported = [] + for xl in range(half): + column = xl*half+yl + supported.append(column) + cols.append(column) + rows.append(yl*half+xl) + for yr in range(half): + for xr in range(half): + value = int(yl == xr and yr == xl) + need(value == int(yr*half+xr == column), 'half-swap unfolding entry') + need(len(supported) == half, 'row indexing') + need(sorted(rows) == list(range(size)) and sorted(cols) == list(range(size)), + 'unfolding is a full permutation matrix') + # Rank-D column projection has exactly the stated discarded energy. + for bond in (0, 1, size//2, size): + discarded_square = sum(1 for j in cols if j >= bond) + need(discarded_square == size-bond, 'sharp unfolding Frobenius tail') + counts.append({'width': 2*k, 'unfolding_rank': size, 'entry_checks': size*size}) + walsh = [] + for k in range(1, 7): + size = 1 << k + h = [[G(-1 if (a & b).bit_count() % 2 else 1) for b in range(size)] + for a in range(size)] + for a in range(size): + for b in range(size): + # Integer evaluation is an independent exact Gram oracle. + inner = sum((-1 if ((a ^ b) & t).bit_count() % 2 else 1) + for t in range(size)) + need(inner == (size if a == b else 0), 'paired-phase Walsh Gram') + for bond in (0, 1, size//2, size): + discarded = sum(1 for row in h for j in range(bond, size) if row[j]) + need(discarded == size*(size-bond), 'paired-phase discarded energy') + walsh.append({'width': 2*k, 'cut_rank': size, 'squared_singular_value': size}) + return {'half_swaps': counts, 'paired_quadratic_phases': walsh} + + +def approximate_cutoff_control(): + # A fixed unitary per instance can pass small-width tolerance checks and + # still have a large late-width error. All comparisons are exact rationals. + cases = [] + for n in (16, 64, 128): + alpha = G(n, 1)/G(n, -1) + value = G(1) + for width in range(1, 9): + value = value*alpha + error = value-G(1) + square = error.a*error.a+error.b*error.b + need(square <= Fraction(4*width*width, n*n), 'short-width unitary tolerance') + late = 3*n//2 + value = G(1) + for _ in range(late): + value = value*alpha + error = value-G(1) + need(error.a*error.a+error.b*error.b > 2, 'large late unitary error') + cases.append({'parameter': n, 'early_widths': 8, 'late_width': late, + 'late_error_squared_exceeds': 2}) + return cases + + +def source_suite(): + sources = load(ROOT/'SOURCES.json') + source_row = next(row for row in sources['files'] + if row['path'] == 'research/native-tensor-cutoff/examples/source-conjugation.json') + need(hashlib.sha256((ROOT/'SOURCE-FIXTURE.json').read_bytes()).hexdigest() == source_row['sha256'], + 'portable literal source fixture hash') + fixture = load(ROOT/'SOURCE-FIXTURE.json') + blocks = native_frontend(fixture) + certificates = [] + for i, row in enumerate(blocks): + for j, block in enumerate(row): + data, cert, _ = verified(block, 'all_positive_widths') + certificates.append({'output': i, 'input': j, 'states': data['states'], + 'invariant_rows': cert['rank']}) + # Independently enumerate the literal conjugation on all source addresses. + n = fixture['axes'] + units = (G(1), G(0, 1), G(-1), G(0, -1)) + + def literal(recipe, address): + bits = [(address >> j) & 1 for j in range(n)] + out = [((recipe['offset'] >> j) & 1) ^ + (sum(bits[k] for k in range(n) if recipe['matrix_rows'][j] >> k & 1) % 2) + for j in range(n)] + phase = recipe['phase'] + sum(a*b for a, b in zip(recipe['linear_Z4'], bits)) + for j in range(n): + for k in range(j+1, n): + phase += 2*bits[j]*bits[k]*((recipe['quadratic_rows'][j] >> k) & 1) + return sum(bit << j for j, bit in enumerate(out)), units[phase % 4] + + g, z, r = (fixture['generators'][s] for s in ('G', 'Z', 'R')) + inverse = {literal(g, x)[0]: (x, G(1)/literal(g, x)[1]) for x in range(1 << n)} + for x in range(1 << n): + a, pa = inverse[x] + b, pb = literal(z, a) + c, pc = literal(g, b) + target, phase = literal(r, x) + need((c, pa*pb*pc) == (target, phase), 'source conjugation all addresses') + p = prefix_xor(1 << n, 4) + encoded = compose(transpose(p), compose(blocks[1][0], p)) + data, cert, _ = verified(encoded, 'all_positive_widths') + changed = deepcopy(fixture) + changed['generators']['R']['phase'] = 0 + wrong = native_frontend(changed)[1][0] + _, mutation, _ = verified(wrong, 'counterexample') + need(len(mutation['word']) == 1, 'source absolute phase mutation') + return {'source_axes': n, 'source_instruction_count': len(fixture['program']), + 'independent_source_addresses': 1 << n, 'all_owner_blocks': certificates, + 'encoded_source_shear_states': data['states'], + 'encoded_source_invariant_rows': cert['rank'], + 'encoded_source_local_entries': len(data['transitions']), + 'absolute_phase_mutation_width': 1} + + +def controls(data, certificate): + rejected = [] + + def reject(name, problem, claim): + try: + check(problem, claim) + except (ValueError, ZeroDivisionError): + rejected.append(name) + else: + raise ValueError('control accepted: '+name) + + c = deepcopy(certificate); c['width_bound'] += 1 + reject('width-bound', data, c) + c = deepcopy(certificate); del c['seeds'][next(iter(c['seeds']))] + reject('missing-seed-symbol', data, c) + c = deepcopy(certificate); del c['closure'][next(iter(c['closure']))] + reject('missing-closure-symbol', data, c) + c = deepcopy(certificate) + symbol = next(iter(c['closure'])) + from exact import scalar + c['closure'][symbol][0][0] = (scalar(c['closure'][symbol][0][0])+G(1)).json() + reject('wrong-closure', data, c) + changed = deepcopy(data) + nonzero_column = next(j for j in range(data['states']) if any(scalar(v[j]) for v in certificate['basis'])) + changed['right'] = [[int(i == nonzero_column)] for i in range(data['states'])] + reject('changed-dirty-return-binding', changed, certificate) + c = deepcopy(certificate); c['problem_sha256'] = fingerprint(changed) + reject('changed-dirty-return-semantic', changed, c) + bad = deepcopy(data); bad['left'][0][0] = 0.5 + reject('float-coefficient', bad, certificate) + bad = deepcopy(data); bad['transitions']['01,0'] = bad['transitions'][next(iter(bad['transitions']))] + reject('noncanonical-alphabet-entry', bad, certificate) + _, negative, _ = verified(cyclic_delay(4), 'counterexample') + c = deepcopy(negative); c['value'] = 0 + reject('zero-counterexample', cyclic_delay(4).problem(), c) + c = deepcopy(negative); c['word'] = c['word'][:-1] + reject('wrong-counterexample-width', cyclic_delay(4).problem(), c) + return rejected + + +def standalone(data, certificate): + with tempfile.TemporaryDirectory(prefix='finite-memory-checker-') as folder: + out = Path(folder) + for name in ('exact.py', 'check_certificate.py'): + (out/name).write_bytes((ROOT/name).read_bytes()) + (out/'problem.json').write_text(json.dumps(data)) + (out/'certificate.json').write_text(json.dumps(certificate)) + before = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in out.iterdir()} + for p in out.iterdir(): + p.chmod(0o444) + out.chmod(0o555) + try: + for optimized in (False, True): + # Isolated mode excludes the script directory, so this standalone + # CLI deliberately uses -B and a private empty bytecode prefix. + args = [sys.executable, '-B', '-X', 'pycache_prefix='+str(out/'absent-cache')] + if optimized: + args.append('-O') + args += [str(out/'check_certificate.py'), str(out/'problem.json'), str(out/'certificate.json')] + run = subprocess.run(args, cwd=out, env={'PATH': ''}, capture_output=True, text=True, timeout=30) + need(run.returncode == 0, 'standalone checker: '+run.stderr[-1000:]) + need(json.loads(run.stdout)['status'] == 'PASS_ALL_POSITIVE_WIDTHS', 'standalone output') + after = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in out.iterdir()} + need(before == after, 'standalone bytes/inventory changed') + finally: + out.chmod(0o755) + for p in out.iterdir(): + p.chmod(0o644) + return 'producer_absent_readonly_empty_PATH_normal_and_optimized' + + +def source_pins(root): + sources = load(ROOT/'SOURCES.json') + for row in sources['files']: + need(hashlib.sha256((Path(root)/row['path']).read_bytes()).hexdigest() == row['sha256'], + 'source hash: '+row['path']) + need((Path(root)/'research/native-tensor-cutoff/examples/source-conjugation.json').read_bytes() == + (ROOT/'SOURCE-FIXTURE.json').read_bytes(), 'literal source fixture equality') + return len(sources['files']) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--suite', choices=('all', 'core'), default='all') + parser.add_argument('--source-root') + args = parser.parse_args() + result = {'status': 'PASS_FINITE_MEMORY_LIFTING_CALIBRATION', 'core': core_suite()} + if args.suite == 'all': + result['columns'], data, cert = column_suite() + result['routing'] = routing_suite() + result['approximate_cutoff_controls'] = approximate_cutoff_control() + result['native'] = source_suite() + result['rejections'] = controls(data, cert) + result['standalone'] = standalone(data, cert) + if args.source_root: + source_pins(args.source_root) + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()