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


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

  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_desc1_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_set_desc1_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ seg sel base:
      vmx_set_desc1_spec (Int.unsigned seg) (Int.unsigned sel) (Int.unsigned base) labd = Some labd´ →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_set_desc1_spec_low_step s WB (Vint seg :: Vint sel :: Vint base :: nil) (m´0, labd) Vundef (m´0, labd´).

  Inductive vmx_set_desc2_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_set_desc2_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ seg lim ar:
      vmx_set_desc2_spec (Int.unsigned seg) (Int.unsigned lim) (Int.unsigned ar) labd = Some labd´ →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_set_desc2_spec_low_step s WB (Vint seg :: 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´ pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
      vmcs_set_defaults_spec pml4ept_b stack_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 STACK_LOC = Some stack_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 nil (m´0, labd) (Vundef) (m´0, labd´).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    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_desc1_spec_low: compatsem LDATAOps :=
      csem vmx_set_desc1_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::nil)) Tvoid.

    Definition vmx_set_desc2_spec_low: compatsem LDATAOps :=
      csem vmx_set_desc2_spec_low_step (type_of_list_type (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 Tnil Tvoid.

  End WITHMEM.

End SPECIFICATION.