feat: VCOutcome uses unknown instead of sat for unvalidated SMT results

[MikaelMayer]

When the SMT solver returns "sat", it does not necessarily mean the property is truly satisfiable — uninterpreted functions may admit spurious models. This PR makes VCOutcome sound by treating unvalidated SMT "sat" results as "unknown" until counter-example validation is implemented.

Changes:

• Result.unknown now carries an optional candidate model (candidateModel : Option (CounterEx Ident)), distinguishing between an empty model (some []) and no model available (none). This allows unknown results to preserve counterexample data for future validation while clarifying that the model is unverified.
• SolverPhaseLog is a structure with phase : String and result : SMT.Result fields, so each log entry is labeled with the pipeline phase that produced it. VCOutcome gains a solverLog : List SolverPhaseLog field — an ordered list recording both the raw solver results (labeled solver.sat / solver.val) and per-phase adjusted results, for future diagnostic and traceability tooling.
• In the verification pipeline, every SMT "sat" result that we can't reliably validate is converted to "unknown" (with the model attached). The ways we know a SMT "sat" is preserved is that
  • There was no procedure eliminated from the entry of the procedure to the assertion point
  • There was no loop eliminated from the entry of the procedure to the assertion point.
  • For front-end, by default "sat" is not preserved until they implement a validation procedure, as front-ends might encode functions with uninterpreted functions.
• PipelinePhase structure couples each program-to-program transformation with its AbstractedPhase (model validation), ensuring transforms and their soundness annotations stay in sync. Each AbstractedPhase carries a name field that flows into the solver log. corePipelinePhases is the single parameterized function that drives both the pipeline and the validation — it accepts the target procedure list and factory, and returns the full pipeline including filtering, call/loop elimination, precondition elimination, and the final keep-set filter. coreAbstractedPhases is derived from it via .map (.phase).
• All filter phases (FilterProcedures, keep-set filter) and PrecondElim are explicit pipeline phases marked as model-preserving, since they only remove procedures or add new assertions without introducing over-approximations.
• Pipeline phase types (ModelValidation, AbstractedPhase, PipelinePhase, obligationHasLabelPrefix, modelPreservingPipelinePhase) are defined in Strata/Languages/Core/PipelinePhase.lean. Each transform pass defines its own pipeline phase next to its implementation: callElimPipelinePhase in CallElim.lean, loopElimPipelinePhase in LoopElim.lean, filterProceduresPipelinePhase in FilterProcedures.lean, and precondElimPipelinePhase in PrecondElim.lean.
• Label prefixes used by call elimination (callElimAssertPrefix, callElimAssumePrefix) are defined in CallElim.lean. createAsserts/createAssumes accept a labelPrefix parameter, decoupling the generic helpers from the call-elimination-specific prefixes.
• loopElimPipelinePhase is placed last in the pipeline because loop elimination happens during evaluation (not as a program-to-program pass), making it the closest phase to SMT.
• Phase validation is non-cascading: each phase with modelToValidate independently validates the model, regardless of whether the current result is .sat or .unknown. A phase can demote .sat m to .unknown (some m) (when the model fails validation) or promote .unknown (some m) back to .sat m (when the model passes validation against the pre-phase semantics). Phases without a validator (modelPreserving) pass results through unchanged. When no candidate model is available (.unknown none), validation is skipped.
• In bug-finding modes (bugFinding and bugFindingAssumingCompleteSpec), unreachable assertions are now errors instead of warnings. Dead code in bug-finding contexts signals a specification or implementation problem. Added docs/VerificationModes.md documenting the three verification modes and their error classification, referenced from the README (in the "Running Analyses" section, after lake exe strata verify is introduced).
• Extracted unreachableMsg helper to deduplicate the check-mode/property match pattern in VCOutcome.label and VCOutcome.emoji.
• Per-pass obligation tests live next to their transforms: StrataTest/Transform/CallElim.lean and StrataTest/Transform/LoopElim.lean.

Test expectations updated to reflect the new behavior. Note that in many cases in Core, we keep "sat" unchanged. It's only changing what the front-end receive.

Fixes #721

[aqjune-aws]

Thanks. Adding the name field to AbstractedPhase seems to make sense to me. :)