From 9494fc4e2ecd5070ca21b8b5422a77f046da3ac9 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Thu, 15 Oct 2026 17:06:00 +0530 Subject: [PATCH] Bit helper-deletion ladder under optimal window-respecting re-hosting (d = 0..6) Prices d further width-8 helper deletions on the bit supplier after PR1043's R438 and PR2423's re-hosting. - For each slack S = 45..99 there is a unique optimal slot layout: the exact DP plus an exhaustive cross-check of up to 728,466,365 layouts. - All window splits are feasible, and the placements are audited. - 21 certified endpoints under three declared local-profile models. Under PR1043's measured per-deletion delta, each deletion is worth about +0.082% c, reaching +0.494% at d = 6. The controls reproduce the PR589, PR1043 and PR2423 endpoints. An adversarial verifier recomputed all 21 rows independently. Bit headroom only; no kappa claim (the complex supplier binds). Co-Authored-By: Claude Opus 5.5 --- research/bit-deletion-ladder/README.md | 127 + research/bit-deletion-ladder/RECEIPT.json | 2568 +++++++++++++++++ research/bit-deletion-ladder/SOURCES.json | 18 + research/bit-deletion-ladder/TASK.json | 68 + research/bit-deletion-ladder/VERIFY.json | 21 + .../bit-deletion-ladder/deletion_ladder.py | 471 +++ research/bit-deletion-ladder/vendor/NOTICE.md | 17 + .../pr2423/vendor/pr1043/CERTIFICATE.json | 2052 +++++++++++++ .../vendor/pr2423/vendor/pr1043/NOTICE.md | 28 + .../vendor/pr2423/verify_rehost.py | 770 +++++ 10 files changed, 6140 insertions(+) create mode 100644 research/bit-deletion-ladder/README.md create mode 100644 research/bit-deletion-ladder/RECEIPT.json create mode 100644 research/bit-deletion-ladder/SOURCES.json create mode 100644 research/bit-deletion-ladder/TASK.json create mode 100644 research/bit-deletion-ladder/VERIFY.json create mode 100644 research/bit-deletion-ladder/deletion_ladder.py create mode 100644 research/bit-deletion-ladder/vendor/NOTICE.md create mode 100644 research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/CERTIFICATE.json create mode 100644 research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/NOTICE.md create mode 100644 research/bit-deletion-ladder/vendor/pr2423/verify_rehost.py diff --git a/research/bit-deletion-ladder/README.md b/research/bit-deletion-ladder/README.md new file mode 100644 index 0000000000..3a2ba1a6ae --- /dev/null +++ b/research/bit-deletion-ladder/README.md @@ -0,0 +1,127 @@ +# Bit-supplier helper-deletion ladder (d = 0..6) + +**Bit headroom only. No new κ. No word is built here.** The selected record is complex-bound. Rows with d ≥ 1 +price hypothetical words that have d fewer width-8 helpers, under a declared local-profile model. d = 1 is PR1043's +R438 word (open, not admitted) with PR2423's re-hosting. PR1250 (seed11) found that helper 470 is the only removable +helper of the fixed word, so d ≥ 2 needs changed words. This ladder prices what those words would be worth. + +## Result + +R = 439 − d. S = 3996 − 9R width-8 slack units per replica. The endpoint c is accepted at c and rejected at +c + 1e-24 by both pinned engines. + +| d | R | S | certified optimum (unique) | window splits | c TEMPLATE | c RANK1 | c RANK7 | % vs PR589 (T/R1/R7) | +|---|---|---|---|---|---|---|---|---| +| 0 | 439 | 45 | 9×(42,5) | 10/10 | 0.001733427039589844234749 | (same) | (same) | 0 / 0 / 0 | +| 1 | 438 | 54 | 10×(42,5)+1×(42,4) | 22/22 | 0.001734802047828389852783 | 0.001735999416922188281944 | 0.001734846264120199151475 | +0.0793 / +0.1484 / +0.0819 | +| 2 | 437 | 63 | 12×(42,5)+1×(28,3) | 26/26 | 0.001736238589146810207048 | 0.001738638963216633253344 | 0.001736327170598942735353 | +0.1622 / +0.3007 / +0.1673 | +| 3 | 436 | 72 | 14×(42,5)+1×(28,2) | 30/30 | 0.001737652736279473456500 | 0.001741261678825470976241 | 0.001737785828526572282621 | +0.2438 / +0.4520 / +0.2515 | +| 4 | 435 | 81 | 16×(42,5)+1×(14,1) | 34/34 | 0.001739118212671177105905 | 0.001743941623958466180686 | 0.001739295973174498110179 | +0.3283 / +0.6066 / +0.3386 | +| 5 | 434 | 90 | 18×(42,5) | 19/19 | 0.001740604775296424266918 | 0.001746648581745032521636 | 0.001740827361879356617556 | +0.4141 / +0.7627 / +0.4269 | +| 6 | 433 | 99 | 19×(42,5)+1×(42,4) | 40/40 | 0.001741991196114600260000 | 0.001749260420895977867718 | 0.001742258732839957487271 | +0.4941 / +0.9134 / +0.5095 | + +The local-profile models below add their delta once per deletion to PR589's R439 profile +{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}. Each delta removes rank mass 8, and the script checks this. + +- **TEMPLATE**: d·{1:−2, 2:+2, 3:−1, 7:−1}, PR1043's measured delta. +- **RANK1**: d·{1:−8}. +- **RANK7**: d·{7:−1, 1:−1}. + +**Increments.** Steps per deletion, in % of PR589's c, for d = 1..6: + +- TEMPLATE: 0.0793, 0.0829, 0.0816, 0.0845, 0.0858, 0.0800. +- RANK1: 0.148–0.156. +- RANK7: 0.082–0.088. + +The ladder is close to linear, at about +0.082% per deletion for TEMPLATE. The steps alternate because the +partial-slot layout changes with S mod 5. The prior float screen gave about +0.079% per deletion. That figure is the +d = 1 TEMPLATE step, and later steps are slightly larger. + +**Labels.** Neither alternative model is an envelope. RANK1 is not an upper envelope: with the same mass, {1:-10, 2:+1} gives c = 0.0017361170 and {1:-64, 7:+8} gives c = 0.0017452803 at d = 1, against RANK1's 0.0017359994 (adversarial reviewer). "RANK7" is not a lower envelope. With mass held fixed, removing {7, 1} is worth more than the TEMPLATE +delta, because g(r) = r(64/r)^c is concave, so 2g(2) > g(1) + g(3). TEMPLATE is the lowest of the three models in +every row. It is not a lower bound over arbitrary local changes either. Lowering eight rank-7 children by one each +(mass −8, no count change) would be worth less still. That case was not computed. + +**Layouts.** The optimum stays "fully idle 42-slots first". The leftover S mod 5 units go to a single partial slot: +(42,4) for residue 4, (28,3) for 3, (28,2) for 2 and (14,1) for 1. Runner-up gaps in moment units are all +positive, between 5.9e-8 and 3.3e-7. + +## What was checked (all in `deletion_ladder.py`, receipt `RECEIPT.json`) + +1. **DP.** PR2423's `certify_optimum` (exact top-3 interval DP) runs in a fixed-point loop. A candidate from the DP + at c0 + 1e-24 is priced, and the DP at the row's own c + 1e-24 must return the same layout. It does in every row. + The optimum and the runner-up are certified unique. Every one of the 21 rows is cross-checked by PR2423's + branch-and-bound `exhaustive_topk`. Layouts covered per d are 3,160,688; 10,556,685; 30,058,381; 75,757,148; + 173,394,328; 367,063,269; and 728,466,365. Each count equals an independent generating-function count, which + also reproduces PR2423's counts at S = 45 and 54. The exhaustive pass was tractable for every d (about 5 s at + S = 99), so it was not dropped anywhere. +2. **Windows.** Every split of each (capacity, u) count over the two children of its capacity class was tested + (10–40 per d). seed72 `maxflow_assign` and PR2423's all-subsets `hall_check` agree on every split, and all splits + are feasible at every d. For the all-in-children-6/7/8 split, an explicit placement of 9R occurrences per + replica was built and checked: + - built with seed14 `allocate` (R set on that module instance only); + - equal slot for slot to PR442 `hosting_core.expand`; + - audited by seed14 `placement_audit` and `owners_for_replicas` and by PR2423's `audit_slots`; + - remainders equal to the DP optimum. + At d = 1 its slot-list sha256 equals PR2423's placement. +3. **Endpoints.** PR1023 `packing.endpoint` (both engines plus the inherited surcharge) runs for 21 rows. The + hosted rank mass is invariant at 1,808,352, and there is one idle child per slot. +4. **Controls (88 negative, plus the positive ones below).** + - d = 0 gives PR589's c in all three models, and the layout is PR589's selection. + - d = 1 TEMPLATE local equals PR1043's certified profile, and c = 0.001734802047828389852783. + - d = 1 RANK7 local equals PR2423's transported-word profile (b), and c = 0.001734846264120199151475 = PR2423's c_b. + - PR2423's `verify_rehost.main` is replayed end to end (PASS, 29 controls) and agrees with c_a, c_b, the S = 54 + DP certificate and the placement hash. + - Negative controls (each must be rejected): + - Wrong slack S + 1 and S − 1, at every d. Rejected by the hosted-rank-mass check and by the window-demand total. + - R + 1 supply into the optimum. + - A DP with the optimum's rarest move dropped, compared against the exhaustive pass. + - The runner-up claimed optimal. + - c + 1e-24 accepted, for each of the 21 rows. + - A local model with mass −7. + - A local model with negative counts. + - Tampered vendored bytes. + +## Not verified / scope + +- **No word exists for d ≥ 2.** The local models are declared, not derived. Real changed words could have other + local deltas (see Labels above), other A-side costs, or fail PR1043-style legality and replay checks. +- **Fixed inputs.** W = 28416 (live stock 2KvT) and the PR589 frame, schedule, windows and capacities are held fixed + for every d. This is the same assumption PR2423 makes at d = 1. +- **Slot model scope.** The optimum is over the PR1023 no-bank, width-8-only slot model. Width-7 conversions, banks + and changes of slot capacities are out of scope. Window feasibility is shown a posteriori for the slot-model + optimum, and it holds, so no window-constrained re-optimisation was needed. +- **Engines.** Python stdlib engines only. The native C++17/Boost lane, which PR1043's review requests, was not run. +- **Runtime.** About 77 s on CPython 3.14.4, Linux x86_64, no network. Deterministic: `--check RECEIPT.json` passes + byte for byte. The script refuses `python -O`. + +## Reproduce + +From the repository root, CPython ≥ 3.10, standard library only, about 80 s: + + python3 -I -B research/bit-deletion-ladder/deletion_ladder.py --check research/bit-deletion-ladder/RECEIPT.json + +The expected final line starts with `PASS_BIT_DELETION_LADDER d=0..6 exhaustive=21/21 windows_feasible=7/7`. All +results were run on CPython 3.14.4; the registered Python 3.12 replay was not run locally. + +## Open next questions + +- Is there any changed word with a second removable helper? PR1250 says not on the fixed word. Pricing (d = 2) is + worth about +0.083% c over d = 1 under TEMPLATE. +- What is the true worst-case local delta per deletion, given the word's legal local moves? That would give a + certified lower envelope instead of three models. +- None of this moves κ unless the complex side stops binding. Bit headroom at d = 6 is still above complex. + +## Credits and licence + +- PR1043 (Ali Romman): the R438 deletion and its certificate (vendored). +- PR2423 (this author): the re-hosting DP, windows, placement and transport, vendored with pins. +- PR1023: the slot model and `g_interval`. +- seed72 and seed14 packages: windows, allocation and audits. +- PR589 / PR555: the selected bit word. +- PR1250 / `bit-source-substitution-seed11`: the result that only helper 470 is removable. + +Prepared by Sagar Thakrar with substantial AI assistance (Claude Code, Anthropic, Claude Opus 5.5). An AI builder +agent and an adversarial AI verifier were used. The verifier independently recomputed all 21 rows (layouts by +exhaustive enumeration, endpoints by Decimal bisection, windows by a 512-subset Hall test) and matched every +digit. No independent human review is claimed. Apache-2.0. diff --git a/research/bit-deletion-ladder/RECEIPT.json b/research/bit-deletion-ladder/RECEIPT.json new file mode 100644 index 0000000000..b81f26af76 --- /dev/null +++ b/research/bit-deletion-ladder/RECEIPT.json @@ -0,0 +1,2568 @@ +{ + "claims": { + "certificate": "per row: moment(opt, c+1e-24) > 1 by both engines; every other no-bank slot layout has a certified larger idle sum at c+1e-24 with the same child count and local profile; so no layout in the PR1023 slot model reaches c+1e-24 for that local model", + "kappa": "unchanged; the bit side does not bind", + "max_d": 6 + }, + "inputs": { + "main_tree": { + "research/bit-helper470-window-placement-seed14/verify.py": { + "git_blob": "c716a44e3b920f91918903d3480560e3882fbe80", + "sha256": "9cceeb610eccd6171585b056020ab6c44d7428de403a9ed035be1df9ae63f55b" + }, + "research/bit589-width-packing/SOURCES.json": { + "git_blob": "f6a97de32691a1d426ac4819aad24c0c8414d97e", + "sha256": "53fe98c8f01de7e32e3110e591d62e60292abb38cc11ecde4839f2eebd3b5fbc" + }, + "research/bit589-width-packing/packing.py": { + "git_blob": "a6079ee0dd4d8037be477a3c4497f472348bde07", + "sha256": "2bb5515807714807961289e4ee6958c3ad7e0c27bbec4d9212b138c662a6cc7b" + }, + "research/bit589-width7-windows-seed72/verify.py": { + "git_blob": "7f79a47146b150c9446e5f45e401d70b5cd12427", + "sha256": "a5341ed222af84b51cd18645dd6b23e4613c0275cbf2663c94b07a9f916e9e60" + }, + "research/bit589-width7-windows-seed72/windows.py": { + "git_blob": "4bb4f075ad5c1a49b4af310094bde6b2a4ea0c2e", + "sha256": "a24295a51333b168ab73215f8a4bbb5bf831be829f572d1cde15fc322049c635" + }, + "research/bit589-width7-windows-seed72/wopt.py": { + "git_blob": "4e0bd3704d1a2be460ed25b363e95918119e8d42", + "sha256": "a72daf1c7cff422543371a220fd391fe3b33552ac6ed52763f50b0c2f93d9532" + }, + "research/e8-bit-p111-tuned/data/selection9-p111.json": { + "git_blob": "e69ea66a3add357f570fc5552ab6368b3c8f9bb2", + "sha256": "4ab1ed4529683cd184987f8bc3031fb7408b9cd22c25ab9cf541a8aaf896eaf1" + }, + "research/e8-bit-p111-tuned/tune/EXPECTED.json": { + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py": { + "git_blob": "8864ca9b942a3507171edca0cf6cbaaf10fcf434", + "sha256": "57e558c80a2fea6e291587b04afd76dfaee3550729997798b61f33daf90b8ec9" + }, + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": { + "git_blob": "3df12bd632f1fdba825ced57110a1fee82eb2857", + "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py": { + "git_blob": "68b536daa9e6546c0aa046934bf840aaa3c3fde3", + "sha256": "d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3" + }, + "research/native-complex-moment552/engines/base_two_moment.py": { + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + "research/native-complex-moment552/engines/moment.py": { + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + "research/native-complex-moment552/engines/outer.py": { + "git_blob": "43007488ad2c43187c77cc6798beff8b1cd76ad2", + "sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c" + } + }, + "vendored": { + "vendor/pr2423/vendor/pr1043/CERTIFICATE.json": { + "git_blob": "56400920050c523e6e399f2455137b36c35cf528", + "origin": "PR1043 (Ali Romman, @aliromman) head e309e17f83f5759b1ea1fa24a76f24838784cb4d, research/bit-boundary-persistence/CERTIFICATE.json (via PR2423 vendor/pr1043/)", + "sha256": "32c6cd6103006d627909cabdaf5083238c661a6582016a8b21075bd01c892eff" + }, + "vendor/pr2423/verify_rehost.py": { + "git_blob": "58c76b9d7b6ed12e4473a4b38b5193f867b2d674", + "origin": "PR2423 (Sagar Thakrar, @thakrarsagar) head 13cd273dc13c98244b1f9bcf588b6e828cbc0347, research/bit-r438-transport-rehost/verify_rehost.py", + "sha256": "4774841de10a8386204519174c5e56eb14f5852b20058db38a65a1034eeba275" + } + } + }, + "ladder": [ + { + "R": 439, + "d": 0, + "exhaustive_layouts_covered": 3160688, + "layouts_total": 3160688, + "models": { + "rank1": { + "dp_certificate": { + "c_star": "0.001733427039589844234750", + "exhaustive_layouts_covered": 3160688, + "optimum": "9x(42,5)", + "optimum_idle_per_replica": { + "2": 435, + "4": 444, + "42": 9, + "6": 444, + "7": 666 + }, + "runner_up": "8x(42,5) + 1x(14,1) + 1x(42,4)", + "runner_up_gap_moment": [ + "0.0000003322715521960530587537556494937834", + "0.0000003322715521960530587537556494937835" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.018883656854406087435093441072030701", + "0.018883656854406087435093441072030702" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 435, + "34": 1, + "4": 444, + "42": 8, + "6": 443, + "7": 666 + }, + "slack_units": 45, + "third": "8x(42,5) + 1x(28,1) + 1x(42,4)" + }, + "endpoint": "0.001733427039589844234749", + "endpoint_fraction": "1733427039589844234749/1000000000000000000000000", + "gain_vs_pr589_percent": "0.00000000", + "hosted_children": 904896, + "hosted_profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "42": 288, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5129 + }, + "rank7": { + "dp_certificate": { + "c_star": "0.001733427039589844234750", + "exhaustive_layouts_covered": 3160688, + "optimum": "9x(42,5)", + "optimum_idle_per_replica": { + "2": 435, + "4": 444, + "42": 9, + "6": 444, + "7": 666 + }, + "runner_up": "8x(42,5) + 1x(14,1) + 1x(42,4)", + "runner_up_gap_moment": [ + "0.0000003322715521960530587537556494937834", + "0.0000003322715521960530587537556494937835" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.018883656854406087435093441072030701", + "0.018883656854406087435093441072030702" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 435, + "34": 1, + "4": 444, + "42": 8, + "6": 443, + "7": 666 + }, + "slack_units": 45, + "third": "8x(42,5) + 1x(28,1) + 1x(42,4)" + }, + "endpoint": "0.001733427039589844234749", + "endpoint_fraction": "1733427039589844234749/1000000000000000000000000", + "gain_vs_pr589_percent": "0.00000000", + "hosted_children": 904896, + "hosted_profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "42": 288, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5129 + }, + "template": { + "dp_certificate": { + "c_star": "0.001733427039589844234750", + "exhaustive_layouts_covered": 3160688, + "optimum": "9x(42,5)", + "optimum_idle_per_replica": { + "2": 435, + "4": 444, + "42": 9, + "6": 444, + "7": 666 + }, + "runner_up": "8x(42,5) + 1x(14,1) + 1x(42,4)", + "runner_up_gap_moment": [ + "0.0000003322715521960530587537556494937834", + "0.0000003322715521960530587537556494937835" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.018883656854406087435093441072030701", + "0.018883656854406087435093441072030702" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 435, + "34": 1, + "4": 444, + "42": 8, + "6": 443, + "7": 666 + }, + "slack_units": 45, + "third": "8x(42,5) + 1x(28,1) + 1x(42,4)" + }, + "endpoint": "0.001733427039589844234749", + "endpoint_fraction": "1733427039589844234749/1000000000000000000000000", + "gain_vs_pr589_percent": "0.00000000", + "hosted_children": 904896, + "hosted_profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "42": 288, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5129 + } + }, + "optimum": "9x(42,5)", + "optimum_idle_per_replica": { + "2": 435, + "4": 444, + "42": 9, + "6": 444, + "7": 666 + }, + "placement": { + "hosted_residual_roles": 126432, + "occurrences_per_replica": 3951, + "selection_patterns": [ + [ + 0, + [ + 8 + ], + 222 + ], + [ + 1, + [], + 222 + ], + [ + 2, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 3, + [], + 222 + ], + [ + 4, + [ + 8, + 8, + 8, + 8, + 8 + ], + 222 + ], + [ + 5, + [], + 222 + ], + [ + 6, + [], + 9 + ], + [ + 6, + [ + 8, + 8, + 8, + 8, + 8 + ], + 213 + ], + [ + 7, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 8, + [ + 8 + ], + 222 + ] + ], + "slot_list_sha256": "a7fc286701c36d5206b0f24f57bde0baffcec0e77e52a93dad80ad891c95e887", + "split": "9x(42,5) with split {\"6\": [[5, 9]]}" + }, + "runner_up": "8x(42,5) + 1x(14,1) + 1x(42,4)", + "slack_units_per_replica": 45, + "third": "8x(42,5) + 1x(28,1) + 1x(42,4)", + "windows": { + "note": "every split of each (capacity, u) count over the two children of that capacity class; seed72 maxflow_assign and the all-subsets Hall test agree on each", + "splits_checked": 10, + "splits_feasible": 10 + } + }, + { + "R": 438, + "d": 1, + "exhaustive_layouts_covered": 10556685, + "layouts_total": 10556685, + "models": { + "rank1": { + "dp_certificate": { + "c_star": "0.001735999416922188281945", + "exhaustive_layouts_covered": 10556685, + "optimum": "10x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 433, + "34": 1, + "4": 444, + "42": 10, + "6": 444, + "7": 666 + }, + "runner_up": "10x(42,5) + 1x(14,1) + 1x(28,3)", + "runner_up_gap_moment": [ + "0.0000001391379882539980782001065300463447", + "0.0000001391379882539980782001065300463448" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007907490148451218780268454315593864", + "0.007907490148451218780268454315593865" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 434, + "28": 1, + "4": 443, + "42": 10, + "6": 443, + "7": 666 + }, + "slack_units": 54, + "third": "10x(42,5) + 1x(28,1) + 1x(28,3)" + }, + "endpoint": "0.001735999416922188281944", + "endpoint_fraction": "216999927115273535243/125000000000000000000000", + "gain_vs_pr589_percent": "0.14839836", + "hosted_children": 902592, + "hosted_profile": { + "1": 378720, + "2": 400352, + "3": 22752, + "34": 32, + "4": 26880, + "42": 320, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1315, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5121, + "step_vs_previous_d_percent": "0.14839836" + }, + "rank7": { + "dp_certificate": { + "c_star": "0.001734846264120199151476", + "exhaustive_layouts_covered": 10556685, + "optimum": "10x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 433, + "34": 1, + "4": 444, + "42": 10, + "6": 444, + "7": 666 + }, + "runner_up": "10x(42,5) + 1x(14,1) + 1x(28,3)", + "runner_up_gap_moment": [ + "0.0000001390456087131328961495995128689269", + "0.0000001390456087131328961495995128689270" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007902240034384768753974039515366855", + "0.007902240034384768753974039515366856" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 434, + "28": 1, + "4": 443, + "42": 10, + "6": 443, + "7": 666 + }, + "slack_units": 54, + "third": "10x(42,5) + 1x(28,1) + 1x(28,3)" + }, + "endpoint": "0.001734846264120199151475", + "endpoint_fraction": "69393850564807966059/40000000000000000000000", + "gain_vs_pr589_percent": "0.08187391", + "hosted_children": 904320, + "hosted_profile": { + "1": 380736, + "2": 400352, + "3": 22752, + "34": 32, + "4": 26880, + "42": 320, + "5": 29376, + "6": 17376, + "7": 26496 + }, + "local_profile": { + "1": 1322, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 18 + }, + "local_rank_mass": 5121, + "step_vs_previous_d_percent": "0.08187391" + }, + "template": { + "dp_certificate": { + "c_star": "0.001734802047828389852784", + "exhaustive_layouts_covered": 10556685, + "optimum": "10x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 433, + "34": 1, + "4": 444, + "42": 10, + "6": 444, + "7": 666 + }, + "runner_up": "10x(42,5) + 1x(14,1) + 1x(28,3)", + "runner_up_gap_moment": [ + "0.0000001390420665268048703185105882609695", + "0.0000001390420665268048703185105882609696" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007902038724851374389941593752047420", + "0.007902038724851374389941593752047421" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 434, + "28": 1, + "4": 443, + "42": 10, + "6": 443, + "7": 666 + }, + "slack_units": 54, + "third": "10x(42,5) + 1x(28,1) + 1x(28,3)" + }, + "endpoint": "0.001734802047828389852783", + "endpoint_fraction": "1734802047828389852783/1000000000000000000000000", + "gain_vs_pr589_percent": "0.07932311", + "hosted_children": 904320, + "hosted_profile": { + "1": 380448, + "2": 400928, + "3": 22464, + "34": 32, + "4": 26880, + "42": 320, + "5": 29376, + "6": 17376, + "7": 26496 + }, + "local_profile": { + "1": 1321, + "2": 1344, + "3": 78, + "4": 44, + "5": 102, + "6": 11, + "7": 18 + }, + "local_rank_mass": 5121, + "step_vs_previous_d_percent": "0.07932311" + } + }, + "optimum": "10x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 433, + "34": 1, + "4": 444, + "42": 10, + "6": 444, + "7": 666 + }, + "placement": { + "hosted_residual_roles": 126144, + "occurrences_per_replica": 3942, + "selection_patterns": [ + [ + 0, + [ + 8 + ], + 222 + ], + [ + 1, + [], + 222 + ], + [ + 2, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 3, + [], + 222 + ], + [ + 4, + [ + 8, + 8, + 8, + 8, + 8 + ], + 222 + ], + [ + 5, + [], + 222 + ], + [ + 6, + [], + 10 + ], + [ + 6, + [ + 8 + ], + 1 + ], + [ + 6, + [ + 8, + 8, + 8, + 8, + 8 + ], + 211 + ], + [ + 7, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 8, + [ + 8 + ], + 222 + ] + ], + "slot_list_sha256": "1ef76bb87f1cfac7b4281c308bd71064c1fb1b6b4b267cfe9f3290212a5de11e", + "split": "10x(42,5) + 1x(42,4) with split {\"6\": [[4, 1], [5, 10]]}" + }, + "runner_up": "10x(42,5) + 1x(14,1) + 1x(28,3)", + "slack_units_per_replica": 54, + "third": "10x(42,5) + 1x(28,1) + 1x(28,3)", + "windows": { + "note": "every split of each (capacity, u) count over the two children of that capacity class; seed72 maxflow_assign and the all-subsets Hall test agree on each", + "splits_checked": 22, + "splits_feasible": 22 + } + }, + { + "R": 437, + "d": 2, + "exhaustive_layouts_covered": 30058381, + "layouts_total": 30058381, + "models": { + "rank1": { + "dp_certificate": { + "c_star": "0.001738638963216633253345", + "exhaustive_layouts_covered": 30058381, + "optimum": "12x(42,5) + 1x(28,3)", + "optimum_idle_per_replica": { + "2": 432, + "28": 1, + "4": 443, + "42": 12, + "6": 444, + "7": 666 + }, + "runner_up": "12x(42,5) + 1x(42,3)", + "runner_up_gap_moment": [ + "0.0000001358277578010348445979908476952031", + "0.0000001358277578010348445979908476952032" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007719363131348412288193015856213784", + "0.007719363131348412288193015856213785" + ], + "runner_up_idle_per_replica": { + "2": 431, + "26": 1, + "4": 444, + "42": 12, + "6": 444, + "7": 666 + }, + "slack_units": 63, + "third": "11x(42,5) + 2x(42,4)" + }, + "endpoint": "0.001738638963216633253344", + "endpoint_fraction": "54332467600519789167/31250000000000000000000", + "gain_vs_pr589_percent": "0.30067164", + "hosted_children": 900288, + "hosted_profile": { + "1": 376416, + "2": 400320, + "28": 32, + "3": 22752, + "4": 26848, + "42": 384, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1307, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5113, + "step_vs_previous_d_percent": "0.15227328" + }, + "rank7": { + "dp_certificate": { + "c_star": "0.001736327170598942735354", + "exhaustive_layouts_covered": 30058381, + "optimum": "12x(42,5) + 1x(28,3)", + "optimum_idle_per_replica": { + "2": 432, + "28": 1, + "4": 443, + "42": 12, + "6": 444, + "7": 666 + }, + "runner_up": "12x(42,5) + 1x(42,3)", + "runner_up_gap_moment": [ + "0.0000001356468465108521742318809762622283", + "0.0000001356468465108521742318809762622284" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007709081580904750765946259642934961", + "0.007709081580904750765946259642934962" + ], + "runner_up_idle_per_replica": { + "2": 431, + "26": 1, + "4": 444, + "42": 12, + "6": 444, + "7": 666 + }, + "slack_units": 63, + "third": "11x(42,5) + 2x(42,4)" + }, + "endpoint": "0.001736327170598942735353", + "endpoint_fraction": "1736327170598942735353/1000000000000000000000000", + "gain_vs_pr589_percent": "0.16730620", + "hosted_children": 903744, + "hosted_profile": { + "1": 380448, + "2": 400320, + "28": 32, + "3": 22752, + "4": 26848, + "42": 384, + "5": 29376, + "6": 17376, + "7": 26208 + }, + "local_profile": { + "1": 1321, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 17 + }, + "local_rank_mass": 5113, + "step_vs_previous_d_percent": "0.08543229" + }, + "template": { + "dp_certificate": { + "c_star": "0.001736238589146810207049", + "exhaustive_layouts_covered": 30058381, + "optimum": "12x(42,5) + 1x(28,3)", + "optimum_idle_per_replica": { + "2": 432, + "28": 1, + "4": 443, + "42": 12, + "6": 444, + "7": 666 + }, + "runner_up": "12x(42,5) + 1x(42,3)", + "runner_up_gap_moment": [ + "0.0000001356399145105257381262671178737936", + "0.0000001356399145105257381262671178737937" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007708687621462198749192012843003439", + "0.007708687621462198749192012843003440" + ], + "runner_up_idle_per_replica": { + "2": 431, + "26": 1, + "4": 444, + "42": 12, + "6": 444, + "7": 666 + }, + "slack_units": 63, + "third": "11x(42,5) + 2x(42,4)" + }, + "endpoint": "0.001736238589146810207048", + "endpoint_fraction": "217029823643351275881/125000000000000000000000", + "gain_vs_pr589_percent": "0.16219601", + "hosted_children": 903744, + "hosted_profile": { + "1": 379872, + "2": 401472, + "28": 32, + "3": 22176, + "4": 26848, + "42": 384, + "5": 29376, + "6": 17376, + "7": 26208 + }, + "local_profile": { + "1": 1319, + "2": 1346, + "3": 77, + "4": 44, + "5": 102, + "6": 11, + "7": 17 + }, + "local_rank_mass": 5113, + "step_vs_previous_d_percent": "0.08287290" + } + }, + "optimum": "12x(42,5) + 1x(28,3)", + "optimum_idle_per_replica": { + "2": 432, + "28": 1, + "4": 443, + "42": 12, + "6": 444, + "7": 666 + }, + "placement": { + "hosted_residual_roles": 125856, + "occurrences_per_replica": 3933, + "selection_patterns": [ + [ + 0, + [ + 8 + ], + 222 + ], + [ + 1, + [], + 222 + ], + [ + 2, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 3, + [], + 222 + ], + [ + 4, + [ + 8, + 8, + 8, + 8, + 8 + ], + 222 + ], + [ + 5, + [], + 222 + ], + [ + 6, + [], + 12 + ], + [ + 6, + [ + 8, + 8, + 8, + 8, + 8 + ], + 210 + ], + [ + 7, + [], + 1 + ], + [ + 7, + [ + 8, + 8, + 8 + ], + 221 + ], + [ + 8, + [ + 8 + ], + 222 + ] + ], + "slot_list_sha256": "c1f6930b8e81a5b34b3a7af4b10c5ccc94e1ee3b63e44c5f7eb0574633b8c023", + "split": "12x(42,5) + 1x(28,3) with split {\"6\": [[5, 12]], \"7\": [[3, 1]]}" + }, + "runner_up": "12x(42,5) + 1x(42,3)", + "slack_units_per_replica": 63, + "third": "11x(42,5) + 2x(42,4)", + "windows": { + "note": "every split of each (capacity, u) count over the two children of that capacity class; seed72 maxflow_assign and the all-subsets Hall test agree on each", + "splits_checked": 26, + "splits_feasible": 26 + } + }, + { + "R": 436, + "d": 3, + "exhaustive_layouts_covered": 75757148, + "layouts_total": 75757148, + "models": { + "rank1": { + "dp_certificate": { + "c_star": "0.001741261678825470976242", + "exhaustive_layouts_covered": 75757148, + "optimum": "14x(42,5) + 1x(28,2)", + "optimum_idle_per_replica": { + "2": 430, + "20": 1, + "4": 443, + "42": 14, + "6": 444, + "7": 666 + }, + "runner_up": "14x(42,5) + 2x(14,1)", + "runner_up_gap_moment": [ + "0.0000000606020657432071388225873574239364", + "0.0000000606020657432071388225873574239365" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.003444136600317948113565284697117157", + "0.003444136600317948113565284697117158" + ], + "runner_up_idle_per_replica": { + "14": 2, + "2": 430, + "4": 444, + "42": 14, + "6": 442, + "7": 666 + }, + "slack_units": 72, + "third": "13x(42,5) + 1x(28,3) + 1x(42,4)" + }, + "endpoint": "0.001741261678825470976241", + "endpoint_fraction": "1741261678825470976241/1000000000000000000000000", + "gain_vs_pr589_percent": "0.45197398", + "hosted_children": 897984, + "hosted_profile": { + "1": 374112, + "2": 400256, + "20": 32, + "3": 22752, + "4": 26848, + "42": 448, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1299, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5105, + "step_vs_previous_d_percent": "0.15130233" + }, + "rank7": { + "dp_certificate": { + "c_star": "0.001737785828526572282622", + "exhaustive_layouts_covered": 75757148, + "optimum": "14x(42,5) + 1x(28,2)", + "optimum_idle_per_replica": { + "2": 430, + "20": 1, + "4": 443, + "42": 14, + "6": 444, + "7": 666 + }, + "runner_up": "14x(42,5) + 2x(14,1)", + "runner_up_gap_moment": [ + "0.0000000604810343691094303483870186625860", + "0.0000000604810343691094303483870186625861" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.003437258145265227145559531044632088", + "0.003437258145265227145559531044632089" + ], + "runner_up_idle_per_replica": { + "14": 2, + "2": 430, + "4": 444, + "42": 14, + "6": 442, + "7": 666 + }, + "slack_units": 72, + "third": "13x(42,5) + 1x(28,3) + 1x(42,4)" + }, + "endpoint": "0.001737785828526572282621", + "endpoint_fraction": "1737785828526572282621/1000000000000000000000000", + "gain_vs_pr589_percent": "0.25145499", + "hosted_children": 903168, + "hosted_profile": { + "1": 380160, + "2": 400256, + "20": 32, + "3": 22752, + "4": 26848, + "42": 448, + "5": 29376, + "6": 17376, + "7": 25920 + }, + "local_profile": { + "1": 1320, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 16 + }, + "local_rank_mass": 5105, + "step_vs_previous_d_percent": "0.08414879" + }, + "template": { + "dp_certificate": { + "c_star": "0.001737652736279473456501", + "exhaustive_layouts_covered": 75757148, + "optimum": "14x(42,5) + 1x(28,2)", + "optimum_idle_per_replica": { + "2": 430, + "20": 1, + "4": 443, + "42": 14, + "6": 444, + "7": 666 + }, + "runner_up": "14x(42,5) + 2x(14,1)", + "runner_up_gap_moment": [ + "0.0000000604764000149857188780790716484462", + "0.0000000604764000149857188780790716484463" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.003436994765651668375278989799924494", + "0.003436994765651668375278989799924495" + ], + "runner_up_idle_per_replica": { + "14": 2, + "2": 430, + "4": 444, + "42": 14, + "6": 442, + "7": 666 + }, + "slack_units": 72, + "third": "13x(42,5) + 1x(28,3) + 1x(42,4)" + }, + "endpoint": "0.001737652736279473456500", + "endpoint_fraction": "3475305472558946913/2000000000000000000000", + "gain_vs_pr589_percent": "0.24377701", + "hosted_children": 903168, + "hosted_profile": { + "1": 379296, + "2": 401984, + "20": 32, + "3": 21888, + "4": 26848, + "42": 448, + "5": 29376, + "6": 17376, + "7": 25920 + }, + "local_profile": { + "1": 1317, + "2": 1348, + "3": 76, + "4": 44, + "5": 102, + "6": 11, + "7": 16 + }, + "local_rank_mass": 5105, + "step_vs_previous_d_percent": "0.08158100" + } + }, + "optimum": "14x(42,5) + 1x(28,2)", + "optimum_idle_per_replica": { + "2": 430, + "20": 1, + "4": 443, + "42": 14, + "6": 444, + "7": 666 + }, + "placement": { + "hosted_residual_roles": 125568, + "occurrences_per_replica": 3924, + "selection_patterns": [ + [ + 0, + [ + 8 + ], + 222 + ], + [ + 1, + [], + 222 + ], + [ + 2, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 3, + [], + 222 + ], + [ + 4, + [ + 8, + 8, + 8, + 8, + 8 + ], + 222 + ], + [ + 5, + [], + 222 + ], + [ + 6, + [], + 14 + ], + [ + 6, + [ + 8, + 8, + 8, + 8, + 8 + ], + 208 + ], + [ + 7, + [ + 8 + ], + 1 + ], + [ + 7, + [ + 8, + 8, + 8 + ], + 221 + ], + [ + 8, + [ + 8 + ], + 222 + ] + ], + "slot_list_sha256": "d8b49cb2fa692c1f7d9c8b02fbe100226f5c1a900c5a8a3c44aa20073cf3a7da", + "split": "14x(42,5) + 1x(28,2) with split {\"6\": [[5, 14]], \"7\": [[2, 1]]}" + }, + "runner_up": "14x(42,5) + 2x(14,1)", + "slack_units_per_replica": 72, + "third": "13x(42,5) + 1x(28,3) + 1x(42,4)", + "windows": { + "note": "every split of each (capacity, u) count over the two children of that capacity class; seed72 maxflow_assign and the all-subsets Hall test agree on each", + "splits_checked": 30, + "splits_feasible": 30 + } + }, + { + "R": 435, + "d": 4, + "exhaustive_layouts_covered": 173394328, + "layouts_total": 173394328, + "models": { + "rank1": { + "dp_certificate": { + "c_star": "0.001743941623958466180687", + "exhaustive_layouts_covered": 173394328, + "optimum": "16x(42,5) + 1x(14,1)", + "optimum_idle_per_replica": { + "14": 1, + "2": 428, + "4": 444, + "42": 16, + "6": 443, + "7": 666 + }, + "runner_up": "16x(42,5) + 1x(28,1)", + "runner_up_gap_moment": [ + "0.0000000591062961728324715427467109242120", + "0.0000000591062961728324715427467109242121" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.003359129024094415022717381075244816", + "0.003359129024094415022717381075244817" + ], + "runner_up_idle_per_replica": { + "12": 1, + "2": 428, + "4": 443, + "42": 16, + "6": 444, + "7": 666 + }, + "slack_units": 81, + "third": "16x(42,5) + 1x(42,1)" + }, + "endpoint": "0.001743941623958466180686", + "endpoint_fraction": "871970811979233090343/500000000000000000000000", + "gain_vs_pr589_percent": "0.60657784", + "hosted_children": 895680, + "hosted_profile": { + "1": 371808, + "14": 32, + "2": 400192, + "3": 22752, + "4": 26880, + "42": 512, + "5": 29376, + "6": 17344, + "7": 26784 + }, + "local_profile": { + "1": 1291, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5097, + "step_vs_previous_d_percent": "0.15460386" + }, + "rank7": { + "dp_certificate": { + "c_star": "0.001739295973174498110180", + "exhaustive_layouts_covered": 173394328, + "optimum": "16x(42,5) + 1x(14,1)", + "optimum_idle_per_replica": { + "14": 1, + "2": 428, + "4": 444, + "42": 16, + "6": 443, + "7": 666 + }, + "runner_up": "16x(42,5) + 1x(28,1)", + "runner_up_gap_moment": [ + "0.0000000589485483437494291514595945183036", + "0.0000000589485483437494291514595945183037" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.003350163899471967557535751675664230", + "0.003350163899471967557535751675664231" + ], + "runner_up_idle_per_replica": { + "12": 1, + "2": 428, + "4": 443, + "42": 16, + "6": 444, + "7": 666 + }, + "slack_units": 81, + "third": "16x(42,5) + 1x(42,1)" + }, + "endpoint": "0.001739295973174498110179", + "endpoint_fraction": "1739295973174498110179/1000000000000000000000000", + "gain_vs_pr589_percent": "0.33857401", + "hosted_children": 902592, + "hosted_profile": { + "1": 379872, + "14": 32, + "2": 400192, + "3": 22752, + "4": 26880, + "42": 512, + "5": 29376, + "6": 17344, + "7": 25632 + }, + "local_profile": { + "1": 1319, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 15 + }, + "local_rank_mass": 5097, + "step_vs_previous_d_percent": "0.08711901" + }, + "template": { + "dp_certificate": { + "c_star": "0.001739118212671177105906", + "exhaustive_layouts_covered": 173394328, + "optimum": "16x(42,5) + 1x(14,1)", + "optimum_idle_per_replica": { + "14": 1, + "2": 428, + "4": 444, + "42": 16, + "6": 443, + "7": 666 + }, + "runner_up": "16x(42,5) + 1x(28,1)", + "runner_up_gap_moment": [ + "0.0000000589425123352396437836422316824672", + "0.0000000589425123352396437836422316824673" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.003349820861036339435511955310977977", + "0.003349820861036339435511955310977978" + ], + "runner_up_idle_per_replica": { + "12": 1, + "2": 428, + "4": 443, + "42": 16, + "6": 444, + "7": 666 + }, + "slack_units": 81, + "third": "16x(42,5) + 1x(42,1)" + }, + "endpoint": "0.001739118212671177105905", + "endpoint_fraction": "347823642534235421181/200000000000000000000000", + "gain_vs_pr589_percent": "0.32831915", + "hosted_children": 902592, + "hosted_profile": { + "1": 378720, + "14": 32, + "2": 402496, + "3": 21600, + "4": 26880, + "42": 512, + "5": 29376, + "6": 17344, + "7": 25632 + }, + "local_profile": { + "1": 1315, + "2": 1350, + "3": 75, + "4": 44, + "5": 102, + "6": 11, + "7": 15 + }, + "local_rank_mass": 5097, + "step_vs_previous_d_percent": "0.08454214" + } + }, + "optimum": "16x(42,5) + 1x(14,1)", + "optimum_idle_per_replica": { + "14": 1, + "2": 428, + "4": 444, + "42": 16, + "6": 443, + "7": 666 + }, + "placement": { + "hosted_residual_roles": 125280, + "occurrences_per_replica": 3915, + "selection_patterns": [ + [ + 0, + [ + 8 + ], + 222 + ], + [ + 1, + [], + 222 + ], + [ + 2, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 3, + [], + 222 + ], + [ + 4, + [ + 8, + 8, + 8, + 8, + 8 + ], + 222 + ], + [ + 5, + [], + 222 + ], + [ + 6, + [], + 16 + ], + [ + 6, + [ + 8, + 8, + 8, + 8, + 8 + ], + 206 + ], + [ + 7, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 8, + [], + 1 + ], + [ + 8, + [ + 8 + ], + 221 + ] + ], + "slot_list_sha256": "ca7d4013e95bb2a2d6f2eafa6f82b8f66d07fecb43b1a39db283c50fac37f59c", + "split": "16x(42,5) + 1x(14,1) with split {\"6\": [[5, 16]], \"8\": [[1, 1]]}" + }, + "runner_up": "16x(42,5) + 1x(28,1)", + "slack_units_per_replica": 81, + "third": "16x(42,5) + 1x(42,1)", + "windows": { + "note": "every split of each (capacity, u) count over the two children of that capacity class; seed72 maxflow_assign and the all-subsets Hall test agree on each", + "splits_checked": 34, + "splits_feasible": 34 + } + }, + { + "R": 434, + "d": 5, + "exhaustive_layouts_covered": 367063269, + "layouts_total": 367063269, + "models": { + "rank1": { + "dp_certificate": { + "c_star": "0.001746648581745032521637", + "exhaustive_layouts_covered": 367063269, + "optimum": "18x(42,5)", + "optimum_idle_per_replica": { + "2": 426, + "4": 444, + "42": 18, + "6": 444, + "7": 666 + }, + "runner_up": "17x(42,5) + 1x(14,1) + 1x(42,4)", + "runner_up_gap_moment": [ + "0.0000003348069038748488592721725824210245", + "0.0000003348069038748488592721725824210246" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.019027745961015410370156112204151666", + "0.019027745961015410370156112204151667" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 426, + "34": 1, + "4": 444, + "42": 17, + "6": 443, + "7": 666 + }, + "slack_units": 90, + "third": "17x(42,5) + 1x(28,1) + 1x(42,4)" + }, + "endpoint": "0.001746648581745032521636", + "endpoint_fraction": "436662145436258130409/250000000000000000000000", + "gain_vs_pr589_percent": "0.76274004", + "hosted_children": 893376, + "hosted_profile": { + "1": 369504, + "2": 400128, + "3": 22752, + "4": 26880, + "42": 576, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1283, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5089, + "step_vs_previous_d_percent": "0.15616219" + }, + "rank7": { + "dp_certificate": { + "c_star": "0.001740827361879356617557", + "exhaustive_layouts_covered": 367063269, + "optimum": "18x(42,5)", + "optimum_idle_per_replica": { + "2": 426, + "4": 444, + "42": 18, + "6": 444, + "7": 666 + }, + "runner_up": "17x(42,5) + 1x(14,1) + 1x(42,4)", + "runner_up_gap_moment": [ + "0.0000003336906298752232518490505540675259", + "0.0000003336906298752232518490505540675260" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.018964305877068687849085241088765636", + "0.018964305877068687849085241088765637" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 426, + "34": 1, + "4": 444, + "42": 17, + "6": 443, + "7": 666 + }, + "slack_units": 90, + "third": "17x(42,5) + 1x(28,1) + 1x(42,4)" + }, + "endpoint": "0.001740827361879356617556", + "endpoint_fraction": "435206840469839154389/250000000000000000000000", + "gain_vs_pr589_percent": "0.42691859", + "hosted_children": 902016, + "hosted_profile": { + "1": 379584, + "2": 400128, + "3": 22752, + "4": 26880, + "42": 576, + "5": 29376, + "6": 17376, + "7": 25344 + }, + "local_profile": { + "1": 1318, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 14 + }, + "local_rank_mass": 5089, + "step_vs_previous_d_percent": "0.08834457" + }, + "template": { + "dp_certificate": { + "c_star": "0.001740604775296424266919", + "exhaustive_layouts_covered": 367063269, + "optimum": "18x(42,5)", + "optimum_idle_per_replica": { + "2": 426, + "4": 444, + "42": 18, + "6": 444, + "7": 666 + }, + "runner_up": "17x(42,5) + 1x(14,1) + 1x(42,4)", + "runner_up_gap_moment": [ + "0.0000003336479468485683183525304225717316", + "0.0000003336479468485683183525304225717317" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.018961880115297834668611008975596655", + "0.018961880115297834668611008975596656" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 426, + "34": 1, + "4": 444, + "42": 17, + "6": 443, + "7": 666 + }, + "slack_units": 90, + "third": "17x(42,5) + 1x(28,1) + 1x(42,4)" + }, + "endpoint": "0.001740604775296424266918", + "endpoint_fraction": "870302387648212133459/500000000000000000000000", + "gain_vs_pr589_percent": "0.41407775", + "hosted_children": 902016, + "hosted_profile": { + "1": 378144, + "2": 403008, + "3": 21312, + "4": 26880, + "42": 576, + "5": 29376, + "6": 17376, + "7": 25344 + }, + "local_profile": { + "1": 1313, + "2": 1352, + "3": 74, + "4": 44, + "5": 102, + "6": 11, + "7": 14 + }, + "local_rank_mass": 5089, + "step_vs_previous_d_percent": "0.08575859" + } + }, + "optimum": "18x(42,5)", + "optimum_idle_per_replica": { + "2": 426, + "4": 444, + "42": 18, + "6": 444, + "7": 666 + }, + "placement": { + "hosted_residual_roles": 124992, + "occurrences_per_replica": 3906, + "selection_patterns": [ + [ + 0, + [ + 8 + ], + 222 + ], + [ + 1, + [], + 222 + ], + [ + 2, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 3, + [], + 222 + ], + [ + 4, + [ + 8, + 8, + 8, + 8, + 8 + ], + 222 + ], + [ + 5, + [], + 222 + ], + [ + 6, + [], + 18 + ], + [ + 6, + [ + 8, + 8, + 8, + 8, + 8 + ], + 204 + ], + [ + 7, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 8, + [ + 8 + ], + 222 + ] + ], + "slot_list_sha256": "a8164d30227109a3f6063566fbd8b7b5f46adbd32001080863adc75143803fa6", + "split": "18x(42,5) with split {\"6\": [[5, 18]]}" + }, + "runner_up": "17x(42,5) + 1x(14,1) + 1x(42,4)", + "slack_units_per_replica": 90, + "third": "17x(42,5) + 1x(28,1) + 1x(42,4)", + "windows": { + "note": "every split of each (capacity, u) count over the two children of that capacity class; seed72 maxflow_assign and the all-subsets Hall test agree on each", + "splits_checked": 19, + "splits_feasible": 19 + } + }, + { + "R": 433, + "d": 6, + "exhaustive_layouts_covered": 728466365, + "layouts_total": 728466365, + "models": { + "rank1": { + "dp_certificate": { + "c_star": "0.001749260420895977867719", + "exhaustive_layouts_covered": 728466365, + "optimum": "19x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 424, + "34": 1, + "4": 444, + "42": 19, + "6": 444, + "7": 666 + }, + "runner_up": "19x(42,5) + 1x(14,1) + 1x(28,3)", + "runner_up_gap_moment": [ + "0.0000001402003284490452916850187696988371", + "0.0000001402003284490452916850187696988372" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007967865066416142017042986719524314", + "0.007967865066416142017042986719524315" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 425, + "28": 1, + "4": 443, + "42": 19, + "6": 443, + "7": 666 + }, + "slack_units": 99, + "third": "19x(42,5) + 1x(28,1) + 1x(28,3)" + }, + "endpoint": "0.001749260420895977867718", + "endpoint_fraction": "874630210447988933859/500000000000000000000000", + "gain_vs_pr589_percent": "0.91341492", + "hosted_children": 891072, + "hosted_profile": { + "1": 367200, + "2": 400064, + "3": 22752, + "34": 32, + "4": 26880, + "42": 608, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "local_profile": { + "1": 1275, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "local_rank_mass": 5081, + "step_vs_previous_d_percent": "0.15067488" + }, + "rank7": { + "dp_certificate": { + "c_star": "0.001742258732839957487272", + "exhaustive_layouts_covered": 728466365, + "optimum": "19x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 424, + "34": 1, + "4": 444, + "42": 19, + "6": 444, + "7": 666 + }, + "runner_up": "19x(42,5) + 1x(14,1) + 1x(28,3)", + "runner_up_gap_moment": [ + "0.0000001396394235743489796959301269066035", + "0.0000001396394235743489796959301269066036" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007935987720577401214079100972356092", + "0.007935987720577401214079100972356093" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 425, + "28": 1, + "4": 443, + "42": 19, + "6": 443, + "7": 666 + }, + "slack_units": 99, + "third": "19x(42,5) + 1x(28,1) + 1x(28,3)" + }, + "endpoint": "0.001742258732839957487271", + "endpoint_fraction": "1742258732839957487271/1000000000000000000000000", + "gain_vs_pr589_percent": "0.50949322", + "hosted_children": 901440, + "hosted_profile": { + "1": 379296, + "2": 400064, + "3": 22752, + "34": 32, + "4": 26880, + "42": 608, + "5": 29376, + "6": 17376, + "7": 25056 + }, + "local_profile": { + "1": 1317, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 13 + }, + "local_rank_mass": 5081, + "step_vs_previous_d_percent": "0.08257462" + }, + "template": { + "dp_certificate": { + "c_star": "0.001741991196114600260001", + "exhaustive_layouts_covered": 728466365, + "optimum": "19x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 424, + "34": 1, + "4": 444, + "42": 19, + "6": 444, + "7": 666 + }, + "runner_up": "19x(42,5) + 1x(14,1) + 1x(28,3)", + "runner_up_gap_moment": [ + "0.0000001396179911777525632362868024171784", + "0.0000001396179911777525632362868024171785" + ], + "runner_up_gap_sum_g_per_replica": [ + "0.007934769674614033673844651554973085", + "0.007934769674614033673844651554973086" + ], + "runner_up_idle_per_replica": { + "14": 1, + "2": 425, + "28": 1, + "4": 443, + "42": 19, + "6": 443, + "7": 666 + }, + "slack_units": 99, + "third": "19x(42,5) + 1x(28,1) + 1x(28,3)" + }, + "endpoint": "0.001741991196114600260000", + "endpoint_fraction": "87099559805730013/50000000000000000000", + "gain_vs_pr589_percent": "0.49405924", + "hosted_children": 901440, + "hosted_profile": { + "1": 377568, + "2": 403520, + "3": 21024, + "34": 32, + "4": 26880, + "42": 608, + "5": 29376, + "6": 17376, + "7": 25056 + }, + "local_profile": { + "1": 1311, + "2": 1354, + "3": 73, + "4": 44, + "5": 102, + "6": 11, + "7": 13 + }, + "local_rank_mass": 5081, + "step_vs_previous_d_percent": "0.07998149" + } + }, + "optimum": "19x(42,5) + 1x(42,4)", + "optimum_idle_per_replica": { + "2": 424, + "34": 1, + "4": 444, + "42": 19, + "6": 444, + "7": 666 + }, + "placement": { + "hosted_residual_roles": 124704, + "occurrences_per_replica": 3897, + "selection_patterns": [ + [ + 0, + [ + 8 + ], + 222 + ], + [ + 1, + [], + 222 + ], + [ + 2, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 3, + [], + 222 + ], + [ + 4, + [ + 8, + 8, + 8, + 8, + 8 + ], + 222 + ], + [ + 5, + [], + 222 + ], + [ + 6, + [], + 19 + ], + [ + 6, + [ + 8 + ], + 1 + ], + [ + 6, + [ + 8, + 8, + 8, + 8, + 8 + ], + 202 + ], + [ + 7, + [ + 8, + 8, + 8 + ], + 222 + ], + [ + 8, + [ + 8 + ], + 222 + ] + ], + "slot_list_sha256": "a5d15555512776fc9ed54769e46c92adf875400508cb43275cdd15165ee56b7e", + "split": "19x(42,5) + 1x(42,4) with split {\"6\": [[4, 1], [5, 19]]}" + }, + "runner_up": "19x(42,5) + 1x(14,1) + 1x(28,3)", + "slack_units_per_replica": 99, + "third": "19x(42,5) + 1x(28,1) + 1x(28,3)", + "windows": { + "note": "every split of each (capacity, u) count over the two children of that capacity class; seed72 maxflow_assign and the all-subsets Hall test agree on each", + "splits_checked": 40, + "splits_feasible": 40 + } + } + ], + "negative_controls": [ + { + "name": "vendored_tampered:vendor/pr2423/verify_rehost.py", + "reason": "Fail: sha256 pin: vendor/pr2423/verify_rehost.py", + "rejected": true + }, + { + "name": "vendored_tampered:vendor/pr2423/vendor/pr1043/CERTIFICATE.json", + "reason": "Fail: sha256 pin: vendor/pr2423/vendor/pr1043/CERTIFICATE.json", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d0/template", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d0/template", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d0/rank1", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d0/rank1", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d0/rank7", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d0/rank7", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "wrong_slack_46_priced/d0", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_46_windows/d0", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "wrong_slack_44_priced/d0", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_44_windows/d0", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "supply_R_plus_1_into_optimum/d0", + "reason": "Fail: infeasible: R+1 helpers per stage do not fit", + "rejected": true + }, + { + "name": "dp_with_move_42_5_dropped_vs_exhaustive/d0", + "reason": "Fail: exhaustive enumeration disagrees with the DP (values)", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d1/template", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d1/template", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d1/rank1", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d1/rank1", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d1/rank7", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d1/rank7", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "wrong_slack_55_priced/d1", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_55_windows/d1", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "wrong_slack_53_priced/d1", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_53_windows/d1", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "supply_R_plus_1_into_optimum/d1", + "reason": "Fail: infeasible: R+1 helpers per stage do not fit", + "rejected": true + }, + { + "name": "dp_with_move_42_4_dropped_vs_exhaustive/d1", + "reason": "Fail: exhaustive enumeration disagrees with the DP (values)", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d2/template", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d2/template", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d2/rank1", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d2/rank1", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d2/rank7", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d2/rank7", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "wrong_slack_64_priced/d2", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_64_windows/d2", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "wrong_slack_62_priced/d2", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_62_windows/d2", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "supply_R_plus_1_into_optimum/d2", + "reason": "Fail: infeasible: R+1 helpers per stage do not fit", + "rejected": true + }, + { + "name": "dp_with_move_28_3_dropped_vs_exhaustive/d2", + "reason": "Fail: exhaustive enumeration disagrees with the DP (values)", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d3/template", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d3/template", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d3/rank1", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d3/rank1", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d3/rank7", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d3/rank7", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "wrong_slack_73_priced/d3", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_73_windows/d3", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "wrong_slack_71_priced/d3", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_71_windows/d3", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "supply_R_plus_1_into_optimum/d3", + "reason": "Fail: infeasible: R+1 helpers per stage do not fit", + "rejected": true + }, + { + "name": "dp_with_move_28_2_dropped_vs_exhaustive/d3", + "reason": "Fail: exhaustive enumeration disagrees with the DP (values)", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d4/template", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d4/template", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d4/rank1", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d4/rank1", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d4/rank7", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d4/rank7", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "wrong_slack_82_priced/d4", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_82_windows/d4", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "wrong_slack_80_priced/d4", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_80_windows/d4", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "supply_R_plus_1_into_optimum/d4", + "reason": "Fail: infeasible: R+1 helpers per stage do not fit", + "rejected": true + }, + { + "name": "dp_with_move_14_1_dropped_vs_exhaustive/d4", + "reason": "Fail: exhaustive enumeration disagrees with the DP (values)", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d5/template", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d5/template", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d5/rank1", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d5/rank1", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d5/rank7", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d5/rank7", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "wrong_slack_91_priced/d5", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_91_windows/d5", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "wrong_slack_89_priced/d5", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_89_windows/d5", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "supply_R_plus_1_into_optimum/d5", + "reason": "Fail: infeasible: R+1 helpers per stage do not fit", + "rejected": true + }, + { + "name": "dp_with_move_42_5_dropped_vs_exhaustive/d5", + "reason": "Fail: exhaustive enumeration disagrees with the DP (values)", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d6/template", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d6/template", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d6/rank1", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d6/rank1", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "runner_up_claimed_optimal/d6/rank7", + "reason": "Fail: claimed optimum not certified", + "rejected": true + }, + { + "name": "endpoint_plus_1e-24_accepted/d6/rank7", + "reason": "Fail: moment at c + 1e-24 is not below one", + "rejected": true + }, + { + "name": "wrong_slack_100_priced/d6", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_100_windows/d6", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "wrong_slack_98_priced/d6", + "reason": "Fail: hosted rank mass (wrong slack)", + "rejected": true + }, + { + "name": "wrong_slack_98_windows/d6", + "reason": "Fail: window demand total = 9R", + "rejected": true + }, + { + "name": "supply_R_plus_1_into_optimum/d6", + "reason": "Fail: infeasible: R+1 helpers per stage do not fit", + "rejected": true + }, + { + "name": "dp_with_move_42_4_dropped_vs_exhaustive/d6", + "reason": "Fail: exhaustive enumeration disagrees with the DP (values)", + "rejected": true + }, + { + "name": "local_model_mass_minus_7", + "reason": "Fail: local rank mass = R439 mass - 8d", + "rejected": true + }, + { + "name": "local_model_negative_counts", + "reason": "Fail: local profile counts nonnegative", + "rejected": true + } + ], + "pr2423_replay": { + "c_a": "0.001734802047828389852783", + "c_b": "0.001734846264120199151475", + "c_pr1043_inplace": "0.001734176288479865766692", + "negative_controls": 29, + "placement_slot_list_sha256": "1ef76bb87f1cfac7b4281c308bd71064c1fb1b6b4b267cfe9f3290212a5de11e", + "status": "PASS_R438_WINDOW_REHOST" + }, + "scope": "bit headroom only; no new kappa (the selected record is complex-bound); rows d >= 1 price hypothetical words with d fewer width-8 helpers under a declared local-profile model; d = 1 TEMPLATE is PR1043 (open, not admitted) with PR2423 re-hosting; d >= 2 needs changed words (PR1250: helper 470 is the only removable helper of the fixed word)", + "status": "PASS_BIT_DELETION_LADDER" +} diff --git a/research/bit-deletion-ladder/SOURCES.json b/research/bit-deletion-ladder/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/bit-deletion-ladder/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/bit-deletion-ladder/TASK.json b/research/bit-deletion-ladder/TASK.json new file mode 100644 index 0000000000..a7e671f1fd --- /dev/null +++ b/research/bit-deletion-ladder/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "selected-packing", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "selected-packing", + "question": "Is there a genuinely unsearched, explicitly bounded improvement to the selected packing?", + "starting_points": [ + "certificates/selected-result.json", + "research/heterogeneous-owner-assembly/README.md", + "research/complex-local-word-ceiling/README.md" + ], + "methods": [ + "Search a named unclaimed canonical candidate domain with a reproducible partition.", + "Prove a stronger scoped relaxation or exact optimum for one named residual subproblem." + ], + "acceptance_gate": "Check live PR overlap first, price both suppliers and distinguish a search best from an optimum. Report the word's packing cap from ceiling.ceiling() and the fraction of it realized; label packing gains as such.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Locate the selected packing source in the review and check live PRs for the same residual problem.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Define an unclaimed canonical domain and a favorable bound before starting a new search.", + "bottleneck_link": "An actual paid-profile gain can improve the frontier up to the other supplier cap.", + "allowed_variations": [ + "One bounded residual packing instance or exact relaxation.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Rerunning an existing search with only a different seed as a separate mathematical contribution." + ], + "overlap_terms": [ + "T16", + "owner exchange", + "packing" + ] + }, + "scope_status": "changed", + "actual_scope": "For the bit supplier after PR1043/PR2423: what is each further width-8 helper deletion worth (d = 0..6) under the certified optimal window-respecting re-hosting of the freed slack, for declared per-deletion local-profile models?", + "scope_change_reason": "Drawn on the bit-supplier track (seed 14). The selected bit packing is already slot-optimal (PR1023); the open bounded question is the value of further deletions, which PR2423 left as an open question.", + "bottleneck_link": "Bit headroom only (the complex supplier binds): it tells bit-word searches what a second and later helper deletion would be worth (about +0.08% c each under PR1043's measured delta).", + "budget_minutes": 60, + "stop_rule": "Stop after exact optimal layouts, window feasibility, placements and certified endpoints for d = 0..6 under three declared models, with controls; no word construction.", + "outcome": "completed", + "evidence": "deletion_ladder.py: unique optimal layouts for S = 45..99 (DP plus exhaustive cross-check, up to 728,466,365 layouts), all window splits feasible, audited placements, 21 certified endpoints; TEMPLATE ladder about +0.082% c per deletion (+0.494% at d = 6); controls reproduce PR589, PR1043 and PR2423 endpoints; 88 negative controls; an adversarial verifier independently recomputed all 21 rows.", + "author": "Sagar Thakrar", + "ai_assistance": "Prepared with substantial AI assistance: Claude Code (Anthropic, Claude Opus 5.5) orchestrated an AI builder agent and an adversarial AI verifier (independent recomputation of all rows). No independent human review is claimed.", + "open_questions": [ + { + "question": "Is there a changed bit word with a second removable width-8 helper?", + "why_it_matters": "PR1250 shows helper 470 is the only removable helper on the fixed word; a second deletion would be worth about +0.083% c over d = 1 under the TEMPLATE delta.", + "first_step": "Search source-substitution moves on PR1043's R438 word for a helper whose last read can be served by a retired source.", + "blocked_by": "Requires a changed word and its legality/replay checks." + }, + { + "question": "What is the true worst-case local delta per deletion over the word's legal local moves?", + "why_it_matters": "It would replace the three declared models by a certified lower envelope.", + "first_step": "Bound the local delta of removing a width-8 helper by the minimal concave-cost change of its own climb shape.", + "blocked_by": "Depends on how removal re-solves other registers' frames." + } + ] +} diff --git a/research/bit-deletion-ladder/VERIFY.json b/research/bit-deletion-ladder/VERIFY.json new file mode 100644 index 0000000000..37968892a1 --- /dev/null +++ b/research/bit-deletion-ladder/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/deletion_ladder.py", + "--check", + "{package}/RECEIPT.json" + ], + "timeout_seconds": 300, + "checks": "Exact optimal slot layouts for S = 45..99 (DP plus exhaustive cross-check), window feasibility (max-flow plus Hall), audited placements, certified endpoints for 21 rows; controls reproduce PR589, PR1043 and PR2423 endpoints; 88 negative controls; receipt byte-identical. Expect PASS_BIT_DELETION_LADDER." + } + ] +} diff --git a/research/bit-deletion-ladder/deletion_ladder.py b/research/bit-deletion-ladder/deletion_ladder.py new file mode 100644 index 0000000000..c384162627 --- /dev/null +++ b/research/bit-deletion-ladder/deletion_ladder.py @@ -0,0 +1,471 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Bit-supplier helper-deletion ladder: what d = 0..6 deleted width-8 helpers would be worth (bit headroom only). + +PR589's bit word has R = 439 width-8 helpers; PR1043 deletes helper 470 (R = 438). PR1250 / seed11 found that 470 is +the only removable helper of the fixed word, so every further deletion needs a changed word. This script prices +what such deletions would be worth under the PR1023 slot model, assuming nothing about the changed words except a +declared per-deletion local-profile model. For d = 0..6 (R = 439 - d, slack S = 3996 - 9R width-8 units per +replica) it computes: + + 1. Layout. The certified unique moment-minimising no-bank slot layout for slack S, its runner-up and the runner-up + gap, with PR2423's exact top-3 interval DP (verify_rehost.certify_optimum), cross-checked for every row by + PR2423's independent branch-and-bound enumerator over all layouts (counts checked against a generating function). + 2. Windows. Every split of the optimum's modified slots over the two children of each capacity class is tested with + seed72's maxflow_assign and PR2423's all-subsets Hall test. For one split an explicit placement of all 9R helper + occurrences per replica is built with seed14's allocate (R overridden on the module instance), compared slot for + slot with PR442's hosting_core.expand, and audited by seed14's placement_audit and PR2423's audit_slots. + 3. Endpoints. The hosted idle profile is combined with three declared local-profile models and certified with + PR1023's packing.endpoint (both pinned engines; accepted at c, rejected at c + 1e-24): + TEMPLATE R439 local + d * {1:-2, 2:+2, 3:-1, 7:-1} (PR1043's measured one-deletion delta, repeated) + RANK1 R439 local + d * {1:-8} (each deletion removes eight rank-1 children; illustrative, + NOT an upper envelope: same-mass deltas can price higher) + RANK7 R439 local + d * {7:-1, 1:-1} (each deletion removes one rank-7 and one rank-1 child; + illustrative; d=1 equals PR2423's transported word) + The DP is re-certified at each row's own c + 1e-24 and must return the priced layout. + 4. Controls. d = 0 reproduces PR589's c; d = 1 TEMPLATE equals PR1043's certified local profile and reproduces + PR2423's 0.001734802047828389852783; PR2423's verify_rehost.main is replayed end to end and must agree; a wrong + slack (S + 1 and S - 1) is rejected by the rank-mass and window-demand checks; further negative controls below. + +No word is constructed here. Rows d >= 2 are prices of hypothetical words; every row d >= 1 is conditional on a word +with that many fewer helpers and the declared local model. The selected record is complex-bound; no kappa is claimed. + +Usage: python3 -I -B deletion_ladder.py [--repo ROOT] [--out RECEIPT.json] [--check RECEIPT.json] +The last line printed is PASS_BIT_DELETION_LADDER ... or FAIL_BIT_DELETION_LADDER ... +Standard-library CPython only. Main-tree inputs are read through PR2423's pins (sha256 + git blob); PR2423's +verify_rehost.py and PR1043's CERTIFICATE.json are vendored byte copies pinned here (vendor/NOTICE.md). +""" +import argparse +import hashlib +import itertools +import json +import os +import sys +import time +import types +from collections import Counter +from fractions import Fraction as Q + +TAG = 'BIT_DELETION_LADDER' +HERE = os.path.dirname(os.path.abspath(__file__)) +DEFAULT_REPO = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +VENDOR = { + 'vendor/pr2423/verify_rehost.py': dict( + sha256='4774841de10a8386204519174c5e56eb14f5852b20058db38a65a1034eeba275', + git_blob='58c76b9d7b6ed12e4473a4b38b5193f867b2d674', + origin='PR2423 (Sagar Thakrar, @thakrarsagar) head 13cd273dc13c98244b1f9bcf588b6e828cbc0347, ' + 'research/bit-r438-transport-rehost/verify_rehost.py'), + 'vendor/pr2423/vendor/pr1043/CERTIFICATE.json': dict( + sha256='32c6cd6103006d627909cabdaf5083238c661a6582016a8b21075bd01c892eff', + git_blob='56400920050c523e6e399f2455137b36c35cf528', + origin='PR1043 (Ali Romman, @aliromman) head e309e17f83f5759b1ea1fa24a76f24838784cb4d, ' + 'research/bit-boundary-persistence/CERTIFICATE.json (via PR2423 vendor/pr1043/)'), +} + +DMAX = 6 +MODELS = (('template', {1: -2, 2: 2, 3: -1, 7: -1}), + ('rank1', {1: -8}), + ('rank7', {7: -1, 1: -1})) +PR2423_R438_OPT = '0.001734802047828389852783' # PR2423 R438 optimal re-hosting, PR1043 local profile + + +class Fail(Exception): + pass + + +def require(ok, message): + if not ok: + raise Fail(message) + + +def git_blob(raw): + return hashlib.sha1(b'blob %d\0' % len(raw) + raw).hexdigest() + + +def load_vendored(rel): + path = os.path.join(HERE, *rel.split('/')) + with open(path, 'rb') as handle: + raw = handle.read() + pin = VENDOR[rel] + require(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'sha256 pin: ' + rel) + require(git_blob(raw) == pin['git_blob'], 'git blob pin: ' + rel) + return path, raw + + +def exec_module(name, path, raw): + module = types.ModuleType(name) + module.__file__ = path + sys.modules[name] = module + exec(compile(raw, path, 'exec'), module.__dict__) + return module + + +def layout_count(S, umaxes): + """Number of no-bank layouts with S unused width-8 units: coefficient of x^S in prod_class prod_{u<=umax} 1/(1-x^u) + (one multiset of unused counts per capacity class). Independent of the enumerator.""" + poly = [1] + [0] * S + for umax in umaxes: + for u in range(1, umax + 1): + for s in range(u, S + 1): + poly[s] += poly[s - u] + return poly[S] + + +def main(args): + t0 = time.time() + repo = os.path.abspath(args.repo) + controls = [] + vr_path, vr_raw = load_vendored('vendor/pr2423/verify_rehost.py') + _, cert_raw = load_vendored('vendor/pr2423/vendor/pr1043/CERTIFICATE.json') + VR = exec_module('ladder_pr2423_verify_rehost', vr_path, vr_raw) + # PR2423's own pin of the PR1043 certificate must be the one used here. + require(VR.VENDOR['vendor/pr1043/CERTIFICATE.json']['sha256'] == VENDOR['vendor/pr2423/vendor/pr1043/' + 'CERTIFICATE.json']['sha256'], 'cert pin') + for rel in VENDOR: + path = os.path.join(HERE, *rel.split('/')) + with open(path, 'rb') as handle: + good = handle.read() + bad = good[:-2] + bytes([good[-2] ^ 1]) + good[-1:] + VR.expect_reject(controls, 'vendored_tampered:' + rel, + lambda bad=bad, rel=rel: VR.check_pin(bad, VENDOR[rel]['sha256'], VENDOR[rel]['git_blob'], rel), + 'sha256 pin') + raw = {rel: VR.read_pinned(repo, rel, sha, blob) for rel, (sha, blob) in VR.PINS.items()} + P = VR.load_module('ladder_packing', *raw['research/bit589-width-packing/packing.py']) + S72 = VR.load_module('ladder_seed72_verify', *raw['research/bit589-width7-windows-seed72/verify.py']) + S14 = VR.load_module('ladder_seed14_verify', *raw['research/bit-helper470-window-placement-seed14/verify.py']) + HC = VR.load_module('ladder_pr442_hosting_core', *raw['research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/' + 'vendor/idle-axis-hosting/hosting_core.py']) + T, STAGES, M, V, COPIES, GRID = VR.T, VR.STAGES, VR.M, VR.V, VR.COPIES, VR.GRID + gd = VR.grid_decimal + out = dict(status='PASS_' + TAG, + scope='bit headroom only; no new kappa (the selected record is complex-bound); rows d >= 1 price ' + 'hypothetical words with d fewer width-8 helpers under a declared local-profile model; d = 1 ' + 'TEMPLATE is PR1043 (open, not admitted) with PR2423 re-hosting; d >= 2 needs changed words ' + '(PR1250: helper 470 is the only removable helper of the fixed word)', + inputs=dict(main_tree={rel: dict(sha256=s, git_blob=b) for rel, (s, b) in sorted(VR.PINS.items())}, + vendored={rel: dict(sha256=p['sha256'], git_blob=p['git_blob'], origin=p['origin']) + for rel, p in sorted(VENDOR.items())})) + + # -- 0. Baseline binding (PR589 record, PR1023 slot model, PR1043 certificate, windows). -------------------------- + record = P.pinned_json('bit_record') + selection = P.pinned_json('selection') + model = P.slot_model(record, selection) + W = record['nine']['bit']['live'] + require((model['R'], model['v'], W, model['calls']) == (439, V, 28416, STAGES * T), 'PR589 record dimensions') + c0 = Q(record['nine']['bit_lower']) + require(gd(c0) == VR.C0_DECIMAL, 'PR589 bit endpoint') + local439 = Counter(model['local']) + mass439, kids439 = sum(r * n for r, n in local439.items()), sum(local439.values()) + require((mass439, kids439) == (8 * 439 + 63 + 14 * V, 2920), 'R439 local mass and child count') + cert = json.loads(cert_raw) + require(VR.unkeyed(cert['local']['baseline']['profile']) == dict(local439), 'PR1043 baseline local = PR589') + local1043 = Counter(VR.unkeyed(cert['local']['candidate']['profile'])) + require(cert['local']['candidate']['helpers'] == 438, 'PR1043 candidate is R438') + + WIN72 = S72.WIN + win14 = S14.windows(S14.schedule()) + require(set(WIN72) == {i for i, (p, r, st) in win14.items() if r and st}, 'hosting children agree') + require(all(win14[i][1:] == (WIN72[i][0], tuple(WIN72[i][1])) for i in WIN72), 'seed72 and seed14 windows agree') + require({i: c for i, (c, st) in WIN72.items()} == model['caps'], 'window capacities = PR1023 slot capacities') + hosting = {i: (win14[i][0], WIN72[i][0], tuple(WIN72[i][1])) for i in sorted(WIN72)} + active = {e['stage']: e['pair'] for e in S72.wopt.windows.schedule() if e['kind'] == 'local_cover_sweep'} + require(sorted(active) == list(range(STAGES)), 'one local sweep per stage') + slots = Counter() + for i, (c, st) in WIN72.items(): + slots[c] += COPIES + require(slots == model['slots'] == Counter({7: 666, 14: 444, 28: 444, 42: 444}), 'slots per replica') + units = sum((c // 8) * n for c, n in slots.items()) + require(units == 3996, 'width-8 capacity per replica') + cap_mass = sum(c * n for c, n in slots.items()) + pairs = {} + for i, (pair, cap, st) in hosting.items(): + if cap // 8: + pairs.setdefault(cap, []).append(i) + require({cap: len(ch) for cap, ch in pairs.items()} == {14: 2, 28: 2, 42: 2}, 'two children per capacity class') + umaxes = sorted(cap // 8 for cap in pairs) + for S_, n in VR.EXPECTED_LAYOUTS.items(): + require(layout_count(S_, umaxes) == n, 'generating-function layout count = PR2423 at S=%d' % S_) + HOSTED_MASS = 9 * T * mass439 + T * (cap_mass - 72 * 439) + require(HOSTED_MASS == 1808352, 'hosted rank mass invariant') + + # -- helpers ----------------------------------------------------------------------------------------------------- + def local_model(delta, d): + loc = Counter(local439) + for r, n in delta.items(): + loc[r] += d * n + require(all(n >= 0 for n in loc.values()), 'local profile counts nonnegative') + require(sum(r * n for r, n in loc.items()) == mass439 - 8 * d, 'local rank mass = R439 mass - 8d') + return +loc + + def price(local, idle, label): + H = Counter({r: n * STAGES * T for r, n in local.items()}) + for r, n in idle.items(): + H[r] += n * T + require(all(n > 0 for n in H.values()), 'positive profile entries (%s)' % label) + require(sum(idle.values()) == sum(slots.values()), 'one idle child per slot (%s)' % label) + require(sum(r * n for r, n in H.items()) == HOSTED_MASS, 'hosted rank mass (%s)' % label) + require(M * M > 2 * max(H) ** 2, 'halving guard (%s)' % label) + H = dict(sorted(H.items())) + return P.endpoint(H, W), H + + def splits(layout): + items = sorted(layout) + for combo in itertools.product(*[range(k + 1) for _, k in items]): + assign = {} + for ((cap, u), k), ka in zip(items, combo): + a, b = pairs[cap] + for child, n in ((a, ka), (b, k - ka)): + if n: + assign.setdefault(child, []).append((u, n)) + yield combo, assign + + def demand_of(assign): + dem = {} + for i, (pair, cap, st) in hosting.items(): + dem[i] = (cap // 8) * COPIES - sum(u * n for u, n in assign.get(i, ())) + require(sum(n for _, n in assign.get(i, ())) <= COPIES, 'modified copies within a child') + return dem + + def windows_check(layout, R): + supply = {s: R for s in range(STAGES)} + allowed = {i: set(st) for i, (p, c, st) in hosting.items()} + n_cfg, feasible, first = 0, 0, None + for combo, assign in splits(layout): + dem = demand_of(assign) + require(sum(dem.values()) == STAGES * R, 'window demand total = 9R') + x = S72.maxflow_assign(supply, dem, allowed) + ok, _ = VR.hall_check(supply, dem, allowed) + require((x is not None) == ok, 'max-flow and Hall disagree at %s' % (combo,)) + n_cfg += 1 + if x is not None: + require(all(s in allowed[i] and n > 0 for (s, i), n in x.items()), 'flow inside windows') + require(all(sum(n for (s, i), n in x.items() if i == j) == dem[j] for j in dem), 'flow meets demand') + require(all(sum(n for (s, i), n in x.items() if s == t) == R for t in range(STAGES)), 'flow = supply') + feasible += 1 + if first is None: + first = (combo, assign, x) + return n_cfg, feasible, first + + def placement(assign, x, R, idle_expected): + pats = [] + for i, (pair, cap, st) in sorted(hosting.items()): + f = cap // 8 + mods = Counter() + for u, n in assign.get(i, ()): + mods[f - u] += n + full = COPIES - sum(mods.values()) + if f == 0: + pats.append([i, [], COPIES]) + continue + for h in sorted(mods): + pats.append([i, [8] * h, mods[h]]) + if full: + pats.append([i, [8] * f, full]) + sel = dict(patterns=pats, stages=sorted([i, 8, s, n] for (s, i), n in x.items())) + require(S14.R == 439, 'seed14 R constant') + S14.R = R + try: + alloc = S14.allocate(sel) + rem, _ = S14.placement_audit(alloc, win14, frozenset()) + owners = S14.owners_for_replicas(alloc, win14) + finally: + S14.R = 439 + require(len(alloc) == STAGES * R, 'occurrences per replica') + win_hc = {i: (p, c, frozenset(st)) for i, (p, c, st) in hosting.items()} + ys = {(i, tuple(pat)): n for i, pat, n in pats} + zs = {(i, w, s): n for i, w, s, n in sel['stages']} + slots_hc, rem_hc = HC.expand(win_hc, ys, zs, {s: [(h, 8) for h in range(R)] for s in range(STAGES)}, COPIES) + require(slots_hc == alloc, 'seed14 allocate = PR442 expand (slot for slot)') + idle_s14 = Counter(r for r in rem.values() if r) + idle_hc = Counter(r for r in rem_hc.values() if r) + idle_ind = VR.audit_slots(alloc, hosting, active, R) + require(idle_s14 == idle_hc == idle_ind == idle_expected, 'placement remainders = DP optimum') + seen = set() + for stage, rep, h, fam, child, off, w in owners: + r_, rest = divmod(fam, 8 * V) + pair2, port = divmod(rest, V) + require(r_ == rep and pair2 // 2 == hosting[child][0] != active[stage], 'owner family pair') + require((stage, rep, h) not in seen, 'owner once') + seen.add((stage, rep, h)) + require(len(seen) == STAGES * T * R, 'all hosted residual roles') + canon = json.dumps([list(t) for t in alloc], separators=(',', ':')).encode() + return dict(selection_patterns=pats, occurrences_per_replica=len(alloc), hosted_residual_roles=len(seen), + slot_list_sha256=hashlib.sha256(canon).hexdigest()) + + def certify_row(local, S, exhaustive, label): + """Candidate from the DP at c0 + 1e-24, priced; the DP is re-certified at the row's own c + 1e-24 and must + return the priced layout (fixed point; at most four rounds).""" + c_try = c0 + for _ in range(4): + cand = VR.certify_optimum(P, slots, S, c_try + GRID, W, check_exhaustive=False) + c, H = price(local, cand['idle_opt'], label) + cs = VR.certify_optimum(P, slots, S, c + GRID, W, check_exhaustive=exhaustive) + if cs['idle_opt'] == cand['idle_opt']: + return c, H, cs + c_try = c + raise Fail('DP optimum did not reach a fixed point (%s)' % label) + + # -- 1-3. The ladder. -------------------------------------------------------------------------------------------- + ladder, table = [], [] + layout_cache = {} + for d in range(DMAX + 1): + R = 439 - d + S = units - STAGES * R + require(S == 45 + 9 * d, 'slack') + expected = layout_count(S, umaxes) + row = dict(d=d, R=R, slack_units_per_replica=S, layouts_total=expected, models={}) + lays = {} + for name, delta in MODELS: + local = local_model(delta, d) + require(sum(local.values()) == kids439 + d * sum(delta.values()), 'local child count') + c, H, cs = certify_row(local, S, True, '%s d=%d' % (name, d)) + require(cs['covered'] == expected, 'exhaustive enumeration covered every layout (d=%d %s)' % (d, name)) + require(VR.claim_is_optimal(cs, cs['opt']), 'optimum certifies') + VR.expect_reject(controls, 'runner_up_claimed_optimal/d%d/%s' % (d, name), + lambda cs=cs: require(VR.claim_is_optimal(cs, cs['run']), 'claimed optimum not certified'), + 'claimed optimum not certified') + + def accept_next(H=H, c=c): + lo, hi = P.MOMENT.moment(H, M, W, c + GRID, True) + require(hi < 1, 'moment at c + 1e-24 is not below one') + VR.expect_reject(controls, 'endpoint_plus_1e-24_accepted/d%d/%s' % (d, name), accept_next, 'not below one') + lays[name] = cs + row['models'][name] = dict(local_profile=VR.keyed(local), local_rank_mass=sum(r * n for r, n in local.items()), + endpoint=gd(c), endpoint_fraction=str(c), + gain_vs_pr589_percent=VR.dfloor(100 * (c - c0) / c0, 8), + hosted_profile=VR.keyed(H), hosted_children=sum(H.values()), + dp_certificate=cs['receipt']) + row['models'][name]['_c'] = c + layouts = {cs['opt'] for cs in lays.values()} + require(len(layouts) == 1, 'all three models select the same layout at d=%d' % d) + cs = lays['template'] + opt, idle_opt = cs['opt'], cs['idle_opt'] + require(all(x['idle_opt'] == idle_opt for x in lays.values()), 'same idle profile') + if opt not in layout_cache: + n_cfg, n_ok, first = windows_check(opt, R) + plc = placement(first[1], first[2], R, idle_opt) if first is not None else None + layout_cache[opt] = (n_cfg, n_ok, first, plc) + n_cfg, n_ok, first, plc = layout_cache[opt] + row.update(optimum=VR.layout_name(opt), optimum_idle_per_replica=VR.keyed(idle_opt), + runner_up=VR.layout_name(cs['run']), third=VR.layout_name(cs['third']), + exhaustive_layouts_covered=cs['covered'], + windows=dict(splits_checked=n_cfg, splits_feasible=n_ok, + note='every split of each (capacity, u) count over the two children of that capacity ' + 'class; seed72 maxflow_assign and the all-subsets Hall test agree on each'), + placement=None if plc is None else dict(plc, split=VR.layout_name(opt) + ' with split ' + + json.dumps({str(k): v for k, v in sorted(first[1].items())}))) + # Wrong slack controls: the S+1 and S-1 optima must be rejected by the rank-mass and window-demand checks. + for wrong in (S + 1, S - 1): + bad = VR.certify_optimum(P, slots, wrong, c0 + GRID, W, check_exhaustive=False) + VR.expect_reject(controls, 'wrong_slack_%d_priced/d%d' % (wrong, d), + lambda bad=bad: price(local_model(MODELS[0][1], d), bad['idle_opt'], 'wrong slack'), + 'hosted rank mass') + VR.expect_reject(controls, 'wrong_slack_%d_windows/d%d' % (wrong, d), + lambda bad=bad: windows_check(bad['opt'], R), 'window demand total') + # Supply of R+1 helpers per stage into the R optimum must not fit. + if first is not None: + VR.expect_reject(controls, 'supply_R_plus_1_into_optimum/d%d' % d, + lambda: require(S72.maxflow_assign({s: R + 1 for s in range(STAGES)}, + demand_of(first[1]), + {i: set(st) for i, (p, c, st) in hosting.items()}) + is not None, 'infeasible: R+1 helpers per stage do not fit'), 'do not fit') + # DP with the optimum's rarest move dropped must disagree with the exhaustive enumerator. + drop = min(opt, key=lambda t: (t[1], t[0]))[0] + VR.expect_reject(controls, 'dp_with_move_%d_%d_dropped_vs_exhaustive/d%d' % (drop + (d,)), + lambda drop=drop: VR.certify_optimum(P, slots, S, row['models']['template']['_c'] + GRID, W, + check_exhaustive=True, dp_drop=(drop,)), + 'exhaustive enumeration disagrees with the DP') + ladder.append(row) + print(' d=%d R=%d S=%d %s splits %d/%d (%.0f s)' % (d, R, S, VR.layout_name(opt), n_ok, n_cfg, + time.time() - t0), flush=True) + + # -- 4. Controls on the ladder. ---------------------------------------------------------------------------------- + cs0 = {n: ladder[0]['models'][n]['_c'] for n, _ in MODELS} + require(all(c == c0 for c in cs0.values()), 'd=0 reproduces the PR589 endpoint in every model') + require(ladder[0]['optimum'] == '9x(42,5)' and + VR.unkeyed(ladder[0]['optimum_idle_per_replica']) == dict(model['idle_rep']), 'd=0 layout = PR589 selection') + require(local_model(MODELS[0][1], 1) == local1043, 'd=1 TEMPLATE local = PR1043 certified local profile') + c1t = ladder[1]['models']['template']['_c'] + require(gd(c1t) == PR2423_R438_OPT == VR.SCOUT_A, 'd=1 TEMPLATE reproduces PR2423 R438 optimal re-hosting') + require(ladder[1]['optimum'] == '10x(42,5) + 1x(42,4)', 'd=1 layout = PR2423 optimum') + # d = 1 RANK7 coincides with PR2423's transported-word profile (b); its endpoint must be PR2423's c_b. + require(local_model(MODELS[2][1], 1) == Counter(VR.LOCAL_B), 'd=1 RANK7 local = PR2423 transported profile (b)') + c1w = ladder[1]['models']['rank7']['_c'] + require(gd(c1w) == VR.SCOUT_B, 'd=1 RANK7 reproduces PR2423 c_b') + VR.expect_reject(controls, 'local_model_mass_minus_7', lambda: local_model({1: -7}, 1), 'local rank mass') + VR.expect_reject(controls, 'local_model_negative_counts', lambda: local_model({7: -4, 1: 20}, 6), + 'nonnegative') + # End-to-end replay of PR2423's verify_rehost.main (vendored, pinned) must agree with the d = 1 row. + vr_out, _, ca, cb, c1043 = VR.main(types.SimpleNamespace(repo=repo)) + require(ca == c1t and cb == c1w, 'PR2423 verify_rehost c_a, c_b = ladder d=1 TEMPLATE, RANK7') + require(gd(c1043) == VR.PR1043_DECIMAL, 'PR2423 replay: PR1043 in-place endpoint') + require(vr_out['dp']['S54_at_c_a_next'] == ladder[1]['models']['template']['dp_certificate'], + 'PR2423 S=54 DP certificate = ladder d=1 TEMPLATE certificate') + require(vr_out['placement']['slot_list_sha256'] == ladder[1]['placement']['slot_list_sha256'], + 'PR2423 placement = ladder d=1 placement (slot list sha256)') + out['pr2423_replay'] = dict(status=vr_out['status'], c_a=gd(ca), c_b=gd(cb), c_pr1043_inplace=gd(c1043), + negative_controls=len(vr_out['negative_controls']), + placement_slot_list_sha256=vr_out['placement']['slot_list_sha256']) + # Monotone in d within each model; per-step increments. + for name, _ in MODELS: + cs_ = [row['models'][name]['_c'] for row in ladder] + require(all(a < b for a, b in zip(cs_, cs_[1:])), 'endpoint increases with d (%s)' % name) + for d in range(1, DMAX + 1): + ladder[d]['models'][name]['step_vs_previous_d_percent'] = VR.dfloor(100 * (cs_[d] - cs_[d - 1]) / c0, 8) + for row in ladder: + for name, _ in MODELS: + c = row['models'][name].pop('_c') + table.append((row['d'], name, c)) + out['ladder'] = ladder + out['negative_controls'] = controls + out['claims'] = dict(kappa='unchanged; the bit side does not bind', max_d=DMAX, + certificate='per row: moment(opt, c+1e-24) > 1 by both engines; every other no-bank slot ' + 'layout has a certified larger idle sum at c+1e-24 with the same child count and ' + 'local profile; so no layout in the PR1023 slot model reaches c+1e-24 for that ' + 'local model') + return out, time.time() - t0, ladder, table, c0 + + +if __name__ == '__main__': + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--repo', default=DEFAULT_REPO, + help='repository root (default: the parent of the research/ directory holding this script)') + ap.add_argument('--out', help='write the JSON receipt here') + ap.add_argument('--check', help='require the regenerated receipt to equal this file byte for byte') + a = ap.parse_args() + if sys.flags.optimize or not __debug__: + print('FAIL_%s refusing to run under python -O (assert-based checks in pinned modules would be skipped)' % TAG) + sys.exit(2) + try: + receipt, elapsed, ladder, table, c0 = main(a) + text = json.dumps(receipt, indent=1, sort_keys=True) + '\n' + if a.check: + with open(a.check) as handle: + require(handle.read() == text, 'receipt differs from ' + a.check) + if a.out: + with open(a.out, 'w') as handle: + handle.write(text) + except (Exception, SystemExit) as e: # seed72's need() raises SystemExit + print('FAIL_%s %s: %s' % (TAG, type(e).__name__, e)) + sys.exit(1) + print('d R S layout windows c_template c_rank1' + ' c_rank7 %vsPR589 (T/R1/R7)') + for row in ladder: + m = row['models'] + print('%d %d %-3d %-25s %2d/%-2d %s %s %s +%s/+%s/+%s' % ( + row['d'], row['R'], row['slack_units_per_replica'], row['optimum'], + row['windows']['splits_feasible'], row['windows']['splits_checked'], + m['template']['endpoint'], m['rank1']['endpoint'], m['rank7']['endpoint'], + m['template']['gain_vs_pr589_percent'][:7], m['rank1']['gain_vs_pr589_percent'][:7], + m['rank7']['gain_vs_pr589_percent'][:7])) + print('python %s; %.1f s' % (sys.version.split()[0], elapsed)) + top = ladder[-1]['models'] + print('PASS_%s d=0..%d exhaustive=%d/%d windows_feasible=%d/%d c_template(d=%d)=%s c_rank1=%s c_rank7=%s ' + 'controls=%d no_new_kappa' % ( + TAG, len(ladder) - 1, sum(1 for r in ladder for m in r['models'].values() + if m['dp_certificate']['exhaustive_layouts_covered'] == r['layouts_total']), + 3 * len(ladder), + sum(1 for r in ladder if r['windows']['splits_feasible']), len(ladder), ladder[-1]['d'], + top['template']['endpoint'], top['rank1']['endpoint'], top['rank7']['endpoint'], + len(receipt['negative_controls']))) diff --git a/research/bit-deletion-ladder/vendor/NOTICE.md b/research/bit-deletion-ladder/vendor/NOTICE.md new file mode 100644 index 0000000000..50899341df --- /dev/null +++ b/research/bit-deletion-ladder/vendor/NOTICE.md @@ -0,0 +1,17 @@ +# Vendored files + +Byte-for-byte copies; nothing here is modified. The sha256 and git blob ids are pinned in +`../deletion_ladder.py` (`VENDOR`) and checked before any use. + +- `pr2423/verify_rehost.py`: Sagar Thakrar (@thakrarsagar), PR2423 head + `13cd273dc13c98244b1f9bcf588b6e828cbc0347`, `research/bit-r438-transport-rehost/verify_rehost.py`. + Apache-2.0. Prepared with Claude Code assistance. Its DP (`topk_dp`, `certify_optimum`), exhaustive + enumerator (`exhaustive_topk`), Hall test, independent placement audit and `main` are imported, not rewritten. +- `pr2423/vendor/pr1043/`: Ali Romman (@aliromman), PR1043 head `e309e17f83f5759b1ea1fa24a76f24838784cb4d`, + `research/bit-boundary-persistence/CERTIFICATE.json` and its `NOTICE.md`, copied unchanged via PR2423's + `vendor/pr1043/` (where `verify_rehost.main` expects it). Apache-2.0; its notice states substantial OpenAI Codex + assistance. + +Main-tree inputs (PR1023 packing.py and engines, seed72 windows, seed14 placement, PR442 hosting_core, PR589 record +and selection) are read from `--repo` through PR2423's `PINS` (sha256 and git blob at canonical main +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`). diff --git a/research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/CERTIFICATE.json b/research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/CERTIFICATE.json new file mode 100644 index 0000000000..5640092005 --- /dev/null +++ b/research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/CERTIFICATE.json @@ -0,0 +1,2052 @@ +{ + "base_commit": "8bddbee377e2f3ce1f1247196c4b290d55767d20", + "boundary": { + "all_paths_sha256": "a030398460debf9b3da94457f0039d9797f374a7baf375f439edaf035b924847", + "before": { + "444": 0, + "77": 186 + }, + "birth": 230, + "changed_surviving_paths": { + "444": [ + [ + 0, + 79, + 509, + 392, + 513, + 1 + ], + [ + 0, + 186, + 509, + 392, + 513, + 1 + ] + ] + }, + "frames": { + "186": { + "lines": [ + 33, + 77 + ], + "rank": 2 + }, + "509": { + "lines": [ + 17, + 22, + 33, + 38, + 50, + 60, + 67, + 77, + 87, + 92 + ], + "rank": 4 + }, + "79": { + "lines": [ + 77 + ], + "rank": 1 + } + }, + "helper": 470, + "new_frame": 186, + "next_frame": { + "444": 509, + "77": 186 + }, + "read": 1993, + "receiver": 444, + "removed_path": [ + 0, + 79, + 1 + ], + "retained_copy_uses": 0, + "source": 77, + "source_path": [ + 79, + 186, + 509, + 386, + 560, + 1 + ], + "source_unchanged": true + }, + "controls": { + "accepted_paid_neutral_pair": { + "extra_adds": 2, + "same_profile": true + }, + "rejected": [ + { + "name": "source77_changed_before_read", + "rejection": "Source changed before the late read" + }, + { + "name": "another_live_carrier_use", + "rejection": "Carrier has another live use" + }, + { + "name": "late_source_read_in_old_line_frame", + "rejection": "Frame descent" + }, + { + "name": "omitted_literal_restoration", + "rejection": "Wrong arbitrary-dirty endpoint" + }, + { + "name": "omitted_dirty_target_compensation", + "rejection": "Wrong arbitrary-dirty endpoint" + }, + { + "name": "deleted_helper_without_returned_idle_charge", + "rejection": "Wrong hosted rank mass" + } + ] + }, + "hosted": { + "baseline": { + "audit": { + "bank_assignments": 0, + "deficit": 10272, + "emitted_events": 7843392, + "emitted_program_sha256": "96c7ad2e744e9a503a4ef5ecd52d0f6a8899bdb5efac2e3aafa0db18adf99523", + "hosted_residuals": 126432, + "live": 28416, + "maxchild": 42, + "mutations_rejected": [ + "slot outside window", + "copy index outside family", + "negative slot offset", + "wrong residual width", + "duplicate helper", + "omitted helper", + "hosted owner in another replica or outside the data stock", + "hosted owner on a wrong data family", + "wrong call orientation", + "duplicate call", + "changed idle rank", + "understated live stock", + "missing remainder summary", + "stale stage count", + "hosted coordinate beyond the pending set", + "overlapping hosted coordinates" + ], + "physical": 28425, + "profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "42": 288, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "rank_mass": 1808352, + "status": "PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT" + }, + "invoice": { + "R": 439, + "bit": { + "bank_assignments": 0, + "charged_prefix_bits": 192, + "charged_two_level_coefficient_bits": 512, + "coefficient_bits": 177, + "halving_depth": 2, + "hosted_residuals": 126432, + "live": 28416, + "maxchild": 42, + "physical": 28425, + "prefix_bits": 177, + "rank_mass": 1808352, + "row_coefficient": 18355, + "two_level_coefficient_bits": 393 + }, + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "bit_lower_decimal": "0.001733427039589844234749", + "bit_profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "42": 288, + "5": 29376, + "6": 17376, + "7": 26784 + }, + "emitted_program_sha256": "96c7ad2e744e9a503a4ef5ecd52d0f6a8899bdb5efac2e3aafa0db18adf99523", + "next_grid_point_rejected": "6933708158359376939/4000000000000000000000", + "replicas": 32, + "stages": 9, + "status": "PASS_NINE_STAGE_WHOLE_HOSTED_BIT_PRICE_AND_CITED_ASSEMBLY" + }, + "parent": { + "all_scalar_columns_restored": true, + "bridge_additions": 63936, + "copy_erase_episodes": 2592, + "halving_integer_inequality": [ + 4096, + 3528 + ], + "independent_unbanked_scalar_columns": 4839, + "local_checks": { + "forward": { + "adds": 24305, + "all_columns": 661, + "cancellation_free_row_l1": 49347, + "copies": 9, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "records": 27234, + "sha256": "a778a0300bbf4b07908ee24c0d271426ba6c70568e788af2f0ac8517897cb5b4" + }, + "reverse": { + "adds": 24305, + "all_columns": 661, + "cancellation_free_row_l1": 1113070, + "copies": 9, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "records": 27234, + "sha256": "98d97804744d691548b4d54868a8a0e5f500c55ab32ac4be96f3ba30e6f5bef8" + } + }, + "local_invocations": 288, + "omitted_bridge_shears_rejected": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17 + ], + "scalar_stages": [ + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": false, + "stage": 0 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": true, + "stage": 1 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": false, + "stage": 2 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": true, + "stage": 3 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": false, + "stage": 4 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": true, + "stage": 5 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": false, + "stage": 6 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": true, + "stage": 7 + }, + { + "all_columns": 4839, + "helper_columns": 3951, + "reverse": false, + "stage": 8 + } + ] + }, + "parent_controls": [ + "omit an idle child", + "omit a bridge", + "omit terminal exchange", + "remove a local invocation", + "understate live stock", + "omit a local paid move", + "wrong reflected copy charge", + "alter residual orthogonal basis", + "misstate replication count", + "misstate stage count", + "alias data across stages", + "delay an idle advance past its level", + "truncate the last idle advance", + "re-use a helper bank slot", + "wrong residual frame", + "alias data across replica groups", + "omit the fourth replica group" + ] + }, + "candidate": { + "audit": { + "bank_assignments": 0, + "deficit": 10272, + "emitted_events": 7826400, + "emitted_program_sha256": "aa12307186ffceae745cb149810a8f69de1bb16a06d71785c7172864d68db607", + "hosted_residuals": 126144, + "live": 28416, + "maxchild": 42, + "mutations_rejected": [ + "slot outside window", + "copy index outside family", + "negative slot offset", + "wrong residual width", + "duplicate helper", + "omitted helper", + "hosted owner in another replica or outside the data stock", + "hosted owner on a wrong data family", + "wrong call orientation", + "duplicate call", + "changed idle rank", + "understated live stock", + "missing remainder summary", + "stale stage count", + "hosted coordinate beyond the pending set", + "overlapping hosted coordinates" + ], + "physical": 28425, + "profile": { + "1": 380448, + "10": 160, + "12": 96, + "14": 32, + "2": 400832, + "3": 22464, + "4": 26784, + "42": 288, + "5": 29376, + "6": 17344, + "7": 26496 + }, + "rank_mass": 1808352, + "status": "PASS_INDEPENDENT_REPLICATED_HOSTING_AUDIT" + }, + "invoice": { + "R": 438, + "bit": { + "bank_assignments": 0, + "charged_prefix_bits": 192, + "charged_two_level_coefficient_bits": 512, + "coefficient_bits": 177, + "halving_depth": 2, + "hosted_residuals": 126144, + "live": 28416, + "maxchild": 42, + "physical": 28425, + "prefix_bits": 177, + "rank_mass": 1808352, + "row_coefficient": 18355, + "two_level_coefficient_bits": 393 + }, + "bit_lower": "433544072119966441673/250000000000000000000000", + "bit_lower_decimal": "0.001734176288479865766692", + "bit_profile": { + "1": 380448, + "10": 160, + "12": 96, + "14": 32, + "2": 400832, + "3": 22464, + "4": 26784, + "42": 288, + "5": 29376, + "6": 17344, + "7": 26496 + }, + "emitted_program_sha256": "aa12307186ffceae745cb149810a8f69de1bb16a06d71785c7172864d68db607", + "next_grid_point_rejected": "1734176288479865766693/1000000000000000000000000", + "replicas": 32, + "stages": 9, + "status": "PASS_NINE_STAGE_WHOLE_HOSTED_BIT_PRICE_AND_CITED_ASSEMBLY" + }, + "parent": { + "all_scalar_columns_restored": true, + "bridge_additions": 63936, + "copy_erase_episodes": 2592, + "halving_integer_inequality": [ + 4096, + 3528 + ], + "independent_unbanked_scalar_columns": 4830, + "local_checks": { + "forward": { + "adds": 24248, + "all_columns": 660, + "cancellation_free_row_l1": 49347, + "copies": 9, + "profile": { + "1": 1321, + "2": 1344, + "3": 78, + "4": 44, + "5": 102, + "6": 11, + "7": 18 + }, + "records": 27175, + "sha256": "bea1cc10547012bc2586c1e0eefa93efaad944b9b081753dcb7946765433df56" + }, + "reverse": { + "adds": 24248, + "all_columns": 660, + "cancellation_free_row_l1": 1113070, + "copies": 9, + "profile": { + "1": 1321, + "2": 1344, + "3": 78, + "4": 44, + "5": 102, + "6": 11, + "7": 18 + }, + "records": 27175, + "sha256": "72d6999a278773914dfd3d8140d91681bb109b3c34425f333a9f02ee12b74266" + } + }, + "local_invocations": 288, + "omitted_bridge_shears_rejected": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17 + ], + "scalar_stages": [ + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": false, + "stage": 0 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": true, + "stage": 1 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": false, + "stage": 2 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": true, + "stage": 3 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": false, + "stage": 4 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": true, + "stage": 5 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": false, + "stage": 6 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": true, + "stage": 7 + }, + { + "all_columns": 4830, + "helper_columns": 3942, + "reverse": false, + "stage": 8 + } + ] + }, + "parent_controls": [ + "omit an idle child", + "omit a bridge", + "omit terminal exchange", + "remove a local invocation", + "understate live stock", + "omit a local paid move", + "wrong reflected copy charge", + "alter residual orthogonal basis", + "misstate replication count", + "misstate stage count", + "alias data across stages", + "delay an idle advance past its level", + "truncate the last idle advance", + "re-use a helper bank slot", + "wrong residual frame", + "alias data across replica groups", + "omit the fourth replica group" + ] + } + }, + "hosting_change": { + "hosted_helpers_per_replica": 3942, + "new_remainders": { + "10": 5, + "12": 3, + "14": 1, + "2": 430, + "4": 441, + "42": 9, + "6": 443, + "7": 666 + }, + "old_remainders": { + "2": 435, + "4": 444, + "42": 9, + "6": 444, + "7": 666 + }, + "removed_slots": [ + [ + 2, + 82, + 16, + 8, + 0, + 248 + ], + [ + 2, + 155, + 0, + 8, + 1, + 248 + ], + [ + 4, + 47, + 24, + 8, + 2, + 248 + ], + [ + 4, + 135, + 16, + 8, + 4, + 248 + ], + [ + 4, + 185, + 32, + 8, + 5, + 248 + ], + [ + 6, + 49, + 24, + 8, + 3, + 248 + ], + [ + 6, + 174, + 32, + 8, + 7, + 248 + ], + [ + 7, + 86, + 0, + 8, + 6, + 248 + ], + [ + 8, + 31, + 0, + 8, + 8, + 248 + ] + ], + "returned_idle_rank_per_replica": 72 + }, + "local": { + "baseline": { + "adds": 24305, + "copies": 9, + "forward_bound": 49347, + "helpers": 439, + "local_bits": 93, + "nine_stage_bits": 177, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "records": 27234, + "registers": 661, + "reverse_bound": 1113070, + "word_sha256": "5642fd0e35a1acc11acff8d0c08350c1617e95f310d4d35ad63a651f9eeeba0b" + }, + "candidate": { + "adds": 24248, + "copies": 9, + "forward_bound": 49347, + "helpers": 438, + "local_bits": 93, + "nine_stage_bits": 177, + "profile": { + "1": 1321, + "2": 1344, + "3": 78, + "4": 44, + "5": 102, + "6": 11, + "7": 18 + }, + "rank_mass": 5121, + "records": 27175, + "registers": 660, + "reverse_bound": 1113070, + "word_sha256": "27609b6880f8913900c0e1758c63a482f8588c16fede1bd0071c6df36ef2e285" + } + }, + "native": { + "baseline": { + "columns": { + "11": { + "bridge_additions": 2664, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "global_live_registers": 1549, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 267355, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "5": { + "bridge_additions": 666, + "copied_center_original_source_immutable": true, + "five_stage_additions": 121525, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "global_live_registers": 883, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 1998, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "global_live_registers": 1327, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 218745, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + }, + "interface": { + "columns": 661, + "conclusion": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": true, + "U_block_form": true + }, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 111 + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "interleaving": { + "B_target_reads_of_registers_rewritten_earlier_in_B": 111, + "B_z_operand_kinds": { + "helper<-helper": 3, + "helper<-source": 13, + "source<-helper": 108, + "source<-source": 375 + }, + "B_z_operand_kinds_by_dim": { + "dim4:helper<-source": 13, + "dim4:source<-source": 375, + "dim6:helper<-helper": 3, + "dim6:source<-helper": 108 + }, + "B_z_write_frame_dims": { + "4": 388, + "6": 111 + }, + "B_z_writes_after_a_target_read_of_the_same_register": 454, + "cleanup_gates": 2574, + "helper_writes_B": 16, + "source_writes_A": 0, + "source_writes_B": 483, + "sources_rewritten_B": 108, + "target_reads_of_targets": 0, + "z_gates_A": 2075, + "z_gates_B": 499 + }, + "punctured": 9, + "status": "PASS_EXACT_REPLAY_AND_INTERLEAVED_INTERFACE", + "totals_on_punctured_hyperplanes": true, + "v": 111 + }, + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24305, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27234, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + } + }, + "candidate": { + "columns": { + "11": { + "bridge_additions": 2664, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1548, + "fresh_center_copies": 99, + "global_live_registers": 1548, + "independent_dirty_registers": 438, + "local_odd_scalar_additions": 24248, + "local_raw_H": [ + [ + 1, + 1321 + ], + [ + 2, + 1344 + ], + [ + 3, + 78 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 18 + ] + ], + "local_registers": 660, + "local_scalar_additions": 24248, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 266728, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "5": { + "bridge_additions": 666, + "copied_center_original_source_immutable": true, + "five_stage_additions": 121240, + "formal_columns_checked": 882, + "fresh_center_copies": 45, + "global_live_registers": 882, + "independent_dirty_registers": 438, + "local_odd_scalar_additions": 24248, + "local_raw_H": [ + [ + 1, + 1321 + ], + [ + 2, + 1344 + ], + [ + 3, + 78 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 18 + ] + ], + "local_registers": 660, + "local_scalar_additions": 24248, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 1998, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1326, + "fresh_center_copies": 81, + "global_live_registers": 1326, + "independent_dirty_registers": 438, + "local_odd_scalar_additions": 24248, + "local_raw_H": [ + [ + 1, + 1321 + ], + [ + 2, + 1344 + ], + [ + 3, + 78 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 18 + ] + ], + "local_registers": 660, + "local_scalar_additions": 24248, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 218232, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24248, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + }, + "interface": { + "columns": 660, + "conclusion": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": true, + "U_block_form": true + }, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "gates": { + "A": 2074, + "B": 712, + "C": 2573, + "D": 111 + }, + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "interleaving": { + "B_target_reads_of_registers_rewritten_earlier_in_B": 111, + "B_z_operand_kinds": { + "helper<-helper": 3, + "helper<-source": 13, + "source<-helper": 108, + "source<-source": 375 + }, + "B_z_operand_kinds_by_dim": { + "dim4:helper<-source": 13, + "dim4:source<-source": 375, + "dim6:helper<-helper": 3, + "dim6:source<-helper": 108 + }, + "B_z_write_frame_dims": { + "4": 388, + "6": 111 + }, + "B_z_writes_after_a_target_read_of_the_same_register": 454, + "cleanup_gates": 2573, + "helper_writes_B": 16, + "source_writes_A": 0, + "source_writes_B": 483, + "sources_rewritten_B": 108, + "target_reads_of_targets": 0, + "z_gates_A": 2074, + "z_gates_B": 499 + }, + "punctured": 9, + "status": "PASS_EXACT_REPLAY_AND_INTERLEAVED_INTERFACE", + "totals_on_punctured_hyperplanes": true, + "v": 111 + }, + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24248, + "containment_pairs_checked": 2384, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2909, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1321 + ], + [ + 2, + 1344 + ], + [ + 3, + 78 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 18 + ] + ], + "rank_mass": 5121, + "records": 27175, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + } + } + }, + "no_new_kappa": true, + "paid_recount": { + "paid_calls": { + "baseline": 904896, + "candidate": 904320 + }, + "returned_idle_rank": 2304, + "saved_calls": 576 + }, + "selected_context": { + "binding": "complex", + "bit_lower": "1733427039589844234749/1000000000000000000000000", + "complex_lower": "416181814685169713943/250000000000000000000000", + "kappa": "1661960547713947/1000000000000000000" + }, + "status": "PASS_R438_SOURCE_BOUNDARY_AND_FULL_HOSTED_INVOICE" +} diff --git a/research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/NOTICE.md b/research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/NOTICE.md new file mode 100644 index 0000000000..e703c9d977 --- /dev/null +++ b/research/bit-deletion-ladder/vendor/pr2423/vendor/pr1043/NOTICE.md @@ -0,0 +1,28 @@ +# Notice + +New material is prepared for Ali Romman (@aliromman), with substantial +OpenAI Codex assistance. It is supplied under Apache-2.0, the repository +license. No independent human review is implied. + +The candidate starts from DreamingOfClouds's PR589 tuning of eumemic's PR555 +punctured word. The construction retains eumemic's PR543 L3 skeleton and +interleaved scalar interface, DreamingOfClouds's PR545 punctured-star geometry, +and the prior work identified in their source notices. + +The native exporter and legality checks come from Dylan Crow's PR370 lineage. +The multi-stage column checker comes from DaysSky's PR381. The parent and +pricing engines come from DreamingOfClouds's PR463/510 and PR315 lineage. +Whole-residual idle hosting comes from DaysSky's PR442, with the owner and +replica checks from chafreaky's PR443/472 lineage. The scalar interface also +uses Zhihao Chen's PR425 work. Jacob Sussman introduced the E8 unit. + +These tools are used from the two unchanged packages pinned in `SOURCES.json`. +Their source notices and licenses remain in those packages. The new builder +and independent record replay were written for this candidate. The new driver +uses the existing adapters and their existing supported parameters; it does +not change the pinned exporters, checkers or pricing engines. + +Source inlining and early helper retirement are prior ideas. The related +PR429/515 and PR433/437 work is acknowledged. PR953, PR980, PR997, PR1001 and PR1015 +were checked for overlap. This package claims one verified boundary and its +complete hosted invoice, not priority for a general circuit method. diff --git a/research/bit-deletion-ladder/vendor/pr2423/verify_rehost.py b/research/bit-deletion-ladder/vendor/pr2423/verify_rehost.py new file mode 100644 index 0000000000..58c76b9d7b --- /dev/null +++ b/research/bit-deletion-ladder/vendor/pr2423/verify_rehost.py @@ -0,0 +1,770 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Window-respecting optimal re-hosting of the R438 bit hosting slack (bit headroom only; no new kappa). + +PR1043 (aliromman) removes helper470 from the PR589 R439 bit word. Its hosting_change folds the nine freed width-8 +slots back into their own hosts in every replica and runs no hosting search. With 438 helpers the PR1023 slot model +has 3996 - 9*438 = 54 width-8 units of slack per replica instead of 45. This script: + + 1. DP. Proves the unique moment-minimising no-bank slot layout for S = 54 at the certified grid point. It uses an + exact top-3 interval DP over (capacity, unused units) built on PR1023's g_interval. An independent branch-and-bound + enumeration over all 10,556,685 layouts (sorted lists, provably skipped tails) cross-checks it, and the runner-up gap is reported as a certified interval. + S = 45 (R439) is a positive control: it reproduces the PR589 selection and PR1023's own width8_optimality. + 2. Windows. Checks every stage-window-feasible split of the optimum's slack over children 4 and 6 with seed72's + maxflow_assign and an independent all-subsets Hall test. + 3. Placement. Builds an explicit placement of all 9*438 helper occurrences per replica with seed14's allocate + (R = 438). It must equal PR442's deterministic expander, and it is audited by seed14's placement_audit and by an + independent audit. All 32 replica owner maps are also checked. + 4. Endpoints. Certifies bit endpoints with PR1023's packing.endpoint, using both pinned engines and the inherited + surcharge. The idle profile is combined with (a) PR1043's R438 local profile and (b) the transported-word profile + (declared input). PR589's c and PR1043's own c, with its own hosting, are reproduced as positive controls. +Negative controls (mutations that must be rejected) are run for every part. + +Usage: python3 -I -B verify_rehost.py [--repo ROOT] [--out RECEIPT.json] [--check RECEIPT.json] +The last line printed is PASS_R438_WINDOW_REHOST ... or FAIL_R438_WINDOW_REHOST ... +Standard-library CPython only. Inputs come from the repository working tree (sha256 and git-blob pinned) and from +vendor/pr1043 (byte copy, sha256 and git-blob pinned). +""" +import argparse +import hashlib +import json +import os +import sys +import time +import types +from collections import Counter +from fractions import Fraction as Q + +TAG = 'R438_WINDOW_REHOST' +HERE = os.path.dirname(os.path.abspath(__file__)) +DEFAULT_REPO = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + +# Main-tree inputs, read from --repo and pinned by sha256 and git blob id. The blob ids are those at canonical main +# 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2 (the research base of this script). +PINS = { + 'research/bit589-width-packing/packing.py': + ('2bb5515807714807961289e4ee6958c3ad7e0c27bbec4d9212b138c662a6cc7b', 'a6079ee0dd4d8037be477a3c4497f472348bde07'), + 'research/bit589-width-packing/SOURCES.json': + ('53fe98c8f01de7e32e3110e591d62e60292abb38cc11ecde4839f2eebd3b5fbc', 'f6a97de32691a1d426ac4819aad24c0c8414d97e'), + 'research/e8-bit-p111-tuned/tune/EXPECTED.json': + ('b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4', 'e293ddc557742637f9f679f083a1a282d87b1b13'), + 'research/e8-bit-p111-tuned/data/selection9-p111.json': + ('4ab1ed4529683cd184987f8bc3031fb7408b9cd22c25ab9cf541a8aaf896eaf1', 'e69ea66a3add357f570fc5552ab6368b3c8f9bb2'), + 'research/native-complex-moment552/engines/moment.py': + ('81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482', '7d697cb45203fe72d97037403d6da41f71f3b7fd'), + 'research/native-complex-moment552/engines/base_two_moment.py': + ('aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098', '14a90fa0e788217856f070382c9e61bd7c603c61'), + 'research/native-complex-moment552/engines/outer.py': + ('c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c', '43007488ad2c43187c77cc6798beff8b1cd76ad2'), + 'research/bit589-width7-windows-seed72/verify.py': + ('a5341ed222af84b51cd18645dd6b23e4613c0275cbf2663c94b07a9f916e9e60', '7f79a47146b150c9446e5f45e401d70b5cd12427'), + 'research/bit589-width7-windows-seed72/wopt.py': + ('a72daf1c7cff422543371a220fd391fe3b33552ac6ed52763f50b0c2f93d9532', '4e0bd3704d1a2be460ed25b363e95918119e8d42'), + 'research/bit589-width7-windows-seed72/windows.py': + ('a24295a51333b168ab73215f8a4bbb5bf831be829f572d1cde15fc322049c635', '4bb4f075ad5c1a49b4af310094bde6b2a4ea0c2e'), + 'research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/idle-axis-hosting/hosting_core.py': + ('d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3', '68b536daa9e6546c0aa046934bf840aaa3c3fde3'), + 'research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/audit_hosted_k.py': + ('57e558c80a2fea6e291587b04afd76dfaee3550729997798b61f33daf90b8ec9', '8864ca9b942a3507171edca0cf6cbaaf10fcf434'), + 'research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py': + ('6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8', '3df12bd632f1fdba825ced57110a1fee82eb2857'), + 'research/bit-helper470-window-placement-seed14/verify.py': + ('9cceeb610eccd6171585b056020ab6c44d7428de403a9ed035be1df9ae63f55b', 'c716a44e3b920f91918903d3480560e3882fbe80'), +} +# Vendored byte copies (see vendor/pr1043/NOTICE.md). +VENDOR = { + 'vendor/pr1043/CERTIFICATE.json': dict( + sha256='32c6cd6103006d627909cabdaf5083238c661a6582016a8b21075bd01c892eff', + git_blob='56400920050c523e6e399f2455137b36c35cf528', + origin='PR1043 (Ali Romman, @aliromman) head e309e17f83f5759b1ea1fa24a76f24838784cb4d, ' + 'research/bit-boundary-persistence/CERTIFICATE.json'), +} + +T, STAGES, M, V = 32, 9, 64, 111 +COPIES = 2 * V +GRID = Q(1, 10 ** 24) +C0_DECIMAL = '0.001733427039589844234749' # PR589 R439 selected bit endpoint +PR1043_DECIMAL = '0.001734176288479865766692' # PR1043's claimed R438 endpoint (own in-place hosting) +SCOUT_A = '0.001734802047828389852783' # predicted endpoint (a); checked, not assumed +SCOUT_B = '0.001734846264120199151475' # predicted endpoint (b); checked, not assumed +# (b) is a declared input here: the paid local profile of the R438 word after one A-transport (op 2027 -> slot 154 at +# frame 79, a PR1345 transport-atlas move on PR1043's word). verify_transport.py in this package rebuilds and replays +# that word and recounts this profile; this script only checks its rank mass and child count. +LOCAL_B = {1: 1322, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 18} +# Number of layouts = coefficient of x^S in 1/(1-x) * 1/((1-x)(1-x^2)(1-x^3)) * 1/((1-x)...(1-x^5)) (classes 14/28/42). +EXPECTED_LAYOUTS = {45: 3160688, 54: 10556685} + + +class Fail(Exception): + pass + + +def require(ok, message): + if not ok: + raise Fail(message) + + +def git_blob(raw): + return hashlib.sha1(b'blob %d\0' % len(raw) + raw).hexdigest() + + +def check_pin(raw, sha, blob, label): + require(hashlib.sha256(raw).hexdigest() == sha, 'sha256 pin: ' + label) + require(git_blob(raw) == blob, 'git blob pin: ' + label) + + +def read_pinned(base, rel, sha, blob): + path = os.path.join(base, *rel.split('/')) + with open(path, 'rb') as handle: + raw = handle.read() + check_pin(raw, sha, blob, rel) + return path, raw + + +def load_module(name, path, raw): + """Execute the already pinned bytes as a module (no second read of the file).""" + module = types.ModuleType(name) + module.__file__ = path + sys.modules[name] = module + exec(compile(raw, path, 'exec'), module.__dict__) + return module + + +def grid_decimal(c): + n = c * 10 ** 24 + require(n.denominator == 1 and n.numerator > 0, 'value on the 1e-24 grid') + s = str(n.numerator).rjust(25, '0') + return s[:-24] + '.' + s[-24:] + + +def fixed(k, n): + sign = '-' if k < 0 else '' + s = str(abs(k)).rjust(n + 1, '0') + return sign + s[:-n] + '.' + s[-n:] + + +def dfloor(x, n=36): + return fixed((x.numerator * 10 ** n) // x.denominator, n) + + +def dceil(x, n=36): + return fixed(-((-x.numerator * 10 ** n) // x.denominator), n) + + +def keyed(hist): + return {str(r): n for r, n in sorted(hist.items()) if n} + + +def unkeyed(hist): + return {int(r): n for r, n in hist.items()} + + +def expect_reject(controls, name, fn, needle, exc=(Exception,)): + """A negative control: fn must raise, with `needle` in the message.""" + try: + fn() + except exc as e: # noqa: PERF203 + message = '%s: %s' % (type(e).__name__, e) + require(needle in str(e), 'control %s rejected for the wrong reason: %s' % (name, message)) + controls.append(dict(name=name, rejected=True, reason=message)) + return + raise Fail('negative control %s was accepted' % name) + + +# --------------------------------------------------------------------------------------------------------------------- +# 1. Slot layouts: exact interval DP and independent exhaustive enumeration. + +def layout_terms(P, slots, c): + """Moves (capacity, u): one slot of that capacity keeps u unused width-8 places. Every capacity has a positive + remainder mod 8, so each slot has exactly one idle child whatever it hosts and the per-child surcharge is the same + for all layouts. The idle cost of a layout is then sum_slots g(remainder), g(r) = r (64/r)^c. Returns the moves, + certified lower and upper bounds of each move's cost change, and the g intervals.""" + rmin = {cap: cap % 8 for cap in slots} + require(all(rmin[cap] > 0 for cap in slots), 'some capacity is divisible by 8') + G = {} + caps = sorted(cap for cap in slots if cap // 8) + for cap in sorted(slots): + for u in range(cap // 8 + 1): + r = rmin[cap] + 8 * u + if r not in G: + G[r] = P.g_interval(r, c) + require(G[r][0] <= G[r][1], 'g interval order') + moves = [(cap, u) for cap in caps for u in range(1, cap // 8 + 1)] + lo = {mv: G[rmin[mv[0]] + 8 * mv[1]][0] - G[rmin[mv[0]]][1] for mv in moves} + hi = {mv: G[rmin[mv[0]] + 8 * mv[1]][1] - G[rmin[mv[0]]][0] for mv in moves} + return moves, lo, hi, G, rmin + + +def topk_dp(moves, lo, S, K): + """Top-K coin-change DP over move types in a fixed order. Each count vector arises on exactly one path, and the + top-K of a union of shifted top-K lists is exact, so this returns the K smallest layout lower bounds exactly.""" + best = [[(Q(0), ())]] + [[] for _ in range(S)] + for mv in moves: + u = mv[1] + new = [list(b) for b in best] + for s in range(u, S + 1): + for k in range(1, s // u + 1): + for v, lay in best[s - k * u]: + new[s].append((v + k * lo[mv], lay + ((mv, k),))) + best = [sorted(b)[:K] for b in new] + return [(v, tuple(sorted(lay))) for v, lay in best[S]] + + +def exhaustive_topk(moves, lo, S, K, dyad): + """Independent check: enumerate every layout as one multiset of unused counts per capacity class, with exact + integer costs (all bounds are multiples of 1/dyad). Branch-and-bound on per-class lists sorted by cost. + Returns the K smallest and the number of layouts covered.""" + ilo = {} + for mv in moves: + x = lo[mv] * dyad + require(x.denominator == 1, 'dyadic bound') + ilo[mv] = x.numerator + caps = sorted({cap for cap, _ in moves}) + tables = {} + for cap in caps: + umax = max(u for c, u in moves if c == cap) + table = {U: [] for U in range(S + 1)} + + def parts(rem, largest, acc, cost, cap=cap, table=table): + if rem == 0: + return + for u in range(min(largest, rem), 0, -1): + for k in range(1, rem // u + 1): + acc2 = acc + (((cap, u), k),) + cost2 = cost + k * ilo[(cap, u)] + used = sum(uu * kk for (_, uu), kk in acc2) + table[used].append((cost2, tuple(sorted(acc2)))) + parts(rem - k * u, u - 1, acc2, cost2) + table[0].append((0, ())) + parts(S, umax, (), 0) + for U in table: + table[U].sort() + tables[cap] = table + top = [] # sorted list of (cost, layout), at most K + covered = 0 + + def walk(i, rem, base, lay): + nonlocal covered + if i == len(caps) - 1: + lst = tables[caps[i]][rem] + covered += len(lst) + for cost, sub in lst: + v = base + cost + if len(top) == K and v > top[-1][0]: + break + top.append((v, tuple(sorted(lay + sub)))) + top.sort() + del top[K:] + return + for U in range(rem + 1): + for cost, sub in tables[caps[i]][U]: + walk(i + 1, rem - U, base + cost, lay + sub) + walk(0, S, 0, ()) + return [(Q(v, dyad), lay) for v, lay in top], covered + + +def idle_of(slots, rmin, layout): + h = Counter() + for cap, n in slots.items(): + h[rmin[cap]] += n + for (cap, u), k in layout: + h[rmin[cap]] -= k + h[rmin[cap] + 8 * u] += k + require(h[rmin[cap]] >= 0, 'more modified slots than slots') + return Counter({r: n for r, n in h.items() if n}) + + +def gap_interval(G, worse, better): + """Certified interval of sum g(worse) - sum g(better) for two idle histograms.""" + d = Counter(worse) + d.subtract(better) + lo = hi = Q(0) + for r, n in d.items(): + if n > 0: + lo += n * G[r][0] + hi += n * G[r][1] + elif n < 0: + lo += n * G[r][1] + hi += n * G[r][0] + return lo, hi + + +def layout_name(layout): + return ' + '.join('%dx(%d,%d)' % (k, cap, u) for (cap, u), k in sorted(layout, key=lambda t: (-t[1], t[0]))) + + +def certify_optimum(P, slots, S, c_star, W, check_exhaustive, dp_drop=()): + moves, lo, hi, G, rmin = layout_terms(P, slots, c_star) + require(S <= min(n for cap, n in slots.items() if cap // 8), 'slot-count limits are not vacuous') + top = topk_dp([mv for mv in moves if mv not in dp_drop], lo, S, 3) # dp_drop: negative control only + require(len(top) == 3, 'fewer than three layouts') + covered = None + if check_exhaustive: + top2, covered = exhaustive_topk(moves, lo, S, 3, P.MOMENT.DYAD) + require([v for v, _ in top2] == [v for v, _ in top], 'exhaustive enumeration disagrees with the DP (values)') + require([lay for _, lay in top2[:2]] == [lay for _, lay in top[:2]], + 'exhaustive enumeration disagrees with the DP (layouts)') + (l_opt, opt), (l_run, run), (l_third, third) = top + + def upper(lay): + return sum((k * hi[mv] for mv, k in lay), Q(0)) + require(l_run > upper(opt), 'optimum is not certified unique') + require(l_third > upper(run), 'runner-up is not certified') + idle_opt, idle_run = idle_of(slots, rmin, opt), idle_of(slots, rmin, run) + g_lo, g_hi = gap_interval(G, idle_run, idle_opt) + require(g_lo > 0, 'runner-up gap not positive') + return dict(c_star=c_star, opt=opt, run=run, third=third, opt_lo=l_opt, run_lo=l_run, idle_opt=idle_opt, + idle_run=idle_run, G=G, rmin=rmin, lo=lo, hi=hi, gap=(g_lo, g_hi), covered=covered, + receipt=dict(c_star=grid_decimal(c_star), slack_units=S, optimum=layout_name(opt), + optimum_idle_per_replica=keyed(idle_opt), runner_up=layout_name(run), + runner_up_idle_per_replica=keyed(idle_run), third=layout_name(third), + runner_up_gap_sum_g_per_replica=[dfloor(g_lo), dceil(g_hi)], + runner_up_gap_moment=[dfloor(T * g_lo / (M * W), 40), dceil(T * g_hi / (M * W), 40)], + exhaustive_layouts_covered=covered)) + + +def claim_is_optimal(cert, claimed): + """True iff `claimed` is certified strictly cheaper than every other layout (uses the certified top-3).""" + upper = sum((k * cert['hi'][mv] for mv, k in claimed), Q(0)) + others = [v for v, lay in ((cert['opt_lo'], cert['opt']), (cert['run_lo'], cert['run'])) if lay != claimed] + return all(v > upper for v in others) + + +# --------------------------------------------------------------------------------------------------------------------- +# 2. Stage windows. + +def hall_check(supply, demand, allowed): + """All-subsets Hall test for the stage -> child transport (independent of max-flow).""" + kids = [i for i in sorted(demand) if demand[i]] + if sum(supply.values()) != sum(demand.values()): + return False, 'totals differ' + for mask in range(1, 1 << len(kids)): + C = [kids[j] for j in range(len(kids)) if mask >> j & 1] + nbr = set() + for i in C: + nbr |= set(allowed[i]) + if sum(demand[i] for i in C) > sum(supply.get(s, 0) for s in nbr): + return False, 'children %s' % C + return True, None + + +def demand_for(config): + """config = (idle copies of child 4, child holding the one-residual copy); the other 10 - x4 idle copies are in + child 6. Children 0, 2, 7, 8 stay full; children 1, 3, 5 (capacity 7) host nothing.""" + x4, partial = config + d = {0: COPIES * 1, 1: 0, 2: COPIES * 3, 3: 0, 5: 0, 7: COPIES * 3, 8: COPIES * 1} + for child, idle in ((4, x4), (6, 10 - x4)): + part = 1 if partial == child else 0 + d[child] = 5 * (COPIES - idle - part) + part + return d + + +# --------------------------------------------------------------------------------------------------------------------- +# 3. Independent placement audit (mirrors the slot rules of audit_hosted_k, written without its code). + +def audit_slots(slots, hosting, active, R): + cells, seen = {}, set() + for i, cp, off, w, s, h in slots: + require(i in hosting, 'unknown host child') + pair, cap, stages = hosting[i] + require(s in stages, 'stage outside window') + require(pair != active[s], 'host pair active at stage') + require(0 <= cp < COPIES and 0 <= h < R and 0 <= s < STAGES, 'index domain') + require(w == 8, 'residual width') + require(0 <= off and off + w <= cap, 'slot extent') + occ = cells.setdefault((i, cp), set()) + new = set(range(off, off + w)) + require(not occ & new, 'cell collision') + occ |= new + require((s, h) not in seen, 'duplicate (stage, helper)') + seen.add((s, h)) + require(seen == {(s, h) for s in range(STAGES) for h in range(R)}, 'missing (stage, helper)') + rem = Counter() + for i, (pair, cap, stages) in hosting.items(): + for cp in range(COPIES): + r = cap - len(cells.get((i, cp), ())) + if r: + rem[r] += 1 + return rem + + +def main(args): + t0 = time.time() + repo = os.path.abspath(args.repo) + raw = {} + for rel, (sha, blob) in PINS.items(): + raw[rel] = read_pinned(repo, rel, sha, blob) + vend = {} + for rel, pin in VENDOR.items(): + vend[rel] = read_pinned(HERE, rel, pin['sha256'], pin['git_blob'])[1] + P = load_module('r438_packing', *raw['research/bit589-width-packing/packing.py']) + S72 = load_module('r438_seed72_verify', *raw['research/bit589-width7-windows-seed72/verify.py']) + S14 = load_module('r438_seed14_verify', *raw['research/bit-helper470-window-placement-seed14/verify.py']) + HC = load_module('r438_pr442_hosting_core', *raw['research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/' + 'vendor/idle-axis-hosting/hosting_core.py']) + cert = json.loads(vend['vendor/pr1043/CERTIFICATE.json']) + controls = [] + pin = VENDOR['vendor/pr1043/CERTIFICATE.json'] + tampered = vend['vendor/pr1043/CERTIFICATE.json'].replace(b'"1": 1321', b'"1": 1320', 1) + require(tampered != vend['vendor/pr1043/CERTIFICATE.json'], 'tamper control setup') + expect_reject(controls, 'vendored_pr1043_certificate_tampered', + lambda: check_pin(tampered, pin['sha256'], pin['git_blob'], 'vendor/pr1043/CERTIFICATE.json'), + 'sha256 pin') + out = dict(status='PASS_' + TAG, scope='bit headroom only; no new kappa; the selected record is complex-bound; every R438 row is conditional on PR1043 (open, not admitted); row (b) also on the transported word of verify_transport.py', + inputs=dict(main_tree={rel: dict(sha256=s, git_blob=b) for rel, (s, b) in sorted(PINS.items())}, + vendored={rel: dict(sha256=p['sha256'], git_blob=p['git_blob'], origin=p['origin']) + for rel, p in VENDOR.items()})) + + # -- 0. Baseline binding: PR589 record, PR1023 slot model, PR1043 certificate. ------------------------------------ + record = P.pinned_json('bit_record') + selection = P.pinned_json('selection') + model = P.slot_model(record, selection) + W = record['nine']['bit']['live'] + require((model['R'], model['v'], W, model['calls']) == (439, V, 28416, STAGES * T), 'PR589 record dimensions') + c0 = Q(record['nine']['bit_lower']) + require(grid_decimal(c0) == C0_DECIMAL, 'PR589 bit endpoint') + local439 = Counter(model['local']) + require(unkeyed(cert['local']['baseline']['profile']) == dict(local439), 'PR1043 baseline local = PR589 record') + require(unkeyed(cert['hosted']['baseline']['invoice']['bit_profile']) == dict(model['H']), + 'PR1043 baseline hosted profile = PR589 record') + require(Q(cert['hosted']['baseline']['invoice']['bit_lower']) == c0, 'PR1043 baseline c = PR589 c') + local_a = Counter(unkeyed(cert['local']['candidate']['profile'])) + require(cert['local']['candidate']['helpers'] == 438 and cert['hosted']['candidate']['invoice']['R'] == 438, 'R438') + d = Counter(local_a) + d.subtract(local439) + require(+d == Counter({2: 2}) and -d == Counter({1: 2, 3: 1, 7: 1}), 'PR1043 local delta {1:-2,2:+2,3:-1,7:-1}') + for name, loc in (('a', local_a), ('b', Counter(LOCAL_B))): + require(sum(r * n for r, n in loc.items()) == 8 * 438 + 63 + 14 * V == 5121, 'local rank mass (%s)' % name) + require(sum(loc.values()) == 2918, 'local child count (%s)' % name) + + # -- 1. Windows and slots. --------------------------------------------------------------------------------------- + WIN72 = S72.WIN # global_k anchor + three window predicates (seed72 windows.py) + win14 = S14.windows(S14.schedule()) # seed14's independent transcription: {idx: (pair, rank, stages)} + require(set(WIN72) == {i for i, (p, r, st) in win14.items() if r and st}, 'hosting children agree') + require(all(win14[i][1:] == (WIN72[i][0], tuple(WIN72[i][1])) for i in WIN72), 'seed72 and seed14 windows agree') + require({i: c for i, (c, st) in WIN72.items()} == model['caps'], 'window capacities = PR1023 slot capacities') + hosting = {i: (win14[i][0], WIN72[i][0], tuple(WIN72[i][1])) for i in sorted(WIN72)} + sched72 = S72.wopt.windows.schedule() + active = {e['stage']: e['pair'] for e in sched72 if e['kind'] == 'local_cover_sweep'} + require(sorted(active) == list(range(STAGES)), 'one local sweep per stage') + slots = Counter() + for i, (c, st) in WIN72.items(): + slots[c] += COPIES + require(slots == model['slots'] == Counter({7: 666, 14: 444, 28: 444, 42: 444}), 'slots per replica') + units = sum((c // 8) * n for c, n in slots.items()) + S439, S438 = units - STAGES * 439, units - STAGES * 438 + require((units, S439, S438) == (3996, 45, 54), 'width-8 slack per replica') + out['windows'] = {str(i): dict(pair=p, capacity=c, stages=list(st)) for i, (p, c, st) in hosting.items()} + out['slots_per_replica'] = keyed(slots) + out['width8_units_per_replica'] = dict(capacity=units, slack_R439=S439, slack_R438=S438) + + # -- 4a. Endpoint positive controls (needed for the DP grid points). --------------------------------------------- + def profile(local, idle): + H = Counter({r: n * STAGES * T for r, n in local.items()}) + for r, n in idle.items(): + H[r] += n * T + require(all(n > 0 for n in H.values()), 'positive profile entries') + return dict(sorted(H.items())) + + def price(local, idle, label): + H = profile(local, idle) + require(sum(r * n for r, n in H.items()) == 1808352, 'hosted rank mass (%s)' % label) + require(M * M > 2 * max(H) ** 2, 'halving guard (%s)' % label) + return P.endpoint(H, W), H + + c_pr589, H_pr589 = price(local439, model['idle_rep'], 'pr589') + require(c_pr589 == c0 and H_pr589 == dict(model['H']), 'positive control: PR589 endpoint reproduced') + # PR1043's own hosting_change, re-derived from the frozen selection with seed14's allocate (R = 439). + alloc439 = S14.allocate(selection['bit']) + removed = [list(x) for x in alloc439 if x[5] == 470 - 2 * V] + require(removed == cert['hosting_change']['removed_slots'], 'PR1043 removed slots re-derived') + rem439, _ = S14.placement_audit(alloc439, win14, frozenset()) + rem_inplace = Counter(rem439) + for i, cp, off, w, s, h in removed: + rem_inplace[(i, cp)] += w + idle_pr1043 = Counter(r for r in rem_inplace.values() if r) + require(dict(idle_pr1043) == unkeyed(cert['hosting_change']['new_remainders']), 'PR1043 in-place remainders') + require(Counter(r for r in rem439.values() if r) == model['idle_rep'], 'PR589 remainders from seed14 allocate') + c_pr1043, H_pr1043 = price(local_a, idle_pr1043, 'pr1043') + require(H_pr1043 == unkeyed(cert['hosted']['candidate']['invoice']['bit_profile']), 'PR1043 hosted profile') + require(c_pr1043 == Q(cert['hosted']['candidate']['invoice']['bit_lower']), 'PR1043 endpoint (certificate)') + require(grid_decimal(c_pr1043) == PR1043_DECIMAL, 'positive control: PR1043 endpoint reproduced') + + # -- 1. Exact DP. S = 45 positive control, then S = 54. -------------------------------------------------------- + c0_star = c0 + GRID + cert45 = certify_optimum(P, slots, S439, c0_star, W, check_exhaustive=True) + require(cert45['covered'] == EXPECTED_LAYOUTS[45], 'exhaustive enumeration covered every S = 45 layout') + require(cert45['opt'] == (((42, 5), 9),), 'S = 45 optimum is nine fully idle 42-slots') + require(cert45['idle_opt'] == model['idle_rep'], 'S = 45 optimum = PR589 selected remainders') + pr1023 = P.width8_optimality(model, c0_star) # PR1023's own per-unit certificate (hard-coded slack 45) + require(pr1023['runner_up'] == 'capacity 42, u = 4' and pr1023['slack_units_per_replica'] == 45, 'PR1023 replay') + + # The PR1023 per-unit argument cannot be reused at R438: its hard-coded slack 45 rejects the R438 model. + model438 = dict(model, R=438, idle_rep=Counter({2: 433, 4: 444, 6: 444, 7: 666, 42: 10, 34: 1})) + expect_reject(controls, 'pr1023_width8_optimality_hardcoded_45_rejects_R438', + lambda: P.width8_optimality(model438, c0_star), 'slack per replica') + + # Endpoint candidates (a) and (b): the DP optimum is computed at each one's own next grid point. + rows = {} + certs = {} + # Candidate layout: the S = 54 DP optimum at c0 + 1e-24. It is priced with each local profile, and the DP is then + # re-certified at that profile's own next grid point, where it must return the same layout. + candidate = certify_optimum(P, slots, S438, c0_star, W, check_exhaustive=False)['idle_opt'] + for name, local, scout in (('a', local_a, SCOUT_A), ('b', Counter(LOCAL_B), SCOUT_B)): + idle = candidate + c, H = price(local, idle, name) + cs = certify_optimum(P, slots, S438, c + GRID, W, check_exhaustive=True) + require(cs['covered'] == EXPECTED_LAYOUTS[54], 'exhaustive enumeration covered every S = 54 layout (%s)' % name) + require(cs['idle_opt'] == idle, 'DP optimum at c + 1e-24 is the priced layout (%s)' % name) + require(grid_decimal(c) == scout, 'scouting endpoint (%s) reproduced' % name) + certs[name] = cs + rows['r438_window_optimum_local_' + name] = dict(endpoint=grid_decimal(c), endpoint_fraction=str(c), + profile=keyed(H), children=sum(H.values()), + rank_mass=sum(r * n for r, n in H.items())) + rows['r438_window_optimum_local_' + name]['_c'] = c + ca = rows['r438_window_optimum_local_a'].pop('_c') + cb = rows['r438_window_optimum_local_b'].pop('_c') + require(certs['a']['opt'] == (((42, 4), 1), ((42, 5), 10)), 'R438 optimum = 10 fully idle 42-slots + one (42,4)') + require(certs['a']['run'] == (((14, 1), 1), ((28, 3), 1), ((42, 5), 10)), 'R438 runner-up') + require(dict(certs['a']['idle_opt']) == {2: 433, 4: 444, 6: 444, 7: 666, 42: 10, 34: 1}, 'R438 idle profile') + c_b_inplace, _ = price(Counter(LOCAL_B), idle_pr1043, 'b_inplace') + c_run_a, _ = price(local_a, certs['a']['idle_run'], 'runner_up_a') + require(c_pr1043 < c_run_a < ca, 'runner-up layout endpoint lies between PR1043 and the optimum') + rows['r438_runner_up_layout_local_a'] = dict(endpoint=grid_decimal(c_run_a), layout=layout_name(certs['a']['run'])) + rows['pr589_r439_selected'] = dict(endpoint=grid_decimal(c0), profile=keyed(H_pr589)) + rows['pr1043_r438_inplace_local_a'] = dict(endpoint=grid_decimal(c_pr1043), profile=keyed(H_pr1043), + children=sum(H_pr1043.values())) + rows['pr1043_r438_inplace_local_b'] = dict(endpoint=grid_decimal(c_b_inplace)) + for key, c in (('r438_window_optimum_local_a', ca), ('r438_window_optimum_local_b', cb), + ('pr1043_r438_inplace_local_b', c_b_inplace), ('r438_runner_up_layout_local_a', c_run_a)): + rows[key]['gain_vs_pr1043_percent'] = dfloor(100 * (c - c_pr1043) / c_pr1043, 8) + rows[key]['gain_vs_pr589_percent'] = dfloor(100 * (c - c0) / c0, 8) + + # PR1043's in-place layout, as a layout: certified strictly worse than the optimum at c_a + 1e-24. + ca_cert = certs['a'] + lay1043 = (((14, 1), 1), ((28, 1), 3), ((42, 1), 5), ((42, 5), 9)) + require(idle_of(slots, ca_cert['rmin'], lay1043) == idle_pr1043, 'PR1043 layout = its in-place remainders') + g1043 = gap_interval(ca_cert['G'], idle_pr1043, ca_cert['idle_opt']) + require(g1043[0] > 0, 'PR1043 in-place layout is strictly worse than the optimum') + require(claim_is_optimal(ca_cert, ca_cert['opt']), 'the optimum certifies') + expect_reject(controls, 'dp_with_move_42_4_dropped_vs_exhaustive', + lambda: certify_optimum(P, slots, S438, ca + GRID, W, check_exhaustive=True, dp_drop=((42, 4),)), + 'exhaustive enumeration disagrees with the DP') + expect_reject(controls, 'runner_up_claimed_optimal', + lambda: require(claim_is_optimal(ca_cert, ca_cert['run']), 'claimed optimum not certified'), + 'claimed optimum not certified') + expect_reject(controls, 'pr1043_inplace_layout_claimed_optimal', + lambda: require(claim_is_optimal(ca_cert, lay1043), 'claimed optimum not certified'), + 'claimed optimum not certified') + bad_idle = Counter(ca_cert['idle_opt']) + bad_idle[34] -= 1 + bad_idle[2] += 1 # silently host the four missing residuals: mass must change + expect_reject(controls, 'optimum_profile_with_partial_slot_dropped', lambda: price(local_a, +bad_idle, 'bad'), + 'hosted rank mass') + for name, c in (('a', ca), ('b', cb)): + H = profile(local_a if name == 'a' else Counter(LOCAL_B), certs[name]['idle_opt']) + + def accept_next(H=H, c=c): + lo, hi = P.MOMENT.moment(H, M, W, c + GRID, True) + require(hi < 1, 'moment at c + 1e-24 is not below one') + expect_reject(controls, 'endpoint_plus_1e-24_accepted_%s' % name, accept_next, 'not below one') + + out['dp'] = dict(S45_positive_control=dict(cert45['receipt'], pr1023_width8_optimality=dict( + runner_up_per_unit=pr1023['runner_up'], margin_lower_bound=pr1023['margin_lower_bound'])), + S54_at_c_a_next=certs['a']['receipt'], S54_at_c_b_next=certs['b']['receipt'], + pr1043_inplace_layout=dict(layout=layout_name(lay1043), idle_per_replica=keyed(idle_pr1043), + gap_sum_g_per_replica_at_c_a_next=[dfloor(g1043[0]), dceil(g1043[1])], + gap_moment_at_c_a_next=[dfloor(T * g1043[0] / (M * W), 40), + dceil(T * g1043[1] / (M * W), 40)])) + + # -- 2. Stage-window feasibility (seed72 max-flow, independent Hall test). ---------------------------------------- + supply = {s: 438 for s in range(STAGES)} + allowed = {i: set(st) for i, (p, c, st) in hosting.items()} + configs = [(x4, part) for x4 in range(11) for part in (4, 6)] + feasible = [] + flows = {} + for cfg in configs: + dem = demand_for(cfg) + require(sum(dem.values()) == STAGES * 438, 'demand total') + x = S72.maxflow_assign(supply, dem, allowed) + ok, _ = hall_check(supply, dem, allowed) + require((x is not None) == ok, 'max-flow and Hall disagree at %s' % (cfg,)) + if x is not None: + require(all(s in allowed[i] and n > 0 for (s, i), n in x.items()), 'flow inside windows') + require(all(sum(n for (s, i), n in x.items() if i == j) == dem[j] for j in dem), 'flow meets demand') + require(all(sum(n for (s, i), n in x.items() if s == t) == 438 for t in range(STAGES)), 'flow uses supply') + feasible.append(cfg) + flows[cfg] = x + require(len(feasible) == len(configs), 'every split of the optimum over children 4/6 is window-feasible') + + def tightened(child, stages): + def run(): + al = dict(allowed) + al[child] = set(stages) + dem = demand_for((0, 6)) + ok, why = hall_check(supply, dem, al) + x = S72.maxflow_assign(supply, dem, al) + require((x is None) == (not ok), 'max-flow and Hall disagree on the tightened window') + require(x is not None, 'infeasible: Hall violated by %s' % why) + return run + expect_reject(controls, 'window_child4_tightened_to_stages_0_1', tightened(4, (0, 1)), 'Hall violated') + expect_reject(controls, 'window_child6_tightened_to_stages_7_8', tightened(6, (7, 8)), 'Hall violated') + + def r439_supply(): + x = S72.maxflow_assign({s: 439 for s in range(STAGES)}, demand_for((0, 6)), allowed) + require(x is not None, 'infeasible: 439 helpers per stage do not fit the R438 optimum') + expect_reject(controls, 'r439_supply_into_r438_optimum', r439_supply, 'do not fit') + out['windows_feasibility'] = dict(configs_checked=len(configs), feasible=len(feasible), + note='x4 idle 42-copies in child 4, 10-x4 in child 6, one-residual copy in ' + 'child 4 or 6; children 0,2,7,8 full; capacity-7 children host nothing') + + # -- 3. Explicit placement of all helper occurrences. ------------------------------------------------------------- + chosen = (0, 6) + x = flows[chosen] + patterns = [[0, [8], COPIES], [1, [], COPIES], [2, [8] * 3, COPIES], [3, [], COPIES], [4, [8] * 5, COPIES], + [5, [], COPIES], [6, [], 10], [6, [8], 1], [6, [8] * 5, COPIES - 11], [7, [8] * 3, COPIES], + [8, [8], COPIES]] + sel438 = dict(patterns=patterns, stages=sorted([i, 8, s, n] for (s, i), n in x.items())) + require(S14.R == 439 and S14.V == V and S14.T == T, 'seed14 constants') + S14.R = 438 # adapt seed14's allocator/audit to R = 438 (module instance only) + try: + alloc = S14.allocate(sel438) + rem438, _ = S14.placement_audit(alloc, win14, frozenset()) + owners = S14.owners_for_replicas(alloc, win14) + finally: + S14.R = 439 + require(len(alloc) == STAGES * 438, 'occurrences per replica') + win_hc = {i: (p, c, frozenset(st)) for i, (p, c, st) in hosting.items()} + ys = {(i, tuple(pat)): n for i, pat, n in patterns} + zs = {(i, w, s): n for i, w, s, n in sel438['stages']} + slots_hc, rem_hc = HC.expand(win_hc, ys, zs, {s: [(h, 8) for h in range(438)] for s in range(STAGES)}, COPIES) + require(slots_hc == alloc, 'seed14 allocate = PR442 expand (slot for slot)') + idle_seed14 = Counter(r for r in rem438.values() if r) + idle_hc = Counter(r for r in rem_hc.values() if r) + idle_mine = audit_slots(alloc, hosting, active, 438) + require(idle_seed14 == idle_hc == idle_mine == ca_cert['idle_opt'], 'placement remainders = DP optimum') + seen = set() + for stage, rep, h, fam, child, off, w in owners: + r_, rest = divmod(fam, 8 * V) + pair2, port = divmod(rest, V) + require(r_ == rep and pair2 // 2 == hosting[child][0] != active[stage], 'owner family pair') + require((stage, rep, h) not in seen, 'owner once') + seen.add((stage, rep, h)) + require(len(seen) == STAGES * T * 438 == 126144, 'all hosted residual roles') + canon = json.dumps([list(t) for t in alloc], separators=(',', ':')).encode() + out['placement'] = dict(split='all 10 idle 42-copies and the one-residual copy in child 6', selection=sel438, + occurrences_per_replica=len(alloc), hosted_residual_roles=len(seen), + idle_per_replica=keyed(idle_seed14), slot_list_sha256=hashlib.sha256(canon).hexdigest(), + builders_agree='seed14 allocate == PR442 hosting_core.expand', + audits='seed14 placement_audit, independent audit_slots, seed14 owners_for_replicas') + + def mutated(fn): + lst = [list(t) for t in alloc] + fn(lst) + return [tuple(t) for t in lst] + + def first(pred, lst): + return next(k for k, t in enumerate(lst) if pred(t)) + + def m_window(lst): + k = first(lambda t: t[0] == 4, lst) + lst[k][4] = 6 # child 4 admits stages 0-5 + def m_collision(lst): + k = first(lambda t: t[0] == 4 and t[2] == 8, lst) + lst[k][2] = 0 + def m_duplicate(lst): + k = first(lambda t: t[0] == 2 and t[2] == 8, lst) + j = first(lambda t: t[4] == lst[k][4] and t[5] != lst[k][5], lst) + lst[k][5] = lst[j][5] + def m_missing(lst): + del lst[-1] + def m_extent(lst): + k = first(lambda t: t[0] == 6 and t[1] == COPIES - 11, lst) + lst[k][2] = 36 # 36 + 8 > 42 + def m_domain(lst): + lst[-1][5] = 438 + def m_width(lst): + lst[0][3] = 7 + mutations = [('placement_stage_outside_window', m_window, 'outside untouched window', 'stage outside window'), + ('placement_cell_collision', m_collision, 'coordinate collision', 'cell collision'), + ('placement_duplicate_helper', m_duplicate, 'duplicate helper', 'duplicate (stage, helper)'), + ('placement_missing_helper', m_missing, 'missing helper', 'missing (stage, helper)'), + ('placement_slot_extent', m_extent, 'slot extent', 'slot extent'), + ('placement_helper_out_of_domain', m_domain, 'owner domain', 'index domain'), + ('placement_width7_residual', m_width, 'helper residual width', 'residual width')] + + def seed14_audit(lst, win, R=438): + S14.R = R + try: + S14.placement_audit(lst, win, frozenset()) + finally: + S14.R = 439 + for name, fn, n14, mine in mutations: + lst = mutated(fn) + expect_reject(controls, name + '/seed14', lambda lst=lst: seed14_audit(lst, win14), n14) + expect_reject(controls, name + '/independent', lambda lst=lst: audit_slots(lst, hosting, active, 438), mine) + # Owner activity: swap the (stage, helper) of the first child-6 role with the first stage-1 role (child j), and + # widen the windows so that both moved roles are inside them: child 6 gets stage 1 (its pair 0 is the active pair + # there) and child j gets the child-6 role's stage (where child j's pair is not active). The occurrence set, + # widths and cells are unchanged; only the active-data (owner inactivity) rule can reject. + lst = [list(t) for t in alloc] + k6 = first(lambda t: t[0] == 6, lst) + kj = first(lambda t: t[4] == 1, lst) + j, s6 = lst[kj][0], lst[k6][4] + require(hosting[6][0] == active[1] and hosting[j][0] != active[s6], 'active-pair control setup') + (lst[kj][4], lst[kj][5]), (lst[k6][4], lst[k6][5]) = (lst[k6][4], lst[k6][5]), (lst[kj][4], lst[kj][5]) + lst = [tuple(t) for t in lst] + win14_mut, hosting_mut = dict(win14), dict(hosting) + for child, extra in ((6, 1), (j, s6)): + win14_mut[child] = win14[child][:2] + (tuple(sorted(set(win14[child][2]) | {extra})),) + hosting_mut[child] = hosting[child][:2] + (tuple(sorted(set(hosting[child][2]) | {extra})),) + expect_reject(controls, 'placement_host_pair_active/seed14', lambda: seed14_audit(lst, win14_mut), + 'host is active data') + expect_reject(controls, 'placement_host_pair_active/independent', + lambda: audit_slots(lst, hosting_mut, active, 438), 'host pair active at stage') + expect_reject(controls, 'placement_audited_as_R439/seed14', lambda: seed14_audit(alloc, win14, R=439), + 'missing helper') + expect_reject(controls, 'placement_audited_as_R439/independent', lambda: audit_slots(alloc, hosting, active, 439), + 'missing (stage, helper)') + + # -- 4. Endpoint summary. ---------------------------------------------------------------------------------------- + out['endpoints'] = rows + out['claims'] = dict( + optimum_idle_per_replica=keyed(ca_cert['idle_opt']), + c_window_optimum_local_a=grid_decimal(ca), c_window_optimum_local_b=grid_decimal(cb), + c_pr1043_inplace=grid_decimal(c_pr1043), c_pr589=grid_decimal(c0), + certificate='moment(opt, c+1e-24) > 1 by both engines; every other no-bank R438 slot layout has a certified ' + 'larger idle sum at c+1e-24 with the same child count and local profile, hence a larger moment; ' + 'so no layout in the slot model reaches c+1e-24', + kappa='unchanged; the bit side does not bind') + out['negative_controls'] = controls + elapsed = time.time() - t0 + return out, elapsed, ca, cb, c_pr1043 + + +if __name__ == '__main__': + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--repo', default=DEFAULT_REPO, + help='repository root (default: the parent of the research/ directory holding this script)') + ap.add_argument('--out', help='write the JSON receipt here (e.g. RECEIPT.json next to this script)') + ap.add_argument('--check', help='require the regenerated receipt to equal this file byte for byte') + a = ap.parse_args() + if sys.flags.optimize or not __debug__: + print('FAIL_%s refusing to run under python -O (assert-based checks in pinned modules would be skipped)' % TAG) + sys.exit(2) + try: + receipt, elapsed, ca, cb, c1043 = main(a) + text = json.dumps(receipt, indent=1, sort_keys=True) + '\n' + if a.check: + with open(a.check) as handle: + require(handle.read() == text, 'receipt differs from ' + a.check) + if a.out: + with open(a.out, 'w') as handle: + handle.write(text) + except (Exception, SystemExit) as e: # seed72's need() raises SystemExit + print('FAIL_%s %s: %s' % (TAG, type(e).__name__, e)) + sys.exit(1) + print('python %s; %.1f s' % (sys.version.split()[0], elapsed)) + print('PASS_%s S=54 opt=10x(42,5)+1x(42,4) idle={2:433,4:444,6:444,7:666,34:1,42:10} c_a=%s c_b=%s ' + 'pr1043_inplace=%s window_splits=22/22 controls=%d no_new_kappa' + % (TAG, grid_decimal(ca), grid_decimal(cb), grid_decimal(c1043), len(receipt['negative_controls'])))