verif_incr should prove that it restores an uninitialized counter

[andrew-appel]

Let's consider three versions of verif_incr:
(1) master branch (VST 2.14), lib/test/verif_incr
(2) vst_on_iris branch, progs64/verif_incr
(3) vst_on_iris branch, lib/test/verif_incr

Right now, in (1) the proof body_compute2 proves a postcondition in which the counter is recombined from its various split shares. The proof in (2) does not do this, it has a postcondition of simply "main_post" which does not care about the SEP clause.

To port VSTlib to VST 3.0, I copied the body_main proof from (2) into the body_compute proof in (3), but there's an admit at the very end for the recombining of shares. @mansky1 , can you fix this in lib/test/verif_incr?

While you're at it, you could refactor the program and proof in progs64/verif_incr with a compute function as in lib/test/verif_incr. Eventually, we should eliminate the duplication between these two copies of verif_incr.

[mansky1]

I believe it's fixed now, and I refactored the progs version to more closely match the lib version (I didn't split out main into a separate file, though).