***********************************************************************
*                                                                     *
*            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 VVMXIntro.
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_get_reg_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmcs_get_reg_spec_low_intro s (WB: _ → Prop) m´0 labd reg res:
      vmx_get_reg_spec (Int.unsigned reg) labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_reg_spec_low_step s WB (Vint reg :: nil) (m´0, labd) (Vint res) (m´0, labd).

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

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

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

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

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

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

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

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

  Inductive vmx_init_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_init_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:
      vmx_init_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 →
      vmx_init_spec_low_step s WB (Vint mbi_adr :: nil) (m´0, labd) Vundef (m´0, labd´).

  Inductive vmx_run_vm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    vm_run_spec_low_intro s m0 labd labd´ b (rs rs´: regset):
      find_symbol s vmx_run_vm = Some b →
      rs PC = Vptr b Int.zero →
      let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
      vm_run_spec rs01 labd = Some (labd´, rs´) →
      asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
      low_level_invariant (Mem.nextblock m0) labd →
      high_level_invariant labd →
      rs ESP ≠ Vundef →
      (∀ b1 o,
         rs ESP = Vptr b1 o →
         Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m0)) →
      let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
                             (undef_regs (List.map preg_of destroyed_at_call) rs)) in
      vmx_run_vm_spec_low_step s rs (m0, labd) (rs0#EAX<- (rs´#EAX)#EBX <- (rs´#EBX)#EDX <- (rs´#EDX)
                                                   #ESI <- (rs´#ESI)#EDI <- (rs´#EDI)#EBP <- (rs´#EBP)
                                                   #PC <- (rs´#RA)) (m0, labd´).


  Inductive vmx_return_from_guest_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | vmx_return_from_guest_low_intro s m0 labd labd´ rs rs´ b:
      find_symbol s vmx_return_from_guest = Some b →
      rs PC = Vptr b Int.zero →
      let rs01 := (Pregmap.init Vundef) #EAX <- (rs EAX) #EBX <- (rs EBX)
                                        #EDX <- (rs EDX) #EDI <- (rs EDI)
                                        #ESI <- (rs ESI) #EBP <- (rs EBP) in
      vmx_return_from_guest_spec rs01 labd = Some (labd´, rs´) →
      asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
      low_level_invariant (Mem.nextblock m0) labd →
      high_level_invariant labd →
      rs ESP ≠ Vundef →
      (∀ b1 o,
         rs ESP = Vptr b1 o →
         Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m0)) →
      let rs0 := (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))
                   # EDI <- (ZMap.get U_EDI rs´)# ESI <- (ZMap.get U_ESI rs´)
                   # EBP <- (ZMap.get U_EBP rs´)# ESP <- (ZMap.get U_ESP rs´)
                   # EBX <- (ZMap.get U_EBX rs´)# EDX <- (ZMap.get U_EDX rs´)
                   # ECX <- (ZMap.get U_ECX rs´)# EAX <- (ZMap.get U_EAX rs´)
                   # PC <- (ZMap.get U_EIP rs´) in
      vmx_return_from_guest_spec_low_step
        s rs (m0, labd) rs0 (m0, labd´).

  Section WITHMEM.

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

    Definition vmx_get_reg_spec_low: compatsem LDATAOps :=
      csem vmx_get_reg_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition vmx_set_reg_spec_low: compatsem LDATAOps :=
      csem vmx_set_reg_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition vmx_get_next_eip_spec_low: compatsem LDATAOps :=
      csem vmx_get_next_eip_spec_low_step Tnil Tint32.

    Definition vmx_get_io_width_spec_low: compatsem LDATAOps :=
      csem vmx_get_io_width_spec_low_step Tnil Tint32.

    Definition vmx_get_io_write_spec_low: compatsem LDATAOps :=
      csem vmx_get_io_write_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_io_rep_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_io_rep_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_io_str_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_io_str_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_io_port_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_io_port_spec_low_step Tnil Tint32.

    Definition vmx_set_mmap_spec_low: compatsem LDATAOps :=
      csem vmx_set_mmap_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::nil)) Tint32.

    Definition vmx_init_spec_low: compatsem LDATAOps :=
      csem vmx_init_spec_low_step (type_of_list_type (Tint32::nil)) Tvoid.

    Definition vmx_run_vm_spec_low: compatsem LDATAOps :=
      asmsem vmx_run_vm vmx_run_vm_spec_low_step.

    Definition vmx_return_from_guest_spec_low: compatsem LDATAOps :=
      asmsem vmx_return_from_guest vmx_return_from_guest_spec_low_step.

  End WITHMEM.

End SPECIFICATION.