From 9d94dda8e1293964b697c1801de486b2537146bc Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 11 Oct 2024 10:29:58 -0700 Subject: [PATCH] More static Java helpers out of extern classes --- .../src/InternalLegacyOverride.dfy | 56 +++++++++---------- .../legacy/InternalLegacyOverride.java | 27 ++++----- 2 files changed, 42 insertions(+), 41 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy index 0747a009f..7230f02a5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy +++ b/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): Result, 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, Types.Error> { - Failure(error) - } + function method CreateBuildSuccess(value: Option): Result, Types.Error> { + Success(value) + } - static function method CreateInternalLegacyOverrideSome(value: InternalLegacyOverride): Option { - Some(value) - } + function method CreateBuildFailure(error: Types.Error): Result, Types.Error> { + Failure(error) + } - static function method CreateInternalLegacyOverrideNone(): Option { - None - } + function method CreateInternalLegacyOverrideSome(value: InternalLegacyOverride): Option { + Some(value) + } - function method CreateEncryptItemSuccess(value: Types.EncryptItemOutput): Result { - Success(value) - } + function method CreateInternalLegacyOverrideNone(): Option { + None + } - function method CreateEncryptItemFailure(error: Types.Error): Result { - Failure(error) - } + function method CreateEncryptItemSuccess(value: Types.EncryptItemOutput): Result { + Success(value) + } - function method CreateDecryptItemSuccess(value: Types.DecryptItemOutput): Result { - Success(value) - } + function method CreateEncryptItemFailure(error: Types.Error): Result { + Failure(error) + } - function method CreateDecryptItemFailure(error: Types.Error): Result { - Failure(error) - } + function method CreateDecryptItemSuccess(value: Types.DecryptItemOutput): Result { + Success(value) + } + function method CreateDecryptItemFailure(error: Types.Error): Result { + Failure(error) } } diff --git a/DynamoDbEncryption/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/internaldafny/legacy/InternalLegacyOverride.java b/DynamoDbEncryption/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/internaldafny/legacy/InternalLegacyOverride.java index b7ee420dc..6aa168ea8 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/internaldafny/legacy/InternalLegacyOverride.java +++ b/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, 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,7 +204,7 @@ public static Result, Error> Build( // Precondition: The encryptor MUST be a DynamoDBEncryptor if (!isDynamoDBEncryptor(maybeEncryptor)) { - return CreateBuildFailure( + return _ExternBase___default.CreateBuildFailure( createError("Legacy encryptor is not supported") ); } @@ -211,7 +212,7 @@ public static Result, Error> Build( final InternalResult 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, 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, Error> Build( legacyOverride.dtor_policy() ); - return CreateBuildSuccess( - CreateInternalLegacyOverrideSome(internalLegacyOverride) + return _ExternBase___default.CreateBuildSuccess( + _ExternBase___default.CreateInternalLegacyOverrideSome(internalLegacyOverride) ); }