diff options
Diffstat (limited to 'scheduling/BTL_SEsimuref.v')
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 852 |
1 files changed, 852 insertions, 0 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v new file mode 100644 index 00000000..d47e53b8 --- /dev/null +++ b/scheduling/BTL_SEsimuref.v @@ -0,0 +1,852 @@ +(** Refinement of BTL_SEtheory data-structures + in order to introduce (and prove correct) a lower-level specification of the simulation test. +*) + +Require Import Coqlib Maps Floats. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import Op Registers. +Require Import RTL BTL OptionMonad BTL_SEtheory. + + +Local Open Scope option_monad_scope. + +(** * Refinement of data-structures and of the specification of the simulation test *) + +Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core. +Local Hint Constructors si_ok: core. + +(* NB: refinement of (symbolic) internal state *) +Record ristate := + { + (** [ris_smem] represents the current smem symbolic evaluations. + (we also recover the history of smem in ris_smem) *) + ris_smem:> smem; + (** For the values in registers: + 1) we store a list of sval evaluations + 2) we encode the symbolic regset by a PTree + a boolean indicating the default sval + See [ris_sreg_get] below. + *) + ris_input_init: bool; + ok_rsval: list sval; + ris_sreg:> PTree.t sval + }. + +Definition ris_sreg_get (ris: ristate) r: sval := + match PTree.get r ris with + | None => if ris_input_init ris then fSinput r else fSundef + | Some sv => sv + end. +Coercion ris_sreg_get: ristate >-> Funclass. + +Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate := + {| ris_smem := ris_smem ris; + ris_input_init := ris_input_init ris; + ok_rsval := ok_rsval ris; + ris_sreg := sreg |}. + +Lemma ris_sreg_set_access (ris: ristate) (sreg: PTree.t sval) r smem rsval: + {| ris_smem := smem; + ris_input_init := ris_input_init ris; + ok_rsval := rsval; + ris_sreg := sreg |} r = + ris_sreg_set ris sreg r. +Proof. + unfold ris_sreg_set, ris_sreg_get; simpl. + reflexivity. +Qed. + +Record ris_ok ctx (ris: ristate) : Prop := { + OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; + OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None +}. +Local Hint Resolve OK_RMEM OK_RREG: core. +Local Hint Constructors ris_ok: core. + +(** + NOTE that this refinement relation *cannot* be decomposed into a abstraction function of type + ristate -> sistate & an equivalence relation on istate. + + Indeed, any [sis] satisfies [forall ctx r, si_ok ctx sis -> eval_sval ctx (sis r) <> None]. + whereas this is generally not true for [ris] that [forall ctx r, ris_ok ctx ris -> eval_sval ctx (ris r) <> None], + except when, precisely, [ris_refines ris sis]. + + An alternative design enabling to define ris_refines as the composition of an equivalence on sistate + and a abstraction function would consist in constraining sistate with an additional [wf] field: + + Record sistate := + { si_pre: iblock_exec_context -> Prop; + si_sreg:> reg -> sval; + si_smem: smem; + si_wf: forall ctx, si_pre ctx -> si_smem <> None /\ forall r, si_sreg r <> None + }. + + Such a constraint should also appear in [ristate]. This is not clear whether this alternative design + would be really simpler. + +*) +Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := { + OK_EQUIV: si_ok ctx sis <-> ris_ok ctx ris; + MEM_EQ: ris_ok ctx ris -> eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(si_smem); + REG_EQ: ris_ok ctx ris -> forall r, eval_sval ctx (ris r) = eval_sval ctx (sis r) +}. +Local Hint Resolve OK_EQUIV MEM_EQ REG_EQ: core. +Local Hint Constructors ris_refines: core. + +Record ris_simu ris1 ris2: Prop := { + SIMU_FAILS: forall sv, List.In sv ris2.(ok_rsval) -> List.In sv ris1.(ok_rsval); + SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem); + SIMU_REG: forall r, ris1 r = ris2 r +}. +Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core. +Local Hint Constructors ris_simu: core. +Local Hint Resolve sge_match: core. + +Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2): + ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2. +Proof. + intros SIMU OK; econstructor; eauto. + - erewrite <- SIMU_MEM; eauto. + erewrite <- smem_eval_preserved; eauto. + - intros; erewrite <- eval_sval_preserved; eauto. +Qed. + +Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2: + ris_simu ris1 ris2 -> + ris_refines (bctx1 ctx) ris1 sis1 -> + ris_refines (bctx2 ctx) ris2 sis2 -> + sistate_simu ctx sis1 sis2. +Proof. + intros RIS REF1 REF2 rs m SEM. + exploit sem_si_ok; eauto. + erewrite OK_EQUIV; eauto. + intros ROK1. + exploit ris_simu_ok_preserv; eauto. + intros ROK2. generalize ROK2; erewrite <- OK_EQUIV; eauto. + intros SOK2. + destruct SEM as (PRE & SMEM & SREG). + unfold sem_sistate; intuition eauto. + + erewrite <- MEM_EQ, <- SIMU_MEM; eauto. + erewrite <- smem_eval_preserved; eauto. + erewrite MEM_EQ; eauto. + + erewrite <- REG_EQ, <- SIMU_REG; eauto. + erewrite <- eval_sval_preserved; eauto. + erewrite REG_EQ; eauto. +Qed. + +Inductive optrsv_refines ctx: (option sval) -> (option sval) -> Prop := + | RefSome rsv sv + (REF:eval_sval ctx rsv = eval_sval ctx sv) + :optrsv_refines ctx (Some rsv) (Some sv) + | RefNone: optrsv_refines ctx None None + . + +Inductive rsvident_refines ctx: (sval + ident) -> (sval + ident) -> Prop := + | RefLeft rsv sv + (REF:eval_sval ctx rsv = eval_sval ctx sv) + :rsvident_refines ctx (inl rsv) (inl sv) + | RefRight id1 id2 + (IDSIMU: id1 = id2) + :rsvident_refines ctx (inr id1) (inr id2) + . + +Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop := + eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args. + +Inductive rfv_refines ctx: sfval -> sfval -> Prop := + | RefGoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc) + | RefCall sig rvos ros rargs args r pc + (SV:rsvident_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + :rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc) + | RefTailcall sig rvos ros rargs args + (SV:rsvident_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + :rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args) + | RefBuiltin ef lbra lba br pc + (BARGS: bargs_refines ctx lbra lba) + :rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc) + | RefJumptable rsv sv lpc + (VAL: eval_sval ctx rsv = eval_sval ctx sv) + :rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc) + | RefReturn orsv osv + (OPT:optrsv_refines ctx orsv osv) + :rfv_refines ctx (Sreturn orsv) (Sreturn osv) +. + +Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2. + +Local Hint Resolve eval_sval_preserved list_sval_eval_preserved smem_eval_preserved eval_list_builtin_sval_preserved: core. + +Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2: + rfv_simu rfv1 rfv2 -> + rfv_refines (bctx1 ctx) rfv1 sfv1 -> + rfv_refines (bctx2 ctx) rfv2 sfv2 -> + sfv_simu ctx sfv1 sfv2. +Proof. + unfold rfv_simu; intros X REF1 REF2. subst. + unfold bctx2; destruct REF1; inv REF2; simpl; econstructor; eauto. + - (* call svid *) + inv SV; inv SV0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. + - (* call args *) + rewrite <- LIST, <- LIST0; eauto. + - (* taillcall svid *) + inv SV; inv SV0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. + - (* tailcall args *) + rewrite <- LIST, <- LIST0; eauto. + - (* builtin args *) + unfold bargs_refines, bargs_simu in *. + rewrite <- BARGS, <- BARGS0; eauto. + - rewrite <- VAL, <- VAL0; eauto. + - (* return *) + inv OPT; inv OPT0; econstructor; eauto. + rewrite <- REF, <- REF0; eauto. +Qed. + +(* refinement of (symbolic) state *) +Inductive rstate := + | Rfinal (ris: ristate) (rfv: sfval) + | Rcond (cond: condition) (rargs: list_sval) (rifso rifnot: rstate) + | Rabort + . + +Record routcome := rout { + _ris: ristate; + _rfv: sfval; +}. + +Fixpoint get_routcome ctx (rst:rstate): option routcome := + match rst with + | Rfinal ris rfv => Some (rout ris rfv) + | Rcond cond args ifso ifnot => + SOME b <- eval_scondition ctx cond args IN + get_routcome ctx (if b then ifso else ifnot) + | Rabort => None + end. + +Inductive rst_simu: rstate -> rstate -> Prop := + | Rfinal_simu ris1 ris2 rfv1 rfv2 + (RIS: ris_simu ris1 ris2) + (RFV: rfv_simu rfv1 rfv2) + : rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2) + | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2 + (IFSO: rst_simu rifso1 rifso2) + (IFNOT: rst_simu rifnot1 rifnot2) + : rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2) + | Rabort_simu: rst_simu Rabort Rabort +(* TODO: extension à voir dans un second temps ! + | Rcond_skip cond rargs rifso1 rifnot1 rst: + rst_simu rifso1 rst -> + rst_simu rifnot1 rst -> + rst_simu (Rcond cond rargs rifso1 rifnot1) rst +*) + . + +Lemma rst_simu_lroutcome rst1 rst2: + rst_simu rst1 rst2 -> + forall f1 f2 (ctx: simu_proof_context f1 f2) ris1 rfv1, + get_routcome (bctx1 ctx) rst1 = Some (rout ris1 rfv1) -> + exists ris2 rfv2, get_routcome (bctx2 ctx) rst2 = Some (rout ris2 rfv2) /\ ris_simu ris1 ris2 /\ rfv_simu rfv1 rfv2. +Proof. + induction 1; simpl; intros f1 f2 ctx lris1 lrfv1 ROUT; try_simplify_someHyps. + erewrite <- eval_scondition_preserved. + autodestruct. + destruct b; simpl; auto. +Qed. + +Inductive rst_refines ctx: rstate -> sstate -> Prop := + | Reffinal ris sis rfv sfv + (RIS: ris_refines ctx ris sis) + (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) + : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) + | Refcond rcond cond rargs args rifso rifnot ifso ifnot + (RCOND: eval_scondition ctx rcond rargs = eval_scondition ctx cond args) + (REFso: eval_scondition ctx rcond rargs = Some true -> rst_refines ctx rifso ifso) + (REFnot: eval_scondition ctx rcond rargs = Some false -> rst_refines ctx rifnot ifnot) + : rst_refines ctx (Rcond rcond rargs rifso rifnot) (Scond cond args ifso ifnot) + | Refabort + : rst_refines ctx Rabort Sabort + . + +Lemma rst_refines_outcome_up ctx rst st: + rst_refines ctx rst st -> + forall ris rfv, + get_routcome ctx rst = Some (rout ris rfv) -> + exists sis sfv, get_soutcome ctx st = Some (sout sis sfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv). +Proof. + induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps. + rewrite RCOND. + autodestruct. + destruct b; simpl; auto. +Qed. + +Lemma rst_refines_outcome_okpreserv ctx rst st: + rst_refines ctx rst st -> + forall sis sfv, + get_soutcome ctx st = Some (sout sis sfv) -> + exists ris rfv, get_routcome ctx rst = Some (rout ris rfv) /\ ris_refines ctx ris sis /\ (ris_ok ctx ris -> rfv_refines ctx rfv sfv). +Proof. + induction 1; simpl; intros lris lrfv ROUT; try_simplify_someHyps. + rewrite RCOND. + autodestruct. + destruct b; simpl; auto. +Qed. + +Local Hint Resolve ris_simu_correct rvf_simu_correct: core. + +Lemma rst_simu_correct f1 f2 (ctx: simu_proof_context f1 f2) rst1 rst2 st1 st2 + (SIMU: rst_simu rst1 rst2) + (REF1: forall sis sfv, get_soutcome (bctx1 ctx) st1 = Some (sout sis sfv) -> si_ok (bctx1 ctx) sis -> rst_refines (bctx1 ctx) rst1 st1) + (REF2: forall ris rfv, get_routcome (bctx2 ctx) rst2 = Some (rout ris rfv) -> ris_ok (bctx2 ctx) ris -> rst_refines (bctx2 ctx) rst2 st2) + :sstate_simu ctx st1 st2. +Proof. + intros sis1 sfv1 SOUT OK1. + exploit REF1; eauto. + clear REF1; intros REF1. + exploit rst_refines_outcome_okpreserv; eauto. clear REF1 SOUT. + intros (ris1 & rfv1 & ROUT1 & REFI1 & REFF1). + rewrite OK_EQUIV in OK1; eauto. + exploit REFF1; eauto. clear REFF1; intros REFF1. + exploit rst_simu_lroutcome; eauto. + intros (ris2 & rfv2 & ROUT2 & SIMUI & SIMUF). clear ROUT1. + exploit ris_simu_ok_preserv; eauto. + clear OK1. intros OK2. + exploit REF2; eauto. clear REF2; intros REF2. + exploit rst_refines_outcome_up; eauto. + intros (sis2 & sfv2 & SOUT & REFI2 & REFF2). + do 2 eexists; split; eauto. +Qed. + + +(** * Properties of the (abstract) operators involved in symbolic execution *) + +Lemma ok_set_mem ctx sm sis: + si_ok ctx (set_smem sm sis) + <-> (si_ok ctx sis /\ eval_smem ctx sm <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. + intuition eauto. +Qed. + +Lemma ok_set_sreg ctx r sv sis: + si_ok ctx (set_sreg r sv sis) + <-> (si_ok ctx sis /\ eval_sval ctx sv <> None). +Proof. + unfold set_sreg; split. + + intros [(SVAL & PRE) SMEM SREG]; simpl in *; split. + - econstructor; eauto. + intros r0; generalize (SREG r0); destruct (Pos.eq_dec r r0); try congruence. + - generalize (SREG r); destruct (Pos.eq_dec r r); try congruence. + + intros ([PRE SMEM SREG] & SVAL). + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. +Qed. + +Lemma si_ok_op_okpreserv ctx op args dest sis: si_ok ctx (sexec_op op args dest sis) -> si_ok ctx sis. +Proof. + unfold sexec_op. rewrite ok_set_sreg. intuition. +Qed. + +Lemma si_ok_load_okpreserv ctx chunk addr args dest sis trap: si_ok ctx (sexec_load trap chunk addr args dest sis) -> si_ok ctx sis. +Proof. + unfold sexec_load. rewrite ok_set_sreg. intuition. +Qed. + +Lemma si_ok_store_okpreserv ctx chunk addr args src sis: si_ok ctx (sexec_store chunk addr args src sis) -> si_ok ctx sis. +Proof. + unfold sexec_store. rewrite ok_set_mem. intuition. +Qed. + +Lemma si_ok_tr_okpreserv ctx fi sis: si_ok ctx (tr_sis (cf ctx) fi sis) -> si_ok ctx sis. +Proof. + unfold tr_sis. intros OK; inv OK. simpl in *. intuition. +Qed. + +(* These lemmas are very bad for eauto: we put them into a dedicated basis. *) +Local Hint Resolve si_ok_tr_okpreserv si_ok_op_okpreserv si_ok_load_okpreserv si_ok_store_okpreserv: sis_ok. + +Lemma sexec_rec_okpreserv ctx ib: + forall k + (CONT: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + sis lsis sfv + (SOUT: get_soutcome ctx (sexec_rec (cf ctx) ib sis k) = Some (sout lsis sfv)) + (OK: si_ok ctx lsis) + ,si_ok ctx sis. +Proof. + induction ib; simpl; try (autodestruct; simpl). + 1-6: try_simplify_someHyps; eauto with sis_ok. + - intros. eapply IHib1. 2-3: eauto. + eapply IHib2; eauto. + - intros k CONT sis lsis sfv. + do 2 autodestruct; eauto. +Qed. + +(* an alternative tr_sis *) + +Definition transfer_sis (inputs: list reg) (sis:sistate): sistate := + {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None); + si_sreg := transfer_sreg inputs sis; + si_smem := sis.(si_smem) |}. + +Lemma ok_transfer_sis ctx inputs sis: + si_ok ctx (transfer_sis inputs sis) + <-> (si_ok ctx sis). +Proof. + unfold transfer_sis. induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. congruence. + + split. + * destruct 1; econstructor; simpl in *; intuition eauto. + * intros X; generalize X. rewrite <- IHl in X; clear IHl. + intros [PRE SMEM SREG]. + econstructor; simpl; eauto. + intros r0; destruct (Pos.eq_dec r r0); try congruence. + intros H; eapply OK_SREG; eauto. +Qed. + +Definition alt_tr_sis := poly_tr (fun f tbl or => transfer_sis (Regset.elements (pre_inputs f tbl or))). + +Lemma tr_sis_alt_def f fi sis: + alt_tr_sis f fi sis = tr_sis f fi sis. +Proof. + unfold tr_sis, str_inputs. destruct fi; simpl; auto. +Qed. + + +(** * Refinement of the symbolic execution (e.g. refinement of [sexec] into [rexec]). + +TODO: Est-ce qu'on garde cette vision purement fonctionnelle de l'implementation ? +=> ça pourrait être pratique quand on va compliquer encore le vérificateur ! + +Du coup, on introduirait une version avec hash-consing qui serait en correspondance +pour une relation d'equivalence sur les ristate ? + +Attention toutefois, il est possible que certaines parties de l'execution soient pénibles à formuler +en programmation fonctionnelle pure (exemple: usage de l'égalité de pointeur comme test d'égalité rapide!) + + +*) + +Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core. + +Lemma eval_list_sval_refpreserv ctx args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + eval_list_sval ctx (list_sval_inj (map ris args)) = + eval_list_sval ctx (list_sval_inj (map (si_sreg sis) args)). +Proof. + intros REF OK. + induction args; simpl; eauto. + intros; erewrite REG_EQ, IHargs; eauto. +Qed. + +Local Hint Resolve eval_list_sval_refpreserv: core. + +Lemma eval_builtin_sval_refpreserv ctx arg ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + eval_builtin_sval ctx (builtin_arg_map ris arg) = eval_builtin_sval ctx (builtin_arg_map sis arg). +Proof. + intros REF OK; induction arg; simpl; eauto. + + erewrite REG_EQ; eauto. + + erewrite IHarg1, IHarg2; eauto. + + erewrite IHarg1, IHarg2; eauto. +Qed. + +Lemma bargs_refpreserv ctx args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + bargs_refines ctx (map (builtin_arg_map ris) args) (map (builtin_arg_map sis) args). +Proof. + unfold bargs_refines. intros REF OK. + induction args; simpl; eauto. + erewrite eval_builtin_sval_refpreserv, IHargs; eauto. +Qed. + +Local Hint Resolve bargs_refpreserv: core. + +Lemma exec_final_refpreserv ctx i ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + rfv_refines ctx (sexec_final_sfv i ris) (sexec_final_sfv i sis). +Proof. + destruct i; simpl; unfold sum_left_map; try autodestruct; eauto. +Qed. + +Definition ris_init: ristate := {| ris_smem:= fSinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. + +Lemma ris_init_correct ctx: + ris_refines ctx ris_init sis_init. +Proof. + unfold ris_init, sis_init; econstructor; simpl in *; eauto. + + split; destruct 1; econstructor; simpl in *; eauto. + congruence. + + destruct 1; simpl in *. unfold ris_sreg_get; simpl. + intros; rewrite PTree.gempty; eauto. +Qed. + +Definition rset_smem rm (ris:ristate): ristate := + {| ris_smem := rm; + ris_input_init := ris.(ris_input_init); + ok_rsval := ris.(ok_rsval); + ris_sreg:= ris.(ris_sreg) + |}. + +Lemma ok_rset_mem ctx rm (ris: ristate): + (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> + ris_ok ctx (rset_smem rm ris) + <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +Lemma rset_mem_correct ctx rm sm ris sis: + (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_smem ctx rm = eval_smem ctx sm) -> + ris_refines ctx (rset_smem rm ris) (set_smem sm sis). +Proof. + destruct 2; intros. + econstructor; eauto. + + rewrite ok_set_mem, ok_rset_mem; intuition congruence. + + rewrite ok_rset_mem; intuition eauto. + + rewrite ok_rset_mem; intuition eauto. +Qed. + +Definition rexec_store chunk addr args src ris: ristate := + let args := list_sval_inj (List.map (ris_sreg_get ris) args) in + let src := ris_sreg_get ris src in + let rm := fSstore ris.(ris_smem) chunk addr args src in + rset_smem rm ris. + +Lemma rexec_store_correct ctx chunk addr args src ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_store chunk addr args src ris) (sexec_store chunk addr args src sis). +Proof. + intros REF; eapply rset_mem_correct; simpl; eauto. + + intros X; rewrite X. repeat autodestruct; eauto. + + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ, REG_EQ; eauto. +Qed. + +(* TODO: reintroduire le "root_apply" ? *) + +Definition rset_sreg r rsv (ris:ristate): ristate := + {| ris_smem := ris.(ris_smem); + ris_input_init := ris.(ris_input_init); + ok_rsval := rsv::ris.(ok_rsval); (* TODO: A CHANGER ? *) + ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *) + |}. + +Lemma ok_rset_sreg ctx r rsv ris: + ris_ok ctx (rset_sreg r rsv ris) + <-> (ris_ok ctx ris /\ eval_sval ctx rsv <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. + intuition subst; eauto. + exploit OK_RREG; eauto. +Qed. + +Lemma rset_reg_correct ctx r rsv sv ris sis: + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) -> + ris_refines ctx (rset_sreg r rsv ris) (set_sreg r sv sis). +Proof. + destruct 1; intros. + econstructor; eauto. + + rewrite ok_set_sreg, ok_rset_sreg; intuition congruence. + + rewrite ok_rset_sreg; intuition eauto. + + rewrite ok_rset_sreg. intros; unfold rset_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto. + destruct (Pos.eq_dec _ _). + * subst; rewrite PTree.gss; eauto. + * rewrite PTree.gso; eauto. +Qed. + +Definition rexec_op op args dst (ris:ristate): ristate := + let args := list_sval_inj (List.map ris args) in + rset_sreg dst (fSop op args) ris. + +Lemma rexec_op_correct ctx op args dst ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_op op args dst ris) (sexec_op op args dst sis). +Proof. + intros REF; eapply rset_reg_correct; simpl; eauto. + intros OK; erewrite eval_list_sval_refpreserv; eauto. +Qed. + +Definition rexec_load trap chunk addr args dst (ris:ristate): ristate := + let args := list_sval_inj (List.map ris args) in + rset_sreg dst (fSload ris.(ris_smem) trap chunk addr args) ris. + +Lemma rexec_load_correct ctx trap chunk addr args dst ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (rexec_load trap chunk addr args dst ris) (sexec_load trap chunk addr args dst sis). +Proof. + intros REF; eapply rset_reg_correct; simpl; eauto. + intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto. +Qed. + +Lemma eval_scondition_refpreserv ctx cond args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + eval_scondition ctx cond (list_sval_inj (map ris args)) = eval_scondition ctx cond (list_sval_inj (map sis args)). +Proof. + intros; unfold eval_scondition. + erewrite eval_list_sval_refpreserv; eauto. +Qed. + + +(* transfer *) + +Definition rseto_sreg r rsv (ris:ristate): ristate := + {| ris_smem := ris.(ris_smem); + ris_input_init := ris.(ris_input_init); + ok_rsval := ris.(ok_rsval); + ris_sreg:= PTree.set r rsv ris.(ris_sreg) (* TODO: A CHANGER *) + |}. + +Lemma ok_rseto_sreg ctx r rsv ris: + ris_ok ctx (rseto_sreg r rsv ris) + <-> (ris_ok ctx ris). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +Lemma rseto_reg_correct ctx r rsv sv ris sis: + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_sval ctx rsv <> None) -> + (ris_ok ctx ris -> eval_sval ctx rsv = eval_sval ctx sv) -> + ris_refines ctx (rseto_sreg r rsv ris) (set_sreg r sv sis). +Proof. + destruct 1; intros. + econstructor; eauto. + + rewrite ok_set_sreg, ok_rseto_sreg; intuition congruence. + + rewrite ok_rseto_sreg; intuition eauto. + + rewrite ok_rseto_sreg. intros; unfold rseto_sreg, set_sreg, ris_sreg_get; simpl. intuition eauto. + destruct (Pos.eq_dec _ _). + * subst; rewrite PTree.gss; eauto. + * rewrite PTree.gso; eauto. +Qed. + +Fixpoint transfer_ris (inputs: list reg) (ris:ristate): ristate := + match inputs with + | nil => {| ris_smem := ris.(ris_smem); + ris_input_init := false; + ok_rsval := ris.(ok_rsval); + ris_sreg:= PTree.empty _ + |} + | r::l => rseto_sreg r (ris_sreg_get ris r) (transfer_ris l ris) + end. + +Lemma ok_transfer_ris ctx inputs ris: + ris_ok ctx (transfer_ris inputs ris) + <-> (ris_ok ctx ris). +Proof. + induction inputs as [|r l]; simpl. + + split; destruct 1; econstructor; simpl in *; intuition eauto. + + rewrite ok_rseto_sreg. auto. +Qed. + +Lemma transfer_ris_correct ctx inputs ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (transfer_ris inputs ris) (transfer_sis inputs sis). +Proof. + destruct 1; intros. + induction inputs as [|r l]. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; simpl; unfold ris_sreg_get; simpl; eauto. + intros; rewrite PTree.gempty. simpl; auto. + + econstructor; eauto. + * erewrite ok_transfer_sis, ok_transfer_ris; eauto. + * erewrite ok_transfer_ris; simpl. + intros; erewrite MEM_EQ. 2: eauto. + - unfold transfer_sis; simpl; eauto. + - rewrite ok_transfer_ris; simpl; eauto. + * erewrite ok_transfer_ris; simpl. + intros H r0. + erewrite REG_EQ. 2: eapply rseto_reg_correct; eauto. + - unfold set_sreg; simpl; auto. + destruct (Pos.eq_dec _ _); simpl; auto. + - intros. rewrite REG_EQ0; auto. apply OK_SREG; tauto. + - rewrite ok_rseto_sreg, ok_transfer_ris. auto. +Qed. + +Definition tr_ris := poly_tr (fun f tbl or => transfer_ris (Regset.elements (pre_inputs f tbl or))). + +Local Hint Resolve transfer_ris_correct ok_transfer_ris: core. +Local Opaque transfer_ris. + +Lemma ok_tr_ris ctx fi ris: + ris_ok ctx (tr_ris (cf ctx) fi ris) + <-> (ris_ok ctx ris). +Proof. + destruct fi; simpl; eauto. +Qed. + +Lemma ris_ok_tr_okpreserv ctx fi ris: ris_ok ctx (tr_ris (cf ctx) fi ris) -> ris_ok ctx ris. +Proof. + rewrite ok_tr_ris; auto. +Qed. + +Lemma tr_ris_correct ctx fi ris sis: + ris_refines ctx ris sis -> + ris_refines ctx (tr_ris (cf ctx) fi ris) (tr_sis (cf ctx) fi sis). +Proof. + intros REF. rewrite <- tr_sis_alt_def. + destruct fi; simpl; eauto. +Qed. + +(** RAFFINEMENT EXEC SYMBOLIQUE **) + +Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate := + match ib with + | BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris) + (* basic instructions *) + | Bnop _ => k ris + | Bop op args res _ => k (rexec_op op args res ris) + | Bload trap chunk addr args dst _ => k (rexec_load trap chunk addr args dst ris) + | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris) + (* composed instructions *) + | Bseq ib1 ib2 => + rexec_rec f ib1 ris (fun ris2 => rexec_rec f ib2 ris2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map ris args) in + let ifso := rexec_rec f ifso ris k in + let ifnot := rexec_rec f ifnot ris k in + Rcond cond args ifso ifnot + end + . + +Definition rexec f ib := rexec_rec f ib ris_init (fun _ => Rabort). + + +Local Hint Resolve ris_init_correct exec_final_refpreserv tr_ris_correct ris_ok_tr_okpreserv + rexec_op_correct rexec_load_correct rexec_store_correct: core. + +Local Hint Constructors rst_refines: core. + +Lemma rexec_rec_correct1 ctx ib: + forall rk k + (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> si_ok ctx sis) + (CONT: forall ris sis lsis sfv st, ris_refines ctx ris sis -> k sis = st -> get_soutcome ctx (k sis) = Some (sout lsis sfv) -> si_ok ctx lsis -> rst_refines ctx (rk ris) (k sis)) + ris sis lsis sfv st + (REF: ris_refines ctx ris sis) + (EXEC: sexec_rec (cf ctx) ib sis k = st) + (SOUT: get_soutcome ctx st = Some (sout lsis sfv)) + (OK: si_ok ctx lsis) + , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st. +Proof. + induction ib; simpl; try (intros; subst; eauto; fail). + - (* seq *) + intros; subst. + eapply IHib1. 3-6: eauto. + + simpl. eapply sexec_rec_okpreserv; eauto. + + intros; subst. eapply IHib2; eauto. + - (* cond *) + intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. + assert (rOK: ris_ok ctx ris). { + erewrite <- OK_EQUIV. 2: eauto. + eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + generalize OUT; clear OUT; simpl. + autodestruct. + intros COND; generalize COND. + erewrite <- eval_scondition_refpreserv; eauto. + econstructor; try_simplify_someHyps. +Qed. + +Lemma rexec_correct1 ctx ib sis sfv: + get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) -> + (si_ok ctx sis) -> + rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). +Proof. + unfold sexec; intros; eapply rexec_rec_correct1; eauto; simpl; congruence. +Qed. + + +(** COPIER-COLLER ... Y a-t-il moyen de l'eviter ? **) + +Lemma ris_ok_op_okpreserv ctx op args dest ris: ris_ok ctx (rexec_op op args dest ris) -> ris_ok ctx ris. +Proof. + unfold rexec_op. rewrite ok_rset_sreg. intuition. +Qed. + +Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris trap: ris_ok ctx (rexec_load trap chunk addr args dest ris) -> ris_ok ctx ris. +Proof. + unfold rexec_load. rewrite ok_rset_sreg. intuition. +Qed. + +Lemma ris_ok_store_okpreserv ctx chunk addr args src ris: ris_ok ctx (rexec_store chunk addr args src ris) -> ris_ok ctx ris. +Proof. + unfold rexec_store. rewrite ok_rset_mem; simpl. + + intuition. + + intros X; rewrite X; simpl. + repeat autodestruct. +Qed. + +(* These lemmas are very bad for eauto: we put them into a dedicated basis. *) +Local Hint Resolve ris_ok_store_okpreserv ris_ok_op_okpreserv ris_ok_load_okpreserv: ris_ok. + +Lemma rexec_rec_okpreserv ctx ib: + forall k + (CONT: forall ris lris rfv, get_routcome ctx (k ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) + ris lris rfv + (ROUT: get_routcome ctx (rexec_rec (cf ctx) ib ris k) = Some (rout lris rfv)) + (OK: ris_ok ctx lris) + ,ris_ok ctx ris. +Proof. + induction ib; simpl; try (autodestruct; simpl). + 1-6: try_simplify_someHyps; eauto with ris_ok. + - intros. eapply IHib1. 2-3: eauto. + eapply IHib2; eauto. + - intros k CONT sis lsis sfv. + do 2 autodestruct; eauto. +Qed. + +Lemma rexec_rec_correct2 ctx ib: + forall rk k + (CONTh: forall ris lris rfv, get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> ris_ok ctx ris) + (CONT: forall ris sis lris rfv st, ris_refines ctx ris sis -> rk ris = st -> get_routcome ctx (rk ris) = Some (rout lris rfv) -> ris_ok ctx lris -> rst_refines ctx (rk ris) (k sis)) + ris sis lris rfv st + (REF: ris_refines ctx ris sis) + (EXEC: rexec_rec (cf ctx) ib ris rk = st) + (SOUT: get_routcome ctx st = Some (rout lris rfv)) + (OK: ris_ok ctx lris) + , rst_refines ctx st (sexec_rec (cf ctx) ib sis k). +Proof. + induction ib; simpl; try (intros; subst; eauto; fail). + - (* seq *) + intros; subst. + eapply IHib1. 3-6: eauto. + + simpl. eapply rexec_rec_okpreserv; eauto. + + intros; subst. eapply IHib2; eauto. + - (* cond *) + intros rk k CONTh CONT ris sis lsis sfv st REF EXEC OUT OK. subst. + assert (OK0: ris_ok ctx ris). { + eapply rexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto. + } + generalize OUT; clear OUT; simpl. + autodestruct. + intros COND; generalize COND. + erewrite eval_scondition_refpreserv; eauto. + econstructor; try_simplify_someHyps. +Qed. + +Lemma rexec_correct2 ctx ib ris rfv: + get_routcome ctx (rexec (cf ctx) ib) = Some (rout ris rfv) -> + (ris_ok ctx ris) -> + rst_refines ctx (rexec (cf ctx) ib) (sexec (cf ctx) ib). +Proof. + unfold rexec; intros; eapply rexec_rec_correct2; eauto; simpl; congruence. +Qed. + +Theorem rexec_simu_correct f1 f2 ib1 ib2: + rst_simu (rexec f1 ib1) (rexec f2 ib2) -> + symbolic_simu f1 f2 ib1 ib2. +Proof. + intros SIMU ctx. + eapply rst_simu_correct; eauto. + + intros; eapply rexec_correct1; eauto. + + intros; eapply rexec_correct2; eauto. +Qed. |