diff --git a/research/modular-normalization-boundary/PROOF.md b/research/modular-normalization-boundary/PROOF.md new file mode 100644 index 0000000000..111e189463 --- /dev/null +++ b/research/modular-normalization-boundary/PROOF.md @@ -0,0 +1,205 @@ +# Exact metric constants and a paid modular query calibration + +This is a scoped written proof. Exact finite checks support it. They do not +replace its quantifiers or establish a multiplication theorem. + +## 1. Three domains give two different optimal constants + +Let N=2^b, b>=1, and let p be odd. Put a=p^(-1) mod N, with 1<=aZ with F(t)=at mod N, use the usual absolute +distance on both copies of Z. Every adjacent difference F(t+1)-F(t) is +congruent to a. Its absolute value is at least m. Thus every such lift has +Lipschitz constant at least m. Choose the shortest signed representative +s of a and set F(t)=st. This attains m on the entire line. The lift is +not periodic. + +For a periodic integer lift G:C_N->Z with G(x)=ax mod N, use d_N on the +domain and absolute distance on the target. Its exact minimum Lipschitz +constant is N-m. To prove the lower bound, orient all N cycle edges and +put Delta_x=G(x+1)-G(x), with x+1 interpreted modulo N. Each Delta_x is +congruent to a, and their sum is zero. Since 01 cannot divide 1 in Z. Thus + + p*m = |ps| >= N-1, m >= (N-1)/p. + +For p=3 the exact value is + + m=(2^b-(-1)^b)/3. + +If b is even, N=1 mod 3 and s=(1-N)/3. If b is odd, N=2 mod 3 and +s=(1+N)/3. These are the shortest representatives. + +Rescale the residue cycle to circumference one, with spacing 1/N. +Its inverse-normalization Lipschitz constant remains m. Inputs 0 and +1/N can produce the same uncertain real observation 1/(2N) when the +allowed input error is 1/(2N). Their normalized outputs have circle +distance m/N. Any common numerical output has error at least m/(2N) +on one of the two inputs, by the triangle inequality. + +For fixed p this output ambiguity does not tend to zero: its lower bound +is (N-1)/(2pN). This statement concerns an unrestricted numerical +interface with that input uncertainty. Exact digital residues have no +such uncertainty. A separated reachable set can also exclude the two +inputs. This is not an extra-bit lower bound for an exact modular +backend, and it does not refute modular borrowed-port echoes. + +## 3. The released three-coordinate cut + +The following coordinates are payload vectors of any common finite width d. +Scalar operations act componentwise. Use the ordinary prefix + + x += z + y -= z + z += x + z += x + z -= y. + +Its integer matrix is + + B = [1 0 1] + [0 1 -1] + [2 -1 4], det(B)=1. + +Let E be the first two coordinates. A supported column c=(u,v,0) has +B*c supported on E exactly when 2u-v=0. Its full column module is +generated by c0=(1,2,0). A supported row r=(u,v,0) has r*B supported +on E exactly when u-v=0. Its full row module is generated by +r0=(1,1,0). Both generators are fixed by B, so using B^-1 gives the +same modules. Their pairing is r0*c0=3. + +Over Z[1/2], all eligible pairings are 3uv. None equals one, since 3 +is not a unit. Modulo 2^b, 3 is a unit and a=3^(-1) supplies a normalized +pair. This is an algebraic change of boundary. It does not supply a +cheap physical native operator. + +## 4. Literal completion, arbitrary dirt and inverse + +On E, four instructions implement S(x,y)=(x+y,2x-y): + + y += x + x *= 3 + x -= y + SWAP(x,y). + +The inverse is + + SWAP(x,y) + x += y + x *= a + y -= x. + +Each instruction uses exact residues modulo N. Apply the prefix B, +then S, then one supplied invertible linear query Q to the first payload, +then S^-1 and the literal inverse of B. This is 5+4+1+4+5=19 instructions. + +Put delta=a*(Q-I)(x+y). The complete endpoint is + + x' = x+delta, + y' = y+2*delta, + z' = z. + +Indeed S^-1= a*S and the changed part is +a*c0*(Q-I)*r0. Because B*c0=c0 and r0*B=r0, conjugation by B leaves +this changed part unchanged. All formulas hold for arbitrary correlated +payloads and arbitrary dirty z. The reverse word, with inverse scalar +coefficients and Q^-1, restores every input exactly. + +For d=2 and Q the payload swap, start at x=z=0 and y=(1,0). +The second entry of x' is a. Thus the modular-inverse expansion survives +the complete query endpoint. It is not removed by the dirty-coordinate +restoration. This is a lower-bound witness for the full endpoint, not a +claim that its exact global operator norm is m. + +## 5. Correct ordinary alphabet and complete direct costs + +A SWAP of two scalar registers cannot equal any product of signed elementary +ADDs modulo N>=4: each ADD has determinant one, while that SWAP has +determinant minus one. The vector instructions here repeat the same scalar +word on each payload entry. This argument does not exclude other words +that mix payload entries or swap an even number of scalar pairs together. +The three familiar ADDs produce a signed swap: + + x += y + y -= x + x += y # endpoint (old_y, -old_x). + +One additional paid negation of y gives the actual swap. This four-step +identity holds over every commutative ring. Replacing both SWAPs gives +25 instructions, not the incorrect three-ADD price. + +| Program | ADD/SUB | SCALE | SWAP | NEGATE | Supplied query | +|---|---:|---:|---:|---:|---:| +| Literal | 14 | 2 | 2 | 0 | 1 | +| Expanded | 20 | 2 | 0 | 2 | 1 | + +These are vector instructions. For payload width d the literal word uses +14d scalar additions/subtractions, 2d scalar multiplications, 16d explicit +reductions, and 6d assignments for the two swaps. The expanded word uses +20d additions/subtractions, 2d multiplications, 2d negations and 24d +reductions. The query's own arithmetic, reductions, scratch and inverse +are separate paid terms; the verifier's dense matrix evaluator is an oracle +implementation, not a free physical query. + +Stored values have b bits. ADD needs b+1 unsigned bits; SUB needs b+1 +signed bits. NEGATE also fits in b+1 signed bits. +The two fixed-coefficient products fit in 2b unsigned bits. With +schoolbook multiplication, direct scalar work outside the query is +O(d*b^2) bit work. Add inverse-coefficient preparation, query execution, +conversion, access, layout, recovery and any physical routing costs. +The reference uses O(db) payload/copy bits plus query storage, loop +indices and O(b) scalar scratch. Its Python allocations are not a +fixed-tape implementation or a tight workspace claim. + +No supplied coefficient, modular reduction, input/output conversion or +query is claimed free. The 19/25 counts are constructive upper bounds, +not shortest-word optima. No favorable complete recursive invoice is +provided. Native realization, numerical conversion, exact recovery and +the full supplier boundary remain open. + +## 6. Attribution and limits + +Nick Petalas's [released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363231) +supplies the quotient/line candidate, pairing-three prefix and proposed +19-instruction calibration. It also reports the three-ADD SWAP cost error. +This continuation independently reconstructs and checks the word, repairs +the paid expansion, distinguishes periodic lifts and supplies a public proof +and registered finite evidence. It does not claim priority for the released +ideas or general modular metric arguments. + +Gareth Davidson / @bitplane's [PR #1159](https://github.com/CrocSwap/integer-mult-bounds/pull/1159) +supplies the exact quotient-valued borrowed-port context. Its own +[scope](https://github.com/CrocSwap/integer-mult-bounds/blob/7c49fe32c55de02c2c873655c804b16e4c3fef0a/research/modular-port-borrowing/README.md) +excludes rounded and general dyadic leaves. We do not audit that backend +or transfer this numerical obstruction to it. Retain shhxera, androolloyd, +Sagar Thakrar, Chafik Boukhalfa and the classical register lineage credited +in that unchanged source. + +All selected assumptions and the selected frontier remain unchanged. +Independent human review, proof-kernel formalization, production native +execution and complete multiplication admission are unrun. +Prepared by Ali Romman with substantial OpenAI Codex assistance. +New work is Apache-2.0. diff --git a/research/modular-normalization-boundary/README.md b/research/modular-normalization-boundary/README.md new file mode 100644 index 0000000000..f0989d097f --- /dev/null +++ b/research/modular-normalization-boundary/README.md @@ -0,0 +1,86 @@ +# Modular inverse normalization: exact metric boundary and paid query word + +**Scoped proof and scalar construction; no new kappa.** This completes +[Nick Petalas's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363231). +It distinguishes three lift domains and corrects the stated SWAP cost error. +The [proof](PROOF.md) gives all quantifiers, the full word, prices and credit. +The [receipt](RESULT.json) records exact finite evidence. + +Let N=2^b, a=p^(-1) mod N for odd p, and m=min(a,N-a). + +| Boundary | Exact optimal Lipschitz constant | +|---|---:| +| Residue cycle to residue cycle | m | +| Integer-line lift, ordinary distance | m | +| Periodic integer lift from the residue cycle | N-m | + +For fixed 1=(N-1)/p. For p=3 the exact value is +`(2^b-(-1)^b)/3`. Thus an unrestricted numerical conversion can have +nonvanishing output ambiguity even when its input error is half a grid unit. +Exact digital residue arithmetic and restricted reachable domains are outside +this obstruction. The periodic lift distinction is necessary: at N=8,p=3, +the first two constants are 3 and the third is 5. + +The handoff's pairing-three cut has a literal 19-instruction completion +with one supplied invertible payload query. It restores the outside dirty +coordinate exactly. A payload-swap query retains the inverse-normalization +expansion at the full endpoint. Two separately paid SWAPs are present. +Replacing each by three ADDs and one NEGATE gives a verified 25-instruction +word. Three ADDs alone give a signed swap and cannot implement a SWAP +modulo N>=4. Both words retain all scaling and reduction costs. + +This is an indexed scalar calibration. The query, coefficient preparation, +conversion, physical access/routing, recovery and compiler costs are separate +paid obligations. No favorable complete recursive bill, native Gaussian +implementation, selected assumption discharge or frontier change is claimed. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/modular-normalization-boundary +python3.12 -B scripts/check_research_commit.py --package research/modular-normalization-boundary --check-source-history +``` + +Expected markers are `PASS_MODULAR_NORMALIZATION_BOUNDARY`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The registered runner checks both normal and optimized execution. +The default verifier compares the stored receipt without changing it. +`--output NEW_FILE` writes a separate receipt and refuses to overwrite a file. + +Finite evidence covers 63 metric contexts and all 73,533 unordered pairs, +8,805 independently enumerated periodic lifts, 255 inverse-three precision +formulas, all 1,638 invertible two-by-two query matrices modulo 2,4,8, +19,656 full basis forward/inverse checks, 768 exhaustive binary dirty cases +and 30 wider cases through 257 bits. Every one of the 19 and 25 instruction +omissions is detected at modulus 32. Additional controls cover the signed +swap, lift-domain confusion, full-endpoint amplification, numerical ambiguity, +nonunit inversion and confusion with real division. + +No predecessor scientific suite, selected cold replay, Lean, Docker, +independent human review or proof-kernel verification is claimed. The +finite enumeration supports the written all-size proof; it does not replace it. +Sources in [SOURCES.json](SOURCES.json) are provenance, not imported code. +The verifier is standalone and has no runtime source dependencies. + +## Open next questions + +Can one actual native producer stay in exact residue arithmetic with paid +conversion and exact recovery, or prove a restricted reachable domain? +First export one complete producer/query/consumer boundary and its full +invoice. The present obstruction does not decide those alternatives. + +## Credit + +Nick Petalas supplied the released metric candidate, pairing-three prefix, +19-instruction completion proposal and disclosed cost error. This work +reconstructs the completion, repairs and tests the paid expansion, distinguishes +periodic lifts, and publishes the exact proof and executable evidence. +Gareth Davidson / @bitplane supplied the exact quotient backend and its scope +in [PR #1159](https://github.com/CrocSwap/integer-mult-bounds/pull/1159). +Its unchanged source retains shhxera, androolloyd, Sagar Thakrar, Chafik +Boukhalfa and the classical register lineage. General congruences, cycle +metrics and two-point ambiguity arguments are classical; no global literature +priority is claimed. Prepared by Ali Romman with substantial OpenAI Codex +assistance. New work is Apache-2.0. diff --git a/research/modular-normalization-boundary/RESULT.json b/research/modular-normalization-boundary/RESULT.json new file mode 100644 index 0000000000..b9578f4b59 --- /dev/null +++ b/research/modular-normalization-boundary/RESULT.json @@ -0,0 +1,469 @@ +{ + "controls": { + "full_query_expansion": true, + "instruction_omissions": 44, + "lift_domain": true, + "nonunit": true, + "numerical_ambiguity": true, + "paid_swap": true, + "periodic_constant": true, + "real_division": true + }, + "metrics": { + "bounded_periodic_lifts": 8805, + "constants": [ + [ + 1, + 1, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 3 + ], + [ + 2, + 3, + 3, + 1, + 3 + ], + [ + 3, + 1, + 1, + 1, + 7 + ], + [ + 3, + 3, + 3, + 3, + 5 + ], + [ + 3, + 5, + 5, + 3, + 5 + ], + [ + 3, + 7, + 7, + 1, + 7 + ], + [ + 4, + 1, + 1, + 1, + 15 + ], + [ + 4, + 3, + 11, + 5, + 11 + ], + [ + 4, + 5, + 13, + 3, + 13 + ], + [ + 4, + 7, + 7, + 7, + 9 + ], + [ + 4, + 9, + 9, + 7, + 9 + ], + [ + 4, + 11, + 3, + 3, + 13 + ], + [ + 4, + 13, + 5, + 5, + 11 + ], + [ + 4, + 15, + 15, + 1, + 15 + ], + [ + 5, + 1, + 1, + 1, + 31 + ], + [ + 5, + 3, + 11, + 11, + 21 + ], + [ + 5, + 5, + 13, + 13, + 19 + ], + [ + 5, + 7, + 23, + 9, + 23 + ], + [ + 5, + 9, + 25, + 7, + 25 + ], + [ + 5, + 11, + 3, + 3, + 29 + ], + [ + 5, + 13, + 5, + 5, + 27 + ], + [ + 5, + 15, + 15, + 15, + 17 + ], + [ + 5, + 17, + 17, + 15, + 17 + ], + [ + 5, + 19, + 27, + 5, + 27 + ], + [ + 5, + 21, + 29, + 3, + 29 + ], + [ + 5, + 23, + 7, + 7, + 25 + ], + [ + 5, + 25, + 9, + 9, + 23 + ], + [ + 5, + 27, + 19, + 13, + 19 + ], + [ + 5, + 29, + 21, + 11, + 21 + ], + [ + 5, + 31, + 31, + 1, + 31 + ], + [ + 6, + 1, + 1, + 1, + 63 + ], + [ + 6, + 3, + 43, + 21, + 43 + ], + [ + 6, + 5, + 13, + 13, + 51 + ], + [ + 6, + 7, + 55, + 9, + 55 + ], + [ + 6, + 9, + 57, + 7, + 57 + ], + [ + 6, + 11, + 35, + 29, + 35 + ], + [ + 6, + 13, + 5, + 5, + 59 + ], + [ + 6, + 15, + 47, + 17, + 47 + ], + [ + 6, + 17, + 49, + 15, + 49 + ], + [ + 6, + 19, + 27, + 27, + 37 + ], + [ + 6, + 21, + 61, + 3, + 61 + ], + [ + 6, + 23, + 39, + 25, + 39 + ], + [ + 6, + 25, + 41, + 23, + 41 + ], + [ + 6, + 27, + 19, + 19, + 45 + ], + [ + 6, + 29, + 53, + 11, + 53 + ], + [ + 6, + 31, + 31, + 31, + 33 + ], + [ + 6, + 33, + 33, + 31, + 33 + ], + [ + 6, + 35, + 11, + 11, + 53 + ], + [ + 6, + 37, + 45, + 19, + 45 + ], + [ + 6, + 39, + 23, + 23, + 41 + ], + [ + 6, + 41, + 25, + 25, + 39 + ], + [ + 6, + 43, + 3, + 3, + 61 + ], + [ + 6, + 45, + 37, + 27, + 37 + ], + [ + 6, + 47, + 15, + 15, + 49 + ], + [ + 6, + 49, + 17, + 17, + 47 + ], + [ + 6, + 51, + 59, + 5, + 59 + ], + [ + 6, + 53, + 29, + 29, + 35 + ], + [ + 6, + 55, + 7, + 7, + 57 + ], + [ + 6, + 57, + 9, + 9, + 55 + ], + [ + 6, + 59, + 51, + 13, + 51 + ], + [ + 6, + 61, + 21, + 21, + 43 + ], + [ + 6, + 63, + 63, + 1, + 63 + ] + ], + "contexts": 63, + "inverse_three_precisions": 255, + "unordered_pairs": 73533 + }, + "query_word": { + "basis_forward_inverse_checks": 19656, + "binary_dirty_cases": 768, + "full_output_sha256": "cec6453a080c0224d148df68acc381cfcd03f35afcf3e9132e6fd5fa01573cfc", + "invertible_queries": 1638, + "wide_cases": 30 + }, + "schema_version": 1 +} diff --git a/research/modular-normalization-boundary/SOURCES.json b/research/modular-normalization-boundary/SOURCES.json new file mode 100644 index 0000000000..237405baa4 --- /dev/null +++ b/research/modular-normalization-boundary/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/modular-port-borrowing/README.md", + "usage": "provenance", + "git_blob": "c55a507a2e844abcb0d74060cfc42c536aeb70a7", + "sha256": "61512ec419a9ae04b1f5321167d14515e4e25db6702704f417cdb32857243fb7" + } + ] +} diff --git a/research/modular-normalization-boundary/TASK.json b/research/modular-normalization-boundary/TASK.json new file mode 100644 index 0000000000..fb2a0dc59f --- /dev/null +++ b/research/modular-normalization-boundary/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Complete the released modular-inverse metric and three-coordinate calibration handoff; distinguish periodic lifts and repair the paid SWAP expansion.", + "scope_change_reason": "The released handoff identifies a numerical quotient boundary and an explicit cost error, not a changed fast native connector.", + "bottleneck_link": "An exact quotient inverse can normalize a dyadically nonunit pairing, but unrestricted numerical conversion has growing metric amplification. Full physical costs remain open.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact metric proof, literal full dirty-state query completion, complete direct counts and bounded independent checks. Do not infer a fast supplier or expand an unpriced physical caller.", + "outcome": "completed", + "evidence": "PROOF.md proves all-domain statements. RESULT.json records independent pair/lift enumeration, full endpoint and inverse checks, and all instruction omission controls.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Can one actual native producer remain in exact residue arithmetic with paid conversion and exact recovery, or prove a restricted reachable domain?", + "why_it_matters": "The numerical ambiguity does not cover either alternative.", + "first_step": "Export one producer/query/consumer boundary with exact types, reachable values and a complete paid invoice.", + "blocked_by": "This package does not supply a native query, physical routing, recovery or conversion cost." + } + ] +} diff --git a/research/modular-normalization-boundary/VERIFY.json b/research/modular-normalization-boundary/VERIFY.json new file mode 100644 index 0000000000..6a2f65aaa6 --- /dev/null +++ b/research/modular-normalization-boundary/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact quotient, line and periodic-lift constants; complete dirty query endpoints/inverses and paid instruction/rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact quotient, line and periodic-lift constants; complete dirty query endpoints/inverses and paid instruction/rejection controls." + } + ] +} diff --git a/research/modular-normalization-boundary/verify.py b/research/modular-normalization-boundary/verify.py new file mode 100644 index 0000000000..f407074172 --- /dev/null +++ b/research/modular-normalization-boundary/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Check modular metrics and the complete paid query word. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +Nick Petalas supplied the released metric and three-coordinate proposals. +""" +import argparse +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import random + +HERE = Path(__file__).resolve().parent + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def distance(x, y, n): + r = (x-y) % n + return min(r, n-r) + + +def det(q): + return q[0][0]*q[1][1]-q[0][1]*q[1][0] + + +def inverse(q, n): + a = pow(det(q), -1, n) + return [[a*q[1][1] % n, -a*q[0][1] % n], + [-a*q[1][0] % n, a*q[0][0] % n]] + + +def mv(q, v, n): + return [sum(a*b for a, b in zip(row, v)) % n for row in q] + + +def word(n, expanded=False): + a = pow(3, -1, n) + prefix = [('add', 0, 2, 1), ('add', 1, 2, -1), + ('add', 2, 0, 1), ('add', 2, 0, 1), ('add', 2, 1, -1)] + encode = [('add', 1, 0, 1), ('scale', 0, 3), + ('add', 0, 1, -1), ('swap', 0, 1)] + decode = [('swap', 0, 1), ('add', 0, 1, 1), + ('scale', 0, a), ('add', 1, 0, -1)] + undo = [('add', dst, src, -c) for _, dst, src, c in reversed(prefix)] + ops = prefix+encode+[('query', 0)]+decode+undo + if expanded: + result = [] + for op in ops: + if op[0] == 'swap': + _, x, y = op + result += [('add', x, y, 1), ('add', y, x, -1), + ('add', x, y, 1), ('negate', y)] + else: + result.append(op) + ops = result + return ops + + +def execute(state, ops, q, n): + state = [list(v) for v in state] + counts = Counter() + reductions = moves = 0 + for op in ops: + kind, target, *args = op + counts[kind] += 1 + if kind == 'add': + source, coefficient = args + state[target] = [(x+coefficient*y) % n + for x, y in zip(state[target], state[source])] + reductions += len(state[target]) + elif kind == 'scale': + state[target] = [x*args[0] % n for x in state[target]] + reductions += len(state[target]) + elif kind == 'negate': + state[target] = [-x % n for x in state[target]] + reductions += len(state[target]) + elif kind == 'swap': + source = args[0] + for j in range(len(state[target])): + saved = state[target][j] + state[target][j] = state[source][j] + state[source][j] = saved + moves += 3 + elif kind == 'query': + state[target] = mv(q, state[target], n) + else: + raise ValueError('Unknown operation') + need(all(type(x) is int and 0 <= x < n for v in state for x in v), + 'Residue boundary') + return state, dict(counts), reductions, moves + + +def reverse_word(ops, n): + result = [] + for op in reversed(ops): + if op[0] == 'add': + result.append((*op[:3], -op[3])) + elif op[0] == 'scale': + result.append((*op[:2], pow(op[2], -1, n))) + else: + result.append(op) + return result + + +def endpoint(state, q, n): + x, y, z = state + a = pow(3, -1, n) + total = [(u+v) % n for u, v in zip(x, y)] + changed = mv(q, total, n) + delta = [(u-v)*a % n for u, v in zip(changed, total)] + return [[(u+v) % n for u, v in zip(x, delta)], + [(u+2*v) % n for u, v in zip(y, delta)], list(z)] + + +def basis(d): + return [[[int(row*d+j == k) for j in range(d)] for row in range(3)] + for k in range(3*d)] + + +def metric_checks(): + pairs = contexts = lifts = 0 + records = [] + for b in range(1, 7): + n = 1 << b + for p in range(1, n, 2): + a = pow(p, -1, n) + m = min(a, n-a) + s = a if a <= n//2 else a-n + ratios, lifted = [], [] + for x in range(n): + for y in range(x+1, n): + d = distance(x, y, n) + ratios.append(F(distance(a*x, a*y, n), d)) + lifted.append(F(abs(a*x % n-a*y % n), d)) + need(abs(s*x-s*y) == m*abs(x-y), 'Affine line lift') + pairs += 1 + need(max(ratios) == m, 'Exact quotient constant') + need(max(lifted) == n-m, 'Exact periodic attainer') + if 1 < p < n: + need(p*m >= n-1, 'Fixed odd normalization lower bound') + records.append([b, p, a, m, n-m]) + contexts += 1 + # This finite lift search is independent of the affine construction. + for n in (2, 4, 8): + for a in range(1, n, 2): + best = None + for shifts in product((-1, 0, 1), repeat=n-1): + values = [0]+[(a*x % n)+k*n for x, k in enumerate(shifts, 1)] + cost = max(abs(values[(x+1) % n]-values[x]) for x in range(n)) + best = cost if best is None else min(best, cost) + lifts += 1 + need(best == n-min(a, n-a), 'Enumerated periodic lifts') + for b in range(2, 257): + n = 1 << b + a = pow(3, -1, n) + need(min(a, n-a) == (n-(-1)**b)//3, 'Inverse-three parity formula') + return dict(contexts=contexts, unordered_pairs=pairs, bounded_periodic_lifts=lifts, + inverse_three_precisions=255, constants=records) + + +def program_checks(): + contexts = columns = dirty = 0 + digest = sha256() + for n in (2, 4, 8): + for entries in product(range(n), repeat=4): + q = [list(entries[:2]), list(entries[2:])] + if not det(q) & 1: + continue + qi = inverse(q, n) + for expanded in (False, True): + ops = word(n, expanded) + need(len(ops) == (25 if expanded else 19), 'Complete word length') + for state in basis(2): + out, counts, reductions, moves = execute(state, ops, q, n) + need(out == endpoint(state, q, n), 'Independent full endpoint') + back, _, _, _ = execute(out, reverse_word(ops, n), qi, n) + need(back == state and out[2] == state[2], 'Inverse and outside dirt') + expected = ({'add': 20, 'scale': 2, 'negate': 2, 'query': 1} + if expanded else {'add': 14, 'scale': 2, 'swap': 2, 'query': 1}) + need(counts == expected and reductions == (48 if expanded else 32) + and moves == (0 if expanded else 12), 'Every paid instruction') + digest.update(json.dumps(out, separators=(',', ':')).encode()) + columns += 1 + if n == 2: + for bits in product(range(2), repeat=6): + state = [list(bits[i:i+2]) for i in range(0, 6, 2)] + out, _, _, _ = execute(state, ops, q, n) + need(out == endpoint(state, q, n), 'Exhaustive binary dirt') + dirty += 1 + contexts += 1 + rng = random.Random(314159) + wider = 0 + for b in (4, 5, 16, 64, 257): + n = 1 << b + for d in (1, 3, 5): + q = [[int(i == j)+(rng.randrange(n) if i < j else 0) + for j in range(d)] for i in range(d)] + state = [[rng.randrange(n) for _ in range(d)] for _ in range(3)] + for expanded in (False, True): + out, _, _, _ = execute(state, word(n, expanded), q, n) + need(out == endpoint(state, q, n), 'Wide dirty endpoint') + wider += 1 + return dict(invertible_queries=contexts, basis_forward_inverse_checks=columns, + binary_dirty_cases=dirty, wide_cases=wider, full_output_sha256=digest.hexdigest()) + + +def controls(): + n, q = 32, [[0, 1], [1, 0]] + omissions = 0 + for expanded in (False, True): + ops = word(n, expanded) + for j in range(len(ops)): + bad = ops[:j]+ops[j+1:] + need(any(execute(v, bad, q, n)[0] != endpoint(v, q, n) for v in basis(2)), + 'Instruction omission detected') + omissions += 1 + three = [('add', 0, 1, 1), ('add', 1, 0, -1), ('add', 0, 1, 1)] + v = [[1], [2], [3]] + need(execute(v, three, [[1]], n)[0] == [[2], [31], [3]], 'Signed swap control') + need(execute(v, three+[('negate', 1)], [[1]], n)[0] == [[2], [1], [3]], + 'Paid SWAP expansion') + need(distance(7, 0, 8) == 1 and abs(3*7-0) == 21, 'Lift domain control') + need(max(abs(3*((x+1) % 8) % 8-(3*x % 8)) for x in range(8)) == 5, + 'Periodic constant is five, not three') + a = pow(3, -1, n) + out = execute([[0, 0], [1, 0], [0, 0]], word(n), q, n)[0] + need(out[0][1] == a and distance(a, 0, n) == 11, 'Full endpoint expansion') + observed = F(1, 2*n) + need(abs(observed) == abs(observed-F(1, n)), 'Ambiguous observation') + need(F(distance(a, 0, n), n)/2 == F(11, 64), 'Output ambiguity') + try: + pow(2, -1, n) + except ValueError: + pass + else: + raise ValueError('Nonunit accepted') + need(a*3 % n == 1 and F(1, 3) != a, 'Residue inverse is not a real coefficient') + return dict(instruction_omissions=omissions, paid_swap=True, lift_domain=True, + periodic_constant=True, full_query_expansion=True, + numerical_ambiguity=True, nonunit=True, real_division=True) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path) + args = parser.parse_args() + receipt = dict(schema_version=1, metrics=metric_checks(), + query_word=program_checks(), controls=controls()) + if args.output: + with args.output.open('x', encoding='utf-8') as stream: + json.dump(receipt, stream, indent=2, sort_keys=True) + stream.write('\n') + else: + need(receipt == json.loads((HERE/'RESULT.json').read_text()), 'Stored receipt mismatch') + print('PASS_MODULAR_NORMALIZATION_BOUNDARY', receipt['metrics']['contexts'], + 'metric contexts;', receipt['query_word']['invertible_queries'], + 'complete invertible queries;', receipt['controls']['instruction_omissions'], + 'instruction controls') + + +if __name__ == '__main__': + main()