seval_condition_refines ---> refinement correct only for successful executions ?

1 files changed, 47 insertions, 19 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index f5285070..294867c0 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -760,19 +760,25 @@ Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hs
   else Error (msg "siexit_simub: conditions do not match")
 .
 
+Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
+
 Definition hsiexit_simu dm f hse1 hse2 (ctx: simu_proof_context f): Prop := forall se1 se2,
   hsistate_exit_refines_stat hse1 se1 ->
   hsistate_exit_refines_stat hse2 se2 ->
   hsistate_exit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
   hsistate_exit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
+  hsok_exit (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 ->
+  hsok_exit (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 ->
   siexit_simu dm f ctx se1 se2.
 
-
 Lemma seval_condition_refines hst st ge sp cond args rs m:
+  hsok_local ge sp rs m hst ->
   hsistate_local_refines ge sp rs m hst st ->
   seval_condition ge sp cond args (hsi_smem_get hst) rs m = seval_condition ge sp cond args (si_smem st) rs m.
 Proof.
-Admitted.
+  intros HOK (OKEQ & MEMEQ & RSEQ). unfold seval_condition.
+  rewrite <- MEMEQ; auto. rewrite hsi_smem_eval_correct. reflexivity.
+Qed.
 
 Local Hint Resolve genv_match: core.
 
@@ -785,7 +791,7 @@ Proof.
   intros (SREGEQ & SMEMEQ) ctx.
   eapply hsilocal_simub_correct in EQ2.
   apply revmap_check_single_correct in EQ3.
-  intros se1 se2 (HCOND1 & HARGS1 & HIFSO1) (HCOND2 & HARGS2 & HIFSO2) HLREF1 HLREF2.
+  intros se1 se2 (HCOND1 & HARGS1 & HIFSO1) (HCOND2 & HARGS2 & HIFSO2) HLREF1 HLREF2 HOK1 HOK2.
   unfold hsistate_exit_refines_dyn in *.
   constructor.
   - unfold siexit_simu_ssem. intros is SEMEXIT.
@@ -828,11 +834,18 @@ Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: l
       end
   end.
 
+Inductive hsok_exits ge sp rs m: list hsistate_exit -> Prop :=
+  | hsok_exits_nil: hsok_exits ge sp rs m nil
+  | hsok_exits_cons: forall l ex, hsok_exits ge sp rs m l -> hsok_exit ge sp rs m ex -> hsok_exits ge sp rs m (ex::l)
+  .
+
 Definition hsiexits_simu dm f (hse1 hse2: list hsistate_exit) (ctx: simu_proof_context f): Prop := forall se1 se2,
   list_forall2 hsistate_exit_refines_stat hse1 se1 ->
   list_forall2 hsistate_exit_refines_stat hse2 se2 ->
   list_forall2 (hsistate_exit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx)) hse1 se1 ->
   list_forall2 (hsistate_exit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx)) hse2 se2 ->
