From cf76445e5b896f91aaccefcfbe96f1c023a8ea70 Mon Sep 17 00:00:00 2001 From: Tugrap <106766396+tugrapaydiner@users.noreply.github.com> Date: Thu, 15 Oct 2026 13:40:37 -0400 Subject: [PATCH 1/7] Preserve exact user checkpoint for isolated query-runtime review --- .github/workflows/faster-query-review.yml | 35 +++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 .github/workflows/faster-query-review.yml diff --git a/.github/workflows/faster-query-review.yml b/.github/workflows/faster-query-review.yml new file mode 100644 index 0000000..f67c14d --- /dev/null +++ b/.github/workflows/faster-query-review.yml @@ -0,0 +1,35 @@ +name: Faster query review +on: + push: + branches: [research/faster-queries-review-20261015] + paths: ['.github/workflows/faster-query-review.yml'] + workflow_dispatch: +permissions: + contents: read +concurrency: + group: faster-query-review-${{ github.ref }} + cancel-in-progress: false +jobs: + source: + runs-on: ubuntu-24.04 + timeout-minutes: 5 + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + persist-credentials: false + - name: Preserve source and complete ancestry + run: | + set -euo pipefail + mkdir -p /tmp/review-source + git rev-parse HEAD > /tmp/review-source/commit.txt + git rev-parse HEAD^{tree} > /tmp/review-source/tree.txt + git bundle create /tmp/review-source/source.bundle HEAD + cd /tmp/review-source + sha256sum source.bundle > SHA256SUMS.txt + - uses: actions/upload-artifact@v4 + with: + name: faster-query-review-source-${{ github.run_id }} + path: /tmp/review-source/ + retention-days: 30 + if-no-files-found: error From f19cffb20308b198415753372e6adaaffe982da5 Mon Sep 17 00:00:00 2001 From: Tugrap <106766396+tugrapaydiner@users.noreply.github.com> Date: Thu, 15 Oct 2026 13:52:02 -0400 Subject: [PATCH 2/7] Stage tested canonical-construction delta without altering the user's branch --- .delivery/canonical-construction.patch | 216 +++++++++++++++++++++++++ 1 file changed, 216 insertions(+) create mode 100644 .delivery/canonical-construction.patch diff --git a/.delivery/canonical-construction.patch b/.delivery/canonical-construction.patch new file mode 100644 index 0000000..2c0abc4 --- /dev/null +++ b/.delivery/canonical-construction.patch @@ -0,0 +1,216 @@ +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/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) From 512ecc64be6c07c205460210475540b513e06f20 Mon Sep 17 00:00:00 2001 From: Tugrap <106766396+tugrapaydiner@users.noreply.github.com> Date: Thu, 15 Oct 2026 13:53:04 -0400 Subject: [PATCH 3/7] Validate and publish the bounded sort-elision change, then compare against the user's latest engine --- .github/workflows/faster-query-review.yml | 166 +++++++++++++++++++++- 1 file changed, 161 insertions(+), 5 deletions(-) diff --git a/.github/workflows/faster-query-review.yml b/.github/workflows/faster-query-review.yml index f67c14d..15ec796 100644 --- a/.github/workflows/faster-query-review.yml +++ b/.github/workflows/faster-query-review.yml @@ -10,26 +10,182 @@ concurrency: group: faster-query-review-${{ github.ref }} cancel-in-progress: false jobs: - source: + publish: runs-on: ubuntu-24.04 - timeout-minutes: 5 + timeout-minutes: 10 + permissions: + contents: write + outputs: + commit: ${{ steps.publish.outputs.commit }} steps: - uses: actions/checkout@v4 with: fetch-depth: 0 - persist-credentials: false - - name: Preserve source and complete ancestry + - 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: Verify the reviewed patch and limit its scope + run: | + set -euo pipefail + test "$(git rev-parse HEAD)" = "$GITHUB_SHA" + git merge-base --is-ancestor 098a8477f6cc8bb696423e78c4d6b6a26a95a0e1 HEAD + echo '2aecaebda361d2ef292b11739b2bf031513dfd7fa99654300371fd33926ef09d .delivery/canonical-construction.patch' | sha256sum --check + git apply --check --index .delivery/canonical-construction.patch + git apply --index .delivery/canonical-construction.patch + python - <<'PY' + import subprocess + expected = {'experiments/compiled_query/exact_native.cpp', 'experiments/compiled_query/test_linear_construction.py', 'experiments/compiled_query/LINEAR_CONSTRUCTION.md'} + actual = set(subprocess.check_output(['git','diff','--cached','--name-only'],text=True).splitlines()) + assert actual == expected, (actual, expected) + PY + echo '67a8b5c8c55dd4fdc5070f2308cabf37a463a7a1294f12a8dd496d792852fb25 experiments/compiled_query/exact_native.cpp' | sha256sum --check + - name: Require the focused native and evidence contracts before publication run: | set -euo pipefail mkdir -p /tmp/review-source + 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=/tmp/review-source/contracts.xml 2>&1 | tee /tmp/review-source/contracts.log + - name: Publish only the tested non-workflow changes + id: publish + run: | + set -euo pipefail + git rm .delivery/canonical-construction.patch + git config user.name 'Tugrap' + git config user.email '106766396+tugrapaydiner@users.noreply.github.com' + git commit -m 'Build canonical implication graphs without redundant global sorts' + git push origin HEAD:research/faster-queries-review-20261015 + echo "commit=$(git rev-parse HEAD)" >> "$GITHUB_OUTPUT" git rev-parse HEAD > /tmp/review-source/commit.txt git rev-parse HEAD^{tree} > /tmp/review-source/tree.txt git bundle create /tmp/review-source/source.bundle HEAD cd /tmp/review-source sha256sum source.bundle > SHA256SUMS.txt - uses: actions/upload-artifact@v4 + if: always() with: name: faster-query-review-source-${{ github.run_id }} path: /tmp/review-source/ retention-days: 30 - if-no-files-found: error + if-no-files-found: warn + compare: + needs: publish + 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: + ref: ${{ needs.publish.outputs.commit }} + 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 immediate parent + 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: + needs: publish + runs-on: ubuntu-24.04 + timeout-minutes: 15 + strategy: + fail-fast: false + matrix: + sanitizer: ['undefined', 'address,undefined'] + steps: + - uses: actions/checkout@v4 + with: + ref: ${{ needs.publish.outputs.commit }} + 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: + needs: publish + runs-on: windows-2022 + timeout-minutes: 15 + env: + PYTHONUTF8: '1' + steps: + - run: git config --global core.autocrlf false + - uses: actions/checkout@v4 + with: + ref: ${{ needs.publish.outputs.commit }} + 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 From 8d28a63707a1e3d56d5d16688924cd3985ee80d7 Mon Sep 17 00:00:00 2001 From: Tugrap <106766396+tugrapaydiner@users.noreply.github.com> Date: Thu, 15 Oct 2026 17:53:57 +0000 Subject: [PATCH 4/7] Build canonical implication graphs without redundant global sorts --- .delivery/canonical-construction.patch | 216 ------------------ .../compiled_query/LINEAR_CONSTRUCTION.md | 74 ++++++ experiments/compiled_query/exact_native.cpp | 28 ++- .../test_linear_construction.py | 84 +++++++ 4 files changed, 182 insertions(+), 220 deletions(-) delete mode 100644 .delivery/canonical-construction.patch create mode 100644 experiments/compiled_query/LINEAR_CONSTRUCTION.md create mode 100644 experiments/compiled_query/test_linear_construction.py diff --git a/.delivery/canonical-construction.patch b/.delivery/canonical-construction.patch deleted file mode 100644 index 2c0abc4..0000000 --- a/.delivery/canonical-construction.patch +++ /dev/null @@ -1,216 +0,0 @@ -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/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) 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/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) From 845ec859cfa1245fd59d642dc6774a0dd4f5dba4 Mon Sep 17 00:00:00 2001 From: Tugrap <106766396+tugrapaydiner@users.noreply.github.com> Date: Thu, 15 Oct 2026 14:02:09 -0400 Subject: [PATCH 5/7] Replace completed one-shot publication with read-only query regression checks --- .github/workflows/faster-query-review.yml | 72 +++-------------------- 1 file changed, 7 insertions(+), 65 deletions(-) diff --git a/.github/workflows/faster-query-review.yml b/.github/workflows/faster-query-review.yml index 15ec796..4221e45 100644 --- a/.github/workflows/faster-query-review.yml +++ b/.github/workflows/faster-query-review.yml @@ -2,7 +2,12 @@ name: Faster query review on: push: branches: [research/faster-queries-review-20261015] - paths: ['.github/workflows/faster-query-review.yml'] + 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 @@ -10,65 +15,7 @@ concurrency: group: faster-query-review-${{ github.ref }} cancel-in-progress: false jobs: - publish: - runs-on: ubuntu-24.04 - timeout-minutes: 10 - permissions: - contents: write - outputs: - commit: ${{ steps.publish.outputs.commit }} - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - - 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: Verify the reviewed patch and limit its scope - run: | - set -euo pipefail - test "$(git rev-parse HEAD)" = "$GITHUB_SHA" - git merge-base --is-ancestor 098a8477f6cc8bb696423e78c4d6b6a26a95a0e1 HEAD - echo '2aecaebda361d2ef292b11739b2bf031513dfd7fa99654300371fd33926ef09d .delivery/canonical-construction.patch' | sha256sum --check - git apply --check --index .delivery/canonical-construction.patch - git apply --index .delivery/canonical-construction.patch - python - <<'PY' - import subprocess - expected = {'experiments/compiled_query/exact_native.cpp', 'experiments/compiled_query/test_linear_construction.py', 'experiments/compiled_query/LINEAR_CONSTRUCTION.md'} - actual = set(subprocess.check_output(['git','diff','--cached','--name-only'],text=True).splitlines()) - assert actual == expected, (actual, expected) - PY - echo '67a8b5c8c55dd4fdc5070f2308cabf37a463a7a1294f12a8dd496d792852fb25 experiments/compiled_query/exact_native.cpp' | sha256sum --check - - name: Require the focused native and evidence contracts before publication - run: | - set -euo pipefail - mkdir -p /tmp/review-source - 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=/tmp/review-source/contracts.xml 2>&1 | tee /tmp/review-source/contracts.log - - name: Publish only the tested non-workflow changes - id: publish - run: | - set -euo pipefail - git rm .delivery/canonical-construction.patch - git config user.name 'Tugrap' - git config user.email '106766396+tugrapaydiner@users.noreply.github.com' - git commit -m 'Build canonical implication graphs without redundant global sorts' - git push origin HEAD:research/faster-queries-review-20261015 - echo "commit=$(git rev-parse HEAD)" >> "$GITHUB_OUTPUT" - git rev-parse HEAD > /tmp/review-source/commit.txt - git rev-parse HEAD^{tree} > /tmp/review-source/tree.txt - git bundle create /tmp/review-source/source.bundle HEAD - cd /tmp/review-source - sha256sum source.bundle > SHA256SUMS.txt - - uses: actions/upload-artifact@v4 - if: always() - with: - name: faster-query-review-source-${{ github.run_id }} - path: /tmp/review-source/ - retention-days: 30 - if-no-files-found: warn compare: - needs: publish runs-on: ${{ matrix.runner }} timeout-minutes: 20 strategy: @@ -81,7 +28,6 @@ jobs: steps: - uses: actions/checkout@v4 with: - ref: ${{ needs.publish.outputs.commit }} fetch-depth: 0 persist-credentials: false - uses: actions/setup-python@v5 @@ -94,7 +40,7 @@ jobs: 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 immediate parent + - 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 @@ -107,7 +53,6 @@ jobs: retention-days: 30 if-no-files-found: warn sanitizers: - needs: publish runs-on: ubuntu-24.04 timeout-minutes: 15 strategy: @@ -117,7 +62,6 @@ jobs: steps: - uses: actions/checkout@v4 with: - ref: ${{ needs.publish.outputs.commit }} persist-credentials: false - uses: actions/setup-python@v5 with: @@ -145,7 +89,6 @@ jobs: retention-days: 30 if-no-files-found: warn windows: - needs: publish runs-on: windows-2022 timeout-minutes: 15 env: @@ -154,7 +97,6 @@ jobs: - run: git config --global core.autocrlf false - uses: actions/checkout@v4 with: - ref: ${{ needs.publish.outputs.commit }} persist-credentials: false - uses: actions/setup-python@v5 with: From 5856ee78db9cd89dcceda593721432769dd0d648 Mon Sep 17 00:00:00 2001 From: Tugrap <106766396+tugrapaydiner@users.noreply.github.com> Date: Thu, 15 Oct 2026 14:05:46 -0400 Subject: [PATCH 6/7] Record immediate-parent latency gains, platform checks and retained negative observations --- .../compiled_query/LINEAR_REVIEW_20261015.md | 185 ++++++++++++++++++ 1 file changed, 185 insertions(+) create mode 100644 experiments/compiled_query/LINEAR_REVIEW_20261015.md diff --git a/experiments/compiled_query/LINEAR_REVIEW_20261015.md b/experiments/compiled_query/LINEAR_REVIEW_20261015.md new file mode 100644 index 0000000..219e632 --- /dev/null +++ b/experiments/compiled_query/LINEAR_REVIEW_20261015.md @@ -0,0 +1,185 @@ +# Continuing the user's faster-queries checkpoint + +**15 October 2026. Exposed synthetic development, not a new confirmation.** + +## Starting point and preserved work + +This continuation starts at the user's `faster-queries` commit +`098a8477f6cc8bb696423e78c4d6b6a26a95a0e1`, not the older prepared-transfer branch. +The user's automatic engine policy, prepared-root contradiction reconstruction, +direct SAT witness serialization, reusable per-call proof scratch, Windows/MSVC +support and seven-arm comparison are retained. The original `faster-queries` +branch is not rewritten. Main, PR #60 and PR #61 are not merged or replaced. + +The user's latest completed seven-arm run, `38691730508`, already passes the +10% development target in all three measured environments. At 1,024 queries, +its auto/equally improved raw ratios are 0.885672 (x86 Python 3.11), 0.896982 +(x86 Python 3.13), and 0.889297 (ARM64 Python 3.13). Its older failed target at +`2afaf00` remains historical evidence. This review does not take credit for the +user's improvements or treat that older failure as the current outcome. + +## New implementation + +Tested, published implementation: **`8d28a63707a1e3d56d5d16688924cd3985ee80d7`**. +Tree: `0753490153b4e68036e30be738f305eed96e57f8`. +Native source SHA-256: +`67a8b5c8c55dd4fdc5070f2308cabf37a463a7a1294f12a8dd496d792852fb25`. + +The core delta is three files: `exact_native.cpp`, +`test_linear_construction.py`, and [the construction proof](LINEAR_CONSTRUCTION.md). +Two unnecessary global sorts are removed: the implication arc sort/deduplication +and the observer's forbidden-pair sort/deduplication. Both were redundant after +canonical original-edge admission. Every original observer constraint is retained. +The raw control gets the same applicable improvement as the optimized modes. + +Stable forward and reverse CSR scattering now consumes the already ordered +per-vertex incident subsequences. Both resulting adjacencies are byte-for-byte +identical to the previous sorted construction, including singleton unit arcs. +A diagnostic-only native build actually constructs both versions and compares +all four CSR arrays and arc counts before SCC processing. It is never timed. +No ABI, packet format, resource cap, engine-selection threshold or default changes. + +Implication emission plus both CSR builds are O(n+a) after canonical admission, +where a is the implication count. This is not a linear-time claim for the entire +routed constructor: downstream condensation and routing-bridge sorts remain. +It is an implementation specialization, not a new 2-SAT algorithm or a priority +claim. Canonical tuple normalization also retains its own cost. + +## Matched complete-call results against the immediate user checkpoint + +Baseline is **098a847**, not an earlier slower implementation. The existing +seven-arm harness, 48 exposed graph realizations, eight families, five bank sizes, +nine paired repetitions, two warmups, order permutations, process limits and +independent original-input replay are unchanged. Both versions use the same +compiler and options on each host. Raw, routed and automatic parent engines are +all retained; current raw, SCC, routed and automatic engines are all reported. + +The timed boundary is ready immutable SBC1 input through input hashing, native +construction, all solving, complete witnesses/proofs, independent serialized-output +verification, SCQ2 creation, disposal, and output hashing. Packet preparation, +compilation, process startup, evidence writes and post-run Python replay are +outside it. Process wall time and RSS remain separate; this is not a production +latency or total-input-ingestion claim. + +Ratios below are **new automatic-engine time / immediate-parent automatic-engine +time**. Lower is better. They aggregate per-graph median complete-call times +geometrically, rather than pooling individual requests as independent samples. + +| Queries per prepared call | Local x86 / Python 3.13 | CI x86 / Python 3.11 | CI x86 / Python 3.13 | CI ARM64 / Python 3.13 | +|---|---:|---:|---:|---:| +| 1 | 0.547348 | 0.552124 | 0.621886 | 0.663518 | +| 63 | 0.692641 | 0.688031 | 0.730851 | 0.763819 | +| 64 | 0.665747 | 0.682101 | 0.717376 | 0.754774 | +| 65 | 0.682029 | 0.674030 | 0.723055 | 0.756958 | +| 1,024 | 0.922051 | 0.931766 | 0.960653 | 0.945146 | + +The three CI environments therefore show **33.6-44.8% less single-request time** +and **3.9-6.8% less 1,024-request time** than the user's latest automatic engine. +The improvement is predominantly construction cost, not a new propagation rule. + +| CI environment | New/parent auto at 1,024 | Stratified graph-bootstrap 95% interval | New auto / new raw at 1,024 | Existing development target | +|---|---:|---:|---:|---| +| x86 / Python 3.11 | 0.931766 | [0.913470, 0.948929] | 0.878810 | PASS | +| x86 / Python 3.13 | 0.960653 | [0.945421, 0.974489] | 0.897270 | PASS | +| ARM64 / Python 3.13 | 0.945146 | [0.930190, 0.958338] | 0.882249 | PASS | + +The original target is not relaxed: long-bank auto/raw <= 0.90, its upper +95% bound < 1, every family <= 1.10, and single-request aggregate <= 1.10. +The local run also passes. These intervals describe this fixed exposed synthetic +panel, not a population of real applications or independently selected families. + +Every environment completes **15,120 scheduled timed calls and 48 workers**. +Each audit independently checks **1,636 distinct packet/output pairs containing +484,546 decisions**; repeated outputs are deduplicated only in post-run replay. +Native verification still occurs on every call. Repetitions, environments and +prefixes must not be counted as independent problem instances. + +A separate five-mode comparison across all 48 graphs and five lengths verifies +**1,200 complete outputs and all returned metadata identical to the parent**. +The production benchmark separately enforces same-mode raw/routed output equality +and automatic-output equality with its reported selected engine. + +## Tests and independent replay + +| Check | Observed outcome | +|---|---:| +| All compiled-query test modules locally, in recorded groups/fresh processes | 455 passed | +| Focused local subset, included in the 455 | 152 passed | +| Focused CI on x86 Python 3.11 and 3.13 and native ARM64 Python 3.13 | 152 passed on each | +| Actual Windows x64/MSVC, Python 3.13 | 156 passed | +| CI exact-service contracts under UBSan | 112 passed | +| CI exact-service contracts under ASan + UBSan | 112 passed | +| Downloaded final CI audits replayed using Python -S without a native solver | All three identical | +| Stable spectra/, tests/, results/ and data/ versus user checkpoint | Unchanged | + +All seven jobs in workflow `38781025834` finished successfully. The completed +implementation is 8d28a637; its workflow trigger commit is 512ecc64. Each dependent +job checked out the actual published implementation, not the staging commit. +The local timing commit is c3b602f8; its executable/test subtree matches 8d28a637, +and both native source hashes are the value above. Their workflow-only ancestry +differs. Later workflow cleanup/reporting commits do not change that tested code. + +ASan uses detect_leaks=0, so no LeakSanitizer result is claimed. Windows establishes +build and functional coverage here, not a Windows timing-panel result. Local +remaining compiler modules require actual native CUDD; they are not Python-only +substitutes. This step does not claim a rerun of the full model/training repository +suite. The stable public source directories are unchanged. + +## Retained failures and limitations + +An initial combined local compiled-query run ended without a final result. Its +partial log is retained and is not counted as passed. All modules were subsequently +run successfully in the recorded groups/fresh processes above, with JUnit results +and explicit exit statuses for the separately run groups and comparison workers. + +The x86/Python 3.13 CI retains one single-request **new-auto/new-raw** ratio of +1.313129 on `percolated_grid-r4-n512-d1`. The local run 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`. They are not regressions against the parent auto +engine; they still prevent a claim that automatic selection is never slower than +raw on individual measurements. None were removed or rerun until favorable. +No auto/parent-auto cell exceeds 1.25 in these four runs. This is not a universal +no-regression guarantee. Explicit routed mode still loses substantially to raw +on many short-call cells, which is why the user's automatic policy is preserved. + +All exposed cases, all arms, every stored timing, per-family summary and slow +cell remain in the full audits/artifacts. No frozen prior speed failure has been +relabelled or retuned. There is no new outside workload, outside-team replication, +operator adoption, stable installed API promotion or algorithmic-priority result. + +## Assessment and publication + +A provisional whole-program review judgment is **78/100**, not a measured score. +The earlier 75 is improved primarily by the user's now-demonstrated platform +coverage and clean publication, with the new construction optimization adding +execution evidence. It is not a novelty-score increase for removing sorts. + +| Category | Score | +|---|---:| +| Importance and focus | 9/12 | +| Correctness and contracts | 15/15 | +| Experimental rigor | 17/18 | +| Competitors and attribution | 14/15 | +| Novelty and scientific depth | 8/15 | +| Generalization and portability | 8/10 | +| Repository/release coherence | 7/8 | +| Independent replication and impact | 0/7 | + +The code remains opt-in research. A versioned installed exact-query API and an +operator-defined evaluation would address larger remaining gaps than another +exposed-panel tuning cycle. The next prospective test must use a newly frozen +endpoint/protocol and new workload, not rename these already exposed 48 graphs. + +This continuation is isolated on `research/faster-queries-review-20261015`, based +on `faster-queries`. The temporary source patch is removed and the publication +workflow is replaced by read-only validation. Main and the user's branch are +unchanged. No default promotion or merge is implied. + +Completed cross-platform workflow: +https://github.com/tugrapaydiner/SPECTRA/actions/runs/38781025834 + +The recovery handoff contains immutable original CI ZIPs with their GitHub SHA-256 +receipts, full local evidence, all three separate replay receipts, the 1,200-output +comparison, test logs (including the incomplete combined attempt), and the exact +published Git source. Hosted artifacts retain their stated 30-day lifetime; the +recovery archive is the durable copy. From dfa45150293e9701290578b40c794a3d5aa86c47 Mon Sep 17 00:00:00 2001 From: Tugrap <106766396+tugrapaydiner@users.noreply.github.com> Date: Thu, 15 Oct 2026 14:08:35 -0400 Subject: [PATCH 7/7] Tighten checkpoint report and use exact rounded local ratios from the audit --- .../compiled_query/LINEAR_REVIEW_20261015.md | 317 ++++++++---------- 1 file changed, 148 insertions(+), 169 deletions(-) diff --git a/experiments/compiled_query/LINEAR_REVIEW_20261015.md b/experiments/compiled_query/LINEAR_REVIEW_20261015.md index 219e632..1dcb03e 100644 --- a/experiments/compiled_query/LINEAR_REVIEW_20261015.md +++ b/experiments/compiled_query/LINEAR_REVIEW_20261015.md @@ -1,185 +1,164 @@ -# Continuing the user's faster-queries checkpoint - -**15 October 2026. Exposed synthetic development, not a new confirmation.** - -## Starting point and preserved work - -This continuation starts at the user's `faster-queries` commit -`098a8477f6cc8bb696423e78c4d6b6a26a95a0e1`, not the older prepared-transfer branch. -The user's automatic engine policy, prepared-root contradiction reconstruction, -direct SAT witness serialization, reusable per-call proof scratch, Windows/MSVC -support and seven-arm comparison are retained. The original `faster-queries` -branch is not rewritten. Main, PR #60 and PR #61 are not merged or replaced. - -The user's latest completed seven-arm run, `38691730508`, already passes the -10% development target in all three measured environments. At 1,024 queries, -its auto/equally improved raw ratios are 0.885672 (x86 Python 3.11), 0.896982 -(x86 Python 3.13), and 0.889297 (ARM64 Python 3.13). Its older failed target at -`2afaf00` remains historical evidence. This review does not take credit for the -user's improvements or treat that older failure as the current outcome. - -## New implementation - -Tested, published implementation: **`8d28a63707a1e3d56d5d16688924cd3985ee80d7`**. -Tree: `0753490153b4e68036e30be738f305eed96e57f8`. -Native source SHA-256: -`67a8b5c8c55dd4fdc5070f2308cabf37a463a7a1294f12a8dd496d792852fb25`. - -The core delta is three files: `exact_native.cpp`, -`test_linear_construction.py`, and [the construction proof](LINEAR_CONSTRUCTION.md). -Two unnecessary global sorts are removed: the implication arc sort/deduplication -and the observer's forbidden-pair sort/deduplication. Both were redundant after -canonical original-edge admission. Every original observer constraint is retained. -The raw control gets the same applicable improvement as the optimized modes. - -Stable forward and reverse CSR scattering now consumes the already ordered -per-vertex incident subsequences. Both resulting adjacencies are byte-for-byte -identical to the previous sorted construction, including singleton unit arcs. -A diagnostic-only native build actually constructs both versions and compares -all four CSR arrays and arc counts before SCC processing. It is never timed. -No ABI, packet format, resource cap, engine-selection threshold or default changes. - -Implication emission plus both CSR builds are O(n+a) after canonical admission, -where a is the implication count. This is not a linear-time claim for the entire -routed constructor: downstream condensation and routing-bridge sorts remain. -It is an implementation specialization, not a new 2-SAT algorithm or a priority -claim. Canonical tuple normalization also retains its own cost. - -## Matched complete-call results against the immediate user checkpoint - -Baseline is **098a847**, not an earlier slower implementation. The existing -seven-arm harness, 48 exposed graph realizations, eight families, five bank sizes, -nine paired repetitions, two warmups, order permutations, process limits and -independent original-input replay are unchanged. Both versions use the same -compiler and options on each host. Raw, routed and automatic parent engines are -all retained; current raw, SCC, routed and automatic engines are all reported. - -The timed boundary is ready immutable SBC1 input through input hashing, native -construction, all solving, complete witnesses/proofs, independent serialized-output -verification, SCQ2 creation, disposal, and output hashing. Packet preparation, -compilation, process startup, evidence writes and post-run Python replay are -outside it. Process wall time and RSS remain separate; this is not a production -latency or total-input-ingestion claim. - -Ratios below are **new automatic-engine time / immediate-parent automatic-engine -time**. Lower is better. They aggregate per-graph median complete-call times -geometrically, rather than pooling individual requests as independent samples. - -| Queries per prepared call | Local x86 / Python 3.13 | CI x86 / Python 3.11 | CI x86 / Python 3.13 | CI ARM64 / Python 3.13 | +# 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.692641 | 0.688031 | 0.730851 | 0.763819 | -| 64 | 0.665747 | 0.682101 | 0.717376 | 0.754774 | -| 65 | 0.682029 | 0.674030 | 0.723055 | 0.756958 | +| 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 | -The three CI environments therefore show **33.6-44.8% less single-request time** -and **3.9-6.8% less 1,024-request time** than the user's latest automatic engine. -The improvement is predominantly construction cost, not a new propagation rule. +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 at 1,024 | Stratified graph-bootstrap 95% interval | New auto / new raw at 1,024 | Existing development target | +| CI environment | New/parent auto, 1,024 | Graph-bootstrap 95% interval | New auto/new raw, 1,024 | Development target | |---|---:|---:|---:|---| -| x86 / Python 3.11 | 0.931766 | [0.913470, 0.948929] | 0.878810 | PASS | -| x86 / Python 3.13 | 0.960653 | [0.945421, 0.974489] | 0.897270 | PASS | -| ARM64 / Python 3.13 | 0.945146 | [0.930190, 0.958338] | 0.882249 | PASS | +| 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 original target is not relaxed: long-bank auto/raw <= 0.90, its upper -95% bound < 1, every family <= 1.10, and single-request aggregate <= 1.10. -The local run also passes. These intervals describe this fixed exposed synthetic -panel, not a population of real applications or independently selected families. +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. -Every environment completes **15,120 scheduled timed calls and 48 workers**. -Each audit independently checks **1,636 distinct packet/output pairs containing -484,546 decisions**; repeated outputs are deduplicated only in post-run replay. -Native verification still occurs on every call. Repetitions, environments and -prefixes must not be counted as independent problem instances. +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 five-mode comparison across all 48 graphs and five lengths verifies -**1,200 complete outputs and all returned metadata identical to the parent**. -The production benchmark separately enforces same-mode raw/routed output equality -and automatic-output equality with its reported selected engine. +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. -## Tests and independent replay +## Verification -| Check | Observed outcome | +| Check | Result | |---|---:| -| All compiled-query test modules locally, in recorded groups/fresh processes | 455 passed | -| Focused local subset, included in the 455 | 152 passed | -| Focused CI on x86 Python 3.11 and 3.13 and native ARM64 Python 3.13 | 152 passed on each | -| Actual Windows x64/MSVC, Python 3.13 | 156 passed | -| CI exact-service contracts under UBSan | 112 passed | -| CI exact-service contracts under ASan + UBSan | 112 passed | -| Downloaded final CI audits replayed using Python -S without a native solver | All three identical | -| Stable spectra/, tests/, results/ and data/ versus user checkpoint | Unchanged | - -All seven jobs in workflow `38781025834` finished successfully. The completed -implementation is 8d28a637; its workflow trigger commit is 512ecc64. Each dependent -job checked out the actual published implementation, not the staging commit. -The local timing commit is c3b602f8; its executable/test subtree matches 8d28a637, -and both native source hashes are the value above. Their workflow-only ancestry -differs. Later workflow cleanup/reporting commits do not change that tested code. - -ASan uses detect_leaks=0, so no LeakSanitizer result is claimed. Windows establishes -build and functional coverage here, not a Windows timing-panel result. Local -remaining compiler modules require actual native CUDD; they are not Python-only -substitutes. This step does not claim a rerun of the full model/training repository -suite. The stable public source directories are unchanged. - -## Retained failures and limitations +| 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 is not counted as passed. All modules were subsequently -run successfully in the recorded groups/fresh processes above, with JUnit results -and explicit exit statuses for the separately run groups and comparison workers. - -The x86/Python 3.13 CI retains one single-request **new-auto/new-raw** ratio of -1.313129 on `percolated_grid-r4-n512-d1`. The local run 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`. They are not regressions against the parent auto -engine; they still prevent a claim that automatic selection is never slower than -raw on individual measurements. None were removed or rerun until favorable. -No auto/parent-auto cell exceeds 1.25 in these four runs. This is not a universal -no-regression guarantee. Explicit routed mode still loses substantially to raw -on many short-call cells, which is why the user's automatic policy is preserved. - -All exposed cases, all arms, every stored timing, per-family summary and slow -cell remain in the full audits/artifacts. No frozen prior speed failure has been -relabelled or retuned. There is no new outside workload, outside-team replication, -operator adoption, stable installed API promotion or algorithmic-priority result. - -## Assessment and publication - -A provisional whole-program review judgment is **78/100**, not a measured score. -The earlier 75 is improved primarily by the user's now-demonstrated platform -coverage and clean publication, with the new construction optimization adding -execution evidence. It is not a novelty-score increase for removing sorts. - -| Category | Score | -|---|---:| -| Importance and focus | 9/12 | -| Correctness and contracts | 15/15 | -| Experimental rigor | 17/18 | -| Competitors and attribution | 14/15 | -| Novelty and scientific depth | 8/15 | -| Generalization and portability | 8/10 | -| Repository/release coherence | 7/8 | -| Independent replication and impact | 0/7 | - -The code remains opt-in research. A versioned installed exact-query API and an -operator-defined evaluation would address larger remaining gaps than another -exposed-panel tuning cycle. The next prospective test must use a newly frozen -endpoint/protocol and new workload, not rename these already exposed 48 graphs. - -This continuation is isolated on `research/faster-queries-review-20261015`, based -on `faster-queries`. The temporary source patch is removed and the publication -workflow is replaced by read-only validation. Main and the user's branch are -unchanged. No default promotion or merge is implied. - -Completed cross-platform workflow: +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 contains immutable original CI ZIPs with their GitHub SHA-256 -receipts, full local evidence, all three separate replay receipts, the 1,200-output -comparison, test logs (including the incomplete combined attempt), and the exact -published Git source. Hosted artifacts retain their stated 30-day lifetime; the -recovery archive is the durable copy. +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.