Avancement

1 files changed, 508 insertions, 11 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index dec7aa99..2a759ebb 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -600,7 +600,6 @@ Proof.
   - unfold hsi_sreg_eval. rewrite H. eapply hC_hsval_correct in Hexta1; [| simpl; eauto].
     simpl in Hexta1. unfold seval_hsval. rewrite <- Hexta1. simpl. reflexivity.
 Qed.
-Global Opaque hsi_sreg_get.
 Hint Resolve hsi_sreg_eval_correct: wlp.
 
 Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
@@ -619,11 +618,9 @@ Proof.
   intros H0 (H1 & _ & _). apply H1. eapply ssem_local_sok. eauto.
 Qed.
 
-Definition is_subset {A: Type} (lv2 lv1: list A) := forall v, In v lv2 -> In v lv1.
-
 Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
 (*      is_subset (hsi_lsmem hst2) (hsi_lsmem hst1) *)
-     is_subset (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
+     incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
   /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> hsi_sreg_get hst2 r = hsi_sreg_get hst1 r)
   /\ hsi_smem hst1 = hsi_smem hst2.
 
@@ -754,22 +751,157 @@ Proof.
       rewrite B; auto.
 Admitted. (** FIXME - requires to add some hypothesis that hsi_sreg_get may return something *)
 
-End CanonBuilding.
-
 Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
   phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
   PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2).
 
-Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit :=
-  DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";;
-  struct_check n res "revmap_check_single: n and res are physically different".
+Theorem hsilocal_simu_check_correct hst1 hst2:
+  WHEN hsilocal_simu_check hst1 hst2 ~> tt THEN
+  hsilocal_simu_core None hst1 hst2.
+Proof.
+  wlp_simplify. constructor; [|constructor]; [assumption | | congruence].
+  intros. unfold hsi_sreg_get. rewrite (PTree_eq_check_correct _ hst1 hst2); [|eassumption].
+  reflexivity.
+Qed.
+Hint Resolve hsilocal_simu_check_correct: wlp.
+Global Opaque hsilocal_simu_check.
 
 Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
   phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
   Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
   PTree_frame_eq_check frame (hsi_sreg hst1) (hsi_sreg hst2).
 
