diff --git a/research/rank7-r1-t740-cap/CLAIM.json b/research/rank7-r1-t740-cap/CLAIM.json new file mode 100644 index 0000000000..30c2f74318 --- /dev/null +++ b/research/rank7-r1-t740-cap/CLAIM.json @@ -0,0 +1,76 @@ +{ + "allocation": { + "payload_sha256": { + "DISPATCH.json": "90edc935320dd6264e98dc735d868df3c95f5901c70d7d96171001fcb295cce0", + "FILL.json.gz": "b56bfed2c542e63f4139e8e3ebb9fe0c979a3bab1ba6a934e2113f40f5c7e0f0", + "ORDER.json": "927226d702bf3cada076f4c459da9063c0df7e7154a62955cf75c40cf30215b9", + "PROFILE.json": "83130e5231b3693c2af871c430833601de83fdd8851c024df4f78efc76c8deef" + }, + "relocations": 332, + "source": "PR2979 allocation/ (T74 ORDER/DISPATCH/FILL, used unchanged by PR3015), ten lockstep copies (PR2969 convention)", + "touched_bins": 263 + }, + "baseline_head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "baseline_kappa": "17291509735342244286949999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "baseline_pr": 3015, + "best_open_claim_head": "217edac2ebfa6250536bd6df153de14901a69395", + "best_open_claim_kappa": "0.0017291512039830184429979999999999999999999998999999999999999999999999", + "best_open_claim_pr": 3021, + "calls": 6660, + "complex_lower": "345830551200866186907/200000000000000000000000", + "fixed_inventory_cap": { + "cap_lower": "345830551200866186907/200000000000000000000000", + "cap_upper": "17291527560043309345351/10000000000000000000000000", + "realized": "attained: the literal idle histogram is exactly 740 x the optimal basic idle profile (verify.py)" + }, + "gain_over_pr3015": "22280876331323/12500000000000000000000", + "gain_over_pr3015_decimal": "1.78247010650584E-9", + "gain_over_pr3021": "1552021312491537/1000000000000000000000000", + "gain_over_pr3021_float": 1.552021312491537e-09, + "headline_convention": "floor of the exact root lower end at 24 digits, minus 10^-46 and 10^-70, as PR2979/PR3015/PR3021 (tools/audit_allocation_moment.py)", + "helpers": 408, + "idle": { + "1": 173160, + "3": 49617, + "48": 281903, + "5": 17205 + }, + "kappa": "17291527560043309345349999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017291527560043309345349999999999999999999998999999999999999999999999", + "live_families": 663040, + "local_profile": { + "1": 2443, + "2": 707, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "meaning": "Moment nomination: PR3015's R1 words (PR2979's words with Jeremy Kothe's declared restore edit R1) with a literal T740 allocation that attains their fixed-capacity packing cap. PR3015's complete T74 release covers the words; the T740 allocation's complete admission/outer release is separate.", + "physical_families": 663549, + "profile": { + "1": 16443540, + "2": 4708620, + "3": 1594737, + "4": 719280, + "48": 281903, + "5": 137085, + "8": 53280 + }, + "replicas": 740, + "roles": 2717280, + "root_lower": "345830551200866186907/200000000000000000000000", + "root_upper": "17291527560043309345351/10000000000000000000000000", + "scope": "Packing composed with PR3015's declared R1 edit; no other word, gate, frame, scalar or cleanup change. Inherited all-size/compiler/theorem hypotheses remain. No selected-frontier change and no independent human review is claimed.", + "status": "FINITE_OWNER_AND_MOMENT_CANDIDATE_OUTER_PENDING", + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + }, + "words": "PR3015 edits/FINAL-WORD-base.json.gz and FINAL-WORD-extra.json.gz (vendored as data/R1-WORD-*.json.gz), unchanged", + "zero_buffers": 91 +} diff --git a/research/rank7-r1-t740-cap/README.md b/research/rank7-r1-t740-cap/README.md new file mode 100644 index 0000000000..60e2306737 --- /dev/null +++ b/research/rank7-r1-t740-cap/README.md @@ -0,0 +1,177 @@ +# R1 words at their packing cap (T740): conditional κ = 0.001729152756004330934535 − 10⁻⁴⁶ − 10⁻⁷⁰ + +```text +Status / UTC update / priority revision: DONE (moment nomination; see "Scope") · 2026-10-16 · priority revision 6 · base main d8e0f83f +Concrete question and changed premise: PR3015's R1 restore edit keeps every helper width, window and the 91-buffer + namespace of PR2979, and its fixed-capacity cap certificate has the same optimal basis as PR2979's. So an allocation + that attains PR2979's cap also attains R1's. Can that be done literally? +Established result and evidence status: yes. A literal T740 allocation is ten lockstep copies of PR2979's T74 fill + (which PR3015 uses unchanged) plus 332 whole-role relocations. Its idle histogram is exactly 740 x the optimal basic + idle profile, and with the R1 words its exact root equals the R1 cap. Gains: about 1.5520e-9 over PR3021's released + headline (R1 + PR3018 packing) and 1.7825e-9 over PR3015. Packing only; author-checked (AI-assisted); not + maintainer-reviewed. +Public artifact URL + exact commit: this package (see the PR). +Next useful task: the complete T740 admission/outer release. Further gains need more word edits (R2, ...). +Active claim / expiry: released. +``` + +## Result + +| | κ (headline; each − 10⁻⁴⁶ − 10⁻⁷⁰) | words | T | packing | +|---|---|---|---:|---| +| PR #3015 (Jeremy Kothe) | 0.001729150973534224428695 | PR2979 + R1 | 74 | PR2979's fill, 1.78e-9 below the R1 cap | +| PR #3021 (Nick Petalas) | 0.001729151203983018442998 | PR2979 + R1 | 74 | PR3018's journal, 1.55e-9 below | +| **this package** | **0.001729152756004330934535** | **PR2979 + R1** | **740** | **attains the R1 cap** | + +- Exact gains are `1552021312491537/10^24` over PR3021 and `178247010650584/10^23` over PR3015 (CLAIM.json). +- The words are PR3015's two R1 words, used unchanged (`data/R1-WORD-*.json.gz`; provenance in VENDOR.json). + - Local profile per call: {1:2443, 2:707, 3:232, 4:108, 5:18, 8:8}. + - Width inventory: {4:26, 5:2, 6:16, 7:52, 8:99, 9:213}. + - 91 private buffers. +- The allocation has 740 replicas, 6,660 calls and 2,717,280 helper roles. +- Complete paid profile: {1:16441320, 2:4708620, 3:1594737, 4:719280, 5:137085, 8:53280, 48:281903}. +- Physical stock: 663,040 live + 408 helpers + 8 centres + 91 buffers + 2 guards = **663,549**. +- The exact root bracket [0.001729152756004330934535, 0.0017291527560043309345351] is exactly PR3015's certified R1 + cap. + +**Concurrent work.** Nick Petalas' [PR3024](https://github.com/CrocSwap/integer-mult-bounds/pull/3024) attains the same +kind of cap at T740 for PR2979's words without R1. It uses a 550-row journal on PR3018's fill. This package's 332 +relocations were found independently from PR2979's own fill; they reach the same idle histogram. PR3024 records the R1 +composition as a separate obligation, and that composition is what this package adds. + +## Why T740 and why it composes with R1 + +**Why T740.** On the optimal face (12 tight patterns), exact row multipliers fix three counts per replica: + +| pattern | count per replica | +|---|---| +| [9,9,9]@32 | 93/4 | +| [9,9,9,9,9]@48 | 1341/20 | +| []@48 | 7619/20 | + +- Since 1341 = 3²·149 is prime to 20, an integral optimum needs 20 | T. +- T740 is the first multiple of PR2917's T74 order with that property. +- At T74 the best integral mix is 1.55e-9 below the cap, which is where PR3021 sits. + +**Why it composes with R1.** R1 changes the local profile by −2H₁ + H₂ per call and nothing else that the allocation +reads: helper widths, entrances, endpoints, windows, order, dispatch and buffers are all unchanged. PR3015's R1 cap +certificate has the same 10-pattern basis and the same idle profile as PR2979's. `verify.py` re-derives: + +- the R1 providers from the words; +- the face counts and the optimality of every literal bin pattern; +- the equality of the root and the R1 cap. + +## Construction + +`lift.py` defines the allocation completely, in two steps. + +1. **Lift.** PR2979's literal T74 ORDER, DISPATCH and FILL (PR3015 uses them unchanged) are copied ten times in + lockstep, in Dugongue's PR2969 convention. With j = 0, …, 9: + - call (s, r) at time t → call (s, r + 74j) at time 10t + j; + - role (t, h, o, c, p, z) → role (10t + j, h, o + 74j, c, p, z). +2. **Relocate.** The roles in `allocation/RELOCATIONS.json` move to their listed bins, and the 263 touched bins are + repacked as compact prefixes. + +### What the relocations change + + 60 x [4,8,9,9,9,9]@48 -> 57 x [9,9,9,9,9]@48 + 3 x []@48 + 75 x [9,9,9]@32 -> 60 x [4,9,9,9]@32 + 15 x [8,8,8,8]@32 + +The displaced 4s and 8s are late, while almost all [9,9,9] bins close early. So each one travels along a chain of +same-width exchanges (`construction/plan_t740.py`, seeded greedy; `construction/CHAINS.json`): + +1. It enters an unlocked bin whose window contains its call. +2. It evicts a same-width role of an earlier call, which moves on in turn. + +Every intermediate bin keeps its pattern. In all, 332 roles move: 150 in step A, 45 in B, 80 in C, 12 in D and 45 in E. +The search reads only widths, windows and families, so the same relocations serve PR2979's words and R1's. + +## Verification + +Both registered commands use the standard library only, under Python 3.12. + +**`verify.py` (about 70 seconds)** checks: + +- **Pins.** + - Live pins of the PR2979 inputs on main. + - Vendored-file pins (VENDOR.json): exact PR heads, Git blob IDs and SHA-256. +- **Providers.** The R1 words re-derive the providers: + - widths identical to PR2979's registry; + - local profile = R1; + - 91 buffers. +- **Allocation.** The deterministic T740 rebuild has pinned canonical payload SHA-256. +- **Owner engine.** PR2979's vendored engine checks all 2,717,280 roles: + - windows, same-call families, capacities, masks and compact prefixes; + - the complete paid profile and the rank mass. +- **Physical stock.** 663,549. +- **Cap and optimal face.** + - PR3015's R1 cap certificate is re-verified with PR2979's `relax_exact.py`. + - Exact fixed face counts. + - The idle histogram is 740 × the basic optimum. + - Every bin pattern is tight. + - The root bracket equals the cap bracket. +- **Moment.** The dyadic moment auditor is re-pinned to PR3015's headline and shows a strict gain. An exact + comparison also shows a strict gain over PR3021. +- **Claim.** CLAIM.json is bound to the results. + +**`controls.py` (about four minutes)** checks seven controls: + +| control | result | +|---|---| +| bare lift | valid, but its root is PR3015's (below the cap) | +| dropped chain link | rejected by the engine | +| window violation | rejected by the engine | +| family collision | rejected by the engine | +| stale profile | rejected by the engine | +| tampered relocations | the payload pin fails | +| wrong moment baseline | rejected | + +```sh +python3 scripts/research_package.py --package research/rank7-r1-t740-cap --check-only +python3.12 scripts/research_package.py --package research/rank7-r1-t740-cap +python3 -B research/rank7-r1-t740-cap/construction/plan_t740.py --out /tmp/t740-plan # provenance: regenerates RELOCATIONS.json +``` + +## Scope + +- **Packing composed with R1.** No word, gate, frame, scalar or cleanup changes are made beyond PR3015's declared R1 + edit. +- **Inherited claims.** PR3015's (and PR2979's) word-level, native and release claims are inherited unchanged. So are + all of PR2979's inherited all-size, compiler, hosting, precision and analytic hypotheses. +- **Review status.** PR2979 is an archived source package and PR3015/PR3021 are open. None is scientifically admitted, + and the independent audits they need apply here too. +- **Open finite obligation.** The complete fresh-native admission and modern outer release have not yet been rerun for + the T740 allocation. PR3015's and PR3021's releases are at T74. This is a moment nomination with literal T740 owners, + the same status as PR3024 and PR2969. +- **What is not claimed.** No selected-frontier change, no new mechanism, and no independent human review. +- **Optimality.** The R1 cap is the optimum of the fixed-capacity relaxation, so no allocation of the R1 words in this + model can do better. + +## Open next questions + +1. **Complete T740 release.** + - First step: rerun PR3015's reproduce.py chain with the T740 ORDER/DISPATCH/FILL that `verify.py --work DIR` writes. + T-dependent physical and prefix constants come from the order. + - Blocked by: replay time and memory at ten times PR3015's 271,728 roles. +2. **More declared edits.** + - Why it matters: packing is exhausted for these words, so only a changed local profile raises κ further. + - First step: price candidate edits with PR3015's exhaustive 2-4-gate restore-block search. Each new local profile + with the same basis inherits this allocation's cap attainment. + +These are recorded as structured `open_questions` in TASK.json. + +## Credit + +- **Jeremy Kothe (PR #3015):** the declared R1 edit, R1 words and R1 cap certificate. +- **Marius-Paul Dumitrean (PR #2979):** the words under R1, the literal T74 fill lifted here and the checkers. +- **Nick Petalas (PR #3018, #3021, #3022, #3024):** the integrality analysis lineage and the concurrent T740 cap for + PR2979's words. +- **Dugongue (PR #2969):** the lockstep T-lift convention and cross-copy moves. +- **themilkman216:** the observation about the T at which these caps become integral. +- **Mason Hale (PR #2917):** chronology and owner/moment checks. +- **Tekalign:** the independent owner checker. +- **Jeremy Diviney (PR #2908):** the moment auditor arithmetic. +- **Yiyang Lu:** the flow model. +- **icekylinx:** the exact auditor. + +New work by Rohan Arun, prepared with substantial AI assistance (Anthropic Claude). Apache-2.0. Retained notices apply. diff --git a/research/rank7-r1-t740-cap/SOURCES.json b/research/rank7-r1-t740-cap/SOURCES.json new file mode 100644 index 0000000000..40dabf31f2 --- /dev/null +++ b/research/rank7-r1-t740-cap/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-joint-endframes/CLAIM.json", + "usage": "input", + "git_blob": "8ec2ce4e440c0b584ee982c551e526a011c9324c", + "sha256": "436e0d297cbdf195445d3697d496ac675e95210b79e70ce602a6a6667a4c6ce9" + }, + { + "path": "research/rank7-joint-endframes/allocation/DISPATCH.json", + "usage": "input", + "git_blob": "9544fee4e6ee1f202cee22bfaeaf229ee3b2515e", + "sha256": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c" + }, + { + "path": "research/rank7-joint-endframes/allocation/FILL.json.gz", + "usage": "input", + "git_blob": "8d4fd644d60ba2c98106dc770803b647afdf0963", + "sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39" + }, + { + "path": "research/rank7-joint-endframes/allocation/ORDER.json", + "usage": "input", + "git_blob": "7409c4df1092241729739596c7648bda504e6aad", + "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1" + }, + { + "path": "research/rank7-joint-endframes/allocation/PROVIDERS.json", + "usage": "input", + "git_blob": "e1d99e12cfa3ac8375984d85c0b040dc36ea1312", + "sha256": "f2edb7922f3029a5d607437e737775ff3371bca49ebab62e5e2495d16d3bf573" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "usage": "input", + "git_blob": "7a1db55a4d53ee99280be4f3ab7d29f7b2033adf", + "sha256": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "usage": "input", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/independent_owners.py", + "usage": "input", + "git_blob": "16013201b19054f7e45398ecf10af74c9c6a9114", + "sha256": "77a848729159e271ba64f403dfd59dddb13044b17b2950fa56700f442e2fe461" + }, + { + "path": "research/rank7-joint-endframes/tools/audit_allocation_moment.py", + "usage": "input", + "git_blob": "623ae14fbeaacf2f1b2302ae23b40c52586b7342", + "sha256": "c632527ecf092f013862660dbd7f52b599a50b321a8aa88ddc45af0547e79cb5" + }, + { + "path": "research/rank7-joint-endframes/tools/relax.py", + "usage": "input", + "git_blob": "97dfe35c434283ca6e83818e61aed65740522f50", + "sha256": "0fed1c56b50a2e6d44deeeb6db0f1c7e1f71b86d1747130e1a9202216249a728" + }, + { + "path": "research/rank7-joint-endframes/tools/relax_exact.py", + "usage": "input", + "git_blob": "0be97756bb9d8b072c962c147d4b4d3b3122f884", + "sha256": "baf1855d6095c951a90d19a0d8094bd33290519940b732e2b758c5647830f044" + }, + { + "path": "research/rank7-joint-endframes/tools/root.py", + "usage": "input", + "git_blob": "bd6dc2eb4e5013625d17cc08461b67622bcfed69", + "sha256": "55f5aca39b5ee2fe4687ac8863e6c24569010f27a332883c069b8e14b8fe09e3" + }, + { + "path": "research/rank7-joint-endframes/vendor/preload_move.py", + "usage": "input", + "git_blob": "55b435035bbc439a9d55e8abd125993208cef8d9", + "sha256": "c8fda4674644fcd5cbf39b6645ce148a21daa90a998b678cbe51f970b78b0044" + } + ] +} diff --git a/research/rank7-r1-t740-cap/TASK.json b/research/rank7-r1-t740-cap/TASK.json new file mode 100644 index 0000000000..c5c441ddac --- /dev/null +++ b/research/rank7-r1-t740-cap/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "selected-packing", + "priority_revision": 6, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "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" + ], + "existing_checks": [ + { + "scope": "Packing-independent ceiling for the selected paid profile under the one-unpaid-coordinate coverage and halving guard.", + "evidence": "docs/research/community-efficient1000-review.md", + "remaining": "A changed word or model requires new pricing; a local packing search must name uncovered scope.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "PR3015's R1 words (PR2979's words plus Jeremy Kothe's declared restore edit R1) with a literal T740 allocation attaining their fixed-capacity packing cap: ten lockstep copies of PR2979's literal T74 fill (used unchanged by PR3015; PR2969's lift convention) plus 332 explicit whole-role relocations along same-width exchange chains, putting the pattern mix on an integral point of the optimal face.", + "scope_change_reason": "The card targets the selected record's packing, whose ceiling is already reviewed. The live open question is the newest candidate's integrality gap: PR3015/PR3021 release R1 at T74, 1.78e-9/1.55e-9 below R1's certified cap, and the optimal face needs 20 | T. Bounded, packing-only composition with PR3015's declared edit, reported against the exact R1 cap (attained).", + "bottleneck_link": "Packing only: the paid local profile is PR3015's, so the gain is capped by R1's fixed-capacity relaxation; this attains it (+1.552e-9 over PR3021's released headline, +1.782e-9 over PR3015). It closes the packing layer for these words.", + "budget_minutes": 240, + "stop_rule": "Publish only if the R1 words re-derive the providers, PR2979's owner engine accepts the literal T740 allocation with the claimed complete profile, the idle histogram is exactly 740 x the optimal basic idle profile (root = R1 cap), and the re-pinned moment auditor shows a strict gain over PR3015 with an exact strict gain over PR3021; otherwise stop.", + "outcome": "completed", + "evidence": "verify.py (stdlib, about 70 s): live PR2979 input pins and vendored PR3015/PR3021 pins (heads, Git blobs, SHA-256); providers re-derived from the R1 words (PR2979 widths, R1 local profile, 91 buffers); deterministic T740 rebuild with pinned canonical payload SHA-256; owner engine over 2,717,280 roles; physical 663,549; R1 cap certificate re-verified; exact fixed face counts (20 | T); idle = 740 x basic optimum; all bin patterns tight; root bracket = R1 cap bracket; moment auditor re-pinned to PR3015 (strict gain); exact strict gain over PR3021. controls.py (stdlib, about 4 min): seven controls rejected or losing the gain.", + "author": "Rohan Arun", + "ai_assistance": "Substantial AI assistance (Anthropic Claude) for the analysis, search, implementation and checks; no independent human review is claimed.", + "open_questions": [ + { + "question": "Does the complete fresh-native admission and modern outer release pass for the T740 allocation with the R1 words?", + "why_it_matters": "PR3015/PR3021 release R1 only at T74; a T740 release would turn this moment nomination into a complete conditional candidate.", + "first_step": "Run PR3015's reproduce.py chain with the T740 ORDER/DISPATCH/FILL written by verify.py --work DIR, rederiving T-dependent physical/prefix constants from the order.", + "blocked_by": "Replay time and memory at ten times PR3015's 271,728 roles; no structural blocker is known." + }, + { + "question": "Which further declared edits (beyond R1) lower the local profile while keeping the same optimal basis?", + "why_it_matters": "Packing is exhausted for these words; a changed local profile with the same basis inherits this allocation's cap attainment at no packing cost.", + "first_step": "Rerun PR3015's exhaustive 2-4-gate restore-block search on the R1 words and screen each candidate's cap certificate basis.", + "blocked_by": "None known; the search tooling is in PR3015." + } + ] +} diff --git a/research/rank7-r1-t740-cap/VENDOR.json b/research/rank7-r1-t740-cap/VENDOR.json new file mode 100644 index 0000000000..681498fd0d --- /dev/null +++ b/research/rank7-r1-t740-cap/VENDOR.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "upstream_repository": "https://github.com/CrocSwap/integer-mult-bounds", + "files": [ + { + "pr": 3015, + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "path": "research/rank7-joint-endframes-restore-edit/edits/FINAL-WORD-base.json.gz", + "package_path": "data/R1-WORD-base.json.gz", + "git_blob": "4f0483657396a7f735873e1b252482c53dfb2eb6", + "sha256": "77d9be7ac47347894e034d8b67bf07ff8a5e1c317923ed5dd9257c492187dcf5", + "bytes": 71434, + "role": "PR3015 R1 base provider word (edit R1 on PR2979 words)", + "author": "Jeremy Kothe (jeremykothe2)" + }, + { + "pr": 3015, + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "path": "research/rank7-joint-endframes-restore-edit/edits/FINAL-WORD-extra.json.gz", + "package_path": "data/R1-WORD-extra.json.gz", + "git_blob": "81f95e21ede115e8bdb6bd522c641b37b740bdf7", + "sha256": "18d9c448ce892aa19f162e214760d0bd4ecb09f814b9b859dbf11f3ca637e9ea", + "bytes": 71430, + "role": "PR3015 R1 extra provider word", + "author": "Jeremy Kothe (jeremykothe2)" + }, + { + "pr": 3015, + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "path": "research/rank7-joint-endframes-restore-edit/certificates/RELAX-CAP.json", + "package_path": "certificates/R1-RELAX-CAP.json", + "git_blob": "41ec3a5f037dd64daade435a4c02468ecbdae524", + "sha256": "6380d23931bfcdf4bd2684dd19bb60db543f570bc88873f5effd53387beb28b0", + "bytes": 1760, + "role": "PR3015 Fractions-only fixed-capacity cap certificate of the R1 profile", + "author": "Jeremy Kothe (jeremykothe2)" + }, + { + "pr": 3015, + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "path": "research/rank7-joint-endframes-restore-edit/CLAIM.json", + "package_path": "comparators/PR3015-CLAIM.json", + "git_blob": "70813f559e2878f0c5403c0b859eefe602f70abc", + "sha256": "f9b9fbaaac794c0ce279c238a33a2f34f8c91a34d97ccdeb5ec98b7b8ba56d73", + "bytes": 7138, + "role": "PR3015 released headline (moment-auditor baseline)", + "author": "Jeremy Kothe (jeremykothe2)" + }, + { + "pr": 3015, + "head": "e244296debb45fe6f4da84d29e4d64fbab55fda0", + "path": "research/rank7-joint-endframes-restore-edit/allocation/PROFILE.json", + "package_path": "comparators/PR3015-PROFILE.json", + "git_blob": "05766f448600d2f94699f42818aa8150f49fd934", + "sha256": "5626c44edd6d5b209cd4e2d2a824e07bfba696e0856f3964b81fcb01c78eaad8", + "bytes": 104, + "role": "PR3015 literal T74 complete profile (moment-auditor baseline)", + "author": "Jeremy Kothe (jeremykothe2)" + }, + { + "pr": 3021, + "head": "217edac2ebfa6250536bd6df153de14901a69395", + "path": "research/rank7-restore-packing-composition/evidence/OUTER-CLAIM.json", + "package_path": "comparators/PR3021-OUTER-CLAIM.json", + "git_blob": "a8d657563624b98d8bb238878a6c20fa74a1f593", + "sha256": "8beb062c36169728a8f82a5eda6638c2a83125f16e7e5de56f3a13d9cba5e1f5", + "bytes": 2141, + "role": "PR3021 released headline (best open claim at submission)", + "author": "Nick Petalas (petalas)" + } + ] +} diff --git a/research/rank7-r1-t740-cap/VERIFY.json b/research/rank7-r1-t740-cap/VERIFY.json new file mode 100644 index 0000000000..620c2ffd85 --- /dev/null +++ b/research/rank7-r1-t740-cap/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-joint-endframes/CLAIM.json", + "research/rank7-joint-endframes/allocation/DISPATCH.json", + "research/rank7-joint-endframes/allocation/FILL.json.gz", + "research/rank7-joint-endframes/allocation/ORDER.json", + "research/rank7-joint-endframes/allocation/PROVIDERS.json", + "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "research/rank7-joint-endframes/allocation/vendor/independent_owners.py", + "research/rank7-joint-endframes/tools/audit_allocation_moment.py", + "research/rank7-joint-endframes/tools/relax.py", + "research/rank7-joint-endframes/tools/relax_exact.py", + "research/rank7-joint-endframes/tools/root.py", + "research/rank7-joint-endframes/vendor/preload_move.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 400, + "checks": "Live PR2979 input pins and vendored PR3015/PR3021 pins; providers re-derived from PR3015's R1 words; deterministic T740 rebuild (lift.py) with pinned canonical payload SHA-256; PR2979's vendored owner engine on all 2,717,280 roles with the claimed complete profile; physical stock 663,549; PR3015's R1 cap certificate re-verified; exact fixed counts on the optimal face (20 | T); idle histogram = 740 x optimal basic idle profile; every bin pattern tight; root bracket = R1 cap bracket; dyadic moment auditor re-pinned to PR3015's headline (strict gain); exact strict gain over PR3021; CLAIM.json binding." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/controls.py" + ], + "timeout_seconds": 600, + "checks": "Seven failure controls: bare lift (valid, PR3015's root, below the cap); dropped chain link, window violation, same-call family collision and stale profile rejected by the owner engine; tampered relocations fail the payload pin; wrong moment baseline rejected." + } + ] +} diff --git a/research/rank7-r1-t740-cap/allocation/EXPECTED.json b/research/rank7-r1-t740-cap/allocation/EXPECTED.json new file mode 100644 index 0000000000..6c00d2ee9d --- /dev/null +++ b/research/rank7-r1-t740-cap/allocation/EXPECTED.json @@ -0,0 +1,15 @@ +{ + "calls": 6660, + "payload_convention": "SHA-256 of json.dumps(obj, sort_keys=True, separators=(\",\", \":\")) + \"\\n\" (uncompressed), as lift.canonical", + "payload_sha256": { + "DISPATCH.json": "90edc935320dd6264e98dc735d868df3c95f5901c70d7d96171001fcb295cce0", + "FILL.json.gz": "b56bfed2c542e63f4139e8e3ebb9fe0c979a3bab1ba6a934e2113f40f5c7e0f0", + "ORDER.json": "927226d702bf3cada076f4c459da9063c0df7e7154a62955cf75c40cf30215b9", + "PROFILE.json": "83130e5231b3693c2af871c430833601de83fdd8851c024df4f78efc76c8deef" + }, + "physical": 663549, + "relocations": 332, + "replicas": 740, + "roles": 2717280, + "touched_bins": 263 +} diff --git a/research/rank7-r1-t740-cap/allocation/PROFILE.json b/research/rank7-r1-t740-cap/allocation/PROFILE.json new file mode 100644 index 0000000000..0345ea9df8 --- /dev/null +++ b/research/rank7-r1-t740-cap/allocation/PROFILE.json @@ -0,0 +1,9 @@ +{ + "1": 16443540, + "2": 4708620, + "3": 1594737, + "4": 719280, + "5": 137085, + "8": 53280, + "48": 281903 +} diff --git a/research/rank7-r1-t740-cap/allocation/RELOCATIONS.json b/research/rank7-r1-t740-cap/allocation/RELOCATIONS.json new file mode 100644 index 0000000000..81a0c2be3d --- /dev/null +++ b/research/rank7-r1-t740-cap/allocation/RELOCATIONS.json @@ -0,0 +1 @@ +[[500,53,407,4,3],[500,58,416,6,4],[500,69,302,4,90],[500,74,38,6,84],[500,83,704,6,56],[500,85,223,4,82],[500,90,482,4,68],[500,99,487,4,71],[500,101,372,6,68],[500,106,598,4,53],[500,113,120,4,100],[500,115,224,4,25],[500,117,520,6,30],[500,122,704,6,71],[500,129,712,6,10],[500,131,446,6,11],[500,133,298,6,45],[500,138,490,4,58],[500,145,342,6,17],[500,147,705,4,33],[500,149,305,6,6],[500,154,39,6,44],[500,161,593,6,75],[500,163,672,4,31],[500,165,2,4,1],[500,170,231,6,7],[501,129,601,6,76],[501,131,39,4,46],[501,133,631,6,45],[501,138,334,6,72],[501,145,75,6,25],[501,147,630,6,36],[501,149,446,6,34],[501,154,445,6,36],[501,161,712,6,37],[501,163,334,6,57],[501,165,379,4,5],[501,170,191,4,49],[1480,58,606,4,36],[1480,69,495,4,16],[1480,74,604,4,13],[1480,83,234,4,4],[1480,85,123,4,11],[1480,90,532,4,18],[1480,99,384,4,16],[1480,101,234,4,0],[1480,106,495,4,22],[1480,113,236,4,8],[1480,115,86,4,2],[1480,117,530,4,4],[1480,122,14,4,2],[1480,129,310,4,36],[1480,131,12,4,7],[1480,133,421,4,15],[1480,138,199,4,32],[3260,53,26,4,101],[3261,53,100,4,101],[3262,53,26,4,95],[3263,53,26,4,98],[3264,53,100,4,98],[3265,53,26,4,109],[3266,53,26,6,3],[3267,53,26,4,99],[3268,53,26,4,92],[3269,53,26,4,94],[3270,53,100,4,99],[3271,53,26,4,108],[3272,53,26,4,93],[3273,53,100,4,95],[3274,53,26,4,103],[3275,53,26,4,107],[3276,53,26,6,2],[3277,53,100,4,94],[3278,53,100,4,96],[3279,53,26,4,96],[3540,53,26,4,106],[3540,58,26,4,105],[3540,69,26,4,104],[3540,74,26,4,102],[3540,83,26,4,100],[3540,85,26,4,97],[3541,53,26,6,5],[3541,58,26,6,4],[3541,69,26,6,1],[3541,74,26,6,0],[3541,83,26,4,111],[3541,85,26,4,110],[3542,53,100,4,103],[3542,58,100,4,102],[3542,69,100,4,100],[3542,74,100,4,97],[3542,83,100,4,93],[3542,85,100,4,92],[4189,218,171,13,111],[4190,218,615,13,111],[4320,106,30,4,105],[4320,113,30,4,104],[4320,115,30,4,103],[4320,117,30,4,102],[4320,122,30,4,101],[4320,129,30,4,100],[4320,131,30,4,99],[4320,133,30,4,98],[4320,138,30,4,97],[4320,145,30,4,96],[4320,147,30,4,95],[4320,149,30,4,94],[4320,154,30,4,93],[4320,161,30,4,92],[4320,163,30,4,91],[4320,165,30,4,90],[4320,170,30,4,89],[4891,0,294,13,111],[4951,0,470,13,111],[4971,0,60,13,111],[4972,0,652,13,111],[4973,0,578,13,111],[4974,0,507,13,111],[4975,0,504,13,111],[4976,0,393,13,111],[4977,0,430,13,111],[4978,0,356,13,111],[4979,0,541,13,111],[5105,206,256,13,82],[5106,206,256,13,82],[5107,206,256,13,82],[5108,206,256,13,82],[5109,206,256,13,82],[5110,206,315,12,17],[5111,206,315,12,17],[5112,206,315,12,17],[5113,206,315,12,17],[5114,206,315,12,17],[5115,206,540,12,3],[5116,206,540,12,3],[5117,206,540,12,3],[5118,206,540,12,3],[5119,206,540,12,3],[5165,12,329,8,20],[5166,12,329,8,20],[5167,12,329,8,20],[5168,12,329,8,20],[5169,12,329,8,20],[5170,12,647,12,86],[5171,12,647,12,86],[5172,12,647,12,86],[5173,12,647,12,86],[5174,12,647,12,86],[5175,12,92,12,81],[5176,12,92,12,81],[5177,12,92,12,81],[5178,12,92,12,81],[5179,12,92,12,81],[5305,0,622,10,83],[5306,0,622,10,83],[5307,0,622,10,83],[5308,0,622,10,83],[5309,0,622,10,83],[5310,0,464,12,101],[5311,0,464,12,101],[5312,0,464,12,101],[5313,0,464,12,101],[5314,0,464,12,101],[5315,0,244,13,88],[5316,0,244,13,88],[5317,0,244,13,88],[5318,0,244,13,88],[5319,0,244,13,88],[5369,66,331,13,111],[5370,66,208,13,111],[5391,0,245,13,111],[5491,0,97,13,111],[5492,0,319,13,111],[5493,0,282,13,111],[5494,0,322,13,111],[5495,0,467,13,111],[5496,0,581,13,111],[5497,0,134,13,111],[5498,0,359,13,111],[5499,0,23,13,111],[5540,74,167,15,54],[5541,74,93,15,55],[5542,74,19,15,58],[5543,74,167,15,58],[5544,74,167,15,53],[5545,74,19,15,54],[5546,74,19,15,53],[5547,74,93,15,56],[5548,74,19,15,56],[5549,74,26,14,0],[5550,74,174,14,0],[5551,74,167,15,57],[5552,74,93,15,53],[5553,74,167,15,55],[5554,74,19,15,57],[5555,74,167,15,56],[5556,74,93,15,58],[5557,74,93,15,54],[5558,74,93,15,57],[5559,74,19,15,55],[5580,2,729,14,0],[5581,2,655,14,0],[5582,2,581,14,0],[5583,2,581,14,0],[5584,2,581,14,0],[5585,2,359,14,0],[5586,2,285,14,0],[5587,2,285,14,0],[5588,2,211,14,0],[5589,2,137,14,0],[5590,2,63,14,0],[5591,2,63,14,0],[5592,2,692,14,0],[5593,2,618,14,0],[5594,2,618,14,0],[5595,2,544,14,0],[5596,2,470,14,0],[5597,2,470,14,0],[5598,2,470,14,0],[5599,2,396,14,0],[5689,340,627,13,111],[5690,340,72,13,111],[5720,406,692,14,0],[5720,407,433,14,0],[5721,406,211,14,0],[5721,407,396,14,0],[5722,406,359,14,0],[5722,407,655,14,0],[5723,406,396,14,0],[5723,407,507,14,0],[5724,406,692,14,0],[5724,407,544,14,0],[5725,406,507,14,0],[5725,407,285,14,0],[5726,406,507,14,0],[5726,407,137,14,0],[5727,406,137,14,0],[5727,407,507,14,0],[5728,406,433,14,0],[5728,407,729,14,0],[5729,406,729,14,0],[5729,407,655,14,0],[5730,406,729,14,0],[5730,407,544,14,0],[5731,406,396,14,0],[5731,407,285,14,0],[5732,406,211,14,0],[5732,407,655,14,0],[5733,406,544,14,0],[5733,407,618,14,0],[5734,406,359,14,0],[5734,407,433,14,0],[5735,406,470,14,0],[5735,407,359,14,0],[5736,406,63,14,0],[5736,407,137,14,0],[5737,406,211,14,0],[5737,407,692,14,0],[5738,406,63,14,0],[5738,407,618,14,0],[5739,406,433,14,0],[5739,407,581,14,0],[5909,0,726,13,111],[5910,0,689,13,111],[6000,165,23,15,8],[6001,165,23,15,5],[6002,165,23,15,12],[6003,165,23,15,14],[6004,165,322,14,0],[6005,165,23,15,18],[6006,165,23,15,9],[6007,165,23,15,13],[6008,165,23,15,3],[6009,165,23,15,19],[6010,165,100,14,0],[6011,165,248,14,0],[6012,165,23,15,6],[6013,165,23,15,4],[6014,165,23,15,15],[6015,165,23,15,11],[6016,165,23,15,16],[6017,165,23,15,17],[6018,165,23,15,7],[6019,165,23,15,10],[6151,340,137,13,111],[6152,340,590,13,111],[6153,340,285,13,111],[6154,340,26,13,111],[6155,340,655,13,111],[6156,340,100,13,111],[6157,340,211,13,111],[6158,340,174,13,111],[6159,340,729,13,111],[6191,340,248,13,111],[6192,340,433,13,111],[6193,340,368,13,111],[6194,340,553,13,111],[6195,340,442,13,111],[6196,340,544,13,111],[6197,340,35,13,111],[6198,340,220,13,111],[6199,340,618,13,111],[6251,1,396,13,111],[6460,385,623,14,0],[6461,385,401,14,0],[6462,385,216,14,0],[6463,385,364,14,0],[6464,385,179,14,0],[6465,385,660,14,0],[6466,385,697,14,0],[6467,385,290,14,0],[6468,385,253,14,0],[6469,385,734,14,0],[6470,385,105,14,0],[6471,385,31,14,0],[6472,385,475,14,0],[6473,385,327,14,0],[6474,385,438,14,0],[6475,385,142,14,0],[6476,385,512,14,0],[6477,385,586,14,0],[6478,385,549,14,0],[6479,385,68,14,0],[6611,1,701,13,111],[6612,1,405,13,111],[6613,1,516,13,111],[6614,1,257,13,111],[6615,1,183,13,111],[6616,1,738,13,111],[6617,1,479,13,111],[6618,1,664,13,111],[6619,1,109,13,111]] diff --git a/research/rank7-r1-t740-cap/certificates/R1-RELAX-CAP.json b/research/rank7-r1-t740-cap/certificates/R1-RELAX-CAP.json new file mode 100644 index 0000000000..41ec3a5f03 --- /dev/null +++ b/research/rank7-r1-t740-cap/certificates/R1-RELAX-CAP.json @@ -0,0 +1,124 @@ +{ + "basis_patterns": [ + { + "capacity": 8, + "count_per_replica": "672", + "widths": [ + 8 + ] + }, + { + "capacity": 32, + "count_per_replica": "115/4", + "widths": [ + 7, + 8, + 8, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "234", + "widths": [ + 4, + 9, + 9, + 9 + ] + }, + { + "capacity": 48, + "count_per_replica": "1341/20", + "widths": [ + 9, + 9, + 9, + 9, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "93/4", + "widths": [ + 9, + 9, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "144", + "widths": [ + 6, + 8, + 9, + 9 + ] + }, + { + "capacity": 32, + "count_per_replica": "18", + "widths": [ + 5, + 9, + 9, + 9 + ] + }, + { + "capacity": 16, + "count_per_replica": "35/4", + "widths": [ + 8, + 8 + ] + }, + { + "capacity": 16, + "count_per_replica": "1757/4", + "widths": [ + 7, + 9 + ] + }, + { + "capacity": 48, + "count_per_replica": "7619/20", + "widths": [] + } + ], + "cap_lower": "345830551200866186907/200000000000000000000000", + "cap_lower_decimal": "0.001729152756004330934535", + "cap_upper": "17291527560043309345351/10000000000000000000000000", + "cap_upper_decimal": "0.0017291527560043309345351", + "idle_per_replica": { + "1": "234", + "3": "1341/20", + "48": "7619/20", + "5": "93/4" + }, + "inventory_per_call": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + }, + "local_per_call": { + "1": 2443, + "2": 707, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "patterns": 2551, + "rank_mass_identity": true, + "scenario": "final words of PR2979 plus declared restore edit list (R1, Stack2979)", + "status": "PASS_EXACT_RELAXATION_CAP", + "strict_patterns": 2539, + "tight_patterns": 12 +} diff --git a/research/rank7-r1-t740-cap/comparators/PR3015-CLAIM.json b/research/rank7-r1-t740-cap/comparators/PR3015-CLAIM.json new file mode 100644 index 0000000000..70813f559e --- /dev/null +++ b/research/rank7-r1-t740-cap/comparators/PR3015-CLAIM.json @@ -0,0 +1,229 @@ +{ + "admitted_package_manifest_sha256": "75a1536a7eaafa59c553d62c0ec8ce9a0b68f7365ecadea590ab85c7a78e0c1b", + "baseline_head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3", + "baseline_kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "baseline_pr": 2969, + "baseline_status": "FINITE_NATIVE_OWNER_AND_MOMENT_CANDIDATE_OUTER_PENDING", + "calls": 666, + "complex_lower": "345830194706844885739/200000000000000000000000", + "declared_edits": { + "count": 1, + "edits_sha256": "c9c68660d07bfd12ed20fd8cbfe3d36301ceb2d7bb9b4ea11350cc399b19e0b1", + "previous_kappa": "0.0017290339826465135177169999999999999999999998999999999999999999999999", + "previous_pr": 2979 + }, + "fill_sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "fixed_inventory_cap": { + "cap_lower": "345830551200866186907/200000000000000000000000", + "cap_upper": "17291527560043309345351/10000000000000000000000000", + "realized": "below the fractional optimum by the recorded gap (check_cap.py); the cap basis is fractional at T74" + }, + "gain": "1023149757223910029/200000000000000000000000", + "helpers": 408, + "independent_inputs": 632, + "kappa": "17291509735342244286949999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017291509735342244286949999999999999999999998999999999999999999999999", + "live_families": 66304, + "local_profile": { + "1": 2443, + "2": 707, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "native_receipt_sha256": "bc03c643a2209ec74f6efe9f74c29d7a1836b1be4b6bfe6e9ee5f3d82c01d19c", + "physical_families": 66813, + "previous_claims": { + "pr2942": { + "claim_file": "comparators/PR2942-CLAIM.json", + "gain": "6334653671010100699/1000000000000000000000000", + "head": "a027b0f6fdb0ab2b42ba10fc31b53960166bf2bf", + "kappa": "17228163198632143279959999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2942 + }, + "pr2957": { + "claim_file": "comparators/PR2957-CLAIM.json", + "gain": "1358389615871564431/250000000000000000000000", + "head": "b74b25f3ccc84c16e1a801d73b2f47e5ea764c78", + "kappa": "17237174150707381709709999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2957 + }, + "pr2966": { + "claim_file": "comparators/PR2966-CLAIM.json", + "gain": "5116701010772251283/1000000000000000000000000", + "head": "e62d3eb9005117d82a9babcfa937ecc53237c490", + "kappa": "17240342725234521774119999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2966 + }, + "pr2969": { + "claim_file": "allocation/baseline/CLAIM.json", + "gain": "1023149757223910029/200000000000000000000000", + "head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3", + "kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2969 + }, + "pr2979": { + "claim_file": "comparators/PR2979-CLAIM.json", + "gain": "58495443855455489/500000000000000000000000", + "head": "be191346391661f4d35fc0d1508d0a6029572576", + "kappa": "17290339826465135177169999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "pr": 2979 + } + }, + "profile": { + "1": 1644348, + "2": 470862, + "3": 159468, + "4": 71928, + "48": 28190, + "5": 13716, + "8": 5328 + }, + "release_receipt_sha256": "f6ddfdbbdd343cfd0a11e1d7b00cb9a8a6fbc9c7a64159b0d5abaf7de88cecf2", + "replicas": 74, + "scope": "Conditional finite supplier/outer certificate for PR2979's words (mdumitrean: joint rank-7 end frames, five further paired extractions, fourteen PR2957 rewrites) with one declared literal restore edit (R1, Stack2979 / Jeremy Kothe) and PR2979's literal T74 allocation unchanged (paid profile re-derived). Inherited all-size/compiler/theorem hypotheses remain. No selected-frontier change or independent-human-review claim.", + "source_manifest_sha256": "9215312229c431078ba61daf106edb8caf20b33f48317d46438a341552cf153f", + "stages": { + "stage1": { + "frame_edits": 139, + "groups": { + "A": { + "W": [ + 256, + 128, + 64, + 38, + 20, + 10, + 1 + ], + "helpers": [ + 331, + 450, + 451, + 508, + 509 + ] + }, + "B": { + "W": [ + 256, + 128, + 64, + 34, + 17, + 11, + 4 + ], + "helpers": [ + 299, + 448, + 449, + 484, + 485 + ] + }, + "C": { + "W": [ + 256, + 128, + 64, + 32, + 19, + 11, + 6 + ], + "helpers": [ + 452, + 453, + 532, + 533 + ] + }, + "D": { + "W": [ + 256, + 128, + 64, + 37, + 21, + 8, + 3 + ], + "helpers": [ + 454, + 455, + 556, + 557 + ] + }, + "V45": { + "W": [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + "helpers": [ + 249, + 251, + 265, + 267 + ] + } + }, + "kind": "joint codimension-2 end-frame lowering (frame-only)", + "record_sha256": "5fbfce004330ebc1fbac8de264614fe295f1a074811b478db4892c3bc3852cd3" + }, + "stage2": { + "extractions": [ + { + "helper": 226, + "normal": 42, + "step": 1 + }, + { + "helper": 228, + "normal": 42, + "step": 2 + }, + { + "helper": 230, + "normal": 42, + "step": 3 + }, + { + "helper": 363, + "normal": 7, + "step": 4 + }, + { + "helper": 395, + "normal": 7, + "step": 5 + } + ], + "kind": "rank-8 paired input/output extractions" + }, + "stage3": { + "applier_sha256": "2509f1335e47543f8814b42d6bf83032b30c5899b4f7cc62a6adc03f5138ae13", + "count": 14, + "kind": "declared exactness-preserving gate rewrites (Jeremy Kothe, PR2957), re-addressed", + "rewrites_sha256": "a37ade675876e4f5b00b33066c84f495fccd264863b7eb5d813837b1d01c3e7d" + } + }, + "status": "CONDITIONAL_CANDIDATE_COMPLETE_FINITE_RELEASE", + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + }, + "zero_buffers": 91 +} diff --git a/research/rank7-r1-t740-cap/comparators/PR3015-PROFILE.json b/research/rank7-r1-t740-cap/comparators/PR3015-PROFILE.json new file mode 100644 index 0000000000..05766f4486 --- /dev/null +++ b/research/rank7-r1-t740-cap/comparators/PR3015-PROFILE.json @@ -0,0 +1,9 @@ +{ + "1": 1644348, + "2": 470862, + "3": 159468, + "4": 71928, + "5": 13716, + "8": 5328, + "48": 28190 +} \ No newline at end of file diff --git a/research/rank7-r1-t740-cap/comparators/PR3021-OUTER-CLAIM.json b/research/rank7-r1-t740-cap/comparators/PR3021-OUTER-CLAIM.json new file mode 100644 index 0000000000..a8d6575636 --- /dev/null +++ b/research/rank7-r1-t740-cap/comparators/PR3021-OUTER-CLAIM.json @@ -0,0 +1,13 @@ +{ + "b": "certified complex_lower - 1e-104 (outer/B.json)", + "baseline_head": "e2ca469b08385d3d5e29a918d66dbefaf889e9f3", + "baseline_kappa": "17240352247481048785499999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "branch": "fine source-prime padding (PR1786, chafreaky; Trudgian's prime theorem; vendor/pr1786) with the gauge-free interiors (PR1758), the radix-distributed union schedule with per-visit tag work and the explicit Strassen boundary (tau=45/16); epsilon=1-1.0009765625e-3080 is a free parameter (outer/FINE-PADDING-COMPOSITION.md): kappa = C - 1/F - B, the fixed-grid maximum (epsilon q is 1.70e-3083 below q); the structured boundary of the previous package is not used; omega_C<=9/4 not used; recertified endpoint: the supplier native endpoint is certified to 1e-3000 (accept at the endpoint, reject at endpoint + 1e-3000, repaired fine engines in integer fixed point), and all free slacks are 1e-3080 or below", + "fixed_grid_maximum": "kappa=C-10^-70-10^-46 exactly; same fixed-grid-maximum proof at precision24.", + "gain": "159874351091048889/31250000000000000000000", + "kappa": "0.0017291512039830184429979999999999999999999998999999999999999999999999", + "kappa_rational": "17291512039830184429979999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "outer": "PR1673 capped phase-cell fusion (Vlado Vojdanovski)", + "retuned_slacks": "Endpoint precision24; free gaps follow outer/check_ledger.py from the frozen SPEC.", + "supplier": "PR1661 T74 pivot-566 stack with PR2226 anticipatory dirty borrowing, the PR2312 width exchange, frame refit and kernels, the PR2322 handoffs, the PR2435/PR2447 entrance raise, the PR2436 lifted-target aliases, and the PR2530 (zxv) eight source-partner aliases with an owner fill evacuated by the PR2559 (philippeVV) method; this package: six pre-life hostings (cold hosts 273, 275, 289, 291, 305, 321 host helpers 482, 483, 494, 495, 507, 519), a one-gate frame refit with the retired-lender alias 653<-563, and a new exact owner fill" +} diff --git a/research/rank7-r1-t740-cap/construction/CHAINS.json b/research/rank7-r1-t740-cap/construction/CHAINS.json new file mode 100644 index 0000000000..aeb5c0e8ae --- /dev/null +++ b/research/rank7-r1-t740-cap/construction/CHAINS.json @@ -0,0 +1 @@ +[{"step":"A","kind":"out","role":[5550,74],"bin":[63,13,111],"width":4},{"step":"A:end","kind":"in","role":[5550,74],"bin":[174,14,0],"width":4},{"step":"A","kind":"out","role":[5549,74],"bin":[692,13,111],"width":4},{"step":"A:end","kind":"in","role":[5549,74],"bin":[26,14,0],"width":4},{"step":"A","kind":"out","role":[6011,165],"bin":[146,13,111],"width":4},{"step":"A:end","kind":"in","role":[6011,165],"bin":[248,14,0],"width":4},{"step":"A","kind":"out","role":[3268,53],"bin":[615,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,170],"bin":[26,4,92],"width":4},{"step":"A:hop0","kind":"in","role":[3268,53],"bin":[26,4,92],"width":4},{"step":"A:end","kind":"in","role":[500,170],"bin":[231,6,7],"width":4},{"step":"A","kind":"out","role":[3272,53],"bin":[208,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,165],"bin":[26,4,93],"width":4},{"step":"A:hop0","kind":"in","role":[3272,53],"bin":[26,4,93],"width":4},{"step":"A:end","kind":"in","role":[500,165],"bin":[2,4,1],"width":4},{"step":"A","kind":"out","role":[6010,165],"bin":[72,13,111],"width":4},{"step":"A:end","kind":"in","role":[6010,165],"bin":[100,14,0],"width":4},{"step":"A","kind":"out","role":[3269,53],"bin":[689,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,163],"bin":[26,4,94],"width":4},{"step":"A:hop0","kind":"in","role":[3269,53],"bin":[26,4,94],"width":4},{"step":"A:end","kind":"in","role":[500,163],"bin":[672,4,31],"width":4},{"step":"A","kind":"out","role":[3262,53],"bin":[171,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,161],"bin":[26,4,95],"width":4},{"step":"A:hop0","kind":"in","role":[3262,53],"bin":[26,4,95],"width":4},{"step":"A:end","kind":"in","role":[500,161],"bin":[593,6,75],"width":4},{"step":"A","kind":"out","role":[6004,165],"bin":[331,13,111],"width":4},{"step":"A:end","kind":"in","role":[6004,165],"bin":[322,14,0],"width":4},{"step":"A","kind":"out","role":[6008,165],"bin":[627,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,170],"bin":[23,15,3],"width":4},{"step":"A:hop0","kind":"in","role":[6008,165],"bin":[23,15,3],"width":4},{"step":"A:hop1","kind":"out","role":[1480,138],"bin":[30,4,89],"width":4},{"step":"A:hop1","kind":"in","role":[4320,170],"bin":[30,4,89],"width":4},{"step":"A:end","kind":"in","role":[1480,138],"bin":[199,4,32],"width":4},{"step":"A","kind":"out","role":[3279,53],"bin":[726,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,154],"bin":[26,4,96],"width":4},{"step":"A:hop0","kind":"in","role":[3279,53],"bin":[26,4,96],"width":4},{"step":"A:end","kind":"in","role":[500,154],"bin":[39,6,44],"width":4},{"step":"A","kind":"out","role":[6013,165],"bin":[294,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,165],"bin":[23,15,4],"width":4},{"step":"A:hop0","kind":"in","role":[6013,165],"bin":[23,15,4],"width":4},{"step":"A:hop1","kind":"out","role":[1480,133],"bin":[30,4,90],"width":4},{"step":"A:hop1","kind":"in","role":[4320,165],"bin":[30,4,90],"width":4},{"step":"A:end","kind":"in","role":[1480,133],"bin":[421,4,15],"width":4},{"step":"A","kind":"out","role":[5546,74],"bin":[470,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3540,85],"bin":[19,15,53],"width":4},{"step":"A:hop0","kind":"in","role":[5546,74],"bin":[19,15,53],"width":4},{"step":"A:hop1","kind":"out","role":[500,149],"bin":[26,4,97],"width":4},{"step":"A:hop1","kind":"in","role":[3540,85],"bin":[26,4,97],"width":4},{"step":"A:end","kind":"in","role":[500,149],"bin":[305,6,6],"width":4},{"step":"A","kind":"out","role":[3263,53],"bin":[245,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,147],"bin":[26,4,98],"width":4},{"step":"A:hop0","kind":"in","role":[3263,53],"bin":[26,4,98],"width":4},{"step":"A:end","kind":"in","role":[500,147],"bin":[705,4,33],"width":4},{"step":"A","kind":"out","role":[3267,53],"bin":[541,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,145],"bin":[26,4,99],"width":4},{"step":"A:hop0","kind":"in","role":[3267,53],"bin":[26,4,99],"width":4},{"step":"A:end","kind":"in","role":[500,145],"bin":[342,6,17],"width":4},{"step":"A","kind":"out","role":[5545,74],"bin":[396,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3540,83],"bin":[19,15,54],"width":4},{"step":"A:hop0","kind":"in","role":[5545,74],"bin":[19,15,54],"width":4},{"step":"A:hop1","kind":"out","role":[500,138],"bin":[26,4,100],"width":4},{"step":"A:hop1","kind":"in","role":[3540,83],"bin":[26,4,100],"width":4},{"step":"A:end","kind":"in","role":[500,138],"bin":[490,4,58],"width":4},{"step":"A","kind":"out","role":[3260,53],"bin":[23,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,133],"bin":[26,4,101],"width":4},{"step":"A:hop0","kind":"in","role":[3260,53],"bin":[26,4,101],"width":4},{"step":"A:end","kind":"in","role":[500,133],"bin":[298,6,45],"width":4},{"step":"A","kind":"out","role":[5559,74],"bin":[729,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3540,74],"bin":[19,15,55],"width":4},{"step":"A:hop0","kind":"in","role":[5559,74],"bin":[19,15,55],"width":4},{"step":"A:hop1","kind":"out","role":[500,131],"bin":[26,4,102],"width":4},{"step":"A:hop1","kind":"in","role":[3540,74],"bin":[26,4,102],"width":4},{"step":"A:end","kind":"in","role":[500,131],"bin":[446,6,11],"width":4},{"step":"A","kind":"out","role":[3274,53],"bin":[356,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,129],"bin":[26,4,103],"width":4},{"step":"A:hop0","kind":"in","role":[3274,53],"bin":[26,4,103],"width":4},{"step":"A:end","kind":"in","role":[500,129],"bin":[712,6,10],"width":4},{"step":"A","kind":"out","role":[5548,74],"bin":[618,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3540,69],"bin":[19,15,56],"width":4},{"step":"A:hop0","kind":"in","role":[5548,74],"bin":[19,15,56],"width":4},{"step":"A:hop1","kind":"out","role":[500,122],"bin":[26,4,104],"width":4},{"step":"A:hop1","kind":"in","role":[3540,69],"bin":[26,4,104],"width":4},{"step":"A:end","kind":"in","role":[500,122],"bin":[704,6,71],"width":4},{"step":"A","kind":"out","role":[5554,74],"bin":[359,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3540,58],"bin":[19,15,57],"width":4},{"step":"A:hop0","kind":"in","role":[5554,74],"bin":[19,15,57],"width":4},{"step":"A:hop1","kind":"out","role":[500,117],"bin":[26,4,105],"width":4},{"step":"A:hop1","kind":"in","role":[3540,58],"bin":[26,4,105],"width":4},{"step":"A:end","kind":"in","role":[500,117],"bin":[520,6,30],"width":4},{"step":"A","kind":"out","role":[5542,74],"bin":[174,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3540,53],"bin":[19,15,58],"width":4},{"step":"A:hop0","kind":"in","role":[5542,74],"bin":[19,15,58],"width":4},{"step":"A:hop1","kind":"out","role":[500,115],"bin":[26,4,106],"width":4},{"step":"A:hop1","kind":"in","role":[3540,53],"bin":[26,4,106],"width":4},{"step":"A:end","kind":"in","role":[500,115],"bin":[224,4,25],"width":4},{"step":"A","kind":"out","role":[3275,53],"bin":[430,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,113],"bin":[26,4,107],"width":4},{"step":"A:hop0","kind":"in","role":[3275,53],"bin":[26,4,107],"width":4},{"step":"A:end","kind":"in","role":[500,113],"bin":[120,4,100],"width":4},{"step":"A","kind":"out","role":[6001,165],"bin":[109,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,163],"bin":[23,15,5],"width":4},{"step":"A:hop0","kind":"in","role":[6001,165],"bin":[23,15,5],"width":4},{"step":"A:hop1","kind":"out","role":[1480,131],"bin":[30,4,91],"width":4},{"step":"A:hop1","kind":"in","role":[4320,163],"bin":[30,4,91],"width":4},{"step":"A:end","kind":"in","role":[1480,131],"bin":[12,4,7],"width":4},{"step":"A","kind":"out","role":[6012,165],"bin":[220,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,161],"bin":[23,15,6],"width":4},{"step":"A:hop0","kind":"in","role":[6012,165],"bin":[23,15,6],"width":4},{"step":"A:hop1","kind":"out","role":[1480,129],"bin":[30,4,92],"width":4},{"step":"A:hop1","kind":"in","role":[4320,161],"bin":[30,4,92],"width":4},{"step":"A:end","kind":"in","role":[1480,129],"bin":[310,4,36],"width":4},{"step":"A","kind":"out","role":[6018,165],"bin":[664,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,154],"bin":[23,15,7],"width":4},{"step":"A:hop0","kind":"in","role":[6018,165],"bin":[23,15,7],"width":4},{"step":"A:hop1","kind":"out","role":[1480,122],"bin":[30,4,93],"width":4},{"step":"A:hop1","kind":"in","role":[4320,154],"bin":[30,4,93],"width":4},{"step":"A:end","kind":"in","role":[1480,122],"bin":[14,4,2],"width":4},{"step":"A","kind":"out","role":[3271,53],"bin":[134,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,106],"bin":[26,4,108],"width":4},{"step":"A:hop0","kind":"in","role":[3271,53],"bin":[26,4,108],"width":4},{"step":"A:end","kind":"in","role":[500,106],"bin":[598,4,53],"width":4},{"step":"A","kind":"out","role":[3265,53],"bin":[393,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,101],"bin":[26,4,109],"width":4},{"step":"A:hop0","kind":"in","role":[3265,53],"bin":[26,4,109],"width":4},{"step":"A:end","kind":"in","role":[500,101],"bin":[372,6,68],"width":4},{"step":"A","kind":"out","role":[5552,74],"bin":[211,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3541,85],"bin":[93,15,53],"width":4},{"step":"A:hop0","kind":"in","role":[5552,74],"bin":[93,15,53],"width":4},{"step":"A:hop1","kind":"out","role":[500,99],"bin":[26,4,110],"width":4},{"step":"A:hop1","kind":"in","role":[3541,85],"bin":[26,4,110],"width":4},{"step":"A:end","kind":"in","role":[500,99],"bin":[487,4,71],"width":4},{"step":"A","kind":"out","role":[6000,165],"bin":[35,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,149],"bin":[23,15,8],"width":4},{"step":"A:hop0","kind":"in","role":[6000,165],"bin":[23,15,8],"width":4},{"step":"A:hop1","kind":"out","role":[1480,117],"bin":[30,4,94],"width":4},{"step":"A:hop1","kind":"in","role":[4320,149],"bin":[30,4,94],"width":4},{"step":"A:end","kind":"in","role":[1480,117],"bin":[530,4,4],"width":4},{"step":"A","kind":"out","role":[5557,74],"bin":[581,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3541,83],"bin":[93,15,54],"width":4},{"step":"A:hop0","kind":"in","role":[5557,74],"bin":[93,15,54],"width":4},{"step":"A:hop1","kind":"out","role":[500,90],"bin":[26,4,111],"width":4},{"step":"A:hop1","kind":"in","role":[3541,83],"bin":[26,4,111],"width":4},{"step":"A:end","kind":"in","role":[500,90],"bin":[482,4,68],"width":4},{"step":"A","kind":"out","role":[5541,74],"bin":[100,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3541,74],"bin":[93,15,55],"width":4},{"step":"A:hop0","kind":"in","role":[5541,74],"bin":[93,15,55],"width":4},{"step":"A:hop1","kind":"out","role":[500,85],"bin":[26,6,0],"width":4},{"step":"A:hop1","kind":"in","role":[3541,74],"bin":[26,6,0],"width":4},{"step":"A:end","kind":"in","role":[500,85],"bin":[223,4,82],"width":4},{"step":"A","kind":"out","role":[5547,74],"bin":[544,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3541,69],"bin":[93,15,56],"width":4},{"step":"A:hop0","kind":"in","role":[5547,74],"bin":[93,15,56],"width":4},{"step":"A:hop1","kind":"out","role":[500,83],"bin":[26,6,1],"width":4},{"step":"A:hop1","kind":"in","role":[3541,69],"bin":[26,6,1],"width":4},{"step":"A:end","kind":"in","role":[500,83],"bin":[704,6,56],"width":4},{"step":"A","kind":"out","role":[3276,53],"bin":[504,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,74],"bin":[26,6,2],"width":4},{"step":"A:hop0","kind":"in","role":[3276,53],"bin":[26,6,2],"width":4},{"step":"A:end","kind":"in","role":[500,74],"bin":[38,6,84],"width":4},{"step":"A","kind":"out","role":[6006,165],"bin":[479,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,147],"bin":[23,15,9],"width":4},{"step":"A:hop0","kind":"in","role":[6006,165],"bin":[23,15,9],"width":4},{"step":"A:hop1","kind":"out","role":[1480,115],"bin":[30,4,95],"width":4},{"step":"A:hop1","kind":"in","role":[4320,147],"bin":[30,4,95],"width":4},{"step":"A:end","kind":"in","role":[1480,115],"bin":[86,4,2],"width":4},{"step":"A","kind":"out","role":[3266,53],"bin":[467,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[500,69],"bin":[26,6,3],"width":4},{"step":"A:hop0","kind":"in","role":[3266,53],"bin":[26,6,3],"width":4},{"step":"A:end","kind":"in","role":[500,69],"bin":[302,4,90],"width":4},{"step":"A","kind":"out","role":[6019,165],"bin":[738,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,145],"bin":[23,15,10],"width":4},{"step":"A:hop0","kind":"in","role":[6019,165],"bin":[23,15,10],"width":4},{"step":"A:hop1","kind":"out","role":[1480,113],"bin":[30,4,96],"width":4},{"step":"A:hop1","kind":"in","role":[4320,145],"bin":[30,4,96],"width":4},{"step":"A:end","kind":"in","role":[1480,113],"bin":[236,4,8],"width":4},{"step":"A","kind":"out","role":[5558,74],"bin":[655,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3541,58],"bin":[93,15,57],"width":4},{"step":"A:hop0","kind":"in","role":[5558,74],"bin":[93,15,57],"width":4},{"step":"A:hop1","kind":"out","role":[500,58],"bin":[26,6,4],"width":4},{"step":"A:hop1","kind":"in","role":[3541,58],"bin":[26,6,4],"width":4},{"step":"A:end","kind":"in","role":[500,58],"bin":[416,6,4],"width":4},{"step":"A","kind":"out","role":[6015,165],"bin":[442,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,138],"bin":[23,15,11],"width":4},{"step":"A:hop0","kind":"in","role":[6015,165],"bin":[23,15,11],"width":4},{"step":"A:hop1","kind":"out","role":[1480,106],"bin":[30,4,97],"width":4},{"step":"A:hop1","kind":"in","role":[4320,138],"bin":[30,4,97],"width":4},{"step":"A:end","kind":"in","role":[1480,106],"bin":[495,4,22],"width":4},{"step":"A","kind":"out","role":[5556,74],"bin":[507,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3541,53],"bin":[93,15,58],"width":4},{"step":"A:hop0","kind":"in","role":[5556,74],"bin":[93,15,58],"width":4},{"step":"A:hop1","kind":"out","role":[500,53],"bin":[26,6,5],"width":4},{"step":"A:hop1","kind":"in","role":[3541,53],"bin":[26,6,5],"width":4},{"step":"A:end","kind":"in","role":[500,53],"bin":[407,4,3],"width":4},{"step":"A","kind":"out","role":[5544,74],"bin":[322,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3542,85],"bin":[167,15,53],"width":4},{"step":"A:hop0","kind":"in","role":[5544,74],"bin":[167,15,53],"width":4},{"step":"A:hop1","kind":"out","role":[501,170],"bin":[100,4,92],"width":4},{"step":"A:hop1","kind":"in","role":[3542,85],"bin":[100,4,92],"width":4},{"step":"A:end","kind":"in","role":[501,170],"bin":[191,4,49],"width":4},{"step":"A","kind":"out","role":[5540,74],"bin":[26,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3542,83],"bin":[167,15,54],"width":4},{"step":"A:hop0","kind":"in","role":[5540,74],"bin":[167,15,54],"width":4},{"step":"A:hop1","kind":"out","role":[501,165],"bin":[100,4,93],"width":4},{"step":"A:hop1","kind":"in","role":[3542,83],"bin":[100,4,93],"width":4},{"step":"A:end","kind":"in","role":[501,165],"bin":[379,4,5],"width":4},{"step":"A","kind":"out","role":[3277,53],"bin":[578,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[501,163],"bin":[100,4,94],"width":4},{"step":"A:hop0","kind":"in","role":[3277,53],"bin":[100,4,94],"width":4},{"step":"A:end","kind":"in","role":[501,163],"bin":[334,6,57],"width":4},{"step":"A","kind":"out","role":[6002,165],"bin":[183,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,133],"bin":[23,15,12],"width":4},{"step":"A:hop0","kind":"in","role":[6002,165],"bin":[23,15,12],"width":4},{"step":"A:hop1","kind":"out","role":[1480,101],"bin":[30,4,98],"width":4},{"step":"A:hop1","kind":"in","role":[4320,133],"bin":[30,4,98],"width":4},{"step":"A:end","kind":"in","role":[1480,101],"bin":[234,4,0],"width":4},{"step":"A","kind":"out","role":[6007,165],"bin":[553,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,131],"bin":[23,15,13],"width":4},{"step":"A:hop0","kind":"in","role":[6007,165],"bin":[23,15,13],"width":4},{"step":"A:hop1","kind":"out","role":[1480,99],"bin":[30,4,99],"width":4},{"step":"A:hop1","kind":"in","role":[4320,131],"bin":[30,4,99],"width":4},{"step":"A:end","kind":"in","role":[1480,99],"bin":[384,4,16],"width":4},{"step":"A","kind":"out","role":[3273,53],"bin":[282,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[501,161],"bin":[100,4,95],"width":4},{"step":"A:hop0","kind":"in","role":[3273,53],"bin":[100,4,95],"width":4},{"step":"A:end","kind":"in","role":[501,161],"bin":[712,6,37],"width":4},{"step":"A","kind":"out","role":[6003,165],"bin":[257,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,129],"bin":[23,15,14],"width":4},{"step":"A:hop0","kind":"in","role":[6003,165],"bin":[23,15,14],"width":4},{"step":"A:hop1","kind":"out","role":[1480,90],"bin":[30,4,100],"width":4},{"step":"A:hop1","kind":"in","role":[4320,129],"bin":[30,4,100],"width":4},{"step":"A:end","kind":"in","role":[1480,90],"bin":[532,4,18],"width":4},{"step":"A","kind":"out","role":[3278,53],"bin":[652,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[501,154],"bin":[100,4,96],"width":4},{"step":"A:hop0","kind":"in","role":[3278,53],"bin":[100,4,96],"width":4},{"step":"A:end","kind":"in","role":[501,154],"bin":[445,6,36],"width":4},{"step":"A","kind":"out","role":[5553,74],"bin":[285,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3542,74],"bin":[167,15,55],"width":4},{"step":"A:hop0","kind":"in","role":[5553,74],"bin":[167,15,55],"width":4},{"step":"A:hop1","kind":"out","role":[501,149],"bin":[100,4,97],"width":4},{"step":"A:hop1","kind":"in","role":[3542,74],"bin":[100,4,97],"width":4},{"step":"A:end","kind":"in","role":[501,149],"bin":[446,6,34],"width":4},{"step":"A","kind":"out","role":[3264,53],"bin":[319,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[501,147],"bin":[100,4,98],"width":4},{"step":"A:hop0","kind":"in","role":[3264,53],"bin":[100,4,98],"width":4},{"step":"A:end","kind":"in","role":[501,147],"bin":[630,6,36],"width":4},{"step":"A","kind":"out","role":[3270,53],"bin":[60,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[501,145],"bin":[100,4,99],"width":4},{"step":"A:hop0","kind":"in","role":[3270,53],"bin":[100,4,99],"width":4},{"step":"A:end","kind":"in","role":[501,145],"bin":[75,6,25],"width":4},{"step":"A","kind":"out","role":[6014,165],"bin":[368,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,122],"bin":[23,15,15],"width":4},{"step":"A:hop0","kind":"in","role":[6014,165],"bin":[23,15,15],"width":4},{"step":"A:hop1","kind":"out","role":[1480,85],"bin":[30,4,101],"width":4},{"step":"A:hop1","kind":"in","role":[4320,122],"bin":[30,4,101],"width":4},{"step":"A:end","kind":"in","role":[1480,85],"bin":[123,4,11],"width":4},{"step":"A","kind":"out","role":[6016,165],"bin":[516,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,117],"bin":[23,15,16],"width":4},{"step":"A:hop0","kind":"in","role":[6016,165],"bin":[23,15,16],"width":4},{"step":"A:hop1","kind":"out","role":[1480,83],"bin":[30,4,102],"width":4},{"step":"A:hop1","kind":"in","role":[4320,117],"bin":[30,4,102],"width":4},{"step":"A:end","kind":"in","role":[1480,83],"bin":[234,4,4],"width":4},{"step":"A","kind":"out","role":[6017,165],"bin":[590,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,115],"bin":[23,15,17],"width":4},{"step":"A:hop0","kind":"in","role":[6017,165],"bin":[23,15,17],"width":4},{"step":"A:hop1","kind":"out","role":[1480,74],"bin":[30,4,103],"width":4},{"step":"A:hop1","kind":"in","role":[4320,115],"bin":[30,4,103],"width":4},{"step":"A:end","kind":"in","role":[1480,74],"bin":[604,4,13],"width":4},{"step":"A","kind":"out","role":[5555,74],"bin":[433,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3542,69],"bin":[167,15,56],"width":4},{"step":"A:hop0","kind":"in","role":[5555,74],"bin":[167,15,56],"width":4},{"step":"A:hop1","kind":"out","role":[501,138],"bin":[100,4,100],"width":4},{"step":"A:hop1","kind":"in","role":[3542,69],"bin":[100,4,100],"width":4},{"step":"A:end","kind":"in","role":[501,138],"bin":[334,6,72],"width":4},{"step":"A","kind":"out","role":[6005,165],"bin":[405,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,113],"bin":[23,15,18],"width":4},{"step":"A:hop0","kind":"in","role":[6005,165],"bin":[23,15,18],"width":4},{"step":"A:hop1","kind":"out","role":[1480,69],"bin":[30,4,104],"width":4},{"step":"A:hop1","kind":"in","role":[4320,113],"bin":[30,4,104],"width":4},{"step":"A:end","kind":"in","role":[1480,69],"bin":[495,4,16],"width":4},{"step":"A","kind":"out","role":[3261,53],"bin":[97,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[501,133],"bin":[100,4,101],"width":4},{"step":"A:hop0","kind":"in","role":[3261,53],"bin":[100,4,101],"width":4},{"step":"A:end","kind":"in","role":[501,133],"bin":[631,6,45],"width":4},{"step":"A","kind":"out","role":[5551,74],"bin":[137,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3542,58],"bin":[167,15,57],"width":4},{"step":"A:hop0","kind":"in","role":[5551,74],"bin":[167,15,57],"width":4},{"step":"A:hop1","kind":"out","role":[501,131],"bin":[100,4,102],"width":4},{"step":"A:hop1","kind":"in","role":[3542,58],"bin":[100,4,102],"width":4},{"step":"A:end","kind":"in","role":[501,131],"bin":[39,4,46],"width":4},{"step":"A","kind":"out","role":[5543,74],"bin":[248,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[3542,53],"bin":[167,15,58],"width":4},{"step":"A:hop0","kind":"in","role":[5543,74],"bin":[167,15,58],"width":4},{"step":"A:hop1","kind":"out","role":[501,129],"bin":[100,4,103],"width":4},{"step":"A:hop1","kind":"in","role":[3542,53],"bin":[100,4,103],"width":4},{"step":"A:end","kind":"in","role":[501,129],"bin":[601,6,76],"width":4},{"step":"A","kind":"out","role":[6009,165],"bin":[701,13,111],"width":4},{"step":"A:hop0","kind":"out","role":[4320,106],"bin":[23,15,19],"width":4},{"step":"A:hop0","kind":"in","role":[6009,165],"bin":[23,15,19],"width":4},{"step":"A:hop1","kind":"out","role":[1480,58],"bin":[30,4,105],"width":4},{"step":"A:hop1","kind":"in","role":[4320,106],"bin":[30,4,105],"width":4},{"step":"A:end","kind":"in","role":[1480,58],"bin":[606,4,36],"width":4},{"step":"B","kind":"out","role":[5119,206],"bin":[729,14,0],"width":9},{"step":"B","kind":"out","role":[5179,12],"bin":[729,14,0],"width":9},{"step":"B","kind":"out","role":[5319,0],"bin":[729,14,0],"width":9},{"step":"B","kind":"out","role":[5118,206],"bin":[655,14,0],"width":9},{"step":"B","kind":"out","role":[5178,12],"bin":[655,14,0],"width":9},{"step":"B","kind":"out","role":[5318,0],"bin":[655,14,0],"width":9},{"step":"B","kind":"out","role":[5117,206],"bin":[581,14,0],"width":9},{"step":"B","kind":"out","role":[5177,12],"bin":[581,14,0],"width":9},{"step":"B","kind":"out","role":[5317,0],"bin":[581,14,0],"width":9},{"step":"B","kind":"out","role":[5116,206],"bin":[507,14,0],"width":9},{"step":"B","kind":"out","role":[5176,12],"bin":[507,14,0],"width":9},{"step":"B","kind":"out","role":[5316,0],"bin":[507,14,0],"width":9},{"step":"B","kind":"out","role":[5115,206],"bin":[433,14,0],"width":9},{"step":"B","kind":"out","role":[5175,12],"bin":[433,14,0],"width":9},{"step":"B","kind":"out","role":[5315,0],"bin":[433,14,0],"width":9},{"step":"B","kind":"out","role":[5114,206],"bin":[359,14,0],"width":9},{"step":"B","kind":"out","role":[5174,12],"bin":[359,14,0],"width":9},{"step":"B","kind":"out","role":[5314,0],"bin":[359,14,0],"width":9},{"step":"B","kind":"out","role":[5113,206],"bin":[285,14,0],"width":9},{"step":"B","kind":"out","role":[5173,12],"bin":[285,14,0],"width":9},{"step":"B","kind":"out","role":[5313,0],"bin":[285,14,0],"width":9},{"step":"B","kind":"out","role":[5112,206],"bin":[211,14,0],"width":9},{"step":"B","kind":"out","role":[5172,12],"bin":[211,14,0],"width":9},{"step":"B","kind":"out","role":[5312,0],"bin":[211,14,0],"width":9},{"step":"B","kind":"out","role":[5111,206],"bin":[137,14,0],"width":9},{"step":"B","kind":"out","role":[5171,12],"bin":[137,14,0],"width":9},{"step":"B","kind":"out","role":[5311,0],"bin":[137,14,0],"width":9},{"step":"B","kind":"out","role":[5110,206],"bin":[63,14,0],"width":9},{"step":"B","kind":"out","role":[5170,12],"bin":[63,14,0],"width":9},{"step":"B","kind":"out","role":[5310,0],"bin":[63,14,0],"width":9},{"step":"B","kind":"out","role":[5109,206],"bin":[692,14,0],"width":9},{"step":"B","kind":"out","role":[5169,12],"bin":[692,14,0],"width":9},{"step":"B","kind":"out","role":[5309,0],"bin":[692,14,0],"width":9},{"step":"B","kind":"out","role":[5108,206],"bin":[618,14,0],"width":9},{"step":"B","kind":"out","role":[5168,12],"bin":[618,14,0],"width":9},{"step":"B","kind":"out","role":[5308,0],"bin":[618,14,0],"width":9},{"step":"B","kind":"out","role":[5107,206],"bin":[544,14,0],"width":9},{"step":"B","kind":"out","role":[5167,12],"bin":[544,14,0],"width":9},{"step":"B","kind":"out","role":[5307,0],"bin":[544,14,0],"width":9},{"step":"B","kind":"out","role":[5106,206],"bin":[470,14,0],"width":9},{"step":"B","kind":"out","role":[5166,12],"bin":[470,14,0],"width":9},{"step":"B","kind":"out","role":[5306,0],"bin":[470,14,0],"width":9},{"step":"B","kind":"out","role":[5105,206],"bin":[396,14,0],"width":9},{"step":"B","kind":"out","role":[5165,12],"bin":[396,14,0],"width":9},{"step":"B","kind":"out","role":[5305,0],"bin":[396,14,0],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5105,206],"bin":[256,13,82],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5106,206],"bin":[256,13,82],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5107,206],"bin":[256,13,82],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5108,206],"bin":[256,13,82],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5109,206],"bin":[256,13,82],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5110,206],"bin":[315,12,17],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5111,206],"bin":[315,12,17],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5112,206],"bin":[315,12,17],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5113,206],"bin":[315,12,17],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5114,206],"bin":[315,12,17],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5115,206],"bin":[540,12,3],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5116,206],"bin":[540,12,3],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5117,206],"bin":[540,12,3],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5118,206],"bin":[540,12,3],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5119,206],"bin":[540,12,3],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5165,12],"bin":[329,8,20],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5166,12],"bin":[329,8,20],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5167,12],"bin":[329,8,20],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5168,12],"bin":[329,8,20],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5169,12],"bin":[329,8,20],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5170,12],"bin":[647,12,86],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5171,12],"bin":[647,12,86],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5172,12],"bin":[647,12,86],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5173,12],"bin":[647,12,86],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5174,12],"bin":[647,12,86],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5175,12],"bin":[92,12,81],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5176,12],"bin":[92,12,81],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5177,12],"bin":[92,12,81],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5178,12],"bin":[92,12,81],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5179,12],"bin":[92,12,81],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5305,0],"bin":[622,10,83],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5306,0],"bin":[622,10,83],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5307,0],"bin":[622,10,83],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5308,0],"bin":[622,10,83],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5309,0],"bin":[622,10,83],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5310,0],"bin":[464,12,101],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5311,0],"bin":[464,12,101],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5312,0],"bin":[464,12,101],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5313,0],"bin":[464,12,101],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5314,0],"bin":[464,12,101],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5315,0],"bin":[244,13,88],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5316,0],"bin":[244,13,88],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5317,0],"bin":[244,13,88],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5318,0],"bin":[244,13,88],"width":9},{"step":"B:nine_into_empty48","kind":"in","role":[5319,0],"bin":[244,13,88],"width":9},{"step":"C","kind":"out","role":[5730,406],"bin":[63,13,111],"width":8},{"step":"C:end","kind":"in","role":[5730,406],"bin":[729,14,0],"width":8},{"step":"C","kind":"out","role":[5729,406],"bin":[692,13,111],"width":8},{"step":"C:end","kind":"in","role":[5729,406],"bin":[729,14,0],"width":8},{"step":"C","kind":"out","role":[6471,385],"bin":[146,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5580,2],"bin":[31,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6471,385],"bin":[31,14,0],"width":8},{"step":"C:end","kind":"in","role":[5580,2],"bin":[729,14,0],"width":8},{"step":"C","kind":"out","role":[5728,407],"bin":[615,13,111],"width":8},{"step":"C:end","kind":"in","role":[5728,407],"bin":[729,14,0],"width":8},{"step":"C","kind":"out","role":[5732,407],"bin":[208,13,111],"width":8},{"step":"C:end","kind":"in","role":[5732,407],"bin":[655,14,0],"width":8},{"step":"C","kind":"out","role":[6470,385],"bin":[72,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5581,2],"bin":[105,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6470,385],"bin":[105,14,0],"width":8},{"step":"C:end","kind":"in","role":[5581,2],"bin":[655,14,0],"width":8},{"step":"C","kind":"out","role":[5729,407],"bin":[689,13,111],"width":8},{"step":"C:end","kind":"in","role":[5729,407],"bin":[655,14,0],"width":8},{"step":"C","kind":"out","role":[5722,407],"bin":[171,13,111],"width":8},{"step":"C:end","kind":"in","role":[5722,407],"bin":[655,14,0],"width":8},{"step":"C","kind":"out","role":[6464,385],"bin":[331,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5582,2],"bin":[179,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6464,385],"bin":[179,14,0],"width":8},{"step":"C:end","kind":"in","role":[5582,2],"bin":[581,14,0],"width":8},{"step":"C","kind":"out","role":[6468,385],"bin":[627,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5583,2],"bin":[253,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6468,385],"bin":[253,14,0],"width":8},{"step":"C:end","kind":"in","role":[5583,2],"bin":[581,14,0],"width":8},{"step":"C","kind":"out","role":[5739,407],"bin":[726,13,111],"width":8},{"step":"C:end","kind":"in","role":[5739,407],"bin":[581,14,0],"width":8},{"step":"C","kind":"out","role":[6473,385],"bin":[294,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5584,2],"bin":[327,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6473,385],"bin":[327,14,0],"width":8},{"step":"C:end","kind":"in","role":[5584,2],"bin":[581,14,0],"width":8},{"step":"C","kind":"out","role":[5726,406],"bin":[470,13,111],"width":8},{"step":"C:end","kind":"in","role":[5726,406],"bin":[507,14,0],"width":8},{"step":"C","kind":"out","role":[5723,407],"bin":[245,13,111],"width":8},{"step":"C:end","kind":"in","role":[5723,407],"bin":[507,14,0],"width":8},{"step":"C","kind":"out","role":[5727,407],"bin":[541,13,111],"width":8},{"step":"C:end","kind":"in","role":[5727,407],"bin":[507,14,0],"width":8},{"step":"C","kind":"out","role":[5725,406],"bin":[396,13,111],"width":8},{"step":"C:end","kind":"in","role":[5725,406],"bin":[507,14,0],"width":8},{"step":"C","kind":"out","role":[5720,407],"bin":[23,13,111],"width":8},{"step":"C:end","kind":"in","role":[5720,407],"bin":[433,14,0],"width":8},{"step":"C","kind":"out","role":[5739,406],"bin":[729,13,111],"width":8},{"step":"C:end","kind":"in","role":[5739,406],"bin":[433,14,0],"width":8},{"step":"C","kind":"out","role":[5734,407],"bin":[356,13,111],"width":8},{"step":"C:end","kind":"in","role":[5734,407],"bin":[433,14,0],"width":8},{"step":"C","kind":"out","role":[5728,406],"bin":[618,13,111],"width":8},{"step":"C:end","kind":"in","role":[5728,406],"bin":[433,14,0],"width":8},{"step":"C","kind":"out","role":[5734,406],"bin":[359,13,111],"width":8},{"step":"C:end","kind":"in","role":[5734,406],"bin":[359,14,0],"width":8},{"step":"C","kind":"out","role":[5722,406],"bin":[174,13,111],"width":8},{"step":"C:end","kind":"in","role":[5722,406],"bin":[359,14,0],"width":8},{"step":"C","kind":"out","role":[5735,407],"bin":[430,13,111],"width":8},{"step":"C:end","kind":"in","role":[5735,407],"bin":[359,14,0],"width":8},{"step":"C","kind":"out","role":[6461,385],"bin":[109,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5585,2],"bin":[401,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6461,385],"bin":[401,14,0],"width":8},{"step":"C:end","kind":"in","role":[5585,2],"bin":[359,14,0],"width":8},{"step":"C","kind":"out","role":[6472,385],"bin":[220,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5586,2],"bin":[475,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6472,385],"bin":[475,14,0],"width":8},{"step":"C:end","kind":"in","role":[5586,2],"bin":[285,14,0],"width":8},{"step":"C","kind":"out","role":[6478,385],"bin":[664,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5587,2],"bin":[549,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6478,385],"bin":[549,14,0],"width":8},{"step":"C:end","kind":"in","role":[5587,2],"bin":[285,14,0],"width":8},{"step":"C","kind":"out","role":[5731,407],"bin":[134,13,111],"width":8},{"step":"C:end","kind":"in","role":[5731,407],"bin":[285,14,0],"width":8},{"step":"C","kind":"out","role":[5725,407],"bin":[393,13,111],"width":8},{"step":"C:end","kind":"in","role":[5725,407],"bin":[285,14,0],"width":8},{"step":"C","kind":"out","role":[5732,406],"bin":[211,13,111],"width":8},{"step":"C:end","kind":"in","role":[5732,406],"bin":[211,14,0],"width":8},{"step":"C","kind":"out","role":[6460,385],"bin":[35,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5588,2],"bin":[623,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6460,385],"bin":[623,14,0],"width":8},{"step":"C:end","kind":"in","role":[5588,2],"bin":[211,14,0],"width":8},{"step":"C","kind":"out","role":[5737,406],"bin":[581,13,111],"width":8},{"step":"C:end","kind":"in","role":[5737,406],"bin":[211,14,0],"width":8},{"step":"C","kind":"out","role":[5721,406],"bin":[100,13,111],"width":8},{"step":"C:end","kind":"in","role":[5721,406],"bin":[211,14,0],"width":8},{"step":"C","kind":"out","role":[5727,406],"bin":[544,13,111],"width":8},{"step":"C:end","kind":"in","role":[5727,406],"bin":[137,14,0],"width":8},{"step":"C","kind":"out","role":[5736,407],"bin":[504,13,111],"width":8},{"step":"C:end","kind":"in","role":[5736,407],"bin":[137,14,0],"width":8},{"step":"C","kind":"out","role":[6466,385],"bin":[479,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5589,2],"bin":[697,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6466,385],"bin":[697,14,0],"width":8},{"step":"C:end","kind":"in","role":[5589,2],"bin":[137,14,0],"width":8},{"step":"C","kind":"out","role":[5726,407],"bin":[467,13,111],"width":8},{"step":"C:end","kind":"in","role":[5726,407],"bin":[137,14,0],"width":8},{"step":"C","kind":"out","role":[6479,385],"bin":[738,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5590,2],"bin":[68,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6479,385],"bin":[68,14,0],"width":8},{"step":"C:end","kind":"in","role":[5590,2],"bin":[63,14,0],"width":8},{"step":"C","kind":"out","role":[5738,406],"bin":[655,13,111],"width":8},{"step":"C:end","kind":"in","role":[5738,406],"bin":[63,14,0],"width":8},{"step":"C","kind":"out","role":[6475,385],"bin":[442,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5591,2],"bin":[142,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6475,385],"bin":[142,14,0],"width":8},{"step":"C:end","kind":"in","role":[5591,2],"bin":[63,14,0],"width":8},{"step":"C","kind":"out","role":[5736,406],"bin":[507,13,111],"width":8},{"step":"C:end","kind":"in","role":[5736,406],"bin":[63,14,0],"width":8},{"step":"C","kind":"out","role":[5724,406],"bin":[322,13,111],"width":8},{"step":"C:end","kind":"in","role":[5724,406],"bin":[692,14,0],"width":8},{"step":"C","kind":"out","role":[5720,406],"bin":[26,13,111],"width":8},{"step":"C:end","kind":"in","role":[5720,406],"bin":[692,14,0],"width":8},{"step":"C","kind":"out","role":[5737,407],"bin":[578,13,111],"width":8},{"step":"C:end","kind":"in","role":[5737,407],"bin":[692,14,0],"width":8},{"step":"C","kind":"out","role":[6462,385],"bin":[183,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5592,2],"bin":[216,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6462,385],"bin":[216,14,0],"width":8},{"step":"C:end","kind":"in","role":[5592,2],"bin":[692,14,0],"width":8},{"step":"C","kind":"out","role":[6467,385],"bin":[553,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5593,2],"bin":[290,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6467,385],"bin":[290,14,0],"width":8},{"step":"C:end","kind":"in","role":[5593,2],"bin":[618,14,0],"width":8},{"step":"C","kind":"out","role":[5733,407],"bin":[282,13,111],"width":8},{"step":"C:end","kind":"in","role":[5733,407],"bin":[618,14,0],"width":8},{"step":"C","kind":"out","role":[6463,385],"bin":[257,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5594,2],"bin":[364,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6463,385],"bin":[364,14,0],"width":8},{"step":"C:end","kind":"in","role":[5594,2],"bin":[618,14,0],"width":8},{"step":"C","kind":"out","role":[5738,407],"bin":[652,13,111],"width":8},{"step":"C:end","kind":"in","role":[5738,407],"bin":[618,14,0],"width":8},{"step":"C","kind":"out","role":[5733,406],"bin":[285,13,111],"width":8},{"step":"C:end","kind":"in","role":[5733,406],"bin":[544,14,0],"width":8},{"step":"C","kind":"out","role":[5724,407],"bin":[319,13,111],"width":8},{"step":"C:end","kind":"in","role":[5724,407],"bin":[544,14,0],"width":8},{"step":"C","kind":"out","role":[5730,407],"bin":[60,13,111],"width":8},{"step":"C:end","kind":"in","role":[5730,407],"bin":[544,14,0],"width":8},{"step":"C","kind":"out","role":[6474,385],"bin":[368,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5595,2],"bin":[438,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6474,385],"bin":[438,14,0],"width":8},{"step":"C:end","kind":"in","role":[5595,2],"bin":[544,14,0],"width":8},{"step":"C","kind":"out","role":[6476,385],"bin":[516,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5596,2],"bin":[512,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6476,385],"bin":[512,14,0],"width":8},{"step":"C:end","kind":"in","role":[5596,2],"bin":[470,14,0],"width":8},{"step":"C","kind":"out","role":[6477,385],"bin":[590,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5597,2],"bin":[586,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6477,385],"bin":[586,14,0],"width":8},{"step":"C:end","kind":"in","role":[5597,2],"bin":[470,14,0],"width":8},{"step":"C","kind":"out","role":[5735,406],"bin":[433,13,111],"width":8},{"step":"C:end","kind":"in","role":[5735,406],"bin":[470,14,0],"width":8},{"step":"C","kind":"out","role":[6465,385],"bin":[405,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5598,2],"bin":[660,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6465,385],"bin":[660,14,0],"width":8},{"step":"C:end","kind":"in","role":[5598,2],"bin":[470,14,0],"width":8},{"step":"C","kind":"out","role":[5721,407],"bin":[97,13,111],"width":8},{"step":"C:end","kind":"in","role":[5721,407],"bin":[396,14,0],"width":8},{"step":"C","kind":"out","role":[5731,406],"bin":[137,13,111],"width":8},{"step":"C:end","kind":"in","role":[5731,406],"bin":[396,14,0],"width":8},{"step":"C","kind":"out","role":[5723,406],"bin":[248,13,111],"width":8},{"step":"C:end","kind":"in","role":[5723,406],"bin":[396,14,0],"width":8},{"step":"C","kind":"out","role":[6469,385],"bin":[701,13,111],"width":8},{"step":"C:hop0","kind":"out","role":[5599,2],"bin":[734,14,0],"width":8},{"step":"C:hop0","kind":"in","role":[6469,385],"bin":[734,14,0],"width":8},{"step":"C:end","kind":"in","role":[5599,2],"bin":[396,14,0],"width":8},{"step":"D","kind":"out","role":[4190,218],"bin":[63,13,111],"width":9},{"step":"D","kind":"out","role":[5370,66],"bin":[63,13,111],"width":9},{"step":"D","kind":"out","role":[5690,340],"bin":[63,13,111],"width":9},{"step":"D","kind":"out","role":[5910,0],"bin":[63,13,111],"width":9},{"step":"D","kind":"out","role":[4189,218],"bin":[692,13,111],"width":9},{"step":"D","kind":"out","role":[5369,66],"bin":[692,13,111],"width":9},{"step":"D","kind":"out","role":[5689,340],"bin":[692,13,111],"width":9},{"step":"D","kind":"out","role":[5909,0],"bin":[692,13,111],"width":9},{"step":"D","kind":"out","role":[4891,0],"bin":[146,13,111],"width":9},{"step":"D","kind":"out","role":[4951,0],"bin":[146,13,111],"width":9},{"step":"D","kind":"out","role":[5391,0],"bin":[146,13,111],"width":9},{"step":"D","kind":"out","role":[6251,1],"bin":[146,13,111],"width":9},{"step":"D:end","kind":"in","role":[4190,218],"bin":[615,13,111],"width":9},{"step":"D:end","kind":"in","role":[5370,66],"bin":[208,13,111],"width":9},{"step":"D:end","kind":"in","role":[5690,340],"bin":[72,13,111],"width":9},{"step":"D:end","kind":"in","role":[5910,0],"bin":[689,13,111],"width":9},{"step":"D:end","kind":"in","role":[4189,218],"bin":[171,13,111],"width":9},{"step":"D:end","kind":"in","role":[5369,66],"bin":[331,13,111],"width":9},{"step":"D:end","kind":"in","role":[5689,340],"bin":[627,13,111],"width":9},{"step":"D:end","kind":"in","role":[5909,0],"bin":[726,13,111],"width":9},{"step":"D:end","kind":"in","role":[4891,0],"bin":[294,13,111],"width":9},{"step":"D:end","kind":"in","role":[4951,0],"bin":[470,13,111],"width":9},{"step":"D:end","kind":"in","role":[5391,0],"bin":[245,13,111],"width":9},{"step":"D:end","kind":"in","role":[6251,1],"bin":[396,13,111],"width":9},{"step":"E","kind":"out","role":[4979,0],"bin":[739,12,10],"width":9},{"step":"E","kind":"out","role":[5499,0],"bin":[739,12,10],"width":9},{"step":"E","kind":"out","role":[6159,340],"bin":[739,12,10],"width":9},{"step":"E","kind":"out","role":[6199,340],"bin":[739,12,10],"width":9},{"step":"E","kind":"out","role":[6619,1],"bin":[739,12,10],"width":9},{"step":"E:end","kind":"in","role":[4979,0],"bin":[541,13,111],"width":9},{"step":"E:end","kind":"in","role":[5499,0],"bin":[23,13,111],"width":9},{"step":"E:end","kind":"in","role":[6159,340],"bin":[729,13,111],"width":9},{"step":"E:end","kind":"in","role":[6199,340],"bin":[618,13,111],"width":9},{"step":"E:end","kind":"in","role":[6619,1],"bin":[109,13,111],"width":9},{"step":"E","kind":"out","role":[4978,0],"bin":[665,12,10],"width":9},{"step":"E","kind":"out","role":[5498,0],"bin":[665,12,10],"width":9},{"step":"E","kind":"out","role":[6158,340],"bin":[665,12,10],"width":9},{"step":"E","kind":"out","role":[6198,340],"bin":[665,12,10],"width":9},{"step":"E","kind":"out","role":[6618,1],"bin":[665,12,10],"width":9},{"step":"E:end","kind":"in","role":[4978,0],"bin":[356,13,111],"width":9},{"step":"E:end","kind":"in","role":[5498,0],"bin":[359,13,111],"width":9},{"step":"E:end","kind":"in","role":[6158,340],"bin":[174,13,111],"width":9},{"step":"E:end","kind":"in","role":[6198,340],"bin":[220,13,111],"width":9},{"step":"E:end","kind":"in","role":[6618,1],"bin":[664,13,111],"width":9},{"step":"E","kind":"out","role":[4977,0],"bin":[591,12,10],"width":9},{"step":"E","kind":"out","role":[5497,0],"bin":[591,12,10],"width":9},{"step":"E","kind":"out","role":[6157,340],"bin":[591,12,10],"width":9},{"step":"E","kind":"out","role":[6197,340],"bin":[591,12,10],"width":9},{"step":"E","kind":"out","role":[6617,1],"bin":[591,12,10],"width":9},{"step":"E:end","kind":"in","role":[4977,0],"bin":[430,13,111],"width":9},{"step":"E:end","kind":"in","role":[5497,0],"bin":[134,13,111],"width":9},{"step":"E:end","kind":"in","role":[6157,340],"bin":[211,13,111],"width":9},{"step":"E:end","kind":"in","role":[6197,340],"bin":[35,13,111],"width":9},{"step":"E:end","kind":"in","role":[6617,1],"bin":[479,13,111],"width":9},{"step":"E","kind":"out","role":[4976,0],"bin":[517,12,10],"width":9},{"step":"E","kind":"out","role":[5496,0],"bin":[517,12,10],"width":9},{"step":"E","kind":"out","role":[6156,340],"bin":[517,12,10],"width":9},{"step":"E","kind":"out","role":[6196,340],"bin":[517,12,10],"width":9},{"step":"E","kind":"out","role":[6616,1],"bin":[517,12,10],"width":9},{"step":"E:end","kind":"in","role":[4976,0],"bin":[393,13,111],"width":9},{"step":"E:end","kind":"in","role":[5496,0],"bin":[581,13,111],"width":9},{"step":"E:end","kind":"in","role":[6156,340],"bin":[100,13,111],"width":9},{"step":"E:end","kind":"in","role":[6196,340],"bin":[544,13,111],"width":9},{"step":"E:end","kind":"in","role":[6616,1],"bin":[738,13,111],"width":9},{"step":"E","kind":"out","role":[4975,0],"bin":[443,12,10],"width":9},{"step":"E","kind":"out","role":[5495,0],"bin":[443,12,10],"width":9},{"step":"E","kind":"out","role":[6155,340],"bin":[443,12,10],"width":9},{"step":"E","kind":"out","role":[6195,340],"bin":[443,12,10],"width":9},{"step":"E","kind":"out","role":[6615,1],"bin":[443,12,10],"width":9},{"step":"E:end","kind":"in","role":[4975,0],"bin":[504,13,111],"width":9},{"step":"E:end","kind":"in","role":[5495,0],"bin":[467,13,111],"width":9},{"step":"E:end","kind":"in","role":[6155,340],"bin":[655,13,111],"width":9},{"step":"E:end","kind":"in","role":[6195,340],"bin":[442,13,111],"width":9},{"step":"E:end","kind":"in","role":[6615,1],"bin":[183,13,111],"width":9},{"step":"E","kind":"out","role":[4974,0],"bin":[369,12,10],"width":9},{"step":"E","kind":"out","role":[5494,0],"bin":[369,12,10],"width":9},{"step":"E","kind":"out","role":[6154,340],"bin":[369,12,10],"width":9},{"step":"E","kind":"out","role":[6194,340],"bin":[369,12,10],"width":9},{"step":"E","kind":"out","role":[6614,1],"bin":[369,12,10],"width":9},{"step":"E:end","kind":"in","role":[4974,0],"bin":[507,13,111],"width":9},{"step":"E:end","kind":"in","role":[5494,0],"bin":[322,13,111],"width":9},{"step":"E:end","kind":"in","role":[6154,340],"bin":[26,13,111],"width":9},{"step":"E:end","kind":"in","role":[6194,340],"bin":[553,13,111],"width":9},{"step":"E:end","kind":"in","role":[6614,1],"bin":[257,13,111],"width":9},{"step":"E","kind":"out","role":[4973,0],"bin":[295,12,10],"width":9},{"step":"E","kind":"out","role":[5493,0],"bin":[295,12,10],"width":9},{"step":"E","kind":"out","role":[6153,340],"bin":[295,12,10],"width":9},{"step":"E","kind":"out","role":[6193,340],"bin":[295,12,10],"width":9},{"step":"E","kind":"out","role":[6613,1],"bin":[295,12,10],"width":9},{"step":"E:end","kind":"in","role":[4973,0],"bin":[578,13,111],"width":9},{"step":"E:end","kind":"in","role":[5493,0],"bin":[282,13,111],"width":9},{"step":"E:end","kind":"in","role":[6153,340],"bin":[285,13,111],"width":9},{"step":"E:end","kind":"in","role":[6193,340],"bin":[368,13,111],"width":9},{"step":"E:end","kind":"in","role":[6613,1],"bin":[516,13,111],"width":9},{"step":"E","kind":"out","role":[4972,0],"bin":[221,12,10],"width":9},{"step":"E","kind":"out","role":[5492,0],"bin":[221,12,10],"width":9},{"step":"E","kind":"out","role":[6152,340],"bin":[221,12,10],"width":9},{"step":"E","kind":"out","role":[6192,340],"bin":[221,12,10],"width":9},{"step":"E","kind":"out","role":[6612,1],"bin":[221,12,10],"width":9},{"step":"E:end","kind":"in","role":[4972,0],"bin":[652,13,111],"width":9},{"step":"E:end","kind":"in","role":[5492,0],"bin":[319,13,111],"width":9},{"step":"E:end","kind":"in","role":[6152,340],"bin":[590,13,111],"width":9},{"step":"E:end","kind":"in","role":[6192,340],"bin":[433,13,111],"width":9},{"step":"E:end","kind":"in","role":[6612,1],"bin":[405,13,111],"width":9},{"step":"E","kind":"out","role":[4971,0],"bin":[147,12,10],"width":9},{"step":"E","kind":"out","role":[5491,0],"bin":[147,12,10],"width":9},{"step":"E","kind":"out","role":[6151,340],"bin":[147,12,10],"width":9},{"step":"E","kind":"out","role":[6191,340],"bin":[147,12,10],"width":9},{"step":"E","kind":"out","role":[6611,1],"bin":[147,12,10],"width":9},{"step":"E:end","kind":"in","role":[4971,0],"bin":[60,13,111],"width":9},{"step":"E:end","kind":"in","role":[5491,0],"bin":[97,13,111],"width":9},{"step":"E:end","kind":"in","role":[6151,340],"bin":[137,13,111],"width":9},{"step":"E:end","kind":"in","role":[6191,340],"bin":[248,13,111],"width":9},{"step":"E:end","kind":"in","role":[6611,1],"bin":[701,13,111],"width":9}] diff --git a/research/rank7-r1-t740-cap/construction/plan_t740.py b/research/rank7-r1-t740-cap/construction/plan_t740.py new file mode 100644 index 0000000000..289656be8b --- /dev/null +++ b/research/rank7-r1-t740-cap/construction/plan_t740.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Search provenance (not an entry point of verify.py): how allocation/RELOCATIONS.json was found. + +Start: ten lockstep copies of PR #2979's literal T74 fill (lift.py with no relocations). Its pattern mix is ten times +PR2979's T74 mix, which contains 60 non-tight [4,8,9,9,9,9]@48 bins and 17,280 [9,9,9]@32 bins; the optimal face of the +fixed-capacity relaxation (certificates/RELAX-CAP.json of PR2979) has an integral point at T740 that differs only by + 60 x [4,8,9,9,9,9]@48 -> 57 x [9,9,9,9,9]@48 + 3 x []@48 + 75 x [9,9,9]@32 -> 60 x [4,9,9,9]@32 + 15 x [8,8,8,8]@32 (both sides tight; widths and bins balance). +The chronology forbids doing this directly (the 4s and 8s of the [4,8,9,9,9,9] bins are late, almost all [9,9,9] bins +close early), so each displaced role travels along a chain of same-width exchanges: it enters an unlocked bin whose +window contains its call and evicts a same-width role of an earlier call, until a target bin can take the last role. +Every intermediate bin keeps its pattern. Steps: + A 60 fours -> 60 [9,9,9]@32 bins (become [4,9,9,9]); + B 15 [9,9,9]@32 bins Z (the latest-closing ones) send their 45 nines into 9 early empty @48 bins (5 each); + C 60 eights -> the Z bins (4 each; become [8,8,8,8]); + D three [4,8,9,9,9,9] bins are emptied; their 12 nines go one each into 12 of the other 57; + E nine late [9,9,9,9,9]@48 bins are emptied; their 45 nines go one each into the remaining 45 of the 57. +Greedy, seeded (seed 1), first fit; exchanges always move to a strictly earlier call, so chains terminate. + +Usage (from the repository root): python3 -B research/rank7-r1-t740-cap/construction/plan_t740.py --out DIR +The search only reads helper widths, windows and families, which PR3015's R1 edit leaves unchanged. +Writes DIR/RELOCATIONS.json and DIR/CHAINS.json and re-checks the rebuilt allocation with PR2979's vendored engine. +Rohan Arun, with substantial AI assistance (Anthropic Claude). Apache-2.0. +""" +import argparse +import collections +import json +import random +import sys +import time +import types +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PKG = HERE.parent +SRC = PKG.parent / 'rank7-joint-endframes' +sys.path.insert(0, str(PKG)) +import lift as L # noqa: E402 + + +def load(name, path): + module = types.ModuleType(name) + module.__file__ = str(path) + exec(compile(Path(path).read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--out', type=Path, required=True) + ap.add_argument('--seed', type=int, default=1) + args = ap.parse_args() + rng = random.Random(args.seed) + engine = load('owners2979', SRC / 'allocation/vendor/independent_owners.py') + template, plan = L.read(SRC / 'allocation/vendor/TEMPLATE.json.gz'), L.read(SRC / 'allocation/vendor/PLAN.json.gz') + providers = L.read(SRC / 'allocation/PROVIDERS.json') + for pv in providers.values(): + pv['actual_paid_profile'] = {int(r): n for r, n in pv['actual_paid_profile'].items()} + T, order, dispatch, fill, _ = L.build(SRC / 'allocation', [], providers) + rows = fill['rows'] + d = {(s, r): p for s, r, p in dispatch} + win = engine.windows(template, order, T) + fam = lambda o, c, p: o * 896 + (2 * plan['pairs'][str(c)] + plan['sides'][str(c)]) * 112 + p + WID = [providers[d[tuple(order[r[0]])]]['widths'][r[1]] for r in rows] + bins = collections.defaultdict(list) + used = collections.defaultdict(set) + for i, (t, h, o, c, p, z) in enumerate(rows): + bins[o, c, p].append(i) + used[t].add(fam(o, c, p)) + pattern = lambda b: tuple(sorted(WID[i] for i in bins[b])) + allbins = [(o, c, p) for (o, c) in win for p in range(112)] + bypat = collections.defaultdict(list) + for b in allbins: + bypat[win[b[0], b[1]][0], pattern(b)].append(b) + for k in bypat: + rng.shuffle(bypat[k]) + X = list(bypat[48, (4, 8, 9, 9, 9, 9)]) + assert len(X) == 60 + locked = set(X) + + def fits(i, b): + t = rows[i][0] + cap, lo, hi = win[b[0], b[1]] + return lo < t <= hi and fam(*b) not in used[t] + + chains = [] + + def detach(i, label): + t, h, o, c, p, z = rows[i] + used[t].discard(fam(o, c, p)) + bins[o, c, p].remove(i) + rows[i][2:5] = [-1, -1, -1] + chains.append(dict(step=label, kind='out', role=[t, h], bin=[o, c, p], width=WID[i])) + + def attach(i, b, label): + assert rows[i][2] == -1 and fits(i, b), (label, i, b) + t = rows[i][0] + rows[i][2:5] = list(b) + bins[b].append(i) + used[t].add(fam(*b)) + chains.append(dict(step=label, kind='in', role=rows[i][:2], bin=list(b), width=WID[i])) + + exchange = {} + + def chain(i, targets, label, maxhops=40): + w = WID[i] + if w not in exchange: + exchange[w] = sorted((rows[k][0], b, k) for b in allbins if b not in locked for k in bins[b] if WID[k] == w) + cur = i + for hop in range(maxhops): + tgt = next((b for b in targets() if fits(cur, b)), None) + if tgt is not None: + attach(cur, tgt, label + ':end') + return tgt + t = rows[cur][0] + nxt = None + for tt, b, k in exchange[w]: + if tt >= t: + break + if b in locked or rows[k][2:5] != list(b): + continue + cap, lo, hi = win[b[0], b[1]] + if lo < t <= hi and fam(*b) not in used[t]: + nxt = (b, k) + break + if nxt is None: + return None + b, k = nxt + detach(k, label + ':hop%d' % hop) + attach(cur, b, label + ':hop%d' % hop) + locked.add(b) + cur = k + return None + + t0 = time.time() + Y = list(bypat[32, (9, 9, 9)]) + Z = sorted(Y, key=lambda b: -win[b[0], b[1]][2])[:15] + locked.update(Z) + for i in [k for b in X for k in bins[b] if WID[k] == 4]: + detach(i, 'A') + tgt = chain(i, lambda: [y for y in Y if y not in locked], 'A') + assert tgt is not None, 'step A' + locked.add(tgt) + E48 = [b for b in bypat[48, ()] if b not in locked] + held = [] + for z in Z: + for i in list(bins[z]): + detach(i, 'B') + held.append(i) + held.sort(key=lambda i: rows[i][0]) + remaining = list(held) + for e in E48: + if not remaining: + break + if e in locked: + continue + group, calls = [], set() + cap, lo, hi = win[e[0], e[1]] + for i in remaining: + t = rows[i][0] + if t not in calls and lo < t <= hi and fam(*e) not in used[t]: + group.append(i) + calls.add(t) + if len(group) == 5: + break + if len(group) < 5: + continue + for i in group: + attach(i, e, 'B:nine_into_empty48') + remaining.remove(i) + locked.add(e) + assert not remaining + count = {z: 0 for z in Z} + for i in [k for b in X for k in bins[b] if WID[k] == 8]: + detach(i, 'C') + tgt = chain(i, lambda: [z for z in Z if count[z] < 4], 'C') + assert tgt is not None, 'step C' + count[tgt] += 1 + assert all(v == 4 for v in count.values()) + emptied, keep = X[:3], X[3:] + want = {b: 1 for b in keep} + open_keep = lambda: [b for b in keep if want[b]] + nines = [i for b in emptied for i in bins[b] if WID[i] == 9] + for i in nines: + detach(i, 'D') + for i in nines: + tgt = chain(i, open_keep, 'D') + assert tgt is not None, 'step D' + want[tgt] -= 1 + late = [b for b in bypat[48, (9, 9, 9, 9, 9)] if b not in locked] + late.sort(key=lambda b: -win[b[0], b[1]][1]) + emptied95 = 0 + for b in late: + if not any(want.values()): + break + if b in locked: + continue + ns = [i for i in bins[b] if WID[i] == 9] + if len(ns) != 5: + continue + if not all(any(win[k[0], k[1]][1] < rows[i][0] <= win[k[0], k[1]][2] for k in open_keep()) for i in ns): + continue + locked.add(b) + for i in ns: + detach(i, 'E') + for i in ns: + tgt = chain(i, open_keep, 'E') + assert tgt is not None, 'step E' + want[tgt] -= 1 + emptied95 += 1 + assert emptied95 == 9 and not any(want.values()) + assert all(r[2] >= 0 for r in rows) + print('search %.1f s, chain events %d' % (time.time() - t0, len(chains)), flush=True) + final = {} + for e in chains: + if e['kind'] == 'in': + final[tuple(e['role'])] = e['bin'] + relocations = sorted([t, h] + b for (t, h), b in final.items()) + base_bins = {(r[0], r[1]): (r[2], r[3], r[4]) for r in L.lift_rows(L.read(SRC / 'allocation/FILL.json.gz'))} + relocations = [e for e in relocations if base_bins[e[0], e[1]] != tuple(e[2:])] + args.out.mkdir(parents=True, exist_ok=False) + (args.out / 'RELOCATIONS.json').write_text(json.dumps(relocations, separators=(',', ':')) + '\n') + (args.out / 'CHAINS.json').write_text(json.dumps(chains, separators=(',', ':')) + '\n') + T, order, dispatch, fill, touched = L.build(SRC / 'allocation', relocations, providers) + t0 = time.time() + result, _, _ = engine.check(T, order, fill, d, None, plan, template, providers) + print('relocations', len(relocations), 'touched bins', len(touched), 'engine %.1f s' % (time.time() - t0), 'idle', result['idle'], flush=True) + + +if __name__ == '__main__': + main() diff --git a/research/rank7-r1-t740-cap/controls.py b/research/rank7-r1-t740-cap/controls.py new file mode 100644 index 0000000000..ed6b8abff0 --- /dev/null +++ b/research/rank7-r1-t740-cap/controls.py @@ -0,0 +1,131 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Registered failure controls for research/rank7-r1-t740-cap (standard library only, about four to five minutes). + +Each control changes one thing and must be rejected (or, for the ablation, must lose the gain): + no_relocations ten lockstep copies of PR2979's T74 fill alone (PR3015's allocation): a valid allocation whose root is PR3015's, + strictly below the cap (the relocations are what attains it); + dropped_chain_link one relocation of an exchange chain omitted: the owner engine rejects the allocation; + window_violation one relocated role sent to a same-capacity bin whose window excludes its call; + family_collision one relocated role sent to a bin of a family its call already uses; + stale_profile the claimed complete profile with one extra rank-1 child; + tampered_relocations two relocated roles of different widths exchange destinations: payload pin fails; + wrong_moment_baseline the moment auditor fed PR2969's claim instead of PR3015's: authenticated-baseline rejection. +Rohan Arun, with substantial AI assistance (Anthropic Claude). Apache-2.0. +""" +import collections +import json +import shutil +import sys +import tempfile +import time +from fractions import Fraction as Q +from pathlib import Path + +PKG = Path(__file__).resolve().parent +sys.path.insert(0, str(PKG)) +import lift as L # noqa: E402 +import verify as V # noqa: E402 + + +def main(): + if not __debug__: + raise SystemExit('refusing python -O: this checker relies on assertions') + start = time.monotonic() + V.check_pins() + providers = V.derive_providers() + engine = V.load('owners2979_r1_controls', V.SRC / 'allocation/vendor/independent_owners.py') + plan, template = L.read(V.SRC / 'allocation/vendor/PLAN.json.gz'), L.read(V.SRC / 'allocation/vendor/TEMPLATE.json.gz') + relocations = L.read(PKG / 'allocation/RELOCATIONS.json') + expected = L.read(PKG / 'allocation/EXPECTED.json') + claimed = {int(k): v for k, v in L.read(PKG / 'allocation/PROFILE.json').items()} + sys.path.insert(0, str(V.SRC / 'tools')) + import root as R + cap_lo = Q(L.read(PKG / 'certificates/R1-RELAX-CAP.json')['cap_lower']) + results = {} + + def build(rel): + T, order, dispatch, fill, touched = L.build(V.SRC / 'allocation', rel, providers) + return T, order, {(s, r): p for s, r, p in dispatch}, fill + + def rejected(name, rel, claim=claimed): + T, order, d, fill = build(rel) + try: + engine.check(T, order, fill, d, claim, plan, template, providers) + except ValueError as error: + results[name] = 'rejected: ' + str(error) + return + raise AssertionError('accepted corrupted allocation: ' + name) + + # ablation: no relocations + T, order, d, fill = build([]) + result, win, _ = engine.check(T, order, fill, d, None, plan, template, providers) + prof = {int(k): v for k, v in result['profile'].items()} + base = {int(k): v for k, v in L.read(PKG / 'comparators/PR3015-PROFILE.json').items()} + V.need(prof == {r: 10 * n for r, n in base.items()} and prof != claimed, 'lift alone = ten times the PR3015 profile') + lo, hi = R.kappa_from_profile(prof, T) + V.need(hi < cap_lo and (lo, hi) == R.kappa_from_profile(base, 74), 'lift alone keeps the PR3015 root below the cap') + results['no_relocations'] = 'valid allocation, root bracket [%s, %s] below the cap by %.4e' % (lo, hi, float(cap_lo - hi)) + # one omitted chain link: the first relocation whose destination bin also loses a role + sources = {} + base_rows = {(r[0], r[1]): (r[2], r[3], r[4]) for r in L.lift_rows(L.read(V.SRC / 'allocation/FILL.json.gz'))} + for e in relocations: + sources.setdefault(base_rows[e[0], e[1]], []).append(e) + link = next(e for e in relocations if tuple(e[2:]) in sources) + rejected('dropped_chain_link', [e for e in relocations if e is not link]) + # window violation: same capacity, window excludes the call + e = relocations[0] + cap = win[e[2], e[3]][0] + (o, c), _ = next(((k, v) for k, v in win.items() if v[0] == cap and not v[1] < e[0] <= v[2])) + bad = [list(x) for x in relocations] + bad[0] = [e[0], e[1], o, c, e[4]] + rejected('window_violation', bad) + # family collision: a bin (same window class) of a family already used by the call + t0 = e[0] + T_, order_, d_, fill_ = build(relocations) + used = {(r[2], r[3], r[4]) for r in fill_['rows'] if r[0] == t0 and r[1] != e[1]} + target = next(b for b in sorted(used) if win[b[0], b[1]][1] < t0 <= win[b[0], b[1]][2]) + bad = [list(x) for x in relocations] + bad[0] = [e[0], e[1]] + list(target) + rejected('family_collision', bad) + # stale profile + wrong = dict(claimed) + wrong[1] += 1 + rejected('stale_profile', relocations, wrong) + # tampered relocations: swap destinations of two roles of different widths + width = lambda x: providers[d_[tuple(order_[x[0]])]]['widths'][x[1]] + a = relocations[0] + b = next(x for x in relocations if width(x) != width(a)) + bad = [list(x) for x in relocations] + ia, ib = relocations.index(a), relocations.index(b) + bad[ia] = a[:2] + b[2:] + bad[ib] = b[:2] + a[2:] + T2, order2, dispatch2, fill2, touched2 = L.build(V.SRC / 'allocation', bad, providers) + V.need(L.digest(fill2) != expected['payload_sha256']['FILL.json.gz'], 'tampered relocations change the pinned payload') + results['tampered_relocations'] = 'rejected: canonical FILL payload differs from allocation/EXPECTED.json' + # moment auditor with a wrong baseline + moment = V.load('moment_controls', PKG / 'tools/audit_allocation_moment.py') + repo = V.ROOT + with tempfile.TemporaryDirectory() as tmp: + cand, wrongbase = Path(tmp) / 'candidate', Path(tmp) / 'baseline' + cand.mkdir() + wrongbase.mkdir() + (cand / 'ORDER.json').write_bytes(L.canonical(order_)) + (cand / 'PROFILE.json').write_bytes(L.canonical({str(r): n for r, n in sorted(claimed.items())})) + shutil.copyfile(V.SRC / 'allocation/baseline/CLAIM.json', wrongbase / 'CLAIM.json') + shutil.copyfile(V.SRC / 'allocation/baseline/ORDER.json', wrongbase / 'ORDER.json') + shutil.copyfile(V.SRC / 'allocation/baseline/PROFILE.json', wrongbase / 'PROFILE.json') + try: + moment.run(cand, wrongbase) + except ValueError as error: + results['wrong_moment_baseline'] = 'rejected: ' + str(error) + else: + raise AssertionError('moment auditor accepted an unauthenticated baseline') + V.need(set(results) == {'no_relocations', 'dropped_chain_link', 'window_violation', 'family_collision', 'stale_profile', + 'tampered_relocations', 'wrong_moment_baseline'}, 'all controls ran') + print(json.dumps(results, indent=1, sort_keys=True)) + print('PASS_RANK7_R1_T740_CAP_CONTROLS %d controls %.1f s' % (len(results), time.monotonic() - start)) + + +if __name__ == '__main__': + main() diff --git a/research/rank7-r1-t740-cap/data/R1-WORD-base.json.gz b/research/rank7-r1-t740-cap/data/R1-WORD-base.json.gz new file mode 100644 index 0000000000..4f04836573 Binary files /dev/null and b/research/rank7-r1-t740-cap/data/R1-WORD-base.json.gz differ diff --git a/research/rank7-r1-t740-cap/data/R1-WORD-extra.json.gz b/research/rank7-r1-t740-cap/data/R1-WORD-extra.json.gz new file mode 100644 index 0000000000..81f95e21ed Binary files /dev/null and b/research/rank7-r1-t740-cap/data/R1-WORD-extra.json.gz differ diff --git a/research/rank7-r1-t740-cap/lift.py b/research/rank7-r1-t740-cap/lift.py new file mode 100644 index 0000000000..445c0b660c --- /dev/null +++ b/research/rank7-r1-t740-cap/lift.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Deterministic T740 allocation of PR #2979's unchanged words. + +The allocation is defined by three things only: + 1. PR #2979's literal T74 allocation (research/rank7-joint-endframes/allocation: ORDER, DISPATCH, FILL); + 2. ten lockstep copies of it, in Dugongue's PR #2969 lift convention: + call (s, r) at T74 time t -> call (s, r + 74 j) at T740 time 10 t + j (j = 0..9), + role (t, h, o, c, p, z) -> role (10 t + j, h, o + 74 j, c, p, z); + 3. allocation/RELOCATIONS.json: 332 roles [time, helper, owner_replica, child, port], each moved to the given bin. +Every bin that a relocated role leaves or enters is repacked as a compact prefix in (time, helper) order; no other row +changes. Standard library only. Columns of FILL rows: time, helper, owner_replica, child, port, offset. + +Rohan Arun, with substantial AI assistance (Anthropic Claude). Apache-2.0. +""" +import gzip +import hashlib +import json +from collections import defaultdict +from pathlib import Path + +COPIES = 10 +SOURCE_T = 74 +METHOD = ('PR2979 literal T74 fill lifted to ten lockstep copies (PR2969 convention, T740) plus 332 explicit whole-role ' + 'relocations (allocation/RELOCATIONS.json); touched bins repacked as compact prefixes in (time, helper) order') + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def read(path): + raw = Path(path).read_bytes() + return json.loads(gzip.decompress(raw) if raw[:2] == b'\x1f\x8b' else raw) + + +def canonical(obj): + """Canonical JSON payload bytes; SHA-256 pins refer to these bytes (not to any gzip container).""" + return (json.dumps(obj, sort_keys=True, separators=(',', ':')) + '\n').encode() + + +def digest(obj): + return hashlib.sha256(canonical(obj)).hexdigest() + + +def lift_order(order74): + return [[s, r + SOURCE_T * j] for s, r in order74 for j in range(COPIES)] + + +def lift_dispatch(dispatch74): + return [[s, r + SOURCE_T * j, p] for s, r, p in dispatch74 for j in range(COPIES)] + + +def lift_rows(fill74): + return [[COPIES * t + j, h, o + SOURCE_T * j, c, p, z] for t, h, o, c, p, z in fill74['rows'] for j in range(COPIES)] + + +def build(source_allocation, relocations, providers): + """Return (T, order, dispatch, fill, touched_bins). `providers` maps provider id -> {'widths': [...]}.""" + source = Path(source_allocation) + order74, dispatch74, fill74 = read(source / 'ORDER.json'), read(source / 'DISPATCH.json'), read(source / 'FILL.json.gz') + need(fill74['columns'] == ['time', 'helper', 'owner_replica', 'child', 'port', 'offset'], 'source fill columns') + need(len(order74) == 9 * SOURCE_T and len(dispatch74) == 9 * SOURCE_T, 'source T74 order/dispatch') + T = SOURCE_T * COPIES + order, dispatch, rows = lift_order(order74), lift_dispatch(dispatch74), lift_rows(fill74) + provider_of = {(s, r): p for s, r, p in dispatch} + where = {(row[0], row[1]): i for i, row in enumerate(rows)} + need(len(where) == len(rows), 'unique (time, helper) roles') + touched, moved = set(), set() + for entry in relocations: + need(len(entry) == 5 and all(type(x) is int for x in entry), 'relocation shape [time, helper, owner, child, port]') + t, h, o, c, p = entry + need((t, h) in where and (t, h) not in moved, 'relocated role exists and moves once') + moved.add((t, h)) + row = rows[where[t, h]] + old = (row[2], row[3], row[4]) + need(old != (o, c, p), 'a relocation changes the bin') + touched.add(old) + touched.add((o, c, p)) + row[2], row[3], row[4] = o, c, p + members = defaultdict(list) + for i, row in enumerate(rows): + key = (row[2], row[3], row[4]) + if key in touched: + members[key].append(i) + for key, ids in members.items(): + offset = 0 + for i in sorted(ids, key=lambda k: (rows[k][0], rows[k][1])): + rows[i][5] = offset + offset += providers[provider_of[tuple(order[rows[i][0]])]]['widths'][rows[i][1]] + rows.sort() + fill = {'columns': list(fill74['columns']), 'dispatch_overrides': [], 'method': METHOD, 'rows': rows} + return T, order, dispatch, fill, touched + + +def write(out, T, order, dispatch, fill, profile): + """Write the T740 allocation in PR2979's layout (gzip mtime 0) and return the canonical payload SHA-256 values.""" + out = Path(out) + out.mkdir(parents=True, exist_ok=False) + payloads = {'ORDER.json': order, 'DISPATCH.json': dispatch, 'FILL.json.gz': fill, + 'PROFILE.json': {str(r): n for r, n in sorted(profile.items())}} + for name, obj in payloads.items(): + data = canonical(obj) + (out / name).write_bytes(gzip.compress(data, mtime=0) if name.endswith('.gz') else data) + return {name: digest(obj) for name, obj in payloads.items()} diff --git a/research/rank7-r1-t740-cap/tools/audit_allocation_moment.py b/research/rank7-r1-t740-cap/tools/audit_allocation_moment.py new file mode 100644 index 0000000000..c3e21c80ab --- /dev/null +++ b/research/rank7-r1-t740-cap/tools/audit_allocation_moment.py @@ -0,0 +1,84 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent dyadic interval moment auditor, atlas D020. +Retained PR2908 arithmetic by Jeremy Diviney and its credited upstream authors; +Mason Hale with OpenAI Codex assistance changes only the authenticated baseline. +Marius-Paul Dumitrean (Claude Code assisted) changes only the authenticated baseline, to the PR2917 headline (PR2930), +to the PR2930 headline (PR2942) and to Dugongue's PR2969 moment nomination (its T370 ORDER/PROFILE). +Rohan Arun (Anthropic Claude assisted) changes only the authenticated baseline, to Jeremy Kothe's PR3015 headline (its T74 ORDER/PROFILE). +Uses only Python integers/Fraction; imports no inherited numerical implementation. +This authenticates a paid histogram and its root, not a physical realization. +""" +from fractions import Fraction as F +from pathlib import Path +from functools import lru_cache +from collections import Counter +import argparse,json,hashlib + +BITS=192 +SCALE=1<=1,'log domain');k=0 + while q>2:q/=2;k+=1 + def unit(y): + z=(y-1)/(y+1);z2=z*z;term=z;value=F(0) + for j in range(128): + value+=term/(2*j+1);term*=z2 + remainder=2*term/(257*(1-z2)) + return 2*value,2*value+remainder + l,u=unit(q);l2,u2=unit(F(2));return down(l+k*l2),up(u+k*u2) +def exp_bounds(y): + need(0<=y0,'profile domain');l,u=log_bounds(F(73,rank));a=exp_bounds(b*l)[0];z=exp_bounds(b*u)[1];weight=F(rank*count,73*W);lo+=weight*a;hi+=weight*z + return down(lo),up(hi) +def run(candidate,source): + import sys + if hasattr(sys,'set_int_max_str_digits'):sys.set_int_max_str_digits(0) + need(hashlib.sha256((source/'CLAIM.json').read_bytes()).hexdigest()=='f9b9fbaaac794c0ce279c238a33a2f34f8c91a34d97ccdeb5ec98b7b8ba56d73','exact pinned PR3015 headline') + prof={int(k):v for k,v in json.loads((candidate/'PROFILE.json').read_bytes()).items()} + old={int(k):v for k,v in json.loads((source/'PROFILE.json').read_bytes()).items()} + W=896*(1+max(r for s,r in json.loads((candidate/'ORDER.json').read_bytes()))) + oldW=896*(1+max(r for s,r in json.loads((source/'ORDER.json').read_bytes()))) + need(sum(r*n for r,n in prof.items())==W*73-W*320//896,'new rank mass') + need(sum(r*n for r,n in old.items())==oldW*73-oldW*320//896,'old rank mass') + # No floating endpoint or inherited numerical implementation is used. + q=10**26;lo=0;hi=q//200 + need(moment(prof,F(lo,q),W)[1]<1 and moment(prof,F(hi,q),W)[0]>1,'global root bracket') + while hi-lo>1: + mid=(lo+hi)//2;l,u=moment(prof,F(mid,q),W) + if u<1:lo=mid + elif l>1:hi=mid + else:raise ValueError('interval precision insufficient') + endpoint=F((lo//100),10**24) + target=endpoint-F(1,10**46)-F(1,10**70) + prior=F(json.loads((source/'CLAIM.json').read_bytes())['kappa']) + need(target>prior and target1,'overstated endpoint rejected') + wrong=dict(prof);wrong[32]=wrong.get(32,0)+1 + need(moment(wrong,F(lo,q),W)[0]>1,'omitted rank charge rejected') + import decimal + with decimal.localcontext() as c: + c.prec=80 + todec=lambda x:str(decimal.Decimal(x.numerator)/decimal.Decimal(x.denominator)) + texttarget=todec(target);textgain=todec(target-prior) + return dict(status='PASS_SEPARATE_EXACT_RATIONAL_FRONTIER_MOMENT',lower=str(F(lo,q)),upper=str(F(hi,q)),outer_endpoint=str(endpoint),target=str(target),target_decimal=texttarget,previous=str(prior),gain=str(target-prior),gain_decimal=textgain,W=W,oldW=oldW,normalized_profile_delta=normalized_delta,new_moment_at_full_prior=[str(x)for x in at_old],profile_sha256=hashlib.sha256((candidate/'PROFILE.json').read_bytes()).hexdigest(),baseline_profile_sha256=hashlib.sha256((source/'PROFILE.json').read_bytes()).hexdigest(),baseline_claim_sha256=hashlib.sha256((source/'CLAIM.json').read_bytes()).hexdigest(),method='Independent 128-term atanh / degree24 exponential with explicit positive tails and outward 192-bit dyadic rounding',controls=['zero log/exp identities','overstated endpoint','added rank32 charge'],scope='Complete paid histogram and exact moment only; full native/physical/outer release is separate.') +if __name__=='__main__': + p=argparse.ArgumentParser();p.add_argument('--candidate',type=Path,required=True);p.add_argument('--source',type=Path,required=True);p.add_argument('--out',type=Path,required=True);a=p.parse_args() + need(not a.out.exists(),'fresh output required');d=run(a.candidate,a.source);a.out.write_text(json.dumps(d,sort_keys=True,indent=2)+'\n',encoding='utf-8',newline='\n');print(json.dumps({k:d[k]for k in ['status','target_decimal','gain_decimal','lower','upper']})) diff --git a/research/rank7-r1-t740-cap/verify.py b/research/rank7-r1-t740-cap/verify.py new file mode 100644 index 0000000000..e58a8e438d --- /dev/null +++ b/research/rank7-r1-t740-cap/verify.py @@ -0,0 +1,263 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Registered check: PR #3015's R1 words with a T740 allocation that attains their fixed-capacity packing cap. + +Standard library only (Python 3.10+, assertions enabled); about one to two minutes on one core. + 1. Live input pins (SOURCES.json) for the PR2979 files used (allocation, engine, template, tools) and the vendored + PR3015/PR3021 files (VENDOR.json: exact PR heads, Git blobs, SHA-256). + 2. Providers: PR3015's two R1 words (data/R1-WORD-*.json.gz) re-derive the provider registry with PR2979's frame + accounting (vendor/preload_move.py frame_report): helper widths equal PR2979's registry (R1 changes none), local + profile {1:2443, 2:707, 3:232, 4:108, 5:18, 8:8}, 408 helpers, 8 centres, 91 private buffers. + 3. Allocation: lift.py rebuilds the T740 ORDER/DISPATCH/FILL from PR2979's literal T74 allocation (which PR3015 uses + unchanged) and allocation/RELOCATIONS.json; canonical payload SHA-256 values equal allocation/EXPECTED.json. + 4. Owners: PR2979's vendored owner engine (PR2839/PR2751 lineage) checks all 2,717,280 roles at T740 with the R1 + providers: helper identities, windows, same-call family exclusions, capacities, masks, compact prefixes, the complete + paid profile (= allocation/PROFILE.json) and the rank-mass identity. Physical stock = live + 408 + 8 + 91 + 2. + 5. Optimal face: PR3015's Fractions-only cap certificate for the R1 profile (certificates/R1-RELAX-CAP.json, + re-verified with PR2979's relax_exact.py); exact row multipliers fix [9,9,9]@32, [9,9,9,9,9]@48 and []@48 at 93/4, + 1341/20 and 7619/20 per replica (an integral optimum needs 20 | T); the literal idle histogram is exactly 740 x the + optimal basic idle profile; every literal bin pattern has identically zero reduced cost; the exact root bracket of the + literal profile equals the R1 cap bracket. + 6. Moment: the dyadic moment auditor (PR2917/PR2979 lineage) with its authenticated baseline re-pinned to PR3015's + headline: strict gain; exact comparison with PR3021's released headline: strict gain. + 7. CLAIM.json agrees with all of the above. +Failure controls are in controls.py (separately registered). +Rohan Arun, with substantial AI assistance (Anthropic Claude). Apache-2.0. +""" +import argparse +import collections +import hashlib +import json +import shutil +import sys +import tempfile +import time +import types +from fractions import Fraction as Q +from pathlib import Path + +PKG = Path(__file__).resolve().parent +SRC = PKG.parent / 'rank7-joint-endframes' +ROOT = PKG.parent.parent +sys.path.insert(0, str(PKG)) +import lift as L # noqa: E402 + +T, BUFFERS, HELPERS, CENTRES, GUARDS = 740, 91, 408, 8, 2 +R1_LOCAL = {1: 2443, 2: 707, 3: 232, 4: 108, 5: 18, 8: 8} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def sha(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def load(name, path): + module = types.ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(Path(path).read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +def check_pins(): + sources = L.read(PKG / 'SOURCES.json') + inputs = [f for f in sources['files'] if f['usage'] == 'input'] + need(len(inputs) >= 13, 'pinned PR2979 inputs') + for f in inputs: + need(sha(ROOT / f['path']) == f['sha256'], 'live input pin ' + f['path']) + vendored = L.read(PKG / 'VENDOR.json')['files'] + need(len(vendored) == 6, 'vendored PR3015/PR3021 files') + for f in vendored: + data = (PKG / f['package_path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == f['sha256'] and len(data) == f['bytes'], 'vendored pin ' + f['package_path']) + need(hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() == f['git_blob'], 'vendored Git blob ' + f['package_path']) + return {f['path']: f['sha256'] for f in inputs} + + +def derive_providers(): + frames = load('rank7_frames_r1', SRC / 'vendor/preload_move.py') + registry = L.read(SRC / 'allocation/PROVIDERS.json') + derived = {} + for tag, pid in (('base', 'gauge44'), ('extra', 'extra')): + word = L.read(PKG / f'data/R1-WORD-{tag}.json.gz') + profile, inventory = frames.frame_report(word) + need(profile == word['report']['local_profile'] and inventory == word['report']['width_inventory'], 'frame report ' + tag) + helpers = sorted(set(range(224, 704)) - set(word['removed'])) + widths = [len(word['helper_final'].get(str(h), [0] * 9)) - len(word['start_extra'].get(str(h), [])) for h in helpers] + need(len(helpers) == HELPERS and len(word['centers']) == CENTRES, 'helpers ' + tag) + need(widths == registry[pid]['widths'], 'R1 keeps every ordered helper width of PR2979 ' + tag) + buffers = {r for gate in word['cleanup'] for r in (gate[1:3] if gate[0] == 'add' else gate[1:2]) if r >= 704} + need(buffers == {704 + int(h) for h in word['helper_final']} and len(buffers) == BUFFERS, 'private buffers ' + tag) + local = {int(k): v for k, v in profile.items()} + need(local == R1_LOCAL, 'R1 local profile ' + tag) + derived[pid] = {'widths': widths, 'actual_paid_profile': local} + return derived + + +def optimal_face(providers): + """Re-verify PR3015's R1 cap certificate; return (cap_lo, cap_hi, idle_per_replica, tight predicate, fixed counts).""" + sys.path.insert(0, str(SRC / 'tools')) + import relax as X + import relax_exact as RE + cert = L.read(PKG / 'certificates/R1-RELAX-CAP.json') + loc = {int(k): v for k, v in cert['local_per_call'].items()} + inv = {int(k): v for k, v in cert['inventory_per_call'].items()} + for pv in providers.values(): + need(pv['actual_paid_profile'] == loc and dict(collections.Counter(pv['widths'])) == inv, 'certificate = actual R1 words') + r = RE.verify_basis(cert['local_per_call'], cert['inventory_per_call'], cert['basis_patterns']) + need(r['status'] == 'PASS_EXACT_RELAXATION_CAP' and r['patterns'] == 2551 and r['tight_patterns'] == 12, 'cap certificate') + need((Q(r['cap_lower']), Q(r['cap_upper'])) == (Q(cert['cap_lower']), Q(cert['cap_upper'])), 'cap bracket') + widths, caps = sorted(inv), sorted(X.BINS) + basis = [RE.pattern_of(e, widths, X.BINS) for e in cert['basis_patterns']] + cols = [X.column(p, caps, widths) for p in basis] + Binv = X.rat_inverse([[cols[k][i] for k in range(len(basis))] for i in range(len(cols[0]))]) + Y = [] + for j in range(len(cols[0])): + row = collections.Counter() + for k, p in enumerate(basis): + if p[2] and Binv[k][j]: + row[p[2]] += Binv[k][j] + Y.append(row) + + def tight(cap, ws): + counts = tuple(list(ws).count(w) for w in widths) + idle = cap - sum(ws) + a = X.column((cap, counts, idle), caps, widths) + coeff = collections.Counter({idle: Q(1)} if idle else {}) + for j, aj in enumerate(a): + for k, v in Y[j].items(): + coeff[k] -= aj * v + return not any(v != 0 for v in coeff.values()) + tight_list = [(cap, counts) for cap, counts, idle in X.patterns(X.BINS, widths) + if tight(cap, [w for w, k in zip(widths, counts) for _ in range(k)])] + need(len(tight_list) == 12, 'twelve tight patterns') + rhs = [Q(X.BINS[c]) for c in caps] + [9 * Q(inv[w]) for w in widths] + tcols = [X.column((cap, counts, cap - sum(w * k for w, k in zip(widths, counts))), caps, widths) for cap, counts in tight_list] + + def fixed_count(index): + n = len(rhs) + rows = [[Q(tcols[j][i]) for i in range(n)] + [Q(int(j == index))] for j in range(len(tcols))] + piv, r_ = [], 0 + for col in range(n): + k = next((k for k in range(r_, len(rows)) if rows[k][col] != 0), None) + if k is None: + continue + rows[r_], rows[k] = rows[k], rows[r_] + rows[r_] = [v / rows[r_][col] for v in rows[r_]] + for k2 in range(len(rows)): + if k2 != r_ and rows[k2][col] != 0: + rows[k2] = [a - rows[k2][col] * b for a, b in zip(rows[k2], rows[r_])] + piv.append(col) + r_ += 1 + if any(all(v == 0 for v in row[:n]) and row[n] != 0 for row in rows): + return None + lam = [Q(0)] * n + for k, col in enumerate(piv): + lam[col] = rows[k][n] + return sum(l * b for l, b in zip(lam, rhs)) + name = lambda cap, counts: '%d:%s' % (cap, '+'.join(str(w) for w, k in zip(widths, counts) for _ in range(k)) or 'empty') + fixed = {name(*tight_list[j]): fixed_count(j) for j in range(len(tight_list))} + fixed = {k: v for k, v in fixed.items() if v is not None} + need(fixed.get('32:9+9+9') == Q(93, 4) and fixed.get('48:9+9+9+9+9') == Q(1341, 20) and fixed.get('48:empty') == Q(7619, 20), 'counts fixed on the optimal face') + need(all((T * v).denominator == 1 for v in fixed.values()) and any((74 * v).denominator != 1 for v in fixed.values()), 'integral at T740, not at T74') + need(all(any((t * v).denominator != 1 for v in fixed.values()) for t in range(1, 20)), 'no integral optimum for T < 20') + return (Q(r['cap_lower']), Q(r['cap_upper']), {int(k): Q(v) for k, v in r['idle_per_replica'].items()}, tight, + {k: str(v) for k, v in sorted(fixed.items())}) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--work', type=Path, help='optional fresh directory: writes the T740 allocation and RESULT.json') + args = ap.parse_args() + if not __debug__: + raise SystemExit('refusing python -O: this checker relies on assertions') + start = time.monotonic() + pins = check_pins() + providers = derive_providers() + engine = load('owners2979_r1', SRC / 'allocation/vendor/independent_owners.py') + plan, template = L.read(SRC / 'allocation/vendor/PLAN.json.gz'), L.read(SRC / 'allocation/vendor/TEMPLATE.json.gz') + relocations = L.read(PKG / 'allocation/RELOCATIONS.json') + expected = L.read(PKG / 'allocation/EXPECTED.json') + claimed = {int(k): v for k, v in L.read(PKG / 'allocation/PROFILE.json').items()} + need(len(relocations) == expected['relocations'] == 332, 'relocation count') + Tn, order, dispatch, fill, touched = L.build(SRC / 'allocation', relocations, providers) + need(Tn == T and len(touched) == expected['touched_bins'], 'T740 and touched bins') + payload = {'ORDER.json': L.digest(order), 'DISPATCH.json': L.digest(dispatch), 'FILL.json.gz': L.digest(fill), + 'PROFILE.json': L.digest({str(r): n for r, n in sorted(claimed.items())})} + need(payload == expected['payload_sha256'], 'canonical T740 payloads') + d = {(s, r): p for s, r, p in dispatch} + need(len(d) == len(dispatch) == 9 * T, 'unique literal dispatch') + t0 = time.monotonic() + result, win, _ = engine.check(T, order, fill, d, claimed, plan, template, providers) + engine_seconds = time.monotonic() - t0 + need(result['roles'] == 9 * T * HELPERS == 2717280 and result['rank_mass'] == 65088 * T, 'complete roles and mass') + physical = result['live'] + HELPERS + CENTRES + BUFFERS + GUARDS + need(physical == expected['physical'] == 663549, 'physical stock') + cap_lo, cap_hi, idle_rep, tight, fixed = optimal_face(providers) + idle = {int(k): v for k, v in result['idle'].items()} + need(idle == {r: T * n for r, n in idle_rep.items()}, 'literal idle histogram = 740 x optimal basic idle profile') + width = {pid: pv['widths'] for pid, pv in providers.items()} + contents = collections.defaultdict(list) + for t, h, o, c, p, z in fill['rows']: + contents[o, c, p].append(width[d[tuple(order[t])]][h]) + census = collections.Counter() + for (o, c), (cap, lo, hi) in win.items(): + for p in range(112): + census[cap, tuple(sorted(contents.get((o, c, p), [])))] += 1 + need(all(tight(cap, ws) for cap, ws in census), 'every literal bin pattern is on the optimal face') + sys.path.insert(0, str(SRC / 'tools')) + import root as R + lo, hi = R.kappa_from_profile(claimed, T) + need((lo, hi) == (cap_lo, cap_hi), 'exact root bracket of the literal profile = R1 fixed-capacity cap bracket') + claim3015 = L.read(PKG / 'comparators/PR3015-CLAIM.json') + claim3021 = L.read(PKG / 'comparators/PR3021-OUTER-CLAIM.json') + base_profile = {int(k): v for k, v in L.read(PKG / 'comparators/PR3015-PROFILE.json').items()} + need(base_profile == {int(k): v for k, v in claim3015['profile'].items()}, 'PR3015 profile file = its claim') + b_lo, b_hi = R.kappa_from_profile(base_profile, 74) + need(Q(claim3015['kappa']) < b_lo < b_hi < cap_lo, 'PR3015 literal T74 root below the R1 cap') + moment = load('moment_r1', PKG / 'tools/audit_allocation_moment.py') + with tempfile.TemporaryDirectory() as tmp: + cand, base = Path(tmp) / 'candidate', Path(tmp) / 'baseline' + cand.mkdir() + base.mkdir() + (cand / 'ORDER.json').write_bytes(L.canonical(order)) + (cand / 'PROFILE.json').write_bytes(L.canonical({str(r): n for r, n in sorted(claimed.items())})) + shutil.copyfile(PKG / 'comparators/PR3015-CLAIM.json', base / 'CLAIM.json') + shutil.copyfile(SRC / 'allocation/ORDER.json', base / 'ORDER.json') + shutil.copyfile(PKG / 'comparators/PR3015-PROFILE.json', base / 'PROFILE.json') + audit = moment.run(cand, base) + need(audit['status'] == 'PASS_SEPARATE_EXACT_RATIONAL_FRONTIER_MOMENT', 'moment auditor') + target = Q(audit['target']) + need(Q(audit['previous']) == Q(claim3015['kappa']) < target < lo, 'strict gain over the PR3015 headline') + need(Q(claim3021['kappa']) == Q(claim3021['kappa_rational']) < target, 'strict gain over the PR3021 released headline') + claim = L.read(PKG / 'CLAIM.json') + need(Q(claim['kappa']) == target and Q(claim['complex_lower']) == Q(audit['outer_endpoint']), 'claimed headline') + need(Q(claim['gain_over_pr3015']) == target - Q(claim3015['kappa']), 'claimed gain over PR3015') + need(Q(claim['gain_over_pr3021']) == target - Q(claim3021['kappa']), 'claimed gain over PR3021') + need((Q(claim['root_lower']), Q(claim['root_upper'])) == (lo, hi) == (Q(claim['fixed_inventory_cap']['cap_lower']), Q(claim['fixed_inventory_cap']['cap_upper'])), 'claimed root = cap') + need({int(k): v for k, v in claim['profile'].items()} == claimed and claim['replicas'] == T and claim['physical_families'] == physical, 'claimed profile/T/physical') + out = dict(status='PASS_RANK7_R1_T740_CAP', T=T, calls=9 * T, roles=result['roles'], relocations=len(relocations), + touched_bins=len(touched), physical=physical, idle=result['idle'], profile=result['profile'], + pattern_census={'%d:%s' % (cap, '+'.join(map(str, ws)) or 'empty'): n for (cap, ws), n in sorted(census.items())}, + fixed_on_optimal_face_per_replica=fixed, root_lower=str(lo), root_upper=str(hi), cap_lower=str(cap_lo), cap_upper=str(cap_hi), + pr3015_literal_root=[str(b_lo), str(b_hi)], target=audit['target'], target_decimal=audit['target_decimal'], + gain_over_pr3015=audit['gain'], gain_over_pr3015_decimal=audit['gain_decimal'], gain_over_pr3021=str(target - Q(claim3021['kappa'])), + gain_over_pr3021_float=float(target - Q(claim3021['kappa'])), payload_sha256=payload, input_sha256=pins, + engine_seconds=round(engine_seconds, 1), seconds=round(time.monotonic() - start, 1), + scope='Finite literal T740 owner geometry, paid profile and exact moment for PR3015\'s R1 words; their word/native ' + 'checks are inherited from PR3015/PR2979 unchanged; complete admission/outer release at T740 is separate.') + if args.work: + work = args.work.resolve() + need(not work.exists() and not work.is_relative_to(PKG), 'fresh work directory outside the package') + L.write(work / 'allocation', T, order, dispatch, fill, claimed) + (work / 'RESULT.json').write_text(json.dumps(out, sort_keys=True, indent=1) + '\n') + print(json.dumps({k: out[k] for k in ('status', 'T', 'roles', 'relocations', 'physical', 'idle', 'target_decimal', 'gain_over_pr3015_decimal', 'gain_over_pr3021_float', 'seconds')})) + print('PASS_RANK7_R1_T740_CAP', audit['target_decimal']) + + +if __name__ == '__main__': + main()