diff --git a/research/ordered-dirty-echo/CERTIFICATE.json b/research/ordered-dirty-echo/CERTIFICATE.json new file mode 100644 index 0000000000..55a3720c2a --- /dev/null +++ b/research/ordered-dirty-echo/CERTIFICATE.json @@ -0,0 +1,537 @@ +{ + "assignment_seed": 56, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "exhaustive_domain": { + "cost_alphabet": [ + 1, + 3 + ], + "cost_budget_cases": 642, + "leaf_counts": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "optimizer_shapes": 13, + "ordered_trees": 207, + "scratch_budgets": "0 through leaf_count-1" + }, + "invalid_inputs_rejected": 6, + "mutation_controls": { + "insufficient_scratch": "rejected", + "omitted_restore": "rejected", + "reversed_factor_order": "rejected", + "underpriced_middle": "rejected" + }, + "nonlinear_counterexample": { + "composed_value": 1, + "first_map": "f(x)=x", + "initial_scratch": [ + 0, + 1 + ], + "second_map": "g(x)=x^2", + "source": 1, + "target_increments": [ + 1, + 3 + ] + }, + "pr689_baselines": [ + { + "calls": 40, + "leaves": 7, + "scratch": 4 + }, + { + "calls": 160, + "leaves": 15, + "scratch": 5 + }, + { + "calls": 512, + "leaves": 27, + "scratch": 6 + }, + { + "calls": 2112, + "leaves": 56, + "scratch": 8 + } + ], + "predecessor_words": 64, + "schema_version": 1, + "source_pins": { + "local_files": [ + { + "commit": "bfff94e78f0e75ebd2593e3cc7710ae5290e8be3", + "path": "vendor/pr673_echo.py", + "sha256": "63d44c48801f51720a7cc994d6b5e2e857d1aa4fae4c6b83c0cca032b3d9e13b" + } + ], + "manifest_sha256": "e7fcc194b6f2c4fe7332b7fefc57f9b8d28b9d562ed6a6985d387de5a82e318e" + }, + "witnesses": [ + { + "budget": 6, + "calls": 464, + "costs": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "leaf_multiplicities": [ + 8, + 16, + 8, + 16, + 16, + 16, + 16, + 16, + 16, + 16, + 32, + 16, + 16, + 16, + 32, + 16, + 16, + 16, + 16, + 16, + 16, + 32, + 16, + 16, + 16, + 16, + 16 + ], + "scratch": 6, + "tree": [ + [ + [ + 0, + 1, + 2 + ], + [ + 3, + 4 + ], + [ + [ + 5, + 6 + ], + [ + 7, + 8 + ] + ] + ], + [ + [ + 9, + 10, + 11 + ], + 12, + [ + 13, + 14, + 15 + ] + ], + [ + [ + [ + 16, + 17 + ], + [ + 18, + 19 + ] + ], + [ + 20, + 21, + 22 + ], + [ + [ + 23, + 24 + ], + [ + 25, + 26 + ] + ] + ] + ], + "weighted_cost": 464, + "word_sha256": "77458872393722319c77f4f548313418b5df01f5c8c2f9f01fb6e291c4dc1ca9" + }, + { + "budget": 8, + "calls": 1600, + "costs": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "leaf_multiplicities": [ + 16, + 32, + 16, + 32, + 32, + 16, + 32, + 16, + 32, + 32, + 32, + 32, + 32, + 16, + 32, + 16, + 32, + 32, + 16, + 32, + 16, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 16, + 32, + 16, + 32, + 32, + 16, + 32, + 16, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32, + 32 + ], + "scratch": 8, + "tree": [ + [ + [ + [ + 0, + 1, + 2 + ], + [ + 3, + 4 + ], + [ + 5, + 6, + 7 + ] + ], + [ + [ + 8, + 9 + ], + 10, + [ + 11, + 12 + ] + ], + [ + [ + 13, + 14, + 15 + ], + [ + 16, + 17 + ], + [ + 18, + 19, + 20 + ] + ] + ], + [ + [ + [ + 21, + 22 + ], + 23, + [ + 24, + 25 + ] + ], + [ + 26, + 27 + ], + [ + [ + 28, + 29 + ], + 30, + [ + 31, + 32 + ] + ] + ], + [ + [ + [ + 33, + 34, + 35 + ], + [ + 36, + 37 + ], + [ + 38, + 39, + 40 + ] + ], + [ + [ + 41, + 42 + ], + 43, + [ + 44, + 45 + ] + ], + [ + [ + [ + 46, + 47 + ], + 48, + [ + 49, + 50 + ] + ], + [ + [ + 51, + 52 + ], + 53, + [ + 54, + 55 + ] + ] + ] + ] + ], + "weighted_cost": 1600, + "word_sha256": "572877d9d7ab6b4f8c5c155c047672dead156ab6bec96073578e43dfd2497eef" + }, + { + "budget": 4, + "calls": 36, + "costs": [ + 3, + 2, + 1, + 9, + 8, + 7, + 6 + ], + "leaf_multiplicities": [ + 4, + 8, + 4, + 4, + 4, + 8, + 4 + ], + "scratch": 4, + "tree": [ + [ + 0, + 1, + 2 + ], + 3, + [ + 4, + 5, + 6 + ] + ], + "weighted_cost": 180, + "word_sha256": "aed49c5b55cafe90fd2f882e228fc2cbb04c12c0c19319d03c665ae52313f28c" + }, + { + "budget": 5, + "calls": 40, + "costs": [ + 3, + 2, + 1, + 9, + 8, + 7, + 6 + ], + "leaf_multiplicities": [ + 8, + 8, + 8, + 4, + 4, + 4, + 4 + ], + "scratch": 5, + "tree": [ + [ + [ + 0, + 1 + ], + 2, + 3 + ], + 4, + [ + 5, + 6 + ] + ], + "weighted_cost": 168, + "word_sha256": "54d4e9709e6810ab746b49f2f44aae6564e0d3620d34e1556d5c29e4237d80b4" + } + ], + "word_encoding": "UTF-8 compact JSON instruction array followed by LF" +} diff --git a/research/ordered-dirty-echo/CLAIM.md b/research/ordered-dirty-echo/CLAIM.md new file mode 100644 index 0000000000..f4c5cf4c72 --- /dev/null +++ b/research/ordered-dirty-echo/CLAIM.md @@ -0,0 +1,64 @@ +# Ordered dirty echo under a scratch budget + +- Track: recursive interfaces; OS-random assignment seed **56** (`secrets.randbelow(100)`). +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Claim time: 2026-10-13 04:42 UTC; expected finish: 05:17 UTC. +- Object: the ordered multiway dirty echo from PR #673 at + `bfff94e78f0e75ebd2593e3cc7710ae5290e8be3`. +- Method: exact interval dynamic programming for ordered binary/ternary + composition trees, with arbitrary positive integer leaf costs and a hard + peak scratch-array budget. No factor permutation or new leaf operation. +- Deliverable: written complete cost recurrence, a small reproducible optimizer, + exact witnesses, and independent nonlinear restoration/linear product checks. +- Stop rule: one package; finish experimentation by 05:07 UTC and reserve the + remaining ten minutes for verification and handoff. + +No pinned coordination issue existed at the initial GitHub check. This local +claim replaces a public reservation. Open PRs were checked through #709. + +Three candidates considered: common Fourier boundary fusion (the existing +`fourier-boundary-fusion/REPORT.md` already supplies a strong obstruction), +Gaussian RHS boundary batching (#481 already supplies that construction), and +scratch-budgeted ordered dirty composition. The third was chosen because +#663 establishes the binary count and #689 optimizes balanced ternary uniform +costs, but #689 explicitly excludes unbalanced splits and unequal leaf costs. +Seed 56 selects the binary/ternary mixed-tree class (2 + 56 mod 3 = 4 is the +first scratch-budget probe); it is not used as evidence of novelty. + +The selected conditional result is +`51110230636731/31250000000000000 = 0.001635527380375392`, as bound by +`certificates/selected-result.json` to #626 and its maintainer review. +This work does not change that record or `upstream/` and does not assert a +new multiplication exponent. + +Prepared for Sagar Thakrar (@thakrarsagar), with substantial OpenAI Codex +assistance. Apache-2.0. Predecessor attribution and exact source pins will +accompany the completed result. + +## Result update — 2026-10-13 04:57 UTC + +Completed early and submitted as [PR #730](https://github.com/CrocSwap/integer-mult-bounds/pull/730). +The experiment stopped before the allotted cutoff; the final phase was devoted +to verification, overlap review and packaging. No pinned coordination issue +existed at the final check, so this is the single local result update. + +The optimum within the stated all-dirty reserved-connector tree class is +464 calls at 27 factors / six borrowed arrays and 1,600 at 56 factors / eight +borrowed arrays. The improved balanced baseline from #689 uses 512 and 2,112 +respectively. Four exact witnesses, a written optimality proof, complete +accounting and independent checks are packaged here. All 642 exhaustive +cost/budget cases, 207 tree shapes, 64 predecessor-word comparisons, four +mathematical mutations and two external package-corruption controls passed. +The selected-record check and standalone isolated replay passed. Full scope +and skipped checks are in README.md and VALIDATION.json; no new κ is claimed. + +The final pre-submission refresh covered 547 open PRs through #728. #689 +remained at `0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a`. #673 advanced to +`156f259b99723468cfdd2b5d47d0ba894f09bea7` with separate bit-role sharing +research; all three consumed source files remain unchanged from our pin. +Concurrent #714 (`efad8a40094ab453c0525efef0b0eff2a5d8b850`) uses one clean +root checkpoint with balanced binary children. Our borrowed arrays remain +arbitrary/dirty, and the entire ordered binary/ternary tree is optimized. +That clean-checkpoint result is a distinct storage contract and is not an +input to this contribution. The base and current upstream main remained +`66849e1475c930fd7732b1a0067ffee7e1e95f60` at the publication check. diff --git a/research/ordered-dirty-echo/NOTICE.md b/research/ordered-dirty-echo/NOTICE.md new file mode 100644 index 0000000000..38f2decc43 --- /dev/null +++ b/research/ordered-dirty-echo/NOTICE.md @@ -0,0 +1,41 @@ +# Attribution and license + +Prepared for **Sagar Thakrar (@thakrarsagar)** with substantial **OpenAI Codex +assistance**, including separate workers for the written proof and independent +verification. New code and documentation are Apache-2.0 under the repository's +root [LICENSE](../../LICENSE). No independent human review is claimed. + +- **androolloyd**, [PR #673](https://github.com/CrocSwap/integer-mult-bounds/pull/673): + the multiway dirty echo, its nonlinear restoration identity, recursive + instruction generator, and precision/resource argument. Its full-transform + experiment supplies the scoped negative result for a direct all-role adapter. + `vendor/pr673_echo.py` retains the exact source, including its AI disclosure. + `optimize.py` adapts that emitter to an explicit ordered tree; this package + contributes the interval optimization and its independently checked witnesses. +- **Dillon Amburgey (@dillona)**, + [PR #689](https://github.com/CrocSwap/integer-mult-bounds/pull/689): the minimum + among recursively balanced ternary splits with uniform leaf costs, and the + corrected baseline used here. The result at 15 factors is credited to #689; + this package's savings at 27 and 56 factors use a larger, explicitly scoped + tree class. No claim of priority over general alphabetic-tree optimization + algorithms is made. +- **Chafik Boukhalfa (@chafreaky)**, + [PR #628](https://github.com/CrocSwap/integer-mult-bounds/pull/628), head + `0768f97d06c623b8211e651543c66135796b62bf`: the rounded cyclic-inverse leaves, + balanced binary dirty commutator, and inherited preparation/precision + contracts. Those analytic and numerical implementations are not re-audited + or copied here. Their cited mathematical predecessors retain their credit. +- **0xkilgore**, [PR #663](https://github.com/CrocSwap/integer-mult-bounds/pull/663), + head `e0e546fd01b396478c68b6b6c5a16d87515983ba`: independent nonlinear + restoration audit and the exact count for the balanced binary dispatcher. + +[SOURCES.json](SOURCES.json) records exact source commits, SHA-256 hashes and +Git blob identifiers. The checker needs no network or pending-PR checkout. +Only the vendored echo is an executable predecessor dependency. The other +pins document comparisons, mathematical dependencies, and the selected-result +context at the base commit. + +The accepted #626 construction remains credited to Jeremy Kothe's K-triangle +construction and the complete supplier/owner-allocation lineage in the +[maintainer review](../../docs/research/community-k492-review.md). This local +interface research neither alters that construction nor establishes a new κ. diff --git a/research/ordered-dirty-echo/PROOF.md b/research/ordered-dirty-echo/PROOF.md new file mode 100644 index 0000000000..cbe77951c2 --- /dev/null +++ b/research/ordered-dirty-echo/PROOF.md @@ -0,0 +1,313 @@ +# Optimal ordered binary/ternary dirty-echo schedules + +This note proves the recurrence used by the optimizer. It extends the schedule +class of [PR673](https://github.com/CrocSwap/integer-mult-bounds/pull/673) to +arbitrary contiguous binary and ternary splits with positive integer leaf +prices and a cap on borrowed arrays. The echo identity belongs to PR673. +[PR689](https://github.com/CrocSwap/integer-mult-bounds/pull/689) optimizes +uniform call counts within recursively balanced ternary splits. Our class +also permits unbalanced splits and mixed fanout, without reordering factors. + +The result concerns local schedules. It does not supply a transform layout, +recursive multiplication profile, bit supplier, or new kappa. + +## Fixed objects and contracts + +The base commit is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The predecessor sources used here are pinned at: + +- PR673, `bfff94e78f0e75ebd2593e3cc7710ae5290e8be3`, + `research/cyclic-dirty-commutator-audit/echo.py` and `ECHO-PROOF.md`. +- PR689, `0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a`, + `research/ternary-dirty-composition/README.md` and `ternary.py`. +- PR628, `0768f97d06c623b8211e651543c66135796b62bf`, + `research/prime-power-cyclic-scan/DIRTY-PROOF.md`, as inherited and credited + by PR673. Its leaf bounds remain conditional on its stated hypotheses. +- The integration obstruction is in + `research/dirty-echo-integration/PROOF.md` at the same pinned PR673 commit. + +Let `A_0,...,A_(n-1)` be composable linear maps on equal-length arrays. +Their order is fixed. A leaf for index `i` implements the additive action +`y += A_i x` in exact arithmetic. A schedule tree partitions the interval +`[0,n)` into consecutive nonempty child intervals. Each internal node has +two or three children. Thus a subtree for `[i,j)` implements +`y += A_(j-1) ... A_i x`. + +For rounded execution, replace a leaf map by a deterministic increment +`f_i(x)` that is independent of its target. A valid leaf restores its source +exactly and its negative subtracts exactly the same represented increment. +All internal arithmetic, accesses and temporary work required to satisfy this +contract belong to the leaf's price. Fixed descriptors and phase data must +remain unchanged and cannot alias any mutable data. Every source, target and +borrowed array used by the schedule is distinct. Arbitrary overlapping views +and hidden stateful callbacks are outside this contract. + +At a node with `k` children, reserve `k-1` connector arrays for the node's +whole execution. Every child uses a deeper borrowed pool disjoint from all +ancestor sources, targets and connector arrays. The deeper pool is reused +between calls because each child restores it. This is PR673's allocation +discipline. The claimed optimum is within this discipline; it is not an +optimum over schedules that reuse ancestor storage according to lifetimes. + +## Exact linear identity and nonlinear restoration + +Write the child maps in order as `B_1,...,B_k` and the connector arrays as +`z_1,...,z_(k-1)`. Let `C` be the sequence + +```text +z_1 += B_1 x +z_2 += B_2 z_1 +... +z_(k-1) += B_(k-1) z_(k-2). +``` + +Let `D` omit the first update of `C`. The node executes + +```text +C; y += B_k z_(k-1); inverse(C); +D; y -= B_k z_(k-1); inverse(D). +``` + +Here inverse means reverse the sequence and invert each operation. Merely +changing signs in the original order is not the specified inverse. + +Both ladders restore all connectors. Compare their forward states starting +from the same initial dirt. At `z_1` their difference is `B_1 x`. By linearity, +at `z_i` the difference is `B_i ... B_1 x`. The two target updates therefore +sum to `B_k ... B_1 x`. This argument uses no commutativity. Applying it +inductively to consecutive factor intervals proves the advertised ordered +product for every tree in the class. + +Restoration requires less than linearity. Suppose by induction each child +adds a deterministic function of its source and initial deeper dirt, +independently of its target, and restores its source and deeper dirt. Every +inverse ladder call sees the same source and deeper dirt as its forward mate: +later ladder calls have already been undone, and the intervening update to +`y` cannot affect a ladder source or its scratch. Hence all connectors and +deeper scratch are restored exactly. The root source never changes after a +completed child call. Each node is itself a target-independent additive +operation with an exact inverse, closing the induction. + +For example, write the nonlinear child increments as `f,g,h`, with their +restored deeper dirt suppressed from notation. The binary output increment is + +```text +g(z + f(x)) - g(z). +``` + +The ternary output increment is + +```text +h(z_2 + g(z_1 + f(x))) - h(z_2 + g(z_1)). +``` + +These formulas explain both exact restoration and the possible dependence of +the output on initial dirt. They are generally not the nonlinear composition +`g(f(x))` or `h(g(f(x)))`. For a scalar negative control, `f(x)=x`, `g(z)=z*z`, +`x=1`, and `z=1` give binary increment `3`, whereas `g(f(x))=1`. +The linear product proof must not be applied to rounded nonlinear increments. + +The restoration statement assumes valid leaf inputs throughout execution. +It does not promise transactional rollback after invalid coefficients, +arithmetic overflow, an exception, or a stateful callback. + +## Complete local accounting + +Let `c_i` be the positive integer price of one signed leaf invocation at a +fixed common arithmetic precision and layout. It must be an exact price or +a charged upper bound valid for both signs and every occurrence, including +the permitted transient source values and array roles. The optimizer does +not model prices that change with a leaf's calling context. The two endpoint +children occur twice in the node word; every interior child occurs four +times. In particular, for weighted +price `W`, unweighted leaf count `N`, and borrowed-array count `S`, + +```text +W(leaf i) = c_i, N(leaf i) = 1, S(leaf i) = 0 +W(binary) = 2 W(left) + 2 W(right) +W(ternary) = 2 W(left) + 4 W(middle) + 2 W(right) +S(binary) = 1 + max(S(left), S(right)) +S(ternary) = 2 + max(S(left), S(middle), S(right)). +``` + +The same recurrences for `W` with every `c_i=1` give `N`. Equivalently, a leaf's +multiplicity is the product of the factors `2` or `4` on its root-to-leaf path, +and `W` is the sum of multiplicity times price. The scratch formulas are exact +for the stated reserved-connector allocator, since child calls run serially +and restore the deeper pool. For length `L`, the schedule borrows `L*S` data +words, in addition to source and target, for `S+2` total array roles. These +words may contain arbitrary dirt. No zero initialization, hidden copy or +additional clean length-`L` array is part of this schedule. + +Every repetition, including a call inside an inverse ladder, is charged. +The leaf price must cover its forward pass, output pass, source undo, +validation, coefficient/phase accesses and the arithmetic needed for exact +represented subtraction. Routing or frame changes may be included in these +prices only when the same bound applies to every occurrence and context. +Otherwise their costs remain additional explicit terms. Preparation is also +additional unless it is already included. A complete local bill has the form + +```text +preparation + sum_i multiplicity_i * charged_leaf_price_i + + remaining_routing_and_frame_work + schedule_dispatch. +``` + +The selected schedule tree occupies `O(n)` descriptor records. The iterative +emitter streams its instruction word with `O(N)` dispatch operations. To see +this, expand each invoked binary node into its four child calls and each +invoked ternary node into its eight child calls. The resulting execution tree +has `N` leaves and at most `(N-1)/3` internal nodes, each handled by a constant +number of record operations. + +The pending stack executes this tree in depth-first order. At most seven +unvisited sibling calls remain for each ancestor of the current call. With +`h` internal ancestors its size is at most `1+7h`. Each such ancestor reserves +at least one connector, so `h<=S` and the live stack uses `O(S+1)` records. +The small command lists for the currently expanded node have at most eight +entries. The leaf's own clean scalar workspace, factor descriptor storage +and arithmetic workspace remain additional resources. The `O(n)` selected +tree and `O(S+1)` live stack are separate storage charges. + +The optimizer minimizes the displayed weighted leaf bill. It cannot infer +prices for an unimplemented source-access mechanism, assume a free phase +table, or omit restoration performed inside a leaf. + +## Dynamic programming optimum at each scratch budget + +Let `F(i,j,b)` be the minimum weighted leaf bill for `[i,j)` with at most `b` +borrowed arrays in this allocation discipline. Infeasible values are infinity. +The base cases are `F(i,i+1,b)=c_i` for `b>=0`; every state with `b<0` is +infeasible. For intervals with at least two factors, + +```text +F(i,j,b) = min of + + 2 F(i,m,b-1) + 2 F(m,j,b-1) for i < m < j, + + 2 F(i,m,b-2) + 4 F(m,l,b-2) + 2 F(l,j,b-2) for i < m < l < j. +``` + +Any legal nonleaf schedule has a binary or ternary root and one of the listed +contiguous partitions. Its child budgets are at most `b-(k-1)`, so induction +on interval length bounds its cost below by the corresponding displayed sum. +Conversely, concatenate child minimizers for any finite displayed sum using +the node word. They restore the common deeper pool and use at most `b` arrays, +so the sum is attainable. Taking the minimum proves both completeness and +optimality. Every child is shorter than its parent, and the number of trees +is finite; there is no search cutoff in this recurrence. Ties may choose any +attaining tree without changing the proof. + +The offline optimizer has at most `O((b+1)*n^2)` interval-budget states. +Each state considers `O(n)` binary cuts and `O(n^2)` ternary cut pairs, using +a constant number of cached-state accesses and integer arithmetic/comparison +operations per choice. Thus planning takes `O((b+1)*n^4)` such operations and +stores `O((b+1)*n^2)` states. For `b>=1` these are `O(b*n^4)` operations and +`O(b*n^2)` states. Each retained state stores a price and at most three +references to child trees, so it does not copy a full tree per state. These +are operation and record counts; integer bit complexity and the implementation +cost of memo-table accesses remain additional. Arbitrarily large prices are +not treated as constant-bit integers. + +Planning is separate from executing the selected schedule. The complete cost +of finding and running a schedule is this planning cost plus the local bill +above, including preparation, routing/frame work and dispatch. Reusing a +previously computed tree can amortize planning only when that reuse is part +of the application. The call-count improvements alone do not establish an +end-to-end runtime improvement after planning is charged. + +Useful invariants are independent of the objective values: + +- `F(i,j,b)` is nonincreasing in `b`. +- A nonempty interval of length `n` is feasible exactly when `n<=2^b`. + Inductively a node with `k` children holds at most + `k*2^(b-(k-1))<=2^b` leaves for `k` equal to `2` or `3`. Recursively balanced + binary splits attain scratch `ceil(log2 n)`. +- Every tree uses at most `n-1` connector arrays along a path. Each node on + that path contributes `k-1` off-path child subtrees, each containing at least + one distinct leaf. Thus budgets above `n-1` cannot improve the optimum. + +This is an exact finite-class optimization theorem. A finite executable replay +checks an implementation of the recurrence and generated words; it is not a +formal proof of a multiplication theorem or an optimality claim outside this +class. + +## Finite witnesses + +The implemented recurrence and the pinned PR689 resource function give these +uniform-price results. Every row uses the same scratch cap for both schedules. + +| Factors | Borrowed arrays | Total roles | PR689 balanced calls | Optimized calls | +|---|---:|---:|---:|---:| +| 27 | 6 | 8 | 512 | 464 | +| 56 | 8 | 10 | 2112 | 1600 | + +The 27-factor witness has a root partition into `9,7,11` consecutive factors. +It lies outside recursively balanced ternary splitting, so the improvement +does not repeat PR689's placement optimization. The corresponding pinned +PR673 counts are `512` and `2144`; the table uses the stronger balanced +predecessor. These are local leaf counts, not completed outputs on every role. + +For the fixed ordered prices `(3,2,1,9,8,7,6)`, scratch cap `4` yields weighted +price `180` with `36` leaf calls. Cap `5` yields weighted price `168` with `40` +leaf calls. This example separates the weighted objective from invocation +count and motivates reporting both. The weights are an abstract scheduling +fixture, not measured supplier costs. + +## Precision and the inherited integration obstruction + +Weighted prices must be fixed before optimization. If two trees have different +leaf counts, minimizing their weighted prices at one precision need not +minimize their total bit complexity after precision is increased separately. +Report `N`, `W` and `S` separately and reprice any selected implementation at +its required precision. + +For the pinned PR628 leaves, retain all PR673 hypotheses and notation: +`n=r-1`, `0= p+1 + ceil(log2(N*a*(D+1))) + (N-1)*ceil(log2(G)), +``` + +together with the two leaf precision conditions. Coefficient and phase +preparation errors retain their separate inherited budget and source-norm +scaling. The schedule changes `N`; it does not remove those conditions. + +The earlier all-role integration rejection also survives these splits. +For every tree with `n>=2`, `N>=4n-4`. First, induction gives `N>=2n-1` for +every subtree: every child is invoked at least twice and the root has at most +`n` children. More explicitly, summing `2(2n_i-1)` gives `4n-2k>=2n` at an +internal node, and the leaf case is equality. At the root, each endpoint +therefore contributes at least `4n_i-2`; each interior contributes at least +`4n_i`, using `N_i>=n_i`. Summing gives `4n-4`. + +In the pinned three-shear all-role adapter, even granting one recursive child +per additive leaf and making every wrapper free gives the moment +`Phi(b)=3N/(2*n^(1-b))`. At `b=0`, it is at least `6-6/n>=3`; it increases for +`b>=0`. Thus the same optimistic admission test rejects every positive-saving +profile obtained solely by this adapter. This is a scoped negative result for +that integration, not a lower bound for arbitrary suppliers. Neither smaller +local counts nor an unequal leaf-price witness is a new kappa certificate. + +## Attribution + +The multiway echo identity, restored-input interface and local error budget +are credited to PR673 and its author, androolloyd, building on Chafik Boukhalfa's +PR628 rounded leaf and Ali Romman's PR621 kernel. PR689 supplies the balanced +ternary comparison and explicitly leaves unbalanced splits and unequal leaf +prices open. Their notices and the repository's Apache-2.0 terms apply to +their work. This note and its accompanying optimizer were prepared with +substantial OpenAI Codex assistance; contributor details are in the claim. diff --git a/research/ordered-dirty-echo/README.md b/research/ordered-dirty-echo/README.md new file mode 100644 index 0000000000..ed1966e00d --- /dev/null +++ b/research/ordered-dirty-echo/README.md @@ -0,0 +1,114 @@ +# Fewer dirty-echo calls at a fixed scratch budget + +**Recursive-interface research / finite construction refinement; no new κ.** + +An exact ordered-tree optimizer reduces the complete dirty-echo call count +from **512 to 464** for 27 factors with six borrowed arrays, and from +**2,112 to 1,600** for 56 factors with eight borrowed arrays. Both comparisons +use Dillon Amburgey's improved balanced ternary schedule in +[PR #689](https://github.com/CrocSwap/integer-mult-bounds/pull/689). +Every inverse and restoration call is included. The factor order is unchanged. +These are operation counts, not measured runtime improvements. +The factor counts are generic interface fixtures, not asserted prime-power +cyclic-inversion parameters for the inherited PR628 implementation. + +The mechanism is androolloyd's +[PR #673](https://github.com/CrocSwap/integer-mult-bounds/pull/673) dirty echo. +Its first and last children execute twice, while the middle child executes +four times. Allowing unbalanced contiguous splits and mixed binary/ternary +nodes reduces repeated work. At 27 factors the chosen root split is +`9,7,11`, outside #689's recursively balanced class. The 15-factor result +of 160 calls already belongs to #689 and is retained as a comparison control. + +## Reproduce + +From the repository root, with Python 3.10+ and its standard library: + +```sh +python3 -I -O -B research/ordered-dirty-echo/verify.py +``` + +Expected: `PASS_ORDERED_DIRTY_ECHO`, with the exact coverage counts described +below. The command authenticates the vendored predecessor, recomputes all +fields of [CERTIFICATE.json](CERTIFICATE.json), and compares the complete +result. No network, optional library, pending-PR checkout, or generated cache +is needed. The checks remain active under optimized Python. + +[VALIDATION.json](VALIDATION.json) records the local environment, isolated +package replay, selected-record check, and two additional certificate/source +corruption checks. It distinguishes these runs from checks not performed. + +The certificate contains each selected tree, ordered prices, scratch budget, +actual reserved scratch, weighted cost, leaf count, per-factor multiplicity, +and a hash of the complete emitted instruction word. `--emit` prints the +recomputed certificate for inspection; it does not overwrite the frozen file. + +## What is optimized + +For fixed positive integer leaf prices and a cap on borrowed arrays, +[optimize.py](optimize.py) finds the minimum charged leaf cost over every +ordered binary/ternary tree. Each node reserves all its connectors throughout +its child calls. Children share a deeper scratch pool because they restore it. +This is the predecessor's allocation discipline. Ancestor-storage reuse, +factor permutations, fanout above three, and different echo words are outside +the optimization class. + +The [written proof](PROOF.md) gives the complete recurrence, exact linear +product, nonlinear restoration contract, execution/preparation/precision +charges, and proof of the dynamic program's optimum within this class. +Source and target add two further array roles: the two uniform witnesses +have eight and ten total roles respectively. + +Unequal prices are supported at a **fixed common precision and layout**. The +seed-derived abstract prices `(3,2,1,9,8,7,6)` have minimum weighted cost +180 with four borrowed arrays and 168 with five. Their call counts are 36 +and 40 respectively, so a weighted reduction need not reduce calls or the +precision needed by a concrete implementation. These prices are a scheduling +fixture, not measured supplier costs. + +## Verification and completed coverage + +- Exhaustive comparison against a separate postfix-tree enumerator covers + every cost vector in `{1,3}^n`, for `1 <= n <= 6` and every scratch budget + `0 <= b <= n-1`: **642 cost/budget cases and 207 ordered tree shapes**. + A separate path-based calculation checks cost and scratch use. +- Exact free noncommutative expressions check the ordered linear product and + cancellation of every dirty input for all 207 trees and all four larger + witnesses, in both signs. This does not assume the factors commute. +- Exact nonlinear integer maps test source/scratch restoration and inverse + execution for two dirty inputs per tree and witness. A concrete nonlinear + example confirms that restored dirt can still affect the output increment. +- Omitted restoration, reversed factor order, an undercharged middle child, + and insufficient scratch must each fail for the intended reason. +- The emitted words for the predecessor's balanced trees are compared with + its unchanged, source-pinned generator. The certificate also retains #689's + corrected balanced counts. + +The proof establishes the recurrence for the stated finite-tree class. The +executable coverage is bounded; it is not a formal verification of the +multiplication theorem. No random candidate search or early search cutoff is +used. The assignment seed is 56; it selects the 56-factor probe and the +unequal-price fixture `c_i = 1 + ((56 + 17*i) mod 9)`, `0 <= i < 7`. + +## Scope and handoff + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +[SOURCES.json](SOURCES.json) pins the actual #673 and #689 sources, and +[NOTICE.md](NOTICE.md) preserves attribution and substantial AI-assistance +disclosure. The [local sprint claim](CLAIM.md) records the three candidate +tasks, overlap review, stopping rule, and result. + +At that base, the selected result is the reviewed #626 composition with +κ = `51110230636731/31250000000000000`. Its certificate, actual K492 owner +construction, and maintainer review were followed before selecting this task. +This package changes only its own research directory. + +The local echo still needs an admitted all-role supplier, physical layout, +source/phase access, routing, coefficient preparation, rounding and exact +recovery before it can contribute to a multiplication bound. The pinned +three-shear direct adapter has optimistic moment at least `6-6/n >= 3` for +`n >= 2`, even after these optimizations; it fails the required contraction. +The proof explains why. The selected construction's compiler, common-label, +mutable-basis, hosting, residual, precision, tape and analytic assumptions +remain inherited. No selected cold replay, full repository suite, Lean proof, +remote CI, or practical performance benchmark is claimed for this package. diff --git a/research/ordered-dirty-echo/SOURCES.json b/research/ordered-dirty-echo/SOURCES.json new file mode 100644 index 0000000000..7b5331a114 --- /dev/null +++ b/research/ordered-dirty-echo/SOURCES.json @@ -0,0 +1,54 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 56, + "selected_result": { + "path": "certificates/selected-result.json", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "kappa": "51110230636731/31250000000000000", + "source_head": "660de893d27bb7abd1d5b01b1640207528a5c851" + }, + "predecessors": [ + { + "pr": 673, + "commit": "bfff94e78f0e75ebd2593e3cc7710ae5290e8be3", + "contributor": "androolloyd", + "role": "ordered multiway echo and full-transform cost boundary", + "files": [ + { + "path": "research/cyclic-dirty-commutator-audit/echo.py", + "sha256": "63d44c48801f51720a7cc994d6b5e2e857d1aa4fae4c6b83c0cca032b3d9e13b", + "git_blob": "76a31171368eb945815cc00dce931c6c7a88e836", + "local_copy": "vendor/pr673_echo.py" + }, + { + "path": "research/cyclic-dirty-commutator-audit/ECHO-PROOF.md", + "sha256": "e98e459720d8013618853bb4836558cf8bb06a4a1be03fe0954a76f178ecf403", + "git_blob": "23bf89c55e5c4dd82b674d9269dedee34d77510b" + }, + { + "path": "research/dirty-echo-integration/PROOF.md", + "sha256": "f25eb16d70f499091908107c5a314e2dab2fb71e956fe6150d7a188f1b90e517", + "git_blob": "9540138bf39d5050bfb3e371640fe752c876523c" + } + ] + }, + { + "pr": 689, + "commit": "0dedef12f05f9a06faf9d4e1c8b1462c0e3bff3a", + "contributor": "Dillon Amburgey / dillona", + "role": "balanced ternary comparison", + "files": [ + { + "path": "research/ternary-dirty-composition/ternary.py", + "sha256": "aea6122da02900da3362f888f9237362a1ec6800345d5205d3ef79e6fa4a731c", + "git_blob": "a8c2eb5775777c76c88f335d1e6e55ed3a9862c3" + }, + { + "path": "research/ternary-dirty-composition/README.md", + "sha256": "d316d01169e44a1879aab4eba9aec6ef63eaf6bad2cb70fddadb06a183946bbf", + "git_blob": "cc58c0a9e3c07c1c0515036b999c0bb56abce059" + } + ] + } + ] +} diff --git a/research/ordered-dirty-echo/VALIDATION.json b/research/ordered-dirty-echo/VALIDATION.json new file mode 100644 index 0000000000..d182fdf1dc --- /dev/null +++ b/research/ordered-dirty-echo/VALIDATION.json @@ -0,0 +1,61 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "date_utc": "2026-10-13", + "environment": { + "platform": "macOS 26.5.2 arm64", + "python": "3.14.8", + "dependencies": "Python standard library only" + }, + "checks": [ + { + "command": "python3 -I -O -B research/ordered-dirty-echo/verify.py", + "exit_code": 0, + "result": "PASS_ORDERED_DIRTY_ECHO: 642 exhaustive cases; 207 ordered trees; 64 pinned predecessor words; 4 witnesses; 4 rejected mutations" + }, + { + "command": "python3 -I -B research/ordered-dirty-echo/verify.py", + "exit_code": 0, + "result": "Complete certificate matches under ordinary and optimized Python" + }, + { + "command": "python3 -I -O -B /tmp/ordered-dirty-echo-seed56-portable/verify.py", + "exit_code": 0, + "result": "Standalone package copy passes from /tmp using only its own files and the standard library" + }, + { + "command": "make selected-record-check", + "exit_code": 0, + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000" + }, + { + "command": "git diff --cached --check", + "exit_code": 0, + "result": "No whitespace errors" + } + ], + "external_negative_controls": [ + { + "mutation": "Replace certificate schema_version integer 1 with boolean true in the standalone copy", + "result": "Nonzero exit: certificate differs from complete replay" + }, + { + "mutation": "Change the vendored predecessor docstring in the standalone copy", + "result": "Nonzero exit before import: predecessor source pin" + } + ], + "dependency_refresh": { + "pr673_observed_head": "156f259b99723468cfdd2b5d47d0ba894f09bea7", + "pinned_head": "bfff94e78f0e75ebd2593e3cc7710ae5290e8be3", + "consumed_source_diff": "empty for echo.py, ECHO-PROOF.md and dirty-echo-integration/PROOF.md", + "new_work": "Separate bit-role-sharing-budget research; no ordered-tree optimization overlap" + }, + "not_run": [ + "full repository suite", + "selected frontier cold replay", + "remote CI", + "Lean or other formal proof checker", + "PR628 rounded leaf numerical replay", + "practical runtime benchmark" + ], + "scope": "Exact finite scheduling evidence plus a written finite-class optimum proof; no new kappa or full multiplication theorem" +} diff --git a/research/ordered-dirty-echo/optimize.py b/research/ordered-dirty-echo/optimize.py new file mode 100644 index 0000000000..d48f14658f --- /dev/null +++ b/research/ordered-dirty-echo/optimize.py @@ -0,0 +1,86 @@ +"""Exact ordered binary/ternary dirty-echo trees at a fixed scratch budget. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +Apache-2.0. The instruction emitter adapts androolloyd's PR673 echo.py; +see NOTICE.md and vendor/pr673_echo.py for its unchanged source. +""" + +from functools import lru_cache + + +def optimize(costs, budget): + """Return (minimum charged cost, tree); raise ValueError if infeasible. + + Prices cover complete leaf calls at one common precision. A tree is a + factor index or a tuple of two/three children, in original factor order. + All connector arrays remain reserved during every descendant call. + """ + costs = tuple(costs) + if not costs or any(type(c) is not int or c <= 0 for c in costs): + raise ValueError("positive integer leaf costs required") + if type(budget) is not int or budget < 0: + raise ValueError("nonnegative integer scratch budget required") + + @lru_cache(None) + def solve(lo, hi, available): + if hi - lo == 1: + return costs[lo], lo + if available < 1: + return None + best = None + for mid in range(lo + 1, hi): + left = solve(lo, mid, available - 1) + right = solve(mid, hi, available - 1) + if left is not None and right is not None: + charge = 2 * (left[0] + right[0]) + if best is None or charge < best[0]: + best = charge, (left[1], right[1]) + if available >= 2: + for first in range(lo + 1, hi - 1): + left = solve(lo, first, available - 2) + if left is None: + continue + for second in range(first + 1, hi): + middle = solve(first, second, available - 2) + right = solve(second, hi, available - 2) + if middle is not None and right is not None: + charge = 2 * left[0] + 4 * middle[0] + 2 * right[0] + if best is None or charge < best[0]: + best = charge, (left[1], middle[1], right[1]) + return best + + result = solve(0, len(costs), budget) + if result is None: + raise ValueError("scratch budget cannot hold an ordered echo tree") + return result + + +def resources(tree, costs): + """Return actual peak reserved scratch and the complete leaf charge.""" + if isinstance(tree, int): + return 0, costs[tree] + children = [resources(child, costs) for child in tree] + scratch = len(tree) - 1 + max(depth for depth, _ in children) + charge = sum((2 if i in (0, len(tree) - 1) else 4) * cost + for i, (_, cost) in enumerate(children)) + return scratch, charge + + +def instructions(tree, src=0, dst=1, scratch_first=2, sign=1): + """Emit the PR673 echo, or its reverse inverse, for an optimized tree.""" + pending = [(tree, src, dst, scratch_first, sign)] + while pending: + node, source, target, first, direction = pending.pop() + if isinstance(node, int): + yield source, target, node, direction + continue + k = len(node) + chain = [(node[i], source if i == 0 else first + i - 1, + first + i, 1) for i in range(k - 1)] + last = (node[-1], first + k - 2, target, 1) + invert = lambda commands: [(t, s, d, -q) for t, s, d, q in reversed(commands)] + commands = chain + [last] + invert(chain) + chain[1:] + invert([last]) + invert(chain[1:]) + if direction == -1: + commands = invert(commands) + pending.extend((child, s, d, first + k - 1, q) + for child, s, d, q in reversed(commands)) diff --git a/research/ordered-dirty-echo/vendor/pr673_echo.py b/research/ordered-dirty-echo/vendor/pr673_echo.py new file mode 100644 index 0000000000..76a3117136 --- /dev/null +++ b/research/ordered-dirty-echo/vendor/pr673_echo.py @@ -0,0 +1,75 @@ +"""Multiway dirty echo composition of PR628's restored-input leaf shears. + +Prepared for androolloyd with substantial OpenAI Codex assistance. Apache-2.0. +No new multiplication exponent is asserted. Read ECHO-PROOF.md for the storage +tradeoff and the complete inherited local error recurrence. +""" + + +def partition(count, fanout): + if count < 1 or fanout < 2: + raise ValueError('positive factor count and fanout >= 2 required') + k = min(count, fanout) + quotient, remainder = divmod(count, k) + return [quotient + (i < remainder) for i in range(k)] + + +def resources(count, fanout): + if count < 1 or fanout < 2: + raise ValueError('positive factor count and fanout >= 2 required') + if count == 1: + return 0, 1 + sizes = partition(count, fanout) + children = [resources(n, fanout) for n in sizes] + scratch = len(sizes)-1 + max(depth for depth, _ in children) + calls = sum((2 if i in (0, len(sizes)-1) else 4)*cost + for i, (_, cost) in enumerate(children)) + return scratch, calls + + +def instructions(first, count, src, dst, scratch_first, fanout, sign=1): + """Stream the exact instruction word or its reverse inverse.""" + if count == 1: + yield src, dst, first, sign + return + sizes = partition(count, fanout) + k = len(sizes) + offsets = [first] + for size in sizes[:-1]: + offsets.append(offsets[-1]+size) + # C: populate the whole dirty chain. D: the same chain without its first link. + chain = [(offsets[i], sizes[i], src if i == 0 else scratch_first+i-1, + scratch_first+i, 1) for i in range(k-1)] + last = (offsets[-1], sizes[-1], scratch_first+k-2, dst, 1) + invert = lambda commands: [(a,n,s,t,-q) for a,n,s,t,q in reversed(commands)] + commands = chain + [last] + invert(chain) + chain[1:] + invert([last]) + invert(chain[1:]) + if sign == -1: + commands = invert(commands) + for a,n,s,t,q in commands: + yield from instructions(a,n,s,t,scratch_first+k-1,fanout,q) + + +def compose(leaf_module, x, y, factors, scratch, phases, beta, bits, direction, + sign=1, fanout=8): + """Apply the dirty echo using a pinned PR628 leaf, restoring x and scratch.""" + if direction not in (-1,1) or sign not in (-1,1): + raise ValueError('orientation and sign') + depth, count = resources(len(factors), fanout) + arrays = [x,y]+scratch + if len(scratch) < depth: + raise ValueError('dirty depth') + if len({id(a) for a in arrays}) != len(arrays): + raise ValueError('all ancestor arrays distinct') + if any(phases is a for a in arrays): + raise ValueError('phase array aliases mutable data') + if not x or any(len(a) != len(x) for a in arrays) or len(phases) != len(x): + raise ValueError('array lengths') + if any(a*a+b*b != 1 for a,b in phases): + raise ValueError('unit phases') + stats = dict(leaves=0,scalar_steps=0) + for src,dst,index,q in instructions(0,len(factors),0,1,2,fanout,sign): + leaf_module.leaf(arrays[src],arrays[dst],factors[index],phases,beta,bits, + direction,q,stats) + if stats['leaves'] != count: + raise ValueError('leaf accounting') + return stats diff --git a/research/ordered-dirty-echo/verify.py b/research/ordered-dirty-echo/verify.py new file mode 100644 index 0000000000..9d0e3f51cb --- /dev/null +++ b/research/ordered-dirty-echo/verify.py @@ -0,0 +1,369 @@ +"""Independent finite checks for ordered mixed-arity dirty echoes. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +Apache-2.0. These finite checks are not a proof of the multiplication theorem. +Run with Python normally or with -O; no check uses an assert statement. +""" + +import argparse +from collections import Counter +from functools import lru_cache +import hashlib +import importlib.util +from itertools import product +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +from optimize import instructions, optimize, resources + + +def check(condition, message): + if not condition: + raise AssertionError(message) + + +@lru_cache(None) +def all_trees(count): + """Enumerate postfix leaf/binary/ternary words by stack reduction.""" + found = [] + + def visit(next_leaf, stack): + if next_leaf == count and len(stack) == 1: + found.append(stack[0]) + return + if next_leaf < count: + visit(next_leaf + 1, stack + (next_leaf,)) + for arity in (2, 3): + if len(stack) >= arity: + visit(next_leaf, stack[:-arity] + (stack[-arity:],)) + + visit(0, ()) + check(len(found) == len(set(found)), "duplicate exhaustive tree") + return tuple(found) + + +def oracle_resources(tree, costs): + """Price each root-to-leaf path; do not call the production recurrence.""" + pending = [(tree, 0, 1)] + scratch = weighted = 0 + leaves = [] + while pending: + node, occupied, multiplicity = pending.pop() + if isinstance(node, int): + scratch = max(scratch, occupied) + weighted += multiplicity * costs[node] + leaves.append(node) + continue + arity = len(node) + for position in range(arity - 1, -1, -1): + copies = 2 if position in (0, arity - 1) else 4 + pending.append((node[position], occupied + arity - 1, + multiplicity * copies)) + check(leaves == list(range(len(costs))), "factor order or coverage") + return scratch, weighted + + +@lru_cache(None) +def leaf_counts(tree): + return Counter(index for _, _, index, _ in instructions(tree)) + + +def run_formal(word, register_count): + """Exact free-algebra expressions: (operator word, initial register).""" + registers = [{((), origin): 1} for origin in range(register_count)] + for source, target, factor, sign in word: + check(source != target, "aliased source and destination") + check(sign in (-1, 1), "invalid instruction sign") + for (prefix, origin), coefficient in registers[source].items(): + term = ((factor,) + prefix, origin) + registers[target][term] = registers[target].get(term, 0) + sign * coefficient + registers[target] = {term: value for term, value in registers[target].items() + if value} + return registers + + +def validate_word(tree, costs, budget, word=None, claimed_cost=None, sign=1): + if word is None: + word = tuple(instructions(tree, sign=sign)) + else: + word = tuple(word) + check(word, "empty instruction word") + largest = max(max(source, target) for source, target, _, _ in word) + check(largest < budget + 2, "insufficient scratch") + measured_cost = sum(costs[factor] for _, _, factor, _ in word) + if claimed_cost is not None: + check(measured_cost == claimed_cost, "weighted leaf price") + registers = run_formal(word, budget + 2) + expected = [{((), origin): 1} for origin in range(budget + 2)] + expected[1][(tuple(range(len(costs) - 1, -1, -1)), 0)] = sign + check(registers == expected, "ordered product and dirty restoration") + + +def nonlinear_restore(tree, budget): + """Exact nonlinear integer maps with bounded values, not rounded floats.""" + word = tuple(instructions(tree)) + inverse = tuple(instructions(tree, sign=-1)) + check(inverse == tuple((s, t, i, -q) for s, t, i, q in reversed(word)), + "reverse-inverse instruction word") + for offset in (0, 7): + initial = [(-1) ** i * (3 * i + offset + 2) for i in range(budget + 2)] + registers = initial[:] + for source, target, factor, sign in word: + value = registers[source] % 17 + nonlinear = (value * value + (factor + 2) * value + factor) % 17 - 8 + registers[target] += sign * nonlinear + check(registers[0] == initial[0] and registers[2:] == initial[2:], + "nonlinear dirty restoration") + for source, target, factor, sign in inverse: + value = registers[source] % 17 + nonlinear = (value * value + (factor + 2) * value + factor) % 17 - 8 + registers[target] += sign * nonlinear + check(registers == initial, "nonlinear reverse-inverse restoration") + + +def rejected(call, expected_message): + try: + call() + except AssertionError as error: + check(expected_message in str(error), "mutation failed for the wrong reason") + else: + raise AssertionError("mutation was accepted: " + expected_message) + + +def exhaustive_check(): + cases = 0 + checked_trees = set() + counts = [] + for count in range(1, 7): + trees = all_trees(count) + counts.append(len(trees)) + for costs in product((1, 3), repeat=count): + priced = [(oracle_resources(tree, costs), tree) for tree in trees] + for budget in range(count): + feasible = [(price, tree) for (scratch, price), tree in priced + if scratch <= budget] + try: + actual, tree = optimize(costs, budget) + except ValueError: + check(not feasible, "optimizer rejected a feasible domain") + else: + check(feasible, "optimizer accepted an infeasible domain") + check(actual == min(price for price, _ in feasible), + "optimizer differs from exhaustive minimum") + scratch, oracle_price = oracle_resources(tree, costs) + check((scratch, actual) == resources(tree, costs), + "production resource accounting") + check(actual == oracle_price and scratch <= budget, + "optimizer witness resources") + check(actual == sum(costs[i] * n for i, n in leaf_counts(tree).items()), + "weighted instruction accounting") + checked_trees.add(tree) + cases += 1 + # Check every enumerated shape, including shapes the optimizer never chooses. + for tree in trees: + costs = (1,) * count + scratch, price = oracle_resources(tree, costs) + validate_word(tree, costs, scratch, claimed_cost=price) + validate_word(tree, costs, scratch, claimed_cost=price, sign=-1) + nonlinear_restore(tree, scratch) + check(counts == [1, 1, 3, 10, 38, 154], "exhaustive tree counts") + return cases, sum(counts), len(checked_trees) + + +def witness_check(): + weighted = (3, 2, 1, 9, 8, 7, 6) + cases = (((1,) * 27, 6, 464, 464), ((1,) * 56, 8, 1600, 1600), + (weighted, 4, 180, 36), (weighted, 5, 168, 40)) + records = [] + for costs, budget, expected, calls in cases: + price, tree = optimize(costs, budget) + check(price == expected, "recorded witness") + scratch, oracle_price = oracle_resources(tree, costs) + check(price == oracle_price and scratch <= budget, "witness path accounting") + check(sum(leaf_counts(tree).values()) == calls, "witness call count") + validate_word(tree, costs, budget, claimed_cost=price) + validate_word(tree, costs, budget, claimed_cost=price, sign=-1) + nonlinear_restore(tree, budget) + word = tuple(instructions(tree)) + encoded = (json.dumps(word, separators=(",", ":")) + "\n").encode("utf-8") + records.append(dict(costs=list(costs), budget=budget, scratch=scratch, + weighted_cost=price, calls=calls, + tree=json.loads(json.dumps(tree)), + leaf_multiplicities=[leaf_counts(tree)[i] + for i in range(len(costs))], + word_sha256=hashlib.sha256(encoded).hexdigest())) + return records + + +def refined_ternary_baseline(count): + """PR689's longer-end split, independently priced as a level frontier.""" + pending = [(count, 0, 1)] + calls = scratch = 0 + while pending: + size, occupied, copies = pending.pop() + if size == 1: + calls += copies + scratch = max(scratch, occupied) + elif size == 2: + pending.extend(((1, occupied + 1, copies * 2),) * 2) + else: + quotient, remainder = divmod(size, 3) + pending.extend(((quotient + (remainder > 0), occupied + 2, copies * 2), + (quotient, occupied + 2, copies * 4), + (quotient + (remainder > 1), occupied + 2, copies * 2))) + return scratch, calls + + +def baseline_check(): + # Pinned PR689 ternary.py's public resources order is (calls, scratch). + for count, expected in ((7, (4, 40)), (15, (5, 160)), + (27, (6, 512)), (56, (8, 2112))): + check(refined_ternary_baseline(count) == expected, "PR689 baseline") + + +def check_pins(): + manifest = (HERE / "SOURCES.json").read_bytes() + sources = json.loads(manifest) + checked = [] + for predecessor in sources["predecessors"]: + for source in predecessor["files"]: + if "local_copy" in source: + digest = hashlib.sha256((HERE / source["local_copy"]).read_bytes()).hexdigest() + check(digest == source["sha256"], "predecessor source pin") + checked.append(dict(path=source["local_copy"], sha256=digest, + commit=predecessor["commit"])) + check(checked, "missing local predecessor pins") + return sources, dict(manifest_sha256=hashlib.sha256(manifest).hexdigest(), + local_files=checked) + + +def predecessor_check(): + spec = importlib.util.spec_from_file_location("pr673_echo", HERE / "vendor/pr673_echo.py") + predecessor = importlib.util.module_from_spec(spec) + spec.loader.exec_module(predecessor) + + def balanced(first, count, fanout): + if count == 1: + return first + arity = min(count, fanout) + quotient, remainder = divmod(count, arity) + children = [] + for position in range(arity): + size = quotient + (position < remainder) + children.append(balanced(first, size, fanout)) + first += size + return tuple(children) + + compared = 0 + for count in range(1, 17): + for fanout in (2, 3): + tree = balanced(0, count, fanout) + costs = (1,) * count + scratch, price = oracle_resources(tree, costs) + check((scratch, price) == predecessor.resources(count, fanout), + "pinned predecessor resource comparison") + for sign in (1, -1): + word = tuple(instructions(tree, sign=sign)) + pinned = tuple(predecessor.instructions(0, count, 0, 1, 2, fanout, sign)) + check(word == pinned, "pinned predecessor instruction comparison") + validate_word(tree, costs, scratch, word=word, claimed_cost=price, sign=sign) + compared += 1 + return compared + + +def nonlinear_counterexample(): + increments = [] + for dirty in (0, 1): + registers = [1, 0, dirty] + for source, target, factor, sign in instructions((0, 1)): + increment = registers[source] if factor == 0 else registers[source] ** 2 + registers[target] += sign * increment + check(registers[0] == 1 and registers[2] == dirty, + "nonlinear counterexample restoration") + increments.append(registers[1]) + check(increments == [1, 3], "nonlinear dirty-dependent increment") + return dict(first_map="f(x)=x", second_map="g(x)=x^2", source=1, + initial_scratch=[0, 1], target_increments=increments, + composed_value=1) + + +def input_check(): + cases = (((), 0), ((0,), 0), ((True,), 0), ((1.5,), 0), + ((1,), -1), ((1,), True)) + for costs, budget in cases: + try: + optimize(costs, budget) + except ValueError: + pass + else: + raise AssertionError("invalid optimizer input accepted") + check(optimize([1], 0) == (1, 0), "valid list input") + return len(cases) + + +def mutation_check(): + tree = (0, 1, 2) + costs = (1, 1, 1) + word = tuple(instructions(tree)) + rejected(lambda: validate_word(tree, costs, 2, word=word[:-1]), + "ordered product and dirty restoration") + reversed_order = [(s, t, 2 - i, q) for s, t, i, q in word] + rejected(lambda: validate_word(tree, costs, 2, word=reversed_order), + "ordered product and dirty restoration") + rejected(lambda: validate_word(tree, costs, 2, claimed_cost=6), + "weighted leaf price") + rejected(lambda: validate_word(tree, costs, 1), "insufficient scratch") + return dict(omitted_restore="rejected", reversed_factor_order="rejected", + underpriced_middle="rejected", insufficient_scratch="rejected") + + +def build_certificate(): + sources, pins = check_pins() + cases, trees, optimal_shapes = exhaustive_check() + witnesses = witness_check() + baseline_check() + mutations = mutation_check() + return dict(schema_version=1, base_commit=sources["base_commit"], + assignment_seed=sources["assignment_seed"], source_pins=pins, + exhaustive_domain=dict(leaf_counts=list(range(1, 7)), cost_alphabet=[1, 3], + scratch_budgets="0 through leaf_count-1", + cost_budget_cases=cases, ordered_trees=trees, + optimizer_shapes=optimal_shapes), + predecessor_words=predecessor_check(), + invalid_inputs_rejected=input_check(), + word_encoding="UTF-8 compact JSON instruction array followed by LF", + witnesses=witnesses, + pr689_baselines=[dict(leaves=n, scratch=refined_ternary_baseline(n)[0], + calls=refined_ternary_baseline(n)[1]) + for n in (7, 15, 27, 56)], + nonlinear_counterexample=nonlinear_counterexample(), + mutation_controls=mutations) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print the recomputed certificate") + args = parser.parse_args() + certificate = build_certificate() + if args.emit: + print(json.dumps(certificate, indent=2, sort_keys=True)) + return + recorded = json.loads((HERE / "CERTIFICATE.json").read_text()) + check(json.dumps(certificate, sort_keys=True) == json.dumps(recorded, sort_keys=True), + "certificate differs from complete replay") + domain = certificate["exhaustive_domain"] + print(f"PASS_ORDERED_DIRTY_ECHO: {domain['cost_budget_cases']} exhaustive cases; " + f"{domain['ordered_trees']} ordered trees; " + f"{certificate['predecessor_words']} pinned predecessor words; " + f"{len(certificate['witnesses'])} witnesses; " + f"{len(certificate['mutation_controls'])} rejected mutations") + print("Exact formal ordered products and nonlinear integer restoration checked; " + "finite coverage only.") + + +if __name__ == "__main__": + main()