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

[doublewhy]

Plain-language summary

• Context: OpenRAE uses a constraint solver to decide whether a scenario's finite choices can all be satisfied.
• Problem: One analysis could rebuild the same solver thousands of times, its five-second limit covered each individual check instead of the whole operation, and an inconclusive answer could be mistaken for evidence.
• Fix: Reuse one solver, enforce one five-second deadline across construction and every check, and fail safely without publishing partial evidence.

Summary

Build one deterministic incremental QF_LIA solver session per normalized model. Clauses and fixed witness choices are selected through temporary assumptions, preserving the incumbent initial decision, canonical witness order, and sorted-deletion core reduction without rebuilding the expression graph.

The governed 5,000 ms timeout is now one monotonic operation deadline beginning before solver construction. Every native check receives only the remaining time, and a result arriving after the deadline is rejected. The existing finite check-count budget remains an independent bound.

The shared check path also fails closed on Z3 unknown, preserves bounded operational context at the service boundary, rejects duplicate clause IDs before solver construction, and represents empty membership explicitly as false. No partial SAT/UNSAT, canonical-witness, or subset-minimal-core evidence is emitted after an incomplete check.

Related issues

Closes #1108

Closes #1114

Related: #826 (closed governed-profile lineage). Prior proposal: #1083.

Changes

• replace per-probe solver reconstruction with one assumption-gated incremental session
• enforce one monotonic operation deadline across construction, checks, and deterministic result selection
• reject unknown, budget exhaustion, duplicate clause IDs, and deadline expiry through typed operational errors
• preserve solver phase, check count/budget, timeout, and bounded reason without emitting partial evidence
• document architecture, alternatives, compatibility, nonclaims, and ASR-530 traceability for fix(processor): bound the complete satisfiability solver operation #1108 and [BUG] Fail closed when Z3 returns unknown during satisfiability evidence construction #1114
• add differential property tests, deadline-boundary tests, construction-count regression, and defensive failure-path coverage

Test plan

• Satisfiability solver/service regressions on CPython 3.12.13: 30 passed
• Satisfiability CLI, SDL parser, reference processor, and processor-manifest regressions: 123 passed, 1 skipped, 1 deselected
• Parallel satisfiability run with coverage: 30 passed
• Changed executable-line coverage: 100% (120/120, diff-cover against origin/dev)
• Changed branch coverage: 100%; _solver.py is 100% line and branch covered, and all introduced _service.py branches are covered
• Python 3.12 non-host suite under coverage: 6,405 passed, 1 skipped after excluding the libvirt guest-certification file and its /usr/bin/busybox builder test
• Ruff format and lint pass
• Repository policy passes; Ground Control requirement lookup skipped cleanly when its service was unavailable
• Canonical verification integration, contracts, static policy/lint, and docs lanes pass
• Complete canonical nox -s verify: attempted; this macOS worktree lacks /usr/bin/busybox for host-specific libvirt tests and the pinned offline Isabelle acquisition

Checklist

• Code follows the project coding standards
• Classified FM2: bounded constraint semantics with typed IR and differential/property coverage
• No published contract schema changed; regeneration is not applicable
• PR title is a Conventional Commit
• Architectural and normative formal-semantics documentation updated

Notes for review

• Based directly on dev commit 3d6e369b after merged PR feat: separate compute kind from realization substrate #1082.
• Closed issue Governed whole-scenario constraint satisfiability and solver evidence #826 is lineage only; this PR does not attempt to close it.
• Solver package/version, QF_LIA theory, evidence schema, replay digest, witness order, and core-reduction order are unchanged.
• The five-second limit is an in-process bound, not hard process isolation against a compromised native Z3 library.
• This draft contains only the solver/satisfiability slice and does not alter or close fix(processor): fail loudly on z3 unknown in the satisfiability solver #1083.