Repository navigation
Integrate proof-carrying exact queries, installed API, and exam repair - #66
Merged
Merged
Conversation
…exhaustive contracts
…with source receipts
…ndent replay and failure-safe resume 145 native comparator/harness contracts pass locally. Preserve exact one-query inputs, full original witnesses, binary output and hashing costs, backend disposal, source/dependency receipts, Linux process limits and all negative outcomes. Add Python 3.11/3.13 development matrix on exposed WAP05/06 only. UNKNOWN remains incomplete; no new holdout, score increase or flagship claim.
…d run unchanged workspace audits
…grouping for stronger CUDD controls
…amortized soft guards
…ce-guard regression contracts
…s without replacing legacy evidence
… and total original-model reconstruction
… checker contract
…ost session matrix
…cycle and native-backend requirements
…Python 3.11 and 3.13
…-ordered next gates Preserve 237 native contracts on Python 3.11/3.13, 2590 passing public CPU tests, 449 protected historical files, complete-cost two-graph results and all timeout/UNKNOWN/OOM limitations. This is additive development validation, not a native solver speedup, new holdout, outside replication, package release or flagship regrade.
…come validation Implement independently checked SAT colourings and SBP1 original-literal UNSAT paths, raw/SCC/sparse-proof controls, strict SCQ2 transport, and charged proof generation, checking and disposal. Preserve legacy UNKNOWN outcomes and all historical evidence. Add exhaustive original-input, forgery, lifecycle and process-replay contracts plus Python 3.11/3.13 and sanitizer development workflow. Exact staged/source tree: 8c40f09. Opt-in research infrastructure; not a new release, general SAT novelty or fresh holdout result.
…lete-cost comparison Retain original-edge SCC routing trees and DAG bridges instead of a second proof-graph search. Give raw, SCC, sparse and routed exact controls the same sparse pin preparation. Version native ABI and capsule handles, preserving rejection before dereference. Add an independently prepared original-input replay checker with scalar-reference differential tests. Preserve wide-mask API failures and add a mathematically identical common-mask bank without filtering requests or observing answers. Local validation: 338 comparator/service/replay contracts; 58 changed-native contracts under UBSan and ASan+UBSan. Tested source tree 469906f. No default, frozen result, release or flagship claim changes.
…research gates Record completed original-input proof checks, matched raw/native SAT/CUDD costs across three environments, both Python-version and sanitizer contracts, and successful replay of all eight final CI audits. Preserve the first cancelled audit, wide-mask API errors, legacy UNKNOWN results and SAT-only regressions. Reporting-only addition on tested implementation 1556309. No executable, experiment input, default, release or frozen result changes. Whole-program review remains a provisional low-70s assessment, not a flagship claim.
… branch Preserve main's migration core and the original proof-carrying/CUDD baseline. No default, frozen evidence or released package changes. Prepared source and prospective protocol follow as a separately verified checkpoint.
…h and path guards
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Consolidated integration into
mainThis is the single integration point for the completed exact-query line and supersedes stacked drafts #60, #61, #62, #63 and #64.
It integrates exact SAT/UNSAT queries with complete witnesses or portable contradiction proofs, prepared native execution, independent replay, the versioned installed
spectra.exactAPI, proof-carrying exam repair, strict ITC-2007 validation, and the completed prospective multi-instance transfer checks.Head:
13d1d4192e97a4e372ac4aac7743a88b55e814bc.The head is a descendant of current
main, 90 commits ahead and zero behind. Current head workflows passed:exact-public-apipublic-packageQuery runtime checksThe functionality remains opt-in and the documented claim boundaries remain intact. This merge does not claim universal speed superiority, operator adoption, outside replication, or unrestricted timetabling support.
After merge, the stacked drafts will be closed as superseded and obsolete experimental PRs will be archived instead of remaining open indefinitely.