Fix KMS

.github/workflows/library_java_tests.yml

@@ -12,6 +12,7 @@ on:
 jobs:
   testJava:
     strategy:
+      fail-fast: false
       matrix:
         library:
           [

ComAmazonawsKms/runtimes/java/src/main/java/software/amazon/cryptography/services/kms/internaldafny/__default.java

@@ -6,6 +6,7 @@
 import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence;
 import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String;
 
+import StandardLibraryInterop_Compile.WrappersInterop;
 import Wrappers_Compile.Option;
 import Wrappers_Compile.Result;
 import dafny.DafnySequence;
@@ -40,12 +41,12 @@ public static Result<IKMSClient, Error> KMSClient() {
         )
         .build();
       final IKMSClient shim = new Shim(client, region);
-      return Result.create_Success(shim);
+      return CreateSuccessOfClient(shim);
     } catch (Exception e) {
       Error dafny_error = Error.create_KMSInternalException(
         Option.create_Some(CharacterSequence(e.getMessage()))
       );
-      return Result.create_Failure(dafny_error);
+      return CreateFailureOfError(dafny_error);
     }
   }
 
@@ -76,12 +77,12 @@ public static Result<IKMSClient, Error> KMSClientForRegion(
         )
         .build();
       final IKMSClient shim = new Shim(client, regionString);
-      return Result.create_Success(shim);
+      return CreateSuccessOfClient(shim);
     } catch (Exception e) {
       Error dafny_error = Error.create_KMSInternalException(
         Option.create_Some(CharacterSequence(e.getMessage()))
       );
-      return Result.create_Failure(dafny_error);
+      return CreateFailureOfError(dafny_error);
     }
   }
 
@@ -98,14 +99,14 @@ public static Wrappers_Compile.Option<Boolean> RegionMatch(
     // have no way to determine what region it is
     // configured with.
     if (shim.region() == null) {
-      return Option.create_None();
+      return WrappersInterop.CreateBooleanNone());
     }
 
     // Otherwise we kept record of the region
     // when we created the client.
     String shimRegion = shim.region();
     String regionStr = String(region);
-    return Option.create_Some(regionStr.equals(shimRegion));
+    return WrappersInterop.CreateBooleanSome(regionStr.equals(shimRegion));
   }
 
   private static String UserAgentSuffix() {

StandardLibrary/src/WrappersInterop.dfy

@@ -0,0 +1,48 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../../libraries/src/Wrappers.dfy"
+
+//
+// Helper functions for extern code to call in order to create common wrapper types.
+//
+// This is currently necessary to abstract away from differences in TypeDescriptor usage
+// in the Java backend across different versions of Dafny:
+// after Dafny 4.2 methods like Option.create_Some()
+// also require explicit TypeDescriptor arguments.
+// If we declare a `CreateSome<T>(t: T)` function,
+// the compiled version may or may not need a type descriptor,
+// which means externs would need to have different Java code for different Dafny versions.
+// But if we define a non-generic version for a specific type,
+// Dafny will emit the right type descriptor instances inside the compiled method,
+// so the calling signature is the same across Dafny versions.
+//
+// These may be useful for other target languages in the future as well,
+// to similarly abstract away from Dafny compilation internal details.
+//
+// See also DafnyApiCodegen.generateResultOfClientHelperFunctions() in smithy-dafny,
+// which solves the same problem by emitting similar helper methods for each client type.
+//
+module StandardLibraryInterop {
+
+  import opened Wrappers
+
+  class WrappersInterop {
+
+    static function method CreateStringSome(s: string): Option<string> {
+      Some(s)
+    }
+
+    static function method CreateStringNone(): Option<string> {
+      None
+    }
+
+    static function method CreateBooleanSome(b: bool): Option<bool> {
+      Some(b)
+    }
+
+    static function method CreateBooleanNone(): Option<bool> {
+      None
+    }
+  }
+}