add valid_read
finish proof of first loop invariant
finish proof of second loop invariant
add post condition on zero bits