Require Export Coqlib.
Require Export Errors.
Require Export AST.
Require Export Integers.
Require Export Floats.
Require Export Op.
Require Export Asm.
Require Export Events.
Require Export Globalenvs.
Require Export Smallstep.
Require Export Values.
Require Export Memory.
Require Export Maps.
Require Export CommonTactic.
Require Export AuxLemma.
Require Export FlatMemory.
Require Export AuxStateDataType.
Require Export Constant.
Require Export GlobIdent.
Require Export RealParams.
Require Export LoadStoreSem3high.
Require Export AsmImplLemma.
Require Export GenSem.
Require Export RefinementTactic.
Require Export PrimSemantics.
Require Export XOmega.

Require Export liblayers.logic.PTreeModules.
Require Export liblayers.logic.LayerLogicImpl.
Require Export liblayers.compcertx.Stencil.
Require Export liblayers.compcertx.MakeProgram.
Require Export liblayers.compat.CompatLayers.
Require Export liblayers.compat.CompatGenSem.
Require Export compcert.cfrontend.Ctypes.

Require Export LayerCalculusLemma.
Require Export AbstractDataType.

Require Export PIPCIntro.
Require Export PHThread.
Require Export OracleCHANRel.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Open Scope string_scope.
Open Scope error_monad_scope.
Open Scope Z_scope.

Notation HDATA := RData.
Notation LDATA := RData.

Notation HDATAOps := (cdata (cdata_ops := pipcintro_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := phthread_data_ops) LDATA).

Section Refinement.

  Section WITHMEM.

    Context `{single_oracle_prop: SingleOracleProp}.
    Context `{real_params : RealParams}.
    Context `{multi_oracle_prop: MultiOracleProp}.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Record relate_RData (f: meminj) (hadt: HDATA) (ladt: LDATA) :=
      mkrelate_RData {
          flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
          vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
          CR3_re: CR3 hadt = CR3 ladt;
          ikern_re: ikern hadt = ikern ladt;
          pg_re: pg hadt = pg ladt;
          ihost_re: ihost hadt = ihost ladt;
          AC_re: AC hadt = AC ladt;
          ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
          ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
          
          nps_re: nps hadt = nps ladt;
          init_re: init hadt = init ladt;

          pperm_re: pperm hadt = pperm ladt;
          PT_re: PT hadt = PT ladt;
          ptp_re: ptpool hadt = ptpool ladt;
          idpde_re: idpde hadt = idpde ladt;
          ipt_re: ipt hadt = ipt ladt;
          

          CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
          cid_re: cid hadt = cid ladt;
          big_log_re: big_log hadt = big_log ladt;
          big_oracle_re: big_oracle hadt = big_oracle ladt;
          lock_re: lock hadt = lock ladt;

          com1_re: com1 hadt = com1 ladt;
          console_re: console hadt = console ladt;
          console_concrete_re: console_concrete hadt = console_concrete ladt;
          ioapic_re: ioapic ladt = ioapic hadt;
          lapic_re: lapic ladt = lapic hadt;
          intr_flag_re: intr_flag ladt = intr_flag hadt;
          curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
          in_intr_re: in_intr ladt = in_intr hadt;
          drv_serial_re: drv_serial hadt = drv_serial ladt;

          kctxt_re: kctxt_inj f num_proc (kctxt hadt) (kctxt ladt);
          uctxt_re: uctxt_inj f (uctxt hadt) (uctxt ladt);
          syncchpool_re: syncchpool hadt = syncchpool ladt;
          

          

          ept_re: ept hadt = ept ladt;
          vmcs_re: VMCSPool_inj f (vmcs hadt) (vmcs ladt);
          vmx_re: VMXPool_inj f (vmx hadt) (vmx ladt)
        }.

    Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
    | MATCH_RDATA: ∀ habd m f s, match_RData s habd m f.

    Local Hint Resolve MATCH_RDATA.

    Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
      {
        relate_AbData s f d1 d2 := relate_RData f d1 d2;
        match_AbData s d1 m f := match_RData s d1 m f;
        new_glbl := nil
      }.

    Section Rel_Property.

      Lemma relate_incr:
        ∀ abd abd´ f f´,
          relate_RData f abd abd´
          → inject_incr f f´
          → relate_RData f´ abd abd´.
      Proof.
        inversion 1; subst; intros; inv H; constructor; eauto.
        - eapply kctxt_inj_incr; eauto.
        - eapply uctxt_inj_incr; eauto.
        - unfold VMCSPool_inj.
          intros.
          eapply VMCS_inj_incr; eauto.
        - unfold VMXPool_inj.
          intros.
          eapply VMX_inj_incr; eauto.
      Qed.

    End Rel_Property.

    Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
    Proof.
      constructor; intros; simpl; trivial.
      eapply relate_incr; eauto.
    Qed.


  End WITHMEM.

End Refinement.