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..d81020062d --- /dev/null +++ b/research/reader-restoration-cuts-seed53/CLAIM.md @@ -0,0 +1,84 @@ +# 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. + +## 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. 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()