Function decimal4 

pub open spec fn decimal4(bytes: Seq<u8>, pos: usize) -> u16

{
    (((bytes[pos as int] - ASCII_0) as u16 * 1000u16)
        + ((bytes[pos + 1] - ASCII_0) as u16 * 100u16)
        + ((bytes[pos + 2] - ASCII_0) as u16 * 10u16)
        + (bytes[pos + 3] - ASCII_0) as u16) as u16
}