WIP: fixing simpl

theories/opt/ex1.v

@@ -37,7 +37,7 @@ Proof.
   (* Write local *)
   rewrite (vrel_eq _ _ _ AREL).
   sim_apply sim_simple_write_local; [solve_sim..|].
-  intros arg ->. simpl.
+  intros sarg targ ??. simplify_eq.
   sim_apply sim_simple_let=>/=.
   apply: sim_simple_result.
   (* Retag local *)
@@ -88,8 +88,8 @@ Proof.
   sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
   { rewrite lookup_insert. done. }
   (* Finishing up. *)
-  eapply sim_body_viewshift.
-  { do 5 eapply viewshift_frame_r. eapply vs_call_empty_public. }
+  (* eapply sim_body_viewshift.
+  { do 5 eapply viewshift_frame_r. eapply vs_call_empty_public. } *)
   apply: sim_body_result=>Hval. do 2 (split; first done). split.
   - solve_res.
   - constructor; simpl; auto.

theories/sim/program.v

@@ -36,7 +36,8 @@ Proof.
     { eapply rrel_mono; [done|apply cmra_included_r|exact VRET]. }
     split; [|done].
     exists O. split; [by rewrite -STACKT|].
-    apply cmap_lookup_op_l_equiv_pub; [apply VALID|].
-    by rewrite /= lookup_singleton.
+    rewrite /end_call_sat /=.
+    apply cmap_lookup_op_l_equiv; [apply VALID|].
+    by rewrite /to_cmUR fmap_insert lookup_insert.
   - instantiate (1:=ε). rewrite right_id left_id. apply wsat_init_state.
 Qed.

theories/sim/refl.v

@@ -324,8 +324,8 @@ Theorem sim_mod_fun_refl f :
 Proof.
   intros Hwf. eapply (sim_fun_simple sem_steps); first done.
   intros fs ft r es et vs vt c Hlk Hrel Hsubst1 Hsubst2.
-  eapply sim_simple_viewshift.
-  { eapply viewshift_frame_l. eapply vs_call_empty_public. }
+  (* eapply sim_simple_viewshift.
+  { eapply viewshift_frame_l. eapply vs_call_empty_public. } *)
   eapply sim_simple_frame_r.
   destruct (subst_l_map _ _ _ _ _ _ _ (rrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
   { clear -Hrel. induction Hrel; eauto using Forall2. }

theories/sim/simple.v

@@ -143,7 +143,7 @@ Qed.
 
 (** * Simple proof for a function body. *)
 Definition fun_post_simple c (r: resUR) (n: nat) vs vt :=
-  res_callState c csPub ≼ r ∧ rrel r vs vt.
+  res_cs c ∅ ≼ r ∧ rrel r vs vt.
 
 Lemma sim_fun_simple n (esf etf: function) :
   length (esf.(fun_args)) = length (etf.(fun_args)) →
@@ -152,7 +152,7 @@ Lemma sim_fun_simple n (esf etf: function) :
     Forall2 (vrel rf) vls vlt →
     subst_l (esf.(fun_args)) (Val <$> vls) (esf.(fun_body)) = Some es →
     subst_l (etf.(fun_args)) (Val <$> vlt) (etf.(fun_body)) = Some et →
-    rf ⋅ res_callState c (csOwned ∅) ⊨ˢ{n,fs,ft} es ≥ et : fun_post_simple c) →
+    rf ⋅ res_cs c ∅ ⊨ˢ{n,fs,ft} es ≥ et : fun_post_simple c) →
   ⊨ᶠ esf ≥ etf.
 Proof.
   intros Hl HH fs ft Hlook rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
@@ -173,7 +173,7 @@ Lemma sim_fun_simple1 n (esf etf: function) :
     vrel rf vs vt →
     subst_l (esf.(fun_args)) [Val vs] (esf.(fun_body)) = Some es →
     subst_l (etf.(fun_args)) [Val vt] (etf.(fun_body)) = Some et →
-    rf ⋅ res_callState c (csOwned ∅) ⊨ˢ{n,fs,ft} es ≥ et : fun_post_simple c) →
+    rf ⋅ res_cs c ∅ ⊨ˢ{n,fs,ft} es ≥ et : fun_post_simple c) →
   ⊨ᶠ esf ≥ etf.
 Proof.
   intros Hls Hlt HH. eapply sim_fun_simple.
