chore: Fix nightly build (aside from verification)

.github/actions/polymorph_codegen/action.yml

@@ -116,6 +116,7 @@ runs:
         make -C submodules/MaterialProviders/AwsCryptographicMaterialProviders setup_prettier
         make -C submodules/MaterialProviders/ComAmazonawsKms setup_prettier
         make -C submodules/MaterialProviders/ComAmazonawsDynamodb setup_prettier
+        make -C submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders setup_prettier
 
     - name: Regenerate Java code using smithy-dafny
       # npx seems to be unavailable on Windows GHA runners,

.github/workflows/ci_examples_java.yml

@@ -60,6 +60,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: ${{ github.event_name == 'schedule' || inputs.nightly }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: DynamoDbEncryption
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
       - name: Build and locally deploy dependencies for examples
         shell: bash
         working-directory: ./DynamoDbEncryption

.github/workflows/ci_test_java.yml

@@ -55,7 +55,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}

.github/workflows/ci_test_net.yml

@@ -60,7 +60,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}

.github/workflows/ci_verification.yml

@@ -53,7 +53,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.6.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy

@@ -22,6 +22,43 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry
 
     predicate method {:extern} IsLegacyInput(input: Types.DecryptItemInput)
 
+    // The following functions are for the benefit of the extern implementation to call,
+    // avoiding direct references to generic datatype constructors
+    // since their calling pattern is different between different versions of Dafny
+    // (i.e. after 4.2, explicit type descriptors are required).
+
+    static function method CreateBuildSuccess(value: Option<InternalLegacyOverride>): Result<Option<InternalLegacyOverride>, Types.Error> {
+      Success(value)
+    }
+
+    static function method CreateBuildFailure(error: Types.Error): Result<Option<InternalLegacyOverride>, Types.Error> {
+      Failure(error)
+    }
+
+    static function method CreateInternalLegacyOverrideSome(value: InternalLegacyOverride): Option<InternalLegacyOverride> {
+      Some(value)
+    }
+
+    static function method CreateInternalLegacyOverrideNone(): Option<InternalLegacyOverride> {
+      None
+    }
+
+    function method CreateEncryptItemSuccess(value: Types.EncryptItemOutput): Result<Types.EncryptItemOutput, Types.Error> {
+      Success(value)
+    }
+
+    function method CreateEncryptItemFailure(error: Types.Error): Result<Types.EncryptItemOutput, Types.Error> {
+      Failure(error)
+    }
+
+    function method CreateDecryptItemSuccess(value: Types.DecryptItemOutput): Result<Types.DecryptItemOutput, Types.Error> {
+      Success(value)
+    }
+
+    function method CreateDecryptItemFailure(error: Types.Error): Result<Types.DecryptItemOutput, Types.Error> {
+      Failure(error)
+    }
+
   }
 
 }

DynamoDbEncryption/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/internaldafny/legacy/InternalLegacyOverride.java

@@ -1,5 +1,19 @@
 package software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.legacy;
 
+/**
+ * This file does *NOT* import a lot of things.
+ * This is because it is dealing with converting
+ * between different versions of the same name.
+ * The DynamoDbItemEncryptor module has Dafny and Java versions
+ * of the same type.
+ * This means that `EncryptItemOutput` for example
+ * needs to be disambiguated between the Dafny version and the Java version.
+ * In order to make it clearer at each call-site exactly what is happening
+ * the full import is used.
+ * IDEs tend to fight this so I'm sorry.
+ */
+
+import StandardLibraryInternal.InternalResult;
 import Wrappers_Compile.Option;
 import Wrappers_Compile.Result;
 import com.amazonaws.services.dynamodbv2.datamodeling.encryption.DynamoDBEncryptor;
@@ -16,22 +30,9 @@
 import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy;
 import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative;
 import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error;
-/**
- * This file does *NOT* import a lot of things.
- * This is because it is dealing with converting
- * between different versions of the same name.
- * The DynamoDbItemEncryptor module has Dafny and Java versions
- * of the same type.
- * This means that `EncryptItemOutput` for example
- * needs to be disambiguated between the Dafny version and the Java version.
- * In order to make it clearer at each call-site exactly what is happening
- * the full import is used.
- * IDEs tend to fight this so I'm sorry.
- */
-
 import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction;
 