+  hsok_exits (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 ->
+  hsok_exits (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 ->
   siexits_simu dm f se1 se2 ctx.
 
 Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
@@ -840,12 +853,13 @@ Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
   hsiexits_simu dm f lhse1 lhse2 ctx.
 Proof.
   induction lhse1.
-  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _.
+  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _ _ _.
     inv HEREFS1. inv HEREFS2. constructor.
   - (* simpl. *) unfold hsiexits_simub. intros. destruct lhse2; try discriminate. explore.
     fold hsiexits_simub in EQ1.
     eapply hsiexit_simub_correct in EQ. apply IHlhse1 in EQ1.
-    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2. inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. constructor; auto.
+    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2 HOK1 HOK2.
+    inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. inv HOK1. inv HOK2. constructor; auto.
     apply EQ1; assumption.
 Qed.
 
@@ -854,11 +868,16 @@ Definition hsistate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: h
   do _ <- hsiexits_simub dm f (hsi_exits hst1) (hsi_exits hst2);
   OK tt.
 
+Definition hsok_internal ge sp rs m hst :=
+  hsok_exits ge sp rs m (hsi_exits hst) /\ hsok_local ge sp rs m (hsi_local hst).
+
 Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
   hsistate_refines_stat hst1 st1 ->
   hsistate_refines_stat hst2 st2 ->
   hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
   hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
+  hsok_internal (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
+  hsok_internal (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 ->
   sistate_simu dm f st1 st2 ctx.
 
 Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2,
@@ -942,7 +961,8 @@ Lemma hsistate_simub_correct dm f hst1 hst2:
   forall ctx, hsistate_simu dm f hst1 hst2 ctx.
 Proof.
   unfold hsistate_simub. intro. explore. unfold hsistate_simu.
-  intros ctx st1 st2 (PCEQ1 & HEREFD1) (PCEQ2 & HEREFD2) (HREF1 & HLREF1) (HREF2 & HLREF2) is1 SEMI.
+  intros ctx st1 st2 (PCEQ1 & HEREFD1) (PCEQ2 & HEREFD2)
+    (HREF1 & HLREF1) (HREF2 & HLREF2) (HOKE1 & HOKL1) (HOKE2 & HOKL2) is1 SEMI.
   exploit hsiexits_simub_correct; eauto. intro ESIMU.
   unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
   - destruct SEMI as (SSEML & PCEQ & ALLFU).
@@ -962,11 +982,13 @@ Proof.
       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).
+        assert (LENEQ': length (si_exits st1) = length (si_exits st2))
+          by (eapply list_forall2_length; eauto).
         congruence. }
     destruct EXTSIMU as (SEMSIMU & _). eapply SEMSIMU in SSEME; eauto.
     destruct SSEME as (is2 & SSEME2 & ISIMU).
-    unfold istate_simu in ISIMU. rewrite ICONT in ISIMU. destruct ISIMU as (path & PATHEQ & SIMULIVE & REVBIND).
+    unfold istate_simu in ISIMU. rewrite ICONT in ISIMU.
+    destruct ISIMU as (path & PATHEQ & SIMULIVE & REVBIND).
     destruct SIMULIVE as (CONTEQ & REGLIVE & MEMEQ).
     unfold ssem_internal. exists is2.
     rewrite <- CONTEQ. rewrite ICONT. constructor; auto.
@@ -974,11 +996,15 @@ Proof.
     + unfold istate_simu. rewrite ICONT. eexists. repeat (constructor; eauto).
 Qed.
 
+Definition hsok ge sp rs m hst := hsok_internal ge sp rs m (hinternal hst).
+
 Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
   forall st1 st2,
   hsstate_refines hst1 st1 ->
-  hsstate_refines hst2 st2 -> sstate_simu f dm st1 st2 ctx.
-
+  hsstate_refines hst2 st2 ->
+  hsok (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
+  hsok (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 ->
+  sstate_simu f dm st1 st2 ctx.
 
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): res unit :=
   match ln with
@@ -1215,14 +1241,16 @@ Proof.
   - destruct fv2; try discriminate. intro. explore.
     apply svos_simub_correct in EQ3. apply list_sval_simub_correct in EQ4.
     subst. apply revmap_check_single_correct in EQ. constructor; auto.
-    + admit.
-    + admit.
+    + destruct svos0; constructor; [| reflexivity ].
+      erewrite <- seval_preserved; eauto. constructor.
+    + erewrite <- list_sval_eval_preserved; eauto. constructor.
   (* Stailcall *)
   - destruct fv2; try discriminate. intro. explore.
     apply svos_simub_correct in EQ0. apply list_sval_simub_correct in EQ1.
     subst. constructor; auto.
-    + admit.
-    + admit.
+    + destruct s2; constructor; [| reflexivity].
+      erewrite <- seval_preserved; eauto. constructor.
+    + erewrite <- list_sval_eval_preserved; eauto. constructor.
   (* Sbuiltin *)
   - destruct fv2; try discriminate. intro. explore.
     apply revmap_check_single_correct in EQ1. apply list_builtin_arg_simub_correct in EQ2.
@@ -1230,13 +1258,12 @@ Proof.
   (* Sjumptable *)
   - destruct fv2; try discriminate. intro. explore.
     apply revmap_check_list_correct in EQ. apply sval_simub_correct in EQ0. subst.
-    constructor; auto.
-    admit.
+    constructor; auto. erewrite <- seval_preserved; eauto. constructor.
   (* Sreturn *)
   - destruct fv2; try discriminate. destruct o; destruct o0; try discriminate.
     + intro. apply sval_simub_correct in H. subst. constructor; auto.
     + constructor; auto.
-Admitted.
+Qed.
 
 Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
   do u1 <- hsistate_simub dm f (hinternal hst1) (hinternal hst2);
@@ -1249,7 +1276,7 @@ Lemma hsstate_simub_correct dm f hst1 hst2 ctx:
 Proof.
   unfold hsstate_simub. intro. explore.
   eapply sfval_simub_correct in EQ1. eapply hsistate_simub_correct in EQ.
-  intros st1 st2 (SREF1 & LREF1 & FREF1) (SREF2 & LREF2 & FREF2).
+  intros st1 st2 (SREF1 & LREF1 & FREF1) (SREF2 & LREF2 & FREF2) HOK1 HOK2.
   constructor; [eauto |].
   destruct SREF1 as (PCEQ1 & _ ). destruct SREF2 as (PCEQ2 & _ ).
   rewrite <- PCEQ1. rewrite <- PCEQ2. rewrite <- FREF1. rewrite <- FREF2.
@@ -1284,7 +1311,8 @@ Proof.
   rewrite SEXEC1 in SEXEC; inversion SEXEC; subst.
   eexists; split; eauto.
   intros; eapply hsstate_simub_correct; eauto.
-Qed.
+  all: admit. (* FIXME - le raffinement n'est prouvé correct que dans le cas où on ne fail pas *)
+Admitted.
 
 Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm :=
   match lm with