add retag for immut ref

theories/lang/steps_retag.v

-From stbor.lang Require Export defs steps_foreach steps_list steps_wf.
+From stbor.lang Require Export defs steps_foreach steps_list steps_wf steps_progress.
 
 Set Default Proof Using "Type".
 
-(* FIXME; should not require [Unique] *)
-Definition tag_on_top (stks: stacks) l tag : Prop :=
-  ∃ prot, (stks !! l) ≫= head = Some (mkItem Unique (Tagged tag) prot).
+Definition tag_on_top (stks: stacks) l t pm : Prop :=
+  ∃ prot, (stks !! l) ≫= head = Some (mkItem pm (Tagged t) prot).
 
 (** Active protector preserving *)
 Definition active_preserving (cids: call_id_stack) (stk stk': stack) :=
@@ -690,9 +689,9 @@ Qed.
 
 (** Tag-on-top *)
 Lemma tag_on_top_write σ l tg stks :
-  tag_on_top σ.(sst) l tg →
+  tag_on_top σ.(sst) l tg Unique →
   memory_written (sst σ) (scs σ) l (Tagged tg) 1 = Some stks →
-  tag_on_top stks l tg.
+  tag_on_top stks l tg Unique.
 Proof.
   rewrite /memory_written /tag_on_top /= shift_loc_0.
   destruct (sst σ !! l) eqn:Hlk; last done. simpl.
@@ -704,39 +703,65 @@ Proof.
   simpl. done.
 Qed.
 
-Lemma tag_on_top_grant_unique stk old it cids  stk'
-  (UNIQ: it.(perm) = Unique) :
+Lemma tag_on_top_grant_uniq_SRO stk old it cids  stk'
+  (UNIQ: it.(perm) = Unique ∨ it.(perm) = SharedReadOnly) :
   grant stk old it cids = Some stk' → is_stack_head it stk'.
 Proof.
   rewrite /grant.
   case find_granting as [gip|]; [|done].
-  rewrite /= UNIQ /=. case access1 => [[n1 stk1]/=|//].
-  destruct stk1; [|case decide => ?]; intros; simplify_eq; by eexists.
+  destruct UNIQ as [UNIQ|UNIQ];
+  rewrite /= UNIQ /=; (case access1 => [[n1 stk1]/=|//]);
+  (destruct stk1; [|case decide => ?]; intros; simplify_eq; by eexists).
 Qed.
 
-Lemma tag_on_top_reborrowN_uniq α cids l n to tn α' pro :
-  reborrowN α cids l n to (Tagged tn) Unique pro = Some α' →
-  ∀ i, (i < n)%nat → tag_on_top α' (l +ₗ i) tn.
+Lemma tag_on_top_reborrowN_uniq_SRO α cids l n to tn pm α' pro
+  (UNIQ: pm = Unique ∨ pm = SharedReadOnly) :
+  reborrowN α cids l n to (Tagged tn) pm pro = Some α' →
+  ∀ i, (i < n)%nat → tag_on_top α' (l +ₗ i) tn pm.
 Proof.
   intros RB i Lt.
   destruct (for_each_lookup_case_2 _ _ _ _ _ RB) as [EQ _].
   specialize (EQ _ Lt) as (stk & stk' & Eq & Eq' & GR).
-  apply tag_on_top_grant_unique in GR as [stk1 Eq1]; [|done].
+  apply tag_on_top_grant_uniq_SRO in GR as [stk1 Eq1]; [|done].
   rewrite /tag_on_top Eq' Eq1 /=. by eexists.
 Qed.
 
 Lemma tag_on_top_retag_ref_uniq α cids nxtp l old T pro tn α' nxtp' :
   retag_ref α cids nxtp l old T (UniqueRef false) pro
     = Some (Tagged tn, α', nxtp') →
-  ∀ i, (i < tsize T)%nat → tag_on_top α' (l +ₗ i) tn.
+  ∀ i, (i < tsize T)%nat → tag_on_top α' (l +ₗ i) tn Unique.
 Proof.
   intros RT i. destruct (tsize T) as [|n] eqn:Eqsz; [lia|].
   rewrite -Eqsz.
   move : RT. rewrite /retag_ref {1}Eqsz /=.
   case reborrowN as [α1|] eqn:RB; [|done]. simpl. intros ?. simplify_eq.
-  eapply tag_on_top_reborrowN_uniq; eauto.
+  eapply tag_on_top_reborrowN_uniq_SRO; eauto.
 Qed.
 
+Lemma tag_on_top_retag_ref_shr α cids nxtp l old T pro tn α' nxtp'
+  (FRZ: is_freeze T) :
+  retag_ref α cids nxtp l old T SharedRef pro
+    = Some (Tagged tn, α', nxtp') →
+  ∀ i, (i < tsize T)%nat → tag_on_top α' (l +ₗ i) tn SharedReadOnly.
+Proof.
+  intros RT i. destruct (tsize T) as [|n] eqn:Eqsz; [lia|].
+  rewrite -Eqsz.
+  move : RT. rewrite /retag_ref {1}Eqsz /= visit_freeze_sensitive_is_freeze //.
+  case reborrowN as [α1|] eqn:RB; [|done]. simpl. intros ?. simplify_eq.
+  eapply tag_on_top_reborrowN_uniq_SRO; eauto.
+Qed.
+
+Lemma tag_on_top_shr_active_SRO α l t :
+  tag_on_top α l t SharedReadOnly →
+  ∃ stk, α !! l = Some stk ∧ t ∈ active_SRO stk.
+Proof.
+  intros [pro Eq]. destruct (α !! l) as [stk|]; [|done].
+  simpl in Eq. destruct stk as [|it stk']; [done|].
+  simpl in Eq. simplify_eq. eexists. split; [done|].
+  rewrite /= elem_of_union elem_of_singleton. by left.
+Qed.
+
+(* retag *)
 Lemma retag_nxtp_change α cids c nxtp l otag ntag rk pk T α' nxtp'
   (TS: (O < tsize T)%nat)
   (RK: match pk with | RawPtr _ => rk = RawRt | _ => True end) :

theories/sim/left_step.v

@@ -113,7 +113,7 @@ Proof.
     - 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.
+  have TOT: tag_on_top σt.(sst) l t Unique.
   { destruct HDi as [stk' Eqstk'].
     rewrite /tag_on_top Eqstk Eqstk' /= -Eqpit -Eqti. destruct it. by eexists. }
 

theories/sim/refl_mem_step.v

@@ -915,7 +915,7 @@ Lemma sim_body_write_unique_local_1 fs ft r r' n l t k T vs vt h0 σs σt Φ :
   (∀ ss st, vs = [ss] → vt = [st] →
     let σs' := mkState (<[l := ss]> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
     let σt' := mkState (<[l := st]> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
-    tag_on_top σt'.(sst) l t →
+    tag_on_top σt'.(sst) l t Unique →
     Φ (r' ⋅ res_tag t k (<[l := (ss,st)]>h0)) n (ValR [☠%S]) σs' (ValR [☠%S]) σt') →
   r ⊨{n,fs,ft}
     (Place l (Tagged t) T <- #vs, σs) ≥ (Place l (Tagged t) T <- #vt, σt) : Φ.
@@ -1004,7 +1004,7 @@ Proof.
     - 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.
+  have TOT: tag_on_top σt.(sst) l t Unique.
   { destruct HDi as [stk' Eqstk'].
     rewrite /tag_on_top Eqstk Eqstk' /= -Eqpit -Eqti. destruct it. by eexists. }
 
@@ -1184,7 +1184,7 @@ Lemma sim_body_write_unique_1
   r' ≡ r'' ⋅ rs →
   (let σs' := mkState (write_mem l [s] σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
    let σt' := mkState (write_mem l [s] σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
-    tag_on_top σt'.(sst) l tg →
+    tag_on_top σt'.(sst) l tg Unique →
     Φ (r' ⋅ res_tag tg tkUnique (<[l:=(s,s)]> h)) n (ValR [☠]%S) σs' (ValR [☠]%S) σt') →
   r ⊨{n,fs,ft}
     (Place l (Tagged tg) T <- #[s], σs) ≥ (Place l (Tagged tg) T <- #[s], σt) : Φ.
@@ -1407,9 +1407,12 @@ Proof.
   - by apply IH.
 Qed.
 
-Lemma sim_body_retag_mut_ref_default fs ft r n ptr T σs σt Φ :
+
+Lemma sim_body_retag_ref_default fs ft mut r n ptr T σs σt Φ :
   (0 < tsize T)%nat →
-  let pk : pointer_kind := (RefPtr Mutable) in
+  let pk : pointer_kind := (RefPtr mut) in
+  let pm := match mut with Mutable => Unique | Immutable => SharedReadOnly end in
+  (if mut is Immutable then is_freeze T else True) →
   (* Ptr(l,otg) comes from the arguments, so [otg] must be a public tag. *)
   arel r ptr ptr →
   (∀ l told tnew hplt c cids α' nxtp',
@@ -1421,16 +1424,17 @@ Lemma sim_body_retag_mut_ref_default fs ft r n ptr T σs σt Φ :
       stack for each [l +ₗ i].
       TODO: we can also specify that [hplt] knows the values of [l +ₗ i]'s. *)
     (∀ i: nat, (i < tsize T)%nat →
-      is_Some $ hplt !! (l +ₗ i) ∧ tag_on_top α' (l +ₗ i) tnew) →
+      is_Some $ hplt !! (l +ₗ i) ∧ tag_on_top α' (l +ₗ i) tnew pm) →
     let σs' := mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc) in
     let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in
     let s_new := ScPtr l (Tagged tnew) in
-    Φ (r ⋅ res_tag tnew tkUnique hplt) n (ValR [s_new]) σs' (ValR [s_new]) σt') →
+    let tk := match mut with Mutable => tkUnique | Immutable => tkPub end in
+    Φ (r ⋅ res_tag tnew tk hplt) n (ValR [s_new]) σs' (ValR [s_new]) σt') →
   r ⊨{n,fs,ft}
     (Retag #[ptr] pk T Default, σs) ≥
     (Retag #[ptr] pk T Default, σt) : Φ.
 Proof.
-  intros NZST pk AREL POST. pfold. intros NT. intros.
+  intros NZST pk pm FRZ AREL POST. pfold. intros NT. intros.
   have WSAT1 := WSAT. (* back up *)
 
   destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
@@ -1479,17 +1483,18 @@ Proof.
 
   set tnew := σt.(snp).
   set hplt : heaplet := write_hpl l (combine vs vt) ∅.
-  set r' : resUR := r ⋅ res_tag tnew tkUnique hplt.
+  set tk := match mut with Mutable => tkUnique | Immutable => tkPub end.
+  set r' : resUR := r ⋅ res_tag tnew tk hplt.
 
   have HNP := wsat_tmap_nxtp _ _ _ WSAT1.
-  have VALID': ✓ (r_f ⋅ r ⋅ res_tag tnew tkUnique hplt).
+  have VALID': ✓ (r_f ⋅ r ⋅ res_tag tnew tk hplt).
   { apply (local_update_discrete_valid_frame (r_f ⋅ r) ε);
       [by rewrite right_id|]. rewrite right_id.
     by apply res_tag_alloc_local_update. }
-  have Eqc': (r_f ⋅ r ⋅ res_tag tnew tkUnique hplt).(rcm)  ≡ (r_f ⋅ r).(rcm)
+  have Eqc': (r_f ⋅ r ⋅ res_tag tnew tk hplt).(rcm)  ≡ (r_f ⋅ r).(rcm)
     by rewrite /= right_id.
   have HLt: ∀ t kh, (r_f ⋅ r).(rtm) !! t ≡ Some kh →
-                    (r_f ⋅ r ⋅ res_tag tnew tkUnique hplt).(rtm) !! t ≡ Some kh.
+                    (r_f ⋅ r ⋅ res_tag tnew tk hplt).(rtm) !! t ≡ Some kh.
   { intros t kh Eqt.
     rewrite lookup_op res_tag_lookup_ne.
     - by rewrite right_id.
@@ -1527,7 +1532,8 @@ Proof.
         rewrite EqlT in Lti.
         specialize (Eqshp  _ Lti). rewrite Eqvs1 in Eqshp.
         specialize (Eqthp  _ Lti). rewrite Eqvt1 in Eqthp.
-        intros (stk' & pm & pro & Eqstk' & In' & NDIS). simpl in Eqstk'.
+        destruct mut.
+        * intros (stk' & pm' & pro & Eqstk' & In' & NDIS). simpl in Eqstk'.
           do 2 (split; [done|]).
           exists stk'. split; [done|].
           have EqRT':
@@ -1537,6 +1543,15 @@ Proof.
             as [pro1 Eqstk1]. rewrite Eqstk' /= in Eqstk1.
           clear -Eqstk1. destruct stk' as [|? stk1]; [done|].
           simpl in Eqstk1. simplify_eq. by exists pro1, stk1.
+        * intros (stk' & pm' & pro & Eqstk' & In' & NDIS). simpl in Eqstk'.
+          do 2 (split; [done|]).
+          exists stk'. split; [done|].
+          have EqRT':
+            retag_ref σt.(sst) σt.(scs) σt.(snp) l otg T SharedRef None =
+              Some (Tagged tnew, α', S tnew) by done.
+          have HTOP := (tag_on_top_retag_ref_shr _ _ _ _ _ _ _ _ _ _ FRZ EqRT' _ Lti).
+          clear -HTOP Eqstk'.
+          apply tag_on_top_shr_active_SRO in HTOP as (?&?&?). by simplify_eq.
       + rewrite res_tag_lookup_ne; [|done].
         rewrite right_id => Eqt.
         (* TODO: duplicate proof with retag_public *)
@@ -1553,7 +1568,7 @@ Proof.
             apply tagKindR_local_exclusive_r. }
           move : NEq Eqstk.
           by eapply retag_Some_local.
-        * destruct PRE as (stk' & pm & pro & Eqstk' & In' & ND).
+        * destruct PRE as (stk' & pm' & pro & Eqstk' & In' & ND).
           destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ EqRT _ _ t' _ Eqstk' In')
             as (stk & Eqstk & In); [done..|].
           destruct PINV as (Eqss & Eqst & HP); [simpl; naive_solver|].
@@ -1562,11 +1577,11 @@ Proof.
           destruct HP as (stk1 & Eqstk1 & opro1 & HTOP).
           rewrite Eqstk1 in Eqstk. simplify_eq.
           have ND2 := proj2 (state_wf_stack_item _ WFT _ _ Eqstk1).
-          assert (opro1 = pro ∧ pm = Unique) as [].
+          assert (opro1 = pro ∧ pm' = Unique) as [].
           { have In1 : mkItem Unique (Tagged t') opro1 ∈ stk.
             { destruct HTOP as [? HTOP]. rewrite HTOP. by left. }
             have EQ := stack_item_tagged_NoDup_eq _ _ _ t' ND2 In1 In eq_refl eq_refl.
-            by simplify_eq. } subst opro1 pm. exists pro.
+            by simplify_eq. } subst opro1 pm'. exists pro.
           have NEq: Tagged t' ≠ otg.
           { intros ?. subst otg. simpl in AREL.
             destruct AREL as (_ & _ & ht & Eqh').
@@ -1575,7 +1590,7 @@ Proof.
           move : HTOP.
           by apply (retag_item_head_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT
                       _ _ _ _ _ ND2 Eqstk1 Eqstk' NEq In').
-        * destruct PRE as (stk' & pm & pro & Eqstk' & In' & ND).
+        * destruct PRE as (stk' & pm' & pro & Eqstk' & In' & ND).
           destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ EqRT _ _ t' _ Eqstk' In')
             as (stk & Eqstk & In); [done..|].
           destruct PINV as (Eqss & Eqst & HP); [simpl; naive_solver|].
@@ -1594,10 +1609,10 @@ Proof.
       intros tc L EqL. specialize (CINV _ _ EqL) as [Ltp CINV].
       split; [by simpl; lia|].
       intros l1 InL. simpl.
-      specialize (CINV _ InL) as (stk & pm & Eqstk & In & NDIS).
+      specialize (CINV _ InL) as (stk & pm' & Eqstk & In & NDIS).
       destruct (retag_item_active_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT
                     _ _ _ _ _ Eqstk Ltc In) as (stk' & Eqstk' & In').
-      by exists stk', pm.
+      by exists stk', pm'.
     - (* TODO: duplicate proof with retag_public *)
       rewrite cmra_assoc. do 4 (split; [done|]).
       move => l' /PUBP [PB|PV].
@@ -1611,9 +1626,13 @@ Proof.
   intros i Lti. split.
   - clear -Lti EqlT.
     apply write_hpl_is_Some. by rewrite EqlT.
-  - move : Lti. eapply tag_on_top_retag_ref_uniq. exact EqRT.
+  - move : Lti.
+    destruct mut.
+    + eapply tag_on_top_retag_ref_uniq. exact EqRT.
+    + eapply tag_on_top_retag_ref_shr; [done|exact EqRT].
 Qed.
 
+
 (** InitCall *)
 Lemma sim_body_init_call fs ft r n es et σs σt Φ :
   let σs' := mkState σs.(shp) σs.(sst) (σs.(snc) :: σs.(scs)) σs.(snp) (S σs.(snc)) in

theories/sim/right_step.v

@@ -49,7 +49,7 @@ Lemma sim_body_copy_local_unique_r
   fs ft (r r': resUR) (h: heaplet) n (l: loc) t k T (ss st: scalar) es σs σt Φ
   (LU: k = tkLocal ∨ k = tkUnique) :
   tsize T = 1%nat →
-  tag_on_top σt.(sst) l t →
+  tag_on_top σt.(sst) l t Unique →
   r ≡ r' ⋅ res_tag t k h →
   h !! l = Some (ss, st) →
   (r ⊨{n,fs,ft} (es, σs) ≥ (#[st], σt) : Φ : Prop) →
@@ -112,7 +112,7 @@ Qed.
 Lemma sim_body_copy_unique_r
   fs ft (r r': resUR) (h: heaplet) n (l: loc) t T (ss st: scalar) es σs σt Φ :
   tsize T = 1%nat →
-  tag_on_top σt.(sst) l t →
+  tag_on_top σt.(sst) l t Unique →
   r ≡ r' ⋅ res_tag t tkUnique h →
   h !! l = Some (ss, st) →
   (r ⊨{n,fs,ft} (es, σs) ≥ (#[st], σt) : Φ : Prop) →
@@ -120,7 +120,7 @@ Lemma sim_body_copy_unique_r
 Proof. apply sim_body_copy_local_unique_r. by right. Qed.
 
 Lemma vsP_res_mapsto_tag_on_top (r: resUR) l t s σs σt :
-  (r ⋅ res_loc l [s] t) ={σs,σt}=> (λ _ _ σt, tag_on_top σt.(sst) l t : Prop).
+  (r ⋅ res_loc l [s] t) ={σs,σt}=> (λ _ _ σt, tag_on_top σt.(sst) l t Unique : Prop).
 Proof.
   intros r_f. rewrite cmra_assoc.
   intros (WFS & WFT & VALID & PINV & CINV & SREL).

theories/sim/simple.v

@@ -317,29 +317,25 @@ Proof.
   eapply sim_simple_copy_local_r; done.
 Qed.
 
-Lemma sim_simple_retag_mut_ref fs ft r n (ptr: scalar) ty Φ :
+Lemma sim_simple_retag_ref fs ft r n (ptr: scalar) m ty Φ :
   (0 < tsize ty)%nat →
+  (if m is Immutable then is_freeze ty else True) →
   arel r ptr ptr →
   (∀ l told tnew hplt,
     ptr = ScPtr l told →
     let s_new := ScPtr l (Tagged tnew) in
-(*    let tk := match m with Mutable => tkUnique | Immutable => tkPub end in
-    match m with
-    | Mutable => is_Some (hplt !! l_inner)
-    | Immutable => if is_freeze ty then is_Some (hplt !! l_inner) else True
-    end → *)
+    let tk := match m with Mutable => tkUnique | Immutable => tkPub end in
     let s_new := ScPtr l (Tagged tnew) in
-    let tk := tkUnique in
     (∀ i: nat, (i < tsize ty)%nat → is_Some $ hplt !! (l +ₗ i)) →
     Φ (r ⋅ res_tag tnew tk hplt) n (ValR [s_new]) (ValR [s_new])) →
   r ⊨ˢ{n,fs,ft}
-    Retag #[ptr] (RefPtr Mutable) ty Default
+    Retag #[ptr] (RefPtr m) ty Default
   ≥
-    Retag #[ptr] (RefPtr Mutable) ty Default
+    Retag #[ptr] (RefPtr m) ty Default
   : Φ.
 Proof.
-  intros ?? HH σs σt.
-  apply sim_body_retag_mut_ref_default; eauto.
+  intros ??? HH σs σt.
+  apply sim_body_retag_ref_default; eauto.
   intros ??????????? HS. do 2 (split; [done|]). eapply HH; eauto.
   intros ??. by apply HS.
 Qed.