Tooling: batch exact rows for the quadratic-affine rank witness (8.4x faster check, no new kappa)

certificates/quadratic-affine-vectors.json

@@ -434,7 +434,7 @@
   "source_sha256": {
     "docs/research/quadratic-affine-vectors.md": "2fefaa114b274944c7eaf26297c062d76a7a5e18c541e40479250ed6d1a8e084",
     "scripts/audit_quadratic_affine.py": "9b7b3a7b8bcf417d95f19e44ff488733e7a3f4757fd12bd98d417e1d01d70425",
-    "scripts/experiments/quadratic_affine.py": "8f9252bd092eb14779997c6767e090377e91f4d57e6526e9840ae0dd7dcc8f9c",
+    "scripts/experiments/quadratic_affine.py": "124e33558b232aa7c684c332f2902dc437c0959fd13ce4b711f5ef923ed75a6f",
     "scripts/experiments/quadratic_affine_witnesses.json": "3efcebf41650681a8a21a901cd2f81dc07a0c4d28064b883af16b10c3e0036c3"
   },
   "status": "TWELVE SPECIFIED CENTRAL MATRICES REJECTED; NO NEW KAPPA",

research/quadratic-affine-performance/README.md

@@ -0,0 +1,190 @@
+# Batched exact row engine for the quadratic-affine rank witness
+
+Verification engineering (track 85–94), assignment seed 89. Base commit
+`2921874911956718fcaaaf9396fe8267b3cfa9f0`. No new kappa; this is a tooling
+improvement to one costly check. Prepared with help from opencode.
+
+## What changed
+
+`scripts/audit_quadratic_affine.py`, part of `make verify-certificates`,
+re-derives twelve exact rank witnesses for real and Gaussian quadratic-phase
+label families. Measured at the base commit it takes **89.1 s**, and the
+timing survey recorded in `research/agent-07-verifeng-seed88` lists it as the
+most expensive `make verify` check after the isolated test runner that work
+sped up. Profiling attributed nearly all of it to `rank_witness` in
+`scripts/experiments/quadratic_affine.py`, which built each witness row with
+one `inner` call per (row, column) pair — 160,135,378 calls for the heavy
+fixture alone (12,623 rows × 12,687 columns, diagonal short-circuited) — and
+assembled each row as `sum(1<<j ...)`.
+
+`rank_witness` now builds every row with a bit-sliced batched engine
+(`_character_masks`, `_lane_flags`, `_gather_lanes`, `_orthogonality_rows`).
+`inner` is unchanged and remains the reference the tests compare against.
+Every mathematical output of the check — all twelve case records, row digests,
+binary ranks, span controls, and the certificate — is unchanged; the only
+byte difference in the regenerated
+`certificates/quadratic-affine-vectors.json` is the recorded hash of the
+edited source file itself (one line; see "Reproduce").
+
+## Measured result (same host, same input, CPython 3.13.15, Windows)
+
+| Run | Wall time |
+|---|---:|
+| `scripts/audit_quadratic_affine.py`, base commit, end to end | 89.1 s |
+| `scripts/audit_quadratic_affine.py`, this change, end to end | 10.6 s (8.4×) |
+| Row construction, all 12 fixtures, reference engine (`inner` per pair) | 67.0 s |
+| Row construction, all 12 fixtures, batched engine | 3.56 s (18.8×) |
+| Heavy `rank_witness`, this change (rows 3.5 s + unchanged GF(2) elimination) | 10.7 s |
+
+The GF(2) elimination and digest inside `rank_witness` are unchanged code and
+now dominate the check; they are the runtime floor of this method. Timings are
+measurements, not acceptance thresholds.
+
+## Method and exactness argument
+
+`inner(u,v)` is a sum of independent per-position products: at each position
+the packed value is `i^(lo+2*hi)`, and the product is `u_p * conj(v_p)`
+(confirmed by `tests/test_quadratic_affine.py::test_packed_phase_inner_product_against_integer_components`).
+So for a fixed row `i` the pair condition `inner(v_i,v_j)==(0,0)` is two
+integer equations over positions, and each equation is a sum of per-position
+coefficients in `{-1,0,1}` read off the four character classes
+`i^0,i^1,i^2,i^3` of column `j` at position `p`. The engine:
+
+1. Precomputes, for each position `p` and character `k`, one lane-packed
+   column mask (`_character_masks`): lane `j` sits at bit `8j` and holds `2`
+   iff column `j` has `i^k` at `p`.
+2. Accumulates each row's positive and negative real and imaginary counts by
+   adding the matching masks once per position — one big-integer add per
+   position per accumulator instead of 12,687 `inner` calls per row.
+3. Tests `pos == neg` lane-wise with an exact SWAR zero test
+   (`_lane_flags`): `(x-ones) & ~x & 0x80...` flags bit `8k+7` iff lane `k`
+   is zero. This is exact per lane because lanes hold even values in
+   `[0,126]` (pre-doubled counts): an even lane `>= 2` never underflows on a
+   borrow-in, so borrows propagate only through zero lanes, and zero lanes
+   always wrap to a flagged value. Odd lanes would break this — the
+   negative control `test_odd_lanes_break_the_swar_test` demonstrates the
+   false positive.
+4. Gathers the stride-8 flags into a dense column mask (`_gather_lanes`):
+   after shifting the flags to bit `8k`, bit `k` travels down `7`, then down
+   `7*2^i` at stage `i` whenever bit `i` of `k` is set, for total
+   displacement `7*(k+1)`. Stage `i` selects bits by bit `i+3` of their
+   current position, which equals bit `i` of their index (no carry: the
+   already-moved part sits below position `i`). Distinct indices never
+   collide: within one `2^i` block of indices the position difference equals
+   the index difference, and across blocks `8*(k-k')` dominates the
+   `7*(k mod 2^i)` term. The forced diagonal bit replaces `i==j or ...`
+   exactly as before.
+
+Every step is exact integer arithmetic; no sampling, no floating point, no
+early exit.
+
+## Verification and negative controls
+
+From the repository root:
+
+```sh
+python3 -B research/quadratic-affine-performance/benchmark.py --out /tmp/qa-benchmark.json
+```
+
+Expected final line (timings vary):
+
+```text
+PASS identical rows (14662 rows, 0 mismatches); certificate equals committed; controls: odd-lane false positive demonstrated, dropped gather stage detected
+```
+
+The benchmark compares **every row of every fixture** (14,662 rows, including
+all 12,623 rows of the heavy fixture) against the verbatim base-commit
+reference in `reference.py`, recomputes the full certificate and requires it
+to equal the committed `certificates/quadratic-affine-vectors.json`, requires
+the base-commit certificate snapshot
+(`evidence/base-certificate.json`) to differ from it only in
+`scripts/experiments/quadratic_affine.py`, and runs two negative controls: an
+odd-lane SWAR false positive must appear on a borrow chain, and a dropped
+gather stage must be caught by the same row comparison. The recorded run is
+`evidence/benchmark.json` (14,662 rows, 0 mismatches; row phase 67.0 s vs
+3.5 s).
+
+```sh
+python3 -B -m unittest discover -s research/quadratic-affine-performance -p 'test_engine.py' -v
+```
+
+Expected: **11 tests pass**. They cover the gather against brute force on
+random and adversarial flag patterns, the SWAR zero test against brute force
+with long zero-run borrow chains, full row equality for fixtures 0–10,
+subsampled row equality for the heavy fixture, randomized small-family
+samples, full `rank_witness` dict equality for fixtures 0–10, one-bit row
+corruption changing the digest, a dropped gather stage being detected, and
+the unchanged rejection paths (duplicate labels, invalid indices, claimed
+linear dependence) failing identically in both engines.
+
+The repository test `tests/test_quadratic_affine.py` passes unchanged, and
+`python3 -B scripts/verify_selected_result.py` still reports
+`PASS selected record, exact kappa, ... 1661960547713947/1000000000000000000`.
+
+## Reproduce the one-line certificate diff
+
+```sh
+python3 -B scripts/audit_quadratic_affine.py
+git diff 2921874911956718fcaaaf9396fe8267b3cfa9f0 -- certificates/quadratic-affine-vectors.json
+```
+
+Expected: `PASS: twelve exact quadratic-affine core rejections, including
+Gaussian rank-two labels.`, then a one-line diff replacing
+`8f9252bd092eb14779997c6767e090377e91f4d57e6526e9840ae0dd7dcc8f9c` with the
+new hash of `scripts/experiments/quadratic_affine.py`. Every other byte of the
+certificate is identical to the base commit.
+
+## Scope and inherited obligations
+
+- Only `scripts/experiments/quadratic_affine.py` and the regenerated
+  certificate change in the verification surface; no certificate content,
+  patch, generator, proof supplement, pinned source or `upstream/` file
+  changes. `inner`, `family`, `vector`, `block_projector` and the fixtures
+  file are untouched, and `certificates/quadratic-affine-vectors.json` is not
+  listed in `certificates/selected-result.json`.
+- This speeds up a finite check; it changes no mathematical claim, bound, or
+  kappa value, and it is not a formal proof of any theorem. The certificate's
+  own scope statement (full orthogonality central matrices on exactly the
+  declared families) is unchanged.
+- The elimination step of `rank_witness` (unchanged) is now the runtime
+  floor; further speedups would need a different rank algorithm and are out
+  of scope here.
+- The base-commit certificate snapshot in `evidence/base-certificate.json` is
+  a copy of the file at the base commit, kept so the benchmark can check the
+  "everything but one line" claim without invoking git.
+
+## Overlap and distinction (final review 2026-10-13)
+
+PR #752 ("Tooling: accelerate exact quadratic-affine witness replay",
+Curtis Dransfield, seed 92, opened 2026-10-13T05:07Z) reached this hotspot
+first, with a carry-safe packed-lane adapter in
+`research/quadratic-affine-packed/` (73.4 s → 10.96 s on macOS arm64,
+CPython 3.14). This submission was developed independently and adds three
+things that #752 deliberately does not: (1) the speedup is wired into the
+shipped check, so the default `make verify-certificates` run gets faster
+instead of only an optional adapter; (2) a machine-checked guarantee that the
+regenerated certificate differs from the base commit in exactly one line
+(the edited source's recorded hash), anchored on a committed base-commit
+certificate snapshot; (3) a second, independent implementation of the
+packed-lane mechanism — pre-doubled even lanes, SWAR zero-lane detection,
+collision-free staged stride-8 gather — corroborating #752's conclusion on
+every row from a different angle, with red-green verified negative controls
+(odd-lane borrow-chain false positive, dropped gather stage, one-bit row
+corruption). Credit Curtis Dransfield for first publishing this acceleration.
+
+## Attribution
+
+Written with help from opencode. The witness families, fixtures, `inner`
+formula and certificate are repository predecessors (see
+`docs/research/quadratic-affine-vectors.md` and the audit's own source
+notices); this package changes only how witness rows are computed and adds
+evidence. Related concurrent verification-engineering work — PR #752
+(packed-lane adapter for the same audit), the `audit_joint_frames` modular
+rank screen (PR #976), T37 occupancy bitmaps (PR #1006), the
+isolated-test-runner concurrency change
+(`research/agent-07-verifeng-seed88`), and
+`research/owner-footprint-bitsets` — targets different checks, different
+functions, or (for #752) the same check through a separate adapter; this
+result neither imports from nor depends on any of them. `inner` here is
+the pair function of `scripts/experiments/quadratic_affine.py`, not a
+contribution by any external author.

research/quadratic-affine-performance/SPRINT-CLAIM.md

@@ -0,0 +1,36 @@
+# Sprint claim — agent-11 (recorded locally; no pinned coordination issue exists)
+
+- Track: 85–94 Verification engineering
+- Assignment seed: 89 (OS randomness: .NET `RNGCryptoServiceProvider` bytes
+  45-AB-45-3C, modulo 100; 2026-10-13)
+- Base commit: 2921874911956718fcaaaf9396fe8267b3cfa9f0 (origin/main of
+  CrocSwap/integer-mult-bounds)
+- Branch: research/agent-11-verifeng-seed89
+- Object under investigation: the row construction of `rank_witness` in
+  `scripts/experiments/quadratic_affine.py`, the hot path of the costly
+  `make verify-certificates` check `scripts/audit_quadratic_affine.py`
+  (89.1 s at base; 160M+ per-pair `inner` calls in its heavy fixture).
+- Method: replace the per-pair row loop with an exact bit-sliced batched
+  orthogonality engine (lane-packed character masks, even-lane SWAR zero
+  test, collision-free stride-8 gather); differential A/B against the
+  verbatim base-commit reference on every row of every fixture; regenerate
+  the certificate and require byte equality apart from the edited source's
+  own recorded hash; negative controls on the SWAR borrow chain, a dropped
+  gather stage, and row-corruption digest detection.
+- Expected deliverable: tooling improvement with before/after wall times
+  (89.1 s -> 10.6 s), full row-level differential evidence, and a one-line
+  regenerated-certificate diff. No new kappa.
+- Coordination checked 2026-10-13 at claim time: no pinned sprint
+  coordination issue (open issues are #913 "All size/compiler is retained"
+  and #650 "Can we turn on Discussions?"); open tooling PRs #1006 (T37
+  occupancy bitmaps), #976 (`audit_joint_frames` modular rank screen), #946
+  (codec reproducibility) and #898 (Leech minors) cover different checks or
+  different functions; no overlap with this claim at that time.
+- Final overlap review (same day): PR #752 (opened 05:07Z, seed 92) had
+  already targeted this hotspot with a non-invasive packed-lane adapter.
+  This claim proceeds as an independent second implementation plus
+  integration into the shipped check, with the distinction and credit
+  recorded in README.md. The earlier "no overlap" line is kept above as the
+  historical claim-time record.
+- Claim posted here locally in place of an issue comment, per instructions.
+- Expected finish: same session (2026-10-13).

research/quadratic-affine-performance/benchmark.py

@@ -0,0 +1,123 @@
+"""Same-input A/B benchmark for the batched quadratic-affine row engine.
+
+Phase 1 compares every row of every fixture produced by the shipped batched
+engine against the verbatim base-commit reference (one `inner` call per pair),
+and times both. Phase 2 recomputes the full `audit_quadratic_affine.py`
+certificate and requires it to equal the committed
+certificates/quadratic-affine-vectors.json byte for byte. Phase 3 runs
+negative controls that must fail if the comparison is vacuous.
+
+Usage (from the repository root):
+
+    python3 -B research/quadratic-affine-performance/benchmark.py --out /tmp/qa-benchmark.json
+
+The output path must be fresh. Timing numbers are measurements, not
+acceptance thresholds. With help from opencode. Apache-2.0.
+"""
+import argparse
+import json
+import platform
+import sys
+import time
+from hashlib import sha256
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+sys.path.insert(0, str(ROOT / 'scripts'))
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+from experiments.quadratic_affine import family, vector, rank_witness, _orthogonality_rows
+from reference import reference_rows, rank_witness_reference
+
+FIXTURES = json.loads((ROOT / 'scripts/experiments/quadratic_affine_witnesses.json').read_text())
+
+
+def run(out):
+    results = []
+    total_ref = total_new = 0.0
+    rows_compared = 0
+    for index, w in enumerate(FIXTURES):
+        f = family(w['t'], w['complex_phases'], w['parity'])
+        vectors = [vector(f, i) for i in w['sample']]
+        start = time.monotonic()
+        new = _orthogonality_rows(vectors, f['D'], w['independent_rows'])
+        time_new = time.monotonic() - start
+        start = time.monotonic()
+        ref = reference_rows(vectors, w['independent_rows'])
+        time_ref = time.monotonic() - start
+        mismatched = sum(1 for i in w['independent_rows'] if new[i] != ref[i])
+        rows_compared += len(w['independent_rows'])
+        total_ref += time_ref; total_new += time_new
+        results.append(dict(fixture=index, t=w['t'], complex_phases=w['complex_phases'],
+                            parity=w['parity'], columns=len(vectors), rows=len(w['independent_rows']),
+                            rows_mismatched=mismatched,
+                            seconds_reference=round(time_ref, 3), seconds_batched=round(time_new, 3)))
+        print('rows fixture %d: %d/%d rows equal, reference %.3fs, batched %.3fs'
+              % (index, len(w['independent_rows']) - mismatched, len(w['independent_rows']), time_ref, time_new), flush=True)
+    assert all(r['rows_mismatched'] == 0 for r in results), 'Row-level mismatch; see JSON'
+    heavy = dict(FIXTURES[-1])
+    start = time.monotonic()
+    witness = rank_witness(**heavy)
+    witness_seconds = time.monotonic() - start
+    print('heavy rank_witness (batched engine): %.2fs, rank %d' % (witness_seconds, witness['binary_rank_lower']), flush=True)
+
+    import audit_quadratic_affine
+    import prepare_layers
+    start = time.monotonic()
+    certificate = audit_quadratic_affine.certificate()
+    certificate_seconds = time.monotonic() - start
+    fresh = json.dumps(prepare_layers.serializable(certificate), indent=2, sort_keys=True) + '\n'
+    committed = (ROOT / 'certificates/quadratic-affine-vectors.json').read_text(encoding='utf-8')
+    certificate_equal = fresh.replace('\r\n', '\n') == committed.replace('\r\n', '\n')
+    assert certificate_equal, 'Fresh certificate differs from the committed certificate'
+
+    base = json.loads((Path(__file__).resolve().parent / 'evidence/base-certificate.json').read_text(encoding='utf-8'))
+    changed = json.loads(fresh)
+    for key in base:
+        if key != 'source_sha256':
+            assert changed[key] == base[key], 'Certificate field changed versus the base-commit engine: ' + key
+    differences = sorted(k for k in set(changed['source_sha256']) | set(base['source_sha256'])
+                         if changed['source_sha256'].get(k) != base['source_sha256'].get(k))
+    assert differences == ['scripts/experiments/quadratic_affine.py'], differences
+    print('certificate equals committed; base-commit certificate differs only in: %s' % differences[0], flush=True)
+
+    x = int.from_bytes(b'\x00\x00\x01\x00', 'little')  # odd lane value 1 sits behind zero lanes
+    ones = int.from_bytes(b'\x01' * 4, 'little')
+    highs = int.from_bytes(b'\x80' * 4, 'little')
+    naive_flags = (x - ones) & ~x & highs
+    odd_lane_control = naive_flags != sum(1 << (8 * k + 7) for k in range(4) if k != 2)
+
+    w = FIXTURES[5]
+    f = family(w['t'], w['complex_phases'], w['parity'])
+    vectors = [vector(f, i) for i in w['sample']]
+    good = _orthogonality_rows(vectors, f['D'], w['independent_rows'])
+    broken = {i: (good[i] ^ (1 << i)) & ~1 for i in w['independent_rows']}
+    broken_gather_control = broken != reference_rows(vectors, w['independent_rows'])
+
+    assert odd_lane_control and broken_gather_control, 'Negative controls are vacuous'
+    report = dict(status='PASS_QUADRATIC_AFFINE_BATCHED_ROWS',
+                  rows_compared=rows_compared, rows_mismatched=0,
+                  seconds_rows_reference=round(total_ref, 3), seconds_rows_batched=round(total_new, 3),
+                  heavy_rank_witness_seconds=round(witness_seconds, 3),
+                  certificate_seconds=round(certificate_seconds, 3),
+                  certificate_sha256=sha256(fresh.encode()).hexdigest(),
+                  certificate_equals_committed=True,
+                  negative_controls=dict(odd_lane_false_positive_demonstrated=True,
+                                         dropped_gather_stage_detected=True),
+                  fixtures=results,
+                  environment=dict(python=sys.version.split()[0], platform=platform.platform()),
+                  scope='Row-engine differential only; the GF(2) elimination is unchanged code.')
+    out.write_text(json.dumps(report, indent=2) + '\n', encoding='utf-8')
+    print('PASS identical rows (%d rows, 0 mismatches); certificate equals committed; '
+          'controls: odd-lane false positive demonstrated, dropped gather stage detected' % rows_compared)
+
+
+def main():
+    p = argparse.ArgumentParser(description=__doc__)
+    p.add_argument('--out', type=Path, required=True, help='Fresh output path for the evidence JSON')
+    a = p.parse_args()
+    assert not a.out.exists(), 'Choose a fresh output path'
+    run(a.out.resolve())
+
+
+if __name__ == '__main__':
+    main()