From b9ac0d07eb9cdc31c4dca8dcc218943998edd3e8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 16 Oct 2026 17:04:43 +0100 Subject: [PATCH] test(research): certify linear high-route wrapper costs --- research/high-route-prefix-cost/README.md | 229 +++++ research/high-route-prefix-cost/RESULT.json | 804 ++++++++++++++++++ research/high-route-prefix-cost/SOURCES.json | 156 ++++ research/high-route-prefix-cost/TASK.json | 136 +++ research/high-route-prefix-cost/VERIFY.json | 56 ++ research/high-route-prefix-cost/invoice.py | 58 ++ research/high-route-prefix-cost/runtime.py | 418 +++++++++ .../high-route-prefix-cost/test_verify.py | 207 +++++ research/high-route-prefix-cost/verify.py | 112 +++ 9 files changed, 2176 insertions(+) create mode 100644 research/high-route-prefix-cost/README.md create mode 100644 research/high-route-prefix-cost/RESULT.json create mode 100644 research/high-route-prefix-cost/SOURCES.json create mode 100644 research/high-route-prefix-cost/TASK.json create mode 100644 research/high-route-prefix-cost/VERIFY.json create mode 100644 research/high-route-prefix-cost/invoice.py create mode 100644 research/high-route-prefix-cost/runtime.py create mode 100644 research/high-route-prefix-cost/test_verify.py create mode 100644 research/high-route-prefix-cost/verify.py diff --git a/research/high-route-prefix-cost/README.md b/research/high-route-prefix-cost/README.md new file mode 100644 index 0000000000..1d69cbf05f --- /dev/null +++ b/research/high-route-prefix-cost/README.md @@ -0,0 +1,229 @@ +# Exact linear wrapper bill for complete high routes + +The unchanged pooled `route_packet` wrapper adds at most **265 V physical +read/write/unit-move operations** to the complete cube routines it calls. +Consuming and clearing its returned output raises this to **277 V**. +Both constants are sharp over the stated canonical wrapper domain. +The [proof below](#exact-invoice-and-proof) gives an exact invoice, not an +extrapolation from measured ratios. + +This answers the prefix extraction, movement and disposal part of PR2968's +released complete-route handoff. It does **not** finish the uniform single-cube +bill, whole caller, bootstrap-stage reserve or supplier admission. There is no +new kappa and no selected-frontier change. + +## Contract and sources + +Let `C,H,F` be positive integers, encoded by canonical binary Count tapes with +no leading zero digits. The borrowed source contains `C` complete cubes, each +with `H` high records and `F` Boolean payload bits per record. Put `r=H*F` and +`V=C*r`. All borrowed heads start at the canonical origin. The actual selected +shape is `H=Q^(m*m)`, but the wrapper argument does not require that restriction. + +Use the retained `ScratchPool.install` and its factory, with initialized blank +roles and enough free inventory for successful execution. A cube call must +preserve its borrowed local source and context, return a distinct owned dense +`r`-bit output, and return both stream heads to their canonical origins. Let +`U_i` be the **entire actual cube-call traffic** for prefix `i`. This includes +its encoded setup, high-bank initialization/erasure, native B1 calls, scaling, +ADD/sign/carry work, intermediate disposal and returned output allocation. +No uniform bound on `U_i` is assumed by the exact identity. + +The scientific sources are Jose Manuel/jmbarrancoml's PR2915, author head +`fecc5a87574df441ddc3dad44f99fca9bd7fdd92`, and its frozen PR2899/PR2809/PR2753 +and PR2157 dependencies. This package consumes the exact modules and archives +retained on canonical main `47fa55b3cd8c7cf8879206f33569bc59d637dad8`. +[SOURCES.json](SOURCES.json) pins every declared external input. It neither edits +nor substitutes a frozen implementation. + +The wrapper is `routes.route_packet` in PR2899's nested PR2809/PR2753 export. +The reached replacement is `high_route.execute` through `stage.Adapter` and +`StagePool`. The proof also uses the retained `stream.Counter`, `copy_bits`, +`copy_rows`, `Tape.rewind/clear` and the pool's one blank read per acquisition. +PR2877's countdown identity and PR2951/PR2968's scaling/pool work are credited +predecessors, not new results here. + +The currency counts physical reads, writes and unit moves, including numerical +Word tapes and the native parking controller. It excludes host bookkeeping, +finite-control allocator selection, compilation and initial marker provisioning. +Thus 265 and 277 are **not complete machine-step constants**. The returned native +session is retained for reuse; its eventual enclosing-caller cleanup is separate. + +## Exact invoice and proof + +Write `b(n)=bit_length(n)` and `s(n)=popcount(n)`. PR2877's fully drained +canonical Counter bill, before its physical acquisition read, is + +```text +D(n) = 15*n + 14*b(n) - 5*s(n) + 36. +``` + +The retained `one_bit_suffix` probe costs `P(F)=4` for even F, `15` for +`F>1` congruent to one modulo four, and `12` otherwise. This follows by +following its early-return reads and rewinds on canonical binary digits. +A payload bit copy costs five operations. For F>1, `copy_bits` also pays +`D(F)+1` for its pooled countdown. Therefore the exact `copy_rows` invoice is + +```text +R(H,F) = D(H)+1 + H*(P(F)+5*F + [F>1]*(D(F)+1)). +``` + +Here and below each `+1` acquisition is the actual pool's blank-marker read, +not an assumed free constructor. The two calls to `copy_rows` per prefix pay +`2R`. The remaining per-prefix work outside the cube routine is: + +| Operation | Traffic | +| --- | ---: | +| Acquire the local stream | 1 | +| Rewind it after extraction | `2r+3` | +| Probe the consumed changed stream | 1 | +| Clear changed at its consumed head | `7r+7` | +| Clear the preserved local source at origin | `5r+7` | + +Their sum is `14r+19`. Across the whole packet, source and output final rewinds +add `4Cr+6`. Initial source rewind, final source-extent check, output acquisition +and outer Counter acquisition add six more. The complete outer countdown pays +`D(C)`, including its final disposal. Consequently + +```text +T_open = sum_i U_i + C*(2R(H,F)+18r+19) + D(C)+12, +T_closed = T_open + 5Cr+7. +``` + +The closed interval clears the returned owned output at its rewound head. It +does not dispose borrowed context or preprovisioned permanent inventories. +No cube or native call is multiplied by the prefix count a second time. + +### Uniform bound and sharpness + +Since `b(n)<=n` and `s(n)>=1`, + +```text +D(n)+1 <= 61n for n>=1, +D(n)+1 <= 45n for n>=2, +D(C)+12 <= 72C. +``` + +The second bound follows from `D(n)+1<=29n+32`. Thus: + +- For F=1, `R<=78r`. +- For F=2, the exact `P(2)=4` and `D(2)+1=90` give `R<=165r/2`. +- For F>=3, `R<=(50+76/F)r<=226r/3`. + +The open wrapper bill per prefix is at most `2R+18r+91`. For F=1 this is +at most `174r+91<=265r`. For F=2 use `r>=2`, giving at most `457r/2`. +For F>=3 use `r>=3`, giving at most `199r`. Hence + +```text +T_open <= sum_i U_i + 265V, +T_closed <= sum_i U_i + 277V. +``` + +At `C=H=F=1`, the exact wrapper invoices are 265 and 277, respectively. +An actual Q=1 reduced route attains both in the controls. Sharpness concerns +this wrapper/currency/domain, not a minimum implementation cost or a selected +stopped caller's attainable parameters. + +If every cube has a proved tariff `U_i<=G*r`, the full packet therefore costs +at most `(G+265)V`, or `(G+277)V` with output disposal. Unknown single-cube +charges have not become zero. For equal complete cube traces, the exact useful +cross-check is `T(C)=C*(T(1)-D(1)-12)+D(C)+12`. Equal traces are checked in the +finite fixtures, not assumed for an arbitrary substitute cube routine. + +## Replay and measured evidence + +From the repository root, with standard-library CPython 3.12 or newer: + +```sh +python3.12 -Werror -B scripts/research_package.py --package research/high-route-prefix-cost +``` + +The primary command authenticates inputs before loading complete source modules. +It replays 44 complete reduced routes, 125,689 payload bits and 1,314 actual +native B1 calls, with direct q-adic affine-matrix endpoint checks. Cases include +Q=1,3,5,9, forward/inverse noncommuting words, suffixes 1/3, prefix counts through +17, and complementary payloads. Native calls take the **elementary** B1 branch; +no fitted selected GL64 payload execution is claimed. + +The observer counts raw physical Tape methods once, and adds the native +controller's non-Tape operations. Each complete interval must also agree with +the sum of unique physical-object meters. Word/Lease alias meters are not added +again. Native and cube interval snapshots are entry-relative, excluding earlier +initialization. The observer attaches to the stable adapter method because +`StagePool` reinstalls the route alias after every native return. The checker +requires exactly C observed cube intervals, not merely C reported outputs. + +For q=3, w=2, F=1, the complete one-prefix route costs **438,000** operations. +Its cube costs 431,027, including 154,884 inside six actual native calls. The +wrapper costs exactly **6,973**. Three prefixes cost 1,313,895, or 1,315,117 +including output disposal. Full typed records are in [RESULT.json](RESULT.json). + +The controls independently exercise 256 pooled countdowns and 121 complete +`copy_rows` calls. They check the sharp bounds on 32,768 triples and the actual +attaining route. An endpoint-preserving mutant adds C redundant reads outside +each cube call. At C=3 it adds nine operations, which the invoice rejects. +A noncanonical extra zero in the prefix count preserves the endpoint but adds +14 operations, demonstrating why the canonical-input premise matters. Semantic, +source, missing-declaration and typed-receipt corruptions also reject. + +The registered normal/optimized CPython 3.12.15 replay passed locally on Linux +x86_64, as did the 13 optimized control groups on CPython 3.13.5. The repository +workflow suite passed 158 tests with 11 platform skips. Ruff checks and formatting +passed. These are local results, not hosted CI evidence. + +These are finite corroborations of the written wrapper proof. The endpoint +patterns are not a new independent-column census. Complete cold supplier replay, +formal-kernel verification, independent human review and hosted CI are separate. + +## Implementation bounds + +The new harness has no recursion. Fixture prefixes are at most 17, widths at +most three, and total payload at most 100,000 bits. Source inventories have at +most 64 rows, at most 32 MiB per file and at most 64 MiB total. The managed +Python runtime allocates within those fixture limits; it is not the proposed +fixed-tape multiplication machine. Existing source inventories and routines are +left unchanged. All new functions fit within 60 physical lines. + +Dynamic loading and temporary method replacement are confined to the five +explicitly authenticated source modules and finite observer targets. They are +needed to run the exact frozen implementation and observe physical operations, +not to alter its arithmetic or loops. Context managers restore methods, successful +outputs and fixture resources are explicitly released, and both source loaders' +temporary exports are explicitly cleaned. General source failure recovery remains +outside the inherited successful-execution contract. + +The registered replay enables Python warnings as errors. Local diagnostics use +`ruff check --select E,F,I,UP,B,SIM` and `ruff format --check`. A whole-repository +static typing migration is not part of this dynamic-source audit. + +## Open next questions + +1. Prove a uniform **single-cube** invoice for the reached source. Start with + encoded extent/high-bank setup and ordered high-field ADD, then compose the + already audited sign/scaling and complete B1 tariff. This matters because + the wrapper theorem only lifts those costs. The all-width native and source + contracts remain dependencies. +2. Compose a complete machine-step and storage ledger. Start with fixed pool + selection, marker provisioning and native inventory reuse at common cuts. + The exact I/O bill does not price finite-control transitions or establish a + whole-stage reserve coefficient. + +The decision is to finish this independent wrapper audit, not expand the +construction family. [TASK.json](TASK.json) records the changed task scope, +coordination and upstream freshness. + +## Credit + +Jose Manuel/jmbarrancoml supplied PR2915's route/adapter implementation and +PR2899/PR2809 physical compositions. David Arias supplied PR2753's logical +caller. Arham Tahir supplied PR2877's shared countdown identity. PR2951/PR2968 +supply the earlier scaling and pool invoices. The PR2157 factor words and +DreamingOfClouds' selected PR589 work on eumemic's base retain their source +attribution. PR2708's `selected-route-live-volume` proves a separate storage +bound for the older decorated-key cube, not this I/O tariff. No predecessor +implementation, storage bound or countdown identity is claimed as new. This +package adds the exact wrapper invoice, sharp linear constants +and independent complete-route cost partition. + +Nick Petalas. Apache-2.0. Substantial automated assistance; no independent +human review is claimed. diff --git a/research/high-route-prefix-cost/RESULT.json b/research/high-route-prefix-cost/RESULT.json new file mode 100644 index 0000000000..2f7e256a25 --- /dev/null +++ b/research/high-route-prefix-cost/RESULT.json @@ -0,0 +1,804 @@ +{ + "bits": 125689, + "cases": 44, + "groups": [ + { + "complementary": { + "cube_bits": 3, + "cube_traffic": 1029, + "disposed_traffic": 2539, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 1, + "pool_peak": 7, + "prefixes": 3, + "q": 3, + "traffic": 2487, + "width": 1, + "wrapper_traffic": 1458 + }, + "parameters": { + "fibre_value": 3, + "q": 3, + "width": 1 + }, + "rows": [ + { + "cube_bits": 3, + "cube_traffic": 343, + "disposed_traffic": 886, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 1, + "q": 3, + "traffic": 864, + "width": 1, + "wrapper_traffic": 521 + }, + { + "cube_bits": 3, + "cube_traffic": 686, + "disposed_traffic": 1722, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 2, + "q": 3, + "traffic": 1685, + "width": 1, + "wrapper_traffic": 999 + }, + { + "cube_bits": 3, + "cube_traffic": 1029, + "disposed_traffic": 2539, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 3, + "q": 3, + "traffic": 2487, + "width": 1, + "wrapper_traffic": 1458 + }, + { + "cube_bits": 3, + "cube_traffic": 1372, + "disposed_traffic": 3380, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 4, + "q": 3, + "traffic": 3313, + "width": 1, + "wrapper_traffic": 1941 + }, + { + "cube_bits": 3, + "cube_traffic": 2401, + "disposed_traffic": 5836, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 7, + "q": 3, + "traffic": 5724, + "width": 1, + "wrapper_traffic": 3323 + }, + { + "cube_bits": 3, + "cube_traffic": 2744, + "disposed_traffic": 6682, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 8, + "q": 3, + "traffic": 6555, + "width": 1, + "wrapper_traffic": 3811 + }, + { + "cube_bits": 3, + "cube_traffic": 3087, + "disposed_traffic": 7499, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 9, + "q": 3, + "traffic": 7357, + "width": 1, + "wrapper_traffic": 4270 + }, + { + "cube_bits": 3, + "cube_traffic": 5488, + "disposed_traffic": 13272, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 16, + "q": 3, + "traffic": 13025, + "width": 1, + "wrapper_traffic": 7537 + }, + { + "cube_bits": 3, + "cube_traffic": 5831, + "disposed_traffic": 14089, + "fibre": 3, + "inverse": false, + "native_calls": 0, + "native_trace_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + "native_traffic": 0, + "pattern": 0, + "pool_peak": 7, + "prefixes": 17, + "q": 3, + "traffic": 13827, + "width": 1, + "wrapper_traffic": 7996 + } + ] + }, + { + "complementary": { + "cube_bits": 81, + "cube_traffic": 1293081, + "disposed_traffic": 1315117, + "fibre": 1, + "inverse": false, + "native_calls": 18, + "native_trace_sha256": "63f3bdb39069eef6a20496d62e3586c786b9218cc104e4141028e35bcc58e864", + "native_traffic": 464652, + "pattern": 1, + "pool_peak": 20, + "prefixes": 3, + "q": 3, + "traffic": 1313895, + "width": 2, + "wrapper_traffic": 20814 + }, + "parameters": { + "fibre_value": 1, + "q": 3, + "width": 2 + }, + "rows": [ + { + "cube_bits": 81, + "cube_traffic": 431027, + "disposed_traffic": 438412, + "fibre": 1, + "inverse": false, + "native_calls": 6, + "native_trace_sha256": "ede1867e82c0100ac40c18d370470301bca2cd3d8907ad6b046d971eeeefcc01", + "native_traffic": 154884, + "pattern": 0, + "pool_peak": 20, + "prefixes": 1, + "q": 3, + "traffic": 438000, + "width": 2, + "wrapper_traffic": 6973 + }, + { + "cube_bits": 81, + "cube_traffic": 862054, + "disposed_traffic": 876774, + "fibre": 1, + "inverse": false, + "native_calls": 12, + "native_trace_sha256": "2c94294f7eca32d4518dcfc005b43b67082893104dedbb430662366e2fdd8c67", + "native_traffic": 309768, + "pattern": 0, + "pool_peak": 20, + "prefixes": 2, + "q": 3, + "traffic": 875957, + "width": 2, + "wrapper_traffic": 13903 + }, + { + "cube_bits": 81, + "cube_traffic": 1293081, + "disposed_traffic": 1315117, + "fibre": 1, + "inverse": false, + "native_calls": 18, + "native_trace_sha256": "63f3bdb39069eef6a20496d62e3586c786b9218cc104e4141028e35bcc58e864", + "native_traffic": 464652, + "pattern": 0, + "pool_peak": 20, + "prefixes": 3, + "q": 3, + "traffic": 1313895, + "width": 2, + "wrapper_traffic": 20814 + }, + { + "cube_bits": 81, + "cube_traffic": 1724108, + "disposed_traffic": 1753484, + "fibre": 1, + "inverse": false, + "native_calls": 24, + "native_trace_sha256": "37461b839625afe1ae9bc59d3ed6d564d660ed3195d3d276cabb354704af7d74", + "native_traffic": 619536, + "pattern": 0, + "pool_peak": 20, + "prefixes": 4, + "q": 3, + "traffic": 1751857, + "width": 2, + "wrapper_traffic": 27749 + }, + { + "cube_bits": 81, + "cube_traffic": 3017189, + "disposed_traffic": 3068518, + "fibre": 1, + "inverse": false, + "native_calls": 42, + "native_trace_sha256": "650ce468e50f9706026c806bce4aa0a76b10f254541e2996d88ab75afe9f6530", + "native_traffic": 1084188, + "pattern": 0, + "pool_peak": 20, + "prefixes": 7, + "q": 3, + "traffic": 3065676, + "width": 2, + "wrapper_traffic": 48487 + }, + { + "cube_bits": 81, + "cube_traffic": 3448216, + "disposed_traffic": 3506890, + "fibre": 1, + "inverse": false, + "native_calls": 48, + "native_trace_sha256": "1c20526b527286352ff68870e2cad03953c38adc5766ea02ad67468d4146ea1b", + "native_traffic": 1239072, + "pattern": 0, + "pool_peak": 20, + "prefixes": 8, + "q": 3, + "traffic": 3503643, + "width": 2, + "wrapper_traffic": 55427 + }, + { + "cube_bits": 81, + "cube_traffic": 3879243, + "disposed_traffic": 3945233, + "fibre": 1, + "inverse": false, + "native_calls": 54, + "native_trace_sha256": "39ac9bb147a5d6ddf037a70b34aaa5fb4a41cca3193b42e03c8db4b9facc89b7", + "native_traffic": 1393956, + "pattern": 0, + "pool_peak": 20, + "prefixes": 9, + "q": 3, + "traffic": 3941581, + "width": 2, + "wrapper_traffic": 62338 + }, + { + "cube_bits": 81, + "cube_traffic": 6896432, + "disposed_traffic": 7013688, + "fibre": 1, + "inverse": false, + "native_calls": 96, + "native_trace_sha256": "88784bf1e282e5b066111b81f3fb71c6552f119bdab6d0c7a1ec4b91194f4d52", + "native_traffic": 2478144, + "pattern": 0, + "pool_peak": 20, + "prefixes": 16, + "q": 3, + "traffic": 7007201, + "width": 2, + "wrapper_traffic": 110769 + }, + { + "cube_bits": 81, + "cube_traffic": 7327459, + "disposed_traffic": 7452031, + "fibre": 1, + "inverse": false, + "native_calls": 102, + "native_trace_sha256": "8c03f461a5e1828df7fc5d4812d52f7d60e2e4ec5223456e63a215ab25e77014", + "native_traffic": 2633028, + "pattern": 0, + "pool_peak": 20, + "prefixes": 17, + "q": 3, + "traffic": 7445139, + "width": 2, + "wrapper_traffic": 117680 + } + ] + }, + { + "complementary": { + "cube_bits": 243, + "cube_traffic": 2128686, + "disposed_traffic": 2215360, + "fibre": 3, + "inverse": true, + "native_calls": 18, + "native_trace_sha256": "47e897f9d8d8ef5ee18cbfeed8128e891afe34c6984499e25afad3cd284c22ac", + "native_traffic": 754326, + "pattern": 1, + "pool_peak": 20, + "prefixes": 3, + "q": 3, + "traffic": 2211708, + "width": 2, + "wrapper_traffic": 83022 + }, + "parameters": { + "fibre_value": 3, + "inverse": true, + "q": 3, + "width": 2 + }, + "rows": [ + { + "cube_bits": 243, + "cube_traffic": 709562, + "disposed_traffic": 738493, + "fibre": 3, + "inverse": true, + "native_calls": 6, + "native_trace_sha256": "a2df50dff441fd4e97906ae941e9af39d526035684e0459b92e46a9c248a9fed", + "native_traffic": 251442, + "pattern": 0, + "pool_peak": 20, + "prefixes": 1, + "q": 3, + "traffic": 737271, + "width": 2, + "wrapper_traffic": 27709 + }, + { + "cube_bits": 243, + "cube_traffic": 1419124, + "disposed_traffic": 1476936, + "fibre": 3, + "inverse": true, + "native_calls": 12, + "native_trace_sha256": "52557aa068cdcf89d2d7bdba9b0be8e84faeb96c34fa3752f2b0e7c8c85bea0a", + "native_traffic": 502884, + "pattern": 0, + "pool_peak": 20, + "prefixes": 2, + "q": 3, + "traffic": 1474499, + "width": 2, + "wrapper_traffic": 55375 + }, + { + "cube_bits": 243, + "cube_traffic": 2128686, + "disposed_traffic": 2215360, + "fibre": 3, + "inverse": true, + "native_calls": 18, + "native_trace_sha256": "47e897f9d8d8ef5ee18cbfeed8128e891afe34c6984499e25afad3cd284c22ac", + "native_traffic": 754326, + "pattern": 0, + "pool_peak": 20, + "prefixes": 3, + "q": 3, + "traffic": 2211708, + "width": 2, + "wrapper_traffic": 83022 + }, + { + "cube_bits": 243, + "cube_traffic": 2838248, + "disposed_traffic": 2953808, + "fibre": 3, + "inverse": true, + "native_calls": 24, + "native_trace_sha256": "7400e0aeac297b5c4d2279fbdbcb00e759682de28c584fc0cdc5252d4e7bc5ce", + "native_traffic": 1005768, + "pattern": 0, + "pool_peak": 20, + "prefixes": 4, + "q": 3, + "traffic": 2948941, + "width": 2, + "wrapper_traffic": 110693 + }, + { + "cube_bits": 243, + "cube_traffic": 4966934, + "disposed_traffic": 5169085, + "fibre": 3, + "inverse": true, + "native_calls": 42, + "native_trace_sha256": "bc4ad1c1bdf9bfd3bf42bbf8a41506852f2590175d2c2833f009edc8e286dcc9", + "native_traffic": 1760094, + "pattern": 0, + "pool_peak": 20, + "prefixes": 7, + "q": 3, + "traffic": 5160573, + "width": 2, + "wrapper_traffic": 193639 + }, + { + "cube_bits": 243, + "cube_traffic": 5676496, + "disposed_traffic": 5907538, + "fibre": 3, + "inverse": true, + "native_calls": 48, + "native_trace_sha256": "7afe8897b011683019f70a76ac733d130d28ddc0949f3a88b5e06ac13a5fd556", + "native_traffic": 2011536, + "pattern": 0, + "pool_peak": 20, + "prefixes": 8, + "q": 3, + "traffic": 5897811, + "width": 2, + "wrapper_traffic": 221315 + }, + { + "cube_bits": 243, + "cube_traffic": 6386058, + "disposed_traffic": 6645962, + "fibre": 3, + "inverse": true, + "native_calls": 54, + "native_trace_sha256": "e30d73838521b0a320d1692c6932e2d0368e8b82e2c4ba5ffe0ee0d7d88eca0d", + "native_traffic": 2262978, + "pattern": 0, + "pool_peak": 20, + "prefixes": 9, + "q": 3, + "traffic": 6635020, + "width": 2, + "wrapper_traffic": 248962 + }, + { + "cube_bits": 243, + "cube_traffic": 11352992, + "disposed_traffic": 11814984, + "fibre": 3, + "inverse": true, + "native_calls": 96, + "native_trace_sha256": "c6a1fbce22a38450d5e2ebf0baa09dd5c2d2e2490707f88fafd1c97681d44c46", + "native_traffic": 4023072, + "pattern": 0, + "pool_peak": 20, + "prefixes": 16, + "q": 3, + "traffic": 11795537, + "width": 2, + "wrapper_traffic": 442545 + }, + { + "cube_bits": 243, + "cube_traffic": 12062554, + "disposed_traffic": 12553408, + "fibre": 3, + "inverse": true, + "native_calls": 102, + "native_trace_sha256": "59408cd453fd68dc6ee1f3d38ca4bb0ba90a982da75c33585595fda67df58e0c", + "native_traffic": 4274514, + "pattern": 0, + "pool_peak": 20, + "prefixes": 17, + "q": 3, + "traffic": 12532746, + "width": 2, + "wrapper_traffic": 470192 + } + ] + }, + { + "complementary": { + "cube_bits": 625, + "cube_traffic": 6062745, + "disposed_traffic": 6226957, + "fibre": 1, + "inverse": true, + "native_calls": 18, + "native_trace_sha256": "dada88ae8f18582c38579f1d3ffcfa5c660c49236368579f92a0bc464259200d", + "native_traffic": 1244808, + "pattern": 1, + "pool_peak": 20, + "prefixes": 3, + "q": 5, + "traffic": 6217575, + "width": 2, + "wrapper_traffic": 154830 + }, + "parameters": { + "fibre_value": 1, + "inverse": true, + "q": 5, + "width": 2 + }, + "rows": [ + { + "cube_bits": 625, + "cube_traffic": 2020915, + "disposed_traffic": 2075692, + "fibre": 1, + "inverse": true, + "native_calls": 6, + "native_trace_sha256": "a45cd5ff45661cea9503a097a5e36dd878683a01a29bc6bd28bb3ea88a816e23", + "native_traffic": 414936, + "pattern": 0, + "pool_peak": 20, + "prefixes": 1, + "q": 5, + "traffic": 2072560, + "width": 2, + "wrapper_traffic": 51645 + }, + { + "cube_bits": 625, + "cube_traffic": 4041830, + "disposed_traffic": 4151334, + "fibre": 1, + "inverse": true, + "native_calls": 12, + "native_trace_sha256": "cbd30a2a73be3f88e78d882ca8a5919017f4865656e9d8739ecf02f760781326", + "native_traffic": 829872, + "pattern": 0, + "pool_peak": 20, + "prefixes": 2, + "q": 5, + "traffic": 4145077, + "width": 2, + "wrapper_traffic": 103247 + }, + { + "cube_bits": 625, + "cube_traffic": 6062745, + "disposed_traffic": 6226957, + "fibre": 1, + "inverse": true, + "native_calls": 18, + "native_trace_sha256": "dada88ae8f18582c38579f1d3ffcfa5c660c49236368579f92a0bc464259200d", + "native_traffic": 1244808, + "pattern": 0, + "pool_peak": 20, + "prefixes": 3, + "q": 5, + "traffic": 6217575, + "width": 2, + "wrapper_traffic": 154830 + }, + { + "cube_bits": 625, + "cube_traffic": 8083660, + "disposed_traffic": 8302604, + "fibre": 1, + "inverse": true, + "native_calls": 24, + "native_trace_sha256": "607a409b6737b59e347f8c78058ccee930d62b6e4f28554585eca7f98f5cf9dd", + "native_traffic": 1659744, + "pattern": 0, + "pool_peak": 20, + "prefixes": 4, + "q": 5, + "traffic": 8290097, + "width": 2, + "wrapper_traffic": 206437 + }, + { + "cube_bits": 625, + "cube_traffic": 14146405, + "disposed_traffic": 14529478, + "fibre": 1, + "inverse": true, + "native_calls": 42, + "native_trace_sha256": "7f0940e4c205bcdc4219e9f709f640c3ffb3e9727ec6e07b216891e26d99927d", + "native_traffic": 2904552, + "pattern": 0, + "pool_peak": 20, + "prefixes": 7, + "q": 5, + "traffic": 14507596, + "width": 2, + "wrapper_traffic": 361191 + }, + { + "cube_bits": 625, + "cube_traffic": 16167320, + "disposed_traffic": 16605130, + "fibre": 1, + "inverse": true, + "native_calls": 48, + "native_trace_sha256": "c904f1e9bd281fb9ff43e339fd2793f124175bc718e478db1993da38ae1a5d73", + "native_traffic": 3319488, + "pattern": 0, + "pool_peak": 20, + "prefixes": 8, + "q": 5, + "traffic": 16580123, + "width": 2, + "wrapper_traffic": 412803 + }, + { + "cube_bits": 625, + "cube_traffic": 18188235, + "disposed_traffic": 18680753, + "fibre": 1, + "inverse": true, + "native_calls": 54, + "native_trace_sha256": "02a8e8b316097acb58f0c99cc0800367e58c9f93a0f0bc7b906b427a99c4486f", + "native_traffic": 3734424, + "pattern": 0, + "pool_peak": 20, + "prefixes": 9, + "q": 5, + "traffic": 18652621, + "width": 2, + "wrapper_traffic": 464386 + }, + { + "cube_bits": 625, + "cube_traffic": 32334640, + "disposed_traffic": 33210168, + "fibre": 1, + "inverse": true, + "native_calls": 96, + "native_trace_sha256": "c114de2e562f14fb5d3baeb356386a1434abdcc0db89b8e93737b959f33f8a66", + "native_traffic": 6638976, + "pattern": 0, + "pool_peak": 20, + "prefixes": 16, + "q": 5, + "traffic": 33160161, + "width": 2, + "wrapper_traffic": 825521 + }, + { + "cube_bits": 625, + "cube_traffic": 34355555, + "disposed_traffic": 35285791, + "fibre": 1, + "inverse": true, + "native_calls": 102, + "native_trace_sha256": "8163bfcf4b862b18e4a6dda846e6ef548d10e6bf5529472a79fcd0d500dc9dbf", + "native_traffic": 7053912, + "pattern": 0, + "pool_peak": 20, + "prefixes": 17, + "q": 5, + "traffic": 35232659, + "width": 2, + "wrapper_traffic": 877104 + } + ] + }, + { + "complementary": { + "cube_bits": 6561, + "cube_traffic": 68213304, + "disposed_traffic": 69927034, + "fibre": 1, + "inverse": false, + "native_calls": 18, + "native_trace_sha256": "a05331b2ceae1ed6166583d337471c50425945c9c612f20b5048155734db39ff", + "native_traffic": 19509282, + "pattern": 1, + "pool_peak": 20, + "prefixes": 3, + "q": 3, + "traffic": 69828612, + "width": 3, + "wrapper_traffic": 1615308 + }, + "parameters": { + "fibre_value": 1, + "q": 3, + "width": 3 + }, + "rows": [ + { + "cube_bits": 6561, + "cube_traffic": 22737768, + "disposed_traffic": 23309051, + "fibre": 1, + "inverse": false, + "native_calls": 6, + "native_trace_sha256": "8af16654abd901d4e9602c0b9e25fc216bcdfbd215f5936276be2117b4c44e8f", + "native_traffic": 6503094, + "pattern": 0, + "pool_peak": 20, + "prefixes": 1, + "q": 3, + "traffic": 23276239, + "width": 3, + "wrapper_traffic": 538471 + }, + { + "cube_bits": 6561, + "cube_traffic": 45475536, + "disposed_traffic": 46618052, + "fibre": 1, + "inverse": false, + "native_calls": 12, + "native_trace_sha256": "76eb4c96d43ba7024cb6248fe1abaec47d00d5c6e8254365834ec35bebc50669", + "native_traffic": 13006188, + "pattern": 0, + "pool_peak": 20, + "prefixes": 2, + "q": 3, + "traffic": 46552435, + "width": 3, + "wrapper_traffic": 1076899 + }, + { + "cube_bits": 6561, + "cube_traffic": 68213304, + "disposed_traffic": 69927034, + "fibre": 1, + "inverse": false, + "native_calls": 18, + "native_trace_sha256": "a05331b2ceae1ed6166583d337471c50425945c9c612f20b5048155734db39ff", + "native_traffic": 19509282, + "pattern": 0, + "pool_peak": 20, + "prefixes": 3, + "q": 3, + "traffic": 69828612, + "width": 3, + "wrapper_traffic": 1615308 + } + ] + } + ], + "native_calls": 1314, + "rows_sha256": "89d69b837dbefd20874ab0090bfacf2e14db58ae8e33b81e1ee9e90365691e05", + "status": "PASS_HIGH_ROUTE_PREFIX_COST" +} diff --git a/research/high-route-prefix-cost/SOURCES.json b/research/high-route-prefix-cost/SOURCES.json new file mode 100644 index 0000000000..1388300537 --- /dev/null +++ b/research/high-route-prefix-cost/SOURCES.json @@ -0,0 +1,156 @@ +{ + "schema_version": 1, + "base_commit": "47fa55b3cd8c7cf8879206f33569bc59d637dad8", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/bit2234-stock-threshold/README.md", + "usage": "input", + "git_blob": "ede0d322c477af91d4c2cc33db0fd10958f45eab", + "sha256": "1e050c9f963421d751d9208092f9a15321ed77810e03912df8eb5eb56bbb06e7" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL-TEMPLATE.json.gz", + "usage": "input", + "git_blob": "9eafb8776cbf78c72124f833534469ddfa5e98ec", + "sha256": "0357b7cfbd7c29b4983982baf153c8a9f1e1e412690cd7fa9fc3d23d7963b20f" + }, + { + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL.json", + "usage": "input", + "git_blob": "1f648db9e63e7bfcaa6d5b1dd9fa6503caac47d2", + "sha256": "8de008a7978d4b7189cbec2470443619149a2b7b2f0f862540eeee4b23d3a819" + }, + { + "path": "research/community-hyperplane599-audit/pr589/bit589/v9/nine/GEOMETRY.json", + "usage": "input", + "git_blob": "44006542202ca6037533a754f0bcd00549d7e088", + "sha256": "0058c491d839142aa99ef86a5ec697ce99857632228531512ea3fa74fb24d734" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/high-scaling-scratch-traffic/PROOF.md", + "usage": "input", + "git_blob": "b564145c83e1d01ea7c6383453bf6eec13ee3ed9", + "sha256": "528fe54729c7d4711d6566d177a778dccd8e9f0f9724654519223bb13f85c69f" + }, + { + "path": "research/high-scaling-total-traffic/traffic.py", + "usage": "input", + "git_blob": "586e46091367fad031ce46270bcbfbc63dbddd2a", + "sha256": "df1c63bb5343998bf9e3109a3c54b34b6d961a3222b52a427649886d5020ae40" + }, + { + "path": "research/idle-axis-hosting/PROOF.md", + "usage": "input", + "git_blob": "4468a00349b4f68dce103e785a8392099435e1d6", + "sha256": "cfe34bf0b64259661312dae22c3a23adc5bf6f6326951eee5c1488ccfc347542" + }, + { + "path": "research/pr589-five-helper-hosting/PROOF.md", + "usage": "input", + "git_blob": "bbd3f12b9a32b3ad3cba85a2d5a1b3054214fa02", + "sha256": "59cae781bfbe1a01ed9e66a8efeeb5a2b995e5ecdf908586b23ecc39f2b8d647" + }, + { + "path": "research/pr589-five-helper-hosting/verify.py", + "usage": "input", + "git_blob": "dbc71f56bb4205ebe378ada1f9f4ea88630d1d39", + "sha256": "cf90e19ae9991b0698be03d395a8cc29061ecb307eb7fea19adfb2d23c25a367" + }, + { + "path": "research/recursive-parking-boundary/README.md", + "usage": "input", + "git_blob": "251f335ebaccc11d69393ee7aeb5a2e84526d0bb", + "sha256": "491aa208391ee4c2936510b1a5c5c018dd5509d9a0e88687c72ab8406cd77b18" + }, + { + "path": "research/selected-bit-fast-primitives/compile_routes.py", + "usage": "input", + "git_blob": "37263fdc327b4a300ccfaa0b7ad650012ab3d59c", + "sha256": "1bfef464dfb3e33d9d57f53b657b2d1fe3598bc453be49000a5e782b622e8585" + }, + { + "path": "research/selected-bit-fast-primitives/high_route.py", + "usage": "input", + "git_blob": "ec7481f890147be7763f4da729fd879a88a87e8e", + "sha256": "13d9c706e7bad2fa3b7d2a97d19b58f2c4efac06d2bb76b613b40069c38b1cd2" + }, + { + "path": "research/selected-bit-fast-primitives/inputs/pr2157.tar", + "usage": "input", + "git_blob": "9504807466071f56519f8663ccb532076a42a273", + "sha256": "db202c7b91b5b8b9340f96f870d54e275854f0b73839451c7c15bd7895ac3639" + }, + { + "path": "research/selected-bit-fast-primitives/inputs/pr2899.tar", + "usage": "input", + "git_blob": "e85ce82745879141e416ac6d9e3551ff959871aa", + "sha256": "fc4a2e07423835737c8fb3872664b16ff12aa4cf83b1e26e49878debef40c531" + }, + { + "path": "research/selected-bit-fast-primitives/kernels.py", + "usage": "input", + "git_blob": "de9fb08c35e92c8354ae622276866385fd07e3d2", + "sha256": "c4b91333817f7fcea44b1d32e01095cd71aeb673ed3608d2e25f4c06d56bb420" + }, + { + "path": "research/selected-bit-fast-primitives/stage.py", + "usage": "input", + "git_blob": "765ae9e11af3acb9458d7a1444a9e79112b72d96", + "sha256": "44e334162d12868ce6bb50c501cd2eba8c527f59ce7a144614edd8cd6f533647" + }, + { + "path": "research/selected-bit-fast-primitives/stage_sources.py", + "usage": "input", + "git_blob": "27383dd1553672f9c82139f80b628b2a094628d8", + "sha256": "55c6631cce4f76e14b66b6195468c36b544e2374cc6c59702135c664bff10822" + }, + { + "path": "research/selected-bit-local-ring-sweeps/PROOF.md", + "usage": "input", + "git_blob": "4330de85dd9862ed15d84ab917887d249753df99", + "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7" + }, + { + "path": "research/selected-bit-recursive-closure/PROOF.md", + "usage": "input", + "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531", + "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344" + }, + { + "path": "upstream/build/sections/02-streams.tex", + "usage": "input", + "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", + "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab" + } + ] +} diff --git a/research/high-route-prefix-cost/TASK.json b/research/high-route-prefix-cost/TASK.json new file mode 100644 index 0000000000..f1bd709446 --- /dev/null +++ b/research/high-route-prefix-cost/TASK.json @@ -0,0 +1,136 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 5, + "base_commit": "47fa55b3cd8c7cf8879206f33569bc59d637dad8", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact physical-I/O invoice and sharp 265V/277V overhead bound for the canonical pooled PR2915 route_packet wrapper, corroborated by complete reduced high routes with actual B1 intervals.", + "scope_change_reason": "The selected-stage cutoff followups are already covered. Take PR2968's released local H2 route-cost handoff, narrowing the result to prefix extraction, movement, disposal and single-cube lifting instead of a whole-stage stock coefficient. The all-width single-cube tariff remains open.", + "bottleneck_link": "A current H2 cost implication needs complete routing charges. This proves the actual old-prefix wrapper does not introduce an extra prefix/width factor, conditional on its explicit cube contract. It does not admit a stock envelope or change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the source-bound wrapper proof, exact physical metering, semantic and cost controls, publication check and focused PR. Do not expand the source construction or infer a uniform cube tariff from finite ratios.", + "outcome": "partial", + "evidence": "README.md contains the exact all-parameter canonical-wrapper proof. RESULT.json records 44 complete routes, 125689 bits and 1314 actual elementary-branch B1 calls. Registered verification includes independent raw-meter agreement, affine endpoint checks and 13 behavioral controls.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance; no independent human review is claimed.", + "open_questions": [ + { + "question": "What complete uniform single-cube tariff does the reached PR2915 route provide?", + "why_it_matters": "The exact wrapper theorem lifts that tariff but does not prove its width dependence.", + "first_step": "Price encoded extent/high-bank setup and ordered high-field ADD, then compose proved sign/scaling and the actual complete B1 tariff.", + "blocked_by": "All-width native/source contracts and unresolved remaining cube charges." + }, + { + "question": "How do physical I/O, fixed-role allocator and marker provisioning compose into a complete machine-step and storage ledger?", + "why_it_matters": "265 and 277 count raw I/O, not every finite-control step or complete caller reserve.", + "first_step": "Bind fixed inventory selection, marker initialization and native reuse at common cuts, keeping already charged I/O separate.", + "blocked_by": "Physical placement and full caller/storage/refinement dependencies remain open." + } + ], + "assignment_nonce": "6288a44eb853813accd6eb84031982f0", + "track": "adversarial-audit", + "catalogue_scope_key": "f5c32b23bcd01d2e356d", + "refined_scope_key": "pr2915-pooled-route-packet-complete-physical-io-wrapper", + "declared_milestone": "Independent scoped cost audit, not complete supplier or whole-stage reserve", + "complete_cost_boundary": { + "proved": "T_open=sum(U_i)+W(C,H,F), W<=265V; output disposal gives W_closed<=277V. All native intervals stay inside U_i.", + "constructive": "Finite complete source runs with existing actual pool, high bank and B1 elementary branch.", + "unknown": "Uniform all-width cube tariff, full machine-step/allocator/marker cost, fitted native dependencies, complete physical storage and caller admission." + }, + "family_expansion_decision": "Finish this wrapper audit; do not expand the construction family.", + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-18976973", + "predecessor": "PR2968 released complete-route handoff; PR2915 implementation; PR2877 countdown; PR2951 scaling invoice", + "entry_coverage": { + "open_prs": 227, + "closed_prs": 2435, + "discussions": 1675, + "complete_pagination": true, + "warnings": [] + } + }, + "freshness": { + "upstream_commit": "066f57ff795dbe6d0a0ecc11fe742eadcec00c39", + "priority_revision": 5, + "checked_at_utc": "2026-10-16T16:02:59.269842+00:00", + "guidance_selected_and_inputs": "Root instructions, task catalogue, selected record and all 23 live source pins unchanged since base. Updated intake/archive guidance was read; other changes are unrelated archival research and ledger metadata. No base migration needed.", + "overlap": { + "open_prs": { + "fetched_at": "2026-10-16T15:58:21.320631+00:00", + "complete_pagination": true, + "records": 227 + }, + "discussions": { + "fetched_at": "2026-10-16T15:58:48.210755+00:00", + "complete_pagination": true, + "records": 1681 + }, + "closed_prs": { + "fetched_at": "2026-10-16T15:59:12.725189+00:00", + "complete_pagination": true, + "records": 2437 + } + }, + "warnings": [], + "coverage_limit": "Open/closed PR bodies and Discussion bodies/comments/replies plus local package metadata, not arbitrary diffs or unpublished work." + }, + "verification": { + "environment": "Linux-6.6.87.2-microsoft-standard-WSL2-x86_64-with-glibc2.41 / CPython 3.13.5", + "registered_replay": "CPython 3.12.15 primary and optimized controls passed; 44 complete routes, 125689 bits, 1314 actual elementary B1 calls, 13 behavioral groups.", + "workflow_tests": "158 tests, 11 skips; suite passed.", + "limits": "No hosted CI result, fitted native/selected GL64 payload, full selected cold replay, formal proof or independent human review." + }, + "nearest_overlap": [ + { + "source": "PR2968 high-scaling-scratch-traffic", + "delta": "Its released full-route handoff. This contributes the wrapper tariff and a complete route/native partition, not another scaling invoice." + }, + { + "source": "PR2708 selected-route-live-volume", + "delta": "It proves storage for the older decorated-key cube. This proves physical I/O for the unchanged wrapper with the reached fast cube; it does not claim its storage result." + } + ] +} diff --git a/research/high-route-prefix-cost/VERIFY.json b/research/high-route-prefix-cost/VERIFY.json new file mode 100644 index 0000000000..be33e1db9b --- /dev/null +++ b/research/high-route-prefix-cost/VERIFY.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit2234-stock-threshold/README.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL-TEMPLATE.json.gz", + "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL.json", + "research/community-hyperplane599-audit/pr589/bit589/v9/nine/GEOMETRY.json", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/high-scaling-scratch-traffic/PROOF.md", + "research/high-scaling-total-traffic/traffic.py", + "research/idle-axis-hosting/PROOF.md", + "research/pr589-five-helper-hosting/PROOF.md", + "research/pr589-five-helper-hosting/verify.py", + "research/recursive-parking-boundary/README.md", + "research/selected-bit-fast-primitives/compile_routes.py", + "research/selected-bit-fast-primitives/high_route.py", + "research/selected-bit-fast-primitives/inputs/pr2157.tar", + "research/selected-bit-fast-primitives/inputs/pr2899.tar", + "research/selected-bit-fast-primitives/kernels.py", + "research/selected-bit-fast-primitives/stage.py", + "research/selected-bit-fast-primitives/stage_sources.py", + "research/selected-bit-local-ring-sweeps/PROOF.md", + "research/selected-bit-recursive-closure/PROOF.md", + "upstream/build/sections/02-streams.tex" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Complete measured routes, raw physical counters, exact prefix law, native-call invoices, independent affine endpoints and ownership" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized positive, semantic and cost mutants, padded-prefix rejection, source and typed-receipt controls" + } + ] +} diff --git a/research/high-route-prefix-cost/invoice.py b/research/high-route-prefix-cost/invoice.py new file mode 100644 index 0000000000..a0de096b0f --- /dev/null +++ b/research/high-route-prefix-cost/invoice.py @@ -0,0 +1,58 @@ +"""Independent closed invoices for the unchanged pooled route_packet wrapper.""" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def positive(value): + require(type(value) is int and value > 0, "positive integer cardinality") + + +def countdown(value): + """PR2877's fully drained canonical Counter bill, without pool acquisition.""" + positive(value) + return 15 * value + 14 * value.bit_length() - 5 * value.bit_count() + 36 + + +def suffix_probe(value): + positive(value) + if value % 2 == 0: + return 4 + return 15 if value > 1 and value % 4 == 1 else 12 + + +def copy_rows(highs, fibre): + """Include all nested countdowns and one blank read per scratch acquisition.""" + positive(highs) + positive(fibre) + per_slice = suffix_probe(fibre) + 5 * fibre + if fibre > 1: + per_slice += countdown(fibre) + 1 + return countdown(highs) + 1 + highs * per_slice + + +def wrapper(prefixes, highs, fibre, disposed=False): + positive(prefixes) + positive(highs) + positive(fibre) + require(type(disposed) is bool, "disposal mode") + cube = highs * fibre + result = prefixes * (2 * copy_rows(highs, fibre) + 18 * cube + 19) + result += countdown(prefixes) + 12 + if disposed: + result += 5 * prefixes * cube + 7 + return result + + +def predict(single, prefixes, disposed=False, cube_bits=0): + """Exact prefix law when the complete cube trace is invariant across prefixes.""" + require(type(single) is int and single > countdown(1) + 12, "single-prefix bill") + positive(prefixes) + require(type(disposed) is bool, "disposal mode") + result = prefixes * (single - countdown(1) - 12) + countdown(prefixes) + 12 + if disposed: + positive(cube_bits) + result += 5 * prefixes * cube_bits + 7 + return result diff --git a/research/high-route-prefix-cost/runtime.py b/research/high-route-prefix-cost/runtime.py new file mode 100644 index 0000000000..ab4a03e422 --- /dev/null +++ b/research/high-route-prefix-cost/runtime.py @@ -0,0 +1,418 @@ +"""Authenticated complete routes with an independent physical-I/O observer.""" + +import atexit +import hashlib +import json +import sys +from contextlib import ExitStack +from fractions import Fraction +from pathlib import Path +from types import ModuleType, SimpleNamespace +from unittest.mock import patch + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PREDECESSOR = ROOT / "research/selected-bit-fast-primitives" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + rows = json.loads((PACKAGE / "SOURCES.json").read_bytes())["files"] + require(0 < len(rows) <= 64, "bounded source inventory") + seen, data, total = set(), {}, 0 + for row in rows: + if row["usage"] != "input": + continue + name = row["path"] + require( + name not in seen and not Path(name).is_absolute(), "unique relative input" + ) + require(".." not in Path(name).parts, "contained input") + seen.add(name) + target = ROOT / name + require(target.is_file() and not target.is_symlink(), "regular input: " + name) + size = target.stat().st_size + require(size <= 32 * 1024 * 1024, "bounded input size") + total += size + require(total <= 64 * 1024 * 1024, "bounded total source bytes") + body = target.read_bytes() + require( + hashlib.sha256(body).hexdigest() == row["sha256"], "source hash: " + name + ) + data[name] = body + return data + + +def load_module(name, data): + relative = "research/selected-bit-fast-primitives/" + name + ".py" + require(relative in data, "declared executable source: " + name) + path = ROOT / relative + result = ModuleType(name) + result.__file__ = str(path) + sys.modules[name] = result + # Complete authenticated modules, not edited ASTs or cached bytecode. + exec(compile(data[relative], str(path), "exec"), result.__dict__) # noqa: S102 + return result + + +def close(): + for name in ("source", "stage_sources"): + temporary = getattr(sys.modules.get(name), "_temporary", None) + if temporary is not None: + temporary.cleanup() + + +def load(): + data = authenticate() + names = ("stage_sources", "compile_routes", "kernels", "high_route", "stage") + require(not any(name in sys.modules for name in names), "cold audit namespace") + stage_sources = load_module("stage_sources", data) + try: + _source, retained, _data = stage_sources.activate() + except BaseException: + close() + raise + atexit.register(close) + for name in ("compile_routes", "kernels", "high_route", "stage"): + load_module(name, data) + names = ( + "cardinal_counts", + "directory", + "low_codes", + "macro_code", + "ordinary", + "physical_words", + "records", + "routes", + "scratch_pool", + "stream", + "words", + ) + modules = {name: __import__(name) for name in names} + return SimpleNamespace( + **modules, + retained=retained, + stage=sys.modules["stage"], + registry=sys.modules["compile_routes"].Registry, + ) + + +class Trace: + """Count actual Tape methods once, not their aliasing Word/Lease meters.""" + + def __init__(self, runtime, native): + self.runtime, self.native = runtime, native + self.operations = 0 + + def wrap(self, method): + def counted(*args, **kwargs): + self.operations += 1 + return method(*args, **kwargs) + + return counted + + def snapshot(self): + parking = self.native.runtime.numerical + extra = sum( + counts[key] + for counts in (parking.codec_counts, parking.machine.counts) + for key in ("reads", "writes", "moves") + ) + return self.operations + extra + + def installed(self): + stack = ExitStack() + tape = self.runtime.records.Tape + for name in ("read", "write", "step"): + stack.enter_context( + patch.object(tape, name, self.wrap(getattr(tape, name))) + ) + return stack + + +def native_fixture(runtime, q): + return runtime.ordinary.Ordinary( + q, + SimpleNamespace(codes=SimpleNamespace(q=q)), + SimpleNamespace(families=0), + (runtime.macro_code.Code((("unreachable",),), 0),), + capacity=64, + ) + + +def prepare(runtime, prefixes, q, width, fibre_value, inverse, pattern): + require(type(prefixes) is int and 1 <= prefixes <= 17, "fixture prefix range") + require(q in (3, 5) and type(q) is int, "fixture radix") + require(type(width) is int and 1 <= width <= 3, "fixture width") + require(type(fibre_value) is int and 1 <= fibre_value <= 3, "fixture fibre") + require( + type(inverse) is bool and type(pattern) is int and pattern in (0, 1), + "fixture variant", + ) + bits = q ** (4 * (width - 1)) * fibre_value + require(prefixes * bits <= 100000, "fixture volume limit") + codes = runtime.low_codes.LowCodes(q, 2, 1) + word = ( + ("add", 0, 1, Fraction(1, 2)), + ("scale", 1, 1, Fraction(-2)), + ("swap", 0, 1, Fraction(1)), + ) + if inverse: + word = sys.modules["compile_routes"].inverse_word(word) + chart = runtime.retained.replay(word, 2) + registry = runtime.registry(2) + registry.register(chart, word) + route = runtime.routes.compile_route(((1, 0), (0, 1)), chart, codes) + count = runtime.cardinal_counts.Count + maximum = count.literal(q**width) + bank = runtime.physical_words.PhysicalArena(64) + bank.prepare(maximum) + modulus = bank.load(maximum) + ring = runtime.words.Ring(modulus) + context = runtime.directory.Context(ring, codes) + old_count, fibre = count.literal(prefixes), count.literal(fibre_value) + source = runtime.records.Tape() + initial = bytes( + ((i * 13 ^ i // 3 ^ 5) & 1) ^ pattern for i in range(prefixes * bits) + ) + for bit in initial: + source.append(bit) + source.rewind() + native = native_fixture(runtime, q) + adapter = runtime.stage.Adapter(native, registry, capacity=64) + pool = runtime.scratch_pool.ScratchPool(q * q + 256) + scope = runtime.stage.StagePool(pool, adapter) + return SimpleNamespace(**locals()) + + +def physical_tapes(state): + native, machine = state.native, state.native.runtime + tapes = [ + state.source, + state.maximum.tape, + state.context.highs.tape, + state.old_count.tape, + state.fibre.tape, + native.output, + machine.output, + ] + tapes.extend( + ( + *state.pool.tapes, + *native.pool.tapes, + *machine.pool.tapes, + *machine.roles.values(), + *machine.handoff.values(), + ) + ) + for bank in ( + state.bank, + state.adapter.high_bank, + *native.banks, + machine.arena, + machine.indices, + ): + tapes.extend(word.tape for word in (*bank.words, bank.template)) + return tuple({id(tape): tape for tape in tapes}.values()) + + +def meters(tapes, trace): + parking = trace.native.runtime.numerical + return sum( + meter.reads + meter.writes + meter.moves for meter in (t.meter for t in tapes) + ) + sum( + counts[key] + for counts in (parking.codec_counts, parking.machine.counts) + for key in ("reads", "writes", "moves") + ) + + +def endpoint(state, output): + """Direct full q-adic matrix multiplication, independent of factor execution.""" + q, width, fibre = state.q, state.width, state.fibre_value + high, modulus = q ** (width - 1), q**width + lifted = [ + [int(x.numerator * pow(x.denominator, -1, modulus)) % modulus for x in row] + for row in state.chart + ] + expected = bytearray(len(state.initial)) + for ordinal in range(high**4): + digits, remaining = [0] * 4, ordinal + for position in range(3, -1, -1): + remaining, digits[position] = divmod(remaining, high) + matrix = [ + [int(i == j) + q * digits[2 * i + j] for j in range(2)] for i in range(2) + ] + target = 0 + for i in range(2): + for j in range(2): + value = sum(matrix[i][k] * lifted[k][j] for k in range(2)) % modulus + target = target * high + (value - state.route.target_low[i][j]) // q + for prefix in range(state.prefixes): + for suffix in range(fibre): + origin = prefix * state.bits + ordinal * fibre + suffix + destination = prefix * state.bits + target * fibre + suffix + expected[destination] = state.initial[origin] + require( + bytes(output.physical.cells[1 : len(expected) + 1]) == expected, + "affine endpoint", + ) + require( + all( + bit == state.runtime.words.BLANK + for bit in output.physical.cells[len(expected) + 1 :] + ), + "output extent", + ) + require( + bytes(state.source.cells[1 : len(expected) + 1]) == state.initial, + "borrowed input", + ) + require(state.source.head == output.head == 1, "canonical endpoint heads") + + +def borrowed_tapes(state): + return ( + state.source, + state.old_count.tape, + state.fibre.tape, + state.context.highs.tape, + state.modulus.tape, + state.ring.one.tape, + state.context.cap.tape, + ) + + +def completed_boundary(state, output, originals): + borrowed = borrowed_tapes(state) + require(state.pool.live == {output.slot: output}, "only returned output is owned") + require( + tuple(bytes(tape.cells) for tape in borrowed) == originals, + "all borrowed input and context bytes preserved", + ) + require(all(tape.head == 1 for tape in borrowed), "all borrowed heads returned") + require( + not state.adapter.high_bank.live and not state.adapter.high_bank.initialized, + "complete high-bank teardown", + ) + require( + state.native.closed and state.native.output.read() == state.runtime.words.BLANK, + "completed and consumed native output", + ) + endpoint(state, output) + + +def execute(state, prefix_probe=False): + runtime, native = state.runtime, state.native + trace, calls, cubes = Trace(runtime, native), [], [] + original_run = native.run + + def observed(*args, **kwargs): + start = trace.snapshot() + result = original_run(*args, **kwargs) + calls.append(dict(traffic=trace.snapshot() - start, fitted=native.last_fitted)) + return result + + original_cube = state.adapter.route_cube + + def observed_cube(*args, **kwargs): + if prefix_probe: + # Deliberate C^2 cost mutant outside the cube invoice. + for _ in range(state.prefixes): + state.source.read() + before = trace.snapshot() + result = original_cube(*args, **kwargs) + cubes.append(trace.snapshot() - before) + return result + + tapes = physical_tapes(state) + originals = tuple(bytes(tape.cells) for tape in borrowed_tapes(state)) + # StagePool rebinds routes.route_cube after every B1 return. Observe the + # stable adapter method so later prefixes cannot silently escape the census. + with ( + trace.installed(), + patch.object(native, "run", observed), + patch.object(state.adapter, "route_cube", observed_cube), + state.scope.install(), + ): + # Entry deltas exclude native construction/initial marker erasure. + start, raw = trace.snapshot(), meters(tapes, trace) + output = runtime.routes.route_packet( + state.source, state.route, state.context, state.old_count, state.fibre + ) + traffic = trace.snapshot() - start + require(traffic == meters(tapes, trace) - raw, "raw meter/observer agreement") + try: + # Oracle and ownership probes are outside the measured interval. + completed_boundary(state, output, originals) + finally: + disposal_start = trace.snapshot() + output.clear() + disposal = trace.snapshot() - disposal_start + require(disposal == 5 * len(state.initial) + 7, "exact output disposal") + state.pool.empty() + return traffic, disposal, calls, cubes + + +def cleanup(state): + state.adapter.close() + state.context.close() + state.ring.close() + state.bank.free(state.modulus) + state.bank.erase_owned() + for value in (state.maximum, state.old_count, state.fibre): + value.close() + state.source.clear() + require( + not state.bank.live and not state.adapter.high_bank.live, + "closed numerical work", + ) + + +def run_case( + runtime, + prefixes, + q=3, + width=2, + fibre_value=1, + inverse=False, + pattern=0, + prefix_probe=False, +): + state = prepare(runtime, prefixes, q, width, fibre_value, inverse, pattern) + try: + traffic, disposal, calls, cubes = execute(state, prefix_probe) + require(len(calls) == state.adapter.calls["swaps"], "all reached B1 intervals") + require( + len(cubes) == state.adapter.calls["cubes"] == prefixes, + "one observed cube per prefix", + ) + require( + all(row["fitted"] is False for row in calls), + "declared elementary B1 fixtures", + ) + return dict( + prefixes=prefixes, + q=q, + width=width, + fibre=fibre_value, + inverse=inverse, + pattern=pattern, + cube_bits=state.bits, + traffic=traffic, + disposed_traffic=traffic + disposal, + cube_traffic=sum(cubes), + wrapper_traffic=traffic - sum(cubes), + native_calls=len(calls), + native_traffic=sum(row["traffic"] for row in calls), + native_trace_sha256=hashlib.sha256( + json.dumps(calls, sort_keys=True).encode() + ).hexdigest(), + pool_peak=state.pool.peak, + ) + finally: + cleanup(state) diff --git a/research/high-route-prefix-cost/test_verify.py b/research/high-route-prefix-cost/test_verify.py new file mode 100644 index 0000000000..afc0efd07d --- /dev/null +++ b/research/high-route-prefix-cost/test_verify.py @@ -0,0 +1,207 @@ +#!/usr/bin/env python3 +"""Behavioral controls for the actual route wrapper and its cost observer.""" + +import copy +import sys +import unittest +from pathlib import Path +from unittest.mock import patch + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import invoice +import runtime +import verify + + +class AuditTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.runtime = runtime.load() + cls.native = runtime.native_fixture(cls.runtime, 3) + cls.single = runtime.run_case(cls.runtime, 1) + + def test_literal_complete_invoice(self): + row = self.single + self.assertEqual(row["traffic"], 438000) + self.assertEqual(row["cube_traffic"], 431027) + self.assertEqual(row["wrapper_traffic"], 6973) + self.assertEqual(row["native_traffic"], 154884) + self.assertEqual(row["native_calls"], 6) + self.assertEqual(row["disposed_traffic"], 438412) + verify.check_wrapper(row) + + def test_alias_meters_are_not_physical_objects(self): + pool = self.runtime.scratch_pool.ScratchPool(1) + lease = pool.acquire() + trace = runtime.Trace(self.runtime, self.native) + meter = lease.physical.meter + before = meter.reads + meter.writes + meter.moves + with trace.installed(): + start = trace.snapshot() + lease.append(self.runtime.words.ONE) + lease.rewind() + self.assertEqual(lease.read(), self.runtime.words.ONE) + lease.clear() + actual = trace.snapshot() - start + physical = meter.reads + meter.writes + meter.moves - before + alias = lease.meter.reads + lease.meter.writes + lease.meter.moves + self.assertEqual(actual, 21) + self.assertEqual(physical, 21) + self.assertEqual(physical + alias, 42) + pool.empty() + + def test_counter_oracle(self): + count = self.runtime.cardinal_counts.Count + pool = self.runtime.scratch_pool.ScratchPool(4) + trace = runtime.Trace(self.runtime, self.native) + for value in range(1, 257): + source = count.literal(value) + with trace.installed(), pool.install(): + start = trace.snapshot() + counter = self.runtime.stream.Counter(source) + for _ in range(value): + self.assertFalse(counter.finished) + counter.decrement() + self.assertTrue(counter.finished) + counter.close() + actual = trace.snapshot() - start + self.assertEqual(actual, invoice.countdown(value) + 1) + pool.empty() + source.close() + + def test_copy_rows_oracle(self): + count, tape = self.runtime.cardinal_counts.Count, self.runtime.records.Tape + pool = self.runtime.scratch_pool.ScratchPool(8) + trace = runtime.Trace(self.runtime, self.native) + values = (1, 2, 3, 4, 5, 8, 9, 13, 16, 17, 33) + for highs in values: + for fibre in values: + rows, suffix = count.literal(highs), count.literal(fibre) + source, output = tape(), tape() + expected = bytes(i % 2 for i in range(highs * fibre)) + for bit in expected: + source.append(bit) + source.rewind() + with trace.installed(), pool.install(): + start = trace.snapshot() + self.runtime.routes.copy_rows(source, output, rows, suffix) + actual = trace.snapshot() - start + self.assertEqual(actual, invoice.copy_rows(highs, fibre)) + self.assertEqual(bytes(output.cells[1:]), expected) + pool.empty() + for item in (source, output): + item.clear() + rows.close() + suffix.close() + + def test_sharp_wrapper_constants(self): + self.assertEqual(invoice.wrapper(1, 1, 1), 265) + self.assertEqual(invoice.wrapper(1, 1, 1, True), 277) + for prefixes in range(1, 33): + for highs in range(1, 33): + for fibre in range(1, 33): + volume = prefixes * highs * fibre + self.assertLessEqual( + invoice.wrapper(prefixes, highs, fibre), 265 * volume + ) + self.assertLessEqual( + invoice.wrapper(prefixes, highs, fibre, True), 277 * volume + ) + actual = runtime.run_case(self.runtime, 1, width=1) + self.assertEqual(actual["wrapper_traffic"], 265) + self.assertEqual(actual["disposed_traffic"] - actual["cube_traffic"], 277) + + def test_endpoint_preserving_quadratic_cost_mutant(self): + ordinary = runtime.run_case(self.runtime, 3) + mutant = runtime.run_case(self.runtime, 3, prefix_probe=True) + # Both complete calls passed the affine endpoint and ownership oracle. + self.assertEqual(mutant["traffic"] - ordinary["traffic"], 9) + self.assertEqual(mutant["cube_traffic"], ordinary["cube_traffic"]) + self.assertEqual(mutant["native_traffic"], ordinary["native_traffic"]) + with self.assertRaisesRegex(ValueError, "exact wrapper invoice"): + verify.check_wrapper(mutant) + with self.assertRaisesRegex(ValueError, "complete typed receipt"): + verify.check_receipt(mutant, ordinary) + + def test_complemented_payload_and_prefix_lift(self): + complemented = runtime.run_case(self.runtime, 3, pattern=1) + verify.check_lift(self.single, complemented) + self.assertEqual(complemented["traffic"], 1313895) + self.assertEqual(complemented["disposed_traffic"], 1315117) + self.assertEqual(complemented["native_calls"], 18) + + def test_padded_prefix_changes_the_invoice(self): + state = runtime.prepare(self.runtime, 1, 3, 2, 1, False, 0) + try: + # Same value, one extra high zero before RIGHT. This is deliberately + # outside the canonical-input premise, not a selected-source bug. + state.old_count.tape.cells.insert(-1, self.runtime.words.ZERO) + traffic, _disposal, _calls, cubes = runtime.execute(state) + self.assertEqual(traffic, self.single["traffic"] + 14) + self.assertEqual(sum(cubes), self.single["cube_traffic"]) + self.assertNotEqual(traffic - sum(cubes), invoice.wrapper(1, 81, 1)) + finally: + runtime.cleanup(state) + + def test_endpoint_fault(self): + state = runtime.prepare(self.runtime, 1, 3, 1, 1, False, 0) + output = state.pool.acquire() + try: + output.append(state.initial[0] ^ 1) + output.rewind() + with self.assertRaisesRegex(ValueError, "affine endpoint"): + runtime.endpoint(state, output) + finally: + output.clear() + state.pool.empty() + runtime.cleanup(state) + + def test_cost_omission_and_type_corruptions(self): + for key, change in ( + ("traffic", -1), + ("wrapper_traffic", -1), + ("native_traffic", -self.single["native_traffic"]), + ): + altered = copy.deepcopy(self.single) + altered[key] += change + with self.assertRaisesRegex(ValueError, "complete typed receipt"): + verify.check_receipt(altered, self.single) + altered = copy.deepcopy(self.single) + altered["prefixes"] = True + with self.assertRaisesRegex(ValueError, "complete typed receipt"): + verify.check_receipt(altered, self.single) + + def test_invalid_domains(self): + for value in (0, -1, True, 1.0): + with self.assertRaisesRegex(ValueError, "positive integer cardinality"): + invoice.wrapper(value, 1, 1) + for prefixes in (0, 18, True): + with self.assertRaisesRegex(ValueError, "fixture prefix range"): + runtime.prepare(self.runtime, prefixes, 3, 1, 1, False, 0) + for fibre in (0, 4, True): + with self.assertRaisesRegex(ValueError, "fixture fibre"): + runtime.prepare(self.runtime, 1, 3, 1, fibre, False, 0) + + def test_source_corruption_and_missing_declaration(self): + original = Path.read_bytes + target = runtime.PREDECESSOR / "high_route.py" + + def corrupted(path): + body = original(path) + return body + b"\n# corruption\n" if path == target else body + + with ( + patch.object(Path, "read_bytes", corrupted), + self.assertRaisesRegex(ValueError, "source hash: .*high_route.py"), + ): + runtime.authenticate() + with self.assertRaisesRegex(ValueError, "declared executable source"): + runtime.load_module("kernels", {}) + + def test_cold_namespace(self): + with self.assertRaisesRegex(ValueError, "cold audit namespace"): + runtime.load() + + +if __name__ == "__main__": + unittest.main() diff --git a/research/high-route-prefix-cost/verify.py b/research/high-route-prefix-cost/verify.py new file mode 100644 index 0000000000..9d03041034 --- /dev/null +++ b/research/high-route-prefix-cost/verify.py @@ -0,0 +1,112 @@ +#!/usr/bin/env python3 +"""Exact old-prefix lifting of complete reached high-route traffic.""" + +import argparse +import hashlib +import json +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from invoice import predict, wrapper +from runtime import PACKAGE, load, require, run_case + +PREFIXES = (1, 2, 3, 4, 7, 8, 9, 16, 17) +CONFIGURATIONS = ( + dict(q=3, width=1, fibre_value=3), + dict(q=3, width=2, fibre_value=1), + dict(q=3, width=2, fibre_value=3, inverse=True), + dict(q=5, width=2, fibre_value=1, inverse=True), +) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def check_receipt(actual, expected): + require(canonical(actual) == canonical(expected), "complete typed receipt") + + +def check_wrapper(row): + highs = row["q"] ** (4 * (row["width"] - 1)) + expected = wrapper(row["prefixes"], highs, row["fibre"]) + require(row["wrapper_traffic"] == expected, "exact wrapper invoice") + volume = row["prefixes"] * row["cube_bits"] + require(expected <= 265 * volume, "uniform wrapper bound") + closed = row["disposed_traffic"] - row["cube_traffic"] + require( + closed == wrapper(row["prefixes"], highs, row["fibre"], True), + "closed wrapper invoice", + ) + require(closed <= 277 * volume, "uniform closed wrapper bound") + + +def check_lift(single, row): + check_wrapper(row) + require( + row["traffic"] == predict(single["traffic"], row["prefixes"]), "prefix lift" + ) + require( + row["disposed_traffic"] + == predict(single["traffic"], row["prefixes"], True, row["cube_bits"]), + "disposed prefix lift", + ) + require( + row["native_calls"] == row["prefixes"] * single["native_calls"], + "native call multiplicity", + ) + require( + row["native_traffic"] == row["prefixes"] * single["native_traffic"], + "native traffic multiplicity", + ) + + +def group(runtime, parameters, prefixes): + rows = [run_case(runtime, count, **parameters) for count in prefixes] + require(rows[0]["prefixes"] == 1, "single-prefix reference first") + for row in rows: + check_lift(rows[0], row) + complementary = run_case(runtime, 3, **parameters, pattern=1) + check_lift(rows[0], complementary) + return dict(parameters=parameters, rows=rows, complementary=complementary) + + +def result(): + runtime = load() + groups = [group(runtime, parameters, PREFIXES) for parameters in CONFIGURATIONS] + groups.append(group(runtime, dict(q=3, width=3, fibre_value=1), (1, 2, 3))) + rows = [row for item in groups for row in (*item["rows"], item["complementary"])] + return dict( + status="PASS_HIGH_ROUTE_PREFIX_COST", + cases=len(rows), + bits=sum(row["prefixes"] * row["cube_bits"] for row in rows), + native_calls=sum(row["native_calls"] for row in rows), + groups=groups, + rows_sha256=hashlib.sha256(canonical(rows).encode()).hexdigest(), + ) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--emit", action="store_true", help="print, never replace, a new receipt" + ) + args = parser.parse_args() + actual = result() + if args.emit: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + path = PACKAGE / "RESULT.json" + require(path.stat().st_size <= 1024 * 1024, "bounded receipt") + check_receipt(actual, json.loads(path.read_bytes())) + print( + actual["status"], + "cases=" + str(actual["cases"]), + "bits=" + str(actual["bits"]), + "native_calls=" + str(actual["native_calls"]), + ) + + +if __name__ == "__main__": + main()