***********************************************************************
*                                                                     *
*            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 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}.

  Notation LDATA := RData.

  Notation LDATAOps := (cdata LDATA).

  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 ((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 ((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 →
      let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
      Mem.store Mint32 m0 b0 VMX_HOST_EBP (rs01 EBP) = Some m1 →
      Mem.store Mint32 m1 b0 VMX_HOST_EDI (rs01 EDI) = Some m2 →
      Mem.load Mint32 m2 b0 VMX_G_RAX = Some v0 →
      Mem.load Mint32 m2 b0 VMX_G_RBX = Some v1 →
      Mem.load Mint32 m2 b0 VMX_G_RDX = Some v2 →
      Mem.load Mint32 m2 b0 VMX_G_RSI = Some v3 →
      Mem.load Mint32 m2 b0 VMX_G_RDI = Some v4 →
      Mem.load Mint32 m2 b0 VMX_G_RBP = Some v5 →
      Mem.load Mint32 m2 b0 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) →
      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 →
      find_symbol s VMX_LOC = Some b0 →

      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_G_RDI (rs01 EDI) = Some m1 →
      Mem.store Mint32 m1 b0 VMX_G_RAX (rs01 EAX) = Some m2 →
      Mem.store Mint32 m2 b0 VMX_G_RBX (rs01 EBX) = Some m3 →
      Mem.store Mint32 m3 b0 VMX_G_RDX (rs01 EDX) = Some m4 →
      Mem.store Mint32 m4 b0 VMX_G_RSI (rs01 ESI) = Some m5 →
      Mem.store Mint32 m5 b0 VMX_G_RBP (rs01 EBP) = Some m6 →

      Mem.load Mint32 m6 b0 VMX_HOST_EBP = Some v0 →
      Mem.load Mint32 m6 b0 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_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_G_RIP (Vint v0) = Some m0 →
      Mem.store Mint32 m0 b0 VMX_EXIT_REASON (Vint v1) = Some m1 →
      Mem.store Mint32 m1 b0 VMX_EXIT_QUALIFICATION (Vint v2) = Some m2 →
      Mem.store Mint32 m2 b0 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.MemoryModel}.
    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.