Integrate proof-carrying exact queries, installed API, and exam repair

.github/workflows/checkpoint-recovery.yml

@@ -0,0 +1,59 @@
+name: checkpoint-recovery
+on:
+  push:
+    branches: [research/100-blitz-20261016]
+    paths: ['.github/workflows/checkpoint-recovery.yml']
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: checkpoint-recovery-${{ github.ref }}
+  cancel-in-progress: false
+jobs:
+  recover:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - name: Verify repository and create exact recovery materials
+        env:
+          REVIEW_BASE: 575eb1e657fc8c5d06fd56a519efd59f95dc0a2d
+        run: |
+          set -euo pipefail
+          mkdir -p checkpoint-recovery
+          git merge-base --is-ancestor "$REVIEW_BASE" HEAD
+          git diff --check "$REVIEW_BASE"..HEAD
+          git fsck --strict
+          git rev-parse HEAD > checkpoint-recovery/source_commit.txt
+          git rev-parse HEAD^{tree} > checkpoint-recovery/source_tree.txt
+          printf '%s\n' "$REVIEW_BASE" > checkpoint-recovery/review_base.txt
+          git log --format='%H %T %s' "$REVIEW_BASE"..HEAD > checkpoint-recovery/commit_ledger.txt
+          git diff --binary "$REVIEW_BASE"..HEAD > checkpoint-recovery/review.patch
+          git format-patch --stdout --binary "$REVIEW_BASE"..HEAD > checkpoint-recovery/review-series.patch
+          git archive --format=tar.gz --output=checkpoint-recovery/source.tar.gz HEAD
+          git bundle create checkpoint-recovery/source.bundle HEAD
+          git bundle verify checkpoint-recovery/source.bundle > checkpoint-recovery/bundle-verify.txt 2>&1
+          python - <<'PY'
+          import hashlib, json
+          from pathlib import Path
+          root = Path('checkpoint-recovery')
+          files = {}
+          for path in sorted(root.iterdir()):
+              if path.is_file() and path.name != 'SHA256SUMS.json':
+                  files[path.name] = {
+                      'bytes': path.stat().st_size,
+                      'sha256': hashlib.sha256(path.read_bytes()).hexdigest(),
+                  }
+          (root / 'SHA256SUMS.json').write_text(
+              json.dumps(files, indent=2, sort_keys=True) + '\n', encoding='utf-8')
+          PY
+      - uses: actions/upload-artifact@v4
+        with:
+          name: spectra-100-blitz-recovery-${{ github.sha }}
+          path: checkpoint-recovery/
+          include-hidden-files: true
+          retention-days: 90
+          if-no-files-found: error

.github/workflows/itc-exam-suite.yml

