chore: Adopt SmithyDafnyMakefile.mk, progress towards fixing nightly …

…build (#797)

Replaces nearly all of the `SharedMakefile.mk` with the common `smithy-dafny/SmithyDafnyMakefile.mk` makefile, just retaining configuration variables specific to this repo (such as the path to the `smithy-dafny` submodule). Uses the new features in that makefile and `smithy-dafny` itself to make the projects forwards-compatible with the latest Dafny nightly prerelease, and hence will MOSTLY fix the nightly build once merged. "Mostly" because I still need to fix some externs to make them use the pattern that avoids the Java TypeDescriptor differences between Dafny versions, but that can be fixed in a follow-up PR.

Highlights of the changes:

* Apply the same workflow changes as aws/aws-cryptographic-material-providers-library#195 to use `smithy-dafny` to regenerate code, either to check that the output matches what's checked in (in a new separate codegen workflow) or to be compatible with newer versions of Dafny in the nightly build (in existing workflows).
  * In this case we also have to locally update the MPL submodule to the latest, so that we can pick up the forwards-compatible changes to that repo, and regenerate code transitively. Generating code is unfortunately getting quite expensive, especially since the shared makefile logic isn't sophisticated enough to avoid regenerating the same code multiple times.
  * Because the code in this repo wasn't formatted already, but applying newer `smithy-dafny` code generation automatically formats, all the generated has trivial layout changes.
  * Also extracted a manual patch.
  * ~Applied a lot of [explicit client downcasting](https://github.com/aws/aws-database-encryption-sdk-dynamodb/pull/797/files#diff-692e2b06d124c9775e2fcd9cd9dbd10e0c8ea470e08174ed0b258b0301622581R182) to account for the change in `smithy-dafny` ~ (the change in smithy-dafny was undone so this isn't necessary any more)
* Converted `Beacon.CheckBytesToHex()` from a "test lemma" to a dynamic test, because on the latest Dafny the verification got even more expensive, and this didn't seem to introduce any real additional risk.

.github/actions/polymorph_codegen/action.yml

@@ -0,0 +1,144 @@
+#
+# 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'
+      working-directory: submodules/MaterialProviders
+      shell: bash
+      run: |
+        git checkout main
+        git pull
+        git submodule update --init --recursive
+
+    - name: Update top-level project.properties file in MPL
+      if: inputs.update-and-regenerate-mpl == 'true'
+      shell: bash
+      working-directory: submodules/MaterialProviders
+      run: |
+        make generate_properties_file
+
+    # Update 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: Generate smithy-dafny-project.properties file
+      if: inputs.update-and-regenerate-mpl == 'true'
+      env:
+        DAFNY_VERSION: ${{ inputs.dafny }}
+      shell: bash
+      run: |
+        make generate_properties_file
+
+    - name: Update top-level project.properties file
+      if: inputs.update-and-regenerate-mpl == 'true'
+      shell: bash
+      run: |
+        awk -F= '!a[$1]++' smithy-dafny-project.properties project.properties > merged.properties
+        mv merged.properties project.properties
+        cat project.properties
+
+    - 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 submodules/MaterialProviders/AwsCryptographyPrimitives setup_prettier
+        make -C submodules/MaterialProviders/AwsCryptographicMaterialProviders setup_prettier
+        make -C submodules/MaterialProviders/ComAmazonawsKms setup_prettier
+        make -C submodules/MaterialProviders/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/ci_codegen.yml

@@ -0,0 +1,56 @@
+# This workflow regenerates code using smithy-dafny and checks that the output matches what's checked in.
+name: Library Code Generation
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  code-generation:
+    strategy:
+      fail-fast: false
+      matrix:
+        library:
+          [
+            DynamoDbEncryption,
+            TestVectors
+          ]
+        # 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@v3
+        with:
+          submodules: recursive
+
+      # 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: 4.2.0
+
+      - 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/ci_test_java.yml

@@ -58,6 +58,15 @@ jobs:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.nightly }}
+        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 ${{ matrix.java-version }}
         uses: actions/setup-java@v4
         with:

.github/workflows/ci_test_net.yml

@@ -65,6 +65,15 @@ jobs:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.nightly }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
       - name: Download Dependencies 
         working-directory: ./${{ matrix.library }}
         run: make setup_net

.github/workflows/ci_verification.yml

@@ -28,6 +28,7 @@ jobs:
     # Don't run the nightly build on forks
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     strategy:
+      fail-fast: false
       matrix:
         # Break up verification between namespaces over multiple
         # actions to take advantage of parallelization
@@ -51,8 +52,17 @@ jobs:
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
+
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.nightly }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: DynamoDbEncryption
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
 
-      - name: Verify ${{ matrix.library }} Dafny code
+      - name: Verify ${{ matrix.service }} Dafny code
         shell: bash
         working-directory: ./DynamoDbEncryption
         run: |

DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.2.0.patch

