path: root/scheduling/RTLpathSE_simu_specs.v

(** Low-level specifications of the simulation tests by symbolic execution with hash-consing *)

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL RTLpath.
Require Import Errors.
Require Import RTLpathSE_theory RTLpathLivegenproof.
Require Import Axioms.
Require Import Lia.

Local Open Scope error_monad_scope.
Local Open Scope option_monad_scope.

Require Export Impure.ImpHCons.
Import HConsing.

Import ListNotations.
Local Open Scope list_scope.

(** * Auxilary notions on simulation tests *)

Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) outframe (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop :=
    forall is1, ssem_local (the_ge1 ctx) (the_sp ctx) sl1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) ->
    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 outframe is1 is2.

(* a kind of 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) outframe (ctx: simu_proof_context f) (se1 se2: sistate_exit) :=
  (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) ->
      exists is2,
          ssem_exit (the_ge2 ctx) (the_sp ctx) se2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) (ipc is2)
      /\  istate_simu f dm outframe is1 is2.

Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) outframe (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) :=
  list_forall2 (siexit_simu dm f outframe ctx) lse1 lse2.


(** * Implementation of Data-structure use in Hash-consing *)

(** ** Implementation of symbolic values/symbolic memories with hash-consing data *)

Inductive hsval :=
  | HSinput (r: reg) (hid: hashcode)
  | HSop (op: operation) (lhsv: list_hsval) (hid: hashcode) (** NB: does not depend on the memory ! *)
  | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode)
with list_hsval :=
  | HSnil (hid: hashcode)
  | HScons (hsv: hsval) (lhsv: list_hsval) (hid: hashcode)
with hsmem :=
  | HSinit (hid: hashcode)
  | HSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval) (hid:hashcode).

Scheme hsval_mut := Induction for hsval Sort Prop
with list_hsval_mut := Induction for list_hsval Sort Prop
with hsmem_mut := Induction for hsmem Sort Prop.



(** Symbolic final value -- from hash-consed values
  It does not seem useful to hash-consed these final values (because they are final).
*)
Inductive hsfval :=
  | HSnone
  | HScall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) (res: reg) (pc: node)
  | HStailcall (sig: signature) (svos: hsval + ident) (lsv: list_hsval)
  | HSbuiltin (ef: external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc: node)
  | HSjumptable (sv: hsval) (tbl: list node)
  | HSreturn (res: option hsval)
.

(** * gives the semantics of hash-consed symbolic values *)
Fixpoint hsval_proj hsv :=
  match hsv with
  | HSinput r _ => Sinput r
  | HSop op hl _ => Sop op (hsval_list_proj hl) Sinit (** NB: use the initial memory of the path ! *)
  | HSload hm t chk addr hl _ => Sload (hsmem_proj hm) t chk addr (hsval_list_proj hl)
  end
with hsval_list_proj hl :=
  match hl with
  | HSnil _ => Snil
  | HScons hv hl _ => Scons (hsval_proj hv) (hsval_list_proj hl)
  end
with hsmem_proj hm :=
  match hm with
  | HSinit _ => Sinit
  | HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv)
  end.

(** We use a Notation instead a Definition, in order to get more automation "for free" *)
Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv))
  (only parsing, at level 0, ge at next level, sp at next level, hsv at next level): hse.

Local Open Scope hse.

Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv))
  (only parsing, at level 0, ge at next level, sp at next level, lhv at next level): hse.
Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm))
  (only parsing, at level 0, ge at next level, sp at next level, hsm at next level): hse.

Notation "'sval_refines' ge sp rs0 m0 hv sv" := (seval_hsval ge sp hv rs0 m0 = seval_sval ge sp sv rs0 m0)
  (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hv at next level, sv at next level): hse.
Notation "'list_sval_refines' ge sp rs0 m0 lhv lsv" := (seval_list_hsval ge sp lhv rs0 m0 = seval_list_sval ge sp lsv rs0 m0)
  (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, lhv at next level, lsv at next level): hse.
Notation "'smem_refines' ge sp rs0 m0 hm sm" := (seval_hsmem ge sp hm rs0 m0 = seval_smem ge sp sm rs0 m0)
  (only parsing, at level 0, ge at next level, sp at next level, rs0 at next level, m0 at next level, hm at next level, sm at next level): hse.


