vera lsp now serves the four standard features, all computed by pure
backing functions in vera/lsp/features.py over one Analysis bundle
(parse -> typecheck-with-artifacts -> warm incremental verify), with
all verification serialised through the server's single
VerificationSession under a lock (Z3 contexts are not thread-safe).

- publishDiagnostics on didOpen/didChange: parse/transform errors
  (single-diagnostic short-circuit, matching the CLI), type-check
  diagnostics, verification diagnostics, plus a synthesised
  per-function verification-tier Hint computed from the obligation
  stream (decision R3: the verifier stays silent about successes; the
  Hint is LSP-layer presentation — 'fn: Tier 1 — all contracts proven
  by Z3' / 'Tier 3 — N of M obligations fall back to runtime checks';
  suppressed for functions with violated obligations). didClose
  clears squiggles.
- Hover: type of the smallest recorded expression span under the
  cursor, from the new checker side-table.
- Definition: @T.n -> the parameter it names via slots.slot_table
  (De Bruijn most-recent-first); indices binding through let/match
  return None (documented signature-level scope; #181 owns full
  binding resolution).
- Completion: at a typed hole (or immediately after it), the in-scope
  bindings with their types, innermost first; '?' added as a trigger
  character.

Checker (#222 Phase D artifacts, decision R4 — opt-in, zero cost for
existing callers):
- typecheck_with_artifacts() returns (diagnostics, CheckArtifacts)
  with a Span->pretty-type side-table and structured HoleSite records.
- _synth_expr is now a thin recording wrapper over _synth_expr_impl
  (the dispatcher; walker-coverage marker travels with it — checker
  verified green), so every synthesis including recursion is recorded.
- _check_hole's binding collection factored into
  _collect_scope_bindings(), shared by the W001 fix hint and the LSP
  completion payload.

Tier plumbing:
- Diagnostic gains tier: int | None (surfaced in to_dict() only when
  set — schema-additive); the verifier's six Tier-3 fallback warnings
  (E520-E525) now carry tier=3; the LSP diagnostic puts it in data.

Tests (tests/test_lsp.py 30 -> 44): parse-error path, type-error
short-circuit, tier in diagnostic data, tier-Hint synthesis +
violated-suppression, hover (smallest span / off-expression / parse
error), definition (most-recent-parameter jump, out-of-range None,
off-slot None), hole completion (inside/after/away).

Validation: mypy strict clean (68 files), ruff S clean, 978 adjacent
suite tests green (obligations + verifier + checker + errors), doc
counts consistent (4,264 tests).

Part of #222 (Phase D). Release prep follows before the PR.

Co-Authored-By: Claude <noreply@anthropic.invalid>

…und 1)

CodeRabbit round 1 (valid, Major): definition_at bound 'enclosing' to
the first top-level FnDecl whose subtree contained the cursor, so a
slot inside a where-block function jumped to the OUTER function's
parameter list. Now the innermost FnDecl containing the cursor (by
smallest span) wins, and the SlotRef is located within it. New test
pins a where-block helper: the slot jumps to helper's signature line,
not outer's.

Co-Authored-By: Claude <noreply@anthropic.invalid>

CodeRabbit round 2 (valid): the test was appended at the file tail,
which placed it inside TestHoleCompletion. It validates definition_at
and now sits with the other definition tests. No logic changes.

Co-Authored-By: Claude <noreply@anthropic.invalid>