From a341471127ab570dcca1fa3ee1deaded3c5ca496 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 14:04:34 +0000 Subject: [PATCH] perf(research): accelerate E7 replay with intersection counters --- .../e7-intersection-counters/BENCHMARK.json | 112 +++++++++++ research/e7-intersection-counters/PROOF.md | 90 +++++++++ research/e7-intersection-counters/README.md | 137 ++++++++++++++ .../e7-intersection-counters/SOURCES.json | 54 ++++++ research/e7-intersection-counters/TASK.json | 61 ++++++ research/e7-intersection-counters/VERIFY.json | 41 ++++ .../e7-intersection-counters/benchmark.py | 57 ++++++ research/e7-intersection-counters/engine.py | 99 ++++++++++ research/e7-intersection-counters/replay.py | 72 +++++++ research/e7-intersection-counters/verify.py | 177 ++++++++++++++++++ 10 files changed, 900 insertions(+) create mode 100644 research/e7-intersection-counters/BENCHMARK.json create mode 100644 research/e7-intersection-counters/PROOF.md create mode 100644 research/e7-intersection-counters/README.md create mode 100644 research/e7-intersection-counters/SOURCES.json create mode 100644 research/e7-intersection-counters/TASK.json create mode 100644 research/e7-intersection-counters/VERIFY.json create mode 100644 research/e7-intersection-counters/benchmark.py create mode 100644 research/e7-intersection-counters/engine.py create mode 100644 research/e7-intersection-counters/replay.py create mode 100644 research/e7-intersection-counters/verify.py diff --git a/research/e7-intersection-counters/BENCHMARK.json b/research/e7-intersection-counters/BENCHMARK.json new file mode 100644 index 0000000000..378fd328f3 --- /dev/null +++ b/research/e7-intersection-counters/BENCHMARK.json @@ -0,0 +1,112 @@ +{ + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "cpu_count": 18, + "load_average": [ + 3.92578125, + 3.45361328125, + 2.77392578125 + ], + "errors": 0, + "serial": true, + "command_flags": [ + "-I", + "-W", + "error", + "-B" + ], + "records": [ + { + "engine": "original", + "seconds": 0.37083045789040625, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "intersection", + "seconds": 0.29308387520723045, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "original", + "seconds": 0.3668871249537915, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "intersection", + "seconds": 0.2906480410601944, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "original", + "seconds": 0.3726658751256764, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "intersection", + "seconds": 0.29022570815868676, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "original", + "seconds": 0.3703519580885768, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "intersection", + "seconds": 0.291430874960497, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "original", + "seconds": 0.3705076249316335, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + }, + { + "engine": "intersection", + "seconds": 0.2877717078663409, + "returncode": 0, + "stdout_sha256": "2853012eeacb5e0354e938bc1a137fb4790db281967da8e454fa5f30366a15c4", + "stderr_bytes": 0 + } + ], + "median_seconds": { + "original": 0.3705076249316335, + "intersection": 0.2906480410601944 + }, + "range_seconds": { + "original": [ + 0.3668871249537915, + 0.3726658751256764 + ], + "intersection": [ + 0.2877717078663409, + 0.29308387520723045 + ] + }, + "reduction": 0.21554099969244866, + "implementation_sha256": { + "engine.py": "882d0177e990b0534bb16ec188a622b6167051505bdb5a7b19b4462499a72e47", + "replay.py": "8cae6e46cc8ceddc9b1a714191750f00c39acca92a1b435ccea9accfcae4e1e8", + "benchmark.py": "ec0d4dbfe8231330af8b10378bce8d6e6f9a64c6ca6e2c503711d5bad921e24f", + "SOURCES.json": "1a7991ac02dcdd08338ff0d308a101b9aefd87dc2ab8cebc6d9d5dcb2d4a3fab" + } +} diff --git a/research/e7-intersection-counters/PROOF.md b/research/e7-intersection-counters/PROOF.md new file mode 100644 index 0000000000..be68c50af4 --- /dev/null +++ b/research/e7-intersection-counters/PROOF.md @@ -0,0 +1,90 @@ +# Exact intersection counters for translated bit lanes + +This implementation proof was produced by Nick Petalas. Apache-2.0. + +## Model and reused machinery + +Ali Romman's PR5729 represents independent binary generators as integer +bitsets. The first b generators define 2^b parallel lanes. For coordinate j, +integer C_j has bit l equal to coordinate j of the low-generator word u_l. +The remaining generators are traversed in binary reflected Gray order, +producing an offset v. Lane l represents exactly u_l xor v. + +The new implementation retains that representation, assignment order, +source population-plane adder, threshold selector and final word extraction +order. It changes how the weight planes for one translated batch are formed. +The statement here concerns this changed computation, not a new proof of +the E7 classification or its geometry. + +## Weight identity + +For binary words u,v, count separately the coordinates where both are one. +Their contribution is two to wt(u)+wt(v) and zero to wt(u xor v). A coordinate +with just one set bit contributes one to both sides. Thus + +```text +wt(u xor v) = wt(u) + wt(v) - 2 wt(u and v). +``` + +Compute the population planes for all u_l once, before the offset loop. +For offset v, pass only the coordinate columns C_j with v_j=1 to the +retained population-plane adder. In every lane this gives wt(u_l and v). +The scalar wt(v) is obtained by ordinary integer popcount. + +`translated_planes` adds that scalar to the fixed wt(u_l) planes and +subtracts twice the intersection count. The adder uses the usual full-adder +parity/carry identity. The subtractor uses the ordinary full-subtractor +borrow identity + +```text +borrow_out = (not a and (b or borrow_in)) or (b and borrow_in). +``` + +All Boolean operations act independently on corresponding bits of the +integer operands. Carries and borrows move to the next weight plane, never +to another coefficient lane. + +Let k=bit_length(width). The implementation keeps the low k weight planes, +so its arithmetic is modulo 2^k. Intermediate addition or subtraction can +wrap. The final true weight is between zero and width, and width<2^k for +positive width. Therefore its residue identifies the true weight uniquely. +Width zero is a separate valid empty-word case: the threshold accepts the +sole zero lane, with no weight plane needed. + +The retained `at_most` predicate consequently selects exactly the same +lanes as the original translated-column population count. The high offset +sequence and low-lane extraction order are identical. Independent generators +make the assignment-to-word map injective, so every qualifying word is +returned once, in the same order. No cached support set or classification +result participates in this computation. + +## Complete caller preservation + +`replay.py` authenticates six source files and loads the unchanged PR5729 +`classify.py`. Its private `run_path` dispatch substitutes only the +`low_weight_words` binding returned for that consumer's exact `binary.py` +path. Every other load follows the original function. Both comparator +modes use the same dispatch and authentication boundary. + +The source `main` still executes its complete `check`, including root/frame +construction, ambient slices, support enumeration, reflections, rational +ranks, orbit partition, all retained controls and comparison of the complete +result dictionary with the pinned RESULT.json. Its two output lines are +compared byte for byte between fresh original/intersection processes. +No production source or predecessor certificate is modified. + +## Finite evidence and limits + +The verifier compares every independent unordered generator set in F2^4 +under every bound 0..4 and batch size 1..5. Its literal subset-XOR oracle +checks contents; comparison with the source iterator also checks ordering. +There are 1,381 sets and 34,525 complete comparisons, all enumerated. +Another 108 fixed wide-code cases reach width 127. An independent scalar +popcount check covers all 87,381 ordered pairs u,v over widths 0..8, +including arithmetic wraparound. Sixteen rejected inputs and three changed +input/bound histories exercise validation and absence of result caching. + +These tests corroborate the implementation proof. The complete caller +checks preserve the predecessor computation rather than strengthen its +scientific conclusion. Timings describe this host, not every environment. +There is no new support bound, supplier, physical algorithm or kappa claim. diff --git a/research/e7-intersection-counters/README.md b/research/e7-intersection-counters/README.md new file mode 100644 index 0000000000..2d1cb197a6 --- /dev/null +++ b/research/e7-intersection-counters/README.md @@ -0,0 +1,137 @@ +# Faster complete E7 replay using intersection counters + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: measured verifier improvement with a scoped equivalence proof +and exact finite conformance. No new kappa is claimed. + +The complete current E7 classification replay has median time 0.290648 s +with intersection counters, versus 0.370508 s with Ali Romman's PR5729 +bit-lane engine. That is a 21.55% reduction on this host. Five alternating +fresh processes per engine have ranges 0.287772..0.293084 s and +0.366887..0.372666 s, respectively. All ten outputs are byte-identical, +with zero failures. [BENCHMARK.json](BENCHMARK.json) is the generated receipt +with raw samples, interpreter/environment and implementation hashes. + +The new step uses + +```text +wt(u xor v) = wt(u) + wt(v) - 2 wt(u and v). +``` + +It computes fixed lane weights once, then counts only columns selected by +the changing offset. Exact bit-plane addition and subtraction recover every +translated weight. [PROOF.md](PROOF.md) covers modular wraparound, every +coefficient assignment and iterator order. All complete classification +checks still run in the unchanged consumer. + +## Reproduce + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e7-intersection-counters/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/e7-intersection-counters/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e7-intersection-counters +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e7-intersection-counters --check-source-history +``` + +Another CPython 3.12 path can replace this host's path. Expected markers are +`PASS_E7_INTERSECTION_COUNTERS` and `PASS_REGISTERED_RESEARCH_PACKAGE`. +Default replay writes no files and prints a generated receipt bound to all +ten package files. The registered commands exercise normal and optimized +Python, including two complete fresh scientific callers in each mode. + +For the opt-in accelerated complete replay: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e7-intersection-counters/replay.py +``` + +Add `--engine original` for the current PR5729 comparator. To generate new +local timings, run `benchmark.py --output /absolute/path/outside/package.json` +with the same interpreter and flags. Timing includes process startup, +source authentication, imports, complete code enumeration, all downstream +classification checks, receipt comparison and output. The additional generic +conformance suite is outside that performance comparison. + +The verifier enumerates 34,525 complete small-code comparisons on 1,381 +independent generator sets, 108 wide-code cases and 87,381 scalar word pairs +for the new arithmetic. It rejects sixteen malformed or over-capacity inputs +and checks three changed-input histories. Outputs retain the original +iterator order. The complete E7 consumer compares its entire internal result +with the retained receipt, then emits identical output with both engines. + +## Measurement and scope + +The unreported baseline profile puts 0.236 of 0.623 instrumented seconds in +population-plane counting. Reflection transport and rational elimination +remain substantial unchanged costs, limiting the complete speedup. This +profile is diagnostic and is not one of the ten timing samples. Both timed +engines use the current default batch size sixteen. No stale original Gray +iterator is used as the comparator. + +Measurements used CPython 3.12.15, macOS arm64 and eighteen logical CPUs. +The entry load averages were 1.46, 2.83 and 2.48; other work can share the +host. Alternating serial processes give both engines the same exposure to +that noise. This is a local observation, not a hardware-independent speed +promise, a multiplication runtime benchmark or a CI timing certificate. + +The adapter accepts widths 0..127, at most 27 independent generators, +batch sizes 1..20 and at most 65,536 high-offset batches. These explicit +capacities include the complete E7 caller. They restrict the generic helper +interface, not the scientific replay's coefficient coverage. A generator +outside those capacities is rejected, rather than partially enumerated. +This is an opt-in standalone consumer substitution; production adoption, +concurrent shared-process use and other codes are outside the claim. + +## Provenance and credit + +Base main is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. +SOURCES.json pins all six live inputs. The selected-binding first example +passes at conditional kappa .003125804; no selected cold replay is run. +The `replay-runtime` card is refined to this originally posed counter +implementation question. It changes no scientific support theorem. + +Credit Ali Romman's [PR5729](https://github.com/CrocSwap/integer-mult-bounds/pull/5729) +for the bit-lane representation, Boolean population/threshold routines and +complete consumer, and his [PR5669](https://github.com/CrocSwap/integer-mult-bounds/pull/5669) +for the classification and retained checks. Nick Petalas's PR5238 supplies +the inherited geometry. Their source files and credit lines stay unchanged. +The weight identity and binary arithmetic are classical; the new contribution +is their intersection-count implementation and complete-command evidence. +No general literature-priority claim is made. + +Live claims, open PRs, recent account work, main READMEs and merged formula +searches were checked. Sparse local coverage is incomplete. The canonical +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294736) +records the corrected target. No predecessor audit is the deliverable. +Independent human and formal proof-kernel review are unclaimed. There is no +new native/physical caller, compiler, precision/tape, BIT or outer admission; +Lean, Docker and the selected scientific replay were not run. + +## Open next questions + +Can this opt-in engine replace the production iterator at a named caller +boundary, with regenerated dependent source pins? Begin with one explicit +installation and source-bound compatibility check. This package preserves +frozen sources and supplies the complete opt-in comparison; production +integration is separate. TASK.json records relevance, first step and blockers. +No further optimization or mathematical search is reserved. + +## Verifier constraints + +New functions are below sixty physical lines. There is no recursion. Explicit +capacities bound rows, bit lanes, widths, batches, subprocesses and timeouts. +The largest bit-lane table has 127 columns of at most 2^20 bits. The fixed +verification fixtures use smaller tables and at most 1,024 literal words. +Every complete child process has a sixty-second timeout and its exit status, +stderr and exact output are checked. + +Power of Ten rules 3 and 9 require managed-runtime deviations. Python allocates +bounded integers, tuples and lists during checking. `run_path` dispatches +only to named local source/adapter files, after authenticating external +inputs. The partial iterator has exactly the retained population/threshold +helpers as injected call targets. Each standalone process owns its temporary +consumer binding. Warnings are errors in both registered modes; no shared +source, diagnostics configuration or repository-wide suite changes. diff --git a/research/e7-intersection-counters/SOURCES.json b/research/e7-intersection-counters/SOURCES.json new file mode 100644 index 0000000000..a868916836 --- /dev/null +++ b/research/e7-intersection-counters/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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/e7-bitsliced-exhaustion/binary.py", + "usage": "input", + "git_blob": "cad9fc43ec0244bce415a76bc61b6445ffbd7519", + "sha256": "e79ad4d1d4be1748cf09aacc4274a316000d4b5922f13495778892b9309dc56e" + }, + { + "path": "research/e7-bitsliced-exhaustion/classify.py", + "usage": "input", + "git_blob": "3c14a223aebb5b05562c2db4f37eacc87148f9a3", + "sha256": "9fbdf0d4ad5c7a5feddfda2bfda7fbfedcdbc1361543b6ec7ef0f8ecc6bfb6c1" + }, + { + "path": "research/e7-bitsliced-exhaustion/source/RESULT.json", + "usage": "input", + "git_blob": "d32035693b23f114723c953c94370b349aa13cad", + "sha256": "2742bd01c85c988cb4b8c13359839ce9e10672bde1a40c8bf668aae70b12c98d" + }, + { + "path": "research/e7-bitsliced-exhaustion/source/SOURCES.json", + "usage": "input", + "git_blob": "195cf52a31ad494b2a4444beaa2bf66f0c8942e8", + "sha256": "6281c850b2827c2d10624822c9fa2aed4f7ecf50e1c615777e72214aa568ecc6" + }, + { + "path": "research/e7-bitsliced-exhaustion/source/vendor/PR5238.py", + "usage": "input", + "git_blob": "781a074d45126b1a84b92ee2393dc95790c0cb1b", + "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2" + }, + { + "path": "research/e7-bitsliced-exhaustion/source/vendor/PR5238.md", + "usage": "input", + "git_blob": "5dc802961147c41af039e899d8baa3c8bb9e3909", + "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085" + } + ] +} diff --git a/research/e7-intersection-counters/TASK.json b/research/e7-intersection-counters/TASK.json new file mode 100644 index 0000000000..1b4e5e0eba --- /dev/null +++ b/research/e7-intersection-counters/TASK.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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": "Implement intersection-based bit-lane weights and reduce the complete current E7 classification replay while preserving all checks and exact outputs.", + "scope_change_reason": "Refine replay-runtime to an originally posed arithmetic change in the retained PR5729 consumer; no predecessor scientific audit.", + "bottleneck_link": "Reduce complete replay cost for E7 deletion/decoder research while retaining every finite classification obligation.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified complete-command speed improvement; do not continue tuning.", + "outcome": "completed", + "evidence": "BENCHMARK.json; PROOF.md; 34525 small-code comparisons, 108 wide cases, 87381 arithmetic pairs, 16 rejected inputs, 3 invalidation histories and byte-identical complete callers.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a named production caller adopt this intersection counter with all affected pins regenerated?", + "why_it_matters": "The package provides an opt-in complete replay, while default callers remain unchanged.", + "first_step": "Choose one explicit consumer installation, compare its complete source-bound behavior and update every affected input pin.", + "blocked_by": "Production integration is outside this isolated package." + } + ] +} diff --git a/research/e7-intersection-counters/VERIFY.json b/research/e7-intersection-counters/VERIFY.json new file mode 100644 index 0000000000..1af5962707 --- /dev/null +++ b/research/e7-intersection-counters/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e7-bitsliced-exhaustion/binary.py", + "research/e7-bitsliced-exhaustion/classify.py", + "research/e7-bitsliced-exhaustion/source/RESULT.json", + "research/e7-bitsliced-exhaustion/source/SOURCES.json", + "research/e7-bitsliced-exhaustion/source/vendor/PR5238.py", + "research/e7-bitsliced-exhaustion/source/vendor/PR5238.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact counter arithmetic, complete small/wide-code conformance, malformed/invalidation controls, generated timing receipt and both complete scientific callers. Normal mode." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact counter arithmetic, complete small/wide-code conformance, malformed/invalidation controls, generated timing receipt and both complete scientific callers. Optimized mode." + } + ] +} diff --git a/research/e7-intersection-counters/benchmark.py b/research/e7-intersection-counters/benchmark.py new file mode 100644 index 0000000000..39080181b2 --- /dev/null +++ b/research/e7-intersection-counters/benchmark.py @@ -0,0 +1,57 @@ +"""Measure alternating complete E7 replays; write a generated timing receipt.""" +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + if args.output.resolve().is_relative_to(HERE.resolve()): + raise ValueError("write benchmark output outside the package") + rows = [] + for label in ("original", "intersection") * 5: + command = [sys.executable, "-I", "-W", "error", "-B", + str(HERE / "replay.py"), "--engine", label] + start = time.perf_counter() + result = subprocess.run(command, capture_output=True, timeout=60) + elapsed = time.perf_counter() - start + if result.returncode or result.stderr: + raise ValueError("complete replay failed: " + result.stderr.decode()) + if not result.stdout.startswith(b"PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION\n"): + raise ValueError("complete scientific work was not reported") + rows.append(dict(engine=label, seconds=elapsed, returncode=result.returncode, + stdout_sha256=sha256(result.stdout).hexdigest(), + stderr_bytes=len(result.stderr))) + if len({row["stdout_sha256"] for row in rows}) != 1: + raise ValueError("complete scientific output differs") + samples = {label: [r["seconds"] for r in rows if r["engine"] == label] + for label in ("original", "intersection")} + medians = {label: statistics.median(values) for label, values in samples.items()} + files = ("engine.py", "replay.py", "benchmark.py", "SOURCES.json") + receipt = dict(python=sys.version, executable=sys.executable, + platform=platform.platform(), cpu_count=os.cpu_count(), + load_average=os.getloadavg(), errors=0, serial=True, + command_flags=["-I", "-W", "error", "-B"], records=rows, + median_seconds=medians, + range_seconds={label: [min(v), max(v)] for label, v in samples.items()}, + reduction=1 - medians["intersection"] / medians["original"], + implementation_sha256={name: sha256((HERE / name).read_bytes()).hexdigest() + for name in files}) + args.output.write_text(json.dumps(receipt, indent=2) + "\n") + print(json.dumps({key: receipt[key] for key in + ("median_seconds", "range_seconds", "reduction", "errors")})) + + +if __name__ == "__main__": + main() diff --git a/research/e7-intersection-counters/engine.py b/research/e7-intersection-counters/engine.py new file mode 100644 index 0000000000..0283d450ae --- /dev/null +++ b/research/e7-intersection-counters/engine.py @@ -0,0 +1,99 @@ +"""Intersection counters produced by Nick Petalas. Apache-2.0. + +Ali Romman's PR5729 supplies the injected population and threshold routines. +""" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def checked_rows(generators, width, maximum, batch_bits): + need(type(width) is int and 0 <= width <= 127, "width outside 0..127") + need(type(maximum) is int and 0 <= maximum <= width, "invalid weight bound") + need(type(batch_bits) is int and 1 <= batch_bits <= 20, "invalid batch size") + rows = [] + pivots = {} + for index, row in enumerate(generators): + need(index < 27, "dimension exceeds 27") + need(type(row) is int and 0 < row < 1 << width, "invalid generator") + residual = row + for pivot in range(width - 1, -1, -1): + if residual >> pivot & 1: + if pivot in pivots: + residual ^= pivots[pivot] + else: + pivots[pivot] = residual + break + need(residual != 0, "dependent generators") + rows.append(row) + count = min(batch_bits, len(rows)) + need(len(rows) - count <= 16, "batch count exceeds 65536") + return tuple(rows), count + + +def lane_columns(rows, width, count, mask): + columns = [0] * width + for index in range(count): + block = 1 << index + pattern = mask // ((1 << (2 * block)) - 1) * (((1 << block) - 1) << block) + row = rows[index] + for coordinate in range(width): + if row >> coordinate & 1: + columns[coordinate] ^= pattern + return columns + + +def translated_planes(base, intersection, offset_weight, mask, powers): + """Compute base + offset_weight - 2*intersection modulo 2**powers.""" + result = [] + carry = 0 + for power in range(powers): + a = base[power] if power < len(base) else 0 + b = mask if offset_weight >> power & 1 else 0 + parity = a ^ b + result.append(parity ^ carry) + carry = (a & b) | (parity & carry) + borrow = 0 + for power in range(powers): + a = result[power] + b = intersection[power - 1] if 1 <= power <= len(intersection) else 0 + result[power] = a ^ b ^ borrow + borrow = ((~a) & (b | borrow)) | (b & borrow) + return result + + +def selected_word(rows, coefficient, offset): + word = offset + for index in range(min(20, len(rows))): + if coefficient >> index & 1: + word ^= rows[index] + return word + + +def low_weight_words(generators, width, maximum, batch_bits=16, *, + population_planes, at_most): + rows, count = checked_rows(generators, width, maximum, batch_bits) + lanes = 1 << count + mask = (1 << lanes) - 1 + columns = lane_columns(rows, width, count, mask) + base = population_planes(columns) + offset = 0 + for index in range(1 << (len(rows) - count)): + if index: + changed = (index & -index).bit_length() - 1 + offset ^= rows[count + changed] + terms = [columns[j] for j in range(width) if offset >> j & 1] + intersection = population_planes(terms) + planes = translated_planes(base, intersection, offset.bit_count(), + mask, width.bit_length()) + hits = at_most(planes, maximum, mask) + for _ in range(lanes): + if not hits: + break + low = hits & -hits + coefficient = low.bit_length() - 1 + yield selected_word(rows, coefficient, offset) + hits ^= low + need(hits == 0, "lane extraction exhausted") diff --git a/research/e7-intersection-counters/replay.py b/research/e7-intersection-counters/replay.py new file mode 100644 index 0000000000..10391bea21 --- /dev/null +++ b/research/e7-intersection-counters/replay.py @@ -0,0 +1,72 @@ +"""Run the complete retained E7 consumer with one chosen counter engine.""" +import argparse +from functools import partial +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys + +HERE = Path(__file__).resolve().parent +REPO = HERE.parent.parent +SOURCE = REPO / "research/e7-bitsliced-exhaustion" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def read_bytes(path): + need(path.stat().st_size <= 1_048_576, "input exceeds one MiB") + return path.read_bytes() + + +def authenticate(): + sources = json.loads(read_bytes(HERE / "SOURCES.json")) + rows = [row for row in sources["files"] if row["usage"] == "input"] + need(len(rows) == 6, "expected six live inputs") + for row in rows: + data = read_bytes(REPO / row["path"]) + need(sha256(data).hexdigest() == row["sha256"], + "source digest mismatch: " + row["path"]) + + +def engines(): + original = run_path(str(SOURCE / "binary.py")) + current = run_path(str(HERE / "engine.py")) + fast = partial(current["low_weight_words"], + population_planes=original["population_planes"], + at_most=original["at_most"]) + return original["low_weight_words"], fast + + +def execute(engine_name): + authenticate() + old, new = engines() + selected = old if engine_name == "original" else new + binary = SOURCE / "binary.py" + + def dispatch(path, *args, **kwargs): + if Path(path) == binary: + need(not args and not kwargs, "unexpected binary loader contract") + return {"low_weight_words": selected} + return run_path(path, *args, **kwargs) + + consumer = run_path(str(SOURCE / "classify.py")) + consumer["main"].__globals__["run_path"] = dispatch + consumer["main"]() + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--engine", choices=("original", "intersection"), + default="intersection") + args = parser.parse_args() + sys.dont_write_bytecode = True + sys.pycache_prefix = str(HERE / "unused-bytecode-namespace") + execute(args.engine) + + +if __name__ == "__main__": + main() diff --git a/research/e7-intersection-counters/verify.py b/research/e7-intersection-counters/verify.py new file mode 100644 index 0000000000..7abbdf37d8 --- /dev/null +++ b/research/e7-intersection-counters/verify.py @@ -0,0 +1,177 @@ +"""Exact conformance and complete-caller replay for intersection counters.""" +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +from runpy import run_path +import statistics +import subprocess +import sys + +HERE = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def literal_words(rows): + words = [0] + for row in rows: + words.extend([word ^ row for word in words[:]]) + return words + + +def small_codes(original, current): + codes = comparisons = 0 + for dimension in range(5): + for rows in combinations(range(1, 16), dimension): + literal = literal_words(rows) + if len(set(literal)) != len(literal): + continue + codes += 1 + for maximum in range(5): + expected = sorted(word for word in literal if word.bit_count() <= maximum) + for batch in range(1, 6): + old = list(original(rows, 4, maximum, batch)) + new = list(current(rows, 4, maximum, batch)) + need(new == old and sorted(new) == expected, + "small-code content or iterator order changed") + comparisons += 1 + need((codes, comparisons) == (1381, 34525), "small-code coverage changed") + return codes, comparisons + + +def wide_codes(original, current): + comparisons = 0 + for width in (0, 1, 7, 31, 63, 64, 65, 127): + dimension = min(10, width) + rows = [] + for i in range(dimension): + extra = sum((((i + 1) * (j + 3) + (i ^ j)).bit_count() & 1) << j + for j in range(width - dimension)) + rows.append((extra << dimension) | (1 << i)) + literal = literal_words(rows) + for maximum in sorted({0, width // 3, width // 2, width}): + expected = sorted(word for word in literal if word.bit_count() <= maximum) + for batch in (1, 3, 7, 16): + new = list(current(rows, width, maximum, batch)) + need(new == list(original(rows, width, maximum, batch)), + "wide-code iterator order changed") + need(sorted(new) == expected, "wide-code content changed") + comparisons += 1 + return comparisons + + +def arithmetic_cases(translated, population): + pairs = 0 + for width in range(9): + lanes = 1 << width + mask = (1 << lanes) - 1 + columns = [sum(1 << lane for lane in range(lanes) if lane >> bit & 1) + for bit in range(width)] + base = population(columns) + for offset in range(1 << width): + intersection = population([columns[j] for j in range(width) + if offset >> j & 1]) + planes = translated(base, intersection, offset.bit_count(), + mask, width.bit_length()) + for lane in range(lanes): + actual = sum((plane >> lane & 1) << bit + for bit, plane in enumerate(planes)) + need(actual == (lane ^ offset).bit_count(), + "translated population arithmetic differs") + pairs += 1 + return pairs + + +def reject(action): + try: + action() + except ValueError: + return + raise ValueError("invalid input was accepted") + + +def controls(engine): + cases = [([1], -1, 0, 1), ([1], True, 0, 1), ([1], 128, 0, 1), + ([1], 1, -1, 1), ([1], 1, True, 1), ([1], 1, 2, 1), + ([True], 1, 1, 1), ([-1], 1, 1, 1), ([2], 1, 1, 1), + ([0], 1, 1, 1), ([1, 2, 3], 2, 1, 1), + ([1], 1, 1, 0), ([1], 1, 1, 21), ([1], 1, 1, True), + ([1 << i for i in range(28)], 28, 1, 16), + ([1 << i for i in range(18)], 18, 1, 1)] + for args in cases: + reject(lambda args=args: list(engine(*args))) + # Successive changed inputs must not reuse an old result table. + need(list(engine([1, 2], 3, 1)) == [0, 1, 2], "initial input control") + need(list(engine([3, 4], 3, 1)) == [0, 4], "changed generator control") + need(list(engine([1, 2], 3, 0)) == [0], "changed bound control") + return len(cases), 3 + + +def benchmark_receipt(): + receipt = json.loads((HERE / "BENCHMARK.json").read_text()) + rows = receipt["records"] + need(len(rows) == 10 and receipt["errors"] == 0, "benchmark coverage") + need([r["engine"] for r in rows] == ["original", "intersection"] * 5, + "benchmark was not alternating") + need(all(r["returncode"] == 0 and r["stderr_bytes"] == 0 for r in rows), + "benchmark includes a failed replay") + need(len({r["stdout_sha256"] for r in rows}) == 1, "benchmark outputs differ") + medians = {label: statistics.median(r["seconds"] for r in rows if r["engine"] == label) + for label in ("original", "intersection")} + need(receipt["median_seconds"] == medians, "benchmark median changed") + need(receipt["reduction"] == 1 - medians["intersection"] / medians["original"], + "benchmark reduction changed") + need(medians["intersection"] < medians["original"], "no measured improvement") + for name, expected in receipt["implementation_sha256"].items(): + need(sha256((HERE / name).read_bytes()).hexdigest() == expected, + "benchmark implementation changed: " + name) + return receipt["reduction"] + + +def complete_callers(): + outputs = [] + for label in ("original", "intersection"): + command = [sys.executable, "-I", "-W", "error", "-B", + str(HERE / "replay.py"), "--engine", label] + result = subprocess.run(command, capture_output=True, timeout=60) + need(result.returncode == 0 and not result.stderr, + "complete replay failed: " + result.stderr.decode()) + need(result.stdout.startswith(b"PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION\n"), + "complete scientific work was not reported") + outputs.append(result.stdout) + need(outputs[0] == outputs[1], "complete classification output differs") + return sha256(outputs[0]).hexdigest() + + +def main(): + sys.dont_write_bytecode = True + replay = run_path(str(HERE / "replay.py")) + replay["authenticate"]() + original, current = replay["engines"]() + code = run_path(str(HERE / "engine.py")) + helpers = run_path(str(replay["SOURCE"] / "binary.py")) + codes, comparisons = small_codes(original, current) + wide = wide_codes(original, current) + pairs = arithmetic_cases(code["translated_planes"], helpers["population_planes"]) + rejected, invalidations = controls(current) + reduction = benchmark_receipt() + complete_hash = complete_callers() + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "engine.py", "replay.py", "verify.py", "benchmark.py", "BENCHMARK.json") + hashes = {name: sha256((HERE / name).read_bytes()).hexdigest() for name in names} + print(json.dumps(dict(status="PASS_E7_INTERSECTION_COUNTERS", codes=codes, + small_comparisons=comparisons, wide_comparisons=wide, + arithmetic_pairs=pairs, rejected_inputs=rejected, + invalidation_controls=invalidations, + complete_output_sha256=complete_hash, + recorded_local_reduction=reduction, + python=sys.version.split()[0], package_sha256=hashes), + sort_keys=True)) + + +if __name__ == "__main__": + main()