diff --git a/research/r420-target-compensation/CERTIFICATE.json b/research/r420-target-compensation/CERTIFICATE.json new file mode 100644 index 0000000000..afb301eff8 --- /dev/null +++ b/research/r420-target-compensation/CERTIFICATE.json @@ -0,0 +1,79 @@ +{ + "status": "PASS_R420_TARGET_COMPENSATION", + "original_word_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "word_sha256": "f40efc3d8ac7437324ea23b777c89c82f0d41e3e9009fceb5a495612f148aaf5", + "basis_operations": 205, + "helper_injections": 11633, + "reduced_matrix_sha256": "1b14e9cafe164d20f1d89723ea3b404008b45bdbd32962920c77c6a2c85d191f", + "D_boundary_sha256": "4c62fc7593da47d45e906658c9750771146ce624fa3cddc88552027181449c5e", + "labels": { + "labels": 120, + "lattice_rank": 8, + "gram_det": 1, + "frames": 672 + }, + "native_columns": [ + 660, + 660 + ], + "separate_column_walk_forward_reverse": [ + 660, + 660 + ], + "original_bill": { + "D_adds": 19922, + "total_adds": 26916, + "forward": 144651, + "reverse": 2270064, + "five_stage_prefix": "998206739997057013039187410944", + "five_stage_bits": 100, + "nine_stage_prefix": "440858815560454746902811617646181283465263876766227759104", + "nine_stage_bits": 189, + "charged_nine_stage_bits": 192 + }, + "candidate_bill": { + "D_adds": 12043, + "total_adds": 19037, + "forward": 144651, + "reverse": 4409580, + "five_stage_prefix": "3766506725834174621276259609600", + "five_stage_bits": 102, + "nine_stage_prefix": "6276767299280756808558449610647393916158564399044362240000", + "nine_stage_bits": 192, + "charged_nine_stage_bits": 192 + }, + "geometry": { + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca", + "moves": 2940, + "copies": 9, + "erasures": 9, + "helpers": 420, + "paid_profile": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112 + }, + "saved_local_adds": 7879, + "saved_9_stage_32_replica_adds": 2269152, + "old_gate_local_H2_accepts": false, + "replacement_D_boundary_accepts": true, + "negative_controls": [ + "omit one entrance basis gate", + "omit one exit basis gate", + "apply exit basis in forward order", + "omit all entrance basis gates (zero targets would miss this)", + "inject K instead of E K", + "omit one dirty-helper injection", + "basis operation at full frame", + "read a source at frame zero", + "self XOR", + "write a helper", + "F2-neutral pair exceeds the prefix allowance", + "basis recipe uses an extra register", + "incorrect immutable source pin" + ] +} diff --git a/research/r420-target-compensation/HOSTED-CERTIFICATE.json b/research/r420-target-compensation/HOSTED-CERTIFICATE.json new file mode 100644 index 0000000000..2ec12013a7 --- /dev/null +++ b/research/r420-target-compensation/HOSTED-CERTIFICATE.json @@ -0,0 +1,130 @@ +{ + "status": "PASS_R420_TARGET_COMPENSATION_HOSTED", + "word_sha256": "f40efc3d8ac7437324ea23b777c89c82f0d41e3e9009fceb5a495612f148aaf5", + "local_adds": 19037, + "local_records": 21995, + "local_rank_mass": 5112, + "five_stage_columns": 900, + "nine_stage_columns": 1380, + "nine_stage_bridge_controls": 18, + "record_controls": [ + "omit-basis-add", + "omit-helper-add", + "omit-copy", + "understated-move" + ], + "parent_mutations_rejected": [ + "omit an idle child", + "omit a bridge", + "omit terminal exchange", + "remove a local invocation", + "understate live stock", + "omit a local paid move", + "wrong reflected copy charge", + "alter residual orthogonal basis", + "misstate replication count", + "misstate stage count", + "alias data across stages", + "delay an idle advance past its level", + "truncate the last idle advance", + "re-use a helper bank slot", + "wrong residual frame", + "alias data across replica groups", + "omit the fourth replica group" + ], + "hosted_mutations_rejected": [ + "slot outside window", + "copy index outside family", + "negative slot offset", + "wrong residual width", + "duplicate helper", + "omitted helper", + "hosted owner in another replica or outside the data stock", + "hosted owner on a wrong data family", + "wrong call orientation", + "duplicate call", + "changed idle rank", + "understated live stock", + "missing remainder summary", + "stale stage count", + "hosted coordinate beyond the pending set", + "overlapping hosted coordinates" + ], + "hosted_events": 6334560, + "hosted_profile": { + "1": 380160, + "2": 426624, + "4": 32640, + "5": 34560, + "6": 15360, + "7": 23040, + "8": 2592, + "42": 3456 + }, + "hosted_residuals": 120960, + "live": 30720, + "physical": 30729, + "invoice": { + "live": 30720, + "physical": 30729, + "maxchild": 42, + "rank_mass": 1956096, + "hosted_residuals": 120960, + "bank_assignments": 0, + "prefix_bits": 192, + "charged_prefix_bits": 192, + "coefficient_bits": 192, + "two_level_coefficient_bits": 424, + "charged_two_level_coefficient_bits": 512, + "row_coefficient": 18355, + "halving_depth": 2 + }, + "unchanged_bit_lower": "413456747036699736067/250000000000000000000000", + "cited_complex_lower": "65528268492323474503/40000000000000000000000", + "unchanged_kappa": "51110230636731/31250000000000000", + "outer_strict_constraints": 47, + "outer_controls": [ + "next_grid", + "zero_eta", + "zero_beta", + "unit_beta" + ], + "parent_unbanked_columns": 4740, + "parent_bridge_controls": 18, + "expanded_invoice": { + "original": { + "terms": { + "local_and_bridge_adds": "7820928", + "high_level_routing": "540759810610176", + "physical_row_routing": "61872964416", + "good_calls_and_compiler": "246569815252224", + "fixed_setup": "4194304", + "copy_erase_episodes": "2592", + "selectors": "5436702144", + "prefix": "440858815560454746902811617646181283465263876766227759104", + "constant": "1" + }, + "coefficient": "440858815560454746902811617646181283465264664163175305889", + "coefficient_bits": 189, + "two_level_coefficient": "163943430630425998331250076398909206538196936862890235015817458025743362212780131597636668378324437046354474839780809607936900", + "two_level_bits": 416 + }, + "candidate": { + "terms": { + "local_and_bridge_adds": "5551776", + "high_level_routing": "540759810610176", + "physical_row_routing": "61872964416", + "good_calls_and_compiler": "246569815252224", + "fixed_setup": "4194304", + "copy_erase_episodes": "2592", + "selectors": "5436702144", + "prefix": "6276767299280756808558449610647393916158564399044362240000", + "constant": "1" + }, + "coefficient": "6276767299280756808558449610647393916158565186441307517633", + "coefficient_bits": 192, + "two_level_coefficient": "33232806291910364952528164923528257432272329823214455231380848889502185837217737407915654349022508479867048703838288249854740484", + "two_level_bits": 424 + } + } +} diff --git a/research/r420-target-compensation/README.md b/research/r420-target-compensation/README.md new file mode 100644 index 0000000000..d81df58d1d --- /dev/null +++ b/research/r420-target-compensation/README.md @@ -0,0 +1,287 @@ +# R420 compensation through a reversible target basis + +**Finite bit-circuit improvement; no new kappa.** Eumemic's +[PR543](https://github.com/CrocSwap/integer-mult-bounds/pull/543) R420 word +implements its frame-zero dirty-helper compensation with 19,922 binary XORs. +This package implements exactly the same F2 boundary map with **12,043 XORs**, +including both target-basis changes. The complete native word falls from +**26,916 to 19,037 XORs**, a saving of 7,879 (29.27%). It uses the same helpers, +copies, frame paths and recursive children. + +The tradeoff is a larger cancellation-free prefix bound. A budget-constrained +search keeps the nine-stage prefix within its existing **192-bit charge**; +the complete invoice still fits its existing **512-bit coefficient charge**. +Fresh native, nine-stage, physical hosting and exact assembly checks pass. +This is a circuit-count result, not a measured multiplication speedup. + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected construction at +that base is #626 with #543, at conditional +`kappa = 51110230636731/31250000000000000 = 0.001635527380375392`. +Its actual [assembly](../community-k492-audit/pr626/replay/ASSEMBLY.json) +is complex-bound. The selected files and all predecessor inputs are untouched. + +The final overlap refresh found concurrent **PR686/PR694**, which also factor +this compensation but change and restore helper rows. This contribution uses +the **target side**, permits successive noncommuting row operations, enforces +the complete nine-stage prefix budget during nomination, and includes a fresh +hosted invoice/assembly replay. The comparison and credit are explicit below. + +## Reproduce + +From the repository root, Python 3.11+ and its standard library suffice for +the finite construction, native labels/frames, both complete column walks, +local invoice and 13 negative controls: + +```sh +python3 -I -B research/r420-target-compensation/verify.py +``` + +Expected final line: + +```text +PASS_R420_TARGET_COMPENSATION D=19922->12043 total=26916->19037 columns=660 rank_mass=5112 nine_bits=192 controls=13 +``` + +The command verifies the frozen recipe without trusting or rerunning the search. +It makes no output files by default. `--output build/NEW-DIRECTORY` also saves +the reconstructed word and report; existing directories are refused. Word +identity is canonical decompressed JSON, not a regenerated gzip-container hash. + +For a fresh complete hosted replay, use a C++17 compiler with Boost headers and +install `requirements.txt` into a virtual environment. Then run: + +```sh +python3 -I -B research/r420-target-compensation/replay_hosted.py +``` + +Expected final status: + +```text +PASS_R420_TARGET_COMPENSATION_HOSTED local_adds=19037 hosted_events=6334560 prefix_charge=192 coefficient_charge=512 kappa=unchanged +``` + +It creates a unique directory under `build/`, records the exact subprocess +commands and logs, and uses the frozen original hosting selection. It needs +SymPy, but no NumPy, SciPy, optimization solver or network. Compilation and +replay are sequential. `--cxx` selects the compiler and `--output` selects a +fresh output directory. The checked environment was Linux, Python 3.12.3, +SymPy 1.14.0, mpmath 1.3.0 and GCC 13.3.0. Assertions must remain enabled. + +## The boundary identity and its interface + +Write `s` for the 420 arbitrary helper inputs and `y` for the 120 arbitrary +target inputs. The original D is `y <- y + K s`, for a fixed binary +120-by-420 matrix K. Its rows are recovered directly from the pinned word. +All participating rows start and finish D at frame zero. + +The 205 pairs in [candidate.json](candidate.json) denote elementary +transvections `y[a] ^= y[b]`, using zero-based target indices. Let E be their +product in execution order, and put `R = E K` over F2. Execute: + +1. The 205 transvections, giving `E y`. +2. The 11,633 helper additions specified by the nonzero entries of R. +3. The same 205 transvections in reverse order. + +Each transvection is its own inverse over F2. The output is therefore +`E^-1 (E y + R s) = y + K s`. Sources and helpers are never written. This +argument applies to arbitrary incoming target values, including dirty targets; +it requires no initially zero workspace and introduces no workspace row. + +The new transcript does **not** satisfy PR543's syntactic H2, which requires +every D gate to read only helpers. Its old direct-summation computation of +`K_equals_D` also does not apply. The verifier records both old predicates as +false, retains every other H1–H5/U/J/U-inverse check, and separately verifies +the exact D boundary `(x,y,s) -> (x,y+K s,s)` on all 660 symbolic columns. + +This is a sufficient replacement for H2: the unchanged raw word has +`(z,y) -> (U z, y + J x + K s)`, with `J = I`, and the unchanged C restores +`z = (x,s)`. Substituting any legal frame-zero transcript with the stated D +boundary gives the same composite map as the original D. Every new ADD is +between rows already at frame zero, and D leaves their frames there; the +unchanged remainder consequently sees identical values and frames. The +inherited common-label realization treats these frame-zero XORs in the same +way as other common-frame additions. Its all-size realization remains an +inherited assumption. + +The equality asserted here is over F2. This is not equality of the positive +integer transfer matrices: those matrices grow, as the next section records. +The signed inverse in the inherited lifted program reverses the literal +instructions and negates ADD coefficients. Both orientations' absolute-value +prefix bills are recomputed from those actual instructions. + +## Complete cost and prefix accounting + +| Quantity | Original | New | +|---|---:|---:| +| D helper-read XORs | 19,922 | 11,633 | +| D entrance / exit target-basis XORs | 0 / 0 | 205 / 205 | +| Total D XORs | 19,922 | 12,043 | +| Other native XORs, including scatter and cleanup | 6,994 | 6,994 | +| Complete native XORs | 26,916 | 19,037 | +| Native record count | 29,874 | 21,995 | +| Native MOVE records | 2,940 | 2,940 | +| Helpers / retained COPY–ERASE pairs | 420 / 9 | 420 / 9 | +| Native paid rank mass | 5,112 | 5,112 | +| Native forward bound F | 144,651 | 144,651 | +| Native reverse bound B | 2,270,064 | 4,409,580 | +| Five-stage bound `64 F^3 B^2`, bits | 100 | 102 | +| Nine-stage bound `2^18 F^5 B^4`, bits | 189 | 192 | +| Charged nine-stage prefix bits | 192 | 192 | +| Two-level coefficient bits | 416 | 424 | +| Charged two-level coefficient bits | 512 | 512 | +| Emitted hosted instructions | 8,603,712 | 6,334,560 | + +Every register has the same ordered frame path. Including the nine rank-8 +COPY charges, the local profile remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`. Its moment for every `0 < p < 1` is +`1320 + 1440*2^p + 60*4^p + 120*5^p + 9*8^p`. + +In units of inherited frame-zero ADD work, the changed local cost is +`C_fixed + (205 + 11633 + 205) * C_ADD0` in place of +`C_fixed + 19922 * C_ADD0`. Here `C_fixed` includes the unchanged A/scatter/B/C, +all frame transitions, all source access outside D, retained copies, clears +and recursive children. D's helper accesses and both basis changes are fully +included; there is no deferred basis restoration. + +The complete nine-stage construction makes 288 local calls. Its local-ADD +invoice term falls by `288 * 7879 = 2,269,152`. The 69,120 bridge additions, +2,592 COPY–ERASE episodes, 120,960 hosted residuals, 30,720 live / 30,729 +physical rows, all route selectors, and the hosted recursive profile remain. +Maximum child rank is 42 and halving depth is two. The inherited emitter, +parent audit and hosting audit rebuild and check these quantities. + +[HOSTED-CERTIFICATE.json](HOSTED-CERTIFICATE.json) expands every finite-invoice +term: local/bridge additions, high-level and physical-row routing, paid calls +and compiler work, fixed setup, copies/clears, selectors and the prefix. The +**unrounded coefficient increases** because the prefix grows; the existing +192/512-bit allowances still suffice. This package claims neither entrywise +positive domination nor a reduced unrounded coefficient. Both exact moment +engines reproduce the bit lower bound +`413456747036699736067/250000000000000000000000`. All 47 assembly inequalities +reproduce the selected kappa using the pinned #626 complex lower bound. The +complex supplier is cited, not rebuilt by this bit-only replay. + +## Bounded experiment and evidence + +Assignment seed **18** was drawn from OS randomness. It chooses the first of +three candidates by `18 mod 3`: factor D; resynthesize the nine retained totals; +or resynthesize phase-B block 8. The D object was chosen before experimentation +and recorded in the local sprint claims. [RESEARCH.json](RESEARCH.json) records +the overlap scan and exact pending-PR heads. + +The nomination greedily replaces row `R[a]` by `R[a] XOR R[b]`, charging two +extra basis gates. It examines every ordered distinct pair at each step and +uses a seeded tie break among maximum positive savings. To respect the prefix +bill, it admits only steps that keep F at most 144,651 and B at most **4,409,638**, +the exact integer fourth-root cutoff for `2^18 F^5 B^4 < 2^192`. + +The fast admission calculation is exact. If A is the positive forward basis +matrix and B0 the positive reversed-basis matrix, a new row step `(a,b)` raises +the output-bound vector by +`2 * B0[:,a] * ((A y)[b] + sum(h[j] for j in R[b] minus R[a]))`. +This follows by expanding the new endpoint +`B0 T (T A y + R' h)`: `T^2 = I + 2 e_ab`, and the changed helper row differs +by twice the entries in `R[b] minus R[a]`. Admission is applied to the actual +forward and reverse entry bounds. Fresh literal execution checks the resulting +bound independently of this incremental calculation. + +The guarded trial accepted 205 steps and examined **2,941,680 ordered pairs**, +including the final pass with no admissible positive-gain pair. An unrestricted +control with the same seed accepted 328 steps, examined **4,698,120 pairs** and +reached 10,384 D XORs, but needed 201 nine-stage bits (charged 256) and exceeded +the five-stage 104-bit allowance. It was rejected. Both trials had a cap of +1,000 accepted steps and stopped before it. No zero-gain detours, column +operations or other target bases were exhaustively searched; 12,043 is not +claimed optimal. + +The exact nomination, counts and trace hashes reproduce with: + +```sh +python3 -I -B research/r420-target-compensation/search.py +``` + +`verify.py` uses the predecessor's exact lattice/frame/symbolic-row engine and +a separate Boolean-column walk of all 660 columns in both orientations. The +full replay freshly compiles the predecessor C++ engines: 900 five-stage and +1,380 nine-stage formal columns, six and eighteen omitted-bridge controls, +and exact record geometry/copy accounting. The global template checks 4,740 +unbanked columns and eighteen omitted bridges; the parent and hosted audits +reject seventeen and sixteen mutations. Four new record controls omit a basis +ADD, helper ADD or COPY, or understate a MOVE rank. Four assembly controls also +remain active. The finite results do not constitute a formal proof of the +complete multiplication theorem. + +The 13 native controls cover missing entrance/exit gates, wrong inverse order, +untransformed helper injection, helper omission, illegal frames/operands, +extra registers, an incorrect source pin, and a cancelling gate pair that +preserves F2 semantics while exceeding the prefix allowance. A specific +control omits the entire entrance basis: it still passes when targets start +at zero, but fails the required arbitrary-target boundary. This demonstrates +why clean-target tests would be insufficient. + +## Scope and attribution + +PR543's word, compensation matrix, interleaved interface and checker are +**eumemic's**, at reviewed head `2065fe4f72a914d907f1046603f5a36f17018535`, +building on #493. Credit also remains with **Dylan Crow** for the E8 word and +record/checker lineage; **DreamingOfClouds** for #503/#510 and generalized +nine-stage accounting; **DaysSky** for bridged columns and whole-call hosting; +**Zhihao Chen** for the mutable-source/common-label and compressed geometry +lineage; and **Chafik Boukhalfa** for physical routes, templates and audits. +See the original [R420 README](../e8-bit-r420/README.md) and the selected +[maintainer review](../../docs/research/community-k492-review.md) for cumulative +credit. All consumed predecessor source files are pinned in +[SOURCES.json](SOURCES.json) and remain unchanged. + +PR670 and PR674 reduce phase-B blocks 3 and 5, and PR790 (seed 19) +resynthesizes block 9. This result changes only D and uses a +reversible target-basis factorization under a prefix budget. No composition +with those pending block changes is certified here. PR661's fixed-order +phase-B frame bound is not reopened. PR677 completes a native +ADDRESS-query restored DATA shear; it is a different interface and algebra. +None is an execution dependency. PR249/309's compensation transport concerns +later frames; this construction keeps compensation at frame zero. + +The final anonymous refresh, at **2026-10-13 04:25:33 UTC**, inspected the 100 +most recently updated open PRs in addition to the initial 497-PR snapshot. +It found directly related work published during this experiment: + +- **Mikhail R. Gadelha's [PR686](https://github.com/CrocSwap/integer-mult-bounds/pull/686)**, + head `23dcb610c2b156b76b9d599ea296c3cbde224b2d`, restores a single helper pair + and saves 108 ADDs. Its written semantic D-boundary substitution is credited. +- **Greer Guthrie's [PR694](https://github.com/CrocSwap/integer-mult-bounds/pull/694)**, + head `9732ac127dd4bef98a846aaa904c20b5a84e72c1`, reports 201 disjoint helper + pairs and 6,934 saved ADDs. It factors on the right, `K' = K P^-1`, and + restores the helper basis. The present factorization is on the left, + `R = E K`, and restores arbitrary incoming target values without writing + helpers. Its 205 successive target operations are not restricted to a + disjoint matching. The result uses **945 fewer native ADDs** than PR694's + reported construction; its forward/reverse norm tradeoff is different, + so this is not an entrywise domination claim. PR694 explicitly leaves the + hosted-parent invoice open at that head; this package supplies a full + nine-stage hosted replay for its own target-basis word. + +The frame-zero substitution principle and elementary basis-change identity +are not claimed as new priority over those contributions. No PR686/694 code, +pair matching or recipe was imported: the target circuit and initial complete +hosted replay were already frozen before this refresh. The package was renamed +to `r420-target-compensation` to avoid PR694's directory name. This is a +meaningfully different implementation of the same D boundary with additional +budget and integration evidence; no composition with either helper circuit is +claimed. The same refresh found **Ali Romman's PR688** hosting the PR670/674 +block composition, and **mtpsl's PR691** changing phase-A quad 13. Those change +different scalar subwords and are also credited as concurrent work. + +All-size compilation, common-label/mutable-basis realization, pooled hosting, +normalized residuals, precision/tape recovery and analytic transfer remain +inherited assumptions. There is no circuit optimality theorem, new kappa, +eleven-stage physical replay or complete Lean multiplication proof. Adopting +the replacement into a selected supplier would require a maintainer to accept +the D-boundary lemma and update the relevant source bindings; this standalone +package makes no such selection change. + +Submitted by **@commdata2338** with substantial AI assistance: **OpenAI Codex** +(GPT-6-Astra) did the research, code, proof text and verification, and Claude +Code packaged the submission. Computational cross-checks do not claim +independent human review. +New files are under the repository's **Apache-2.0** license. diff --git a/research/r420-target-compensation/RESEARCH.json b/research/r420-target-compensation/RESEARCH.json new file mode 100644 index 0000000000..b618fda8aa --- /dev/null +++ b/research/r420-target-compensation/RESEARCH.json @@ -0,0 +1,124 @@ +{ + "track": "bit supplier", + "assignment_seed": 18, + "seed_source": "secrets.randbelow(100), using operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "selected_kappa": "51110230636731/31250000000000000", + "selected_binding": "complex", + "object": "PR543 R420 phase D, 120-by-420 dirty-helper compensation; 19922 original binary XORs", + "method": "Reversible target-row basis, R=E K, with both E and E inverse paid; exact 192-bit nine-stage prefix guard", + "candidates": [ + "factor R420 D using target rows", + "resynthesize the nine R420 phase-A retained totals", + "resynthesize R420 phase-B block 8" + ], + "candidate_selection": "18 mod 3 = 0", + "stopping_rule": "two seed-18 greedy trials (one guarded, one unrestricted control), each capped at 1000 accepted row steps; stop when no admissible positive-gain ordered pair remains", + "optimality_claim": false, + "initial_overlap": { + "snapshot_count": 497, + "snapshot_sha256": "d0058c0e76acb9a52aee50e7ba34af74a1968bd456b82eb1d89c2559917b0a62", + "source": "owner-provided 497-open-PR snapshot dated 2026-10-12 22:47 America/Chicago; no API enumeration repeated", + "inspected_heads": { + "661": "9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89", + "670": "2e31fcad7f9ecc8b97039ecb2333e581fd725fa1", + "674": "1b01fd8b135fb2c458554fbbbab4338336bf366d" + }, + "related_scope": { + "661": "fixed-order phase-B frame bound, excludes scalar resynthesis", + "670": "block 3, 50-to-33 XOR rewrite", + "674": "block 5, 46-to-34 integer sum-sharing rewrite", + "249/309": "compensation transport to later frames, unlike the present fixed frame-zero factorization" + } + }, + "concurrent_scopes_same_submitter": { + "PR790": { + "seed": 19, + "object": "R420 phase-B block 9, integer matrix factorization" + } + }, + "difference_from_pr677": "PR677 restores native ADDRESS-query DATA shears with recursive-query/workspace costs; this package changes a fixed finite F2 compensation map with no new recursive query", + "local_claim": "recorded locally by the submitter; stated in the pull request", + "frozen_construction_utc": "2026-10-13T04:19:10Z", + "attribution": "Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex, GPT-6-Astra; packaged with Claude Code)", + "license": "Apache-2.0", + "followup_overlap_inspected_heads": { + "249": "96495746c786d6d0339dbb38c7f553d4af3f88ed", + "309": "aeb4808af1392e565e7071cbeb2c29608201cf24" + }, + "final_overlap": { + "retrieved_at": "2026-10-13T04:25:33.527311+00:00", + "refreshed_open_prs": 100, + "initial_inventory": 497, + "api_requests_for_refresh": 1, + "metadata_file_sha256": "c1e35c15300762c684b035b2b92dc4f796c6d6cd153ec1abab4328a5b5e406ce", + "relevant_prs": [ + { + "number": 694, + "title": "Research: save 6,934 R420 XORs with a restored helper basis", + "author": "g-guthrie", + "updatedAt": "2026-10-13T04:19:55Z", + "head": "research/seed12-bit-supplier", + "head_sha": "9732ac127dd4bef98a846aaa904c20b5a84e72c1" + }, + { + "number": 691, + "title": "Research: shorten R420 phase-A quad 13 from 19 to 12 XORs (no new kappa)", + "author": "mtpsl", + "updatedAt": "2026-10-13T04:16:35Z", + "head": "research/r420-quad13", + "head_sha": "ee6b9175fe006c11871802866c487b5ecc1a93a4" + }, + { + "number": 688, + "title": "Research: compose R420 circuits with 16,704 fewer hosted instructions (no new kappa)", + "author": "aliromman", + "updatedAt": "2026-10-13T04:08:46Z", + "head": "codex/seed15-r420-block-circuit", + "head_sha": "bb05c40c3e6319aa8c131b06a105e3648ac6c95b" + }, + { + "number": 686, + "title": "Research: save 108 R420 XORs with restored frame-zero sharing (no new kappa)", + "author": "mikhailramalho", + "updatedAt": "2026-10-13T04:06:36Z", + "head": "research/r420-frame-zero-pair", + "head_sha": "23dcb610c2b156b76b9d599ea296c3cbde224b2d" + }, + { + "number": 677, + "title": "Research note: restored DATA-shear boundaries for PR #521's native BIT query (exact query costs, no new \u03ba)", + "author": "commdata2338", + "updatedAt": "2026-10-13T03:43:59Z", + "head": "seed57-restored-shear", + "head_sha": "613c02b8b4411f991f108dcc1481b3f9100b996f" + }, + { + "number": 674, + "title": "Research: reduce R420 block 5 from 46 to 34 XOR gates (no new kappa)", + "author": "x0hu", + "updatedAt": "2026-10-13T03:41:09Z", + "head": "codex/r420-block5-resynthesis", + "head_sha": "1b01fd8b135fb2c458554fbbbab4338336bf366d" + }, + { + "number": 670, + "title": "Research: simplify one R420 block from 50 to 33 XOR gates (no new kappa)", + "author": "yongjae321", + "updatedAt": "2026-10-13T03:30:19Z", + "head": "research/r420-block3-xor-seed13", + "head_sha": "2e31fcad7f9ecc8b97039ecb2333e581fd725fa1" + }, + { + "number": 661, + "title": "Scoped negative result: R420 phase-B frames are moment-optimal at fixed gate order", + "author": "yuj1r0", + "updatedAt": "2026-10-13T03:07:36Z", + "head": "codex/r420-phase-b-frame-bound", + "head_sha": "9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89" + } + ], + "finding": "Concurrent PR686/694 treat the same D boundary using restored helper bases. This result uses a target basis, successive noncommuting row operations, an exact nine-stage prefix guard, 945 fewer native ADDs than PR694 reports, and a fresh complete hosted replay for its own word. The package was renamed to avoid PR694 directory collision. No priority for the general semantic D substitution is claimed. PR688 composes phase-B blocks; PR691 changes phase-A quad 13. No code or recipe imported from these concurrent PRs." + }, + "local_claims_seen_before_handoff": "four local sprint claims; hashes kept by the submitter" +} diff --git a/research/r420-target-compensation/SOURCES.json b/research/r420-target-compensation/SOURCES.json new file mode 100644 index 0000000000..43c64b39ed --- /dev/null +++ b/research/r420-target-compensation/SOURCES.json @@ -0,0 +1,48 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source_pr543_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "selection": "PR626 with PR543; selected frontier and predecessor inputs unchanged", + "files": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "research/community-family588-audit/pr543/RESULT9.json": "f2a326be2a501ec6cac7c04719d31bf3b0007175c1a549538a11ec617128ae1e", + "research/community-family588-audit/pr543/cout/columns_k4.json": "76728003ec61f70c00b8ccff99e5b40e94b4b8042583e1d9b50ba2d2460394ef", + "research/community-family588-audit/pr543/v9/hosted/AUDIT.json": "c077fdccdd3a536f5acba2cdd1e3392787722ac2a9e2061cd4b7c7ae80bdb286", + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/e8-bit-carrier-skeleton/code/nine/geometry.py": "36eeda3184bd009e89462b65c8725d10860c444f8da8f1f87e5f6e50120011ca", + "research/e8-bit-carrier-skeleton/data/bit/bitE8-r865.json.gz": "1fb726ea3818fe0837cceb0dd22a71a0814f064e5e781628104610d6468e0e55", + "research/e8-bit-carrier-skeleton/data/eleven/residual-isometries.json": "0fa5b353a0321af2ce4e2045db1d4c2d6418a11663894e2afcdb1eaa1984bddc", + "research/e8-bit-r420/DEPENDS.json": "fa9253078c444b8f4a57e849048f727c3c8233c3dc3c7f651bef2cf7bb0178c5", + "research/e8-bit-r420/EXPECTED.json": "06eccee9f6b77e140833df83407e7996dc948c17d49b0779ab171fbe463fd28d", + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/e8-bit-r420/SOURCE-pr510.json": "5e84c26ba837ce029acd1b5089e5533d2ebde793deede84215322112e95e06f8", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-r420/data/selection9-r420.json": "9737b5f39367ee5a8affa52e5fbb92d1408f0f9e9f14ed64d6f00ea9428b291c", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/code/adapt.py": "27b6b77cc4ebf439f9019e63a22dedc1ef72ee65fe120aad3d17316b1df06d7b", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/code/assemble9.py": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py": "57e558c80a2fea6e291587b04afd76dfaee3550729997798b61f33daf90b8ec9", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_parent_k.py": "374e1d983589463bbfa06b6e9f2ffafb9d2c14acf97b1f858593a3cef90e93d2", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/bank_routes_k.py": "ea678a7befda10c6f1b9dd38a36fe1437c6468472bd649f60b9f01522047e0bf", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/emit_k.py": "298b16c3d4f58a468ad1a64564c8500cb281414a3f3c0428fd467908eeb4a4b4", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/hosting_k.py": "081c3b95b18d900d97ce82af64fb428f085b6adc6d8ca93ea920797dad7eb81e", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/bank_routes.py": "7c6997c455bd55acca3a1603797c34e7733d557c27a7694a1429ff15773a505d", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/config.py": "283d7fad45155ee91e704d63ec947cf4a60aeff5cc43510bc0e835f7da7d8767", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/e8core.py": "1cb286196c1530d06f50f0997febc5993b388f33464e295611b920ba30a24eeb", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r740-replica32/code/tile_m.py": "d6ae4a556472d403773cd2117c992bfc10e1187112da1b3893f3fae628a131dd", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py": "d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3" + }, + "source_pr510_head": "64edee18af02aab0c1696b677a0287dd0146381b", + "source_pr543_main_dependency_commit": "db0e57bc7f36b5ac0fc844ad7ce1396165ee6647" +} diff --git a/research/r420-target-compensation/VALIDATION.json b/research/r420-target-compensation/VALIDATION.json new file mode 100644 index 0000000000..ba57bab074 --- /dev/null +++ b/research/r420-target-compensation/VALIDATION.json @@ -0,0 +1,83 @@ +{ + "status": "PASS_LOCAL_FINITE_AND_COMPLETE_NINE_STAGE_HOSTED_REPLAY", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "environment": { + "system": "Linux", + "python": "3.12.3", + "sympy": "1.14.0", + "mpmath": "1.3.0", + "compiler": "GCC 13.3.0", + "thread_policy": "sequential child processes; OMP, OpenBLAS and MKL thread counts set to 1" + }, + "commands": [ + { + "command": "python3 -I -B research/r420-target-compensation/verify.py", + "result": "PASS; 660 symbolic columns and a separate 660-column walk in each direction, 13 native controls" + }, + { + "command": "python3 -I -B research/r420-target-compensation/search.py", + "result": "PASS; exact frozen candidate and both search summaries reproduced" + }, + { + "command": "../.venv/bin/python -I -B research/r420-target-compensation/replay_hosted.py --output build/r420-target-compensation-final", + "result": "PASS; full report equals HOSTED-CERTIFICATE.json" + }, + { + "command": "python3 -B scripts/verify_selected_result.py", + "result": "PASS; selected record, exact kappa, original source inventory and proof supplement" + }, + { + "command": "python3 -O -I -B research/r420-target-compensation/verify.py", + "result": "expected rejection before checking: assertions must remain enabled in predecessor checks" + }, + { + "command": "git diff --check", + "result": "PASS" + } + ], + "canonical_word_sha256": "f40efc3d8ac7437324ea23b777c89c82f0d41e3e9009fceb5a495612f148aaf5", + "full_receipt": "HOSTED-CERTIFICATE.json", + "local_receipt": "CERTIFICATE.json", + "logs_sha256": { + "adapt-audit.log": "29f0a8f80096c360958685252859c9d106b43c4432fce0c636988a472a69fecd", + "compile-columns2.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "compile-columns4.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "compile-legality.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "export.log": "379705e6b1619a45a4427a2091ec665091fa04de290fe13ec2f08313d9187c64", + "five-stage.log": "0d9b69a1e564ffa9c1efbd0a4d83a7fb7c309fbd7aa0e854ac8ca5068b682121", + "geometry.log": "2e178fef74f54c8e6916d86415b8074e40ce27ba9fea0d2a33eb4d19cffda0b1", + "global.log": "3fc5ee3d2d229c8374f02bd71edefa17e1785a09fbe34b0fa4addd51f0dc6762", + "host-audit.log": "4343d386e22e630d1bfe220c4fc3758bdd104b1c3d86f310fc38d089ab84ec11", + "host.log": "090ba5ed34bf9b57fd3ec5e3b09078ad82fd3df4db98e490a2b945355ea4ff6b", + "invoice.log": "93741da4cc5eec2b6682e8ee46e6a78ff51310b6b8df22e27e559abeb4f3ee26", + "legality.log": "3000fa150205e577dffec79fddf4d782dd4dd4178f0e1985f170fdfd5e20c0b0", + "native.log": "063bdb80ea1dbc49103eb7336d0465a2e4bb74a2a4e84880845cc13ae2bf9aca", + "nine-stage.log": "8992e6152ff1a2d251d39790ce0165bcfab64afb4c415ce63a55cdb2db73ef27", + "omit-basis-add.log": "f85c6d1b3e3ba33de33b8a1b67726ed7eec2aeb725bdfa096baaf51dac0724e1", + "omit-copy.log": "97c44824ff543b2659973389205847d8d32003f48c8130f93a210297482361b0", + "omit-helper-add.log": "f85c6d1b3e3ba33de33b8a1b67726ed7eec2aeb725bdfa096baaf51dac0724e1", + "parent-audit.log": "9b86aec25ffe5cf9f66f902dd1348e1191247086236ccbf504bc0d962ed308d7", + "stage.log": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "understated-move.log": "aaef28322733869bf55f864edf432161c5e7be3853d97c2adb9c4fab305ac92d" + }, + "logs_scope": "Hashes identify this Linux execution only, not mathematical equality across environments; generated container hashes and timings are not certificate comparison criteria.", + "replay_coverage": { + "native_columns": 660, + "five_stage_columns": 900, + "nine_stage_columns": 1380, + "parent_unbanked_columns": 4740, + "hosted_events": 6334560, + "hosted_residuals": 120960, + "outer_strict_constraints": 47 + }, + "limits": [ + "No repository-wide make verify; only the added package and selected-record binding were checked.", + "No full complex-supplier replay; the selected PR626 complex lower bound is pinned and cited.", + "No remote CI or Lean run.", + "No composition with PR686/694 helper bases or concurrent phase-A/B replacements.", + "Inherited all-size, physical realization, tape/precision and analytic assumptions remain." + ], + "overlap": "One final anonymous API refresh at 2026-10-13T04:25:33.527311+00:00; 100 recent open PRs checked against the initial 497-PR inventory. PR686/694 overlap is credited and distinguished in README.md and RESEARCH.json.", + "publication": "local branch and patch only; no GitHub write performed", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human review claimed." +} diff --git a/research/r420-target-compensation/candidate.json b/research/r420-target-compensation/candidate.json new file mode 100644 index 0000000000..83fabcf57d --- /dev/null +++ b/research/r420-target-compensation/candidate.json @@ -0,0 +1,873 @@ +{ + "format": "r420-compensation-target-basis-v1", + "assignment_seed": 18, + "original_word_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "basis_operations": [ + [ + 102, + 99 + ], + [ + 114, + 116 + ], + [ + 119, + 113 + ], + [ + 17, + 23 + ], + [ + 119, + 114 + ], + [ + 28, + 25 + ], + [ + 8, + 14 + ], + [ + 114, + 8 + ], + [ + 28, + 102 + ], + [ + 104, + 110 + ], + [ + 80, + 36 + ], + [ + 104, + 102 + ], + [ + 102, + 17 + ], + [ + 53, + 54 + ], + [ + 73, + 74 + ], + [ + 73, + 53 + ], + [ + 11, + 13 + ], + [ + 11, + 8 + ], + [ + 21, + 19 + ], + [ + 94, + 88 + ], + [ + 61, + 78 + ], + [ + 85, + 34 + ], + [ + 80, + 85 + ], + [ + 77, + 79 + ], + [ + 56, + 62 + ], + [ + 56, + 53 + ], + [ + 71, + 65 + ], + [ + 71, + 53 + ], + [ + 69, + 67 + ], + [ + 101, + 96 + ], + [ + 58, + 50 + ], + [ + 20, + 18 + ], + [ + 101, + 20 + ], + [ + 89, + 91 + ], + [ + 112, + 118 + ], + [ + 29, + 24 + ], + [ + 21, + 29 + ], + [ + 26, + 31 + ], + [ + 26, + 20 + ], + [ + 76, + 78 + ], + [ + 47, + 91 + ], + [ + 47, + 85 + ], + [ + 117, + 115 + ], + [ + 117, + 112 + ], + [ + 5, + 3 + ], + [ + 98, + 103 + ], + [ + 35, + 55 + ], + [ + 99, + 100 + ], + [ + 64, + 51 + ], + [ + 22, + 16 + ], + [ + 22, + 98 + ], + [ + 111, + 105 + ], + [ + 111, + 29 + ], + [ + 109, + 107 + ], + [ + 109, + 20 + ], + [ + 63, + 57 + ], + [ + 69, + 63 + ], + [ + 82, + 6 + ], + [ + 59, + 79 + ], + [ + 15, + 9 + ], + [ + 15, + 5 + ], + [ + 90, + 92 + ], + [ + 75, + 72 + ], + [ + 75, + 63 + ], + [ + 86, + 29 + ], + [ + 2, + 4 + ], + [ + 2, + 112 + ], + [ + 38, + 32 + ], + [ + 90, + 38 + ], + [ + 6, + 3 + ], + [ + 24, + 72 + ], + [ + 49, + 50 + ], + [ + 49, + 63 + ], + [ + 97, + 100 + ], + [ + 97, + 29 + ], + [ + 45, + 41 + ], + [ + 46, + 43 + ], + [ + 38, + 46 + ], + [ + 40, + 44 + ], + [ + 18, + 16 + ], + [ + 112, + 5 + ], + [ + 1, + 7 + ], + [ + 1, + 5 + ], + [ + 1, + 112 + ], + [ + 55, + 53 + ], + [ + 42, + 93 + ], + [ + 42, + 85 + ], + [ + 51, + 66 + ], + [ + 59, + 51 + ], + [ + 107, + 93 + ], + [ + 48, + 37 + ], + [ + 54, + 50 + ], + [ + 106, + 108 + ], + [ + 106, + 98 + ], + [ + 95, + 37 + ], + [ + 92, + 83 + ], + [ + 74, + 12 + ], + [ + 40, + 45 + ], + [ + 60, + 79 + ], + [ + 60, + 61 + ], + [ + 116, + 84 + ], + [ + 70, + 68 + ], + [ + 70, + 77 + ], + [ + 98, + 70 + ], + [ + 76, + 51 + ], + [ + 61, + 76 + ], + [ + 57, + 72 + ], + [ + 87, + 32 + ], + [ + 87, + 57 + ], + [ + 23, + 39 + ], + [ + 96, + 23 + ], + [ + 0, + 92 + ], + [ + 30, + 68 + ], + [ + 67, + 66 + ], + [ + 110, + 12 + ], + [ + 13, + 64 + ], + [ + 88, + 77 + ], + [ + 36, + 55 + ], + [ + 14, + 91 + ], + [ + 25, + 94 + ], + [ + 43, + 33 + ], + [ + 113, + 98 + ], + [ + 31, + 53 + ], + [ + 10, + 12 + ], + [ + 10, + 5 + ], + [ + 81, + 94 + ], + [ + 81, + 84 + ], + [ + 27, + 79 + ], + [ + 26, + 109 + ], + [ + 52, + 70 + ], + [ + 41, + 58 + ], + [ + 65, + 5 + ], + [ + 66, + 56 + ], + [ + 33, + 56 + ], + [ + 34, + 32 + ], + [ + 117, + 1 + ], + [ + 75, + 69 + ], + [ + 60, + 59 + ], + [ + 19, + 107 + ], + [ + 86, + 76 + ], + [ + 94, + 106 + ], + [ + 16, + 69 + ], + [ + 113, + 69 + ], + [ + 119, + 11 + ], + [ + 64, + 109 + ], + [ + 62, + 3 + ], + [ + 40, + 69 + ], + [ + 68, + 90 + ], + [ + 57, + 80 + ], + [ + 83, + 90 + ], + [ + 9, + 83 + ], + [ + 112, + 90 + ], + [ + 81, + 69 + ], + [ + 18, + 90 + ], + [ + 7, + 56 + ], + [ + 110, + 61 + ], + [ + 50, + 56 + ], + [ + 108, + 71 + ], + [ + 39, + 73 + ], + [ + 105, + 59 + ], + [ + 103, + 61 + ], + [ + 63, + 73 + ], + [ + 78, + 56 + ], + [ + 7, + 28 + ], + [ + 30, + 109 + ], + [ + 31, + 59 + ], + [ + 115, + 90 + ], + [ + 78, + 106 + ], + [ + 33, + 80 + ], + [ + 24, + 69 + ], + [ + 7, + 1 + ], + [ + 54, + 69 + ], + [ + 58, + 1 + ], + [ + 55, + 106 + ], + [ + 118, + 28 + ], + [ + 113, + 56 + ], + [ + 116, + 15 + ], + [ + 74, + 61 + ], + [ + 116, + 11 + ], + [ + 54, + 28 + ], + [ + 110, + 109 + ], + [ + 108, + 61 + ], + [ + 13, + 61 + ], + [ + 100, + 28 + ], + [ + 30, + 59 + ], + [ + 30, + 69 + ], + [ + 24, + 73 + ], + [ + 93, + 28 + ], + [ + 100, + 11 + ], + [ + 89, + 38 + ], + [ + 92, + 106 + ], + [ + 34, + 38 + ], + [ + 68, + 69 + ], + [ + 4, + 90 + ], + [ + 43, + 106 + ], + [ + 43, + 69 + ], + [ + 44, + 42 + ], + [ + 95, + 90 + ], + [ + 37, + 69 + ], + [ + 58, + 90 + ], + [ + 37, + 42 + ], + [ + 111, + 97 + ], + [ + 111, + 21 + ], + [ + 118, + 69 + ], + [ + 118, + 61 + ] + ], + "search": { + "guarded": { + "guarded": true, + "seed": 18, + "max_steps": 1000, + "accepted_steps": 205, + "ordered_pairs_examined": 2941680, + "admissible_positive_pairs": 209881, + "stopping": "no_admissible_positive_gain_pair", + "trace_sha256": "346b26c10bed49c05d8c0bd5a172df3aef0aa20062e123d96b2e6e3b630bd0c4", + "reverse_cap": 4409638, + "bill": { + "D_adds": 12043, + "total_adds": 19037, + "forward": 144651, + "reverse": 4409580, + "five_stage_prefix": "3766506725834174621276259609600", + "five_stage_bits": 102, + "nine_stage_prefix": "6276767299280756808558449610647393916158564399044362240000", + "nine_stage_bits": 192, + "charged_nine_stage_bits": 192 + } + }, + "unrestricted_control": { + "guarded": false, + "seed": 18, + "max_steps": 1000, + "accepted_steps": 328, + "ordered_pairs_examined": 4698120, + "admissible_positive_pairs": 288634, + "stopping": "no_admissible_positive_gain_pair", + "trace_sha256": "63767924c051b641c2a3c48d87537aed94a3a3cd481ee45c7473db9e176f10f8", + "reverse_cap": null, + "bill": { + "D_adds": 10384, + "total_adds": 17378, + "forward": 144651, + "reverse": 19146788, + "five_stage_prefix": "71012720752611549315351263087616", + "five_stage_bits": 106, + "nine_stage_prefix": "2231160631838402558220757462273893322135432768944973056835584", + "nine_stage_bits": 201, + "charged_nine_stage_bits": 256 + } + } + } +} diff --git a/research/r420-target-compensation/common.py b/research/r420-target-compensation/common.py new file mode 100644 index 0000000000..8cbf7052f2 --- /dev/null +++ b/research/r420-target-compensation/common.py @@ -0,0 +1,149 @@ +"""Finite R420 compensation construction; Apache-2.0, substantial Codex assistance.""" + +import copy +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +V, R, N = 120, 420, 660 + + +class Reject(ValueError): + pass + + +def need(condition, message): + if not condition: + raise Reject(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def read_word(): + return json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + + +def rows_of(word): + need((word["v"], word["R"]) == (V, R), "wrong dimensions") + rows = [0] * V + for frame, destination, sources in word["D"]: + need(frame == 0 and V <= destination < 2 * V, "original D shape") + need(len(sources) == len(set(sources)), "duplicate helper") + for source in sources: + need(2 * V <= source < N, "original D must read helpers") + rows[destination - V] ^= 1 << (source - 2 * V) + return rows + + +def make_word(original, operations): + """Emit E, the literal helper injection E K, then E inverse over F2.""" + rows = rows_of(original) + basis = [] + for pair in operations: + need(isinstance(pair, list) and len(pair) == 2, "bad basis pair") + a, b = pair + need(type(a) is int and type(b) is int and 0 <= a < V and 0 <= b < V and a != b, + "invalid basis transvection") + rows[a] ^= rows[b] + basis.append([0, V + a, [V + b]]) + injection = [[0, V + a, [2 * V + b for b in range(R) if row >> b & 1]] + for a, row in enumerate(rows) if row] + word = copy.deepcopy(original) + word["D"] = basis + injection + list(reversed(basis)) + return word, rows + + +def scalar_stream(word): + """ADD / COPY / CLEAR, keeping the inherited one-copy-at-a-time lifecycle.""" + stream = [] + for section in ("D", "A", "scatter", "B", "C"): + if section == "scatter": + for k, source in enumerate(word["ret"]): + stream.append(("copy", N, source)) + for t, row in enumerate(word["scatter"]): + if k in row: + stream.append(("add", V + t, N)) + stream.append(("clear", N, source)) + else: + for _, destination, sources in word[section]: + stream.extend(("add", destination, source) for source in sources) + return stream + + +def norm_replay(stream, reverse=False, initial=None): + values = [1] * N + [0] if initial is None else list(initial) + maximum = max(values) + opened = None + for kind, destination, source in (reversed(stream) if reverse else stream): + if reverse: + kind = {"copy": "clear", "clear": "copy"}.get(kind, kind) + if kind == "add": + need(destination != N and (source != N or opened is not None), "bad copy access") + need(opened != destination, "copied original was changed") + values[destination] += values[source] + maximum = max(maximum, values[destination]) + elif kind == "copy": + need(opened is None and destination == N, "bad copy opening") + values[N] = values[source] + opened = source + else: + need(kind == "clear" and opened == source and destination == N, "bad copy closure") + values[N] = 0 + opened = None + need(opened is None and values[N] == 0, "unclosed copy") + return maximum, values + + +def bill(word): + stream = scalar_stream(word) + forward, _ = norm_replay(stream) + reverse, _ = norm_replay(stream, reverse=True) + five = 64 * forward ** 3 * reverse ** 2 + nine = (1 << 18) * forward ** 5 * reverse ** 4 + return { + "D_adds": sum(len(g[2]) for g in word["D"]), + "total_adds": sum(k == "add" for k, _, _ in stream), + "forward": forward, + "reverse": reverse, + "five_stage_prefix": str(five), + "five_stage_bits": five.bit_length(), + "nine_stage_prefix": str(nine), + "nine_stage_bits": nine.bit_length(), + "charged_nine_stage_bits": 64 * ((nine.bit_length() + 63) // 64), + } + + +def search_context(original): + """Bounds just outside D, derived by literal execution of the fixed exterior.""" + need(not any(V <= source < 2 * V for section in ("A", "B", "C") + for _, _, sources in original[section] for source in sources), + "the search formula assumes no target reads outside D") + empty = dict(original, D=[]) + stream = scalar_stream(empty) + initial = [1] * N + [0] + initial[V:2 * V] = [0] * V + exterior_peak, forward = norm_replay(stream, initial=initial) + reverse_peak, reverse = norm_replay(stream, reverse=True) + return exterior_peak, forward[V:2 * V], reverse_peak, reverse + + +def fourth_root(n): + lo, hi = 0, 1 << ((n.bit_length() + 3) // 4) + while hi - lo > 1: + middle = (hi + lo) // 2 + if middle ** 4 <= n: + lo = middle + else: + hi = middle + need(lo ** 4 <= n < (lo + 1) ** 4, "fourth-root bracket") + return lo diff --git a/research/r420-target-compensation/replay_hosted.py b/research/r420-target-compensation/replay_hosted.py new file mode 100644 index 0000000000..146b550c78 --- /dev/null +++ b/research/r420-target-compensation/replay_hosted.py @@ -0,0 +1,249 @@ +"""Fresh native, nine-stage, hosted and invoice replay of the changed bit word. + +Requires SymPy 1.14, a C++17 compiler and Boost headers. No optimizer or network. +Apache-2.0; prepared with substantial OpenAI Codex assistance. +""" + +import argparse +import json +import os +import shutil +import struct +import subprocess +import sys +import tempfile +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from common import HERE, ROOT, need +from verify import pins + + +def invoice_detail(adds, prefix, hosted, global_receipt, geometry): + """Expand every term of the pinned assemble9.py finite invoice using ints.""" + m, stages, replicas, helpers = 64, 9, 32, 420 + live, physical, depth = hosted["live"], hosted["physical"], 2 + paid = sum(hosted["profile"].values()) + episodes = global_receipt["copy_erase_episodes"] + operations = stages * replicas * adds + global_receipt["bridge_additions"] + events = (8 * replicas * stages * (240 + helpers) + 8 * (8 * 120 * replicas) + + 2 * stages * replicas * helpers + 2 * episodes) + selectors = 2 * stages * replicas * ( + live - 1 + helpers * m * (geometry["max_route_factors"] + 144 + 2 + m - 1 + m)) + terms = { + "local_and_bridge_adds": operations, + "high_level_routing": events * 16 * (m * m + 1) ** 2, + "physical_row_routing": events * physical, + "good_calls_and_compiler": paid * (8 * m * m + 8 + 128 * (2 * m) ** 3), + "fixed_setup": 16 * m ** 3, + "copy_erase_episodes": episodes, + "selectors": selectors, + "prefix": prefix, + "constant": 1, + } + coefficient = sum(terms.values()) + two = (coefficient + 1) ** depth * (paid + 1) ** depth + return {"terms": {k: str(v) for k, v in terms.items()}, + "coefficient": str(coefficient), "coefficient_bits": coefficient.bit_length(), + "two_level_coefficient": str(two), "two_level_bits": two.bit_length()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="fresh directory; default: unique directory under build/") + parser.add_argument("--cxx", default="c++") + parser.add_argument("--write-certificate", action="store_true", help="create a missing hosted certificate") + args = parser.parse_args() + need(not sys.flags.optimize, "assertions must be enabled") + try: + import resource + resource.setrlimit(resource.RLIMIT_CORE, (0, 0)) + except ImportError: + pass + manifest = json.loads((HERE / "SOURCES.json").read_text()) + pins(manifest) + if args.output: + out = args.output.resolve() + out.mkdir(parents=True, exist_ok=False) + else: + (ROOT / "build").mkdir(exist_ok=True) + out = Path(tempfile.mkdtemp(prefix="r420-compensation-hosted-", dir=ROOT / "build")) + (out / "logs").mkdir() + (out / "bin").mkdir() + (out / "tmp").mkdir() + environment = dict(os.environ, PYTHONDONTWRITEBYTECODE="1", TMPDIR=str(out / "tmp"), + OMP_NUM_THREADS="1", OPENBLAS_NUM_THREADS="1", MKL_NUM_THREADS="1") + commands = [] + + def run(label, command, expected_error=None): + command = [str(x) for x in command] + commands.append({"label": label, "argv": command, "expected_error": expected_error}) + (out / "commands.json").write_text(json.dumps(commands, indent=2) + "\n") + with (out / "logs" / (label + ".log")).open("w") as log: + proc = subprocess.run(command, cwd=ROOT, env=environment, stdout=log, stderr=subprocess.STDOUT) + need((proc.returncode != 0) if expected_error else (proc.returncode == 0), + f"{label}: unexpected exit {proc.returncode}; see {out / 'logs' / (label + '.log')}") + if expected_error: + need(expected_error in (out / "logs" / (label + ".log")).read_text(), + label + ": did not reject for the intended reason") + print(("REJECT " if expected_error else "PASS ") + label, flush=True) + + def python(label, script, *arguments): + run(label, [sys.executable, "-E", "-s", "-B", script, *arguments]) + + def read(path): + return json.loads(path.read_text()) + + predecessor = ROOT / "research/e8-bit-carrier-skeleton" + bit = predecessor / "code/bit" + checkers = bit / "checkers" + pricing = ROOT / "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage" + vk = pricing / "vendor/e8-r715-eleven-stage-whole/code" + local = out / "local" + python("native", HERE / "verify.py", "--output", local) + word = local / "word.json.gz" + python("export", bit / "export_records.py", word, local / "records") + python("stage", bit / "regression/stage_cohort.py", local / "records", local / "records", + local / "cin", local / "cout") + compile_flags = ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9", "-DVPORTS=120", "-DRHELP=420"] + run("compile-legality", [args.cxx, *compile_flags, checkers / "legality_h.cpp", "-o", out / "bin/legality"]) + for k in (2, 4): + run(f"compile-columns{k}", [args.cxx, *compile_flags, f"-DKPAIRS={k}", checkers / "columns_k.cpp", + "-o", out / f"bin/columns{k}"]) + run("legality", [out / "bin/legality", local / "cin", local / "cout", local / "cout/legality.json"]) + records = local / "cout/COHORT249-RECORDS.bin" + run("five-stage", [out / "bin/columns2", records, local / "cout/columns.json"]) + run("nine-stage", [out / "bin/columns4", records, local / "cout/columns_k4.json"]) + native = read(local / "report.json") + legality = read(local / "cout/legality.json") + nine = read(local / "cout/columns_k4.json") + five = read(local / "cout/columns.json") + need(legality["common_frame_ADDs"] == nine["local_scalar_additions"] == native["candidate_bill"]["total_adds"], + "C++ addition census disagreement") + need(legality["rank_mass"] == 5112 and dict(nine["local_raw_H"]) == + {int(k): v for k, v in native["geometry"]["paid_profile"].items()}, "C++ recursive profile disagreement") + need(nine["formal_columns_checked"] == 1380 and five["formal_columns_checked"] == 900, + "C++ formal-column coverage") + need(len(nine["negative_controls"]) == 18 and all(c["rejected"] for c in nine["negative_controls"]), + "nine-stage omitted-bridge controls") + for item, key in zip(nine["signed_lift_prefix"], ("forward", "reverse")): + need(int(item["cancellation_free_signed_row_l1_upper"]) == native["candidate_bill"][key], + "C++ prefix disagreement") + need(nine["payload_prefix_upper"] == native["candidate_bill"]["five_stage_prefix"], + "C++ five-stage formula disagreement") + + # Detect errors in the serialized stream, not only in the word interpreter. + raw = list(struct.iter_unpack("<6i", records.read_bytes())) + first_basis = next(i for i, row in enumerate(raw) if row[0] == 1 and row[5] == 1) + first_helper = next(i for i, row in enumerate(raw) if row[0] == 1 and row[5] == 1 and row[2] >= 240) + first_copy = next(i for i, row in enumerate(raw) if row[0] == 2) + first_move = next(i for i, row in enumerate(raw) if row[0] == 0 and row[4] > 0) + mutations = [] + for name, index in (("omit-basis-add", first_basis), ("omit-helper-add", first_helper), ("omit-copy", first_copy)): + path = out / (name + ".bin") + path.write_bytes(b"".join(struct.pack("<6i", *row) for i, row in enumerate(raw) if i != index)) + reason = "bounderase" if name == "omit-copy" else "local defining-decoder full formal column" + run(name, [out / "bin/columns4", path, out / (name + ".json")], expected_error=reason) + mutations.append(name) + mutated = [list(row) for row in raw] + mutated[first_move][4] -= 1 + directory = out / "understated-move" + directory.mkdir() + for name in ("COHORT249-FRAMES.json", "COHORT249-INITIAL.json", "COHORT249-SELECTION.json"): + shutil.copyfile(local / "cout" / name, directory / name) + (directory / "COHORT249-RECORDS.bin").write_bytes(b"".join(struct.pack("<6i", *row) for row in mutated)) + run("understated-move", [out / "bin/legality", local / "cin", directory, directory / "receipt.json"], + expected_error="illegal or mispriced MOVE") + mutations.append("understated-move") + + python("geometry", predecessor / "code/nine/geometry.py", "--source", predecessor, "--out", local / "nine") + python("global", vk / "global_k.py", "--word", word, "--local-check", local, "--out", local / "nine", + "--isometries", predecessor / "data/eleven/residual-isometries.json") + python("adapt-audit", pricing / "code/adapt.py", vk, out / "adapted") + python("parent-audit", out / "adapted/audit_parent_k.py", "--local-check", local, + "--out", local / "nine", "--word", word) + python("host", vk / "emit_k.py", local / "nine", local, local / "hosted", + "--selection", ROOT / "research/e8-bit-r420/data/selection9-r420.json", "--key", "bit") + python("host-audit", vk / "audit_hosted_k.py", local, local / "hosted", local / "hosted/AUDIT.json") + + # The complex lower bound is a pinned input from the selected certificate, + # not a claim to have rebuilt the complex supplier in this bit-only replay. + selected = read(ROOT / "research/community-k492-audit/pr626/replay/ASSEMBLY.json") + assembly_root = out / "assembly-input" + engines = Path("code/hub/e8-r740-replica32/code/engines") + (assembly_root / engines).mkdir(parents=True) + for name in ("moment.py", "base_two_moment.py", "outer.py"): + shutil.copyfile(predecessor / engines / name, assembly_root / engines / name) + (assembly_root / "data").mkdir() + (assembly_root / "data/complex-b.json").write_text(json.dumps({ + "suppliers": [{"name": "selected626", "b": selected["complex_lower"]}]}) + "\n") + python("invoice", pricing / "code/assemble9.py", local, local / "hosted", local / "hosted/AUDIT.json", + assembly_root, out / "INVOICE.json", "selected626") + global_receipt = read(local / "nine/GLOBAL.json") + parent = read(local / "nine/AUDIT.json") + hosted = read(local / "hosted/AUDIT.json") + invoice = read(out / "INVOICE.json") + expected = read(ROOT / "research/e8-bit-r420/EXPECTED.json") + need(invoice["bit_profile"] == expected["nine"]["profile"], "hosted paid profile changed") + need(invoice["bit_lower"] == selected["bit_lower"], "bit saving changed") + need(invoice["kappa"]["selected626"]["kappa"] == selected["kappa"], "selected assembly not reproduced") + need(invoice["bit"]["charged_prefix_bits"] == 192 and + invoice["bit"]["charged_two_level_coefficient_bits"] == 512, "invoice allowance increased") + need(global_receipt["global_prefix_bound"] == native["candidate_bill"]["nine_stage_prefix"], + "global nine-stage prefix disagreement") + need(hosted["hosted_residuals"] == 120960 and hosted["bank_assignments"] == 0, + "hosted helper census changed") + geometry = read(local / "nine/GEOMETRY.json") + detail = {name: invoice_detail(native[name + "_bill"]["total_adds"], + int(native[name + "_bill"]["nine_stage_prefix"]), + hosted, global_receipt, geometry) + for name in ("original", "candidate")} + need(detail["candidate"]["coefficient_bits"] == invoice["bit"]["coefficient_bits"] and + detail["candidate"]["two_level_bits"] == invoice["bit"]["two_level_coefficient_bits"], + "expanded candidate invoice disagreement") + need(detail["original"]["coefficient_bits"] == expected["nine"]["bit"]["coefficient_bits"] and + detail["original"]["two_level_bits"] == expected["nine"]["bit"]["two_level_coefficient_bits"], + "expanded original invoice disagreement") + result = { + "status": "PASS_R420_TARGET_COMPENSATION_HOSTED", + "word_sha256": native["word_sha256"], + "local_adds": legality["common_frame_ADDs"], + "local_records": legality["records"], + "local_rank_mass": legality["rank_mass"], + "five_stage_columns": five["formal_columns_checked"], + "nine_stage_columns": nine["formal_columns_checked"], + "nine_stage_bridge_controls": len(nine["negative_controls"]), + "parent_unbanked_columns": global_receipt["independent_unbanked_scalar_columns"], + "parent_bridge_controls": len(global_receipt["omitted_bridge_shears_rejected"]), + "record_controls": mutations, + "parent_mutations_rejected": parent["mutations_rejected"], + "hosted_mutations_rejected": hosted["mutations_rejected"], + "hosted_events": hosted["emitted_events"], + "hosted_profile": hosted["profile"], + "hosted_residuals": hosted["hosted_residuals"], + "live": hosted["live"], + "physical": hosted["physical"], + "invoice": invoice["bit"], + "expanded_invoice": detail, + "unchanged_bit_lower": invoice["bit_lower"], + "cited_complex_lower": selected["complex_lower"], + "unchanged_kappa": invoice["kappa"]["selected626"]["kappa"], + "outer_strict_constraints": invoice["kappa"]["selected626"]["strict_outer_constraints"], + "outer_controls": invoice["kappa"]["selected626"]["outer_controls"], + } + certificate = HERE / "HOSTED-CERTIFICATE.json" + if args.write_certificate: + with certificate.open("x") as f: + json.dump(result, f, indent=2) + f.write("\n") + else: + need(result == read(certificate), "hosted certificate mismatch") + (out / "report.json").write_text(json.dumps(result, indent=2) + "\n") + pins(manifest) + print(f"PASS_R420_TARGET_COMPENSATION_HOSTED local_adds=19037 hosted_events={result['hosted_events']} " + "prefix_charge=192 coefficient_charge=512 kappa=unchanged", flush=True) + print("Replay files: " + str(out), flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/r420-target-compensation/requirements.txt b/research/r420-target-compensation/requirements.txt new file mode 100644 index 0000000000..fd3aa7c5b2 --- /dev/null +++ b/research/r420-target-compensation/requirements.txt @@ -0,0 +1,3 @@ +# Only the optional complete hosted replay needs these packages. +sympy==1.14.0 +mpmath==1.3.0 diff --git a/research/r420-target-compensation/search.py b/research/r420-target-compensation/search.py new file mode 100644 index 0000000000..fe6a9f8a3b --- /dev/null +++ b/research/r420-target-compensation/search.py @@ -0,0 +1,132 @@ +"""Bounded nomination, not an optimality proof. Apache-2.0; Codex assistance.""" + +import argparse +import json +import random +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from common import (HERE, N, R, V, bill, digest, fourth_root, make_word, need, + read_word, rows_of, search_context) + + +def nominate(original, seed=18, max_steps=1000, guarded=True): + rng = random.Random(seed) + rows = rows_of(original) + peak, extra, reverse_peak, entry = search_context(original) + need(peak == 144651 and reverse_peak == 144651, "unexpected exterior") + cap = fourth_root(((1 << 192) - 1) // ((1 << 18) * peak ** 5)) + fp, rp, helper = [1] * V, entry[V:2 * V], entry[2 * V:N] + need(len(helper) == R, "helper bound dimensions") + cache = {} + + def weight(mask): + if mask in cache: + return cache[mask] + original_mask, total = mask, 0 + while mask: + low = mask & -mask + total += helper[low.bit_length() - 1] + mask -= low + cache[original_mask] = total + return total + + # columns of the positive reverse basis matrix B; P is the forward + # basis applied to the relevant incoming norm vector (fp or rp). + columns = [{i: 1} for i in range(V)] + fo = [1 + row.bit_count() for row in rows] + ro = [rp[i] + weight(row) for i, row in enumerate(rows)] + operations, trace = [], [] + considered = admitted = 0 + stopping = "step_limit" + for _ in range(max_steps): + room_f = [min((peak - extra[i] - fo[i]) // (2 * c) for i, c in col.items()) + for col in columns] + room_r = [min((cap - ro[i]) // (2 * c) for i, c in col.items()) + for col in columns] + weights = [row.bit_count() for row in rows] + best, choices = 0, [] + for a in range(V): + for b in range(V): + if a == b: + continue + considered += 1 + gain = weights[a] - (rows[a] ^ rows[b]).bit_count() - 2 + if gain <= 0: + continue + new = rows[b] & ~rows[a] + df, dr = fp[b] + new.bit_count(), rp[b] + weight(new) + if guarded and (df > room_f[a] or dr > room_r[a]): + continue + admitted += 1 + if gain > best: + best, choices = gain, [(a, b, df, dr)] + elif gain == best: + choices.append((a, b, df, dr)) + if not choices: + stopping = "no_admissible_positive_gain_pair" + break + a, b, df, dr = rng.choice(choices) + for i, coefficient in columns[a].items(): + fo[i] += 2 * coefficient * df + ro[i] += 2 * coefficient * dr + for i, coefficient in columns[a].items(): + columns[b][i] = columns[b].get(i, 0) + coefficient + fp[a] += fp[b] + rp[a] += rp[b] + rows[a] ^= rows[b] + operations.append([a, b]) + trace.append([a, b, best, sum(r.bit_count() for r in rows) + 2 * len(operations), max(ro)]) + word, rebuilt_rows = make_word(original, operations) + actual = bill(word) + need(rows == rebuilt_rows and actual["reverse"] == max(ro), "incremental reverse bound mismatch") + need(actual["forward"] == max(peak, max(x + y for x, y in zip(fo, extra))), + "incremental forward bound mismatch") + if guarded: + need(actual["nine_stage_bits"] <= 192, "guard did not preserve the allowance") + return operations, { + "guarded": guarded, + "seed": seed, + "max_steps": max_steps, + "accepted_steps": len(operations), + "ordered_pairs_examined": considered, + "admissible_positive_pairs": admitted, + "stopping": stopping, + "trace_sha256": digest(trace), + "reverse_cap": cap if guarded else None, + "bill": actual, + } + + +def discover(): + original = read_word() + operations, guarded = nominate(original) + _, unrestricted = nominate(original, guarded=False) + return { + "format": "r420-compensation-target-basis-v1", + "assignment_seed": 18, + "original_word_sha256": digest(original), + "basis_operations": operations, + "search": {"guarded": guarded, "unrestricted_control": unrestricted}, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, + help="write a newly nominated candidate; refuses an existing file") + args = parser.parse_args() + candidate = discover() + if args.output: + with args.output.open("x") as f: + json.dump(candidate, f, indent=2) + f.write("\n") + else: + need(candidate == json.loads((HERE / "candidate.json").read_text()), + "search did not reproduce the frozen candidate") + print("PASS_REPRODUCIBLE_SEARCH guarded_steps=205 D_adds=12043 trials=2 seed=18") + + +if __name__ == "__main__": + main() diff --git a/research/r420-target-compensation/verify.py b/research/r420-target-compensation/verify.py new file mode 100644 index 0000000000..12aa1f0828 --- /dev/null +++ b/research/r420-target-compensation/verify.py @@ -0,0 +1,268 @@ +"""Exact finite verification, without rerunning the search. + +Apache-2.0; prepared with substantial OpenAI Codex assistance. +""" + +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +import sys +from collections import Counter +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from common import (HERE, N, R, ROOT, V, Reject, bill, canonical, digest, + make_word, need, norm_replay, read_word, rows_of, scalar_stream) + +XCHECK = "research/e8-bit-r420/code/xcheck.py" + + +def pins(manifest): + for name, expected in manifest["files"].items(): + need(hashlib.sha256((ROOT / name).read_bytes()).hexdigest() == expected, + "source pin mismatch: " + name) + + +def boundary(original, word): + """An exact transcript-level substitute for the old gate-local H2.""" + values = [1 << r for r in range(N)] + for frame, destination, sources in word["D"]: + need(frame == 0, "D left frame zero") + need(V <= destination < 2 * V, "D destination is not a target") + need(bool(sources) and len(set(sources + [destination])) == len(sources) + 1, + "D has duplicate or self operands") + need(all(type(s) is int and V <= s < N for s in sources), "D source outside target/helper rows") + for source in sources: + values[destination] ^= values[source] + expected = [1 << r for r in range(N)] + for t, row in enumerate(rows_of(original)): + expected[V + t] ^= row << (2 * V) + need(values == expected, "D boundary is not (x, y + K s, s)") + return digest(values) + + +def columns(word, reverse=False): + """A separate Boolean-column walk, including explicit copy/clear work. + + This does not import the symbolic-row engine or the scalar-stream builder. + The two implementations are computational cross-checks, not human review. + """ + phases = ["D", "A", "scatter", "B", "C"] + if reverse: + phases.reverse() + for column in range(N): + values = bytearray(N + 1) + values[column] = 1 + for section in phases: + if section == "scatter": + indices = range(len(word["ret"])) + if reverse: + indices = reversed(indices) + for k in indices: + values[N] = values[word["ret"][k]] + for t, row in enumerate(word["scatter"]): + if k in row: + values[V + t] ^= values[N] + values[N] = 0 + else: + gates = reversed(word[section]) if reverse else word[section] + for _, destination, sources in gates: + for source in sources: + values[destination] ^= values[source] + expected = bytearray(N + 1) + expected[column] = 1 + if column < V: + expected[V + column] = 1 + need(values == expected, f"column {column}, reverse={reverse}: bad full endpoint") + return N + + +def geometry(word, dimensions): + current = list(word["start"]) + paths = [[f] for f in current] + profile, moves = Counter(), 0 + + def visit(register, frame): + nonlocal moves + if current[register] != frame: + rank = dimensions[frame] - dimensions[current[register]] + need(rank > 0, "non-increasing frame visit") + profile[rank] += 1 + current[register] = frame + paths[register].append(frame) + moves += 1 + + for section in ("D", "A", "scatter", "B", "C"): + if section == "scatter": + for register in word["ret"]: + profile[dimensions[current[register]]] += 1 + else: + for frame, destination, sources in word[section]: + for register in [destination] + sources: + visit(register, frame) + for register, frame in enumerate(word["final"]): + visit(register, frame) + return { + "frame_paths_sha256": digest(paths), + "moves": moves, + "copies": len(word["ret"]), + "erasures": len(word["ret"]), + "helpers": word["R"], + "paid_profile": {str(k): v for k, v in sorted(profile.items())}, + "rank_mass": sum(k * v for k, v in profile.items()), + } + + +def budget(original_bill, result): + need(result["total_adds"] < original_bill["total_adds"], "no scalar saving") + need(result["forward"] <= original_bill["forward"], "larger forward allowance") + need(result["five_stage_bits"] <= 104, "five-stage prefix allowance exceeded") + need(result["nine_stage_bits"] <= 192, "nine-stage prefix allowance exceeded") + + +def controls(original, word, candidate, original_bill): + rejected = [] + + def rejects(name, thunk): + try: + thunk() + except Reject: + rejected.append(name) + else: + raise Reject("negative control accepted: " + name) + + def changed(gates): + return dict(word, D=gates) + + d = word["D"] + count = len(candidate["basis_operations"]) + rejects("omit one entrance basis gate", lambda: boundary(original, changed(d[1:]))) + rejects("omit one exit basis gate", lambda: boundary(original, changed(d[:-1]))) + wrong_inverse = d[:len(d) - count] + list(reversed(d[len(d) - count:])) + rejects("apply exit basis in forward order", lambda: boundary(original, changed(wrong_inverse))) + rejects("omit all entrance basis gates (zero targets would miss this)", + lambda: boundary(original, changed(d[count:]))) + # Explicitly exhibit the blind spot of a test restricted to zero targets. + values = [0] * V + [0] * V + [1 << r for r in range(R)] + for _, destination, sources in d[count:]: + for source in sources: + values[destination] ^= values[source] + need(values[V:2 * V] == rows_of(original), "zero-target blind-spot control changed") + wrong_middle = d[:count] + copy.deepcopy(original["D"]) + d[len(d) - count:] + rejects("inject K instead of E K", lambda: boundary(original, changed(wrong_middle))) + missing = copy.deepcopy(d) + missing[count][2].pop() + rejects("omit one dirty-helper injection", lambda: boundary(original, changed(missing))) + illegal = copy.deepcopy(d) + illegal[0][0] = 1 + rejects("basis operation at full frame", lambda: boundary(original, changed(illegal))) + illegal = copy.deepcopy(d) + illegal[count][2][0] = 0 + rejects("read a source at frame zero", lambda: boundary(original, changed(illegal))) + illegal = copy.deepcopy(d) + illegal[0][2][0] = illegal[0][1] + rejects("self XOR", lambda: boundary(original, changed(illegal))) + illegal = copy.deepcopy(d) + illegal[0][1] = 240 + rejects("write a helper", lambda: boundary(original, changed(illegal))) + # A neutral pair is a valid F2 circuit but is unacceptable to this paid budget. + _, reverse_values = norm_replay(scalar_stream(word), reverse=True) + source = V + max(range(V), key=lambda t: reverse_values[V + t]) + destination = V + (source - V + 1) % V + pair = [[0, destination, [source]], [0, destination, [source]]] + neutral = changed(pair + d) + need(boundary(original, neutral) == boundary(original, word), "neutral pair changed F2 map") + rejects("F2-neutral pair exceeds the prefix allowance", lambda: budget(original_bill, bill(neutral))) + bad_ops = copy.deepcopy(candidate["basis_operations"]) + bad_ops[0][0] = V + rejects("basis recipe uses an extra register", lambda: make_word(original, bad_ops)) + bad_pin = {"files": {"research/e8-bit-r420/data/bitE8mut-r420.json.gz": "0" * 64}} + rejects("incorrect immutable source pin", lambda: pins(bad_pin)) + return rejected + + +def verify(candidate): + original = read_word() + need(candidate["format"] == "r420-compensation-target-basis-v1", "candidate format") + need(candidate["assignment_seed"] == 18, "assignment seed") + need(candidate["original_word_sha256"] == digest(original), "candidate source mismatch") + word, reduced = make_word(original, candidate["basis_operations"]) + need(all(word[k] == original[k] for k in original if k != "D"), "outside D changed") + endpoint = boundary(original, word) + spec = importlib.util.spec_from_file_location("predecessor_xcheck", ROOT / XCHECK) + predecessor = importlib.util.module_from_spec(spec) + spec.loader.exec_module(predecessor) + base = predecessor.Word(original) + labels, base_full = base.labels(), base.full() + base_h, base_c, _ = base.interface() + need(all(base_h.values()) and all(base_c.values()), "baseline interface failure") + check = predecessor.Word(word) + full = check.full() + h, c, _ = check.interface() + need(all(v for k, v in h.items() if k != "H2_D_frame0_targets_from_helpers"), "unchanged hypothesis failed") + need(all(v for k, v in c.items() if k != "K_equals_D"), "unchanged conclusion failed") + # The old gate-local predicate and its direct-summation K calculation really + # do reject this circuit. They are replaced by the checked D boundary above. + need(h["H2_D_frame0_targets_from_helpers"] is False and c["K_equals_D"] is False, + "expected old interface rejection not observed") + before, after = bill(original), bill(word) + budget(before, after) + old_geometry, new_geometry = geometry(original, base.fdim), geometry(word, check.fdim) + need(old_geometry == new_geometry, "frame/copy/recursive profile changed") + need(after == candidate["search"]["guarded"]["bill"], "nomination bill mismatch") + coverage = [columns(word, reverse) for reverse in (False, True)] + negative = controls(original, word, candidate, before) + result = { + "status": "PASS_R420_TARGET_COMPENSATION", + "original_word_sha256": digest(original), + "word_sha256": digest(word), + "basis_operations": len(candidate["basis_operations"]), + "helper_injections": sum(r.bit_count() for r in reduced), + "reduced_matrix_sha256": digest(reduced), + "D_boundary_sha256": endpoint, + "labels": labels, + "native_columns": [base_full["columns"], full["columns"]], + "separate_column_walk_forward_reverse": coverage, + "original_bill": before, + "candidate_bill": after, + "geometry": new_geometry, + "saved_local_adds": before["total_adds"] - after["total_adds"], + "saved_9_stage_32_replica_adds": 9 * 32 * (before["total_adds"] - after["total_adds"]), + "old_gate_local_H2_accepts": False, + "replacement_D_boundary_accepts": True, + "negative_controls": negative, + } + return result, word + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="new output directory for the word and report") + parser.add_argument("--write-certificate", action="store_true", help="create a missing certificate after fresh verification") + args = parser.parse_args() + need(not sys.flags.optimize, "assertions must remain enabled in predecessor checks") + manifest = json.loads((HERE / "SOURCES.json").read_text()) + pins(manifest) + candidate = json.loads((HERE / "candidate.json").read_text()) + result, word = verify(candidate) + certificate = HERE / "CERTIFICATE.json" + if args.write_certificate: + with certificate.open("x") as f: + json.dump(result, f, indent=2) + f.write("\n") + else: + need(result == json.loads(certificate.read_text()), "certificate mismatch") + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + (args.output / "word.json.gz").write_bytes(gzip.compress(canonical(word), mtime=0)) + (args.output / "report.json").write_text(json.dumps(result, indent=2) + "\n") + pins(manifest) + print(f"PASS_R420_TARGET_COMPENSATION D=19922->12043 total=26916->19037 " + f"columns=660 rank_mass=5112 nine_bits=192 controls={len(result['negative_controls'])}") + + +if __name__ == "__main__": + main()