diff --git a/.github/workflows/faster-query-review.yml b/.github/workflows/faster-query-review.yml new file mode 100644 index 0000000..4221e45 --- /dev/null +++ b/.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 diff --git a/experiments/compiled_query/LINEAR_CONSTRUCTION.md b/experiments/compiled_query/LINEAR_CONSTRUCTION.md new file mode 100644 index 0000000..78823c4 --- /dev/null +++ b/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 +``` diff --git a/experiments/compiled_query/LINEAR_REVIEW_20261015.md b/experiments/compiled_query/LINEAR_REVIEW_20261015.md new file mode 100644 index 0000000..1dcb03e --- /dev/null +++ b/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. diff --git a/experiments/compiled_query/exact_native.cpp b/experiments/compiled_query/exact_native.cpp index 36c2834..96182ee 100644 --- a/experiments/compiled_query/exact_native.cpp +++ b/experiments/compiled_query/exact_native.cpp @@ -357,8 +357,26 @@ struct Index { arcs.emplace_back(a,b^1U);arcs.emplace_back(b,a^1U); } } - std::sort(arcs.begin(),arcs.end());arcs.erase(std::unique(arcs.begin(),arcs.end()),arcs.end()); - full_arcs=arcs.size();original=CSR(2*n,arcs);CSR reverse(2*n,arcs,true);comp=components(original,reverse); + // Input owns sorted unique (u,v), u(comp[2*v]> i & 1) + for masks in itertools.product((1, 2, 3, 4, 5, 6), repeat=3): + p = BinaryListProblem.create(3, 3, edges, masks) + replay(diagnostic, p, ((), ((0, 1),), ((1, 2),), ((2, 0),))) + + +@pytest.mark.parametrize('n', (0, 1, 2, 31, 64, 129)) +def test_large_labels_relabelling_and_tile_boundaries(diagnostic, n): + rng = random.Random(58013 + n) + labels = (0, 1, 17, 62, 63) + masks = tuple(sum(1 << c for c in rng.sample(labels, rng.choice((1, 2)))) + for _ in range(n)) + edges = tuple((u, v) for u in range(n) for v in range(u + 1, n) + if rng.random() < .19) + p = BinaryListProblem.create(n, 64, edges, masks) + rows = tuple(tuple((rng.randrange(n), rng.getrandbits(64)) + for _ in range(rng.randrange(5))) if n else () + for _ in range(129)) + for count in (1, 63, 64, 65, 129): + replay(diagnostic, p, rows[:count]) + + +def test_tuple_normalization_precedes_linear_native_construction(diagnostic): + # Bypass BinaryListProblem normalization: the native tuple path must still + # supply canonical edges to the new constructor before either CSR is built. + module = diagnostic._module + canonical = ((0, 1), (0, 3), (1, 2), (2, 3)) + noisy = ((3, 2), (3, 0), (0, 1), (2, 1), (1, 0), (0, 3)) + masks = (3, 1, 3, 2) + for mode in range(4): + a = module.create(4, 2, canonical, masks, mode, 16 << 20) + b = module.create(4, 2, noisy, masks, mode, 16 << 20) + assert module.info(a) == module.info(b) + for query in ((), ((0, 1),), ((0, 2),), ((3, 0),)): + assert module.solve(a, query) == module.solve(b, query)