diff options
Diffstat (limited to 'scheduling/RTLpathSE_simu_specs.v')
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 889 |
1 files changed, 889 insertions, 0 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v new file mode 100644 index 00000000..c9e272c0 --- /dev/null +++ b/scheduling/RTLpathSE_simu_specs.v @@ -0,0 +1,889 @@ +(** 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. + +Local Open Scope error_monad_scope. +Local Open Scope option_monad_scope. + +Require Export Impure.ImpHCons. + +Import ListNotations. +Local Open Scope list_scope. + +(** * Auxilary notions on simulation tests *) + +Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (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 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) (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 is1 is2. + +Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) := + list_forall2 (siexit_simu dm f 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. + +Declare Scope hse. +Local Open Scope hse. + + +(** 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. +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. + + +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 (oalive: option Regset.t) (hst1 hst2: hsistate_local) := + List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1) + /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> 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 of ge1 ge2 sp rs0 m0 rs m st1 st2: + hsilocal_simu_spec of 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 -> + match of with + | None => ssem_local ge2 sp st2 rs0 m0 rs m + | Some alive => + 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' + end. +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. } + destruct of as [alive |]. + - 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. + - constructor; [|constructor]. + + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2. + + 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. + + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _). + destruct CORE as (_ & C & _). rewrite <- A; auto. unfold hsi_sreg_eval, hsi_sreg_proj. + rewrite C; [|auto]. erewrite seval_preserved; [| eapply GFS]. + unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; auto. +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 (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. + +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_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 hse1 hse2 ctx: + hsiexit_simu_spec dm f hse1 hse2 -> + hsiexit_simu dm f 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 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. + +(** ** Specification of the simulation test on [list hsistate_exit]. + It is motivated by [hsiexit_simu_spec_correct theorem] below +*) + +Definition hsiexits_simu dm f (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop := + list_forall2 (hsiexit_simu dm f 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 lhse1 lhse2 ctx: + hsiexits_simu_spec dm f lhse1 lhse2 -> + hsiexits_simu dm f 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 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) -> + (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 ctx lse1 lse2: + siexits_simu dm f 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 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. + + +(** ** Specification of the simulation test on [hsistate]. + It is motivated by [hsistate_simu_spec_correct theorem] below +*) + +Definition hsistate_simu_spec dm f (hse1 hse2: hsistate) := + list_forall2 (hsiexit_simu_spec dm f) (hsi_exits hse1) (hsi_exits hse2) + /\ hsilocal_simu_spec None (hsi_local hse1) (hsi_local hse2). + +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 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_spec_correct dm f hst1 hst2 ctx: + hsistate_simu_spec dm f hst1 hst2 -> + hsistate_simu dm f 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) (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. + * eapply nested_sok_prop; eauto. + eapply ssem_local_sok; 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. + * 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 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) (hst1 hst2: hsstate) := + hsistate_simu_spec dm f (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 (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_spec_correct dm f ctx hst1 hst2: + hsstate_simu_spec dm f hst1 hst2 -> + hsstate_simu dm f 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. |