Function encode_cbor_value 

pub open spec fn encode_cbor_value(
    value: CborValueSpec,
) -> (CborHead, Sum<(), Sum<(), Sum<Seq<u8>, Sum<(Seq<Seq<u8>>, u8), Sum<Seq<char>, Sum<(Seq<Seq<char>>, u8), Sum<Seq<CborValueSpec>, Sum<(Seq<CborValueSpec>, u8), Sum<Seq<(CborValueSpec, CborValueSpec)>, Sum<(Seq<(CborValueSpec, CborValueSpec)>, u8), Sum<CborValueSpec, Sum<(), Never>>>>>>>>>>>>)

{
    #[verusfmt::skip]
    match value {
        CborValueSpec::Integer(value) if value >= 0 => {
            (
                CborHead {
                    major: MajorType::Unsigned,
                    value: CborHeadValue::Argument(value as u64),
                },
                L(()),
            )
        }
        CborValueSpec::Integer(value) => {
            (
                CborHead {
                    major: MajorType::Negative,
                    value: CborHeadValue::Argument((-1 - value as int) as u64),
                },
                R(L(())),
            )
        }
        CborValueSpec::Bytes(bytes) => {
            (
                CborHead {
                    major: MajorType::Bytes,
                    value: CborHeadValue::Argument(bytes.len() as u64),
                },
                R(R(L(bytes))),
            )
        }
        CborValueSpec::Text(text) => {
            (
                CborHead {
                    major: MajorType::Text,
                    value: CborHeadValue::Argument(
                        vstd::utf8::encode_utf8(text).len() as u64,
                    ),
                },
                R(R(R(R(L(text))))),
            )
        }
        CborValueSpec::Array(values) => {
            (
                CborHead {
                    major: MajorType::Array,
                    value: CborHeadValue::Argument(values.len() as u64),
                },
                R(R(R(R(R(R(L(values))))))),
            )
        }
        CborValueSpec::Map(entries) => {
            (
                CborHead {
                    major: MajorType::Map,
                    value: CborHeadValue::Argument(entries.len() as u64),
                },
                R(R(R(R(R(R(R(R(L(entries))))))))),
            )
        }
        CborValueSpec::Tag(tag, value) => {
            (
                CborHead {
                    major: MajorType::Tag,
                    value: CborHeadValue::Argument(tag),
                },
                R(R(R(R(R(R(R(R(R(R(L(*value))))))))))),
            )
        }
        CborValueSpec::Float(value) => {
            (
                CborHead {
                    major: MajorType::Simple,
                    value: CborHeadValue::Float(value),
                },
                R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
            )
        }
        CborValueSpec::Bool(value) => {
            (
                CborHead {
                    major: MajorType::Simple,
                    value: CborHeadValue::Simple(if value { 21 } else { 20 }),
                },
                R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
            )
        }
        CborValueSpec::Null => {
            (
                CborHead {
                    major: MajorType::Simple,
                    value: CborHeadValue::Simple(22),
                },
                R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
            )
        }
        CborValueSpec::Undefined => {
            (
                CborHead {
                    major: MajorType::Simple,
                    value: CborHeadValue::Simple(23),
                },
                R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
            )
        }
        CborValueSpec::Simple(value) => {
            (
                CborHead {
                    major: MajorType::Simple,
                    value: CborHeadValue::Simple(value),
                },
                R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
            )
        }
    }
}