in DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java [444:494]
public static EncryptedDataKeyDescription EncryptedDataKeyDescription(
software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedDataKeyDescription nativeValue
) {
DafnySequence<? extends Character> keyProviderId;
keyProviderId =
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
nativeValue.keyProviderId()
);
Option<DafnySequence<? extends Character>> keyProviderInfo;
keyProviderInfo =
Objects.nonNull(nativeValue.keyProviderInfo())
? Option.create_Some(
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
nativeValue.keyProviderInfo()
)
)
: Option.create_None(
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
);
Option<DafnySequence<? extends Character>> branchKeyId;
branchKeyId =
Objects.nonNull(nativeValue.branchKeyId())
? Option.create_Some(
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
nativeValue.branchKeyId()
)
)
: Option.create_None(
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
);
Option<DafnySequence<? extends Character>> branchKeyVersion;
branchKeyVersion =
Objects.nonNull(nativeValue.branchKeyVersion())
? Option.create_Some(
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
nativeValue.branchKeyVersion()
)
)
: Option.create_None(
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
);
return new EncryptedDataKeyDescription(
keyProviderId,
keyProviderInfo,
branchKeyId,
branchKeyVersion
);
}