-public class InternalLegacyOverride {
+public class InternalLegacyOverride extends _ExternBase_InternalLegacyOverride {
 
   private DynamoDBEncryptor encryptor;
   private Map<String, Set<EncryptionFlags>> actions;
@@ -69,7 +70,7 @@ public static TypeDescriptor<InternalLegacyOverride> _typeDescriptor() {
     );
   }
 
-  public Boolean IsLegacyInput(
+  public boolean IsLegacyInput(
     software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput input
   ) {
     //= specification/dynamodb-encryption-client/decrypt-item.md#determining-legacy-items
@@ -94,7 +95,9 @@ > EncryptItem(
   ) {
     // Precondition: Policy MUST allow the caller to encrypt.
     if (!_policy.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT()) {
-      return createFailure("Legacy Policy does not support encrypt.");
+      return CreateEncryptItemFailure(
+        createError("Legacy Policy does not support encrypt.")
+      );
     }
 
     try {
@@ -124,9 +127,9 @@ > EncryptItem(
         software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny.EncryptItemOutput(
           nativeOutput
         );
-      return Result.create_Success(dafnyOutput);
+      return CreateEncryptItemSuccess(dafnyOutput);
     } catch (Exception ex) {
-      return Result.create_Failure(Error.create_Opaque(ex));
+      return CreateEncryptItemFailure(Error.create_Opaque(ex));
     }
   }
 
@@ -146,7 +149,9 @@ > DecryptItem(
       !_policy.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT() &&
       !_policy.is_FORBID__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT()
     ) {
-      return createFailure("Legacy Policy does not support decrypt.");
+      return CreateDecryptItemFailure(
+        createError("Legacy Policy does not support decrypt.")
+      );
     }
     try {
       Map<
@@ -175,9 +180,9 @@ > DecryptItem(
         software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny.DecryptItemOutput(
           nativeOutput
         );
-      return Result.create_Success(dafnyOutput);
+      return CreateDecryptItemSuccess(dafnyOutput);
     } catch (Exception ex) {
-      return Result.create_Failure(Error.create_Opaque(ex));
+      return CreateDecryptItemFailure(Error.create_Opaque(ex));
     }
   }
 
@@ -186,7 +191,7 @@ public static Result<Option<InternalLegacyOverride>, Error> Build(
   ) {
     // Check for early return (Postcondition): If there is no legacyOverride there is nothing to do.
     if (encryptorConfig.dtor_legacyOverride().is_None()) {
-      return Result.create_Success(Option.create_None());
+      return CreateBuildSuccess(CreateInternalLegacyOverrideNone());
     }
     final software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyOverride legacyOverride =
       encryptorConfig.dtor_legacyOverride().dtor_value();
@@ -198,43 +203,48 @@ public static Result<Option<InternalLegacyOverride>, Error> Build(
 
     // Precondition: The encryptor MUST be a DynamoDBEncryptor
     if (!isDynamoDBEncryptor(maybeEncryptor)) {
-      return createFailure("Legacy encryptor is not supported");
+      return CreateBuildFailure(
+        createError("Legacy encryptor is not supported")
+      );
     }
     // Preconditions: MUST be able to create valid encryption context
-    final Result<EncryptionContext, Error> maybeEncryptionContext =
+    final InternalResult<EncryptionContext, Error> maybeEncryptionContext =
       legacyEncryptionContext(encryptorConfig);
-    if (maybeEncryptionContext.is_Failure()) {
-      return Result.create_Failure(maybeEncryptionContext.dtor_error());
+    if (maybeEncryptionContext.isFailure()) {
+      return CreateBuildFailure(maybeEncryptionContext.error());
     }
     // Precondition: All actions MUST be supported types
-    final Result<Map<String, Set<EncryptionFlags>>, Error> maybeActions =
-      legacyActions(legacyOverride.dtor_attributeActionsOnEncrypt());
-    if (maybeActions.is_Failure()) {
-      return Result.create_Failure(maybeEncryptionContext.dtor_error());
+    final InternalResult<
+      Map<String, Set<EncryptionFlags>>,
+      Error
+    > maybeActions = legacyActions(
+      legacyOverride.dtor_attributeActionsOnEncrypt()
+    );
+    if (maybeActions.isFailure()) {
+      return CreateBuildFailure(maybeEncryptionContext.error());
     }
 
     final InternalLegacyOverride internalLegacyOverride =
       new InternalLegacyOverride(
         (DynamoDBEncryptor) maybeEncryptor,
-        maybeActions.dtor_value(),
-        maybeEncryptionContext.dtor_value(),
+        maybeActions.value(),
+        maybeEncryptionContext.value(),
         legacyOverride.dtor_policy()
       );
 
-    return Result.create_Success(Option.create_Some(internalLegacyOverride));
+    return CreateBuildSuccess(
+      CreateInternalLegacyOverrideSome(internalLegacyOverride)
+    );
   }
 
   //  Everything below this point is an implementation detail
 
-  public static <T> Result<T, Error> createFailure(String message) {
+  public static Error createError(String message) {
     final DafnySequence<Character> dafnyMessage =
       software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
         message
       );
-    final Error dafnyEx = Error.create_DynamoDbItemEncryptorException(
-      dafnyMessage
-    );
-    return Result.create_Failure(dafnyEx);
+    return Error.create_DynamoDbItemEncryptorException(dafnyMessage);
   }
 
   public static boolean isDynamoDBEncryptor(
@@ -253,7 +263,10 @@ public static DafnySequence<Character> ToDafnyString(String s) {
     );
   }
 
-  public static Result<EncryptionContext, Error> legacyEncryptionContext(
+  public static InternalResult<
+    EncryptionContext,
+    Error
+  > legacyEncryptionContext(
     software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig config
   ) {
     try {
@@ -272,13 +285,16 @@ public static Result<EncryptionContext, Error> legacyEncryptionContext(
           .build()
         : encryptionContextBuilder.build();
 
-      return Result.create_Success(encryptionContext);
+      return InternalResult.success(encryptionContext);
     } catch (Exception ex) {
-      return Result.create_Failure(Error.create_Opaque(ex));
+      return InternalResult.failure(Error.create_Opaque(ex));
     }
   }
 
-  public static Result<Map<String, Set<EncryptionFlags>>, Error> legacyActions(
+  public static InternalResult<
+    Map<String, Set<EncryptionFlags>>,
+    Error
+  > legacyActions(
     DafnyMap<
       ? extends DafnySequence<? extends Character>,
       ? extends CryptoAction
@@ -311,14 +327,14 @@ public static Result<Map<String, Set<EncryptionFlags>>, Error> legacyActions(
         }
       };
       attributeActionsOnEncrypt.forEach(buildLegacyActions);
-      return Result.create_Success(legacyActions);
+      return InternalResult.success(legacyActions);
     } catch (IllegalArgumentException ex) {
       final Error dafnyEx = Error.create_DynamoDbItemEncryptorException(
         ToDafnyString(ex.getMessage())
       );
-      return Result.create_Failure(dafnyEx);
+      return InternalResult.failure(dafnyEx);
     } catch (Exception ex) {
-      return Result.create_Failure(Error.create_Opaque(ex));
+      return InternalResult.failure(Error.create_Opaque(ex));
     }
   }
 

DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj

@@ -31,11 +31,35 @@
     <NoWarn>CS0105,CS0618</NoWarn>
   </PropertyGroup>
 
+  <PropertyGroup>
+    <!-- This is somewhat brittle,
+         but having the value in a properties file
+         that can be shared is worth it.
+         See: https://learn.microsoft.com/en-us/visualstudio/msbuild/property-functions?view=vs-2022
+         for more details on property functions
+
+         This takes a properties file (a=b)
+         1. Loads the file
+         2. Splits on `dafnyVersion=` and takes everything to the right of that
+           e.g. the version + any trailing data
+         3. Splits on newline and takes the second element.
+           This SHOULD be the value of `dafnyVersion` and not contain any trailing data
+     -->
+    <projectProperties>
+      $([System.IO.File]::ReadAllText('$(MSBuildProjectDirectory)/../../../project.properties'))
+    </projectProperties>
+    <dropBeforeDafnyVersionProperty>
+      $([System.Text.RegularExpressions.Regex]::Split("$(projectProperties)", "dafnyVersion=")[1])
+    </dropBeforeDafnyVersionProperty>
+    <DafnyVersion>
+      $([System.Text.RegularExpressions.Regex]::Split("$(dropBeforeDafnyVersionProperty)", "\n")[1])
+    </DafnyVersion>
+  </PropertyGroup>
 
   <ItemGroup>
     <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.303.14"/>
     <PackageReference Include="AWSSDK.Core" Version="3.7.304.7"/>
-    <PackageReference Include="DafnyRuntime" Version="4.2.0" />
+    <PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
     <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
     <!--
               System.Collections.Immutable can be removed once dafny.msbuild is updated with

project.properties

@@ -1,4 +1,5 @@
 projectJavaVersion=3.5.0-SNAPSHOT
 mplDependencyJavaVersion=1.4.0
+dafnyVersion=4.2.0
 dafnyRuntimeJavaVersion=4.2.0
 smithyDafnyJavaConversionVersion=0.1