+Lemma setoid_in {A: Type} (a: A): forall l,
+  SetoidList.InA (fun x y => x = y) a l ->
+  In a l.
+Proof.
+  induction l; intros; inv H.
+  - constructor. reflexivity.
+  - right. auto.
+Qed.
+
+Lemma regset_elements_in r rs:
+  Regset.In r rs ->
+  In r (Regset.elements rs).
+Proof.
+  intros. exploit Regset.elements_1; eauto. intro SIN.
+  apply setoid_in. assumption.
+Qed.
+
+Theorem hsilocal_frame_simu_check_correct hst1 hst2 alive:
+  WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> tt THEN
+  hsilocal_simu_core (Some alive) hst1 hst2.
+Proof.
+  wlp_simplify. constructor; [|constructor]; [assumption | | congruence].
+  intros. unfold hsi_sreg_get.
+  rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ].
+  apply regset_elements_in. assumption.
+Qed.
+Hint Resolve hsilocal_frame_simu_check_correct: wlp.
+Global Opaque hsilocal_frame_simu_check.
+
+(** Simulation of exits *)
+
+Definition hsiexit_simu_core dm f (hse1 hse2: hsistate_exit) :=
+  (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path
+    /\ hsilocal_simu_core (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2))
+  /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1)
+  /\ hsi_cond hse1 = hsi_cond hse2
+  /\ hsi_scondargs hse1 = hsi_scondargs hse2 (* FIXME - should there be something about okvals ? *).
+
+(** NB: we split the refinement relation between a "static" part -- independendent of the initial context
+   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.
+
+Definition hsok_exit ge sp rs m hse := hsok_local ge sp rs m (hsi_elocal hse).
+
+Definition hseval_condition ge sp cond hcondargs hmem rs0 m0 :=
+  seval_condition ge sp cond (hsval_list_proj hcondargs) (hsmem_proj hmem) rs0 m0.
+
+Lemma hseval_condition_preserved ge ge' sp cond args mem rs0 m0:
+  (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
+  hseval_condition ge sp cond args mem rs0 m0 = hseval_condition ge' sp cond args mem rs0 m0.
+Proof.
+  intros. unfold hseval_condition. erewrite seval_condition_preserved; [|eapply H].
+  reflexivity.
+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.
+
+Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
+  hsiexit_refines_stat hse1 se1 ->
+  hsiexit_refines_stat hse2 se2 ->
+  hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
+  hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
+  siexit_simu dm f ctx se1 se2.
+
+Lemma hsiexit_simu_core_nofail dm f hse1 hse2 ge1 ge2 sp rs m:
+  hsiexit_simu_core dm f hse1 hse2 ->
+  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
+  hsok_exit ge1 sp rs m hse1 ->
+  hsok_exit ge2 sp rs m hse2.
+Proof.
+  intros CORE GFS HOK1.
+  destruct CORE as ((p & _ & CORE') & _ & _ & _).
+  eapply hsilocal_simu_core_nofail; eauto.
+Qed.
+
+Theorem hsiexit_simu_core_correct dm f hse1 hse2 ctx:
+  hsiexit_simu_core dm f hse1 hse2 ->
+  hsiexit_simu dm f ctx hse1 hse2.
+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.
+    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 (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. }
+  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 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].
+  - 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.
+Qed.
+
+Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2:
+  hsiexit_simu dm f ctx hse1 hse2 ->
+  hsiexit_refines_stat hse1 se1 ->
+  hsiexit_refines_stat hse2 se2 ->
+  hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
+  hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
+  siexit_simu dm f ctx se1 se2.
+Proof.
+  auto.
+Qed.
+
+Definition revmap_check_single (dm: PTree.t node) (n tn: node) : ?? unit :=
+  DO res <~ some_or_fail (dm ! tn) "revmap_check_single: no mapping for tn";;
+  struct_check n res "revmap_check_single: n and res are physically different".
+
 Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit): ?? unit :=
   struct_check (hsi_cond hse1) (hsi_cond hse2) "hsiexit_simu_check: conditions do not match";;
   phys_check (hsi_scondargs hse1) (hsi_scondargs hse2) "hsiexit_simu_check: args do not match";;
@@ -777,6 +909,37 @@ Definition hsiexit_simu_check (dm: PTree.t node) (f: RTLpath.function) (hse1 hse
   DO path <~ some_or_fail ((fn_path f) ! (hsi_ifso hse1)) "hsiexit_simu_check: internal error";;
   hsilocal_frame_simu_check (Regset.elements path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2).
 
+Theorem hsiexit_simu_check_correct dm f hse1 hse2:
+  WHEN hsiexit_simu_check dm f hse1 hse2 ~> tt THEN
+  hsiexit_simu_core dm f hse1 hse2.
+Proof.
+  wlp_simplify. constructor; [| constructor; [| constructor]]. 2-4: assumption.
+  exists a. constructor. 1-2: assumption.
+Qed.
+Hint Resolve hsiexit_simu_check_correct: wlp.
+Global Opaque hsiexit_simu_check.
+
+Definition hsiexits_simu dm f (ctx: simu_proof_context f) lhse1 lhse2: Prop :=
+  list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2.
+
+Definition hsiexits_simu_core dm f lhse1 lhse2: Prop :=
+  list_forall2 (hsiexit_simu_core dm f) lhse1 lhse2.
+
+Theorem hsiexits_simu_core_correct dm f lhse1 lhse2 ctx:
+  hsiexits_simu_core dm f lhse1 lhse2 ->
+  hsiexits_simu dm f ctx lhse1 lhse2.
+Proof.
+  induction 1; [constructor|].
+  constructor; [|apply IHlist_forall2; assumption].
+  apply hsiexit_simu_core_correct; assumption.
+Qed.
+
+Definition hsiexits_refines_stat lhse lse :=
+  list_forall2 hsiexit_refines_stat lhse lse.
+
+Definition hsiexits_refines_dyn ge sp rs0 m0 lhse se :=
+  list_forall2 (hsiexit_refines_dyn ge sp rs0 m0) lhse se.
+
 Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
   match lhse1,lhse2 with
   | nil, nil => RET tt
@@ -786,10 +949,294 @@ Fixpoint hsiexits_simu_check (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhs
   | _, _ => FAILWITH "siexists_simu_check:  lengths do not match"
   end.
 
+Theorem hsiexits_simu_check_correct dm f: forall le1 le2,
+  WHEN hsiexits_simu_check dm f le1 le2 ~> tt THEN
+  hsiexits_simu_core dm f le1 le2.
+Proof.
+  induction le1; intros; wlp_simplify.
+  - destruct le2; [constructor|]. simpl in Hexta. (* Absurd case *) admit.
+  - destruct le2.
+    + (* Absurd case again *) admit.
+    + assert (hsiexit_simu_check dm f a h ~~> tt /\ hsiexits_simu_check dm f le1 le2 ~~> exta). { admit. }
+      destruct H as (A & B). apply hsiexit_simu_check_correct in A.
+      constructor; [assumption|]. apply IHle1 in B. assumption.
+Admitted.
+Hint Resolve hsiexits_simu_check_correct: wlp.
+Global Opaque hsiexits_simu_check.
+
+Definition hsistate_simu_core dm f (hse1 hse2: hsistate) :=
+     dm ! (hsi_pc hse2) = Some (hsi_pc hse1)
+  /\ list_forall2 (hsiexit_simu_core dm f) (hsi_exits hse1) (hsi_exits hse2)
+  /\ hsilocal_simu_core None (hsi_local hse1) (hsi_local hse2).
+
+Definition hsistate_refines_stat (hst: hsistate) (st:sistate): Prop :=
+  hsi_pc hst = si_pc st
+  /\ hsiexits_refines_stat (hsi_exits hst) (si_exits st).
+
+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).
+
+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 ->
+  sistate_simu dm f st1 st2 ctx.
+
+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) ->
+  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).
+  apply IHlist_forall2 in ALLFU.
+  destruct H as (CONDSIMU & _).
+  inv INEXT; [|eauto].
+  erewrite <- CONDSIMU; eauto.
+Qed.
+
+Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2:
+  hsiexits_simu dm f ctx lhse1 lhse2 ->
+  forall lse1 lse2,
+  hsiexits_refines_stat lhse1 lse1 ->
+  hsiexits_refines_stat lhse2 lse2 ->
+  hsiexits_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 lse1 ->
+  hsiexits_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse2 lse2 ->
+  siexits_simu dm f lse1 lse2 ctx.
+Proof.
+  induction 1.
+  - intros. inv H. inv H0. constructor.
+  - intros lse1 lse2 SREF1 SREF2 DREF1 DREF2. inv SREF1. inv SREF2. inv DREF1. inv DREF2.
+    constructor; [| eapply IHlist_forall2; eauto].
+    eapply hsiexit_simu_siexit; eauto.
+Qed.
+
+Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2:
+  siexits_simu dm f lse1 lse2 ctx -> 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.
+    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.
+Qed.
+
+Lemma list_forall2_nth_error {A} (l1 l2: list A) P:
+  list_forall2 P l1 l2 ->
+  forall x1 x2 n,
+  nth_error l1 n = Some x1 ->
+  nth_error l2 n = Some x2 ->
+  P x1 x2.
+Proof.
+  induction 1.
+  - intros. rewrite nth_error_nil in H. discriminate.
+  - intros x1 x2 n. destruct n as [|n]; simpl.
+    + intros. inv H1. inv H2. assumption.
+    + apply IHlist_forall2.
+Qed.
+
+Lemma is_tail_length {A} (l1 l2: list A):
+  is_tail l1 l2 ->
+  (length l1 <= length l2)%nat.
+Proof.
+  induction l2.
+  - intro. destruct l1; auto. apply is_tail_false in H. contradiction.
+  - intros ITAIL. inv ITAIL; auto.
+    apply IHl2 in H1. clear IHl2. simpl. omega.
+Qed.
+
+Lemma is_tail_nth_error {A} (l1 l2: list A) x:
+  is_tail (x::l1) l2 ->
+  nth_error l2 ((length l2) - length l1 - 1) = Some x.
+Proof.
+  induction l2.
+  - intro ITAIL. apply is_tail_false in ITAIL. contradiction.
+  - intros ITAIL. assert (length (a::l2) = S (length l2)) by auto. rewrite H. clear H.
+    assert (forall n n', ((S n) - n' - 1)%nat = (n - n')%nat) by (intros; omega). rewrite H. clear H.
+    inv ITAIL.
+    + assert (forall n, (n - n)%nat = 0%nat) by (intro; omega). rewrite H.
+      simpl. reflexivity.
+    + exploit IHl2; eauto. intros. clear IHl2.
+      assert (forall n n', (n > n')%nat -> (n - n')%nat = S (n - n' - 1)%nat) by (intros; omega).
+      exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2.
+      assert ((length l2 > length l1)%nat) by omega. clear H2.
+      rewrite H0; auto.
+Qed.
+
+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.
+  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).
+  exploit hsiexits_simu_core_correct; eauto. intro HESIMU.
+  unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
+  - destruct SEMI as (SSEML & PCEQ & ALLFU).
+    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.
+    + 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).
+Qed.
+
 Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
