diff --git a/research/radical-fanout-inverse-tables/README.md b/research/radical-fanout-inverse-tables/README.md new file mode 100644 index 0000000000..5db86ef8c4 --- /dev/null +++ b/research/radical-fanout-inverse-tables/README.md @@ -0,0 +1,194 @@ +# Static inverse tables remove 1,661,435 repeated tuple searches + +This contribution was produced by Nick Petalas. Apache-2.0. + +The complete radical-fanout command performs **260 `tuple.index` calls instead +of 1,661,695**, with byte-identical complete output. The change precomputes +additive inverses and unit inverses once per immutable finite ring. It retains +every demand, word, literal input, arithmetic check, control and shortest-path +query in lee-phys's [PR6210](https://github.com/CrocSwap/integer-mult-bounds/pull/6210). + +Claim type: an exact implementation-work reduction with a scoped equivalence +argument and finite conformance evidence. This is a verifier-engineering +contribution, not a new mathematical tariff, an audit of the predecessor theorem, +a supplier admission or a new kappa. Wall time is reported separately below. + +## Implementation and equivalence + +[retained_source.py](retained_source.py) is the exact published verifier at +`4e08457f4d0b69c00a6ca62eca81c8d0a55f3e60`. [UPSTREAM.json](UPSTREAM.json) +records its original path, Git blob, SHA256 and author, together with the exact +source README. The pending commit is not required in the local Git object store. +All executable bytes required for replay are retained here. [SOURCES.json](SOURCES.json) +pins only canonical-ancestor task and selected-record provenance. + +[fast.py](fast.py) authenticates the retained executable before importing it. +Its only replacement is the `Ring` class used by the retained ring factory. +The new frozen subclass adds two tuples and overrides `neg` and `inv`. +The source's full `main`, constructors, scalar interpreter, checks, Dijkstra +search and output statements execute unchanged. + +For a valid ring table, the cached entry at x is exactly the original +`add[x].index(0)` or `mul[x].index(one)`. The tuples cannot become stale because +the original operation tables and the new tables are immutable. A fresh ring +builds fresh tables. There is no persisted answer or workload cache. +For a nonunit, the sentinel sends execution through the original failing +lookup, preserving its `ValueError` and message. Python negative indices and +out-of-range indices also preserve their original behavior. + +It follows by induction over scalar instructions that every intermediate state, +gate coefficient and endpoint is unchanged. The search's neighbor states, costs, +heap ties and returned paths are unchanged too. No case is replaced by a cached +verdict. Constructor table scans are included in the full command and in the +260-call count. Construction also adds one membership test per ring element; +the count above is specifically `tuple.index` invocations, not every table read. + +The executable accepts ring orders 1 through 81. The theorem's supplied fixtures +have orders 16, 81 and 64, and its nonlocal rejection fixture has order four. +The adapter adds at most 162 tuple entries per ring. Successful inverse queries +and all negations then use constant-time tuple indexing instead of a row search. +The explicit nonunit failure path retains its row search. + +## Evidence + +The new checker compares every element at both its nonnegative and negative +Python index in all three rings, 322 element/index cases. It also checks the +out-of-range exception type and message, rejects invalid orders and nonsquare +tables, and rejects changed executable source before import. Sixteen controls +run under normal and optimized Python. + +Two fresh complete commands have equal stdout. Separate untimed profiles run +both complete workloads again and count exactly 1,661,695 and 260 tuple searches. +All four outputs agree, with SHA256 +`6fcd968e3899b567f520b5b05bde6c481dd7581a754026af2aa300bf6396da1d`. +The generated receipt is printed to stdout and binds the actual local package +hashes. No receipt is handwritten or stored as an expected scientific answer. + +The preserved source output enumerates 22,152 demands, 221,520 words, +1,772,160 formal forward/inverse evaluations, 1,310,720 literal evaluations, +four oracle queries and 8,465 settled entries. These are the predecessor's +workload and counters, not new mathematical findings claimed here. + +## Wall-time measurement + +The benchmark times fresh complete scientific commands, including imports, +table initialization, every check and the four shortest-path searches. It +compares every complete stdout and fails on a nonzero exit or stderr. Profiling +is separate from the reported timing sweep. The generic package runner and +export tools are outside the measured boundary. + +The wall-time comparison is **inconclusive on this shared host**. Ten alternating +pairs have zero errors and equal complete output. The optimized median is lower, +but the ranges overlap and the difference is smaller than run-to-run variation. +No portable elapsed-time improvement is claimed. + +| Complete command | Median seconds | Range seconds | +| --- | ---: | ---: | +| Retained source | 3.555522 | 3.155300 to 3.913315 | +| Inverse-table adapter | 3.256747 | 3.027612 to 3.633472 | + +Raw alternating pairs, in seconds, are: + +| Pair | Retained | Adapter | +| ---: | ---: | ---: | +| 1 | 3.762916 | 3.384731 | +| 2 | 3.551804 | 3.531334 | +| 3 | 3.913315 | 3.633472 | +| 4 | 3.899865 | 3.448595 | +| 5 | 3.621823 | 3.143365 | +| 6 | 3.559239 | 3.291734 | +| 7 | 3.329549 | 3.221761 | +| 8 | 3.421450 | 3.030692 | +| 9 | 3.202639 | 3.033553 | +| 10 | 3.155300 | 3.027612 | + +Environment: CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. The final +load averages were 4.43, 4.00 and 3.12. Other research processes shared the host; +the measured commands themselves ran serially. Both engines used identical +warning-strict flags and fresh private bytecode namespaces. The adapter digest +was `a556f916c57b6fb25d1cbcb54abbaf92d1cc32dc96e4c5fc886b461328e31f32`. + +The separate baseline profile records 0.238 seconds of tuple-index self-time +within 6.546 profiled seconds. Endpoint interpretation, count bookkeeping and +shortest-path expansion remain substantial work. Tracing changes the timing +distribution, so this profile explains the limited scope of the optimization +rather than establishing an untraced speed bound. The exact lookup-count +reduction is the result being shipped; timing does not certify a faster multiplier. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/radical-fanout-inverse-tables/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/radical-fanout-inverse-tables/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/radical-fanout-inverse-tables +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/radical-fanout-inverse-tables --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/radical-fanout-inverse-tables/benchmark.py --rounds 10 +``` + +Another CPython 3.12 path may replace the displayed interpreter. Set +`IMB_RUN_ROOT` to an existing private scratch directory to collect all temporary +files there; otherwise the system temporary directory is used. Direct replay +needs no Git, network, foreign commit or +third-party package. Child interpreters use fresh private bytecode namespaces +and `-B`; all temporary directories are removed. The optional benchmark prints +all raw samples, complete-output digests, environment and summary statistics. +CI registers conformance, not a host-specific runtime threshold. + +## Limits and engineering choices + +This changes only an isolated optional replay. It does not patch the predecessor +package, shared runner or selected result. The predecessor mathematics remains +a cited result with its own review obligations. No selected scientific cold +replay, physical/native/compiler/stock/precision/outer proof, Lean or Docker run +is claimed. All five selected framework assumptions remain. Independent human +and formal proof-kernel review are unclaimed. + +New functions fit within sixty lines. The new table loops are bounded by 81; +conformance uses three fixed rings; timing accepts five through ten rounds; +each child has a 120-second timeout. The retained source already has explicit +search resource guards and is unchanged. Its long functions and search loops +are retained dependencies, not newly refactored code. Managed Python allocation +is a documented deviation from fixed-allocation guidance. New table capacity +is bounded as above. The four inverse-method targets in the conformance helper +and the single explicit ring-factory replacement are bounded uses of dispatch. +Warning-strict normal and optimized execution are registered. No external linter +or proof assistant is required. Local compilation is checked without writing +bytecode files. + +Build the Lever led to the rerunnable checker and benchmark. Prove It Works led +to complete-command equality, actual profile counts and the corrupt-source +control. Explain the Number keeps the wall-time uncertainty separate from the +exact lookup reduction. The engineering-mode playbook is Autonomous local run. + +## Open next questions + +Does this table adapter produce a stable complete wall-time gain on an idle +Linux CPython 3.12 host? Run five or more alternating complete commands with +`benchmark.py`, retain all output digests, and report medians and ranges. The +workload is supplied; an additional host measurement is missing. A source-level +factory hook could later integrate the adapter without altering the mathematical +workload, but no integration or additional optimization is reserved here. + +## Credit and overlap + +The new inverse-table adapter, equivalence explanation, checker and measurement +script were produced by Nick Petalas. The radical-triple theorem, complete +enumerated workload, interpreter and search are lee-phys's. Retain the source's +credit to #5259/#5514, Ali Romman #5266/#5310, lee-phys #5139/#5163, Nick Petalas +#5208/#4916, Krzysztof Wojt #5045, Ross Richardson #3063/#3121, Cinna Davis, +Anthony, Oscar Fennell, Tekalign and the retained lineage. The two retained +source files preserve their original credit verbatim. + +The scientific base is canonical main +`a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8. The selected +binding-only orientation passed and resolves to PR6030 at kappa .003125804; +the older value in current-priority prose is not used as the selected value. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279673) +reserves this optimization. Live open and account PRs, active Discussions, +recent handoffs, local locks, merged term searches and main README searches +found no matching optimization in their stated coverage. The overlap helper +covered 338 open PRs and 5,957 Discussion records with complete remote pagination, +but only 91 of 8,623 local note records. Separate Git README searches cover the +omitted main files for the distinctive terms; neither search proves novelty. diff --git a/research/radical-fanout-inverse-tables/SOURCE-README.md b/research/radical-fanout-inverse-tables/SOURCE-README.md new file mode 100644 index 0000000000..a122a5de58 --- /dev/null +++ b/research/radical-fanout-inverse-tables/SOURCE-README.md @@ -0,0 +1,368 @@ +# Exact tariff for three independent radical demands + +**Scoped written proof with exact finite corroboration; no new kappa.** +For three arbitrary dirty rows over the sixteen-element ring + + R16 = F2[e,h,z]/(e,h,z)^2, + lambda = (e,h,e+h+z), + +this package determines the exact cost for every six strictly positive +receiving-row prices. The price envelope has **ten indispensable linear +terms**, with matching words and a lower bound covering every finite +interleaving. The theorem extends to every commutative unital local ring +whose three demand classes in `m/m^2` are linearly independent over `R/m`. +Neither finiteness nor `m^2=0` is needed for that extension. + +This answers the non-zero-sum, three-generator question explicitly left in +lee-phys [#5259](https://github.com/CrocSwap/integer-mult-bounds/pull/5259). +That predecessor's nineteen-term theorem concerns nonprincipal **zero-sum** +triples. Here the sum is z, and its cheaper two-insertion families do not +supply the requested endpoint. Ali Romman's +[#5310](https://github.com/CrocSwap/integer-mult-bounds/pull/5310) +classifies source-insertion feasibility; it does not settle this total tariff. + +## Contract and theorem + +Let R be a commutative local ring with `1 != 0`, maximal ideal m and residue +field `k=R/m`. Assume + + lambda_i in m, i=0,1,2, + [lambda_0], [lambda_1], [lambda_2] are k-linearly independent in m/m^2. + +There are exactly three independent arbitrary dirty rows `a_i in R^w`, +`w >= 1`, and one disjoint preserved source `p in R^w`. A fixed finite +straight-line word must send each row to `a_i+lambda_i p` for every input. +The only gates are + + P_i(beta): A_i <- A_i + beta p, price mu_i > 0; + E_ij(alpha): A_i <- A_i + alpha A_j, price c_i > 0, i != j. + +Every coefficient and ordered pair is available. Prices are finite, +stationary, coefficient-independent complete abstract prices; ADD prices +depend only on the receiving row. Zero-coefficient gates may be deleted. +There are no auxiliary rows, clearing operations, observations, adaptive +branches or free basis changes. An inverse execution has its own bill. + +**Theorem.** For distinct i,j,k define + + D = mu_0 + mu_1 + mu_2, + T_i = 2mu_i + 2c_j + 2c_k, + R_ij;k = 2mu_i + mu_j + 2c_k. + +Then the exact optimum is the minimum of D, the three T terms and the six R +terms. Equivalently, writing `{i,j}={0,1,2}\{k}`, + + B_k = mu_i + mu_j + min(mu_i,mu_j) + 2c_k, + OPT = min(D,T_0,T_1,T_2,B_0,B_1,B_2). + +Each of the ten expanded terms is uniquely cheapest for some strictly +positive prices. This is a complete **price envelope**, not a claim that +these ten count vectors form the complete componentwise Pareto frontier. +The distinction matters in the two-root, two-insertion case below. + +For R16, `m=(e,h,z)`, `m^2=0`, and `k=F2`. The coefficient matrix of +`(e,h,e+h+z)` in the basis `(e,h,z)` is triangular with diagonal entries 1, +so the hypothesis holds. With common prices `mu_i=mu` and `c_i=c`, + + OPT = min(3mu, 2mu+4c). + +The switch is at `mu=4c`. With unequal prices `(mu;c)=(3,5,10;1,3,2)`, +the optimum is **15**, attained by `R_01;2`. With `(1,9,9;1,1,1)`, it is +**6**, attained by `T_0`. + +## Lower bound for arbitrary interleavings + +Track the three dirt coefficients and the source coefficient in each row. +The dirt matrix starts at I. Every ADD is an invertible elementary row +operation, and an insertion does not affect dirt. Thus every prefix and +suffix dirt matrix is invertible. Correctness on all inputs forces the +final dirt matrix to be I and the final source column to be lambda. Scalar +inputs already force these identities; they also suffice for every width w. + +### Incoming-row return lemma + +A row cannot receive exactly one nonzero ADD in a restoring word. Suppose +its only incoming ADD is `E_ij(alpha)`, and let M be the preceding invertible +dirt matrix. Row i has remained the standard row e_i. The update changes it +to `e_i+alpha m_j`, where m_j is row j of M. No subsequent operation changes +this dirt row. Restoration would imply `alpha m_j=0`; right multiplication +by `M^-1` gives `alpha e_j=0`, hence `alpha=0`, a contradiction. + +Consequently, a row with a nonzero demand and no insertion must receive at +least two ADDs. With no incoming ADD its source coefficient would stay zero; +exactly one is excluded by the lemma. This is the incoming-row argument +credited to #3063/#4916/#5163 and used in #5259. It applies to the **total** +number of incoming ADDs, not separately to each directed edge. + +### Two insertions must both use units + +If the insertion coefficients are beta_t and their rows are r_t, linearity +of the source column gives the exact identity + + lambda = sum_t (L_t e_(r_t)) beta_t, (1) + +where L_t is the invertible matrix of all ADDs after insertion t. Later +insertions add their own terms and do not change this propagation rule. +Equation (1) permits arbitrary earlier/later insertions, cancellations and +feedback through other rows. + +Every element of a local ring is either in m or is a unit. There is no +zero-insertion solution because all three demands are nonzero. + +* With one insertion having a unit coefficient, reduction of (1) modulo m + gives a nonzero field scalar times a column of an invertible matrix. That + column cannot vanish, whereas lambda reduces to zero. If instead the + coefficient lies in m, reducing (1) modulo `m^2` places all three demand + classes in the span of one class. Both possibilities contradict the + hypotheses. Thus at least two insertions are necessary. +* With exactly two insertions and exactly one unit coefficient, the same + reduction modulo m leaves one nonzero invertible-matrix column and gives + a contradiction. If neither coefficient is a unit, both lie in m. For + `beta in m`, the class of `a beta` in `m/m^2` equals the residue of a times + the class of beta. Therefore (1) puts the three demand classes in the span + of the two insertion classes, which has dimension at most two. This also + contradicts independence. + +Hence **every solution with exactly two insertions has two unit insertion +coefficients**. This conclusion does not rule out such words: the matching +T words below use two units. It rules out the rank-two nonunit mechanism. + +### Classify the insertion support + +Write S for the set of rows receiving nonzero insertions, and K_i for the +number of nonzero incoming ADDs into row i. + +1. If S contains all three rows, the bill is at least D. +2. If `S={i}`, the preceding argument forces at least two insertions into i. + The other two rows have nonzero demand and no insertion, so `K_j,K_k>=2`. + The bill is at least T_i. +3. Let `S={i,j}` and let k have no insertion, so `K_k>=2`. If row i receives + at least two insertions, the bill is at least `R_ij;k`; the same conclusion + with i,j interchanged holds if j receives at least two. +4. The only remaining case has exactly one insertion in each of i and j. + Both insertion coefficients are units. If i received no ADD, its final + source coefficient would equal its sole unit insertion coefficient, + contrary to `lambda_i in m`. Thus `K_i>0`, hence `K_i>=2` by the return + lemma; likewise `K_j>=2`. Every such word costs at least + + mu_i+mu_j+2c_i+2c_j+2c_k + = (T_i+T_j)/2 + c_i+c_j + > min(T_i,T_j). (2) + + It therefore cannot be cheapest at any strictly positive price vector. + +These alternatives exhaust all finite words and prove the stated lower +bound. In particular, (2) is a **price-dependent comparison with a pair of +other words**, not componentwise domination by a single count vector. It +establishes the envelope without classifying all unexposed Pareto vectors. + +## Matching words + +All words below are listed in chronological order. For any current dirty +rows, the echo + + E_ji(a), P_i(b), E_ji(-a) + +increments root i by `b p` and receiver j by `-ab p`, while restoring all +original dirt. Indeed j first becomes `A_j+a A_i`, root i then becomes +`A_i+b p`, and the last gate leaves `A_j-ab p`. This calculation remains +valid when A_i and A_j already contain source contributions. + +Set `u_i=lambda_i-1`. Since `lambda_i in m`, u_i is a unit. Independence +makes every lambda_i nonzero. Thus all coefficients in these words are +nonzero and their displayed count vectors are exact. + +* **D:** `P_0(lambda_0), P_1(lambda_1), P_2(lambda_2)`. +* **T_i:** for the other two rows j,k, use + + E_ji(-lambda_j), P_i(1), E_ji(lambda_j), + E_ki(-lambda_k u_i^-1), P_i(u_i), E_ki(lambda_k u_i^-1). + + The first echo delivers lambda_j to j, the second delivers lambda_k to k, + and i receives `1+u_i=lambda_i`. The bill is `2mu_i+2c_j+2c_k`. +* **R_ij;k:** use + + E_ki(-lambda_k), P_i(1), E_ki(lambda_k), + P_i(u_i), P_j(lambda_j). + + The echo delivers lambda_k to k; the last two insertions leave the + remaining demands. The bill is `2mu_i+mu_j+2c_k`. + +For R16, signs disappear, `u_i=1+lambda_i` is self-inverse and +`lambda_k u_i^-1=lambda_k`. In particular a six-gate T_0 word is + + E_10(h), P_0(1), E_10(h), + E_20(e+h+z), P_0(1+e), E_20(e+h+z). + +These constructions attain every term of the lower envelope. Combined with +the preceding exhaustive lower bound, they prove the theorem for arbitrary +strictly positive real prices, independently of finite computation. + +## All ten terms are necessary + +Prices below are ordered `(mu_0,mu_1,mu_2;c_0,c_1,c_2)`. + +| Unique minimum | Positive prices | Value | Next smallest term | +| --- | --- | ---: | ---: | +| D | `(1,1,1;1,1,1)` | 3 | 5 | +| T_0 | `(1,3,3;1,1,1)` | 6 | 7 | +| R_01;2 | `(1,2,5;1,2,1)` | 6 | 7 | + +Row permutations expose all three T and all six R terms. A uniquely +minimizing term remains so in a neighborhood of its witness prices, so it +cannot be omitted from the formula. The verifier checks all permutations. + +The rank hypothesis is substantive. For the lower-rank demand `(e,h,e+h)` +in the **same R16**, the predecessor M word + + E_01(1), E_20(1), P_0(e+h), P_1(h), E_20(1), E_01(1) + +is correct and costs **14** at `(3,5,10;1,3,2)`, less than the present +formula's **15**. Its classes are dependent; the theorem does not apply. +The current three-generator target cannot use this cheaper word. + +## Finite evidence and reproduction + +`verify.py` is self-contained standard-library Python. Source files are +historical provenance, not runtime inputs. The coordinate ring interpreter +checks all commutative ring axioms, identifies the unique maximal ideal and +its square, and enumerates **every** ordered demand triple satisfying the +independence hypothesis in these three rings: + +| Ring | Size | Size of m | Size of m^2 | Accepted triples | +| --- | ---: | ---: | ---: | ---: | +| `F2[e,h,z]/(e,h,z)^2` | 16 | 8 | 1 | 168 | +| `F3[e,h,z]/(e,h,z)^2` | 81 | 27 | 1 | 11,232 | +| `(Z/4)[x,y]/(x,y)^2` | 64 | 32 | 4 | 10,752 | + +The first two counts are `|GL_3(F2)|=7*6*4` and +`|GL_3(F3)|=26*24*18`. In the third ring, `m=(2,x,y)` and +`m^2={0,2x,2y,2x+2y}`; there are `168*4^3` independent triples. +This last fixture tests the extension beyond square-zero maximal ideals. + +The checks cover 22,152 demands, 221,520 words and 1,772,160 formal +forward/inverse column evaluations. For the requested R16 demand they also +check all `16^4=65,536` scalar dirty/source inputs for each of ten words in +both directions: 1,310,720 literal evaluations. Eleven controls exercise +rank loss, a unit demand, nonlocality, missing dirty preparation, an +odd-characteristic sign error, omission of a necessary unit inverse, +the false per-edge return lemma and nonpositive prices. + +An independent implementation packs the complete `3 x 4` coefficient +matrix into 48 bits and uses bit arithmetic for R16. All 1,048,576 packed +coefficient/row products are compared with the coordinate implementation. +Bidirectional Dijkstra then permits every nonzero coefficient for every +one of the three insertion and six ADD locations: **135 neighbors per +state**, with no restriction on intermediate dirt, source support, unit +coefficients or gate patterns. It has no formula-derived cutoff or initial +upper bound. It stops only when its queue lower bound meets the best +complete path. Guards at 50,000 settled states and 1,000,000 combined +discovered states (checked before each expansion) raise an error rather +than certifying an unfinished search. Every returned path is replayed in +the coordinate interpreter and its bill is recomputed. + +The four price queries use `(1,1,1;1,1,1)`, `(1,10,10;10,1,1)`, +`(1,2,10;10,10,1)` and `(1/2,2/3,3/4;1,4/3,5/4)`. Their exact optima are +respectively `3`, `6`, `6` and `23/12`, covering strict D, T and R regimes +and nonintegral prices. +These queries corroborate the proof; they are not an exhaustive price scan +or the justification for the all-ring/all-real-price theorem. An exploratory +search at `(1/2,4/3,7/3;2/3,3/4,1/5)` was interrupted before certification; +another at `(1/2,1,5/2;1/2,1,2/3)` hit a resource guard. Neither is counted +as evidence. The registered cases use bounded representative prices. + +From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/r16-radical-triple-fanout --check-only +python3.12 -B scripts/research_package.py --package research/r16-radical-triple-fanout +``` + +`VERIFY.json` registers isolated, warning-strict normal and optimized +Python 3.12 executions. Direct exported-source replay is also supported: + +```sh +python3.12 -I -W error -B research/r16-radical-triple-fanout/verify.py +python3.12 -I -O -W error -B research/r16-radical-triple-fanout/verify.py +``` + +The script reports `PASS_R16_RADICAL_TRIPLE_FANOUT no_new_kappa` on success. +Checks use explicit exceptions, so `-O` does not disable them. + +Local validation used CPython 3.12.13 on macOS 26.7.1 (x86_64). Both +registered commands and metadata/source pins pass; one direct normal replay +took 11.83 seconds, a single-run observation rather than a benchmark. The +four search queries settled 8,465 entries in total. Three disposable +optimized-script mutations were rejected: charging a T word for only one +insertion, deleting its first dirty preparation, and replacing the required +unit inverse by 1. These checks do not require an installed solver or network. + +## Provenance, overlap and limits + +Base: canonical main `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, refreshed at +entry on 2026-10-29 UTC. Exact Git-blob and SHA256 pins are in `SOURCES.json`. +`TASK.json` retains priority revision 8 and the original `bit-helper-contract` +card, explicitly recording the donor-assigned algebraic scope change. +No random card was drawn or rerolled. + +The immediately preceding overlap snapshot completely paginated 328 open +PRs at 17:27 UTC and 5,940 Discussion/comment/reply records at 17:30 UTC. +Entry checks refreshed main, current coordination threads and all-state PR +searches for the nonprincipal/three-generator and e,h,z fanout problem. +At the 17:54 UTC submission checkpoint, canonical main remained unchanged; +the refreshed discussions/handoffs/fanout thread and all-state PR searches +found no updates since the snapshot and no same-scope result or active claim. +The local +note scan covered 42 packages and omitted 8,581 tracked notes in the sparse +checkout; it was not treated as a complete repository-history review. +This is a bounded project-overlap check, not a proof of global novelty. + +The source pins all resolve at the base commit, which is the direct parent +of this contribution. The optional full-history preflight is not claimed: +this is a shallow checkout. Hosted CI and independent review are separate +pending steps; no selected-operator, Lean, Docker or historical suite replay +is needed for this isolated five-file addition. + +The written lower bound requires mathematical review. Finite replay is not +proof-kernel verification, independent human approval or admission as a +multiplication supplier. This package does not settle directed-edge tariffs, +nonlocal rings, dependent demand classes, extra helpers or all unexposed +Pareto vectors. Applying a word physically requires pricing coefficients, +source access, routing, precision, stock and the full H2/K interface. The +selected frontier is unchanged and no new kappa is claimed. + +## Open next questions + +The structured questions are also recorded in `TASK.json`. + +1. Determine the **complete Pareto frontier** for the requested R16 demand. + The exact positive-price envelope can omit unexposed vectors. The first + unresolved branch is one unit insertion in each of two different rows: + classify which restoring count vectors are attainable, beginning with + `(P_i,P_j,P_k)=(1,1,0)` and `K=(2,2,2)`. Equation (2) settles their price + relevance but neither their existence nor componentwise minimality. +2. Determine the tariff with independently priced directed ADD edges. + This matters when two parents feeding the same row have different costs. + Begin with a cheap directed three-cycle and full dirt tracking. The + present incoming-row lemma loses edge information; the five-ADD identity + in the verifier rules out simply imposing two calls on every used edge. + +These are proposed follow-ups, not overlap reservations or claims of novelty. + +## Credit + +Prepared by lee-phys with substantial OpenAI Codex assistance in source +inspection, derivation, implementation, checking and writing. No subagents +or independent reviewers were used. Apache-2.0. + +The interpreter, count bookkeeping and bidirectional shortest-path method +adapt lee-phys #5259/#5514, pinned here; predecessors remain unchanged. +Credit Ali Romman #5266/#5310 for source-insertion feasibility, lee-phys +#5139/#5163/#5259 for ideal invariance, the local-ring boundary and the +non-zero-sum handoff, Nick Petalas #5208/#4916 for the equal-demand theorem +and ring-valued contract, Krzysztof Wojt #5045 for source-count classification +and two-row restoring words, Ross Richardson #3063/#3121 for tariff and +dirt-restoration arguments, and Cinna Davis, Anthony, Oscar Fennell, +Tekalign and the retained lineage. The new step is the independent-class +obstruction to nonunit two-insertion words, the two-root price comparison, +and the matching ten-term envelope over general commutative local rings. diff --git a/research/radical-fanout-inverse-tables/SOURCES.json b/research/radical-fanout-inverse-tables/SOURCES.json new file mode 100644 index 0000000000..75db18102e --- /dev/null +++ b/research/radical-fanout-inverse-tables/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/radical-fanout-inverse-tables/TASK.json b/research/radical-fanout-inverse-tables/TASK.json new file mode 100644 index 0000000000..c3e9078a39 --- /dev/null +++ b/research/radical-fanout-inverse-tables/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Precompute immutable additive and unit inverse tables in the complete PR6210 command, prove scoped equivalence, and measure unchanged complete replays.", + "scope_change_reason": "Select one complete radical-fanout replay and preserve its entire finite workload. This is verifier engineering, not a new tariff or an audit.", + "bottleneck_link": "Remove repeated finite-ring inverse scans without dropping checks, so complete mechanism replays require less interpreter work.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact work reduction with unchanged complete output. Do not extend the mathematical tariff or optimize other paths.", + "outcome": "completed", + "evidence": "Full-command tuple.index count decreases from 1661695 to 260; all complete stdout is identical. 322 index cases and 16 controls pass. Ten alternating full-command pairs have zero errors; wall-time comparison remains inconclusive because timing ranges overlap.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the unchanged complete command show a stable wall-time gain on an idle Linux CPython 3.12 host?", + "why_it_matters": "The exact repeated-search reduction is portable; elapsed-time gains depend on the host and remaining interpreter work.", + "first_step": "Run benchmark.py for at least five alternating pairs, preserving all output digests, and report medians and ranges.", + "blocked_by": "An additional host measurement; no missing executable dependency." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279673", + "source_pr": 6210, + "source_author": "lee-phys", + "source_head": "4e08457f4d0b69c00a6ca62eca81c8d0a55f3e60" + } +} diff --git a/research/radical-fanout-inverse-tables/UPSTREAM.json b/research/radical-fanout-inverse-tables/UPSTREAM.json new file mode 100644 index 0000000000..4d4251f58c --- /dev/null +++ b/research/radical-fanout-inverse-tables/UPSTREAM.json @@ -0,0 +1,22 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "pull_request": 6210, + "commit": "4e08457f4d0b69c00a6ca62eca81c8d0a55f3e60", + "author": "lee-phys", + "files": [ + { + "retained": "retained_source.py", + "path": "research/r16-radical-triple-fanout/verify.py", + "git_blob": "5e5ebe9ce3cd8b6e8e24f803eb4b7e30daa14ab9", + "sha256": "f2f4b7f8cfb900488af2ac86202fa2a177279c97302cc6d84a64135b157e2b3c", + "bytes": 14921 + }, + { + "retained": "SOURCE-README.md", + "path": "research/r16-radical-triple-fanout/README.md", + "git_blob": "a122a5de58e72d9b126fe6bf3085c3852813d204", + "sha256": "291eef5b1b08c1560660cdc9ac6891274477a2f0c9b505c22f66c986abbad3f9", + "bytes": 18181 + } + ] +} diff --git a/research/radical-fanout-inverse-tables/VERIFY.json b/research/radical-fanout-inverse-tables/VERIFY.json new file mode 100644 index 0000000000..1bb074adac --- /dev/null +++ b/research/radical-fanout-inverse-tables/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact inverse/exception conformance, full-command stdout equality, full-workload tuple.index counts and corrupt-source rejection." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same conformance, work counts and rejection checks with assertions disabled." + } + ] +} diff --git a/research/radical-fanout-inverse-tables/benchmark.py b/research/radical-fanout-inverse-tables/benchmark.py new file mode 100644 index 0000000000..093d0b72f9 --- /dev/null +++ b/research/radical-fanout-inverse-tables/benchmark.py @@ -0,0 +1,52 @@ +"""Alternating complete-command measurements, produced by Nick Petalas.""" + +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import statistics +import sys +import time + +from verify import authenticate, execute, require + + +HERE = Path(__file__).resolve().parent + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--rounds', type=int, choices=range(5, 11), default=5) + args = parser.parse_args() + authenticate() + samples, expected = [], None + for iteration in range(args.rounds): + for name in ('retained_source.py', 'fast.py'): + start = time.perf_counter() + result = execute(HERE / name) + elapsed = time.perf_counter()-start + require(result.returncode == 0 and not result.stderr, 'measured command failed') + if expected is None: + expected = result.stdout + require(result.stdout == expected, 'measured complete output changed') + require(result.stdout.endswith(b'PASS_R16_RADICAL_TRIPLE_FANOUT no_new_kappa\n'), + 'measured workload did not finish') + samples.append(dict(engine=name, round=iteration+1, wall_seconds=elapsed, + stdout_sha256=hashlib.sha256(result.stdout).hexdigest())) + summary = {} + for name in ('retained_source.py', 'fast.py'): + values = [s['wall_seconds'] for s in samples if s['engine'] == name] + summary[name] = dict(median=statistics.median(values), minimum=min(values), + maximum=max(values)) + report = dict(samples=samples, summary=summary, errors=0, python=sys.version, + platform=platform.platform(), cpu_count=os.cpu_count(), + stdout_equal=True, load_average=os.getloadavg(), + source_sha256=hashlib.sha256((HERE/'retained_source.py').read_bytes()).hexdigest(), + fast_sha256=hashlib.sha256((HERE/'fast.py').read_bytes()).hexdigest()) + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/radical-fanout-inverse-tables/fast.py b/research/radical-fanout-inverse-tables/fast.py new file mode 100644 index 0000000000..3ba5bc2f8e --- /dev/null +++ b/research/radical-fanout-inverse-tables/fast.py @@ -0,0 +1,57 @@ +"""Static inverse tables for the retained complete fanout command. + +Inverse-table changes produced by Nick Petalas. Apache-2.0. +The theorem, interpreter, search and enumerated workload remain lee-phys's. +""" + +from dataclasses import dataclass, field +import hashlib +from pathlib import Path + + +SOURCE_SHA256 = 'f2f4b7f8cfb900488af2ac86202fa2a177279c97302cc6d84a64135b157e2b3c' +source_path = Path(__file__).with_name('retained_source.py') +if hashlib.sha256(source_path.read_bytes()).hexdigest() != SOURCE_SHA256: + raise ValueError('retained executable source bytes changed') + +import retained_source as source # Authenticate before importing executable bytes. + + +@dataclass(frozen=True) +class InverseTableRing(source.Ring): + """Keep one immutable answer per element, including the nonunit sentinel.""" + + _neg: tuple = field(init=False, repr=False, compare=False) + _inv: tuple = field(init=False, repr=False, compare=False) + + def __post_init__(self): + if not 1 <= self.n <= 81: + raise ValueError('supported ring order is 1 through 81') + if len(self.add) != self.n or len(self.mul) != self.n: + raise ValueError('one addition and multiplication row per element') + if any(len(row) != self.n for row in (*self.add, *self.mul)): + raise ValueError('square operation tables required') + negatives = tuple(row.index(0) for row in self.add) + units = tuple(row.index(self.one) if self.one in row else None + for row in self.mul) + object.__setattr__(self, '_neg', negatives) + object.__setattr__(self, '_inv', units) + + def neg(self, x): + return self._neg[x] + + def inv(self, x): + value = self._inv[x] + if value is None: + return self.mul[x].index(self.one) + return value + + +def main(): + # One explicit factory boundary; no workload, check or search is replaced. + source.Ring = InverseTableRing + source.main() + + +if __name__ == '__main__': + main() diff --git a/research/radical-fanout-inverse-tables/retained_source.py b/research/radical-fanout-inverse-tables/retained_source.py new file mode 100644 index 0000000000..5e5ebe9ce3 --- /dev/null +++ b/research/radical-fanout-inverse-tables/retained_source.py @@ -0,0 +1,380 @@ +#!/usr/bin/env python3 +"""Bounded exact corroboration of README.md; no new kappa. + +lee-phys, with substantial OpenAI Codex assistance; Apache-2.0. +The ring interpreter and bidirectional search adapt the credited #5259/#5514 +verifiers. No predecessor package is imported or needed at runtime. +""" +from dataclasses import dataclass +from fractions import Fraction +from heapq import heappop, heappush +from itertools import permutations, product +from math import lcm +import json + + +def require(test, message): + if not test: + raise RuntimeError(message) + + +@dataclass(frozen=True) +class Ring: + name: str + n: int + one: int + add: tuple + mul: tuple + + def neg(self, x): + return self.add[x].index(0) + + def inv(self, x): + return self.mul[x].index(self.one) + + +def ring_from_functions(name, n, one, add, mul): + return Ring(name, n, one, + tuple(tuple(add(x, y) for y in range(n)) for x in range(n)), + tuple(tuple(mul(x, y) for y in range(n)) for x in range(n))) + + +def truncated_polynomials(modulus, variables): + # Constant plus independent variables, with every variable product zero. + # Modulus 4 retains 2*x != 0 and a non-square-zero maximal ideal. + width = variables+1 + + def digits(x): + return tuple((x//modulus**k) % modulus for k in range(width)) + + def add(x, y): + a, b = digits(x), digits(y) + return sum(((a[k]+b[k]) % modulus)*modulus**k for k in range(width)) + + def mul(x, y): + a, b = digits(x), digits(y) + return (a[0]*b[0]) % modulus + sum( + ((a[0]*b[k]+a[k]*b[0]) % modulus)*modulus**k for k in range(1, width)) + + return ring_from_functions(f'Z/{modulus}[{variables} variables]/(variables)^2', + modulus**width, 1, add, mul) + + +def check_ring(r): + es = range(r.n) + require(r.one != 0, 'nonzero ring') + for a, b in product(es, repeat=2): + require(r.add[a][b] in es and r.mul[a][b] in es, 'closure') + require(r.add[a][b] == r.add[b][a] and r.mul[a][b] == r.mul[b][a], 'commutativity') + for a in es: + require(r.add[a][0] == a and r.mul[a][r.one] == a and r.mul[a][0] == 0, 'identities') + require(r.add[a][r.neg(a)] == 0, 'additive inverse') + for a, b, c in product(es, repeat=3): + require(r.add[r.add[a][b]][c] == r.add[a][r.add[b][c]], 'addition associativity') + require(r.mul[r.mul[a][b]][c] == r.mul[a][r.mul[b][c]], 'multiplication associativity') + require(r.mul[a][r.add[b][c]] == r.add[r.mul[a][b]][r.mul[a][c]], 'distributivity') + + +def local_data(r): + radical = tuple(x for x in range(r.n) if r.one not in r.mul[x]) + m = set(radical) + if r.one in m or any(r.add[x][y] not in m for x in m for y in m) or any( + r.mul[x][y] not in m for x in m for y in range(r.n)): + raise ValueError('the finite ring must be local') + generators = {r.mul[x][y] for x in m for y in m} + square = {0} + for g in generators: + principal = {r.mul[a][g] for a in range(r.n)} + square = {r.add[x][y] for x in square for y in principal} + covered, representatives = set(), [] + for x in range(r.n): + if x not in covered: + representatives.append(x) + covered.update(r.add[x][y] for y in m) + return radical, frozenset(square), tuple(representatives) + + +def validate_demand(r, d, data): + m, square, representatives = data + if len(d) != 3 or any(x not in m for x in d): + raise ValueError('three demands in the maximal ideal required') + for coefficients in product(representatives, repeat=3): + if coefficients == (0, 0, 0): + continue + value = 0 + for a, x in zip(coefficients, d): + value = r.add[value][r.mul[a][x]] + if value in square: + raise ValueError('demand classes must be independent modulo m^2') + + +def formula(mu, c): + if len(mu) != 3 or len(c) != 3 or min((*mu, *c)) <= 0: + raise ValueError('six strictly positive prices required') + values = [sum(mu)] + for k in range(3): + i, j = [r for r in range(3) if r != k] + values.append(2*mu[k]+2*c[i]+2*c[j]) + values.append(mu[i]+mu[j]+min(mu[i], mu[j])+2*c[k]) + return min(values) + + +def patterns(): + out = [('D', 0, 1, 2, (1, 1, 1, 0, 0, 0))] + for i in range(3): + j, k = [r for r in range(3) if r != i] + v = [0]*6 + v[i], v[3+j], v[3+k] = 2, 2, 2 + out.append(('T', i, j, k, tuple(v))) + for i, j, k in permutations(range(3)): + v = [0]*6 + v[i], v[j], v[3+k] = 2, 1, 2 + out.append(('R', i, j, k, tuple(v))) + return out + + +def construct(r, d, pattern): + mode, i, j, k, _ = pattern + if mode == 'D': + return [(t, 3, d[t]) for t in range(3)] + u = r.add[d[i]][r.neg(r.one)] + if mode == 'T': + a = r.mul[d[k]][r.inv(u)] + return [(j, i, r.neg(d[j])), (i, 3, r.one), (j, i, d[j]), + (k, i, r.neg(a)), (i, 3, u), (k, i, a)] + if mode == 'R': + return [(k, i, r.neg(d[k])), (i, 3, r.one), (k, i, d[k]), + (i, 3, u), (j, 3, d[j])] + raise ValueError('unknown construction') + + +def inverse(r, word): + return [(i, j, r.neg(a)) for i, j, a in reversed(word)] + + +def execute(r, word, entry): + out = list(entry) + for i, j, a in word: + out[i] = r.add[out[i]][r.mul[a][out[j]]] + return tuple(out) + + +def target(r, d, entry): + return tuple(r.add[entry[i]][r.mul[d[i]][entry[3]]] for i in range(3))+(entry[3],) + + +def endpoint(r, d, word): + rev = inverse(r, word) + for k in range(4): + entry = tuple(r.one if j == k else 0 for j in range(4)) + want = target(r, d, entry) + if execute(r, word, entry) != want or execute(r, rev, want) != entry: + return False + return True + + +def counts(word): + return tuple(sum(i == k and j == 3 for i, j, _ in word) for k in range(3))+tuple( + sum(i == k and j != 3 for i, j, _ in word) for k in range(3)) + + +def bill(word, prices): + return sum(prices[i if j == 3 else 3+i] for i, j, _ in word) + + +# Independent R16 arithmetic: four 4-bit coefficients per 16-bit row. +# Multiplying the constant-bit mask by a radical digit cannot carry across +# 4-bit lanes. No coordinate ring tables, constructors or formula are used. +def packed_product(a, row): + return (row if a & 1 else 0) ^ ((a & 14)*(row & 0x1111)) + + +def neighbors(state, weights): + rows = [(state >> (16*i)) & 65535 for i in range(3)] + for i in range(3): + for a in range(1, 16): + yield state ^ (a << (16*i+12)), weights[i], (i, 3, a) + for j in range(3): + if j != i: + for a in range(1, 16): + yield state ^ (packed_product(a, rows[j]) << (16*i)), weights[3+i], (i, j, a) + + +def oracle(demand, prices): + scale = lcm(*(Fraction(x).denominator for x in prices)) + weights = tuple(int(Fraction(x)*scale) for x in prices) + require(min(weights) > 0, 'positive oracle weights') + start = 1 | (16 << 16) | (256 << 32) + goal = start | sum(x << (16*i+12) for i, x in enumerate(demand)) + ds = [{start: 0}, {goal: 0}] + qs = [[(0, start)], [(0, goal)]] + ps = [{start: None}, {goal: None}] + best, meet = None, None + settled = [0, 0] + while qs[0] and qs[1]: + for s in (0, 1): + while qs[s] and qs[s][0][0] != ds[s][qs[s][0][1]]: + heappop(qs[s]) + if not qs[0] or not qs[1]: + break + if best is not None and qs[0][0][0]+qs[1][0][0] >= best: + break + s = int(qs[1][0][0] < qs[0][0][0]) + du, u = heappop(qs[s]) + settled[s] += 1 + require(sum(settled) <= 50000 and len(ds[0])+len(ds[1]) <= 1000000, + 'oracle resource guard; query not certified') + for v, cost, gate in neighbors(u, weights): + dv = du+cost + if v not in ds[s] or dv < ds[s][v]: + ds[s][v] = dv + ps[s][v] = (u, gate) + heappush(qs[s], (dv, v)) + if v in ds[1-s]: + candidate = dv+ds[1-s][v] + if best is None or candidate < best: + best, meet = candidate, v + require(meet is not None, 'oracle endpoints disconnected') + forward, back = [], [] + u = meet + while ps[0][u] is not None: + u, gate = ps[0][u] + forward.append(gate) + u = meet + while ps[1][u] is not None: + u, gate = ps[1][u] + back.append(gate) # All nonzero-coefficient primitives are involutions here. + return Fraction(best, scale), list(reversed(forward))+back, settled + + +def main(): + r16, r81, r64 = truncated_polynomials(2, 3), truncated_polynomials(3, 3), truncated_polynomials(4, 2) + pats = patterns() + vectors = [p[-1] for p in pats] + require(len(vectors) == len(set(vectors)) == 10, 'ten distinct envelope vectors') + total = dict(demands=0, words=0, formal_forward_inverse=0, literal_forward_inverse=0, + exposed_vectors=0, controls=0, oracle_queries=0, oracle_settled=0) + fixtures = [] + for r, expected in ((r16, 168), (r81, 11232), (r64, 10752)): + check_ring(r) + data = local_data(r) + accepted = 0 + for d in product(data[0], repeat=3): + try: + validate_demand(r, d, data) + except ValueError: + continue + accepted += 1 + for pat in pats: + word = construct(r, d, pat) + require(all(a != 0 and i != j for i, j, a in word), 'nonzero legal gates') + require(endpoint(r, d, word), 'constructed dirt endpoint/inverse') + require(counts(word) == pat[-1], 'claimed counts') + total['words'] += 1 + total['formal_forward_inverse'] += 8 + require(accepted == expected, 'exhaustive independent-class triple count') + total['demands'] += accepted + fixtures.append(dict(ring=r.name, independent_triples=accepted, maximal_ideal=len(data[0]), + square_ideal=len(data[1]), residue_field=len(data[2]))) + print('CHECK_RING', r.n, accepted, flush=True) + + d = (2, 4, 14) + words = [construct(r16, d, p) for p in pats] + for word in words: + rev = inverse(r16, word) + for entry in product(range(16), repeat=4): + want = target(r16, d, entry) + require(execute(r16, word, entry) == want and execute(r16, rev, want) == entry, + 'literal R16 forward/inverse') + total['literal_forward_inverse'] += 2 + + representative_prices = [(1,1,1,1,1,1), (1,3,3,1,1,1), (1,2,5,1,2,1)] + exposed = set() + for prices in representative_prices: + for perm in permutations(range(3)): + p = tuple(prices[i] for i in perm)+tuple(prices[3+i] for i in perm) + costs = [bill(word, p) for word in words] + minimum = min(costs) + require(costs.count(minimum) == 1, 'strict positive-price exposure') + require(minimum == formula(p[:3], p[3:]), 'compressed envelope') + exposed.add(costs.index(minimum)) + require(len(exposed) == 10, 'all ten terms strictly exposed') + total['exposed_vectors'] = len(exposed) + for mu, c in product(range(1, 13), repeat=2): + require(formula((mu,)*3, (c,)*3) == min(3*mu, 2*mu+4*c), 'uniform-price specialization') + + # The lower rank zero-sum triple admits a cheaper predecessor M word. + rank_two = (2,4,6) + old_word = [(0,1,1), (2,0,1), (0,3,6), (1,3,4), (2,0,1), (0,1,1)] + prices = (3,5,10,1,3,2) + require(endpoint(r16, rank_two, old_word), 'rank-two predecessor word') + require(bill(old_word, prices) == 14 < formula(prices[:3], prices[3:]) == 15, + 'rank-three hypothesis is essential') + total['controls'] += 1 + for bad, fragment in [((0,4,14), 'independent'), (rank_two, 'independent'), + ((1,4,14), 'maximal ideal')]: + try: + validate_demand(r16, bad, local_data(r16)) + except ValueError as error: + require(fragment in str(error), 'correct hypothesis rejection') + total['controls'] += 1 + else: + raise RuntimeError('accepted demand outside theorem') + nonlocal_ring = ring_from_functions('F2 x F2', 4, 3, lambda x,y: x ^ y, lambda x,y: x & y) + check_ring(nonlocal_ring) + try: + local_data(nonlocal_ring) + except ValueError: + total['controls'] += 1 + else: + raise RuntimeError('accepted nonlocal ring') + corrupt = words[1][1:] + require(execute(r16, corrupt, (0,0,0,1)) == (*d,1), 'dirty-only corruption premise') + require(not endpoint(r16, d, corrupt), 'missing preparation must fail on dirt') + total['controls'] += 1 + d81 = (3,9,39) + bad_sign = construct(r81, d81, pats[1]) + i, j, a = bad_sign[0] + bad_sign[0] = (i, j, r81.neg(a)) + require(not endpoint(r81, d81, bad_sign), 'odd-characteristic sign control') + total['controls'] += 1 + d64 = (4,2,22) + bad_inverse = construct(r64, d64, pats[1]) + bad_inverse[3], bad_inverse[5] = (2,0,r64.neg(d64[2])), (2,0,d64[2]) + require(not endpoint(r64, d64, bad_inverse), 'unit inverse is necessary when m^2 is nonzero') + total['controls'] += 1 + relator = [(0,1,1), (1,2,1), (0,1,1), (1,2,1), (0,2,1)] + require(endpoint(r16, (0,0,0), relator), 'three-row identity control') + require(sum((i,j) == (0,2) for i,j,_ in relator) == 1, 'row-return lemma is not per edge') + total['controls'] += 1 + for bad_prices in [(0,1,1,1,1,1), (1,1,1,-1,1,1)]: + try: + formula(bad_prices[:3], bad_prices[3:]) + except ValueError: + total['controls'] += 1 + else: + raise RuntimeError('accepted nonpositive prices') + + for a in range(16): + for row in range(65536): + expected = sum(r16.mul[a][(row >> (4*k)) & 15] << (4*k) for k in range(4)) + require(packed_product(a, row) == expected, 'independent packed arithmetic') + cases = [('D', (1,1,1,1,1,1)), ('T', (1,10,10,10,1,1)), + ('R', (1,2,10,10,10,1)), + ('rational', (Fraction(1,2),Fraction(2,3),Fraction(3,4), + Fraction(1),Fraction(4,3),Fraction(5,4)))] + results = [] + for name, prices in cases: + value, path, settled = oracle(d, prices) + require(value == formula(prices[:3], prices[3:]), f'oracle mismatch: {name}') + require(endpoint(r16, d, path) and bill(path, prices) == value, 'oracle path replay and bill') + total['oracle_queries'] += 1 + total['oracle_settled'] += sum(settled) + results.append(dict(case=name, optimum=str(value), settled=settled)) + print('CHECK_ORACLE', name, str(value), settled, flush=True) + print(json.dumps(dict(fixtures=fixtures, counts=total, oracle=results), sort_keys=True)) + print('PASS_R16_RADICAL_TRIPLE_FANOUT no_new_kappa') + + +if __name__ == '__main__': + main() diff --git a/research/radical-fanout-inverse-tables/verify.py b/research/radical-fanout-inverse-tables/verify.py new file mode 100644 index 0000000000..690e9f2160 --- /dev/null +++ b/research/radical-fanout-inverse-tables/verify.py @@ -0,0 +1,148 @@ +"""Inverse-table conformance and full-command equality, produced by Nick Petalas.""" + +import contextlib +import cProfile +import hashlib +import io +import json +import os +from pathlib import Path +import pstats +import subprocess +import sys +import tempfile + + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + provenance = json.loads((HERE / 'UPSTREAM.json').read_text()) + require(provenance['pull_request'] == 6210, 'wrong predecessor') + require(len(provenance['files']) == 2, 'two retained source files') + for row in provenance['files']: + path = HERE / row['retained'] + require(path.parent == HERE, 'local source path') + data = path.read_bytes() + require(len(data) == row['bytes'], 'source length changed') + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'source changed') + + +def observed(call, argument): + try: + return ('value', call(argument)) + except (IndexError, ValueError) as error: + return (type(error).__name__, str(error)) + + +def conformance(): + import fast + source = fast.source + elements = controls = 0 + for modulus, variables in ((2, 3), (3, 3), (4, 2)): + ring = source.truncated_polynomials(modulus, variables) + cached = fast.InverseTableRing(ring.name, ring.n, ring.one, ring.add, ring.mul) + for x in range(-ring.n, ring.n): + require(observed(ring.neg, x) == observed(cached.neg, x), 'negative table') + require(observed(ring.inv, x) == observed(cached.inv, x), 'unit table') + elements += 1 + for x in (-ring.n-1, ring.n): + require(observed(ring.neg, x) == observed(cached.neg, x), 'neg index error') + require(observed(ring.inv, x) == observed(cached.inv, x), 'inv index error') + controls += 2 + require(cached._neg[cached._neg[ring.one]] == ring.one, 'negation involution') + tiny = source.truncated_polynomials(2, 1) + for n, add, mul in ((82, tiny.add, tiny.mul), (4, (), tiny.mul), + (4, tiny.add, tuple(row[:-1] for row in tiny.mul))): + try: + fast.InverseTableRing('invalid', n, tiny.one, add, mul) + except ValueError: + controls += 1 + else: + raise ValueError('invalid table accepted') + return elements, controls + + +def execute(script, cwd=HERE): + env = dict(os.environ) + env.pop('PYTHONOPTIMIZE', None) + env.pop('PYTHONPATH', None) + scratch = env.get('IMB_RUN_ROOT') + with tempfile.TemporaryDirectory(prefix='inverse-table-bytecode-', dir=scratch) as cache: + command = [sys.executable, '-W', 'error', '-B', '-X', 'pycache_prefix='+cache] + if sys.flags.optimize: + command.append('-O') + command.append(str(script)) + return subprocess.run(command, cwd=cwd, env=env, capture_output=True, timeout=120) + + +def corruption_control(): + scratch = os.environ.get('IMB_RUN_ROOT') + with tempfile.TemporaryDirectory(prefix='inverse-table-control-', dir=scratch) as directory: + root = Path(directory) + for name in ('fast.py', 'retained_source.py'): + (root / name).write_bytes((HERE / name).read_bytes()) + with (root / 'retained_source.py').open('ab') as stream: + stream.write(b'\nraise RuntimeError("executed corrupt source")\n') + result = execute(root / 'fast.py', root) + require(result.returncode != 0, 'changed source accepted') + require(b'retained executable source bytes changed' in result.stderr, + 'source must reject before import') + require(b'executed corrupt source' not in result.stderr, 'corrupt source executed') + + +def profiled_call(entry): + output = io.StringIO() + profile = cProfile.Profile() + with contextlib.redirect_stdout(output): + profile.runcall(entry) + stats = pstats.Stats(profile).stats + matches = [value[1] for key, value in stats.items() + if key[2] == ""] + require(len(matches) == 1, 'CPython tuple-index counter unavailable') + return output.getvalue(), matches[0] + + +def search_reduction(expected): + import fast + original_class = fast.source.Ring + try: + before, before_searches = profiled_call(fast.source.main) + after, after_searches = profiled_call(fast.main) + finally: + fast.source.Ring = original_class + require(before.encode() == after.encode() == expected, 'profiled workload changed') + require(0 < after_searches < before_searches, 'no exact search-count improvement') + return dict(before=before_searches, after=after_searches) + + +def main(): + authenticate() + elements, controls = conformance() + baseline = execute(HERE / 'retained_source.py') + optimized = execute(HERE / 'fast.py') + for result in (baseline, optimized): + require(result.returncode == 0 and not result.stderr, 'complete command failed') + require(baseline.stdout == optimized.stdout, 'complete stdout differs') + require(baseline.stdout.endswith(b'PASS_R16_RADICAL_TRIPLE_FANOUT no_new_kappa\n'), + 'complete workload did not finish') + corruption_control() + searches = search_reduction(baseline.stdout) + files = tuple(p for p in sorted(HERE.iterdir()) if p.is_file()) + require(len(files) <= 16, 'bounded local package inventory') + receipt = dict(status='PASS_RADICAL_FANOUT_INVERSE_TABLES', elements=elements, + controls=controls+1, complete_commands=2, + profiled_complete_workloads=2, tuple_index_searches=searches, + stdout_sha256=hashlib.sha256(baseline.stdout).hexdigest(), + package_hashes={p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in files}) + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == '__main__': + main()