Library mcertikos.virt.intel.VEPTInit

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

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

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

Require Import AbstractDataType.

Require Export VEPTOp.
Require Import LoadStoreSem3.

Abstract Data and Primitives at this 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 ept_mmap_inv: PreservesInvariants ept_mmap_spec.
    Proof.
      constructor; intros; inv_generic_sem H;
      functional inversion H2; subst; trivial.
      -
        inv H0; functional inversion H.
        constructor; trivial; intros; simpl in ×.
      -
        inv H0; functional inversion H.
        constructor; simpl; eauto 2; try congruence; intros.
      -
        functional inversion H.
        split; trivial.
    Qed.

    Global Instance ept_set_permission_inv: PreservesInvariants ept_set_permission_spec.
    Proof.
      constructor; intros; inv_generic_sem H;
      functional inversion H2; subst; trivial.
      -
        inv H0; functional inversion H.
        constructor; trivial; intros; simpl in ×.
      -
        inv H0; functional inversion H.
        constructor; simpl; eauto 2; try congruence; intros.
      -
        functional inversion H.
        split; trivial.
    Qed.

  End INV.

Layer Definition