From 5fcfa050f2fc5445d7f0997206c5044b17f7e88f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 12:48:53 +0100 Subject: [PATCH] feat(research): prove exact finite-width mixing tradeoff --- .../README.md | 216 ++++++++++++++++ .../SOURCES.json | 30 +++ .../TASK.json | 114 +++++++++ .../VERIFY.json | 34 +++ .../verify.py | 241 ++++++++++++++++++ 5 files changed, 635 insertions(+) create mode 100644 research/finite-width-call-mixing-tradeoff/README.md create mode 100644 research/finite-width-call-mixing-tradeoff/SOURCES.json create mode 100644 research/finite-width-call-mixing-tradeoff/TASK.json create mode 100644 research/finite-width-call-mixing-tradeoff/VERIFY.json create mode 100644 research/finite-width-call-mixing-tradeoff/verify.py diff --git a/research/finite-width-call-mixing-tradeoff/README.md b/research/finite-width-call-mixing-tradeoff/README.md new file mode 100644 index 0000000000..af2a5b4023 --- /dev/null +++ b/research/finite-width-call-mixing-tradeoff/README.md @@ -0,0 +1,216 @@ +# Exact finite-width slice-call versus binary-addition tradeoff + +For one dense m-axis transform at width f, using at most s slice calls, +the exact minimum number of binary scalar additions is + +``` +A_min(m,f,s) = f*(m-s), m,f >= 1, 0 <= s <= m. +``` + +This is a scoped mathematical proof with exact finite corroboration. The +lower bound permits arbitrary monomial free operations. Attainment permits +permutations acting on individual digit columns, one zero helper, free copies +and free resets. Those are explicit assumptions of this resource model. +The tied-column engine of Jacob Alan Sussman's [PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628) +is a narrower model. The upper construction here is width-aware and does not +supply an upper construction in that engine. No new kappa is claimed. + +The first fixture is m=3, f=2, s=2. Two tied slice calls and two binary +additions attain the transform. One addition cannot suffice, regardless of +the number of zero helpers, free monomial maps, copies or resets. + +## Contract + +Put a=(1+i)/2, b=(1-i)/2 and C=a*I+b*X, where X exchanges the two basis +vectors. A register has coordinate space + +``` +V = (complex^(2^m))^(tensor f), dim V = 2^(mf). +K = (C^(tensor m))^(tensor f). +``` + +Index V by f columns of m binary address coordinates. For a +nonzero v in F2^m, X_v translates one address by v and a paid slice call is + +``` +(C_v)^(tensor f), C_v=a*I+b*X_v. +``` + +There are finitely many registers, with no fixed upper bound. One register +starts with arbitrary input x; all others start at zero. A program is a finite +straight-line sequence of input-independent linear operations. Its operations +are: + +- A paid slice call on one register, counted once per invocation. +- A binary scalar addition r := lambda*p + mu*q, counted once. Coefficients + are arbitrary fixed complex numbers, with no magnitude restriction. +- Free unary monomial maps, scalar multiplications, copies and resets to zero. + +A monomial map has one nonzero entry in every row and column. Its choice can +depend on m and f, but not on x. Free copies may create a register or overwrite +one; arbitrary-arity sums must be expressed using counted binary additions. +The output is K*x in the input register, with every helper returned to zero. +All call and addition costs include their use on helpers. There is no free +arbitrary scalar matrix mixing across registers and no nonzero advice input. +The program must be exact for every x at its stated finite width. + +The lower bound below also holds if helpers need not be returned. Attainment +uses one helper and the explicitly allowed resets; it does not restore an +arbitrary dirty helper or provide a reversible implementation of a reset. + +## Proof of the lower bound + +Fix any input basis column e_j. At the start, every register has support at +most one. Let p and q be the numbers of paid calls and binary additions so +far. By induction every register has support at most 2^(fp+q). + +A unary monomial map preserves support. Scaling, copying and resetting cannot +increase the largest support. An addition has support contained in the union +of its two inputs, so it increases the global support bound by a factor at +most two. Every column of C_v has two nonzero entries, so every column of its +f-fold tensor power has 2^f nonzero entries. Applying a paid call therefore +increases the support bound by a factor at most 2^f. Cancellations can only +reduce support. These observations prove the induction for any register and +any finite program, including singular mixing and erasures. + +Both a and b are nonzero. Every column of K consequently has exactly 2^(mf) +nonzero entries. An exact program with p calls and A additions must satisfy + +``` +2^(mf) <= 2^(fp+A), hence A >= f*(m-p). +``` + +If p<=s<=m, this implies A>=f*(m-s). This is a support argument over the +complex field, not a numerical approximation or a finite-search inference. +It is the quantitative resource consequence of the support method cited below. + +## Attainment in the width-aware model + +First apply one tied slice call C_(e_j)^(tensor f) for each of s distinct +coordinate axes j. These calls implement C on sf individual bits. + +For each remaining axis and each of the f columns, use the following four +steps. Let X_(j,c) flip that single address bit in that one column. + +``` +helper := input_register +helper := X_(j,c) * helper +input_register := a*input_register + b*helper +helper := 0 +``` + +The third step is one binary addition. Its action on the input register is +exactly C on the selected bit. All selected bit operators commute. After the +f*(m-s) iterations, every one of the mf bits has received C once, so the +complete endpoint is K*x with the helper zero. There is no input-dependent +control or free dense transform in the construction. + +The complete declared invoice is s paid calls, A=f*(m-s) binary additions, +A copies, A one-bit monomial permutations and A resets. The additions use two +free scalar multiplications apiece. No further workspace is needed. Thus the +lower bound is attained for every m,f,s in the theorem's domain. + +The uncharged monomial operations and resets are a formal resource assumption; +they do not describe a physical instruction invoice. In particular, individual +column flips are wider than the tied-column free-address operations in #4628. + +## Explicit width threshold + +A proposed all-width family with fixed s= floor(A/(m-s)) + 1. +``` + +The formula needs no bound on the number of free monomial maps or helpers. +It sharpens an eventual support-growth obstruction to an exact width/resource +tradeoff. For example, at m=3 and s=2, a budget of 17 binary additions cannot +work at width 18. At finite widths a zero-call construction is possible in +the wider model, but it uses exactly mf additions. A fixed program whose +addition count is independent of f cannot obtain that behavior at all widths. +The theorem gives no direct-sum lower bound for several independent outputs. + +## Evidence and reproduction + +The universal statements are the written proofs above. The standalone +standard-library checker corroborates bounded instances using Gaussian-integer +numerators with a common power-of-two denominator. It executes the copy, +permutation, addition and reset steps on every input basis column. An independent +closed Hamming-distance formula supplies each expected target column. It checks +both the complete output operator and the helper's zero endpoint. + +The 33 construction fixtures cover m=1..4, f=1..3, mf<=8 and every s=0..m, +with all 1,928 input basis columns checked. +A separate subset expansion tests all nonzero paid directions for m=1..3, +f=1..3, mf<=6, comprising 26 cases and 770 input columns. Eight invalid-input +controls and seven operation mutations reject, including omitted operations and +replacement of the required individual-column permutations by a tied flip. +The printed receipt enumerates the exact coverage, hashes the endpoint +transcript and binds all five package source files. `--emit-receipt` produces +JSON alone. Both modes write nothing; store any receipts outside the checkout. + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/finite-width-call-mixing-tradeoff +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/finite-width-call-mixing-tradeoff/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/finite-width-call-mixing-tradeoff/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/finite-width-call-mixing-tradeoff --check-source-history +``` + +The direct marker is `PASS_FINITE_WIDTH_CALL_MIXING_TRADEOFF no_new_kappa`. +Normal and optimized execution retain all checks through explicit exceptions. +The verifier needs neither Git, network access nor predecessor executables. +The metadata and source-history checks additionally use Git provenance. + +## Scope, provenance and implementation limits + +The original formal-interface-lemma card is changed to a written resource +lemma, with no proof-assistant formalization. The selected-source orientation +command passed on base a5df48c55ea806d7952b65acc9c76d878ff09b13, priority 7. +This is a side result about the cost hidden by free register mixing. It does +not resolve the small-saving cases listed in #4628 or change any selected input. + +The live overlap snapshot covered 333 open PRs and 4,362 Discussion records +with complete pagination. The sparse local scan covered 145 of 6,918 indexed +notes. Distinctive main-tree and merged-PR searches were also run. This coverage +does not establish novelty against unpublished work or arbitrary historical diffs. + +All verifier loops have fixed bounds. Vectors have at most 256 coordinates; +Gaussian exponents are at most eight, and each program has at most 32 steps. +No recursive call, external process, dynamic code loading or callback dispatch +is used. Functions fit within 60 physical lines. Python and its standard library +allocate managed objects during replay, a Power-of-Ten rule 3 deviation. The +fixed domains bound live vectors and integer sizes; runtime allocations are +not independently instrumented. Warning-strict normal and optimized replay +provide the configured diagnostics. No external static analyzer is configured. + +Independent human and formal proof-kernel review are unclaimed. There is no +physical tape, routing, precision, compiler or ownership implementation here; +no supplier admission, selected cold replay or complete multiplication theorem +is claimed. No kappa or selected-frontier change follows. + +## Open next questions + +- What is the exact finite-width addition/call tradeoff when every free address + permutation must act identically on every digit column? Start with m=2,f=2 + and identify which dense endpoints lie in the generated operator span. The + one-column shifts used for attainment here are forbidden in that model. +- What changes when the helper is arbitrary dirty data and every operation + must be reversible? Start with one unimplemented bit and derive a complete + return word. This construction's copies and resets cannot supply that word. + +## Credit + +This contribution is produced by Nick Petalas. Jacob Alan Sussman's #4628, +head ee4fd87f064017c23e5a86fc1dcfe0a5237caed3, supplies the all-width support +argument in [PROOF.md section 4](https://github.com/CrocSwap/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/PROOF.md) +and the width-one zero-scratch example. That argument and those certificates +are cited predecessors, not replayed deliverables. The new step is the exact +binary-addition resource law, its explicit first failing width and its sharp +width-aware construction. Support counting and the one-bit linear identity +are elementary methods; no literature-priority claim is made for them. +Credit eumemic #288 and Swapnil Jain for the retained subspace/call framework, +Jose Manuel #2108 for the scalar-mixing obstruction context, and the retained +register-model contributors. New material is Apache-2.0. diff --git a/research/finite-width-call-mixing-tradeoff/SOURCES.json b/research/finite-width-call-mixing-tradeoff/SOURCES.json new file mode 100644 index 0000000000..0f8de76a73 --- /dev/null +++ b/research/finite-width-call-mixing-tradeoff/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/abelian-cayley-metric-scope/sources/pr288-README.md", + "usage": "provenance", + "git_blob": "dc04f533bd0f3b185969bb259e876a73714f7285", + "sha256": "c091e98c415e2a80bb28402b789363eb97dd3492061ca8875e421ae437de7482" + }, + { + "path": "research/two-register-three-mix/README.md", + "usage": "provenance", + "git_blob": "593549db00fac1a10734868380eab28bcb584cc2", + "sha256": "3353fe948c75fbfc56841260db02d5e14aba966d157d3390fe3d4785e397af60" + } + ] +} diff --git a/research/finite-width-call-mixing-tradeoff/TASK.json b/research/finite-width-call-mixing-tradeoff/TASK.json new file mode 100644 index 0000000000..c989f4d103 --- /dev/null +++ b/research/finite-width-call-mixing-tradeoff/TASK.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the sharp one-output finite-width resource law A_min=f*(m-s) for at most s<=m tied slice calls and counted binary scalar additions, with width-aware monomial free operations and zero scratch.", + "scope_change_reason": "Original work replaces the card proof-assistant audit premise with a quantitative successor to Jacob Alan Sussman PR4628 section 4. The lower bound is general, while sharpness explicitly widens the tied-column free maps.", + "bottleneck_link": "A side resource result exposes the finite-width addition budget hidden by free register mixing; it supplies no actual supplier or multiplication exponent.", + "budget_minutes": 60, + "stop_rule": "Package the first proved exact tradeoff after bounded full-endpoint corroboration; do not pursue multiple outputs or physical lowering.", + "outcome": "completed", + "evidence": "README.md supplies the universal support proof and width-aware attaining construction. verify.py checks exact full columns, helper cleanup, tensor primitives and mutation controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Determine the exact tradeoff with tied-column free address permutations.", + "why_it_matters": "The wider free maps are required for the displayed attainment.", + "first_step": "Study m=2,f=2 and the generated operator span.", + "blocked_by": "Individual-column flips are forbidden." + }, + { + "question": "Determine the reversible tradeoff with arbitrary dirty helper input.", + "why_it_matters": "Zero resets do not implement dirty restoration.", + "first_step": "Construct or obstruct the complete return word for one remaining bit.", + "blocked_by": "The copied and erased helper is not arbitrary dirty input." + } + ], + "predecessor": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4628", + "head": "ee4fd87f064017c23e5a86fc1dcfe0a5237caed3", + "usage": "Cited mathematical context; no executable or external proof-relevant runtime input." + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "machine": "arm64", + "requirements": "standard library only", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144895" +} diff --git a/research/finite-width-call-mixing-tradeoff/VERIFY.json b/research/finite-width-call-mixing-tradeoff/VERIFY.json new file mode 100644 index 0000000000..a3d77c0452 --- /dev/null +++ b/research/finite-width-call-mixing-tradeoff/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 complete construction endpoints, zero helper, independent Hamming-distance target, subset-expanded tied calls, support invariants and operation/input rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact complete construction endpoints, zero helper, independent Hamming-distance target, subset-expanded tied calls, support invariants and operation/input rejection controls." + } + ] +} diff --git a/research/finite-width-call-mixing-tradeoff/verify.py b/research/finite-width-call-mixing-tradeoff/verify.py new file mode 100644 index 0000000000..af4c9cc01a --- /dev/null +++ b/research/finite-width-call-mixing-tradeoff/verify.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written resource law. Apache-2.0.""" +import argparse +import hashlib +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def parameters(m, f, s): + require(all(type(v) is int for v in (m, f, s)), "integer parameters required") + require(1 <= m <= 4 and 1 <= f <= 3, "outside finite replay domain") + require(m * f <= 8 and 0 <= s <= m, "invalid replay shape") + + +def gaussian_product(x, y): + a, b = x + c, d = y + return a*c-b*d, a*d+b*c + + +def gaussian_power(x, exponent): + require(0 <= exponent <= 8, "power outside replay bound") + result = (1, 0) + for _ in range(exponent): + result = gaussian_product(result, x) + return result + + +def combine(x, y): + """Compute a*x+b*y, with a=(1+i)/2 and b=(1-i)/2.""" + values, exponent = x + other, other_exponent = y + require(len(values) == len(other), "different vector lengths") + require(exponent == other_exponent, "different common denominators") + result = tuple((r-t+u+v, r+t+v-u) + for (r, t), (u, v) in zip(values, other)) + return result, exponent + 1 + + +def shift(state, mask): + values, exponent = state + require(0 < mask < len(values), "invalid XOR mask") + return tuple(values[j ^ mask] for j in range(len(values))), exponent + + +def paid(state, direction, m, f): + require(0 < direction < (1 << m), "invalid paid direction") + for column in range(f): + state = combine(state, shift(state, direction << (m * column))) + return state + + +def program(m, f, s): + parameters(m, f, s) + steps = [("paid", 1 << axis) for axis in range(s)] + for axis in range(s, m): + for column in range(f): + steps.extend((("copy", 0), ("shift", 1 << (m*column+axis)), + ("mix", 0), ("clear", 0))) + return tuple(steps) + + +def support(state): + return sum(value != (0, 0) for value in state[0]) + + +def execute(steps, m, f, input_column): + n = 1 << (m*f) + require(0 <= input_column < n, "invalid input column") + zero = ((0, 0),) * n + x = (tuple((int(j == input_column), 0) for j in range(n)), 0) + helper = (zero, 0) + calls = additions = 0 + for kind, operand in steps: + if kind == "paid": + x = paid(x, operand, m, f) + calls += 1 + elif kind == "copy": + require(support(helper) == 0, "copy requires zero helper") + helper = x + elif kind == "shift": + helper = shift(helper, operand) + elif kind == "mix": + x = combine(x, helper) + additions += 1 + elif kind == "clear": + helper = (zero, 0) + else: + raise ValueError("unknown instruction") + require(max(support(x), support(helper)) <= 1 << (f*calls+additions), + "support budget exceeded") + return x, helper, calls, additions + + +def reference(m, f, column): + bits = m*f + values = tuple(gaussian_product(gaussian_power((1, 1), bits-d), + gaussian_power((1, -1), d)) + for d in range(bits + 1)) + return tuple(values[(j ^ column).bit_count()] for j in range(1 << bits)), bits + + +def equal_states(x, y): + values, exponent = x + other, other_exponent = y + common = max(exponent, other_exponent) + return tuple((r << (common-exponent), t << (common-exponent)) + for r, t in values) == tuple( + (r << (common-other_exponent), t << (common-other_exponent)) + for r, t in other) + + +def construction_checks(): + digest = hashlib.sha256() + fixtures = columns = 0 + for m in range(1, 5): + for f in range(1, 4): + if m*f > 8: + continue + for s in range(m + 1): + steps = program(m, f, s) + fixtures += 1 + for column in range(1 << (m*f)): + x, helper, calls, additions = execute(steps, m, f, column) + require(equal_states(x, reference(m, f, column)), "wrong endpoint") + require(support(helper) == 0, "helper not returned to zero") + require(calls == s and additions == f*(m-s), "wrong invoice") + require(support(x) == 1 << (m*f), "target is not dense") + digest.update(repr((m, f, s, column, x)).encode()) + columns += 1 + return fixtures, columns, digest.hexdigest() + + +def tensor_reference(m, f, direction, column): + n = 1 << (m*f) + values = [(0, 0)] * n + for subset in range(1 << f): + index = column + for digit in range(f): + if (subset >> digit) & 1: + index ^= direction << (m*digit) + d = subset.bit_count() + require(values[index] == (0, 0), "tensor paths collided") + values[index] = gaussian_product(gaussian_power((1, 1), f-d), + gaussian_power((1, -1), d)) + return tuple(values), f + + +def tensor_checks(): + cases = columns = 0 + for m in range(1, 4): + for f in range(1, 4): + if m*f > 6: + continue + n = 1 << (m*f) + for direction in range(1, 1 << m): + cases += 1 + for column in range(n): + state = (tuple((int(j == column), 0) for j in range(n)), 0) + actual = paid(state, direction, m, f) + require(equal_states(actual, tensor_reference(m, f, direction, column)), + "paid tensor differs from subset expansion") + require(support(actual) == 1 << f, "wrong paid support") + columns += 1 + return cases, columns + + +def rejection_checks(): + cases = ((0, 2, 0), (3, 0, 0), (3, 2, -1), (3, 2, 4), + (True, 2, 0), (2, 1.5, 0), (4, 3, 0), (5, 1, 1)) + count = 0 + for args in cases: + try: + program(*args) + except ValueError: + count += 1 + else: + raise ValueError("invalid shape accepted") + return count + + +def mutation_checks(): + m, f, s = 3, 2, 2 + steps = program(m, f, s) + rejected = 0 + for index, (kind, _) in enumerate(steps): + if kind not in ("paid", "mix", "clear"): + continue + mutant = steps[:index] + steps[index+1:] + wrong = False + for column in range(1 << (m*f)): + try: + x, helper, _, _ = execute(mutant, m, f, column) + wrong |= not equal_states(x, reference(m, f, column)) or support(helper) != 0 + except ValueError: + wrong = True + require(wrong, "single-operation mutant survived") + rejected += 1 + wrong_masks = tuple((kind, (1 << 2) | (1 << 5)) if kind == "shift" else (kind, v) + for kind, v in steps) + x, _, _, _ = execute(wrong_masks, m, f, 0) + require(not equal_states(x, reference(m, f, 0)), "tied-mask mutant survived") + return rejected + 1 + + +def receipt(): + fixtures, columns, digest = construction_checks() + tensor_cases, tensor_columns = tensor_checks() + result = {"claim_type": "scoped proof with finite corroboration", + "construction_fixtures": fixtures, "full_input_columns": columns, + "endpoint_sha256": digest, "paid_tensor_cases": tensor_cases, + "paid_tensor_input_columns": tensor_columns, + "input_rejections": rejection_checks(), + "mutation_rejections": mutation_checks(), "no_new_kappa": True} + root = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["source_sha256"] = {} + for name in names: + data = (root / name).read_bytes() + require(len(data) <= 262144, "package file exceeds receipt bound") + result["source_sha256"][name] = hashlib.sha256(data).hexdigest() + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + result = receipt() + if not args.emit_receipt: + print("PASS_FINITE_WIDTH_CALL_MIXING_TRADEOFF no_new_kappa") + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()