From 973be9349877aee8cb41af13544959f885f97887 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Jul 2019 00:21:54 +0200
Subject: [PATCH] lots of stubs for ex1

---
 theories/lang/notation.v      |  2 +-
 theories/lang/steps_retag.v   |  2 ++
 theories/opt/ex1.v            | 49 ++++++++++++++++++++++++++----
 theories/sim/body.v           | 27 +++++++++++++++--
 theories/sim/cmra.v           |  3 +-
 theories/sim/left_step.v      | 39 ++++++++++++++++++++++++
 theories/sim/refl.v           |  2 +-
 theories/sim/refl_mem_step.v  | 31 +++++++++++++++----
 theories/sim/refl_pure_step.v | 14 ++++++---
 theories/sim/right_step.v     | 47 +++++++++++++++++++++++------
 theories/sim/simple.v         | 38 +++++++++++++++++-------
 theories/sim/tactics.v        | 56 ++++++++++++++++++++++++++++-------
 12 files changed, 260 insertions(+), 50 deletions(-)

diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 0d8b606..8cf0f4e 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -53,7 +53,7 @@ Notation "'Box<' T '>'" := (Reference RawPtr T%T)
 
 (** Pointer operations *)
 Notation "& e" := (Ref e%E) (at level 8, format "& e") : expr_scope.
