From 95fd439596f72575d3869277c2d01aca1ca6ab6a Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 22:02:42 -0500 Subject: [PATCH] research: add borrowed-source Gray mask fanout --- .../EXPECTED.json | 15 ++ .../PROOF.md | 66 ++++++++ .../README.md | 120 ++++++++++++++ .../SOURCES.json | 148 ++++++++++++++++++ .../TASK.json | 104 ++++++++++++ .../VERIFY.json | 40 +++++ .../verify.py | 129 +++++++++++++++ 7 files changed, 622 insertions(+) create mode 100644 research/borrowed-source-gray-mask-fanout-seed9b2fe133/EXPECTED.json create mode 100644 research/borrowed-source-gray-mask-fanout-seed9b2fe133/PROOF.md create mode 100644 research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md create mode 100644 research/borrowed-source-gray-mask-fanout-seed9b2fe133/SOURCES.json create mode 100644 research/borrowed-source-gray-mask-fanout-seed9b2fe133/TASK.json create mode 100644 research/borrowed-source-gray-mask-fanout-seed9b2fe133/VERIFY.json create mode 100644 research/borrowed-source-gray-mask-fanout-seed9b2fe133/verify.py diff --git a/research/borrowed-source-gray-mask-fanout-seed9b2fe133/EXPECTED.json b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/EXPECTED.json new file mode 100644 index 0000000000..853af8d900 --- /dev/null +++ b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/EXPECTED.json @@ -0,0 +1,15 @@ +{ + "status": "PASS_GRAY_MASK_FANOUT", + "width": 1, + "source_rows": 3, + "target_classes": 3, + "targets_per_class": 3, + "scalar_boundary_states": 4096, + "direct_adds": 21, + "borrowed_adds": 13, + "anchor_transition_adds": 4, + "target_write_adds": 9, + "saving_adds": 8, + "minimum_closed_tour_adds": 4, + "negative_controls": 4 +} diff --git a/research/borrowed-source-gray-mask-fanout-seed9b2fe133/PROOF.md b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/PROOF.md new file mode 100644 index 0000000000..dfd4e970f3 --- /dev/null +++ b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/PROOF.md @@ -0,0 +1,66 @@ +# Exact boundary proof and scoped cost statement + +## Algebraic identity + +Work over `F2`. The twelve input rows are + +``` +(A, B, C, X_1, X_2, X_3, Y_1, Y_2, Y_3, Z_1, Z_2, Z_3). +``` + +An operation `u ^= v` replaces row `u` by `u+v`; it is an invertible +elementary row operation for arbitrary row values. Apply, in order, + +``` +A ^= B +X_i ^= A (i = 1,2,3) +A ^= C +Y_i ^= A (i = 1,2,3) +A ^= B +Z_i ^= A (i = 1,2,3) +A ^= C +``` + +The successive values of `A` are `A+B`, `A+B+C`, `A+C`, and `A`. Therefore +the three target families receive exactly `A+B`, `A+B+C`, and `A+C`, while +`A`, `B`, and `C` return to their initial values. This proves the boundary +identity for arbitrary rows, not only for the finite replay inputs. Since +row ADDs act coordinatewise, the identity holds for every width `L`. + +The reverse sequence restores the complete input. Every operation is +self-inverse, so this inverse uses the same 13 charged ADDs. + +## Cost accounting + +The independent per-target circuit uses `2+3+2 = 7` ADDs per three-target +class: two per `X_i`, three per `Y_i`, and two per `Z_i`. Its total is 21. +The borrowed-source circuit uses four anchor transitions and one write to +each of nine targets, for a total of 13. Each ADD reads one source row and +writes one destination row, so these operation, row-read, and row-write +counts all decrease from 21 to 13. At width `L`, each count of ADDs +corresponds to that many length-`L` XOR passes; the arithmetic bill is 21L +versus 13L bit XORs. + +The mask-state path is a closed walk on the square `Q_2`. It starts at `00`, +visits `10`, `11`, and `01`, and returns to `00`. A closed walk visiting all +four vertices has at least four edges; the displayed Gray cycle has four. +Thus the anchor-transition count is optimal among one-anchor schedules that +visit each required mask state and perform one ADD per target. Combined +with the necessary nine target writes in that schedule class, the class +minimum is 13. No unrestricted CNOT lower bound is claimed. + +## Exact certificate coverage + +`verify.py` constructs the 12-by-12 transfer matrix over `F2` for both the +independent and borrowed schedules and requires exact equality with the +specified boundary matrix. It then checks all 4096 scalar input states, +including all source and target values, and checks that reversing the +borrowed schedule restores every state. The negative controls remove the +final restoration, one mask transition, one target write, or replace the +return transition with the wrong source. Each must fail the complete +boundary comparison. + +This is a small exact construction certificate, not a supplier invoice. +Every listed operation is charged. The model contains no tape head, clean +allocation, copies, hosted execution, frame conversion, precision bound, +or recursive multiplication call, so those quantities are not inferred. diff --git a/research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md new file mode 100644 index 0000000000..e38b2c442c --- /dev/null +++ b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md @@ -0,0 +1,120 @@ +# Borrowed source rows can tour several parity masks + +**Exact local bit-circuit construction; no new kappa.** Three arbitrary +source rows and nine arbitrary target rows require 21 independent row ADDs +to apply three different source parities to three targets each. A borrowed +source row can walk through the three parity masks in one closed Gray tour, +fan each mask out once, and return to its arbitrary initial value in 13 +ADDs. The eight-ADD saving includes the complete source restoration. + +## Boundary map + +For any row width `L >= 1`, let `A`, `B`, `C` and all target rows be +arbitrary elements of `F2^L`. The boundary must preserve `A`, `B`, and `C` +and make + +``` +X_i' = X_i + A + B +Y_i' = Y_i + A + B + C +Z_i' = Z_i + A + C (i = 1, 2, 3). +``` + +The three target classes are independent. No source or target starts clean. +The source row `A` is an internal borrowed helper, and its exact restoration +is part of the output contract. + +## Construction and complete invoice + +Use `A` as the anchor and visit these masks of `(B,C)`: + +| Anchor contents | Operation | Fanout | +|---|---|---:| +| `A` | `A ^= B` | — | +| `A+B` | add `A` to each `X_i` | 3 | +| `A+B+C` | `A ^= C` | — | +| `A+B+C` | add `A` to each `Y_i` | 3 | +| `A+C` | `A ^= B` | — | +| `A+C` | add `A` to each `Z_i` | 3 | +| `A` | `A ^= C` | — | + +The anchor itinerary is `00 -> 10 -> 11 -> 01 -> 00`. Four charged source +transitions and nine charged target writes give **13 row ADDs**. At width +`L`, the bill is `13L` bit XORs, 13 source-row reads, and 13 destination-row +writes. + +The independent baseline applies the sources separately to each target: +six ADDs for the `X` rows, nine for the `Y` rows, and six for the `Z` rows, +for **21 row ADDs** (`21L` bit XORs, 21 reads and 21 writes). Thus this local +construction saves 8 ADDs, or 8L bit XORs. Preparation and final restoration +are both included. Neither circuit uses copies, a clean helper, an extra +recursive child, a frame change, or a precision operation. Both use the +same aligned row frame. Head movement and hosting are not resources in this +row-register model; no claim about a hosted supplier or the selected +recursive profile is made. + +Separately preparing and restoring each mask costs 17 ADDs: each target is +updated once, and the three independent anchor round trips cost 2, 4, and 2 +ADDs. Sharing transitions along the four-state Gray cycle reduces that +invoice to 13. Within the declared one-anchor schedule class, the four +transitions are minimal: the closed walk must visit all four vertices of the +two-dimensional mask square, and a four-edge cycle attains the lower bound. +This is not a global minimum claim over arbitrary CNOT circuits. + +## Relation to the selected bound and prior work + +The originating task is `bit-helper-contract`; its scope is changed from +the inherited R439 H2/K helper-star word to this exact borrowed-source +boundary. The replacement is local: a temporary helper write is permitted +only when the arbitrary source row is restored exactly and every target has +its specified boundary value. This package does not assert a new general +H2/K criterion for R439. + +Nearby work includes open PR [#2241](https://github.com/CrocSwap/integer-mult-bounds/pull/2241), +which shears one of two retained outputs to hold one fixed sum before fanout; +merged PR [#1968](https://github.com/CrocSwap/integer-mult-bounds/pull/1968), +which accumulates shared product terms before a two-wave dirty-output fanout; +and open PR [#2259](https://github.com/CrocSwap/integer-mult-bounds/pull/2259), +which fuses a four-source update into one aligned target stream. Open PR +[#2045](https://github.com/CrocSwap/integer-mult-bounds/pull/2045) and +[Discussion #2036](https://github.com/CrocSwap/integer-mult-bounds/discussions/2036) +use a newly allocated clean coded helper to send one three-source sum to two +outputs and restore it. Open PR [#1937](https://github.com/CrocSwap/integer-mult-bounds/pull/1937) +works inside the R439 helper-star donor interface. Earlier Discussion +[#1167 comment 18920388](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18920388) +prices a fixed four-source parity through one arbitrary dirty helper and +corrects helper contamination. Here one existing arbitrary source row walks +through three distinct parities; transition reuse across mask classes is the +mechanism under study. These comparisons are scope distinctions, not a +novelty certificate. + +The construction is an exact local XOR-network result. No source-word +occurrence, selected supplier admission, recursive billing, or `kappa` +improvement is established. Source and selected-record pins are in +[`SOURCES.json`](SOURCES.json); the changed task scope and claim are in +[`TASK.json`](TASK.json). + +## Reproduction + +```sh +python3 -I -B research/borrowed-source-gray-mask-fanout-seed9b2fe133/verify.py +python3 -I -O -B research/borrowed-source-gray-mask-fanout-seed9b2fe133/verify.py +python3 scripts/research_package.py --package research/borrowed-source-gray-mask-fanout-seed9b2fe133 --check-only +``` + +The replay checks the exact 12-row linear map, all `2^12` one-bit dirty +states, inverse execution, the 21-versus-13 invoice, the minimum four-edge +one-anchor tour, and four controls for a leaked anchor, a missing parity +transition, a missing target update, and a wrong return transition. + +## Open next questions + +1. **Find an actual caller.** Search one source-pinned bit word for three + target classes that need these shared parity masks at a common aligned + frame. Charge the actual source references, frame schedule, host and + recursive calls before claiming supplier relevance. +2. **More mask classes.** For a specified higher-dimensional source-mask + family, find the shortest closed Hamming tour through the required masks + and compare its charged transition count with independent mask preparation. + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. No +independent human review or proof-kernel verification is claimed. Apache-2.0. diff --git a/research/borrowed-source-gray-mask-fanout-seed9b2fe133/SOURCES.json b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/SOURCES.json new file mode 100644 index 0000000000..e862d2492c --- /dev/null +++ b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/SOURCES.json @@ -0,0 +1,148 @@ +{ + "schema_version": 1, + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "seed": "9b2fe13334259f250375373f4f2b3806", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "input", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "autoresearch.md", + "usage": "provenance", + "git_blob": "9b6cbfef0fb725f28c177038d32f482706e12c94", + "sha256": "79d0c8be61d90dd6c46b6e7250e0c88713d29854128d8d1361b6343682dad1d8" + }, + { + "path": "scripts/choose_research_task.py", + "usage": "provenance", + "git_blob": "695639622a283190948c4187bdbb41997e6e43d7", + "sha256": "f1af1e70858ab1d033ce20ee1968201bc592eb9e3fd05ab8ad78c842c0b028d1" + }, + { + "path": "scripts/research_package.py", + "usage": "provenance", + "git_blob": "6733ec2f5700e6602d60dc95938c1ea1854980f0", + "sha256": "b077068519d85bc04a7192d8bcd2fdbc1ce487ea2b7264ed7f437c439b0a16de" + } + ], + "predecessors": [ + { + "pr": 2241, + "head": "5688d8b17830dbb813fba5a509f52449383903fa", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2241", + "relation": "one fixed temporary sum anchor with two retained clean outputs" + }, + { + "pr": 1968, + "head": "f039d4df1d2fa094771977fbe3584a9ba1149e86", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1968", + "relation": "multiple shared product terms accumulated before dirty-output fanout" + }, + { + "pr": 2259, + "head": "2d3fda68576db8f80fbfebcb7322832bc08fd138", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2259", + "relation": "four-source aligned update of one target stream" + }, + { + "discussion_comment": "18920388", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18920388", + "relation": "fixed four-source parity through an arbitrary dirty helper, with helper contamination correction" + }, + { + "pr": 1937, + "head": "8b4a4d59eb5df9971d44587d9980c3dd0b18fc96", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1937", + "relation": "R439 multi-donor helper-star absorption under the pinned twisted helper interface" + }, + { + "pr": 2045, + "head": "4b3fb343f3336d43db71beaf356c8cd0f2be8e46", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2045", + "relation": "three-source clean coded helper cached to two outputs and restored" + }, + { + "discussion": "2036", + "discussion_comment": "18930988", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2036#discussioncomment-18930988", + "relation": "completed clean-cache claim corresponding to PR #2045" + } + ], + "overlap_refresh": { + "searched_at": "2026-10-15T02:58:55.672928Z", + "coverage": { + "open_prs": 494, + "discussions": 978, + "complete_pagination": true, + "warnings": [] + }, + "terms": [ + "borrowed anchor", + "mask tour", + "parity masks", + "multi-mask helper-star", + "helper contract" + ], + "related_matches": [ + { + "pr": 2241, + "head": "5688d8b17830dbb813fba5a509f52449383903fa" + }, + { + "pr": 1968, + "head": "f039d4df1d2fa094771977fbe3584a9ba1149e86" + }, + { + "pr": 2259, + "head": "2d3fda68576db8f80fbfebcb7322832bc08fd138" + }, + { + "pr": 1937, + "head": "8b4a4d59eb5df9971d44587d9980c3dd0b18fc96" + }, + { + "pr": 2045, + "head": "4b3fb343f3336d43db71beaf356c8cd0f2be8e46" + }, + { + "discussion": "2036", + "comment": "18930988" + }, + { + "discussion": "1167", + "comment": "18920388" + } + ], + "result": "Related fixed-mask, dirty-output-anchor, R439 helper-star, and clean-cache work found and pinned; no exact borrowed-source multi-mask Gray-tour match appeared. This is overlap evidence, not a novelty certificate." + } +} diff --git a/research/borrowed-source-gray-mask-fanout-seed9b2fe133/TASK.json b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/TASK.json new file mode 100644 index 0000000000..f06de2253b --- /dev/null +++ b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "seed": "9b2fe13334259f250375373f4f2b3806", + "track": "bit-mechanisms", + "task_id": "bit-helper-contract", + "selector_scope_key": "bfb61f829a81535adeae", + "priority_revision": 4, + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2270", + "claim_expiry_utc": "2026-10-15T04:55:00Z", + "scope_status": "changed", + "scope_change_reason": "The suggested R439 H2/K helper-star boundary has extensive predecessor and current overlap. This scope tests a different complete local boundary: one arbitrary source row is borrowed, reconfigured through three target parities, and restored after a closed Gray tour. It is not a general H2/K replacement theorem.", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "actual_scope": "For arbitrary binary rows A,B,C and three arbitrary targets in each of the AB, ABC, and AC parity classes, implement the exact target map with one borrowed source row following 00->10->11->01->00 and restoring its arbitrary boundary value.", + "bottleneck_link": "A proven row-add saving can reduce a bit mechanism only if a source-pinned supplier word contains these parity classes at one compatible frame; no such occurrence or selected-profile effect is known.", + "stop_rule": "Stop after exact transfer-matrix equality, exhaustive 2^12 one-bit arbitrary-dirty replay, four meaningful negative controls, the charged 21-versus-13 row-add profile, and the one-anchor tour bound. Do not claim a supplier or kappa result without a pinned caller.", + "evidence": "verify.py certifies the 12-row map and reverse schedule, checks all 4096 scalar input states, enumerates the six mask visitation orders, and rejects four boundary mutations. EXPECTED.json records the exact receipt; PROOF.md gives the identity and cost argument.", + "outcome": "completed", + "open_questions": [ + { + "question": "Does a source-pinned bit word contain these three parity classes at a common aligned frame?", + "why_it_matters": "An actual caller and its source, frame, and recursive costs determine whether the local eight-ADD saving can affect the conditional bound.", + "first_step": "Search one pinned bit-source interval for targets with common supports AB, ABC, and AC, then price each row reference and frame transition.", + "blocked_by": "No source-word occurrence is established in this package." + }, + { + "question": "How much can a borrowed source save for a specified larger family of parity masks?", + "why_it_matters": "The transition tour may amortize source preparation across many target classes.", + "first_step": "Fix a finite mask set and multiplicities, then minimize the closed Hamming walk and compare its full transition bill with independent preparation.", + "blocked_by": "The current exact result covers only the three masks in a two-dimensional square." + } + ], + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in scope selection, algebra, implementation, exact replay, and writing; no subagents or independent human review.", + "hub_pointer_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18939243", + "overlap_update_hub_pointer": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18939320", + "related_predecessors": [ + { + "pr": 2241, + "head": "5688d8b17830dbb813fba5a509f52449383903fa" + }, + { + "pr": 1968, + "head": "f039d4df1d2fa094771977fbe3584a9ba1149e86" + }, + { + "pr": 2259, + "head": "2d3fda68576db8f80fbfebcb7322832bc08fd138" + }, + { + "pr": 1937, + "head": "8b4a4d59eb5df9971d44587d9980c3dd0b18fc96" + }, + { + "pr": 2045, + "head": "4b3fb343f3336d43db71beaf356c8cd0f2be8e46" + }, + { + "discussion": "2036", + "comment": "18930988" + }, + { + "discussion": "1167", + "comment": "18920388" + } + ] +} diff --git a/research/borrowed-source-gray-mask-fanout-seed9b2fe133/VERIFY.json b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/VERIFY.json new file mode 100644 index 0000000000..955df0d262 --- /dev/null +++ b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact transfer matrix, 4096 arbitrary dirty inputs, inverse, operation invoice, mask tour, and four negative controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Repeat exact construction and controls with optimized Python to ensure assertions are not required for hidden side effects." + } + ], + "inputs": [ + "research/borrowed-source-gray-mask-fanout-seed9b2fe133/README.md", + "research/borrowed-source-gray-mask-fanout-seed9b2fe133/PROOF.md", + "research/borrowed-source-gray-mask-fanout-seed9b2fe133/EXPECTED.json", + "research/borrowed-source-gray-mask-fanout-seed9b2fe133/verify.py", + "research/borrowed-source-gray-mask-fanout-seed9b2fe133/TASK.json", + "research/borrowed-source-gray-mask-fanout-seed9b2fe133/SOURCES.json", + "research/borrowed-source-gray-mask-fanout-seed9b2fe133/VERIFY.json", + "docs/research/agent-task-catalog.json", + "certificates/selected-result.json" + ] +} diff --git a/research/borrowed-source-gray-mask-fanout-seed9b2fe133/verify.py b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/verify.py new file mode 100644 index 0000000000..be2b4e48f9 --- /dev/null +++ b/research/borrowed-source-gray-mask-fanout-seed9b2fe133/verify.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +"""Exact dirty-boundary replay for the borrowed-source Gray-mask circuit.""" +import json +from itertools import permutations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +EXPECTED = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8")) + + +def candidate_schedule(): + ops = [(1, 0)] # A <- A+B + ops += [(0, 3 + i) for i in range(3)] # X_i <- X_i+A + ops += [(2, 0)] # A <- A+B+C + ops += [(0, 6 + i) for i in range(3)] # Y_i <- Y_i+A + ops += [(1, 0)] # A <- A+C + ops += [(0, 9 + i) for i in range(3)] # Z_i <- Z_i+A + ops += [(2, 0)] # restore A + return ops + + +def direct_schedule(): + ops = [] + for destination_start, sources in ( + (3, (0, 1)), + (6, (0, 1, 2)), + (9, (0, 2)), + ): + for i in range(3): + ops.extend((source, destination_start + i) for source in sources) + return ops + + +def apply(values, ops): + out = list(values) + for source, destination in ops: + out[destination] ^= out[source] + return tuple(out) + + +def transfer_rows(ops): + rows = [1 << i for i in range(12)] + for source, destination in ops: + rows[destination] ^= rows[source] + return tuple(rows) + + +def expected_rows(): + rows = [1 << i for i in range(12)] + for i in range(3): + rows[3 + i] ^= rows[0] ^ rows[1] + rows[6 + i] ^= rows[0] ^ rows[1] ^ rows[2] + rows[9 + i] ^= rows[0] ^ rows[2] + return tuple(rows) + + +def expected_state(values): + a, b, c = values[:3] + out = list(values) + for i in range(3): + out[3 + i] ^= a ^ b + out[6 + i] ^= a ^ b ^ c + out[9 + i] ^= a ^ c + return tuple(out) + + +def tour_length(order): + state = 0 + length = 0 + for next_state in order: + length += (state ^ next_state).bit_count() + state = next_state + length += state.bit_count() + return length + + +def control_fails(ops): + return transfer_rows(ops) != expected_rows() + + +def main(): + candidate = candidate_schedule() + direct = direct_schedule() + target = expected_rows() + + assert len(candidate) == 13 + assert len(direct) == 21 + assert transfer_rows(candidate) == target + assert transfer_rows(direct) == target + + # The anchor walks through the three required nonempty masks in Gray order. + masks = (1, 3, 2) + tour_costs = [tour_length(order) for order in permutations(masks)] + assert min(tour_costs) == 4 + assert tour_length(masks) == 4 + + # Exhaust every arbitrary dirty one-bit input to all 12 rows. + for word in range(1 << 12): + initial = tuple((word >> i) & 1 for i in range(12)) + got = apply(initial, candidate) + assert got == expected_state(initial) + assert apply(got, reversed(candidate)) == initial + assert apply(initial, direct) == got + + # Failure controls: source leakage, wrong parity transition, missing fanout, + # and an incorrect restoration source. + controls = [] + controls.append(candidate[:-1]) + controls.append(candidate[:4] + candidate[5:]) + controls.append(candidate[:10] + candidate[11:]) + controls.append(candidate[:-1] + [(1, 0)]) + assert all(control_fails(control) for control in controls) + + assert len(controls) == EXPECTED["negative_controls"] + assert len(candidate) == EXPECTED["borrowed_adds"] + assert len(direct) == EXPECTED["direct_adds"] + assert EXPECTED["direct_adds"] - EXPECTED["borrowed_adds"] == EXPECTED["saving_adds"] + assert EXPECTED["anchor_transition_adds"] + EXPECTED["target_write_adds"] == len(candidate) + assert (1 << 12) == EXPECTED["scalar_boundary_states"] + + print( + "PASS_GRAY_MASK_FANOUT width=1 source_rows=3 target_classes=3 targets_per_class=3 " + "direct_adds=21 borrowed_adds=13 transitions=4 target_writes=9 saving=8 " + "scalar_states=4096 min_tour=4 controls=4" + ) + + +if __name__ == "__main__": + main()