***********************************************************************
*                                                                     *
*            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 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 LoadStoreSem2.
Require Import AsmImplLemma.
Require Import LAsm.
Require Import RefinementTactic.
Require Import PrimSemantics.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.ClightModules.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatClightSem.

Require Import PProc.

Require Import AbstractDataType.

Section SPECIFICATION.

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

  Context `{real_params: RealParams}.

  Notation LDATAOps := (cdata RData).

  Inductive setEPML4_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setEPML4_spec_low_intro s (WB: _ → Prop) (m´0 m0 m1: mwd LDATAOps) b0 ofs pml4_idx:
      find_symbol s EPT_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 4 Vzero = Some m0 →
      Mem.store Mint32 m0 b0 0 (Vptr b0 ofs) = Some m1 →
      Int.unsigned ofs = PgSize + EPTEPERM →
      Int.unsigned pml4_idx = 0 →
      kernel_mode (snd m´0) →
      setEPML4_spec_low_step s WB (Vint pml4_idx :: nil) m´0 Vundef m1.

  Inductive setEPDPTE_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setEPDPTE_spec_low_intro s (WB: _ → Prop) (m´0 m0 m1: mwd LDATAOps) b0 pdpt ofs pml4_idx:
      find_symbol s EPT_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 (PgSize + (Int.unsigned pdpt) × 8 + 4) Vzero = Some m0 →
      Mem.store Mint32 m0 b0 (PgSize + (Int.unsigned pdpt) × 8) (Vptr b0 ofs) = Some m1 →
      Int.unsigned ofs = ((Int.unsigned pdpt) + 2) × PgSize + EPTEPERM →
      Int.unsigned pml4_idx = 0 →
      0 ≤ Int.unsigned pdpt ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
      kernel_mode (snd m´0) →
      setEPDPTE_spec_low_step s WB (Vint pml4_idx :: Vint pdpt :: nil) m´0 Vundef m1.

  Inductive setEPDTE_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setEPDTE_spec_low_intro s (WB: _ → Prop) (m´0 m0 m1: mwd LDATAOps) b0 pdpt pdir ofs pml4_idx:
      find_symbol s EPT_LOC = Some b0 →
      Mem.store Mint32 m´0 b0 (((Int.unsigned pdpt) + 2) × PgSize +
                               ((Int.unsigned pdir) × 8) + 4) Vzero = Some m0 →
      Mem.store Mint32 m0 b0 (((Int.unsigned pdpt) + 2) × PgSize +
                               ((Int.unsigned pdir) × 8)) (Vptr b0 ofs) = Some m1 →
      Int.unsigned ofs = (6 + (Int.unsigned pdpt) × 512 + (Int.unsigned pdir))
                         × PgSize + EPTEPERM →
      Int.unsigned pml4_idx = 0 →
      0 ≤ Int.unsigned pdpt ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
      0 ≤ Int.unsigned pdir ≤ EPT_PDIR_INDEX (Int.max_unsigned) →
      kernel_mode (snd m´0) →
      setEPDTE_spec_low_step s WB (Vint pml4_idx :: Vint pdpt :: Vint pdir :: nil) m´0 Vundef m1.

  Inductive setEPTE_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    setEPTE_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 pdpt pdir ptab hpa pml4_idx:
      find_symbol s EPT_LOC = Some b0 →
      Mem.store Mint64 m´0 b0 ((6 + (Int.unsigned pdpt) × 512 + (Int.unsigned pdir)) × PgSize +
                               ((Int.unsigned ptab) × 8)) (Vlong (Int64.repr (Int.unsigned hpa))) = Some m0 →
      Int.unsigned pml4_idx = 0 →
      0 ≤ Int.unsigned pdpt ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
      0 ≤ Int.unsigned pdir ≤ EPT_PDIR_INDEX (Int.max_unsigned) →
      0 ≤ Int.unsigned ptab ≤ EPT_PTAB_INDEX (Int.max_unsigned) →
      kernel_mode (snd m´0) →
      setEPTE_spec_low_step
        s WB (Vint pml4_idx :: Vint pdpt :: Vint pdir :: Vint ptab :: Vint hpa :: nil)
                   m´0 Vundef m0.

  Inductive getEPTE_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    getEPTE_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 pdpt pdir ptab hpa pml4_idx:
      find_symbol s EPT_LOC = Some b0 →
      Mem.load Mint64 m´0 b0 ((6 + (Int.unsigned pdpt) × 512 + (Int.unsigned pdir)) × PgSize +
                               ((Int.unsigned ptab) × 8)) = Some (Vlong (Int64.repr (Int.unsigned hpa))) →
      Int.unsigned pml4_idx = 0 →
      0 ≤ Int.unsigned pdpt ≤ EPT_PDPT_INDEX (Int.max_unsigned) →
      0 ≤ Int.unsigned pdir ≤ EPT_PDIR_INDEX (Int.max_unsigned) →
      0 ≤ Int.unsigned ptab ≤ EPT_PTAB_INDEX (Int.max_unsigned) →
      kernel_mode (snd m´0) →
      getEPTE_spec_low_step s WB (Vint pml4_idx :: Vint pdpt :: Vint pdir :: Vint ptab :: nil) m´0 (Vint hpa) m´0.

  Section WITHMEM.

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

    Definition setEPML4_spec_low: compatsem LDATAOps :=
      csem setEPML4_spec_low_step (type_of_list_type (Tint32::nil)) Ctypes.Tvoid.

    Definition setEPDPTE_spec_low: compatsem LDATAOps :=
      csem setEPDPTE_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Ctypes.Tvoid.

    Definition setEPDTE_spec_low: compatsem LDATAOps :=
      csem setEPDTE_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::nil)) Ctypes.Tvoid.

    Definition setEPTE_spec_low: compatsem LDATAOps :=
      csem setEPTE_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::Tint32::Tint32::nil)) Ctypes.Tvoid.

    Definition getEPTE_spec_low: compatsem LDATAOps :=
      csem getEPTE_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::Tint32::nil)) Tint32.

  End WITHMEM.

End SPECIFICATION.