diff --git a/certificates/affine-vector-screens.json b/certificates/affine-vector-screens.json index 7553cd304e..2b13cf1dee 100644 --- a/certificates/affine-vector-screens.json +++ b/certificates/affine-vector-screens.json @@ -143,7 +143,7 @@ "source_sha256": { "docs/research/affine-vector-screens.md": "22e5beab6df8127fc4377142768fc1a0a3317d7e8fba52c089670ecf1aa076b6", "scripts/audit_affine_vectors.py": "a3fccaeadb9a5db72c33787a055a54374504a6aa231907080396b2cf822e94a7", - "scripts/experiments/affine_vector_screens.py": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", + "scripts/experiments/affine_vector_screens.py": "c499289fc25b5d180df22f70694a7b1c4cfed68f00a9a59bbf4f7ae1b52327a9", "scripts/experiments/affine_vector_witnesses.json": "672a4318c48f5286ce088d34736c38957b7f662a5f753d440dbc638e7da5f62a", "scripts/experiments/cube_core_family.py": "e58f1f4067bda2d4838343f42ec2505316f006561f0702e869847d88b85413a8", "scripts/experiments/single_intersection.py": "6874d41b75590369182ed61e0c6da5b547e035e0e43b50ea2b39e1f3861dca6d" diff --git a/research/leech-minor-production/NOTICE.md b/research/leech-minor-production/NOTICE.md new file mode 100644 index 0000000000..1a1e60116a --- /dev/null +++ b/research/leech-minor-production/NOTICE.md @@ -0,0 +1,20 @@ +# Attribution and license + +Prepared by Wentao Li ([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor), wentaol4@illinois.edu) with substantial +AI assistance for orientation, overlap search, profiling, production wiring, +packaging, benchmarking and writing. Not independent human peer review. +Apache-2.0; see the repository root `LICENSE`. + +The exact base-256 byte-lane algorithm and its no-carry argument were introduced +by **Jerry Chen (@CubeJerry)** in the opt-in adapter +`research/leech-minor-byte-lanes/` (incorporated +[CrocSwap/integer-mult-bounds#898](https://github.com/CrocSwap/integer-mult-bounds/pull/898); +see that package's NOTICE.md). This package wires an equivalent check into the +production `scripts/experiments/affine_vector_screens.py:leech_minor` path used +by `make verify-certificates`. + +The original affine/vector screens, Golay inventory, Leech line generators, +rational span witnesses, binary elimination and nine-screen certificate are by +**Douglas R. Colkitt**. Upstream material retains its own source notices and +license. diff --git a/research/leech-minor-production/README.md b/research/leech-minor-production/README.md new file mode 100644 index 0000000000..9c34f8fe7a --- /dev/null +++ b/research/leech-minor-production/README.md @@ -0,0 +1,103 @@ +# Production byte-lane Leech-minor rows + +**Tooling improvement; no new kappa.** At base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, +`scripts/experiments/affine_vector_screens.py:leech_minor` still built each +binary row with the historical pairwise sparse-dot genexpr. Jerry Chen's +opt-in adapter `research/leech-minor-byte-lanes/` (incorporated +[CrocSwap/integer-mult-bounds#898](https://github.com/CrocSwap/integer-mult-bounds/pull/898)) +already proved an exact base-256 byte-lane algorithm with identical receipts. +This package wires that equivalent check into the **production** source used by +`scripts/audit_affine_vectors.py` / `make verify-certificates`. + +Only the source pin for `scripts/experiments/affine_vector_screens.py` changes +inside `certificates/affine-vector-screens.json`. Every matrix entry is still +materialised; Golay inventory, norms, rational span witnesses, binary +elimination, polynomial-code screens and the retained historical `2^-31` +language are unchanged. Selected frontier untouched. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/leech-minor-production/verify.py +python3.12 -I -O -B research/leech-minor-production/verify.py +python3.12 -B scripts/research_package.py --package research/leech-minor-production +python3.12 -I -B research/leech-minor-production/benchmark.py --rounds 5 +``` + +Expected: + +```text +PASS_LEECH_MINOR_PRODUCTION leech_cases=5 code_cases=4 certs=1 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/leech-minor-production outcome=completed +PASS_IDENTICAL_LEECH_MINOR_PRODUCTION_RECEIPTS +``` + +Default verify is read-only. Use `--write-certificate` only after editing the +production source. Timing is host-descriptive and is not a correctness gate. + +On Linux / CPython 3.12.3, five alternating fresh-process pairs gave median +**leech-only 5.579 → 1.043 s (5.35×)** and **complete audit 9.465 → 4.213 s +(2.25×)**. Samples are in [`RESULT.json`](RESULT.json). + +## Why the byte lanes are equivalent + +Coordinates of every Leech sample vector lie in `[-4,4]`. For each coordinate +`k`, pack nonnegative base-256 integers + +```text +P_k = sum_j (v_j[k] + 4) 256^j +M_k = sum_j (4 - v_j[k]) 256^j +``` + +For a row vector `u` with `||u||_1 <= 31` (true of every historical Leech row: +l1 norms 8, 16 or 26), + +```text +S_u = sum_{u[k]>0} u[k] P_k + sum_{u[k]<0} (-u[k]) M_k +``` + +has byte `j` equal to `dot(u,v_j) + 4 ||u||_1`, with every digit at most +`8*31 < 256` and no inter-column carries. Decoding bytes and comparing to +`shift + 4 ||u||_1`, while forcing the diagonal, returns exactly +`C[i,j] = (i == j or dot(v_i,v_j) == shift)` in the original column order. +This is the same argument as `research/leech-minor-byte-lanes/README.md`. + +## Overlap and credit + +Closest priors: + +- [Jerry Chen / leech-minor-byte-lanes](../leech-minor-byte-lanes/) — opt-in + byte-lane adapter (#898 incorporated); this package is the production wiring. +- [CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756) + — identical-receipt tooling quality bar. +- Open leave-alone tooling on other objects (#1922 joint frames, #2054/#2150 + shared/mixed-point, #2100 ternary, #2117 DisjointTensor.frame_data, #2194 + production verify_factor, #1861 parity-side) was not reopened. + +Douglas R. Colkitt authored the affine/vector screens and original checker. +Jerry Chen authored the byte-lane algorithm. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance, under +Apache-2.0. + +## Open next questions + +1. **Question:** Should the four polynomial-code screens in the same audit + receive a similar production packing pass? + **Why it matters:** After Leech minors shrink, the unchanged cubic-code path + is a larger share of the complete audit. + **First step:** Profile `audit_affine_vectors.certificate` with production + lanes already merged. + **Blocked by:** No open identical-receipt adapter yet for + `polynomial_code_witness`. + +2. **Question:** Should `research/leech-minor-byte-lanes/` note that production + now ships the same algorithm? + **Why it matters:** That package's source-admission string match expects the + historical pairwise block. + **First step:** Add a one-line status note without editing pinned evidence. + **Blocked by:** Maintainer preference on touching incorporated historical + packages. diff --git a/research/leech-minor-production/RESULT.json b/research/leech-minor-production/RESULT.json new file mode 100644 index 0000000000..79916b565f --- /dev/null +++ b/research/leech-minor-production/RESULT.json @@ -0,0 +1,142 @@ +{ + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, implementation, packaging, benchmarking and writing. Not independent human peer review.", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "complete_audit": { + "median_baseline_seconds": 9.46477570900015, + "median_optimized_seconds": 4.212500120000186, + "median_ratio": 2.246830964837986, + "rounds": 5, + "samples": [ + { + "baseline_seconds": 9.46477570900015, + "optimized_seconds": 4.516600023000137, + "order": [ + "baseline", + "optimized" + ], + "ratio": 2.0955532171992513, + "round": 0 + }, + { + "baseline_seconds": 12.871481419000247, + "optimized_seconds": 4.212500120000186, + "order": [ + "optimized", + "baseline" + ], + "ratio": 3.0555444634621587, + "round": 1 + }, + { + "baseline_seconds": 10.286713764999604, + "optimized_seconds": 5.023797816999831, + "order": [ + "baseline", + "optimized" + ], + "ratio": 2.047597084856958, + "round": 2 + }, + { + "baseline_seconds": 9.034710279999672, + "optimized_seconds": 4.105965091000144, + "order": [ + "optimized", + "baseline" + ], + "ratio": 2.2003865302710035, + "round": 3 + }, + { + "baseline_seconds": 8.674803519999841, + "optimized_seconds": 3.795328679999784, + "order": [ + "baseline", + "optimized" + ], + "ratio": 2.2856527725025213, + "round": 4 + } + ], + "scope": "audit" + }, + "engines": { + "baseline": "research/leech-minor-production/baseline.py", + "optimized": "scripts/experiments/affine_vector_screens.py" + }, + "environment": { + "cpu_affinity_set": false, + "executable": "/usr/bin/python3.12", + "implementation": "CPython", + "os_caches_flushed": false, + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]" + }, + "leech_only": { + "median_baseline_seconds": 5.579358917999798, + "median_optimized_seconds": 1.0430829469996752, + "median_ratio": 5.348912024732329, + "rounds": 5, + "samples": [ + { + "baseline_seconds": 5.555424422000215, + "optimized_seconds": 0.6638417809999737, + "order": [ + "baseline", + "optimized" + ], + "ratio": 8.368597128116638, + "round": 0 + }, + { + "baseline_seconds": 5.502019425999606, + "optimized_seconds": 1.0430829469996752, + "order": [ + "optimized", + "baseline" + ], + "ratio": 5.274766922252559, + "round": 1 + }, + { + "baseline_seconds": 5.914984036000078, + "optimized_seconds": 0.8409578649998366, + "order": [ + "baseline", + "optimized" + ], + "ratio": 7.033627108061148, + "round": 2 + }, + { + "baseline_seconds": 5.984793322999849, + "optimized_seconds": 1.187062658999821, + "order": [ + "optimized", + "baseline" + ], + "ratio": 5.041682743219666, + "round": 3 + }, + { + "baseline_seconds": 5.579358917999798, + "optimized_seconds": 1.1603133880003043, + "order": [ + "baseline", + "optimized" + ], + "ratio": 4.808493098244192, + "round": 4 + } + ], + "scope": "leech" + }, + "no_new_kappa": true, + "predecessor": "research/leech-minor-byte-lanes/", + "source_sha256": { + "baseline.py": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", + "research/leech-minor-byte-lanes/lanes.py": "2c242d4284e1c8520cbc0cfbbb20ddf186c662e5f6173bed400bbd4022df34c7", + "scripts/experiments/affine_vector_screens.py": "c499289fc25b5d180df22f70694a7b1c4cfed68f00a9a59bbf4f7ae1b52327a9" + }, + "status": "PASS_IDENTICAL_LEECH_MINOR_PRODUCTION_RECEIPTS" +} diff --git a/research/leech-minor-production/SOURCES.json b/research/leech-minor-production/SOURCES.json new file mode 100644 index 0000000000..950049f79c --- /dev/null +++ b/research/leech-minor-production/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "certificates/affine-vector-screens.json", + "usage": "provenance", + "git_blob": "7553cd304e62c7a3c9136046663d418cb068f0e8", + "sha256": "e7920c3305bd5e3058d2614fadc064ec1f658029183325f600c7ee4b56a7906e" + }, + { + "path": "docs/research/affine-vector-screens.md", + "usage": "provenance", + "git_blob": "13f454478b554408cb55fdb31d514162b5c4b241", + "sha256": "22e5beab6df8127fc4377142768fc1a0a3317d7e8fba52c089670ecf1aa076b6" + }, + { + "path": "scripts/audit_affine_vectors.py", + "usage": "provenance", + "git_blob": "9f5e3dff5e7c0444d160fec3a773fd702b0bc569", + "sha256": "a3fccaeadb9a5db72c33787a055a54374504a6aa231907080396b2cf822e94a7" + }, + { + "path": "scripts/experiments/affine_vector_screens.py", + "usage": "provenance", + "git_blob": "0686b47d4844bedc9dddfacb0bff52ec552120a2", + "sha256": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1" + }, + { + "path": "scripts/experiments/affine_vector_witnesses.json", + "usage": "input", + "git_blob": "0e9a488ac4912cbf2bb83894c1b6c9b607cc02cd", + "sha256": "672a4318c48f5286ce088d34736c38957b7f662a5f753d440dbc638e7da5f62a" + }, + { + "path": "research/leech-minor-byte-lanes/lanes.py", + "usage": "input", + "git_blob": "095173fba90d619d8ff9cc46e28431af85fee65d", + "sha256": "2c242d4284e1c8520cbc0cfbbb20ddf186c662e5f6173bed400bbd4022df34c7" + }, + { + "path": "research/leech-minor-byte-lanes/README.md", + "usage": "provenance", + "git_blob": "f6f50385e8f08aea1b1eda245681b4add515cdc2", + "sha256": "5ac99737af9ab3422faef2825d8e592d32d7dcb90fff83cd025702e895fead26" + } + ] +} diff --git a/research/leech-minor-production/TASK.json b/research/leech-minor-production/TASK.json new file mode 100644 index 0000000000..9872f134a7 --- /dev/null +++ b/research/leech-minor-production/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_seed": "18e9e0f2162f8e721bb7a7069be16c7f", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Can the production affine-vector Leech-minor checker (scripts/experiments/affine_vector_screens.py:leech_minor, exercised by scripts/audit_affine_vectors.py / certificates/affine-vector-screens.json) adopt the exact base-256 byte-lane row construction from research/leech-minor-byte-lanes/ so the shipped verify-certificates path is faster while every matrix entry, row digest, binary rank and admission flag stays identical?", + "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. Expertise override selected verifier-engineering after profiling make verify-certificates poles. Leave-alone objects (joint frames, shared-point, mixed-point verify, ternary frames, parity-side, DisjointTensor.frame_data, production verify_factor) and deferred micro-opts were not reopened. Jerry Chen's incorporated #898 already proved an opt-in identical-receipt accelerator; production still used the historical pairwise sparse-dot genexpr.", + "bottleneck_link": "Side result on review throughput: affine-vector screens are part of verify-certificates. Faster identical Leech-minor rows do not change kappa or the binding complex supplier.", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, packaging, benchmarking and writing", + "outcome": "completed", + "evidence": "PASS_LEECH_MINOR_PRODUCTION via research/leech-minor-production/verify.py (also under -O); PASS_IDENTICAL_LEECH_MINOR_PRODUCTION_RECEIPTS via benchmark.py; certificates/affine-vector-screens.json differs from base only in the affine_vector_screens.py source pin.", + "author": "Wentao Li", + "email": "wentaol4@illinois.edu", + "github": "VictorLiwentao", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving production leech_minor change with frozen baseline, identical Leech and full-audit payloads, rejection/temp-corruption controls, certificate pin discipline, registered replay and a measured before/after median. Do not invent kappa or reopen leave-alone objects.", + "open_questions": [ + { + "question": "Should the four polynomial-code screens in the same audit receive a similar production packing pass?", + "why_it_matters": "After Leech minors shrink, the unchanged cubic-code xor_permute path is a larger share of the complete audit.", + "first_step": "Profile audit_affine_vectors.certificate with production lanes already merged and name the residual hot function.", + "blocked_by": "No open identical-receipt adapter yet for polynomial_code_witness." + }, + { + "question": "Should research/leech-minor-byte-lanes/ document that production now ships the same algorithm?", + "why_it_matters": "The frozen opt-in adapter's source-admission string match will fail against the new production block if rerun as-is.", + "first_step": "Add a one-line status note to that package README without editing its pinned evidence.", + "blocked_by": "Maintainer preference on touching incorporated historical packages." + } + ] +} diff --git a/research/leech-minor-production/VERIFY.json b/research/leech-minor-production/VERIFY.json new file mode 100644 index 0000000000..d06b5e3892 --- /dev/null +++ b/research/leech-minor-production/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/leech-minor-byte-lanes/lanes.py", + "certificates/affine-vector-screens.json", + "scripts/experiments/affine_vector_screens.py", + "scripts/experiments/affine_vector_witnesses.json", + "scripts/audit_affine_vectors.py" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 300, + "checks": "Exact baseline copy of the base-commit affine_vector_screens.py; identical leech_minor receipts on all five frozen fixtures; rejection and temp-copy corruption controls; certificate differs from base only in the affine_vector_screens.py source pin; duplicate JSON-key check; read-only default." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 300, + "checks": "Same equivalence and pin discipline under -O (require() gates remain)." + } + ] +} diff --git a/research/leech-minor-production/baseline.py b/research/leech-minor-production/baseline.py new file mode 100644 index 0000000000..0686b47d48 --- /dev/null +++ b/research/leech-minor-production/baseline.py @@ -0,0 +1,120 @@ +"""Exact finite screens for specified affine inner-product zero patterns. + +A rank rejection concerns C=I plus the entire stated relation, not all +binary matrices supported on it and not all subfamilies of these vectors. +""" +from collections import Counter +from functools import cache +from itertools import combinations +from hashlib import sha256 + +from certify import require +from audit_joint_frames import matrix,rank +from experiments.single_intersection import rank_of_rows +from experiments.cube_core_family import xor_permute + + +@cache +def golay_code(): + generator=sum(1<>i&1:value^=generator<>i&1] + for mask in range(128): + if mask.bit_count()%2:continue + v=[0]*24;v[support[0]]=2 + for j,i in enumerate(support[1:]):v[i]=-2 if mask>>j&1 else 2 + out.append(tuple(v)) + require(len(out)==552+48576,'Wrong octad count') + for i in range(24): + for word in golay_code(): + if (word&1)!=int(i==0):continue + v=[-1 if word>>j&1 else 1 for j in range(24)];v[i]*=-3;out.append(tuple(v)) + require(len(out)==len(set(out))==98280,'Wrong number of distinct lines') + require(all(sum(x*x for x in v)==32 and next(x for x in v if x)>0 for v in out), + 'Wrong norm or antipodal normalization') + # The two-coordinate vectors alone span all 24 rational coordinates. + require(rank(matrix([out[i] for i in [0]+list(range(1,46,2))]))==24, + 'Rational ambient rank is not certified') + return tuple(out) + + +def leech_minor(global_indices, independent_rows, shift=0, signed=False): + require(shift in (-16,-8,0,8,16),'Unsupported affine offset') + require(signed or shift==0,'Shifted cases here use the full signed family') + lines=leech_lines();size=len(lines);n=size*(2 if signed else 1);d=24+int(shift!=0) + require(global_indices and len(set(global_indices))==len(global_indices) + and all(type(i) is int and 0<=i=n, + independent_rows_sha256=digest.hexdigest(),full_matrix_expanded=False) + + +def polynomial_code_base(extra): + """RM(2,5) without constants, enlarged by the listed cubic monomials.""" + require(all(len(S)==3 and tuple(sorted(set(S)))==tuple(S) + and all(type(i) is int and 0<=i<5 for i in S) for S in extra), + 'Use distinct-coordinate cubic monomials') + require(len(set(map(tuple,extra)))==len(extra) and len(extra)<=3,'Code discovery size exceeded') + monomials=[S for degree in (1,2) for S in combinations(range(5),degree)]+list(map(tuple,extra)) + basis=[sum(1<>i&1 for i in S)) for S in monomials] + require(rank_of_rows(basis)==len(basis),'Polynomial code generators are dependent') + n=1<>1);bit=gray^old;old=gray;value^=basis[bit.bit_length()-1] + if value.bit_count()==16:data[gray//8]|=1<<(gray%8) + # Linear polynomials give all 32 real Walsh characters, an orthogonal basis. + walsh=[[1-2*((a&x).bit_count()%2) for x in range(32)] for a in range(32)] + require(all(sum(x*y for x,y in zip(u,v))==32*int(i==j) + for i,u in enumerate(walsh) for j,v in enumerate(walsh)), 'Walsh rank witness failed') + return dict(n=n,d=32,basis=basis,base=int.from_bytes(data,'little'), + base_sha256=sha256(data).hexdigest()) + + +def polynomial_code_witness(extra, independent_rows): + data=polynomial_code_base(extra);n=data['n'] + require(independent_rows and len(set(independent_rows))==len(independent_rows) + and all(type(i) is int and 0<=i=n,base_sha256=data['base_sha256'], + full_matrix_expanded=False) diff --git a/research/leech-minor-production/benchmark.py b/research/leech-minor-production/benchmark.py new file mode 100644 index 0000000000..a55ea904c2 --- /dev/null +++ b/research/leech-minor-production/benchmark.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process before/after timings for production Leech lanes. + +Timing is descriptive evidence for RESULT.json. Equivalence is enforced by +verify.py; this script fails only on unequal receipts or subprocess errors. +""" +from __future__ import annotations + +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent + +WORKER = r""" +import importlib.util +import json +import sys +import time +from pathlib import Path + +root = Path(sys.argv[1]) +engine = sys.argv[2] +scope = sys.argv[3] +sys.path.insert(0, str(root / "scripts")) + +if engine == "baseline": + spec = importlib.util.spec_from_file_location( + "affine_vector_screens_baseline", + root / "research/leech-minor-production/baseline.py", + ) + screens = importlib.util.module_from_spec(spec) + spec.loader.exec_module(screens) +else: + from experiments import affine_vector_screens as screens + +data = json.loads((root / "scripts/experiments/affine_vector_witnesses.json").read_text()) +# Warm shared Golay / Leech inventories outside the timed window. +screens.leech_lines() + +if scope == "leech": + t0 = time.perf_counter() + receipts = [screens.leech_minor(**fixture) for fixture in data["leech"]] + elapsed = time.perf_counter() - t0 + print(json.dumps({"elapsed": elapsed, "receipts": receipts}, sort_keys=True)) +else: + import audit_affine_vectors as audit + import experiments.affine_vector_screens as live + from prepare_layers import serializable + + # audit_affine_vectors binds leech_minor at import time; patch both. + live.leech_minor = screens.leech_minor + audit.leech_minor = screens.leech_minor + t0 = time.perf_counter() + cert = audit.certificate() + elapsed = time.perf_counter() - t0 + payload = serializable(cert) + payload.pop("source_sha256", None) + print(json.dumps({"elapsed": elapsed, "payload": payload}, sort_keys=True)) +""" + + +def run_engine(engine: str, scope: str) -> dict: + env = os.environ.copy() + env.pop("PYTHONOPTIMIZE", None) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run( + [sys.executable, "-I", "-B", "-c", WORKER, str(ROOT), engine, scope], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + check=False, + ) + if proc.returncode != 0: + raise SystemExit(f"engine={engine} scope={scope} failed\n{proc.stderr}\n{proc.stdout}") + return json.loads(proc.stdout.strip().splitlines()[-1]) + + +def measure(scope: str, rounds: int) -> dict: + baseline_samples = [] + optimized_samples = [] + reference = None + samples = [] + for round_index in range(rounds): + order = ("baseline", "optimized") if round_index % 2 == 0 else ("optimized", "baseline") + pair = {} + for engine in order: + payload = run_engine(engine, scope) + key = "receipts" if scope == "leech" else "payload" + if reference is None: + reference = payload[key] + elif payload[key] != reference: + raise SystemExit(f"receipt mismatch scope={scope} round={round_index} engine={engine}") + pair[engine] = payload["elapsed"] + baseline_samples.append(pair["baseline"]) + optimized_samples.append(pair["optimized"]) + samples.append( + { + "round": round_index, + "order": list(order), + "baseline_seconds": pair["baseline"], + "optimized_seconds": pair["optimized"], + "ratio": pair["baseline"] / pair["optimized"] if pair["optimized"] else None, + } + ) + print( + f"scope={scope} round={round_index} order={order[0]}->{order[1]} " + f"baseline={pair['baseline']:.6f}s optimized={pair['optimized']:.6f}s", + flush=True, + ) + base_med = statistics.median(baseline_samples) + opt_med = statistics.median(optimized_samples) + return { + "scope": scope, + "rounds": rounds, + "median_baseline_seconds": base_med, + "median_optimized_seconds": opt_med, + "median_ratio": base_med / opt_med if opt_med else None, + "samples": samples, + } + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--output", type=Path, default=PACKAGE / "RESULT.json") + args = parser.parse_args(argv) + if args.rounds < 1: + raise SystemExit("--rounds must be >= 1") + + leech = measure("leech", args.rounds) + audit = measure("audit", args.rounds) + result = { + "status": "PASS_IDENTICAL_LEECH_MINOR_PRODUCTION_RECEIPTS", + "ai_assistance": ( + "Substantial AI assistance for orientation, overlap search, profiling, " + "implementation, packaging, benchmarking and writing. Not independent " + "human peer review." + ), + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessor": "research/leech-minor-byte-lanes/", + "engines": { + "baseline": "research/leech-minor-production/baseline.py", + "optimized": "scripts/experiments/affine_vector_screens.py", + }, + "source_sha256": { + "baseline.py": sha256((PACKAGE / "baseline.py").read_bytes()).hexdigest(), + "scripts/experiments/affine_vector_screens.py": sha256( + (ROOT / "scripts/experiments/affine_vector_screens.py").read_bytes() + ).hexdigest(), + "research/leech-minor-byte-lanes/lanes.py": sha256( + (ROOT / "research/leech-minor-byte-lanes/lanes.py").read_bytes() + ).hexdigest(), + }, + "environment": { + "python": sys.version, + "executable": sys.executable, + "platform": platform.platform(), + "implementation": platform.python_implementation(), + "os_caches_flushed": False, + "cpu_affinity_set": False, + }, + "leech_only": leech, + "complete_audit": audit, + "no_new_kappa": True, + } + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print(result["status"]) + print( + f"leech_median {leech['median_baseline_seconds']:.6f} -> " + f"{leech['median_optimized_seconds']:.6f} ({leech['median_ratio']:.3f}x)" + ) + print( + f"audit_median {audit['median_baseline_seconds']:.6f} -> " + f"{audit['median_optimized_seconds']:.6f} ({audit['median_ratio']:.3f}x)" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/leech-minor-production/verify.py b/research/leech-minor-production/verify.py new file mode 100644 index 0000000000..c369fa04b6 --- /dev/null +++ b/research/leech-minor-production/verify.py @@ -0,0 +1,204 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and rejection controls for production Leech byte lanes. + +Read-only by default. Regenerates no certificate unless --write-certificate is +passed. Timing is not a pass gate; see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +from copy import deepcopy +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +SCRIPTS = ROOT / "scripts" +sys.path.insert(0, str(SCRIPTS)) + +from certify import require # noqa: E402 +from prepare_layers import serializable # noqa: E402 +from audit_affine_vectors import certificate as production_certificate # noqa: E402 +from experiments import affine_vector_screens as production # noqa: E402 + +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ORIGINAL_BLOB = "0686b47d4844bedc9dddfacb0bff52ec552120a2" +ORIGINAL_SHA256 = "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1" +BASE_CERTIFICATE_SHA256 = "e7920c3305bd5e3058d2614fadc064ec1f658029183325f600c7ee4b56a7906e" +WITNESSES = SCRIPTS / "experiments" / "affine_vector_witnesses.json" + + +def load_module(path: Path, name: str): + spec = importlib.util.spec_from_file_location(name, path) + require(spec is not None and spec.loader is not None, f"missing module {path}") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def unique_object(pairs): + out = {} + for key, value in pairs: + require(key not in out, f"duplicate JSON key: {key}") + out[key] = value + return out + + +def load_json_unique(path: Path) -> dict: + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_object) + + +def load_base_certificate_bytes() -> bytes: + return subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:certificates/affine-vector-screens.json"], + cwd=ROOT, + ) + + +def check_baseline_bytes() -> None: + original = subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:scripts/experiments/affine_vector_screens.py"], + cwd=ROOT, + ) + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base affine_vector_screens.py sha256 drift") + require( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:scripts/experiments/affine_vector_screens.py"], + cwd=ROOT, + ) + .decode() + .strip() + == ORIGINAL_BLOB, + "base affine_vector_screens.py blob drift", + ) + require( + (PACKAGE / "baseline.py").read_bytes() == original, + "baseline.py must be an exact copy of the base-commit source", + ) + + +def check_leech_equivalence(baseline, optimized) -> list[dict]: + data = load_json_unique(WITNESSES) + rows = [] + for fixture in data["leech"]: + old = baseline.leech_minor(**fixture) + new = optimized.leech_minor(**fixture) + require(old == new, f"leech_minor receipt differs for shift={fixture.get('shift')}") + require(old["positive_deficit_excluded"], "admission flag lost") + require(old["binary_rank_lower"] == len(fixture["independent_rows"]), "rank mismatch") + rows.append(old) + require(len(rows) == 5, "expected five frozen Leech minors") + return rows + + +def check_rejections(baseline, optimized) -> None: + for eng, name in ((baseline, "baseline"), (optimized, "optimized")): + try: + eng.leech_minor([0, 0], [0]) + raise AssertionError(f"{name} accepted duplicate global indices") + except ValueError as exc: + require("index" in str(exc).lower() or "invalid" in str(exc).lower(), str(exc)) + try: + eng.leech_minor([0], [0], shift=3) + raise AssertionError(f"{name} accepted unsupported shift") + except ValueError as exc: + require("offset" in str(exc).lower() or "shift" in str(exc).lower(), str(exc)) + try: + eng.leech_minor([0, 1], [0, 1], shift=-8, signed=False) + raise AssertionError(f"{name} accepted shifted unsigned family") + except ValueError as exc: + require("signed" in str(exc).lower() or "shift" in str(exc).lower(), str(exc)) + + +def check_temp_corruption(optimized) -> None: + with tempfile.TemporaryDirectory(prefix="leech-minor-prod-") as tmp: + dest = Path(tmp) / "affine_vector_screens.py" + shutil.copy2(SCRIPTS / "experiments" / "affine_vector_screens.py", dest) + text = dest.read_text(encoding="utf-8") + # Drop every selected bit (including the forced diagonal) so the binary + # rank gate must reject the frozen independent-row witness. + mutated = text.replace( + "if i == j or value == shift + offset", + "if False", + 1, + ) + require(mutated != text, "mutation did not edit production source text") + dest.write_text(mutated, encoding="utf-8") + mutant = load_module(dest, "affine_vector_screens_mutant") + data = load_json_unique(WITNESSES) + fixture = data["leech"][0] + try: + mutant.leech_minor(**fixture) + raise AssertionError("mutant accepted a zero-row lane decode") + except ValueError as exc: + require( + "dependent" in str(exc).lower() or "independent" in str(exc).lower(), + str(exc), + ) + # Production path still accepts the frozen fixture. + optimized.leech_minor(**fixture) + + +def check_certificate(write: bool) -> dict: + result = production_certificate() + path = ROOT / "certificates" / "affine-vector-screens.json" + text = json.dumps(serializable(result), indent=2, sort_keys=True) + "\n" + if write: + path.write_text(text, encoding="utf-8") + committed = path.read_text(encoding="utf-8") + require( + committed == text, + "working certificates/affine-vector-screens.json does not match regenerated certificate()", + ) + load_json_unique(path) + base = load_base_certificate_bytes() + require(sha256(base).hexdigest() == BASE_CERTIFICATE_SHA256, "base certificate sha256 drift") + old = json.loads(base.decode("utf-8")) + new = json.loads(committed) + old_pin = old["source_sha256"].pop("scripts/experiments/affine_vector_screens.py") + new_pin = new["source_sha256"].pop("scripts/experiments/affine_vector_screens.py") + require(old_pin == ORIGINAL_SHA256, "unexpected base pin") + require( + new_pin == digest_file(SCRIPTS / "experiments" / "affine_vector_screens.py"), + "certificate pin != working source", + ) + require(old == new, "certificate changed outside the single affine_vector_screens.py source pin") + return result + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write-certificate", + action="store_true", + help="rewrite certificates/affine-vector-screens.json (default: read-only check)", + ) + args = parser.parse_args(argv) + + check_baseline_bytes() + baseline = load_module(PACKAGE / "baseline.py", "affine_vector_screens_baseline") + rows = check_leech_equivalence(baseline, production) + check_rejections(baseline, production) + check_temp_corruption(production) + result = check_certificate(write=args.write_certificate) + print( + "PASS_LEECH_MINOR_PRODUCTION " + f"leech_cases={len(rows)} " + f"code_cases={len(result['polynomial_code_screens'])} " + "certs=1 no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/experiments/affine_vector_screens.py b/scripts/experiments/affine_vector_screens.py index 0686b47d48..1262596e88 100644 --- a/scripts/experiments/affine_vector_screens.py +++ b/scripts/experiments/affine_vector_screens.py @@ -59,7 +59,48 @@ def leech_lines(): return tuple(out) +def _leech_lane_rows(sample, indices, shift): + """Exact C[i,j]=(i==j or dot(sample[i],sample[j])==shift) via base-256 lanes. + + Coordinates lie in [-4,4]. Each selected row has l1 norm <= 31, so every + accumulated digit is at most 8*31 < 256 (no inter-column carries). This is + the production form of research/leech-minor-byte-lanes/; every matrix entry + is still materialised and checked. + """ + require(sample and sample[0], 'Empty sample') + dimension = len(sample[0]) + require(all(len(v) == dimension and + all(type(x) is int and -4 <= x <= 4 for x in v) + for v in sample), 'Invalid byte-lane coordinates') + require(indices and len(set(indices)) == len(indices) and + all(type(i) is int and 0 <= i < len(sample) for i in indices), + 'Invalid selected rows') + require(type(shift) is int, 'Integer shift required') + require(all(sum(abs(x) for x in sample[i]) <= 31 for i in indices), + 'Byte-lane carry bound exceeded') + plus = [int.from_bytes(bytes(v[k] + 4 for v in sample), 'little') + for k in range(dimension)] + minus = [int.from_bytes(bytes(4 - v[k] for v in sample), 'little') + for k in range(dimension)] + rows = [] + for i in indices: + u = sample[i] + offset = 4 * sum(abs(x) for x in u) + packed = sum(x * plus[k] if x > 0 else -x * minus[k] + for k, x in enumerate(u) if x) + values = packed.to_bytes(len(sample), 'little') + rows.append(sum(1 << j for j, value in enumerate(values) + if i == j or value == shift + offset)) + return rows + + def leech_minor(global_indices, independent_rows, shift=0, signed=False): + """Reject one stated Leech central minor by exact binary rank. + + Row construction uses exact base-256 byte lanes (equivalent to the + historical pairwise sparse-dot genexpr). Golay inventory, norms, rational + span witnesses, elimination and admission checks are unchanged. + """ require(shift in (-16,-8,0,8,16),'Unsupported affine offset') require(signed or shift==0,'Shifted cases here use the full signed family') lines=leech_lines();size=len(lines);n=size*(2 if signed else 1);d=24+int(shift!=0) @@ -74,12 +115,9 @@ def leech_minor(global_indices, independent_rows, shift=0, signed=False): base=[tuple(v)+(1,) for v in [lines[i] for i in [0]+list(range(1,46,2))]] base.append(tuple(-x for x in lines[0])+(1,)) require(rank(matrix(base))==25,'Affine rational rank failed') - packed=[];digest=sha256() - for i in independent_rows: - sparse=[(a,x) for a,x in enumerate(sample[i]) if x] - row=sum(1<