fix(processor): bound the complete solver operation (#1108)

docs/decisions/issue-1108-asr-530-operation-bounded-solver.md

@@ -0,0 +1,39 @@
+# Issue 1108 / ASR-530 Operation-Bounded Solver
+
+Date: 2026-08-11
+
+Issue: #1108. Requirement: ASR-530. Related: #1114 and closed issue #826.
+
+## Decision
+
+One satisfiability analysis builds one deterministic incremental QF_LIA solver
+session. Each normalized clause is encoded once behind a Boolean assumption.
+The initial decision, canonical witness probes, and sorted-deletion core probes
+select clauses and fixed domain indices through assumptions; they do not rebuild
+the variable and expression graph.
+
+A monotonic 5000 ms operation deadline starts before solver construction and
+covers expression construction, every Z3 call, and deterministic result
+selection. Each check receives the remaining operation time, rounded up to a
+positive millisecond and capped at the governed timeout. A result that returns
+after the deadline is an operational failure, never SAT or UNSAT evidence.
+The existing derived check-count budget remains an independent cardinality
+bound.
+
+## Compatibility and Nonclaims
+
+The normalized theory, solver package/logic/options, initial decision, canonical
+lexicographic witness order, sorted-deletion subset-minimal core order, evidence
+schema, and replay digest remain unchanged. The configuration field
+`timeout_ms=5000` now honestly bounds the whole solver operation rather than
+each individual check. This is an in-process resource bound; it is not a claim
+of hard process isolation against a compromised native Z3 library.
+
+## Verification
+
+Differential property tests compare complete SAT assignments and UNSAT cores
+with the incumbent rebuilding algorithm over generated bounded models. Tests
+count one solver construction, force expiry during construction, before a
+check, inside repeated selection, and immediately after a nominal Z3 result,
+and verify that no partial evidence crosses the service boundary. A high-check
+shape guards against renewed per-check graph construction.

docs/decisions/issue-1114-solver-operational-safety-remediation.md

@@ -0,0 +1,94 @@
+# Issue 1114 Solver Operational-Safety Remediation
+
+Date: 2026-08-11
+
+Issue: #1114. Requirement: ASR-530. Related lineage: closed issue #826.
+
+This note records the bounded operational-safety correction without modifying
+the immutable issue-826 preflight. It does not change the v1 theory,
+solver package pin, solver configuration contract, witness order, or
+core-reduction order.
+
+## Gap Claim
+
+Z3 may return `unknown` under the configured per-check timeout. The witness and
+core loops compared only against their desired decisive result, so `unknown`
+could silently skip a canonical witness candidate or retain a removable core
+clause while the emitted evidence still claimed the governed selection rule.
+Duplicate clause ids also reached tracked assumptions through a collapsing
+dictionary, and empty memberships relied on an implicit zero-argument `Or`.
+
+## Existing Surface Audit
+
+The normalized contract already requires unique clause ids and finite bounded
+symbols, domains, and clauses. The service already translates adapter failure
+to `SatisfiabilityOperationalError`, and the evidence contract already records
+the 5000 ms per-check timeout. The shared `_check()` seam is used by the initial
+decision, witness selection, and core reduction, making it the single complete
+place to reject `unknown`.
+
+## Lineage And Precedent
+
+ADR-086 and the normative satisfiability specification distinguish completed
+SAT/UNSAT outcomes from operational failure. The issue-826 preflight explicitly
+forbids mapping unknown, timeout, or exhaustion to a semantic outcome and
+requires bounded repeated checks for canonical witnesses and reduced cores.
+
+## Literature And Practice
+
+SMT solver APIs expose `sat`, `unsat`, and `unknown` as distinct results; a
+resource-limited `unknown` is not evidence for either decision. Deterministic
+core reduction and lexicographic witness selection therefore require every
+probe to complete decisively before their stronger labels may be published.
+
+## Alternatives Considered
+
+1. **Retain the old branch behavior.** Rejected because it can publish an
+   overclaim that appears only as later replay drift.
+2. **Map unknown to `unsupported`.** Rejected because translation coverage is
+   complete; solver non-completion is an operational failure.
+3. **Retry unknown automatically.** Rejected because unrecorded retries change
+   the operational profile and can make latency unbounded.
+4. **Add a caller-configurable check limit to the v1 wire contract.** Rejected
+   as an unnecessary profile/schema change.
+5. **Reject unknown centrally and derive a finite check budget from the bound
+   normalized model.** Chosen.
+
+## Chosen Architecture
+
+Before constructing tracked assumptions, the adapter defensively rejects
+duplicate clause ids. Empty membership is explicitly `false`. `_check()` raises
+a structured `SolverOperationalError` for `unknown`, recording phase, check
+count, derived check budget, the governed 5000 ms timeout, and Z3's bounded
+reason string. The service preserves those safe fields on
+`SatisfiabilityOperationalError`; it emits no partial evidence.
+
+For model symbols `S`, domains `D(s)`, and clauses `C`, the run budget is:
+
+```text
+B = 1 + max(|C|, sum(|D(s)| for s in S))
+```
+
+One check is the initial decision. Only one of the bounded branches then runs:
+at most one deletion probe per clause, or at most one feasibility probe per
+domain member. The budget is thus derived from digest-bound normalized input,
+not a hidden configuration knob, and its maximum is bounded by the published
+contract cardinalities.
+
+## Documentation Defense
+
+The normative solver section now states the decisive-result rule, explicit
+empty-membership semantics, derived budget, and observable operational-error
+fields. No schema is regenerated because completed evidence is unchanged and
+an operational failure emits no evidence envelope.
+
+## Verification Plan
+
+- Force the first or second solver call to return unknown and prove that no
+  outcome, witness, or core evidence is emitted.
+- Assert phase, call count, budget, timeout, and reason survive the service
+  boundary.
+- Inject duplicate clause identity past model validation and require a bounded
+  adapter error rather than a raw Z3 exception.
+- Exercise an empty target domain as explicit unsatisfiability and exhaust a
+  synthetic zero-check budget before solver construction.

docs/requirements/ASR-530/requirement.md

@@ -52,5 +52,11 @@ Agent-assisted development can produce internally coherent code and documentatio
 - TESTS → TEST `implementations/python/tests/test_scenario_satisfiability.py` (Scenario satisfiability analysis and evidence tests)
 - TESTS → TEST `implementations/python/tests/test_satisfiability_cli.py` (Governed satisfiability CLI tests)
 - IMPLEMENTS → GITHUB_ISSUE `826` (Governed whole-scenario constraint satisfiability and solver evidence)
+- IMPLEMENTS → GITHUB_ISSUE `1114` (Fail-closed incomplete solver checks and defensive solver-boundary validation)
+- DOCUMENTS → DOCUMENTATION `docs/decisions/issue-1114-solver-operational-safety-remediation.md` (Incomplete-check operational-safety remediation)
+- DOCUMENTS → GITHUB_ISSUE `1108` (Complete-operation satisfiability deadline)
+- DOCUMENTS → DOCUMENTATION `docs/decisions/issue-1108-asr-530-operation-bounded-solver.md` (Incremental solver and monotonic deadline decision)
+- IMPLEMENTS → CODE_FILE `implementations/python/packages/raes_processor/satisfiability/_solver.py` (Single-session solver and operation-wide deadline)
+- TESTS → TEST `implementations/python/tests/test_scenario_satisfiability.py` (Differential, timeout, and construction-count regressions)
 - IMPLEMENTS → PROOF `docs/research/formal-semantic-validation/bundles/retest-v2.json` (Formal semantic validation atomic retest evidence release v2)
 - IMPLEMENTS → GITHUB_ISSUE `828` (Re-test formal semantic validation, satisfiability, and exploit-path claims)

implementations/python/packages/raes_processor/satisfiability/_service.py

@@ -27,7 +27,7 @@
     canonical_contract_digest,
 )
 
