fix step_over_call

theories/opt/ex1.v

@@ -49,7 +49,7 @@ Proof.
   move=>l_i tg_i hplt /= Hl_i.
   (* Call *)
   sim_apply sim_simple_let_val=>/=.
-  sim_apply (sim_simple_call 10 [] [] ε). constructor. solve_res.
+  sim_apply (sim_simple_call 10 [] [] ε). admit. constructor. solve_res.
   intros rf frs frt FREL.
   apply sim_simple_val.
 

theories/sim/body.v

@@ -24,7 +24,7 @@ Proof.
     pclearbot. right. eapply CIH; eauto.
   - econstructor 2; eauto.
     intros.
-    destruct (CONT _ _ _ σs' σt' VRET STACK) as [idx' SIM'].
+    destruct (CONT _ _ _ σs' σt' VRET WSAT1 STACK) as [idx' SIM'].
     exists idx'. pclearbot.
     right. eapply CIH; eauto.
 Qed.
@@ -51,9 +51,10 @@ Proof.
     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). }
+    { instantiate (1:= rf ⋅ rc). by rewrite -cmra_assoc (cmra_assoc r_f). }
     intros.
-    specialize (CONT _ _ _ σs' σt' VRET STACK) as [idx' SIM'].
+    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.
 
@@ -155,8 +156,8 @@ Proof.
         { pclearbot. left. eapply paco7_mon_bot; eauto. }
       + eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
             Ks1 Kt1 fid vl_tgt _ _ _ _ CALLTGT); eauto; [by etrans|].
-        intros r4 vs4 vt4 σs4 σt4 VREL4 STACK4.
-        destruct (CONT _ _ _ σs4 σt4 VREL4 STACK4) as [idx4 CONT4].
+        intros r4 vs4 vt4 σs4 σt4 VREL4 WSAT4 STACK4.
+        destruct (CONT _ _ _ σs4 σt4 VREL4 WSAT4 STACK4) as [idx4 CONT4].
         exists idx4. pclearbot. left.  eapply paco7_mon_bot; eauto.
     - (* et makes a step *)
       constructor 1. intros.
@@ -172,8 +173,8 @@ Proof.
     eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
             (Ks1 ++ Ks) (Kt1 ++ Kt) fid vl_tgt); [by rewrite CALLTGT fill_app|..];
             eauto; [rewrite fill_app; by apply fill_tstep_rtc|].
-    intros r' vs' vt' σs' σt' VREL' STACK'.
-    destruct (CONT _ _ _ σs' σt' VREL' STACK') as [idx' CONT2]. clear CONT.
+    intros r' vs' vt' σs' σt' VREL' WSAT' STACK'.
+    destruct (CONT _ _ _ σs' σt' VREL' WSAT' STACK') as [idx' CONT2]. clear CONT.
     exists idx'. rewrite 2!fill_app.
     pclearbot. right. by apply CIH. }
 Qed.

theories/sim/local.v

