Function size_in_range 

pub open spec fn size_in_range<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize>(
    len: nat,
) -> bool

{
    &&& (HAS_MIN ==> MIN as nat <= len)
    &&& (HAS_MAX ==> len <= MAX as nat)

}