From e4eb97178bdc083cf9e60f8796cf93cddbe27dbf Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 13:11:49 +0000 Subject: [PATCH] perf(research): stream disjoint DAG hashes with lower allocation --- research/disjoint-dag-streaming/PROOF.md | 118 ++++++++++++ research/disjoint-dag-streaming/README.md | 162 +++++++++++++++++ research/disjoint-dag-streaming/SOURCES.json | 48 +++++ research/disjoint-dag-streaming/TASK.json | 67 +++++++ research/disjoint-dag-streaming/VERIFY.json | 40 +++++ .../disjoint-dag-streaming/accelerator.py | 128 +++++++++++++ research/disjoint-dag-streaming/benchmark.py | 120 +++++++++++++ research/disjoint-dag-streaming/verify.py | 169 ++++++++++++++++++ 8 files changed, 852 insertions(+) create mode 100644 research/disjoint-dag-streaming/PROOF.md create mode 100644 research/disjoint-dag-streaming/README.md create mode 100644 research/disjoint-dag-streaming/SOURCES.json create mode 100644 research/disjoint-dag-streaming/TASK.json create mode 100644 research/disjoint-dag-streaming/VERIFY.json create mode 100644 research/disjoint-dag-streaming/accelerator.py create mode 100644 research/disjoint-dag-streaming/benchmark.py create mode 100644 research/disjoint-dag-streaming/verify.py diff --git a/research/disjoint-dag-streaming/PROOF.md b/research/disjoint-dag-streaming/PROOF.md new file mode 100644 index 0000000000..df40febc9f --- /dev/null +++ b/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. diff --git a/research/disjoint-dag-streaming/README.md b/research/disjoint-dag-streaming/README.md new file mode 100644 index 0000000000..32f2ea89ed --- /dev/null +++ b/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. diff --git a/research/disjoint-dag-streaming/SOURCES.json b/research/disjoint-dag-streaming/SOURCES.json new file mode 100644 index 0000000000..ea9242835f --- /dev/null +++ b/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" + } + ] +} diff --git a/research/disjoint-dag-streaming/TASK.json b/research/disjoint-dag-streaming/TASK.json new file mode 100644 index 0000000000..9e0506c80b --- /dev/null +++ b/research/disjoint-dag-streaming/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "An opt-in bounded-memory DAG serializer for the unchanged DisjointTensor.verify checks, with exact canonical-byte and complete-receipt equivalence and paired h=26 measurements.", + "scope_change_reason": "Takes the explicit DAG-serialization question in Wentao Li PR2117. This is verifier engineering on a historical checker, not a new mathematical supplier or an audit of predecessor results.", + "bottleneck_link": "Side result on review resources: avoid whole-document JSON allocation in a historical exact checker. This neither changes the binding complex supplier nor improves kappa.", + "budget_minutes": 60, + "stop_rule": "Ship the first material allocation reduction with identical bytes and all checks. Stop after packaging; leave default adoption and compile-memory work open.", + "outcome": "completed", + "evidence": "PROOF.md gives the scoped byte equivalence and buffer bound. verify.py checks 1623 schemas, six complete receipts through h=26, 41 rejecting controls and the complete nondigest checker AST. benchmark.py supplies five interleaved fresh-process pairs with exact receipt checks and separate traced-allocation runs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the default disjoint-tensor checker adopt the streaming encoder while preserving historical source bindings?", + "why_it_matters": "The measured allocation reduction is currently opt-in.", + "first_step": "Specify a source-pin migration and retain the historical implementations and certificates unchanged.", + "blocked_by": "Default adoption and historical replay migration are outside this isolated package." + }, + { + "question": "Can the remaining compile allocation be reduced with a streamed reversible-embedding check?", + "why_it_matters": "The full verification still peaks near 41 MB even though digest allocation is below 1 MB.", + "first_step": "Profile the retained users, edges, gates and values, then specify an iterator that preserves every freshness and output check.", + "blocked_by": "No replacement compile algorithm or equivalent ownership protocol is supplied here." + } + ] +} diff --git a/research/disjoint-dag-streaming/VERIFY.json b/research/disjoint-dag-streaming/VERIFY.json new file mode 100644 index 0000000000..d0e8233052 --- /dev/null +++ b/research/disjoint-dag-streaming/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/disjoint-tensor-frame-unions/README.md", + "scripts/binary_phase_frames.py", + "scripts/certify.py", + "scripts/exclusion_circuit.py", + "scripts/experiments/disjoint_tensor.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact canonical JSON bytes on 1623 schemas and six circuits through h=26; identical complete receipts; unchanged nondigest checker AST; malformed input, changed-source, omitted-statement and circuit-corruption rejection." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete coverage and rejection controls with assertions disabled." + } + ] +} diff --git a/research/disjoint-dag-streaming/accelerator.py b/research/disjoint-dag-streaming/accelerator.py new file mode 100644 index 0000000000..0c9744ffed --- /dev/null +++ b/research/disjoint-dag-streaming/accelerator.py @@ -0,0 +1,128 @@ +"""Opt-in bounded-memory serialization for the unchanged disjoint-tensor checks. + +This contribution was produced by Nick Petalas. Apache-2.0. +The verify body retains Douglas Colkitt's original checker, including Wentao +Li's support-mask optimization. Only its digest expression changes. +""" +from hashlib import sha256 +import json +from math import comb +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +MAX_NODES = 1_000_000 +MAX_SUPPORT_BITS = 10_000 +CHUNK_BYTES = 65_536 + + +def check_sources(root=ROOT, overrides=None): + """Authenticate every declared live input before importing its code.""" + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + overrides = {} if overrides is None else overrides + for row in manifest["files"]: + if row["usage"] == "input": + name = row["path"] + data = overrides[name] if name in overrides else (root / name).read_bytes() + if sha256(data).hexdigest() != row["sha256"]: + raise ValueError("Source changed: " + name) + + +check_sources() +# -B prohibits bytecode writes, but does not prohibit old bytecode reads. +sys.dont_write_bytecode = True +cache_prefix = PACKAGE / ".disabled-bytecode-cache" +if cache_prefix.exists(): + raise ValueError("The disabled cache namespace must be absent") +sys.pycache_prefix = str(cache_prefix) +sys.path.insert(0, str(ROOT / "scripts")) +from certify import require +from experiments.disjoint_tensor import DisjointTensor, plan + + +def chunks(circuit, chunk_bytes=CHUNK_BYTES): + """Yield the exact compact JSON bytes with a bounded row buffer.""" + require(type(chunk_bytes) is int and 1 <= chunk_bytes <= CHUNK_BYTES, + "Invalid chunk budget") + size = len(circuit.support) + require(size == len(circuit.args) and size <= MAX_NODES, + "Node-array budget exceeded") + require(len(circuit.active) <= size, "Invalid active-node count") + buffer = bytearray(b"[") + for position, node in enumerate(sorted(circuit.active)): + require(type(node) is int and 0 <= node < size, "Invalid node") + support = circuit.support[node] + require(type(support) is int and support >= 0 + and support.bit_length() <= MAX_SUPPORT_BITS, "Invalid support") + pair = circuit.args[node] + if pair is None: + args = "null" + else: + require(type(pair) is tuple and len(pair) == 2 + and all(type(x) is int and 0 <= x < size for x in pair), + "Invalid argument pair") + args = f"[{pair[0]},{pair[1]}]" + if position: + buffer.extend(b",") + buffer.extend(f'[{node},{args},"{support}"]'.encode("ascii")) + if len(buffer) >= chunk_bytes: + yield bytes(buffer) + buffer.clear() + buffer.extend(b"]") + yield bytes(buffer) + + +def stream_digest(circuit): + """Consume every chunk before returning the canonical DAG SHA256.""" + digest = sha256() + for chunk in chunks(circuit): + digest.update(chunk) + return digest.hexdigest() + + +def verify(self): + for node in sorted(self.active): + if self.args[node]: + a, b = self.args[node] + require(a < node and b < node and not self.support[a]&self.support[b], + 'An addition uses cancellation or is not acyclic') + require(self.support[node] == self.support[a]|self.support[b], 'Wrong sum') + # Expected output support equals the full input mask with every input + # that meets T cleared. Equivalent to the historical genexpr + # sum(1<> i & 1}) + expected = reference_bytes(circuit) + for budget in (1, 7, 64, fast.CHUNK_BYTES): + actual = b"".join(fast.chunks(circuit, budget)) + require(actual == expected, "Tiny-schema bytes differ") + require(fast.stream_digest(circuit) == sha256(expected).hexdigest(), + "Tiny-schema digest differs") + cases += 1 + for bits in (1, 8, 64, 127, 1024, fast.MAX_SUPPORT_BITS): + circuit = SimpleNamespace(support=[0, (1 << bits) - 1], + args=[None, (0, 1)], active={1, 0}) + require(b"".join(fast.chunks(circuit, 7)) == reference_bytes(circuit), + "Large-integer bytes differ") + cases += 1 + return cases + + +def check_rejections(): + cases = [ + ([0], [None], {-1}), ([0], [None], {1}), ([0], [None], {True}), + ([-1], [None], {0}), (["1"], [None], {0}), + ([1 << fast.MAX_SUPPORT_BITS], [None], {0}), + ([0], [(0,)], {0}), ([0], [(0, True)], {0}), + ([0], [[0, 0]], {0}), ([0], [(0, 1)], {0}), + ([0], [], {0}), ([0], [None], {0, 1}), + (range(fast.MAX_NODES + 1), range(fast.MAX_NODES + 1), set()), + ] + for support, args, active in cases: + circuit = SimpleNamespace(support=support, args=args, active=active) + rejects(lambda: fast.stream_digest(circuit), "malformed schema") + good = SimpleNamespace(support=[0], args=[None], active={0}) + for budget in (0, -1, True, fast.CHUNK_BYTES + 1): + rejects(lambda: list(fast.chunks(good, budget)), "chunk budget") + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = [row for row in manifest["files"] if row["usage"] == "input"] + for row in inputs: + data = (fast.ROOT / row["path"]).read_bytes() + b"\n" + rejects(lambda: fast.check_sources(overrides={row["path"]: data}), "source drift") + original = coverage_guard() + for index in range(len(original.body) - 1): + mutant = copy.deepcopy(original) + mutant.body.pop(index) + rejects(lambda: coverage_guard(mutant), "omitted checker statement") + return len(cases) + 4 + len(inputs) + len(original.body) - 1 + + +def check_circuits(): + fixtures = [(4, 1), (6, 2), (6, 3), (8, 3), (10, 3), (26, 3)] + records = [] + for h, k in fixtures: + circuit = fast.DisjointTensor(h, k) + baseline = circuit.verify() + streamed = fast.verify(circuit) + require(baseline == streamed, "Complete verification receipts differ") + pieces = list(fast.chunks(circuit)) + require(max(map(len, pieces)) <= fast.CHUNK_BYTES + 3039, + "Row-buffer bound exceeded") + require(b"".join(pieces) == reference_bytes(circuit), + "Real-circuit bytes differ") + records.append(streamed) + for kind in range(4): + circuit = fast.DisjointTensor(8) + node = next(i for i in sorted(circuit.active) if circuit.args[i] is not None) + if kind == 0: + circuit.support[node] ^= 1 + elif kind == 1: + circuit.args[node] = (node, circuit.args[node][1]) + elif kind == 2: + circuit.additions = 1_000_000_000 + else: + target = next(iter(circuit.outputs)) + circuit.outputs[target] = 1 + rejects(circuit.verify, "baseline circuit fault") + rejects(lambda: fast.verify(circuit), "streamed circuit fault") + return records + + +def main(): + fast.check_sources() + coverage_guard() + byte_cases = check_bytes() + rejection_cases = check_rejections() + records = check_circuits() + print(json.dumps({ + "status": "PASS_DISJOINT_DAG_STREAMING", + "schema_cases": byte_cases, "rejection_cases": rejection_cases + 8, + "full_receipt_fixtures": len(records), "h26": records[-1], + "claim_type": "tooling improvement with scoped serialization equivalence", + "no_new_kappa": True, + }, sort_keys=True)) + + +if __name__ == "__main__": + main()