docs: Create developer guide for Python, remove leading whitespace from designs folder name

designs/codegen/python/design-codegen.md

@@ -0,0 +1,67 @@
+# Concepts
+
+## Differences between Smithy-Dafny Python projects and other languages
+
+### Interpreted vs. Compiled
+
+Languages like Java and .NET are compiled, but Python is interpreted. This results in some important differences in Python:
+
+1. Python imports modules based on filepath.
+   If a module is located at `my_project/internaldafny/generated/SomeModule.py`, it must be imported as `my_project.internaldafny.generated.SomeModule`. (There are some hacks to work around this, but these are hacks.)
+   This contrasts with Java/.NET, which import modules based on declared namespace. (ex.) Java might have a file at `dafny-generated/SomeModule/SomeClass.java` , but that class declares `package SomeModule` . To import this class, you would write `import SomeModule.SomeClass`.
+2. Python links externs to generated code at runtime.
+   When a Dafny-Python module is imported, it runs initialization glue code that will 1) import all of its generated Dafny (in a topological order to avoid circular dependencies), 2) import all of its externs.
+   Then, each extern class must 1) extend the generated class, 2) override the generated class with the extern class.
+   This contrasts with Java/.NET, where the externs extend partial/base generated classes, and link together at compile time.
+
+## Smithy-Python Integration
+
+### Smithy-Python “Hard Fork”
+
+Smithy-Dafny relies on a “hard fork” of Smithy-Python.
+
+Alternatives rejected include:
+
+- **Submodule; create a regular fork of Smithy-Python.**
+  - `smithy-lang` can’t create its own fork of Smithy-Python because `smithy-lang/smithy-python` is the real Smithy-Python
+  - It would be improper to add some prefix/suffix to make the names not collide because `smithy-lang` is a shared AWS resource, and doing this would pollute the org’s repositories
+  - It would be improper to have Smithy-Dafny reference some other owner’s fork of Smithy-Python because both projects are under `smithy-lang`.
+- **Submodule; create a non-main branch on Smithy-Python**. This would add churn to Smithy-Dafny’s development process. Developers would need to get a change reviewed by the Smithy-Python team before they can deploy a change through Smithy-Dafny. It would also be improper to refer to a non-main branch.
+
+### Smithy-Dafny code integration with Smithy-Python
+
+Smithy-Dafny generates Python code by integrating with [Smithy-Python](https://github.com/smithy-lang/smithy-python/tree/develop/codegen).
+Smithy-Dafny integrates with Smithy-Python via two integration mechanisms:
+
+1. Smithy’s [plugin Integration](https://smithy.io/2.0/guides/building-codegen/making-codegen-pluggable.html) interface. This is used by code in a protocol’s `customize/` directory. See [LocalService’s customize directory](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/customize) as an example.
+   Codegen that uses this integration includes:
+   1. Override the HTTP protocol in Smithy-Python and generate protocols for local services, wrapped local services, and Dafny AWS SDK shims
+   2. Write custom content to some files from the `customize` directive
+2. Extending Smithy-Python classes and overriding its methods. This is used by code in a protocol’s `extensions/` directory. See [LocalService’s extensions directory](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/extensions) as an example.
+   Codegen that uses this integration includes:
+   1. Overriding Smithy-Python’s client class generation to generate a synchronous client
+   2. Overriding Smithy-Python’s shape writer to handle Smithy-Dafny-specific shapes (Positional shapes, Reference shapes, etc)
+
+Smithy-Dafny’s Python integration uses both mechanisms, but could probably be refactored to only use one or the other. A refactor to only extend Smithy-Python’s classes would be lower-lift than only implementing the plugin interface. There isn’t a pressing need to do this refactor, other than simplification.
+
+#### **Limitations of the Plugin Interface**
+
+The plugin interface has some gaps that prevent Smithy-Dafny’s Python codegen from exclusively using it. This is a non-exhaustive list:
+
+1. **Doesn’t support changing shape generation.** Smithy-Python doesn’t recognize certain shapes, like shapes with Positional and Reference traits. (We wouldn’t expect it to; these are Smithy-Dafny-specific traits.) The plugin interface doesn’t let a plugin override a codegen’s shape generation to change how shapes are generated.
+2. **Doesn’t support changing symbol generation.** Smithy-Python doesn’t understand how to generate references to symbols in other namespaces (what Smithy-Dafny calls “Dependencies”). The plugin interface doesn’t let a plugin override a codegen’s symbol generation to change how shapes are referenced.
+3. **Doesn’t support overriding client generation.** Smithy-Python generates an async client, while Smithy-Dafny-Python requires a synchronous client. The plugin interface doesn’t let a plugin override a codegen’s client generation.
+4. **Protocols without shapes.** Smithy-Dafny generates shims for AWS SDKs and wrapped local services. These protocols don’t require shape generation. Smithy-Python always generates all shapes it visits.
+
+The workarounds to these involve extending Smithy-Python’s classes to work around these limitations.
+
+#### **Extending Smithy-Python’s implementation**
+
+Where Smithy-Dafny directly extends Smithy-Python, it prefers to do so by modifying access levels in Smithy-Python (e.g., making private methods protected or public), or by refactoring to introduce a new method that can be overridden via class extension.
+
+This appears to be discouraged by Smithy. Smithy code generators tend to declare classes as `private` and/or `final` , suggesting class extensions aren’t preferred.
+
+#### Future Work
+
+1. Upstreaming changes from Smithy-Dafny’s Smithy-Python fork; relying on Smithy-Python upstream
+   1. This should probably wait until Smithy-Python’s interfaces are finalized. Right now, Smithy-Python notes “WARNING: All interfaces are subject to change”. It might cause unneeded churn to integrate with Smithy-Python more closely now if Smithy-Dafny needs to update again later.

docs/getting-started.md

@@ -0,0 +1,15 @@
+# Makefile Variables
+
+To create a Smithy-Dafny project, you will need a Makefile with the following variables defined.
+These variables apply to all languages.
+Some languages have additional required variables.
+
+- `PROJECT_SERVICES`: List of names of each local service in the project.
+- `PROJECT_INDEX`: This is a space-delimited list of `Index.dfy` files for your dependencies.
+- `PROJECT_DEPENDENCIES`: List of top-level directory names for dependencies for the project.
+- `SERVICE_NAMESPACE_<service>`: For each service in `PROJECT_SERVICES`, this is the Smithy namespace for shapes attached to that local service.
+- `SERVICE_DEPS_<service>`: For each service in `PROJECT_SERVICES`, this is the list of paths to `Model/` directories for dependencies of that service.
+
+Examples:
+
+- [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsCryptographicMaterialProviders/Makefile). This project sets all of these variables with multiple dependencies.

docs/nested-externs.md

@@ -0,0 +1,78 @@
+#### Modules with “nested” extern attributes
+
+The content in this file is relevant for Smithy-Dafny Python and Go projects.
+
+Modules with a “nested” extern attribute (“nested extern modules”) can’t be used with Python or Go.
+A "nested" extern attribute has `.`s in it. (e.g. `{:extern "my.namespace.my.project.internaldafny}`).
+
+Ideally, one wouldn’t define nested extern modules.
+However, some projects that build for Java, NET, and Rust use nested extern attributes to prefix generated Dafny code with an "internal" prefix.
+For legacy support, Smithy-Dafny supports using `sed` to strip away the nested extern attribute.
+
+**Simple “nested” externs**
+For an existing project `MyProject` that uses a nested extern string like `"my.namespace.my.project.internaldafny"` , the Makefile for the project should be updated as follows:
+
+```
+ENABLE_EXTERN_PROCESSING=1  # This MUST go before `include ``../``SharedMakefileV2``.``mk
+
+include ../SharedMakefileV2.mk`
+
+...
+
+TYPES_FILE_PATH=Model/MyProject.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"my.namespace.my.project.internaldafny.types\" } MyProjectTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module MyProjectTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"my.namespace.my.project.internaldafny\" } MyProject refines AbstractMyProjectService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module MyProject refines MyProject {"
+```
+
+This setup will work for “simple” projects that only define nested extern modules in `Index.dfy` and the types file.
+
+Examples:
+
+- [Constraints TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/Constraints/Makefile). Almost all TestModels are “simple.”
+- [DDB TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/aws-sdks/ddb/Makefile). All AWS SDK projects should be simple.
+
+**Complex “nested” externs**
+Some projects use nested extern modules in files other than `Index.dfy` and the types file.
+For these “complex” projects, you will need to define new sed strings _and_ override the default Makefile targets.
+If you have a file `MySpecialFile.dfy` that requires sed replacement, you will need to override some targets:
+
+```
+ENABLE_EXTERN_PROCESSING=1
+
+...
+
+MY_SPECIAL_FILE_FILE_PATH=src/MySpecialFile.dfy
+MY_SPECIAL_FILE_WITH_EXTERN_STRING="module {:extern \"my.namespace.my.special.file.internaldafny\" } MySpecialFile"
+MY_SPECIAL_FILE_WITHOUT_EXTERN_STRING="module MySpecialFile"
+
+...
+
+# Override target; handle both the Index.dfy file and the new file
+_sed_index_file_add_extern:
+    $(MAKE) _sed_file SED_FILE_PATH=$(MY_SPECIAL_FILE_FILE_PATH) SED_BEFORE_STRING=$(MY_SPECIAL_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(MY_SPECIAL_FILE_WITH_EXTERN_STRING)
+    $(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITH_EXTERN_STRING)
+
+_sed_index_file_remove_extern:
+    $(MAKE) _sed_file SED_FILE_PATH=$(MY_SPECIAL_FILE_FILE_PATH) SED_BEFORE_STRING=$(MY_SPECIAL_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(MY_SPECIAL_FILE_WITHOUT_EXTERN_STRING)
+    $(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING)
+```
+
+Examples:
+
+- [MultipleModels TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/MultipleModels/Makefile). Any Smithy-Dafny project with multiple local services is “Complex.”
+- [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsCryptographicMaterialProviders/Makefile). This project has multiple local services, but also applies nested extern attributes to some of its other modules (SynchronizedLocalCMC and StormTrackingCMC).
+
+The following Makefile targets exist and can be overridden:
+
+```
+_sed_types_file_remove_extern
+_sed_index_file_remove_extern
+_sed_wrapped_types_file_remove_extern
+_sed_types_file_add_extern
+_sed_index_file_add_extern
+_sed_wrapped_types_file_add_extern
+```

docs/python/getting-started.md

@@ -0,0 +1,158 @@
+# Getting Started
+
+To install dependencies to build a Smithy-Dafny project in Python, first run
+
+```
+make setup_python
+```
+
+# Makefile Variables
+
+To build a Smithy-Dafny Python project, you will need to add the following variables to your Makefile.
+
+- `PYTHON_MODULE_NAME`: The name of the Python module for generated code.
+- `TRANSLATION_RECORD_PYTHON` : For each dependency (including StandardLibrary), the path to the generated `.dtr` file for that dependency’s generated Dafny code.
+- `PYTHON_DEPENDENCY_MODULE_NAMES`: For each dependency, this is a map from a Smithy namespace to the `PYTHON_MODULE_NAME` variable for that dependency.
+
+Examples:
+
+- [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsCryptographicMaterialProviders/Makefile). This project sets all of these variables with multiple dependencies.
+
+### Smithy-Dafny Python Project Structure
+
+(Assuming you have made the Makefile updates specified above, then:)
+
+These commands will set up the base file structure for a Python project:
+
+1. `make polymorph_dafny`
+2. `make polymorph_python`
+3. `make transpile_python`
+
+This structure follows:
+
+```
+MyProject/runtimes/python/
+├── src/
+│   └── my_project/
+│       ├── __init__.py
+│       ├── internaldafny/
+│       │   ├── generated/
+│       │   │   ├── [all Dafny-generated source code from `make transpile_python`]
+│       │   │   └── dafny_src-py.dtr
+│       │   └── extern/
+│       │       ├── __init__.py
+│       │       └── [all manually written externs]
+│       └── smithygenerated/
+│           └── my_project/
+│               └── [all Smithy-Dafny-generated source code from `make polymorph_python`]
+├── test/
+│   ├──  __init__.py  # empty
+│   └── internaldafny/
+│       ├── __init__.py  # empty
+│       ├── test_dafny_wrapper.py
+│       ├── generated/
+│       │   ├── [all Dafny-generated test code from `make transpile_python`]
+│       └── extern/
+│           ├── __init__.py
+│           └── [all manually test written externs]
+├── pyproject.toml
+├── tox.ini
+└── .gitignore
+```
+
+- `src/` : Project source code.
+  - `my_project/` : Python module that will be distributed to end users. This is the top-level name of the package that is imported by users. (ex. `import my_project`). The top-level name is defined by the Smithy-Dafny project’s Makefile’s `PYTHON_MODULE_NAME` variable; see [Makefile Updates](https://quip-amazon.com/SahBABLOQkya#temp:C:KIXe7b270945e2b419180867c04e).
+    - `__init__.py`: Initializes generated Dafny code and performs optional project setup. See Appendix.
+    - `internaldafny/`: Dafny-generated code and externs.
+      - `generated/`: Dafny-generated code.
+        - `dafny_src-py.dtr`: [Dafny translation record](https://dafny.org/dafny/DafnyRef/DafnyRef#sec-dtr-files) for this project’s generated code. This is critical to let other projects use this project as a dependency. Other projects will read this file to determine how to refer to this project’s generated Dafny code.
+      - `extern/`: Holds manually-written externs. You don’t need this if you don’t have any source externs.
+        - `__init__.py` : Initializes externs. See Appendix.
+    - `smithygenerated/`: Smithy-Dafny generated code.
+      - `my_project/`: Smithy-generated code for a LocalService’s namespace.
+      - Note: If a Smithy-Dafny project has multiple LocalServices, there will be multiple folders in this directory. Each folder will named be the LocalService’s Smithy namespace converted to snakecase. For an example, see [Crypto Tools’ MPL](https://github.com/aws/aws-cryptographic-material-providers-library/tree/main/AwsCryptographicMaterialProviders/runtimes/python/src/aws_cryptographic_materialproviders/smithygenerated).
+- `test/`: Project test code.
+  - `internaldafny/`: Dafny tests.
+    - `test_dafny_wrapper.py`: See Appendix.
+      - `generated/` : Dafny-generated test code.
+      - `extern/`: Holds manually-written test externs. You don’t need this if you don’t have any test externs.
+  - Any other test groupings, ex. `functional/`: Other tests for the project that aren’t Dafny-generated. For an example, See [Crypto Tools’ AwsCryptographyPrimitives](https://github.com/aws/aws-cryptographic-material-providers-library/tree/main/AwsCryptographyPrimitives/runtimes/python/test).
+- `pyproject.toml` : Project configuration and dependencies file. See Appendix.
+- `tox.ini` : Test configuration file. See Appendix.
+
+# Externs
+
+In Python, Dafny externs are not loaded at compile time because "compile time" doesn't exist in Python. Python code is interpreted, not compiled.
+Smithy-Dafny Python projects use this pattern to link extern code when the Smithy-Dafny module is loaded.
+
+Smithy-Dafny Python extern implementations must:
+
+1. Extend the generated class, if there is one
+2. “Export” itself to the generated class
+   1. **Why?** The Dafny-generated code expects that generated code behaves like it has extern code. The extern class that extends the generated class has this behavior. Overwriting the generated class with the extern class matches Dafny’s expectation.
+
+Annotated sample implementation:
+
+```
+# If this is generated by `transpile_python`
+import my_project.internaldafny.generated.ModuleWithExtern.SomeExternCLass
+# Your extern might need code from the generated module
+from my_project.internaldafny.generated.ModuleWithExtern import *
+
+# Extern should extend generated class, if one is generated
+class SomeExternClass(my_project.internaldafny.generated.SomeExternClass):
+    ...
+
+# Export extern class to generated class
+my_project.internaldafny.generated.ModuleWithExtern.SomeExternClass = SomeExternClass
+```
+
+This extern file should be placed at `my_project/internaldafny/extern`.
+
+Every project that has externs must also have an `__init__.py` located at `my_project/internaldafny/extern` with the code at [TODO].
+
+Examples:
+
+- [Extern TestModel](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/Extern/runtimes/python/src/simple_dafnyextern/internaldafny/extern).
+
+# Appendix
+
+## Code Samples
+
+### Project Initialization Files
+
+Every Smithy-Dafny project should have a file at `src/your_project/__init__.py` with the following content:
+
+```
+# Initialize generated Dafny
+from .internaldafny.generated import module_
+
+# Initialize externs
+# (If you don't have externs, omit this import)
+from .internaldafny import extern
+```
+
+This file is executed when your project is imported.
+
+This file primarily exists to initialize a project’s Dafny code.
+
+First, this file initializes generated Dafny by importing the generated `module_.py`.
+`module_.py` is a Dafny-generated file that imports a project’s generated Dafny topologically (i.e. avoiding circular dependencies in import dependencies).
+
+Second, this file initializes externs.
+(This order is important; externs rely on generated code, and the generated code must be imported first to avoid circular dependencies.)
+
+To use externs in source code, you must add a file at `my_project/internaldafny/extern/__init__.py`.
+This file is executed by the root `__init__.py` when the project is imported.
+This file will import externs.
+
+```
+from . import (
+    MyExtern
+)
+```
+
+Examples:
+
+- [Constraints TestModel](https://github.com/smithy-lang/smithy-dafny/blob/main-1.x/TestModels/Constraints/runtimes/python/src/simple_constraints/__init__.py). This has no externs, so the `import extern` line is omitted.
+- [Extern TestModel](https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/Extern/runtimes/python/src/simple_dafnyextern). This has both generated and extern code.