def com_amazonaws_kms_ReEncryptRequest()

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

def com_amazonaws_kms_ReEncryptRequest(native_input):
    return DafnyReEncryptRequest(
        CiphertextBlob=Seq(native_input["CiphertextBlob"]),
        SourceEncryptionContext=(
            Option_Some(
                Map(
                    {
                        Seq(
                            "".join(
                                [
                                    chr(int.from_bytes(pair, "big"))
                                    for pair in zip(
                                        *[iter(key.encode("utf-16-be"))] * 2
                                    )
                                ]
                            )
                        ): Seq(
                            "".join(
                                [
                                    chr(int.from_bytes(pair, "big"))
                                    for pair in zip(
                                        *[iter(value.encode("utf-16-be"))] * 2
                                    )
                                ]
                            )
                        )
                        for (key, value) in native_input[
                            "SourceEncryptionContext"
                        ].items()
                    }
                )
            )
            if "SourceEncryptionContext" in native_input.keys()
            else Option_None()
        ),
        SourceKeyId=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[iter(native_input["SourceKeyId"].encode("utf-16-be"))]
                                * 2
                            )
                        ]
                    )
                )
            )
            if "SourceKeyId" in native_input.keys()
            else Option_None()
        ),
        DestinationKeyId=Seq(
            "".join(
                [
                    chr(int.from_bytes(pair, "big"))
                    for pair in zip(
                        *[iter(native_input["DestinationKeyId"].encode("utf-16-be"))]
                        * 2
                    )
                ]
            )
        ),
        DestinationEncryptionContext=(
            Option_Some(
                Map(
                    {
                        Seq(
                            "".join(
                                [
                                    chr(int.from_bytes(pair, "big"))
                                    for pair in zip(
                                        *[iter(key.encode("utf-16-be"))] * 2
                                    )
                                ]
                            )
                        ): Seq(
                            "".join(
                                [
                                    chr(int.from_bytes(pair, "big"))
                                    for pair in zip(
                                        *[iter(value.encode("utf-16-be"))] * 2
                                    )
                                ]
                            )
                        )
                        for (key, value) in native_input[
                            "DestinationEncryptionContext"
                        ].items()
                    }
                )
            )
            if "DestinationEncryptionContext" in native_input.keys()
            else Option_None()
        ),
        SourceEncryptionAlgorithm=(
            Option_Some(
                aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_EncryptionAlgorithmSpec(
                    native_input["SourceEncryptionAlgorithm"]
                )
            )
            if "SourceEncryptionAlgorithm" in native_input.keys()
            else Option_None()
        ),
        DestinationEncryptionAlgorithm=(
            Option_Some(
                aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_EncryptionAlgorithmSpec(
                    native_input["DestinationEncryptionAlgorithm"]
                )
            )
            if "DestinationEncryptionAlgorithm" in native_input.keys()
            else Option_None()
        ),
        GrantTokens=(
            Option_Some(
                Seq(
                    [
                        Seq(
                            "".join(
                                [
                                    chr(int.from_bytes(pair, "big"))
                                    for pair in zip(
                                        *[iter(list_element.encode("utf-16-be"))] * 2
                                    )
                                ]
                            )
                        )
                        for list_element in native_input["GrantTokens"]
                    ]
                )
            )
            if "GrantTokens" in native_input.keys()
            else Option_None()
        ),
        DryRun=(
            Option_Some(native_input["DryRun"])
            if "DryRun" in native_input.keys()
            else Option_None()
        ),
    )