Function skip_ascii_spaces 

pub open spec fn skip_ascii_spaces(bytes: Seq<u8>, start: nat) -> nat

{
    if start < bytes.len() && bytes[start as int] == ASCII_SPACE {
        skip_ascii_spaces(bytes, start + 1)
    } else {
        start
    }
}