More static Java helpers out of extern classes

Author: robin-aws

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy

@@ -22,43 +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)
-    }
+  // 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 CreateBuildFailure(error: Types.Error): Result<Option<InternalLegacyOverride>, Types.Error> {
-      Failure(error)
-    }
+  function method CreateBuildSuccess(value: Option<InternalLegacyOverride>): Result<Option<InternalLegacyOverride>, Types.Error> {
+    Success(value)
+  }
 
-    static function method CreateInternalLegacyOverrideSome(value: InternalLegacyOverride): Option<InternalLegacyOverride> {
-      Some(value)
-    }
+  function method CreateBuildFailure(error: Types.Error): Result<Option<InternalLegacyOverride>, Types.Error> {
+    Failure(error)
+  }
 
-    static function method CreateInternalLegacyOverrideNone(): Option<InternalLegacyOverride> {
-      None
-    }
+  function method CreateInternalLegacyOverrideSome(value: InternalLegacyOverride): Option<InternalLegacyOverride> {
+    Some(value)
+  }
 
-    function method CreateEncryptItemSuccess(value: Types.EncryptItemOutput): Result<Types.EncryptItemOutput, Types.Error> {
-      Success(value)
-    }
+  function method CreateInternalLegacyOverrideNone(): Option<InternalLegacyOverride> {
+    None
+  }
 
-    function method CreateEncryptItemFailure(error: Types.Error): Result<Types.EncryptItemOutput, Types.Error> {
-      Failure(error)
-    }
+  function method CreateEncryptItemSuccess(value: Types.EncryptItemOutput): Result<Types.EncryptItemOutput, Types.Error> {
+    Success(value)
+  }
 
-    function method CreateDecryptItemSuccess(value: Types.DecryptItemOutput): Result<Types.DecryptItemOutput, Types.Error> {
-      Success(value)
-    }
+  function method CreateEncryptItemFailure(error: Types.Error): Result<Types.EncryptItemOutput, Types.Error> {
+    Failure(error)
+  }
 
-    function method CreateDecryptItemFailure(error: Types.Error): Result<Types.DecryptItemOutput, 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

@@ -28,10 +28,11 @@
 import software.amazon.awssdk.core.SdkBytes;
 import software.amazon.cryptography.dbencryptionsdk.dynamodb.ILegacyDynamoDbEncryptor;
 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;
 import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction;
 
+import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.legacy._ExternBase___default;
+
 public class InternalLegacyOverride extends _ExternBase_InternalLegacyOverride {
 
   private DynamoDBEncryptor encryptor;
@@ -95,7 +96,7 @@ > EncryptItem(
   ) {
     // Precondition: Policy MUST allow the caller to encrypt.
     if (!_policy.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT()) {
-      return CreateEncryptItemFailure(
+      return _ExternBase___default.CreateEncryptItemFailure(
         createError("Legacy Policy does not support encrypt.")
       );
     }
@@ -127,9 +128,9 @@ > EncryptItem(
         software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny.EncryptItemOutput(
           nativeOutput
         );
-      return CreateEncryptItemSuccess(dafnyOutput);
+      return _ExternBase___default.CreateEncryptItemSuccess(dafnyOutput);
     } catch (Exception ex) {
-      return CreateEncryptItemFailure(Error.create_Opaque(ex));
+      return _ExternBase___default.CreateEncryptItemFailure(Error.create_Opaque(ex));
     }
   }
 
@@ -149,7 +150,7 @@ > DecryptItem(
       !_policy.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT() &&
       !_policy.is_FORBID__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT()
     ) {
-      return CreateDecryptItemFailure(
+      return _ExternBase___default.CreateDecryptItemFailure(
         createError("Legacy Policy does not support decrypt.")
       );
     }
@@ -180,9 +181,9 @@ > DecryptItem(
         software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny.DecryptItemOutput(
           nativeOutput
         );
-      return CreateDecryptItemSuccess(dafnyOutput);
+      return _ExternBase___default.CreateDecryptItemSuccess(dafnyOutput);
     } catch (Exception ex) {
-      return CreateDecryptItemFailure(Error.create_Opaque(ex));
+      return _ExternBase___default.CreateDecryptItemFailure(Error.create_Opaque(ex));
     }
   }
 
@@ -191,7 +192,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 CreateBuildSuccess(CreateInternalLegacyOverrideNone());
+      return _ExternBase___default.CreateBuildSuccess(_ExternBase___default.CreateInternalLegacyOverrideNone());
     }
     final software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyOverride legacyOverride =
       encryptorConfig.dtor_legacyOverride().dtor_value();
@@ -203,15 +204,15 @@ public static Result<Option<InternalLegacyOverride>, Error> Build(
 
     // Precondition: The encryptor MUST be a DynamoDBEncryptor
     if (!isDynamoDBEncryptor(maybeEncryptor)) {
-      return CreateBuildFailure(
+      return _ExternBase___default.CreateBuildFailure(
         createError("Legacy encryptor is not supported")
       );
     }
     // Preconditions: MUST be able to create valid encryption context
     final InternalResult<EncryptionContext, Error> maybeEncryptionContext =
       legacyEncryptionContext(encryptorConfig);
     if (maybeEncryptionContext.isFailure()) {
-      return CreateBuildFailure(maybeEncryptionContext.error());
+      return _ExternBase___default.CreateBuildFailure(maybeEncryptionContext.error());
     }
     // Precondition: All actions MUST be supported types
     final InternalResult<
@@ -221,7 +222,7 @@ public static Result<Option<InternalLegacyOverride>, Error> Build(
       legacyOverride.dtor_attributeActionsOnEncrypt()
     );
     if (maybeActions.isFailure()) {
-      return CreateBuildFailure(maybeEncryptionContext.error());
+      return _ExternBase___default.CreateBuildFailure(maybeEncryptionContext.error());
     }
 
     final InternalLegacyOverride internalLegacyOverride =
@@ -232,8 +233,8 @@ public static Result<Option<InternalLegacyOverride>, Error> Build(
         legacyOverride.dtor_policy()
       );
 
-    return CreateBuildSuccess(
-      CreateInternalLegacyOverrideSome(internalLegacyOverride)
+    return _ExternBase___default.CreateBuildSuccess(
+            _ExternBase___default.CreateInternalLegacyOverrideSome(internalLegacyOverride)
     );
   }