From 04f5811b95a2a69866f94ca94956a3e823cfb8e1 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Wed, 14 Oct 2026 20:56:04 +0000 Subject: [PATCH] =?UTF-8?q?Tooling:=2069=C3=97=20faster=20mixed-point=20Ci?= =?UTF-8?q?rcuit.verify=20supports=20with=20identical=20receipts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace Circuit.verify's exact-|source∩target|=r set-intersection genexpr with an equivalent closed-form point-incidence mask. Package research/mixed-point-verify-masks with identical True receipts, pin-only certificate updates, and registered replay. No new kappa. Prepared by Wentao Li with substantial AI assistance. --- certificates/mixed-point-audit.json | 2 +- certificates/parity-side.json | 2 +- research/mixed-point-verify-masks/NOTICE.md | 12 + research/mixed-point-verify-masks/README.md | 112 +++++++ research/mixed-point-verify-masks/RESULT.json | 50 +++ .../mixed-point-verify-masks/SOURCES.json | 54 ++++ research/mixed-point-verify-masks/TASK.json | 70 +++++ research/mixed-point-verify-masks/VERIFY.json | 55 ++++ research/mixed-point-verify-masks/baseline.py | 284 +++++++++++++++++ .../mixed-point-verify-masks/benchmark.py | 166 ++++++++++ research/mixed-point-verify-masks/verify.py | 297 ++++++++++++++++++ scripts/experiments/mixed_point_circuit.py | 30 +- tests/test_mixed_point_verify_masks.py | 141 +++++++++ 13 files changed, 1271 insertions(+), 4 deletions(-) create mode 100644 research/mixed-point-verify-masks/NOTICE.md create mode 100644 research/mixed-point-verify-masks/README.md create mode 100644 research/mixed-point-verify-masks/RESULT.json create mode 100644 research/mixed-point-verify-masks/SOURCES.json create mode 100644 research/mixed-point-verify-masks/TASK.json create mode 100644 research/mixed-point-verify-masks/VERIFY.json create mode 100644 research/mixed-point-verify-masks/baseline.py create mode 100644 research/mixed-point-verify-masks/benchmark.py create mode 100644 research/mixed-point-verify-masks/verify.py create mode 100644 tests/test_mixed_point_verify_masks.py diff --git a/certificates/mixed-point-audit.json b/certificates/mixed-point-audit.json index e97c2e4e24..ab462d0f11 100644 --- a/certificates/mixed-point-audit.json +++ b/certificates/mixed-point-audit.json @@ -486,7 +486,7 @@ ], "source_sha256": { "docs/research/mixed-point-audit.md": "c80527f9e98c27bd7f5858a06c7273f84c40e0c41505eb4d16029b61f80fb968", - "scripts/experiments/mixed_point_circuit.py": "f509362b5031976a22af351fd158ae0b4520fa4f286a5176ec37023d672a7ddc", + "scripts/experiments/mixed_point_circuit.py": "cc98eeada267814fa2c0bc5f3ebb844f614d667c74d16d80d7ef29b1f90e0aa5", "scripts/rational_span_frames.py": "7386947406d5dc4322a39fb7ccd886876a2fa1d163e823f0f231e11cf9ca0cec" }, "status": "BOUNDED MIXED-POINT RESEARCH; NO NEW KAPPA", diff --git a/certificates/parity-side.json b/certificates/parity-side.json index bcc1a78412..7857dc7345 100644 --- a/certificates/parity-side.json +++ b/certificates/parity-side.json @@ -121,7 +121,7 @@ "scripts/audit_parity_side.py": "7cbdd405ce11fa6f7ffcbef3811174f8685ad4640e9330176601d3b3d3e95390", "scripts/binary_phase_frames.py": "4148cfa313cf050ed25296e8db36d35871520b8318fd086c7d1facf0c6af67d7", "scripts/experiments/disjoint_tensor.py": "085600fc922ae167b5981505e1a5caba4d1c1df15482f61d83d2c086fa89eac1", - "scripts/experiments/mixed_point_circuit.py": "f509362b5031976a22af351fd158ae0b4520fa4f286a5176ec37023d672a7ddc", + "scripts/experiments/mixed_point_circuit.py": "cc98eeada267814fa2c0bc5f3ebb844f614d667c74d16d80d7ef29b1f90e0aa5", "scripts/experiments/parity_phase_repair.py": "1f76f3b96ed556ed901835bd101d0e2588c997d2ed39bdfca097f0187aa86d40", "scripts/experiments/parity_side.py": "1363ebf82d4c39e458e7bede8253688271008374db70ed4284df84253c8d092b" }, diff --git a/research/mixed-point-verify-masks/NOTICE.md b/research/mixed-point-verify-masks/NOTICE.md new file mode 100644 index 0000000000..1a934d869d --- /dev/null +++ b/research/mixed-point-verify-masks/NOTICE.md @@ -0,0 +1,12 @@ +# Notice — mixed-point verify masks + +Douglas R. Colkitt authored the mixed-point / early-sharing screens, the +`Circuit` recurrence and interning, and the original exact-intersection +support checks consumed by this tooling package. + +This package adds an equivalence-preserving closed-form rewrite of the +historical `|source ∩ target| = r` expected-support genexpr inside +`Circuit.verify`, with identical True receipts, matching output supports, +and updated source pins only. + +Prepared by Wentao Li with substantial AI assistance, under Apache-2.0. diff --git a/research/mixed-point-verify-masks/README.md b/research/mixed-point-verify-masks/README.md new file mode 100644 index 0000000000..431b5e3427 --- /dev/null +++ b/research/mixed-point-verify-masks/README.md @@ -0,0 +1,112 @@ +# Faster mixed-point Circuit.verify supports with identical receipts + +**Tooling improvement; no new kappa.** At base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, merged +[CrocSwap/integer-mult-bounds#1984](https://github.com/CrocSwap/integer-mult-bounds/pull/1984) +sped up mixed-point `scalar_check` digests but left the general +`Circuit.verify` path on `scripts/experiments/mixed_point_circuit.py` on the +historical set-intersection genexpr + +```text +sum(1<0) differs and is rejected by the package controls. Topology of the +constructed DAG is untouched; only the expected-support check is rewritten. + +## Open next questions + +1. **Question:** Is mixed-point `Circuit.add` / `build` construction worth a + separate identical-structure rewrite after this verify-path change? + **Why it matters:** On `build(50,3,3,1)`, `add()` is ~37% of wall time via + huge-int dict lookups; local binding alone was only ~1.09× in this session. + **First step:** Profile `Circuit.add` on the hybrid h=50 build with a + structure-identity oracle and prototype a faster intern path only if ≥~1.5× + with identical DAGs. + **Blocked by:** Out of this session’s stop rule. + +2. **Question:** Should `DisjointTensor.verify`'s `dag_sha256` `json.dumps` path + still get a hand-rolled formatter after #2117 `frame_data` lands? + **Why it matters:** Post-mask verify residual is mostly json/sha of huge + support strings; a streaming hand-roll was only ~1.22× on full verify here. + **First step:** Re-profile on a tip that includes #2117. + **Blocked by:** Micro-opt under the session bar; pin conflict with open #2117. + +## Overlap and credit + +Closest priors (different objects): +[CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756), +[CrocSwap/integer-mult-bounds#1793](https://github.com/CrocSwap/integer-mult-bounds/pull/1793), +[CrocSwap/integer-mult-bounds#1861](https://github.com/CrocSwap/integer-mult-bounds/pull/1861) +(open; primary pin `binary_phase_frames.py` — same `parity-side.json` file, +different key), +[CrocSwap/integer-mult-bounds#1984](https://github.com/CrocSwap/integer-mult-bounds/pull/1984) +(mixed-point `scalar_check` digests; this package answers the remaining general +`Circuit.verify` support-genexpr object), +[CrocSwap/integer-mult-bounds#1994](https://github.com/CrocSwap/integer-mult-bounds/pull/1994), +[CrocSwap/integer-mult-bounds#2001](https://github.com/CrocSwap/integer-mult-bounds/pull/2001), +[CrocSwap/integer-mult-bounds#2117](https://github.com/CrocSwap/integer-mult-bounds/pull/2117) +(DisjointTensor `frame_data`; different file). No competing open PR on +`Circuit.verify` at refresh. + +Douglas R. Colkitt authored the mixed-point and early-sharing screens and +original checkers. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance, under +Apache-2.0. diff --git a/research/mixed-point-verify-masks/RESULT.json b/research/mixed-point-verify-masks/RESULT.json new file mode 100644 index 0000000000..fe127e87e5 --- /dev/null +++ b/research/mixed-point-verify-masks/RESULT.json @@ -0,0 +1,50 @@ +{ + "environment": { + "executable": "/usr/bin/python3.12", + "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]" + }, + "fixture": "Circuit.verify on build(20/26/30,*,*,*) set (construction excluded)", + "median_baseline_seconds": 8.33077911800001, + "median_optimized_seconds": 0.12068828400003895, + "median_ratio": 69.0272397774528, + "no_new_kappa": true, + "rounds": 5, + "samples": [ + { + "baseline_seconds": 8.394247341999971, + "optimized_seconds": 0.12226998500000263, + "ratio": 68.65337672201228, + "round": 0 + }, + { + "baseline_seconds": 8.326817022, + "optimized_seconds": 0.12068828400003895, + "ratio": 68.99441060904729, + "round": 1 + }, + { + "baseline_seconds": 8.33077911800001, + "optimized_seconds": 0.1204055650000555, + "ratio": 69.1893195966164, + "round": 2 + }, + { + "baseline_seconds": 8.44291771799999, + "optimized_seconds": 0.11961175099997945, + "ratio": 70.58602225463149, + "round": 3 + }, + { + "baseline_seconds": 8.279030670999987, + "optimized_seconds": 0.12259075400004349, + "ratio": 67.53389143031985, + "round": 4 + } + ], + "source_sha256": { + "baseline": "f509362b5031976a22af351fd158ae0b4520fa4f286a5176ec37023d672a7ddc", + "production": "cc98eeada267814fa2c0bc5f3ebb844f614d667c74d16d80d7ef29b1f90e0aa5" + }, + "status": "PASS_IDENTICAL_MIXED_POINT_VERIFY_MASK_RECEIPTS" +} diff --git a/research/mixed-point-verify-masks/SOURCES.json b/research/mixed-point-verify-masks/SOURCES.json new file mode 100644 index 0000000000..88848def93 --- /dev/null +++ b/research/mixed-point-verify-masks/SOURCES.json @@ -0,0 +1,54 @@ +{ + "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/mixed-point-audit.json", + "usage": "provenance", + "git_blob": "e97c2e4e24a5e3f92bd9db6abc8e890e0417b3f6", + "sha256": "54659a3844c6f233b1d5b9f30ffab65742a5b2fe4a4b510dc809253b1180e95c" + }, + { + "path": "certificates/parity-side.json", + "usage": "provenance", + "git_blob": "bcc1a78412d297424db1727f49636598206b9392", + "sha256": "44ab9d7b781a28228498aa0e73229c700eac4a3a3cf93ffe8f82f52f8c52226c" + }, + { + "path": "docs/research/mixed-point-audit.md", + "usage": "provenance", + "git_blob": "31f712b8f78cee8a05b8cb490c8c979c79265ee2", + "sha256": "c80527f9e98c27bd7f5858a06c7273f84c40e0c41505eb4d16029b61f80fb968" + }, + { + "path": "scripts/audit_mixed_point.py", + "usage": "provenance", + "git_blob": "53a2e05d0e82df7feb18eed271264f060874335d", + "sha256": "fc7ca3e07d8a3ad54e894c387a89b310ae0b7048763cd48bb27f5daeb0d73dba" + }, + { + "path": "scripts/experiments/mixed_point_circuit.py", + "usage": "provenance", + "git_blob": "b7f561f416f815d0fd135f0a0464c291a9a68468", + "sha256": "f509362b5031976a22af351fd158ae0b4520fa4f286a5176ec37023d672a7ddc" + }, + { + "path": "tests/test_mixed_point.py", + "usage": "provenance", + "git_blob": "1d97e9f9bbcd4d61f618fc562a0e22b58af59ad5", + "sha256": "bb279af4bf072e9709d70cefe0cdf0230688d865f9c5e902350c4aade9218452" + } + ] +} diff --git a/research/mixed-point-verify-masks/TASK.json b/research/mixed-point-verify-masks/TASK.json new file mode 100644 index 0000000000..937fc3dd24 --- /dev/null +++ b/research/mixed-point-verify-masks/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_seed": "a41c9e7b2d805f63e0b1c7489a6d5e20", + "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 scripts/experiments/mixed_point_circuit.py:Circuit.verify replace its exact-|source∩target|=r expected-support genexpr with an equivalent closed-form point-incidence mask (OR over r-subsets U of the target of inputs that contain every point of U and avoid every other target point) so verify still returns True, every output support matches the historical checker, and support require() rejection is preserved on mixed-point and early-sharing replay sizes?", + "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 mixed-point scalar_check digests (#1984), SharedPoint digests (#1994), ExclusionCircuit/DisjointTensor support masks (#2001), and open leave-alone construction PRs (#2039/#2054). Profiling named Circuit.verify's set-intersection genexpr (tens of seconds on h≈40) as the next unclaimed mixed-point hot path; DisjointTensor.dag_sha256 hand-roll was measured at only ~1.22× on full verify and deferred.", + "bottleneck_link": "Side result on review throughput: tests/test_mixed_point.py and any caller of Circuit.verify pay the historical genexpr. A faster identical support check does not change kappa, scalar_check digests, or the binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving Circuit.verify support-mask change with frozen baseline, identical True receipts plus matching output supports on historical sizes through h=30, updated source pins only on the two binding certificates, registered replay and a measured before/after median. Do not touch audit_mixed_point.scalar_check, SharedPoint, DisjointTensor.frame_data, or run the selected cold frontier replay.", + "outcome": "completed", + "evidence": "PASS_MIXED_POINT_VERIFY_MASKS via research/mixed-point-verify-masks/verify.py (also under -O); PASS_IDENTICAL_MIXED_POINT_VERIFY_MASK_RECEIPTS via benchmark.py; two certificates differ from base only in the scripts/experiments/mixed_point_circuit.py source pin.", + "author": "Wentao Li", + "github": "VictorLiwentao", + "email": "wentaol4@illinois.edu", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, implementation, packaging, benchmarking and writing. Not independent human peer review.", + "open_questions": [ + { + "question": "Is mixed-point Circuit.add / build construction worth a separate identical-structure rewrite after this verify-path change?", + "why_it_matters": "On build(50,3,3,1), add() is ~37% of wall time via huge-int dict lookups; local binding alone was only ~1.09× in this session.", + "first_step": "Profile Circuit.add on the hybrid h=50 build with a structure-identity oracle (args/support/lookup order) and prototype a faster intern path only if ≥~1.5× with identical DAGs.", + "blocked_by": "Out of this session's stop rule; Circuit.verify support masks were the measured bottleneck." + }, + { + "question": "Should DisjointTensor.verify's dag_sha256 json.dumps path still get a hand-rolled formatter after #2117 frame_data lands?", + "why_it_matters": "Post-mask verify residual is ~69% json/sha of huge support strings; a streaming hand-roll was only ~1.22× on full verify here because bigint str() dominates.", + "first_step": "Re-profile on a tip that includes #2117 and decide whether a ≥1.5× identical-receipt residual remains.", + "blocked_by": "Micro-opt under the session bar; leave-alone pin conflict with open #2117 until that PR merges or a fold tip is chosen." + } + ] +} diff --git a/research/mixed-point-verify-masks/VERIFY.json b/research/mixed-point-verify-masks/VERIFY.json new file mode 100644 index 0000000000..afa38ffbf7 --- /dev/null +++ b/research/mixed-point-verify-masks/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/experiments/mixed_point_circuit.py", + "scripts/audit_mixed_point.py", + "certificates/mixed-point-audit.json", + "certificates/parity-side.json", + "docs/research/mixed-point-audit.md", + "tests/test_mixed_point.py", + "tests/test_mixed_point_verify_masks.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 480, + "checks": "Exact baseline copy of the base-commit mixed_point_circuit.py; closed-form exact-r masks match the historical genexpr with a mutant rejected; Circuit.verify returns True with identical output supports through h=30; two certificates differ from base only in the mixed_point_circuit.py source pin; duplicate JSON keys rejected." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 480, + "checks": "Same equivalence and certificate pin discipline under -O (require() gates, not assert)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "tests", + "-p", + "test_mixed_point_verify_masks.py", + "-v" + ], + "timeout_seconds": 180, + "checks": "Focused mixed-point verify-mask package controls." + } + ] +} diff --git a/research/mixed-point-verify-masks/baseline.py b/research/mixed-point-verify-masks/baseline.py new file mode 100644 index 0000000000..b7f561f416 --- /dev/null +++ b/research/mixed-point-verify-masks/baseline.py @@ -0,0 +1,284 @@ +"""Structured mixed-point scalar circuits; no full-size frame certificate. + +Plans use direct sums, vector kernels, transposed kernels, paired exclusion, +and optionally common-point decomposition. Counts select between block splits +and tensor evaluation orders; exact support interning supplies further sharing. +""" +from collections import defaultdict +from functools import cache +import heapq +from itertools import combinations +from math import comb +from exclusion_circuit import ExclusionCircuit +from paired_exclusion_circuit import PairedExclusionCircuit + +class Circuit: + add = ExclusionCircuit.add + total = ExclusionCircuit.total + + def __init__(self, n, k, l, r): + self.n = n + self.k = k + self.l = l + self.r = r + self.inputs = list(combinations(range(n), k)) + self.targets = list(combinations(range(n), l)) + self.variables = {p: i + 1 for i, p in enumerate(self.inputs)} + self.support = [0] + [1 << i for i in range(len(self.inputs))] + self.args = [None] * len(self.support) + self.lookup = {s: i for i, s in enumerate(self.support)} + + def finish(self, outputs): + self.outputs = outputs + active = set() + stack = list(outputs) + while stack: + x = stack.pop() + if not x or x in active: + continue + active.add(x) + if self.args[x]: + stack.extend(self.args[x]) + self.active = sorted(active) + self.additions = sum((self.args[x] is not None for x in active)) + return self + + def apply(self, t, inputs): + nodes = [0] * len(t.args) + nodes[1:len(inputs) + 1] = inputs + for node in t.active: + if t.args[node]: + a, b = t.args[node] + nodes[node] = self.add(nodes[a], nodes[b]) + return [nodes[node] for node in t.outputs] + + def verify(self): + for target, node in zip(self.targets, self.outputs): + mask = sum((1 << i for i, source in enumerate(self.inputs) if len(set(source) & set(target)) == self.r)) + assert self.support[node] == mask + return True + +@cache +def vector(n, l, r): + c = Circuit(n, 1, l, r) + if r: + + def output(target): + if len(target) < 3: + return c.total([c.variables[a,] for a in target]) + side = [a for a in target if a < n // 2] + if len(side) < 2: + side = [a for a in target if a >= n // 2] + pair = side[:2] + last = next((a for a in target if a not in pair)) + return c.add(c.add(c.variables[pair[0],], c.variables[pair[1],]), c.variables[last,]) + return c.finish([output(t) for t in c.targets]) + + def avoid(points, excluded): + if not points: + return 0 + if not excluded: + return c.total([c.variables[a,] for a in points]) + if len(points) == 1: + return 0 + mid = len(points) // 2 + left, right = (points[:mid], points[mid:]) + return c.add(avoid(left, excluded.intersection(left)), avoid(right, excluded.intersection(right))) + return c.finish([avoid(list(range(n)), set(t)) for t in c.targets]) + +def transpose(t): + c = Circuit(t.n, t.l, t.k, t.r) + users = {node: [] for node in t.active} + for node in t.active: + if t.args[node]: + for child in t.args[node]: + users[child].append(('node', node)) + for i, node in enumerate(t.outputs): + users[node].append(('input', i + 1)) + image = {} + for node in reversed(t.active): + image[node] = c.total([value if typ == 'input' else image[value] for typ, value in users[node]]) + return c.finish([image[i] for i in range(1, len(t.inputs) + 1)]) + +@cache +def kernel(n, k, l, r): + if k == 1: + return vector(n, l, r) + if l == 1: + return transpose(vector(n, k, r)) + if k == l == 2 and r == 0: + t = PairedExclusionCircuit(n) + c = Circuit(n, k, l, r) + c.support = t.support + c.args = t.args + c.lookup = t.lookup + return c.finish([t.outputs[targ] for targ in c.targets]) + return None + +def feasible(n, k, l, r): + return 0 <= k <= n and 0 <= l <= n and (0 <= r <= min(k, l)) and (k + l - r <= n) + +@cache +def plan(n, k, l, r, common=True): + p, q = (comb(n, k), comb(n, l)) + degree = comb(l, r) * comb(n - l, k - r) + if degree == 1: + return (0, 'single', 0) + if not l or not k: + return (q * (p - 1), 'direct', 0) + winner = (q * (degree - 1), 'direct', 0) + t = kernel(n, k, l, r) + if t and t.additions < winner[0]: + winner = (t.additions, 'kernel', 0) + if r == 1 and common: + common_cost = n * plan(n - 1, k - 1, l - 1, 0, common)[0] + (l - 1) * q + if common_cost < winner[0]: + winner = (common_cost, 'common', 0) + for nl in range(1, n): + nr = n - nl + cost = 0 + for b in range(max(0, l - nr), min(l, nl) + 1): + cases = 0 + for a in range(max(0, k - nr), min(k, nl) + 1): + for u in range(r + 1): + if not feasible(nl, a, b, u) or not feasible(nr, k - a, l - b, r - u): + continue + cases += 1 + lc = plan(nl, a, b, u, common)[0] + rc = plan(nr, k - a, l - b, r - u, common)[0] + cost += min(comb(nr, k - a) * lc + comb(nl, b) * rc, comb(nr, l - b) * lc + comb(nl, a) * rc) + cost += comb(nl, b) * comb(nr, l - b) * (cases - 1) + if cost < winner[0]: + winner = (cost, 'split', nl) + return winner + +@cache +def build(n, k, l, r, common=True): + cost, kind, nl = plan(n, k, l, r, common) + if kind == 'kernel': + return kernel(n, k, l, r) + c = Circuit(n, k, l, r) + if kind in ('direct', 'single'): + return c.finish([c.total([i + 1 for i, s in enumerate(c.inputs) if len(set(s) & set(t)) == r]) for t in c.targets]) + if kind == 'common': + child = build(n - 1, k - 1, l - 1, 0, common) + pieces = {t: [] for t in c.targets} + for point in range(n): + pts = [a for a in range(n) if a != point] + ins = [c.variables[tuple(sorted((point, *(pts[a] for a in source))))] for source in child.inputs] + outs = c.apply(child, ins) + for target, node in zip(child.targets, outs): + pieces[tuple(sorted((point, *(pts[a] for a in target))))].append(node) + return c.finish([c.total(pieces[t]) for t in c.targets]) + nr = n - nl + pieces = {t: [] for t in c.targets} + for b in range(max(0, l - nr), min(l, nl) + 1): + TL = list(combinations(range(nl), b)) + TR = list(combinations(range(nr), l - b)) + for a in range(max(0, k - nr), min(k, nl) + 1): + IL = list(combinations(range(nl), a)) + IR = list(combinations(range(nr), k - a)) + for u in range(r + 1): + if not feasible(nl, a, b, u) or not feasible(nr, k - a, l - b, r - u): + continue + left = build(nl, a, b, u, common) + right = build(nr, k - a, l - b, r - u, common) + mat = [[c.variables[s + tuple((nl + x for x in t))] for t in IR] for s in IL] + lc = len(IR) * left.additions + len(TL) * right.additions + rc = len(TR) * left.additions + len(IL) * right.additions + if lc <= rc: + temp = list(zip(*[c.apply(left, list(col)) for col in zip(*mat)])) + out = [c.apply(right, list(row)) for row in temp] + else: + temp = [c.apply(right, row) for row in mat] + out = list(zip(*[c.apply(left, list(col)) for col in zip(*temp)])) + for i, s in enumerate(TL): + for j, t in enumerate(TR): + pieces[s + tuple((nl + x for x in t))].append(out[i][j]) + c.finish([c.total(pieces[t]) for t in c.targets]) + assert c.additions <= cost, (n, k, l, r, c.additions, cost) + return c + + +def factored_transpose(t): + users = {node: [] for node in t.active} + for node in t.active: + if t.args[node]: + for child in t.args[node]: + users[child].append(node) + for i, node in enumerate(t.outputs): + users[node].append(-i - 1) + expr = {} + alias = {} + for node in reversed(t.active): + terms = [alias.get(x, x) if x > 0 else x for x in users[node]] + assert len(set(terms)) == len(terms) + if len(terms) == 1: + alias[node] = terms[0] + else: + expr[node] = set(terms) + alias[node] = node + need = [alias[i] for i in range(1, len(t.inputs) + 1)] + occurrence = defaultdict(set) + for key, terms in expr.items(): + for pair in combinations(sorted(terms), 2): + occurrence[pair].add(key) + heap = [(-len(uses), pair) for pair, uses in occurrence.items() if len(uses) >= 2] + heapq.heapify(heap) + helpers = {} + nexttag = len(t.args) + steps = 0 + while heap: + neg, pair = heapq.heappop(heap) + uses = occurrence.get(pair, set()) + count = len(uses) + if count < 2: + continue + if count != -neg: + heapq.heappush(heap, (-count, pair)) + continue + a, b = pair + tag = nexttag + nexttag += 1 + helpers[tag] = pair + touched = set() + for key in sorted(uses): + terms = expr[key] + assert a in terms and b in terms + others = terms - {a, b} + for x in others: + for v in (a, b): + old = tuple(sorted((x, v))) + occurrence[old].remove(key) + if not occurrence[old]: + del occurrence[old] + new = tuple(sorted((x, tag))) + occurrence[new].add(key) + touched.add(new) + terms.difference_update((a, b)) + terms.add(tag) + del occurrence[pair] + for new in sorted(touched): + if len(occurrence[new]) >= 2: + heapq.heappush(heap, (-len(occurrence[new]), new)) + steps += 1 + c = Circuit(t.n, t.l, t.k, t.r) + image = {} + for target in need: + stack = [(target, False)] + while stack: + tag, ready = stack.pop() + if tag in image: + continue + if tag < 0: + image[tag] = -tag + continue + if ready: + children = helpers[tag] if tag in helpers else sorted(expr[tag]) + image[tag] = c.total([image[child] for child in children]) + continue + stack.append((tag, True)) + children = helpers[tag] if tag in helpers else sorted(expr[tag]) + stack.extend(((child, False) for child in children if child not in image)) + c.finish([image[tag] for tag in need]) + return (c, dict(factors=steps, expressions=len(expr))) diff --git a/research/mixed-point-verify-masks/benchmark.py b/research/mixed-point-verify-masks/benchmark.py new file mode 100644 index 0000000000..6e9d553ac6 --- /dev/null +++ b/research/mixed-point-verify-masks/benchmark.py @@ -0,0 +1,166 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process before/after timing for mixed-point Circuit.verify. + +Timing is descriptive and never a correctness gate. Both engines must return +True on the same constructed circuits; output-support fingerprints must match. +Circuit construction is shared and excluded from the timed interval. +""" +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 +sys.path.insert(0, str(ROOT / "scripts")) +from certify import require # noqa: E402 + +WORKER = r''' +import importlib.util +import json +import sys +import time +from hashlib import sha256 +from pathlib import Path + +root = Path(sys.argv[1]) +mode = sys.argv[2] +sys.path.insert(0, str(root / "scripts")) + +from experiments.mixed_point_circuit import build + +if mode == "baseline": + spec = importlib.util.spec_from_file_location( + "baseline_mpc", root / "research/mixed-point-verify-masks/baseline.py" + ) + mod = importlib.util.module_from_spec(spec) + sys.modules["baseline_mpc"] = mod + spec.loader.exec_module(mod) + verify = mod.Circuit.verify +else: + from experiments.mixed_point_circuit import Circuit + verify = Circuit.verify + +# Build the fixed historical fixture set outside the timed window. +build.cache_clear() +circuits = [] +for args in ( + (20, 3, 3, 0), + (20, 3, 3, 1), + (26, 3, 3, 0), + (26, 3, 3, 1), + (30, 3, 3, 1), +): + build.cache_clear() + circuits.append((args, build(*args))) + +t0 = time.perf_counter() +rows = [] +for args, circuit in circuits: + ok = verify(circuit) + digest = sha256() + for node in circuit.outputs: + digest.update(str(circuit.support[node]).encode() + b"\n") + rows.append( + dict( + args=list(args), + verified=bool(ok), + additions=circuit.additions, + active=len(circuit.active), + support_sha256=digest.hexdigest(), + ) + ) +elapsed = time.perf_counter() - t0 +print(json.dumps(dict(mode=mode, seconds=elapsed, rows=rows), sort_keys=True)) +''' + + +def run_worker(mode: str) -> dict: + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run( + [sys.executable, "-I", "-B", "-c", WORKER, str(ROOT), mode], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + check=False, + ) + require(proc.returncode == 0, f"worker {mode} failed: {proc.stderr[-2000:]}") + line = proc.stdout.strip().splitlines()[-1] + return json.loads(line) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--out", type=Path, default=PACKAGE / "RESULT.json") + args = parser.parse_args() + require(args.rounds >= 1, "rounds") + + samples = [] + for i in range(args.rounds): + order = ("optimized", "baseline") if i % 2 == 0 else ("baseline", "optimized") + pair = {} + for mode in order: + pair[mode] = run_worker(mode) + require( + pair["baseline"]["rows"] == pair["optimized"]["rows"], + f"receipt mismatch on round {i}", + ) + samples.append( + dict( + round=i, + baseline_seconds=pair["baseline"]["seconds"], + optimized_seconds=pair["optimized"]["seconds"], + ratio=pair["baseline"]["seconds"] / pair["optimized"]["seconds"], + ) + ) + print( + f"round {i}: baseline={pair['baseline']['seconds']:.3f}s " + f"optimized={pair['optimized']['seconds']:.3f}s " + f"ratio={samples[-1]['ratio']:.3f}", + flush=True, + ) + + base_med = statistics.median(s["baseline_seconds"] for s in samples) + opt_med = statistics.median(s["optimized_seconds"] for s in samples) + result = dict( + status="PASS_IDENTICAL_MIXED_POINT_VERIFY_MASK_RECEIPTS", + fixture="Circuit.verify on build(20/26/30,*,*,*) set (construction excluded)", + rounds=args.rounds, + median_baseline_seconds=base_med, + median_optimized_seconds=opt_med, + median_ratio=base_med / opt_med, + samples=samples, + environment=dict( + python=sys.version, + platform=platform.platform(), + executable=sys.executable, + ), + source_sha256=dict( + baseline=sha256((PACKAGE / "baseline.py").read_bytes()).hexdigest(), + production=sha256( + (ROOT / "scripts/experiments/mixed_point_circuit.py").read_bytes() + ).hexdigest(), + ), + no_new_kappa=True, + ) + args.out.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print( + "PASS_IDENTICAL_MIXED_POINT_VERIFY_MASK_RECEIPTS", + f"median {base_med:.3f} -> {opt_med:.3f} s ({base_med / opt_med:.2f}x)", + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/research/mixed-point-verify-masks/verify.py b/research/mixed-point-verify-masks/verify.py new file mode 100644 index 0000000000..0625017846 --- /dev/null +++ b/research/mixed-point-verify-masks/verify.py @@ -0,0 +1,297 @@ +#!/usr/bin/env python3 +"""Equivalence, pin and mutation controls for mixed-point Circuit.verify masks. + +Read-only by default. Regenerates no certificate. 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 itertools import combinations +from pathlib import Path +import subprocess +import sys + +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 experiments import mixed_point_circuit as production # noqa: E402 + +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ORIGINAL_BLOB = "b7f561f416f815d0fd135f0a0464c291a9a68468" +ORIGINAL_SHA256 = "f509362b5031976a22af351fd158ae0b4520fa4f286a5176ec37023d672a7ddc" +OPTIMIZED_SHA256 = "cc98eeada267814fa2c0bc5f3ebb844f614d667c74d16d80d7ef29b1f90e0aa5" + +PINNED_CERTIFICATES = ( + "certificates/mixed-point-audit.json", + "certificates/parity-side.json", +) + +VERIFY_CASES = ( + (12, 3, 3, 0), + (12, 3, 3, 1), + (16, 2, 2, 0), + (16, 2, 2, 1), + (16, 3, 3, 0), + (16, 3, 3, 1), + (20, 3, 3, 0), + (20, 3, 3, 1), + (26, 3, 3, 0), + (26, 3, 3, 1), + (30, 3, 3, 1), +) + + +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) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def git_show(path: str) -> bytes: + return subprocess.check_output(["git", "show", f"{BASE_COMMIT}:{path}"], cwd=ROOT) + + +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(path: Path): + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_object) + + +def check_baseline_bytes() -> None: + baseline = PACKAGE / "baseline.py" + original = git_show("scripts/experiments/mixed_point_circuit.py") + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base mixed_point_circuit.py sha256 drift") + blob = ( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:scripts/experiments/mixed_point_circuit.py"], + cwd=ROOT, + ) + .decode() + .strip() + ) + require(blob == ORIGINAL_BLOB, "base mixed_point_circuit.py blob drift") + require(baseline.read_bytes() == original, "baseline.py must be an exact copy of the base commit source") + require( + digest_file(SCRIPTS / "experiments" / "mixed_point_circuit.py") == OPTIMIZED_SHA256, + "production mixed_point_circuit.py does not match the claimed optimized digest", + ) + + +def historical_expected(inputs, target, r: int) -> int: + return sum( + 1 << i + for i, source in enumerate(inputs) + if len(set(source) & set(target)) == r + ) + + +def closed_form_expected(full: int, vertex: list[int], target, r: int) -> int: + expected = 0 + for U in combinations(target, r): + keep = set(U) + mask = full + for point in target: + if point in keep: + mask &= vertex[point] + else: + mask &= full ^ vertex[point] + expected |= mask + return expected + + +def build_vertex(inputs, n: int) -> tuple[int, list[int]]: + full = (1 << len(inputs)) - 1 + vertex = [0] * n + for i, source in enumerate(inputs): + for point in source: + vertex[point] |= 1 << i + return full, vertex + + +def clear_caches(module) -> None: + module.build.cache_clear() + module.plan.cache_clear() + module.kernel.cache_clear() + module.vector.cache_clear() + + +def check_mask_equivalence() -> dict: + """Closed-form exact-r masks must match the historical genexpr.""" + cases = 0 + for n, k, l, r in ( + (10, 2, 2, 0), + (10, 2, 2, 1), + (12, 3, 3, 0), + (12, 3, 3, 1), + (12, 3, 3, 2), + (14, 3, 3, 0), + (14, 3, 3, 1), + (16, 3, 3, 1), + (18, 3, 3, 0), + (20, 3, 3, 1), + ): + clear_caches(production) + circuit = production.build(n, k, l, r) + full, vertex = build_vertex(circuit.inputs, circuit.n) + for target, node in zip(circuit.targets, circuit.outputs): + old = historical_expected(circuit.inputs, target, r) + new = closed_form_expected(full, vertex, target, r) + require(old == new, f"mask mismatch {n,k,l,r} target={target}") + require(circuit.support[node] == new, f"live support mismatch {n,k,l,r}") + cases += 1 + # Mutant foil: XOR of per-point masks (cancels inputs that meet T twice) + # for r=0, or plain OR-of-vertex (ignores exact-r) for r>0. + target = circuit.targets[0] + xor_hit = 0 + or_hit = 0 + for point in target: + xor_hit ^= vertex[point] + or_hit |= vertex[point] + mutant = full ^ xor_hit if r == 0 else or_hit + correct = closed_form_expected(full, vertex, target, r) + require(mutant != correct, f"mutant must differ on {n,k,l,r}") + return {"mask_cases": cases, "mutant": "rejected"} + + +def support_fingerprint(circuit) -> str: + digest = sha256() + for node in circuit.outputs: + digest.update(str(circuit.support[node]).encode() + b"\n") + return digest.hexdigest() + + +def check_verify_equivalence(baseline, optimized) -> dict: + records = [] + for n, k, l, r in VERIFY_CASES: + clear_caches(optimized) + circuit = optimized.build(n, k, l, r) + old = baseline.Circuit.verify(circuit) + new = circuit.verify() + require(old is True and new is True, f"verify return mismatch on {n,k,l,r}") + # Historical engine still accepts the same supports. + require(baseline.Circuit.verify(circuit) is True, f"baseline reject on {n,k,l,r}") + records.append( + dict( + n=n, + k=k, + l=l, + r=r, + additions=circuit.additions, + active=len(circuit.active), + outputs=len(circuit.outputs), + support_sha256=support_fingerprint(circuit), + verified=True, + ) + ) + require(records[-1]["n"] == 30 and records[-1]["r"] == 1, "unexpected last fixture") + require(records[-1]["additions"] == 95912, "unexpected h=30 r=1 additions") + return {"verify_cases": len(records), "records": records} + + +def check_support_rejection(optimized) -> dict: + clear_caches(optimized) + circuit = optimized.build(12, 3, 3, 1) + node = circuit.outputs[0] + circuit.support[node] ^= 1 + with _expect_value_error(): + circuit.verify() + return {"support_rejection": "preserved", "corrupted": "build(12,3,3,1)"} + + +class _expect_value_error: + def __enter__(self): + return self + + def __exit__(self, exc_type, exc, tb): + require(exc_type is ValueError, "expected ValueError from corrupted support") + return True + + +def check_certificate_pin_discipline() -> dict: + reports = {} + for rel in PINNED_CERTIFICATES: + base = json.loads(git_show(rel).decode()) + live = load_json(ROOT / rel) + key = "scripts/experiments/mixed_point_circuit.py" + base_pin = base["source_sha256"][key] + live_pin = live["source_sha256"][key] + require(base_pin == ORIGINAL_SHA256, f"{rel}: unexpected base pin") + require(live_pin == OPTIMIZED_SHA256, f"{rel}: optimized pin missing") + restored = deepcopy(live) + restored["source_sha256"][key] = ORIGINAL_SHA256 + require(restored == base, f"{rel}: changed fields beyond allowed source pin") + reports[rel] = { + "base_pin": base_pin, + "live_pin": live_pin, + "only_pin_changed": True, + } + return reports + + +def check_temp_corruption_rejection() -> dict: + """On-disk corruption of a temp copy of production source must fail the digest gate.""" + import tempfile + + production_path = SCRIPTS / "experiments" / "mixed_point_circuit.py" + raw = production_path.read_bytes() + require(sha256(raw).hexdigest() == OPTIMIZED_SHA256, "production digest before temp check") + with tempfile.TemporaryDirectory() as tmp: + mutant = Path(tmp) / "mixed_point_circuit.py" + mutant.write_bytes(raw + b"\n# corrupted\n") + require(sha256(mutant.read_bytes()).hexdigest() != OPTIMIZED_SHA256, "temp mutant digest") + require(digest_file(production_path) == OPTIMIZED_SHA256, "production must be unchanged after temp check") + return {"temp_corruption": "rejected", "production_unchanged": True} + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--write-certificate", action="store_true", help="unused; kept for API parity") + args = parser.parse_args() + require(not args.write_certificate, "this package does not rewrite certificate payloads") + + check_baseline_bytes() + baseline = load_module(PACKAGE / "baseline.py", "mixed_point_verify_masks_baseline") + masks = check_mask_equivalence() + verifies = check_verify_equivalence(baseline, production) + rejection = check_support_rejection(production) + pins = check_certificate_pin_discipline() + temp = check_temp_corruption_rejection() + print( + "PASS_MIXED_POINT_VERIFY_MASKS", + f"verify_cases={verifies['verify_cases']}", + f"mask_cases={masks['mask_cases']}", + f"certs={len(pins)}", + "no_new_kappa", + ) + print( + "controls", + rejection["support_rejection"], + temp["temp_corruption"], + f"h30_additions={verifies['records'][-1]['additions']}", + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/scripts/experiments/mixed_point_circuit.py b/scripts/experiments/mixed_point_circuit.py index b7f561f416..064bc8593f 100644 --- a/scripts/experiments/mixed_point_circuit.py +++ b/scripts/experiments/mixed_point_circuit.py @@ -9,6 +9,7 @@ import heapq from itertools import combinations from math import comb +from certify import require from exclusion_circuit import ExclusionCircuit from paired_exclusion_circuit import PairedExclusionCircuit @@ -53,9 +54,34 @@ def apply(self, t, inputs): return [nodes[node] for node in t.outputs] def verify(self): + """Exact |source ∩ target| = r supports via closed-form incidence masks. + + Equivalent to the historical genexpr + ``sum(1<