From ce08fe61d030b27da74c367cf4f9da537a3ddd06 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:21:38 +0000 Subject: [PATCH] feat(research): cut signed Hadamard lowering to 208 primitives --- research/hadamard-extra-source/README.md | 242 ++++++++++++++++++++ research/hadamard-extra-source/SOURCES.json | 36 +++ research/hadamard-extra-source/TASK.json | 110 +++++++++ research/hadamard-extra-source/VERIFY.json | 34 +++ research/hadamard-extra-source/verify.py | 221 ++++++++++++++++++ 5 files changed, 643 insertions(+) create mode 100644 research/hadamard-extra-source/README.md create mode 100644 research/hadamard-extra-source/SOURCES.json create mode 100644 research/hadamard-extra-source/TASK.json create mode 100644 research/hadamard-extra-source/VERIFY.json create mode 100644 research/hadamard-extra-source/verify.py diff --git a/research/hadamard-extra-source/README.md b/research/hadamard-extra-source/README.md new file mode 100644 index 0000000000..c9806658e7 --- /dev/null +++ b/research/hadamard-extra-source/README.md @@ -0,0 +1,242 @@ +# A 208-primitive signed Hadamard connector + +This contribution was produced by Nick Petalas. Apache-2.0. + +An explicit exact construction reduces the signed four-source/four-output +Hadamard batch from the cited 222 primitive calls in Cinna Davis's +[PR #1158](https://github.com/CrocSwap/integer-mult-bounds/pull/1158) to +**208**, a saving of **14**. The new word has 22 complete top-level queries, +62 internal echo nodes and four dirty scratch rows. The cited comparator +has 24 queries, 66 echo nodes and the same four dirty rows. Its result is +used as a predecessor, not audited or replayed here. + +The change is two additional restoring queries on the cheapest source. +They permit four fewer readouts on the first output. This leaves the +predecessor's exactly-eight-source-call class, so it does not contradict +that class's optimum. The claim is an exact finite construction with a +scoped algebraic proof. Neither unrestricted optimality nor a new kappa +is claimed. + +## Contract + +There are four read-only sources x_j, four distinct accumulating outputs y_i, +and an arbitrary dirty connector z. For exact additive linear maps A_i,B_j, +the permitted queries are + +```text +source j, sign s: z += s B_j x_j +output i, sign s: y_i += s A_i z s in {-1,+1}. +``` + +Maps need not commute. Each query restores its private workspace and every +source it reads. Outputs cannot be borrowed as workspace. The target is + +```text +y_i += sum_j H_ij A_i B_j x_j, +H = [ 1 1 1 1 ] + [ 1 -1 1 -1 ] + [ 1 1 -1 -1 ] + [ 1 -1 -1 1 ]. +``` + +All row numbers below are zero-based. All rows have a common compatible +module or vector-space dimension. The identities use only addition, +subtraction and composition, so the proof works over any commutative base +ring with exact linear maps. Rounded or nonlinear children require a +separate contract. + +## The word and proof + +Execute the following ten source events in order. A symbol +j or -j means +a signed source query, not a scalar operation assumed free. + +```text +-0, -1, +0, +3, -2, -3, +1, +0, -0, +2. +``` + +Let q_t be the source-coefficient vector in z after t source events. +Initially q_0=0, and z=z_initial+sum_j (q_t)_j B_j x_j. The complete path is + +```text +t: 0 1 2 3 4 5 6 7 8 9 10 +q_t[0]: 0 -1 -1 0 0 0 0 0 1 0 0 +q_t[1]: 0 0 -1 -1 -1 -1 -1 0 0 0 0 +q_t[2]: 0 0 0 0 0 -1 -1 -1 -1 -1 0 +q_t[3]: 0 0 0 0 1 1 0 0 0 0 0 +``` + +Insert these readouts at their indicated source-prefix visits: + +```text +output 0: +A_0 z at t=10 and t=4; -A_0 z at t=2 and t=6 +output 1: +A_1 z twice at t=3; -A_1 z at t=1 and t=5 +output 2: +A_2 z at t=8; -A_2 z at t=4 +output 3: +A_3 z at t=5; -A_3 z at t=1. +``` + +Readouts at a common visit can be executed in either order because they +write distinct outputs, or repeatedly add the same source value. The two +positive output-1 calls are both paid. No doubling instruction is free. + +For each output the signed coefficients of z_initial sum to zero. The +remaining source coefficients are exactly + +```text +q_10 - q_2 + q_4 - q_6 = (1, 1, 1, 1) +2 q_3 - q_1 - q_5 = (1,-1, 1,-1) +q_8 - q_4 = (1, 1,-1,-1) +q_5 - q_1 = (1,-1,-1, 1). +``` + +Linearity therefore proves the desired map without exchanging the order +of A_i and B_j. Also q_10=0, so z restores exactly. Source queries never +write x, and readouts only accumulate into y. Initial output values are +preserved additively. This proves the complete arbitrary-input endpoint. + +## Every child and inverse is charged + +Use the predecessor's fixed product lengths + +```text +A lengths = (2,3,4,5), B lengths = (1,2,3,4). +``` + +Factors are listed in application order. For a product with n factors, +split the first b=floor(n/2) from the last a=ceil(n/2), so the operator is +A B. A positive product query is the literal dirty echo + +```text +u += B source; target += A u; +u -= B source; target -= A u. +``` + +Its negative is the complete reversed word with all signs negated. +This restores arbitrary u and implements the product in its original +order. Descendant scratch excludes both active rows and all ancestors. +The written induction proves the lowering at every finite dimension. + +The primitive and internal-node recurrences are + +```text +C(1)=1, C(n)=2 C(b)+2 C(a), C(1..5)=(1,4,10,16,28) +I(1)=0, I(n)=1+2 I(b)+2 I(a), I(1..5)=(0,1,3,5,9). +``` + +The new source profile is (4,2,2,2), costing +`4*1+2*4+2*10+2*16=64` primitives and 18 echo nodes. The output profile is +(4,4,2,2), costing `4*4+4*10+2*16+2*28=144` primitives and 44 echo nodes. +Thus the literal program has **208 primitives and 62 echo nodes**. There +are ten source queries and twelve readouts. The largest child has length +five and uses three private dirty rows; including z gives four dirty rows. +The verifier expands every call and checks these counts directly. + +Under the predecessor's complete-cost notation, price a primitive by E, +an echo node's extra control by D, a complete query dispatch by Q, and +all remaining preparation/placement costs by P+R. The new complete bill is + +```text +208 E + 62 D + 22 Q + P_new + R_new. +``` + +Against the cited comparator, the benefit survives precisely when its +additional P+R expense is less than `14 E + 4 D + 2 Q`. This charges extra +source calls and every child/inverse. It does not assert that physical +layout or precision makes P and R equal. The same 24 distinct factor maps +are used; no new coefficient oracle is supplied. + +## Evidence and reproduction + +From the worktree root, using CPython 3.12 and only the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/hadamard-extra-source/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/hadamard-extra-source/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/hadamard-extra-source +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/hadamard-extra-source --check-source-history +``` + +Another CPython 3.12 installation may replace that interpreter path. +Expected markers are `PASS_HADAMARD_EXTRA_SOURCE`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The source-history check requires committed package bytes and full history. + +The verifier checks the formal query endpoint with independent A/B symbols, +then expands all 208 leaves and checks the endpoint with independent +noncommuting primitive symbols. Both include every input role and all +four arbitrary dirty rows. Separate dense matrix execution checks all 24 +basis inputs and two dense inputs for each of four factor assignments, +104 input cases in total. Every case also runs the complete literal inverse. +There are 25 rejection controls: deleting each of 22 top-level calls, +deleting the final primitive restoration, changing one target sign and +aliasing the active registers. Checks use explicit exceptions and remain +active under optimized Python. Generated stdout receipts bind all five +package files by SHA256. No receipt is handwritten. + +A bounded proposal search with deterministic seed 1158 found this word on +its tenth path and stopped immediately. Only the witness, its proof and +standalone verifier are part of the result; no census or optimality claim +is made. No predecessor scientific executable is imported or replayed. + +## Scope, provenance and credit + +Scientific base is canonical main +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. The selected +baseline passed its source-binding check only. This is a historical +recursive-interface side result, explicitly changed from the +`bit-new-register-model` card. It does not supply a native larger-register +BIT program, current caller or selected-supplier improvement. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220061) +names the additional-source boundary. Live PRs, this account's recent PRs, +handoffs, active Discussions, local reservations, all-main README terms, +targeted merged PRs and the overlap helper were checked. Sparse local notes, +arbitrary historical diffs and unpublished work are not fully covered. +[SOURCES.json](SOURCES.json) binds predecessor proof text as historical +provenance. There are no external runtime inputs. + +Credit Cinna Davis / 1337isnot1337 #1158 for the exact eight-source-call +census, weighted envelope, 222-primitive comparator and explicit excluded +boundary, and #997 for the signed Hadamard batch. Retain Martin #1088, +Jerry Chen / CubeJerry #889, Ross Richardson #934/#943/#944 and Chafik +Boukhalfa #628 for the weighted-repair, connector and dirty-echo lineage. +Their results are cited, not claimed as new. All predecessor files and +credit lines are unchanged. The new material is the ten-source word, +its 208-primitive lowering and exact verification. + +Native realization, physical routing, precision/error propagation, stock, +complete supplier admission and the multiplication theorem remain unproved. +No Lean, Docker or selected scientific cold replay was run. Independent +human and formal proof-kernel review are unclaimed. Selected kappa is +unchanged. + +## Open next questions + +1. What is the least weighted query price with arbitrary restoring source + multiplicities for this fixed Hadamard target? Begin with this word as + an upper bound and derive a lower bound that charges each source + separately. Unbounded integer paths need a completeness argument; + bounded sampling does not provide one. +2. Can one actual physical caller retain the saving after all layout and + precision costs? Bind that caller and compare its additional P+R cost + with `14E+4D+2Q`. No such caller is supplied here. + +The structured questions, relevance and blockers are in TASK.json. + +## Verifier bounds + +The verifier has no recursion, subprocesses, network access or write path. +Functions are at most 37 physical lines. The formal pass has at most 208 +calls, 12 registers and 2,048 retained monomials per destination. Lowering +has a 512-iteration guard and depth three. Dense execution has exactly +104 fixed inputs of 24 scalar coordinates and at most 208 steps per pass. +Receipt reads are limited to 128 KiB plus one guard byte per fixed file. +Normal/optimized warning-strict runs and in-memory source compilation +provide the available Python diagnostics. No external analyzer was run. + +Power of Ten rule 3 needs a managed-runtime deviation: CPython allocates +objects dynamically. The fixed call, dimension, polynomial and read limits +bound this terminating verifier's live collections. Internal integers have +no fixed machine width; the input fixtures and finite operation count bound +their growth. No allocator-internals or fixed-memory runtime claim is made. +The literal inverse is the reverse of a finite 208-step list. The direct +call graph is acyclic and all failure checks propagate as exceptions. diff --git a/research/hadamard-extra-source/SOURCES.json b/research/hadamard-extra-source/SOURCES.json new file mode 100644 index 0000000000..375c30e8e5 --- /dev/null +++ b/research/hadamard-extra-source/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/hadamard-readout-census/PROOF.md", + "usage": "provenance", + "git_blob": "b8e7db27bf0750275ea515666bf6c2ac046ee288", + "sha256": "7d785eca19c16e6d6b196b4afb187bbf8197f9a9e0edb152aaeae3581ad73e65" + }, + { + "path": "research/hadamard-readout-census/README.md", + "usage": "provenance", + "git_blob": "8bb0721e43cf737c731810468cebd1eaf6121fe2", + "sha256": "a21e7488eee84daae23d0a338debf6a8281584a3f67f1ec0609daf6a8bba6859" + }, + { + "path": "research/signed-hadamard-batch-seed55/README.md", + "usage": "provenance", + "git_blob": "fb146527f08eaa6b933550b56d535a9ca97f806b", + "sha256": "408401c5e83c78a61621c08250f24578f289306d6e7d62b9132039cc9a152ecc" + } + ] +} diff --git a/research/hadamard-extra-source/TASK.json b/research/hadamard-extra-source/TASK.json new file mode 100644 index 0000000000..f7d37fe339 --- /dev/null +++ b/research/hadamard-extra-source/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "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. 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": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "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.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Explicit 208-primitive signed Hadamard four-source/four-output construction using ten restoring source queries and twelve readouts, with arbitrary dirty connector and all child scratch restored.", + "scope_change_reason": "The larger/nonabelian BIT card is changed to an exact-linear signed connector side result. PR1158 explicitly excludes additional source calls; the new word changes that hypothesis. It does not claim a native BIT improvement.", + "bottleneck_link": "Complete paid child counts can fall when two extra cheap source calls replace expensive readouts. This historical connector illustrates that boundary change; no selected supplier or kappa changes.", + "budget_minutes": 60, + "stop_rule": "Stop at the first strict verified improvement over the cited 222 primitive construction, or after at most 100000 sampled paths and the session budget.", + "outcome": "completed", + "evidence": "Written coefficient proof; independent formal expansion of 22 query calls and all 208 primitive calls; 104 dense input and literal-inverse pairs; 25 rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the smallest complete weighted query price when arbitrary restoring source multiplicities are allowed for this fixed Hadamard target?", + "why_it_matters": "The new word beats the fixed-eight-source optimum but has no unrestricted optimality proof.", + "first_step": "Use the explicit 10-source word as an upper bound and derive a lower bound that charges each source separately.", + "blocked_by": "Unbounded integer source paths and query multiplicities require a completeness argument beyond bounded sampling." + }, + { + "question": "Can a named physical caller retain the 14 primitive, four echo-node and two dispatch savings after layout and precision costs?", + "why_it_matters": "The algebraic reduction alone does not improve the selected supplier.", + "first_step": "Bind one caller and compare its complete P and R overhead with 14E+4D+2Q.", + "blocked_by": "No actual caller, physical routing or rounded-error contract is supplied here." + } + ], + "claim_type": "exact finite construction with scoped algebraic proof", + "coordination_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220061", + "search": { + "seed": 1158, + "attempted_paths": 10, + "accepted_trial_zero_based": 9, + "stop_on_first_improvement": true, + "maximum_paths": 100000, + "source_profile": [ + 4, + 2, + 2, + 2 + ] + }, + "predecessors": [ + { + "pr": 1158, + "author": "Cinna Davis / 1337isnot1337", + "head": "6336d879c0ba168463bf2f6fae9e653c870299fc", + "use": "Cited eight-source-call weighted optimum and balanced 222-primitive comparator; not replayed." + }, + { + "pr": 997, + "author": "Cinna Davis / 1337isnot1337", + "head": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "use": "Signed Hadamard batch and arbitrary-dirty product-child lineage." + } + ], + "verification_environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + }, + "overlap": { + "checked_utc": "2026-10-27T15:18:39.896801+00:00", + "base": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "sources": "live open PRs, 307 account PRs created in the last seven days, latest handoffs, active Discussions, all-main README terms, targeted merged PR searches, local batch reservations and find_overlap.py", + "limits": "Sparse local files; no exhaustive arbitrary code diffs, unpublished work or global literature priority claim." + } +} diff --git a/research/hadamard-extra-source/VERIFY.json b/research/hadamard-extra-source/VERIFY.json new file mode 100644 index 0000000000..0078cc285d --- /dev/null +++ b/research/hadamard-extra-source/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact formal query/primitive endpoints, complete leaf and echo invoice, dense noncommuting input/inverse pairs, missing-call/sign/alias rejection controls and generated package hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact formal query/primitive endpoints, complete leaf and echo invoice, dense noncommuting input/inverse pairs, missing-call/sign/alias rejection controls and generated package hashes." + } + ] +} diff --git a/research/hadamard-extra-source/verify.py b/research/hadamard-extra-source/verify.py new file mode 100644 index 0000000000..aad8e85a3e --- /dev/null +++ b/research/hadamard-extra-source/verify.py @@ -0,0 +1,221 @@ +"""Exact new Hadamard connector and literal dirty-child replay; stdlib only.""" +import hashlib +import json +from pathlib import Path +import sys + +H = ((1, 1, 1, 1), (1, -1, 1, -1), + (1, 1, -1, -1), (1, -1, -1, 1)) +SOURCE = ((0, -1), (1, -1), (0, 1), (3, 1), (2, -1), + (3, -1), (1, 1), (0, 1), (0, -1), (2, 1)) +# (visited source-prefix number, output, sign); repeated taps are paid. +TAPS = ((1, 1, -1), (1, 3, -1), (2, 0, -1), + (3, 1, 1), (3, 1, 1), (4, 0, 1), (4, 2, -1), + (5, 1, -1), (5, 3, 1), (6, 0, -1), + (8, 2, 1), (10, 0, 1)) +A_LENGTH = (2, 3, 4, 5) +B_LENGTH = (1, 2, 3, 4) +FILES = ('README.md', 'SOURCES.json', 'TASK.json', 'VERIFY.json', 'verify.py') + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def program(): + calls = [] + for t in range(11): + if t: + j, sign = SOURCE[t - 1] + calls.append((8, j, ('B', j), sign)) + for at, i, sign in TAPS: + if at == t: + calls.append((4 + i, 8, ('A', i), sign)) + require(len(calls) == 22, 'top-level call count') + return tuple(calls) + + +def formal_endpoint(calls): + # Each polynomial maps (outer-to-inner operator word, initial role) to Z. + rows = [{((), r): 1} for r in range(12)] + for dst, src, label, sign in calls: + require(0 <= dst < 12 and 0 <= src < 12 and dst != src, + 'invalid register pair') + require(sign in (-1, 1), 'invalid sign') + for (word, root), coefficient in tuple(rows[src].items()): + key = ((label,) + word, root) + rows[dst][key] = rows[dst].get(key, 0) + sign * coefficient + if rows[dst][key] == 0: + del rows[dst][key] + require(len(rows[dst]) <= 2048, 'formal polynomial capacity') + return rows + + +def expected_endpoint(): + rows = [{((), r): 1} for r in range(12)] + for i in range(4): + for j in range(4): + rows[4 + i][((('A', i), ('B', j)), j)] = H[i][j] + return rows + + +def factors(label): + kind, i = label + length = A_LENGTH[i] if kind == 'A' else B_LENGTH[i] + # Listed in application order; the rightmost matrix acts first. + return tuple((kind, i, k) for k in range(length)) + + +def lower(calls): + leaves = [] + echoes = 0 + max_depth = 0 + stack = [(d, s, factors(op), sign, (9, 10, 11)) + for d, s, op, sign in reversed(calls)] + for _ in range(512): + if not stack: + break + dst, src, fs, sign, scratch = stack.pop() + require(dst != src and dst not in scratch and src not in scratch, + 'dirty scratch aliases an active role') + max_depth = max(max_depth, 3 - len(scratch)) + if len(fs) == 1: + leaves.append((dst, src, fs[0], sign)) + continue + require(len(fs) <= 5 and scratch, 'child depth capacity') + echoes += 1 + u, rest = scratch[0], scratch[1:] + cut = len(fs) // 2 + b, a = fs[:cut], fs[cut:] + parts = [(u, src, b, 1, rest), (dst, u, a, 1, rest), + (u, src, b, -1, rest), (dst, u, a, -1, rest)] + if sign == -1: + parts = [(d, s, f, -e, pool) + for d, s, f, e, pool in reversed(parts)] + stack.extend(reversed(parts)) + require(not stack, 'lowering iteration bound') + require(len(leaves) == 208 and echoes == 62 and max_depth == 3, + 'complete child bill') + return tuple(leaves), echoes + + +def primitive_expected(): + rows = [{((), r): 1} for r in range(12)] + for i in range(4): + for j in range(4): + word = tuple(reversed(factors(('A', i)))) + word += tuple(reversed(factors(('B', j)))) + rows[4 + i][(word, j)] = H[i][j] + return rows + + +def matrix(label, variant): + kind, i, k = label + n = 1 + i + 2 * k + (7 if kind == 'A' else 0) + variant + return ((n % 5 - 2, (n * n + 1) % 7 - 3), + ((3 * n + 2) % 7 - 3, (n + 3) % 5 - 2)) + + +def apply_matrix(m, v): + return tuple(sum(m[i][j] * v[j] for j in range(2)) for i in range(2)) + + +def dense_replay(calls, initial, variant): + rows = [tuple(row) for row in initial] + for dst, src, label, sign in calls: + value = apply_matrix(matrix(label, variant), rows[src]) + rows[dst] = tuple(rows[dst][k] + sign * value[k] for k in range(2)) + return rows + + +def dense_expected(initial, variant): + rows = [tuple(row) for row in initial] + for i in range(4): + for j in range(4): + value = tuple(initial[j]) + for op in factors(('B', j)) + factors(('A', i)): + value = apply_matrix(matrix(op, variant), value) + rows[4 + i] = tuple(rows[4 + i][k] + H[i][j] * value[k] + for k in range(2)) + return rows + + +def check_dense(leaves): + count = 0 + inverse = tuple((d, s, op, -sign) for d, s, op, sign in reversed(leaves)) + for variant in range(4): + inputs = [] + for column in range(24): + inputs.append([tuple(int(2 * r + k == column) for k in range(2)) + for r in range(12)]) + inputs += [[(r - 7, 3 * r - 8) for r in range(12)], + [(5 - 2 * r, r * r - 9) for r in range(12)]] + for initial in inputs: + result = dense_replay(leaves, initial, variant) + require(result == dense_expected(initial, variant), 'dense endpoint') + require(dense_replay(inverse, result, variant) == initial, + 'literal full inverse') + count += 1 + return count + + +def controls(calls, leaves): + rejected = 0 + target = expected_endpoint() + for i in range(len(calls)): + require(formal_endpoint(calls[:i] + calls[i + 1:]) != target, + 'undetected missing top-level call') + rejected += 1 + require(formal_endpoint(leaves[:-1]) != primitive_expected(), + 'undetected missing primitive restoration') + rejected += 1 + # Change one demanded sign: the computed map must reject the false target. + wrong = expected_endpoint() + wrong[4][((('A', 0), ('B', 0)), 0)] = -1 + require(formal_endpoint(calls) != wrong, 'undetected target-sign error') + rejected += 1 + try: + formal_endpoint(((8, 8, ('A', 0), 1),)) + except ValueError: + rejected += 1 + else: + raise ValueError('accepted aliasing') + return rejected + + +def receipt(): + hashes = {} + for name in FILES: + with (Path(__file__).resolve().parent / name).open('rb') as handle: + data = handle.read(131073) + require(len(data) <= 131072, 'receipt file capacity') + hashes[name] = hashlib.sha256(data).hexdigest() + return hashes + + +def main(): + calls = program() + require(formal_endpoint(calls) == expected_endpoint(), 'formal query map') + leaves, echoes = lower(calls) + require(formal_endpoint(leaves) == primitive_expected(), 'formal leaf map') + a_profile = tuple(sum(op == ('A', i) for _, _, op, _ in calls) + for i in range(4)) + b_profile = tuple(sum(op == ('B', i) for _, _, op, _ in calls) + for i in range(4)) + require(a_profile == (4, 4, 2, 2) and b_profile == (4, 2, 2, 2), + 'query profiles') + require(sum(op[0] == 'B' for _, _, op, _ in leaves) == 64, 'source price') + require(sum(op[0] == 'A' for _, _, op, _ in leaves) == 144, 'readout price') + print(json.dumps({'status': 'PASS_HADAMARD_EXTRA_SOURCE', + 'primitive_calls': len(leaves), 'echo_nodes': echoes, + 'top_level_queries': len(calls), + 'source_profile': b_profile, 'readout_profile': a_profile, + 'dense_inputs_and_inverse_pairs': check_dense(leaves), + 'rejection_controls': controls(calls, leaves), + 'package_sha256': receipt(), 'python': sys.version, + 'claim': 'exact construction; no new kappa'}, sort_keys=True)) + + +if __name__ == '__main__': + main()