in ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/smithygenerated/com_amazonaws_kms/aws_sdk_to_dafny.py [0:0]
def com_amazonaws_kms_KeyMetadata(native_input):
return DafnyKeyMetadata(
AWSAccountId=(
Option_Some(
Seq(
"".join(
[
chr(int.from_bytes(pair, "big"))
for pair in zip(
*[
iter(
native_input["AWSAccountId"].encode("utf-16-be")
)
]
* 2
)
]
)
)
)
if "AWSAccountId" in native_input.keys()
else Option_None()
),
KeyId=Seq(
"".join(
[
chr(int.from_bytes(pair, "big"))
for pair in zip(
*[iter(native_input["KeyId"].encode("utf-16-be"))] * 2
)
]
)
),
Arn=(
Option_Some(
Seq(
"".join(
[
chr(int.from_bytes(pair, "big"))
for pair in zip(
*[iter(native_input["Arn"].encode("utf-16-be"))] * 2
)
]
)
)
)
if "Arn" in native_input.keys()
else Option_None()
),
CreationDate=(
Option_Some(_dafny.Seq(native_input["CreationDate"].isoformat()))
if "CreationDate" in native_input.keys()
else Option_None()
),
Enabled=(
Option_Some(native_input["Enabled"])
if "Enabled" in native_input.keys()
else Option_None()
),
Description=(
Option_Some(
Seq(
"".join(
[
chr(int.from_bytes(pair, "big"))
for pair in zip(
*[iter(native_input["Description"].encode("utf-16-be"))]
* 2
)
]
)
)
)
if "Description" in native_input.keys()
else Option_None()
),
KeyUsage=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_KeyUsageType(
native_input["KeyUsage"]
)
)
if "KeyUsage" in native_input.keys()
else Option_None()
),
KeyState=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_KeyState(
native_input["KeyState"]
)
)
if "KeyState" in native_input.keys()
else Option_None()
),
DeletionDate=(
Option_Some(_dafny.Seq(native_input["DeletionDate"].isoformat()))
if "DeletionDate" in native_input.keys()
else Option_None()
),
ValidTo=(
Option_Some(_dafny.Seq(native_input["ValidTo"].isoformat()))
if "ValidTo" in native_input.keys()
else Option_None()
),
Origin=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_OriginType(
native_input["Origin"]
)
)
if "Origin" in native_input.keys()
else Option_None()
),
CustomKeyStoreId=(
Option_Some(
Seq(
"".join(
[
chr(int.from_bytes(pair, "big"))
for pair in zip(
*[
iter(
native_input["CustomKeyStoreId"].encode(
"utf-16-be"
)
)
]
* 2
)
]
)
)
)
if "CustomKeyStoreId" in native_input.keys()
else Option_None()
),
CloudHsmClusterId=(
Option_Some(
Seq(
"".join(
[
chr(int.from_bytes(pair, "big"))
for pair in zip(
*[
iter(
native_input["CloudHsmClusterId"].encode(
"utf-16-be"
)
)
]
* 2
)
]
)
)
)
if "CloudHsmClusterId" in native_input.keys()
else Option_None()
),
ExpirationModel=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_ExpirationModelType(
native_input["ExpirationModel"]
)
)
if "ExpirationModel" in native_input.keys()
else Option_None()
),
KeyManager=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_KeyManagerType(
native_input["KeyManager"]
)
)
if "KeyManager" in native_input.keys()
else Option_None()
),
CustomerMasterKeySpec=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_CustomerMasterKeySpec(
native_input["CustomerMasterKeySpec"]
)
)
if "CustomerMasterKeySpec" in native_input.keys()
else Option_None()
),
KeySpec=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_KeySpec(
native_input["KeySpec"]
)
)
if "KeySpec" in native_input.keys()
else Option_None()
),
EncryptionAlgorithms=(
Option_Some(
Seq(
[
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_EncryptionAlgorithmSpec(
list_element
)
for list_element in native_input["EncryptionAlgorithms"]
]
)
)
if "EncryptionAlgorithms" in native_input.keys()
else Option_None()
),
SigningAlgorithms=(
Option_Some(
Seq(
[
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_SigningAlgorithmSpec(
list_element
)
for list_element in native_input["SigningAlgorithms"]
]
)
)
if "SigningAlgorithms" in native_input.keys()
else Option_None()
),
KeyAgreementAlgorithms=(
Option_Some(
Seq(
[
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_KeyAgreementAlgorithmSpec(
list_element
)
for list_element in native_input["KeyAgreementAlgorithms"]
]
)
)
if "KeyAgreementAlgorithms" in native_input.keys()
else Option_None()
),
MultiRegion=(
Option_Some(native_input["MultiRegion"])
if "MultiRegion" in native_input.keys()
else Option_None()
),
MultiRegionConfiguration=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_MultiRegionConfiguration(
native_input["MultiRegionConfiguration"]
)
)
if "MultiRegionConfiguration" in native_input.keys()
else Option_None()
),
PendingDeletionWindowInDays=(
Option_Some(native_input["PendingDeletionWindowInDays"])
if "PendingDeletionWindowInDays" in native_input.keys()
else Option_None()
),
MacAlgorithms=(
Option_Some(
Seq(
[
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_MacAlgorithmSpec(
list_element
)
for list_element in native_input["MacAlgorithms"]
]
)
)
if "MacAlgorithms" in native_input.keys()
else Option_None()
),
XksKeyConfiguration=(
Option_Some(
aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_XksKeyConfigurationType(
native_input["XksKeyConfiguration"]
)
)
if "XksKeyConfiguration" in native_input.keys()
else Option_None()
),
)