@@ -254,26 +254,26 @@ Qed.
 (** * Memory: local *)
 Lemma sim_simple_alloc_local fs ft r n T Φ :
   (∀ (l: loc) (tg: nat),
-    let r' := res_mapsto l (repeat ☠%S (tsize T)) tg in
+    let r' := res_loc l (repeat (☠%S,☠%S) (tsize T)) tg in
     Φ (r ⋅ r') n (PlaceR l (Tagged tg) T) (PlaceR l (Tagged tg) T)) →
   r ⊨ˢ{n,fs,ft} Alloc T ≥ Alloc T : Φ.
 Proof.
   intros HH σs σt. apply sim_body_alloc_local; eauto.
 Qed.
 
-Lemma sim_simple_write_local fs ft r r' n l tg ty v v' Φ :
+Lemma sim_simple_write_local fs ft r r' n l tg ty vs vt v' Φ :
   tsize ty = 1%nat →
-  r ≡ r' ⋅ res_mapsto l [v'] tg →
-  (∀ s, v = [s] → Φ (r' ⋅ res_mapsto l [s] tg) n (ValR [☠%S]) (ValR [☠%S])) →
+  r ≡ r' ⋅ res_loc l [v'] tg →
+  (∀ ss st, vs = [ss] → vt = [st] → Φ (r' ⋅ res_loc l [(ss,st)] tg) n (ValR [☠%S]) (ValR [☠%S])) →
   r ⊨ˢ{n,fs,ft}
-    (Place l (Tagged tg) ty <- #v) ≥ (Place l (Tagged tg) ty <- #v)
+    (Place l (Tagged tg) ty <- #vs) ≥ (Place l (Tagged tg) ty <- #vt)
   : Φ.
 Proof. intros Hty Hres HH σs σt. eapply sim_body_write_local_1; eauto. Qed.
 
-Lemma sim_simple_copy_local_l fs ft r r' n l tg ty s et Φ :
+Lemma sim_simple_copy_local_l fs ft r r' n l tg ty ss st et Φ :
   tsize ty = 1%nat →
-  r ≡ r' ⋅ res_mapsto l [s] tg →
-  (r ⊨ˢ{n,fs,ft} #[s] ≥ et : Φ) →
+  r ≡ r' ⋅ res_loc l [(ss, st)] tg →
+  (r ⊨ˢ{n,fs,ft} #[ss] ≥ et : Φ) →
   r ⊨ˢ{n,fs,ft}
     Copy (Place l (Tagged tg) ty) ≥ et
   : Φ.
@@ -282,10 +282,10 @@ Proof.
   eapply sim_body_copy_local_l; eauto.
 Qed.
 
-Lemma sim_simple_copy_local_r fs ft r r' n l tg ty s es Φ :
+Lemma sim_simple_copy_local_r fs ft r r' n l tg ty ss st es Φ :
   tsize ty = 1%nat →
-  r ≡ r' ⋅ res_mapsto l [s] tg →
-  (r ⊨ˢ{n,fs,ft} es ≥ #[s] : Φ) →
+  r ≡ r' ⋅ res_loc l [(ss,st)] tg →
+  (r ⊨ˢ{n,fs,ft} es ≥ #[st] : Φ) →
   r ⊨ˢ{S n,fs,ft}
     es ≥ Copy (Place l (Tagged tg) ty)
   : Φ.
@@ -294,10 +294,10 @@ Proof.
   eapply sim_body_copy_local_r; eauto.
 Qed.
 
-Lemma sim_simple_copy_local fs ft r r' n l tg ty s Φ :
+Lemma sim_simple_copy_local fs ft r r' n l tg ty ss st Φ :
   tsize ty = 1%nat →
-  r ≡ r' ⋅ res_mapsto l [s] tg →
-  (r ⊨ˢ{n,fs,ft} #[s] ≥ #[s] : Φ) →
+  r ≡ r' ⋅ res_loc l [(ss,st)] tg →
+  (r ⊨ˢ{n,fs,ft} #[ss] ≥ #[st] : Φ) →
   r ⊨ˢ{S n,fs,ft}
     Copy (Place l (Tagged tg) ty) ≥ Copy (Place l (Tagged tg) ty)
   : Φ.
@@ -309,7 +309,7 @@ Qed.
 
 Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty Φ :
   (0 < tsize ty)%nat →
-  r ≡ r' ⋅ res_mapsto l [s] tg →
+  r ≡ r' ⋅ res_loc l [(s,s)] tg →
   arel rs s' s →
   r' ≡ r'' ⋅ rs →
   (∀ l_inner tg_inner hplt,
@@ -321,7 +321,7 @@ Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty Φ :
     end → *)
     let tk := tkUnique in
     is_Some (hplt !! l_inner) →
-    Φ (r'' ⋅ rs ⋅ res_mapsto l [s_new] tg ⋅ res_tag tg_inner tk hplt) n (ValR [☠%S]) (ValR [☠%S])) →
+    Φ (r'' ⋅ rs ⋅ res_loc l [(s_new,s_new)] tg ⋅ res_tag tg_inner tk hplt) n (ValR [☠%S]) (ValR [☠%S])) →
   r ⊨ˢ{n,fs,ft}
     Retag (Place l (Tagged tg) (Reference (RefPtr Mutable) ty)) Default
   ≥