rewrite contract of SetBit64
reformulate invariants