Module SimMemLift

Require Import CoqlibC.
Require Import Memory.
Require Import Values.
Require Import Maps.
Require Import Events.
Require Import Globalenvs.
Require Import sflib.
Require Import RelationClasses.
Require Import FSets.
Require Import Ordered.
Require Import AST.
Require Import Integers.

Require Import ModSem.
Require Export SimMem.

Set Implicit Arguments.



Module SimMemLift.


  Class class (SM: SimMem.class) :=
  { lepriv_Trans :> Transitive SimMem.lepriv;

    lift: SimMem.t -> SimMem.t;
    unlift: SimMem.t -> SimMem.t -> SimMem.t;

    lift_wf: forall mrel, SimMem.wf mrel -> SimMem.wf (lift mrel);
    lift_src: forall mrel, (lift mrel).(SimMem.src) = mrel.(SimMem.src);
    lift_tgt: forall mrel, (lift mrel).(SimMem.tgt) = mrel.(SimMem.tgt);
    unlift_src: forall mrel0 mrel1, (unlift mrel0 mrel1).(SimMem.src) = mrel1.(SimMem.src);
    unlift_tgt: forall mrel0 mrel1, (unlift mrel0 mrel1).(SimMem.tgt) = mrel1.(SimMem.tgt);
    lift_spec: forall mrel0 mrel1, SimMem.le (lift mrel0) mrel1 -> SimMem.wf mrel0 -> SimMem.le mrel0 (unlift mrel0 mrel1);
    unlift_wf: forall mrel0 mrel1,
        SimMem.wf mrel0 -> SimMem.wf mrel1 -> SimMem.le (lift mrel0) mrel1 -> SimMem.wf (unlift mrel0 mrel1);

    lift_sim_val: forall mrel, SimMem.sim_val mrel <2= SimMem.sim_val (lift mrel);


    lift_priv: forall sm0 (MWF: SimMem.wf sm0), SimMem.lepriv sm0 (lift sm0);
    unlift_priv: forall
        sm_at sm_arg sm_ret
        (MWF: SimMem.wf sm_at)
        (MLIFT: SimMem.lepriv sm_at sm_arg)
        (MLE: SimMem.le sm_arg sm_ret)
        (MWF: SimMem.wf sm_ret),
        SimMem.lepriv sm_ret (unlift sm_at sm_ret);
  }.

  Section PROPS.

  Context {SM: SimMem.class}.
  Context {SML: SimMemLift.class SM}.

  Lemma lift_sim_regset: forall sm0, SimMem.sim_regset sm0 <2= SimMem.sim_regset (SimMemLift.lift sm0).
Proof.
ii. eapply SimMemLift.lift_sim_val; et. Qed.

  Lemma le_lift_lepriv
        sm0 sm1 sm_lift
        (MWF0: SimMem.wf sm0)
        (MWF1: SimMem.wf sm1)
        (MLE: SimMem.le sm0 sm1)
        (MLIFT: SimMemLift.lift sm1 = sm_lift):
      <<MLE: SimMem.lepriv sm0 sm_lift>>.
Proof.
    subst. hexploit (SimMemLift.lift_priv sm1); eauto. intro T. r. etrans; et.
  Qed.

  Lemma lift_args
        args_src args_tgt sm_arg0
        (ARGS: SimMem.sim_args args_src args_tgt sm_arg0):
      <<ARGS: SimMem.sim_args args_src args_tgt (SimMemLift.lift sm_arg0)>>.
Proof.
    inv ARGS.
    - econs; eauto.
      + eapply SimMemLift.lift_sim_val; et.
      + erewrite <- SimMem.sim_val_list_spec in *.
        eapply Forall2_impl.
        { eapply SimMemLift.lift_sim_val; et. }
        ss.
      + rewrite SimMemLift.lift_src. ss.
      + rewrite SimMemLift.lift_tgt. ss.
    - econs 2; eauto.
      + eapply lift_sim_regset; et.
      + rewrite SimMemLift.lift_src. ss.
      + rewrite SimMemLift.lift_tgt. ss.
  Qed.


  End PROPS.

End SimMemLift.