start with rewriting 8-bit specs
minor formatting
make contract more compact
merge assertions
adapt proof of loop invariant of Bitwalker_Peek
reformulate contract and adapt some proofs