Reduce disjoint verifier peak traced allocation by 62% (no new κ)

research/disjoint-dag-streaming/PROOF.md

@@ -0,0 +1,118 @@
+# Exact streaming serialization and retained checks
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+The encoder accepts a finite set of active integer node indices, an argument
+array and a support array of the same length. The arrays have at most
+1,000,000 entries. Each argument is either `None` or a two-tuple of valid
+nonnegative integer indices. Each support is a nonnegative integer of at
+most 10,000 bits. Boolean indices and supports are rejected. The measured
+`h=26` instance lies within these limits.
+
+These bounds are explicit limits of this opt-in encoder. The support-bit bound
+covers the default input-width budget; the node bound is an additional limit.
+They do not assert that every possible expansion fits. The unchanged
+checker still decides support, topology, recurrence and embedding validity.
+The encoder is not an alternative mathematical admission test.
+
+## Canonical bytes
+
+The old expression is
+
+```python
+json.dumps([[i, args[i], str(support[i])] for i in sorted(active)],
+           separators=(',', ':')).encode()
+```
+
+For a valid row, compact JSON encodes an index by its decimal digits, `None`
+by `null`, and a two-tuple by its two decimal entries inside square brackets.
+The support has already been converted to a string. It contains only decimal
+digits, so neither escaping nor character-set selection changes it. The
+resulting row is exactly `[i,null,"s"]` or `[i,[a,b],"s"]`.
+
+The new encoder emits the same initial square bracket, those same rows in
+the same sorted order, one comma between successive rows, and the same final
+square bracket. The empty set emits `[]`. Its concatenated chunks therefore
+equal the old byte string, including tuple/null distinction and digit order.
+This statement is byte equality, stronger than matching two SHA256 digests.
+Incremental SHA256 consumes the concatenation in order, so it returns the
+same digest. There is no omitted lazy computation: `stream_digest` exhausts
+the generator before returning.
+
+## Buffer bound
+
+At most six decimal digits encode an index. A pair uses at most fifteen
+characters. A 10,000-bit nonnegative integer uses at most 3,011 decimal
+digits, since `2**10000 < 10**3011`. Including brackets, commas and quotes,
+one row has at most 3,038 bytes. Its preceding separator adds at most one.
+
+The buffer is flushed after the row that reaches the configured threshold
+`B`, where `1 <= B <= 65536`. Before that row its length is below `B`,
+except for the initial single bracket when `B=1`.
+Thus every emitted chunk has at most `B + 3039` bytes, a conservative bound
+also covering the final bracket and the empty case. No allocation grows
+with the sum of the serialized row lengths. Sorting still retains `O(n)`
+node references, and Python retains a constant number of chunk/row copies.
+The additional serialization space is `O(n + B + d)`, where `d <= 3011` is
+the largest decimal support length. This is not a claim of constant space,
+process RSS reduction, or a bound on the circuit's existing storage.
+
+The historical encoder retains all row strings, a complete JSON string and
+its encoded bytes. The new encoder eliminates those whole-document copies.
+The allocation experiment starts after construction, and separately measures
+the digest and the complete verification call with `tracemalloc`.
+
+## Check conservation and invalidation
+
+`accelerator.verify` is a static copy of the pinned method with exactly two
+changes: remove its final `encoded = ...` assignment, and replace its
+`dag_sha256` expression by `stream_digest(self)`. The registered verifier
+compares the entire function AST after exactly those substitutions. Any other
+statement or expression change fails that comparison. Thus the support,
+acyclicity, disjointness, recurrence, physical embedding, fanout freshness and
+output checks, and every other receipt field, are retained. No checks are
+replaced by cached success.
+
+The adapter authenticates its declared live input bytes before importing the
+checker and its dependencies. Direct invocations select an absent bytecode
+namespace and prohibit bytecode writes. The sources must remain stable during
+an invocation. Five changed-input controls reject drift; a future source
+change requires an explicit new adapter comparison, not silent reuse.
+
+Finite corroboration includes every support choice in `{0,1,2,3}`, every
+argument choice and every active subset on arrays of length zero through
+two. There are 1,617 such schemas. Six large-integer fixtures bring the total
+to 1,623. Four chunk thresholds exercise delimiter and flush boundaries.
+Six actual circuits include singleton inputs, pairs, triples and `h=26`.
+Both complete receipts and actual bytes agree. Controls also remove each
+nondigest top-level statement and corrupt four actual circuits. The same
+checks run under optimized Python.
+
+This proves a scoped serialization equivalence and checks its application to
+the retained verifier. It adds no supplier, multiplication theorem, native
+cost model, formal proof-kernel result or new kappa.
+
+## Code constraints
+
+The new encoder uses no recursion, dynamic evaluation, subprocess or global
+mutation of the original checker. Its loops are bounded by one million nodes,
+two argument entries, and a fixed chunk budget. The benchmark uses five to
+ten pairs of serial subprocesses, each with a 120-second timeout. All new
+functions fit within sixty lines. Boundary guards use explicit exceptions
+and remain active under `-O`.
+
+Python requires managed allocations. The deviation from Power of Ten's
+fixed-allocation rule is limited to these bounded arrays, strings and chunks;
+the buffer bound above and explicit input limits provide the control.
+The unchanged constructor and compiler retain their original recursion,
+allocation and assertion contracts. Rewriting them would expand this task
+beyond serialization. Their exact bytes, the AST guard, full receipt checks
+and direct corruption controls prevent this adapter from changing them.
+A separate streamed compiler would need its own ownership and iteration
+proof before replacing that dependency.
+
+No project Python linter is configured for this package, and Ruff is absent
+from the local interpreter. Registered normal and optimized runs use
+`-W error`; the exact-AST comparison also parses both checker implementations.

