Module BTL_SEsimuref

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 Classes.RelationClasses.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import OptionMonad BTL BTL_SEtheory.
Require Import ValueDomain.
Import ListNotations.
Import SvalNotations.
Import HConsing.

Local Open Scope option_monad_scope.
Local Open Scope lazy_bool_scope.

Local Hint Resolve OK_PRE OK_SMEM OK_SREG: core.
Local Hint Constructors sis_ok: core.

Inductive rrules_set: Type := RRexpansions | RRstrength | RRschedule (rel : bool) | RRnone.

parameters to control the symbolic execution

Record se_mode := {
se_abs_strict is true if we consider the semantics that checks that the addresses match their annotations (that is ctx_bc <> None)
  se_abs_strict: bool;
When se_ok_check is set, the check will imediatly fail instead of adding new values to ok_rsval.
  se_ok_check: bool;
}.

Definition ctx_se_mode (m : se_mode) (ctx : iblock_common_context) : Prop :=
  ctx_strict_reflect (ctx_bc ctx) (se_abs_strict m).

Definition se_mode_set_ok_check (m : se_mode) : se_mode :=
  {| se_abs_strict := se_abs_strict m;
     se_ok_check := true |}.

Getters and setters for hid

Definition sval_get_hid (sv: sval): hashcode :=
  match sv with
  | Sinput _ hid => hid
  | Sop _ _ hid => hid
  | Sfoldr _ _ _ hid => hid
  | Sload _ _ _ _ _ _ hid => hid
  end.

Definition list_sval_get_hid (lsv: list_sval): hashcode :=
  match lsv with
  | Snil hid => hid
  | Scons _ _ hid => hid
  end.

Definition smem_get_hid (sm: smem): hashcode :=
  match sm with
  | Sinit hid => hid
  | Sstore _ _ _ _ _ _ hid => hid
  end.

Definition sval_set_hid (sv: sval) (hid: hashcode): sval :=
  match sv with
  | Sinput r _ => Sinput r hid
  | Sop o lsv _ => Sop o lsv hid
  | Sfoldr op lsv sv0 _ => Sfoldr op lsv sv0 hid
  | Sload sm trap chunk addr lsv aaddr _ => Sload sm trap chunk addr lsv aaddr hid
  end.

Definition list_sval_set_hid (lsv: list_sval) (hid: hashcode): list_sval :=
  match lsv with
  | Snil _ => Snil hid
  | Scons sv lsv _ => Scons sv lsv hid
  end.

Definition smem_set_hid (sm: smem) (hid: hashcode): smem :=
  match sm with
  | Sinit _ => Sinit hid
  | Sstore sm chunk addr lsv sinfo srce _ => Sstore sm chunk addr lsv sinfo srce hid
  end.

Lemma sval_set_hid_correct ctx x y:
  sval_set_hid x unknown_hid = sval_set_hid y unknown_hid ->
  sval_equiv ctx x y.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Global Hint Resolve sval_set_hid_correct: core.

Lemma list_sval_set_hid_correct ctx x y:
  list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid ->
  list_sval_equiv ctx x y.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Global Hint Resolve list_sval_set_hid_correct: core.

Lemma smem_set_hid_correct ctx x y:
  smem_set_hid x unknown_hid = smem_set_hid y unknown_hid ->
  smem_equiv ctx x y.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Global Hint Resolve smem_set_hid_correct: core.

refined (symbolic) internal state and abstract operators over states


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 ok_rsval of sval evaluations 2) we encode the symbolic regset by a PTree ris_sreg_get + a boolean ris_input_init indicating the default option sval See ris_sreg_get below.
    ris_input_init: bool;
ok_rsval is a list of expresions that evaluate without error when ris_ok holds.
    ok_rsval: list sval;
    ris_sreg: PTree.t sval
  }.

Definition ris_sreg_get (ris: ristate) r: option sval :=
   match ris.(ris_sreg)!r with
   | None => ASSERT ris_input_init ris IN Some (fSinput r)
   | Some sv => Some sv
   end.

Coercion ris_sreg_get: ristate >-> Funclass.

Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ris.(ris_input_init);
     ok_rsval := ris.(ok_rsval);
     ris_sreg := sreg |}.

Definition ris_input_false (ris: ristate): ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := false;
     ok_rsval := ris.(ok_rsval);
     ris_sreg := ris.(ris_sreg) |}.

Definition ris_sreg_ok_set (ris: ristate) sreg rsvals: ristate :=
  {| ris_smem := ris.(ris_smem);
     ris_input_init := ris.(ris_input_init);
     ok_rsval := rsvals;
     ris_sreg := sreg |}.

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

Definition alive_sval (ctx : iblock_common_context) (sv : sval) : Prop :=
  alive (eval_sval ctx sv).

Record ris_ok ctx (ris: ristate) : Prop := {
  OK_RMEM: alive (eval_smem ctx (ris_smem ris));
  OK_RREG: Forall (alive_sval ctx) (ok_rsval ris)
}.
Local Hint Resolve OK_RMEM OK_RREG: core.
Local Hint Constructors ris_ok: core.

Lemma ris_ok_dec ctx ris:
  {ris_ok ctx ris}+{~ris_ok ctx ris}.
Proof.
  case (eval_smem ctx ris.(ris_smem)) eqn:MEM.
    2:right; intros []; congruence.
  case (Forall_dec (alive_sval ctx)) with (l:=ris.(ok_rsval)) as [OK|KO].
    { intros sv; unfold alive_sval; case eval_sval as [|]; [left|right]; congruence. }
  - left; constructor; congruence.
  - right; auto.
