diff --git a/research/rank7-final-fill-controls/README.md b/research/rank7-final-fill-controls/README.md new file mode 100644 index 0000000000..b478e8308a --- /dev/null +++ b/research/rank7-final-fill-controls/README.md @@ -0,0 +1,268 @@ +# V45 final-word controls fail the complete packing budget + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +Apache-2.0. No independent human or formal-kernel review is claimed. + +Every control that restores at least one of PR2979's four V45 endpoints from +rank seven to rank eight fails its claimed complex saving, even after allowing +arbitrary fractional repacking in the fixed capacity model. The control retaining +only helper249 at rank seven has complete moment **at least 1.000005090277**. +The fully coordinated final word passes at the same saving. + +This is a finite independent invoice audit and a scoped obstruction. It does +not report a defect in the shipped joint construction, a new supplier, or a +new kappa. The selected frontier is unchanged. + +## Exact object and difference from earlier checks + +The source is [PR2979](https://github.com/CrocSwap/integer-mult-bounds/pull/2979), +head `be191346391661f4d35fc0d1508d0a6029572576`. The base is +`463113d675af7410ac91d53a4fed51ec6494eb9a`, priority revision 6. +All twelve live inputs in [SOURCES.json](SOURCES.json) match both the base +checkout and the original PR head. No predecessor Python code is executed, +imported or copied. Coordination is in [discussion #2612](https://github.com/CrocSwap/integer-mult-bounds/discussions/2612). + +The four original helper names are `249,251,265,267`; their compact allocation +indices, derived from the actual removed-role lists, are `25,27,41,43`. +Each has zero entrance and the common final seven-dimensional space +`[256,128,64,35,16,11,5]`. Its own parent endpoint has dimension eight and +contains that space. + +A control replaces any subset of these four terminal entries with their parent +rank-eight entries. **All final scalar gates, partner frames, later extraction +and rewrite stages, other endpoints, dispatch and private names stay fixed.** +Both providers independently pass the resulting monotone frame recount. Each +widened endpoint adds exactly one rank-one terminal child per invocation and +one unit of helper residual width. The fixed T74 dispatch has 666 invocations. + +These are controls of the **final word**, not reconstructions of the original +stage-one experiment. [PR2993](https://github.com/CrocSwap/integer-mult-bounds/pull/2993) +and the [V45 profile audit](../rank7-v45-profile-audit/README.md) already check +that original group's local profile and losing singleton guide price. +[PR3014](https://github.com/CrocSwap/integer-mult-bounds/pull/3014) proves a complete +cost increase when lowering V45 on the older PR2942 assignment. This package +answers its changed-final-fill question: it checks the actual final assignment, +then bounds all repackings of these explicitly different controls. +[PR2987](https://github.com/CrocSwap/integer-mult-bounds/pull/2987)'s chronological +packing audit and later allocation refinements retain their separate scope. +The earlier [single-lowering](../rank7-v45-single-lowering/README.md) and +[shipped-invoice](../rank7-v45-shipped-invoice/README.md) checks by jwr establish +the recorded guide margins and endpoint/buffer inventory. They do not check +these counterfactual final allocations or the complete packing lower bound. + +## Complete recursive invoice and literal capacity witnesses + +The checker reads all 271,728 placements and all 149,184 bins. It reconstructs +source availability intervals from the source event schedule, checks each +replica's stage order, unique roles, distinct physical families within a call, +nonoverlapping coordinate masks and compact prefixes. Empty bins are charged. +The two independently recounted local profiles are + +```text +{1:2445, 2:706, 3:232, 4:108, 5:18, 8:8}. +``` + +The actual dispatch is 250 base and 416 extra calls. The independently rebuilt +idle profile and complete profile are + +```text +idle {1:17310, 3:4956, 5:1728, 48:28190} +complete {1:1645680, 2:470196, 3:159468, 4:71928, + 5:13716, 8:5328, 48:28190}. +``` + +The complete rank mass is 4,816,512. The per-call local rank mass minus helper +width mass is 1,856; widening an endpoint increases both by one. Consequently, +a legal control allocation must replace its idle invoice as well. Retaining +the final idle profile while adding the control's terminal children violates +the complete rank-mass identity. + +Every one of the 2,664 V45 occurrences lies in a bin with zero idle remainder. +Grant free compaction inside each bin and even arbitrary rearrangement of its +disjoint axes. Restoring any endpoint to rank eight still exceeds capacity. + +| Widened endpoints | Overfull bins | Excess width | Whole-occurrence width that must leave those bins | +|---|---:|---:|---:| +| 249 only | 646 | 666 | at least 5,110 | +| 251 only | 650 | 666 | at least 5,142 | +| 265 only | 650 | 666 | at least 5,142 | +| 267 only | 650 | 666 | at least 5,142 | +| 251,265,267 (only 249 remains lowered) | 1,938 | 1,998 | at least 15,354 | +| all four | 2,578 | 2,664 | at least 20,428 | + +For example, bin `(owner=2, child=0, port=99)` has capacity 16. It contains +helper index 27 at time 0 with width 7 and helper index 177 at time 4 with width 9. +Widening original helper251 makes the required width 17. The result contains +an explicit witness and a digest of every witness for each of the sixteen +subsets; `--witnesses` can emit them all. + +For any capacity-preserving reassignment, each overfull source bin must lose +at least one of its original whole helper occurrences. In these actual bins +the excess is at most two and every occupant is wider than the excess, so the +minimum total width deleted from a bin is its shortest new occupant width. +Summing those minima gives the last column. The bound is sharp in the +relaxation that permits deletion into a free sink. It does not construct a +legal relocation, price movement, or allow required occurrences to disappear. + +## Why no repacking rescues the controls at the source saving + +Use the exact claimed complex saving + +```text +a = 1729033982646513517717 / 1000000000000000000000000. +``` + +Write `t_r = r^(1-a)`, with `t_0=0`. There are, per replica, 672 bins of capacity 8 +and 448 each of capacities 16, 32 and 48. The local word has nine invocations per +replica and width inventory `{4:26,5:2,6:16,7:52,8:99,9:213}` per invocation. +Its complete normalized moment is the per-replica tariff sum divided by +`896*t_73`. + +For a capacity-c bin containing n_w helpers of width w, the idle tariff is +`t_(c-sum(w*n_w))`. Define helper potentials + +```text +p9 = (t3 - t48)/5 p8 = (3*p9 - t5)/4 +p7 = 2*p8 - p9 p6 = 3*p8 - 2*p9 +p5 = -t5 p4 = t1 + 4*p8 - 3*p9 +``` + +and bin potentials + +```text +alpha8 = -p8, alpha16 = -2*p8, alpha32 = -4*p8, alpha48 = t48. +``` + +These solve the ten equalities of the retained fractional basis. The checker +independently enumerates **all 2,551 patterns** over widths 4 through 9 in the +four capacities and verifies + +```text +alpha_c + sum(n_w*p_w) <= t_(c-sum(w*n_w)). +``` + +Twelve patterns are symbolically tight. Every other inequality has a strictly +positive rational lower bound. Summing these inequalities proves a lower bound +for the entire idle bill, including fractional mixtures and allocations that +ignore chronology. Adding every local child gives a lower bound for the +complete recursive invoice, not only its idle component. +Explicitly, for bin counts `B_c`, width inventory `I_w` per call and local +profile `L_r` per call, the lower bill per replica is + +```text +sum_c B_c*alpha_c + 9*sum_w I_w*p_w + 9*sum_r L_r*t_r. +``` + +The checker derives `B_c` from all source bins and independently binds the +source fractional basis to these bin counts and to `9*I_w`. + +Widening one endpoint changes that bound per invocation by + +```text +t1 + p8 - p7 = (20*t1 + t3 + 5*t5 - t48)/20. +``` + +This direction is strictly positive for every `a>0`: the positive ranks 1, 3, 5 +have total rank mass 48, and each has `r^(-a) > 48^(-a)`. The dual feasibility +and the following numerical separations are certified at the stated source +saving; no claim of dual optimality over every saving is needed. + +| Widened endpoint count | Certified lower bound on complete moment, rounded downward | +|---:|---:| +| 1 | 1.000001693386 | +| 2 | 1.000003391832 | +| 3 | 1.000005090277 | +| 4 | 1.000006788723 | + +The baseline fractional bound has headroom at this saving, and the **actual** +complete baseline profile independently satisfies the strict moment inequality. +Thus rejecting the controls is not caused by testing above the joint word's +own accepted numeric endpoint. No numerical root search or additional endpoint +digits are supplied. + +`dual.py` uses integer arithmetic only. Successive floor/ceiling integer square +roots enclose `r^(1/2^j)` on a 256-bit grid. The first 128 binary exponent bits +of a give a lower exponent; one last root bounds the omitted tail. Outward +rounded products enclose `r^a`, and division gives bounds on `r^(1-a)`. +Rational linear combinations then enclose every dual slack and moment margin. +All full rational bounds are retained in [RESULT.json](RESULT.json). + +## Physical ledger and remaining obligations + +The nominal stock arithmetic is preserved exactly: + +```text +66,304 live families + 408 helper names + 8 centres ++ 91 private buffers + 2 coefficient families = 66,813. +``` + +The checker binds the 91 private names to the actual cleanup operand inventory +and preserves all 5,207 cleanup operations per provider. This is namespace and +invoice accounting; private zero-return and physical reuse are separate +obligations. No scalar, wrapper, movement, prefix or precision charge is +removed. Unpriced costs are not assumed to vanish: the packing relaxation +rejects the controls already, before additional physical implementation costs. + +The scientific scope stops at the fixed whole-helper capacity model. Changed +words, partner frames, helper splitting/coding, capacity pools, consumer +contracts or local rank profiles are outside it. Native phases and full warp +semantics, dirty-input operator identities, complete ownership/backing and +movement, physical scalar implementations, prefix/precision/tape, outer release +and all-size/compiler implications are not checked. Both supplier caps and the +selected exponent remain unmodified; no new bit-side cap or outer transfer is +asserted. Failure of the complex budget is sufficient for this control test. + +## Reproduce + +Python 3.12, standard library only, no network or solver: + +```sh +python3 -B scripts/research_package.py --package research/rank7-final-fill-controls +``` + +The verifier prints + +```text +PASS_RANK7_FINAL_FILL_CONTROLS cases=16 rejected_controls=15 roles=271728 bins=149184 packing_patterns=2551 +``` + +The registered hook also runs thirteen behavioral groups. They include an +explicit-point-set frame oracle, algebraic square/cube bounds for the interval +engine, a separate pattern enumerator, all-subset axis-spill counts, exhaustive +small deletion subsets, and semantic rejection of missing/duplicate roles, +family conflicts, unavailable windows, overlapping/noncompact slices, omitted +source bins, missing private names, unpaid children, an infeasible dual and an +omitted pattern. An optimized Git-free export passes, and a changed source +byte is rejected before decoding. Checks use exceptions and survive `-O`. + +`verify.py --emit` prints the deterministic result. `verify.py --witnesses +WITNESSES.json` exclusively creates the optional full witness file. Default +verification does not write repository artifacts. The full result requires +about five seconds locally; behavioral controls take about twelve seconds. + +## Open next questions + +The two questions in [TASK.json](TASK.json) distinguish original stage-one +attribution from supplier admission. A matched complete comparison of the +original parent/joint/single words needs separately legal allocations and all +charges; these final-word controls do not supply it. A physical admission audit +should join the exact final fill to the native/private evidence and choose one +remaining consumer cost. Another lowering or packing search is not started. + +## Predecessor credit + +Marius-Paul Dumitrean (mdumitrean) supplied PR2979's construction, +PR2942 parent words, final allocation and fractional basis. Nick Petalas supplied +PR2993's independent frame audit and PR3014's old-assignment obstruction and +handoff. Ross Richardson supplied PR2987's independent chronological packing +analysis. Jeremy Kothe supplied the frame/cleanup conventions and rewrite +lineage; Mason Hale supplied PR2917's T74 call order and dispatch and, with +Jeremy Diviney, the paired-extraction chain. +Credit the retained V45 price/inventory checks by jwr (James Reed; PR3112 and +PR3119) and Gonzalo Mier's V45 profile audit (PR3079) as complementary evidence. +Retain Yiyang Lu's allocation lineage, Tekalign's source-window/owner conventions, +Dugongue's packing and owner-engine lineage (PR2863, PR2839), icekylinx, Sagar +Thakrar, themilkman216 and the geometry/native/owner contributors credited by +the immutable source package. The earlier native endpoint audits, Nick Petalas's +PR3006 and PR3008 and ToikY's PR3038, are credited as complementary evidence, +not imported implementations or newly checked here. diff --git a/research/rank7-final-fill-controls/RESULT.json b/research/rank7-final-fill-controls/RESULT.json new file mode 100644 index 0000000000..423f58f267 --- /dev/null +++ b/research/rank7-final-fill-controls/RESULT.json @@ -0,0 +1,4755 @@ +{ + "baseline": { + "bins": 149184, + "calls": 666, + "centres": 8, + "coefficient_families": 2, + "complete_profile": { + "1": 1645680, + "2": 470196, + "3": 159468, + "4": 71928, + "48": 28190, + "5": 13716, + "8": 5328 + }, + "helpers": 408, + "idle_profile": { + "1": 17310, + "3": 4956, + "48": 28190, + "5": 1728 + }, + "live_families": 66304, + "physical_families": 66813, + "private_buffers": 91, + "provider_counts": { + "extra": 416, + "gauge44": 250 + }, + "rank_mass": 4816512, + "roles": 271728 + }, + "cases": [ + { + "added_local_children": {}, + "added_width": 0, + "all_packings_rejected_at_source_saving": false, + "all_witnesses_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "feasible_without_reassignment": true, + "first_witness": null, + "moved_occurrences_lower_bound": 0, + "moved_width_lower_bound": 0, + "overfull_bins": 0, + "retained_lowered": [ + 249, + 251, + 265, + 267 + ], + "total_excess": 0, + "touched_bins": [], + "widened": [] + }, + { + "added_local_children": { + "1": 666 + }, + "added_width": 666, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "cb65c6bc5c4c58cb79572cbd630b044a8c07fcb510be5ee50b9e6ae8b0bf4516", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 7 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 25, + 7 + ], + [ + 7, + 10, + 206, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 646, + "moved_width_lower_bound": 5110, + "overfull_bins": 646, + "retained_lowered": [ + 251, + 265, + 267 + ], + "total_excess": 666, + "touched_bins": [ + { + "added_width": 1, + "count": 626, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 20, + "old_idle": 0 + } + ], + "widened": [ + 249 + ] + }, + { + "added_local_children": { + "1": 666 + }, + "added_width": 666, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "694fde2a75623580b764a2c6a8a4232b193a3be1bdf3e25459519ee58da10161", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 6 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 27, + 7 + ], + [ + 7, + 10, + 207, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 650, + "moved_width_lower_bound": 5142, + "overfull_bins": 650, + "retained_lowered": [ + 249, + 265, + 267 + ], + "total_excess": 666, + "touched_bins": [ + { + "added_width": 1, + "count": 634, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 16, + "old_idle": 0 + } + ], + "widened": [ + 251 + ] + }, + { + "added_local_children": { + "1": 1332 + }, + "added_width": 1332, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "4eaa1bf3618cec3ebd853466f12d6818087cffe43467ec433c88042bafae7240", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 6 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 27, + 7 + ], + [ + 7, + 10, + 207, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1290, + "moved_width_lower_bound": 10216, + "overfull_bins": 1290, + "retained_lowered": [ + 265, + 267 + ], + "total_excess": 1332, + "touched_bins": [ + { + "added_width": 1, + "count": 1248, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 42, + "old_idle": 0 + } + ], + "widened": [ + 249, + 251 + ] + }, + { + "added_local_children": { + "1": 666 + }, + "added_width": 666, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "1f4c1a9afde3f36902862ea545adda29f40b9977ab6796fef9d54916f95f183b", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 5 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 41, + 7 + ], + [ + 7, + 10, + 208, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 650, + "moved_width_lower_bound": 5142, + "overfull_bins": 650, + "retained_lowered": [ + 249, + 251, + 267 + ], + "total_excess": 666, + "touched_bins": [ + { + "added_width": 1, + "count": 634, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 16, + "old_idle": 0 + } + ], + "widened": [ + 265 + ] + }, + { + "added_local_children": { + "1": 1332 + }, + "added_width": 1332, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "097219003262df4b324ba36e6b29747b6a439b0693077ac6674d9fb5dc41ec94", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 5 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 41, + 7 + ], + [ + 7, + 10, + 208, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1296, + "moved_width_lower_bound": 10252, + "overfull_bins": 1296, + "retained_lowered": [ + 251, + 267 + ], + "total_excess": 1332, + "touched_bins": [ + { + "added_width": 1, + "count": 1260, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 36, + "old_idle": 0 + } + ], + "widened": [ + 249, + 265 + ] + }, + { + "added_local_children": { + "1": 1332 + }, + "added_width": 1332, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "fd977534bc2f3acab7b637ba23088702f83a1838b57058f5240af143aa820012", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 5 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 41, + 7 + ], + [ + 7, + 10, + 208, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1294, + "moved_width_lower_bound": 10248, + "overfull_bins": 1294, + "retained_lowered": [ + 249, + 267 + ], + "total_excess": 1332, + "touched_bins": [ + { + "added_width": 1, + "count": 1256, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 38, + "old_idle": 0 + } + ], + "widened": [ + 251, + 265 + ] + }, + { + "added_local_children": { + "1": 1998 + }, + "added_width": 1998, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "92d616f8ab02b1527c83d32b8d8cbd6ee8a86510368a828f1895549bf2530b5c", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 5 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 41, + 7 + ], + [ + 7, + 10, + 208, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1934, + "moved_width_lower_bound": 15322, + "overfull_bins": 1934, + "retained_lowered": [ + 267 + ], + "total_excess": 1998, + "touched_bins": [ + { + "added_width": 1, + "count": 1870, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 64, + "old_idle": 0 + } + ], + "widened": [ + 249, + 251, + 265 + ] + }, + { + "added_local_children": { + "1": 666 + }, + "added_width": 666, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "102bdb636441910b10d7a9e43ee3a64b1efb794e5ee76a47252a3038fbfc34b6", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 650, + "moved_width_lower_bound": 5142, + "overfull_bins": 650, + "retained_lowered": [ + 249, + 251, + 265 + ], + "total_excess": 666, + "touched_bins": [ + { + "added_width": 1, + "count": 634, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 16, + "old_idle": 0 + } + ], + "widened": [ + 267 + ] + }, + { + "added_local_children": { + "1": 1332 + }, + "added_width": 1332, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "48087bf3d976c82952a8ccaf703fe90120b2352a1b4deaa49214d8bf627118f2", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1296, + "moved_width_lower_bound": 10252, + "overfull_bins": 1296, + "retained_lowered": [ + 251, + 265 + ], + "total_excess": 1332, + "touched_bins": [ + { + "added_width": 1, + "count": 1260, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 36, + "old_idle": 0 + } + ], + "widened": [ + 249, + 267 + ] + }, + { + "added_local_children": { + "1": 1332 + }, + "added_width": 1332, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "114ccc69d6970fadbc7ece5e9fdd5bc52bc3266ee0221b78fdc13fcbebbd8ce0", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1300, + "moved_width_lower_bound": 10284, + "overfull_bins": 1300, + "retained_lowered": [ + 249, + 265 + ], + "total_excess": 1332, + "touched_bins": [ + { + "added_width": 1, + "count": 1268, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 32, + "old_idle": 0 + } + ], + "widened": [ + 251, + 267 + ] + }, + { + "added_local_children": { + "1": 1998 + }, + "added_width": 1998, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "b75bc754cf1bcda9717b7ab681a292ea2c125699662fe154fd723559f6edc370", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1940, + "moved_width_lower_bound": 15358, + "overfull_bins": 1940, + "retained_lowered": [ + 265 + ], + "total_excess": 1998, + "touched_bins": [ + { + "added_width": 1, + "count": 1882, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 58, + "old_idle": 0 + } + ], + "widened": [ + 249, + 251, + 267 + ] + }, + { + "added_local_children": { + "1": 1332 + }, + "added_width": 1332, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "76f78f59d94d67cc56ed3d61e1e633f45cf937f294bac40588ff6c3f0d2e0c12", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1294, + "moved_width_lower_bound": 10248, + "overfull_bins": 1294, + "retained_lowered": [ + 249, + 251 + ], + "total_excess": 1332, + "touched_bins": [ + { + "added_width": 1, + "count": 1256, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 38, + "old_idle": 0 + } + ], + "widened": [ + 265, + 267 + ] + }, + { + "added_local_children": { + "1": 1998 + }, + "added_width": 1998, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "7c87d867f095d70b1bb602cd5ce531574d2d126abcca1efe01cac109df725a3a", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1940, + "moved_width_lower_bound": 15358, + "overfull_bins": 1940, + "retained_lowered": [ + 251 + ], + "total_excess": 1998, + "touched_bins": [ + { + "added_width": 1, + "count": 1882, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 58, + "old_idle": 0 + } + ], + "widened": [ + 249, + 265, + 267 + ] + }, + { + "added_local_children": { + "1": 1998 + }, + "added_width": 1998, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "4a6340b56e7ae3c469268a1fe3444d9fe0dffd5a651d7a99be04c115c1451a00", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 1938, + "moved_width_lower_bound": 15354, + "overfull_bins": 1938, + "retained_lowered": [ + 249 + ], + "total_excess": 1998, + "touched_bins": [ + { + "added_width": 1, + "count": 1878, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 60, + "old_idle": 0 + } + ], + "widened": [ + 251, + 265, + 267 + ] + }, + { + "added_local_children": { + "1": 2664 + }, + "added_width": 2664, + "all_packings_rejected_at_source_saving": true, + "all_witnesses_sha256": "69086827938cc3bf3096f25122c22ee4338bd811f2cdec4902bac554298d3071", + "feasible_without_reassignment": false, + "first_witness": { + "bin": [ + 0, + 2, + 4 + ], + "capacity": 16, + "excess": 1, + "extra_width": 1, + "minimum_evacuated_width": 8, + "placements": [ + [ + 0, + 2, + 43, + 7 + ], + [ + 7, + 10, + 209, + 9 + ] + ], + "source_window": [ + -1, + 10 + ], + "used_before": 16 + }, + "moved_occurrences_lower_bound": 2578, + "moved_width_lower_bound": 20428, + "overfull_bins": 2578, + "retained_lowered": [], + "total_excess": 2664, + "touched_bins": [ + { + "added_width": 1, + "count": 2492, + "old_idle": 0 + }, + { + "added_width": 2, + "count": 86, + "old_idle": 0 + } + ], + "widened": [ + 249, + 251, + 265, + 267 + ] + } + ], + "helper_indices": { + "249": 25, + "251": 27, + "265": 41, + "267": 43 + }, + "limits": [ + "No control repacking is constructed or priced.", + "These controls retain all final stage-2/3 scalar and frame edits.", + "Original stage-1 guide controls remain separate predecessor evidence.", + "No native phase, dirty restoration, movement, precision/tape or outer/all-size admission." + ], + "packing_relaxation": { + "actual_baseline_margin_interval": [ + "-467135356707554589004619755778945833344974544949198837356297/4284307301780699230672126445321452590570989432628700869459930608292785796677632", + "-467135356707549895092850677663423237645815335454682465452787/4284307301780699230672126445321452590570989432628700869459930608292785796677632" + ], + "bins_per_replica": { + "16": "448", + "32": "448", + "48": "448", + "8": "672" + }, + "cost_direction": { + "1": "1", + "3": "1/20", + "48": "-1/20", + "5": "1/4" + }, + "interval_method": "integer square roots; 256-bit tariff grid, 128 exponent bits", + "minimum_strict_slack_lower": "9381475436729307759575807284486059934382985397013541490562639727951411764939/2315841784746323908471419700173758157065399693312811280789151680158262592798720", + "pattern_count": 2551, + "patterns_sha256": "83d5128d6a0bf2548e312bedbba0848ececfb66d48dc4650acc10efddcced886", + "per_occurrence_extra_cost_interval": [ + "7093607356294933678425019761958257832162375538708145949687913740252474034283/578960446186580977117854925043439539266349923328202820197287920039565648199680", + "7093607356294933678425019761958257851557769559122834780679630881684034117011/578960446186580977117854925043439539266349923328202820197287920039565648199680" + ], + "per_replica_excess_over_896_times_73_power": [ + { + "all_packings_rejected": false, + "lower": "-95082521318202475072414040555912027526267165671027345578711589224604784651/289480223093290488558927462521719769633174961664101410098643960019782824099840", + "upper": "-11885315164775309384051755069449358895678018899389037299675039185412859449/36185027886661311069865932815214971204146870208012676262330495002472853012480", + "widened_count": 0 + }, + { + "all_packings_rejected": true, + "complete_moment_lower_bound": "536983215263948163811576201602028967552576574063678123113910035809936213797033983/536982305945360106411602549025603588802625492230600458536181507365518080468807296", + "complete_moment_lower_decimal": "1.000001693386", + "lower": "6365230116401799815568034977651249657572831543652044099699110926933297586809/57896044618658097711785492504343953926634992332820282019728792003956564819968", + "upper": "6365230116401799815568034977651313078036960781022610628836456852267978217307/57896044618658097711785492504343953926634992332820282019728792003956564819968", + "widened_count": 1 + }, + { + "all_packings_rejected": true, + "complete_moment_lower_bound": "18794444455471289060606719968659942676500495482653618240234695327613991373988908101/18794380708087603724406089215896125608091892228071016048766352757793132816408255360", + "complete_moment_lower_decimal": "1.000003391832", + "lower": "63747383685336200630752763817068408603254582602191468342569820858557580652741/289480223093290488558927462521719769633174961664101410098643960019782824099840", + "upper": "31873691842668100315376381908534362825767515980710609293380984418081542524331/144740111546645244279463731260859884816587480832050705049321980009891412049920", + "widened_count": 2 + }, + { + "all_packings_rejected": true, + "complete_moment_lower_bound": "18794476376704392387808272881248871488660810873078502171482539401880215265081626797/18794380708087603724406089215896125608091892228071016048766352757793132816408255360", + "complete_moment_lower_decimal": "1.000005090277", + "lower": "95668616788663402183665352745880568918645007486122716186644087082448673371437/289480223093290488558927462521719769633174961664101410098643960019782824099840", + "upper": "95668616788663402183665352745880885912885260017729384029341653410986279010789/289480223093290488558927462521719769633174961664101410098643960019782824099840", + "widened_count": 3 + }, + { + "all_packings_rejected": true, + "complete_moment_lower_bound": "18794508297937495715009825793837800300821126263503386102730383476146439156174345493/18794380708087603724406089215896125608091892228071016048766352757793132816408255360", + "complete_moment_lower_decimal": "1.000006788723", + "lower": "127589849891990603736577941674692729234035432370053964030718353306339766090133/289480223093290488558927462521719769633174961664101410098643960019782824099840", + "upper": "31897462472997650934144485418673261543558872018509387367980334496452368243229/72370055773322622139731865630429942408293740416025352524660990004945706024960", + "widened_count": 4 + } + ], + "saving": "1729033982646513517717/1000000000000000000000000", + "tight_patterns": [ + [ + 8, + [ + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 0, + 2, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 1, + 0, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 4, + 0 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 1, + 2, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 1, + 0, + 1, + 2 + ] + ], + [ + 32, + [ + 0, + 1, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 1, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 5 + ] + ] + ] + }, + "providers": { + "extra": { + "baseline_profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "cleanup_operations": 5207, + "controls": [ + { + "local_profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [], + "widened": [], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251, + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251, + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251, + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2449, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251, + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 48, + "8": 103, + "9": 213 + } + } + ], + "private_names": [ + 930, + 932, + 934, + 953, + 955, + 969, + 971, + 981, + 986, + 997, + 1002, + 1003, + 1008, + 1011, + 1013, + 1015, + 1018, + 1024, + 1027, + 1029, + 1031, + 1034, + 1035, + 1041, + 1043, + 1045, + 1050, + 1057, + 1059, + 1061, + 1066, + 1067, + 1073, + 1075, + 1077, + 1082, + 1089, + 1091, + 1093, + 1098, + 1099, + 1112, + 1116, + 1128, + 1132, + 1152, + 1153, + 1154, + 1155, + 1156, + 1157, + 1158, + 1159, + 1188, + 1189, + 1202, + 1203, + 1204, + 1205, + 1212, + 1213, + 1214, + 1215, + 1216, + 1217, + 1235, + 1236, + 1237, + 1247, + 1258, + 1259, + 1260, + 1261, + 1270, + 1271, + 1276, + 1277, + 1278, + 1279, + 1284, + 1285, + 1286, + 1287, + 1288, + 1289, + 1290, + 1291, + 1292, + 1293, + 1294, + 1295 + ], + "v45_events": [ + [ + 249, + [ + "A", + 2036 + ], + [], + [ + 296 + ], + 1 + ], + [ + 251, + [ + "A", + 2038 + ], + [], + [ + 168 + ], + 1 + ], + [ + 249, + [ + "A", + 2046 + ], + [ + 296 + ], + [ + 261, + 45 + ], + 1 + ], + [ + 251, + [ + "A", + 2050 + ], + [ + 168 + ], + [ + 133, + 45 + ], + 1 + ], + [ + 265, + [ + "A", + 2190 + ], + [], + [ + 104 + ], + 1 + ], + [ + 267, + [ + "A", + 2192 + ], + [], + [ + 475 + ], + 1 + ], + [ + 265, + [ + "A", + 2200 + ], + [ + 104 + ], + [ + 69, + 45 + ], + 1 + ], + [ + 267, + [ + "A", + 2235 + ], + [ + 475 + ], + [ + 475, + 45 + ], + 1 + ], + [ + 249, + [ + "B", + 459 + ], + [ + 261, + 45 + ], + [ + 261, + 222, + 45 + ], + 1 + ], + [ + 267, + [ + "B", + 459 + ], + [ + 475, + 45 + ], + [ + 261, + 222, + 45 + ], + 1 + ], + [ + 265, + [ + "B", + 460 + ], + [ + 69, + 45 + ], + [ + 133, + 69, + 45 + ], + 1 + ], + [ + 251, + [ + "B", + 460 + ], + [ + 133, + 45 + ], + [ + 133, + 69, + 45 + ], + 1 + ], + [ + 249, + [ + "B", + 461 + ], + [ + 261, + 222, + 45 + ], + [ + 256, + 219, + 40, + 5 + ], + 1 + ], + [ + 265, + [ + "B", + 463 + ], + [ + 133, + 69, + 45 + ], + [ + 261, + 133, + 69, + 45 + ], + 1 + ], + [ + 265, + [ + "B", + 467 + ], + [ + 261, + 133, + 69, + 45 + ], + [ + 256, + 128, + 64, + 40, + 27, + 5 + ], + 2 + ], + [ + 267, + [ + "B", + 468 + ], + [ + 261, + 222, + 45 + ], + [ + 261, + 133, + 69, + 38, + 21, + 11 + ], + 3 + ], + [ + 251, + [ + "B", + 469 + ], + [ + 133, + 69, + 45 + ], + [ + 267, + 128, + 64, + 40, + 16, + 5 + ], + 3 + ], + [ + 249, + [ + "B", + 470 + ], + [ + 256, + 219, + 40, + 5 + ], + [ + 256, + 139, + 64, + 40, + 16, + 5 + ], + 2 + ], + [ + 249, + [ + "restore", + 124 + ], + [ + 256, + 139, + 64, + 40, + 16, + 5 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ], + [ + 251, + [ + "restore", + 125 + ], + [ + 267, + 128, + 64, + 40, + 16, + 5 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ], + [ + 267, + [ + "restore", + 126 + ], + [ + 261, + 133, + 69, + 38, + 21, + 11 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ], + [ + 265, + [ + "restore", + 147 + ], + [ + 256, + 128, + 64, + 40, + 27, + 5 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ] + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + } + }, + "gauge44": { + "baseline_profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "cleanup_operations": 5207, + "controls": [ + { + "local_profile": { + "1": 2445, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [], + "widened": [], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251, + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251, + 265 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2446, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 51, + "8": 100, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2447, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 50, + "8": 101, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2448, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 251, + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 49, + "8": 102, + "9": 213 + } + }, + { + "local_profile": { + "1": 2449, + "2": 706, + "3": 232, + "4": 108, + "5": 18, + "8": 8 + }, + "terminal_added_ranks": [ + [ + 249, + [ + "terminal", + 249 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 251, + [ + "terminal", + 251 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 265, + [ + "terminal", + 265 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ], + [ + 267, + [ + "terminal", + 267 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + [ + 256, + 128, + 64, + 33, + 16, + 9, + 5, + 2 + ], + 1 + ] + ], + "widened": [ + 249, + 251, + 265, + 267 + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 48, + "8": 103, + "9": 213 + } + } + ], + "private_names": [ + 930, + 932, + 934, + 953, + 955, + 969, + 971, + 981, + 986, + 997, + 1002, + 1003, + 1008, + 1011, + 1013, + 1015, + 1018, + 1024, + 1027, + 1029, + 1031, + 1034, + 1035, + 1041, + 1043, + 1045, + 1050, + 1057, + 1059, + 1061, + 1066, + 1067, + 1073, + 1075, + 1077, + 1082, + 1089, + 1091, + 1093, + 1098, + 1099, + 1112, + 1116, + 1128, + 1132, + 1152, + 1153, + 1154, + 1155, + 1156, + 1157, + 1158, + 1159, + 1188, + 1189, + 1202, + 1203, + 1204, + 1205, + 1212, + 1213, + 1214, + 1215, + 1216, + 1217, + 1235, + 1236, + 1237, + 1247, + 1258, + 1259, + 1260, + 1261, + 1270, + 1271, + 1276, + 1277, + 1278, + 1279, + 1284, + 1285, + 1286, + 1287, + 1288, + 1289, + 1290, + 1291, + 1292, + 1293, + 1294, + 1295 + ], + "v45_events": [ + [ + 249, + [ + "A", + 2036 + ], + [], + [ + 296 + ], + 1 + ], + [ + 251, + [ + "A", + 2038 + ], + [], + [ + 168 + ], + 1 + ], + [ + 249, + [ + "A", + 2046 + ], + [ + 296 + ], + [ + 261, + 45 + ], + 1 + ], + [ + 251, + [ + "A", + 2050 + ], + [ + 168 + ], + [ + 133, + 45 + ], + 1 + ], + [ + 265, + [ + "A", + 2190 + ], + [], + [ + 104 + ], + 1 + ], + [ + 267, + [ + "A", + 2192 + ], + [], + [ + 475 + ], + 1 + ], + [ + 265, + [ + "A", + 2200 + ], + [ + 104 + ], + [ + 69, + 45 + ], + 1 + ], + [ + 267, + [ + "A", + 2235 + ], + [ + 475 + ], + [ + 475, + 45 + ], + 1 + ], + [ + 249, + [ + "B", + 459 + ], + [ + 261, + 45 + ], + [ + 261, + 222, + 45 + ], + 1 + ], + [ + 267, + [ + "B", + 459 + ], + [ + 475, + 45 + ], + [ + 261, + 222, + 45 + ], + 1 + ], + [ + 265, + [ + "B", + 460 + ], + [ + 69, + 45 + ], + [ + 133, + 69, + 45 + ], + 1 + ], + [ + 251, + [ + "B", + 460 + ], + [ + 133, + 45 + ], + [ + 133, + 69, + 45 + ], + 1 + ], + [ + 249, + [ + "B", + 461 + ], + [ + 261, + 222, + 45 + ], + [ + 256, + 219, + 40, + 5 + ], + 1 + ], + [ + 265, + [ + "B", + 463 + ], + [ + 133, + 69, + 45 + ], + [ + 261, + 133, + 69, + 45 + ], + 1 + ], + [ + 265, + [ + "B", + 467 + ], + [ + 261, + 133, + 69, + 45 + ], + [ + 256, + 128, + 64, + 40, + 27, + 5 + ], + 2 + ], + [ + 267, + [ + "B", + 468 + ], + [ + 261, + 222, + 45 + ], + [ + 261, + 133, + 69, + 38, + 21, + 11 + ], + 3 + ], + [ + 251, + [ + "B", + 469 + ], + [ + 133, + 69, + 45 + ], + [ + 267, + 128, + 64, + 40, + 16, + 5 + ], + 3 + ], + [ + 249, + [ + "B", + 470 + ], + [ + 256, + 219, + 40, + 5 + ], + [ + 256, + 139, + 64, + 40, + 16, + 5 + ], + 2 + ], + [ + 249, + [ + "restore", + 124 + ], + [ + 256, + 139, + 64, + 40, + 16, + 5 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ], + [ + 251, + [ + "restore", + 125 + ], + [ + 267, + 128, + 64, + 40, + 16, + 5 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ], + [ + 267, + [ + "restore", + 126 + ], + [ + 261, + 133, + 69, + 38, + 21, + 11 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ], + [ + 265, + [ + "restore", + 147 + ], + [ + 256, + 128, + 64, + 40, + 27, + 5 + ], + [ + 256, + 128, + 64, + 35, + 16, + 11, + 5 + ], + 1 + ] + ], + "width_inventory": { + "4": 26, + "5": 2, + "6": 16, + "7": 52, + "8": 99, + "9": 213 + } + } + }, + "result_kind": "finite capacity certificate and scoped obstruction", + "source_head": "be191346391661f4d35fc0d1508d0a6029572576", + "source_sha256": { + "research/rank7-joint-endframes/CLAIM.json": "436e0d297cbdf195445d3697d496ac675e95210b79e70ce602a6a6667a4c6ce9", + "research/rank7-joint-endframes/allocation/DISPATCH.json": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c", + "research/rank7-joint-endframes/allocation/FILL.json.gz": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "research/rank7-joint-endframes/allocation/ORDER.json": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1", + "research/rank7-joint-endframes/allocation/PROFILE.json": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf", + "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e", + "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "research/rank7-joint-endframes/certificates/RELAX-CAP.json": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e", + "research/rank7-joint-endframes/data/PARENT-base.json.gz": "54ca34c749e3228d7e2df3d8dbf7aa1568c2872490166997c5962f12fd03da35", + "research/rank7-joint-endframes/data/PARENT-extra.json.gz": "eded756dfe8f411c3d1f80a3ac16516f0ea5dd6f9866728b2179b157630fa7b6", + "research/rank7-joint-endframes/data/WORD-base.json.gz": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d", + "research/rank7-joint-endframes/data/WORD-extra.json.gz": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7" + }, + "status": "PASS_RANK7_FINAL_FILL_CONTROLS" +} diff --git a/research/rank7-final-fill-controls/SOURCES.json b/research/rank7-final-fill-controls/SOURCES.json new file mode 100644 index 0000000000..b783111277 --- /dev/null +++ b/research/rank7-final-fill-controls/SOURCES.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "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", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/CLAIM.json" + }, + { + "path": "research/rank7-joint-endframes/allocation/DISPATCH.json", + "usage": "input", + "git_blob": "9544fee4e6ee1f202cee22bfaeaf229ee3b2515e", + "sha256": "65e435bd68e97243c003677271b88485a29d4d0fae2dff1354100404a145e74c", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/DISPATCH.json" + }, + { + "path": "research/rank7-joint-endframes/allocation/FILL.json.gz", + "usage": "input", + "git_blob": "8d4fd644d60ba2c98106dc770803b647afdf0963", + "sha256": "c2136be9434cda511a1a8a44d98f9f72ea5376830a8426674253b4ee351c4c39", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/FILL.json.gz" + }, + { + "path": "research/rank7-joint-endframes/allocation/ORDER.json", + "usage": "input", + "git_blob": "7409c4df1092241729739596c7648bda504e6aad", + "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/ORDER.json" + }, + { + "path": "research/rank7-joint-endframes/allocation/PROFILE.json", + "usage": "input", + "git_blob": "46a83eeda67ab67cccbffe8b7ad8e44368b40ea7", + "sha256": "94a819747f3ced41f1544ada0036c983fc0c92847b9644380f877a06cd7931cf", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/PROFILE.json" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "usage": "input", + "git_blob": "7a1db55a4d53ee99280be4f3ab7d29f7b2033adf", + "sha256": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "usage": "input", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz" + }, + { + "path": "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "usage": "input", + "git_blob": "14de38f85eedf4a96500173576184a439348328c", + "sha256": "b272680de5842f7fd5f442cd0aeadfd317fe6af266ddee1a1e0738a919ba856e", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/certificates/RELAX-CAP.json" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "usage": "input", + "git_blob": "1ca8287d6ae5eb45d87db65b369be8d09ba692b2", + "sha256": "54ca34c749e3228d7e2df3d8dbf7aa1568c2872490166997c5962f12fd03da35", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/data/PARENT-base.json.gz" + }, + { + "path": "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "usage": "input", + "git_blob": "c39913ce24cbce4c841eabcc9b1e5a18e4ccc754", + "sha256": "eded756dfe8f411c3d1f80a3ac16516f0ea5dd6f9866728b2179b157630fa7b6", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/data/PARENT-extra.json.gz" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-base.json.gz", + "usage": "input", + "git_blob": "d9aa96a93fea5f7395e7783aef0bc117c0a0ae89", + "sha256": "abaf67bfcb257528658c906b612f57025617592bd7889828f92b97a5f4f4300d", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/data/WORD-base.json.gz" + }, + { + "path": "research/rank7-joint-endframes/data/WORD-extra.json.gz", + "usage": "input", + "git_blob": "74f6cb64595c21f7726ae77e69437868620bdcee", + "sha256": "e0eaf64c4d5d324693d43889bce1b9e53e8da00402105c8c978fd102f208bed7", + "pin": "head:be191346391661f4d35fc0d1508d0a6029572576:research/rank7-joint-endframes/data/WORD-extra.json.gz" + } + ] +} diff --git a/research/rank7-final-fill-controls/TASK.json b/research/rank7-final-fill-controls/TASK.json new file mode 100644 index 0000000000..bfffee30da --- /dev/null +++ b/research/rank7-final-fill-controls/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "PR2979 final-word V45 terminal controls: complete frozen-fill capacity witnesses and a code-disjoint packing-dual rejection at the source complex saving.", + "scope_change_reason": "The original V45 stage-one/single-control local profiles and old-parent-fill obstruction are already checked. This audits the missing implication at the shipped final fill, retains later stages explicitly, and uses the existing fixed-capacity pattern domain to test whether any repacking can retain the claimed saving. No new lowering or allocation search.", + "bottleneck_link": "A coordinated local improvement must survive its complete residual-width and idle invoice. The final-word single-retained-endpoint control fails even the optimistic complete packing relaxation, independently of physical implementation costs.", + "budget_minutes": 60, + "stop_rule": "Stop after all sixteen final terminal controls, the literal full invoice, the existing 2551-pattern dual and semantic controls. Do not synthesize new allocations, compute new roots or promote a supplier.", + "outcome": "completed", + "evidence": "All 271728 roles and 149184 bins pass the baseline check. Every nonempty V45 terminal-widening subset fails literal capacity; keeping only helper249 lowered overfills 1938 bins by 1998 units and requires at least 15354 whole-helper width units to leave them. An independent integer-square-root enclosure checks all 2551 dual inequalities; the complete moment of that control is at least 1.000005090277 at the exact source saving, even under fractional repacking. See RESULT.json; no new supplier or kappa.", + "author": "commdata2338", + "ai_assistance": "Prepared with substantial OpenAI Codex assistance in derivation, implementation, checking and writing. No independent human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Can the original stage-one V45 experiment be compared using separately legal, fully priced allocations for its parent, joint and single-endpoint words?", + "why_it_matters": "The final-word controls here retain stage-two/three changes; their strict rejection does not assign the total final gain to stage one alone.", + "first_step": "Use the exact stage-one words already retained by PR2993 and construct or certify a complete allocation for each declared comparison, with idle, private and physical charges.", + "blocked_by": "No such matched full allocations are constructed here; a new bounded construction budget and family decision are needed." + }, + { + "question": "Does the checked final-word frame/allocation invoice meet the full native, physical and precision contracts?", + "why_it_matters": "A passing complete recursive histogram and nominal stock arithmetic do not establish supplier admission.", + "first_step": "Join the exact final source and owner placement to the existing native endpoint and peer-private audits, then identify one still-unbound physical consumer cost.", + "blocked_by": "Native closure, arbitrary dirty restoration, backing/movement, precision/tape, outer and all-size/compiler obligations remain separate." + } + ], + "scope_key": "5e0f415b25b13c102653/pr2979-final-fill-v45-terminal-controls", + "selection": { + "kind": "released-handoff refinement", + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2612", + "handoff_pr": 3014, + "card_lookup_seed": "00000000000000000000000000000000", + "track": "independent-verification", + "existing_checks": "PR2993 and rank7-v45-profile-audit cover original local controls; PR3014 covers the older PR2942 fill; PR2987 covers the final allocation. PR3006/3008/3038 cover separate native boundaries." + }, + "source_heads": { + "2979": "be191346391661f4d35fc0d1508d0a6029572576", + "3014": "16e8db5656b4fea487a2212395f39707bf134f7a", + "2987": "02c3047a1e78e6e35e7573c12434ba26f6f9bd96", + "2993": "34a7003866390618b8e8006dc483e7a37a37903f" + }, + "overlap": { + "checked_utc": "2026-10-17T17:28:10+00:00", + "open_prs_fetched_at": "2026-10-17T17:04:11.636955+00:00", + "discussions_fetched_at": "2026-10-17T17:04:42.538402+00:00", + "complete_pagination": true, + "limitation": "Offline cached coverage can miss later changes; merged packages and local ledger were also inspected. No novelty guarantee.", + "final_check": { + "checked_utc": "2026-10-17T17:56:55.955421+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-17T17:49:11.608413+00:00", + "complete_pagination": true, + "records": 253 + }, + "discussions": { + "fetched_at": "2026-10-17T17:52:04.322463+00:00", + "complete_pagination": true, + "records": 2017 + } + }, + "queries": [ + "--task independent-moment", + "terminal widening; V45 final; single-endpoint control; saturated V45", + "--all-terms V45 control" + ], + "nearest_additional_checks": [ + "rank7-v45-profile-audit", + "rank7-v45-single-lowering", + "rank7-v45-shipped-invoice", + "PR3202 native R2 slice; separate source and question" + ], + "limitation": "Offline metadata covers complete paginated records at the stated timestamps, not subsequent work or arbitrary code diffs. The readable board snapshot was read separately." + } + }, + "refresh_checkpoint": { + "checked_utc": "2026-10-17T17:57:07.027080+00:00", + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "canonical_main": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "changed_paths": [], + "priority_revision": 6, + "frozen_inputs_preserved": true + } +} diff --git a/research/rank7-final-fill-controls/VERIFY.json b/research/rank7-final-fill-controls/VERIFY.json new file mode 100644 index 0000000000..a9d22d69e9 --- /dev/null +++ b/research/rank7-final-fill-controls/VERIFY.json @@ -0,0 +1,40 @@ +{ + "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/PROFILE.json", + "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "research/rank7-joint-endframes/certificates/RELAX-CAP.json", + "research/rank7-joint-endframes/data/PARENT-base.json.gz", + "research/rank7-joint-endframes/data/PARENT-extra.json.gz", + "research/rank7-joint-endframes/data/WORD-base.json.gz", + "research/rank7-joint-endframes/data/WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All literal roles/bins, both local frame ledgers, 16 terminal controls, complete invoice, and 2551 exact packing-dual inequalities at the source saving." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Thirteen behavioral groups: finite geometry/price mutations, explicit-span and exact algebraic interval oracles, independent pattern enumeration, all-subset axis spills, optimized Git-free export and source corruption." + } + ] +} diff --git a/research/rank7-final-fill-controls/allocation.py b/research/rank7-final-fill-controls/allocation.py new file mode 100644 index 0000000000..b963d0cabd --- /dev/null +++ b/research/rank7-final-fill-controls/allocation.py @@ -0,0 +1,169 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Literal capacity witnesses, with all source bins included in the invoice.""" + +from collections import Counter, defaultdict +from hashlib import sha256 +import json + +from local import V45, need + + +def digest(value): + return sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def window_table(template, order, plan): + need(template["m"] == 73, "source ambient width 73") + need(len(order) == 666, "666 ordered calls") + times = {} + progress = [0] * 74 + for t, entry in enumerate(order): + need(len(entry) == 2 and all(type(x) is int for x in entry), "call pair") + stage, replica = entry + need(0 <= replica < 74 and stage == progress[replica], "replica stage order") + progress[replica] += 1 + times[replica, stage] = t + need(progress == [9] * 74, "complete T74 calls") + capacities, source_bins = {}, set() + for item in template["idle_children"]: + child, rank = item["child"], item["rank"] + need(type(child) is int and type(rank) is int and 0 < rank <= 48, + "child capacity") + need(child not in capacities or capacities[child] == rank, "consistent capacity") + port = item["port"] + need(type(port) is int and 0 <= port < 112 and (child, port) not in source_bins, + "unique source child/port") + source_bins.add((child, port)) + capacities[child] = rank + need(set(capacities) == set(range(18)), "18 source idle children") + need(source_bins == {(child, port) for child in range(18) for port in range(112)}, + "complete source bin inventory") + local_pairs = {e["stage"]: e["pair"] for e in template["recipe"] if e["kind"] == "local"} + need(set(local_pairs) == set(range(9)), "nine source local pairs") + stage, touched, specs = None, {}, {} + for event in template["execution_schedule"]: + tag = event["kind"] + if tag == "local_cover_sweep": + stage = event["stage"] + touched[local_pairs[stage]] = stage + elif tag == "bridge": + touched[event["src"]] = touched[event["dst"]] = stage + elif tag == "idle_cover_sweep": + for child in event["child_indices"]: + if child in capacities: + need(child not in specs, "one deadline per child") + need(plan["pairs"][str(child)] == event["pair"], "child physical pair") + need(plan["sides"][str(child)] in (0, 1), "child physical side") + specs[child] = (touched.get(event["pair"], -1), stage) + else: + need(tag in ("terminal_Y_translations", "terminal", "bank_padding_cover_sweep", + "translate_every_live_family"), "known source event") + need(set(specs) == set(capacities), "complete deadline inventory") + windows = {} + for replica in range(74): + for child, (start, stop) in specs.items(): + begin = times[replica, start] if start >= 0 else -1 + windows[replica, child] = (capacities[child], begin, times[replica, stop]) + return windows + + +def verify_fill(fill, order, dispatch, plan, windows, local_data): + need(fill["columns"] == ["time", "helper", "owner_replica", "child", "port", "offset"], + "fill columns") + need(len(fill["rows"]) == 666 * 408, "complete role row count") + need(len(dispatch) == 666, "complete dispatch count") + provider_by_call = {} + for stage, replica, provider in dispatch: + key = (stage, replica) + need(key not in provider_by_call and key in map(tuple, order), "unique dispatch call") + need(provider in local_data, "known dispatch provider") + provider_by_call[key] = provider + for stage, replica, provider in fill.get("dispatch_overrides", []): + need(provider_by_call[stage, replica] == provider, "dispatch override binding") + coverage = bytearray(666 * 408) + families = set() + bins = defaultdict(list) + masks = {} + for row in fill["rows"]: + need(len(row) == 6 and all(type(x) is int for x in row), "integer fill row") + t, h, replica, child, port, offset = row + need(0 <= t < 666 and 0 <= h < 408 and 0 <= port < 112, "role bounds") + role = 408 * t + h + need(not coverage[role], "unique call/helper role") + coverage[role] = 1 + need((replica, child) in windows, "existing owner window") + capacity, begin, stop = windows[replica, child] + need(begin < t <= stop, "open-start closed-end source window") + fam = (t, replica, 2 * plan["pairs"][str(child)] + plan["sides"][str(child)], port) + need(fam not in families, "distinct physical helper families in a call") + families.add(fam) + provider = provider_by_call[tuple(order[t])] + width = local_data[provider]["widths"][h] + need(0 <= offset and offset + width <= capacity, "positive source slice fits") + key = (replica, child, port) + bits = ((1 << width) - 1) << offset + need(masks.get(key, 0) & bits == 0, "disjoint occupied source axes") + masks[key] = masks.get(key, 0) | bits + bins[key].append((offset, t, h, width)) + need(all(coverage), "all helper roles present") + for key, mask in masks.items(): + width = sum(row[3] for row in bins[key]) + need(mask == (1 << width) - 1, "compact occupied source prefix") + bins[key].sort() + return bins, Counter(provider_by_call.values()) + + +def bill(bins, windows, counts, local_data): + idle = Counter() + for (replica, child), (capacity, _begin, _stop) in windows.items(): + for port in range(112): + used = sum(row[3] for row in bins.get((replica, child, port), [])) + need(0 <= used <= capacity, "whole bin capacity") + if used < capacity: + idle[capacity - used] += 1 + full = Counter(idle) + for provider, calls in counts.items(): + full.update({r: n * calls for r, n in local_data[provider]["profile"].items()}) + need(sum(r * n for r, n in full.items()) == 74 * 65088, "complete rank-mass identity") + return idle, full + + +def control_case(bins, windows, helper_indices, widened): + need(set(widened) <= set(V45), "only four V45 controls") + selected = {helper_indices[h] for h in widened} + touched = Counter() + witnesses = [] + for key, rows in sorted(bins.items()): + increase = sum(row[2] in selected for row in rows) + if not increase: + continue + capacity, begin, end = windows[key[:2]] + used = sum(row[3] for row in rows) + remaining = capacity - used + touched[remaining, increase] += 1 + excess = increase - remaining + if excess > 0: + new_widths = [row[3] + (row[2] in selected) for row in rows] + # Every positive excess in these actual bins is smaller than any + # one occupant. The cheapest deletion is therefore one shortest + # whole occurrence; incoming placements could only increase it. + need(0 < excess <= min(new_widths), "one-departure deletion relaxation") + witnesses.append(dict(bin=list(key), capacity=capacity, used_before=used, + extra_width=increase, excess=excess, + minimum_evacuated_width=min(new_widths), + source_window=[begin, end], + placements=[list(row) for row in rows])) + total_added = sum(m * n for (_remaining, m), n in touched.items()) + need(total_added == 666 * len(widened), "each changed endpoint charged at every call") + result = dict(widened=list(widened), retained_lowered=[h for h in V45 if h not in widened], + feasible_without_reassignment=not witnesses, + added_local_children={"1": total_added} if total_added else {}, + added_width=total_added, overfull_bins=len(witnesses), + total_excess=sum(w["excess"] for w in witnesses), + touched_bins=[dict(old_idle=r, added_width=m, count=n) + for (r, m), n in sorted(touched.items())], + first_witness=witnesses[0] if witnesses else None, + all_witnesses_sha256=digest(witnesses), + moved_occurrences_lower_bound=len(witnesses), + moved_width_lower_bound=sum(w["minimum_evacuated_width"] for w in witnesses)) + return result, witnesses diff --git a/research/rank7-final-fill-controls/dual.py b/research/rank7-final-fill-controls/dual.py new file mode 100644 index 0000000000..d47ae1dd46 --- /dev/null +++ b/research/rank7-final-fill-controls/dual.py @@ -0,0 +1,180 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent packing lower bound; integer square roots enclose tariffs. + +No optimizer, predecessor interval engine, or numerical root search is used. +Vectors below express dual potentials as rational linear combinations of +t_r = r**(1-a). Their constraints are checked on every admissible pattern. +""" + +from collections import Counter +from fractions import Fraction as F +from math import isqrt + +from allocation import digest +from local import need + +BITS = 256 +EXPONENT_BITS = 128 +Q = 1 << BITS +WIDTHS = (4, 5, 6, 7, 8, 9) +CAPACITIES = (8, 16, 32, 48) + + +def ceil_div(n, d): + return -(-n // d) + + +def ceil_sqrt(n): + root = isqrt(n) + return root + (root * root != n) + + +def tariff(rank, saving): + """Return integer bounds divided by Q for rank**(1-saving).""" + need(type(rank) is int and 0 <= rank <= 73, "tariff rank bound") + need(F(0) <= saving < F(1), "tariff saving domain") + if rank == 0: + return 0, 0 + scaled = saving * (1 << EXPONENT_BITS) + exponent = scaled.numerator // scaled.denominator + low = high = Q + root_low = root_high = rank * Q + for j in range(EXPONENT_BITS): + root_low = isqrt(root_low * Q) + root_high = ceil_sqrt(root_high * Q) + if exponent & (1 << (EXPONENT_BITS - 1 - j)): + low = low * root_low // Q + high = ceil_div(high * root_high, Q) + if scaled != exponent: + high = ceil_div(high * root_high, Q) + return rank * Q * Q // high, ceil_div(rank * Q * Q, low) + + +def linear(*terms): + """Sum (rational coefficient, sparse tariff vector) terms.""" + result = Counter() + for coefficient, vector in terms: + for rank, value in vector.items(): + result[rank] += F(coefficient) * value + return {r: q for r, q in result.items() if q} + + +def unit(rank): + return {rank: F(1)} if rank else {} + + +def interval(vector, tariffs): + lower = upper = F(0) + for rank, coefficient in vector.items(): + lo, hi = tariffs[rank] + lower += coefficient * (lo if coefficient > 0 else hi) / Q + upper += coefficient * (hi if coefficient > 0 else lo) / Q + return lower, upper + + +def potentials(): + # These solve the ten source basis equalities. The verification below + # checks those equalities symbolically, as well as every inequality. + p9 = linear((F(1, 5), unit(3)), (-F(1, 5), unit(48))) + p8 = linear((F(3, 4), p9), (-F(1, 4), unit(5))) + p7 = linear((2, p8), (-1, p9)) + p6 = linear((3, p8), (-2, p9)) + p5 = linear((-1, unit(5))) + p4 = linear((1, unit(1)), (4, p8), (-3, p9)) + alpha = {8: linear((-1, p8)), 16: linear((-2, p8)), + 32: linear((-4, p8)), 48: unit(48)} + return alpha, {4: p4, 5: p5, 6: p6, 7: p7, 8: p8, 9: p9} + + +def patterns(capacity): + # Finite dynamic enumeration of the established six-width alphabet. + states = [(0, ())] + for width in WIDTHS: + states = [(used + count * width, old + (count,)) + for used, old in states + for count in range((capacity - used) // width + 1)] + return states + + +def check(source, local_profile, inventory, windows, saving): + need(source["local_per_call"] == {str(k): v for k, v in local_profile.items()}, + "cap certificate local binding") + need(source["inventory_per_call"] == {str(k): v for k, v in inventory.items()}, + "cap certificate width binding") + tariffs = {r: tariff(r, saving) for r in range(74)} + alpha, pi = potentials() + tight, strict_lowers, records = [], [], [] + for capacity in CAPACITIES: + for used, counts in patterns(capacity): + slack = linear((1, unit(capacity - used)), (-1, alpha[capacity]), + *((-n, pi[w]) for w, n in zip(WIDTHS, counts, strict=True))) + record = [capacity, list(counts)] + records.append(record) + if not slack: + tight.append(record) + else: + lo, _hi = interval(slack, tariffs) + need(lo > 0, "dual inequality on every packing pattern") + strict_lowers.append(lo) + need(len(records) == source["patterns"] == 2551, "complete fixed pattern domain") + need(len(tight) == source["tight_patterns"] == 12, "symbolically tight patterns") + for row in source["basis_patterns"]: + capacity = row["capacity"] + counts = Counter(row["widths"]) + slack = linear((1, unit(capacity - sum(row["widths"]))), (-1, alpha[capacity]), + *((-n, pi[w]) for w, n in counts.items())) + need(not slack, "literal source basis is tight for these potentials") + total_capacities = Counter(cap for cap, _start, _stop in windows.values()) + bins_per_replica = {cap: F(n * 112, 74) for cap, n in total_capacities.items()} + need(set(bins_per_replica) == set(CAPACITIES), "same bin alphabet") + lower_bill = linear(*((count, alpha[cap]) for cap, count in bins_per_replica.items()), + *((9 * count, pi[w]) for w, count in inventory.items()), + *((9 * count, unit(r)) for r, count in local_profile.items())) + margin = linear((1, lower_bill), (-896, unit(73))) + change = linear((1, unit(1)), (1, pi[8]), (-1, pi[7])) + split = {1: F(1), 3: F(1, 20), 5: F(1, 4), 48: -F(1, 20)} + need(change == split, "symbolic terminal-widening cost direction") + cases = [] + for widened in range(5): + lo, hi = interval(linear((1, margin), (9 * widened, change)), tariffs) + if widened: + need(lo > 0, "control fails even the complete packing relaxation") + else: + need(hi < 0, "baseline relaxation has headroom at the actual claim") + record = dict(widened_count=widened, lower=str(lo), upper=str(hi), + all_packings_rejected=lo > 0) + if widened: + bound = 1 + lo / (896 * F(tariffs[73][1], Q)) + record["complete_moment_lower_bound"] = str(bound) + scaled = bound.numerator * 10**12 // bound.denominator + record["complete_moment_lower_decimal"] = f"{scaled // 10**12}.{scaled % 10**12:012d}" + cases.append(record) + # Bind the displayed fractional primal to the actual bin and helper totals. + actual = Counter() + for row in source["basis_patterns"]: + count = F(row["count_per_replica"]) + need(count >= 0, "nonnegative source basis counts") + actual[row["capacity"]] += count + need(dict(actual) == bins_per_replica, "source primal bin totals") + widths = Counter() + for row in source["basis_patterns"]: + for width in row["widths"]: + widths[width] += F(row["count_per_replica"]) + need(widths == Counter({w: 9 * n for w, n in inventory.items()}), + "source primal helper totals") + return dict(saving=str(saving), interval_method="integer square roots; 256-bit tariff grid, 128 exponent bits", + pattern_count=len(records), tight_patterns=tight, + patterns_sha256=digest(records), minimum_strict_slack_lower=str(min(strict_lowers)), + bins_per_replica={str(k): str(v) for k, v in sorted(bins_per_replica.items())}, + cost_direction={str(r): str(q) for r, q in sorted(change.items())}, + per_occurrence_extra_cost_interval=[str(v) for v in interval(change, tariffs)], + per_replica_excess_over_896_times_73_power=cases) + + +def check_actual_bill(profile, saving): + tariffs = {r: tariff(r, saving) for r in set(profile) | {73}} + margin = linear(*((F(n, 74), unit(r)) for r, n in profile.items()), + (-896, unit(73))) + lo, hi = interval(margin, tariffs) + need(hi < 0, "actual baseline complete moment passes at the source saving") + return [str(lo), str(hi)] diff --git a/research/rank7-final-fill-controls/local.py b/research/rank7-final-fill-controls/local.py new file mode 100644 index 0000000000..6ed400fe19 --- /dev/null +++ b/research/rank7-final-fill-controls/local.py @@ -0,0 +1,152 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Recount the fixed nine-axis frame contract using binary elimination. + +No predecessor evaluator, frame accountant or owner checker is imported. +Frame tariffs and centre descent conventions are inherited, not redefined here. +""" + +from collections import Counter +from functools import lru_cache + +V45 = (249, 251, 265, 267) +FULL = tuple(1 << i for i in range(8, -1, -1)) + + +def need(value, message): + if not value: + raise ValueError(message) + + +def basis(vectors): + need(len(vectors) <= 9, "nine-axis basis bound") + need(all(type(v) is int and 0 < v < 512 for v in vectors), + "nonzero nine-bit generator") + return _basis_cached(vectors) + + +@lru_cache(maxsize=4096) +def _basis_cached(vectors): + pivots = {} + for v in vectors: + for p in sorted(pivots, reverse=True): + if v & (1 << p): + v ^= pivots[p] + need(v != 0, "independent frame generators") + p = v.bit_length() - 1 + for q in pivots: + if pivots[q] & (1 << p): + pivots[q] ^= v + pivots[p] = v + return tuple(pivots[p] for p in sorted(pivots, reverse=True)) + + +def contains(big, small): + for v in small: + for p in big: + if v & (1 << (p.bit_length() - 1)): + v ^= p + if v: + return False + return True + + +def hyperplane(normal): + need(type(normal) is int and 0 < normal < 512, "nonzero port") + p = normal.bit_length() - 1 + return basis(tuple((1 << i) ^ (((normal >> i) & 1) << p) + for i in range(9) if i != p)) + + +def recount(word, terminal_overrides=None): + need(word["report"]["v"] == 112 and word["report"]["h"] == 9 + and word["report"]["R"] == 480, "fixed word dimensions") + need(len(word["ports"]) == 112, "port inventory") + removed = word["removed"] + need(len(removed) == len(set(removed)) == 72 + and all(type(r) is int and 224 <= r < 704 for r in removed), + "removed helper inventory") + live = set(range(704)) - set(removed) + start = [basis((q,)) for q in word["ports"]] + [()] * 592 + end = [FULL] * 112 + [hyperplane(q) for q in word["ports"]] + [FULL] * 480 + for r, b in word["start_extra"].items(): + need(int(r) in live, "live entrance") + start[int(r)] = basis(tuple(b)) + for r, b in word["helper_final"].items(): + need(int(r) in live and int(r) >= 224, "live helper endpoint") + end[int(r)] = basis(tuple(b)) + for r, b in (terminal_overrides or {}).items(): + need(r in V45, "bounded terminal override") + end[r] = basis(tuple(b)) + frames, profile, v45_events = list(start), Counter(), [] + + def move(r, target, location): + need(type(r) is int and r in live, "live frame role") + old = frames[r] + need(contains(target, old), "monotone frame containment") + rank = len(target) - len(old) + if rank: + profile[rank] += 1 + if r in V45: + v45_events.append([r, location, list(old), list(target), rank]) + frames[r] = target + + def scalar(g, location): + if g[0] == "warp": + need(len(g) == 5 and g[1] in live, "inline warp shape") + old, new = basis(tuple(g[-2])), basis(tuple(g[-1])) + need(frames[g[1]] == old and len(old) == len(new), "inline warp frame") + frames[g[1]] = new + return + need(g[0] in ("add", "scale"), "scalar gate kind") + need(len(g) == (6 if g[0] == "add" else 5), "scalar gate arity") + target = basis(tuple(g[-1])) + for r in (g[1:3] if g[0] == "add" else g[1:2]): + move(r, target, location) + + need(all(len(word[s]) <= 10000 for s in ("A", "B", "restore", "cut")), + "bounded scalar sections") + for i, g in enumerate(word["A"]): + scalar(g, ["A", i]) + need(len(word["centers"]) == len(word["center_frames"]) == 8, + "eight centre children") + for r, b in zip(word["centers"], word["center_frames"], strict=True): + previous = basis(tuple(b)) + need(frames[r] == previous, "centre frame at cut") + levels = {basis(tuple(word["target_levels"].get(str(g[1] - 112), []))) + for g in word["cut"] if g[2] == r} + for level in sorted(levels, key=lambda x: (-len(x), x)): + need(contains(previous, level), "nested centre descent") + if len(previous) > len(level): + profile[len(previous) - len(level)] += 1 + previous = level + warps = {} + need(len(word["warps"]) <= 480, "warp count") + for position, r, matrix, old, new in word["warps"]: + need(type(position) is int and 0 <= position <= len(word["B"]), + "warp position") + need(len(basis(tuple(matrix))) == 9, "invertible warp matrix") + before, after = basis(tuple(old)), basis(tuple(new)) + need(len(before) == len(after), "rank preserving warp") + warps.setdefault(position, []).append((r, before, after)) + for i in range(len(word["B"]) + 1): + for r, old, new in warps.get(i, []): + need(r in live and frames[r] == old, "warp entrance frame") + frames[r] = new + if i < len(word["B"]): + scalar(word["B"][i], ["B", i]) + for i, g in enumerate(word["restore"]): + scalar(g, ["restore", i]) + for r in sorted(live): + move(r, end[r], ["terminal", r]) + helpers = sorted(live - set(range(224))) + widths = [len(end[r]) - len(start[r]) for r in helpers] + need(len(helpers) == 408 and all(0 < n <= 9 for n in widths), + "408 positive helper widths") + private = {r for g in word["cleanup"] + for r in (g[1:3] if g[0] == "add" else g[1:2]) if r >= 704} + need(private == {704 + int(r) for r in word["helper_final"]}, + "private names match restored helpers") + need(sum(r * n for r, n in profile.items()) - sum(widths) == 1856, + "local rank mass minus helper width mass") + return dict(profile=profile, helpers=helpers, widths=widths, + private_names=sorted(private), v45_events=v45_events) diff --git a/research/rank7-final-fill-controls/test_verify.py b/research/rank7-final-fill-controls/test_verify.py new file mode 100644 index 0000000000..cab39b717a --- /dev/null +++ b/research/rank7-final-fill-controls/test_verify.py @@ -0,0 +1,278 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral controls for the fixed-source capacity certificate.""" + +from collections import Counter +from copy import deepcopy +from fractions import Fraction as F +import itertools +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +from allocation import bill, control_case, verify_fill, window_table +from local import V45, basis, contains, recount +import dual +import verify + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.files, _ = verify.read_sources() + cls.local = {name: recount(cls.files[f"data/WORD-{tag}.json.gz"]) + for name, tag in (("gauge44", "base"), ("extra", "extra"))} + cls.order = cls.files["allocation/ORDER.json"] + cls.plan = cls.files["allocation/vendor/PLAN.json.gz"] + cls.fill = cls.files["allocation/FILL.json.gz"] + cls.dispatch = cls.files["allocation/DISPATCH.json"] + cls.windows = window_table(cls.files["allocation/vendor/TEMPLATE.json.gz"], + cls.order, cls.plan) + cls.bins, cls.counts = cls.check_fill(cls.fill) + cls.indices = {h: cls.local["gauge44"]["helpers"].index(h) for h in V45} + + @classmethod + def check_fill(cls, fill): + return verify_fill(fill, cls.order, cls.dispatch, cls.plan, cls.windows, cls.local) + + def test_binary_elimination_against_explicit_point_sets(self): + def points(vectors): + answer = {0} + for v in vectors: + answer |= {x ^ v for x in answer} + return answer + frames = {()} + for tag in ("base", "extra"): + w = self.files[f"data/WORD-{tag}.json.gz"] + for section in ("A", "B", "restore"): + frames.update(tuple(g[-1]) for g in w[section]) + frames.update(tuple(b) for b in w["helper_final"].values()) + for frame in frames: + reduced = basis(frame) + self.assertEqual(points(frame), points(reduced)) + self.assertEqual(reduced, basis(tuple(reversed(frame)))) + for line in ((), (1,), (30,), (45,), (256,)): + self.assertEqual(contains(reduced, basis(line)), points(line) <= points(frame)) + with self.assertRaisesRegex(ValueError, "independent"): + basis((1, 2, 3)) + with self.assertRaisesRegex(ValueError, "nine-bit"): + basis((True,)) + + def test_actual_geometry_rejections(self): + rows = self.fill["rows"] + def candidate(new_rows): + return dict(self.fill, rows=new_rows) + with self.assertRaisesRegex(ValueError, "row count"): + self.check_fill(candidate(rows[:-1])) + duplicate = list(rows) + duplicate[1] = rows[0] + with self.assertRaisesRegex(ValueError, "unique call/helper"): + self.check_fill(candidate(duplicate)) + booleans = list(rows) + booleans[0] = list(rows[0]) + booleans[0][1] = False + with self.assertRaisesRegex(ValueError, "integer fill"): + self.check_fill(candidate(booleans)) + family = list(rows) + family[1] = list(rows[1]) + family[1][2:5] = rows[0][2:5] + with self.assertRaisesRegex(ValueError, "physical helper families"): + self.check_fill(candidate(family)) + deadline = list(rows) + deadline[0] = list(rows[0]) + deadline[0][2:4] = [0, 12] + with self.assertRaisesRegex(ValueError, "source window"): + self.check_fill(candidate(deadline)) + incomplete = deepcopy(self.files["allocation/vendor/TEMPLATE.json.gz"]) + incomplete["idle_children"].pop() + with self.assertRaisesRegex(ValueError, "complete source bin"): + window_table(incomplete, self.order, self.plan) + + def test_overlap_and_noncompact_source_slices(self): + rows = self.fill["rows"] + moved = list(rows) + index = next(i for i, row in enumerate(rows) if row[5] > 0) + moved[index] = list(rows[index]) + moved[index][5] = 0 + with self.assertRaisesRegex(ValueError, "disjoint occupied"): + self.check_fill(dict(self.fill, rows=moved)) + # A hole without an overlapping slice is still not the promised prefix. + one = next((key, value[-1]) for key, value in self.bins.items() + if self.windows[key[:2]][0] > sum(row[3] for row in value)) + key, row = one + index = next(i for i, r in enumerate(rows) + if (r[2], r[3], r[4]) == key and r[0] == row[1]) + moved = list(rows) + moved[index] = list(rows[index]) + moved[index][5] += 1 + with self.assertRaisesRegex(ValueError, "compact occupied"): + self.check_fill(dict(self.fill, rows=moved)) + + def test_local_terminal_and_private_controls(self): + word = self.files["data/WORD-base.json.gz"] + base = self.local["gauge44"] + parent = self.files["data/PARENT-base.json.gz"] + controls = verify.word_controls(word, parent, base) + self.assertEqual(controls[14]["local_profile"][1], base["profile"][1] + 3) + self.assertEqual([r[4] for r in controls[14]["terminal_added_ranks"]], [1, 1, 1]) + bad = deepcopy(word) + del bad["helper_final"]["249"] + with self.assertRaisesRegex(ValueError, "private names"): + recount(bad) + bad_parent = deepcopy(parent) + bad_parent["helper_final"]["249"] = [1, 2, 4, 8, 16, 32, 64, 128] + with self.assertRaisesRegex(ValueError, "inside old"): + verify.word_controls(word, bad_parent, base) + + def test_complete_invoice_and_false_control_invoice(self): + idle, complete = bill(self.bins, self.windows, self.counts, self.local) + self.assertEqual(idle, Counter({1: 17310, 3: 4956, 5: 1728, 48: 28190})) + self.assertEqual(complete, verify.integer_profile(self.files["allocation/PROFILE.json"])) + missing = deepcopy(self.local) + missing["gauge44"]["profile"][1] -= 1 + with self.assertRaisesRegex(ValueError, "rank-mass"): + bill(self.bins, self.windows, self.counts, missing) + # Reusing the final idle bill with a widened terminal silently exceeds + # the fixed coverage mass, before any numerical root is evaluated. + wrong_idle = deepcopy(self.local) + for provider in wrong_idle.values(): + provider["profile"][1] += 3 + with self.assertRaisesRegex(ValueError, "rank-mass"): + bill(self.bins, self.windows, self.counts, wrong_idle) + + def test_single_control_witness_and_sharp_deletion_relaxation(self): + result, witnesses = control_case(self.bins, self.windows, self.indices, [251, 265, 267]) + self.assertEqual((result["overfull_bins"], result["total_excess"], + result["moved_width_lower_bound"]), (1938, 1998, 15354)) + selected = {self.indices[h] for h in (251, 265, 267)} + for witness in witnesses: + widths = [row[3] + (row[2] in selected) for row in witness["placements"]] + # Exhaustive small subsets independently price the free-sink + # deletion relaxation. This does not construct a legal relocation. + deletions = [sum(group) for n in range(1, len(widths) + 1) + for group in itertools.combinations(widths, n) + if sum(group) >= witness["excess"]] + self.assertEqual(min(deletions), witness["minimum_evacuated_width"]) + self.assertGreater(sum(widths), witness["capacity"]) + self.assertLessEqual(sum(widths) - min(deletions), witness["capacity"]) + + def test_all_subset_capacity_with_an_axis_counter(self): + for mask in range(16): + widened = [h for i, h in enumerate(V45) if mask & (1 << i)] + selected = {self.indices[h] for h in widened} + result, witnesses = control_case(self.bins, self.windows, self.indices, widened) + count, excess = 0, 0 + for key, rows in self.bins.items(): + if not any(row[2] in selected for row in rows): + continue + cursor = 0 + spilled = set() + capacity = self.windows[key[:2]][0] + for row in rows: + for axis in range(cursor, cursor + row[3] + (row[2] in selected)): + if axis >= capacity: + spilled.add(axis) + cursor += row[3] + (row[2] in selected) + count += bool(spilled) + excess += len(spilled) + self.assertEqual((count, excess), (len(witnesses), result["total_excess"])) + + def test_export_optimized_cli_and_corrupt_input(self): + with tempfile.TemporaryDirectory(prefix="final-fill-control-") as tmp: + root = Path(tmp) + package = root / "research" / verify.PACKAGE.name + shutil.copytree(verify.PACKAGE, package, ignore=shutil.ignore_patterns("__pycache__")) + manifest = verify.decode((package / "SOURCES.json").read_bytes()) + for entry in manifest["files"]: + if entry["usage"] == "input": + dest = root / entry["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / entry["path"], dest) + command = [sys.executable, "-O", "-B", str(package / "verify.py")] + run = subprocess.run(command, capture_output=True, text=True, timeout=90) + self.assertEqual(run.returncode, 0, run.stderr) + self.assertIn("PASS_RANK7_FINAL_FILL_CONTROLS", run.stdout) + corrupt = root / verify.SOURCE / "allocation/ORDER.json" + corrupt.write_bytes(corrupt.read_bytes() + b" ") + run = subprocess.run(command, capture_output=True, text=True, timeout=90) + self.assertNotEqual(run.returncode, 0) + self.assertIn("source SHA256 mismatch", run.stderr) + + def test_strict_receipt_json_and_histograms(self): + with self.assertRaisesRegex(ValueError, "duplicate JSON"): + verify.decode('{"rank": 7, "rank": 8}') + with self.assertRaisesRegex(ValueError, "positive integer"): + verify.integer_profile({"-1": 4}) + with self.assertRaisesRegex(ValueError, "positive integer"): + verify.integer_profile({"1": True}) + + def test_tariff_intervals_against_exact_algebraic_inequalities(self): + for rank in range(1, 74): + self.assertEqual(dual.tariff(rank, F(0)), (rank * dual.Q, rank * dual.Q)) + lo, hi = dual.tariff(rank, F(1, 2)) + self.assertLessEqual(lo * lo, rank * dual.Q**2) + self.assertGreaterEqual(hi * hi, rank * dual.Q**2) + lo, hi = dual.tariff(rank, F(1, 3)) + self.assertLessEqual(lo**3, rank**2 * dual.Q**3) + self.assertGreaterEqual(hi**3, rank**2 * dual.Q**3) + if rank > 1: + half = dual.tariff(rank, F(1, 2)) + self.assertGreater(lo, half[1]) + self.assertEqual(dual.tariff(0, F(1, 2)), (0, 0)) + + def test_exact_pattern_domain(self): + # A separate recursive multiset walk checks the Cartesian enumerator. + def walk(remaining, start, prefix): + answer = {tuple(prefix.count(w) for w in dual.WIDTHS)} + for i in range(start, len(dual.WIDTHS)): + w = dual.WIDTHS[i] + if w <= remaining: + answer |= walk(remaining - w, i, prefix + [w]) + return answer + for capacity in dual.CAPACITIES: + expected = walk(capacity, 0, []) + actual = {counts for used, counts in dual.patterns(capacity)} + self.assertEqual(actual, expected) + + def packing_check(self, source=None): + return dual.check(source or self.files["certificates/RELAX-CAP.json"], + self.local["gauge44"]["profile"], + Counter(self.local["gauge44"]["widths"]), self.windows, + F(self.files["CLAIM.json"]["complex_lower"])) + + def test_dual_source_binding_and_complete_control_bounds(self): + result = self.packing_check() + self.assertEqual(result["pattern_count"], 2551) + rows = result["per_replica_excess_over_896_times_73_power"] + self.assertLess(F(rows[0]["upper"]), 0) + for row in rows[1:]: + self.assertGreater(F(row["lower"]), 0) + self.assertGreater(F(row["complete_moment_lower_bound"]), 1) + self.assertEqual(rows[3]["complete_moment_lower_decimal"], "1.000005090277") + bad = deepcopy(self.files["certificates/RELAX-CAP.json"]) + bad["inventory_per_call"]["7"] -= 1 + with self.assertRaisesRegex(ValueError, "width binding"): + self.packing_check(bad) + bad = deepcopy(self.files["certificates/RELAX-CAP.json"]) + bad["basis_patterns"][0]["count_per_replica"] = "671" + with self.assertRaisesRegex(ValueError, "primal bin totals"): + self.packing_check(bad) + + def test_infeasible_dual_and_omitted_pattern_rejected(self): + alpha, pi = dual.potentials() + pi[7] = dual.linear((1, pi[7]), (F(1, 1000), dual.unit(1))) + with patch.object(dual, "potentials", return_value=(alpha, pi)): + with self.assertRaisesRegex(ValueError, "dual inequality"): + self.packing_check() + original = dual.patterns + with patch.object(dual, "patterns", side_effect=lambda c: original(c)[1:]): + with self.assertRaisesRegex(ValueError, "pattern domain"): + self.packing_check() + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/rank7-final-fill-controls/verify.py b/research/rank7-final-fill-controls/verify.py new file mode 100644 index 0000000000..42ea5e7fd0 --- /dev/null +++ b/research/rank7-final-fill-controls/verify.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check V45 terminal controls against the literal final T74 allocation.""" + +import argparse +from collections import Counter +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path +import sys + +from allocation import bill, control_case, verify_fill, window_table +import dual +from local import V45, basis, contains, need, recount + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = "research/rank7-joint-endframes/" +SOURCE_HEAD = "be191346391661f4d35fc0d1508d0a6029572576" + + +def unique_object(items): + result = {} + for key, value in items: + need(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def decode(raw): + return json.loads(raw, object_pairs_hook=unique_object) + + +def read_sources(): + manifest = decode((PACKAGE / "SOURCES.json").read_bytes()) + files, hashes = {}, {} + for entry in manifest["files"]: + if entry["usage"] != "input": + continue + path = entry["path"] + need(path.startswith(SOURCE) and ".." not in Path(path).parts, "fixed source root") + raw = (ROOT / path).read_bytes() + need(len(raw) <= 16 * 1024 * 1024, "raw source size bound") + actual = hashlib.sha256(raw).hexdigest() + need(actual == entry["sha256"], "source SHA256 mismatch: " + path) + payload = gzip.decompress(raw) if path.endswith(".gz") else raw + need(len(payload) <= 64 * 1024 * 1024, "decoded source size bound") + files[path.removeprefix(SOURCE)] = decode(payload) + hashes[path] = actual + need(len(files) == 12, "twelve exact live inputs") + return files, hashes + + +def integer_profile(data): + result = Counter() + for key, count in data.items(): + rank = int(key) + need(str(rank) == key and 0 < rank <= 73 and type(count) is int and count > 0, + "positive integer rank histogram") + result[rank] = count + return result + + +def word_controls(word, parent, baseline): + old_ends = {} + for helper in V45: + current = basis(tuple(word["helper_final"][str(helper)])) + previous = basis(tuple(parent["helper_final"][str(helper)])) + need(len(current) == 7 and len(previous) == 8 and contains(previous, current), + "V45 rank-seven subspace inside old rank-eight endpoint") + need(helper not in map(int, word["start_extra"]), "zero V45 entrance") + old_ends[helper] = parent["helper_final"][str(helper)] + out = [] + for mask in range(16): + widened = [h for i, h in enumerate(V45) if mask & (1 << i)] + candidate = recount(word, {h: old_ends[h] for h in widened}) + expected = Counter(baseline["profile"]) + if widened: + expected[1] += len(widened) + need(candidate["profile"] == expected, "terminal-only local H1 delta") + need(candidate["private_names"] == baseline["private_names"], "unchanged private names") + need(candidate["widths"] == [n + (h in widened) for h, n in + zip(baseline["helpers"], baseline["widths"], strict=True)], + "only selected residual widths change") + out.append(dict(widened=widened, local_profile=dict(sorted(candidate["profile"].items())), + width_inventory=dict(sorted(Counter(candidate["widths"]).items())), + terminal_added_ranks=[e for e in candidate["v45_events"] + if e[1][0] == "terminal"])) + return out + + +def compute(): + files, hashes = read_sources() + local_data, provider_receipts = {}, {} + for provider, tag in (("gauge44", "base"), ("extra", "extra")): + word = files[f"data/WORD-{tag}.json.gz"] + parent = files[f"data/PARENT-{tag}.json.gz"] + data = recount(word) + need(data["profile"] == integer_profile(word["report"]["local_profile"]), + "word report matches independent local recount") + need(Counter(data["widths"]) == integer_profile(word["report"]["width_inventory"]), + "width inventory matches word report") + need(len(data["private_names"]) == 91, "91 charged private names") + local_data[provider] = data + provider_receipts[provider] = dict( + baseline_profile=dict(sorted(data["profile"].items())), + width_inventory=dict(sorted(Counter(data["widths"]).items())), + private_names=data["private_names"], + cleanup_operations=len(word["cleanup"]), + v45_events=data["v45_events"], + controls=word_controls(word, parent, data), + ) + need(local_data["gauge44"]["helpers"] == local_data["extra"]["helpers"] + and local_data["gauge44"]["widths"] == local_data["extra"]["widths"], + "identical ordered helper inventory across providers") + need(local_data["gauge44"]["profile"] == local_data["extra"]["profile"], + "identical local tariff profile across providers") + order = files["allocation/ORDER.json"] + plan = files["allocation/vendor/PLAN.json.gz"] + windows = window_table(files["allocation/vendor/TEMPLATE.json.gz"], order, plan) + bins, counts = verify_fill(files["allocation/FILL.json.gz"], order, + files["allocation/DISPATCH.json"], plan, windows, local_data) + idle, full = bill(bins, windows, counts, local_data) + claim = files["CLAIM.json"] + need(full == integer_profile(files["allocation/PROFILE.json"]) + == integer_profile(claim["profile"]), "literal complete profile agrees") + need(dict(counts) == {"extra": 416, "gauge44": 250}, "actual provider counts") + need(claim["calls"] == 666 and claim["replicas"] == 74 and claim["helpers"] == 408 + and claim["zero_buffers"] == 91, "claim stock inputs") + physical = 896 * 74 + 408 + 8 + 91 + 2 + need(claim["live_families"] == 896 * 74 and claim["physical_families"] == physical, + "complete nominal physical stock including private buffers") + helper_indices = {h: local_data["gauge44"]["helpers"].index(h) for h in V45} + saving = Fraction(claim["complex_lower"]) + packing = dual.check(files["certificates/RELAX-CAP.json"], + local_data["gauge44"]["profile"], + Counter(local_data["gauge44"]["widths"]), windows, saving) + packing["actual_baseline_margin_interval"] = dual.check_actual_bill(full, saving) + cases, all_witnesses = [], {} + for mask in range(16): + widened = [h for i, h in enumerate(V45) if mask & (1 << i)] + case, witnesses = control_case(bins, windows, helper_indices, widened) + need(all(row["old_idle"] == 0 for row in case["touched_bins"]), + "every affected bin is saturated") + need(case["total_excess"] == 666 * len(widened), "all added width becomes excess") + need(case["feasible_without_reassignment"] == (mask == 0), + "only the four-lowered endpoint choice fits") + case["all_packings_rejected_at_source_saving"] = packing[ + "per_replica_excess_over_896_times_73_power"][len(widened)]["all_packings_rejected"] + cases.append(case) + all_witnesses[str(mask)] = witnesses + result = dict( + status="PASS_RANK7_FINAL_FILL_CONTROLS", + source_head=SOURCE_HEAD, source_sha256=hashes, + result_kind="finite capacity certificate and scoped obstruction", + providers=provider_receipts, helper_indices=helper_indices, + baseline=dict(calls=666, roles=666 * 408, bins=len(windows) * 112, + provider_counts=dict(counts), idle_profile=dict(sorted(idle.items())), + complete_profile=dict(sorted(full.items())), + rank_mass=sum(r * n for r, n in full.items()), + live_families=896 * 74, helpers=408, centres=8, + private_buffers=91, coefficient_families=2, physical_families=physical), + cases=cases, packing_relaxation=packing, + limits=["No control repacking is constructed or priced.", + "These controls retain all final stage-2/3 scalar and frame edits.", + "Original stage-1 guide controls remain separate predecessor evidence.", + "No native phase, dirty restoration, movement, precision/tape or outer/all-size admission."], + ) + # Normalize integer dictionary keys to their JSON spelling for receipt comparison. + return decode(json.dumps(result)), all_witnesses + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print fresh deterministic receipt") + parser.add_argument("--witnesses", type=Path, help="write all exact overfull-bin witnesses") + args = parser.parse_args() + result, witnesses = compute() + if args.witnesses: + with args.witnesses.open("x") as stream: + json.dump(witnesses, stream, indent=2, sort_keys=True) + stream.write("\n") + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(result == decode((PACKAGE / "RESULT.json").read_bytes()), + "deterministic result differs") + print(result["status"] + " cases=16 rejected_controls=15 roles=271728 bins=149184 packing_patterns=2551") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, TypeError, IndexError) as exc: + print("FAIL: " + str(exc), file=sys.stderr) + raise SystemExit(1) from None