diff --git a/research/core-section-gray-replay/PROOF.md b/research/core-section-gray-replay/PROOF.md new file mode 100644 index 0000000000..c78c5a9ebf --- /dev/null +++ b/research/core-section-gray-replay/PROOF.md @@ -0,0 +1,92 @@ +# Exact Gray-code replacement of the section enumerator + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped implementation-equivalence proof. Gray-code enumeration +and packed binary columns are classical. James Reed's PR3773 supplies the +scientific consumer and its E8 core result. Neither the geometry nor the +published histogram is a new theorem of this package. + +## The computed object + +Let c_0,...,c_(s-1) be d-bit binary coordinate vectors. For a d-bit mask m, +the predecessor's expression computes + + h(m) = #{j : popcount(m AND c_j) is even}. + +It builds an integer whose set bits are the distinct original root indices +of those j, then takes its population count. Those root indices are distinct +because they come from the bits of a set intersection. Thus the expression +equals h(m). The consumer requires the multiset of h(m) for all nonzero masks. +It still evaluates every core separately, including repeated isomorphism types. + +## Packed columns and the invariant + +For 0<=i> bit) & 1) << index + for index, value in enumerate(coordinates)) + for bit in range(dimension)] + counts = [len(coordinates)] * (1 << dimension) + odd = 0 + for step in range(1, 1 << dimension): + bit = (step & -step).bit_length() - 1 + odd ^= columns[bit] + mask = step ^ (step >> 1) + counts[mask] = len(coordinates) - odd.bit_count() + return tuple(counts) + + +def gray_sections(coordinates, dimension): + return Counter(gray_counts(coordinates, dimension)[1:]) + + +def authenticate(root=ROOT): + """Authenticate every declared live input before executing any source.""" + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = tuple(row for row in manifest["files"] if row["usage"] == "input") + require(len(inputs) == 3, "the complete three-input binding is required") + payloads = {} + for row in inputs: + path = root / row["path"] + payload = path.read_bytes() + require(sha256(payload).hexdigest() == row["sha256"], + "source drift: " + row["path"]) + payloads[row["path"]] = payload + return payloads + + +def load_consumer(engine="gray", root=ROOT): + require(engine in ("original", "gray"), "unknown engine") + payloads = authenticate(root) + path = root / SOURCE + text = payloads[SOURCE].decode("utf-8") + require(text.count(OLD) == 1 and "gray_sections" not in text, + "the isolated source adapter no longer matches") + if engine == "gray": + text = text.replace(OLD, NEW) + module = ModuleType("_core_section_consumer") + module.__file__ = str(path) + module.gray_sections = gray_sections + # Only authenticated predecessor source is compiled. Its __main__ guard + # remains false; main() below still executes its full scientific consumer. + exec(compile(text, str(path), "exec"), module.__dict__) + return module + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--engine", choices=("original", "gray"), default="gray") + args = parser.parse_args() + load_consumer(args.engine).main() + + +if __name__ == "__main__": + main() diff --git a/research/core-section-gray-replay/verify.py b/research/core-section-gray-replay/verify.py new file mode 100644 index 0000000000..ca4fdd5c18 --- /dev/null +++ b/research/core-section-gray-replay/verify.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +"""Finite conformance of the new Gray enumerator and its complete consumer. + +Produced by Nick Petalas. Apache-2.0. PR3773's geometry/histogram remain +James Reed's results. This checks implementation equivalence, not novelty +or independent mathematical acceptance of those results. +""" + +import argparse +from collections import Counter +from contextlib import redirect_stdout +from hashlib import sha256 +from io import StringIO +from itertools import product +import json +from pathlib import Path +import runpy +import tempfile + +PACKAGE = Path(__file__).resolve().parent +REPLAY = runpy.run_path(str(PACKAGE / "replay.py")) +gray_counts = REPLAY["gray_counts"] +load_consumer = REPLAY["load_consumer"] +require = REPLAY["require"] +MARKER = "PASS_CORE_SECTION_CAPACITY pairs=3780 sections=127 no_new_kappa\n" + + +def direct_counts(coordinates, dimension): + return tuple(sum((mask & value).bit_count() % 2 == 0 + for value in coordinates) + for mask in range(1 << dimension)) + + +def verify_small(): + cases = 0 + masks = 0 + for dimension in range(5): + for size in range(4): + for coordinates in product(range(1 << dimension), repeat=size): + observed = gray_counts(coordinates, dimension) + require(observed == direct_counts(coordinates, dimension), + "small complete mask table differs") + cases += 1 + masks += len(observed) + coordinates = tuple((37 * index) % 1024 for index in range(256)) + require(gray_counts(coordinates, 10) == direct_counts(coordinates, 10), + "capacity-boundary mask table differs") + return {"small_coordinate_lists": cases, "small_masks": masks, + "capacity_boundary_masks": 1024} + + +def verify_complete(): + consumer = load_consumer() + calls = [] + + def checked_sections(coordinates, dimension): + observed = gray_counts(coordinates, dimension) + require(observed == direct_counts(coordinates, dimension), + "reached core mask table differs") + require(dimension == 7 and len(coordinates) == 24, + "source adapter reached a different domain") + calls.append((dimension, len(coordinates), len(observed) - 1)) + return Counter(observed[1:]) + + consumer.gray_sections = checked_sections + output = StringIO() + with redirect_stdout(output): + consumer.main() + require(output.getvalue() == MARKER, "complete scientific stdout differs") + require(len(calls) == 3780, "a complete core invocation is missing") + sections = sum(row[2] for row in calls) + return {"core_calls": len(calls), "nonzero_mask_sections": sections, + "reference_parity_evaluations": sum(n * q for _, n, q in calls), + "gray_column_bit_tests": sum(d * n for d, n, _ in calls), + "gray_xor_updates": sections, + "complete_stdout_sha256": sha256(output.getvalue().encode()).hexdigest()} + + +def rejected(operation, expected): + try: + operation() + except (ValueError, FileNotFoundError, SystemExit) as error: + require(expected in str(error), "control failed for a different reason") + return 1 + raise ValueError("control accepted: " + expected) + + +def verify_boundaries(): + invalid = (((), -1, "dimension must"), ((), 11, "dimension must"), + ((), True, "dimension must"), ((), 1.0, "dimension must"), + ((-1,), 2, "coordinate outside"), ((4,), 2, "coordinate outside"), + ((True,), 2, "coordinate outside"), ((1.0,), 2, "coordinate outside"), + ((0,) * 257, 2, "at most 256"), ({0}, 2, "at most 256")) + controls = sum(rejected(lambda c=c, d=d: gray_counts(c, d), + expected) for c, d, expected in invalid) + controls += rejected(lambda: load_consumer("missing"), "unknown engine") + payloads = REPLAY["authenticate"]() + with tempfile.TemporaryDirectory(prefix="core-gray-controls-") as directory: + root = Path(directory) + for name, payload in payloads.items(): + path = root / name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(payload) + for name, payload in payloads.items(): + path = root / name + path.write_bytes(payload + b"\n") + controls += rejected(lambda: load_consumer(root=root), "source drift") + path.unlink() + controls += rejected(lambda: load_consumer(root=root), name) + path.write_bytes(payload) + return controls + + +def verify_mutations(): + mutants = ( + lambda c, d: Counter(gray_counts(c, d)), # Incorrectly includes mask zero. + lambda c, d: Counter(gray_counts(c, d)[1:-1]), + lambda c, d: Counter(len(c) - count for count in gray_counts(c, d)[1:]), + lambda c, d: Counter(gray_counts(c[1:], d)[1:]), + ) + controls = 0 + for mutant in mutants: + consumer = load_consumer() + consumer.gray_sections = mutant + controls += rejected(consumer.main, "a section histogram moved") + consumer = load_consumer() + consumer.EXPECTED = {0: 2, 8: 15, 12: 96, 16: 15} + controls += rejected(consumer.main, "a section histogram moved") + consumer = load_consumer() + original_span = consumer.span_coordinates + consumer.span_coordinates = lambda values: (6, original_span(values)[1]) + controls += rejected(consumer.main, "a common core moved") + return controls + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = {**verify_small(), **verify_complete(), + "boundary_controls": verify_boundaries(), + "scientific_mutation_controls": verify_mutations(), + "status": "PASS_CORE_SECTION_GRAY_REPLAY"} + result["package_sha256"] = { + path.name: sha256(path.read_bytes()).hexdigest() + for path in sorted(PACKAGE.iterdir()) if path.is_file()} + if args.receipt: + target = args.receipt.resolve() + require(not target.is_relative_to(REPLAY["ROOT"]), + "receipts must stay outside the checkout") + target.write_text(json.dumps(result, sort_keys=True, indent=2) + "\n") + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()