Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import XOmega.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.

Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaProc.

Require Import AbstractDataType.

Require Import LoadStoreSem2.
Require Export TTrapArg.
Require Export ObjTrap.
Require Export TrapPrimSemantics.

Section WITHMEM.

  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.

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

  Section Prim.

    Section TRAP_GET_QUOTA.

      Lemma trap_get_quota_high_inv:
        ∀ d d',
          trap_get_quota_spec d = Some d'→
          high_level_invariant d →
          high_level_invariant d'.
      Proof.
        intros. functional inversion H.
        eapply uctx_set_errno_high_inv; try eassumption.
        eapply uctx_set_retval1_high_inv; eassumption.
      Qed.

      Lemma trap_get_quota_low_inv:
        ∀ d d' n,
          trap_get_quota_spec d = Some d'→
          low_level_invariant n d →
          low_level_invariant n d'.
      Proof.
        intros. functional inversion H.
        eapply uctx_set_errno_low_inv; try eassumption.
        eapply uctx_set_retval1_low_inv; eassumption.
      Qed.

      Lemma trap_get_quota_kernel_mode:
        ∀ d d',
          trap_get_quota_spec d = Some d'→
          kernel_mode d →
          kernel_mode d'.
      Proof.
        intros. functional inversion H.
        eapply uctx_set_errno_kernel_mode; try eassumption.
        eapply uctx_set_retval1_kernel_mode; eassumption.
      Qed.

      Global Instance trap_get_quota_inv: PreservesInvariants trap_get_quota_spec.
      Proof.
        preserves_invariants_simpl';
          [ eapply trap_get_quota_low_inv
          | eapply trap_get_quota_high_inv
          | eapply trap_get_quota_kernel_mode ];
          eassumption.
      Qed.

    End TRAP_GET_QUOTA.

    Section PRINT.

      Lemma print_high_inv:
        ∀ d d',
          print_spec d = Some d'→
          high_level_invariant d →
          high_level_invariant d'.
      Proof.
        intros. functional inversion H. subst; simpl.
        eapply uctx_set_errno_high_inv; try eassumption.
        inv H0; split; trivial.
      Qed.

      Lemma print_low_inv:
        ∀ d d' n,
          print_spec d = Some d'→
          low_level_invariant n d →
          low_level_invariant n d'.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; try eassumption.
        inv H0; split; trivial.
      Qed.

      Lemma print_kernel_mode:
        ∀ d d',
          print_spec d = Some d'→
          kernel_mode d →
          kernel_mode d'.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; try eassumption.
      Qed.

      Global Instance print_inv: PreservesInvariants print_spec.
      Proof.
        preserves_invariants_simpl'.
        - eapply print_low_inv; eauto.
        - eapply print_high_inv; eauto.
        - eapply print_kernel_mode; eauto.
      Qed.

    End PRINT.



    Section TRAP_CHAN_RECEIVE.

      Lemma trap_receivechan_high_inv:
        ∀ d d',
          trap_receivechan_spec d = Some d'→
          high_level_invariant d →
          high_level_invariant d'.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
        eapply syncreceive_chan_high_level_inv; eauto.
      Qed.

      Lemma trap_receivechan_low_inv:
        ∀ d d' n,
          trap_receivechan_spec d = Some d'→
          low_level_invariant n d →
          low_level_invariant n d'.
      Proof.
        intros. functional inversion H; subst; simpl.
        eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
        eapply syncreceive_chan_low_level_inv; eauto.
      Qed.

      Lemma trap_receivechan_kernel_mode:
        ∀ d d',
          trap_receivechan_spec d = Some d'→
          kernel_mode d →
          kernel_mode d'.
      Proof.
        intros. functional inversion H; subst.
        eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
        eapply syncreceive_chan_kernel_mode; eauto.
      Qed.

      Global Instance trap_receivechan_inv: PreservesInvariants trap_receivechan_spec.
      Proof.
        preserves_invariants_simpl'.
        - eapply trap_receivechan_low_inv; eauto.
        - eapply trap_receivechan_high_inv; eauto.
        - eapply trap_receivechan_kernel_mode; eauto.
      Qed.

    End TRAP_CHAN_RECEIVE.


    Section PTFault_RESV_INV.

      Lemma ptfault_resv_high_inv:
        ∀ d d' i,
          ptfault_resv_spec i d = Some d'→
          high_level_invariant d →
          high_level_invariant d'.
      Proof.
        intros; functional inversion H; subst; simpl; trivial.
        eapply ptResv_high_level_inv; eauto.
      Qed.

      Lemma ptfault_resv_low_inv:
        ∀ d d' i n,
          ptfault_resv_spec i d = Some d'→
          low_level_invariant n d →
          low_level_invariant n d'.
      Proof.
        intros; functional inversion H; subst; simpl; trivial.
        eapply ptResv_low_level_inv; eauto.
      Qed.

      Lemma ptfault_resv_kernel_mode:
        ∀ d d' i,
          ptfault_resv_spec i d = Some d'→
          kernel_mode d →
          kernel_mode d'.
      Proof.
        intros; functional inversion H; subst; trivial;
        eapply ptResv_kernel_mode; eauto.
      Qed.

      Global Instance ptfault_resv_inv: PreservesInvariants ptfault_resv_spec.
      Proof.
        preserves_invariants_simpl'.
        - eapply ptfault_resv_low_inv; eauto.
        - eapply ptfault_resv_high_inv; eauto.
        - eapply ptfault_resv_kernel_mode; eauto.
      Qed.

    End PTFault_RESV_INV.

    Global Instance trap_proc_create_inv: TrapProcCreateINV trap_proc_create_spec.
    Proof.
      destruct proc_create_inv.
      split; unfold trap_proc_create_spec; intros;
        destruct (uctx_arg3_spec d); try discriminate H;
        destruct (zle_le 0 z
                         (cquota (ZMap.get (cid d) (AC d)) -
                          cusage (ZMap.get (cid d) (AC d)))) eqn:Hquota; subdestruct; auto.
      - eapply uctx_set_errno_high_inv; eauto.
        eapply uctx_set_retval1_high_inv; eauto.
        eapply pcreate_high_level_invariant; eauto.
      - eapply uctx_set_errno_high_inv; eauto.
      - eapply uctx_set_errno_high_inv; eauto.
      - eapply uctx_set_errno_high_inv; eauto.
      - eapply uctx_set_errno_low_inv; eauto.
        eapply uctx_set_retval1_low_inv; eauto.
        eapply pcreate_low_level_invariant; eauto;
        eapply stencil_find_symbol_inject'; eauto;
        eapply flat_inj_inject_incr; assumption.
      - eapply uctx_set_errno_low_inv; eauto.
      - eapply uctx_set_errno_low_inv; eauto.
      - eapply uctx_set_errno_low_inv; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
        eapply uctx_set_retval1_kernel_mode; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
      - eapply uctx_set_errno_kernel_mode; eauto.
      - eapply Mem.load_extends in Hdestruct9; eauto.
        destruct Hdestruct9 as [v2[HLD HV]].
        inv HV. subrewrite'.
      - pose proof H1 as Hsymbol. apply H1 in Hdestruct8.
        eapply Mem.load_inject in Hdestruct9; eauto.
        destruct Hdestruct9 as [v2[HLD HV]].
        rewrite Z.add_0_r in HLD. subst.
        rewrite HLD. inv HV; eauto.
        rewrite H4 in Hdestruct8.
        inv Hdestruct8. rewrite Int.add_zero.
        subrewrite'.
    Qed.

    Section TRAP_SHARE.

      Lemma trap_offer_shared_mem_high_inv:
        ∀ d d',
          trap_offer_shared_mem_spec d = Some d'→
          high_level_invariant d →
          high_level_invariant d'.
      Proof.
        intros. functional inversion H. subst; simpl.
        - eapply uctx_set_errno_high_inv; try eassumption.
          eapply uctx_set_retval1_high_inv; try eassumption.
          eapply offer_shared_mem_high_level_inv; eauto.
        - eapply uctx_set_errno_high_inv; try eassumption.
      Qed.

      Lemma trap_offer_shared_mem_low_inv:
        ∀ d d' n,
          trap_offer_shared_mem_spec d = Some d'→
          low_level_invariant n d →
          low_level_invariant n d'.
      Proof.
        intros. functional inversion H; subst; simpl.
        - eapply uctx_set_errno_low_inv; try eassumption.
          eapply uctx_set_retval1_low_inv; try eassumption.
          eapply offer_shared_mem_low_level_inv; eauto.
        - eapply uctx_set_errno_low_inv; try eassumption.
      Qed.

      Lemma trap_offer_shared_mem_kernel_mode:
        ∀ d d',
          trap_offer_shared_mem_spec d = Some d'→
          kernel_mode d →
          kernel_mode d'.
      Proof.
        intros. functional inversion H; subst.
        - eapply uctx_set_errno_kernel_mode; try eassumption.
          eapply uctx_set_retval1_kernel_mode; try eassumption.
          eapply offer_shared_mem_kernel_mode; eauto.
        - eapply uctx_set_errno_kernel_mode; try eassumption.
      Qed.

      Global Instance trap_offer_shared_mem_inv: PreservesInvariants trap_offer_shared_mem_spec.
      Proof.
        preserves_invariants_simpl'.
        - eapply trap_offer_shared_mem_low_inv; eauto.
        - eapply trap_offer_shared_mem_high_inv; eauto.
        - eapply trap_offer_shared_mem_kernel_mode; eauto.
      Qed.

    End TRAP_SHARE.

  End Prim.

  Definition ttrap_fresh : compatlayer (cdata RData) :=
    ptfault_resv ↦ gensem ptfault_resv_spec
                  ⊕ sys_proc_create ↦ trap_proccreate_compatsem trap_proc_create_spec
                  ⊕ sys_get_quota ↦ gensem trap_get_quota_spec
                  
                  ⊕ sys_receive_chan ↦ gensem trap_receivechan_spec
                  ⊕ sys_offer_shared_mem ↦ gensem trap_offer_shared_mem_spec
                  ⊕ print ↦ gensem print_spec
                  .

  Definition ttrap_passthrough : compatlayer (cdata RData) :=
    fload ↦ gensem fload_spec
          ⊕ fstore ↦ gensem fstore_spec
          
          ⊕ pt_read ↦ gensem ptRead_spec
          ⊕ container_alloc ↦ gensem alloc_spec
          
          ⊕ get_curid ↦ gensem get_curid_spec
          ⊕ thread_wakeup ↦ gensem thread_wakeup_spec

          ⊕ syncsendto_chan_pre ↦ gensem syncsendto_chan_pre_spec
          ⊕ syncsendto_chan_post ↦ gensem syncsendto_chan_post_spec

          ⊕ uctx_get ↦ gensem uctx_get_spec
          ⊕ uctx_set ↦ gensem uctx_set_spec

          
          ⊕ proc_init ↦ gensem proc_init_spec
          ⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
          ⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
          ⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
          ⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
          ⊕ uctx_arg5 ↦ gensem uctx_arg5_spec
          ⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
          ⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec

          ⊕ trap_get ↦ primcall_trap_info_get_compatsem trap_info_get_spec
          ⊕ trap_set ↦ primcall_trap_info_ret_compatsem trap_info_ret_spec
          ⊕ thread_yield ↦ primcall_thread_schedule_compatsem thread_yield_spec (prim_ident:= thread_yield)
          ⊕ thread_sleep ↦ primcall_thread_transfer_compatsem thread_sleep_spec
          ⊕ proc_start_user ↦ primcall_start_user_compatsem proc_start_user_spec
          ⊕ proc_exit_user ↦ primcall_exit_user_compatsem proc_exit_user_spec
          ⊕ accessors ↦ {| exec_load := (@exec_loadex _ _ Hmwd);
                           exec_store := (@exec_storeex _ _ Hmwd) |}.

  Definition ttrap : compatlayer (cdata RData) := ttrap_fresh ⊕ ttrap_passthrough.

End WITHMEM.