Library mcertikos.multithread.phbthread.ObjPHBThreadINTELVIRT

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Integers.
Require Import Values.
Require Import ASTExtra.
Require Import Constant.
Require Import Constant.
Require Import GlobIdent.

Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.

Require Import RealParams.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalRealIntelModule.

Require Import ObjInterruptDriver.
Require Import ObjConsole.
Require Import OracleInstances.
Require Import ObjSerialDriver.
Require Import ObjVMMDef.
Require Import CalTicketLock.
Require Import DeviceStateDataType.

Require Import AbstractDataType.
Require Import AuxSingleAbstractDataType.
Require Import ObjPHBFlatMem.
Require Import AlgebraicMem.
Require Import GlobalOracleProp.
Require Import SingleConfiguration.

Require Import Z64Lemma.

Require Import ObjEPT.
Require Import ObjVMCS.
Require Import ObjVMX.
Require Import BigLogThreadConfigFunction.

Section PHBSPECSIntelVirt.

  Context `{real_param_ops : RealParamsOps}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{threads_conf_ops: ThreadsConfigurationOps}.

  Section SINGLE_VIRT_SPECS.

    Function single_rdmsr_spec (r: Z) (adt: PData) : option Z64 :=
      match (ikern (snd adt), ihost (snd adt)) with
      | (true, true) ⇒ Some (VZ64 0)
      | _ ⇒ None
      end.

    Function single_wrmsr_spec (r: Z) (v: Z64) (adt: PData) :=
      match (ikern (snd adt), ihost (snd adt)) with
      | (true, true) ⇒ Some 0
      | _ ⇒ None
      end.

    Notation NOT_PROCBASED_INT_WINDOW_EXITING := 4294967291 % Z.
    Function single_vmx_set_intercept_intwin_spec (enable: Z) (adt: PData) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get C_VMCS_PRI_PROC_BASED_CTLS d with
                 | Vint ctrls ⇒
                   if zeq enable 1 then
                     let res := Z.lor (Int.unsigned ctrls) PROCBASED_INT_WINDOW_EXITING in
                     let d´ := ZMap.set C_VMCS_PRI_PROC_BASED_CTLS (Vint (Int.repr res)) d in
                     Some (sh_adt, pv_adt {pv_vmcs: (VMCSValid revid abrtid d´)})
                   else
                     let res := Z.land (Int.unsigned ctrls) NOT_PROCBASED_INT_WINDOW_EXITING in
                     let d´ := ZMap.set C_VMCS_PRI_PROC_BASED_CTLS (Vint (Int.repr res)) d in
                     Some (sh_adt, pv_adt {pv_vmcs: (VMCSValid revid abrtid d´)})
                 | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_set_desc1_spec (seg sel base: Z) (adt: PData) : option PData :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match vmx_set_desc1_aux seg sel base d with
                 | Some d´ ⇒ Some (sh_adt, pv_adt {pv_vmcs: (VMCSValid revid abrtid d´)})
                 | None ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_set_desc2_spec (seg lim ar: Z) (adt: PData) : option PData :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                match vmx_set_desc2_aux seg lim ar d with
                | Some d´ ⇒ Some (sh_adt, pv_adt {pv_vmcs: (VMCSValid revid abrtid d´)})
                | None ⇒ None
                end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_inject_event_spec (type vector errcode ev : Z) (adt: PData) : option PData :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get C_VMCS_ENTRY_INTR_INFO d with
                 | Vint intr_info ⇒
                   let i := Int.unsigned intr_info in
                   let is_invalid := Z.land i VMCS_INTERRUPTION_INFO_VALID in
                   if zeq is_invalid 0 then
                     let i1 := Z.lor VMCS_INTERRUPTION_INFO_VALID type in
                     let i2 := Z.lor i1 vector in
                     if zeq ev 1 then
                       let i3 := Z.lor i2 VMCS_INTERRUPTION_INFO_EV in
                       let d1 := ZMap.set C_VMCS_ENTRY_INTR_INFO (Vint (Int.repr i3)) d in
                       let d2 := ZMap.set C_VMCS_ENTRY_EXCEPTION_ERROR (Vint (Int.repr errcode)) d1 in
                       Some (sh_adt, pv_adt {pv_vmcs: (VMCSValid revid abrtid d2)})
                     else
                       let d1 := ZMap.set C_VMCS_ENTRY_INTR_INFO (Vint (Int.repr i2)) d in
                       Some (sh_adt, pv_adt {pv_vmcs: (VMCSValid revid abrtid d1)})
                   else
                     Some adt
                  | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_set_tsc_offset_spec (tsc_offset: Z64) (adt: PData) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 Some (sh_adt, pv_adt {pv_vmcs: (VMCSValid revid abrtid (write64_aux C_VMCS_TSC_OFFSET tsc_offset d))})
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_tsc_offset_spec (adt: PData): option Z64 :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get C_VMCS_TSC_OFFSET d, ZMap.get (C_VMCS_TSC_OFFSET + 1) d with
                 | Vint v1, Vint v2 ⇒ Some (VZ64 (Z64ofwords (Int.unsigned v2) (Int.unsigned v1)))
                 | _ , _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_exit_reason_spec (adt: PData) : option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get C_VMCS_EXIT_REASON d with
                 | Vint r ⇒ Some (Z.land (Int.unsigned r) EXIT_REASON_MASK)
                 | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_exit_fault_addr_spec (adt: PData): option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get C_VMCS_GUEST_PHYSICAL_ADDRESS d with
                 | Vint v ⇒ Some (Int.unsigned v)
                 | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_exit_qualification_spec (adt: PData): option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (ZMap.get VMX_EXIT_QUALIFICATION´ (vmx pv_adt)) with
               | Vint v ⇒ Some (Int.unsigned v)
               |_ ⇒ None
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_check_pending_event_spec (adt: PData) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get C_VMCS_ENTRY_INTR_INFO d with
                 | Vint ctrls ⇒
                   if zeq (Z.land (Int.unsigned ctrls) VMCS_INTERRUPTION_INFO_VALID) 0 then
                     Some 0
                   else Some 1
                 | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_check_int_shadow_spec (adt: PData) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get C_VMCS_GUEST_INTERRUPTIBILITY d with
                 | Vint ctrls ⇒
                   if zeq (Z.land (Int.unsigned ctrls) VMCS_INTERRUPTIBILITY_STI_or_MOVSS_BLOCKING) 0 then Some 0 else Some 1
                 | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_reg_spec (reg: Z) (adt: PData) : option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match Z2reg_type reg with
               | Some (TVMX z) ⇒
                 match ZMap.get z (vmx pv_adt) with
                 | Vint v ⇒ Some (Int.unsigned v)
                 | _ ⇒ None
                 end
               | Some (TVMCS z) ⇒
                 match (vmcs pv_adt) with
                 | VMCSValid revid abrtid d ⇒
                   match ZMap.get z d with
                   | Vint v ⇒ Some (Int.unsigned v)
                   | _ ⇒ None
                   end
                 end
               | _ ⇒ None
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_set_reg_spec (reg v: Z) (adt: PData): option PData :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
             match Z2reg_type reg with
             | Some (TVMX z) ⇒ Some (sh_adt, pv_adt {pv_vmx: ZMap.set z (Vint (Int.repr v)) (vmx pv_adt)})
               | Some (TVMCS z) ⇒
                 match (vmcs pv_adt) with
                   | VMCSValid revid abrtid d ⇒
                     Some (sh_adt, pv_adt {pv_vmcs: VMCSValid revid abrtid (ZMap.set z (Vint (Int.repr v)) d)})
                 end
               | _ ⇒ None
             end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_next_eip_spec (adt: PData) : option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get VMX_G_RIP´ (vmx pv_adt) with
                 | Vint v1 ⇒
                   match ZMap.get C_VMCS_EXIT_INSTRUCTION_LENGTH d with
                   | Vint v2 ⇒ Some (Int.unsigned v1 + Int.unsigned v2)
                   | _ ⇒ None
                   end
                 | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_io_width_spec (adt: PData): option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match ZMap.get VMX_EXIT_QUALIFICATION´ (vmx pv_adt) with
               | Vint v ⇒
                 let qsize := Z.land (Int.unsigned v) EXIT_QUAL_IO_SIZE in
                 if zeq qsize EXIT_QUAL_IO_ONE_BYTE then Some SZ8
                 else if zeq qsize EXIT_QUAL_IO_TWO_BYTE then Some SZ16
                      else Some SZ32
               |_ ⇒ None
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_io_write_spec (adt: PData): option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
             match ZMap.get VMX_EXIT_QUALIFICATION´ (vmx pv_adt) with
             | Vint v ⇒
               let qdir := (Z.land (Z.shiftr (Int.unsigned v) EXIT_QUAL_IO_DIR) 1) in
               if zeq qdir EXIT_QUAL_IO_IN then Some 0
               else Some 1
             |_ ⇒ None
             end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_exit_io_rep_spec (adt: PData): option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match ZMap.get VMX_EXIT_QUALIFICATION´ (vmx pv_adt) with
               | Vint v ⇒
                 let qrep := Z.land (Z.shiftr (Int.unsigned v) EXIT_QUAL_IO_REP) 1 in
                 Some qrep
               |_ ⇒ None
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_exit_io_str_spec (adt: PData): option Z :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match ZMap.get VMX_EXIT_QUALIFICATION´ (vmx pv_adt) with
               | Vint v ⇒
                 let qrep := Z.land (Z.shiftr (Int.unsigned v) EXIT_QUAL_IO_STR) 1 in
                 Some qrep
               |_ ⇒ None
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_get_exit_io_port_spec (adt: PData) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
            | (true, true, true, true) ⇒
              if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
                match ZMap.get VMX_EXIT_QUALIFICATION´ (vmx pv_adt) with
                | Vint v ⇒
                  Some ((Int.unsigned v) / C_EXIT_QUAL_IO_PORT)
                | _ ⇒ None
                end
              else None
            | _ ⇒ None
            end
      else None.


    Function single_ept_add_mapping_spec (gpa hpa : Z) (memtype: Z) (adt: PData) : option (PData × Z) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 gpa maxpage then
               if zle_lt 0 hpa maxpage then
                 if zle_lt 0 memtype 4096 then
                   let pml4 := EPT_PML4_INDEX gpa in
                   let pdpt := EPT_PDPT_INDEX gpa in
                   let pdir := EPT_PDIR_INDEX gpa in
                   let ptab := EPT_PTAB_INDEX gpa in
                   match ZMap.get pml4 (ept pv_adt) with
                   | EPML4EValid epdpt ⇒
                     match ZMap.get pdpt epdpt with
                     | EPDPTEValid epdt ⇒
                       match ZMap.get pdir epdt with
                       | EPDTEValid eptab ⇒
                         let va := Z.lor (Z.lor (Z.land hpa EPT_ADDR_MASK) EPT_PG_IGNORE_PAT_or_PERM)
                                         (Z.shiftl memtype EPT_PG_MEMORY_TYPE) in
                         let eptab´ := ZMap.set ptab (EPTEValid va) eptab in
                         let epdt´ := ZMap.set pdir (EPDTEValid eptab´) epdt in
                         let pdpte´ := ZMap.set pdpt (EPDPTEValid epdt´) epdpt in
                         let ept´ := ZMap.set pml4 (EPML4EValid pdpte´) (ept pv_adt) in
                         Some ((sh_adt, pv_adt {pv_ept: ept´}), 0)
                       | _ ⇒ None
                       end
                     | _ ⇒ None
                     end
                   | _ ⇒ None
                   end
                 else None
               else None
             else None
           | _ ⇒ None
           end
      else None.

    Function single_ept_invalidate_mappings_spec (adt: PData) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, ihost pv_adt) with
             | (true, true, true) ⇒ Some 0
             | _ ⇒ None
           end
      else None.

    Function single_vmx_set_mmap_spec (gpa : Z) (hpa : Z) (mem_type: Z) (adt: PData) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match single_ept_add_mapping_spec gpa hpa mem_type adt with
           | Some (adt´, res) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               if zle_le 0 res Int.max_unsigned then
                 if zle_lt 0 mem_type 4096 then
                   if zeq res 0 then
                     match single_ept_invalidate_mappings_spec adt´ with
                     | Some z ⇒ Some (adt´, z)
                     | _ ⇒ None
                 end
                   else Some (adt´, res)
                 else None
               else None
             else None
           | _ ⇒ None
           end
      else None.


    Definition single_vm_run_spec (rs: regset) (adt: PData) : option (PData × regset) :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (ikern pv_adt, pg sh_adt, ihost pv_adt, init sh_adt) with
           | (true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 match ZMap.get VMX_G_RIP´ (vmx pv_adt) with
                 | Vint v ⇒
                   let d´ := ZMap.set C_VMCS_GUEST_RIP (Vint v) d in
                   let vvmx := (vmx pv_adt) in
                   let rs´ := (Pregmap.init Vundef)
                                # EAX <- (ZMap.get VMX_G_RAX´ vvmx) # EBX <- (ZMap.get VMX_G_RBX´ vvmx)
                                # EDX <- (ZMap.get VMX_G_RDX´ vvmx) # ESI <- (ZMap.get VMX_G_RSI´ vvmx)
                                # EDI <- (ZMap.get VMX_G_RDI´ vvmx) # EBP <- (ZMap.get VMX_G_RBP´ vvmx)
                                # RA <- (ZMap.get VMX_G_RIP´ vvmx) in
                   let vvmx1 := ZMap.set VMX_HOST_EBP´ (rs EBP) vvmx in
                   let vvmx2 := ZMap.set VMX_HOST_EDI´ (rs EDI) vvmx1 in
                   Some ((sh_adt, pv_adt {pv_vmx: vvmx2} {pv_vmcs: VMCSValid revid abrtid d´} {pv_ihost: false}), rs´)
                 | _ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_return_from_guest_spec (adt: PData) : option PData :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, ikern pv_adt, pg sh_adt, ihost pv_adt) with
           | (true, true, true, false) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               match (vmcs pv_adt) with
               | VMCSValid revid abrtid d ⇒
                 let vvmx := (vmx pv_adt) in
                 match ZMap.get C_VMCS_GUEST_RIP d, ZMap.get C_VMCS_EXIT_REASON d,
                       ZMap.get C_VMCS_EXIT_QUALIFICATION d with
                 | Vint v1, Vint v2, Vint v3 ⇒
                   let vvmx1 := ZMap.set VMX_G_RIP´ (Vint v1) vvmx in
                   let vvmx2 := ZMap.set VMX_EXIT_REASON´ (Vint v2) vvmx1 in
                   let vvmx3 := ZMap.set VMX_EXIT_QUALIFICATION´ (Vint v3) vvmx2 in
                   let vvmx4 := ZMap.set VMX_LAUNCHED´ Vone vvmx3 in
                   Some (sh_adt, pv_adt {pv_ihost: true} {pv_vmx: vvmx4})
                 | _,_,_ ⇒ None
                 end
               end
             else None
           | _ ⇒ None
           end
      else None.

    Function single_vmx_init_spec
             (pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b: block)
             (adt: PData) : option PData :=
      let sh_adt := fst adt in
      let pv_adt := snd adt in
      if zeq (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) vm_handling_cid
      then match (init sh_adt, pg sh_adt, in_intr pv_adt, ikern pv_adt, ihost pv_adt, ipt pv_adt) with
           | (true, true, true, true, true, true) ⇒
             if zle_lt 0 (CPU_ID sh_adt) NUM_VMS then
               if zle_lt 0 (ZMap.get (CPU_ID sh_adt) (cid sh_adt)) num_proc then
                 Some (sh_adt, ((pv_adt {pv_ept: (Calculate_EPDPTE 3 (ZMap.set 0 (EPML4EValid (ZMap.init EPDPTEUndef))
                                                                               (ept pv_adt)))})
                                  {pv_vmcs: (Calculate_VMCS_at_i (CPU_ID sh_adt)
                                                                 (ZMap.get (CPU_ID sh_adt) (cid sh_adt))
                                                                 (vmcs pv_adt)
                                                                 real_vmxinfo pml4ept_b stack_b idt_b
                                                                 msr_bitmap_b io_bitmap_b host_rip_b) })
                                 {pv_vmx: (Calculate_VMX_at_i (vmx pv_adt))})
               else None
             else None
           | _ ⇒ None
           end
      else None.

  End SINGLE_VIRT_SPECS.

End PHBSPECSIntelVirt.