diff --git a/research/cross-port-thin-capacity/PROOF.md b/research/cross-port-thin-capacity/PROOF.md new file mode 100644 index 0000000000..cf794f5db8 --- /dev/null +++ b/research/cross-port-thin-capacity/PROOF.md @@ -0,0 +1,119 @@ +# Cross-port information capacity for the thin-query pool + +This is a scoped proof. The general ingredient is classical linear information +dimension. The repository's outside-input rank probe already states the fixed- +observation quotient formula; its centre-nonlinear-fresh-floor package applies +dimension arguments to a different centre history. The new claim here is the +conditional cross-port thin-pool capacity constraint and its 528-request +consequences below. It proposes no physical primitive. + +## Observation contract + +Let K be any field. The input x ranges over the whole finite-dimensional space +X. A row of X* is a scalar linear observable. Initially the consumer knows all +observations in a subspace F of X*. It must return all observations in T. + +A request returns at most c scalar linear observations of x. Its rows may depend +on previously observed values, including the initial free observations. Each +request's rows are fixed once that previous transcript is fixed. Free computation, +mixing across ports, feedback, and final decoding may be arbitrary deterministic +functions of the known transcript. They reveal no additional information about x. +There is no hidden input-dependent control channel. Every execution is finite. + +The capacity c counts scalar output coordinates. It is neither a native frame +rank nor the number of ports with a nonzero coefficient. A field response with +several independently readable coordinates is a vector response and must be +charged for those coordinates. Correlated or restricted inputs are outside X. + +## Theorem 1: capacity on every successful transcript + +Put D = dim(F + T) - dim F. Every protocol correct for every x has, on every +execution, total returned scalar capacity at least D. A sharper statement uses +the rank of the actual returned rows modulo F, which must be at least D. + +Proof. Fix an execution on x, and collect its actual query rows in Q. Suppose +there is h in ker F intersect ker Q with T h nonzero. The execution on x+h has +the same initial transcript. Inductively, each request chooses the same rows +and returns the same values, so it also makes the same control decisions and +stops with the same decoder output. Its required answer differs by T h. This +contradicts correctness. Thus ker(F + Q) is contained in ker T. By finite- +dimensional duality, T is contained in F + Q. Therefore + + D <= dim(F + Q) - dim F <= number of returned scalar coordinates + <= sum_j c_j. + +This argument permits nonlinear decoding and data-dependent query selection. +Randomness with a correctness guarantee for every fixed random tape can be +fixed first. No claim is made about bounded-error randomized protocols. + +The bound is sharp in this abstract oracle contract. Choose D target rows +complementing F inside F+T, request them, and reconstruct every target using F. +Group the D rows into packets of the declared capacities when their total is +at least D. This is an information-theoretic upper bound. It does not show +chronological availability or physical implementation of these queries. + +## Theorem 2: independent ports and extra free information + +For P independent port inputs X_p, suppose free and target rows are port-local +and F = direct_sum F_p, T = direct_sum T_p. Then + + D = sum_p [dim(F_p + T_p) - dim F_p]. + +This follows by taking dimensions of direct sums. Theorem 1 permits every query +row to mix all ports, so it is stronger than summing bounds for protocols +restricted to port-local requests. An invertible linear change of all input +coordinates preserves the dimensions. Relabeling or mixing ports cannot +replace P independent inputs with one correlated input. + +If an additional free observation space S is supplied, the exact oracle +minimum becomes D_S = dim(F + S + T) - dim(F + S). The dimension formula gives + + D_S >= D - [dim(F + S) - dim F]. + +Consequently, reducing the necessary scalar capacity by k needs at least k +new independent free observations modulo F. This lower bound is sharp by +choosing S inside a complement of F in F+T. Where those observations come from, +and what they cost, are separate physical questions. + +## Conditional application to the reported thin-query deficit + +Matarener's [PR #5996](https://github.com/CrocSwap/integer-mult-bounds/pull/5996), +head `47242572d3b22ce49371245edc561dd75bf263e8`, reports a one-port quotient +dimension of fifteen for the retained p16 controllers. Its README at that +head defines the scalar specialization and credits the controller lineage. +That reported quotient dimension is an explicit premise here. Its computation +is not rerun, and no scientific acceptance of that predecessor is claimed. + +If P independent copies of that observation contract are required, Theorem 2 +gives D = 15P. Thus 104 ports require total scalar capacity 1560 and 112 ports +require 1680, even with dense cross-port encoding, arbitrary joint decoding and +adaptive feedback as defined above. The atlas's 528-request target therefore +requires the following output capacities. + +- At 104 ports, capacity at most two per request is insufficient. If every + request has capacity at most three, at least 504 of the 528 requests must + have capacity three. The remaining 24 can have capacity two. These capacities + sum to 1560. With fewer than 528 requests the necessary count of capacity-three + requests can only increase, until it is infeasible. +- At 112 ports, capacity at most three per request is insufficient. If every + request has capacity at most four, at least 96 of the 528 requests must have + capacity four. The remaining 432 can have capacity three. Their total is 1680. +- If all requests remain scalar, meeting 528 needs at least 1032 new free + dimensions at 104 ports, or 1152 at 112 ports, beyond the cited free span. + +For the first two statements, if n requests have maximum capacity r, their +total capacity is at most (r-1)*528+n. Solve this necessary inequality for n. +The displayed distributions attain equality only as abstract output budgets. +They are not causal controllers or invoices. In particular a rank-r native +job has not been proved to deliver r scalar observations at the desired price. + +## Scope of the obstruction + +The new exclusion is for scalar or capacity-limited observations on independent +port inputs. A channel supported on all ports can still return only one scalar. +A channel exposing an entire port vector can have large capacity and is not +excluded. Restricted input families, new paid full outputs, changed target +relations, input-dependent side channels and approximate recovery require +different hypotheses. The proof does not identify native frame rank with +information capacity. No physical execution, complete paid moment, compiler, +stock, precision, tape tariff, all-size admission or new kappa is supplied. diff --git a/research/cross-port-thin-capacity/README.md b/research/cross-port-thin-capacity/README.md new file mode 100644 index 0000000000..3b8e68a8bc --- /dev/null +++ b/research/cross-port-thin-capacity/README.md @@ -0,0 +1,98 @@ +# Dense port mixing does not reduce scalar thin-query information + +Claim type: scoped mathematical proof with exact finite corroboration. No new +kappa or selected-frontier change. + +The [proof](PROOF.md) extends a port-local information deficit to arbitrary +linear queries mixing independent ports, with adaptive query selection and +arbitrary deterministic decoding. If each port needs fifteen dimensions beyond +its free information, P ports need total returned scalar capacity at least 15P. +Touching many ports with one scalar response does not increase its capacity. + +This builds on Matarener's [PR #5996](https://github.com/CrocSwap/integer-mult-bounds/pull/5996), +exact head `47242572d3b22ce49371245edc561dd75bf263e8`, and its question about +cross-port channels. The reported per-port deficit is cited as a premise. This +package does not replay or validate it. The linear information principle is +classical; the new contribution is the cross-port observation contract and its +conditional thin-pool capacity constraints. The repository's +[outside-input rank probe](../outside-input-research-targets/README.md) already +states the fixed-observation quotient formula. Matarener's +[nonlinear centre floor](../centre-nonlinear-fresh-floor/README.md) covers a +different history and continuous or semialgebraic fresh encoders. Neither is +replayed here, and neither source's general dimension principle is claimed new. + +For 528 requests on 104 independent ports, scalar capacity two is insufficient; +with capacity at most three, at least 504 requests need capacity three. For 112 +ports, capacity three is insufficient; with capacity at most four, at least 96 +requests need capacity four. Keeping every request scalar instead requires at +least 1032 or 1152 additional free dimensions respectively. + +These are necessary information budgets, not physical schedules. Scalar output +capacity is explicitly different from native frame rank. Binding the actual +multi-port data and its free operations to this contract remains an obligation. +An entire independently readable output vector is charged by its coordinates. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/cross-port-thin-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/cross-port-thin-capacity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cross-port-thin-capacity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cross-port-thin-capacity --check-source-history +``` + +The standalone verifier needs no Git, network or predecessor source. It +enumerates all triples of binary free/query/target subspaces in dimensions zero +through four. Through dimension three, a separate literal input-fiber oracle +checks whether any lookup-table decoder exists. Rational recoding and +side-information fixtures, adaptive decision trees, packet arithmetic, and +semantic/boundary controls corroborate the written proof. The universal theorem +rests on that proof, not these finite examples. `--receipt PATH` writes a new +receipt bound to package file hashes outside the package. + +The run enumerates 304,993 subspace triples and makes 4,230 independent fiber +comparisons. It also checks 116 rational fixtures, 510 complete adaptive +transcripts, 255 ambiguous shortened transcripts, four semantic controls and +four invalid-input rejections. Normal and optimized commands each completed +locally in under one second; these are replay-budget observations, not speedups. + +## Verifier bounds + +No recursive code, solver, subprocess, network access or hidden input is used. +The largest subspace census has 67 spaces, 4489 pair joins and 67 cubed triples. +Binary vectors have at most eight bits, spans at most 256 elements, and rational +matrices at most 32 rows by 16 columns. Adaptive trees enumerate at most 256 +inputs per dimension. Every function is below sixty lines. Invariants use +explicit exceptions and stay enabled under optimization. The four indirect +control calls have a fixed, visible target list. Source hashing reads six files +of at most one MiB each. The optional receipt is created exclusively. + +Power-of-Ten rule 3 deviation: Python's managed objects and Fraction arithmetic +allocate during verification, so fixed allocation after initialization is not +claimed. The finite dimensions above bound live collections and integer sizes; +there is no unbounded input arithmetic. The compensation is checked by the +boundary controls and both registered executions. A larger-input verifier must +declare new bounds before extending these constants. Rule 10 uses warning-strict +normal and optimized replay; no separate Python static analyzer is configured +for this isolated package. + +## Open next questions + +- Can a physical thin query deliver enough independently readable coordinates + to meet the capacity distribution above at a favorable complete cost? First + specify its input/output maps and native frame tariff. Physical realization, + dirty restoration and causal availability are unproved. +- Do the actual port data and every allowed free operation admit the independent + direct-sum observation model? First give the input-coordinate and free-span + maps. This package does not establish that application premise. +- Can a changed producer supply the required new free information more cheaply + than the omitted scalar requests? First price one new independent observable, + including its later consumption and restoration. No such producer is supplied. + +The proof and verifier were produced by Nick Petalas. Credit Matarener for the +per-port deficit and question, Cinna Davis for the controllers, Ali Romman for +the direct-controller construction, Dugongue for the target atlas, and the +predecessor lineage retained in PR #5996. Independent human and formal +proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/cross-port-thin-capacity/SOURCES.json b/research/cross-port-thin-capacity/SOURCES.json new file mode 100644 index 0000000000..d596e2e530 --- /dev/null +++ b/research/cross-port-thin-capacity/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/cross-port-thin-capacity/TASK.json b/research/cross-port-thin-capacity/TASK.json new file mode 100644 index 0000000000..520cc4835b --- /dev/null +++ b/research/cross-port-thin-capacity/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "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": "Adaptive cross-port scalar-observation capacity for independent copies of the reported fifteen-dimensional thin-query deficit, with 528-request output-capacity and free-information lower bounds.", + "scope_change_reason": "Take the multi-port channel question of Matarener PR5996. Replace port-local requests by arbitrary cross-port linear observations and adaptive feedback; this is a conditional information obstruction rather than a new productive-target invoice.", + "bottleneck_link": "A compressed thin-query pool needs real output capacity or newly supplied information. Dense support alone does not pay the 15P information deficit. The result screens a proposed interface before physical construction, without identifying capacity with native frame rank.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved cross-port information bound and its 528-request consequences; no physical expansion or predecessor replay.", + "outcome": "completed", + "evidence": "PROOF.md; standalone exact verify.py; hash-bound receipts generated outside the package.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physical thin query attain the necessary multi-output capacity distribution at a favorable complete price?", + "why_it_matters": "Capacity one cannot meet the target under the independent-port observation contract.", + "first_step": "Write the exact input/output map and native frame tariff for one multi-output query.", + "blocked_by": "No physical primitive, causal availability, dirty restoration or full cost is supplied." + }, + { + "question": "Does the actual multi-port caller satisfy the direct-sum observation premises?", + "why_it_matters": "The 104/112-port application is conditional on independent inputs and preservation of the specified free information.", + "first_step": "Give its input-coordinate and free-operation maps into the observation model.", + "blocked_by": "This package neither validates PR5996 nor binds physical multi-port semantics." + }, + { + "question": "Can a changed producer supply the missing 1032 or 1152 free dimensions at favorable cost?", + "why_it_matters": "Such new information is another explicit way to escape the scalar-output exclusion.", + "first_step": "Price one newly independent observable, its later consumption and restoration.", + "blocked_by": "No such changed producer is supplied." + } + ], + "predecessor_premise": { + "pr": 5996, + "author": "Matarener", + "head": "47242572d3b22ce49371245edc561dd75bf263e8", + "status": "reported, not replayed here", + "premise": "dim(F_p + T_p) - dim F_p = 15", + "application_hypotheses": [ + "independent port input spaces", + "free information is the direct sum of the reported local free spaces", + "each request capacity counts all returned scalar observations" + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227495" + }, + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + } +} diff --git a/research/cross-port-thin-capacity/VERIFY.json b/research/cross-port-thin-capacity/VERIFY.json new file mode 100644 index 0000000000..27837c3d9f --- /dev/null +++ b/research/cross-port-thin-capacity/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All binary subspace triples through dimension four, independent fiber oracle through dimension three, rational recoding, adaptive transcripts, packet budgets and controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same scientific checks with optimization; all invariants use explicit exceptions." + } + ] +} diff --git a/research/cross-port-thin-capacity/verify.py b/research/cross-port-thin-capacity/verify.py new file mode 100644 index 0000000000..12bae4e17d --- /dev/null +++ b/research/cross-port-thin-capacity/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Exact corroboration of PROOF.md. Standard library; Apache-2.0.""" + +import argparse +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def binary_span(rows, dimension): + require(0 <= dimension <= 8, "binary dimension outside 0..8") + require(len(rows) <= 16, "too many binary rows") + require(all(0 <= r < 1 << dimension for r in rows), "invalid binary row") + vectors = {0} + for row in rows: + vectors |= {v ^ row for v in vectors} + require(len(vectors) <= 1 << dimension, "span capacity") + return frozenset(vectors) + + +def subspaces(dimension): + """All RREF bases, without traversal or random choices; n <= 4.""" + require(0 <= dimension <= 4, "subspace census dimension outside 0..4") + spaces = {} + for rank in range(dimension + 1): + for pivots in combinations(range(dimension), rank): + slots = [(i, j) for i, p in enumerate(pivots) + for j in range(p + 1, dimension) if j not in pivots] + for values in product((0, 1), repeat=len(slots)): + rows = [1 << p for p in pivots] + for (i, j), bit in zip(slots, values, strict=True): + rows[i] |= bit << j + span = binary_span(rows, dimension) + require(span not in spaces, "RREF duplicate") + spaces[span] = tuple(rows) + return spaces + + +def observation(rows, point): + return tuple((row & point).bit_count() % 2 for row in rows) + + +def fiber_decodable(free, query, target, dimension): + """Independent oracle: allow any lookup-table decoder on actual fibers.""" + fibers = {} + for point in range(1 << dimension): + transcript = observation(free + query, point) + answer = observation(target, point) + if transcript in fibers and fibers[transcript] != answer: + return False + fibers[transcript] = answer + return True + + +def census(): + triples = fibers = 0 + per_dimension = [] + for dimension in range(5): + spaces = subspaces(dimension) + # Enumerate every ordered square binary matrix as a separate completeness oracle. + all_spans = {binary_span(rows, dimension) + for rows in product(range(1 << dimension), repeat=dimension)} + require(set(spaces) == all_spans, "RREF census is incomplete") + keys = tuple(spaces) + ranks = {s: len(spaces[s]) for s in keys} + joins = {(f, q): binary_span(spaces[f] + spaces[q], dimension) + for f in keys for q in keys} + for free in keys: + for target in keys: + deficit = ranks[joins[free, target]] - ranks[free] + minimum = dimension + 1 + for query in keys: + decoded = target <= joins[free, query] + if decoded: + require(ranks[query] >= deficit, "capacity bound failed") + minimum = min(minimum, ranks[query]) + if dimension <= 3: + actual = fiber_decodable(spaces[free], spaces[query], + spaces[target], dimension) + require(actual == decoded, "fiber/row-space disagreement") + fibers += 1 + triples += 1 + require(minimum == deficit, "abstract bound is not sharp") + per_dimension.append({"dimension": dimension, "subspaces": len(keys)}) + return {"triples": triples, "fiber_comparisons": fibers, + "subspaces": per_dimension} + + +def rational_rank(matrix, columns): + require(0 <= columns <= 16 and len(matrix) <= 32, "rational matrix capacity") + require(all(len(row) == columns for row in matrix), "ragged matrix") + rows = [[Fraction(x) for x in row] for row in matrix] + pivot = 0 + for column in range(columns): + index = next((i for i in range(pivot, len(rows)) if rows[i][column]), None) + if index is None: + continue + rows[pivot], rows[index] = rows[index], rows[pivot] + scale = rows[pivot][column] + rows[pivot] = [x / scale for x in rows[pivot]] + for i in range(pivot + 1, len(rows)): + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[pivot], strict=True)] + pivot += 1 + return pivot + + +def direct_sum_fixtures(): + cases = 0 + for ports in range(1, 5): + for per_port in range(1, 5): + dimension = ports * per_port + target = [[int(j <= i) for j in range(dimension)] + for i in range(dimension)] + require(rational_rank(target, dimension) == dimension, "dense recoding") + for known in range(dimension + 1): + free = target[:known] + deficit = rational_rank(free + target, dimension) - known + require(deficit == dimension - known, "side-information deficit") + if known < dimension: + require(rational_rank(free + target[known:-1], dimension) + < dimension, "missing observation accepted") + cases += 1 + return cases + + +def adaptive_fixtures(): + leaves = failures = 0 + for dimension in range(1, 9): + transcripts = {} + prefixes = {} + for point in range(1 << dimension): + answers, rows = [], [] + for stage in range(dimension): + row = 1 << stage + for earlier in range(stage): + if answers[earlier] ^ (stage % 2): + row ^= 1 << earlier + answer = (row & point).bit_count() % 2 + rows.append(row) + answers.append(answer) + require(len(binary_span(rows, dimension)) == 1 << (stage + 1), + "adaptive triangular independence") + key = tuple(answers) + require(key not in transcripts, "full adaptive transcript collision") + transcripts[key] = point + prefixes.setdefault(key[:-1], []).append(point) + leaves += 1 + for values in prefixes.values(): + require(len(values) == 2 and values[0] != values[1], "short adaptive fiber") + failures += 1 + return {"full_transcripts": leaves, "short_ambiguous_fibers": failures} + + +def capacity_rows(): + rows = [] + for ports, cap in ((104, 3), (112, 4)): + demand, requests = 15 * ports, 528 + high = demand - (cap - 1) * requests + require(0 <= high <= requests, "capacity histogram feasibility") + capacities = [cap] * high + [cap - 1] * (requests - high) + require(sum(capacities) == demand, "capacity histogram equality") + require(sum(capacities) - 1 < demand, "one fewer dimension must fail") + rows.append({"ports": ports, "demand": demand, "requests": requests, + "maximum_capacity": cap, "minimum_maximum_capacity_calls": high, + "lower_capacity_calls": requests - high, + "scalar_side_information_needed": demand - requests}) + require(rows[0]["demand"] == 1560 and rows[1]["demand"] == 1680, + "conditional application arithmetic") + return rows + + +def controls(): + require(not fiber_decodable((), (15,), (1, 2, 4, 8), 4), "support/rank confusion") + correlated = {(bit, bit, bit, bit) for bit in (0, 1)} + require(len({row[0] for row in correlated}) == len(correlated), "correlation escape") + require(fiber_decodable((), (1, 2, 4, 8), (1, 2, 4, 8), 4), "vector output escape") + require(fiber_decodable((8,), (1, 2, 4), (1, 2, 4, 8), 4), "free-side-info escape") + rejected = 0 + for function, args in ((binary_span, ((16,), 4)), + (binary_span, ((), 9)), + (subspaces, (5,)), + (rational_rank, ([[1, 2]], 1))): + try: + function(*args) + except ValueError: + rejected += 1 + require(rejected == 4, "boundary rejection controls") + return {"semantic": 4, "invalid_inputs": rejected} + + +def source_hashes(package): + hashes = {} + for name in ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py"): + with (package / name).open("rb") as stream: + data = stream.read(1_048_577) + require(len(data) <= 1_048_576, "source file exceeds one MiB") + hashes[name] = hashlib.sha256(data).hexdigest() + return hashes + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a new hash-bound receipt outside the package") + args = parser.parse_args() + report = {"claim_type": "scoped-proof", "binary_census": census(), + "rational_fixtures": direct_sum_fixtures(), + "adaptive": adaptive_fixtures(), "conditional_capacity": capacity_rows(), + "controls": controls()} + package = Path(__file__).resolve().parent + report["source_sha256"] = source_hashes(package) + if args.receipt: + destination = args.receipt.resolve() + require(not destination.is_relative_to(package), "receipt must be outside package") + with destination.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(report, indent=2, sort_keys=True) + "\n") + print("PASS_CROSS_PORT_THIN_CAPACITY " + json.dumps(report, sort_keys=True)) + + +if __name__ == "__main__": + main()