Function cbor_wire_valid 

pub open spec fn cbor_wire_valid<const DET: bool>(
    wire: (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>>>>>>>>>>>>),
) -> bool

{
    #[verusfmt::skip]
    match wire {
        (
            CborHead { major: MajorType::Unsigned, value: CborHeadValue::Argument(_) },
            L(()),
        ) => true,
        (
            CborHead { major: MajorType::Negative, value: CborHeadValue::Argument(_) },
            R(L(())),
        ) => true,
        (
            CborHead { major: MajorType::Bytes, value: CborHeadValue::Argument(len) },
            R(R(L(bytes))),
        ) => len == bytes.len(),
        (
            CborHead { major: MajorType::Bytes, value: CborHeadValue::Indefinite },
            R(R(R(L(_)))),
        ) => !DET,
        (
            CborHead { major: MajorType::Text, value: CborHeadValue::Argument(len) },
            R(R(R(R(L(text))))),
        ) => len == vstd::utf8::encode_utf8(text).len(),
        (
            CborHead { major: MajorType::Text, value: CborHeadValue::Indefinite },
            R(R(R(R(R(L(_)))))),
        ) => !DET,
        (
            CborHead { major: MajorType::Array, value: CborHeadValue::Argument(len) },
            R(R(R(R(R(R(L(values))))))),
        ) => len == values.len(),
        (
            CborHead { major: MajorType::Array, value: CborHeadValue::Indefinite },
            R(R(R(R(R(R(R(L(_)))))))),
        ) => !DET,
        (
            CborHead { major: MajorType::Map, value: CborHeadValue::Argument(len) },
            R(R(R(R(R(R(R(R(L(entries))))))))),
        ) => len == entries.len(),
        (
            CborHead { major: MajorType::Map, value: CborHeadValue::Indefinite },
            R(R(R(R(R(R(R(R(R(L(_)))))))))),
        ) => !DET,
        (
            CborHead { major: MajorType::Tag, value: CborHeadValue::Argument(_) },
            R(R(R(R(R(R(R(R(R(R(L(_))))))))))),
        ) => true,
        (
            CborHead { major: MajorType::Simple, value },
            R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))),
        ) => {
            match value {
                CborHeadValue::Float(_) => true,
                CborHeadValue::Simple(value) => value <= 23u8 || value >= 32u8,
                _ => false,
            }
        }
        _ => false,
    }
}