Partial padder output correctness proof

[jadephilipoom]

Another update on the padder proofs:

• All the scariest admits from the invariant-preservation proof are now proven
• Half of the padder output-correctness proof is sketched out with a few admits

Everything seems to be on track so far, although the bit-fiddling is annoying in the is_final case. Mostly automated now, but we could go farther.