Python POC

.github/workflows/smithy-dafny-conversion.yml

@@ -11,10 +11,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
       - uses: actions/setup-java@v3
         with:
           distribution: 'corretto'
-          java-version: '8'
+          java-version: '17'
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]

.github/workflows/smithy-polymorph.yml

@@ -11,6 +11,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
       - uses: actions/setup-java@v3
         with:
           distribution: 'corretto'
@@ -35,6 +38,14 @@ jobs:
           arguments: :smithy-dafny-codegen:publishToMavenLocal
           build-root-directory: codegen
 
+      # Required for building Smithy-Dafny
+      # TODO: This step can and should be removed once Smithy-Python is on Maven central
+      - name: Locally cache smithy-python-codegen
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :smithy-python-codegen:publishToMavenLocal
+          build-root-directory: submodules/smithy-python/codegen
+
       - name: Sanity-check SQS test model via plugin
         uses: gradle/gradle-build-action@v2
         with:

.github/workflows/test_models_dafny_verification.yml

@@ -71,7 +71,14 @@ jobs:
         run: |
           git config --global core.longpaths true
 
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version: '17'
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]

.github/workflows/test_models_java_tests.yml

@@ -80,6 +80,8 @@ jobs:
           role-session-name: JavaTests
 
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]

.github/workflows/test_models_net_tests.yml

@@ -83,6 +83,8 @@ jobs:
           role-session-name: NetTests
 
       - uses: actions/checkout@v3
+        with:
+          submodules: recursive
 
       - name: Setup Dafny
         uses: dafny-lang/[email protected]

.github/workflows/test_models_python_tests.yml

@@ -0,0 +1,126 @@
+# This workflow performs tests in Python.
+name: Library Python tests
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main-1.x
+  workflow_dispatch:
+    # Manual trigger for this workflow, either the normal version
+    # or the nightly build that uses the latest Dafny prerelease
+    # (accordingly to the "nightly" parameter).
+    inputs:
+      nightly:
+        description: 'Run the nightly build'
+        required: false
+        type: boolean
+  schedule:
+    # Nightly build against Dafny's nightly prereleases,
+    # for early warning of verification issues or regressions.
+    # Timing chosen to be adequately after Dafny's own nightly build,
+    # but this might need to be tweaked:
+    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
+    - cron: "30 16 * * *"
+
+jobs:
+  testPython:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'smithy-lang'
+    strategy:
+      matrix:
+        library: [
+          # TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
+          TestModels/Aggregate,
+          # TestModels/AggregateReferences,
+          TestModels/Constraints,
+          TestModels/Constructor,
+          TestModels/Dependencies,
+          TestModels/Errors,
+          TestModels/Extendable,
+          TestModels/Extern,
+          TestModels/LocalService,
+          TestModels/Refinement,
+          TestModels/Resource,
+          # TestModels/SimpleTypes/BigDecimal,
+          # TestModels/SimpleTypes/BigInteger,
+          TestModels/SimpleTypes/SimpleBlob,
+          TestModels/SimpleTypes/SimpleBoolean,
+          # TestModels/SimpleTypes/SimpleByte,
+          TestModels/SimpleTypes/SimpleDouble,
+          TestModels/SimpleTypes/SimpleEnum,
+          # TestModels/SimpleTypes/SimpleEnumV2,
+          # TestModels/SimpleTypes/SimpleFloat,
+          TestModels/SimpleTypes/SimpleInteger,
+          TestModels/SimpleTypes/SimpleLong,
+          # TestModels/SimpleTypes/SimpleShort,
+          TestModels/SimpleTypes/SimpleString,
+          # TestModels/SimpleTypes/SimpleTimestamp,
+          TestModels/Union,
+          # TestModels/aws-sdks/ddb,
+          # TestModels/aws-sdks/kms,
+        ]
+    runs-on: "ubuntu-latest"
+    permissions:
+      id-token: write
+      contents: read
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v1
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-PolymorphTestModels-Role-us-west-2
+          role-session-name: PythonTests
+
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: 'nightly-latest'
+
+      - name: Setup Python for running tests
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.11
+          architecture: x64
+      - run: |
+          python -m pip install --upgrade pip
+          pip install --upgrade tox
+          pip install poetry
+
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version: '17'
+
+      - name: Generate Polymorph Dafny and Python code
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          make polymorph_dafny
+          make polymorph_python
+
+      - name: Compile ${{ matrix.library }} implementation
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make build_python CORES=$CORES
+
+      - name: Test ${{ matrix.library }}
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          make test_python

.gitignore

@@ -2,5 +2,5 @@
 /.idea
 /.history
 /.smithy.lsp.log
-
+*.pyc
 */**/.idea

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "submodules/smithy-python"]
+	path = submodules/smithy-python
+	url = [email protected]:lucasmcdonald3/smithy-python.git

TestModels/.gitignore

@@ -9,6 +9,10 @@
 **/runtimes/java/src/main/dafny-generated/
 **/runtimes/java/src/test/dafny-generated/
 
+# Dafny Generated Python
+**/runtimes/python/src/**/internal_generated_dafny/*.py
+**/runtimes/python/test/internal_generated_dafny/*.py
+
 # Polymorph Generated Dafny
 **/Model/*Types.dfy
 **/Model/*TypesWrapped.dfy
@@ -20,10 +24,21 @@
 # Polymorph Generated Java
 **/runtimes/java/src/main/smithy-generated/
 
+# Polymorph Generated Python
+**/runtimes/python/src/**/smithygenerated/
+
 # .NET Artifacts
 **/bin
 **/obj
 
