Function decimal_4 

pub exec fn decimal_4(bytes: &[u8], pos: usize) -> u16

requires

pos <= usize::MAX - 3,

pos + 3 < bytes.len(),

ascii_digit(bytes@[pos as int]),

ascii_digit(bytes@[pos as int + 1]),

ascii_digit(bytes@[pos as int + 2]),

ascii_digit(bytes@[pos as int + 3]),

returns

decimal4(bytes@, pos),