diff --git a/research/causal-query-cache-stock/PROOF.md b/research/causal-query-cache-stock/PROOF.md new file mode 100644 index 0000000000..0352b97f7c --- /dev/null +++ b/research/causal-query-cache-stock/PROOF.md @@ -0,0 +1,178 @@ +# Minimum persistent cache at the minimum acquisition count + +This scoped proof and its compiler were produced by Nick Petalas. + +## Contract and statement + +Let K be any field. Fix a finite list of row vectors v_1,...,v_m in K^n. +There is an immutable bank x of n arbitrary independent payload fields. +At request i the value v_i x is available, and the requested answer is +Q(v_i x), for one common K-linear query Q and one common physical ABI. +The response is delivered before request i+1. Delivered responses cannot +be read again. Any copy retained by the responder counts as cache. + +Ordinary instructions take scalar K-linear combinations. An acquisition +applies Q to an ordinary combination of the original bank and returns one +payload field. Queries never take query-dependent data as their inputs. +For the lower bound, arbitrary prefetch of available ordinary combinations +is permitted. The upper construction only queries the current request. +The word and its coefficients are fixed independently of payload contents. +No external query-dependent advice or consumer feedback is available. + +We require formal query correctness: ordinary and queried coefficients +are distinguished. Equivalently analyze values as a x + b Qx with the two +coefficient rows independent. This is justified by a faithful formal +operator model, or by requiring the same scalar protocol to work for all +linear Q and all payloads. It is not justified for a fixed scalar Q. +No second nonordinary operator or non-scalar ordinary address algebra is +admitted here. + +Owned cache fields and one response/work field may be initialized and +erased, at positive cost. Original sources are unchanged. Dirty spectators +are untouched. This is the observational owned-erasure contract, not a +reversible dirty-workspace theorem. Ordinary arithmetic, moves, entry +scrubs, output delivery and all clears must be charged by an installation. + +Set, at the cut after response i has been delivered, + + V_i = span(v_1,...,v_i), + W_i = span(v_(i+1),...,v_m), + r = dim span(v_1,...,v_m), + d_i = dim(V_i intersect W_i) + = dim V_i + dim W_i - r. + +The empty spans at i=0,m are zero. Persistent cache counts all owned +query-dependent state across these cuts. A response/work field is empty +at every cut and is counted separately during a request. + +**Theorem.** The minimum number of acquisitions is r. Among protocols +using exactly r acquisitions, every cut needs at least d_i persistent +fields. One causal protocol attains all these lower bounds simultaneously. +Consequently the exact minimum persistent capacity is + + b = max_(0 <= i <= m) d_i. + +The same protocol can be implemented using b cache fields and one +response/work field, with scalar ADD, nonzero SCALE, SWAP and owned CLEAR. +It uses no additional payload field for a basis conversion. This b+1 +upper bound on total temporary fields is not claimed optimal. + +## The new lower bound + +Each acquired answer contributes one queried coefficient row. Ordinary +instructions can only combine those rows. All delivered answers together +have row span of dimension r, so at least r acquisitions are necessary. + +Consider an arbitrary correct protocol using exactly r acquisitions. +Let p_i be the number acquired by cut i. Past answers span V_i, so +p_i >= dim V_i, even if the protocol prefetched future rows or discarded +old answers. Let C_i be the span of queried coefficient rows in its +persistent state at that cut. If k_i fields persist, dim C_i <= k_i. +Ordinary parts in the same fields do not increase this queried dimension. + +Only the persistent state and r-p_i subsequent acquisitions can supply +queried coefficients to future answers. Past consumer outputs are +unavailable by contract. Therefore + + dim W_i <= dim C_i + (r-p_i), + +and hence + + k_i >= dim W_i-r+p_i + >= dim W_i-r+dim V_i + = d_i. + +This argument permits arbitrary linear cache encodings, discarded cache +values, prefetch, raw-source retention and scalar computation on raw +sources. None of them supplies an additional queried coefficient row. +It does not cover query feedback or free access to past consumer outputs. + +## A single schedule attains every cut bound + +Retain answers for a basis of U_i=V_i intersect W_i after cut i. +Initially U_0=0. At request i, write v=v_i. + +If v belongs to V_(i-1), it also belongs to W_(i-1), since it is a current +or future request at the preceding cut. Thus v belongs to U_(i-1), and +its answer is reconstructed from the cache with no query. Otherwise query +the actually available v x once. The number of such rank increases is r. + +For the transition to U_i, observe + + U_i is a subspace of U_(i-1) + span(v). + +Indeed write u=a+c v with u in U_i and a in V_(i-1). Both u and v belong +to W_(i-1), so a belongs to V_(i-1) intersect W_(i-1). Every new basis +answer can therefore be formed from the old cache and the response. +After conversion, deliver the response and clear the response/work field. +Only dim U_i=d_i independent cache answers remain. At the final cut U_m=0, +so the cache is empty. This proves simultaneous attainment and the theorem. + +The basis choice and causal reconstruction build on Dugongue's #5803, +volume-scheduling S12-S13. The contribution here is the matching per-cut +lower bound, its global minimum-capacity consequence, and the bounded +instruction-emitting compiler. The dimension identity is classical linear +algebra and is the usual connectivity function of the represented matroid; +no worldwide priority claim for that function is made. Request order is +fixed. Optimizing order is a different problem. + +## Why basis conversion needs no second payload bank + +Pad the old cache by zero fields to b entries and append the current +response. Express each new cache basis row in the old basis plus v. +These coefficients and a last row preserving the response give a square +(b+1)-by-(b+1) scalar matrix T. The unwanted cache rows are zero. + +Two-sided Gaussian elimination constructs invertible L,R with + + L T R = diag(I_s,0). + +Execute R^-1 on the existing bank, clear the last b+1-s transformed +coordinates, and execute L^-1. These operations realize T on every bank +input. Each elementary matrix is a scalar ADD, nonzero SCALE or SWAP. +No temporary payload field is used. The response may move during this +conversion but is restored before delivery. The compiler emits those +individual instructions, not a simultaneous-assignment oracle. + +For a bank of h=b+1 fields, the reduction uses at most h pivot steps, +h row swaps, h column swaps, h scales, h(h-1) row ADDs and h(h-1) column +ADDs. Its emitted inverse factors and clears have at most 2h^2+2h +instructions. Preparing a dependent response uses at most b ADDs, and +its post-delivery clear uses one. Entry scrubbing uses h clears. +Thus an installation may charge at most + + h + m (2h^2+2h+b+1) + +such ordinary instructions, in addition to r acquisitions, current-source +assembly, descriptor construction and access, coefficient arithmetic, +output transport, and their physical routing/precision costs. Scalars +must actually be admitted at the common chart. Elimination over a field +does not prove a dyadic-only implementation or a uniform physical tariff. + +## An unbounded strict stock improvement over retaining named answers + +For n>=1 request e_1,...,e_n, followed by e_1+...+e_n. The total rank is n. +For each cut 1<=i<=n, U_i is the line spanned by e_1+...+e_i. Hence b=1. +The responder accumulates the queried running sum and uses exactly n +queries. Keeping every individually acquired answer until its final use +would instead retain n fields at the cut before the last response. +That fixed-value policy is a comparator, not a lower bound for general +cache encodings. The new theorem supplies the latter lower bound of one. + +## Boundaries that matter + +- If previous responses remain readable, the width formula can overcharge + the responder's private cache. Those responses are additional state. +- If reacquisitions are allowed, b need not be necessary. Requesting one + nonzero row twice uses one query and one persistent field at the optimum; + two queries use zero persistent fields. +- If Q is an ordinary scalar, queried and ordinary rows are not independent, + and the acquisition lower bound can fail entirely. +- Query feedback, noncommuting ordinary operators, differing frames, + source mutations, input-dependent control and dirty-return-only work + fields have different contracts. + +The proof is all-size within this contract. The executable compiler and +finite checks have the separate bounded domains stated in README.md. +No selected supplier installation, new kappa, full multiplication theorem, +independent human review or formal proof-kernel acceptance is claimed. diff --git a/research/causal-query-cache-stock/README.md b/research/causal-query-cache-stock/README.md new file mode 100644 index 0000000000..9dddd3339c --- /dev/null +++ b/research/causal-query-cache-stock/README.md @@ -0,0 +1,186 @@ +# Exact persistent stock for minimum-query streams + +This contribution was produced by Nick Petalas. Apache-2.0. + +For a fixed chronological list of common-query requests, let V_i and W_i +be the scalar row spans of past and future requests at cut i. Put +r=rank(all requests). The exact minimum persistent cache, among protocols +using the minimum r acquisitions, is + +```text +b = max_i dim(V_i intersect W_i) + = max_i (rank(V_i) + rank(W_i) - r). +``` + +One causal program attains every cut lower bound simultaneously. The +[proof](PROOF.md) allows arbitrary linear cache encodings and legal prefetch +in the lower bound. The upper construction only queries the current +request. [compile.py](compile.py) emits individual scalar ADD, nonzero +SCALE, SWAP and owned CLEAR instructions using b cache fields plus one +response/work field. No second conversion bank is hidden. + +Claim type: scoped written proof with exact finite corroboration and a +bounded constructive compiler. This is a new matching stock lower bound +and compiler for the common-query observational interface. Dugongue's +[#5803](https://github.com/CrocSwap/integer-mult-bounds/pull/5803), scheduling +S12-S13, supplies the causal query-basis and one-cut intersection +compression constructions. Those are cited predecessors, not audit targets. +The rank identity and represented-matroid connectivity function are +classical. No claim of worldwide novelty for those ingredients is made. + +For example, request e_1,...,e_n and then their sum. Exactly n acquisitions +and one persistent field suffice for every n>=1. Retaining the individually +acquired answers until their last use would use n persistent fields. +This construction changes the retained values. It does not merely reassign +fixed lifetimes to fewer slots. + +## Exact boundary + +Sources are immutable and arbitrary. Every request is an ordinary scalar +row on that source bank, available at its request time. Answers are +observational outputs, delivered in order and inaccessible after delivery. +All query-dependent state crossing a cut counts toward the cache. A copy +kept by the responder counts too. Ordinary and queried coefficients must +be formally distinguishable. A scalar Q is outside the lower bound. + +Queries take only ordinary source combinations. Query feedback, +non-scalar ordinary operator algebras, source mutations, consumer feedback, +different charts and read-access to past outputs have different contracts. +Owned erasure is permitted and charged. Original sources and arbitrary +dirty spectators are preserved. This is not a dirty-return-only workspace +construction. The exact result concerns persistent stock at delivery cuts; +b+1 is an upper bound on total temporary payload fields, not a claimed +minimum for every microstep. + +An installation must pay all ordinary instructions, current-source +assembly, initial scrubs, delivery, routing, coefficients, descriptors, +clears and physical access. With h=b+1, the proof gives an ordinary scalar +instruction bound h+m(2h^2+2h+b+1), separately from the r acquisitions. +General field elimination does not automatically give dyadic scalar +recipes. No selected supplier region is installed or repriced here. +No new kappa, selected-frontier change or full multiplication theorem is +claimed. The five selected framework assumptions remain. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/causal-query-cache-stock/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/causal-query-cache-stock/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/causal-query-cache-stock +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/causal-query-cache-stock --check-source-history +``` + +Another CPython 3.12 may replace the absolute interpreter path. The direct +verifier emits `PASS_CAUSAL_QUERY_CACHE_STOCK` in a generated JSON receipt +bound to SHA256 hashes of all package files. It writes nothing. Registered +replay also prints `PASS_REGISTERED_RESEARCH_PACKAGE`; publication checking +prints `PASS_RESEARCH_COMMIT_BYTES`. No receipt is hand-authored or trusted +as an input. Redirect output into a scratch directory if a saved receipt +is wanted. + +The compiler accepts a JSON object with exactly `prime`, `dimension` and +`rows`. Its executable domain is at most 24 requests on 1..8 sources over +F_2, F_3, F_5, F_7 or F_11, with canonical integer residue entries. Empty +streams and zero rows are accepted. For example: + +```json +{"prime": 3, "dimension": 2, "rows": [[1,0], [0,1], [1,1]]} +``` + +Save that object outside the checkout and run: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/causal-query-cache-stock/compile.py /absolute/path/problem.json +``` + +The result has two acquisitions, persistent width one and a two-field bank. +Its cuts, acquisition decisions and literal ordinary instructions are +included. Compilation chooses a basis from the supplied coefficient rows; +it is offline metadata work, not a free physical source observer. + +## Evidence + +The independent finite-state oracle enumerates every subspace as a subset +of its finite vector space and tests additive closure. For each capacity, +it tries every available retained subspace and minimizes acquisition count. +It uses no elimination or intersection routine from the compiler. +The complete domains, including zero rows and empty streams, are: + +| Field and source dimension | Maximum request length | Streams | Subspaces | +| --- | ---: | ---: | ---: | +| F_2, dimension 2 | 6 | 5,461 | 5 | +| F_2, dimension 3 | 4 | 4,681 | 16 | +| F_3, dimension 2 | 4 | 7,381 | 6 | + +All 17,523 oracle optima match the emitted persistent width and minimum +query count. Literal instruction replay checks every delivered formal +answer, each retained basis, entry scrubbing, exit zero and two independent +dirty spectators. Separate complete matrix tests check all 2-by-2 matrices +over F_2,F_3,F_5 and all 3-by-3 matrices over F_2, totaling 1,234 matrices. +Forty running-sum family cases cover all five supported fields and source +dimensions 1..8. Six boundary cases exercise the full 24-request and +nine-field-bank limits, including rank zero. + +Twenty-one rejection controls cover invalid domains, deleted acquisition, +missing entry scrub, false query count, destroyed output, a spectator +address, changed cache basis, aliased ADD, zero SCALE, Boolean address and +unknown instruction. The finite oracle restricts acquisitions to the +current request; the written lower proof additionally permits legal +prefetch. Neither finite enumeration nor Python execution proves all-size +physical implementation or formal-kernel acceptance. + +## Verification scope and code constraints + +Scientific base is canonical main +e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8, with selected +conditional kappa 0.00363005817 from #7000. The first baseline example passed +as source-binding orientation only. [SOURCES.json](SOURCES.json) pins the +selected record, catalogue, priorities and the two predecessor prose files +as historical provenance. No predecessor mathematical suite is imported or +replayed. [TASK.json](TASK.json) records the changed card scope and +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539387). + +The original caller/native acceptance gate remains unmet. Native operators, +matched physical ABIs, supported scalar recipes, owned erasure, compiler, +precision/tape, stock and analytic recovery require a separate installation. +Selected cold replay, Lean, Docker, supplier admission, independent human +review and proof-kernel review are unrun and unclaimed. + +New code is nonrecursive and functions are shorter than 60 lines. Compiler +inputs bound requests by 24 and source dimension by eight; derived matrices +have at most sixteen unknowns or nine bank rows. Finite oracle spaces have +at most nine elements, so it enumerates at most 512 subsets. All failures +use explicit exceptions that remain active under optimization. + +Power of Ten rule 3 has a managed-runtime deviation: Python allocates +lists, dictionaries and integers during these bounded computations. +Streams are checked one at a time and only a digest and counts persist. +Rule 8/9 has a fixed-source loading deviation: the verifier executes only +the package-local compile.py through runpy, with a fixed finite callable +set. No external source or input-provided code is loaded. Warning-strict +normal/optimized replay, in-memory syntax parsing and whitespace checks +supply the available diagnostics. No new external dependency or shared +configuration is introduced. + +## Open next questions + +1. Does an actual common-ABI source request stream have a smaller b than + its retained-answer bank? Export its literal immutable source rows and + delivery cuts first, then price every coefficient conversion, route and + clear. The missing blocker is an installed physical request stream. +2. What is the exact stock versus reacquisition tradeoff when more than r + queries are allowed? Start with an independently enumerated small stream + where capacity b-1 needs additional queries. The theorem fixes the + minimum query count and supplies no global tradeoff formula. + +## Credit + +Credit David Ganz / Dugongue and #5803 S12-S13 for causal basis acquisition +and sufficient future-demand intersection compression. Retain that +package's credit to Ali Romman, ToikY, zxv, Cinna Davis, Cao Yifan, +Ryanson Jonathan, Jacob Alan Sussman and the native/ownership/compiler +lineage. Classical span, dimension and Gaussian-elimination methods are +not claimed as new. The matching lower bound, scoped synthesis and finite +checks were produced by Nick Petalas. Predecessor files are unchanged. diff --git a/research/causal-query-cache-stock/SOURCES.json b/research/causal-query-cache-stock/SOURCES.json new file mode 100644 index 0000000000..35ff580002 --- /dev/null +++ b/research/causal-query-cache-stock/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/current-priorities.md", + "usage": "provenance", + "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91", + "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc" + }, + { + "path": "research/frontier-mathematical-atlas/README.md", + "usage": "provenance", + "git_blob": "bd99e5776cbe3a04e02a5ba483451599a7421944", + "sha256": "afef8b805f0f04dee48f4eab6e5f02ec6a209eba060da856a08453c23e319ba1" + }, + { + "path": "research/frontier-mathematical-atlas/volume-scheduling.md", + "usage": "provenance", + "git_blob": "1bffed6b1e1ed7afa8f5736f45d1a9c774d9fe63", + "sha256": "9aa9666e9fd1f18ee8b6be542b944fe9eceae0acc364dba9719fd9dd94022eb0" + } + ] +} diff --git a/research/causal-query-cache-stock/TASK.json b/research/causal-query-cache-stock/TASK.json new file mode 100644 index 0000000000..91b9a101ac --- /dev/null +++ b/research/causal-query-cache-stock/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "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 minimum persistent cache at minimum acquisition count for a fixed chronological scalar common-query observational stream, with an instruction-emitting bounded compiler.", + "scope_change_reason": "The caller card is changed to the stock-optimality question left by PR5803 S12-S13 and SQ05. This is an interface side result, with no installed selected-source region or native tariff reduction.", + "bottleneck_link": "A rank-minimal query cache can use fewer retained fields than its acquired basis, which could reduce owned stock after a separately priced physical installation. The complete source/caller acceptance gate remains unmet.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved exact cache-stock formula and verified compiler; do not extend to query feedback, order optimization, additional query budgets or supplier installation.", + "outcome": "completed", + "evidence": "PROOF.md proves the per-cut lower bound d_i and simultaneous attainment; verify.py compares all 17523 streams with an independent all-subspace oracle, replays literal bank instructions, checks 1234 complete matrix cases, 40 sum-family cases, 6 domain boundaries and 21 rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual common-ABI source request stream realize a lower persistent bank using this compiler?", + "why_it_matters": "It could reduce owned stock without increasing query count.", + "first_step": "Export the immutable source rows and delivery cuts, then price every basis operation, route and clear.", + "blocked_by": "No actual selected-source physical request stream is installed by this package." + }, + { + "question": "What is the sharp persistent stock versus additional acquisition tradeoff?", + "why_it_matters": "A smaller physical reserve may justify paid reacquisition.", + "first_step": "Choose a small independently enumerated stream whose capacity b-1 requires more than r queries.", + "blocked_by": "The theorem fixes the globally minimum query count; a general tradeoff formula is not supplied." + } + ], + "claim_type": "scoped-proof", + "coordination": { + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539387", + "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/5803", + "source_author": "Dugongue" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + } +} diff --git a/research/causal-query-cache-stock/VERIFY.json b/research/causal-query-cache-stock/VERIFY.json new file mode 100644 index 0000000000..d67fa4185a --- /dev/null +++ b/research/causal-query-cache-stock/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 finite all-subspace stock oracle, emitted arbitrary-input endpoints, complete matrix compiler cases, domain boundaries and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact finite all-subspace stock oracle, emitted arbitrary-input endpoints, complete matrix compiler cases, domain boundaries and rejection controls with assertions disabled." + } + ] +} diff --git a/research/causal-query-cache-stock/compile.py b/research/causal-query-cache-stock/compile.py new file mode 100644 index 0000000000..a1273b4937 --- /dev/null +++ b/research/causal-query-cache-stock/compile.py @@ -0,0 +1,203 @@ +"""Emit a rank-minimal common-query stream with minimum persistent cache. + +The executable domain is at most 24 requests on 1..8 sources over one of +the listed prime fields. The accompanying proof has no such finite bounds. +""" + +import argparse +import json +from pathlib import Path + +PRIMES = (2, 3, 5, 7, 11) +MAX_DIMENSION = 8 +MAX_REQUESTS = 24 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def validate(problem): + need(type(problem) is dict, "problem must be an object") + need(set(problem) == {"prime", "dimension", "rows"}, "unexpected keys") + prime, dimension, rows = (problem[k] for k in ("prime", "dimension", "rows")) + need(type(prime) is int and prime in PRIMES, "unsupported prime") + need(type(dimension) is int and 1 <= dimension <= MAX_DIMENSION, "dimension") + need(type(rows) is list and len(rows) <= MAX_REQUESTS, "request count") + for row in rows: + need(type(row) is list and len(row) == dimension, "row shape") + need(all(type(x) is int and 0 <= x < prime for x in row), "coefficient") + return prime, dimension, rows + + +def rref(rows, columns, prime): + matrix = [list(row) for row in rows] + pivots = [] + for column in range(columns): + candidates = [i for i in range(len(pivots), len(matrix)) if matrix[i][column]] + if not candidates: + continue + pivot = len(pivots) + index = candidates[0] + matrix[pivot], matrix[index] = matrix[index], matrix[pivot] + scale = pow(matrix[pivot][column], -1, prime) + matrix[pivot] = [x * scale % prime for x in matrix[pivot]] + for index in range(len(matrix)): + if index != pivot: + factor = matrix[index][column] + matrix[index] = [(a - factor * b) % prime + for a, b in zip(matrix[index], matrix[pivot])] + pivots.append(column) + return matrix, pivots + + +def basis(rows, dimension, prime): + matrix, pivots = rref(rows, dimension, prime) + return matrix[:len(pivots)] + + +def kernel(rows, columns, prime): + matrix, pivots = rref(rows, columns, prime) + result = [] + for free in range(columns): + if free not in pivots: + vector = [0] * columns + vector[free] = 1 + for index, pivot in enumerate(pivots): + vector[pivot] = -matrix[index][free] % prime + result.append(vector) + return result + + +def combination(coefficients, rows, dimension, prime): + return [sum(c * row[j] for c, row in zip(coefficients, rows)) % prime + for j in range(dimension)] + + +def intersection(left, right, dimension, prime): + equations = [[row[j] for row in left] + [-row[j] % prime for row in right] + for j in range(dimension)] + relations = kernel(equations, len(left) + len(right), prime) + rows = [combination(v[:len(left)], left, dimension, prime) for v in relations] + return basis(rows, dimension, prime) + + +def coordinates(row, spanning, dimension, prime): + columns = len(spanning) + equations = [[v[j] for v in spanning] + [row[j]] for j in range(dimension)] + reduced, pivots = rref(equations, columns, prime) + need(all(any(line[:columns]) or line[-1] == 0 for line in reduced), + "row is outside the supplied span") + result = [0] * columns + for index, pivot in enumerate(pivots): + result[pivot] = reduced[index][-1] + need(combination(result, spanning, dimension, prime) == row, "coordinate residual") + return result + + +def inverse_row_operation(operation, prime): + kind, *args = operation + if kind == "scale": + return [kind, args[0], pow(args[1], -1, prime)] + if kind == "add": + return [kind, args[0], args[1], -args[2] % prime] + need(kind == "swap", "noninvertible reduction operation") + return operation[:] + + +def matrix_program(target, prime): + """Factor T=L^-1 diag(I_r,0) R^-1 into in-place row instructions.""" + size = len(target) + matrix = [row[:] for row in target] + left, right = [], [] + rank = 0 + for pivot in range(size): + candidates = [(i, j) for i in range(pivot, size) + for j in range(pivot, size) if matrix[i][j]] + if not candidates: + break + i, j = candidates[0] + matrix[pivot], matrix[i] = matrix[i], matrix[pivot] + left.append(["swap", pivot, i]) + for row in matrix: + row[pivot], row[j] = row[j], row[pivot] + right.append(["swap", pivot, j]) + factor = pow(matrix[pivot][pivot], -1, prime) + matrix[pivot] = [x * factor % prime for x in matrix[pivot]] + left.append(["scale", pivot, factor]) + for i in range(size): + if i != pivot and matrix[i][pivot]: + factor = -matrix[i][pivot] % prime + matrix[i] = [(a + factor * b) % prime + for a, b in zip(matrix[i], matrix[pivot])] + left.append(["add", i, pivot, factor]) + for j in range(size): + if j != pivot and matrix[pivot][j]: + factor = -matrix[pivot][j] % prime + for i in range(size): + matrix[i][j] = (matrix[i][j] + factor * matrix[i][pivot]) % prime + right.append(["add", pivot, j, -factor % prime]) + rank += 1 + diagonal = [[int(i == j and i < rank) for j in range(size)] for i in range(size)] + need(matrix == diagonal, "two-sided reduction residual") + return right + [["clear", i] for i in range(rank, size)] + [ + inverse_row_operation(op, prime) for op in reversed(left)] + + +def cut_spaces(rows, dimension, prime): + cuts = [] + for index in range(len(rows) + 1): + past = basis(rows[:index], dimension, prime) + future = basis(rows[index:], dimension, prime) + shared = intersection(past, future, dimension, prime) + cuts.append({"past_rank": len(past), "future_rank": len(future), + "basis": shared}) + return cuts + + +def transition(old, new, request, cache_width, dimension, prime): + size = cache_width + 1 + matrix = [[0] * size for _ in range(size)] + for i, row in enumerate(new): + coeff = coordinates(row, old + [request], dimension, prime) + matrix[i][:len(old)] = coeff[:-1] + matrix[i][-1] = coeff[-1] + matrix[-1][-1] = 1 + return matrix_program(matrix, prime) + + +def compile_stream(problem): + prime, dimension, rows = validate(problem) + cuts = cut_spaces(rows, dimension, prime) + rank = cuts[-1]["past_rank"] + width = max(len(cut["basis"]) for cut in cuts) + stages = [] + for index, request in enumerate(rows): + old, new = cuts[index]["basis"], cuts[index + 1]["basis"] + acquire = cuts[index + 1]["past_rank"] > cuts[index]["past_rank"] + prepare = [] + if not acquire: + coeff = coordinates(request, old, dimension, prime) + prepare = [["add", width, j, value] for j, value in enumerate(coeff) if value] + stages.append({"acquire": acquire, "prepare": prepare, + "transition": transition(old, new, request, width, dimension, prime)}) + need(sum(stage["acquire"] for stage in stages) == rank, "acquisition count") + need(all(len(cut["basis"]) == cut["past_rank"] + cut["future_rank"] - rank + for cut in cuts), "cut dimension identity") + return {"schema": "causal-query-cache-stock/1", "problem": problem, + "queries": rank, "cache_width": width, "bank_fields": width + 1, + "initial_clear": list(range(width + 1)), "cuts": cuts, "stages": stages} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("problem", type=Path) + args = parser.parse_args() + need(args.problem.stat().st_size <= 65536, "problem exceeds 64 KiB") + problem = json.loads(args.problem.read_text()) + print(json.dumps(compile_stream(problem), sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/causal-query-cache-stock/verify.py b/research/causal-query-cache-stock/verify.py new file mode 100644 index 0000000000..3a33ade30b --- /dev/null +++ b/research/causal-query-cache-stock/verify.py @@ -0,0 +1,257 @@ +"""Finite corroboration and literal instruction replay for the cache theorem.""" + +from copy import deepcopy +import hashlib +from itertools import product +import json +from pathlib import Path +import runpy + +PACKAGE = Path(__file__).resolve().parent +ENGINE = runpy.run_path(str(PACKAGE / "compile.py")) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def row_add(left, right, factor, prime): + return [(a + factor * b) % prime for a, b in zip(left, right)] + + +def operate(bank, operation, prime, capacity): + need(type(operation) is list and operation, "instruction shape") + kind, *args = operation + sizes = {"clear": 1, "scale": 2, "swap": 2, "add": 3} + need(kind in sizes and len(args) == sizes[kind], "instruction arity") + indices = args[:2] if kind in ("swap", "add") else args[:1] + need(all(type(i) is int and 0 <= i < capacity for i in indices), "slot index") + target = args[0] + if kind == "clear": + bank[target] = [0] * len(bank[target]) + elif kind == "swap": + bank[target], bank[args[1]] = bank[args[1]], bank[target] + elif kind == "scale": + need(type(args[1]) is int and 0 < args[1] < prime, "scale unit") + bank[target] = [x * args[1] % prime for x in bank[target]] + else: + need(target != args[1], "ADD alias") + need(type(args[2]) is int and 0 <= args[2] < prime, "ADD coefficient") + bank[target] = row_add(bank[target], bank[args[1]], args[2], prime) + + +def replay(plan): + prime, dimension, rows = ENGINE["validate"](plan["problem"]) + width = plan["cache_width"] + need(type(width) is int and 0 <= width <= dimension, "cache width") + capacity, columns = width + 1, dimension + width + 3 + bank = [[int(j == dimension + i) for j in range(columns)] + for i in range(capacity + 2)] + spectators = deepcopy(bank[capacity:]) + need(plan["bank_fields"] == capacity, "bank capacity") + need(plan["initial_clear"] == list(range(capacity)), "entry scrub") + for slot in plan["initial_clear"]: + operate(bank, ["clear", slot], prime, capacity) + need(len(plan["stages"]) == len(rows), "stage count") + need(len(plan["cuts"]) == len(rows) + 1, "cut count") + acquisitions, instructions = 0, capacity + for index, (row, stage) in enumerate(zip(rows, plan["stages"])): + need(type(stage["acquire"]) is bool, "acquisition flag") + if stage["acquire"]: + need(not any(bank[width]), "query port was not cleared") + bank[width] = row[:] + [0] * (columns - dimension) + acquisitions += 1 + for instruction in stage["prepare"] + stage["transition"]: + operate(bank, instruction, prime, capacity) + instructions += 1 + need(bank[width] == row + [0] * (columns - dimension), "wrong delivered answer") + expected = plan["cuts"][index + 1]["basis"] + need(len(expected) <= width, "cut overflows cache") + desired = [v + [0] * (columns - dimension) for v in expected] + desired += [[0] * columns for _ in range(width - len(expected))] + need(bank[:width] == desired, "wrong retained cache") + operate(bank, ["clear", width], prime, capacity) + instructions += 1 + need(acquisitions == plan["queries"], "wrong acquisition total") + need(all(not any(v) for v in bank[:capacity]), "exit cache not zero") + need(bank[capacity:] == spectators, "dirty spectator changed") + return instructions + + +def digits(code, prime, dimension): + return [(code // prime ** j) % prime for j in range(dimension)] + + +def finite_spaces(prime, dimension): + """Independent oracle: enumerate every subset and test additive closure.""" + order = prime ** dimension + vectors = [digits(i, prime, dimension) for i in range(order)] + addition = [[sum(((a[k] + b[k]) % prime) * prime ** k + for k in range(dimension)) for b in vectors] for a in vectors] + spaces = [] + for mask in range(1, 1 << order, 2): + elements = [i for i in range(order) if mask >> i & 1] + if all(mask >> addition[a][b] & 1 for a in elements for b in elements): + dimension_here = next(d for d in range(dimension + 1) + if prime ** d == len(elements)) + spaces.append((mask, dimension_here)) + spans, options = {}, {} + for mask, _ in spaces: + for code in range(order): + multiple, span = 0, 0 + for _ in range(prime): + for a in range(order): + if mask >> a & 1: + span |= 1 << addition[a][multiple] + multiple = addition[multiple][code] + spans[mask, code] = span + for limit in range(dimension + 1): + options[mask, limit] = [sub for sub, d in spaces + if d <= limit and sub & mask == sub] + return spaces, spans, options + + +def oracle_width(codes, rank, dimension, spans, options): + """Enumerate every linear cache state; minimize queries for each capacity.""" + for limit in range(dimension + 1): + states = {1: 0} + for code in codes: + following = {} + for mask, queries in states.items(): + cost = queries + int(not (mask >> code & 1)) + available = spans[mask, code] + for subspace in options[available, limit]: + following[subspace] = min(following.get(subspace, len(codes) + 1), cost) + states = following + if min(states.values()) == rank: + return limit + raise ValueError("finite state oracle found no rank-minimal schedule") + + +def exhaustive_streams(prime, dimension, maximum, digest): + spaces, spans, options = finite_spaces(prime, dimension) + cases, instructions = 0, 0 + for length in range(maximum + 1): + for codes in product(range(prime ** dimension), repeat=length): + full = 1 + for code in codes: + full = spans[full, code] + rank = next(d for mask, d in spaces if mask == full) + rows = [digits(code, prime, dimension) for code in codes] + problem = {"prime": prime, "dimension": dimension, "rows": rows} + plan = ENGINE["compile_stream"](problem) + need(plan["queries"] == rank, "independent span rank disagrees") + optimum = oracle_width(codes, rank, dimension, spans, options) + need(plan["cache_width"] == optimum, "independent stock optimum disagrees") + instructions += replay(plan) + digest.update(json.dumps([prime, dimension, codes, rank, optimum], + separators=(",", ":")).encode()) + cases += 1 + return {"prime": prime, "dimension": dimension, "maximum_length": maximum, + "all_subspaces": len(spaces), "streams": cases, "instructions": instructions} + + +def matrix_checks(): + cases, instructions = 0, 0 + for prime, size in ((2, 2), (3, 2), (5, 2), (2, 3)): + for flat in product(range(prime), repeat=size * size): + target = [list(flat[i * size:(i + 1) * size]) for i in range(size)] + bank = [[int(i == j) for j in range(size)] for i in range(size)] + program = ENGINE["matrix_program"](target, prime) + for operation in program: + operate(bank, operation, prime, size) + need(bank == target, "matrix instruction endpoint disagrees") + cases += 1 + instructions += len(program) + return {"matrices": cases, "instructions": instructions} + + +def family_checks(): + cases, instructions = 0, 0 + for prime in ENGINE["PRIMES"]: + for dimension in range(1, 9): + unit = [[int(i == j) for j in range(dimension)] for i in range(dimension)] + rows = unit + [[1] * dimension] + problem = {"prime": prime, "dimension": dimension, "rows": rows} + saved = deepcopy(problem) + plan = ENGINE["compile_stream"](problem) + need(plan["queries"] == dimension and plan["cache_width"] == 1, + "running-sum family does not attain one cache field") + need(problem == saved, "compiler changed input") + instructions += replay(plan) + cases += 1 + boundary_cases = 0 + for prime in ENGINE["PRIMES"]: + unit = [[int(i == j) for j in range(8)] for i in range(8)] + plan = ENGINE["compile_stream"]({"prime": prime, "dimension": 8, "rows": unit * 3}) + need(plan["queries"] == 8 and plan["cache_width"] == 8, "maximum bank boundary") + instructions += replay(plan) + boundary_cases += 1 + plan = ENGINE["compile_stream"]({"prime": 11, "dimension": 8, "rows": [[0] * 8] * 24}) + need(plan["queries"] == plan["cache_width"] == 0, "zero-request rank boundary") + instructions += replay(plan) + return {"sum_family_cases": cases, "boundary_cases": boundary_cases + 1, + "instructions": instructions} + + +def reject(call, message): + try: + call() + except (ValueError, KeyError, IndexError, TypeError): + return 1 + raise ValueError("accepted control: " + message) + + +def controls(): + compile_stream = ENGINE["compile_stream"] + valid = {"prime": 3, "dimension": 2, "rows": [[1, 0], [0, 1], [1, 1]]} + bad_inputs = [None, {}, dict(valid, prime=True), dict(valid, prime=4), + dict(valid, dimension=0), dict(valid, dimension=9), + dict(valid, rows=[[1]]), dict(valid, rows=[[True, 0]]), + dict(valid, rows=[[3, 0]]), dict(valid, rows=[[1, 0]] * 25), + dict(valid, extra=0)] + count = sum(reject(lambda item=item: compile_stream(item), "input boundary") + for item in bad_inputs) + plan = compile_stream(valid) + replay(plan) + mutants = [] + changed = deepcopy(plan) + changed["stages"][0]["acquire"] = False + mutants.append(changed) + changed = deepcopy(plan) + changed["initial_clear"] = [] + mutants.append(changed) + changed = deepcopy(plan) + changed["queries"] -= 1 + mutants.append(changed) + changed = deepcopy(plan) + changed["stages"][0]["transition"].append(["clear", changed["cache_width"]]) + mutants.append(changed) + changed = deepcopy(plan) + changed["stages"][0]["transition"].append(["clear", changed["bank_fields"]]) + mutants.append(changed) + changed = deepcopy(plan) + changed["cuts"][1]["basis"][0][0] = 0 + mutants.append(changed) + count += sum(reject(lambda item=item: replay(item), "changed schedule") for item in mutants) + bank = [[1, 0], [0, 1]] + for instruction in (["add", 0, 0, 1], ["scale", 0, 0], ["clear", True], ["jump", 0]): + count += reject(lambda op=instruction: operate(bank, op, 3, 2), "instruction boundary") + return count + + +def main(): + digest = hashlib.sha256() + domains = [exhaustive_streams(p, n, length, digest) + for p, n, length in ((2, 2, 6), (2, 3, 4), (3, 2, 4))] + result = {"status": "PASS_CAUSAL_QUERY_CACHE_STOCK", "domains": domains, + "matrix_compiler": matrix_checks(), "family": family_checks(), + "rejection_controls": controls(), "stream_digest": digest.hexdigest()} + result["files"] = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(PACKAGE.iterdir()) if path.is_file()} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()