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

@@ -62,6 +62,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

@@ -59,7 +59,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

@@ -66,7 +66,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

@@ -54,7 +54,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 }}

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

@@ -13,6 +13,7 @@
  * IDEs tend to fight this so I'm sorry.
  */
 
+import Dafny.Aws.Cryptography.Primitives.Types.InternalResult;
 import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction;
 import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error;
 import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy;
@@ -26,13 +27,12 @@
 import dafny.TypeDescriptor;
 import software.amazon.awssdk.core.SdkBytes;
 import software.amazon.cryptography.dbencryptionsdk.dynamodb.ILegacyDynamoDbEncryptor;
-import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative;
 
 import java.util.*;
 import java.util.function.BiConsumer;
 import java.util.stream.Collectors;
 
-public class InternalLegacyOverride {
+public class InternalLegacyOverride extends _ExternBase_InternalLegacyOverride {
   private DynamoDBEncryptor encryptor;
   private Map<String, Set<EncryptionFlags>> actions;
   private EncryptionContext encryptionContext;
@@ -74,7 +74,7 @@ public static TypeDescriptor<InternalLegacyOverride> _typeDescriptor() {
     return TypeDescriptor.referenceWithInitializer(InternalLegacyOverride.class, () -> null);
   }
 
-  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
@@ -95,7 +95,7 @@ public Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencrypto
 
     // 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 {
@@ -135,9 +135,9 @@ public Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencrypto
         .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));
     }
   }
 
@@ -152,7 +152,7 @@ public Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencrypto
     //# and the input item [is an item written in the legacy format](#determining-legacy-items),
     //# this operation MUST fail.
     if (!_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<String, software.amazon.awssdk.services.dynamodb.model.AttributeValue> encryptedItem = software
@@ -191,9 +191,9 @@ public Result<software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencrypto
         .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));
     }
   }
 
@@ -203,7 +203,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()
@@ -214,35 +214,34 @@ 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 = legacyEncryptionContext(encryptorConfig);
-    if (maybeEncryptionContext.is_Failure()) {
-      return Result.create_Failure(maybeEncryptionContext.dtor_error());
+    final InternalResult<EncryptionContext, Error> maybeEncryptionContext = legacyEncryptionContext(encryptorConfig);
+    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(
@@ -262,7 +261,7 @@ public static DafnySequence<Character> ToDafnyString(String s)
     return software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(s);
   }
 
-  public static Result<EncryptionContext, Error> legacyEncryptionContext(
+  public static InternalResult<EncryptionContext, Error> legacyEncryptionContext(
     software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig config
   ) {
     try {
@@ -275,13 +274,13 @@ public static Result<EncryptionContext, Error> legacyEncryptionContext(
         ? encryptionContextBuilder.withRangeKeyName(ToNativeString(config.dtor_sortKeyName().dtor_value())).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> attributeActionsOnEncrypt
   ) {
     try {
@@ -303,12 +302,12 @@ 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.300.2"/>
     <PackageReference Include="AWSSDK.Core" Version="3.7.300.2"/>
-    <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.4.0-SNAPSHOT
-mplDependencyJavaVersion=1.3.0
+mplDependencyJavaVersion=1.3.0-SNAPSHOT
+dafnyVersion=4.2.0
 dafnyRuntimeJavaVersion=4.2.0
 smithyDafnyJavaConversionVersion=0.1