Strong monotonicity proofs for the new shallow executor

[skeuchel]

The new shallow executor currently only has weak monotonicity proofs like e.g.

katamaran/theories/Staging/NewShallow/Executor.v

Lines 917 to 922 in 1ff10d9

	Instance exec_aux_monotonic :
	Proper (MonotonicCall ==> MonotonicExec) (exec_aux).
	Proof.
	intros ec1 ec2 ec_mon Γ τ s.
	induction s; intros P Q PQ ?; cbn; solve_monotonic.
	Qed.

This monotonicity property is not strong enough to finish the soundness proof of the new shallow executor. We loose the (non-persistent) induction hypothesis from the Löb induction when using it

katamaran/theories/Staging/NewShallow/IrisInstance.v

Lines 896 to 916 in 1ff10d9

	Lemma sound :
	ForeignSem -> LemmaSem -> Shallow.ValidContractCEnv ->
	⊢ Shallow.ValidContractEnvSem semWP.
	Proof.
	intros extSem lemSem vcenv.
	iLöb as "IH".
	iIntros (σs σ f).
	specialize (vcenv σs σ f).
	destruct (CEnv f) as [[Σe δΔ req res ens]|];[|trivial].
	iIntros (ι) "PRE".
	specialize (vcenv _ eq_refl).
	cbn in vcenv.
	rewrite env.Forall_forall in vcenv.
	specialize (vcenv ι).
	rewrite CPureSpecM.wp_produce in vcenv.
	cbn in vcenv.
	iPoseProof (vcenv with "[$] PRE") as "vcenv". clear vcenv.
	iApply (sound_stm extSem lemSem).
	iRevert "vcenv".
	iApply CHeapSpecM.exec_aux_monotonic.
	Abort.

We can probably make this quite structured like the current monotonicity proofs if we build up respectful, forall_relation, pointwise_relation etc. relation constructors up over separation logic propositions. This can probably hugely benefit from #36