@@ -0,0 +1,130 @@
+name: itc-exam-suite
+on:
+  push:
+    branches: [research/100-blitz-20261016]
+    paths:
+      - '.github/workflows/itc-exam-suite.yml'
+      - 'spectra/exact*.py'
+      - 'spectra/exam_repair.py'
+      - 'spectra/itc2007_exam.py'
+      - 'spectra/_native/exact_binary.cpp'
+      - 'experiments/compiled_query/exact.py'
+      - 'experiments/compiled_query/exact_native.cpp'
+      - 'experiments/compiled_query/test_exact.py'
+      - 'experiments/compiled_query/itc_exam_transfer.py'
+      - 'experiments/compiled_query/itc_exam_suite.py'
+      - 'experiments/compiled_query/test_itc_exam_transfer.py'
+      - 'experiments/compiled_query/test_itc_exam_suite.py'
+      - 'experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md'
+      - 'experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md'
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: itc-exam-suite-${{ github.ref }}
+  cancel-in-progress: false
+env:
+  OMP_NUM_THREADS: '1'
+  OPENBLAS_NUM_THREADS: '1'
+jobs:
+  suite:
+    name: Prospective ITC suite (${{ matrix.runner }}, Python ${{ matrix.python }})
+    runs-on: ${{ matrix.runner }}
+    timeout-minutes: 60
+    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==8.4.2'
+      - uses: actions/checkout@v4
+        with:
+          repository: davidvanbulck/ITC-2007-CETT
+          ref: ed2d4c0cf5302b77a8b321cd0380de0bb579d538
+          path: upstream/ITC-2007-CETT
+          persist-credentials: false
+      - name: Validate selector and suite contracts
+        run: |
+          set -euo pipefail
+          python -m pytest \
+            tests/public/test_exam_repair.py \
+            tests/public/test_itc2007_exam.py \
+            --confcutdir=tests/public -q \
+            --junitxml=suite-public-contracts.xml
+          python -m pytest \
+            experiments/compiled_query/test_exact.py \
+            experiments/compiled_query/test_itc_exam_transfer.py \
+            experiments/compiled_query/test_itc_exam_suite.py \
+            -q -k 'auto or tiled_witnesses or itc or suite' \
+            --junitxml=suite-research-contracts.xml
+      - name: Build and exercise the installed application API
+        run: |
+          set -euo pipefail
+          python -m build --wheel --outdir suite-wheel
+          python -m venv suite-install
+          suite-install/bin/python -m pip install --no-deps suite-wheel/*.whl
+          suite-install/bin/python -I scripts/check_exam_repair_installation.py \
+            --out installed-exam-repair.json | tee installed-exam-repair.log
+      - name: Freeze all roles before any holdout execution
+        run: |
+          set -euo pipefail
+          python -m experiments.compiled_query.itc_exam_suite freeze \
+            --root itc-suite-evidence \
+            --upstream-root upstream/ITC-2007-CETT \
+            --queries 1024 \
+            --holdout-max-auto-raw-ratio 1.15 | tee freeze.log
+      - name: Execute and independently audit every case
+        run: |
+          set -euo pipefail
+          python -m experiments.compiled_query.itc_exam_suite run \
+            --root itc-suite-evidence | tee run.log
+          python -S -m experiments.compiled_query.itc_exam_suite audit \
+            --root itc-suite-evidence | tee audit.log
+          python - <<'PY'
+          import json
+          from pathlib import Path
+          result = json.loads(Path('itc-suite-evidence/suite-audit.json').read_text())
+          assert result['functional_complete']
+          assert result['holdout_gate_pass'], result['holdout_failures']
+          roles = [case['role'] for case in result['cases']]
+          assert roles == ['development', 'holdout', 'holdout']
+          for case in result['cases']:
+              assert case['queries'] == 1024
+              assert case['sat'] + case['unsat'] == 1024
+              assert case['auto_vs_raw_paired_median_ratio'] > 0
+          print('Prospective holdout guardrail passed. Not a full timetabling claim.')
+          PY
+      - name: Preserve exact environment and source receipts
+        if: always()
+        run: |
+          set -euo pipefail
+          mkdir -p suite-receipts
+          git rev-parse HEAD > suite-receipts/source_commit.txt
+          git rev-parse HEAD^{tree} > suite-receipts/source_tree.txt
+          git -C upstream/ITC-2007-CETT rev-parse HEAD > suite-receipts/upstream_commit.txt
+          python -VV > suite-receipts/python.txt
+          uname -a > suite-receipts/platform.txt
+          lscpu > suite-receipts/cpu.txt
+          cp suite-public-contracts.xml suite-research-contracts.xml \
+            freeze.log run.log audit.log installed-exam-repair.json \
+            installed-exam-repair.log suite-receipts/ 2>/dev/null || true
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: itc-exam-suite-${{ matrix.runner }}-py${{ matrix.python }}-${{ github.run_id }}
+          path: |
+            itc-suite-evidence/
+            suite-receipts/
+            suite-wheel/
+          retention-days: 90
+          if-no-files-found: warn

.github/workflows/itc-exam-transfer.yml

@@ -0,0 +1,118 @@
+name: itc-exam-transfer
+on:
+  push:
+    branches: [research/100-blitz-20261016]
+    paths:
+      - '.github/workflows/itc-exam-transfer.yml'
+      - 'spectra/exact*.py'
+      - 'spectra/exam_repair.py'
+      - 'spectra/itc2007_exam.py'
+      - 'spectra/_native/exact_binary.cpp'
+      - 'experiments/compiled_query/itc_exam_transfer.py'
+      - 'experiments/compiled_query/test_itc_exam_transfer.py'
+      - 'experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md'
+      - 'experiments/compiled_query/itc_exam_suite.py'
+      - 'experiments/compiled_query/test_itc_exam_suite.py'
+      - 'experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md'
+      - 'tests/public/test_exam_repair.py'
+      - 'tests/public/test_itc2007_exam.py'
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: itc-exam-transfer-${{ github.ref }}
+  cancel-in-progress: false
+env:
+  OMP_NUM_THREADS: '1'
+  OPENBLAS_NUM_THREADS: '1'
+jobs:
+  transfer:
+    name: ITC conflict-core transfer (${{ matrix.runner }}, Python ${{ matrix.python }})
+    runs-on: ${{ matrix.runner }}
+    timeout-minutes: 45
+    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 }}
+      - name: Install the pinned test runner
+        run: python -m pip install 'pytest==8.4.2'
+      - uses: actions/checkout@v4
+        with:
+          repository: davidvanbulck/ITC-2007-CETT
+          ref: ed2d4c0cf5302b77a8b321cd0380de0bb579d538
+          path: upstream/ITC-2007-CETT
+          persist-credentials: false
+      - name: Check the public adapter and immutable evidence harness
+        run: |
+          set -euo pipefail
+          python -m pytest \
+            tests/public/test_exam_repair.py \
+            tests/public/test_itc2007_exam.py \
+            --confcutdir=tests/public -q \
+            --junitxml=transfer-public-contracts.xml
+          python -m pytest \
+            experiments/compiled_query/test_itc_exam_transfer.py \
+            -q --junitxml=transfer-research-contracts.xml
+      - name: Freeze the published instance only after the protocol is committed
+        run: |
+          set -euo pipefail
+          python -m experiments.compiled_query.itc_exam_transfer freeze \
+            --root itc-transfer-evidence \
+            --instance upstream/ITC-2007-CETT/examtt-instances/Instances/set9.exam \
+            --solution upstream/ITC-2007-CETT/InitMethods/SolStore/set9_OBSIFeas_0.sol \
+            --license upstream/ITC-2007-CETT/LICENSE \
+            --queries 1024 \
+            --evaluation-role development | tee freeze.log
+      - name: Run every exact engine and replay every answer
+        run: |
+          set -euo pipefail
+          python -m experiments.compiled_query.itc_exam_transfer run \
+            --root itc-transfer-evidence | tee run.log
+          python -S -m experiments.compiled_query.itc_exam_transfer audit \
+            --root itc-transfer-evidence | tee audit.log
+          python - <<'PY'
+          import json
+          from pathlib import Path
+          result = json.loads(Path('itc-transfer-evidence/audit.json').read_text())
+          assert result['functional_complete']
+          assert result['baseline_valid_full_itc_hard_constraints']
+          assert result['queries'] == 1024
+          assert result['model']['schema'] == 'spectra.itc2007.conflict_core.v1'
+          assert result['modes']['auto']['auto_policy'] == 'structural-v2'
+          assert result['modes']['auto']['selected_mode'] == 'raw'
+          assert result['modes']['auto']['auto_policy_reason'] == 'high_pin_density'
+          print('Functional transfer complete. This is not a full ITC timetable claim.')
+          PY
+      - name: Preserve exact source and environment receipts
+        if: always()
+        run: |
+          set -euo pipefail
+          mkdir -p transfer-receipts
+          git rev-parse HEAD > transfer-receipts/source_commit.txt
+          git rev-parse HEAD^{tree} > transfer-receipts/source_tree.txt
+          git -C upstream/ITC-2007-CETT rev-parse HEAD > transfer-receipts/upstream_commit.txt
+          python -VV > transfer-receipts/python.txt
+          uname -a > transfer-receipts/platform.txt
+          lscpu > transfer-receipts/cpu.txt
+          cp transfer-public-contracts.xml transfer-research-contracts.xml \
+            freeze.log run.log audit.log transfer-receipts/ 2>/dev/null || true
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: itc-exam-transfer-${{ matrix.runner }}-py${{ matrix.python }}-${{ github.run_id }}
+          path: |
+            itc-transfer-evidence/
+            transfer-receipts/
+          retention-days: 90
+          if-no-files-found: warn

.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-*", "research/faster-queries-review-*"]
+    branches: [main, "maintenance/**", "research/deductive-search-*", "research/focused-search-*", "research/research-engineering-*", "research/faster-queries-review-*", "research/exact-public-api-*"]
   workflow_dispatch:
 permissions:
   contents: read
@@ -48,6 +48,7 @@ jobs:
           .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
+          .public-package/install/venv/bin/python -I scripts/check_exam_repair_installation.py --out .public-package/exam-repair-install.json | tee .public-package/exam-repair-install.txt
       - name: Run and replay frozen compact-state comparison
         run: |
           set -o pipefail

docs/EXAM_REPAIR.md

@@ -0,0 +1,70 @@
+# Proof-carrying bounded exam repair
+
+`spectra.exam_repair` maps a narrow operational rescheduling problem to the
+versioned `spectra.exact` API:
+
+- each exam has one or two pre-approved candidate periods;
+- exams sharing a student may not use the same period;
+- explicit exam exclusions are also supported;
+- current period closures, fixed moves, and allowed-period restrictions are
+  intersected into an exact query;
+- SAT returns a complete named assignment;
+- UNSAT returns an independently verifiable proof that can be translated into
+  named exams, periods, and a shared-student/exclusion chain.
+
+```python
+from spectra.exam_repair import ExamRepairModel
+from spectra.exact import ExactRuntime, build_exact_runtime
+
+model = ExamRepairModel.create(
+    period_ids=("Monday AM", "Monday PM"),
+    exam_ids=("MATH101", "CHEM101", "HIST101"),
+    students=((11, 20), (20, 31), (31,)),
+    candidate_periods=(("Monday AM", "Monday PM"),) * 3,
+)
+query = model.freeze_event(
+    closed_periods=(),
+    fixed=(("MATH101", "Monday AM"), ("CHEM101", "Monday AM")),
+)
+
+runtime = ExactRuntime(build_exact_runtime("exact-native"))
+with runtime.prepare(model.problem, mode="scc") as session:
+    answer = session.solve(query)
+
+if answer.status == "SAT_VERIFIED":
+    print(model.assignment_from_labels(answer.labels, query))
+else:
+    print(model.explain_unsat(query, answer.proof))
+```
+
+## Scope boundary
+
+This is **bounded repair**, not full timetabling.  The adapter does not generate
+candidate periods or model room capacity, room assignment, precedence,
+coincidence, or soft objectives.  Those constraints must be incorporated before
+admission or checked separately.
+
+`spectra.itc2007_exam` provides a strict reader for the ITC-2007 examination
+format.  Its `conflict_core` conversion preserves an immutable receipt of every
+constraint class outside the bounded model and refuses conversion unless the
+caller explicitly acknowledges those omissions.
+
+The research transfer protocol is documented in
+[`ITC_EXAM_TRANSFER_PROTOCOL.md`](../experiments/compiled_query/ITC_EXAM_TRANSFER_PROTOCOL.md).
+
+## Prospective multi-instance evaluation
+
+The selector-v2 policy and its `set10`/`set12` execution holdouts are fixed in
+[`ITC_EXAM_SUITE_PROTOCOL.md`](../experiments/compiled_query/ITC_EXAM_SUITE_PROTOCOL.md).
+The completed cross-platform measurements, retained negative repetitions and
+artifact digests are published in the
+[`2026-10-16 suite results`](../experiments/compiled_query/ITC_EXAM_SUITE_RESULTS_20261016.md).
+The suite rotates measured engine order, preserves every failed cell, and gates
+only the predeclared auto/raw overhead on holdout cases.  Passing that suite is
+application-transfer evidence, not an operator deployment or full ITC-2007
+optimization result.
+
+An outside runner can reproduce the source, installed-wheel, freeze, execution and
+offline-audit boundaries using the
+[independent replication guide](../experiments/compiled_query/ITC_EXAM_REPLICATION.md).
+Negative or conflicting replications are explicitly valid results.