diff --git a/research/p112-compatibility-kernels/PROOF.md b/research/p112-compatibility-kernels/PROOF.md new file mode 100644 index 0000000000..22a08fb718 --- /dev/null +++ b/research/p112-compatibility-kernels/PROOF.md @@ -0,0 +1,100 @@ +# Exact restriction-kernel evaluation + +This contribution was produced by Nick Petalas. Apache-2.0. +The census, decoder theorem and scientific receipt are Philipp / mightyOil's +[PR1325](https://github.com/CrocSwap/integer-mult-bounds/pull/1325). +Binary elimination and rank-nullity are classical. PR1325's `independent.py` +already computes nullities by stacking equations in nine coefficient +coordinates. No priority for that method is claimed. The new contribution is +direct restriction of bit-string basis rows as an exact, faster evaluator +preserving the primary command's complete scientific object and ordered digest. + +## The replacement identity + +Let V be a binary vector space of bit strings of length n. Let g_1,...,g_d +be an independent basis. For a bit mask M, restriction to M is the linear map + +```text +R_M : V -> F_2^n, v -> v & M. +``` + +Its matrix has rows g_i & M. Therefore + +```text +dim {v in V : v & M = 0} = d - rank_F2(g_i & M : 1<=i<=d). +``` + +The predecessor constructs that kernel by filtering every vector in V and +takes log_2 of the resulting cardinality. A binary vector space of dimension k +has exactly 2^k elements, so both methods return exactly the same integer. +The restriction images may be dependent even when the original basis is +independent. Elimination must occur after restriction; subtracting the number +of nonzero restricted basis vectors would be wrong. + +For each plane with canonical generators x,y, the predecessor tests +`not z & (x|y) & conflict[a][k]`. Choose +`M=(x|y)&conflict[a][k]`. For its single-vector census choose +`M=z&conflict[a][3]`. These are exactly the two uses replaced in `fast.py`. +No predicate, selected mask or plane representative changes. + +## Complete output preservation + +The implementation retains each source geometry, pairing, support and span +constructor. It visits the same sorted spaces, the same canonical plane test +`y < x^y`, the same three anchors and the same partner order. Each dimension +tuple is equal by the identity above. Consequently every census increment and +every canonical byte fed to the ordered plane digest agrees. + +The source's real-span, code-dimension and zero-cost checks remain. Every +decoder witness, nonconstant example and all six rejection controls are +retained, in their original order. The new orchestration calls the pinned +source's `decode` and `check_identity` functions. The complete returned object, +including source hashes, is compared with the unchanged source certificate. +The CLI prints the identical scientific success line. Exclusive `--write` +creation produces the same sorted, indented scientific JSON and rejects +overwriting an existing file. These statements concern preservation of the +source contract; they are not independent validation of the decoder theorem. + +## Exact restriction work + +The three coordinate spaces have 256 elements and dimension eight; the extra +space has 512 elements and dimension nine. For each of the 32,385 planes, +the source masks 256+256+512 partner vectors. Its 765 single-vector queries +each mask 512 vectors. Thus it performs + +```text +32385*(256+256+512) + 765*512 = 33,553,920 vector restrictions. +``` + +The replacement masks 8+8+9 basis rows per plane and nine per single query: + +```text +32385*(8+8+9) + 765*9 = 816,510 basis-row restrictions. +``` + +This removes 32,737,410 restrictions in those queries. It introduces bounded +binary elimination and builds four bases once. The calculation is not a total +instruction count or an asymptotic multiplication bound. The verifier counts +all 97,920 replacement queries and their masked basis rows during the complete +replay. Timing measures the complete CLI, including unchanged work. + +## Bounded conformance + +The conformance checker enumerates all 67 subspaces of F_2^4 and all 16 masks, +for 1,072 cases. Its independent oracle counts literal vectors in each kernel. +Another 320 fixtures cover basis dimensions zero through nine and 112-bit +strings, again enumerating every vector. Five direct boundary controls cover +the zero space, zero restriction, injective restriction, dependent restricted +images and bit 111. The unchanged complete scientific object and digest are +also compared. Quantified correctness follows from rank-nullity, rather than +extrapolation from these fixtures. + +## Limits + +The evaluator is opt-in and tied to the exact retained source bytes. Its +orchestration duplicates the source's contract and fails the source hash if +that contract changes. The kernel routine assumes an independent basis of +at most nine rows. Source construction and explicit dimension checks enforce +that premise. This is a finite evaluation improvement. It supplies no new +decoder floor, physical COPY word, paid histogram, supplier admission, kappa +or complete multiplication theorem. diff --git a/research/p112-compatibility-kernels/README.md b/research/p112-compatibility-kernels/README.md new file mode 100644 index 0000000000..114cb649c9 --- /dev/null +++ b/research/p112-compatibility-kernels/README.md @@ -0,0 +1,136 @@ +# Faster exact P112 plane compatibility + +This contribution was produced by Nick Petalas. Apache-2.0. + +The complete PR1325 scientific replay takes a local median **0.326 seconds** +with the restriction-kernel evaluator, versus **1.365 seconds** with the +retained source command, a **76.09% reduction** across five alternating runs +per side. All runs succeed with identical scientific stdout. This is a scoped +implementation-preservation proof, finite conformance evidence and a local +performance observation. No new kappa is claimed. + +Philipp / mightyOil's [PR1325](https://github.com/CrocSwap/integer-mult-bounds/pull/1325) +supplies the census, equality theorem, witnesses and source implementation. +Its mathematics is a cited premise. The new step restricts bit-string basis +rows, preserving the complete 32,385-plane and +765-vector domains, canonical digest, witnesses and six rejection controls. +The predecessor package stays unchanged. + +For a binary space with independent basis g_i, the exact replacement is + +```text +log2(number of vectors v with v & mask = 0) + = dimension(V) - binary_rank(g_i & mask). +``` + +[PROOF.md](PROOF.md) proves preservation of the complete scientific object. +The query stage masks 816,510 basis rows instead of 33,553,920 space vectors. +It also performs binary elimination and prepares four bases. This is not a +claim that the whole command has only 816,510 operations. + +## Reproduce + +Run from the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p112-compatibility-kernels/fast.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p112-compatibility-kernels/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p112-compatibility-kernels +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p112-compatibility-kernels --check-source-history +``` + +A reviewer can substitute their CPython 3.12 executable. The fast CLI prints +the same `PASS_SPARSE_REDUNDANT_DECODER` line as the source. The conformance +checker prints `PASS_P112_COMPATIBILITY_KERNELS` in a generated JSON stdout +receipt bound to all eight package files. It checks 1,072 exhaustive small +subspace/mask cases, 320 wide cases, five boundaries, the complete scientific +object and counted query work. Both registered commands include that complete +replay, with and without `-O`; each has a 120-second limit. + +To reproduce the comparison, choose a fresh output path outside the checkout: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/p112-compatibility-kernels/benchmark.py --write /tmp/p112-kernel-benchmark.json +``` + +The harness runs each entire command five times in alternating order, with +identical `-I -O -W error -B` flags. It checks exit status, exact stdout and +empty stderr for every sample. Source hashes, interpreter startup, census, +decoder checks, controls and certificate comparison all occur inside the +timed subprocess. It refuses to overwrite its output. + +## Local timing evidence + +CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. The machine was shared; +the observed load averages were 9.46, 7.27 and 4.49. Other research and Git +processes were active. Alternation limits drift but does not establish a +portable performance guarantee. All ten commands returned success, with zero +stderr bytes and equal stdout hashes. + +| Command | Five wall times, seconds | Median | Range | +|---|---|---|---| +| Source | 1.433095, 1.656254, 1.364952, 1.351939, 1.306152 | 1.364952 | 1.306152 to 1.656254 | +| Kernel | 0.317710, 0.338164, 0.326321, 0.331216, 0.293263 | 0.326321 | 0.293263 to 0.338164 | + +CPU times are close to wall times on both sides. A separate, untimed cProfile +run attributes most source time to `run`, which contains the compatibility +comprehensions; all-pairs identity checks are the next substantial component. +The reduced scans explain the gain. The complete command still executes those +identity checks, source preparation, canonical JSON and hashing. The timing +comparison excludes the additional conformance verifier and does not claim +to accelerate the predecessor's independent implementation or package tests. + +## Scope and credit + +Sources are pinned to canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. The card +`census-pruning-audit` changes scope to exact census acceleration, as recorded +in [TASK.json](TASK.json). The selected binding positive control passed. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361674) +names this exact evaluation target. + +PR1325's independent implementation already uses coefficient-space equations +and rank-nullity. This contribution claims the faster primary-receipt evaluator, +not priority for kernel dimensions or another mathematical verification. +The source retains Philipp / mightyOil's attribution and the PR845, +coordinate-reader, nine-term representation and deficiency-plane lineage. +Classical binary elimination and rank-nullity are used here. No predecessor +proof is audited or independently certified. Actual native delivery, dirty +restoration in a physical caller, complete recursive charges, stock, precision +and supplier admission remain outside this result. No selected cold replay, +Lean, Docker or independent human/formal-kernel review is claimed. + +## Open next questions + +Can the same kernel evaluator accelerate a different complete decoder census? +First profile its full command and identify its exact subspace-restriction +contract. Each source's ordering, receipt and rejection controls must survive; +this package proves no automatic compatibility. This is the sole Open next +questions item; research stops at the first verified improvement. + +## Verifier bounds and deviations + +The new code has no recursion. Kernel elimination uses at most nine passes +per row. Plane loops have three anchors and at most 255 by 254 candidate +pairs per anchor. Spaces have at most 512 vectors, masks have at most 112 +bits and scientific fixtures have 112 rows. Source reads in the adapter are +bounded at one MiB per file before hash validation. The small-space generator has +four rounds, at most 67 spaces and sixteen vectors; wide enumeration has ten +dimensions, 32 masks and at most 512 vectors. Benchmarking has ten subprocesses, +each with a 60-second timeout. All new functions are below 60 physical lines. +Explicit exceptions remain active under optimized Python. + +Power of Ten rules 3, 8 and 9 require managed-runtime deviations. Python +integers, JSON and containers allocate; fixed domains bound live collections. +One module with the exact source path is compiled from authenticated bytes, +and the verifier similarly loads the local evaluator. No generated expression +or user-supplied module name is executed, and bytecode caches are not read. +The retained source and six named control callbacks are the bounded indirect +targets. Their results are checked or intentionally discarded only where the +source also discards unused witness arrays. A future generic external-input +interface would require explicit capacity validation and a separate review. + +Warning-strict normal and optimized execution and AST/function-size inspection +are the available diagnostics. Inherited source style is preserved through +the immutable adapter rather than changed in a frozen package. This is an +opt-in evaluator, not a shared verifier or CI-selection change. diff --git a/research/p112-compatibility-kernels/SOURCES.json b/research/p112-compatibility-kernels/SOURCES.json new file mode 100644 index 0000000000..3dda8db8b5 --- /dev/null +++ b/research/p112-compatibility-kernels/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "research/sparse-redundant-decoder/verify.py", + "sha256": "7b0e3f5eb26f43c1ce4c3c5f72769f941dbc4c9698e97a58663d29501b117b56", + "git_blob": "c718ae77daab508ecc8a7091bac1f2af853c5142", + "usage": "input" + }, + { + "path": "research/sparse-redundant-decoder/CERTIFICATE.json", + "sha256": "3d347dc6be878b1e05fb545319628744c62b43d0c3d237641fe68901bc9355e5", + "git_blob": "c5fc4d5b06f4c1fae8e94fc1acac65180d2c5995", + "usage": "input" + }, + { + "path": "research/sparse-redundant-decoder/SOURCES.json", + "sha256": "3a82dc2a7a89e99b3ad16cf2f5005d809126d0d83b97f937b1896e1655e02b14", + "git_blob": "279f42f66921b2e151ab9bd5382c3826b10b234a", + "usage": "input" + }, + { + "path": "research/sparse-redundant-decoder/README.md", + "sha256": "e0a201011aa1eb0d3df0c0bef1bc598ffa29287af832336321fec173fab36fa5", + "git_blob": "f029f0d617311d1d1c0c11bb4fe99ce511db3c9f", + "usage": "input" + }, + { + "path": "research/sparse-redundant-decoder/PROOF.md", + "sha256": "7133bd2d095ddf06b0db6059e6234e8cd8fe7130c53922e5f22249b05600121c", + "git_blob": "99929e38b7d5f25a0b5459600c26dcdbd01d230a", + "usage": "input" + }, + { + "path": "research/complex-decoder-field-extension-seed44/PROOF.md", + "sha256": "a89530576d8a5e1ae8778d601b37140d954212cd46e06b87a3f565294ee251a2", + "git_blob": "4a3063de8fe606a88bd5bdb9b7d2e5dccb70f73f", + "usage": "input" + }, + { + "path": "research/complex-frame-pair-decoders/PROOF.md", + "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74", + "git_blob": "889f3a653ed1bdbb7df61ebe3af4f2103602a1f4", + "usage": "input" + }, + { + "path": "research/p112-single-lift/PROOF.md", + "sha256": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1", + "git_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a", + "usage": "input" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "research/sparse-redundant-decoder/independent.py", + "usage": "provenance", + "git_blob": "79bdb105c9693751c93f20afd9272665d2f91389", + "sha256": "bfeb28b49e58add76fd1e562f2342cd273b3a4bd1a7f112b81a780219765eeb2" + } + ] +} diff --git a/research/p112-compatibility-kernels/TASK.json b/research/p112-compatibility-kernels/TASK.json new file mode 100644 index 0000000000..71c40533f3 --- /dev/null +++ b/research/p112-compatibility-kernels/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "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": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact restriction-kernel evaluation of the complete PR1325 P112 plane-compatibility census, preserving its scientific receipt.", + "scope_change_reason": "The donation requires original work rather than predecessor validation. This changes the audit card to an implementation-preservation proof and a new exact evaluation algorithm for the unchanged finite census.", + "bottleneck_link": "Makes exact decoder screening cheaper without weakening finite coverage; supplies no physical COPY word or better exponent.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified complete-command improvement; do not extend the algorithm.", + "outcome": "completed", + "evidence": "PROOF.md; full certificate and ordered stream comparison; exhaustive small-subspace conformance; alternating complete CLI benchmark.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361674", + "open_questions": [ + { + "question": "Can the same restriction-kernel evaluator accelerate an explicitly different decoder census?", + "why_it_matters": "Larger source spaces make literal partner-vector scans expensive.", + "first_step": "Profile one complete command and expose its precise binary subspace restriction.", + "blocked_by": "Each source has a separate output, ordering and control contract; no automatic applicability is proved." + } + ] +} diff --git a/research/p112-compatibility-kernels/VERIFY.json b/research/p112-compatibility-kernels/VERIFY.json new file mode 100644 index 0000000000..7f1bfaaa4c --- /dev/null +++ b/research/p112-compatibility-kernels/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/sparse-redundant-decoder/verify.py", + "research/sparse-redundant-decoder/CERTIFICATE.json", + "research/sparse-redundant-decoder/SOURCES.json", + "research/sparse-redundant-decoder/README.md", + "research/sparse-redundant-decoder/PROOF.md", + "research/complex-decoder-field-extension-seed44/PROOF.md", + "research/complex-frame-pair-decoders/PROOF.md", + "research/p112-single-lift/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full optimized scientific receipt; all 67 four-dimensional binary subspaces and masks; 112-bit restriction fixtures; exact operation counters and boundary controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete conformance and source-bound replay under optimized Python." + } + ] +} diff --git a/research/p112-compatibility-kernels/benchmark.py b/research/p112-compatibility-kernels/benchmark.py new file mode 100644 index 0000000000..d5edbda96b --- /dev/null +++ b/research/p112-compatibility-kernels/benchmark.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +"""Alternate five complete source and kernel CLI runs. Nick Petalas.""" + +import argparse +import hashlib +import json +from pathlib import Path +import platform +import resource +import statistics +import subprocess +import sys +import time + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +EXPECTED = ("PASS_SPARSE_REDUNDANT_DECODER planes=32385 single_vectors=765 " + "minimum=64 all_active=65 equality_shifts=4 controls=6 no_new_kappa\n") + + +def measure(program): + argv = [sys.executable, "-I", "-O", "-W", "error", "-B", str(program)] + before = resource.getrusage(resource.RUSAGE_CHILDREN) + start = time.perf_counter() + result = subprocess.run(argv, cwd=ROOT, text=True, capture_output=True, timeout=60) + wall = time.perf_counter() - start + after = resource.getrusage(resource.RUSAGE_CHILDREN) + if result.returncode or result.stdout != EXPECTED or result.stderr: + raise ValueError("complete command failed: " + result.stdout + result.stderr) + return {"wall_seconds": wall, + "cpu_seconds": after.ru_utime + after.ru_stime - before.ru_utime - before.ru_stime, + "exit_code": result.returncode, "stdout_sha256": hashlib.sha256(result.stdout.encode()).hexdigest()} + + +def summary(rows): + values = [row["wall_seconds"] for row in rows] + return {"median_seconds": statistics.median(values), "minimum_seconds": min(values), + "maximum_seconds": max(values), "runs": rows} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", type=Path, required=True) + args = parser.parse_args() + programs = [("source", ROOT / "research/sparse-redundant-decoder/verify.py"), + ("kernel", HERE / "fast.py")] + samples = {name: [] for name, _ in programs} + for _ in range(5): + for name, program in programs: + samples[name].append(measure(program)) + result = {"python": sys.version, "platform": platform.platform(), + "argv_flags": ["-I", "-O", "-W", "error", "-B"], "errors": 0, + "order": ["source", "kernel"] * 5, + "timing_scope": "whole subprocess including interpreter, source hashes, census, witnesses, controls and receipt comparison", + **{name: summary(rows) for name, rows in samples.items()}} + with args.write.open("x", encoding="utf-8") as handle: + handle.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p112-compatibility-kernels/fast.py b/research/p112-compatibility-kernels/fast.py new file mode 100644 index 0000000000..9fbf12a255 --- /dev/null +++ b/research/p112-compatibility-kernels/fast.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Restriction-kernel evaluator, produced by Nick Petalas. + +The complete census and scientific contract are Philipp / mightyOil's PR1325. +The pinned predecessor stays unchanged. Apache-2.0. +""" + +import argparse +from collections import Counter +import hashlib +import json +from pathlib import Path +from types import ModuleType + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/sparse-redundant-decoder/verify.py" +MARKER = ("PASS_SPARSE_REDUNDANT_DECODER planes=32385 single_vectors=765 " + "minimum=64 all_active=65 equality_shifts=4 controls=6 no_new_kappa") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read_bytes(path): + with path.open("rb") as handle: + payload = handle.read(1048577) + need(len(payload) <= 1048576, "one MiB source capacity") + return payload + + +def load_source(): + pins = json.loads(read_bytes(HERE / "SOURCES.json")) + source_bytes = None + for item in pins["files"]: + if item["usage"] == "input": + path = ROOT / item["path"] + payload = read_bytes(path) + need(hashlib.sha256(payload).hexdigest() == item["sha256"], + "source hash: " + item["path"]) + if path == SOURCE: + source_bytes = payload + need(source_bytes is not None, "missing source pin") + source = ModuleType("p112_pinned_source") + source.__file__ = str(SOURCE) + # Compile the authenticated bytes directly; do not consult a bytecode cache. + exec(compile(source_bytes, str(SOURCE), "exec"), source.__dict__) + return source + + +def kernel_dimension(generators, mask): + """Dimension of vectors in span(generators) vanishing on mask. + + Callers supply an independent binary basis, at most nine 112-bit rows. + Restriction is linear; its nullity is d minus the restricted row rank. + """ + pivots = {} + for row in generators: + value = row & mask + for _ in range(9): + if not value: + break + pivot = value.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = value + break + value ^= pivots[pivot] + else: + raise ValueError("basis capacity exceeded") + return len(generators) - len(pivots) + + +def plane_census(source, spaces, bases, conflict): + planes = [] + stream = hashlib.sha256() + for anchor in range(3): + others = [k for k in range(4) if k != anchor] + census = Counter() + space = spaces[anchor] + for i, x in enumerate(space[1:], 1): + for y in space[i + 1:]: + if y >= x ^ y: + continue + union = x | y + dims = [kernel_dimension(bases[k], union & conflict[anchor][k]) + for k in others] + need(dims == [0, 0, 1], "plane compatibility dimensions") + census[tuple(dims)] += 1 + stream.update(source.canonical([anchor, x, y, dims]).encode() + b"\n") + need(sum(census.values()) == 10795, "complete plane count") + planes.append({"anchor": anchor, "partner_order": others, + "counts": {",".join(map(str, k)): v + for k, v in sorted(census.items())}}) + return planes, stream.hexdigest() + + +def single_census(spaces, bases, conflict): + single = [] + for anchor in range(3): + census = Counter() + for z in spaces[anchor][1:]: + dim = kernel_dimension(bases[3], z & conflict[anchor][3]) + need(dim <= 2, "nonzero coordinate deficiency forces extra deficiency <=2") + census[dim] += 1 + need(census == {1: 1, 2: 254}, "complete single-vector census") + single.append({"anchor": anchor, + "dimensions": {str(k): v for k, v in sorted(census.items())}}) + return single + + +def decoder_witnesses(source, roots, rows, supports): + witnesses = [] + shifts_list = [("zero", [0] * 112)] + shifts_list += [(f"coordinate_{j}", [r[j] for r in roots]) for j in range(3)] + for name, shifts in shifts_list: + info, _, _ = source.decode(roots, shifts, rows, supports) + need(info["total"] == 64 and info["active_terms"] == 8, "all equality witnesses") + witnesses.append({"name": name, **info}) + shifts = [0] * 112 + shifts[40] = 2 + info, d, t = source.decode(roots, shifts, rows, supports) + need(info["costs"] == [8] * 8 + [1] and info["active_terms"] == 9, + "sharp all-active witness") + witnesses.append({"name": "all_active_single_row", "row": 40, "shift": 2, **info}) + costs = [] + for s in range(12): + shifts = [((i * 17 + s * 13 + 40) % 7) - 3 for i in range(112)] + item, _, _ = source.decode(roots, shifts, rows, supports) + need(item["total"] >= 64, "finite shift check") + costs.append(item["total"]) + return witnesses, costs, d, t + + +def source_controls(source, roots, rows, spaces, d, t): + controls = [] + + def reject(name, operation): + try: + operation() + except ValueError: + controls.append(name) + else: + raise ValueError("control not rejected: " + name) + + damaged = [list(x) for x in d] + damaged[40][0] += 2 + reject("missing_shift_subtraction", lambda: source.check_identity(roots, damaged, t)) + damaged_t = [list(x) for x in t] + for i, row in enumerate(roots): + damaged_t[i][8] = row[0] + row[1] + reject("missing_third_normal_coordinate", + lambda: source.check_identity(roots, d, damaged_t)) + wrong = [row ^ ((1 << 112) - 1) for row in rows] + reject("missing_pairing_affine_one", + lambda: need(len(source.basis(wrong)) == 9, "binary pairing dimension")) + reject("unpunctured_unit", lambda: need( + [source.dimension(s) for s in source.setup(source.geometry(True))[3]] + == [8] * 8 + [9], "puncture contract")) + reject("omitted_ratio_conflict", + lambda: need(source.dimension(spaces[1]) == 0, "plane lemma missing conflicts")) + reject("incomplete_plane_inventory", + lambda: need(10794 == (255 * 254) // 6, "complete planes")) + return controls + + +def run(source): + sources = source.check_sources() + roots = source.geometry() + need(len(roots) == 112, "P112 frame puncture") + need(all(sum(r[j] * r[k] for r in roots) == (56 if j == k else 0) + for j in range(8) for k in range(8)), "real root span via R-transpose-R=56I") + _, rows, supports, allspaces = source.setup(roots) + need([source.dimension(s) for s in allspaces] == [8] * 8 + [9], + "column-code dimensions") + need(all(any(rows[i] >> j & 1 for j in y) + for y in supports for i in range(112)), "zero term cost iff row support empty") + spaces = [allspaces[k] for k in (0, 1, 2, 8)] + bases = [source.basis(space) for space in spaces] + need([len(b) for b in bases] == [8, 8, 8, 9], "restriction basis dimensions") + vals = [r[:3] + (0,) for r in roots] + conflict = [[sum((v[j] != v[k]) << i for i, v in enumerate(vals)) + for k in range(4)] for j in range(4)] + planes, plane_digest = plane_census(source, spaces, bases, conflict) + single = single_census(spaces, bases, conflict) + witnesses, costs, d, t = decoder_witnesses(source, roots, rows, supports) + controls = source_controls(source, roots, rows, spaces, d, t) + need(witnesses[-1]["total"] == 65 and witnesses[0]["total"] == 64, + "active/zero distinction") + return {"schema_version": 1, "scope": "fixed coordinate frame plus e0+e1+e2 on P112", + "base_commit": source.BASE, "roots": 112, "root_digest": source.digest(roots), + "pairing_digest": source.digest(rows), "column_support_sizes": list(map(len, supports)), + "column_code_dimensions": [source.dimension(s) for s in allspaces], + "planes": planes, "plane_count": 32385, "plane_stream_sha256": plane_digest, + "single_vector_census": single, "single_vectors": 765, "witnesses": witnesses, + "equality_shifts": ["0", "r0", "r1", "r2"], "all_active_minimum": 65, + "minimum": 64, "finite_example_costs": costs, + "identity_entries_checked": 17 * 112 * 112, "controls": controls, + "source_inputs": sources, "new_kappa": False} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", type=Path) + args = parser.parse_args() + source = load_source() + result = run(source) + if args.write: + with args.write.open("x", encoding="utf-8") as handle: + handle.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads((SOURCE.parent / "CERTIFICATE.json").read_text()) + need(source.canonical(result) == source.canonical(expected), "certificate exact replay") + print(MARKER) + + +if __name__ == "__main__": + main() diff --git a/research/p112-compatibility-kernels/verify.py b/research/p112-compatibility-kernels/verify.py new file mode 100644 index 0000000000..a433a1c156 --- /dev/null +++ b/research/p112-compatibility-kernels/verify.py @@ -0,0 +1,113 @@ +#!/usr/bin/env python3 +"""Finite conformance and a generated source-bound receipt. Nick Petalas.""" + +import hashlib +import json +from pathlib import Path +from types import ModuleType + + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_fast(): + path = HERE / "fast.py" + module = ModuleType("p112_fast") + module.__file__ = str(path) + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + return module + + +def small_subspaces(fast, source): + spaces = {frozenset({0})} + for _ in range(4): + expanded = set(spaces) + for space in spaces: + for vector in range(16): + expanded.add(space | frozenset(x ^ vector for x in space)) + spaces = expanded + need(len(spaces) <= 67, "four-dimensional subspace capacity") + need(len(spaces) == 67, "complete four-dimensional subspace census") + checks = 0 + for space in spaces: + basis = source.basis(sorted(space)) + for mask in range(16): + count = sum(not vector & mask for vector in space) + dimension = fast.kernel_dimension(basis, mask) + need(1 << dimension == count, "restriction kernel versus literal vector set") + checks += 1 + return checks + + +def wide_cases(fast): + checks = 0 + for dimension in range(10): + basis = [((1 << i) | (1 << (i + 50))) for i in range(dimension)] + for pattern in range(32): + mask = sum(((pattern >> (i % 5)) & 1) << i for i in range(112)) + count = 0 + for coefficients in range(1 << dimension): + value = 0 + for i in range(dimension): + if coefficients >> i & 1: + value ^= basis[i] + count += not value & mask + need(1 << fast.kernel_dimension(basis, mask) == count, "112-bit kernel fixture") + checks += 1 + return checks + + +def scientific_replay(fast, source): + counts = {"queries": 0, "masked_basis_rows": 0} + original = fast.kernel_dimension + + def counted(basis, mask): + counts["queries"] += 1 + counts["masked_basis_rows"] += len(basis) + return original(basis, mask) + + fast.kernel_dimension = counted + try: + result = fast.run(source) + finally: + fast.kernel_dimension = original + expected = json.loads((fast.SOURCE.parent / "CERTIFICATE.json").read_text()) + need(source.canonical(result) == source.canonical(expected), "complete scientific receipt") + need(counts == {"queries": 97920, "masked_basis_rows": 816510}, "full kernel work count") + baseline_rows = 32385 * (256 + 256 + 512) + 765 * 512 + need(baseline_rows == 33553920, "literal predecessor mask count") + return result, {**counts, "predecessor_masked_vectors": baseline_rows} + + +def controls(fast): + need(fast.kernel_dimension([], (1 << 112) - 1) == 0, "zero space") + need(fast.kernel_dimension([1, 2, 4], 0) == 3, "zero restriction") + need(fast.kernel_dimension([1, 2, 4], 7) == 0, "injective restriction") + need(fast.kernel_dimension([3, 5], 1) == 1, "restriction-dependent basis images") + need(fast.kernel_dimension([1 << 111], 1 << 111) == 0, "highest permitted bit") + return 5 + + +def main(): + fast = load_fast() + source = fast.load_source() + small = small_subspaces(fast, source) + wide = wide_cases(fast) + control_count = controls(fast) + result, work = scientific_replay(fast, source) + names = ["README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "fast.py", "verify.py", "benchmark.py"] + hashes = {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() for name in names} + receipt = {"status": "PASS_P112_COMPATIBILITY_KERNELS", "small_cases": small, + "wide_cases": wide, "controls": control_count, "work": work, + "scientific_sha256": source.digest(result), "package_sha256": hashes} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()