From 20165927fce9064a148774bcea412adf789a44f4 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:46:06 +0000 Subject: [PATCH] feat(research): prove sharp Gaussian overwrite clean capacity --- .../PROOF.md | 128 ++++++++++++++ .../README.md | 113 ++++++++++++ .../SOURCES.json | 18 ++ .../TASK.json | 118 +++++++++++++ .../VERIFY.json | 32 ++++ .../engine.py | 96 +++++++++++ .../verify.py | 163 ++++++++++++++++++ 7 files changed, 668 insertions(+) create mode 100644 research/gaussian-smith-reversible-capacity/PROOF.md create mode 100644 research/gaussian-smith-reversible-capacity/README.md create mode 100644 research/gaussian-smith-reversible-capacity/SOURCES.json create mode 100644 research/gaussian-smith-reversible-capacity/TASK.json create mode 100644 research/gaussian-smith-reversible-capacity/VERIFY.json create mode 100644 research/gaussian-smith-reversible-capacity/engine.py create mode 100644 research/gaussian-smith-reversible-capacity/verify.py diff --git a/research/gaussian-smith-reversible-capacity/PROOF.md b/research/gaussian-smith-reversible-capacity/PROOF.md new file mode 100644 index 0000000000..712f935ef6 --- /dev/null +++ b/research/gaussian-smith-reversible-capacity/PROOF.md @@ -0,0 +1,128 @@ +# Sharp clean capacity for reversible Gaussian overwrite + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and predecessor results + +Let pi=1+i, R_P=Z[i]/(pi^P), N=2^n, and +F(x)=C tensor n times x over R_P, where C=[[i,1],[1,i]]. +Both n and P are nonnegative integers. R_0 is the singleton ring. + +Ali Romman's [PR #5821](https://github.com/CrocSwap/integer-mult-bounds/pull/5821), +head `c137f338117e8a88816ce254efe3b1494809711f`, proves the response-image +information formula + + D(n,P) = sum_(j=0)^n binom(n,j) max(P-2j,0). + +It leaves reversible truncation and cleanup explicitly open in README question 4. +Its source is Dugongue's [PR #5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815), +head `f0fcda576df410dc15cd5b8183d4f74d284eba2b`, which supplies + + C = S diag(1,pi^2) T, + T(a,b) = (a-i*b,b), S(a,b) = (i*a,a+b). + +These are cited predecessor results, not claims of this contribution. Their +tensor factors T_n and S_n are permutations of R_P^N. The diagonal factor at +label u is multiplication by pi^(2|u|). The new result below concerns a +destructive reversible interface, unlike the predecessor's source-preserving +array computation. No predecessor census, precision theorem or invoice is +replayed as the deliverable. + +## Theorem + +Consider any permutation on a public field R_P^N, c initially zero bits, and +an arbitrary finite borrowed dirty field B. For every x and every initial +dirty value b, require the final public field to equal F(x). All auxiliary +outputs must stay within those c bits and B. Allow arbitrary reversible +mixing, nonlinear operations, and changes to the dirty field. + +The exact minimum c is + + K(n,P) = NP - D(n,P) + = sum_(j=0)^n binom(n,j) min(2j,P). + +A permutation attaining c=K can return B unchanged. This is a logical +reversible-encoding theorem, without a gate-count, running-time or tape claim. +The initially zero bits become retained output information. They are not +promised clean again at the end. + +### Necessity, including arbitrary dirty workspace + +Restrict the permutation to the allowed input slice where the c bits are zero. +There are 2^(NP)|B| distinct inputs in that slice. The required output field +has 2^D possibilities by the cited theorem. The remaining fields have at most +2^c|B| possibilities. Injectivity therefore requires + + 2^(NP)|B| <= 2^D 2^c |B|, + +and hence c>=NP-D. This argument permits the borrowed field to change. Requiring +its restoration cannot weaken the bound. It also permits an arbitrary finite +nonbinary B. Arbitrary initially unknown states do not supply clean capacity. + +### Sufficiency by explicit permutation + +Every element of R_P has a unique P-bit pi-adic representation + + z = sum_(t=0)^(P-1) d_t pi^t, d_t in {0,1}. + +Successive reduction modulo pi and exact division by pi prove uniqueness. +For a diagonal exponent 2|u|, put e=min(2|u|,P), q=P-e. +Write its P input bits as a q-bit low part l and an e-bit high part h. +Allocate e initially zero bits a. Apply the bit permutation + + (l,h,a) -> (a,l,h), + +where the first e+q=P output bits are the public coordinate and the last e +bits are the auxiliary coordinate. When a=0, the public coordinate represents +pi^e*l modulo pi^P, exactly pi^(2|u|)*z. The high part h retains the lost +information. For arbitrary a, this remains a permutation, with literal inverse + + (a,l,h) -> (l,h,a). + +If e=P, the entire public coordinate is swapped with its clean field. If e=0, +the step is the identity. Thus zero raw precision and zero tensor depth also +have valid endpoints. + +First apply T_n to the public field. Apply these disjoint coordinate +permutations, using a total of sum_u min(2|u|,P)=K clean bits. Finally apply +S_n to the public field. Tensoring the cited factorization proves that a zero +auxiliary input gives F(x). Composition proves a permutation on every public +and auxiliary state, not just on the allowed zero slice. Leave B untouched. +To invert, apply S_n inverse, the inverse coordinate permutations, and T_n +inverse. This construction attains the lower bound. + +## Consequences and scope + +For normalized precision p with the predecessor's raw exponent P=p+n, + + K = sum_j binom(n,j) min(2j,p+n). + +In particular, if p>=n, all exponents are unsaturated and + + K = sum_j binom(n,j) 2j = n 2^n. + +At p=n>0, the sharp initially clean capacity is half the public raw input +bit count, since that input has 2n 2^n bits. The attaining auxiliary output +retains those n 2^n bits. + +For n>0 and P>0, K>0. A reversible host cannot complete this overwrite and +reset all nonpublic fields while retaining only the rounded modular response. +If the c clean bits must finish zero, the output-count bound has factor one +in place of 2^c, and contradicts injectivity whenever K>0. Even allowing the +dirty field to change cannot repair that deficit. +Restoring the auxiliary to zero requires preserving or recovering additional +input information, changing the output contract, or permitting irreversible +erasure. An exact unrounded invertible response is a different contract. + +The predecessor preserves the original source. That source already retains +the information lost by F, so this overwrite lower bound does not apply to +its source-preserving compute-copy-uncompute route. This result neither +invalidates that route nor prices its additional passes. + +The all-size statement rests on this written argument and the cited Smith +and image theorems. The checker verifies new finite reversible augmentations, +including nonzero auxiliary states, inverse recovery, every individual lost +bit, and dirty-capacity inequalities. It does not reestablish the predecessor's +image theorem by counting its outputs. Physical reversible primitives, their +gate and tape costs, reusable clean restoration, the five selected framework +assumptions and any kappa improvement remain open here. diff --git a/research/gaussian-smith-reversible-capacity/README.md b/research/gaussian-smith-reversible-capacity/README.md new file mode 100644 index 0000000000..5be20d99d2 --- /dev/null +++ b/research/gaussian-smith-reversible-capacity/README.md @@ -0,0 +1,113 @@ +# Sharp clean storage for reversible Gaussian overwrite + +The exact initially clean storage for destructively overwriting +`C tensor n times x modulo pi^P`, with `C=[[i,1],[1,i]]` and `pi=1+i`, is + +```text +K(n,P) = sum_j binom(n,j) min(2j,P) bits. +``` + +This minimum allows arbitrary reversible mixing and arbitrary finite borrowed +dirty workspace, even if the dirty field may change. An explicit bit permutation +through the cited Smith factors attains it while leaving dirty workspace alone. +The retained auxiliary output cannot then be erased reversibly from the modular +response alone. This answers the destructive-overwrite portion of Open next +question 4 in [Ali Romman's PR #5821](https://github.com/CrocSwap/integer-mult-bounds/pull/5821). + +At normalized precision `p>=n`, raw precision is `P=p+n` and the sharp clean +capacity is `n*2^n` bits. At `p=n>0`, that is half the public raw input size. +These are storage bounds, without a time or kappa improvement. + +## Claim and evidence + +This is a scoped written mathematical proof with exact finite corroboration. +[PROOF.md](PROOF.md) states the contract, counting lower bound, attaining +permutation, inverse and cleanup consequence. The predecessor's image theorem +and Smith factors are cited; its image census and precision/cost replays are +not this contribution. The new verifier checks the augmented reversible map. + +The finite checks enumerate 17,898 full public/auxiliary states in 14 complete +permutations, including 646 clean-input endpoints. They also check 432 larger +interfaces, 272 clean endpoints, 1,492 individual retained-bit witnesses, +216 dirty-undercapacity comparisons, ten invalid-input controls and four +semantic controls. The verifier emits a generated SHA256-bound receipt to +stdout and writes no files. No receipt is hand-authored or stored in this package. + +The original `uniform-transfer-audit` card is explicitly changed to this +successor-interface result. It concerns `owned_erasure` and `precision_tape` +boundaries, but does not discharge an assumption of selected #5599. The source +preserving array contract remains different: retaining the original source +already retains the lost information. Physical reversible gates, tape routing, +operation costs, reusable clean restoration and independent human/formal +proof-kernel review remain unclaimed. The selected frontier is unchanged. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +PY=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 +"$PY" -W error -B research/gaussian-smith-reversible-capacity/verify.py +"$PY" -O -W error -B research/gaussian-smith-reversible-capacity/verify.py +"$PY" -B scripts/research_package.py --package research/gaussian-smith-reversible-capacity +"$PY" -B scripts/check_research_commit.py --package research/gaussian-smith-reversible-capacity --check-source-history +``` + +The last command checks publication bytes after committing. Both registered +commands have 30-second timeouts. Normal and optimized verification use explicit +exceptions, so optimization cannot remove the checks. A Git-free exported copy +can run the direct verifier from any working directory. Source history is +required only for metadata provenance and publication checks. No predecessor +code, Git object from a pending PR, network access or dependency installation +is needed by the scientific replay. + +## Execution bounds and implementation decisions + +Only `overwrite` and `dimensions` are the executable interface; arithmetic and +chart helpers receive validated internal values. The implementation caps depth +at 8 and raw precision at 16, hence 256 public coordinates and 4,096 bits in +each public/auxiliary field. This bound restricts the executable corroboration, +not the all-size written theorem. Exhaustive enumeration is separately capped +at 14 total bits. Larger fixtures use `n<=5`, `P<=8` and eight patterns per case. + +The implementation uses bounded loops without recursion, direct calls and no +generated code. Every function is under 60 physical lines. Runtime contracts +and verifier failures use exceptions that remain active under optimization. +Python requires dynamic object allocation, a Power of Ten rule 3 deviation. +Its scope is this bounded offline model. Fixed dimension limits, a maximum +16,384-entry exhaustive state set and the registered timeout bound resources; +no host-memory or physical-tape bound is inferred from Python execution. +A lower-level physical implementation would need its own allocation and +operation ledger. Warning-strict normal/optimized replay is the available +diagnostic check; separate Python static analyzers are unavailable on PATH. + +## Open next questions + +1. Implement the attaining pi-adic permutation on one permitted reversible + native/tape host. The clean-capacity optimum alone gives no operation bill. + Start with the one-axis map and charge chart conversion and each bit move; + the physical gate alphabet and representation contract are blockers. +2. Price source-preserving compute-copy-uncompute against destructive overwrite + plus retained kernel information for one real caller. Start by listing exactly + which source or kernel information the caller retains at its next cut. + Caller lifetimes and a complete paid bill are required before comparing routes. + +## Credit and provenance + +This contribution was produced by Nick Petalas. Apache-2.0. +Credit Ali Romman #5821 for the explicit open question and image-information +theorem; Dugongue #5815 for the Smith circuit and Gaussian correction context; +and the classical finite-ring cardinality and reversible-embedding arguments. +The Gaussian/native/controller/compiler lineage retained by those sources, +including Cinna Davis, Cao Yifan and the credited predecessor contributors, +remains theirs. Their files and credit lines are unchanged. + +The exact predecessor heads are recorded in [PROOF.md](PROOF.md) and +[TASK.json](TASK.json). They are literature references, not runtime dependencies. +[SOURCES.json](SOURCES.json) pins the task catalogue and selected-record +provenance at main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. +Live overlap checks included the handoff board, open PRs, this account's recent +PRs, concurrent reservations, exact main-text searches and merged-PR searches. +The cached helper searched 426 open PRs and 5,331 discussion records; its sparse +local notes covered 200 of 7,845 paths. Direct Git searches supplemented that +incomplete local coverage. No global literature-priority claim follows. diff --git a/research/gaussian-smith-reversible-capacity/SOURCES.json b/research/gaussian-smith-reversible-capacity/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/gaussian-smith-reversible-capacity/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/gaussian-smith-reversible-capacity/TASK.json b/research/gaussian-smith-reversible-capacity/TASK.json new file mode 100644 index 0000000000..6c554b75b7 --- /dev/null +++ b/research/gaussian-smith-reversible-capacity/TASK.json @@ -0,0 +1,118 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp initially clean bit capacity and attaining reversible permutation for destructive raw Gaussian tensor overwrite, with arbitrary finite dirty workspace.", + "scope_change_reason": "The user requests a new result rather than an audit. Answer PR5821 README Open next question 4 at the successor modular overwrite interface; do not claim to discharge a selected assumption.", + "bottleneck_link": "A source-preserving array reset does not supply a reversible destructive overwrite. The result prices the lost-information capacity exactly and identifies when retained source information is necessary; native and tape costs remain open.", + "budget_minutes": 60, + "stop_rule": "Ship this first sharp scoped capacity theorem and attaining interface once bounded local package and publication checks pass; do not extend to a physical implementation.", + "outcome": "completed", + "evidence": "Written lower bound and explicit all-state inverse; generated source-bound stdout receipt from normal/optimized finite replay. No predecessor image census is rerun.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Implement the attaining permutation on a permitted reversible native/tape host.", + "why_it_matters": "Logical clean capacity does not bound physical operations or movement.", + "first_step": "Implement and price the one-axis chart and bit permutation.", + "blocked_by": "Physical gate alphabet, representation and tape contract." + }, + { + "question": "Compare source-preserving cleanup with destructive overwrite plus retained kernel data at one real caller.", + "why_it_matters": "These interfaces retain different information and cannot share a cleanup invoice without justification.", + "first_step": "List the caller source/kernel information and lifetimes at its next cut.", + "blocked_by": "Actual caller schedule and complete paid-operation bill." + } + ], + "predecessors": [ + { + "pr": 5821, + "author": "Ali Romman", + "head": "c137f338117e8a88816ce254efe3b1494809711f", + "role": "README Open next question 4 and cited response-image theorem", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5821" + }, + { + "pr": 5815, + "author": "Dugongue", + "head": "f0fcda576df410dc15cd5b8183d4f74d284eba2b", + "role": "Cited Gaussian Smith factorization and retained construction lineage", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5815" + } + ], + "overlap": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214971", + "checked_at_utc": "2026-10-27T10:38:47Z", + "source": "PR #5821", + "scope": "Live handoffs and open PRs; recent own PRs; concurrent reservations; main text and merged title/body searches. Sparse helper local coverage is incomplete.", + "open_related_prs": [ + 5813, + 5815, + 5821, + 5825, + 5780 + ] + } +} diff --git a/research/gaussian-smith-reversible-capacity/VERIFY.json b/research/gaussian-smith-reversible-capacity/VERIFY.json new file mode 100644 index 0000000000..c65a6067c7 --- /dev/null +++ b/research/gaussian-smith-reversible-capacity/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Complete new public/auxiliary permutations, inverse recovery, required response endpoints, lost-bit witnesses, dirty capacity and rejection controls; generated source hashes." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "The same scientific checks with optimization; explicit exceptions preserve every assertion." + } + ] +} diff --git a/research/gaussian-smith-reversible-capacity/engine.py b/research/gaussian-smith-reversible-capacity/engine.py new file mode 100644 index 0000000000..b75ee0f6b5 --- /dev/null +++ b/research/gaussian-smith-reversible-capacity/engine.py @@ -0,0 +1,96 @@ +"""Finite logical reversible Gaussian overwrite interface. Apache-2.0.""" + +from math import comb + + +def dimensions(n: int, precision: int) -> tuple[int, int]: + """Bound this executable model; the written theorem has no such bounds.""" + if type(n) is not int or type(precision) is not int: + raise ValueError("depth and precision must be integers") + if not 0 <= n <= 8 or not 0 <= precision <= 16: + raise ValueError("executable bounds are 0 <= n <= 8, 0 <= P <= 16") + clean = sum(comb(n, j) * min(2 * j, precision) for j in range(n + 1)) + return 1 << n, clean + + +def gaussian(label: int, precision: int) -> tuple[int, int]: + """Evaluate the P binary pi-adic digits, pi=1+i.""" + real, imag, power_real, power_imag = 0, 0, 1, 0 + for j in range(precision): + if (label >> j) & 1: + real += power_real + imag += power_imag + power_real, power_imag = power_real - power_imag, power_real + power_imag + return real, imag + + +def residue(real: int, imag: int, precision: int) -> int: + """Extract P digits using exact division by pi after subtracting parity.""" + label = 0 + for j in range(precision): + digit = (real + imag) & 1 + label |= digit << j + real, imag = (real - digit + imag) // 2, (imag - real + digit) // 2 + return label + + +def chart(bank: tuple[int, ...], n: int, precision: int, kind: str) -> tuple[int, ...]: + """Apply cited unimodular tensor factors, without any truncation.""" + result = list(bank) + axes = range(n - 1, -1, -1) if kind.endswith("inv") else range(n) + for axis in axes: + for low in range(1 << n): + high = low | (1 << axis) + if low != high: + ar, ai = gaussian(result[low], precision) + br, bi = gaussian(result[high], precision) + if kind == "T": + first, second = (ar + bi, ai - br), (br, bi) + elif kind == "Tinv": + first, second = (ar - bi, ai + br), (br, bi) + elif kind == "S": + first, second = (-ai, ar), (ar + br, ai + bi) + elif kind == "Sinv": + first, second = (ai, -ar), (br - ai, bi + ar) + else: + raise ValueError("unknown chart") + result[low] = residue(*first, precision) + result[high] = residue(*second, precision) + return tuple(result) + + +def rotate(bank: tuple[int, ...], auxiliary: int, precision: int, + inverse: bool = False) -> tuple[tuple[int, ...], int]: + """Rotate (live, lost, clean) to (clean, live, lost) at every label.""" + output = [0] * len(bank) + recovered = 0 + offset = 0 + for u, value in enumerate(bank): + lost = min(2 * u.bit_count(), precision) + live = precision - lost + auxiliary_part = (auxiliary >> offset) & ((1 << lost) - 1) + if inverse: + output[u] = (value >> lost) | (auxiliary_part << live) + recovered |= (value & ((1 << lost) - 1)) << offset + else: + output[u] = ((value & ((1 << live) - 1)) << lost) | auxiliary_part + recovered |= (value >> live) << offset + offset += lost + return tuple(output), recovered + + +def overwrite(bank: tuple[int, ...], auxiliary: int, n: int, precision: int, + inverse: bool = False) -> tuple[tuple[int, ...], int]: + """Permutation on NP+K bits; auxiliary zero gives the required response.""" + size, clean = dimensions(n, precision) + if len(bank) != size or any(type(x) is not int or not 0 <= x < (1 << precision) + for x in bank): + raise ValueError("bank must contain 2^n canonical P-digit labels") + if type(auxiliary) is not int or not 0 <= auxiliary < (1 << clean): + raise ValueError("auxiliary state must fit exactly K bits") + if type(inverse) is not bool: + raise ValueError("inverse must be Boolean") + before, after = ("Sinv", "Tinv") if inverse else ("T", "S") + middle = chart(bank, n, precision, before) + middle, garbage = rotate(middle, auxiliary, precision, inverse) + return chart(middle, n, precision, after), garbage diff --git a/research/gaussian-smith-reversible-capacity/verify.py b/research/gaussian-smith-reversible-capacity/verify.py new file mode 100644 index 0000000000..c13f33077a --- /dev/null +++ b/research/gaussian-smith-reversible-capacity/verify.py @@ -0,0 +1,163 @@ +"""Bounded new reversible-interface checks; emit a source-bound receipt.""" + +import hashlib +import json +from math import comb +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from engine import chart, dimensions, gaussian, overwrite, residue, rotate + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def unpack(value: int, size: int, precision: int) -> tuple[int, ...]: + return tuple((value >> (u * precision)) & ((1 << precision) - 1) + for u in range(size)) + + +def literal_response(bank: tuple[int, ...], n: int, precision: int) -> tuple[int, ...]: + """An endpoint oracle for the new interface, using only C butterflies.""" + result = [gaussian(value, precision) for value in bank] + for axis in range(n): + for low in range(1 << n): + high = low | (1 << axis) + if low != high: + ar, ai = result[low] + br, bi = result[high] + result[low] = (br - ai, bi + ar) + result[high] = (ar - bi, ai + br) + return tuple(residue(*value, precision) for value in result) + + +def complete_permutations() -> dict[str, int]: + cases, states, clean_endpoints = 0, 0, 0 + for n in range(4): + for precision in range(5): + size, clean = dimensions(n, precision) + public_bits = size * precision + if public_bits + clean > 14: + continue + seen = set() + for state in range(1 << (public_bits + clean)): + bank = unpack(state, size, precision) + auxiliary = state >> public_bits + output, garbage = overwrite(bank, auxiliary, n, precision) + require(overwrite(output, garbage, n, precision, True) == + (bank, auxiliary), "full-state inverse failed") + require((output, garbage) not in seen, "permutation collision") + seen.add((output, garbage)) + if auxiliary == 0: + require(output == literal_response(bank, n, precision), + "clean overwrite endpoint failed") + clean_endpoints += 1 + states += 1 + require(len(seen) == (1 << (public_bits + clean)), "missing state") + cases += 1 + return {"complete_permutation_cases": cases, "full_states": states, + "clean_endpoints": clean_endpoints} + + +def larger_interfaces() -> dict[str, int]: + cases, endpoints, erasure_collisions = 0, 0, 0 + for n in range(6): + for precision in range(9): + size, clean = dimensions(n, precision) + expected = size * precision - sum( + comb(n, j) * max(precision - 2 * j, 0) for j in range(n + 1)) + require(clean == expected, "capacity complement failed") + if precision >= 2 * n: + require(clean == n * size, "high-precision closed form failed") + for sample in range(8): + bank = tuple((sample * 17 + u * u + 3 * u) % (1 << precision) + for u in range(size)) + auxiliary = ((1 << clean) - 1) if sample & 1 else 0 + output, garbage = overwrite(bank, auxiliary, n, precision) + require(overwrite(output, garbage, n, precision, True) == + (bank, auxiliary), "larger inverse failed") + if auxiliary == 0: + require(output == literal_response(bank, n, precision), + "larger clean endpoint failed") + endpoints += 1 + cases += 1 + zero = (0,) * size + for bit in range(clean): + first = overwrite(zero, 0, n, precision, True) + second = overwrite(zero, 1 << bit, n, precision, True) + require(first[1] == second[1] == 0, "fiber witness is not clean") + require(first[0] != second[0], "kernel bit was not independent") + require(overwrite(second[0], 0, n, precision) == (zero, 1 << bit), + "lost-bit witness failed") + erasure_collisions += 1 + return {"larger_interfaces": cases, "larger_clean_endpoints": endpoints, + "independent_garbage_bit_witnesses": erasure_collisions} + + +def dirty_capacity() -> dict[str, int]: + """Pigeonhole counts include every dirty state, even with changed outputs.""" + cases = 0 + for lost in range(1, 9): + for dirty in range(6): + for clean in range(lost): + inputs = 1 << (lost + dirty) + outputs = 1 << (clean + dirty) + require(inputs > outputs, "undercapacity was accepted") + cases += 1 + return {"dirty_undercapacity_comparisons": cases} + + +def controls() -> dict[str, int]: + rejected = 0 + invalid = [((0,), 0, -1, 1), ((0,), 0, 9, 1), ((0,), 0, 0, 17), + ((0,), 0, True, 1), ((2,), 0, 0, 1), ((0, 0), 0, 0, 1), + ((0,), -1, 0, 1), ((0,), 1, 0, 1), ((0,), 0, 0, -1)] + for bank, auxiliary, n, precision in invalid: + try: + overwrite(bank, auxiliary, n, precision) + except ValueError: + rejected += 1 + else: + raise RuntimeError("invalid interface was accepted") + # Replacing pi^(2|u|) by pi^|u| produces a wrong public endpoint. + bank = chart((0, 1), 1, 3, "Tinv") + require(overwrite(bank, 0, 1, 3)[0] != chart((0, 2), 1, 3, "S"), + "wrong-valuation control did not distinguish") + # Forgetting one retained bit merges two legal inputs with the same output. + x0 = overwrite((0, 0), 0, 1, 3, True)[0] + x1 = overwrite((0, 0), 1, 1, 3, True)[0] + y0, h0 = overwrite(x0, 0, 1, 3) + y1, h1 = overwrite(x1, 0, 1, 3) + require(x0 != x1 and y0 == y1 and (h0 >> 1) == (h1 >> 1), + "garbage-erasure collision control failed") + # Uninitialized auxiliary bits can leak into the required output. + require(overwrite((0, 0), 1, 1, 3)[0] != (0, 0), + "dirty-in-place-of-clean control did not distinguish") + require(rotate((0, 7), 0, 3) != ((0, 0), 0), + "zeroing all discarded data was accepted") + try: + overwrite((0,), 0, 0, 1, 1) + except ValueError: + rejected += 1 + else: + raise RuntimeError("non-Boolean inverse flag was accepted") + return {"invalid_input_controls": rejected, "semantic_controls": 4} + + +def main() -> None: + receipt = {"status": "PASS", "claim_type": "scoped proof with finite corroboration"} + for result in (complete_permutations(), larger_interfaces(), dirty_capacity(), controls()): + receipt.update(result) + package = Path(__file__).resolve().parent + files = ("engine.py", "verify.py", "PROOF.md", "README.md", "TASK.json", + "SOURCES.json", "VERIFY.json") + receipt["sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in files} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()