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 Conventions.
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}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Notation LDATA := RData.

  Notation LDATAOps := (cdata (cdata_ops := pproc_data_ops) LDATA).


  Notation EptSize := 8413184.

  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 (EptSize × (CPU_ID (snd m´0)) +
                               4) Vzero = Some m0 →
      Mem.store Mint32 m0 b0 (EptSize × (CPU_ID (snd m0)) +
                              0) (Vptr b0 ofs) = Some m1 →
      Int.unsigned ofs = EptSize × (CPU_ID (snd m0)) + 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 (EptSize × (CPU_ID (snd m´0)) +
                               PgSize + (Int.unsigned pdpt) × 8 + 4) Vzero = Some m0 →
      Mem.store Mint32 m0 b0 (EptSize × (CPU_ID (snd m0)) +
                              PgSize + (Int.unsigned pdpt) × 8) (Vptr b0 ofs) = Some m1 →
      Int.unsigned ofs = EptSize × (CPU_ID (snd m0)) + ((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 (EptSize × (CPU_ID (snd m´0)) +
                               ((Int.unsigned pdpt) + 2) × PgSize +
                               ((Int.unsigned pdir) × 8) + 4) Vzero = Some m0 →
      Mem.store Mint32 m0 b0 (EptSize × (CPU_ID (snd m0)) +
                              ((Int.unsigned pdpt) + 2) × PgSize +
                              ((Int.unsigned pdir) × 8)) (Vptr b0 ofs) = Some m1 →
      Int.unsigned ofs = EptSize × (CPU_ID (snd m0)) + (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 (EptSize × (CPU_ID (snd m´0)) +
                               (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 (EptSize × (CPU_ID (snd m´0)) +
                              (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.

  Inductive ept_invalidate_mappings_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | ept_invalidate_mappings_spec_low_intro s m´0 rs b b0:
      find_symbol s ept_invalidate_mappings = Some b →
      rs PC = Vptr b Int.zero →
      asm_invariant (mem := mwd LDATAOps) s rs m´0 →
      kernel_mode (snd m´0) →
      high_level_invariant (snd m´0) →
      find_symbol s EPT_LOC = Some b0 →
      let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                 :: IR EDX :: RA :: nil)
                             (undef_regs (List.map preg_of destroyed_at_call) rs)) in
      ept_invalidate_mappings_spec_low_step s rs m´0 (rs´#PC <- (rs#RA)#EAX <- Vzero) m´0.

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    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.
    Definition ept_invalidate_mappings_spec_low: compatsem LDATAOps :=
      asmsem_withsig ept_invalidate_mappings ept_invalidate_mappings_spec_low_step
                     (mksignature nil (Some AST.Tint) cc_default).

  End WITHMEM.

End SPECIFICATION.