Function invert_byte 

pub open spec fn invert_byte(b: u8) -> u8

{ !b }