Function is_printable_byte 

pub open spec fn is_printable_byte(b: u8) -> bool

{
    ||| (0x41 <= b <= 0x5a)
    ||| (0x61 <= b <= 0x7a)
    ||| (0x30 <= b <= 0x39)
    ||| b == 0x20
    ||| b == 0x27
    ||| b == 0x28
    ||| b == 0x29
    ||| b == 0x2b
    ||| b == 0x2c
    ||| b == 0x2d
    ||| b == 0x2e
    ||| b == 0x2f
    ||| b == 0x3a
    ||| b == 0x3d
    ||| b == 0x3f

}