(** ** Implementation of symbolic states (with hash-consing) *)

(** *** Syntax and semantics of symbolic internal local states 

The semantics is given by the refinement relation [hsilocal_refines] wrt to (abstract) symbolic internal local states

*)

(* NB: "h" stands for hash-consing *)
Record hsistate_local := 
  { 
    (** [hsi_smem] represents the current smem symbolic evaluations.
        (we also recover the history of smem in hsi_smem)  *)
    hsi_smem:> hsmem;
    (** For the values in registers:
        1) we store a list of sval evaluations
        2) we encode the symbolic regset by a PTree *)
    hsi_ok_lsval: list hsval;
    hsi_sreg:> PTree.t hsval
  }.

Definition hsi_sreg_proj (hst: PTree.t hsval) r: sval :=
   match PTree.get r hst with
   | None => Sinput r
   | Some hsv => hsval_proj hsv
   end.

Definition hsi_sreg_eval ge sp hst r := seval_sval ge sp (hsi_sreg_proj hst r).

Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
     (forall hsv, List.In hsv (hsi_ok_lsval hst) -> seval_hsval ge sp hsv rs0 m0 <> None)
  /\ (seval_hsmem ge sp (hst.(hsi_smem)) rs0 m0 <> None).

(* refinement link between a (st: sistate_local) and (hst: hsistate_local) *)
Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) :=
      (sok_local ge sp rs0 m0 st <-> hsok_local ge sp rs0 m0 hst)
  /\  (hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 (hsi_smem hst) (st.(si_smem)))
  /\  (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0)
  /\  (* the below invariant allows to evaluate operations in the initial memory of the path instead of the current memory *)
      (forall m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
  .

(** *** Syntax and semantics of symbolic exit states *)
Record hsistate_exit := mk_hsistate_exit
  { hsi_cond: condition; hsi_scondargs: list_hsval; hsi_elocal: hsistate_local; hsi_ifso: node }.

(** 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_ifso hext = si_ifso ext.

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)
   /\ (hsok_local ge sp rs0 m0 (hsi_elocal hext) ->
        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 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.


(** *** Syntax and Semantics of symbolic internal state *)

Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }.

(* expresses the "monotony" of sok_local along sequences *)
Inductive nested_sok ge sp rs0 m0: sistate_local -> list sistate_exit -> Prop :=
    nsok_nil st: nested_sok ge sp rs0 m0 st nil
  | nsok_cons st se lse:
     (sok_local ge sp rs0 m0 st -> sok_local ge sp rs0 m0 (si_elocal se)) ->
     nested_sok ge sp rs0 m0 (si_elocal se) lse ->
     nested_sok ge sp rs0 m0 st (se::lse).

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.

Lemma nested_sok_elocal ge sp rs0 m0 st2 exits:
  nested_sok ge sp rs0 m0 st2 exits ->
  forall st1, (sok_local ge sp rs0 m0 st1 -> sok_local ge sp rs0 m0 st2) ->
  nested_sok ge sp rs0 m0 st1 exits.
Proof.
  induction 1; [intros; constructor|].
  intros. constructor; auto.
Qed.

Lemma nested_sok_tail ge sp rs0 m0 st lx exits:
  is_tail lx exits ->
  nested_sok ge sp rs0 m0 st exits ->
  nested_sok ge sp rs0 m0 st lx.
Proof.
  induction 1; [auto|].
  intros. inv H0. eapply IHis_tail. eapply nested_sok_elocal; eauto.
Qed.

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)
  /\ nested_sok ge sp rs0 m0 (si_local st) (si_exits st) (* invariant necessary to prove "monotony" of sok_local along execution *)
  .

(** *** Syntax and Semantics of symbolic state *)

Definition hfinal_proj (hfv: hsfval) : sfval := 
  match hfv with
  | HSnone => Snone
  | HScall s hvi hlv r pc => Scall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv) r pc
  | HStailcall s hvi hlv => Stailcall s (sum_left_map hsval_proj hvi) (hsval_list_proj hlv)
  | HSbuiltin ef lbh br pc => Sbuiltin ef (List.map (builtin_arg_map hsval_proj) lbh) br pc
  | HSjumptable hv ln => Sjumptable (hsval_proj hv) ln
  | HSreturn oh => Sreturn (option_map hsval_proj oh)
  end.

