diff --git a/research/dic3-shift-table-replay/MEASUREMENTS.json b/research/dic3-shift-table-replay/MEASUREMENTS.json new file mode 100644 index 0000000000..69c9819371 --- /dev/null +++ b/research/dic3-shift-table-replay/MEASUREMENTS.json @@ -0,0 +1,188 @@ +{ + "schema": "dic3-shift-benchmark/v1", + "samples": [ + { + "baseline": true, + "elapsed_ns": 8703674917, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py", + "--baseline" + ] + }, + { + "baseline": false, + "elapsed_ns": 5255297125, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py" + ] + }, + { + "baseline": true, + "elapsed_ns": 9010664000, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py", + "--baseline" + ] + }, + { + "baseline": false, + "elapsed_ns": 5738952459, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py" + ] + }, + { + "baseline": true, + "elapsed_ns": 8699651375, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py", + "--baseline" + ] + }, + { + "baseline": false, + "elapsed_ns": 5142203750, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py" + ] + }, + { + "baseline": true, + "elapsed_ns": 9105424291, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py", + "--baseline" + ] + }, + { + "baseline": false, + "elapsed_ns": 5884180042, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py" + ] + }, + { + "baseline": true, + "elapsed_ns": 8585229791, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py", + "--baseline" + ] + }, + { + "baseline": false, + "elapsed_ns": 5058665541, + "returncode": 0, + "stderr_bytes": 0, + "stdout_sha256": "215612ee4088458105764a46f3801e1e9b8fe4a4bf7b615a18f80e2f50870875", + "command": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-I", + "-W", + "error", + "-B", + "/Users/nick/git/imb-research-7/research/dic3-shift-table-replay/replay.py" + ] + } + ], + "baseline": { + "median_ns": 8703674917, + "min_ns": 8585229791, + "max_ns": 9105424291 + }, + "prepared": { + "median_ns": 5255297125, + "min_ns": 5058665541, + "max_ns": 5884180042 + }, + "reduction_fraction": 0.39619790776705544, + "errors": 0, + "identical_complete_outputs": 10, + "stdout": "PASS_DIC3_BOUNDED_DIAGONAL_SEARCH ops=56 pair_states=2409 triple_states=94727 depth4_endpoints=1482 depth5_endpoints=1230 depth4_hits=0 depth5_hits=0 coverage4=a1398353921f55628c8329852554a6538f2a075eccc51ae127e25bfc791727f3 coverage5=816765d363f764fdaf4b3cbe4f1bc10ed235fc664924ea11a4112046d2157a1b\n", + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "machine": "arm64", + "cpu_count": 18, + "load_average_at_end": [ + 3.82958984375, + 3.0390625, + 2.30859375 + ], + "source_hashes": { + "replay.py": "bc8da3e823b98f2810a6f52ccb55eb1f32e64d248ad4721649f1e97c3dc3ae95", + "benchmark.py": "b856af72d1d97cacb190a01b10d406e566464ea89140adb23ca348335b389096", + "SOURCES.json": "8b64563672ef974790fec59721f9497fda73603acca38e1087f6c42c1ee4dee5" + } +} diff --git a/research/dic3-shift-table-replay/PROFILE.json b/research/dic3-shift-table-replay/PROFILE.json new file mode 100644 index 0000000000..f077a8dbcd --- /dev/null +++ b/research/dic3-shift-table-replay/PROFILE.json @@ -0,0 +1,112 @@ +{ + "profile": "complete original verify.py command, separate from timing samples", + "total_seconds": 21.962037332999994, + "functions": [ + { + "file": "search.py", + "line": 148, + "function": "right_monomial_shift", + "primitive_calls": 58798872, + "calls": 58798872, + "self_seconds": 7.742912155000001, + "cumulative_seconds": 9.857434091 + }, + { + "file": "search.py", + "line": 195, + "function": "", + "primitive_calls": 65332080, + "calls": 65332080, + "self_seconds": 6.1734341090000004, + "cumulative_seconds": 16.0308682 + }, + { + "file": "search.py", + "line": 84, + "function": "", + "primitive_calls": 1120, + "calls": 1120, + "self_seconds": 3.812e-05, + "cumulative_seconds": 3.812e-05 + }, + { + "file": "search.py", + "line": 188, + "function": "", + "primitive_calls": 13824, + "calls": 13824, + "self_seconds": 0.0009715640000000001, + "cumulative_seconds": 0.0009715640000000001 + }, + { + "file": "search.py", + "line": 28, + "function": "", + "primitive_calls": 13, + "calls": 13, + "self_seconds": 5.084e-06, + "cumulative_seconds": 1.0248e-05 + }, + { + "file": "search.py", + "line": 26, + "function": "", + "primitive_calls": 156, + "calls": 156, + "self_seconds": 1.2459e-05, + "cumulative_seconds": 2.7168e-05 + }, + { + "file": "search.py", + "line": 71, + "function": "", + "primitive_calls": 280, + "calls": 280, + "self_seconds": 3.6714e-05, + "cumulative_seconds": 3.6714e-05 + }, + { + "file": "search.py", + "line": 179, + "function": "search_domain", + "primitive_calls": 2, + "calls": 2, + "self_seconds": 3.728927634, + "cumulative_seconds": 20.475300375 + } + ], + "inputs_sha256": { + "EXPECTED.json": "4d6328e45fdc691834824dff8a2c31049c8ff1dd7eada3063ddd19e16cb169e7", + "search.py": "ef90932a6d28bd2dc459fb02681a5cc376b4fc88ee3788db558beab129593e04", + "verify.py": "6502484b0a7b7932d97963083a52b4a16c041561259b380c210342869c4f6951" + }, + "candidate_profile": { + "total_seconds": 12.420828617999987, + "functions": [ + { + "file": "replay.py", + "line": 83, + "function": "prepared_shift", + "calls": 58798872, + "self_seconds": 1.6327811030000001, + "cumulative_seconds": 1.6327811030000001 + }, + { + "file": "search.py", + "line": 195, + "function": "", + "calls": 65332080, + "self_seconds": 5.41832988, + "cumulative_seconds": 7.051110983 + }, + { + "file": "search.py", + "line": 179, + "function": "search_domain", + "calls": 2, + "self_seconds": 3.397297855, + "cumulative_seconds": 10.967569084 + } + ] + } +} diff --git a/research/dic3-shift-table-replay/README.md b/research/dic3-shift-table-replay/README.md new file mode 100644 index 0000000000..22cd81187c --- /dev/null +++ b/research/dic3-shift-table-replay/README.md @@ -0,0 +1,150 @@ +# Prepared coefficient permutations for the complete Dic3 replay + +This contribution was produced by Nick Petalas. Apache-2.0. + +The complete retained PR2069 command takes **39.62% less median wall time +locally**, from 8.703675 s to 5.255297 s, by replacing repeated coefficient-bit +scans with a prepared table of 49,152 integers. The original search, endpoint +domain, raw-word controls, saved certificate and printed mathematical result +remain unchanged. This is an implementation-preservation proof with exact +finite conformance and local performance evidence. It supplies no new +mathematical endpoint, multiplication theorem or kappa. + +Baseline range is 8.585230 to 9.105424 s; candidate range is 5.058666 to +5.884180 s. Five alternating fresh-process pairs ran on CPython 3.12.15, +macOS arm64. Every candidate beat every baseline. All ten commands succeeded +with empty stderr and identical complete output. Shared-host background load +was uncontrolled; the initial load averages were 2.80, 2.71, 2.03 on 18 CPUs. + +The separate profile records 58,798,872 calls to the old shift function and +64,868,328 iterations of its bit scan. That function consumes 9.857 of 21.962 +profiled seconds. Preparation uses 49,140 recurrence steps; every subsequent +shift is two tuple lookups. [MEASUREMENTS.json](MEASUREMENTS.json) contains all +ten complete fresh-process samples and their identical output hashes. Timing +includes process startup, source authentication, source execution, table +preparation, both complete searches, all original controls and output capture. + +The benchmark compares the same authenticated driver with its single optional +replacement enabled or disabled. Both modes call the unchanged original +`main`. Each process starts with an empty original ring-product cache. The +profile is a separate run and is excluded from the reported samples. + +## Preservation argument + +Represent a coefficient of `F2[Dic3]` by a twelve-bit integer. For group element +g, right multiplication permutes its bits by `i -> i*g`. Let `T[g,m]` be that +permuted mask. Then + +```text +T[g,0] = 0 +T[g,m] = T[g,m xor b] xor (1 << ((index b)*g)), b = m & -m. +``` + +The smaller mask `m xor b` has already been prepared. Induction on m proves +that each table entry equals the original set-bit loop, including zero. +Right multiplication is a bijection, so no support bit disappears or changes +its multiplicity. All results are the same built-in Python integers. + +The authenticated caller supplies only `0 <= m < 4096` and `0 <= g < 12`. +Its initial coefficients are zero or group basis bits; ring multiplication, +matrix multiplication and XOR preserve the mask range. Endpoint elements come +from `range(12)`. Thus direct table indexing covers every reached call. This +internal replacement is not a new public API for negative or oversized masks. + +`replay.py` authenticates all three executable/data inputs before loading either +source. It executes their exact bytes, binds the original checker's `search` +import to that fresh module, and replaces only `right_monomial_shift`. The +original function is pure and has no cache or I/O effects. Every subsequent +operation therefore receives the same value and type. Dictionary insertion +order, shortest representatives, join lookups, endpoint ordering, rejection +controls and complete output are preserved. No result table substitutes for +a search. The checkout must remain stable while a command runs. + +## Reproduce + +From the repository root, CPython 3.12 and its standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dic3-shift-table-replay/replay.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dic3-shift-table-replay/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/dic3-shift-table-replay/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dic3-shift-table-replay +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dic3-shift-table-replay --check-source-history +``` + +Another CPython 3.12 path may replace the local interpreter. The complete replay +prints the unchanged `PASS_DIC3_BOUNDED_DIAGONAL_SEARCH` line. The conformance +command additionally prints `PASS_DIC3_SHIFT_TABLE_REPLAY` in a generated JSON +receipt bound to all package files. It checks all 49,152 coefficients against +both the old implementation and an independent normal-form formula, all +589,824 group-action compositions, and nine named rejection/distinction +controls. Changed or missing source files reject before source execution. +Correctness checks use explicit exceptions and remain active under `-O`. + +To repeat the local timing experiment, use a fresh external output path: + +```sh +python3.12 -I -W error -B research/dic3-shift-table-replay/benchmark.py --output /tmp/dic3-measurement-new.json +``` + +The benchmark performs five alternating baseline/candidate pairs, with a +120-second bound per complete command. It fails on any nonzero exit, stderr, +missing completion marker or changed complete output. Timing evidence is +local, and the registered replay imposes no portable speed threshold. + +## Scope and credit + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected PR6030. The `replay-runtime` card is refined to one complete pinned +command; its source-binding first example passed. Live open/account PRs, +recent handoffs, active Discussions, merged searches and main object/formula +searches were checked. The cached overlap scan reports sparse local notes +and possibly stale remote coverage. Unpublished work and arbitrary historical +diffs remain outside that coverage. No same-command competing optimization was +found within it. + +Cinna Davis / 1337isnot1337's [PR2069](https://github.com/CrocSwap/integer-mult-bounds/pull/2069) +retains the search, proof, certificate and original controls. David Govea's +PR720, eumemic's PR288 and the retained register-model lineage keep their +credit. Nick Petalas's older PR5205 concerns a different six-call mathematical +layer; it is neither extended nor replayed here. Finite lookup tables and +bit-permutation recurrences are classical. The new contribution is this +source-bound optional implementation, its preservation proof and complete +command measurements. No global algorithm-priority claim is made. + +No predecessor source, frozen evidence, shared verifier or selected-frontier +file is changed. Native operations, physical callers, compiler, restoration, +precision/tape, stock and outer admission remain outside scope. Selected cold +replay, Lean and Docker are unrun. Independent human and formal proof-kernel +review are unclaimed. Successful execution of the retained checker is +conformance evidence, not a new audit deliverable or scientific acceptance. + +## Code constraints + +The new table has exactly twelve rows of 4,096 entries. Preparation has 49,140 +iterations; coefficient comparison has 49,152 and composition comparison +589,824. The benchmark launches exactly ten serial children, each bounded by +120 seconds. Source inputs are three regular files of at most 65,536 bytes. +There is no recursion. New functions fit within 60 physical lines. The only +module replacement is temporary, process-local and restored in `finally`. +The installed callable owns an immutable table for that module's lifetime. +Warning-strict normal and optimized executions provide runtime diagnostics. + +Power of Ten rule 3 has a CPython managed-allocation deviation for bounded +integers, tuples and original source objects. The additional prepared state +is 49,152 integer references plus tuple headers, with each value below 4096; +one row and twelve images are live during construction. Original search-state +and ring-cache limits are inherited unchanged from the finite command. +Rules 8 and 9 have a source-loading/dispatch deviation: exactly two pinned, +size-bounded Python modules execute through `compile`/`exec`, and one named +pure function is replaced. Authentication and the complete finite conformance +domain constrain these operations. A future native deployment requiring fixed +allocation or static dispatch would need a separate implementation. No such +deployment is supplied or implied here. + +## Open next questions + +Should a future default replay adopt this table? First define how immutable +historical source pins are retained while making the optimized command the +entry point. Adoption and its invalidation policy are not implemented here. +No further search layer or optimization is reserved. diff --git a/research/dic3-shift-table-replay/SOURCES.json b/research/dic3-shift-table-replay/SOURCES.json new file mode 100644 index 0000000000..a6cf757ada --- /dev/null +++ b/research/dic3-shift-table-replay/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-dicyclic-diagonal-seed620ca/EXPECTED.json", + "usage": "input", + "git_blob": "1ac1f22370a40cc422bb4dfe8f07379436611fa2", + "sha256": "4d6328e45fdc691834824dff8a2c31049c8ff1dd7eada3063ddd19e16cb169e7" + }, + { + "path": "research/bit-dicyclic-diagonal-seed620ca/search.py", + "usage": "input", + "git_blob": "63a68d7ee804d5d23e394e063fabbafef5106518", + "sha256": "ef90932a6d28bd2dc459fb02681a5cc376b4fc88ee3788db558beab129593e04" + }, + { + "path": "research/bit-dicyclic-diagonal-seed620ca/verify.py", + "usage": "input", + "git_blob": "270a3d1ab9b2bcc2e28f81f0f92d44c9fa302bb8", + "sha256": "6502484b0a7b7932d97963083a52b4a16c041561259b380c210342869c4f6951" + } + ] +} diff --git a/research/dic3-shift-table-replay/TASK.json b/research/dic3-shift-table-replay/TASK.json new file mode 100644 index 0000000000..25984c7f50 --- /dev/null +++ b/research/dic3-shift-table-replay/TASK.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Preserve the entire pinned PR2069 default replay while preparing the finite right-monomial coefficient permutations once per process.", + "scope_change_reason": "The replay-runtime card is refined to its measured repeated coefficient-bit scan; no mathematical search domain is extended.", + "bottleneck_link": "Faster complete exact replays reduce review friction while retaining every original check and source invalidation.", + "budget_minutes": 60, + "stop_rule": "Stop after the first complete-command improvement with identical output, exhaustive permutation conformance and bounded failure controls.", + "outcome": "completed", + "evidence": "Five alternating fresh-process pairs: median 8.703674917 s to 5.255297125 s, 39.6197907767 percent reduction, ten identical complete outputs, zero failures. All 49152 coefficient and 589824 composition cases are checked.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Should the prepared table become a future default replay entry point?", + "why_it_matters": "It could remove the repeated coefficient scans for future consumers while preserving immutable source history.", + "first_step": "Specify the exact default-entry migration and retain the historical command and pins.", + "blocked_by": "No default-adoption or historical-source migration contract is implemented." + } + ] +} diff --git a/research/dic3-shift-table-replay/VERIFY.json b/research/dic3-shift-table-replay/VERIFY.json new file mode 100644 index 0000000000..28c5549380 --- /dev/null +++ b/research/dic3-shift-table-replay/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-dicyclic-diagonal-seed620ca/EXPECTED.json", + "research/bit-dicyclic-diagonal-seed620ca/search.py", + "research/bit-dicyclic-diagonal-seed620ca/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 49152 old/literal/prepared coefficient values, 589824 action compositions, source corruption and group/coefficient controls, timing-record bindings, and the unchanged complete original default replay." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete conformance and original scientific command with optimized Python; explicit exceptions retain every new check." + } + ] +} diff --git a/research/dic3-shift-table-replay/benchmark.py b/research/dic3-shift-table-replay/benchmark.py new file mode 100644 index 0000000000..408dc4d3c8 --- /dev/null +++ b/research/dic3-shift-table-replay/benchmark.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python3 +"""Time five alternating pairs of complete authenticated Dic3 replays.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def one_run(baseline: bool) -> tuple[dict, bytes]: + command = [sys.executable, "-I", "-W", "error", "-B", str(PACKAGE / "replay.py")] + if baseline: + command.append("--baseline") + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + start = time.perf_counter_ns() + result = subprocess.run(command, cwd=ROOT, env=env, capture_output=True, + timeout=120, check=False) + elapsed = time.perf_counter_ns() - start + row = {"baseline": baseline, "elapsed_ns": elapsed, + "returncode": result.returncode, "stderr_bytes": len(result.stderr), + "stdout_sha256": hashlib.sha256(result.stdout).hexdigest(), + "command": command} + if result.returncode or result.stderr: + raise RuntimeError("complete replay failed: " + repr(row) + + result.stderr.decode(errors="replace")) + if not result.stdout.startswith(b"PASS_DIC3_BOUNDED_DIAGONAL_SEARCH "): + raise RuntimeError("complete replay omitted its scientific result") + return row, result.stdout + + +def measure() -> dict: + samples = [] + reference = None + for index in range(10): + row, output = one_run(index % 2 == 0) + if reference is None: + reference = output + if output != reference: + raise RuntimeError("complete scientific output changed") + samples.append(row) + print(index + 1, row["baseline"], row["elapsed_ns"], flush=True) + groups = [[r["elapsed_ns"] for r in samples if r["baseline"] == side] + for side in (True, False)] + summaries = [{"median_ns": statistics.median(g), "min_ns": min(g), + "max_ns": max(g)} for g in groups] + return {"schema": "dic3-shift-benchmark/v1", "samples": samples, + "baseline": summaries[0], "prepared": summaries[1], + "reduction_fraction": 1 - summaries[1]["median_ns"] / summaries[0]["median_ns"], + "errors": 0, "identical_complete_outputs": 10, + "stdout": reference.decode(), "python": sys.version, + "platform": platform.platform(), "machine": platform.machine(), + "cpu_count": os.cpu_count(), "load_average_at_end": os.getloadavg(), + "source_hashes": {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in ("replay.py", "benchmark.py", "SOURCES.json")}} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", required=True, type=Path) + args = parser.parse_args() + if args.output.resolve().is_relative_to(ROOT): + parser.error("write measurements outside the checkout") + if args.output.exists(): + parser.error("output must be a new file") + result = measure() + with args.output.open("x") as stream: + stream.write(json.dumps(result, indent=2) + "\n") + print("PASS_DIC3_SHIFT_BENCHMARK", result["reduction_fraction"]) + + +if __name__ == "__main__": + main() diff --git a/research/dic3-shift-table-replay/replay.py b/research/dic3-shift-table-replay/replay.py new file mode 100644 index 0000000000..f384df089f --- /dev/null +++ b/research/dic3-shift-table-replay/replay.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Run the unchanged Dic3 checker with one prepared coefficient permutation.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +from pathlib import Path +import sys +import types + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = "research/bit-dicyclic-diagonal-seed620ca/" +INPUTS = tuple(SOURCE + name for name in ("search.py", "verify.py", "EXPECTED.json")) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def source_bytes(root: Path = ROOT) -> dict[str, bytes]: + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + require({row["path"] for row in rows} == set(INPUTS), "source inventory changed") + require(len(rows) == 3, "duplicate source pin") + payloads = {} + for row in rows: + path = root / row["path"] + require(path.is_file() and not path.is_symlink(), "missing regular input") + require(path.stat().st_size <= 65536, "source size exceeds bound") + payload = path.read_bytes() + require(hashlib.sha256(payload).hexdigest() == row["sha256"], + "source digest mismatch: " + row["path"]) + payloads[row["path"]] = payload + return payloads + + +def load_sources(root: Path = ROOT) -> tuple[types.ModuleType, types.ModuleType]: + payloads = source_bytes(root) + search = types.ModuleType("dic3_pinned_search") + search.__file__ = str(root / (SOURCE + "search.py")) + exec(compile(payloads[SOURCE + "search.py"], search.__file__, "exec"), + search.__dict__) + checker = types.ModuleType("dic3_pinned_checker") + checker.__file__ = str(root / (SOURCE + "verify.py")) + previous = sys.modules.get("search") + sys.modules["search"] = search + try: + exec(compile(payloads[SOURCE + "verify.py"], checker.__file__, "exec"), + checker.__dict__) + finally: + if previous is None: + del sys.modules["search"] + else: + sys.modules["search"] = previous + require(checker.search is search, "checker did not bind the pinned search") + return search, checker + + +def shift_tables(group: tuple[tuple[int, ...], ...]) -> tuple[tuple[int, ...], ...]: + require(len(group) == 12 and all(len(row) == 12 for row in group), + "expected twelve group elements") + require(all(sorted(row[g] for row in group) == list(range(12)) + for g in range(12)), "right translation is not a permutation") + tables = [] + for g in range(12): + row = [0] * 4096 + images = tuple(1 << group[i][g] for i in range(12)) + for mask in range(1, 4096): + bit = mask & -mask + row[mask] = row[mask ^ bit] ^ images[bit.bit_length() - 1] + tables.append(tuple(row)) + return tuple(tables) + + +def install(search: types.ModuleType) -> tuple[tuple[int, ...], ...]: + tables = shift_tables(search.GROUP_TABLE) + + def prepared_shift(mask: int, g: int) -> int: + # The authenticated caller supplies 0<=mask<4096 and 0<=g<12. + return tables[g][mask] + + search.right_monomial_shift = prepared_shift + return tables + + +def run(baseline: bool = False) -> None: + search, checker = load_sources() + if not baseline: + install(search) + checker.main() + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--baseline", action="store_true") + args = parser.parse_args() + run(args.baseline) + + +if __name__ == "__main__": + main() diff --git a/research/dic3-shift-table-replay/verify.py b/research/dic3-shift-table-replay/verify.py new file mode 100644 index 0000000000..160a4da874 --- /dev/null +++ b/research/dic3-shift-table-replay/verify.py @@ -0,0 +1,135 @@ +#!/usr/bin/env python3 +"""Check all prepared permutations, source rejection, and the complete replay.""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path +import statistics +import sys +import tempfile + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +import replay + + +def literal_shift(mask: int, g: int) -> int: + k, ell = g % 6, g // 6 + out = 0 + for i in range(12): + if (mask >> i) & 1: + j, bit = i % 6, i // 6 + power = (j + (k if bit == 0 else -k) + 3 * bit * ell) % 6 + out ^= 1 << (power + 6 * ((bit + ell) % 2)) + return out + + +def check_tables(search, tables) -> dict: + original = search.right_monomial_shift + count = 0 + for g in range(12): + for mask in range(4096): + expected = literal_shift(mask, g) + replay.require(tables[g][mask] == expected == original(mask, g), + "prepared shift changed a coefficient") + replay.require(expected.bit_count() == mask.bit_count(), + "permutation changed support cardinality") + count += 1 + composition = 0 + for g in range(12): + for h in range(12): + for mask in range(4096): + replay.require(tables[h][tables[g][mask]] == tables[search.GROUP_TABLE[g][h]][mask], + "right-action composition changed") + composition += 1 + return {"coefficient_cases": count, "composition_cases": composition} + + +def expect_rejection(action, label: str) -> None: + try: + action() + except (ValueError, OSError, KeyError, json.JSONDecodeError): + return + raise ValueError("control did not reject: " + label) + + +def controls(search, tables) -> list[str]: + labels = [] + for name, group in (("missing group row", search.GROUP_TABLE[:-1]), + ("short group row", ((),) + search.GROUP_TABLE[1:]), + ("nonpermutation", tuple((0,) * 12 for _ in range(12)))): + expect_rejection(lambda: replay.shift_tables(group), name) + labels.append(name) + left_tables = replay.shift_tables(tuple(zip(*search.GROUP_TABLE))) + expect_rejection(lambda: check_tables(search, left_tables), "left multiplication") + labels.append("left versus right multiplication") + changed = list(tables[1]) + changed[1 << 6] ^= 1 + mutant = (tables[0], tuple(changed)) + tables[2:] + expect_rejection(lambda: check_tables(search, mutant), "coefficient mutation") + labels.append("coefficient mutation") + payloads = replay.source_bytes() + with tempfile.TemporaryDirectory(prefix="dic3-source-controls-") as directory: + root = Path(directory) + for name, payload in payloads.items(): + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(payload) + replay.source_bytes(root) + for name, payload in payloads.items(): + target = root / name + target.write_bytes(payload + b"\n") + expect_rejection(lambda: replay.source_bytes(root), name) + labels.append("changed " + name) + target.write_bytes(payload) + target = root / replay.INPUTS[0] + target.unlink() + expect_rejection(lambda: replay.source_bytes(root), "missing source") + labels.append("missing source") + return labels + + +def check_measurement() -> None: + result = json.loads((PACKAGE / "MEASUREMENTS.json").read_text()) + replay.require(len(result["samples"]) == 10 and result["errors"] == 0, + "incomplete timing evidence") + for index, row in enumerate(result["samples"]): + replay.require(row["baseline"] == (index % 2 == 0), "timing order changed") + replay.require(row["returncode"] == row["stderr_bytes"] == 0, + "timed execution failed") + replay.require(row["stdout_sha256"] == hashlib.sha256(result["stdout"].encode()).hexdigest(), + "timed complete output changed") + for name, digest in result["source_hashes"].items(): + replay.require(hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() == digest, + "timing implementation changed: " + name) + for side, name in ((True, "baseline"), (False, "prepared")): + values = [r["elapsed_ns"] for r in result["samples"] if r["baseline"] == side] + replay.require(all(0 < value < 120_000_000_000 for value in values), + "timing exceeded its declared domain") + expected = {"median_ns": statistics.median(values), "min_ns": min(values), + "max_ns": max(values)} + replay.require(result[name] == expected, "timing summary changed") + reduction = 1 - result["prepared"]["median_ns"] / result["baseline"]["median_ns"] + replay.require(result["reduction_fraction"] == reduction > 0, + "recorded timing reduction changed") + + +def main() -> None: + check_measurement() + search, checker = replay.load_sources() + tables = replay.shift_tables(search.GROUP_TABLE) + counts = check_tables(search, tables) + rejected = controls(search, tables) + installed = replay.install(search) + replay.require(installed == tables, "installed table changed") + checker.main() + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file()} + print(json.dumps({"status": "PASS_DIC3_SHIFT_TABLE_REPLAY", **counts, + "controls": rejected, "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()