Updates from _impl.v to _impl_junk.v

1 files changed, 102 insertions, 55 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 8cb45c55..f5821810 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -527,12 +527,6 @@ Global Opaque PTree_frame_eq_check.
 
 (** hsilocal_simu_check and properties *)
 
-(* negation of sabort_local *)
-Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop :=
-  (st.(si_pre) ge sp rs0 m0)
-  /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None
-  /\ forall (r: reg), seval_sval ge sp (si_sreg st r) rs0 m0 <> None.
-
 Lemma ssem_local_sok ge sp rs0 m0 st rs m:
   ssem_local ge sp st rs0 m0 rs m -> sok_local ge sp rs0 m0 st.
 Proof.
@@ -808,8 +802,7 @@ Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) :=
    and a "dynamic" part -- that depends on it
 *)
 Definition hsiexit_refines_stat (hext: hsistate_exit) (ext: sistate_exit): Prop :=
-     hsi_cond hext = si_cond ext
-  /\ hsi_ifso hext = si_ifso ext.
+  hsi_ifso hext = si_ifso ext.
 
 Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
 
@@ -826,8 +819,9 @@ Qed.
 
 Definition hsiexit_refines_dyn ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop :=
    hsilocal_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext)
-   /\ hseval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0
-         = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0.
+   /\ (hsok_local ge sp rs0 m0 (hsi_elocal hext) -> 
+        hseval_condition ge sp (hsi_cond hext) (hsi_scondargs hext) (hsi_smem (hsi_elocal hext)) rs0 m0
+         = seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs0 m0).
 
 Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
   hsiexit_refines_stat hse1 se1 ->
@@ -853,32 +847,36 @@ Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx:
 Proof.
   intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2.
   assert (SEVALC:
-    seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) 
-  (the_rs0 ctx) (the_m0 ctx) =
-    seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) 
-  (the_rs0 ctx) (the_m0 ctx)).
-  { destruct HDYN1 as (_ & SCOND1). rewrite <- SCOND1 by assumption. clear SCOND1.
-    destruct HDYN2 as (_ & SCOND2). rewrite <- SCOND2 by assumption. clear SCOND2.
+   sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1) ->
+    (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond st1) (si_scondargs st1) (si_smem (si_elocal st1)) 
+      (the_rs0 ctx) (the_m0 ctx)) =
+    (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond st2) (si_scondargs st2) (si_smem (si_elocal st2)) 
+      (the_rs0 ctx) (the_m0 ctx))).
+  { destruct HDYN1 as ((OKEQ1 & _) & SCOND1).
+    rewrite OKEQ1; intro OK1. rewrite <- SCOND1 by assumption. clear SCOND1.
+    generalize (genv_match ctx).
+    intro GFS; refine (modusponens _ _ (hsiexit_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _ _) _); eauto.
+    destruct HDYN2 as (_ & SCOND2). intro OK2. rewrite <- SCOND2 by assumption. clear OK1 OK2 SCOND2.
     destruct SIMUC as ((path & _ & LSIMU) & _ & CONDEQ & ARGSEQ). destruct LSIMU as (_ & _ & MEMEQ).
     rewrite CONDEQ. rewrite ARGSEQ. rewrite MEMEQ. erewrite <- hseval_condition_preserved; eauto.
-    eapply ctx. }
+  }
   constructor; [assumption|]. intros is1 ICONT SSEME.
+  assert (OK1: sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal st1)). {
+    destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok; eauto. }
   assert (HOK1: hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1). {
-    unfold hsok_exit. destruct SSEME as (_ & SSEML & _). apply ssem_local_sok in SSEML.
-    destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. }
+    unfold hsok_exit. destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. }
   refine (modusponens _ _ (hsiexit_simu_core_nofail _ _ _ _ _ _ _ _ _ _ _ _) _).
     2: eapply ctx. all: eauto. intro HOK2.