Section HFINAL_REFINES.

Variable ge: RTL.genv.
Variable sp: val.
Variable rs0: regset.
Variable m0: mem.

Definition option_refines (ohsv: option hsval) (osv: option sval) :=
  match ohsv, osv with
  | Some hsv, Some sv => sval_refines ge sp rs0 m0 hsv sv
  | None, None => True
  | _, _ => False
  end.

Definition sum_refines (hsi: hsval + ident) (si: sval + ident) :=
  match hsi, si with
  | inl hv, inl sv => sval_refines ge sp rs0 m0 hv sv
  | inr id, inr id' => id = id'
  | _, _ => False
  end.

Definition bargs_refines (hargs: list (builtin_arg hsval)) (args: list (builtin_arg sval)): Prop :=
  seval_list_builtin_sval ge sp (List.map (builtin_arg_map hsval_proj) hargs) rs0 m0 = seval_list_builtin_sval ge sp args rs0 m0.

Inductive hfinal_refines: hsfval -> sfval -> Prop :=
  | hsnone_ref: hfinal_refines HSnone Snone
  | hscall_ref: forall hros ros hargs args s r pc,
      sum_refines hros ros ->
      list_sval_refines ge sp rs0 m0 hargs args ->
      hfinal_refines (HScall s hros hargs r pc) (Scall s ros args r pc)
  | hstailcall_ref: forall hros ros hargs args s,
      sum_refines hros ros ->
      list_sval_refines ge sp rs0 m0 hargs args ->
      hfinal_refines (HStailcall s hros hargs) (Stailcall s ros args)
  | hsbuiltin_ref: forall ef lbha lba br pc,
      bargs_refines lbha lba ->
      hfinal_refines (HSbuiltin ef lbha br pc) (Sbuiltin ef lba br pc)
  | hsjumptable_ref: forall hsv sv lpc,
      sval_refines ge sp rs0 m0 hsv sv -> hfinal_refines (HSjumptable hsv lpc) (Sjumptable sv lpc)
  | hsreturn_ref: forall ohsv osv,
      option_refines ohsv osv -> hfinal_refines (HSreturn ohsv) (Sreturn osv).

End HFINAL_REFINES.

(* TODO gourdinl Leave this here ? *)
Section FAKE_HSVAL.
(* BEGIN "fake" hsval without real hash-consing *)
(* TODO: 
  2) reuse these definitions in hSinput, hSop, etc 
     in order to factorize proofs ?
*)

Definition fSinput (r: reg): hsval :=
  HSinput r unknown_hid.

Lemma fSinput_correct r ge sp rs0 m0: (* useless trivial lemma ? *)
  sval_refines ge sp rs0 m0 (fSinput r) (Sinput r).
Proof.
  auto.
Qed.

Definition fSop (op:operation) (lhsv: list_hsval): hsval :=
   HSop op lhsv unknown_hid.

Lemma fSop_correct op lhsv ge sp rs0 m0 lsv sm m: forall
   (MEM: seval_smem ge sp sm rs0 m0 = Some m)
   (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
   (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
   sval_refines ge sp rs0 m0 (fSop op lhsv) (Sop op lsv sm).
Proof.
  intros; simpl. rewrite <- LR, MEM.
  destruct (seval_list_sval _ _ _ _); try congruence.
  eapply op_valid_pointer_eq; eauto.
Qed.

Definition fsi_sreg_get (hst: PTree.t hsval) r: hsval :=
   match PTree.get r hst with 
   | None => fSinput r
   | Some sv => sv
   end.

Lemma fsi_sreg_get_correct hst r ge sp rs0 m0 (f: reg -> sval): forall
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    sval_refines ge sp rs0 m0 (fsi_sreg_get hst r) (f r).
Proof.
   unfold hsi_sreg_eval, hsi_sreg_proj, fsi_sreg_get; intros; simpl.
   rewrite <- RR. destruct (hst ! r); simpl; auto.
Qed.

Definition fSnil: list_hsval :=
   HSnil unknown_hid.

(* TODO: Lemma fSnil_correct *)

Definition fScons (hsv: hsval) (lhsv: list_hsval): list_hsval :=
   HScons hsv lhsv unknown_hid.

(* TODO: Lemma fScons_correct *)

(* END "fake" hsval ... *)

End FAKE_HSVAL.


Record hsstate := { hinternal:> hsistate; hfinal: hsfval }.

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))
  /\ (forall ge sp rs0 m0, hsok_local ge sp rs0 m0 (hsi_local (hinternal hst)) -> hfinal_refines ge sp rs0 m0 (hfinal hst) (final st))
  .