Qed.

Lemma ris_ok_preserved ctx ris:
  ris_ok (bcctx1 ctx) ris <-> ris_ok (bcctx2 ctx) ris.
Proof.
  split; intros H; inv H; econstructor; eauto;
  solve [rewrite smem_eval_preserved in *; auto
        |eapply Forall_impl; try eassumption; eauto;
         intro; unfold alive_sval; rewrite eval_sval_preserved; auto].
Qed.

Lemma ris_ok_set_sreg ctx ris sreg:
  ris_ok ctx ris <-> ris_ok ctx (ris_sreg_set ris sreg).
Proof.
  split; intro OK; inv OK; econstructor; auto.
Qed.

Lemma ris_sreg_set_access (ris: ristate) (sreg: PTree.t sval) r rsval:
  ris_sreg_ok_set ris sreg rsval r = ris_sreg_set ris sreg r.
Proof.
  unfold ris_sreg_set, ris_sreg_get; simpl.
  reflexivity.
Qed.

Lemma ris_input_false_ok ctx ris:
  ris_ok ctx ris <-> ris_ok ctx (ris_input_false ris).
Proof.
  split; intros ROK; inv ROK; constructor; auto.
Qed.

Ltac simplify_ctx :=
  try erewrite <- !sis_ok_preserved in *;
  try erewrite <- !ris_ok_preserved in *;
  try erewrite <- !smem_eval_preserved in *;
  try erewrite <- !eval_sval_preserved in *;
  try erewrite <- !eval_scondition_preserved in *;
  try erewrite <- !sis_pre_preserved in *.



Definition red_PTree_set (r: reg) (sv: sval) (ris: ristate): PTree.t sval :=
  match (ris_input_init ris), sv with
  | true, Sinput r' _ =>
      if Pos.eq_dec r r'
      then PTree.remove r' ris.(ris_sreg)
      else PTree.set r sv ris.(ris_sreg)
  | _, _ => PTree.set r sv ris.(ris_sreg)
  end.

Lemma red_PTree_set_spec r sv ris ctx r0:
  optsv_simu ctx (ris_sreg_set ris (red_PTree_set r sv ris) r0)
                 (if Pos.eq_dec r r0 then Some sv else ris r0).
Proof.
  unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl.
  case (Pos.eq_dec r r0) as [<- | R0].
  - case ris_input_init.
    + case sv; simpl; intros; try (rewrite PTree.gss; reflexivity).
      case Pos.eq_dec as [<-|].
      * rewrite PTree.grs. constructor; reflexivity.
      * rewrite PTree.gss. reflexivity.
    + rewrite PTree.gss. reflexivity.
  - case ris_input_init. case sv; intros. case Pos.eq_dec as [<-|].
    all:rewrite ?PTree.gso, ?PTree.gro by auto; reflexivity.
Qed.
Global Opaque red_PTree_set.

Lemma red_PTree_set_refines_none (ctx: iblock_common_context) (r r0:reg) ris sv:
  ris_sreg_set ris (red_PTree_set r sv ris) r0 = None <->
  (if Pos.eq_dec r r0 then Some sv else ris r0) = None.
Proof.
  specialize (red_PTree_set_spec r sv ris ctx r0); inversion 1; split; congruence.
Qed.


refinement of (symbolic) internal states


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, sis_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 := { sis_pre: iblock_exec_context -> Prop; sis_sreg:> reg -> sval; sis_smem: smem; si_wf: forall ctx, sis_pre ctx -> sis_smem <> None /\ forall r, sis_sreg r <> None }. Such a constraint should also appear in ristate. This is not clear whether this alternative design would be really simpler.

Definition ris_empty := {| ris_smem := fSinit;
                           ris_input_init := true;
                           ok_rsval := nil;
                           ris_sreg := PTree.empty _ |}.

Record ris_refines_ok ctx (ris: ristate) (sis: sistate): Prop := {
  ROK: ris_ok ctx ris;
  SOK: sis_ok ctx sis;
  MEM_EQ: eval_smem ctx ris.(ris_smem) = eval_smem ctx sis.(sis_smem);
  ALIVE_EQ: forall r, ris r = None <-> sis r = None;
  REG_EQ: forall r, osval_equiv ctx (ris r) (sis r)
}.

Record ris_refines ctx (ris: ristate) (sis: sistate): Prop := {
  OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris;
  REF: ris_ok ctx ris -> ris_refines_ok ctx ris sis
}.

Lemma wref [ctx ris sis]:
  ris_refines_ok ctx ris sis ->
  ris_refines ctx ris sis.
Proof.
  intro RR. inversion RR. constructor; tauto.
Qed.

Lemma ok_ref [ctx ris sis]:
  ris_ok ctx ris -> ris_refines ctx ris sis ->
  ris_refines_ok ctx ris sis.
Proof.
  auto using REF.
Qed.

Lemma ok_ref_si [ctx ris sis]:
  sis_ok ctx sis -> ris_refines ctx ris sis ->
  ris_refines_ok ctx ris sis.
Proof.
  intros ? []. tauto.
Qed.

Record ris_refines_ok_introT ctx ris sis : Prop := {
  RI_MEM_EQ: smem_equiv ctx (ris_smem ris) (sis_smem sis);
  RI_ALIVE_EQ: forall (r : reg), ris r = None <-> sis r = None;
  RI_REG_EQ: forall (r : reg), osval_equiv ctx (ris r) (sis r)
}.