@@ -49,6 +49,7 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
              (* For any new resource r' that supports the returned values are
                 related w.r.t. (r ⋅ r' ⋅ r_f) *)
              (VRET: vrel r' v_src v_tgt)
+             (WSAT: wsat (r_f ⋅ (rc ⋅ r')) σs' σt')
              (STACK: σt.(scs) = σt'.(scs)),
         ∃ idx', sim_local_body (rc ⋅ r') idx'
                                (fill Ks (Val v_src)) σs'
@@ -106,8 +107,8 @@ Proof.
     specialize (STEP _ _ STEPT) as (es' & σs' & r' & idx' & STEP' & WSAT' & SIM').
     exists es', σs', r', idx'. do 2 (split; [done|]).
     pclearbot. right. eapply CIH; eauto.
-  - econstructor 2; eauto. intros.
-    destruct (CONT _ _ _ σs' σt' VRET STACK) as [idx' SIM'].
+  - econstructor 2; eauto. intros r' vs vt σs' σt' VRET WSAT1 STACK.
+    destruct (CONT _ _ _ σs' σt' VRET WSAT1 STACK) as [idx' SIM'].
     exists idx'. pclearbot. right. eapply CIH; eauto.
 Qed.
 
@@ -131,8 +132,8 @@ Definition sim_local_fun
                           (fun_post esat σt.(scs)).
 
 Definition sim_local_funs (esat: A → state → state → Prop) : Prop :=
-  ∀ name fn_tgt, fnt !! name = Some fn_tgt → ∃ fn_src,
-    fns !! name = Some fn_src ∧
+  ∀ name fn_src, fns !! name = Some fn_src → ∃ fn_tgt,
+    fnt !! name = Some fn_tgt ∧
     length fn_src.(fun_b) = length fn_tgt.(fun_b) ∧
     sim_local_fun esat fn_src fn_tgt.
 

theories/sim/local_adequacy.v

@@ -203,19 +203,26 @@ Proof.
       { eapply list_Forall_to_value. eauto. }
       { exact x2. }
       eauto. i. des. subst.
-      destruct (FUNS _ _ x3) as ([xls ebs HCss] & Eqfs & Eql & SIMf).
-      destruct (subst_l_is_Some xls (Val <$> vl_src) ebs) as [ess Eqss].
-      { rewrite fmap_length (Forall2_length _ _ _ VREL).
-        rewrite Eql (subst_l_is_Some_length _ _ _ _ x4) fmap_length //. }
+      have NT: never_stuck fns (Call #[ScFnPtr fid] (Val <$> vl_src)) σ1_src.
+      { apply (never_stuck_fill_inv _ Ks).
+        eapply never_stuck_tstep_rtc; eauto.
+        by apply (never_stuck_fill_inv _ K_src0). }
+      edestruct NT as [[]|[e2 [σ2 RED]]]; [constructor 1|done|].
+      apply tstep_call_inv in RED; last first.
+      { apply list_Forall_to_value. eauto. }
+      destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ?). subst e2 σ2.
+      destruct (FUNS _ _ Eqfs) as ([xlt2 ebt2 HCt2] & Eqft2 & Eql2 & SIMf).
+      rewrite Eqft2 in x3. simplify_eq.
       specialize (SIMf _ _ _ _ _ σ1_src σ_tgt VREL Eqss x4) as [idx2 SIMf].
       esplits.
       * left. eapply tc_rtc_l.
         { apply fill_tstep_rtc. eauto. }
         { econs. rewrite -fill_app. eapply (head_step_fill_tstep).
-          econs; econs; eauto. apply list_Forall_to_value. eauto. }
+          econs. eapply (CallBS _ _ _ _ xls ebs); eauto.
+          apply list_Forall_to_value. eauto. }
       * right. apply CIH. econs.
         { econs 2; eauto. i. instantiate (1 := mk_frame _ _ _ _). ss.
-          destruct (CONT r' v_src v_tgt σ_src' σ_tgt' VRET).
+          destruct (CONT r' v_src v_tgt σ_src' σ_tgt' VRET WSAT').
           { rewrite CIDS. eauto. }
           pclearbot. esplits; eauto.
         }

theories/sim/program.v

@@ -12,13 +12,16 @@ Lemma sim_prog_sim_classical
                              ~ terminal e' /\
                              ~ reducible prog_src e' σ'}
       (FUNS: sim_local_funs wsat vrel prog_src prog_tgt end_call_sat)
-      (MAINT: ∃ ebt HCt, prog_tgt !! "main" = Some (@FunV [] ebt HCt))
+      (MAINT: ∃ ebs HCs, prog_src !! "main" = Some (@FunV [] ebs HCs))
   : behave_prog prog_tgt <1= behave_prog prog_src.
 Proof.
-  destruct MAINT as (ebt & HCt & Eqt).
-  destruct (FUNS _ _ Eqt) as ([xls ebs HCs] & Eqs & Eql & SIMf).
+  destruct MAINT as (ebs & HCs & Eqs).
+  destruct (FUNS _ _ Eqs) as ([xlt ebt HCt] & Eqt & Eql & SIMf).
+  simpl in Eql. symmetry in Eql.
   apply nil_length_inv in Eql. simplify_eq/=.
-  specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM]; [simpl; done..|].
+  specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM];
+    [simpl; done..|].
+
   unfold behave_prog.
   eapply (adequacy_classical _ _ idx); [apply NSD| |by apply wf_init_state..].
   eapply sim_local_conf_sim; eauto.
@@ -40,7 +43,8 @@ Proof.
     have HL: (init_res ⋅ r').(rcm) !! 0%nat ≡ Some (to_callStateR csPub).
     { apply cmap_lookup_op_l_equiv_pub; [apply VALID|].
       by rewrite /= lookup_singleton. }
-    split. { destruct ((init_res ⋅ r').(rcm) !! 0%nat). by eexists. by inversion HL. }
+    split.
+    { destruct ((init_res ⋅ r').(rcm) !! 0%nat). by eexists. by inversion HL. }
     intros r_f VALIDf T HL2. exfalso.
     move : HL2. rewrite lookup_op HL. apply callStateR_exclusive_2.
   - instantiate (1:=ε). rewrite right_id left_id. apply wsat_init_state.

theories/sim/refl_step.v

@@ -1199,7 +1199,7 @@ Qed.
 Lemma sim_body_step_over_call fs ft
   rc rv n fid vls vlt σs σt Φ
   (VREL: Forall2 (vrel rv) vls vlt)
-  :
+  (FUNS: sim_local_funs wsat vrel fs ft end_call_sat) :
   (∀ r' vs vt σs' σt' (VRET: vrel r' vs vt)
     (STACKS: σs.(scs) = σs'.(scs))
     (STACKT: σt.(scs) = σt'.(scs)), ∃ n',
@@ -1207,16 +1207,28 @@ Lemma sim_body_step_over_call fs ft
   rc ⋅ rv ⊨{n,fs,ft}
     (Call #[ScFnPtr fid] (Val <$> vls), σs) ≥ (Call #[ScFnPtr fid] (Val <$> vlt), σt) : Φ.
 Proof.
-  (* intros CONT. pfold. intros NT r_f WSAT. split; [|done|].
-  { right. exists (EndCall (InitCall et')), σt.
+  intros CONT. pfold. intros NT r_f WSAT.
+  edestruct NT as [[]|[e2 [σ2 RED]]]; [constructor 1|done|].
+  apply tstep_call_inv in RED; last first.
+  { apply list_Forall_to_value. eauto. }
+  destruct RED as (xls & ebs & HCs & ebss & Eqfs & Eqss & ? & ?). subst e2 σ2.
+  destruct (FUNS _ _ Eqfs) as ([xlt ebt HCt] & Eqft & Eql & SIMf).
+  simpl in Eql.
+  destruct (subst_l_is_Some xlt (Val <$> vlt) ebt) as [est Eqst].
+  { rewrite fmap_length -(Forall2_length _ _ _ VREL) -Eql
+            (subst_l_is_Some_length _ _ _ _ Eqss) fmap_length //. }
+  split; [|done|].
+  { right. exists (EndCall (InitCall est)), σt.
      eapply (head_step_fill_tstep _ []). econstructor. econstructor; try done.
      apply list_Forall_to_value. eauto. }
   eapply (sim_local_body_step_over_call _ _ _ _ _ _ _ _ _ _ _ _ _
             [] [] fid vlt vls); eauto; [done|].
-  intros r' ? ? σs' σt' VR STACK. simplify_eq.
-  destruct (CONT _ _ _ σs' σt' VR STACK) as [n' ?].
-  exists n'. by left. *)
-Admitted.
+  intros r' ? ? σs' σt' VR WSAT' STACK.
+  destruct (CONT _ _ _ σs' σt' VR) as [n' ?]; [|done|exists n'; by left].
+  destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (?&?&?Eqcss&?).
+  destruct WSAT' as (?&?&?&?&?&SREL'&?). destruct SREL' as (?&?&?Eqcss'&?).
+  by rewrite Eqcss' Eqcss.
+Qed.
 
 (** Let *)
 Lemma sim_body_let fs ft r n x es1 es2 et1 et2 σs σt Φ :

theories/sim/simple.v

@@ -108,6 +108,7 @@ Qed.
 (* [Val <$> _] in the goal makes this not work with [apply], but
 we'd need tactic support for anything better. *)
 Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
+  sim_local_funs wsat vrel fs ft end_call_sat →
   Forall2 (vrel rv) vls vlt →
   r ≡ r' ⋅ rv →
   (∀ rret vs vt, vrel rret vs vt →
@@ -115,12 +116,13 @@ Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
   r ⊨ˢ{n,fs,ft}
     (Call #[ScFnPtr fid] (Val <$> vls), css) ≥ (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.
 Proof.
-  intros Hrel Hres HH σs σt <-<-.
+  intros Hfns Hrel Hres HH σs σt <-<-.
   eapply sim_body_res_proper; last apply: sim_body_step_over_call.
   - symmetry. exact: Hres.
   - done.
+  - done.
   - intros. exists n'. eapply sim_body_res_proper; last apply: HH; try done.
-Admitted.
+Qed.
 
 (** * Memory *)
 Lemma sim_simple_alloc_local fs ft r n T css cst Φ :