Tooling: 1.69× faster production R439 omission atlas via packed lanes with identical certificates

research/omission-lanes-production/NOTICE.md

@@ -0,0 +1,14 @@
+# Notice
+
+This package wires Sagar Thakrar’s (@thakrarsagar) proved opt-in packed
+literal omission lanes from `research/omission-lanes-seed92/` (incorporated
+CrocSwap [#1433](https://github.com/CrocSwap/integer-mult-bounds/pull/1433))
+into the production R439 omission atlas
+`research/r439-omission-atlas-seed81/verify.py`.
+
+Credit **woklerx** for the retained PR1017 / seed81 complete single-ADD
+omission atlas, and **Sagar Thakrar** for the exact integer-lane packing.
+Predecessor notices in the atlas and opt-in package remain intact.
+
+Prepared by Wentao Li (VictorLiwentao, https://x.com/Is__Victor) with substantial
+AI assistance. Apache-2.0.

research/omission-lanes-production/README.md

@@ -0,0 +1,82 @@
+# Production packed lanes for the R439 omission atlas
+
+**Tooling improvement; no new kappa.** At base
+`0b1cccf86e2f5132ed286a26ef0a681a495740ea`,
+`research/r439-omission-atlas-seed81/verify.py` still replayed every single-ADD
+omission with a fresh 661-bit row map. Sagar Thakrar’s opt-in adapter
+`research/omission-lanes-seed92/` (incorporated
+[#1433](https://github.com/CrocSwap/integer-mult-bounds/pull/1433)) already
+proved sixteen independent omissions in integer bit lanes with identical
+complete certificates. This package wires that equivalent rewrite into the
+**production** PR1017 atlas used by R439 omission tooling.
+
+The historical per-omission `replay(gates,k)` helper is retained for baseline
+and witness checks. Dependent packages that live-pinned the pairwise-era atlas
+digest are demoted or refreshed: opt-in `omission-lanes-seed92` vendors
+pairwise `baseline.py`; `r439-three-omission-distance` demotes its atlas
+`verify.py` pin to provenance (it has its own independent replay).
+
+## Reproduce
+
+Python **3.12**, standard library only, from the repository root:
+
+```sh
+python3.12 -I -B research/omission-lanes-production/verify.py
+python3.12 -I -O -B research/omission-lanes-production/verify.py
+python3.12 -B scripts/research_package.py --package research/omission-lanes-production
+taskset -c 0 python3.12 -I -B research/omission-lanes-production/benchmark.py --rounds 5 --write-result
+```
+
+Expected:
+
+```text
+PASS_OMISSION_LANES_PRODUCTION honest=1 matrices=5563 short_checks=… corruption=1 certs=1 no_new_kappa
+PASS_REGISTERED_RESEARCH_PACKAGE research/omission-lanes-production outcome=completed
+PASS_IDENTICAL_OMISSION_LANES_PRODUCTION_RECEIPTS
+```
+
+Default verify is read-only. Temp-copy packed-mutant bit-flip foil rejects via
+audit failure. Package gates under `-O` still load checkers with
+`compile(..., optimize=0)`. Full `make verify`, selected cold replay, Lean, and
+multiplication-theorem obligations were not rerun for this isolated
+historical-checker change.
+
+## Result
+
+On Linux / CPython 3.12.3 with `taskset -c 0`, five alternating fresh-process
+pairs over the complete 5,563-mutant atlas gave the median wall time recorded
+in [`RESULT.json`](RESULT.json). Timing is host-descriptive and is not a
+correctness gate. Every honest receipt matches
+`research/r439-omission-atlas-seed81/CERTIFICATE.json`.
+
+## Why the packed lanes are equivalent
+
+Pack a batch of `B` omissions as width-`N` lanes inside one Python integer.
+Lane `j` occupies bits `[jN, (j+1)N)`. An ADD is an XOR of source into
+destination; XOR cannot carry across lanes. Suppressing lane `j` at omitted
+gate `k` is exactly the historical `if k != omit` guard for that lane. See
+`research/omission-lanes-seed92/`.
+
+## Open next questions
+
+- Should other historical copies of the same literal omission loop adopt packed
+  lanes with coordinated digest refresh?
+- Should `research/omission-lanes-seed92` be marked superseded as an opt-in
+  monkey-patch now that production ships packed lanes?
+
+## Overlap and credit
+
+Closest priors (different delivery):
+
+- `research/omission-lanes-seed92/` / [#1433](https://github.com/CrocSwap/integer-mult-bounds/pull/1433)
+  — opt-in packed lanes; this is the production wiring.
+- [CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756)
+  — identical-receipt tooling quality bar.
+- Leave-alone tooling through [#2412](https://github.com/CrocSwap/integer-mult-bounds/pull/2412)
+  and pending `cursor/scalar-fused-dyadic-production-60b9` / deferred
+  `cursor/ck-dyadic-replay-production-60b9` were not reopened.
+
+Credit woklerx and Sagar Thakrar. Prepared by Wentao Li
+([VictorLiwentao](https://github.com/VictorLiwentao),
+[Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance.
+Apache-2.0.

research/omission-lanes-production/RESULT.json

@@ -0,0 +1,29 @@
+{
+  "schema_version": 1,
+  "package": "research/omission-lanes-production",
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "workload": "complete R439 omission atlas (5563 literal single-ADD mutants)",
+  "rounds": 5,
+  "baseline_seconds": [
+    3.7081245949998447,
+    3.605200038999783,
+    3.5811381710000205,
+    3.6684772500000236,
+    3.6298425279999265
+  ],
+  "production_seconds": [
+    2.090888160999839,
+    2.143346830000155,
+    2.1176058920000287,
+    2.166503299999931,
+    2.1509510230000615
+  ],
+  "median_baseline_seconds": 3.6298425279999265,
+  "median_production_seconds": 2.143346830000155,
+  "median_speedup": 1.6935395042899632,
+  "baseline_sha256": "127d7679fb26e264018548a1301b2f0f437d834eb1f0ffa215556243077ff866",
+  "production_sha256": "6c3c94b01e3db5fb6d9e45eda4f60628252de1fab218e6e8233cc7949afd8966",
+  "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]",
+  "platform": "Linux 6.12.94+",
+  "note": "Host-descriptive; not a correctness gate. Receipts identical each round."
+}

research/omission-lanes-production/SOURCES.json

@@ -0,0 +1,56 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1"
+    },
+    {
+      "path": "research/r439-omission-atlas-seed81/verify.py",
+      "usage": "provenance",
+      "git_blob": "759d18d73dbab5d7620ce61395110aa57c06f901",
+      "sha256": "127d7679fb26e264018548a1301b2f0f437d834eb1f0ffa215556243077ff866",
+      "note": "Literal-era digest retained as provenance; working production file ships packed lanes (see OPTIMIZED digest in verify.py). Live equivalence uses package baseline.py plus working production path."
+    },
+    {
+      "path": "research/r439-omission-atlas-seed81/CERTIFICATE.json",
+      "usage": "input",
+      "sha256": "05c44b5d818862563a6674131024b1460d1e7bcb7828e4ebee4ec0198129e4e7",
+      "git_blob": "32cbc2379deea1ddf79feb05cb422da643e730b7"
+    },
+    {
+      "path": "research/r439-omission-atlas-seed81/SOURCES.json",
+      "usage": "input",
+      "sha256": "6056be2b6fb0bc511bf215d658d440c7bf5cc9bd856eeff62c2361edb513989c",
+      "git_blob": "55517ccdcbca283bd7383b0fc651e3e7449b5991"
+    },
+    {
+      "path": "research/r439-helper-stars-seed19/candidate.json.gz",
+      "usage": "input",
+      "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8",
+      "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+      "usage": "input",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a"
+    },
+    {
+      "path": "research/omission-lanes-seed92/replay.py",
+      "usage": "provenance",
+      "sha256": "041b36011d32d034843e279544336f696d39eaadab303cc386930db25d694024",
+      "git_blob": "851d9b715eb6b56a27a312ae0bb4129c3c9c4376",
+      "note": "Opt-in packed kernel at base_commit; working tree may carry production-wiring hygiene edits."
+    }
+  ]
+}

research/omission-lanes-production/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 4,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "chooser_seed": "omission-lanes-production-60b9",
+  "budget_minutes": 60,
+  "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": "Can the production R439 omission atlas research/r439-omission-atlas-seed81/verify.py adopt the proved exact packed integer-lane omission replays from research/omission-lanes-seed92/ (#1433) so that the shipped atlas is faster while every certificate field stays identical?",
+  "scope_change_reason": "The catalogue card asks for one measured replay bottleneck with before/after wall time and retained checks. Expertise override selected verifier-engineering after surveying leave-alone production rewrites through #2412, pending scalar-fused-dyadic production, and the deferred thin ck-dyadic production tip. Remaining proved opt-in adapter #1433 still left production atlas on per-omission literal replay; Linux host probe measured ~1.77× for the opt-in packing.",
+  "bottleneck_link": "Faster trustworthy PR1017 omission-atlas audits increase review throughput for R439 tooling without changing kappa or check coverage.",
+  "stop_rule": "Stop after wiring one production object with identical-receipt evidence, pin-drift demotions, and a descriptive before/after wall-time sample clearly above ~1.5×; do not invent kappa or reopen leave-alone objects.",
+  "evidence": "PASS_OMISSION_LANES_PRODUCTION via research/omission-lanes-production/verify.py (also under -O); PASS_REGISTERED_RESEARCH_PACKAGE; PASS_IDENTICAL_OMISSION_LANES_PRODUCTION_RECEIPTS via pinned-CPU benchmark.py --rounds 5; vendor baseline.py; demote live atlas pins in omission-lanes-seed92 and r439-three-omission-distance.",
+  "author": "Wentao Li",
+  "email": "wentaol4@illinois.edu",
+  "github": "VictorLiwentao",
+  "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, packaging, benchmarking and writing. Not independent human peer review.",
+  "outcome": "completed",
+  "open_questions": [
+    {
+      "question": "Should other historical copies of the same literal omission loop adopt packed lanes with coordinated digest refresh?",
+      "why_it_matters": "Sibling research packages may still pay per-omission replay cost.",
+      "first_step": "Enumerate packages that call replay(gates,k) over the same 5563-gate domain.",
+      "blocked_by": "Maintainer inventory-refresh preference / one-object stop rule."
+    },
+    {
+      "question": "Should research/omission-lanes-seed92 be marked superseded as an opt-in monkey-patch now that production ships packed lanes?",
+      "why_it_matters": "Maintainers may want one recommended path for the PR1017 atlas.",
+      "first_step": "Add a one-line pointer in that package README after this change merges.",
+      "blocked_by": "Documentation-only follow-up."
+    }
+  ]
+}

research/omission-lanes-production/VERIFY.json

@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/omission-lanes-production/baseline.py",
+    "research/r439-omission-atlas-seed81/verify.py",
+    "research/r439-omission-atlas-seed81/CERTIFICATE.json",
+    "research/r439-omission-atlas-seed81/SOURCES.json",
+    "research/r439-helper-stars-seed19/candidate.json.gz",
+    "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+    "research/omission-lanes-seed92/replay.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Exact baseline copy of the base-commit atlas; production equals the packed-lane transform; identical honest certificate and 5563 matrices; short-word/batch controls; temp-copy packed-mutant bit-flip corruption control; duplicate JSON-key check; read-only default verify."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Same equivalence and pin discipline under -O. Loaders use compile(..., optimize=0) so atlas need() admission stays enforced."
+    }
+  ]
+}