From 94ef5de84f6b0c921c6c267deaec5d7fe26bf727 Mon Sep 17 00:00:00 2001 From: just-mn <77879381+just-mn@users.noreply.github.com> Date: Tue, 13 Oct 2026 13:28:35 +0200 Subject: [PATCH 1/2] Pin historical data-corner checker inputs Record exact source and receipt pins for an opt-in replay optimization. Prepared with OpenAI Codex assistance. --- research/data-corner-performance/SOURCE.json | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 research/data-corner-performance/SOURCE.json 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" + } +} From 4e1d75e312d09107298ceeb27a79d96f369459db Mon Sep 17 00:00:00 2001 From: just-mn <77879381+just-mn@users.noreply.github.com> Date: Tue, 13 Oct 2026 13:30:48 +0200 Subject: [PATCH 2/2] Add faster exhaustive data-corner replay and validation Cache eligible update columns per pivot while preserving the original checks. Include six full replay measurements, matching receipts, source pins, regression tests, and contribution attribution. Substantial OpenAI Codex assistance. --- research/data-corner-performance/CLAIM.json | 29 +++ research/data-corner-performance/NOTICE.md | 35 ++++ research/data-corner-performance/OVERLAP.json | 131 ++++++++++++ .../data-corner-performance/PRELIMINARY.json | 26 +++ research/data-corner-performance/README.md | 131 ++++++++++++ research/data-corner-performance/RESULT.json | 82 ++++++++ .../data-corner-performance/VALIDATION.json | 19 ++ research/data-corner-performance/replay.py | 121 ++++++++++++ .../data-corner-performance/test_replay.py | 186 ++++++++++++++++++ 9 files changed, 760 insertions(+) create mode 100644 research/data-corner-performance/CLAIM.json create mode 100644 research/data-corner-performance/NOTICE.md create mode 100644 research/data-corner-performance/OVERLAP.json create mode 100644 research/data-corner-performance/PRELIMINARY.json create mode 100644 research/data-corner-performance/README.md create mode 100644 research/data-corner-performance/RESULT.json create mode 100644 research/data-corner-performance/VALIDATION.json create mode 100644 research/data-corner-performance/replay.py create mode 100644 research/data-corner-performance/test_replay.py 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/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()