From c713ff9eff95446508aeb865a9f58b1758b2a00a Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Wed, 14 Oct 2026 14:19:59 -0400 Subject: [PATCH] Add pair-source connector path result: five-source minimum 10, 72-query support bound attained Aaron Wang, with help from opencode. One added operation family (pair-source connector calls B_jk) on research/universal-connector-boundary's five-source model: exact minimum universal source path 10 (construction plus exhaustive nine-point census excluding 9), all-31-nonzero-row batch exactly 72 complete queries (the support bound the fixed alphabet proves unattainable), priced against the predecessor fixture with dirty replay and mutation controls. --- .../CERTIFICATE.json | 41 +++ .../EXPECTED.json | 11 + .../README.md | 137 +++++++++ .../SOURCES.json | 30 ++ .../TASK.json | 76 +++++ .../VERIFY.json | 35 +++ .../verify.py | 261 ++++++++++++++++++ 7 files changed, 591 insertions(+) create mode 100644 research/connector-pair-source-path-seed2cdb/CERTIFICATE.json create mode 100644 research/connector-pair-source-path-seed2cdb/EXPECTED.json create mode 100644 research/connector-pair-source-path-seed2cdb/README.md create mode 100644 research/connector-pair-source-path-seed2cdb/SOURCES.json create mode 100644 research/connector-pair-source-path-seed2cdb/TASK.json create mode 100644 research/connector-pair-source-path-seed2cdb/VERIFY.json create mode 100644 research/connector-pair-source-path-seed2cdb/verify.py diff --git a/research/connector-pair-source-path-seed2cdb/CERTIFICATE.json b/research/connector-pair-source-path-seed2cdb/CERTIFICATE.json new file mode 100644 index 0000000000..1b41b34b51 --- /dev/null +++ b/research/connector-pair-source-path-seed2cdb/CERTIFICATE.json @@ -0,0 +1,41 @@ +{ + "result": "pair-source connector calls B_jk: z += B_j x_j + B_k x_k on the universal-connector-boundary five-source model", + "scope": "one added complete-call family; everything else of research/universal-connector-boundary's Exact interface unchanged", + "minimum_source_path_length": 10, + "prefixes": [0, 2, 3, 5, 13, 15, 30, 26, 10, 8, 0], + "word_steps": [2, 1, 6, 8, 2, 17, 4, 16, 2, 8], + "step_weights": [1, 1, 2, 1, 1, 2, 1, 1, 1, 1], + "step_call_types": ["B_1", "B_0", "B_12", "B_3", "B_1", "B_04", "B_2", "B_4", "B_1", "B_3"], + "multiplicities": [2, 4, 2, 2, 2], + "weight_sum": 12, + "coverage_count": 32, + "queries_all31_matrix": 72, + "lower_bound": { + "readout_queries": 62, + "source_path_length": ">= 10", + "nine_point_census": { + "sets": 7888725, + "covering": 0, + "max_coverage": 29, + "method": "recursive enumeration (search_paths.py) and independent itertools enumeration (verify.py --full) agree" + }, + "counting_step": "C(8,2) = 28 < 31 so |P| >= 9; the census gives |P| >= 10; closure gives |P| <= L" + }, + "predecessor": { + "package": "research/universal-connector-boundary", + "fixed_alphabet_queries": 74, + "fixed_alphabet_support_bound": "72, proven unattainable in the fixed alphabet (README: the support bound of 72 is unattainable; parity rules out 73)", + "fixture_b_leaf_prices": [1, 4, 10, 16, 28], + "predecessor_best_b_leaf_cost_min_relabeling": 120 + }, + "pricing": { + "b_leaf_cost_fixed_labeling": 126, + "b_leaf_cost_min_relabeling": 120, + "b_leaf_cost_max_relabeling": 174, + "leaves_forward_min_relabeling": 182, + "queries": 72, + "dispatch_break_even": "at the optimal labeling this schedule ties the predecessor's leaf cost exactly and saves 2 dispatch records; at the fixed fixture labeling it is +12 leaf charges versus -2 dispatch records, so it is favorable iff one query's dispatch/dispatch-record cost exceeds 6 leaf-price units" + }, + "credit": "Aaron Wang, with help from opencode", + "base_commit": "51122344de9382e784c7f89953456d8cd55513ef" +} diff --git a/research/connector-pair-source-path-seed2cdb/EXPECTED.json b/research/connector-pair-source-path-seed2cdb/EXPECTED.json new file mode 100644 index 0000000000..02f7394e53 --- /dev/null +++ b/research/connector-pair-source-path-seed2cdb/EXPECTED.json @@ -0,0 +1,11 @@ +{ + "fast": { + "command": "python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py", + "expected_stdout_last_line": "PASS_CONNECTOR_PAIR_SOURCE_PATH" + }, + "full_census": { + "command": "python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py --full", + "expected_stdout_last_line": "PASS_CONNECTOR_PAIR_SOURCE_PATH_CENSUS", + "expected_census": {"sets": 7888725, "covering": 0, "max_coverage": 29} + } +} diff --git a/research/connector-pair-source-path-seed2cdb/README.md b/research/connector-pair-source-path-seed2cdb/README.md new file mode 100644 index 0000000000..22aade420a --- /dev/null +++ b/research/connector-pair-source-path-seed2cdb/README.md @@ -0,0 +1,137 @@ +# Pair-source connector calls: five-source universal path of exactly ten, and the 72-query support bound attained + +**Recursive-interface construction plus exact finite exclusion; no new kappa.** +Aaron Wang, with help from opencode. + +Add exactly one operation family to the connector alphabet of +[research/universal-connector-boundary](../universal-connector-boundary/README.md): +the **pair-source connector call** `B_jk: z += B_j x_j + B_k x_k`, one complete +query depositing two sources at once, charged two coefficient/source accesses +and one query record. Everything else of that Exact interface is unchanged: +dirty rows, paired readouts, restoration of `z`, no free copies. + +Result on the five-source, all-31-nonzero-row matrix: + +| Quantity | Fixed alphabet (predecessor) | With pair-source calls | +|---|---:|---:| +| Minimum universal source path | 12 | 10 | +| Complete queries, all-31 matrix | 74 | 72 | +| Support bound `2*(5+31)` | 72, unattainable | 72, attained | +| Source-side leaf cost, best labeling | 120 | 120 | + +The query optimum in the extended alphabet is **exactly 72**: 62 paired +readouts (each nonzero row needs two `A_i` calls) plus a source path of at +least 10, and the word below attains 10. In the fixed alphabet the same +support bound of 72 was proved unattainable by the 945-pairing census, and +parity ruled out 73. + +## The word + +Closed walk on `F_2^5`, one step per source query, step vectors of Hamming +weight 1 (single `B_j`) or 2 (pair `B_jk`): + +```text +prefixes: 0 2 3 5 13 15 30 26 10 8 0 +steps: 2 1 6 8 2 17 4 16 2 8 +calls: B_1 B_0 B_12 B_3 B_1 B_04 B_2 B_4 B_1 B_3 +``` + +The prefix set `P = {0,2,3,5,8,10,13,15,26,30}` has `P XOR P = F_2^5` +(verified two ways in `verify.py`). Place each output's two `A_i` readouts at +the two boundaries whose prefix XOR is its row mask; characteristic two makes +the dirty connector contributions cancel. Source multiplicities are +`(2,4,2,2,2)`, all even, so `z` is restored. + +## Why ten is optimal + +1. Each of the 31 nonzero masks needs its own unordered pair of prefixes, and + `C(8,2) = 28 < 31`, so `|P| >= 9`. +2. A complete census of all `C(31,8) = 7,888,725` nine-point sets of `F_2^5` + finds **zero** with `P XOR P = F_2^5`; maximum coverage is **29**. Two + independent implementations agree (recursive DFS in the discovery script; + `itertools.combinations` in `verify.py --full`). So `|P| >= 10`. +3. The walk is closed (`z` restoration), so `|P| <= L`; hence `L >= 10`, and + the word attains 10. + +This is a finite computational exclusion for the stated interface, not an +impossibility theorem for other circuit models. + +## Pricing (predecessor fixture) + +Fixture: B factor leaf prices `1, 4, 10, 16, 28`; each `A` leaf price 1; every +call doubled for the inverse in the complete cost; dispatch `D` paid per root +query. Renaming sources preserves coverage, so free relabeling is granted on +both sides. + +| Schedule | Queries | B leaves (min relabeling) | Total leaves | +|---|---:|---:|---:| +| This word, best labeling | 72 | 120 | 182 | +| This word, fixture labeling | 72 | 126 | 188 | +| Predecessor ten-call path | 74 | 118 | 182 | +| Predecessor twelve-call path | 74 | 120 | 182 | + +At the best labeling this schedule ties the predecessor's leaf cost exactly +and saves 2 dispatch records, so the completed cost is strictly lower for any +positive per-query dispatch. At the fixed fixture labeling it pays +`+12` leaf charges (doubled) against `-2 D`, favorable iff one query's +dispatch/dispatch-record cost exceeds 6 leaf-price units. The tie at the best +labeling is optimal among 72-query schedules: a length-10 source path needs at +least one pair call (pure-single ten-call paths are excluded by the +predecessor's 945-pairing census), so its weight sum is at least 12, and +weight sum 12 with even multiplicities gives exactly this multiset. + +## Verification + +```sh +python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py +``` + +Expected: `PASS_CONNECTOR_PAIR_SOURCE_PATH`. Checks the word (two coverage +recomputations), the dirty replay at `L = 1,2,3` with seeded dense +nonsymmetric noncommuting `F_2` maps and arbitrary dirty `x`, `z`, `y` +(exact boundary on all 31 outputs), three mutation controls (dropped call, +mutated step, misplaced readouts) that must all be rejected, and the pricing +numbers. + +```sh +python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py --full +``` + +Expected: `CENSUS {"sets": 7888725, "covering": 0, "max_coverage": 29}` then +`PASS_CONNECTOR_PAIR_SOURCE_PATH_CENSUS`. This is the exact nine-point census +behind `L >= 10`; it takes a few minutes. + +## Scope and limits + +- Exactly one added family (`B_jk`); a different extension is a different + question. Pair calls are charged, never free. +- No instance of this interface is claimed inside the selected supplier; this + is not a kappa claim and the selected record is unchanged. The `a < D/E` + diagnostic is not applicable: no supplier moment or recursive profile + changes here. +- The necessity side (62 readouts, two per nonzero row) inherits the + predecessor's specialization argument unchanged; only the source-path side + changes. +- The census covers nine-point sets exhaustively and finds the length-10 word + by seeded random search over covering sets (seed 4242, trial 911); minimality + rests on the census plus the counting bound, not on search exhaustion at 10. + +## Open next questions + +1. **Do triple-source calls `B_jkℓ` reach the readout-dominated floor?** The + source path could drop toward 8 or 9, but each call's leaf charge grows; + the same prefix-set method answers it. Blocker: none; a bounded census of + weight-3 steps is the first step. +2. **Six sources with pair calls.** The predecessor stops at the five-source + boundary. For six sources the counting bound gives `|P| >= 12` + (`C(11,2) = 55 < 63 <= C(12,2)`); does a pair-call universal path of length + 12 exist? Blocker: the set census grows to `C(63,11)`; it needs a walkwise + search rather than a setwise one. +3. **Common-label realization of pair calls.** The predecessor leaves + realization open for single calls; a pair call needs two coefficient + accesses in one query record, which a real compiler must price. + +Predecessor credit: `research/universal-connector-boundary` (fixed-alphabet +four/five-source boundary, 945-pairing census, 74-query optimum) and PR934's +three-by-three result. Claim thread: +https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18930631 diff --git a/research/connector-pair-source-path-seed2cdb/SOURCES.json b/research/connector-pair-source-path-seed2cdb/SOURCES.json new file mode 100644 index 0000000000..98ff80da60 --- /dev/null +++ b/research/connector-pair-source-path-seed2cdb/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "51122344de9382e784c7f89953456d8cd55513ef", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "path": "research/universal-connector-boundary/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + ] +} diff --git a/research/connector-pair-source-path-seed2cdb/TASK.json b/research/connector-pair-source-path-seed2cdb/TASK.json new file mode 100644 index 0000000000..467c073eb5 --- /dev/null +++ b/research/connector-pair-source-path-seed2cdb/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "seed": "2cdb401748aa1ad1efaa95e93dcff850", + "track": "recursive-interfaces", + "priority_revision": 3, + "scope_key": "0c9f43f3c7d61edb36fe", + "base_commit": "51122344de9382e784c7f89953456d8cd55513ef", + "scope_status": "refined", + "scope_change_reason": "The card asks for one explicit alphabet extension with its implementation charged. Refined to the pair-source connector call family B_jk: z += B_j x_j + B_k x_k on the pinned five-source universal-connector-boundary model: one complete query per pair call, charged two coefficient/source accesses, no other interface change.", + "actual_scope": "Add exactly one operation family (pair-source connector calls B_jk) to the fixed single-source connector alphabet and determine the exact minimum universal source path and exact complete-query optimum for the five-source all-31-nonzero-row matrix in the extended alphabet, priced against the predecessor's fixture.", + "bottleneck_link": "The connector batch's complete queries are recursive-interface boundary work: the fixed alphabet's optimum 74 sat above the 72-query support bound which that alphabet proves unattainable. The pair family changes exactly this boundary cost: 74 -> 72, support bound attained.", + "stop_rule": "Stop when the exact minimum source path is pinned (construction plus exhaustive nine-point census), one fully priced comparison against the predecessor fixture is recorded, and the dirty replay and controls pass. No search beyond length 10 and no second alphabet family in this session.", + "evidence": "verify.py: word with D(w)=F2^5 by two recomputations, dirty replay at L=1,2,3 with seeded dense nonsymmetric noncommuting maps and exact boundary on all 31 outputs, three mutation controls rejected, exact pricing numbers; verify.py --full: independent itertools census of all 7,888,725 nine-point sets (0 covering, maximum coverage 29) excluding length 9.", + "outcome": "completed", + "author": "Aaron Wang", + "ai_assistance": "with help from opencode", + "open_questions": [ + { + "question": "Do triple-source calls B_jkl lower the five-source universal path below ten, and at what leaf price?", + "why_it_matters": "Each added source per call raises leaf cost but could shorten the path; the prefix-set method answers it exactly and would locate the family-size optimum.", + "first_step": "Repeat the closed-walk census with steps of Hamming weight up to 3 (25 step types) at lengths 8 and 9, with the same counting lower bound.", + "blocked_by": "Nothing structural; it is a bounded enumeration, though larger than the weight-1/2 scan." + }, + { + "question": "What is the pair-call universal path minimum for six sources?", + "why_it_matters": "The predecessor stops at the five-source boundary; six sources test whether the pair family scales or the covering sets become walkable only at large length.", + "first_step": "Establish the counting bound (|P| >= 12 since C(11,2) = 55 < 63 <= C(12,2)) and run a walkwise search at lengths 12 and 13 on F_2^6.", + "blocked_by": "The setwise census grows to C(63,11); a walkwise or meet-in-the-middle search is required instead." + }, + { + "question": "How does a real compiler price a pair-source call's second coefficient access inside one query record?", + "why_it_matters": "The 72-query result assumes a pair call is one dispatch record with two coefficient/source accesses; the break-even against the fixed alphabet depends on that price.", + "first_step": "Instantiate one pair call in the universal-connector-boundary tape implementation sketch and count its instruction records and coefficient reads.", + "blocked_by": "The predecessor leaves common-label realization open even for single calls; this inherits that blocker." + } + ], + "predecessor_credit": "research/universal-connector-boundary (fixed-alphabet four/five-source boundary, 945-pairing census, 74-query optimum) and PR934's three-by-three result.", + "time_cap": "one session; census capped at the nine-point scan; one bounded pivot maximum (none used)" +} diff --git a/research/connector-pair-source-path-seed2cdb/VERIFY.json b/research/connector-pair-source-path-seed2cdb/VERIFY.json new file mode 100644 index 0000000000..b6924f7603 --- /dev/null +++ b/research/connector-pair-source-path-seed2cdb/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "word (two coverage recomputations), dirty replay at L=1,2,3 with exact boundary, three mutation controls, pricing numbers", + "timeout_seconds": 300 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py", + "--full" + ], + "checks": "exact nine-point census excluding length 9 (7,888,725 sets; zero covering; maximum coverage 29)", + "timeout_seconds": 600 + } + ], + "inputs": [ + "research/connector-pair-source-path-seed2cdb/verify.py", + "research/connector-pair-source-path-seed2cdb/CERTIFICATE.json" + ] +} diff --git a/research/connector-pair-source-path-seed2cdb/verify.py b/research/connector-pair-source-path-seed2cdb/verify.py new file mode 100644 index 0000000000..eceeaa753d --- /dev/null +++ b/research/connector-pair-source-path-seed2cdb/verify.py @@ -0,0 +1,261 @@ +"""Verify the pair-source connector result (package connector-pair-source-path-seed2cdb). + +Result: with exactly one added operation family -- pair-source connector calls +B_jk: z += B_j x_j + B_k x_k, one complete query per call -- the five-source +universal source path drops from twelve calls (fixed alphabet) to exactly ten, +and the all-31-nonzero-row batch drops from 74 to exactly 72 complete queries, +attaining the support bound the fixed alphabet proves unattainable. + +Checks (fast): + 1. Certificate word: closed walk, steps of Hamming weight 1 or 2, coverage + D(w) = P XOR P = F2^5 by two independent recomputations. + 2. Bound chain constants: C(8,2) = 28 < 31. + 3. Dirty replay at L = 1,2,3: seeded dense nonsymmetric noncommuting F2 + maps, arbitrary dirty x/z/y, all-31 matrix schedule, exact boundary. + 4. Mutation controls: every mutation must break the boundary check. + 5. Pricing: predecessor fixture leaf prices (1,4,10,16,28); query/leaf + counts and the dispatch break-even. + +Checks (--full): the exact nine-point census excluding L = 9 (independent +itertools enumeration of all C(31,8) sets; expects zero covering sets and +maximum coverage 29). + +Aaron Wang, with help from opencode. Apache-2.0. +""" +import itertools +import json +import os +import random +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) + +# Word: closed walk of ten steps over weight-1/2 vectors in F2^5. +PREFIXES = [0, 2, 3, 5, 13, 15, 30, 26, 10, 8, 0] +STEPS = [2, 1, 6, 8, 2, 17, 4, 16, 2, 8] +WEIGHTS = [1, 1, 2, 1, 1, 2, 1, 1, 1, 1] + +PRICES = [1, 4, 10, 16, 28] # predecessor fixture: B factor leaf prices +N_SRC = 5 +N_OUT = 31 + +def wt(v): + return bin(v).count("1") + +def coverage_pairs(points): + """Method 1: explicit pairwise XOR set.""" + return {a ^ b for a in points for b in points} + +def coverage_bits(points): + """Method 2: bitmask accumulation.""" + cov = 0 + for i in range(len(points)): + for j in range(len(points)): + cov |= 1 << (points[i] ^ points[j]) + return cov + +def check_word(): + assert PREFIXES[0] == 0 and PREFIXES[-1] == 0, "walk must close" + assert len(STEPS) == 10 == len(PREFIXES) - 1 + for i, s in enumerate(STEPS): + assert s != 0 and wt(s) in (1, 2), "step %d not a legal call" % i + assert PREFIXES[i] ^ PREFIXES[i + 1] == s, "step %d disagrees with prefixes" % i + P = PREFIXES[:-1] # distinct prefixes (q_10 = q_0) + assert len(set(P)) == 10, "prefix set must be simple" + cov1 = coverage_pairs(P) + cov2 = coverage_bits(P) + assert len(cov1) == 32 and cov2 == (1 << 32) - 1, "coverage must be all of F2^5" + assert sum(1 for v in range(32) if v in cov1) == 32 + mults = [sum(1 for s in STEPS if s >> j & 1) for j in range(N_SRC)] + assert all(m % 2 == 0 for m in mults), "closure forces even multiplicities" + return mults + +def boundaries_for(mask): + """First pair of prefixes whose XOR is the mask.""" + for s in range(len(PREFIXES)): + for t in range(s + 1, len(PREFIXES)): + if PREFIXES[s] ^ PREFIXES[t] == mask: + return s, t + raise AssertionError("mask %d uncovered" % mask) + +def schedule(): + """All-31 matrix: readout pairs per output at prefix boundaries.""" + out = [[] for _ in PREFIXES] + for m in range(1, N_OUT + 1): + s, t = boundaries_for(m) + out[s].append((m, 0)) + out[t].append((m, 1)) + return out + +def mat_vec(rows, x): + r = 0 + k = 0 + while x: + if x & 1: + r ^= rows[k] + x >>= 1 + k += 1 + return r + +def run_schedule(word, sched, Bm, Am, xs, z0, ys): + """Execute complete calls; return final (z, ys) or None on contract error.""" + z = z0 + ys = list(ys) + if len(word) != 10: + return None + for step in range(11): + for (m, half) in sched[step]: + ys[m - 1] ^= mat_vec(Am[m - 1], z) + if step < 10: + s = word[step] + for j in range(N_SRC): + if s >> j & 1: + z ^= mat_vec(Bm[j], xs[j]) + return z, ys + +def expected_for_mask(mask, Bm, Am, xs): + acc = 0 + for j in range(N_SRC): + if mask >> j & 1: + acc ^= mat_vec(Am, mat_vec(Bm[j], xs[j])) + return acc + +def check_replay(): + """Smallest falsifying instances: L = 1,2,3 with dirty state.""" + sched = schedule() + cases = 0 + for L in (1, 2, 3): + for case in range(2): + rng = random.Random(1000 * L + case + 7) + Bm = [[rng.getrandbits(L) for _ in range(L)] for _ in range(N_SRC)] + Am = [[rng.getrandbits(L) for _ in range(L)] for _ in range(N_OUT)] + xs = [rng.getrandbits(L) for _ in range(N_SRC)] + z0 = rng.getrandbits(L) + ys0 = [rng.getrandbits(L) for _ in range(N_OUT)] + z, ys = run_schedule(STEPS, sched, Bm, Am, xs, z0, ys0) + assert z == z0, "z must be restored (L=%d case %d)" % (L, case) + for m in range(1, N_OUT + 1): + exp = expected_for_mask(m, Bm, Am[m - 1], xs) + assert ys[m - 1] == ys0[m - 1] ^ exp, ( + "output %d wrong at L=%d case %d" % (m, L, case)) + cases += 1 + return cases + +def check_controls(): + """Every mutation must break the boundary check on a replay case.""" + sched = schedule() + L = 3 + rng = random.Random(4242) + Bm = [[rng.getrandbits(L) for _ in range(L)] for _ in range(N_SRC)] + Am = [[rng.getrandbits(L) for _ in range(L)] for _ in range(N_OUT)] + xs = [rng.getrandbits(L) for _ in range(N_SRC)] + z0 = rng.getrandbits(L) + ys0 = [rng.getrandbits(L) for _ in range(N_OUT)] + + def boundary_ok(word, sched_local): + r = run_schedule(word, sched_local, Bm, Am, xs, z0, ys0) + if r is None: + return False + z, ys = r + if z != z0: + return False + for m in range(1, N_OUT + 1): + exp = expected_for_mask(m, Bm, Am[m - 1], xs) + if ys[m - 1] != ys0[m - 1] ^ exp: + return False + return True + + assert boundary_ok(STEPS, sched), "positive control must pass" + + # Control 1: drop one source call (breaks closure). + w1 = STEPS[:-1] + [0] + assert not boundary_ok(w1, sched), "dropped call must be rejected" + + # Control 2: mutate one pair call to a different legal step. + w2 = list(STEPS) + w2[3] = 3 + assert not boundary_ok(w2, sched), "mutated step must be rejected" + + # Control 3: move output 5's readouts one boundary later (wrong mask). + s3 = [row[:] for row in sched] + moved = [] + for row in s3: + moved.append([(m, h) for (m, h) in row if m != 5]) + s, t = boundaries_for(5) + moved[(s + 1) % 11].append((5, 0)) + moved[(t + 1) % 11].append((5, 1)) + assert not boundary_ok(STEPS, moved), "misplaced readouts must be rejected" + return 3 + +def check_pricing(): + mults = [sum(1 for s in STEPS if s >> j & 1) for j in range(N_SRC)] + assert sum(mults) == 12 + fixed = sum(m * c for m, c in zip(mults, PRICES)) + srt = sorted(mults, reverse=True) + prs = sorted(PRICES) + min_cost = sum(m * c for m, c in zip(srt, prs)) + max_cost = sum(m * c for m, c in zip(srt, reversed(prs))) + queries = 10 + 2 * N_OUT # source calls + two readouts per nonzero output + leaves_min = min_cost + N_OUT * 2 + assert queries == 72 + # predecessor fixture rows (universal-connector-boundary README table) + pred = {"ten-call path": (74, 182), "twelve-call path": (74, 200)} + return { + "multiplicities": mults, + "b_leaf_cost_fixed_labeling": fixed, + "b_leaf_cost_min_relabeling": min_cost, + "b_leaf_cost_max_relabeling": max_cost, + "queries": queries, + "leaves_min_relabeling": leaves_min, + "predecessor_rows": pred, + } + +def full_census(): + """Independent itertools enumeration of all nine-point sets.""" + total = 0 + covering = 0 + max_cov = 0 + for comb in itertools.combinations(range(1, 32), 8): + pts = (0,) + comb + cov = 1 # zero mask + for i in range(9): + pi = pts[i] + for j in range(i + 1, 9): + cov |= 1 << (pi ^ pts[j]) + total += 1 + c = cov.bit_count() + if c > max_cov: + max_cov = c + if cov == (1 << 32) - 1: + covering += 1 + assert total == 7888725, total + assert covering == 0, covering + assert max_cov == 29, max_cov + return {"sets": total, "covering": covering, "max_coverage": max_cov} + +def main(): + cert_path = os.path.join(HERE, "CERTIFICATE.json") + with open(cert_path, "r", encoding="utf-8") as f: + cert = json.load(f) + assert cert["prefixes"] == PREFIXES and cert["word_steps"] == STEPS, ( + "CERTIFICATE.json disagrees with verify.py constants") + + mults = check_word() + cases = check_replay() + controls = check_controls() + pricing = check_pricing() + + if "--full" in sys.argv: + census = full_census() + print("CENSUS", json.dumps(census)) + print("PASS_CONNECTOR_PAIR_SOURCE_PATH_CENSUS") + return + + print("word ok: 10 steps, coverage 32, multiplicities", mults) + print("replay ok: %d dirty cases at L=1,2,3" % cases) + print("controls ok: %d mutations rejected" % controls) + print("pricing", json.dumps(pricing)) + print("PASS_CONNECTOR_PAIR_SOURCE_PATH") + +if __name__ == "__main__": + main()