state a local retag lemma

theories/opt/ex1.v

@@ -36,9 +36,18 @@ Proof.
   sim_apply sim_simple_let_place=>/=.
   (* Write *)
   rewrite (vrel_eq _ _ _ FREL).
-  sim_apply sim_simple_write_local; first solve_res.
-  intros s ->. clear dependent vs. simpl.
+  sim_apply sim_simple_write_local. solve_res.
+  intros s ->. simpl.
   sim_apply sim_simple_let_val=>/=.
   apply sim_simple_place.
-
+  (* Retag. *)
+  sim_apply sim_simple_let_place=>/=.
+  destruct vs as [|s' vs]; first by inversion FREL.
+  apply Forall2_cons_inv in FREL as [FREL FTAIL].
+  destruct vs as [|]; last by inversion FTAIL. clear FTAIL.
+  sim_apply sim_simple_retag_local. solve_res. done. solve_res.
+  move=>l_i tg_i hplt /= Hl_i.
+  (* Call *)
+  sim_apply sim_simple_let_val=>/=.
+  
 Abort.

theories/sim/cmra.v

@@ -296,8 +296,11 @@ Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
 
 (** Resources that we own. *)
 
+Definition res_tag tg tk h : resUR :=
+  ({[tg := (to_tagKindR tk, to_agree <$> h)]}, ε, ε).
+
 Definition res_callState (c: call_id) (cs: call_state) : resUR :=
-  ((ε, {[c := to_callStateR cs]}), ε).
+  (ε, {[c := to_callStateR cs]}, ε).
 
 Definition res_mapsto l s stk : resUR :=
-  (ε, {[ l := to_locStateR (lsLocal s stk)]}).
+  (ε, ε, {[ l := to_locStateR (lsLocal s stk)]}).

theories/sim/simple.v

@@ -115,7 +115,6 @@ Proof.
   intros HH σs σt <-<-. apply sim_body_alloc_local=>/=. eauto.
 Qed.
 
-(* FIXME notation is so broken, can one write this down without the Val? *)
 Lemma sim_simple_write_local fs ft r r' n l tg Ts Tt v v' css cst Φ :
   r ≡ r' ⋅ res_mapsto l v' (init_stack (Tagged tg)) →
   (∀ s, v = [s] → Φ (r' ⋅ res_mapsto l s (init_stack (Tagged tg))) n (ValR [☠%S]) css (ValR [☠%S]) cst) →
@@ -125,6 +124,26 @@ Lemma sim_simple_write_local fs ft r r' n l tg Ts Tt v v' css cst Φ :
 Proof.
 Admitted.
 
+Lemma sim_simple_retag_local fs ft r r' r'' rf n l s' s tg m ty css cst Φ :
+  r ≡ r' ⋅ res_mapsto l s (init_stack (Tagged tg)) →
+  arel rf s' s →
+  r' ≡ r'' ⋅ rf →
+  (∀ l_inner tg_inner hplt,
+    let s := ScPtr l_inner (Tagged tg_inner) 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 →
+    Φ (r' ⋅ res_mapsto l s (init_stack (Tagged tg)) ⋅ res_tag tg_inner tk hplt) n (ValR [☠%S]) css (ValR [☠%S]) cst) →
+  r ⊨ˢ{n,fs,ft}
+    (Retag (Place l (Tagged tg) (Reference (RefPtr m) ty)) Default, css)
+  ≥
+    (Retag (Place l (Tagged tg) (Reference (RefPtr m) ty)) Default, cst)
+  : Φ.
+Proof.
+Admitted.
+
 (** * Pure *)
 Lemma sim_simple_let_val fs ft r n x (vs1 vt1: value) es2 et2 css cst Φ :
   r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css) ≥ (subst' x vt1 et2, cst) : Φ →