Module SimMemExt

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 IntegersC LinkingC.
Require Import SimSymb Skeleton Mod ModSem.
Require SimSymbId.
Require Import SimMemLift.

Set Implicit Arguments.




Record t' := mk {
  src: mem;
  tgt: mem;
}.

Program Instance SimMemExt : SimMem.class :=
{ t := t';
  src := src;
  tgt := tgt;
  wf := fun (rel: t') => Mem.extends rel.(src) rel.(tgt);
  le := fun (mrel0 mrel1: t') => True;
  lepriv := top2;
  sim_val := fun (_: t') => Val.lessdef;
  sim_val_list := fun (_: t') => Val.lessdef_list;
}.
Next Obligation.
  do 2 (apply Axioms.functional_extensionality; i).
  apply prop_ext1.
  split; i; ss; clarify.
  - ginduction x; ii; inv H; ss. econs; eauto.
  - induction H; econs; eauto.
Qed.
Next Obligation.
inv H. ss. Qed.


Program Instance SimMemExtLift: SimMemLift.class SimMemExt :=
{ lift := id;
  unlift := fun _ => id;
}.

Global Program Instance SimSymbExtends: SimSymb.class SimMemExt := {
  t := unit;
  le := SimSymbId.le;
  sim_sk := SimSymbId.sim_sk;
  sim_skenv (_: SimMem.t) (_: unit) := SimSymbId.sim_skenv;
}.
Next Obligation.
ss. Qed.
Next Obligation.
rr in SIMSK. clarify. Qed.
Next Obligation.
eapply SimSymbId.sim_sk_link; eauto. Qed.
Next Obligation.
rr in SIMSKE. clarify. Qed.
Next Obligation.
  exploit SimSymbId.sim_sk_load_sim_skenv; eauto. i; des.
  eexists. eexists (mk _ _). esplits; ss; eauto.
  - apply Mem.extends_refl.
  - rewrite MAINSIM. ss.
Qed.
Next Obligation.
eapply SimSymbId.sim_skenv_monotone; try apply SIMSKENV; eauto. Qed.
Next Obligation.
  exploit SimSymbId.sim_skenv_func_bisim; eauto. i; des.
  inv H. inv SIMSKENV. econs; eauto.
  ii; ss. eapply FUNCFSIM; eauto. rpapply FUNCSRC. f_equal. inv SIMFPTR; ss.
Qed.
Next Obligation.
esplits; eauto. eapply SimSymbId.system_sim_skenv; eauto.
Qed.
Next Obligation.
  inv ARGS; ss. destruct sm0; ss; clarify.
  exploit external_call_mem_extends; eauto. i. des.
  exists (mk retv_src.(Retv.m) m2'). exists (Retv.mk vres' m2').
  esplits; ss; eauto.
  { eapply external_call_symbols_preserved; eauto.
    eapply SimSymbId.sim_skenv_equiv; eauto. }
  destruct retv_src; ss. econs; ss; eauto.
Qed.