reformulate informal spec of Bitwalker_Poke
reformulate comments
describe loop invariants of Bitwalker_Poke
just an empty line added