From 7519539e28eaa59f6cb1ebc7a83413ade5521afa Mon Sep 17 00:00:00 2001 From: Stephan Arrington <284007938+steph4n-gh@users.noreply.github.com> Date: Mon, 12 Oct 2026 23:38:35 -0400 Subject: [PATCH] Add exact integer exponential intervals with pinned replay evidence --- .github/workflows/exact-exp-performance.yml | 22 ++ research/exact-exp-performance/CLAIM.json | 60 +++++ research/exact-exp-performance/NOTICE.md | 24 ++ research/exact-exp-performance/README.md | 174 ++++++++++++++ research/exact-exp-performance/SOURCE.json | 20 ++ research/exact-exp-performance/benchmark.py | 106 +++++++++ .../evidence/benchmark-python313.json | 124 ++++++++++ .../evidence/benchmark-python314.json | 124 ++++++++++ .../evidence/initial-benchmark-python313.json | 119 ++++++++++ .../evidence/initial-benchmark-python314.json | 119 ++++++++++ .../evidence/tests-python313-optimized.txt | 17 ++ .../evidence/tests-python314.txt | 17 ++ research/exact-exp-performance/fast_exp.py | 40 ++++ research/exact-exp-performance/run.py | 75 +++++++ research/exact-exp-performance/test_exp.py | 212 ++++++++++++++++++ research/exact-exp-performance/test_replay.py | 210 +++++++++++++++++ 16 files changed, 1463 insertions(+) create mode 100644 .github/workflows/exact-exp-performance.yml create mode 100644 research/exact-exp-performance/CLAIM.json create mode 100644 research/exact-exp-performance/NOTICE.md create mode 100644 research/exact-exp-performance/README.md create mode 100644 research/exact-exp-performance/SOURCE.json create mode 100644 research/exact-exp-performance/benchmark.py create mode 100644 research/exact-exp-performance/evidence/benchmark-python313.json create mode 100644 research/exact-exp-performance/evidence/benchmark-python314.json create mode 100644 research/exact-exp-performance/evidence/initial-benchmark-python313.json create mode 100644 research/exact-exp-performance/evidence/initial-benchmark-python314.json create mode 100644 research/exact-exp-performance/evidence/tests-python313-optimized.txt create mode 100644 research/exact-exp-performance/evidence/tests-python314.txt create mode 100644 research/exact-exp-performance/fast_exp.py create mode 100644 research/exact-exp-performance/run.py create mode 100644 research/exact-exp-performance/test_exp.py create mode 100644 research/exact-exp-performance/test_replay.py diff --git a/.github/workflows/exact-exp-performance.yml b/.github/workflows/exact-exp-performance.yml new file mode 100644 index 0000000000..350353b230 --- /dev/null +++ b/.github/workflows/exact-exp-performance.yml @@ -0,0 +1,22 @@ +name: Exact exponential interval checks + +on: + pull_request: + paths: + - 'research/exact-exp-performance/**' + - '.github/workflows/exact-exp-performance.yml' + workflow_dispatch: + +jobs: + focused-checks: + runs-on: ubuntu-latest + strategy: + matrix: + python: ['3.11', '3.14'] + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - name: Exact arithmetic and full checker controls + run: python -B -m unittest discover -s research/exact-exp-performance -p 'test_*.py' -v diff --git a/research/exact-exp-performance/CLAIM.json b/research/exact-exp-performance/CLAIM.json new file mode 100644 index 0000000000..b7db7684c5 --- /dev/null +++ b/research/exact-exp-performance/CLAIM.json @@ -0,0 +1,60 @@ +{ + "track": "Verification engineering", + "assignment_seed": 91, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "started_utc": "2026-10-13T03:25:21Z", + "claimed_utc": "2026-10-13T03:27:07.120724+00:00", + "expected_finish_utc": "2026-10-13T04:10:00Z", + "time_budget": "45-minute cap; orientation completed in under 2 minutes; final verification/handoff phase begins at the recorded time and occupies at least the final quarter of actual work.", + "coordination": "No pinned issues and no sprint coordination issue among the open issues; local claim per sprint instructions.", + "candidates": [ + "Clifford state evaluation (overlaps PR662)", + "Independent owner-checker exact exponential intervals (selected: 91 modulo 3 = 1)", + "Streaming selected inventory hashes (unmeasured benefit)" + ], + "scope": "The 16-term Taylor exponential interval helper in research/complex-k492-owner-repair/extras/exact_intervals.py, used by the independent owner-map moment check.", + "hypothesis": "Homogeneous integer polynomial evaluation can return exactly the same rational lower/upper bounds with fewer Fraction reductions.", + "method": "Same 16 Taylor terms, same tail x^17/(17!*(1-x/18)), same 200-bit outward rounding, exact input domain 0 <= a <= b < 1; differential tests and same-input alternating benchmarks, including the complete pinned independent owner check if fixtures are available.", + "deliverable": "Opt-in source-pinned kernel and replay adapter, exact equivalence argument, negative controls, raw before/after timings, no new kappa.", + "overlap_review": { + "open_pr_count": 488, + "most_recent_seen": 668, + "relevant_prs": [ + 662, + 667, + 367, + 452, + 333, + 220 + ], + "distinction": "PR667 optimizes a logarithm helper in a different moment engine; this work changes only the independent checker exponential polynomial. No dependency on pending PR code." + }, + "limits": "No frozen sources or selected frontier edits; finite validation is not a full multiplication theorem.", + "final_verification_started_utc": "2026-10-13T03:35:00Z", + "overlap_refresh": { + "checked_utc": "2026-10-13T03:36:28.422795+00:00", + "open_pr_count": 491, + "highest_number": 671, + "pinned_coordination_issues": [], + "main_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "exact_intervals_search_results": [], + "exponential_search_results": [ + 479, + 67, + 605, + 229, + 91, + 70, + 634, + 585 + ], + "assessment": "No competing exponential-kernel implementation found; PR667 logarithm optimization is adjacent but distinct." + }, + "result": { + "status": "completed tooling contribution; no new kappa", + "summary": "Exact integer exponential kernel with full receipt equality; no claimed substantial full-check speedup. Focused correctness and rejection tests pass on Python3.13/3.14. See README and evidence for measured timings.", + "link": "https://github.com/steph4n-gh/integer-mult-bounds/tree/codex/exact-exp-interval-performance/research/exact-exp-performance", + "scope": "Same 16-term Taylor polynomial, tail and 200-bit rounding; unchanged frozen verifier executed on archived native fixtures." + } +} diff --git a/research/exact-exp-performance/NOTICE.md b/research/exact-exp-performance/NOTICE.md new file mode 100644 index 0000000000..898b6817e2 --- /dev/null +++ b/research/exact-exp-performance/NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and license + +Prepared for Stephan Arrington (`steph4n-gh`) with substantial OpenAI Codex +assistance in implementation, mathematical derivation, tests and review. +New files are under the repository's Apache-2.0 license. + +The pinned `exact_intervals.py` and `check_owner_map.py` are from Chafik +Boukhalfa/chafreaky's PR626 independent owner-map checking work, prepared with +OpenAI Codex. The native suppliers and dispatch come from Jeremy Kothe's +PR622/623 and their Claude-assisted construction. The PR622 fixture is the +maintainer's archived fresh replay. No frozen source is copied or edited here. + +The underlying lineage includes DreamingOfClouds' cold-helper construction, +Rohan Arun's PR559 recurrence correction, eumemic's bit supplier, icekylinx's +direct-delivery work and GamingPuzzled's owner-headroom lead. Their source +notices, licenses and substantial-assistance disclosures remain in +`research/complex-k492-owner-repair/NOTICE.md` and its dependencies. This notice +does not replace them or claim their constructions as new work. + +Related pending tooling contributions PR667 (logarithm arithmetic), PR662 +(Clifford state evaluation), PR367 (exact frame algebra) and PR452 (native +replay) are acknowledged; their code is not imported and they are not +dependencies. Integer Horner evaluation is standard algebra, not a claimed +novel mathematical technique. diff --git a/research/exact-exp-performance/README.md b/research/exact-exp-performance/README.md new file mode 100644 index 0000000000..4acd81b44e --- /dev/null +++ b/research/exact-exp-performance/README.md @@ -0,0 +1,174 @@ +# Exact exponential intervals with integer arithmetic + +**Tooling improvement and bounded end-to-end performance result; no new κ.** + +This opt-in kernel evaluates the independent PR626 owner checker's exponential +intervals with integer arithmetic. It returns exactly the same two rational +bounds as the pinned reference: the same degree-16 Taylor polynomial, geometric +remainder bound, and 200-bit outward rounding. It changes neither precision nor +the moment admission threshold. + +On the actual 18 exponential argument pairs used by the archived owner check, +15 alternating pairs per interpreter on macOS arm64 measured approximately +**13× faster arithmetic**. Each kernel batch repeats those 18 pairs 50 times. + +| Local interpreter | Kernel reference → integer | Ratio | Complete owner check reference → integer | Ratio | +| --- | ---: | ---: | ---: | ---: | +| CPython 3.14.4 | 0.62026 s → 0.04810 s | 12.90× | 0.38281 s → 0.37411 s | 1.023× | +| CPython 3.13.5 | 0.63399 s → 0.04867 s | 13.03× | 0.41303 s → 0.40023 s | 1.032× | + +**The complete-check improvement is small (about 2–3% less wall time).** An +initial Python 3.14 run showed only 0.5% improvement. The checker also reads and +validates native programs and 35,424 owner roles. The arithmetic gain should +not be presented as a frontier-replay speedup or a substantial complete-check +acceleration. + +Raw per-pair timings, environments, input/output fingerprints, implementation +hashes and receipt hashes are in [the Python 3.14 evidence](evidence/benchmark-python314.json) +and [Python 3.13 evidence](evidence/benchmark-python313.json). Earlier exploratory +runs are retained as `evidence/initial-benchmark-*.json`; they predate the addition +of implementation hashes to the reporting code. They are not discarded because +of their less favorable timings. Timings are machine-specific, include normal +OS caching, and have no pass/fail threshold. The final two interpreter runs were +sequential. Every complete-check receipt is byte-identical to the pinned baseline. + +## Reproduce + +From the repository root, with Python 3.11+ and the standard library only: + +```sh +python3 -B -m unittest discover -s research/exact-exp-performance -p 'test_*.py' -v +``` + +Expected result: **11 tests pass**, including exact kernel comparisons and the +complete independent owner checker with negative controls. This does not run +supplier construction or the full selected frontier suite. + +To repeat the timing experiment (use a fresh output filename): + +```sh +python3 -B research/exact-exp-performance/benchmark.py --pairs 15 --out /tmp/exact-exp-benchmark.json +``` + +Expected marker: `PASS_EXACT_EXP_BENCHMARK`; timing ratios may differ. +Both engines receive identical input pairs. Pair order alternates. The complete +check runs in a fresh process for each engine, including source admission, +imports, JSON decoding, all existing owner checks and output writing. Entire +receipts are compared after each pair, in addition to each engine's baseline +receipt pin. Kernel timing excludes logarithm construction and input preparation; +the complete-check timing includes them. + +For a single opt-in replay: + +```sh +python3 -B research/exact-exp-performance/run.py --engine integer --out /tmp/exact-exp-owner.json +``` + +Expected marker: `PASS independent map and exact moments`. The complete report +SHA-256 is `ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092`. +`--engine reference` executes the unchanged reference. Existing output paths and +paths inside the repository are refused. Run from a full checkout: the archived +fixtures are already committed and no network access is needed. + +## Why the bounds are identical + +For a reduced `Fraction` x = p/q with q > 0, let + +``` +c_j = 16! / j! +N = sum(c_j * p^j * q^(16-j), j=0..16) +d = 16! * q^16. +``` + +Thus N/d is exactly P₁₆(x) = Σ xʲ/j!. The reference forms the same polynomial +by rational term multiplication and addition. The candidate starts N=1 and +Q=1, then for j=15,…,0 sets Q←qQ and N←pN+c_jQ. After processing j, + +``` +N = sum(c_k * p^(k-j) * q^(16-k), k=j..16), Q = q^(16-j). +``` + +This invariant follows directly by multiplication by p and adding the k=j +term. At j=0 it gives the numerator and denominator above without intermediate +fraction normalization. + +The reference's upper remainder is + +``` +R(x) = x^17 / (17! * (1 - x/18)). +``` + +For 0≤x<1, all Taylor terms are nonnegative and the ratios after the first +omitted term are at most x/18, so the geometric bound covers the entire tail. +With the same N,d and t = 17(18q-p)>0, + +``` +P₁₆(x) + R(x) = (N*t + 18*p^17) / (d*t). +``` + +The candidate therefore returns floor(2²⁰⁰P₁₆(a))/2²⁰⁰ and +ceil(2²⁰⁰(P₁₆(b)+R(b)))/2²⁰⁰ by integer division. These are exactly the +reference's `down` and `up`, including grid boundaries and zero. Python integers +are unbounded; there is no floating-point arithmetic or input-dependent cache. + +Supported inputs are `Fraction` endpoints satisfying 0≤a≤b<1, exactly the +actual owner-checker calls. Other types are rejected explicitly. This does not +promise compatibility with accidental behavior on floats or other numeric types. +Invalid intervals raise `ValueError`; checks remain active under optimized Python. + +## Validation scope + +The kernel tests compare all **276 boundary pairs** and **480 seed-91 rational +pairs**, with denominator sizes through 1024 bits, to the source-pinned reference. +A separate direct-power/factorial implementation checks the arithmetic, and a +degree-64 enclosure supplies exact witnesses for rounding and tail controls. +Five negative mechanisms are detected: an omitted polynomial term, an omitted +tail, an incorrect tail ratio, and inward rounding at either endpoint. These +finite checks corroborate the algebraic argument; they are not a formal proof +of the multiplication theorem. + +The replay test executes **32 subprocess controls** covering both engines: +normal and optimized-Python positives, existing-output protection, repository +output refusal, changed and missing pinned sources, and a wrong receipt digest. +Mathematical mutations exercise both moment thresholds, owner width/family/call/ +footprint checks, call chronology, native hashes and orientation counts. For +these mutations only, the test bypasses adapter source admission and recomputes +the relevant input pins in a temporary copy, so rejection comes from the actual +checker obligation. It requires the specific expected error, not just any crash. +These controls pass on local Python 3.14.4 and Python 3.13.5 (the latter suite +also under `-O`); each suite runs the checker with and without optimization. +The dedicated Linux workflow is separate from these recorded local results. + +`SOURCE.json` pins the exact base, reference helper, full checker, six package +inputs and four archived native artifacts. `run.py` executes the unchanged +checker via `runpy` and narrowly intercepts its import of `exact_intervals.py`: +the original module is loaded first, then only `exp` is replaced. The original +logarithm, source checks, geometry, both program orientations, owner capacities, +disjointness, compaction, rank mass, exact moments and outer conversion all run. +The import hook is restored afterward and must apply exactly once. + +The archived native words are reused from the maintainer's PR622 replay; the +owner map is PR626. **No fresh supplier construction, controller replay, +47-inequality assembly, Lean build or full `make verify` is claimed.** All-size +compilation, common-label/mutable-basis realization, pooled hosting, +precision/tape/recovery and analytic assumptions remain inherited. Frozen +packages, `upstream/`, default commands and the selected result are unchanged. + +## Provenance and overlap + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. OS-random assignment seed: **91**. +The local claim and three considered tasks are recorded in `CLAIM.json`. No +pinned sprint coordination issue existed at the initial check. + +Chafik Boukhalfa's PR626 supplies the independent checker; Jeremy Kothe's +PR622/623 supplies the native construction and inherited dispatch. The archive +comes from the maintainer's review. See [NOTICE.md](NOTICE.md) and the retained +[construction notice](../complex-k492-owner-repair/NOTICE.md) for the cumulative +contributor and AI-assistance record. + +Pending PR667 optimizes logarithms in a different moment engine; it is related +work, not a dependency or a source of this implementation. PR662 addresses +Clifford states; PR367 and PR452 address frame algebra and native replay. +This submission changes only exponential interval evaluation and preserves its +negative end-to-end performance result. It makes no priority claim for integer +Horner evaluation. diff --git a/research/exact-exp-performance/SOURCE.json b/research/exact-exp-performance/SOURCE.json new file mode 100644 index 0000000000..0a6a190c1e --- /dev/null +++ b/research/exact-exp-performance/SOURCE.json @@ -0,0 +1,20 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "reviewed_provider_head": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "reviewed_owner_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "owner_receipt_sha256": "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "files": { + "research/complex-k492-owner-repair/extras/check_owner_map.py": "d240458ad39a08c242d136c0f1edbda0cb0b93977897f6543c9f430576c9c7dd", + "research/complex-k492-owner-repair/extras/exact_intervals.py": "aa3c2327c5d3742248b720a87b2de0bbe2e34ed2af89a578e3c8d5bd2656a9cf", + "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323", + "research/complex-k492-owner-repair/data/PLAN.json": "8c48ef6ce079916314126c5c3ff0003b32f24cf0fbfb2a033fc93e1e1949b5d5", + "research/complex-k492-owner-repair/data/OWNERS.json.gz": "251e82cec1f40e6c1289703667f403104b957f1254dc4f6baa6df9a3d0c751de", + "research/complex-k492-owner-repair/comparison/PR623-SPEC.json": "436d3df54e6ce2433d56435afd569708e5fb22bc638571f5134ab12a9f9099f5", + "research/complex-k492-owner-repair/comparison/PR623-PLAN.json": "c919c366ef1d3528f1884e47dfce858ab3164b099740e4c17cde6f697b3ec458", + "research/complex-k492-owner-repair/comparison/PR622-NATIVE-HASHES.json": "28479a183387bcb608bd9ee0572f617c17f316b79ce4a6fa1277ed8689fb3431", + "research/community-k492-audit/pr622/replay/ck-local/CANONICAL-WORD.json.gz": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45", + "research/community-k492-audit/pr622/replay/ck-local/LOCAL-PROGRAMS.json.gz": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3", + "research/community-k492-audit/pr622/replay/jp8-local/CANONICAL-WORD.json.gz": "7a3fec1022d3b2b1bd986302a327735ec521d17b043f4a5acb96253a56f6193c", + "research/community-k492-audit/pr622/replay/jp8-local/LOCAL-PROGRAMS.json.gz": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98" + } +} diff --git a/research/exact-exp-performance/benchmark.py b/research/exact-exp-performance/benchmark.py new file mode 100644 index 0000000000..41a649dfd7 --- /dev/null +++ b/research/exact-exp-performance/benchmark.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Alternating same-input kernel and fresh-process complete owner-check timings.""" +import argparse +from fractions import Fraction +import hashlib +import importlib.util +import json +import platform +import statistics +import subprocess +import sys +import tempfile +from time import perf_counter +from pathlib import Path + +import fast_exp +from run import HERE, PACKAGE, REFERENCE, check_sources + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True).encode()).hexdigest() + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--pairs', type=int, default=15) + parser.add_argument('--repeats', type=int, default=50, + help='repetitions of the 18-call native exponential batch') + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + if args.pairs < 3 or args.repeats < 1 or args.out.exists(): + parser.error('Use at least 3 pairs, positive repeats, and a fresh output file') + check_sources() + spec = importlib.util.spec_from_file_location('reference', REFERENCE) + reference = importlib.util.module_from_spec(spec) + spec.loader.exec_module(reference) + selected = json.loads((PACKAGE / 'data/SPEC.json').read_text()) + previous = json.loads((PACKAGE / 'comparison/PR623-SPEC.json').read_text()) + profile = selected['expected']['global_profile'] + endpoints = [Fraction(s['expected']['complex_lower']) for s in (previous, selected)] + inputs = [] + for endpoint in endpoints: + for width in sorted(map(int, profile)): + low, high = reference.log(Fraction(73, width)) + inputs.append((endpoint * low, endpoint * high)) + expected = [reference.exp(*ab) for ab in inputs] + if [fast_exp.exp(*ab) for ab in inputs] != expected: + raise ValueError('Native exponential bounds differ') + kernels = {'reference': reference.exp, 'integer': fast_exp.exp} + kernel_times = {name: [] for name in kernels} + replay_times = {name: [] for name in kernels} + receipt_hashes = [] + with tempfile.TemporaryDirectory(prefix='exact-exp-benchmark-') as temp: + for pair in range(args.pairs): + order = ('reference', 'integer') if pair % 2 == 0 else ('integer', 'reference') + for name in order: + fn = kernels[name] + start = perf_counter() + for _ in range(args.repeats): + result = [fn(*ab) for ab in inputs] + kernel_times[name].append(perf_counter() - start) + if result != expected: + raise ValueError('Timed kernel bounds differ') + outputs = [] + for name in order: + out = Path(temp) / f'{pair}-{name}.json' + start = perf_counter() + subprocess.run([sys.executable, '-B', str(HERE / 'run.py'), + '--engine', name, '--out', str(out)], + check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + replay_times[name].append(perf_counter() - start) + outputs.append(out.read_bytes()) + if outputs[0] != outputs[1]: + raise ValueError('Complete owner-check receipts differ') + receipt_hashes.append(hashlib.sha256(outputs[0]).hexdigest()) + + def stats(times): + medians = {name: statistics.median(values) for name, values in times.items()} + return {'seconds': times, 'median_seconds': medians, + 'ratio_of_medians': medians['reference'] / medians['integer']} + + report = { + 'status': 'PASS_EXACT_EXP_BENCHMARK', + 'scope': 'Exact exponential kernel and archived-input independent owner check; no supplier rebuild or full frontier timing.', + 'environment': {'python': sys.version, 'platform': platform.platform(), + 'machine': platform.machine()}, + 'source_manifest_sha256': hashlib.sha256((HERE / 'SOURCE.json').read_bytes()).hexdigest(), + 'implementation_sha256': {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in ('fast_exp.py', 'run.py', 'benchmark.py')}, + 'pairs': args.pairs, 'order': 'reference-first for even pairs, integer-first for odd pairs', + 'native_batch_size': len(inputs), 'kernel_batch_repeats': args.repeats, + 'inputs_sha256': digest([[str(a), str(b)] for a, b in inputs]), + 'exact_output_sha256': digest([[str(a), str(b)] for a, b in expected]), + 'kernel': stats(kernel_times), 'complete_owner_check': stats(replay_times), + 'owner_receipt_sha256_each_pair': receipt_hashes, + } + with args.out.open('x') as stream: + json.dump(report, stream, indent=2) + stream.write('\n') + print(report['status']) + for name in ('kernel', 'complete_owner_check'): + print(name, report[name]['median_seconds'], 'ratio', report[name]['ratio_of_medians']) + + +if __name__ == '__main__': + main() diff --git a/research/exact-exp-performance/evidence/benchmark-python313.json b/research/exact-exp-performance/evidence/benchmark-python313.json new file mode 100644 index 0000000000..32cfba4b93 --- /dev/null +++ b/research/exact-exp-performance/evidence/benchmark-python313.json @@ -0,0 +1,124 @@ +{ + "status": "PASS_EXACT_EXP_BENCHMARK", + "scope": "Exact exponential kernel and archived-input independent owner check; no supplier rebuild or full frontier timing.", + "environment": { + "python": "3.13.5 (main, Jun 11 2025, 15:36:57) [Clang 17.0.0 (clang-1700.0.13.3)]", + "platform": "macOS-27.0-arm64-arm-64bit-Mach-O", + "machine": "arm64" + }, + "source_manifest_sha256": "b494c4bb2018d93d403f2bfb00e35170e95ad509b551f5c9ce0a9ba20ded73fe", + "implementation_sha256": { + "fast_exp.py": "7fa9bb3f42fd7e54b45249148bd5a8e33552dbacd7f0fc990ce64cda0f8bb983", + "run.py": "ac6c2f8c646cccf3ff1f093ece3f36d81b39804d8e4618061dc5c4b01a522314", + "benchmark.py": "fa7249601ccf8ad002fa625389ce5295b8b68ff6a17701779404e12195808564" + }, + "pairs": 15, + "order": "reference-first for even pairs, integer-first for odd pairs", + "native_batch_size": 18, + "kernel_batch_repeats": 50, + "inputs_sha256": "058a0f61a975744ed38a50a36e536226cd084c1ee8091a3a439e6a89088bf9f5", + "exact_output_sha256": "30da533372965142cbfe1d0fec7ff1dbccf71630ec33413d7f4448792fc2d28c", + "kernel": { + "seconds": { + "reference": [ + 0.6261990829370916, + 0.6267952090129256, + 0.6307432497851551, + 0.6326785841956735, + 0.6295592081733048, + 0.6449042498134077, + 0.6740677091293037, + 0.6275382079184055, + 0.6315525830723345, + 0.6394032500684261, + 0.6365269999951124, + 0.6339916666038334, + 0.6349055417813361, + 0.6353879580274224, + 0.6460819588974118 + ], + "integer": [ + 0.04874983290210366, + 0.04801883269101381, + 0.048724791035056114, + 0.04838970908895135, + 0.04813562473282218, + 0.04907912481576204, + 0.048614250030368567, + 0.04806662490591407, + 0.048683874774724245, + 0.048673707991838455, + 0.048180708196014166, + 0.04862691694870591, + 0.04889683285728097, + 0.04910391615703702, + 0.04877858282998204 + ] + }, + "median_seconds": { + "reference": 0.6339916666038334, + "integer": 0.048673707991838455 + }, + "ratio_of_medians": 13.025341457653902 + }, + "complete_owner_check": { + "seconds": { + "reference": [ + 0.3933421247638762, + 0.40828479221090674, + 0.41123987501487136, + 0.415370334405452, + 0.46323675010353327, + 0.4174872078001499, + 0.4118826249614358, + 0.41302870819345117, + 0.39167175022885203, + 0.40264029102399945, + 0.4170317919924855, + 0.43176070787012577, + 0.4426597082056105, + 0.4270590841770172, + 0.41096491692587733 + ], + "integer": [ + 0.37978158285841346, + 0.39157508267089725, + 0.39652250008657575, + 0.3993824156932533, + 0.48932295897975564, + 0.4002309590578079, + 0.40088229067623615, + 0.38860604213550687, + 0.3824490839615464, + 0.38238424994051456, + 0.4098954163491726, + 0.4329877910204232, + 0.4181719161570072, + 0.4218668332323432, + 0.46009312476962805 + ] + }, + "median_seconds": { + "reference": 0.41302870819345117, + "integer": 0.4002309590578079 + }, + "ratio_of_medians": 1.031975910023979 + }, + "owner_receipt_sha256_each_pair": [ + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092" + ] +} diff --git a/research/exact-exp-performance/evidence/benchmark-python314.json b/research/exact-exp-performance/evidence/benchmark-python314.json new file mode 100644 index 0000000000..8248f0823f --- /dev/null +++ b/research/exact-exp-performance/evidence/benchmark-python314.json @@ -0,0 +1,124 @@ +{ + "status": "PASS_EXACT_EXP_BENCHMARK", + "scope": "Exact exponential kernel and archived-input independent owner check; no supplier rebuild or full frontier timing.", + "environment": { + "python": "3.14.4 (main, Apr 7 2026, 13:13:20) [Clang 21.0.0 (clang-2100.0.123.102)]", + "platform": "macOS-27.0-arm64-arm-64bit-Mach-O", + "machine": "arm64" + }, + "source_manifest_sha256": "b494c4bb2018d93d403f2bfb00e35170e95ad509b551f5c9ce0a9ba20ded73fe", + "implementation_sha256": { + "fast_exp.py": "7fa9bb3f42fd7e54b45249148bd5a8e33552dbacd7f0fc990ce64cda0f8bb983", + "run.py": "ac6c2f8c646cccf3ff1f093ece3f36d81b39804d8e4618061dc5c4b01a522314", + "benchmark.py": "fa7249601ccf8ad002fa625389ce5295b8b68ff6a17701779404e12195808564" + }, + "pairs": 15, + "order": "reference-first for even pairs, integer-first for odd pairs", + "native_batch_size": 18, + "kernel_batch_repeats": 50, + "inputs_sha256": "058a0f61a975744ed38a50a36e536226cd084c1ee8091a3a439e6a89088bf9f5", + "exact_output_sha256": "30da533372965142cbfe1d0fec7ff1dbccf71630ec33413d7f4448792fc2d28c", + "kernel": { + "seconds": { + "reference": [ + 0.6137787909246981, + 0.613791124895215, + 0.6306102089583874, + 0.6253988337703049, + 0.6192872091196477, + 0.6196418749168515, + 0.6145920832641423, + 0.618783500045538, + 0.6157597922720015, + 0.6222482500597835, + 0.6208359999582171, + 0.6202599173411727, + 0.6274084588512778, + 0.6230338751338422, + 0.629992582835257 + ], + "integer": [ + 0.04763841675594449, + 0.0480960002169013, + 0.04832941573113203, + 0.047628083266317844, + 0.048143708147108555, + 0.04858329193666577, + 0.04791979119181633, + 0.047701832838356495, + 0.047126749996095896, + 0.04775958368554711, + 0.04862099979072809, + 0.0480678747408092, + 0.04870887519791722, + 0.049970833119004965, + 0.0483885002322495 + ] + }, + "median_seconds": { + "reference": 0.6202599173411727, + "integer": 0.0480960002169013 + }, + "ratio_of_medians": 12.896288975048877 + }, + "complete_owner_check": { + "seconds": { + "reference": [ + 0.3841769169084728, + 0.3571634995751083, + 0.38025933410972357, + 0.38422704208642244, + 0.3785141250118613, + 0.38771516690030694, + 0.39242787519469857, + 0.38281383318826556, + 0.3621501252055168, + 0.3659708332270384, + 0.38178899977356195, + 0.3926674169488251, + 0.37142925010994077, + 0.38529091607779264, + 0.3852257081307471 + ], + "integer": [ + 0.38487099995836616, + 0.40502704167738557, + 0.40185608295723796, + 0.38312325021252036, + 0.35080416686832905, + 0.37640145793557167, + 0.37240083422511816, + 0.3741065412759781, + 0.33369566639885306, + 0.3669335409067571, + 0.36795095866546035, + 0.37414287496358156, + 0.3502917499281466, + 0.38252100022509694, + 0.36539358273148537 + ] + }, + "median_seconds": { + "reference": 0.38281383318826556, + "integer": 0.3741065412759781 + }, + "ratio_of_medians": 1.0232748988632736 + }, + "owner_receipt_sha256_each_pair": [ + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092" + ] +} diff --git a/research/exact-exp-performance/evidence/initial-benchmark-python313.json b/research/exact-exp-performance/evidence/initial-benchmark-python313.json new file mode 100644 index 0000000000..635e94b92a --- /dev/null +++ b/research/exact-exp-performance/evidence/initial-benchmark-python313.json @@ -0,0 +1,119 @@ +{ + "status": "PASS_EXACT_EXP_BENCHMARK", + "scope": "Exact exponential kernel and archived-input independent owner check; no supplier rebuild or full frontier timing.", + "environment": { + "python": "3.13.5 (main, Jun 11 2025, 15:36:57) [Clang 17.0.0 (clang-1700.0.13.3)]", + "platform": "macOS-27.0-arm64-arm-64bit-Mach-O", + "machine": "arm64" + }, + "source_manifest_sha256": "b494c4bb2018d93d403f2bfb00e35170e95ad509b551f5c9ce0a9ba20ded73fe", + "pairs": 15, + "order": "reference-first for even pairs, integer-first for odd pairs", + "native_batch_size": 18, + "kernel_batch_repeats": 50, + "inputs_sha256": "058a0f61a975744ed38a50a36e536226cd084c1ee8091a3a439e6a89088bf9f5", + "exact_output_sha256": "30da533372965142cbfe1d0fec7ff1dbccf71630ec33413d7f4448792fc2d28c", + "kernel": { + "seconds": { + "reference": [ + 0.606672374997288, + 0.6074720825999975, + 0.6049682502634823, + 0.5989783341065049, + 0.6110455831512809, + 0.6094845002517104, + 0.6109257498756051, + 0.6103269159793854, + 0.5989611661061645, + 0.6118009579367936, + 0.6121225417591631, + 0.5998510415665805, + 0.6140748332254589, + 0.6200351673178375, + 0.626863416749984 + ], + "integer": [ + 0.047804083209484816, + 0.04657583311200142, + 0.046107999980449677, + 0.04579250002279878, + 0.047123834025114775, + 0.04623241722583771, + 0.0470877499319613, + 0.046143459156155586, + 0.046662500128149986, + 0.046104374807327986, + 0.04771950002759695, + 0.04685879126191139, + 0.04774837475270033, + 0.046659333165735006, + 0.04680058406665921 + ] + }, + "median_seconds": { + "reference": 0.6103269159793854, + "integer": 0.046662500128149986 + }, + "ratio_of_medians": 13.07960169950677 + }, + "complete_owner_check": { + "seconds": { + "reference": [ + 0.41760158305987716, + 0.39585937513038516, + 0.4055372909642756, + 0.41440558386966586, + 0.42082241689786315, + 0.41979933297261596, + 0.40510941576212645, + 0.39060558285564184, + 0.414130125194788, + 0.41337916580960155, + 0.40478979190811515, + 0.40916716726496816, + 0.4436621661297977, + 0.4166890410706401, + 0.392968500033021 + ], + "integer": [ + 0.3827620828524232, + 0.3578190840780735, + 0.33855366706848145, + 0.41614808328449726, + 0.4138476671651006, + 0.37416520807892084, + 0.428485875017941, + 0.4049978330731392, + 0.3994293753057718, + 0.4240069161169231, + 0.3392647919245064, + 0.3756780424155295, + 0.42288949992507696, + 0.42371983267366886, + 0.37888424983248115 + ] + }, + "median_seconds": { + "reference": 0.41337916580960155, + "integer": 0.3994293753057718 + }, + "ratio_of_medians": 1.0349242979266382 + }, + "owner_receipt_sha256_each_pair": [ + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092" + ] +} diff --git a/research/exact-exp-performance/evidence/initial-benchmark-python314.json b/research/exact-exp-performance/evidence/initial-benchmark-python314.json new file mode 100644 index 0000000000..fc31cf9208 --- /dev/null +++ b/research/exact-exp-performance/evidence/initial-benchmark-python314.json @@ -0,0 +1,119 @@ +{ + "status": "PASS_EXACT_EXP_BENCHMARK", + "scope": "Exact exponential kernel and archived-input independent owner check; no supplier rebuild or full frontier timing.", + "environment": { + "python": "3.14.4 (main, Apr 7 2026, 13:13:20) [Clang 21.0.0 (clang-2100.0.123.102)]", + "platform": "macOS-27.0-arm64-arm-64bit-Mach-O", + "machine": "arm64" + }, + "source_manifest_sha256": "b494c4bb2018d93d403f2bfb00e35170e95ad509b551f5c9ce0a9ba20ded73fe", + "pairs": 15, + "order": "reference-first for even pairs, integer-first for odd pairs", + "native_batch_size": 18, + "kernel_batch_repeats": 50, + "inputs_sha256": "058a0f61a975744ed38a50a36e536226cd084c1ee8091a3a439e6a89088bf9f5", + "exact_output_sha256": "30da533372965142cbfe1d0fec7ff1dbccf71630ec33413d7f4448792fc2d28c", + "kernel": { + "seconds": { + "reference": [ + 0.6138253747485578, + 0.6245250841602683, + 0.6526142503134906, + 0.615237332880497, + 0.6119221253320575, + 0.6350596663542092, + 0.6145592918619514, + 0.644073833245784, + 0.6277244579978287, + 0.6084865420125425, + 0.6234460831619799, + 0.622539333999157, + 0.6237291246652603, + 0.6218038750812411, + 0.6237267921678722 + ], + "integer": [ + 0.047090125270187855, + 0.04824233427643776, + 0.04787504067644477, + 0.04749687481671572, + 0.047836166340857744, + 0.04886154178529978, + 0.04852283280342817, + 0.04862929182127118, + 0.048248833045363426, + 0.04745941702276468, + 0.04868825012817979, + 0.04736954206600785, + 0.04802754195407033, + 0.0478683328256011, + 0.04860812518745661 + ] + }, + "median_seconds": { + "reference": 0.6234460831619799, + "integer": 0.04802754195407033 + }, + "ratio_of_medians": 12.981011681967683 + }, + "complete_owner_check": { + "seconds": { + "reference": [ + 0.4142444576136768, + 0.3943261248059571, + 0.37281033396720886, + 0.39044558303430676, + 0.3780746250413358, + 0.3774481671862304, + 0.40338174998760223, + 0.4136562077328563, + 0.38366108294576406, + 0.3608795003965497, + 0.35224362509325147, + 0.3856989583000541, + 0.4091540826484561, + 0.39799312502145767, + 0.37490849988535047 + ], + "integer": [ + 0.3956982088275254, + 0.36995579209178686, + 0.358068541623652, + 0.39499470917508006, + 0.38706841692328453, + 0.3491929592564702, + 0.36535329231992364, + 0.40702395886182785, + 0.3838283750228584, + 0.3941767090000212, + 0.3606880414299667, + 0.42702499963343143, + 0.3701369590125978, + 0.377616083715111, + 0.3983702501282096 + ] + }, + "median_seconds": { + "reference": 0.3856989583000541, + "integer": 0.3838283750228584 + }, + "ratio_of_medians": 1.0048734887749877 + }, + "owner_receipt_sha256_each_pair": [ + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092", + "ec82a647bc3567efef91a1588c86f012cdbb5decac0c25a9f38ba5d11762a092" + ] +} diff --git a/research/exact-exp-performance/evidence/tests-python313-optimized.txt b/research/exact-exp-performance/evidence/tests-python313-optimized.txt new file mode 100644 index 0000000000..3e2fd2bcd9 --- /dev/null +++ b/research/exact-exp-performance/evidence/tests-python313-optimized.txt @@ -0,0 +1,17 @@ +test_exact_rounding_obligations (test_exp.ExactExpTests.test_exact_rounding_obligations) ... ok +test_higher_order_certified_enclosures (test_exp.ExactExpTests.test_higher_order_certified_enclosures) ... ok +test_independent_direct_power_oracle (test_exp.ExactExpTests.test_independent_direct_power_oracle) ... ok +test_input_contract (test_exp.ExactExpTests.test_input_contract) ... ok +test_invalid_domains_rejected (test_exp.ExactExpTests.test_invalid_domains_rejected) ... ok +test_negative_control_omitted_polynomial_term (test_exp.ExactExpTests.test_negative_control_omitted_polynomial_term) ... ok +test_negative_controls_inward_rounding (test_exp.ExactExpTests.test_negative_controls_inward_rounding) ... ok +test_negative_controls_tail (test_exp.ExactExpTests.test_negative_controls_tail) ... ok +test_reference_pin_and_boundary_differential (test_exp.ExactExpTests.test_reference_pin_and_boundary_differential) ... ok +test_seeded_rational_differential (test_exp.ExactExpTests.test_seeded_rational_differential) ... ok +test_full_replay (test_replay.ReplayTests.test_full_replay) ... ok + +---------------------------------------------------------------------- +Ran 11 tests in 14.410s + +OK +PASS 32 whole-check subprocess controls; exact receipt equality, both engines, and -O (13.683s) diff --git a/research/exact-exp-performance/evidence/tests-python314.txt b/research/exact-exp-performance/evidence/tests-python314.txt new file mode 100644 index 0000000000..fd88eab1e1 --- /dev/null +++ b/research/exact-exp-performance/evidence/tests-python314.txt @@ -0,0 +1,17 @@ +test_exact_rounding_obligations (test_exp.ExactExpTests.test_exact_rounding_obligations) ... ok +test_higher_order_certified_enclosures (test_exp.ExactExpTests.test_higher_order_certified_enclosures) ... ok +test_independent_direct_power_oracle (test_exp.ExactExpTests.test_independent_direct_power_oracle) ... ok +test_input_contract (test_exp.ExactExpTests.test_input_contract) ... ok +test_invalid_domains_rejected (test_exp.ExactExpTests.test_invalid_domains_rejected) ... ok +test_negative_control_omitted_polynomial_term (test_exp.ExactExpTests.test_negative_control_omitted_polynomial_term) ... ok +test_negative_controls_inward_rounding (test_exp.ExactExpTests.test_negative_controls_inward_rounding) ... ok +test_negative_controls_tail (test_exp.ExactExpTests.test_negative_controls_tail) ... ok +test_reference_pin_and_boundary_differential (test_exp.ExactExpTests.test_reference_pin_and_boundary_differential) ... ok +test_seeded_rational_differential (test_exp.ExactExpTests.test_seeded_rational_differential) ... ok +test_full_replay (test_replay.ReplayTests.test_full_replay) ... ok + +---------------------------------------------------------------------- +Ran 11 tests in 11.829s + +OK +PASS 32 whole-check subprocess controls; exact receipt equality, both engines, and -O (11.098s) diff --git a/research/exact-exp-performance/fast_exp.py b/research/exact-exp-performance/fast_exp.py new file mode 100644 index 0000000000..cda3e123f9 --- /dev/null +++ b/research/exact-exp-performance/fast_exp.py @@ -0,0 +1,40 @@ +"""Exact replacement for the pinned independent checker exponential enclosure. + +Same Taylor polynomial, geometric tail and 200-bit outward rounding. Only +integer arithmetic is used before constructing the two returned Fractions. +Stephan Arrington, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from math import factorial + +D = 1 << 200 +FACTORIAL_16 = factorial(16) +COEFFICIENTS = tuple(FACTORIAL_16 // factorial(j) for j in range(17)) + + +def _polynomial(x): + """Return unreduced N, d with N/d = sum(x**j/j! for j in 0..16).""" + p, q = x.numerator, x.denominator + numerator = 1 + q_power = 1 + for coefficient in reversed(COEFFICIENTS[:-1]): + q_power *= q + numerator = numerator * p + coefficient * q_power + return numerator, FACTORIAL_16 * q_power + + +def exp(a, b): + """Return exactly the reference bounds for exact 0 <= a <= b < 1.""" + if not isinstance(a, Fraction) or not isinstance(b, Fraction): + raise TypeError('Fraction endpoints required') + if not 0 <= a <= b < 1: + raise ValueError('positive small exponent') + low_n, low_d = _polynomial(a) + high_n, high_d = _polynomial(b) + p, q = b.numerator, b.denominator + tail_factor = 17 * (18 * q - p) + high_n = high_n * tail_factor + 18 * p ** 17 + high_d *= tail_factor + low = (D * low_n) // low_d + high = -((-D * high_n) // high_d) + return Fraction(low, D), Fraction(high, D) diff --git a/research/exact-exp-performance/run.py b/research/exact-exp-performance/run.py new file mode 100644 index 0000000000..ed8779c88c --- /dev/null +++ b/research/exact-exp-performance/run.py @@ -0,0 +1,75 @@ +#!/usr/bin/env python3 +"""Replay the pinned complete owner check, optionally replacing only E.exp.""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path +import runpy +import sys + +from fast_exp import exp + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = ROOT / 'research/complex-k492-owner-repair' +REFERENCE = PACKAGE / 'extras/exact_intervals.py' +FIXTURE = ROOT / 'research/community-k492-audit/pr622/replay' + + +def check_sources(): + manifest = json.loads((HERE / 'SOURCE.json').read_text()) + for name, expected in manifest['files'].items(): + actual = hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + if actual != expected: + raise ValueError('Pinned input changed: ' + name) + + +def replay(engine, out): + check_sources() + out = out.resolve() + if out.exists() or out.is_relative_to(ROOT): + raise ValueError('Use a fresh output path outside the repository') + original_spec = importlib.util.spec_from_file_location + original_argv = sys.argv + replacements = [] + + def spec_with_exp(name, location, *args, **kwargs): + spec = original_spec(name, location, *args, **kwargs) + if Path(location).resolve() == REFERENCE: + original_exec = spec.loader.exec_module + + def exec_with_exp(module): + original_exec(module) + module.exp = exp + replacements.append(str(location)) + + spec.loader.exec_module = exec_with_exp + return spec + + try: + if engine == 'integer': + importlib.util.spec_from_file_location = spec_with_exp + sys.argv = [str(PACKAGE / 'extras/check_owner_map.py'), + '--work', str(FIXTURE), '--out', str(out)] + runpy.run_path(sys.argv[0], run_name='__main__') + finally: + importlib.util.spec_from_file_location = original_spec + sys.argv = original_argv + if len(replacements) != (1 if engine == 'integer' else 0): + raise ValueError('Exponential replacement was not applied exactly once') + expected = json.loads((HERE / 'SOURCE.json').read_text())['owner_receipt_sha256'] + if hashlib.sha256(out.read_bytes()).hexdigest() != expected: + raise ValueError('Owner receipt differs from pinned reference') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--engine', choices=('reference', 'integer'), required=True) + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + replay(args.engine, args.out) + + +if __name__ == '__main__': + main() diff --git a/research/exact-exp-performance/test_exp.py b/research/exact-exp-performance/test_exp.py new file mode 100644 index 0000000000..3a40690ea2 --- /dev/null +++ b/research/exact-exp-performance/test_exp.py @@ -0,0 +1,212 @@ +#!/usr/bin/env python3 +"""Bounded exact checks for the opt-in exponential interval kernel. + +Run from any directory: python3 research/exact-exp-performance/test_exp.py +Stephan Arrington, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q +from decimal import Decimal +import hashlib +import importlib.util +from math import factorial +from pathlib import Path +import random +import unittest + +from fast_exp import D, exp + + +REFERENCE = ( + Path(__file__).resolve().parents[1] + / "complex-k492-owner-repair/extras/exact_intervals.py" +) +REFERENCE_SHA256 = "aa3c2327c5d3742248b720a87b2de0bbe2e34ed2af89a578e3c8d5bd2656a9cf" +RANDOM_SEED = 91 +RANDOM_CASES = 480 + + +def load_reference(): + actual = hashlib.sha256(REFERENCE.read_bytes()).hexdigest() + if actual != REFERENCE_SHA256: + raise ValueError(f"reference source pin mismatch: {actual}") + spec = importlib.util.spec_from_file_location("pinned_exact_intervals", REFERENCE) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module.exp + + +def polynomial(x, degree=16): + """Independent direct power/factorial sum; no homogeneous evaluation.""" + return sum((x ** j / factorial(j) for j in range(degree + 1)), Q(0)) + + +def remainder(x, degree=16, ratio_denominator=None): + r = degree + 2 if ratio_denominator is None else ratio_denominator + return x ** (degree + 1) / (factorial(degree + 1) * (1 - x / r)) + + +def floor_grid(x): + whole, _ = divmod(x.numerator * D, x.denominator) + return Q(whole, D) + + +def ceil_grid(x): + whole, residual = divmod(x.numerator * D, x.denominator) + return Q(whole + bool(residual), D) + + +def direct_oracle(a, b): + return floor_grid(polynomial(a)), ceil_grid(polynomial(b) + remainder(b)) + + +def random_cases(): + rng = random.Random(RANDOM_SEED) + # Includes denominators far beyond floating point precision and the + # rounding grid, while keeping this regression suite comfortably bounded. + widths = (2, 7, 17, 53, 64, 127, 200, 257, 521, 1024) + for i in range(RANDOM_CASES): + bits = widths[i % len(widths)] + denominator_a = rng.randrange(1 << (bits - 1), 1 << bits) + denominator_b = rng.randrange(1 << (bits - 1), 1 << bits) + a = Q(rng.randrange(denominator_a), denominator_a) + b = Q(rng.randrange(denominator_b), denominator_b) + yield min(a, b), max(a, b) + + +def boundary_cases(): + points = { + Q(0), Q(1, 2), Q(1, 3), Q(2, 3), Q(17, 18), Q(18, 19), + Q(1, D * D), Q(1, D), Q(2, D), Q(D - 1, D), + Q(D * D - 1, D * D), Q(10 ** 100 - 1, 10 ** 100), + Q(1, 10 ** 100), Q((1 << 1024) - 1, 1 << 1024), + } + for denominator in (3, 7, 17, 19, 101, 65537): + points.update((Q(1, denominator), Q(denominator - 1, denominator))) + ordered = sorted(points) + for i, a in enumerate(ordered): + for b in ordered[i:]: + yield a, b + + +class ExactExpTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.reference = staticmethod(load_reference()) + + def assert_exact(self, candidate, cases): + for a, b in cases: + with self.subTest(a=a, b=b): + expected = self.reference(a, b) + self.assertEqual(candidate(a, b), expected) + + def test_reference_pin_and_boundary_differential(self): + self.assertEqual(D, 1 << 200) + self.assert_exact(exp, boundary_cases()) + + def test_seeded_rational_differential(self): + self.assert_exact(exp, random_cases()) + + def test_independent_direct_power_oracle(self): + # This second oracle uses powers and factorials, rather than either + # reference term recurrence or candidate homogeneous integer recurrence. + cases = [(Q(i, 64), Q(j, 64)) for i in range(0, 64, 7) + for j in range(i, 64, 11)] + cases += list(random_cases())[::12] + for a, b in cases: + with self.subTest(a=a, b=b): + self.assertEqual(exp(a, b), direct_oracle(a, b)) + + def test_exact_rounding_obligations(self): + for a, b in list(boundary_cases())[::7]: + low, high = exp(a, b) + unrounded_low = polynomial(a) + unrounded_high = polynomial(b) + remainder(b) + self.assertLessEqual(low, unrounded_low) + self.assertLess(unrounded_low - low, Q(1, D)) + self.assertGreaterEqual(high, unrounded_high) + self.assertLess(high - unrounded_high, Q(1, D)) + self.assertEqual(D % low.denominator, 0) + self.assertEqual(D % high.denominator, 0) + + def test_higher_order_certified_enclosures(self): + # Positive Taylor terms give P_64 <= exp(x); the geometric tail gives + # exp(x) <= P_64 + R_64. The candidate interval encloses both bounds. + points = [Q(i, 64) for i in range(64)] + points += [Q(1, D * D), Q(D * D - 1, D * D)] + previous = None + for x in points: + low, high = exp(x, x) + tighter_low = polynomial(x, 64) + tighter_high = tighter_low + remainder(x, 64) + self.assertLessEqual(low, tighter_low) + self.assertGreaterEqual(high, tighter_high) + self.assertLessEqual(low, high) + # Only the initial sorted grid participates in monotonicity. + if x.denominator <= 64: + if previous is not None: + self.assertLessEqual(previous[0], low) + self.assertLessEqual(previous[1], high) + previous = low, high + + def test_invalid_domains_rejected(self): + invalid = [ + (Q(-1), Q(0)), (Q(-1, D * D), Q(0)), + (Q(0), Q(1)), (Q(1), Q(1)), (Q(0), Q(2)), + (Q(2, 3), Q(1, 3)), (Q(1, D), Q(1, D * D)), + ] + for a, b in invalid: + with self.subTest(a=a, b=b): + with self.assertRaises(ValueError): + exp(a, b) + with self.assertRaises(ValueError): + self.reference(a, b) + + def test_input_contract(self): + self.assertEqual(exp(Q(0), Q(0)), (Q(1), Q(1))) + for a, b in [(0, Q(0)), (Q(0), 0), (False, Q(0)), + (0.0, Q(1, 2)), (Q(0), 0.5), ("0", Q(0)), + (Decimal(0), Q(0)), + (Q(0), None), (complex(0), Q(0))]: + with self.subTest(a=a, b=b): + with self.assertRaises(TypeError): + exp(a, b) + + def test_negative_control_omitted_polynomial_term(self): + x = Q(1, 2) + mutant = floor_grid(polynomial(x, 15)), ceil_grid(polynomial(x) + remainder(x)) + self.assertNotEqual(mutant, self.reference(x, x)) + # The missing term is large enough to remain detectable after rounding. + self.assertGreater(polynomial(x) - polynomial(x, 15), Q(1, D)) + + def test_negative_controls_tail(self): + x = Q(1, 2) + certified_lower = polynomial(x, 64) + correct = self.reference(x, x) + for bad_tail in (Q(0), remainder(x, ratio_denominator=19)): + mutant = floor_grid(polynomial(x)), ceil_grid(polynomial(x) + bad_tail) + self.assertNotEqual(mutant, correct) + # These are genuine under-enclosures of exp(x), witnessed with + # exact rationals rather than a floating point exp implementation. + self.assertLess(mutant[1], certified_lower) + + def test_negative_controls_inward_rounding(self): + x = Q(1, D * D) + unrounded_low = polynomial(x) + unrounded_high = unrounded_low + remainder(x) + certified_lower = polynomial(x, 64) + certified_upper = certified_lower + remainder(x, 64) + correct = self.reference(x, x) + upward_low = ceil_grid(unrounded_low), ceil_grid(unrounded_high) + downward_high = floor_grid(unrounded_low), floor_grid(unrounded_high) + self.assertNotEqual(upward_low, correct) + self.assertNotEqual(downward_high, correct) + self.assertGreater(upward_low[0], certified_upper) + self.assertLess(downward_high[1], certified_lower) + + +if __name__ == "__main__": + print(f"reference sha256: {REFERENCE_SHA256}") + print(f"exact differential cases: {len(list(boundary_cases()))} boundary + " + f"{RANDOM_CASES} random (seed {RANDOM_SEED})") + print("negative controls: omitted term; omitted/wrong tail; inward lower/upper rounding") + unittest.main(verbosity=2) diff --git a/research/exact-exp-performance/test_replay.py b/research/exact-exp-performance/test_replay.py new file mode 100644 index 0000000000..64de76e2d9 --- /dev/null +++ b/research/exact-exp-performance/test_replay.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Bounded whole-check equality and rejection controls for both exp engines. + +Only the twelve pinned inputs and adapter files are copied to a temporary +repository. Mathematical mutation controls deliberately bypass the adapter's +source admission in a child process, so they exercise the unchanged checker. +Normal, source-admission and output controls use the public command directly. +""" +import gzip +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import time +import unittest + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = Path('research/complex-k492-owner-repair') +FIXTURE = Path('research/community-k492-audit/pr622/replay') +ENGINES = ('reference', 'integer') + +# This override exists only in the test process for intentionally changed inputs. +# The checker and the adapter's exp substitution still execute unchanged. +MUTATION_DRIVER = '''\ +from pathlib import Path +import runpy +import sys +sys.path.insert(0, str(Path(sys.argv[1]).parent)) +namespace = runpy.run_path(sys.argv[1]) +namespace['replay'].__globals__['check_sources'] = lambda: None +namespace['replay'](sys.argv[2], Path(sys.argv[3])) +''' + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def dump(path, value): + raw = (json.dumps(value, indent=2) + '\n').encode() + path.write_bytes(gzip.compress(raw, mtime=0) if path.suffix == '.gz' else raw) + + +def run_controls(): + started = time.perf_counter() + source = load(HERE / 'SOURCE.json') + checks = 0 + with tempfile.TemporaryDirectory(prefix='exact-exp-replay-controls-') as name: + temporary = Path(name) + stage = temporary / 'repository' + adapter = stage / 'research/exact-exp-performance/run.py' + output_dir = temporary / 'outputs' + output_dir.mkdir() + + def restore_inputs(): + for relative in source['files']: + target = stage / relative + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / relative, target) + + restore_inputs() + for filename in ('run.py', 'fast_exp.py', 'SOURCE.json'): + adapter.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(HERE / filename, adapter.parent / filename) + + def run(case, engine, *, rejection=None, mutate=False, optimized=True, + output=None): + nonlocal checks + output = output or output_dir / f'{case}-{engine}.json' + command = [sys.executable, '-B'] + if optimized: + command.append('-O') + if mutate: + command += ['-c', MUTATION_DRIVER, str(adapter), engine, str(output)] + else: + command += [str(adapter), '--engine', engine, '--out', str(output)] + result = subprocess.run(command, capture_output=True, text=True, timeout=30) + if rejection is None: + need(result.returncode == 0, f'{case}/{engine}: {result.stderr}') + need('PASS independent map and exact moments' in result.stdout, + f'{case}/{engine}: checker did not finish') + need(hashlib.sha256(output.read_bytes()).hexdigest() + == source['owner_receipt_sha256'], + f'{case}/{engine}: receipt differs from frozen reference') + else: + need(result.returncode != 0 and rejection in result.stderr, + f'{case}/{engine}: expected {rejection!r}, got ' + f'{result.returncode}, {result.stderr!r}') + checks += 1 + return output + + reports = [] + for optimized in (False, True): + for engine in ENGINES: + reports.append(run('positive-O' if optimized else 'positive', engine, + optimized=optimized).read_bytes()) + need(all(report == reports[0] for report in reports), + 'Whole reports differ between engines or under -O') + + reused = output_dir / 'existing.json' + sentinel = b'existing output must survive\n' + reused.write_bytes(sentinel) + for engine in ENGINES: + run('output-reuse', engine, output=reused, + rejection='Use a fresh output path outside the repository') + need(reused.read_bytes() == sentinel, 'Existing output was overwritten') + inside = stage / f'forbidden-{engine}.json' + run('output-in-repository', engine, output=inside, + rejection='Use a fresh output path outside the repository') + need(not inside.exists(), 'Output was written inside the repository') + + spec_path = stage / PACKAGE / 'data/SPEC.json' + spec_path.write_bytes(spec_path.read_bytes() + b'\n') + for engine in ENGINES: + run('source-tamper', engine, rejection='Pinned input changed:') + restore_inputs() + missing = stage / FIXTURE / 'jp8-local/LOCAL-PROGRAMS.json.gz' + missing.unlink() + for engine in ENGINES: + run('source-missing', engine, rejection='FileNotFoundError') + restore_inputs() + + manifest_path = adapter.parent / 'SOURCE.json' + changed_manifest = load(manifest_path) + changed_manifest['owner_receipt_sha256'] = '0' * 64 + dump(manifest_path, changed_manifest) + for engine in ENGINES: + run('receipt-tamper', engine, rejection='Owner receipt differs from pinned reference') + shutil.copyfile(HERE / 'SOURCE.json', manifest_path) + + def reject_mutation(case, reason): + for engine in ENGINES: + output = output_dir / f'{case}-{engine}.json' + run(case, engine, rejection='ValueError: ' + reason, mutate=True, + output=output) + need(not output.exists(), f'{case}/{engine}: rejected checker wrote a receipt') + restore_inputs() + + for label, relative in (('candidate', 'data/SPEC.json'), + ('PR623', 'comparison/PR623-SPEC.json')): + path = stage / PACKAGE / relative + spec = load(path) + spec['expected']['complex_lower'] = '1/100' + dump(path, spec) + reject_mutation('moment-' + label, 'strict exact moment ' + label) + + for case, field, value, reason in ( + ('owner-width', 'width', None, 'actual width'), + ('owner-family', 'family', None, 'physical family'), + ('owner-call', 'stage', None, 'ordered complete call'), + ('owner-footprint', 'offset', 1000000, 'window and footprint')): + path = stage / PACKAGE / 'data/OWNERS.json.gz' + roles = load(path) + roles[0][field] = roles[0][field] + 1 if value is None else value + dump(path, roles) + spec = load(spec_path) + spec['data']['owners_sha256'] = hashlib.sha256(path.read_bytes()).hexdigest() + dump(spec_path, spec) + reject_mutation(case, reason) + + plan_path = stage / PACKAGE / 'data/PLAN.json' + plan = load(plan_path) + plan['provider_calls'][0]['time'] = plan['provider_calls'][1]['time'] + dump(plan_path, plan) + spec = load(spec_path) + spec['data']['plan_sha256'] = hashlib.sha256(plan_path.read_bytes()).hexdigest() + dump(spec_path, spec) + reject_mutation('plan-chronology', 'complete chronology') + + canonical_path = stage / FIXTURE / 'jp8-local/CANONICAL-WORD.json.gz' + canonical = load(canonical_path) + canonical['test_only_metadata'] = True + dump(canonical_path, canonical) + reject_mutation('native-hash', 'unchanged PR622 native word and program') + + programs_path = stage / FIXTURE / 'jp8-local/LOCAL-PROGRAMS.json.gz' + programs = load(programs_path) + paid_event = next(event for event in programs['forward'] + if event[0] in ('climb', 'center')) + paid_event[-1] += 1 + dump(programs_path, programs) + native_hashes_path = stage / PACKAGE / 'comparison/PR622-NATIVE-HASHES.json' + native_hashes = load(native_hashes_path) + native_hashes['jp8/LOCAL-PROGRAMS.json.gz'] = hashlib.sha256( + programs_path.read_bytes()).hexdigest() + dump(native_hashes_path, native_hashes) + reject_mutation('native-orientation', 'both actual orientations') + + print(f'PASS {checks} whole-check subprocess controls; exact receipt equality, ' + f'both engines, and -O ({time.perf_counter() - started:.3f}s)') + + +class ReplayTests(unittest.TestCase): + def test_full_replay(self): + run_controls() + + +if __name__ == '__main__': + unittest.main()