Connecting all the bits of the testing verification proofs

[catalin-hritcu]

We did some bottom-up proving and some top-down proving but the two parts don't really connect yet. On the contrary, there are places where this reveals real incompleteness in the testing which we should actually try to fix.

To some extent we are also suffering from the lack of an end-to-end non-interference proof, but that's the subject of another unfinished development (the one for the JFP paper). This is not about "testing verification".