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 LoadStoreSem2.

Require Import TTrap.
Require Export TrapArgGen.
Require Import TrapGenSpec.

Section Refinement.

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

  Context `{real_params: RealParams}.

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

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

  Section WITHMEM.

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

    Section OneStep_Forward_Relation.

      Section FRESH_PIM.

        Lemma trap_get_quota_kernel_mode:
          ∀ d2 d2',
            trap_get_quota_spec d2 = Some d2'
            → kernel_mode d2.
        Proof.
          unfold trap_get_quota_spec. intros.
          destruct (get_curid_spec d2) eqn:Hdestruct; try discriminate.
          functional inversion Hdestruct; subst; simpl; auto.
        Qed.

        Lemma trap_get_quota_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_get_quota_spec) trap_get_quota_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_get_quota_exist; try eapply valid_curid; eauto 1.
          intros (labd' & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_get_quota_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_offer_shared_mem_kernel_mode:
          ∀ d2 d2',
            trap_offer_shared_mem_spec d2 = Some d2'
            → kernel_mode d2.
        Proof.
          unfold trap_offer_shared_mem_spec. intros.
          destruct (uctx_arg2_spec d2) eqn:Hdestruct; try discriminate.
          functional inversion Hdestruct; subst; simpl; auto.
        Qed.

        Lemma trap_offer_shared_mem_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_offer_shared_mem_spec) trap_offer_shared_mem_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_offer_shared_mem_exist; try eapply valid_curid; eauto 1.
          intros (labd' & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_offer_shared_mem_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma print_kernel_mode:
          ∀ d d',
            print_spec d = Some d'
            → kernel_mode d.
        Proof.
          unfold print_spec; intros.
          destruct (uctx_arg2_spec d) eqn:Hdestruct; try discriminate.
          functional inversion Hdestruct; subst; simpl; auto.
        Qed.

        Lemma print_spec_ref:
          compatsim (crel HDATA LDATA) (gensem print_spec) print_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit print_exist; eauto 1.
          try eapply valid_curid; eauto 1.
          intros (labd' & HP & HM).
          refine_split; try econstructor; eauto.
          - eapply print_kernel_mode; eauto.
          - constructor.
        Qed.




        Lemma trap_receivechan_kernel_mode:
          ∀ d2 d2',
            trap_receivechan_spec d2 = Some d2'
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          functional inversion H1; subst; simpl; auto.
        Qed.

        Lemma trap_receivechan_spec_ref:
          compatsim (crel HDATA LDATA) (gensem trap_receivechan_spec) trap_receivechan_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_receivechan_exist; try eapply valid_curid; eauto 1.
          intros (labd' & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_receivechan_kernel_mode; eassumption.
          - constructor.
        Qed.


        Lemma ptfault_resv_kernel_mode:
          ∀ d2 d2' v,
            ptfault_resv_spec v d2 = Some d2'
            → kernel_mode d2.
        Proof.
          intros. functional inversion H.
          - functional inversion H5.
            + functional inversion H8; subst; simpl; auto.
            + functional inversion H7; subst; simpl; auto.
          - subst; simpl; auto.
        Qed.

        Lemma ptf_resv_spec_ref:
          compatsim (crel HDATA LDATA) (gensem ptfault_resv_spec) ptf_resv_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit ptfault_resv_exist; try eapply valid_curid; eauto 1.
          intros (labd' & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply ptfault_resv_kernel_mode; eassumption.
          - constructor.
        Qed.

        Lemma trap_proc_create_kernel_mode:
          ∀ d2 d2' v1 v2,
            trap_proc_create_spec v1 v2 d2 = Some d2'
            → kernel_mode d2.
        Proof.
          unfold trap_proc_create_spec. intros.
          destruct (uctx_arg2_spec d2) eqn:Hdestruct; try discriminate.
          functional inversion Hdestruct; subst; simpl; auto.
          unfold uctx_set_errno_spec in H; subdestruct; auto.
        Qed.

        Lemma trap_proc_create_spec_ref:
          compatsim (crel HDATA LDATA) (trap_proccreate_compatsem trap_proc_create_spec) trap_proc_create_spec_low.
        Proof.
          compatsim_simpl (@match_AbData).
          exploit trap_proc_create_exist; try eapply valid_curid; eauto 1.
          intros (labd' & HM & HR).
          refine_split; try econstructor; eauto.
          - eapply trap_proc_create_kernel_mode; eassumption.
          - constructor.
        Qed.


      End FRESH_PIM.

      Lemma passthrough_correct:
        sim (crel HDATA LDATA) ttrap_passthrough ttraparg.
      Proof.
        sim_oplus.
        - apply fload_sim.
        - apply fstore_sim.
        - apply ptRead_sim.
        - apply alloc_sim.
        - apply get_curid_sim.
        - apply thread_wakeup_sim.

        - apply syncsendto_chan_pre_sim.
        - apply syncsendto_chan_post_sim.

        - apply uctx_get_sim.
        - apply uctx_set_sim.
        - apply proc_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_arg4_sim.
          intros. eapply valid_curid; eauto.
        - apply uctx_arg5_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 trap_info_get_sim.
        - apply trap_info_ret_sim.
        - apply thread_yield_sim.
        - apply thread_sleep_sim.
        - apply proc_start_user_sim.
          intros. eapply valid_curid; eauto.
        - apply proc_exit_user_sim.
        - layer_sim_simpl.
          + eapply load_correct2.
          + eapply store_correct2.
      Qed.

    End OneStep_Forward_Relation.

  End WITHMEM.

End Refinement.