@@ -0,0 +1,48 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+index 9a951767..5c0cee33 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+@@ -7,6 +7,43 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
+ {
+   public static class TypeConversion
+   {
++    // BEGIN MANUAL EDIT
++    public static AWS.Cryptography.KeyStore.KeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient value)
++    {
++      if (value is software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient dafnyValue)
++      {
++        return new AWS.Cryptography.KeyStore.KeyStore(dafnyValue);
++      }
++      throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
++    }
++    public static software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(AWS.Cryptography.KeyStore.KeyStore value)
++    {
++      if (value is AWS.Cryptography.KeyStore.KeyStore nativeValue)
++      {
++        return nativeValue.impl();
++      }
++      throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
++    }
++    public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor value)
++    {
++      if (value is NativeWrapper_LegacyDynamoDbEncryptor nativeWrapper) return nativeWrapper._impl;
++      return new LegacyDynamoDbEncryptor(value);
++
++    }
++    public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor value)
++    {
++      switch (value)
++      {
++        case LegacyDynamoDbEncryptor valueWithImpl:
++          return valueWithImpl._impl;
++        case LegacyDynamoDbEncryptorBase nativeImpl:
++          return new NativeWrapper_LegacyDynamoDbEncryptor(nativeImpl);
++        default:
++          throw new System.ArgumentException(
++              "Custom implementations of LegacyDynamoDbEncryptor must extend LegacyDynamoDbEncryptorBase.");
++      }
++    }
++    // END MANUAL EDIT
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconKeySource FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconKeySource(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IBeaconKeySource value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource)value;

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -453,17 +453,17 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
   import Operations : AbstractAwsCryptographyDbEncryptionSdkDynamoDbOperations
   function method DefaultDynamoDbEncryptionConfig(): DynamoDbEncryptionConfig
   method DynamoDbEncryption(config: DynamoDbEncryptionConfig := DefaultDynamoDbEncryptionConfig())
-    returns (res: Result<IDynamoDbEncryptionClient, Error>)
+    returns (res: Result<DynamoDbEncryptionClient, Error>)
     ensures res.Success? ==>
               && fresh(res.value)
               && fresh(res.value.Modifies)
               && fresh(res.value.History)
               && res.value.ValidState()
 
-  // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
+  // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
   function method CreateSuccessOfClient(client: IDynamoDbEncryptionClient): Result<IDynamoDbEncryptionClient, Error> {
     Success(client)
-  } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
+  }
   function method CreateFailureOfError(error: Error): Result<IDynamoDbEncryptionClient, Error> {
     Failure(error)
   }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -439,17 +439,4 @@ module BaseBeacon {
     else
       [HexChar(TruncateNibble(bytes[0] % 16, topBits))] + ToHexString(bytes[1..])
   }
-
-  lemma {:vcs_split_on_every_assert} CheckBytesToHex()
-    ensures
-      && var bytes := [1,2,3,4,5,6,7,0xb7];
-      && BytesToHex(bytes, 1) == "1"
-      && BytesToHex(bytes, 2) == "3"
-      && BytesToHex(bytes, 3) == "7"
-      && BytesToHex(bytes, 4) == "7"
-      && BytesToHex(bytes, 5) == "17"
-      && BytesToHex(bytes, 6) == "37"
-      && BytesToHex(bytes, 7) == "37"
-      && BytesToHex(bytes, 8) == "b7"
-  {}
 }

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy

@@ -28,7 +28,7 @@ module
   }
 
   method DynamoDbEncryption(config: DynamoDbEncryptionConfig)
-    returns (res: Result<IDynamoDbEncryptionClient, Error>)
+    returns (res: Result<DynamoDbEncryptionClient, Error>)
     ensures res.Success? ==> res.value is DynamoDbEncryptionClient
   {
     var internalConfig := Operations.Config();

DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy

@@ -739,4 +739,20 @@ module TestBaseBeacon {
     var src := GetLiteralSource([1,2,3,4,5], version);
     var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src);
   }
+
+  method {:test} CheckBytesToHex()
+  {
+    var bytes := [1,2,3,4,5,6,7,0xb7];
+    // These could be asserted instead,
+    // but they get too expensive
+    // on more recent versions of Dafny.
+    expect BytesToHex(bytes, 1) == "1";
+    expect BytesToHex(bytes, 2) == "3";
+    expect BytesToHex(bytes, 3) == "7";
+    expect BytesToHex(bytes, 4) == "7";
+    expect BytesToHex(bytes, 5) == "17";
+    expect BytesToHex(bytes, 6) == "37";
+    expect BytesToHex(bytes, 7) == "37";
+    expect BytesToHex(bytes, 8) == "b7";
+  }
 }

DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy

@@ -211,6 +211,7 @@ module BeaconTestFixtures {
     ensures fresh(output.client.Modifies)
   {
     var client :- expect Primitives.AtomicPrimitives();
+
     var keyNameSet := set b <- version.standardBeacons :: b.name;
     var keyNames := SortedSets.ComputeSetToOrderedSequence2(keyNameSet, CharLess);
     var keys :- expect SI.GetHmacKeys(client, keyNames, keyNames, key);