(** * Intermediate specifications of the simulation tests *)

(** ** Specification of the simulation test on [hsistate_local].
       It is motivated by [hsilocal_simu_spec_correct theorem] below
*)
Definition hsilocal_simu_spec (alive: Regset.t) (hst1 hst2: hsistate_local) :=
     List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
  /\ (forall r, Regset.In r alive -> PTree.get r hst2 = PTree.get r hst1)
  /\ hsi_smem hst1 = hsi_smem hst2.

Definition seval_sval_partial ge sp rs0 m0 hsv :=
  match seval_hsval ge sp hsv rs0 m0 with
  | Some v => v
  | None => Vundef
  end.

Definition select_first (ox oy: option val) :=
  match ox with
  | Some v => Some v
  | None => oy
  end.

(** If the register was computed by hrs, evaluate the symbolic value from hrs.
    Else, take the value directly from rs0 *)
Definition seval_partial_regset ge sp rs0 m0 hrs :=
  let hrs_eval := PTree.map1 (seval_sval_partial ge sp rs0 m0) hrs in
  (fst rs0, PTree.combine select_first hrs_eval (snd rs0)).

Lemma seval_partial_regset_get ge sp rs0 m0 hrs r:
  (seval_partial_regset ge sp rs0 m0 hrs) # r =
  match (hrs ! r) with Some sv => seval_sval_partial ge sp rs0 m0 sv | None => (rs0 # r) end.
Proof.
  unfold seval_partial_regset. unfold Regmap.get. simpl.
  rewrite PTree.gcombine; [| simpl; reflexivity]. rewrite PTree.gmap1.
  destruct (hrs ! r); simpl; [reflexivity|].
  destruct ((snd rs0) ! r); reflexivity.
Qed.

Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m:
  ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst.
Proof.
  intros H0 (H1 & _ & _). apply H1. eapply ssem_local_sok. eauto.
Qed.

Lemma hsilocal_simu_spec_nofail ge1 ge2 of sp rs0 m0 hst1 hst2:
  hsilocal_simu_spec of hst1 hst2 ->
  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
  hsok_local ge1 sp rs0 m0 hst1 ->
  hsok_local ge2 sp rs0 m0 hst2.
Proof.
  intros (RSOK & _ & MEMOK) GFS (OKV & OKM). constructor.
  - intros sv INS. apply RSOK in INS. apply OKV in INS. erewrite seval_preserved; eauto.
  - erewrite MEMOK in OKM. erewrite smem_eval_preserved; eauto.
Qed.

Theorem hsilocal_simu_spec_correct hst1 hst2 alive ge1 ge2 sp rs0 m0 rs m st1 st2:
  hsilocal_simu_spec alive hst1 hst2 ->
  hsilocal_refines ge1 sp rs0 m0 hst1 st1 ->
  hsilocal_refines ge2 sp rs0 m0 hst2 st2 ->
  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
  ssem_local ge1 sp st1 rs0 m0 rs m ->
  let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2)
  in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'.
