Second half of invariant-preservation proof is now written (with some admits). I tried making an intermediate specification that was essentially a Gallina implementation of the padder's step function, but it didn't end up making things much simpler so I determined it wasn't worth its costs in terms of complexity. Next, I'll address the major admits here, and ideally factor any remaining admits into lemmas that have nothing to do with the padder (e.g. facts about N or lists).
Second half of invariant-preservation proof is now written (with some admits). I tried making an intermediate specification that was essentially a Gallina implementation of the padder's step function, but it didn't end up making things much simpler so I determined it wasn't worth its costs in terms of complexity. Next, I'll address the major admits here, and ideally factor any remaining admits into lemmas that have nothing to do with the padder (e.g. facts about
Nor lists).