From 1f1c37ba713d027fb0c568f0dcfa41c42feaa884 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 14:49:49 +0000 Subject: [PATCH] feat(research): prove exact 20-ADD G20 chain/exchange component floor The 18-register chain/exchange component of the PR5840 boundary splits into two closed 9-wire parts. Exhaustive budgeted search, with row and transposed-column admissible bounds, excludes every scratch-free word of at most 19 ADDs on the 18 wires, so the source 20 is exact. No new kappa. --- research/g20-chain-exchange-floor/PROOF.md | 94 +++++++ research/g20-chain-exchange-floor/README.md | 99 +++++++ .../g20-chain-exchange-floor/SOURCES.json | 24 ++ research/g20-chain-exchange-floor/TASK.json | 103 +++++++ research/g20-chain-exchange-floor/VERIFY.json | 36 +++ research/g20-chain-exchange-floor/verify.py | 254 ++++++++++++++++++ 6 files changed, 610 insertions(+) create mode 100644 research/g20-chain-exchange-floor/PROOF.md create mode 100644 research/g20-chain-exchange-floor/README.md create mode 100644 research/g20-chain-exchange-floor/SOURCES.json create mode 100644 research/g20-chain-exchange-floor/TASK.json create mode 100644 research/g20-chain-exchange-floor/VERIFY.json create mode 100644 research/g20-chain-exchange-floor/verify.py diff --git a/research/g20-chain-exchange-floor/PROOF.md b/research/g20-chain-exchange-floor/PROOF.md new file mode 100644 index 0000000000..3d5f4282f1 --- /dev/null +++ b/research/g20-chain-exchange-floor/PROOF.md @@ -0,0 +1,94 @@ +# Exact minimum of the G20 chain/exchange component + +## Model + +Work over F2 on the 32 boundary wires of PR5840. A state is a list of rows: +row `w` is the set of input coordinates currently held on wire `w`. An ADD is +`x_d <- x_d + x_s` with `d != s`, cost one. No scratch, reset, copy or free +relabelling of wires is allowed. A word implements a target when it maps the +identity rows to the target rows exactly. + +## The component + +Replaying the authenticated PR5840 `left_program` gives `left_rows`. Wires +`0..15, 30, 31` form a closed set: their rows read only those coordinates and +no other wire reads them. The source word spends fourteen chain ADDs and two +three-ADD exchanges (`SWAP 15 30`, `SWAP 14 31`) there: **20 ADDs**. The other +fourteen wires carry the three isolated four-wire bank exchanges covered by +#5850/#5851 and two untouched wires. + +The 18-register component splits again into two closed 9-wire parts: + +``` +even wires 0,2,...,12 : x_{2i} = e_{2i} + e_{2i+2} (i = 0..6) + wire 14 : e_31 + wire 31 : e_14 +odd wire 1 : e_1 + wires 3,...,13 : x_{2i+1} = e_1 + e_3 + ... + e_{2i+1} + wire 15 : e_30 + wire 30 : e_1 + e_3 + ... + e_13 + e_15 +``` + +The source spends ten ADDs on each part. + +## Statement + +1. Every word on the nine even wires implementing the even part has at least + 10 ADDs. The same holds for the odd part. +2. Every word on all eighteen component wires implementing the component, + including words whose ADDs cross between the even and odd parts, has at + least 20 ADDs. +3. The right boundary is the reverse of the left word and the exact inverse + map, so it has the same minimum. Each component side is exactly 20. + +## Hand proof of the even bound + +All nine even rows differ from the identity, so each even wire is a +destination at least once. A nine-ADD word therefore updates each wire exactly +once, and that update must produce its final row. A chain wire `2i` holds +`e_{2i}` before its update and its final row after it, so it never holds a +coordinate `e_31`. Suppose wire 14 is updated first among 14 and 31. Its +source must hold `e_14 + e_31`; wire 31 still holds `e_31`, and no chain wire +holds `e_31`. If wire 31 is updated first, its source must also hold +`e_14 + e_31`; wire 14 still holds `e_14`. Either case is impossible. + +## Computer proof of all three bounds + +`verify.py` runs an exhaustive depth-first search for each budget from zero up +to the source cost. It prunes a state only by two admissible bounds: + +- each row of the state that differs from the target needs one more ADD; +- the remaining map `R = target * state^-1` needs at least as many ADDs as it + has non-unit columns. The reversed word of transposed ADDs implements `R^T` + with the same length, and the row bound applies to `R^T`. + +The search tracks `R^T` incrementally: the state step `x_a += x_c` changes +`R^T` row `c` to `R^T[c] + R^T[a]`. A memo records the largest failed budget +for each state, which is sound because failure at budget `b` implies failure +at every smaller budget. Every ADD of the restricted wire set is tried at each +node, so no ordering or normal form is assumed. A search that exceeds its node +limit fails the check instead of reporting a bound. + +The first feasible budget is the minimum. Its witness word is replayed as rows +and on every Boolean input of the wires. Four controls must behave as known: +the chain alone needs exactly 14, a weakened even target fits in nine, and a +two-wire exchange needs exactly three. + +## Consequence for the source boundary + +Within the stated model, a side of the PR5840 boundary cannot gain by +resynthesising the chain together with the bank 7/15 exchange, or by mixing +even and odd chain wires, as long as the gates stay on these 18 wires. +Adding the component-local six-ADD floor of the other three exchanges +(#5850/#5851) gives 20 + 18 = 38 per side and 76 per port. This is still a +component-local statement: gates linking the 18 wires to the exchange wires or +to the two untouched wires are not covered, so no global 32-wire minimum is +proved. + +## Not covered + +General GL2 bases inside equal-target pairs (pairs `(2k, 2k+1)` mix the even +and odd parts and change the target), scratch or helper wires, gates leaving +the component, changed controllers, nonunit tariffs, and any recursive, +physical, compiler or precision cost. The paid recursive profile is unchanged +and kappa is unchanged. diff --git a/research/g20-chain-exchange-floor/README.md b/research/g20-chain-exchange-floor/README.md new file mode 100644 index 0000000000..4a17f10717 --- /dev/null +++ b/research/g20-chain-exchange-floor/README.md @@ -0,0 +1,99 @@ +# G20 chain/exchange component: exact 20-ADD minimum + +**Scoped negative result; no new kappa.** The remaining 18-register component +of the PR5840 G20 boundary (wires 0-15, 30, 31: fourteen chain ADDs plus the +bank 7/15 exchange) needs exactly **20 unit ADDs per side**, even when gates +may mix chain and exchange operations anywhere on those 18 wires. The source +attains 20. The component splits into two closed 9-wire parts, and each needs +exactly 10. + +This answers, inside the component, the question that +[#5850](https://github.com/CrocSwap/integer-mult-bounds/pull/5850) leaves open +("the remaining 18-register component ... may permit a cheaper complete +boundary") and the joint chain/exchange question of +[#5851](https://github.com/CrocSwap/integer-mult-bounds/pull/5851). With their +component-local six-ADD exchange floor, 20 + 3 x 6 = 38 per side and 76 per +port stay optimal for synthesis that keeps gates inside each component. + +Claim type: finite exhaustive certificate (a computer proof), with a written +model and a hand proof of the even 9-wire bound in [PROOF.md](PROOF.md). It is +not a 32-wire global minimum, a search failure, a new kappa or a complete +multiplication theorem. + +## Result + +| Target (scratch-free, unit ADDs) | Wires | Source cost | Exact minimum | +|---|---:|---:|---:| +| even part: chain on 0,2,...,12 with exchange 14/31 | 9 | 10 | 10 | +| odd part: prefix chain on 1,3,...,13 with exchange 15/30 | 9 | 10 | 10 | +| whole component, cross-part gates allowed | 18 | 20 | 20 | + +The search excludes every word of at most 19 ADDs on the 18 wires. It visits +2,016,480 nodes at budget 19 and finds a 20-ADD witness at budget 20. + +## Reproduce + +From the repository root, with CPython 3.12 and only the standard library: + +```sh +python3 -I -W error -B research/g20-chain-exchange-floor/verify.py +python3 -B scripts/research_package.py --package research/g20-chain-exchange-floor +``` + +Expected last line of the direct run: +`PASS_G20_CHAIN_EXCHANGE_FLOOR component18=20 even9=10 odd9=10 controls=4`. +Locally a run takes about 35 seconds and 400 MB of memory. + +The only live input is the PR5840 controller already vendored by #5851 at +`research/g20-isolated-exchange-floor/inputs/CONTROLLER.json` (SHA256 pinned in +[SOURCES.json](SOURCES.json) and checked by the verifier). The verifier replays +both source programs against the stored rows, checks that the 18 wires are +closed and that the right boundary is the exact inverse, then runs the search. + +## Method + +Exhaustive depth-first search for each budget, trying every ADD on the wire +set at every node. Pruning uses two admissible bounds: rows that still differ +from the target, and non-unit columns of the remaining map (valid because the +reversed transposed word has the same length). Failed states are memoized with +their largest failed budget. A node limit turns an overlong search into a +failure, never into a bound. Witnesses are replayed on all Boolean inputs. +Controls: the chain alone needs exactly 14, a weakened even target fits in +nine, and a two-wire exchange needs exactly three. + +## Limits + +Not covered: gates linking the component to the other 14 boundary wires, +general GL2 bases in the equal-target pairs `(2k, 2k+1)` (they mix the two +parts and change the target), scratch or helpers, a changed controller, +nonunit tariffs, and every recursive, physical, compiler, precision or analytic +obligation. The paid recursive profile is unchanged. The selected conditional +kappa 0.00310045 and its five framework assumptions are unchanged. + +## Open next questions + +1. Does any scratch-free word on all 32 boundary wires implement one side in + fewer than 38 ADDs? This matters because every current floor is + component-local. First step: run the same search on the chain component + plus one four-wire exchange (22 wires, budget 25). Blocker: search cost + grows quickly with wires and slack, so a stronger bound or a written + argument is likely needed. +2. Do GL2 bases inside the equal-target pairs lower the 20-ADD component cost? + This matters because pair bases are the freedom PR5840 released. First + step: enumerate the pair-basis orbit of the 18-wire target up to + cost-preserving symmetries and search the cheapest representatives. + Blocker: each basis must also be priced at the caller and checked against + the target diagonal. + +Structured versions are in [TASK.json](TASK.json). + +## Credit + +Ali Romman supplied the PR5840 G20 target-pair boundary and its controller. +Charan . (#5850, #5851) posed the 18-register and joint chain/exchange +questions and proved the isolated four-wire exchange floor cited above; the +controller copy vendored by #5851 is the input. Their retained lineage +(PR5834, PR5807/5828, PR5708/5671, ai-nanachi PR5512, Dugongue, ToikY) is +recorded in those packages. Budgeted depth-first search and the transpose +argument are standard; the new work is the component decomposition, the exact +20-ADD minimum and its verifier, produced by Nick Petalas. Apache-2.0. diff --git a/research/g20-chain-exchange-floor/SOURCES.json b/research/g20-chain-exchange-floor/SOURCES.json new file mode 100644 index 0000000000..0aa2e7a3f4 --- /dev/null +++ b/research/g20-chain-exchange-floor/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json", + "usage": "input", + "git_blob": "73fa9f40a032f11dabf357eba69066fcf9bf0a02", + "sha256": "978536e852c0cfbc150f143e19d2cfddbb434bac6017d914974eb99f641593a8" + } + ] +} diff --git a/research/g20-chain-exchange-floor/TASK.json b/research/g20-chain-exchange-floor/TASK.json new file mode 100644 index 0000000000..c8534208f5 --- /dev/null +++ b/research/g20-chain-exchange-floor/TASK.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact scratch-free unit-ADD minimum of the 18-register chain/exchange component (wires 0-15, 30, 31) of the PR5840 G20 boundary: 20 per side, with both closed 9-wire parts exactly 10. Gates may cross between the parts but stay on the 18 wires.", + "scope_change_reason": "The card asks for a changed helper path or independent-target split with a complete BIT moment. This side result instead answers the boundary-synthesis question PR5850 leaves open for the remaining 18-register component, without changing helpers, targets or the recursive profile.", + "bottleneck_link": "Closes one proposed scalar route to a cheaper G20 boundary: joint chain/exchange resynthesis on the component wires cannot beat the source. Remaining scalar routes must use gates leaving the component, scratch, GL2 pair bases or a changed controller.", + "budget_minutes": 60, + "stop_rule": "Stop at the exact minimum for the 18-wire component (or a shorter witness). Do not enlarge to the full 32-wire boundary.", + "outcome": "negative-result", + "evidence": "verify.py: exhaustive budgeted search with admissible row/column bounds, witness replay on all Boolean inputs, four controls; PROOF.md gives the model and a hand proof of the even 9-wire bound.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does any scratch-free ADD word on all 32 boundary wires implement a PR5840 boundary side in fewer than 38 ADDs?", + "why_it_matters": "This result and PR5850/PR5851 are component-local; gates linking the chain component to the exchange or untouched wires are not covered.", + "first_step": "Extend the same budgeted search to the chain component plus one four-wire exchange (22 wires, budget 25) before attempting all 32 wires.", + "blocked_by": "Search cost grows quickly with wires and slack; a stronger admissible bound or a written argument is needed." + }, + { + "question": "Do general GL2 bases inside the equal-target pairs (2k, 2k+1) of the chain component lower its 20-ADD cost?", + "why_it_matters": "Pair bases mix the even and odd 9-wire parts and change the target map, so this exact minimum does not cover them.", + "first_step": "Enumerate the pair-basis orbit of the 18-wire target modulo the bases that leave the cost unchanged and search the cheapest representatives.", + "blocked_by": "Each basis change must also be priced at the caller and checked against the target diagonal." + } + ], + "predecessors": [ + { + "pr": 5850, + "author": "Charan .", + "path": "research/g20-gl2-tail-floor", + "relationship": "Poses the open 18-register component question; its four-wire exchange floor is cited for the 38-per-side total." + }, + { + "pr": 5851, + "author": "Charan .", + "path": "research/g20-isolated-exchange-floor", + "relationship": "Its vendored PR5840 controller is the live input; its isolated-exchange floor is cited, not replayed." + }, + { + "pr": 5840, + "author": "Ali Romman", + "relationship": "G20 target-pair boundary construction whose left/right programs are the object studied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219123" +} diff --git a/research/g20-chain-exchange-floor/VERIFY.json b/research/g20-chain-exchange-floor/VERIFY.json new file mode 100644 index 0000000000..7698056cd3 --- /dev/null +++ b/research/g20-chain-exchange-floor/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Source replay and component closure, exhaustive budgeted exclusion of words of at most 19 ADDs on the 18-wire component (9 for each 9-wire part), witness replay on all Boolean inputs, four controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same exact exclusion and controls with assertions disabled; all checks use explicit exceptions." + } + ] +} diff --git a/research/g20-chain-exchange-floor/verify.py b/research/g20-chain-exchange-floor/verify.py new file mode 100644 index 0000000000..784c6c6ab6 --- /dev/null +++ b/research/g20-chain-exchange-floor/verify.py @@ -0,0 +1,254 @@ +#!/usr/bin/env python3 +"""Exact ADD minimum for the PR5840 G20 chain/exchange component. + +Replays the authenticated PR5840 boundary words, extracts the 18-register +component (wires 0..15, 30, 31), and proves by exhaustive budgeted search +that no scratch-free word of at most 19 unit ADDs on those 18 wires implements +it. The source word has 20 ADDs, so 20 is exact. The two closed 9-wire +subcomponents are each shown to need exactly 10. + +Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import json +import sys +import time +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +CONTROLLER = ROOT / "research/g20-isolated-exchange-floor/inputs/CONTROLLER.json" +CONTROLLER_SHA256 = "978536e852c0cfbc150f143e19d2cfddbb434bac6017d914974eb99f641593a8" +WIRES = 32 +COMPONENT = tuple(range(16)) + (30, 31) +EVEN = (0, 2, 4, 6, 8, 10, 12, 14, 31) +ODD = (1, 3, 5, 7, 9, 11, 13, 15, 30) +SEARCH_LIMIT_NODES = 50_000_000 + + +class CheckError(Exception): + pass + + +def require(condition, message): + if not condition: + raise CheckError(message) + + +def run_program(program): + """Rows are bitmasks of input coordinates held on each wire. + + ["ADD", d, s] means x_d <- x_d + x_s; ["SWAP", a, b] exchanges wires. + """ + rows = [1 << i for i in range(WIRES)] + for op, a, b in program: + require(a != b and 0 <= a < WIRES and 0 <= b < WIRES, f"bad operands {op} {a} {b}") + if op == "SWAP": + rows[a], rows[b] = rows[b], rows[a] + elif op == "ADD": + rows[a] ^= rows[b] + else: + raise CheckError(f"unknown instruction {op}") + return rows + + +def restrict(rows, wires): + """Rows of the closed wire set, re-indexed to local coordinates.""" + local = {w: i for i, w in enumerate(wires)} + out = [] + for w in wires: + mask = 0 + for j in range(WIRES): + if rows[w] >> j & 1: + require(j in local, f"wire {w} reads coordinate {j} outside its component") + mask |= 1 << local[j] + out.append(mask) + for w in range(WIRES): + if w not in local: + require(all(not (rows[w] >> j & 1) for j in wires), + f"outside wire {w} reads component coordinates") + return tuple(out) + + +def transpose(rows): + n = len(rows) + return tuple(sum(((rows[i] >> j) & 1) << i for i in range(n)) for j in range(n)) + + +class Search: + """Is the target reachable from the identity within a given ADD budget? + + Admissible prunes: every row of the current state that differs from the + target is the destination of at least one remaining ADD; the transpose of + the remaining map R = target * state^-1 has a word of the same length, so + every non-unit column of R also needs one. R^T is tracked incrementally: + the row step x_a += x_c on the state turns R^T row c into R^T[c] + R^T[a]. + Failed (state, budget) pairs are memoized; failure at budget b implies + failure at every smaller budget. + """ + + def __init__(self, target): + self.target = tuple(target) + self.n = len(target) + self.unit = tuple(1 << i for i in range(self.n)) + self.ops = [(a, c) for a in range(self.n) for c in range(self.n) if a != c] + self.failed = {} + self.nodes = 0 + + def reachable(self, budget): + self.failed.clear() + self.nodes = 0 + word = [] + found = self._dfs(self.unit, transpose(self.target), budget, word) + return found, list(reversed(word)) + + def _dfs(self, state, rt, budget, word): + # Children are bound-checked here before recursion; the bound of the + # root is checked by the caller-facing wrapper below. + self.nodes += 1 + if self.nodes > SEARCH_LIMIT_NODES: + raise CheckError("search node limit exceeded; result would be inconclusive") + target, unit = self.target, self.unit + if state == target: + return True + if budget <= 0 or self.failed.get(state, -1) >= budget: + return False + rows_off = sum(1 for i in range(self.n) if state[i] != target[i]) + cols_off = sum(1 for j in range(self.n) if rt[j] != unit[j]) + if max(rows_off, cols_off) > budget: + return False + child = budget - 1 + for a, c in self.ops: + new_a = state[a] ^ state[c] + r = rows_off - (state[a] != target[a]) + (new_a != target[a]) + if r > child: + continue + new_c = rt[c] ^ rt[a] + k = cols_off - (rt[c] != unit[c]) + (new_c != unit[c]) + if k > child: + continue + nxt = list(state) + nxt[a] = new_a + nrt = list(rt) + nrt[c] = new_c + if self._dfs(tuple(nxt), tuple(nrt), child, word): + word.append((a, c)) + return True + self.failed[state] = budget + return False + + +def apply_local(word, n): + rows = [1 << i for i in range(n)] + for a, c in word: + rows[a] ^= rows[c] + return tuple(rows) + + +def exact_minimum(target, floor, label): + """Return (minimum, witness, per-budget node counts) with exclusion below.""" + search = Search(target) + log = [] + for budget in range(floor + 1): + start = time.perf_counter() + found, word = search.reachable(budget) + log.append((budget, found, search.nodes, round(time.perf_counter() - start, 2))) + if found: + require(len(word) <= budget, f"{label}: witness longer than budget") + require(apply_local(word, len(target)) == tuple(target), f"{label}: witness does not replay") + return budget, word, log + raise CheckError(f"{label}: no word within {floor} ADDs") + + +def literal_check(word, wires, target_rows): + """Replay a local ADD word on all 2^k Boolean inputs of its wires.""" + k = len(wires) + for x in range(1 << k): + vals = [(x >> i) & 1 for i in range(k)] + for a, c in word: + vals[a] ^= vals[c] + for i in range(k): + expect = bin(target_rows[i] & x).count("1") & 1 + require(vals[i] == expect, "literal truth-table mismatch") + + +def main(): + raw = CONTROLLER.read_bytes() + require(hashlib.sha256(raw).hexdigest() == CONTROLLER_SHA256, "controller SHA256 mismatch") + boundaries = json.loads(raw)["boundaries"] + left = run_program(boundaries["left_program"]) + right = run_program(boundaries["right_program"]) + require(left == boundaries["left_rows"], "left rows do not replay") + require(right == boundaries["right_rows"], "right rows do not replay") + require(boundaries["boundary_unit_ADDs_per_port"] == 76, "source ADD count changed") + + def adds_in(program, wires): + return sum(1 for op, a, b in program if op == "ADD" and a in wires) + + def swaps_in(program, wires): + return sum(1 for op, a, b in program if op == "SWAP" and a in wires) + + comp = set(COMPONENT) + require(adds_in(boundaries["left_program"], comp) == 14, "left chain count") + require(swaps_in(boundaries["left_program"], comp) == 2, "left swap count") + require(all(b in comp for op, a, b in boundaries["left_program"] if a in comp), "component not closed") + source_cost = 14 + 3 * 2 + require(source_cost == 20, "source component cost") + + left_comp = restrict(left, COMPONENT) + right_comp = restrict(right, COMPONENT) + even = restrict(left, EVEN) + odd = restrict(left, ODD) + + # The inverse boundary is the reversed word (every ADD and SWAP is an + # involution), so it has the same exact minimum. Check it is the inverse. + n = len(COMPONENT) + composed = [0] * n + for i in range(n): + for j in range(n): + if right_comp[i] >> j & 1: + composed[i] ^= left_comp[j] + require(tuple(composed) == tuple(1 << i for i in range(n)), "right is not the inverse of left") + + results = {} + for label, target, floor in (("even9", even, 10), ("odd9", odd, 10), ("component18", left_comp, 20)): + start = time.perf_counter() + minimum, word, log = exact_minimum(target, floor, label) + literal_check(word, list(range(len(target))), target) + results[label] = minimum + print(f"{label}: minimum={minimum} nodes_by_budget={[(b, nodes) for b, _, nodes, _ in log]} " + f"seconds={time.perf_counter() - start:.1f}", flush=True) + + require(results == {"even9": 10, "odd9": 10, "component18": 20}, f"unexpected minima {results}") + + # Controls: the search must find known shorter words. + # 1. The chain alone (no exchange) costs its 14 ADDs, below 20. + chain_only = [1 << i for i in range(WIRES)] + for op, a, b in boundaries["left_program"]: + if op == "ADD": + chain_only[a] ^= chain_only[b] + chain_comp = restrict(chain_only, COMPONENT) + found, _ = Search(chain_comp).reachable(14) + require(found, "control: chain-only target should fit in 14") + found, _ = Search(chain_comp).reachable(13) + require(not found, "control: chain-only target should not fit in 13") + # 2. A target with one chain ADD removed must be reachable in 9 on 9 wires. + weakened = list(even) + weakened[0] = 1 # wire 0 left unchanged + found, word = Search(tuple(weakened)).reachable(9) + require(found and len(word) <= 9, "control: weakened even target should fit in 9") + # 3. A pure exchange of two wires costs exactly three. + swap = (2, 1) + require(not Search(swap).reachable(2)[0] and Search(swap).reachable(3)[0], "control: swap") + + print("one side: chain/exchange component 20 + three isolated exchanges 3*6 = 38; both sides 76") + print("PASS_G20_CHAIN_EXCHANGE_FLOOR component18=20 even9=10 odd9=10 controls=4") + return 0 + + +if __name__ == "__main__": + try: + sys.exit(main()) + except CheckError as exc: + print(f"FAIL_G20_CHAIN_EXCHANGE_FLOOR: {exc}", file=sys.stderr) + sys.exit(1)