-from ._solver import SolverOperationalError, solve_model
+from ._solver import SOLVER_TIMEOUT_MS, SolverOperationalError, solve_model
 from ._translation import translate_scenario
 
 ANALYSIS_PROFILE = "raes-finite-domain-satisfiability-v1"
@@ -40,6 +40,33 @@ class SatisfiabilityEvidenceError(ValueError):
 class SatisfiabilityOperationalError(RuntimeError):
     """The production analyzer failed outside the typed outcome domain."""
 
+    def __init__(
+        self,
+        message: str,
+        *,
+        solver_phase: str | None = None,
+        solver_check_count: int | None = None,
+        solver_check_budget: int | None = None,
+        solver_timeout_ms: int | None = None,
+        solver_reason: str | None = None,
+    ) -> None:
+        self.solver_phase = solver_phase
+        self.solver_check_count = solver_check_count
+        self.solver_check_budget = solver_check_budget
+        self.solver_timeout_ms = solver_timeout_ms
+        self.solver_reason = solver_reason
+        details = []
+        if solver_phase is not None:
+            details.append(f"phase={solver_phase}")
+        if solver_check_count is not None and solver_check_budget is not None:
+            details.append(f"check={solver_check_count}/{solver_check_budget}")
+        if solver_timeout_ms is not None:
+            details.append(f"timeout_ms={solver_timeout_ms}")
+        if solver_reason is not None:
+            details.append(f"reason={solver_reason}")
+        rendered = f"{message} ({', '.join(details)})" if details else message
+        super().__init__(rendered)
+
 
 def analyze_scenario_file(
     path: Path,
@@ -86,7 +113,14 @@ def analyze_scenario_file(
     try:
         result = solve_model(translation.model)
     except SolverOperationalError as exc:
-        raise SatisfiabilityOperationalError("the pinned solver did not complete") from exc
+        raise SatisfiabilityOperationalError(
+            "the pinned solver did not complete",
+            solver_phase=exc.phase,
+            solver_check_count=exc.check_count,
+            solver_check_budget=exc.check_budget,
+            solver_timeout_ms=exc.timeout_ms,
+            solver_reason=exc.reason,
+        ) from exc
     if result.outcome is SatisfiabilityOutcome.SATISFIABLE:
         assert result.assignment is not None
         instantiated = instantiate_scenario(
@@ -149,7 +183,7 @@ def _solver_configuration() -> SolverConfigurationModel:
             engine_version=engine_version,
             logic="QF_LIA",
             random_seed=0,
-            timeout_ms=5000,
+            timeout_ms=SOLVER_TIMEOUT_MS,
             threads=1,
             auto_config=False,
             model=True,