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

#195)

Applies several fixes/improvements in order to work with newer Dafny versions.

* Adds `smithy-dafny` as a submodule so that we can lock down the exact commit used to generate code, and use the tool in CI.
* Updates the shared makefile with similar improvements to smithy-dafny's (hook up `--library-root` and `--patch-files-dir`, generate dependencies first)
* Regenerates the checked-in code using a newer `smithy-dafny` to abstract away from the changes in Java TypeDescriptors when constructing datatypes in Dafny 4.3. This includes adding some helper methods to Dafny code for the benefit of Java external code, in the same style as smithy-lang/smithy-dafny#301 did.
  * Also updated various `__default` classes to use the above to avoid constructing Dafny datatypes directly. 
  * Regenerating means that the effect of smithy-lang/smithy-dafny#311 on C# code shows up too.
  * Introduced `InternalResult<T, R>` to replace some internal-only uses of Dafny's compiled `Result` type, to avoid even more Dafny helper methods. 
* Leverage the `smithy-dafny` `<library-root>/codegen-patches[/<service>]` feature to extract out manual patch files.
  * This allows building with a newer version of Dafny to work despite having to regenerate code differently, in some cases by providing different patch files for different version ranges.
  * Cheated slightly by using this to conditionally remove an instance of `{:vcs_split_on_every_assert}` on `AwsKmsKeyring.OnDecrypt'` that is necessary on Dafny 4.2 but makes things work on Dafny 4.4 (which was not the intention of the patching feature, but also solves this problem much more cheaply than having to refactor the code to work in both versions :)
* Add regenerating code to CI, either to verify that it matches what's checked in, or to pick up the necessary changes to work with newer Dafny versions.

Manually verified the CI passes on the source branch with the latest Dafny nightly prerelease: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/8039889665

Note that CI will now reject making further manual edits to generated files without capturing those edits in patch files. The error message will suggest how to update the patch files accordingly. See also https://github.com/smithy-lang/smithy-dafny/tree/main-1.x/TestModels/CodegenPatches

.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