diff --git a/research/independent-queue-ceilings/README.md b/research/independent-queue-ceilings/README.md new file mode 100644 index 0000000000..5ca9ca3c41 --- /dev/null +++ b/research/independent-queue-ceilings/README.md @@ -0,0 +1,194 @@ +# Independent integer-root check of the nine frozen packing ceilings + +All nine packing-relaxation brackets in Douglas Colkitt's +[PR1264 census](../complex-queue-ceiling-census/README.md) pass a separately +written integer-root calculation. The fourteen source profiles and idle +histograms reproduce the census exactly. No numerical discrepancy was found. +**Independent finite verification; no new construction or kappa.** + +Revision 3 uses this census to assess the remaining benefit of packing. Both +the census and its [PR1240 predecessor](../complex-local-word-ceiling/README.md) +use the same atanh/Taylor engine. This package adds a different numerical +method and an offline check of the original source extraction, including the +mixed-provider rational counts. It imports no predecessor executable. + +## Result and exact scope + +The table gives each certified upper endpoint `a_hi`; its lower endpoint is +exactly `a_hi - 10^-15`. At both 96/192 and 128/256 exponent/fractional bits, +the outward rational intervals prove + +`relax(a_hi - 10^-15) < 1 < relax(a_hi)`. + +| Profile | Exact `a_hi` | Frozen claims | +|---|---:|---| +| W1 | 0.001690166683079 | #1124, #1130 | +| W4 | 0.001690126076663 | #1152 | +| W5 | 0.001690094712065 | #1157 | +| W2, selected at the base | 0.001690054109089 | #1129, #1131 | +| W8 | 0.001687160482514 | #1195 | +| W9 | 0.001687102547672 | #1196, #1204, #1225 | +| W3 | 0.001687062088401 | #1148 | +| W6 | 0.001686657172581 | #1178 | +| W7, mixed providers | 0.001686519526354 | #1193, #1239 | + +Thus the original common strict planning cap is corroborated: + +`kappa < 1690166683079 / 1001690166683079 < 0.001687314840`. + +This is the frozen fourteen-claim domain of PR1264, **not the current open PR +queue**. Profile labels identify aggregate paid profiles, not circuit +identities. The cap applies only under the fixed coverage law, width 73, +896/9 live families per call, centre charge 64, and rank-51 idle relaxation. +The conversion to kappa retains the predecessor's balanced-transfer premise. +A relaxation root is not an attainable supplier optimum. + +The selected PR1094 assembly and independent receipt separately reproduce W2 +with 144 calls, 14,336 live families, and 1,646 idle-rank units per call. Their +reported endpoint is below the W2 bracket. This does not re-execute that +assembly or re-certify its endpoint moment. + +The committed [RESULT.json](RESULT.json) contains every exact rational moment +interval at both precisions, all profile memberships, per-claim count evidence, +14 semantic controls, 2,640 exact algebraic power comparisons, and 72 exact +zero-saving child costs. [test_verify.py](test_verify.py) adds 13 test groups +covering arithmetic corruption, source drift, missing inputs, omitted cases, +wrong brackets, mixed-count rounding, and optimized read-only relocation. + +## Source extraction and its boundary + +[SOURCES.json](SOURCES.json) pins the four immutable main-branch inputs and the +historical task/selection provenance at +`ee055dc44815497927ef618fc985b93c2dcbda2a`. [UPSTREAM.json](UPSTREAM.json) binds +21 original JSON blobs to each frozen head/path pair in the census. They were +retrieved through GitHub's Contents API at those exact heads; each response's +Git blob ID and raw bytes were checked. The compressed copies in `inputs/` +retain the exact original JSON bytes. Offline replay checks both SHA256 and +Git blob hashes of the **decompressed payload**, not the gzip container. + +The new extractor uses explicit fields and JSON paths, not the predecessor's +recursive matching routine. Every call count is independently read from +`calls`, `complete_invocations`, or the sum of `provider_counts`. Ten claims +also provide an explicit `live` field. The cited receipts for **#1124, #1130, +#1178 and #1195 omit it**; for those four, `W = 896 N / 9` remains an explicit +template premise, now distinguished in the receipt. This audit does not claim +to have recovered their physical live stock from operations. + +For each claim the checker requires nonnegative integer histograms, an idle +subprofile with ranks at most 51, `9 W = 896 N`, and +`sum_r r H_r = 72 W + 64 N`. It then computes each local count as +`L_r = (H_r - I_r) / N` using exact fractions and compares the complete census +grouping. Titles and recorded endpoints are checked against the original +source fields, not used as numerical evidence of admission. + +W7's exact counts are +`{1:783550/333, 2:169496/333, 3:137362/333, 4:42458/333, 5:82, 8:8}`. +The predecessor's README displays rounded values, while its actual calculation +correctly retains these fractions. Substituting the display values changes +the lower-endpoint sign; this is a useful corruption control, **not a defect +in the predecessor's certificate**. + +## Enclosure and ceiling arguments + +Let `S = 2^P` and `x = m/r >= 1`. The initial integer bounds are +`floor(S x) <= S x <= ceil(S x)`. If `l/S <= y <= u/S`, then + +`isqrt(l S)/S <= sqrt(y) <= ceil_sqrt(u S)/S`. + +Squaring both nonnegative sides proves each inequality. Repeating this gives +outward bounds for `x^(1/2^j)`. For a binary exponent `k/2^B`, multiply the +root factors selected by the bits of `k`, rounding every scaled product down +for the lower bound and up for the upper bound. Positivity preserves the +enclosure at every multiplication. For rational `a`, set +`k_lo = floor(2^B a)` and `k_hi = ceil(2^B a)`. Since `x >= 1`, exponent +monotonicity sandwiches `x^a` between those two dyadic powers. Multiplication +by the exact positive rational `r/m` encloses `(r/m)^(1-a)`. + +The arithmetic oracle in the controls is different: for rational `a = p/q`, +it checks `lo^q <= x^p <= hi^q` by direct exact integer powers. This catches +root rounding, bit-order and exponent-bracketing errors without using another +root or transcendental implementation. Equality and intervals crossing one +produce an explicit unresolved error, never a successful endpoint decision. + +For the inherited ceiling theorem, write `w = 896/9`. The coverage law gives +total rank mass `72 w + 64 = 7232` per call. Subtract the local mass to obtain +idle mass `M`. At `a >= 0`, a rank-r child's cost per rank unit is +`m^(a-1) r^(-a)`, nonincreasing in `r`. Therefore every idle histogram with +ranks at most 51 costs at least `(M/51) (51/73)^(1-a)`. The guard admits 51 +and excludes 52 because `2*51^2 < 73^2 < 2*52^2`. The resulting lower bound is + +`relax(a) = [sum_r L_r (r/73)^(1-a) + (M/51)(51/73)^(1-a)] / w`. + +All terms have positive bases below one and nonnegative counts, so the +relaxation is strictly increasing for these profiles. Its two certified signs +bracket its unique root. At or above the upper endpoint, even this favorable +relaxation exceeds one; adding nonnegative implementation charges cannot +repair that inequality. The theorem and model are credited to PR1240/PR1012; +the new result is their independent numerical and extraction corroboration. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B scripts/research_package.py --package research/independent-queue-ceilings +``` + +This validates provenance, runs the complete receipt check and the corruption +tests. The generic hook uses the four explicitly declared external inputs. +The direct check also works without Git or network when those four files and +this package are copied with their repository-relative paths: + +```sh +python3.12 -I -O -B research/independent-queue-ceilings/verify.py +``` + +Expected output begins `PASS_INDEPENDENT_QUEUE_CEILINGS` and reports 14 claims, +9 profiles, 18 endpoint signs, 18 refined signs, 14 semantic controls and 21 +source blobs. `verify.py --write` explicitly regenerates only this package's +receipt. Ordinary replay is read-only. Full Git history is needed by the +registered wrapper's provenance checks. + +Unrun obligations: operation/frame or owner reconstruction, native supplier +admission, chronological hosting, physical live-stock derivation, exceptional +charges for actual suppliers, bootstrap/outer feasibility, precision/tape, +all-size and analytic interfaces, and a full Lean multiplication theorem. + +## Open next questions + +Can the four template-derived live counts be bound to explicit physical +inventories in their original packages? This would remove a source-extraction +premise, not improve kappa. A first step is to locate each pinned template or +owner inventory and recount active data families while retaining its role +distinction. Those additional inputs and the physical reconstruction are +outside this package. The structured question is in [TASK.json](TASK.json). + +## Credit and overlap + +Douglas Colkitt's PR1240 supplies the ceiling theorem and original numerical +engine; PR1264 supplies the frozen census and all nine reported brackets. +PR1012 supplies the coverage identity. The fourteen frozen constructions are +credited to jeremykothe2 (#1124/#1130), aliromman (#1129), chafreaky +(#1131/#1152/#1196), tomdif (#1148), rohanarun (#1157/#1178/#1225), +jeremydiviney (#1193), mdumitrean (#1195), and GamingPuzzled (#1204/#1239). +This package asserts no construction or discovery credit. +The selected lineage includes Rohan Arun, Jeremy Kothe and Hao Yan, with full +attribution in the selected review. + +Integer-root endpoint verification already appears in arkfx's PR706 and +Arham-Tahir64's PR1577; this implementation was written separately. +Arham-Tahir64's PR1605 independently checks the +selected baseline bracket as part of its rank-one block-budget study. This +package's additional domain is the complete nine-profile census and its +twenty-one original source blobs. Discussion #1606 changes port count and +Discussion #1328 changes the coverage law; neither is attempted here. + +Started from current main at the exact base above, using task `independent-moment` +and nonce `488b8bb97d866ded02e80a47a4e9d7e1`. Coordination: +[Discussion #1620](https://github.com/CrocSwap/integer-mult-bounds/discussions/1620). +Search coverage and limits are recorded in TASK.json; a clear search result is +not a novelty certificate. + +Prepared by Hanson Sun (bbMisk) with substantial OpenAI Codex assistance in +scope selection, implementation, mathematical explanation, testing and writing. +New material and copied repository inputs retain Apache-2.0. diff --git a/research/independent-queue-ceilings/RESULT.json b/research/independent-queue-ceilings/RESULT.json new file mode 100644 index 0000000000..f19fa5472c --- /dev/null +++ b/research/independent-queue-ceilings/RESULT.json @@ -0,0 +1,834 @@ +{ + "arithmetic": { + "exponent_bits": 96, + "fractional_bits": 192, + "refined_exponent_bits": 128, + "refined_fractional_bits": 256 + }, + "claims": [ + { + "count_evidence": { + "calls": [ + [ + "profile/complete_invocations", + 144 + ], + [ + "idle/complete_invocations", + 144 + ] + ], + "live": [], + "live_mode": "inferred from source N under the 896/9 template premise" + }, + "head": "7c0e3ee0e2d4f6c00d033a4f1dfe4e793e7ecae4", + "idle_mass_per_call": "1648", + "local": { + "1": "2406", + "2": "432", + "3": "426", + "4": "138", + "5": "84", + "8": "8" + }, + "pr": 1124 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/provider_counts:sum", + 333 + ] + ], + "live": [ + [ + "idle/expected/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "a007dc2e1cc7ae7e8f7ec1343e8883fe43259f21", + "idle_mass_per_call": "1646", + "local": { + "1": "2412", + "2": "418", + "3": "432", + "4": "142", + "5": "82", + "8": "8" + }, + "pr": 1129 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/complete_invocations", + 144 + ], + [ + "idle/complete_invocations", + 144 + ] + ], + "live": [], + "live_mode": "inferred from source N under the 896/9 template premise" + }, + "head": "1558508e5cbff0b7c534d1c4cc7a0fb1b7145c1c", + "idle_mass_per_call": "1648", + "local": { + "1": "2406", + "2": "432", + "3": "426", + "4": "138", + "5": "84", + "8": "8" + }, + "pr": 1130 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/calls", + 333 + ], + [ + "idle/calls", + 333 + ] + ], + "live": [ + [ + "profile/live", + 33152 + ], + [ + "idle/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "fcdc42737b703323d8ed550a528141a482e68e96", + "idle_mass_per_call": "1646", + "local": { + "1": "2412", + "2": "418", + "3": "432", + "4": "142", + "5": "82", + "8": "8" + }, + "pr": 1131 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/provider_counts:sum", + 144 + ] + ], + "live": [ + [ + "idle/expected/live", + 14336 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "506ea08dd77388105682044ebb0848ce9b274964", + "idle_mass_per_call": "1642", + "local": { + "1": "2364", + "2": "498", + "3": "412", + "4": "130", + "5": "82", + "8": "8" + }, + "pr": 1148 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/calls", + 333 + ], + [ + "idle/calls", + 333 + ] + ], + "live": [ + [ + "profile/live", + 33152 + ], + [ + "idle/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "d376209304f05551f975b0ddf6eaa84edc4ae31a", + "idle_mass_per_call": "1648", + "local": { + "1": "2406", + "2": "432", + "3": "424", + "4": "142", + "5": "82", + "8": "8" + }, + "pr": 1152 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/provider_counts:sum", + 333 + ] + ], + "live": [ + [ + "idle/expected/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "c5647aecc8ff44e49776860bb75520bfe3e88f1e", + "idle_mass_per_call": "1646", + "local": { + "1": "2412", + "2": "418", + "3": "434", + "4": "138", + "5": "84", + "8": "8" + }, + "pr": 1157 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/provider_counts:sum", + 144 + ] + ], + "live": [], + "live_mode": "inferred from source N under the 896/9 template premise" + }, + "head": "6d4d0dd1c2df531a3350495dd15e00105793c52d", + "idle_mass_per_call": "1642", + "local": { + "1": "2372", + "2": "494", + "3": "414", + "4": "126", + "5": "84", + "8": "8" + }, + "pr": 1178 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/calls", + 333 + ], + [ + "idle/calls", + 333 + ] + ], + "live": [ + [ + "profile/live", + 33152 + ], + [ + "idle/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "4e392e90e3fca8f395e35d6a23644920160a9f0f", + "idle_mass_per_call": "545954/333", + "local": { + "1": "783550/333", + "2": "169496/333", + "3": "137362/333", + "4": "42458/333", + "5": "82", + "8": "8" + }, + "pr": 1193 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/provider_counts:sum", + 144 + ] + ], + "live": [], + "live_mode": "inferred from source N under the 896/9 template premise" + }, + "head": "cc1b023b123622abba467c7933f3759f8034c753", + "idle_mass_per_call": "1642", + "local": { + "1": "2358", + "2": "504", + "3": "408", + "4": "134", + "5": "80", + "8": "8" + }, + "pr": 1195 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/calls", + 333 + ], + [ + "idle/calls", + 333 + ] + ], + "live": [ + [ + "profile/live", + 33152 + ], + [ + "idle/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "7015903d1d01a2b50ff16f85184edc2686f69e37", + "idle_mass_per_call": "1642", + "local": { + "1": "2364", + "2": "498", + "3": "414", + "4": "126", + "5": "84", + "8": "8" + }, + "pr": 1196 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/provider_counts:sum", + 333 + ] + ], + "live": [ + [ + "idle/expected/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "d49f96b75257c8a5eb4862eb99fbaffc738dcc1b", + "idle_mass_per_call": "1642", + "local": { + "1": "2364", + "2": "498", + "3": "414", + "4": "126", + "5": "84", + "8": "8" + }, + "pr": 1204 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/provider_counts:sum", + 333 + ], + [ + "idle/calls", + 333 + ] + ], + "live": [ + [ + "idle/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "aac9ce7d83e02989eed76e08815cfd2399214e90", + "idle_mass_per_call": "1642", + "local": { + "1": "2364", + "2": "498", + "3": "414", + "4": "126", + "5": "84", + "8": "8" + }, + "pr": 1225 + }, + { + "count_evidence": { + "calls": [ + [ + "profile/calls", + 333 + ], + [ + "idle/calls", + 333 + ] + ], + "live": [ + [ + "profile/live", + 33152 + ], + [ + "idle/live", + 33152 + ] + ], + "live_mode": "direct source field and template agreement" + }, + "head": "12e04a30d7381a2a60bf2d7260febcb37f14e454", + "idle_mass_per_call": "545954/333", + "local": { + "1": "783550/333", + "2": "169496/333", + "3": "137362/333", + "4": "42458/333", + "5": "82", + "8": "8" + }, + "pr": 1239 + } + ], + "endpoint_decisions": 18, + "exact_power_controls": { + "algebraic_comparisons": 2640, + "exact_zero_saving_ranks": 72 + }, + "max_kappa_cap_exact": "1690166683079/1001690166683079", + "profiles": [ + { + "claims": [ + 1124, + 1130 + ], + "id": "W1", + "idle_mass_per_call": "1648", + "kappa_cap_exact": "1690166683079/1001690166683079", + "local": { + "1": "2406", + "2": "432", + "3": "426", + "4": "138", + "5": "84", + "8": "8" + }, + "lower": { + "a": "845083341539/500000000000000", + "moment_minus_one": [ + "-59926194137337547181746169047907483134185668503/51321583788521501925121414324145880618052858113937946177437696", + "-239704776549342665369170212692880953468021832919/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "-631681809464512272188494680369791726577390389108375320543932784825/540980640916741265018923641960589905490477368357872715192345832484970141677780992", + "-4421772666251585905319430450012772859278820121745100008725477209083/3786864486417188855132465493724129338433341578505109006346420827394790991744466944" + ], + "sign": "below" + }, + "upper": { + "a": "1690166683079/1000000000000000", + "moment_minus_one": [ + "178178519513961503258332759126123892060907934597/102643167577043003850242828648291761236105716227875892354875392", + "89089259756982632468619995444629165341323925731/51321583788521501925121414324145880618052858113937946177437696" + ], + "refined_moment_minus_one": [ + "3286813548906540479372733815753853203211555144575341771928224778497/1893432243208594427566232746862064669216670789252554503173210413697395495872233472", + "6573627097813080958745499944083475633304219953814050824622617103639/3786864486417188855132465493724129338433341578505109006346420827394790991744466944" + ], + "sign": "above" + } + }, + { + "claims": [ + 1152 + ], + "id": "W4", + "idle_mass_per_call": "1648", + "kappa_cap_exact": "1690126076663/1001690126076663", + "local": { + "1": "2406", + "2": "432", + "3": "424", + "4": "142", + "5": "82", + "8": "8" + }, + "lower": { + "a": "845063038331/500000000000000", + "moment_minus_one": [ + "-12020597287487486608116630087069239500115412641/14663309653863286264320404092613108748015102318267984622125056", + "-168288362024817288975596024272803971025543964339/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "-55435220443851725978684914385255338220533723952141496990016831013/67622580114592658127365455245073738186309671044734089399043229060621267709722624", + "-3104372344855696654806322892224480685421515553125365096253270198887/3786864486417188855132465493724129338433341578505109006346420827394790991744466944" + ], + "sign": "below" + }, + "upper": { + "a": "1690126076663/1000000000000000", + "moment_minus_one": [ + "427787732236771454540693625024291100887154612067/205286335154086007700485657296583522472211432455751784709750784", + "106946933059194744519682605499494267781790969129/51321583788521501925121414324145880618052858113937946177437696" + ], + "refined_moment_minus_one": [ + "3945645407222193602392595696309448867469979660128987888339024974655/1893432243208594427566232746862064669216670789252554503173210413697395495872233472", + "3945645407222193602392611852984357994993266167506413359659263042337/1893432243208594427566232746862064669216670789252554503173210413697395495872233472" + ], + "sign": "above" + } + }, + { + "claims": [ + 1157 + ], + "id": "W5", + "idle_mass_per_call": "1646", + "kappa_cap_exact": "338018942413/200338018942413", + "local": { + "1": "2412", + "2": "418", + "3": "434", + "4": "138", + "5": "84", + "8": "8" + }, + "lower": { + "a": "6601932469/3906250000000", + "moment_minus_one": [ + "-44865640494921664352195281160758111475947326889/51321583788521501925121414324145880618052858113937946177437696", + "-89731280989839566867445259697218644767589779357/102643167577043003850242828648291761236105716227875892354875392" + ], + "refined_moment_minus_one": [ + "-827624987912865314251440962837198142295843903382366230038287055493/946716121604297213783116373431032334608335394626277251586605206848697747936116736", + "-827624987912865314251432884353871662639753366745574279505367010291/946716121604297213783116373431032334608335394626277251586605206848697747936116736" + ], + "sign": "below" + }, + "upper": { + "a": "338018942413/200000000000000", + "moment_minus_one": [ + "416624295729511976082885321934591671457419444377/205286335154086007700485657296583522472211432455751784709750784", + "416624295729519499756775927210703965497866277349/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "7685361758211894239792260651008480291218639797853499442076376160973/3786864486417188855132465493724129338433341578505109006346420827394790991744466944", + "1921340439552973559948073241235446552490296787695183857863221889831/946716121604297213783116373431032334608335394626277251586605206848697747936116736" + ], + "sign": "above" + } + }, + { + "claims": [ + 1129, + 1131 + ], + "id": "W2", + "idle_mass_per_call": "1646", + "kappa_cap_exact": "1690054109089/1001690054109089", + "local": { + "1": "2412", + "2": "418", + "3": "432", + "4": "142", + "5": "82", + "8": "8" + }, + "lower": { + "a": "52814190909/31250000000000", + "moment_minus_one": [ + "-414832914115274191461908544658861579508128631197/205286335154086007700485657296583522472211432455751784709750784", + "-414832914115266667607795449182386147252505274051/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "-956539575004435027771643708907230602035106441933680177030137209787/473358060802148606891558186715516167304167697313138625793302603424348873968058368", + "-1093188085719354317453302479507212742303437716654870218764759892283/540980640916741265018923641960589905490477368357872715192345832484970141677780992" + ], + "sign": "below" + }, + "upper": { + "a": "1690054109089/1000000000000000", + "moment_minus_one": [ + "181268222290676465765337416517801096626081759063/205286335154086007700485657296583522472211432455751784709750784", + "25895460327240569945635787431684908091956632819/29326619307726572528640808185226217496030204636535969244250112" + ], + "refined_moment_minus_one": [ + "208988031580776698425207355320351182817934835480227486112590997977/236679030401074303445779093357758083652083848656569312896651301712174436984029184", + "3343808505292427174803349999832974545361933056863702606960402282827/3786864486417188855132465493724129338433341578505109006346420827394790991744466944" + ], + "sign": "above" + } + }, + { + "claims": [ + 1195 + ], + "id": "W8", + "idle_mass_per_call": "1642", + "kappa_cap_exact": "843580241257/500843580241257", + "local": { + "1": "2358", + "2": "504", + "3": "408", + "4": "134", + "5": "80", + "8": "8" + }, + "lower": { + "a": "1687160482513/1000000000000000", + "moment_minus_one": [ + "-519759547104292938693187469409186932507784136879/205286335154086007700485657296583522472211432455751784709750784", + "-32484971694017837622978822789177131594402677495/12830395947130375481280353581036470154513214528484486544359424" + ], + "refined_moment_minus_one": [ + "-4793935672650001828036866734389375979139999774234902622223461854609/1893432243208594427566232746862064669216670789252554503173210413697395495872233472", + "-4793935672650001828036850549394548775426032879291549123551977698303/1893432243208594427566232746862064669216670789252554503173210413697395495872233472" + ], + "sign": "below" + }, + "upper": { + "a": "843580241257/500000000000000", + "moment_minus_one": [ + "19340341929796331821218206081147621726943725123/51321583788521501925121414324145880618052858113937946177437696", + "77361367719192864010399129134516689445719162375/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "1427065351508066933132819636128431341798609366641503451291771980053/3786864486417188855132465493724129338433341578505109006346420827394790991744466944", + "1427065351508066933132852006118085749344969902715429971548755428361/3786864486417188855132465493724129338433341578505109006346420827394790991744466944" + ], + "sign": "above" + } + }, + { + "claims": [ + 1196, + 1204, + 1225 + ], + "id": "W9", + "idle_mass_per_call": "1642", + "kappa_cap_exact": "210887818459/125210887818459", + "local": { + "1": "2364", + "2": "498", + "3": "414", + "4": "126", + "5": "84", + "8": "8" + }, + "lower": { + "a": "1687102547671/1000000000000000", + "moment_minus_one": [ + "-132878722014152101651940242208388855198628322389/205286335154086007700485657296583522472211432455751784709750784", + "-132878722014144564665435541252021175527311253277/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "-2451179777836534978903301387688255067439984046640809056103024460831/3786864486417188855132465493724129338433341578505109006346420827394790991744466944", + "-2451179777836534978903269016577706983482124939501114109708751220077/3786864486417188855132465493724129338433341578505109006346420827394790991744466944" + ], + "sign": "below" + }, + "upper": { + "a": "210887818459/125000000000000", + "moment_minus_one": [ + "464262869648118488312918374293016418746516428845/205286335154086007700485657296583522472211432455751784709750784", + "464262869648126025299423075276961952808447825381/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "4282069169662425964666567414639775969496698082738408732595515798301/1893432243208594427566232746862064669216670789252554503173210413697395495872233472", + "8564138339324851929333167200390100023069701255318051637685684153267/3786864486417188855132465493724129338433341578505109006346420827394790991744466944" + ], + "sign": "above" + } + }, + { + "claims": [ + 1148 + ], + "id": "W3", + "idle_mass_per_call": "1642", + "kappa_cap_exact": "1687062088401/1001687062088401", + "local": { + "1": "2364", + "2": "498", + "3": "412", + "4": "130", + "5": "82", + "8": "8" + }, + "lower": { + "a": "4217655221/2500000000000", + "moment_minus_one": [ + "-122498388001115797663164837169473877208123182493/102643167577043003850242828648291761236105716227875892354875392", + "-244996776002224058159603062941171800022364838641/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "-4519392825797082832262145700949053454342894561706712460867718161755/3786864486417188855132465493724129338433341578505109006346420827394790991744466944", + "-564924103224635354032764166133057269877068248806228143312327629593/473358060802148606891558186715516167304167697313138625793302603424348873968058368" + ], + "sign": "below" + }, + "upper": { + "a": "1687062088401/1000000000000000", + "moment_minus_one": [ + "176079547155420270353105377558004595418744532239/102643167577043003850242828648291761236105716227875892354875392", + "176079547155424038936468683270681844857664208387/102643167577043003850242828648291761236105716227875892354875392" + ], + "refined_moment_minus_one": [ + "3248094342990748549010363048629429917703272721201273549386180333505/1893432243208594427566232746862064669216670789252554503173210413697395495872233472", + "203005896436921784313148702160732972839104467509041125529022225525/118339515200537151722889546678879041826041924328284656448325650856087218492014592" + ], + "sign": "above" + } + }, + { + "claims": [ + 1178 + ], + "id": "W6", + "idle_mass_per_call": "1642", + "kappa_cap_exact": "1686657172581/1001686657172581", + "local": { + "1": "2372", + "2": "494", + "3": "414", + "4": "126", + "5": "84", + "8": "8" + }, + "lower": { + "a": "84332858629/50000000000000", + "moment_minus_one": [ + "-54902427349483654231786357258341044809069710871/29326619307726572528640808185226217496030204636535969244250112", + "-384316991446378040644844344811500123291324958677/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "-7089397184389423133475855076460636624221755031055684904237380156077/3786864486417188855132465493724129338433341578505109006346420827394790991744466944", + "-1772349296097355783368955674199535244903216567651484076475154772821/946716121604297213783116373431032334608335394626277251586605206848697747936116736" + ], + "sign": "below" + }, + "upper": { + "a": "1686657172581/1000000000000000", + "moment_minus_one": [ + "212982355803860587543228047275289685114360900439/205286335154086007700485657296583522472211432455751784709750784", + "212982355803868126520888203299770433629131635365/205286335154086007700485657296583522472211432455751784709750784" + ], + "refined_moment_minus_one": [ + "561261572818526552079000083969137741714731811586890266720816342005/540980640916741265018923641960589905490477368357872715192345832484970141677780992", + "982207752432421466138258241861614959182631217840188905553759045571/946716121604297213783116373431032334608335394626277251586605206848697747936116736" + ], + "sign": "above" + } + }, + { + "claims": [ + 1193, + 1239 + ], + "id": "W7", + "idle_mass_per_call": "545954/333", + "kappa_cap_exact": "843259763177/500843259763177", + "local": { + "1": "783550/333", + "2": "169496/333", + "3": "137362/333", + "4": "42458/333", + "5": "82", + "8": "8" + }, + "lower": { + "a": "1686519526353/1000000000000000", + "moment_minus_one": [ + "-8549806939633903484057850805712327950422587617623/7595594400701182284917969319973590331471823000862816034260779008", + "-8549806939633624519585159043404262372161541039091/7595594400701182284917969319973590331471823000862816034260779008" + ], + "refined_moment_minus_one": [ + "-39429025123761902883292784049480924814186935709424290192112649147535/35028496499358996909975305816948196380508409601172258308704392653401816673636319232", + "-78858050247523805766584969027318371126272997851021663950011201922863/70056992998717993819950611633896392761016819202344516617408785306803633347272638464" + ], + "sign": "below" + }, + "upper": { + "a": "843259763177/500000000000000", + "moment_minus_one": [ + "242000636401702173262655579128541698826207014045/135635614298235397944963737856671255919139696443978857754656768", + "6776017819247800333590702097263486378252066857701/3797797200350591142458984659986795165735911500431408017130389504" + ], + "refined_moment_minus_one": [ + "249990933101115701992283202212671544500054784895740628979495722345415/140113985997435987639901223267792785522033638404689033234817570613607266694545276928", + "249990933101115701992284400355958501508639855583481089733871520969833/140113985997435987639901223267792785522033638404689033234817570613607266694545276928" + ], + "sign": "above" + } + } + ], + "published_strict_cap": "0.001687314840", + "refinement_endpoint_decisions": 18, + "scope": "Frozen PR1264 extraction and coverage-law relaxation arithmetic only. No realized circuit, owner, physical cost, supplier or full multiplication theorem check.", + "selected": { + "calls": 144, + "idle_mass_per_call": "1646", + "live": 14336, + "word": "W2" + }, + "semantic_controls": [ + "idle_rank_52", + "negative_local_count", + "local_mass_over_budget", + "inconclusive_is_not_rejection", + "wrong_live_normalization", + "idle_not_subprofile", + "same_ratio_wrong_absolute_call_count", + "boolean_in_aggregate", + "count_and_mass_preserving_profile_changes_sign", + "missing_centre_changes_sign", + "rank_48_instead_of_51_changes_lower_sign", + "upper_endpoint_used_as_lower", + "lower_endpoint_used_as_upper", + "W7_display_rounding_changes_lower_sign" + ], + "status": "PASS_INDEPENDENT_QUEUE_CEILINGS", + "upstream_blob_count": 21 +} diff --git a/research/independent-queue-ceilings/SOURCES.json b/research/independent-queue-ceilings/SOURCES.json new file mode 100644 index 0000000000..f1f2055ace --- /dev/null +++ b/research/independent-queue-ceilings/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "ee055dc44815497927ef618fc985b93c2dcbda2a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/INDEPENDENT1094.json", + "usage": "input", + "git_blob": "009a385e26858058a18188364078d162aa6f9519", + "sha256": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd" + }, + { + "path": "research/complex-queue-ceiling-census/RESULT.json", + "usage": "input", + "git_blob": "756f36f8503eb472a64f39ff132a2c4210238f8a", + "sha256": "c4654c57268ab81e92b8c8d0e00f3f8c8a29a201eafd3e76eea9db78ca8a1135" + }, + { + "path": "research/complex-queue-ceiling-census/SNAPSHOT.json", + "usage": "input", + "git_blob": "fe91d71c2a1140b236d440956c3626a36e7e1160", + "sha256": "b56518da8b94554560c9643a7bca97075622dd8beb0996e75e7b8036cc0b4875" + } + ] +} diff --git a/research/independent-queue-ceilings/TASK.json b/research/independent-queue-ceilings/TASK.json new file mode 100644 index 0000000000..2184c73b56 --- /dev/null +++ b/research/independent-queue-ceilings/TASK.json @@ -0,0 +1,244 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 3, + "base_commit": "ee055dc44815497927ef618fc985b93c2dcbda2a", + "original_card": { + "id": "independent-moment", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "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." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently reconstruct the frozen PR1264 fourteen-claim ledger split from its pinned JSON source blobs and certify all nine packing-relaxation brackets with a separately written integer-square-root power enclosure. Include the selected PR1094 split and mixed-provider rational counts; do not re-audit physical realizability or claim novelty for the ceiling theorem.", + "scope_change_reason": "The suggested selected-supplier ledger and endpoint audits are already covered by PR1051/1052/1069/1091/1262/1293/1421. This contribution changes the audited object to the frozen PR1264 nine-profile planning census, preserving the card's independent exact-enclosure and source-ledger method. No supplier or architecture is changed.", + "bottleneck_link": "Revision 3 uses the PR1240/1264 ceilings to direct research away from packing. A separately implemented all-profile arithmetic audit makes that planning evidence independently checkable.", + "budget_minutes": 60, + "stop_rule": "One sixty-minute session: stop after the frozen fourteen claims, nine brackets, selected split, exact controls and source binding. Do not extend to the moving PR queue or perform physical supplier replay.", + "outcome": "completed", + "evidence": "RESULT.json: all 14 original aggregate/idle pairs reconstruct nine exact local profiles; all 18 bracket signs pass at 96/192 bits and again at 128/256 bits; selected PR1094 split matches W2. 21 immutable source blobs, 14 semantic controls, 2640 exact power comparisons, 72 zero-saving costs, and 13 corruption/relocation test groups. Four live counts remain template-derived and are explicitly identified.", + "author": "Hanson Sun (bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance with scope selection, source inspection, implementation, proof explanation, testing and packaging.", + "open_questions": [ + { + "question": "Can the four template-derived live counts (#1124, #1130, #1178, #1195) be tied to explicit physical inventories at their pinned heads?", + "why_it_matters": "This would replace an inherited source-extraction premise with a direct inventory binding, without changing any certified arithmetic or kappa.", + "first_step": "Locate each frozen template/owner inventory and recount live data families separately from physical roles.", + "blocked_by": "Those additional original inventories and physical reconstruction are outside the twenty-one receipt blobs audited here." + } + ], + "selection": { + "seed": "488b8bb97d866ded02e80a47a4e9d7e1", + "track": "independent-verification", + "scope_key": "c6f2494b197df3bc3591", + "method": "Independent enclosure allowed by the card; rebuild local and idle aggregate split from original pinned JSON receipts." + }, + "entry_overlap": { + "searched_at": "2026-10-14T04:09:02.834266+00:00", + "open_prs": 732, + "discussions": 253, + "complete_pagination": true, + "nearby": [ + "PR1240: predecessor ceiling and atanh/Taylor engine", + "PR1264: predecessor fourteen-claim extraction and nine ceilings", + "PR1605: rank-one block budgets, independently checks baseline only", + "PR1577 and PR706: prior integer-root endpoint method on other profiles", + "Discussion1606: changed port-count lever", + "Discussion1328: changed coverage-law lever" + ], + "limits": "Title/body/comments and top-level package search; no code-diff-wide novelty claim." + }, + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1620", + "claim_expiry_utc": "2026-10-14T06:12:00Z" + }, + "predecessor_credit": [ + { + "pr": 1124, + "author": "jeremykothe2", + "frozen_head": "7c0e3ee0e2d4f6c00d033a4f1dfe4e793e7ecae4" + }, + { + "pr": 1129, + "author": "aliromman", + "frozen_head": "a007dc2e1cc7ae7e8f7ec1343e8883fe43259f21" + }, + { + "pr": 1130, + "author": "jeremykothe2", + "frozen_head": "1558508e5cbff0b7c534d1c4cc7a0fb1b7145c1c" + }, + { + "pr": 1131, + "author": "chafreaky", + "frozen_head": "fcdc42737b703323d8ed550a528141a482e68e96" + }, + { + "pr": 1148, + "author": "tomdif", + "frozen_head": "506ea08dd77388105682044ebb0848ce9b274964" + }, + { + "pr": 1152, + "author": "chafreaky", + "frozen_head": "d376209304f05551f975b0ddf6eaa84edc4ae31a" + }, + { + "pr": 1157, + "author": "rohanarun", + "frozen_head": "c5647aecc8ff44e49776860bb75520bfe3e88f1e" + }, + { + "pr": 1178, + "author": "rohanarun", + "frozen_head": "6d4d0dd1c2df531a3350495dd15e00105793c52d" + }, + { + "pr": 1193, + "author": "jeremydiviney", + "frozen_head": "4e392e90e3fca8f395e35d6a23644920160a9f0f" + }, + { + "pr": 1195, + "author": "mdumitrean", + "frozen_head": "cc1b023b123622abba467c7933f3759f8034c753" + }, + { + "pr": 1196, + "author": "chafreaky", + "frozen_head": "7015903d1d01a2b50ff16f85184edc2686f69e37" + }, + { + "pr": 1204, + "author": "GamingPuzzled", + "frozen_head": "d49f96b75257c8a5eb4862eb99fbaffc738dcc1b" + }, + { + "pr": 1225, + "author": "rohanarun", + "frozen_head": "aac9ce7d83e02989eed76e08815cfd2399214e90" + }, + { + "pr": 1239, + "author": "GamingPuzzled", + "frozen_head": "12e04a30d7381a2a60bf2d7260febcb37f14e454" + } + ], + "nearby_verification_heads": [ + { + "number": 1605, + "author": { + "login": "Arham-Tahir64" + }, + "headRefOid": "488f2ecf1835c6d813e96543656dddf0062fdc9a", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1605" + }, + { + "number": 1577, + "author": { + "login": "Arham-Tahir64" + }, + "headRefOid": "b024b3e12c8911312e1fcf07417e076168602a01", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1577" + }, + { + "number": 706, + "author": { + "login": "arkfx" + }, + "headRefOid": "0f7dbb54948775c010b5e5bc8ab3cf92a52a9b25", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/706" + } + ], + "final_overlap": { + "searched_at": "2026-10-14T04:24:11.975086+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T04:23:32.662797+00:00", + "complete_pagination": true, + "records": 740 + }, + "discussions": { + "fetched_at": "2026-10-14T04:24:11.929868+00:00", + "complete_pagination": true, + "records": 267 + } + }, + "warnings": [], + "matches_total": 8, + "related_matches": [ + { + "kind": "discussion", + "number": 1620, + "head": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1620", + "title": "CLAIM: independent integer-root audit of the frozen nine packing ceilings" + }, + { + "kind": "discussion", + "number": 1561, + "head": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1561", + "title": "Independent integer-root audit of PR1536 200-digit complex endpoints" + }, + { + "kind": "pr", + "number": 1577, + "head": "b024b3e12c8911312e1fcf07417e076168602a01", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1577", + "title": "Independent integer-root audit of PR1536's 200-digit complex endpoints" + }, + { + "kind": "discussion-comment", + "number": 1166, + "head": null, + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18909652", + "title": "Handoffs and requests for independent checks" + } + ], + "assessment": "No new same-domain audit found in covered titles/bodies/comments. PR1577 and Discussion1561 remain a different endpoint domain; PR1264 is the credited predecessor. This is independent corroboration, not a novelty claim.", + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission." + }, + "publication_base_check": { + "origin_main": "0a201997097b8a89b638f3a2afcb35db4184c8b2", + "required_inputs_unchanged_from_task_base": true + }, + "validation": { + "python": "3.12.13", + "platform": "macOS arm64", + "registered_replay": "passed", + "test_groups": 13, + "primary_census_replay": "passed unchanged", + "selected_record_check": "passed unchanged", + "hosted_ci": "not run locally" + } +} diff --git a/research/independent-queue-ceilings/UPSTREAM.json b/research/independent-queue-ceilings/UPSTREAM.json new file mode 100644 index 0000000000..d42aa5ce54 --- /dev/null +++ b/research/independent-queue-ceilings/UPSTREAM.json @@ -0,0 +1,173 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "records": [ + { + "head": "12e04a30d7381a2a60bf2d7260febcb37f14e454", + "path": "research/mixed-fusions-x54-t37/CLAIM.json", + "git_blob": "6c8a74450ac18d3752080e72a00a13dc36005561", + "sha256": "b78546b8b23e36c0ba87e3f16c58a530f5efec4f65e250e95b717cd1dc5dc739", + "local": "inputs/6c8a74450ac18d3752080e72a00a13dc36005561.json.gz", + "size": 1241 + }, + { + "head": "1558508e5cbff0b7c534d1c4cc7a0fb1b7145c1c", + "path": "research/gauge44-ends7-x54-t16/RESULT.json", + "git_blob": "b59a7802f700b5b91eef5e8b13829b05897051c0", + "sha256": "e84145a136dce8483034ed536795568dfc15ede3e44f5e07ff86620eec4dbd98", + "local": "inputs/b59a7802f700b5b91eef5e8b13829b05897051c0.json.gz", + "size": 3827 + }, + { + "head": "4e392e90e3fca8f395e35d6a23644920160a9f0f", + "path": "research/mixed-x54-t37/CLAIM.json", + "git_blob": "db33352b51efa9bc8538dd65dd6abc867dd587cc", + "sha256": "3f3f69063862ccc9c6f2a4d0deb57c2b17e687313380a16f3213ba02eb0b36de", + "local": "inputs/db33352b51efa9bc8538dd65dd6abc867dd587cc.json.gz", + "size": 1318 + }, + { + "head": "506ea08dd77388105682044ebb0848ce9b274964", + "path": "research/k8-joint-entrances/SPEC.json", + "git_blob": "9aeea5c043aafa9ce0cd5f05fe6b404de5d5454f", + "sha256": "55bdb68d5d126c6be0e0acc419bd62301a978afd514f9834ed1e08b1aa4f563e", + "local": "inputs/9aeea5c043aafa9ce0cd5f05fe6b404de5d5454f.json.gz", + "size": 24422 + }, + { + "head": "506ea08dd77388105682044ebb0848ce9b274964", + "path": "research/k8-joint-entrances/evidence/ASSEMBLY.json", + "git_blob": "2a7f39918bd9ed4a01543e2de65343fe53cbcea3", + "sha256": "ebac2870cf0f52d6ac0e8213bb766f4b980a253d6d9d207a0e29bafca8121b4b", + "local": "inputs/2a7f39918bd9ed4a01543e2de65343fe53cbcea3.json.gz", + "size": 85004 + }, + { + "head": "6d4d0dd1c2df531a3350495dd15e00105793c52d", + "path": "research/k8-dem-x54/CLAIM.json", + "git_blob": "bf5cc64c1b337e0979a435703c3ce7a721957cd6", + "sha256": "4d64a5b1ff04dfd0a25d7ca0ea551a5c314c4dc9fdd6a3bc99f93989e682f8c4", + "local": "inputs/bf5cc64c1b337e0979a435703c3ce7a721957cd6.json.gz", + "size": 1173 + }, + { + "head": "6d4d0dd1c2df531a3350495dd15e00105793c52d", + "path": "research/k8-dem-x54/evidence/ASSEMBLY.json", + "git_blob": "e7e2fa84d6b05cae0879c09741ea5aa799297751", + "sha256": "8763074bfa264d09fb0b9689a046c71e5d95befab294a1016dc0a328686fe4ee", + "local": "inputs/e7e2fa84d6b05cae0879c09741ea5aa799297751.json.gz", + "size": 85674 + }, + { + "head": "7015903d1d01a2b50ff16f85184edc2686f69e37", + "path": "research/complex-t37-joint-x54-owners/CLAIM.json", + "git_blob": "9696f82ff045a3e88ec7a585664bf6d2ed5545dc", + "sha256": "2e26c180b3d7027740f4e0b484c1332ead0ed16605a175b992dbc0f5a6be0b5c", + "local": "inputs/9696f82ff045a3e88ec7a585664bf6d2ed5545dc.json.gz", + "size": 1319 + }, + { + "head": "7c0e3ee0e2d4f6c00d033a4f1dfe4e793e7ecae4", + "path": "research/gauge44-ends7-x54-t16/RESULT.json", + "git_blob": "087f35df23bd847ec4437decb4796486d231f33a", + "sha256": "0cabd7661da0d91e9141f6d4bfe8530e4c29cb30add3c67aecb71e2b5ffb9120", + "local": "inputs/087f35df23bd847ec4437decb4796486d231f33a.json.gz", + "size": 3915 + }, + { + "head": "a007dc2e1cc7ae7e8f7ec1343e8883fe43259f21", + "path": "research/r480-owner-optimum/data/SPEC.json", + "git_blob": "579a28450ef4a8b918aab3a369b2a1f9bc2a8bb2", + "sha256": "7dabffb3f25e95233025e55235b76db51d96fa070d6f5bfd0a28005f5efa2642", + "local": "inputs/579a28450ef4a8b918aab3a369b2a1f9bc2a8bb2.json.gz", + "size": 39346 + }, + { + "head": "a007dc2e1cc7ae7e8f7ec1343e8883fe43259f21", + "path": "research/r480-owner-optimum/evidence/ASSEMBLY.json", + "git_blob": "0e696d96ee15219b1b9008c9162649ccf906a3d9", + "sha256": "d2ef417968ea68bd5abc0ad8d2d27ba99bfcede6cff8743a25ec34358a54cb9b", + "local": "inputs/0e696d96ee15219b1b9008c9162649ccf906a3d9.json.gz", + "size": 84283 + }, + { + "head": "aac9ce7d83e02989eed76e08815cfd2399214e90", + "path": "research/joint-x54-t37/CANDIDATE.json", + "git_blob": "79190f04e19b1a6bc4d277f0ae06e1c8acac10d4", + "sha256": "5f28fa2a491d100f266f1ab15e7acc7186a1a671afe4e631dca589f739da4ff3", + "local": "inputs/79190f04e19b1a6bc4d277f0ae06e1c8acac10d4.json.gz", + "size": 1822 + }, + { + "head": "aac9ce7d83e02989eed76e08815cfd2399214e90", + "path": "research/joint-x54-t37/evidence/strict/ASSEMBLY.json", + "git_blob": "5b3cdd2785bec7aad0fe91d704c76db8bab0ce6a", + "sha256": "5cb1346fe9c50314c6340f2ce7963a7fd3dbc73e3a4698e85c6c4f634c8c89ad", + "local": "inputs/5b3cdd2785bec7aad0fe91d704c76db8bab0ce6a.json.gz", + "size": 85542 + }, + { + "head": "c5647aecc8ff44e49776860bb75520bfe3e88f1e", + "path": "research/k8-x54-t37/data/SPEC.json", + "git_blob": "15c3572aa90d618dc41801e6fb4b58bab31d41c0", + "sha256": "2ada5abf34eee9a5d273fb07b11e4b6ddd55e64cb3a9e5e54bcf0b51f274488f", + "local": "inputs/15c3572aa90d618dc41801e6fb4b58bab31d41c0.json.gz", + "size": 39338 + }, + { + "head": "c5647aecc8ff44e49776860bb75520bfe3e88f1e", + "path": "research/k8-x54-t37/evidence/k8-x54/ASSEMBLY.json", + "git_blob": "da4786ac7f77ed5a0b2eab886ef5c4c83022b7ff", + "sha256": "66e18095164c9036ad0b698b3778e9d5d46ad88b5dd6f6ee1a3b6f91c51ecde1", + "local": "inputs/da4786ac7f77ed5a0b2eab886ef5c4c83022b7ff.json.gz", + "size": 84206 + }, + { + "head": "cc1b023b123622abba467c7933f3759f8034c753", + "path": "research/k8-source-holder-fusions/CLAIM.json", + "git_blob": "b7853d4e8faba09df248f3e7be0843862aa1e2b7", + "sha256": "f9729f9a42b9f3f1e438028f0e2338ebb14a19933faa8230cd8c3f530c95751f", + "local": "inputs/b7853d4e8faba09df248f3e7be0843862aa1e2b7.json.gz", + "size": 1632 + }, + { + "head": "cc1b023b123622abba467c7933f3759f8034c753", + "path": "research/k8-source-holder-fusions/evidence/ASSEMBLY.json", + "git_blob": "f126fc2c7fc41eadbf41a0369db0f66789a99419", + "sha256": "14bca9de8823ef199134906755bba79c1cfda044296634263097e283d3a8bc49", + "local": "inputs/f126fc2c7fc41eadbf41a0369db0f66789a99419.json.gz", + "size": 85743 + }, + { + "head": "d376209304f05551f975b0ddf6eaa84edc4ae31a", + "path": "research/complex-t37-ends7-owners/CLAIM.json", + "git_blob": "86721e03e62ef7873fca425a765ec338862f6e0d", + "sha256": "82923581c50be03d09282ec43a6035167a802473f96d28c6d65cc4cce2ef83d0", + "local": "inputs/86721e03e62ef7873fca425a765ec338862f6e0d.json.gz", + "size": 1073 + }, + { + "head": "d49f96b75257c8a5eb4862eb99fbaffc738dcc1b", + "path": "research/k8-joint-x54-t37/data/SPEC.json", + "git_blob": "449d9554d625c0d7aefe5ec2cd4845d7a03e957f", + "sha256": "e0e563af9789d76dd641bfe38eddc785774c55aaf5d9c3908518e288e6a1c5e8", + "local": "inputs/449d9554d625c0d7aefe5ec2cd4845d7a03e957f.json.gz", + "size": 39347 + }, + { + "head": "d49f96b75257c8a5eb4862eb99fbaffc738dcc1b", + "path": "research/k8-joint-x54-t37/evidence/ASSEMBLY.json", + "git_blob": "5ed2f48baaa9a2eefc151e065256f58fcfac9711", + "sha256": "71a9e13b96772c0d6338f109d1210e2ca17e8cfeab87004e3c67fca24dbc2fe2", + "local": "inputs/5ed2f48baaa9a2eefc151e065256f58fcfac9711.json.gz", + "size": 85539 + }, + { + "head": "fcdc42737b703323d8ed550a528141a482e68e96", + "path": "research/complex-t37-seven-slot-owners/CLAIM.json", + "git_blob": "084f76cf2381bb161a580bb85e5f43f20d9e21eb", + "sha256": "e02bfcebc992818318575c331309eaf96456786a3d93567853b4ec83aa194eaf", + "local": "inputs/084f76cf2381bb161a580bb85e5f43f20d9e21eb.json.gz", + "size": 1204 + } + ] +} diff --git a/research/independent-queue-ceilings/VERIFY.json b/research/independent-queue-ceilings/VERIFY.json new file mode 100644 index 0000000000..f9e4f5ff96 --- /dev/null +++ b/research/independent-queue-ceilings/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/INDEPENDENT1094.json", + "research/complex-queue-ceiling-census/RESULT.json", + "research/complex-queue-ceiling-census/SNAPSHOT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All frozen source extractions, nine exact brackets at two precisions, selected split, semantic controls, direct algebraic oracle and complete receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py", + "-v" + ], + "timeout_seconds": 120, + "checks": "13 arithmetic, schema, source-inventory, corruption and optimized read-only relocation tests." + } + ] +} diff --git a/research/independent-queue-ceilings/bounds.py b/research/independent-queue-ceilings/bounds.py new file mode 100644 index 0000000000..a1cdb12528 --- /dev/null +++ b/research/independent-queue-ceilings/bounds.py @@ -0,0 +1,115 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Directed integer-root enclosures; no logarithms, exponentials or floats. + +Written for this audit by Hanson Sun with OpenAI Codex assistance. The method +has precedents in PR706/PR1577; no code from either implementation is imported. +""" +from fractions import Fraction as Q +from functools import lru_cache +from math import isqrt + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ceil_div(n, d): + return -(-n // d) + + +def sqrt_up(n): + r = isqrt(n) + return r + (r * r != n) + + +@lru_cache(maxsize=None) +def root_ladder(n, d, exponent_bits, precision): + """Enclose (n/d)^(1/2^j), j=1..exponent_bits, scaled by 2^precision.""" + require(type(n) is int and type(d) is int and n >= d > 0, + 'root base must be a rational >= 1') + require(type(exponent_bits) is int and type(precision) is int + and 1 <= exponent_bits <= 1024 and 1 <= precision <= 2048, + 'unsupported root precision') + scale = 1 << precision + lo, hi = n * scale // d, ceil_div(n * scale, d) + ladder = [] + for _ in range(exponent_bits): + lo, hi = isqrt(lo * scale), sqrt_up(hi * scale) + ladder.append((lo, hi)) + return tuple(ladder) + + +def rational_power(n, d, a, exponent_bits=96, precision=192): + """Return rational lo <= (n/d)^a <= hi for n/d >= 1 and 0 <= a <= 1. + + The exponent is bracketed by adjacent dyadics. Each selected binary digit + multiplies an independently outward-rounded member of the root ladder. + All intermediate products are rounded outwards before the next product. + """ + require(type(a) in (int, Q) and Q(0) <= a <= Q(1), 'exponent outside [0,1]') + a = Q(a) + roots = root_ladder(n, d, exponent_bits, precision) + scale, denominator = 1 << precision, 1 << exponent_bits + low_k = a.numerator * denominator // a.denominator + high_k = ceil_div(a.numerator * denominator, a.denominator) + + def dyadic(k, upper): + if k == denominator: + return ceil_div(n * scale, d) if upper else n * scale // d + value = scale + for j, pair in enumerate(roots, 1): + if k & (1 << (exponent_bits - j)): + product = value * pair[upper] + value = ceil_div(product, scale) if upper else product // scale + return value + + return Q(dyadic(low_k, False), scale), Q(dyadic(high_k, True), scale) + + +def child_cost(rank, width, a, exponent_bits=96, precision=192): + require(type(rank) is int and type(width) is int and 0 < rank < width, + 'child rank must lie strictly between zero and width') + lo, hi = rational_power(width, rank, a, exponent_bits, precision) + return Q(rank, width) * lo, Q(rank, width) * hi + + +def relaxation(local, a, *, width=73, families=896, stages=9, centre=64, + cap=51, exponent_bits=96, precision=192): + """Fully charged local profile plus optimistically concentrated idle mass. + + This is only the PR1240 coverage-law relaxation. Physical supplier costs + and other interfaces are not inferred from this numerical calculation. + """ + require(type(width) is int and type(cap) is int and 0 < cap < width + and 2 * cap * cap < width * width, 'invalid halving-guard cap') + require(type(families) is int and families > 0 + and type(stages) is int and stages > 0, 'invalid family normalization') + require(type(centre) in (int, Q) and centre >= 0, 'invalid centre charge') + require(type(local) is dict and bool(local), 'empty local profile') + for rank, count in local.items(): + require(type(rank) is int and 0 < rank < width + and type(count) in (int, Q) and count >= 0, 'invalid local child') + w = Q(families, stages) + local_mass = sum(rank * count for rank, count in local.items()) + idle_mass = (width - 1) * w + centre - local_mass + require(idle_mass >= 0, 'local mass exceeds coverage budget') + lo = hi = Q(0) + for rank, count in sorted(local.items()): + lower, upper = child_cost(rank, width, a, exponent_bits, precision) + lo += count * lower + hi += count * upper + lower, upper = child_cost(cap, width, a, exponent_bits, precision) + lo += idle_mass / cap * lower + hi += idle_mass / cap * upper + return lo / w, hi / w + + +def side(interval): + lo, hi = interval + require(lo <= hi, 'reversed interval') + if hi < 1: + return 'below' + if lo > 1: + return 'above' + raise ValueError('interval does not separate one') diff --git a/research/independent-queue-ceilings/inputs/084f76cf2381bb161a580bb85e5f43f20d9e21eb.json.gz b/research/independent-queue-ceilings/inputs/084f76cf2381bb161a580bb85e5f43f20d9e21eb.json.gz new file mode 100644 index 0000000000..b29985881d Binary files /dev/null and b/research/independent-queue-ceilings/inputs/084f76cf2381bb161a580bb85e5f43f20d9e21eb.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/087f35df23bd847ec4437decb4796486d231f33a.json.gz b/research/independent-queue-ceilings/inputs/087f35df23bd847ec4437decb4796486d231f33a.json.gz new file mode 100644 index 0000000000..e610137f1a Binary files /dev/null and b/research/independent-queue-ceilings/inputs/087f35df23bd847ec4437decb4796486d231f33a.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/0e696d96ee15219b1b9008c9162649ccf906a3d9.json.gz b/research/independent-queue-ceilings/inputs/0e696d96ee15219b1b9008c9162649ccf906a3d9.json.gz new file mode 100644 index 0000000000..6ce58c5766 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/0e696d96ee15219b1b9008c9162649ccf906a3d9.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/15c3572aa90d618dc41801e6fb4b58bab31d41c0.json.gz b/research/independent-queue-ceilings/inputs/15c3572aa90d618dc41801e6fb4b58bab31d41c0.json.gz new file mode 100644 index 0000000000..caff0817be Binary files /dev/null and b/research/independent-queue-ceilings/inputs/15c3572aa90d618dc41801e6fb4b58bab31d41c0.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/2a7f39918bd9ed4a01543e2de65343fe53cbcea3.json.gz b/research/independent-queue-ceilings/inputs/2a7f39918bd9ed4a01543e2de65343fe53cbcea3.json.gz new file mode 100644 index 0000000000..c92a6b2509 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/2a7f39918bd9ed4a01543e2de65343fe53cbcea3.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/449d9554d625c0d7aefe5ec2cd4845d7a03e957f.json.gz b/research/independent-queue-ceilings/inputs/449d9554d625c0d7aefe5ec2cd4845d7a03e957f.json.gz new file mode 100644 index 0000000000..af45c5fa18 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/449d9554d625c0d7aefe5ec2cd4845d7a03e957f.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/579a28450ef4a8b918aab3a369b2a1f9bc2a8bb2.json.gz b/research/independent-queue-ceilings/inputs/579a28450ef4a8b918aab3a369b2a1f9bc2a8bb2.json.gz new file mode 100644 index 0000000000..fb7f9e3116 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/579a28450ef4a8b918aab3a369b2a1f9bc2a8bb2.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/5b3cdd2785bec7aad0fe91d704c76db8bab0ce6a.json.gz b/research/independent-queue-ceilings/inputs/5b3cdd2785bec7aad0fe91d704c76db8bab0ce6a.json.gz new file mode 100644 index 0000000000..049db8e95d Binary files /dev/null and b/research/independent-queue-ceilings/inputs/5b3cdd2785bec7aad0fe91d704c76db8bab0ce6a.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/5ed2f48baaa9a2eefc151e065256f58fcfac9711.json.gz b/research/independent-queue-ceilings/inputs/5ed2f48baaa9a2eefc151e065256f58fcfac9711.json.gz new file mode 100644 index 0000000000..9ebd49302c Binary files /dev/null and b/research/independent-queue-ceilings/inputs/5ed2f48baaa9a2eefc151e065256f58fcfac9711.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/6c8a74450ac18d3752080e72a00a13dc36005561.json.gz b/research/independent-queue-ceilings/inputs/6c8a74450ac18d3752080e72a00a13dc36005561.json.gz new file mode 100644 index 0000000000..6b10a88e23 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/6c8a74450ac18d3752080e72a00a13dc36005561.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/79190f04e19b1a6bc4d277f0ae06e1c8acac10d4.json.gz b/research/independent-queue-ceilings/inputs/79190f04e19b1a6bc4d277f0ae06e1c8acac10d4.json.gz new file mode 100644 index 0000000000..24bf571891 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/79190f04e19b1a6bc4d277f0ae06e1c8acac10d4.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/86721e03e62ef7873fca425a765ec338862f6e0d.json.gz b/research/independent-queue-ceilings/inputs/86721e03e62ef7873fca425a765ec338862f6e0d.json.gz new file mode 100644 index 0000000000..36a475235f Binary files /dev/null and b/research/independent-queue-ceilings/inputs/86721e03e62ef7873fca425a765ec338862f6e0d.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/9696f82ff045a3e88ec7a585664bf6d2ed5545dc.json.gz b/research/independent-queue-ceilings/inputs/9696f82ff045a3e88ec7a585664bf6d2ed5545dc.json.gz new file mode 100644 index 0000000000..2e832ce07d Binary files /dev/null and b/research/independent-queue-ceilings/inputs/9696f82ff045a3e88ec7a585664bf6d2ed5545dc.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/9aeea5c043aafa9ce0cd5f05fe6b404de5d5454f.json.gz b/research/independent-queue-ceilings/inputs/9aeea5c043aafa9ce0cd5f05fe6b404de5d5454f.json.gz new file mode 100644 index 0000000000..1a1156fbeb Binary files /dev/null and b/research/independent-queue-ceilings/inputs/9aeea5c043aafa9ce0cd5f05fe6b404de5d5454f.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/b59a7802f700b5b91eef5e8b13829b05897051c0.json.gz b/research/independent-queue-ceilings/inputs/b59a7802f700b5b91eef5e8b13829b05897051c0.json.gz new file mode 100644 index 0000000000..a82e5e4dff Binary files /dev/null and b/research/independent-queue-ceilings/inputs/b59a7802f700b5b91eef5e8b13829b05897051c0.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/b7853d4e8faba09df248f3e7be0843862aa1e2b7.json.gz b/research/independent-queue-ceilings/inputs/b7853d4e8faba09df248f3e7be0843862aa1e2b7.json.gz new file mode 100644 index 0000000000..2af499d880 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/b7853d4e8faba09df248f3e7be0843862aa1e2b7.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/bf5cc64c1b337e0979a435703c3ce7a721957cd6.json.gz b/research/independent-queue-ceilings/inputs/bf5cc64c1b337e0979a435703c3ce7a721957cd6.json.gz new file mode 100644 index 0000000000..993994b05b Binary files /dev/null and b/research/independent-queue-ceilings/inputs/bf5cc64c1b337e0979a435703c3ce7a721957cd6.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/da4786ac7f77ed5a0b2eab886ef5c4c83022b7ff.json.gz b/research/independent-queue-ceilings/inputs/da4786ac7f77ed5a0b2eab886ef5c4c83022b7ff.json.gz new file mode 100644 index 0000000000..8405975d42 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/da4786ac7f77ed5a0b2eab886ef5c4c83022b7ff.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/db33352b51efa9bc8538dd65dd6abc867dd587cc.json.gz b/research/independent-queue-ceilings/inputs/db33352b51efa9bc8538dd65dd6abc867dd587cc.json.gz new file mode 100644 index 0000000000..ec044dec03 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/db33352b51efa9bc8538dd65dd6abc867dd587cc.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/e7e2fa84d6b05cae0879c09741ea5aa799297751.json.gz b/research/independent-queue-ceilings/inputs/e7e2fa84d6b05cae0879c09741ea5aa799297751.json.gz new file mode 100644 index 0000000000..468e063e79 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/e7e2fa84d6b05cae0879c09741ea5aa799297751.json.gz differ diff --git a/research/independent-queue-ceilings/inputs/f126fc2c7fc41eadbf41a0369db0f66789a99419.json.gz b/research/independent-queue-ceilings/inputs/f126fc2c7fc41eadbf41a0369db0f66789a99419.json.gz new file mode 100644 index 0000000000..5f432e26a3 Binary files /dev/null and b/research/independent-queue-ceilings/inputs/f126fc2c7fc41eadbf41a0369db0f66789a99419.json.gz differ diff --git a/research/independent-queue-ceilings/test_verify.py b/research/independent-queue-ceilings/test_verify.py new file mode 100644 index 0000000000..d556ad9c94 --- /dev/null +++ b/research/independent-queue-ceilings/test_verify.py @@ -0,0 +1,192 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Failure controls for arithmetic, extracted data, source pins and replay.""" +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import bounds as B +import verify as V + + +class AuditTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.external = V.load_external() + cls.snapshot = cls.external[V.SNAPSHOT] + cls.census = cls.external[V.CENSUS] + cls.upstream = V.load_upstream(cls.snapshot) + + def run_audit(self, snapshot=None, census=None, upstream=None): + return V.audit(self.snapshot if snapshot is None else snapshot, + self.census if census is None else census, + self.upstream if upstream is None else upstream, + self.external[V.ASSEMBLY], self.external[V.SELECTED_AUDIT]) + + def test_floor_square_root_is_not_an_upper_bound(self): + # Integer-power comparison, independent of the root recurrence, must + # detect an upper rounding replaced by floor at deliberately low precision. + B.root_ladder.cache_clear() + with patch.object(B, 'sqrt_up', B.isqrt): + _, hi = B.rational_power(2, 1, Q(1, 2), 1, 8) + self.assertLess(hi * hi, 2) + B.root_ladder.cache_clear() + lo, hi = B.rational_power(2, 1, Q(1, 2), 1, 8) + self.assertLessEqual(lo * lo, 2) + self.assertGreaterEqual(hi * hi, 2) + + def test_wrong_exponent_bit_order_breaks_exact_power(self): + B.root_ladder.cache_clear() + original = B.root_ladder + with patch.object(B, 'root_ladder', lambda *a: tuple(reversed(original(*a)))): + lo, hi = B.rational_power(3, 1, Q(1, 4), 2, 64) + self.assertFalse(lo**4 <= 3 <= hi**4) + + def test_lost_exponent_ceiling_breaks_non_dyadic_power(self): + # A floor dyadic exponent alone is insufficient for an upper bound. + _, hi = B.rational_power(2, 1, Q(1, 4), 2, 64) + self.assertLess(hi**3, 2) # cannot enclose 2^(1/3) + lo, hi = B.rational_power(2, 1, Q(1, 3), 2, 64) + self.assertLessEqual(lo**3, 2) + self.assertGreaterEqual(hi**3, 2) + + def test_unresolved_and_exact_equality_do_not_decide(self): + for interval in ((Q(9, 10), Q(11, 10)), (Q(1), Q(1)), (Q(2), Q(1))): + with self.assertRaises(ValueError): + B.side(interval) + + def test_fractional_mixed_profile_is_not_rounded(self): + census = deepcopy(self.census) + row = next(w for w in census['words'] if w['id'] == 'W7') + self.assertEqual(Q(row['local_profile_per_call']['3']), Q(137362, 333)) + self.assertEqual(Q(row['local_profile_per_call']['4']), Q(42458, 333)) + # Even the README's close display rounding, not just flooring to an + # integer, is not the exact mixed-provider profile. + row['local_profile_per_call']['3'] = '825/2' + with self.assertRaisesRegex(ValueError, 'unknown or repeated'): + self.run_audit(census=census) + + def test_omitted_profile_or_claim_fails(self): + census = deepcopy(self.census); census['words'].pop() + with self.assertRaisesRegex(ValueError, 'profile domain'): + self.run_audit(census=census) + snap = deepcopy(self.snapshot); snap['claims'].pop() + with self.assertRaisesRegex(ValueError, 'claim domain'): + self.run_audit(snapshot=snap) + + def test_wrong_membership_and_ceiling_fail(self): + census = deepcopy(self.census) + census['words'][0]['claims'][0] = 9999 + with self.assertRaisesRegex(ValueError, 'membership'): + self.run_audit(census=census) + census = deepcopy(self.census) + census['words'][0]['a_ceiling'] = str(Q(census['words'][0]['a_ceiling']) - V.GRID) + with self.assertRaisesRegex(ValueError, 'endpoint sign'): + self.run_audit(census=census) + + def test_wrong_source_provider_count_fails(self): + upstream = deepcopy(self.upstream) + claim = next(c for c in self.snapshot['claims'] if c['pr'] == 1195) + upstream[claim['head'], claim['profile_file']]['provider_counts']['gauge44'] += 9 + with self.assertRaisesRegex(ValueError, 'call count'): + V.reconstruct(claim, upstream) + + def test_missing_absolute_count_is_not_inferred_from_ratio(self): + # This is stronger than accepting W/N=896/9 without an original N. + claim = next(c for c in self.snapshot['claims'] if c['pr'] == 1124) + upstream = deepcopy(self.upstream) + del upstream[claim['head'], claim['profile_file']]['complete_invocations'] + with self.assertRaisesRegex(ValueError, 'source call counts'): + V.reconstruct(claim, upstream) + + def test_schema_rejects_boolean_negative_and_float(self): + for value in (True, -1, 1.0): + with self.assertRaises(ValueError): + V.histogram({'1': value}) + for a in (-Q(1, 10), Q(11, 10), True, 0.01): + with self.assertRaises(ValueError): + B.rational_power(73, 1, a) + + def test_source_corruption_and_inventory_omission(self): + with tempfile.TemporaryDirectory() as name: + temp = Path(name) + shutil.copytree(HERE, temp / 'package') + package = temp / 'package' + manifest = json.loads((package / 'UPSTREAM.json').read_text()) + row = manifest['records'][0] + target = package / row['local'] + raw = gzip.decompress(target.read_bytes()) + # Same-length content corruption; recompression headers are irrelevant. + raw = raw.replace(b'"kappa"', b'"KAPPA"', 1) + target.write_bytes(gzip.compress(raw, mtime=0)) + with self.assertRaisesRegex(ValueError, 'SHA256'): + V.load_upstream(self.snapshot, package) + # Even changing the secondary SHA256 cannot defeat the original Git blob. + row['sha256'] = hashlib.sha256(raw).hexdigest() + (package / 'UPSTREAM.json').write_text(V.canonical(manifest)) + with self.assertRaisesRegex(ValueError, 'Git blob'): + V.load_upstream(self.snapshot, package) + manifest['records'].pop() + (package / 'UPSTREAM.json').write_text(V.canonical(manifest)) + with self.assertRaisesRegex(ValueError, 'inventory'): + V.load_upstream(self.snapshot, package) + + def test_external_source_drift_and_inventory_omission(self): + with tempfile.TemporaryDirectory() as name: + temp = Path(name) + for relative in V.REQUIRED: + target = temp / relative + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(V.ROOT / relative, target) + package = temp / 'package'; package.mkdir() + shutil.copyfile(HERE / 'SOURCES.json', package / 'SOURCES.json') + target = temp / V.SNAPSHOT + target.write_bytes(target.read_bytes() + b' ') + with self.assertRaisesRegex(ValueError, 'source drift'): + V.load_external(temp, package) + sources = json.loads((package / 'SOURCES.json').read_text()) + sources['files'] = [r for r in sources['files'] if r['path'] != V.SNAPSHOT] + (package / 'SOURCES.json').write_text(V.canonical(sources)) + with self.assertRaisesRegex(ValueError, 'inventory'): + V.load_external(temp, package) + + def test_optimized_read_only_relocation_and_receipt_corruption(self): + with tempfile.TemporaryDirectory() as name: + root = Path(name) + package = root / 'research' / HERE.name + shutil.copytree(HERE, package) + for relative in V.REQUIRED: + target = root / relative + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(V.ROOT / relative, target) + files = sorted(p for p in root.rglob('*') if p.is_file()) + before = {p: p.read_bytes() for p in files} + for p in files: + p.chmod(0o444) + cmd = [sys.executable, '-I', '-O', '-B', str(package / 'verify.py')] + passed = subprocess.run(cmd, cwd=root, capture_output=True, text=True, timeout=30) + self.assertEqual(passed.returncode, 0, passed.stderr) + self.assertIn('PASS_INDEPENDENT_QUEUE_CEILINGS', passed.stdout) + self.assertEqual(before, {p: p.read_bytes() for p in files}) + receipt = package / 'RESULT.json'; receipt.chmod(0o644) + data = json.loads(receipt.read_text()) + data['endpoint_decisions'] = True + receipt.write_text(V.canonical(data)) + failed = subprocess.run(cmd, cwd=root, capture_output=True, text=True, timeout=30) + self.assertNotEqual(failed.returncode, 0) + self.assertIn('receipt differs', failed.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/independent-queue-ceilings/verify.py b/research/independent-queue-ceilings/verify.py new file mode 100644 index 0000000000..5c1744434a --- /dev/null +++ b/research/independent-queue-ceilings/verify.py @@ -0,0 +1,348 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent offline audit of the frozen PR1264 census; see README.md. + +Hanson Sun with substantial OpenAI Codex assistance. No predecessor executable +is imported. Default operation checks the complete deterministic receipt; +--write explicitly regenerates only this package's RESULT.json. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from bounds import child_cost, rational_power, relaxation, require, side + +ROOT = HERE.parents[1] +SNAPSHOT = 'research/complex-queue-ceiling-census/SNAPSHOT.json' +CENSUS = 'research/complex-queue-ceiling-census/RESULT.json' +ASSEMBLY = 'research/community-frontier1094-audit/ASSEMBLY.json' +SELECTED_AUDIT = 'research/community-frontier1094-audit/INDEPENDENT1094.json' +REQUIRED = {SNAPSHOT, CENSUS, ASSEMBLY, SELECTED_AUDIT} +GRID = Q(1, 10**15) + + +def canonical(value): + return json.dumps(value, indent=2, sort_keys=True) + '\n' + + +def same(a, b, message): + # JSON comparison must distinguish bool/int and float/int, unlike ==. + require(canonical(a) == canonical(b), message) + + +def load_external(root=ROOT, package=HERE): + sources = json.loads((package / 'SOURCES.json').read_text()) + inputs = [r for r in sources['files'] if r['usage'] == 'input'] + require(len(inputs) == len(REQUIRED) and {r['path'] for r in inputs} == REQUIRED, + 'external source inventory differs') + out = {} + for row in inputs: + raw = (root / row['path']).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row['sha256'], + 'external source drift: ' + row['path']) + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + require(blob == row['git_blob'], 'external Git blob differs') + out[row['path']] = json.loads(raw) + return out + + +def load_upstream(snapshot, package=HERE): + manifest = json.loads((package / 'UPSTREAM.json').read_text()) + require(manifest['repository'] == 'CrocSwap/integer-mult-bounds', 'wrong upstream repository') + expected = {(c['head'], c[k+'_file'], c[k+'_blob']) + for c in snapshot['claims'] for k in ('profile', 'idle')} + rows = manifest['records'] + keys = [(r['head'], r['path'], r['git_blob']) for r in rows] + require(len(keys) == len(set(keys)) and set(keys) == expected, + 'upstream input inventory differs') + out = {} + for row in rows: + blob = row['git_blob'] + require(row['local'] == 'inputs/' + blob + '.json.gz', 'noncanonical input path') + raw = gzip.decompress((package / row['local']).read_bytes()) + require(type(row['size']) is int and len(raw) == row['size'], 'upstream input size differs') + require(hashlib.sha256(raw).hexdigest() == row['sha256'], 'upstream SHA256 differs') + require(hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == blob, + 'upstream Git blob differs') + out[row['head'], row['path']] = json.loads(raw) + return out + + +def histogram(raw): + require(type(raw) is dict and bool(raw), 'empty histogram') + out = {} + for key, value in raw.items(): + require(type(key) is str and key.isdigit() and str(int(key)) == key, + 'noncanonical rank') + rank = int(key) + require(0 < rank < 73 and type(value) is int and value >= 0, + 'invalid histogram entry') + if value: + out[rank] = value + return out + + +def split(profile, idle, calls, live): + require(type(calls) is int and calls > 0 and calls % 9 == 0, + 'invalid complete call count') + require(type(live) is int and live > 0 and 9 * live == 896 * calls, + 'wrong live-family normalization') + p, i = histogram(profile), histogram(idle) + require(all(rank <= 51 and count <= p.get(rank, 0) for rank, count in i.items()), + 'idle profile is not a guard-admissible subprofile') + mass = sum(rank * count for rank, count in p.items()) + require(mass == 72 * live + 64 * calls, 'coverage mass differs') + local = {rank: Q(count - i.get(rank, 0), calls) + for rank, count in p.items() if count != i.get(rank, 0)} + idle_mass = Q(sum(rank * count for rank, count in i.items()), calls) + require(sum(rank * count for rank, count in local.items()) + idle_mass == 7232, + 'per-call mass does not reconcile') + return local, idle_mass + + +def at(obj, pointer): + require(type(pointer) is str and pointer.startswith('/'), 'invalid source JSON pointer') + for key in pointer[1:].split('/'): + obj = obj[key] + return obj + + +def source_counts(profile, idle): + """Bind N to original fields; explicitly distinguish four inferred W values.""" + call_evidence = [] + live_evidence = [] + for label, obj in (('profile', profile), ('idle', idle)): + for key in ('calls', 'complete_invocations'): + if key in obj: + n = obj[key] + require(type(n) is int and n > 0, 'invalid source calls') + call_evidence.append((label + '/' + key, n)) + if 'provider_counts' in obj: + counts = obj['provider_counts'] + require(type(counts) is dict and bool(counts) + and all(type(n) is int and n > 0 for n in counts.values()), + 'invalid provider counts') + call_evidence.append((label + '/provider_counts:sum', sum(counts.values()))) + for prefix, block in (('', obj), ('/expected', obj.get('expected', {}))): + if 'live' in block: + w = block['live'] + require(type(w) is int and w > 0, 'invalid source live stock') + live_evidence.append((label + prefix + '/live', w)) + require(call_evidence and len({v for _, v in call_evidence}) == 1, + 'missing or inconsistent source call counts') + n = call_evidence[0][1] + w = Q(896 * n, 9) + require(w.denominator == 1, 'source count is not complete replicas') + if live_evidence: + require(all(v == w for _, v in live_evidence), 'source live stock differs from template') + mode = 'direct source field and template agreement' + else: + mode = 'inferred from source N under the 896/9 template premise' + return n, int(w), dict(calls=call_evidence, live=live_evidence, live_mode=mode) + + +def reconstruct(claim, upstream): + p = upstream[claim['head'], claim['profile_file']] + i = upstream[claim['head'], claim['idle_file']] + profile = p['complex_profile'] + idle = {r: n for r, n in at(i, claim['idle_json_path']).items() if n} + same(profile, claim['profile'], 'source aggregate differs') + same(idle, claim['idle'], 'source idle histogram differs') + same(p['complex_lower'], claim['complex_lower'], 'source complex endpoint differs') + same(p['kappa'], claim['kappa'], 'source kappa differs') + require(Q(claim['title_kappa']) == Q(p['kappa']), 'title kappa differs') + calls, live, count_evidence = source_counts(p, i) + same(calls, claim['calls'], 'source call count differs') + same(live, claim['live'], 'source live count differs') + local, idle_mass = split(profile, idle, calls, live) + return local, idle_mass, count_evidence + + +def profile_json(local): + return {str(rank): str(count) for rank, count in sorted(local.items())} + + +def sign_record(local, a, expected): + interval = relaxation(local, a) + require(side(interval) == expected, 'claimed endpoint sign differs') + fine = relaxation(local, a, exponent_bits=128, precision=256) + require(side(fine) == expected, 'refined endpoint sign differs') + require(max(interval[0], fine[0]) <= min(interval[1], fine[1]), + 'enclosures are disjoint') + return {'a': str(a), 'moment_minus_one': [str(x - 1) for x in interval], + 'refined_moment_minus_one': [str(x - 1) for x in fine], 'sign': expected} + + +def audit(snapshot, census, upstream, assembly, selected): + claims = snapshot['claims'] + require(len(claims) == 14 and len({c['pr'] for c in claims}) == 14, 'wrong frozen claim domain') + require(len(census['words']) == 9 and len({w['id'] for w in census['words']}) == 9, + 'wrong frozen profile domain') + groups, claim_rows = {}, [] + for claim in claims: + local, idle_mass, evidence = reconstruct(claim, upstream) + key = canonical(profile_json(local)) + groups.setdefault(key, []).append(claim['pr']) + claim_rows.append({'pr': claim['pr'], 'head': claim['head'], + 'local': profile_json(local), 'idle_mass_per_call': str(idle_mass), + 'count_evidence': evidence}) + require(len(groups) == 9, 'reconstructed profile count differs') + observed = set() + records = [] + for word in census['words']: + key = canonical(word['local_profile_per_call']) + require(key in groups and key not in observed, 'unknown or repeated census profile') + observed.add(key) + same(sorted(groups[key]), word['claims'], 'profile membership differs') + local = {int(r): Q(n) for r, n in word['local_profile_per_call'].items()} + require(str(sum(r * n for r, n in local.items())) == word['local_mass_per_call'], + 'reported local mass differs') + hi = Q(word['a_ceiling']) + require((hi / GRID).denominator == 1 and GRID < hi < 1, 'off-grid ceiling') + lo = hi - GRID + cap = hi / (1 + hi) + for claim in claims: + if claim['pr'] in groups[key]: + require(Q(claim['complex_lower']) < lo and Q(claim['kappa']) < cap, + 'claim exceeds its relaxation bracket') + records.append({'id': word['id'], 'claims': word['claims'], + 'local': profile_json(local), + 'idle_mass_per_call': str(7232 - sum(r * n for r, n in local.items())), + 'lower': sign_record(local, lo, 'below'), + 'upper': sign_record(local, hi, 'above'), + 'kappa_cap_exact': str(cap)}) + same(assembly['complex_profile'], selected['owner']['profile'], 'selected profile differs') + n, w = selected['price']['calls'], selected['price']['live'] + local, idle_mass = split(assembly['complex_profile'], selected['owner']['idle'], n, w) + w2 = next(row for row in records if row['id'] == 'W2') + same(profile_json(local), w2['local'], 'selected profile is not W2') + require(idle_mass == 1646, 'selected idle mass differs') + same(assembly['complex_lower'], selected['price']['complex_lower'], 'selected endpoint differs') + require(Q(assembly['complex_lower']) < Q(w2['lower']['a']), 'selected endpoint above W2 bracket') + maximum = max(Q(r['kappa_cap_exact']) for r in records) + require(maximum < Q('0.001687314840'), 'published rounded global cap is too small') + return dict(status='PASS_INDEPENDENT_QUEUE_CEILINGS', claims=claim_rows, + profiles=records, endpoint_decisions=18, refinement_endpoint_decisions=18, + arithmetic={'exponent_bits': 96, 'fractional_bits': 192, + 'refined_exponent_bits': 128, 'refined_fractional_bits': 256}, + max_kappa_cap_exact=str(maximum), published_strict_cap='0.001687314840', + selected={'word': 'W2', 'calls': n, 'live': w, 'idle_mass_per_call': str(idle_mass)}, + scope='Frozen PR1264 extraction and coverage-law relaxation arithmetic only. ' + 'No realized circuit, owner, physical cost, supplier or full multiplication theorem check.') + + +def controls(snapshot, census, upstream): + out = [] + def rejects(name, action): + try: + action() + except ValueError: + out.append(name) + else: + raise ValueError('negative control accepted: ' + name) + + claim = snapshot['claims'][0] + local, _, _ = reconstruct(claim, upstream) + rejects('idle_rank_52', lambda: relaxation(local, Q(1, 1000), cap=52)) + rejects('negative_local_count', lambda: relaxation({1: -1}, Q(1, 1000))) + rejects('local_mass_over_budget', lambda: relaxation({1: 7233}, Q(1, 1000))) + rejects('inconclusive_is_not_rejection', lambda: side((Q(999, 1000), Q(1001, 1000)))) + rejects('wrong_live_normalization', lambda: split(claim['profile'], claim['idle'], + claim['calls'], 69120)) + bad_idle = deepcopy(claim['idle']); bad_idle['2'] = claim['profile']['2'] + 1 + rejects('idle_not_subprofile', lambda: split(claim['profile'], bad_idle, + claim['calls'], claim['live'])) + changed = deepcopy(claim); changed['calls'] *= 2; changed['live'] *= 2 + rejects('same_ratio_wrong_absolute_call_count', lambda: reconstruct(changed, upstream)) + changed2 = deepcopy(claim); changed2['profile']['1'] = True + rejects('boolean_in_aggregate', lambda: reconstruct(changed2, upstream)) + # Spread two rank-2 children into rank 1 and rank 3, preserving both child + # count and rank mass. Strict concavity lowers the moment for 0