Function decode_cbor_wire 

pub open spec fn decode_cbor_wire(
    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>>>>>>>>>>>>),
) -> CborValueSpec

{
    let head = wire.0;
    #[verusfmt::skip]
    match wire.1 {
        L(()) => {
            match head.value {
                CborHeadValue::Argument(value) => CborValueSpec::Integer(value as i128),
                _ => arbitrary(),
            }
        }
        R(L(())) => {
            match head.value {
                CborHeadValue::Argument(value) => {
                    CborValueSpec::Integer((-1 - value as int) as i128)
                }
                _ => arbitrary(),
            }
        }
        R(R(L(bytes))) => CborValueSpec::Bytes(bytes),
        R(R(R(L((chunks, _break))))) => CborValueSpec::Bytes(chunks.flatten()),
        R(R(R(R(L(text))))) => CborValueSpec::Text(text),
        R(R(R(R(R(L((chunks, _break))))))) => CborValueSpec::Text(chunks.flatten()),
        R(R(R(R(R(R(L(values))))))) => CborValueSpec::Array(values),
        R(R(R(R(R(R(R(L((values, _break))))))))) => CborValueSpec::Array(values),
        R(R(R(R(R(R(R(R(L(entries))))))))) => CborValueSpec::Map(entries),
        R(R(R(R(R(R(R(R(R(L((entries, _break))))))))))) => CborValueSpec::Map(entries),
        R(R(R(R(R(R(R(R(R(R(L(value))))))))))) => {
            match head.value {
                CborHeadValue::Argument(tag) => CborValueSpec::Tag(tag, Box::new(value)),
                _ => arbitrary(),
            }
        }
        R(R(R(R(R(R(R(R(R(R(R(L(())))))))))))) => {
            match head.value {
                CborHeadValue::Float(value) => CborValueSpec::Float(value),
                CborHeadValue::Simple(20) => CborValueSpec::Bool(false),
                CborHeadValue::Simple(21) => CborValueSpec::Bool(true),
                CborHeadValue::Simple(22) => CborValueSpec::Null,
                CborHeadValue::Simple(23) => CborValueSpec::Undefined,
                CborHeadValue::Simple(value) => CborValueSpec::Simple(value),
                _ => arbitrary(),
            }
        }
        _ => arbitrary(),
    }
}