Library mcertikos.objects.tmobj.ObjTMVMXINIT

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.

Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalRealIntelModule.
Require Import CalTicketLock.
Require Import liblayers.compat.CompatGenSem.
Require Import ObjEPT.
Require Import ObjVMX.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Require Import SingleOracle.

Section OBJ_VMXINIT.

  Context `{real_params: RealParams}.
  Context `{thread_conf_ops: ThreadsConfigurationOps}.

  Function thread_vmx_init_spec
           (pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b: block)
           (adt: RData) : option RData :=
    if zeq (ZMap.get (CPU_ID adt) (cid adt)) vm_handling_cid
    then vmx_init_spec pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b adt
    else None.

End OBJ_VMXINIT.

Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import IntelPrimSemantics.
Require Import AuxLemma.

Section OBJ_SIM.

  Context `{data : CompatData RData}.
  Context `{data0 : CompatData RData}.

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

  Notation HDATAOps := (cdata (cdata_prf := data) RData).
  Notation LDATAOps := (cdata (cdata_prf := data0) RData).

  Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
                               (stencil_ops:= stencil_ops) HDATAOps LDATAOps}.

  Lemma val_inject_vint_eq:
    ∀ f n v v´ i,
      val_inject f (ZMap.get n v) (ZMap.get n v´)
      → ZMap.get n v = Vint i
      → ZMap.get n v´ = Vint i.
  Proof.
    intros.
    rewrite H0 in H; inversion H; reflexivity.
  Qed.

  Section THREAD_VMX_INIT_SIM.

    Context `{thread_conf_ops: ThreadsConfigurationOps}.

    Context `{real_params: RealParams}.

    Context {re1: relate_impl_iflags}.
    Context {re2: relate_impl_vmx}.
    Context {re3: relate_impl_vmcs}.
    Context {re4: relate_impl_ipt}.
    Context {re7: relate_impl_init}.
    Context {re15: relate_impl_cid}.
    Context {re18: relate_impl_ept}.
    Context {re22: relate_impl_in_intr}.
    Context {re23: relate_impl_CPU_ID}.
    Context {re24: relate_impl_vmcs}.
    Context {re25: relate_impl_vmx}.

    Let block_inject_neutral f b :=
      ∀ ofs, val_inject f (Vptr b ofs) (Vptr b ofs).

    Lemma thread_vmx_init_exist:
      ∀ s habd habd´ labd pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b f,
        thread_vmx_init_spec pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b habd = Some habd´
        → relate_AbData s f habd labd
        → block_inject_neutral f pm4ept_b
        → block_inject_neutral f stack_b
        → block_inject_neutral f idt_b
        → block_inject_neutral f msr_bitmap_b
        → block_inject_neutral f io_bitmap_b
        → block_inject_neutral f host_rip_b
        → ∃ labd´, thread_vmx_init_spec pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b labd = Some labd´
                         ∧ relate_AbData s f habd´ labd´.
    Proof.
      unfold thread_vmx_init_spec; intros.
      exploit relate_impl_CPU_ID_eq; eauto; inversion 1.
      exploit relate_impl_cid_eq; eauto; inversion 1.
      revert H; subrewrite; subdestruct.
      eauto using vmx_init_exist.
    Qed.

    Context {mt2: match_impl_vmx}.
    Context {mt3: match_impl_vmcs}.
    Context {mt18: match_impl_ept}.

    Lemma thread_vmx_init_match:
      ∀ s d d´ m pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b f,
        thread_vmx_init_spec pm4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b d = Some d´
        → match_AbData s d m f
        → match_AbData s d´ m f.
    Proof.
      unfold thread_vmx_init_spec; intros.
      subdestruct; inv H; trivial.
      eauto using vmx_init_match.
    Qed.

    Context {inv: VMCSSetDefaultsInvariants (data_ops := data_ops) thread_vmx_init_spec}.
    Context {inv0: VMCSSetDefaultsInvariants (data_ops := data_ops0) thread_vmx_init_spec}.

    Lemma inject_incr_block_inject_neutral_snd s f i b :
      find_symbol s i = Some b
      → inject_incr (Mem.flat_inj (genv_next s)) f
      → block_inject_neutral f b.
    Proof.
      unfold block_inject_neutral;
      intros symbol_exists incr ?.
      apply val_inject_ptr with 0%Z.
      - apply incr.
        unfold Mem.flat_inj.
        destruct (plt b (genv_next s)); try reflexivity.
        contradict n.
        eapply genv_symb_range; eassumption.
      - symmetry; apply Int.add_zero.
    Qed.

    Lemma thread_vmx_init_sim :
      ∀ id,
        sim (crel RData RData) (id ↦ vmcs_set_defaults_compatsem thread_vmx_init_spec)
            (id ↦ vmcs_set_defaults_compatsem thread_vmx_init_spec).
    Proof.
      intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
      exploit thread_vmx_init_exist; eauto 2 using inject_incr_block_inject_neutral_snd.

      intros [labd´ [HP HM]].
      match_external_states_simpl.
      eapply thread_vmx_init_match; eauto.
    Qed.

  End THREAD_VMX_INIT_SIM.

End OBJ_SIM.