diff --git a/research/compact-two-target-translation-minimum/PROOF.md b/research/compact-two-target-translation-minimum/PROOF.md new file mode 100644 index 0000000000..a36d169086 --- /dev/null +++ b/research/compact-two-target-translation-minimum/PROOF.md @@ -0,0 +1,137 @@ +# Five translations are necessary for the actual invariant agreement set + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Fixed interface and claim + +Take two target blocks, each consisting of one low target bit followed by a +five-bit window. Write + + y = b0 + 2 W0 + 64 b1 + 128 W1, 0 <= y < 4096, + u = u0 + 8 u1, t = t0 + 8 t1, 0 <= u,t < 64. + +Each control digit is in 0..7, each window in 0..31, and each b is a bit. +All complete fields are modular at exactly these widths. Both constant source +bits are one. There are no other fields. The desired endpoint is + + T(u,t,y) = (u,t,y XOR 65). + +Use the two-subcall macro of Benny Zhao's PR6812. In each four-update subcall, +z_i is the parity of the current u digit and p_i=64^i. Its updates are + + y += sum_i 2 z_i t_i p_i modulo 4096; + t += sum_i b_i(y) 8^i modulo 64; + y += sum_i z_i (1 - 2 t_i) p_i modulo 4096; + t -= sum_i (b_i(y) XOR z_i) 8^i modulo 64. + +Every read uses the current field after the preceding update. Between the +subcalls add 9 to u; after the second subcall subtract 9. Call the complete +raw map S. The source constants need no transport under data translation. +This is the fixed logical word, not a priced implementation of constant XOR. + +An allowed translation adds independent constants modulo the periods of the +six coordinates u0,u1,t0,t1,W0,W1. It leaves b0,b1 unchanged. A menu entry D +runs D^-1 S D. A selector sigma must satisfy sigma(Tx)=sigma(x), so its +record can be recomputed from the returned state. No other selector memory +or cleanup mechanism is included. + +**Result.** The least number of entries in such a menu, correct on every +state with an invariant selector, is five. This is a finite operator +certificate combined with a written proof covering every menu of this form. +It is not an all-parameter theorem or a complete multiplication theorem. + +## Exact maximal invariant agreement core + +Let A={x:Sx=Tx}. Since T is an involution, the largest T-invariant subset of +A is G=A intersect T(A). Indeed, invariant H contained in A implies both x +and Tx belong to A whenever x belongs to H. Conversely G is T-invariant. +On G, S=T, so it is also invariant under the restricted raw execution. +This elementary core construction is prior agreement/guard methodology. + +The finite certificate in verify.py establishes the following exact equality +on **all 16,777,216 states**, without assuming that either subcall is exact: + + G = { u0 < 7, t0 < 7, t1 < 7, W0 + t0 < 32 }. (1) + +The certificate directly enumerates all 64*64*4096 complete inputs and checks +Sx and, whenever Sx=Tx, S(Tx). It finds 11,441,280 raw agreement states and +10,185,728 core states. A second digit-vector implementation checks both +executions on all 131,072 representatives with u1 in {0,1} and W1=0, +including all target parities. It finds 89,385 raw agreements and 79,576 core +states there. The full enumeration independently checks every lift, so the +proof does not depend on extrapolating these representative counts. + +One cannot use A in place of G. For example S(0,7,0)=(0,7,65), whereas +S(0,7,65)=(0,7,3984). The first point agrees but its T-mate does not. + +Every allowed D commutes with T. Thus an invariant selector can choose entry +D on the orbit {x,Tx} exactly when Dx belongs to G. By (1), only translations +of (u0,t0,t1,W0) matter. Arbitrary additional u1 or W1 translations do not +alter the following argument. + +## Adversary for every four-entry menu + +Write entry j's four relevant constants as (a_j,b_j,c_j,d_j), with periods +(8,8,8,32). Repeated entries are allowed. Pad any shorter nonempty menu to +four entries by repeating its last entry. + +Choose an ordering C,D of entries 0,1 such that + + b_D - b_C is not 1 modulo 8. + +Such an ordering always exists: if one difference is 1, the reverse difference +is 7. Set the original coordinates to + + u0 = 7-a_2 modulo 8, + t1 = 7-c_3 modulo 8, + t0 = 7-b_C modulo 8. + +Entry 2 now fails u0<7, entry 3 fails t1<7, and entry C fails t0<7. +Let v=(t0+b_D) modulo 8. The choice of C,D ensures v is nonzero. Finally set + + W0 = 32-v-d_D modulo 32. + +After entry D's translation, W0=32-v lies in 25..31, so W0+t0=32 and (1) +fails. Hence none of the four entries contains this T-orbit in its agreement +core. No invariant selector can choose an entry on that orbit. This proves +the lower bound for arbitrary constants, not just a searched menu family. + +The executable adversary checks every one of the 4,096 t0-shift profiles, +with deterministic varied constants in the other coordinates, and checks +their generated witnesses against the separate literal interpreter. Those +fixtures corroborate the formula; the argument above supplies the quantifier +over all other coordinate constants. It does not claim an enumeration of +all four-entry menus. + +## Attaining five entries + +Take, for k=0..4, + + (a_k,b_k,c_k,d_k) = (k,k,k,6k), + +and leave u1,W1 unchanged. This is the r=2 specialization of PR6812's +attaining menu. Its sufficient product guard is contained in (1). +Each of the three guarded control coordinates can exclude at most one phase. +For the lower window, the five bad preimage intervals have length six and +are disjoint in a 32-value period, since 5*6<=32. Thus the window excludes +at most one phase. Five phases cannot all be excluded by four coordinates. + +The verifier checks coverage directly using (1) on all 16,384 tuples of the +four relevant restored coordinates. Selecting the least good phase is +T-invariant because these coordinates are all restored by T. On that phase, +D^-1 S D=T by the exact core certificate. Five entries therefore suffice. + +The predecessor proves sufficiency and minimality for its *product guard*. +The new step is that even the actual, larger invariant agreement core cannot +reduce this two-target menu to four entries. + +## Boundaries and next direction + +The lower bound needs the fixed radix, windows, all-one source, raw word, +coordinate-translation alphabet, and invariant-selector contract above. +It does not constrain arbitrary changed words, coordinate mixing, larger +menus chosen with non-invariant retained records, other source functions, +other widths, or physical selector costs. A smaller menu must change at +least one of these hypotheses. No selected assumption is discharged and no +new kappa is supplied. Independent human and formal proof-kernel review are +unclaimed. diff --git a/research/compact-two-target-translation-minimum/README.md b/research/compact-two-target-translation-minimum/README.md new file mode 100644 index 0000000000..c9b520c6d4 --- /dev/null +++ b/research/compact-two-target-translation-minimum/README.md @@ -0,0 +1,114 @@ +# The actual two-target agreement core still needs five translations + +This contribution was produced by Nick Petalas. Apache-2.0. + +For the compact two-target switch with radix 8, two five-bit windows and +constant source pair (1,1), the exact minimum coordinate-translation menu +with an endpoint-invariant selector is **five**. Four entries fail even if +they exploit every actual invariant agreement state, rather than just the +sufficient product guard of Benny Zhao / zhaobenny's +[PR6812](https://github.com/CrocSwap/integer-mult-bounds/pull/6812). + +This answers one bounded instance of that package's Open next question 2. +The contribution is a sharp negative result, with a finite certificate and +a written combinatorial proof. The five-entry upper construction is credited +prior work. No new physical implementation or kappa is claimed. + +[PROOF.md](PROOF.md) defines every field, update, translation and selector. +For the raw macro S and desired involution T, its exact maximal invariant +agreement core is + + u0 < 7, t0 < 7, t1 < 7, W0+t0 < 32. + +The verifier directly enumerates all 16,777,216 complete states. It finds +11,441,280 raw agreement states and 10,185,728 core states. A separate +digit-vector engine agrees on all 131,072 quotient representatives. +An explicit adversary defeats any four-entry menu with arbitrary coordinate +constants. Five entries cover all 16,384 relevant coordinate tuples. + +Raw agreement alone is insufficient for a selector that must be recomputed +after return. The certificate includes an agreement point whose endpoint +mate fails, four isolated core-clause omissions, all 4,096 lower-temporary +shift profiles for the adversary, short-menu fixtures and invalid-menu checks. +It does not claim to enumerate all four-entry menus. + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/compact-two-target-translation-minimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/compact-two-target-translation-minimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/compact-two-target-translation-minimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/compact-two-target-translation-minimum --check-source-history +``` + +Substitute another CPython 3.12 executable elsewhere. The direct verifier +prints generated JSON containing `PASS_COMPACT_TWO_TARGET_TRANSLATION_MINIMUM` +and SHA256 hashes of the package files. It writes no files by default. +`--receipt /new/path.json` writes an exclusive new receipt and refuses to +overwrite an existing file. Normal and optimized modes retain all checks. +Predecessor text is pinned as historical provenance; no predecessor code is +imported or replayed. [VERIFY.json](VERIFY.json) registers both direct modes. +Local verification used CPython 3.12.15 on macOS 27.0.1 arm64. + +## Scope and limitations + +The controls have exactly two base-eight digits each. The data field has +exactly twelve bits, containing two target/window blocks. Every dirty value +at these widths is covered. Translations add constants independently modulo +each digit or window period and leave target bits unchanged. The selector +must be unchanged by the desired endpoint. Whole-field rotations with +cross-digit carries, coupled coordinate maps and extra selector-cleanup +state are outside this alphabet. + +This changed scope of `uniform-transfer-audit` is a logical interface side +result motivated by compact-switch exceptional repair. It settles no +selected all-size assumption. Native realization, physical translations, +selection, source evaluation, tape/precision, hosting, restoration invoices, +compiler closure and analytic transfer remain unpriced or unproved here. +No selected cold replay, predecessor scientific suite, Lean or Docker run +is supplied. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. Does the five-entry lower bound survive other radices and window widths? + This would distinguish a fixed finite obstruction from a family-wide one. + First derive a symbolic invariant-core formula for the same all-one + two-target word. The finite classification here does not prove that formula. +2. Can a changed translation alphabet or selector cleanup beat five entries + at this same geometry? First give a concrete coupled map or a retained + non-invariant selector contract and charge its cleanup. Physical costs and + a legal implementation remain blockers. + +## Credit and provenance + +Benny Zhao / zhaobenny's PR6812 supplies the composed terminal-carry interface, +the open raw-agreement cover question and the five-entry sufficient menu. +John-Michael Smith / PR763 and Hanson Sun / PR1219 and PR1247 supply the +terminal carry and highest-window cancellation lineage. Nick Petalas's +older PR6231 supplies the coordinate-translation interface and conservative +cover. Arham Tahir / PR1603, Aaron Wang / PR1823 and woklerx / PR1856 supply +the invariant-guard and full-modulus agreement methodology. Douglas Colkitt, +Sagar Thakrar, unpaidmoon, Cinna Davis, Hiroki KUMAZAKI and Ryanson Jonathan +retain the compact-switch and arbitrary-source lineage credited in PR6812. +The exact fixed-geometry core, four-menu adversary and new verifier are the +contribution here. [SOURCES.json](SOURCES.json) pins the source text and the +assignment at main e54523517d0f03e58352e647c403a5af3e525a57. + +## Verifier bounds + +The largest loop enumerates exactly 64*64*4096 states; each raw evaluation +has two subcalls. The second engine covers exactly 131,072 representatives, +and the remaining loops have the fixed bounds stated above. No recursion, +network, subprocess, dynamic code generation or unbounded work queue is used. +Functions stay below sixty physical lines. Explicit exceptions enforce the +mathematical checks in normal and optimized Python. + +Power of Ten rule 3 has a managed-runtime deviation: Python allocates integers, +tuples and JSON objects during execution. The full-domain scan keeps constant +live state; the remaining bounded collections have at most 4,096 profiles +visited sequentially, five phases, six invalid fixtures and six package files. +The runtime's internal allocator is not statically controlled. The fixed +domains and warning-strict registered runs are the compensating controls. +A native fixed-storage implementation would be needed to remove this deviation. diff --git a/research/compact-two-target-translation-minimum/SOURCES.json b/research/compact-two-target-translation-minimum/SOURCES.json new file mode 100644 index 0000000000..f4a613e783 --- /dev/null +++ b/research/compact-two-target-translation-minimum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/terminal-carry-guard-cover/PROOF.md", + "usage": "provenance", + "git_blob": "3dc4c0be7f6d0166407ba1bf27e5bf176f784a6f", + "sha256": "80833edf2a4796c07eb7b1be993e7dfe87123f13f6f8bc0d25c73a800cbc96f3" + }, + { + "path": "research/terminal-carry-guard-cover/README.md", + "usage": "provenance", + "git_blob": "256d400130f3d961b3834aa96806bc055ca6dff0", + "sha256": "9e62f7a02ca23d89fb6350b77109ae1459add3706a1283f805213d8d43de14cf" + } + ] +} diff --git a/research/compact-two-target-translation-minimum/TASK.json b/research/compact-two-target-translation-minimum/TASK.json new file mode 100644 index 0000000000..dda935fe97 --- /dev/null +++ b/research/compact-two-target-translation-minimum/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact invariant agreement core and sharp five-entry coordinate-translation minimum for the two-target B=8, five-bit-window, all-one-source compact switch.", + "scope_change_reason": "Take the raw-agreement cover question in zhaobenny PR6812, rather than audit a selected all-size assumption. This is a finite logical-interface side result.", + "bottleneck_link": "Compact-switch exceptional repair and selector cleanup can only improve if a cheaper complete logical interface exists. The actual invariant agreement set does not reduce this fixed five-entry menu.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original result; package the fixed-geometry core and sharp four-menu obstruction without extending to other parameters.", + "outcome": "negative-result", + "evidence": "PROOF.md and both independent arithmetic engines in verify.py; full enumeration and a constructive menu adversary.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the same minimum hold for other radices and window widths?", + "why_it_matters": "A family theorem would distinguish the finite obstruction from a universal one in this word.", + "first_step": "Derive a symbolic invariant-core formula for two all-one sources.", + "blocked_by": "No all-parameter core proof is supplied." + }, + { + "question": "Can coupled translations or a non-invariant retained selector beat five entries?", + "why_it_matters": "The exact fixed-alphabet minimum identifies hypotheses a smaller menu must change.", + "first_step": "Specify one changed map or selector-cleanup contract at the same geometry.", + "blocked_by": "Physical implementation and cleanup costs are unknown." + } + ] +} diff --git a/research/compact-two-target-translation-minimum/VERIFY.json b/research/compact-two-target-translation-minimum/VERIFY.json new file mode 100644 index 0000000000..efe26f4569 --- /dev/null +++ b/research/compact-two-target-translation-minimum/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": 300, + "checks": "Complete 16,777,216-state invariant-core classification, separate 131,072-state engine, five-cover enumeration, constructive four-menu adversary and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same exact finite certificate and controls with optimized Python." + } + ] +} diff --git a/research/compact-two-target-translation-minimum/verify.py b/research/compact-two-target-translation-minimum/verify.py new file mode 100644 index 0000000000..8d9ba18f47 --- /dev/null +++ b/research/compact-two-target-translation-minimum/verify.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Exact two-target invariant-agreement and translation certificate. Apache-2.0.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def raw(u, t, y): + """Fixed B=8, two 6-bit data blocks, constant source pair (1,1).""" + for step in range(2): + z0, z1 = u % 2, (u // 8) % 2 + y = (y + 2*z0*(t % 8) + 128*z1*(t // 8)) % 4096 + t = (t + y % 2 + 8*((y // 64) % 2)) % 64 + y = (y + z0*(1-2*(t % 8)) + 64*z1*(1-2*(t // 8))) % 4096 + t = (t - ((y % 2) ^ z0) - 8*(((y // 64) % 2) ^ z1)) % 64 + if step == 0: + u = (u + 9) % 64 + return (u - 9) % 64, t, y + + +def literal(u, t, y): + """Separate packed-update implementation using explicit digit vectors.""" + for step in range(2): + parity = [(u // (8**i)) % 2 for i in range(2)] + temporary = [(t // (8**i)) % 8 for i in range(2)] + increment = sum(2*parity[i]*temporary[i]*(64**i) for i in range(2)) + y = (y + increment) % 4096 + target = [(y // (64**i)) % 2 for i in range(2)] + t = (t + sum(target[i]*(8**i) for i in range(2))) % 64 + live = [(t // (8**i)) % 8 for i in range(2)] + increment = sum(parity[i]*(1-2*live[i])*(64**i) for i in range(2)) + y = (y + increment) % 4096 + target = [(y // (64**i)) % 2 for i in range(2)] + t = (t - sum((target[i] ^ parity[i])*(8**i) for i in range(2))) % 64 + if step == 0: + u = (u + 1 + 8) % 64 + return (u - 1 - 8) % 64, t, y + + +def core(x): + a, b, c, w = x + return a < 7 and b < 7 and c < 7 and w + b < 32 + + +def translate(x, shift): + return tuple((v+d) % period for v, d, period in zip(x, shift, (8, 8, 8, 32))) + + +def validate_menu(menu): + if not isinstance(menu, (list, tuple)) or not 1 <= len(menu) <= 5: + raise ValueError("menu needs one through five entries") + for row in menu: + if not isinstance(row, (list, tuple)) or len(row) != 4: + raise ValueError("translation needs four coordinates") + if any(type(v) is not int or not 0 <= v < p + for v, p in zip(row, (8, 8, 8, 32))): + raise ValueError("noncanonical translation coordinate") + + +def defeat_four(menu): + """Return one restored-coordinate orbit missed by an arbitrary short menu.""" + validate_menu(menu) + if len(menu) > 4: + raise ValueError("four-entry adversary does not cover five entries") + rows = list(menu) + [menu[-1]]*(4-len(menu)) + c, d = (0, 1) if (rows[1][1]-rows[0][1]) % 8 != 1 else (1, 0) + t0 = (7-rows[c][1]) % 8 + td = (t0+rows[d][1]) % 8 + require(td != 0, "ordered-pair choice must leave a nonzero digit") + witness = ((7-rows[2][0]) % 8, t0, (7-rows[3][2]) % 8, + (32-td-rows[d][3]) % 32) + require(all(not core(translate(witness, row)) for row in rows), + "adversary must defeat every entry") + return witness + + +def quotient_check(): + counts = {"quotient_states": 0, "quotient_agreement": 0, "quotient_core": 0} + for u0, z1, t0, t1, w, b0, b1 in itertools.product( + range(8), range(2), range(8), range(8), range(32), range(2), range(2)): + u, t, y = u0+8*z1, t0+8*t1, b0+2*w+64*b1 + first, second = literal(u, t, y), literal(u, t, y ^ 65) + require(first == raw(u, t, y) and second == raw(u, t, y ^ 65), + "independent packed-update disagreement") + agreement = first == (u, t, y ^ 65) + invariant = agreement and second == (u, t, y) + require(invariant == core((u0, t0, t1, w)), "exact core classification") + counts["quotient_states"] += 1 + counts["quotient_agreement"] += agreement + counts["quotient_core"] += invariant + return counts + + +def full_check(): + counts = {"full_states": 0, "full_agreement": 0, "full_core": 0} + for u, t in itertools.product(range(64), repeat=2): + for y in range(4096): + agreement = raw(u, t, y) == (u, t, y ^ 65) + invariant = agreement and raw(u, t, y ^ 65) == (u, t, y) + require(invariant == core((u % 8, t % 8, t // 8, (y // 2) % 32)), + "full-field core classification") + counts["full_states"] += 1 + counts["full_agreement"] += agreement + counts["full_core"] += invariant + return counts + + +def cover_check(): + menu = [(k, k, k, 6*k) for k in range(5)] + validate_menu(menu) + selected = [0]*5 + for x in itertools.product(range(8), range(8), range(8), range(32)): + phases = [k for k, row in enumerate(menu) if core(translate(x, row))] + require(bool(phases), "five entries must cover every restored-coordinate orbit") + selected[phases[0]] += 1 + require(sum(selected) == 16384, "complete coordinate domain") + return {"upper_menu": menu, "least_phase_counts": selected, + "covered_coordinate_tuples": sum(selected)} + + +def adversary_check(): + count = 0 + for digits in itertools.product(range(8), repeat=4): + # Every t0-translation profile, with varied other coordinates. + seed = sum(v*(8**i) for i, v in enumerate(digits)) + menu = [((seed+3*i) % 8, digits[i], (seed//8+5*i) % 8, + (seed//64+7*i) % 32) for i in range(4)] + witness = defeat_four(menu) + for row in menu: + a, b, c, w = translate(witness, row) + u, t, y = a, b+8*c, 2*w + require(not (literal(u, t, y) == (u, t, y ^ 65) + and literal(u, t, y ^ 65) == (u, t, y)), + "adversary must fail the actual invariant endpoint") + count += 1 + for size in range(1, 4): + defeat_four([(0, 0, 0, 0)]*size) + return {"all_t0_shift_profiles": count, "short_menu_fixtures": 3} + + +def rejection_controls(): + fixtures = [(7, 0, 0, 0), (0, 7, 0, 0), (0, 0, 7, 0), (0, 1, 0, 31)] + for omitted, x in enumerate(fixtures): + a, b, c, w = x + clauses = (a < 7, b < 7, c < 7, w+b < 32) + require(all(v for i, v in enumerate(clauses) if i != omitted), + "clause-omission fixture must isolate its clause") + u, t, y = a, b+8*c, 2*w + require(not (raw(u, t, y) == (u, t, y ^ 65) + and raw(u, t, y ^ 65) == (u, t, y)), "omission must fail") + require(raw(0, 7, 0) == (0, 7, 65) + and raw(0, 7, 65) != (0, 7, 0), "agreement is not an invariant guard") + invalid = [[], [(0, 0, 0)], [(True, 0, 0, 0)], [(8, 0, 0, 0)], + [(0, 0, 0, 32)], [(0, 0, 0, 0)]*6] + for menu in invalid: + try: + validate_menu(menu) + except ValueError: + continue + raise ValueError("invalid menu accepted") + try: + defeat_four([(0, 0, 0, 0)]*5) + except ValueError: + return {"clause_omissions": 4, "agreement_without_invariance": 1, + "invalid_menus": len(invalid), "five_entry_adversary_rejected": 1} + raise ValueError("adversary improperly accepted a five-entry menu") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write new receipt, never overwrite") + args = parser.parse_args() + result = {"status": "PASS_COMPACT_TWO_TARGET_TRANSLATION_MINIMUM", + "claim_type": "finite certificate and scoped combinatorial proof", + "geometry": {"B": 8, "window_values": 32, "source": [1, 1], + "control_modulus": 64, "data_modulus": 4096}, + "minimum_invariant_translation_menu": 5} + result.update(quotient_check()) + result.update(full_check()) + result.update(cover_check()) + result.update(adversary_check()) + result["controls"] = rejection_controls() + require(result["full_states"] == 16777216, "complete full-field enumeration") + require(result["full_core"] == 128*result["quotient_core"], "quotient lifting") + package = Path(__file__).resolve().parent + files = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + result["package_sha256"] = {} + for name in files: + path = package / name + require(path.stat().st_size <= 1048576, "bounded package source file") + result["package_sha256"][name] = hashlib.sha256(path.read_bytes()).hexdigest() + encoded = json.dumps(result, sort_keys=True, indent=2)+"\n" + if args.receipt: + with args.receipt.open("x", encoding="utf-8") as output: + output.write(encoded) + print(encoded, end="") + + +if __name__ == "__main__": + main()