def com_amazonaws_kms_CreateKeyRequest()

in ComAmazonawsKms/runtimes/python/src/aws_cryptography_internal_kms/smithygenerated/com_amazonaws_kms/aws_sdk_to_dafny.py [0:0]
136 lines of code
17 McCabe index (conditional complexity)

def com_amazonaws_kms_CreateKeyRequest(native_input):
    return DafnyCreateKeyRequest(
        Policy=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[iter(native_input["Policy"].encode("utf-16-be"))] * 2
                            )
                        ]
                    )
                )
            )
            if "Policy" 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()
        ),
        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()
        ),
        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()
        ),
        BypassPolicyLockoutSafetyCheck=(
            Option_Some(native_input["BypassPolicyLockoutSafetyCheck"])
            if "BypassPolicyLockoutSafetyCheck" in native_input.keys()
            else Option_None()
        ),
        Tags=(
            Option_Some(
                Seq(
                    [
                        aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_Tag(
                            list_element
                        )
                        for list_element in native_input["Tags"]
                    ]
                )
            )
            if "Tags" in native_input.keys()
            else Option_None()
        ),
        MultiRegion=(
            Option_Some(native_input["MultiRegion"])
            if "MultiRegion" in native_input.keys()
            else Option_None()
        ),
        XksKeyId=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[iter(native_input["XksKeyId"].encode("utf-16-be"))]
                                * 2
                            )
                        ]
                    )
                )
            )
            if "XksKeyId" in native_input.keys()
            else Option_None()
        ),
    )