Proof.
  intros CORE HREF1 HREF2 GFS SEML.
  refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto.
  intro HOK1.
  refine (modusponens _ _ (hsilocal_simu_spec_nofail _ _ _ _ _ _ _ _ _ _ _) _); eauto.
  intro HOK2.
  destruct SEML as (PRE & MEMEQ & RSEQ).
  assert (SIPRE: si_pre st2 ge2 sp rs0 m0). { destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. }
  assert (SMEMEVAL: seval_smem ge2 sp (si_smem st2) rs0 m0 = Some m). {
    destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
    destruct CORE as (_ & _ & MEMEQ3).
    rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
    erewrite smem_eval_preserved; [| eapply GFS].
    rewrite MEMEQ1; auto. }
   constructor.
   + constructor; [assumption | constructor; [assumption|]].
      destruct HREF2 as (B & _ & A & _).
      (** B is used for the auto below. *)
      assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto.
      intro r. rewrite <- H. clear H. 
      generalize (A HOK2 r). unfold hsi_sreg_eval.
      rewrite seval_partial_regset_get.
      unfold hsi_sreg_proj.
      destruct (hst2 ! r) eqn:HST2; [| simpl; reflexivity].
      unfold seval_sval_partial. generalize HOK2; rewrite <- B; intros (_ & _ & C) D.
      assert (seval_sval ge2 sp (hsval_proj h) rs0 m0 <> None) by congruence.
      destruct (seval_sval ge2 sp _ rs0 m0); [reflexivity | contradiction].
    + intros r ALIVE. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
      destruct CORE as (_ & C & _). rewrite seval_partial_regset_get.
      assert (OPT: forall (x y: val), Some x = Some y -> x = y) by congruence.
      destruct (hst2 ! r) eqn:HST2; apply OPT; clear OPT.
      ++ unfold seval_sval_partial.
         assert (seval_sval ge2 sp (hsval_proj h) rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). {
           unfold hsi_sreg_eval, hsi_sreg_proj. rewrite HST2. reflexivity. }
         rewrite H. clear H. unfold hsi_sreg_eval, hsi_sreg_proj. rewrite C; [|assumption].
         erewrite seval_preserved; [| eapply GFS].
         unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; [|assumption]. rewrite RSEQ. reflexivity.
      ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval, hsi_sreg_proj.
         rewrite <- C; [|assumption]. rewrite HST2. reflexivity.
Qed.

