chore: Adopt SmithyDafnyMakefile.mk, fix nightly build

.github/actions/polymorph_codegen/action.yml

@@ -0,0 +1,116 @@
+#
+# This local action serves two purposes:
+#
+# 1. For core workflows like pull.yml and push.yml,
+#    it is uses to check that the checked in copy of generated code
+#    matches what the current submodule version of smithy-dafny generates.
+#    This is important to ensure whenever someone changes the models
+#    or needs to regenerate to pick up smithy-dafny improvements,
+#    they don't have to deal with unpleasant surprises.
+#
+# 2. For workflows that check compatibility with other Dafny versions,
+#    such as nightly_dafny.yml, it is necessary to regenerate the code
+#    for that version of Dafny first.
+#    This is ultimately because some of the code smithy-dafny generates
+#    is tightly coupled to what code Dafny itself generates.
+#    A concrete example is that Dafny 4.3 added TypeDescriptors
+#    as parameters when constructing datatypes like Option and Result.
+#
+#    This is why this is a composite action instead of a reusable workflow:
+#    the latter executes in a separate runner environment,
+#    but here we need to actually overwrite the generated code in place
+#    so that subsequent steps can work correctly.
+#
+# This action assumes that the given version of Dafny and .NET 6.0.x
+# have already been set up, since they are used to format generated code.
+#
+# Note that recursively generating code doesn't currently work in this repo
+# with the version of the mpl pinned by the submodule,
+# because the SharedMakefileV2.mk in it doesn't work with newer versions of smithy-dafny.
+# Therefore by default we don't recursively regenerate code
+# (accomplished by setting the POLYMORPH_DEPENDENCIES environment variable to "").
+# If `update-and-regenerate-mpl` is true, we first pull the latest mpl,
+# which is necessary both for Makefile compatibility and so we can regenerate mpl code
+# for compatibility with newer versions of Dafny.
+#
+
+name: "Polymorph code generation"
+description: "Regenerates code using smithy-dafny, and optionally checks that the result matches the checked in state"
+inputs:
+  dafny:
+    description: "The Dafny version to run"
+    required: true
+    type: string
+  library:
+    description: "Name of the library to regenerate code for"
+    required: true
+    type: string
+  diff-generated-code:
+    description: "Diff regenerated code against committed state"
+    required: true
+    type: boolean
+  update-and-regenerate-mpl:
+    description: "Locally update MPL to the tip of master and regenerate its code too"
+    required: false
+    default: false
+    type: boolean
+runs:
+  using: "composite"
+  steps:
+    - name: Update MPL submodule locally if requested
+      if: inputs.update-and-regenerate-mpl == 'true'
+      shell: bash
+      run: |
+        git submodule update --init --recursive --remote --merge mpl
+
+    - name: Don't regenerate dependencies unless requested
+      id: dependencies
+      shell: bash
+      run: |
+        echo "PROJECT_DEPENDENCIES=${{ inputs.update-and-regenerate-mpl != 'true' && 'PROJECT_DEPENDENCIES=' || '' }}" >> $GITHUB_OUTPUT
+
+    - name: Regenerate Dafny code using smithy-dafny
+      # Unfortunately Dafny codegen doesn't work on Windows:
+      # https://github.com/smithy-lang/smithy-dafny/issues/317
+      if: runner.os != 'Windows'
+      working-directory: ./${{ inputs.library }}
+      shell: bash
+      run: |
+        make polymorph_dafny ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }}
+
+    - name: Set up prettier in MPL
+      if: inputs.update-and-regenerate-mpl == 'true'
+      shell: bash
+      # Annoyingly, prettier has to be installed in each library individually.
+      # And this is only necessary or even possible if we've updated the mpl submodule.
+      run: |
+        make -C mpl/AwsCryptographyPrimitives setup_prettier
+        make -C mpl/AwsCryptographicMaterialProviders setup_prettier
+        make -C mpl/ComAmazonawsKms setup_prettier
+        make -C mpl/ComAmazonawsDynamodb setup_prettier
+
+    - name: Regenerate Java code using smithy-dafny
+      # npx seems to be unavailable on Windows GHA runners,
+      # so we don't regenerate Java code on them either.
+      if: runner.os != 'Windows'
+      working-directory: ./${{ inputs.library }}
+      shell: bash
+      # smithy-dafny also formats generated code itself now,
+      # so prettier is a necessary dependency.
+      run: |
+        make setup_prettier
+        make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }}
+
+    - name: Regenerate .NET code using smithy-dafny
+      working-directory: ./${{ inputs.library }}
+      shell: bash
+      run: |
+        make polymorph_dotnet ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }}
+
+    - name: Check regenerated code against commited code
+      # Composite action inputs seem to not actually support booleans properly for some reason
+      if: inputs.diff-generated-code == 'true'
+      working-directory: ./${{ inputs.library }}
+      shell: bash
+      run: |
+        make check_polymorph_diff

.github/workflows/daily_ci.yml

@@ -6,6 +6,12 @@ on:
     - cron: "00 15 * * 1-5"
 
 jobs:
+  daily-ci-codegen:
+    # Don't run the cron builds on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_dafny_codegen.yml
+    with:
+      dafny: '4.2.0'
   daily-ci-verification:
     # Don't run the cron builds on forks
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'