-  destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _).
+  destruct SSEME as (SCOND & SLOC & PCEQ). destruct SIMUC as ((path & PATH & LSIMU) & REVEQ & _ & _); eauto.
   destruct HDYN1 as (LREF1 & _). destruct HDYN2 as (LREF2 & _).
   exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl.
   intros (SSEML & EQREG).
   eexists (mk_istate (icontinue is1) (si_ifso st2) _ (imem is1)). simpl. constructor.
-  - constructor; [|constructor]; [congruence | eassumption | reflexivity].
+  - constructor; intuition congruence || eauto.
   - unfold istate_simu. rewrite ICONT.
-    simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1). { destruct HREF1 as (_ & IFSO). congruence. }
-    exists path. constructor; [|constructor]; [congruence | | ].
-    + constructor; [|constructor]; simpl; auto.
-    + destruct HREF2 as (_ & IFSO). congruence.
+    simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1) by congruence.
+    exists path. constructor; [|constructor]; [congruence| |congruence].
+    constructor; [|constructor]; simpl; auto.
 Qed.
 
 Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2:
@@ -964,9 +962,43 @@ Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop :=
   hsi_pc hst = si_pc st
   /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st).
 
+Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop :=
+    nsok_nil st: nested_sok ge sp rs0 m0 st nil
+  | nsok_cons st se lse:
+     (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) ->
+     nested_sok ge sp rs0 m0 (si_elocal se) lse ->
+     nested_sok ge sp rs0 m0 st (se::lse).
+
+Lemma nested_sok_prop ge sp st sle rs0 m0:
+  nested_sok ge sp rs0 m0 st sle ->
+  sok_local ge sp rs0 m0 st ->
+  forall se, In se sle -> sok_local ge sp rs0 m0 (si_elocal se).
+Proof.
+  induction 1; simpl; intuition (subst; eauto).
+Qed.
+
+Lemma nested_sok_elocal ge sp rs0 m0 st2 exits:
+  nested_sok ge sp rs0 m0 st2 exits ->
+  forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) ->
+  nested_sok ge sp rs0 m0 st1 exits.
+Proof.
+  induction 1; [intros; constructor|].
+  intros. constructor; auto.
+Qed.
+
+Lemma nested_sok_tail ge sp rs0 m0 st lx exits:
+  is_tail lx exits ->
+  nested_sok ge sp rs0 m0 st exits ->
+  nested_sok ge sp rs0 m0 st lx.
+Proof.
+  induction 1; [auto|].
+  intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto.
+Qed.
+
 Definition hsistate_refines_dyn ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop :=
      hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st)
-  /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st).
+  /\ hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st)
+  /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st).
 
 Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
   hsistate_refines_stat hst1 st1 ->
@@ -994,22 +1026,25 @@ Remark init_hsistate_correct_dyn ge sp rs0 m0 pc:
 Proof.
   unfold init_hsistate. wlp_step_bind hst HST.
   wlp_simplify.
-  constructor; simpl; auto.
+  constructor; simpl; auto; [|constructor].
   - apply list_forall2_nil.
   - apply init_hsistate_local_correct. assumption.
+  - constructor.
 Qed.
 
 Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2,
   siexits_simu dm f lse1 lse2 ctx ->
   all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) ->
+  (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
   all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx).
 Proof.
-  induction 1; [unfold all_fallthrough; contradiction|].
-  intros X ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU).
+  induction 1; [unfold all_fallthrough; contradiction|]; simpl.
+  intros X OK ext INEXT. eapply all_fallthrough_revcons in X. destruct X as (SEVAL & ALLFU).
   apply IHlist_forall2 in ALLFU.
-  destruct H as (CONDSIMU & _).
-  inv INEXT; [|eauto].
-  erewrite <- CONDSIMU; eauto.
+  - destruct H as (CONDSIMU & _).
+    inv INEXT; [|eauto].
+    erewrite <- CONDSIMU; eauto.
+  - intros; intuition.
 Qed.
 
 Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2:
@@ -1029,23 +1064,27 @@ Proof.
 Qed.
 
 Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2:
