use more bit ops
stuck with coq proof of Poke