fix(verifier): symbolic Seq encoding treats out-of-range head() as defined, disagreeing with concrete engines

[rizumita]

Problem

Found by the #648 C6 typed-agreement suite (recorded there as a self-retiring exclusion, re-measured every run): a partial Seq read (head()) evaluated in property context on an empty sequence disagrees across engines, and BMC's side of the disagreement is a plausible-looking verdict built on a phantom value.

Minimal reproduction (from rust/fslc/tests/typed_agreement/relations.rs::r6_property_context_seq_head_disagrees_across_engines_self_retiring_exclusion):

spec R6HeadPropertyDisagreement {
  type Item = 0..2
  state { queue: Seq<Item, 2> }
  init { queue = Seq {} }
  action stay() { queue = queue }
  invariant HeadRead { queue.head() >= 0 }
}

Observed (re-measured on every suite run):

• fsl_runtime::bfs / fsl_runtime::verify_explicit: raw RuntimeError ("head() on empty sequence") — no verdict. Monitor::current_violation[_selected], unlike Monitor::execute_selected's post-step check, does not catch is_partial_operation_error and convert it to a partial_op violation.
• fsl_verifier::verify_bounded: returns a verdict — violated, kind:"invariant" (not partial_op), name:"HeadRead", step:0. The symbolic Seq encoding treats head() on an empty sequence as defined, with a solver-chosen value that can lie outside Item's own 0..2 bound.

Why this is more than a labeling difference

The solver being free to pick a phantom value cuts both ways: here it produces a spurious violated, but the same freedom can satisfy a reachable witness or falsify an invariant's negation — i.e. a false green on the other polarity. LANGUAGE.md §3 documents property-context totalization for / and % only; it makes no such promise for head/pop/at/index, and neither engine family currently implements a consistent contract for them in property context.

The same symbolic-Seq gap surfaces in action context as three different shapes (recorded, not asserted, in relations.rs::r6_action_context_partial_operations_are_caught_only_by_the_concrete_engines): clean verdict (divide/remainder — those are checked concretely elsewhere), spurious type_bound on the assigned scalar (head/at/index), and verify_bounded returning Err("model sequence length is negative") (pop).

What the fix must decide

A contract decision before code: either (a) property-context partial Seq reads become a defined totalization documented in LANGUAGE.md (like //%), implemented identically in Monitor/explicit/BMC, or (b) they are uniformly rejected/classified (partial_op or a check-time error) by all engines. Cross-path invariant: symbolic and concrete evaluation must agree on definedness for every partial operation in every context — the #648 suite's exclusion self-retires the day they do.

Refs

#648 (suite + exclusion), #537 C6/C1, docs/DESIGN-conformance-harness.md "Two confirmed findings", LANGUAGE.md §3 (Euclidean totalization is //%-only)