From 1263091c34f49122a61bc6b3d880931c1b1af405 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Sun, 18 Oct 2026 21:29:48 -0500 Subject: [PATCH] research: audit exact T74 moment endpoints --- .../EXTERNAL-SOURCES.json | 20 ++ research/moment-endpoint-boundary/README.md | 77 ++++++ .../moment-endpoint-boundary/SOURCES.json | 30 +++ research/moment-endpoint-boundary/TASK.json | 66 +++++ research/moment-endpoint-boundary/VERIFY.json | 24 ++ .../inputs/PR3576-PROOF.md | 243 ++++++++++++++++++ .../inputs/PR3576-rate.py | 181 +++++++++++++ research/moment-endpoint-boundary/verify.py | 169 ++++++++++++ 8 files changed, 810 insertions(+) create mode 100644 research/moment-endpoint-boundary/EXTERNAL-SOURCES.json create mode 100644 research/moment-endpoint-boundary/README.md create mode 100644 research/moment-endpoint-boundary/SOURCES.json create mode 100644 research/moment-endpoint-boundary/TASK.json create mode 100644 research/moment-endpoint-boundary/VERIFY.json create mode 100644 research/moment-endpoint-boundary/inputs/PR3576-PROOF.md create mode 100644 research/moment-endpoint-boundary/inputs/PR3576-rate.py create mode 100644 research/moment-endpoint-boundary/verify.py diff --git a/research/moment-endpoint-boundary/EXTERNAL-SOURCES.json b/research/moment-endpoint-boundary/EXTERNAL-SOURCES.json new file mode 100644 index 0000000000..6e90b5744d --- /dev/null +++ b/research/moment-endpoint-boundary/EXTERNAL-SOURCES.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "pull_request": 3576, + "head_commit": "1630afea0fc1083717b5b2799b8de7a819a6ea02", + "base_commit": "20ecf2891d80b5acf18f980b2164fb44ea7faa90", + "files": [ + { + "source_path": "research/t74-retuned-ordinary-layer/PROOF.md", + "local_path": "inputs/PR3576-PROOF.md", + "git_blob": "055c093ffd09b38eebb78e50e179909f007e25f4", + "sha256": "e393df9aaf1a2a1027377cf30e27ea16255d4d2fbefffeef0857f31a64ba7378" + }, + { + "source_path": "research/t74-retuned-ordinary-layer/rate.py", + "local_path": "inputs/PR3576-rate.py", + "git_blob": "99983e724d5faa0828d6508bba18b43f3774881c", + "sha256": "a66e97da03752c72ffabe57048eab80b0fbe00b0d4c4b5a0c7debca845b81d53" + } + ] +} diff --git a/research/moment-endpoint-boundary/README.md b/research/moment-endpoint-boundary/README.md new file mode 100644 index 0000000000..17c9ee00ec --- /dev/null +++ b/research/moment-endpoint-boundary/README.md @@ -0,0 +1,77 @@ +# Exact moment endpoint acceptance audit + +This is a bounded arithmetic audit of the moment acceptance boundary in +[PR #3576](https://github.com/CrocSwap/integer-mult-bounds/pull/3576), head +`1630afea0fc1083717b5b2799b8de7a819a6ea02`. The moment uses the complete T74 +profile and order from the source archive in +[PR #2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979). + +The original `independent-moment` card proposed reconstructing a frame group, +single-change control, and invoice. Live overlap found that PR #3576 already +supplies the complete moment through two exact interval engines, together with +the direct ordinary-rate and one-extra-rank-one controls. This package changes +scope to the uncovered endpoint-consumption question: are the inequalities, +strict boundary, and decimal rounding direction used correctly when accepting +those intervals? + +## Result + +No endpoint-direction or rounding defect was found in the audited acceptance +code. The pinned source tests `upper < 1` for the accepted sigma moment and +`lower > 1` for the two rejected alternatives. It floors the lower endpoint and +ceils the upper endpoint using integer arithmetic. + +The independent `Fraction` check reads the three intervals from the exact +PR3576 proof bytes and verifies these strict comparisons: + +| Case | Exact interval over `10^30` | Exact comparison used | +| --- | --- | --- | +| `sigma = 998271/1000000` | `[999999903535664027556833879161, 999999903535664027556833879162]` | upper `< 1`, with `1 - upper > 9/10^8` | +| ordinary exponent `tau` | `[1000003022093731739239177793276, 1000003022093731739239177793277]` | lower `> 1` | +| sigma with one extra rank-one child | `[1000000111677363244276477808366, 1000000111677363244276477808367]` | lower `> 1` | + +The test uses no floating point and imports neither enclosure engine. Its +canaries put a rational one third of a 30-place unit above and below one, verify +floor/ceiling enclose both values, and show that the corresponding inward +rounding mutations fail. Equality-at-one and intervals straddling one catch +non-strict and wrong-endpoint comparator mutations. The exact proof and rate +source bytes, their Git blob ids, and their SHA256 hashes are retained in +`inputs/` and `EXTERNAL-SOURCES.json`. The rate source's profile/order hashes are +also checked against the live #2979 inputs pinned in `SOURCES.json`. + +These checks validate how the published intervals are consumed. They do not +rederive either enclosure, replay the full T74 package, or establish a supplier +or multiplication theorem. The source claim retains its physical, production, +and outer-transfer limits; the selected frontier is unchanged. + +## Reproduce + +From the repository root: + +```sh +python3 -I -B research/moment-endpoint-boundary/verify.py +python3 scripts/research_package.py --package research/moment-endpoint-boundary --check-only +python3.12 scripts/research_package.py --package research/moment-endpoint-boundary +``` + +The first command runs only the independent endpoint arithmetic and controls. +The package replay runs the same bounded verifier after metadata validation. +The captured PR source bytes can be checked against its exact commit with: + +```sh +git show 1630afea0fc1083717b5b2799b8de7a819a6ea02:research/t74-retuned-ordinary-layer/PROOF.md | sha256sum +git show 1630afea0fc1083717b5b2799b8de7a819a6ea02:research/t74-retuned-ordinary-layer/rate.py | sha256sum +``` + +## Open next questions + +- **Does a future production T74 call path consume this same complete profile and strict moment contract?** This matters because the endpoint check covers the numeric acceptance step only. The first step is to trace the actual retuned constructor into the production T74 call and bind its profile to the pinned `ORDER.json` and `PROFILE.json`. The full production GL64/T74 payload was not run in PR #3576 and remains a blocker to resolving this question here. + +## Credit + +Credit Hiroki Kumazaki and PR #3576 for the rate transfer and its source-pinned +two-engine certificate; Douglas Colkitt and Nick Petalas for the retained +interval engines; Jose Manuel for PR #3562 and the PR #3477 T74 layer; Marius-Paul +Dumitrean and the cited predecessor authors for PR #2979 and its T74 profile. +This audit reuses their interval claims and does not claim a new enclosure +method. New audit code is Apache-2.0. diff --git a/research/moment-endpoint-boundary/SOURCES.json b/research/moment-endpoint-boundary/SOURCES.json new file mode 100644 index 0000000000..48937f571e --- /dev/null +++ b/research/moment-endpoint-boundary/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-joint-endframes/allocation/ORDER.json", + "usage": "input", + "git_blob": "7409c4df1092241729739596c7648bda504e6aad", + "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1" + }, + { + "path": "research/rank7-joint-endframes/allocation/PROFILE.json", + "usage": "input", + "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7", + "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf" + } + ] +} diff --git a/research/moment-endpoint-boundary/TASK.json b/research/moment-endpoint-boundary/TASK.json new file mode 100644 index 0000000000..bc46984b2d --- /dev/null +++ b/research/moment-endpoint-boundary/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "actual_scope": "For PR3576's complete T74 moment intervals over the PR2979 profile and order, independently check the exact inequality direction, strictness, and 30-place outward-rounding boundary with rational endpoint substitutions and corruption controls.", + "scope_change_reason": "Live overlap showed open PR3576 already supplies the full T74 moment computation through two exact engines plus direct-rate and extra-rank-one controls. I narrowed the card to the nonduplicative acceptance boundary and did not reconstruct frames, repeat the invoice, or build another enclosure engine.", + "bottleneck_link": "The T74 moment is the strict gate used to turn the complete paid profile into a layer-rate bound. An endpoint-direction or inward-rounding error could invalidate that local rate step.", + "budget_minutes": 60, + "stop_rule": "Stop after exact rational checks of the three published intervals, both strict inequality directions, the stated sigma gap, and one-unit boundary/rounding canaries. Do not rederive the interval engines or extend into production payload and outer admission.", + "outcome": "completed", + "evidence": "verify.py checks the exact PR3576 proof/rate source bytes, their Git blob IDs, the source-pinned PR2979 PROFILE/ORDER inputs, strict endpoint comparisons, the sigma margin, equality and straddling controls, and outward floor/ceiling behavior near one.", + "author": "Cinna Davis", + "ai_assistance": "OpenAI Codex assisted with source discovery, exact-rational verifier implementation, and packaging.", + "open_questions": [ + { + "question": "Does a future production T74 call path consume the same complete profile and strict moment contract that PR3576 certifies?", + "why_it_matters": "The endpoint audit confirms only the numerical acceptance boundary; source-to-production execution and the inherited physical and outer conditions remain separate.", + "first_step": "Trace the actual production entry point through the retuned constructor into the T74 call and bind its full profile to the pinned ORDER and PROFILE hashes.", + "blocked_by": "PR3576 records no full production GL64/T74 payload execution, and this session did not inspect or run that payload." + } + ] +} diff --git a/research/moment-endpoint-boundary/VERIFY.json b/research/moment-endpoint-boundary/VERIFY.json new file mode 100644 index 0000000000..bbbdf09147 --- /dev/null +++ b/research/moment-endpoint-boundary/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-joint-endframes/allocation/ORDER.json", + "research/rank7-joint-endframes/allocation/PROFILE.json", + "research/moment-endpoint-boundary/inputs/PR3576-PROOF.md", + "research/moment-endpoint-boundary/inputs/PR3576-rate.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source bytes; exact rational moment endpoint directions and gap; strict equality, straddling, corruption, and outward-rounding controls" + } + ] +} diff --git a/research/moment-endpoint-boundary/inputs/PR3576-PROOF.md b/research/moment-endpoint-boundary/inputs/PR3576-PROOF.md new file mode 100644 index 0000000000..055c093ffd --- /dev/null +++ b/research/moment-endpoint-boundary/inputs/PR3576-PROOF.md @@ -0,0 +1,243 @@ +# Retuned ordinary work in the unchanged T74 recursion + +The new result is a conditional rate transfer and an opt-in factory binding. +It combines Jose Manuel's PR3562 ordinary bound at `c=1/577` with his +PR3477 T74 physical layer. It changes neither the T74 word, positive-child +histogram, recursion stop, guard nor root dimension. In particular, it does +not substitute an ordinary exponent directly for a supplier moment exponent. +The two exponents now have the opposite ordering from PR3477's proof. + +PR3562 is pinned at `abb93be8b9ceca07a2b17f3a97db7bb6b074271d`; its complete +[proof](inputs/pr3562-PROOF.md) is retained verbatim with this package. +The canonical T74 inputs are +from main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. `SOURCES.json` and the +factory verifier bind the precise executable and proof inputs. + +## 1. Quantified conditional claim + +Retain PR3477's fixed source-admissible prime `q=213*2^80+1`, T74 native +identities, same-label backward convention, chronological whole-owner +hosting, complete spectators, parent-return protocol, coefficient-height +induction and source-to-physical cost contracts. Retain the complete PR2753 +C0 caller and PR2809/PR2899 ordinary/binary refinement, including the +compatible stock, preparation, elementary primitives, canonical contexts, +fixed tape inventory and successful-return ownership conditions. +PR3562 supplies the stronger ordinary exponent under these premises: + +``` +c=1/577, a=c(1-c)=576/332929, +tau=1-a=332353/332929. +``` + +For the retained T74 root domain take `p>=2`, `d=floor(p^(997/1000))`, +`K=floor(d^(1/500))`, at most `d` selected axes `rho+jK`, and `0<=rho9/10^8`. The geometric-series +constant below is finite, less than `10^8/9`; it is not dropped from the bill. +Both engines use rational arithmetic, with independent logarithm reductions +and outward tail bounds. Their source notices and mathematical attribution +are retained. This package claims no new interval method. + +Two failed alternatives matter for acceptance. At the new ordinary exponent +`tau`, the complete moment is strictly greater than one: + +``` +mu_tau in [1000003022093731739239177793276, + 1000003022093731739239177793277] / 10^30. +``` + +At `sigma`, adding even one rank-one child makes the moment exceed one: + +``` +mu_sigma_with_one_extra_rank1 in + [1000000111677363244276477808366, + 1000000111677363244276477808367] / 10^30. +``` + +Thus neither a direct ordinary-rate substitution nor an unpriced extra +recursive operation is covered. A physical linear cost remains a physical +linear cost; this test does not assign a rank-one tariff to an unspecified +operation. + +## 3. The weighted tree when tau is below sigma + +At an internal node of positive selected width `e`, put `f=floor(e/73)`. +Each rank-`r` child has width `r*f<=r*e/73=1`, `e^tau<=e^sigma`; hence (2) is at most +`C*V_node*e^sigma*((log p)^tau+1)`. Summing (1) over tree levels yields + +``` +T_internal <= C*V_root*d^sigma*((log p)^tau+1)/(1-mu_sigma). +``` + +There is no additional depth factor: the level potentials form a geometric +series. This is the changed step. The predecessor inequality +`e^tau<=d^(tau-sigma)*e^sigma`, useful when `sigma=1`. Because `mu_sigma<=1`, the sum of the potentials +`V_leaf*e_leaf^sigma` over the stopped-leaf antichain is at most the initial +`V_root*d^sigma`. This follows by replacing any internal node by its +children in (1); the tree is finite because every positive child contracts. +The retained elementary leaf cost `O(V_leaf*e_leaf)` therefore sums to + +``` +T_leaf = O(V_root*d^(sigma+beta*(1-sigma))), +sigma+beta*(1-sigma)=998272729/10^9. (3) +``` + +The root's existing front/back/depth reservations retain their cost +`O(V*d^(499/500)*log p)` and all fixed-record setup charges. In the direct +branch, `D<=Q0` and the unchanged reservation formula gives +`Q0=O(log(2d)+d^(499/500)*log p+1)`. Its elementary `O(V*(D+1))` bill is +therefore covered by the same reservation bound, even when `D` grows. +An empty selected set still pays its copies. Only the finitely small `p` +range is absorbed by a fixed constant. Root padding by less than two occurs +once, multiplying the whole internal/leaf bill by a constant. It is not +applied afresh at each recursive child. + +Put `alpha=998273/10^6`. The complete strict power margins are + +| Contribution | Exponent before logarithmic absorption | `alpha` minus exponent | +| --- | --- | --- | +| Internal nodes | `sigma=998271/10^6` | `1/500000` | +| Stopped leaves | `998272729/10^9` | `271/10^9` | +| Root reservations | `499/500` | `273/10^6` | + +Since `d=floor(p^(997/1000))`, `log p=O(log(2d))`. For any fixed positive +`delta` and fixed nonnegative `t`, `(log(2d))^t=O(d^delta)` as `d` tends +to infinity. Apply this with strictly positive margins to the internal and +reservation terms. Equation (3) is below `d^alpha` as well. This proves the +stated layer bound, with constants depending on the fixed margins and source. +There is no logarithm deletion at exponent `sigma`, and no claim that +`.001727` is an optimal layer saving. + +The enlarged fixed precision guard, numerical height induction, root +normalization, one final truncation and pointwise spectator restoration are +unchanged. PR3562 preserves the ordinary endpoint and numerical/context +contracts; it changes the compiled width choice and its uniform cost. The +existing fixed role/parent-parking space proof therefore continues to apply, +with its fixed constants and successful-return interpretation. No complete +GL64/O73 production execution is inferred from this reasoning. + +## 5. Factory binding, controls and remaining boundaries + +`factory.py` supplies opt-in `build_native(q)` and `production_layer(prepared)`. +The factory creates the ordinary backend with the PR3562 profile +`numerator=1, denominator=577`, while retaining the selected row factor, +dimension/rank, catalogue, topology, compiled programs, capacities and +`fixture_index_floor=0`. This ordinary object must be the actual native +argument consumed by the T74 machine and root. An unmodified factory using +the old profile still has the old ordinary exponent and does not justify +this claim. The source-bound factory checks exercise this distinction; +they do not construct the impractical production catalogue. The unchanged +live T74 binding is loaded under a private module name, preserving the +native catalogue's distinct archived `binding` module. Scoped import paths +and module-identity checks bind both implementations without modifying +either source. The constructor recorders cover the complete production +entry point; the reduced-root receipt separately reports actual ordinary +method calls, rather than treating an installed object as an executed call. + +The exact rate controls reject the old ordinary exponent at the proposed +final rate, an earlier `e^500 0, "strict " + name + " power margin") + return dict(internal=internal, leaf=leaf, reservation=reservation, margins=margins) + + +def rejected(action, expected): + try: + action() + except ValueError as error: + need(expected in str(error), "control rejected for the wrong reason") + return True + raise ValueError("control unexpectedly accepted: " + expected) + + +def run(root=ROOT): + profile, order, engines = read_sources(root) + need(TAU == 1 - Q(576, 332929), "PR3562 ordinary exponent") + need(TAU < SIGMA, "changed ordering requires the tau<=sigma tree branch") + moments = two_moments(engines, profile, SIGMA) + need(all(upper < 1 for _lower, upper in moments), "complete T74 moment passes") + # A round, source-relative gap is convenient for the written tree bound. + need(all(1 - upper > Q(9, 10**8) for _lower, upper in moments), + "strict moment gap above nine times ten to minus eight") + rates = budget(TAU, SIGMA, BETA, ALPHA) + need(rates["leaf"] == Q(998272729, 10**9), "actual stopping-rule leaf exponent") + need(rates["margins"] == dict(internal=Q(1, 500000), + leaf=Q(271, 10**9), reservation=Q(273, 10**6)), + "complete exact power margins") + + # These are failed mathematical alternatives, not altered PASS strings. + naive = two_moments(engines, profile, TAU) + need(all(lower > 1 for lower, _upper in naive), + "ordinary exponent cannot itself serve as T74 moment exponent") + extra_child = dict(profile) + extra_child[1] += 1 + extra = two_moments(engines, extra_child, SIGMA) + need(all(lower > 1 for lower, _upper in extra), + "one uncharged rank-one child breaks the chosen moment") + controls = { + "direct_ordinary_moment_rejected_by_both_engines": True, + "one_extra_rank_one_child_rejected_by_both_engines": True, + "old_ordinary_profile_rejected": rejected( + lambda: budget(OLD_TAU, SIGMA, BETA, ALPHA), "strict internal power margin"), + "earlier_stopping_at_power_500_rejected": rejected( + lambda: budget(TAU, SIGMA, Q(1, 500), ALPHA), "strict leaf power margin"), + "omitted_leaf_penalty_target_rejected": rejected( + lambda: budget(TAU, SIGMA, BETA, SIGMA + Q(1, 10**6)), "strict leaf power margin"), + "unabsorbed_internal_log_rejected": rejected( + lambda: budget(TAU, SIGMA, BETA, SIGMA), "strict internal power margin"), + "unabsorbed_reservation_log_rejected": rejected( + lambda: budget(TAU, SIGMA, BETA, ALPHA, ALPHA), "strict reservation power margin"), + } + return dict( + status="PASS_CONDITIONAL_RETUNED_T74_RATE", + calls=len(order), families=FAMILIES, dimension=DIMENSION, + profile={str(rank): count for rank, count in sorted(profile.items())}, + children=sum(profile.values()), rank_mass=sum(r * n for r, n in profile.items()), + sigma=str(SIGMA), ordinary_exponent=str(TAU), stopping_exponent=str(BETA), + internal_exponent=str(rates["internal"]), leaf_exponent=str(rates["leaf"]), + reservation_exponent=str(rates["reservation"]), final_exponent=str(ALPHA), + moment_gap_lower="9/100000000", + moments={"retained_256_bit": outward(moments[0]), + "independent_positive_series": outward(moments[1])}, + rejected_alternatives={ + "direct_ordinary_moment": [outward(value) for value in naive], + "one_extra_rank_one_child": [outward(value) for value in extra]}, + margins={name: str(gap) for name, gap in rates["margins"].items()}, + layer_saving=str(1 - ALPHA), prior_layer_saving=str(1 - OLD_ALPHA), + improvement=str(OLD_ALPHA - ALPHA), controls=controls, + scope="Conditional complete T74 layer with retuned ordinary cost; no payload, integer kappa or outer-transfer admission.") + + +if __name__ == "__main__": + print(json.dumps(run(), indent=2, sort_keys=True)) diff --git a/research/moment-endpoint-boundary/verify.py b/research/moment-endpoint-boundary/verify.py new file mode 100644 index 0000000000..d1e6357a1e --- /dev/null +++ b/research/moment-endpoint-boundary/verify.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""Exact rational audit of the PR3576 moment acceptance boundary.""" + +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import re + + +P = Path(__file__).resolve().parent +ROOT = P.parents[1] +SCALE = 10**30 +HEAD = "1630afea0fc1083717b5b2799b8de7a819a6ea02" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def sha256(data): + return hashlib.sha256(data).hexdigest() + + +def git_blob(data): + header = b"blob " + str(len(data)).encode("ascii") + b"\0" + return hashlib.sha1(header + data).hexdigest() + + +def floor_scaled(value, scale): + return value.numerator * scale // value.denominator + + +def ceil_scaled(value, scale): + return -((-value.numerator * scale) // value.denominator) + + +def below_one(interval): + return interval[1] < 1 + + +def above_one(interval): + return interval[0] > 1 + + +def main(): + ext = json.loads((P / "EXTERNAL-SOURCES.json").read_bytes()) + need(ext["pull_request"] == 3576 and ext["head_commit"] == HEAD + and ext["base_commit"] == "20ecf2891d80b5acf18f980b2164fb44ea7faa90", + "pinned PR3576 head") + rows = { + row["source_path"]: {key: row[key] for key in ("local_path", "git_blob", "sha256")} + for row in ext["files"] + } + expected_sources = { + "research/t74-retuned-ordinary-layer/PROOF.md": { + "local_path": "inputs/PR3576-PROOF.md", + "git_blob": "055c093ffd09b38eebb78e50e179909f007e25f4", + "sha256": "e393df9aaf1a2a1027377cf30e27ea16255d4d2fbefffeef0857f31a64ba7378", + }, + "research/t74-retuned-ordinary-layer/rate.py": { + "local_path": "inputs/PR3576-rate.py", + "git_blob": "99983e724d5faa0828d6508bba18b43f3774881c", + "sha256": "a66e97da03752c72ffabe57048eab80b0fbe00b0d4c4b5a0c7debca845b81d53", + }, + } + need(rows == expected_sources, "exact PR3576 source paths and content pins") + inputs = {} + for source_path, row in rows.items(): + data = (P / row["local_path"]).read_bytes() + need(sha256(data) == row["sha256"], "source SHA256: " + source_path) + need(git_blob(data) == row["git_blob"], "source Git blob: " + source_path) + inputs[source_path] = data + + proof = inputs["research/t74-retuned-ordinary-layer/PROOF.md"].decode("utf-8") + rate = inputs["research/t74-retuned-ordinary-layer/rate.py"].decode("utf-8") + profile_path = "research/rank7-joint-endframes/allocation/PROFILE.json" + order_path = "research/rank7-joint-endframes/allocation/ORDER.json" + profile_hash = sha256((ROOT / profile_path).read_bytes()) + order_hash = sha256((ROOT / order_path).read_bytes()) + need(profile_hash == "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf", + "#2979 paid profile source pin") + need(order_hash == "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1", + "#2979 T74 call order source pin") + for source_path, digest in ((profile_path, profile_hash), (order_path, order_hash)): + need(source_path in rate and digest in rate, "PR3576 rate.py authenticates " + source_path) + + source_contract = ( + 'need(all(upper < 1 for _lower, upper in moments), "complete T74 moment passes")', + 'need(all(lower > 1 for lower, _upper in naive),', + 'need(all(lower > 1 for lower, _upper in extra),', + "lower=lower.numerator * scale // lower.denominator", + "upper=-((-upper.numerator * scale) // upper.denominator)", + ) + need(all(fragment in rate for fragment in source_contract), + "pinned source uses strict endpoint directions and outward rounding") + + numerators = re.findall(r"\[(\d+)\s*,\s*(\d+)\]\s*/\s*10\^30", proof) + expected = [ + ("999999903535664027556833879161", "999999903535664027556833879162"), + ("1000003022093731739239177793276", "1000003022093731739239177793277"), + ("1000000111677363244276477808366", "1000000111677363244276477808367"), + ] + need(numerators == expected, "three exact 30-place intervals from pinned proof") + intervals = [tuple(F(int(endpoint), SCALE) for endpoint in pair) for pair in numerators] + sigma, tau, extra = intervals + need(all(lo <= hi and hi - lo == F(1, SCALE) for lo, hi in intervals), + "adjacent, ordered rational endpoints") + + need(below_one(sigma), "sigma moment upper endpoint is strictly below one") + sigma_gap = 1 - sigma[1] + promised_gap = F(9, 10**8) + need(sigma_gap > promised_gap, "sigma interval clears the strict 9e-8 gap") + need(above_one(tau), "ordinary-exponent lower endpoint is strictly above one") + need(above_one(extra), "extra-rank-one lower endpoint is strictly above one") + + # Equality and straddling canaries catch non-strict and wrong-endpoint tests. + equality = (F(1), F(1)) + straddling = (F(SCALE - 1, SCALE), F(SCALE + 1, SCALE)) + need(not below_one(equality) and not above_one(equality), "strict equality boundary rejects") + need(not below_one(straddling) and not above_one(straddling), + "correct endpoint tests reject an interval straddling one") + need(straddling[0] < 1 and straddling[1] > 1, + "wrong-endpoint mutants would accept the straddling canary") + need(not below_one((sigma[0], F(1))), "sigma upper corruption to equality rejects") + need(not above_one((F(1), tau[1])), "tau lower corruption to equality rejects") + need(not above_one((F(1), extra[1])), "extra rank-one lower corruption to equality rejects") + + # Exercise outward floor/ceiling one third of a decimal ulp from one. + near_below = 1 - F(1, 3 * SCALE) + near_above = 1 + F(1, 3 * SCALE) + low_below, high_below = floor_scaled(near_below, SCALE), ceil_scaled(near_below, SCALE) + low_above, high_above = floor_scaled(near_above, SCALE), ceil_scaled(near_above, SCALE) + need((low_below, high_below) == (SCALE - 1, SCALE), "outward rounding below one") + need((low_above, high_above) == (SCALE, SCALE + 1), "outward rounding above one") + need(F(low_below, SCALE) <= near_below <= F(high_below, SCALE), + "lower/upper rounding encloses below-one rational") + need(F(low_above, SCALE) <= near_above <= F(high_above, SCALE), + "lower/upper rounding encloses above-one rational") + need(F(ceil_scaled(near_below, SCALE), SCALE) > near_below, + "upward-rounded lower-end mutant is inward") + need(F(floor_scaled(near_above, SCALE), SCALE) < near_above, + "downward-rounded upper-end mutant is inward") + + result = { + "status": "PASS_EXACT_MOMENT_ENDPOINT_ACCEPTANCE", + "source_head": HEAD, + "intervals_over_1e30": [list(pair) for pair in numerators], + "sigma_gap": str(sigma_gap), + "sigma_excess_over_9e-8": str(sigma_gap - promised_gap), + "tau_lower_excess_over_one": str(tau[0] - 1), + "extra_rank1_lower_excess_over_one": str(extra[0] - 1), + "controls": { + "strict_equality_rejected": True, + "wrong_endpoint_direction_canary": True, + "sigma_upper_corruption_to_one_rejected": True, + "tau_lower_corruption_to_one_rejected": True, + "extra_lower_corruption_to_one_rejected": True, + "outward_rounding_ulp_canaries": True, + "inward_rounding_mutants_detected": True, + }, + "scope": "Checks exact consumption and outward rounding of the published intervals; does not rederive either moment enclosure.", + } + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()