def com_amazonaws_kms_GrantListEntry()

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

def com_amazonaws_kms_GrantListEntry(native_input):
    return DafnyGrantListEntry(
        KeyId=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[iter(native_input["KeyId"].encode("utf-16-be"))] * 2
                            )
                        ]
                    )
                )
            )
            if "KeyId" in native_input.keys()
            else Option_None()
        ),
        GrantId=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[iter(native_input["GrantId"].encode("utf-16-be"))] * 2
                            )
                        ]
                    )
                )
            )
            if "GrantId" in native_input.keys()
            else Option_None()
        ),
        Name=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[iter(native_input["Name"].encode("utf-16-be"))] * 2
                            )
                        ]
                    )
                )
            )
            if "Name" 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()
        ),
        GranteePrincipal=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[
                                    iter(
                                        native_input["GranteePrincipal"].encode(
                                            "utf-16-be"
                                        )
                                    )
                                ]
                                * 2
                            )
                        ]
                    )
                )
            )
            if "GranteePrincipal" in native_input.keys()
            else Option_None()
        ),
        RetiringPrincipal=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[
                                    iter(
                                        native_input["RetiringPrincipal"].encode(
                                            "utf-16-be"
                                        )
                                    )
                                ]
                                * 2
                            )
                        ]
                    )
                )
            )
            if "RetiringPrincipal" in native_input.keys()
            else Option_None()
        ),
        IssuingAccount=(
            Option_Some(
                Seq(
                    "".join(
                        [
                            chr(int.from_bytes(pair, "big"))
                            for pair in zip(
                                *[
                                    iter(
                                        native_input["IssuingAccount"].encode(
                                            "utf-16-be"
                                        )
                                    )
                                ]
                                * 2
                            )
                        ]
                    )
                )
            )
            if "IssuingAccount" in native_input.keys()
            else Option_None()
        ),
        Operations=(
            Option_Some(
                Seq(
                    [
                        aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_GrantOperation(
                            list_element
                        )
                        for list_element in native_input["Operations"]
                    ]
                )
            )
            if "Operations" in native_input.keys()
            else Option_None()
        ),
        Constraints=(
            Option_Some(
                aws_cryptography_internal_kms.smithygenerated.com_amazonaws_kms.aws_sdk_to_dafny.com_amazonaws_kms_GrantConstraints(
                    native_input["Constraints"]
                )
            )
            if "Constraints" in native_input.keys()
            else Option_None()
        ),
    )