research/disjoint-dag-streaming/README.md

@@ -0,0 +1,162 @@
+# Stream disjoint-tensor DAG hashes with lower allocation
+
+This opt-in adapter reduces peak traced allocation during complete
+`DisjointTensor(26).verify()` from **107,703,062 to 41,079,356 bytes**, about
+**62%**, while returning the identical complete receipt. The historical
+checker and its certificates remain unchanged.
+
+Claim type: **tooling improvement with a scoped serialization-equivalence
+proof**. This answers Open next question 1 of Wentao Li's
+[PR #2117](https://github.com/CrocSwap/integer-mult-bounds/pull/2117).
+It supplies neither a new mathematical construction nor a new kappa.
+
+## What changes
+
+The old checker builds every DAG row, a complete JSON document and its encoded
+bytes before hashing. [accelerator.py](accelerator.py) emits the same compact
+JSON bytes into bounded chunks and hashes them incrementally. It keeps a
+static copy of the original `verify` body; only its final digest construction
+changes. The registered check compares the entire function AST after exactly
+that substitution, so a removed or weakened nondigest check is rejected.
+
+[PROOF.md](PROOF.md) proves exact byte equality for the restricted
+integer/tuple/null schema, gives a conservative 68,575-byte bound on each
+emitted chunk, and explains sorting and managed-memory costs. The explicit
+limits are one million array entries and 10,000 bits per support. This is an
+opt-in bound, not a claim that all possible historical expansion budgets fit.
+Source authentication runs before checker imports. Direct execution disables
+old bytecode reads as well as new bytecode writes.
+
+## Reproduce
+
+From the repository root, using the tested CPython 3.12 interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/disjoint-dag-streaming
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/disjoint-dag-streaming/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/disjoint-dag-streaming/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/disjoint-dag-streaming --check-source-history
+```
+
+The interpreter path is host-specific; another CPython 3.12 installation can
+run the same standard-library-only checks. Expected direct result:
+`PASS_DISJOINT_DAG_STREAMING`, 1,623 schema fixtures, six complete circuit
+receipts and 41 rejecting controls. Both Python modes run identical coverage.
+
+To repeat the descriptive benchmark, choose an existing output directory
+outside the checkout and run:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/disjoint-dag-streaming/benchmark.py --rounds 5 --output "$disjoint_run_dir/measurements.json"
+```
+
+The benchmark refuses an output inside the checkout. Its generated JSON
+contains samples, source hashes, environment, node counts, errors and full
+receipts. Timing is not a CI correctness gate, and no generated log or export
+belongs in the checkout.
+
+## Evidence
+
+The written equivalence proof is corroborated by all 1,617 length-zero-through-
+two schemas with supports in `{0,1,2,3}`, every argument choice and active
+subset; six large-integer fixtures extend through 10,000-bit supports. Four
+chunk thresholds exercise flush and delimiter cases. Six complete circuits
+cover `(h,k) = (4,1), (6,2), (6,3), (8,3), (10,3), (26,3)`. Both their actual
+bytes and complete verification receipts agree.
+
+The largest fixture has 60,372 active nodes, 57,772 additions, 2,600 inputs,
+2,600 outputs and 4,604,600 nonzero coefficients. Its unchanged DAG digest is
+`5da8011dadf51d6121d343416fa38b6b4bf524fd689e5b1b2def91324660f19b`.
+Every value comes from an executed circuit. The contribution is the changed
+encoder, not a re-audit or new proof of those predecessor circuit counts.
+
+The 41 controls comprise 13 malformed schemas, four invalid chunk budgets,
+five changed declared inputs, eleven deleted nondigest top-level statements,
+and eight rejection calls on four corrupted actual circuits. The corruption
+cases change a sum support, create a cycle, exceed the recurrence count and
+change an output binding. The original and accelerated methods both reject.
+
+## Measurements
+
+CPython 3.12.15, macOS arm64, standard library only. Five fresh-process pairs
+alternate order. Both sides build the same circuit and consume every result;
+all full receipts agree and there are zero errors. Five traced-allocation
+measurements per side give the same respective peaks. The table gives median
+wall time with minimum and maximum in brackets.
+
+| Quantity | Original | Streaming |
+| --- | ---: | ---: |
+| Digest peak traced allocation | 84,685,162 B | 691,046 B |
+| Complete verify peak traced allocation | 107,703,062 B | 41,079,356 B |
+| Digest wall time | 0.227564 s [0.226946, 0.229425] | 0.204584 s [0.203043, 0.224004] |
+| Complete verify wall time | 0.322287 s [0.318810, 0.355722] | 0.299514 s [0.294348, 0.309523] |
+| Construction plus verify wall time | 0.399820 s [0.397821, 0.433130] | 0.377585 s [0.371520, 0.388686] |
+
+These are additional Python allocations after circuit construction, measured
+with `tracemalloc`. They are not process RSS, retained circuit memory, or a
+physical multiplier memory claim. Timing is measured separately with tracing
+disabled. Construction-plus-verification includes circuit construction and the
+complete checker, while import and source authentication are excluded equally.
+The primary result is allocation reduction. The modest timing difference is
+host-descriptive and is not a portable speed guarantee.
+
+| Pair | Original verify s | Streaming verify s | Original construction + verify s | Streaming construction + verify s |
+| --- | ---: | ---: | ---: | ---: |
+| 1 | 0.323283917 | 0.302542917 | 0.399819792 | 0.380593542 |
+| 2 | 0.321335458 | 0.299513541 | 0.398702042 | 0.377585041 |
+| 3 | 0.322286625 | 0.295842375 | 0.402609333 | 0.373650625 |
+| 4 | 0.318810458 | 0.294347792 | 0.397820750 | 0.371520042 |
+| 5 | 0.355722250 | 0.309522667 | 0.433130208 | 0.388685959 |
+
+An untimed-in-the-report profile of the original verification spent 0.105 s
+of 0.380 s in `compile`, 0.044 s in JSON encoding, and most remaining time in
+the checker body, which includes decimal support conversion. These scalar
+conversion and compile costs remain. The machine had 18 logical CPUs and
+load averages 2.64, 3.55, 3.73 before the run; unrelated processes were active,
+so order is interleaved. No other replay was run concurrently in this worktree.
+
+## Scope and provenance
+
+Canonical base is `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision
+8. [SOURCES.json](SOURCES.json) binds the four imported checker/dependency
+files and the predecessor question. The selected record and original task
+card are provenance only. Existing default sources, frozen certificates,
+archives, selected frontier and predecessor credit are unchanged.
+
+Live overlap included paginated snapshots of 379 open PRs and 5,784 Discussion
+records, recent account contributions, the latest handoffs and active threads,
+batch reservations, distinctive main README searches and merged-PR searches.
+Sparse local notes covered 70 of 8,348 paths, so their omissions are explicit.
+The relevant existing PRs #2001, #2039, #2117 and #2150 accelerate other paths
+or leave this exact question open. No exhaustive novelty claim is made about
+unpublished work or arbitrary historical diffs.
+
+The complete selected supplier, full historical audit suites, Lean, Docker,
+native costs, all-size compiler, precision/tape, erasure and exact-recovery
+obligations were not rerun or discharged. This package does not change a
+mathematical result or supplier admission.
+
+## Open next questions
+
+1. Can the default checker adopt this encoder while preserving historical
+   source bindings? Specify the source-pin migration and retain old evidence
+   first. Default adoption is outside this opt-in package.
+2. Can the remaining compiler allocation be reduced while preserving every
+   physical embedding and freshness check? Start with its users, edges, gates
+   and values. A streamed compiler needs a separate ownership argument.
+
+The structured questions, first steps and blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution was produced by Nick Petalas. Douglas R. Colkitt authored
+the retained disjoint-tensor and reversible-embedding checker. Wentao Li
+[@VictorLiwentao](https://github.com/VictorLiwentao) supplied
+[#2001](https://github.com/CrocSwap/integer-mult-bounds/pull/2001),
+[#2117](https://github.com/CrocSwap/integer-mult-bounds/pull/2117), the explicit
+serialization question, and earlier byte-preserving formatter precedents.
+Stephan Arrington's [#1044](https://github.com/CrocSwap/integer-mult-bounds/pull/1044)
+supplies the retained frame-union lineage. Incremental SHA256 and compact JSON
+are standard techniques. The new contribution is this exact bounded-chunk
+encoder, its source-bound application and the measured allocation reduction.
+Apache-2.0. Independent human and formal proof-kernel review are unclaimed.

research/disjoint-dag-streaming/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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"
+    },
+    {
+      "path": "research/disjoint-tensor-frame-unions/README.md",
+      "usage": "input",
+      "git_blob": "6becefba9edf6d3546a4d4226705686069473aa5",
+      "sha256": "4e83cabb12511ca83820a7b28110a1f758ce82f73cdd5fd923156c35d93e1f59"
+    },
+    {
+      "path": "scripts/binary_phase_frames.py",
+      "usage": "input",
+      "git_blob": "c8e4fa71fe60550324f9e43c1dd5ad6d9bf4e2f4",
+      "sha256": "4148cfa313cf050ed25296e8db36d35871520b8318fd086c7d1facf0c6af67d7"
+    },
+    {
+      "path": "scripts/certify.py",
+      "usage": "input",
+      "git_blob": "a773311b726fd1ef98a056f6f76010e872d7908a",
+      "sha256": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e"
+    },
+    {
+      "path": "scripts/exclusion_circuit.py",
+      "usage": "input",
+      "git_blob": "b0e2f3e03d7de791ca936dfd92cee2134c7dd4f5",
+      "sha256": "f9fbcd6e85e442cbd0926ac0887414e20735b2dc923d2d5822c803ceb46726d3"
+    },
+    {
+      "path": "scripts/experiments/disjoint_tensor.py",
+      "usage": "input",
+      "git_blob": "cc85de3024d191b79bf64ced2b39d782854fe491",
+      "sha256": "23763a4b6086fb3d19f9282fff5c118f53fa52e7a7f17da1bde990bd4cf8b6ac"
+    }
+  ]
+}