fix(processor): enforce solver deadline boundaries

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

@@ -96,21 +96,26 @@ class SolverResult:
 def solve_model(model: NormalizedConstraintModel) -> SolverResult:
     """Solve one normalized model and select deterministic portable evidence."""
 
+    started_ns = _monotonic_ns()
+    budget = _solver_check_budget(model, started_ns=started_ns)
     _require_unique_clause_ids(model)
     all_clause_ids = tuple(clause.clause_id for clause in model.clauses)
-    budget = _solver_check_budget(model)
+    budget.checkpoint("model-validation", check_count=budget.checks_used)
     session = _SolverSession(model, budget)
     # ``_check`` fails loudly on ``z3.unknown``, so a non-satisfiable decision
     # here is decisively unsatisfiable rather than an incomplete timeout.
     if session.check(all_clause_ids, {}, phase="initial-decision") == z3.sat:
-        return SolverResult(
+        result = SolverResult(
             outcome=SatisfiabilityOutcome.SATISFIABLE,
             assignment=_select_witness(model, all_clause_ids, session),
         )
-    return SolverResult(
-        outcome=SatisfiabilityOutcome.UNSATISFIABLE,
-        core=_reduce_unsat_core(all_clause_ids, session),
-    )
+    else:
+        result = SolverResult(
+            outcome=SatisfiabilityOutcome.UNSATISFIABLE,
+            core=_reduce_unsat_core(all_clause_ids, session),
+        )
+    budget.checkpoint("result-selection", check_count=budget.checks_used)
+    return result
 
 
 def _require_unique_clause_ids(model: NormalizedConstraintModel) -> None:
@@ -125,12 +130,19 @@ def _require_unique_clause_ids(model: NormalizedConstraintModel) -> None:
         )
 
 
-def _solver_check_budget(model: NormalizedConstraintModel) -> _CheckBudget:
+def _solver_check_budget(
+    model: NormalizedConstraintModel,
+    *,
+    started_ns: int | None = None,
+) -> _CheckBudget:
     """Bound the two possible finite algorithms without a second profile knob."""
 
     witness_checks = sum(len(symbol.domain) for symbol in model.symbols)
     core_checks = len(model.clauses)
-    return _CheckBudget(max_checks=1 + max(witness_checks, core_checks))
+    return _CheckBudget(
+        max_checks=1 + max(witness_checks, core_checks),
+        started_ns=_monotonic_ns() if started_ns is None else started_ns,
+    )
 
 
 def _select_witness(

implementations/python/tests/test_scenario_satisfiability.py

@@ -655,7 +655,7 @@ def test_published_maximum_witness_shape_has_a_finite_derived_budget() -> None:
 
 
 def test_operation_deadline_covers_model_construction(monkeypatch: pytest.MonkeyPatch) -> None:
-    clock = iter((0, SOLVER_TIMEOUT_MS * 1_000_000))
+    clock = iter((0, 0, SOLVER_TIMEOUT_MS * 1_000_000))
     monkeypatch.setattr(solver_adapter.time, "monotonic_ns", clock.__next__)
     model = _normalized_model([1], [[]])
 
@@ -667,6 +667,26 @@ def test_operation_deadline_covers_model_construction(monkeypatch: pytest.Monkey
     assert raised.value.reason == "operation-deadline-exhausted"
 
 
+def test_operation_deadline_starts_before_model_validation(monkeypatch: pytest.MonkeyPatch) -> None:
+    clock = {"now": 0}
+    original_validation = solver_adapter._require_unique_clause_ids
+
+    def validation_finishing_at_deadline(model: NormalizedConstraintModel) -> None:
+        original_validation(model)
+        clock["now"] = SOLVER_TIMEOUT_MS * 1_000_000
+
+    monkeypatch.setattr(solver_adapter.time, "monotonic_ns", lambda: clock["now"])
+    monkeypatch.setattr(solver_adapter, "_require_unique_clause_ids", validation_finishing_at_deadline)
+    model = _normalized_model([1], [[]])
+
+    with pytest.raises(SolverOperationalError, match="operation deadline exhausted") as raised:
+        solve_model(model)
+
+    assert raised.value.phase == "model-validation"
+    assert raised.value.check_count == 0
+    assert raised.value.reason == "operation-deadline-exhausted"
+
+
 def test_result_returned_after_operation_deadline_is_rejected(monkeypatch: pytest.MonkeyPatch) -> None:
     clock = {"now": 0}
     original_check = z3.Solver.check
@@ -686,3 +706,28 @@ def complete_after_deadline(self: z3.Solver, *assumptions: object) -> z3.CheckSa
     assert raised.value.phase == "initial-decision"
     assert raised.value.check_count == 1
     assert raised.value.reason == "operation-deadline-exhausted"
+
+
+def test_result_selection_finishing_at_operation_deadline_is_rejected(monkeypatch: pytest.MonkeyPatch) -> None:
+    clock = {"now": 0}
+    original_selection = solver_adapter._select_witness
+
+    def selection_finishing_at_deadline(
+        model: NormalizedConstraintModel,
+        all_clause_ids: tuple[str, ...],
+        session: solver_adapter._SolverSession,
+    ) -> dict[str, str | int | bool]:
+        assignment = original_selection(model, all_clause_ids, session)
+        clock["now"] = SOLVER_TIMEOUT_MS * 1_000_000
+        return assignment
+
+    monkeypatch.setattr(solver_adapter.time, "monotonic_ns", lambda: clock["now"])
+    monkeypatch.setattr(solver_adapter, "_select_witness", selection_finishing_at_deadline)
+    model = _normalized_model([1], [[]])
+
+    with pytest.raises(SolverOperationalError, match="operation deadline exhausted") as raised:
+        solve_model(model)
+
+    assert raised.value.phase == "result-selection"
+    assert raised.value.check_count == 2
+    assert raised.value.reason == "operation-deadline-exhausted"