From 085c32a25e2a09b029fa816195b97fa93d6f0788 Mon Sep 17 00:00:00 2001 From: ross Date: Tue, 13 Oct 2026 23:23:02 +1100 Subject: [PATCH] Research: compose CK target and helper compensation bases --- research/complex-ck-two-sided/CLAIM.md | 42 + research/complex-ck-two-sided/EXPECTED.json | 240 ++ research/complex-ck-two-sided/NOTICE.md | 31 + research/complex-ck-two-sided/PROOF.md | 115 + research/complex-ck-two-sided/README.md | 108 + research/complex-ck-two-sided/RECIPE.json | 2377 +++++++++++++++++ research/complex-ck-two-sided/SOURCES.json | 41 + research/complex-ck-two-sided/VALIDATION.md | 62 + research/complex-ck-two-sided/experiment.py | 284 ++ research/complex-ck-two-sided/independent.py | 307 +++ .../complex-ck-two-sided/test_independent.py | 99 + research/complex-ck-two-sided/test_package.py | 95 + research/complex-ck-two-sided/verify.py | 156 ++ 13 files changed, 3957 insertions(+) create mode 100644 research/complex-ck-two-sided/CLAIM.md create mode 100644 research/complex-ck-two-sided/EXPECTED.json create mode 100644 research/complex-ck-two-sided/NOTICE.md create mode 100644 research/complex-ck-two-sided/PROOF.md create mode 100644 research/complex-ck-two-sided/README.md create mode 100644 research/complex-ck-two-sided/RECIPE.json create mode 100644 research/complex-ck-two-sided/SOURCES.json create mode 100644 research/complex-ck-two-sided/VALIDATION.md create mode 100644 research/complex-ck-two-sided/experiment.py create mode 100644 research/complex-ck-two-sided/independent.py create mode 100644 research/complex-ck-two-sided/test_independent.py create mode 100644 research/complex-ck-two-sided/test_package.py create mode 100644 research/complex-ck-two-sided/verify.py diff --git a/research/complex-ck-two-sided/CLAIM.md b/research/complex-ck-two-sided/CLAIM.md new file mode 100644 index 0000000000..be693fd39e --- /dev/null +++ b/research/complex-ck-two-sided/CLAIM.md @@ -0,0 +1,42 @@ +# Sprint claim: CK two-sided compensation (seed 38) + +- Track: complex supplier; OS-random assignment seed **38** (`secrets.randbelow(100)`). +- Start: 2026-10-13 12:01:59 UTC. Expected finish: **2026-10-13 12:42 UTC** (23:42 Melbourne). +- Exact base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +- Selected record at base: reviewed conditional PR799, kappa `0.001661634653669567`. +- Object: historical PR626 CK provider's frame-zero arbitrary-helper compensation. +- Hypothesis: after a signed target-forest transform, disjoint signed helper shears + can reduce the complete compensation bill further. Reprice the transformed + matrix; do not add independent savings from PR807 and PR816. +- Method: exact dyadic matrix arithmetic, a signed target forest, then a bounded + all-ordered-helper-pair/sign census and deterministic disjoint greedy selection. + Seed 38 diversifies forest/pair tie breaks. Charge preparation and restoration + on both sides, literal coefficient work, source reads, and unchanged children. +- Expected deliverable: one executable finite circuit with exact replay and pins, + or a scoped negative result if the complete budget fails. No new kappa. +- Candidates considered: X4 helper pairs (obvious follow-up to PR901); this + two-sided CK compensation (selected); JP8 coefficient routes (crowded by + PR793/811/837/839/882). This changes the search class, not only its seed. +- Coordination: GitHub returned zero pinned issues. Local claim used. Refreshed + 703 open PRs through #912 before claiming; read PR807/816/901/909 and relevant + accepted ledger/review. PR807 changes helpers alone; PR816 targets alone. + No pending source code is imported. Credit and exact predecessor pins will + accompany the result. Delegated work stays within this compensation scope. +- Budget: at most first 8 minutes for orientation; final 10 minutes reserved + for verification and handoff. + +## Completed result (single claim update) + +Completed finite circuit construction: 106 target-forest edges and 112 disjoint +helper pairs reduce the complete compensation bill from 49,624 to 11,965 +component primitives. Both full orientations save 75,318 real primitives, +including 8,798 beyond the target-only forest. All 725 arbitrary input columns, +both arithmetic engines, native frame/wrapper checks, 10 new and 25 inherited +controls pass. Prefixes are 41/65 bits; denominator budgets remain 3/8 bits. +No new kappa and no claim of joint optimality or global admission. + +Result: [exact receipt](EXPECTED.json), [construction proof](PROOF.md), and +[validation/handoff](VALIDATION.md). Branch: `research/complex-seed38`. +The final refresh found no pinned issue and 705 open PRs through #915; no +overlapping two-sided CK contribution was found. PR807/816 are credited as +precursors, with complete repricing rather than an additive savings claim. diff --git a/research/complex-ck-two-sided/EXPECTED.json b/research/complex-ck-two-sided/EXPECTED.json new file mode 100644 index 0000000000..1268b94e77 --- /dev/null +++ b/research/complex-ck-two-sided/EXPECTED.json @@ -0,0 +1,240 @@ +{ + "status": "FINITE_CK_TWO_SIDED_COMPENSATION_NO_NEW_KAPPA", + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "seed": 38, + "source_pins_sha256": "5db1688947b52af69d4670c159b994e6ceb927f7a1fce0656d2459ad7dab9c2d", + "recipe_sha256": "a77b4cc1bdf70b52fb000cc75040afd253a63beb72139616232ebbfd58cbd437", + "columns": { + "logical": 716, + "private": 9 + }, + "search": { + "target_edges": 12544, + "helper_cases": 128524, + "profitable_helper_cases": 1525, + "target_basis_edges": 106, + "helper_pairs": 112 + }, + "panel_component_prices": { + "baseline": 49624, + "target_only": 16364, + "two_sided": 11965 + }, + "programs": { + "forward": { + "baseline": { + "real_primitives": 224938, + "prefix_l1": "920709848294", + "prefix_bits": 40, + "maximum_denominator_power": 3, + "program_sha256": "24d4fdd9641278242add4c3ed9843e138e04f6a54d067cf6b755f6bcba84978f", + "primitive_word_sha256": "76f540eb9b679eb33a9b22c7f1ad96063c70dd1e84171e5c42eb3e7f824da8ef", + "scalar_macros": 21936, + "primitive_counts": { + "add": 44127, + "clear": 42902, + "copy": 8, + "double": 5585, + "halve": 19499, + "negate": 348 + } + }, + "candidate": { + "real_primitives": 149620, + "prefix_l1": "1200150150114", + "prefix_bits": 41, + "maximum_denominator_power": 3, + "program_sha256": "46cbc67d4bf6768e7531a2c31f7a5105ef2f572d25045f0ce8877b41d8e30356", + "primitive_word_sha256": "228baefc17e57c5d499b4118af5f1d3336ce4a102eca82f2a8d7e43a65ab182b", + "scalar_macros": 15773, + "primitive_counts": { + "add": 31582, + "clear": 30576, + "copy": 8, + "double": 5374, + "halve": 6922, + "negate": 348 + } + }, + "real_saved": 75318, + "additional_real_saved_vs_target_forest": 8798 + }, + "backward": { + "baseline": { + "real_primitives": 224986, + "prefix_l1": "146068000389976309073/32", + "prefix_bits": 62, + "maximum_denominator_power": 8, + "program_sha256": "314b814a33d1339c7862112a4c927c19af0aee03dead0f841c983814a9f24d58", + "primitive_word_sha256": "ae56e8b527f88897d4b8be72f142666f5e159c424a567e61adfebd643a0260b8", + "scalar_macros": 21936, + "primitive_counts": { + "add": 44143, + "clear": 42918, + "double": 5585, + "halve": 19499, + "negate": 348 + } + }, + "candidate": { + "real_primitives": 149668, + "prefix_l1": "626977768061479717259/32", + "prefix_bits": 65, + "maximum_denominator_power": 8, + "program_sha256": "326571ffa80b1fc7c60a2c5316396cccfbac75e83913da9f0d5132f9da264f95", + "primitive_word_sha256": "60df568ec2923dfac35c53ca86135dcead61c33bd167fe69a8a94a1a709415e3", + "scalar_macros": 15773, + "primitive_counts": { + "add": 31598, + "clear": 30592, + "double": 5374, + "halve": 6922, + "negate": 348 + } + }, + "real_saved": 75318, + "additional_real_saved_vs_target_forest": 8798 + } + }, + "independent_recipe": { + "method": "Prim signed-forest minimum; exhaustive ordered signed helper-pair census", + "baseline_panel_price": 49624, + "target_minimum": 16364, + "helper_search": { + "cases": 128524, + "profitable": 1525, + "census_sha256": "7969fdd428e83a60a965c02b94ee906357ed53683fd705933f224214c0e069bf", + "gain": 4399 + }, + "complete_panel_price": 11965 + }, + "native": { + "checks": { + "forward": { + "sha256": "46cbc67d4bf6768e7531a2c31f7a5105ef2f572d25045f0ce8877b41d8e30356", + "events": 21093, + "scalar_macros": 15773, + "real_component_primitive_bound": 149620, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "all_columns": 716, + "private_centers_cleared": true, + "private_coefficient_stream_cleared_after_each_macro": true + }, + "backward": { + "sha256": "326571ffa80b1fc7c60a2c5316396cccfbac75e83913da9f0d5132f9da264f95", + "events": 21093, + "scalar_macros": 15773, + "real_component_primitive_bound": 149668, + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "all_columns": 716, + "private_centers_cleared": true, + "private_coefficient_stream_cleared_after_each_macro": true + } + }, + "local": { + "forward": { + "all_exact_columns": 716, + "prefix_l1_upper": "1200150150114", + "prefix_bits_upper": 41, + "charged_payload_bits": 192, + "private_work_erased": true + }, + "backward": { + "all_exact_columns": 716, + "prefix_l1_upper": "626977768061479717259/32", + "prefix_bits_upper": 65, + "charged_payload_bits": 192, + "private_work_erased": true + } + }, + "paid_profiles": { + "forward": { + "1": 2596, + "2": 552, + "4": 160, + "8": 8, + "3": 304, + "5": 70, + "6": 8 + }, + "backward": { + "1": 2596, + "2": 552, + "4": 160, + "8": 8, + "3": 304, + "5": 70, + "6": 8 + } + }, + "negative_controls_rejected": [ + "wrong_scale", + "missing_center", + "wrong_common_frame", + "wrong_child_rank", + "missing_pre_wrapper", + "missing_post_wrapper", + "wrapper_with_wrong_frame", + "wrapper_in_wrong_phase", + "wrapper_on_a_data_register", + "wrapper_on_a_target_register", + "wrapper_on_a_centre_register", + "hpe_pre_wrapper_resolved_to_full_recipe", + "hpe_post_wrapper_without_terminal_frame", + "hpe_post_wrapper_wrong_terminal_frame", + "hpe_tail_gate_at_full_frame", + "hpe_tail_climb_dropped", + "hpe_helper_exit_adapter_to_full", + "hpe_tail_gate_moved_into_full_cleanup", + "cold_hpe_pre_wrapper_replaced_by_identity_entry_adapter", + "cold_hpe_pre_wrapper_dropped", + "cold_hpe_post_wrapper_replaced_by_exit_adapter", + "cold_hpe_pre_wrapper_resolved_to_cold_full_convention", + "cold_hpe_wrapper_with_nonzero_entrance", + "cold_hpe_post_wrapper_wrong_terminal_frame", + "cold_hpe_premix_gate_before_pre_wrapper" + ], + "logs": { + "hpe_emit_local.py": [ + "PASS emitted forward 21093 events", + "PASS emitted backward 21093 events" + ], + "hpe_audit_local.py": [ + "independent emitted replay PASS forward", + "independent emitted replay PASS backward", + "PASS_INDEPENDENT_LOCAL_SCALAR_FRAME_AND_WRAPPER_REPLAY 25 controls rejected" + ] + } + }, + "controls": { + "rejected": [ + "omitted_target_preparation", + "omitted_helper_preparation", + "omitted_helper_restoration", + "omitted_target_restoration", + "reversed_target_preparation", + "reversed_target_restoration", + "wrong_helper_preparation_sign", + "wrong_residual_sign", + "cold_wrapped_helper_access", + "omitted_initial_work_clear" + ], + "omitted_target_preparation_passes_helper_only": true + } +} diff --git a/research/complex-ck-two-sided/NOTICE.md b/research/complex-ck-two-sided/NOTICE.md new file mode 100644 index 0000000000..a3092796ce --- /dev/null +++ b/research/complex-ck-two-sided/NOTICE.md @@ -0,0 +1,31 @@ +# Attribution and license + +New contribution by **Ross Richardson (@RossRichardson)**, with substantial +**OpenAI Codex assistance** for research selection, construction, code, proofs, +verification and writing. A separate AI worker implemented the integer-dyadic +checker and Prim/census check without importing the construction algorithm; +another reviewed the two-sided identity and native interface. This is not +independent human peer review. New files use the repository's **Apache-2.0** +license; see `../../LICENSE`. + +The mechanism combines and reprices ideas from: + +- **David Awad, PR807**, restored CK helper pairs, + `b1a5c533a22c2665600102d872f6a84e0664a70d`. +- **@dd-hemant, PR816**, signed CK target forests, + `133735a2cc2319c12ba5d786214b2217e083e7da`. +- **Sricharan Vagvala, PR749**, rational JP8 restored target pairs; and + **Oscar Fennell, PR759**, binary target forests and superroot reduction, + as credited by PR816. + +No pending implementation is copied or vendored. The new construction and +checker are written for this experiment. No additive combination of predecessor +savings is assumed, and no priority claim is made for either individual basis +mechanism. + +The unchanged retained inputs and native scripts carry their existing notices: +**icekylinx**'s PR425/433 scalar/compiler lineage, **DreamingOfClouds**' framed +extensions, **Jeremy Kothe**'s PR622 supplier and **Chafik Boukhalfa**'s PR626 +owner-repair package, with the earlier cold-end, frame, residual, source-gauge, +physical-owner, bit-supplier and recurrence contributors recorded in the +repository's `CONTRIBUTORS.md`. Those notices and source files remain unchanged. diff --git a/research/complex-ck-two-sided/PROOF.md b/research/complex-ck-two-sided/PROOF.md new file mode 100644 index 0000000000..21bbe41899 --- /dev/null +++ b/research/complex-ck-two-sided/PROOF.md @@ -0,0 +1,115 @@ +# Finite two-sided compensation identity and price + +Let `y` be the 112 target registers and `h` the 254 helper registers read by +PR626 CK compensation. Its map is `(y,h) -> (y+C h,h)`, with entries of `C` +in `(1/4) Z`. All relevant registers start in frame zero. The source helpers +also end at the full frame: none requires an entrance wrapper before access. +These properties are checked from the historical SPEC-bound canonical word. +The preceding precondition is retained, so `y` and `h` are arbitrary inputs. + +## Circuit + +For a signed target forest, define `(T y)_t = y_t - s_t y_parent(t)` on nonroots +and `(T y)_t=y_t` on roots. Prepare its shears deepest-first, so each parent is +read in its original basis. This produces `T y`; it also gives the literal +row formula `(T C)_t=C_t-s_t C_parent(t)`. The inverse reverses the chronological +preparation list and negates its coefficients. + +Next prepare disjoint helper shears `h_a += s h_b`, with `s` in `{-1,+1}`; +let their product be `H`. Since every helper occurs in at most one pair, the +updates commute and `H^-1` negates their coefficients. Right multiplication +of `D=T C` by `H^-1` changes exactly column `b` to `D_b-s D_a` in each pair. +Use the columns of `D`, not the original `C`, to compute this residual. + +The emitted chronological circuit is + +```text +y <- T y +h <- H h +y <- y + (T C H^-1) h +h <- H^-1 h +y <- T^-1 y +``` + +Hence its output is `T^-1(T y + T C H^-1 H h)=y+C h`, with helpers restored. +Every step is an explicit frame-zero scalar addition. No extra register, +recursive child, source copy or unpriced boundary work is used. The target +and helper bank preparation commute across banks, but target internal order +must remain as specified. + +For a logical addition `E=I+q e_t e_s^T`, `E^-T=I-q e_s e_t^T`. Mapping each +logical gate to this dual in the **same chronological order** dualizes the +whole map, because `(AB)^-T=A^-T B^-T`. Consequently the candidate backward +panel equals the inherited `(y,h)->(y,h-C^T y)`. Helpers at that panel boundary +need not equal their inputs; the rest of the complete backward program restores +them. Dualize the logical additions before lowering. The destructive private +clears themselves are not asserted to be invertible. + +## Exact complete price + +For reduced nonzero `q=a/2^d`, the inherited binary-Horner price in one component +is `p(q)=3+floor(log2|a|)+popcount(|a|)+d`. Set `p(0)=0` because zero entries emit +no gate. The initial work clear, every source accumulation and doubling, each +halving, signed target accumulation, and final clear are included. A unit shear +costs four component primitives, so preparation plus restoration costs eight. +Applying the same scalar arithmetic to real and imaginary parts doubles prices. + +For a fixed signed target forest with `e_T` edges, and fixed disjoint helper +pairs with `e_H` edges, the compensation price is exactly + +```text +8 e_T + 8 e_H + sum_(i,j) p((T C H^-1)_(i,j)). +``` + +The target-only forest is obtained by a minimum spanning tree on the 112 target +rows and a superroot: root-edge price `sum_j p(C_ij)` and signed-edge price +`8+sum_j p(C_ij-s C_kj)`. Edge prices are symmetric since `p(q)=p(-q)`. Removing +the superroot gives the forest, and the chronological schedule above realizes +its cost. A separately implemented Prim algorithm corroborates the Kruskal +price. This standard reduction proves a floor only within the target-only +signed-unit forest class; it says nothing about the joint two-sided optimum. + +For one helper choice `(a,b,s)` on `D=T C`, the complete saving is +`sum_i[p(D_ib)-p(D_ib-s D_ia)]-8`. Scores add for register-disjoint pairs since +they change different columns and do not modify each other's source columns. +The greedy selection is a construction, not a maximum-weight matching proof. + +| Compensation stage | Component primitives | +|---|---:| +| Original `C` | 49,624 | +| Target forest, including 212 basis gates | 16,364 | +| Two-sided, including 212 target and 224 helper basis gates | 11,965 | + +The residual has 2,105 nonzero additions, yielding 2,541 total additions. +The helper stage saves 4,399 component primitives beyond the target-only +forest. Therefore both complete orientations save +`2(49,624-11,965)=75,318` real primitives, including `2(4,399)=8,798` beyond +that target-only price. No pricing improvement outside compensation is used. + +## Prefixes, children and verification limits + +Starting from norm one for every independent input, propagate a positive +envelope through every literal primitive: addition sums norms, doubling/halving +scale them, copying copies the norm, and clearing sets it to zero. This gives +an upper bound on every scalar row norm, including work values before division. +The candidate maxima are `1200150150114` forward and +`626977768061479717259/32` backward (41 and 65 bits). Both are strictly below +`2^192`; the higher bounds are reported rather than assumed unchanged. +The largest reduced dyadic denominator exponent across every intermediate +symbolic row remains 3 forward and 8 backward, equal to the original programs. +Both arithmetic engines check this separately from the magnitude envelope. + +The native paid histogram remains +`{1:2596,2:552,3:304,4:160,5:70,6:8,8:8}`: 3,698 children. +All non-scalar events retain their literal order, including center operations, +frame climbs, residual wrappers and adapters. No changed asymptotic recurrence +or κ follows from this finite scalar saving. Global hosting/invoice admission +and all-size/analytic obligations remain outside this contribution. + +Two new arithmetic implementations check the full original/candidate scalar +projections in both directions on 725 independent input columns. The unchanged +native emitter/auditor separately checks the finite common-frame and wrapper +contract on all 716 logical columns, with its 25 original rejection controls. +Ten new controls include omitted target preparation: it passes a helper-only +projection and fails arbitrary-target checking, illustrating why all-column +replay is required. These finite checks do not formalize the full theorem. diff --git a/research/complex-ck-two-sided/README.md b/research/complex-ck-two-sided/README.md new file mode 100644 index 0000000000..e08efda490 --- /dev/null +++ b/research/complex-ck-two-sided/README.md @@ -0,0 +1,108 @@ +# Two-sided CK compensation: 8,798 real primitives beyond target forests + +**Finite complex-supplier circuit construction; no new κ.** On the historical +PR626 CK provider, a signed target forest followed by disjoint signed helper +shears reduces the frame-zero compensation from 8,704 to **2,541 additions**. +The complete local programs save **75,318 real-component primitives each**. +This is **8,798 beyond the 66,520 saving of the target-forest class alone**. + +| Complete scalar program | Original | Two-sided | Saving | +|---|---:|---:|---:| +| Forward | 224,938 | 149,620 | 75,318 | +| Inverse transpose | 224,986 | 149,668 | 75,318 | +| Scalar macros, either orientation | 21,936 | 15,773 | 6,163 | + +These are exact circuit counts, not elapsed-time measurements. Every source +access, coefficient preparation, target/helper basis change and restoration, +private clear, and unchanged scalar operation is charged. The paid recursive +histogram, all non-scalar events, helper inventory and physical frames are +unchanged. All 492 helpers restore at the complete local endpoint. The positive +prefix bounds rise from 40/62 to **41/65 bits**, within the inherited **192-bit +local allowance**; no unchanged global precision invoice is asserted. +The maximum exact symbolic denominator powers remain **3 forward and 8 +backward**, checked at every literal primitive, including transient work. + +## Reproduction + +From the repository root, with Python 3.10+ and its standard library: + +```sh +python3 -I -B research/complex-ck-two-sided/verify.py +``` + +Expected final line: + +```text +PASS_CK_TWO_SIDED target_edges=106 helper_pairs=112 cases=128524 saved_real=75318 additional_vs_target=8798 columns=716+9 orientations=2 controls=10+25 no_new_kappa +``` + +The default command checks the committed recipe and receipt without rewriting +them. It recomputes the whole search, replays both complete original/candidate +programs with Fraction arithmetic and a separately implemented integer-dyadic +checker, and runs the unchanged native emitter and frame/wrapper auditor in a +temporary directory. `--record` deliberately replaces this package's recipe +and expected receipt only after all mathematical checks pass. The package has +no third-party dependency and works when invoked outside the repository. + +`RECIPE.json` specifies all target edges, helper pairs, costs and census hashes. +`EXPECTED.json` binds both literal primitive words, complete scalar counts, +prefix bounds, native paid profiles and control results. The accompanying tests +exercise source/receipt corruption and the separate arithmetic implementation. + +## What is new, and what is inherited + +David Awad's [PR807](https://github.com/CrocSwap/integer-mult-bounds/pull/807) +changes the CK helper basis alone. @dd-hemant's +[PR816](https://github.com/CrocSwap/integer-mult-bounds/pull/816) changes its target +basis alone, following Sricharan Vagvala's rational target pairs in #749 and +Oscar Fennell's binary target forests in #759. This contribution **reprices and +constructs helper changes after the target transformation**. It does not add +the two earlier independent savings. The row and column mechanisms interact: +the two-sided saving is 75,318, not 66,520 + 35,872. + +No pending implementation is imported. The target forest has the same 16,364 +component-primitive price as PR816; seed 38 selects a particular tied forest. +The additional evidence is the complete, explicitly restored two-sided circuit +and its literal checks. The separate checker uses a different Prim algorithm +to confirm the target-only floor and independently redoes the helper census. +No joint optimum, best matching, or asymptotic improvement is claimed. + +The exact base is **`f567884aeb8851b6e794af1184119a3bfbe1e631`**. At this base the +selected conditional result is PR799, **κ = 0.001661634653669567**. The experiment +intentionally uses the retained PR626 CK checkpoint, pinned to +`660de893d27bb7abd1d5b01b1640207528a5c851`, with PR622 source +`f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`. It does not transport the result to X4. +`SOURCES.json` records exact source digests, the historical SPEC binding, and +pending predecessor heads. Compressed inputs are checked by their decompressed +payloads; their original container digests are retained as provenance only. + +## Bounded search and scope + +The OS-random track seed is **38**. The search is exhaustive over **12,544** +signed/root target edges and then **128,524** ordered helper-pair/sign choices +on that selected target forest. **1,525** helper choices have positive complete +savings. One deterministic greedy pass selects **112 disjoint pairs**. +SHA-256 of seed 38 and a candidate breaks equal-price ties. All target edges are +priced; Kruskal stops after completing its tree. The helper pass stops after +examining every profitable sorted candidate; all pair scores were computed. +There is no time cutoff or omitted part of this finite domain. The helper-pair space is assessed on the transformed +matrix, so this is not a repeat of the helper-only search with another seed. + +The result permits arbitrary data, target and helper inputs, plus arbitrary +private centers and coefficient work on entry. In the forward compensation +panel helpers are restored; in the inverse-transpose panel their prescribed +change is `h <- h - C^T y`. Both complete programs restore their helper inputs. +The private centers and work erase via the inherited charged clears. + +Adopting this alternative compensation syntax in the production constructor, +rebinding artifacts, and refreshing the complete global owner/invoice/assembly +remain separate work. The paid child profile and recurrence exponent do not +change. Uniform compilation, common-label/mutable-source realization, whole-call +hosting, precision/tape and analytic transfer remain inherited assumptions. +The scalar projection ignores non-scalar child action; the unchanged native +checker separately validates finite frames, wrappers and child counts. This is +not a proof of the full multiplication theorem or a cold construction replay. + +See [PROOF.md](PROOF.md) for the circuit identity and complete price, +[VALIDATION.md](VALIDATION.md) for executed checks, and [NOTICE.md](NOTICE.md) +for attribution and substantial AI-assistance disclosure. diff --git a/research/complex-ck-two-sided/RECIPE.json b/research/complex-ck-two-sided/RECIPE.json new file mode 100644 index 0000000000..17063955a6 --- /dev/null +++ b/research/complex-ck-two-sided/RECIPE.json @@ -0,0 +1,2377 @@ +{ + "seed": 38, + "targets": [ + 112, + 113, + 114, + 115, + 116, + 117, + 118, + 119, + 120, + 121, + 122, + 123, + 124, + 125, + 126, + 127, + 128, + 129, + 130, + 131, + 132, + 133, + 134, + 135, + 136, + 137, + 138, + 139, + 140, + 141, + 142, + 143, + 144, + 145, + 146, + 147, + 148, + 149, + 150, + 151, + 152, + 153, + 154, + 155, + 156, + 157, + 158, + 159, + 160, + 161, + 162, + 163, + 164, + 165, + 166, + 167, + 168, + 169, + 170, + 171, + 172, + 173, + 174, + 175, + 176, + 177, + 178, + 179, + 180, + 181, + 182, + 183, + 184, + 185, + 186, + 187, + 188, + 189, + 190, + 191, + 192, + 193, + 194, + 195, + 196, + 197, + 198, + 199, + 200, + 201, + 202, + 203, + 204, + 205, + 206, + 207, + 208, + 209, + 210, + 211, + 212, + 213, + 214, + 215, + 216, + 217, + 218, + 219, + 220, + 221, + 222, + 223 + ], + "sources": [ + 224, + 225, + 226, + 227, + 228, + 229, + 230, + 231, + 232, + 233, + 235, + 236, + 237, + 238, + 239, + 240, + 241, + 242, + 243, + 244, + 245, + 246, + 247, + 248, + 249, + 251, + 252, + 253, + 254, + 255, + 256, + 257, + 258, + 259, + 260, + 261, + 262, + 263, + 264, + 265, + 267, + 268, + 269, + 270, + 271, + 272, + 273, + 274, + 275, + 276, + 277, + 278, + 279, + 280, + 283, + 284, + 285, + 286, + 287, + 288, + 289, + 290, + 291, + 292, + 293, + 294, + 295, + 296, + 299, + 300, + 301, + 302, + 303, + 304, + 305, + 306, + 307, + 308, + 309, + 310, + 311, + 312, + 315, + 316, + 317, + 318, + 319, + 320, + 321, + 322, + 323, + 324, + 325, + 326, + 327, + 328, + 331, + 332, + 333, + 334, + 335, + 336, + 337, + 338, + 339, + 340, + 341, + 342, + 343, + 344, + 347, + 348, + 349, + 350, + 351, + 352, + 353, + 354, + 355, + 356, + 357, + 358, + 359, + 360, + 363, + 364, + 365, + 366, + 367, + 368, + 369, + 370, + 371, + 372, + 373, + 374, + 375, + 376, + 379, + 380, + 381, + 382, + 383, + 384, + 385, + 386, + 387, + 388, + 389, + 390, + 391, + 392, + 395, + 396, + 397, + 398, + 399, + 400, + 401, + 402, + 403, + 404, + 405, + 406, + 407, + 408, + 409, + 411, + 412, + 413, + 414, + 415, + 416, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 427, + 428, + 429, + 430, + 431, + 432, + 433, + 434, + 435, + 436, + 437, + 438, + 439, + 440, + 441, + 443, + 444, + 445, + 446, + 447, + 460, + 462, + 464, + 466, + 469, + 470, + 471, + 472, + 473, + 474, + 475, + 476, + 485, + 487, + 496, + 497, + 498, + 499, + 505, + 507, + 509, + 511, + 516, + 517, + 518, + 519, + 520, + 521, + 522, + 523, + 536, + 537, + 548, + 549, + 552, + 553, + 554, + 555, + 560, + 561, + 564, + 566, + 572, + 573, + 575, + 577, + 580, + 582, + 589, + 590, + 591, + 592 + ], + "target_forest": [ + [ + 20, + 37, + 1, + 8 + ], + [ + 41, + 42, + 1, + 8 + ], + [ + 14, + 15, + 1, + 7 + ], + [ + 21, + 36, + 1, + 7 + ], + [ + 37, + 36, + 1, + 7 + ], + [ + 42, + 53, + 1, + 7 + ], + [ + 47, + 46, + 1, + 7 + ], + [ + 52, + 105, + 1, + 7 + ], + [ + 15, + 106, + -1, + 6 + ], + [ + 25, + 79, + 1, + 6 + ], + [ + 36, + 110, + -1, + 6 + ], + [ + 46, + 110, + 1, + 6 + ], + [ + 53, + 106, + 1, + 6 + ], + [ + 56, + 38, + 1, + 6 + ], + [ + 87, + 7, + 1, + 6 + ], + [ + 93, + 58, + 1, + 6 + ], + [ + 98, + 48, + 1, + 6 + ], + [ + 105, + 106, + 1, + 6 + ], + [ + 111, + 110, + 1, + 6 + ], + [ + 3, + 66, + 1, + 5 + ], + [ + 7, + 81, + 1, + 5 + ], + [ + 38, + 12, + -1, + 5 + ], + [ + 48, + 24, + -1, + 5 + ], + [ + 58, + 6, + -1, + 5 + ], + [ + 79, + 9, + 1, + 5 + ], + [ + 86, + 1, + 1, + 5 + ], + [ + 89, + 9, + 1, + 5 + ], + [ + 94, + 61, + 1, + 5 + ], + [ + 102, + 19, + 1, + 5 + ], + [ + 106, + 9, + 1, + 5 + ], + [ + 110, + 81, + -1, + 5 + ], + [ + 1, + 82, + -1, + 4 + ], + [ + 6, + 82, + 1, + 4 + ], + [ + 9, + 2, + 1, + 4 + ], + [ + 12, + 100, + 1, + 4 + ], + [ + 19, + 101, + -1, + 4 + ], + [ + 24, + 32, + 1, + 4 + ], + [ + 61, + 2, + 1, + 4 + ], + [ + 62, + 63, + 1, + 4 + ], + [ + 66, + 67, + -1, + 4 + ], + [ + 81, + 27, + 1, + 4 + ], + [ + 84, + 60, + 1, + 4 + ], + [ + 90, + 10, + 1, + 4 + ], + [ + 2, + 72, + 1, + 3 + ], + [ + 8, + 95, + 1, + 3 + ], + [ + 10, + 11, + 1, + 3 + ], + [ + 27, + 57, + 1, + 3 + ], + [ + 32, + 45, + -1, + 3 + ], + [ + 35, + 85, + 1, + 3 + ], + [ + 43, + 16, + 1, + 3 + ], + [ + 60, + 83, + -1, + 3 + ], + [ + 63, + 70, + 1, + 3 + ], + [ + 67, + 80, + 1, + 3 + ], + [ + 69, + 97, + 1, + 3 + ], + [ + 75, + 28, + 1, + 3 + ], + [ + 82, + 28, + -1, + 3 + ], + [ + 91, + 11, + 1, + 3 + ], + [ + 100, + 77, + -1, + 3 + ], + [ + 101, + 54, + 1, + 3 + ], + [ + 103, + 17, + 1, + 3 + ], + [ + 11, + 71, + -1, + 2 + ], + [ + 16, + 51, + 1, + 2 + ], + [ + 17, + 31, + 1, + 2 + ], + [ + 18, + 40, + 1, + 2 + ], + [ + 26, + 88, + 1, + 2 + ], + [ + 28, + 22, + -1, + 2 + ], + [ + 45, + 107, + 1, + 2 + ], + [ + 49, + 34, + 1, + 2 + ], + [ + 50, + 109, + 1, + 2 + ], + [ + 54, + 39, + 1, + 2 + ], + [ + 57, + 92, + 1, + 2 + ], + [ + 59, + 30, + 1, + 2 + ], + [ + 68, + 5, + 1, + 2 + ], + [ + 70, + 71, + 1, + 2 + ], + [ + 72, + 0, + 1, + 2 + ], + [ + 77, + 31, + 1, + 2 + ], + [ + 78, + 13, + 1, + 2 + ], + [ + 80, + 88, + -1, + 2 + ], + [ + 83, + 73, + 1, + 2 + ], + [ + 85, + 107, + 1, + 2 + ], + [ + 95, + 88, + 1, + 2 + ], + [ + 96, + 64, + 1, + 2 + ], + [ + 97, + 5, + -1, + 2 + ], + [ + 99, + 44, + 1, + 2 + ], + [ + 108, + 22, + 1, + 2 + ], + [ + 0, + 76, + 1, + 1 + ], + [ + 5, + 4, + -1, + 1 + ], + [ + 13, + 104, + -1, + 1 + ], + [ + 22, + 33, + 1, + 1 + ], + [ + 23, + 33, + 1, + 1 + ], + [ + 29, + 74, + 1, + 1 + ], + [ + 30, + 74, + 1, + 1 + ], + [ + 31, + 4, + 1, + 1 + ], + [ + 34, + 33, + -1, + 1 + ], + [ + 39, + 55, + 1, + 1 + ], + [ + 40, + 55, + 1, + 1 + ], + [ + 44, + 104, + 1, + 1 + ], + [ + 51, + 104, + 1, + 1 + ], + [ + 64, + 4, + 1, + 1 + ], + [ + 65, + 4, + 1, + 1 + ], + [ + 71, + 104, + 1, + 1 + ], + [ + 73, + 74, + -1, + 1 + ], + [ + 88, + 55, + -1, + 1 + ], + [ + 92, + 76, + 1, + 1 + ], + [ + 107, + 74, + 1, + 1 + ], + [ + 109, + 33, + 1, + 1 + ] + ], + "helper_pairs": [ + [ + 149, + 154, + -1, + 147 + ], + [ + 121, + 126, + -1, + 139 + ], + [ + 62, + 70, + -1, + 135 + ], + [ + 93, + 98, + -1, + 129 + ], + [ + 35, + 37, + -1, + 127 + ], + [ + 107, + 112, + -1, + 110 + ], + [ + 135, + 140, + -1, + 109 + ], + [ + 76, + 84, + -1, + 103 + ], + [ + 48, + 56, + -1, + 97 + ], + [ + 20, + 22, + -1, + 94 + ], + [ + 192, + 194, + -1, + 91 + ], + [ + 146, + 155, + 1, + 89 + ], + [ + 104, + 113, + 1, + 89 + ], + [ + 177, + 179, + -1, + 84 + ], + [ + 174, + 172, + -1, + 80 + ], + [ + 161, + 170, + 1, + 79 + ], + [ + 118, + 127, + 1, + 79 + ], + [ + 34, + 43, + 1, + 79 + ], + [ + 159, + 157, + -1, + 74 + ], + [ + 19, + 28, + 1, + 74 + ], + [ + 124, + 128, + 1, + 72 + ], + [ + 68, + 72, + 1, + 72 + ], + [ + 54, + 58, + 1, + 72 + ], + [ + 5, + 7, + -1, + 72 + ], + [ + 176, + 185, + 1, + 69 + ], + [ + 132, + 141, + 1, + 69 + ], + [ + 191, + 200, + 1, + 67 + ], + [ + 152, + 156, + 1, + 67 + ], + [ + 162, + 164, + -1, + 64 + ], + [ + 63, + 71, + 1, + 64 + ], + [ + 4, + 13, + 1, + 62 + ], + [ + 82, + 86, + 1, + 60 + ], + [ + 90, + 99, + 1, + 59 + ], + [ + 110, + 114, + 1, + 53 + ], + [ + 138, + 142, + 1, + 52 + ], + [ + 189, + 188, + -1, + 51 + ], + [ + 41, + 31, + -1, + 49 + ], + [ + 77, + 85, + 1, + 49 + ], + [ + 49, + 57, + 1, + 49 + ], + [ + 96, + 100, + 1, + 44 + ], + [ + 44, + 39, + -1, + 41 + ], + [ + 196, + 201, + -1, + 40 + ], + [ + 94, + 92, + 1, + 37 + ], + [ + 125, + 115, + -1, + 34 + ], + [ + 153, + 143, + -1, + 34 + ], + [ + 23, + 18, + -1, + 34 + ], + [ + 183, + 173, + -1, + 34 + ], + [ + 111, + 101, + -1, + 34 + ], + [ + 24, + 29, + -1, + 31 + ], + [ + 181, + 186, + -1, + 30 + ], + [ + 26, + 16, + -1, + 29 + ], + [ + 69, + 60, + -1, + 29 + ], + [ + 38, + 33, + -1, + 29 + ], + [ + 150, + 148, + 1, + 28 + ], + [ + 80, + 79, + 1, + 27 + ], + [ + 136, + 134, + 1, + 26 + ], + [ + 160, + 165, + 1, + 25 + ], + [ + 83, + 74, + -1, + 24 + ], + [ + 97, + 87, + -1, + 24 + ], + [ + 1, + 2, + -1, + 23 + ], + [ + 131, + 145, + 1, + 23 + ], + [ + 66, + 65, + 1, + 23 + ], + [ + 108, + 106, + 1, + 23 + ], + [ + 122, + 120, + 1, + 22 + ], + [ + 52, + 51, + 1, + 21 + ], + [ + 25, + 27, + 1, + 20 + ], + [ + 42, + 40, + 1, + 20 + ], + [ + 166, + 171, + -1, + 20 + ], + [ + 109, + 102, + 1, + 20 + ], + [ + 151, + 144, + 1, + 20 + ], + [ + 55, + 46, + -1, + 19 + ], + [ + 139, + 129, + -1, + 19 + ], + [ + 117, + 103, + 1, + 18 + ], + [ + 137, + 130, + 1, + 15 + ], + [ + 12, + 10, + 1, + 15 + ], + [ + 197, + 199, + 1, + 15 + ], + [ + 11, + 0, + -1, + 12 + ], + [ + 198, + 187, + -1, + 12 + ], + [ + 15, + 30, + 1, + 12 + ], + [ + 123, + 116, + -1, + 11 + ], + [ + 167, + 169, + -1, + 10 + ], + [ + 182, + 184, + -1, + 10 + ], + [ + 47, + 53, + 1, + 10 + ], + [ + 67, + 61, + -1, + 10 + ], + [ + 219, + 223, + 1, + 10 + ], + [ + 9, + 14, + -1, + 10 + ], + [ + 253, + 249, + 1, + 10 + ], + [ + 168, + 158, + -1, + 9 + ], + [ + 242, + 238, + 1, + 9 + ], + [ + 203, + 207, + 1, + 9 + ], + [ + 202, + 208, + 1, + 8 + ], + [ + 45, + 59, + 1, + 8 + ], + [ + 243, + 237, + 1, + 8 + ], + [ + 224, + 91, + 1, + 7 + ], + [ + 206, + 36, + 1, + 7 + ], + [ + 180, + 175, + 1, + 6 + ], + [ + 215, + 231, + 1, + 6 + ], + [ + 213, + 205, + 1, + 6 + ], + [ + 252, + 212, + 1, + 6 + ], + [ + 216, + 229, + -1, + 5 + ], + [ + 95, + 88, + 1, + 5 + ], + [ + 204, + 248, + 1, + 5 + ], + [ + 195, + 190, + -1, + 4 + ], + [ + 81, + 75, + 1, + 4 + ], + [ + 8, + 3, + -1, + 4 + ], + [ + 221, + 225, + 1, + 4 + ], + [ + 247, + 239, + -1, + 4 + ], + [ + 227, + 220, + 1, + 3 + ], + [ + 230, + 218, + 1, + 2 + ], + [ + 214, + 217, + 1, + 1 + ], + [ + 250, + 210, + 1, + 1 + ], + [ + 211, + 251, + 1, + 1 + ] + ], + "forest_search": { + "edges": 12544, + "price": 16364, + "chosen": [ + [ + 8, + 0, + 76, + 1 + ], + [ + 8, + 73, + 83, + 1 + ], + [ + 8, + 5, + 68, + 1 + ], + [ + 8, + 54, + 101, + 1 + ], + [ + 8, + 34, + 49, + 1 + ], + [ + 8, + 70, + 71, + 1 + ], + [ + 8, + 48, + 98, + 1 + ], + [ + 8, + 2, + 72, + 1 + ], + [ + 8, + 14, + 15, + 1 + ], + [ + 8, + 67, + 80, + 1 + ], + [ + 8, + 6, + 82, + 1 + ], + [ + 8, + 21, + 36, + 1 + ], + [ + 8, + 13, + 78, + 1 + ], + [ + 8, + 12, + 100, + 1 + ], + [ + 18, + 7, + 87, + 1 + ], + [ + 18, + 110, + 111, + 1 + ], + [ + 18, + 52, + 105, + 1 + ], + [ + 18, + 44, + 99, + 1 + ], + [ + 18, + 28, + 75, + 1 + ], + [ + 18, + 46, + 47, + 1 + ], + [ + 18, + 10, + 90, + 1 + ], + [ + 18, + 27, + 81, + 1 + ], + [ + 18, + 26, + 88, + 1 + ], + [ + 18, + 53, + 106, + 1 + ], + [ + 18, + 4, + 65, + 1 + ], + [ + 18, + 60, + 84, + 1 + ], + [ + 18, + 69, + 97, + 1 + ], + [ + 18, + 29, + 74, + 1 + ], + [ + 18, + 51, + 104, + 1 + ], + [ + 18, + 11, + 91, + 1 + ], + [ + 18, + 3, + 66, + 1 + ], + [ + 18, + 25, + 79, + 1 + ], + [ + 18, + 1, + 86, + 1 + ], + [ + 18, + 9, + 89, + 1 + ], + [ + 22, + 38, + 56, + 1 + ], + [ + 22, + 24, + 32, + 1 + ], + [ + 22, + 19, + 102, + 1 + ], + [ + 22, + 31, + 77, + 1 + ], + [ + 22, + 39, + 55, + 1 + ], + [ + 22, + 35, + 85, + 1 + ], + [ + 22, + 50, + 109, + 1 + ], + [ + 22, + 23, + 33, + 1 + ], + [ + 28, + 57, + 92, + 1 + ], + [ + 28, + 61, + 94, + 1 + ], + [ + 28, + 16, + 43, + 1 + ], + [ + 28, + 41, + 42, + 1 + ], + [ + 28, + 62, + 63, + 1 + ], + [ + 28, + 20, + 37, + 1 + ], + [ + 30, + 17, + 103, + 1 + ], + [ + 30, + 22, + 108, + 1 + ], + [ + 30, + 58, + 93, + 1 + ], + [ + 30, + 30, + 59, + 1 + ], + [ + 30, + 45, + 107, + 1 + ], + [ + 30, + 64, + 96, + 1 + ], + [ + 30, + 18, + 40, + 1 + ], + [ + 30, + 8, + 95, + 1 + ], + [ + 151, + 22, + 33, + 1 + ], + [ + 177, + 85, + 107, + 1 + ], + [ + 178, + 2, + 9, + 1 + ], + [ + 178, + 4, + 5, + -1 + ], + [ + 180, + 15, + 106, + -1 + ], + [ + 182, + 80, + 88, + -1 + ], + [ + 185, + 13, + 104, + -1 + ], + [ + 190, + 77, + 100, + -1 + ], + [ + 195, + 39, + 54, + 1 + ], + [ + 196, + 4, + 64, + 1 + ], + [ + 197, + 73, + 74, + -1 + ], + [ + 200, + 88, + 95, + 1 + ], + [ + 203, + 40, + 55, + 1 + ], + [ + 205, + 17, + 31, + 1 + ], + [ + 210, + 28, + 82, + -1 + ], + [ + 220, + 24, + 48, + -1 + ], + [ + 222, + 32, + 45, + -1 + ], + [ + 223, + 33, + 34, + -1 + ], + [ + 223, + 1, + 82, + -1 + ], + [ + 229, + 30, + 74, + 1 + ], + [ + 240, + 19, + 101, + -1 + ], + [ + 242, + 6, + 58, + -1 + ], + [ + 244, + 12, + 38, + -1 + ], + [ + 249, + 36, + 110, + -1 + ], + [ + 254, + 60, + 83, + -1 + ], + [ + 254, + 5, + 97, + -1 + ], + [ + 259, + 66, + 67, + -1 + ], + [ + 264, + 33, + 109, + 1 + ], + [ + 265, + 11, + 71, + -1 + ], + [ + 266, + 44, + 104, + 1 + ], + [ + 268, + 76, + 92, + 1 + ], + [ + 275, + 16, + 51, + 1 + ], + [ + 280, + 63, + 70, + 1 + ], + [ + 286, + 10, + 11, + 1 + ], + [ + 302, + 7, + 81, + 1 + ], + [ + 306, + 9, + 79, + 1 + ], + [ + 308, + 2, + 61, + 1 + ], + [ + 323, + 74, + 107, + 1 + ], + [ + 324, + 55, + 88, + -1 + ], + [ + 327, + 81, + 110, + -1 + ], + [ + 330, + 42, + 53, + 1 + ], + [ + 330, + 4, + 31, + 1 + ], + [ + 330, + 105, + 106, + 1 + ], + [ + 332, + 22, + 28, + -1 + ], + [ + 336, + 71, + 104, + 1 + ], + [ + 337, + 27, + 57, + 1 + ], + [ + 338, + 46, + 110, + 1 + ], + [ + 346, + 36, + 37, + 1 + ], + [ + 361, + 9, + 106, + 1 + ], + [ + 378, + -1, + 33, + 0 + ], + [ + 380, + -1, + 4, + 0 + ], + [ + 384, + -1, + 55, + 0 + ], + [ + 385, + -1, + 74, + 0 + ], + [ + 385, + -1, + 104, + 0 + ], + [ + 431, + 0, + 72, + 1 + ], + [ + 445, + -1, + 76, + 0 + ] + ], + "census_sha256": "de253811759ddc0f20f1639348d1d336c9de674dd19ba0eeaaac220f60b617c2" + }, + "helper_search": { + "cases": 128524, + "profitable": 1525, + "census_sha256": "7969fdd428e83a60a965c02b94ee906357ed53683fd705933f224214c0e069bf", + "gain": 4399 + }, + "baseline_panel_price": 49624, + "two_sided_panel_price": 11965, + "baseline_additions": 8704, + "candidate_additions": 2541, + "residual_additions": 2105, + "residual_quarters_sha256": "b8b1696acf38b1cb91804fc2f5393f919ceb0465f8f67ef0bf56e62ed18cde23", + "panel_sha256": "637ed472f9b8c6b35e35d64b9cc1ffb42b0ed4d880559315c702c4e5f3a3fae7" +} diff --git a/research/complex-ck-two-sided/SOURCES.json b/research/complex-ck-two-sided/SOURCES.json new file mode 100644 index 0000000000..2d7ca6c051 --- /dev/null +++ b/research/complex-ck-two-sided/SOURCES.json @@ -0,0 +1,41 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "source_pr626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "source_pr622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "predecessor_pr807": "b1a5c533a22c2665600102d872f6a84e0664a70d", + "predecessor_pr816": "133735a2cc2319c12ba5d786214b2217e083e7da", + "files": [ + { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz", + "sha256": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7", + "committed_container_sha256": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45", + "encoding": "gzip" + }, + { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-PROGRAMS.json.gz", + "sha256": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "committed_container_sha256": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3", + "encoding": "gzip" + }, + { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/LOCAL-CHECKS.json", + "sha256": "059c4e59142bdf5c19dc7c0afebcddfec28e6e60cbc7299b8bdcc624afbc0cbe" + }, + { + "path": "research/complex-571-cold14-k492c/code/hpe_emit_local.py", + "sha256": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805" + }, + { + "path": "research/complex-571-cold14-k492c/code/hpe_audit_local.py", + "sha256": "6bd9a1e279c9c9e4f3767d9f82e537b559292906feb2ddab02f380fb6523a810" + }, + { + "path": "research/complex-k492-owner-repair/data/SPEC.json", + "sha256": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323" + }, + { + "path": "certificates/checkpoints/k492626.json", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + } + ] +} diff --git a/research/complex-ck-two-sided/VALIDATION.md b/research/complex-ck-two-sided/VALIDATION.md new file mode 100644 index 0000000000..8584e5b9ab --- /dev/null +++ b/research/complex-ck-two-sided/VALIDATION.md @@ -0,0 +1,62 @@ +# Validation and handoff + +Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +Environment: macOS 26.5.2 arm64; CPython **3.14.6**; standard library only. +No Linux or hosted-CI pass is implied by these local checks. + +## Executed checks + +- `python3 -I -B research/complex-ck-two-sided/verify.py`: complete deterministic + recipe/receipt reproduction. All 12,544 target-edge prices and 128,524 helper + cases completed. Separate Prim/census arithmetic agrees. +- Both original and replacement full scalar programs pass on 716 logical plus + nine arbitrary private input columns, under Fraction and separate integer + dyadic arithmetic. Complete counts are 224,938 -> 149,620 and + 224,986 -> 149,668. Native emitter output equals the constructed programs. + Both engines also agree that every intermediate symbolic coefficient needs + at most 3 forward / 8 backward binary denominator bits, unchanged from baseline. +- Unchanged inherited native audit passes both 716-column frame/wrapper checks, + unchanged paid profiles, and all **25** original negative controls. +- **10** new controls detect omitted target/helper preparation or restoration, + wrong helper or residual sign, reversed target order, illegal wrapped-helper + access and omitted initial dirty-work clear. The illegal-helper control + preserves source count and checks the exact rejection reason. Omitted target + preparation deliberately passes helper-only checking and fails full checking. +- `python3 -I -B research/complex-ck-two-sided/test_package.py`: **7 tests pass**, + including every emitted coefficient on arbitrary source/target/work, source + mutation/removal, recompression, non-scalar preservation and bad recipe costs. +- `python3 -I -B research/complex-ck-two-sided/test_independent.py`: **6 tests + pass**, covering exact dyadic arithmetic, private dirt, copy aliasing, restored + helpers and malformed instructions. +- All three commands also pass with `-O`; inherited native subprocesses use + isolated mode without `-O`, retaining their assertion-based checks. +- A minimal source closure at a temporary path containing spaces passes from + outside the checkout, after recompressing the program input. A typed receipt + mutation and a helper-gain recipe mutation are rejected; verification leaves + existing output bytes unchanged, including on failure. +- `make selected-record-check` and the five tests in + `tests/test_selected_result.py` pass on the unchanged selected PR799 record. + +The exact reproducible results are in `EXPECTED.json`; source and predecessor +pins are in `SOURCES.json`. Compression container changes are deliberately +accepted only when the decompressed source payload is unchanged. + +## Scope + +Only this research directory is added. `upstream/`, selected-result records, +existing generators, unrelated artifacts and predecessor implementations are +unchanged. Full repository `make verify`, full cold construction rebuilding, +global hosting/invoice/assembly admission and Lean are not claimed. The relevant +checks here establish the finite compensation rewrite and native local interface; +the selected production construction has not been modified. + +Current main was fetched unchanged during the pre-submission overlap check. +The final complete snapshot contained 705 open PRs through #915. Exact heads for +PR807/816 remain those in `SOURCES.json`. No pinned sprint issue exists, so the +claim and result are local. No matching two-sided CK work was found. PR816's +standalone target-forest minimum is independently corroborated; this adds helper +changes *after* that transformation, with a full recomputed cost and replay. + +Production adoption still needs a typed alternative-compensation step and new +source bindings, complete global invoices and admission. Neither the historical +CK checkpoint nor current X4 selection receives a new κ from this package. diff --git a/research/complex-ck-two-sided/experiment.py b/research/complex-ck-two-sided/experiment.py new file mode 100644 index 0000000000..66a1606d48 --- /dev/null +++ b/research/complex-ck-two-sided/experiment.py @@ -0,0 +1,284 @@ +"""Exact bounded two-sided CK compensation construction. + +Ross Richardson with substantial OpenAI Codex assistance, Apache-2.0. +Target forests follow dd-hemant PR816; helper shears follow David Awad PR807. +This implementation is new; no pending PR code is imported. +""" +from collections import deque +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROVIDER = 'research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck' +SEED = 38 +BASE = 'f567884aeb8851b6e794af1184119a3bfbe1e631' + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(x): + return json.dumps(x, sort_keys=True, separators=(',', ':')).encode() + + +def digest(x): + return hashlib.sha256(canonical(x)).hexdigest() + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def load(): + pins = read(HERE / 'SOURCES.json') + for item in pins['files']: + path = ROOT / item['path'] + raw = path.read_bytes() + payload = gzip.decompress(raw) if item.get('encoding') == 'gzip' else raw + require(hashlib.sha256(payload).hexdigest() == item['sha256'], 'source pin: ' + item['path']) + p = ROOT / PROVIDER + w = read(p / 'CANONICAL-WORD.json.gz') + ps = read(p / 'LOCAL-PROGRAMS.json.gz') + checks = read(p / 'LOCAL-CHECKS.json') + spec = read(ROOT / 'research/complex-k492-owner-repair/data/SPEC.json')['providers']['ck'] + for name in ('CANONICAL-WORD.json.gz', 'LOCAL-PROGRAMS.json.gz', 'LOCAL-CHECKS.json'): + require(digest(read(p/name)) == spec['artifact_semantic_sha256'][name], 'historical SPEC binding: '+name) + for orientation in ps: + require(digest(ps[orientation]) == checks[orientation]['sha256'], 'program binding') + require(digest(ps[orientation]) == spec['program_hashes'][orientation], 'historical program binding') + return w, ps, checks + + +@lru_cache(None) +def price_quarter(x): + """Inherited binary-Horner price of the coefficient x/4, in one component.""" + if not x: + return 0 + a, d = abs(x), 2 + while d and not a % 2: + a //= 2 + d -= 1 + return 3 + a.bit_length() - 1 + a.bit_count() + d + + +def matrix(w): + rows = sorted({e[1] for e in w['compensation']}) + cols = sorted({e[2] for e in w['compensation']}) + require(len(rows) == 112 and len(cols) == 254, 'CK compensation shape') + require(set(rows).isdisjoint(cols), 'disjoint source/target banks') + require(all(w['start'][r] == 0 for r in rows + cols), 'common frame zero') + require(all(w['final'][r] == 1 for r in cols), 'helpers must be unwrapped at entry') + ri, ci = {r: i for i, r in enumerate(rows)}, {c: i for i, c in enumerate(cols)} + C = [[0] * len(cols) for _ in rows] + for tag, target, source, a, b, frame in w['compensation']: + require(tag == 'add' and frame == 0, 'compensation instruction') + q = Q(a, b) * 4 + require(q.denominator == 1, 'quarter-grid compensation') + C[ri[target]][ci[source]] += q.numerator + return rows, cols, C + + +def rowcost(row): + return sum(map(price_quarter, row)) + + +def forest(C): + """Kruskal on signed row differences plus superroot, deterministic ties.""" + n = len(C) + edges = [(rowcost(C[i]), -1, i, 0) for i in range(n)] + for i in range(n): + for j in range(i): + for sign in (-1, 1): + edges.append((8 + rowcost([a - sign*b for a, b in zip(C[i], C[j])]), j, i, sign)) + edges.sort(key=lambda e: (e[0], digest([SEED, list(e)]))) + parent = list(range(n + 1)) + def root(i): + i += 1 + while parent[i] != i: + parent[i] = parent[parent[i]] + i = parent[i] + return i + chosen = [] + for weight, a, b, sign in edges: + ar, br = root(a), root(b) + if ar != br: + parent[ar] = br + chosen.append([weight, a, b, sign]) + if len(chosen) == n: + break + adj = {i: [] for i in range(-1, n)} + for weight, a, b, sign in chosen: + adj[a].append((b, sign)); adj[b].append((a, sign)) + visited = {-1}; queue = deque([(-1, 0)]); oriented = [] + while queue: + a, depth = queue.popleft() + for b, sign in sorted(adj[a]): + if b not in visited: + visited.add(b); queue.append((b, depth + 1)) + if a != -1: + oriented.append([b, a, sign, depth]) + require(len(visited) == n+1, 'forest connectivity') + oriented.sort(key=lambda x: (-x[3], x[0], x[1])) + D = [row[:] for row in C] + for child, par, sign, _ in oriented: + D[child] = [a - sign*b for a, b in zip(C[child], C[par])] + total = sum(e[0] for e in chosen) + require(total == sum(map(rowcost, D)) + 8*len(oriented), 'forest pricing') + return oriented, D, {'edges': len(edges), 'price': total, + 'chosen': chosen, 'census_sha256': digest(edges)} + + +def helpers(D): + columns = list(map(list, zip(*D))) + n = len(columns) + costs = list(map(rowcost, columns)) + census = hashlib.sha256(); profitable = [] + count = 0 + for a in range(n): + for b in range(n): + if a == b: + continue + for sign in (-1, 1): + # H: h_a += sign*h_b. Column b changes under right H^-1. + gain = costs[b] - rowcost([v-sign*u for u, v in zip(columns[a], columns[b])]) - 8 + rec = [a, b, sign, gain] + census.update(canonical(rec) + b'\n'); count += 1 + if gain > 0: + profitable.append(rec) + profitable.sort(key=lambda x: (-x[3], digest([SEED, x]))) + used = set(); selected = [] + for a, b, sign, gain in profitable: + if a not in used and b not in used: + used.update((a,b)); selected.append([a,b,sign,gain]) + E = [row[:] for row in D] + for a,b,sign,gain in selected: + for row in E: + row[b] -= sign*row[a] + actual_gain = sum(map(rowcost,D)) - sum(map(rowcost,E)) - 8*len(selected) + require(actual_gain == sum(x[3] for x in selected), 'disjoint helper gains') + return selected, E, {'cases': count, 'profitable': len(profitable), + 'census_sha256': census.hexdigest(), 'gain': actual_gain} + + +def addition(target, source, q): + q = Q(q) + require(target != source and q, 'invalid addition') + return ['add', target, source, q.numerator, q.denominator, 0] + + +def construct(w): + targets, sources, C = matrix(w) + T, D, tree = forest(C) + H, E, pair = helpers(D) + prepT = [addition(targets[c], targets[p], -s) for c,p,s,_ in T] + prepH = [addition(sources[a], sources[b], s) for a,b,s,_ in H] + residual = [addition(t, sources[j], Q(x,4)) for t,row in zip(targets,E) + for j,x in enumerate(row) if x] + def inverse(es): + return [addition(e[1],e[2],-Q(e[3],e[4])) for e in reversed(es)] + panel = prepT + prepH + residual + inverse(prepH) + inverse(prepT) + recipe = {'seed': SEED, 'targets': targets, 'sources': sources, + 'target_forest': T, 'helper_pairs': H, + 'forest_search': tree, 'helper_search': pair, + 'baseline_panel_price': sum(map(rowcost,C)), + 'two_sided_panel_price': sum(map(rowcost,E))+8*(len(T)+len(H)), + 'baseline_additions': len(w['compensation']), + 'candidate_additions': len(panel), 'residual_additions': len(residual), + 'residual_quarters_sha256': digest(E), 'panel_sha256': digest(panel)} + require(recipe['baseline_panel_price'] - recipe['two_sided_panel_price'] > 0, 'no complete saving') + return panel, recipe + + +def scalar(e, backward): + _,t,s,a,b,_ = e + if backward: + t,s,a = s,t,-a + return ['scalar', ['add',['L',t],['L',s],a,b], 0] + + +def replace_programs(w, original, panel): + result = {} + begin = 1 + len(w['precondition']) + end = begin + len(w['compensation']) + for name, events in original.items(): + require(events[0] == ['phase','zero_frame_precondition'], 'program phase') + require(events[end] == ['phase','entry_adapters'], 'compensation boundary') + require(events[begin:end] == [scalar(e,name=='backward') for e in w['compensation']], 'literal compensation binding') + result[name] = events[:begin] + [scalar(e,name=='backward') for e in panel] + events[end:] + require([e for e in events if e[0]!='scalar'] == + [e for e in result[name] if e[0]!='scalar'], 'non-scalar preservation') + return result + + +def lower(op): + """Literal inherited (unoptimized) binary Horner with dirty work erased.""" + tag, target = op[0], tuple(op[1]); work = ('W',0) + require(target != work, 'work aliases target') + if tag == 'clear': + return [('clear',target)] + if tag == 'copy': + return [('copy',target,tuple(op[2]))] + if tag == 'scale': + q = Q(op[2],op[3]); a,b = abs(q.numerator),q.denominator + require(a and a&(a-1)==0 and b&(b-1)==0, 'scale not signed power of two') + shift = a.bit_length()-b.bit_length() + return [('double' if shift>0 else 'halve',target)]*abs(shift) + ([('negate',target)] if q<0 else []) + require(tag == 'add', 'unknown scalar operation') + source = tuple(op[2]); q=Q(op[3],op[4]); a,b=abs(q.numerator),q.denominator + require(source not in (target,work) and q and b&(b-1)==0, 'invalid dyadic add') + ops=[('clear',work)] + for i,bit in enumerate(bin(a)[2:]): + if i: ops.append(('double',work)) + if bit=='1': ops.append(('add',work,source,1)) + ops += [('halve',work)]*(b.bit_length()-1) + ops += [('add',target,work,1 if q>0 else -1),('clear',work)] + return ops + + +def primitives(events): + for event in events: + if event[0]=='scalar': + yield from lower(event[1]) + + +def fraction_replay(events, n=716, centers=8): + """Fresh full arbitrary-input scalar projection; nonscalars checked separately.""" + refs=[('L',i) for i in range(n)]+[('C',i) for i in range(centers)]+[('W',0)] + state={r:{i:Q(1)} for i,r in enumerate(refs)} + env={r:Q(1) for r in refs}; peak=Q(1); count=0; grid=0 + for op in primitives(events): + tag,t=op[:2]; count+=1 + if tag=='clear': state[t]={};env[t]=Q(0) + elif tag=='copy': state[t]=dict(state[op[2]]);env[t]=env[op[2]] + elif tag in ('double','halve','negate'): + q={'double':Q(2),'halve':Q(1,2),'negate':Q(-1)}[tag] + state[t]={i:q*x for i,x in state[t].items()};env[t]*=abs(q) + else: + _,_,s,sign=op + env[t]+=env[s] + for i,x in list(state[s].items()): + value=state[t].get(i,Q(0))+sign*x + if value: state[t][i]=value + else: state[t].pop(i,None) + peak=max(peak,env[t]) + grid=max(grid,max((x.denominator.bit_length()-1 for x in state[t].values()),default=0)) + return state, {'real_primitives':2*count,'prefix_l1':str(peak), + 'prefix_bits':peak.numerator.bit_length()-peak.denominator.bit_length()+1, + 'maximum_denominator_power':grid} + + +def endpoint(state, backward, n=716, v=112): + for i in range(n): + expected={i:Q(1)} + if backward and i> reduction for column, value in terms.items()} + exponent -= reduction + return terms, exponent + + +def _sum_rows(left, right, sign): + left_terms, left_exponent = left + right_terms, right_exponent = right + exponent = max(left_exponent, right_exponent) + result = {column: value << (exponent - left_exponent) + for column, value in left_terms.items()} + for column, value in right_terms.items(): + result[column] = result.get(column, 0) + sign * (value << (exponent - right_exponent)) + return _normal_row(result, exponent) + + +def _normal_number(numerator, exponent): + if numerator == 0: + return 0, 0 + reduction = min(exponent, (numerator & -numerator).bit_length() - 1) + return numerator >> reduction, exponent - reduction + + +def _sum_numbers(left, right): + exponent = max(left[1], right[1]) + numerator = ((left[0] << (exponent - left[1])) + + (right[0] << (exponent - right[1]))) + return _normal_number(numerator, exponent) + + +def _greater(left, right): + return (left[0] << right[1]) > (right[0] << left[1]) + + +def _serialize_row(row): + terms, exponent = row + return {"denominator_power": exponent, + "terms": [[column, terms[column]] for column in sorted(terms)]} + + +def replay(primitives, n=716, centers=8): + """Return a JSON-serializable exact endpoint, cost and positive prefix. + + The vocabulary is clear(ref), copy(target, source), add(target, source, + sign), double(ref), halve(ref), negate(ref), represented as JSON lists. + Add's sign must be exactly +1 or -1. References are ["L", index], + ["C", index], or the unique coefficient scratch ["W", 0]. + + Basis symbols 0..n-1 are L inputs, n..n+centers-1 are C inputs and + n+centers is the W input. Non-scalar events must be checked separately, + never passed here. This function accepts an iterable so callers need not + materialize a second copy of a long literal program. + """ + _require(type(n) is int and n > 0, "n must be a positive integer") + _require(type(centers) is int and centers >= 0, "centers must be a nonnegative integer") + sizes = {"L": n, "C": centers, "W": 1} + refs = [(kind, index) for kind, size in sizes.items() for index in range(size)] + rows = {ref: ({column: 1}, 0) for column, ref in enumerate(refs)} + envelope = {ref: (1, 0) for ref in refs} + prefix = (1, 0) + prefix_at = -1 + maximum_denominator_power = 0 + counts = Counter() + + def reference(value, instruction_index): + _require(isinstance(value, (list, tuple)) and len(value) == 2, + f"instruction {instruction_index}: malformed register reference") + kind, index = value + _require(type(kind) is str and kind in sizes and type(index) is int + and 0 <= index < sizes[kind], + f"instruction {instruction_index}: register outside declared domain") + return kind, index + + arities = {"clear": 2, "copy": 3, "add": 4, + "double": 2, "halve": 2, "negate": 2} + for instruction_index, instruction in enumerate(primitives): + _require(isinstance(instruction, (list, tuple)) and bool(instruction), + f"instruction {instruction_index}: malformed primitive") + operation = instruction[0] + _require(type(operation) is str and operation in arities, + f"instruction {instruction_index}: unknown primitive {operation!r}") + _require(len(instruction) == arities[operation], + f"instruction {instruction_index}: wrong primitive arity") + target = reference(instruction[1], instruction_index) + counts[operation] += 1 + if operation == "clear": + rows[target] = ({}, 0) + envelope[target] = (0, 0) + elif operation == "copy": + source = reference(instruction[2], instruction_index) + # Rows are immutable by convention: updates always allocate a row. + rows[target] = rows[source] + envelope[target] = envelope[source] + elif operation == "add": + source = reference(instruction[2], instruction_index) + sign = instruction[3] + _require(type(sign) is int and sign in (-1, 1), + f"instruction {instruction_index}: add sign must be +1 or -1") + _require(target != source, + f"instruction {instruction_index}: add aliases its source") + rows[target] = _sum_rows(rows[target], rows[source], sign) + envelope[target] = _sum_numbers(envelope[target], envelope[source]) + else: + terms, exponent = rows[target] + numerator, denominator_power = envelope[target] + if operation == "negate": + rows[target] = ({column: -value for column, value in terms.items()}, exponent) + elif operation == "double": + rows[target] = _normal_row({column: 2 * value for column, value in terms.items()}, exponent) + envelope[target] = _normal_number(2 * numerator, denominator_power) + else: + rows[target] = _normal_row(terms, exponent + 1) + envelope[target] = _normal_number(numerator, denominator_power + 1) + if _greater(envelope[target], prefix): + prefix = envelope[target] + prefix_at = instruction_index + maximum_denominator_power = max(maximum_denominator_power, rows[target][1]) + + return { + "arithmetic": "exact integer sparse rows over dyadic denominators", + "input_columns": len(refs), + "logical_registers": n, + "center_registers": centers, + "scratch_registers": 1, + "primitive_count": sum(counts.values()), + "primitive_counts": dict(sorted(counts.items())), + "maximum_denominator_power": maximum_denominator_power, + "positive_prefix": { + "numerator": prefix[0], + "denominator_power": prefix[1], + "strict_power_of_two_bits": prefix[0].bit_length() - prefix[1], + "first_maximum_instruction": prefix_at, + }, + "endpoint": {kind: [_serialize_row(rows[kind, index]) for index in range(size)] + for kind, size in sizes.items()}, + } + + +def check_endpoint(result, orientation, v=112): + """Check additive forward or inverse-transpose ports and erased private work. + + Forward: L[v+i] += L[i]. Backward: L[i] -= L[v+i]. All remaining + logical columns are restored exactly, including every helper dirt input. + This test uses explicit exceptions and remains active with Python -O. + """ + _require(orientation in ("forward", "backward"), "unknown orientation") + n = result["logical_registers"] + _require(type(v) is int and 0 < 2 * v <= n, "invalid port count") + endpoint = result["endpoint"] + _require(len(endpoint["L"]) == n, "wrong number of logical outputs") + for index, actual in enumerate(endpoint["L"]): + terms = {index: 1} + if orientation == "forward" and v <= index < 2 * v: + terms[index - v] = 1 + elif orientation == "backward" and index < v: + terms[v + index] = -1 + expected = _serialize_row((terms, 0)) + _require(actual == expected, + f"{orientation}: incorrect logical output L[{index}]") + for kind in ("C", "W"): + _require(len(endpoint[kind]) == result["center_registers" if kind == "C" else "scratch_registers"], + f"wrong number of {kind} outputs") + for index, actual in enumerate(endpoint[kind]): + _require(actual == _serialize_row(({}, 0)), + f"{orientation}: private register {kind}[{index}] is not erased") + return True + + +def check_recipe(word, recipe): + """Independently price the finite recipe and repeat its helper census. + + Prim's algorithm checks the signed target-forest minimum, independently of + the constructor's Kruskal implementation and tie ordering. Pricing counts + literal binary digits and denominator halvings; it does not use bit_count + or the constructor's price routine. The helper pairs are verified as a + disjoint selection, without asserting their global optimality. + """ + targets = sorted({event[1] for event in word["compensation"]}) + sources = sorted({event[2] for event in word["compensation"]}) + _require((len(targets), len(sources)) == (112, 254), "unexpected compensation shape") + _require(targets == recipe["targets"] and sources == recipe["sources"], "recipe bank mismatch") + _require(set(targets).isdisjoint(sources), "compensation banks overlap") + _require(all(word["start"][r] == 0 for r in targets + sources), "nonzero compensation frame") + _require(all(word["final"][r] == 1 for r in sources), "wrapped helper before entry adapter") + ti, si = {r: i for i, r in enumerate(targets)}, {r: i for i, r in enumerate(sources)} + matrix = [[0] * len(sources) for _ in targets] + for tag, target, source, numerator, denominator, frame in word["compensation"]: + _require(tag == "add" and frame == 0 and denominator > 0 + and (4 * numerator) % denominator == 0, "non-quarter compensation") + matrix[ti[target]][si[source]] += (4 * numerator) // denominator + prices = {0: 0} + + def price(value): + if value not in prices: + integer, halvings = abs(value), 2 + while halvings and integer % 2 == 0: + integer //= 2 + halvings -= 1 + digits = [] + while integer: + digits.append(integer % 2) + integer //= 2 + prices[value] = 3 + halvings + sum(digits) + len(digits) - 1 + return prices[value] + + def cost(rows): + return sum(price(value) for row in rows for value in row) + + distances = [sum(map(price, row)) for row in matrix] + reached, minimum = set(), 0 + for _ in targets: + j = min((j for j in range(len(targets)) if j not in reached), key=distances.__getitem__) + reached.add(j) + minimum += distances[j] + for i in range(len(targets)): + if i not in reached: + edge = 8 + min(sum(price(x - sign * y) for x, y in zip(matrix[i], matrix[j])) + for sign in (-1, 1)) + distances[i] = min(distances[i], edge) + transformed = [row[:] for row in matrix] + parent = {} + for child, ancestor, sign, _depth in recipe["target_forest"]: + _require(type(child) is int and type(ancestor) is int + and 0 <= child < len(targets) and 0 <= ancestor < len(targets) + and child != ancestor and child not in parent + and type(sign) is int and sign in (-1, 1), "invalid target-forest edge") + parent[child] = ancestor + transformed[child] = [x - sign * y for x, y in zip(transformed[child], transformed[ancestor])] + for child in parent: + visited = set() + while child in parent: + _require(child not in visited, "target forest has a cycle") + visited.add(child) + child = parent[child] + forest_cost = cost(transformed) + 8 * len(parent) + _require(forest_cost == minimum == recipe["forest_search"]["price"], "target forest is not minimum priced") + columns = list(zip(*transformed)) + column_costs = [sum(map(price, col)) for col in columns] + census = hashlib.sha256() + cases = profitable = 0 + gains = {} + for a in range(len(sources)): + for b in range(len(sources)): + if a == b: + continue + for sign in (-1, 1): + gain = column_costs[b] - sum(price(y - sign * x) for x, y in zip(columns[a], columns[b])) - 8 + cases += 1 + profitable += gain > 0 + gains[a, b, sign] = gain + census.update((json.dumps([a, b, sign, gain], separators=(",", ":")) + "\n").encode()) + used, total_gain = set(), 0 + for a, b, sign, gain in recipe["helper_pairs"]: + _require(a not in used and b not in used and a != b, "helper pair collision") + _require((a, b, sign) in gains and gain == gains[a, b, sign] and gain > 0, "incorrect selected helper gain") + used.update((a, b)) + total_gain += gain + for row in transformed: + row[b] -= sign * row[a] + helper_summary = {"cases": cases, "profitable": profitable, + "census_sha256": census.hexdigest(), "gain": total_gain} + _require(helper_summary == recipe["helper_search"], "helper census mismatch") + complete = cost(transformed) + 8 * (len(parent) + len(recipe["helper_pairs"])) + _require(complete == minimum - total_gain == recipe["two_sided_panel_price"], "complete panel price mismatch") + _require(cost(matrix) == recipe["baseline_panel_price"], "baseline panel price mismatch") + return {"method": "Prim signed-forest minimum; exhaustive ordered signed helper-pair census", + "baseline_panel_price": cost(matrix), "target_minimum": minimum, + "helper_search": helper_summary, "complete_panel_price": complete} diff --git a/research/complex-ck-two-sided/test_independent.py b/research/complex-ck-two-sided/test_independent.py new file mode 100644 index 0000000000..f0e480fda9 --- /dev/null +++ b/research/complex-ck-two-sided/test_independent.py @@ -0,0 +1,99 @@ +"""Small arithmetic and defect-sensitivity checks for the separate replay. + +Run: python3 -m unittest discover -s research/complex-ck-two-sided -p test_independent.py +Prepared for Ross with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import unittest +from pathlib import Path +import sys + +# Permit the documented isolated-mode invocation without ambient PYTHONPATH. +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from independent import ReplayError, check_endpoint, replay + + +class IndependentReplayTests(unittest.TestCase): + def test_exact_signed_dyadic_and_positive_envelope(self): + result = replay([ + ["copy", ["W", 0], ["L", 0]], + ["halve", ["W", 0]], + ["add", ["L", 1], ["W", 0], -1], + ["double", ["W", 0]], + ["add", ["L", 1], ["W", 0], 1], + ["negate", ["L", 0]], + ["clear", ["W", 0]], + ], n=2, centers=0) + self.assertEqual(result["endpoint"]["L"], [ + {"denominator_power": 0, "terms": [[0, -1]]}, + {"denominator_power": 1, "terms": [[0, 1], [1, 2]]}, + ]) + self.assertEqual(result["primitive_count"], 7) + self.assertEqual(result["positive_prefix"]["numerator"], 5) + self.assertEqual(result["positive_prefix"]["denominator_power"], 1) + self.assertEqual(result["maximum_denominator_power"], 1) + transient = replay([["halve", ["L", 0]], ["double", ["L", 0]]], n=1, centers=0) + self.assertEqual(transient["maximum_denominator_power"], 1) + self.assertEqual(transient["endpoint"]["L"][0]["denominator_power"], 0) + + def test_all_private_registers_enter_dirty(self): + result = replay([], n=2, centers=1) + self.assertEqual(result["input_columns"], 4) + self.assertEqual(result["endpoint"]["C"][0]["terms"], [[2, 1]]) + self.assertEqual(result["endpoint"]["W"][0]["terms"], [[3, 1]]) + with self.assertRaises(ReplayError): + check_endpoint(result, "forward", v=1) + + def test_both_endpoints_and_helper_restoration(self): + for orientation in ("forward", "backward"): + target, source, sign = ((1, 0, 1) if orientation == "forward" else (0, 1, -1)) + program = [ + ["clear", ["C", 0]], + ["clear", ["W", 0]], + ["add", ["L", 2], ["L", 0], 1], + ["add", ["L", 2], ["L", 0], -1], + ["add", ["L", target], ["L", source], sign], + ] + self.assertTrue(check_endpoint(replay(program, n=3, centers=1), orientation, v=1)) + with self.assertRaises(ReplayError): + check_endpoint(replay(program[:3] + program[4:], n=3, centers=1), orientation, v=1) + + def test_missing_scratch_clear_exposes_entering_dirt(self): + program = [ + ["add", ["W", 0], ["L", 0], 1], + ["add", ["L", 1], ["W", 0], 1], + ["clear", ["W", 0]], + ] + with self.assertRaises(ReplayError): + check_endpoint(replay(program, n=2, centers=0), "forward", v=1) + self.assertTrue(check_endpoint( + replay([["clear", ["W", 0]]] + program, n=2, centers=0), "forward", v=1)) + + def test_copy_does_not_alias_later_mutations(self): + result = replay([ + ["copy", ["W", 0], ["L", 0]], + ["add", ["L", 0], ["L", 1], 1], + ["halve", ["W", 0]], + ], n=2, centers=0) + self.assertEqual(result["endpoint"]["W"][0], + {"denominator_power": 1, "terms": [[0, 1]]}) + + def test_malformed_instructions_fail_closed(self): + examples = [ + ["add", ["L", 0], ["L", 1], 2], + ["add", ["L", 0], ["L", 1], True], + ["add", ["L", 0], ["L", 0], 1], + ["clear", ["L", 2]], + ["clear", ["W", 1]], + ["clear", ["L", True]], + ["scale", ["L", 0], 1, 2], + ["negate", ["L", 0], "unexpected"], + ["phase", "anything"], + ] + for instruction in examples: + with self.subTest(instruction=instruction), self.assertRaises(ReplayError): + replay([instruction], n=2, centers=0) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/complex-ck-two-sided/test_package.py b/research/complex-ck-two-sided/test_package.py new file mode 100644 index 0000000000..efc9cd1c18 --- /dev/null +++ b/research/complex-ck-two-sided/test_package.py @@ -0,0 +1,95 @@ +"""Focused provenance, pricing and corruption controls for the finite package. + +Ross Richardson with substantial OpenAI Codex assistance. Apache-2.0. +""" +import copy +from fractions import Fraction as Q +import gzip +import json +from pathlib import Path +import shutil +import sys +import tempfile +import unittest +from unittest.mock import patch + +sys.path.insert(0,str(Path(__file__).resolve().parent)) +import experiment as e +import independent + + +class PackageTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.word,cls.programs,cls.checks=e.load() + cls.panel,cls.recipe=e.construct(cls.word) + + def source_closure(self, root): + for item in e.read(e.HERE/'SOURCES.json')['files']: + source=e.ROOT/item['path'];dest=root/item['path'] + dest.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(source,dest) + + def test_recompression_keeps_mathematical_input(self): + with tempfile.TemporaryDirectory(prefix='ck closure ') as tmp: + root=Path(tmp);self.source_closure(root) + path=root/e.PROVIDER/'CANONICAL-WORD.json.gz' + path.write_bytes(gzip.compress(gzip.decompress(path.read_bytes()),compresslevel=1,mtime=1234567)) + with patch.object(e,'ROOT',root): + self.assertEqual(e.load()[0],self.word) + + def test_changed_and_missing_source_rejected(self): + with tempfile.TemporaryDirectory() as tmp: + root=Path(tmp);self.source_closure(root) + path=root/e.PROVIDER/'CANONICAL-WORD.json.gz' + changed=copy.deepcopy(self.word);changed['compensation'][0][3]*=-1 + path.write_bytes(gzip.compress(e.canonical(changed))) + with patch.object(e,'ROOT',root): + with self.assertRaisesRegex(ValueError,'source pin'): + e.load() + path.unlink() + with self.assertRaises(FileNotFoundError): + e.load() + + def test_all_emitted_coefficients_exact_with_dirty_work(self): + coefficients=set() + for programs in (self.programs,e.replace_programs(self.word,self.programs,self.panel)): + for events in programs.values(): + for event in events: + if event[0]=='scalar' and event[1][0]=='add': + coefficients.add(Q(event[1][3],event[1][4])) + for q in sorted(coefficients): + result=independent.replay(e.lower(['add',['L',1],['L',0],q.numerator,q.denominator]),n=2,centers=0) + expected={'denominator_power':q.denominator.bit_length()-1, + 'terms':[[0,q.numerator],[1,q.denominator]]} + self.assertEqual(result['endpoint']['L'][1],expected) + self.assertEqual(result['endpoint']['L'][0],{'denominator_power':0,'terms':[[0,1]]}) + self.assertEqual(result['endpoint']['W'][0],{'denominator_power':0,'terms':[]}) + cost=3+len(bin(abs(q.numerator)))-3+bin(abs(q.numerator)).count('1')+q.denominator.bit_length()-1 + self.assertEqual(result['primitive_count'],cost) + self.assertGreater(len(coefficients),100) + + def test_non_scalar_and_other_scalar_segments_unchanged(self): + changed=e.replace_programs(self.word,self.programs,self.panel) + begin=1+len(self.word['precondition']);end=begin+len(self.word['compensation']) + for name,original in self.programs.items(): + self.assertEqual(changed[name][:begin],original[:begin]) + self.assertEqual(changed[name][begin+len(self.panel):],original[end:]) + self.assertEqual([x for x in changed[name] if x[0]!='scalar'],[x for x in original if x[0]!='scalar']) + + def test_repeated_helpers_fail_independent_recipe(self): + bad=copy.deepcopy(self.recipe);bad['helper_pairs'].append(bad['helper_pairs'][0]) + with self.assertRaisesRegex(independent.ReplayError,'helper pair collision'): + independent.check_recipe(self.word,bad) + + def test_tampered_cost_fails_independent_recipe(self): + bad=copy.deepcopy(self.recipe);bad['two_sided_panel_price']-=1 + with self.assertRaisesRegex(independent.ReplayError,'complete panel price'): + independent.check_recipe(self.word,bad) + + def test_typed_json_comparison_distinguishes_bool(self): + # JSON object equality alone treats True as 1; committed receipts use bytes. + self.assertNotEqual(e.canonical({'price':1}),e.canonical({'price':True})) + + +if __name__=='__main__': + unittest.main() diff --git a/research/complex-ck-two-sided/verify.py b/research/complex-ck-two-sided/verify.py new file mode 100644 index 0000000000..139b9eca14 --- /dev/null +++ b/research/complex-ck-two-sided/verify.py @@ -0,0 +1,156 @@ +"""Reproduce the bounded CK two-sided construction and its finite evidence. + +Ross Richardson, substantial OpenAI Codex assistance. Apache-2.0. +Run from any directory with Python 3.10+ and the standard library. +""" +import argparse +import copy +from fractions import Fraction as Q +import gzip +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import experiment as e +import independent as independent + + +def summary_integer(result): + peak=result['positive_prefix'] + return {'real_primitives':2*result['primitive_count'], + 'prefix_l1':str(Q(peak['numerator'], 2**peak['denominator_power'])), + 'prefix_bits':peak['strict_power_of_two_bits'], + 'maximum_denominator_power':result['maximum_denominator_power']} + + +def native(w, programs): + """Unchanged inherited emitter, common-frame/wrapper audit and 25 controls.""" + with tempfile.TemporaryDirectory(prefix='ck-two-sided-') as directory: + out=Path(directory) + (out/'CANONICAL-WORD.json.gz').write_bytes(gzip.compress(e.canonical(w),mtime=0)) + logs={} + for script in ('hpe_emit_local.py','hpe_audit_local.py'): + path=e.ROOT/'research/complex-571-cold14-k492c/code'/script + # -I ignores PYTHONOPTIMIZE; parent -O must not disable inherited asserts. + run=subprocess.run([sys.executable,'-I','-B',str(path),str(out)],capture_output=True,text=True) + e.require(run.returncode==0, 'native '+script+' failed:\n'+run.stdout+run.stderr) + logs[script]=run.stdout.strip().splitlines() + rebuilt=e.read(out/'LOCAL-PROGRAMS.json.gz') + e.require(e.canonical(rebuilt)==e.canonical(programs),'native emitter program disagreement') + checks=e.read(out/'LOCAL-CHECKS.json') + audit=e.read(out/'INDEPENDENT-LOCAL-REPLAY.json') + e.require(len(audit['negative_controls_rejected'])==25,'native control coverage') + return {'checks':checks, 'local':audit['local'], 'paid_profiles':audit['paid_profiles'], + 'negative_controls_rejected':audit['negative_controls_rejected'], 'logs':logs} + + +def controls(w, panel, recipe): + """Actual faulty circuits, checked against every arbitrary input column.""" + base_events=[e.scalar(x,False) for x in w['compensation']] + reference,_=e.fraction_replay(base_events) + nt=len(recipe['target_forest']); nh=len(recipe['helper_pairs']); nr=recipe['residual_additions'] + mutants={ + 'omitted_target_preparation':panel[1:], + 'omitted_helper_preparation':panel[:nt]+panel[nt+1:], + 'omitted_helper_restoration':panel[:nt+nh+nr]+panel[nt+nh+nr+1:], + 'omitted_target_restoration':panel[:-1], + 'reversed_target_preparation':list(reversed(panel[:nt]))+panel[nt:], + 'reversed_target_restoration':panel[:-nt]+list(reversed(panel[-nt:])), + } + wrong=copy.deepcopy(panel);wrong[nt][3]*=-1;mutants['wrong_helper_preparation_sign']=wrong + wrong=copy.deepcopy(panel);wrong[nt+nh][3]*=-1;mutants['wrong_residual_sign']=wrong + rejected=[]; helper_only_control=False + for label,mutant in mutants.items(): + state,_=e.fraction_replay([e.scalar(x,False) for x in mutant]) + e.require(state!=reference,'mutation accepted: '+label) + if label=='omitted_target_preparation': + project=lambda st: {r:{k:v for k,v in row.items() if 224<=k<716} + for r,row in st.items()} + e.require(project(state)==project(reference),'helper-only blind spot was not reproduced') + helper_only_control=True + rejected.append(label) + # A source-ineligible cold helper is forbidden before its paid pre-wrapper. + cold=next(r for r in range(224,716) if w['start'][r]==0 and w['final'][r]!=1) + bad=copy.deepcopy(w);replaced=bad['compensation'][0][2] + for operation in bad['compensation']: + if operation[2]==replaced: operation[2]=cold + try: e.matrix(bad) + except ValueError as error: + e.require(str(error)=='helpers must be unwrapped at entry','cold control rejected for wrong reason') + rejected.append('cold_wrapped_helper_access') + else: raise ValueError('cold helper mutation accepted') + # An initial clear is mathematically needed for arbitrary coefficient work. + p=e.lower(['add',['L',1],['L',0],1,1]) + good=independent.replay(p,n=2,centers=0) + independent.check_endpoint(good,'forward',v=1) + try: independent.check_endpoint(independent.replay(p[1:],n=2,centers=0),'forward',v=1) + except independent.ReplayError: rejected.append('omitted_initial_work_clear') + else: raise ValueError('dirty work mutation accepted') + return {'rejected':rejected,'omitted_target_preparation_passes_helper_only':helper_only_control} + + +def verify(record=False): + w,original,checks=e.load() + panel,recipe=e.construct(w) + candidate=e.replace_programs(w,original,panel) + expected_recipe=e.HERE/'RECIPE.json' + if not record: + e.require(e.canonical(e.read(expected_recipe))==e.canonical(recipe),'RECIPE.json does not reproduce') + result={'status':'FINITE_CK_TWO_SIDED_COMPENSATION_NO_NEW_KAPPA', + 'base_commit':e.BASE,'seed':e.SEED,'source_pins_sha256':e.digest(e.read(e.HERE/'SOURCES.json')), + 'recipe_sha256':e.digest(recipe),'columns':{'logical':716,'private':9}, + 'search':{'target_edges':recipe['forest_search']['edges'], + 'helper_cases':recipe['helper_search']['cases'], + 'profitable_helper_cases':recipe['helper_search']['profitable'], + 'target_basis_edges':len(recipe['target_forest']), + 'helper_pairs':len(recipe['helper_pairs'])}, + 'panel_component_prices':{'baseline':recipe['baseline_panel_price'], + 'target_only':recipe['forest_search']['price'], + 'two_sided':recipe['two_sided_panel_price']}, + 'programs':{}} + result['independent_recipe']=independent.check_recipe(w,recipe) + for name in ('forward','backward'): + result['programs'][name]={} + for label,events in (('baseline',original[name]),('candidate',candidate[name])): + state,receipt=e.fraction_replay(events) + e.endpoint(state,name=='backward') + other=independent.replay(e.primitives(events)) + independent.check_endpoint(other,name) + e.require(receipt==summary_integer(other),'integer/Fraction replay disagreement') + e.require(receipt['prefix_bits']<=192,'inherited 192-bit allowance exceeded') + if label=='baseline': + e.require(receipt['real_primitives']==checks[name]['real_component_primitive_bound'],'baseline invoice mismatch') + result['programs'][name][label]={**receipt,'program_sha256':e.digest(events), + 'primitive_word_sha256':e.digest(list(e.primitives(events))), + 'scalar_macros':sum(x[0]=='scalar' for x in events), + 'primitive_counts':other['primitive_counts']} + r=result['programs'][name] + saved=r['baseline']['real_primitives']-r['candidate']['real_primitives'] + e.require(saved==2*(recipe['baseline_panel_price']-recipe['two_sided_panel_price']),'complete price mismatch') + r['real_saved']=saved + r['additional_real_saved_vs_target_forest']=2*recipe['helper_search']['gain'] + nw=copy.deepcopy(w);nw['compensation']=panel + result['native']=native(nw,candidate) + for name in ('forward','backward'): + r=result['programs'][name]['candidate']; nc=result['native']['checks'][name]; na=result['native']['local'][name] + e.require(nc['real_component_primitive_bound']==r['real_primitives'],'native price mismatch') + e.require(na['prefix_l1_upper']==r['prefix_l1'],'native prefix mismatch') + e.require(nc['paid_profile']==checks[name]['paid_profile'],'paid profile changed') + result['controls']=controls(w,panel,recipe) + if record: + expected_recipe.write_text(json.dumps(recipe,indent=2)+'\n') + (e.HERE/'EXPECTED.json').write_text(json.dumps(result,indent=2)+'\n') + else: + e.require(e.canonical(e.read(e.HERE/'EXPECTED.json'))==e.canonical(result),'EXPECTED.json does not reproduce') + print('PASS_CK_TWO_SIDED target_edges=106 helper_pairs=112 cases=128524 saved_real=75318 additional_vs_target=8798 columns=716+9 orientations=2 controls=10+25 no_new_kappa') + return result + + +if __name__=='__main__': + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--record',action='store_true',help='replace this package receipts after all checks pass') + args=parser.parse_args() + verify(args.record)