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

katamaran/case_study/RiscvPmp/LoopVerification.v

Lines 329 to 352 in 1ff10d9

	Lemma valid_semTriple_loop : ⊢ semTriple_loop.
	Proof.
	iLöb as "H".
	iIntros (m h i mpp entries) "(HStep & HMod & HTrap & HRec)".
	cbn.
	unfold fun_loop.
	iApply (semWP_seq (call step) (call loop)).
	iApply semWP_call_inline_later.
	iApply (semWP_mono with "[HStep]").
	iApply (valid_step_semTriple with "HStep").
	Unshelve. 2: auto.
	iModIntro.
	iIntros (v δ) "[HRes | [HRes | [HRes | HRes]]]";
	iApply (semWP_call_inline loop _).
	- iDestruct "HRes" as "(? & ? & ? & ? & ? & [%i' (? & ?)] & ? & ? & ?)".
	unfold semTriple_loop.
	iApply ("H" $! m h i' mpp entries).
	unfold loop_pre.
	iFrame.
	now iExists i'.
	- iApply ("HMod" with "HRes").
	- iApply ("HTrap" with "HRes").
	- iApply ("HRec" with "HRes").
	Qed.

Currently blocked by #37