Assertions to lean on abstract refinement.

We can't prove that the caller cap must be a reply cap or that
the frames mapped in an arbitrary address space are backed by caps
without appealing to the abstract invariants, which means yet more
assertions in haskell and work in the abstract/haskell refinement.