Extract richer PySpec data: class hierarchy, kwargs, and assert preconditions

[joehendrix]

Summary

This PR extends the PySpec translator to handle richer Python constructs:
class inheritance with inner classes (exception hierarchies), **kwargs
parameter storage, and translation of assert statements into structured
SpecExpr preconditions. Six new DDM categories and a specWarning
method on PySpecMClass support round-trip serialization and non-fatal
diagnostics.

Details

• Class hierarchy support. ClassDef gains bases, fields,
  classVars, and subclasses fields. The translator now parses base
  class lists (resolving names to PythonIdent, special-casing
  Exception), field declarations (AnnAssign), class variable
  assignments (Assign), and inner ClassDef statements. A new
  ClassDecl DDM category with ClassFieldDecl and ClassVarDecl
  sub-categories provides serialization. FieldDecl is renamed to
  DictFieldDecl to disambiguate from ClassFieldDecl.
• **kwargs stored as a single typed parameter. ArgDecls gains a
  kwargs : Option (String × SpecType) field that preserves the parameter
  name and its type, rather than expanding TypedDict fields into
  individual kwonly args. A new KwargsDecl DDM category encodes this as
  a 0-or-1-element Seq, consistent with how DDM represents optionality
  elsewhere.
• Assert statements translated to SpecExpr preconditions. The old
  SpecPred placeholder is replaced by a SpecExpr inductive with
  constructors for six assert patterns: isinstance, len >=/<=,
  value >=/<=, and enum == chains. getIndex takes a recursive
  SpecExpr subject with a var base case, so nested subscripts like
  kwargs["ContactInformation"]["FullName"] can be represented when
  support is added later. Unrecognized patterns produce .placeholder
  with a specWarning including the full AST.
• DDM round-trip for new types. Six new DDM categories
  (ClassFieldDecl, ClassVarDecl, ClassDecl, KwargsDecl,
  SpecExprDecl, Assertion) with symmetric toDDM/fromDDM pairs.
  mkFunDecl now serializes kwargs, preconditions, and
  postconditions. FieldDecl renamed to DictFieldDecl.
• specWarning infrastructure. PySpecMClass gains a specWarning
  method so the translator can report non-fatal issues (skipped
  statements, unrecognized patterns) without aborting. Warnings are
  emitted to stderr at the end of translation.
• Bounded array access throughout. All array indexing in
  transAssertExpr and collectEnumValues uses decideProp or
  dependent if h : instead of forced [0]!/[1]!, letting the type
  checker verify bounds statically.
• Unit test for kwargs and preconditions. kwargs_function(**kw: str)
  with isinstance and valueGe asserts is added to main.py with
  corresponding expected DDM output in SpecsTest.lean.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.