reduction de la preuve de raffinement du exit à ok_allexit

2 files changed, 81 insertions, 54 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 4e159b15..96854123 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -49,19 +49,6 @@ Proof.
   unfold hsi_sreg_eval, hsi_sreg_get; destruct (PTree.get r hst); simpl; auto.
 Qed.
 
-(* 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.
-  unfold sok_local, ssem_local. 
-  intuition congruence.
-Qed.
-
 Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
      (forall sv, List.In sv (hsi_ok_lsval hst) -> seval_sval ge sp sv rs0 m0 <> None)
   /\ (seval_smem ge sp hst.(hsi_smem) rs0 m0 <> None).
@@ -216,8 +203,8 @@ Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
 
 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)
-   /\ seval_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) -> seval_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 ->
@@ -243,26 +230,31 @@ 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; exploit 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 <- seval_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. }
   exploit 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].
@@ -329,14 +321,16 @@ Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f):
 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:
@@ -356,23 +350,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 se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
+  forall ext1 lx1,
   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 OK ext lx1 H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction.
+  - simpl; intros OK ext1 lx1 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.
+      * 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:
@@ -417,11 +415,20 @@ Proof.
       rewrite H0; auto.
 Qed.
 
+
+Lemma ok_allexit ge sp st rs m is1:
+  ssem_internal ge sp st rs m is1 ->
+  forall se, In se (si_exits st) -> sok_local ge sp rs m (si_elocal se).
+Admitted. (* TODO !! *)
+
+
 Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx:
   hsistate_simu_core dm f hst1 hst2 ->
   hsistate_simu dm f hst1 hst2 ctx.
 Proof.
   intros SIMUC st1 st2 HREF1 HREF2 DREF1 DREF2 is1 SEMI.
+  generalize (ok_allexit _ _ _ _ _ _ SEMI).
+  intros EXOK.
   destruct HREF1 as (PCREF1 & EREF1). destruct HREF2 as (PCREF2 & EREF2).
   destruct DREF1 as (DEREF1 & LREF1). destruct DREF2 as (DEREF2 & LREF2).
   destruct SIMUC as (PCSIMU & ESIMU & LSIMU).
@@ -431,18 +438,20 @@ 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.
     + 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. }
+    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.
@@ -1158,7 +1167,7 @@ Proof.
 Qed.
 
 Lemma seval_condition_refines hst st ge sp cond args rs m:
-  hsok_local ge sp rs m hst ->
+  hsok_local ge sp rs m hst -> 
   hsilocal_refines ge sp rs m hst st ->
   seval_condition ge sp cond args (hsi_smem hst) rs m
   = seval_condition ge sp cond args (si_smem st) rs m.
@@ -1226,9 +1235,13 @@ Proof.
       erewrite seval_smem_refines; eauto.
       erewrite seval_sval_refines; eauto.
   - (* Icond *)
-    admit. (* TODO *)
-Admitted.
-
+    destruct REF as (EXREF & LREF). constructor; simpl; [|assumption].
+    constructor; [|assumption].
+    constructor; simpl; [assumption|].
+    intros; erewrite seval_condition_refines; eauto.
+    unfold seval_condition.
+    erewrite seval_list_sval_refines; eauto.
+Qed.
 
 Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate :=
   match path with
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v
index 3ae6e713..4fb6bee3 100644
--- a/kvx/lib/RTLpathSE_theory.v
+++ b/kvx/lib/RTLpathSE_theory.v
@@ -1865,11 +1865,25 @@ Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (sl1 sl2: sista
     exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2)
                 /\ istate_simu f dm is1 is2.
 
+(* 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.
+  unfold sok_local, ssem_local. 
+  intuition congruence.
+Qed.
+
 Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof_context f) (se1 se2: sistate_exit) :=
-    (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) 
-      (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) 
-  = (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2)
-      (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx))
+  (sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1) ->
+          (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) 
+                             (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) =
+          (seval_condition (the_ge2 ctx) (the_sp ctx) (si_cond se2) (si_scondargs se2)
+                             (si_smem (si_elocal se2)) (the_rs0 ctx) (the_m0 ctx)))
   /\ forall is1,
       icontinue is1 = false ->
       ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) ->