Symbolic element alignment and slice length

Highlights

• Symbolic element alignment & slice length — generic T now uses a shared
  symbolic align_T (bound by the layout constraint sizeof_T % align_T == 0)
  and a materialized slice_len (size = slice_len · sizeof_T), making
  alignment and bounds reasoning precise for generic slice/array operations.
• Type invariants at return — the slice invariant
  (NonNull/Align/ValidNum/Allocated/Init) is established by
  init_parameters and re-proved at return, expressed via any(...) with DST
  slice fields.
• Precise InBound SMT — symbolic element sizes cancel the sizeof_T factor,
  and the slice bound is unified to index < len.
• Send/Sync auto-trait verification — Send modeled as
  any(NoRawPtr, TamedRawPtr) via struct invariants.
• DefId-based API classification — std APIs are classified by DefId (incl.
  lang items) instead of name matching, across multiple nightlies.
• Contract IR as a boolean AST — Property is now Atom | And | Or, with
  N-disjunct any(...) and NoPadding support.