From c2527419aa030fb71985d99f99e915d192e388bd Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 02:27:04 -0500 Subject: [PATCH] Research: bound generator-priced affine target sharing --- .../CERTIFICATE.json | 120 +++++ .../bit-affine-generator-sharing/README.md | 125 +++++ .../bit-affine-generator-sharing/SOURCES.json | 30 ++ .../bit-affine-generator-sharing/TASK.json | 101 ++++ .../bit-affine-generator-sharing/VERIFY.json | 32 ++ .../independent.py | 271 ++++++++++ .../bit-affine-generator-sharing/verify.py | 485 ++++++++++++++++++ 7 files changed, 1164 insertions(+) create mode 100644 research/bit-affine-generator-sharing/CERTIFICATE.json create mode 100644 research/bit-affine-generator-sharing/README.md create mode 100644 research/bit-affine-generator-sharing/SOURCES.json create mode 100644 research/bit-affine-generator-sharing/TASK.json create mode 100644 research/bit-affine-generator-sharing/VERIFY.json create mode 100644 research/bit-affine-generator-sharing/independent.py create mode 100644 research/bit-affine-generator-sharing/verify.py diff --git a/research/bit-affine-generator-sharing/CERTIFICATE.json b/research/bit-affine-generator-sharing/CERTIFICATE.json new file mode 100644 index 0000000000..1074dbf037 --- /dev/null +++ b/research/bit-affine-generator-sharing/CERTIFICATE.json @@ -0,0 +1,120 @@ +{ + "conclusion": "both fixed two-register endpoints require 8 calls", + "controls": { + "all_24_formal_group_elements_enumerated": true, + "all_24_paid_factors_included": true, + "all_6_rank_one_idempotents_enumerated": true, + "changed_affine_target_mutation_rejected": true, + "direct_formal_endpoint_passes": true, + "inverse_target_pair_verified": true, + "omitted_call_mutations_rejected": true, + "two_endpoints_share_identical_complete_state_balls": true + }, + "direct_controls": { + "all_8_single_call_omissions_rejected": true, + "changed_target_and_target_order_rejected": true, + "inverse_pair_word": [ + "a:N=1000", + "b:N=1000", + "a:N=1000", + "v:N=1000", + "a:N=0001", + "b:N=0001", + "a:N=0001", + "u:N=0001" + ], + "same_target_word": [ + "a:N=1000", + "b:N=1000", + "a:N=1000", + "v:N=1000", + "a:N=0001", + "b:N=0001", + "a:N=0001", + "v:N=0001" + ] + }, + "first_endpoint": { + "direct_calls_total": 8, + "direct_word_per_target": "abav", + "formal_endpoint": "diag([h],[h])", + "map_per_target": "h(x0,x1)=(x1,x0+1)", + "minimum": 8, + "rank_floor": 4, + "search": { + "endpoint_reachable_within_7": false, + "left_radius": 3, + "left_state_sha256": "a0dade172de4088b86500e54ae8cc2389b447719fe7f250c2503151262633793", + "left_states": 6457, + "left_states_examined": 6457, + "minimum_word_length_found": null, + "right_radius": 4, + "right_state_sha256": "7ff93fe51d26c756210384dc31e97472f405853e00dc90413448f7f5a3c22bbe", + "right_states": 90859 + }, + "short_witness": null + }, + "model": { + "address_group": "AGL_2(F_2)", + "calls_per_label_per_idempotent": 1, + "factor": "D_N(g)=I+([g]+[1])N", + "formal_ring": "F_2[AGL_2(F_2)]", + "free_scalar_mixing": "GL_2(F_2), normalized into the six paid idempotents by augmentation", + "paid_factor_count": 24, + "paid_labels": { + "a": { + "matrix_row_major": "1011", + "translation": "00" + }, + "b": { + "matrix_row_major": "1101", + "translation": "00" + }, + "u": { + "matrix_row_major": "1001", + "translation": "01" + }, + "v": { + "matrix_row_major": "1001", + "translation": "10" + } + }, + "rank_one_idempotents": [ + "0001", + "0011", + "0101", + "1000", + "1010", + "1100" + ], + "registers": 2, + "workspace": "none" + }, + "pivot_endpoint": { + "direct_calls_total": 8, + "direct_words": [ + "abav", + "abau" + ], + "formal_endpoint": "diag([h],[h_inverse])", + "maps": [ + "h(x0,x1)=(x1,x0+1)", + "h_inverse(x0,x1)=(x1+1,x0)" + ], + "minimum": 8, + "rank_floor": 4, + "search": { + "endpoint_reachable_within_7": false, + "left_radius": 3, + "left_state_sha256": "a0dade172de4088b86500e54ae8cc2389b447719fe7f250c2503151262633793", + "left_states": 6457, + "left_states_examined": 6457, + "minimum_word_length_found": null, + "right_radius": 4, + "right_state_sha256": "7ff93fe51d26c756210384dc31e97472f405853e00dc90413448f7f5a3c22bbe", + "right_states": 90859 + }, + "short_witness": null + }, + "schema_version": 1 +} diff --git a/research/bit-affine-generator-sharing/README.md b/research/bit-affine-generator-sharing/README.md new file mode 100644 index 0000000000..260cbfc195 --- /dev/null +++ b/research/bit-affine-generator-sharing/README.md @@ -0,0 +1,125 @@ +# Generator-priced affine target sharing + +**Scoped negative result; no new \(\kappa\).** In the formal +\(\mathbb F_2[\mathrm{AGL}_2(\mathbb F_2)]\) model with two target registers, +four paid address generators, and all six rank-one scalar idempotents, both +\[ +\operatorname{diag}([h],[h]) +\quad\text{and}\quad +\operatorname{diag}([h],[h^{-1}]), +\qquad h(x_0,x_1)=(x_1,x_0+1), +\] +have exact minimum cost **8 calls**. The direct words use four calls per +target. A complete formal radius-seven search finds no saving, even though the +general homogeneous displacement-rank floor is only four calls. + +This tests a new cost rule: only the two coordinate shears and two coordinate +translations have unit price. PR #1333 prices every rank-one affine address +map at one call and proves the general displacement-rank floor. Its stated +generator-priced follow-up leaves room for a sharing gain; these two exact +endpoints do not realize it. The result is limited to two registers and the +two displayed target profiles. + +## Exact model and complete cost + +Work in the noncommutative group algebra +\(\mathbb F_2[G]\), \(G=\mathrm{AGL}_2(\mathbb F_2)\). The paid labels are +\[ +a(x_0,x_1)=(x_0+x_1,x_1),\quad +b(x_0,x_1)=(x_0,x_1+x_0),\quad +u(x_0,x_1)=(x_0+1,x_1),\quad +v(x_0,x_1)=(x_0,x_1+1). +\] +Each costs one. A call chooses any of the six rank-one idempotents +\(N\in M_2(\mathbb F_2)\) and applies +\[ +D_N(g)=I+([g]+[1])N. +\] +Free scalar \(GL_2(\mathbb F_2)\) mixing is retained as the inherited +optimistic relaxation. Moving it through the paid factors conjugates each +idempotent; augmentation \([g]\mapsto1\) forces the net scalar map to be the +identity, so enumerating all six idempotents covers interleaved free mixing. +Address labels outside \(\{a,b,u,v\}\) are forbidden. + +The target \(h\) has a shortest address word *abav*, length four, and +\(\operatorname{rank}_{\mathbb F_2}[A_h-I\mid b_h]=2\). Its inverse +\(h^{-1}(x_0,x_1)=(x_1+1,x_0)\) has shortest word *abau* and the same rank. +Thus each endpoint has direct cost 8 and the general displacement-rank floor +4. The mechanism had at most four calls of optimistic headroom. There is no +helper register or copied information; both arbitrary-input target registers +are represented in the exact endpoint. Each address call is charged once. +Physical/compiler realization, recursive supplier costs, precision, hosting, +and admission into the selected bit construction are outside this local model. + +The selected conditional record remains **complex-binding** according to +scripts/research_baseline.py. Consequently even a local bit saving would not +by itself change its \(\kappa\); this result claims no supplier-wide saving. + +## Exact search and controls + +Each paid factor is a formal involution because every allowed address label +satisfies \(g^2=1\) and every \(N\) satisfies \(N^2=N\). For a word of at most +seven calls, split its factor sequence after at most three calls. The verifier +enumerates exact states in the radius-three and radius-four balls. If \(P\) is +the prefix and \(T=QP\) the endpoint, then the required suffix is +\(Q=TP^{-1}\). Every state is the full \(2\times2\) matrix of 24 formal +coefficients; no finite address representation is used for acceptance. + +The two independent implementations agree on 6,457 radius-three states and +90,859 radius-four states, with their canonical state digests in +CERTIFICATE.json. The first uses packed row-major \(AGL_2\) matrices and a +rank-one update. The second enumerates all 24 permutations of the four address +points and multiplies the two formal coefficients of each factor directly. +Neither finds a word of length at most seven for either endpoint. The direct +eight-call words replay coefficient by coefficient, so the minima are exactly +eight in both stated cases. + +The replay also verifies all 24 paid factors, all 24 formal group elements, +all six idempotents, factor involution, both direct words, rejection of every +single-call deletion from each direct word, and a changed-target/order +mutation. These checks establish the finite algebraic result only. + +## Reproduce + +From the repository root: + + python3 -I -B research/bit-affine-generator-sharing/verify.py + python3 -I -B research/bit-affine-generator-sharing/independent.py + python3 scripts/research_package.py --package research/bit-affine-generator-sharing + +The first two commands should print PASS_BIT_AFFINE_GENERATOR_SHARING and +PASS_BIT_AFFINE_GENERATOR_SHARING_INDEPENDENT. TASK.json records seed, base, +changed scope, exact cost model, stopping rule, and next question. SOURCES.json +pins the retained AGL predecessor review/proof. No predecessor implementation +is imported. + +## Overlap and attribution + +Gareth Davidson (@bitplane), PR #1333, supplies the broader AGL group model, +the displacement-rank floor, and the generator-priced next question. Related +coordinate-CNOT-only linear targets are recorded in TASK.json. Two nearby +Discussion #1317 claims use three registers: comment 18918042 studies +\(\operatorname{diag}([a],[b],[aba])\) with only the two CNOT labels, while +comment 18918291 studies \(\operatorname{diag}([a],[b],[h])\) with labels +\(a,b,t_x\). The latter shares the map \(h\), but changes both the target tuple +and the address alphabet. This package prices \(a,b,t_x,t_y\) and gives exact +two-register minima for \(\operatorname{diag}([h],[h])\) and +\(\operatorname{diag}([h],[h^{-1}])\). Open PR #1696 submits a scoped exact +five-call result for the three-register CNOT-only target +\(\operatorname{diag}([a],[b],[aba])\); this package adds the two affine +two-target profiles under the four-label alphabet. A separate current claim, +Discussion #1700, studies rational rank-one frames with two independent +address relations; its group and cost premise differ. No selected-result or +physical-supplier change is claimed. + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. There has +been no independent human review. New work is Apache-2.0; predecessor files +remain unchanged. + +## Open next questions + +Could a third target register or another explicitly priced affine target family +permit sharing? First choose one three-target endpoint, compute its direct +generator lengths and displacement-rank floor, and stop if the fully charged +optimistic gap is zero. This package does not cover larger target tuples, +workspace, or a physical/compiler admission. diff --git a/research/bit-affine-generator-sharing/SOURCES.json b/research/bit-affine-generator-sharing/SOURCES.json new file mode 100644 index 0000000000..0fab3e70bd --- /dev/null +++ b/research/bit-affine-generator-sharing/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/binary-affine-register-bound/PROOF.md", + "usage": "input", + "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83", + "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b" + }, + { + "path": "research/binary-affine-register-bound/README.md", + "usage": "input", + "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c", + "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a" + } + ] +} diff --git a/research/bit-affine-generator-sharing/TASK.json b/research/bit-affine-generator-sharing/TASK.json new file mode 100644 index 0000000000..9518119cf3 --- /dev/null +++ b/research/bit-affine-generator-sharing/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "session_seed": "f024daf023fbb77c64b7b0501cb0db7e", + "track": "bit-mechanisms", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18918046", + "finding_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18918154", + "claim_expires_utc": "2026-10-14T09:20:00Z", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum-call results for two fixed two-register endpoints in formal F2[AGL_2(F2)], where only the two coordinate shears and two coordinate translations are unit-price address labels: diag([h],[h]) and diag([h],[h_inverse]), with h(x0,x1)=(x1,x0+1).", + "scope_change_reason": "PR1333 already proves the all-register displacement-rank floor when every rank-one affine address map costs one call. This task instead charges only four elementary affine generators and asks whether their longer direct words permit register sharing. The helper-contract suggestion overlaps the R439 helper-star lineage and PR1194/PR1306. The first identical-target search found no saving, so one bounded pivot changed the endpoint to an inverse affine pair to test inter-target cancellation.", + "bottleneck_link": "A real saving in a paid bit-call alphabet could lower a bit-circuit profile. The selected conditional record remains complex-binding, and this abstract result supplies no physical bit supplier or kappa change.", + "budget_minutes": 60, + "stop_rule": "Complete the exact radius-seven 3+4 join for the identical and inverse-pair endpoints, compare an independent permutation-group coefficient engine, and stop without enlarging the target/register domain.", + "outcome": "negative-result", + "evidence": "CERTIFICATE.json records the two radius-seven outcomes and canonical state hashes; verify.py and independent.py agree on both formal searches, the 6457/90859 state-ball counts, and the direct eight-call controls.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in scoping, implementation, verification and writing; no independent human review claimed.", + "open_questions": [ + { + "question": "Can a third target register or a different affine target family enable sharing in this four-generator alphabet?", + "why_it_matters": "The two fixed two-register profiles have no saving, but the exact search does not bound larger target tuples or workspace.", + "first_step": "Choose one explicit three-target AGL2 endpoint, compute every direct generator length and displacement-rank floor, then test whether the optimistic budget leaves room for a strict saving.", + "blocked_by": "This package does not enumerate larger register dimensions and does not give a physical/compiler admission for the affine address alphabet." + } + ], + "predecessors": [ + "PR1333: broad AGL displacement-rank theorem and generator-priced follow-up question", + "PR1414, PR1491, PR1495, PR1496, PR1567: related coordinate-CNOT linear target scopes, not this translation-bearing AGL2 alphabet" + ], + "predecessor_heads": { + "PR1333": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "PR1414": "9e1640094f649ba6db9742796825a8d6c238989b", + "PR1496": "0b1420fcc47e2137c5f0a5b9aa347cd001fff9cd" + }, + "concurrent_scope": "Discussion 1317 comments 18918042 and 18918291 claim three-register heterogeneous endpoints. Comment 18918291 uses the same affine target h once, but only labels a,b,t_x and the endpoint diag([a],[b],[h]); this package prices a,b,t_x,t_y and gives exact minima for the two-register endpoints diag([h],[h]) and diag([h],[h_inverse]). Discussion 1700 claims a four-register rational two-relation model, a different address group and cost premise.", + "overlap_snapshot": { + "observed_utc": "2026-10-14T07:30:58Z", + "pull_requests": { + "complete_pagination": true, + "open_count": 398, + "relevant_heads": { + "PR1696": "4dadd2745da777f166c842c19a497791b0ec755c", + "PR1690": "dfd15686309d26eb98740942c4e84cddeafae7d8", + "PR1680": "a281330e84e64ad357e35b338796c96144a345ce", + "PR1662": "01cc02b164ecc4f9d84df3f56a1fe65b88daf390", + "PR1496": "0b1420fcc47e2137c5f0a5b9aa347cd001fff9cd", + "PR1705": "ad6b7d641b3e8576a95add7981fa75b6a8278fbc" + }, + "closest": "PR1696 proves an exact five-call minimum for diag([a],[b],[aba]) on three registers over GL2(F2) with only two CNOT labels. It is a related but different endpoint, register count, and alphabet.", + "other_nearby": "PR1705 studies four repeated linear coordinate-SWAP targets at four registers; it has no translation-bearing affine endpoint or generator-priced four-label alphabet." + }, + "discussions": { + "complete_top_level_pagination": true, + "top_level_count": 118, + "relevant_thread": "Discussion 1317, all 11 comments inspected", + "other_active_model": "Discussion 1700 is a four-register rational two-relation scope." + }, + "limits": "The repository overlap helper could not refresh PR data because installed gh rejects --slurp. Direct complete REST pagination was used for all 398 open PR bodies; the current Discussion 1317 thread was fully read at updatedAt 2026-10-14T07:24:28Z, including the neighboring three-register affine claim. A subsequent all-discussions GraphQL refresh hit the GitHub GraphQL rate limit. This is an overlap check, not a novelty certificate." + } +} diff --git a/research/bit-affine-generator-sharing/VERIFY.json b/research/bit-affine-generator-sharing/VERIFY.json new file mode 100644 index 0000000000..be84d50031 --- /dev/null +++ b/research/bit-affine-generator-sharing/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/binary-affine-register-bound/PROOF.md", + "research/binary-affine-register-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rebuild the full formal AGL2 radius-three/four state balls, exact-join both endpoints, verify the direct eight-call controls and certificate digests." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independently enumerate AGL2 as the permutations of four points, multiply factor coefficients generically, and compare both endpoint joins and canonical state hashes." + } + ] +} diff --git a/research/bit-affine-generator-sharing/independent.py b/research/bit-affine-generator-sharing/independent.py new file mode 100644 index 0000000000..2ca0f23da0 --- /dev/null +++ b/research/bit-affine-generator-sharing/independent.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +"""Independent formal-word replay using the four-point permutation model.""" + +from __future__ import annotations + +import hashlib +import itertools +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +POINTS = tuple(range(4)) +PERMUTATIONS = tuple(itertools.permutations(POINTS)) +PERM_ID = {p: i for i, p in enumerate(PERMUTATIONS)} +GROUP_PRODUCT = tuple( + tuple(PERM_ID[tuple(g[h[x]] for x in POINTS)] for h in PERMUTATIONS) + for g in PERMUTATIONS +) +IDENTITY = PERM_ID[POINTS] + + +def affine_permutation(a: int, b: int) -> tuple[int, ...]: + images = [] + for x in POINTS: + x0, x1 = x & 1, (x >> 1) & 1 + y0 = (((a >> 0) & 1) & x0) ^ (((a >> 1) & 1) & x1) ^ (b & 1) + y1 = (((a >> 2) & 1) & x0) ^ (((a >> 3) & 1) & x1) ^ ((b >> 1) & 1) + images.append(y0 | (y1 << 1)) + return tuple(images) + + +def packed_affine(permutation: tuple[int, ...]) -> tuple[int, int]: + translation = permutation[0] + col0 = permutation[1] ^ translation + col1 = permutation[2] ^ translation + matrix = ( + (col0 & 1) + | ((col1 & 1) << 1) + | (((col0 >> 1) & 1) << 2) + | (((col1 >> 1) & 1) << 3) + ) + return matrix, translation + + +PRIMARY_GROUP_IDS = { + (0b1011, 0): "a", + (0b1101, 0): "b", + (0b1001, 0b01): "u", + (0b1001, 0b10): "v", +} +LABELS = ("a", "b", "u", "v") +LABEL_PERMS = { + label: affine_permutation(*pair) for pair, label in PRIMARY_GROUP_IDS.items() +} +LABEL_IDS = {label: PERM_ID[permutation] for label, permutation in LABEL_PERMS.items()} +TARGET_PERM = affine_permutation(0b0110, 0b10) +INVERSE_PERM = affine_permutation(0b0110, 0b01) +TARGET_ID = PERM_ID[TARGET_PERM] +INVERSE_ID = PERM_ID[INVERSE_PERM] + + +def multiply_2x2(a: int, b: int) -> int: + out = 0 + for i in range(2): + for j in range(2): + x = 0 + for k in range(2): + x ^= ((a >> (2 * i + k)) & 1) & ((b >> (2 * k + j)) & 1) + out |= x << (2 * i + j) + return out + + +def rank_2x2(a: int) -> int: + cols = ((a & 1) | (((a >> 2) & 1) << 1), ((a >> 1) & 1) | (((a >> 3) & 1) << 1)) + return int(cols[0] != 0) + int(cols[1] != 0 and cols[1] != cols[0]) + + +def idempotents() -> tuple[int, ...]: + values = set() + for u in (1, 2, 3): + for v in (1, 2, 3): + if ((u & v).bit_count() & 1) == 1: + n = 0 + for i in range(2): + for j in range(2): + n |= (((u >> i) & 1) & ((v >> j) & 1)) << (2 * i + j) + values.add(n) + result = tuple(sorted(values)) + if len(result) != 6: + raise AssertionError("outer-product enumeration did not give six idempotents") + return result + + +IDEMPOTENTS = idempotents() +FACTORS = tuple((label, LABEL_IDS[label], n) for label in LABELS for n in IDEMPOTENTS) +FACTOR_IDS = {(label, n): i for i, (label, _, n) in enumerate(FACTORS)} +IDENTITY_STATE = (1 << IDENTITY, 0, 0, 1 << IDENTITY) + + +def shift_poly(poly: int, gid: int) -> int: + """Left-convolve by one group element using explicit permutation products.""" + result = 0 + remaining = poly + while remaining: + bit = remaining & -remaining + source = bit.bit_length() - 1 + result ^= 1 << GROUP_PRODUCT[gid][source] + remaining ^= bit + return result + + +def left_factor(state: tuple[int, int, int, int], fid: int) -> tuple[int, int, int, int]: + """Generic 2x2 matrix product using the two formal coefficients of D_N(g).""" + _, gid, n = FACTORS[fid] + at_identity = 0b1001 ^ n + out = [] + for i in range(2): + for j in range(2): + value = 0 + for k in range(2): + entry = 1 << (2 * i + k) + if at_identity & entry: + value ^= state[2 * k + j] + if n & entry: + value ^= shift_poly(state[2 * k + j], gid) + out.append(value) + return tuple(out) # type: ignore[return-value] + + +def replay(word: bytes) -> tuple[int, int, int, int]: + state = IDENTITY_STATE + for fid in word: + state = left_factor(state, fid) + return state + + +def word_for(labels: bytes, n: int) -> bytes: + return bytes(FACTOR_IDS[(chr(label), n)] for label in labels) + + +def radius_ball(radius: int) -> dict[tuple[int, int, int, int], bytes]: + states = {IDENTITY_STATE: b""} + frontier = [IDENTITY_STATE] + for _ in range(radius): + following = [] + for state in frontier: + for fid in range(len(FACTORS)): + nxt = left_factor(state, fid) + if nxt not in states: + states[nxt] = states[state] + bytes((fid,)) + following.append(nxt) + frontier = following + return states + + +def canonical_digest(states: dict[tuple[int, int, int, int], bytes]) -> str: + # The primary certificate indexes the same formal group by packed (A,b). + permutation_to_primary = {} + for gid, permutation in enumerate(PERMUTATIONS): + pair = packed_affine(permutation) + if rank_2x2(pair[0]) != 2 or pair[1] not in range(4): + raise AssertionError("a four-point permutation was not affine") + permutation_to_primary[gid] = pair + if len(set(permutation_to_primary.values())) != 24: + raise AssertionError("the permutation-to-affine map is not bijective") + # AGL_2(F_2) has 24 affine maps, so this verifies the faithful S4 model. + # Reconstruct the primary enumeration order without importing its verifier. + primary_pairs = [] + for a in range(16): + if rank_2x2(a) != 2: + continue + for b in range(4): + primary_pairs.append((a, b)) + primary_index = {pair: i for i, pair in enumerate(primary_pairs)} + permutation_to_primary_index = { + gid: primary_index[pair] for gid, pair in permutation_to_primary.items() + } + digest = hashlib.sha256() + for state in sorted(states, key=lambda s: tuple(remap_poly(p, permutation_to_primary_index) for p in s)): + mapped = tuple(remap_poly(p, permutation_to_primary_index) for p in state) + digest.update(" ".join(f"{x:06x}" for x in mapped).encode("ascii")) + digest.update(b"\n") + return digest.hexdigest() + + +def remap_poly(poly: int, group_map: dict[int, int]) -> int: + result = 0 + while poly: + bit = poly & -poly + source = bit.bit_length() - 1 + result |= 1 << group_map[source] + poly ^= bit + return result + + +def left_target(state: tuple[int, int, int, int], targets: tuple[int, int]) -> tuple[int, int, int, int]: + return tuple( + shift_poly(state[2 * i + j], targets[i]) + for i in range(2) + for j in range(2) + ) # type: ignore[return-value] + + +def target_state(targets: tuple[int, int]) -> tuple[int, int, int, int]: + return (1 << targets[0], 0, 0, 1 << targets[1]) + + +def exact_join( + targets: tuple[int, int], + left: dict[tuple[int, int, int, int], bytes], + right: dict[tuple[int, int, int, int], bytes], +) -> bytes | None: + best = None + for state, prefix in left.items(): + inverse = replay(prefix[::-1]) + suffix = right.get(left_target(inverse, targets)) + if suffix is not None: + candidate = prefix + suffix + if best is None or (len(candidate), candidate) < (len(best), best): + best = candidate + return best + + +def main() -> None: + cert = json.loads((ROOT / "CERTIFICATE.json").read_text()) + if len(PERMUTATIONS) != 24 or len(LABEL_IDS) != 4 or len(FACTORS) != 24: + raise AssertionError("independent permutation model is incomplete") + if len(set(LABEL_PERMS.values())) != 4: + raise AssertionError("generator labels are not distinct") + if rank_2x2(0b1011) != 2 or rank_2x2(0b1101) != 2: + raise AssertionError("elementary shear matrices were not invertible") + + direct_same = word_for(b"abav", 0b0001) + word_for(b"abav", 0b1000) + direct_inverse = word_for(b"abav", 0b0001) + word_for(b"abau", 0b1000) + same_state = target_state((TARGET_ID, TARGET_ID)) + inverse_state = target_state((TARGET_ID, INVERSE_ID)) + if replay(direct_same) != same_state or replay(direct_inverse) != inverse_state: + raise AssertionError("generic coefficient multiplication rejected a direct word") + for factor_id in range(len(FACTORS)): + if replay(bytes((factor_id, factor_id))) != IDENTITY_STATE: + raise AssertionError("generic factor multiplication found a non-involution") + + left = radius_ball(3) + right = radius_ball(4) + primary_same = cert["first_endpoint"]["search"] + primary_inverse = cert["pivot_endpoint"]["search"] + if len(left) != primary_same["left_states"] or len(right) != primary_same["right_states"]: + raise AssertionError("independent ball cardinalities disagree") + if canonical_digest(left) != primary_same["left_state_sha256"]: + raise AssertionError("independent radius-three formal states disagree") + if canonical_digest(right) != primary_same["right_state_sha256"]: + raise AssertionError("independent radius-four formal states disagree") + same = exact_join((TARGET_ID, TARGET_ID), left, right) + inverse = exact_join((TARGET_ID, INVERSE_ID), left, right) + if (same is None) != (primary_same["minimum_word_length_found"] is None): + raise AssertionError("independent identical-target join disagrees") + if (inverse is None) != (primary_inverse["minimum_word_length_found"] is None): + raise AssertionError("independent inverse-pair join disagrees") + for word, endpoint in ((same, same_state), (inverse, inverse_state)): + if word is not None and replay(word) != endpoint: + raise AssertionError("independent search returned a false witness") + print("PASS_BIT_AFFINE_GENERATOR_SHARING_INDEPENDENT") + print( + f"permutation_group={len(PERMUTATIONS)} factors={len(FACTORS)} " + f"radius_states={len(left)}/{len(right)} same={None if same is None else len(same)} " + f"inverse_pair={None if inverse is None else len(inverse)}" + ) + + +if __name__ == "__main__": + main() diff --git a/research/bit-affine-generator-sharing/verify.py b/research/bit-affine-generator-sharing/verify.py new file mode 100644 index 0000000000..a777e81936 --- /dev/null +++ b/research/bit-affine-generator-sharing/verify.py @@ -0,0 +1,485 @@ +#!/usr/bin/env python3 +"""Exact radius-seven search in F2[AGL_2(F2)] for two affine targets.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +from collections import deque +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +ID_MATRIX = 0b1001 +IDENTITY_AFFINE = (ID_MATRIX, 0) +GENERATORS = { + "a": (0b1011, 0), # x0 <- x0 + x1 + "b": (0b1101, 0), # x1 <- x1 + x0 + "u": (ID_MATRIX, 0b01), # x0 <- x0 + 1 + "v": (ID_MATRIX, 0b10), # x1 <- x1 + 1 +} +TARGET = (0b0110, 0b10) # h(x0,x1) = (x1, x0+1) +MUTATED_TARGET = (0b0110, 0b01) # h'(x0,x1) = (x1+1, x0) +DIRECT_LABELS = b"abav" +DIRECT_MUTATED_LABELS = b"abau" + + +def matrix_product(a: int, b: int) -> int: + """Multiply packed row-major 2x2 matrices over F2.""" + out = 0 + for i in range(2): + for j in range(2): + value = 0 + for k in range(2): + value ^= ((a >> (2 * i + k)) & 1) & ((b >> (2 * k + j)) & 1) + out |= value << (2 * i + j) + return out + + +def matrix_rank(a: int) -> int: + rows = [a & 0b11, (a >> 2) & 0b11] + rank = 0 + for col in (1, 0): + pivot = next((r for r in range(rank, 2) if (rows[r] >> col) & 1), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for r in range(2): + if r != rank and ((rows[r] >> col) & 1): + rows[r] ^= rows[rank] + rank += 1 + return rank + + +def compose(g: tuple[int, int], h: tuple[int, int]) -> tuple[int, int]: + """Return g after h for affine maps x -> A*x+b.""" + ag, bg = g + ah, bh = h + a = matrix_product(ag, ah) + b = 0 + for i in range(2): + value = (bg >> i) & 1 + for j in range(2): + value ^= ((ag >> (2 * i + j)) & 1) & ((bh >> j) & 1) + b |= value << i + return a, b + + +def affine_elements() -> tuple[tuple[int, int], ...]: + return tuple( + (a, b) + for a in range(16) + if matrix_rank(a) == 2 + for b in range(4) + ) + + +GROUP = affine_elements() +GROUP_ID = {g: i for i, g in enumerate(GROUP)} +GROUP_PRODUCT = tuple( + tuple(GROUP_ID[compose(g, h)] for h in GROUP) for g in GROUP +) +UNIT = GROUP_ID[IDENTITY_AFFINE] +TARGET_ID = GROUP_ID[TARGET] +MUTATED_TARGET_ID = GROUP_ID[MUTATED_TARGET] + + +def idempotents() -> tuple[int, ...]: + found = [] + for n in range(16): + if n and matrix_rank(n) == 1 and matrix_product(n, n) == n: + found.append(n) + return tuple(found) + + +IDEMPOTENTS = idempotents() +FACTORS = tuple( + (label, GROUP_ID[GENERATORS[label]], n) + for label in GENERATORS + for n in IDEMPOTENTS +) +FACTOR_ID = {(label, n): i for i, (label, _, n) in enumerate(FACTORS)} + + +def make_shift_table(gid: int) -> tuple[tuple[int, ...], ...]: + table = [] + for chunk in range(6): + values = [] + for nibble in range(16): + out = 0 + for offset in range(4): + source = 4 * chunk + offset + if source < len(GROUP) and ((nibble >> offset) & 1): + out |= 1 << GROUP_PRODUCT[gid][source] + values.append(out) + table.append(tuple(values)) + return tuple(table) + + +SHIFT_TABLES = { + gid: make_shift_table(gid) + for gid in { + UNIT, + TARGET_ID, + MUTATED_TARGET_ID, + *(GROUP_ID[g] for g in GENERATORS.values()), + } +} + + +def shift_left(poly: int, gid: int) -> int: + table = SHIFT_TABLES[gid] + return ( + table[0][poly & 0xF] + | table[1][(poly >> 4) & 0xF] + | table[2][(poly >> 8) & 0xF] + | table[3][(poly >> 12) & 0xF] + | table[4][(poly >> 16) & 0xF] + | table[5][(poly >> 20) & 0xF] + ) + + +IDENTITY_STATE = (1 << UNIT, 0, 0, 1 << UNIT) + + +def left_factor(state: tuple[int, int, int, int], factor_id: int) -> tuple[int, int, int, int]: + """Compute D_N(g) * state exactly in M_2(F2[G]).""" + _, gid, n = FACTORS[factor_id] + out = [] + for i in range(2): + for j in range(2): + mixed = 0 + for k in range(2): + if (n >> (2 * i + k)) & 1: + mixed ^= state[2 * k + j] + out.append(state[2 * i + j] ^ mixed ^ shift_left(mixed, gid)) + return tuple(out) # type: ignore[return-value] + + +def replay(word: bytes) -> tuple[int, int, int, int]: + state = IDENTITY_STATE + for factor_id in word: + state = left_factor(state, factor_id) + return state + + +def word_for_labels(labels: bytes, n: int) -> bytes: + return bytes(FACTOR_ID[(chr(label), n)] for label in labels) + + +DIRECT_WORD = word_for_labels(DIRECT_LABELS, 0b0001) + word_for_labels( + DIRECT_LABELS, 0b1000 +) +MUTATED_DIRECT_WORD = word_for_labels(DIRECT_MUTATED_LABELS, 0b0001) + word_for_labels( + DIRECT_MUTATED_LABELS, 0b1000 +) +PIVOT_DIRECT_WORD = word_for_labels(DIRECT_LABELS, 0b0001) + word_for_labels( + DIRECT_MUTATED_LABELS, 0b1000 +) + + +def diagonal_target(hid: int) -> tuple[int, int, int, int]: + return (1 << hid, 0, 0, 1 << hid) + + +TARGET_STATE = diagonal_target(TARGET_ID) +MUTATED_TARGET_STATE = diagonal_target(MUTATED_TARGET_ID) +PIVOT_TARGETS = (TARGET_ID, MUTATED_TARGET_ID) +PIVOT_TARGET_STATE = (1 << TARGET_ID, 0, 0, 1 << MUTATED_TARGET_ID) +REVERSED_PIVOT_STATE = (1 << MUTATED_TARGET_ID, 0, 0, 1 << TARGET_ID) + + +def target_left_times( + state: tuple[int, int, int, int], targets: tuple[int, int] +) -> tuple[int, int, int, int]: + """Multiply diag([h0],[h1]) by state on the left.""" + return tuple( + shift_left(state[2 * row + col], targets[row]) + for row in range(2) + for col in range(2) + ) # type: ignore[return-value] + + +def radius_ball(radius: int) -> dict[tuple[int, int, int, int], bytes]: + """Shortest witness to every exact group-algebra state within radius.""" + seen = {IDENTITY_STATE: b""} + frontier = [IDENTITY_STATE] + for _ in range(radius): + next_frontier = [] + for state in frontier: + prefix = seen[state] + for factor_id in range(len(FACTORS)): + nxt = left_factor(state, factor_id) + if nxt not in seen: + seen[nxt] = prefix + bytes((factor_id,)) + next_frontier.append(nxt) + frontier = next_frontier + return seen + + +def state_digest(states: dict[tuple[int, int, int, int], bytes]) -> str: + digest = hashlib.sha256() + for state in sorted(states): + digest.update(" ".join(f"{x:06x}" for x in state).encode("ascii")) + digest.update(b"\n") + return digest.hexdigest() + + +def factor_name(factor_id: int) -> str: + label, _, n = FACTORS[factor_id] + entries = "".join(str((n >> i) & 1) for i in range(4)) + return f"{label}:N={entries}" + + +def word_names(word: bytes) -> list[str]: + return [factor_name(fid) for fid in word] + + +def displacement_rank(h: tuple[int, int]) -> int: + a, b = h + columns = [] + for j in range(2): + columns.append( + (((a >> j) & 1) ^ int(j == 0)) + | ((((a >> (2 + j)) & 1) ^ int(j == 1)) << 1) + ) + columns.append(b) + basis: list[int] = [] + for col in columns: + x = col + for y in basis: + x = min(x, x ^ y) + if x: + basis.append(x) + basis.sort(reverse=True) + return len(basis) + + +def shortest_address_word(target: tuple[int, int]) -> tuple[int, bytes]: + distances = {IDENTITY_AFFINE: (0, b"")} + queue = deque([IDENTITY_AFFINE]) + labels = tuple(GENERATORS) + while queue: + current = queue.popleft() + distance, word = distances[current] + for label in labels: + nxt = compose(GENERATORS[label], current) + if nxt not in distances: + distances[nxt] = (distance + 1, word + label.encode("ascii")) + queue.append(nxt) + return distances[target] + + +def exact_join( + targets: tuple[int, int], + left: dict[tuple[int, int, int, int], bytes], + right: dict[tuple[int, int, int, int], bytes], + radius_left: int = 3, + radius_right: int = 4, +) -> tuple[dict, bytes | None]: + best: bytes | None = None + best_length: int | None = None + for prefix_state, prefix_word in left.items(): + inverse_state = replay(prefix_word[::-1]) + needed_suffix = target_left_times(inverse_state, targets) + suffix_word = right.get(needed_suffix) + if suffix_word is None: + continue + candidate = prefix_word + suffix_word + if best_length is None or (len(candidate), candidate) < (best_length, best): + best = candidate + best_length = len(candidate) + details = { + "left_radius": radius_left, + "right_radius": radius_right, + "left_states": len(left), + "right_states": len(right), + "left_state_sha256": state_digest(left), + "right_state_sha256": state_digest(right), + "left_states_examined": len(left), + "endpoint_reachable_within_7": best is not None, + "minimum_word_length_found": best_length, + } + return details, best + + +def build_certificate() -> tuple[dict, bytes | None]: + if len(GROUP) != 24 or len(IDEMPOTENTS) != 6 or len(FACTORS) != 24: + raise AssertionError("the declared AGL2 group/factor alphabet is incomplete") + for g in (GROUP_ID[x] for x in GENERATORS.values()): + if GROUP_PRODUCT[g][g] != UNIT: + raise AssertionError("each paid address generator must be an involution") + for n in IDEMPOTENTS: + if matrix_product(n, n) != n or matrix_rank(n) != 1: + raise AssertionError("bad rank-one idempotent enumeration") + for g in range(len(GROUP)): + if GROUP_PRODUCT[UNIT][g] != g or GROUP_PRODUCT[g][UNIT] != g: + raise AssertionError("the affine group identity table is inconsistent") + for h in range(len(GROUP)): + for k in range(len(GROUP)): + if GROUP_PRODUCT[GROUP_PRODUCT[g][h]][k] != GROUP_PRODUCT[g][GROUP_PRODUCT[h][k]]: + raise AssertionError("the affine multiplication table is not associative") + for factor_id in range(len(FACTORS)): + if left_factor(left_factor(IDENTITY_STATE, factor_id), factor_id) != IDENTITY_STATE: + raise AssertionError("a paid factor is not a formal involution") + + direct_distance, direct_address_word = shortest_address_word(TARGET) + mutated_distance, mutated_address_word = shortest_address_word(MUTATED_TARGET) + target_rank = displacement_rank(TARGET) + if direct_distance != 4 or direct_address_word != b"abav": + raise AssertionError("the pinned target direct-distance calculation changed") + if mutated_distance != 4 or mutated_address_word != b"abau": + raise AssertionError("the changed-target direct-distance control changed") + if target_rank != 2 or displacement_rank(MUTATED_TARGET) != 2: + raise AssertionError("the displacement-rank accounting changed") + if replay(DIRECT_WORD) != TARGET_STATE: + raise AssertionError("the eight-call direct positive control failed") + if replay(MUTATED_DIRECT_WORD) != MUTATED_TARGET_STATE: + raise AssertionError("the changed-target direct control failed") + if TARGET_STATE == MUTATED_TARGET_STATE or replay(DIRECT_WORD) == MUTATED_TARGET_STATE: + raise AssertionError("the changed-target negative control failed") + for i in range(len(DIRECT_WORD)): + if replay(DIRECT_WORD[:i] + DIRECT_WORD[i + 1 :]) == TARGET_STATE: + raise AssertionError(f"omitting direct call {i} unexpectedly preserves the endpoint") + + if compose(TARGET, MUTATED_TARGET) != IDENTITY_AFFINE: + raise AssertionError("the pivot target is not the inverse affine map") + if compose(MUTATED_TARGET, TARGET) != IDENTITY_AFFINE: + raise AssertionError("the pivot target is not a two-sided inverse") + if replay(PIVOT_DIRECT_WORD) != PIVOT_TARGET_STATE: + raise AssertionError("the eight-call inverse-pair control failed") + if replay(PIVOT_DIRECT_WORD) == REVERSED_PIVOT_STATE: + raise AssertionError("the target-order mutation was not distinguished") + for i in range(len(PIVOT_DIRECT_WORD)): + if replay(PIVOT_DIRECT_WORD[:i] + PIVOT_DIRECT_WORD[i + 1 :]) == PIVOT_TARGET_STATE: + raise AssertionError(f"omitting pivot direct call {i} preserves the endpoint") + + left = radius_ball(3) + right = radius_ball(4) + same_join, same_witness = exact_join((TARGET_ID, TARGET_ID), left, right) + pivot_join, pivot_witness = exact_join(PIVOT_TARGETS, left, right) + if same_witness is not None and replay(same_witness) != TARGET_STATE: + raise AssertionError("the same-target short witness failed full formal replay") + if pivot_witness is not None and replay(pivot_witness) != PIVOT_TARGET_STATE: + raise AssertionError("the inverse-pair short witness failed full formal replay") + for target_state, witness in ( + (TARGET_STATE, same_witness), + (PIVOT_TARGET_STATE, pivot_witness), + ): + if witness is not None: + for i in range(len(witness)): + if replay(witness[:i] + witness[i + 1 :]) == target_state: + raise AssertionError("a returned short witness was not minimal") + if ( + same_join["left_state_sha256"] != pivot_join["left_state_sha256"] + or same_join["right_state_sha256"] != pivot_join["right_state_sha256"] + ): + raise AssertionError("the shared exhaustive state sets changed between endpoints") + + result = { + "schema_version": 1, + "model": { + "address_group": "AGL_2(F_2)", + "formal_ring": "F_2[AGL_2(F_2)]", + "registers": 2, + "workspace": "none", + "free_scalar_mixing": "GL_2(F_2), normalized into the six paid idempotents by augmentation", + "paid_labels": { + label: {"matrix_row_major": f"{g[0]:04b}", "translation": f"{g[1]:02b}"} + for label, g in GENERATORS.items() + }, + "calls_per_label_per_idempotent": 1, + "rank_one_idempotents": [f"{n:04b}" for n in IDEMPOTENTS], + "paid_factor_count": len(FACTORS), + "factor": "D_N(g)=I+([g]+[1])N", + }, + "first_endpoint": { + "map_per_target": "h(x0,x1)=(x1,x0+1)", + "formal_endpoint": "diag([h],[h])", + "direct_word_per_target": direct_address_word.decode("ascii"), + "direct_calls_total": 2 * direct_distance, + "rank_floor": 2 * target_rank, + "search": same_join, + "short_witness": None + if same_witness is None + else {"length": len(same_witness), "factors": word_names(same_witness)}, + "minimum": 8 if same_witness is None else len(same_witness), + }, + "pivot_endpoint": { + "maps": [ + "h(x0,x1)=(x1,x0+1)", + "h_inverse(x0,x1)=(x1+1,x0)", + ], + "formal_endpoint": "diag([h],[h_inverse])", + "direct_words": [ + direct_address_word.decode("ascii"), + mutated_address_word.decode("ascii"), + ], + "direct_calls_total": direct_distance + mutated_distance, + "rank_floor": target_rank + displacement_rank(MUTATED_TARGET), + "search": pivot_join, + "short_witness": None + if pivot_witness is None + else {"length": len(pivot_witness), "factors": word_names(pivot_witness)}, + "minimum": 8 if pivot_witness is None else len(pivot_witness), + }, + "direct_controls": { + "same_target_word": word_names(DIRECT_WORD), + "inverse_pair_word": word_names(PIVOT_DIRECT_WORD), + "all_8_single_call_omissions_rejected": True, + "changed_target_and_target_order_rejected": True, + }, + "conclusion": ( + "both fixed two-register endpoints require 8 calls" + if same_witness is None and pivot_witness is None + else "bounded exact minima recorded for both endpoints" + ), + "controls": { + "all_24_formal_group_elements_enumerated": len(GROUP) == 24, + "all_6_rank_one_idempotents_enumerated": len(IDEMPOTENTS) == 6, + "all_24_paid_factors_included": len(FACTORS) == 24, + "direct_formal_endpoint_passes": True, + "omitted_call_mutations_rejected": True, + "changed_affine_target_mutation_rejected": True, + "inverse_target_pair_verified": True, + "two_endpoints_share_identical_complete_state_balls": True, + }, + } + return result, pivot_witness + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument( + "--write-certificate", + action="store_true", + help="write the deterministically recomputed certificate during development", + ) + args = parser.parse_args() + actual, witness = build_certificate() + path = ROOT / "CERTIFICATE.json" + encoded = json.dumps(actual, indent=2, sort_keys=True) + "\n" + if args.write_certificate: + path.write_text(encoded) + print("WROTE_BIT_AFFINE_GENERATOR_SHARING_CERTIFICATE") + else: + expected = json.loads(path.read_text()) + if actual != expected: + raise SystemExit("FAIL_BIT_AFFINE_GENERATOR_SHARING_CERTIFICATE_MISMATCH") + print("PASS_BIT_AFFINE_GENERATOR_SHARING") + print(actual["conclusion"]) + first = actual["first_endpoint"] + pivot = actual["pivot_endpoint"] + print( + "radius_states=" + f"{pivot['search']['left_states']}/" + f"{pivot['search']['right_states']} " + f"examined={pivot['search']['left_states_examined']} " + f"same_target_min={first['minimum']} " + f"inverse_pair_min={pivot['minimum']} " + f"pivot_witness_length={None if witness is None else len(witness)}" + ) + + +if __name__ == "__main__": + main()