diff --git a/research/clean-four-source-uniform-tariff/PROOF.md b/research/clean-four-source-uniform-tariff/PROOF.md new file mode 100644 index 0000000000..ecfb9f7ab1 --- /dev/null +++ b/research/clean-four-source-uniform-tariff/PROOF.md @@ -0,0 +1,201 @@ +# Exact four-source uniform paid-clean tariff + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Use Ali Romman's [PR #5372](https://github.com/CrocSwap/integer-mult-bounds/pull/5372) +paid clean-row contract, extending Cinna Davis's #1954 and the connector lineage +of Ross Richardson's #943. There are four immutable sources x_j, arbitrary +incoming outputs y_m for all fifteen nonzero four-bit masks, and one paid owned +row c. Allocate and zero c once. Subsequently allow only complete calls + +``` +B_j: c += B_j x_j j = 0,1,2,3 +A_m: y_m += A_m c m = 1,...,15. +``` + +The spaces are nonzero finite-dimensional F2 vector spaces with compatible +linear maps. Each complete call satisfies its own scratch/head restoration +contract. The original dirty connector is untouched. No output is read, no +source changes, and no observer inspects intermediate outputs. At exit c=0 and + +``` +y_m(out) = y_m(in) + A_m sum_{j in m} B_j x_j. +``` + +A finite word must work for every choice of maps and data. It may depend on +prices, but cannot rely on a particular map identity. Further zeroing, another +row, source feedback, output feedback or a fused map call changes the contract. + +Let each complete source call have uniform price b>0 and each complete output +call uniform price a>0. The new exact map-call optimum is + +``` +OPT(b,a) = min(8b + 23a, 16b + 15a). +``` + +The eight-source-call branch is optimal when b>=a; the sixteen-source-call +branch is optimal when b<=a. They tie at b=a. The componentwise-minimal +**total-count pairs** (source calls L, readouts R) are exactly + +``` +(8,23), (10,21), (12,19), (14,17), (16,15). +``` + +This is a frontier of two aggregate counts, not a classification of the nineteen +individual call counts or the full heterogeneous-price question in #6254. +Add the common allocation, zeroing, release and admission bill. Constant uniform +per-call charges can be included in a and b; word-dependent physical costs need +a separate analysis. No physical supplier or new kappa follows from this result. + +## Lower bound for every finite word + +The source-mask reduction and the one-versus-two-readout observation are from +#5372. We apply them with four sources and show attainment of their sharp +tradeoff, including the previously uncovered b>a region. + +Specialize all maps to identity on a common scalar coordinate. Independent +source bits then make c's formal coefficient a vertex p of F2^4. Each B_j call +toggles coordinate j, so the source word is a closed cube walk from zero. Every +source must occur to supply its singleton output. Its occurrence count is even +because c is restored for arbitrary independent inputs. Consequently L is even +and L>=8. This argument applies to any unbounded finite word, including words +that revisit vertices or read an output more than twice. + +Let V be the set of visited vertices and k=|V|-1 its number of nonzero vertices. +The initial and final vertices both equal zero, so k<=min(L-1,15). Every output +needs a readout. A target m outside V needs at least two, since one readout adds +only one visited mask. Thus + +``` +R >= k + 2(15-k) = 30-k >= max(31-L,15). +``` + +For 8<=L<=16 this gives + +``` +bL + aR >= 31a + (b-a)L. +``` + +The minimum of this affine expression on [8,16] is the smaller of its endpoint +values, 8b+23a and 16b+15a. For L>=16, positivity and R>=15 give the lower bound +16b+15a directly. This proves the displayed lower bound for all positive real +prices and all finite legal words. The specialization lower-bounds the generic +contract; it does not lower-bound a particular degenerate map assignment. + +## Attainment for arbitrary compatible maps + +Use the source word + +``` +0,1,0,2,1,3,2,3 +``` + +where a label j means one B_j call. Its prefix walk is + +``` +0,1,3,2,6,4,12,8,0. +``` + +There are seven distinct nonzero visited vertices. Read their seven matching +outputs once. Read each of the other eight outputs at the following pair of +visited vertices: + +| Target | Readout vertices | +|---|---| +| 5 | 1,4 | +| 7 | 1,6 | +| 9 | 1,8 | +| 10 | 2,8 | +| 11 | 3,8 | +| 13 | 1,12 | +| 14 | 2,12 | +| 15 | 3,12 | + +Each pair XORs to its target, so there are 7+2*8=23 readouts. At prefix p, +induction on the actual source calls gives c_p=sum_{j in p} B_j x_j. Linearity +then gives A_m c_u + A_m c_v = A_m sum_{j in m} B_j x_j whenever u XOR v=m. +Schedule each readout at its chosen vertex's first arrival. Outputs are never +read, so these writes do not affect later source operations. The owned row +returns to zero; arbitrary initial outputs, sources and original dirty state +have the required endpoint. No inversion, commutation, square dimension or +nonsingularity of any map is needed. + +The sixteen-call attainer is #5372's classical reflected Gray cycle. It visits +every nonzero mask once and reads each output once, giving (16,15). Neither the +Gray cycle nor its clean-row use is claimed as new. + +For completeness, these source words attain each intermediate total-count pair: + +| L | Source word | R | +|---|---|---| +| 8 | 01021323 | 23 | +| 10 | 0102010323 | 21 | +| 12 | 010201030203 | 19 | +| 14 | 01020103010213 | 17 | +| 16 | 0102010301020103 | 15 | + +Each is a simple closed walk with L-1 nonzero vertices and contains the seven +nonzero vertices of the eight-call attainer. Therefore every omitted target +still has a two-vertex representation. Read visited targets once and omitted +targets twice to obtain R=31-L. These finite walk properties can also be checked +directly from the displayed words. The code generates the literal map calls. + +The lower bound covers every even L>=8, and any L>16 pair is dominated by +(16,15). The five attained pairs therefore form the full aggregate Pareto +frontier. Its intermediate pairs tie only at a=b; they are not uniquely exposed +by a strictly positive uniform price pair. No claim is made that the eight-call +cube word itself is a new Gray-code or universal dirty-connector construction. +The new result is this exact paid-clean four-source tariff and its count frontier. + +## Finite corroboration + +The universal lower bound above supplies the real-price and unbounded-word +quantifiers. The self-contained checker additionally enumerates source-walk +states (position, visited set) with a shortest possible completion of at most +sixteen calls. Zero is always visited, giving at most 16*2^15 states. Breadth-first +search merges only identical states, whose subsequent possibilities agree. +A state at length l and position p is pruned only when l+weight(p)>16, since +weight(p) is the exact minimum number of cube edges returning p to zero. + +For every closed visited set, the checker independently computes minimum +readouts by both a group-graph breadth-first search and a 0/1 subset-XOR dynamic +program. Repeated use of the same visited mask cancels over F2, so subset-XOR +suffices. Each output can use its own optimal subset because outputs are never +read. A visited set's shortest source walk and these readouts can be combined by +placing writes at the first corresponding visits. The Gray attainer dominates +all words longer than sixteen under positive uniform prices. Thus this finite +reduction represents every potentially optimal word without a hidden cutoff. + +The generated receipt reports 190231 walk states, 20769 closed visited sets, +20440 spanning closed visited sets, the five minimal pairs, 147 exact price +comparisons, 4880 literal rectangular-map executions and 174 rejecting controls. +The rectangular executions use 3-by-2 source maps, 2-by-3 output maps, sixteen +map fixtures including zero maps, every one of 44 incoming basis bits, zero and +sixteen mixed input states. Counts are executions, not exhaustive enumeration +of all maps. Deleting any emitted call from the five schedules is rejected; +four malformed source words are also rejected. All checks survive -O. + +## Implementation limits + +The verifier has no recursion, subprocesses, dynamic code generation or file +writes. All loops have fixed finite domains. The walk queue/distance map hold +at most 16*2^15 states, the visited-set domain is at most 2^15, each additive +search has sixteen vertices, and every source word has at most sixteen labels. +Functions stay below sixty physical lines. Explicit exceptions preserve +invariants under optimization. The receipt hashes package files and verifies +both live predecessor input hashes; historical source validation is separate. + +Power of Ten rule 3 deviation: CPython and its standard library allocate during +these finite offline checks. The fixed domains above bound live collections; +fixed storage after initialization is not claimed. Rule 10 limitation: no +static type checker or linter is required by the standard-library environment. +Warning-strict syntax/AST inspection and normal/optimized registered replay are +the available diagnostics. No shared build configuration changes. + +Physical map lowering, provisioning, routing, descriptors, ownership admission, +precision/tape, recursive hosting and the full signed supplier bill remain open. +The five selected assumptions are unchanged. No predecessor scientific replay, +selected cold replay, Lean, Docker, independent human review, formal proof-kernel +acceptance or complete multiplication theorem is claimed. diff --git a/research/clean-four-source-uniform-tariff/README.md b/research/clean-four-source-uniform-tariff/README.md new file mode 100644 index 0000000000..eed1c7d71a --- /dev/null +++ b/research/clean-four-source-uniform-tariff/README.md @@ -0,0 +1,94 @@ +# Exact four-source uniform clean-row tariff + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. In the generic +four-source paid-clean connector contract of Ali Romman's #5372, all positive +uniform complete source/readout prices b,a have exact optimum + +``` +min(8b + 23a, 16b + 15a). +``` + +The complete frontier of total source/readout counts is (8,23), (10,21), +(12,19), (14,17), (16,15). An explicit eight-call source walk reads seven outputs +once and eight twice. The [proof](PROOF.md) bounds every finite legal word and +executes all fifteen target updates for arbitrary compatible F2-linear maps, +including singular and rectangular maps. For example, b=10,a=1 gives exact +map-call cost 103, versus the classical Gray schedule's 175. Common paid row +allocation, zeroing and release costs must still be added. + +This settles the uniform-price specialization of Open next question 2 in the +older [#6254](https://github.com/CrocSwap/integer-mult-bounds/pull/6254). It does +not classify individual call counts or settle heterogeneous prices. The source +mask counting argument and general Gray construction are credited inputs; the +new result is their sharp four-source tariff and aggregate frontier. Research +stopped at this first result. There is no new kappa or selected-frontier change. + +## Reproduction and evidence + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clean-four-source-uniform-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-four-source-uniform-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-four-source-uniform-tariff --check-source-history +``` + +Use another CPython 3.12 path elsewhere. The registered runner separately runs +normal and optimized warning-strict commands, each limited to 120 seconds. +The verifier writes no files and prints a generated, SHA256-bound JSON receipt +with marker `PASS_CLEAN_FOUR_SOURCE_UNIFORM_TARIFF`. + +Finite coverage is 190231 source-walk states, 20769 closed visited sets, 20440 +spanning closed sets, two independent XOR-distance algorithms for every closed +set, five attaining profiles, 147 exact price comparisons, 4880 rectangular-map +executions and 174 rejecting controls. These counts describe enumerated states +and executions. The written proof supplies the universal price, map and word +quantifiers. The finite reduction covers every potentially optimal uniform-price +word; it is not merely a length-sixteen search without a dominance argument. +No predecessor scientific verifier was replayed as this deliverable. + +## Scope and sources + +Canonical base e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8, +selected #7000 with conditional kappa 0.00363005817. The priority prose still +names an older selection. The selected source-binding orientation and card's +945-pairing positive control passed; neither is evidence of the new theorem. +[TASK.json](TASK.json) records the changed card scope and advance claim. +[SOURCES.json](SOURCES.json) pins the two live contract/question inputs and +historical catalogue/selected-record provenance. Source hashes authenticate +those bytes; they do not certify predecessor mathematics. + +The model has one paid clean row, immutable sources, unread dirty outputs and +one final restoration. Fixed per-call prices and the generic all-map requirement +are essential. Physical map/native lowering, row provisioning, descriptors, +routing, precision/tape, ownership admission, recursive hosting and the full +signed supplier invoice remain open. The five selected assumptions are unchanged. +No selected cold replay, full native/caller replay, Lean, Docker, independent +human review, formal proof-kernel acceptance or complete multiplication theorem +is claimed. CI finite replay and independent scientific review are distinct. +The [proof](PROOF.md) also records the bounded managed-allocation and static +analysis limitations of the verifier. + +## Open next questions + +1. Determine the four-source heterogeneous frontier. First use weighted source + edges and target-specific readout costs in the finite visited-state reduction. + The sixteen-call dominance cutoff here depends on uniform prices and does + not settle the individual-count frontier. No such extension is reserved. +2. Identify an actual recursive caller whose complete prices favor the eight-call + branch. First price its clean-row lifetime, full maps, routing, descriptors, + restoration and precision. No physical caller or full positive invoice is + supplied here. + +## Credit + +Credit Ali Romman #5372 for the paid-clean contract analysis, source-mask lower +bound and general-n Gray optimum in the a>=b region; Nick Petalas #6254 for the +three-source tariff and explicit four-source question; Cinna Davis #1954 for the +paid-row extension and #2271 for related borrowed-source Gray tours; Ross +Richardson #943 for the connector lineage. Cube walks, Gray cycles, shortest +paths and subset-XOR dynamic programming are classical. This contribution claims +the four-source tariff theorem, aggregate frontier and its rerunnable checker. +All predecessor files and credit lines remain unchanged. diff --git a/research/clean-four-source-uniform-tariff/SOURCES.json b/research/clean-four-source-uniform-tariff/SOURCES.json new file mode 100644 index 0000000000..475a9c0300 --- /dev/null +++ b/research/clean-four-source-uniform-tariff/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/clean-connector-gray-optimum/PROOF.md", + "usage": "input", + "git_blob": "3f1df5128e713d24c80942856826e510b03fc415", + "sha256": "82d5401187424c26a21e8f21dfe9aebbee8e419a3a363b108151d472620df73a" + }, + { + "path": "research/clean-three-source-tariffs/README.md", + "usage": "input", + "git_blob": "b3a9cd99e801782d41bc02ada719e8353d01ea08", + "sha256": "890dcfcbb7c05cb19e526cc0204481069b92699aba94e4a33d37ccf6d608a7d9" + } + ] +} diff --git a/research/clean-four-source-uniform-tariff/TASK.json b/research/clean-four-source-uniform-tariff/TASK.json new file mode 100644 index 0000000000..e1933a8934 --- /dev/null +++ b/research/clean-four-source-uniform-tariff/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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 four-source paid-clean connector tariff for all positive uniform source/readout prices; complete aggregate source/readout count frontier.", + "scope_change_reason": "Take the uniform-price specialization of Open next question 2 in older PR6254 within PR5372's existing paid-clean alphabet. This is a local interface side result, not an alphabet extension or supplier.", + "bottleneck_link": "The sharp source/readout tradeoff selects a legal clean-row schedule before its caller pays hosting, allocation, restoration and precision costs; no complete supplier gain is asserted.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original four-source result, package it and do not extend the source count or price model.", + "outcome": "completed", + "evidence": "PROOF.md gives an all-finite-word counting proof and explicit arbitrary-map attainers. verify.py independently enumerates visited states and subset-XOR costs, executes dirty rectangular endpoints and rejects deleted calls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the full four-source heterogeneous-price frontier?", + "why_it_matters": "Uniform aggregate counts do not price independent source and output calls.", + "first_step": "Use the finite visited-state reduction with weighted source edges and target-specific readout costs, then identify the minimal individual count vectors.", + "blocked_by": "No heterogeneous classification is supplied; the sixteen-call uniform dominance cutoff cannot be silently reused." + }, + { + "question": "Can a named recursive caller profit from the eight-call branch?", + "why_it_matters": "An abstract map-call saving need not survive the complete supplier invoice.", + "first_step": "Pin one caller and price the clean-row lifetime, complete maps, routing, descriptors, restoration and precision.", + "blocked_by": "No physical caller or favorable full signed bill is supplied." + } + ], + "claim_type": "scoped written proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540620", + "source_question": { + "pr": 6254, + "author": "petalas", + "question": "Open next question 2: four-source heterogeneous paid-clean frontier. This contribution settles uniform prices only.", + "contract_predecessor": 5372, + "contract_author": "aliromman" + }, + "upstream_checkpoint": { + "commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "priority_revision": 8, + "checked_utc": "2026-11-11T11:20:32Z", + "selected_kappa": "0.00363005817" + } +} diff --git a/research/clean-four-source-uniform-tariff/VERIFY.json b/research/clean-four-source-uniform-tariff/VERIFY.json new file mode 100644 index 0000000000..711f6f4077 --- /dev/null +++ b/research/clean-four-source-uniform-tariff/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/clean-connector-gray-optimum/PROOF.md", + "research/clean-three-source-tariffs/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact visited-state and independent subset-XOR corroboration, five attainers, rectangular dirty-input endpoints and deletion controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with Python assertions disabled; explicit contracts stay active." + } + ] +} diff --git a/research/clean-four-source-uniform-tariff/verify.py b/research/clean-four-source-uniform-tariff/verify.py new file mode 100644 index 0000000000..8a7af74c5f --- /dev/null +++ b/research/clean-four-source-uniform-tariff/verify.py @@ -0,0 +1,295 @@ +#!/usr/bin/env python3 +"""Exact four-source clean-row tariff certificate. Apache-2.0.""" +from collections import deque +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path +import json +from random import Random + + +WORDS = ( + (0, 1, 0, 2, 1, 3, 2, 3), + (0, 1, 0, 2, 0, 1, 0, 3, 2, 3), + (0, 1, 0, 2, 0, 1, 0, 3, 0, 2, 0, 3), + (0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 1, 3), + (0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 0, 1, 0, 3), +) +PROFILES = ((8, 23), (10, 21), (12, 19), (14, 17), (16, 15)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def prefixes(word): + require(isinstance(word, tuple) and len(word) <= 16, "word capacity") + result = [0] + for label in word: + require(type(label) is int and 0 <= label < 4, "source label") + result.append(result[-1] ^ (1 << label)) + require(result[-1] == 0, "owned row not restored") + return result + + +def representations(values): + """Shortest paths in the additive group, with explicit finite bounds.""" + require(len(values) <= 15 and len(set(values)) == len(values), "value set") + require(all(type(v) is int and 1 <= v <= 15 for v in values), "mask") + paths = [None] * 16 + paths[0] = () + queue = deque([0]) + for _ in range(16): + if not queue: + break + current = queue.popleft() + for value in values: + target = current ^ value + if paths[target] is None: + paths[target] = paths[current] + (value,) + queue.append(target) + require(not queue, "additive-state capacity") + return paths + + +def subset_distances(values): + """Independent 0/1 subset dynamic program, not a group-graph BFS.""" + distances = [99] * 16 + distances[0] = 0 + for value in values: + old = distances + distances = [min(old[m], 1 + old[m ^ value]) for m in range(16)] + return distances + + +def schedule(word): + walk = prefixes(word) + values = tuple(sorted(set(walk) - {0})) + paths = representations(values) + require(all(p is not None for p in paths), "source span") + at_vertex = [[] for _ in range(16)] + for target in range(1, 16): + for value in paths[target]: + at_vertex[value].append(target) + calls = [("allocate", 0), ("zero", 0)] + used = set() + for index, label in enumerate(word): + calls.append(("B", label)) + vertex = walk[index + 1] + if vertex not in used: + calls.extend(("A", target) for target in at_vertex[vertex]) + used.add(vertex) + calls.append(("release", 0)) + return tuple(calls), tuple(paths) + + +def check_formal(calls): + require(len(calls) <= 50, "call capacity") + active = False + allocated = False + released = False + current = None + outputs = [0] * 16 + counts = [0, 0] + for kind, index in calls: + if kind == "allocate": + require(not allocated and not released, "allocation lifetime") + allocated = True + elif kind == "zero": + require(allocated and not active and not released, "zero lifetime") + active = True + current = 0 + elif kind in ("A", "B"): + require(active and not released, "call lifetime") + if kind == "B": + require(type(index) is int and 0 <= index < 4, "B index") + current ^= 1 << index + counts[0] += 1 + else: + require(type(index) is int and 1 <= index < 16, "A index") + outputs[index] ^= current + counts[1] += 1 + elif kind == "release": + require(active and not released and current == 0, "release restoration") + released = True + active = False + else: + raise ValueError("unknown call") + require(released and outputs == list(range(16)), "target endpoint") + return tuple(counts) + + +def closed_visited_sets(): + """All useful walks, merging states only by position and visited set.""" + # Zero is always visited, so at most 16 * 2^15 states exist. + start = (1 << 4) + distances = {start: 0} + queue = deque([start]) + closed = {} + for _ in range(16 * (1 << 15)): + if not queue: + break + state = queue.popleft() + length = distances[state] + position, visited = state & 15, state >> 4 + if position == 0 and visited not in closed: + closed[visited] = length + if length == 16: + continue + for label in range(4): + next_position = position ^ (1 << label) + if length + 1 + next_position.bit_count() > 16: + continue + next_visited = visited | (1 << next_position) + next_state = (next_visited << 4) | next_position + if next_state not in distances: + distances[next_state] = length + 1 + queue.append(next_state) + require(not queue, "walk-state capacity") + return closed, len(distances) + + +def check_oracle(): + closed, state_count = closed_visited_sets() + candidates = [] + spanning = 0 + spectrum = {} + for visited, length in sorted(closed.items()): + values = tuple(m for m in range(1, 16) if visited & (1 << m)) + paths = representations(values) + distances = subset_distances(values) + require(distances == [99 if p is None else len(p) for p in paths], + "independent XOR distances") + if 99 in distances: + continue + spanning += 1 + reads = sum(distances) + spectrum[length] = min(spectrum.get(length, 99), reads) + candidates.append((length, reads)) + frontier = [] + best_reads = 99 + for pair in sorted(set(candidates)): + if pair[1] < best_reads: + frontier.append(pair) + best_reads = pair[1] + frontier = tuple(frontier) + require(frontier == PROFILES, "exact finite frontier") + require(tuple(sorted(spectrum.items())) == PROFILES, "length spectrum") + return candidates, {"walk_states": state_count, "closed_sets": len(closed), + "spanning_closed_sets": spanning, "frontier": frontier} + + +def check_prices(candidates): + prices = [(Fraction(b), Fraction(a)) for b in range(1, 13) + for a in range(1, 13)] + prices += [(Fraction(1, 3), Fraction(2, 7)), + (Fraction(2, 7), Fraction(1, 3)), (Fraction(5, 11), Fraction(5, 11))] + for b, a in prices: + actual = min(length * b + reads * a for length, reads in candidates) + require(actual == min(8 * b + 23 * a, 16 * b + 15 * a), "price theorem") + return len(prices) + + +def linear_map(rows, value): + return sum(((row & value).bit_count() % 2) << i for i, row in enumerate(rows)) + + +def execute(calls, source_maps, output_maps, initial): + # Layout: four two-bit sources; fifteen two-bit outputs; three owned bits; + # three untouched dirty-connector bits. All 44 incoming bits are admitted. + sources = tuple((initial >> (2 * j)) & 3 for j in range(4)) + outputs = [(initial >> (8 + 2 * j)) & 3 for j in range(15)] + owned = (initial >> 38) & 7 + dirty = (initial >> 41) & 7 + for kind, index in calls: + if kind == "zero": + owned = 0 + elif kind == "B": + owned ^= linear_map(source_maps[index], sources[index]) + elif kind == "A": + outputs[index - 1] ^= linear_map(output_maps[index - 1], owned) + else: + require(kind in ("allocate", "release"), "execution action") + expected = [(initial >> (8 + 2 * j)) & 3 for j in range(15)] + for target in range(1, 16): + combined = 0 + for j in range(4): + if target & (1 << j): + combined ^= linear_map(source_maps[j], sources[j]) + expected[target - 1] ^= linear_map(output_maps[target - 1], combined) + require(outputs == expected and owned == 0, "rectangular endpoint") + require(sources == tuple((initial >> (2 * j)) & 3 for j in range(4)), "source") + require(dirty == ((initial >> 41) & 7), "dirty connector") + + +def check_endpoints(schedules): + total = 0 + states = [0] + [1 << bit for bit in range(44)] + states += [((1 << 44) - 1) // (i + 1) for i in range(1, 17)] + for seed in range(16): + rng = Random(seed) + source_maps = tuple(tuple(rng.randrange(4) for _ in range(3)) + for _ in range(4)) + output_maps = tuple(tuple(rng.randrange(8) for _ in range(2)) + for _ in range(15)) + if seed == 0: + source_maps = ((0, 0, 0),) * 4 + output_maps = ((0, 0),) * 15 + for calls in schedules: + for initial in states: + execute(calls, source_maps, output_maps, initial) + total += 1 + return total + + +def check_controls(schedules): + rejected = 0 + for calls in schedules: + for index in range(len(calls)): + # Every emitted call in an attaining schedule is essential. + try: + check_formal(calls[:index] + calls[index + 1:]) + except ValueError: + rejected += 1 + else: + raise ValueError("deleted-call control accepted") + for word in ((4, 4), (0,), (True, True), tuple([0] * 18)): + try: + prefixes(word) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid-word control accepted") + return rejected + + +def source_bindings(package): + metadata = json.loads((package / "SOURCES.json").read_text()) + root = package.parent.parent + for row in metadata["files"]: + if row["usage"] == "input": + require(sha256((root / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "source hash: " + row["path"]) + return {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + + +def main(): + package = Path(__file__).resolve().parent + hashes = source_bindings(package) + schedules = [] + for word, expected in zip(WORDS, PROFILES, strict=True): + calls, _ = schedule(word) + require(check_formal(calls) == expected, "attaining profile") + schedules.append(calls) + candidates, coverage = check_oracle() + coverage["price_comparisons"] = check_prices(candidates) + coverage["rectangular_executions"] = check_endpoints(schedules) + coverage["rejecting_controls"] = check_controls(schedules) + print(json.dumps({"status": "PASS_CLEAN_FOUR_SOURCE_UNIFORM_TARIFF", + "coverage": coverage, "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()