Library mcertikos.proc.PKContextNew

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
***********************************************************************

This file defines the abstract data and the primitives for the PKContext layer, which will introduce abstraction of kernel context

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 LoadStoreSem2.
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 CalRealPTB.
Require Import CalRealSMSPool.

Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import INVLemmaContainer.

Require Export PKContext.
Require Import AbstractDataType.

Abstract Data and Primitives at MPMap layer

The abstract data at MPMap layer is the same with MPTNew layer

Section WITHMEM.

  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.

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

Proofs that the primitives satisfies the invariants at this layer

  Section INV.

    Global Instance kctxt_new_inv: DNewInvariants ObjThread.kctxt_new_spec.
    Proof.
      constructor; intros; inv H0;
      unfold ObjThread.kctxt_new_spec in *;
      subdestruct; inv H; simpl; auto.
      -
        constructor; trivial; intros; simpl in ×.
        eapply kctxt_inject_neutral_gss_flatinj´; eauto.
        eapply kctxt_inject_neutral_gss_flatinj; eauto.

      -
        constructor; simpl; eauto 2; try congruence; intros.
        + exploit split_container_valid; eauto.
          assert (Htmp:= a0); decompose [and] Htmp; eapply container_split_some´; eauto.
          auto.
        + eapply ptb_true_set_true; eauto.
        + eapply PTB_defined_defined_true; eauto.
        + eapply container_split_PTB_AC_valid´; eauto.
    Qed.

  End INV.

Layer Definition