fix index for values

theories/lang/steps_inversion.v

@@ -108,6 +108,14 @@ Proof.
     by eapply fill_not_result, (result_head_stuck fns).
 Qed.
 
+Lemma result_tstep_rtc e σ e' σ' :
+  terminal e → (e, σ) ~{fns}~>* (e', σ') → e' = e ∧ σ' = σ.
+Proof.
+  intros [v Eqe].
+  inversion 1 as [|x [] z STEP]; [done|].
+  apply result_tstep_stuck in STEP. by rewrite Eqe in STEP.
+Qed.
+
 Lemma tstep_reducible_fill_inv K e σ :
   to_result e = None →
   reducible fns (fill K e) σ → reducible fns e σ.

theories/sim/body.v

@@ -3,16 +3,106 @@ From stbor.sim Require Export instance.
 
 Set Default Proof Using "Type".
 
+
+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 Φ :
+  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') : Φ) →
+  r ⊨{n,fs,ft} (fill Ks es, σs) ≥ (fill Kt et, σt) : Φ.
+Proof.
+  revert r n Ks Kt es et σs σt Φ. pcofix CIH.
+  intros r1 n Ks Kt es et σs σt Φ SIM. pfold. punfold SIM. intros NT ??.
+  have NT2 := never_stuck_fill_inv _ _ _ _ NT.
+  destruct (SIM NT2 _ WSAT) as [NTT TM ST]. clear SIM. split.
+  { destruct NTT as [[vt Eqvt]|RED].
+    - rewrite -(of_to_result _ _ Eqvt).
+      destruct (TM _ Eqvt) as (vs' & σs' & r' & SS' & WSAT' & CONT).
+      have STEPK: (fill (Λ:=bor_ectxi_lang fs) Ks es, σs)
+                ~{fs}~>* (fill (Λ:=bor_ectxi_lang fs) Ks vs', σs').
+      { by apply fill_tstep_rtc. }
+      have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NT.
+      punfold CONT.
+      destruct (CONT NT3 _ WSAT') as [NTT' _ _]. done.
+    - right. by eapply tstep_reducible_fill. }
+  { (* Kt[et] is a value *)
+    clear ST. intros vt Eqvt.
+    destruct (fill_result _ Kt et) as [Tt ?]; [by eexists|].
+    subst Kt. simpl in *.
+    destruct (TM _ Eqvt) as (vs' & σs' & r' & SS' & WSAT' & CONT).
+    punfold CONT.
+    have STEPK: (fill (Λ:=bor_ectxi_lang fs) Ks es, σs)
+                ~{fs}~>* (fill (Λ:=bor_ectxi_lang fs) Ks vs', σs').
+    { by apply (fill_tstep_rtc fs Ks es). }
+    have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NT.
+    destruct (CONT NT3 _ WSAT') as [NTT' TM' ST'].
+    destruct (TM' vt) as (vs2 & σs2 & r2 & SS2 & ?);
+      [by apply to_of_result|].
+    exists vs2, σs2, r2. split; [|done].
+    etrans; [|apply SS2]. by apply fill_tstep_rtc. }
+  (* Kt[et] makes a step *)
+  inversion_clear ST as [|Ks1 Kt1].
+  { (* step into Kt[et] *)
+   destruct (to_result et) as [vt|] eqn:Eqvt.
+    - (* et is value *)
+      have ? : et = of_result vt. { symmetry. by apply of_to_result. }
+      subst et. clear Eqvt.
+      destruct (TM _ eq_refl) as (vs' & σs' & r' & SS' & WSAT' & CONT').
+      clear TM.
+      have STEPK: (fill (Λ:=bor_ectxi_lang fs) Ks es, σs)
+                  ~{fs}~>* (fill (Λ:=bor_ectxi_lang fs) Ks vs', σs').
+      { by apply (fill_tstep_rtc fs Ks es). }
+      have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NT.
+      punfold CONT'.
+      destruct (CONT' NT3 _ WSAT') as [NTT' TM' ST']. clear CONT' WSAT' STEP.
+      inversion ST' as [|Ks1 Kt1].
+      + constructor 1. intros.
+        destruct (STEP _ _ STEPT) as (es2 & σs2 & r2 & idx2 & SS2 & WSAT2 & CONT2).
+        exists es2, σs2, r2, idx2. split; last split; [|done|].
+        { clear -SS2 SS' STEPK.
+          destruct SS2 as [|[]].
+          - left. eapply tc_rtc_l; eauto.
+          - simplify_eq. inversion STEPK; simplify_eq.
+            + by right.
+            + left. eapply tc_rtc_r; [by apply tc_once|eauto]. }
+        { 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 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.
+      destruct (fill_tstep_inv _ _ _ _ _ _ Eqvt STEPT) as [et2 [? STEP2]].
+      subst et'.
+      destruct (STEP _ _ STEP2) as (es' & σs' & r' & idx' & SS' & WSAT' & CONT').
+      exists (fill Ks es'), σs', r', idx'. split; last split; [|done|].
+      + clear -SS'. destruct SS' as [|[]].
+        * left. by apply fill_tstep_tc.
+        * simplify_eq. right. split; [|done]. lia.
+      + pclearbot. right. by apply CIH. }
+  { (* Kt[et] has a call, and we step over the call *)
+    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' 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.
+
+
 Lemma sim_body_result fs ft r n es et σs σt Φ :
   (✓ r → Φ r n es σs et σt : Prop) →
-  r ⊨{S n,fs,ft} (of_result es, σs) ≥ (of_result et, σt) : Φ.
+  r ⊨{n,fs,ft} (of_result es, σs) ≥ (of_result et, σt) : Φ.
 Proof.
   intros POST. pfold.  split; last first.
   { constructor 1. intros vt' ? STEPT'. exfalso.
     apply result_tstep_stuck in STEPT'. by rewrite to_of_result in STEPT'. }
   { move => ? /= Eqvt'. symmetry in Eqvt'. simplify_eq.
-    exists es, σs, r, n. split; last split.
-    - right. split; [lia|]. eauto.
+    exists es, σs, r. split; last split.
+    - constructor 1.
     - eauto.
     - rewrite to_of_result in Eqvt'. simplify_eq.
       apply POST. by destruct WSAT as (?&?&?%cmra_valid_op_r &?). }
@@ -31,7 +121,7 @@ Proof.
   specialize (SIM NT r_f WSAT) as [NOTS TE SIM].
   constructor; [done|..].
   { intros.
-    destruct (TE _ TERM) as (vs' & σs' & r'' & idx' & STEP' & WSAT' & HΦ).
+    destruct (TE _ TERM) as (vs' & σs' & r'' & STEP' & WSAT' & HΦ).
     naive_solver. }
   inversion SIM.
   - left. intros.
@@ -57,8 +147,8 @@ Proof.
   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 & idx' & STEP' & WSAT' & POST).
-    exists vs', σs', (rf ⋅ r2), idx'.
+  { 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.
@@ -83,114 +173,16 @@ Proof. intros. eapply sim_body_frame'; eauto. Qed.
 Lemma sim_body_val_elim fs ft r n vs σs vt σt Φ :
   r ⊨{n,fs,ft} ((Val vs), σs) ≥ ((Val vt), σt) : Φ →
   ∀ r_f (WSAT: wsat (r_f ⋅ r) σs σt),
-  ∃ r' idx', Φ r' idx' (ValR vs) σs (ValR vt) σt ∧ wsat (r_f ⋅ r') σs σt.
+  ∃ r', Φ r' n (ValR vs) σs (ValR vt) σt ∧ wsat (r_f ⋅ r') σs σt.
 Proof.
   intros SIM r_f WSAT. punfold SIM.
   specialize (SIM (never_stuck_val fs vs σs) _ WSAT) as [ST TE STEPSS].
   specialize (TE (ValR vt) eq_refl)
-    as (vs' & σs' & r' & idx' & STEP' & WSAT' & POST).
-  exists r', idx'.
+    as (vs' & σs' & r' & STEP' & WSAT' & POST).
+  exists r'.
   assert (σs' = σs ∧ vs' = vs) as [].
-  { destruct STEP' as [STEP'|[Eq1 Eq2]]; [|simplify_eq].
-    - by apply result_tstep_tc_stuck in STEP'.
-    - split; [done|].
-      have Eq := to_of_result vs'. rewrite -H /= in Eq. by simplify_eq. }
+  { inversion STEP' as [x y Eq|x [] z STEP2] ; subst; simplify_eq.
+    - have Eq2 := to_of_result vs'. rewrite -Eq /= in Eq2. by simplify_eq.
+    - by apply result_tstep_stuck in STEP2. }
   subst σs' vs'. 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 Φ :
-  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') : Φ) →
-  r ⊨{n,fs,ft} (fill Ks es, σs) ≥ (fill Kt et, σt) : Φ.
-Proof.
-  revert r n Ks Kt es et σs σt Φ. pcofix CIH.
-  intros r1 n Ks Kt es et σs σt Φ SIM. pfold. punfold SIM. intros NT ??.
-  have NT2 := never_stuck_fill_inv _ _ _ _ NT.
-  destruct (SIM NT2 _ WSAT) as [NTT TM ST]. clear SIM. split.
-  { destruct NTT as [[vt Eqvt]|RED].
-    - rewrite -(of_to_result _ _ Eqvt).
-      destruct (TM _ Eqvt) as (vs' & σs' & r' & idx' & SS' & WSAT' & CONT).
-      have STEPK: (fill (Λ:=bor_ectxi_lang fs) Ks es, σs)
-                ~{fs}~>* (fill (Λ:=bor_ectxi_lang fs) Ks vs', σs').
-      { apply fill_tstep_rtc. destruct SS' as [|[? Eq]].
-        by apply tc_rtc. clear -Eq. by simplify_eq. }
-      have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NT.
-      punfold CONT.
-      destruct (CONT NT3 _ WSAT') as [NTT' _ _]. done.
-    - right. by eapply tstep_reducible_fill. }
-  { (* Kt[et] is a value *)
-    clear ST. intros vt Eqvt.
-    destruct (fill_result _ Kt et) as [Tt ?]; [by eexists|].
-    subst Kt. simpl in *.
-    destruct (TM _ Eqvt) as (vs' & σs' & r' & idx' & SS' & WSAT' & CONT).
-    punfold CONT.
-    have STEPK: (fill (Λ:=bor_ectxi_lang fs) Ks es, σs)
-                ~{fs}~>* (fill (Λ:=bor_ectxi_lang fs) Ks vs', σs').
-    { apply (fill_tstep_rtc fs Ks es). destruct SS' as [|[? Eq]].
-      by apply tc_rtc. clear -Eq. by simplify_eq. }
-    have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NT.
-    destruct (CONT NT3 _ WSAT') as [NTT' TM' ST'].
-    destruct (TM' vt) as (vs2 & σs2 & r2 & idx2 & SS2 & ?);
-      [by apply to_of_result|].
-    exists vs2, σs2, r2, idx2. split; [|done].
-    destruct SS2 as [|[Lt Eq]].
-    - left. eapply tc_rtc_l; eauto.
-    - clear -SS' Eq Lt.
-      inversion Eq as [Eq1]. clear Eq. subst.
-      destruct SS' as [SS'|[? SS']].
-      + left. by apply fill_tstep_tc.
-      + simplify_eq. right. split; [|done]. lia.
-  }
-  (* Kt[et] makes a step *)
-  inversion_clear ST as [|Ks1 Kt1].
-  { (* step into Kt[et] *)
-   destruct (to_result et) as [vt|] eqn:Eqvt.
-    - (* et is value *)
-      have ? : et = of_result vt. { symmetry. by apply of_to_result. }
-      subst et. clear Eqvt.
-      destruct (TM _ eq_refl) as (vs' & σs' & r' & idx' & SS' & WSAT' & CONT').
-      clear TM.
-      have STEPK: (fill (Λ:=bor_ectxi_lang fs) Ks es, σs)
-                  ~{fs}~>* (fill (Λ:=bor_ectxi_lang fs) Ks vs', σs').
-      { apply (fill_tstep_rtc fs Ks es). destruct SS' as [|[? Eq]].
-        by apply tc_rtc. clear -Eq. by simplify_eq. }
-      have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NT.
-      punfold CONT'.
-      destruct (CONT' NT3 _ WSAT') as [NTT' TM' ST']. clear CONT' WSAT' STEP.
-      inversion ST' as [|Ks1 Kt1].
-      + constructor 1. intros.
-        destruct (STEP _ _ STEPT) as (es2 & σs2 & r2 & idx2 & SS2 & WSAT2 & CONT2).
-        exists es2, σs2, r2, idx2. split; last split; [|done|].
-        { clear -SS2 SS' STEPK.
-          destruct SS2 as [|[]]; [|destruct SS' as [|[]]].
-          - left. eapply tc_rtc_l; eauto.
-          - simplify_eq. left. by apply fill_tstep_tc.
-          - simplify_eq. right. split; [|done]. lia. }
-        { 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 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.
-      destruct (fill_tstep_inv _ _ _ _ _ _ Eqvt STEPT) as [et2 [? STEP2]].
-      subst et'.
-      destruct (STEP _ _ STEP2) as (es' & σs' & r' & idx' & SS' & WSAT' & CONT').
-      exists (fill Ks es'), σs', r', idx'. split; last split; [|done|].
-      + clear -SS'. destruct SS' as [|[]].
-        * left. by apply fill_tstep_tc.
-        * simplify_eq. right. split; [|done]. lia.
-      + pclearbot. right. by apply CIH. }
-  { (* Kt[et] has a call, and we step over the call *)
-    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' 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/global.v

@@ -38,8 +38,8 @@ Record sim_base (sim: SIM_CONFIG) (idx1: nat) (eσ1_src eσ1_tgt: expr * state)
     (terminal eσ1_tgt.1 ∨ reducible fnt eσ1_tgt.1 eσ1_tgt.2) ;
   (* (2) If [eσ1_tgt] is terminal, then [eσ1_src] terminates with some steps. *)
   sim_terminal :
-    terminal eσ1_tgt.1 → ∃ idx2 eσ2_src,
-      sflib.__guard__ (eσ1_src ~{fns}~>+ eσ2_src ∨ ((idx2 < idx1)%nat ∧ eσ1_src = eσ2_src)) ∧
+    terminal eσ1_tgt.1 → ∃ eσ2_src,
+      eσ1_src ~{fns}~>* eσ2_src ∧
       terminal eσ2_src.1 ∧ sim_expr_terminal eσ2_src.1 eσ1_tgt.1 ;
   (* (3) If [eσ1_tgt] steps to [eσ2_tgt] with 1 step,
        then exists [eσ2_src] s.t. [eσ1_src] steps to [eσ2_src] with * step. *)

theories/sim/global_adequacy.v

@@ -85,12 +85,9 @@ Proof.
       * unfold reducible in ST. des. eapply NS.
         destruct x. eauto.
     + clear sim_stuck. exploit sim_terminal; eauto. i. des.
-      pfold. econs.
-      * instantiate (1 := eσ2_src). unguardH x0. des.
-        { apply tc_rtc. eauto. }
-        { subst. reflexivity. }
-      * unfold terminal in *. des.
-        econs 2. unfold term. erewrite x2; eauto.
+      pfold. econs; eauto.
+      unfold terminal in *. des.
+      econs 2. unfold term. erewrite x2; eauto.
     + pclearbot. exploit sim_step; eauto. i. revert sim_stuck.
       rename s' into conf'_tgt.
       have WFT': Wf conf'_tgt.2 by eapply tstep_wf; eauto.

theories/sim/local.v

@@ -63,11 +63,9 @@ Record sim_local_body_base (r_f: A) (sim_local_body : SIM)
     (* if tgt is terminal *)
     ∀ vt (TERM: to_result et = Some vt),
       (* then src can get terminal *)
-      ∃ vs' σs' r' idx',
-        sflib.__guard__ ((es, σs) ~{fs}~>+ (of_result vs', σs') ∨
-                         ((idx' < idx)%nat ∧ (es, σs) = (of_result vs', σs'))) ∧
+      ∃ vs' σs' r', (es, σs) ~{fs}~>* (of_result vs', σs') ∧
         (* and re-establish wsat *)
-        wsat (r_f ⋅ r') σs' σt ∧ Φ r' idx' vs' σs' vt σt ;
+        wsat (r_f ⋅ r') σs' σt ∧ Φ r' idx vs' σs' vt σt ;
   sim_local_body_step :
       _sim_local_body_step r_f sim_local_body r idx es σs et σt Φ
 }.
@@ -100,7 +98,7 @@ Proof.
   intros NT r_f WSAT. specialize (SIM NT r_f WSAT) as [NOTS TE SIM].
   constructor; [done|..].
   { intros.
-    destruct (TE _ TERM) as (vs' & σs' & r' & idx' & STEP' & WSAT' & HΦ).
+    destruct (TE _ TERM) as (vs' & σs' & r' & STEP' & WSAT' & HΦ).
     naive_solver. }
   inversion SIM.
   - left. intros.
@@ -165,7 +163,7 @@ Proof.
   specialize (SIM NT r_f WSAT2) as [NOTS TE SIM].
   constructor; [done|..].
   { intros.
-    destruct (TE _ TERM) as (vs' & σs' & r' & idx' & STEP' & WSAT' & HΦ).
+    destruct (TE _ TERM) as (vs' & σs' & r' & STEP' & WSAT' & HΦ).
     naive_solver. }
   inversion SIM.
   - left. intros.

theories/sim/local_adequacy.v

@@ -94,11 +94,10 @@ Proof.
     destruct sim_local_body_stuck as [vt Eqvt].
     rewrite -(of_to_result _ _ Eqvt).
     destruct (sim_local_body_terminal _ Eqvt)
-      as (vs' & σs' & r' & idx' & SS' & WSAT' & (c & CALLIDS & ESAT') & VREL).
+      as (vs' & σs' & r' & SS' & WSAT' & (c & CALLIDS & ESAT') & VREL).
     have STEPK: (fill (Λ:=bor_ectxi_lang fns) K_src0 e_src0, σ_src)
               ~{fns}~>* (fill (Λ:=bor_ectxi_lang fns) K_src0 vs', σs').
-    { apply fill_tstep_rtc. destruct SS' as [|[? Eq]].
-      by apply tc_rtc. clear -Eq. simplify_eq. constructor. }
+    { by apply fill_tstep_rtc. }
     have NT3:= never_stuck_tstep_rtc _ _ _ _ _ STEPK NEVER_STUCK.
     clear -STEPK NT3 FRAMES WSAT' VREL.
     inversion FRAMES. { left. rewrite to_of_result. by eexists. }
@@ -141,7 +140,7 @@ Proof.
             σs2 = mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc) ∧
             σt2 = mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc) ∧
             r2 = r'.
-      have SIMEND : r' ⊨{idx',fns,fnt} (EndCall vs1, σs) ≥ (EndCall vt1, σt) : Φ.
+      have SIMEND : r' ⊨{idx,fns,fnt} (EndCall vs1, σs) ≥ (EndCall vt1, σt) : Φ.
       { apply sim_body_end_call; auto; [naive_solver|].
         clear -VR. intros. rewrite /Φ. simpl. split; last naive_solver.
         by eexists _, _. }
@@ -154,8 +153,7 @@ Proof.
                         (EndCallCtx :: K_src frame0 ++ K_f_src) e_src0, σ_src)
             ~{fns}~>* (fill (Λ:= bor_ectxi_lang fns)
                         (EndCallCtx :: K_src frame0 ++ K_f_src) vs1, σs).
-      { apply fill_tstep_rtc. destruct x as [|[? Eq]].
-        by apply tc_rtc. clear -Eq. simplify_eq. constructor. }
+      { by apply fill_tstep_rtc. }
       have NT3 := never_stuck_tstep_rtc _ _ _ _ _ STEPK NEVER_STUCK.
       rewrite /= in NT3.
       have NT4 := never_stuck_fill_inv _ _ _ _ NT3.
@@ -172,8 +170,7 @@ Proof.
       intros [idx3 SIMFR]. rename σ2_tgt into σt2.
       do 2 eexists. split.
       - left. apply fill_tstep_tc. eapply tc_rtc_l; [|apply STEPS].
-        apply (fill_tstep_rtc _ [EndCallCtx]).
-        clear -x. destruct x as [|[]]. by apply tc_rtc. simplify_eq. constructor.
+        by apply (fill_tstep_rtc _ [EndCallCtx]).
 
       - right. apply CIH. econs; eauto.
         + rewrite fill_app. eauto.

theories/sim/refl_step.v

@@ -35,7 +35,7 @@ Proof.
   have STEPS: (Alloc T, σs) ~{fs}~> (Place l t T, σs').
   { subst l σs' t. rewrite Eqlst -Eqnp.
     eapply (head_step_fill_tstep _ []),  alloc_head_step. }
-  eexists _, σs', (r ⋅ r'), (S n). split; last split.
+  eexists _, σs', (r ⋅ r'), n. split; last split.
   { left. by apply tc_once. }
   { have HLF : ∀ i, (i < tsize T)%nat → (r_f ⋅ r).(rlm) !! (l +ₗ i) = None.
     { intros i Lti.
@@ -366,7 +366,7 @@ Proof.
     have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
     admit.
   }
-  exists (Val vs), σs', (r ⋅ (core (r_f ⋅ r))), (S n). split; last split.
+  exists (Val vs), σs', (r ⋅ (core (r_f ⋅ r))), n. split; last split.
   { left. by constructor 1. }
   { rewrite cmra_assoc -CORE.
     split; last split; last split; last split; last split; last split.
@@ -549,7 +549,7 @@ Proof.
     rewrite EQL in EqD. rewrite -Eqnp in IN.
     eapply (head_step_fill_tstep _ []), write_head_step'; eauto. }
 
-  exists (#[☠])%V, σs', (r' ⋅ res_mapsto l 1 s (init_stack (Tagged tg))), (S n).
+  exists (#[☠])%V, σs', (r' ⋅ res_mapsto l 1 s (init_stack (Tagged tg))), n.
   split; last split.
   { left. by constructor 1. }
   { have HLlrf: (r_f ⋅ r) .(rlm) !! l ≡ Some (to_locStateR (lsLocal v' (init_stack (Tagged tg)))).
@@ -699,7 +699,7 @@ Proof.
   have HL2: if k0 then  (r_f.(rtm) ⋅ r.(rtm)) !! tg = Some (to_tagKindR tkUnique, h0) else True.
   { destruct k0; [|done].
     by apply (tmap_lookup_op_r _ _ _ _ (proj1 (proj1 VALID)) Eqtg). }
-  exists (#[☠])%V, σs', r', (S n). split; last split.
+  exists (#[☠])%V, σs', r', n. split; last split.
   { left. by constructor 1. }
   { have Eqrlm: (r_f ⋅ r').(rlm) ≡ (r_f ⋅ r).(rlm) by destruct k0.
     destruct (for_each_lookup _ _ _ _ _ Eqα') as [EQ1 EQ2].
@@ -1180,7 +1180,7 @@ Proof.
   { destruct WSAT as (?&?&?&?&?&SREL&?). destruct SREL as (? & ? & Eqcs' & ?).
     eapply (head_step_fill_tstep _ []).
     econstructor. by econstructor. econstructor. by rewrite Eqcs'. }
-  exists (Val vs), σs', r, (S n).
+  exists (Val vs), σs', r, n.
   destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
   split; last split.
   { left. by constructor 1. }
@@ -1216,8 +1216,8 @@ Lemma sim_body_end_call_elim' fs ft r n vs vt σs σt Φ :
   ∀ r_f et' σt' (WSAT: wsat (r_f ⋅ r) σs σt)
     (NT: never_stuck fs (EndCall (Val vs)) σs)
     (STEPT: (EndCall (Val vt), σt) ~{ft}~> (et', σt')),
-  ∃ r' idx' σs', (EndCall (Val vs), σs) ~{fs}~>+ (Val vs, σs') ∧ et' = Val vt ∧
-    Φ r' idx' (ValR vs) σs' (ValR vt) σt' ∧
+  ∃ r' n' σs', (EndCall (Val vs), σs) ~{fs}~>+ (Val vs, σs') ∧ et' = Val vt ∧
+    Φ r' n' (ValR vs) σs' (ValR vt) σt' ∧
     wsat (r_f ⋅ r') σs' σt'.
 Proof.
   intros SIM r_f et' σt' WSAT NT STEPT.
@@ -1236,73 +1236,27 @@ Proof.
   specialize (SIMV NT1 _ WSAT1) as [ST1 TE1 STEPS1].
   apply tstep_end_call_inv in STEPT as (? & Eq1 &? & ? & ? & ? & ?);
         [|by eexists]. simpl in Eq1. symmetry in Eq1. simplify_eq.
-  specialize (TE1 vt eq_refl) as (vs2 & σs2 & r2 & idx2 & STEP2 & WSAT2 & POST).
-  exists r2, idx2, σs2.
-  have ?: vs2 = vs.
+  specialize (TE1 vt eq_refl) as (vs2 & σs2 & r2 & STEP2 & WSAT2 & POST).
+  exists r2, n1, σs2.
+  assert (vs2 = vs ∧ (EndCall #vs, σs) ~{fs}~>+ ((#vs)%E, σs2)) as [].
   { clear -STEP1 STEP2.
     destruct STEP1 as [STEP1|[Eq11 Eq12]]; [|simplify_eq].
-    - apply tstep_end_call_inv_tc in STEP1 as (? & Eq1 &? & ? & ? & ? & ?);
-        [|by eexists]. simpl in Eq1.
-      simplify_eq. destruct STEP2 as [?%result_tstep_tc_stuck|[]]; [done|].
-      simplify_eq.
-      have Eq := to_of_result vs2. rewrite -H1 /= in Eq. by simplify_eq.
-    - have Eq := to_of_result vs2.
-      destruct STEP2 as [STEP2|[? STEP2]].
-      + apply tstep_end_call_inv_tc in STEP2 as (? & Eq' &? & ? & ? & ? & ?);
-          [|by eexists].
-        simpl in Eq'. simplify_eq.
-        rewrite H /= in Eq. by simplify_eq.
-      + simplify_eq. by rewrite -H0 in Eq. }
-  subst vs2. split; [|done].
-  destruct STEP1 as [|[]], STEP2 as [|[]]; simplify_eq.
-  - eapply tc_rtc_l; eauto.
-  - done.
-  - done.
-Qed.
-
-Lemma sim_body_end_call_elim fs ft r n vs vt σs σt Φ :
-  r ⊨{n,fs,ft} (EndCall (Val vs), σs) ≥ (EndCall (Val vt), σt) : Φ →
-  ∀ r_f σs' σt' (WSAT: wsat (r_f ⋅ r) σs σt)
-    (NT: never_stuck fs (EndCall (Val vs)) σs)
-    (STEPS: (EndCall (Val vs), σs) ~{fs}~> (Val vs, σs'))
-    (STEPT: (EndCall (Val vt), σt) ~{ft}~> (Val vt, σt')),
-  ∃ r' idx', Φ r' idx' (ValR vs) σs' (ValR vt) σt' ∧ wsat (r_f ⋅ r') σs' σt'.
-Proof.
-  intros SIM r_f σs' σt' WSAT NT STEPS STEPT.
-  punfold SIM.
-  specialize (SIM NT _ WSAT) as [NOSK TERM STEPSS].
-  inversion STEPSS; last first.
-  { exfalso. clear -CALLTGT. symmetry in CALLTGT.
-    apply fill_end_call_decompose in CALLTGT as [[]|[K' [? Eq]]]; [done|].
-    destruct (fill_result ft K' (Call #[ScFnPtr fid] (Val <$> vl_tgt))) as [[] ?];
-      [rewrite Eq; by eexists|done]. }
-  specialize (STEP _ _ STEPT) as (es1 & σs1 & r1 & n1 & STEP1 & WSAT1 & SIMV).
-  have STEPK: (EndCall #vs, σs) ~{fs}~>* (es1, σs1).
-  { destruct STEP1 as [|[]]. by apply tc_rtc. by simplify_eq. }
-  have NT1 := never_stuck_tstep_rtc _ _ _ _ _ STEPK NT.
-  pclearbot. punfold SIMV.
-  specialize (SIMV NT1 _ WSAT1) as [ST1 TE1 STEPS1].
-  specialize (TE1 vt eq_refl) as (vs2 & σs2 & r2 & idx2 & STEP2 & WSAT2 & POST).
-  exists r2, idx2.
-  assert (σs2 = σs' ∧ vs2 = vs) as [].
-  { clear -STEP1 STEP2 STEPS.
-    apply tstep_end_call_inv in STEPS as (? & ? &? & ? & ? & ? & ?);
-      [|by eexists].
-    destruct STEP1 as [STEP1|[Eq11 Eq12]]; [|simplify_eq].
-    - apply tstep_end_call_inv_tc in STEP1 as (? & ? &? & ? & ? & ? & ?);
-        [|by eexists].
-      simplify_eq. destruct STEP2 as [?%result_tstep_tc_stuck|[]]; [done|].
-      simplify_eq.
-      rewrite H1 in H5. simplify_eq. split; [done|].
-      have Eq := to_of_result vs2. rewrite -H2 in Eq. by simplify_eq.
-    - have Eq := to_of_result vs2. 
-      destruct STEP2 as [STEP2|[? STEP2]].
-      + apply tstep_end_call_inv_tc in STEP2 as (? & ? &? & ? & ? & ? & ?);
-          [|by eexists].
-        rewrite H1 in H3. simplify_eq. split; [done|].
-        rewrite H2 in Eq. by simplify_eq.
-      + simplify_eq. by rewrite -H2 in Eq. }
-  subst σs2 vs2. done.
+    - have STEP1' := STEP1.
+       apply tstep_end_call_inv_tc in STEP1 as (v1 & Eq1 &? & ? & ? & ? & ?);
+        [|by eexists]. simplify_eq.
+      apply result_tstep_rtc in STEP2 as [Eq3 Eq4]; [|by eexists].
+      rewrite /to_result in Eq1. simplify_eq.
+      have Eq := to_of_result vs2. rewrite Eq3 /to_result in Eq. by simplify_eq.
+    - inversion STEP2 as [x1 x2 Eq2|x1 [] x3 STEP3 STEP4]; simplify_eq.
+      + have Eq := to_of_result vs2. by rewrite -Eq2 in Eq.
+      + have STEP3' := STEP3.
+        apply tstep_end_call_inv in STEP3 as (v1 & Eq1 &? & ? & ? & ? & ?);
+          [|by eexists]. simplify_eq.
+        apply result_tstep_rtc in STEP4 as [Eq3 Eq4]; [|by eexists].
+        rewrite /to_result in Eq1. simplify_eq.
+        have Eq := to_of_result vs2. rewrite Eq3 /to_result in Eq.
+        simplify_eq. split; [done|]. by apply tc_once. }
+  by subst vs2.
 Qed.
 
 (** PURE STEP ----------------------------------------------------------------*)

theories/sim/simple.v

@@ -90,14 +90,14 @@ Qed.
 
 Lemma sim_simple_val fs ft r n (vs vt: value) css cst Φ :
   Φ r n vs css vt cst →
-  r ⊨ˢ{S n,fs,ft} (vs, css) ≥ (vt, cst) : Φ.
+  r ⊨ˢ{n,fs,ft} (vs, css) ≥ (vt, cst) : Φ.
 Proof.
   intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ vs vt). done.
 Qed.
 
 Lemma sim_simple_place fs ft r n ls lt ts tt tys tyt css cst Φ :
   Φ r n (PlaceR ls ts tys) css (PlaceR lt tt tyt) cst →
-  r ⊨ˢ{S n,fs,ft} (Place ls ts tys, css) ≥ (Place lt tt tyt, cst) : Φ.
+  r ⊨ˢ{n,fs,ft} (Place ls ts tys, css) ≥ (Place lt tt tyt, cst) : Φ.
 Proof.
   intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)). done.
 Qed.