From 240ab1ef40d2f22c04f162d02bd6e54df47f04ef Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 01:25:53 +0530 Subject: [PATCH 1/2] Add reader-aware restoration cut planner and exact counterexample --- .../CERTIFICATE.json | 127 ++++ .../reader-restoration-cuts-seed53/CLAIM.md | 67 ++ .../reader-restoration-cuts-seed53/NOTICE.md | 31 + .../reader-restoration-cuts-seed53/README.md | 198 ++++++ .../SOURCES.json | 29 + .../VALIDATION.md | 78 +++ .../fixture.json | 12 + .../reader-restoration-cuts-seed53/planner.py | 73 +++ .../sources/pr1155/CERTIFICATE.json | 75 +++ .../sources/pr1155/README.md | 267 ++++++++ .../sources/pr1155/verify.py | 614 ++++++++++++++++++ .../test_package.py | 58 ++ .../reader-restoration-cuts-seed53/verify.py | 255 ++++++++ 13 files changed, 1884 insertions(+) create mode 100644 research/reader-restoration-cuts-seed53/CERTIFICATE.json create mode 100644 research/reader-restoration-cuts-seed53/CLAIM.md create mode 100644 research/reader-restoration-cuts-seed53/NOTICE.md create mode 100644 research/reader-restoration-cuts-seed53/README.md create mode 100644 research/reader-restoration-cuts-seed53/SOURCES.json create mode 100644 research/reader-restoration-cuts-seed53/VALIDATION.md create mode 100644 research/reader-restoration-cuts-seed53/fixture.json create mode 100644 research/reader-restoration-cuts-seed53/planner.py create mode 100644 research/reader-restoration-cuts-seed53/sources/pr1155/CERTIFICATE.json create mode 100644 research/reader-restoration-cuts-seed53/sources/pr1155/README.md create mode 100644 research/reader-restoration-cuts-seed53/sources/pr1155/verify.py create mode 100644 research/reader-restoration-cuts-seed53/test_package.py create mode 100644 research/reader-restoration-cuts-seed53/verify.py diff --git a/research/reader-restoration-cuts-seed53/CERTIFICATE.json b/research/reader-restoration-cuts-seed53/CERTIFICATE.json new file mode 100644 index 0000000000..12a046a46e --- /dev/null +++ b/research/reader-restoration-cuts-seed53/CERTIFICATE.json @@ -0,0 +1,127 @@ +{ + "base": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "fixture": { + "cost": 1, + "cuts": [ + 5 + ], + "segments": [ + { + "cost": 1, + "negate": [ + 0 + ], + "start": 0, + "stop": 5 + } + ] + }, + "forced_cut_2": { + "cost": 5, + "cuts": [ + 1, + 2, + 3, + 4, + 5 + ], + "segments": [ + { + "cost": 1, + "negate": [ + 0 + ], + "start": 0, + "stop": 1 + }, + { + "cost": 1, + "negate": [ + 0 + ], + "start": 1, + "stop": 2 + }, + { + "cost": 1, + "negate": [ + 0 + ], + "start": 2, + "stop": 3 + }, + { + "cost": 1, + "negate": [ + 0 + ], + "start": 3, + "stop": 4 + }, + { + "cost": 1, + "negate": [ + 0 + ], + "start": 4, + "stop": 5 + } + ] + }, + "invalid_input_controls": 9, + "mathematical_controls": [ + "changed reader destroys cancellation", + "checkpoint after child two destroys saving", + "final equality does not authorize an intermediate cut", + "same children in a different order lose cancellation" + ], + "retained_pr1155": { + "deferred_mults": 1, + "eager_mults": 5, + "old_certificate": "PASS", + "probes": 3 + }, + "scalar_exhaustion": { + "batches": 1555, + "max_children": 4, + "partitions": 11311 + }, + "scalar_instruction_invoice": { + "common_sufficient_signed_bits": 7, + "deferred": { + "adds": 5, + "coefficient_reads": 10, + "data_reads": 11, + "data_writes": 11, + "multiplies": 5, + "negations": 6, + "program_records": 6 + }, + "eager": { + "adds": 5, + "coefficient_reads": 10, + "data_reads": 15, + "data_writes": 15, + "multiplies": 5, + "negations": 10, + "program_records": 10 + }, + "input_D": 11, + "input_W": 7, + "output_D": 32, + "output_W": 7 + }, + "scope": "exact diagonal readers and signs; every chosen cut matches eager data and workspace; no new kappa", + "seed": 53, + "seeded_longer": { + "batches": 160, + "max_children": 8, + "max_dimension": 3, + "partitions": 5264 + }, + "status": "PASS_READER_RESTORATION_CUTS", + "two_coordinate_exhaustion": { + "batches": 1296, + "partitions": 2592 + } +} diff --git a/research/reader-restoration-cuts-seed53/CLAIM.md b/research/reader-restoration-cuts-seed53/CLAIM.md new file mode 100644 index 0000000000..e88a661cee --- /dev/null +++ b/research/reader-restoration-cuts-seed53/CLAIM.md @@ -0,0 +1,67 @@ +# Reader-aware restoration cuts + +Status: claimed, recursive interfaces, OS-random seed 53. Owner Sagar Thakrar +with OpenAI Codex, chat `01a136c4-b32d-7a30-92f0-d8dffa66b80f`, local host. +Scope key: `restoration-coalescing/diagonal-readers/checkpoint-correct-cuts`. + +Cycle starts 2026-10-13 19:37:19 UTC. Scope deadline 19:45:19 UTC; +verification starts by 20:07:19 UTC; hard finish 20:17:19 UTC. +Checkout: `/Users/thakrarsagar-dev/Documents/Codex/2026-10-13/continue-the-user-s-research-loop-13/work/integer-mult-bounds`. +Fetch completed 19:37:56 UTC. Clean local main and fetched origin/main were +both `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` at 19:38:11 UTC, before +creating `research/cycle08-seed53-recursive-interfaces`. That is the base. +Prior branches are preserved. + +## Three candidates and reductions before implementation + +1. **Selected: permit diagonal readers during restoration coalescing.** + PR1155, `9821c6e9388f3fc097e94b72be9fa7b41a849527`, gives read-free + phase/permutation examples, a failing reader example, a written model and + cost recurrence. Its README calls absence of readers necessary. Read the + README, actual Batch interpreter, builders, verifier and certificate. + Cheap counterexample in its exact model: five scalar children all negate + W and read coefficients `[1,1,1,-1,1]`. Eager and deferred outputs both + increment D by `3W`; one final negation restores W. All five children read + W. At child two the data values differ, so an intermediate observation is + a real constraint. New evidence: a necessary and sufficient interval test, + minimum-cost checkpoint-correct partition tool, full node recurrence and + exact independent enumeration. No novelty is claimed for matrix algebra. +2. **Rejected: extend four-way port borrowing to higher arity.** PR1164, + `0b2077e929ec488a4d38b3523688a8a68bf1b43e`, already gives the chain word, + endpoint/middle call multiplicities and a pool-count induction. Read its + PROOF.md and embedded PR1057 proof. Replacing four by k is a direct + consequence and a larger replay would add no distinct result. +3. **Rejected: fixed unequal positive/negative connector-query prices.** + Accepted PR1088, `b0396aad724fec58630fbd4d13a809c562f18d9e`, proves the + signed three-by-three weighted optimum. Read the retained README and + query alphabet. Uniform correctness forces equal positive/negative counts + for each named query, reducing its fixed directional prices to their + average. This does not produce a new optimization problem. + +## Scope and overlap + +The selected domain is a fixed ordered batch of exact diagonal reader shears +and diagonal signs over characteristic zero. Every chosen restoration cut +must match eager D and W, with optional mandatory cuts. The tool does not +optimize arbitrary reversible programs, permit inaccurate intermediate cuts, +change children, or claim a supplier or kappa improvement. A complete price +must include child calls, source access, workspace, preparation, control, +restoration and any physical adapters. + +Inspected all 1170 PRs available at the check, including 786 open PRs, their +bodies, the central ledger, selected PR1094 construction/assembly/source +manifest and review, prior loop negatives, and live discussions 1163/1166/1167. +There is no pinned sprint issue. The immediately refreshed discussion 1166 has +Adam Gall's unrelated PR279 provenance claim at 19:42:46 UTC; no overlapping +restoration claim appeared. The latest open PR was 1177. +Claim is local as specified by the research brief. No separate issue is opened. +PR249 `96495746c786d6d0339dbb38c7f553d4af3f88ed` and PR309 +`aeb4808af1392e565e7071cbeb2c29608201cf24` transport dirty-helper responses +through concrete supplier words; that algebra is credited, not reinvented as +a new mechanism. The distinct deliverable corrects PR1155's applicability claim +and supplies a reader-aware cut planner with a precise observation contract. +Prior PR1168's pending-output fanout cap is a different query alphabet. + +Stop if a matching planner or correction appears, or if no useful checked +artifact is ready by the verification deadline. At most one pivot, with the +original clock unchanged. Recheck overlap at first result and before submission. diff --git a/research/reader-restoration-cuts-seed53/NOTICE.md b/research/reader-restoration-cuts-seed53/NOTICE.md new file mode 100644 index 0000000000..c86cefe681 --- /dev/null +++ b/research/reader-restoration-cuts-seed53/NOTICE.md @@ -0,0 +1,31 @@ +# Credit and license + +Prepared for Sagar Thakrar, GitHub `thakrarsagar`, with substantial OpenAI Codex +assistance in investigation, proof writing, implementation and verification. +New material is licensed under the repository's Apache License 2.0. + +Aaron Wang / Navinor's PR1155, with opencode assistance, supplies the batch model, +read-free coalescing examples, a valid failing-reader example and the original +cost discussion. The retained README and verifier at +`9821c6e9388f3fc097e94b72be9fa7b41a849527` are byte-identical to their original +Git blobs. The retained certificate has a final newline appended, with identical +parsed content. Its source attribution and Apache-2.0 terms are preserved. This +package corrects a stated necessity claim without changing that predecessor. + +The general algebra of dirty-response transport is credited to eumemic's PR249 +and PR309 and their retained construction lineages. The exact heads are in +SOURCES.json. This package makes no priority claim for linear cancellation, +composed inverses or dynamic programming. Its added evidence is the concrete +PR1155 counterexample, observation boundary, restricted cut planner and independent +finite enumeration. + +PR1164 by woklerx, Gareth Davidson's PR1057, Koroffstrogov's PR758 and their +predecessors retain credit for dirty echo and port-borrowing mechanisms. They +were inspected as overlap, not used as runtime dependencies. `martinxxx9`'s +PR1088 and Ross Richardson's PR944 retain the signed connector results used to +reject another candidate. PR1168 is the separate pending-output fanout result +from the previous loop cycle. + +The unchanged selected PR1094 construction is Rohan Arun's packing on Jeremy +Kothe's PR1087 and the cumulative supplier, controller and bit lineages credited +in the selected review. No claimed improvement to those results follows here. diff --git a/research/reader-restoration-cuts-seed53/README.md b/research/reader-restoration-cuts-seed53/README.md new file mode 100644 index 0000000000..f58d1581de --- /dev/null +++ b/research/reader-restoration-cuts-seed53/README.md @@ -0,0 +1,198 @@ +# Restoration cuts that allow workspace readers + +This recursive-interface construction removes four of five restorations in a +batch where every child reads the dirty workspace. It also provides an exact +planner for the cheapest checkpoint-correct partition of a fixed diagonal +batch. No supplier, paid moment, runtime improvement or new kappa is claimed. + +The counterexample corrects the stated necessity of read-free children in +[PR1155](https://github.com/CrocSwap/integer-mult-bounds/pull/1155). Its retained +verifier reproduces both its original certificate and this new example. The +original failing-reader example remains valid; it does not establish necessity. +The added value is a checked applicability correction and a usable cut planner, +not a claim that linear cancellation or dynamic programming is new. + +## Five readers, one restoration + +Use scalar state D,W with arbitrary initial values. Each child first performs +`D += b_i W`, then `W = -W`, with reader coefficients + +``` +b = [1, 1, 1, -1, 1]. +``` + +Eager execution restores W after every child. Deferred execution lets it drift +until the batch ends. In both cases D ends at `D_initial + 3 W_initial`, and +one final negation restores deferred W. All five readers are nonzero, including +readers of the changed workspace. The restoration bill is five negations versus +one. With `D_initial=11,W_initial=7`, both end at `(32,7)`. + +After child two, eager D is 25 and deferred D is 11. Requiring an observation +and restoration there makes the optimal bill five again. Output timing is part +of the contract. This is not safe substitution under arbitrary prefix observers. + +## Reproduce and use + +Python 3.11 or newer, standard library only, from the repository root: + +```sh +rtk proxy python3 -I -O -B research/reader-restoration-cuts-seed53/verify.py +rtk proxy python3 -I -O -B research/reader-restoration-cuts-seed53/test_package.py +rtk proxy python3 -I -B research/reader-restoration-cuts-seed53/planner.py research/reader-restoration-cuts-seed53/fixture.json +``` + +The verifier prints +`PASS_READER_RESTORATION_CUTS restoration=5->1 forced_cut=5 exhaustive=2851 seeded=160`. +The package test reports relocation, canonical regeneration and four rejected +corruptions. The planner emits cost 1, cuts `[5]` and a final negation of coordinate +zero. Adding `"required": [2]` to a copy of the fixture yields cost 5 and all five +cuts. Coordinates are zero based; cuts count completed children, from one to r. + +Planner input contains `children`, each with equally sized integer `reader` and +`signs` arrays, and positive integer `prices` for complete coordinate negations. +Signs must be -1 or 1. Optional `overhead` is a nonnegative complete per-nonempty- +restoration dispatch charge. `required` lists mandatory cuts. An empty batch is +valid. Zero reader coefficients represent workspace-independent data work; +such independent increments can be added unchanged outside this model. + +## Exact criterion and proof + +Let D,W have N coordinates over a characteristic-zero field. Child i applies + +``` +D <- D + diag(b_i) W +W <- diag(g_i) W, g_ij in {-1,1}. +``` + +The child restores its private work and preserves all other data. Source and +target do not alias. There are no intermediate observers except declared cuts, +no hidden state, no rounding and no other dependence on W or old D. The eager +comparator restores W after each child. The planner accepts integer readers; +the proof itself also holds for rational or complex readers. + +For an interval [a,b), define `p_a=1` componentwise and +`p_(i+1)=g_i p_i`. Just before child i the deferred workspace is `p_i W_entry`. +The deferred-minus-eager data increment is therefore + +``` +diag(E_ab) W_entry, E_ab = sum_(i=a)^(b-1) b_i (p_i - 1). +``` + +The interval is correct for every input exactly when every coordinate of E_ab +is zero. Sufficiency follows by substitution. For necessity, a nonzero entry +is detected by its workspace basis vector. Applying the final diagonal sign +`p_b` restores W since each sign is its own inverse. Read-free intervals set +every b_i to zero, but they are only one sufficient case. The example above +has two nonzero residual terms that cancel. + +For general linear readers B_i and invertible workspace maps G_i the same +calculation gives `sum B_i(P_i-I)=0`, with ordered prefixes P_i. This is context +for the correction, not an implemented general-matrix optimizer. Unlike earlier +dirty-response transport, this tool changes no reader and moves no supplier gate. + +## Restricted optimum + +Every selected cut must reproduce eager D and W. This requirement applies even +to additional cuts introduced by the planner. A legal interval cannot cross a +mandatory cut. Its price is the sum of the supplied prices of the coordinates +with final sign -1, plus overhead if that set is nonempty. Identity restoration +emits no command and costs zero under this explicit model. + +Set `F(0)=0`. For b from one through r, minimize + +``` +F(b) = min_(legal [a,b)) F(a) + restore_price(a,b). +``` + +Every legal partition has a final interval and its preceding prefix is a legal +partition. Conversely, adjoining a legal interval to a correct prefix gives a +correct partition. Induction proves the recurrence gives the minimum in this +class. Ties use fewer segments, then lexicographic cuts. Single-child intervals +are always correct, so an input satisfying the schema always has a plan. + +This does not optimize schedules whose errors persist across an inserted cut +and cancel later, reordering, changed child implementations, non-diagonal +restorations, or arbitrary reversible programs. The literal-column checker +enumerates partitions independently and tests equality at every proposed cut. + +The implementation computes residuals and prefixes with O(r^2 N) integer +arithmetic operations, plus O(r^3) worst-case required-cut tests and tuple +copying/tie comparisons. Storage is O(r^2 N + r^2), including candidate masks +and saved cut tuples. Integer bit costs are additional. No precomputed plan or +descriptor is assumed free. + +## Complete node bill and precision + +Let C_i be the complete cost of child i under the deferred interface, including +its recursive descendants, source/coefficient accesses, private work and its +restoration, data readout, workspace sign change, routing and frame adapters. +The same fixed upper price and common precision must be valid for every allowed +incoming state and for both eager and deferred schedules. Children cannot have +unpriced dependence on the current workspace value. + +For node v, the complete conditional recurrence is + +``` +T_v = admission_v + preparation_v + planning_v + program_storage_and_reads_v + + sum_i T_child_i + sum_i local_child_work_i + + sum_(emitted restorations h) Restore_v(h) + + batch_control_v + routing_or_frame_work_not_in_children_v. +``` + +Here `T_child_i + local_child_work_i = C_i`. Restore_v must include reads, +negations, writes, mask/descriptor access, dispatch, head return and any private +work. If a backend realizes Restore_v as the supplied additive prices plus the +supplied overhead, the planner is optimal for that restoration term. Otherwise +this price model must not be used for that backend. Eager replaces the emitted +restorations by each child's inverse sign. All other terms stay explicitly +charged; different preparation/program/control costs must be compared too. +Repeated nodes use the displayed recurrence, paying planning where it occurs. +There is no claimed improvement to the selected unequal-rank child moment. + +For exact integer input bounds `|W_j|<=U`, `|D_j|<=V`, both schedules satisfy +`|W_j|<=U` and `|D_j|<=V+U sum_i |b_ij|` at all prefixes. Products obey the +same majorant. A sufficient common signed width is one plus the bit length of +the maximum of U, `V+U max_j sum_i |b_ij|`, and all coefficient magnitudes. +The fixture takes U=7,V=11 and seven signed bits. This is an exact integer +headroom bound, not a numerical rounding theorem. + +For the fixture, the specified scalar interpreter reads W,D and b,g per child, +multiplies bW, adds to D, writes D, and negates/writes W for g=-1. A restoration +reads W, negates it and writes W. Both programs execute five multiplies and five +adds, and read ten coefficients. Eager/deferred data reads are 15/11, data writes +15/11, negations 10/6 and program records 10/6. Each record's bit decoding and +travel cost, storage, initial admission, preparation and planner work are the +separate terms above. The interpreter also reverses the literal program. +These are counted operations, not a runtime benchmark or fixed-tape compiler. + +## Evidence, sources and remaining work + +[CERTIFICATE.json](CERTIFICATE.json) records 1,555 exhaustive scalar batches of +length zero through four, 1,296 exhaustive two-coordinate two-child batches, +and 160 deterministic seed-53 longer batches of length five through eight. +All binary cut masks are exhausted within each declared batch, after enforcing +mandatory cuts. The independent interpreter retains every D and W basis column. +The certificate records the exact partition counts. Finite tests support the +written proof; they are not a formal proof of the multiplication theorem. + +Controls change the cancelling reader, add an intermediate observation, reorder +a read around a workspace change, corrupt an emitted cost and mutate source or +certificate bytes. Nine input errors and one unknown CLI field are rejected. +The unchanged PR1155 certificate still passes. Its exact Batch implementation +also confirms the new construction on real and imaginary basis inputs and a +nontrivial dirty Gaussian input. No claim is made against its valid negative +example or its finite recorded counts. Its heterogeneous-cost discussion is +outside this contribution's scope. + +Base `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` selected PR1094 at conditional +kappa `836330098538459/500000000000000000`. [SOURCES.json](SOURCES.json) binds +the runtime predecessor files and records separate context-only selected pins. +The package replays offline from its own directory. It does not depend on a +future moving selected record. [CLAIM.md](CLAIM.md) records assignment, rejected +covered candidates, exact heads and overlap. [NOTICE.md](NOTICE.md) preserves +credit and license. [VALIDATION.md](VALIDATION.md) records environments and checks. + +Supplier realization, common labels and frames, whole-call hosting, fixed-tape +routing, precision/recovery beyond the exact integer model, and analytic transfer +remain unproved here. No selected source, frozen upstream file or other PR is +modified. No full cold replay or proof-assistant verification is claimed. diff --git a/research/reader-restoration-cuts-seed53/SOURCES.json b/research/reader-restoration-cuts-seed53/SOURCES.json new file mode 100644 index 0000000000..207571949b --- /dev/null +++ b/research/reader-restoration-cuts-seed53/SOURCES.json @@ -0,0 +1,29 @@ +{ + "base": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "predecessor": { + "pr": 1155, + "head": "9821c6e9388f3fc097e94b72be9fa7b41a849527", + "directory": "research/restoration-coalescing", + "credit": "Aaron Wang / Navinor, with opencode assistance", + "license": "Apache-2.0", + "copy_note": "README.md and verify.py are byte-identical to the pinned Git blobs. CERTIFICATE.json has one final LF appended; its parsed JSON is unchanged." + }, + "files": { + "sources/pr1155/README.md": "1af4e8d65700207092859b80fa5e4f4a7bd254ac0104d83c2b74e3a7477e823b", + "sources/pr1155/CERTIFICATE.json": "d19d11803dcd8b6932854ae7008055a4b22665bf4759011af466f2ca1f655153", + "sources/pr1155/verify.py": "f8745ec2bac4032d6e98cb68300c1780b84b4a8ffde24e64730ac2ca5903b78b" + }, + "context_only_at_base": { + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "research/community-frontier1094-audit/SELECTED-SOURCE.json": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b", + "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + "other_overlap_heads": { + "PR1164": "0b2077e929ec488a4d38b3523688a8a68bf1b43e", + "PR1088": "b0396aad724fec58630fbd4d13a809c562f18d9e", + "PR249": "96495746c786d6d0339dbb38c7f553d4af3f88ed", + "PR309": "aeb4808af1392e565e7071cbeb2c29608201cf24", + "PR1168": "b53b07b5aed4e00358a0d0061ad99dbf5190ca2b" + } +} diff --git a/research/reader-restoration-cuts-seed53/VALIDATION.md b/research/reader-restoration-cuts-seed53/VALIDATION.md new file mode 100644 index 0000000000..01633c2a0f --- /dev/null +++ b/research/reader-restoration-cuts-seed53/VALIDATION.md @@ -0,0 +1,78 @@ +# Validation record + +Verification and packaging began by 2026-10-13 19:52:45 UTC, ahead of the +20:07:19 verification deadline. The cycle's hard finish is 20:17:19 UTC. +Host: macOS 26.5.2, arm64. CPython 3.11.15 and 3.14.8, standard library only. + +Both interpreters passed normal and optimized isolated verifier runs: + +```sh +rtk proxy python3.11 -I -B research/reader-restoration-cuts-seed53/verify.py +rtk proxy python3.11 -I -O -B research/reader-restoration-cuts-seed53/verify.py +rtk proxy python3 -I -B research/reader-restoration-cuts-seed53/verify.py +rtk proxy python3 -I -O -B research/reader-restoration-cuts-seed53/verify.py +``` + +Expected `PASS_READER_RESTORATION_CUTS restoration=5->1 forced_cut=5 exhaustive=2851 seeded=160`. + +- 1,555 exhaustive scalar batches, all lengths zero through four, signs ±1 and + readers -1,0,1. 11,311 partitions replayed independently. +- 1,296 exhaustive two-coordinate two-child batches, signs ±1 and readers + -1,0,1 in each coordinate. Prices `[2,5]`, nonempty restoration overhead 3. + 2,592 partitions replayed independently. +- 160 deterministic seed-53 batches, lengths five through eight, dimensions + one through three, reader values -3 through 3, positive prices one through + nine, overhead zero through three, and declared mandatory cuts. Every cut + mask satisfying those cuts was tested, 5,264 partitions in total. +- All D/W basis columns and every selected cut are checked. Exact equality, + no floating-point tolerances or sampled input vectors in this oracle. +- The five-reader construction and its literal inverse pass. The scalar + instruction invoice is recounted and included in the certificate. +- Four mathematical controls distinguish final equality from intermediate + legality, remove the cancellation, reorder a reader, and require child-two + observation. Nine invalid planner inputs are rejected. +- PR1155's original certificate reproduces with its unchanged checker. Its + Batch implementation confirms five-versus-one restoration multiplication + counts and equality for real and imaginary basis inputs plus `W=7-3i`. + +On both interpreters, the package test passes in optimized isolated subprocesses: + +```sh +rtk proxy python3.11 -I -O -B research/reader-restoration-cuts-seed53/test_package.py +rtk proxy python3 -I -O -B research/reader-restoration-cuts-seed53/test_package.py +``` + +This relocates the package, regenerates and compares every parsed certificate +field, checks the public planner CLI, and rejects four independent file +corruptions plus an unknown CLI field. The corruption cases alter the saved +cost, pinned source, cancelling reader and emitted planner cost. No shell, +network or repository-wide source is needed by the relocated checker. + +Certificate SHA256: +`3968403e53ec0937bd9ee1203de402b3d40810e7b489ad4ff31960ddc69face1`. +JSON serialization is deterministic. The retained PR1155 certificate differs +from its upstream bytes only by an appended final LF, as declared in SOURCES.json; +its parsed fields and original verifier are unchanged. + +Repository guard checks: + +```sh +rtk proxy python3 -B scripts/verify_selected_result.py +rtk proxy python3 -B -m unittest discover -s tests -p 'test_selected*.py' +rtk git diff --check +``` + +Selected integrity passes at unchanged conditional kappa +`836330098538459/500000000000000000`; all 25 selected tests pass. No pre-existing +tracked file is changed. New material is confined to this research directory. + +At the first completed result, the live queue through PR1184 was checked again. +PR1155, PR1164 and accepted PR1088 retained the exact heads in SOURCES.json and +had no review or comment correcting the read-free condition. No matching planner +or correction appeared. The claim remains in its original scope, with no pivot. + +Not run: the complete selected cold replay, full historical repository suite, +Linux execution, hosted CI, proof-assistant formalization or independent human +review. This package does not alter the selected construction, so a cold replay +is not the applicable verification target. Supplier admission and the remaining +physical and analytic interfaces are not established by these finite checks. diff --git a/research/reader-restoration-cuts-seed53/fixture.json b/research/reader-restoration-cuts-seed53/fixture.json new file mode 100644 index 0000000000..01b9fc95c0 --- /dev/null +++ b/research/reader-restoration-cuts-seed53/fixture.json @@ -0,0 +1,12 @@ +{ + "children": [ + {"reader": [1], "signs": [-1]}, + {"reader": [1], "signs": [-1]}, + {"reader": [1], "signs": [-1]}, + {"reader": [-1], "signs": [-1]}, + {"reader": [1], "signs": [-1]} + ], + "prices": [1], + "required": [], + "overhead": 0 +} diff --git a/research/reader-restoration-cuts-seed53/planner.py b/research/reader-restoration-cuts-seed53/planner.py new file mode 100644 index 0000000000..5584a8d895 --- /dev/null +++ b/research/reader-restoration-cuts-seed53/planner.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Minimum paid sign restorations at checkpoint-correct batch cuts. Apache-2.0.""" +import argparse +import json +from pathlib import Path + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def plan(children, prices, required=(), overhead=0): + """Children read D += reader*W, then W *= signs, component by component.""" + need(isinstance(children, list), "children must be a list") + need(isinstance(prices, list) and prices, "prices must be a nonempty list") + need(all(type(p) is int and p > 0 for p in prices), "prices must be positive integers") + need(type(overhead) is int and overhead >= 0, "overhead must be a nonnegative integer") + n, r = len(prices), len(children) + need(isinstance(required, (list, tuple)), "required must be a list or tuple") + need(all(type(k) is int and 0 < k <= r for k in required), "required cut out of range") + need(len(set(required)) == len(required), "duplicate required cut") + for child in children: + need(isinstance(child, dict) and set(child) == {"signs", "reader"}, "invalid child fields") + for key in ("signs", "reader"): + need(isinstance(child[key], list) and len(child[key]) == n, "child dimension mismatch") + need(all(type(x) is int for x in child[key]), "child entries must be integers") + need(all(x in (-1, 1) for x in child["signs"]), "sign must be -1 or 1") + + intervals = {} + for start in range(r): + prefix, residual = [1] * n, [0] * n + for stop in range(start + 1, r + 1): + child = children[stop - 1] + for j in range(n): + residual[j] += child["reader"][j] * (prefix[j] - 1) + prefix[j] *= child["signs"][j] + if any(start < k < stop for k in required): + continue + if not any(residual): + negative = [j for j, sign in enumerate(prefix) if sign == -1] + cost = sum(prices[j] for j in negative) + (overhead if negative else 0) + intervals[start, stop] = {"start": start, "stop": stop, + "negate": negative, "cost": cost} + best = [(0, 0, ())] + [None] * r + for stop in range(1, r + 1): + choices = [] + for start in range(stop): + if (start, stop) in intervals and best[start] is not None: + cost, count, cuts = best[start] + choices.append((cost + intervals[start, stop]["cost"], count + 1, cuts + (stop,))) + best[stop] = min(choices) + cost, _, cuts = best[r] + starts = (0,) + cuts[:-1] + return {"cost": cost, "cuts": list(cuts), + "segments": [intervals[a, b] for a, b in zip(starts, cuts)]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("input", type=Path, help="JSON with children, prices, optional required and overhead") + args = parser.parse_args() + try: + data = json.loads(args.input.read_text()) + need(isinstance(data, dict) and {"children", "prices"} <= set(data), "missing input fields") + need(set(data) <= {"children", "prices", "required", "overhead"}, "unknown input fields") + print(json.dumps(plan(**data), indent=2, sort_keys=True)) + except (OSError, ValueError, TypeError) as exc: + parser.exit(1, "FAIL_RESTORATION_PLAN: " + str(exc) + "\n") + + +if __name__ == "__main__": + main() diff --git a/research/reader-restoration-cuts-seed53/sources/pr1155/CERTIFICATE.json b/research/reader-restoration-cuts-seed53/sources/pr1155/CERTIFICATE.json new file mode 100644 index 0000000000..a4cd1ee9dd --- /dev/null +++ b/research/reader-restoration-cuts-seed53/sources/pr1155/CERTIFICATE.json @@ -0,0 +1,75 @@ +{ + "base": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "cases": { + "hetero_negative": { + "children": 3, + "composed_form": "dense", + "composed_inverse_dense": true, + "composed_inverse_nnz": 64, + "deferred_dense_mults": 64, + "eager_structured_mults": 16, + "mult_elimination": false, + "observables_equal": true + }, + "perm": { + "children": 3, + "composed_form": "perm", + "deferred_moves": 8, + "deferred_restoration_passes": 1, + "eager_moves": 24, + "eager_restoration_passes": 3, + "observables_equal": true + }, + "phase": { + "children": 3, + "composed_form": "diag", + "deferred_mults": 8, + "deferred_restoration_passes": 1, + "eager_mults": 24, + "eager_restoration_passes": 3, + "mult_ratio": "3", + "observables_equal": true + }, + "reader_negative": { + "discrepancy": [ + [ + "0", + "0" + ], + [ + "3", + "-1" + ], + [ + "4", + "0" + ], + [ + "6", + "0" + ], + [ + "3", + "-1" + ], + [ + "6", + "4" + ], + [ + "6", + "0" + ], + [ + "3", + "5" + ] + ], + "discrepancy_nonzero": true, + "observables_equal": false + } + }, + "dimension_N": 8, + "e": 3, + "summary": "phase=PASS perm=PASS hetero_dense=CONFIRMED reader_diverges=CONFIRMED" +} diff --git a/research/reader-restoration-cuts-seed53/sources/pr1155/README.md b/research/reader-restoration-cuts-seed53/sources/pr1155/README.md new file mode 100644 index 0000000000..43ef54beed --- /dev/null +++ b/research/reader-restoration-cuts-seed53/sources/pr1155/README.md @@ -0,0 +1,267 @@ +# Restoration coalescing across a recursion batch + +Research note: one explicit way to eliminate restoration work, with a complete +cost recurrence, a sharp correctness boundary, and a sharp cost boundary. +Navinor, with help from opencode. Apache-2.0. **No new multiplication exponent.** + +## Summary + +Every recursive child that borrows a dirty workspace stream must return it, and +the inherited contract restores it **after every child** so that the next child +sees the node-entry state. When a node issues `r` children this pays `r` +restoration passes. This note prices a single operator-level change: let the +workspace drift across the batch and replace the `r` restorations by the **one** +composed restoration `(G_r...G_1)^{-1}` at the node exit. The question is not +what a particular assembly does with that slack (that is assembly pricing), but +when this rewrite is even a *valid and pass-reducing identity on the restored +operator*. Two independent conditions decide it, both decidable exactly. + +* **Correctness (read-free batch).** The deferred single restoration returns the + identical observables (final data and final workspace) if and only if no child + reads the workspace's intermediate value to build an observable output. If the + workspace is write-only scratch across the batch, deferral is exact. One reader + child breaks it; the note gives a concrete counterexample over Gaussian + rationals. + +* **Cost (composable family).** Deferral removes restoration work only when the + individual restoration operators are closed under a composition that stays + cheap to apply. Diagonal unit phases compose to a diagonal unit phase and + permutations compose to a permutation, so a batch of `r` such restorations + collapses from `r` passes to `1` pass. When the restorations are a *mixture* + (a phase, a Walsh transform, a permutation), the composed restoration is a + dense linear map; applying it once costs `N^2` scalar multiplications against + `16` for the three structured eager restorations in the tested batch, so + deferral *loses*. Structure, not the number of restorations alone, decides. + +Both facts are checked by one exact stdlib program over Gaussian rationals. +Nothing here changes the selected frontier, `upstream/`, or the assembly. + +## Reproduce + +From the repository root, Python 3.10+, standard library only: + +```sh +python3 -I -O -B research/restoration-coalescing/verify.py +``` + +Expected first line: + +``` +PASS_RESTORATION_COALESCING phase=3->1(x3) perm=3->1 hetero_dense=True reader_diverges=True +``` + +The command recomputes the certificate and compares every field with +[CERTIFICATE.json](CERTIFICATE.json), failing on any drift. `--json` prints the +full certificate; `--write PATH` writes the same deterministic result elsewhere. +There is no floating point, no random tolerance, and no imported supplier +verifier. Coefficients are exact Gaussian rationals (`Fraction` real and +imaginary parts); the checker builds every operator explicitly at `N = 8`. + +## Starting point and scope selection + +Base commit `ce7ad1b6ab09452c3478723a2e96ed5ff212dc08` (current `origin/main`). +At this base the selected conditional result is the +`CrocSwap/integer-mult-bounds#1094`-on-`CrocSwap/integer-mult-bounds#1087` +assembly, +`kappa = 836330098538459/500000000000000000 = 0.001672660197076918`; see the +[selected record](../../certificates/selected-result.json) and +[current status](../../docs/research/current-status.md). This note does not +adopt any larger number from a pending pull request. + +The OS-generated assignment seed was **53**, assigning the recursive-interface +track (one explicit way to eliminate boundary or restoration work, with a +complete cost recurrence). The three candidates I weighed were: coalescing +per-child dirty-workspace restoration (chosen); deferring the compact-control +"exceptional-address repair charged at every node"; and eliminating the Walsh +entrance/exit boundary between same-subset children. The seed selected +restoration coalescing because it is the one whose correctness and cost +conditions can both be decided exactly and independently, without re-opening a +closed supplier search. + +There was no pinned sprint coordination issue reachable here. The local +[claim](CLAIM.json) records the three candidates, the overlap check against +`research/seed51-clean-residual-dilation` (seed 51, recursive-interface track: +a spectral-split residual encoder, a different object), and the scope. +Exact source and dependency heads are in [SOURCE-PINS.json](SOURCE-PINS.json). + +## The model + +State is a data stream `D` and a borrowed dirty workspace stream `W`, each of +`N` Gaussian-rational positions, plus a read-only source vector `s`. A node +issues `r` children. Child `i` applies an invertible workspace operator `G_i` +(as scratch) and contributes a data increment: + +``` +scratch-only child i : D' = D + B_i s , W' = G_i W +reader child i : D' = D + B_i W , W' = G_i W (reads W) +``` + +The inherited **eager** rule restores `W` to its node-entry value `w0` after +every child, i.e. it applies `G_i^{-1}` immediately. The **deferred** rule lets +`W` drift and applies the single composed restoration +`(G_r ... G_1)^{-1} = G_1^{-1} ... G_r^{-1}` at the node exit. Observables are +the final `D` and final `W`. The child data work `sum_i B_i(·)` is identical in +both schemes and cancels from the comparison; only restoration is priced. + +This is the same restoration invariant the repository already charges: dirty +connectors and private child scratch are restored +(`CrocSwap/integer-mult-bounds#905`, `CrocSwap/integer-mult-bounds#929`, +`CrocSwap/integer-mult-bounds#951`; +[universal-connector-boundary](../universal-connector-boundary/README.md)), and +the compact-control construction "restores arbitrary values ... and charges +exceptional-address repair at every node" ([current status](../../docs/research/current-status.md)). + +## Complete cost recurrence + +Write `Restore(N)` for one restoration pass over `N` coefficient positions. In +the repository's additive accounting a coefficient pass is a `Scan(N,p)`; a +diagonal unit-phase restoration is exactly one such pass, and a permutation +restoration is one routing pass. Let `r` be the children per node. The node's +restoration term is + +``` +eager : r * Restore(N) +deferred: 1 * Restore_composed(N) +``` + +**Composable family (phases, or permutations).** `Restore_composed(N) = +Restore(N)`, because the composition stays in the family. The node saves + +``` +(r - 1) * Restore(N) = (r - 1) * Scan(N, p) +``` + +plus the `O(r)` bookkeeping of composing `r` phase/permutation descriptors, +which is not an `N`-volume pass. Over a recursion with `r` children per node and +`d` levels, the total restoration overhead falls by the same factor `r` +(`sum_nodes r*Scan -> sum_nodes 1*Scan`), while every child term +`(k/m)^sigma / W` is untouched. The full node recurrence, restoring only the +changed term, is + +``` +R(N, {k_i}) = sum_i (k_i/m)^sigma / W + Restore(N) + O(r) + unchanged + ^ was r * Restore(N) in the inherited rule +``` + +**Heterogeneous family.** `Restore_composed(N) = Theta(N^2)` (a dense +matrix-vector product), against `sum_i` of the structured eager restorations. +At `N = 8` the exact counts are `64` dense multiplications versus `16` across +the three structured restorations, so the deferred rule is `4x` more expensive +and is rejected. The obstruction is structural: composing a phase with a Walsh +transform with a permutation destroys the structure that made each individual +restoration cheap. Deferral does **not** remove work here. + +This is a complete invoice for the restoration term only. It is not a transfer +into the tight fixed-tape overhead allowance, and it makes no claim that the +restoration term is binding in the selected assembly. If restoration is a +lower-order term beside the child recursion, the induced change to `kappa` is +zero. **No stronger bound is claimed.** + +## Exact evidence and limits + +`verify.py` builds every operator explicitly at `N = 8` over Gaussian rationals +and checks, on the actual vectors: + +1. **Phase batch (3 children, read-free).** Deferred equals eager on both + observables; the composed restoration is verified to be diagonal and applied + as one pass. Restoration passes `3 -> 1`; multiplications `24 -> 8`. +2. **Permutation batch (3 children, read-free).** Deferred equals eager; the + composed restoration is verified to be a permutation and applied as one + routing pass. Restoration passes `3 -> 1`; moves `24 -> 8`; multiplications + `0 -> 0`. +3. **Reader negative control (correctness).** A single reader child is inserted. + The final workspace is still restored to `w0`, but the data output of the + deferred scheme differs from eager by an explicit nonzero Gaussian-rational + vector. This is a concrete counterexample: the read-free condition is + necessary, not a stylistic choice. +4. **Heterogeneous negative control (cost).** A phase, a Walsh transform and a + permutation compose to a dense operator (64 of 64 entries nonzero). The + structured-form detector self-checks each cheap application against the exact + dense product on the standard basis before using it, so the low cost figures + are certified against the exact operator rather than assumed. Deferred `64` + multiplications beat nothing: the eager structured sum is `16`. + +For each batch the composed restoration is *derived* from the exact dense +product `G_1^{-1} ... G_r^{-1}` and then checked to agree with it, so a +composition-order bug cannot silently flatter the result. Controls that must +fail do fail: no "no candidate" claim, no impossibility theorem, no optimality +claim for the eager rule. + +The scope is a restoration-elimination mechanism, its recurrence, and its exact +applicability boundary. It is **not** an all-size physical compiler, a numerical +precision contract, a common tape, an analytic transfer, a full owner schedule, +or the integer-multiplication theorem. The finite checks are exact algebraic +identities and exact cost counts; they do not certify a whole E8 word or the +selected `kappa`. Neither the selected frontier nor `upstream/` changes. Inherited +all-size/compiler, hosting, precision/tape and analytic assumptions remain with +their existing constructions. + +## Relation to concurrent and prior work + +Two concurrent, same-track contributions already price *restoration deferral* at +the assembly level, and this note is deliberately narrower and complementary, +not a replacement or a re-derivation of either. + +* **[CrocSwap/integer-mult-bounds#1012](https://github.com/CrocSwap/integer-mult-bounds/pull/1012)** + (thakrarsagar, seed 57) prices restoration deferral of the U8 helper + rank/frame *climbs* inside the hosted T37 recurrence, using the hosting lemma + and the `8k+1+hosted+idle=73` coverage identity, and reports exact kappa + ceilings. Its conclusion is that deferral is *mass-neutral* there and its value + is consolidation inside shared hosting windows. That is a statement about rank + mass and window capacity in one frozen assembly. + +* **[CrocSwap/integer-mult-bounds#974](https://github.com/CrocSwap/integer-mult-bounds/pull/974)** + (avirazza, same track) prices the same boundary classes with zero parent cost; + thakrarsagar's note independently reproduces its T37 one-unit value. + +This note asks a different question at a different layer: **as an operator +identity, when does replacing `r` restorations by one composed restoration +preserve the observables and actually remove passes?** Its two answers — the +read-free condition (correctness) and the composable-family condition (cost) — +are exact algebraic facts about the restored operator, independent of any +assembly, kappa ceiling, hosting lemma, or T37 payload. The cost unit here is a +coefficient/routing pass (a diagonal unit phase is one `Scan`, a permutation is +one `Route`, per the retained recurrence vocabulary), not the rank mass those +assembly notes count. So there is no contradiction with the "mass-neutral" +finding there: helper climbs are rank-advancing frame work whose mass is +coverage-productive, whereas the restoration passes coalesced here are +phase/routing passes whose operators compose. This note gives the +operator-level preconditions and a standalone sub-second exact verifier (no T37 +archives, no pinned engines); those notes give the assembly-level ceiling +effect. Both are needed before deferral can be placed in a real supplier call. +Where thakrarsagar's note shows the T37 slack is consolidation in shared +windows, this note shows exactly which restoration families admit a genuine +`r -> 1` pass reduction at all, and which (heterogeneous) make it worse. + +This is a second, independent treatment of the restoration question using a +meaningfully different method (exact Gaussian-rational operator algebra and +structure detection, versus assembly-level pricing on frozen payloads), as the +sprint invites. It does not claim priority on "restoration deferral" and does not +reproduce either note's numbers. + +## Attribution + +The eager per-child restoration contract and the dirty-connector model are +repository-wide: `CrocSwap/integer-mult-bounds#905`/ +`CrocSwap/integer-mult-bounds#929`/ `CrocSwap/integer-mult-bounds#951` (Chafik +Boukhalfa), `CrocSwap/integer-mult-bounds#877`/ +`CrocSwap/integer-mult-bounds#896` (Gareth Davidson), +`CrocSwap/integer-mult-bounds#934`/ `CrocSwap/integer-mult-bounds#943`/ +`CrocSwap/integer-mult-bounds#944`/ `CrocSwap/integer-mult-bounds#953` (Ross +Richardson), and +[universal-connector-boundary](../universal-connector-boundary/README.md). The +compact-control per-node restoration/repair charge is credited to Douglas +Colkitt's retained construction ([current status](../../docs/research/current-status.md)). +The unequal-width child recurrence `(k/m)^sigma / W` is from the retained +[complex batching note](../../notes/batched-complex-rows.tex). + +The sibling recursive-interface note +[research/clean-residual-dilation](../clean-residual-dilation/README.md) (seed 51, +Douglas R. Colkitt with Codex) prices a *spectral-split residual encoder* and its +own per-stream dirty restoration. This note is a different object (restoration +coalescing across a batch, not encoded hosting), reaches a different and +independent boundary (read-free + composable family), and does not rely on its +conclusions. Where both charge a "restoration" pass, the accounting vocabulary is +shared but the mechanisms are distinct. This encoder-free coalescing result, +exact checker and scoped recurrence were developed by Navinor with help from +opencode, under the repository's Apache-2.0 license. diff --git a/research/reader-restoration-cuts-seed53/sources/pr1155/verify.py b/research/reader-restoration-cuts-seed53/sources/pr1155/verify.py new file mode 100644 index 0000000000..d5b6df2607 --- /dev/null +++ b/research/reader-restoration-cuts-seed53/sources/pr1155/verify.py @@ -0,0 +1,614 @@ +#!/usr/bin/env python3 +"""Exact checker for the restoration-coalescing research note. + +Independently builds a recursion batch that borrows a dirty workspace stream, +then compares the inherited eager per-child restoration against a deferred +single-pass restoration. All arithmetic is exact Gaussian rationals +(Fraction real and imaginary parts); no floating point, no random tolerance, +no imported supplier verifier. Pure standard library. + +Run: + python3 -I -O -B research/restoration-coalescing/verify.py + +Expected first line: + PASS_RESTORATION_COALESCING phase=... perm=... hetero=... reader=... + +`--write PATH` emits the deterministic certificate JSON to PATH. +`--json` prints the full certificate to stdout. +""" +from __future__ import annotations + +import argparse +import json +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +BASE = "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +# -------------------------------------------------------------------------- +# Exact Gaussian rationals: a + b i, a,b in Fraction. +# -------------------------------------------------------------------------- +class G: + __slots__ = ("re", "im") + + def __init__(self, re=0, im=0): + self.re = Fraction(re) + self.im = Fraction(im) + + def __add__(self, other): + other = _g(other) + return G(self.re + other.re, self.im + other.im) + + __radd__ = __add__ + + def __neg__(self): + return G(-self.re, -self.im) + + def __sub__(self, other): + return self + (-_g(other)) + + def __mul__(self, other): + other = _g(other) + return G(self.re * other.re - self.im * other.im, + self.re * other.im + self.im * other.re) + + __rmul__ = __mul__ + + def conj(self): + return G(self.re, -self.im) + + def scale(self, s): + return G(self.re * Fraction(s), self.im * Fraction(s)) + + def __eq__(self, other): + other = _g(other) + return self.re == other.re and self.im == other.im + + def is_zero(self): + return self.re == 0 and self.im == 0 + + def key(self): + return (str(self.re), str(self.im)) + + def __repr__(self): + return f"({self.re}+{self.im}i)" + + +def _g(x): + return x if isinstance(x, G) else G(x) + + +def gi_pow(j): + """i^j for integer j, exact.""" + j %= 4 + return (G(1), G(0, 1), G(-1), G(0, -1))[j] + + +def popcount(x): + return bin(x).count("1") + + +# -------------------------------------------------------------------------- +# Structured appliers. Each returns (result_vector, opcount_dict). +# -------------------------------------------------------------------------- +def apply_diag(v, phases): + """Diagonal unit-phase restoration. Cost: one coefficient pass = N mults.""" + need(len(v) == len(phases), "diag dimension") + out = [p * x for p, x in zip(phases, v)] + return out, {"passes": 1, "mults": len(v), "adds": 0} + + +def apply_perm(v, perm): + """Permutation restoration. Cost: one routing pass = N moves, 0 mults.""" + need(sorted(perm) == list(range(len(v))), "perm not a permutation") + out = [v[perm[x]] for x in range(len(v))] + return out, {"passes": 1, "mults": 0, "adds": 0, "moves": len(v)} + + +def _walsh_dense(e): + n = 1 << e + H = [[G((-1) ** (popcount(x & y))) for y in range(n)] for x in range(n)] + return H + + +def apply_walsh_fast(v): + """Fast Walsh-Hadamard on e bits, then scale by 1/N = H^{-1}. + Cost: N*log2(N) adds and N mults (the 1/N scaling). Exact.""" + n = len(v) + need(n & (n - 1) == 0, "walsh length") + e = n.bit_length() - 1 + a = list(v) + adds = 0 + step = 1 + while step < n: + for i in range(0, n, 2 * step): + for j in range(i, i + step): + u, w = a[j], a[j + step] + a[j] = u + w + a[j + step] = u - w + adds += 2 + step *= 2 + scale = Fraction(1, n) + out = [x.scale(scale) for x in a] + return out, {"passes": 1, "mults": n, "adds": adds} + + +def apply_dense(M, v): + """Dense matrix-vector product. Cost: N^2 mults + N(N-1) adds.""" + n = len(v) + out = [] + mults = 0 + adds = 0 + for x in range(n): + acc = G(0) + for y in range(n): + acc = acc + M[x][y] * v[y] + mults += 1 + adds += 1 + out.append(acc) + adds -= 1 # N-1 additions per row + return out, {"passes": 1, "mults": mults, "adds": max(adds, 0), "dense": True} + + +# -------------------------------------------------------------------------- +# Linear algebra on exact matrices (used to build and verify compositions). +# -------------------------------------------------------------------------- +def mat_identity(n): + return [[G(1) if x == y else G(0) for y in range(n)] for x in range(n)] + + +def mat_diag(phases): + n = len(phases) + return [[phases[x] if x == y else G(0) for y in range(n)] for x in range(n)] + + +def mat_perm(perm): + n = len(perm) + return [[G(1) if perm[x] == y else G(0) for y in range(n)] for x in range(n)] + + +def mat_mul(A, B): + n = len(A) + out = [[G(0)] * n for _ in range(n)] + for x in range(n): + for k in range(n): + if A[x][k].is_zero(): + continue + a = A[x][k] + for y in range(n): + if B[k][y].is_zero(): + continue + out[x][y] = out[x][y] + a * B[k][y] + return out + + +def mat_vec(M, v): + n = len(v) + return [sum((M[x][y] * v[y] for y in range(n)), G(0)) for x in range(n)] + + +def mat_eq(A, B): + return all(A[x][y] == B[x][y] for x in range(len(A)) for y in range(len(A))) + + +def mat_nnz(M): + return sum(1 for row in M for c in row if not c.is_zero()) + + +# -------------------------------------------------------------------------- +# The recursion batch. +# +# State: D (data stream) and W (borrowed dirty workspace), both length N. +# A fixed source vector s (read-only) supplies each child's data increment. +# +# scratch-only child i : D' = D + B_i s , W' = G_i W +# reader child i : D' = D + B_i W , W' = G_i W (reads W) +# +# The inherited invariant restores W to its node-entry value w0 after EVERY +# child (eager). The deferred scheme lets W drift and restores it ONCE at the +# node exit via (G_r ... G_1)^{-1}. Observables are the final D and final W. +# -------------------------------------------------------------------------- +class Batch: + def __init__(self, n, e): + self.n = n + self.e = e + self.Walsh = _walsh_dense(e) + + def run_eager(self, w0, children): + """Restore W to w0 after each child. Returns (D, W, cost).""" + n = self.n + D = [G(0)] * n + W = list(w0) + cost = {"passes": 0, "mults": 0, "adds": 0, "moves": 0, "restoration_passes": 0} + for child in children: + kind = child["kind"] + Bvec = child["B"] + s = child["s"] + Gmat = child["G"] + inverse = child["Ginv"] # restoration operator G_i^{-1} + apply = child["apply_inverse"] # callable(v) -> (vec, cost) + if kind == "reader": + incr = _scalevec(Bvec, W) + else: + incr = _scalevec(Bvec, s) + D = _vecadd(D, incr) + W = mat_vec(Gmat, W) # child dirties the workspace + # eager restoration to w0 (equivalently apply G_i^{-1} to the + # just-dirtied W; both return exactly w0 when the invariant held). + W, rcost = apply(W) + _acc(cost, rcost) + cost["restoration_passes"] += 1 + return D, W, cost + + def run_deferred(self, w0, children, deferred_apply): + """No intermediate restoration; one composed restoration at exit. + + deferred_apply applies (G_r ... G_1)^{-1} to the drifted workspace using + whatever structure the composed operator RETAINS: a diagonal phase, a + permutation, or a dense matrix. This is where the cost result lives.""" + n = self.n + D = [G(0)] * n + W = list(w0) + cost = {"passes": 0, "mults": 0, "adds": 0, "moves": 0, "restoration_passes": 0} + for child in children: + kind = child["kind"] + Bvec = child["B"] + s = child["s"] + Gmat = child["G"] + if kind == "reader": + incr = _scalevec(Bvec, W) + else: + incr = _scalevec(Bvec, s) + D = _vecadd(D, incr) + W = mat_vec(Gmat, W) # no restoration here + # one composed restoration: (G_r ... G_1)^{-1} applied to drifted W + W, rcost = deferred_apply(W) + _acc(cost, rcost) + cost["restoration_passes"] += 1 + return D, W, cost + + +def _vecadd(a, b): + return [x + y for x, y in zip(a, b)] + + +def _scalevec(Bvec, v): + return [b * x for b, x in zip(Bvec, v)] + + +def _acc(total, delta): + for k in ("mults", "adds", "moves", "passes"): + total[k] = total.get(k, 0) + delta.get(k, 0) + + +# -------------------------------------------------------------------------- +# Operator construction helpers returning full child records. +# -------------------------------------------------------------------------- +def make_child(B, s, Gmat, Ginv_mat, apply_inverse, kind, inv_struct): + return { + "B": B, "s": s, "G": Gmat, + "Ginv": Ginv_mat, + "apply_inverse": apply_inverse, + "kind": kind, + "inv_struct": inv_struct, # ("diag",phases)|("perm",perm)|("walsh",e) + "composed_inverse_dense": None, + } + + +def build_phase_children(n, e, a_list): + """Scratch-only children whose restorations are diagonal unit phases.""" + children = [] + for a in a_list: + phases = [gi_pow(a * popcount(x)) for x in range(n)] + inv_phases = [p.conj() for p in phases] # unit phase inverse + Gmat = mat_diag(phases) + Ginv = mat_diag(inv_phases) + B = [G(1) for _ in range(n)] + s = [G(popcount(x) + 1) for x in range(n)] + apply_inv = lambda v, ph=inv_phases: apply_diag(v, ph) + children.append(make_child(B, s, Gmat, Ginv, apply_inv, "scratch", + ("diag", inv_phases))) + return children + + +def build_perm_children(n, e, shifts): + """Scratch-only children whose restorations are permutations (rotations).""" + children = [] + for sh in shifts: + perm = [((x + sh) % n) for x in range(n)] + inv_perm = [((x - sh) % n) for x in range(n)] + Gmat = mat_perm(perm) + Ginv = mat_perm(inv_perm) + B = [G(1) for _ in range(n)] + s = [G(x + 1) for x in range(n)] + apply_inv = lambda v, ip=inv_perm: apply_perm(v, ip) + children.append(make_child(B, s, Gmat, Ginv, apply_inv, "scratch", + ("perm", inv_perm))) + return children + + +def build_hetero_children(n, e): + """Scratch-only children with MIXED restoration families: a diagonal + phase, then a Walsh transform, then a permutation. Their composition is + dense and destroys the cheap structure.""" + phase = [gi_pow(popcount(x)) for x in range(n)] + inv_phase = [p.conj() for p in phase] + c0 = make_child([G(1)] * n, [G(popcount(x) + 1) for x in range(n)], + mat_diag(phase), mat_diag(inv_phase), + (lambda v, ph=inv_phase: apply_diag(v, ph)), "scratch", + ("diag", inv_phase)) + H = _walsh_dense(e) + # H^{-1} = (1/N) H + Hinv = [[c.scale(Fraction(1, n)) for c in row] for row in H] + c1 = make_child([G(1)] * n, [G(x + 1) for x in range(n)], + H, Hinv, + (lambda v: apply_walsh_fast(v)), "scratch", + ("walsh", e)) + sh = 1 + perm = [((x + sh) % n) for x in range(n)] + inv_perm = [((x - sh) % n) for x in range(n)] + c2 = make_child([G(1)] * n, [G(2) for _ in range(n)], + mat_perm(perm), mat_perm(inv_perm), + (lambda v, ip=inv_perm: apply_perm(v, ip)), "scratch", + ("perm", inv_perm)) + return [c0, c1, c2] + + +def build_reader_children(n, e): + """One scratch-only child then one READER child (reads W into D).""" + a_list = [1, 1] + children = build_phase_children(n, e, a_list) + children[1]["kind"] = "reader" + return children + + +# -------------------------------------------------------------------------- +# Compose the individual structured inverses; return a deferred_apply that uses +# the RETAINED structure, plus a description of what structure survived. +# -------------------------------------------------------------------------- +def _is_diag(M): + n = len(M) + for x in range(n): + for y in range(n): + if x != y and not M[x][y].is_zero(): + return False + return True + + +def _is_perm(M): + n = len(M) + for x in range(n): + row = [y for y in range(n) if not M[x][y].is_zero()] + if len(row) != 1 or M[x][row[0]] != G(1): + return False + cols = set() + for x in range(n): + col = [y for y in range(n) if not M[y][x].is_zero()] + if len(col) != 1: + return False + cols.add(col[0]) + return len(cols) == n + + +def compose_structured(children): + """Return (deferred_apply, description). + + The mathematically exact composed restoration is + (G_r ... G_1)^{-1} = G_1^{-1} ... G_r^{-1}, built as a dense product by + direct_composed_inverse. We then detect whether that exact product RETAINS + cheap structure: + + * diagonal -> a single unit-phase pass (N mults) + * permutation -> a single routing pass (moves, 0 mults) + * otherwise -> dense (N^2 mults) + + The structured form is derived from the exact dense product and then checked + to agree with it on the standard basis, so the cheap application is certified + against the exact operator rather than assumed.""" + n = len(children[0]["B"]) + dense = direct_composed_inverse(children) # exact G_1^{-1}...G_r^{-1} + if _is_diag(dense): + ph = [dense[x][x] for x in range(n)] + # self-check: diagonal application equals dense application + for x in range(n): + basis = [G(1) if y == x else G(0) for y in range(n)] + a, _ = apply_diag(basis, ph) + b = mat_vec(dense, basis) + need(_veceq(a, b), "diag structured != dense") + return (lambda v, p=ph: apply_diag(v, p)), {"form": "diag", "nnz": mat_nnz(dense)} + if _is_perm(dense): + perm = [0] * n + for x in range(n): + for y in range(n): + if not dense[x][y].is_zero(): + perm[x] = y + for x in range(n): + basis = [G(1) if y == x else G(0) for y in range(n)] + a, _ = apply_perm(basis, perm) + b = mat_vec(dense, basis) + need(_veceq(a, b), "perm structured != dense") + return (lambda v, p=perm: apply_perm(v, p)), {"form": "perm", "nnz": mat_nnz(dense)} + return (lambda v, M=dense: apply_dense(M, v)), {"form": "dense", + "nnz": mat_nnz(dense)} + + +def direct_composed_inverse(children): + """Return (G_r ... G_1)^{-1}. + + The workspace drifts as W_r = (G_r ... G_1) w0. Since + (G_r ... G_1)^{-1} = G_1^{-1} G_2^{-1} ... G_r^{-1}, we build the product in + forward child order: acc = G_1^{-1} G_2^{-1} ... G_r^{-1}. + Applying acc to W_r returns w0 exactly.""" + n = len(children[0]["B"]) + inv = mat_identity(n) + for child in children: # forward order + inv = mat_mul(inv, child["Ginv"]) # acc = acc * G_i^{-1} + return inv + + +# -------------------------------------------------------------------------- +# Main verification. +# -------------------------------------------------------------------------- +def verify(): + cert = {"base": BASE, "cases": {}} + n = 8 + e = 3 + batch = Batch(n, e) + w0 = [G(popcount(x) + 1, x % 3) for x in range(n)] + + # ---- Case 1: homogeneous phase restorations, read-free batch. ---- + phase_children = build_phase_children(n, e, [1, 2, 3]) + r = len(phase_children) + comp_inv = direct_composed_inverse(phase_children) + phase_defer, phase_desc = compose_structured(phase_children) + need(phase_desc["form"] == "diag", "phase composition should stay diagonal") + + D_e, W_e, cost_e = batch.run_eager(w0, phase_children) + D_d, W_d, cost_d = batch.run_deferred(w0, phase_children, phase_defer) + need(_veceq(D_e, D_d), "phase: data mismatch under deferral") + need(_veceq(W_d, w0), "phase: workspace not restored by deferral") + need(_veceq(W_e, w0), "phase: workspace not restored eagerly") + need(cost_e["restoration_passes"] == r, "phase: eager restoration count") + need(cost_d["restoration_passes"] == 1, "phase: deferred restoration count") + need(cost_d["mults"] < cost_e["mults"], "phase: deferral should cut mults") + cert["cases"]["phase"] = { + "children": r, + "composed_form": phase_desc["form"], + "eager_restoration_passes": cost_e["restoration_passes"], + "deferred_restoration_passes": cost_d["restoration_passes"], + "eager_mults": cost_e["mults"], + "deferred_mults": cost_d["mults"], + "mult_ratio": str(Fraction(cost_e["mults"], max(cost_d["mults"], 1))), + "observables_equal": True, + } + + # ---- Case 2: homogeneous permutation restorations, read-free batch. ---- + perm_children = build_perm_children(n, e, [1, 2, 4]) + r2 = len(perm_children) + perm_defer, perm_desc = compose_structured(perm_children) + need(perm_desc["form"] == "perm", "perm composition should stay a permutation") + D_e2, W_e2, cost_e2 = batch.run_eager(w0, perm_children) + D_d2, W_d2, cost_d2 = batch.run_deferred(w0, perm_children, perm_defer) + need(_veceq(D_e2, D_d2), "perm: data mismatch under deferral") + need(_veceq(W_d2, w0), "perm: workspace not restored by deferral") + need(cost_e2["restoration_passes"] == r2, "perm: eager restoration count") + need(cost_d2["restoration_passes"] == 1, "perm: deferred restoration count") + need(cost_d2["mults"] <= cost_e2["mults"], "perm: deferral should not raise mults") + cert["cases"]["perm"] = { + "children": r2, + "composed_form": perm_desc["form"], + "eager_restoration_passes": cost_e2["restoration_passes"], + "deferred_restoration_passes": cost_d2["restoration_passes"], + "eager_moves": cost_e2.get("moves", 0), + "deferred_moves": cost_d2.get("moves", 0), + "observables_equal": True, + } + + # ---- Case 3 (negative control, correctness): reader child breaks deferral. ---- + reader_children = build_reader_children(n, e) + reader_defer, _ = compose_structured(reader_children) + D_e3, W_e3, _ = batch.run_eager(w0, reader_children) + D_d3, W_d3, _ = batch.run_deferred(w0, reader_children, reader_defer) + need(_veceq(W_d3, w0), "reader: final workspace should still be restored") + need(not _veceq(D_e3, D_d3), "reader: deferral should CHANGE the data output") + diff = _vecsub(D_e3, D_d3) + need(any(not c.is_zero() for c in diff), "reader: expected nonzero discrepancy") + cert["cases"]["reader_negative"] = { + "observables_equal": False, + "discrepancy_nonzero": True, + "discrepancy": [c.key() for c in diff], + } + + # ---- Case 4 (negative control, cost): heterogeneous composition is dense. ---- + hetero = build_hetero_children(n, e) + comp_inv4 = direct_composed_inverse(hetero) + hetero_defer, hetero_desc = compose_structured(hetero) + need(hetero_desc["form"] == "dense", + "hetero: composed inverse should be dense (structure destroyed)") + # eager restoration cost = sum of structured inverse applications + eager_struct_cost = {"mults": 0, "adds": 0, "moves": 0, "passes": 0} + for c in hetero: + _, rc = c["apply_inverse"](list(w0)) + _acc(eager_struct_cost, rc) + # deferred restoration cost = one application of the composed inverse + _, dcost = hetero_defer(list(w0)) + nnz = mat_nnz(comp_inv4) + is_dense = nnz == n * n + D_e4, W_e4, cost_e4 = batch.run_eager(w0, hetero) + D_d4, W_d4, cost_d4 = batch.run_deferred(w0, hetero, hetero_defer) + need(_veceq(D_e4, D_d4), "hetero: data mismatch under deferral") + need(_veceq(W_d4, w0), "hetero: workspace not restored by deferral") + need(is_dense, "hetero: composed inverse should be dense") + need(dcost["mults"] >= eager_struct_cost["mults"], + "hetero: expected no mult elimination for dense composition") + cert["cases"]["hetero_negative"] = { + "children": len(hetero), + "composed_form": hetero_desc["form"], + "composed_inverse_nnz": nnz, + "composed_inverse_dense": is_dense, + "eager_structured_mults": eager_struct_cost["mults"], + "deferred_dense_mults": dcost["mults"], + "observables_equal": True, + "mult_elimination": False, + } + + cert["dimension_N"] = n + cert["e"] = e + cert["summary"] = ( + "phase=PASS perm=PASS hetero_dense=CONFIRMED reader_diverges=CONFIRMED" + ) + return cert + + +def _veceq(a, b): + return len(a) == len(b) and all(x == y for x, y in zip(a, b)) + + +def _vecsub(a, b): + return [x - y for x, y in zip(a, b)] + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--write", type=Path) + ap.add_argument("--json", action="store_true") + args = ap.parse_args() + + cert = verify() + phase = cert["cases"]["phase"] + perm = cert["cases"]["perm"] + reader = cert["cases"]["reader_negative"] + hetero = cert["cases"]["hetero_negative"] + + line = ( + "PASS_RESTORATION_COALESCING " + f"phase={phase['eager_restoration_passes']}->{phase['deferred_restoration_passes']}" + f"(x{phase['mult_ratio']}) " + f"perm={perm['eager_restoration_passes']}->{perm['deferred_restoration_passes']} " + f"hetero_dense={hetero['composed_inverse_dense']} " + f"reader_diverges={reader['observables_equal'] == False}" + ) + committed = ROOT / "CERTIFICATE.json" + if args.write is None and committed.exists(): + recorded = json.loads(committed.read_text()) + if json.dumps(recorded, sort_keys=True) != json.dumps(cert, sort_keys=True): + raise ValueError("recomputed certificate differs from committed CERTIFICATE.json") + print(line) + if args.json: + print(json.dumps(cert, indent=2, sort_keys=True)) + if args.write: + args.write.write_text(json.dumps(cert, indent=2, sort_keys=True)) + print(f"WROTE {args.write}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/reader-restoration-cuts-seed53/test_package.py b/research/reader-restoration-cuts-seed53/test_package.py new file mode 100644 index 0000000000..bc751283e8 --- /dev/null +++ b/research/reader-restoration-cuts-seed53/test_package.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +"""Relocated optimized CLI checks and four corruption controls. Apache-2.0.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def run(root, script, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(root / script), *map(str, args)], + cwd=root.parent, capture_output=True, text=True, timeout=30) + + +def main(): + with tempfile.TemporaryDirectory(prefix="reader-cuts-") as tmp: + copy = Path(tmp) / "package" + shutil.copytree(ROOT, copy, ignore=shutil.ignore_patterns("__pycache__")) + result = run(copy, "verify.py") + need(result.returncode == 0 and "PASS_READER_RESTORATION_CUTS" in result.stdout, result.stderr) + result = run(copy, "verify.py", "--json") + need(result.returncode == 0 and json.loads(result.stdout) == json.loads((copy / "CERTIFICATE.json").read_text()), + "relocated canonical regeneration") + result = run(copy, "planner.py", copy / "fixture.json") + need(result.returncode == 0 and json.loads(result.stdout)["cost"] == 1, "public planner CLI") + mutations = [ + ("CERTIFICATE.json", lambda s: s.replace('"cost": 1', '"cost": 2', 1), "saved certificate mismatch"), + ("sources/pr1155/verify.py", lambda s: s + "\n# changed source\n", "source hash"), + ("fixture.json", lambda s: s.replace('"reader": [-1]', '"reader": [1]', 1), "five-child construction"), + ("planner.py", lambda s: s.replace('"cost": cost, "cuts"', '"cost": cost + 1, "cuts"', 1), + "planner disagrees"), + ] + for path, change, message in mutations: + file = copy / path + original = file.read_text() + altered = change(original) + need(altered != original, "mutation did not change input") + file.write_text(altered) + result = run(copy, "verify.py") + file.write_text(original) + need(result.returncode != 0 and message in result.stderr, "mutation not rejected: " + path) + invalid = copy / "bad-input.json" + invalid.write_text('{"children": [], "prices": [1], "ignored": true}') + result = run(copy, "planner.py", invalid) + need(result.returncode != 0 and "unknown input fields" in result.stderr, "unknown CLI field accepted") + print("PASS_READER_CUT_PACKAGE relocation=PASS regeneration=PASS corruptions=4 cli_controls=1") + + +if __name__ == "__main__": + main() diff --git a/research/reader-restoration-cuts-seed53/verify.py b/research/reader-restoration-cuts-seed53/verify.py new file mode 100644 index 0000000000..1fc80c088c --- /dev/null +++ b/research/reader-restoration-cuts-seed53/verify.py @@ -0,0 +1,255 @@ +#!/usr/bin/env python3 +"""Independent literal-column and exhaustive-partition checks. Apache-2.0.""" +import argparse +import copy +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys + +ROOT = Path(__file__).resolve().parent + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def literal(children, prices, cuts, overhead=0): + """Replay every D/W input column; compare the whole state at each cut.""" + n = len(prices) + state = [[int(i == j) for j in range(2 * n)] for i in range(2 * n)] + eager = copy.deepcopy(state) + start, cost, negative = 0, 0, [] + for i, child in enumerate(children): + for j, (sign, reader) in enumerate(zip(child["signs"], child["reader"])): + state[j] = [x + reader * y for x, y in zip(state[j], state[n + j])] + state[n + j] = [sign * x for x in state[n + j]] + eager[j] = [x + reader * y for x, y in zip(eager[j], eager[n + j])] + if i + 1 in cuts: + negative = [] + for j in range(n): + sign = 1 + for child_back in reversed(children[start:i + 1]): + sign *= child_back["signs"][j] + if sign == -1: + negative.append(j) + state[n + j] = [-x for x in state[n + j]] + cost += sum(prices[j] for j in negative) + (overhead if negative else 0) + if state != eager: + return None + start = i + 1 + need(start == len(children), "literal word has no final checkpoint") + return cost + + +def brute(children, prices, required=(), overhead=0): + r = len(children) + if not r: + return (0, 0, ()), 1 + best, count = None, 0 + for mask in range(1 << (r - 1)): + cuts = tuple(i + 1 for i in range(r - 1) if mask >> i & 1) + (r,) + if not set(required) <= set(cuts): + continue + count += 1 + cost = literal(children, prices, cuts, overhead) + if cost is not None: + key = cost, len(cuts), cuts + if best is None or key < best: + best = key + return best, count + + +def checked_plan(planner, data): + actual = planner.plan(**data) + expected, count = brute(**data) + key = actual["cost"], len(actual["cuts"]), tuple(actual["cuts"]) + need(key == expected, "planner disagrees with independent partition enumeration") + need(literal(data["children"], data["prices"], actual["cuts"], data.get("overhead", 0)) == actual["cost"], + "plan failed complete-column replay") + previous = 0 + for segment in actual["segments"]: + need(segment["start"] == previous and segment["stop"] > previous, "segment endpoints") + chunk = data["children"][previous:segment["stop"]] + negative = [j for j in range(len(data["prices"])) + if sum(c["signs"][j] == -1 for c in chunk) % 2] + need(segment["negate"] == negative, "wrong emitted restoration") + need(segment["cost"] == sum(data["prices"][j] for j in negative) + + (data.get("overhead", 0) if negative else 0), "unpaid emitted restoration") + previous = segment["stop"] + return actual, count + + +def source_replay(): + pins = json.loads((ROOT / "SOURCES.json").read_text()) + for path, digest in pins["files"].items(): + need(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == digest, "source hash: " + path) + old = load("retained_pr1155", ROOT / "sources/pr1155/verify.py") + need(json.loads(json.dumps(old.verify())) == json.loads((ROOT / "sources/pr1155/CERTIFICATE.json").read_text()), + "retained certificate no longer reproduces") + children = [] + for b in (1, 1, 1, -1, 1): + phases = [old.G(-1)] + child = old.make_child([old.G(b)], [old.G(0)], old.mat_diag(phases), + old.mat_diag(phases), lambda v: old.apply_diag(v, [old.G(-1)]), + "reader", ("diag", phases)) + children.append(child) + batch = old.Batch(1, 0) + apply, _ = old.compose_structured(children) + probes = [old.G(1), old.G(0, 1), old.G(7, -3)] + for w in probes: + de, we, ce = batch.run_eager([w], children) + dd, wd, cd = batch.run_deferred([w], children, apply) + need(de[0] == dd[0] == old.G(3) * w and we[0] == wd[0] == w, "retained reader witness") + need(ce["mults"] == 5 and cd["mults"] == 1, "retained restoration invoice") + return {"old_certificate": "PASS", "probes": len(probes), "eager_mults": 5, "deferred_mults": 1} + + +def scalar_invoice(children, result): + data, workspace = 11, 7 + counts = {"data_reads": 0, "coefficient_reads": 0, "data_writes": 0, + "multiplies": 0, "adds": 0, "negations": 0, "program_records": 0} + word = [] + restore = {s["stop"]: s["negate"] for s in result["segments"]} + for i, child in enumerate(children): + b, g = child["reader"][0], child["signs"][0] + data += b * workspace + workspace *= g + word.append(("child", b, g)) + counts["data_reads"] += 2 + counts["coefficient_reads"] += 2 + counts["data_writes"] += 1 + (g == -1) + counts["multiplies"] += 1 + counts["adds"] += 1 + counts["negations"] += g == -1 + counts["program_records"] += 1 + if restore.get(i + 1): + need(restore[i + 1] == [0], "scalar restore mask") + workspace = -workspace + word.append(("restore",)) + counts["data_reads"] += 1 + counts["data_writes"] += 1 + counts["negations"] += 1 + counts["program_records"] += 1 + need((data, workspace) == (32, 7), "literal scalar result") + for event in reversed(word): + if event[0] == "restore": + workspace = -workspace + else: + _, b, g = event + workspace *= g + data -= b * workspace + need((data, workspace) == (11, 7), "literal inverse") + return counts + + +def verify(): + retained = source_replay() + planner = load("restoration_cut_planner", ROOT / "planner.py") + fixture = json.loads((ROOT / "fixture.json").read_text()) + chosen, _ = checked_plan(planner, fixture) + need(chosen["cost"] == 1 and chosen["cuts"] == [5], "five-child construction") + forced = dict(fixture, required=[2]) + observed, _ = checked_plan(planner, forced) + need(observed["cost"] == 5, "observation boundary must remove saving") + eager = planner.plan(fixture["children"], [1], required=[1, 2, 3, 4, 5]) + invoice = {"eager": scalar_invoice(fixture["children"], eager), + "deferred": scalar_invoice(fixture["children"], chosen), + "input_D": 11, "input_W": 7, "output_D": 32, "output_W": 7, + "common_sufficient_signed_bits": 7} + + batches = partitions = 0 + alphabet = [{"reader": [b], "signs": [g]} for g in (-1, 1) for b in (-1, 0, 1)] + for r in range(5): + for word in itertools.product(alphabet, repeat=r): + _, count = checked_plan(planner, {"children": list(word), "prices": [1]}) + batches += 1 + partitions += count + scalar = {"batches": batches, "partitions": partitions, "max_children": 4} + + alphabet2 = [{"reader": list(b), "signs": list(g)} + for g in itertools.product((-1, 1), repeat=2) + for b in itertools.product((-1, 0, 1), repeat=2)] + batches = partitions = 0 + for word in itertools.product(alphabet2, repeat=2): + _, count = checked_plan(planner, {"children": list(word), "prices": [2, 5], "overhead": 3}) + batches += 1 + partitions += count + two_coordinate = {"batches": batches, "partitions": partitions} + + rng = random.Random(53) + partitions = 0 + for trial in range(160): + n, r = 1 + trial % 3, 5 + trial % 4 + data = {"children": [{"signs": [rng.choice((-1, 1)) for _ in range(n)], + "reader": [rng.randrange(-3, 4) for _ in range(n)]} for _ in range(r)], + "prices": [rng.randrange(1, 10) for _ in range(n)], + "required": [i for i in range(1, r + 1) if rng.randrange(5) == 0], + "overhead": rng.randrange(4)} + _, count = checked_plan(planner, data) + partitions += count + + controls = [] + changed = copy.deepcopy(fixture) + changed["children"][3]["reader"] = [1] + changed_plan, _ = checked_plan(planner, changed) + need(changed_plan["cost"] == 5, "broken cancellation must cost five") + controls += ["changed reader destroys cancellation", "checkpoint after child two destroys saving"] + need(literal(fixture["children"], [1], [2, 5]) is None, "unchecked intermediate cut accepted") + controls.append("final equality does not authorize an intermediate cut") + read_first = [{"reader": [1], "signs": [-1]}, {"reader": [0], "signs": [-1]}] + read_last = [{"reader": [0], "signs": [-1]}, {"reader": [1], "signs": [-1]}] + need(planner.plan(read_first, [1])["cost"] == 0 and planner.plan(read_last, [1])["cost"] == 2, + "reader order boundary") + controls.append("same children in a different order lose cancellation") + mutations = [dict(fixture, prices=[0]), dict(fixture, prices=[True]), + dict(fixture, required=[0]), dict(fixture, required=[6]), + dict(fixture, required=[2, 2]), dict(fixture, overhead=-1), + dict(fixture, children=[{"signs": [0], "reader": [1]}]), + dict(fixture, children=[{"signs": [-1], "reader": [1, 2]}]), + dict(fixture, children=[{"signs": [-1], "reader": [1.0]}])] + for bad in mutations: + try: + planner.plan(**bad) + except ValueError: + continue + raise ValueError("invalid input accepted") + return {"status": "PASS_READER_RESTORATION_CUTS", "base": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "seed": 53, "fixture": chosen, "forced_cut_2": observed, + "scalar_instruction_invoice": invoice, + "retained_pr1155": retained, "scalar_exhaustion": scalar, + "two_coordinate_exhaustion": two_coordinate, + "seeded_longer": {"batches": 160, "partitions": partitions, "max_children": 8, "max_dimension": 3}, + "mathematical_controls": controls, "invalid_input_controls": len(mutations), + "scope": "exact diagonal readers and signs; every chosen cut matches eager data and workspace; no new kappa"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json", action="store_true", help="print recomputed certificate without comparing saved certificate") + args = parser.parse_args() + try: + result = verify() + if args.json: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(result == json.loads((ROOT / "CERTIFICATE.json").read_text()), "saved certificate mismatch") + print("PASS_READER_RESTORATION_CUTS restoration=5->1 forced_cut=5 exhaustive=2851 seeded=160") + except (OSError, ValueError, TypeError, KeyError) as exc: + parser.exit(1, "FAIL_READER_RESTORATION_CUTS: " + str(exc) + "\n") + + +if __name__ == "__main__": + main() From 85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 01:27:47 +0530 Subject: [PATCH 2/2] Record completed reader restoration claim and PR handoff --- .../reader-restoration-cuts-seed53/CLAIM.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/research/reader-restoration-cuts-seed53/CLAIM.md b/research/reader-restoration-cuts-seed53/CLAIM.md index e88a661cee..d81020062d 100644 --- a/research/reader-restoration-cuts-seed53/CLAIM.md +++ b/research/reader-restoration-cuts-seed53/CLAIM.md @@ -65,3 +65,20 @@ Prior PR1168's pending-output fanout cap is a different query alphabet. Stop if a matching planner or correction appears, or if no useful checked artifact is ready by the verification deadline. At most one pivot, with the original clock unchanged. Recheck overlap at first result and before submission. + +## Result and release + +Completed with [PR1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199). +Five nonzero readers admit one restoration instead of five. An observation after +child two removes the saving. The package supplies a written criterion and +restricted optimum, the cut planner, the exact complete-node accounting model, +and an independent literal-column enumeration of 19,167 partitions across 3,011 +declared batches. The retained PR1155 certificate also reproduces unchanged. +No new kappa, adopted supplier or runtime improvement is claimed. + +Verification and handoff started by 19:52:45 UTC. All relevant checks in +VALIDATION.md pass. Final overlap at 19:56:39 UTC covered 808 open PRs through +1196 and all active discussions; no matching correction or planner appeared. +Upstream main was freshly fetched again and remained +`1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`, the original investigation base. +No pivot. This scope is complete; do not rerun it as a new experiment.