+# Python Artifacts
+**/runtimes/python/src/**.egg-info/
+**/runtimes/python/.pytest_cache
+**/runtimes/python/.tox
+**/runtimes/python/build
+**/runtimes/python/poetry.lock
+**/runtimes/python/**/poetry.lock
+
 # JetBrains
 **/.idea/
 **/Folder.DotSettings.user

TestModels/Aggregate/runtimes/python/pyproject.toml

@@ -0,0 +1,26 @@
+[tool.poetry]
+name = "simple-aggregate"
+version = "0.1.0"
+description = ""
+authors = ["AWS <[email protected]>"]
+packages = [
+    { include = "simple_aggregate", from = "src" }
+]
+# Include all of the following .gitignored files in package distributions,
+# even though it is not included in version control
+include = ["**/smithygenerated/*.py", "**/internal_generated_dafny/*.py"]
+
+[tool.poetry.dependencies]
+python = "^3.11.0"
+simple-aggregate-internaldafny = { path = "src/simple_aggregate/internal_generated_dafny", develop = false}
+# TODO: Depend on PyPi once Smithy-Python publishes their Python package there
+smithy-python = { path = "../../../../submodules/smithy-python/python-packages/smithy-python", develop = false}
+standard-library = {path = "../../../dafny-dependencies/StandardLibrary/runtimes/python", develop = false}
+
+[tool.poetry.group.test.dependencies]
+pytest = "^7.4.0"
+simple-aggregate-test-internaldafny = { path = "test/internal_generated_dafny", develop = false}
+
+[build-system]
+requires = ["poetry-core"]
+build-backend = "poetry.core.masonry.api"

TestModels/Aggregate/runtimes/python/src/simple_aggregate/extern/wrapped_simple_aggregate.py

@@ -0,0 +1,16 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+import simple_aggregate_internaldafny_wrapped
+from simple_aggregate.smithygenerated.client import SimpleAggregate
+from simple_aggregate.smithygenerated.shim import SimpleAggregateShim
+import Wrappers
+
+@staticmethod
+def WrappedSimpleAggregate(config):
+    wrapped_config = config
+    impl = SimpleAggregate(wrapped_config)
+    wrapped_client = SimpleAggregateShim(impl)
+    return Wrappers.Result_Success(wrapped_client)
+
+simple_aggregate_internaldafny_wrapped.default__.WrappedSimpleAggregate = WrappedSimpleAggregate

TestModels/Aggregate/runtimes/python/src/simple_aggregate/internal_generated_dafny/pyproject.toml

@@ -0,0 +1,21 @@
+[tool.poetry]
+name = "simple-aggregate-internaldafny"
+version = "0.1.0"
+description = ""
+authors = ["AWS <[email protected]>"]
+packages = [
+    # Globally install all internaldafny modules
+    # such that a module X can be imported with `import X`
+    # from anywhere in the Python runtime that installs this module
+    { include = "*.py" },
+]
+# Include all of the following .gitignored files in package distributions,
+# even though it is not included in version control
+include = ["*.py"]
+
+[tool.poetry.dependencies]
+python = "^3.11.0"
+
+[build-system]
+requires = ["poetry-core"]
+build-backend = "poetry.core.masonry.api"

TestModels/Aggregate/runtimes/python/test/extern/test_dafny_wrapper.py

@@ -0,0 +1,27 @@
+"""
+Wrapper file for executing Dafny tests from pytest.
+This allows us to import modules required by Dafny-generated tests
+before executing Dafny-generated tests.
+pytest will find and execute the `test_dafny` method below,
+which will execute the `test.py` file in the `dafny` directory.
+"""
+
+import glob
+from os.path import isfile, join
+import importlib
+
+# Import modules required for Dafny-generated tests.
+# This is not generated; these must be manually added.
+
+from simple_aggregate.extern import wrapped_simple_aggregate
+
+# End import modules required for Dafny-generated tests
+
+def test_dafny():
+  dafny_modules = glob.glob(join("/".join(__file__.split("/")[:-2]) + "/internal_generated_dafny/", "*.py"), recursive=True)
+  for f in dafny_modules:
+    if isfile(f) and f.endswith('test.py'):
+      fname = str(f).split("/")[-1].split(".")[0]
+      spec = importlib.util.spec_from_file_location(fname, f)
+      module = importlib.util.module_from_spec(spec)
+      spec.loader.exec_module(module)

TestModels/Aggregate/runtimes/python/test/internal_generated_dafny/pyproject.toml

@@ -0,0 +1,21 @@
+[tool.poetry]
+name = "simple-aggregate-test-internaldafny"
+version = "0.1.0"
+description = ""
+authors = ["AWS <[email protected]>"]
+packages = [
+    # Globally install all internaldafny modules
+    # such that a module X can be imported with `import X`
+    # from anywhere in the Python runtime that installs this module
+    { include = "*.py" },
+]
+# Include all of the following .gitignored files in package distributions,
+# even though it is not included in version control
+include = ["*.py"]
+
+[tool.poetry.dependencies]
+python = "^3.11.0"
+
+[build-system]
+requires = ["poetry-core"]
+build-backend = "poetry.core.masonry.api"

TestModels/Aggregate/runtimes/python/tox.ini

@@ -0,0 +1,13 @@
+[tox]
+isolated_build = True
+envlist =
+  py{311}
+
+[testenv]
+skip_install = true
+allowlist_externals = poetry
+commands_pre =
+    poetry lock
+    poetry install
+commands =
+    poetry run pytest test/ --import-mode importlib

TestModels/Aggregate/smithy-build.json

@@ -0,0 +1,11 @@
+{
+    "version": "1.0",
+    "plugins": {
+        "dafny-client-codegen": {
+            "service": "simple.aggregate#SimpleAggregate",
+            "module": "simple_aggregate",
+            "moduleVersion": "0.0.1",
+            "protocol": "aws.polymorph#localService"
+        }
+    }
+}