Phase A of the LSP / obligation-core plan on #222: obligations become
first-class records and a long-lived session reuses one z3.Solver
across a whole program. Behavior-preserving by construction and by
test: reification is observational (records created at the existing
discharge sites, in discharge order, never altering solver state), and
the new differential oracle pins warm == cold across the full corpus.

New package vera/obligations/:
- core.py: ProofObligation dataclass — identity (fn, kind, expr text,
  span, content_key() sha256 digest) + outcome (status, counterexample,
  error code). Kinds: requires / ensures / decreases / nat_sub /
  call_pre. Status vocabulary mirrors the verifier's tier bookkeeping
  (verified <-> tier1; tier3+timeout <-> tier3_runtime; violated <->
  error diagnostic, excluded from totals).
- session.py: VerificationSession — the Phase A daemon object. Owns one
  SmtContext lazily; verify_source() runs parse -> typecheck ->
  ContractVerifier(shared_smt=...) with reset() between functions and
  ADT-registry resync between programs; caches last_program for Phase
  B's diffing. Single-file project model (imports resolve from disk);
  not thread-safe by design (Phase D serialises through one worker).
- __init__.py: core exported eagerly; session symbols lazily via PEP
  562 to break the verifier <-> session import cycle.

vera/verifier.py:
- VerifyResult gains obligations (default empty — source-compatible).
- ContractVerifier gains shared_smt hook; cold path (None) is
  byte-identical to before: fresh SmtContext per function.
- All six discharge sites record obligations: generic-fn early return
  (E520), requires (assumed; E521 fallback), ensures (E522/E523
  fallbacks, E524 timeout, violations with counterexample), decreases
  (E525 fallback), @Nat-@Nat sites (E502 violations), call-site
  precondition violations (Phase A records call_pre only on violation;
  successful call-pre checks discharge silently inside the SMT layer's
  _translate_call — enumerating successes is a Phase B extension).

vera/smt.py:
- reset() hardened for actual use (it previously had zero callers):
  now also clears _path_conditions, _index_fns, _array_element_sorts,
  and _length_fns (re-seeded with the Int default), and re-applies the
  solver timeout. The _length_fns clear is load-bearing: get_rank_fn
  asserts its ForAll rank(x) >= 0 axiom only at dict-miss, so a
  surviving cache entry after solver.reset() would silently skip the
  axiom and ADT-measure decreases checks would diverge warm-vs-cold.
  Found by inspection while wiring the warm path; pinned by the oracle.

tests/test_obligations.py (250 tests):
- Differential oracle: warm VerificationSession == cold verify() on
  diagnostics (content + order), summary (field-for-field), and the
  obligation stream (identity + outcome), plus warm-twice determinism,
  parametrized over all 35 examples and every verify/run-level
  conformance program.
- Summary <-> obligation consistency on every corpus program.
- Unit tests per kind/status: violated ensures carries counterexample;
  violated nat_sub carries E502; generic-fn contracts fall to tier3
  with E520; trivial contracts enumerate as verified; content keys are
  stable across runs and distinguish identical text at two sites;
  session reuses one solver, caches last_program, short-circuits on
  type errors, and resyncs the ADT registry between programs.

Existing suites pass unchanged (hard rail): test_verifier.py +
test_verifier_coverage.py 237/237. mypy strict clean (62 files).
Doc counts updated (3,961 -> 4,211 tests; 32 -> 33 files; new
TESTING.md row); site assets regenerated.

Part of #222 (Phase A). Release prep and PR follow in the next commit.

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

Two findings, both valid:

- ruff S110 (security lint, CI lint job): expr_text_for wrapped
  format_expr in try/except-pass as a defensive guard. format_expr is
  total (it ends in a '<expr>' fallback), so the guard was dead code —
  removed it rather than noqa'ing it. The class-name fallback stays for
  the non-Expr contract shape (Invariant, #686, which never reaches the
  function-contract path today).

- CodeRabbit (Major): call_pre obligations were keyed on the callee's
  contract node, so two call sites violating the same precondition
  inherited the contract's span and collapsed to one content_key —
  breaking Phase B cache identity — and dropped the E501 code that
  _report_call_violation emits. _record_obligation gains a span_node
  override; call_pre now records the CALL SITE span, the callee's
  contract text, and error_code=E501. New test pins the scenario: two
  violating calls -> two obligations, same expr_text, distinct
  content_keys, both E501, spans at the caller not the contract.

Validation: ruff S clean, mypy clean (62 files), 251 obligation tests +
237 hard-rail verifier tests green, doc counts updated (4,212).

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

CodeRabbit round 2 (valid): the call-site keying test asserted only
relational properties (texts equal each other, line != 2), which an
incorrect mapping could still satisfy. Now pins the exact rendered
contract text ('@Int.0 > 0' — format_expr renders bare, without the
backticks CodeRabbit's suggested diff guessed), the exact caller line
(14) for both obligations, and distinct columns for the two call sites.

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