WIP: copy

theories/sim/instance.v

@@ -12,6 +12,9 @@ Notation "r |==> r'" := (viewshift wsat r r') (at level 65, format "r  |==>  r'"
 Notation "r |={ σs , σt }=> r'" := (viewshift_state wsat r r' σs σt)
   (at level 65, format "r  |={ σs , σt }=>  r'").
 
+Notation "r ={ σs , σt }=> P" := (viewshiftP wsat r P σs σt)
+  (at level 65, format "r  ={ σs , σt }=>  P").
+
 Notation rrel := (rrel vrel).
 
 (** "modular" simulation relations dont make assumptions

theories/sim/left_step.v

 From iris.algebra Require Import local_updates.
 
 From stbor.lang Require Import steps_progress steps_inversion steps_retag.
-From stbor.sim Require Export instance.
+From stbor.sim Require Export instance invariant_access body.
 
 Set Default Proof Using "Type".
 
@@ -53,16 +53,89 @@ Proof.
 Qed.
 
 Lemma sim_body_copy_unique_l
-  fs ft (r r': resUR) (h: heaplet) n (l: loc) tg T (s: scalar) et σs σt Φ :
+  fs ft (r r': resUR) (h: heaplet) n (l: loc) t T (s: scalar) et σs σt Φ :
   tsize T = 1%nat →
-  r ≡ r' ⋅ res_tag tg tkUnique h →
+  r ≡ r' ⋅ res_tag t tkUnique h →
   h !! l = Some s →
   (r ⊨{n,fs,ft} (#[s], σs) ≥ (et, σt) : Φ : Prop) →
-  r ⊨{n,fs,ft} (Copy (Place l (Tagged tg) T), σs) ≥ (et, σt) : Φ.
+  r ⊨{n,fs,ft} (Copy (Place l (Tagged t) T), σs) ≥ (et, σt) : Φ.
 Proof.
+  intros LenT Eqr Eqs CONT. pfold. intros NT. intros.
+  have WSAT1 := WSAT. (* backup *)
+
+  (* making a step *)
+  edestruct (NT (Copy (Place l (Tagged t) T)) σs) as [[]|[es' [σs' STEPS]]];
+    [done..|].
+  destruct (tstep_copy_inv _ (PlaceR _ _ _) _ _ _ STEPS)
+      as (l'&t'&T'& vs & α' & EqH & ? & Eqvs & Eqα' & ?).
+  symmetry in EqH. simplify_eq.
+
+  rewrite LenT read_mem_equation_1 /= in Eqvs.
+  destruct (σs.(shp) !! l) as [s'|] eqn:Eqs'; [|done].
+  simpl in Eqvs. simplify_eq.
+
+  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
+  (* some lookup properties *)
+  have VALIDr := cmra_valid_op_r _ _ VALID. rewrite ->Eqr in VALIDr.
+  have HLtr: r.(rtm) !! t ≡ Some (to_tagKindR tkUnique, to_agree <$> h).
+  { rewrite Eqr.
+    eapply tmap_lookup_op_unique_included;
+      [apply VALIDr|apply cmra_included_r|].
+    rewrite res_tag_lookup //. }
+  have HLtrf: (r_f ⋅ r).(rtm) !! t ≡ Some (to_tagKindR tkUnique, to_agree <$> h).
+  { apply tmap_lookup_op_r_unique_equiv; [apply VALID|done]. }
+
+  (* Unique: stack unchanged *)
+  destruct (for_each_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
+  specialize (EQ1 O) as (stk & stk' & Eqstk & Eqstk' & ACC1); [rewrite LenT; lia|].
+  rewrite shift_loc_0_nat in Eqstk, Eqstk'.
+  move : ACC1. case access1 as [[n1 stk1]|] eqn:ACC1; [|done].
+  simpl. intros Eqs1. symmetry in Eqs1. simplify_eq.
+
+  destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
+  rewrite Eqst in Eqstk. rewrite Eqcs in ACC1.
+
+  destruct (unique_access_head _ _ _ _ _ _ _ _ s _ Eqstk ACC1 PINV HLtrf)
+    as (it & Eqpit & Eqti & HDi & Eqhp); [by rewrite lookup_fmap Eqs |].
+
+  have ?: α' = σt.(sst).
+  { move : Eqα'.
+    rewrite LenT /= /memory_read /= /= shift_loc_0_nat Eqst Eqstk /= Eqcs ACC1 /=.
+    destruct (tag_unique_head_access σt.(scs) stk (Tagged t) it.(protector) AccessRead)
+      as [ns Eqss].
+    - destruct HDi as [stk' Eq']. exists stk'. rewrite Eq'. f_equal.
+      rewrite -Eqpit -Eqti. by destruct it.
+    - rewrite ACC1 in Eqss. simplify_eq. rewrite insert_id //. by inversion 1. }
+  subst α'. rewrite Eqstk in Eqstk'. symmetry in Eqstk'. simplify_eq.
+
+  have TOT: tag_on_top σt.(sst) l t.
+  { destruct HDi as [stk' Eqstk'].
+    rewrite /tag_on_top Eqstk Eqstk' /= -Eqpit -Eqti. destruct it. by eexists. }
+
+  rewrite (_: mkState σs.(shp) σt.(sst) σs.(scs) σs.(snp) σs.(snc) = σs) in STEPS;
+    last first. { rewrite -Eqst. by destruct σs. }
+
+  (* we read s' from σs(l), we know [s] is in σt(l), now we have to prove that
+    s' = s *)
+  assert (s' = s). { admit. } subst s'.
+
+  have STEPSS: (Copy (Place l (Tagged t) T), σs) ~{fs}~>* (#[s]%E, σs)
+    by apply rtc_once.
+  have NT' := never_stuck_tstep_once _ _ _ _ _ STEPS NT.
+  (* TODO: the following is the same in most proofs, generalize it *)
+  punfold CONT. specialize (CONT NT' _ WSAT1) as [RE TE ST]. split; [done|..].
+  - intros. specialize (TE _ TERM) as (vs' & σs' & r1 & STEPS' & POST).
+    exists vs', σs', r1. split; [|done]. etrans; eauto.
+  - inversion ST.
+    + constructor 1. intros.
+      destruct (STEP _ _ STEPT) as (es' & σs' & r1 & n' & STEPS' & POST).
+      exists es', σs', r1, n'. split; [|done].
+      left. destruct STEPS' as [?|[]].
+      * eapply tc_rtc_l; eauto.
+      * simplify_eq. by apply tc_once.
+    + econstructor 2; eauto. by etrans.
 Admitted.
 
-(* should be a fairly direct consequence of the above *)
 Lemma sim_body_copy_local_l fs ft r r' n l tg ty s et σs σt Φ :
   tsize ty = 1%nat →
   r ≡ r' ⋅ res_mapsto l [s] tg →
@@ -71,6 +144,9 @@ Lemma sim_body_copy_local_l fs ft r r' n l tg ty s et σs σt Φ :
     (Copy (Place l (Tagged tg) ty), σs) ≥ (et, σt)
   : Φ.
 Proof.
-Admitted.
+  intros Hty Hr. rewrite Hr cmra_assoc. intros CONT.
+  eapply sim_body_copy_unique_l; eauto.
+  by rewrite lookup_insert.
+Qed.
 
 End left.

theories/sim/local.v

@@ -192,6 +192,19 @@ Lemma viewshift_sim_local_body r1 r2 n es σs et σt Φ :
   sim_local_body r2 n es σs et σt Φ → sim_local_body r1 n es σs et σt Φ.
 Proof. intros VS. apply viewshift_state_sim_local_body. intros ?. by apply VS. Qed.
 
+
+Definition viewshiftP r (P: A → state → state → Prop) (σs σt: state) :=
+  ∀ r_f, wsat (r_f ⋅ r) σs σt → P r σs σt.
+
+Lemma viewshiftP_sim_local_body r n es σs et σt Φ (P : A → state → state → Prop) :
+  viewshiftP r P σs σt →
+  (P r σs σt → sim_local_body r n es σs et σt Φ) →
+  sim_local_body r n es σs et σt Φ.
+Proof.
+  intros VS HP. pfold. intros NT r_f WSAT.
+  specialize (HP (VS _ WSAT)). punfold HP. apply sim_local_body_mono.
+Qed.
+
 End local.
 
 Hint Resolve sim_local_body_mono : paco.

theories/sim/refl_mem_step.v

@@ -464,21 +464,7 @@ Proof.
   (* unfolding rrel for place *)
   simpl in RRELp. destruct RRELp as [VREL _].
   inversion VREL as [|???? ARELp U]; subst; simplify_eq. clear U VREL.
-  destruct ARELp as (_ & _ & ARELp).
-
-  simpl in RRELv.
-  have SHR: ∀ l' t', priv_loc (r_f ⋅ r) l' t' →
-            ∀ i, (i < tsize T)%nat → l' ≠ (l +ₗ i).
-  { intros l' t' PV i Lt Eq. subst l'.
-    destruct (for_each_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
-    specialize (EQ1 _ Lt) as (stk & stk' & Eqstk & Eqstk' & ACC).
-    move : ACC. case access1 as [[n' stk'1]|] eqn:ACC ; [|done].
-    simpl. intros. simplify_eq.
-    eapply (priv_pub_access_UB (r_f ⋅ r) (l +ₗ i) _ _ _ _ _ _ Eqstk);
-      [by eexists|exact WSAT1|exact PV|].
-    destruct t; [|done]. destruct ARELp as [h Eqh].
-    apply (tmap_lookup_op_r_equiv_pub r_f.(rtm)) in Eqh as [h1 Eqh1];
-      [|apply VALID]. by eexists _. }
+  destruct ARELp as (_ & _ & ARELp). simpl in RRELv.
 
   exists (#[☠])%V, σs', r, n. split; last split.
   { left. by constructor 1. }
@@ -822,7 +808,7 @@ Proof.
             - left. move : PB. done.
             - by right. }
 
-    (* lamp_inv *)
+    (* lmap_inv *)
     - move : LINV. rewrite Eqr 2!cmra_assoc.
       intros LINV l1 t1 Eq1. simpl. specialize (LINV l1 t1 Eq1) as (?&?&?).
       do 2 (split; [done|]).

theories/sim/right_step.v

@@ -53,17 +53,36 @@ Lemma sim_body_copy_unique_r
   (r ⊨{n,fs,ft} (es, σs) ≥ (#[s], σt) : Φ : Prop) →
   r ⊨{S n,fs,ft} (es, σs) ≥ (Copy (Place l (Tagged tg) T), σt) : Φ.
 Proof.
+  intros LenT TOP Eqr Eqs CONT.
 Admitted.
 
-(* should be a fairly direct consequence of the above. *)
-Lemma sim_body_copy_local_r fs ft r r' n l tg ty s es σs σt Φ :
+
+Lemma vsP_res_mapsto_tag_on_top (r: resUR) l t s σs σt :
+  (r ⋅ res_mapsto l [s] t) ={σs,σt}=> (λ _ _ σt, tag_on_top σt.(sst) l t : Prop).
+Proof.
+  intros r_f. rewrite cmra_assoc.
+  intros (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
+  have Hrf: ((r_f ⋅ r ⋅ res_mapsto l [s] t).(rlm) !! l : optionR tagR) ≡ Some (to_tagR t).
+  { move : (proj2 VALID l).
+    rewrite lookup_op (res_mapsto_llookup_1 l [s] t); [|simpl;lia].
+    intros Eq%(exclusive_Some_r (to_tagR t)). by rewrite Eq left_id. }
+  specialize (LINV _ _ Hrf) as (?& Eqst &?).
+  rewrite /tag_on_top Eqst /=. by eexists.
+Qed.
+
+Lemma sim_body_copy_local_r fs ft r r' n l t ty s es σs σt Φ :
   tsize ty = 1%nat →
-  r ≡ r' ⋅ res_mapsto l [s] tg →
+  r ≡ r' ⋅ res_mapsto l [s] t →
   (r ⊨{n,fs,ft} (es, σs) ≥ (#[s], σt) : Φ) →
   r ⊨{S n,fs,ft}
-    (es, σs) ≥ (Copy (Place l (Tagged tg) ty), σt)
+    (es, σs) ≥ (Copy (Place l (Tagged t) ty), σt)
   : Φ.
 Proof.
-Admitted.
+  intros Hty Hr. rewrite Hr. intros CONT.
+  eapply viewshiftP_sim_local_body; [apply vsP_res_mapsto_tag_on_top|].
+  simpl. intros TOP. move : CONT. rewrite cmra_assoc. intros CONT.
+  eapply sim_body_copy_unique_r; eauto.
+  by rewrite lookup_insert.
+Qed.
 
 End right.