deref/ref take results

theories/lang/steps_inversion.v

@@ -474,16 +474,18 @@ Proof.
   - by exists (Ki :: K').
 Qed.
 
-Lemma tstep_ref_inv l tg T e' σ σ'
-  (STEP: ((& (Place l tg T))%E, σ) ~{fns}~> (e', σ')) :
-  e' = #[ScPtr l tg]%E ∧ σ' = σ ∧ is_Some (σ.(shp) !! l).
+Lemma tstep_ref_inv (pl: result)  e' σ σ'
+  (STEP: ((& pl)%E, σ) ~{fns}~> (e', σ')) :
+  ∃ l tg T, pl = PlaceR l tg T ∧ e' = #[ScPtr l tg]%E ∧ σ' = σ ∧ is_Some (σ.(shp) !! l).
 Proof.
   inv_tstep. symmetry in Eq.
   destruct (fill_ref_decompose _ _ _ Eq)
     as [[]|[K' [? Eq']]]; subst.
-  - clear Eq. simpl in HS. by inv_head_step.
+  - clear Eq. simpl in HS. inv_head_step.
+    have Eq1 := to_of_result pl. rewrite -H /to_result in Eq1. simplify_eq.
+    naive_solver.
   - apply result_head_stuck, (fill_not_result _ K') in HS.
-    by rewrite Eq' in HS.
+    by rewrite Eq' to_of_result in HS.
 Qed.
 
 (** Deref *)
@@ -498,17 +500,19 @@ Proof.
   - by exists (Ki :: K').
 Qed.
 
-Lemma tstep_deref_inv l tg T e' σ σ'
-  (STEP: ((Deref #[ScPtr l tg] T)%E, σ) ~{fns}~> (e', σ')) :
-  e' = Place l tg T ∧ σ' = σ ∧
+Lemma tstep_deref_inv (rf: result) T e' σ σ'
+  (STEP: ((Deref rf T)%E, σ) ~{fns}~> (e', σ')) :
+  ∃ l tg, rf = (ValR [ScPtr l tg])%R ∧ e' = Place l tg T ∧ σ' = σ ∧
   (∀ (i: nat), (i < tsize T)%nat → l +ₗ i ∈ dom (gset loc) σ.(shp)).
 Proof.
   inv_tstep. symmetry in Eq.
   destruct (fill_deref_decompose _ _ _ _ Eq)
     as [[]|[K' [? Eq']]]; subst.
-  - clear Eq. simpl in HS. by inv_head_step.
+  - clear Eq. simpl in HS. inv_head_step.
+    have Eq1 := to_of_result rf. rewrite -H0 /to_result in Eq1. simplify_eq.
+    naive_solver.
   - apply result_head_stuck, (fill_not_result _ K') in HS.
-    by rewrite Eq' in HS.
+    by rewrite Eq' to_of_result in HS.
 Qed.
 
 (** Call *)
@@ -728,17 +732,21 @@ Proof.
   - subst K. by exists (Ki :: K0).
 Qed.
 
-Lemma tstep_copy_inv l tg T e' σ σ'
-  (STEP: (Copy (Place l tg T), σ) ~{fns}~> (e', σ')) :
-  ∃ v α', e' = Val v ∧ read_mem l (tsize T) σ.(shp) = Some v ∧
+Lemma tstep_copy_inv (pl: result) e' σ σ'
+  (STEP: (Copy pl, σ) ~{fns}~> (e', σ')) :
+  ∃ l tg T v α',
+    pl = PlaceR l tg T ∧
+    e' = Val v ∧ read_mem l (tsize T) σ.(shp) = Some v ∧
     memory_read σ.(sst) σ.(scs) l tg (tsize T) = Some α' ∧
     σ' = mkState σ.(shp) α' σ.(scs) σ.(snp) σ.(snc).
 Proof.
   inv_tstep. symmetry in Eq.
   destruct (fill_copy_decompose _ _ _ Eq) as [[]|[K' [? Eq']]]; subst.
-  - clear Eq. simpl in HS. inv_head_step. naive_solver.
+  - clear Eq. simpl in HS. inv_head_step.
+    have Eq1 := to_of_result pl. rewrite -H0 /to_result in Eq1. simplify_eq.
+    naive_solver.
   - exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
-    + rewrite /= Eq'. by eexists.
+    + rewrite /= Eq' to_of_result. by eexists.
     + by rewrite Eq1' in HS.
 Qed.
 
@@ -776,9 +784,12 @@ Proof.
   - subst K. right. by exists r1, (Ki :: K').
 Qed.
 
-Lemma tstep_write_inv l tg T v e' σ σ'
-  (STEP: ((Place l tg T <- #v)%E, σ) ~{fns}~> (e', σ')) :
-  ∃ α', e' = (#[☠]%V) ∧
+Lemma tstep_write_inv (pl r: result) e' σ σ'
+  (STEP: ((pl <- r)%E, σ) ~{fns}~> (e', σ')) :
+  ∃ l tg T v α',
+    pl = PlaceR l tg T ∧
+    r = ValR v ∧
+    e' = (#[☠]%V) ∧
     memory_written σ.(sst) σ.(scs) l tg (tsize T) = Some α' ∧
     (∀ (i: nat), (i < length v)%nat → l +ₗ i ∈ dom (gset loc) σ.(shp)) ∧
     (v <<t σ.(snp)) ∧ (length v = tsize T) ∧
@@ -787,12 +798,15 @@ Proof.
   inv_tstep. symmetry in Eq.
   destruct (fill_write_decompose _ _ _ _ Eq)
     as [[]|[[K' [? Eq']]|[? [K' [? [Eq' ?]]]]]]; subst.
-  - clear Eq. simpl in HS. inv_head_step. naive_solver.
+  - clear Eq. simpl in HS. inv_head_step.
+    have Eq1 := to_of_result pl. rewrite -H0 /to_result in Eq1.
+    have Eq2 := to_of_result r. rewrite -H1 /to_result in Eq2. simplify_eq.
+    naive_solver.
   - exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
-    + rewrite /= Eq'. by eexists.
+    + rewrite /= Eq' to_of_result. by eexists.
     + by rewrite Eq1' in HS.
   - exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
-    + rewrite /= Eq'. by eexists.
+    + rewrite /= Eq' to_of_result. by eexists.
     + by rewrite Eq1' in HS.
 Qed.
 

theories/sim/left_step.v

@@ -14,8 +14,10 @@ Lemma sim_body_copy_left_1
 Proof.
   intros COND. pfold. intros NT r_f WSAT.
   edestruct NT as [[]|[es1 [σs1 STEP1]]]; [constructor 1|done|].
-  destruct (tstep_copy_inv _ _ _ _ _ _ _ STEP1) as (vs & α' & ? & Eqvs & READ & ?).
-  subst es1 σs1. rewrite /= read_mem_equation_1 /= in Eqvs.
+  destruct (tstep_copy_inv _ (PlaceR l (Tagged t) int) _ _ _ STEP1)
+    as (l' & t' & T' & vs & α' & EqH & ? & Eqvs & READ & ?).
+  symmetry in EqH. simplify_eq.
+  rewrite /= read_mem_equation_1 /= in Eqvs.
   destruct (σs.(shp) !! l) as [s|] eqn:Eqs; [|done]. simpl in Eqvs. simplify_eq.
   specialize (COND _ eq_refl).
 

theories/sim/refl.v

@@ -102,13 +102,14 @@ Proof.
     move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
     eapply sim_simple_post_mono, IHe; [|by auto..].
     intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
-    Fail eapply sim_simple_deref.
-    admit.
+    have ?:= (rrel_eq _  _ _ Hrel). subst rt.
+    eapply sim_simple_deref. intros. by subst.
   - (* Ref *)
     move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
     eapply sim_simple_post_mono, IHe; [|by auto..].
     intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
-    Fail eapply sim_simple_ref.
+    have ?:= (rrel_eq _  _ _ Hrel). subst rt.
+    eapply sim_simple_ref. intros. subst.
     admit.
   - (* Copy *) admit.
   - (* Write *) admit.

theories/sim/refl_mem_step.v

@@ -296,8 +296,8 @@ Proof.
   { right.
     destruct (NT (Copy (Place l (Tagged t) Ts)) σs) as [[]|[es' [σs' STEPS]]];
       [done..|].
-    destruct (tstep_copy_inv _ _ _ _ _ _ _ STEPS)
-      as (vs & α' & ? & Eqvs & Eqα' & ?). subst es'.
+    destruct (tstep_copy_inv _ (PlaceR l (Tagged t) Ts) _ _ _ STEPS)
+      as (?&?&?& vs & α' & EqH & ? & Eqvs & Eqα' & ?). symmetry in EqH. simplify_eq.
     destruct (read_mem_is_Some l (tsize Tt) σt.(shp)) as [vt Eqvt].
     { intros m. rewrite (srel_heap_dom _ _ _ WFS WFT SREL) -EQS.
       apply (read_mem_is_Some' l (tsize Ts) σs.(shp)). by eexists. }
@@ -306,8 +306,8 @@ Proof.
     exists (#vt)%E, (mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc)).
     by eapply (head_step_fill_tstep _ []), copy_head_step'. }
   constructor 1. intros.
-  destruct (tstep_copy_inv _ _ _ _ _ _ _ STEPT) as (vt & α' & ? & Eqvt & Eqα' & ?).
-  subst et'.
+  destruct (tstep_copy_inv _ (PlaceR l (Tagged t) Tt) _ _ _ STEPT)
+    as (?&?&?& vt & α' & EqH & ? & Eqvt & Eqα' & ?). symmetry in EqH. simplify_eq.
   destruct (read_mem_is_Some l (tsize Ts) σs.(shp)) as [vs Eqvs].
   { intros m. rewrite -(srel_heap_dom _ _ _ WFS WFT SREL) EQS.
     apply (read_mem_is_Some' l (tsize Tt) σt.(shp)). by eexists. }
@@ -374,7 +374,7 @@ Proof.
     - by apply (tstep_wf _ _ _ STEPS WFS).
     - by apply (tstep_wf _ _ _ STEPT WFT).
     - done.
-    - intros t1 k h Eqt. specialize (PINV t1 k h Eqt) as [Lt PI]. subst σt'. simpl.
+    - intros t1 k h Eqt. specialize (PINV t1 k h Eqt) as [Lt PI]. simpl.
       split; [done|]. intros l' s' Eqk'.
       specialize (PI _ _ Eqk') as [? PI]. split; [done|].
       intros stk' Eqstk'.
@@ -394,7 +394,7 @@ Proof.
       destruct k.
       + eapply access1_head_preserving; eauto.
       + eapply access1_active_SRO_preserving; eauto.
-    - intros c cs Eqc. specialize (CINV _ _ Eqc). subst σt'. simpl.
+    - intros c cs Eqc. specialize (CINV _ _ Eqc). simpl.
       clear -Eqα' CINV. destruct cs as [[T|]| |]; [|done..].
       destruct CINV as [IN CINV]. split; [done|].
       intros t1 InT. specialize (CINV _ InT) as [? CINV]. split; [done|].
@@ -403,8 +403,8 @@ Proof.
       destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
         as [stk [Eqstk AS]].
       exists stk, pm'. split; last split; [done| |done]. by apply AS.
-    - subst σt'. rewrite /srel /=. by destruct SREL as (?&?&?&?&?).
-    - subst σs' σt'. intros l1. simpl. intros Inl1.
+    - rewrite /srel /=. by destruct SREL as (?&?&?&?&?).
+    - intros l1. simpl. intros Inl1.
       specialize (LINV _ Inl1) as [InD1 LINV]. split; [done|].
       intros s stk Eqs.
       have HLF : ∀ i, (i < tsize Tt)%nat → l1 ≠ (l +ₗ i).
@@ -417,7 +417,7 @@ Proof.
   apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)). intros.
   have VREL2: vrel (r ⋅ (core (r_f ⋅ r))) vs vt.
   { eapply vrel_mono; [done| |exact VREL']. apply cmra_included_r. }
-  subst σt'. apply POST; eauto.
+  apply POST; eauto.
 Admitted.
 
 (** Write *)
@@ -510,17 +510,19 @@ Proof.
   split; [|done|].
   { right.
     edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
-    destruct (tstep_write_inv _ _ _ _ _ _ _ _ STEPS)
-      as (α' & ? & Eqα' & EqD & IN & EQL & ?).
-    subst es'. setoid_rewrite <-(srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
+    destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPS)
+      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQL & ?).
+    symmetry in EqH, EqH'. simplify_eq.
+    setoid_rewrite <-(srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
     destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
     rewrite Eqst Eqcs in Eqα'. rewrite Eqnp in IN. rewrite EQL in EqD.
     exists (#[☠])%V,
            (mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc)).
     eapply (head_step_fill_tstep _ []), write_head_step'; eauto. }
   constructor 1. intros.
-  destruct (tstep_write_inv _ _ _ _ _ _ _ _ STEPT)
-    as (α' & ? & Eqα' & EqD & IN & EQL & ?). subst et'.
+  destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPT)
+      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQL & ?).
+  symmetry in EqH, EqH'. simplify_eq.
   assert (∃ s, v = [s]) as [s ?].
   { rewrite LenT in EQL. destruct v as [|s v]; [simpl in EQL; done|].
     exists s. destruct v; [done|simpl in EQL; lia]. } subst v.
@@ -584,7 +586,7 @@ Proof.
           (<[l:=Cinl (Excl (v', init_stack (Tagged tg)))]> (r_f.2 ⋅ r'.2))).
       { by rewrite lookup_insert. }
       by apply exclusive_local_update.
-    - subst σt'. intros t k h HL. destruct (PINV t k h) as [? PI].
+    - intros t k h HL. destruct (PINV t k h) as [? PI].
       { rewrite Eqr. move: HL. by rewrite 4!lookup_op /= 2!right_id. }
       split; [done|]. simpl.
       intros l1 s1 Eqs1. specialize (PI l1 s1 Eqs1) as [HLs1 PI].
@@ -595,11 +597,11 @@ Proof.
         rewrite lookup_op (lookup_op (r_f.2 ⋅ r'.2)) /init_local_res /= 2!lookup_fmap.
         do 2 rewrite lookup_insert_ne //. }
       by setoid_rewrite lookup_insert_ne.
-    - subst σt'. intros c cs. simpl. rewrite -HCEq. intros Eqcm.
+    - intros c cs. simpl. rewrite -HCEq. intros Eqcm.
       move : CINV. rewrite Eqr cmra_assoc => CINV.
       specialize (CINV _ _ Eqcm). destruct cs as [[]| |]; [|done..].
       destruct CINV as [? CINV]. split; [done|]. by setoid_rewrite <- HTEq.
-    - subst σt'. destruct SREL as (?&?&?&?& REL). do 4 (split; [done|]).
+    - destruct SREL as (?&?&?&?& REL). do 4 (split; [done|]).
       simpl. intros l1 Inl1 Eq1.
       have NEql1: l1 ≠ l.
       { intros ?. subst l1. move : Eq1. rewrite lookup_op HLN left_id.
@@ -619,7 +621,7 @@ Proof.
         setoid_rewrite Eqr. setoid_rewrite cmra_assoc. by setoid_rewrite <- HTEq.
       + right. move : REL. setoid_rewrite Eqr. setoid_rewrite cmra_assoc.
         rewrite /priv_loc. by setoid_rewrite <- HTEq.
-    - subst σt'. move : LINV. rewrite Eqr cmra_assoc.
+    - move : LINV. rewrite Eqr cmra_assoc.
       (* TODO: general property of lmap_inv w.r.t to separable resource *)
       intros LINV l1 Inl1.
       have EqD': dom (gset loc) (r_f ⋅ r' ⋅ res_mapsto l 1 s (init_stack (Tagged tg))).(rlm)
@@ -648,7 +650,7 @@ Proof.
           by inversion 1. }
   left.
   eapply (sim_body_result _ _ _ _ (ValR [☠%S]) (ValR [☠%S])).
-  intros. simpl. subst σt'. by apply POST.
+  intros. simpl. by apply POST.
 Qed.
 
 Lemma sim_body_write_related_values
@@ -675,9 +677,10 @@ Proof.
   split; [|done|].
   { right.
     edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
-    destruct (tstep_write_inv _ _ _ _ _ _ _ _ STEPS)
-      as (α' & ? & Eqα' & EqD & IN & EQL & ?).
-    subst es'. setoid_rewrite <-(srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
+    destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPS)
+      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQL & ?).
+    symmetry in EqH, EqH'. simplify_eq.
+    setoid_rewrite <-(srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
     destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
     rewrite Eqst Eqcs EQS in Eqα'. rewrite -EQL in EQS.
     rewrite EQS in EqD. rewrite Eqnp in IN.
@@ -685,8 +688,9 @@ Proof.
            (mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc)).
     by eapply (head_step_fill_tstep _ []), write_head_step'. }
   constructor 1. intros.
-  destruct (tstep_write_inv _ _ _ _ _ _ _ _ STEPT)
-    as (α' & ? & Eqα' & EqD & IN & EQL & ?). subst et'.
+  destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPT)
+      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQL & ?).
+  symmetry in EqH, EqH'. simplify_eq.
   set σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc).
   have STEPS: ((Place l (Tagged tg) Ts <- v)%E, σs) ~{fs}~> ((#[☠])%V, σs').
   { setoid_rewrite (srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
@@ -734,7 +738,7 @@ Proof.
             move : Eqt. rewrite lookup_op Eqtg. by move => /tagKindR_exclusive_2.
           + right. naive_solver. }
       split.
-      { subst σt'. simpl. destruct CASEt as [(?&?&?&?Eqh)|[Eqh NEQ]].
+      { simpl. destruct CASEt as [(?&?&?&?Eqh)|[Eqh NEQ]].
         - subst t k k0. apply (PINV tg tkUnique h0). by rewrite HL2.
         - move : Eqh. apply PINV. }
       intros l' s' Eqk'. split.
@@ -752,7 +756,7 @@ Proof.
           destruct (PI l' ss0) as [? _]; [|done]. by rewrite Eqs0 Eqss0.
         - specialize (PINV _ _ _ Eqh) as [? PINV].
           specialize (PINV _ _ Eqk') as [EQ _]. rewrite /r' /=. by destruct k0. }
-      intros stk'. subst σt'. simpl.
+      intros stk'. simpl.
       destruct (write_mem_lookup_case l v σt.(shp) l')
           as [[i [Lti [Eqi Eqmi]]]|[NEql Eql]]; last first.
       { (* l' is NOT written to *)
@@ -829,7 +833,7 @@ Proof.
       intros c cs Eqc'.
       have Eqc: (r_f ⋅ r).(rcm) !! c ≡ Some cs.
       { move  : Eqc'. rewrite /r'. by destruct k0. }
-      specialize (CINV _ _ Eqc). subst σt'. simpl.
+      specialize (CINV _ _ Eqc). simpl.
       clear -Eqα' CINV Eqtg VALID HL HL2. destruct cs as [[T|]| |]; [|done..].
       destruct CINV as [IN CINV]. split; [done|].
       intros t InT. specialize (CINV _ InT) as [? CINV]. split; [done|].
@@ -860,7 +864,7 @@ Proof.
           as [stk [Eqstk AS]].
         exists stk, pm'. split; last split; [done|by apply AS|done].
     - (* srel *)
-      subst σt'. rewrite /srel /=. destruct SREL as (?&?&?&?&Eq).
+      rewrite /srel /=. destruct SREL as (?&?&?&?&Eq).
       repeat split; [done..|].
       intros l1 InD1 Eq1.
       destruct (write_mem_lookup l v σs.(shp)) as [EqN EqO]. rewrite /r'.
@@ -934,8 +938,8 @@ Proof.
           { exists h. rewrite /rtm /= HL lookup_insert_ne //. }
     - intros l'. rewrite -> Eqrlm. setoid_rewrite Eqrlm.
       intros InD. specialize (LINV _ InD) as [? LINV].
-      split. { subst σt'. rewrite /= write_mem_dom //. }
-      intros s stk Eq. subst σt'. rewrite /=.
+      split. { rewrite /= write_mem_dom //. }
+      intros s stk Eq. rewrite /=.
       specialize (LINV _ _ Eq) as (?&?&?&?).
       destruct (write_mem_lookup l v σs.(shp)) as [_ HLs].
       destruct (write_mem_lookup l v σt.(shp)) as [_ HLt].
@@ -948,7 +952,7 @@ Proof.
   }
   left.
   eapply (sim_body_result fs ft r' n (ValR [☠%S]) (ValR [☠%S])).
-  intros. simpl. subst σt'. by apply POST.
+  intros. simpl. by apply POST.
 Qed.
 
 (** Retag *)

theories/sim/refl_pure_step.v

@@ -186,54 +186,61 @@ Lemma sim_body_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 σs σt Φ :
 Proof. apply sim_body_let; eauto. Qed.
 
 (** Ref *)
-Lemma sim_body_ref fs ft r n l tgs tgt Ts Tt σs σt Φ :
-  Φ r n (ValR [ScPtr l tgs]) σs (ValR [ScPtr l tgt]) σt : Prop →
-  r ⊨{n,fs,ft} ((& (Place l tgs Ts))%E, σs) ≥ ((& (Place l tgt Tt))%E, σt) : Φ.
+Lemma sim_body_ref fs ft r n (pl: result) σs σt Φ :
+  (∀ l t T, pl = PlaceR l t T →
+    Φ r n (ValR [ScPtr l t]) σs (ValR [ScPtr l t]) σt : Prop) →
+  r ⊨{n,fs,ft} ((& pl)%E, σs) ≥ ((& pl)%E, σt) : Φ.
 Proof.
-  intros SIM. pfold.
+  intros POST. pfold.
   intros NT r_f WSAT. split; [|done|].
   { right.
-    destruct (NT (& (Place l tgs Ts))%E σs) as [[]|[es' [σs' STEPS]]]; [done..|].
-    destruct (tstep_ref_inv _ _ _ _ _ _ _ STEPS) as [? [? IS]]. subst es' σs'.
+    destruct (NT (& pl)%E σs) as [[]|[es' [σs' STEPS]]]; [done..|].
+    destruct (tstep_ref_inv _ _ _ _ _ STEPS) as (l & tg & T & ? & ? & ? & IS).
+    simplify_eq.
     have ?: is_Some (σt.(shp) !! l).
     { clear -WSAT IS. move : IS.
       by rewrite -2!(elem_of_dom (D:=gset loc)) -wsat_heap_dom. }
-    exists #[ScPtr l tgt]%E, σt.
+    exists #[ScPtr l tg]%E, σt.
     eapply (head_step_fill_tstep _ []). by econstructor; econstructor. }
   constructor 1. intros.
-  destruct (tstep_ref_inv _ _ _ _ _ _ _ STEPT) as [? [? IS]]. subst et' σt'.
+  destruct (tstep_ref_inv _ _ _ _ _ STEPT) as (l & tg & T & ? & ? & ? & IS).
+  simplify_eq.
   have ?: is_Some (σs.(shp) !! l).
   { clear -WSAT IS. move : IS.
     by rewrite -2!(elem_of_dom (D:=gset loc)) wsat_heap_dom. }
-  exists #[ScPtr l tgs]%E, σs, r, n. split.
+  exists #[ScPtr l tg]%E, σs, r, n. split.
   { left. constructor 1. eapply (head_step_fill_tstep _ []).
     by econstructor; econstructor. }
   split; [done|]. left.
-  by apply (sim_body_result _ _ _ _ (ValR _) (ValR _)).
+  apply (sim_body_result _ _ _ _ (ValR _) (ValR _)).
+  intros. by eapply POST.
 Qed.
 
 (** Deref *)
-Lemma sim_body_deref fs ft r n l tgs tgt Ts Tt σs σt Φ
-  (EQS: tsize Ts = tsize Tt) :
-  Φ r n (PlaceR l tgs Ts) σs (PlaceR l tgt Tt) σt : Prop →
-  r ⊨{n,fs,ft} (Deref #[ScPtr l tgs] Ts, σs) ≥ (Deref #[ScPtr l tgt] Tt, σt) : Φ.
+Lemma sim_body_deref fs ft r n (rf: result) T σs σt Φ :
+  (∀ l t, rf = ValR [ScPtr l t] →
+    Φ r n (PlaceR l t T) σs (PlaceR l t T) σt : Prop ) →
+  r ⊨{n,fs,ft} (Deref rf T, σs) ≥ (Deref rf T, σt) : Φ.
 Proof.
-  intros SIM. pfold.
+  intros POST. pfold.
   intros NT r_f WSAT. split; [|done|].
   { right.
-    destruct (NT (Deref #[ScPtr l tgs] Ts) σs) as [[]|[es' [σs' STEPS]]]; [done..|].
-    destruct (tstep_deref_inv _ _ _ _ _ _ _ STEPS) as [? [? IS]]. subst es' σs'.
-    have ?: (∀ (i: nat), (i < tsize Tt)%nat → l +ₗ i ∈ dom (gset loc) σt.(shp)).
-    { clear -WSAT IS EQS. rewrite -EQS. move => i /IS. by rewrite -wsat_heap_dom. }
-    exists (Place l tgt Tt), σt.
+    destruct (NT (Deref rf T) σs) as [[]|[es' [σs' STEPS]]]; [done..|].
+    destruct (tstep_deref_inv _ _ _ _ _ _ STEPS) as (l & t & ? & ? & ? & IS).
+    subst.
+    have ?: (∀ (i: nat), (i < tsize T)%nat → l +ₗ i ∈ dom (gset loc) σt.(shp)).
+    { clear -WSAT IS. by setoid_rewrite wsat_heap_dom. }
+    exists (Place l t T), σt.
     eapply (head_step_fill_tstep _ []). by econstructor; econstructor. }
   constructor 1. intros.
-  destruct (tstep_deref_inv _ _ _ _ _ _ _ STEPT) as [? [? IS]]. subst et' σt'.
-  have ?: (∀ (i: nat), (i < tsize Ts)%nat → l +ₗ i ∈ dom (gset loc) σs.(shp)).
-  { clear -WSAT IS EQS. rewrite EQS. move => i /IS. by rewrite wsat_heap_dom. }
-  exists (Place l tgs Ts), σs, r, n. split.
+  destruct (tstep_deref_inv _ _ _ _ _ _ STEPT) as (l & t & ? & ? & ? & IS).
+  subst.
+  have ?: (∀ (i: nat), (i < tsize T)%nat → l +ₗ i ∈ dom (gset loc) σs.(shp)).
+  { clear -WSAT IS. by setoid_rewrite <- wsat_heap_dom. }
+  exists (Place l t T), σs, r, n. split.
   { left. constructor 1. eapply (head_step_fill_tstep _ []).
     by econstructor; econstructor. }
   split; [done|].
-  left. by apply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)).
+  left. apply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)).
+  intros. by eapply POST.
 Qed.

theories/sim/simple.v

@@ -210,16 +210,17 @@ Lemma sim_simple_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 css cst Φ :
   r ⊨ˢ{n,fs,ft} (let: x := Place ls ts tys in es2, css) ≥ ((let: x := Place lt tt tyt in et2), cst) : Φ.
 Proof. intros HH σs σt <-<-. apply sim_body_let; eauto. Qed.
 
-Lemma sim_simple_ref fs ft r n l tgs tgt Ts Tt css cst Φ :
-  Φ r n (ValR [ScPtr l tgs]) css (ValR [ScPtr l tgt]) cst →
-  r ⊨ˢ{n,fs,ft} ((& (Place l tgs Ts))%E, css) ≥ ((& (Place l tgt Tt))%E, cst) : Φ.
+Lemma sim_simple_ref fs ft r n (pl: result) css cst Φ :
+  (∀ l t T, pl = PlaceR l t T →
+    Φ r n (ValR [ScPtr l t]) css (ValR [ScPtr l t]) cst) →
+  r ⊨ˢ{n,fs,ft} ((& pl)%E, css) ≥ ((& pl)%E, cst) : Φ.
 Proof. intros HH σs σt <-<-. apply sim_body_ref; eauto. Qed.
 
-Lemma sim_simple_deref fs ft r n l tgs tgt Ts Tt css cst Φ :
-  tsize Ts = tsize Tt →
-  Φ r n (PlaceR l tgs Ts) css (PlaceR l tgt Tt) cst →
-  r ⊨ˢ{n,fs,ft} (Deref #[ScPtr l tgs] Ts, css) ≥ (Deref #[ScPtr l tgt] Tt, cst) : Φ.
-Proof. intros ? HH σs σt <-<-. apply sim_body_deref; eauto. Qed.
+Lemma sim_simple_deref fs ft r n (rf: result) T css cst Φ :
+  (∀ l t, rf = ValR [ScPtr l t] →
+    Φ r n (PlaceR l t T) css (PlaceR l t T) cst) →
+  r ⊨ˢ{n,fs,ft} (Deref rf T, css) ≥ (Deref rf T, cst) : Φ.
+Proof. intros HH σs σt <-<-. apply sim_body_deref; eauto. Qed.
 
 Lemma sim_simple_var fs ft r n css cst var Φ :
   r ⊨ˢ{n,fs,ft} (Var var, css) ≥ (Var var, cst) : Φ.