Lemma ris_refines_intro ctx ris sis
  (OK_EQUIV: sis_ok ctx sis <-> ris_ok ctx ris)
  (REF: ris_ok ctx ris -> sis_ok ctx sis -> ris_refines_ok_introT ctx ris sis):
  ris_refines ctx ris sis.
Proof.
  constructor. assumption.
  intros ROK; apply OK_EQUIV in ROK as SOK.
  case (REF ROK SOK) as [?].
  constructor; auto.
Qed.

Lemma ris_refines_intro_not_ok ctx ris sis:
  ~ris_ok ctx ris ->
  ~sis_ok ctx sis ->
  ris_refines ctx ris sis.
Proof.
  intros; constructor; tauto.
Qed.

Global Hint Resolve wref: core.

Lemma ris_refines_ok_morph [ctx ri si0 si1]:
  sistate_eq ctx si0 si1 ->
  ris_refines_ok ctx ri si0 <-> ris_refines_ok ctx ri si1.
Proof.
  revert si0 si1; eassert (Sym : _). 2:{
    intros si0 si1 EQ; split.
    + apply (Sym si0 si1 EQ).
    + apply Sym; symmetry; apply EQ.
  }
  intros si0 si1 EQ []; inversion EQ; constructor; auto.
  - apply (sis_ok_morph EQ); auto.
  - rewrite <- EQ_SIS_SMEM; assumption.
  - intros r; rewrite ALIVE_EQ0; specialize (EQ_SIS_SREG r); inversion EQ_SIS_SREG; split; congruence.
  - intros r; rewrite REG_EQ0, (eval_osv_morph (EQ_SIS_SREG r)). reflexivity.
Qed.

Lemma ris_refines_morph [ctx ri si0 si1]:
  sistate_eq ctx si0 si1 ->
  ris_refines ctx ri si0 ->
  ris_refines ctx ri si1.
Proof.
  intros EQ []; constructor.
  - rewrite <- (sis_ok_morph EQ). apply OK_EQUIV0.
  - intros ?. apply (ris_refines_ok_morph EQ). auto.
Qed.

Lemma ris_ok_empty ctx:
  ris_ok ctx ris_empty.
Proof.
  unfold ris_empty; constructor; simpl; solve [constructor|congruence].
Qed.

Lemma ris_refines_ok_empty ctx:
  ris_refines_ok ctx ris_empty sis_empty.
Proof.
  constructor; auto.
  - apply ris_ok_empty.
  - apply sis_ok_empty.
  - reflexivity.
Qed.
Global Hint Resolve ris_ok_empty ris_refines_ok_empty: sempty.

Local Hint Resolve ROK SOK MEM_EQ REG_EQ: core.
Local Hint Constructors ris_refines: core.
Local Hint Unfold build_frame: core.
Local Hint Resolve build_frame_intro: core.

Lemma ris_refines_reg_some [ctx ris sis r sv]
  (RR: ris_refines_ok ctx ris sis)
  (RG: ris r = Some sv):
  exists sv', sis r = Some sv' /\ sval_equiv ctx sv sv'.
Proof.
  inversion RR.
  case (sis r) as [sv'|] eqn:SIS.
  - eexists; split; eauto.
    specialize (REG_EQ0 r); rewrite RG, SIS in REG_EQ0; auto.
  - exfalso. apply ALIVE_EQ0 in SIS; auto; congruence.
Qed.

Lemma ris_refines_reg_simu ctx ris sis r
  (RR: ris_refines_ok ctx ris sis):
  optsv_simu ctx (ris r) (sis r).
Proof.
  apply ALIVE_EQ with (r:=r) in RR as A.
  apply REG_EQ with (r:=r) in RR as E.
  revert A E.
  case (ris r), (sis r); try solve [constructor; auto].
  1:intros [_ C]. 2:intros [C _]. all:exfalso; lapply C; congruence.
Qed.

Lemma ris_refines_ok_preserved ctx ris sis:
  ris_refines_ok (bcctx1 ctx) ris sis <-> ris_refines_ok (bcctx2 ctx) ris sis.
Proof.
  intuition; econstructor; inv H; simplify_ctx; auto.
  all:
    intros r; specialize REG_EQ0 with r;
    unfold eval_osv in *; intros; repeat autodestruct; simplify_ctx; auto.
Qed.

Lemma ris_refines_preserved ctx ris sis:
  ris_refines (bcctx1 ctx) ris sis <-> ris_refines (bcctx2 ctx) ris sis.
Proof.
  split; intros []; constructor; simplify_ctx; auto.
  all:intro OK; apply ris_refines_ok_preserved; auto.
Qed.

Lemma eval_osv_match_sreg ctx si1 si2:
  (forall r, si1 r = None -> si2 r = None) ->
  (forall r, osval_equiv ctx (si1 r) (si2 r)) ->
  forall rs, match_sreg ctx si1 rs -> match_sreg ctx si2 rs.
Proof.
  unfold match_sreg; intros ALIVE EVAL rs MATCH r sv H.
  generalize (EVAL r); intros EVALr; try_simplify_someHyps.
  intros; rewrite <- EVALr.
  unfold eval_osv; autodestruct; simpl in *; try_simplify_someHyps.
  intros; exploit ALIVE; eauto. congruence.
Qed.

Lemma ris_refines_ok_build_frame ctx ris sis:
  ris_refines_ok ctx ris sis ->
  forall r, (build_frame ris r) <-> (build_frame sis r).
Proof.
  unfold build_frame; intros REF r. erewrite ALIVE_EQ; eauto; intuition.
Qed.

Lemma ris_refines_ok_match_sreg ctx ris sis:
  ris_refines_ok ctx ris sis ->
  forall rs, match_sreg ctx ris rs <-> match_sreg ctx sis rs.
Proof.
  intros REF rs. split; eapply eval_osv_match_sreg.
  - intros; erewrite <- ALIVE_EQ; eauto.
  - intros; erewrite REG_EQ; eauto.
  - intros; erewrite ALIVE_EQ; eauto.
  - intros; erewrite REG_EQ; eauto.
Qed.

Lemma ris_refines_sreg_ok ctx ris sis:
  ris_refines_ok ctx ris sis ->
  sreg_ok ctx ris.
Proof.
  intros REF r sv H1 H2.
  exploit REG_EQ; eauto.
  erewrite H1; simpl.
  erewrite H2. intros; destruct (sis r) eqn: SISr; simpl in *; try congruence.
  + exploit OK_SREG; eauto.
  + erewrite <- ALIVE_EQ in SISr; eauto. congruence.
Qed.
Local Hint Resolve ris_refines_sreg_ok: core.

Properties of the (abstract) operators involved in symbolic execution


Lemma ok_set_mem ctx sm sis:
  sis_ok ctx (set_smem sm sis)
  <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None).
