Function axiom_bitvec_len_bound 

pub broadcast proof fn axiom_bitvec_len_bound<T: BitStore, O: BitOrder>(bv: &BitVec<T, O>)

requires

obeys_bitvec_model::<T, O>(),

ensures

bitvec_view(bv).len() <= (usize::MAX as int) / 8,

Bit length is bounded by BitSlice::<T, O>::MAX_BITS (= usize::MAX >> 3).