Fix the block-certainty mechanism

It now actually does what it says on the tin. I also distinguish assumed-execution from certain-execution, which will be important for LFCache2.
Fix handling of assumed loops.

Also add new version of md5sum-spec and printf-spec which need a few more assume-edges now we're more faithful with the certain-block concept.