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.

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.

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)
  | 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.



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
  | 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.

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

Record hsistate_local :=
  {
    hsi_smem:> hsmem;
    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).

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)
  /\
      (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 }.

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.

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 }.

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).

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.

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.

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)
  .

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.

Section FAKE_HSVAL.

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

Lemma fSinput_correct r ge sp rs0 m0:
  sval_refines ge sp rs0 m0 (fSinput r) (Sinput r).

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).

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).

Definition fSnil: list_hsval :=
   HSnil unknown_hid.


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



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.

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.

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.

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.

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'.

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).

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.

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.

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.


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).


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.


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.

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.

Lemma is_tail_length {A} (l1 l2: list A):
  is_tail l1 l2 ->
  (length l1 <= length l2)%nat.

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.

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.

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
  | _ => 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.

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.

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.

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.

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.

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.

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.

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.