diff --git a/certificates/quadratic-affine-vectors.json b/certificates/quadratic-affine-vectors.json index 18c312304c..1db5efb408 100644 --- a/certificates/quadratic-affine-vectors.json +++ b/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", diff --git a/research/quadratic-affine-performance/README.md b/research/quadratic-affine-performance/README.md new file mode 100644 index 0000000000..c21cfe1250 --- /dev/null +++ b/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<= 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. diff --git a/research/quadratic-affine-performance/SPRINT-CLAIM.md b/research/quadratic-affine-performance/SPRINT-CLAIM.md new file mode 100644 index 0000000000..e1935be933 --- /dev/null +++ b/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). diff --git a/research/quadratic-affine-performance/benchmark.py b/research/quadratic-affine-performance/benchmark.py new file mode 100644 index 0000000000..535d2cb120 --- /dev/null +++ b/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() diff --git a/research/quadratic-affine-performance/evidence/base-certificate.json b/research/quadratic-affine-performance/evidence/base-certificate.json new file mode 100644 index 0000000000..18c312304c --- /dev/null +++ b/research/quadratic-affine-performance/evidence/base-certificate.json @@ -0,0 +1,442 @@ +{ + "cases": [ + { + "binary_rank_lower": 3, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 8, + "support_dimension": 0 + }, + { + "labels": 112, + "support_dimension": 2 + } + ], + "d": 8, + "ell": 1, + "independent_row_sha256": "04205b87874457edde2d90ce2a00b55eb75135ab369b9759bc884535acf524be", + "minor_columns": 83, + "n": 120, + "normalized_dimension": "8", + "parity": 0, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 3 + }, + { + "binary_rank_lower": 3, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 56, + "support_dimension": 1 + }, + { + "labels": 64, + "support_dimension": 3 + } + ], + "d": 8, + "ell": 1, + "independent_row_sha256": "493320464010d3aa12dec1347ae01cdc1603ea54f637584f5ab8e4cfed770df9", + "minor_columns": 83, + "n": 120, + "normalized_dimension": "8", + "parity": 1, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 3 + }, + { + "binary_rank_lower": 5, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 8, + "support_dimension": 0 + }, + { + "labels": 56, + "support_dimension": 1 + }, + { + "labels": 112, + "support_dimension": 2 + }, + { + "labels": 64, + "support_dimension": 3 + } + ], + "d": 8, + "ell": 1, + "independent_row_sha256": "088559689cbb530c2daa97a8ff06951596ba6c0efcaed4d67b4ef92e5becf1b0", + "minor_columns": 85, + "n": 240, + "normalized_dimension": "8", + "parity": null, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 3 + }, + { + "binary_rank_lower": 23, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 16, + "support_dimension": 0 + }, + { + "labels": 1120, + "support_dimension": 2 + }, + { + "labels": 1024, + "support_dimension": 4 + } + ], + "d": 16, + "ell": 1, + "independent_row_sha256": "ce685a73653ff086931e69c7b43da874fab0b66242a08f568850145602202634", + "minor_columns": 103, + "n": 2160, + "normalized_dimension": "16", + "parity": 0, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 4 + }, + { + "binary_rank_lower": 23, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 240, + "support_dimension": 1 + }, + { + "labels": 1920, + "support_dimension": 3 + } + ], + "d": 16, + "ell": 1, + "independent_row_sha256": "f18c08c3ad89c72c8d1b2c14308bcb9a3f43771695f1c4e6520246a9ed4cb046", + "minor_columns": 103, + "n": 2160, + "normalized_dimension": "16", + "parity": 1, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 4 + }, + { + "binary_rank_lower": 45, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 16, + "support_dimension": 0 + }, + { + "labels": 240, + "support_dimension": 1 + }, + { + "labels": 1120, + "support_dimension": 2 + }, + { + "labels": 1920, + "support_dimension": 3 + }, + { + "labels": 1024, + "support_dimension": 4 + } + ], + "d": 16, + "ell": 1, + "independent_row_sha256": "2f0d88a49358f4078c830d30bb14ddce052ca44e909fe709b6d449540ccde74a", + "minor_columns": 125, + "n": 4320, + "normalized_dimension": "16", + "parity": null, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 4 + }, + { + "binary_rank_lower": 383, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 32, + "support_dimension": 0 + }, + { + "labels": 9920, + "support_dimension": 2 + }, + { + "labels": 63488, + "support_dimension": 4 + } + ], + "d": 32, + "ell": 1, + "independent_row_sha256": "cf179a75beb2ce20cbbf90732ab302cebeb2a804d1311d8f90e85386dc473951", + "minor_columns": 463, + "n": 73440, + "normalized_dimension": "32", + "parity": 0, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 5 + }, + { + "binary_rank_lower": 383, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 992, + "support_dimension": 1 + }, + { + "labels": 39680, + "support_dimension": 3 + }, + { + "labels": 32768, + "support_dimension": 5 + } + ], + "d": 32, + "ell": 1, + "independent_row_sha256": "0604f1e9909430c4fe40f44b9e9980a4b835610d29f8bf24d7a4a6bcc5a7fa9c", + "minor_columns": 463, + "n": 73440, + "normalized_dimension": "32", + "parity": 1, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 5 + }, + { + "binary_rank_lower": 765, + "complex_phases": false, + "counts_by_support_dimension": [ + { + "labels": 32, + "support_dimension": 0 + }, + { + "labels": 992, + "support_dimension": 1 + }, + { + "labels": 9920, + "support_dimension": 2 + }, + { + "labels": 39680, + "support_dimension": 3 + }, + { + "labels": 63488, + "support_dimension": 4 + }, + { + "labels": 32768, + "support_dimension": 5 + } + ], + "d": 32, + "ell": 1, + "independent_row_sha256": "16364f47c38056a7099cfa9c3d5a9b6034012f598efaf92bc947f39f071e177d", + "minor_columns": 845, + "n": 146880, + "normalized_dimension": "32", + "parity": null, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 5 + }, + { + "binary_rank_lower": 23, + "complex_phases": true, + "counts_by_support_dimension": [ + { + "labels": 8, + "support_dimension": 0 + }, + { + "labels": 112, + "support_dimension": 1 + }, + { + "labels": 448, + "support_dimension": 2 + }, + { + "labels": 512, + "support_dimension": 3 + } + ], + "d": 16, + "ell": 2, + "independent_row_sha256": "334094c6d1688f62bcb103b39d1a4ee5cc85b006500257e1d7fc3d2fdf342f8c", + "minor_columns": 87, + "n": 1080, + "normalized_dimension": "8", + "parity": null, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 3 + }, + { + "binary_rank_lower": 383, + "complex_phases": true, + "counts_by_support_dimension": [ + { + "labels": 16, + "support_dimension": 0 + }, + { + "labels": 480, + "support_dimension": 1 + }, + { + "labels": 4480, + "support_dimension": 2 + }, + { + "labels": 15360, + "support_dimension": 3 + }, + { + "labels": 16384, + "support_dimension": 4 + } + ], + "d": 32, + "ell": 2, + "independent_row_sha256": "99a853fe6e1459634bcbb9aac2586652966401769ef1caf3d9220413ce4bc611", + "minor_columns": 447, + "n": 36720, + "normalized_dimension": "16", + "parity": null, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 4 + }, + { + "binary_rank_lower": 12623, + "complex_phases": true, + "counts_by_support_dimension": [ + { + "labels": 32, + "support_dimension": 0 + }, + { + "labels": 1984, + "support_dimension": 1 + }, + { + "labels": 39680, + "support_dimension": 2 + }, + { + "labels": 317440, + "support_dimension": 3 + }, + { + "labels": 1015808, + "support_dimension": 4 + }, + { + "labels": 1048576, + "support_dimension": 5 + } + ], + "d": 64, + "ell": 2, + "independent_row_sha256": "2be6aa315e63e445f96ed62440637fe75f4f8f7b0077534b68d75eb3d8cf6bed", + "minor_columns": 12687, + "n": 2423520, + "normalized_dimension": "32", + "parity": null, + "positive_deficit_excluded": true, + "scope": "Only I plus the full orthogonality relation on this exact vector family; no rank upper bound asserted", + "t": 5 + } + ], + "rational_span_controls": [ + { + "exact_rank": 8, + "parity": 0, + "spanning_vectors": 8, + "t": 3 + }, + { + "exact_rank": 8, + "parity": 1, + "spanning_vectors": 8, + "t": 3 + }, + { + "exact_rank": 8, + "parity": null, + "spanning_vectors": 8, + "t": 3 + }, + { + "exact_rank": 16, + "parity": 0, + "spanning_vectors": 16, + "t": 4 + }, + { + "exact_rank": 16, + "parity": 1, + "spanning_vectors": 16, + "t": 4 + }, + { + "exact_rank": 16, + "parity": null, + "spanning_vectors": 16, + "t": 4 + }, + { + "exact_rank": 32, + "parity": 0, + "spanning_vectors": 32, + "t": 5 + }, + { + "exact_rank": 32, + "parity": 1, + "spanning_vectors": 32, + "t": 5 + }, + { + "exact_rank": 32, + "parity": null, + "spanning_vectors": 32, + "t": 5 + } + ], + "retained_kappa": "1/2147483648", + "scope": "Full orthogonality central matrices on exactly the declared real/Gaussian families; not arbitrary supported matrices or subfamilies.", + "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_witnesses.json": "3efcebf41650681a8a21a901cd2f81dc07a0c4d28064b883af16b10c3e0036c3" + }, + "status": "TWELVE SPECIFIED CENTRAL MATRICES REJECTED; NO NEW KAPPA", + "upstream_commit": "adc7f1241b42e322a6451854ab7e4b4c146bf78a" +} diff --git a/research/quadratic-affine-performance/evidence/benchmark.json b/research/quadratic-affine-performance/evidence/benchmark.json new file mode 100644 index 0000000000..7604a1919a --- /dev/null +++ b/research/quadratic-affine-performance/evidence/benchmark.json @@ -0,0 +1,154 @@ +{ + "status": "PASS_QUADRATIC_AFFINE_BATCHED_ROWS", + "rows_compared": 14662, + "rows_mismatched": 0, + "seconds_rows_reference": 66.986, + "seconds_rows_batched": 3.541, + "heavy_rank_witness_seconds": 10.7, + "certificate_seconds": 10.635, + "certificate_sha256": "d85881ccdcfd1cca04bb99226e5cbdca48d4cc005a35f5860f2e2771ec9b041b", + "certificate_equals_committed": true, + "negative_controls": { + "odd_lane_false_positive_demonstrated": true, + "dropped_gather_stage_detected": true + }, + "fixtures": [ + { + "fixture": 0, + "t": 3, + "complex_phases": false, + "parity": 0, + "columns": 83, + "rows": 3, + "rows_mismatched": 0, + "seconds_reference": 0.0, + "seconds_batched": 0.0 + }, + { + "fixture": 1, + "t": 3, + "complex_phases": false, + "parity": 1, + "columns": 83, + "rows": 3, + "rows_mismatched": 0, + "seconds_reference": 0.0, + "seconds_batched": 0.0 + }, + { + "fixture": 2, + "t": 3, + "complex_phases": false, + "parity": null, + "columns": 85, + "rows": 5, + "rows_mismatched": 0, + "seconds_reference": 0.0, + "seconds_batched": 0.0 + }, + { + "fixture": 3, + "t": 4, + "complex_phases": false, + "parity": 0, + "columns": 103, + "rows": 23, + "rows_mismatched": 0, + "seconds_reference": 0.001, + "seconds_batched": 0.0 + }, + { + "fixture": 4, + "t": 4, + "complex_phases": false, + "parity": 1, + "columns": 103, + "rows": 23, + "rows_mismatched": 0, + "seconds_reference": 0.001, + "seconds_batched": 0.0 + }, + { + "fixture": 5, + "t": 4, + "complex_phases": false, + "parity": null, + "columns": 125, + "rows": 45, + "rows_mismatched": 0, + "seconds_reference": 0.001, + "seconds_batched": 0.0 + }, + { + "fixture": 6, + "t": 5, + "complex_phases": false, + "parity": 0, + "columns": 463, + "rows": 383, + "rows_mismatched": 0, + "seconds_reference": 0.053, + "seconds_batched": 0.006 + }, + { + "fixture": 7, + "t": 5, + "complex_phases": false, + "parity": 1, + "columns": 463, + "rows": 383, + "rows_mismatched": 0, + "seconds_reference": 0.053, + "seconds_batched": 0.006 + }, + { + "fixture": 8, + "t": 5, + "complex_phases": false, + "parity": null, + "columns": 845, + "rows": 765, + "rows_mismatched": 0, + "seconds_reference": 0.196, + "seconds_batched": 0.017 + }, + { + "fixture": 9, + "t": 3, + "complex_phases": true, + "parity": null, + "columns": 87, + "rows": 23, + "rows_mismatched": 0, + "seconds_reference": 0.0, + "seconds_batched": 0.0 + }, + { + "fixture": 10, + "t": 4, + "complex_phases": true, + "parity": null, + "columns": 447, + "rows": 383, + "rows_mismatched": 0, + "seconds_reference": 0.049, + "seconds_batched": 0.005 + }, + { + "fixture": 11, + "t": 5, + "complex_phases": true, + "parity": null, + "columns": 12687, + "rows": 12623, + "rows_mismatched": 0, + "seconds_reference": 66.631, + "seconds_batched": 3.505 + } + ], + "environment": { + "python": "3.13.15", + "platform": "Windows-11-10.0.26200-SP0" + }, + "scope": "Row-engine differential only; the GF(2) elimination is unchanged code." +} diff --git a/research/quadratic-affine-performance/reference.py b/research/quadratic-affine-performance/reference.py new file mode 100644 index 0000000000..d7446fd271 --- /dev/null +++ b/research/quadratic-affine-performance/reference.py @@ -0,0 +1,54 @@ +"""Verbatim pre-change reference rows and rank witness for differential tests. + +Copied from scripts/experiments/quadratic_affine.py at base commit +2921874911956718fcaaaf9396fe8267b3cfa9f0 (the `inner` function and the +`sum(1<> (8 * k + 7)) & 1) + + +class Primitives(unittest.TestCase): + def test_gather_matches_brute_force(self): + rng = random.Random(1234) + for lanes in (1, 2, 3, 7, 8, 9, 63, 64, 65, 200, 300): + for pattern in ('random', 'all', 'single'): + flags = 0 + for k in range(lanes): + if pattern == 'all' or (pattern == 'single' and k == lanes - 1) or rng.random() < 0.5: + flags |= 1 << (8 * k + 7) + self.assertEqual(_gather_lanes(flags, lanes), brute_gather(flags, lanes), + (lanes, pattern)) + + def test_lane_flags_match_brute_force_with_borrow_chains(self): + rng = random.Random(99) + for trial in range(400): + lanes = rng.randint(1, 150) + vals = [2 * rng.randint(0, 32) for _ in range(lanes)] + if trial % 2 == 0: # long zero runs force borrow chains through many lanes + vals = [0 if rng.random() < 0.85 else 2 * rng.randint(1, 32) for _ in range(lanes)] + x = 0 + for k, v in enumerate(vals): + x |= v << (8 * k) + want = sum(1 << (8 * k + 7) for k in range(lanes) if vals[k] == 0) + self.assertEqual(_lane_flags(x, lanes), want, vals[:20]) + + def test_odd_lanes_break_the_swar_test(self): + """Negative control: without pre-doubled (even) lanes the SWAR zero + test false-flags a value-1 lane behind a zero run; that is why the + masks hold doubled counts.""" + lanes = 4 + vals = [0, 0, 1, 0] # lane 2 = 1 sits behind two zero lanes + x = 0 + for k, v in enumerate(vals): + x |= v << (8 * k) + naive = sum(1 << (8 * k + 7) for k in range(lanes) if (x - int.from_bytes(b'\x01' * lanes, 'little') + & ~x & int.from_bytes(b'\x80' * lanes, 'little')) >> (8 * k + 7) & 1) + self.assertNotEqual(naive, sum(1 << (8 * k + 7) for k in range(lanes) if vals[k] == 0), + 'odd-lane adversary should mis-flag; control would be vacuous') + + +class RowsAgainstReference(unittest.TestCase): + def test_every_row_of_small_and_medium_fixtures(self): + for index in range(11): + w = FIXTURES[index] + f = family(w['t'], w['complex_phases'], w['parity']) + vectors = [vector(f, i) for i in w['sample']] + rows = _orthogonality_rows(vectors, f['D'], w['independent_rows']) + self.assertEqual(rows, reference_rows(vectors, w['independent_rows']), + 'fixture %d rows differ from the reference engine' % index) + + def test_heavy_fixture_rows_subsampled(self): + w = FIXTURES[11] + f = family(w['t'], w['complex_phases'], w['parity']) + vectors = [vector(f, i) for i in w['sample']] + chosen = w['independent_rows'][::211] + rows = _orthogonality_rows(vectors, f['D'], chosen) + self.assertEqual(rows, reference_rows(vectors, chosen)) + + def test_random_samples_small_families(self): + rng = random.Random(7) + for t, complex_phases, parity in ((2, True, None), (3, False, 0), (3, False, 1), + (3, True, None), (4, False, None)): + f = family(t, complex_phases, parity) + for _ in range(4): + sample = rng.sample(range(f['n']), min(f['n'], 40)) + chosen = rng.sample(range(len(sample)), min(len(sample), 12)) + vectors = [vector(f, i) for i in sample] + self.assertEqual(_orthogonality_rows(vectors, f['D'], chosen), + reference_rows(vectors, chosen)) + + def test_rank_witness_matches_reference(self): + for index in range(11): + w = FIXTURES[index] + self.assertEqual(rank_witness(**w), rank_witness_reference(**w), 'fixture %d' % index) + + def test_row_corruption_changes_digest(self): + """Negative control: a one-bit row change must change the recorded + digest, so the byte-identical digests in the certificate are evidence.""" + w = dict(t=3, complex_phases=False, parity=None, sample=FIXTURES[2]['sample'], + independent_rows=FIXTURES[2]['independent_rows']) + good = rank_witness(**w) + f = family(w['t'], w['complex_phases'], w['parity']) + vectors = [vector(f, i) for i in w['sample']] + rows = _orthogonality_rows(vectors, f['D'], w['independent_rows']) + rows[w['independent_rows'][0]] ^= 1 # flip one column bit + from hashlib import sha256 + bytewidth = (len(w['sample']) + 7) // 8 + digest = sha256() + for i in w['independent_rows']: + digest.update(rows[i].to_bytes(bytewidth, 'little')) + self.assertNotEqual(digest.hexdigest(), good['independent_row_sha256']) + + def test_broken_gather_is_detected(self): + """Negative control: dropping a gather stage must be caught by the + same row comparison the benchmark uses.""" + 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 = {} + for i in w['independent_rows']: + s, lo, hi = vectors[i] + broken[i] = (good[i] ^ (1 << i)) & ~1 # emulate a dropped final gather stage + self.assertNotEqual(broken, reference_rows(vectors, w['independent_rows'])) + + +class RejectionsPreserved(unittest.TestCase): + def test_reference_and_shipped_reject_identically(self): + for call in (dict(t=1, complex_phases=False, parity=None, sample=[0, 0], independent_rows=[0]), + dict(t=1, complex_phases=False, parity=None, sample=[0, 1], independent_rows=[0, 0]), + dict(t=1, complex_phases=False, parity=None, sample=[0, 1], independent_rows=[2]), + dict(t=1, complex_phases=False, parity=None, sample=[0, 4], independent_rows=[0])): + with self.assertRaises(ValueError): + rank_witness(**call) + with self.assertRaises(ValueError): + rank_witness_reference(**call) + + def test_dependent_rows_still_fail(self): + """The claimed-independence rejection fires on a crafted dependent + row set, proving failure detection is intact through the new path.""" + import experiments.quadratic_affine as qa + original = qa._orthogonality_rows + try: + qa._orthogonality_rows = lambda vectors, D, indices: {0: 0b001, 1: 0b010, 2: 0b011} + with self.assertRaises(ValueError): + qa.rank_witness(1, False, None, [0, 1, 2, 3], [0, 1, 2]) + finally: + qa._orthogonality_rows = original + + +if __name__ == '__main__': + unittest.main() diff --git a/scripts/experiments/quadratic_affine.py b/scripts/experiments/quadratic_affine.py index 271e0a4e0b..8e9f9f6416 100644 --- a/scripts/experiments/quadratic_affine.py +++ b/scripts/experiments/quadratic_affine.py @@ -112,15 +112,104 @@ def block_projector(v,D): return P +def _character_masks(vectors,D): + """Lane-packed column masks: lane j of masks[k][p] holds 2 iff column j + holds i^k at position p. Lanes sit at bit 8j to match _lane_flags, and + pre-doubling keeps every lane even so the SWAR zero test stays exact.""" + n=len(vectors) + lists=[[[] for _ in range(D)] for _ in range(4)] + for j,(s,lo,hi) in enumerate(vectors): + x=s + while x: + p=x.bit_length()-1;x^=1<

>p)&1)+2*((hi>>p)&1)][p].append(j) + masks=[[0]*D for _ in range(4)] + for k in range(4): + for p in range(D): + js=lists[k][p] + if js: + buf=bytearray(n) + for j in js:buf[j]=2 + masks[k][p]=int.from_bytes(buf,'little') + return masks + + +def _lane_flags(x,lanes): + """Exact zero-lane mask for 8-bit lanes holding even values in [0,126]. + + Even lanes never underflow on borrow-in, so borrows propagate only + through zero lanes and the classic SWAR zero test is exact per lane. + Lanes live at bit 8k, so the byte width is the lane count. Returns + bit 8k+7 set iff lane k is zero.""" + ones=int.from_bytes(b'\x01'*lanes,'little') + return (x-ones)&~x&int.from_bytes(b'\x80'*lanes,'little') + + +_GATHER_CACHE={} + + +def _gather_lanes(flags,lanes): + """Compress stride-8 lane flags at bit 8k+7 into bit k of a dense mask. + + Each 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 (equal to bit i of their index), and + distinct indices never collide: within one 2**i block positions differ + by the index difference, across blocks the 8*(k-k') term dominates.""" + x=flags>>7 + masks=_GATHER_CACHE.get(lanes) + if masks is None: + masks=[] + i=0 + while (1<>(7<>p)&1)+2*((hi>>p)&1) + a,b,c,d=(masks[ev][p],masks[(ev+2)&3][p],masks[(ev+3)&3][p],masks[(ev+1)&3][p]) + if a:pos_r+=a + if b:neg_r+=b + if c:pos_i+=c + if d:neg_i+=d + rows[i]=_gather_lanes(_lane_flags(pos_r^neg_r,n)&_lane_flags(pos_i^neg_i,n),n)|(1<