(** ** Specification of the simulation test on [hsistate_exit].
       It is motivated by [hsiexit_simu_spec_correct theorem] below
*)
Definition hsiexit_simu_spec dm f (hse1 hse2: hsistate_exit) :=
  (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path
    /\ hsilocal_simu_spec 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.

Definition hsiexit_simu dm f outframe (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 outframe ctx se1 se2.

Lemma hsiexit_simu_spec_nofail dm f hse1 hse2 ge1 ge2 sp rs m:
  hsiexit_simu_spec dm f hse1 hse2 ->
  (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
  hsok_local ge1 sp rs m (hsi_elocal hse1) ->
  hsok_local ge2 sp rs m (hsi_elocal hse2).
Proof.
  intros CORE GFS HOK1.
  destruct CORE as ((p & _ & CORE') & _ & _ & _).
  eapply hsilocal_simu_spec_nofail; eauto.
Qed.

Theorem hsiexit_simu_spec_correct dm f outframe hse1 hse2 ctx:
  hsiexit_simu_spec dm f hse1 hse2 ->
  hsiexit_simu dm f outframe ctx hse1 hse2.
Proof.
  intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2.
  assert (SEVALC:
   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_spec_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 <- hseval_condition_preserved; eauto.
  }
  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_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (hsi_elocal hse1)). {
    destruct HDYN1 as (LREF & _). destruct LREF as (OKEQ & _ & _). rewrite <- OKEQ. assumption. }
  exploit hsiexit_simu_spec_nofail. 2: eapply ctx. all: eauto. intro HOK2.
  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_spec_correct; eauto; [apply ctx|]. simpl.
  intros (SSEML & EQREG).
  eexists (mk_istate (icontinue is1) (si_ifso st2) _ (imem is1)). simpl. constructor.
  - constructor; intuition congruence || eauto.
  - unfold istate_simu. rewrite ICONT.
    simpl. assert (PCEQ': hsi_ifso hse1 = ipc is1) by congruence.
    exists path. constructor; [|constructor]; [congruence| |congruence].
    constructor; [|constructor]; simpl; auto.
Qed.

Remark hsiexit_simu_siexit dm f outframe ctx hse1 hse2 se1 se2:
  hsiexit_simu dm f outframe 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 outframe ctx se1 se2.
Proof.
  auto.
Qed.

(** ** Specification of the simulation test on [list hsistate_exit].
       It is motivated by [hsiexit_simu_spec_correct theorem] below
*)

Definition hsiexits_simu dm f outframe (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop :=
  list_forall2 (hsiexit_simu dm f outframe ctx) lhse1 lhse2.

Definition hsiexits_simu_spec dm f lhse1 lhse2: Prop :=
  list_forall2 (hsiexit_simu_spec dm f) lhse1 lhse2.

Theorem hsiexits_simu_spec_correct dm f outframe lhse1 lhse2 ctx:
  hsiexits_simu_spec dm f lhse1 lhse2 ->
  hsiexits_simu dm f outframe ctx lhse1 lhse2.
Proof.
  induction 1; [constructor|].
  constructor; [|apply IHlist_forall2; assumption].
  apply hsiexit_simu_spec_correct; assumption.
Qed.


Lemma siexits_simu_all_fallthrough dm f outframe ctx: forall lse1 lse2,
  siexits_simu dm f outframe 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|]; 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.
  - intros; intuition.
Qed.


Lemma siexits_simu_all_fallthrough_upto dm f outframe ctx lse1 lse2:
  siexits_simu dm f outframe lse1 lse2 ctx ->
  forall ext1 lx1,
  (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
  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 ext lx1. intros OK H. destruct H as (ITAIL & ALLFU). eapply is_tail_false in ITAIL. contradiction.
  - simpl; intros ext lx1 OK 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.
      * intuition. apply OK. eassumption.
      * constructor; eauto.
      * intros (ext2 & lx2 & ALLFUE2 & LENEQ).
        eexists; eexists. constructor; eauto.
        eapply all_fallthrough_upto_exit_cons; eauto.
Qed.


Lemma hsiexits_simu_siexits dm f outframe ctx lhse1 lhse2:
  hsiexits_simu dm f outframe 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 outframe 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.


(** ** Specification of the simulation test on [hsistate].
       It is motivated by [hsistate_simu_spec_correct theorem] below
*)

Definition hsistate_simu_spec dm f outframe (hse1 hse2: hsistate) :=
     list_forall2 (hsiexit_simu_spec dm f) (hsi_exits hse1) (hsi_exits hse2)
  /\ hsilocal_simu_spec outframe (hsi_local hse1) (hsi_local hse2).

Definition hsistate_simu dm f outframe (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 outframe st1 st2 ctx.

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. lia.
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; lia). rewrite H. clear H.
    inv ITAIL.
    + assert (forall n, (n - n)%nat = 0%nat) by (intro; lia). 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; lia).
      exploit (is_tail_length (x::l1)); eauto. intro. simpl in H2.
      assert ((length l2 > length l1)%nat) by lia. clear H2.
      rewrite H0; auto.
Qed.

Theorem hsistate_simu_spec_correct dm f outframe hst1 hst2 ctx:
  hsistate_simu_spec dm f outframe hst1 hst2 ->
  hsistate_simu dm f outframe hst1 hst2 ctx.
Proof.
  intros (ESIMU & LSIMU) st1 st2 (PCREF1 & EREF1) (PCREF2 & EREF2) DREF1 DREF2 is1 SEMI.
  destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _).
  exploit hsiexits_simu_spec_correct; eauto. intro HESIMU.
  unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
  - destruct SEMI as (SSEML & PCEQ & ALLFU).
    exploit hsilocal_simu_spec_correct; eauto; [apply ctx|]. simpl. intro SSEML2.
    exists (mk_istate (icontinue is1) (si_pc st2) (seval_partial_regset (the_ge2 ctx) (the_sp ctx) 
              (the_rs0 ctx) (the_m0 ctx) (hsi_local hst2)) (imem is1)). constructor.
    + unfold ssem_internal. simpl. rewrite ICONT.
      destruct SSEML2 as [SSEMLP EQLIVE].
      constructor; [assumption | constructor; [reflexivity |]].
      eapply siexits_simu_all_fallthrough; eauto.
      * eapply hsiexits_simu_siexits; eauto.
      * eapply nested_sok_prop; eauto.
        eapply ssem_local_sok; eauto.
    + unfold istate_simu. rewrite ICONT.
      destruct SSEML2 as [SSEMLP EQLIVE].
      constructor; simpl; auto.
  - destruct SEMI as (ext & lx & SSEME & ALLFU).
    assert (SESIMU: siexits_simu dm f outframe (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
    exploit siexits_simu_all_fallthrough_upto; eauto.
    * destruct ALLFU as (ITAIL & ALLF).
      exploit nested_sok_tail; eauto. intros NESTED2.
      inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML.
      eapply nested_sok_prop; eauto.
    * intros (ext2 & lx2 & ALLFU2 & LENEQ).
      assert (EXTSIMU: siexit_simu dm f outframe 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.


(** ** Specification of the simulation test on [sfval].
       It is motivated by [hfinal_simu_spec_correct theorem] below
*)


Definition final_simu_spec (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_spec (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (hf1 hf2: hsfval): Prop :=
  final_simu_spec 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.

Lemma list_proj_refines_eq ge ge' sp rs0 m0 lsv lhsv:
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  list_sval_refines ge sp rs0 m0 lhsv lsv ->
  forall lhsv' lsv',
  list_sval_refines ge' sp rs0 m0 lhsv' lsv' ->
  hsval_list_proj lhsv = hsval_list_proj lhsv' ->
  seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0.
Proof.
  intros GFS H lhsv' lsv' H' H0.
  erewrite <- H, H0.
  erewrite list_sval_eval_preserved; eauto.
Qed.

Lemma seval_builtin_sval_preserved ge ge' sp sv rs0 m0:
   (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
   seval_builtin_sval ge sp sv rs0 m0 =
   seval_builtin_sval ge' sp sv rs0 m0.
Proof.
  induction sv; intro FIND; cbn.
  all: try (erewrite seval_preserved by eauto); trivial.
  all: erewrite IHsv1 by eauto; erewrite IHsv2 by eauto; reflexivity.
Qed.

Lemma seval_list_builtin_sval_preserved ge ge' sp lsv rs0 m0:
   (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) ->
   seval_list_builtin_sval ge sp lsv rs0 m0 =
   seval_list_builtin_sval ge' sp lsv rs0 m0.
Proof.
  induction lsv; intro FIND; cbn. { trivial. }
  erewrite seval_builtin_sval_preserved by eauto.
  erewrite IHlsv by eauto.
  reflexivity.
Qed.                              

Lemma barg_proj_refines_eq ge ge' sp rs0 m0:
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  forall lhsv lsv, bargs_refines ge sp rs0 m0 lhsv lsv ->
  forall lhsv' lsv', bargs_refines ge' sp rs0 m0 lhsv' lsv' ->
  List.map (builtin_arg_map hsval_proj) lhsv = List.map (builtin_arg_map hsval_proj) lhsv' ->
  seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0.
Proof.
  unfold bargs_refines; intros GFS lhsv lsv H lhsv' lsv' H' H0.
  erewrite <- H, H0.
  erewrite seval_list_builtin_sval_preserved; eauto.
Qed.

Lemma sval_refines_proj ge ge' sp rs m hsv sv hsv' sv':
  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
  sval_refines ge sp rs m hsv sv ->
  sval_refines ge' sp rs m hsv' sv' ->
  hsval_proj hsv = hsval_proj hsv' ->
  seval_sval ge sp sv rs m = seval_sval ge' sp sv' rs m.
Proof.
  intros GFS REF REF' PROJ.
  rewrite <- REF, PROJ.
  erewrite <- seval_preserved; eauto.
Qed.

Theorem hfinal_simu_spec_correct dm f ctx opc1 opc2 hf1 hf2 f1 f2:
  hfinal_simu_spec dm f opc1 opc2 hf1 hf2 ->
  hfinal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf1 f1 ->
  hfinal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hf2 f2 ->
  sfval_simu dm f opc1 opc2 ctx f1 f2.
Proof.
  assert (GFS: forall s : ident, Genv.find_symbol (the_ge1 ctx) s = Genv.find_symbol (the_ge2 ctx) s) by apply ctx.
  intros CORE FREF1 FREF2.
  destruct hf1; inv FREF1.
  (* Snone *)
  - destruct hf2; try contradiction. inv FREF2.
    inv CORE. constructor. assumption.
  (* Scall *)
  - rename H5 into SREF1. rename H6 into LREF1.
    destruct hf2; try contradiction. inv FREF2.
    rename H5 into SREF2. rename H6 into LREF2.
    destruct CORE as (PCEQ & ? & ? & ? & ?). subst.
    rename H0 into SVOSEQ. rename H1 into LSVEQ.
    constructor; [assumption | |].
    + destruct svos.
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ.
        simpl in SREF1. simpl in SREF2.
        rewrite <- SREF1. rewrite <- SREF2.
        erewrite <- seval_preserved; [| eapply GFS]. congruence.
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ. congruence.
    + erewrite list_proj_refines_eq; eauto.
  (* Stailcall *)
  - rename H3 into SREF1. rename H4 into LREF1.
    destruct hf2; try (inv CORE; fail). inv FREF2.
    rename H4 into LREF2. rename H3 into SREF2.
    inv CORE. rename H1 into SVOSEQ. rename H2 into LSVEQ.
    constructor.
    + destruct svos. (** Copy-paste from Scall *)
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ.
        simpl in SREF1. simpl in SREF2.
        rewrite <- SREF1. rewrite <- SREF2.
        erewrite <- seval_preserved; [| eapply GFS]. congruence.
      * destruct svos0; try discriminate. destruct ros; try contradiction.
        destruct ros0; try contradiction. constructor.
        simpl in SVOSEQ. inv SVOSEQ. congruence.
    + erewrite list_proj_refines_eq; eauto.
  (* Sbuiltin *)
  - rename H4 into BREF1. destruct hf2; try (inv CORE; fail). inv FREF2.
    rename H4 into BREF2. inv CORE. destruct H0 as (? & ? & ?). subst.
    rename H into PCEQ. rename H1 into ARGSEQ. constructor; [assumption|].
    erewrite barg_proj_refines_eq; eauto. constructor.
  (* Sjumptable *)
  - rename H2 into SREF1. destruct hf2; try contradiction. inv FREF2.
    rename H2 into SREF2. destruct CORE as (A & B). constructor; [assumption|].
    erewrite sval_refines_proj; eauto.
  (* Sreturn *)
  - rename H0 into SREF1.
    destruct hf2; try discriminate. inv CORE.
    inv FREF2. destruct osv; destruct res; inv SREF1.
    + destruct res0; try discriminate. destruct osv0; inv H1.
      constructor. simpl in H0. inv H0. erewrite sval_refines_proj; eauto.
    + destruct res0; try discriminate. destruct osv0; inv H1. constructor.
Qed.


(** ** Specification of the simulation test on [hsstate].
       It is motivated by [hsstate_simu_spec_correct theorem] below
*)

Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) :=
     hsistate_simu_spec dm f outframe (hinternal hst1) (hinternal hst2)
  /\ hfinal_simu_spec dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2).

Definition hsstate_simu dm f outframe (hst1 hst2: hsstate) ctx: Prop :=
  forall st1 st2,
  hsstate_refines hst1 st1 ->
  hsstate_refines hst2 st2 -> sstate_simu dm f outframe st1 st2 ctx.

Theorem hsstate_simu_spec_correct dm f outframe ctx hst1 hst2:
  hsstate_simu_spec dm f outframe hst1 hst2 ->
  hsstate_simu dm f outframe hst1 hst2 ctx.
Proof.
  intros (SCORE & FSIMU) st1 st2 (SREF1 & DREF1 & FREF1) (SREF2 & DREF2 & FREF2).
  generalize SCORE. intro SIMU; eapply hsistate_simu_spec_correct in SIMU; eauto.
  constructor; auto.
  intros is1 SEM1 CONT1.
  unfold hsistate_simu in SIMU. exploit SIMU; clear SIMU; eauto.
  unfold istate_simu, ssem_internal in *; intros (is2 & SEM2 & SIMU).
  rewrite! CONT1 in *. destruct SIMU as (CONT2 & _).
  rewrite! CONT1, <- CONT2 in *.
  destruct SEM1 as (SEM1 & _ & _).
  destruct SEM2 as (SEM2 & _ & _).
  eapply hfinal_simu_spec_correct in FSIMU; eauto.
  - destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
    eapply FSIMU.
  - eapply FREF1. exploit DREF1. intros (_ & (OK & _) & _). rewrite <- OK. eapply ssem_local_sok; eauto.
  - eapply FREF2. exploit DREF2. intros (_ & (OK & _) & _). rewrite <- OK. eapply ssem_local_sok; eauto.
Qed.