+  revmap_check_single dm (hsi_pc hst1) (hsi_pc hst2);;
   hsilocal_simu_check (hsi_local hst1) (hsi_local hst2);;
   hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2).
 
+Theorem hsistate_simu_check_correct dm f hst1 hst2:
+  WHEN hsistate_simu_check dm f hst1 hst2 ~> tt THEN
+  hsistate_simu_core dm f hst1 hst2.
+Proof.
+  wlp_simplify.
+  constructor; [|constructor]. 1-3: assumption.
+Qed.
+Hint Resolve hsistate_simu_check_correct: wlp.
+Global Opaque hsistate_simu_check.
+
+Definition hsi_proj (hsi: hsval + ident) := match hsi with
+  | inl hv => inl (hsval_proj hv)
+  | inr id => inr id
+  end.
+
+Fixpoint barg_proj (bhv: builtin_arg hsval) := match bhv with
+  | BA hv => BA (hsval_proj hv)
+  | BA_splitlong ba1 ba2 => BA_splitlong (barg_proj ba1) (barg_proj ba2)
+  | BA_addptr ba1 ba2 => BA_addptr (barg_proj ba1) (barg_proj ba2)
+  | BA_int i => BA_int i
+  | BA_long i => BA_long i
+  | BA_float f => BA_float f
+  | BA_single f32 => BA_single f32
+  | BA_loadstack m p => BA_loadstack m p
+  | BA_addrstack p => BA_addrstack p
+  | BA_loadglobal c i p => BA_loadglobal c i p
+  | BA_addrglobal i p => BA_addrglobal i p
+  end.
+
+Fixpoint barg_list_proj lbh := match lbh with
+  | [] => []
+  | bh::lbh => (barg_proj bh) :: (barg_list_proj lbh)
+  end.
+
+Definition option_hsval_proj oh := match oh with None => None | Some h => Some (hsval_proj h) end.
+
+Definition hfinal_proj hfv := match hfv with
+  | HSnone => Snone
+  | HScall s hvi hlv r pc => Scall s (hsi_proj hvi) (hsval_list_proj hlv) r pc
+  | HStailcall s hvi hlv => Stailcall s (hsi_proj hvi) (hsval_list_proj hlv)
+  | HSbuiltin ef lbh br pc => Sbuiltin ef (barg_list_proj lbh) br pc
+  | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln
+  | HSreturn oh => Sreturn (option_hsval_proj oh)
+  end.
+
+Definition hfinal_refines (hfv: hsfval) (fv: sfval) := (hfinal_proj hfv) = fv.
+
+Remark hfinal_refines_snone: hfinal_refines HSnone Snone.
+Proof.
+  reflexivity.
+Qed.
+
+Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop :=
+  match f1 with
+  | Scall sig1 svos1 lsv1 res1 pc1 =>
+      match f2 with
+      | Scall sig2 svos2 lsv2 res2 pc2 =>
+          dm ! pc2 = Some pc1 /\ sig1 = sig2 /\ svos1 = svos2 /\ lsv1 = lsv2 /\ res1 = res2
+      | _ => False
+      end
+  | Sbuiltin ef1 lbs1 br1 pc1 =>
+      match f2 with
+      | Sbuiltin ef2 lbs2 br2 pc2 =>
+          dm ! pc2 = Some pc1 /\ ef1 = ef2 /\ lbs1 = lbs2 /\ br1 = br2
+      | _ => False
+      end
+  | Sjumptable sv1 lpc1 =>
+      match f2 with
+      | Sjumptable sv2 lpc2 =>
+          ptree_get_list dm lpc2 = Some lpc1 /\ sv1 = sv2
+      | _ => False
+      end
+  | Snone =>
+      match f2 with
+      | Snone => dm ! pc2 = Some pc1
+      | _ => False
+      end
+  (* Stailcall, Sreturn *)
+  | _ => f1 = f2
+  end.
+
+Definition hfinal_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (hf1 hf2: hsfval): Prop :=
+  final_simu_core dm f pc1 pc2 (hfinal_proj hf1) (hfinal_proj hf2).
+
+Lemma svident_simu_refl f ctx s:
+  svident_simu f ctx s s.
+Proof.
+  destruct s; constructor; [| reflexivity].
+  erewrite <- seval_preserved; [| eapply ctx]. constructor.
+Qed.
+
+Theorem hfinal_simu_core_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2:
+  hfinal_simu_core dm f opc1 opc2 hf1 hf2 ->
+  hfinal_refines hf1 f1 ->
+  hfinal_refines hf2 f2 ->
+  sfval_simu dm f opc1 opc2 ctx f1 f2.
+Proof.
+  intros CORE FREF1 FREF2.
+  rewrite <- FREF1. rewrite <- FREF2. clear FREF1. clear FREF2. (* FIXME - to change when the refinement is more complex *)
+  destruct hf1.
+  (* Snone *)
+  - destruct hf2; try contradiction. simpl. inv CORE. constructor. assumption.
+  (* Scall *)
+  - destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ? & ?). subst.
+    simpl. rewrite H0. rewrite H1. clear H0 H1.
+    constructor; [assumption | apply svident_simu_refl|].
+    erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor.
+  (* Stailcall *)
+  - rewrite <- CORE. constructor; [apply svident_simu_refl|].
+    erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor.
+  (* Sbuiltin *)
+  - destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ?). subst.
+    simpl. rewrite H0. clear H0.
+    constructor; [assumption | reflexivity].
+  (* Sjumptable *)
+  - destruct hf2; try contradiction. destruct CORE as (PCEQ & ?).
+    simpl. rewrite H. clear H. constructor; [assumption|].
+    erewrite <- seval_preserved; [| eapply ctx]. constructor.
+  (* Sreturn *)
+  - destruct hf2; inv CORE. simpl. rewrite H0. constructor.
+Qed.
+
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): ?? unit :=
   match ln, ln' with
   | nil, nil => RET tt
