From 6396612541cda6a5fad0d2949e4e80a30991e572 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 18:37:50 +0530 Subject: [PATCH 1/3] Recycled-bit --all nesting: output-identical fraction-free null_exact fast path Install an integer fraction-free drop-in for PR97 linalg.null_exact (and an integer frames147.prim) at runtime from recycled-bit-integration/verify.py; frozen PR97/bit-reuse-147 files stay byte-unchanged. VERIFY_NULL=reference restores the Fraction kernel; VERIFY_NULL=audit runs both and asserts equality. Only the verify.py source pin in certificate.json changes. New package research/recycled-bit-nesting-reuse: profile, refuted late_frames basis-reuse idea (2.6% key coverage), same-input timings, equality audits, differential check and negative controls. Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Co-Authored-By: Claude Opus 5.5 --- .../recycled-bit-integration/certificate.json | 2 +- research/recycled-bit-integration/verify.py | 86 +++++++++++ research/recycled-bit-nesting-reuse/README.md | 127 ++++++++++++++++ .../recycled-bit-nesting-reuse/SOURCES.json | 36 +++++ research/recycled-bit-nesting-reuse/TASK.json | 73 ++++++++++ .../recycled-bit-nesting-reuse/VERIFY.json | 24 ++++ research/recycled-bit-nesting-reuse/verify.py | 135 ++++++++++++++++++ 7 files changed, 482 insertions(+), 1 deletion(-) create mode 100644 research/recycled-bit-nesting-reuse/README.md create mode 100644 research/recycled-bit-nesting-reuse/SOURCES.json create mode 100644 research/recycled-bit-nesting-reuse/TASK.json create mode 100644 research/recycled-bit-nesting-reuse/VERIFY.json create mode 100644 research/recycled-bit-nesting-reuse/verify.py diff --git a/research/recycled-bit-integration/certificate.json b/research/recycled-bit-integration/certificate.json index 769063a187..114c40f5ae 100644 --- a/research/recycled-bit-integration/certificate.json +++ b/research/recycled-bit-integration/certificate.json @@ -335,7 +335,7 @@ "research/recycled-bit-integration/plan.json": "ab8887e5d852fdce16a883a1ffc3173e109708a484b986cb2574e1ee634bf784", "research/recycled-bit-integration/row.json": "075c8ff2f9f1b25f6b81dc0c6ec31adc766944cb59badc4bc6e42668993ca073", "research/recycled-bit-integration/selection146.json": "407fac7fc3f3497ddf347fc7a820a6b863c2147d18f1be325b57d37998475a3e", - "research/recycled-bit-integration/verify.py": "a5508f429d0ff6d441d9d07f6d1f9a83ce2335eb59b2041abbc65327b6a4a0b9", + "research/recycled-bit-integration/verify.py": "3299094e922fa45fc82a3a68634515df2340c0bbdb8d2faf1c71d90bfbf37d18", "scripts/paired_cube_bit.py": "677ff674f48860336ca96c4ab6d7fa9053bf7137d20ba368445d20e236765dbe", "scripts/paired_cube_network.py": "293662b7f8772dd398399a1c19966faf7d155f024543d0c06601eabb800f35cf", "scripts/structured_bulk_assembly.py": "e99467e14211fba699878ed036e1e2362eb8e395dc22f9ecdcecc7fbf2cc736d", diff --git a/research/recycled-bit-integration/verify.py b/research/recycled-bit-integration/verify.py index 77767998d4..19d42495c6 100644 --- a/research/recycled-bit-integration/verify.py +++ b/research/recycled-bit-integration/verify.py @@ -6,6 +6,8 @@ Default: reconstruct, check exact new frame pairs and complete symbolic scalar maps. --all: additionally check every distinct inherited frame transition over Q. Both frame-pair loops run on forked workers (VERIFY_JOBS, default the CPU count); each check is unchanged. +The exact null spaces use an integer fraction-free kernel with output identical to PR97 linalg.null_exact +(VERIFY_NULL=reference uses the original Fraction kernel; VERIFY_NULL=audit runs both and asserts equality). --write: write the deterministic certificate after all checks pass. """ import sys @@ -21,6 +23,7 @@ import multiprocessing import os from pathlib import Path +from math import gcd import random import time @@ -29,6 +32,7 @@ sys.path.insert(0, str(ROOT / 'research/bit-reuse-147')) import word147 import price147 +import frames147 from frames147 import Exact import paired_cube_network as pcn @@ -56,6 +60,87 @@ def sources(): ROOT / 'certificates/paired-cube-complex-input.json'] return {str(p.relative_to(ROOT)): sha256(p.read_bytes()).hexdigest() for p in sorted(set(paths))} +def null_exact_ff(A, k): + """For an integer matrix: the same list of rows as PR97 linalg.null_exact (Fraction RREF), fraction-free. + + The steps mirror null_exact one for one: reduce each row by the earlier pivot rows, take its first nonzero + entry as pivot, clear that column in the earlier rows. Each stored row is a nonzero rational multiple of the + corresponding Fraction row (pivots kept positive), so the pivots and the reduced row space agree; for each free + column f, x has x_f = lcm of the pivots and x_pc = -b[f] * lcm / b[pc], a positive multiple of the Fraction + vector, and dividing by the gcd gives the same primitive vector as linalg.primitive. + """ + R = []; piv = []; pv = [] + for r0 in A: + r = list(r0) + for pc, p, b in zip(piv, pv, R): + c = r[pc] + if c: r = [p * x - c * y for x, y in zip(r, b)] + i = next((i for i, x in enumerate(r) if x), None) + if i is None: continue + g = gcd(*r) + if r[i] < 0: g = -g + if g != 1: r = [x // g for x in r] + a = r[i] + for t, b in enumerate(R): + c = b[i] + if c: + b = [a * x - c * y for x, y in zip(b, r)]; g = gcd(*b) + if g != 1: b = [x // g for x in b] + R[t] = b; pv[t] = b[piv[t]] + R.append(r); piv.append(i); pv.append(a) + pivots = set(piv); out = [] + for f in range(k): + if f in pivots: continue + lcm = 1 + for p, b in zip(pv, R): + if b[f]: lcm = lcm * p // gcd(lcm, p) + x = [0] * k; x[f] = lcm + for pc, p, b in zip(piv, pv, R): + if b[f]: x[pc] = -b[f] * (lcm // p) + g = gcd(*x) + out.append([v // g for v in x] if g != 1 else x) + return out + +_ORIGINAL = {} + +def install_null_kernel(folder, mode=None): + """Replace null_exact in the pinned PR97 modules (and prim in frames147) before Exact is built. + + The frozen files are not edited. Non-integer or ragged input falls back to the original functions.""" + mode = mode or os.environ.get('VERIFY_NULL', 'fast') + assert mode in ('fast', 'reference', 'audit'), mode + if str(folder) not in sys.path: + sys.path.insert(0, str(folder)) + import linalg + import check_lifted + ref_null = _ORIGINAL.setdefault('null_exact', linalg.null_exact) + ref_prim = _ORIGINAL.setdefault('prim', frames147.prim) + if mode == 'reference': + linalg.null_exact = check_lifted.null_exact = ref_null + frames147.prim = ref_prim + return mode + def integral(A, k): + return all(len(r) == k and all(type(x) is int for x in r) for r in A) + def null_fast(A, k): + return null_exact_ff(A, k) if integral(A, k) else ref_null(A, k) + def null_audit(A, k): + out = ref_null(A, k) + assert null_fast(A, k) == out, ('null_exact kernel mismatch', A, k) + return out + def prim_fast(r): + for x in r: + if type(x) is not int: return ref_prim(r) + g = gcd(*r) + return [x // g for x in r] if g else list(r) + def prim_audit(r): + out = ref_prim(r) + assert prim_fast(r) == out, ('prim mismatch', r) + return out + null, prim = (null_fast, prim_fast) if mode == 'fast' else (null_audit, prim_audit) + linalg.null_exact = check_lifted.null_exact = null + frames147.prim = prim + return mode + _EXACT = None _NONDEG = False @@ -123,6 +208,7 @@ def main(): fresh = word.new_moves(led) assert set(fresh) == set(old.new_moves(old_led)), 'Composition changed the new-frame obligations' log('PASS exact composed plan, chronological ledger and unchanged set of new frame pairs') + log('null_exact kernel: %s' % install_null_kernel(folder)) exact = Exact(S, W, folder) failed = check_moves(exact, fresh, nondegenerate=True) assert not failed, failed[:5] diff --git a/research/recycled-bit-nesting-reuse/README.md b/research/recycled-bit-nesting-reuse/README.md new file mode 100644 index 0000000000..4acffea26c --- /dev/null +++ b/research/recycled-bit-nesting-reuse/README.md @@ -0,0 +1,127 @@ +# recycled-bit-nesting-reuse + +**Tooling improvement. No new bound is claimed; kappa, certificate content and predicates are unchanged.** + +`make verify-recycled-bit` (`python3 research/recycled-bit-integration/verify.py --all`) is the longest job in +`verify.yml`. On main run 38506758315, job "verify (3.11, recycled-bit)", it took 657 s. Of that, 619 s was the stage +`PASS exact rational nesting (4878 new pairs; all inherited pairs checked)`. That stage builds +`frames147.Exact` from the pinned PR97 h=23 witness, then checks `inside` for all 202,190 ledger moves and +`inside` plus `nondegenerate` for the 4,878 fresh moves. This package records why the stage is slow, +refutes the first reuse idea, and documents an output-identical replacement for its main exact kernel. + +## What changed + +`research/recycled-bit-integration/verify.py` now defines `null_exact_ff` and `install_null_kernel`. Before +`Exact` is built, `main()` replaces `linalg.null_exact` and `check_lifted.null_exact` with an integer, fraction-free +kernel. It also replaces `frames147.prim` with an integer gcd version. These replacements happen at runtime. The +frozen files `references/partial-gauge/pr97/{linalg,check_lifted}.py` and `research/bit-reuse-147/frames147.py` +are byte-unchanged. Input that is not integral, or whose rows are ragged, falls back to the original function. +`VERIFY_NULL=reference` restores the original Fraction kernel. `VERIFY_NULL=audit` runs both kernels on every call +and asserts that their outputs are equal. The fork pool from 6fd436d0d (PR218) is kept as it was. The only other +change is the `verify.py` entry in `research/recycled-bit-integration/certificate.json` `source_sha256`. Every other +certificate byte, the move multiset, the predicates and the five PASS lines are the same. The run also prints one +extra informational line, `null_exact kernel: fast`. + +**Why the output is identical, not merely equivalent.** `null_exact_ff` repeats the steps of PR97 `null_exact`: +reduce each row by the earlier pivot rows, take its first nonzero entry as the pivot, then clear that column in +the earlier rows. By induction, every stored integer row is a nonzero rational multiple of the Fraction row at the +same step, with the pivot kept positive. So the pivot columns are the same, and the free columns come in the same +increasing order. For each free column f, the integer vector has `x_f = lcm(pivots)` and +`x_pc = -b[f] * lcm / b[pc]`. This is a positive multiple of the Fraction vector (`x_f = 1`, `x_pc = -b[f]/b[pc]`). +`linalg.primitive` maps a vector to the unique primitive integer multiple with the same sign, so dividing by the +gcd returns the same list of rows. `prim` on integer rows equals `x // gcd`. The equality was also measured: see +below. + +## Measurements + +All runs were on one shared host (4 CPUs, Python 3.14.4, `nice -n 10`), on the pinned base input. Timings in the +same row come from the same process, or from back-to-back runs, so they compare the same input. Other sessions +were running on the host, so the absolute times are noisy. + +| Measurement | Reference (Fraction `null_exact`) | Fast (fraction-free) | Equality | +| --- | --- | --- | --- | +| `null_exact` calls inside `Exact.__init__` (4,473 calls; mostly `late_frames` intersections) | 23.43 s kernel time | 2.88 s (8.1x) | all 4,473 identical | +| Deterministic sample: 400 ledger moves (`random.Random(1)`), 709 keys, 345 annihilators. Basis + null, rep 1 / rep 2 | 4.50 s / 3.88 s | 1.25 s / 1.11 s (3.5-3.6x) | basis and null maps identical | +| Same sample, `inside` dot products | 0.024 / 0.034 s | 0.024 / 0.025 s | — | +| Full-key audit (one process, both kernels on every call): every distinct basis key and every target annihilator of the 202,190 ledger moves | FULLKEY_REF | FULLKEY_FAST | FULLKEY_EQ | +| Full `--all` replay, `VERIFY_JOBS=3`, wall time of the nesting stage / whole run | FULLREF | FULLFAST | five PASS lines, kappa=472154791/10^12, certificate equal | + +**Profile of the stage (before).** The cProfile figures are inflated by profiling overhead. Of `Exact.__init__` +(about 160 s unprofiled), `Frames.dims` takes the largest share: about 52% of the profile, almost all of it +mod-p `Echelon.reduce` in `rank_mod`. `late_frames` takes about 32% (unprofiled 25.5 s), mostly the Fraction +`null_exact` in `intersect_exact`. `cobases` and `spans` take the rest. In the per-move work, a cProfile of 600 +basis and 300 null calls put about 72% of the time in `linalg.null_exact`, with Fraction arithmetic dominating. +The new kernel removes most of that time. It does not touch `dims`, which this package leaves unchanged +(see Open next questions). + +**Negative result for the first hypothesis (basis reuse from `late_frames`).** The planned mechanism was to seed +`Exact`'s basis memo from the `exact_basis` cache that `check_lifted.late_frames` builds and then throws away. +That cache holds 2,230 keys. The ledger moves use 86,789 distinct keys (n 64,042; v 11,374; sigma 8,181; +out 1,771; c 1,396; ret 23; '0' 1; F 1), so the cache covers 2.6% of them. Reuse alone cannot materially shorten the +stage, so that mechanism was dropped. This is the one pivot recorded in TASK.json. + +## Reproduce + +```sh +python3 -B research/recycled-bit-nesting-reuse/verify.py # ~40 s; last line PASS_RECYCLED_BIT_NULL_KERNEL +make verify-recycled-bit # full replay; five PASS lines, + # kappa=472154791/1000000000000 +VERIFY_NULL=audit python3 research/recycled-bit-integration/verify.py --all # full replay, both kernels on every call +``` + +`verify.py` in this package is the bounded check. It runs 3,012 differential matrices: edge cases (empty input, +k = 0/1, zero rows) and a deterministic random family (rank-deficient stacks, entries from {0,1} up to 2^80). It +runs 20,000 `prim` rows and checks the fallback on Fraction and ragged input. It also runs these negative controls, +which must fail: + +* a sign-flipped kernel row, and a doubled (non-primitive) row, differ from the reference; +* `VERIFY_NULL=audit` raises `null_exact kernel mismatch` when the fast kernel is replaced by a sign-flipped one; +* with the fast kernel installed, `check_moves` reports a swapped strict inclusion (non-nested move), and + `nondegenerate` rejects a degenerate frame (the span of 1^9 0^14, where 9*9 - 9^2 = 0); +* the certificate pins the new `verify.py` bytes. An edited `verify.py` changes `sources()`, so + `assert read(dest) == cert` fails. + +## Scope, inherited assumptions, unresolved obligations + +* This is an engineering change to one replay. It makes no mathematical claim beyond "same outputs". The + certificate is still the conditional composed bit-register witness of `recycled-bit-integration`. Its retained + analytic, fixed-tape, uniform-recursion, prime and ordinary-leaf interfaces remain assumptions, as before. +* The identity argument above is a proof sketch in this README, not a formal proof. The empirical evidence is + finite: the full-key audit recorded above, the init audit and the differential tests. +* Coverage: the call set audited was {all 4,473 init calls} and {basis of every distinct key, null of every + distinct target} in the order described above. Bases depend only on their keys, so these are the distinct + `null_exact` inputs of the `--all` path. Worker processes call the same functions on the same keys. +* CI wall time was not measured. The full runs used `VERIFY_JOBS=3` on a loaded host, so no CI speedup factor is + claimed. Sibling PR #2361 (CI selection) would run this job less often. The speedup still matters for + `make verify`, scheduled runs and relevant PRs. +* Historical receipts under `research/community-efficient1000-audit/checks/` record the old `verify.py` sha + (`a5508f42...`) as snapshots. No live verifier re-hashes them. They are left unchanged as historical evidence. + +## Open next questions + +1. *Question:* can `Frames.dims` (mod-p `Echelon` rank, now the largest remaining part of `Exact.__init__`) be + made faster with identical ranks? *Why:* after this change it is the largest serial cost before the pool + starts, and the forked workers do not share it. *First step:* replace the per-row list comprehension in + `Echelon.reduce` with a packed-integer or batched elimination mod Q31, behind the same runtime-install and + audit pattern. *Blocked by:* nothing; it needs its own equality audit on all 112,920 `_rank` calls. +2. *Question:* should the parent build the bases of shared source keys once before forking? *Why:* the 4 workers + rebuild overlapping source-key bases, and copy-on-write sharing would remove that duplicate work. *First step:* + measure the overlap of source keys across the current chunks. *Blocked by:* memory. Prebuilding all 86,789 + bases in the parent may use more than the CI runner can spare. Measure RSS first. +3. *Question:* do the other replays that use PR97 `null_exact` (`research/bit-reuse-147/verify.py`, + `research/gauge-recycling/verify.py`, `check_lifted.py` itself) benefit from the same installer? *Why:* the + kernel is shared. *First step:* profile `make verify-bit-reuse-147` and check its share of `null_exact`. + *Blocked by:* each verifier pins its own sources, so each would need its own pin update and review. + +## Credit + +* `research/recycled-bit-integration`: Douglas Colkitt, with OpenAI Codex assistance. It composes Thomas Marchand + (#146), William Porter (#147), gupt1156 (#148) and DaysSky (#150), per its `SOURCE.json`. +* PR97 `check_lifted.py` / `linalg.py`: Swapnil Jain. +* Fork-pool parallelization of this stage: Joel Pulikkan / GamingPuzzled (PR218, cherry-picked as 6fd436d0d). +* Related verifier speedups with an exact method: CubeJerry (PR1461, annihilator containment for the h=10/12 + audits) and RichardHoekstra (PR239, `rational_span_frames` nondegeneracy). + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +Base commit `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Source pins are in [SOURCES.json](SOURCES.json), and the +replay command and inputs are in [VERIFY.json](VERIFY.json). diff --git a/research/recycled-bit-nesting-reuse/SOURCES.json b/research/recycled-bit-nesting-reuse/SOURCES.json new file mode 100644 index 0000000000..a070681578 --- /dev/null +++ b/research/recycled-bit-nesting-reuse/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "references/partial-gauge/pr97/check_lifted.py", + "usage": "input", + "git_blob": "4a19240e2fe5f55891d842fd451bd0cb24e4ae76", + "sha256": "c3e87ad6b31f377df549421f53d22b99131d2228dcd08a1956913211383cbd6c" + }, + { + "path": "references/partial-gauge/pr97/linalg.py", + "usage": "input", + "git_blob": "a81cbaa61e2c09075f900546ec46833103b77ac1", + "sha256": "56cc779911a3c5c901bc5194ccaf97f720157a2c4ba602b07ee8642af2676b8b" + }, + { + "path": "research/bit-reuse-147/frames147.py", + "usage": "input", + "git_blob": "a336706b4803754d99f8d9bf9f7c92802a61fea4", + "sha256": "7345f18dca75fd20084830a40427067b4e7567d20b67f12f17f2d91abad9a471" + } + ] +} diff --git a/research/recycled-bit-nesting-reuse/TASK.json b/research/recycled-bit-nesting-reuse/TASK.json new file mode 100644 index 0000000000..9a31683aa8 --- /dev/null +++ b/research/recycled-bit-nesting-reuse/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "One replay stage: the exact rational nesting stage of make verify-recycled-bit (recycled-bit-integration/verify.py --all), whose Exact init and per-move basis/annihilator work is dominated by PR97 linalg.null_exact (Fraction RREF). Replace that kernel (and frames147.prim) at runtime by an output-identical fraction-free integer kernel, with an in-tree audit mode and before/after timing on the same pinned input.", + "scope_change_reason": "Refined from the card's generic \"profile one replay\" to one measured stage. The first mechanism (seed the basis memo from check_lifted.late_frames' discarded exact_basis cache) was refuted by measurement: the cache covers 2,230 of 86,789 distinct ledger-move keys (2.6%). One evidence-driven pivot to the dominant measured kernel (about 72% of per-move cost) with an identical-output requirement.", + "bottleneck_link": "verify-recycled-bit is the longest verify.yml job (657 s on main run 38506758315, 619 s in this stage); a faster identical replay shortens review/CI turnaround for every PR that runs it and for make verify. It is a side result for the kappa bottleneck: no mathematical change.", + "budget_minutes": 90, + "stop_rule": "Stop and submit a profiling note instead of a code change if the fast kernel gives < 1.5x on the sampled basis+null workload, if any output differs from the reference null_exact, or if the full after-run cannot finish by 2026-10-15T13:40:15Z (then report subset-only results).", + "outcome": "completed", + "evidence": "See README Measurements: init-call audit (4,473 calls identical, 8.1x kernel time), 400-move sample (3.5x basis+null, identical maps), full-key audit, full --all before/after runs, package verify.py controls.", + "author": "thakrarsagar", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5): profiling, kernel, audit, controls and write-up; reviewed and submitted by thakrarsagar.", + "open_questions": [ + { + "question": "Can Frames.dims (mod-p Echelon rank in check_lifted) be made faster with identical ranks?", + "why_it_matters": "After this change it is the largest serial part of Exact.__init__, paid before the worker pool starts.", + "first_step": "Install a packed or batched mod-Q31 elimination behind the same runtime-install/audit pattern and audit all 112,920 _rank calls.", + "blocked_by": "Nothing; needs its own equality audit." + }, + { + "question": "Should the parent build shared source-key bases once before forking the pool?", + "why_it_matters": "Workers rebuild overlapping source-key bases; copy-on-write sharing removes the duplicate work.", + "first_step": "Measure source-key overlap across the current chunks and the parent RSS for prebuilt bases.", + "blocked_by": "Memory on CI runners if all 86,789 bases are prebuilt." + }, + { + "question": "Do bit-reuse-147 and gauge-recycling replays, which also use PR97 null_exact via frames147.Exact, benefit from the same installer?", + "why_it_matters": "The kernel is shared, so the same identical-output speedup may apply.", + "first_step": "Profile make verify-bit-reuse-147 and measure its null_exact share.", + "blocked_by": "Each verifier pins its own sources and needs its own pin update and review." + } + ] +} diff --git a/research/recycled-bit-nesting-reuse/VERIFY.json b/research/recycled-bit-nesting-reuse/VERIFY.json new file mode 100644 index 0000000000..782f7e3473 --- /dev/null +++ b/research/recycled-bit-nesting-reuse/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "references/partial-gauge/pr97/check_lifted.py", + "references/partial-gauge/pr97/linalg.py", + "research/bit-reuse-147/frames147.py", + "research/recycled-bit-integration/certificate.json", + "research/recycled-bit-integration/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "null_exact_ff == PR97 linalg.null_exact on 3012 structured/random matrices; fast prim == frames147.prim; fallback on Fraction/ragged input; controls: sign-flipped/non-primitive kernel rows differ, VERIFY_NULL=audit rejects a wrong kernel, non-nested move reported, degenerate frame rejected, certificate pins the current verify.py. Expected last line PASS_RECYCLED_BIT_NULL_KERNEL." + } + ] +} diff --git a/research/recycled-bit-nesting-reuse/verify.py b/research/recycled-bit-nesting-reuse/verify.py new file mode 100644 index 0000000000..d8c1c2ffe7 --- /dev/null +++ b/research/recycled-bit-nesting-reuse/verify.py @@ -0,0 +1,135 @@ +#!/usr/bin/env python3 +"""Bounded differential check of the fraction-free null_exact kernel used by recycled-bit-integration/verify.py. + +thakrarsagar, with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. + +Checks (seconds, stdlib only): + 1. null_exact_ff(A, k) == PR97 linalg.null_exact(A, k) (list equality of integer rows) on structured edge + cases and a deterministic random family: empty input, k = 0/1, zero rows, rank-deficient stacks, + 0/1 and +-1 entries, and entries up to 2^80; + 2. the installed fast prim equals frames147.prim on integer rows; non-integer or ragged input falls back + to the original functions (same output, same exception); + 3. install_null_kernel patches linalg, check_lifted and frames147 in place, and VERIFY_NULL=audit catches a + kernel whose output differs from the reference; + 4. negative controls: a sign-flipped kernel row and a non-primitive row differ from the reference; with the + fast kernel installed, check_moves reports a non-nested move and the nondegeneracy predicate rejects a + degenerate frame; the certificate pins the current verify.py bytes, not the base bytes. +This is a finite differential test plus a structural argument (see README); the full-input equality audit and +the full `--all` replay are recorded in README, not re-run here. +""" +import sys +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') +from fractions import Fraction +from hashlib import sha256 +import json +import os +from pathlib import Path +import random + +ROOT = Path(__file__).resolve().parents[2] +PR97 = ROOT / 'references/partial-gauge/pr97' +os.environ.pop('VERIFY_NULL', None) +sys.path.insert(0, str(ROOT / 'research/bit-reuse-147')) +sys.path.insert(0, str(ROOT / 'research/recycled-bit-integration')) +import verify as V # research/recycled-bit-integration/verify.py (main() is not run) +assert Path(V.__file__).resolve() == ROOT / 'research/recycled-bit-integration/verify.py', V.__file__ +import frames147 +REF_PRIM = frames147.prim +sys.path.insert(0, str(PR97)) +import linalg +import check_lifted +REF_NULL = linalg.null_exact +BASE_VERIFY_SHA = 'a5508f429d0ff6d441d9d07f6d1f9a83ce2335eb59b2041abbc65327b6a4a0b9' + + +def cases(seed=20261015, count=3000): + yield from [([], 0), ([], 1), ([], 4), ([[0]], 1), ([[7]], 1), ([[0, 0, 0]], 3), ([[0, 0], [0, 0]], 2), + ([[1, 2, 3]], 3), ([[-2, 4, -6], [1, -2, 3]], 3), ([[0, 3, 0, -6], [0, 0, 0, 0]], 4), + ([[1, 0], [0, 1], [1, 1]], 2), ([[2**90, -3], [5, 2**70]], 2)] + rng = random.Random(seed) + for _ in range(count): + k = rng.randint(1, 30); m = rng.randint(0, 35) + lo, hi = rng.choice([(0, 1), (-1, 1), (-3, 3), (-10**6, 10**6), (-2**80, 2**80)]) + dens = rng.choice([0.1, 0.3, 0.6, 1.0]) + A = [[rng.randint(lo, hi) if rng.random() < dens else 0 for _ in range(k)] for _ in range(m)] + if m > 2 and rng.random() < 0.4: + for _ in range(rng.randint(1, 5)): + u, v = rng.sample(range(m), 2); cu, cv = rng.randint(-5, 5), rng.randint(-5, 5) + A.append([cu * x + cv * y for x, y in zip(A[u], A[v])]) + rng.shuffle(A) + yield A, k + + +def main(): + n = nonempty = 0 + for A, k in cases(): + out = V.null_exact_ff(A, k) + assert out == REF_NULL(A, k), ('kernel mismatch', A, k) + assert all(type(x) is int for r in out for x in r) + n += 1; nonempty += bool(out) + print('PASS null_exact_ff == linalg.null_exact on %d matrices (%d with a nonzero kernel)' % (n, nonempty)) + + assert V.install_null_kernel(PR97, 'fast') == 'fast' + fast_null, fast_prim = linalg.null_exact, frames147.prim + assert check_lifted.null_exact is fast_null and fast_null is not REF_NULL and fast_prim is not REF_PRIM + rng = random.Random(7); m = 0 + for _ in range(20000): + r = [rng.randint(-60, 60) * rng.randint(0, 1) for _ in range(rng.randint(0, 25))] + assert fast_prim(r) == REF_PRIM(r) and all(type(x) is int for x in fast_prim(r)); m += 1 + frac = [[Fraction(1, 2), Fraction(-3, 4), 0]] + assert fast_null(frac, 3) == REF_NULL(frac, 3) and fast_prim(frac[0]) == REF_PRIM(frac[0]) + for bad in ([[1, 2]], 3), ([[1, 2, 3, 4]], 3): + errs = [] + for f in (fast_null, REF_NULL): + try: errs.append(('ok', f(*bad))) + except Exception as e: errs.append(type(e).__name__) + assert errs[0] == errs[1], ('ragged fallback', bad, errs) + print('PASS installed fast prim on %d rows; Fraction and ragged input fall back to the reference' % m) + + # negative controls on the kernel + A = [[1, 2, 3, 4], [2, 0, 1, 1]] + flipped = [[-x for x in r] for r in V.null_exact_ff(A, 4)] + scaled = [[2 * x for x in r] for r in V.null_exact_ff(A, 4)] + assert flipped != REF_NULL(A, 4) and scaled != REF_NULL(A, 4) + assert V.install_null_kernel(PR97, 'audit') == 'audit' + assert linalg.null_exact(A, 4) == REF_NULL(A, 4) + saved = V.null_exact_ff + V.null_exact_ff = lambda A, k: [[-x for x in r] for r in saved(A, k)] + try: + linalg.null_exact(A, 4) + raise SystemExit('FAIL audit mode accepted a sign-flipped kernel') + except AssertionError as e: + assert 'null_exact kernel mismatch' in str(e.args[0]) + finally: + V.null_exact_ff = saved + print('PASS controls: sign-flipped and non-primitive kernel rows differ; VERIFY_NULL=audit rejects a wrong kernel') + + # predicates with the fast kernel installed (synthetic frames; Exact.__init__ is not run) + V.install_null_kernel(PR97, 'fast') + E = object.__new__(frames147.Exact) + E.h = h = 23; E.null_exact = linalg.null_exact; E.rank_mod = linalg.rank_mod; E.Q31 = linalg.Q31 + E.full = [[int(i == j) for j in range(h)] for i in range(h)]; E._null = {} + e = lambda i: [int(j == i) for j in range(h)] + E._basis = {('x', 'small'): [[1, 1] + [0] * 21], + ('x', 'big'): [e(0), e(1), [0, 0, 1, 1, -2] + [0] * 18], + ('x', 'degenerate'): [[1] * 9 + [0] * 14]} + assert V.check_moves(E, [('r', ('x', 'small'), ('x', 'big'))]) == [] + assert V.check_moves(E, [('r', ('x', 'big'), ('x', 'small'))]) == [('r', ('x', 'big'), ('x', 'small'))] + assert E.null(('x', 'big')) == REF_NULL(E._basis[('x', 'big')], h) + assert E.nondegenerate(('x', 'small')) and not E.nondegenerate(('x', 'degenerate')) + bad = V.check_moves(E, [('r', ('x', 'small'), ('x', 'big')), ('r', ('x', 'degenerate'), ('x', 'big'))], + nondegenerate=True) + assert bad == [('r', ('x', 'degenerate'), ('x', 'big'))], bad + print('PASS controls: non-nested move reported, degenerate frame rejected (fast kernel installed)') + + cert = json.loads((ROOT / 'research/recycled-bit-integration/certificate.json').read_text()) + pin = cert['source_sha256']['research/recycled-bit-integration/verify.py'] + now = sha256((ROOT / 'research/recycled-bit-integration/verify.py').read_bytes()).hexdigest() + assert pin == now != BASE_VERIFY_SHA and V.sources()['research/recycled-bit-integration/verify.py'] == pin + print('PASS certificate pins the current verify.py (%s...), not the base bytes (%s...)' % (pin[:12], BASE_VERIFY_SHA[:12])) + print('PASS_RECYCLED_BIT_NULL_KERNEL') + + +if __name__ == '__main__': + main() From a0ffc1520ceae5d2174959aeb0023687c4c3fb79 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 18:51:53 +0530 Subject: [PATCH 2/3] recycled-bit-nesting-reuse: record full-key audit, full before/after runs, bench.py Complete full-key equality audit (145,513 null_exact + 1,683,853 prim calls identical) and back-to-back full --all runs (VERIFY_JOBS=3): nesting stage 410 s -> 226 s wall, same five PASS lines and certificate. Add the reproducible audit/timing harness bench.py. Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Co-Authored-By: Claude Opus 5.5 --- research/recycled-bit-nesting-reuse/README.md | 25 ++++-- research/recycled-bit-nesting-reuse/TASK.json | 2 +- research/recycled-bit-nesting-reuse/bench.py | 82 +++++++++++++++++++ 3 files changed, 102 insertions(+), 7 deletions(-) create mode 100644 research/recycled-bit-nesting-reuse/bench.py diff --git a/research/recycled-bit-nesting-reuse/README.md b/research/recycled-bit-nesting-reuse/README.md index 4acffea26c..6909f6403d 100644 --- a/research/recycled-bit-nesting-reuse/README.md +++ b/research/recycled-bit-nesting-reuse/README.md @@ -26,8 +26,8 @@ extra informational line, `null_exact kernel: fast`. reduce each row by the earlier pivot rows, take its first nonzero entry as the pivot, then clear that column in the earlier rows. By induction, every stored integer row is a nonzero rational multiple of the Fraction row at the same step, with the pivot kept positive. So the pivot columns are the same, and the free columns come in the same -increasing order. For each free column f, the integer vector has `x_f = lcm(pivots)` and -`x_pc = -b[f] * lcm / b[pc]`. This is a positive multiple of the Fraction vector (`x_f = 1`, `x_pc = -b[f]/b[pc]`). +increasing order. For each free column f, the integer vector has `x_f = lcm` (the lcm of the pivot values `b[pc]` +of the rows with `b[f] != 0`) and `x_pc = -b[f] * lcm / b[pc]`. This is a positive multiple of the Fraction vector (`x_f = 1`, `x_pc = -b[f]/b[pc]`). `linalg.primitive` maps a vector to the unique primitive integer multiple with the same sign, so dividing by the gcd returns the same list of rows. `prim` on integer rows equals `x // gcd`. The equality was also measured: see below. @@ -37,14 +37,21 @@ below. All runs were on one shared host (4 CPUs, Python 3.14.4, `nice -n 10`), on the pinned base input. Timings in the same row come from the same process, or from back-to-back runs, so they compare the same input. Other sessions were running on the host, so the absolute times are noisy. +An earlier fast run, made while the host was more heavily loaded (a profiler and this package's check were +also running), took 284 s for the stage and 304 s in total. The `null_exact` fallback path (non-integer or ragged +input) was not counted separately. A fallback call runs the reference kernel itself, so it cannot cause a +mismatch. +A repeat of the committed `bench.py` on a less loaded host, stopped before the full-key loop, gave these figures. +The init kernel time went from 15.66 s to 1.90 s (8.2x). The sample basis + null time went from 2.92 s / 2.86 s to +0.95 s / 0.88 s (3.1-3.3x), and the maps were again identical. | Measurement | Reference (Fraction `null_exact`) | Fast (fraction-free) | Equality | | --- | --- | --- | --- | | `null_exact` calls inside `Exact.__init__` (4,473 calls; mostly `late_frames` intersections) | 23.43 s kernel time | 2.88 s (8.1x) | all 4,473 identical | | Deterministic sample: 400 ledger moves (`random.Random(1)`), 709 keys, 345 annihilators. Basis + null, rep 1 / rep 2 | 4.50 s / 3.88 s | 1.25 s / 1.11 s (3.5-3.6x) | basis and null maps identical | | Same sample, `inside` dot products | 0.024 / 0.034 s | 0.024 / 0.025 s | — | -| Full-key audit (one process, both kernels on every call): every distinct basis key and every target annihilator of the 202,190 ledger moves | FULLKEY_REF | FULLKEY_FAST | FULLKEY_EQ | -| Full `--all` replay, `VERIFY_JOBS=3`, wall time of the nesting stage / whole run | FULLREF | FULLFAST | five PASS lines, kappa=472154791/10^12, certificate equal | +| Full-key audit (one process, both kernels on every call): basis of all 86,789 distinct ledger-move keys, then the annihilator of all 85,017 distinct targets | `null_exact`: 145,513 calls, 381.0 s; `prim`: 1,683,853 calls, 70.6 s | 48.7 s (7.8x); 3.6 s (19.6x) | all 145,513 + 1,683,853 identical (complete, not time-stopped) | +| Full `--all` replay, `VERIFY_JOBS=3`, back-to-back runs while the audit process was also running: nesting-stage wall / whole-run wall / user CPU | 410 s / 427.7 s / 825 s | 226 s / 243.5 s / 369 s (1.81x stage wall, 2.24x CPU) | both runs printed the same five PASS lines with kappa=472154791/10^12, and both matched the committed certificate | **Profile of the stage (before).** The cProfile figures are inflated by profiling overhead. Of `Exact.__init__` (about 160 s unprofiled), `Frames.dims` takes the largest share: about 52% of the profile, almost all of it @@ -66,9 +73,14 @@ stage, so that mechanism was dropped. This is the one pivot recorded in TASK.jso python3 -B research/recycled-bit-nesting-reuse/verify.py # ~40 s; last line PASS_RECYCLED_BIT_NULL_KERNEL make verify-recycled-bit # full replay; five PASS lines, # kappa=472154791/1000000000000 -VERIFY_NULL=audit python3 research/recycled-bit-integration/verify.py --all # full replay, both kernels on every call +python3 -B research/recycled-bit-nesting-reuse/bench.py # ~13 min: init audit, sample timing, full-key audit +VERIFY_NULL=audit python3 research/recycled-bit-integration/verify.py --all # optional; both kernels on every call ``` +`bench.py` produced the audit and timing rows of the table above; its final `summary` line holds the numbers. The +`VERIFY_NULL=audit` full replay was not run end to end in this session. The bounded check exercises its assertion +path, and `bench.py` covers the same distinct inputs. + `verify.py` in this package is the bounded check. It runs 3,012 differential matrices: edge cases (empty input, k = 0/1, zero rows) and a deterministic random family (rank-deficient stacks, entries from {0,1} up to 2^80). It runs 20,000 `prim` rows and checks the fallback on Fraction and ragged input. It also runs these negative controls, @@ -89,7 +101,8 @@ which must fail: * The identity argument above is a proof sketch in this README, not a formal proof. The empirical evidence is finite: the full-key audit recorded above, the init audit and the differential tests. * Coverage: the call set audited was {all 4,473 init calls} and {basis of every distinct key, null of every - distinct target} in the order described above. Bases depend only on their keys, so these are the distinct + distinct target}. The 8,991 keys of the 4,878 fresh moves are a subset of the ledger keys, and the fresh moves + are a subset of the ledger moves. Bases depend only on their keys, so these are the distinct `null_exact` inputs of the `--all` path. Worker processes call the same functions on the same keys. * CI wall time was not measured. The full runs used `VERIFY_JOBS=3` on a loaded host, so no CI speedup factor is claimed. Sibling PR #2361 (CI selection) would run this job less often. The speedup still matters for diff --git a/research/recycled-bit-nesting-reuse/TASK.json b/research/recycled-bit-nesting-reuse/TASK.json index 9a31683aa8..8131a95507 100644 --- a/research/recycled-bit-nesting-reuse/TASK.json +++ b/research/recycled-bit-nesting-reuse/TASK.json @@ -47,7 +47,7 @@ "budget_minutes": 90, "stop_rule": "Stop and submit a profiling note instead of a code change if the fast kernel gives < 1.5x on the sampled basis+null workload, if any output differs from the reference null_exact, or if the full after-run cannot finish by 2026-10-15T13:40:15Z (then report subset-only results).", "outcome": "completed", - "evidence": "See README Measurements: init-call audit (4,473 calls identical, 8.1x kernel time), 400-move sample (3.5x basis+null, identical maps), full-key audit, full --all before/after runs, package verify.py controls.", + "evidence": "Same host, same pinned input: init audit 4,473 null_exact calls identical (kernel 23.43 s -> 2.88 s); 400-move sample basis+null 4.50/3.88 s -> 1.25/1.11 s with identical maps; complete full-key audit 145,513 null_exact + 1,683,853 prim calls identical (381.0 s -> 48.7 s; 70.6 s -> 3.6 s); full --all with VERIFY_JOBS=3: nesting stage 410 s -> 226 s wall (whole run 427.7 s -> 243.5 s; user CPU 825 s -> 369 s), same five PASS lines and kappa, certificate equal. Bounded package check with negative controls: research/recycled-bit-nesting-reuse/verify.py. CI wall time not measured.", "author": "thakrarsagar", "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5): profiling, kernel, audit, controls and write-up; reviewed and submitted by thakrarsagar.", "open_questions": [ diff --git a/research/recycled-bit-nesting-reuse/bench.py b/research/recycled-bit-nesting-reuse/bench.py new file mode 100644 index 0000000000..ccb7ef1201 --- /dev/null +++ b/research/recycled-bit-nesting-reuse/bench.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python3 +"""Equality audit and same-process before/after timing of the null_exact/prim kernels on the pinned h=23 input. + +thakrarsagar, with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +Usage: python3 -B research/recycled-bit-nesting-reuse/bench.py [STOP_UTC_ISO] (about 13 min, about 1.3 GB RSS; not part +of the bounded check). Builds Exact once with both kernels on every call (init audit). It then times a deterministic +400-move sample with each kernel in turn, and audits the basis of every distinct ledger-move key and the annihilator +of every distinct target. An optional STOP time ends the full-key audit early, and the output reports PARTIAL. +""" +import sys, time, random, json, hashlib, resource +from datetime import datetime, timezone +from pathlib import Path +ROOT = str(Path(__file__).resolve().parents[2]) +sys.path.insert(0, ROOT + '/research/bit-reuse-147'); sys.path.insert(0, ROOT + '/research/recycled-bit-integration') +import verify as V, word147, frames147 +assert V.__file__.startswith(ROOT + "/research/recycled-bit-integration"), V.__file__ +STOP = datetime.fromisoformat(sys.argv[1]) if len(sys.argv) > 1 else None +t0 = time.time() +_, W, _, S, record, folder = word147.load_schedule() +plan = json.load(open(ROOT + '/research/recycled-bit-integration/plan.json')) +word = word147.Word(S, plan['elim'], plan['retained'], plan['pairs']); led = word.ledger(); fresh = word.new_moves(led) +moves = led['moves']; print('ledger', len(moves), 'fresh', len(fresh), flush=True) +sys.path.insert(0, str(folder)); import linalg, check_lifted as cl +ref_null, ref_prim = linalg.null_exact, frames147.prim +V.install_null_kernel(folder, 'fast'); fast_null, fast_prim = linalg.null_exact, frames147.prim +st = dict(nc=0, nref=0.0, nfast=0.0, pc=0, pref=0.0, pfast=0.0) +def null_a(A, k): + a = time.perf_counter(); o = ref_null(A, k); b = time.perf_counter(); f = fast_null(A, k); c = time.perf_counter() + assert f == o, ('MISMATCH', A, k) + st['nc'] += 1; st['nref'] += b - a; st['nfast'] += c - b; return o +def prim_a(r): + a = time.perf_counter(); o = ref_prim(r); b = time.perf_counter(); f = fast_prim(r); c = time.perf_counter() + assert f == o and all(type(x) is int for x in f), ('MISMATCH prim', r) + st['pc'] += 1; st['pref'] += b - a; st['pfast'] += c - b; return o +def set_kernels(n, p): linalg.null_exact = cl.null_exact = n; frames147.prim = p +set_kernels(null_a, prim_a) +t = time.time(); E = frames147.Exact(S, W, folder); print('init (audit both kernels)', round(time.time() - t, 1), 's', dict(st), flush=True) +init_st = dict(st) +# deterministic 400-move sample (seed 1), end-to-end before/after in this process +rng = random.Random(1); samp = rng.sample(sorted(moves, key=str), 400) +keys = sorted({a for _, a, b in samp} | {b for _, a, b in samp}, key=str) +def run_sample(): + E._basis.clear(); E._null.clear(); E.null_exact = linalg.null_exact + t = time.perf_counter() + for k in keys: E.basis(k) + tb = time.perf_counter() - t; t = time.perf_counter() + for _, a, b in samp: + B = E.basis(b) + if B and len(B) < E.h: E.null(b) + tn = time.perf_counter() - t; t = time.perf_counter() + ok = all(E.inside(a, b) for _, a, b in samp); ti = time.perf_counter() - t + return tb, tn, ti, ok, dict(E._basis), dict(E._null) +res = {} +for rep in range(2): + for name, nk, pk in (('reference', ref_null, ref_prim), ('fast', fast_null, fast_prim)): + set_kernels(nk, pk); tb, tn, ti, ok, Bd, Nd = run_sample() + res.setdefault(name, []).append((round(tb, 3), round(tn, 3), round(ti, 3))) + assert ok; res[name + '_maps'] = (Bd, Nd) + print('sample', name, 'basis', round(tb, 3), 'null', round(tn, 3), 'inside', round(ti, 3), flush=True) +assert res['reference_maps'] == res['fast_maps']; print('sample maps identical: keys', len(keys), 'nulls', len(res['fast_maps'][1]), flush=True) +del res['reference_maps'], res['fast_maps'] +# full-key audit: every distinct basis key and every distinct target annihilator of the 202,190 ledger moves +set_kernels(null_a, prim_a); E.null_exact = null_a; E._basis.clear(); E._null.clear() +for k in st: st[k] = 0 if isinstance(st[k], int) else 0.0 +allkeys = sorted({a for _, a, b in moves} | {b for _, a, b in moves}, key=str) +targets = sorted({b for _, a, b in moves}, key=str) +done_b = done_n = 0; complete = False +for k in allkeys: + if STOP and datetime.now(timezone.utc) >= STOP: break + E.basis(k); done_b += 1 + if done_b % 10000 == 0: print('basis audited', done_b, dict(st), flush=True) +else: + for b in targets: + if STOP and datetime.now(timezone.utc) >= STOP: break + B = E.basis(b) + if B and len(B) < E.h: E.null(b) + done_n += 1 + else: complete = True +print('FULL-KEY AUDIT', 'complete' if complete else 'PARTIAL (time stop)', 'basis keys', done_b, '/', len(allkeys), + 'targets', done_n, '/', len(targets), 'calls', dict(st), flush=True) +print('summary', json.dumps(dict(init=init_st, sample=res, keys=len(allkeys), targets=len(targets), + maxrss_mb=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss // 1024, total_s=round(time.time() - t0, 1))), flush=True) From 222063b96ec1a109a8c9f40e5d615498a737c6dd Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Thu, 15 Oct 2026 19:23:49 +0530 Subject: [PATCH 3/3] recycled-bit-nesting-reuse: address review (input materialisation, trust scope, credits) - null_fast/prim_fast materialise their input before the type check; re-pin verify.py (e8da17f2...). - README: speedup given as ~1.44-1.81x from one pair on a loaded host (before = VERIFY_NULL=reference); late_frames time bound for the negative result; trusted-base shift and dropped-vector gap stated; 52 historical receipts; 6fd436d0d precedent and base pins; Python 3.12 replay not run; PR97 credit to Zhihao Chen / jacklightChen; Open next question 4 (fail-closed guard). - Reran package check and make verify-recycled-bit: same PASS lines, kappa=472154791/10^12. Co-Authored-By: Claude Opus 5.5 --- .../recycled-bit-integration/certificate.json | 2 +- research/recycled-bit-integration/verify.py | 2 + research/recycled-bit-nesting-reuse/README.md | 40 +++++++++++++++---- research/recycled-bit-nesting-reuse/TASK.json | 2 +- 4 files changed, 37 insertions(+), 9 deletions(-) diff --git a/research/recycled-bit-integration/certificate.json b/research/recycled-bit-integration/certificate.json index 114c40f5ae..cd0d740b30 100644 --- a/research/recycled-bit-integration/certificate.json +++ b/research/recycled-bit-integration/certificate.json @@ -335,7 +335,7 @@ "research/recycled-bit-integration/plan.json": "ab8887e5d852fdce16a883a1ffc3173e109708a484b986cb2574e1ee634bf784", "research/recycled-bit-integration/row.json": "075c8ff2f9f1b25f6b81dc0c6ec31adc766944cb59badc4bc6e42668993ca073", "research/recycled-bit-integration/selection146.json": "407fac7fc3f3497ddf347fc7a820a6b863c2147d18f1be325b57d37998475a3e", - "research/recycled-bit-integration/verify.py": "3299094e922fa45fc82a3a68634515df2340c0bbdb8d2faf1c71d90bfbf37d18", + "research/recycled-bit-integration/verify.py": "e8da17f2b9a06d33c38cd3fea515fc9f5b1cf04ab6d5de0ed8451c65bbb85a8a", "scripts/paired_cube_bit.py": "677ff674f48860336ca96c4ab6d7fa9053bf7137d20ba368445d20e236765dbe", "scripts/paired_cube_network.py": "293662b7f8772dd398399a1c19966faf7d155f024543d0c06601eabb800f35cf", "scripts/structured_bulk_assembly.py": "e99467e14211fba699878ed036e1e2362eb8e395dc22f9ecdcecc7fbf2cc736d", diff --git a/research/recycled-bit-integration/verify.py b/research/recycled-bit-integration/verify.py index 19d42495c6..da8d6bb1fc 100644 --- a/research/recycled-bit-integration/verify.py +++ b/research/recycled-bit-integration/verify.py @@ -122,12 +122,14 @@ def install_null_kernel(folder, mode=None): def integral(A, k): return all(len(r) == k and all(type(x) is int for x in r) for r in A) def null_fast(A, k): + A = [list(r) for r in A] # materialise once, so one-shot iterables are not consumed by the type check return null_exact_ff(A, k) if integral(A, k) else ref_null(A, k) def null_audit(A, k): out = ref_null(A, k) assert null_fast(A, k) == out, ('null_exact kernel mismatch', A, k) return out def prim_fast(r): + r = list(r) for x in r: if type(x) is not int: return ref_prim(r) g = gcd(*r) diff --git a/research/recycled-bit-nesting-reuse/README.md b/research/recycled-bit-nesting-reuse/README.md index 6909f6403d..b06c0aedf3 100644 --- a/research/recycled-bit-nesting-reuse/README.md +++ b/research/recycled-bit-nesting-reuse/README.md @@ -51,7 +51,7 @@ The init kernel time went from 15.66 s to 1.90 s (8.2x). The sample basis + null | Deterministic sample: 400 ledger moves (`random.Random(1)`), 709 keys, 345 annihilators. Basis + null, rep 1 / rep 2 | 4.50 s / 3.88 s | 1.25 s / 1.11 s (3.5-3.6x) | basis and null maps identical | | Same sample, `inside` dot products | 0.024 / 0.034 s | 0.024 / 0.025 s | — | | Full-key audit (one process, both kernels on every call): basis of all 86,789 distinct ledger-move keys, then the annihilator of all 85,017 distinct targets | `null_exact`: 145,513 calls, 381.0 s; `prim`: 1,683,853 calls, 70.6 s | 48.7 s (7.8x); 3.6 s (19.6x) | all 145,513 + 1,683,853 identical (complete, not time-stopped) | -| Full `--all` replay, `VERIFY_JOBS=3`, back-to-back runs while the audit process was also running: nesting-stage wall / whole-run wall / user CPU | 410 s / 427.7 s / 825 s | 226 s / 243.5 s / 369 s (1.81x stage wall, 2.24x CPU) | both runs printed the same five PASS lines with kappa=472154791/10^12, and both matched the committed certificate | +| Full `--all` replay, `VERIFY_JOBS=3`, back-to-back runs while the audit process was also running: nesting-stage wall / whole-run wall / user CPU | 410 s / 427.7 s / 825 s | 226 s / 243.5 s / 369 s (1.81x stage wall, 2.24x CPU; a second, more loaded fast run took 284 s, 1.44x). This is one before/after pair on a loaded host; the before-run is `VERIFY_NULL=reference` on the patched `verify.py`, which installs the original PR97 kernel | both runs printed the same five PASS lines with kappa=472154791/10^12, and both matched the committed certificate | **Profile of the stage (before).** The cProfile figures are inflated by profiling overhead. Of `Exact.__init__` (about 160 s unprofiled), `Frames.dims` takes the largest share: about 52% of the profile, almost all of it @@ -64,8 +64,9 @@ The new kernel removes most of that time. It does not touch `dims`, which this p **Negative result for the first hypothesis (basis reuse from `late_frames`).** The planned mechanism was to seed `Exact`'s basis memo from the `exact_basis` cache that `check_lifted.late_frames` builds and then throws away. That cache holds 2,230 keys. The ledger moves use 86,789 distinct keys (n 64,042; v 11,374; sigma 8,181; -out 1,771; c 1,396; ret 23; '0' 1; F 1), so the cache covers 2.6% of them. Reuse alone cannot materially shorten the -stage, so that mechanism was dropped. This is the one pivot recorded in TASK.json. +out 1,771; c 1,396; ret 23; '0' 1; F 1), so the cache covers 2.6% of them. Key count is not cost, so the cost bound is this: every `exact_basis` result the cache could supply was computed +inside `late_frames`, whose total is about 25.5 s per process (unprofiled). Reuse therefore saves at most about +6% of the 410 s stage, so that mechanism was dropped. This is the one pivot recorded in TASK.json. ## Reproduce @@ -107,8 +108,28 @@ which must fail: * CI wall time was not measured. The full runs used `VERIFY_JOBS=3` on a loaded host, so no CI speedup factor is claimed. Sibling PR #2361 (CI selection) would run this job less often. The speedup still matters for `make verify`, scheduled runs and relevant PRs. -* Historical receipts under `research/community-efficient1000-audit/checks/` record the old `verify.py` sha - (`a5508f42...`) as snapshots. No live verifier re-hashes them. They are left unchanged as historical evidence. +* Historical receipts record the old pins as snapshots: 52 JSON files across + `research/community-efficient{200,...,1000}-audit/` contain both the base `verify.py` sha (`a5508f42...`) and the + base `certificate.json` sha (`4004ea4c...`). No live verifier, test, script or workflow re-hashes them + (`research/pr946-pin-migration` scans its own pinned base commit). They are left unchanged as historical evidence. +* Trusted base: in the default (fast) mode, acceptance of the exact rational nesting check now depends on the new + `null_exact_ff`, not on the reviewed PR97 kernel. Its equivalence rests on (a) the proof sketch above and + (b) the recorded complete audit on the pinned input. The end-to-end replay does not detect an *incomplete* + kernel by itself: a reviewer mutant that dropped the last null vector still passed, because `inside()` only + becomes more permissive (a perturbed entry, by contrast, fails PR97 `exact_basis`). The package check + (`research/recycled-bit-nesting-reuse/verify.py`) is the guard, and CI runs it only when this package changes. + Maintainers may wish to run `VERIFY_NULL=audit` periodically or add a fail-closed completeness guard (Open next + question 4). +* `sources()` of `recycled-bit-integration` does not pin `references/partial-gauge/pr97/linalg.py` or + `check_lifted.py` (pre-existing). This package's SOURCES.json pins them at the base bytes; widening the + certificate pins is left out of this focused change. +* Editing the live `recycled-bit-integration` verifier and its own certificate pin follows the precedent of + 6fd436d0d (the cherry-pick of PR218), and needs maintainer acceptance. Base pins of the two modified files: + `verify.py` `a5508f42...` -> current pin in `certificate.json`; `certificate.json` base `4004ea4c...`. +* Python: all checks ran on Python 3.14.4. The registered Python 3.12 replay in VERIFY.json was not run locally + (no 3.12 on the host); CI 3.11/3.13 were not run locally either. +* The wrappers materialise their input (`[list(r) for r in A]`, `list(r)`) before the type check, so one-shot + iterables are handled like the reference; every call site in this path passes lists. ## Open next questions @@ -125,12 +146,17 @@ which must fail: `research/gauge-recycling/verify.py`, `check_lifted.py` itself) benefit from the same installer? *Why:* the kernel is shared. *First step:* profile `make verify-bit-reuse-147` and check its share of `null_exact`. *Blocked by:* each verifier pins its own sources, so each would need its own pin update and review. +4. *Question:* should `null_fast` fail closed on an incomplete or wrong kernel? *Why:* the end-to-end replay + tolerates a dropped null vector (see Scope). *First step:* assert that each output row annihilates `A` and that + `len(out) >= k - rank_mod(A, Q31)` (rank mod p is at most rank over Q, and the outputs are independent by their + free-column structure), then measure the overhead. *Blocked by:* nothing; it changes `verify.py` and its pin again. ## Credit * `research/recycled-bit-integration`: Douglas Colkitt, with OpenAI Codex assistance. It composes Thomas Marchand - (#146), William Porter (#147), gupt1156 (#148) and DaysSky (#150), per its `SOURCE.json`. -* PR97 `check_lifted.py` / `linalg.py`: Swapnil Jain. + (#146), William Porter (#147), Rohan Gupta / gupt1156 (#148) and DaysSky (#150), per its `SOURCE.json`. +* PR97 snapshot (Zhihao Chen / jacklightChen; imported under `references/partial-gauge/pr97`): `check_lifted.py` / + `linalg.py` frame/lifted checking sources by Swapnil Jain. * Fork-pool parallelization of this stage: Joel Pulikkan / GamingPuzzled (PR218, cherry-picked as 6fd436d0d). * Related verifier speedups with an exact method: CubeJerry (PR1461, annihilator containment for the h=10/12 audits) and RichardHoekstra (PR239, `rational_span_frames` nondegeneracy). diff --git a/research/recycled-bit-nesting-reuse/TASK.json b/research/recycled-bit-nesting-reuse/TASK.json index 8131a95507..86d1aa6a74 100644 --- a/research/recycled-bit-nesting-reuse/TASK.json +++ b/research/recycled-bit-nesting-reuse/TASK.json @@ -47,7 +47,7 @@ "budget_minutes": 90, "stop_rule": "Stop and submit a profiling note instead of a code change if the fast kernel gives < 1.5x on the sampled basis+null workload, if any output differs from the reference null_exact, or if the full after-run cannot finish by 2026-10-15T13:40:15Z (then report subset-only results).", "outcome": "completed", - "evidence": "Same host, same pinned input: init audit 4,473 null_exact calls identical (kernel 23.43 s -> 2.88 s); 400-move sample basis+null 4.50/3.88 s -> 1.25/1.11 s with identical maps; complete full-key audit 145,513 null_exact + 1,683,853 prim calls identical (381.0 s -> 48.7 s; 70.6 s -> 3.6 s); full --all with VERIFY_JOBS=3: nesting stage 410 s -> 226 s wall (whole run 427.7 s -> 243.5 s; user CPU 825 s -> 369 s), same five PASS lines and kappa, certificate equal. Bounded package check with negative controls: research/recycled-bit-nesting-reuse/verify.py. CI wall time not measured.", + "evidence": "Same host, same pinned input: init audit 4,473 null_exact calls identical (kernel 23.43 s -> 2.88 s); 400-move sample basis+null 4.50/3.88 s -> 1.25/1.11 s with identical maps; complete full-key audit 145,513 null_exact + 1,683,853 prim calls identical (381.0 s -> 48.7 s; 70.6 s -> 3.6 s); full --all with VERIFY_JOBS=3: nesting stage 410 s -> 226 s wall, about 1.44-1.81x from one before/after pair on a loaded host, before-run = VERIFY_NULL=reference on the patched file (whole run 427.7 s -> 243.5 s; user CPU 825 s -> 369 s), same five PASS lines and kappa, certificate equal. Bounded package check with negative controls: research/recycled-bit-nesting-reuse/verify.py. CI wall time not measured.", "author": "thakrarsagar", "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5): profiling, kernel, audit, controls and write-up; reviewed and submitted by thakrarsagar.", "open_questions": [