From 90d1c7271bf0479c137acc340644d2d6e2130532 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 22:04:04 +0000 Subject: [PATCH] feat(research): linearize polynomial helper call profiles --- .../PROOF.md | 109 +++++++ .../README.md | 111 +++++++ .../RESULT.json | 26 ++ .../SOURCES.json | 36 +++ .../TASK.json | 80 +++++ .../VERIFY.json | 32 ++ .../compiler.py | 140 +++++++++ .../verify.py | 277 ++++++++++++++++++ 8 files changed, 811 insertions(+) create mode 100644 research/polynomial-helper-profile-domination/PROOF.md create mode 100644 research/polynomial-helper-profile-domination/README.md create mode 100644 research/polynomial-helper-profile-domination/RESULT.json create mode 100644 research/polynomial-helper-profile-domination/SOURCES.json create mode 100644 research/polynomial-helper-profile-domination/TASK.json create mode 100644 research/polynomial-helper-profile-domination/VERIFY.json create mode 100644 research/polynomial-helper-profile-domination/compiler.py create mode 100644 research/polynomial-helper-profile-domination/verify.py diff --git a/research/polynomial-helper-profile-domination/PROOF.md b/research/polynomial-helper-profile-domination/PROOF.md new file mode 100644 index 0000000000..3ae0bd55d9 --- /dev/null +++ b/research/polynomial-helper-profile-domination/PROOF.md @@ -0,0 +1,109 @@ +# Zero-state extraction preserves the labelled linear interface + +## Contract + +Let K be an infinite field and R a subring of K. There are finitely many +vector registers of a common finite dimension d. The data and dirty workspace +vary independently over K. A specified subset of scratch registers may instead +start at zero. Every gate has distinct source a and target b, a fixed K-linear +operator T, a label ell, and a fixed scalar polynomial p in R[t] with p(0)=0. +It performs one of the following operations. Powers in p are coordinatewise. + + b += p(Ta), or b += T p(a). + +The source and other registers stay unchanged. Each gate is invertible by +subtracting the same increment. No invertibility assumption on T is needed. +The sequence, coefficients, operators, ports and labels are independent of +input values. A label records one allowed paid operator class. Multiplication +by any scalar in R is permitted in the linear class at that same label charge. +The polynomial class grants its extra pointwise arithmetic for free. This is +an optimistic operator-call model, not a physical implementation claim. + +The call profile n_ell counts gates of each label. Any nonnegative tariff +sum_ell w_ell n_ell is allowed. Labels may encode rank, operator, orientation, +ports and other fixed distinctions. There is no claim that these counts alone +constitute the selected supplier's complete invoice. + +## Theorem + +Suppose a word in this model implements an exact linear endpoint L on every +allowed input. Include every required dirty return and clean-scratch return in +that endpoint. Replace each gate by + + b += p'(0) T a. + +If p'(0)=0, delete its gate. The extracted word has the same endpoint on the +same allowed input space. For every label, its call count is at most the +original call count. Thus every attainable polynomial call profile is dominated +coordinatewise by an attainable linear profile. The attainable Pareto-minimal +profiles, and the minimum for every nonnegative tariff, are identical in the +two classes. This holds with any finite number of clean or dirty registers. + +## Proof + +Let J be the ideal generated by all independent input coordinates in their +polynomial ring over K. Substitute zero for the initialized clean coordinates. +Every initial register has zero constant term. Inductively this remains true +after each gate because T is linear and p(0)=0. + +Modulo J squared, a polynomial p(u) with u in J equals p'(0)u. Linear T +commutes with taking degree one. Therefore either gate placement induces +exactly the displayed linear shear on the degree-one parts. This proves by +induction in chronological order that the extracted word equals the degree-one +part of the complete original endpoint, including every workspace output. + +Over an infinite field, equality of polynomial functions on all independent +inputs implies equality of their polynomials. For completeness, a univariate +nonzero polynomial has at most its degree many roots. Induction in the number +of variables applies that fact to the coefficient polynomials in the last +variable. Hence an endpoint that is the linear function L has degree-one part +L itself. This proves the endpoint statement. Equivalently the proof is the +chain rule at the common fixed zero state. + +A retained gate has its old T, label, ports, placement and order. Its scalar +p'(0) is in R. A discarded gate induces the identity on degree-one parts. +Consequently no label count increases. Linear gates are already polynomial +gates, proving equality of the profile minima in both directions. The same +argument applies separately at every permitted dimension. If a fixed word +uses a uniform operator family T_f, the single extracted word is independent +of f, so an all-width endpoint gives an all-width extracted endpoint. + +## What the theorem excludes + +Adding zero-preserving pointwise polynomial gates to this labelled linear +helper model cannot evade any call-profile obstruction proved for its full +linear scalar class. This conclusion does not require a common flag, a +commuting operator alphabet, a bound on polynomial degree, or a bound on the +number of borrowed registers across different candidate words. Each word +must be finite. The executable checks a bounded rational subcase. + +The conclusion concerns exactly the same linear output contract. A nonlinear +output could carry different information and require a different consumer. +No selected-word result, supplier lower bound or multiplication theorem is +inferred here. In particular, a lower bound limited to signs or unit scalar +coefficients cannot be used if derivatives introduce other allowed scalars. +Representation changes and their frame, precision, scalar, movement and +restoration costs require their own implementation argument. The theorem +only preserves the declared operator-call labels and the algebraic returns. + +## Essential boundaries + +1. A nonzero constant can move the trajectory away from zero. For example, + adding 1 to a source, adding its square to a target, subtracting 1 from + the source, subtracting the source square from the target, and subtracting + 1 from the target produces the exact linear endpoint target += 2 source. Differentiating each gate at zero separately would + miss the linear term. This word is outside the contract. +2. Over F2, target += source squared is the linear map target += source on + every input, but its formal degree-one part is the identity. Thus the + infinite-field or polynomial-identity hypothesis matters. The same issue + arises on a restricted finite grid inside an infinite field. +3. Linearizing a word never proves that its endpoint is linear. The single + gate target += source + source squared has the same degree-one part as + an addition but has a different endpoint. Exact endpoint verification is + a separate premise; basis-only testing is insufficient. +4. Branching, rounded arithmetic, discontinuous bit operations and nonlinear + address permutations are outside these polynomial data-value gates. + +The degree-one quotient, chain rule and polynomial identity principle are +classical. The contribution is their explicit labelled-profile domination +statement for this helper contract and its bounded executable extraction. diff --git a/research/polynomial-helper-profile-domination/README.md b/research/polynomial-helper-profile-domination/README.md new file mode 100644 index 0000000000..856cd05826 --- /dev/null +++ b/research/polynomial-helper-profile-domination/README.md @@ -0,0 +1,111 @@ +# Polynomial helper gates cannot reduce the labelled linear call minimum + +This contribution was produced by Nick Petalas. + +**Scoped proof with finite exact corroboration; no new kappa.** Grant each +paid linear-operator call a free, fixed coordinatewise polynomial before or +after it. Require every polynomial to fix zero. For an exact linear endpoint +over an infinite field, this extension has exactly the same Pareto-minimal +labelled operator-call profiles as the linear model, with every required dirty +and clean return included. Any finite number of workspace registers is allowed. + +The extraction is explicit: + + b += p(Ta) or b += T p(a) becomes b += p'(0) T a. + +A zero derivative deletes that call. Every other call retains its operator, +ports, label and chronological position. Scalar multiplication by p'(0) must +be permitted in the comparison's linear class. [PROOF.md](PROOF.md) proves the +statement with the degree-one quotient, gives its uniform-family corollary, +and spells out the necessary assumptions. Classical polynomial linearization +is the method; the new step is the declared helper-interface profile theorem +and executable extraction, without any claim of literature priority. + +This rejects one proposed escape route from a linear call lower bound even +when polynomial arithmetic is granted free. It does not exclude arbitrary +nonlinear computation. Nonzero constant gates, branching, finite-grid or +rounded execution, nonlinear address permutations, and changed output +contracts need separate analysis. Actual scalar, frame, native, movement, +precision, stock and compiler costs are not equated by this theorem. The +selected supplier and frontier are unchanged. + +## Exact evidence and reproduction + +The rational implementation in [compiler.py](compiler.py) has a bounded, +validated immutable input contract. It extracts the linear word; it does not +certify the premise that the original endpoint is linear. The checker uses +complete sparse multivariate polynomial expansion to certify that premise +on its fixtures, including every dirty coordinate. A separate dual-number +interpreter corroborates extraction. Literal rational execution checks the +same directions against the known target. The receipt is generated and bound +to SHA256 hashes of all seven source/metadata files. + +The finite corpus has 145 exact linear-endpoint fixtures and 1,029 directions +for each of dual-number and numerical comparison, plus 14 controls. It includes +singular and nonsymmetric operators, rational coefficients, both polynomial +placements, clean and dirty borrowed registers, exact inverses, and successive +blocks with noncommuting operators. The five-gate dirty echo's illustrative +profile changes from `T:3, read:2` to `T:2, read:2`. These labels denote abstract +operator classes, not measured Fourier ranks or selected-word jobs. + +From the worktree root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/polynomial-helper-profile-domination/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/polynomial-helper-profile-domination +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/polynomial-helper-profile-domination --check-source-history +``` + +A portable checkout can use any CPython 3.12 interpreter in those commands. +The registered checks run normal and optimized modes with warnings as errors. +No predecessor mathematical replay, supplier admission, Lean build, Docker +run or complete multiplier is required or claimed. Independent human and +formal proof-kernel review are unclaimed. + +## Relation to previous work + +Jose Manuel / jmbarrancoml's [#1757](https://github.com/CrocSwap/integer-mult-bounds/pull/1757) +proves a cut obstruction for arbitrary deterministic finite-alphabet gates +under frame conditions. The present theorem uses a different infinite-field +polynomial model, has no common-flag premise, and preserves call labels. +Chris R / Clear1nsight's [#3992](https://github.com/CrocSwap/integer-mult-bounds/pull/3992) +uses a generic Jacobian or transcendence-degree bound for a typed Toom-only +boundary. It does not extract a chronological word or compare call profiles. +Both results are cited premises/context, not audit targets or new claims here. +The finite-menu adaptivity investigation claimed in #1166 concerns branch +selection among linear maps and is separate from this fixed nonlinear word. +No predecessor code is copied or executed. Exact context pins are in +[SOURCES.json](SOURCES.json), alongside the current card and selected record. + +## Open next questions + +- Can nonzero constant trajectories produce a genuinely cheaper complete + complex helper word? First account for preparation, constants, the varying + coordinate derivatives, retained outputs and restoration. The explicit + translated-square counterexample only shows why this proof does not apply. +- Can a physical finite-grid polynomial or bit-operation mechanism save calls + while meeting the selected source's precision and all-input requirements? + First specify that grid and the exact nonlinear consumer; the F2 square + control shows why a formal derivative is not a certificate on a finite grid. + +These are reopening conditions, not an implementation campaign. TASK.json +records the changed card, stopping rule and remaining obligations. + +## Verification bounds + +The extractor accepts at most eight roles of width four, 32 gates and scalar +polynomials of degree four. Input numerators and denominators are at most +1,024 in magnitude. Rational evaluation rejects intermediates exceeding +4,096 bits. The finite symbolic checker caps each polynomial at 512 monomials +and total degree 16. It uses no recursion or generated code. Every function +is below 60 physical lines. Explicit runtime checks remain active under `-O`. + +Python's Fraction arithmetic, dictionaries, tuples and standard dataclass +construction allocate dynamically. This is a managed-runtime deviation from +Power of Ten rule 3, restricted to this finite checker/extractor. The input, +term, degree and scalar bounds constrain live state and reject exhaustion. +The small fixture corpus is checked in both modes. A fixed-capacity backend +would be needed if this extractor became a production bounded-memory service; +no such service or physical memory tariff is claimed. Warning-strict replay +and an AST syntax/function-length check are the available diagnostics; no +separate static type checker is a package dependency. diff --git a/research/polynomial-helper-profile-domination/RESULT.json b/research/polynomial-helper-profile-domination/RESULT.json new file mode 100644 index 0000000000..1b49ce023f --- /dev/null +++ b/research/polynomial-helper-profile-domination/RESULT.json @@ -0,0 +1,26 @@ +{ + "claim_type": "scoped proof with finite exact corroboration", + "controls": 14, + "dirty_echo_profile": { + "after": { + "T": 2, + "read": 2 + }, + "before": { + "T": 3, + "read": 2 + } + }, + "dual_and_numeric_directions_each": 1029, + "linear_endpoint_fixtures": 145, + "source_sha256": { + "PROOF.md": "187fc5788d0a033c89c16f0a8b0255cd1f3754d5abb84c786de0fdc4be8a207d", + "README.md": "198a63ce6e68f927fef96f8f7114d7ac78d6cc5bdb17c15b7c1069f6e7829a02", + "SOURCES.json": "01247337000ae4a51c606345c88d912f7e274f1919ced8309e28d659b90fab4c", + "TASK.json": "4cebe6ad9d98bb7d5298f165dec4d611ba797ac289ab81439e11dc7922e3da2b", + "VERIFY.json": "bdfa25ef3e90f2328bf1623bf1b011706e085d2a31085775a6e1cbe9a0892605", + "compiler.py": "47a7aecb033ef80ae83fe0465117420f807d60e1e4ad3e2baabebdb53dfaba6a", + "verify.py": "8ea1457cb1152e834b13a16c5c8fda9e9cf099a10c17bc5d42e620480025d386" + }, + "status": "PASS_POLYNOMIAL_HELPER_PROFILE_DOMINATION" +} diff --git a/research/polynomial-helper-profile-domination/SOURCES.json b/research/polynomial-helper-profile-domination/SOURCES.json new file mode 100644 index 0000000000..771a436a78 --- /dev/null +++ b/research/polynomial-helper-profile-domination/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/current-priorities.md", + "usage": "provenance", + "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91", + "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc" + }, + { + "path": "research/nonlinear-frame-cut-bound/README.md", + "usage": "provenance", + "git_blob": "1fae484c0dc371afb0ec0d0c9b1f781d78dbffbb", + "sha256": "411b78a56180e835bb97e59b9845968d84ad3fb8f5658acde684e4491b3b1c3e" + }, + { + "path": "research/selected-toom3-typed-block/README.md", + "usage": "provenance", + "git_blob": "ad87055215a158817ff90f7599c012cf7a69cf3d", + "sha256": "259a0d675673adb0a5005cbd939029c013acf58b238d18ae216996505293a3a2" + } + ] +} diff --git a/research/polynomial-helper-profile-domination/TASK.json b/research/polynomial-helper-profile-domination/TASK.json new file mode 100644 index 0000000000..a15eba7490 --- /dev/null +++ b/research/polynomial-helper-profile-domination/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the 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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "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": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove and implement zero-state extraction showing equality of Pareto-minimal labelled operator-call profiles between fixed zero-preserving polynomial helper shears and linear shears for exact linear endpoints over an infinite field.", + "scope_change_reason": "Original investigation of nonlinear data-value arithmetic as a changed helper-operation model; this is a scoped obstruction rather than a constructed supplier.", + "bottleneck_link": "Excludes free zero-preserving polynomial processing as a way around the full scalar linear class's labelled operator-call lower bounds. Complete physical and selected supplier costs remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified profile-domination theorem; do not extend to translated, branching or finite-grid programs.", + "outcome": "completed", + "evidence": "PROOF.md gives the quantified theorem; compiler.py extracts a bounded rational word; verify.py checks exact symbolic endpoints, separate dual-number arithmetic, literal rational values, inverses and boundary controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a nonzero constant trajectory lower a complete helper bill?", + "why_it_matters": "The common fixed zero state is essential to this obstruction.", + "first_step": "Specify one translated polynomial word and charge constants, coordinate-dependent derivatives and restoration.", + "blocked_by": "No complete charged word or compatible scalar/frame realization is supplied." + }, + { + "question": "Can a finite-grid nonlinear mechanism save paid calls?", + "why_it_matters": "Polynomial-function equality on a finite grid does not imply a degree-one identity.", + "first_step": "Name the exact grid, precision contract, nonlinear consumer and arbitrary dirty inputs.", + "blocked_by": "Rounded, finite-grid and bit operations are outside this theorem." + } + ] +} diff --git a/research/polynomial-helper-profile-domination/VERIFY.json b/research/polynomial-helper-profile-domination/VERIFY.json new file mode 100644 index 0000000000..8042cab27d --- /dev/null +++ b/research/polynomial-helper-profile-domination/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": 120, + "checks": "Exact polynomial endpoints and inverses, labelled extraction, independent dual-number and numerical comparisons, boundary and invalid-input controls, source-bound receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same coverage with optimized Python; explicit checks must remain enabled." + } + ] +} diff --git a/research/polynomial-helper-profile-domination/compiler.py b/research/polynomial-helper-profile-domination/compiler.py new file mode 100644 index 0000000000..1fd1bd6f0f --- /dev/null +++ b/research/polynomial-helper-profile-domination/compiler.py @@ -0,0 +1,140 @@ +"""Bounded rational implementation of the zero-state linear extraction. + +The universal statement is in PROOF.md. This module does not certify that a +polynomial word has a linear endpoint. Its caller must establish that premise. +""" +from collections import Counter +from dataclasses import dataclass +from fractions import Fraction as Q + +MAX_ROLES = 8 +MAX_WIDTH = 4 +MAX_GATES = 32 +MAX_DEGREE = 4 +MAX_COEFFICIENT = 1024 +MAX_RUNTIME_BITS = 4096 + + +@dataclass(frozen=True) +class Gate: + source: int + target: int + operator: tuple[tuple[Q, ...], ...] + polynomial: tuple[Q, ...] + placement: str + label: str + + +@dataclass(frozen=True) +class Program: + roles: int + width: int + gates: tuple[Gate, ...] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def bounded_scalar(value: Q) -> None: + require(type(value) is Q, "coefficients must be Fractions") + require(abs(value.numerator) <= MAX_COEFFICIENT, "numerator limit") + require(value.denominator <= MAX_COEFFICIENT, "denominator limit") + + +def validate(program: Program) -> None: + require(type(program.roles) is int, "integer role count required") + require(type(program.width) is int, "integer width required") + require(2 <= program.roles <= MAX_ROLES, "role limit") + require(1 <= program.width <= MAX_WIDTH, "width limit") + require(type(program.gates) is tuple, "immutable gate tuple required") + require(len(program.gates) <= MAX_GATES, "gate limit") + for gate in program.gates: + require(type(gate.source) is int and type(gate.target) is int, + "integer ports required") + require(0 <= gate.source < program.roles, "source port") + require(0 <= gate.target < program.roles, "target port") + require(gate.source != gate.target, "aliased ports") + require(gate.placement in ("before", "after"), "polynomial placement") + require(type(gate.label) is str and 1 <= len(gate.label) <= 32, + "paid label") + require(type(gate.operator) is tuple, "immutable operator required") + require(len(gate.operator) == program.width, "operator height") + for row in gate.operator: + require(type(row) is tuple and len(row) == program.width, + "operator width") + for value in row: + bounded_scalar(value) + require(type(gate.polynomial) is tuple, "immutable polynomial required") + require(1 <= len(gate.polynomial) <= MAX_DEGREE + 1, "degree limit") + for value in gate.polynomial: + bounded_scalar(value) + require(gate.polynomial[0] == 0, "gate does not fix zero") + + +def linearize(program: Program) -> Program: + validate(program) + gates = [] + for gate in program.gates: + coefficient = gate.polynomial[1] if len(gate.polynomial) > 1 else Q(0) + if coefficient: + gates.append(Gate(gate.source, gate.target, gate.operator, + (Q(0), coefficient), gate.placement, gate.label)) + result = Program(program.roles, program.width, tuple(gates)) + validate(result) + return result + + +def profile(program: Program) -> dict[str, int]: + validate(program) + return dict(sorted(Counter(gate.label for gate in program.gates).items())) + + +def runtime_scalar(value: Q) -> Q: + require(max(abs(value.numerator).bit_length(), value.denominator.bit_length()) + <= MAX_RUNTIME_BITS, "runtime scalar size limit") + return value + + +def apply_operator(operator: tuple[tuple[Q, ...], ...], + vector: list[Q]) -> list[Q]: + return [runtime_scalar(sum( + (coefficient * value for coefficient, value in zip(row, vector)), Q(0))) + for row in operator] + + +def polynomial_value(coefficients: tuple[Q, ...], value: Q) -> Q: + result = Q(0) + for coefficient in reversed(coefficients): + result = runtime_scalar(result * value + coefficient) + return result + + +def evaluate(program: Program, initial: tuple[Q, ...]) -> tuple[Q, ...]: + validate(program) + require(len(initial) == program.roles * program.width, "input shape") + for value in initial: + bounded_scalar(value) + state = [list(initial[i * program.width:(i + 1) * program.width]) + for i in range(program.roles)] + for gate in program.gates: + source = state[gate.source] + if gate.placement == "after": + image = apply_operator(gate.operator, source) + increment = [polynomial_value(gate.polynomial, value) for value in image] + else: + image = [polynomial_value(gate.polynomial, value) for value in source] + increment = apply_operator(gate.operator, image) + state[gate.target] = [runtime_scalar(old + new) for old, new in + zip(state[gate.target], increment)] + return tuple(value for row in state for value in row) + + +def inverse(program: Program) -> Program: + validate(program) + result = Program(program.roles, program.width, tuple( + Gate(g.source, g.target, g.operator, tuple(-c for c in g.polynomial), + g.placement, g.label) for g in reversed(program.gates))) + validate(result) + return result diff --git a/research/polynomial-helper-profile-domination/verify.py b/research/polynomial-helper-profile-domination/verify.py new file mode 100644 index 0000000000..957cd62f9d --- /dev/null +++ b/research/polynomial-helper-profile-domination/verify.py @@ -0,0 +1,277 @@ +"""Exact finite corroboration; --record writes a generated receipt outside package.""" +import argparse +import hashlib +import json +from dataclasses import replace +from fractions import Fraction as Q +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +from compiler import Gate, Program, evaluate, inverse, linearize, profile, require, validate + +MAX_TERMS = 512 +MAX_TOTAL_DEGREE = 16 +SOURCE_FILES = ("README.md", "PROOF.md", "compiler.py", "verify.py", "TASK.json", + "SOURCES.json", "VERIFY.json") + + +def scale(poly, coefficient): + return {m: c * coefficient for m, c in poly.items() if c * coefficient} + + +def add(left, right): + require(len(left) <= MAX_TERMS and len(right) <= MAX_TERMS, "term input limit") + result = dict(left) + for monomial, coefficient in right.items(): + value = result.get(monomial, Q(0)) + coefficient + if value: + result[monomial] = value + else: + result.pop(monomial, None) + require(len(result) <= MAX_TERMS, "term output limit") + return result + + +def multiply(left, right): + require(len(left) <= MAX_TERMS and len(right) <= MAX_TERMS, "product input limit") + result = {} + for a, x in left.items(): + for b, y in right.items(): + monomial = tuple(i + j for i, j in zip(a, b)) + require(sum(monomial) <= MAX_TOTAL_DEGREE, "symbolic degree limit") + result[monomial] = result.get(monomial, Q(0)) + x * y + require(len(result) <= MAX_TERMS, "product term limit") + return {m: c for m, c in result.items() if c} + + +def substitution(poly, coefficients, variables): + one = {(0,) * variables: Q(1)} + power = one + result = {} + for exponent, coefficient in enumerate(coefficients): + if exponent: + power = multiply(power, poly) + result = add(result, scale(power, coefficient)) + return result + + +def symbolic(program, clean=()): + validate(program) + variables = program.roles * program.width + initial = [{tuple(int(i == j) for i in range(variables)): Q(1)} + if j // program.width not in clean else {} + for j in range(variables)] + state = list(initial) + for gate in program.gates: + start = gate.source * program.width + source = state[start:start + program.width] + if gate.placement == "before": + source = [substitution(p, gate.polynomial, variables) for p in source] + increment = [] + for row in gate.operator: + value = {} + for coefficient, poly in zip(row, source): + value = add(value, scale(poly, coefficient)) + increment.append(value) + if gate.placement == "after": + increment = [substitution(p, gate.polynomial, variables) for p in increment] + for i, value in enumerate(increment): + index = gate.target * program.width + i + state[index] = add(state[index], value) + return initial, state + + +def linear_part(state): + return [{m: c for m, c in poly.items() if sum(m) == 1} for poly in state] + + +def dual_run(program, direction): + """Independent nilpotent arithmetic; no symbolic or extraction routines.""" + state = [(Q(0), c) for c in direction] + for gate in program.gates: + start = gate.source * program.width + values = state[start:start + program.width] + if gate.placement == "before": + values = [dual_polynomial(gate.polynomial, v) for v in values] + image = [(sum((a * v[0] for a, v in zip(row, values)), Q(0)), + sum((a * v[1] for a, v in zip(row, values)), Q(0))) + for row in gate.operator] + if gate.placement == "after": + image = [dual_polynomial(gate.polynomial, v) for v in image] + for i, value in enumerate(image): + index = gate.target * program.width + i + old = state[index] + state[index] = (old[0] + value[0], old[1] + value[1]) + require(all(value == 0 for value, _ in state), "zero trajectory invariant") + return tuple(tangent for _, tangent in state) + + +def dual_polynomial(coefficients, value): + answer = (Q(0), Q(0)) + for coefficient in reversed(coefficients): + a, b = answer + c, d = value + answer = (a * c + coefficient, a * d + b * c) + return answer + + +def operator(rows): + return tuple(tuple(Q(c) for c in row) for row in rows) + + +def fixtures(): + operators = (operator(((1,),)), operator(((1, 1), (1, -1))), + operator(((0, Q(1, 2)), (1, 0))), + operator(((1, 2), (0, 0)))) + cases = [] + for matrix in operators: + for placement in ("before", "after"): + for a in (Q(-1), Q(0), Q(1, 2), Q(1)): + for tail in ((Q(1),), (Q(-1), Q(1)), (Q(0), Q(1), Q(2))): + p = (Q(0), a) + tail + q = (Q(0), Q(1) - a) + tuple(-c for c in tail) + gates = (Gate(0, 1, matrix, p, placement, "paid"), + Gate(0, 1, matrix, q, placement, "paid")) + expected = Program(2, len(matrix), + (replace(gates[0], polynomial=(Q(0), Q(1))),)) + cases.append(("pair", Program(2, len(matrix), gates), expected, ())) + for matrix in operators: + for placement in ("before", "after"): + for a in (Q(0), Q(1, 2), Q(-1)): + cases.append(echo_fixture(matrix, placement, a, ())) + cases.append(echo_fixture(matrix, placement, a, (1,))) + require(len(cases) == 144, "fixture family count") + return cases + + +def echo_fixture(matrix, placement, a, clean): + width = len(matrix) + identity = operator(tuple(tuple(int(i == j) for j in range(width)) + for i in range(width))) + p = (Q(0), a, Q(1), Q(-1)) + u = Gate(0, 1, matrix, p, placement, "T") + v = Gate(1, 2, identity, (Q(0), Q(1)), "after", "read") + gates = (u, v, replace(u, polynomial=tuple(-c for c in p)), + replace(v, polynomial=(Q(0), Q(-1))), + Gate(0, 2, matrix, (Q(0), Q(0), Q(-1), Q(1)), placement, "T")) + expected = Program(3, width, (Gate(0, 2, matrix, (Q(0), a), + placement, "T"),)) + return "echo", Program(3, width, gates), expected, clean + + +def check_fixture(program, expected, clean): + initial, full = symbolic(program, clean) + _, target = symbolic(expected, clean) + require(full == target, "claimed linear endpoint is false") + extracted = linearize(program) + _, tangent = symbolic(extracted, clean) + require(tangent == target == linear_part(full), "extracted endpoint") + before, after = profile(program), profile(extracted) + require(all(count <= before.get(label, 0) for label, count in after.items()), + "profile increased") + double = Program(program.roles, program.width, program.gates + inverse(program).gates) + require(symbolic(double, clean)[1] == initial, "arbitrary-dirt inverse") + n = program.roles * program.width + directions = [tuple(Q(int(i == j)) for i in range(n)) for j in range(n)] + directions += [tuple(Q((i + shift) % 3 - 1) for i in range(n)) + for shift in range(3)] + for vector in directions: + vector = tuple(Q(0) if i // program.width in clean else v + for i, v in enumerate(vector)) + require(dual_run(program, vector) == evaluate(extracted, vector), + "independent dual-number extraction") + require(evaluate(program, vector) == evaluate(expected, vector), + "literal arbitrary-input evaluation") + return len(directions) + + +def controls(): + matrix = operator(((1,),)) + base = Gate(0, 1, matrix, (Q(0), Q(1), Q(1)), "after", "paid") + mutants = (replace(base, source=1), replace(base, source=-1), + replace(base, polynomial=(Q(1), Q(1))), + replace(base, polynomial=(Q(0),) * 6), + replace(base, operator=()), replace(base, placement="somewhere"), + replace(base, label=""), replace(base, polynomial=(Q(0), Q(1025)))) + rejected = 0 + for gate in mutants: + try: + linearize(Program(2, 1, (gate,))) + except ValueError: + rejected += 1 + require(rejected == len(mutants), "invalid gate accepted") + nonlinear = Program(2, 1, (base,)) + full = symbolic(nonlinear)[1] + require(full != symbolic(linearize(nonlinear))[1], "endpoint premise lost") + trap = Program(2, 1, (replace(base, polynomial=(Q(0), Q(-1), Q(1))),)) + for value in ((Q(0), Q(0)), (Q(1), Q(0)), (Q(0), Q(1))): + require(evaluate(trap, value) == value, "basis trap fixture") + require(evaluate(trap, (Q(2), Q(0))) != (Q(2), Q(0)), "basis-only trap lost") + require(linearize(Program(2, 1, (replace(base, polynomial=(Q(0), Q(0), Q(1))),))) + .gates == (), "zero derivative not deleted") + require(all((x * x) % 2 == x for x in range(2)), "finite-field boundary") + for x in range(-3, 4): + require((x + 1) ** 2 - x ** 2 - 1 == 2 * x, + "linear endpoint with nonzero-constant trajectory") + mixing = operator(((1, 1), (0, 1))) + square = Gate(0, 1, mixing, (Q(0), Q(0), Q(1)), "after", "T") + require(evaluate(Program(2, 2, (square,)), (Q(1), Q(1), Q(0), Q(0))) + == (Q(1), Q(1), Q(4), Q(1)), "polynomial after operator") + require(evaluate(Program(2, 2, (replace(square, placement="before"),)), + (Q(1), Q(1), Q(0), Q(0))) + == (Q(1), Q(1), Q(2), Q(1)), "polynomial before operator") + # A noncommuting two-block fixture checks source changes between blocks. + a = echo_fixture(operator(((1, 1), (0, 1))), "after", Q(1), ()) + b = echo_fixture(operator(((0, 1), (1, 0))), "before", Q(1), ()) + remapped = tuple(replace(g, source=2 - g.source, target=2 - g.target) + for g in b[1].gates) + expected_b = tuple(replace(g, source=2 - g.source, target=2 - g.target) + for g in b[2].gates) + combined = Program(3, 2, a[1].gates + remapped) + expected = Program(3, 2, a[2].gates + expected_b) + return rejected + 6, check_fixture(combined, expected, ()) + + +def report(): + dual_cases = 0 + cases = fixtures() + for _, program, expected, clean in cases: + dual_cases += check_fixture(program, expected, clean) + rejected, extra = controls() + hashes = {} + for name in SOURCE_FILES: + path = ROOT / name + require(path.stat().st_size <= 4 * 1024 * 1024, "source size limit") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + sample = echo_fixture(operator(((1, 1), (0, 1))), "after", Q(1), ()) + return {"status": "PASS_POLYNOMIAL_HELPER_PROFILE_DOMINATION", + "claim_type": "scoped proof with finite exact corroboration", + "linear_endpoint_fixtures": len(cases) + 1, + "dual_and_numeric_directions_each": dual_cases + extra, + "controls": rejected, + "dirty_echo_profile": {"before": profile(sample[1]), + "after": profile(linearize(sample[1]))}, + "source_sha256": hashes} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--record", type=Path) + args = parser.parse_args() + result = report() + if args.record: + destination = args.record.resolve() + require(not destination.is_relative_to(ROOT), "record outside package") + with destination.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + path = ROOT / "RESULT.json" + require(path.stat().st_size <= 1024 * 1024, "receipt size limit") + require(result == json.loads(path.read_text()), "receipt mismatch") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()