add LeftBit64 macro
fix macro LeftBit64
add new function PokeBitInBytes3
add missing parentheses
activate more loop invariants