Add PySpec-to-Laurel translation and method call dispatch

[joehendrix]

Summary

Enable end-to-end verification of Python programs that call AWS SDK methods by translating PySpec type stubs into Core prelude declarations and resolving method calls to the correct prelude procedures.

Details

PySpec-to-Laurel translation (Specs/ToLaurel.lean, new)

PySpec files describe Python library APIs as type signatures in Ion format. This PR adds a translator that converts those signatures into Laurel declarations (opaque procedures and composite types) which are then lowered to Core and merged into the verification prelude. This gives the verifier knowledge of library types and method signatures that were previously invisible.

The translator also builds an overload dispatch table — a map from factory function names to their string-literal-dispatched return types (e.g., boto3.client("iam") → AWSIdentityManagementV20100508). This is stored as a HashMap String (HashMap String PythonIdent) for O(1) lookup.

Types not yet supported in CorePrelude (e.g., typing.Any, bytes, Optional[float]) are mapped to TString via an unsupportedType placeholder, with TODO comments marking them for future CorePrelude additions.

Method call dispatch (PythonToLaurel.lean)

The Python-to-Laurel translator previously rendered all method calls (e.g., iam.get_role(...)) as pyExprToString, producing names like "iam_get_role" that never matched any prelude procedure — so every SDK call became a Hole (opaque havoc). This PR adds dispatch logic that:

1. Resolves factory calls via the dispatch table: matches boto3.client("iam") against the overload table and produces a New expression for the appropriate service type.
2. Resolves method calls on typed variables: looks up the variable's type in context, constructs the correct prelude procedure name (e.g., AWSIdentityManagementV20100508_get_role), and prepends the object as the self argument.
3. Falls back to a static call by flattened name for unrecognized calls.

All three steps live inside translateCall, which takes the raw Python call expression directly. The .Call arm in translateExpr is a single delegation to translateCall.

AnnAssign dispatch fallback: Python type-stub names (e.g., IAMClient) don't match PySpec service names (e.g., AWSIdentityManagementV20100508). When an AnnAssign annotation resolves to PyAnyType and the initializer is a dispatched factory call, the translator falls back to the dispatch table to infer the correct UserDefined type. This ensures subsequent method calls on the variable resolve correctly.

Unrecognized type annotations in Python source are mapped to TString via pyUnsupportedType, allowing translation to proceed without modifying the CorePrelude.

CLI integration (StrataMain.lean)

• pyAnalyzeLaurel --pyspec <ion_file> translates PySpec files and merges them into the Core prelude before verification.
• pyAnalyzeLaurel --dispatch <ion_file> extracts only the overload dispatch table (no Laurel translation) for lightweight factory-call resolution.
• pySpecToLaurel command for standalone PySpec-to-Laurel inspection.
• buildPySpecPrelude handles the multi-file merge pipeline with name collision detection.

PySpec infrastructure (Specs/Decls.lean, Specs.lean, Specs/DDM.lean)

• Inhabited instance added to PythonIdent (needed for HashMap default values).
• TypedDict fields changed from isTotal : Bool to per-field fieldRequired : Array Bool to support Required[T]/NotRequired[T] annotations.
• Support for Unpack[TypedDict] in **kwargs expansion.

Testing

ToLaurelTest.lean adds 15 #guard_msgs tests covering the PySpec-to-Laurel translation: primitive and complex type mapping, optional type patterns (Union[None, T]), literal and TypedDict types, class/type definitions, void returns, error cases (unknown types, empty types, unsupported unions), overload dispatch with both extern and local class return types, extractOverloads filtering, and a regression test for externTypeDecl.

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

[ssomayyajula]

The logic to translate PySpec to Laurel (in particular, of classes to composites with instance procedures) looks good to me. The only thing that concerns me is how the translation handles static dispatch. By building a dispatch table for methods overloaded on the Python side, the Python->Laurel translator seems to be doing type checking work that it shouldn't have to do / wouldn't already be resolved by assuming maximal type annotation of the input file.

That is, I'd rather see:

• PySpec -> Laurel build the typing environment not just from local variables and function parameters, but also module-level declarations: this would catch type annotations on instance variables of a class.
• As a result, statically resolving the type of boto3.client(s) would just be a matter of (1) looking up the type annotated on the enclosing declaration/assignment and (2) construct the monomorphized method name as is already done in this PR.

EDIT: I see that you attempt to resolve a method call first by type annotation and then by look up in the dispatch table...I think this is fine in isolation, but it is separately a bad thing that stub names and PySpec service names don't match sometimes. It seems to be a symptom of out-of-date stubs: if that were resolved, would you still need to build a dispatch table? Or would you want to keep this functionality anyway?

[joehendrix]

Hi Siva, you are right. If every assignment is annotated or inferable from class definitions (for cases like self.client = static_method('service_name')) and there is consistency between the class names in PySpec and user annotations, then the static dispatch code may not be needed.

Currently neither really seems to be the case, so I'd like to unblock this. I think it's better to try to get things working now then postpone for future changes.

[andrewmwells-amazon]

Currently neither really seems to be the case, so I'd like to unblock this. I think it's better to try to get things working now then postpone for future changes.

Agreed. It should be easy to remove this in the future if we reach a point where it's not needed. One thing I could see doing is raising a warning if we find an inconsistency (but that can be a future PR).

[ssomayyajula]

Sounds good to me!