From d3220b9d9c3748e560e23768556b095217ffb21a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 12 Nov 2026 19:24:32 +0000 Subject: [PATCH] feat(research): derive exact rounded-program lattice hulls --- research/rounded-program-affine-hull/PROOF.md | 172 ++++++++++ .../rounded-program-affine-hull/README.md | 140 ++++++++ .../rounded-program-affine-hull/SOURCES.json | 36 +++ .../rounded-program-affine-hull/TASK.json | 105 ++++++ .../rounded-program-affine-hull/VERIFY.json | 34 ++ .../rounded-program-affine-hull/verify.py | 302 ++++++++++++++++++ 6 files changed, 789 insertions(+) create mode 100644 research/rounded-program-affine-hull/PROOF.md create mode 100644 research/rounded-program-affine-hull/README.md create mode 100644 research/rounded-program-affine-hull/SOURCES.json create mode 100644 research/rounded-program-affine-hull/TASK.json create mode 100644 research/rounded-program-affine-hull/VERIFY.json create mode 100644 research/rounded-program-affine-hull/verify.py diff --git a/research/rounded-program-affine-hull/PROOF.md b/research/rounded-program-affine-hull/PROOF.md new file mode 100644 index 0000000000..28f93a306f --- /dev/null +++ b/research/rounded-program-affine-hull/PROOF.md @@ -0,0 +1,172 @@ +# Exact images and affine-lattice hulls of rounded-linear programs + +## 1. Contract + +Let the independent parameters be `z in Z^k`, with finite `k >= 1`. +A program has finitely many scalar registers. Its initial registers and +every unrounded assignment are rational affine combinations of `z` and +previous registers. A rounded assignment applies + + R(t) = floor(t + 1/2) + +to such a rational affine combination. Outputs are any fixed list of +registers. Write the resulting map as `F: Z^k -> Q^m`. + +This includes a rational affine entrance `x=x0+Bz`, correlated or redundant +parameters, separately rounded shears and rational rescaling. A fixed +rational-grid rounder is a composition of rational scaling, R and scaling +back. No variable products, data-dependent branches, unbounded iteration, +overflow or saturation are included. A finite unrolled sequence is allowed. + +An affine lattice means `y+Lambda`, where Lambda is a finitely generated +additive subgroup of `Q^m`. Its rank may be less than m. These groups are +discrete in their real linear spans because their generators are rational. +All integer combinations use signed, unbounded integer coefficients. + +## 2. A computable translation lattice + +Replace each occurrence of R by the identity map. Propagate the linear +coefficient row of each register with respect to z through this idealized +program. Let `d_j in Q^(1 x k)` be the idealized coefficient row of the +argument of rounded assignment j, and let `M in Q^(m x k)` be the final +output coefficient matrix. Affine constants do not enter these rows. + +Choose any finite-index subgroup `H <= Z^k` such that + + d_j h is an integer for every rounded assignment j and every h in H. (1) + +Such a subgroup always exists. If q is the least common multiple of all +denominators in all d_j, with q=1 when there are no rounded assignments, +then `q Z^k` satisfies (1). Alternatively, the kernel of the finite-image +map `h -> (d_j h mod Z)_j` gives a possibly larger H. Neither choice is +asserted to be the maximal translation subgroup of F. + +**Translation lemma.** For every z in `Z^k` and h in H, + + F(z+h) = F(z) + M h. (2) + +Proof. Induct through the actual program. Initially each register has +exactly its idealized linear drift on replacing z by z+h. Rational affine +combinations preserve this property. At rounded assignment j, the induction +hypothesis makes the actual argument drift exactly `d_j h`. This is an +integer by (1), and `R(t+n)=R(t)+n` for every real t and integer n, including +negative t and half-integer ties. Thus the rounded register has the same +drift as its idealized counterpart. The output rows give (2). No linearity +of the rounded program has been assumed. + +## 3. Exact output set and its smallest affine lattice + +Let C be any complete set of representatives of `Z^k/H`, containing 0, +and let `h_1,...,h_k` be an integer basis of H. Define + + L0 = M H = sum_i Z (M h_i), + G = L0 + sum_(c in C) Z (F(c)-F(0)). + +**Theorem.** The complete, unbounded output set and its smallest containing +affine lattice are exactly + + F(Z^k) = union_(c in C) (F(c) + L0), (3) + hull_Z(F(Z^k)) = F(0) + G. (4) + +Proof of (3). Every z is uniquely c+h with c in C and h in H. Equation +(2) gives `F(z)=F(c)+Mh`. Conversely every element of `F(c)+MH` equals +`F(c+h)` for some h in H. Both inclusions therefore hold, even when M +has a kernel or L0 has smaller rank than the output space. + +Proof of (4). Formula (3) places every output in `F(0)+G`. Conversely, +suppose an affine lattice contains all outputs. Since it contains F(0), +write it as `F(0)+Lambda`. It contains each difference `F(c)-F(0)`. +It also contains `F(h_i)-F(0)=M h_i`. Therefore `G <= Lambda`. +This proves minimality among all affine lattices, including skew lattices +and lattices with lower rank. It proves independence from C, its basis and +the permissible H used to compute the answer. + +For the rectangular choice `H=q Z^k`, (4) gives an explicit finite +generating list with at most `q^k - 1 + k` vectors: + + F(c)-F(0) for c in {0,...,q-1}^k except 0, + q M e_i for i=1,...,k. (5) + +This is an exact finite reduction, not a polynomial-time bound. The +denominator product or the number of input parameters can make q^k large. +No optimality of this generating-list length or period is claimed. + +## 4. Necessary and sufficient closure test + +For a proposed rational target affine lattice `y0+Lambda`, the following +three finite conditions are jointly necessary and sufficient: + + F(0)-y0 belongs to Lambda; + M h_i belongs to Lambda for every basis vector h_i of H; + F(c)-F(0) belongs to Lambda for every c in C. (6) + +This follows directly from (4), or from both inclusions of (3). Membership +in a rational finitely generated lattice is an exact integer-module +problem after clearing denominators. Thus (6) is a decision procedure, +with no numerical tolerance and no bounded-reachability assumption. + +For a sequence of separately specified input and target lattices, applying +(6) at every boundary proves preservation by induction from an admitted +entrance. This is a conditional interface implication. It neither proves +that the chosen entrance describes an actual selected caller nor states +that replacing a nonlinear reachable set by its hull preserves all its +nonlattice information. The lattice hull is the strongest *affine-lattice* +consequence of the given complete parameter domain. + +## 5. Why residue outputs alone are insufficient + +Consider the separately rounded shear on a new input domain + + x=3n, y=2m, + F(n,m) = (3n, 2m + R(3n/2)). + +Here q=2 is a valid rectangular period and + + M = [[3,0],[3/2,2]], + F(0,0) = (0,0), + q M e_1 = (6,3), q M e_2 = (0,4). + +All four residue outputs for `n,m in {0,1}` have even second coordinate. +Checking only these outputs would incorrectly admit target `3Z x 2Z`. +The actual output `F(2,0)=(6,3)` rejects it. The missing obligation is the +drift generator, not another residue representative. + +The residue difference `(3,2)`, the generator `(6,3)` and the residue +difference `(0,2)` generate precisely `3Z x Z`: subtract twice `(3,2)` +from `(6,3)` to obtain `(0,-1)`, then obtain `(3,0)`. Every output has +first coordinate divisible by 3, proving the reverse containment. +Consequently the exact hull is `3Z x Z`, while `(0,1)` belongs to this +hull and is not an output. This distinguishes the hull from the output set. +The idealized output lattice contains `(3,3/2)`, so it would incorrectly +reject the actually valid target `3Z x Z`. Thus ideal-image-only testing +can also give a false closure verdict, in the other direction. + +For this example the larger H with basis `(2,0),(0,1)` uses just two +residue representatives, with drift generators `(6,3),(0,2)`. It yields +the same hull. The proof does not require the rectangular period to be +minimal. + +## 6. Evidence and scope + +The written induction and subgroup argument prove the quantified result. +The companion verifier corroborates it on nested and two-input rational +programs. Its second route computes the integer lattice generated by +literal outputs in a larger signed parameter box, without idealizing any +rounding node. It also checks actual translation identities and explicit +failures of residue-only and ideal-image-only shortcuts. + +woklerx #1848 supplies the source question about closure under intervening +updates and the separate mixed-precision cancellation interface. Adam Gall +#1908 already shows that ideal closure does not imply actual rounded-leaf +closure. Nick Petalas #6446 classifies common invariant planar lattices for +opposite rounded shears. Their results are cited rather than replayed, and +the theorem here does not depend on any of their numerical certificates. +Integer-translation equivariance, lattice normal forms and finite-coset +reasoning are classical. No literature-wide priority is claimed for those +ingredients. The new contribution is this exact output-set/hull formula +and finite closure criterion for the stated rounded-program interface. + +No particular selected native program is admitted. Actual reachable input +domains, physical owners, restoration, movement/storage/precision charges, +the full recursive invoice and the selected five framework assumptions +remain separate. There is no new kappa or complete multiplication theorem. diff --git a/research/rounded-program-affine-hull/README.md b/research/rounded-program-affine-hull/README.md new file mode 100644 index 0000000000..9571157e2a --- /dev/null +++ b/research/rounded-program-affine-hull/README.md @@ -0,0 +1,140 @@ +# Exact affine-lattice output hulls for rounded-linear programs + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written proof with exact finite corroboration. + +For every finite rational rounded-linear program on integer parameters, +the complete output set is a computable finite union of translates of one +lattice. Its smallest containing affine lattice has an explicit finite +generating set. This gives a necessary and sufficient test for closure in +any proposed rational affine target lattice, including changing domains +and internally nested rounding nodes. + +For `R(t)=floor(t+1/2)`, replace each rounding node by the identity and +propagate its argument's rational linear row. Let q clear every denominator +in these rows, M be the idealized output matrix and `C={0,...,q-1}^k`. +Then the new exact formulas are + +```text +F(Z^k) = union_(c in C) (F(c) + q M Z^k) +hull_Z(F(Z^k)) = F(0) + span_Z({q M e_i}_i, {F(c)-F(0)}_c) +``` + +[PROOF.md](PROOF.md) proves translation equivariance by induction through +the actual rounded program and proves both equalities and minimality. +A larger permissible translation lattice may reduce the residue set. +The rectangular formula uses at most `q^k-1+k` generators; it makes no +polynomial-time or minimal-period claim. + +The distinction between residues and drift matters. On the entrance +`x=3n, y=2m`, the shear `(x,y) -> (x,y+R(x/2))` has even second coordinates +on all four q=2 residue representatives. Nevertheless `F(2,0)=(6,3)`. +Its exact affine-lattice hull is `3Z x Z`, while the proposed target +`3Z x 2Z` fails. Ideal-image and residue-only closure tests both miss +information supplied by the formula. The output set itself is smaller +than its hull. + +## Evidence and reproduction + +From the repository root with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rounded-program-affine-hull/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rounded-program-affine-hull/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-program-affine-hull +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-program-affine-hull --check-source-history +``` + +Another CPython 3.12 path may substitute. The last command requires the +committed package. Direct verification is read-only and Git-free. It prints +a generated JSON receipt bound to all six package source hashes, followed +by `PASS_ROUNDED_PROGRAM_AFFINE_HULL`. Both direct modes are registered in +[VERIFY.json](VERIFY.json); the runner reports `PASS_REGISTERED_RESEARCH_PACKAGE`. + +The finite census contains 80 one-parameter nested-rounding programs and +256 two-parameter rounded-shear programs with rational affine entrances. +Across these 336 programs it checks 3,904 residue outputs, 33,696 literal +outputs in signed parameter boxes and 6,336 affine target-closure comparisons. +The literal-output route generates its lattice without idealizing the +rounding nodes. All translation identities and hull comparisons agree. +These are enumerated fixtures, not a count of distinct functions. + +An independent determinantal-minor check and rank-one content check cover +all 729 ordered triples of planar vectors with coordinates in `{-1,0,1}`. +Fourteen named semantic controls cover the drift counterexample, ideal +image, nested denominators, signed ties, a smaller nonrectangular period, +rank-zero and unrounded rational maps. Five malformed-program cases reject. +The universal statements rest on the written proof, rather than this census. + +## Source, credit and scope + +Credit woklerx [#1848](https://github.com/CrocSwap/integer-mult-bounds/pull/1848), +head `d975e19e7e931fc2b45792a4f7140ac13759a7da`, for the explicit question +about closure under intervening rounded updates and the affine-domain +mixed-precision interface. Its cancellation theorem is a cited result. +Retain Gareth Davidson, Chafik Boukhalfa and Ali Romman's precision and +dirty-restoration lineage credited there. + +Adam Gall [#1908](https://github.com/CrocSwap/integer-mult-bounds/pull/1908) +already gives a source-specific internally rounded-leaf counterexample. +Nick Petalas [#6446](https://github.com/CrocSwap/integer-mult-bounds/pull/6446) +classifies a common invariant integer lattice for opposite planar rounded +shears. Those contracts are related context; neither result nor executable +is used as a step in this proof. Their numerical certificates are not +replayed. The new formula and general closure criterion above are the +contribution. The elementary translation, coset and integer-lattice +methods are classical, with no literature-wide priority claim. + +[TASK.json](TASK.json) records a change from the caller-specific +`uniform-transfer-audit` card to this general precision-interface lemma. +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572796) +states the same mathematical scope. Canonical base is +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8 and selected +#7000. [SOURCES.json](SOURCES.json) binds the source question and related +packages as historical provenance. There are no external runtime inputs. + +Live open PRs, this account's recent work, the latest handoff posts, +active discussions, local reservations, main-tree README terms and merged +PR searches were checked. The cached card scan covered 768 open PRs, +7,355 Discussion records and 10,178 local note records, with separately +reported freshness. A dedicated author/date scan of 768 open and 6,175 +closed PRs found no recent account PR referencing #1848. Searches cover +titles, bodies and notes, not every code diff or unpublished result. + +## Limits and verification design + +The contract has fixed rational affine arithmetic and half-up rounding, +with finitely many nodes and unrestricted integer parameters. Variable +products, data-dependent branches, overflow and saturation are excluded. +The output lattice need not equal the actual reachable set. Replacing +a reachable set by its hull discards nonlattice information. + +No actual selected caller, entrance contract or useful precision policy +is established. Complete native implementation, owners and restoration, +movement/storage/precision charges, recursive invoice and all five selected +framework assumptions remain open. No new kappa, supplier admission, +selected-frontier change or complete multiplication theorem is claimed. +Independent human and formal proof-kernel review are unclaimed. No +predecessor scientific replay, selected cold replay, Lean or Docker run +was performed. + +The verifier has no recursion, subprocesses, external libraries or writes. +Its fixture contract limits inputs to two parameters, eight nodes and +period at most 12. Each literal parameter box therefore has at most 1,296 +points; only one program's vectors are live. Package source reads are +capped at 128 KiB each. All checks remain active under optimized Python. +Functions fit within 60 physical lines. Python's dynamic allocation is +a managed-runtime deviation from fixed memory; these bounds constrain +live collections, while no allocation-free or static-analyzer claim is +made. Warning-strict normal and optimized execution provide the available +interpreter diagnostics. + +## Open next questions + +Apply the criterion to one literal selected rounded caller with an admitted +rational affine entrance. First extract its fixed rounded-linear fragment +and compute the residue outputs and drift vectors, then test the next +required source domain. The caller's exact entrance and reachability, +later inverse compatibility and complete precision, movement, storage and +restoration bill remain blockers. No continuation is part of this result; +the structured question is in [TASK.json](TASK.json). diff --git a/research/rounded-program-affine-hull/SOURCES.json b/research/rounded-program-affine-hull/SOURCES.json new file mode 100644 index 0000000000..6120962875 --- /dev/null +++ b/research/rounded-program-affine-hull/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/affine-lattice-inverse-precision/README.md", + "usage": "provenance", + "git_blob": "01d4a83e39092d609b16f81772b8bd057522abd7", + "sha256": "e28d3637dcb322c12205f5754656393f7d066f715a9653a794b879f2e8707373" + }, + { + "path": "research/rounded-leaf-lattice-closure/README.md", + "usage": "provenance", + "git_blob": "505a6b7d6e833b32cb3b6893522dab64a174311f", + "sha256": "8346e7579c265c5c4d96bd61f25c954422ccd74394eca63f41f564085e4f75b8" + }, + { + "path": "research/rounded-shear-lattice-closure/README.md", + "usage": "provenance", + "git_blob": "5d1c98c8cfb62ad29531472000a8385a9571cda3", + "sha256": "dd69ded761a095392f97a620df89227f552991fcb530282d62a2a96daa39095c" + } + ] +} diff --git a/research/rounded-program-affine-hull/TASK.json b/research/rounded-program-affine-hull/TASK.json new file mode 100644 index 0000000000..e235977c6b --- /dev/null +++ b/research/rounded-program-affine-hull/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Prove exact finite-coset output images, smallest affine-lattice hulls and a necessary-and-sufficient target-lattice closure test for finite rational rounded-linear programs on integer parameters.", + "scope_change_reason": "The card asks about a selected caller. This contribution supplies a new general interface lemma motivated by PR1848, with no selected-caller application or discharge of a framework assumption.", + "bottleneck_link": "Correlated precision policies need preservation through actual rounded updates. The finite closure criterion retains both residue outputs and drift generators, avoiding ideal-map and residue-only shortcuts.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved output-hull and closure theorem. Do not extend to an actual selected program or optimize the finite residue enumeration.", + "outcome": "completed", + "evidence": "PROOF.md supplies the quantified proof; verify.py corroborates 336 rational programs with 33,696 literal signed-box outputs, 3,904 residue outputs and 6,336 target affine-lattice closure comparisons.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one literal selected rounded caller preserve a useful affine source domain under this criterion?", + "why_it_matters": "A safe source lattice can support a precision policy only after every reached boundary is proved compatible.", + "first_step": "Extract one fixed rounded-linear fragment and its admitted rational affine entrance; generate its residue outputs and drift vectors, then test the required next source domain.", + "blocked_by": "The exact entrance/reachability contract and complete precision, movement, storage and restoration costs remain unproved." + } + ], + "claim_type": "scoped written proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572796", + "source_question": { + "pr": 1848, + "author": "woklerx", + "head": "d975e19e7e931fc2b45792a4f7140ac13759a7da", + "path": "research/affine-lattice-inverse-precision/README.md", + "section": "Open next questions" + }, + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "upstream_checkpoint": { + "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "checked_at": "2026-11-12T19:23:26Z", + "priority_revision": 8, + "selected_pr": 7000, + "selected_kappa": "363005817/100000000000" + } +} diff --git a/research/rounded-program-affine-hull/VERIFY.json b/research/rounded-program-affine-hull/VERIFY.json new file mode 100644 index 0000000000..402788940f --- /dev/null +++ b/research/rounded-program-affine-hull/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 translation and output-lattice identities, target closure comparisons, independently checked planar normal forms and rejecting boundary controls; generated hash-bound stdout receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact translation and output-lattice identities, target closure comparisons, independently checked planar normal forms and rejecting boundary controls; generated hash-bound stdout receipt." + } + ] +} diff --git a/research/rounded-program-affine-hull/verify.py b/research/rounded-program-affine-hull/verify.py new file mode 100644 index 0000000000..71abb81a10 --- /dev/null +++ b/research/rounded-program-affine-hull/verify.py @@ -0,0 +1,302 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration of PROOF.md; standard library, no writes.""" + +from fractions import Fraction as Q +from hashlib import sha256 +from itertools import product +from math import gcd, lcm +from pathlib import Path +import json + +type Step = tuple[bool, tuple[tuple[int, Q], ...], Q] +type Program = tuple[int, tuple[Step, ...], tuple[int, int]] +type Vector = tuple[Q, Q] + +MAX_STEPS = 8 +MAX_PERIOD = 12 +PACKAGE_FILES = ( + "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py" +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def round_half_up(value: Q) -> Q: + shifted = value + Q(1, 2) + return Q(shifted.numerator // shifted.denominator) + + +def program(k: int, steps: tuple[Step, ...], outputs: tuple[int, int]) -> Program: + require(type(k) is int and 1 <= k <= 2, "parameter count") + require(1 <= len(steps) <= MAX_STEPS, "step count") + for position, (rounded, terms, offset) in enumerate(steps): + require(type(rounded) is bool and isinstance(offset, Q), "step fields") + require(len(terms) <= MAX_STEPS + 2, "term count") + for index, coefficient in terms: + require(type(index) is int and 0 <= index < k + position, "reference") + require(isinstance(coefficient, Q), "coefficient") + require(abs(coefficient) <= 12 and coefficient.denominator <= 12, + "coefficient bound") + require(abs(offset) <= 12 and offset.denominator <= 12, "offset bound") + require(len(outputs) == 2 and all(type(i) is int and 0 <= i < k + len(steps) + for i in outputs), "outputs") + return k, steps, outputs + + +def evaluate(p: Program, z: tuple[int, ...]) -> Vector: + k, steps, outputs = p + require(len(z) == k and all(type(x) is int for x in z), "parameter tuple") + values = [Q(x) for x in z] + for rounded, terms, offset in steps: + value = offset + sum((c * values[i] for i, c in terms), Q(0)) + values.append(round_half_up(value) if rounded else value) + return values[outputs[0]], values[outputs[1]] + + +def linear_data(p: Program) -> tuple[int, tuple[tuple[Q, ...], ...]]: + k, steps, outputs = p + rows = [tuple(Q(i == j) for j in range(k)) for i in range(k)] + period = 1 + for rounded, terms, _offset in steps: + row = tuple(sum((c * rows[i][j] for i, c in terms), Q(0)) + for j in range(k)) + if rounded: + period = lcm(period, *(x.denominator for x in row)) + rows.append(row) + require(period <= MAX_PERIOD, "period capacity") + return period, tuple(rows[i] for i in outputs) + + +def subtract(left: Vector, right: Vector) -> Vector: + return left[0] - right[0], left[1] - right[1] + + +def integer_basis(vectors: list[tuple[int, int]]) -> tuple[tuple[int, int], ...]: + """Column Hermite basis using Bezout on the first coordinate.""" + first, second = 0, 0 + for x, y in vectors: + if x == 0: + continue + if first == 0: + first, second = abs(x), y if x > 0 else -y + continue + divisor = gcd(first, x) + modulus = abs(x) // divisor + a = pow(first // divisor, -1, modulus) if modulus > 1 else 0 + b = (divisor - a * first) // x + require(a * first + b * x == divisor, "Bezout identity") + first, second = divisor, a * second + b * y + if first == 0: + vertical = gcd(*(y for _x, y in vectors)) + return ((0, vertical),) if vertical else () + vertical = gcd(*(y - (x // first) * second for x, y in vectors)) + if vertical: + return (first, second % vertical), (0, vertical) + return ((first, second),) + + +def rational_basis(vectors: list[Vector]) -> tuple[int, tuple[tuple[int, int], ...]]: + denominator = lcm(*(v.denominator for row in vectors for v in row)) + scaled = [(int(x * denominator), int(y * denominator)) for x, y in vectors] + return denominator, integer_basis(scaled) + + +def same_lattice(left: list[Vector], right: list[Vector]) -> bool: + denominator = lcm(*(v.denominator for row in left + right for v in row)) + a = [(int(x * denominator), int(y * denominator)) for x, y in left] + b = [(int(x * denominator), int(y * denominator)) for x, y in right] + return integer_basis(a) == integer_basis(b) + + +def in_hermite(v: Vector, h: int, r: int, k: int) -> bool: + first = v[0] / h + return first.denominator == 1 and ((v[1] - r * first) / k).denominator == 1 + + +def certificate(p: Program) -> tuple[int, Vector, list[Vector], dict]: + k = p[0] + q, matrix = linear_data(p) + base = evaluate(p, (0,) * k) + residues = {c: evaluate(p, c) for c in product(range(q), repeat=k)} + drift = [tuple(q * matrix[j][i] for j in range(2)) for i in range(k)] + generators = drift + [subtract(v, base) for v in residues.values()] + return q, base, generators, residues + + +def check_program(p: Program) -> dict[str, int]: + q, base, generators, residues = certificate(p) + k = p[0] + _q, matrix = linear_data(p) + literal = [] + for z in product(range(-q, 2 * q), repeat=k): + value = evaluate(p, z) + residue = tuple(x % q for x in z) + displacement = tuple(x - r for x, r in zip(z, residue, strict=True)) + expected = tuple(residues[residue][j] + sum( + (matrix[j][i] * displacement[i] for i in range(k)), Q(0)) + for j in range(2)) + require(value == expected, "actual translation identity") + literal.append(subtract(value, base)) + require(same_lattice(generators, literal), "literal output hull") + closure_checks = 0 + if q <= 2: + for h, k2 in product(range(1, 4), repeat=2): + for r in range(k2): + for offset in (Q(0), Q(1, 2)): + anchor = subtract(base, (offset, Q(0))) + claimed = all(in_hermite(v, h, r, k2) + for v in [anchor] + generators) + observed = all(in_hermite(v, h, r, k2) + for v in [anchor] + literal) + require(claimed == observed, "target affine closure") + closure_checks += 1 + return {"programs": 1, "literal_outputs": len(literal), + "residue_outputs": len(residues), "closure_checks": closure_checks} + + +def nested_program(a: Q, b: Q, alpha: Q, beta: Q) -> Program: + return program(1, ( + (True, ((0, a),), alpha), + (True, ((1, b),), beta), + (False, ((2, Q(1, 3)),), Q(0)), + ), (0, 3)) + + +def shear_program(h: int, r: int, k: int, a: Q, b: Q, + alpha: Q, beta: Q) -> Program: + return program(2, ( + (False, ((0, Q(h)),), Q(1, 3)), + (False, ((0, Q(r)), (1, Q(k))), Q(-1, 4)), + (True, ((2, a),), alpha), + (False, ((3, Q(1)), (4, Q(1))), Q(0)), + (True, ((5, b),), beta), + (False, ((2, Q(1)), (6, Q(1))), Q(0)), + ), (7, 5)) + + +def census() -> dict[str, int]: + totals = dict(programs=0, literal_outputs=0, residue_outputs=0, closure_checks=0) + slopes_a = tuple(Q(x, 2) for x in (-3, -1, 0, 1, 3)) + slopes_b = (Q(-2, 3), Q(0), Q(2, 3), Q(3, 2)) + for a, b, alpha, beta in product(slopes_a, slopes_b, (Q(0), Q(1, 2)), + (Q(0), Q(1, 2))): + result = check_program(nested_program(a, b, alpha, beta)) + totals = {key: totals[key] + result[key] for key in totals} + slopes = (Q(-1, 2), Q(0), Q(1, 2), Q(2, 3)) + for h, r, k in ((1, 0, 1), (2, 0, 1), (3, 0, 2), (2, 1, 3)): + for a, b, alpha, beta in product(slopes, slopes, (Q(0), Q(1, 2)), + (Q(0), Q(1, 2))): + result = check_program(shear_program(h, r, k, a, b, alpha, beta)) + totals = {key: totals[key] + result[key] for key in totals} + require(totals["programs"] == 336, "complete program inventory") + return totals + + +def basis_controls() -> int: + """Compare full-rank normal-form indices with every two-column minor.""" + vectors = tuple(product(range(-1, 2), repeat=2)) + for rows in product(vectors, repeat=3): + basis = integer_basis(list(rows)) + minors = gcd(*(a * d - b * c for a, b in rows for c, d in rows)) + if minors: + require(len(basis) == 2, "full-rank normal form") + require(basis[0][0] * basis[1][1] == minors, "index from minors") + else: + require(len(basis) <= 1, "rank-deficient normal form") + nonzero = [v for v in rows if v != (0, 0)] + if nonzero: + x, y = nonzero[0] + content = gcd(x, y) + sign = 1 if x > 0 or (x == 0 and y > 0) else -1 + unit = (sign * x // content, sign * y // content) + scale = gcd(*(coordinate for v in rows for coordinate in v)) + require(basis == ((scale * unit[0], scale * unit[1]),), + "rank-one normal form") + else: + require(basis == (), "zero normal form") + for x, y in rows: + if len(basis) == 2: + h, r = basis[0] + require(in_hermite((Q(x), Q(y)), h, r, basis[1][1]), "basis spans") + return len(vectors) ** 3 + + +def semantic_controls() -> dict: + p = program(2, ( + (False, ((0, Q(3)),), Q(0)), + (False, ((1, Q(2)),), Q(0)), + (True, ((2, Q(1, 2)),), Q(0)), + (False, ((3, Q(1)), (4, Q(1))), Q(0)), + ), (2, 5)) + q, base, generators, residues = certificate(p) + reduced_h = [(Q(6), Q(3)), (Q(0), Q(2)), (Q(3), Q(2))] + nested = nested_program(Q(1, 2), Q(1, 2), Q(0), Q(0)) + zero = program(1, ((True, ((0, Q(0)),), Q(1, 3)),), (1, 1)) + linear = program(1, ((False, ((0, Q(2, 3)),), Q(1, 4)),), (0, 1)) + checks = { + "example period and origin": q == 2 and base == (0, 0), + "residue screen passes": all(in_hermite(v, 3, 0, 2) for v in residues.values()), + "literal drift witness": evaluate(p, (2, 0)) == (6, 3), + "omit-drift rejects": not all(in_hermite(v, 3, 0, 2) for v in generators), + "exact hull": same_lattice(generators, [(Q(3), Q(0)), (Q(0), Q(1))]), + "ideal-image rejects": not in_hermite((Q(3), Q(3, 2)), 3, 0, 1) + and all(in_hermite(v, 3, 0, 1) for v in generators) + and not same_lattice(generators, [(Q(3), Q(3, 2)), (Q(0), Q(2))]), + "nonrectangular period": same_lattice(generators, reduced_h), + "hull not image finite control": all( + evaluate(p, (0, m)) != (0, 1) for m in range(-3, 4)), + "nested denominator": linear_data(nested)[0] == 4, + "actual inner rounding": evaluate(nested, (1,))[1] == Q(1, 3), + "invalid period two rejects": evaluate(nested, (2,))[1] != Q(1, 6), + "signed ties": round_half_up(Q(-1, 2)) == 0 and round_half_up(Q(1, 2)) == 1, + "rank-zero image": rational_basis(certificate(zero)[2]) == (1, ()), + "unrounded rational map": linear_data(linear)[0] == 1, + } + for name, condition in checks.items(): + require(condition, name) + check_program(zero) + check_program(linear) + return {"example_hull": "3Z x Z", "example_rejected_target": "3Z x 2Z", + "example_drift_witness": [6, 3], "semantic_controls": list(checks)} + + +def invalid_controls() -> int: + invalid = ( + (0, ((False, ((0, Q(1)),), Q(0)),), (0, 0)), + (1, ((False, ((1, Q(1)),), Q(0)),), (0, 0)), + (1, ((False, ((0, 1),), Q(0)),), (0, 0)), + (1, ((False, ((0, Q(1, 13)),), Q(0)),), (0, 0)), + (1, ((False, ((0, Q(1)),), Q(0)),), (0, 2)), + ) + rejected = 0 + for args in invalid: + try: + program(*args) + except ValueError: + rejected += 1 + require(rejected == len(invalid), "invalid inputs must reject") + return rejected + + +def main() -> None: + result = census() + result["basis_controls"] = basis_controls() + result.update(semantic_controls()) + result["invalid_controls"] = invalid_controls() + directory = Path(__file__).resolve().parent + hashes = {} + for name in PACKAGE_FILES: + source = directory / name + require(source.stat().st_size <= 128 * 1024, "package source capacity") + data = source.read_bytes() + require(len(data) <= 128 * 1024, "package source capacity") + hashes[name] = sha256(data).hexdigest() + print(json.dumps({"result": result, "sha256": hashes}, sort_keys=True)) + print("PASS_ROUNDED_PROGRAM_AFFINE_HULL") + + +if __name__ == "__main__": + main()