From cd08b0157410c9c023bf9c5d87a1a6ad3963506a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 15:10:38 +0000 Subject: [PATCH] feat(research): solve small-codimension partial query acquisition --- research/partial-query-optimum/ENGINEERING.md | 72 +++++ research/partial-query-optimum/PROOF.md | 128 ++++++++ research/partial-query-optimum/README.md | 117 ++++++++ research/partial-query-optimum/SOURCES.json | 24 ++ research/partial-query-optimum/TASK.json | 95 ++++++ research/partial-query-optimum/VERIFY.json | 36 +++ research/partial-query-optimum/optimizer.py | 277 ++++++++++++++++++ research/partial-query-optimum/verify.py | 209 +++++++++++++ 8 files changed, 958 insertions(+) create mode 100644 research/partial-query-optimum/ENGINEERING.md create mode 100644 research/partial-query-optimum/PROOF.md create mode 100644 research/partial-query-optimum/README.md create mode 100644 research/partial-query-optimum/SOURCES.json create mode 100644 research/partial-query-optimum/TASK.json create mode 100644 research/partial-query-optimum/VERIFY.json create mode 100644 research/partial-query-optimum/optimizer.py create mode 100644 research/partial-query-optimum/verify.py diff --git a/research/partial-query-optimum/ENGINEERING.md b/research/partial-query-optimum/ENGINEERING.md new file mode 100644 index 0000000000..b4aead9e8c --- /dev/null +++ b/research/partial-query-optimum/ENGINEERING.md @@ -0,0 +1,72 @@ +# Implementation bounds + +The exit predicate is a proved exact acquisition reduction, a bounded +constructor and certificate checker agreeing with exhaustive subset optima, +followed by one focused publication. The autonomous local run playbook was +used. Build the Lever led to the reusable optimizer and certificate checker. +Prove It Works led to literal subset and vector-set oracles and actual CLI +replays, rather than inference from certificate self-consistency. + +## Code inspection + +The scope is optimizer.py and verify.py. All control flow is structured, +without recursion, dynamic code generation, network access, mutable global +caches or background tasks. Optimizer entry points validate width at most +256, at most 4096 queries and 256 target vectors, integer costs in +0..10^12, target inclusion in the query span, and codimension at most four. +Booleans are rejected as integer inputs. + +There are at most 67 candidate subspaces. Producer span-extension layers +number at most five and contain at most 67 canonical bases; each tries at +most 15 new vectors. The independent checker enumerates at most 16 pivot +sets and at most 16 free-entry assignments per set. A subspace vector set +has at most 16 elements. Per-candidate elimination retains at most 256 rows. +Dual construction reduces 256 ambient unit vectors. Input and certificate +files are limited to eight million bytes. Certificates retain at most +67*256 selected indices and dual vectors. No search-budget exhaustion is +reported as mathematical infeasibility. + +The finite oracle uses at most seven queries, 128 subsets, eight vector +values and 2187 cost assignments. The separate subspace oracle scans at +most 32768 subsets containing zero and tests at most 256 XOR pairs each. +CLI checks launch three serial subprocesses with 30-second timeouts, wait +for their completion and inspect their return codes. Temporary files are +owned by one context-managed directory and removed on every normal or +exceptional exit. Set TMPDIR to the run's scratch directory for local replay. + +Explicit exception checks remain active under optimized Python. They check +source hashes, target coverage, dual independence, eligible coverage, +cheapest-basis exchanges, missing-target separators, complete quotient +enumeration and the final minimum. The checker reconstructs actual vectors; +it does not trust a reported rank or price. Malformed input rejects before +optimization. Failed checks propagate; scientific success is never cached. + +All application functions fit within approximately sixty physical lines. +Shared helpers operate on small explicit values; certificate verification +does not call the optimizer. Both registered commands use isolated Python, +warnings as errors and disabled bytecode writes. The direct and registered +replays exercise the real optimizer and CLI. No external static analyzer or +proof-kernel verification is claimed. + +## Managed-runtime deviation + +Rule: Power of Ten rule 3, allocation before steady operation. + +Location: optimizer.py and verify.py. + +Reason: CPython dynamically allocates arbitrary-precision integers, lists, +sets and dictionaries. This exact one-shot program cannot disable runtime +allocation while retaining its Python interface. + +Scope: bounded constructor, checker and finite corroboration only. + +Compensating control: enforced input caps, at most 67 candidate certificates, +at most 256 rows per elimination and one current exhaustive instance. No +unbounded queue, recursive stack or persistent cache exists. + +Verification: maximum-width/query-count case, maximum-codimension case, +oversize rejection, exhaustive oracles and subprocess timeout checks. + +Follow-up: any native steady-operation implementation must allocate fixed +capacity storage before taking over this interface. That implementation is +outside this result. diff --git a/research/partial-query-optimum/PROOF.md b/research/partial-query-optimum/PROOF.md new file mode 100644 index 0000000000..421d0c7c2f --- /dev/null +++ b/research/partial-query-optimum/PROOF.md @@ -0,0 +1,128 @@ +# Exact acquisition by quotient superspaces + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and result + +Let K be a finite field of order q. Let v_1,...,v_n be vectors with +nonnegative real acquisition costs a_i. Acquiring a subset S permits free +linear reconstruction from its span. Let V=span(v_i), let U be a specified +target subspace of V, and put c=dim(V)-dim(U). Costs are charged once per +acquired index. Zero vectors, duplicates, zero costs, an empty query pool +and U=0 are allowed. + +For every R<=V/U, let W_R be its inverse image under the quotient map, let +E_R={i : v_i in W_R}, and let T_R=span(v_i : i in E_R). Compute a cheapest +basis B_R from the indices E_R for T_R. Discard R if U is not contained +in T_R. Then + + OPT(U) = min_R sum_{i in B_R} a_i, + +over the retained candidates. There are exactly + + N_q(c) = sum_{k=0}^c product_{j=0}^{k-1} (q^c-q^j)/(q^k-q^j) + +candidates. The number of weighted-basis problems depends only on target +codimension. The empty product is one. For q=2 and c=0,1,2,3,4 the counts +are 1,2,5,16,67. The executable covers q=2 and c<=4. + +This is an exact algorithm for additive acquisition. The finite-field +restriction concerns bounded enumeration. The underlying reduction holds +over any field if all superspaces can be considered. No polynomial bound +in c, physical reconstruction cost or new multiplication exponent is asserted. + +## Proof of the reduction + +Every retained B_R spans U, so its acquisition is feasible and OPT(U) is at +most its cost. Conversely, let S be an optimal feasible acquisition and put +W=span(v_i : i in S). Since U<=W<=V, W is the inverse image of exactly one +quotient subspace R. All indices of S belong to E_R. Therefore T_R=W: +inclusion in W follows from eligibility, while the reverse inclusion follows +from S. Remove dependent vectors from S to obtain a basis of W. Nonnegative +costs ensure removal cannot increase cost. A cheapest basis B_R consequently +costs at most S. That candidate is retained and attains OPT(U). Finiteness +of the index set supplies an optimum, including at zero cost. There is always +a retained candidate at W=V. + +The basis need not have rank dim(U). Paying for extra independent directions +can be cheaper than buying queries entirely in U. It is also unnecessary +that eligible queries span the entire W_R. The algorithm uses their actual +span T_R and explicitly checks target coverage. + +## Counting and constructing quotient spaces + +The number of ordered independent k-tuples in K^c is product_j(q^c-q^j). +Each k-dimensional subspace has exactly product_j(q^k-q^j) ordered bases. +Division and summation prove N_q(c), the classical Gaussian binomial count. + +The constructor starts with the zero subspace and repeatedly adjoins every +vector outside each current subspace. Every extension increases rank, and +canonical reduced bases identify repetitions. Induction on rank proves +completeness. The checker uses a different enumeration: choose all pivot +positions, assign every permitted free entry in reduced row echelon form, +then enumerate the resulting vector set. Unique reduced forms prove that +it lists every quotient subspace exactly once. Both enumerations terminate +after c rank layers. A third finite corroboration scans all vector subsets +and tests closure under XOR for c<=4. + +To construct the quotient map, extend a basis of U to a basis of V and take +the coordinate forms of the added elements. The checker accepts any c forms +that vanish on U and map V onto K^c. Rank-nullity makes their kernel on V +exactly U, so they parameterize the same complete superspace family. No +favorable choice of quotient coordinates is assumed. + +## Checkable candidate optimality + +The binary certificate gives selected indices and dual forms d_j with +d_j(v_i)=delta_ji on selected vectors. This proves independence. For every +eligible v, the checker computes coordinates d_j(v), reconstructs v, and +checks that every used selected index has price at most the price of v. +The coordinates prove full eligible coverage and the absence of an improving +single-element basis exchange. + +That exchange condition implies global cheapest-basis optimality. At every +strict price threshold, all cheaper eligible vectors are spanned by cheaper +selected vectors. Thus the selected cheap prefix has the full rank of the +eligible cheap prefix. Every other basis contains at most that many cheap +vectors. Summing these rank inequalities over the finite distinct prices, +or pairing sorted basis prices, proves that every other basis costs at least +as much. This is classical weighted linear-matroid greedy optimality, +inherited from Ali Romman's PR5791 contract rather than a new matroid theorem. + +If a candidate cannot span U, its certificate supplies one target vector and +a linear functional that is one there and zero on every eligible query. +No eligible acquisition can obtain that target. Otherwise the checker +reconstructs every target from the selected basis. After checking all +quotient spaces, it checks the reported minimum. The certificate checker +does not rerun global subset optimization. + +## First strict improvement and an interior necessity example + +For queries (1,2,3), prices (3,2,2), and target U=span(1) in F2^2, a cheapest +whole-span basis buys 2 and 3 for four units. Both are needed to reconstruct +the target in that basis. The new optimizer buys query 1 for three units. +Here c=1, so only U and V are considered. + +For queries (1,2,3,4,7), prices (8,2,2,1,2), and target span(1) in F2^3, +queries entirely in U cost eight. A cheapest whole-span basis costs five. +The intermediate superspace span(1,2) has a four-unit basis (2,3), and four +is optimal. Every query costs at least one; the sole one-unit vector is 4, +and neither it nor any price-two vector is the target. A subset cheaper than +four cannot span 1: XOR with the sole one-unit vector 4 sends the +price-two vectors 2,3,7 to 6,7,3. This shows why considering only U and V is insufficient +once c=2. No predecessor numerical result is used for either example. + +## Attribution and scope + +Ali Romman / PR5791 supplies whole-span acquisition, the partial-target +question and its exchange certificate contract. Nick Petalas / PR5878 gives +the earlier sharp c+1 guarantee for pruning a cheapest whole-span basis. +The new step is the exact quotient-superspace reduction with a complete +bounded optimizer and certificate. Quotient spaces, rank-nullity, Gaussian +binomial counting and weighted matroid selection are classical tools. +No literature-wide priority for enumerative optimization is claimed. + +This does not price XOR reconstruction, physical delivery, restoration, +phase realization, storage or native legality. A source-to-query adapter, +complete signed supplier invoice and all-size caller remain separate proof +obligations. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/partial-query-optimum/README.md b/research/partial-query-optimum/README.md new file mode 100644 index 0000000000..d5c4fc914c --- /dev/null +++ b/research/partial-query-optimum/README.md @@ -0,0 +1,117 @@ +# Exact partial-query acquisition at small codimension + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: scoped written proof and constructive optimizer with exact finite +corroboration. Independent human and formal proof-kernel review are unclaimed. + +A target subspace U need not require the entire query span V. The new exact +reduction considers every superspace of U through V/U, buys a cheapest basis +of the queries eligible in that superspace, and takes the cheapest candidate +that spans U. For a finite field of order q and c=dim(V)-dim(U), the number +of candidates is the sum of the Gaussian binomial coefficients [c choose k]_q. +It depends on target codimension. For binary c=0,1,2,3,4, the exact counts +are 1,2,5,16,67. [PROOF.md](PROOF.md) proves the reduction for every finite +field and arbitrary finite query pools with nonnegative costs. + +The executable handles binary width through 256, at most 4096 queries and +256 target vectors, codimension through four, and integer prices through +10^12. Zero prices, duplicate/zero queries and empty targets are included. +The checker proves candidate independence, full eligible coverage and +cheapest-basis exchange optimality, or checks a missing-target separator. +An independent RREF enumeration checks that no quotient space was omitted. +The constructor uses span extension. Neither executes predecessor code. + +For queries 1,2,3 with prices 3,2,2 and target 1, whole-span basis pruning +pays four; the new optimum is three. At codimension two, an intermediate +superspace can beat both the target space and the whole space. The proof +gives a five-query example with respective optima eight, four and five. +These are acquisition prices in a declared algebraic relaxation. + +## Reproduce + +From the repository root, with the standard library and CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/partial-query-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/partial-query-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/partial-query-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/partial-query-optimum --check-source-history +``` + +Set TMPDIR to an existing private external scratch directory for the three +short CLI subprocess checks. Another CPython 3.12 path may replace the local +path. The scientific marker is PASS_PARTIAL_QUERY_OPTIMUM. Each replay +prints a generated receipt bound to all eight package files by SHA256 and +writes no persistent artifact. The registered runner executes both modes. + +For a new problem, write JSON with exactly these keys: + +```json +{"width":2,"vectors":[1,2,3],"costs":[3,2,2],"targets":[1]} +``` + +Run `python3.12 -I -B research/partial-query-optimum/optimizer.py problem.json` +and save stdout as certificate.json outside the checkout. Check that file +with the same command followed by `--check certificate.json`. The minimum +is three. Vectors are binary coordinate bitmasks encoded as JSON integers. +The target must lie in the query span; unsupported domains reject explicitly. +The certificate records all candidate bases, quotient forms and the winner. + +## Evidence and limits + +The complete finite replay compares every weighted seven-vector pool with +prices in 0,1,2 against every target subspace of F2^3. A second complete +family includes duplicate and zero queries. Its oracle enumerates purchased +index subsets and literal XOR spans, without Gaussian elimination. Three +independent quotient enumerators, malformed-input and certificate controls, +maximum width/query count and codimension, and actual CLI production/checking +are also exercised. The replay checks 36,207 exhaustive optima and 147,258 candidate bases, +nine corrupted certificates, ten invalid problems and three CLI runs. +The receipt reports these exact enumerated counts. + +The written argument establishes the quantified theorem. Finite evidence +corroborates the bounded implementation. [ENGINEERING.md](ENGINEERING.md) +states resource bounds and the managed-runtime allocation deviation. + +Linear reconstruction is free only in this acquisition model. XOR cost, +physical delivery, phases, borrowed-state restoration, owned storage, native +legality, precision, compiler closure and the full supplier/outer bill remain +separate. No native, selected cold, Lean or Docker replay, new kappa, +selected-frontier change or complete multiplication theorem is claimed. + +## Sources and overlap + +Ali Romman / [PR5791](https://github.com/CrocSwap/integer-mult-bounds/pull/5791) +poses partial-target acquisition separately from its whole-span optimum. +Its retained [guide](../../docs/research/binary-query-basis.md) is pinned as +an authenticated documentary input, without executing its implementation. +Nick Petalas / [PR5878](https://github.com/CrocSwap/integer-mult-bounds/pull/5878) +gives the earlier sharp c+1 approximation guarantee for pruning any cheapest +whole-span basis. That result is cited context, not replayed or audited. +Classical quotient spaces, rank-nullity, Gaussian binomial counting and +weighted linear-matroid greedy selection retain their credit. The new step +is the exact small-codimension reduction and its certificate implementation; +no literature-wide priority for enumerative optimization is claimed. + +The base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision eight. +[SOURCES.json](SOURCES.json) pins the original card and selected record as +historical provenance. [TASK.json](TASK.json) explicitly changes the formal +interface card to this algebraic side result. The binding-only selected +baseline passed; no selected scientific replay is inferred. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376723) +followed live open-PR, recent-account, main README, merged-PR and handoff +searches. Distinctive terms included partial-query acquisition, quotient +subspaces, superspaces, codimension, Gaussian binomial and target-aware +acquisition. Cached overlap has sparse local coverage; explicit Git searches +covered main READMEs for those terms. This does not cover arbitrary historical +diffs or unpublished work and is not a novelty certificate. No predecessor +package or credit line is changed. + +## Open next questions + +Can one actual native helper caller satisfy this additive acquisition contract +with an affordable reconstruction bill? Pin its query pool and target space, +then price the winning acquisition, reconstruction, delivery, storage and +restoration together. Missing source binding and physical tariffs block a +supplier or kappa claim. The structured question is in TASK.json. diff --git a/research/partial-query-optimum/SOURCES.json b/research/partial-query-optimum/SOURCES.json new file mode 100644 index 0000000000..05dbb26ab5 --- /dev/null +++ b/research/partial-query-optimum/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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": "docs/research/binary-query-basis.md", + "usage": "input", + "git_blob": "291bce46071c77b76b17ddfc3571df676b95c529", + "sha256": "cd60665849910830381a6a5b0c8f0d10b4bc9e54d50286eeacaf200fffd6f660" + } + ] +} diff --git a/research/partial-query-optimum/TASK.json b/research/partial-query-optimum/TASK.json new file mode 100644 index 0000000000..cb73e16aec --- /dev/null +++ b/research/partial-query-optimum/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Exact additive binary-query acquisition at target codimension at most four, with a quotient-superspace proof, complete optimality certificates and exhaustive subset corroboration.", + "scope_change_reason": "A bounded algebraic side result answering PR5791 partial-target acquisition; no proof-kernel formalization or selected assumption discharge is claimed.", + "bottleneck_link": "Target-aware acquisition can reduce a declared helper/query purchase bill; physical reconstruction and delivery still need pricing before supplier use.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact reduction and verified bounded optimizer; defer physical adapters and larger codimensions.", + "outcome": "completed", + "evidence": "PROOF.md; optimizer.py; normal and optimized verify.py; independent subset oracle; complete candidate certificates.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual native helper caller satisfy the additive acquisition contract after reconstruction is priced?", + "why_it_matters": "Only a complete physical invoice can transfer the algebraic saving to the supplier.", + "first_step": "Pin a caller, extract its binary query pool and target space, and price one winning acquisition with reconstruction, storage and restoration.", + "blocked_by": "No source-to-query adapter or physical reconstruction tariff is supplied." + } + ] +} diff --git a/research/partial-query-optimum/VERIFY.json b/research/partial-query-optimum/VERIFY.json new file mode 100644 index 0000000000..06c7f298f3 --- /dev/null +++ b/research/partial-query-optimum/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/binary-query-basis.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact partial acquisition against independent subset enumeration; quotient completeness; candidate-certificate corruption, boundary and CLI controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same complete scientific replay and rejecting controls with optimization enabled." + } + ] +} diff --git a/research/partial-query-optimum/optimizer.py b/research/partial-query-optimum/optimizer.py new file mode 100644 index 0000000000..12d6e16be3 --- /dev/null +++ b/research/partial-query-optimum/optimizer.py @@ -0,0 +1,277 @@ +"""Exact additive partial-query acquisition at binary codimension at most four.""" + +from __future__ import annotations + +import argparse +import json +from itertools import combinations +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def integer(value: object, lower: int, upper: int) -> int: + require(type(value) is int and lower <= value <= upper, "integer out of range") + return value + + +def reducer(vectors: list[int] | tuple[int, ...]) -> dict[int, tuple[int, int]]: + """Keep triangular rows and their expressions in the supplied vectors.""" + rows: dict[int, tuple[int, int]] = {} + for index, vector in enumerate(vectors): + residue, expression = reduce_vector(vector, rows) + if residue: + rows[residue.bit_length() - 1] = (residue, expression ^ (1 << index)) + return rows + + +def reduce_vector(vector: int, rows: dict[int, tuple[int, int]]) -> tuple[int, int]: + expression = 0 + for pivot in sorted(rows, reverse=True): + if vector & (1 << pivot): + row, coordinates = rows[pivot] + vector ^= row + expression ^= coordinates + return vector, expression + + +def canonical(vectors: list[int] | tuple[int, ...]) -> tuple[int, ...]: + rows = reducer(vectors) + pivots = sorted(rows) + values = {pivot: rows[pivot][0] for pivot in pivots} + for pivot in pivots: + for later in pivots: + if later > pivot and values[later] & (1 << pivot): + values[later] ^= values[pivot] + return tuple(values[pivot] for pivot in reversed(pivots)) + + +def duals_and_remainders(basis: list[int], width: int) -> tuple[list[int], list[int]]: + rows = reducer(basis) + require(len(rows) == len(basis), "dependent basis") + duals = [0] * len(basis) + remainders = [] + for bit in range(width): + residue, coordinates = reduce_vector(1 << bit, rows) + remainders.append(residue) + for index in range(len(basis)): + if coordinates & (1 << index): + duals[index] |= 1 << bit + return duals, remainders + + +def dot(left: int, right: int) -> int: + return (left & right).bit_count() & 1 + + +def image(vector: int, forms: list[int]) -> int: + return sum(dot(vector, form) << index for index, form in enumerate(forms)) + + +def reconstruct(mask: int, basis: list[int]) -> int: + result = 0 + for index, vector in enumerate(basis): + if mask & (1 << index): + result ^= vector + return result + + +def parse_problem(problem: object) -> tuple[int, list[int], list[int], list[int], int]: + require(type(problem) is dict, "problem must be an object") + require(set(problem) == {"width", "vectors", "costs", "targets"}, "problem keys") + width = integer(problem["width"], 1, 256) + vectors, costs, targets = (problem[key] for key in ("vectors", "costs", "targets")) + require(type(vectors) is list and len(vectors) <= 4096, "query count") + require(type(costs) is list and len(costs) == len(vectors), "cost count") + require(type(targets) is list and len(targets) <= 256, "target count") + for vector in vectors + targets: + integer(vector, 0, (1 << width) - 1) + for cost in costs: + integer(cost, 0, 10**12) + query_rows, target_rows = reducer(vectors), reducer(targets) + require(all(reduce_vector(target, query_rows)[0] == 0 for target in targets), + "target outside query span") + codimension = len(query_rows) - len(target_rows) + require(codimension <= 4, "codimension exceeds four") + return width, vectors, costs, targets, codimension + + +def subspaces_by_extension(dimension: int) -> list[int]: + """Enumerate spans by strict rank extension, at most 67 spaces.""" + layers: list[set[tuple[int, ...]]] = [{()}] + for rank in range(dimension): + following = set() + for basis in layers[rank]: + rows = reducer(basis) + for vector in range(1, 1 << dimension): + if reduce_vector(vector, rows)[0]: + following.add(canonical(list(basis) + [vector])) + layers.append(following) + spaces = [] + for layer in layers: + for basis in layer: + spaces.append(sum(1 << reconstruct(mask, list(basis)) + for mask in range(1 << len(basis)))) + return sorted(spaces) + + +def subspaces_by_rref(dimension: int) -> list[int]: + """Separate complete enumerator for the certificate checker.""" + spaces = [] + for rank in range(dimension + 1): + for pivots in combinations(range(dimension), rank): + cells = [(row, column) for row, pivot in enumerate(pivots) + for column in range(pivot + 1, dimension) if column not in pivots] + for assignment in range(1 << len(cells)): + basis = [1 << pivot for pivot in pivots] + for bit, (row, column) in enumerate(cells): + if assignment & (1 << bit): + basis[row] |= 1 << column + spaces.append(sum(1 << reconstruct(mask, basis) + for mask in range(1 << rank))) + require(len(spaces) == len(set(spaces)), "duplicate RREF spaces") + return sorted(spaces) + + +def quotient_forms(vectors: list[int], targets: list[int], width: int) -> list[int]: + basis = list(canonical(targets)) + target_rank = len(basis) + rows = reducer(basis) + for vector in vectors: + if reduce_vector(vector, rows)[0]: + basis.append(vector) + rows = reducer(basis) + duals, _ = duals_and_remainders(basis, width) + return duals[target_rank:] + + +def candidate(vectors: list[int], costs: list[int], targets: list[int], + eligible: list[int], width: int) -> dict: + selected = [] + rows: dict[int, tuple[int, int]] = {} + for index in sorted(eligible, key=lambda index: (costs[index], index)): + residue, _ = reduce_vector(vectors[index], rows) + if residue: + selected.append(index) + rows[residue.bit_length() - 1] = (residue, 0) + basis = [vectors[index] for index in selected] + duals, remainders = duals_and_remainders(basis, width) + result = {"selected": selected, "duals": duals, "missing_target": None, + "separator": None} + for index, target in enumerate(targets): + residue, _ = reduce_vector(target, reducer(basis)) + if residue: + bit = residue.bit_length() - 1 + result["missing_target"] = index + result["separator"] = sum(1 << position for position in range(width) + if remainders[position] & (1 << bit)) + break + return result + + +def solve(problem: dict) -> dict: + width, vectors, costs, targets, codimension = parse_problem(problem) + forms = quotient_forms(vectors, targets, width) + images = [image(vector, forms) for vector in vectors] + entries = [] + for space in subspaces_by_extension(codimension): + eligible = [index for index, value in enumerate(images) if space & (1 << value)] + entry = candidate(vectors, costs, targets, eligible, width) + entries.append({"space": space, **entry}) + winners = [(sum(costs[index] for index in entry["selected"]), entry["space"]) + for entry in entries if entry["missing_target"] is None] + require(bool(winners), "full quotient must be feasible") + cost, winner = min(winners) + return {"schema": "partial-query-optimum/v1", "quotient_forms": forms, + "entries": entries, "cost": cost, "winner": winner} + + +def check_entry(entry: object, space: int, vectors: list[int], costs: list[int], + targets: list[int], forms: list[int], width: int) -> int | None: + require(type(entry) is dict and set(entry) == + {"space", "selected", "duals", "missing_target", "separator"}, "entry keys") + require(integer(entry["space"], 1, (1 << (1 << len(forms))) - 1) == space, + "wrong or missing quotient space") + selected, duals = entry["selected"], entry["duals"] + require(type(selected) is list and len(selected) <= width, "selected count") + for index in selected: + integer(index, 0, len(vectors) - 1) + require(len(set(selected)) == len(selected), "duplicate selection") + require(type(duals) is list and len(duals) == len(selected), "dual count") + for form in duals: + integer(form, 0, (1 << width) - 1) + eligible = [index for index, vector in enumerate(vectors) + if space & (1 << image(vector, forms))] + eligible_set = set(eligible) + require(all(index in eligible_set for index in selected), "ineligible selection") + basis = [vectors[index] for index in selected] + for row, form in enumerate(duals): + require(all(dot(form, vector) == (row == column) + for column, vector in enumerate(basis)), "bad independence dual") + for index in eligible: + coordinates = image(vectors[index], duals) + require(reconstruct(coordinates, basis) == vectors[index], "basis misses eligible query") + require(all(not coordinates & (1 << position) or costs[index] >= costs[chosen] + for position, chosen in enumerate(selected)), "improving basis exchange") + if entry["missing_target"] is not None: + missing = integer(entry["missing_target"], 0, len(targets) - 1) + separator = integer(entry["separator"], 1, (1 << width) - 1) + require(dot(separator, targets[missing]) == 1 and + all(dot(separator, vectors[index]) == 0 for index in eligible), + "invalid infeasibility separator") + return None + require(entry["separator"] is None, "unexpected separator") + require(all(reconstruct(image(target, duals), basis) == target for target in targets), + "target not acquired") + return sum(costs[index] for index in selected) + + +def check(problem: dict, certificate: object) -> int: + width, vectors, costs, targets, codimension = parse_problem(problem) + require(type(certificate) is dict and set(certificate) == + {"schema", "quotient_forms", "entries", "cost", "winner"}, "certificate keys") + require(certificate["schema"] == "partial-query-optimum/v1", "certificate schema") + forms = certificate["quotient_forms"] + require(type(forms) is list and len(forms) == codimension, "quotient dimension") + for form in forms: + integer(form, 0, (1 << width) - 1) + require(all(image(target, forms) == 0 for target in targets), "quotient moves target") + require(len(reducer([image(vector, forms) for vector in vectors])) == codimension, + "quotient not surjective") + spaces = subspaces_by_rref(codimension) + entries = certificate["entries"] + require(type(entries) is list and len(entries) == len(spaces), "incomplete superspace list") + attainable = [] + for space, entry in zip(spaces, entries, strict=True): + cost = check_entry(entry, space, vectors, costs, targets, forms, width) + if cost is not None: + attainable.append((cost, space)) + require(bool(attainable), "no feasible candidate") + cost = integer(certificate["cost"], 0, width * 10**12) + winner = integer(certificate["winner"], 1, (1 << (1 << codimension)) - 1) + require((cost, winner) == min(attainable), "nonoptimal reported winner") + return cost + + +def read_json(path: Path) -> object: + require(path.stat().st_size <= 8_000_000, "JSON file exceeds eight MB") + return json.loads(path.read_text(encoding="utf-8")) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("problem", type=Path) + parser.add_argument("--check", type=Path) + arguments = parser.parse_args() + problem = read_json(arguments.problem) + certificate = read_json(arguments.check) if arguments.check else solve(problem) + cost = check(problem, certificate) + print(json.dumps({"status": "PASS_PARTIAL_QUERY_CERTIFICATE", "cost": cost} + if arguments.check else certificate, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/partial-query-optimum/verify.py b/research/partial-query-optimum/verify.py new file mode 100644 index 0000000000..29ac08fd89 --- /dev/null +++ b/research/partial-query-optimum/verify.py @@ -0,0 +1,209 @@ +"""Bounded exact corroboration; no predecessor implementation is executed.""" + +from __future__ import annotations + +import copy +import hashlib +import json +from pathlib import Path +import subprocess +import sys +import tempfile +from itertools import product + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +sys.path.insert(0, str(PACKAGE)) +from optimizer import check, solve, subspaces_by_extension, subspaces_by_rref + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def authenticate() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for source in sources["files"]: + if source["usage"] == "input": + digest = hashlib.sha256((ROOT / source["path"]).read_bytes()).hexdigest() + require(digest == source["sha256"], "source bytes changed") + + +def literal_span(vectors: list[int]) -> int: + """Truth-set doubling, independent of Gaussian elimination.""" + values = {0} + for vector in vectors: + values |= {value ^ vector for value in values} + return sum(1 << value for value in values) + + +def literal_spaces(width: int) -> list[int]: + """Scan every subset of the vector set and test XOR closure.""" + spaces = [] + for mask in range(1, 1 << (1 << width), 2): + values = [value for value in range(1 << width) if mask & (1 << value)] + if all(mask & (1 << (left ^ right)) for left in values for right in values): + spaces.append(mask) + return spaces + + +def subset_inventory(vectors: list[int]) -> list[tuple[int, int]]: + return [(mask, literal_span([vector for index, vector in enumerate(vectors) + if mask & (1 << index)])) + for mask in range(1 << len(vectors))] + + +def oracle(inventory: list[tuple[int, int]], costs: list[int], target_space: int) -> int: + return min(sum(cost for index, cost in enumerate(costs) if mask & (1 << index)) + for mask, space in inventory if space & target_space == target_space) + + +def exhaustive() -> dict[str, int]: + comparisons = 0 + entries = 0 + for vectors, width in [(list(range(1, 8)), 3), ([0, 1, 1, 2, 3], 2)]: + inventory = subset_inventory(vectors) + spaces = literal_spaces(width) + for costs in product(range(3), repeat=len(vectors)): + costs = list(costs) + for space in spaces: + targets = [value for value in range(1 << width) if space & (1 << value)] + problem = {"width": width, "vectors": vectors, + "costs": costs, "targets": targets} + certificate = solve(problem) + actual = check(problem, certificate) + require(actual == oracle(inventory, costs, space), "partial optimum mismatch") + comparisons += 1 + entries += len(certificate["entries"]) + return {"exhaustive_optima": comparisons, "checked_candidate_bases": entries} + + +def rejection(problem: dict, certificate: dict) -> None: + try: + check(problem, certificate) + except (ValueError, TypeError, KeyError): + return + raise ValueError("corrupted certificate accepted") + + +def certificate_controls() -> int: + problem = {"width": 3, "vectors": [1, 2, 3, 4, 7], + "costs": [8, 2, 2, 1, 2], "targets": [1]} + certificate = solve(problem) + require(check(problem, certificate) == 4, "intermediate-space optimum") + feasible = [(entry["space"], sum(problem["costs"][i] for i in entry["selected"])) + for entry in certificate["entries"] if entry["missing_target"] is None] + require(feasible[0][1] == 8 and feasible[-1][1] == 5, "endpoint prices") + mutants = [] + mutant = copy.deepcopy(certificate) + mutant["entries"].pop(1) + mutants.append(mutant) + mutant = copy.deepcopy(certificate) + mutant["quotient_forms"] = [0, 0] + mutants.append(mutant) + mutant = copy.deepcopy(certificate) + mutant["entries"][0]["duals"][0] = 0 + mutants.append(mutant) + mutant = copy.deepcopy(certificate) + mutant["cost"] += 1 + mutants.append(mutant) + mutant = copy.deepcopy(certificate) + mutant["cost"], mutant["winner"] = 5, feasible[-1][0] + mutants.append(mutant) + mutant = copy.deepcopy(certificate) + mutant["entries"][0]["selected"] = [1] + mutants.append(mutant) + mutant = copy.deepcopy(certificate) + mutant["cost"] = True + mutants.append(mutant) + for mutant in mutants: + rejection(problem, mutant) + absent = {"width": 3, "vectors": [3, 2, 4], "costs": [2, 2, 1], "targets": [1]} + missing_certificate = solve(absent) + require(missing_certificate["entries"][0]["missing_target"] == 0, "separator fixture") + mutant = copy.deepcopy(missing_certificate) + mutant["entries"][0]["separator"] = 4 + rejection(absent, mutant) + expensive = {"width": 2, "vectors": [1, 2, 3], "costs": [9, 1, 1], "targets": [1, 2]} + mutant = solve(expensive) + mutant["entries"][0]["selected"] = [0, 1] + mutant["entries"][0]["duals"] = [1, 2] + mutant["cost"] = 10 + rejection(expensive, mutant) + return len(mutants) + 2 + + +def boundary_and_invalid() -> dict: + counts = [] + for dimension in range(5): + direct = literal_spaces(dimension) + require(direct == subspaces_by_extension(dimension) == subspaces_by_rref(dimension), + "incomplete quotient enumeration") + counts.append(len(direct)) + require(counts == [1, 2, 5, 16, 67], "Gaussian subspace counts") + wide = {"width": 256, "vectors": [1 << i for i in range(256)] * 16, + "costs": list(range(256)) * 16, "targets": [1 << i for i in range(255)]} + require(check(wide, solve(wide)) == sum(range(255)), "wide boundary") + codimension_four = {"width": 6, "vectors": list(range(64)), + "costs": [value.bit_count() for value in range(64)], "targets": [1, 2]} + require(check(codimension_four, solve(codimension_four)) == 2, "codimension four boundary") + empty = {"width": 1, "vectors": [], "costs": [], "targets": []} + require(check(empty, solve(empty)) == 0, "empty problem") + invalid = [] + for field, value in [("width", True), ("width", 257), ("vectors", [2]), + ("costs", [True]), ("costs", [-1]), ("costs", []), + ("targets", [2])]: + problem = {"width": 1, "vectors": [1], "costs": [1], "targets": [1]} + problem[field] = value + invalid.append(problem) + invalid.append({"width": 2, "vectors": [1], "costs": [1], "targets": [2]}) + invalid.append({"width": 5, "vectors": [1, 2, 4, 8, 16], "costs": [1] * 5, + "targets": []}) + invalid.append({"width": 1, "vectors": [1] * 4097, "costs": [1] * 4097, + "targets": [1]}) + for problem in invalid: + try: + solve(problem) + except ValueError: + continue + raise ValueError("invalid problem accepted") + return {"quotient_space_counts": counts, "boundary_cases": 3, + "invalid_problem_rejections": len(invalid)} + + +def cli_control() -> int: + problem = {"width": 2, "vectors": [1, 2, 3], "costs": [3, 2, 2], "targets": [1]} + with tempfile.TemporaryDirectory(prefix="partial-query-") as directory: + problem_path, certificate_path = (Path(directory) / name for name in ("input.json", "cert.json")) + problem_path.write_text(json.dumps(problem), encoding="utf-8") + command = [sys.executable, "-I", "-W", "error", "-B", str(PACKAGE / "optimizer.py")] + result = subprocess.run(command + [str(problem_path)], check=True, capture_output=True, + text=True, timeout=30) + certificate_path.write_text(result.stdout, encoding="utf-8") + checked = subprocess.run(command + [str(problem_path), "--check", str(certificate_path)], + check=True, capture_output=True, text=True, timeout=30) + require(json.loads(checked.stdout)["cost"] == 3, "CLI optimum") + certificate_path.write_text('{"schema": "wrong"}', encoding="utf-8") + rejected = subprocess.run(command + [str(problem_path), "--check", str(certificate_path)], + capture_output=True, text=True, timeout=30) + require(rejected.returncode != 0, "CLI corrupted certificate accepted") + return 3 + + +def main() -> None: + authenticate() + counts = exhaustive() + counts.update(boundary_and_invalid()) + counts["certificate_rejections"] = certificate_controls() + counts["cli_runs"] = cli_control() + files = ["README.md", "PROOF.md", "ENGINEERING.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "optimizer.py", "verify.py"] + receipt = {"status": "PASS_PARTIAL_QUERY_OPTIMUM", "python": sys.version, + "counts": counts, "sha256": {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in files}} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()