Skip to content

Accelerate exact mixed-point construction 1.51× (no new κ) #6007

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 28, 2026
Merged

Accelerate exact mixed-point construction 1.51× (no new κ) #6007

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
267 changes: 267 additions & 0 deletions research/mixed-point-support-interning/BENCHMARK.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,267 @@
{
"complete_process": {
"baseline": {
"maximum": 4.690894667059183,
"median": 4.538428250001743,
"minimum": 4.469825042062439
},
"candidate": {
"maximum": 3.5410334169864655,
"median": 3.440444082953036,
"minimum": 3.104844499961473
},
"reduction": 0.24193048927198213,
"speedup": 1.319140244856494
},
"construction": {
"baseline": {
"maximum": 3.489661291008815,
"median": 3.3839167499681935,
"minimum": 3.335645416053012
},
"candidate": {
"maximum": 2.345284124952741,
"median": 2.2460121660260484,
"minimum": 1.9319452090421692
},
"reduction": 0.33626849240686574,
"speedup": 1.5066333126571978
},
"environment": {
"cpu_count": 18,
"executable": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
"load": [
3.74951171875,
3.5302734375,
2.71533203125
],
"platform": "macOS-27.0.1-arm64-arm-64bit",
"python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]"
},
"errors": 0,
"samples": [
{
"active": 509194,
"additions": 489594,
"build_seconds": 3.489661291008815,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.9058362920768559,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2037841920,
"process_seconds": 4.690894667059183,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "baseline",
"verify_seconds": 0.05716524994932115
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 2.2460121660260484,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.9801619159989059,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2138570752,
"process_seconds": 3.5410334169864655,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "candidate",
"verify_seconds": 0.056872959015890956
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 3.3357087079202756,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.868792959023267,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2036137984,
"process_seconds": 4.4883591659599915,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "baseline",
"verify_seconds": 0.056672625010833144
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 2.345284124952741,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.8810744578950107,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2139553792,
"process_seconds": 3.5308248749934137,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "candidate",
"verify_seconds": 0.06221175007522106
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 3.3839167499681935,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.8667492909589782,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2039922688,
"process_seconds": 4.538428250001743,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "baseline",
"verify_seconds": 0.059838084038347006
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 2.269305207999423,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.8623156249523163,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2140405760,
"process_seconds": 3.440444082953036,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "candidate",
"verify_seconds": 0.05716758407652378
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 3.335645416053012,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.861448916955851,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2033614848,
"process_seconds": 4.469825042062439,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "baseline",
"verify_seconds": 0.05315654200967401
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 2.068434457993135,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.8721394590102136,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2136653824,
"process_seconds": 3.374925334006548,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "candidate",
"verify_seconds": 0.06760345795191824
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 3.4270764999091625,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.9830873750615865,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2036924416,
"process_seconds": 4.68306275003124,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "baseline",
"verify_seconds": 0.0630757090402767
},
{
"active": 509194,
"additions": 489594,
"build_seconds": 1.9319452090421692,
"case": [
50,
3,
3,
1,
1
],
"digest_seconds": 0.8540269579971209,
"errors": 0,
"factored": false,
"nodes": 509195,
"peak_rss_native_units": 2137964544,
"process_seconds": 3.104844499961473,
"signature": "216a04c7a7fb08be0f5951bb4e13ec06f251fa03ac99dd96e9c4fa689c2ed4bf",
"variant": "candidate",
"verify_seconds": 0.052203333005309105
}
],
"schema_version": 1,
"source_sha256": {
"baseline/certify.py": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e",
"baseline/exclusion_circuit.py": "f9fbcd6e85e442cbd0926ac0887414e20735b2dc923d2d5822c803ceb46726d3",
"baseline/mixed_point_circuit.py": "cc98eeada267814fa2c0bc5f3ebb844f614d667c74d16d80d7ef29b1f90e0aa5",
"baseline/paired_exclusion_circuit.py": "8f05f04cf06217befd6d0ee0f2d7d0c5c5eb32cfab8c9a8ca7917fd6d620b7d2",
"benchmark.py": "3d5515387aed41d3a165d6ac23ee41295d1ed922fc92b5f2cda47e9e1298801b",
"candidate/exclusion_circuit.py": "f029e7a91f125f4ce7fdad3ed8f86e1fd7ca705540d4b15b644bdf6819eed894",
"candidate/interning.py": "b4376a824060cad5376dd25bc8e38908d539a624fd76beaa8fd5ffddbcf0855c",
"candidate/mixed_point_circuit.py": "6d37b7d79506c7a5739712650a44890eb54f1188a04bdc6ec39a21090f852788",
"run_builder.py": "c156735096aaa7d6be1a04258e29317a339c6e44d2d7b78022d67dffd1f8f89f"
},
"workload": "build(50,3,3,1,common=True)"
}
44 changes: 44 additions & 0 deletions research/mixed-point-support-interning/ENGINEERING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
# Verification boundaries

