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

.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);