Library mcertikos.proc.PUCtxtIntro


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 INVLemmaContainer.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaProc.

Require Import ObjProc.
Require Import PUCtxtIntroDef.

Require Import AbstractDataType.

Require Export PQThread.
Require Import LoadStoreSem2.

Abstract Data and Primitives at this layer

Section WITHMEM.

  Local Open Scope Z_scope.

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

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

Proofs that the primitives satisfies the invariants at this layer

  Section INV.

    Global Instance uctx_set_inv: PreservesInvariants uctx_set_spec.
    Proof.
      preserves_invariants_simpl low_level_invariant high_level_invariant; eauto 2.
      eapply uctxt_inject_neutral_gss; eauto.
      eapply uctxt_inject_neutral0_gss; eauto.
      eapply uctxt_inject_neutral0_Vint.
    Qed.

    Global Instance uctx_set_eip_inv: UCTXSetEIPInvariants uctx_set_eip_spec.
    Proof.
      constructor; intros.
      -
        inv H1. functional inversion H; inv H.
        constructor; trivial.
        eapply uctxt_inject_neutral_gss; eauto.
        eapply uctxt_inject_neutral0_gss; eauto.
        eapply uctxt_inject_neutral0_Vptr_flat; eauto.
      -
        inv H0. functional inversion H; inv H.
        constructor; trivial.
      -
        functional inversion H; inv H.
        constructor; trivial.
    Qed.

    Global Instance save_uctx_inv: SaveUCtxInvariants save_uctx_spec.
    Proof.
      constructor; intros.
      -
        inv H0. functional inversion H; inv H.
        constructor; trivial.
        eapply uctxt_inject_neutral_gss; eauto.
        repeat eapply uctxt_inject_neutral0_gss;
          try eapply uctxt_inject_neutral0_Vint.
        apply uctxt_inject_neutral0_init; eauto.
      -
        inv H0. functional inversion H; inv H.
        constructor; trivial.
      -
        functional inversion H; inv H.
        constructor; trivial.
    Qed.

    Global Instance restore_uctx_inv: RestoreUCtxInvariants restore_uctx_spec.
    Proof.
      constructor; intros.
      -
        inv H0. functional inversion H; inv H.
        constructor; trivial.
      -
        inv H0. functional inversion H; inv H.
        subst. constructor; auto; simpl in *; intros; try congruence.
    Qed.

  End INV.

Layer Definition

  Definition puctxtintro_fresh_c : compatlayer (cdata RData) :=
    uctx_get gensem uctx_get_spec
              uctx_set gensem uctx_set_spec
              uctx_set_eip uctx_set_eip_compatsem uctx_set_eip_spec
              save_uctx save_uctx_compatsem save_uctx_spec.

  Definition puctxtintro_fresh_asm : compatlayer (cdata RData) :=
    restore_uctx primcall_restoreuctx_compatsem restore_uctx_spec (fun abdZMap.get (CPU_ID abd) (cid abd))
                  elf_load elf_load_compatsem.

  Definition puctxtintro_passthrough : compatlayer (cdata RData) :=
    fload gensem fload_spec
           fstore gensem fstore_spec
           vmxinfo_get gensem vmxinfo_get_spec
           palloc gensem palloc_spec
          
           set_pt gensem setPT_spec
           pt_read gensem ptRead_spec
           pt_resv gensem ptResv_spec
           shared_mem_status gensem shared_mem_status_spec
           offer_shared_mem gensem offer_shared_mem_spec
          
           thread_spawn dnew_compatsem biglow_thread_spawn_spec
           thread_wakeup gensem biglow_thread_wakeup_spec
           thread_yield primcall_thread_schedule_compatsem biglow_thread_yield_spec (prim_ident:= thread_yield)
           thread_sleep primcall_thread_transfer_compatsem biglow_thread_sleep_spec
           sched_init gensem biglow_sched_init_spec

           pt_in primcall_general_compatsem´ ptin_spec (prim_ident:= pt_in)
           pt_out primcall_general_compatsem´ ptout_spec (prim_ident:= pt_out)
           container_get_nchildren gensem container_get_nchildren_spec
           container_get_quota gensem container_get_quota_spec
           container_get_usage gensem container_get_usage_spec
           container_can_consume gensem container_can_consume_spec

           get_CPU_ID gensem get_CPU_ID_spec
           get_curid gensem get_curid_spec
          

           acquire_lock_CHAN gensem acquire_lock_SC_spec
           release_lock_CHAN gensem release_lock_SC_spec
           get_sync_chan_busy gensem get_sync_chan_busy_spec
           set_sync_chan_busy gensem set_sync_chan_busy_spec

          
          
          
          
          
           ipc_send_body gensem ipc_send_body_spec
           ipc_receive_body gensem ipc_receive_body_spec

          
          
          

           cli gensem cli_spec
           sti gensem sti_spec
           serial_intr_disable gensem serial_intr_disable_spec
           serial_intr_enable gensem serial_intr_enable_spec
           serial_putc gensem serial_putc_spec
           cons_buf_read gensem cons_buf_read_spec

           proc_create_postinit gensem proc_create_postinit_spec
           trap_in primcall_general_compatsem trapin_spec
           trap_out primcall_general_compatsem trapout_spec
           host_in primcall_general_compatsem hostin_spec
           host_out primcall_general_compatsem hostout_spec
           trap_get primcall_trap_info_get_compatsem trap_info_get_spec
           trap_set primcall_trap_info_ret_compatsem trap_info_ret_spec
           accessors {| exec_load := (@exec_loadex _ _ _ _ _ _ _ _ _ _ _ _ _ Hmwd);
                           exec_store := (@exec_storeex _ _ _ _ _ _ _ _ _ _ _ _ _ Hmwd) |}.

  Definition puctxtintro : compatlayer (cdata RData) :=
    (puctxtintro_fresh_c puctxtintro_fresh_asm) puctxtintro_passthrough.

End WITHMEM.