SUCCESS: prouve 1 des admit de hsistate_simu_core_correct.

Le deuxième doit marcher à peu près pareil modulo siexits_simu_all_fallthrough_upto à corriger ?

1 files changed, 13 insertions, 14 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 6fa4ea59..24e3cc74 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -359,7 +359,7 @@ Qed.
 
 Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2:
   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 se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) (* FIXME: semble bcp trop fort !*) ->
   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,
@@ -423,12 +423,13 @@ Proof.
       rewrite H0; auto.
 Qed.
 
-(*
-Lemma ok_allexit ge sp hst st rs m:
-  hsiexits_refines_dyn ge sp rs m hst st ->
-  forall se, In se st -> sok_local ge sp rs m (si_elocal se).
-Admitted. (* TODO !! *)
-*)
+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.
 
 Theorem hsistate_simu_core_correct dm f hst1 hst2 ctx:
   hsistate_simu_core dm f hst1 hst2 ->
@@ -437,10 +438,6 @@ 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 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _).
-(*
-  generalize (ok_allexit _ _ _ _ _ _ DEREF1).
-  intros EXOK.
-*)
   destruct SIMUC as (PCSIMU & ESIMU & LSIMU).
   exploit hsiexits_simu_core_correct; eauto. intro HESIMU.
   unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
@@ -450,7 +447,8 @@ Proof.
     + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]].
       eapply siexits_simu_all_fallthrough; eauto.
       * eapply hsiexits_simu_siexits; eauto.
-      * admit.
+      * 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).
@@ -471,7 +469,7 @@ Proof.
       + 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.
+Admitted.
 
 (* Definition hfinal_refines hfv fv := forall pge ge sp npc stk f rs0 m0 rs' m' t s',
   ssem_final pge ge sp npc stk f rs0 m0 hfv rs' m' t s' <-> ssem_final pge ge sp npc stk f rs0 m0 fv rs' m' t s'. *)
@@ -1386,9 +1384,10 @@ Qed.
 Remark init_hsistate_correct_dyn ge sp rs0 m0 pc:
   hsistate_refines_dyn ge sp rs0 m0 (init_hsistate pc) (init_sistate pc).
 Proof.
-  constructor; simpl; auto.
+  constructor; [|constructor]; simpl; auto.
   - apply list_forall2_nil.
   - apply init_hsistate_local_correct.
+  - constructor.
 Qed.
 
 Definition hsexec (f: function) (pc:node): option hsstate :=