Proof.
  split; destruct 1; econstructor; simpl in *; eauto.
  intuition eauto.
Qed.

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 -> smem_equiv ctx rm sm) ->
  ris_refines ctx (rset_smem rm ris) (set_smem sm sis).
Proof.
  destruct 2; intros.
  constructor; [|intros ROK; apply ok_rset_mem in ROK as [ROK ?]; auto; case (REF0 ROK) as []; constructor];
    eauto;
    try solve [rewrite ok_rset_mem; intuition eauto];
    rewrite ?ok_set_mem, ?ok_rset_mem; intuition congruence.
Qed.

Lemma rset_mem_correct1 ctx rm sm ris sis:
  (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
  ris_refines_ok ctx ris sis ->
  smem_equiv ctx rm sm ->
  ris_refines ctx (rset_smem rm ris) (set_smem sm sis).
Proof.
  intros; apply rset_mem_correct; auto.
Qed.

refinement of (symbolic) final values


Lemma svident_simu_preserved ctx rvos ros:
  svident_simu (bcctx1 ctx) rvos ros <-> svident_simu (bcctx2 ctx) rvos ros.
Proof.
  split; intros H; inv H; econstructor; simplify_ctx; eauto.
Qed.

Lemma sfv_simu_preserved ctx sfv1 sfv2:
  sfv_simu (bcctx1 ctx) sfv1 sfv2 <-> sfv_simu (bcctx2 ctx) sfv1 sfv2.
Proof.
  split; intros H; inv H; econstructor; eauto;
  unfold bargs_simu, bargs_simu in *;
  try (apply svident_simu_preserved; auto);
  try (rewrite !list_sval_eval_preserved in *; auto);
  try (rewrite !eval_list_builtin_sval_preserved in *; auto);
  try (inv OPT; econstructor);
  simplify_ctx; auto.
Qed.

Some preservation properties wrt theory

 
Lemma refines_opt_sv ctx ris sis r sS sR:
  ris_refines_ok ctx ris sis ->
  sis r = Some sS -> ris r = Some sR ->
  sval_equiv ctx sR sS.
Proof.
  intros. destruct H.
  specialize REG_EQ0 with r. rewrite H0, H1 in REG_EQ0.
  simpl in REG_EQ0. auto.
Qed.

Lemma eval_list_sval_refpreserv ctx args ris sis:
  ris_refines_ok ctx ris sis ->
  forall lsv lsv',
  lmap_sv ris args = Some lsv ->
  lmap_sv (sis_sreg sis) args = Some lsv' ->
  list_sval_equiv ctx lsv lsv'.
Proof.
  intros REF.
  induction args; simpl; try_simplify_someHyps.
  repeat autodestruct; intros.
  try_simplify_someHyps; intros.
  erewrite refines_opt_sv; eauto.
  erewrite IHargs; eauto.
Qed.
Local Hint Resolve eval_list_sval_refpreserv: core.

Lemma eval_builtin_sval_refpreserv ctx arg ris sis:
  ris_refines_ok ctx ris sis ->
  forall ba ba',
  map_builtin_arg_opt ris arg = Some ba ->
  map_builtin_arg_opt sis arg = Some ba' ->
  eval_builtin_sval ctx ba = eval_builtin_sval ctx ba'.
Proof.
  unfold eval_builtin_sval.
  induction arg; simpl; repeat autodestruct; try_simplify_someHyps.
  - intros; erewrite refines_opt_sv; eauto.
  - intros; erewrite (IHarg1 _ b b1), (IHarg2 _ b0 b2); eauto.
  - intros; erewrite (IHarg1 _ b b1), (IHarg2 _ b0 b2); eauto.
  Unshelve. all: auto.
Qed.

Lemma bargs_refpreserv ctx args ris sis:
  ris_refines_ok ctx ris sis ->
  forall lba lba',
  bamap_opt (map_builtin_arg_opt ris) args = Some lba ->
  bamap_opt (map_builtin_arg_opt sis) args = Some lba' ->
  bargs_simu ctx lba lba'.
Proof.
  unfold bargs_simu, bamap_opt, eval_list_builtin_sval. intros REF.
  induction args; simpl; try_simplify_someHyps.
  repeat autodestruct; try_simplify_someHyps.
  intros; erewrite eval_builtin_sval_refpreserv, IHargs; eauto.
Qed.

Local Hint Resolve bargs_refpreserv refines_opt_sv: core.
Local Hint Constructors sfv_simu optsv_simu svident_simu: core.

Lemma exec_final_refpreserv ctx i ris sis sfv sfv':
  ris_refines_ok ctx ris sis ->
  sexec_final_sfv i ris = Some sfv ->
  sexec_final_sfv i sis = Some sfv' ->
  sfv_simu ctx sfv sfv'.
Proof.
  destruct i; simpl; unfold sum_left_optmap;
  repeat autodestruct; try_simplify_someHyps; eauto.
Qed.

refinement of (symbolic) states



Definition rstate := pstate ristate.

Definition rst_ok_in ctx rs1 rs2 :=
  forall ris2, get_soutcome ctx rs2 = Some ris2 -> ris_ok ctx ris2.(_sis) ->
  exists ris1, get_soutcome ctx rs1 = Some ris1 /\ ris_ok ctx ris1.(_sis).

Inductive rout_refines_ok ctx : option (poutcome ristate) -> option (poutcome sistate) -> Prop :=
  rst_refines_ok_intro
    (rt : poutcome ristate)
    (st : poutcome sistate)
    (RST_RR : ris_refines_ok ctx rt.(_sis) st.(_sis))
    (RST_RFV : sfv_simu ctx rt.(_sfv) st.(_sfv))
  : rout_refines_ok ctx (Some rt) (Some st).

Definition rst_refines_ok ctx (rs : rstate) (ss : sstate) :=
  rout_refines_ok ctx (get_soutcome ctx rs) (get_soutcome ctx ss).

Inductive rout_refines ctx (rt : option (poutcome ristate)) (st : option (poutcome sistate)) : Prop :=
  | ROUT_OK_intro (RR_OUT : rout_refines_ok ctx rt st)
  | ROUT_KO_intro (ROUT_KO : forall rout, rt = Some rout -> ~ris_ok ctx rout.(_sis))
                  (SOUT_KO : forall sout, st = Some sout -> ~sis_ok ctx sout.(_sis)).

Definition rst_refines ctx (rs : rstate) (ss : sstate) :=
  rout_refines ctx (get_soutcome ctx rs) (get_soutcome ctx ss).

Lemma ok_rst_ref ctx rs ss out
  (ROUT : get_soutcome ctx rs = Some out)
  (ROK : ris_ok ctx out.(_sis))
  (RST : rst_refines ctx rs ss):
  rst_refines_ok ctx rs ss.
Proof.
  inversion RST. 2:exfalso; eapply ROUT_KO; eauto.
  unfold rst_refines_ok; exact RR_OUT.
Qed.

Lemma ok_rst_ref_si ctx rs ss out
  (SOUT : get_soutcome ctx ss = Some out)
  (SOK : sis_ok ctx out.(_sis))
  (RST : rst_refines ctx rs ss):
  rst_refines_ok ctx rs ss.
Proof.
  inversion RST. 2:exfalso; eapply SOUT_KO; eauto.
  unfold rst_refines_ok; exact RR_OUT.
Qed.

Lemma wrst_ref ctx rs ss:
  rst_refines_ok ctx rs ss ->
  rst_refines ctx rs ss.
Proof.
  apply ROUT_OK_intro.
Qed.

Lemma rout_refines_None ctx:
  rout_refines ctx None None.
Proof.
  apply ROUT_KO_intro; discriminate 1.
Qed.


Inductive rst_refines_struct ctx: rstate -> sstate -> Prop :=
  | Reffinal ris sis rfv sfv
      (RIS: ris_refines ctx ris sis)
      (RFV: sfv_simu ctx rfv sfv)
      :rst_refines_struct ctx (Sfinal 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_struct ctx rifso ifso)
      (REFnot: eval_scondition ctx rcond rargs = Some false ->
        rst_refines_struct ctx rifnot ifnot)
      :rst_refines_struct ctx (Scond rcond rargs rifso rifnot) (Scond cond args ifso ifnot)
  | Refabort
      :rst_refines_struct ctx Sabort Sabort
  .

Lemma rst_refines_of_struct ctx rs ss:
  rst_refines_struct ctx rs ss ->
  rst_refines ctx rs ss.
Proof.
  unfold rst_refines; induction 1; simpl.
  - case (ris_ok_dec ctx ris) as [OK|KO].
    + apply (ok_ref OK) in RIS; inversion RIS.
      apply ROUT_OK_intro; constructor; simpl; tauto.
    + apply OK_EQUIV in RIS; apply ROUT_KO_intro; injection 1 as <-; simpl; tauto.
  - rewrite <- RCOND; destruct eval_scondition as [[|]|].
    + apply H; reflexivity.
    + apply H0; reflexivity.
    + apply rout_refines_None.
  - apply rout_refines_None.
Qed.

Simulation between refined (internal) states


Simulation properties on internal states


Record ris_simu ctx (ris1 ris2 : ristate) : Prop := {
  SIMU_FAILS: ris_ok ctx ris1 -> ris_ok ctx ris2;
  SIMU_MEM: ris1.(ris_smem) = ris2.(ris_smem);
  SIMU_REG: forall r, alive (ris1 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 ris1 ris2 ctx:
  ris_simu ctx ris1 ris2 -> ris_ok ctx ris1 -> ris_ok ctx ris2.
Proof.
  intros SIMU OK; eauto.
Qed.

Lemma ris_simu_match_sreg_preserv ris1 ris2 ctx rs:
  ris_simu ctx ris1 ris2 ->
  sreg_ok ctx ris2 ->
  match_sreg ctx ris1 rs ->
  exists rs', match_sreg ctx ris2 rs' /\ eqlive_reg (build_frame ris1) rs rs'.
Proof.
  intros [] OK MATCH.
  exists (eval_map_sreg ctx (fun x => x) ris2.(ris_sreg)).
  eassert (MATCH2: _). 2:split;[exact MATCH2|].
  - intros r sv H. specialize (OK r sv H). revert H OK.
    unfold ris_sreg_get; rewrite eval_map_sreg_correct.
    repeat autodestruct; try_simplify_someHyps.
  - intros r.
    unfold build_frame; case ris_sreg_get as [sv|] eqn:RIS; [intros _ | congruence].
    apply MATCH in RIS as EQ1. revert EQ1.
    rewrite (SIMU_REG0 r) in RIS by congruence.
    apply MATCH2 in RIS as ->. try_simplify_someHyps.
Qed.

Lemma ris_simu_correct ris1 ris2 ctx sis1 sis2:
  ris_simu ctx ris1 ris2 ->
  ris_refines ctx ris1 sis1 ->
  ris_refines ctx ris2 sis2 ->
  sistate_simu ctx sis1 sis2.
Proof.
  intros SIMU REF1 REF2 rs m SEM.
  exploit sem_sis_ok; eauto.
    erewrite OK_EQUIV; eauto.
    intros ROK1.
  exploit ris_simu_ok_preserv; eauto.
    intros ROK2.
  apply ok_ref in REF1, REF2; auto; inversion REF1. inversion REF2.
  destruct SEM as (PRE & SMEM & SREG).
  exploit ris_simu_match_sreg_preserv; eauto.
  { erewrite ris_refines_ok_match_sreg; eauto. }
  intros (rs2 & MATCH & EQLIVE).
  exists rs2; unfold sem_sistate; repeat split.
  + eapply SOK; eauto.
  + erewrite <- MEM_EQ, <- SIMU_MEM; eauto.
    erewrite MEM_EQ; eauto.
  + erewrite <- ris_refines_ok_match_sreg; eauto.
  + intros; eapply eqlive_reg_monotonic; eauto.
    intros; erewrite ris_refines_ok_build_frame; eauto.
Qed.

Lemma ris_simu_correct_build_frame ris1 ris2 ctx sis1 sis2:
  ris_simu ctx ris1 ris2 ->
  ris_refines_ok ctx ris1 sis1 ->
  ris_refines ctx ris2 sis2 ->
  forall r, build_frame sis1 r -> build_frame sis2 r.
Proof.
  intros RIS REF1 REF2.
  exploit ris_simu_ok_preserv; eauto.
  intros ROK2 r; apply (ok_ref ROK2) in REF2.
  erewrite <- ris_refines_ok_build_frame; eauto.
  erewrite <- (ris_refines_ok_build_frame ctx ris2 sis2); eauto.
  destruct (ris1 r) eqn: X; auto.
  try_simplify_someHyps; intros.
  inv RIS; rewrite SIMU_REG0 in X; eauto.
Qed.

Simulation relation


Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2.

The simulation can either be "light" (i.e. only on the final internal state), or "hard", with an additional check on final values. The "light" simulation is used to verify application of history invariants.
Inductive rst_simu ctx: bool -> rstate -> rstate -> Prop :=
  | Rfinal_simu_light ris1 ris2 rfv1 rfv2
      (RIS: ris_simu ctx ris1 ris2)
      : rst_simu ctx true (Sfinal ris1 rfv1) (Sfinal ris2 rfv2)
  | Rfinal_simu_hard ris1 ris2 rfv1 rfv2
      (RIS: ris_simu ctx ris1 ris2)
      (RFV: rfv_simu rfv1 rfv2)
      : rst_simu ctx false (Sfinal ris1 rfv1) (Sfinal ris2 rfv2)
  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2 light_check
      (IFSO: eval_scondition ctx cond rargs = Some true ->
        rst_simu ctx light_check rifso1 rifso2)
      (IFNOT: eval_scondition ctx cond rargs = Some false ->
        rst_simu ctx light_check rifnot1 rifnot2)
      : rst_simu ctx light_check
        (Scond cond rargs rifso1 rifnot1) (Scond cond rargs rifso2 rifnot2)
  | Rabort_simu light_check: rst_simu ctx light_check Sabort Sabort
  .

Definition routcome := poutcome ristate.

Local Hint Resolve eval_sval_preserved list_sval_eval_preserved
  smem_eval_preserved eval_list_builtin_sval_preserved: core.

Lemma rvf_simu_correct rfv1 rfv2 ctx sfv1 sfv2:
  rfv_simu rfv1 rfv2 ->
  sfv_simu ctx rfv1 sfv1 ->
  sfv_simu ctx rfv2 sfv2 ->
  sfv_simu ctx sfv1 sfv2.
Proof.
  unfold rfv_simu; intros X REF1 REF2. subst.
  destruct REF1; inv REF2; simpl; econstructor; eauto.
  - (* call svid *)
    inv SVID; inv SVID0; econstructor; eauto.
    rewrite <- SIMU, <- SIMU0; eauto.
  - (* call args *)
    rewrite <- ARGS, <- ARGS0; eauto.
  - (* taillcall svid *)
    inv SVID; inv SVID0; econstructor; eauto.
    rewrite <- SIMU, <- SIMU0; eauto.
  - (* tailcall args *)
    rewrite <- ARGS, <- ARGS0; eauto.
  - (* builtin args *)
    unfold bargs_simu in *.
    rewrite <- BARGS, <- BARGS0; eauto.
  - (* jumptable arg *)
    rewrite <- VAL, <- VAL0; eauto.
  - (* return *)
    inv OPT; inv OPT0; econstructor; eauto.
    rewrite <- SIMU, <- SIMU0; eauto.
Qed.

Lemma rst_simu_lroutcome_light ctx light_check rst1 rst2:
   rst_simu ctx light_check rst1 rst2 ->
   light_check = true ->
   forall ris1 ris2 rfv1 rfv2,
   get_soutcome ctx rst1 = Some (sout ris1 rfv1) ->
   get_soutcome ctx rst2 = Some (sout ris2 rfv2) ->
   ris_simu ctx ris1 ris2.
Proof.
  induction 1; simpl; intros lc lris1 lris2 lrfv1 lrfv2 ROUT1 ROUT2; try_simplify_someHyps.
  repeat autodestruct; eauto.
Qed.

Lemma rst_simu_lroutcome_hard ctx light_check rst1 rst2:
   rst_simu ctx light_check rst1 rst2 ->
   light_check = false ->
   forall ris1 rfv1,
   get_soutcome ctx rst1 = Some (sout ris1 rfv1) ->
   exists ris2 rfv2,
    get_soutcome ctx rst2 = Some (sout ris2 rfv2) /\ ris_simu ctx ris1 ris2 /\ rfv_simu rfv1 rfv2.
Proof.
  induction 1; simpl; intros lc lris1 lrfv1 ROUT; simplify_option.
Qed.

Local Hint Resolve ris_simu_correct rvf_simu_correct: core.

Lemma rst_simu_light_correct ctx rst1 rst2 st1 st2 sis1 sis2 sfv1 sfv2
  (SIMU: rst_simu ctx true rst1 rst2)
  (REF1: get_soutcome ctx st1 = Some (sout sis1 sfv1) -> sis_ok ctx sis1 ->
    rst_refines ctx rst1 st1)
  (REF2: get_soutcome ctx st2 = Some (sout sis2 sfv2) -> sis_ok ctx sis2 ->
    rst_refines ctx rst2 st2)
  (REF1_OK: symb_exec_ok ctx st1 sis1 sfv1)
  (REF2_OK: symb_exec_ok ctx st2 sis2 sfv2)
  :sistate_simu ctx sis1 sis2.
Proof.
  destruct REF1_OK as (SOUT1 & OK1); destruct REF2_OK as (SOUT2 & OK2).
  exploit REF1; eauto; exploit REF2; eauto.
  clear REF2; clear REF1.
  unfold rst_refines; rewrite SOUT1, SOUT2.
  inversion 1. 2:exfalso; eapply SOUT_KO; eauto.
    inversion RR_OUT as [[ris2 rsfv2] ? RR2 _ ROUT2]; simpl in *.
  inversion 1. 2:exfalso; eapply SOUT_KO; eauto.
    inversion RR_OUT0 as [[ris1 rsfv1] ? RR1 _ ROUT1]; simpl in *.
  exploit rst_simu_lroutcome_light; eauto.
Qed.

Lemma rst_simu_hard_correct ctx rst1 rst2 st1 st2
  (SIMU: rst_simu ctx false rst1 rst2)
  (REF1: forall sis sfv, get_soutcome ctx st1 = Some (sout sis sfv) -> sis_ok ctx sis ->
    rst_refines ctx rst1 st1)
  (REF2: forall ris rfv, get_soutcome ctx rst2 = Some (sout ris rfv) -> ris_ok ctx ris ->
    rst_refines ctx rst2 st2)
  :match_sexec_live ctx st1 st2.
Proof.
  unfold match_sexec_live.
  intros sis1 sfv1 (SOUT & OK1).
  exploit REF1; eauto. clear REF1.
  unfold rst_refines; rewrite SOUT.
  inversion 1. 2:exfalso; eapply SOUT_KO; eauto.
    inversion RR_OUT as [[ris1 rsfv1] ? RR1 RF1 ROUT1]; simpl in *.
  exploit rst_simu_lroutcome_hard; eauto.
  intros (ris2 & rfv2 & ROUT2 & SIMUI & SIMUF); clear ROUT1.
  exploit ris_simu_ok_preserv; eauto.
  intros ROK2.
  exploit REF2; eauto. clear REF2.
  unfold rst_refines; rewrite ROUT2.
  inversion 1. 2:exfalso; eapply ROUT_KO; eauto.
    inversion RR_OUT0 as [? [sis2 sfv2] RR2 RF2 _ROUT2 SOUT2]; simpl in *.
  exists sis2, sfv2; repeat (split; eauto).
  intros; eapply ris_simu_correct_build_frame; eauto.
Qed.

si_ok preservation under sexec

Lemma sis_ok_op_okpreserv ctx op args dest sis sis':
  sexec_op op args dest sis = Some sis' ->
  sis_ok ctx sis' -> sis_ok ctx sis.
Proof.
  unfold sexec_op. autodestruct.
  intros H1 H2; inv H2.
  rewrite ok_set_sreg. intuition.
Qed.

Lemma sis_ok_load_okpreserv ctx chunk addr args aaddr dest sis sis' trap:
  sexec_load trap chunk addr args aaddr dest sis = Some sis' ->
  sis_ok ctx sis' ->
  sis_ok ctx sis.
Proof.
  unfold sexec_load. autodestruct.
  intros H1 H2; inv H2.
  rewrite ok_set_sreg. intuition.
Qed.

Lemma sis_ok_store_okpreserv ctx chunk addr args aargs src sis sis':
  sexec_store chunk addr args aargs src sis = Some sis' ->
  sis_ok ctx sis' ->
  sis_ok ctx sis.
Proof.
  unfold sexec_store. repeat autodestruct.
  intros H1 H2 H3; inv H1; inv H3.
  rewrite ok_set_mem. intuition.
Qed.

Local Hint Resolve sis_ok_op_okpreserv sis_ok_load_okpreserv sis_ok_store_okpreserv: sis_ok.

This lemma is used in BTL_SEimpl.v
Lemma sexec_rec_okpreserv ctx ib:
  forall k
  (CONT: forall sis lsis sfv,
    get_soutcome ctx (k sis) = Some (sout lsis sfv) ->
    sis_ok ctx lsis ->
    sis_ok ctx sis)
  sis lsis sfv
  (SOUT: get_soutcome ctx (sexec_rec ib sis k) = Some (sout lsis sfv))
  (SOK: sis_ok ctx lsis),
  sis_ok ctx sis.
Proof.
  induction ib; simpl.
  1-5: try_simplify_someHyps; try autodestruct; eauto with sis_ok; try discriminate.
  - simpl. intros; inv SOUT. eauto.
  - intros. eapply IHib1. 2-3: eauto.
    eapply IHib2; eauto.
  - intros k CONT sis lsis sfv.
    repeat (intros; try_simplify_someHyps; autodestruct).
    simpl; congruence.
Qed.

Refinement definitions used in the implementation and in the intermediate ref proof.


Substitution property

Definition reg_subst (ris: ristate) (sis: sistate) (si: fpasv) ctx :=
  forall r, eval_osv ctx (ris r) = eval_sval ctx (sv_subst (sis_smem sis) sis (ext si r)).

Lemma substitution_rule_si_empty ctx (ris: ristate) sis
  (RR: ris_refines_ok ctx ris sis)
  (RINIT: ris_input_init ris = true)
  :reg_subst ris sis si_empty ctx.
Proof.
  inversion RR; simpl;
  unfold reg_subst, eval_osv; intros; autodestruct; simpl.
  - autodestruct; eauto.
    rewrite <- ALIVE_EQ0; congruence.
  - unfold ris_sreg_get. rewrite RINIT.
    autodestruct.
Qed.
Global Hint Resolve substitution_rule_si_empty: sempty.

root_op application

Definition root_sapply (rsv: root_op) (lir: list ireg) (sis: sistate) si: option sval :=
  SOME lsv <- lmap_sv (ir_subst_si sis si) lir IN
  Some (root_apply rsv lsv (sis_smem sis)).
Coercion root_sapply: root_op >-> Funclass.

Lemma root_sapply_rop_subst ctx (rop: root_op) args sis si sv
  (RSV: rop args sis si = Some sv)
  :sval_equiv ctx sv (sv_subst (sis_smem sis) sis (rop_subst (ext si) rop args)).
Proof.
  revert RSV; unfold root_sapply, rop_subst, root_apply.
  repeat autodestruct; intros ROP LMAP HINV; inv HINV; simpl;
  erewrite lmap_sv_lsv_subst; auto.
Qed.

Definition may_trap (strict : bool) (rsv: root_op) (args_len : nat): bool :=
  match rsv with
  | Rop op => is_trapping_op op ||| negb (Nat.eqb args_len (args_of_operation op))
  | Rload TRAP _ _ _ => true
  | Rload NOTRAP _ _ _ => false
  end.

Lemma lazy_orb_negb_false (b1 b2:bool):
  (b1 ||| negb b2) = false <-> (b1 = false /\ b2 = true).
Proof.
  unfold negb. repeat autodestruct; simpl; intuition (try congruence).
Qed.

Lemma may_trap_correct ctx strict (rsv: root_op) (sm : smem)
  (STRICT : ctx_strict_reflect (ctx_bc ctx) strict):
  forall lsv lv,
  eval_list_sval ctx lsv = Some lv ->
  may_trap strict rsv (length lv) = false ->
  eval_smem ctx sm <> None ->
  eval_sval ctx (root_apply rsv lsv sm) <> None.
Proof.
  destruct rsv; simpl; try congruence; intros lsv lv.
  - rewrite lazy_orb_negb_false. intros OK1 (TRAP1 & LEN)OK2.
    simpl; autodestruct; intros; injection OK1 as ->.
    eapply is_trapping_op_sound; eauto.
    apply Nat.eqb_eq in LEN.
    eassumption.
  - intros OK1 X OK2.
    simpl. unfold root_sapply.
    repeat autodestruct.
Qed.


Fixpoint lsv_length (l : list_sval) : nat :=
  match l with
  | Snil _ => O
  | Scons _ l _ => S (lsv_length l)
  end.

Lemma eval_list_sval_length ctx lsv lv:
  eval_list_sval ctx lsv = Some lv ->
  lsv_length lsv = Datatypes.length lv.
Proof.
  revert lv; induction lsv; simplify_option; injection 1 as <-; reflexivity.
Qed.


Relation between the implementation states for common operations


Record ris_rel (m : se_mode) (ris0 ris1 : ristate) := {
  RRL_INPUT: ris0.(ris_input_init) = ris1.(ris_input_init);
  RRL_OK: forall ctx, ris_ok ctx ris1 -> ris_ok ctx ris0;
  RRL_OK_SI: m.(se_ok_check) = true ->
             forall ctx, ris_ok ctx ris0 -> ris_ok ctx ris1;
}.

Global Instance ris_rel_PreOrder {m : se_mode}: PreOrder (ris_rel m).
Proof.
  constructor.
  - constructor; solve [reflexivity|tauto].
  - intros ? ? ? [?] [?]; constructor; eauto; etransitivity; eauto.
Qed.

Generated by coq2html