diff --git a/research/p104-owned772-relay-descent/EDIT.json.gz b/research/p104-owned772-relay-descent/EDIT.json.gz new file mode 100644 index 0000000000..13d635abaa Binary files /dev/null and b/research/p104-owned772-relay-descent/EDIT.json.gz differ diff --git a/research/p104-owned772-relay-descent/EXPECT.json b/research/p104-owned772-relay-descent/EXPECT.json new file mode 100644 index 0000000000..c968786929 --- /dev/null +++ b/research/p104-owned772-relay-descent/EXPECT.json @@ -0,0 +1,36 @@ +{ + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "chain_commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "control_sites": { + "arbitrary_input_compensation": 13609, + "late_correction": 15666, + "owned_clear": 14479, + "owned_descent": 13641 + }, + "events": 22834, + "helper_delta": {}, + "interval": [ + "312781137239/100000000000000", + "7819528431/2500000000000" + ], + "inventory": [ + 770, + 29, + 31, + 13 + ], + "paid_calls": 66780, + "paid_delta": { + "1": -1, + "6": -1, + "7": 1 + }, + "predecessor_head": "4cef86d87e47dfcc5a511c99c9f0067c861271b0", + "productive_fields": 13444, + "rank_mass_surplus": 760, + "sign_sites": { + "arbitrary_input_compensation": 13609, + "rerouted_read": 13642 + }, + "status": "PASS_P104_OWNED772_KAPPA_312780400" +} diff --git a/research/p104-owned772-relay-descent/INDEPENDENT.json b/research/p104-owned772-relay-descent/INDEPENDENT.json new file mode 100644 index 0000000000..6e4a8dc7a8 --- /dev/null +++ b/research/p104-owned772-relay-descent/INDEPENDENT.json @@ -0,0 +1,231 @@ +{ + "base": { + "endpoint_coefficients": 638401, + "events": 22828, + "local_helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "local_paid": { + "1": 2217, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 9, + "7": 8, + "8": 1 + }, + "operations": { + "ADD": 18431, + "CLEAR": 31, + "COPY": 23, + "INIT": 31, + "MOVE": 3451, + "SCALE": 861 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid_calls": 66798, + "paid_rank_mass": 240152, + "peak_owned": 13, + "productive_fields": 13444, + "public": 770, + "real_scalar_allowance": 189730, + "rows_checked": 799, + "target_rank_mass": 240912, + "whole_paid": { + "1": 41466, + "16": 416, + "2": 8226, + "24": 416, + "3": 8928, + "32": 416, + "4": 1800, + "40": 416, + "48": 416, + "5": 2934, + "56": 416, + "6": 162, + "64": 416, + "7": 144, + "72": 208, + "8": 18 + }, + "whole_targets": { + "1": 252, + "145": 208, + "17": 416, + "2": 144, + "25": 416, + "3": 72, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "6": 36, + "65": 416, + "7": 162, + "73": 208, + "8": 342, + "9": 6930 + } + }, + "candidate": { + "endpoint_coefficients": 638401, + "events": 22834, + "local_helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "local_paid": { + "1": 2216, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 8, + "7": 9, + "8": 1 + }, + "operations": { + "ADD": 18438, + "CLEAR": 31, + "COPY": 23, + "INIT": 31, + "MOVE": 3450, + "SCALE": 861 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid_calls": 66780, + "paid_rank_mass": 240152, + "peak_owned": 13, + "productive_fields": 13444, + "public": 770, + "real_scalar_allowance": 189806, + "rows_checked": 799, + "target_rank_mass": 240912, + "whole_paid": { + "1": 41448, + "16": 416, + "2": 8226, + "24": 416, + "3": 8928, + "32": 416, + "4": 1800, + "40": 416, + "48": 416, + "5": 2934, + "56": 416, + "6": 144, + "64": 416, + "7": 162, + "72": 208, + "8": 18 + }, + "whole_targets": { + "1": 252, + "145": 208, + "17": 416, + "2": 144, + "25": 416, + "3": 72, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "6": 36, + "65": 416, + "7": 162, + "73": 208, + "8": 342, + "9": 6930 + } + }, + "local_paid_delta": { + "1": -1, + "6": -1, + "7": 1 + }, + "negative_controls": { + "borrow_owned_move": "MOVE ownership at 13641", + "clear791_before_last_read": "common chart at 13636", + "copy_into_dirty_owned": "COPY cleared owned destination at 13639", + "dependent_frame_basis": "linearly independent frame basis", + "hold791_across772_lifetime": "complete return/storage contract", + "non_dyadic_scale": "dyadic bounded scalar at 13639", + "nonunit_scale": "dyadic unit SCALE at 13639", + "omit_arbitrary_input_compensation": "arbitrary-input endpoint row 145", + "omit_owned_return": "complete return/storage contract", + "omit_top162_compensation": "arbitrary-input endpoint row 162", + "reverse_compensation_sign": "arbitrary-input endpoint row 145", + "wrong_move_source_chart": "MOVE source chart at 13641" + }, + "owned791_references": [ + [ + 13478, + [ + "INIT", + 791, + 549 + ] + ], + [ + 13479, + [ + "COPY", + 791, + 173, + "1", + 549 + ] + ], + [ + 13480, + [ + "ADD", + 121, + 791, + "1/2", + 549 + ] + ], + [ + 13635, + [ + "COPY", + 770, + 791, + "1", + 549 + ] + ], + [ + 13636, + [ + "CLEAR", + 791, + 549 + ] + ] + ] +} diff --git a/research/p104-owned772-relay-descent/NATIVE-AUDIT.json b/research/p104-owned772-relay-descent/NATIVE-AUDIT.json new file mode 100644 index 0000000000..f794a7d0ac --- /dev/null +++ b/research/p104-owned772-relay-descent/NATIVE-AUDIT.json @@ -0,0 +1,53 @@ +{ + "columns_checked": 2048, + "complex_entries_compared": 1048576, + "controls": { + "absolute_phase_only": "rejected", + "child_sign": "rejected" + }, + "new_signed_map_count": 3, + "paid_move_delta_maps": [ + { + "columns": 512, + "frames": [ + 3, + 529 + ], + "matrix_sha256": "dcdb1a896ef8c98018be0111bec67cd30761a9d9190e1876841b7c6fae40d806", + "rank": 7, + "role": "existing_helper_map_positive_control" + }, + { + "columns": 512, + "frames": [ + 520, + 737 + ], + "matrix_sha256": "45b79c2b4d43bddc7a713ace98aafb18fd8f1f2803fe604e821c284d2c2094fb", + "rank": 2, + "role": "new_signed_map" + }, + { + "columns": 512, + "frames": [ + 529, + 520 + ], + "matrix_sha256": "6cb29fe68a85e01b13b937dcd8723b099673b015fc38fd2f1bdfbba8a9f70aa1", + "rank": 1, + "role": "new_signed_map" + }, + { + "columns": 512, + "frames": [ + 737, + 595 + ], + "matrix_sha256": "62180012f1f2ef1338b46a982bf1f058681af990ca0204ad1b6a611f6dc0198c", + "rank": 3, + "role": "new_signed_map" + } + ], + "scope": "Three new finite 9-qubit signed maps and one existing helper-map positive control; other unchanged maps reuse predecessor evidence; uniform native_all_columns remains assumed.", + "unchanged_helper_maps_and_main_adapters": true +} diff --git a/research/p104-owned772-relay-descent/NATIVE-SOURCES.json b/research/p104-owned772-relay-descent/NATIVE-SOURCES.json new file mode 100644 index 0000000000..ca14e01f2b --- /dev/null +++ b/research/p104-owned772-relay-descent/NATIVE-SOURCES.json @@ -0,0 +1,26 @@ +{ + "base": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "size": 6824, + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "usage": "input" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "size": 12323, + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "usage": "input" + }, + { + "path": "research/p104-contact-independent-audit/capsule/outputs/p104-native-contact-audit-20261025/check.py", + "size": 11654, + "sha256": "43fd40847a0853c0ac511d58ce77ef822a5c6dd1b25f662f01cefaa3196a2f7d", + "git_blob": "e7e663bebaf13f44c95fb8eb118b472cf377e137", + "usage": "input" + } + ] +} diff --git a/research/p104-owned772-relay-descent/PRICING-EDITS.json b/research/p104-owned772-relay-descent/PRICING-EDITS.json new file mode 100644 index 0000000000..59b5d32223 --- /dev/null +++ b/research/p104-owned772-relay-descent/PRICING-EDITS.json @@ -0,0 +1,18 @@ +[ + [ + "KAPPA, TESTED = Q('0.00312476680'), Q('0.003124766805')", + "KAPPA, TESTED = Q('0.003127804'), Q('0.003127809')" + ], + [ + "PREVIOUS = Q('0.00312418633064')", + "PREVIOUS = Q('0.003127137')" + ], + [ + "sum(targets.values()) == 13444 and sum(paid.values()) == 66870", + "sum(targets.values()) == 13444 and sum(paid.values()) == 66780" + ], + [ + "'kappa_decimal':'0.00312476680','previous_pr5811':PREVIOUS", + "'kappa_decimal':'0.003127804','previous_pr6143':PREVIOUS" + ] +] diff --git a/research/p104-owned772-relay-descent/PROOF.md b/research/p104-owned772-relay-descent/PROOF.md new file mode 100644 index 0000000000..93ea9ae397 --- /dev/null +++ b/research/p104-owned772-relay-descent/PROOF.md @@ -0,0 +1,140 @@ +# Owned-772 descent and public-731 relay elimination + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The predecessor construction and checker are credited to DreamingOfClouds +(PR6143, PR6030 and PR5907), Ali Romman (PR5827), and the cumulative P104 +lineage named in their retained notices. This note proves only the local edit; +the complete conditional claim also needs the inherited native/caller/pricing +checks and five framework assumptions. + +## Frozen objects + +Base: PR6143 at `4cef86d87e47dfcc5a511c99c9f0067c861271b0`, +`research/p104-root-relay-descent/WORD.json.gz`. The canonical JSON SHA256 is +`b66406fa1027ba08ac2a85154ba73289f258f90d79454a193e685221bc61430d`. +The new canonical JSON SHA256 is +`0572c956c77b0ee2ef47169c9df52269bc719e37c7003f3f0245179aea0aad71`. +`EDIT.json.gz` consists of literal new events and exact slices of the base +program. Regeneration requires no solver. No initial/final frame, frame basis, +public register, or productive helper target changes. + +Indices below are zero-based indices in the frozen PR6143 base. They are +explanatory; the executable certificate is the complete new word. + +## Exact scalar identity + +Let `u` denote the independent initial value in public helper 731. It is +unchanged throughout its frame-3 prefix: before the relay it is read at three +frame-3 ADDs but is never a scalar destination. Let `rho` be register 146's +value just after base event 13474 (`146 += 440` in frame 529), and let +`v = -rho/2`. Register 146 does not change again until event 16903, after all +uses discussed here. + +The original 772 lifetime copies `rho`, contributes `-rho/2` to register 162, +scales itself to `v`, descends from 529 to 595, and contributes `v` to 708 +and 731. Hence 731 holds `u+v` during its ascending relay. The edit leaves +731 at `u` and has 772 deliver `v` directly. + +For each of the eight relay readers, the old update `r += q*(u+v)` is +replaced by `r += q*u` in frame 3 and `r += q*v` in its old meeting frame: + +| Reader | q | Meeting frame | Frame dimension | +| --- | ---: | ---: | ---: | +| 572 | 2 | 595 | 1 | +| 582 | 2 | 595 | 1 | +| 581 | 2 | 595 | 1 | +| 134 | -2 | 595 | 1 | +| 450 | 4 | 595 | 1 | +| 496 | 4 | 595 | 1 | +| 451 | -4 | 737 | 4 | +| 497 | -4 | 520 | 6 | + +The frame-3 update is inserted immediately before the reader's first MOVE, +using 731 itself, which still holds `u` in frame 3. For each reader there is +no intervening source use or SCALE before its old relay read. Intervening +ADDs into that reader commute with adding `q*u`. For readers 451 and 497, +the `v` update moves earlier, to the corresponding point of 772's descent; +they are already at frames 737 and 520, and have no intervening source use +or SCALE before their old read. The remaining six `v` reads stay at their +original chronological locations. + +The top-frame read `162 += 2*731` formerly contributed `2*u+2*v`. It now +contributes `2*u` and an adjacent `162 += -146` in frame 529 supplies +`2*v = -rho`. This uses register 146 while it still contains `rho`. +The former cleanup `731 += rho/2` is deleted: the base cleanup sends +`u+v` to `u`; the new register already holds `u`. The subsequent read of +731 by 146 consequently sees the same value. + +The original 772 contribution `162 += -rho/2` is retimed without changing +its value: it becomes `162 += 772` just after 772 is scaled to `v`. +Register 162 has no intervening source use, SCALE or other event between +these two positions. The loading of 708 and the first read of 708 by 127 +are also retimed. Register 708's MOVE from 595 to 602 follows those reads, +and precedes every old read of 708 at 602. No public output or later value +changes. The complete rational replay checks the result on all 799 formal +input columns, including every arbitrary independent helper input. + +## Frames, lifetime and chronology + +The base paths are + +- owned 772: `529 -> 595` (dimensions `7 -> 1`); +- public 731: `3 -> 595 -> 737 -> 520 -> 529` + (dimensions `0 -> 1 -> 4 -> 6 -> 7`). + +The new paths are + +- owned 772: `529 -> 520 -> 737 -> 595` + (dimensions `7 -> 6 -> 4 -> 1`); +- public 731: `3 -> 529` (dimensions `0 -> 7`). + +All containments are the strict reverse of already used base containments. +Reader 497 is at 520 and reader 451 is at 737 before the new descent starts. +All other scalar gates retain common frames, including each compensation. + +The new 772 lifetime starts immediately after base event 13641, the last +read of owned register 791 (`COPY 770 <- 791`). The CLEAR of 791 is moved +from base event 15597 to that point, before the INIT of 772. There is no +later read, write, MOVE or COPY involving 791. The slot released by its +legal CLEAR covers the extended 772 lifetime. This is actual chronological +liveness, not an argument from matching INIT/CLEAR multisets. The new CLEAR +of 772 follows the last 595 read (reader 496, base event 14468). + +Public count 770, owned labels 29, owned lifetimes 31 and peak live owned +count 13 are all unchanged. Every owned register is cleared at return. +The complete new program has 22,834 events (six more than PR6143), safely +below the inherited 26,000-event bound. It adds seven ADDs net and removes +one MOVE net; INIT, CLEAR, COPY and SCALE multisets are unchanged. The exact +ordinary scalar allowance increases from 189,730 to 189,806, by 76. + +## Complete signed local budget + +Writing `H_r = r^t`, the old paths cost `H_6 + H_1 + H_3 + H_2 + H_1`; +the new paths cost `H_1 + H_2 + H_3 + H_7`. Thus the complete local paid +profile changes by `-H_1 - H_6 + H_7`. Productive targets, rank mass, +public endpoints, caller query/idles, and helper normalization obligations +are unchanged. No credit is assigned to owned scratch. + +For every `0 < t < 1`, strict subadditivity gives `1 + 6^t > 7^t`. +Thus the local complete signed gain is positive throughout that exponent +range. The caller invokes the local word 18 times, so the full paid profile +changes by `-18 H_1 -18 H_6 +18 H_7`, and its paid-call count drops from +66,798 to 66,780. Every newly used signed native map and its absolute phase +still needs the complete native replay; this algebra does not replace it. +The productive count 13,444 and rank-mass surplus 760 remain unchanged. + +## What is new and what is not + +PR6143 rerouted roots 770/771 through helpers 705/706. This edit uses the +separate root 772 and relay 731; its frame-3 compensation is particularly +simple because 731 has no preceding scalar writes. Retiming the now-dead +791 lifetime is needed to compose all three root changes without increasing +peak occupancy. PR6136's chart-only A-E searches keep the scalar program; +this edit changes the read sources and compensating ADDs, so it is outside +those reported finite domains. This does not show those domains or the +broader supplier globally optimal. + +The new word is a finite conditional construction. It does not discharge +native-all-column, owned-erasure, compiler, precision/tape or analytic +recovery assumptions, materialize the uniform word or rounded multiplier, +or authorize changing the selected frontier. diff --git a/research/p104-owned772-relay-descent/README.md b/research/p104-owned772-relay-descent/README.md new file mode 100644 index 0000000000..83c9219414 --- /dev/null +++ b/research/p104-owned772-relay-descent/README.md @@ -0,0 +1,188 @@ +# Conditional κ = 0.003127804: one more owned-root relay removal + +This package adds one finite construction to DreamingOfClouds' pending +[PR6143](https://github.com/CrocSwap/integer-mult-bounds/pull/6143): owned register +772 delivers its value directly while public helper 731 takes a single hop. +Eight compensating reads preserve 731's arbitrary independent input. Moving +791's CLEAR immediately after its last read makes the longer 772 lifetime fit +within the unchanged peak of 13 owned fields. + +The complete conditional claim is **κ = 781951/250000000 = 0.003127804**, an +increase of **0.000000667 over PR6143's 0.003127137** and **0.000002000 over the +selected PR6030 claim 0.003125804**. This changes the complete paid profile; +it is not additional digits of the predecessor's crossing. The selected record +is unchanged. The five framework assumptions remain. + +| Complete construction | PR6143 input | This word | +| --- | ---: | ---: | +| Paid recursive calls | 66,798 | 66,780 | +| Productive fields | 13,444 | 13,444 | +| Paid / target rank mass | 240,152 / 240,912 | 240,152 / 240,912 | +| Public / owned labels / lifetimes / peak | 770 / 29 / 31 / 13 | 770 / 29 / 31 / 13 | +| Local events | 22,828 | 22,834 | +| Local ordinary scalar allowance | 189,730 | 189,806 | + +The exact raw crossing lies in **(0.00312781137239, 0.00312781137240)**. +The compiler is tested at **0.003127809**, with exact gap +`d = (tested − κ)/7 = 1/1400000000`. The unchanged admitted BIT budget `.0034` +still exceeds this complex supplier's saving. This is a small improvement to +the complete conditional multiplication bound, subject to the same assumptions +and independent admission; it is not a measured runtime improvement. + +## Construction and complete cost + +[PROOF.md](PROOF.md) gives the scalar identity, eight reader coefficients, +chronology and budget. The old paths are + +- owned 772: `529 → 595`; +- public 731: `3 → 595 → 737 → 520 → 529`. + +The new paths are + +- owned 772: `529 → 520 → 737 → 595`; +- public 731: `3 → 529`. + +Let `u` be helper 731's arbitrary input and `v = −146/2` at the stated causal +cut. Each old reader receives `q(u+v)`. It now receives `qu` at frame 3 and +`qv` from 772 at its legal meeting frame. A final correction to 162 and the +removed cleanup of 731 preserve every endpoint. No owned register earns +productive credit, and no helper input is assumed zero. The INIT, CLEAR, COPY +and SCALE multisets stay unchanged; their actual chronological legality is +checked separately. + +Per local invocation, paid cost changes by `−H1−H6+H7`, where `Hr = r^t`; +productive targets do not change. Across all 18 invocations the signed saving +is `18(1+6^t−7^t)>0` for `0 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "348599999253/350000000000", + "fixed_halo_explicit_metadata_branch": "26950000001/350000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000", + "new_semantic_group_guard": "3/1400000000" + }, + "margins": { + "boundary_algebraic_matrix": "30652507178105357/9800000000000000000", + "fused_gaussian": "30652507134316071/9800000000000000000", + "global_coordinate_router": "2736831/875000000", + "group_bit_router": "3831564266789507/1225000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "30652500178105357/9800000000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "4011902507178105357/9800000000000000000" + }, + "parameters": { + "a": "2736831/875000000", + "b": "21894653/7000000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "8911902500178105357/9800000000000000000", + "complex_uniform_saving": "10947329/3500000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "781951/250000000", + "lambda_": "1993744387/2000000000", + "lambda_prime": "6978105357/7000000000", + "layout": "1/1400000000", + "q": "21894643/7000000000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "3127809/1000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "238169/875000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "888097510321894643/4900000000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "27978105357/9800000000000000000", + "cap_above_band": "4011902500178105357/9800000000000000000", + "cap_below_cell": "888097492821894643/9800000000000000000", + "cap_below_phase_cell_power": "10688097499821894643/9800000000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "196855347/7000000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "27934316071/9800000000000000000", + "gaussian_above_main": "3478105357/4900000000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "4366789507/1225000000000000000", + "group_gauge_power_slack": "888097509971894643/4900000000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "3489052681/3500000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "698416790400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000", + "lambda_above_sigma": "3/2800000000", + "lambda_above_tau": "1/2800000000", + "lambda_prime_above_lambda": "1/2800000000", + "lambda_prime_above_leaf": "13978105347/9800000000000000000", + "leaf_saving_above_effective": "6978105347/9800000000000000000", + "main_transform_above_kappa": "20978105357/9800000000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "33686131587/437500000", + "microbox_halo_volume": "110600000003/1400000000", + "new_complex_uniform_saving_above_b": "1/1400000000", + "new_semantic_guard_with_C1_one": "1/1400000000", + "polynomial_products_above_kappa": "6978105367/7000000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "13978105347/9800000000000000000", + "q_positive": "21894643/7000000000", + "short_record_fallback": "6978105347/7000000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "3981250027978105357/9800000000000000000", + "stop_below_one": "1399999999/1400000000", + "stop_positive": "1/1400000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000", + "union_tag_work_per_visit_fits_record": "3/1400000000" + } + }, + "paid": { + "1": 41448, + "16": 416, + "2": 8226, + "24": 416, + "3": 8928, + "32": 416, + "4": 1800, + "40": 416, + "48": 416, + "5": 2934, + "56": 416, + "6": 144, + "64": 416, + "7": 162, + "72": 208, + "8": 18 + }, + "paid_calls": 66780, + "previous_pr6143": "3127137/1000000000", + "productive_fields": 13444, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_ceiling": { + "derivative_upper": "-367571871779244516468098385167341811961974287814764077581374543/1569275433846670190958947355801916604025588861116008628224", + "interval": [ + "0", + "17/5000" + ] + }, + "raw_headroom": [ + "737239/100000000000000", + "18431/2500000000000" + ], + "raw_root_interval": [ + "312781137239/100000000000000", + "7819528431/2500000000000" + ], + "relative_gain_percent": "66700/3127137", + "strictification": { + "alpha": { + "lower": "0.999999997597602047163659262770", + "upper": "0.999999997597602047163659262771" + }, + "cutoff": 16, + "delta": { + "lower": "0.950629888154892922927071566565", + "upper": "0.950629888154892922927071566566" + }, + "floor": 17, + "gamma": { + "lower": "0.975636844088298228795948151586", + "upper": "0.975636844088298228795948151587" + }, + "normalized_paid_upper": "1048576000976562501/1048576001073741824", + "power": 1024, + "reserve": "1/1000000000000", + "tail_block": 128, + "tail_decay": "125/128", + "tail_offset": "1/7", + "tested": "3127809/1000000000" + }, + "targets": { + "1": 252, + "145": 208, + "17": 416, + "2": 144, + "25": 416, + "3": 72, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "6": 36, + "65": 416, + "7": 162, + "73": 208, + "8": 342, + "9": 6930 + }, + "whole_idle_jobs": 3120 + }, + "controls": { + "damaged_base_word": "Exact source SHA256: research/p104-root-relay-descent/WORD.json.gz", + "damaged_source_LOCAL-EDITS.json": "Exact source SHA256: research/p104-unread-path-resynthesis/LOCAL-EDITS.json", + "damaged_source_NOTICE": "Exact source SHA256: research/p104-unread-path-resynthesis/NOTICE", + "damaged_source_PLAN.json": "Exact source SHA256: research/p104-unread-path-resynthesis/PLAN.json", + "extra_target_credit": "Every productive helper has a native target", + "missing_arbitrary_input_compensation": "All public and owned rows", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "missing_late_correction": "All public and owned rows", + "missing_owned_clear": "All public and owned exits", + "missing_owned_descent": "Common scalar chart", + "unpaid_query": "Complete field and call counts", + "wrong_sign_arbitrary_input_compensation": "All public and owned rows", + "wrong_sign_rerouted_read": "All public and owned rows" + }, + "limits": [ + "All five inherited framework assumptions remain.", + "The large uniform word and rounded multiplier are not materialized.", + "Author checks do not establish independent acceptance.", + "The selected frontier is unchanged." + ], + "local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2216, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 8, + "7": 9, + "8": 1 + }, + "paid_rank_mass": 5952, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 189806 + }, + "native": { + "distinct_maps": 2924, + "helper_normalizers": 1124, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "5f3820f2b8b2565b03e628e170c01b59dea2e9385b5d6968b6877180314f2dac", + "wrong_phase_rejected": true + }, + "paid_delta": { + "1": -1, + "6": -1, + "7": 1 + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 638401, + "columns": 799 + }, + "source_local": { + "endpoint_coefficients": 638401, + "helpers": { + "1": 14, + "2": 8, + "3": 4, + "4": 107, + "5": 14, + "6": 2, + "7": 9, + "8": 19, + "9": 385 + }, + "owned_fields": 29, + "owned_lifetimes": 31, + "paid": { + "1": 2217, + "2": 457, + "3": 496, + "4": 100, + "5": 163, + "6": 9, + "7": 8, + "8": 1 + }, + "paid_rank_mass": 5952, + "peak_owned_fields": 13, + "public_inputs": 770, + "real_scalar_allowance": 189730 + }, + "status": "PASS_P104_OWNED772_KAPPA_312780400", + "target_delta": {} +} diff --git a/research/p104-owned772-relay-descent/SOURCES.json b/research/p104-owned772-relay-descent/SOURCES.json new file mode 100644 index 0000000000..f9eaedd8c0 --- /dev/null +++ b/research/p104-owned772-relay-descent/SOURCES.json @@ -0,0 +1,233 @@ +{ + "archived_files": [ + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "f725d2bb87b3322512cb76eefbe3a9b26ece7176", + "path": "research/p104-unread-path-resynthesis/LOCAL-EDITS.json", + "sha256": "c4d195bcf17209a129bacf5b8ebd311d475c44405feb040683f096858f87a987", + "size": 59 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "8fc3f76cc0d66f19c9abd7c7111ec69c73c0434d", + "path": "research/p104-unread-path-resynthesis/NOTICE", + "sha256": "fe02063ca48bf070303ac05f613ab1e6e4dd9ee62141f7e7012d855faf7b0c78", + "size": 6714 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "dc269304a438d39c9aa60256eb33c4d439fb378a", + "path": "research/p104-unread-path-resynthesis/PLAN.json", + "sha256": "46bada733d461d7d5154ba5ede7d32697eaa00ab7380a0ceaf53324b9084d1a8", + "size": 1030 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "205de2990148e83bdac27aea49de593ffbefee0a", + "path": "research/p104-unread-path-resynthesis/PRICING-EDITS.json", + "sha256": "7cec40c77056d30d879ff6752bf785ce1773c11e6c959cc8f33c351b828e3c8a", + "size": 437 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "eae2e1b895284155a1485f240a0ad43a4b52c0aa", + "path": "research/p104-unread-path-resynthesis/PROOF.md", + "sha256": "16b1ba9b9468b097796d900ac04f9a278e09cba5ec9e08436b6e06ee066b385b", + "size": 6614 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "e663d069442adfb224de108031f80b603180d873", + "path": "research/p104-unread-path-resynthesis/README.md", + "sha256": "5f5026b41eb3f822652d4b41b5f4f81c4a285ac77d7ec34f41fabdbdad4b0252", + "size": 4574 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "e2e078df445d6c1b988cf926fed3bc7570a88237", + "path": "research/p104-unread-path-resynthesis/RESULT.json", + "sha256": "e437dd9fc7368de705cef8a9d27c6161f1b246f36e320e5c155dde89f88e16e2", + "size": 13257 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "4531538f264f4aaf9bd5e0d6be74758578fab749", + "path": "research/p104-unread-path-resynthesis/SOURCES.json", + "sha256": "b6aa6b569e76a7ab07f59e3d3c1204dad485bc9d6638211907a3f619073b6e33", + "size": 8164 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "1b7c6ccdb6a32e89b11f70163e1b4b409f5693d6", + "path": "research/p104-unread-path-resynthesis/TASK.json", + "sha256": "2548bea7e62ee5d8b988c72988c7f8cf69ed623994e662929639ff857620942f", + "size": 7801 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "1a3fa30e394a9837ec6d57adc019144ac323ea67", + "path": "research/p104-unread-path-resynthesis/VALIDATION.md", + "sha256": "593470975c818bd86d3af813d86d8a6c17ef51c0e7e437e14a0c94de1286112c", + "size": 1790 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "988b0541663f9bddf08d3c80ff09cacd87d9ab4c", + "path": "research/p104-unread-path-resynthesis/VERIFY.json", + "sha256": "c0c2995e2961dcad87e5f78fac22b519c629a1da77e661f924fa5101a87fde4d", + "size": 677 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "969ff0c9b474bc9d2df2eec8482e17cfb75c1fbe", + "path": "research/p104-unread-path-resynthesis/WITNESS.json", + "sha256": "6f9bb837e47c5b10f6d008d57a87415c7013e2076f3313fde1848d27b3314e67", + "size": 677 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "6341a49f717bd64ef2a5b7c440bd86d5513425dc", + "path": "research/p104-unread-path-resynthesis/WORD.json.gz", + "sha256": "5d50e5654910c9535e9025de0f644bb2dece2396e799b4a766110363448fd0b0", + "size": 122919 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "7d33cb8646ea7492131853070e97afd5935521da", + "path": "research/p104-unread-path-resynthesis/construct.py", + "sha256": "e23a70d1fa000c05c6e05a6d8c909cd47b8aabc6c7505f925fc0235575076c9c", + "size": 2371 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "a1f7e63c7dd3b5ef4cde70b96e8ad6aa30cdc684", + "path": "research/p104-unread-path-resynthesis/inputs/pr5786-source.tar", + "sha256": "9ca76daeb8db6b623d7329628248fae114946f35fb036c3171fcdba868131dc2", + "size": 3788800 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "bd91106cde0cc8c201329bedc2d45af65c582b57", + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-NOTICE", + "sha256": "2f87017c7497194392d41c8ae80e5e1cfcf14651627cea2f918c1c8924c9858d", + "size": 1027 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "71a8c020a59e8469cd547511766db92fa79480c4", + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-PROOF.md", + "sha256": "87756328c812a9076a55d5ebe1b9ea81d8fdcb166608cb39b0b43cca2cdc8593", + "size": 12191 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "2e73d97bdd2b2c13e05e66299722e0aa30c2d050", + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-RESULT.json", + "sha256": "2ba9ec0c06ce0c2683cdd704cacb63e6bb9afeb90a07a16fb63ec9e55696c488", + "size": 19496 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "3633d78556932b1d66285c19d888fcd7c62cdbf1", + "path": "research/p104-unread-path-resynthesis/inputs/pr5811-WORD.json.gz", + "sha256": "690656bfca9c6f0366527d158ca4edb14f83c410604d647953c20c7c94bea2e8", + "size": 122915 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223", + "path": "research/p104-unread-path-resynthesis/local.py", + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597", + "size": 9394 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "f2882694610b9bb49ddd7b6d99ccd628ae58be37", + "path": "research/p104-unread-path-resynthesis/pricing.py", + "sha256": "04b36429147f2809468d9ff037e26eaa70e66a5180e4b5c71a060bd5d14ffd9c", + "size": 11028 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "3b4c60838a43cb849707292bac144f14ad7fc8f1", + "path": "research/p104-unread-path-resynthesis/sources.py", + "sha256": "f96de7d80f369c12f6f904b7935610979d59617ed0d49963841e86b9a2b45557", + "size": 2488 + }, + { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "git_blob": "2a4d91891374a872dbee92b86bd21ebfb305c029", + "path": "research/p104-unread-path-resynthesis/verify.py", + "sha256": "41f71fff49c041d44048652228c901221555762f7ff3e11a088aa270ce6820a7", + "size": 7142 + } + ], + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "base_word": { + "commit": "4cef86d87e47dfcc5a511c99c9f0067c861271b0", + "git_blob": "fc6958401dfc110b48ecf6f0575111e9e2906438", + "local_path": "inputs/pr6143-WORD.json.gz", + "path": "research/p104-root-relay-descent/WORD.json.gz", + "pr": 6143, + "repository": "DreamingOfClouds/integer-mult-bounds", + "sha256": "108f3ae8ed1e30e8c525c13ab98159cb43a3b195b887bc24984eca3a95531436", + "size": 119977 + }, + "files": [ + { + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "path": "certificates/selected-result.json", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + }, + { + "git_blob": "1e10936044959f81a4c5fcd5bdb7b9e4c060ec8e", + "path": "research/p104-helper470-twin-rung-removal/inputs/pr5827-source.tar", + "sha256": "7af5908a4d83e83e28f59523fd7494841f669b7295311cfdbc3027fa65c5826d", + "usage": "input" + }, + { + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "path": "LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "usage": "input" + }, + { + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "size": 6824, + "usage": "input" + }, + { + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "path": "research/p104-native-channel/vendor/native_verify.py", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "size": 12323, + "usage": "input" + }, + { + "git_blob": "e7e663bebaf13f44c95fb8eb118b472cf377e137", + "path": "research/p104-contact-independent-audit/capsule/outputs/p104-native-contact-audit-20261025/check.py", + "sha256": "43fd40847a0853c0ac511d58ce77ef822a5c6dd1b25f662f01cefaa3196a2f7d", + "size": 11654, + "usage": "input" + } + ], + "pending_dependency_note": "PR6143 is not in publication ancestry. Its immutable WORD bytes are vendored and separately authenticated by size, SHA256, and Git blob in base_word; no source-history claim is made for that off-main head.", + "schema_version": 1, + "source_archive": { + "commit": "05cd36e5af06d7a3790e30ce3f449fa89b853768", + "files": 23, + "package": "research/p104-unread-path-resynthesis", + "pr": 5827, + "repository_path": "research/p104-helper470-twin-rung-removal/inputs/pr5827-source.tar", + "sha256": "7af5908a4d83e83e28f59523fd7494841f669b7295311cfdbc3027fa65c5826d" + } +} diff --git a/research/p104-owned772-relay-descent/TASK.json b/research/p104-owned772-relay-descent/TASK.json new file mode 100644 index 0000000000..1f204896cc --- /dev/null +++ b/research/p104-owned772-relay-descent/TASK.json @@ -0,0 +1,142 @@ +{ + "actual_scope": "Compose one new P104 owned-772/public-731 relay descent at root frame 595 with pending PR6143. Preserve arbitrary helper inputs by eight frame-3 compensations and release owned 791 after its last read. Check the complete word, paid/target invoice, compiler and outer claim.", + "ai_assistance": "Substantial OpenAI Codex assistance: coordinator and complementary construction, pricing and independent-check agents. AI reviews are not independent human acceptance.", + "assignment_seed": 33, + "author": "@CubeJerry, with OpenAI Codex assistance", + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "bottleneck_link": "The complete paid profile changes by 18*(-H1-H6+H7), with identical productive targets and caller boundaries. Strict subadditivity gives a positive signed gain for 0> shift for k, v in row.items()}, exponent - shift + return row, exponent + + +def scaled_row(state, numerator, denominator_exp): + row, exponent = state + return reduce_row({k: v * numerator for k, v in row.items()}, exponent + denominator_exp) + + +def accumulated_row(left, right, numerator, denominator_exp): + lr, le = left + rr, re = right + exponent = max(le, re + denominator_exp) + out = {k: v << (exponent - le) for k, v in lr.items()} + shift = exponent - re - denominator_exp + for k, v in rr.items(): + out[k] = out.get(k, 0) + ((v * numerator) << shift) + return reduce_row(out, exponent) + + +def replay(word): + n, m = word['public'], word['owned_fields'] + check(type(n) is int and 767 <= n <= 770, 'public inventory') + check(type(m) is int and 8 <= m <= 29, 'owned inventory') + check(len(word['initial']) == len(word['final']) == n, 'boundary dimensions') + check(len(word['program']) < 26000, 'retained event cap') + frames = [echelon(v) for v in word['frames']] + frame_count = len(frames) + check(all(type(f) is int and 0 <= f < frame_count for f in word['initial'] + word['final']), 'boundary frame indices') + rows = [({i: 1}, 0) for i in range(n + m)] + at = list(word['initial']) + [None] * m + allocated = set() + paid, operations = Counter(), Counter() + lifetimes = peak = scalar = 0 + for i, event in enumerate(word['program']): + check(isinstance(event, list) and len(event) >= 2, f'event form at {i}') + kind, target = event[:2] + check(type(target) is int and 0 <= target < n + m, f'target at {i}') + operations[kind] += 1 + if kind == 'MOVE': + check(len(event) == 5, f'MOVE arity at {i}') + old, new, private = event[2:] + check(type(old) is int and type(new) is int and 0 <= old < frame_count and 0 <= new < frame_count, f'MOVE frame index at {i}') + check(type(private) is bool and private == (target in allocated), f'MOVE ownership at {i}') + check(at[target] == old, f'MOVE source chart at {i}') + lower, upper = (new, old) if private else (old, new) + check(len(frames[lower]) < len(frames[upper]) and contains(frames[upper], frames[lower]), f'MOVE strict nesting at {i}') + paid[len(frames[upper]) - len(frames[lower])] += 1 + at[target] = new + elif kind == 'INIT': + check(len(event) == 3 and type(event[2]) is int and 0 <= event[2] < frame_count, f'INIT form at {i}') + check(target >= n and target not in allocated and at[target] is None, f'INIT ownership at {i}') + allocated.add(target) + rows[target] = ({}, 0) + at[target] = event[2] + lifetimes += 1 + peak = max(peak, len(allocated)) + scalar += 2 + elif kind == 'CLEAR': + check(len(event) == 3 and target in allocated and at[target] == event[2], f'CLEAR ownership/chart at {i}') + allocated.remove(target) + rows[target] = ({}, 0) + at[target] = None + scalar += 2 + else: + check(kind in ('ADD', 'COPY', 'SCALE'), f'known opcode at {i}') + check(len(event) == (4 if kind == 'SCALE' else 5), f'scalar arity at {i}') + coefficient = Fraction(event[-2]) + num, den = coefficient.numerator, coefficient.denominator + check(num != 0 and den & (den - 1) == 0 and abs(coefficient) + 1 < 2**16, f'dyadic bounded scalar at {i}') + check(type(event[-1]) is int and at[target] == event[-1] and at[target] is not None, f'scalar target chart at {i}') + exp = den.bit_length() - 1 + if kind == 'SCALE': + check(abs(num) & (abs(num) - 1) == 0, f'dyadic unit SCALE at {i}') + rows[target] = scaled_row(rows[target], num, exp) + scalar += 2 * (abs(abs(num).bit_length() - den.bit_length()) + int(num < 0)) + else: + source = event[2] + check(type(source) is int and 0 <= source < n + m and source != target, f'scalar source role at {i}') + check(at[source] == at[target], f'common chart at {i}') + if kind == 'COPY': + check(target in allocated and not rows[target][0], f'COPY cleared owned destination at {i}') + rows[target] = scaled_row(rows[source], num, exp) + else: + rows[target] = accumulated_row(rows[target], rows[source], num, exp) + scalar += 2 * (3 + abs(num).bit_length() - 1 + abs(num).bit_count() + exp) + check(not allocated and 0 < peak <= 13 and at[:n] == word['final'], 'complete return/storage contract') + live = set(word['live']) + check(len(live) == len(word['live']) == len(word['ports']) == 104 and all(type(r) is int and 0 <= r < 112 for r in live), 'main input inventory') + main = live | {r + 112 for r in live} + check(len(main) == 208, 'disjoint main roles') + for target, row in enumerate(rows): + expected = {target: 1} if target < n else {} + if target - 112 in live: + expected[target - 112] = 1 + check(row == (expected, 0), f'arbitrary-input endpoint row {target}') + helpers = Counter() + for r in range(n): + if r not in main: + a, b = frames[word['initial'][r]], frames[word['final'][r]] + check(len(a) < len(b) and contains(b, a), f'helper {r} endpoint inclusion') + helpers[len(b) - len(a)] += 1 + whole_paid = Counter({r: 18 * count for r, count in paid.items()}) + whole_targets = Counter({r: 18 * count for r, count in helpers.items()}) + whole_paid[1] += 1560 + whole_targets[145] += 208 + for length in (7, 8): + for position in range(1, length + 1): + whole_paid[8 * (position + 1)] += 208 + whole_targets[8 * (position + 1) + 1] += 208 + ordered = lambda counter: {str(k): v for k, v in sorted(counter.items())} + return { + 'events': len(word['program']), 'operations': dict(sorted(operations.items())), + 'rows_checked': n + m, 'endpoint_coefficients': (n + m)**2, + 'public': n, 'owned_fields': m, 'owned_lifetimes': lifetimes, + 'peak_owned': peak, 'real_scalar_allowance': scalar, + 'local_paid': ordered(paid), 'local_helpers': ordered(helpers), + 'whole_paid': ordered(whole_paid), 'whole_targets': ordered(whole_targets), + 'paid_calls': sum(whole_paid.values()), 'productive_fields': sum(whole_targets.values()), + 'paid_rank_mass': sum(k * v for k, v in whole_paid.items()), + 'target_rank_mass': sum(k * v for k, v in whole_targets.items()), + } + + +def audit(base, candidate, controls=True): + old, new = replay(base), replay(candidate) + check(base.keys() == candidate.keys(), 'same word schema fields') + check(all(base[k] == candidate[k] for k in base if k != 'program'), 'unchanged boundary and frame metadata') + delta = {k: new['local_paid'].get(k, 0) - old['local_paid'].get(k, 0) for k in set(new['local_paid']) | set(old['local_paid'])} + delta = {k: v for k, v in delta.items() if v} + check(delta == {'1': -1, '6': -1, '7': 1}, f'exact local paid delta: {delta}') + check(new['whole_targets'] == old['whole_targets'], 'unchanged complete target profile') + check(new['target_rank_mass'] - new['paid_rank_mass'] == 760, 'retained rank mass surplus') + references_791 = [(i, e) for i, e in enumerate(candidate['program']) + if e[1] == 791 or (e[0] in ('ADD', 'COPY') and e[2] == 791)] + check([e[0] for _, e in references_791] == ['INIT', 'COPY', 'ADD', 'COPY', 'CLEAR'], + 'complete retained owned-791 use sequence') + check(references_791[-2][1] == ['COPY', 770, 791, '1', 549] + and references_791[-1][0] == references_791[-2][0] + 1, + 'early owned-791 erasure immediately follows its final use') + result = {'base': old, 'candidate': new, 'local_paid_delta': delta, + 'owned791_references': references_791} + if controls: + faults = {} + def reject(label, changed): + try: + replay(changed) + except (ValueError, ZeroDivisionError) as error: + faults[label] = str(error) + else: + raise ValueError('Accepted negative control: ' + label) + # Select the newly inserted public-input compensation without relying on + # event indices or a generator's declarations. + old_events = Counter(tuple(e) for e in base['program']) + new_events = Counter(tuple(e) for e in candidate['program']) - old_events + compensations = {e for e in new_events if e[0] == 'ADD' and e[2] == 731 and e[-1] == 3} + check(compensations, 'new arbitrary-input compensation exists') + position = next(i for i, e in enumerate(candidate['program']) if tuple(e) in compensations) + word = deepcopy(candidate); del word['program'][position]; reject('omit_arbitrary_input_compensation', word) + word = deepcopy(candidate); word['program'][position][-2] = str(-Fraction(word['program'][position][-2])); reject('reverse_compensation_sign', word) + position = next(i for i, e in enumerate(candidate['program']) if e[0] == 'MOVE' and e[1] == 772) + word = deepcopy(candidate); word['program'][position][-1] = False; reject('borrow_owned_move', word) + word = deepcopy(candidate); word['program'][position][2] = 3; reject('wrong_move_source_chart', word) + position = next(i for i, e in enumerate(candidate['program']) if e[0] == 'CLEAR' and e[1] == 772) + word = deepcopy(candidate); del word['program'][position]; reject('omit_owned_return', word) + position = next(i for i, e in enumerate(candidate['program']) if e[0] == 'COPY' and e[1] == 772) + word = deepcopy(candidate); word['program'].insert(position, ['ADD', 772, word['program'][position][2], '1', word['program'][position][-1]]); reject('copy_into_dirty_owned', word) + position = next(i for i, e in enumerate(candidate['program']) if e[0] == 'SCALE' and e[1] == 772) + word = deepcopy(candidate); word['program'][position][-2] = '1/3'; reject('non_dyadic_scale', word) + word = deepcopy(candidate); word['program'][position][-2] = '3/2'; reject('nonunit_scale', word) + word = deepcopy(candidate); word['frames'][595].append(word['frames'][595][0]); reject('dependent_frame_basis', word) + clear791 = references_791[-1][0] + word = deepcopy(candidate) + word['program'][clear791 - 1], word['program'][clear791] = word['program'][clear791], word['program'][clear791 - 1] + reject('clear791_before_last_read', word) + position = next(i for i, e in enumerate(candidate['program']) if e == ['ADD', 162, 146, '-1', 529]) + word = deepcopy(candidate); del word['program'][position]; reject('omit_top162_compensation', word) + word = deepcopy(candidate) + held = word['program'].pop(clear791) + late = next(i for i, e in enumerate(word['program']) if e[0] == 'CLEAR' and e[1] == 772) + word['program'].insert(late + 1, held) + reject('hold791_across772_lifetime', word) + result['negative_controls'] = faults + return result + + +def new_summary(result): + candidate = result['candidate'] + return {'rows': candidate['rows_checked'], 'paid_calls': candidate['paid_calls'], 'negative_controls': len(result['negative_controls'])} + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('base', nargs='?', default=str(Path(__file__).resolve().parent / 'inputs/pr6143-WORD.json.gz')) + parser.add_argument('candidate', nargs='?', default=str(Path(__file__).resolve().parent / 'WORD.json.gz')) + parser.add_argument('--output') + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = audit(load(args.base), load(args.candidate)) + raw = json.dumps(result, sort_keys=True, indent=2) + '\n' + if args.output: + Path(args.output).write_text(raw) + receipt = Path(__file__).resolve().parent / 'INDEPENDENT.json' + if args.write: + receipt.write_text(raw) + else: + check(receipt.read_text() == raw, 'exact independent receipt') + print('PASS_INDEPENDENT_ROOT595_RELAY_AUDIT', new_summary(result)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-owned772-relay-descent/inputs/pr6143-WORD.json.gz b/research/p104-owned772-relay-descent/inputs/pr6143-WORD.json.gz new file mode 100644 index 0000000000..fc6958401d Binary files /dev/null and b/research/p104-owned772-relay-descent/inputs/pr6143-WORD.json.gz differ diff --git a/research/p104-owned772-relay-descent/native_audit.py b/research/p104-owned772-relay-descent/native_audit.py new file mode 100644 index 0000000000..a60e9b7c11 --- /dev/null +++ b/research/p104-owned772-relay-descent/native_audit.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Dense all-column check of four new paid MOVE pairs in the root595 edit. + +Three are new signed native maps; 3->529 was already used as helper 731's +endpoint and is retained here as a positive control. + +The inventory/lowering comparison follows Matarener's PR5960. It uses the +unchanged Clear1nsight exact Gaussian-dyadic dense interpreter and retained +Clifford/literal compilers, authenticated before import. New contribution: +source-bound delta selection and a reproducible four-map receipt. This is +finite native coverage, not the native_all_columns uniform assumption. +Prepared for @CubeJerry with OpenAI Codex assistance. Apache-2.0. +""" +from hashlib import sha1, sha256 +from pathlib import Path +import argparse +import gzip +import importlib.util +import json +import sys + +HERE = Path(__file__).resolve().parent + + +def need(ok, label): + if not ok: + raise ValueError(label) + + +def read(path): + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + + +def import_pinned(root): + pins = read(HERE / 'NATIVE-SOURCES.json')['files'] + modules = [] + for i, pin in enumerate(pins): + raw = (root / pin['path']).read_bytes() + need(len(raw) == pin['size'] and sha256(raw).hexdigest() == pin['sha256'] + and sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == pin['git_blob'], + 'immutable native source: ' + pin['path']) + name = f'root595_native_dependency_{i}' + spec = importlib.util.spec_from_file_location(name, root / pin['path']) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + modules.append(module) + return modules + + +def audit(base, candidate, root): + need(base['frames'] == candidate['frames'], 'unchanged native frames') + need(all(base[k] == candidate[k] for k in ('initial', 'final', 'live', 'ports')), 'unchanged helper maps and main adapters') + old = {(e[2], e[3]) for e in base['program'] if e[0] == 'MOVE'} + new = {(e[2], e[3]) for e in candidate['program'] if e[0] == 'MOVE'} + tasks = sorted(new - old) + need(tasks == [(3, 529), (520, 737), (529, 520), (737, 595)], 'complete new paid-MOVE-pair inventory') + main_roles = set(base['live']) | {r + 112 for r in base['live']} + old_helpers = {(base['initial'][r], base['final'][r]) + for r in range(base['public']) if r not in main_roles} + new_signed = set(tasks) - old_helpers + need(new_signed == {(520, 737), (529, 520), (737, 595)}, 'three new signed native maps') + compiler, literal, dense = import_pinned(root) + frames = candidate['frames'] + receipts = [] + control_recipe = control_expected = None + for a, b in tasks: + operator = compiler.canonical_frame(9, tuple(frames[a])).adjoint().then(compiler.canonical_frame(9, tuple(frames[b]))) + recipe, _ = compiler.lower_child(operator) + rank = abs(len(frames[a]) - len(frames[b])) + need(recipe['rank'] == rank, 'lowering rank') + actual = literal.recipe(recipe) + expected = literal.adjoint(literal.frame(frames[a], 9)) + literal.frame(frames[b], 9) + ac, ec = dense.compile_circuit(actual), dense.compile_circuit(expected) + digest = sha256() + for column in range(512): + left = dense.dense_column(ac, column) + right = dense.dense_column(ec, column) + need(left == right, f'exact column for {a}->{b}, {column}') + real, imag, exponent = left + need(sum(v*v for v in real) + sum(v*v for v in imag) == 1 << (2*exponent), 'unit column norm') + need(sum(bool(x or y) for x, y in zip(real, imag)) == 1 << rank, 'native child support rank') + digest.update(json.dumps([column, exponent, real, imag], separators=(',', ':')).encode()) + receipts.append({'frames': [a, b], 'rank': rank, 'columns': 512, + 'role': 'new_signed_map' if (a, b) in new_signed else 'existing_helper_map_positive_control', + 'matrix_sha256': digest.hexdigest()}) + if control_recipe is None: + control_recipe, control_expected = actual, expected + fault = control_recipe + (('phase', 1),) + need(literal.tableau(fault) == literal.tableau(control_recipe), 'phase-only mutation preserves signed tableau') + need(dense.first_difference(fault, control_expected) is not None, 'phase-only mutation rejected by dense interpreter') + flipped = list(control_recipe) + i = next(i for i, gate in enumerate(flipped) if gate[0] == 'C') + flipped[i] = ('C', flipped[i][1], -flipped[i][2]) + need(dense.first_difference(tuple(flipped), control_expected) is not None, 'child sign mutation rejected') + return {'paid_move_delta_maps': receipts, 'new_signed_map_count': len(new_signed), + 'columns_checked': 512*len(tasks), 'complex_entries_compared': 512*512*len(tasks), + 'unchanged_helper_maps_and_main_adapters': True, 'controls': {'absolute_phase_only': 'rejected', 'child_sign': 'rejected'}, + 'scope': 'Three new finite 9-qubit signed maps and one existing helper-map positive control; other unchanged maps reuse predecessor evidence; uniform native_all_columns remains assumed.'} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('base', nargs='?', default=str(HERE / 'inputs/pr6143-WORD.json.gz')) + parser.add_argument('candidate', nargs='?', default=str(HERE / 'WORD.json.gz')) + parser.add_argument('--source-root', type=Path, default=HERE.parents[1]) + parser.add_argument('--output', type=Path) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = audit(read(args.base), read(args.candidate), args.source_root) + raw = json.dumps(result, sort_keys=True, indent=2) + '\n' + if args.output: + args.output.write_text(raw) + receipt = HERE / 'NATIVE-AUDIT.json' + if args.write: + receipt.write_text(raw) + else: + need(receipt.read_text() == raw, 'exact dense native receipt') + print('PASS_ROOT595_NEW_NATIVE_MAPS', result['new_signed_map_count'], 'new signed maps;', result['columns_checked'], 'columns checked') + + +if __name__ == '__main__': + main() diff --git a/research/p104-owned772-relay-descent/pricing.py b/research/p104-owned772-relay-descent/pricing.py new file mode 100644 index 0000000000..71c972df08 --- /dev/null +++ b/research/p104-owned772-relay-descent/pricing.py @@ -0,0 +1,184 @@ +"""Complete mixed-target price, compiler and outer transfer. + +The interval and compiler bounds follow zxv and Cao Yifan. The productive +recursion is by Jacob Alan Sussman. The controller is by Cinna Davis. +Adapted from Ali Romman's PR5544/5545 for the two coupled contact changes. +Successor choices were prepared for thu-nmrc with OpenAI Codex assistance. +Helper-subspace targets were added by Ali Romman with OpenAI Codex assistance. +The source commuting-contact construction is by Pierre-Loic Doulcet (hexapode) in PR5565. +The source coupled-frame change is by Ali Romman with OpenAI Codex in PR5601. +Five fixed boundary relations are from Ali Romman's PR5602. +The shared and delayed relays are from flyingviper's PR5605 and PR5612. The preparation is from +Scratch-net's PR5606. Their costs and target debit are included. +Ali Romman's complete caller/price proof and all predecessor credit are retained. +The paid A2 change is from zxv PR5643. The three helper relations are from +Ali Romman PR5644. The four-gate change is by Ali Romman with Codex assistance. +The four interior basis changes are by Ali Romman with Codex assistance. +Paid intermediate meetings: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +import local as L + +KAPPA, TESTED = Q('0.003127804'), Q('0.003127809') +PREVIOUS = Q('0.003127137') + + +def encode(x): + if isinstance(x,Q): + return str(x) + if isinstance(x,dict): + return {str(k):encode(v) for k,v in x.items()} + if isinstance(x,(list,tuple)): + return [encode(v) for v in x] + return x + + +def assemble(local, native, word, physical): + paid, targets = Counter(), Counter() + counts = Counter() + L.need(local['helpers'] == native['helpers'], 'Every productive helper has a native target') + for e in word['physical_events']: + counts[e[0]] += 1 + if e[0] == 'LOCAL': + L.need(e[3] is False, 'Every source invocation is forward') + paid.update(local['paid']) + targets.update(local['helpers']) + elif e[0] == 'QUERY_SHEAR': + paid[1] += 104 + elif e[0] == 'IDLE': + paid[8*len(e[2])] += 208 + main = Counter() + idle = Counter({8*len(e[2]):0 for e in word['physical_events'] if e[0] == 'IDLE'}) + for e in word['physical_events']: + if e[0] == 'IDLE': + idle[8*len(e[2])] += 208 + L.need(idle == physical['whole_idle_jobs'], 'Every whole idle has a native Gaussian and full rank') + for term in word['diagonal']: + main[1+8*sum(term[1:])] += 104 + L.need(main == physical['main_targets'], 'Every main target has its full native phase') + targets.update(main) + L.need(counts['LOCAL'] == 18 and counts['QUERY_SHEAR'] == counts['IDLE'] == 15, 'Complete call census') + # Recount by the two path lengths, without using emitted main diagonals. + second_t = Counter({r:18*n for r,n in local['helpers'].items()}) + second_p = Counter({r:18*n for r,n in local['paid'].items()}) + second_t[145] += 208 + second_p[1] += 15*104 + for length in (7,8): + for j in range(1,length+1): + second_t[1+8*(j+1)] += 208 + second_p[8*(j+1)] += 208 + L.need((targets,paid) == (second_t,second_p), 'Independent full invoice') + L.need(max(targets) == 145 and max(paid) == 72, 'Maximum recursive ranks') + L.need(sum(targets.values()) == 13444 and sum(paid.values()) == 66780, 'Complete field and call counts') + L.need(sum(r*n for r,n in targets.items())-sum(r*n for r,n in paid.items()) == 760, 'Complete rank surplus') + return targets,paid,counts + + +def run(local,native,word,physical): + T,P,counts = assemble(local,native,word,physical) + E = L.load(L.ROOT/'research/higher-moment-strictification/verify.py','p104_productive_intervals') + other = L.load(L.ROOT/'research/kappa-rebuild/architecture/mixed_target_probe.py','p104_productive_second_intervals') + def margin(k): + a,b = E.moment(T,1-k), E.moment(P,1-k) + return a[0]-b[1],a[1]-b[0] + lo,hi,grid = 0,10**12,10**14 + while hi-lo > 1: + m=(lo+hi)//2 + if margin(Q(m,grid))[0] > 0: + lo=m + else: + hi=m + lower,upper = Q(lo,grid),Q(hi,grid) + signed = Counter(T) + signed.subtract(P) + cap = Q('.0034') + derivative_upper = Q(0) + for rank, count in signed.items(): + logarithm = E.log_bounds(rank) + low = E.mul(E.power(rank, 1-cap), logarithm)[0] + high = rank*logarithm[1] + derivative_upper -= count*(low if count >= 0 else high) + L.need(derivative_upper < 0, 'Unique raw crossing below the retained BIT cap') + L.need(margin(lower)[0] > 0 and margin(upper)[1] < 0, 'Strict rational crossing enclosure') + L.need(PREVIOUS < KAPPA < TESTED < lower and margin(PREVIOUS)[0] > 0, 'Changed complete bill improves the source claim') + t,u,v,c,b = 1-TESTED,Q(1,7),1024,16,17 + target,paid = E.moment(T,t),E.moment(P,t) + tl,th = other.moment(T,TESTED) + pl,ph = other.moment(P,TESTED) + L.need(tl > ph and max(tl,target[0]) <= min(th,target[1]) and max(pl,paid[0]) <= min(ph,paid[1]), 'Two exact moment engines') + alpha = E.divide(paid,target) + gamma = E.divide(E.moment(P,t+u),E.mul(E.power(c,u),target)) + delta = E.divide((Q(sum(T.values())*b),)*2,E.mul(E.power(c,TESTED),target)) + reserve,decay = Q(1,10**12),Q(125,128) + L.need(alpha[1] < 1-reserve and gamma[1] < decay and delta[1] < decay, 'All three charged tail ratios') + L.need(decay**128 < Q(1,16), 'Both tail decay blocks') + normalized = 1/(1+v*reserve)+Q(4,2**32) + L.need(normalized < 1 and c**64 < b**63, 'Full completion, splitting and rounding charges') + theta,power = Q(63,64),1024 + eta = E.scale(E.power(145,-v*TESTED),t) + L.need(2*(c**v)**64 <= (145**v)**63 and eta[0] > theta**power, 'Shifted exits and complement capacity') + L.need(E.power(145,v*TESTED)[1] < 2**power, 'Compiler initial range') + gap = (TESTED-KAPPA)/7 + L.need(gap.numerator == 1, 'Exact compiler integer grid') + step = gap.denominator + def wins(j): + return (step*j+1)**power < 2**j + left,right=1,2 + while not wins(right): + left,right=right,2*right + while right-left > 1: + m=(left+right)//2 + if wins(m): + right=m + else: + left=m + H=step*right + L.need(H > 8*v and wins(right) and not wins(right-1), 'Finite uniform threshold with predecessor rejection') + local_routes = (sum(local['paid'].values())+native['helper_normalizers']+native['main_adapters']+4*104+4*local['owned_lifetimes'])*1000 + L.need(local['real_scalar_allowance']+local_routes < 10**7, 'Every local scalar, route and owned operation is funded') + boundary = sum(len(word['boundaries'][side+'_program']) for side in ('left','right')) + raw = 18*10**7 + 15*1664 + 32*104*(len(word['physical_events'])+boundary) + raw += 32*104*(26+1000) + L.need(raw < 10**9, 'Complete nonrecursive raw bound') + bit = L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT'] + atom = Q(bit['atom']) + ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599') + admitted=Q(bit['admitted']) + L.need(atom > ordinary > admitted > TESTED and atom < 1-ordinary, 'Retained BIT admission and stock') + outer_module=L.load(L.ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py','p104_productive_outer') + params={'kappa':KAPPA,'tested_saving':TESTED,'complex_uniform_saving':KAPPA+6*gap, + 'b':KAPPA+5*gap,'a':KAPPA+4*gap,'q':KAPPA+3*gap,'bit_saving':admitted, + 'epsilon':1-gap,'beta':1-3*gap,'r0':gap/10,'stop':gap,'layout':gap,'d':gap} + outer=outer_module.ledger(params) + outer['functional_checks']['actual_new_BIT_stock_sublinear']=params['beta']*(1-atom) + L.need(len(outer['strict_checks']) == 54 and len(outer['functional_checks']) == 4, 'Complete outer predicate inventory') + L.need(all(x > 0 for key in ('strict_checks','functional_checks') for x in outer[key].values()), 'All outer inequalities strict') + wrong_cutoff = E.divide((Q(sum(T.values())*21),)*2,E.mul(E.power(20,TESTED),target)) + L.need(wrong_cutoff[0] > 1, 'Old cutoff fails with this helper inventory') + old_completion = E.divide((Q(sum(T.values())*18),)*2,E.mul(E.power(17,TESTED),target)) + L.need(old_completion[0] > Q(39,40), 'PR5718 completion-tail bound fails with the new target count') + old_offset = E.divide(E.moment(P,t+Q(1,5)),E.mul(E.power(16,Q(1,5)),target)) + L.need(old_offset[0] > decay, 'The old tail offset fails at the new cutoff') + bad=outer_module.ledger(dict(params,bit_saving=Q('.0027'))) + L.need(any(x <= 0 for x in bad['strict_checks'].values()), 'Insufficient BIT contract rejected') + return encode({'kappa':KAPPA,'kappa_decimal':'0.003127804','previous_pr6143':PREVIOUS,'gain':KAPPA-PREVIOUS, + 'relative_gain_percent':100*(KAPPA/PREVIOUS-1),'raw_root_interval':[lower,upper], + 'raw_headroom':[lower-KAPPA,upper-KAPPA], + 'raw_ceiling':{'interval':[Q(0),cap],'derivative_upper':derivative_upper},'margin_at_previous':E.display(margin(PREVIOUS)), + 'targets':T,'paid':P,'productive_fields':sum(T.values()),'paid_calls':sum(P.values()), + 'rank_mass_surplus':760,'full_forward_calls':18,'query_shears':15,'whole_idle_jobs':3120, + 'strictification':{'tested':TESTED,'power':v,'cutoff':c,'floor':b,'tail_offset':u,'reserve':reserve,'tail_decay':decay,'tail_block':128, + 'alpha':E.display(alpha),'gamma':E.display(gamma),'delta':E.display(delta),'normalized_paid_upper':normalized}, + 'compiler':{'theta':theta,'logarithm_power':power,'eta':E.display(eta),'gap':gap,'H':H,'N':'2^'+str(H), + 'integer_test_exponent':right,'uniform_saving':params['complex_uniform_saving'],'word_materialized':False}, + 'nonrecursive':{'local_scalar':local['real_scalar_allowance'],'local_routes':local_routes, + 'raw_scalar_upper':raw,'raw_budget':10**9,'peak_owned_fields':local['peak_owned_fields'], + 'fixed_scalar_growth_bound':'At most 2^(16*26000) before native factors; a declared constant, not an attained norm.', + 'local_paid_rank_mass':local['paid_rank_mass'], + 'tensor_native_growth_bound':'Each rank-r Gaussian has row l1 norm at most 2^(rf); use local_paid_rank_mass for the whole word.'}, + 'ordinary_BIT':bit,'outer':outer, + 'negative_controls':{'source_completion':'Rejected at cutoff17, floor18 and decay39/40', + 'source_offset':'Rejected at cutoff16 with tail offset1/5', + 'old_cutoff':'Rejected by completion-tail ratio greater than one','old_BIT':'Rejected by outer inequalities'}}) diff --git a/research/p104-owned772-relay-descent/sources.py b/research/p104-owned772-relay-descent/sources.py new file mode 100644 index 0000000000..c2b4b5d2c0 --- /dev/null +++ b/research/p104-owned772-relay-descent/sources.py @@ -0,0 +1,81 @@ +"""Authenticate PR6143's word (the base of the edit) and open PR5827's published package (the verifier chain) +before importing any of its code. + +Adapted for @CubeJerry with OpenAI Codex assistance from DreamingOfClouds' PR6143/PR6030 +(with Claude Opus 5.5 assistance) and the credited Ali Romman chain. Apache-2.0. +The archive format and per-file checks follow PR5827's own sources.py (Ali Romman, OpenAI Codex assistance). +""" +from contextlib import contextmanager +from hashlib import sha1, sha256 +from pathlib import Path, PurePosixPath +import importlib.util +import json +import sys +import tarfile +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + import gzip + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def authenticate(raw, pin): + need(len(raw) == pin['size'], 'Exact source size: ' + pin['path']) + need(sha256(raw).hexdigest() == pin['sha256'], 'Exact source SHA256: ' + pin['path']) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == pin['git_blob'], + 'Exact source Git blob: ' + pin['path']) + + +@contextmanager +def sources(): + """Yield the directory of PR5827's extracted package (every file authenticated).""" + pins = json.loads((HERE / 'SOURCES.json').read_bytes()) + archive = pins['source_archive'] + path = HERE.parents[1] / archive['repository_path'] + need(sha256(path.read_bytes()).hexdigest() == archive['sha256'], 'Exact source archive') + members = {p['path']: p for p in pins['archived_files']} + need(len(members) == len(pins['archived_files']) == archive['files'], 'Exact source inventory') + with tempfile.TemporaryDirectory(prefix='p104-base-source-') as directory: + root = Path(directory) + with tarfile.open(path, 'r:') as bundle: + seen = set() + for member in bundle.getmembers(): + name = PurePosixPath(member.name) + need(member.isfile() and not name.is_absolute() and '..' not in name.parts + and '\\' not in member.name and ':' not in member.name, + 'Regular relative source file') + need(member.name in members and member.name not in seen, 'Unique declared source file') + seen.add(member.name) + raw = bundle.extractfile(member).read() + authenticate(raw, members[member.name]) + target = root.joinpath(*name.parts) + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(raw) + need(seen == set(members), 'Complete source archive') + yield root / archive['package'] + + +def base_word(): + """PR6143's WORD.json.gz payload, authenticated against the exact pending-head pin in SOURCES.json.""" + import gzip + pin = json.loads((HERE / 'SOURCES.json').read_bytes())['base_word'] + raw = (HERE / pin['local_path']).read_bytes() + authenticate(raw, pin) + return json.loads(gzip.decompress(raw)) diff --git a/research/p104-owned772-relay-descent/test_portability.py b/research/p104-owned772-relay-descent/test_portability.py new file mode 100644 index 0000000000..e0b2cb071f --- /dev/null +++ b/research/p104-owned772-relay-descent/test_portability.py @@ -0,0 +1,87 @@ +"""Regenerated-output portability controls; immutable inputs stay exact. + +Maintainer repair by Douglas Colkitt with OpenAI Codex assistance. +Construction and verifier: DreamingOfClouds; retained predecessors in README. +Apache-2.0. +""" +from copy import deepcopy +import gzip +import io +import json +from pathlib import Path +import sys +import unittest +import zlib + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from construct import matches_shipped, payload +from sources import authenticate + + +class WordPortabilityTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.shipped = (HERE / 'WORD.json.gz').read_bytes() + cls.word = json.loads(gzip.decompress(cls.shipped)) + + def test_original_word(self): + self.assertTrue(matches_shipped(self.word, self.shipped)) + + def test_os_header_variants(self): + # Byte 9 is gzip's OS field. Neither the payload nor CRC changes. + for code in (0, 3, 19, 255): + changed = bytearray(self.shipped) + changed[9] = code + with self.subTest(os_code=code): + self.assertTrue(matches_shipped(self.word, bytes(changed))) + + def test_compression_timestamp_and_filename(self): + for level in (1, 6, 9): + with self.subTest(level=level): + buffer = io.BytesIO() + with gzip.GzipFile(filename='different-name.json', mode='wb', + compresslevel=level, mtime=1700000000, + fileobj=buffer) as stream: + stream.write(payload(self.word)) + self.assertNotEqual(buffer.getvalue(), self.shipped) + self.assertTrue(matches_shipped(self.word, buffer.getvalue())) + + def test_changed_event_and_unknown_field_rejected(self): + changed = deepcopy(self.word) + changed['program'].pop() + self.assertFalse(matches_shipped(changed, self.shipped)) + changed = deepcopy(self.word) + changed['unexpected_proof_field'] = 1 + self.assertFalse(matches_shipped(changed, self.shipped)) + + def test_boolean_is_not_an_integer(self): + changed = deepcopy(self.word) + move = next(event for event in changed['program'] if event[0] == 'MOVE') + self.assertIs(type(move[4]), bool) + move[4] = int(move[4]) + # Python object equality alone would silently accept this mutation. + self.assertEqual(changed, self.word) + self.assertFalse(matches_shipped(changed, self.shipped)) + + def test_extra_payload_and_corrupt_container_rejected(self): + self.assertFalse(matches_shipped(self.word, gzip.compress(payload(self.word) + b' '))) + self.assertFalse(matches_shipped(self.word, self.shipped + gzip.compress(b'not a word'))) + for bad in (self.shipped[:20], self.shipped[:-8] + b'\0' * 8): + with self.subTest(size=len(bad)): + with self.assertRaises((gzip.BadGzipFile, EOFError, zlib.error)): + matches_shipped(self.word, bad) + + def test_immutable_source_still_uses_exact_bytes(self): + pin = json.loads((HERE / 'SOURCES.json').read_bytes())['base_word'] + raw = (HERE / pin['local_path']).read_bytes() + authenticate(raw, pin) + changed = bytearray(raw) + changed[9] = 3 if raw[9] != 3 else 19 + self.assertEqual(gzip.decompress(raw), gzip.decompress(changed)) + with self.assertRaises(ValueError): + authenticate(bytes(changed), pin) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/p104-owned772-relay-descent/verify.py b/research/p104-owned772-relay-descent/verify.py new file mode 100644 index 0000000000..e6af37ceae --- /dev/null +++ b/research/p104-owned772-relay-descent/verify.py @@ -0,0 +1,149 @@ +"""Verify the edited PR6143 word with PR5827's own chain (the chain PR6143 used). Apache-2.0. + +Adapted for @CubeJerry with OpenAI Codex assistance from DreamingOfClouds' PR6143/PR6030 +(with Claude Opus 5.5 assistance) and the credited Ali Romman chain. The chain below is +PR5827's own verifier (its package is authenticated from inputs/ and loaded unmodified, apart from +pricing.py whose declared literal edits are in PRICING-EDITS.json); the word is regenerated by +construct.py from PR6143's word (authenticated against its exact pending-head pin) and the explicit edit list. +Parts: --part build (authentication, regeneration, exact replay and storage inventory), + --part chain (the complete chain; includes build). Default: chain. +""" +from collections import Counter +from contextlib import ExitStack +from copy import deepcopy +from fractions import Fraction as Q +from pathlib import Path +import json, sys, tempfile +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from sources import sources, load, need, read, authenticate, base_word +from construct import construct, matches_shipped + +EXPECT = read(HERE / 'EXPECT.json') + + +def reject(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('Invalid control accepted') + + +def delta(after, before): + value = Counter(after) + value.subtract(before) + return {str(r): n for r, n in sorted(value.items()) if n} + + +def run(part): + with ExitStack() as contexts: + parent = contexts.enter_context(sources()) # PR5827's extracted package + cursor = contexts.enter_context(load(parent / 'sources.py', 'base_source_top').sources()) + for depth in range(7): # PR5827's own seven-deep source chain + module = load(cursor / 'sources.py', 'base_source_' + str(depth)) + cursor, root = contexts.enter_context(module.sources()) + text = (parent / 'pricing.py').read_text(encoding='utf-8') + for old, new in read(HERE / 'PRICING-EDITS.json'): + need(text.count(old) == 1, 'Unique declared pricing edit') + text = text.replace(old, new) + need(text == (HERE / 'pricing.py').read_text(encoding='utf-8'), 'Shipped pricing.py = PR5827 pricing.py + declared edits only') + L = load(parent / 'local.py', 'local') + L.ROOT = root + source = base_word() # PR6143's word, authenticated + word = construct(source, read(HERE / 'EDIT.json.gz')) + need(matches_shipped(word, (HERE / 'WORD.json.gz').read_bytes()), 'Entire regenerated WORD payload, byte for byte') + need(all(type(e[4]) is bool for e in word['program'] if e[0] == 'MOVE'), 'Canonical MOVE private flags') + baseline, local = L.replay(source), L.replay(word) + need((local['public_inputs'], local['owned_fields'], local['owned_lifetimes'], local['peak_owned_fields']) == + (baseline['public_inputs'], baseline['owned_fields'], baseline['owned_lifetimes'], baseline['peak_owned_fields']) + == tuple(EXPECT['inventory']), 'Unchanged storage inventory') + need(len(word['program']) == EXPECT['events'] <= 26000, 'Event count within the retained bound') + need(delta(local['paid'], baseline['paid']) == EXPECT['paid_delta'], 'Exact paid-profile delta') + need(delta(local['helpers'], baseline['helpers']) == EXPECT['helper_delta'], 'Exact productive-target delta') + print('PASS regenerated WORD.json.gz, exact replay, storage inventory, paid delta', EXPECT['paid_delta'], flush=True) + if part == 'build': + print(EXPECT['status'] + '_BUILD'); return None + columns = L.reverse_columns(word) + need(columns['columns'] == 799, 'All input columns') + print('PASS all input columns and separate transpose', flush=True) + native = L.native(word) + C = load(root / 'research/p104-productive-controller/caller.py', 'base_caller') + caller = C.construct() + need(caller == read(root / 'research/p104-productive-controller/CONTROLLER.json'), 'Exact physical caller') + physical = C.physical(caller, word) + print('PASS native maps, absolute phases, adapters and complete physical caller', flush=True) + P = load(HERE / 'pricing.py', 'edit_price') + price = P.run(local, native, caller, physical) + need(price['raw_root_interval'] == EXPECT['interval'], 'Exact crossing interval') + need((price['paid_calls'], price['productive_fields'], price['rank_mass_surplus']) == + (EXPECT['paid_calls'], EXPECT['productive_fields'], EXPECT['rank_mass_surplus']), 'Invoice') + need(len(price['outer']['strict_checks']) == 54 and len(price['outer']['functional_checks']) == 4, 'Outer inventory') + # the base word's profile, scaled as in the invoice, must fail at the new claim + E = L.load(root / 'research/higher-moment-strictification/verify.py', 'base_price_engine') + old_p = {int(r): n for r, n in price['paid'].items()} + old_t = {int(r): n for r, n in price['targets'].items()} + for r in set(baseline['paid']) | set(local['paid']): + old_p[r] = old_p.get(r, 0) + 18 * (baseline['paid'].get(r, 0) - local['paid'].get(r, 0)) + for r in set(baseline['helpers']) | set(local['helpers']): + old_t[r] = old_t.get(r, 0) + 18 * (baseline['helpers'].get(r, 0) - local['helpers'].get(r, 0)) + margin = E.moment(old_t, 1 - P.KAPPA)[1] - E.moment(old_p, 1 - P.KAPPA)[0] + need(margin < 0, 'PR6143 full profile fails at the new claim') + print('PASS both rational engines, completion, compiler and all outer costs', price['raw_root_interval'], flush=True) + + controls = C.controls(caller) + for label, make in EXPECT_CONTROLS(word, source): + controls[label] = reject(make) + bad = deepcopy(local); bad['paid'][1] -= 1 + controls['unpaid_query'] = reject(lambda: P.assemble(bad, native, caller, physical)) + bad = deepcopy(local); bad['helpers'][9] += 1 + controls['extra_target_credit'] = reject(lambda: P.assemble(bad, native, caller, physical)) + bw = read(HERE / 'SOURCES.json')['base_word']; raw = (HERE / bw['local_path']).read_bytes() + controls['damaged_base_word'] = reject(lambda: authenticate(bytes([raw[0] ^ 1]) + raw[1:], bw)) + for pin in read(HERE / 'SOURCES.json')['archived_files'][:3]: + raw = (parent / Path(pin['path']).relative_to(read(HERE / 'SOURCES.json')['source_archive']['package'])).read_bytes() + controls['damaged_source_' + Path(pin['path']).name] = reject( + lambda raw=raw, pin=pin: authenticate(bytes([raw[0] ^ 1]) + raw[1:], pin)) + result = dict(status=EXPECT['status'], base_commit=EXPECT['base_commit'], source_local=baseline, local=local, + paid_delta=EXPECT['paid_delta'], target_delta=EXPECT['helper_delta'], separate_columns=columns, + native=native, physical_caller=physical, complete_cost=price, + base_margin_upper_at_new_claim=margin, controls=controls, + limits=['All five inherited framework assumptions remain.', + 'The large uniform word and rounded multiplier are not materialized.', + 'Author checks do not establish independent acceptance.', + 'The selected frontier is unchanged.']) + return P.encode(result) + + +def EXPECT_CONTROLS(word, source): + """Corruptions of the edited word that the exact replay must reject.""" + L = sys.modules['local'] + out = [] + for label, index in EXPECT['control_sites'].items(): + bad = deepcopy(word); bad['program'].pop(index) + out.append(('missing_' + label, lambda bad=bad: L.replay(bad))) + for label, index in EXPECT['sign_sites'].items(): + bad = deepcopy(word); q = Q(bad['program'][index][-2]); bad['program'][index][-2] = str(-q) + out.append(('wrong_sign_' + label, lambda bad=bad: L.replay(bad))) + return out + + +def main(): + part = sys.argv[sys.argv.index('--part') + 1] if '--part' in sys.argv else 'chain' + need(part in ('build', 'chain'), '--part must be build or chain') + with tempfile.TemporaryDirectory(prefix='p104-edit-bytecode-') as cache: + sys.pycache_prefix = cache + result = run(part) + if result is None: + return + path = HERE / 'RESULT.json' + if '--write' in sys.argv: + path.write_bytes((json.dumps(result, sort_keys=True, indent=2) + '\n').encode()) + else: + need(read(path) == result, 'Exact retained output: RESULT.json') + print(EXPECT['status'], flush=True) + + +if __name__ == '__main__': + main()