Function tag_lead_bit 

pub open spec fn tag_lead_bit(tag: Tag) -> u64

{ 1u64 << tag_lead_index(tag) }