diff --git a/research/contiguous-helper-storage-gap/README.md b/research/contiguous-helper-storage-gap/README.md new file mode 100644 index 0000000000..4848049785 --- /dev/null +++ b/research/contiguous-helper-storage-gap/README.md @@ -0,0 +1,144 @@ +# Exact contiguous helper storage: 5q versus peak 4q + +For the eight fixed half-open lifetimes below, each width multiplied by any +positive real q, the minimum capacity for one fixed contiguous block per helper +is exactly **5q**. Freely split fixed slot sets need exactly **4q**. Thus even +complete advance knowledge of the lifetimes leaves a 25% contiguous-storage +surcharge and an additive gap q. + +This is a scoped mathematical proof with finite corroboration. It gives an +explicit obstruction at the contiguous-block boundary excluded by Ali Romman's +[PR #5763](https://github.com/CrocSwap/integer-mult-bounds/pull/5763), head +`cee2336bc3a20c586b1dbb55152d97a114c657a6`. That allocator permits separated +ranges. Its theorem and implementation are cited, not audited or rerun here. +The general dynamic storage allocation problem is classical; this package +contributes this explicit scaled family and its exact optimum, not the general +observation that contiguity can cost space. + +## Contract and instance + +An address range is half-open. A helper keeps its assigned address range or +ranges throughout its lifetime. Simultaneously live helpers must have disjoint +address sets. Addresses lie in [0,H). Allocation before the run may use all +lifetimes. Movement during a lifetime is excluded. There is no alignment +restriction. With integer q, all displayed endpoints are integer addresses. + +The table gives times, widths divided by q, a contiguous capacity-5q layout, +and a split capacity-4q layout. Every displayed address is multiplied by q. + +| Helper | Lifetime | Width | Contiguous range | Split ranges | +|---|---|---:|---|---| +| A | [0,8) | 1 | [0,1) | [0,1) | +| B | [2,12) | 1 | [1,2) | [1,2) | +| C | [4,14) | 1 | [4,5) | [2,3) | +| D | [6,10) | 1 | [2,3) | [3,4) | +| X | [0,2) | 3 | [1,4) | [1,4) | +| Y | [2,4) | 2 | [2,4) | [2,4) | +| Z | [10,12) | 2 | [2,4) | [0,1), [3,4) | +| W | [12,14) | 3 | [0,3) | [0,2), [3,4) | + +The loads on the successive intervals starting at times 0,2,4,6,8,10,12 +are 4q,4q,3q,4q,3q,4q,4q. Hence the split layout attains the necessary peak +capacity 4q. The contiguous column directly proves an upper bound of 5q. + +## Lower bound for arbitrary real addresses + +First set q=1. Any real contiguous layout can be compressed to an integer +layout of no greater capacity. Order all helpers by their original bottom +address, breaking ties arbitrarily. For each helper in that order, put its new +bottom at the maximum new top among its earlier time-overlapping neighbors, +or at zero if there are none. These bottoms are integers. Induction shows that +each new bottom is at most its original bottom: each earlier overlapping top +was originally below this helper's original bottom. Every overlapping pair +keeps its order and remains disjoint. Therefore every new top is at most the +corresponding original top. + +If a real layout had H<5, this compression would give integer capacity at most +4. A,B,C,D are simultaneously live on [6,8). Their four unit blocks must +therefore fill the four cells 0,1,2,3. + +1. X has width 3 and overlaps A. Thus A occupies an end cell. +2. W has width 3 and overlaps C. Thus C occupies the other end cell, since A + and C overlap each other. +3. Y has width 2 and overlaps A,B. Its two cells are exactly the eventual + C,D cells, which must therefore be adjacent. +4. Z has width 2 and overlaps B,C. Its two cells are exactly the eventual + A,D cells, which must therefore be adjacent. + +D cannot be adjacent to both end cells of a four-cell line. This contradiction +excludes every H<5, including noninteger addresses. The displayed layout attains +5. Dividing all widths and addresses by any positive real q reduces the general +case to q=1, so the optimum is 5q. + +No claim of a smallest obstruction by helper count, a worst-case approximation +ratio, or novelty of the general storage-allocation phenomenon is made. + +## Evidence and reproduction + +From the repository root, use CPython 3.12. The verifier needs only its standard +library and writes no files unless `--receipt` is supplied. + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/contiguous-helper-storage-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/contiguous-helper-storage-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/contiguous-helper-storage-gap +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/contiguous-helper-storage-gap --check-source-history +``` + +Expected marker: `PASS_CONTIGUOUS_HELPER_STORAGE_GAP`. The replay checks both +layouts and every event load; all 8! = 40320 total address orders with exact +longest-path compression; and, independently, all 9216 integer placements at +capacity 4. The order enumeration returns minimum capacity 5. Exact rational +scales and invalid-layout controls check scaling, collisions, contiguity and the +half-open boundary. Normal and optimized commands use explicit checks, not +Python assertions. An optional generated receipt binds the package file hashes. +The written proof supplies the unbounded positive-real quantifier; the finite +checks do not replace it. + +## Relation to current research + +The selected baseline command passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` +at main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. It reported +selected kappa .00310045 and admitted BIT saving .0034. This was orientation, +not a supplier replay. The random picker suggested portable replay work; the +explicit boundary in #5763 supplied this mathematical side question instead. +The original card is preserved in TASK.json with `scope_status: changed`. + +The result prevents a peak-width certificate from being transferred silently +to a fixed contiguous native interface. It does not establish that a selected +supplier requires contiguous blocks, infer any actual supplier's storage bill, +construct routes or cleanup, optimize chronology, or improve kappa. Physical +ownership, restoration, tape movement, precision and all-size compiler premises +remain outside the claim. No predecessor scientific replay was run. + +## Open next questions + +- Can one actual native caller use split fixed ranges with its complete route + and address-description bill? Start with a source-pinned helper access trace + and lower each split access. Safe lifetimes and a declared native interface + are prerequisites. +- Can a restricted family of native helper lifetimes always attain peak width + with contiguous blocks? First identify a source-derived interval restriction + that excludes the eight-helper pattern. No such source restriction is assumed + here. + +The corresponding structured questions are in TASK.json. The first exact gap +was retained without expanding the construction search. + +## Credit and implementation bounds + +This result was produced by Nick Petalas. Ali Romman supplied #5763's split-range +interface and its explicit contiguity boundary. Its context credits the T74 pool +of #2655 and the owned-lifetime audit #5717; those results are not needed by this +self-contained proof. The general model is classical dynamic storage allocation, +as described by [Naor, Orda and Petruschka, 2000](https://cris.technion.ac.il/en/publications/dynamic-storage-allocation-with-known-durations-4/). +No predecessor code is copied. Apache-2.0. + +The verifier uses no recursion or dynamic dispatch. Its finite inputs have eight +helpers, at most two address segments per helper, seven time slabs, 40320 total +orders and 9216 coordinate assignments. Each function stays below 60 lines. +Python allocates integers, tuples and dictionaries during replay, so fixed +allocation in Power of Ten rule 3 is a managed-runtime deviation. The enumerated +domains bound live state; no list of all orders or layouts is retained. Warning- +strict normal and optimized replays provide the available runtime diagnostics. +A static native implementation would require a separate fixed-storage review. diff --git a/research/contiguous-helper-storage-gap/SOURCES.json b/research/contiguous-helper-storage-gap/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/contiguous-helper-storage-gap/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/contiguous-helper-storage-gap/TASK.json b/research/contiguous-helper-storage-gap/TASK.json new file mode 100644 index 0000000000..20a950b4e5 --- /dev/null +++ b/research/contiguous-helper-storage-gap/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "portable-replay", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "portable-replay", + "question": "Can one reproducible environment or artifact-comparison failure be repaired?", + "starting_points": [ + "research/gzip-container-reproducibility/README.md", + "docs/ci-verification.md" + ], + "methods": [ + "Reproduce one portability failure and add a minimal cross-environment fix.", + "Audit one canonical-payload comparison for omitted proof-relevant fields." + ], + "acceptance_gate": "Preserve immutable source hashes and proof-relevant content; a different compressed byte stream alone is not a mathematical mismatch.", + "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": "Reproduce one specific mismatch or audit one canonical comparison for omitted proof-relevant fields.", + "bottleneck_link": "Portable exact checks prevent environment failures from blocking valid contributions.", + "allowed_variations": [ + "One interpreter/version mismatch or one payload field comparison." + ], + "scope_change_triggers": [ + "Removing immutable-source pins because generated compressed bytes differ." + ], + "overlap_terms": [ + "gzip container", + "reproducibility", + "canonical payload" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact fixed-contiguous capacity of an explicit eight-helper family and compare its split-range optimum.", + "scope_change_reason": "The random card suggested portable replay work. The donor asks for an original mathematical result, so the explicit contiguous-block boundary of PR5763 supplies a self-contained storage-contract side question instead of an audit or portability repair.", + "bottleneck_link": "Side result: peak live width cannot certify fixed contiguous native storage. A source-specific physical bill must establish whether split ranges or movement are legal.", + "budget_minutes": 60, + "stop_rule": "Retain and package the first exact storage gap; do not expand the construction search.", + "outcome": "completed", + "evidence": "README.md proves 5q versus 4q for every positive real q. verify.py independently checks 40320 address orders, 9216 capacity-four placements, explicit layouts, rational scales and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual native caller use split fixed ranges with a complete route and address-description bill?", + "why_it_matters": "The split-range optimum is relevant only when the native interface and its charges permit it.", + "first_step": "Extract a source-pinned helper access trace and lower every split access.", + "blocked_by": "Safe source lifetimes and a declared native address and movement contract are not supplied here." + }, + { + "question": "Which source-derived lifetime restrictions guarantee a contiguous layout at peak width?", + "why_it_matters": "A genuine restriction could prevent the eight-helper obstruction in a particular supplier.", + "first_step": "Identify a structural restriction in one actual native trace and check whether it excludes this pattern.", + "blocked_by": "No source-specific lifetime restriction is assumed or proved in this package." + } + ], + "claim_type": "scoped mathematical proof with finite corroboration", + "predecessors": [ + { + "pr": 5763, + "author": "Ali Romman", + "head": "cee2336bc3a20c586b1dbb55152d97a114c657a6", + "use": "Question source and split-range interface context only; no predecessor implementation or theorem replay." + } + ] +} diff --git a/research/contiguous-helper-storage-gap/VERIFY.json b/research/contiguous-helper-storage-gap/VERIFY.json new file mode 100644 index 0000000000..063d1de047 --- /dev/null +++ b/research/contiguous-helper-storage-gap/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": "40320 exact address orders, independent 9216-position exclusion, both layouts, rational scales, half-open seams and malformed-layout rejection." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same mathematical corroboration and rejection controls under optimized Python." + } + ] +} diff --git a/research/contiguous-helper-storage-gap/verify.py b/research/contiguous-helper-storage-gap/verify.py new file mode 100644 index 0000000000..0a595c75e7 --- /dev/null +++ b/research/contiguous-helper-storage-gap/verify.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check the explicit eight-helper contiguous storage obstruction. + +Produced by Nick Petalas. General context: classical dynamic storage allocation; +Ali Romman PR5763 states the split-range interface boundary. No source is imported. +""" + +import argparse +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +import json +from math import factorial, prod +from pathlib import Path +import sys + + +# Times are fixed. The last component is width divided by the common scale q. +JOBS = ( + (0, 8, 1), (2, 12, 1), (4, 14, 1), (6, 10, 1), + (0, 2, 3), (2, 4, 2), (10, 12, 2), (12, 14, 3), +) +CONTIGUOUS = tuple(((x, x + row[2]),) for x, row in zip( + (0, 1, 4, 2, 1, 2, 2, 0), JOBS)) +SPLIT = ( + ((0, 1),), ((1, 2),), ((2, 3),), ((3, 4),), + ((1, 4),), ((2, 4),), ((0, 1), (3, 4)), ((0, 2), (3, 4)), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def time_overlap(left, right): + return max(left[0], right[0]) < min(left[1], right[1]) + + +def check_layout(jobs, segments, capacity, contiguous): + """Check widths, boundaries and pairwise occupied-set intersections.""" + require(len(jobs) == len(segments) == 8, "expected eight helpers") + require(capacity > 0, "capacity must be positive") + for i, (row, pieces) in enumerate(zip(jobs, segments)): + require(row[0] < row[1] and row[2] > 0, "invalid lifetime or width") + require(1 <= len(pieces) <= 2, "segment count outside bounded model") + require(not contiguous or len(pieces) == 1, "contiguity violated") + require(sum(b - a for a, b in pieces) == row[2], "width differs") + for a, b in pieces: + require(0 <= a < b <= capacity, "address outside capacity") + for left, right in zip(pieces, pieces[1:]): + require(left[1] <= right[0], "own segments intersect or unsorted") + for j in range(i): + if time_overlap(row, jobs[j]): + for a, b in pieces: + for c, d in segments[j]: + require(b <= c or d <= a, "live address collision") + + +def scaled_instance(q): + require(isinstance(q, (int, Fraction)) and q > 0, "positive rational scale required") + jobs = tuple((a, b, q * w) for a, b, w in JOBS) + contiguous = tuple(tuple((q * a, q * b) for a, b in row) for row in CONTIGUOUS) + split = tuple(tuple((q * a, q * b) for a, b in row) for row in SPLIT) + return jobs, contiguous, split + + +def check_scales(): + scales = (Fraction(1, 3), Fraction(1, 2), 1, 2, 7, 10**60) + expected_loads = (4, 4, 3, 4, 3, 4, 4) + for q in scales: + jobs, contiguous, split = scaled_instance(q) + check_layout(jobs, contiguous, 5 * q, True) + check_layout(jobs, split, 4 * q, False) + loads = tuple(sum(w for a, b, w in jobs if a <= t < b) + for t in range(0, 14, 2)) + require(loads == tuple(q * v for v in expected_loads), "event load differs") + require(max(loads) == 4 * q, "peak differs") + # Release at time 2 precedes allocation at time 2. + require(not time_overlap(JOBS[4], JOBS[5]), "half-open seam overlaps") + require(time_overlap(JOBS[0], JOBS[4]), "positive overlap omitted") + return len(scales) + + +def compressed_layout(order, jobs): + """Earliest addresses for the overlap orientation induced by a total order.""" + require(len(jobs) == 8 and sorted(order) == list(range(8)), "invalid order") + bottoms = [0] * 8 + for k, i in enumerate(order): + bottoms[i] = max((bottoms[j] + jobs[j][2] for j in order[:k] + if time_overlap(jobs[i], jobs[j])), default=0) + capacity = max(bottoms[i] + jobs[i][2] for i in range(8)) + segments = tuple(((bottoms[i], bottoms[i] + jobs[i][2]),) for i in range(8)) + check_layout(jobs, segments, capacity, True) + return capacity, segments + + +def check_all_orders(): + minimum = sum(row[2] for row in JOBS) + count = 0 + for order in permutations(range(8)): + capacity, _segments = compressed_layout(order, JOBS) + require(capacity >= 5, "found order below the proved minimum") + minimum = min(minimum, capacity) + count += 1 + require(count == factorial(8) == 40320, "incomplete address-order enumeration") + require(minimum == 5, "contiguous optimum differs") + return count, minimum + + +def check_integer_exclusion(): + """Independent coordinate enumeration, without the compression recurrence.""" + choices = tuple(range(5 - row[2]) for row in JOBS) + require(prod(len(c) for c in choices) == 9216, "coordinate domain differs") + count = 0 + for bottoms in product(*choices): + legal = True + for i in range(8): + for j in range(i): + if time_overlap(JOBS[i], JOBS[j]): + legal = legal and (bottoms[i] + JOBS[i][2] <= bottoms[j] + or bottoms[j] + JOBS[j][2] <= bottoms[i]) + require(not legal, "found capacity-four coordinate placement") + count += 1 + require(count == 9216, "incomplete integer-coordinate enumeration") + return count + + +def check_controls(): + collision = list(CONTIGUOUS) + collision[3] = ((1, 2),) + wrong_width = list(CONTIGUOUS) + wrong_width[4] = ((1, 3),) + cases = ( + (CONTIGUOUS, 4, True, "capacity"), + (tuple(collision), 5, True, "collision"), + (tuple(wrong_width), 5, True, "width"), + (SPLIT, 4, True, "contiguity"), + ) + for segments, capacity, contiguous, expected in cases: + try: + check_layout(JOBS, segments, capacity, contiguous) + except ValueError as error: + require(expected in str(error), "control failed for another reason") + else: + raise ValueError("invalid layout accepted: " + expected) + # Reverse order exercises the opposite orientation of every overlap edge. + reverse_capacity, _segments = compressed_layout(tuple(reversed(range(8))), JOBS) + require(reverse_capacity >= 5, "reverse order violates minimum") + return len(cases) + + +def package_hashes(): + package = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result = {} + for name in names: + with (package / name).open("rb") as stream: + raw = stream.read(1024 * 1024 + 1) + require(len(raw) <= 1024 * 1024, "package file exceeds byte bound") + result[name] = sha256(raw).hexdigest() + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write the generated hash-bound report") + args = parser.parse_args() + scales = check_scales() + order_count, minimum = check_all_orders() + coordinates = check_integer_exclusion() + controls = check_controls() + report = { + "status": "PASS_CONTIGUOUS_HELPER_STORAGE_GAP", + "claim_type": "scoped mathematical proof with finite corroboration", + "unit_contiguous_minimum": minimum, + "unit_split_minimum": 4, + "address_orders_checked": order_count, + "capacity_four_coordinates_checked": coordinates, + "rational_scales_checked": scales, + "invalid_layout_controls_rejected": controls, + "python": sys.version.split()[0], + "package_sha256": package_hashes(), + "scope": "Fixed eight-helper family. Positive-real scaling is proved in README.md. " + "No physical supplier, source cleanup, kappa or complete multiplication theorem.", + } + payload = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + require(args.receipt.resolve().parent.is_dir(), "receipt parent does not exist") + written = args.receipt.write_text(payload, encoding="utf-8") + require(written == len(payload), "short receipt write") + print(payload, end="") + + +if __name__ == "__main__": + main()