diff --git a/.github/workflows/exact-public-api.yml b/.github/workflows/exact-public-api.yml new file mode 100644 index 0000000..198e52f --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/.github/workflows/public-package.yml b/.github/workflows/public-package.yml index 405c360..4efdf81 100644 --- a/.github/workflows/public-package.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index 7792183..8274cd6 100644 --- a/CHANGELOG.md +++ b/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`. diff --git a/README.md b/README.md index a90e23c..9a67972 100644 --- a/README.md +++ b/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. diff --git a/SECURITY.md b/SECURITY.md index cf83f66..67a3daf 100644 --- a/SECURITY.md +++ b/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 diff --git a/docs/API.md b/docs/API.md index 14e9eeb..d518c00 100644 --- a/docs/API.md +++ b/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 diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md index 9b9f4d5..207f1d2 100644 --- a/docs/DEVELOPMENT.md +++ b/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 diff --git a/docs/EXACT_API.md b/docs/EXACT_API.md new file mode 100644 index 0000000..cafb0dc --- /dev/null +++ b/docs/EXACT_API.md @@ -0,0 +1,168 @@ +# Proof-carrying exact-query API + +The current unreleased source tree exposes a versioned, installable API for exact +queries over a fixed simple conflict graph when every original vertex has one or +two allowed colours. It is available as `spectra.exact`. + +This API is separate from bounded CNF search and from the older quotient runtime. +Every completed call returns either a complete original-vertex colouring or a +portable original-literal contradiction proof. There is no `UNKNOWN` outcome for +an admitted completed call, no silent fallback solver, and no compilation during +module import. + +## Contract versions + +| Layer | Version | Role | +|---|---:|---| +| Public Python API | `EXACT_API_VERSION = 1` | names, validation and result objects | +| Native extension ABI | `EXACT_NATIVE_ABI = 3` | CPython extension entry points | +| Query bank | `SBQ1` | immutable current restrictions for a prepared graph | +| Full session packet | `SBC1` | immutable graph, domains and request bank | +| Certified answer bank | `SCQ2` | full SAT labels or complete UNSAT proof per row | +| Contradiction proof | `SBP1` | original-literal paths checked without solver state | + +The Python package version remains `0.7.1` until an actual package release is +made. The exact API version is its explicit contract version; source availability +on a branch is not a PyPI release. + +## Explicit native build + +Ordinary wheels remain compiler-free. Building the exact runtime is an explicit +local operation and requires GIL-enabled CPython plus a supported C++ compiler. +Linux uses `g++`; Windows x64 uses a configured MSVC developer environment. + +```python +from pathlib import Path +from spectra.exact import build_exact_runtime, ExactRuntime + +library = build_exact_runtime(Path("exact-native-build")) +runtime = ExactRuntime(library) +``` + +The builder publishes the extension only with an adjacent `build.json`. The +receipt binds the packaged C++ source hash, compiler command and version, Python +implementation and SOABI, API/ABI versions, and final binary hash. `ExactRuntime` +checks this receipt by default before loading executable code. Loading a separately +managed trusted extension without a receipt requires the explicit +`verify_receipt=False` override. + +The receipt proves local identity, not compiler trust, source provenance beyond +the installed package, sandboxing, or absence of vulnerabilities. + +## Original-address problem and persistent session + +```python +from spectra.exact import ExactProblem, verify_answer + +problem = ExactProblem.create( + n=4, + palette=3, + edges=((0, 1), (1, 2), (2, 3)), + masks=(0b011, 0b110, 0b101, 0b011), +) + +with runtime.prepare(problem, mode="scc") as session: + query = ((0, 0b001), (3, 0b010)) + answer = session.solve(query) + assert answer.status in {"SAT_VERIFIED", "UNSAT_VERIFIED"} + assert session.check(query, answer) + assert verify_answer( + problem, query, answer.status, answer.labels, answer.proof + ) +``` + +`ExactProblem.create` owns immutable, canonical inputs. Edges are converted to +sorted unique `(left, right)` pairs. Each domain mask must contain exactly one or +two colours from a palette of at most 64 colours. + +Persistent modes are `raw`, `scc`, `sparse`, and `route`. They share the same +answer contract. `route` changes proof reconstruction, not the mathematical +problem. Persistent sessions own a solver and a separately constructed observer; +closing is idempotent, and subsequent use fails closed. + +## One-call prepared session + +`SBC1` is the deployment-oriented input form. It contains the complete fixed graph, +original domains, and request bank. The solver and observer each parse the bytes +independently. One call constructs both owners, answers every request, checks every +witness or proof, serializes `SCQ2`, and disposes native state. + +```python +from spectra.exact import pack_session_packet, verify_session_output + +queries = ( + (), + ((0, 0b001),), + ((0, 0b001), (1, 0b001)), +) +packet = pack_session_packet(problem, queries) +result = runtime.solve_session_packet(packet, mode="auto") +assert result.query_count == len(queries) +assert verify_session_output(packet, result.output) +``` + +The opt-in `auto` mode uses only graph structure and request-bank length. It does +not inspect measured timings or cached answers. The result metadata names the +selected engine. Explicit modes retain their meaning. + +`pack_session_packet` accepts ordinary Python inputs. `pack_validated_session_packet` +is for already admitted immutable inputs and still rechecks exact types, bounds, +edge ordering and query geometry. The strict decoder rejects reversed, duplicate, +unsorted, truncated, overlong, or reserved-bit-modified packets rather than +repairing them. + +## Independent replay and CLI + +`verify_answer`, `verify_certified_output`, and `verify_session_output` use only +standard-library Python and original inputs. They do not load the native extension, +receive SCC identifiers, or trust the solver's previous decision. + +```bash +spectra exact verify request.sbc1 answer.scq2 +``` + +The command defaults to a 64 MiB limit for each input file and returns exit code +`0` for a fully verified bank, `1` for well-formed evidence that fails semantic +verification, and `2` for malformed input, I/O errors, or invalid settings. + +An explicit build is also available: + +```bash +spectra exact build exact-native-build +``` + +No command downloads a compiler or dependency. + +## Resource and performance boundary + +`max_bytes` is a conservative admission bound for native owners, scratch arrays, +proof envelopes, serialized output and the final immutable Python bytes copy. It +is not a total process-RSS limit, hard deadline, Python-object bound, or protection +against an untrusted compiler. Use operating-system process limits for hostile or +multi-tenant workloads. + +Ready-`SBC1` timings begin after packet preparation. They include packet parsing and +hashing, native construction, solving, complete witnesses/proofs, independent +native checking, `SCQ2` construction, disposal, and output hashing. They exclude +JSON decoding, packet creation, compilation, process startup and offline Python +replay. Do not present them as first-use application latency. + +The current performance evidence uses exposed synthetic development graphs and is +not an independent application benchmark. The installed API does not inherit the +frozen WAP result, create a general SAT claim, or establish algorithmic novelty. + +## Tested boundary + +The API contracts require: + +- byte equality between the packaged and research native source in the repository; +- strict packet and output decoders; +- SAT and UNSAT proof replay from original inputs; +- build-receipt tamper rejection; +- persistent and one-call native execution; +- installed-wheel operation outside the checkout; +- Linux x86 and ARM64 builds, Windows x64/MSVC builds, and sanitizer checks in the + dedicated workflow. + +See [Security](../SECURITY.md), [Development](DEVELOPMENT.md), and the exact-query +research reports under `experiments/compiled_query/` for evidence and limitations. diff --git a/docs/README.md b/docs/README.md index 132090e..f11fd18 100644 --- a/docs/README.md +++ b/docs/README.md @@ -23,6 +23,7 @@ historical neural, MCTS, low-bit, general-SAT, or universal CPU-performance clai |---|---| | Install and run the public tools | [Quick start](../README.md#base-toolkit-quick-start) | | Understand API, input formats and return values | [API and CLI](API.md) | +| Build and use checked SAT/UNSAT exact queries | [Proof-carrying exact API](EXACT_API.md) | | Check released, merged, experimental and failed work | [Current status](STATUS.md) | | Run tests, build a wheel or reproduce experiments | [Development](DEVELOPMENT.md) | | Prepare a package release | [Release checklist](RELEASING.md) | diff --git a/docs/RELEASING.md b/docs/RELEASING.md index d11a5ce..d8a87e0 100644 --- a/docs/RELEASING.md +++ b/docs/RELEASING.md @@ -21,10 +21,14 @@ never upload changed bytes under an already published version. Run the complete [development test/build procedure](DEVELOPMENT.md), including public contracts, fast research regressions, a wheel built from the sdist, -11 installed-only checks, navigation/version checks and the history-based +installed-only checks, navigation/version checks and the history-based workspace audit. Retain exact commands, exit statuses, environments and logs. Native execution and historical evidence replays are additional checks, not -implied by successful wheel installation. Report excluded slow tests explicitly. +implied by successful wheel installation. A release containing `spectra.exact` +must also pass the installed-wheel exact check on the final wheel, verify its +packaged C++ source inventory, compile under the supported Linux and Windows +builders, and retain the ABI/API/build-receipt results. Report excluded slow tests +and disabled leak detection explicitly. ```bash python scripts/check_release_readiness.py diff --git a/docs/STATUS.md b/docs/STATUS.md index 23a4860..d7af2a0 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -13,6 +13,12 @@ source. A source checkout is therefore not byte-identical to the v0.7.1 wheel. No new package, PyPI publication, or replacement release asset is implied by the WAP research merge. +The current unreleased source additionally contains `spectra.exact` API version 1 +(native ABI 3). It packages the proof-carrying exact-query source and verifies an +explicit local build from an installed wheel. This source availability is not a +v0.8 release, and the exact-query development measurements remain separate from +the confirmed WAP endpoint. + ## Flagship research result SPECTRA's principal result is the certified original-address quotient for repeated diff --git a/scripts/check_current_installation.py b/scripts/check_current_installation.py index c0986e7..e73d0eb 100644 --- a/scripts/check_current_installation.py +++ b/scripts/check_current_installation.py @@ -21,6 +21,7 @@ REQUIRED_SOURCES = { "spectra/_native/blocked_linear.cpp", "spectra/_native/fp_step.cpp", + "spectra/_native/exact_binary.cpp", "deploy/m10_dense_extension.cpp", "deploy/replay_ordered_extension.cpp", "deploy/cpp_sparse_kernel/extension.cpp", "deploy/cpp_sparse_kernel/spectra_kernel.cpp", } diff --git a/scripts/check_exact_installation.py b/scripts/check_exact_installation.py new file mode 100644 index 0000000..9827c09 --- /dev/null +++ b/scripts/check_exact_installation.py @@ -0,0 +1,98 @@ +"""Build and exercise the proof-carrying exact API from an installed wheel. + +Run with the installation venv's Python and ``-I`` so repository packages cannot +satisfy imports. Native compilation is explicit and uses the host compiler. +""" +from __future__ import annotations + +import argparse +import importlib.util +import json +import os +from pathlib import Path +import sys +import tempfile + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def main(argv=None): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path) + args = parser.parse_args(argv) + output = args.out.resolve() if args.out is not None else None + previous = Path.cwd() + # A loaded extension module remains locked until process exit on Windows. + # The temporary build is disposable, so defer that platform's final removal + # to the runner/OS rather than converting a completed API check into failure. + with tempfile.TemporaryDirectory( + prefix='spectra-exact-installed-', + ignore_cleanup_errors=(os.name == 'nt')) as temporary: + root = Path(temporary) + try: + os.chdir(root) + import spectra.exact as exact + + module_path = Path(exact.__file__).resolve() + source_path = exact.SOURCE.resolve() + prefix = Path(sys.prefix).resolve() + require(module_path.is_relative_to(prefix), + 'exact API must come from installed wheel') + require(source_path.is_relative_to(prefix) and source_path.is_file(), + 'installed wheel must include exact native source') + for dependency in ('torch', 'numpy', 'pytest', 'pysat'): + require(importlib.util.find_spec(dependency) is None, + 'unexpected optional dependency: ' + dependency) + require(importlib.util.find_spec('experiments') is None, + 'installed contract must not import repository experiments') + + library = exact.build_exact_runtime(root / 'native') + runtime = exact.ExactRuntime(library) + problem = exact.ExactProblem.create(2, 2, ((0, 1),), (3, 3)) + queries = ((), ((0, 1),), ((0, 1), (1, 1))) + packet = exact.pack_session_packet(problem, queries) + result = runtime.solve_session_packet(packet, mode='auto') + require( + (result.query_count, result.sat_count, result.unsat_count) == (3, 2, 1), + 'unexpected installed exact decisions', + ) + require(exact.verify_session_output(packet, result.output), + 'independent installed replay rejected output') + rows = exact.decode_certified_output( + result.output, problem.n, len(queries)) + require(tuple(code for code, _, _ in rows) == (1, 1, 0), + 'unexpected installed SCQ2 rows') + receipt = json.loads(library.with_name('build.json').read_text()) + require(receipt['exact_api_version'] == exact.EXACT_API_VERSION == 1, + 'exact API version differs') + require(receipt['native_abi'] == exact.EXACT_NATIVE_ABI == 3, + 'native ABI differs') + report = { + 'status': 'PASS', + 'scope': 'actual installed wheel; isolated Python; explicit native build', + 'module': str(module_path), + 'source': str(source_path), + 'exact_api_version': exact.EXACT_API_VERSION, + 'native_abi': exact.EXACT_NATIVE_ABI, + 'queries': result.query_count, + 'sat': result.sat_count, + 'unsat': result.unsat_count, + 'selected_mode': result.info['selected_mode'], + 'optional_dependencies': False, + 'receipt_source_sha256': receipt['source_sha256'], + 'receipt_library_sha256': receipt['library_sha256'], + } + text = json.dumps(report, indent=2, sort_keys=True) + '\n' + if output is not None: + output.parent.mkdir(parents=True, exist_ok=True) + output.write_text(text, encoding='utf-8') + print(text, end='') + finally: + os.chdir(previous) + + +if __name__ == '__main__': + main() diff --git a/spectra/_native/exact_binary.cpp b/spectra/_native/exact_binary.cpp new file mode 100644 index 0000000..96182ee --- /dev/null +++ b/spectra/_native/exact_binary.cpp @@ -0,0 +1,1086 @@ +// Exact binary-list support with original-literal contradiction paths. +// MIT: repository LICENSE. Established 2-SAT/SCC/implication closure, not novelty. +#define PY_SSIZE_T_CLEAN +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#if defined(_MSC_VER) +#include +#endif + +namespace { +using U = uint32_t; +using W = uint64_t; +constexpr U NIL = UINT32_MAX, MAX_N = 100000, MAX_E = 2000000, MAX_P = 1000000; +constexpr const char* SOLVER = "spectra.exact_binary.solver.v3"; +constexpr const char* OBSERVER = "spectra.exact_binary.observer.v3"; +struct Invalid : std::runtime_error { using std::runtime_error::runtime_error; }; +struct Resource : std::runtime_error { using std::runtime_error::runtime_error; }; +W number(PyObject* value, const char* message, W cap = UINT64_MAX) { + if (!PyLong_CheckExact(value)) throw Invalid(message); + W n = PyLong_AsUnsignedLongLong(value); + if (PyErr_Occurred()) { PyErr_Clear(); throw Invalid(message); } + if (n > cap) throw Invalid(message); + return n; +} +void tuple(PyObject* value, const char* message) { + if (!PyTuple_CheckExact(value)) throw Invalid(message); +} +W palette(U k) { return k == 64 ? UINT64_MAX : ((W(1) << k) - 1); } +#if defined(_MSC_VER) +U first(W v) { unsigned long index=0;_BitScanForward64(&index,v);return static_cast(index); } +// Do not require POPCNT on the Windows portable build. +U bits(W v) { U count=0;while(v) {v&=v-1;++count;}return count; } +#else +U first(W v) { return static_cast(__builtin_ctzll(v)); } +U bits(W v) { return static_cast(__builtin_popcountll(v)); } +#endif +struct Pin { U vertex; W allowed; }; +std::vector read_query(PyObject* q, U n, W cap) { + tuple(q, "queries require exact tuples"); + W size = static_cast(PyTuple_GET_SIZE(q)); + if (size > MAX_P || 32*size + 64*W(n+1) + 4096 > cap) + throw Resource("query scratch/pin admission exceeds cap"); + std::vector pins; pins.reserve(size); + for (Py_ssize_t i=0; i=n) throw Invalid("pin vertex outside graph"); + pins.push_back({static_cast(v),allowed}); + } + return pins; // every row is checked, including after an earlier contradiction +} +struct Input { + U n,k; W cap; + std::vector masks; + std::vector> edges; + Input(U nv,U kv,std::vector> es,std::vector ms,W limit) + :n(nv),k(kv),cap(limit),masks(std::move(ms)),edges(std::move(es)) {} + Input(PyObject* nv, PyObject* kv, PyObject* es, PyObject* ms, W limit):cap(limit) { + n=static_cast(number(nv,"n outside supported bound",MAX_N)); + k=static_cast(number(kv,"palette outside [1,64]",64)); + if (!k) throw Invalid("palette outside [1,64]"); + tuple(es,"edges require exact tuples"); tuple(ms,"masks require exact tuples"); + if (PyTuple_GET_SIZE(ms)!=n) throw Invalid("mask count differs"); + W m=static_cast(PyTuple_GET_SIZE(es)); + if (m>MAX_E || 768*W(n+1)+384*(m+1)+8192>cap) + throw Resource("conservative construction payload admission exceeds cap"); + masks.reserve(n); + for (U v=0;v2) + throw Invalid("original domains require one or two palette colours"); + masks.push_back(d); + } + edges.reserve(m); + for (Py_ssize_t i=0;i=n || v>=n || u==v) throw Invalid("edge needs distinct in-range vertices"); + edges.emplace_back(std::min(u,v),std::max(u,v)); + } + std::sort(edges.begin(),edges.end()); + edges.erase(std::unique(edges.begin(),edges.end()),edges.end()); + } +}; +struct CSR { + std::vector off, to; + CSR()=default; + CSR(U n, const std::vector>& arcs, bool reverse=false):off(n+1,0),to(arcs.size()) { + for(auto e:arcs) ++off[(reverse?e.second:e.first)+1]; + for(U v=0;v components(const CSR& g,const CSR& r) { + U n=static_cast(g.off.size()-1); + std::vector seen(n,0); + std::vector order; order.reserve(n); + std::vector> stack; stack.reserve(n); + for(U root=0;root comp(n,NIL), todo; todo.reserve(n); U id=0; + for(auto it=order.rbegin();it!=order.rend();++it) if(comp[*it]==NIL) { + comp[*it]=id;todo.push_back(*it); + while(!todo.empty()) {U v=todo.back();todo.pop_back(); + for(U j=r.off[v];j& out,U x) {for(U j=0;j<4;++j) out.push_back(static_cast(x>>(8*j)));} +void qword(std::vector& out,W x) {for(U j=0;j<8;++j) out.push_back(static_cast(x>>(8*j)));} +U load32(const uint8_t* data,size_t at) {U x=0;for(U j=0;j<4;++j)x|=U(data[at+j])<<(8*j);return x;} +W load64(const uint8_t* data,size_t at) {W x=0;for(U j=0;j<8;++j)x|=W(data[at+j])<<(8*j);return x;} +std::vector proof(U kind,const std::vector& a,const std::vector& b) { + std::vector out;out.reserve(16+4*(a.size()+b.size())); + out.insert(out.end(),{'S','B','P','1'}); word(out,kind);word(out,static_cast(a.size()));word(out,static_cast(b.size())); + for(U v:a) word(out,v); + for(U v:b) word(out,v); + return out; +} +std::vector trace(const std::vector& parent,U v) { + std::vector path; + while(true) {path.push_back(v);if(parent[v]==v) break; + if(parent[v]==NIL || path.size()>parent.size()) throw std::logic_error("invalid parent chain"); + v=parent[v]; + } + std::reverse(path.begin(),path.end());return path; +} + +// SBQ1 solver-side parser. It owns no Python objects and borrows immutable bytes +// only for one native call. The observer has a separately written parser below, +// so a shared offset bug cannot silently validate its own output. +struct SolverBank { + const uint8_t* data;size_t size;U count,pins;size_t offsets_at=16,vertices_at,masks_at; + SolverBank(const uint8_t* bytes,size_t length,U n):data(bytes),size(length),count(0),pins(0),vertices_at(0),masks_at(0) { + if(size<20 || std::memcmp(data,"SBQ1",4)) throw Invalid("invalid SBQ1 solver packet"); + count=load32(data,4);pins=load32(data,8); + if(load32(data,12)!=0 || count>MAX_P || pins>MAX_P) throw Invalid("invalid SBQ1 solver header"); + W expected=20+4*W(count)+12*W(pins); + if(expected!=size) throw Invalid("SBQ1 solver length differs"); + vertices_at=20+4*W(count);masks_at=vertices_at+4*W(pins); + U previous=load32(data,offsets_at); + if(previous!=0) throw Invalid("SBQ1 solver offsets must start at zero"); + for(U i=1;i<=count;++i) { + U next=load32(data,offsets_at+4*W(i)); + if(nextpins) throw Invalid("SBQ1 solver offsets differ"); + previous=next; + } + if(previous!=pins) throw Invalid("SBQ1 solver offsets do not consume pins"); + for(U i=0;i=n) + throw Invalid("SBQ1 solver vertex outside graph"); + } + U begin(U row) const {return load32(data,offsets_at+4*W(row));} + U end(U row) const {return load32(data,offsets_at+4*W(row+1));} + U query_count() const {return count;} + U pin_count() const {return pins;} + std::vector row(U index) const { + U first_pin=begin(index),last_pin=end(index);std::vector result;result.reserve(last_pin-first_pin); + for(U i=first_pin;iMAX_P || total>MAX_P) + throw Invalid("invalid SBQ1 observer header"); + W geometry=16+4*W(rows+1)+12*W(total); + if(geometry!=bytes) throw Invalid("SBQ1 observer geometry differs"); + vertices=16+4*W(rows+1);masks=vertices+4*W(total); + U at=0; + for(U i=0;i<=rows;++i) { + U next=load32(payload,table+4*W(i)); + if((i==0 && next!=0) || nexttotal) + throw Invalid("SBQ1 observer offsets differ"); + at=next; + } + if(at!=total) throw Invalid("SBQ1 observer pin bank is not consumed"); + for(U i=0;i=n) + throw Invalid("SBQ1 observer vertex outside graph"); + } + std::vector row(U index) const { + U begin=load32(payload,table+4*W(index)); + U finish=load32(payload,table+4*W(index+1)); + std::vector result;result.reserve(finish-begin); + for(U i=begin;i original_masks; + std::vector> original_edges; + SolverSessionPacket(const uint8_t* bytes,size_t length,W cap):data(bytes),size(length), + n(0),k(0),edge_count(0),count(0),pins(0),edges_at(0),offsets_at(0),vertices_at(0),allowed_at(0) { + if(size<36 || std::memcmp(data,"SBC1",4)) throw Invalid("invalid SBC1 solver packet"); + n=load32(data,4);k=load32(data,8);edge_count=load32(data,12); + count=load32(data,16);pins=load32(data,20); + if(n>MAX_N || !k || k>64 || edge_count>MAX_E || count>MAX_P || pins>MAX_P + || load32(data,24)!=0 || load32(data,28)!=0) + throw Invalid("invalid SBC1 solver header"); + W expected=36+8*W(n)+8*W(edge_count)+4*W(count)+12*W(pins); + if(expected!=size) throw Invalid("SBC1 solver length differs"); + W construction=768*W(n+1)+384*W(edge_count+1)+8192; + if(construction>cap || W(size)>cap-construction) + throw Resource("SBC1 solver construction admission exceeds cap"); + edges_at=masks_at+8*W(n);offsets_at=edges_at+8*W(edge_count); + vertices_at=offsets_at+4*W(count+1);allowed_at=vertices_at+4*W(pins); + original_masks.reserve(n); + for(U v=0;v2) + throw Invalid("SBC1 solver original domain differs"); + original_masks.push_back(domain); + } + original_edges.reserve(edge_count);U previous_left=0,previous_right=0;bool have_previous=false; + for(U i=0;i=right || right>=n || (have_previous && (leftpins) throw Invalid("SBC1 solver offsets differ"); + previous=next; + } + if(previous!=pins) throw Invalid("SBC1 solver offsets do not consume pins"); + for(U i=0;i=n) + throw Invalid("SBC1 solver query vertex outside graph"); + } + U query_count() const {return count;} + U pin_count() const {return pins;} + std::vector row(U index) const { + U begin=load32(data,offsets_at+4*W(index)),end=load32(data,offsets_at+4*W(index+1)); + std::vector result;result.reserve(end-begin); + for(U i=begin;i domains; + std::vector> edges; + ObserverSessionPacket(const uint8_t* source,size_t length,W cap):payload(source),bytes(length), + vertices_count(0),palette_size(0),edges_count(0),rows(0),total(0),edge_table(0),offset_table(0),vertex_table(0),mask_table(0) { + if(bytes<36 || payload[0]!='S' || payload[1]!='B' || payload[2]!='C' || payload[3]!='1') + throw Invalid("invalid SBC1 observer packet"); + vertices_count=load32(payload,4);palette_size=load32(payload,8);edges_count=load32(payload,12); + rows=load32(payload,16);total=load32(payload,20); + if(vertices_count>MAX_N || palette_size<1 || palette_size>64 || edges_count>MAX_E + || rows>MAX_P || total>MAX_P || load32(payload,24) || load32(payload,28)) + throw Invalid("invalid SBC1 observer header"); + W geometry=32+8*W(vertices_count)+8*W(edges_count)+4*W(rows+1)+12*W(total); + if(geometry!=bytes) throw Invalid("SBC1 observer geometry differs"); + W construction=768*W(vertices_count+1)+384*W(edges_count+1)+8192; + if(construction>cap || W(bytes)>cap-construction) + throw Resource("SBC1 observer construction admission exceeds cap"); + edge_table=domain_table+8*W(vertices_count);offset_table=edge_table+8*W(edges_count); + vertex_table=offset_table+4*W(rows+1);mask_table=vertex_table+4*W(total); + domains.reserve(vertices_count); + for(U v=0;v2) + throw Invalid("SBC1 observer original domain differs"); + domains.push_back(domain); + } + edges.reserve(edges_count);U last_left=0,last_right=0;bool have=false; + for(U i=0;ilast_left || (left==last_left && right>last_right); + if(left>=right || right>=vertices_count || !ordered) + throw Invalid("SBC1 observer edge bank differs"); + edges.emplace_back(left,right);last_left=left;last_right=right;have=true; + } + U consumed=0; + for(U i=0;i<=rows;++i) { + U next=load32(payload,offset_table+4*W(i)); + if((i==0 && next!=0) || nexttotal) + throw Invalid("SBC1 observer offsets differ"); + consumed=next; + } + if(consumed!=total) throw Invalid("SBC1 observer pin bank is not consumed"); + for(U i=0;i=vertices_count) + throw Invalid("SBC1 observer query vertex outside graph"); + } + U query_count() const {return rows;} + U pin_count() const {return total;} + std::vector row(U index) const { + U begin=load32(payload,offset_table+4*W(index)),end=load32(payload,offset_table+4*W(index+1)); + std::vector result;result.reserve(end-begin); + for(U i=begin;i labels,certificate;W visits=0,arcs=0;}; +struct Index { + U n,k,nc=0,bad=NIL;bool condensed,sparse,routed;W cap;W full_arcs=0; + std::vector masks; + std::vector lo,hi,base; + std::vector comp,opposite; + std::vector inward,outward,representative,cross_from,cross_to; + CSR original,dag; + Index(Input p,U mode,U bank_size=0):n(p.n),k(p.k),condensed(mode!=0),sparse(mode==2),routed(mode==3),cap(p.cap),masks(std::move(p.masks)),lo(n),hi(n,255),base(n) { + std::vector> arcs;arcs.reserve(4*p.edges.size()+n); + for(U v=0;v(comp[2*v]=64 && bad==NIL; + routed=condensed && nc<=n; + } + if(condensed && bad==NIL) { + opposite.assign(nc,NIL); + for(U v=0;v<2*n;++v) { + U a=comp[v],b=comp[v^1U]; + if(a==b || (opposite[a]!=NIL && opposite[a]!=b)) throw std::logic_error("complement mapping differs"); + opposite[a]=b; + } + // Routed mode builds the same ordered DAG from its original-edge + // bridges below. Sorting both the links and bridges repeats work. + if(!routed) { + std::vector> links;links.reserve(arcs.size()); + for(auto e:arcs) if(comp[e.first]!=comp[e.second]) links.emplace_back(comp[e.first],comp[e.second]); + std::sort(links.begin(),links.end());links.erase(std::unique(links.begin(),links.end()),links.end()); + dag=CSR(nc,links); + } + } else if(!condensed) {std::vector().swap(comp);} + if(sparse || routed) { + if(routed) { + inward.assign(2*n,NIL);outward.assign(2*n,NIL); + representative.assign(nc,NIL); + for(U v=0;v<2*n;++v) if(representative[comp[v]]==NIL) representative[comp[v]]=v; + } + // Reachability-preserving original-edge subgraph: inward/outward + // trees in each SCC plus one original arc per condensation edge. + // Full original graph remains separately owned by the verifier. + std::vector> keep; + if(sparse) keep.reserve(std::min(full_arcs,4*W(n)+dag.to.size())); + std::vector seen(2*n,0); + std::vector queue;queue.reserve(2*n); + for(U direction=0;direction<2;++direction) { + std::fill(seen.begin(),seen.end(),0); + const CSR& g=direction?reverse:original; + for(U root=0;root<2*n;++root) if(!seen[root]) { + queue.clear();queue.push_back(root);seen[root]=1; + if(routed) (direction?inward:outward)[root]=root; + for(size_t head=0;head> bridges;bridges.reserve(arcs.size()); + for(auto e:arcs) if(comp[e.first]!=comp[e.second]) + bridges.emplace_back(comp[e.first],comp[e.second],e.first,e.second); + std::sort(bridges.begin(),bridges.end()); + std::vector> routed_links; + if(routed && bad==NIL) routed_links.reserve(bridges.size()); + U previous_a=NIL,previous_b=NIL; + for(auto e:bridges) {U a=std::get<0>(e),b=std::get<1>(e); + if(a!=previous_a || b!=previous_b) { + if(sparse) keep.emplace_back(std::get<2>(e),std::get<3>(e)); + if(routed && bad==NIL) { + routed_links.emplace_back(a,b); + cross_from.push_back(std::get<2>(e));cross_to.push_back(std::get<3>(e)); + } + previous_a=a;previous_b=b; + } + } + std::sort(keep.begin(),keep.end());keep.erase(std::unique(keep.begin(),keep.end()),keep.end()); + if(keep.size()>arcs.size()) throw std::logic_error("proof subgraph grew beyond original"); + if(routed) { + if(bad==NIL) dag=CSR(nc,routed_links); + if(cross_from.size()!=dag.to.size()) throw std::logic_error("routing bridge geometry differs"); + for(U c=0;c within(U from,U target,Answer& answer) const { + if(from==target) return {from}; + if(comp[from]!=comp[target]) throw std::logic_error("intra-component routing crosses SCCs"); + std::vector tail; + for(U v=target;;v=outward[v]) { + tail.push_back(v); + if(outward[v]==v) break; + if(tail.size()>2*W(n) || outward[v]==NIL) throw std::logic_error("invalid outward routing tree"); + ++answer.arcs; + } + // Join at the first inward vertex on the outward root-to-target path. + // This removes tree-overlap cycles without a graph search or n-sized + // scratch. Sorted membership avoids a hash-table worst-case assumption. + auto membership=tail;std::sort(membership.begin(),membership.end()); + std::vector result; + U meeting=NIL; + for(U v=from;;v=inward[v]) { + result.push_back(v); + if(std::binary_search(membership.begin(),membership.end(),v)) {meeting=v;break;} + if(result.size()>2*W(n) || inward[v]==NIL || inward[v]==v) + throw std::logic_error("routing trees do not meet"); + ++answer.arcs; + } + size_t at=static_cast(std::find(tail.begin(),tail.end(),meeting)-tail.begin()); + while(at) result.push_back(tail[--at]); + return result; + } + std::vector lift(U target,const std::vector& parent,const std::vector& edge, + const std::vector& seed,Answer& answer) const { + U c=comp[target];std::vector chain; + while(parent[c]!=c) { + if(parent[c]==NIL || edge[c]==NIL || chain.size()>=nc) + throw std::logic_error("routing predecessor chain missing"); + chain.push_back(edge[c]);c=parent[c]; + } + U current=seed[c];if(current==NIL) throw std::logic_error("current request root missing"); + std::vector result{current}; + for(auto it=chain.rbegin();it!=chain.rend();++it) { + auto segment=within(current,cross_from[*it],answer); + result.insert(result.end(),segment.begin()+1,segment.end()); + current=cross_to[*it];result.push_back(current);++answer.arcs; + } + auto segment=within(current,target,answer); + result.insert(result.end(),segment.begin()+1,segment.end()); + if(result.size()>2*W(n)) throw std::logic_error("lifted proof exceeds simple-path bound"); + return result; + } + std::vector path(U from,U target,Answer& a) const { + if(routed) return within(from,target,a); + std::vector parent(2*n,NIL),queue;queue.reserve(2*n);parent[from]=from;queue.push_back(from); + for(size_t head=0;head& seeds,std::vector& parent,Answer& a) const { + if(routed) throw std::logic_error("routed proofs must not invoke original-graph search"); + parent.assign(2*n,NIL);std::vector queue;queue.reserve(2*n);U conflict=NIL; + for(U v:seeds) if(parent[v]==NIL) {parent[v]=v;queue.push_back(v); + if(parent[v^1U]!=NIL) {conflict=v;break;}} + for(size_t head=0;conflict==NIL && head& pins, + const std::vector* known_base_proof=nullptr) const { + Answer answer; + // Give every exact mode the same sparse request preparation, including + // the cheap raw control. All pins were validated before this function. + auto restrictions=pins; + std::sort(restrictions.begin(),restrictions.end(),[](Pin a,Pin b){return a.vertex seeds;seeds.reserve(std::min(pins.size(),n)); + for(size_t i=0;iempty()) { + answer.certificate=*known_base_proof;return answer; + } + auto a=path(2*bad,2*bad+1,answer),b=path(2*bad+1,2*bad,answer); + answer.certificate=proof(3,a,b);return answer; + } + return solve_roots(seeds); + } + // Roots belong to this request only. The caller has already intersected + // every restriction and ruled out empty domains and a fixed contradiction. + Answer solve_roots(const std::vector& seeds) const { + Answer answer; + std::vector parent; + std::vector reached; + if(condensed) { + reached.assign(nc,0);std::vector queue;queue.reserve(nc);U conflict=NIL; + std::vector route_parent,route_edge,route_seed; + if(routed) {route_parent.assign(nc,NIL);route_edge.assign(nc,NIL);route_seed.assign(nc,NIL);} + for(U v:seeds) {U c=comp[v];if(!reached[c]) { + reached[c]=1;queue.push_back(c); + if(routed) {route_parent[c]=c;route_seed[c]=v;} + if(reached[opposite[c]]) {conflict=c;break;} + }} + for(size_t head=0;conflict==NIL && head seen;U epoch=0; + U next(U literals) { + if(seen.size()!=literals) {seen.assign(literals,0);epoch=0;} + if(epoch==UINT32_MAX) {std::fill(seen.begin(),seen.end(),0);epoch=0;} + return ++epoch; + } +}; +struct Observer { + U n,k;W cap; + std::vector masks; + std::vector> edges,conflicts; + std::vector colors; + explicit Observer(Input p):n(p.n),k(p.k),cap(p.cap),masks(std::move(p.masks)),edges(std::move(p.edges)),colors(2*n,255) { + for(U v=0;v>c)&1) colors[2*v+side++]=static_cast(c);} + // Independently derive exactly the original equal-colour conflicts. The + // observer never receives the solver's implication graph or SCC index. + conflicts.reserve(2*edges.size()); + for(auto edge:edges) { + W shared=masks[edge.first]&masks[edge.second]; + while(shared) { + U color=first(shared);shared&=shared-1; + U left=2*edge.first+(colors[2*edge.first]!=color); + U right=2*edge.second+(colors[2*edge.second]!=color); + conflicts.emplace_back(left,right); + } + } + // Each admitted original edge is unique; each shared colour creates + // one distinct forbidden literal pair. Verification scans every pair, + // so neither sorting nor duplicate elimination is needed here. Keep + // the independently owned original edges sorted for proof-hop lookup. + } + W bytes() const {return 8*W(masks.capacity()+edges.capacity()+conflicts.capacity())+colors.capacity();} + bool hop(U a,U b) const { + U u=a/2,v=b/2; + if(u==v) return (a%2)==1 && (b%2)==0 && bits(masks[u])==1; + if(colors[a]==255 || colors[b^1U]==255 || colors[a]!=colors[b^1U]) return false; + return std::binary_search(edges.begin(),edges.end(),std::make_pair(std::min(u,v),std::max(u,v))); + } + bool verify(const std::vector& pins,U status,const uint8_t* labels,size_t len,const uint8_t* data,size_t size, + ProofScratch* scratch=nullptr) const { + if(status==1) { + if(len!=n || size) return false; + for(U v=0;v=k || !((masks[v]>>labels[v])&1)) return false; + for(auto pair:conflicts) + if(labels[pair.first/2]==colors[pair.first] + && labels[pair.second/2]==colors[pair.second]) return false; + for(auto p:pins) if(!((p.allowed>>labels[p.vertex])&1)) return false; + return true; + } + if(status!=0 || len || size<16 || std::memcmp(data,"SBP1",4)) return false; + auto get=[data](size_t at)->U {U value=0;for(U j=0;j<4;++j) value|=U(data[at+j])<<(8*j);return value;}; + U kind=get(4), na=get(8),nb=get(12); + if(W(16)+4*(W(na)+nb)!=size || na>2*W(n)+1 || nb>2*W(n)) return false; + // Proof checks need only the cited original root domains, not an + // n-element domain copy. Pin validation is still complete and unsampled. + auto effective=[&](U vertex) {W d=masks[vertex];for(auto pin:pins) if(pin.vertex==vertex) d&=pin.allowed;return d;}; + if(kind==1) return na==1 && nb==0 && get(16)2*W(n)) return false; + // Read bounded paths directly from the serialized certificate. A fresh + // generation checks simplicity for each path; the backing array can be + // reused within this call without retaining any validation result. + ProofScratch local;auto& work=scratch?*scratch:local; + auto path_ok=[&](size_t offset,U count) { + U stamp=work.next(2*n),previous=NIL; + for(U i=0;i=2*n || work.seen[literal]==stamp) return false; + work.seen[literal]=stamp; + if(i && !hop(previous,literal)) return false; + previous=literal; + } + return true; + }; + if(!path_ok(16,na) || !path_ok(16+4*W(na),nb)) return false; + U a_first=get(16),a_last=get(16+4*W(na-1)); + U b_first=get(16+4*W(na)),b_last=get(16+4*(W(na)+nb-1)); + if(kind==3) return a_first==b_last && a_last==b_first && a_last==(a_first^1U); + auto forced=[&](U literal) {return colors[literal]!=255 && effective(literal/2)==(W(1)< + bool verify_bank(const Bank& bank,const uint8_t* output,size_t size) const { + U rows=bank.query_count(); + if(size<16 || std::memcmp(output,"SCQ2",4) || load32(output,4)!=n || load64(output,8)!=rows) + return false; + size_t at=16; + std::vector selected(n,0); + ProofScratch proof_scratch; // call-local, also for concurrent observer use + for(U first_row=0;first_row(64,rows-first_row);W sat_mask=0; + std::fill(selected.begin(),selected.end(),0); + for(U lane=0;lanesize) return false; + U status=output[at];const uint8_t* labels=output+at+1; + U length=load32(output,at+1+W(n));at+=W(n)+5; + if(W(length)>size-at) return false; + auto pins=bank.row(first_row+lane); + if(status==1) { + if(length) return false; + W bit=W(1)<>labels[pin.vertex])&1)) return false; + } else if(status==0) { + for(U v=0;v output; + W visits=0,arcs=0,proof_bytes=0; + U sat=0,unsat=0,tiles=0; + bool tiled=false; +}; +template +BankResult run_rows(Index& solver,Observer& observer,const SolverRows& solver_rows, + const ObserverRows& observer_rows,size_t packet_size,W total_cap, + const char* schema) { + if(solver.n!=observer.n || solver.k!=observer.k) + throw Invalid("solver and observer geometry differs"); + U count=solver_rows.query_count(),pins=solver_rows.pin_count(); + if(count!=observer_rows.query_count() || pins!=observer_rows.pin_count()) + throw std::logic_error("independent request parsers disagree"); + W retained=solver.bytes()+observer.bytes(); + W per_row=25+17*W(solver.n); + W output_bound=16+per_row*W(count); + // Covers parsed request copies, up to 64 complete answers, bit-lane state, + // proof replay scratch, vector metadata, and output serialization. Python + // inputs and allocator metadata remain outside this conservative native cap. + // Two output envelopes cover vector reallocation and the immutable Python + // bytes handoff while the native vector is still alive. Not an RSS limit. + W scratch=2048*W(solver.n+1)+64*W(pins)+64*W(count)+8192; + if(retained>total_cap || W(packet_size)>total_cap-retained + || output_bound>(total_cap-retained-W(packet_size))/2 + || scratch>total_cap-retained-W(packet_size)-2*output_bound) + throw Resource("combined exact bank solve/verify/output admission exceeds cap"); + BankResult result; + W initial=16+W(count)*(W(solver.n)+25); + if(initial>std::numeric_limits::max()) + throw Resource("exact bank output reserve exceeds platform size"); + result.output.reserve(static_cast(initial)); + result.output.insert(result.output.end(),{'S','C','Q','2'});word(result.output,solver.n);qword(result.output,count); + + auto reserve_row=[&](size_t proof_size) { + W row_bytes=5+W(solver.n)+proof_size; + if(row_bytes>output_bound-result.output.size()) + throw Resource("SCQ2 output exceeds admitted bound"); + W required=result.output.size()+row_bytes; + if(required>result.output.capacity()) { + // Bound capacity explicitly instead of relying on vector growth. + W grown=std::min(output_bound,std::max(required,2*W(result.output.capacity()))); + result.output.reserve(static_cast(grown)); + } + }; + auto append=[&](const Answer& answer) { + reserve_row(answer.certificate.size()); + result.visits+=answer.visits;result.arcs+=answer.arcs; + result.output.push_back(answer.sat?1:0); + if(answer.sat) { + if(answer.labels.size()!=solver.n || !answer.certificate.empty()) + throw std::logic_error("SAT bank row geometry differs"); + result.output.insert(result.output.end(),answer.labels.begin(),answer.labels.end());++result.sat; + } else { + if(!answer.labels.empty() || answer.certificate.size()>UINT32_MAX) + throw std::logic_error("UNSAT bank row geometry differs"); + result.output.resize(result.output.size()+solver.n,0);++result.unsat; + } + word(result.output,static_cast(answer.certificate.size())); + result.output.insert(result.output.end(),answer.certificate.begin(),answer.certificate.end()); + result.proof_bytes+=answer.certificate.size(); + if(W(result.output.size())>output_bound) + throw Resource("SCQ2 output exceeds admitted bound"); + }; + + // The quotient component IDs are topological. For sufficiently large banks, + // propagate 64 independent requests as bits through the same DAG traversal. + // Contradiction certificates are still reconstructed by the ordinary exact + // solver per UNSAT lane, so proof semantics and independent checking remain + // unchanged. This is a batching optimization, not a new satisfiability rule. + const bool use_tiles=solver.condensed && solver.bad==NIL && count>=64; + if(use_tiles) { + result.tiled=true; + for(U first_row=0;first_row(64,count-first_row); + std::vector> roots(lanes); + std::vector empty(lanes,NIL),conflict(lanes,NIL); + std::vector reached(solver.nc,0); + for(U lane=0;lane(restrictions.size(),solver.n)); + for(size_t i=0;i high_choices; + if(sat_lanes) { + high_choices.resize(solver.n); + for(U v=0;v parent; + solver.raw_closure(roots[lane],parent,answer); + } + if(answer.sat) + throw std::logic_error("bit-lane contradiction did not replay"); + } else { + // Write directly into the admitted SCQ2 row. Its four-byte + // proof length stays zero; no temporary label vector/copy. + reserve_row(0); + size_t at=result.output.size(); + result.output.resize(at+W(solver.n)+5,0); + result.output[at]=1;++result.sat; + W bit=W(1)< base_proof; + for(U row=0;row=16 + && load32(answer.certificate.data(),4)==3) + base_proof=answer.certificate; + append(answer); + } + } + if(!observer.verify_bank(observer_rows,result.output.data(),result.output.size())) + throw std::logic_error(std::string("serialized ")+schema+" bank failed independent observer"); + return result; +} +BankResult run_bank(Index& solver,Observer& observer,const uint8_t* data,size_t size) { + SolverBank solver_bank(data,size,solver.n); + ObserverBank observer_bank(data,size,observer.n); + W observer_bytes=observer.bytes(); + W total_cap=solver.cap>UINT64_MAX-observer_bytes?UINT64_MAX:solver.cap+observer_bytes; + return run_rows(solver,observer,solver_bank,observer_bank,size,total_cap,"SBQ1"); +} +PyObject* exception() { + try {throw;} catch(const Invalid& e){PyErr_SetString(PyExc_ValueError,e.what());} + catch(const Resource& e){PyErr_SetString(PyExc_MemoryError,e.what());} + catch(const std::bad_alloc&){PyErr_NoMemory();} + catch(const std::exception& e){PyErr_SetString(PyExc_RuntimeError,e.what());} + catch(...){PyErr_SetString(PyExc_RuntimeError,"unknown native failure");} + return nullptr; +} +void destroy_index(PyObject* c){delete static_cast(PyCapsule_GetPointer(c,SOLVER));} +void destroy_observer(PyObject* c){delete static_cast(PyCapsule_GetPointer(c,OBSERVER));} +template T* handle(PyObject* p,const char* tag) {auto* t=static_cast(PyCapsule_GetPointer(p,tag));if(!t){PyErr_Clear();throw Invalid("invalid exact-service handle");}return t;} +PyObject* create(PyObject*,PyObject* args) { + PyObject *nv,*kv,*es,*ms,*mode,*cap; + if(!PyArg_ParseTuple(args,"OOOOOO",&nv,&kv,&es,&ms,&mode,&cap)) return nullptr; + try {W limit=number(cap,"invalid memory payload cap"),which=number(mode,"mode must be 0, 1, 2 or 3",3); + Input input(nv,kv,es,ms,limit);std::unique_ptr result; + {Released guard;result=std::make_unique(std::move(input),static_cast(which));} + PyObject* capsule=PyCapsule_New(result.get(),SOLVER,destroy_index);if(capsule) result.release(); + return capsule; + }catch(...){return exception();} +} +PyObject* observer_create(PyObject*,PyObject* args) { + PyObject *nv,*kv,*es,*ms,*cap; + if(!PyArg_ParseTuple(args,"OOOOO",&nv,&kv,&es,&ms,&cap)) return nullptr; + try {Input input(nv,kv,es,ms,number(cap,"invalid memory payload cap")); + auto result=std::make_unique(std::move(input));PyObject* capsule=PyCapsule_New(result.get(),OBSERVER,destroy_observer); + if(capsule) result.release(); + return capsule; + }catch(...){return exception();} +} +PyObject* solve(PyObject*,PyObject* args) { + PyObject *h,*q; + if(!PyArg_ParseTuple(args,"OO",&h,&q)) return nullptr; + try {auto* x=handle(h,SOLVER);auto pins=read_query(q,x->n,x->cap);Answer a; + {Released guard;a=x->solve(pins);} + PyObject* labels=PyBytes_FromStringAndSize(reinterpret_cast(a.labels.data()),static_cast(a.labels.size())); + if(!labels) return nullptr; + PyObject* cert=PyBytes_FromStringAndSize(reinterpret_cast(a.certificate.data()),static_cast(a.certificate.size())); + if(!cert){Py_DECREF(labels);return nullptr;} + return Py_BuildValue("iNNKK",a.sat?1:0,labels,cert,static_cast(a.visits),static_cast(a.arcs)); + }catch(...){return exception();} +} +PyObject* solve_bank(PyObject*,PyObject* args) { + PyObject *solver_handle,*observer_handle,*packet; + if(!PyArg_ParseTuple(args,"OOO",&solver_handle,&observer_handle,&packet)) return nullptr; + try { + auto* solver=handle(solver_handle,SOLVER);auto* observer=handle(observer_handle,OBSERVER); + if(!PyBytes_CheckExact(packet)) throw Invalid("query bank must be immutable exact bytes"); + const auto* data=reinterpret_cast(PyBytes_AS_STRING(packet)); + size_t size=static_cast(PyBytes_GET_SIZE(packet));BankResult result; + {Released guard;result=run_bank(*solver,*observer,data,size);} + PyObject* output=PyBytes_FromStringAndSize(reinterpret_cast(result.output.data()), + static_cast(result.output.size())); + if(!output) return nullptr; + return Py_BuildValue("NKKKKKK",output, + static_cast(result.sat+result.unsat), + static_cast(result.sat), + static_cast(result.unsat), + static_cast(result.proof_bytes), + static_cast(result.visits), + static_cast(result.arcs)); + }catch(...){return exception();} +} +PyObject* solve_session_packet(PyObject*,PyObject* args) { + PyObject *packet,*mode,*cap; + if(!PyArg_ParseTuple(args,"OOO",&packet,&mode,&cap)) return nullptr; + try { + if(!PyBytes_CheckExact(packet)) throw Invalid("session packet must be immutable exact bytes"); + W which=number(mode,"mode must be 0, 1, 2, 3 or 4",4); + W limit=number(cap,"invalid memory payload cap"); + if(limit<(1U<<20)) throw Invalid("memory payload cap must be at least 1 MiB"); + const auto* data=reinterpret_cast(PyBytes_AS_STRING(packet)); + size_t size=static_cast(PyBytes_GET_SIZE(packet)); + std::unique_ptr solver;std::unique_ptr observer;BankResult result; + { + Released guard; + ObserverSessionPacket observer_rows(data,size,limit); + observer=std::make_unique(observer_rows.take_input(limit)); + W observer_bytes=observer->bytes(); + if(observer_bytes>=limit) throw Resource("SBC1 observer consumes session cap"); + SolverSessionPacket solver_rows(data,size,limit-observer_bytes); + solver=std::make_unique(solver_rows.take_input(limit-observer_bytes), + static_cast(which),solver_rows.query_count()); + result=run_rows(*solver,*observer,solver_rows,observer_rows,size,limit,"SBC1"); + } + PyObject* output=PyBytes_FromStringAndSize(reinterpret_cast(result.output.data()), + static_cast(result.output.size())); + if(!output) return nullptr; + PyObject* metadata=Py_BuildValue("{sI,sI,sK,sK,sK,sK,sK,sK,sO,sO,ss}", + "vertices",solver->n,"components",solver->nc, + "original_arcs",static_cast(solver->full_arcs), + "retained_proof_arcs",static_cast(solver->original.to.size()), + "condensation_arcs",static_cast(solver->dag.to.size()), + "retained_array_bytes",static_cast(solver->bytes()), + "routing_array_bytes",static_cast(solver->routing_bytes()), + "native_observer_array_bytes",static_cast(observer->bytes()), + "original_adjacency_retained",solver->routed?Py_False:Py_True, + "base_satisfiable",solver->bad==NIL?Py_True:Py_False, + "selected_mode",solver->routed?"route":(solver->sparse?"sparse":(solver->condensed?"scc":"raw"))); + if(!metadata){Py_DECREF(output);return nullptr;} + PyObject* kernel=PyUnicode_FromString(result.tiled?"tile64":"serial"); + PyObject* tiles=PyLong_FromUnsignedLong(result.tiles); + if(!kernel || !tiles || PyDict_SetItemString(metadata,"bank_kernel",kernel)<0 + || PyDict_SetItemString(metadata,"bank_tiles",tiles)<0) { + Py_XDECREF(kernel);Py_XDECREF(tiles);Py_DECREF(output);Py_DECREF(metadata);return nullptr; + } + Py_DECREF(kernel);Py_DECREF(tiles); + return Py_BuildValue("NKKKKKKN",output, + static_cast(result.sat+result.unsat), + static_cast(result.sat), + static_cast(result.unsat), + static_cast(result.proof_bytes), + static_cast(result.visits), + static_cast(result.arcs),metadata); + }catch(...){return exception();} +} +PyObject* verify(PyObject*,PyObject* args) { + PyObject *h,*q,*status,*labels,*proof_bytes; + if(!PyArg_ParseTuple(args,"OOOOO",&h,&q,&status,&labels,&proof_bytes)) return nullptr; + try {auto* o=handle(h,OBSERVER);auto pins=read_query(q,o->n,o->cap); + if(!PyBytes_CheckExact(labels)||!PyBytes_CheckExact(proof_bytes)||!PyLong_CheckExact(status)) Py_RETURN_FALSE; + W code=number(status,"bad decision",1); + const auto* l=reinterpret_cast(PyBytes_AS_STRING(labels)); + const auto* p=reinterpret_cast(PyBytes_AS_STRING(proof_bytes)); + size_t nl=PyBytes_GET_SIZE(labels),np=PyBytes_GET_SIZE(proof_bytes);bool ok; + {Released guard;ok=o->verify(pins,static_cast(code),l,nl,p,np);} + return PyBool_FromLong(ok); + }catch(...){return exception();} +} +PyObject* check_bank(PyObject*,PyObject* args) { + PyObject *observer_handle,*packet,*output; + if(!PyArg_ParseTuple(args,"OOO",&observer_handle,&packet,&output)) return nullptr; + try { + auto* observer=handle(observer_handle,OBSERVER); + if(!PyBytes_CheckExact(packet) || !PyBytes_CheckExact(output)) Py_RETURN_FALSE; + const auto* request_data=reinterpret_cast(PyBytes_AS_STRING(packet)); + const auto* answer_data=reinterpret_cast(PyBytes_AS_STRING(output)); + size_t request_size=static_cast(PyBytes_GET_SIZE(packet)); + size_t answer_size=static_cast(PyBytes_GET_SIZE(output));bool ok; + {Released guard;ObserverBank bank(request_data,request_size,observer->n); + ok=observer->verify_bank(bank,answer_data,answer_size);} + return PyBool_FromLong(ok); + }catch(...){return exception();} +} +PyObject* info(PyObject*,PyObject* h) { + try {auto* x=handle(h,SOLVER); + return Py_BuildValue("{sI,sI,sK,sK,sK,sK,sK,sO,sO}","vertices",x->n,"components",x->nc, + "original_arcs",static_cast(x->full_arcs), + "retained_proof_arcs",static_cast(x->original.to.size()), + "condensation_arcs",static_cast(x->dag.to.size()), + "retained_array_bytes",static_cast(x->bytes()), + "routing_array_bytes",static_cast(x->routing_bytes()), + "original_adjacency_retained",x->routed?Py_False:Py_True, + "base_satisfiable",x->bad==NIL?Py_True:Py_False); + }catch(...){return exception();} +} +PyObject* observer_bytes(PyObject*,PyObject* h) {try{return PyLong_FromUnsignedLongLong(handle(h,OBSERVER)->bytes());}catch(...){return exception();}} +PyObject* abi(PyObject*,PyObject*){return PyLong_FromLong(3);} +PyMethodDef methods[]={ + {"create",create,METH_VARARGS,nullptr},{"observer_create",observer_create,METH_VARARGS,nullptr}, + {"solve",solve,METH_VARARGS,nullptr},{"solve_bank",solve_bank,METH_VARARGS,nullptr}, + {"solve_session_packet",solve_session_packet,METH_VARARGS,nullptr}, + {"verify",verify,METH_VARARGS,nullptr},{"check_bank",check_bank,METH_VARARGS,nullptr}, + {"info",info,METH_O,nullptr},{"observer_bytes",observer_bytes,METH_O,nullptr}, + {"abi",abi,METH_NOARGS,nullptr},{nullptr,nullptr,0,nullptr}}; +PyModuleDef module={PyModuleDef_HEAD_INIT,"_spectra_exact_binary",nullptr,-1,methods,nullptr,nullptr,nullptr,nullptr}; +} +PyMODINIT_FUNC PyInit__spectra_exact_binary(){return PyModule_Create(&module);} diff --git a/spectra/cli.py b/spectra/cli.py index aa8f2e6..9b430c9 100644 --- a/spectra/cli.py +++ b/spectra/cli.py @@ -9,6 +9,18 @@ from . import __version__ from ._json import DEFAULT_MAX_BYTES, load_file +EXACT_FILE_MAX_BYTES = 64 << 20 + + +def _read_binary(path: Path, *, max_bytes: int) -> bytes: + if type(max_bytes) is not int or not 1 <= max_bytes <= sys.maxsize - 1: + raise ValueError("max-bytes must be a positive bounded integer") + with path.open("rb") as stream: + data = stream.read(max_bytes + 1) + if len(data) > max_bytes: + raise ValueError(f"{path} exceeds max-bytes") + return data + def _emit(value: dict, destination: Path | None) -> None: text = json.dumps(value, indent=2, sort_keys=True, allow_nan=False) + "\n" @@ -38,6 +50,15 @@ def main(argv: list[str] | None = None) -> int: check_parser = actions.add_parser("check", help="Check a complete Boolean witness against original clauses") check_parser.add_argument("input", type=Path) check_parser.add_argument("witness", type=Path, help="JSON object with a Boolean-list witness field") + exact = commands.add_parser("exact", help="Proof-carrying exact binary-domain tools") + exact_actions = exact.add_subparsers(dest="action", required=True) + exact_build = exact_actions.add_parser("build", help="Explicitly compile the bundled ABI-3 native runtime") + exact_build.add_argument("directory", type=Path) + exact_build.add_argument("--compiler") + exact_verify = exact_actions.add_parser("verify", help="Replay an SBC1 -> SCQ2 result without native code") + exact_verify.add_argument("packet", type=Path) + exact_verify.add_argument("output", type=Path) + exact_verify.add_argument("--max-bytes", type=int, default=EXACT_FILE_MAX_BYTES) evidence = commands.add_parser("evidence", help="Verify a portable hash/size manifest, not scientific validity") evidence.add_argument("root", type=Path) evidence.add_argument("manifest", type=Path) @@ -50,12 +71,41 @@ def main(argv: list[str] | None = None) -> int: from .svm_stream import execute _emit(execute(args), None) elif args.command == "doctor": + from .exact import EXACT_API_VERSION, EXACT_NATIVE_ABI, SOURCE as EXACT_SOURCE _emit({"version": __version__, "python": platform.python_version(), "torch_installed": importlib.util.find_spec("torch") is not None, - "cnf_requires_torch": False}, None) + "cnf_requires_torch": False, + "exact_api_version": EXACT_API_VERSION, + "exact_native_abi": EXACT_NATIVE_ABI, + "exact_source_packaged": EXACT_SOURCE.is_file()}, None) elif args.command == "evidence": from .evidence import verify _emit(verify(args.root, load_file(args.manifest, max_bytes=args.max_json_bytes)), None) + elif args.command == "exact": + from .exact import (EXACT_API_VERSION, EXACT_NATIVE_ABI, build_exact_runtime, + decode_certified_output, unpack_session_packet, + verify_session_output) + if args.action == "build": + library = build_exact_runtime(args.directory, compiler=args.compiler) + record = json.loads(library.with_name("build.json").read_text(encoding="utf-8")) + _emit({"status": "BUILT", "library": str(library), + "build_receipt": str(library.with_name("build.json")), + "exact_api_version": EXACT_API_VERSION, + "native_abi": EXACT_NATIVE_ABI, + "source_sha256": record["source_sha256"], + "library_sha256": record["library_sha256"]}, None) + else: + packet = _read_binary(args.packet, max_bytes=args.max_bytes) + output = _read_binary(args.output, max_bytes=args.max_bytes) + problem, rows = unpack_session_packet(packet) + decoded = decode_certified_output(output, problem.n, len(rows)) + verified = verify_session_output(packet, output) + _emit({"verified": verified, "queries": len(decoded), + "sat": sum(code == 1 for code, _, _ in decoded), + "unsat": sum(code == 0 for code, _, _ in decoded), + "exact_api_version": EXACT_API_VERSION, + "native_abi": EXACT_NATIVE_ABI}, None) + return 0 if verified else 1 else: from .cnf import read_dimacs, solve, solve_indexed, solve_deductive, solve_focused with args.input.open(encoding="utf-8") as stream: @@ -79,7 +129,7 @@ def main(argv: list[str] | None = None) -> int: _emit({"valid": not violated, "unsatisfied": list(violated), "formula_sha256": problem.sha256()}, None) return 0 if not violated else 1 - except (OSError, ValueError, TypeError) as error: + except (OSError, ValueError, TypeError, RuntimeError, NotImplementedError) as error: print(f"spectra: {error}", file=sys.stderr) return 2 return 0 diff --git a/spectra/exact.py b/spectra/exact.py new file mode 100644 index 0000000..983d335 --- /dev/null +++ b/spectra/exact.py @@ -0,0 +1,613 @@ +"""Versioned proof-carrying exact queries for fixed binary-domain graphs. + +The public API is dependency-light and explicit: native compilation never occurs on +import, there is no fallback solver, and every completed answer is independently +checked against the original graph, domains, and current restrictions. +""" +from __future__ import annotations + +from dataclasses import dataclass +import hashlib +import importlib.util +import json +import os +from pathlib import Path +import platform +import shutil +import struct +import subprocess +import sys +import sysconfig +import tempfile +import threading +import time +from typing import Iterable, Sequence + +from .exact_problem import ExactProblem +from .exact_proof import decode_proof, verify_answer + +SOURCE = Path(__file__).with_name('_native') / 'exact_binary.cpp' +EXACT_API_VERSION = 1 +EXACT_NATIVE_ABI = 3 +DEFAULT_BYTES = 512 << 20 +MAX_BYTES = (1 << 64) - 1 +QUERY_BANK_HEADER = struct.Struct('<4sIII') +QUERY_BANK_MAGIC = b'SBQ1' +SESSION_PACKET_HEADER = struct.Struct('<4s7I') +SESSION_PACKET_MAGIC = b'SBC1' + + +def build_exact_runtime(directory: Path, *, compiler: str | None = None, + sanitizer: str = 'none') -> Path: + """Build on Linux or Windows x64; bind source, flags, Python ABI and binary. + + Windows needs a configured MSVC x64 developer prompt and CPython import + libraries. Sanitizer builds remain Linux-only. No compiler is installed here. + """ + windows = sys.platform == 'win32' + if sys.platform not in ('linux', 'win32'): + raise NotImplementedError('native builder supports Linux and Windows x64') + if sys.implementation.name != 'cpython' or sysconfig.get_config_var('Py_GIL_DISABLED'): + raise ValueError('GIL-enabled CPython is required') + if sanitizer not in ('none', 'undefined', 'address,undefined'): + raise ValueError('unsupported sanitizer') + if windows and sanitizer != 'none': + raise ValueError('sanitizer builds currently require Linux') + compiler = compiler or ('cl' if windows else 'g++') + cc = shutil.which(compiler) + if cc is None: + raise FileNotFoundError(compiler) + dest = Path(directory).resolve() + dest.mkdir(parents=True, exist_ok=True) + library = dest / ('_spectra_exact_binary' + sysconfig.get_config_var('EXT_SUFFIX')) + receipt = dest / 'build.json' + if library.exists() or receipt.exists(): + raise FileExistsError('build outputs already exist') + flags = ['-std=c++17', '-shared', '-fPIC', '-Wall', '-Wextra', '-Werror', + '-fno-fast-math', '-ffp-contract=off'] + flags += ['-O3', '-DNDEBUG'] if sanitizer == 'none' else [ + '-O1', '-g', '-fno-omit-frame-pointer', '-fsanitize=' + sanitizer, + '-fno-sanitize-recover=all'] + start = time.perf_counter_ns() + with tempfile.TemporaryDirectory(dir=dest) as tmp: + target = Path(tmp) / library.name + if windows: + from spectra.svm_build import command_for + if sysconfig.get_config_var('Py_DEBUG'): + raise ValueError('Windows debug Python is not supported') + name = f'python{sys.version_info.major}{sys.version_info.minor}.lib' + import_library = Path(sys.base_prefix) / 'libs' / name + if not import_library.is_file(): + raise ValueError('CPython import library missing: ' + str(import_library)) + command = command_for(SOURCE.resolve(), target, target='portable', compiler=cc, + include=Path(sysconfig.get_path('include')), import_library=import_library) + else: + command = [cc, *flags, '-I' + sysconfig.get_path('include'), str(SOURCE), '-o', str(target)] + result = subprocess.run(command, cwd=tmp, capture_output=True, text=True, + encoding='utf-8', errors='replace', timeout=120) + if result.returncode: + raise RuntimeError(result.stdout + result.stderr) + version = subprocess.run([cc] if windows else [cc, '--version'], + capture_output=True, text=True, encoding='utf-8', errors='replace', check=not windows) + record = dict(exact_api_version=EXACT_API_VERSION, native_abi=EXACT_NATIVE_ABI, + library_name=library.name, python_executable=sys.executable, python_version=sys.version, + python_implementation=platform.python_implementation(), + soabi=sysconfig.get_config_var('SOABI'), platform=platform.platform(), + source_sha256=hashlib.sha256(SOURCE.read_bytes()).hexdigest(), + library_sha256=hashlib.sha256(target.read_bytes()).hexdigest(), + command=command, sanitizer=sanitizer, + elapsed_ns=time.perf_counter_ns()-start, + compiler=version.stdout + version.stderr, + stdout=result.stdout, stderr=result.stderr) + os.link(target, library) + try: + with receipt.open('x') as stream: + json.dump(record, stream, sort_keys=True, indent=2) + stream.write('\n') + except BaseException: + # Never leave a newly published library with a missing/partial receipt. + library.unlink(missing_ok=True) + receipt.unlink(missing_ok=True) + raise + return library + + +@dataclass(frozen=True) +class ExactAnswer: + status: str + labels: bytes + proof: bytes + visited: int + arcs_scanned: int + + +@dataclass(frozen=True) +class ExactBankAnswer: + """One already-serialized, independently checked SCQ2 answer bank.""" + + output: bytes + query_count: int + sat_count: int + unsat_count: int + proof_bytes: int + visited: int + arcs_scanned: int + + +@dataclass(frozen=True) +class ExactSessionPacketAnswer(ExactBankAnswer): + """One-shot prepared-input result including native construction metadata.""" + + info: dict + + +def _checked_query_rows(n: int, rows: Iterable[tuple[tuple[int, int], ...]] + ) -> tuple[tuple[tuple[int, int], ...], ...]: + if type(n) is not int or not 0 <= n <= 1_000_000: + raise ValueError('n must be an exact bounded nonnegative integer') + checked = [] + for row in rows: + if type(row) is not tuple: + raise ValueError('frozen query rows must be exact tuples') + copied = [] + for pin in row: + if type(pin) is not tuple or len(pin) != 2: + raise ValueError('frozen query pins must be exact pairs') + vertex, allowed = pin + if (type(vertex) is not int or not 0 <= vertex < n or + type(allowed) is not int or not 0 <= allowed < 1 << 64): + raise ValueError('invalid frozen query pin') + copied.append((vertex, allowed)) + checked.append(tuple(copied)) + return tuple(checked) + + +def pack_query_bank(problem: ExactProblem, + queries: Iterable[Iterable[Sequence[int]]]) -> bytes: + """Freeze and serialize current requests without consulting any solver. + + ``SBQ1`` is problem-independent except for original-vertex bounds. The native + solver and observer each parse and validate the immutable byte string + independently. Packing is real endpoint work and must be charged when an + ordinary Python request bank is the advertised input. + """ + p = ExactProblem.create(problem.n, problem.palette, + problem.edges, problem.masks) + rows = tuple(p.freeze_query(query) for query in queries) + return pack_frozen_query_bank(p.n, rows) + + +def pack_frozen_query_bank(n: int, + rows: Iterable[tuple[tuple[int, int], ...]]) -> bytes: + """Serialize already-frozen rows while independently rechecking pin syntax. + + This avoids rebuilding and sorting the fixed graph after :class:`Case` has + already admitted it. It does not trust query contents: exact tuple geometry, + integer types, uint64 masks, and original-vertex bounds are checked again. + """ + rows = _checked_query_rows(n, rows) + if len(rows) > 1_000_000: + raise ValueError('query bank exceeds one million rows') + pins = sum(map(len, rows)) + if pins > 1_000_000: + raise ValueError('query bank exceeds one million pins') + size = QUERY_BANK_HEADER.size + 4 * (len(rows) + 1) + 12 * pins + payload = bytearray(size) + QUERY_BANK_HEADER.pack_into(payload, 0, QUERY_BANK_MAGIC, len(rows), pins, 0) + offset_at = QUERY_BANK_HEADER.size + vertex_at = offset_at + 4 * (len(rows) + 1) + mask_at = vertex_at + 4 * pins + cursor = 0 + struct.pack_into(' bytes: + """Validate ordinary inputs and create one immutable prepared session packet.""" + p = ExactProblem.create(problem.n, problem.palette, + problem.edges, problem.masks) + rows = tuple(p.freeze_query(query) for query in queries) + return pack_validated_session_packet(p, rows) + + +def pack_validated_session_packet(problem: ExactProblem, + rows: Iterable[tuple[tuple[int, int], ...]]) -> bytes: + """Serialize a previously admitted problem and frozen request bank. + + The graph is still scanned for exact types, sorted uniqueness and bounds, but + it is not copied and re-sorted. This function is intended for study-freeze or + deployment preparation; its cost is outside a ready-packet endpoint and must + be reported separately. + """ + n, palette_value = problem.n, problem.palette + if type(n) is not int or not 0 <= n <= 100_000: + raise ValueError('session packet n outside native bound') + if type(palette_value) is not int or not 1 <= palette_value <= 64: + raise ValueError('session packet palette outside [1, 64]') + if type(problem.masks) is not tuple or len(problem.masks) != n: + raise ValueError('session packet masks differ') + palette_mask = (1 << palette_value) - 1 if palette_value < 64 else (1 << 64) - 1 + for mask in problem.masks: + if (type(mask) is not int or mask <= 0 or mask & ~palette_mask or + mask.bit_count() not in (1, 2)): + raise ValueError('session packet original domain differs') + if type(problem.edges) is not tuple or len(problem.edges) > 2_000_000: + raise ValueError('session packet edge bank differs') + previous = None + for edge in problem.edges: + if (type(edge) is not tuple or len(edge) != 2 or + any(type(v) is not int for v in edge) or + not 0 <= edge[0] < edge[1] < n or + (previous is not None and edge <= previous)): + raise ValueError('session packet edges must be sorted unique pairs') + previous = edge + rows = _checked_query_rows(n, rows) + pins = sum(map(len, rows)) + if len(rows) > 1_000_000 or pins > 1_000_000: + raise ValueError('session packet query bank exceeds supported bound') + edge_count = len(problem.edges) + size = (SESSION_PACKET_HEADER.size + 8 * n + 8 * edge_count + + 4 * (len(rows) + 1) + 12 * pins) + payload = bytearray(size) + SESSION_PACKET_HEADER.pack_into(payload, 0, SESSION_PACKET_MAGIC, n, + palette_value, edge_count, len(rows), pins, 0, 0) + masks_at = SESSION_PACKET_HEADER.size + edges_at = masks_at + 8 * n + offsets_at = edges_at + 8 * edge_count + vertices_at = offsets_at + 4 * (len(rows) + 1) + allowed_at = vertices_at + 4 * pins + for index, mask in enumerate(problem.masks): + struct.pack_into(' tuple[ExactProblem, + tuple[tuple[tuple[int, int], ...], ...]]: + """Strict, slow Python reference decoder for tests and artifact inspection.""" + if type(payload) is not bytes or len(payload) < SESSION_PACKET_HEADER.size + 4: + raise ValueError('invalid session packet') + magic, n, palette_value, edge_count, count, pins, reserved0, reserved1 = \ + SESSION_PACKET_HEADER.unpack_from(payload) + expected = (SESSION_PACKET_HEADER.size + 8 * n + 8 * edge_count + + 4 * (count + 1) + 12 * pins) + if (magic != SESSION_PACKET_MAGIC or reserved0 or reserved1 or expected != len(payload) + or n > 100_000 or edge_count > 2_000_000 or count > 1_000_000 or pins > 1_000_000): + raise ValueError('session packet header or geometry differs') + masks_at = SESSION_PACKET_HEADER.size + edges_at = masks_at + 8 * n + offsets_at = edges_at + 8 * edge_count + vertices_at = offsets_at + 4 * (count + 1) + allowed_at = vertices_at + 4 * pins + masks = struct.unpack_from('<' + 'Q' * n, payload, masks_at) if n else () + edges = tuple(struct.unpack_from('= right for left, right in zip(edges, edges[1:])): + raise ValueError('session packet edges must be sorted unique pairs') + problem = ExactProblem.create(n, palette_value, edges, masks) + offsets = struct.unpack_from('<' + 'I' * (count + 1), payload, offsets_at) + if offsets[0] != 0 or offsets[-1] != pins or any(a > b for a, b in zip(offsets, offsets[1:])): + raise ValueError('session packet offsets differ') + rows = [] + for begin, end in zip(offsets, offsets[1:]): + row = tuple((struct.unpack_from(' tuple[tuple[tuple[int, int], ...], ...]: + """Strict Python reference decoder used by tests and artifact inspection.""" + if type(payload) is not bytes or type(n) is not int or n < 0: + raise ValueError('query bank requires immutable bytes and nonnegative n') + if len(payload) < QUERY_BANK_HEADER.size + 4: + raise ValueError('truncated query bank') + magic, count, pins, reserved = QUERY_BANK_HEADER.unpack_from(payload) + expected = QUERY_BANK_HEADER.size + 4 * (count + 1) + 12 * pins + if magic != QUERY_BANK_MAGIC or reserved != 0 or expected != len(payload): + raise ValueError('query bank header or length differs') + if count > 1_000_000 or pins > 1_000_000: + raise ValueError('query bank count exceeds supported bound') + offset_at = QUERY_BANK_HEADER.size + vertex_at = offset_at + 4 * (count + 1) + mask_at = vertex_at + 4 * pins + offsets = struct.unpack_from('<' + 'I' * (count + 1), payload, offset_at) + if offsets[0] != 0 or offsets[-1] != pins or any(a > b for a, b in zip(offsets, offsets[1:])): + raise ValueError('query bank offsets differ') + rows = [] + for begin, end in zip(offsets, offsets[1:]): + row = [] + for index in range(begin, end): + vertex = struct.unpack_from('= n: + raise ValueError('query bank vertex outside graph') + row.append((vertex, allowed)) + rows.append(tuple(row)) + return tuple(rows) + + +def _read_build_receipt(library: Path) -> dict: + """Validate the explicit native-build receipt before loading executable code.""" + library = Path(library).resolve() + receipt = library.with_name('build.json') + try: + record = json.loads(receipt.read_text(encoding='utf-8')) + except (OSError, json.JSONDecodeError) as error: + raise ValueError('trusted exact runtime requires a valid adjacent build.json') from error + if type(record) is not dict: + raise ValueError('exact runtime build receipt must be an object') + required = { + 'exact_api_version': EXACT_API_VERSION, + 'native_abi': EXACT_NATIVE_ABI, + 'library_name': library.name, + 'python_implementation': platform.python_implementation(), + 'soabi': sysconfig.get_config_var('SOABI'), + } + for key, value in required.items(): + if record.get(key) != value: + raise ValueError(f'exact runtime build receipt {key} differs') + if record.get('source_sha256') != hashlib.sha256(SOURCE.read_bytes()).hexdigest(): + raise ValueError('exact runtime source hash differs from this installed API') + try: + binary = library.read_bytes() + except OSError as error: + raise ValueError('exact runtime library is not readable') from error + if record.get('library_sha256') != hashlib.sha256(binary).hexdigest(): + raise ValueError('exact runtime library hash differs from its receipt') + return record + + +class ExactRuntime: + """Trusted ABI-3 runtime loaded from an explicit, receipt-bound build.""" + + def __init__(self, library: Path, *, verify_receipt: bool = True): + self.build_receipt = _read_build_receipt(library) if verify_receipt else None + spec = importlib.util.spec_from_file_location('_spectra_exact_binary', Path(library).resolve()) + if spec is None or spec.loader is None: + raise ValueError('invalid trusted native extension path') + self._module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self._module) + if self._module.abi() != EXACT_NATIVE_ABI: + raise ValueError('unsupported exact binary ABI') + + def prepare(self, problem: ExactProblem, *, mode: str = 'scc', + max_bytes: int = DEFAULT_BYTES) -> 'ExactSession': + return ExactSession(self._module, problem, mode=mode, max_bytes=max_bytes) + + def solve_session_packet(self, packet: bytes, *, mode: str = 'route', + max_bytes: int = DEFAULT_BYTES) -> ExactSessionPacketAnswer: + """Construct, solve, verify, serialize and dispose one prepared SBC1 session. + + Opt-in ``auto`` uses raw traversal below 64 requests or on a base-infeasible + graph. Otherwise it uses routed proofs when SCCs at least halve the + literal graph, and plain SCC batching when they do not. Selection uses + fixed-graph structure and bank length, never measured answers or timings. + ``info['selected_mode']`` names the actual engine. Explicit modes and the + default retain their meaning; this policy is an experimental heuristic. + """ + if type(packet) is not bytes: + raise ValueError('session packet must be immutable exact bytes') + if mode not in ('scc', 'raw', 'sparse', 'route', 'auto'): + raise ValueError('mode must be scc, raw, sparse, route or auto') + if type(max_bytes) is not int or not (1 << 20) <= max_bytes <= MAX_BYTES: + raise ValueError('max_bytes must be an exact uint64 of at least 1 MiB') + values = self._module.solve_session_packet( + packet, {'raw': 0, 'scc': 1, 'sparse': 2, 'route': 3, 'auto': 4}[mode], max_bytes) + output, count, sat, unsat, proof_bytes, visits, arcs, info = values + info = {**info, 'backend': 'native-exact-binary', 'mode': mode, + 'exact_api_version': EXACT_API_VERSION, 'native_abi': EXACT_NATIVE_ABI, + 'prepared_input': True, 'input_schema': 'SBC1', + 'output_schema': 'SCQ2', 'portable_unsat_certificate': True, + 'query_answer_cache': False, + 'resource_limit_kind': 'conservative native array admission, not RSS'} + return ExactSessionPacketAnswer(output, count, sat, unsat, proof_bytes, + visits, arcs, info) + + +class ExactSession: + def __init__(self, module, problem: ExactProblem, *, mode: str, + max_bytes: int): + if mode not in ('scc', 'raw', 'sparse', 'route'): + raise ValueError('mode must be scc, raw, sparse or route') + if type(max_bytes) is not int or not (1 << 20) <= max_bytes <= MAX_BYTES: + raise ValueError('max_bytes must be an exact uint64 of at least 1 MiB') + self.problem = ExactProblem.create(problem.n, problem.palette, problem.edges, problem.masks) + self._module, self.mode = module, mode + self._lock = threading.RLock() + self._solver = self._observer = None + self._max_bytes = max_bytes + self._owned_bytes = 0 + p = self.problem + try: + # The two native owners parse original inputs separately. + self._observer = module.observer_create(p.n, p.palette, p.edges, p.masks, max_bytes) + observer_bytes = module.observer_bytes(self._observer) + if observer_bytes >= max_bytes: + raise MemoryError('combined native owners exhaust the session cap') + self._solver = module.create(p.n, p.palette, p.edges, p.masks, + {'raw': 0, 'scc': 1, 'sparse': 2, 'route': 3}[mode], max_bytes - observer_bytes) + self._owned_bytes = observer_bytes + module.info(self._solver)['retained_array_bytes'] + except BaseException: + self.close() + raise + + def _require_open(self) -> None: + if self._solver is None or self._observer is None: + raise RuntimeError('exact binary session is closed') + + def _admit_query(self, query) -> None: + # Conservatively include both native owners, active scratch and returned + # proof/label payload. Python input objects and allocator overhead are not + # bounded by this check; a process cap remains a separate concern. + bound = self._owned_bytes + 512*(self.problem.n+1) + 32*len(query) + 8192 + if len(query) > 1_000_000 or bound > self._max_bytes: + raise MemoryError('combined native query payload admission exceeds cap') + + def solve(self, restrictions=()) -> ExactAnswer: + query = self.problem.freeze_query(restrictions) + with self._lock: + self._require_open() + self._admit_query(query) + decision, labels, proof, visits, arcs = self._module.solve(self._solver, query) + if not self._module.verify(self._observer, query, decision, labels, proof): + raise AssertionError('exact answer failed independent original-input observer') + return ExactAnswer('SAT_VERIFIED' if decision else 'UNSAT_VERIFIED', + labels, proof, visits, arcs) + + def solve_bank(self, packet: bytes) -> ExactBankAnswer: + """Solve, independently verify, and serialize a complete SBQ1 bank.""" + if type(packet) is not bytes: + raise ValueError('query bank must be immutable exact bytes') + with self._lock: + self._require_open() + output, count, sat, unsat, proof_bytes, visits, arcs = self._module.solve_bank( + self._solver, self._observer, packet) + if type(output) is not bytes: + raise AssertionError('native bank endpoint returned mutable output') + return ExactBankAnswer(output, count, sat, unsat, proof_bytes, visits, arcs) + + def check_bank(self, packet: bytes, output: bytes) -> bool: + """Reparse and check a serialized answer bank with the native observer.""" + if type(packet) is not bytes or type(output) is not bytes: + return False + with self._lock: + self._require_open() + return bool(self._module.check_bank(self._observer, packet, output)) + + def check(self, restrictions, answer: ExactAnswer) -> bool: + query = self.problem.freeze_query(restrictions) + with self._lock: + self._require_open() + self._admit_query(query) + if type(answer) is not ExactAnswer or answer.status not in ('SAT_VERIFIED', 'UNSAT_VERIFIED'): + return False + return self._module.verify(self._observer, query, int(answer.status == 'SAT_VERIFIED'), + answer.labels, answer.proof) + + @property + def info(self) -> dict: + with self._lock: + self._require_open() + return {**self._module.info(self._solver), 'backend': 'native-exact-binary', + 'exact_api_version': EXACT_API_VERSION, 'native_abi': EXACT_NATIVE_ABI, + 'mode': self.mode, 'query_answer_cache': False, + 'portable_unsat_certificate': True, 'proof_schema': 'SBP1', + 'native_observer_array_bytes': self._module.observer_bytes(self._observer), + 'resource_limit_kind': 'conservative native array admission, not RSS', + 'exact_scope': 'one/two-colour original domains, fixed conflict graph'} + + def close(self) -> None: + with self._lock: + self._solver = self._observer = None + + def __enter__(self): + with self._lock: + self._require_open() + return self + + def __exit__(self, *_args): + self.close() + + +CERTIFIED_OUTPUT_HEADER = struct.Struct('<4sIQ') + + +def decode_certified_output(payload: bytes, n: int, + count: int) -> tuple[tuple[int, bytes, bytes], ...]: + """Strictly decode SCQ2 without importing or trusting the native runtime.""" + if type(n) is not int or n < 0 or type(count) is not int or count < 0: + raise ValueError('invalid expected certified-output geometry') + if type(payload) is not bytes or len(payload) < CERTIFIED_OUTPUT_HEADER.size: + raise ValueError('invalid certified output') + if CERTIFIED_OUTPUT_HEADER.unpack_from(payload) != (b'SCQ2', n, count): + raise ValueError('certified output header differs') + rows: list[tuple[int, bytes, bytes]] = [] + offset = CERTIFIED_OUTPUT_HEADER.size + if count > (len(payload) - offset) // (n + 5): + raise ValueError('truncated certified row bank') + for _ in range(count): + if offset + n + 5 > len(payload): + raise ValueError('truncated certified row') + code = payload[offset] + labels = payload[offset + 1:offset + 1 + n] + length = struct.unpack_from(' len(payload): + raise ValueError('truncated proof bank') + proof = payload[offset:offset + length] + offset += length + if code == 1: + if proof: + raise ValueError('SAT row must not carry contradiction evidence') + elif code == 0: + if any(labels): + raise ValueError('UNSAT padding must be zero') + decode_proof(proof, n) + else: + raise ValueError('unknown certified decision') + rows.append((code, labels, proof)) + if offset != len(payload): + raise ValueError('unconsumed certified output bytes') + return tuple(rows) + + +def verify_certified_output(problem: ExactProblem, + queries: Iterable[Iterable[Sequence[int]]], + output: bytes) -> bool: + """Replay every SCQ2 row from original Python inputs only.""" + try: + checked = ExactProblem.create(problem.n, problem.palette, + problem.edges, problem.masks) + rows = tuple(checked.freeze_query(query) for query in queries) + answers = decode_certified_output(output, checked.n, len(rows)) + return all(verify_answer( + checked, query, + 'SAT_VERIFIED' if code else 'UNSAT_VERIFIED', + labels if code else b'', proof, + ) for query, (code, labels, proof) in zip(rows, answers)) + except (ValueError, TypeError, AttributeError, OverflowError, struct.error): + return False + + +def verify_session_output(packet: bytes, output: bytes) -> bool: + """Replay an SBC1 -> SCQ2 result without loading native code.""" + try: + problem, rows = unpack_session_packet(packet) + except (ValueError, TypeError, struct.error): + return False + return verify_certified_output(problem, rows, output) + + +__all__ = [ + 'EXACT_API_VERSION', 'EXACT_NATIVE_ABI', 'DEFAULT_BYTES', + 'ExactProblem', 'ExactAnswer', 'ExactBankAnswer', 'ExactSessionPacketAnswer', + 'ExactRuntime', 'ExactSession', 'build_exact_runtime', + 'pack_query_bank', 'pack_frozen_query_bank', 'unpack_query_bank', + 'pack_session_packet', 'pack_validated_session_packet', 'unpack_session_packet', + 'decode_proof', 'verify_answer', 'decode_certified_output', + 'verify_certified_output', 'verify_session_output', +] diff --git a/spectra/exact_problem.py b/spectra/exact_problem.py new file mode 100644 index 0000000..e7b5089 --- /dev/null +++ b/spectra/exact_problem.py @@ -0,0 +1,73 @@ +"""Immutable original-address inputs for SPECTRA's exact-query API.""" +from __future__ import annotations + +from dataclasses import dataclass +from typing import Iterable, Sequence + + +@dataclass(frozen=True, slots=True) +class ExactProblem: + """A fixed simple conflict graph with one or two colours per vertex.""" + + n: int + palette: int + edges: tuple[tuple[int, int], ...] + masks: tuple[int, ...] + + @classmethod + def create(cls, n: int, palette: int, edges: Iterable[Sequence[int]], + masks: Iterable[int]) -> 'ExactProblem': + if type(n) is not int or not 0 <= n <= 100_000: + raise ValueError('n must be an exact integer in [0, 100000]') + if type(palette) is not int or not 1 <= palette <= 64: + raise ValueError('palette must be an exact integer in [1, 64]') + snapshot = tuple(masks) + if len(snapshot) != n: + raise ValueError('mask count differs from vertex count') + palette_mask = (1 << palette) - 1 if palette < 64 else (1 << 64) - 1 + for mask in snapshot: + if (type(mask) is not int or mask <= 0 or mask & ~palette_mask + or mask.bit_count() not in (1, 2)): + raise ValueError('each original domain must contain one or two palette colours') + copied: list[tuple[int, int]] = [] + for edge in edges: + row = tuple(edge) + if (len(row) != 2 or any(type(v) is not int or not 0 <= v < n for v in row) + or row[0] == row[1]): + raise ValueError('edge must contain two distinct in-range exact integers') + copied.append((min(row), max(row))) + if len(copied) > 2_000_000: + raise ValueError('edge count exceeds native bound') + return cls(n, palette, tuple(sorted(set(copied))), snapshot) + + def colors(self) -> tuple[tuple[int, ...], ...]: + return tuple(tuple(c for c in range(self.palette) if mask >> c & 1) + for mask in self.masks) + + def freeze_query(self, restrictions: Iterable[Sequence[int]]) -> tuple[tuple[int, int], ...]: + copied: list[tuple[int, int]] = [] + for item in restrictions: + row = tuple(item) + if (len(row) != 2 or type(row[0]) is not int or not 0 <= row[0] < self.n + or type(row[1]) is not int or not 0 <= row[1] < 1 << 64): + raise ValueError('query must contain in-range vertex/uint64-mask pairs') + copied.append((row[0], row[1])) + if len(copied) > 1_000_000: + raise ValueError('query exceeds one million pins') + return tuple(copied) + + def check(self, labels: bytes, query: Iterable[Sequence[int]] = ()) -> bool: + """Check a complete label vector against original inputs only.""" + try: + frozen = self.freeze_query(query) + if type(labels) is not bytes or len(labels) != self.n: + return False + allowed = list(self.masks) + for vertex, mask in frozen: + allowed[vertex] &= mask + if any(color >= self.palette or not ((allowed[v] >> color) & 1) + for v, color in enumerate(labels)): + return False + return all(labels[left] != labels[right] for left, right in self.edges) + except (TypeError, ValueError, OverflowError): + return False diff --git a/spectra/exact_proof.py b/spectra/exact_proof.py new file mode 100644 index 0000000..b0c840e --- /dev/null +++ b/spectra/exact_proof.py @@ -0,0 +1,96 @@ +"""Public standard-library SBP1 verifier, independent of the native solver. + +No compiler imports, native index, saved feasibility result, SCC certificate or +answer bank. Literal 2*v denotes the lower available colour; 2*v+1 the higher +(or the unavailable alternative for a singleton). All integers are little endian. +""" +from __future__ import annotations + +import struct + +HEADER = struct.Struct('<4sIII') + + +def decode_proof(payload: bytes, n: int) -> tuple[int, tuple[int, ...], tuple[int, ...]]: + if type(n) is not int or not 0 <= n <= 100_000: + raise ValueError('invalid original variable count') + if type(payload) is not bytes or not HEADER.size <= len(payload) <= 20 + 16*n: + raise ValueError('invalid bounded proof buffer') + magic, kind, left, right = HEADER.unpack_from(payload) + if magic != b'SBP1' or len(payload) != HEADER.size + 4*(left+right): + raise ValueError('proof header/length differs') + if kind == 1: + if left != 1 or right != 0: + raise ValueError('empty-domain proof needs one original vertex') + elif kind in (2, 3): + if not 1 <= left <= 2*n or not 1 <= right <= 2*n: + raise ValueError('path size outside original literal count') + else: + raise ValueError('unsupported proof kind') + values = tuple(value[0] for value in struct.iter_unpack(' bool: + """Reject invalid input/evidence; check truth only from original constraints. + + `visited`/timing counters are not evidence and are intentionally not inputs. + A valid proof can remain valid under stronger restrictions; mere difference + from a previous byte string does not make a proof fresh or stale. + """ + try: + n, k = problem.n, problem.palette + if type(n) is not int or not 0 <= n <= 100_000 or type(k) is not int or not 1 <= k <= 64: + return False + masks = tuple(problem.masks) + if len(masks) != n or any(type(d) is not int or d <= 0 or d >> k or d.bit_count() > 2 for d in masks): + return False + choices = tuple(tuple(c for c in range(k) if d & (1 << c)) for d in masks) + edges = set() + for row in problem.edges: + u, v = row + if any(type(x) is not int or not 0 <= x < n for x in (u, v)) or u == v: + return False + edges.add((min(u, v), max(u, v))) + allowed = list(masks) + for row in query: + vertex, domain = row + if (type(vertex) is not int or not 0 <= vertex < n or + type(domain) is not int or not 0 <= domain < 1 << 64): + return False + allowed[vertex] &= domain + if type(labels) is not bytes or type(certificate) is not bytes: + return False + if status == 'SAT_VERIFIED': + return (not certificate and len(labels) == n + and all(c < k and (allowed[v] >> c) & 1 for v, c in enumerate(labels)) + and all(labels[u] != labels[v] for u, v in edges)) + if status != 'UNSAT_VERIFIED' or labels: + return False + kind, a, b = decode_proof(certificate, n) + if kind == 1: + return a[0] < n and allowed[a[0]] == 0 + if (any(not 0 <= x < 2*n for x in a+b) or + len(set(a)) != len(a) or len(set(b)) != len(b)): + return False + + def color(literal): + row = choices[literal // 2] + return row[literal % 2] if literal % 2 < len(row) else None + + for path in (a, b): + for before, after in zip(path, path[1:]): + u, v = before // 2, after // 2 + if u == v: + if before != 2*u+1 or after != 2*u or len(choices[u]) != 1: + return False + elif ((min(u, v), max(u, v)) not in edges or color(before) is None + or color(after ^ 1) is None or color(before) != color(after ^ 1)): + return False + if kind == 3: + return a[0] == b[-1] and a[-1] == b[0] and a[-1] == (a[0] ^ 1) + return (a[-1] == (b[-1] ^ 1) and + all(color(root) is not None and allowed[root//2] == 1 << color(root) + for root in (a[0], b[0]))) + except (ValueError, TypeError, AttributeError, OverflowError, struct.error): + return False diff --git a/tests/public/test_exact_api.py b/tests/public/test_exact_api.py new file mode 100644 index 0000000..7b9ebc4 --- /dev/null +++ b/tests/public/test_exact_api.py @@ -0,0 +1,196 @@ +"""Installed proof-carrying exact-query API contracts. + +These are correctness and packaging contracts, not performance claims. Native +compilation is explicit and skipped only when the platform has no supported local +compiler; the dedicated exact-public workflow requires it. +""" +from __future__ import annotations + +import hashlib +import json +import os +from pathlib import Path +import shutil +import struct +import sys + +import pytest + +from spectra.cli import main as cli_main +from spectra.exact import ( + EXACT_API_VERSION, + EXACT_NATIVE_ABI, + ExactProblem, + ExactRuntime, + build_exact_runtime, + decode_certified_output, + pack_query_bank, + pack_session_packet, + unpack_query_bank, + unpack_session_packet, + verify_answer, + verify_certified_output, + verify_session_output, +) + +ROOT = Path(__file__).resolve().parents[2] + + +def tiny_problem() -> ExactProblem: + return ExactProblem.create(2, 2, ((0, 1),), (0b11, 0b11)) + + +def test_public_contract_versions_and_packaged_source_identity(): + assert EXACT_API_VERSION == 1 + assert EXACT_NATIVE_ABI == 3 + packaged = ROOT / 'spectra/_native/exact_binary.cpp' + research = ROOT / 'experiments/compiled_query/exact_native.cpp' + assert packaged.read_bytes() == research.read_bytes() + assert hashlib.sha256(packaged.read_bytes()).hexdigest() == hashlib.sha256( + research.read_bytes()).hexdigest() + + +def test_problem_canonicalizes_inputs_but_packets_require_canonical_bytes(): + problem = ExactProblem.create(3, 3, ((2, 1), (0, 1), (1, 0)), (0b011, 0b110, 0b101)) + assert problem.edges == ((0, 1), (1, 2)) + packet = pack_session_packet(problem, ((), ((0, 1),))) + decoded, rows = unpack_session_packet(packet) + assert decoded == problem and rows == ((), ((0, 1),)) + + # Reverse the first canonical edge inside SBC1. The strict decoder must reject + # rather than silently sort attacker-controlled prepared bytes. + damaged = bytearray(packet) + edge_at = struct.Struct('<4s7I').size + 8 * problem.n + damaged[edge_at:edge_at + 8] = struct.pack(' bool: + return bool(shutil.which('cl' if sys.platform == 'win32' else 'g++')) + + +@pytest.fixture(scope='session') +def exact_build(tmp_path_factory): + supplied = os.environ.get('SPECTRA_EXACT_LIBRARY') + if supplied is not None: + return Path(supplied).resolve() + if sys.platform not in ('linux', 'win32') or not _compiler_available(): + pytest.skip('supported native compiler is unavailable') + return build_exact_runtime(tmp_path_factory.mktemp('public-exact-runtime')) + + +@pytest.fixture(scope='session') +def exact_runtime(exact_build): + return ExactRuntime(exact_build) + + +def test_receipt_bound_build_rejects_tampering(tmp_path, exact_build): + build = tmp_path / 'build' + build.mkdir() + library = build / exact_build.name + shutil.copy2(exact_build, library) + shutil.copy2(exact_build.with_name('build.json'), build / 'build.json') + record_path = library.with_name('build.json') + record = json.loads(record_path.read_text()) + record['source_sha256'] = '0' * 64 + record_path.write_text(json.dumps(record)) + with pytest.raises(ValueError, match='source hash'): + ExactRuntime(library) + + +def test_native_session_returns_checked_sat_and_unsat(exact_runtime): + problem = tiny_problem() + unsat_query = ((0, 1), (1, 1)) + with exact_runtime.prepare(problem, mode='scc') as session: + sat = session.solve(()) + unsat = session.solve(unsat_query) + assert sat.status == 'SAT_VERIFIED' + assert problem.check(sat.labels) + assert verify_answer(problem, (), sat.status, sat.labels, sat.proof) + assert unsat.status == 'UNSAT_VERIFIED' + assert verify_answer(problem, unsat_query, unsat.status, unsat.labels, unsat.proof) + assert session.check((), sat) + assert session.check(unsat_query, unsat) + assert session.info['exact_api_version'] == EXACT_API_VERSION + assert session.info['native_abi'] == EXACT_NATIVE_ABI + + +def test_one_call_packet_output_is_independently_replayable(exact_runtime): + problem = tiny_problem() + queries = ((), ((0, 1),), ((0, 1), (1, 1))) + packet = pack_session_packet(problem, queries) + result = exact_runtime.solve_session_packet(packet, mode='auto') + assert result.query_count == 3 + assert result.sat_count == 2 and result.unsat_count == 1 + rows = decode_certified_output(result.output, problem.n, len(queries)) + assert tuple(code for code, _, _ in rows) == (1, 1, 0) + assert verify_certified_output(problem, queries, result.output) + assert verify_session_output(packet, result.output) + + damaged = bytearray(result.output) + damaged[-1] ^= 1 + assert not verify_session_output(packet, bytes(damaged)) + + +def test_runtime_close_is_idempotent_and_fail_closed(exact_runtime): + session = exact_runtime.prepare(tiny_problem()) + session.close() + session.close() + with pytest.raises(RuntimeError): + session.solve(()) + + +def test_cli_replays_certified_output_without_native_code(tmp_path, capsys): + problem = tiny_problem() + query = ((0, 0),) + packet = pack_session_packet(problem, (query,)) + proof = struct.pack('<4sIII I', b'SBP1', 1, 1, 0, 0) + output = struct.pack('<4sIQ', b'SCQ2', problem.n, 1) + b'\x00' + bytes(problem.n) + struct.pack('