Playbook: performance issue. The measured question is complete construction
of the unchanged hybrid mixed-point fixture. A diagnostic profile identifies
large-support interning. One compact-key mechanism was tested, then frozen at
the first exact structural gain. Five alternating fresh-process pairs include
every sample, the unchanged full output check and complete structural hashing.
No predecessor mathematical audit or wider construction search is a deliverable.

Build the Lever shaped the result by retaining an opt-in builder, an exact
oracle and a reproducible benchmark instead of a timing-only note. Prove It
Works shaped the result by comparing full small DAGs and every large DAG field,
and by forcing key collisions. Explain the Number shaped the result by reporting
the whole process as well as construction, profiling outside measurements and
retaining memory costs and sample ranges.

The new interner is iterative. Its scans are bounded by the input/node caps;
the fixed verifier has 28 oracle cases, 16 builder pairs and eight controls.
CLI parameters, full-output size, subprocess timeouts and sample counts have
explicit bounds. Each sample waits for the complete child and checks its exit
status, stderr, output, work count and signature. Output files use exclusive
creation. Runtime errors propagate to a failing command; no retry hides them.

Python allocations are a managed-runtime deviation from fixed allocation.
Inputs and nodes have explicit caps; no constant-space claim is made. Peak RSS
is measured for each serial sample. No new function uses recursion, reflection,
dynamic source execution or generated executable code. Imports select two fixed
source directories. The verifier's string replacements only check the declared
adapter diff; they do not execute generated code. The original frozen builder
retains recursive summation and planning. This is an explicit inherited-code
deviation; the CLI bounds n by 50 and support count by 25,000, and no recursion
or algorithm in those sources is changed.

New functions use ordinary structured exits and remain within about one page.
The bucket invariant, complete-support match, first-decomposition oracle and
unchanged caller structure are executable checks. New overlap and boundary
guards remain enabled under optimized Python. Existing baseline assertions
are retained byte for byte; optimized replay does not claim they remain active.

Warning-strict normal and optimized runs cover the real artifact and all
registered checks. No project-wide analyzer configuration or shared code is
changed. Frozen source retains its existing formatting and diagnostics. This
is a scoped engineering result, not a claim that every historical source
complies with these implementation rules.
25 changes: 25 additions & 0 deletions research/mixed-point-support-interning/PROFILE.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
elapsed 5.202703042072244 nodes 509195 active 509194 adds 489594
27705499 function calls (25084876 primitive calls) in 5.202 seconds

Ordered by: internal time
List reduced from 41 to 18 due to restriction <18>

