Finish the soundness proof of the new shallow executor

[skeuchel]

The new shallow executor currently residing in theories/Staging/NewShallow/Executor.v uses separation logic propositions directly and does away with a shallow representation of heaps. Moreover, the soundness of this executor is proven in theories/Staging/NewShallow/IrisInstance.v against the iris instance directly, without going through intermediate Hoare triples.

This new executor is the first step towards producing separation logic-based symbolic verification conditions. It should be useful in itself, for instance in manual verifications like https://github.com/katamaran-project/katamaran/blob/1ff10d9e74e66e89ed9f9729dea041f2d488d7dc/case_study/RiscvPmp/LoopVerification.v#L329-L352

Currently blocked by https://github.com/katamaran-project/katamaran/issues/37