-  siexits_simu dm f lse1 lse2 ctx -> forall ext1 lx1,
+  siexits_simu dm f lse1 lse2 ctx ->
+  forall ext1 lx1,
+  (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
   all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) ->
   exists ext2 lx2,
     all_fallthrough_upto_exit (the_ge2 ctx) (the_sp ctx) ext2 lx2 lse2 (the_rs0 ctx) (the_m0 ctx)
   /\ length lx1 = length lx2.
 Proof.
   induction 1.
-  - intros. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction.
-  - intros ext1 lx1 ALLFUE.
+  - intros ext lx1. intros OK H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction.
+  - simpl; intros ext lx1 OK ALLFUE.
     destruct ALLFUE as (ITAIL & ALLFU). inv ITAIL.
     + eexists; eexists.
       constructor; [| eapply list_forall2_length; eauto].
       constructor; [econstructor | eapply siexits_simu_all_fallthrough; eauto].
-    + exploit IHlist_forall2; [constructor; eauto|].
-      intros (ext2 & lx2 & ALLFUE2 & LENEQ).
-      eexists; eexists. constructor; eauto.
-      eapply all_fallthrough_upto_exit_cons; eauto.
+    + exploit IHlist_forall2.
+      * intuition. apply OK. eassumption.
+      * constructor; eauto.
+      * intros (ext2 & lx2 & ALLFUE2 & LENEQ).
+        eexists; eexists. constructor; eauto.
+        eapply all_fallthrough_upto_exit_cons; eauto.
 Qed.
 
 Lemma list_forall2_nth_error {A} (l1 l2: list A) P:
@@ -1096,7 +1135,7 @@ Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx:
 Proof.
   intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI.
   destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2).
-  destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2).
+  destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _).
   destruct SIMUC as (PCSIMU & ESIMU & LSIMU).
   exploit hsiexits_simu_core_correct; eauto. intro HESIMU.
   unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
@@ -1104,25 +1143,33 @@ Proof.
     exploit hsilocal_simu_core_correct; eauto; [apply ctx|]. simpl. intro SSEML2.
     exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor.
     + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]].
-      eapply siexits_simu_all_fallthrough; eauto. eapply hsiexits_simu_siexits; eauto.
+      eapply siexits_simu_all_fallthrough; eauto.
+      * eapply hsiexits_simu_siexits; eauto.
+      * eapply nested_sok_prop; eauto.
+        eapply ssem_local_sok; eauto.
     + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]].
       constructor.
   - destruct SEMI as (ext & lx & SSEME & ALLFU).
     assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
-    exploit siexits_simu_all_fallthrough_upto; eauto. intros (ext2 & lx2 & ALLFU2 & LENEQ).
-    assert (EXTSIMU: siexit_simu dm f ctx ext ext2). {
-      eapply list_forall2_nth_error; eauto.
-      - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto.
-      - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL.
-        assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto).
-        congruence. }
-    destruct EXTSIMU as (CONDEVAL & EXTSIMU).
-    apply EXTSIMU in SSEME; [|assumption]. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU).
-    exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor.
-    + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption.
-    + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ).
-      destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ).
-      exists path. repeat (constructor; auto).
+    exploit siexits_simu_all_fallthrough_upto; eauto.
+    * destruct ALLFU as (ITAIL & ALLF).
+      exploit nested_sok_tail; eauto. intros NESTED2.
+      inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML.
+      eapply nested_sok_prop; eauto.
+    * intros (ext2 & lx2 & ALLFU2 & LENEQ).
+      assert (EXTSIMU: siexit_simu dm f ctx ext ext2). {
+        eapply list_forall2_nth_error; eauto.
+        - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto.
+        - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL.
+          assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto).
+          congruence. }
+      destruct EXTSIMU as (CONDEVAL & EXTSIMU).
+      apply EXTSIMU in SSEME; [|assumption]. clear EXTSIMU. destruct SSEME as (is2 & SSEME2 & ISIMU).
+      exists (mk_istate (icontinue is1) (ipc is2) (irs is2) (imem is2)). constructor.
+      + unfold ssem_internal. simpl. rewrite ICONT. exists ext2, lx2. constructor; assumption.
+      + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ).
+        destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ).
+        exists path. repeat (constructor; auto).
 Qed.
 
 Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=