Add a versioned installed proof-carrying exact-query API

.github/workflows/exact-public-api.yml

@@ -0,0 +1,163 @@
+name: exact-public-api
+on:
+  push:
+    branches: [research/exact-public-api-20261015]
+  pull_request:
+    paths:
+      - 'spectra/exact*.py'
+      - 'spectra/_native/exact_binary.cpp'
+      - 'spectra/cli.py'
+      - 'tests/public/test_exact_api.py'
+      - 'scripts/check_exact_installation.py'
+      - 'scripts/check_current_installation.py'
+      - 'docs/EXACT_API.md'
+      - '.github/workflows/exact-public-api.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: exact-public-api-${{ github.ref }}
+  cancel-in-progress: false
+jobs:
+  linux-installed:
+    name: Installed API (${{ matrix.runner }}, Python ${{ matrix.python }})
+    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 'build==1.3.0' 'pytest==9.0.2' 'python-sat==1.9.dev15'
+      - name: Build packaged source and run public plus exhaustive exact contracts
+        run: |
+          set -euo pipefail
+          mkdir -p exact-public-evidence
+          git rev-parse HEAD > exact-public-evidence/source_commit.txt
+          git rev-parse HEAD^{tree} > exact-public-evidence/source_tree.txt
+          python -VV > exact-public-evidence/python.txt
+          uname -a > exact-public-evidence/platform.txt
+          export SPECTRA_EXACT_LIBRARY="$(python -c "from spectra.exact import build_exact_runtime; print(build_exact_runtime('exact-public-evidence/source-build'))")"
+          python -m pytest tests/public/test_exact_api.py --confcutdir=tests/public -q --junitxml=exact-public-evidence/public-tests.xml 2>&1 | tee exact-public-evidence/public-tests.log
+          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=exact-public-evidence/research-tests.xml 2>&1 | tee exact-public-evidence/research-tests.log
+      - name: Build the compiler-free wheel and test its installed native API
+        run: |
+          set -euo pipefail
+          python -m build --wheel --outdir exact-public-evidence/dist 2>&1 | tee exact-public-evidence/build.log
+          python -m venv exact-public-evidence/install
+          exact-public-evidence/install/bin/python -m pip install --no-deps exact-public-evidence/dist/*.whl
+          exact-public-evidence/install/bin/python -I scripts/check_exact_installation.py --out exact-public-evidence/installed.json 2>&1 | tee exact-public-evidence/installed.log
+          python scripts/check_release_readiness.py --out exact-public-evidence/release-readiness.json
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: exact-public-${{ matrix.runner }}-py${{ matrix.python }}-${{ github.run_id }}
+          path: exact-public-evidence/
+          include-hidden-files: true
+          retention-days: 90
+          if-no-files-found: error
+  windows-installed:
+    runs-on: windows-2022
+    timeout-minutes: 20
+    env:
+      PYTHONUTF8: '1'
+    steps:
+      - run: git config --global core.autocrlf false
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.13'
+      - name: Load MSVC x64
+        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 'build==1.3.0' 'pytest==9.0.2' 'python-sat==1.9.dev15'
+      - name: Run source and installed-wheel contracts under MSVC
+        shell: pwsh
+        run: |
+          New-Item -ItemType Directory -Force exact-public-evidence | Out-Null
+          git rev-parse HEAD | Out-File exact-public-evidence/source_commit.txt
+          python -VV 2>&1 | Out-File exact-public-evidence/python.txt
+          $library = python -c "from spectra.exact import build_exact_runtime; print(build_exact_runtime('exact-public-evidence/source-build'))"
+          "SPECTRA_EXACT_LIBRARY=$library" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
+          $env:SPECTRA_EXACT_LIBRARY = $library
+          python -m pytest tests/public/test_exact_api.py --confcutdir=tests/public -q --junitxml=exact-public-evidence/public-tests.xml 2>&1 | Tee-Object exact-public-evidence/public-tests.log
+          if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE }
+          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=exact-public-evidence/research-tests.xml 2>&1 | Tee-Object exact-public-evidence/research-tests.log
+          if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE }
+          python -m build --wheel --outdir exact-public-evidence/dist 2>&1 | Tee-Object exact-public-evidence/build.log
+          if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE }
+          python -m venv exact-public-evidence/install
+          $python = 'exact-public-evidence/install/Scripts/python.exe'
+          & $python -m pip install --no-deps (Get-ChildItem exact-public-evidence/dist/*.whl).FullName
+          if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE }
+          & $python -I scripts/check_exact_installation.py --out exact-public-evidence/installed.json 2>&1 | Tee-Object exact-public-evidence/installed.log
+          if ($LASTEXITCODE -ne 0) { exit $LASTEXITCODE }
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: exact-public-windows-py3.13-${{ github.run_id }}
+          path: exact-public-evidence/
+          include-hidden-files: true
+          retention-days: 90
+          if-no-files-found: error
+  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==9.0.2' 'python-sat==1.9.dev15'
+      - name: Build packaged source and run exact API contracts under sanitizer
+        env:
+          SANITIZER: ${{ matrix.sanitizer }}
+        run: |
+          set -euo pipefail
+          mkdir -p exact-sanitizer-evidence
+          export SPECTRA_EXACT_LIBRARY="$(python -c "from spectra.exact import build_exact_runtime; import os; print(build_exact_runtime('exact-sanitizer-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 tests/public/test_exact_api.py --confcutdir=tests/public -q --junitxml=exact-sanitizer-evidence/public-tests.xml 2>&1 | tee exact-sanitizer-evidence/public-tests.log
+          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=exact-sanitizer-evidence/research-tests.xml 2>&1 | tee exact-sanitizer-evidence/research-tests.log
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: exact-public-sanitizer-${{ matrix.sanitizer }}-${{ github.run_id }}
+          path: exact-sanitizer-evidence/
+          retention-days: 90
+          if-no-files-found: error

.github/workflows/public-package.yml

@@ -1,7 +1,7 @@
 name: public-package
 on:
   pull_request:
-    branches: [main, "maintenance/**", "research/deductive-search-*", "research/focused-search-*", "research/research-engineering-*"]
+    branches: [main, "maintenance/**", "research/deductive-search-*", "research/focused-search-*", "research/research-engineering-*", "research/faster-queries-review-*"]
   workflow_dispatch:
 permissions:
   contents: read
@@ -47,6 +47,7 @@ jobs:
           python scripts/check_current_installation.py --dist .public-package/dist --out .public-package/install | tee .public-package/install.txt
           .public-package/install/venv/bin/python -I scripts/check_focused_installation.py | tee .public-package/focused-install.txt
           .public-package/install/venv/bin/python -I scripts/check_dpll_installation.py | tee .public-package/dpll-install.txt
+          .public-package/install/venv/bin/python -I scripts/check_exact_installation.py --out .public-package/exact-install.json | tee .public-package/exact-install.txt
       - name: Run and replay frozen compact-state comparison
         run: |
           set -o pipefail

CHANGELOG.md

@@ -2,6 +2,18 @@
 
 ## Unreleased
 
+### Versioned proof-carrying exact-query API
+
+- Add dependency-light `spectra.exact` API version 1 with native ABI 3.
+- Package the exact native source in compiler-free wheels; compilation remains an
+  explicit local action and publishes a source/Python/compiler/binary receipt.
+- Return complete checked SAT colourings or portable `SBP1` UNSAT proofs through
+  persistent sessions and one-call `SBC1` to `SCQ2` execution.
+- Add strict independent Python replay, `spectra exact verify`, installed-wheel
+  native execution, receipt-tamper tests and cross-platform CI contracts.
+- Do not publish a new package version or transfer exposed synthetic performance
+  evidence into the frozen WAP claim.
+
 ### Certified repeated-query compilation
 
 - Integrate SPECTRA's prospectively frozen WAP support-query result into `main`.

README.md

@@ -36,10 +36,11 @@ historical “general reasoner,” MCTS, low-bit, or neural claims.
 [Certificate reproduction](experiments/wap_support/CERTIFICATE_REPRODUCTION_20261009.md) ·
 [Replication guide](experiments/wap_support/REPLICATION.md)
 
-The separate experimental exact-query service now has
-[faster short requests, optional engine selection and Windows builds](experiments/compiled_query/QUERY_LATENCY_RESULTS_20261015.md).
-Its latest development comparison retains a failed speed target against an
-improved raw control; it does not replace the frozen WAP result above.
+The current unreleased tree also contains a
+[versioned proof-carrying exact-query API](docs/EXACT_API.md) with explicit native
+build receipts, complete SAT/UNSAT evidence, installed-wheel checks, automatic
+engine selection and Linux/Windows support. Its performance panels use exposed
+synthetic development graphs and do not replace the frozen WAP result above.
 
 **Package: Python 3.10+ · Flagship complete-call result: Python 3.13 · MIT-licensed project code · CPU-first · explicit verification boundaries**
 
@@ -171,7 +172,34 @@ Independent replication is tracked in
 [issue #55](https://github.com/tugrapaydiner/SPECTRA/issues/55). Negative or
 conflicting replications are explicitly welcome.
 
-## Exact API boundary
+## Proof-carrying exact-query API
+
+The unreleased `spectra.exact` module is an installed, explicitly versioned API for
+fixed conflict graphs whose original vertex domains contain one or two colours.
+Native compilation is explicit and receipt-bound; imports remain standard-library
+only. Every completed admitted call returns a complete checked colouring or an
+independently replayable original-literal contradiction proof.
+
+```python
+from spectra.exact import (
+    ExactProblem, ExactRuntime, build_exact_runtime,
+    pack_session_packet, verify_session_output,
+)
+
+problem = ExactProblem.create(2, 2, ((0, 1),), (0b11, 0b11))
+library = build_exact_runtime("exact-native-build")
+runtime = ExactRuntime(library)
+queries = ((), ((0, 0b01), (1, 0b01)))
+packet = pack_session_packet(problem, queries)
+result = runtime.solve_session_packet(packet, mode="auto")
+assert verify_session_output(packet, result.output)
+```
+
+The API contract, packet layouts, CLI, resource accounting and claim boundary are
+documented in [Proof-carrying exact queries](docs/EXACT_API.md). This is not a
+general SAT or colouring-superiority claim.
+
+## Quotient API boundary
 
 The experimental quotient runtime is opt-in. It does not compile during import and
 does not silently fall back to another solver.

SECURITY.md

@@ -27,11 +27,18 @@ verified source in an isolated environment. Do not expose research loaders to
 uploaded third-party files. A checksum proves identity only when the expected
 checksum itself is trusted. No loader was silently rewritten in this cleanup.
 
-Native execution compiles bundled C++ with the local compiler and uses optional
-PyTorch APIs. Historical dependency pins exist for reproducibility, not as a
-claim of current vulnerability-free support. Review dependencies separately
-before deployment; do not reinterpret an updated dependency's outputs as a
-bitwise replay of the old environment.
+Native execution compiles bundled C++ with the local compiler. Some historical
+runtimes use optional PyTorch APIs; the proof-carrying exact API does not. Its
+builder emits a receipt binding source, Python ABI, compiler command and final
+binary, and the runtime checks that receipt by default. This detects accidental
+or post-build byte changes; it does not sandbox the compiler, authenticate the
+installed package, or prove the native code safe. Build only trusted source with
+a trusted toolchain.
+
+Historical dependency pins exist for reproducibility, not as a claim of current
+vulnerability-free support. Review dependencies separately before deployment; do
+not reinterpret an updated dependency's outputs as a bitwise replay of the old
+environment. Prepared-packet byte admission is not a total RSS or wall-time bound.
 
 ## Reporting
 

docs/API.md

@@ -52,6 +52,26 @@ pool and break/age move policy. This classical candidate has a retained fresh
 synthetic evaluation and independent witness checks. See [focused search](FOCUSED_GUIDE.md)
 for its measured scope, budget semantics and recovery limitations.
 
+## Proof-carrying exact queries
+
+The unreleased `spectra.exact` module supplies an explicit native build, immutable
+original-address problems, persistent sessions, prepared `SBC1` sessions, full
+`SCQ2` answer banks and independent standard-library proof replay. The public API
+version is 1 and the native ABI is 3. Ordinary import never compiles code.
+
+```python
+from spectra.exact import ExactProblem, ExactRuntime, build_exact_runtime
+
+problem = ExactProblem.create(2, 2, ((0, 1),), (3, 3))
+runtime = ExactRuntime(build_exact_runtime("exact-build"))
+with runtime.prepare(problem) as session:
+    answer = session.solve(((0, 1), (1, 1)))
+    assert answer.status == "UNSAT_VERIFIED"
+```
+
+See [Proof-carrying exact-query API](EXACT_API.md) for packet layouts, receipt
+validation, CLI replay, resource limits and the narrow claim boundary.
+
 ## Commands and exit codes
 
 ```bash

docs/DEVELOPMENT.md

@@ -30,7 +30,7 @@ python scripts/audit_workspace.py --out .release-check/workspace.json
 
 The default `python -m build` builds an sdist, then builds the wheel from that
 sdist. The installation check creates a separate virtual environment, installs
-without dependencies, and runs **11 installed-only checks outside the checkout**.
+without dependencies, and runs installed-only checks outside the checkout.
 It verifies the command, APIs and packaged native source inventory. It does not
 substitute an editable install for a wheel test. The public-package CI performs
 the same path; the indexed-efficiency workflow also checks Python 3.10 and 3.13.
@@ -66,8 +66,26 @@ With PyTorch, Ninja and a suitable compiler installed,
 An explicit binary build can use `SPECTRA_BUILD_NATIVE=1` with
 `pip wheel --no-build-isolation .`; compilation failure is an error.
 Ordinary wheels include sources for the existing JIT loaders without compiling
-during installation. Native checks are separate from the dependency-free wheel
-checks. Cross-host bitwise equality is not a blanket runtime guarantee.
+during installation. The proof-carrying exact runtime is built independently of
+PyTorch:
+
+```bash
+python -m spectra exact build exact-native-build
+python -m pytest tests/public/test_exact_api.py
+```
+
+To verify the actual installed wheel rather than the checkout, run the normal
+installation check and then use its isolated interpreter:
+
+```bash
+.release-check/install/venv/bin/python -I scripts/check_exact_installation.py \
+  --out .release-check/install/exact.json
+```
+
+On Windows use `Scripts\python.exe` from a configured MSVC x64 environment.
+Native checks are separate from dependency-free wheel checks. Build receipts bind
+source and binary identity but do not make cross-host bitwise equality a blanket
+runtime guarantee.
 
 ## Reproduce systems comparisons