Updated reloc, made reloc examples use new hint notation.

reloc @ 324ba2b6

-Subproject commit 762295c3ee2215d73dfee17adcc4f0588a385508
+Subproject commit 324ba2b693c0be414c0d7944702d6687e0c935ef

theories/examples/external/reloc/class_instances_reloc.v

-From iris.bi Require Import bi telescopes.
+From iris.bi Require Import bi telescopes lib.laterable.
 From reloc.logic.proofmode Require Import spec_tactics tactics.
 From reloc.logic Require Import model rules derived.
 From diaframe.symb_exec Require Import defs weakestpre.
@@ -67,7 +67,28 @@ Section tpwp.
   Lemma from_tpwp j e E1 E2 Φ : (|={E1}=> tpwp j e E1 E2 Φ) ⊢ spec_ctx -∗ j ⤇ e ={E1, E2}=∗ Φ.
   Proof. rewrite tpwp_eq /=. iIntros "H #HS Hj". iMod "H". by iApply "H". Qed.
 
-  Lemma from_tpwp_pre_rel j e tl tr E A :
+  Lemma refines_spec_ctx tl (tr : expr) E A :
+    (spec_ctx -∗ (REL tl << tr @ E : A)) ⊢ (REL tl << tr @ E : A).
+  Proof.
+    iIntros "Hrel".
+    rewrite {2}refines_eq /refines_def {1}/refines_right /=.
+    iIntros (j') "[#Hs Htr]".
+    iCombine "Hs Htr" as "Htr".
+    iRevert "Htr".
+    fold (refines_right j' tr).
+    change (refines_right j' tr) with
+      match inl tr : rhs_t with
+      | inl e => refines_right j' e
+      | inr k => ⌜j' = k⌝%I
+      end.
+    set (tr' := inl tr).
+    iRevert (j').
+    fold (refines_def E tl tr' A). rewrite /tr'.
+    rewrite -refines_eq.
+    by iApply "Hrel".
+  Qed.
+
+  Lemma from_tpwp_pre_rel j e tl (tr : expr) E A :
     (|={E}=> tpwp j e E E (REL tl << tr @ E : A)) ⊢ j ⤇ e -∗ REL tl << tr @ E : A%I.
   Proof. 
     rewrite tpwp_eq /=.
@@ -93,7 +114,7 @@ Section reloc_executor.
 
   Global Arguments right_execute e !R /.
 
-  Global Instance as_right_execute tl tr E A : AsExecutionOf (REL tl << tr @ E : A) right_execute tr [tele_arg tl; E; A].
+  Global Instance as_right_execute tl (tr : expr) E A : AsExecutionOf (REL tl << tr @ E : A) right_execute tr [tele_arg tl; E; A].
   Proof. done. Qed.
 
   Instance tp_reduction_condition : ReductionCondition (iPropI Σ) expr coPset :=
@@ -179,12 +200,12 @@ Section reloc_executor.
     move => K e A e' M /= HK R R' M' [<- <-]. destruct HK as [K K' HK]. rewrite -HK.
     drop_telescope R as tl E Φ => /=.
     iIntros "[Hred HM]" => /=.
-    rewrite refines_eq /refines_def.
-    iIntros (j K'') "#H3 H4".
+    rewrite refines_eq /refines_def /=.
+    iIntros (j) "[#H3 H4]".
     rewrite -fill_app.
     iMod ("Hred" with "[$H3 $H4] HM") as (a) "[HP Hj]"; simpl. rewrite -HK.
     rewrite refines_eq /refines_def.
-    iApply "HP" => //.
+    iApply "HP" => //. iFrame "#".
     by rewrite fill_app.
   Qed.
 
@@ -218,7 +239,7 @@ Section reloc_executor.
     by iApply "HP".
   Qed.
 
-  Instance left_execute : ExecuteOp (iPropI Σ) expr [tele_pair expr; coPset; lrel Σ] :=
+  Instance left_execute : ExecuteOp (iPropI Σ) expr [tele_pair rhs_t; coPset; lrel Σ] :=
     λ e, λᵗ tr E A, REL e << tr @ E : A.
 
   Global Arguments left_execute e !R /.
@@ -226,9 +247,9 @@ Section reloc_executor.
   Global Instance as_left_execute tl tr E A : AsExecutionOf (REL tl << tr @ E : A) left_execute tl [tele_arg tr; E; A].
   Proof. done. Qed.
 
-  Instance left_template_condition : TemplateCondition (iPropI Σ) [tele_pair expr; coPset; lrel Σ]
+  Instance left_template_condition : TemplateCondition (iPropI Σ) [tele_pair rhs_t; coPset; lrel Σ]
     := (λ Φ, λᵗ tr E A, λ M, λᵗ tr' E' A', λ M', 
-        (A' = A ∧ tr' = tr ∧ (∀ Ψ, M' (fupd E' ⊤ ∘ Ψ) ⊢ |={E, ⊤}=> M Ψ) ∧ (template_mono M' ∧ template_conditionally_absorbing M' (λ P, Persistent P ∨ Timeless P)))
+        (A' = A ∧ tr' = tr ∧ (∀ Ψ, M' (fupd E' ⊤ ∘ Ψ) ⊢ |={E, ⊤}=> M Ψ) ∧ (template_mono M' ∧ template_conditionally_absorbing M' Laterable))
     ).
 
   Global Arguments left_template_condition A !R M !R' M' /.
@@ -329,25 +350,22 @@ Section reloc_executor.
     drop_telescope R' as tr' E' Φ' => /=.
     move => [-> [-> [HMΨ [HM1 HM2]]]].
     rewrite refines_eq /refines_def /=.
-    iIntros "[Hred HM1]" (j K'') "#H3 H4".
+    iIntros "[Hred HM1]" (j) "Hj".
     rewrite /flip /compose /=.
     rewrite -wp_bind /=.
     iApply "Hred".
-    rewrite -HMΨ.
-    iRevert "H3"; iIntros "-#H3"; iStopProof.
-    rewrite assoc.
-    rewrite HM2; last (right; iSolveTC).
-    rewrite HM2; last (left; iSolveTC).
+    rewrite -HMΨ. iStopProof.
+    erewrite HM2; last (destruct tr; iSolveTC).
     apply HM1 => a /=.
-    iIntros "[[HK Hj] #HS]".
+    iIntros "[HK Hj]".
     rewrite refines_eq /refines_def /=.
-    iMod ("HK" with "HS Hj"). rewrite -HK.
+    iMod ("HK" with "Hj"). rewrite -HK.
     by iApply wp_bind_inv.
   Qed.
 
   Proposition tp_condition_execution_step_general {A B : tele} e1 E1 E2 P e2 Q pre:
     (∀ j K', spec_ctx ∗ j ⤇ fill K' e1 -∗ 
-      ∀.. (a : A), tele_app P a -∗ (|={E2}=> ∃.. (b : B), j ⤇ fill K' (tele_app (tele_app e2 a) b) ∗ (tele_app (tele_app Q a) b))) →
+      ∀.. (a : A), tele_app P a -∗ (|={E2}=> ∃.. (b : B), spec_ctx ∗ j ⤇ fill K' (tele_app (tele_app e2 a) b) ∗ (tele_app (tele_app Q a) b))) →
     ReductionStep' tp_reduction_condition pre e1 0%nat (fupd E1 E2) (fupd E2 E1) A B P e2 Q E1.
   Proof.
     rewrite /ReductionStep' /ReductionTemplateStep => Hjk.
@@ -360,7 +378,7 @@ Section reloc_executor.
       iIntros (a) "HP".
       iPoseProof (Hjk j K with "[$Hs $Hj] HP") as "HQ".
       rewrite !bi_texist_exist.
-      iMod "HQ" as (b) "[Hj HQ]".
+      iMod "HQ" as (b) "[_ [Hj HQ]]".
       iExists b.
       by iFrame.
   Qed.
@@ -422,10 +440,11 @@ Section reloc_executor.
       apply sep_mono_r.
       rewrite pure_True // left_id.
       rewrite pure_True // left_id.
+      rewrite pure_False // left_absorb right_id.
       iIntros "$".
     - rewrite step_cmpxchg_fail => //.
       apply fupd_mono.
-      rewrite -(exist_intro _).
+      rewrite -(exist_intro false).
       apply sep_mono_r.
       rewrite pure_False // left_absorb left_id.
       rewrite pure_True // left_id.
@@ -439,7 +458,9 @@ Section reloc_executor.
     apply bi.wand_intro_r.
     apply bi.wand_elim_r', bi.pure_elim' => HNE.
     apply bi.wand_intro_r.
-    by rewrite left_id -step_fork // left_id.
+    rewrite left_id step_fork //.
+    iIntros ">[%x ([#Hs Hj] & _ & Hx)]".
+    iExists _. by iFrame "# ∗".
   Qed.
 
   Lemma pure_step_tp φ n (e : expr) e' E1 E2 :

theories/examples/external/reloc/reloc_automation_base.v

@@ -14,13 +14,13 @@ From iris.heap_lang.lib Require Export ticket_lock.
 Section main.
   Context `{!relocG Σ}.
 
-  Global Instance refines_values_abduct E e1 e2 v1 v2 (A : lrel Σ) :
+  Global Instance refines_values_abduct E e1 (e2 : expr) v1 v2 (A : lrel Σ) :
     IntoVal e1 v1 →
     IntoVal e2 v2 →
-    Abduct (TT := [tele]) false empty_hyp_first (REL e1 << e2 @ E : A)%I id (fupd E ⊤ $ A v1 v2) | 10.
+    HINT1 empty_hyp_first ✱ [|={E, ⊤}=> A v1 v2] ⊫ [id]; REL e1 << e2 @ E : A | 10.
   Proof.
-    rewrite /IntoVal /Abduct /= empty_hyp_first_eq left_id => <- <-.
-    apply refines_ret => //.
+    move => <- <-. iStepS.
+    iApply refines_ret => //.
   Qed.
 
   Global Instance refines_prepend_modal E el er A :
@@ -36,10 +36,10 @@ Section main.
   Proof. exact: fupd_refines. Qed.
 
   Global Instance restore_abduct e1 e2 E A p :
-    Abduct (TT := [tele]) p (REL e1 << e2 : A) (REL e1 << e2 @ E : A)%I id (fupd E ⊤ emp) | 10.
+    HINT1 □⟨p⟩ REL e1 << e2 : A ✱ [fupd E ⊤ emp] ⊫ [id]; REL e1 << e2 @ E : A | 10.
   Proof.
-    rewrite /Abduct /= bi.intuitionistically_if_elim. rewrite modality_ec_frame_r left_id.
-    exact: restore_mask.
+    iStepS. rewrite bi.intuitionistically_if_elim.
+    iApply restore_mask. by iMod "H2" as "_".
   Qed.
 
   (* left execution and tp execution should always be performed *)
@@ -49,7 +49,7 @@ Section main.
     ReshapeExprAnd expr e K e_in' (ReductionTemplateStep wp_red_cond T H [tele_arg ⊤ ; NotStuck] e_in' e_out' MT) →
     SatisfiesContextCondition context_as_item_condition K →
     SatisfiesTemplateCondition left_template_condition R MT R' MT' →
-    Abduct (TT := [tele]) p H P id (MT' $ flip left_execute R' ∘ K ∘ e_out').
+    HINT1 □⟨p⟩ H ✱ [MT' $ flip left_execute R' ∘ K ∘ e_out'] ⊫ [id]; P.
   Proof. intros. eapply execution_abduct_lem => //. iSolveTC. cbn => //. Qed.
 
   Global Instance tp_execution_abduct p H P e R K e_in' T e_out' MT MT' R' :
@@ -57,7 +57,7 @@ Section main.
     ReshapeExprAnd expr e K e_in' (ReductionTemplateStep tp_reduction_condition T H ((λᵗ _ E1 _ _ , E1) R) e_in' e_out' MT) →
     SatisfiesContextCondition context_as_item_condition K →
     SatisfiesTemplateCondition tp_template_condition R MT R' MT' →
-    Abduct (TT := [tele]) p H P id (MT' $ flip tp_execute R' ∘ K ∘ e_out').
+    HINT1 □⟨p⟩ H ✱ [MT' $ flip tp_execute R' ∘ K ∘ e_out'] ⊫ [id]; P.
   Proof. intros. eapply execution_abduct_lem => //. iSolveTC. Qed.
 
   (* right execution should not always be performed *)
@@ -67,7 +67,7 @@ Section main.
     ReshapeExprAnd expr e K e_in' (ReductionTemplateStep tp_reduction_condition T H ((λᵗ _ E1 _, E1) R) e_in' e_out' MT) →
     SatisfiesContextCondition context_as_item_condition K →
     SatisfiesTemplateCondition right_template_condition R MT R' MT' →
-    Abduct (TT := [tele]) p H P id (MT' $ flip right_execute R' ∘ K ∘ e_out').
+    HINT1 □⟨p⟩ H ✱ [MT' $ flip right_execute R' ∘ K ∘ e_out'] ⊫ [id]; P.
   Proof. intros. eapply execution_abduct_lem => //. iSolveTC. Qed.
 
   (* but it should always be performed when the left hand side is a value *)
@@ -78,18 +78,20 @@ Section main.
     ReshapeExprAnd expr e K e_in' (ReductionTemplateStep tp_reduction_condition T H ((λᵗ _ E1 _, E1) R) e_in' e_out' MT) →
     SatisfiesContextCondition context_as_item_condition K →
     SatisfiesTemplateCondition right_template_condition R MT R' MT' →
-    Abduct (TT := [tele]) p H P id (MT' $ flip right_execute R' ∘ K ∘ e_out').
+    HINT1 □⟨p⟩ H ✱ [MT' $ flip right_execute R' ∘ K ∘ e_out'] ⊫ [id]; P.
   Proof. intros; exact: right_execution_abduct. Qed.
 
   Global Instance tpwp_abduct_val j e E1 E2 Φ v:
     IntoVal e v →
-    Abduct (TT := [tele]) false empty_hyp_first (tpwp j e E1 E2 Φ) id (tpwp_def j e E1 E2 Φ).
-  Proof. rewrite /Abduct /= tpwp_eq empty_hyp_first_eq left_id => _ //=. Qed.
+    HINT1 empty_hyp_first ✱ [tpwp_def j e E1 E2 Φ] ⊫ [id]; tpwp j e E1 E2 Φ.
+  Proof. move => <-. iStepS. rewrite tpwp_eq. iStepS. by iApply "H1". Qed.
 
   Global Instance tpwp_abduct_K_val j e E1 E2 Φ v K:
     IntoVal e v →
-    Abduct (TT := [tele]) false empty_hyp_first (tpwp j (fill K e) E1 E2 Φ) id (tpwp_def j (fill K e) E1 E2 Φ).
-  Proof. rewrite /Abduct /= tpwp_eq empty_hyp_first_eq left_id => _ //=. Qed.
+    HINT1 empty_hyp_first ✱ [tpwp_def j (fill K e) E1 E2 Φ] ⊫ [id]; tpwp j (fill K e) E1 E2 Φ.
+  Proof. move => <-. iStepS. rewrite tpwp_eq. iStepS. by iApply "H1". Qed.
+
+  Global Opaque spec_ctx.
 
   Section lock_n_stack_specs.
     (* spin lock specs as tp executions, so that automation can apply them *)

theories/examples/external/reloc/stack_refinement.v

@@ -38,33 +38,27 @@ Section proof.
   Definition sinv (A : lrel Σ) stk stk' : iProp Σ :=
     (∃ (istk : loc), stk  ↦ #istk ∗ stack_link A istk stk')%I.
 
-  Global Instance mapsto_to_stack_content p hd v (tl : loc) E q :
-    BiAbd (TTl := [tele_pair (list val)]) (TTr := [tele_pair (list val)]) p (hd ↦{q} CONSV v #tl)%I (λ xs : list val, stack_contents hd xs) (fupd E E)
-  (λ xs_tl, stack_contents tl xs_tl) (λ xs_tl xs, ⌜xs = v :: xs_tl⌝ ∗ hd ↦□ CONSV v # tl)%I.
+  Global Instance mapsto_to_stack_content p hd v (tl : loc) q :
+    HINT □⟨p⟩ hd ↦{q} CONSV v #tl ✱ [xs_tl; stack_contents tl xs_tl]
+                 ⊫ [bupd] xs;
+              stack_contents hd xs ✱ [⌜xs = v :: xs_tl⌝ ∗ hd ↦□ CONSV v #tl].
   Proof.
-    rewrite /BiAbd /= => xs.
-    rewrite bi.intuitionistically_if_elim.
-    iStepS.
-    iExists (v :: xs).
-    iStepsS.
+    iStepsS. rewrite bi.intuitionistically_if_elim.
+    iExists (v :: x). iStepsS.
   Qed.
 
-  Global Instance mapsto_to_stack_content_empty p hd E q :
-    BiAbd (TTl := [tele]) (TTr := [tele]) p (hd ↦{q} NILV)%I (stack_contents hd []) (fupd E E)
-        emp%I (hd ↦□ NILV)%I.
-  Proof.
-    rewrite /BiAbd /= right_id bi.intuitionistically_if_elim.
-    iStepsS.
-  Qed.
+  Global Instance mapsto_to_stack_content_empty p hd q :
+    HINT □⟨p⟩ hd ↦{q} NILV ✱ [- ; emp] ⊫ [bupd]; stack_contents hd [] ✱ [hd ↦□ NILV].
+  Proof. iStepsS. rewrite bi.intuitionistically_if_elim. iStepsS. Qed.
 
 (*  Opaque is_stack.*)
 
   Global Instance val_of_list_suc l x xs p :
-    BiAbd (TTl := [tele]) (TTr := [tele]) p (l ↦ₛ CONSV x (val_of_list xs))%I (l ↦ₛ val_of_list (x :: xs))%I id emp%I emp%I.
+    HINT □⟨p⟩ l ↦ₛ CONSV x (val_of_list xs) ✱ [- ; emp] ⊫ [id]; l ↦ₛ val_of_list (x :: xs) ✱ [emp].
   Proof. iSolveTC. Qed.
 
   Global Instance val_of_list_empty l p :
-    BiAbd (TTl := [tele]) (TTr := [tele]) p (l ↦ₛ NILV)%I (l ↦ₛ val_of_list [])%I id emp%I emp%I.
+    HINT □⟨p⟩ l ↦ₛ NILV ✱ [- ; emp] ⊫ [id]; l ↦ₛ val_of_list [] ✱ [emp].
   Proof. iSolveTC. Qed. 
 
   Lemma FG_CG_push_refinement N st st' (A : lrel Σ) (v v' : val) :
@@ -189,10 +183,10 @@ Section proof.
     iApply (refines_pack (stackInt A)).
     repeat iApply refines_pair.
     - iStepsS. rel_rec_r. iStepsS.
-    - iStepsS. iIntros "!>". rel_pure_r.
+    - iStepsS. iStepR. do 2 iStepS.
       iApply (FG_CG_pop_refinement with "H5").
       solve_ndisj.
-    - iStepsS. iIntros "!>". rel_pure_r.
+    - iStepsS. iStepR. do 2 iStepS.
       iApply (FG_CG_push_refinement with "H4 H5").
       solve_ndisj.
   Qed.

theories/examples/external/reloc/tests_reloc.v

@@ -19,16 +19,17 @@ Section tests.
       (Hspec : nclose specN ⊆ E) ϕ :
       PureExec ϕ n e e' →
       ϕ →
-      (REL t << fill K' e' @ E : A) ⊢ REL t << fill K' e @ E : A.
+      (REL t << inl $ fill K' e' @ E : A) ⊢ REL t << fill K' e @ E : A.
   Proof.
-    rewrite refines_eq /refines_def => Hpure Hϕ.
-    iIntros "Hlog". iIntros (j K).
-    rewrite -fill_app.
-    iApply class_instances_reloc.from_tpwp.
+    rewrite refines_eq /refines_def => Hpure Hϕ /=.
+    iIntros "Hlog". iIntros (j) "[#Hs Hj]".
+    iApply (class_instances_reloc.from_tpwp with "[Hlog]") => //.
+    rewrite -fill_app. 
     iStepsS.
     rewrite fill_app class_instances_reloc.tpwp_eq /=.
     iStepS.
-    by iApply "Hlog".
+    iStepS.
+    iApply ("Hlog"). iStepsS.
   Qed.
 
 End tests.
\ No newline at end of file