chore: Forwards compatibility with Dafny > 4.2 (including pending 4.5)

.github/actions/polymorph_codegen/action.yml

@@ -0,0 +1,91 @@
+#
+# 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.
+
+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
+outputs:
+  random-number:
+    description: "Random number"
+    value: ${{ steps.random-number-generator.outputs.random-number }}
+runs:
+  using: "composite"
+  steps:
+    # Replace the project.properties file so that we pick up the right runtimes etc.,
+    # in cases where inputs.dafny is different from the current value in that file.
+    - name: Update top-level project.properties file
+      env:
+        DAFNY_VERSION: ${{ inputs.dafny }}
+      shell: bash
+      run: |
+        make generate_properties_file
+
+    - 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
+
+    - 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 -C .. setup_prettier
+        make polymorph_java
+
+    - name: Regenerate .NET code using smithy-dafny
+      working-directory: ./${{ inputs.library }}
+      shell: bash
+      run: |
+        make polymorph_dotnet
+
+    - 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

@@ -16,6 +16,12 @@ jobs:
     uses: ./.github/workflows/library_format.yml
     with:
       dafny: ${{needs.getVersion.outputs.version}}
+  daily-ci-codegen:
+    needs: getVersion
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_codegen.yml
+    with:
+      dafny: ${{needs.getVersion.outputs.version}}
   daily-ci-verification:
     needs: getVersion
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'

.github/workflows/library_codegen.yml

@@ -0,0 +1,64 @@
+# 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:
+          [
+            TestVectorsAwsCryptographicMaterialProviders,
+            AwsCryptographyPrimitives,
+            ComAmazonawsKms,
+            ComAmazonawsDynamodb,
+            AwsCryptographicMaterialProviders,
+            StandardLibrary,
+          ]
+        # 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 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

@@ -8,9 +8,16 @@ 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:
   verification:
     strategy:
+      fail-fast: false
       matrix:
         library:
           [
@@ -23,6 +30,9 @@ jobs:
           ]
         os: [macos-latest-large]
     runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
     env:
       DOTNET_CLI_TELEMETRY_OPTOUT: 1
       DOTNET_NOLOGO: 1
@@ -33,11 +43,12 @@ jobs:
 
       - 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 submodule we DO 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 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 }}
 
@@ -48,8 +59,15 @@ jobs:
         with:
           dotnet-version: "6.0.x"
 
+      - 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
+
       - name: Verify ${{ matrix.library }} Dafny code
-        shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
           # This works because `node` is installed by default on GHA runners
@@ -58,7 +76,6 @@ jobs:
 
       - name: Check solver resource use
         if: success() || failure()
-        shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
           make dafny-reportgenerator

.github/workflows/library_format.yml

@@ -26,6 +26,9 @@ jobs:
           ]
         os: [ubuntu-latest]
     runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
     env:
       DOTNET_CLI_TELEMETRY_OPTOUT: 1
       DOTNET_NOLOGO: 1
@@ -40,20 +43,18 @@ jobs:
       - run: git submodule update --init libraries
 
       - 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: Check format of ${{ matrix.library }} Dafny code
-        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 format_dafny-check
 
       - name: Check format of ${{ matrix.library }} Net code
-        shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
           # This works because `node` is installed by default on GHA runners

.github/workflows/library_java_tests.yml

@@ -8,10 +8,16 @@ 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:
     strategy:
+      fail-fast: false
       matrix:
         library:
           [
@@ -32,6 +38,9 @@ jobs:
     permissions:
       id-token: write
       contents: read
+    defaults:
+      run:
+        shell: bash
     steps:
       - name: Support longpaths on Git checkout
         run: |
@@ -47,22 +56,30 @@ jobs:
 
       - 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 submodule we DO 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 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
+
       - name: Setup Java 8
         uses: actions/setup-java@v3
         with:
           distribution: "corretto"
           java-version: 8
 
       - name: Build ${{ matrix.library }} implementation
-        shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
           # This works because `node` is installed by default on GHA runners

.github/workflows/library_net_tests.yml

@@ -8,10 +8,16 @@ 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:
   testDotNet:
     strategy:
+      fail-fast: false
       matrix:
         library:
           [
@@ -25,6 +31,9 @@ jobs:
         dotnet-version: ["6.0.x"]
         os: [windows-latest, ubuntu-latest, macos-latest]
     runs-on: ${{ matrix.os }}
+    defaults:
+      run:
+        shell: bash
     permissions:
       id-token: write
       contents: read
@@ -45,25 +54,33 @@ jobs:
 
       - 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 submodule we DO 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 smithy-dafny
 
       - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
         uses: actions/setup-dotnet@v3
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - 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
+
       - name: Download Dependencies
         working-directory: ./${{ matrix.library }}
         run: make setup_net
 
       - name: Compile ${{ matrix.library }} implementation
-        shell: bash
         working-directory: ./${{ matrix.library }}
         run: |
           # This works because `node` is installed by default on GHA runners