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

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

Require Import LayerCalculusLemma.
Require Import AbstractDataType.

Require Import LoadStoreSem3high.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Require Import TDispatch.
Require Export TrapGen.
Require Import DispatchGenSpec.

Section Refinement.

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

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

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

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

  Section WITHMEM.

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

    Section OneStep_Forward_Relation.

      Section FRESH_PIM.

        Lemma sys_dispatch_c_kernel_mode:
          ∀ d2 d2´ v1 v2,
            sys_dispatch_c_spec v1 v2 d2 = Some d2´
            → kernel_mode d2.
        Proof.
          unfold sys_dispatch_c_spec. intros.
          destruct (uctx_arg1_spec d2) eqn:Hdestruct; try discriminate.
          functional inversion Hdestruct; subst; simpl; auto.
        Qed.

        Lemma sys_dispatch_c_spec_ref:
          compatsim (crel HDATA LDATA) (trap_proccreate_compatsem sys_dispatch_c_spec) sys_dispatch_c_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit sys_dispatch_c_exist; try eapply valid_curid; eauto 1.
          intros (labd´ & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply sys_dispatch_c_kernel_mode; eassumption.
          - constructor.
        Qed.

      End FRESH_PIM.

      Lemma passthrough_correct:
        sim (crel HDATA LDATA) tdispatch_passthrough ttrap.
      Proof.
        sim_oplus.         - apply thread_vmxinfo_get_sim.
        - apply big2_palloc_sim.
        - apply thread_ptRead_sim.
        - apply big2_ptResv_sim.
        - apply thread_uctx_get_sim.
        - apply thread_uctx_set_sim.

        - apply thread_get_CPU_ID_sim.
        - apply thread_get_curid_sim.

        - apply thread_vm_run_sim, VMX_INJECT.
        - apply thread_vmx_return_from_guest_sim.
        - apply thread_vmx_init_sim.

        - apply uctx_arg1_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_arg2_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_arg3_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_set_errno_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_set_retval1_sim.
          intros. eapply valid_curid; eauto.
        - apply ptfault_resv_sim.
          intros. eapply valid_curid; eauto.

        - apply thread_cli_sim.
        - apply thread_sti_sim.

        - apply thread_trap_info_get_sim.
        - apply thread_trap_info_ret_sim.
        - apply thread_proc_start_user_sim.
          intros. eapply valid_curid; eauto.
        - apply thread_proc_exit_user_sim.
        - apply thread_proc_start_user_sim2.
          intros. eapply valid_curid; eauto.
        - apply thread_proc_exit_user_sim2.
        - layer_sim_simpl.
          + eapply load_correct3high.
          + eapply store_correct3high.
      Qed.
    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.