Got simuliris automation working quite okay now.

theories/examples/external/simuliris/paper.v

@@ -18,68 +18,93 @@ From iris_automation.examples.external.simuliris Require Import simuliris_automa
 From iris_automation.symb_exec Require Import defs.
 From iris_automation Require Import solve_defs proofmode_base lib.intuitionistically.
 
+Global Opaque update_si update_si_strong.
+
+
+Section collect_modal.
+  Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
+  Context {Λ : language}.
+  Context {s : simulirisGS PROP Λ}.
+
+  Global Instance collect_modal_update_si_strong (P : PROP) e π  :
+    CollectModal (update_si_strong e π P) (update_si_strong e π) P | 45.
+  Proof. rewrite /CollectModal //. Qed.
+
+  Global Instance collect_modal_update_si_strong_twice (P : PROP) e π  :
+    CollectModal (update_si_strong e π (update_si_strong e π P)) (update_si_strong e π) P | 40.
+  Proof using BiAffine0.
+    rewrite /CollectModal. apply: anti_symm. 
+    - iMod 1. by do 2 (iApply update_si_stronger_update_si_strong; iApply mod_weaker).
+    - by iMod 1.
+  Qed.
+
+  Global Instance collect_modal_update_si_strong_bupd (P : PROP) e π  :
+    CollectModal (update_si_strong e π (|==> P)) (update_si_strong e π) P | 40.
+  Proof using BiAffine0.
+    rewrite /CollectModal. apply: anti_symm. 
+    - iMod 1. (iApply update_si_stronger_update_si_strong; iApply mod_weaker). iStepsS.
+    - iMod 1 as ">HP". (iApply update_si_stronger_update_si_strong; iApply mod_weaker). iStepsS.
+  Qed.
+End collect_modal.
+
 Section temp.
   Context `{!sheapGS Σ, !sheapInv Σ}.
 
-  Global Instance left_execution_abduct p H P e R K e_in' T e_out' MT MT' R' :
-    AsExecutionOf P left_execute e R →
-    ReshapeExprAnd expr e K e_in' (ReductionTemplateStep target_red_cond T H TargO e_in' e_out' MT) →
-    SatisfiesContextCondition context_as_item_condition K →
-    SatisfiesTemplateCondition mono_template_condition R MT R' MT' →
-    Abduct (TT := [tele]) p H P id (MT' $ flip left_execute R' ∘ K ∘ e_out').
-  Proof. intros. eapply execution_abduct_lem => //; [iSolveTC| done]. Qed.
-
-  Global Instance right_execution_abduct p H P e R K e_in' T e_out' MT MT' R' :
-    AsExecutionOf P right_execute e R →
-    ReshapeExprAnd expr e K e_in' (ReductionTemplateStep source_red_cond T H TargO e_in' e_out' MT) →
-    SatisfiesContextCondition context_as_item_condition K →
-    SatisfiesTemplateCondition mono_template_condition R MT R' MT' →
-    Abduct (TT := [tele]) p H P id (MT' $ flip right_execute R' ∘ K ∘ e_out').
-  Proof. intros. eapply execution_abduct_lem => //; [iSolveTC| done]. Qed.
-
-  Global Instance items_valid_context K : SatisfiesContextCondition context_as_item_condition (fill K).
-  Proof. by econstructor. Qed.
-
-  Global Instance templateM_satisfies_wp_template_condition (TT : tele) (R : TT) n (PROP : bi) (M1 : PROP → PROP) M2 TT1 TT2 Ps Qs :
-    ModalityMono M1 → 
-    ModalityMono M2 → 
-    SatisfiesTemplateCondition mono_template_condition R (template_M n M1 M2 TT1 TT2 Ps Qs) R (template_M n M1 M2 TT1 TT2 Ps Qs).
-  Proof.
-    rewrite /SatisfiesTemplateCondition /= => HM1 HM2.
-    split => //.
-    by apply template_M_is_mono.
-  Qed. About sim_val.
-
-  Global Instance refines_values_abduct v1 v2 π Φ:
-    Abduct (TT := [tele]) false empty_hyp_first (Val v1 ⪯{π} Val v2 {{Φ}} )%I id (|==> Φ v1 v2) | 10.
+  Global Instance sim_call_abd π Φ fname arg_l arg_lv el Kl el_f er Kr er_f arg_r arg_rv :
+    ReshapeExprAnd expr el Kl el_f (
+      TCAnd (TCEq el_f (Call f#fname arg_l)) $
+      TCAnd (TCEq (to_val arg_l) (Some arg_lv)) $
+      ReshapeExprAnd expr er Kr er_f (
+        TCAnd (TCEq er_f (Call f#fname arg_r)) $
+               TCEq (to_val arg_r) (Some arg_rv)
+      )
+    ) →
+    SatisfiesContextCondition context_as_item_condition Kl →
+    SatisfiesContextCondition context_as_item_condition Kr →
+    Abduct (TT := [tele]) false empty_hyp_first (el ⪯{π} er [{Φ}])%I id 
+        (update_si_strong (Kr $ Call f#fname arg_r) π (ext_rel π arg_lv arg_rv ∗ 
+        (∀ v_t' v_s', ext_rel π v_t' v_s' -∗ (Kl (of_val v_t') ⪯{π} Kr (of_val v_s') [{Φ}])))) | 10.
   Proof.
-    rewrite /Abduct /= empty_hyp_first_eq left_id. iStepsS. iApply bupd_sim. by iApply sim_value.
+    rewrite /Abduct /= empty_hyp_first_eq left_id. iStepsS.
+    destruct x as [-> [-> [Hlv [-> [-> Hrv]]]]].
+    destruct x0 as [Kl Kl' HKl'].
+    destruct x1 as [Kr Kr' HKr'].
+    rewrite -HKl' -HKr'.
+    iApply sim_update_si_strong.
+    iStopProof. apply util_classes.modality_mono.
+    iStepS. iApply sim_bind.
+    iApply (sim_call with "H1") => //.
+    - rewrite Hlv //.
+    - rewrite Hrv //.
+    - simpl.
+      iStepsS. rewrite HKl' HKr'. iStepsS.
   Qed.
 
 End temp.
 
-Ltac find_reshape e K e' TC :=
-  lazymatch e with
-  | fill ?Kabs ?e_inner =>
-    reshape_expr e_inner ltac:(fun K' e'' => 
-      unify K (fill Kabs ∘ fill K'); unify e' e'';
-      notypeclasses refine (ConstructReshape e (fill Kabs ∘ fill K') e'' _ (eq_refl) _); iSolveTC )
-  | _ =>
-    reshape_expr e ltac:(fun K' e'' => 
-      unify K (fill K'); unify e' e''; 
-      notypeclasses refine (ConstructReshape e (fill K') e'' _ (eq_refl) _); iSolveTC )
-  end.
-
-Global Hint Extern 4 (ReshapeExprAnd expr ?e ?K ?e' ?TC) => 
-  find_reshape e K e' TC : typeclass_instances.
-
-Global Hint Extern 4 (ReshapeExprAnd (language.expr ?L) ?e ?K ?e' ?TC) =>
-  unify L simp_lang;
-  find_reshape e K e' TC : typeclass_instances.
 
 Section fix_bi.
   Context `{!simpleGS Σ}.
 
