Function cbor_value_valid 

pub open spec fn cbor_value_valid(value: CborValueSpec) -> bool

{
    match value {
        CborValueSpec::Integer(value) => (
            &&& value as int >= -1 - u64::MAX as int
            &&& value as int <= u64::MAX as int

        ),
        CborValueSpec::Bytes(bytes) => bytes.len() <= u64::MAX,
        CborValueSpec::Text(text) => vstd::utf8::encode_utf8(text).len() <= u64::MAX,
        CborValueSpec::Array(values) => values.len() <= u64::MAX,
        CborValueSpec::Map(entries) => entries.len() <= u64::MAX,
        CborValueSpec::Simple(value) => value <= 19u8 || value >= 32u8,
        _ => true,
    }
}