diff --git a/research/invariant-reader-restoration/CERTIFICATE.json b/research/invariant-reader-restoration/CERTIFICATE.json new file mode 100644 index 0000000000..ce2bd9a803 --- /dev/null +++ b/research/invariant-reader-restoration/CERTIFICATE.json @@ -0,0 +1,377 @@ +{ + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "catalytic_wrapper": { + "B_adds_each_direction": 16, + "basis_cases": 19, + "deferred_program_sha256": "280ee0e780a711c4a303c04045c7d218634d13dae5e8aea23702834d3185bc8f", + "eager_program_sha256": "84bb9f6d45cad1deaac111d427626210682b9778bb60d0652bf863cc78c92c9f", + "invoice_deferred": { + "add_instructions": 150, + "scalar_additions": 450, + "source_reads": 300, + "tape_word_travel": 4504, + "target_reads": 150, + "target_writes": 150 + }, + "invoice_eager": { + "add_instructions": 210, + "scalar_additions": 630, + "source_reads": 420, + "tape_word_travel": 5864, + "target_reads": 210, + "target_writes": 210 + }, + "mixed_cases": 1, + "pre_read_adds": 5, + "source_addresses": [ + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19 + ], + "source_matrix": "B x has coordinate x[j] + x[(j+1) mod 8]" + }, + "finite_census": { + "basis_vectors_per_semantics": 2, + "cases": 5832, + "children": 3, + "dimension": 2, + "independent_output_accepted": 2592, + "permutation_alphabet_size": 2, + "reader_alphabet": [ + -1, + 0, + 1 + ], + "shared_final_output_accepted": 2772, + "shared_only_cancellation_cases": 180, + "stopping_rule": "exhaust all 2^3 * 9^3 cases" + }, + "fixture": { + "clean_accumulator_registers": 1, + "clean_temp_registers_in_data": 1, + "composed_permutation": [ + 6, + 5, + 4, + 7, + 2, + 1, + 0, + 3 + ], + "input_basis_cases": 11, + "mixed_or_zero_cases": 2, + "permutations_new_from_old": [ + [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + [ + 3, + 0, + 1, + 2, + 7, + 4, + 5, + 6 + ], + [ + 4, + 5, + 6, + 7, + 0, + 1, + 2, + 3 + ] + ], + "prefix_permutations": [ + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + [ + 1, + 0, + 3, + 2, + 5, + 4, + 7, + 6 + ], + [ + 2, + 1, + 0, + 3, + 6, + 5, + 4, + 7 + ] + ], + "reader_defects": [ + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + "readers": [ + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ] + ] + }, + "format": "invariant-reader-restoration-v1", + "independent_symbolic_check": { + "arbitrary_input_coordinates": 19, + "deferred": { + "invoice": { + "add_instructions": 150, + "scalar_additions": 450, + "source_reads": 300, + "tape_word_travel": 4504, + "target_reads": 150, + "target_writes": 150 + }, + "prefix_coefficient_l1_bounds": { + "accumulator": 3, + "outputs": 5, + "sources": 1, + "temporary": 3, + "workspace": 3 + } + }, + "eager": { + "invoice": { + "add_instructions": 210, + "scalar_additions": 630, + "source_reads": 420, + "tape_word_travel": 5864, + "target_reads": 210, + "target_writes": 210 + }, + "prefix_coefficient_l1_bounds": { + "accumulator": 3, + "outputs": 5, + "sources": 1, + "temporary": 3, + "workspace": 3 + } + }, + "permutation_cases": 873, + "permutation_widths": [ + 1, + 2, + 3, + 4, + 5, + 6 + ], + "symbolic_map_sha256": "ab8d2ab8074e9dfe0948843974c01abb4a51c8664ddd3f60654bf3f6c7c155d1" + }, + "invoice_deferred": { + "add_instructions": 113, + "scalar_additions": 339, + "source_reads": 226, + "tape_word_travel": 2652, + "target_reads": 113, + "target_writes": 113 + }, + "invoice_eager": { + "add_instructions": 173, + "scalar_additions": 519, + "source_reads": 346, + "tape_word_travel": 4012, + "target_reads": 173, + "target_writes": 173 + }, + "negative_controls": { + "backend_contract_rejections": 3, + "dropped_scalar_charge": { + "actual_add_instructions": 113, + "unpaid_claim": 112 + }, + "incompatible_reader": { + "defect": [ + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "deferred_outputs": [ + 1, + 0, + 1 + ], + "eager_outputs": [ + 1, + 1, + 1 + ], + "input_workspace": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "missing_catalytic_pre_reads": [ + 1, + 1, + 1 + ], + "missing_final_restore": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + "missing_inverse_B": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "missing_reader": [ + 0, + 1, + 1 + ], + "shared_target_cancellation": [ + [ + 0, + 0 + ], + [ + -1, + 1 + ], + [ + 1, + -1 + ] + ], + "wrong_inverse_order": [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + "zero_workspace_hides_bad_reader": true + }, + "programs": { + "categories": { + "deferred": { + "forward": 84, + "reader": 5, + "restore": 24 + }, + "eager": { + "forward": 84, + "reader": 5, + "restore": 84 + } + }, + "deferred_adds": 113, + "deferred_sha256": "c004856945711962c5dfc68c9ada43606439319b9b69d721bc99c2e990eef51e", + "eager_adds": 173, + "eager_sha256": "74af53b74abfe5d5bba37b67d94421ba6bf914218d64eb5f58a2d9e391c27276" + }, + "seed": 50, + "source_pins_sha256": "b6df9725d08031d48c41274d06539368c9398ca8b9c47cde2bb681a81dc1487c", + "status": "exact scoped interface and finite literal invoice; no new kappa" +} diff --git a/research/invariant-reader-restoration/CLAIM.md b/research/invariant-reader-restoration/CLAIM.md new file mode 100644 index 0000000000..18a3bc045e --- /dev/null +++ b/research/invariant-reader-restoration/CLAIM.md @@ -0,0 +1,60 @@ +# Local sprint claim + +- Track: recursive interfaces; OS-random assignment seed **50**. +- Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. +- Start: 2026-10-13 19:39 UTC; expected finish: 20:19 UTC. +- Scope: eliminate per-child permutation restoration while retaining nonzero, + invariant linear reads of arbitrary dirty workspace. Prove the exact reader + compatibility condition and price a three-child, eight-coordinate fixture. +- Method: exact rational matrix identities plus an independently checked + in-place permutation/read interpreter. General typed recurrence; no kappa claim. +- Deliverable: one scoped note, deterministic certificate, verifier and negative controls. +- Stop rule: stop construction if the fully paid fixture cannot save work; do + not search different architectures. Reserve 20:09--20:19 UTC for verification. + +## Three candidates considered + +1. Higher-arity exact dirty-port borrowing: overlaps directly with PR1057 and + fresh PR1164, so not selected. +2. Extend the universal five-source connector with another operation: the + accepted 945-pairing obstruction already closes the unchanged alphabet; + no concrete paid extension within this session, so not selected. +3. Restoration deferral with nonzero invariant readers: selected. PR1155's + read-free proposal explicitly excludes readers; test a strictly larger, + precisely typed interface using invariant subspaces instead of more search. + +Seed 50 selects three children (2 + 50 mod 7) and eight coordinates +(2 ** (1 + 50 mod 3)); the method is a direct algebraic construction, not a +random search. This selection is meaningful because it tests observable reads, +which the nearest proposal treats as obstructing deferral. + +## Overlap and accepted context + +Read AGENTS.md, autoresearch.md, CONTRIBUTING.md, the selected certificate, +current status, central PR ledger, selected #1094 construction/manifest/assembly +and maintainer review. Selected conditional kappa is +836330098538459/500000000000000000; complex is binding in that assembly. +No supplier admission or frontier edit is proposed. + +Live open-PR inventory: 786 items. Read precise PR1155, PR1057, PR1164 metadata; +PR1155 head: `9821c6e9388f3fc097e94b72be9fa7b41a849527` (Navinor/Aaron Wang). +Read the accepted universal-connector-boundary and additive-cyclic-no-connector +notes. The invariant-read criterion is a different question from recursive +pool allocation, fixed connector alphabets and hosted restoration rank mass. +Pinned-issue query returned no issues. Discussion board contained only +#1163/#1166/#1167 and no claims at the entry check. The user explicitly provides +for a local claim when no pinned coordination issue exists; no reservation +issue is created. Recheck overlap before submitting. + +Prepared for mightyOil (Philipp), with substantial OpenAI Codex assistance. +Apache-2.0. No independent human review or full theorem verification claimed. + +## Final overlap finding + +The last check found Sagar Thakrar's concurrent #1199 (created 19:57:26 UTC), +head `85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d`. Its pinned README was inspected. +It gives the same necessity correction, a diagonal-sign checkpoint planner and +the general summed-defect identity. Submission is therefore labeled independent +corroboration with distinct noncommuting/permutation, distinct-output, +dirt-independent wrapper and literal scalar/tape coverage. No priority for the +correction or general identity is claimed. No second investigation was launched. diff --git a/research/invariant-reader-restoration/NOTICE.md b/research/invariant-reader-restoration/NOTICE.md new file mode 100644 index 0000000000..40a33613bb --- /dev/null +++ b/research/invariant-reader-restoration/NOTICE.md @@ -0,0 +1,20 @@ +New research note, verifier and scalar backend: prepared for mightyOil (Philipp) +with substantial OpenAI Codex assistance, including scoped Codex subagent work. +Licensed under the repository's Apache License 2.0 (../../LICENSE). + +sources/PR1155-README.md is retained byte-for-byte from Navinor / Aaron Wang, +with opencode assistance, PR1155 head 9821c6e9388f3fc097e94b72be9fa7b41a849527. +Its original Apache-2.0 attribution and content remain intact. It is prior work, +not an accepted premise for its claimed necessary read-free condition. + +sources/BASE-SELECTED.json retains the repository's selected record at base +1b59b624d21924f8e3537cdc1ac52d3be6eda2fe, including cumulative contributor and +source references. It is context, not a newly verified frontier certificate. + +No predecessor code is imported. Exact file hashes and Git blobs are recorded +in SOURCE-PINS.json. The README gives predecessor and concurrent credit. + +Concurrent PR1199 by Sagar Thakrar, with OpenAI Codex assistance, independently +provides the same necessity correction and a diagonal checkpoint planner. +Its README was inspected at 85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d. +No code was imported and no priority for that correction is claimed here. diff --git a/research/invariant-reader-restoration/README.md b/research/invariant-reader-restoration/README.md new file mode 100644 index 0000000000..b884fdff76 --- /dev/null +++ b/research/invariant-reader-restoration/README.md @@ -0,0 +1,315 @@ +# Reader-compatible restoration deferral + +**Research note / exact recursive interface; no new kappa.** Nonzero reads of +borrowed workspace need not prevent deferring its restoration. The precise +condition is that each read annihilates the accumulated drift. A fully expanded +example, including cancellation of incoming dirt and both source calls, reduces +**210 to 150 two-address ADD instructions**, and **5,864 to 4,504 data-tape word +transitions**, for the same fixed borrowing interface. Preparation and control +costs are separately and explicitly charged below; these counts are not a +runtime benchmark or an optimal circuit claim. + +This refines Navinor's [PR1155](https://github.com/CrocSwap/integer-mult-bounds/pull/1155) +at `9821c6e9388f3fc097e94b72be9fa7b41a849527`. Its retained +[original note](sources/PR1155-README.md) states that read-freedom is necessary +and sufficient and uses one failing reader as evidence of necessity. That +counterexample shows that **some** readers fail, not that **every** reader fails. +The construction here has compatible readers after actual nonidentity drift. +PR1155's shared-final-target observability also admits a weaker cancellation +condition, distinguished below. No assertion is made about its executable +fixtures beyond the statement inspected in that pinned note. + +Concurrent [PR1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199) +by Sagar Thakrar at `85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d` independently +corrects the same necessity claim, supplies a diagonal-sign checkpoint planner, +and states the general summed-defect identity. **No priority is claimed for +that correction or the prefix-defect identity.** This package adds separate +noncommuting-permutation evidence, distinct-output admission, an explicitly +dirt-independent shared-B wrapper, and a separately implemented symbolic +scalar/tape invoice. It does not reproduce or supersede PR1199's cut planner. +The exact concurrent source was inspected at the final submission check; +its results are credited, not silently treated as our discovery. + +## Reproduce + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -I -O -B research/invariant-reader-restoration/verify.py +``` + +Expected: + +```text +PASS_INVARIANT_READER_RESTORATION cases=5832 wrapped_adds=210->150 no_new_kappa +``` + +The command verifies retained source hashes, recomputes every certificate field, +and compares against [CERTIFICATE.json](CERTIFICATE.json). Required checks use +explicit exceptions and remain active with `-O`. The companion command +`python3 -I -O -B research/invariant-reader-restoration/test_package.py` checks +relocation, deterministic export and deliberate on-disk corruptions. Neither +command regenerates selected or upstream artifacts. `--write PATH` is explicitly +an authoring/export mode, not acceptance against the committed certificate. + +## Exact typed interface and proof + +Work over the rationals, with all arithmetic exact. Let `z` be arbitrary borrowed +workspace, `y_i` distinct arbitrary output accumulators, and `G_i` fixed invertible +linear workspace maps. A child first performs `y_i += H_i z`, then `z <- G_i z`. +All coefficients are immutable; no output aliases workspace or another output. +Readers are target-independent, and private scratch and tape positions used by +complete child operations are restored. The code specializes `G_i` to permutations +and `H_i` to rows with coefficients in `{-1,0,1}`. + +The eager contract follows each child with `G_i^-1`. The deferred contract +omits these restorations and applies `(G_r ... G_1)^-1` once at batch exit. Put +`P_0 = I`, `P_j = G_j ... G_1`. Then: + +- Eager output `i` is `y_i^0 + H_i z_0`. +- Deferred output `i` is `y_i^0 + H_i P_(i-1) z_0`. +- Both final workspaces are `z_0`. + +Consequently, equality for **all incoming dirty states** is equivalent to + +```text +H_i (P_(i-1) - I) = 0 for every i. (1) +``` + +Sufficiency follows by subtraction. For necessity, a nonzero defect matrix has +a nonzero column; the corresponding standard basis workspace is a counterexample. +This is an all-size algebraic proof, not an inference from the finite census. +For permutation prefixes, each reader row must be constant on each cycle of +that prefix. It need not be invariant under every individual `G_j`, and it need +not vanish. The condition concerns the actual chronological prefix. + +**One shared output at batch exit.** If all readers update the same accumulator, +only their summed defect must vanish: + +```text +sum_i H_i (P_(i-1) - I) = 0. (2) +``` + +For `G_1 = swap(0,1)`, `G_2 = G_3 = I`, and readers `0,e_0,e_1`, the individual +defects are `0,(-1,1),(1,-1)`. Condition (2) holds while (1) fails. If the shared +output is observable after every child, equality of consecutive partial sums +again forces each individual defect to vanish. Thus observability is a material +part of the contract; no general "one reader breaks it" theorem follows. + +## Returning arbitrary dirty workspace without exposing it + +Reading preserved input state is not by itself a catalytic scratch contract: +outputs must be independent of borrowed dirt. Supply a read-only source `x` +and a complete, exact additive call `B: z += Bx`, independent of the old target. +Its inverse is `z -= Bx`; both restore private scratch. Execute: + +1. Pre-read `y_i -= H_i z` for every output. +2. Call `B` to obtain `z_1 = z_0 + Bx`. +3. Execute either compatible reader/permutation batch above. +4. Call the complete inverse `B` after batch restoration. + +The output is `y_i^0 - H_i z_0 + H_i(z_0+Bx) = y_i^0 + H_i Bx`, and final +workspace is exactly `z_0`. Source `x` is unchanged. All `x,z,y_i` ports are +pairwise disjoint and excluded from private child scratch. The routing temporary +and source accumulator are **two admitted clean scalars**, separately charged; +no clean workspace row is assumed. Readers of other live state, nonlinear or +rounded B calls, data-dependent permutations and intermediate observation during +the pre-read/load sandwich are outside this contract. + +The same proof holds for rows of any common length `L`, with `G_i` replaced by +`G_i tensor I_L` and the corresponding block readers. It does not construct a +selected supplier or discharge the repository's physical recursive interfaces. + +## Noncommuting eight-coordinate fixture + +Use old-coordinate-to-new-coordinate cycle notation: + +```text +G_1 = (01)(23)(45)(67) +G_2 = (0123)(4567) +G_3 = (04)(15)(26)(37) +H_1 = e_0, H_2 = e_0 + e_1, H_3 = e_0 + e_2. +``` + +The first two maps do not commute. `P_2 = (02)(46)` and +`P_3 = (06)(15)(24)(37)`. Each reader satisfies (1); the latter two read +workspace that has actually drifted. Both have nonzero dependence on the +original workspace. The catalytic wrapper uses +`(Bx)_j = x_j + x_((j+1) mod 8)`; B need not be invertible or commute with G. +The certificate spells out gather permutations `new[j] = old[p[j]]`, avoiding +ambiguity between cycle and index-array conventions. + +The matrix checker uses dense exact products. The separately implemented +[backend](backend.py) instead composes index arrays, decomposes cycles, emits +scalar instructions and literally loads/unloads its clean accumulator. On every +basis of the 19 arbitrary source/workspace/output coordinates (plus a mixed +case), both complete wrapper programs implement `y_i += H_i Bx`, preserve all +source/workspace coordinates, restore the temporary, and have a working literal +reverse-inverse. This is finite evidence for the actual emitted fixture; the +universal identity is proved above. + +## Complete invoice and recurrence + +A two-address ADD `d += sign*s`, with distinct ports, expands as +`A += memory[s]; memory[d] += sign*A; A -= memory[s]`. Its source is unchanged, +so A returns to zero. It pays two source reads, one target read, one target +write and three scalar additions/subtractions. The data head traverses +`0 -> s -> d -> s -> 0`, paying `2*s + 2*abs(d-s)` word transitions. The scalar +A is separately located in a fixed arithmetic workspace; arithmetic/read/write +macro costs include their internal access and scratch restoration. + +Each permutation cycle is implemented by swaps. A swap uses an initially zero +scalar T and these **six**, fully charged, distinct-port shears: + +```text +T += a; a -= T; a += b; b -= a; b += T; T -= b. +``` + +It returns `(a,b,T)` as `(b,a,0)`. A k-cycle uses `k-1` swaps. Here the forwards +use 14 swaps, eager inverses another 14, and the composed inverse four. There +is no free array copy, hidden permutation, erased scratch or unpaid inverse. +The full wrapper has two 16-ADD B calls and ten reader ADDs. + +| Complete wrapper charge | Eager | Deferred | +|---|---:|---:| +| Forward-permutation ADDs | 84 | 84 | +| Restoration ADDs | 84 | 24 | +| Both B calls | 32 | 32 | +| Pre-reads and batch reads | 10 | 10 | +| **Two-address ADD instructions** | **210** | **150** | +| Scalar additions/subtractions | 630 | 450 | +| Source reads | 420 | 300 | +| Target reads / target writes | 210 / 210 | 150 / 150 | +| Data-tape word transitions | 5,864 | 4,504 | + +Workspace addresses are 0..7, outputs 8..10, T is 11, and immutable source +addresses are 12..19. A is outside that data tape. The instruction stream has +one fixed-width `(opcode,d,s,sign)` record per ADD; both programs use the same +address width. Each event reads one record and returns the data head. Thus +instruction reads, control dispatch and address decoding must be paid 210 and +150 times, respectively, at the same declared per-record cost. No instruction +or coefficient-access cost is claimed to be zero. + +For integer scalar inputs of magnitude less than `2^p`, every workspace value during the +wrapper has magnitude at most `3*2^p`; during swaps it is either one of these +values or zero. An intermediate output is bounded by `9*2^p`, and A loads only +workspace, source or T. Signed width `b = p+5` therefore suffices without +rounding. Allocation includes 20 data words and A, plus instruction storage, +address/control counters and the scratch required by the chosen exact scalar +arithmetic backend. This bound is about this fixture, not a floating-point +precision contract or a fixed-tape multiplication implementation. + +For event-count `K`, scalar-add count `S`, word travel `J`, and word width b, +a complete parametrized online bill is + +```text +W(program;b) = S*c_add(b) + 3K*c_read(b) + K*c_write(b) + + b*J*c_move + K*c_dispatch(b, address_width). +``` + +Here read/write costs include intra-word scans and return to a word boundary; +`c_add` includes arithmetic scratch restoration and scalar register updates; +`c_dispatch` includes instruction-record access, decoding and counter work. +No backend numerical timings are inferred. Online saving for the fixture is +`180*c_add + 180*c_read + 60*c_write + 1360*b*c_move + 60*c_dispatch`. +Startup allocation/zeroing of the two clean scalars is paid in admission `I`. + +For a general node, let `C_B^+/-` be complete recursive source-call costs, +`R_H^-/+` complete reader costs, `Q(G)` complete routing costs, `P_S` program and +coefficient preparation, and `D_S` dispatch/control not already included. With +no double counting of these terms, the recurrences are + +```text +T_E = I + P_E + C_B^+ + C_B^- + R_H^- + R_H^+ + + sum_i [Q(G_i) + Q(G_i^-1)] + D_E, +T_D = I + P_D + C_B^+ + C_B^- + R_H^- + R_H^+ + + sum_i Q(G_i) + Q(P_r^-1) + D_D. +``` + +If `C_B^sign(L) = sum_j C_child(j,sign)(L_j) + A_B^sign(L)`, substitute the +**entire** recurrence in both occurrences. All children, coefficient and source +access, frame conversions, copies, private restoration and tape return belong +in those terms. No child is eliminated by this argument. A caller requiring a +new frame or external layout conversion must add it; this fixture stays in one +fixed coordinate layout. Recursive children may not borrow the live rows. + +Preparation is not free: composing explicit n-entry permutation descriptors +uses `r*n` index lookups and stores (24 of each here), plus validation, inverse +construction, cycle extraction and instruction emission. General descriptors +are not composable in merely `O(r)` work. Budget `O(r*n*log(n+1))` bit work for +index manipulation, in addition to validation/coefficient preparation and +writing the full instruction stream. The implementation computes the product +in both modes to return admission metadata; a lean eager implementation could +omit those 24 updates. We do not use this avoidable baseline work as a saving. +For `M` invocations of a prepared fixed program, pay `I + P_S + M*W_S`. +For a single call, the extra preparation must be smaller than the displayed +online saving before claiming a total speedup. Neither M nor that tradeoff is +silently assumed. The full parametrized bill makes this boundary explicit. + +Directly computing `H_i Bx` can be cheaper than either wrapper in this toy +fixture. This is a legal replacement and correction within a fixed borrowing +interface, **not** a minimum over arbitrary circuits, a claim that a new +supplier is profitable, or a way to increase kappa from operation counts. + +## Coverage, failures and limits + +A further [separate symbolic checker](independent_check.py), included in the +one-command replay, does not import the matrix criterion or backend execution +engine. It checks all 873 permutations of widths 1 through 6 against the emitted +forward words, then reconstructs both full wrapper maps using integer coefficient +vectors. It independently derives every invoice field and bounds all intermediate +coefficient L1 norms: workspace/T/A at most 3, outputs at most 5, source at most 1. +The conservative integer-width allowance above is therefore sufficient. Its +symbolic-map digest and exact bounds are retained in the certificate. + +The finite census exhausts all `2^3 * 9^3 = 5,832` three-child instances with +2-coordinate permutations and reader coefficients in `{-1,0,1}`. Independent +literal state replay on both workspace basis vectors agrees with the matrix +criteria in every case. There are 2,592 compatible distinct-output instances, +2,772 compatible shared-final-output instances, and 180 cancellation-only cases. +This is completed finite coverage, not a new impossibility theorem. + +Controls include an incompatible nonzero reader with an explicit basis witness; +a zero-workspace input that hides that defect; omitted final restoration; +incorrect inverse order on a noncommuting example; an omitted reader; missing +catalytic pre-reads that expose dirt; an omitted inverse B that fails restoration; +and invalid/aliased instruction ports. Certificate/package mutations test +rejection of an unpaid operation, source corruption and receipt corruption. + +The exact general lemma is proved in prose. Neither the finite replay nor the +second Codex agent's algebraic review is independent human review or a formal +proof in a proof assistant. No selected cold replay was run: this isolated note +changes no supplier, selected certificate, shared generator, upstream source, +review ledger or frozen predecessor evidence. All-size compiler, common-label / +mutable-source realization, hosting, precision/tape and analytic transfer +obligations of the selected multiplication result remain open as recorded there. + +## Provenance and credit + +Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. Assignment seed **50**, generated +from OS randomness, selects recursive interfaces and the three-child/eight-entry +fixture. There is no random search. [CLAIM.md](CLAIM.md) records the three narrow +candidates and overlap decision; [SOURCE-PINS.json](SOURCE-PINS.json) identifies +exact context files and retained sources. The selected result at that base is +`836330098538459/500000000000000000`, from #1094 on #1087; complex binds in that +assembly. We do not reassign its binding supplier or modify its frontier. + +Credit Navinor / Aaron Wang with opencode assistance for PR1155's deferral +proposal and motivating reader question. Credit Sagar Thakrar's concurrent #1199 for the same applicability correction +and its distinct checkpoint planner, and his #1012 and +avirazza's #974 for the distinct hosted-assembly cost question; their reported +mass-neutrality is not contradicted by this abstract-interface correction. +Ross Richardson (CubeJerry)'s #889 supplies the shared-B, multiple-output dirty +fanout/echo construction; the pre-read/load/unload wrapper here is an instance +of that established mechanism, not a new batching claim. The additional result +is admitting nonzero readers through intervening workspace permutations using +the exact prefix condition, independently corroborating PR1199. Gareth Davidson's #1057 and woklerx's #1164 concern dirty-pool allocation and +higher-arity echoes, not the reader-defect criterion here. Ross Richardson's +universal-connector work and the repository's preceding dirty-restoration work +retain their own scopes and attribution. No priority claim is made for elementary +linear invariance or echo cancellation. + +Prepared for **mightyOil (Philipp)** with substantial **OpenAI Codex assistance** +in mathematics, implementation, verification and writing, including three scoped +Codex subagents. New files are Apache-2.0; retained source credit is in +[NOTICE.md](NOTICE.md). diff --git a/research/invariant-reader-restoration/SOURCE-PINS.json b/research/invariant-reader-restoration/SOURCE-PINS.json new file mode 100644 index 0000000000..29946cc119 --- /dev/null +++ b/research/invariant-reader-restoration/SOURCE-PINS.json @@ -0,0 +1,139 @@ +{ + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "assignment_seed": 50, + "selected_kappa": "836330098538459/500000000000000000", + "runtime_dependencies": "Python >=3.10 standard library only; no predecessor code imported", + "context_sources": [ + { + "path": "AGENTS.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "61c07e87b8d9df08ad6baf0a261ef952a4e38f54", + "sha256": "d2c06c9289da62f834edd2158a90b7e1e08d1bfce02b3f445b5d61e2a8ecccb4" + }, + { + "path": "CONTRIBUTING.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "d36720b93547f7d22b5383bf67121945949e59af", + "sha256": "ac97a58bd3420989d4a255bad371a2d71aeabb2f220fe2674d96fc55c56065ec" + }, + { + "path": "autoresearch.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "d0e29b88163e073218a5c2b67b6f6ae588f01561", + "sha256": "53c88d63f3c9abd78e291daffce7ccf919fbec4ab19c24114e11415fa041d87c" + }, + { + "path": "certificates/selected-result.json", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/current-status.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "aa3cf49715cd367ad8c4e63ab28856fc0d19794f", + "sha256": "1f59d648763c77d574d18dc59ea8bf62d2ee74aaed3c202c9c8cfa4f901badbd" + }, + { + "path": "docs/research/pr-ledger.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "eccf4d6c1d54746d3d650cf4e7b70e2d1d72d7e5", + "sha256": "4c8ea39063531bb218506e613c5b48d5fd8ea309071dd7bace4f47481021a0a7" + }, + { + "path": "docs/research/community-batch1099-review.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/README.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "f205b7132243aedcb2aa85110a44f0c8cd1e4fe1", + "sha256": "da542711a6a3eb01ce1ebdf8f28a748e6195512687f61d003b95ac5ff281a7b2" + }, + { + "path": "research/universal-connector-boundary/README.md", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ], + "retained_sources": [ + { + "local_path": "sources/PR1155-README.md", + "upstream_path": "research/restoration-coalescing/README.md", + "commit": "9821c6e9388f3fc097e94b72be9fa7b41a849527", + "sha256": "1af4e8d65700207092859b80fa5e4f4a7bd254ac0104d83c2b74e3a7477e823b", + "git_blob": "43ef54beedd197b8a41e7820a155f3186c91ca3a", + "credit": "Navinor / Aaron Wang, with opencode assistance; Apache-2.0" + }, + { + "local_path": "sources/BASE-SELECTED.json", + "upstream_path": "certificates/selected-result.json", + "commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "credit": "Repository maintainers and the contributors credited in the selected record" + } + ], + "related_prs_metadata_only": [ + { + "number": 889, + "head": "e2021d1c9e06948528cbc0a8fd7079b671da981d", + "author": "CubeJerry", + "title": "Research: batch common-factor product shears with dirty restoration", + "scope": "Read for overlap and credit; not imported or independently reproduced." + }, + { + "number": 1012, + "head": "4ceaf380ed41b28dadcc41d2f974f025ac4d8c03", + "author": "thakrarsagar", + "title": "Research note: restoration deferral is mass-neutral in the hosted T37 recurrence (no new kappa)", + "scope": "Read for overlap and credit; not imported or independently reproduced." + }, + { + "number": 974, + "head": "f40cd20a8c257bcfee17508c7de68fee24df0568", + "author": "avirazza", + "title": "Research: T21/T37 interface budget and bit-binding headroom (no new kappa)", + "scope": "Read for overlap and credit; not imported or independently reproduced." + }, + { + "number": 1057, + "head": "78a062df1dcab2bffea5ff4d8243f3da6e465414", + "author": "bitplane", + "title": "Research: exact additive echoes with three dirty arrays at any depth (no new kappa)", + "scope": "Read for overlap and credit; not imported or independently reproduced." + }, + { + "number": 1164, + "head": "0b2077e929ec488a4d38b3523688a8a68bf1b43e", + "author": "woklerx", + "title": "Recursive interface: four-way port borrowing reduces 56-factor echo from 1568 to 1088 calls", + "scope": "Read for overlap and credit; not imported or independently reproduced." + }, + { + "number": 1199, + "head": "85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d", + "author": "thakrarsagar", + "title": "Recursive interface: coalesce restoration with cancelling readers", + "read_source": "research/reader-restoration-cuts-seed53/README.md", + "read_source_sha256": "a073617e65be95d8fe7ceba41387d85171950d19f5e03f2ad1d9d1c8a6f4dae7", + "scope": "Concurrent overlapping correction; README inspected at exact head, no code imported or replay claimed." + } + ] +} diff --git a/research/invariant-reader-restoration/VALIDATION.md b/research/invariant-reader-restoration/VALIDATION.md new file mode 100644 index 0000000000..58cc7cc414 --- /dev/null +++ b/research/invariant-reader-restoration/VALIDATION.md @@ -0,0 +1,55 @@ +# Validation receipt + +Local verification on 2026-10-13, CPython 3.14.7, macOS 27.0.1 arm64. +Base and submission-context main: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. + +Completed commands: + +```sh +python3 -I -O -B research/invariant-reader-restoration/verify.py +python3 -I -O -B research/invariant-reader-restoration/test_package.py +``` + +Outputs: + +```text +PASS_INVARIANT_READER_RESTORATION cases=5832 wrapped_adds=210->150 no_new_kappa +PASS_READER_RESTORATION_PACKAGE relocation=1 deterministic_export=1 corruption_controls=8 +``` + +The main command includes the separate symbolic/permutation checker: all 873 +permutations of widths 1..6, complete source/workspace/output map, exact prefix +bounds and independently computed invoice. The all-input general statement is +proved in README.md; finite census and emitted-program checks are not a formal +proof-assistant theorem. Three narrowly scoped Codex agents helped with the +algebra, separate backend and independent symbolic audit; no human review claimed. + +Certificate SHA256: +`08d6163fc8672667cb49ed9fa7cd1f6b68644450dae062e955c6932efe273862`. +The certificate also binds SOURCE-PINS.json; retained original source bytes and +Git blobs are verified. All 11 context-source SHA256 hashes were checked against +the untouched base checkout. Selected and upstream files are unchanged. + +The first implementation was complete before the final verification phase. +Verification added the independently implemented symbolic checker, tested on-disk +fault rejection and clarified that the p+5 storage bound applies to integers. +No mathematical frontier claim was added. Orientation/selection used less than +the first eight minutes of the planned forty-minute cap, and final verification +and packaging began around 19:52 UTC, after the scoped construction was complete. + +Live overlap checks: 786 open PRs at entry; 802 at the 19:54 UTC refresh, plus +the discussion board. PR1155 remained at +`9821c6e9388f3fc097e94b72be9fa7b41a849527`. The 19:54 refresh found no matching criterion, but the final pre-submission +refresh through #1199 found Sagar Thakrar's direct concurrent overlap. Its +pinned README was inspected, and the package was reframed as independent +corroboration with additional noncommuting, dirt-independent and tape coverage. +No priority for the correction or identity is claimed. Read PR889's shared-factor dirty fanout +and PR1012/#974's distinct hosted-cost notes for precise credit; their heads are +in SOURCE-PINS.json. No pinned issue existed, so coordination remained local as +the user instructed. No reservation issue was opened. + +Not run or claimed: selected frontier cold replay, supplier adoption, shared +artifact regeneration, hosted CI, performance timing, full multiplication +formalization, or an optimized physical bit-tape implementation. These are +outside this isolated package. Exact online primitive/word-travel savings are +separate from the paid preparation term and any end-to-end runtime improvement. diff --git a/research/invariant-reader-restoration/backend.py b/research/invariant-reader-restoration/backend.py new file mode 100644 index 0000000000..8137a05956 --- /dev/null +++ b/research/invariant-reader-restoration/backend.py @@ -0,0 +1,226 @@ +"""Independent integer-scalar compiler and literal fixed-tape interpreter. + +No matrix library or certificate generator is used here. A permutation ``p`` +means ``new[j] = old[p[j]]``. The compiler emits only distinct-port shears +``('add', destination, source, sign)`` with sign +1 or -1. Scalar ports are +fixed consecutive tape words; port 0 is the data-head origin. + +The source register A is a clean scalar outside the tape. One ADD is executed +as A += memory[source], memory[destination] += sign*A, A -= memory[source]. +The tape scratch T used by swaps is a separate word, not a second register A. +Each ADD returns A and the data head to their initial states. Instruction +descriptors and loop/dispatch preparation are not included in this data-tape +invoice; the accompanying note must price or delimit that control cost. +""" + +from __future__ import annotations + +from collections.abc import Iterable, Sequence +from typing import Any + + +Instruction = tuple[str, int, int, int] + + +def _integer(value: object, name: str) -> int: + """Reject bool as well as non-integral values for ports and coefficients.""" + if type(value) is not int: + raise ValueError(f"{name} must be an integer (not bool)") + return value + + +def _inverse(permutation: Sequence[int]) -> list[int]: + inverse = [0] * len(permutation) + for destination, source in enumerate(permutation): + inverse[source] = destination + return inverse + + +def _emit_permutation( + program: list[Instruction], permutation: Sequence[int], temp: int +) -> None: + """Realize disjoint gather cycles with adjacent swaps and one clean T.""" + seen: set[int] = set() + for start in range(len(permutation)): + if start in seen: + continue + cycle: list[int] = [] + cursor = start + while cursor not in seen: + cycle.append(cursor) + seen.add(cursor) + cursor = permutation[cursor] + for first, second in zip(cycle, cycle[1:]): + # (a, b, T=0) -> (b, a, T=0), using no hidden scalar swap. + program.extend( + [ + ("add", temp, first, 1), + ("add", first, temp, -1), + ("add", first, second, 1), + ("add", second, first, -1), + ("add", second, temp, 1), + ("add", temp, second, -1), + ] + ) + + +def compile_batch( + perms: Sequence[Sequence[int]], + readers: Sequence[Sequence[int]], + eager: bool = True, +) -> dict[str, Any]: + """Compile reads followed by forward permutations and their restoration. + + There must be one reader per permutation and at least one child. All + permutations have the same positive width n. Reader entries are -1, 0, + or 1. Input sequences are copied and are never mutated. Child indices + in the returned segments are zero-based; the one deferred restoration + has ``child=None`` because it belongs to the whole batch. + + Ports 0..n-1 hold arbitrary dirty inputs; n+i is child i's distinct output + accumulator, whose initial value may be arbitrary. Port n+r is T and + MUST initially be zero. Each reader adds its linear functional to its + output before that child's forward permutation. Eager mode restores + each child immediately; deferred mode restores only the final product. + Compatibility of deferred readers with their prefixes is a caller proof + obligation, not assumed or silently repaired by this compiler. + + ``composed`` is the gather-index list for G_r ... G_1, even in eager mode. + ``segments`` delimit half-open instruction intervals for separate pricing. + Pass the returned ``program`` to :func:`execute`. + """ + if type(eager) is not bool: + raise ValueError("eager must be bool") + permutations = [list(permutation) for permutation in perms] + rows = [list(reader) for reader in readers] + if not permutations: + raise ValueError("at least one child permutation is required") + n = len(permutations[0]) + if n == 0: + raise ValueError("permutations must have positive width") + r = len(permutations) + if len(rows) != r: + raise ValueError("there must be one reader per permutation") + expected = list(range(n)) + for i, permutation in enumerate(permutations): + if len(permutation) != n: + raise ValueError(f"permutation {i} has the wrong width") + for port in permutation: + _integer(port, f"permutation {i} port") + if sorted(permutation) != expected: + raise ValueError(f"permutation {i} is not a permutation of 0..n-1") + for i, row in enumerate(rows): + if len(row) != n: + raise ValueError(f"reader {i} has the wrong width") + for coefficient in row: + if _integer(coefficient, f"reader {i} coefficient") not in (-1, 0, 1): + raise ValueError(f"reader {i} coefficient must be -1, 0, or 1") + + program: list[Instruction] = [] + segments: list[dict[str, Any]] = [] + composed = list(range(n)) + temp = n + r + for i, (permutation, row) in enumerate(zip(permutations, rows)): + start = len(program) + for source, coefficient in enumerate(row): + if coefficient: + program.append(("add", n + i, source, coefficient)) + segments.append( + {"kind": "reader", "child": i, "start": start, "stop": len(program)} + ) + start = len(program) + _emit_permutation(program, permutation, temp) + segments.append( + {"kind": "forward", "child": i, "start": start, "stop": len(program)} + ) + # If current[j] = original[composed[j]], applying p gives + # current[p[j]] = original[composed[p[j]]]. + composed = [composed[source] for source in permutation] + if eager: + start = len(program) + _emit_permutation(program, _inverse(permutation), temp) + segments.append( + {"kind": "restore", "child": i, "start": start, "stop": len(program)} + ) + if not eager: + start = len(program) + _emit_permutation(program, _inverse(composed), temp) + segments.append( + {"kind": "restore", "child": None, "start": start, "stop": len(program)} + ) + return { + "program": program, + "segments": segments, + "n": n, + "outputs": r, + "temp": temp, + "composed": composed, + } + + +def execute( + program: Iterable[Instruction], initial: Sequence[int] +) -> tuple[list[int], dict[str, int]]: + """Execute literal source-load/target-add/source-unload on copied integers. + + ADD is an instruction count, not a unit-price primitive: its invoice has + two source reads, one target read, one target write, and three scalar + additions/subtractions. For fixed tape ports s,d, the data-head walk is + 0 -> s -> d -> s -> 0, costing 2*s + 2*abs(d-s) word transitions. T's + tape slot is included whenever a compiled swap accesses it. This routine + does not know which port is T; its initial and final cleanliness must be + checked by the caller against the compiler metadata. + """ + memory = list(initial) + for i, value in enumerate(memory): + _integer(value, f"initial scalar {i}") + invoice = { + "add_instructions": 0, + "source_reads": 0, + "target_reads": 0, + "target_writes": 0, + "scalar_additions": 0, + "tape_word_travel": 0, + } + head = 0 + accumulator = 0 + for position, instruction in enumerate(program): + if not isinstance(instruction, (tuple, list)) or len(instruction) != 4: + raise ValueError(f"instruction {position} must have four fields") + operation, destination, source, sign = instruction + if operation != "add": + raise ValueError(f"instruction {position} has an unknown operation") + destination = _integer(destination, "destination") + source = _integer(source, "source") + sign = _integer(sign, "sign") + if not 0 <= destination < len(memory) or not 0 <= source < len(memory): + raise ValueError(f"instruction {position} port is outside memory") + if destination == source: + raise ValueError(f"instruction {position} needs distinct source and target") + if sign not in (-1, 1): + raise ValueError(f"instruction {position} sign must be -1 or 1") + + invoice["tape_word_travel"] += abs(source - head) + head = source + accumulator += memory[source] + invoice["source_reads"] += 1 + invoice["scalar_additions"] += 1 + + invoice["tape_word_travel"] += abs(destination - head) + head = destination + memory[destination] += sign * accumulator + invoice["target_reads"] += 1 + invoice["target_writes"] += 1 + invoice["scalar_additions"] += 1 + + invoice["tape_word_travel"] += abs(source - head) + head = source + accumulator -= memory[source] + invoice["source_reads"] += 1 + invoice["scalar_additions"] += 1 + invoice["tape_word_travel"] += abs(head) + head = 0 + invoice["add_instructions"] += 1 + if accumulator != 0: + raise ValueError(f"instruction {position} failed to clean the source register") + return memory, invoice diff --git a/research/invariant-reader-restoration/independent_check.py b/research/invariant-reader-restoration/independent_check.py new file mode 100644 index 0000000000..3555648f81 --- /dev/null +++ b/research/invariant-reader-restoration/independent_check.py @@ -0,0 +1,149 @@ +#!/usr/bin/env python3 +"""Separately implemented symbolic/cost AI audit; not human or formal review. + +Apache-2.0. Only the candidate compiler is imported from backend.py. This +checker does not import verify.py or use the candidate execution/invoice code. +The symbolic columns represent arbitrary integer input scalars; the routing +temporary has a zero input row and is not admitted as dirty workspace. +""" +from __future__ import annotations + +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent + + +def _require(ok, message): + if not ok: + raise ValueError(message) + + +def _candidate(): + spec = importlib.util.spec_from_file_location( + 'reader_restoration_candidate', HERE / 'backend.py') + _require(spec is not None and spec.loader is not None, + 'candidate compiler unavailable') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def _replay(program, initial): + """Replay shears on coefficient rows, independently deriving all charges.""" + state = [row[:] for row in initial] + columns = len(state[0]) + zero = [0] * columns + accumulator = zero[:] + invoice = dict(add_instructions=0, scalar_additions=0, source_reads=0, + target_reads=0, target_writes=0, tape_word_travel=0) + peaks = dict(workspace=0, outputs=0, temporary=0, sources=0, accumulator=0) + + def observe(): + # Only the twenty-port wrapper uses this fixture-specific partition. + if len(state) == 20: + for kind, indices in [('workspace', range(8)), ('outputs', range(8, 11)), + ('temporary', [11]), ('sources', range(12, 20))]: + peaks[kind] = max(peaks[kind], + max(sum(map(abs, state[i])) for i in indices)) + peaks['accumulator'] = max(peaks['accumulator'], sum(map(abs, accumulator))) + + observe() + for instruction in program: + _require(isinstance(instruction, (tuple, list)) and len(instruction) == 4, + 'malformed candidate instruction') + op, destination, source, sign = instruction + _require(op == 'add', 'unexpected candidate opcode') + _require(all(type(v) is int for v in (destination, source, sign)), + 'candidate ports and sign must be integers') + _require(0 <= destination < len(state) and 0 <= source < len(state), + 'candidate port out of bounds') + _require(destination != source and sign in (-1, 1), + 'invalid or aliased candidate shear') + # Explicitly model the clean register as a symbolic row as well. + accumulator = [a + b for a, b in zip(accumulator, state[source])] + observe() + state[destination] = [a + sign * b + for a, b in zip(state[destination], accumulator)] + observe() + accumulator = [a - b for a, b in zip(accumulator, state[source])] + _require(accumulator == zero, 'symbolic source register not restored') + observe() + invoice['add_instructions'] += 1 + invoice['scalar_additions'] += 3 + invoice['source_reads'] += 2 + invoice['target_reads'] += 1 + invoice['target_writes'] += 1 + # Closed-form walk 0 -> source -> destination -> source -> 0; + # this intentionally does not call the candidate head interpreter. + invoice['tape_word_travel'] += 2 * source + 2 * abs(destination - source) + return state, invoice, peaks + + +def check(): + candidate = _candidate() + permutation_cases = 0 + for n in range(1, 7): + basis = [[int(i == j) for j in range(n)] for i in range(n)] + for permutation in itertools.permutations(range(n)): + pack = candidate.compile_batch([permutation], [[0] * n], eager=True) + forwards = [segment for segment in pack['segments'] + if segment['kind'] == 'forward'] + _require(len(forwards) == 1, 'unexpected forward segment count') + segment = forwards[0] + actual, _, _ = _replay( + pack['program'][segment['start']:segment['stop']], + basis + [[0] * n, [0] * n]) + expected = [basis[index][:] for index in permutation] + [[0] * n, [0] * n] + _require(actual == expected, 'candidate gather permutation is incorrect') + permutation_cases += 1 + _require(permutation_cases == 873, 'incomplete permutation census') + + # Fixed literals, intentionally recreated without importing the verifier. + permutations = [[1, 0, 3, 2, 5, 4, 7, 6], + [3, 0, 1, 2, 7, 4, 5, 6], + [4, 5, 6, 7, 0, 1, 2, 3]] + readers = [[1, 0, 0, 0, 0, 0, 0, 0], + [1, 1, 0, 0, 0, 0, 0, 0], + [1, 0, 1, 0, 0, 0, 0, 0]] + pre_reads = [('add', 8 + i, j, -coefficient) + for i, row in enumerate(readers) + for j, coefficient in enumerate(row) if coefficient] + load = [('add', j, 12 + k, 1) for j in range(8) + for k in (j, (j + 1) % 8)] + unload = [(op, destination, source, -sign) + for op, destination, source, sign in reversed(load)] + initial = [[int(i == j and i != 11) for j in range(20)] for i in range(20)] + expected = [row[:] for row in initial] + # Construct y_i += H_i Bx directly; no permutation/compiler result enters + # the expected map, so both programs must independently meet the contract. + for i, row in enumerate(readers): + for j, coefficient in enumerate(row): + expected[8 + i][12 + j] += coefficient + expected[8 + i][12 + (j + 1) % 8] += coefficient + expected_peaks = dict(workspace=3, outputs=5, temporary=3, sources=1, accumulator=3) + receipt = dict(permutation_cases=permutation_cases, permutation_widths=list(range(1, 7)), + arbitrary_input_coordinates=19, + symbolic_map_sha256=hashlib.sha256( + json.dumps(expected, separators=(',', ':')).encode()).hexdigest()) + for name, eager, count, travel in [('eager', True, 210, 5864), + ('deferred', False, 150, 4504)]: + program = pre_reads + load + candidate.compile_batch( + permutations, readers, eager=eager)['program'] + unload + actual, invoice, peaks = _replay(program, initial) + _require(actual == expected, f'{name} complete symbolic contract failed') + _require(invoice['add_instructions'] == count, f'{name} ADD invoice changed') + _require(invoice['tape_word_travel'] == travel, f'{name} travel invoice changed') + _require(peaks == expected_peaks, f'{name} symbolic prefix bound changed') + receipt[name] = dict(invoice=invoice, prefix_coefficient_l1_bounds=peaks) + return receipt + + +if __name__ == '__main__': + result = check() + print('PASS_INDEPENDENT_READER_AUDIT permutation_cases=873 ' + 'wrapped_adds=210->150 word_travel=5864->4504 symbolic_map=exact') diff --git a/research/invariant-reader-restoration/sources/BASE-SELECTED.json b/research/invariant-reader-restoration/sources/BASE-SELECTED.json new file mode 100644 index 0000000000..ae6a99f28a --- /dev/null +++ b/research/invariant-reader-restoration/sources/BASE-SELECTED.json @@ -0,0 +1,222 @@ +{ + "status": "Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status", + "kappa": "836330098538459/500000000000000000", + "decimal": "0.001672660197076918", + "source_prs": [ + 1094, + 1087, + 1082, + 1074, + 1068, + 1065, + 1063, + 1061, + 1056, + 1055, + 1053, + 1050, + 1042, + 1031, + 1028, + 1022, + 1018, + 1005, + 1004, + 987, + 942, + 890, + 870, + 869, + 858, + 799, + 741, + 699, + 685, + 676, + 664, + 660, + 659, + 656, + 655, + 653, + 658, + 649, + 645, + 635, + 589, + 555, + 545, + 626, + 623, + 622, + 620, + 617, + 615, + 604, + 601, + 596, + 592, + 591, + 593, + 599, + 588, + 543, + 584, + 586, + 583, + 582, + 579, + 576, + 575, + 574, + 571, + 569, + 568, + 567, + 564, + 562, + 561, + 559, + 558, + 552, + 550, + 548, + 541, + 535, + 510, + 503, + 531, + 523, + 493, + 514, + 507, + 484, + 496, + 505, + 522, + 520, + 472, + 458, + 445, + 442, + 425, + 433, + 370, + 361, + 315 + ], + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "proof": "docs/research/community-batch1099-review.md", + "proof_supplements": { + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/complex-571-free4fc8/NOTICE.md": "a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97", + "research/complex-multicold/proof/CONSTRUCTION.md": "27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f", + "research/complex-multicold/vendor/pr559/PROOF.md": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453", + "research/structural-gain/frontier-composition/README.md": "70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887", + "research/complex-joint-prefix/proof/CONSTRUCTION.md": "a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105", + "research/kernel-frame-coalescing/PROOF.md": "fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b", + "research/complex-571-hpeq5/README.md": "4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b", + "research/hyperplane-end-lean/PROOF.md": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9", + "docs/research/community-hyperplane599-review.md": "3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c", + "research/complex-571-cold14-b3/README.md": "1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96", + "research/complex-571-cold14-b3/PROOF-NOTE.md": "1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d", + "scripts/verify_cold617_interface.py": "95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a", + "docs/research/community-cold617-review.md": "b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046", + "research/complex-k492-owner-repair/README.md": "ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902", + "research/complex-k492-owner-repair/PROOF-NOTE.md": "337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5", + "research/complex-k492-owner-repair/PROOF-NOTE-R.md": "22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "scripts/verify_frontier626.py": "2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444", + "scripts/verify_frontier626_bindings.py": "cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280", + "scripts/verify_frontier588_bindings.py": "6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d", + "scripts/verify_hpe_lean_binding.py": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183", + "docs/research/community-frontier741-review.md": "4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a", + "research/complex-sw4-frame8/PROVENANCE.md": "c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0", + "research/e8-bit-p111-tuned/tune/README.md": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d", + "scripts/verify_frontier741.py": "215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b", + "scripts/verify_frontier741_bindings.py": "eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "scripts/verify_frontier799.py": "19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99", + "scripts/verify_frontier799_bindings.py": "43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "docs/research/community-frontier890-review.md": "cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea", + "scripts/verify_frontier890.py": "88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175", + "scripts/verify_replay_coverage.py": "babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5", + "scripts/verify_frontier741_bridge_coverage.py": "9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836", + "certificates/replay-coverage/pr741-sw4-v1.json": "7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756", + "research/complex-t21-owners/PROOF.md": "78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def", + "research/complex-t21-owner-bound/PROOF.md": "2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417", + "research/gauge44-barch/PROOF-NOTE-BARCH.md": "c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d", + "research/complex-double-replica-owners/PROOF.md": "db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc", + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7", + "research/complex-t37-owners/PROOF.md": "09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510", + "research/complex-t37-owners/ALL-T-PROOF.md": "4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b", + ".github/workflows/t37-owners.yml": "c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026", + "docs/research/community-batch1047-review.md": "a6271faf5db0afe3ff7d24a34a3be7a959cdc33ee37784572fba014ee5358787", + "scripts/verify_frontier1042.py": "700fdcaeb6e8f57f6e63c71c2dd1652fc5b183e8d706cd092779bdc0d271e854", + "docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb", + "scripts/verify_frontier1094.py": "c7e20f59968ed5736fb859735de4de207de3418083e37012310ebcded946b949", + "research/community-batch1099-audit/check_frontier1094.py": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + }, + "review": "docs/research/community-batch1099-review.md", + "validation": "docs/research/community-batch1099-integration.json", + "reproduce": "make frontier1094-verify", + "scope": "Finite composition under inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 assumptions. Not a full Lean multiplication theorem.", + "previous_kappa": "1672188119205421/1000000000000000000", + "previous_record": "certificates/checkpoints/frontier1042.json", + "audited_source_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "reviewed_dependency_heads": { + "588": "6d0e53b66c29abd17981881a09eaff41ac862d85", + "543": "2065fe4f72a914d907f1046603f5a36f17018535", + "568": "71c99ac935a33bb7b59a1b4a7af8725a939b0b90", + "569": "1424da81263a5305b35e4cf74ef686c275f03f3f", + "571": "b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3", + "575": "eac6f7e378ab622dac50a2fd4b7ef6eab014de44", + "583": "89be768f0157f5a3d8e4db69cf1748768605eac9", + "586": "4846fee5b06af770e9b3a10c36200f673d656725", + "591": "f622547244bf6d895a571a7b035142ba66279806", + "592": "1f471c445c06a45a32e2c47e8d74c8264b68356b", + "593": "fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4", + "596": "7732dd5e46863ff294b5e443661cb9d99abf4e01", + "599": "bc13c8a3e000442606bd2dbe8583a17649ba6c32", + "601": "529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550", + "604": "1b795c5d7dea746ba310572585c0ef067574b4a6", + "615": "bf8a49a34350599763cced8592db81dc62c2c1c0", + "617": "904d62855723c00f8acef9a287a10768598fdeb2", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "858": "ae2e25fee91540c83ceee5a60e3b07422ce21c7d", + "869": "73e86f69bf9a391e3c334999f7bbe3825dc42759", + "870": "b734850dc348800942f0ffd1f0723fdec7539b2b", + "890": "4b3bd8cbe8e3e81c44161017c9b72c905a8040a8", + "942": "1960cfa919a0945d0ca4cb14ea96237000037903", + "1004": "1974578f82a30158dd5fcdcdf226b83df8e7196f", + "1005": "779e80aef469bc3a28b19f1adde199871a9a22e3", + "1018": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef", + "1022": "58618bcbfe88a252467755fc283c04c3db5ca4fd", + "1028": "be4bd89cb4483dcee43257200cd27601f938f13d", + "1031": "e900534f0beda892c726723524203b97471fb9a3", + "1042": "7e8ef087c02a77038a28a337a7ee3a77039cac0d", + "1094": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "1087": "589d1cedf5ef5f231182f4ec86408616311a8af0", + "1082": "0c2e294ec204e83846d27344f829d15ed9ee7cc6", + "1074": "052afc128954f7b6a2b3c409eb4d72248e4020f2", + "1068": "cc71375eae4e8754da0f5d940cb519d66625fb2e", + "1065": "387d935e354a931d636e2c5e6ee63a6910f78a1b", + "1063": "d9377d32e0c97e41338e704c3960fd6f2fa73806", + "1061": "223f581afb1d63d5f8476a69040617e11bcd50e4", + "1056": "d0201efbd68c4acc9832b84bcc986c8781b83c4f", + "1055": "a8ea308976f1709eef0a328463f010cf51469277", + "1053": "6f92ce8884929c9fd4730c86a28e2e3735de02af", + "1050": "c87242f846cfab8c0b97fd889b5fecb0eacef939", + "987": "5142511af0437572aca71b35d1987cd2b47bb5e3" + } +} diff --git a/research/invariant-reader-restoration/sources/PR1155-README.md b/research/invariant-reader-restoration/sources/PR1155-README.md new file mode 100644 index 0000000000..43ef54beed --- /dev/null +++ b/research/invariant-reader-restoration/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/invariant-reader-restoration/test_package.py b/research/invariant-reader-restoration/test_package.py new file mode 100644 index 0000000000..aa62509b9a --- /dev/null +++ b/research/invariant-reader-restoration/test_package.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Relocation and rejection tests for the scoped evidence package.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def run(directory, *args, success=True): + result = subprocess.run([sys.executable, '-I', '-O', '-B', str(directory/'verify.py'), *map(str,args)], + cwd=directory.parent, capture_output=True, text=True) + require((result.returncode == 0) == success, + f'Unexpected verifier result ({result.returncode}): {result.stdout}{result.stderr}') + if success and not args: + require('PASS_INVARIANT_READER_RESTORATION' in result.stdout, 'missing success marker') + return result + + +def main(): + controls = 0 + with tempfile.TemporaryDirectory(prefix='reader-restoration-') as tmp: + root = Path(tmp) + base = root/'relocated-package' + shutil.copytree(HERE, base) + run(base) + out = root/'export.json' + run(base, '--write', out) + require(out.read_bytes() == (base/'CERTIFICATE.json').read_bytes(), 'nondeterministic export') + + def mutated(name, filename, change): + nonlocal controls + directory = root/name + shutil.copytree(base, directory) + path = directory/filename + path.write_text(change(path.read_text())) + run(directory, success=False) + controls += 1 + + def unpaid(text): + receipt = json.loads(text) + receipt['catalytic_wrapper']['invoice_deferred']['add_instructions'] -= 1 + return json.dumps(receipt) + + def replace_once(old, new): + def change(text): + require(text.count(old) == 1, 'mutation anchor ambiguous or missing') + return text.replace(old, new) + return change + + mutated('unpaid-operation', 'CERTIFICATE.json', unpaid) + mutated('source-drift', 'sources/PR1155-README.md', lambda text: text+'\nCORRUPTED\n') + mutated('unrestored-accumulator', 'backend.py', + replace_once('accumulator -= memory[source]', 'accumulator += memory[source]')) + mutated('bad-swap', 'backend.py', + replace_once('("add", first, temp, -1)', '("add", first, temp, 1)')) + mutated('wrong-product-order', 'backend.py', + replace_once('composed = [composed[source] for source in permutation]', + 'composed = [permutation[source] for source in composed]')) + mutated('missing-wrapper-inverse', 'verify.py', + replace_once("wrapped_d = pre_reads + load + deferred['program'] + unload", + "wrapped_d = pre_reads + load + deferred['program']")) + mutated('missing-wrapper-preread', 'verify.py', + replace_once("wrapped_d = pre_reads + load + deferred['program'] + unload", + "wrapped_d = load + deferred['program'] + unload")) + mutated('wrong-shared-criterion', 'verify.py', + replace_once('expected_shared = not any(total)', 'expected_shared = expected')) + print(f'PASS_READER_RESTORATION_PACKAGE relocation=1 deterministic_export=1 corruption_controls={controls}') + +if __name__ == '__main__': + main() diff --git a/research/invariant-reader-restoration/verify.py b/research/invariant-reader-restoration/verify.py new file mode 100644 index 0000000000..13e4ae6749 --- /dev/null +++ b/research/invariant-reader-restoration/verify.py @@ -0,0 +1,296 @@ +#!/usr/bin/env python3 +"""Exact, scoped reader-compatible restoration evidence. Apache-2.0.""" +from __future__ import annotations +import argparse +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('restoration_backend', HERE / 'backend.py') +backend = importlib.util.module_from_spec(spec) +spec.loader.exec_module(backend) +independent_spec = importlib.util.spec_from_file_location('independent_restoration_check', HERE / 'independent_check.py') +independent = importlib.util.module_from_spec(independent_spec) +independent_spec.loader.exec_module(independent) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def matmul(a, b): + return [[sum(x * y for x, y in zip(row, col)) for col in zip(*b)] for row in a] + + +def pmat(p): + return [[int(p[i] == j) for j in range(len(p))] for i in range(len(p))] + + +def transpose(a): + return list(map(list, zip(*a))) + + +def matrix_data(perms, readers): + n = len(perms[0]) + prefix = identity(n) + prefixes, defects = [], [] + for p, h in zip(perms, readers): + prefixes.append(prefix) + changed = matmul([h], prefix)[0] + defects.append([x - y for x, y in zip(changed, h)]) + prefix = matmul(pmat(p), prefix) + return prefixes, defects, prefix + + +def direct(perms, readers, z, y, eager, shared=False): + """Literal state replay; does not use the matrix criterion or backend.""" + z, y = list(z), list(y) + for i, (p, h) in enumerate(zip(perms, readers)): + y[0 if shared else i] += sum(a * b for a, b in zip(h, z)) + z = [z[j] for j in p] + if eager: + out = [0] * len(p) + for j, src in enumerate(p): + out[src] = z[j] + z = out + if not eager: + # Restore by literal reverse-inverse factors, independently of product. + for p in reversed(perms): + out = [0] * len(p) + for j, src in enumerate(p): + out[src] = z[j] + z = out + return z + y + + +def census(): + # Entire declared domain, no random search or heuristic stopping. + ps = list(itertools.permutations(range(2))) + hs = list(itertools.product((-1, 0, 1), repeat=2)) + cases = independent_ok = shared_ok = cancellation_only = 0 + for perms in itertools.product(ps, repeat=3): + for readers in itertools.product(hs, repeat=3): + _, defects, _ = matrix_data(perms, readers) + expected = all(not any(d) for d in defects) + total = [sum(d[j] for d in defects) for j in range(2)] + expected_shared = not any(total) + observed, observed_shared = True, True + for z in ((1, 0), (0, 1)): + observed &= direct(perms, readers, z, [0]*3, True) == direct(perms, readers, z, [0]*3, False) + observed_shared &= direct(perms, readers, z, [0], True, True) == direct(perms, readers, z, [0], False, True) + require(observed == expected, 'independent-output criterion disagreement') + require(observed_shared == expected_shared, 'shared-output criterion disagreement') + cases += 1 + independent_ok += expected + shared_ok += expected_shared + cancellation_only += expected_shared and not expected + return {'dimension': 2, 'children': 3, 'permutation_alphabet_size': 2, + 'reader_alphabet': [-1, 0, 1], 'cases': cases, + 'independent_output_accepted': independent_ok, + 'shared_final_output_accepted': shared_ok, + 'shared_only_cancellation_cases': cancellation_only, + 'basis_vectors_per_semantics': 2, + 'stopping_rule': 'exhaust all 2^3 * 9^3 cases'} + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def pins(): + source = json.loads((HERE / 'SOURCE-PINS.json').read_text()) + for item in source['retained_sources']: + data = (HERE / item['local_path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == item['sha256'], 'retained source SHA256 mismatch') + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + require(blob == item['git_blob'], 'retained source Git blob mismatch') + selected = json.loads((HERE / 'sources/BASE-SELECTED.json').read_text()) + require(selected['kappa'] == source['selected_kappa'], 'base selected context mismatch') + return source + + +def source_permutation(matrix): + return [row.index(1) for row in matrix] + + +def compile_external_perm(p, n_outputs): + # A one-child batch with zero reader isolates a permutation and its inverse. + pack = backend.compile_batch([p], [[0] * len(p)], eager=True) + # Relocate the scratch register from n+1 to n+n_outputs. + n = len(p) + segment = next(s for s in pack['segments'] if s['kind'] == 'forward') + return [('add', n+n_outputs if d == n+1 else d, + n+n_outputs if s == n+1 else s, sign) + for _, d, s, sign in pack['program'][segment['start']:segment['stop']]] + + +def make_receipt(): + source = pins() + # Convention: new[j] = old[p[j]]. G2 is inverse to cycle notation (0123). + perms = [[1, 0, 3, 2, 5, 4, 7, 6], + [3, 0, 1, 2, 7, 4, 5, 6], + [4, 5, 6, 7, 0, 1, 2, 3]] + readers = [[1,0,0,0,0,0,0,0], [1,1,0,0,0,0,0,0], [1,0,1,0,0,0,0,0]] + prefixes, defects, product = matrix_data(perms, readers) + require(all(not any(d) for d in defects), 'fixture not compatible') + require(matmul(pmat(perms[0]), pmat(perms[1])) != matmul(pmat(perms[1]), pmat(perms[0])), 'fixture must be noncommuting') + eager = backend.compile_batch(perms, readers, eager=True) + deferred = backend.compile_batch(perms, readers, eager=False) + require(pmat(deferred['composed']) == product, 'backend/matrix product disagreement') + n, r = 8, 3 + # One full basis per arbitrary dirty workspace/output coordinate, plus mixed data. + inputs = [[int(i == j) for i in range(n+r)] + [0] for j in range(n+r)] + inputs += [[-7, 4, 0, 9, -2, 13, 5, -11, 31, -17, 2, 0], [0]*12] + for initial in inputs: + a, ai = backend.execute(eager['program'], initial) + b, bi = backend.execute(deferred['program'], initial) + expected = direct(perms, readers, initial[:n], initial[n:n+r], True) + [0] + require(a == b == expected, 'literal backend all-input basis failure') + # Literal inverse must restore every state register, including scratch. + inv = [(op, d, s, -sign) for op, d, s, sign in reversed(deferred['program'])] + restored, _ = backend.execute(inv, b) + require(restored == initial, 'literal inverse failure') + sample = inputs[-2] + _, invoice_e = backend.execute(eager['program'], sample) + _, invoice_d = backend.execute(deferred['program'], sample) + categories = {} + for name, pack in [('eager', eager), ('deferred', deferred)]: + counts = {} + for seg in pack['segments']: + counts[seg['kind']] = counts.get(seg['kind'], 0) + seg['stop']-seg['start'] + categories[name] = counts + require(len(eager['program']) == 173 and len(deferred['program']) == 113, 'literal invoice changed') + + # Catalytic wrapper removes all observable dependence on incoming dirt. + # Immutable source x occupies addresses 12..19. B = I + cyclic shift, + # expanded literally as two source additions per workspace coordinate. + pre_reads = [('add', n+i, j, -h) for i, row in enumerate(readers) + for j, h in enumerate(row) if h] + load = [('add', j, n+r+1+k, 1) for j in range(n) + for k in (j, (j+1) % n)] + unload = [(op, d, s, -sign) for op, d, s, sign in reversed(load)] + wrapped_e = pre_reads + load + eager['program'] + unload + wrapped_d = pre_reads + load + deferred['program'] + unload + wrapped_inputs = [[int(i == j) for i in range(20)] for j in range(20) if j != 11] + wrapped_inputs.append([-7,4,0,9,-2,13,5,-11,31,-17,2,0,3,-5,8,2,1,0,-4,6]) + for initial in wrapped_inputs: + a, _ = backend.execute(wrapped_e, initial) + b, _ = backend.execute(wrapped_d, initial) + x = initial[12:] + bx = [x[j] + x[(j+1) % n] for j in range(n)] + expected = initial[:] + for i, h in enumerate(readers): + expected[n+i] += sum(c*v for c,v in zip(h,bx)) + require(a == b == expected, 'catalytic wrapper or dirty independence failed') + inverse = [(op,d,s,-sign) for op,d,s,sign in reversed(wrapped_d)] + restored, _ = backend.execute(inverse, b) + require(restored == initial, 'wrapped inverse failed') + _, wrapped_ie = backend.execute(wrapped_e, wrapped_inputs[-1]) + _, wrapped_id = backend.execute(wrapped_d, wrapped_inputs[-1]) + require(len(wrapped_e) == 210 and len(wrapped_d) == 150, 'wrapped invoice changed') + wrapper = {'source_matrix': 'B x has coordinate x[j] + x[(j+1) mod 8]', + 'source_addresses': list(range(12,20)), 'basis_cases': 19, 'mixed_cases': 1, + 'pre_read_adds': len(pre_reads), 'B_adds_each_direction': len(load), + 'eager_program_sha256': digest(wrapped_e), 'deferred_program_sha256': digest(wrapped_d), + 'invoice_eager': wrapped_ie, 'invoice_deferred': wrapped_id} + + controls = {} + dirty_only = [1]+[0]*19 + missing_pre = load + deferred['program'] + unload + bad_state, _ = backend.execute(missing_pre, dirty_only) + require(bad_state[8:11] != [0]*3 and bad_state[:8] == dirty_only[:8], 'missing pre-read must expose dirt') + controls['missing_catalytic_pre_reads'] = bad_state[8:11] + source_only = [0]*12 + [1] + [0]*7 + missing_unload = pre_reads + load + deferred['program'] + bad_state, _ = backend.execute(missing_unload, source_only) + require(any(bad_state[:8]), 'unpaid inverse B must fail restoration') + controls['missing_inverse_B'] = bad_state[:8] + bad_readers = [h[:] for h in readers] + bad_readers[1] = [1,0,0,0,0,0,0,0] + _, bad_defects, _ = matrix_data(perms, bad_readers) + witness = [1]+[0]*7 + a = direct(perms, bad_readers, witness, [0]*r, True) + b = direct(perms, bad_readers, witness, [0]*r, False) + require(any(bad_defects[1]) and a != b, 'incompatible reader not detected') + controls['incompatible_reader'] = {'input_workspace': witness, 'eager_outputs': a[n:], 'deferred_outputs': b[n:], 'defect': bad_defects[1]} + require(direct(perms, bad_readers, [0]*n, [0]*r, True) == direct(perms, bad_readers, [0]*n, [0]*r, False), 'zero-workspace masking changed') + controls['zero_workspace_hides_bad_reader'] = True + # Keep emitted reader and forward events; omit final restore. + unrestored = [event for seg in deferred['segments'] if seg['kind'] != 'restore' + for event in deferred['program'][seg['start']:seg['stop']]] + initial = witness+[0]*(r+1) + no_restore, _ = backend.execute(unrestored, initial) + require(no_restore[:n] != witness, 'missing restore control ineffective') + controls['missing_final_restore'] = no_restore[:n] + wrong_order = unrestored[:] + for p in perms: # WRONG: inverse factors must execute in reverse order. + wrong_order += compile_external_perm(source_permutation(transpose(pmat(p))), r) + bad_state, _ = backend.execute(wrong_order, initial) + require(bad_state[:n] != witness, 'inverse-order control ineffective') + controls['wrong_inverse_order'] = bad_state[:n] + # Remove one reader ADD: workspace restoration still succeeds, output fails. + omitted = list(deferred['program']) + del omitted[0] + bad_state, _ = backend.execute(omitted, initial) + expected = direct(perms, readers, witness, [0]*r, True)+[0] + require(bad_state[:n] == witness and bad_state != expected, 'missing reader control ineffective') + controls['missing_reader'] = bad_state[n:n+r] + controls['dropped_scalar_charge'] = {'actual_add_instructions': 113, 'unpaid_claim': 112} + require(sum(categories['deferred'].values()) != 112, 'unpaid instruction not detected') + # Shared final-output cancellation is deliberately outside independent-output admission. + cp = [[1,0], [0,1], [0,1]] + ch = [[0,0], [1,0], [0,1]] + _, cd, _ = matrix_data(cp, ch) + require(any(any(row) for row in cd) and not any(sum(row[j] for row in cd) for j in range(2)), 'cancellation fixture failed') + require(direct(cp,ch,[1,0],[0,0,0],True) != direct(cp,ch,[1,0],[0,0,0],False), 'distinct cancellation control failed') + require(direct(cp,ch,[1,0],[0],True,True) == direct(cp,ch,[1,0],[0],False,True), 'shared cancellation identity failed') + controls['shared_target_cancellation'] = cd + # Backend admission controls: these are contract rejections, not counterexamples. + rejections = 0 + for program, state in [([('add',0,0,1)],[1]), ([('add',0,1,0)],[1,2]), ([('add',0,2,1)],[1,2])]: + try: + backend.execute(program, state) + except (ValueError, TypeError): + rejections += 1 + require(rejections == 3, 'backend contract rejection missing') + controls['backend_contract_rejections'] = rejections + return {'format': 'invariant-reader-restoration-v1', + 'status': 'exact scoped interface and finite literal invoice; no new kappa', + 'base_commit': source['base_commit'], 'seed': 50, + 'source_pins_sha256': hashlib.sha256((HERE/'SOURCE-PINS.json').read_bytes()).hexdigest(), + 'fixture': {'permutations_new_from_old': perms, 'readers': readers, + 'prefix_permutations': [source_permutation(p) for p in prefixes], + 'reader_defects': defects, 'composed_permutation': source_permutation(product), + 'input_basis_cases': n+r, 'mixed_or_zero_cases': 2, + 'clean_temp_registers_in_data': 1, 'clean_accumulator_registers': 1}, + 'programs': {'eager_sha256': digest(eager['program']), 'deferred_sha256': digest(deferred['program']), + 'eager_adds': len(eager['program']), 'deferred_adds': len(deferred['program']), + 'categories': categories}, + 'invoice_eager': invoice_e, 'invoice_deferred': invoice_d, + 'catalytic_wrapper': wrapper, 'independent_symbolic_check': independent.check(), + 'finite_census': census(), 'negative_controls': controls} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='authoring/export mode; normal verification compares stored receipt') + args = parser.parse_args() + receipt = make_receipt() + if args.write: + args.write.write_text(json.dumps(receipt, indent=2, sort_keys=True)+'\n') + print('WROTE_READER_RESTORATION_RECEIPT', args.write) + return + expected = json.loads((HERE/'CERTIFICATE.json').read_text()) + require(receipt == expected, 'stored certificate differs from recomputed evidence') + print('PASS_INVARIANT_READER_RESTORATION cases=5832 wrapped_adds=210->150 no_new_kappa') + +if __name__ == '__main__': + main()