From 61dac6c54e2be2e486a61da40ffeb0d2db743773 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:06:34 +0000 Subject: [PATCH] feat(research): prove sharp one-pass child batching storage --- research/low-type-stream-buffer/PROOF.md | 138 ++++++++++ research/low-type-stream-buffer/README.md | 73 +++++ research/low-type-stream-buffer/SOURCES.json | 35 +++ research/low-type-stream-buffer/TASK.json | 102 +++++++ research/low-type-stream-buffer/VERIFY.json | 34 +++ research/low-type-stream-buffer/verify.py | 270 +++++++++++++++++++ 6 files changed, 652 insertions(+) create mode 100644 research/low-type-stream-buffer/PROOF.md create mode 100644 research/low-type-stream-buffer/README.md create mode 100644 research/low-type-stream-buffer/SOURCES.json create mode 100644 research/low-type-stream-buffer/TASK.json create mode 100644 research/low-type-stream-buffer/VERIFY.json create mode 100644 research/low-type-stream-buffer/verify.py diff --git a/research/low-type-stream-buffer/PROOF.md b/research/low-type-stream-buffer/PROOF.md new file mode 100644 index 0000000000..765a9d8f32 --- /dev/null +++ b/research/low-type-stream-buffer/PROOF.md @@ -0,0 +1,138 @@ +# Sharp one-pass storage for whole-high child batches + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Contract + +Let n,L,s be positive integers. An input stream consists of independent +symbols x[u,l,a], in lexicographic order (u,l,a), where 0<=u=2. Storage means retained +payload information. Every payload-dependent buffer, register, control state, +cursor or address is charged. Fixed schedule counters carry no payload +information and are separate overhead. At a fixed input cut, a retained-state +family of cardinality A^b requires at least b alphabet-symbol equivalents, +or b*log2(A) bits. An unbounded integer cell does not have unit capacity here. +This convention permits arbitrary lossless encodings; it does not assume +that the dispatcher stores literal symbols. Timing is not an external channel. + +## Theorem + +The least possible worst-cut retained payload capacity is exactly + + B = (n-1)(L-1)s. + +A fixed schedule attains B with B literal symbol slots and deterministic +address/control overhead. Thus the result also gives the exact slot bound +in the usual indivisible-record buffer model. It is not a physical tape-time +bound, a native-cell bound for infinite alphabets, or a supplier theorem. + +## Lower bound + +Consider the cut after the first n-1 complete input cycles, immediately +before reading the final cycle. The n=1 or L=1 case has B=0 and needs +only the nonnegativity bound, so assume n,L>=2. + +The dispatcher has not seen x[n-1,0,0]. Correctness for every independent +payload prevents it from emitting that symbol before reading it. Since +output order is fixed, no symbol with l>0 has been emitted yet. + +Fix every l=0 symbol and every final-cycle symbol to one alphabet element. +Vary independently the B symbols with u0. There are A^B such +inputs. All already emitted output symbols have the same value. The +output length can vary, but any payload-dependent output cursor is part +of the charged retained state. + +Two different choices cannot give the same retained state at this input cut. +Otherwise the unread suffix is identical, as are the already emitted output +and its cursor. Determinism would give identical remaining output. Correct +outputs differ at an l>0 symbol, a contradiction. Consequently at least +A^B retained states are required. This counts compressed representations +and payload-dependent control as well as explicit buffers. + +The statement is for exact deterministic dispatch. It does not assert a +bound for randomized approximate recovery or a write-only output channel +that also communicates hidden timing information to another controller. + +## Attaining schedule + +During the first n-1 cycles, emit the l=0 chunk as it arrives and retain +every l>0 chunk. The retained size after k whole cycles is k(L-1)s, +so it never exceeds B. On the final cycle, emit its l=0 chunk directly. +For l=1,...,L-1 in order, first emit and release all retained chunks of +that type in increasing u order, then read and directly emit its final-cycle +chunk. No new retained symbols are required. The buffer ends empty. + +There are nLs input reads and nLs output writes. This counts stream +events only. Accessing the retained chunks in the required order may +require physical movement, indexing or extra tapes, which are unpriced. +For n=1 or L=1, input already has the required order and direct bypass +uses zero payload slots. + +## Delayed-cover substitution + +Ali Romman's PR #5829 at f1e522fc26371617ed60dea3c4609d422d491d2e supplies +the declared whole-high batch address contract. We cite that contract; we +do not replay its address proof. In its notation, at depth j1 and increasing n_j, +the buffer fraction tends to (L-1)/L. A sublinear buffer in V_j cannot +implement this particular one-pass, sequential-child interface in that limit. + +This does not refute #5829's O(V_j) local-space premise. It supplies a +necessary term for one implementation of its still-open dispatcher. Multiple +independently writable child streams, another input pass, random access, +interleaved child execution or a changed parent order can evade the contract. +No assertion is made that the current caller requires this interface. + +## Finite evidence and implementation limits + +The verifier executes literal streams, an independent output-prefix cut +oracle and a minimax dynamic program over every legal read/emit interleaving +for every permutation through length seven. It checks the closed form on +all n,L,s in {1,...,8}, actual binary payloads on a declared complete small +domain, injective binary cut states, algebraic cover substitutions, and +subcritical and malformed-input rejection. The universal claim follows +from the preceding proof, not from the finite bounds. + +The Python code is a simulator, not a measured physical buffer implementation. +Its input, output log and optional snapshots are checker instrumentation. +Only the simulated retained dictionary contributes to its reported payload +peak. It deliberately contains no predecessor imports or scientific replay. + +Power-of-ten rule 3 deviation: CPython and its standard library allocate +managed objects dynamically, including integers and checker logs. Streams +are validated at at most 4096 symbols with signed 64-bit payloads. Production +simulation dictionaries, logs and snapshots have at most 4096 entries each; +the scheduling oracle is called only through size seven, with at most 64 +cells. Cut-state sets have at most 1024 states of at most ten pairs each. +All search loops have explicit finite ranges, functions are below 60 lines, +and checks raise normally under optimized Python. Warning-strict normal and +optimized runs provide the available interpreter diagnostics. A physical +fixed-capacity implementation and its allocator diagnostics remain future work. diff --git a/research/low-type-stream-buffer/README.md b/research/low-type-stream-buffer/README.md new file mode 100644 index 0000000000..a1570fd849 --- /dev/null +++ b/research/low-type-stream-buffer/README.md @@ -0,0 +1,73 @@ +# Exact payload storage for one-pass child batching + +This contribution was produced by Nick Petalas. Apache-2.0. + +For n repeated input cycles, L low types and s symbols per type per cycle, +one forward input pass that emits complete child batches sequentially needs +exactly + + (n-1)(L-1)s + +alphabet-symbol equivalents of retained payload information. The lower bound +permits arbitrary lossless encodings and charges payload-dependent controller +state. An explicit schedule attains it with literal symbol slots. Claim type: +scoped written proof with finite corroboration. See [PROOF.md](PROOF.md). + +This answers one restricted version of the physical-dispatcher question in +[Ali Romman's PR #5829](https://github.com/CrocSwap/integer-mult-bounds/pull/5829), +at head f1e522fc26371617ed60dea3c4609d422d491d2e. Its whole-high batch address +contract is the cited predecessor, not an audited deliverable. At its depth j, +put n_j=T*(L*H)^(D-j-1) and s_j=H^(j+1)*R. The new storage term is +((L-1)/L)*(1-1/n_j)*V_j. The L=2,H=2,T=1,D=2,j=0,R=1 fixture +requires exactly six retained symbols for a sixteen-symbol parent. + +This is an explicit linear-storage term for the stated interface. It does +not refute the predecessor's O(V_j) premise or prove that a physical caller +must use this interface. Multiple writable child streams, rereads, random +access and changed traversal orders are outside scope. Unbounded integer +or exact-complex cells do not have unit information capacity in this model. +Physical movement, numerical precision, native execution, cleanup and the +complete supplier bill remain open. No new kappa or frontier change is claimed. + +## Reproduction + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/low-type-stream-buffer/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/low-type-stream-buffer/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/low-type-stream-buffer +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/low-type-stream-buffer --check-source-history +``` + +Any CPython 3.12 path can replace the local interpreter path. Direct success +prints PASS_LOW_TYPE_STREAM_BUFFER. The verifier checks complete domains +declared in its functions, independent prefix and scheduling oracles, actual +payload outputs, cut-state injectivity and rejection controls. It can write +a generated receipt with --receipt /absolute/path/outside/package.json; +the receipt binds all six package files by SHA256. No generated evidence +is stored in this package. Independent human and formal proof-kernel review +are unclaimed. + +The source manifest pins the task and selected record as historical provenance. +The PR #5829 contract is a cited mathematical premise, recorded separately +with its exact head, paths and hashes; it is not a runtime or Git-history +dependency. No pending predecessor code is imported or fetched during replay. + +## Open next questions + +- Can the final compiled template emit into multiple independently writable + child streams while retaining complete arbitrary-input return and a smaller + local buffer? Start with the sixteen-symbol fixture. Physical stream count, + head placement, return order and a complete movement bill are the blockers. +- What time and storage bill does a literal fixed-tape implementation of the + attaining one-pass schedule incur? Start by charging the six-slot fixture's + retained-chunk reads and releases. A source-bound dispatcher and its cleanup + contract are still required. + +Credit Ali Romman for PR #5829's whole-high batch address contract and open +dispatcher question, Mason Hale for its recursive-allocation predecessor, +and the retained BIT/compiler/cover authors credited there. Streaming +permutation cuts and the elementary information-counting method are classical. +The new contribution is the sharp buffering result for this declared interface, +its delayed-cover substitution, attaining schedule and standalone corroboration. diff --git a/research/low-type-stream-buffer/SOURCES.json b/research/low-type-stream-buffer/SOURCES.json new file mode 100644 index 0000000000..9d6b151e94 --- /dev/null +++ b/research/low-type-stream-buffer/SOURCES.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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" + } + ], + "cited_mathematical_contract": { + "pr": 5829, + "author": "Ali Romman", + "head": "f1e522fc26371617ed60dea3c4609d422d491d2e", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5829", + "role": "Cited address contract and open dispatcher question; no runtime dependency, imported code, or predecessor verification claim.", + "documents": [ + { + "path": "research/delayed-cover-batch-allocation/README.md", + "sha256": "559bee7010e02a436a67528a1b2580881e1d5b7567a66cceb7fe86ae9ba3c557" + }, + { + "path": "research/delayed-cover-batch-allocation/PROOF.md", + "sha256": "adab55de97f1336a58922b2fc92782af335a94a36cbaae34d6d3314d18a882ea" + } + ] + } +} diff --git a/research/low-type-stream-buffer/TASK.json b/research/low-type-stream-buffer/TASK.json new file mode 100644 index 0000000000..33226c7985 --- /dev/null +++ b/research/low-type-stream-buffer/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp retained payload storage for a one-pass parent stream emitting complete low-type child batches sequentially, with the delayed-cover address substitution.", + "scope_change_reason": "The donor requests original work rather than another audit. The formal-interface card is changed to a scoped written dispatcher-storage theorem, not proof-assistant formalization or predecessor verification.", + "bottleneck_link": "Prices one missing local-space term in the delayed-cover physical dispatcher; it does not discharge the full precision_tape assumption.", + "budget_minutes": 60, + "stop_rule": "Ship the first sharp buffer bound with an attaining schedule and independent finite checks; do not extend the model.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; generated receipts live outside the checkout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can multiple independently writable child streams reduce this buffer with complete return?", + "why_it_matters": "The sharp bound depends on one sequential child-output stream.", + "first_step": "Implement the sixteen-symbol, six-buffer fixture with two writable child streams.", + "blocked_by": "Physical stream count, head placement, source binding and full movement/return bill." + }, + { + "question": "What literal fixed-tape cost realizes the attaining one-pass schedule?", + "why_it_matters": "An information bound is not a complete time or physical storage implementation.", + "first_step": "Charge all reads and releases for the six-slot fixture.", + "blocked_by": "A source-bound dispatcher, head movement and cleanup contract." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216164" +} diff --git a/research/low-type-stream-buffer/VERIFY.json b/research/low-type-stream-buffer/VERIFY.json new file mode 100644 index 0000000000..0ad35cd930 --- /dev/null +++ b/research/low-type-stream-buffer/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal batches, all permutations through length seven, independent prefix/minimax scheduling oracles, binary payloads, information-cut injection and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same full finite evidence with interpreter assertions disabled." + } + ] +} diff --git a/research/low-type-stream-buffer/verify.py b/research/low-type-stream-buffer/verify.py new file mode 100644 index 0000000000..97baa70449 --- /dev/null +++ b/research/low-type-stream-buffer/verify.py @@ -0,0 +1,270 @@ +#!/usr/bin/env python3 +"""Finite corroboration of the one-pass low-type buffer theorem. + +Produced by Nick Petalas. Apache-2.0. +The written proof supplies the universal claim. +""" +import argparse +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + +MAX_SYMBOLS = 4096 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def batch_order(n: int, low_types: int, chunk: int) -> tuple[int, ...]: + require(all(type(x) is int and 1 <= x <= MAX_SYMBOLS + for x in (n, low_types, chunk)), "invalid dimensions") + require(n * low_types * chunk <= MAX_SYMBOLS, "stream too large") + return tuple((cycle * low_types + low) * chunk + offset + for low in range(low_types) for cycle in range(n) + for offset in range(chunk)) + + +def validate_stream(payload: tuple[int, ...], order: tuple[int, ...], + capacity: int, cut: int) -> None: + size = len(payload) + require(type(payload) is tuple and 0 <= size <= MAX_SYMBOLS, + "invalid payload length or container") + require(all(type(x) is int and -(1 << 63) <= x < (1 << 63) + for x in payload), "invalid payload symbol") + require(type(order) is tuple and len(order) == size + and all(type(x) is int for x in order) + and set(order) == set(range(size)), "invalid permutation") + require(type(capacity) is int and 0 <= capacity <= size, "invalid capacity") + require(type(cut) is int and 0 <= cut <= size, "invalid cut") + + +def dispatch(payload: tuple[int, ...], order: tuple[int, ...], capacity: int, + cut: int = 0) -> tuple[tuple[int, ...], int, tuple[tuple[int, int], ...]]: + """Simulate one read stream, append-only output and bounded payload slots. + + Output is an observation log unavailable to the simulated controller. + Ready arriving symbols bypass storage. The cut snapshot is instrumentation. + """ + validate_stream(payload, order, capacity, cut) + retained: dict[int, int] = {} + output: list[int] = [] + snapshot: tuple[tuple[int, int], ...] = () + peak = 0 + for index, symbol in enumerate(payload): + if order[len(output)] == index: + output.append(symbol) + else: + require(len(retained) < capacity, "payload capacity exhausted") + retained[index] = symbol + peak = max(peak, len(retained)) + for _ in range(len(payload) - len(output)): + wanted = order[len(output)] + if wanted not in retained: + break + output.append(retained.pop(wanted)) + require(len(retained) == index + 1 - len(output), "lost payload") + if index + 1 == cut: + snapshot = tuple(sorted(retained.items())) + require(not retained and len(output) == len(payload), "incomplete dispatch") + return tuple(output), peak, snapshot + + +def prefix_oracle(order: tuple[int, ...]) -> int: + """Count read indices outside the longest available output prefix.""" + size = len(order) + peak = 0 + for read in range(size + 1): + prefix = size + for rank, index in enumerate(order): + if index >= read: + prefix = rank + break + peak = max(peak, read - prefix) + return peak + + +def schedule_oracle(order: tuple[int, ...]) -> int: + """Minimax over every legal read/emit interleaving, with direct bypass.""" + size = len(order) + best = [[size + 1] * (size + 1) for _ in range(size + 1)] + best[0][0] = 0 + for read in range(size + 1): + for written in range(size + 1): + old = best[read][written] + if old > size: + continue + if written < size and order[written] < read: + best[read][written + 1] = min(best[read][written + 1], old) + if read == size: + continue + best[read + 1][written] = min( + best[read + 1][written], max(old, read + 1 - written)) + if written < size and order[written] == read: + best[read + 1][written + 1] = min( + best[read + 1][written + 1], max(old, read - written)) + return best[size][size] + + +def check_permutations() -> int: + count = 0 + for size in range(8): + payload = tuple(range(size)) + for order in permutations(payload): + output, peak, _ = dispatch(payload, order, size) + require(output == order, "wrong literal permutation") + require(peak == prefix_oracle(order) == schedule_oracle(order), + "independent scheduling disagreement") + count += 1 + return count + + +def check_batches() -> tuple[int, int]: + count = rejected = 0 + for n, low_types, chunk in product(range(1, 9), repeat=3): + order = batch_order(n, low_types, chunk) + expected = (n - 1) * (low_types - 1) * chunk + payload = tuple(range(len(order))) + output, peak, _ = dispatch(payload, order, expected) + require(output == order and peak == expected == prefix_oracle(order), + "batch theorem disagreement") + if expected: + try: + dispatch(payload, order, expected - 1) + except ValueError as error: + require(str(error) == "payload capacity exhausted", "wrong rejection") + rejected += 1 + else: + raise ValueError("subcritical buffer accepted") + count += 1 + return count, rejected + + +def check_payloads() -> int: + count = 0 + for n, low_types, chunk in product(range(1, 5), range(1, 5), range(1, 4)): + size = n * low_types * chunk + if size > 12: + continue + order = batch_order(n, low_types, chunk) + capacity = (n - 1) * (low_types - 1) * chunk + for payload in product((0, 1), repeat=size): + output, peak, _ = dispatch(payload, order, capacity) + require(output == tuple(payload[index] for index in order) + and peak == capacity, "payload corruption") + count += 1 + return count + + +def check_information_cut() -> tuple[int, int]: + families = states = 0 + for n, low_types, chunk in product(range(2, 5), range(2, 5), range(1, 4)): + capacity = (n - 1) * (low_types - 1) * chunk + if capacity > 10: + continue + order = batch_order(n, low_types, chunk) + cut = (n - 1) * low_types * chunk + hidden = tuple((cycle * low_types + low) * chunk + offset + for cycle in range(n - 1) for low in range(1, low_types) + for offset in range(chunk)) + require(len(hidden) == capacity, "wrong cut dimension") + seen = set() + for bits in product((0, 1), repeat=capacity): + payload = [0] * len(order) + for index, bit in zip(hidden, bits, strict=True): + payload[index] = bit + output, _, snapshot = dispatch(tuple(payload), order, capacity, cut) + require(output == tuple(payload[index] for index in order), "bad cut output") + require(tuple(index for index, _ in snapshot) == hidden, + "wrong retained cut indices") + require(snapshot not in seen, "noninjective retained information") + seen.add(snapshot) + states += 1 + require(len(seen) == 2 ** capacity, "missing cut state") + families += 1 + return families, states + + +def check_cover_substitution() -> int: + count = 0 + for low_types, high, slabs, depth, body in product( + range(1, 6), range(1, 5), range(1, 5), range(1, 9), range(1, 5)): + for level in range(depth): + n = slabs * (low_types * high) ** (depth - level - 1) + chunk = high ** (level + 1) * body + volume = slabs * (low_types * high) ** depth * body // low_types ** level + buffer = (n - 1) * (low_types - 1) * chunk + require(n * low_types * chunk == volume, "inconsistent source dimensions") + require(low_types * buffer + == (low_types - 1) * (volume - low_types * chunk), + "incorrect normalized buffer") + count += 1 + return count + + +def check_rejections() -> int: + cases = ( + ((0, 1), (0, 0), 2, 0), ((0, 1), (0, 2), 2, 0), + ((0, 1), (True, 0), 2, 0), ((0, 1), (0,), 2, 0), + ((0, 1), (0, 1), -1, 0), ((0, 1), (0, 1), 3, 0), + ((0, 1), (0, 1), 2, 3), ((0, 1), (0, 1), True, 0), + ((0, 1 << 63), (0, 1), 2, 0), ((False, 1), (0, 1), 2, 0), + ) + for payload, order, capacity, cut in cases: + try: + dispatch(payload, order, capacity, cut) + except ValueError: + pass + else: + raise ValueError("invalid stream accepted") + for args in ((0, 2, 1), (True, 2, 1), (17, 17, 17), (1, -1, 1)): + try: + batch_order(*args) + except ValueError: + pass + else: + raise ValueError("invalid dimensions accepted") + return len(cases) + 4 + + +def verify() -> dict: + batches, exhausted = check_batches() + families, states = check_information_cut() + return { + "status": "PASS_LOW_TYPE_STREAM_BUFFER", + "permutations": check_permutations(), + "batch_shapes": batches, + "subcritical_capacity_rejections": exhausted, + "binary_payloads": check_payloads(), + "information_cut_families": families, + "distinct_information_cut_states": states, + "cover_parameter_substitutions": check_cover_substitution(), + "invalid_input_rejections": check_rejections(), + "claim_type": "scoped written proof; finite corroboration", + } + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + report = verify() + root = Path(__file__).resolve().parent + report["package_sha256"] = { + name: sha256((root / name).read_bytes()).hexdigest() + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + } + encoded = json.dumps(report, sort_keys=True, indent=2) + "\n" + if args.receipt: + require(not args.receipt.resolve().is_relative_to(root), + "receipt must stay outside package") + require(args.receipt.write_text(encoded, encoding="utf-8") == len(encoded), + "incomplete receipt write") + print(encoded, end="") + + +if __name__ == "__main__": + main()