+  Existing Instance load_na_step_source.
+  Existing Instance load_na_step_target.
+
+  Instance bij_insert l_t l_s v_t v_s :
+    BiAbd (TTl := [tele]) (TTr := [tele]) false (l_t ↦t v_t) (l_t ↔h l_s)%I (update_si)
+    (l_s ↦s v_s ∗ †l_t…t 1 ∗ †l_s…s 1 ∗ val_rel v_t v_s)%I (l_t ↔h l_s)%I.
+  Proof.
+    rewrite /BiAbd /=.
+    iStepS. Transparent update_si.
+    rewrite /update_si.
+    iIntros (?????) "(HP_t & HP_s & Hσ_t & Hσ_s & (%L&Hinv&#Hgs))".
+    iMod (heapbij_insertN _ l_t l_s [v_t] [v_s] 1 with "Hinv [H1] [H2] [H5] [H3] [H4]") as "[Hb #Ha]"; try (done || eauto).
+    - by rewrite heap_mapsto_vec_singleton.
+    - by rewrite heap_mapsto_vec_singleton.
+    - simpl. iStepsS.
+    - iFrame "# ∗". iStepsS.
+  Qed.
+  Typeclasses Opaque loc_rel heap_freeable.
+
   (** Example from 2.1 *)
   Definition ex_2_1_unopt : expr := let: "y" := ref(#42) in !"y".
   Definition ex_2_1_opt : expr := let: "y" := ref(#42) in #42.
@@ -88,7 +113,7 @@ Section fix_bi.
     ⊢ {{{ True }}} ex_2_1_opt ⪯[π] ex_2_1_unopt {{{ lift_post (λ v_t v_s, ⌜v_t = v_s⌝) }}}.
   Proof.
     iIntros "!> _". rewrite /ex_2_1_opt /ex_2_1_unopt.
-    iStepsS. (* simpl_subst. ??  don't know why this is a thing *)
+    iStepsS.
   Qed.
 
   (* for completeness : log_rel as described in Sec 4 *)
@@ -113,15 +138,13 @@ Section fix_bi.
     ⊢ {{{ True }}} ex_2_2_1_opt ⪯[π] ex_2_2_1_unopt {{{ lift_post (λ v_t v_s, ⌜v_t = v_s⌝) }}}.
   Proof.
     iIntros "!> _". rewrite /ex_2_2_1_opt /ex_2_2_1_unopt.
-    iStepsS. simpl_subst.
-    sim_bind (Call _ _) (Call _ _). iApply sim_call; [done..|]. iStepsS.
+    iStepsS.
   Qed.
 
   Lemma ex_2_2_1_log :
     ⊢ log_rel ex_2_2_1_opt ex_2_2_1_unopt.
   Proof.
-    log_rel. iStepsS. simpl_subst.
-    sim_bind (Call _ _) (Call _ _). iApply sim_call; [done..|]. iStepsS.
+    log_rel. iStepsS.
   Qed.
 
   (** Second example from 2.2 *)
@@ -136,41 +159,24 @@ Section fix_bi.
     Call f#"f" "y";;
     !"y" + "z".
 
-Typeclasses Opaque heap_freeable.
-
   Lemma ex_2_2_2 π :
     ⊢ {{{ True }}} ex_2_2_2_opt ⪯[π] ex_2_2_2_unopt {{{ lift_post (λ v_t v_s, ⌜v_t = v_s⌝) }}}.
   Proof.
     iIntros "!> _". rewrite /ex_2_2_2_opt /ex_2_2_2_unopt.
-    iStepsS. simpl_subst. iStepsS. simpl_subst.
-    (* escape locations *)
-    iApply (sim_bij_insert with "H4 H2 H3 H1 []"); first done.
-    iIntros "#Hb".
-    sim_bind (Call _ _) (Call _ _). iApply sim_call; [done..|].
-    iIntros (??) "_". iApply lift_post_val.
-    sim_pures. About sim_bij_insert. sim_load v_t v_s as "Hv".
-    (* [omitted in the description in the paper] we use source UB to know that the loaded values must be integers *)
-    iApply sim_safe_implies. iIntros "[(%n & ->) _]".
-    val_discr_source "Hv". sim_pures. sim_val. done.
-  Qed. *) Abort.
+    iStepsS. sim_load v_t v_s as "Hv".
+    iStepS.
+    iStepS. Arguments gen_val_rel : simpl nomatch.
+    iStepS. val_discr_source "Hv".
+    iStepsS.
+  Qed.
 
   Lemma ex_2_2_2_log :
     ⊢ log_rel ex_2_2_2_opt ex_2_2_2_unopt.
   Proof.
-    log_rel. iModIntro. iIntros (π) "_".
-    source_alloc l_s as "Hl_s" "Hf_s". simpl. cbn. cbn. simpl. simpl. cbn.
-unfold heap_freeable.
-    target_alloc l_t as "Hl_t" "Hf_t".
-    source_load. sim_pures.
-    (* escape locations *)
-    iApply (sim_bij_insert with "Hf_t Hf_s Hl_t Hl_s []"); first done.
-    iIntros "#Hb".
-    sim_bind (Call _ _) (Call _ _). iApply sim_call; [done..|].
-    iIntros (??) "_". iApply lift_post_val.
-    sim_pures. sim_load v_t v_s as "Hv".
-    (* [omitted in the description in the paper] we use source UB to know that the loaded values must be integers *)
-    iApply sim_safe_implies. iIntros "[(%n & ->) _]".
-    val_discr_source "Hv". sim_pures. sim_val. done.
+    log_rel. iStepsS.
+    sim_load v_t v_s as "Hv".
+    do 3 iStepS.
+    val_discr_source "Hv". iStepsS.
   Qed.
 
   (** Example from 2.3 *)
@@ -190,73 +196,85 @@ unfold heap_freeable.
     let: "z" := "x" `quot` "y" in
     Call f#"g" "z".
 
+  Lemma eval_quot_cond (x y : Z) (r : val) :
+    y ≠ 0 →
+    r = #(x `quot` y) →
+    bin_op_eval QuotOp #x #y = Some r.
+  Proof.
+    rewrite /bin_op_eval => Hx -> /=.
+    rewrite decide_False //.
+  Qed.
+
+  Hint Extern 4 (vals_compare_safe _ _) => (left; pure_solver.trySolvePure || right; pure_solver.trySolvePure) : solve_pure_add. 
+  Hint Extern 4 (bin_op_eval QuotOp _ _ = Some _) => apply eval_quot_cond; pure_solver.trySolvePure : solve_pure_eq_add.
+
+Lemma W_tac_to_expr_subst' :
+∀ (x : string) (v : val) (e : expr) (P : expr → Prop) (e' : W.expr) e'',
+  e = W.to_expr e' → (∀ v, W.subst x v e' = e'' v) → P (W.to_expr $ e'' v) → P (subst x v e).
+Proof.
+  intros. specialize (H0 v).
+  eapply W.tac_to_expr_subst => //.
+Qed.
+
+Lemma W_tac_to_expr_combine_subst_map' v :
+∀ (e : val → W.expr) (P : expr → Prop) e', (∀ v, W.combine_subst_map [] (e v) = (e' v)) → P (W.to_expr $ e' v) → P (W.to_expr $ e v).
+Proof.
+  intros. specialize (H v).
+  eapply W.tac_to_expr_combine_subst_map => //.
+Qed.
+
+Ltac simpl_subst' :=
+  repeat match goal with
+    | |- context C [apply_func ?fn ?v] =>
+      (* Unfold [apply_func] if the function's components are available *)
+      let arg := open_constr:(_ : string) in
+      let body := open_constr:(_ : expr) in
+      unify fn (arg, body);
+      change (apply_func fn v) with (subst arg v body)
+    end;
+  repeat match goal with
+    | |- context C [subst ?x ?v ?e] =>
+      lazymatch e with
+      | subst _ _ _ => fail
+      | _ => idtac
+      end;
+      pattern (subst x v e);
+      let e' := W.of_expr e in
+      simple refine (W_tac_to_expr_subst' _ _ _ _ e' _ _ _ _); [ shelve
+      | simpl; rewrite ?list_to_map_to_list; reflexivity
+      | intros ?; vm_compute W.subst; reflexivity
+      |];
+      simple refine (W_tac_to_expr_combine_subst_map' _ _ _ _ _ _); [ shelve
+      | intros ?; vm_compute W.combine_subst_map; reflexivity
+      | ];
+      simpl
+    end.
+
+
+Hint Extern 3 (SimplSubst ?e ?e') =>
+  simpl; simpl_subst'; reflexivity : typeclass_instances.
+
   Lemma ex_2_3 π :
     ⊢ {{{ True }}} ex_2_3_opt ⪯[π] ex_2_3_unopt {{{ lift_post (λ v_t v_s, True) }}}.
   Proof.
     iIntros "!> _". rewrite /ex_2_3_opt /ex_2_3_unopt.
-
-    sim_bind (Call _ _) (Call _ _). iApply sim_call; [ done.. | ].
-    iIntros (p_t p_s) "Hv". iApply lift_post_val.
-    sim_pures.
-    source_bind (Fst _).
-    (* exploit source UB to know that the returned vlaue is a pair *)
-    iApply source_red_safe_implies. iIntros "(%x_s & %y_s & ->)".
-    iPoseProof (gen_val_rel_pair_source with "Hv") as "(%x_t & %y_t & -> & Hx_r & Hy_r)".
-    source_pures. sim_pures.
-    (* exploit source UB for the division *)
-    source_bind (_ `quot` _)%E.
-    iApply source_red_safe_implies. iIntros "[(%x & ->) (%y & -> & %Hy)]".
-    (* reduce the divisions *)
-    source_pure _.
-    { rewrite /bin_op_eval. simpl.
-      destruct (decide (y = 0%Z)) as [-> | _]; first done. reflexivity.
-    }
-    val_discr_source "Hx_r". val_discr_source "Hy_r".
-    target_pure _.
-    { rewrite /bin_op_eval. simpl.
-      destruct (decide (y = 0%Z)) as [-> | _]; first done. reflexivity.
-    }
-    simpl. generalize (Z.quot x y) => nz.
-    sim_pures.
-    (* use the gained knowledge *)
-    rewrite bool_decide_false; first last.
-    { contradict Hy. by simplify_eq. }
-    sim_pures. iApply sim_call; [ done.. | ].
-    iIntros (??) "?". iApply lift_post_val. done.
+    iStepsS.
+    iPoseProof (gen_val_rel_pair_source with "H1") as "(%x_t & %y_t & -> & Hx_r & Hy_r)".
+    val_discr_source "Hx_r".
+    val_discr_source "Hy_r".
+    iStepsS. rewrite bool_decide_eq_false_2; last first. { contradict H. by simplify_eq. }
+    iStepsS.
   Qed.
 
   Lemma ex_2_3_log :
     ⊢ log_rel ex_2_3_opt ex_2_3_unopt.
   Proof.
-    log_rel. iModIntro. iIntros (π) "_".
-    sim_bind (Call _ _) (Call _ _). iApply sim_call; [ done.. | ].
-    iIntros (p_t p_s) "Hv". iApply lift_post_val.
-    sim_pures.
-    source_bind (Fst _).
-    (* exploit source UB to know that the returned vlaue is a pair *)
-    iApply source_red_safe_implies. iIntros "(%x_s & %y_s & ->)".
-    iPoseProof (gen_val_rel_pair_source with "Hv") as "(%x_t & %y_t & -> & Hx_r & Hy_r)".
-    source_pures. sim_pures.
-    (* exploit source UB for the division *)
-    source_bind (_ `quot` _)%E.
-    iApply source_red_safe_implies. iIntros "[(%x & ->) (%y & -> & %Hy)]".
-    (* reduce the divisions *)
-    source_pure _.
-    { rewrite /bin_op_eval. simpl.
-      destruct (decide (y = 0%Z)) as [-> | _]; first done. reflexivity.
-    }
-    val_discr_source "Hx_r". val_discr_source "Hy_r".
-    target_pure _.
-    { rewrite /bin_op_eval. simpl.
-      destruct (decide (y = 0%Z)) as [-> | _]; first done. reflexivity.
-    }
-    simpl. generalize (Z.quot x y) => nz.
-    sim_pures.
-    (* use the gained knowledge *)
-    rewrite bool_decide_false; first last.
-    { contradict Hy. by simplify_eq. }
-    sim_pures. iApply sim_call; [ done.. | ].
-    iIntros (??) "H". iApply lift_post_val. iFrame.
+    log_rel. iStepsS.
+    iPoseProof (gen_val_rel_pair_source with "H2") as "(%x_t & %y_t & -> & Hx_r & Hy_r)".
+    val_discr_source "Hx_r".
+    val_discr_source "Hy_r".
+    iStepsS. rewrite bool_decide_eq_false_2; last first. { contradict H. by simplify_eq. }
+    iStepsS.
   Qed.
 
   (** Example from 2.4 *)
@@ -276,9 +294,7 @@ unfold heap_freeable.
     ⊢ {{{ True }}} ex_2_4_opt ⪯[π] ex_2_4_unopt {{{ lift_post (λ v_t v_s, True) }}}.
   Proof.
     iIntros "!> _". rewrite /ex_2_4_opt /ex_2_4_unopt.
-    source_alloc l_s as "Hl_s" "Hf_s".
-    target_alloc l_t as "Hl_t" "Hf_t".
-    target_load. sim_pures.
+    iStepsS. rename x into l_s. rename x0 into l_t.
 
     (* initiate coinduction with the following invariant:
       (compared with the paper version, we carry through the right to deallocate,
@@ -286,74 +302,23 @@ unfold heap_freeable.
         the loop)
     *)
     set inv := (†l_s…s 1 ∗ †l_t…t 1 ∗ l_s ↦s #0 ∗ l_t ↦t #0)%I.
-    iApply (sim_while_while inv with "[$Hf_s $Hl_s $Hf_t $Hl_t]").
-    iModIntro.
-    iIntros "(? & ? & Hl_s & Hl_t)".
-    (* loop condition *)
-    source_load.
-    sim_bind (Call _ _) (Call _ _).
-    iApply sim_call; [done..|].
-    iIntros (v_t v_s) "Hv". iApply lift_post_val.
-    (* retval must be bool *)
-    iApply sim_safe_implies. iIntros "(%b & ->)".
-    val_discr_source "Hv".
-
-    (* CA on loop condition *)
-    destruct b.
-    - (* true, do a loop iteration *)
-      sim_pures. source_load.
-      sim_bind (Call _ _) (Call _ _).
-      iApply sim_call;[done..|].
-      iIntros (??) "_"; iApply lift_post_val.
-      sim_pures.
-      (* use the coinduction hypothesis *)
-      iApply sim_expr_base.
-      iRight. iFrame. done.
-    - (* false, done with the loop *)
-      sim_pures. iApply sim_expr_base. iLeft.
-      iApply lift_post_val. done.
+    iApply (sim_while_while inv with "[$H1 $H2 $H3 $H4]").
+    iStepsS.
+    val_discr_source "H6".
+    destruct x1; iStepsS.
+    iApply sim_expr_base. iSmash.
   Qed.
 
   Lemma ex_2_4_log :
     ⊢ log_rel ex_2_4_opt ex_2_4_unopt.
   Proof.
-    log_rel. iModIntro. iIntros (π) "_".
-    source_alloc l_s as "Hl_s" "Hf_s".
-    target_alloc l_t as "Hl_t" "Hf_t".
-    target_load. sim_pures.
-
-    (* initiate coinduction with the following invariant:
-      (compared with the paper version, we carry through the right to deallocate,
-        for a more realistic example we might use that to deallocate the locations after
-        the loop)
-    *)
+    log_rel. iStepsS.  rename x0 into l_s. rename x1 into l_t.
     set inv := (†l_s…s 1 ∗ †l_t…t 1 ∗ l_s ↦s #0 ∗ l_t ↦t #0)%I.
-    iApply (sim_while_while inv with "[$Hf_s $Hl_s $Hf_t $Hl_t]").
-    iModIntro.
-    iIntros "(? & ? & Hl_s & Hl_t)".
-    (* loop condition *)
-    source_load.
-    sim_bind (Call _ _) (Call _ _).
-    iApply sim_call; [done..|].
-    iIntros (v_t v_s) "Hv". iApply lift_post_val.
-    (* retval must be bool *)
-    iApply sim_safe_implies. iIntros "(%b & ->)".
-    val_discr_source "Hv".
-
-    (* CA on loop condition *)
-    destruct b.
-    - (* true, do a loop iteration *)
-      sim_pures. source_load.
-      sim_bind (Call _ _) (Call _ _).
-      iApply sim_call;[done..|].
-      iIntros (??) "_"; iApply lift_post_val.
-      sim_pures.
-      (* use the coinduction hypothesis *)
-      iApply sim_expr_base.
-      iRight. iFrame. done.
-    - (* false, done with the loop *)
-      sim_pures. iApply sim_expr_base. iLeft.
-      iApply lift_post_val. done.
+    iApply (sim_while_while inv with "[$H5 $H2 $H3 $H4]").
+    iStepsS.
+    val_discr_source "H7".
+    destruct x2; iStepsS.
+    iApply sim_expr_base. iSmash.
   Qed.
 
 End fix_bi.

theories/examples/external/simuliris/simuliris_automation_base.v

@@ -25,10 +25,23 @@ Global Instance context_as_item_condition : ContextCondition expr := λ K, conte
 
 Global Arguments context_as_item_condition K /.
 
+Global Instance items_valid_context K : SatisfiesContextCondition context_as_item_condition (fill K).
+Proof. by econstructor. Qed.
+
 Global Instance mono_template_condition {PROP : bi} {TT : tele} : 
   TemplateCondition PROP TT
   := (λ A R M R' M', template_mono M ∧ R = R' ∧ M = M').
 
+Global Instance templateM_satisfies_wp_template_condition (TT : tele) (R : TT) n (PROP : bi) (M1 : PROP → PROP) M2 TT1 TT2 Ps Qs :
+  ModalityMono M1 → 
+  ModalityMono M2 → 
+  SatisfiesTemplateCondition mono_template_condition R (template_M n M1 M2 TT1 TT2 Ps Qs) R (template_M n M1 M2 TT1 TT2 Ps Qs).
+Proof.
+  rewrite /SatisfiesTemplateCondition /= => HM1 HM2.
+  split => //.
+  by apply template_M_is_mono.
+Qed.
+
 Section target_executor.
   Context `{!sheapGS Σ, sheapInv Σ}.
 
@@ -140,14 +153,182 @@ Section executor.
     iApply sim_expr_mono; last done. eauto.
   Qed.
 
-  Global Instance as_right_execute el er π Φ : AsExecutionOf (el ⪯{π} er [{ Φ }]) right_execute er [tele_arg el; π; Φ].
+  Global Instance as_right_execute el er π Φ : AsExecutionOf (el ⪯{π} er [{ Φ }]) right_execute er [tele_arg el; π; Φ] | 10.
   Proof. done. Qed.
 
-  Global Instance as_left_execute el er π Φ : AsExecutionOf (el ⪯{π} er [{ Φ }]) left_execute el [tele_arg er; π; Φ].
+  Global Instance as_left_execute el er π Φ : AsExecutionOf (el ⪯{π} er [{ Φ }]) left_execute el [tele_arg er; π; Φ] | 20.
   Proof. done. Qed.
+
+  Global Instance prepend_strong_update el er π Φ : 
+    PrependModality (el ⪯{π} er [{ Φ }])%I (update_si_strong er π) (el ⪯{π} er [{ Φ }])%I.
+  Proof.
+    rewrite /PrependModality. apply: anti_symm.
+    - iIntros "H". by iApply sim_update_si_strong.
+    - iStepsS.
+  Qed.
 End executor.
 
 
+Section modalities.
+  Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
+  Context {Λ : language}.
+  Context {s : simulirisGS PROP Λ}.
+
+  Global Instance update_si_ec : ModalityEC update_si.
+  Proof.
+    split.
+    - move => P Q HPQ. rewrite /update_si.
+      do 7 iStepS.
+      iSpecialize ("H1" with "H2"). rewrite -HPQ.
+      iStepsS.
+    - move => P Q. rewrite /update_si.
+      do 7 iStepS.
+      iSpecialize ("H1" with "H3"). 
+      iStepsS.
+  Qed.
+
+  Lemma bupd_stronger_update_si (P : PROP) : bupd P ⊢ update_si P.
+  Proof. rewrite /update_si. iStepsS. Qed.
+
+  Lemma update_si_stronger_update_si_strong π e (P : PROP) : update_si P ⊢ update_si_strong π e P.
+  Proof. 
+    do 9 iStepS.
+    iDestruct ("H1" with "H2") as ">[H2 H1]".
+    iStepsS.
+  Qed.
+
+  Global Instance update_si_split : ModalityECCompat3 update_si update_si update_si.
+  Proof.
+    move => P.
+    rewrite /update_si.
+    do 7 iStepS.
+    iDestruct ("H1" with "H2") as ">[H2 H1]".
+    iDestruct ("H1" with "H2") as ">[H1 H2]".
+    iStepsS.
+  Qed.