diff --git a/theories/sim/body.v b/theories/sim/body.v
index f955efb1adddbde3a0de7c064478c75a1b6acdad..ca2ac1f9dd8a8da066361c04861cf941931efa63 100644
--- a/theories/sim/body.v
+++ b/theories/sim/body.v
@@ -172,11 +172,11 @@ Proof.
 Qed.
 Global Instance: Params (@sim_local_body) 5.
 
-Lemma sim_body_frame' fs ft n (rf r: resUR) es σs et σt Φ :
+Lemma sim_body_frame_r' fs ft n (rf r: resUR) es σs et σt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ : Prop →
   ∀ (r': resUR), r' ≡ rf ⋅ r →
     r' ⊨{n,fs,ft} (es, σs) ≥ (et, σt) :
-    (λ r' n' es' σs' et' σt', ∃ r0, r' = rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
+    (λ r' n' es' σs' et' σt', ∃ r0, r' = r0 ⋅ rf ∧ Φ r0 n' es' σs' et' σt').
 Proof.
   revert n rf r es σs et σt Φ. pcofix CIH.
   intros n rf r0 es σs et σt Φ SIM r' EQ'.
@@ -185,8 +185,9 @@ Proof.
   rewrite ->EQ', ->(cmra_assoc r_f rf r0) in WSAT.
   specialize (SIM NT _ WSAT) as [SU TE ST]. split; [done|..].
   { intros. destruct (TE _ TERM) as (vs' & σs' & r2 & STEP' & WSAT' & POST).
-    exists vs', σs', (rf ⋅ r2).
-    split; last split; [done|by rewrite cmra_assoc|by exists r2]. }
+    exists vs', σs', (r2 ⋅ rf).
+    split; last split; [done|by rewrite [r2 ⋅ rf]comm cmra_assoc|by exists r2].
+ }
   inversion ST.
   - constructor 1. intros.
     specialize (STEP _ _ STEPT) as (es' & σs' & r2 & idx' & STEPS' & WSAT' & SIM').
@@ -201,11 +202,57 @@ Proof.
     exists idx'. pclearbot. right. eapply CIH; eauto. by rewrite cmra_assoc.
 Qed.
 
-Lemma sim_body_frame fs ft n (rf r: resUR) es σs et σt Φ :
+(* So ugly. We just copy the above proof to get the version with the frame added
+on the other side.  There *probably* is a better way... *)
+Lemma sim_body_frame_l' fs ft n (rf r: resUR) es σs et σt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ : Prop →
-  rf ⋅ r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) :
+  ∀ (r': resUR), r' ≡ rf ⋅ r →
+    r' ⊨{n,fs,ft} (es, σs) ≥ (et, σt) :
     (λ r' n' es' σs' et' σt', ∃ r0, r' = rf ⋅ r0 ∧ Φ r0 n' es' σs' et' σt').
-Proof. intros. eapply sim_body_frame'; eauto. Qed.
+Proof.
+  revert n rf r es σs et σt Φ. pcofix CIH.
+  intros n rf r0 es σs et σt Φ SIM r' EQ'.
+  pfold. punfold SIM.
+  intros NT r_f WSAT.
+  rewrite ->EQ', ->(cmra_assoc r_f rf r0) in WSAT.
+  specialize (SIM NT _ WSAT) as [SU TE ST]. split; [done|..].
+  { intros. destruct (TE _ TERM) as (vs' & σs' & r2 & STEP' & WSAT' & POST).
+    exists vs', σs', (rf ⋅ r2).
+    split; last split; [done|by rewrite cmra_assoc|by exists r2].
+ }
+  inversion ST.
+  - constructor 1. intros.
+    specialize (STEP _ _ STEPT) as (es' & σs' & r2 & idx' & STEPS' & WSAT' & SIM').
+    exists es', σs', (rf ⋅ r2), idx'.
+    split; last split; [done|by rewrite cmra_assoc|].
+    pclearbot. right. by eapply CIH.
+  - econstructor 2; eauto.
+    { instantiate (1:= rf ⋅ rc). by rewrite -cmra_assoc (cmra_assoc r_f). }
+    intros.
+    specialize (CONT _ _ _ σs' σt' VRET) as [idx' SIM']; [|done|].
+    { move : WSAT1. by rewrite 3!cmra_assoc. }
+    exists idx'. pclearbot. right. eapply CIH; eauto. by rewrite cmra_assoc.
+Qed.
+
+Lemma sim_body_frame_r fs ft n (rf r: resUR) es σs et σt Φ :
+  r ⊨{n,fs,ft}
+    (es, σs) ≥ (et, σt)
+  : (λ r' n' es' σs' et' σt', Φ (r' ⋅ rf) n' es' σs' et' σt') →
+  r ⋅ rf ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ.
+Proof.
+  intros HH. eapply sim_local_body_post_mono, sim_body_frame_r'; [|done|by rewrite comm].
+  simpl. intros r' n' es' σs' et' σt' (rf' & -> & ?). done.
+Qed.
+
+Lemma sim_body_frame_l fs ft n (rf r: resUR) es σs et σt Φ :
+  r ⊨{n,fs,ft}
+    (es, σs) ≥ (et, σt)
+  : (λ r' n' es' σs' et' σt', Φ (rf ⋅ r') n' es' σs' et' σt') →
+  rf ⋅ r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ.
+Proof.
+  intros HH. eapply sim_local_body_post_mono, sim_body_frame_l'; [|done..].
+  simpl. intros r' n' es' σs' et' σt' (rf' & -> & ?). done.
+Qed.
 
 Lemma sim_body_frame_core fs ft n (r: resUR) es σs et σt Φ :
   r ⊨{n,fs,ft}
@@ -214,8 +261,7 @@ Lemma sim_body_frame_core fs ft n (r: resUR) es σs et σt Φ :
   r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ.
 Proof.
   intros HH. rewrite -(cmra_core_l r).
-  eapply sim_local_body_post_mono, sim_body_frame, HH.
-  intros r' n' rs' σs' rt' σt' [r'' [-> HΦ]]. done.
+  eapply sim_body_frame_l. done.
 Qed.
 
 Lemma sim_body_val_elim fs ft r n vs σs vt σt Φ :
@@ -234,3 +280,9 @@ Proof.
     - by apply result_tstep_stuck in STEP2. }
   subst σs' vs'. done.
 Qed.
+
+Lemma sim_body_viewshift r2 r1 fs ft n es σs et σt Φ :
+  r1 |==> r2 →
+  r2 ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ →
+  r1 ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ.
+Proof. by eapply viewshift_sim_local_body. Qed.
diff --git a/theories/sim/refl.v b/theories/sim/refl.v
index 1586f9c85f02142c724e102956876a61716e4784..19d112062d915287795eeb2276fa75794cadc3bf 100644
--- a/theories/sim/refl.v
+++ b/theories/sim/refl.v
@@ -1,5 +1,5 @@
 From stbor.lang Require Import lang subst_map.
-From stbor.sim Require Import refl_step simple tactics.
+From stbor.sim Require Import refl_step simple tactics viewshift.
 
 Set Default Proof Using "Type".
 
@@ -190,12 +190,13 @@ Proof.
   intros vs vt σs σt Hrel Hsubst1 Hsubst2. exists sem_steps.
   apply sim_body_init_call=>/=.
   set css := snc σs :: scs σs. set cst := snc σt :: scs σt. move=>Hstacks.
-  (* FIXME: viewshift to public call ID, use framing or something to get it to fun_post. *)
+  eapply (sim_body_viewshift (r ⋅ res_callState _ csPub)).
+  { eapply vs_call_empty_public. }
   eapply sim_local_body_post_mono with
     (Φ:=(λ r n vs' σs' vt' σt', sem_post css cst r n vs' σs'.(scs) vt' σt'.(scs))).
-  { intros r' n' rs css' rt cst' (-> & ? & ? & Hrrel).
+  { intros r' n' rs css' rt cst' (-> & Hcss & Hcst & Hrrel). simplify_eq.
     split.
-    - eexists. split. subst cst css. rewrite <-Hstacks. congruence.
+    - eexists. split; first by rewrite Hcst.
       admit. (* end_call_sat *)
     - done.
   }
diff --git a/theories/sim/simple.v b/theories/sim/simple.v
index 66d6b0596d55ebc0124e6c0eb930a096b0caa2a8..81d1b2e18df30fda79efeb985941ddda5aa27939 100644
--- a/theories/sim/simple.v
+++ b/theories/sim/simple.v
@@ -93,8 +93,16 @@ Proof.
   eapply sim_local_body_post_mono, Hold; done.
 Qed.
 
+Lemma sim_simple_viewshift r2 r1 fs ft n es css et cst Φ :
+  r1 |==> r2 →
+  r2 ⊨ˢ{n,fs,ft} (es, css) ≥ (et, cst) : Φ →
+  r1 ⊨ˢ{n,fs,ft} (es, css) ≥ (et, cst) : Φ.
+Proof.
+  intros Hvs Hold σs σt <-<-. eapply viewshift_sim_local_body, Hold; done.
+Qed.
+
 (** Simple proof for a function taking one argument. *)
-(* TODO: make the two call stacks the same. *)
+(* TODO: make the two call stacks the same? *)
 Lemma sim_fun_simple1 n (esf etf: function) :
   length (esf.(fun_args)) = 1%nat →
   length (etf.(fun_args)) = 1%nat →