diff --git a/research/data-corner-performance/CLAIM.json b/research/data-corner-performance/CLAIM.json new file mode 100644 index 0000000000..b521250760 --- /dev/null +++ b/research/data-corner-performance/CLAIM.json @@ -0,0 +1,29 @@ +{ + "track": "verification engineering", + "assignment_seed": 86, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "claimed_at": "2026-10-13T05:41:09.483991+00:00", + "expected_finish": "2026-10-13T06:15:00Z", + "candidates": [ + "ternary-side common-pair DAG signature construction", + "partial-swap positive-label propagation", + "copied-fixed exhaustive data-corner elimination" + ], + "selection": "86 mod 3 = 2; data-corner elimination", + "object": "research/copied-fixed/data_corners.cpp", + "method": "Collect the nonzero active columns of each pivot row once, then use the same ordered columns for every lower-row update. Keep all assertions and the full triple-pair domain.", + "expected_deliverable": "Opt-in source-pinned optimization, same-input full-domain benchmarks, byte-identical receipts, negative controls and equivalence note. No new kappa.", + "coordination": "No pinned sprint issue exists; only open issue #650 requests Discussions. GitHub browser signed out and credential helper unavailable; local claim and patch handoff.", + "initial_overlap": "Read latest 100 updated PRs through #788, review ledger, negative-search inventory, and relevant PR154 bottleneck report. Existing tooling #707/#709/#721/#727/#736/#752/#756/#778/#779 targets different kernels. Search API filename queries returned zero and are not relied on as completeness evidence.", + "outcome": { + "status": "completed tooling improvement; preparing one focused PR", + "result": "README.md", + "evidence": "RESULT.json", + "speedup": 1.7098637444120486, + "full_domain_receipts": "byte-identical in all six alternating benchmark processes", + "resumed_at": "2026-10-13T11:25:05.197584+00:00", + "pause": "User interrupted after the initial work and resumed several hours later; measurements completed at approximately 06:01 UTC before the pause.", + "publication": "User authenticated GitHub as just-mn and explicitly confirmed one PR after the final overlap check." + } +} diff --git a/research/data-corner-performance/NOTICE.md b/research/data-corner-performance/NOTICE.md new file mode 100644 index 0000000000..d5102f7ea9 --- /dev/null +++ b/research/data-corner-performance/NOTICE.md @@ -0,0 +1,35 @@ +# Attribution and license + +This contribution is under the repository's Apache-2.0 license. + +Prepared for Denis (@just-mn) with substantial OpenAI Codex assistance in implementation, +experiment design, documentation and scoped AI review. No independent human +review is claimed. + +The actual checker is the unchanged source at +`research/copied-fixed/data_corners.cpp`, pinned in `SOURCE.json`. Its header +credits Rohan Arun's PR39 geometry checker, James Chang's PR34 pivots, and +OpenAI Codex assistance. Douglas R. Colkitt maintains the repository and its +historical integration and verification infrastructure. This package retains +the original source header in both generated compilation units. + +The historical source manifest `research/copied-fixed/SOURCE.json` records: + +- James Chang / jamesyc, PR34, `7fecbe3651e095fb0f450756afdeefd2a9ee80a2`: + reversed geometry and all-weight rank-cut identities. +- Rohan Arun, PR39, `70ae24129649f6d6d4ec6360962a80c3c42a38f1`: + fixed-middle modular nonvanishing method. +- Rohan Arun, PR40, `43f59ff533598762cbc43a5e14af2bbbc76fabbd`: + the contemporaneous both-fixed baseline. +- The same manifest retains the broader construction and recovery lineage, + including Dominik Scholz, icekylinx, RaD / hipotures and Chafik Boukhalfa. + +eumemic's PR154 (`f571bcbd6e06618aeae0b8279da48060032dc74b`) identified this +repeated historical workload as a verification bottleneck. That report is the +profiling lead; this package introduces the per-pivot update-column optimization +and imports no code from PR154 or any pending optimization PR. + +Recent tooling contributions #707, #709, #721, #727, #736, #752, #756, #778 and +#779 improve distinct determinant, geometry, archive, footprint, inverse, +Hermitian, Fano, Gram and reclamation kernels. They were checked for overlap; +they are not dependencies or independent reviewers of this contribution. diff --git a/research/data-corner-performance/OVERLAP.json b/research/data-corner-performance/OVERLAP.json new file mode 100644 index 0000000000..8a93dad60f --- /dev/null +++ b/research/data-corner-performance/OVERLAP.json @@ -0,0 +1,131 @@ +{ + "checked_at": "2026-10-13T05:52:08.462204+00:00", + "open_pr_count": 618, + "max_pr": 799, + "method": "REST pulls, seven pages at 100/page, updated descending; inspect titles/bodies for selected candidate keywords and latest tooling. Non-atomic snapshot, de-duplicated by number.", + "relevant": [ + { + "number": 154, + "title": "Faster verification: concurrent checks, make verify-parallel, faster paired-cube frames, no joint-dual re-pins", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/154", + "updated_at": "2026-10-09T07:37:04Z", + "head": "f571bcbd6e06618aeae0b8279da48060032dc74b" + }, + { + "number": 47, + "title": "Hill-climbed producers for a conditional \u03ba = 4.105106623e-5 bound", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/47", + "updated_at": "2026-10-08T15:05:44Z", + "head": "117caf164e3b235ef20188aa2dc1b49617e9255c" + }, + { + "number": 44, + "title": "Weighted carrier matching: conditional \u03ba = 4.100629254e-5 > 2^-15", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/44", + "updated_at": "2026-10-08T14:35:23Z", + "head": "1a21794eb5384db0e96d7bc2b11aa6f28cff7a85" + }, + { + "number": 41, + "title": "Alternating pair-block networks for conditional \u03ba = 4.034168124 \u00d7 10\u207b\u2075 > 2\u207b\u00b9\u2075", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/41", + "updated_at": "2026-10-08T13:46:27Z", + "head": "03bde70c0c2a453f1ceae20c619b602841405467" + }, + { + "number": 35, + "title": "Fixed local bases in two stages for conditional \u03ba = 1.6631776e-5", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/35", + "updated_at": "2026-10-08T12:37:15Z", + "head": "9c345a2a11e5f4f3649f7c68214bf9a2a0a3fe9c" + }, + { + "number": 34, + "title": "Reversed two-stage basis and balanced assembly for conditional \u03ba = 1.639226629e-5", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/34", + "updated_at": "2026-10-08T12:10:06Z", + "head": "7fecbe3651e095fb0f450756afdeefd2a9ee80a2" + }, + { + "number": 33, + "title": "Compose smaller two-stage dimensions and data blocks for conditional \u03ba = 1.638103206e-5", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/33", + "updated_at": "2026-10-08T11:49:21Z", + "head": "a499a345c040aa15b68e984a0904eadc485c7a7e" + }, + { + "number": 31, + "title": "Exact data-corner certificates for conditional \u03ba = 1.5878574e-5 > 2^-16", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/31", + "updated_at": "2026-10-08T11:37:30Z", + "head": "122e6453e80330633af701eabd1a6a72dfefd286" + }, + { + "number": 29, + "title": "Two-stage controlled corners for a conditional 15536/10^9 > 2^-16 bound", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/29", + "updated_at": "2026-10-08T11:20:11Z", + "head": "9d963275075fa98f1da821e27757b238dafd6b3c" + }, + { + "number": 21, + "title": "Translated partial-swap frames for a conditional 5499/10^9 > 2^-18 bound", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/21", + "updated_at": "2026-10-08T10:24:48Z", + "head": "5ba6cf0bfb68f2be8d15610e7972207c50254d6a" + }, + { + "number": 17, + "title": "Compose nested geometry and smaller h30 producer for conditional \u03ba = 1.248342e-6 > 2^-20", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/17", + "updated_at": "2026-10-08T10:04:07Z", + "head": "c915b4117626a512dd470adbdbd76963108f5cb3" + }, + { + "number": 16, + "title": "Nested controlled bases for a conditional 9799/10^10 > 2^-20 bound", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/16", + "updated_at": "2026-10-08T09:36:26Z", + "head": "a80f5e676c84b59def9791495df0655efe89a04f" + }, + { + "number": 15, + "title": "Smaller h30 producer and full complex batching for conditional \u03ba > 2^-20", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/15", + "updated_at": "2026-10-08T09:26:21Z", + "head": "a17cab396ce1c79c288bde9d06002cefdc0af8e6" + }, + { + "number": 14, + "title": "Combine source frames and data corners for conditional kappa = 9.0799e-7", + "html_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/14", + "updated_at": "2026-10-08T09:19:26Z", + "head": "1fa5b9a9aaccbebb3eb29ac7ea55811f46464eee" + } + ], + "conclusion": "No matching per-pivot data-corner update-list optimization found. PR154 is the credited profiling lead; related historical construction PRs are not new optimization dependencies.", + "final_refresh": { + "checked_at": "2026-10-13T11:23:38Z", + "open_pr_count": 693, + "highest_pr": 902, + "upstream_head": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "execution_inputs_unchanged": true, + "new_tooling_reviewed": [ + 900, + 898, + 871, + 865, + 853, + 849, + 847, + 841, + 833, + 824, + 819, + 818, + 808, + 797 + ], + "conclusion": "New tooling concerns sparse fusion, Leech minors, joint frames, supplier receipts, dyadic arithmetic, cyclic routing, signed-sparse enumeration, stage pairs, gzip binding, RREF and reclamation. No matching data-corner update-list optimization found." + } +} diff --git a/research/data-corner-performance/PRELIMINARY.json b/research/data-corner-performance/PRELIMINARY.json new file mode 100644 index 0000000000..9e946af7f2 --- /dev/null +++ b/research/data-corner-performance/PRELIMINARY.json @@ -0,0 +1,26 @@ +{ + "status": "preliminary sequential original-then-optimized probe; separate from alternating benchmark", + "compiler": "Apple clang 21.0.0 (clang-2100.3.34.2)", + "flags": [ + "-O3", + "-std=c++17" + ], + "original": { + "wall_seconds": 167.98, + "user_seconds": 165.66, + "system_seconds": 0.94 + }, + "optimized": { + "wall_seconds": 98.78, + "user_seconds": 98.05, + "system_seconds": 0.45 + }, + "complete_stdout_equal": true, + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "source_sha256": { + "research/copied-fixed/data_corners.cpp": "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44", + "research/copied-fixed/data-corners.json": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17" + }, + "optimized_source_sha256": "406a850d496589cd1216eb709baa84fdd8633048b648f05022ae184d1f279448", + "scope": "Full primary-prime checker; unchanged separate rational recovery excluded. Timings from /usr/bin/time -p; no cache flush." +} diff --git a/research/data-corner-performance/README.md b/research/data-corner-performance/README.md new file mode 100644 index 0000000000..ff63513d16 --- /dev/null +++ b/research/data-corner-performance/README.md @@ -0,0 +1,131 @@ +# Exact data-corner replay with cached update columns + +**Tooling improvement; no new κ or construction claim.** This optional runner +accelerates the historical `research/copied-fixed/data_corners.cpp` checker. +It preserves the complete domain of 4,073,300 pairs of triples, every existing +assertion, and the complete output receipt, including all ten modular failures. +At the recorded base, the selected #626/#543 conditional result was +κ = 51110230636731/31250000000000000 = 0.001635527380375392. + +## Reproduce + +Use Python 3.9+ on macOS or Linux and a C++17 compiler, from the repository root: + +```sh +python3 -B research/data-corner-performance/replay.py --benchmark 3 --output /tmp/data-corner-result.json +``` + +Use an output path that does not exist. Expected final line: + +```text +PASS_DATA_CORNER_REPLAY pairs=4073300 complete_receipts_equal=true +``` + +This compiles the pinned original and the optimized source, then runs three +sequential pairs in alternating order. Each process replays the entire domain; +every receipt field must equal the frozen predecessor receipt, and every run's +stdout must be byte-identical. Timings are descriptive, with no pass threshold. +Compilation and receipt comparison are outside the measured process interval. +The interval includes process startup, computation, and captured output. +OS caches are not flushed and other system activity is uncontrolled. + +For the faster complete replay alone, omit `--benchmark`. `CXX` selects the +compiler; both variants use the same `-O3 -std=c++17` flags. The runner refuses +changed source or receipt bytes and refuses a build with `NDEBUG` defined. +No Python or C++ package dependencies are required. + +Focused controls: + +```sh +python3 -B research/data-corner-performance/test_replay.py -v +python3 -O -B research/data-corner-performance/test_replay.py -v +``` + +## Why the change is exact + +After accepting pivot `(i,c)`, the original loop removes `c` from `available`. +For every lower row `r` with `M[r][c] != 0`, it scans all 47 columns, updating +precisely those satisfying `available[j] && M[i][j] != 0`. + +Neither `available` nor pivot row `M[i]` changes during that lower-row loop: +all writes have row index `r > i`. The new code collects this exact ordered +column list once per pivot. Each lower row then performs the identical modular +updates in the identical order, with the identical ratio, and clears the same +pivot entry. By induction over rows and pivots, the matrices, pivot products, +zero checks and first-failure positions agree. List construction occurs after +the existing ordered-zero assertions and does not replace any of them. + +The pivot order is not natural column order. Eligible columns **left of the +pivot must be included**. The separate `j > c` condition belongs only to the +ordered-zero assertions. A regression embeds +`[[2,1],[1,1]]` with pivot order `[1,0]`: the correct pivot product is −1 modulo +1000003; deliberately omitting left-of-pivot updates gives +1 and is detected. +Reversing the cached list is a positive control: distinct column updates +commute, and both the receipt and complete final matrix remain equal. + +The additional stack array holds only 47 integers. The optimization removes +repeated eligibility scans; it does not reuse a result across matrices, omit +pairs, change the prime, or replace exact arithmetic with numerical arithmetic. + +## Evidence and coverage + +`RESULT.json` contains the measured compiler/platform, raw alternating samples, +implementation/generated-source hashes, input pins, and coverage counters. +`PRELIMINARY.json` retains the first same-input measurement separately. +Three alternating process pairs on Apple clang 21.0.0 / macOS arm64 gave +median wall times **169.198 s → 98.954 s (1.710× faster; 41.5% less time)**. +Every stdout and stderr hash agreed. These measurements finished before the +session pause; `VALIDATION.json` records the final checks after resuming. + +The full predecessor receipt covers: + +| Obligation | Count | +|---|---:| +| Triple pairs | 4,073,300 | +| Primary-prime successes | 4,073,290 | +| Primary-prime fallback records | 10 | +| Nonzero pivot checks | 191,444,880 | +| Ordered-zero checks | 1,409,360,440 | +| Per-first-triple product records | 1,771 | + +Seven focused test groups compile the actual original and transformed C++ +elimination bodies in an eight-column harness. They compare complete final +matrices and partial receipts on 48 seed-86 dense/sparse cases and each of eight +failure positions. An independent Python determinant implementation uses +natural-column elimination with row swaps and verifies successful products, +including the sign of non-natural column permutations. These tests also cover +the left-of-pivot mutation, valid reversed updates, invalid ordered zeros, +repeated pivots, source and fixture drift, ambiguous transformation sites, +disabled C++ assertions, and eight corruptions of proof-relevant receipt fields. +This is finite differential validation plus a loop-equivalence argument, not a +formal proof of the multiplication theorem. + +The ten primary-prime failures remain failures in this runner's output. The +historical producer subsequently calls `data_recovery.py`, which verifies their +47 ordered pivots over the rationals. That separate recovery is unchanged and +is outside this optimization and its timing claims. No modular zero is called +a rational counterexample. + +## Scope, provenance and handoff + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +`SOURCE.json` pins the two execution inputs by SHA-256 and Git blob identity. +The runner requires only this package and those two repository-relative files; +it does not access the network or depend on Git during execution. + +`CLAIM.json` records OS-random seed 86, the three candidates, scope and overlap +checks. There was no pinned coordination issue, so the claim is local. The user later +authenticated GitHub and confirmed submission of one focused PR. +A final overlap sweep covered 693 open PRs through #902; no matching optimization +was found. After a user-requested pause, upstream was refreshed to +`f567884aeb8851b6e794af1184119a3bfbe1e631`; both execution input blobs are unchanged there. Existing source +packages, manifests, certificates, default targets and `upstream/` are unchanged. +Only files in this directory are added. + +The selected supplier cold replay, whole-repository `make verify`, Lean, and +remote CI were not rerun for this isolated opt-in historical checker. The +all-size/compiler/common-label/hosting/residual/precision/tape/analytic +assumptions remain. Measurements concern this finite checker, not the selected +frontier or practical integer multiplication. + +See `NOTICE.md` for predecessor credit and AI disclosure. diff --git a/research/data-corner-performance/RESULT.json b/research/data-corner-performance/RESULT.json new file mode 100644 index 0000000000..93f8c8370d --- /dev/null +++ b/research/data-corner-performance/RESULT.json @@ -0,0 +1,82 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "compiler": [ + "c++" + ], + "compiler_version": "Apple clang version 21.0.0 (clang-2100.3.34.2)\nTarget: arm64-apple-darwin27.0.0\nThread model: posix\nInstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin\n", + "coverage": { + "fallback": 10, + "good": 4073290, + "nonzero_pivots": 191444880, + "ordered_zero_checks": 1409360440, + "pairs": 4073300 + }, + "flags": [ + "-O3", + "-std=c++17" + ], + "generated_source_sha256": "992cf0102713d56d8aaa1717a1e308d2ca952b580c4f810188f1540c1d4cfb8f", + "implementation_sha256": "ce7cceeabb816d4a70aaa6352d5ba0432ac7dea4f66f903e3af4fa91aa44c822", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "python": "3.12.13", + "samples": [ + { + "cpu_seconds": 165.882217, + "mode": "original", + "pair": 0, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 166.40425866700025 + }, + { + "cpu_seconds": 98.55262799999998, + "mode": "optimized", + "pair": 0, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 98.87180512499981 + }, + { + "cpu_seconds": 98.65132000000003, + "mode": "optimized", + "pair": 1, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 98.95382237499871 + }, + { + "cpu_seconds": 167.62091299999997, + "mode": "original", + "pair": 1, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 169.19755325000006 + }, + { + "cpu_seconds": 170.62557400000006, + "mode": "original", + "pair": 2, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 174.0469577499989 + }, + { + "cpu_seconds": 98.95722399999987, + "mode": "optimized", + "pair": 2, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 99.43689258400082 + } + ], + "source_sha256": { + "research/copied-fixed/data-corners.json": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "research/copied-fixed/data_corners.cpp": "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44" + }, + "speedup": 1.7098637444120486, + "status": "PASS_DATA_CORNER_REPLAY", + "wall_medians": { + "optimized": 98.95382237499871, + "original": 169.19755325000006 + } +} diff --git a/research/data-corner-performance/SOURCE.json b/research/data-corner-performance/SOURCE.json new file mode 100644 index 0000000000..d3bb8ef318 --- /dev/null +++ b/research/data-corner-performance/SOURCE.json @@ -0,0 +1,11 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "sha256": { + "research/copied-fixed/data_corners.cpp": "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44", + "research/copied-fixed/data-corners.json": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17" + }, + "git_blob": { + "research/copied-fixed/data_corners.cpp": "251f6c87cca42619a0c1b6d83705df5cad0e9c33", + "research/copied-fixed/data-corners.json": "4cb7a2b26fc48afd020b7966c43fd30cf2321514" + } +} diff --git a/research/data-corner-performance/VALIDATION.json b/research/data-corner-performance/VALIDATION.json new file mode 100644 index 0000000000..91d9c0f75f --- /dev/null +++ b/research/data-corner-performance/VALIDATION.json @@ -0,0 +1,19 @@ +{ + "checked_at": "2026-10-13T11:25:05.275000+00:00", + "tests": { + "normal": "7 tests pass", + "python_O": "7 tests pass" + }, + "benchmark": "All 6 fresh processes cover the full fixed domain and match the frozen receipt byte for byte.", + "source_identity": "All SHA256 and Git blob pins agree with base; both input blob IDs unchanged at f567884aeb8851b6e794af1184119a3bfbe1e631", + "measured_implementation_unchanged": true, + "selected_base_certificate_sha256": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "ai_review": "Separate bounded AI review found no loop-equivalence defect; no independent human review claimed. Manifest commit/blob provenance checked separately against Git; runtime admission uses SHA256.", + "not_run": [ + "whole-repository make verify", + "selected cold supplier replay", + "separate historical rational recovery", + "Lean", + "remote CI" + ] +} diff --git a/research/data-corner-performance/replay.py b/research/data-corner-performance/replay.py new file mode 100644 index 0000000000..fe66919a4c --- /dev/null +++ b/research/data-corner-performance/replay.py @@ -0,0 +1,121 @@ +#!/usr/bin/env python3 +"""Source-pinned, opt-in replay of the complete historical data-corner check.""" +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import resource +import shlex +import statistics +import subprocess +import tempfile +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +GUARD = '#ifdef NDEBUG\n#error "Data-corner replay requires assertions"\n#endif\n' +OLD_INVERSE = 'int inv=power(value,prime-2);' +NEW_INVERSE = OLD_INVERSE + ''' + int columns[d],length=0; + for(int j=0;j= 0, 'Negative benchmark pair count') + require(not args.output or not args.output.exists(), 'Output already exists') + manifest, blobs = admitted_inputs() + source = blobs['research/copied-fixed/data_corners.cpp'].decode() + expected = json.loads(blobs['research/copied-fixed/data-corners.json']) + compiler = shlex.split(os.environ.get('CXX', 'c++')) + version = subprocess.check_output([*compiler, '--version'], text=True) + samples = [] + with tempfile.TemporaryDirectory(prefix='data-corner-') as directory: + work = Path(directory) + compile_program(transform(source), work / 'optimized', compiler) + if args.benchmark: + compile_program(source, work / 'original', compiler) + common_stdout = None + for pair in range(args.benchmark or 1): + modes = (['original', 'optimized'] if pair % 2 == 0 else + ['optimized', 'original']) if args.benchmark else ['optimized'] + for mode in modes: + stdout, sample = timed_run(work / mode, expected) + if common_stdout is not None: + require(stdout == common_stdout, 'Original/optimized bytes differ') + common_stdout = stdout + samples.append(dict(pair=pair, mode=mode, **sample)) + print(f'PASS pair={pair} {mode} wall={sample["wall_seconds"]:.3f}s', flush=True) + evidence = dict(status='PASS_DATA_CORNER_REPLAY', base_commit=manifest['base_commit'], + source_sha256=manifest['sha256'], implementation_sha256=sha256(Path(__file__).read_bytes()).hexdigest(), + generated_source_sha256=sha256((GUARD + transform(source)).encode()).hexdigest(), + platform=platform.platform(), python=platform.python_version(), compiler=compiler, + compiler_version=version, flags=['-O3', '-std=c++17'], + coverage={k: expected[k] for k in ('pairs', 'good', 'fallback', 'nonzero_pivots', 'ordered_zero_checks')}, + samples=samples) + if args.benchmark: + medians = {mode: statistics.median(s['wall_seconds'] for s in samples if s['mode'] == mode) + for mode in ('original', 'optimized')} + evidence.update(wall_medians=medians, speedup=medians['original'] / medians['optimized']) + if args.output: + with args.output.open('x') as stream: + stream.write(json.dumps(evidence, indent=2, sort_keys=True) + '\n') + print('PASS_DATA_CORNER_REPLAY pairs=4073300 complete_receipts_equal=true') + + +if __name__ == '__main__': + main() diff --git a/research/data-corner-performance/test_replay.py b/research/data-corner-performance/test_replay.py new file mode 100644 index 0000000000..2a1781ffcb --- /dev/null +++ b/research/data-corner-performance/test_replay.py @@ -0,0 +1,186 @@ +"""Exercise the actual two C++ elimination loops and an independent determinant.""" +import copy +from hashlib import sha256 +import json +from pathlib import Path +import random +import resource +import subprocess +import tempfile +import unittest + +import replay + +P = 1000003 +D = 8 + + +def determinant(matrix): + """Independent natural-column elimination with row pivoting, over F_P.""" + rows = [row[:] for row in matrix] + answer = 1 + for column in range(len(rows)): + pivot = next((r for r in range(column, len(rows)) if rows[r][column]), None) + if pivot is None: + return 0 + if pivot != column: + rows[pivot], rows[column] = rows[column], rows[pivot] + answer = -answer + value = rows[column][column] + answer = answer * value % P + normalized = [x * pow(value, -1, P) % P for x in rows[column]] + for r in range(column + 1, len(rows)): + factor = rows[r][column] + rows[r] = [(x - factor * y) % P for x, y in zip(rows[r], normalized)] + return answer + + +def kernel_program(source): + start = source.index(' bool ok=true;int determinant=1;') + end = source.index(' count++;', start) + return '''#include +#include +#include +#include +#include +using namespace std; +constexpr int prime=1000003,d=8; +''' + source[source.index('int mul('):source.index('int main()')] + ''' +int main(){ + int M[d][d],piv[d]; bool available[d]; + for(int i=0;i>piv[i]; + for(int i=0;i>M[i][j];} + int aa=0,bb=0,cc=0,u=0,v=0,w=0; + int64_t checked=0,zeros=0;vector> rejected; +''' + source[start:end] + ''' + cout<=0;k--)'), + missing_left=optimized.replace('columns[length++]=j;', 'if(j>c)columns[length++]=j;')) + for name, source in variants.items(): + replay.compile_program(kernel_program(source), cls.work / name, ['c++']) + + @classmethod + def tearDownClass(cls): + cls.directory.cleanup() + + def run_kernel(self, mode, matrix, pivots): + data = ' '.join(map(str, pivots + sum(matrix, []))).encode() + return subprocess.run([str(self.work / mode)], input=data, capture_output=True) + + def compare(self, matrix, pivots): + original = self.run_kernel('original', matrix, pivots) + self.assertEqual(original.returncode, 0, original.stderr) + for mode in ('optimized', 'reversed'): + actual = self.run_kernel(mode, matrix, pivots) + self.assertEqual(actual.returncode, 0, actual.stderr) + self.assertEqual(actual.stdout, original.stdout) + return list(map(int, original.stdout.split())) + + def test_seeded_complete_kernel_states_and_independent_determinants(self): + rng = random.Random(86) + for trial in range(48): + pivots = list(range(D)) + if trial == 1: + pivots.reverse() + elif trial > 1: + rng.shuffle(pivots) + lower = [[int(i == j) if i <= j else rng.randrange(P) for j in range(D)] for i in range(D)] + upper = [[(rng.randrange(1, P) if i == j else rng.randrange(P)) + if j >= i and pivots[j] <= pivots[i] else 0 for j in range(D)] for i in range(D)] + matrix = [[0] * D for _ in range(D)] + for i in range(D): + for j in range(D): + matrix[i][pivots[j]] = sum(lower[i][k] * upper[k][j] for k in range(D)) % P + out = self.compare(matrix, pivots) + parity = sum(pivots[i] > pivots[j] for i in range(D) for j in range(i + 1, D)) % 2 + self.assertEqual(out[0], 1) + self.assertEqual(out[2], D) + self.assertEqual(out[1] * (-1 if parity else 1) % P, determinant(matrix)) + + def test_left_of_pivot_update_and_missing_entry_mutation(self): + matrix = [[int(i == j) for j in range(D)] for i in range(D)] + matrix[0][:2], matrix[1][:2] = [2, 1], [1, 1] + pivots = [1, 0] + list(range(2, D)) + actual = self.compare(matrix, pivots) + self.assertEqual(actual[1], P - 1) + mutant = self.run_kernel('missing_left', matrix, pivots) + self.assertEqual(mutant.returncode, 0) + self.assertEqual(int(mutant.stdout.split()[1]), 1) + self.assertNotEqual(mutant.stdout, self.run_kernel('optimized', matrix, pivots).stdout) + + def test_every_failure_position_retains_partial_receipt(self): + for failed in range(D): + matrix = [[int(i == j and i != failed) for j in range(D)] for i in range(D)] + out = self.compare(matrix, list(range(D))) + self.assertEqual((out[0], out[2], out[4], out[5]), (0, failed, 1, failed)) + + def test_ordered_zero_and_repeated_pivot_rejected(self): + identity = [[int(i == j) for j in range(D)] for i in range(D)] + bad_zero = copy.deepcopy(identity) + bad_zero[0][1] = 1 + for matrix, pivots in ((bad_zero, list(range(D))), (identity, [0, 0] + list(range(2, D)))): + for mode in ('original', 'optimized'): + self.assertNotEqual(self.run_kernel(mode, matrix, pivots).returncode, 0) + + def test_source_drift_and_ambiguous_patch_refused(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + for name, data in self.blobs.items(): + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(data) + replay.admitted_inputs(root) + for name, data in self.blobs.items(): + (root / name).write_bytes(data + b' ') + with self.assertRaisesRegex(ValueError, 'Source drift'): + replay.admitted_inputs(root) + (root / name).write_bytes(data) + with self.assertRaisesRegex(ValueError, 'exactly one'): + replay.transform(self.source + replay.OLD_UPDATE) + + def test_complete_receipt_binding(self): + replay.validate_receipt(json.dumps(self.expected), self.expected) + mutations = [] + for key in ('pairs', 'good', 'fallback', 'nonzero_pivots', 'ordered_zero_checks'): + changed = copy.deepcopy(self.expected) + changed[key] += 1 + mutations.append(changed) + for key in ('records', 'fallback_pairs'): + changed = copy.deepcopy(self.expected) + changed[key].pop() + mutations.append(changed) + changed = copy.deepcopy(self.expected) + changed['records'][0][-1] += 1 + mutations.append(changed) + for changed in mutations: + with self.assertRaisesRegex(ValueError, 'receipt differs'): + replay.validate_receipt(json.dumps(changed), self.expected) + + def test_disabled_assertions_refused_at_compile_time(self): + path = self.work / 'disabled.cpp' + path.write_text(replay.GUARD + kernel_program(self.source)) + result = subprocess.run(['c++', '-DNDEBUG', '-std=c++17', str(path), '-o', str(self.work / 'disabled')], + capture_output=True) + self.assertNotEqual(result.returncode, 0) + self.assertIn(b'requires assertions', result.stderr) + + +if __name__ == '__main__': + unittest.main()