ncalls tottime percall cumtime percall filename:lineno(function)
2371564 2.087 0.000 2.254 0.000 exclusion_circuit.py:31(add)
2814596/520348 0.491 0.000 1.578 0.000 exclusion_circuit.py:41(total)
363 0.398 0.001 0.398 0.001 mixed_point_circuit.py:20(__init__)
363 0.372 0.001 0.731 0.002 mixed_point_circuit.py:32(finish)
135 0.279 0.002 1.973 0.015 mixed_point_circuit.py:115(transpose)
229172 0.172 0.000 0.365 0.000 mixed_point_circuit.py:92(output)
6215991 0.167 0.000 0.167 0.000 {built-in method builtins.len}
3780256 0.158 0.000 0.158 0.000 {method 'append' of 'list' objects}
344957/19545 0.134 0.000 0.517 0.000 mixed_point_circuit.py:103(avoid)
3514290 0.124 0.000 0.124 0.000 {method 'pop' of 'list' objects}
827/1 0.105 0.000 3.602 3.602 mixed_point_circuit.py:147(plan)
1912629 0.083 0.000 0.083 0.000 {method 'add' of 'set' objects}
1601664 0.074 0.000 0.074 0.000 {method 'extend' of 'list' objects}
2/1 0.058 0.029 5.202 5.202 mixed_point_circuit.py:181(build)
408 0.056 0.000 0.109 0.000 {built-in method builtins.sum}
50 0.049 0.001 1.101 0.022 mixed_point_circuit.py:47(apply)
1735930 0.048 0.000 0.048 0.000 mixed_point_circuit.py:44(<genexpr>)
45 0.046 0.001 0.267 0.006 exclusion_circuit.py:13(__init__)
52 changes: 52 additions & 0 deletions research/mixed-point-support-interning/PROOF.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
# Exact first-decomposition preservation

Consider a finite sequence of additions on independent input basis supports.
Node 0 has empty support. Input node `j+1` has support `{j}`. A valid addition
has two previously allocated node IDs whose supports are disjoint. The original
rule returns either operand when the other is zero. Otherwise it returns the
first node with the union support, or appends a node with that support and
the ordered argument pair. Assume the declared capacity is not exceeded.

Choose arbitrary bit strings `h_j` of one fixed width, including width zero.
For a support `S`, define `h(S)` as the XOR of `h_j` for `j in S`. Disjointness
gives `h(A union B) = h(A) XOR h(B)`. This identity requires no randomness and
no injectivity assumption.

Maintain a bucket for each key, containing exactly the allocated node IDs with
that key. Initialization establishes this invariant. On an addition, the new
rule computes the full union support and its XOR key. A prior node with equal
support necessarily has that key and is in that bucket. The bucket search
compares full supports, so it finds that node. If there is no equal support,
it appends the new node and inserts its ID into the bucket. Colliding unequal
supports therefore cause extra comparisons, never a false match or a missed
equal support.

Induct on the addition sequence. Both rules initially have the same supports
and node IDs. The zero cases return the same ID. In every other case the bucket
argument proves that the same existing node is returned or that the same new
node is appended. An existing node's arguments are never replaced; a new
node records the same ordered pair. Thus the complete support and argument
sequences are equal after every call. Any deterministic caller receiving those
IDs follows the same subsequent branches and obtains the same output IDs,
traversal and pruning.

The frozen mixed-point caller accesses the interning table only during
initialization, addition and the paired-kernel handoff. The two adapters change
the first two sites and carry the key array together with the table at the
handoff. `verify.py` checks the entire adapted source against those exact
changes. The proof applies to its valid addition sequences. The unchanged
builder's mathematical identity is a predecessor dependency, not a new claim.

The new overlap guard rejects invalid, nondisjoint additions before any write,
including under `-O`. Input-shape and capacity guards also fail before a write.
The node-capacity guard acts only when an actual new node would be needed;
an already interned support remains usable at capacity. This does not promise
identical failure behavior to the old assertion-based rule outside valid input.

There are at most 25,000 input coordinates and 4,000,000 stored nodes. Each
bucket contains at most the current node count. Each stored support has at most
25,000 bits, and each key has at most 64 bits. In the absence of collisions,
the key lookup uses fixed-width integers. Complete support union, disjointness
and equality still use the original bitmasks. No worst-case asymptotic speedup
is claimed: all keys may collide, and then the bucket scan is linear in its
size. Correctness is unconditional on collision frequency.
Loading