@@ -827,9 +1274,9 @@ Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
   | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch"
   end.
 
-Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (fv1 fv2: hsfval) :=
+Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (fv1 fv2: hsfval) :=
   match fv1, fv2 with
-  | HSnone, HSnone => revmap_check_single dm pc1 pc2
+  | HSnone, HSnone => revmap_check_single dm opc1 opc2
   | HScall sig1 svos1 lsv1 res1 pc1, HScall sig2 svos2 lsv2 res2 pc2 =>
       revmap_check_single dm pc1 pc2;;
       phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";;
@@ -853,10 +1300,58 @@ Definition sfval_simu_check (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: n
   | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
   end.
 
+Theorem sfval_simu_check_correct dm f opc1 opc2 fv1 fv2:
+  WHEN sfval_simu_check dm f opc1 opc2 fv1 fv2 ~> tt THEN
+  hfinal_simu_core dm f opc1 opc2 fv1 fv2.
+Proof.
+  wlp_simplify. destruct fv1. admit. (* needs to destruct fv2 and rule out the absurd cases *)
+Admitted.
+Hint Resolve sfval_simu_check_correct: wlp.
+Global Opaque hfinal_simu_core.
+
+Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
+   hsistate_refines_stat (hinternal hst) (internal st)
+  /\ (forall ge sp rs0 m0, hsistate_refines_dyn ge sp rs0 m0 (hinternal hst) (internal st))
+  /\ hfinal_refines (hfinal hst) (final st).
+
+Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
+     hsistate_simu_core dm f (hinternal hst1) (hinternal hst2)
+  /\ hfinal_simu_core dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2).
+
+Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
+  forall st1 st2,
+  hsstate_refines hst1 st1 ->
+  hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx.
+
+Theorem hsstate_simu_core_correct dm f ctx hst1 hst2:
+  hsstate_simu_core dm f hst1 hst2 ->
+  hsstate_simu dm f hst1 hst2 ctx.
+Proof.
+  intros (SCORE & FSIMU). intros st1 st2 HREF1 HREF2.
+  destruct HREF1 as (SREF1 & DREF1 & FREF1). destruct HREF2 as (SREF2 & DREF2 & FREF2).
+  assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE.
+  eapply hsistate_simu_core_correct in SCORE.
+  eapply hfinal_simu_core_correct in FSIMU; eauto.
+  constructor; [apply SCORE; auto|].
+  destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
+  eapply FSIMU.
+Qed.
+
 Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
   hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
   sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).
 
+Theorem hsstate_simu_check_correct dm f hst1 hst2:
+  WHEN hsstate_simu_check dm f hst1 hst2 ~> tt THEN
+  hsstate_simu_core dm f hst1 hst2.
+Proof.
+  wlp_simplify. constructor. 1-2: assumption.
+Qed.
+Hint Resolve hsstate_simu_check_correct: wlp.
+Global Opaque hsstate_simu_core.
+
+End CanonBuilding.
+
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
   let (pc2, pc1) := m in
   (* creating the hash-consing tables *)
@@ -873,6 +1368,8 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
 Lemma simu_check_single_correct dm tf f pc1 pc2:
   WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
   sexec_simu dm f tf pc1 pc2.
+Proof.
+  wlp_simplify. (* TODO *)
 Admitted.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.