diff --git a/research/f3-five-source-connector/CERTIFICATE.json b/research/f3-five-source-connector/CERTIFICATE.json new file mode 100644 index 0000000000..ea7193655b --- /dev/null +++ b/research/f3-five-source-connector/CERTIFICATE.json @@ -0,0 +1,612 @@ +{ + "schema_version": 1, + "field": 3, + "source_word": [ + 0, + 4, + 4, + 0, + 0, + 1, + 3, + 2, + 2, + 1, + 3, + 3, + 4, + 2, + 1 + ], + "readouts": { + "1": [ + 0, + 0, + 1 + ], + "2": [ + 0, + 14, + 14 + ], + "3": [ + 0, + 2, + 6 + ], + "4": [ + 5, + 9, + 11 + ], + "5": [ + 3, + 9, + 11 + ], + "6": [ + 0, + 13, + 13 + ], + "7": [ + 1, + 13, + 13 + ], + "8": [ + 5, + 8, + 12 + ], + "9": [ + 2, + 7, + 14 + ], + "10": [ + 3, + 4, + 7 + ], + "11": [ + 0, + 2, + 7 + ], + "12": [ + 5, + 9, + 12 + ], + "13": [ + 2, + 8, + 14 + ], + "14": [ + 3, + 4, + 8 + ], + "15": [ + 0, + 2, + 8 + ], + "16": [ + 0, + 3, + 4 + ], + "17": [ + 0, + 0, + 2 + ], + "18": [ + 0, + 5, + 6 + ], + "19": [ + 0, + 3, + 6 + ], + "20": [ + 0, + 9, + 11 + ], + "21": [ + 1, + 9, + 11 + ], + "22": [ + 0, + 10, + 11 + ], + "23": [ + 1, + 10, + 11 + ], + "24": [ + 0, + 8, + 12 + ], + "25": [ + 1, + 8, + 12 + ], + "26": [ + 0, + 5, + 7 + ], + "27": [ + 0, + 3, + 7 + ], + "28": [ + 0, + 9, + 12 + ], + "29": [ + 1, + 9, + 12 + ], + "30": [ + 0, + 5, + 8 + ], + "31": [ + 0, + 3, + 8 + ] + }, + "word": [ + [ + "A", + 1 + ], + [ + "A", + 1 + ], + [ + "A", + 2 + ], + [ + "A", + 3 + ], + [ + "A", + 6 + ], + [ + "A", + 11 + ], + [ + "A", + 15 + ], + [ + "A", + 16 + ], + [ + "A", + 17 + ], + [ + "A", + 17 + ], + [ + "A", + 18 + ], + [ + "A", + 19 + ], + [ + "A", + 20 + ], + [ + "A", + 22 + ], + [ + "A", + 24 + ], + [ + "A", + 26 + ], + [ + "A", + 27 + ], + [ + "A", + 28 + ], + [ + "A", + 30 + ], + [ + "A", + 31 + ], + [ + "B", + 0 + ], + [ + "A", + 1 + ], + [ + "A", + 7 + ], + [ + "A", + 21 + ], + [ + "A", + 23 + ], + [ + "A", + 25 + ], + [ + "A", + 29 + ], + [ + "B", + 4 + ], + [ + "A", + 3 + ], + [ + "A", + 9 + ], + [ + "A", + 11 + ], + [ + "A", + 13 + ], + [ + "A", + 15 + ], + [ + "A", + 17 + ], + [ + "B", + 4 + ], + [ + "A", + 5 + ], + [ + "A", + 10 + ], + [ + "A", + 14 + ], + [ + "A", + 16 + ], + [ + "A", + 19 + ], + [ + "A", + 27 + ], + [ + "A", + 31 + ], + [ + "B", + 0 + ], + [ + "A", + 10 + ], + [ + "A", + 14 + ], + [ + "A", + 16 + ], + [ + "B", + 0 + ], + [ + "A", + 4 + ], + [ + "A", + 8 + ], + [ + "A", + 12 + ], + [ + "A", + 18 + ], + [ + "A", + 26 + ], + [ + "A", + 30 + ], + [ + "B", + 1 + ], + [ + "A", + 3 + ], + [ + "A", + 18 + ], + [ + "A", + 19 + ], + [ + "B", + 3 + ], + [ + "A", + 9 + ], + [ + "A", + 10 + ], + [ + "A", + 11 + ], + [ + "A", + 26 + ], + [ + "A", + 27 + ], + [ + "B", + 2 + ], + [ + "A", + 8 + ], + [ + "A", + 13 + ], + [ + "A", + 14 + ], + [ + "A", + 15 + ], + [ + "A", + 24 + ], + [ + "A", + 25 + ], + [ + "A", + 30 + ], + [ + "A", + 31 + ], + [ + "B", + 2 + ], + [ + "A", + 4 + ], + [ + "A", + 5 + ], + [ + "A", + 12 + ], + [ + "A", + 20 + ], + [ + "A", + 21 + ], + [ + "A", + 28 + ], + [ + "A", + 29 + ], + [ + "B", + 1 + ], + [ + "A", + 22 + ], + [ + "A", + 23 + ], + [ + "B", + 3 + ], + [ + "A", + 4 + ], + [ + "A", + 5 + ], + [ + "A", + 20 + ], + [ + "A", + 21 + ], + [ + "A", + 22 + ], + [ + "A", + 23 + ], + [ + "B", + 3 + ], + [ + "A", + 8 + ], + [ + "A", + 12 + ], + [ + "A", + 24 + ], + [ + "A", + 25 + ], + [ + "A", + 28 + ], + [ + "A", + 29 + ], + [ + "B", + 4 + ], + [ + "A", + 6 + ], + [ + "A", + 6 + ], + [ + "A", + 7 + ], + [ + "A", + 7 + ], + [ + "B", + 2 + ], + [ + "A", + 2 + ], + [ + "A", + 2 + ], + [ + "A", + 9 + ], + [ + "A", + 13 + ], + [ + "B", + 1 + ] + ] +} diff --git a/research/f3-five-source-connector/README.md b/research/f3-five-source-connector/README.md new file mode 100644 index 0000000000..3b1b32555f --- /dev/null +++ b/research/f3-five-source-connector/README.md @@ -0,0 +1,201 @@ +# Exact unsigned F3 five-source connector optimum + +This package proves an exact **108 complete-call optimum** for five immutable +sources and all 31 nonzero binary-mask outputs over F3. Every one of the 36 +operators is used exactly three times. Consequently, for any independently +positive fixed complete-call prices, the exact map-call bill is + +```text +3 sum_(j=0..4) c_Bj + 3 sum_(m=1..31) c_Am. +``` + +This is a scoped proof with an explicit finite certificate. It answers the +five-source open question in [#4189](https://github.com/CrocSwap/integer-mult-bounds/pull/4189), +at head `5fb3936dfc8082f438f21c72dd6ca49ff4366ae7`. It is a new batch construction, +not an independent recheck of that contribution's six-call one-source result. +There is no new kappa or selected-frontier change. + +## Exact boundary + +All 37 length-L rows are arbitrary and distinct: five read-only sources x_j, +31 output rows y_m, and one borrowed dirty connector z. For arbitrary F3-linear +maps B_j and A_m of compatible dimension, implement + +```text +y_m += sum_(j: bit_j(m)=1) A_m B_j x_j, m = 1,...,31; +x_j and z unchanged. +``` + +The only operations are unsigned complete calls +`B_j: z += B_j x_j` and `A_m: y_m += A_m z`. Source and coefficient rows are +immutable. Each call preserves other rows, restores its private scratch and +heads, and has action independent of its old target. Data rows are excluded +from private scratch. Outputs are unobserved until completion. +No signed call, direct product, connector scaling, extra connector, mutable +source, frame change, free copy or overwrite is admitted. The maps may be +singular and need not commute. The theorem is uniform in L and these maps, +within this abstract complete-call contract. + +The characteristic-two prefix-difference construction in Ross Richardson's +[#943](../universal-connector-boundary/README.md) has a different field and +cost. Its 74-call number is not an F3 lower bound. Sagar Thakrar's +[#1349](https://github.com/CrocSwap/integer-mult-bounds/pull/1349) allows signed +calls and studies a three-by-three signed target, a different interface. + +## Lower bound over every finite legal word + +Specialize to scalar identity maps and keep the five source scalars and the +initial connector scalar z0 independent. If B_j occurs b_j times, the final +coefficient of x_j in z is b_j modulo three. Restoration forces `3 | b_j`. +If A_m occurs a_m times, the coefficient of z0 added to y_m is a_m modulo +three, since B calls never change that coefficient of z. Removing connector +dirt forces `3 | a_m`. + +Each A_m must occur at least once because its requested row is nonzero. Each +B_j must occur at least once because the singleton output for j depends on +x_j, and B_j is the only operation that can transmit x_j to an output. +Thus every one of the 36 counts is at least three. Every legal generic word +has at least 108 calls, and its positive fixed-price bill is at least the +displayed formula. This argument does not impose a word-length search cap. + +## Attaining word and triple-prefix identity + +Project a word onto its B events. Let q_t be the five source-call counts, +modulo three, after t such events. At that boundary, + +```text +z = z0 + sum_j q_t[j] B_j x_j. +``` + +Three A_m calls at boundaries a,b,c therefore add +`A_m(3 z0 + sum_j (q_a[j]+q_b[j]+q_c[j]) B_j x_j)`. +This is the requested row exactly when that prefix sum equals the binary +coefficient vector of m in F3^5. Boundaries may repeat; multiple unsigned +readouts at one boundary are legal. Distinct output calls commute because +they preserve z and have distinct targets. No commutation of A_m with B_j +is used. + +The source path is + +```text +B0 B4 B4 B0 B0 B1 B3 B2 B2 B1 B3 B3 B4 B2 B1. +``` + +It uses every B_j three times, so q_15=0. The certificate lists a triple for +each of the 31 masks. For example, mask 1 uses boundaries `(0,0,1)`, and mask +31 uses `(0,3,8)`. Here +`q_3=(1,0,0,0,2)` and `q_8=(0,1,1,1,2)`, whose sum is `(1,1,1,1,1)` modulo +three. The verifier enumerates all 816 triples with repetition from the 16 +boundaries and independently regenerates the lexicographically first triple +for each requested mask. It then regenerates and checks the literal 108-call +word in [CERTIFICATE.json](CERTIFICATE.json). This finite list completes the +upper-bound proof. It is not an exhaustive census of source paths. + +Reversing the literal word, keeping every call unsigned, implements the +inverse in another 108 calls. At the reverse occurrence of a readout that +formerly saw q_t, the connector now sees -q_t, because the full source path +has total zero. Each output still has three readouts, so its connector dirt +cancels and its source increment is negated. The connector restores. No +two-call implementation of an individual inverse is charged or assumed. + +## Complete tariff and remaining costs + +The lower bound is attained coordinate by coordinate, so it holds for every +independently positive fixed price, without choosing a different schedule. +Unit prices give 108. Source prices `(1,4,10,16,28)` and readout prices 1 give +270. Those are abstract complete-call bills in F3, not physical runtime +comparisons to a characteristic-two implementation. + +Let I pay input admission and layout, P_F pay reusable coefficient preparation, +and D_W pay instruction storage, reads, dispatch and schedule construction for +this literal word. A conditional completed caller upper bound is + +```text +I + sum_F P_F + D_W + 3 sum_j c_Bj(L) + 3 sum_m c_Am(L). +``` + +Each c_F must already include its actual source/coefficient access, arithmetic, +target update, private scratch restoration, head returns and entry/exit +frames. Only z is shared borrowed scratch at the root. Primitive private +scratch remains additional and excludes all 37 data rows. The fixed table +has 108 instruction records; it is not an unpaid scheduling oracle. +The fixed-price theorem optimizes the map-call sum. Word-dependent I, P_F +or D_W can change a physical optimum and are not set to zero. + +The exact call counts and algebra are **proved**. The displayed total is a +**constructive conditional upper bound** once complete primitives and their +layout are supplied. A selected-supplier consumer, physical primitive prices, +frame/owner admission, coefficient access and precision/outer-transfer +obligations are **unknown here**. This side result closes a local interface +question; it does not justify a supplier implementation campaign. + +## Verification and source binding + +From the repository root, using the supplied interpreter: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/f3-five-source-connector/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/f3-five-source-connector +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/f3-five-source-connector --check-source-history +``` + +Both registered commands run with warnings as errors, once normally and once +with `-O`. Checks use explicit exceptions and remain active in optimized +Python. Expected marker: `PASS_F3_FIVE_SOURCE_CONNECTOR calls=108 masks=31`. +The verifier prints a generated receipt bound to all six package files and +the live predecessor README. It does not write files or hand-author a receipt. +SOURCES.json also pins the original card and selected record as provenance. +No executable or unmerged Git dependency from #4189 is imported. + +The generic coefficient checker treats `A_m z0` and `A_m B_j x_j` separately. +A separate dense implementation checks all 222 input basis vectors and nine +mixed dirty vectors across L=1,2,3, including singular and noncommuting maps. +That gives 462 forward/reverse comparisons and 462 two-direction roundtrips. +Eight semantic controls cover a missing source, a missing readout, changed +source ports, changed output ports, a readout moved across a nonzero prefix, +the wrong inverse direction, and reversed matrix-factor order at L=2,3. +These finite checks support the written proof; they are not a proof-kernel +certificate or a complete multiplication theorem. + +The card's unchanged #943 positive control passed with 945 pairings, +maximum coverage 31, 74 queries and 182 leaves. Selected baseline bindings +also passed after the sparse checkout was widened to the declared input +directories. The selected cold replay, physical/native replay and proof-kernel +build were not run for this isolated interface result. + +The verifier has no recursion, dynamic evaluation or subprocesses. All loops +are bounded by the fixed 15-event path, 816 triples, 108-event word, 36 maps +or L<=3 dense fixtures. No function exceeds 60 lines. Python necessarily +allocates objects during computation, a Power of Ten rule 3 deviation limited +to this bounded offline check. The fixture list has at most 114 states of +111 scalars each, plus a fixed number of comparison states. Every file read +has a 128 KiB cap. The 30-second registered +timeouts and normal/optimized warning checks are compensating controls. +Reassess storage if parameterized searches are ever added. Python has no +compile-time pointer/macro checks; direct calls and shallow list operations +are the inspected equivalents for rules 8 and 9. + +## Open next questions + +The structured questions are in [TASK.json](TASK.json). + +1. Does this same 108-call lower bound admit a schedule at a concrete caller + with immutable sources and unobserved outputs? First identify that caller + and price all 36 complete primitives plus admission and dispatch. A cheaper + recursive invoice is blocked by the missing physical consumer, not by + another search for this already optimal abstract word. +2. For all 242 nonzero ternary coefficient rows on the same five sources, + can one 15-event path supply three readouts per output? That would test the + boundary of count-floor attainment beyond binary demand. First inspect the + triple-prefix coverage of this path, then decide whether that demand has a + useful consumer. No exhaustive search or answer for that different family + is claimed here. + +## Credit + +This contribution was produced by Nick Petalas. It retains Ross Richardson's +#943/#934 prefix-connector lineage, ywz65's five-source contract map, Sagar +Thakrar's distinct signed-F3 comparison in #1349, and Riquelme Soares's #4189 unsigned-F3 +one-source result and explicit batch handoff. No predecessor credit line or +frozen package is changed. Independent human and formal proof-kernel review +are unclaimed. Apache-2.0. diff --git a/research/f3-five-source-connector/SOURCES.json b/research/f3-five-source-connector/SOURCES.json new file mode 100644 index 0000000000..f8ff62762d --- /dev/null +++ b/research/f3-five-source-connector/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/f3-five-source-connector/TASK.json b/research/f3-five-source-connector/TASK.json new file mode 100644 index 0000000000..529934bf26 --- /dev/null +++ b/research/f3-five-source-connector/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact unsigned F3 five-source, all-31-nonzero-binary-mask complete-call optimum, with arbitrary dirty restored connector and positive fixed tariffs.", + "scope_change_reason": "Take the explicit batch open question in PR4189. Change the characteristic-two premise rather than adding an operator; this is a local interface side result, not supplier admission.", + "bottleneck_link": "Closes an explicit complete-call interface question. The 108-call construction attains every operator count floor; a physical consumer and complete costs remain missing before this can affect recursive saving.", + "budget_minutes": 60, + "stop_rule": "Stop after one count-floor witness and bounded semantic verification. Search cap 10000 restored fifteen-event source paths; no further family expansion or selected-frontier change.", + "outcome": "completed", + "evidence": "CERTIFICATE.json supplies the 108-call word. verify.py regenerates all 31 readout triples from 816 choices, checks generic forward/reverse coefficients and dense dirty-bank actions with eight semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a concrete consumer use the 108-call unsigned F3 batch with a favorable full invoice?", + "why_it_matters": "The abstract fixed-call optimum alone does not change a recursive supplier or kappa.", + "first_step": "Identify an immutable-source, unobserved-output caller and price all 36 complete primitives, input admission, coefficient preparation and the literal 108-record dispatch.", + "blocked_by": "No physical or selected-supplier consumer is instantiated in this package." + }, + { + "question": "Can one restored fifteen-event source path cover all 242 nonzero ternary coefficient rows with three readouts per row?", + "why_it_matters": "This tests count-floor attainment for a different demand family; the binary result does not imply it.", + "first_step": "Inspect triple-prefix coverage of this path and first identify whether that full demand has a useful consumer.", + "blocked_by": "Full ternary demand and a reason for a dependent search are outside this result." + } + ], + "predecessor_handoff": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4189", + "head": "5fb3936dfc8082f438f21c72dd6ca49ff4366ae7", + "author": "Riquelme Soares", + "usage": "Context and explicit open question only; no executable dependency." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19079923", + "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "overlap_scope": "100 live open PR titles; 60 recent account PRs; last 30 hub comments; 15 active discussions; helper corpus of 336 open PRs and 2954 discussion records; focused F3 connector search. Closed work and arbitrary diffs are incompletely covered.", + "family_decision": "Narrow to this local module and stop. Complete primitive prices, physical consumer, admission and transfer remain unknown." + } +} diff --git a/research/f3-five-source-connector/VERIFY.json b/research/f3-five-source-connector/VERIFY.json new file mode 100644 index 0000000000..4cf3abca3b --- /dev/null +++ b/research/f3-five-source-connector/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Source hashes, regenerated 108-call witness, generic coefficient proof checks, dirty dense actions/inverses and eight semantic controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Repeat the complete finite certificate and controls under optimized Python; no assertions may be disabled." + } + ] +} diff --git a/research/f3-five-source-connector/verify.py b/research/f3-five-source-connector/verify.py new file mode 100644 index 0000000000..751e01f0f8 --- /dev/null +++ b/research/f3-five-source-connector/verify.py @@ -0,0 +1,259 @@ +#!/usr/bin/env python3 +"""Check the unsigned F3 five-source connector. Produced by Nick Petalas.""" + +from collections import Counter +from hashlib import sha256 +from itertools import combinations_with_replacement +import json +from pathlib import Path +from random import Random + + +HERE = Path(__file__).resolve().parent +PACKAGE_FILES = ( + "README.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "CERTIFICATE.json", "verify.py", +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def small_bytes(path): + with path.open("rb") as handle: + raw = handle.read(131073) + require(len(raw) <= 131072, "JSON exceeds the package's 128 KiB bound") + return raw + + +def read_json(path): + return json.loads(small_bytes(path)) + + +def source_bindings(): + manifest = read_json(HERE / "SOURCES.json") + files = manifest["files"] + require(len(files) == 3, "Unexpected source inventory") + root = HERE.parents[1] + live = {} + for entry in files: + if entry["usage"] == "input": + require(entry["path"] == "research/universal-connector-boundary/README.md", + "Unexpected live input") + digest = sha256(small_bytes(root / entry["path"])).hexdigest() + require(digest == entry["sha256"], "Predecessor source bytes changed") + live[entry["path"]] = digest + require(len(live) == 1, "Missing live source binding") + return live + + +def prefixes(source_word): + value = [0] * 5 + result = [tuple(value)] + for label in source_word: + value[label] = (value[label] + 1) % 3 + result.append(tuple(value)) + return result + + +def first_readouts(source_word): + points = prefixes(source_word) + found = {} + visited = 0 + for triple in combinations_with_replacement(range(16), 3): + visited += 1 + row = tuple(sum(points[t][j] for t in triple) % 3 for j in range(5)) + if all(x in (0, 1) for x in row) and any(row): + mask = sum(x << j for j, x in enumerate(row)) + found.setdefault(str(mask), list(triple)) + require(visited == 816, "Incomplete three-prefix enumeration") + require(len(found) == 31, "Source path does not cover every requested mask") + return found, visited + + +def make_word(source_word, readouts): + word = [] + for boundary in range(16): + for mask in range(1, 32): + for _ in range(readouts[str(mask)].count(boundary)): + word.append(["A", mask]) + if boundary < 15: + word.append(["B", source_word[boundary]]) + return word + + +def certificate(): + data = read_json(HERE / "CERTIFICATE.json") + require(data["schema_version"] == 1 and data["field"] == 3, "Wrong domain") + source_word = data["source_word"] + require(isinstance(source_word, list) and len(source_word) == 15, + "Source path must have fifteen events") + require(all(type(j) is int and 0 <= j < 5 for j in source_word), + "Invalid source label") + require(Counter(source_word) == Counter({j: 3 for j in range(5)}), + "Each source must be called exactly three times") + readouts, triples = first_readouts(source_word) + require(data["readouts"] == readouts, "Readout certificate differs from regeneration") + word = make_word(source_word, readouts) + require(data["word"] == word, "Literal word differs from its boundary certificate") + require(len(word) == 108, "Wrong complete-call count") + counts = Counter((op, j) for op, j in word) + require(len(counts) == 36 and set(counts.values()) == {3}, "Wrong call inventory") + return word, triples + + +def symbolic_action(word, sign=1): + """Coefficients of z0 and the five independent B_j x_j terms.""" + connector = [1, 0, 0, 0, 0, 0] + outputs = [[0] * 6 for _ in range(31)] + for op, label in word: + if op == "B": + connector[label + 1] = (connector[label + 1] + 1) % 3 + else: + outputs[label - 1] = [ + (a + b) % 3 for a, b in zip(outputs[label - 1], connector) + ] + expected = [ + [0] + [sign * ((mask >> j) & 1) % 3 for j in range(5)] + for mask in range(1, 32) + ] + return connector == [1, 0, 0, 0, 0, 0] and outputs == expected + + +def mutation_controls(word): + missing_source = word[:-1] + missing_readout = word[1:] + wrong_source = [[op, (j + 1) % 5 if op == "B" else j] for op, j in word] + wrong_output = [[op, 3 - j if op == "A" and j in (1, 2) else j] + for op, j in word] + moved_readout = [event[:] for event in word] + location = max(i for i, event in enumerate(word) if event == ["A", 31]) + event = moved_readout.pop(location) + moved_readout.append(event) + mutants = [missing_source, missing_readout, wrong_source, + wrong_output, moved_readout] + for mutant in mutants: + require(not symbolic_action(mutant), "Semantic mutation escaped detection") + require(not symbolic_action(word, sign=-1), "Wrong inverse direction escaped") + return len(mutants) + 1 + + +def tariff_checks(word): + totals = [] + for source_prices in ((1, 1, 1, 1, 1), (1, 4, 10, 16, 28)): + prices = {("B", j): price for j, price in enumerate(source_prices)} + prices.update({("A", mask): 1 for mask in range(1, 32)}) + total = sum(prices[(op, label)] for op, label in word) + require(total == 3 * sum(prices.values()), "Literal tariff differs from count floor") + totals.append(total) + require(totals == [108, 270], "Tariff fixtures changed") + return totals + + +def matvec(matrix, vector): + return [sum(a * b for a, b in zip(row, vector)) % 3 for row in matrix] + + +def matrix_bank(width): + rng = Random(width) + readers = [[[rng.randrange(3) for _ in range(width)] + for _ in range(width)] for _ in range(31)] + sources = [[[rng.randrange(3) for _ in range(width)] + for _ in range(width)] for _ in range(5)] + readers[0] = [[int(r == c == 0) for c in range(width)] for r in range(width)] + readers[1] = [[0] * width for _ in range(width)] + sources[0] = [[int(c == (r + 1) % width) for c in range(width)] + for r in range(width)] + return readers, sources + + +def execute(word, state, bank): + rows = [row[:] for row in state] + readers, sources = bank + for op, label in word: + target = 36 if op == "B" else 4 + label + value = matvec(sources[label], rows[label]) if op == "B" else ( + matvec(readers[label - 1], rows[36])) + rows[target] = [(a + b) % 3 for a, b in zip(rows[target], value)] + return rows + + +def direct_target(state, bank, sign=1, wrong_order=False): + rows = [row[:] for row in state] + readers, sources = bank + for mask in range(1, 32): + for j in range(5): + if (mask >> j) & 1: + value = (matvec(sources[j], matvec(readers[mask - 1], state[j])) + if wrong_order else + matvec(readers[mask - 1], matvec(sources[j], state[j]))) + rows[4 + mask] = [(a + sign * b) % 3 + for a, b in zip(rows[4 + mask], value)] + return rows + + +def dirty_states(width): + states = [] + for coordinate in range(37 * width): + state = [[0] * width for _ in range(37)] + state[coordinate // width][coordinate % width] = 1 + states.append(state) + for offset in range(3): + states.append([[(r * width + c + offset) % 3 for c in range(width)] + for r in range(37)]) + return states + + +def dense_checks(word): + reverse = list(reversed(word)) + cases = 0 + order_controls = 0 + for width in (1, 2, 3): + bank = matrix_bank(width) + for state in dirty_states(width): + forward = execute(word, state, bank) + backward = execute(reverse, state, bank) + require(forward == direct_target(state, bank), "Dense forward action failed") + require(backward == direct_target(state, bank, -1), "Dense reverse action failed") + require(execute(reverse, forward, bank) == state, "Forward/reverse failed") + require(execute(word, backward, bank) == state, "Reverse/forward failed") + cases += 1 + if width > 1: + state = [[0] * width for _ in range(37)] + state[0][0] = 1 + require(direct_target(state, bank) != direct_target(state, bank, wrong_order=True), + "Factor-order control did not distinguish noncommuting maps") + order_controls += 1 + return cases, order_controls + + +def main(): + live = source_bindings() + word, triples = certificate() + require(symbolic_action(word), "Generic forward coefficients failed") + require(symbolic_action(list(reversed(word)), -1), "Unsigned reverse failed") + controls = mutation_controls(word) + cases, order_controls = dense_checks(word) + tariffs = tariff_checks(word) + hashes = {name: sha256(small_bytes(HERE / name)).hexdigest() for name in PACKAGE_FILES} + receipt = { + "schema": "f3-five-source-connector/v1", + "claim_type": "scoped proof with finite certificate", + "complete_calls": len(word), "operators": 36, + "prefix_triples": triples, "covered_binary_masks": 31, + "dirty_bank_inputs": cases, "dense_direction_comparisons": 2 * cases, + "dense_roundtrips": 2 * cases, + "semantic_controls": controls + order_controls, + "unit_and_weighted_tariffs": tariffs, + "package_sha256": hashes, "input_sha256": live, + } + encoded = json.dumps(receipt, sort_keys=True, separators=(",", ":")) + print(encoded) + print("RECEIPT_SHA256 " + sha256(encoded.encode()).hexdigest()) + print("PASS_F3_FIVE_SOURCE_CONNECTOR calls=108 masks=31") + + +if __name__ == "__main__": + main()