diff --git a/research/dirty-echo-maximal-equality/PROOF.md b/research/dirty-echo-maximal-equality/PROOF.md new file mode 100644 index 0000000000..5de0f4702c --- /dev/null +++ b/research/dirty-echo-maximal-equality/PROOF.md @@ -0,0 +1,148 @@ +# The maximal equality interval for reserved-scratch dirty echoes + +This scoped combinatorial proof is produced by Nick Petalas. The tree model, +echo semantics and universal lower bound are inherited from Alexander +Schwartzman's [PR784](https://github.com/CrocSwap/integer-mult-bounds/pull/784). +Gareth Davidson's [PR887](https://github.com/CrocSwap/integer-mult-bounds/pull/887) +formalizes the preceding sufficient equality interval. Neither predecessor +claims that interval is maximal. The contribution here is the exact maximal +interval and the complete recursive equality characterization. + +## Model and theorem + +An ordered tree has no unary nodes. A leaf has factor count n=1, completed +call count N=1 and scratch requirement S=0. A node with k>=2 children obeys + +``` +n = sum n_i, +N = 2 N_1 + 4 sum_(1=B_s(n) whenever S<=s. +The new theorem is + +``` +there exists a tree with S<=s, n leaves and N=B_s(n) + if and only if a_s <= n <= 2^s. +``` + +In this interval the exact minimum completed call count is B_s(n). Outside +it, no feasible tree attains that affine bound. The statement includes s=0, +where the unique equality tree is one leaf, and s=1, where it is a binary +pair. Every equality tree uses the full available budget. + +For example s=4,n=11 has exact minimum 96. Its ternary root has child leaf +counts (4,3,4), child calls (16,8,16) and child budgets (2,2,2). Thus the +root bill is 2*16+4*8+2*16=96, with four reserved scratch arrays. The prior +sufficient interval at s=4 started at n=12. PR784 already tabulates finite +optima; this example illustrates the new general theorem and is not claimed +as a newly discovered numerical minimum. + +## Exact slack identity and all equality trees + +Let delta_s(T)=N(T)-B_s(n(T)). For a leaf, + +``` +delta_s(leaf) = (2^s-1)^2. +``` + +For an internal root of arity k, put r=s-k+1, p=2^r, t=2^(k-1), +and w_1=w_k=2, with interior weights w_i=4. Every child has S_i<=r, +so r>=0. Direct substitution gives the exact identity + +``` +delta_s(T) = sum_i w_i delta_r(T_i) + + 2p sum_i (t-w_i)(p-n_i) + + p^2 (t-2)(t-2k+2). (1) +``` + +Indeed sum w_i=4k-4 and 2^s=pt. Expanding the right side cancels the +constant and linear terms to N(T)-2pt sum n_i+p^2 t^2. +All three terms on the right are nonnegative: the predecessor's bound gives +child slack, capacity gives n_i<=p, t>=w_i, and t>=2k-2 for k>=2. +For k>=4, t>2k-2 and t>2, so the final term is strictly positive. +This extracts equality conditions from the inherited inequality without +assuming the predecessor's sufficient construction is exhaustive. + +Consequently every equality tree, and only such a tree, follows these rules +with the indicated contextual budget: + +1. At s=0 it is a leaf. A leaf at any s>0 is not tight. +2. A binary root at s>=1 has two equality children at budget s-1. +3. A ternary root at s>=2 has three equality children at budget s-2, + and its first and last children each have exactly 2^(s-2) leaves. +4. No node with arity at least four occurs. + +For rule 3, the endpoint coefficients t-w_i equal 2, while the middle +coefficient is zero. This proves necessity and sufficiency directly in (1). +A tree of capacity 2^r at budget r is the unique perfect binary tree of +height r. To see this, a root of arity k>=3 has at most +k*2^(r-k+1)<2^r leaves; a binary root must have both children at capacity, +and induction finishes. Thus the endpoint subtrees in rule 3 are uniquely +specified. The classification concerns ordered shapes, not uniqueness of +all equality trees or of schedules in a larger reversible-program class. +Induction on these rules also gives S=s for every equality tree. + +## Exact interval, necessity and constructive sufficiency + +Let E_s be the set of equality leaf counts. The classification yields + +``` +E_0 = {1}, E_1 = {2}, +E_s = (E_(s-1) + E_(s-1)) union (2^(s-1) + E_(s-2)), s>=2, (2) +``` + +where the first plus is the set of pairwise sums and the second translates +a set. Both directions of (2) are constructive because children occupy +consecutive factor intervals. Endpoint perfect binary trees use no extra +space beyond their prescribed child budgets. + +Inductively suppose E_j=[a_j,2^j] over the integers for smaller budgets. +The binary part of (2) is the whole interval +[2a_(s-1),2^s]. The ternary part is +[2^(s-1)+a_(s-2),3*2^(s-2)]. The lower ternary endpoint equals a_s, +since subtracting the integer 2^(s-1) from 2^(s+1)/3 leaves 2^(s-1)/3. +The lower binary endpoint is either a_s or a_s+1. For completeness, + +``` +2 ceil(2^s/3) = a_s + 1, if s is even, +2 ceil(2^s/3) = a_s, if s is odd. +``` + +Also a_s<=3*2^(s-2), because the expression on the right is an integer +at least 2^(s+1)/3. Hence these two integer intervals overlap or are +adjacent, their union is exactly [a_s,2^s], and no smaller leaf count is +possible. This proves the claimed maximal interval for every s. + +An explicit constructor uses a binary root whenever n>=2a_(s-1). +Set the first child size to max(a_(s-1),n-2^(s-1)) and the second to the +remaining size. Both lie in [a_(s-1),2^(s-1)]. If this test fails, use a +ternary root with endpoint sizes 2^(s-2) and middle size n-2^(s-1). +The interval argument places that middle size in E_(s-2). Repeat down +to s=0. The implementation uses a bounded iterative worklist. + +## Scope + +This is an all-size written theorem about a specified tree grammar, with +finite exact corroboration. It supplies no new multiplication exponent, +physical supplier, tape implementation, weighted-price optimum, precision +bound, nonlinear-gate statement or full multiplication theorem. Connector +reuse, clean checkpoints, changing the echo word, interleaved lifetimes, +borrowing ancestor arrays and arbitrary reversible programs are outside it. +The predecessor's unfavorable full-supplier bill is unchanged. The proof is +not checked by a formal kernel; the earlier Lean theorem has not been +extended or rerun. No predecessor audit is a deliverable of this package. diff --git a/research/dirty-echo-maximal-equality/README.md b/research/dirty-echo-maximal-equality/README.md new file mode 100644 index 0000000000..132591ba4a --- /dev/null +++ b/research/dirty-echo-maximal-equality/README.md @@ -0,0 +1,105 @@ +# The exact maximal equality band for dirty echoes + +For the ordered reserved-parent-scratch echo grammar of Alexander +Schwartzman's [#784](https://github.com/CrocSwap/integer-mult-bounds/pull/784), +the affine lower bound is attained exactly when + +``` +ceil(2^(s+1)/3) <= n <= 2^s, +min N = 2^(s+1)n - 4^s. +``` + +This extends the preceding sufficient band `3*2^(s-2) <= n <= 2^s`. +[PROOF.md](PROOF.md) also characterizes every equality tree. Its exact slack +identity permits binary nodes with tight children and ternary nodes with +capacity-saturating endpoints; larger arities have positive slack. +At four scratch arrays the new theorem includes eleven factors and 96 +complete calls. The predecessor's finite table already includes this +numerical optimum. The contribution is the all-size maximality theorem, +not a replay or recount of that table. + +Claim type: scoped proof with exact finite corroboration. No new kappa, +physical supplier or complete multiplication theorem is claimed. +This contribution is produced by Nick Petalas. Independent human and +formal proof-kernel review are unclaimed. + +## Reproduce + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/dirty-echo-maximal-equality +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/dirty-echo-maximal-equality --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dirty-echo-maximal-equality/verify.py +``` + +The first command runs both registered checks. A portable reviewer can replace +the absolute interpreter path with their CPython 3.12 executable. The scientific +verifier also runs outside Git. It compares every field of the generated +[RESULT.json](RESULT.json), including source hashes, and prints +`PASS_DIRTY_ECHO_MAXIMAL_EQUALITY`. `--write /absolute/new/file.json` creates +an exclusive generated receipt and refuses an existing path. + +[oracle.py](oracle.py) independently minimizes over every root arity and +positive child-size composition, without using the new equality threshold. +It checks all budgets 0..8 and factor counts 1..256. A separate whole-tree +enumerator checks the recursive characterization on every ordered tree through +eight leaves, including nonoptimal shapes and every fitting budget through +eight. The constructor supplies every equality size through budget eight. +Boundary and corruption controls run under optimized Python as well. +Finite checks support the written proof; they do not establish its universal +quantifiers by enumeration. Exact coverage is generated in RESULT.json. +No predecessor verifier, Lean build or supplier replay is run. + +## Credit and source boundary + +Alexander Schwartzman #784 supplies the lower bound and sufficient equality +family. Gareth Davidson #887 supplies its scoped Lean formalization, explicitly +without maximality. The original multiway echo and restoration semantics are +androolloyd's #673. Credit Koroffstrogov #758 for the all-arity optimizer, +Sagar Thakrar #730 for ordered binary/ternary optimization, Dillon Amburgey +#689 for the balanced ternary baseline, and the retained Chafik Boukhalfa +#628 leaf lineage. No predecessor implementation is copied or imported. +[SOURCES.json](SOURCES.json) pins the statements as historical provenance. +The model and the necessary definitions are stated completely in PROOF.md. +The source contexts are cited premises; their computations are not rechecked. + +The entry cached scan covered 379 open PRs and 3,859 Discussion records, +with complete reported pagination. Its local corpus included only 102 of +6,319 tracked notes. Relevant predecessor notes were then materialized. +Live handoffs, relevant PR bodies, merged-term searches and all-main README +searches supplement the scan. They do not cover unpublished work or prove +literature novelty. The canonical claim is in +[handoffs #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133745). +New files are Apache-2.0. + +## Limits and verification policy + +The theorem keeps unit leaf prices, all inverse/restoration calls, ordered +factors, static trees and parent-reserved dirty arrays. It does not cover +connector reuse, clean checkpoints or arbitrary reversible programs. The full +supplier bill remains a separate, unfavorable predecessor interface; local +call optimality does not improve kappa. A formal-kernel extension, physical +caller and weighted analogue remain unrun or unresolved. + +The new Python code has bounded inputs and iterative traversals. Functions +fit within 60 physical lines. Explicit exceptions remain active under `-O`. +Managed Python and itertools allocate at runtime, a Power of Ten deviation; +fixed domains of at most 256 leaves, budget eight and eight-leaf exhaustive +trees bound live data. Strict-warning normal/optimized runs and corruption +controls provide the applicable diagnostics. The local oracle import uses one explicit path and the receipt binds its +bytes. Rejection controls dispatch only to two named validation functions. +These bounded Python mechanisms are documented deviations from the strict +metaprogramming and indirect-call rules. No static type checker is configured +for this standalone integer verifier; syntax compilation and strict-warning +execution are the available language diagnostics. + +## Open next questions + +- Determine a closed form for the number of equality trees at each `(s,n)`. + Start from the disjoint binary/ternary shape recurrence in PROOF.md. + This would distinguish existence from schedule multiplicity; no physical + caller is needed, but no such count is proved here. +- Find a useful analytic bound for unequal leaf prices under the same scratch + contract. Start with one fixed ordered price vector and keep all restoration + multipliers. The maximal unit-price equality band alone does not solve it. diff --git a/research/dirty-echo-maximal-equality/RESULT.json b/research/dirty-echo-maximal-equality/RESULT.json new file mode 100644 index 0000000000..dda8d69185 --- /dev/null +++ b/research/dirty-echo-maximal-equality/RESULT.json @@ -0,0 +1,69 @@ +{ + "controls": { + "rejected_inputs": 22, + "structural_controls": 2 + }, + "examples": [ + { + "budget": 4, + "calls": 96, + "leaves": 11, + "postfix_sha256": "c2ef8701595d8fec3daf5c9bf73d14a704b9a4a824b8a15e34adf56cb2d82245", + "scratch": 4 + }, + { + "budget": 6, + "calls": 1408, + "leaves": 43, + "postfix_sha256": "170fe6ff4215c2414a59d88554ef5f8ed44288005728da345265bd0e6b061d6a", + "scratch": 6 + }, + { + "budget": 8, + "calls": 22016, + "leaves": 171, + "postfix_sha256": "f3060db63c8c36e92101a97734bcae5a629596c72a3ca4c4acde415fa3ad0bc9", + "scratch": 8 + } + ], + "minima": { + "cells": 2304, + "equality_sizes_per_budget": [ + 1, + 1, + 2, + 3, + 6, + 11, + 22, + 43, + 86 + ], + "transitions": 51374, + "witnesses": 175 + }, + "schema_version": 1, + "scope": "Scoped written theorem; finite exact corroboration only", + "shapes": { + "equality_occurrences": 9, + "tree_budget_comparisons": 48960, + "trees": 5440, + "trees_per_size": [ + 1, + 1, + 3, + 11, + 45, + 197, + 903, + 4279 + ] + }, + "source_sha256": { + "PROOF.md": "9994f4350e550abd2c31417e8ef4e6846729d9f55bc4159ac0eb68811348580d", + "oracle.py": "f3dcd19bb3286e8fb904ad9fa72308af910911eb0eedeb61bf50f91dc1949d86", + "test_package.py": "397c1040ba0d2a0b72f1aeb55e61195ceee5419014b40c7d26743cc8935d0274", + "verify.py": "c5e3443a901a781f8f8a74343f47f8ded7d16720071db70eaf6acdc9f23abf40" + }, + "status": "PASS_DIRTY_ECHO_MAXIMAL_EQUALITY" +} diff --git a/research/dirty-echo-maximal-equality/SOURCES.json b/research/dirty-echo-maximal-equality/SOURCES.json new file mode 100644 index 0000000000..76e67818c9 --- /dev/null +++ b/research/dirty-echo-maximal-equality/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/dirty-echo-space-budget/PROOF.md", + "usage": "provenance", + "git_blob": "3a7c2f4c84b06592c54a518441f554210867b9f0", + "sha256": "b3c290eb501ac3c806838677aaa50546d2443e638d6f67ac37711c0646fe30ac" + }, + { + "path": "research/lean-dirty-echo-budget/README.md", + "usage": "provenance", + "git_blob": "3727dca7f51ec11fa2543eaaa4c76261e1a58db1", + "sha256": "1795505e18337bcc041eaf579ef666ca3789f85a6ab45da9f5b382d2290cd362" + } + ] +} diff --git a/research/dirty-echo-maximal-equality/TASK.json b/research/dirty-echo-maximal-equality/TASK.json new file mode 100644 index 0000000000..f875aba7d6 --- /dev/null +++ b/research/dirty-echo-maximal-equality/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "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_status": "changed", + "actual_scope": "Determine the exact maximal equality interval and every equality shape for the reserved-scratch all-arity dirty-echo lower bound.", + "scope_change_reason": "Original recursive-interface combinatorial extension of the explicitly nonmaximal sufficient band in Alexander Schwartzman PR784; no audit or re-verification deliverable.", + "bottleneck_link": "Self-contained side result on the exact local restoration-call versus dirty-workspace tradeoff. It does not satisfy the QQ16 physical consumer gate or improve the selected supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after proving the first maximality extension and checking the independent recurrence and exhaustive small shapes; package without enlarging the mechanism.", + "outcome": "completed", + "evidence": "PROOF.md supplies the universal maximality and shape theorem; RESULT.json is generated by verify.py using independent oracle.py and optimized test_package.py controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Count equality trees for each budget and factor count.", + "why_it_matters": "Distinguishes optimal schedule multiplicity from existence.", + "first_step": "Use the disjoint binary/ternary shape recurrence in PROOF.md.", + "blocked_by": "A closed coefficient formula is not derived." + }, + { + "question": "Find analytic unequal-price bounds in the same ordered grammar.", + "why_it_matters": "Complete leaves can have different physical costs.", + "first_step": "Fix one positive ordered price vector and retain every restoration multiplier.", + "blocked_by": "Unit-price equality does not determine weighted optima." + } + ] +} diff --git a/research/dirty-echo-maximal-equality/VERIFY.json b/research/dirty-echo-maximal-equality/VERIFY.json new file mode 100644 index 0000000000..96771b0c6d --- /dev/null +++ b/research/dirty-echo-maximal-equality/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 all-arity minima, independent whole-tree equality classification, constructive witnesses and invalid-domain controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Optimized scientific replay, proof/source/receipt corruption and exclusive-write controls in an external scratch directory." + } + ] +} diff --git a/research/dirty-echo-maximal-equality/oracle.py b/research/dirty-echo-maximal-equality/oracle.py new file mode 100644 index 0000000000..13f4ad62d0 --- /dev/null +++ b/research/dirty-echo-maximal-equality/oracle.py @@ -0,0 +1,87 @@ +"""Independent bounded all-arity minima and literal ordered-tree enumeration. + +Produced by Nick Petalas. Apache-2.0. No predecessor engine is imported. +""" + +from itertools import chain, product + + +def minima(max_budget=8, max_leaves=256): + """Min-plus root composition; no equality threshold or shape rule.""" + if not 0 <= max_budget <= 8 or not 1 <= max_leaves <= 256: + raise ValueError("oracle domain") + # Each edge multiplier is at most 2**(arity-1), so any admitted tree + # costs at most max_leaves * 2**max_budget <= 65536. + infinity = 1 << 128 + rows = [[infinity] * (max_leaves + 1) for _ in range(max_budget + 1)] + transitions = 0 + for budget in range(max_budget + 1): + rows[budget][1] = 1 + for arity in range(2, budget + 2): + child = rows[budget - arity + 1] + capacity = min(max_leaves, 2 ** (budget - arity + 1)) + states = [infinity] * (max_leaves + 1) + states[0] = 0 + for position in range(arity): + multiplier = 2 if position in (0, arity - 1) else 4 + following = [infinity] * (max_leaves + 1) + for prefix in range(max_leaves + 1): + if states[prefix] == infinity: + continue + for size in range(1, min(capacity, max_leaves - prefix) + 1): + if child[size] == infinity: + continue + transitions += 1 + total = prefix + size + value = states[prefix] + multiplier * child[size] + following[total] = min(following[total], value) + states = following + for size in range(2, max_leaves + 1): + rows[budget][size] = min(rows[budget][size], states[size]) + return rows, infinity, transitions + + +def ordered_trees(max_leaves=8): + """Enumerate root cuts and Cartesian products, as postfix arity words.""" + if not 1 <= max_leaves <= 8: + raise ValueError("tree enumeration domain") + trees = [[], [(0,)]] + for size in range(2, max_leaves + 1): + current = [] + for cut_mask in range(1, 1 << (size - 1)): + cuts = [0] + [j for j in range(1, size) if cut_mask >> (j - 1) & 1] + cuts.append(size) + sizes = [right - left for left, right in zip(cuts, cuts[1:])] + for children in product(*(trees[n] for n in sizes)): + current.append(tuple(chain.from_iterable(children)) + (len(sizes),)) + if len(current) > 5000: + raise ValueError("tree capacity exceeded") + if len(set(current)) != len(current): + raise ValueError("duplicate ordered tree") + trees.append(current) + return trees + + +def resource_profile(word): + """Evaluate the literal grammar, separately from the equality classifier.""" + if not 1 <= len(word) <= 511: + raise ValueError("postfix word length") + stack = [] + for arity in word: + if type(arity) is not int or not 0 <= arity <= 256 or arity == 1: + raise ValueError("postfix arity") + if arity == 0: + stack.append((1, 1, 0)) + continue + if len(stack) < arity: + raise ValueError("postfix stack underflow") + children = stack[-arity:] + del stack[-arity:] + leaves = sum(item[0] for item in children) + calls = 2 * children[0][1] + 2 * children[-1][1] + calls += 4 * sum(item[1] for item in children[1:-1]) + scratch = arity - 1 + max(item[2] for item in children) + stack.append((leaves, calls, scratch)) + if len(stack) != 1 or stack[0][0] > 256: + raise ValueError("postfix endpoint") + return stack[0] diff --git a/research/dirty-echo-maximal-equality/test_package.py b/research/dirty-echo-maximal-equality/test_package.py new file mode 100644 index 0000000000..fdf6621ab5 --- /dev/null +++ b/research/dirty-echo-maximal-equality/test_package.py @@ -0,0 +1,114 @@ +"""Optimized standalone replay and actual subprocess corruption controls. + +Produced by Nick Petalas. Apache-2.0. All temporary outputs use TMPDIR. +""" + +import argparse +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + + +ROOT = Path(__file__).resolve().parent + + +def run(directory, *arguments): + result = subprocess.run( + [sys.executable, "-I", "-O", "-W", "error", "-B", + str(directory / "verify.py"), *arguments], + cwd=directory.parent, capture_output=True, text=True, timeout=60, check=False) + return result + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def mutations(directory): + for name in ("PROOF.md", "oracle.py", "verify.py", "test_package.py"): + target = directory / name + original = target.read_bytes() + target.write_bytes(original + b"\n# deliberate corruption\n") + try: + result = run(directory) + require(result.returncode != 0 and "receipt mismatch" in result.stderr, + "source corruption accepted: " + name) + finally: + target.write_bytes(original) + target = directory / "RESULT.json" + original = target.read_bytes() + for replacement in (b'{"status": true}', original.replace(b'"schema_version": 1', + b'"schema_version": true'), + b'{"status": 0, "status": 0}'): + target.write_bytes(replacement) + try: + require(run(directory).returncode != 0, "receipt corruption accepted") + finally: + target.write_bytes(original) + + +def behavioral_mutations(directory): + changes = [ + ("verify.py", "return (2 ** (budget + 1) + 2) // 3", + "return (3 * 2**budget + 3) // 4", "equality size"), + ("verify.py", "ends_full = arity == 2 or (", + "ends_full = arity in (2, 3) or (", "endpoint control"), + ("verify.py", "count - 2 * cap", "count - cap", "leaf invariant"), + ("oracle.py", "else 4", "else 3", "oracle lower bound"), + ] + for index, (name, old, new, reason) in enumerate(changes): + target = directory / name + original = target.read_text() + require(original.count(old) == 1, "ambiguous mutation") + target.write_text(original.replace(old, new)) + try: + # --write bypasses receipt comparison: rejection must come from + # actual scientific checks, rather than a changed source hash. + output = directory.parent / ("mutant-" + str(index) + ".json") + result = run(directory, "--write", str(output)) + require(result.returncode != 0 and reason in result.stderr, + "behavioral mutation escaped: " + name + ": " + result.stderr) + require(not output.exists(), "failed science published a receipt") + finally: + target.write_text(original) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.parse_args() + scratch = Path(os.environ.get("TMPDIR", tempfile.gettempdir())).resolve() + require(scratch.is_dir() and ROOT not in scratch.parents and scratch != ROOT, + "temporary directory must be external") + with tempfile.TemporaryDirectory(prefix="echo-controls-", dir=scratch) as temporary: + directory = Path(temporary) / "package" + directory.mkdir() + for name in ("PROOF.md", "oracle.py", "verify.py", "test_package.py", "RESULT.json"): + shutil.copyfile(ROOT / name, directory / name) + success = run(directory) + require(success.returncode == 0, success.stderr) + require("PASS_DIRTY_ECHO_MAXIMAL_EQUALITY" in success.stdout, "missing pass") + mutations(directory) + behavioral_mutations(directory) + output = Path(temporary) / "generated.json" + generated = run(directory, "--write", str(output)) + require(generated.returncode == 0, generated.stderr) + require(output.read_bytes() == (directory / "RESULT.json").read_bytes(), + "standalone generated receipt differs") + rejected = run(directory, "--write", str(output)) + require(rejected.returncode != 0 and "FileExistsError" in rejected.stderr, + "exclusive output overwritten") + require(output.read_bytes() == (directory / "RESULT.json").read_bytes(), + "rejected write changed output") + print(json.dumps(dict(status="PASS_DIRTY_ECHO_EQUALITY_CONTROLS", + source_corruptions=4, receipt_corruptions=3, + behavioral_mutations=4, standalone_optimized=True, + exclusive_output=True), sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/dirty-echo-maximal-equality/verify.py b/research/dirty-echo-maximal-equality/verify.py new file mode 100644 index 0000000000..ca5da4a77e --- /dev/null +++ b/research/dirty-echo-maximal-equality/verify.py @@ -0,0 +1,219 @@ +"""Exact finite corroboration of the all-size theorem in PROOF.md. + +Produced by Nick Petalas. Apache-2.0. Writes only an explicitly requested +exclusive receipt. All checks remain active under optimized Python. +""" + +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parent +MAX_BUDGET = 8 +MAX_LEAVES = 256 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def threshold(budget): + require(type(budget) is int and 0 <= budget <= MAX_BUDGET, "budget domain") + return (2 ** (budget + 1) + 2) // 3 + + +def construct(budget, leaves): + """Construct each equality size, with no recursive Python calls.""" + lower = threshold(budget) + require(type(leaves) is int and lower <= leaves <= 2**budget, "equality size") + pending = [(budget, leaves)] + word = [] + # At most n leaves and n-1 internal nodes, each with a finish marker. + for _ in range(3 * MAX_LEAVES): + if not pending: + break + level, count = pending.pop() + if level == -1: + word.append(count) + elif level == 0: + require(count == 1, "leaf invariant") + word.append(0) + elif count >= 2 * threshold(level - 1): + first = max(threshold(level - 1), count - 2 ** (level - 1)) + pending.extend([(-1, 2), (level - 1, count - first), (level - 1, first)]) + else: + require(level >= 2, "ternary level") + cap = 2 ** (level - 2) + pending.extend([(-1, 3), (level - 2, cap), + (level - 2, count - 2 * cap), (level - 2, cap)]) + require(not pending, "constructor work bound") + return tuple(word) + + +def equality_budgets(word): + """Recognize only the proved structural rules, without call arithmetic.""" + require(1 <= len(word) <= 511, "word length") + stack = [] + for arity in word: + require(type(arity) is int and 0 <= arity <= MAX_LEAVES and arity != 1, + "word arity") + if arity == 0: + stack.append((1, 1)) + continue + require(len(stack) >= arity, "word underflow") + children = stack[-arity:] + del stack[-arity:] + leaves = sum(item[0] for item in children) + mask = 0 + if arity in (2, 3): + for budget in range(arity - 1, MAX_BUDGET + 1): + child_budget = budget - arity + 1 + tight = all(item[1] >> child_budget & 1 for item in children) + ends_full = arity == 2 or ( + children[0][0] == children[-1][0] == 2**child_budget) + if tight and ends_full: + mask |= 1 << budget + stack.append((leaves, mask)) + require(len(stack) == 1 and stack[0][0] <= MAX_LEAVES, "word endpoint") + return stack[0][1] + + +def load_oracle(): + spec = importlib.util.spec_from_file_location("equality_oracle", ROOT / "oracle.py") + require(spec is not None and spec.loader is not None, "oracle loader") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def check_minima(oracle): + rows, infinity, transitions = oracle.minima(MAX_BUDGET, MAX_LEAVES) + equality_counts = [] + witnesses = 0 + cells = 0 + for budget in range(MAX_BUDGET + 1): + tight_sizes = [] + for leaves in range(1, MAX_LEAVES + 1): + cells += 1 + cost = rows[budget][leaves] + bound = 2 ** (budget + 1) * leaves - 4**budget + feasible = leaves <= 2**budget + require((cost != infinity) == feasible, "oracle feasibility") + if not feasible: + continue + require(cost >= bound, "oracle lower bound") + expected = threshold(budget) <= leaves + require((cost == bound) == expected, "maximal interval") + if expected: + tight_sizes.append(leaves) + word = construct(budget, leaves) + profile = oracle.resource_profile(word) + require(profile == (leaves, bound, budget), "constructed resources") + require(equality_budgets(word) == 1 << budget, "constructed structure") + witnesses += 1 + equality_counts.append(len(tight_sizes)) + return dict(cells=cells, transitions=transitions, + equality_sizes_per_budget=equality_counts, witnesses=witnesses) + + +def check_shapes(oracle): + census = oracle.ordered_trees(8) + per_size = [len(group) for group in census[1:]] + comparisons = 0 + equalities = 0 + for group in census[1:]: + for word in group: + leaves, calls, scratch = oracle.resource_profile(word) + recognized = equality_budgets(word) + for budget in range(MAX_BUDGET + 1): + actual = scratch <= budget and calls == ( + 2 ** (budget + 1) * leaves - 4**budget) + require(bool(recognized >> budget & 1) == actual, "shape equality") + comparisons += 1 + equalities += actual + require(sum(per_size) <= 6000, "enumeration capacity") + return dict(trees_per_size=per_size, trees=sum(per_size), + tree_budget_comparisons=comparisons, equality_occurrences=equalities) + + +def rejection_controls(oracle): + invalid = [(-1, 1), (9, 256), (True, 1), (0, True), (0, 0), + (1, 1), (4, 10), (4, 17), (6, 42), (8, 170)] + count = 0 + for budget, leaves in invalid: + try: + construct(budget, leaves) + except ValueError: + count += 1 + else: + raise ValueError("invalid constructor accepted") + bad_words = [(), (1,), (True,), (2,), (0, 0), (0, 0, 3)] + for word in bad_words: + for function in (equality_budgets, oracle.resource_profile): + try: + function(word) + except ValueError: + count += 1 + else: + raise ValueError("invalid word accepted") + # A ternary root with an unsaturated endpoint is not tight; a flat + # four-child root cannot be tight at any budget, despite feasibility. + unsaturated = construct(2, 3) + construct(2, 3) + construct(2, 4) + (3,) + require(equality_budgets(unsaturated) == 0, "endpoint control") + require(equality_budgets((0, 0, 0, 0, 4)) == 0, "arity-four control") + return dict(rejected_inputs=count, structural_controls=2) + + +def unique_object(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), ensure_ascii=True) + + +def receipt(): + oracle = load_oracle() + examples = [] + for budget, leaves in [(4, 11), (6, 43), (8, 171)]: + word = construct(budget, leaves) + n, calls, scratch = oracle.resource_profile(word) + examples.append(dict(budget=budget, leaves=n, calls=calls, scratch=scratch, + postfix_sha256=hashlib.sha256(bytes(word)).hexdigest())) + hashes = {} + for name in ("PROOF.md", "verify.py", "oracle.py", "test_package.py"): + hashes[name] = hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + return dict(schema_version=1, status="PASS_DIRTY_ECHO_MAXIMAL_EQUALITY", + scope="Scoped written theorem; finite exact corroboration only", + minima=check_minima(oracle), shapes=check_shapes(oracle), + controls=rejection_controls(oracle), examples=examples, + source_sha256=hashes) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="create an exclusive generated receipt") + args = parser.parse_args() + result = receipt() + if args.write is not None: + require(args.write.is_absolute(), "output must be absolute") + with args.write.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads((ROOT / "RESULT.json").read_text(), + object_pairs_hook=unique_object) + require(canonical(result) == canonical(expected), "generated receipt mismatch") + print(result["status"]) + print(canonical(result)) + + +if __name__ == "__main__": + main()