Avancement

2 files changed, 290 insertions, 88 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index c21af3e6..2c4ae088 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -7,6 +7,7 @@ Require Import Op Registers.
 Require Import RTL RTLpath.
 Require Import Errors Duplicate.
 Require Import RTLpathSE_theory.
+Require Import Axioms.
 
 Local Open Scope error_monad_scope.
 Local Open Scope option_monad_scope.
@@ -57,7 +58,7 @@ Definition hsi_smem_eval ge sp (hst: list smem) rs0 m0 : option mem :=
    | sm::_ => seval_smem ge sp sm rs0 m0
    end.
 
-(* negation of sabort_local *)
+(* (* negation of sabort_local *)
 Definition sok_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem): Prop :=
   (st.(si_pre) ge sp rs0 m0)
   /\ seval_smem ge sp st.(si_smem) rs0 m0 <> None
@@ -65,13 +66,13 @@ Definition sok_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (
 
 Definition hsok_local ge sp (hst: hsistate_local) rs0 m0: Prop :=
      (forall sv, List.In sv (hsi_ok_lsval hst) -> seval_sval ge sp sv rs0 m0 <> None)
-  /\ (forall sm, List.In sm (hsi_lsmem hst) -> seval_smem ge sp sm rs0 m0 <> None).
+  /\ (forall sm, List.In sm (hsi_lsmem hst) -> seval_smem ge sp sm rs0 m0 <> None). *)
 
 (* refinement link between a (st: sistate_local) and (hst: hsistate_local) *)
 Definition hsistate_local_refines (hst: hsistate_local) (st: sistate_local) := forall ge sp rs0 m0,
-     (sok_local ge sp st rs0 m0 <-> hsok_local ge sp hst rs0 m0)
-  /\ (hsok_local ge sp hst rs0 m0 -> hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0)
-  /\ (hsok_local ge sp hst rs0 m0 -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0).
+(*      (sok_local ge sp st rs0 m0 <-> hsok_local ge sp hst rs0 m0) *)
+     ((* hsok_local ge sp hst rs0 m0 -> *) hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0)
+  /\ ((* hsok_local ge sp hst rs0 m0 -> *) forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0).
 
 (* Syntax and semantics of symbolic exit states *)
 (* TODO: add hash-consing *)
@@ -117,7 +118,7 @@ Definition hslocal_set_smem (hst:hsistate_local) (sm:smem) :=
      hsi_sreg:= hsi_sreg hst
   |}.
 
-Lemma sok_local_set_mem st sm ge sp rs0 m0:
+(* Lemma sok_local_set_mem st sm ge sp rs0 m0:
   sok_local ge sp (slocal_set_smem st sm) rs0 m0 
   <-> (sok_local ge sp st rs0 m0 /\ seval_smem ge sp sm rs0 m0 <> None).
 Proof.
@@ -129,34 +130,26 @@ Lemma hsok_local_set_mem hst sm ge sp rs0 m0:
   <-> (hsok_local ge sp hst rs0 m0 /\ seval_smem ge sp sm rs0 m0 <> None).
 Proof.
   unfold hslocal_set_smem, hsok_local; simpl; intuition (subst; eauto).
-Qed.
+Qed. *)
 
 Lemma hslocal_set_mem_correct hst st hsm sm:
   hsistate_local_refines hst st ->
-  (forall ge sp rs0 m0, hsok_local ge sp hst rs0 m0 -> seval_smem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0) ->
+  (forall ge sp rs0 m0, (* hsok_local ge sp hst rs0 m0 -> *) seval_smem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0) ->
   hsistate_local_refines (hslocal_set_smem hst hsm) (slocal_set_smem st sm).
 Proof.
   intros LOCREF. intros SMEMEQ.
