diff --git a/research/kernel102-ideal-dual-audit/EXPECTED.json b/research/kernel102-ideal-dual-audit/EXPECTED.json new file mode 100644 index 0000000000..ed37787b05 --- /dev/null +++ b/research/kernel102-ideal-dual-audit/EXPECTED.json @@ -0,0 +1,24 @@ +{ + "status": "PASS_IDEAL_FIXED_WORD_CEILING", + "source_commit": "71acd0c35ee81de848316b3f2b4c3bd15b219c51", + "rejected_b": "6981767/5000000000", + "kappa_upper": "6981767/5006981767", + "patterns": 112, + "helper_uses": 40320, + "remainder_mass": 66240, + "dual_rank": { + "8": "3447293/500000000", + "16": "3447293/250000000", + "32": "5515669/200000000", + "48": "1756813/62500000" + }, + "dual_width": { + "7": "-10847507113/1000000000000", + "8": "-1723646571/250000000000", + "9": "-183854091/62500000000" + }, + "minimum_dual_slack": "258224826574736894288109385316089/10384593717069655257060992658440192000000000", + "ideal_moment_rejection_margin_lower": "1361549599650598695386388853655702852684001/1940672873845977174439558308009303080960000000000000", + "fallback_charges": "all omitted", + "construction_scope": "Conditional on the frozen local profile and inventories; no scalar reconstruction." +} diff --git a/research/kernel102-ideal-dual-audit/LICENSE b/research/kernel102-ideal-dual-audit/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/kernel102-ideal-dual-audit/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/kernel102-ideal-dual-audit/NOTICE.md b/research/kernel102-ideal-dual-audit/NOTICE.md new file mode 100644 index 0000000000..642caa13f8 --- /dev/null +++ b/research/kernel102-ideal-dual-audit/NOTICE.md @@ -0,0 +1,15 @@ +# Attribution and license + +New proof, checker, and tests: Chinmay (@chinmayarvind23), with substantial +OpenAI Codex assistance, 2026. Apache-2.0; the license is included in LICENSE. + +`inputs/ceiling.json` and `inputs/profile.json` are unchanged files from +chafreaky's PR525 at `71acd0c35ee81de848316b3f2b4c3bd15b219c51`. +Their exact paths and hashes are in `SOURCES.json`. PR525 credits OpenAI Codex +assistance and is Apache-2.0. The model, original dual multipliers and numerical +ceiling are credited to PR525, not claimed as discoveries of this audit. + +PR525's construction inherits the #518 pair factory (Dugongue), #507 partial-own +supplier (eumemic), and earlier credited geometry, response-kernel, scheduling, +and moment work. This package uses their published finite model without +reconstructing those constructions or copying their implementation engines. diff --git a/research/kernel102-ideal-dual-audit/PROOF.md b/research/kernel102-ideal-dual-audit/PROOF.md new file mode 100644 index 0000000000..02f46d9c5c --- /dev/null +++ b/research/kernel102-ideal-dual-audit/PROOF.md @@ -0,0 +1,121 @@ +# The fixed-kernel102 ceiling survives removal of fallback charges + +This is a theorem about the finite packing model in [PR525](https://github.com/CrocSwap/integer-mult-bounds/pull/525) +at `71acd0c35ee81de848316b3f2b4c3bd15b219c51`. Its local profile and inventories +are hypotheses; their realization by the supplier is outside this audit. + +There are 72 calls, dimension `m = 73`, and live stock `W = 7680`. One call has +the following paid rank profile and whole-helper widths: + +| Rank | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | +|---|---:|---:|---:|---:|---:|---:|---:|---:| +| Multiplicity | 2537 | 192 | 506 | 88 | 298 | 68 | 1 | 17 | + +| Helper width | 7 | 8 | 9 | +|---|---:|---:|---:| +| Multiplicity per call | 18 | 164 | 378 | + +The original idle children have ranks 8, 16, 32, 48 with respective counts +5760, 3840, 3840, 3840. Every helper is assigned once, wholly inside one idle +child. Each child leaves at most one paid remainder. We drop timing, owner, +and chart constraints, and allow nonnegative real pattern multiplicities. +Every physical allocation satisfying these hypotheses is in this relaxation. + +For a bin rank `R`, a pattern is `(n7,n8,n9)` of nonnegative integers with +`7*n7 + 8*n8 + 9*n9 <= R`; its leftover is `s = R - 7*n7 - 8*n8 - 9*n9`. +The verifier enumerates all 112 such patterns, including the empty pattern. + +At `b = 6981767/5000000000`, put + +``` +c_b(0) = 0 +c_b(s) = s*((73/s)^b - 1), s > 0. +``` + +Use these rational dual multipliers: + +| Bin rank R | eta_R | +|---|---:| +| 8 | 3447293/500000000 | +| 16 | 3447293/250000000 | +| 32 | 5515669/200000000 | +| 48 | 1756813/62500000 | + +| Width w | lambda_w | +|---|---:| +| 7 | -10847507113/1000000000000 | +| 8 | -1723646571/250000000000 | +| 9 | -183854091/62500000000 | + +The lambda values are PR525's published dual. Each eta is its published value +rounded downward to a multiple of `10^-9`. These small reductions allow the +positive fallback costs used by PR525's original checker to be omitted. + +For every pattern, exact arithmetic proves + +``` +c_b(s) >= eta_R + n7*lambda_7 + n8*lambda_8 + n9*lambda_9. +``` + +Multiply each inequality by its nonnegative pattern multiplicity and sum. The bin-count +equalities yield `sum_R stock_R*eta_R`; the helper-count equalities yield +`72*sum_w widths_w*lambda_w`. This is weak duality, including for fractional +allocations. No solver or assertion about an optimizer is needed. +The negative lambda values are valid because every helper count is an equality, +not a one-sided capacity inequality. + +The remainder rank mass is invariant: + +``` +sum_R R*stock_R - 72*sum_w w*widths_w = 66240. +``` + +Adding the local rank mass gives `73*7680 - 2496 = 558144`. Therefore the ideal +moment of every relaxed allocation has lower bound + +``` +[558144 + 72*sum_r profile_r*c_b(r) + + sum_R stock_R*eta_R + 72*sum_w widths_w*lambda_w] / (73*7680). +``` + +The verifier proves this exceeds `1 + 7/10^10`. The smallest certified pattern +slack exceeds `2/10^11`; the exact rational values are in `EXPECTED.json`. + +## Independent rational arithmetic + +For `1 <= y <= 2`, set `z = (y-1)/(y+1)`. The identity + +``` +log(y) = 2*sum_{j>=0} z^(2*j+1)/(2*j+1) +``` + +has nonnegative terms. Its first 20 terms are a lower bound. Write `x = 2^k*y` +with `1 <= y < 2` and add `k` times the same lower bound for `log(2)`. +For `t >= 0`, the first nine terms `sum_{j=0}^8 t^j/j!` are a lower bound for +`exp(t)`. Monotonicity of exp lets us use the lower log bound as its argument. +Both stages round downward to multiples of `2^-128`. Thus every computed +cost is rigorously at most `c_b(s)`. No tail estimate is needed for these +one-sided inequalities. Rank zero is handled separately with exact cost zero. +The implementation uses only integer arithmetic and `fractions.Fraction`. + +## Consequence and limits + +The ideal moment is strictly increasing in `b >= 0`, since all positive ranks +are below 73. Any endpoint passing the strict moment test must satisfy + +``` +b < 6981767/5000000000. +``` + +Under the same outer relation `kappa <= b/(1+b)` used for PR525's ceiling, +this implies `kappa < 6981767/5006981767`, about `0.001394406315999672`. +Adding any nonnegative fallback +charge preserves the exclusion. The obstruction is already present in the +ideal rank moment; it does not depend on those charges. + +This is the same numerical ceiling as PR525, with a weaker cost assumption and +an independent short proof. It does not exclude changed local words, changed +helper widths or idle stocks, split-helper contracts, different paid-remainder +models, or other multiplication algorithms. It neither improves the selected +construction nor certifies PR525's scalar, physical, outer-assembly, or all-size +obligations. The frozen word hash is provenance, not a reconstruction here. diff --git a/research/kernel102-ideal-dual-audit/README.md b/research/kernel102-ideal-dual-audit/README.md new file mode 100644 index 0000000000..16223ebbff --- /dev/null +++ b/research/kernel102-ideal-dual-audit/README.md @@ -0,0 +1,36 @@ +# Kernel102 packing ceiling without fallback charges + +[PR525](https://github.com/CrocSwap/integer-mult-bounds/pull/525) bounds its fixed +packing family by `kappa < 6981767/5006981767`. This package proves that the same +ceiling holds after **removing every positive fallback charge**: the ideal rank +moment alone exceeds one. This strengthens the cost scope of that historical +ceiling, without changing its value or the repository's selected result. + +The checker enumerates 112 bin patterns and proves their dual inequalities +with exact rational positive log/exp series. It imports neither of PR525's +moment engines and uses no solver, third-party package, or network. + +From this directory, with Python 3.10 or later: + +```sh +python -B verify.py +python -B -m unittest -v test_verify.py +python -O -B -m unittest -v test_verify.py +``` + +The same commands work after copying this directory alone outside the repository. +`EXPECTED.json` records the full deterministic result. `SOURCES.json` pins the +two unchanged input JSON files to PR525's exact head with SHA-256 and Git blob +identities. The checker also verifies the certificate's nomination hash. + +See [PROOF.md](PROOF.md) for the weak-duality argument and arithmetic proof. +The local profile and inventories are explicit hypotheses: this small audit +does not rebuild the supplier or discharge the full PR525 review. No new +frontier bound, optimal packing, Lean theorem, or all-size result is claimed. + +Repository base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. + +Prepared by Chinmay (@chinmayarvind23) with substantial OpenAI Codex assistance. +PR525 author chafreaky supplied the model, source profile, original dual and +numerical ceiling. This package supplies the independent arithmetic proof and +the removal of fallback charges. See [NOTICE.md](NOTICE.md). diff --git a/research/kernel102-ideal-dual-audit/SOURCES.json b/research/kernel102-ideal-dual-audit/SOURCES.json new file mode 100644 index 0000000000..5be2bb1c6b --- /dev/null +++ b/research/kernel102-ideal-dual-audit/SOURCES.json @@ -0,0 +1,19 @@ +{ + "commit": "71acd0c35ee81de848316b3f2b4c3bd15b219c51", + "pull_request": 525, + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "files": [ + { + "path": "inputs/ceiling.json", + "sha256": "fc5140e319385473e9ef7195009366fa71822c7f117b215059416ab95ee149a2", + "source_path": "research/partial-own-kernel102-asynchronous/discovery/CEILING102.json", + "git_blob": "41afbcc9479f7483b320c4da27ac7373524876ab" + }, + { + "path": "inputs/profile.json", + "sha256": "62510a6c1ba61863e74905064a959f980856afc13963d3eac50e6e9f7a5a4dad", + "source_path": "research/partial-own-kernel102-asynchronous/discovery/PROFILE102.json", + "git_blob": "8ee827142d16dcd9b4a544ef67279f5884a5538e" + } + ] +} diff --git a/research/kernel102-ideal-dual-audit/VALIDATION.md b/research/kernel102-ideal-dual-audit/VALIDATION.md new file mode 100644 index 0000000000..0aa976a693 --- /dev/null +++ b/research/kernel102-ideal-dual-audit/VALIDATION.md @@ -0,0 +1,35 @@ +# Local validation + +Validated on 2026-10-13 in the official Linux Python image pinned by digest: + +``` +python@sha256:a6e34c598f2467ed0e9a8d349809fcd8b5c603269512df273a0bb1784edc11b1 +``` + +The container had networking disabled, a read-only root and package mount, +all capabilities dropped, no-new-privileges, 512 MiB memory, one CPU, and a +16 MiB temporary filesystem. No upstream code was executed on the host. + +From the package directory, all three commands passed: + +```sh +python -B verify.py +python -B -m unittest -v test_verify.py +python -O -B -m unittest -v test_verify.py +``` + +Each unittest run passed 10 tests, including 26 negative cases: each of the +seven dual coordinates, a feasible but insufficient dual, missing coordinates, +model and endpoint changes, invalid arithmetic domains, and source corruption. +These semantic controls call the mathematical checker directly so rejection +does not merely reflect a changed file hash. Separate source controls exercise +the package boundary. Relocation to a directory without repository context +reproduced the exact result. + +The output matches every field in `EXPECTED.json`: all 112 patterns pass, the +minimum slack exceeds `2/10^11`, and the ideal moment exceeds `1 + 7/10^10`. +Tests pass with Python assertions disabled because acceptance uses explicit +checks. The two input files were compared with their exact PR525 Git blobs. + +This records local tests only. No GitHub CI run or cold reconstruction of +PR525's scalar/physical supplier is claimed. diff --git a/research/kernel102-ideal-dual-audit/inputs/ceiling.json b/research/kernel102-ideal-dual-audit/inputs/ceiling.json new file mode 100644 index 0000000000..41afbcc947 --- /dev/null +++ b/research/kernel102-ideal-dual-audit/inputs/ceiling.json @@ -0,0 +1,38 @@ +{ + "status": "EXACT_DUAL_REJECTS_FIXED_WORD_PACKING_RATE", + "rejected_b": "6981767/5000000000", + "rejected_b_decimal": "0.0013963534", + "kappa_upper": "6981767/5006981767", + "kappa_upper_decimal": "0.001394406315999672383069015477802917271937411470905402240503105870407297", + "rank_stock": { + "16": 3840, + "8": 5760, + "32": 3840, + "48": 3840 + }, + "helper_widths": { + "9": 378, + "8": 164, + "7": 18 + }, + "calls": 72, + "remainder_mass": 66240, + "patterns": 112, + "dual_rank": { + "8": "1723646571/250000000000", + "16": "1723646571/125000000000", + "32": "1723646571/62500000000", + "48": "13725101583018269638981348883856899763231/488281250000000000000000000000000000000000" + }, + "dual_width": { + "7": "-10847507113/1000000000000", + "8": "-1723646571/250000000000", + "9": "-183854091/62500000000" + }, + "min_exact_dual_slack": "0", + "mercator_rejection_margin": "5018732632837207528776629207053395657161124930651556382887178683773394978930474071061580109/6992010905200617916259958311373285650260497244962684928000000000000000000000000000000000000000000000", + "base_two_rejection_margin": "523980135563882060771452539918656982389/730000000000000000000000000000000000000000000000", + "nomination_sha256": "62510a6c1ba61863e74905064a959f980856afc13963d3eac50e6e9f7a5a4dad", + "rank_stock_source_sha256": "d2445e2b1e2eddf4aad72dc4f5211a62eb3e42dfeb08c49bae1949783d0ec5d6", + "scope": "UNADMITTED structural candidate profile from the hashed nomination. Conditional exclusion only if that profile and width inventory hold:72calls,m73,W7680,deficit2496 and unchanged idle ranks; whole helpers assigned once each, one remainder per original idle child. Drops all time, owner-conflict and chart restrictions. Does not bound changed local words, split-child contracts or all algorithms." +} diff --git a/research/kernel102-ideal-dual-audit/inputs/profile.json b/research/kernel102-ideal-dual-audit/inputs/profile.json new file mode 100644 index 0000000000..8ee827142d --- /dev/null +++ b/research/kernel102-ideal-dual-audit/inputs/profile.json @@ -0,0 +1,18 @@ +{ + "profile": { + "1": 2537, + "2": 192, + "3": 506, + "4": 88, + "5": 298, + "8": 17, + "6": 68, + "7": 1 + }, + "widths": { + "9": 378, + "8": 164, + "7": 18 + }, + "word_sha256": "a56423fac9f06d864a42a32450a7dba22389330262551cd266066cb074202828" +} diff --git a/research/kernel102-ideal-dual-audit/test_verify.py b/research/kernel102-ideal-dual-audit/test_verify.py new file mode 100644 index 0000000000..8a4953a232 --- /dev/null +++ b/research/kernel102-ideal-dual-audit/test_verify.py @@ -0,0 +1,123 @@ +"""Semantic controls deliberately bypass source hashes, plus package controls.""" + +import copy +import json +import shutil +import tempfile +import unittest +from pathlib import Path + +import verify as v + +ROOT = Path(__file__).resolve().parent + + +class DualAuditTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.profile, cls.certificate = v.load_inputs(ROOT) + cls.result = v.audit(cls.profile, cls.certificate) + cls.eta = {int(k): v.Q(x) for k, x in cls.result["dual_rank"].items()} + cls.lam = {int(k): v.Q(x) for k, x in cls.result["dual_width"].items()} + + def test_exact_expected_report_and_strict_margins(self): + self.assertEqual(self.result, json.loads((ROOT / "EXPECTED.json").read_bytes())) + self.assertGreater(v.Q(self.result["minimum_dual_slack"]), v.Q(2, 10**11)) + self.assertGreater(v.Q(self.result["ideal_moment_rejection_margin_lower"]), v.Q(7, 10**10)) + + def test_every_rank_multiplier_corruption(self): + for rank in self.eta: + with self.subTest(rank=rank): + eta = dict(self.eta) + eta[rank] += v.Q(1, 10**4) + with self.assertRaisesRegex(ValueError, "dual inequality"): + v.check_dual(eta, self.lam) + + def test_every_width_multiplier_corruption(self): + for width in self.lam: + with self.subTest(width=width): + lam = dict(self.lam) + lam[width] += v.Q(1, 10**4) + with self.assertRaisesRegex(ValueError, "dual inequality"): + v.check_dual(self.eta, lam) + + def test_feasible_but_too_weak_dual_is_rejected(self): + eta = {r: x - 1 for r, x in self.eta.items()} + with self.assertRaisesRegex(ValueError, "ideal moment does not reject"): + v.check_dual(eta, self.lam) + + def test_missing_dual_coordinates(self): + for original, other, is_eta in ((self.eta, self.lam, True), (self.lam, self.eta, False)): + changed = dict(original) + del changed[next(iter(changed))] + with self.assertRaisesRegex(ValueError, "dual .* keys"): + v.check_dual(changed, other) if is_eta else v.check_dual(other, changed) + + def test_changed_model_inputs(self): + mutations = [ + ("profile", "profile", "1"), + ("profile", "widths", "7"), + ("certificate", "helper_widths", "9"), + ("certificate", "rank_stock", "48"), + ] + for target, field, key in mutations: + with self.subTest(target=target, field=field): + profile, certificate = copy.deepcopy(self.profile), copy.deepcopy(self.certificate) + obj = profile if target == "profile" else certificate + obj[field][key] += 1 + with self.assertRaises(ValueError): + v.audit(profile, certificate) + for field in ("calls", "patterns", "remainder_mass"): + with self.subTest(field=field): + certificate = copy.deepcopy(self.certificate) + certificate[field] += 1 + with self.assertRaises(ValueError): + v.audit(self.profile, certificate) + + def test_changed_endpoints(self): + for field in ("rejected_b", "kappa_upper"): + with self.subTest(field=field): + certificate = copy.deepcopy(self.certificate) + certificate[field] = str(v.Q(certificate[field]) + v.Q(1, 10**10)) + with self.assertRaises(ValueError): + v.audit(self.profile, certificate) + + def test_positive_series_domains_and_zero_rank(self): + self.assertEqual(v.rank_cost_lower(0), 0) + self.assertEqual(v.rank_cost_lower(1, v.Q(0)), 0) + self.assertEqual(v.log_lower(v.Q(1)), 0) + self.assertEqual(v.exp_lower(v.Q(0)), 1) + for callback, arg in ((v.log_lower, v.Q(1, 2)), (v.exp_lower, v.Q(-1)), + (v.rank_cost_lower, -1), (v.rank_cost_lower, 73)): + with self.subTest(arg=arg), self.assertRaises(ValueError): + callback(arg) + + def test_relocated_package_and_source_corruption(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) / "standalone" + shutil.copytree(ROOT, root) + self.assertEqual(v.audit(*v.load_inputs(root)), self.result) + path = root / "inputs/profile.json" + path.write_bytes(path.read_bytes() + b" ") + with self.assertRaisesRegex(ValueError, "source sha256"): + v.load_inputs(root) + + def test_source_head_and_file_set(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) / "standalone" + shutil.copytree(ROOT, root) + path = root / "SOURCES.json" + manifest = json.loads(path.read_bytes()) + manifest["commit"] = "0" * 40 + path.write_text(json.dumps(manifest)) + with self.assertRaisesRegex(ValueError, "source commit"): + v.load_inputs(root) + manifest["commit"] = v.SOURCE_COMMIT + manifest["files"].pop() + path.write_text(json.dumps(manifest)) + with self.assertRaisesRegex(ValueError, "source file set"): + v.load_inputs(root) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/kernel102-ideal-dual-audit/verify.py b/research/kernel102-ideal-dual-audit/verify.py new file mode 100644 index 0000000000..061cf915cd --- /dev/null +++ b/research/kernel102-ideal-dual-audit/verify.py @@ -0,0 +1,159 @@ +"""Independent exact proof of the PR525 packing ceiling without fallback charges.""" + +import hashlib +import itertools +import json +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path + +SOURCE_COMMIT = "71acd0c35ee81de848316b3f2b4c3bd15b219c51" +M, LIVE, CALLS = 73, 7680, 72 +B = Q(6981767, 5000000000) +GRID = 1 << 128 +PROFILE = {1: 2537, 2: 192, 3: 506, 4: 88, 5: 298, 6: 68, 7: 1, 8: 17} +WIDTHS = {7: 18, 8: 164, 9: 378} +STOCK = {8: 5760, 16: 3840, 32: 3840, 48: 3840} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def floor_grid(value): + return Q(value.numerator * GRID // value.denominator, GRID) + + +def log_series(value): + """Twenty positive terms of 2*atanh((value-1)/(value+1)).""" + require(Q(1) <= value <= Q(2), "log series domain") + z = (value - 1) / (value + 1) + term, total = z, Q(0) + for k in range(20): + total += term / (2 * k + 1) + term *= z * z + return 2 * total + + +@lru_cache(None) +def log_lower(value): + require(value >= 1, "log domain") + powers = 0 + while value >= 2: + value /= 2 + powers += 1 + return floor_grid(powers * log_series(Q(2)) + log_series(value)) + + +def exp_lower(value): + require(value >= 0, "exp domain") + term, total = Q(1), Q(1) + for k in range(1, 9): + term *= value / k + total += term + return floor_grid(total) + + +@lru_cache(None) +def rank_cost_lower(rank, rate=B): + """Lower bound on r*((73/r)**rate - 1); no fallback term.""" + require(isinstance(rank, int) and 0 <= rank < M, "rank domain") + require(rate >= 0, "rate domain") + if rank == 0: + return Q(0) + return rank * (exp_lower(rate * log_lower(Q(M, rank))) - 1) + + +def patterns(): + # Complete enumeration; includes empty bins and zero-remainder bins. + return [ + (rank, counts, rank - sum(w * n for w, n in zip(WIDTHS, counts))) + for rank in STOCK + for counts in itertools.product(*(range(rank // w + 1) for w in WIDTHS)) + if sum(w * n for w, n in zip(WIDTHS, counts)) <= rank + ] + + +def check_dual(eta, lam, rate=B): + require(set(eta) == set(STOCK), "dual rank keys") + require(set(lam) == set(WIDTHS), "dual width keys") + rows = patterns() + require(len(rows) == 112, "pattern count") + slacks = [ + rank_cost_lower(left, rate) - eta[rank] + - sum(lam[w] * n for w, n in zip(WIDTHS, counts)) + for rank, counts, left in rows + ] + require(min(slacks) >= 0, "dual inequality fails") + residual_mass = sum(r * n for r, n in STOCK.items()) - CALLS * sum( + w * n for w, n in WIDTHS.items() + ) + fixed_mass = CALLS * sum(r * n for r, n in PROFILE.items()) + require(residual_mass == 66240, "remainder mass") + require(fixed_mass + residual_mass == M * LIVE - 2496, "rank conservation") + fixed_extra = CALLS * sum(n * rank_cost_lower(r, rate) for r, n in PROFILE.items()) + dual_extra = sum(n * eta[r] for r, n in STOCK.items()) + CALLS * sum( + n * lam[w] for w, n in WIDTHS.items() + ) + margin = (fixed_mass + residual_mass + fixed_extra + dual_extra) / (M * LIVE) - 1 + require(margin > 0, "ideal moment does not reject") + return min(slacks), margin + + +def audit(profile, certificate): + require({int(k): v for k, v in profile["profile"].items()} == PROFILE, "local profile") + require({int(k): v for k, v in profile["widths"].items()} == WIDTHS, "profile widths") + require({int(k): v for k, v in certificate["helper_widths"].items()} == WIDTHS, "helper widths") + require({int(k): v for k, v in certificate["rank_stock"].items()} == STOCK, "rank stock") + require(certificate["calls"] == CALLS, "call count") + require(certificate["patterns"] == 112, "certificate pattern count") + require(certificate["remainder_mass"] == 66240, "certificate remainder mass") + require(Q(certificate["rejected_b"]) == B, "rejected rate") + require(Q(certificate["kappa_upper"]) == B / (1 + B), "kappa transform") + # Lower the published multipliers to allow removal of its positive fallback. + eta = {int(k): Q((Q(v) * 10**9).__floor__(), 10**9) + for k, v in certificate["dual_rank"].items()} + lam = {int(k): Q(v) for k, v in certificate["dual_width"].items()} + minimum_slack, margin = check_dual(eta, lam) + return { + "status": "PASS_IDEAL_FIXED_WORD_CEILING", + "source_commit": SOURCE_COMMIT, + "rejected_b": str(B), + "kappa_upper": str(B / (1 + B)), + "patterns": 112, + "helper_uses": CALLS * sum(WIDTHS.values()), + "remainder_mass": 66240, + "dual_rank": {str(k): str(v) for k, v in sorted(eta.items())}, + "dual_width": {str(k): str(v) for k, v in sorted(lam.items())}, + "minimum_dual_slack": str(minimum_slack), + "ideal_moment_rejection_margin_lower": str(margin), + "fallback_charges": "all omitted", + "construction_scope": "Conditional on the frozen local profile and inventories; no scalar reconstruction.", + } + + +def load_inputs(root): + manifest = json.loads((root / "SOURCES.json").read_bytes()) + require(manifest["commit"] == SOURCE_COMMIT, "source commit") + files = manifest["files"] + require(len(files) == 2 and {f["path"] for f in files} == { + "inputs/profile.json", "inputs/ceiling.json" + }, "source file set") + for item in files: + raw = (root / item["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == item["sha256"], "source sha256") + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + require(hashlib.sha1(blob).hexdigest() == item["git_blob"], "source git blob") + raw_profile = (root / "inputs/profile.json").read_bytes() + profile = json.loads(raw_profile) + certificate = json.loads((root / "inputs/ceiling.json").read_bytes()) + require(hashlib.sha256(raw_profile).hexdigest() == certificate["nomination_sha256"], "nomination binding") + return profile, certificate + + +if __name__ == "__main__": + root = Path(__file__).resolve().parent + result = audit(*load_inputs(root)) + require(result == json.loads((root / "EXPECTED.json").read_bytes()), "expected report") + print(json.dumps(result, indent=2))