Reduce exact-query construction cost without changing answers or engine policy

.github/workflows/faster-query-review.yml

@@ -0,0 +1,133 @@
+name: Faster query review
+on:
+  push:
+    branches: [research/faster-queries-review-20261015]
+    paths:
+      - experiments/compiled_query/exact.py
+      - experiments/compiled_query/exact_native.cpp
+      - experiments/compiled_query/test_*.py
+      - experiments/compiled_query/query_latency.py
+      - experiments/compiled_query/LINEAR_CONSTRUCTION.md
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: faster-query-review-${{ github.ref }}
+  cancel-in-progress: false
+jobs:
+  compare:
+    runs-on: ${{ matrix.runner }}
+    timeout-minutes: 20
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - {runner: ubuntu-24.04, python: '3.11'}
+          - {runner: ubuntu-24.04, python: '3.13'}
+          - {runner: ubuntu-24.04-arm, python: '3.13'}
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python }}
+      - run: python -m pip install 'pytest==8.4.2' 'python-sat==1.9.dev15'
+      - name: Check native adjacency, proofs, input handling and evidence
+        run: |
+          set -euo pipefail
+          mkdir -p review-evidence
+          git rev-parse HEAD > review-evidence/commit.txt
+          python -m pytest experiments/compiled_query/test_exact.py experiments/compiled_query/test_transfer_hardening.py experiments/compiled_query/test_query_latency.py experiments/compiled_query/test_linear_construction.py -q --junitxml=review-evidence/tests.xml 2>&1 | tee review-evidence/tests.log
+      - name: Compare the unchanged seven-arm schedule against the user checkpoint
+        run: |
+          set -euo pipefail
+          python -m experiments.compiled_query.query_latency run --out review-evidence/comparison --baseline-commit 098a8477f6cc8bb696423e78c4d6b6a26a95a0e1 --include-baseline-auto 2>&1 | tee review-evidence/run.log
+          python -m experiments.compiled_query.query_latency audit --out review-evidence/comparison 2>&1 | tee review-evidence/audit.log
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: linear-review-${{ matrix.runner }}-py${{ matrix.python }}-${{ github.run_id }}
+          path: review-evidence/
+          retention-days: 30
+          if-no-files-found: warn
+  sanitizers:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    strategy:
+      fail-fast: false
+      matrix:
+        sanitizer: ['undefined', 'address,undefined']
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.13'
+      - run: python -m pip install 'pytest==8.4.2' 'python-sat==1.9.dev15'
+      - name: Run all exact-service contracts under the selected sanitizer
+        env:
+          SANITIZER: ${{ matrix.sanitizer }}
+        run: |
+          set -euo pipefail
+          mkdir -p review-evidence
+          git rev-parse HEAD > review-evidence/commit.txt
+          export SPECTRA_EXACT_LIBRARY="$(python -c "from experiments.compiled_query.exact import build_exact_runtime; import os; print(build_exact_runtime('review-evidence/build', sanitizer=os.environ['SANITIZER']))")"
+          export UBSAN_OPTIONS=halt_on_error=1
+          if [ "$SANITIZER" = 'address,undefined' ]; then
+            export LD_PRELOAD="$(g++ -print-file-name=libasan.so):$(g++ -print-file-name=libstdc++.so)"
+            export ASAN_OPTIONS=detect_leaks=0:abort_on_error=1
+          fi
+          python -m pytest experiments/compiled_query/test_exact.py -q --junitxml=review-evidence/tests.xml 2>&1 | tee review-evidence/tests.log
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: linear-review-sanitizer-${{ matrix.sanitizer }}-${{ github.run_id }}
+          path: review-evidence/
+          retention-days: 30
+          if-no-files-found: warn
+  windows:
+    runs-on: windows-2022
+    timeout-minutes: 15
+    env:
+      PYTHONUTF8: '1'
+    steps:
+      - run: git config --global core.autocrlf false
+      - uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.13'
+      - name: Load the installed MSVC x64 environment
+        shell: pwsh
+        run: |
+          $vswhere = "${env:ProgramFiles(x86)}\Microsoft Visual Studio\Installer\vswhere.exe"
+          $vs = & $vswhere -latest -products '*' -requires Microsoft.VisualStudio.Component.VC.Tools.x86.x64 -property installationPath
+          if (-not $vs) { throw 'MSVC x64 build tools not found' }
+          $vcvars = Join-Path $vs 'VC\Auxiliary\Build\vcvars64.bat'
+          $lines = & cmd /c "`"$vcvars`" >nul && set"
+          if ($LASTEXITCODE -ne 0) { throw 'MSVC environment setup failed' }
+          foreach ($line in $lines) {
+            $pair = $line -split '=', 2
+            if ($pair.Count -eq 2 -and $pair[0] -in @('PATH','INCLUDE','LIB','LIBPATH','VCToolsInstallDir','VCINSTALLDIR','WindowsSdkDir','WindowsSDKVersion')) {
+              $line | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
+            }
+          }
+      - run: python -m pip install 'pytest==8.4.2' 'python-sat==1.9.dev15'
+      - name: Check actual MSVC builds and the sorted native reference
+        shell: pwsh
+        run: |
+          New-Item -ItemType Directory -Force review-evidence | Out-Null
+          git rev-parse HEAD | Out-File review-evidence/commit.txt
+          python -m pytest experiments/compiled_query/test_exact.py experiments/compiled_query/test_transfer_hardening.py experiments/compiled_query/test_proof_replay.py experiments/compiled_query/test_linear_construction.py -q --junitxml=review-evidence/tests.xml
+          if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE }
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: linear-review-windows-py3.13-${{ github.run_id }}
+          path: review-evidence/
+          retention-days: 30
+          if-no-files-found: warn

experiments/compiled_query/LINEAR_CONSTRUCTION.md

@@ -0,0 +1,74 @@
+# Linear implication construction from canonical original edges
+
+Continuation base: `098a8477f6cc8bb696423e78c4d6b6a26a95a0e1` (`faster-queries`).
+The user's automatic policy, prepared-root proof reconstruction, direct witness
+serialization, proof scratch reuse and Windows support are preserved.
+
+## Invariant and proof
+
+Both admitted input paths supply a simple undirected graph as strictly increasing
+lexicographic pairs `(u,v)` with `u < v`. The tuple path normalizes and deduplicates
+before construction. Both independent SBC1 parsers reject noncanonical edges.
+Each vertex has one or two distinct original colours.
+
+For any fixed vertex `v`, its incident subsequence of the original edge stream
+visits neighbours less than `v` in increasing order, followed by neighbours
+greater than `v` in increasing order. Each colour shared by an edge's endpoints
+produces two implications: choosing that colour at either endpoint forbids it
+at the other. For a fixed source literal and a fixed neighbour, there is at most
+one outgoing implication; the analogous statement holds for incoming implications.
+Thus the edge-generated targets in every forward CSR row and sources in every
+reverse CSR row are already strictly increasing by literal number.
+
+A singleton has a synthetic unused high literal and a unit arc from that literal
+to its real low literal. No conflict implication leaves its synthetic high literal
+or enters its real low literal. Consequently that unit arc is the only entry of
+its forward source row and reverse target row; prepending the unit arcs does not
+break either ordering. There are no self edges and no duplicate implications.
+
+Stable counting-and-scattering CSR construction on the unsorted global stream
+therefore yields arrays *identical* to construction after lexicographic arc sort
+and deduplication, for both forward and reverse graphs. This preserves SCC IDs,
+base assignments, path traversal order, routing trees and serialized certificates.
+The downstream condensation/bridge sorts remain: this is not a claim that the
+entire routed constructor is linear-time.
+
+The independent observer separately derives one forbidden literal pair for every
+original edge/shared colour. Those pairs are unique; its verifier scans all pairs
+rather than binary-searching them. Dropping that list's sort does not drop any
+constraint. Its independently owned original edge list remains sorted for proof
+hop membership tests. No solver state is passed to the observer.
+
+For `n` vertices, `m` canonical edges and `a <= 4m+n` implications, implication
+emission and both CSR builds now take `O(n+a)` time and `O(n+a)` storage. The removed
+comparison sort was `O(a log a)`; no claim is made about an empirical speedup until
+complete-call measurements finish. This is an implementation specialization of
+established 2-SAT machinery, not a new 2-SAT algorithm or priority claim. See
+Aspvall, Plass and Tarjan (1979), DOI 10.1016/0020-0190(79)90002-4.
+
+## Validation, fixed before the new comparison
+
+A diagnostic-only `SPECTRA_EXACT_VALIDATE_LINEAR_CSR` build reconstructs the old
+sorted arrays and compares *all four native arrays and the arc count* on every
+construction. It must never be used for timing. The focused tests include all
+three-vertex graphs/domain combinations, singleton and bit-63 domains, randomized
+larger graphs, noncanonical tuple inputs, and malformed binary packet rejection.
+Existing exhaustive, MiniCard, proof-mutation, memory, and concurrency contracts
+remain in force. Compare complete SBC1/SCQ2 outputs against the immediate parent
+for all five explicit/automatic modes. No format, ABI, resource cap, default,
+engine-selection threshold, or admission rule changes.
+
+Reuse the user's seven-arm harness with baseline commit `098a847...` in full,
+48 exposed structural graphs, bank lengths 1/63/64/65/1024, nine paired repetitions,
+two warmups, identical host/compiler flags, and original-input replay. Keep the
+existing 10% auto-versus-candidate-raw target unchanged and report its outcome even
+if common raw improvements make that relative target harder. Also report each
+candidate against its immediate-parent counterpart, including previous auto.
+All cases, errors, regressions and nonpassing runs are retained. These are exposed
+development measurements, not a fresh confirmation or outside replication.
+
+```bash
+python -m experiments.compiled_query.query_latency run --out linear-comparison \
+  --baseline-commit 098a8477f6cc8bb696423e78c4d6b6a26a95a0e1 --include-baseline-auto
+python -m experiments.compiled_query.query_latency audit --out linear-comparison
+```

experiments/compiled_query/LINEAR_REVIEW_20261015.md

@@ -0,0 +1,164 @@
+# SPECTRA: continuation from the user's faster-queries branch
+
+**15 October 2026. Exposed synthetic development, not new confirmation.**
+
+## Preserved starting point
+
+User checkpoint: `098a8477f6cc8bb696423e78c4d6b6a26a95a0e1` on `faster-queries`.
+This continuation preserves the user's automatic engine selection, prepared-root
+proof reconstruction, direct witness serialization, reusable proof-checking
+scratch, Windows/MSVC support and seven-arm comparison. The user's branch and
+main are unchanged; earlier PRs are not merged or replaced.
+
+The user's latest run, `38691730508`, already passes the 10% development target
+on x86 Python 3.11, x86 Python 3.13 and ARM64 Python 3.13. Its long-bank auto/raw
+ratios are 0.885672, 0.896982 and 0.889297 respectively. The older failed target
+remains historical evidence. Those improvements belong to the user's checkpoint,
+not to the new optimization reported below.
+
+## New code
+
+Published implementation: `8d28a63707a1e3d56d5d16688924cd3985ee80d7`.
+Implementation tree: `0753490153b4e68036e30be738f305eed96e57f8`.
+Native SHA-256: `67a8b5c8c55dd4fdc5070f2308cabf37a463a7a1294f12a8dd496d792852fb25`.
+Branch: `research/faster-queries-review-20261015`.
+
+Three core files change: `exact_native.cpp`, `test_linear_construction.py` and
+`LINEAR_CONSTRUCTION.md`. Two redundant global sorts are removed: implication
+arc sorting/deduplication and observer forbidden-pair sorting/deduplication.
+The input paths already supply sorted, unique, canonical original edges.
+
+Stable forward and reverse CSR construction consequently produces exactly the
+same adjacency arrays as the old sorted implementation, including singleton unit
+arcs. The proof is in `LINEAR_CONSTRUCTION.md`. Diagnostic-only native builds
+construct both versions and compare all four arrays and the arc count before
+SCC processing. The diagnostic macro is never enabled in benchmark builds.
+
+Every original constraint remains in the independently owned observer. Raw mode
+receives the same applicable improvement. No ABI, packet schema, memory cap,
+automatic-selection threshold, default or public-package behavior changes.
+
+Implication emission and both CSR builds take O(n+a) after canonical admission,
+where a is the implication count. Downstream condensation/routing sorts and tuple
+normalization still have their own costs. This is not a linear-time claim for the
+whole routed constructor, a new 2-SAT algorithm, or an algorithmic-priority claim.
+
+## Matched complete-call results
+
+Baseline: the immediate user checkpoint **098a847**, not an older slower version.
+The unchanged seven-arm schedule retains 48 exposed graph realizations, eight
+families, five bank sizes, nine paired repetitions, two warmups, fixed order
+permutations, process limits and original-input replay. Parent raw/route/auto and
+current raw/SCC/route/auto are all retained, with matching compiler/options.
+
+The timed boundary starts at ready immutable SBC1 input and includes input
+hashing, native construction, solving, full witnesses/proofs, independent
+serialized-output checking, SCQ2 production, native disposal and output hashing.
+Packet preparation, compilation, process startup, evidence writes and post-run
+Python replay are outside it. It is not a production end-to-end latency claim.
+
+Ratios are **new automatic-engine time / parent automatic-engine time**; lower is
+better. Aggregation uses graph medians and geometric means, not pooled queries.
+
+| Queries/call | Local x86 Py3.13 | CI x86 Py3.11 | CI x86 Py3.13 | CI ARM64 Py3.13 |
+|---|---:|---:|---:|---:|
+| 1 | 0.547348 | 0.552124 | 0.621886 | 0.663518 |
+| 63 | 0.692583 | 0.688031 | 0.730851 | 0.763819 |
+| 64 | 0.665698 | 0.682101 | 0.717376 | 0.754774 |
+| 65 | 0.681992 | 0.674030 | 0.723055 | 0.756958 |
+| 1,024 | 0.922051 | 0.931766 | 0.960653 | 0.945146 |
+
+CI therefore shows **33.6-44.8% less single-request time** and **3.9-6.8% less
+1,024-request time** against the user's latest auto engine. Construction cost,
+not a new propagation rule, accounts for the change being tested.
+
+| CI environment | New/parent auto, 1,024 | Graph-bootstrap 95% interval | New auto/new raw, 1,024 | Development target |
+|---|---:|---:|---:|---|
+| x86 Py3.11 | 0.931766 | [0.913470, 0.948929] | 0.878810 | PASS |
+| x86 Py3.13 | 0.960653 | [0.945421, 0.974489] | 0.897270 | PASS |
+| ARM64 Py3.13 | 0.945146 | [0.930190, 0.958338] | 0.882249 | PASS |
+
+The unchanged target requires long-bank auto/raw <= 0.90, its upper 95% bound < 1,
+every family <= 1.10, and single-request aggregate <= 1.10. Local also passes.
+Intervals use the existing 4,000 family-stratified graph resamples and describe
+this fixed exposed synthetic panel, not real-world application populations.
+
+Each environment completes **15,120 timed calls and 48 workers**. Each audit
+checks **1,636 distinct packet/output pairs containing 484,546 decisions**.
+Only post-run replay deduplicates repeated outputs; native checking still occurs
+on every call. Repetitions, prefixes and environments are not independent problems.
+
+A separate comparison of all five modes, 48 graphs and five lengths confirms
+**1,200 entire outputs and all returned metadata identical to the parent**.
+The timing audit also enforces same-mode raw/route byte equality and auto equality
+with its reported selected engine.
+
+## Verification
+
+| Check | Result |
+|---|---:|
+| All local compiled-query modules, in recorded groups/fresh processes | 455 passed |
+| Focused local subset, included above | 152 passed |
+| Focused CI: x86 Py3.11, x86 Py3.13, ARM64 Py3.13 | 152 passed each |
+| Windows x64/MSVC Py3.13 | 156 passed |
+| CI exact contracts under UBSan | 112 passed |
+| CI exact contracts under ASan + UBSan | 112 passed |
+| Three downloaded CI audits replayed with Python -S, no native solver | All identical |
+| Stable spectra/, tests/, results/, data/ against user checkpoint | Unchanged |
+
+All seven jobs in run **38781025834** completed successfully. Its trigger commit
+is 512ecc64; the dependent jobs check out actual published implementation 8d28a637.
+Local timing commit c3b602f8 has the same executable/test subtree and native hash;
+its workflow-only ancestry differs. Later reporting and read-only workflow cleanup
+commits do not alter tested native code.
+
+ASan used detect_leaks=0: no LeakSanitizer claim. Windows is functional/build
+coverage, not a Windows timing panel. The remaining local compiler modules used
+actual native CUDD. This step does not claim a rerun of the entire model/training
+repository suite or promote the experiment into the stable installed API.
+
+## Negative observations retained
+
+An initial combined local compiled-query run ended without a final result. Its
+partial log is retained and not counted as a pass. All modules subsequently passed
+in recorded groups/fresh processes, with JUnit results. Separately run module and
+benchmark/replay controllers retain their explicit exit statuses.
+
+The x86/Py3.13 CI has one single-request **new-auto/new-raw** ratio of 1.313129 on
+`percolated_grid-r4-n512-d1`. Local retains two 63-request new-auto/new-raw ratios
+above 1.25: 1.423691 on `geometric-r4-n512-d1` and 1.396579 on
+`random_bipartite-r3-n512-d0`. These are not regressions against parent auto, but
+rule out a claim that auto is never slower than raw on individual measurements.
+None were dropped or retried until favorable. No auto/parent-auto cell exceeds
+1.25 in the four runs; this is not a universal no-regression guarantee.
+
+Explicit route remains substantially slower than raw on many short-call cells.
+The user's automatic policy, all seven arms, all slow cells and per-family
+results are retained. No historical frozen speed failure is reclassified or
+retuned. No new holdout, external workload, outside-team replication, adoption,
+priority determination, universal memory bound or production latency is claimed.
+
+## Assessment and next gap
+
+My provisional whole-program judgment is **78/100**, not a measured statistic.
+Relative to the earlier 75, credit comes primarily from the user's demonstrated
+platform coverage and publication, plus stronger current execution evidence.
+Removing redundant sorts does not increase the novelty score.
+
+Rubric: importance 9/12; correctness 15/15; experimental rigor 17/18;
+comparators/attribution 14/15; novelty/depth 8/15; generalization/portability 8/10;
+repository/release coherence 7/8; independent replication/impact 0/7.
+
+The next larger gaps are a versioned installed exact-query API and an
+operator-defined evaluation. Any new prospective test needs a newly frozen
+endpoint/protocol and new workload, not a relabeling of these exposed 48 graphs.
+
+Publication is isolated from the user's branch. Temporary patch transport is
+removed and the retained workflow is read-only. No merge/default promotion is
+implied. Completed workflow:
+https://github.com/tugrapaydiner/SPECTRA/actions/runs/38781025834
+
+The recovery handoff retains original CI ZIPs with GitHub SHA-256 receipts, full
+local raw evidence, three replay receipts, the five-mode equivalence comparison,
+test logs including the incomplete attempt, and exact published Git source.
+Hosted artifacts have their stated 30-day retention; the handoff is the durable copy.