Skip to content

Commit

Permalink
More static Java helpers out of extern classes
Browse files Browse the repository at this point in the history
  • Loading branch information
@robin-aws
robin-aws committed Oct 11, 2024
1 parent 8931e27 commit 9d94dda
Show file tree
Hide file tree
Showing 2 changed files with 42 additions and 41 deletions.
56 changes: 28 additions & 28 deletions DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}

}
27 changes: 14 additions & 13 deletions ...y/dbencryptionsdk/dynamodb/itemencryptor/internaldafny/legacy/InternalLegacyOverride.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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.")
);
}
Expand Down Expand Up @@ -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));
}
}

Expand All @@ -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.")
);
}
Expand Down Expand Up @@ -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));
}
}

Expand All @@ -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();
Expand All @@ -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<
Expand All @@ -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 =
Expand All @@ -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)
);
}

Expand Down

0 comments on commit 9d94dda

Please sign in to comment.