Function scan_ascii_digits 

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

{
    if start < bytes.len() && ascii_digit(bytes[start as int]) {
        scan_ascii_digits(bytes, start + 1)
    } else {
        start
    }
}