Function sign_bit_set 

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

{ 0x80u8 <= b }