diff --git a/research/copied-fixed/certificate.json b/research/copied-fixed/certificate.json index 28e29d9982..ce82681fde 100644 --- a/research/copied-fixed/certificate.json +++ b/research/copied-fixed/certificate.json @@ -17769,7 +17769,7 @@ "research/copied-fixed/comparison-pr46.json": "f7a34054403075c51289e58b583c05ff42c43e72d286b9c3ff4fc5ae7f4bca44", "research/copied-fixed/comparison-pr47.json": "d15ecc820d540a2bfea10bc7d72688240aea89245ff27de263b1de0e74e4273a", "research/copied-fixed/data-corners.json": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", - "research/copied-fixed/data_corners.cpp": "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44", + "research/copied-fixed/data_corners.cpp": "406a850d496589cd1216eb709baa84fdd8633048b648f05022ae184d1f279448", "research/copied-fixed/data_recovery.py": "0de7e0fc4f38b066ec319e4dde43bce8f20edd207be9f9736610babf95030253", "research/copied-fixed/links-23.uses": "b215350929d15711b502cdcf5878aeedb2cc7dc81dc764977a28d37ece17f86f", "research/copied-fixed/links-25.uses": "80dd63ea393931211bece7a44329a9da4e2936575cdc3f48c27690bedc2ad0ae", diff --git a/research/copied-fixed/data_corners.cpp b/research/copied-fixed/data_corners.cpp index 251f6c87cc..51cef05c6e 100644 --- a/research/copied-fixed/data_corners.cpp +++ b/research/copied-fixed/data_corners.cpp @@ -50,9 +50,12 @@ int main(){ for(int j=c+1;j +#include +#include +#include +#include +using namespace std; +constexpr int prime=1000003,a=23,b=25,d=47; +int mul(int x,int y){return int(int64_t(x)*y%prime);} +int power(int x,int n){int z=1;for(;n;n>>=1,x=mul(x,x))if(n&1)z=mul(z,x);return z;} +int main(){ + for(int i=2;i*i<=prime;++i)assert(prime%i); + vector R,C,piv; + for(int i=0;i> rejected; + cout<<"{\"prime\":"<= 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() + baseline = blobs['research/data-corner-performance/baseline.cpp'].decode() + production = blobs['research/copied-fixed/data_corners.cpp'].decode() + require(production == transform(baseline), + 'production data_corners.cpp must equal transform(baseline.cpp)') 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) + compile_program(production, work / 'optimized', compiler) if args.benchmark: - compile_program(source, work / 'original', compiler) + compile_program(baseline, work / 'original', compiler) common_stdout = None for pair in range(args.benchmark or 1): modes = (['original', 'optimized'] if pair % 2 == 0 else @@ -102,7 +111,7 @@ def main(): 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(), + generated_source_sha256=sha256((GUARD + production).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')}, diff --git a/research/data-corner-performance/test_replay.py b/research/data-corner-performance/test_replay.py index 2a1781ffcb..300d1c9694 100644 --- a/research/data-corner-performance/test_replay.py +++ b/research/data-corner-performance/test_replay.py @@ -67,9 +67,11 @@ def setUpClass(cls): cls.directory = tempfile.TemporaryDirectory(prefix='corner-controls-') cls.work = Path(cls.directory.name) _, cls.blobs = replay.admitted_inputs() - cls.source = cls.blobs['research/copied-fixed/data_corners.cpp'].decode() + cls.source = cls.blobs['research/data-corner-performance/baseline.cpp'].decode() + cls.production = cls.blobs['research/copied-fixed/data_corners.cpp'].decode() cls.expected = json.loads(cls.blobs['research/copied-fixed/data-corners.json']) - optimized = replay.transform(cls.source) + assert cls.production == replay.transform(cls.source) + optimized = cls.production variants = dict(original=cls.source, optimized=optimized, reversed=optimized.replace('for(int k=0;k=0;k--)'), missing_left=optimized.replace('columns[length++]=j;', 'if(j>c)columns[length++]=j;')) diff --git a/research/data-corner-production/NOTICE.md b/research/data-corner-production/NOTICE.md new file mode 100644 index 0000000000..feb3115caa --- /dev/null +++ b/research/data-corner-production/NOTICE.md @@ -0,0 +1,18 @@ +# Attribution and license + +Prepared by Wentao Li ([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor), wentaol4@illinois.edu) with substantial +AI assistance for orientation, overlap search, profiling, production wiring, +packaging, benchmarking and writing. Not independent human peer review. +Apache-2.0; see the repository root `LICENSE`. + +The cached update-column algorithm and its equivalence argument were introduced +in the opt-in adapter `research/data-corner-performance/` (see that package's +NOTICE.md). This package wires an equivalent loop into the production +`research/copied-fixed/data_corners.cpp` path used by +`make copied-fixed-verify`. + +The historical copied-fixed data-corner checker, receipt and certificate lineage +retain their original author credits in `research/copied-fixed/SOURCE.json` and +`research/copied-fixed/PROOF.md`. Upstream material retains its own source +notices and license. diff --git a/research/data-corner-production/README.md b/research/data-corner-production/README.md new file mode 100644 index 0000000000..340a9912c8 --- /dev/null +++ b/research/data-corner-production/README.md @@ -0,0 +1,108 @@ +# Production cached update columns for the historical data-corner checker + +**Tooling improvement; no new kappa.** At base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, +`research/copied-fixed/data_corners.cpp` still rescanned all 47 columns for +every lower-row update. The opt-in adapter `research/data-corner-performance/` +already proved an exact per-pivot cached-column list with identical receipts. +This package wires that equivalent loop into the **production** checker used by +`research/copied-fixed/producer.py` / `make copied-fixed-verify`. + +Only the `local_sha256` entry for `research/copied-fixed/data_corners.cpp` +changes inside `research/copied-fixed/certificate.json`. The complete domain of +4,073,300 pairs, every assertion, modular fallback recovery and the pinned +`data-corners.json` receipt stay identical. Selected frontier untouched. + +The pairwise-era digest in `research/data-corner-performance/SOURCE.json` is +demoted: that package now vendors `baseline.cpp` and treats working +`data_corners.cpp` as the optimized production source, so research-packages / +local replay do not fail working-source drift. + +## Reproduce + +Python **3.12**, a C++17 compiler (`CXX`, default `c++`), standard library only, +from the repository root: + +```sh +python3.12 -I -B research/data-corner-production/verify.py +python3.12 -I -O -B research/data-corner-production/verify.py +python3.12 -B scripts/research_package.py --package research/data-corner-production +python3.12 -I -B research/data-corner-production/benchmark.py --rounds 5 --out /tmp/data-corner-production-result.json +``` + +Expected: + +```text +PASS_DATA_CORNER_PRODUCTION pairs=4073300 good=4073290 fallback=10 corruption=… certs=1 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/data-corner-production outcome=completed +PASS_IDENTICAL_DATA_CORNER_PRODUCTION_RECEIPTS +``` + +Default verify is read-only. Temp-copy column-fill foil rejects via receipt +mismatch or subprocess failure. Package gates under `-O` still launch +assertion-enabled C++ children (`NDEBUG` is rejected at compile time). Full +`make verify`, selected cold replay, Lean, and multiplication-theorem +obligations were not rerun for this isolated historical-checker change. + +## Result + +On Linux / CPython 3.12.3 with g++ (taskset CPU 0), five alternating +fresh-process pairs gave median wall time **170.101 → 110.463 seconds +(1.54×)**. Timing is host-descriptive and is not a correctness gate; all +samples and environment pins are in [`RESULT.json`](RESULT.json). Every stdout +receipt matches the pinned `data-corners.json` fieldwise. An unpinned multi-core +screen on the same host was noisier (~1.38×); the reported figure is the pinned +five-pair series. + +## Why the cached columns are equivalent + +After accepting pivot `(i,c)`, neither `available` nor pivot row `M[i]` changes +during the lower-row update loop. Collecting + +```text +columns = [j | available[j] && M[i][j]] +``` + +once per pivot, then iterating that list for every lower row `r` with +`M[r][c] != 0`, performs the same modular updates in the same column order as +the historical nested scan. See `research/data-corner-performance/README.md`. + +## Overlap and credit + +Closest priors (different delivery): + +- `research/data-corner-performance/` — opt-in cached-column adapter; this is + the production wiring. +- [CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756) + — identical-receipt tooling quality bar. +- Open leave-alone tooling on other objects (#1922 joint frames, #2039/#2054 + shared-point, #2100 ternary, #2117 DisjointTensor, #2150 mixed-point, + #2194/#2210/#2231/#2239/#2257/#2263/#2276 production rewrites; #1076 + quadratic-affine) was not reopened. Soft note: #2263/#2276 touch + `e8-bit-r420/MANIFEST.sha256`; this tip does not. + +Credit the authors of `research/data-corner-performance/` and the copied-fixed +lineage. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance, under +Apache-2.0. + +## Open next questions + +1. **Question:** Should adjacent historical copies under `research/pair-assembly/`, + `research/skip-strips/`, and `research/split-skip/` adopt the same cached + columns in a follow-up tip? + **Why it matters:** Those trees still pin pairwise-era digests without a + registered VERIFY matrix; a coordinated refresh would remove stale inventory + digests without changing receipts. + **First step:** Diff each `data_corners.cpp` against the production transform + site and list which SOURCE inventories would need provenance demotion. + **Blocked by:** Out of this session’s one-object stop rule. + +2. **Question:** Should `make copied-fixed-verify` grow a microbenchmark gate + for the full 4,073,300-pair replay? + **Why it matters:** A future edit could restore the nested scan without + failing equivalence tests. + **First step:** Decide whether RESULT.json medians belong in CI or remain + descriptive. + **Blocked by:** Maintainer CI-budget preference. diff --git a/research/data-corner-production/RESULT.json b/research/data-corner-production/RESULT.json new file mode 100644 index 0000000000..afe0ac8259 --- /dev/null +++ b/research/data-corner-production/RESULT.json @@ -0,0 +1,114 @@ +{ + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "compiler": [ + "c++" + ], + "compiler_version": "c++ (Ubuntu 13.3.0-6ubuntu2~24.04.1) 13.3.0\nCopyright (C) 2023 Free Software Foundation, Inc.\nThis is free software; see the source for copying conditions. There is NO\nwarranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.\n\n", + "coverage": { + "fallback": 10, + "good": 4073290, + "nonzero_pivots": 191444880, + "ordered_zero_checks": 1409360440, + "pairs": 4073300 + }, + "flags": [ + "-O3", + "-std=c++17" + ], + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "python": "3.12.3", + "rounds": 5, + "samples": [ + { + "cpu_seconds": 167.62473599999998, + "mode": "baseline", + "pair": 0, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 167.66491957999915 + }, + { + "cpu_seconds": 110.44216499999999, + "mode": "optimized", + "pair": 0, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 110.46253971399983 + }, + { + "cpu_seconds": 118.22218999999998, + "mode": "optimized", + "pair": 1, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 118.24173000100018 + }, + { + "cpu_seconds": 183.620519, + "mode": "baseline", + "pair": 1, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 183.65866714500044 + }, + { + "cpu_seconds": 176.37448699999993, + "mode": "baseline", + "pair": 2, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 176.46536360799928 + }, + { + "cpu_seconds": 105.26084699999996, + "mode": "optimized", + "pair": 2, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 105.2775133060004 + }, + { + "cpu_seconds": 99.15634399999995, + "mode": "optimized", + "pair": 3, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 99.17371076000018 + }, + { + "cpu_seconds": 166.14105600000016, + "mode": "baseline", + "pair": 3, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 166.16592618400045 + }, + { + "cpu_seconds": 170.07685900000004, + "mode": "baseline", + "pair": 4, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 170.10126134999973 + }, + { + "cpu_seconds": 123.13955799999988, + "mode": "optimized", + "pair": 4, + "stderr_sha256": "6bf6ce2a0a5b7ab77259410f10f7279f551cb0073ae125ca8b269f4c59d6c3fa", + "stdout_sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "wall_seconds": 123.20335827000054 + } + ], + "source_sha256": { + "research/copied-fixed/data-corners.json": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17", + "research/copied-fixed/data_corners.cpp": "406a850d496589cd1216eb709baa84fdd8633048b648f05022ae184d1f279448", + "research/data-corner-production/baseline.cpp": "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44" + }, + "speedup": 1.5398999678118155, + "status": "PASS_IDENTICAL_DATA_CORNER_PRODUCTION_RECEIPTS", + "wall_medians": { + "baseline": 170.10126134999973, + "optimized": 110.46253971399983 + } +} diff --git a/research/data-corner-production/SOURCES.json b/research/data-corner-production/SOURCES.json new file mode 100644 index 0000000000..72785d2302 --- /dev/null +++ b/research/data-corner-production/SOURCES.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/copied-fixed/certificate.json", + "usage": "provenance", + "git_blob": "28e29d9982b0c67a34976df17f6c403be264d7e3", + "sha256": "0b796a06420b9366f96b26b83d84e6c8804f41c5dfe7633c208483f838418889" + }, + { + "path": "research/copied-fixed/data_corners.cpp", + "usage": "provenance", + "git_blob": "251f6c87cca42619a0c1b6d83705df5cad0e9c33", + "sha256": "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44", + "note": "Pairwise-era production bytes at base_commit; working tree carries the cached-column rewrite. Live equivalence uses package baseline.cpp plus working production path." + }, + { + "path": "research/copied-fixed/data-corners.json", + "usage": "input", + "git_blob": "4cb7a2b26fc48afd020b7966c43fd30cf2321514", + "sha256": "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17" + }, + { + "path": "research/data-corner-performance/README.md", + "usage": "provenance", + "git_blob": "ff63513d16a7642fe1e040de080549cc6af3f740", + "sha256": "eaa548973e42e1ca6695fb3d6a8ae3c738ff29a5c4ccd053c9bf44f6eacb545c" + }, + { + "path": "research/data-corner-performance/replay.py", + "usage": "provenance", + "git_blob": "fe66919a4c7eae2d21fa24a07218b840a2933f2d", + "sha256": "ce7cceeabb816d4a70aaa6352d5ba0432ac7dea4f66f903e3af4fa91aa44c822", + "note": "Historical opt-in runner at base; same tip demotes its live pairwise pin." + } + ] +} diff --git a/research/data-corner-production/TASK.json b/research/data-corner-production/TASK.json new file mode 100644 index 0000000000..e7b0ef2d0e --- /dev/null +++ b/research/data-corner-production/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_seed": "a7c4e91f2b8d0653e1f940c7a5d2b8e6", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Can the production historical data-corner checker (research/copied-fixed/data_corners.cpp, exercised by research/copied-fixed/producer.py / make copied-fixed-verify) adopt the per-pivot cached update-column loop from research/data-corner-performance/ so the shipped copied-fixed path is faster while every pair receipt field stays identical?", + "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. Expertise override selected verifier-engineering after profiling leave-alone production rewrites and remaining proved opt-in adapters. Leave-alone objects (joint frames, shared-point, mixed-point, ternary, parity-side, R420 rref/geometry/mutants, frameopt.close, leech_minor, verify_factor, sparse-fusion, joint-dual replay, quadratic-affine for #1076, e8-bit-r420 MANIFEST-only edits) were skipped. The data-corner opt-in adapter already proved ~1.71× with ~169s→99s absolute wall time; production still used the nested column scan. This session wires that equivalent loop into the shipped source and certificate local pin, and demotes the pairwise-era live pin in research/data-corner-performance/.", + "bottleneck_link": "Side result on review throughput: copied-fixed data-corner replay is part of make copied-fixed-verify / community verification. A faster identical receipt does not change kappa or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving production data_corners.cpp change with frozen baseline, identical complete receipts, corruption controls, certificate pin discipline, registered replay and a measured before/after median. Do not invent kappa or reopen leave-alone objects.", + "outcome": "completed", + "evidence": "PASS_DATA_CORNER_PRODUCTION via research/data-corner-production/verify.py (also under -O); PASS_REGISTERED_RESEARCH_PACKAGE; PASS_IDENTICAL_DATA_CORNER_PRODUCTION_RECEIPTS via pinned-CPU benchmark.py --rounds 5 (median 170.101→110.463 s, 1.54×); research/copied-fixed/certificate.json differs from base only in the data_corners.cpp local_sha256 pin; research/data-corner-performance demotes the pairwise-era working-source pin.", + "author": "Wentao Li", + "github": "VictorLiwentao", + "email": "wentaol4@illinois.edu", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, packaging, benchmarking and writing. Not independent human peer review.", + "open_questions": [ + { + "question": "Should adjacent historical copies under research/pair-assembly/, research/skip-strips/, and research/split-skip/ adopt the same cached columns in a follow-up tip?", + "why_it_matters": "Those trees still pin pairwise-era digests without a registered VERIFY matrix; a coordinated refresh would remove stale inventory digests without changing receipts.", + "first_step": "Diff each data_corners.cpp against the production transform site and list which SOURCE inventories would need provenance demotion.", + "blocked_by": "Out of this session's one-object stop rule." + }, + { + "question": "Should make copied-fixed-verify grow a microbenchmark gate for the full 4,073,300-pair replay?", + "why_it_matters": "A future edit could restore the nested scan without failing equivalence tests.", + "first_step": "Decide whether RESULT.json medians belong in CI or remain descriptive.", + "blocked_by": "Maintainer CI-budget preference." + } + ] +} diff --git a/research/data-corner-production/VERIFY.json b/research/data-corner-production/VERIFY.json new file mode 100644 index 0000000000..a67033745e --- /dev/null +++ b/research/data-corner-production/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/copied-fixed/data_corners.cpp", + "research/copied-fixed/data-corners.json", + "research/copied-fixed/certificate.json", + "research/data-corner-production/baseline.cpp" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Exact baseline copy of the base-commit data_corners.cpp; production equals transform(baseline); identical complete receipts vs pinned data-corners.json; temp-copy column-fill corruption control; certificate differs from base only in the data_corners.cpp local_sha256 pin; duplicate JSON-key check; read-only default." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Same equivalence and pin discipline under -O (require() gates remain; C++ children still assert because NDEBUG is rejected)." + } + ] +} diff --git a/research/data-corner-production/baseline.cpp b/research/data-corner-production/baseline.cpp new file mode 100644 index 0000000000..251f6c87cc --- /dev/null +++ b/research/data-corner-production/baseline.cpp @@ -0,0 +1,77 @@ +// Exhaustive rational nonvanishing certificates via a proved finite prime. +// Adapted from Rohan Arun PR39 geometry.cpp, with James Chang PR34's pivots. +// Both factors are now fixed I+J; every one of the 4,073,300 triple pairs is +// checked. A failed residue test gets a charged 47-singleton fallback. +// Zero identities are proved separately by the inherited exact rank cuts. +// Apache-2.0. Prepared with OpenAI Codex assistance. +#include +#include +#include +#include +#include +using namespace std; +constexpr int prime=1000003,a=23,b=25,d=47; +int mul(int x,int y){return int(int64_t(x)*y%prime);} +int power(int x,int n){int z=1;for(;n;n>>=1,x=mul(x,x))if(n&1)z=mul(z,x);return z;} +int main(){ + for(int i=2;i*i<=prime;++i)assert(prime%i); + vector R,C,piv; + for(int i=0;i> rejected; + cout<<"{\"prime\":"< None: + path = output.with_suffix(".cpp") + path.write_text(GUARD + source, encoding="utf-8") + subprocess.run( + [*compiler, "-O3", "-std=c++17", str(path), "-o", str(output)], + check=True, + capture_output=True, + ) + + +def timed_run(executable: Path, expected: dict) -> dict: + before = resource.getrusage(resource.RUSAGE_CHILDREN) + start = time.perf_counter() + result = subprocess.run([str(executable)], capture_output=True, check=True) + wall = time.perf_counter() - start + after = resource.getrusage(resource.RUSAGE_CHILDREN) + require(json.loads(result.stdout) == expected, "receipt mismatch during benchmark") + return dict( + wall_seconds=wall, + cpu_seconds=(after.ru_utime + after.ru_stime - before.ru_utime - before.ru_stime), + stdout_sha256=sha256(result.stdout).hexdigest(), + stderr_sha256=sha256(result.stderr).hexdigest(), + ) + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--out", type=Path, required=True) + args = parser.parse_args(argv) + require(args.rounds >= 1, "need at least one round") + require(not args.out.exists(), "output already exists") + + baseline = (PACKAGE / "baseline.cpp").read_text(encoding="utf-8") + production = PRODUCTION.read_text(encoding="utf-8") + expected = json.loads(RECEIPT.read_text(encoding="utf-8")) + compiler = shlex.split(os.environ.get("CXX", "c++")) + version = subprocess.check_output([*compiler, "--version"], text=True) + + samples = [] + with tempfile.TemporaryDirectory(prefix="data-corner-bench-") as tmp: + work = Path(tmp) + compile_program(baseline, work / "baseline", compiler) + compile_program(production, work / "optimized", compiler) + for round_index in range(args.rounds): + order = ( + ("baseline", "optimized") + if round_index % 2 == 0 + else ("optimized", "baseline") + ) + for engine in order: + sample = timed_run(work / engine, expected) + samples.append(dict(pair=round_index, mode=engine, **sample)) + print( + f"PASS pair={round_index} {engine} wall={sample['wall_seconds']:.3f}s", + flush=True, + ) + + medians = { + mode: statistics.median(s["wall_seconds"] for s in samples if s["mode"] == mode) + for mode in ("baseline", "optimized") + } + report = dict( + status="PASS_IDENTICAL_DATA_CORNER_PRODUCTION_RECEIPTS", + base_commit="0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + rounds=args.rounds, + platform=platform.platform(), + python=platform.python_version(), + compiler=compiler, + compiler_version=version, + flags=["-O3", "-std=c++17"], + source_sha256={ + "research/data-corner-production/baseline.cpp": sha256( + (PACKAGE / "baseline.cpp").read_bytes() + ).hexdigest(), + "research/copied-fixed/data_corners.cpp": sha256(PRODUCTION.read_bytes()).hexdigest(), + "research/copied-fixed/data-corners.json": sha256(RECEIPT.read_bytes()).hexdigest(), + }, + wall_medians=medians, + speedup=medians["baseline"] / medians["optimized"], + coverage={ + k: expected[k] + for k in ("pairs", "good", "fallback", "nonzero_pivots", "ordered_zero_checks") + }, + samples=samples, + ) + args.out.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print("PASS_IDENTICAL_DATA_CORNER_PRODUCTION_RECEIPTS") + print( + f"median baseline={medians['baseline']:.3f}s " + f"optimized={medians['optimized']:.3f}s " + f"speedup={report['speedup']:.3f}x" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/data-corner-production/verify.py b/research/data-corner-production/verify.py new file mode 100644 index 0000000000..47df92d3e0 --- /dev/null +++ b/research/data-corner-production/verify.py @@ -0,0 +1,200 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and rejection controls for production data-corner columns. + +Read-only by default. Regenerates no certificate unless --write-certificate is +passed. Timing is not a pass gate; see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +from copy import deepcopy +from hashlib import sha256 +import json +import os +from pathlib import Path +import shlex +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +PRODUCTION = ROOT / "research" / "copied-fixed" / "data_corners.cpp" +RECEIPT = ROOT / "research" / "copied-fixed" / "data-corners.json" +CERTIFICATE = ROOT / "research" / "copied-fixed" / "certificate.json" + +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ORIGINAL_BLOB = "251f6c87cca42619a0c1b6d83705df5cad0e9c33" +ORIGINAL_SHA256 = "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44" +BASE_CERTIFICATE_SHA256 = "0b796a06420b9366f96b26b83d84e6c8804f41c5dfe7633c208483f838418889" +RECEIPT_SHA256 = "82dc2d3e116fc003348d6e9ff0cce90fd70d3d6c156580b769ff3d38b3399e17" + +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 str: + return sha256(path.read_bytes()).hexdigest() + + +def unique_object(pairs): + out = {} + for key, value in pairs: + require(key not in out, f"duplicate JSON key: {key}") + out[key] = value + return out + + +def load_json_unique(path: Path): + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_object) + + +def transform(source: str) -> str: + for old, new in ((OLD_INVERSE, NEW_INVERSE), (OLD_UPDATE, NEW_UPDATE)): + require(source.count(old) == 1, "Expected exactly one update site: " + old[:40]) + source = source.replace(old, new) + return source + + +def compile_program(source: str, output: Path, compiler: list[str]) -> None: + path = output.with_suffix(".cpp") + path.write_text(GUARD + source, encoding="utf-8") + subprocess.run( + [*compiler, "-O3", "-std=c++17", str(path), "-o", str(output)], + check=True, + capture_output=True, + ) + + +def run_program(executable: Path) -> bytes: + result = subprocess.run([str(executable)], capture_output=True, check=True) + return result.stdout + + +def check_baseline_bytes() -> bytes: + original = subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:research/copied-fixed/data_corners.cpp"], + cwd=ROOT, + ) + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base data_corners.cpp sha256 drift") + require( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:research/copied-fixed/data_corners.cpp"], + cwd=ROOT, + ) + .decode() + .strip() + == ORIGINAL_BLOB, + "base data_corners.cpp blob drift", + ) + require( + (PACKAGE / "baseline.cpp").read_bytes() == original, + "baseline.cpp must be an exact copy of the base-commit source", + ) + return original + + +def check_production_transform(original: bytes) -> str: + production = PRODUCTION.read_text(encoding="utf-8") + expected = transform(original.decode("utf-8")) + require(production == expected, "production data_corners.cpp != transform(baseline)") + require("columns[d],length=0" in production, "cached column list missing") + require(production.count(OLD_UPDATE) == 0, "pairwise update loop still present") + return production + + +def check_receipt_equivalence(original_source: str, production_source: str) -> dict: + require(digest_file(RECEIPT) == RECEIPT_SHA256, "data-corners.json receipt drift") + expected = load_json_unique(RECEIPT) + compiler = shlex.split(os.environ.get("CXX", "c++")) + with tempfile.TemporaryDirectory(prefix="data-corner-prod-") as tmp: + work = Path(tmp) + compile_program(original_source, work / "original", compiler) + compile_program(production_source, work / "optimized", compiler) + original_out = run_program(work / "original") + optimized_out = run_program(work / "optimized") + require(original_out == optimized_out, "baseline/production stdout bytes differ") + require(json.loads(optimized_out) == expected, "production receipt differs from pinned JSON") + return expected + + +def check_temp_corruption(production_source: str) -> str: + """Mutate the cached-column fill in a temp copy; expect receipt mismatch or abort.""" + with tempfile.TemporaryDirectory(prefix="data-corner-corrupt-") as tmp: + work = Path(tmp) + mutant_source = production_source.replace( + "if(available[j]&&M[i][j])columns[length++]=j;", + "if(available[j]&&M[i][j]&&j>c)columns[length++]=j;", + 1, + ) + require(mutant_source != production_source, "corruption edit did not change source") + compiler = shlex.split(os.environ.get("CXX", "c++")) + compile_program(production_source, work / "honest", compiler) + compile_program(mutant_source, work / "mutant", compiler) + honest = run_program(work / "honest") + proc = subprocess.run([str(work / "mutant")], capture_output=True, check=False) + if proc.returncode != 0: + return "subprocess_failure" + require(proc.stdout != honest, "corruption preserved the complete receipt") + return "receipt_mismatch" + + +def check_certificate(write: bool) -> None: + path = CERTIFICATE + if write: + # Recompute only the local_sha256 entry for data_corners.cpp. + cert = load_json_unique(path) + cert["local_sha256"]["research/copied-fixed/data_corners.cpp"] = digest_file(PRODUCTION) + path.write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n", encoding="utf-8") + committed = path.read_text(encoding="utf-8") + load_json_unique(path) + base = subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:research/copied-fixed/certificate.json"], + cwd=ROOT, + ) + require(sha256(base).hexdigest() == BASE_CERTIFICATE_SHA256, "base certificate sha256 drift") + old = json.loads(base.decode("utf-8")) + new = json.loads(committed) + old_pin = old["local_sha256"].pop("research/copied-fixed/data_corners.cpp") + new_pin = new["local_sha256"].pop("research/copied-fixed/data_corners.cpp") + require(old_pin == ORIGINAL_SHA256, "unexpected base local pin") + require(new_pin == digest_file(PRODUCTION), "certificate pin != working source") + require(old == new, "certificate changed outside the single data_corners.cpp local_sha256 pin") + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write-certificate", + action="store_true", + help="rewrite research/copied-fixed/certificate.json local pin (default: read-only)", + ) + args = parser.parse_args(argv) + + original = check_baseline_bytes() + production = check_production_transform(original) + expected = check_receipt_equivalence(original.decode("utf-8"), production) + corruption = check_temp_corruption(production) + check_certificate(write=args.write_certificate) + print( + "PASS_DATA_CORNER_PRODUCTION " + f"pairs={expected['pairs']} good={expected['good']} " + f"fallback={expected['fallback']} corruption={corruption} " + "certs=1 no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/test_data_corner_production.py b/tests/test_data_corner_production.py new file mode 100644 index 0000000000..5367c4c9d9 --- /dev/null +++ b/tests/test_data_corner_production.py @@ -0,0 +1,78 @@ +#!/usr/bin/env python3 +"""Focused controls for the production data-corner cached-column package.""" +from __future__ import annotations + +from copy import deepcopy +from hashlib import sha256 +import json +import subprocess +import unittest +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[1] +PACKAGE = ROOT / "research" / "data-corner-production" + +ORIGINAL_SHA256 = "d134f43d31b896daf504511991be8608c6ba9d20a6606c57e2e12d4b203b7d44" +PRODUCTION_SHA256 = "406a850d496589cd1216eb709baa84fdd8633048b648f05022ae184d1f279448" +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" + + +class DataCornerProductionTests(unittest.TestCase): + def test_baseline_matches_base_commit_bytes(self): + original = subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:research/copied-fixed/data_corners.cpp"], + cwd=ROOT, + ) + self.assertEqual((PACKAGE / "baseline.cpp").read_bytes(), original) + self.assertEqual(sha256(original).hexdigest(), ORIGINAL_SHA256) + self.assertEqual( + sha256((ROOT / "research/copied-fixed/data_corners.cpp").read_bytes()).hexdigest(), + PRODUCTION_SHA256, + ) + self.assertNotEqual(PRODUCTION_SHA256, ORIGINAL_SHA256) + + def test_certificate_only_changes_data_corners_local_pin(self): + base = json.loads( + subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:research/copied-fixed/certificate.json"], + cwd=ROOT, + ) + ) + live = json.loads( + (ROOT / "research/copied-fixed/certificate.json").read_text(encoding="utf-8") + ) + self.assertEqual( + live["local_sha256"]["research/copied-fixed/data_corners.cpp"], + PRODUCTION_SHA256, + ) + restored = deepcopy(live) + restored["local_sha256"]["research/copied-fixed/data_corners.cpp"] = ORIGINAL_SHA256 + self.assertEqual(restored, base) + + def test_performance_package_vendors_baseline_and_tracks_production(self): + manifest = json.loads( + (ROOT / "research/data-corner-performance/SOURCE.json").read_text(encoding="utf-8") + ) + self.assertEqual( + manifest["sha256"]["research/data-corner-performance/baseline.cpp"], + ORIGINAL_SHA256, + ) + self.assertEqual( + manifest["sha256"]["research/copied-fixed/data_corners.cpp"], + PRODUCTION_SHA256, + ) + self.assertEqual( + manifest["provenance_sha256"]["research/copied-fixed/data_corners.cpp@pre-production"], + ORIGINAL_SHA256, + ) + self.assertEqual( + sha256( + (ROOT / "research/data-corner-performance/baseline.cpp").read_bytes() + ).hexdigest(), + ORIGINAL_SHA256, + ) + + +if __name__ == "__main__": + unittest.main()