***********************************************************************
*                                                                     *
*            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 AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import Conventions.
Require Import VVMCSIntro.
Require Import AbstractDataType.
Require Import mCertiKOSType.

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

Section SPECIFICATION.

  Context `{real_params: RealParams}.

  Notation LDATA := RData.

  Notation LDATAOps := (cdata LDATA).

  Inductive vmx_set_intercept_intwin_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_set_intercept_intwin_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ enable:
      vmx_set_intercept_intwin_spec (Int.unsigned enable) labd = Some labd´ →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_set_intercept_intwin_spec_low_step s WB (Vint enable :: nil) (m´0, labd) Vundef (m´0, labd´).

  Inductive vmx_set_desc_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_set_desc_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ seg sel base lim ar:
      vmx_set_desc_spec (Int.unsigned seg) (Int.unsigned sel) (Int.unsigned base)
        (Int.unsigned lim) (Int.unsigned ar) labd = Some labd´ →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_set_desc_spec_low_step s WB (Vint seg :: Vint sel :: Vint base :: Vint lim :: Vint ar :: nil) (m´0, labd) Vundef (m´0, labd´).

  Inductive vmx_inject_event_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_inject_event_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ type vector errcode ev:
      vmx_inject_event_spec (Int.unsigned type) (Int.unsigned vector)
        (Int.unsigned errcode) (Int.unsigned ev) labd = Some labd´ →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_inject_event_spec_low_step s WB (Vint type :: Vint vector :: Vint errcode :: Vint ev :: nil) (m´0, labd) Vundef (m´0, labd´).

  Inductive vmx_set_tsc_offset_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_set_tsc_offset_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ tsc_offset:
      vmx_set_tsc_offset_spec (VZ64 (Int64.unsigned tsc_offset)) labd = Some labd´ →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_set_tsc_offset_spec_low_step s WB (Vlong tsc_offset::nil) (m´0, labd) Vundef (m´0, labd´).

  Inductive vmx_get_tsc_offset_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_tsc_offset_spec_low_intro s (WB: _ → Prop) m´0 labd tsc_offset:
      vmx_get_tsc_offset_spec labd = Some (VZ64 (Int64.unsigned tsc_offset)) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_tsc_offset_spec_low_step s WB nil (m´0, labd) (Vlong tsc_offset) (m´0, labd).

  Inductive vmx_get_exit_reason_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_exit_reason_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_exit_reason_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_exit_reason_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_get_exit_fault_addr_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_exit_fault_addr_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_exit_fault_addr_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_exit_fault_addr_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_check_pending_event_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_check_pending_event_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_check_pending_event_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_check_pending_event_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_check_int_shadow_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_check_int_shadow_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_check_int_shadow_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_check_int_shadow_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmcs_set_defaults_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmcs_set_defaults_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ mbi_adr pml4ept_b tss_b gdt_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
      vmcs_set_defaults_spec (Int.unsigned mbi_adr) pml4ept_b tss_b gdt_b idt_b msr_bitmap_b io_bitmap_b host_rip_b labd = Some labd´ →
      find_symbol s EPT_LOC = Some pml4ept_b →
      find_symbol s tss_LOC = Some tss_b →
      find_symbol s gdt_LOC = Some gdt_b →
      find_symbol s idt_LOC = Some idt_b →
      find_symbol s msr_bitmap_LOC = Some msr_bitmap_b →
      find_symbol s io_bitmap_LOC = Some io_bitmap_b →
      find_symbol s vmx_return_from_guest = Some host_rip_b →
      kernel_mode labd →
      high_level_invariant labd →
      vmcs_set_defaults_spec_low_step s WB (Vint mbi_adr::nil) (m´0, labd) (Vundef) (m´0, labd´).

  Section WITHMEM.

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

    Notation Tint64 := (Tlong Unsigned noattr).

    Definition vmx_set_intercept_intwin_spec_low: compatsem LDATAOps :=
      csem vmx_set_intercept_intwin_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.

    Definition vmx_set_desc_spec_low: compatsem LDATAOps :=
      csem vmx_set_desc_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::Tint32::Tint32::nil)) Tvoid.

    Definition vmx_inject_event_spec_low: compatsem LDATAOps :=
      csem vmx_inject_event_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::Tint32::nil)) Tvoid.

    Definition vmx_set_tsc_offset_spec_low: compatsem LDATAOps :=
      csem vmx_set_tsc_offset_spec_low_step (type_of_list_type (Tint64::nil)) Tvoid.

    Definition vmx_get_tsc_offset_spec_low: compatsem LDATAOps :=
      csem vmx_get_tsc_offset_spec_low_step Tnil Tint64.

    Definition vmx_get_exit_reason_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_reason_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_fault_addr_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_fault_addr_spec_low_step Tnil Tint32.

    Definition vmx_check_pending_event_spec_low: compatsem LDATAOps :=
      csem vmx_check_pending_event_spec_low_step Tnil Tint32.

    Definition vmx_check_int_shadow_spec_low: compatsem LDATAOps :=
      csem vmx_check_int_shadow_spec_low_step Tnil Tint32.

    Definition vmcs_set_defaults_spec_low: compatsem LDATAOps :=
      csem vmcs_set_defaults_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.

  End WITHMEM.

End SPECIFICATION.