-  intros ge sp rs0 m0. edestruct LOCREF as (OKEQ & SMEMEQ' & REGEQ). constructor; [|constructor].
-  - rewrite hsok_local_set_mem.
+  intros ge sp rs0 m0. edestruct LOCREF as ((* OKEQ & *) SMEMEQ' & REGEQ). constructor.
+(*   - rewrite hsok_local_set_mem.
     rewrite sok_local_set_mem.
     constructor.
     + intros (OKL & SMEMN). constructor. 2: rewrite SMEMEQ; auto.
       all: rewrite <- OKEQ; assumption.
     + intros (HOKL & HSMEM). rewrite OKEQ. constructor; auto.
-      rewrite <- SMEMEQ; auto.
-  - rewrite hsok_local_set_mem. intros (HOKL & HSMEM).
+      rewrite <- SMEMEQ; auto. *)
+  - (* rewrite hsok_local_set_mem. intros (HOKL & HSMEM). *)
     simpl. apply SMEMEQ; assumption.
-  - rewrite hsok_local_set_mem. intros (HOKL & HSMEM).
-    simpl. intuition congruence.
-
-
-(*   unfold hsistate_local_refines. 
-  intros (OK & MEM & VAL) HSM; simpl. intros ge sp rs0 m0.
-  rewrite hsok_local_set_mem.
-  rewrite sok_local_set_mem.
-  rewrite! OK.
-  intuition congruence. *)
+  - (* rewrite hsok_local_set_mem. intros (HOKL & HSMEM). *)
+    simpl. eassumption. (*  intuition congruence. *)
 Qed.
 
 (** ** Assignment of local state *)
@@ -203,6 +196,7 @@ Proof.
   unfold negb; explore; simpl; intuition (try congruence).
 Qed.
 
+(* not used yet *)
 Lemma may_trap_correct (ge: RTL.genv) (sp:val) (rsv: root_sval) (rs0: regset) (m0: mem) (lsv: list sval) (sm: smem):
   may_trap rsv lsv sm = false -> 
   seval_list_sval ge sp (list_sval_inj lsv) rs0 m0 <> None ->
@@ -290,14 +284,15 @@ Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv sm
      hsi_ok_lsval := if may_trap rsv lsv sm then (rsv lsv sm)::(hsi_ok_lsval hst) else hsi_ok_lsval hst;
      hsi_sreg := red_PTree_set r (simplify rsv lsv sm) (hsi_sreg hst) |}.
 
-Definition ok_args hst ge sp rs0 m0 lsv sm :=
-  hsok_local ge sp hst rs0 m0 ->  (seval_list_sval ge sp (list_sval_inj lsv) rs0 m0 <> None /\ seval_smem ge sp sm rs0 m0 <> None).
+Definition ok_args ge sp rs0 m0 lsv sm :=
+  (* hsok_local ge sp hst rs0 m0 ->  *) 
+  (seval_list_sval ge sp (list_sval_inj lsv) rs0 m0 <> None /\ seval_smem ge sp sm rs0 m0 <> None).
 
 Lemma hslocal_set_sreg_correct hst st r (rsv:root_sval) lsv sm sv':
   hsistate_local_refines hst st ->
   (forall ge sp rs0 m0,
-  ok_args hst ge sp rs0 m0 lsv sm ->
-  (hsok_local ge sp hst rs0 m0 -> seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lsv sm) rs0 m0) ) ->
+  ok_args (* hst *) ge sp rs0 m0 lsv sm ->
+  ((* hsok_local ge sp hst rs0 m0 -> *) seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lsv sm) rs0 m0) ) ->
   hsistate_local_refines (hslocal_set_sreg hst r rsv lsv sm) (slocal_set_sreg st r sv').
 Admitted.
 
@@ -332,6 +327,34 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate :=
 
 Local Hint Resolve hsist_set_local_correct hsistate_refines_imp_local_refines hslocal_set_mem_correct: core.
 
+Lemma seval_sval_refines hst st ge sp rs0 m0 p:
+(*   sok_local ge sp st rs0 m0 -> *)
+  hsistate_local_refines hst st ->
+  seval_sval ge sp (hsi_sreg_get hst p) rs0 m0 = seval_sval ge sp (si_sreg st p) rs0 m0.
+Proof.
+  intros (* OKL *) HREF. destruct (HREF ge sp rs0 m0) as ((* OKEQ & *) _ & RSEQ).
+  (* apply OKEQ in OKL. rewrite <- (RSEQ OKL p). *)
+  rewrite <- (RSEQ p).
+  unfold hsi_sreg_get, hsi_sreg_eval. destruct (hst ! p); auto.
+Qed.
+
+Lemma seval_list_sval_refines hsl sl ge sp rs0 m0 l:
+(*   sok_local ge sp sl rs0 m0 -> *)
+  hsistate_local_refines hsl sl ->
+  seval_list_sval ge sp (list_sval_inj (map (hsi_sreg_get hsl) l)) rs0 m0 =
+  seval_list_sval ge sp (list_sval_inj (map (si_sreg sl) l)) rs0 m0.
+Proof.
+  intros (* OKL *) HLREF. destruct (HLREF ge sp rs0 m0) as ((* OKEQ & *) _ & RSEQ).
+  induction l; simpl; auto.
+  erewrite seval_sval_refines; eauto. rewrite IHl. destruct (seval_sval ge sp _ _ _); reflexivity.
+Qed.
+
+Lemma seval_smem_refines hst st rs0 m0 ge sp:
+  hsistate_local_refines hst st ->
+  seval_smem ge sp (hsi_smem_get hst) rs0 m0 = seval_smem ge sp (si_smem st) rs0 m0.
+Proof.
+Admitted.
+
 Lemma hsiexec_inst_correct i hst hst' st:
   hsiexec_inst i hst = Some hst' ->
   hsistate_refines hst st ->
@@ -354,11 +377,15 @@ Proof.
   - (* Istore *) intros REF; eexists; split; eauto.
     eapply hsist_set_local_correct; eauto.
     eapply hslocal_set_mem_correct; eauto.
-    admit. (* TODO: the easiest case of all these TODO ? *)
+    intros. simpl. destruct REF as (_ & _ & LREF).
+    erewrite seval_list_sval_refines; eauto.
+    erewrite seval_smem_refines; eauto.
+    erewrite seval_sval_refines; eauto.
   - (* Icond *) intros REF; eexists; split; eauto.
     admit. (* TODO *)
 Admitted.
 
+
 Lemma hsiexec_inst_error i hst st:
   hsiexec_inst i hst = None ->
   hsistate_refines hst st ->
@@ -395,12 +422,21 @@ Lemma hsiexec_path_correct ps f hst hst' st:
 Proof.
 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'. *)
+
+(* FIXME - too strong, let's change it later.. *)
+Definition hfinal_refines (hfv fv: sfval) := hfv = fv.
+
+Remark hfinal_refines_snone: hfinal_refines Snone Snone.
+Proof.
+Admitted.
+
 Record hsstate := { hinternal:> hsistate; hfinal: sfval }.
 
-(* CS: made hsstate_refines independent of ge, sp, rs0 and m0 *)
 Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
   hsistate_refines (hinternal hst) (internal st)
-  /\ hfinal hst = final st. (* TODO *)
+  /\ hfinal_refines (hfinal hst) (final st).
 
 Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := 
   match i with
@@ -424,23 +460,59 @@ Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval :=
   | _ => Snone
   end.
 
+(* Lemma local_refines_sreg_get hsl sl ge sp rs0 m0:
+  hsistate_local_refines hsl sl ->
+  sok_local ge sp sl rs0 m0 ->
+  hsi_sreg_get hsl = si_sreg sl.
+Proof.
+  intros HREF SOKL. apply functional_extensionality. intro r.
+  destruct (HREF ge sp rs0 m0) as (OKEQ & MEMEQ & RSEQ).
+  apply OKEQ in SOKL. pose (RSEQ SOKL r) as EQ.
+  unfold hsi_sreg_get. 
+Admitted. *)
+
+Lemma sfind_function_conserves hsl sl pge ge sp s rs0 m0:
+  hsistate_local_refines hsl sl ->
+  sfind_function pge ge sp (sum_left_map (hsi_sreg_get hsl) s) rs0 m0 =
+  sfind_function pge ge sp (sum_left_map (si_sreg sl) s) rs0 m0.
+Admitted.
+
 Lemma hsexec_final_correct hsl sl i:
   hsistate_local_refines hsl sl ->
-  hsexec_final i hsl = sexec_final i sl.
+  hfinal_refines (hsexec_final i hsl) (sexec_final i sl).
 Proof.
+(*   destruct i; simpl; intros HLREF; try (apply hfinal_refines_snone).
+  (* Scall *)
+  - constructor.
+    + intro. inv H. constructor; auto.
+      ++ erewrite <- sfind_function_conserves; eauto.
+      ++ erewrite <- seval_list_sval_refines; eauto.
+    + intro. inv H. constructor; auto.
+      ++ erewrite sfind_function_conserves; eauto.
+      ++ erewrite seval_list_sval_refines; eauto.
+  (* Stailcall *)
+  - admit.
+  (* Sbuiltin *)
+  - admit.
+  (* Sjumptable *)
+  - admit.
+  (* Sreturn *)
+  - admit. *)
 Admitted.
 
+
+
 Definition init_hsistate_local := {| hsi_lsmem := Sinit::nil; hsi_ok_lsval := nil; hsi_sreg := PTree.empty sval |}.
 
 Remark init_hsistate_local_correct:
   hsistate_local_refines init_hsistate_local init_sistate_local.
 Proof.
-  constructor; constructor.
-  - intro. destruct H as (_ & SMEM & SVAL). constructor; simpl in *; [contradiction|].
-    intros. destruct H; [|contradiction]. subst. discriminate.
-  - intro. destruct H as (SVAL & SMEM). constructor; [simpl; auto|].
-    constructor; simpl; discriminate.
-  - intro. reflexivity.
+  constructor.
+(*   - intro. destruct H as (_ & SMEM & SVAL). constructor; simpl in *; [contradiction|].
+    intros. destruct H; [|contradiction]. subst. discriminate. *)
+(*   - intro. destruct H as (SVAL & SMEM). constructor; [simpl; auto|].
+    constructor; simpl; discriminate. *)
+  - reflexivity.
   - intros. simpl. unfold hsi_sreg_eval. rewrite PTree.gempty. reflexivity.
 Qed.
 
@@ -463,15 +535,6 @@ Definition hsexec (f: function) (pc:node): option hsstate :=
        | None => {| hinternal := hst; hfinal := hsexec_final i hst.(hsi_local) |}
        end).
 
-(* FIXME - this lemma might be unprovable ?  SB: inutile en principe
-Lemma hsistate_refines_determ hst st st':
-  hsistate_refines hst st ->
-  hsistate_refines hst st' ->
-  st = st'.
-Proof.
-Admitted.
-*)
-
 Lemma hsexec_correct f pc hst:
   hsexec f pc = Some hst ->
   exists st, sexec f pc = Some st /\
@@ -484,9 +547,9 @@ Proof.
   erewrite <- hsistate_refines_pceq; eauto. rewrite EQ1.
   destruct (hsiexec_inst i h) eqn:HINST.
   - destruct (siexec_inst i st0) eqn:SINST.
-    + eexists. constructor; [reflexivity|]. constructor; auto. simpl.
+    + eexists. constructor; [reflexivity|]. constructor; auto; simpl; [|apply hfinal_refines_snone].
       eapply hsiexec_inst_correct in HINST; eauto. destruct HINST as (st' & SINST' & HREF').
-      assert (s = st') by congruence. subst. assumption. (* admit. (* TODO - issue with scope ! *) *)
+      assert (s = st') by congruence. subst. assumption.
     + (* absurd case *)
       eapply hsiexec_inst_correct in HINST; eauto. destruct HINST as (st' & SINST' & _).
       rewrite SINST in SINST'. discriminate.
@@ -497,58 +560,197 @@ Proof.
       apply hsexec_final_correct; auto.
 Qed.
 
-(* NB: inutile en principe.
-Lemma hsexec_complete f pc st:
-  sexec f pc = Some st ->
-  exists hst, hsexec f pc = Some hst /\ hsstate_refines hst st.
-Proof.
-  unfold sexec. intro. explore_hyp.
-  eapply hsiexec_path_complete in EQ0; [| apply init_hsistate_correct].
-  destruct EQ0 as (hst & HPATH & HREF).
-  eexists. constructor.
-  + unfold hsexec. rewrite EQ. rewrite HPATH.
-    erewrite hsistate_refines_pceq; eauto. rewrite EQ1. reflexivity.
-  + destruct (siexec_inst i s) eqn:EINST.
-    - eapply hsiexec_inst_complete in EINST; eauto. destruct EINST as (hst' & HEINST & HREF').
-      rewrite HEINST. constructor; auto.
-    - eapply hsiexec_inst_none in EINST; eauto. rewrite EINST.
-      constructor; auto. simpl.
-      destruct HREF as (_ & _ & HLREF). apply hsexec_final_correct. assumption.
+Definition hsilocal_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate_local) := OK tt.
+
+Definition hsilocal_simu dm f (hst1 hst2: hsistate_local): Prop := forall st1 st2,
+  hsistate_local_refines hst1 st1 ->
+  hsistate_local_refines hst2 st2 ->
+  silocal_simu dm f st1 st2.
+
+Lemma hsilocal_simub_correct dm f hst1 hst2:
+  hsilocal_simub dm f hst1 hst2 = OK tt ->
+  hsilocal_simu dm f hst1 hst2.
+Proof.
+Admitted.
+
+Lemma hsilocal_simub_eq dm f hsl1 hsl2:
+  hsilocal_simub dm f hsl1 hsl2 = OK tt ->
+     hsi_sreg_get (hsi_sreg hsl1) = hsi_sreg_get (hsi_sreg hsl2)
+  /\ hsi_smem_get (hsi_lsmem hsl1) = hsi_smem_get (hsi_lsmem hsl2).
+Proof.
+Admitted.
+
+Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) :=
+  if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then
+    do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2);
+    do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2);
+    revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2)
+  else Error (msg "siexit_simub: conditions do not match")
+.
+
+Definition hsiexit_simu dm f hse1 hse2: Prop := forall se1 se2,
+  hsistate_exit_refines hse1 se1 ->
+  hsistate_exit_refines hse2 se2 ->
+  siexit_simu dm f se1 se2.
+
+(* Lemma seval_condition_refines hst hst' ge sp cond args rs m:
+  hsi_smem_get hst = hsi_smem_get hst' ->
+  seval_condition ge sp cond args (si_smem hst) rs m = seval_condition ge sp cond args (si_smem hst') rs m. *)
+
+
+Lemma seval_condition_refines hst st ge sp cond args rs m:
+  hsistate_local_refines 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.
+
+Lemma hsiexit_simub_correct dm f hse1 hse2:
+  hsiexit_simub dm f hse1 hse2 = OK tt ->
+  hsiexit_simu dm f hse1 hse2.
+Proof.
+  unfold hsiexit_simub. intro. explore.
+  apply list_sval_simub_correct in EQ0. exploit hsilocal_simub_eq; eauto.
+  intros (SREGEQ & SMEMEQ).
+  apply hsilocal_simub_correct in EQ2.
+  apply revmap_check_single_correct in EQ3.
+  intros se1 se2 HEREF1 HEREF2.
+  destruct HEREF1 as (HCOND1 & HARGS1 & HLREF1 & HIFSO1).
+  destruct HEREF2 as (HCOND2 & HARGS2 & HLREF2 & HIFSO2).
+  constructor.
+  - unfold siexit_simu_ssem. intros sp ge ge' GFS LOK rs m is SEMEXIT.
+    destruct SEMEXIT as (SCOND & SLOCAL & SIFSO).
+    let H0 := fresh "SLOCAL" in assert (H0 := SLOCAL).
+    eapply EQ2 in SLOCAL0; eauto. destruct SLOCAL0 as (is2 & SLOCAL' & ISIMU).
+    destruct is2 as [icont ipc irs imem]. simpl in *.
+    exists (mk_istate icont (si_ifso se2) irs imem). simpl.
+    constructor; auto.
+    + repeat (constructor; auto).
+      rewrite <- HARGS2. rewrite <- EQ0.
+      rewrite <- HCOND2. rewrite <- e.
+      erewrite <- seval_condition_refines; eauto. rewrite <- SMEMEQ.
+      rewrite HARGS1. rewrite HCOND1. erewrite seval_condition_refines; eauto.
+      erewrite seval_condition_preserved; eauto.
+    + unfold istate_simu in *. destruct (icontinue is) eqn:ICONT.
+      * destruct ISIMU as (A & B & C). constructor; auto.
+      * destruct ISIMU as (path & PATHEQ & ISIMU & REVEQ). exists path.
+        repeat (constructor; auto). simpl in *. congruence.
+  - unfold siexit_simu_cond. intros sp ge ge' GFS rs m. erewrite seval_condition_preserved; eauto.
+    rewrite <- HARGS2. rewrite <- HCOND2. erewrite <- seval_condition_refines; eauto.
+    rewrite <- HARGS1. rewrite <- HCOND1. erewrite <- seval_condition_refines; eauto.
+    congruence.
+Qed.
+
+Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
+  match lhse1 with
+  | nil =>
+      match lhse2 with
+      | nil => OK tt
+      | _ => Error (msg "siexists_simub: sle1 and sle2 lengths do not match")
+      end
+  | hse1 :: lhse1 =>
+      match lhse2 with
+      | nil => Error (msg "siexits_simub: sle1 and sle2 lengths do not match")
+      | hse2 :: lhse2 =>
+          do _ <- hsiexit_simub dm f hse1 hse2;
+          do _ <- hsiexits_simub dm f lhse1 lhse2;
+          OK tt
+      end
+  end.
+
+Definition hsiexits_simu dm f (hse1 hse2: list hsistate_exit): Prop := forall se1 se2,
+  list_forall2 hsistate_exit_refines hse1 se1 ->
+  list_forall2 hsistate_exit_refines hse2 se2 ->
+  siexits_simu dm f se1 se2.
+
+Lemma hsiexits_simub_correct dm f lhse1: forall lhse2,
+  hsiexits_simub dm f lhse1 lhse2 = OK tt ->
+  hsiexits_simu dm f lhse1 lhse2.
+Proof.
+  induction lhse1.
+  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREF1 HEREF2.
+    inv HEREF1. inv HEREF2. constructor.
+  - (* simpl. *) unfold hsiexits_simub. intros. destruct lhse2; try discriminate. explore.
+    fold hsiexits_simub in EQ1.
+    apply hsiexit_simub_correct in EQ. apply IHlhse1 in EQ1.
+    intros se1 se2 HEREF1 HEREF2. inv HEREF1. inv HEREF2. constructor; auto.
+    apply EQ1; assumption.
+Qed.
+
+Definition hsistate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
+  do _ <- hsilocal_simub dm f (hsi_local hst1) (hsi_local hst2);
+  do _ <- hsiexits_simub dm f (hsi_exits hst1) (hsi_exits hst2);
+  OK tt.
+
+Definition hsistate_simu dm f (hst1 hst2: hsistate): Prop := forall st1 st2,
+  hsistate_refines hst1 st1 ->
+  hsistate_refines hst2 st2 ->
+  sistate_simu dm f st1 st2.
+
+(* Very adapted from sistate_simub_correct ---> should delete sistate_simub_correct after *)
+Lemma hsistate_simub_correct dm f hst1 hst2:
+  hsistate_simub dm f hst1 hst2 = OK tt ->
+  hsistate_simu f dm hst1 hst2.
+Proof.
+  unfold hsistate_simub. intro. explore. unfold hsistate_simu.
+  intros st1 st2 HREF1 HREF2 sp ge1 ge2 GFS LOK rs m is1 SEMI.
+  destruct HREF1 as (PCEQ1 & HEREF1 & HLREF1). destruct HREF2 as (PCEQ2 & HEREF2 & HLREF2).
+  exploit hsiexits_simub_correct; eauto. intro ESIMU.
+  unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
+  - destruct SEMI as (SSEML & PCEQ & ALLFU).
+    exploit silocal_simub_correct; eauto. intros (is2 & SSEML' & ISIMU).
+    destruct is2 as [icont2 ipc2 irs2 imem2]. simpl in *.
+    exists (mk_istate icont2 (si_pc st2) irs2 imem2). constructor; auto.
+    + unfold ssem_internal. simpl.
+      unfold istate_simu in ISIMU. rewrite ICONT in ISIMU.
+      destruct ISIMU as (CONTEQ & RSEQ & MEMEQ). simpl in *.
+      rewrite <- CONTEQ. rewrite ICONT.
+      constructor; [|constructor]; [eassumption | auto | eapply siexits_simu_all_fallthrough; eauto].
+    + unfold istate_simu in *; simpl in *. rewrite ICONT in ISIMU. rewrite ICONT.
+      destruct ISIMU as (A & B & C). simpl in *. constructor; auto.
+  - destruct SEMI as (ext & lx & SSEME & ALLFU).
+    exploit siexits_simu_all_fallthrough_upto; eauto. intros (ext2 & lx2 & ALLFU2 & LENEQ).
+    assert (EXTSIMU: siexit_simu dm f 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 (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).
+    destruct SIMULIVE as (CONTEQ & REGLIVE & MEMEQ).
+    unfold ssem_internal. exists is2.
+    rewrite <- CONTEQ. rewrite ICONT. constructor; auto.
+    + eexists; eexists; constructor; eauto.
+    + unfold istate_simu. rewrite ICONT. eexists. repeat (constructor; eauto).
+  Unshelve. apply dm. (* Very weird to have this *)
 Qed.
-*)
 
 Definition hsstate_simu dm f (hst1 hst2: hsstate): Prop :=
   forall st1 st2,
   (* CS: this hypothesis is not needed? *)
 (*   (forall s : ident, Genv.find_symbol ge2 s = Genv.find_symbol ge1 s) -> *)
   hsstate_refines hst1 st1 ->
-  hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2.
+  hsstate_refines hst2 st2 -> sstate_simu f dm st1 st2.
 
-Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := OK tt. (* TODO *)
+Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
+  do u1 <- hsistate_simub dm f (hinternal hst1) (hinternal hst2);
+  do u2 <- sfval_simub dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2);
+  OK tt.
 
 Lemma hsstate_simub_correct dm f hst1 hst2:
   hsstate_simub dm f hst1 hst2 = OK tt ->
-  hsstate_simu dm f hst1 hst2.
+  hsstate_simu f dm hst1 hst2.
 Proof.
-Admitted.
-
-(* SB: Hum, le "exists st2" ne me plaît pas du tout ici...
-Definition hsexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop :=
-    forall hst1, hsexec f1 pc1 = Some hst1 -> 
-    exists hst2, hsexec f2 pc2 = Some hst2 /\ hsstate_simu dm f1 hst1 hst2.
-
-
-Lemma hsexec_sexec_simu dm f1 f2 pc1 pc2 hst1 hst2:
-  hsexec f1 pc1 = Some hst1 ->
-  hsexec f2 pc2 = Some hst2 ->
-  hsstate_simu dm f1 hst1 hst2 -> sexec_simu dm f1 f2 pc1 pc2.
-Proof.
-  intros HSEXEC1 HSEXEC2 HESIMU.
-  eapply HESIMU in HSEXEC. destruct HSEXEC as (hst' & HSEXEC' & HSSIMU).
-  eapply HSSIMU in HREF. destruct HREF as (st' & HREF' & SSIMU).
-  eapply hsexec_correct in HSEXEC'; eauto.
+  unfold hsstate_simub. intro. explore.
+  apply sfval_simub_correct in EQ1. apply hsistate_simub_correct in EQ.
+  intros st1 st2 (LREF & FREF) (LREF' & FREF').
+  constructor; [auto|].
+  destruct LREF as (PCEQ & _ & _). destruct LREF' as (PCEQ' & _ & _).
+  rewrite <- PCEQ. rewrite <- PCEQ'. rewrite <- FREF. rewrite <- FREF'.
+  assumption.
+  (* FIXME - that proof will have to be changed once hfinal_refines is more complex *)
 Qed.
-*)
 
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node) :=
   let (pc2, pc1) := m in
diff --git a/kvx/lib/RTLpathSchedulerproof.v b/kvx/lib/RTLpathSchedulerproof.v
index 0e55dc6b..1e8adc71 100644
--- a/kvx/lib/RTLpathSchedulerproof.v
+++ b/kvx/lib/RTLpathSchedulerproof.v
@@ -173,8 +173,8 @@ Lemma ssem_final_simu dm f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s:
   list_forall2 match_stackframes stk stk' ->
   (* s_istate_simu f dupmap st st' -> *)
   sfval_simu dm f st.(si_pc) st'.(si_pc) sv sv' ->
-  ssem_final pge ge sp st stk f rs0 m0 sv rs m t s ->
-  exists s', ssem_final tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
+  ssem_final pge ge sp st.(si_pc) stk f rs0 m0 sv rs m t s ->
+  exists s', ssem_final tpge tge sp st'.(si_pc) stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
 Proof.
   Local Hint Resolve transf_fundef_correct: core.
   intros FUN LIVE STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl.