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 VVMCSInit.
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 LDATA := RData.

  Notation LDATAOps := (cdata LDATA).

  Definition vmx_size := VMX_Size´ × 4.

  Inductive vmx_readz_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    vmx_readz_spec_low_intro s (WB: _ → Prop) (m´0: mwd LDATAOps) b0 i v:
      find_symbol s VMX_LOC = Some b0 →
      0 ≤ (Int.unsigned i) < VMX_Size´ →
      Mem.load Mint32 m´0 b0 (vmx_size × (CPU_ID (snd m´0)) + (Int.unsigned i) × 4) = Some (Vint v) →
      kernel_mode (snd m´0) →
      vmx_readz_spec_low_step s WB (Vint i :: nil) m´0 (Vint v) m´0.

  Inductive vmx_writez_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    vmx_writez_spec_low_intro s (WB: _ → Prop) (m´0 m0: mwd LDATAOps) b0 i v:
      find_symbol s VMX_LOC = Some b0 →
      0 ≤ (Int.unsigned i) < VMX_Size´ →
      Mem.store Mint32 m´0 b0 (vmx_size × (CPU_ID (snd m´0)) + (Int.unsigned i) × 4) (Vint v) = Some m0 →
      kernel_mode (snd m´0) →
      vmx_writez_spec_low_step s WB (Vint i :: Vint v :: nil) m´0 Vundef m0.

  Inductive vmx_enter_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    vmx_enter_spec_low_intro s v0 v1 v2 v3 v4 v5 v6
                             (m0 m1 m2: mem) b0 rs rs´ labd labd´ b:
      find_symbol s vmx_enter = Some b →
      rs PC = Vptr b Int.zero →
      find_symbol s VMX_LOC = Some b0 →
      high_level_invariant labd →
      let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
      Mem.store Mint32 m0 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EBP) (rs01 EBP) = Some m1 →
      Mem.store Mint32 m1 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EDI) (rs01 EDI) = Some m2 →
      Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RAX) = Some v0 →
      Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBX) = Some v1 →
      Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDX) = Some v2 →
      Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RSI) = Some v3 →
      Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDI) = Some v4 →
      Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBP) = Some v5 →
      Mem.load Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RIP) = Some v6 →
      rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                            :: RA :: nil)
                        (undef_regs (List.map preg_of destroyed_at_call) rs)) →
      hostout_spec labd = Some labd´ →
      kernel_mode labd →
      asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
      rs ESP ≠ Vundef →
      (∀ b1 o,
         rs ESP = Vptr b1 o →
         Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m0)) →
      vmx_enter_spec_low_step s rs (m0, labd)
                              (rs´#Asm.EAX <- v0 #Asm.EBX <- v1 #Asm.EDX <- v2 #Asm.ESI<- v3#Asm.EDI <- v4
                                  #EBP<- v5 #PC <- v6) (m2, labd´).

  Inductive vmx_exit_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    vmx_exit_spec_low_intro s v0 v1
                             (m0 m1 m2 m3 m4 m5 m6: mem) b0 rs rs´ labd b:
      find_symbol s vmx_exit = Some b →
      rs PC = Vptr b Int.zero →
      rs ECX = Vint (Int.repr (CPU_ID labd × (38 × 4))) →
      find_symbol s VMX_LOC = Some b0 →
      high_level_invariant labd →

      let rs01 := (Pregmap.init Vundef) #EAX <- (rs EAX) #EBX <- (rs EBX)
                                        #EDX <- (rs EDX) #EDI <- (rs EDI)
                                        #ESI <- (rs ESI) #EBP <- (rs EBP) in

      Mem.store Mint32 m0 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDI) (rs01 EDI) = Some m1 →
      Mem.store Mint32 m1 b0 (vmx_size × (CPU_ID labd) + VMX_G_RAX) (rs01 EAX) = Some m2 →
      Mem.store Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBX) (rs01 EBX) = Some m3 →
      Mem.store Mint32 m3 b0 (vmx_size × (CPU_ID labd) + VMX_G_RDX) (rs01 EDX) = Some m4 →
      Mem.store Mint32 m4 b0 (vmx_size × (CPU_ID labd) + VMX_G_RSI) (rs01 ESI) = Some m5 →
      Mem.store Mint32 m5 b0 (vmx_size × (CPU_ID labd) + VMX_G_RBP) (rs01 EBP) = Some m6 →

      Mem.load Mint32 m6 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EBP) = Some v0 →
      Mem.load Mint32 m6 b0 (vmx_size × (CPU_ID labd) + VMX_HOST_EDI) = Some v1 →
      

      rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                            :: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
                        (undef_regs (List.map preg_of destroyed_at_call) rs)) →
      kernel_mode labd →
      asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
      vmx_exit_spec_low_step s rs (m0, labd)
                              (rs´#Asm.EBP <- v0 #Asm.EDI <- v1 #PC <- (rs RA)) (m6, labd).


  Inductive vmx_enter_pre_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    vmx_enter_pre_spec_low_intro s (WB: _ → Prop) m´0 b0 v0 labd labd´:
      find_symbol s VMX_LOC = Some b0 →
      Mem.load Mint32 m´0 b0 (vmx_size × (CPU_ID labd) + VMX_G_RIP) = Some (Vint v0) →
      vmcs_writez_spec C_VMCS_GUEST_RIP (Int.unsigned v0) labd = Some labd´ →
      kernel_mode labd →
      vmx_enter_pre_spec_low_step s WB nil (m´0, labd) Vundef (m´0, labd´).


  Inductive vmx_exit_post_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
    vmx_exit_post_spec_low_intro s (WB: _ → Prop) m´0 m0 m2 m1 m3 b0 v0 v1 v2 labd:
      find_symbol s VMX_LOC = Some b0 →
      vmcs_readz_spec C_VMCS_GUEST_RIP labd = Some (Int.unsigned v0) →
      vmcs_readz_spec C_VMCS_EXIT_REASON labd = Some (Int.unsigned v1) →
      vmcs_readz_spec C_VMCS_EXIT_QUALIFICATION labd = Some (Int.unsigned v2) →

      Mem.store Mint32 m´0 b0 (vmx_size × (CPU_ID labd) + VMX_G_RIP) (Vint v0) = Some m0 →
      Mem.store Mint32 m0 b0 (vmx_size × (CPU_ID labd) + VMX_EXIT_REASON) (Vint v1) = Some m1 →
      Mem.store Mint32 m1 b0 (vmx_size × (CPU_ID labd) + VMX_EXIT_QUALIFICATION) (Vint v2) = Some m2 →
      Mem.store Mint32 m2 b0 (vmx_size × (CPU_ID labd) + VMX_LAUNCHED) Vone = Some m3 →
      kernel_mode labd →
      vmx_exit_post_spec_low_step s WB nil (m´0, labd) Vundef (m3, labd).

  Section WITHMEM.

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

    Notation Tint64 := (Tlong Unsigned noattr).

    Definition vmx_readz_spec_low: compatsem LDATAOps :=
      csem vmx_readz_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition vmx_writez_spec_low: compatsem LDATAOps :=
      csem vmx_writez_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition vmx_enter_pre_spec_low: compatsem LDATAOps :=
      csem vmx_enter_pre_spec_low_step Tnil Tvoid.

    Definition vmx_exit_post_spec_low: compatsem LDATAOps :=
      csem vmx_exit_post_spec_low_step Tnil Tvoid.

    Definition vmx_exit_spec_low: compatsem LDATAOps :=
      asmsem_withsig vmx_exit vmx_exit_spec_low_step (mksignature nil None cc_default).

    Definition vmx_enter_spec_low: compatsem LDATAOps :=
      asmsem_withsig vmx_enter vmx_enter_spec_low_step (mksignature nil None cc_default).

  End WITHMEM.

End SPECIFICATION.