diff --git a/research/weighted-pending-fanout/PROOF.md b/research/weighted-pending-fanout/PROOF.md new file mode 100644 index 0000000000..4c1131c316 --- /dev/null +++ b/research/weighted-pending-fanout/PROOF.md @@ -0,0 +1,201 @@ +# Exact weighted pending-capacity tariff + +This scoped written proof was produced by Nick Petalas. Apache-2.0. + +## Contract + +Retain Sagar Thakrar's PR1168 common-source fanout alphabet. Arrays +`x,z,y_1,...,y_k` start arbitrarily and are distinct. Exact characteristic-zero +linear maps `B,A_1,...,A_k` need not commute. A fixed word must universally +realize + +```text +x unchanged, z unchanged, y_i += A_i B x for every i. +``` + +The only paid root queries, with `s` equal to `+1` or `-1`, are + +```text +B^s: z += s B x +A_i^s: y_i += s A_i z. +``` + +Each is a complete source-preserving, spectator-preserving, private-work +restoring, head-returning query. Their implementations and complete prices +are premises. Inverse queries have the same positive fixed price as forward +queries. There is no direct product query, combined output query, free copy, +output-to-output query, changing source, frame change or overwritten helper. +Universality over the admissible maps is essential to the lower bound. +Special zero maps or relations among maps can admit shorter words. + +An output is unfinished from its first readout query until its permanent +commit. Commit requires the correct all-input value. No later query may +touch it. Unstarted and committed outputs do not count toward the pending +capacity; they remain reserved arrays and are not reusable child scratch. + +The new hypothesis is that output i has positive integer reservation weight +`w_i`, and at every query boundary + +```text +sum_(i unfinished) w_i <= C, +``` + +where C is a positive integer. A commit can occur at a complete-query return. +Weights are declared lifetime reservations. Unequal physical payload widths +or a memory-saving theorem do not follow from this abstract contract. + +## Theorem + +Let `b(w,C)` be the smallest number of bins partitioning the outputs, with +total weight at most C in each bin; put `b(empty,C)=0`. If every `w_i<=C`, +the coordinatewise simultaneous minimum query counts are + +```text +N_Ai = 2 for every i, +N_B = 2 ceil(b(w,C)/2). +``` + +Consequently every positive fixed sign-symmetric complete query price gives + +```text +Q_min = 2 sum_i c_Ai + 2 ceil(b(w,C)/2) c_B. +``` + +If an output has `w_i>C`, no universally correct word exists: it cannot even +be opened. The empty problem has the empty optimum. The theorem is uncapped; +the reference implementation deliberately accepts at most ten outputs. + +## Lower bound for arbitrary words + +Use Ross Richardson's PR938 coefficient state, as retained by PR1168: + +```text +z = z_initial + q B x, +y_i = y_i_initial + e_i A_i z_initial + f_i A_i B x. +``` + +Initially `q=e_i=f_i=0`. A signed B query changes q by s. A signed A_i query +changes `(e_i,f_i)` by `(s,s*q)`. Universal correctness implies final +`q=0,e_i=0,f_i=1`. Necessity already follows by specializing all maps to the +scalar identity and varying initial x and z independently. These coefficient +facts and summation by parts are credited premises, not new audit claims. + +Since each readout changes e_i by a unit, and f_i must change, at least two +readouts of each output are necessary. Since q starts and ends at zero, +the number of B queries is even. + +The discrete product rule gives, for each output, + +```text +1 = f_i(final) = - sum_(B queries) e_i(before query) * delta(q). +``` + +Indeed, an A_i query contributes `q delta(e_i)` both to `delta(e_i q)` and +to `delta(f_i)`, while a B query contributes `e_i delta(q)` only to the +former. The endpoint product is zero. Thus every output has nonzero e_i +immediately before at least one B query. Such an output is unfinished: +before its first readout e_i is zero, and a correct permanent commit has +e_i zero with no later changes. + +Assign each output to one such B query, for example the earliest one. The +outputs assigned to a single event are a subset of its unfinished outputs, +so their total weight is at most C. Nonempty assigned sets partition all +outputs into at most N_B feasible bins. Hence `b(w,C)<=N_B`. Combining this +with evenness gives the stated B lower bound. This argument permits extra +readouts, arbitrary integer excursions of q and e_i, overlapping lifetimes, +idle intervals and any commit order. It does not assume the emitted word. + +## Attainment + +Choose any optimal bin partition `G_0,...,G_(b-1)`. Start with q=0 and, for +bin j, set `s=(-1)^j` and emit + +```text +for i in G_j: A_i^(-s) +B^s +for i in G_j: A_i^s; commit i +``` + +Let z_before be the connector immediately before the B query. Output i +receives exactly + +```text +-s A_i z_before + s A_i(z_before+s Bx) = A_i Bx. +``` + +Only that bin's outputs are unfinished during this block. Every one commits +before the next bin opens. The capacity is legal, all readout counts equal +two, and q alternates between zero and one. If b is odd, append one B^(-1) +after all commits. Otherwise nothing is appended. The connector returns +exactly and the B count is `b+(b mod 2)`. This attains every lower bound +simultaneously, and therefore every declared positive complete price. + +## A strict obstruction to total-weight pricing + +Take `w=(3,3,3,3,3,1)` and `C=5`. The five weight-three outputs must occupy +different bins, and the weight-one output can join any one. Therefore b=5 +and exactly six B calls are needed, together with twelve readouts. The +total-weight relaxation gives only four B calls, since total weight is 16 +and `2 ceil(ceil(16/5)/2)=4`. + +For declared complete prices `c_B=52` and `c_Ai=1`, the correct optimum is +324, whereas that relaxation prices only 220. These are abstract query +prices. They are not the physical primitive prices of a selected supplier. +The new result is the exact packing obstruction and its matching scheduler. +No optimality claim is made over larger query alphabets. + +## Algorithms and finite evidence + +The subset dynamic program stores `d[mask]`, the minimum bins covering that +mask. The bin containing its least item is some feasible submask S containing +that item; remove S and use `1+d[mask xor S]`. Enumerating all such S is exact +and reconstructs an attaining partition. There are O(3^k) arithmetic checks +and O(2^k) table entries. This is exponential in output count, not a claimed +polynomial optimization algorithm. + +An independent oracle successively puts each weight into every feasible +existing bin or a new bin and keeps all distinct sorted load tuples. Labels +of bins can be forgotten because all later feasibility decisions depend +only on loads. This enumerates every feasible packing up to identical loads. +The two methods agree on the fixed multiset domain recorded in the receipt. + +Every emitted schedule in that domain is also executed by ordinary integer +matrix arithmetic on all basis columns of every arbitrary initial row. +Each A_i and B is a literal two-by-two matrix; a checked pair does not +commute. The interpreter checks every commit, every pending-weight boundary, +both unchanged source rows and all outputs. It does not use the coefficient +state to compute its endpoint. + +A separate breadth-first word search checks four weighted three-output +contracts. It considers both signed B queries and every legal signed readout, +without a packing bound, proposed tariff or restrictions on extra readouts. +It searches increasing unit-query lengths through ten. Complete shortest +layers and total distinct state counts appear in the generated receipt. + +Two exact quotients keep that search finite without discarding a better +word. Simultaneously negating q and every e_i, while preserving f_i, is a +sign symmetry of its queries and endpoint. Also, an output reaching +`(e_i,f_i)=(0,1)` can commit immediately: delete all its later readouts from +any successful continuation. Other outputs and the connector do not read +it, its own correct final value remains correct, and reserved pending +capacity only decreases. Thus an optimum exists with these greedy commits. +This proves the search covers a shortest word, even though it does not count +all words or all commit annotations. + +## Remaining obligations + +Predecessor private-work, coefficient preparation and fixed-tape routines +are cited contracts, not executed or admitted here. If I denotes admission, +P denotes reusable preparation and D denotes schedule construction, control +and program access not already included in complete query prices, the full +declared bill is `I+P+D+Q_min`. Packing computation belongs in D when needed; +an optimal packing is not a free runtime oracle. + +This result supplies neither a physical reservation assignment nor an +actual selected producer/consumer. Nonlinear operations, finite-field +torsion, free output mixing, state-dependent prices, release of output +storage, coefficient traffic, native frames, precision, owned erasure, +stock, compiler closure and outer transfer need separate contracts. All five +selected framework assumptions remain. No kappa, selected-frontier update +or complete multiplication theorem follows. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/weighted-pending-fanout/README.md b/research/weighted-pending-fanout/README.md new file mode 100644 index 0000000000..afac6c4a3e --- /dev/null +++ b/research/weighted-pending-fanout/README.md @@ -0,0 +1,164 @@ +# Exact dirty-fanout tariff under weighted pending capacity + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof and constructive scheduler with exact finite +corroboration. If unfinished output i reserves positive integer weight w_i +under capacity C, let b be the minimum bin count for those weights. In the +signed common-source query alphabet with permanent commits, the exact bill is + +```text +N_Ai = 2 for every output, +N_B = 2 ceil(b/2), +Q_min = 2 sum_i c_Ai + 2 ceil(b/2) c_B. +``` + +The new step replaces Sagar Thakrar's [PR1168](https://github.com/CrocSwap/integer-mult-bounds/pull/1168) +cardinality cap by unequal lifetime reservations. The proof covers arbitrary +longer words and gives an attaining schedule. The unweighted formula is a +cited predecessor result. No predecessor executable is imported or replayed. + +For weights `(3,3,3,3,3,1)` and capacity 5, the five large outputs require +different bins. Exactly six shared-source calls and twelve readouts are +necessary and sufficient. Pricing capacity by total weight alone permits +four shared-source calls. At declared complete prices `c_B=52,c_Ai=1`, that +relaxation gives 220 while the exact optimum is 324. These are abstract query +prices, not physical primitive counts or a runtime benchmark. + +## Contract and construction + +Arrays x,z,y_i are initially arbitrary. The only queries are +`z += s Bx` and `y_i += s A_i z`, where s is +1 or -1. Every query preserves +its source, spectators and private work and returns its heads. The fixed +word must work universally for characteristic-zero linear maps A_i,B and +all initial arrays, with endpoint `y_i += A_i Bx`, x,z unchanged. Commutation +and invertibility of the maps are not required. Special relations or zero +maps can change the optimum for a particular instance. + +An output is unfinished from its first readout until a correct permanent +commit. No later query touches it. The sum of unfinished weights may never +exceed C. Storage of unstarted and committed outputs is retained, not freed +as scratch. Weights declare a scheduling resource; the theorem does not +identify them with physical memory or unequal payload widths. + +Partition outputs into optimal feasible bins. For consecutive bins alternate +s=+1,-1 and emit + +```text +for i in bin: readout_i(-s) +shared_source(s) +for i in bin: readout_i(s); commit i +``` + +If the bin count is odd, append one inverse shared-source query. Each bin +finishes before the next opens. [PROOF.md](PROOF.md) proves that every output +must be active at some shared-source query; assigning it to such an event +gives a feasible bin packing. Restoration forces an even query count. + +## Reproduce + +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/weighted-pending-fanout/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/weighted-pending-fanout/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/weighted-pending-fanout +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/weighted-pending-fanout --check-source-history +``` + +Another CPython 3.12 path can replace the local interpreter. Direct replay +prints `PASS_WEIGHTED_PENDING_FANOUT` in a generated JSON receipt binding all +six package files by SHA256. It writes nothing and needs neither Git nor a +predecessor package. The source manifest pins the retained README and notice +as historical provenance, not live executable inputs. No receipt is handwritten. + +The fixed finite domain contains all weight multisets of length zero through +six with weights in 1..C, at C=1..6. Its 1,715 contracts compare subset dynamic +programming with independent enumeration of feasible bin-load states. Every +emitted schedule is executed on all basis columns of every arbitrary initial +array by literal two-by-two integer maps. A checked pair is noncommuting. +The executor checks all commits and capacity boundaries, source and connector +restoration, and every target. It executes 24,126 complete queries in this +domain; 144 contracts strictly exceed the total-weight bound rounded up to +an even integer. + +Four separate breadth-first searches over signed query words have minima +10,8,8,8 for weights `(2,2,2)`, `(1,2,2)`, `(1,1,2)`, `(1,2,3)`, all at +capacity 3. The searches visit 11,416, 36,719, 54,041 and 20,093 distinct +states, respectively, including all layers through the shortest endpoint. +They use neither the packing optimizer nor its proposed price to prune +words. The proof justifies sign symmetry and immediate correct commits. +Eighteen rejecting controls cover invalid resource domains, incomplete or +overweight bins, a missing restore, premature/late output access, a changed +source-query sign and an invalid instruction. A ten-output maximum-capacity +fixture exercises the implementation's boundary. The universal theorem +rests on the written argument, not these finite checks. + +## Limits and implementation constraints + +This reference accepts at most ten outputs and integer capacity at most +65,536. The optimal packing computation is exponential in output count, +using O(3^k) arithmetic checks and O(2^k) table entries. An implementation +must pay packing preparation or supply a separately justified packing. +Admission, reusable coefficient preparation, schedule/control storage and +access add to the complete query bill; they are not set to zero here. + +There is no recursion, subprocess, network, dynamic evaluation or verifier +write path. Functions fit within 60 physical lines. Packing has at most +1,024 table entries; independent load enumeration has at most 203 states; +word search has depth at most ten and at most 100,000 distinct stored states. +The literal executor has at most 24 basis columns and 44 instructions. +Six file reads are capped at 256 KiB each. Explicit exception checks remain +active under `-O`. Normal and optimized warning-strict commands are registered. + +Power of Ten rule 3 has a managed-runtime deviation: Python integers, tuples, +sets and matrices allocate dynamically. The enforced dimensions and search +bounds limit live data; runtime allocator overhead is not instrumented. +Rule 9 has a bounded control-callback deviation: eighteen immediately executed +rejection callbacks call only packing, emit or literal. They retain no state. +AST compilation and warning-strict execution supply local diagnostics. No +separate lint/type analyzer or fixed-allocation native runtime is claimed. + +No selected producer/consumer or physical reservation assignment is supplied. +Nonlinear maps, finite-characteristic torsion, free output mixing, changing +sources, state-dependent tariffs, output-storage reuse and adaptive data-based +words are outside the theorem. Native frames, precision/tapes, owned erasure, +stock, compiler closure and outer transfer remain separate obligations. All +five selected assumptions remain. No kappa, selected-frontier update, complete +multiplication theorem, independent human review or proof-kernel acceptance +is claimed. Selected cold replay, native suites, Lean and Docker are unrun. + +## Credit and scope + +Sagar Thakrar / PR1168 at `b53b07b5aed4e00358a0d0061ad99dbf5190ca2b` supplies +the unfinished-output and permanent-commit interface and its unweighted +all-word lower bound. Ross Richardson / PR938 supplies the coefficient state +and equality-word context. CubeJerry / PR889 supplies shared dirty-source +fanout and complete accounting; Chafik Boukhalfa / PR628 supplies the retained +commutator lineage. The selected native/compiler contributors retain their +existing attribution. Classical bin packing, dynamic programming, summation +by parts and linearity are background; global literature priority is unclaimed. + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +[TASK.json](TASK.json) explicitly changes the uniform-transfer-audit card to +this recursive-interface side theorem. It does not discharge a selected +assumption. Selected-baseline orientation passed and is source binding only. +Discovery stopped at this first verified result. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375366) +followed live handoffs, active Discussions, open/account PRs, local reservations +and main/merged searches for weighted pending capacity, bin packing and general +fanout formulas. Sparse cached notes and unpublished work remain coverage +limits. No absence of overlap is claimed as a novelty certificate. + +## Open next questions + +- Bind one actual common-source caller to proved reservation weights and a + favorable full invoice. Start with its exact lifetimes and include query + implementation, packing, control, restoration and movement. No such caller + or physical reservation assignment is supplied. +- Find a useful caller weight family with an exact cheaper packing algorithm. + Start with a source-bound restriction on its weights; the present general + reference is exponential and schedule preparation must be paid. + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). diff --git a/research/weighted-pending-fanout/SOURCES.json b/research/weighted-pending-fanout/SOURCES.json new file mode 100644 index 0000000000..d37db7b3a9 --- /dev/null +++ b/research/weighted-pending-fanout/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bounded-pending-fanout-seed53/README.md", + "usage": "provenance", + "git_blob": "636098ae1b909c013c35515d4f9049c732b0e363", + "sha256": "0f71af68bf84ace97ee6e9543c9ac22390546c6713e0f2360f3e49383fd2b49f" + }, + { + "path": "research/bounded-pending-fanout-seed53/NOTICE.md", + "usage": "provenance", + "git_blob": "64d83fbb3cb27a361c77763cac4eea8df24e0a43", + "sha256": "6b55ed6abad13b2be3ede9373e1503a88238afa8b41cf3ab7e8e4f551863cad4" + } + ] +} diff --git a/research/weighted-pending-fanout/TASK.json b/research/weighted-pending-fanout/TASK.json new file mode 100644 index 0000000000..871963cf28 --- /dev/null +++ b/research/weighted-pending-fanout/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Exact complete query tariff for universally correct dirty fanout under unequal weighted unfinished-output reservations and permanent commits.", + "scope_change_reason": "Original recursive-interface side theorem extends external PR1168 from a cardinality cap to weighted capacity. It does not audit a predecessor or discharge a selected assumption.", + "bottleneck_link": "Physical callers with unequal lifetime reservations cannot price common-source sharing by total weight alone; an actual supplier binding and complete invoice remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact tariff, matching scheduler and independent finite corroboration.", + "outcome": "completed", + "evidence": "PROOF.md; standalone exact packing, integer endpoint and bounded word-search checks in verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual common-source caller justify unequal reservation weights and fit this tariff into a favorable full invoice?", + "why_it_matters": "The abstract capacity is not physical memory, and the selected native word may not expose this alphabet.", + "first_step": "Pin one literal producer/consumer, assign weights from its lifetime contract and include every complete query, packing, control, restoration and movement cost.", + "blocked_by": "No actual selected caller or paid reservation assignment is supplied." + }, + { + "question": "Can a useful caller family supply an optimal packing without exponential schedule preparation?", + "why_it_matters": "Packing computation is charged in the full schedule bill.", + "first_step": "Specify a source-bound restricted weight family and construct an exact polynomial-time packing algorithm for that family.", + "blocked_by": "No restriction on the general integer weights is assumed here." + } + ], + "verification_environment": { + "implementation": "CPython", + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "dependencies": "standard library only" + } +} diff --git a/research/weighted-pending-fanout/VERIFY.json b/research/weighted-pending-fanout/VERIFY.json new file mode 100644 index 0000000000..5b7eea81a8 --- /dev/null +++ b/research/weighted-pending-fanout/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": "Exact weighted packing, all-dirty integer endpoint, every commit/capacity, bounded all-query word search and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical scientific checks with assertions disabled; explicit exceptions retain all guards." + } + ] +} diff --git a/research/weighted-pending-fanout/verify.py b/research/weighted-pending-fanout/verify.py new file mode 100644 index 0000000000..c2b601caac --- /dev/null +++ b/research/weighted-pending-fanout/verify.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""Exact weighted-capacity fanout construction and independent finite checks.""" + +import hashlib +import json +from itertools import combinations_with_replacement +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def domain(weights, capacity): + require(type(weights) is tuple and len(weights) <= 10, "weight vector") + require(type(capacity) is int and 1 <= capacity <= 65536, "capacity") + require(all(type(w) is int and 1 <= w <= capacity for w in weights), + "positive fitting weights") + + +def packing(weights, capacity): + """Minimum bins by subset DP; the least item fixes each bin's position.""" + domain(weights, capacity) + size = 1 << len(weights) + mass = [0] * size + count = [len(weights) + 1] * size + chosen = [0] * size + count[0] = 0 + for mask in range(1, size): + bit = mask & -mask + mass[mask] = mass[mask ^ bit] + weights[bit.bit_length() - 1] + sub = mask + for _ in range(size): + if sub & bit and mass[sub] <= capacity: + candidate = 1 + count[mask ^ sub] + if candidate < count[mask]: + count[mask], chosen[mask] = candidate, sub + sub = (sub - 1) & mask + if sub == 0: + break + require(chosen[mask] != 0, "fitting singleton must exist") + bins, mask = [], size - 1 + for _ in range(len(weights)): + if mask == 0: + break + sub = chosen[mask] + bins.append(tuple(i for i in range(len(weights)) if sub >> i & 1)) + mask ^= sub + require(mask == 0 and len(bins) == count[-1], "partition reconstruction") + return tuple(bins) + + +def emit(weights, capacity, bins): + domain(weights, capacity) + require(type(bins) is tuple and len(bins) <= len(weights), "bin list") + require(all(type(group) is tuple and len(group) <= len(weights) + for group in bins), "bounded groups") + flat = tuple(i for group in bins for i in group) + require(all(type(i) is int and 0 <= i < len(weights) for i in flat), + "output indices") + require(sorted(flat) == list(range(len(weights))), "partition coverage") + require(all(group and sum(weights[i] for i in group) <= capacity + for group in bins), "bin capacity") + program = [] + for j, group in enumerate(bins): + sign = 1 if j % 2 == 0 else -1 + program.extend(("A", i, -sign) for i in group) + program.append(("B", -1, sign)) + for i in group: + program.extend((("A", i, sign), ("C", i, 0))) + if len(bins) % 2: + program.append(("B", -1, -1)) + require(len(program) <= 4 * len(weights) + 1, "program size") + return tuple(program) + + +def independent_bins(weights, capacity): + """Enumerate all feasible unlabeled bin-load states, at most Bell(6).""" + require(len(weights) <= 6, "independent enumeration domain") + states = {()} + for weight in weights: + following = set() + for loads in states: + following.add(tuple(sorted(loads + (weight,)))) + for j, load in enumerate(loads): + if load + weight <= capacity: + updated = loads[:j] + (load + weight,) + loads[j + 1:] + following.add(tuple(sorted(updated))) + require(len(following) <= 203, "Bell-number state bound") + states = following + return min(map(len, states)) + + +def product(left, right): + return tuple(tuple(sum(left[i][k] * right[k][j] for k in range(2)) + for j in range(len(right[0]))) for i in range(2)) + + +def add_to(target, source, sign): + return tuple(tuple(x + sign * y for x, y in zip(a, b)) + for a, b in zip(target, source)) + + +def literal(weights, capacity, program): + """Execute all basis columns together using ordinary integer matrices.""" + domain(weights, capacity) + n, width = len(weights), 2 * (len(weights) + 2) + initial = tuple(tuple(tuple(int(2 * p + i == j) for j in range(width)) + for i in range(2)) for p in range(n + 2)) + rows, life = list(initial), [0] * n + bmap = ((1, 2), (-1, 1)) + amap = tuple(((i + 1, -1), (2, i)) for i in range(n)) + targets = tuple(add_to(initial[i + 2], product(amap[i], + product(bmap, initial[0])), 1) for i in range(n)) + require(type(program) is tuple and len(program) <= 4 * n + 4, + "literal instruction limit") + require(all(type(row) is tuple and len(row) == 3 for row in program), + "instruction shape") + peak = bcount = acount = 0 + for op, i, sign in program: + require(op in ("A", "B", "C"), "instruction alphabet") + if op == "B": + require(i == -1 and sign in (-1, 1), "B contract") + rows[1] = add_to(rows[1], product(bmap, rows[0]), sign) + bcount += 1 + else: + require(0 <= i < n and life[i] != 2, "committed target touched") + if op == "C": + require(sign == 0 and life[i] == 1, "commit lifecycle") + require(rows[i + 2] == targets[i], "premature commit") + life[i] = 2 + else: + require(sign in (-1, 1), "A sign") + life[i] = 1 + rows[i + 2] = add_to(rows[i + 2], product(amap[i], rows[1]), sign) + acount += 1 + used = sum(w for w, state in zip(weights, life) if state == 1) + require(used <= capacity, "unfinished weight exceeds capacity") + peak = max(peak, used) + require(rows[:2] == list(initial[:2]), "source or connector not restored") + require(all(state == 2 for state in life), "missing commit") + require(tuple(rows[2:]) == targets, "wrong full endpoint") + return acount, bcount, peak + + +def canonical(q, rows): + signs = (q,) + tuple(e for _, e, _ in rows) + first = next((v for v in signs if v), 0) + if first < 0: + return -q, tuple((life, -e, f) for life, e, f in rows) + return q, rows + + +def successors(state, weights, capacity): + q, rows = state + active = sum(w for w, (life, _, _) in zip(weights, rows) if life == 1) + answer = [] + for sign in (-1, 1): + answer.append(canonical(q + sign, rows)) + for i, (life, e, f) in enumerate(rows): + if life == 2 or (life == 0 and active + weights[i] > capacity): + continue + e1, f1 = e + sign, f + sign * q + life1 = 2 if (e1, f1) == (0, 1) else 1 + changed = rows[:i] + ((life1, e1, f1),) + rows[i + 1:] + answer.append(canonical(q, changed)) + return answer + + +def word_minimum(weights, capacity): + """Breadth-first all-unit-query search, without packing or bill pruning.""" + domain(weights, capacity) + require(len(weights) <= 3, "word-search output bound") + start = (0, ((0, 0, 0),) * len(weights)) + layer, seen, sizes = {start}, {start}, [] + for depth in range(11): + sizes.append(len(layer)) + if any(q == 0 and all(life == 2 for life, _, _ in rows) + for q, rows in layer): + return depth, len(seen), sizes + following = set() + for state in layer: + for item in successors(state, weights, capacity): + if item not in seen: + following.add(item) + require(len(following) + len(seen) <= 100000, + "word-search state bound") + seen.update(following) + layer = following + raise ValueError("word-search depth exhausted") + + +def family_checks(): + cases = calls = peak_sum = fragmented = 0 + digest = hashlib.sha256() + for capacity in range(1, 7): + for n in range(7): + for weights in combinations_with_replacement(range(1, capacity + 1), n): + bins = packing(weights, capacity) + require(len(bins) == independent_bins(weights, capacity), + "independent packing disagreement") + program = emit(weights, capacity, bins) + acount, bcount, peak = literal(weights, capacity, program) + require(acount == 2 * n, "readout count") + require(bcount == 2 * ((len(bins) + 1) // 2), "B count") + volume = (sum(weights) + capacity - 1) // capacity + fragmented += bcount > 2 * ((volume + 1) // 2) + cases, calls, peak_sum = cases + 1, calls + acount + bcount, peak_sum + peak + digest.update(json.dumps([weights, capacity, bins, program]).encode()) + return dict(cases=cases, literal_calls=calls, peak_sum=peak_sum, + strict_volume_obstructions=fragmented, trace_sha256=digest.hexdigest()) + + +def rejected(action): + try: + action() + except ValueError: + return 1 + raise ValueError("negative control accepted") + + +def controls(): + count = 0 + for weights, cap in [((0,), 2), ((-1,), 2), ((3,), 2), ((True,), 2), + ((1,), 0), ((1,), True), ((1,), 65537), + ((1,) * 11, 2), ([1], 2), ((1.0,), 2)]: + count += rejected(lambda w=weights, c=cap: packing(w, c)) + weights, cap = (2, 2, 2), 3 + count += rejected(lambda: emit(weights, cap, ((0, 1), (2,)))) + count += rejected(lambda: emit(weights, cap, ((0,), (1,), (1,)))) + program = emit(weights, cap, packing(weights, cap)) + count += rejected(lambda: literal(weights, cap, program[:-1])) + count += rejected(lambda: literal(weights, cap, (("C", 0, 0),) + program)) + count += rejected(lambda: literal(weights, cap, program + (("A", 0, 1),))) + over_capacity = (("A", 0, -1), ("A", 1, -1)) + count += rejected(lambda: literal(weights, cap, over_capacity)) + changed = list(program) + index = next(j for j, row in enumerate(changed) if row[0] == "B") + changed[index] = ("B", -1, -changed[index][2]) + count += rejected(lambda: literal(weights, cap, tuple(changed))) + count += rejected(lambda: literal(weights, cap, (("X", 0, 1),))) + require(product(((1, -1), (2, 0)), ((1, 2), (-1, 1))) != + product(((1, 2), (-1, 1)), ((1, -1), (2, 0))), "noncommuting fixture") + return count + + +def main(): + result = family_checks() + word_cases = [] + for weights, capacity in [((2, 2, 2), 3), ((1, 2, 2), 3), + ((1, 1, 2), 3), ((1, 2, 3), 3)]: + minimum, states, layers = word_minimum(weights, capacity) + bins = packing(weights, capacity) + predicted = 2 * len(weights) + 2 * ((len(bins) + 1) // 2) + require(minimum == predicted, "independent word-search disagreement") + word_cases.append(dict(weights=weights, capacity=capacity, minimum=minimum, + states=states, layers=layers)) + fixture = (3, 3, 3, 3, 3, 1) + bins = packing(fixture, 5) + actual = literal(fixture, 5, emit(fixture, 5, bins)) + require(len(bins) == 5 and actual[:2] == (12, 6), "fragmentation witness") + require(52 * actual[1] + actual[0] == 324, "weighted query bill") + boundary = (65536,) * 10 + require(literal(boundary, 65536, emit(boundary, 65536, + packing(boundary, 65536)))[:2] == (20, 10), "maximum domain") + result.update(word_searches=word_cases, controls=controls(), + witness=dict(weights=fixture, capacity=5, bins=bins, + readouts=12, shared_calls=6, price=324)) + package = Path(__file__).resolve().parent + hashes = {} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + with (package / name).open("rb") as stream: + data = stream.read(262145) + require(len(data) <= 262144, "package file-size bound") + hashes[name] = hashlib.sha256(data).hexdigest() + print(json.dumps(dict(status="PASS_WEIGHTED_PENDING_FANOUT", result=result, + source_sha256=hashes), sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()