Function constructed_bit 

pub open spec fn constructed_bit(constructed: bool) -> u8

{ if constructed { TAG_CONSTRUCTED_MASK } else { 0u8 } }