From cab3df8a0e45d3ba72a898c062afe7bcc2a294cc Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 21:26:52 +0000 Subject: [PATCH] feat(research): minimize completed partial-echo source injections --- research/completed-partial-echo/PROOF.md | 149 ++++++++++ research/completed-partial-echo/README.md | 160 ++++++++++ research/completed-partial-echo/SOURCES.json | 30 ++ research/completed-partial-echo/TASK.json | 108 +++++++ research/completed-partial-echo/VERIFY.json | 37 +++ research/completed-partial-echo/verify.py | 294 +++++++++++++++++++ 6 files changed, 778 insertions(+) create mode 100644 research/completed-partial-echo/PROOF.md create mode 100644 research/completed-partial-echo/README.md create mode 100644 research/completed-partial-echo/SOURCES.json create mode 100644 research/completed-partial-echo/TASK.json create mode 100644 research/completed-partial-echo/VERIFY.json create mode 100644 research/completed-partial-echo/verify.py diff --git a/research/completed-partial-echo/PROOF.md b/research/completed-partial-echo/PROOF.md new file mode 100644 index 0000000000..455e00e1bf --- /dev/null +++ b/research/completed-partial-echo/PROOF.md @@ -0,0 +1,149 @@ +# The exact completed-observation injection tariff + +This contribution was produced by Nick Petalas. It is a scoped written +algebraic proof. Exact finite checks corroborate the implementation; they +are not a proof-kernel verification or a multiplication theorem. + +## Boundary and alphabet + +Work over any field of characteristic zero. Let X and W be vectors in the +same nonzero finite-dimensional space, and let D be a vector in another +nonzero finite-dimensional space. All three incoming vectors are arbitrary +and independent. X is an immutable source, W is borrowed dirty workspace, +and D is an additive receiver. There is no other data storage. + +Fix s independently arbitrary linear maps L_i from the source space to the +receiver space. A word must work uniformly for every tuple of these maps. +Its available instructions, including their positive complete prices, are + +| Instruction | Action | Price | +| --- | --- | --- | +| H_i | D += L_i W | c_i^+ | +| H_i inverse | D -= L_i W | c_i^- | +| J_+ | W += X | a | +| J_- | W -= X | b | + +Every instruction leaves the other fields unchanged. H_i and its inverse +are fixed indivisible source-preserving blocks, including any internal +workspace restoration and normalization. No direct L_i X evaluation, +scalar rescaling, output feedback, query retention, map-dependent word, +additional borrowed field or free copying is permitted. Repetition and +arbitrary interleaving of all labels are allowed. In particular, a lower +bound may not assume that only H_i occurs between checkpoints i-1 and i. + +There are ordered, read-only output checkpoints O_1,...,O_s. At O_j the +required receiver is exactly + + D_initial + (L_1 + ... + L_j) X. + +The observer sees only D. W need not have its incoming value at a checkpoint. +At return, X and W must both equal their incoming values, and D must still +equal its final observed value. Observation execution has a separate cost, +common to every compared word and excluded from this instruction tariff. + +## Theorem + +The exact minimum complete instruction price is + + sum_i (c_i^+ + c_i^-) + ceil(s/2) (a+b). (1) + +In particular, exactly 2 ceil(s/2) source injections suffice. Every word +needs at least one forward and one inverse use of each label and at least +ceil(s/2) uses of each injection direction. These bounds hold simultaneously +and are simultaneously attained, for arbitrary positive prices. + +The unit-price minimum is 2s + 2 ceil(s/2). Separately executing s ordinary +restored echoes costs 4s. For s=2 the minimum falls from eight to six, with +both complete partial outputs observed. This comparison does not remove +any child calls. If a complete array injection costs N scalar additions, +the saving is 2 floor(s/2) N additions, before any changed routing costs. + +## Lower bound + +At every time the workspace has the form W_initial + eX, where e is an +integer. It starts with e=0. Only J_+ and J_- change it, by +1 and -1. + +For each label i let A_i and B_i be the integer coefficients in the +receiver expression + + D = D_initial + sum_i (A_i L_i W_initial + B_i L_i X). + +Initially all coefficients are zero. An H_i instruction with sign +epsilon in {+1,-1} changes A_i by epsilon and B_i by epsilon e. +Injections change none of these coefficients. + +Uniformity in the independently arbitrary maps, together with independent +arbitrary X and W_initial, makes coefficient comparison legitimate. +For example, set all maps except L_i to zero and then set either input +vector to zero. A nonzero scalar multiple of every possible L_i cannot +vanish in characteristic zero. Thus at checkpoint j necessarily + + A_i = 0 for every i; B_i = 1 if i <= j, else 0. (2) + +Include time zero as checkpoint zero. In the interval from checkpoint +i-1 to checkpoint i, A_i changes by zero while B_i changes by one. +Consequently the net number of forward minus inverse H_i instructions +in that interval is zero, and some H_i instruction must occur. There +must be at least one of each sign. Summing these label-specific bounds +gives the first term of (1), even if other labels occur in those intervals. + +Every one of the s checkpoint intervals contains an injection. Otherwise +e would be constant on that interval, and the changes for every label +would satisfy Delta B_i = e Delta A_i. Equation (2) would give the +contradiction 1=0 for its newly observed label. + +Let u,v be the total numbers of J_+,J_- instructions, including any +instructions after the final observation. Exact return of arbitrary W +requires u=v. Therefore 2u=u+v>=s, so u=v>=ceil(s/2). +All prices are positive. Adding these simultaneous bounds proves (1). + +## Attainment and the first improvement + +Start with e=0. For odd i execute the chronological triple + + H_i inverse; J_+; H_i; observe O_i. + +Its receiver change is -L_i W_initial + L_i(W_initial+X)=L_i X, +and it changes e from zero to one. For even i execute + + H_i; J_-; H_i inverse; observe O_i. + +Its receiver change is L_i(W_initial+X)-L_i W_initial=L_i X, +and it changes e from one to zero. These statements preserve arbitrary +incoming D and every prior completed output. If s is odd, finish with J_-. +If s is even no final instruction is needed. The final correction changes +only W, so the last observed output is preserved at return. + +The word uses each H_i once in each direction, ceil(s/2) J_+ instructions, +and ceil(s/2) J_- instructions. It attains every bound above. + +For the smallest strict improvement, s=2, the complete word is + + H_1 inverse; J_+; H_1; O_1; H_2; J_-; H_2 inverse; O_2. + +At O_1 the workspace is W_initial+X; at O_2 and return it is W_initial. +Both receiver observations contain the external-source update, without +any contribution from W_initial. No hidden receiver observation is used. + +## Relation to the cyclic question and its limit + +PR4860 asks for completed partial external-source echoes, beyond its +canonical partial-batch record. The present result answers the normalized +block subproblem: supply a complete canonical batch H_i, price that block +and its actual inverse, and then apply the schedule above. Ross Richardson's +PR1287 supplies the cyclic-equivariant batching and ordinary dirty echo; +PR4860 supplies the canonical normalization tariff. Their costs are included +in c_i^+,c_i^- and are not re-established here. + +The observer must allow the borrowed workspace to retain the shift X at odd +checkpoints. If W is also required to be restored at every observation, +the same proof applied within each interval forces at least one injection +of each sign there. Separate echoes then attain the exact price + + sum_i (c_i^+ + c_i^-) + s(a+b). + +This explains the source of the saving and its boundary. It is not a claim +that canonical cyclic frames may be ignored inside a child, or that a caller +permits shifted workspace at its observations. No actual selected supplier +or observer is bound. The five framework assumptions, physical movement, +native access, ownership, precision, compiler and outer funding remain open. diff --git a/research/completed-partial-echo/README.md b/research/completed-partial-echo/README.md new file mode 100644 index 0000000000..1d63aa5a4b --- /dev/null +++ b/research/completed-partial-echo/README.md @@ -0,0 +1,160 @@ +# Completed partial echoes share source injections + +This contribution was produced by Nick Petalas. Claim type: scoped algebraic +construction and exact optimality proof, with finite corroboration. No new +kappa or physical supplier is claimed. + +Two successive complete external-source updates need six macro calls rather +than eight separate-echo calls, while preserving every observed output and +restoring arbitrary borrowed data. The new step answers the normalized-block +part of [PR4860's second open question](https://github.com/CrocSwap/integer-mult-bounds/pull/4860). + +For s independently arbitrary linear blocks + + H_i(D,W) = (D + L_i W, W), + +let the complete forward/inverse prices be c_i^+,c_i^-. The only additional +instructions are W += X and W -= X, priced a,b>0. X is immutable; X,W,D +all start arbitrary. At checkpoint j the observer must see precisely +D_initial + sum_(i<=j) L_i X. It observes D only. W may retain a source shift +between checkpoints and must return exactly to its incoming value. + +For every s>=1 over a characteristic-zero field, the exact minimum is + + sum_i (c_i^+ + c_i^-) + ceil(s/2) (a+b). + +Every uniform word needs at least one use of each H_i direction, and at least +ceil(s/2) injections of each sign. The same word attains all these bounds, +even with unequal positive prices. The lower bound permits arbitrary +repetitions and interleavings of every child label. + +The first strict improvement is this chronological word: + +```text +H_1 inverse; W += X; H_1; observe D_initial + L_1 X +H_2; W -= X; H_2 inverse; observe D_initial + (L_1+L_2) X +``` + +The workspace is W_initial+X at the first observation and W_initial at +return. Each output is already complete when observed. For unit prices, +the optimum is 2s+2 ceil(s/2), versus 4s for separate restored echoes. No +child call is removed. With N scalar additions per array injection, the +copying saving is 2 floor(s/2) N, before any changed routing costs. + +[PROOF.md](PROOF.md) supplies the coefficient comparison, injection lower +bound, attaining word and the contrasting restored-workspace boundary. +If W must also be restored at every checkpoint, the exact price is instead +sum_i(c_i^++c_i^-)+s(a+b). Thus the saving requires an explicit observer and +workspace contract. + +## Evidence and reproduction + +The standard-library verifier is read-only. From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/completed-partial-echo/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/completed-partial-echo/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/completed-partial-echo +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/completed-partial-echo --check-source-history +``` + +Substitute another CPython 3.12 path elsewhere. The last command checks +publication bytes and declared source ancestry after committing. Expected +markers are PASS_COMPLETED_PARTIAL_ECHO, PASS_REGISTERED_RESEARCH_PACKAGE +and PASS_RESEARCH_COMMIT_BYTES. + +The checks enumerate: + +- 1,600 exact weighted schedule cases through 64 blocks, including unequal + forward/inverse prices and rational injection prices. All 64 shared and + separate-echo words check every formal checkpoint and final return. +- 448 literal matrix fixtures, 2,328 independent X/W/D input columns and + 6,294 complete output observations. These include all scalar map tuples + over {-1,0,1} through four blocks, all pairs of binary-entry 2-by-2 maps + interpreted in characteristic zero, and rectangular rational fixtures. +- Eight separately implemented shortest-word searches for one or two blocks + with positive integer prices. They permit repeated labels, arbitrary + interleavings and source shifts outside {0,1}; they do not assume the + attaining schedule. The unit-price minima are four and six. +- Seventeen rejection controls for omitted directions, reversed injections, + missing observations, unreturned workspace, post-observation corruption, + dependence on repeated maps, a wrongly canonical workspace boundary, and + invalid counts or inexact prices. Checks remain active with optimization. + +Each run emits a generated receipt bound to the six package files and both +declared predecessor text inputs by SHA256. Counts are recomputed, and no +handwritten receipt is used. The all-length lower bound is the written proof; +the finite searches do not exhaust arbitrary word lengths or field elements. + +## Scope, costs and provenance + +Canonical base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8. +The selected record remains PR6030. TASK.json records the change from the +formal-interface card to this abstract boundary subproblem. The current +selected-baseline binding control passed; no selected scientific replay is +part of this result. SOURCES.json pins the catalogue, selected record and +two predecessor READMEs. The verifier authenticates the latter without +importing or replaying their implementations. + +Ross Richardson's PR1287 supplies complete cyclic-equivariant batches and +ordinary dirty echoes. PR4860 supplies the canonical batch tariff and asks +for completed external-source observations. Here every H_i includes its +complete normalization, internal scratch restoration and literal inverse +cost. A block's internal cyclic frame cannot be ignored to claim this saving. +The new proof concerns the outer observation/injection schedule only. + +This is a uniform-word theorem for independently arbitrary maps. Special +relations among fixed L_i can permit other words. Direct L_i X calls, +opened child bodies, scalar rescaling, output feedback, additional fields, +query records, adaptive observations or map-dependent words change the +alphabet and are outside scope. Observation execution and physical source +movement have separate costs. No actual native caller, precision/ownership +contract, tape program, compiler closure, complete signed invoice or outer +funding is supplied. The five inherited framework assumptions remain. +Independent human and formal proof-kernel review are unclaimed. + +The bounded implementation accepts at most 64 blocks and 384 instructions. +Exact positive prices are at most 4096 with denominator at most 4096. Payload +fixtures use at most eight blocks and three coordinates per field. Shortest +paths use at most two labels, cost 18 and one million queue removals, with +explicit failure on exhaustion. No recursion, dynamic code, subprocess, +network access or write occurs in the verifier. Python dynamic allocations +are a Power of Ten rule-3 deviation; these enforced finite domains bound +live state. Warning-strict normal and optimized execution supplies interpreter +diagnostics. There is no fixed-memory implementation or performance claim. + +## Open next questions + +1. Does one actual cyclic-equivariant caller permit shifted borrowed workspace + at a completed output observation? Pin one normalized block, its literal + inverse and the observer's read set, then charge every injection and route. + That missing physical boundary prevents applying the saving to a supplier. +2. What is the optimum if cyclic normalization and source injection may be + interleaved inside the blocks? Begin with one literal child alphabet and + full observer contract. This theorem treats H_i as indivisible and supplies + no optimum for that changed alphabet. + +## Overlap and credit + +The source question is Nick Petalas's PR4860, published October 22, 2026. +Live open PRs, recent account targets, handoff claims, local reservations, +main README searches and merged formula/object searches were checked. +No recent account target cited PR4860. Sparse local notes, unpublished work +and arbitrary historical diffs remain coverage limits. + +The binary partial-output-observation model of commdata2338's PR2020 and +PR5968 fixes drifting two-XOR children and hides a receiver row. This result +observes the whole completed receiver after every update and uses normalized +arbitrary signed linear blocks. Their adapter minima are not recomputed. +PR3417 serializes independent roots with unobserved outputs; its boundary +explicitly excludes intermediate observations. The Boolean multilinear +dirty-input query theorem in PR6393 has one final output and another alphabet; +it does not price these ordered completed observations. + +Credit Ross Richardson / PR1287 for cyclic batching and complete dirty echoes; +Nick Petalas / PR4860 for the normalized observation question; Sagar Thakrar / +PR1227, mightyOil / PR1203, Adam Gall / PR1205, Hanson Sun / PR1488, Cinna Davis / +PR1391, and the retained restoration/echo lineage. Classical linearity and +signed cancellation are used without a global mathematical-priority claim. +Frozen predecessor files and their credit are unchanged. New work is +Apache-2.0. diff --git a/research/completed-partial-echo/SOURCES.json b/research/completed-partial-echo/SOURCES.json new file mode 100644 index 0000000000..492ef126e3 --- /dev/null +++ b/research/completed-partial-echo/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/cyclic-checkpoint-cost/README.md", + "usage": "input", + "git_blob": "00208eb7a03097e4b2f0d9cb25bfaa1d145d9b67", + "sha256": "f4249104e6418596846ad3d6f05067b83b06d021b20edb0c2961b8a50d46ff0e" + }, + { + "path": "research/cyclic-output-restoration/README.md", + "usage": "input", + "git_blob": "2cb99db015f3b24a1fc31158013cf408b75b0225", + "sha256": "fc56e55e76a4d41d9da442ee1af63b4032eb41267a80500814f81027cc0fd087" + } + ] +} diff --git a/research/completed-partial-echo/TASK.json b/research/completed-partial-echo/TASK.json new file mode 100644 index 0000000000..78f5eb9c01 --- /dev/null +++ b/research/completed-partial-echo/TASK.json @@ -0,0 +1,108 @@ +{ + "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 positive weighted instruction tariff for completed partial external-source echoes through normalized indivisible source-preserving blocks, with arbitrary dirty workspace restored at return.", + "scope_change_reason": "The formal-interface card is narrowed to PR4860 Open next question 2 after complete cyclic normalization. This is an abstract observation/injection result, without physical supplier admission.", + "bottleneck_link": "Sharing source injections removes ordinary copying work without removing child calls. It identifies the precise workspace observation contract needed before a physical caller can use the saving.", + "budget_minutes": 60, + "stop_rule": "Stop at the first strict completed-observation improvement; package the six-call two-block word and its matching general tariff. No further construction search.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal theorem; verify.py checks formal coefficients, literal arbitrary-dirty columns, weighted words, bounded shortest paths and semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does one actual cyclic-equivariant caller permit W_initial+X at an output-only observation?", + "why_it_matters": "That boundary permits the injection saving; requiring restored W at every observation removes it.", + "first_step": "Pin one normalized batch, its literal inverse and exact observer read set; price all injections and routing.", + "blocked_by": "No selected supplier or physical observer is bound here." + }, + { + "question": "What is the optimum when canonical child normalization and source injections may be interleaved?", + "why_it_matters": "The present theorem includes complete H_i prices and does not optimize inside those blocks.", + "first_step": "Write one literal cyclic-child and observation alphabet with every source/frame cost.", + "blocked_by": "Opening the normalized blocks changes the alphabet and needs its own proof and full endpoint invoice." + } + ], + "source_question": { + "source": "PR #4860", + "author": "petalas", + "question": "Open next question 2: completed partial external-source echoes", + "created_at": "2026-10-22T22:22:11Z" + }, + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360871" +} diff --git a/research/completed-partial-echo/VERIFY.json b/research/completed-partial-echo/VERIFY.json new file mode 100644 index 0000000000..430f1e2c7e --- /dev/null +++ b/research/completed-partial-echo/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cyclic-checkpoint-cost/README.md", + "research/cyclic-output-restoration/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Formal completed partial outputs and exact dirty returns; literal basis columns; positive unequal prices; independent bounded repeated-label shortest words; semantic and invalid-input rejections; pinned input bytes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact verification with assertions disabled." + } + ] +} diff --git a/research/completed-partial-echo/verify.py b/research/completed-partial-echo/verify.py new file mode 100644 index 0000000000..28f24f2f84 --- /dev/null +++ b/research/completed-partial-echo/verify.py @@ -0,0 +1,294 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact completed-observation echo words; all checks survive Python -O.""" +from __future__ import annotations + +import hashlib +import heapq +import itertools +import json +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +MAX_BLOCKS = 64 +MAX_WORD = 384 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def size(n): + need(type(n) is int and 1 <= n <= MAX_BLOCKS, "invalid block count") + + +def price(value): + need(type(value) in (int, Fraction), "price must be exact") + q = Fraction(value) + need(0 < q <= 4096 and q.denominator <= 4096, "price out of range") + return q + + +def optimum(forward, inverse, up, down): + size(len(forward)) + need(len(inverse) == len(forward), "price dimensions") + f = tuple(price(x) for x in forward) + r = tuple(price(x) for x in inverse) + return sum(f) + sum(r) + ((len(f) + 1) // 2) * (price(up) + price(down)) + + +def schedule(n, eager=False): + size(n) + word = [] + for i in range(n): + sign = 1 if eager or i % 2 == 0 else -1 + word.extend((("H", i, -sign), ("J", -1, sign), ("H", i, sign))) + if eager: + word.append(("J", -1, -1)) + word.append(("O", i, 0)) + if not eager and n % 2: + word.append(("J", -1, -1)) + need(len(word) <= MAX_WORD, "word capacity") + return tuple(word) + + +def parse_word(word, n): + size(n) + need(type(word) is tuple and len(word) <= MAX_WORD, "word capacity/type") + for op in word: + need(type(op) is tuple and len(op) == 3, "instruction shape") + tag, i, sign = op + need(type(i) is int and type(sign) is int, "instruction integer type") + if tag == "H": + need(0 <= i < n and sign in (-1, 1), "child instruction") + elif tag == "J": + need(i == -1 and sign in (-1, 1), "injection instruction") + elif tag == "O": + need(0 <= i < n and sign == 0, "observation instruction") + else: + raise ValueError("unknown instruction") + + +def formal(word, n, canonical=False): + """Track coefficients of independent L_i W_initial and L_i X.""" + parse_word(word, n) + e, observed = 0, 0 + dirt, source = [0] * n, [0] * n + counts = [0, 0, 0, 0] + for tag, i, sign in word: + if tag == "H": + dirt[i] += sign + source[i] += sign * e + counts[sign == -1] += 1 + elif tag == "J": + e += sign + counts[2 + (sign == -1)] += 1 + else: + need(i == observed, "observation order") + need(dirt == [0] * n, "dirty output at observation") + need(source == [int(j <= i) for j in range(n)], "wrong partial output") + need(not canonical or e == 0, "noncanonical observed workspace") + observed += 1 + need(observed == n, "missing observations") + need(e == 0, "workspace not restored") + need(dirt == [0] * n and source == [1] * n, "wrong returned output") + return tuple(counts) + + +def literal(word, maps): + """Separate payload execution on every X/W/D input basis column.""" + n, rows, cols = len(maps), len(maps[0]), len(maps[0][0]) + need(1 <= n <= 8 and 1 <= rows <= 3 and 1 <= cols <= 3, "fixture capacity") + need(all(len(m) == rows and all(len(r) == cols for r in m) for m in maps), + "literal matrix dimensions") + parse_word(word, n) + probes, cuts = 0, 0 + for column in range(2 * cols + rows): + x = [int(column == j) for j in range(cols)] + w = [int(column == cols + j) for j in range(cols)] + d = [int(column == 2 * cols + j) for j in range(rows)] + incoming_w, incoming_d = tuple(w), tuple(d) + for tag, i, sign in word: + if tag == "J": + w = [a + sign * b for a, b in zip(w, x, strict=True)] + elif tag == "H": + d = [d[r] + sign * sum(maps[i][r][c] * w[c] for c in range(cols)) + for r in range(rows)] + else: + want = [incoming_d[r] + sum(maps[j][r][c] * x[c] + for j in range(i + 1) for c in range(cols)) for r in range(rows)] + need(d == want, "literal partial output") + cuts += 1 + need(tuple(w) == incoming_w, "literal dirty return") + need(x == [int(column == j) for j in range(cols)], "literal source return") + want = [incoming_d[r] + sum(matrix[r][c] * x[c] for matrix in maps + for c in range(cols)) for r in range(rows)] + need(d == want, "literal returned output") + probes += 1 + return probes, cuts + + +def advance(state, n): + e, a, b, observed = state + if observed < n and not any(a) and b == tuple(int(i <= observed) for i in range(n)): + observed += 1 + return e, a, b, observed + + +def shortest(n, forward, inverse, up, down, limit): + """Unrestricted repeated-label shortest words, within a finite cost bound.""" + need(n in (1, 2) and 1 <= limit <= 18, "search capacity") + start = (0, (0,) * n, (0,) * n, 0) + queue, distances = [(0, start)], {start: 0} + expanded, generated = 0, 0 + # Every edge costs >=1, so at most sum_(j=0)^limit (2n+2)^j words exist. + for _ in range(1_000_000): + if not queue: + return None, expanded, generated + cost, state = heapq.heappop(queue) + if cost != distances[state]: + continue + e, a, b, observed = state + if observed == n and e == 0 and not any(a) and b == (1,) * n: + return cost, expanded, generated + expanded += 1 + moves = [(up, (e + 1, a, b, observed)), (down, (e - 1, a, b, observed))] + for i in range(n): + for sign, charge in ((1, forward[i]), (-1, inverse[i])): + aa, bb = list(a), list(b) + aa[i] += sign + bb[i] += sign * e + moves.append((charge, (e, tuple(aa), tuple(bb), observed))) + for charge, target in moves: + generated += 1 + target = advance(target, n) + total = cost + charge + if total <= limit and total < distances.get(target, limit + 1): + distances[target] = total + heapq.heappush(queue, (total, target)) + raise ValueError("search state capacity exhausted") + + +def finite_searches(): + results = [] + for n in (1, 2): + fixtures = [(tuple([1] * n), tuple([1] * n), 1, 1), + (tuple(range(1, n + 1)), tuple(range(n, 0, -1)), 1, 2), + (tuple([2] * n), tuple([1] * n), 2, 1), + (tuple([1] * n), tuple([2] * n), 2, 3)] + for f, r, up, down in fixtures: + wanted = optimum(f, r, up, down) + need(wanted.denominator == 1, "integer search budget") + result, expanded, generated = shortest(n, f, r, up, down, int(wanted)) + need(result == wanted, "shortest-word mismatch") + results.append({"blocks": n, "forward": f, "inverse": r, + "up": up, "down": down, "optimum": result, + "expanded": expanded, "generated": generated}) + return results + + +def check_schedules(): + cases = 0 + prices = (1, 2, 3, Fraction(1, 2), Fraction(2, 3)) + for n in range(1, MAX_BLOCKS + 1): + word = schedule(n) + counts = formal(word, n) + need(counts == (n, n, (n + 1) // 2, (n + 1) // 2), "instruction counts") + eager_counts = formal(schedule(n, eager=True), n, canonical=True) + need(eager_counts == (n, n, n, n), "eager counts") + for up, down in itertools.product(prices, repeat=2): + f = tuple(Fraction(i + 1, 7) for i in range(n)) + r = tuple(Fraction(n - i, 5) for i in range(n)) + actual = sum(f[i] if s == 1 else r[i] for t, i, s in word if t == "H") + actual += sum(up if s == 1 else down for t, _, s in word if t == "J") + need(actual == optimum(f, r, up, down), "weighted tariff") + cases += 1 + return cases + + +def check_payloads(): + cases, probes, cuts = 0, 0, 0 + for n in range(1, 5): + for values in itertools.product((-1, 0, 1), repeat=n): + maps = tuple(((value,),) for value in values) + p, c = literal(schedule(n), maps) + cases, probes, cuts = cases + 1, probes + p, cuts + c + for entries in itertools.product((0, 1), repeat=8): + maps = tuple(tuple(tuple(entries[4 * i + 2 * r + c] for c in range(2)) + for r in range(2)) for i in range(2)) + p, c = literal(schedule(2), maps) + cases, probes, cuts = cases + 1, probes + p, cuts + c + for n, rows, cols in itertools.product(range(1, 9), range(1, 4), range(1, 4)): + maps = tuple(tuple(tuple(Fraction((i + r + 2 * c) % 5 - 2, c + 1) + for c in range(cols)) for r in range(rows)) for i in range(n)) + p, c = literal(schedule(n), maps) + cases, probes, cuts = cases + 1, probes + p, cuts + c + return {"fixtures": cases, "basis_columns": probes, "observations": cuts} + + +def controls(): + word = schedule(3) + mutants = [word[1:], word[:2] + word[3:], word[:-1], + tuple((t, i, -s if t == "J" else s) for t, i, s in word), + tuple(op for op in word if op[0] != "O"), + tuple((t, 0 if t == "H" else i, s) for t, i, s in word), + word + (("H", 0, 1),)] + rejected = 0 + for mutant in mutants: + try: + formal(mutant, 3) + except ValueError: + rejected += 1 + else: + raise ValueError("semantic mutant accepted") + try: + formal(schedule(2), 2, canonical=True) + except ValueError: + rejected += 1 + else: + raise ValueError("output checkpoint confused with workspace restoration") + for bad in (True, 0, 65, 1.0): + try: + schedule(bad) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid block count accepted") + for bad in (True, 0, -1, 0.5, Fraction(1, 4097)): + try: + optimum((1,), (1,), bad, 1) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid price accepted") + return rejected + + +def hashes(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + root = HERE.parent.parent + pins = {} + for row in sources["files"]: + if row["usage"] == "input": + digest = hashlib.sha256((root / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], "changed source bytes: " + row["path"]) + pins[row["path"]] = digest + files = sorted(HERE.iterdir()) + need(len(files) <= 12, "package file capacity") + return {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in files if p.is_file()}, pins + + +def main(): + files, pins = hashes() + result = {"weighted_schedule_cases": check_schedules(), "payloads": check_payloads(), + "shortest_words": finite_searches(), "rejections": controls(), + "package_sha256": files, "input_sha256": pins, + "scope": "Scoped written proof and exact finite corroboration; no supplier or kappa."} + print(json.dumps(result, sort_keys=True)) + print("PASS_COMPLETED_PARTIAL_ECHO") + + +if __name__ == "__main__": + main()