.github/workflows/library_codegen.yml

@@ -0,0 +1,60 @@
+# This workflow regenerates code using smithy-dafny and checks that the output matches what's checked in.
+name: Library Code Generation
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+
+jobs:
+  code-generation:
+    strategy:
+      fail-fast: false
+      matrix:
+        library:
+          [
+            AwsEncryptionSDK,
+          ]
+        # Note dotnet is only used for formatting generated code
+        # in this workflow
+        dotnet-version: ["6.0.x"]
+        os: [ubuntu-latest]
+    runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
+
+      - uses: actions/checkout@v4
+      # The specification submodule is private so we don't have access, but we don't need
+      # it to verify the Dafny code. Instead we manually pull the submodules we DO need.
+      - run: git submodule update --init libraries
+      - run: git submodule update --init --recursive mpl
+      - run: git submodule update --init smithy-dafny
+
+      # Only used to format generated code
+      # and to translate version strings such as "nightly-latest"
+      # to an actual DAFNY_VERSION.
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
+        uses: actions/setup-dotnet@v3
+        with:
+          dotnet-version: ${{ matrix.dotnet-version }}
+
+      - uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: ${{ matrix.library }}
+          diff-generated-code: true

.github/workflows/library_dafny_verification.yml

@@ -7,7 +7,12 @@ on:
       dafny:
         description: 'The Dafny version to run'
         required: true
-        type: string  
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   verification:
@@ -31,12 +36,22 @@ jobs:
         run: |
             git submodule update --init libraries
             git submodule update --init --recursive mpl
+            git submodule update --init smithy-dafny
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
       - name: Verify ${{ matrix.library }} Dafny code
         shell: bash
         working-directory: ./${{ matrix.library }}

.github/workflows/library_interop_tests.yml

@@ -46,6 +46,7 @@ jobs:
         run: |
           git submodule update --init libraries
           git submodule update --init --recursive mpl
+          git submodule update --init smithy-dafny
 
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v4
@@ -135,6 +136,7 @@ jobs:
         run: |
           git submodule update --init libraries
           git submodule update --init --recursive mpl
+          git submodule update --init smithy-dafny
 
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v4
@@ -227,6 +229,7 @@ jobs:
         run: |
           git submodule update --init libraries
           git submodule update --init --recursive mpl
+          git submodule update --init smithy-dafny
 
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v4

.github/workflows/library_java_tests.yml

@@ -8,6 +8,11 @@ on:
         description: 'The Dafny version to run'
         required: true
         type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
 
 jobs:
   testJava:
@@ -36,6 +41,7 @@ jobs:
         run: |
             git submodule update --init libraries
             git submodule update --init --recursive mpl
+            git submodule update --init smithy-dafny
 
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v2
@@ -45,10 +51,19 @@ jobs:
           role-session-name: JavaTests
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
       - name: Setup Java 8
         uses: actions/setup-java@v3
         with:

.github/workflows/library_net_tests.yml

@@ -8,6 +8,11 @@ on:
         description: 'The Dafny version to run'
         required: true
         type: string  
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
 
 env:
   # Used in examples
@@ -23,6 +28,7 @@ env:
 jobs:
   testDotNet:
     strategy:
+      fail-fast: false
       matrix:
         os: [
           windows-latest,
@@ -46,6 +52,7 @@ jobs:
         run: |
           git submodule update --init libraries
           git submodule update --init --recursive mpl
+          git submodule update --init smithy-dafny
 
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v2
@@ -60,10 +67,19 @@ jobs:
           dotnet-version: '6.0.x'
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
           dafny-version: ${{ inputs.dafny }}
 
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: AwsEncryptionSDK
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
       - name: Download Dependencies 
         working-directory: ./AwsEncryptionSDK
         run: make setup_net

.github/workflows/manual.yml

@@ -0,0 +1,34 @@
+# This workflow invokes other workflows with the requested Dafny build.
+# It is primarily meant for manual compatibility testing,
+# such as trying out what the next pending nightly build will do ahead of time.
+name: Manual CI
+
+on:
+  workflow_dispatch:
+    inputs:
+      dafny:
+        description: "The Dafny version to use"
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: true
+        type: boolean
+
+jobs:
+  manual-ci-verification:
+    uses: ./.github/workflows/library_dafny_verification.yml
+    with:
+      dafny: ${{ inputs.dafny }}
+      regenerate-code: ${{ inputs.regenerate-code }}
+  # manual-ci-java:
+  #   uses: ./.github/workflows/library_java_tests.yml
+  #   with:
+  #     dafny: ${{ inputs.dafny }}
+  #     regenerate-code: ${{ inputs.regenerate-code }}
+  manual-ci-net:
+    uses: ./.github/workflows/library_net_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}
+      regenerate-code: ${{ inputs.regenerate-code }}

.github/workflows/nighly_dafny.yml

@@ -18,13 +18,16 @@ jobs:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
       dafny: 'nightly-latest'
+      regenerate-code: true
   # dafny-nightly-java:
   #   if: github.event_name != 'schedule' || github.repository_owner == 'aws'
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
   #     dafny: 'nightly-latest'
+  #     regenerate-code: true
   dafny-nightly-net:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_net_tests.yml
     with:
       dafny: 'nightly-latest'
+      regenerate-code: true