-Notation "*{ T } e" := (Deref (Proj (Copy e%E) #[0]) T%T)
+Notation "*{ T } e" := (Deref (Copy e%E) T%T)
   (at level 9, format "*{ T }  e") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
diff --git a/theories/lang/steps_retag.v b/theories/lang/steps_retag.v
index a258410..41f5f26 100644
--- a/theories/lang/steps_retag.v
+++ b/theories/lang/steps_retag.v
@@ -6,6 +6,8 @@ Definition tag_in t (stk: stack) :=
   ∃ pm opro, pm ≠ Disabled ∧ mkItem pm (Tagged t) opro ∈ stk.
 Definition tag_in_stack σ l t :=
   ∃ stk, σ.(sst) !! l = Some stk ∧ tag_in t stk.
+Definition tag_on_top σt l tag : Prop :=
+  tg <$> (σt.(sst) !! l) ≫= head = Some (Tagged tag).
 
 (** Active protector preserving *)
 Definition active_preserving (cids: call_id_stack) (stk stk': stack) :=
diff --git a/theories/opt/ex1.v b/theories/opt/ex1.v
index 71b7e7c..093cda1 100644
--- a/theories/opt/ex1.v
+++ b/theories/opt/ex1.v
@@ -1,4 +1,4 @@
-From stbor.sim Require Import local invariant refl tactics simple program.
+From stbor.sim Require Import local invariant refl tactics simple program refl_step right_step left_step.
 
 Set Default Proof Using "Type".
 
@@ -33,16 +33,16 @@ Proof.
   simplify_eq/=.
   (* InitCall *)
   apply sim_simple_init_call=> c /= {css}.
-  (* Alloc *)
+  (* Alloc local *)
   sim_apply sim_simple_alloc_local=> l t /=.
   sim_apply sim_simple_let=>/=.
-  (* Write *)
+  (* Write local *)
   rewrite (vrel_eq _ _ _ AREL).
   sim_apply sim_simple_write_local; [solve_sim..|].
   intros arg ->. simpl.
   sim_apply sim_simple_let=>/=.
   apply: sim_simple_result.
-  (* Retag. *)
+  (* Retag local *)
   sim_apply sim_simple_let=>/=.
   destruct args as [|args args']; first by inversion AREL.
   apply Forall2_cons_inv in AREL as [AREL ATAIL].
@@ -55,8 +55,45 @@ Proof.
   intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
   apply: sim_simple_result. simpl.
   sim_apply sim_simple_let=>/=.
-  (* Deref *)
-
+  (* Copy local *)
+  sim_apply sim_simple_copy_local; [solve_sim..|].
+  apply: sim_simple_result. simpl.
+  sim_apply sim_simple_deref=>l' t' ?. simplify_eq/=.
+  (* Write unique. We need to drop to complex mode, to preserve some local state info. *)
+  intros σs σt Hσs Hσt. 
+  sim_apply sim_body_write_owned; [solve_sim..|].
+  intros ???? Htop. simplify_eq/=.
+  sim_apply sim_body_let. simplify_eq/=.
+  (* Copy local (right) *)
+  sim_apply_r sim_body_copy_local_r; [solve_sim..|].
+  apply: sim_body_result=>_. simpl.
+  (* Copy unique (right) *)
+  sim_apply_r sim_body_deref_r. simpl.
+  sim_apply_r sim_body_copy_unique_r; [try solve_sim..|].
+  { subst σt'. admit. (* show that tag_op_top is preserved. *) }
+  { rewrite lookup_insert. done. }
+  apply: sim_body_result=>_. simpl.
+  apply: sim_body_let_r. simpl. (* FIXME: figure out why [sim_apply_r] does the wrong thing here *)
+  (* We can go back to simple mode! *)
+  eapply sim_simplify. { intros ?????? HH. exact HH. }
+  simplify_eq/=. rewrite Hσs Hσt. clear- AREL FREL LOOK.
+  (* Call *)
+  sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
+  intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
+  apply: sim_simple_result. simpl.
+  sim_apply sim_simple_let=>/=.
+  (* Copy local (left). We drop to complex just because simple does not support this yet. *)
+  intros σs σt Hσs Hσt.
+  sim_apply_l sim_body_copy_local_l; [solve_sim..|].
+  apply: sim_body_result=>_. simpl.
+  (* Copy unique (left) *)
+  sim_apply_l sim_body_deref_l. simpl.
+  sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
+  { rewrite lookup_insert. done. }
+  apply: sim_body_result=>_. simpl.
+  apply: sim_body_result=>Hval. split.
+  - eexists. split; first done. admit. (* end_call_sat *)
+  - constructor; simpl; auto.
 Admitted.
 
 (** Top-level theorem: Two programs that only differ in the
diff --git a/theories/sim/body.v b/theories/sim/body.v
index cdf2e24..d7f8503 100644
--- a/theories/sim/body.v
+++ b/theories/sim/body.v
@@ -44,9 +44,10 @@ Proof.
   intros. eapply HΦ; done.
 Qed.
 
-Lemma sim_body_bind fs ft r n
-  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
-  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) es et σs σt Φ :
+Lemma sim_body_bind fs ft
+  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) es
+  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
+  r n σs σt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt)
     : (λ r' n' es' σs' et' σt',
         r' ⊨{n',fs,ft} (fill Ks es', σs') ≥ (fill Kt et', σt') : Φ) →
@@ -132,6 +133,26 @@ Proof.
     pclearbot. right. by apply CIH. }
 Qed.
 
+Lemma sim_body_bind_r fs ft
+  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
+  r n es σs σt Φ :
+  r ⊨{n,fs,ft} (#[], σs) ≥ (et, σt)
+    : (λ r' n' _ _ et' σt',
+        r' ⊨{n',fs,ft} (es, σs) ≥ (fill Kt et', σt') : Φ) →
+  r ⊨{n,fs,ft} (es, σs) ≥ (fill Kt et, σt) : Φ.
+Proof.
+Admitted.
+
+Lemma sim_body_bind_l fs ft
+  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) es
+  r n et σs σt Φ :
+  r ⊨{n,fs,ft} (es, σs) ≥ (#[], σt)
+    : (λ r' n' es' σs' _ _,
+        r' ⊨{n',fs,ft} (fill Ks es', σs') ≥ (et, σt) : Φ) →
+  r ⊨{n,fs,ft} (fill Ks es, σs) ≥ (et, σt) : Φ.
+Proof.
+Admitted.
+
 Lemma sim_body_bind_call r n fs ft es σs et σt (fns fnt: result) (pres pret: list result) posts postt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt)
     : (λ r' n' rs' σs' rt' σt',
diff --git a/theories/sim/cmra.v b/theories/sim/cmra.v
index 15556b2..011e9d0 100644
--- a/theories/sim/cmra.v
+++ b/theories/sim/cmra.v
@@ -26,6 +26,7 @@ Definition cmapUR := gmapUR call_id callStateR.
 Definition to_cmapUR (cm: cmap) : cmapUR := fmap to_callStateR cm.
 
 Definition tmap := gmap ptr_id (tag_kind * mem).
+Definition heaplet := gmap loc scalar.
 Definition heapletR := gmapR loc (agreeR scalarC).
 (* ptr_id ⇀ TagKid x (loc ⇀ Ag(Scalar)) *)
 Definition tmapUR := gmapUR ptr_id (prodR tagKindR heapletR).
@@ -352,7 +353,7 @@ Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
 
 (** Resources that we own. *)
 
-Definition res_tag tg tk h : resUR :=
+Definition res_tag tg tk (h: heaplet) : resUR :=
   ({[tg := (to_tagKindR tk, to_agree <$> h)]}, ε, ε).
 
 Definition res_callState (c: call_id) (cs: call_state) : resUR :=
diff --git a/theories/sim/left_step.v b/theories/sim/left_step.v
index 1f12cd4..f83d8cd 100644
--- a/theories/sim/left_step.v
+++ b/theories/sim/left_step.v
@@ -5,6 +5,43 @@ From stbor.sim Require Export instance.
 
 Set Default Proof Using "Type".
 
+Section left.
+Implicit Types Φ: resUR → nat → result → state → result → state → Prop.
+
+Lemma sim_body_let_l fs ft r n x et es1 es2 vs1 σs σt Φ :
+  IntoResult es1 vs1 →
+  r ⊨{n,fs,ft} (subst' x es1 es2, σs) ≥ (et, σt) : Φ →
+  r ⊨{n,fs,ft} (let: x := es1 in es2, σs) ≥ (et, σt) : Φ.
+Proof.
+Admitted.
+
+Lemma sim_body_deref_l fs ft r n et (rt: result) l t T σs σt Φ :
+  IntoResult et rt →
+  (Φ r n (PlaceR l t T) σs rt σt) →
+  r ⊨{n,fs,ft} (Deref #[ScPtr l t] T, σs) ≥ (et, σt) : Φ.
+Proof.
+Admitted.
+
+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 1 s tg →
+  (r ⊨{n,fs,ft} (#[s], σs) ≥ (et, σt) : Φ) →
+  r ⊨{n,fs,ft}
+    (Copy (Place l (Tagged tg) ty), σs) ≥ (et, σt)
+  : Φ.
+Proof.
+Admitted.
+
+Lemma sim_body_copy_unique_l
+  fs ft (r r': resUR) (h: heaplet) n (l: loc) tg T (s: scalar) et σs σt Φ :
+  tsize T = 1%nat →
+  r ≡ r' ⋅ res_tag tg 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) : Φ.
+Proof.
+Admitted.
+
 Lemma sim_body_copy_left_1
   fs ft (r: resUR) k (h: heapletR) n l t et σs σt Φ
   (UNIQUE: r.(rtm) !! t ≡ Some (k, h))
@@ -33,3 +70,5 @@ Proof.
   { (* follows COND *) admit. }
   { (* follows COND *) admit. }
 Abort.
+
+End left.
diff --git a/theories/sim/refl.v b/theories/sim/refl.v
index 54b6145..5defbf3 100644
--- a/theories/sim/refl.v
+++ b/theories/sim/refl.v
@@ -255,7 +255,7 @@ Proof using Type*.
     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 ?]%rrel_with_eq).
-    simplify_eq/=. eapply sim_simple_deref=>l t ?. simplify_eq/=.
+    simplify_eq/=. apply: sim_simple_deref=>l t ?. simplify_eq/=.
     do 3 (split; first done). done.
   - (* Ref *)
     move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
diff --git a/theories/sim/refl_mem_step.v b/theories/sim/refl_mem_step.v
index 19d8dcd..c20a62c 100644
--- a/theories/sim/refl_mem_step.v
+++ b/theories/sim/refl_mem_step.v
@@ -5,6 +5,8 @@ From stbor.sim Require Export instance body.
 
 Set Default Proof Using "Type".
 
+Section mem.
+Implicit Types Φ: resUR → nat → result → state → result → state → Prop.
 
 (** MEM STEP -----------------------------------------------------------------*)
 
@@ -30,7 +32,7 @@ Lemma sim_body_alloc_local fs ft r n T σs σt Φ :
                      (S σt.(snp)) σt.(snc) in
   let rt : resUR := res_tag σt.(snp) tkUnique ∅ in
   let r' : resUR := res_mapsto l (tsize T) ☠ σt.(snp) in
-  Φ (r ⋅ rt ⋅ r') n (PlaceR l t T) σs' (PlaceR l t T) σt' : Prop →
+  Φ (r ⋅ rt ⋅ r') n (PlaceR l t T) σs' (PlaceR l t T) σt' →
   r ⊨{n,fs,ft} (Alloc T, σs) ≥ (Alloc T, σt) : Φ.
 Proof.
   intros l t σs' σt' rt r' POST.
@@ -351,7 +353,7 @@ Lemma sim_body_copy_public fs ft r n l t Ts Tt σs σt Φ
     ∀ α', memory_read σt.(sst) σt.(scs) l (Tagged t) (tsize Tt) = Some α' →
       let σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc) in
       let σt' := mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc) in
-      vrel (r ⋅ r') vs vt → Φ (r ⋅ r') n (ValR vs) σs' (ValR vt) σt' : Prop) →
+      vrel (r ⋅ r') vs vt → Φ (r ⋅ r') n (ValR vs) σs' (ValR vt) σt') →
   r ⊨{n,fs,ft} (Copy (Place l (Tagged t) Ts), σs) ≥ (Copy (Place l (Tagged t) Tt), σt) : Φ.
 Proof.
   intros POST. pfold.
@@ -580,7 +582,7 @@ Lemma sim_body_write_local_1 fs ft r r' n l tg T v v' σs σt Φ :
     let σs' := mkState (<[l := s]> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
     let σt' := mkState (<[l := s]> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
     Φ (r' ⋅ res_mapsto l 1 s tg) n
-      (ValR [☠%S]) σs' (ValR [☠%S]) σt' : Prop) →
+      (ValR [☠%S]) σs' (ValR [☠%S]) σt') →
   r ⊨{n,fs,ft}
     (Place l (Tagged tg) T <- #v, σs) ≥ (Place l (Tagged tg) T <- #v, σt) : Φ.
 Proof.
@@ -739,7 +741,7 @@ Lemma sim_body_write_related_values
   (∀ α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize Tt) = Some α' →
     let σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
     let σt' := mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
-    Φ r' n ((#[☠])%V) σs' ((#[☠]%V)) σt' : Prop) →
+    Φ r' n (ValR [☠]%S) σs' (ValR [☠]%S) σt' : Prop) →
   r ⊨{n,fs,ft}
     (Place l (Tagged tg) Ts <- #v, σs) ≥ (Place l (Tagged tg) Tt <- #v, σt) : Φ.
 Proof.
@@ -1032,6 +1034,23 @@ Proof.
   intros. simpl. by apply POST.
 Qed.
 
+(** can probably be derived from [write_related_values]? *)
+Lemma sim_body_write_owned
+  fs ft (r r' r'' rs: resUR) h n l tg T s σs σt Φ:
+  tsize T = 1%nat →
+  r ≡ r' ⋅ res_tag tg tkUnique h →
+  arel rs s s → (* assuming to-write values are related *)
+  r' ≡ r'' ⋅ rs →
+  (∀ α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize T) = Some α' →
+    let σs' := mkState (write_mem l [s] σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
+    let σt' := mkState (write_mem l [s] σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
+    tag_on_top σt l tg →
+    Φ (r' ⋅ res_tag tg tkUnique (<[l:=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) : Φ.
+Proof.
+Admitted.
+
 (** Retag *)
 
 Lemma retag_ref_change_1 h α cids c nxtp x rk mut T h' α' nxtp'
@@ -1108,7 +1127,7 @@ Lemma sim_body_retag_default fs ft r n x xtag mut T σs σt Φ
       = Some (hs', αs', nps') →
     let σs' := mkState hs' αs' σs.(scs) nps' σs.(snc) in
     let σt' := mkState ht' αt' σt.(scs) npt' σt.(snc) in
-      Φ r n ((#[☠])%V) σs' ((#[☠]%V)) σt' : Prop) →
+      Φ r n (ValR [☠]%S) σs' (ValR [☠]%S) σt' : Prop) →
   r ⊨{n,fs,ft}
     (Retag (Place x xtag Tr) Default, σs) ≥
     (Retag (Place x xtag Tr) Default, σt) : Φ.
@@ -1353,3 +1372,5 @@ Proof.
         simplify_eq. split; [done|]. eexists. split; [|done]. by apply tc_once. }
   subst. simpl. by exists vs, vt.
 Qed.
+
+End mem.
diff --git a/theories/sim/refl_pure_step.v b/theories/sim/refl_pure_step.v
index 9dfe727..2e3b6a3 100644
--- a/theories/sim/refl_pure_step.v
+++ b/theories/sim/refl_pure_step.v
@@ -5,6 +5,10 @@ From stbor.sim Require Export instance body.
 
 Set Default Proof Using "Type".
 
+Section pure.
+Implicit Types Φ: resUR → nat → result → state → result → state → Prop.
+
+
 (** PURE STEP ----------------------------------------------------------------*)
 
 (** Call - step over *)
@@ -88,7 +92,7 @@ Qed.
 (** Conc *)
 Lemma sim_body_conc fs ft r n (r1 r2: result) σs σt Φ :
   (∀ v1 v2, r1 = ValR v1 → r2 = ValR v2 →
-    Φ r n (ValR (v1 ++ v2)) σs (ValR (v1 ++ v2)) σt : Prop) →
+    Φ r n (ValR (v1 ++ v2)) σs (ValR (v1 ++ v2)) σt) →
   r ⊨{n,fs,ft} (Conc r1 r2, σs) ≥ (Conc r1 r2, σt) : Φ.
 Proof.
   intros POST. pfold. intros NT r_f WSAT. split; [|done|].
@@ -110,7 +114,7 @@ Qed.
 Lemma sim_body_bin_op fs ft r n op (r1 r2: result) σs σt Φ :
   (∀ s1 s2 s, r1 = ValR [s1] → r2 = ValR [s2] →
     bin_op_eval σt.(shp) op s1 s2 s →
-    Φ r n (ValR [s]) σs (ValR [s]) σt : Prop) →
+    Φ r n (ValR [s]) σs (ValR [s]) σt) →
   r ⊨{n,fs,ft} (BinOp op r1 r2, σs) ≥ (BinOp op r1 r2, σt) : Φ.
 Proof.
   intros POST. pfold. intros NT r_f WSAT. split; [|done|].
@@ -180,7 +184,7 @@ Qed.
 (** Ref *)
 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 (ValR [ScPtr l t]) σs (ValR [ScPtr l t]) σt) →
   r ⊨{n,fs,ft} ((& pl)%E, σs) ≥ ((& pl)%E, σt) : Φ.
 Proof.
   intros POST. pfold.
@@ -211,7 +215,7 @@ Qed.
 (** Deref *)
 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 (PlaceR l t T) σs (PlaceR l t T) σt) →
   r ⊨{n,fs,ft} (Deref rf T, σs) ≥ (Deref rf T, σt) : Φ.
 Proof.
   intros POST. pfold.
@@ -236,3 +240,5 @@ Proof.
   left. apply: sim_body_result.
   intros. by eapply POST.
 Qed.
+
+End pure.
diff --git a/theories/sim/right_step.v b/theories/sim/right_step.v
index 6c15b61..9f7877f 100644
--- a/theories/sim/right_step.v
+++ b/theories/sim/right_step.v
@@ -5,13 +5,42 @@ From stbor.sim Require Export instance.
 
 Set Default Proof Using "Type".
 
-Lemma sim_body_copy_right_1
-  fs ft (r: resUR) k (h: heapletR) n l t s es σs σt Φ
-  (* we know we're going to read s *)
-  (UNIQUE: r.(rtm) !! t ≡ Some (k, h))
-  (InD: h !! l ≡ Some (to_agree s))
-  (IN: tag_in_stack σt l t) :
-  (σt.(shp) !! l = Some s → r ⊨{n,fs,ft} (es, σs) ≥ (#[s%S], σt) : Φ : Prop) →
-  r ⊨{n,fs,ft} (es, σs) ≥ (Copy (Place l (Tagged t) int), σt) : Φ.
+Section right.
+Implicit Types Φ: resUR → nat → result → state → result → state → Prop.
+
+Lemma sim_body_let_r fs ft r n x es et1 et2 vt1 σs σt Φ :
+  IntoResult et1 vt1 →
+  r ⊨{n,fs,ft} (es, σs) ≥ (subst' x et1 et2, σt) : Φ →
+  r ⊨{S n,fs,ft} (es, σs) ≥ (let: x := et1 in et2, σt) : Φ.
+Proof.
+Admitted.
+
+Lemma sim_body_deref_r fs ft r n es (rs: result) l t T σs σt Φ :
+  IntoResult es rs →
+  (Φ r n rs σs (PlaceR l t T) σt) →
+  r ⊨{S n,fs,ft} (es, σs) ≥ (Deref #[ScPtr l t] T, σt) : Φ.
+Proof.
+Admitted.
+
+Lemma sim_body_copy_local_r fs ft r r' n l tg ty s es σs σt Φ :
+  tsize ty = 1%nat →
+  r ≡ r' ⋅ res_mapsto l 1 s tg →
+  (r ⊨{n,fs,ft} (es, σs) ≥ (#[s], σt) : Φ) →
+  r ⊨{S n,fs,ft}
+    (es, σs) ≥ (Copy (Place l (Tagged tg) ty), σt)
+  : Φ.
+Proof.
+Admitted.
+
+Lemma sim_body_copy_unique_r
+  fs ft (r r': resUR) (h: heaplet) n (l: loc) tg T (s: scalar) es σs σt Φ :
+  tsize T = 1%nat →
+  tag_on_top σt l tg →
+  r ≡ r' ⋅ res_tag tg tkUnique h →
+  h !! l = Some s →
+  (r ⊨{n,fs,ft} (es, σs) ≥ (#[s], σt) : Φ : Prop) →
+  r ⊨{S n,fs,ft} (es, σs) ≥ (Copy (Place l (Tagged tg) T), σt) : Φ.
 Proof.
-Abort.
+Admitted.
+
+End right.
diff --git a/theories/sim/simple.v b/theories/sim/simple.v
index 693499f..5311457 100644
--- a/theories/sim/simple.v
+++ b/theories/sim/simple.v
@@ -8,7 +8,7 @@ want to clean some stuff from your context.
 *)
 
 From stbor.sim Require Export body instance.
-From stbor.sim Require Import refl_step.
+From stbor.sim Require Import refl_step right_step left_step.
 
 Definition fun_post_simple
   initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst :=
@@ -167,9 +167,9 @@ Proof.
 Qed.
 
 Lemma sim_simple_bind fs ft
-  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
-  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft)))
-  es et r n css cst Φ :
+  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs))) es
+  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft))) et
+  r n css cst Φ :
   r ⊨ˢ{n,fs,ft} (es, css) ≥ (et, cst)
     : (λ r' n' es' css' et' cst',
         r' ⊨ˢ{n',fs,ft} (fill Ks es', css') ≥ (fill Kt et', cst') : Φ) →
@@ -268,17 +268,34 @@ Lemma sim_simple_copy_local_l fs ft r r' n l tg ty s et css cst Φ :
     (Copy (Place l (Tagged tg) ty), css) ≥ (et, cst)
   : Φ.
 Proof.
-Admitted.
+  intros ?? Hold σs σt <- <-.
+  eapply sim_body_copy_local_l; eauto.
+Qed.
 
 Lemma sim_simple_copy_local_r fs ft r r' n l tg ty s es css cst Φ :
   tsize ty = 1%nat →
   r ≡ r' ⋅ res_mapsto l 1 s tg →
   (r ⊨ˢ{n,fs,ft} (es, css) ≥ (#[s], cst) : Φ) →
-  r ⊨ˢ{n,fs,ft}
+  r ⊨ˢ{S n,fs,ft}
     (es, css) ≥ (Copy (Place l (Tagged tg) ty), cst)
   : Φ.
 Proof.
-Admitted.
+  intros ?? Hold σs σt <- <-.
+  eapply sim_body_copy_local_r; eauto.
+Qed.
+
+Lemma sim_simple_copy_local fs ft r r' n l tg ty s css cst Φ :
+  tsize ty = 1%nat →
+  r ≡ r' ⋅ res_mapsto l 1 s tg →
+  (r ⊨ˢ{n,fs,ft} (#[s], css) ≥ (#[s], cst) : Φ) →
+  r ⊨ˢ{S n,fs,ft}
+    (Copy (Place l (Tagged tg) ty), css) ≥ (Copy (Place l (Tagged tg) ty), cst)
+  : Φ.
+Proof.
+  intros ?? Hcont.
+  eapply sim_simple_copy_local_l; [done..|].
+  eapply sim_simple_copy_local_r; done.
+Qed.
 
 Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty css cst Φ :
   r ≡ r' ⋅ res_mapsto l 1 s tg →
@@ -351,11 +368,12 @@ Lemma sim_simple_ref fs ft r n (pl: result) css 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 (rf: result) T css cst Φ :
+Lemma sim_simple_deref fs ft r n ef (rf: result) T css cst Φ :
+  IntoResult ef rf →
   (∀ 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.
+  r ⊨ˢ{n,fs,ft} (Deref ef T, css) ≥ (Deref ef 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) : Φ.
diff --git a/theories/sim/tactics.v b/theories/sim/tactics.v
index 974c58a..45acfdc 100644
--- a/theories/sim/tactics.v
+++ b/theories/sim/tactics.v
@@ -41,23 +41,23 @@ Ltac reshape_expr e tac :=
 
 (** bind if K is not empty. Otherwise do nothing.
 Binds cost us steps, so don't waste them! *)
-Ltac sim_body_bind_core Ks Kt es et :=
+Ltac sim_body_bind_core Ks es Kt et :=
   (* Ltac is SUCH a bad language... *)
   match Ks with
   | [] => match Kt with
           | [] => idtac
-          | _ => eapply (sim_body_bind _ _ _ _ Ks Kt es et)
+          | _ => eapply (sim_body_bind _ _ Ks es Kt et)
           end
-  | _ => eapply (sim_body_bind _ _ _ _ Ks Kt es et)
+  | _ => eapply (sim_body_bind _ _ Ks es Kt et)
   end.
-Ltac sim_simple_bind_core Ks Kt es et :=
+Ltac sim_simple_bind_core Ks es Kt et :=
   (* Ltac is SUCH a bad language... *)
   match Ks with
   | [] => match Kt with
           | [] => idtac
-          | _ => eapply (sim_simple_bind _ _ Ks Kt es et)
+          | _ => eapply (sim_simple_bind _ _ Ks es Kt et)
           end
-  | _ => eapply (sim_simple_bind _ _ Ks Kt es et)
+  | _ => eapply (sim_simple_bind _ _ Ks es Kt et)
   end.
 
 Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
@@ -67,7 +67,7 @@ Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
       unify es efocs;
       reshape_expr et ltac:(fun Kt et =>
         unify et efoct;
-        sim_body_bind_core Ks Kt es et
+        sim_body_bind_core Ks es Kt et
       )
     )
   | |- _ ⊨ˢ{_,_,_} (?es, _) ≥ (?et, _) : _ =>
@@ -75,7 +75,7 @@ Tactic Notation "sim_bind" open_constr(efocs) open_constr(efoct) :=
       unify es efocs;
       reshape_expr et ltac:(fun Kt et =>
         unify et efoct;
-        sim_simple_bind_core Ks Kt es et
+        sim_simple_bind_core Ks es Kt et
       )
     )
   end.
@@ -85,19 +85,55 @@ Tactic Notation "sim_apply" open_constr(lem) :=
   | |- _ ⊨{_,_,_} (?es, _) ≥ (?et, _) : _ =>
     reshape_expr es ltac:(fun Ks es =>
       reshape_expr et ltac:(fun Kt et =>
-        sim_body_bind_core Ks Kt es et;
+        sim_body_bind_core Ks es Kt et;
         apply: lem
       )
     )
   | |- _ ⊨ˢ{_,_,_} (?es, _) ≥ (?et, _) : _ =>
     reshape_expr es ltac:(fun Ks es =>
       reshape_expr et ltac:(fun Kt et =>
-        sim_simple_bind_core Ks Kt es et;
+        sim_simple_bind_core Ks es Kt et;
         apply: lem
       )
     )
   end.
 
+Tactic Notation "sim_bind_r" open_constr(efoc) :=
+  match goal with 
+  | |- _ ⊨{_,_,_} (_, _) ≥ (?et, _) : _ =>
+    reshape_expr et ltac:(fun Kt et =>
+      unify et efoc;
+      eapply (sim_body_bind_r _ _ Kt et)
+    )
+  end.
+
+Tactic Notation "sim_apply_r" open_constr(lem) :=
+  match goal with
+  | |- _ ⊨{_,_,_} (?es, _) ≥ (?et, _) : _ =>
+    reshape_expr et ltac:(fun Kt et =>
+      eapply (sim_body_bind_r _ _ Kt et);
+      apply: lem
+    )
+  end.
+
+Tactic Notation "sim_bind_l" open_constr(efoc) :=
+  match goal with 
+  | |- _ ⊨{_,_,_} (?es, _) ≥ (_, _) : _ =>
+    reshape_expr es ltac:(fun Ks es =>
+      unify es efoc;
+      eapply (sim_body_bind_l _ _ Ks es)
+    )
+  end.
+
+Tactic Notation "sim_apply_l" open_constr(lem) :=
+  match goal with
+  | |- _ ⊨{_,_,_} (?es, _) ≥ (_, _) : _ =>
+    reshape_expr es ltac:(fun Ks es =>
+      eapply (sim_body_bind_l _ _ Ks es);
+      apply: lem
+    )
+  end.
+
 
 (** The expectation is that lemmas state their resource requirements as
 [r ≡ frame ⋅ what_lemma_needs].  Users eapply the lemma, and [frame]
-- 
GitLab