fix(processor): enforce solver deadline boundaries

[Brad-Edwards]

Summary

Complete the operation-wide solver deadline introduced by #1127.

• start the monotonic budget at solve_model() entry so model validation and budget derivation count toward the governed timeout
• checkpoint after validation before solver construction
• checkpoint result selection immediately before returning SAT or UNSAT evidence
• reject evidence when validation or final witness materialization reaches the deadline

Context

Follow-up to #1127. This closes the remaining deadline-boundary gap in the work for #1108 and #1114.

Closes #1108
Closes #1114

Verification

• focused satisfiability suite: 32 passed
• full unit lane: 6480 passed, 1 skipped
• integration lane: 57 passed, 2 skipped
• contracts, static checks, documentation, Ruff, and repository policy passed
• completion gate reached the known local-only participant-opacity proof prerequisite; the pinned Isabelle archive is not installed in this worktree

Compatibility

No schema, solver configuration, witness ordering, core reduction, or public API changes.