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.
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.
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.
End PROPS.
End SimMemLift.